%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : KRS080+1 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 10:08:25 EDT 2024 % Result : Unsatisfiable 12.28s 12.40s % Output : CNFRefutation 12.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : KRS080+1 : TPTP v8.2.0. Released v3.1.0. % 0.10/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.32 % Computer : n003.cluster.edu % 0.10/0.32 % Model : x86_64 x86_64 % 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.32 % Memory : 8042.1875MB % 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.32 % CPULimit : 300 % 0.10/0.32 % WCLimit : 300 % 0.10/0.32 % DateTime : Wed Jun 19 14:31:09 EDT 2024 % 0.16/0.32 % CPUTime : % 0.17/0.54 start to proof:theBenchmark % 12.28/12.39 %------------------------------------------- % 12.28/12.39 % File :CSE---1.7 % 12.28/12.39 % Problem :theBenchmark % 12.28/12.39 % Transform :cnf % 12.28/12.39 % Format :tptp:raw % 12.28/12.39 % Command :java -jar mcs_scs.jar %d %s % 12.28/12.39 % 12.28/12.39 % Result :Theorem 3.600000s % 12.28/12.39 % Output :CNFRefutation 3.600000s % 12.28/12.39 %------------------------------------------- % 12.28/12.40 %------------------------------------------------------------------------------ % 12.28/12.40 % File : KRS080+1 : TPTP v8.2.0. Released v3.1.0. % 12.28/12.40 % Domain : Knowledge Representation (Semantic Web) % 12.28/12.40 % Problem : DL Test: t3.2 % 12.28/12.40 % Version : Especial. % 12.28/12.40 % English : % 12.28/12.40 % 12.28/12.40 % Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe % 12.28/12.40 % : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW % 12.28/12.40 % Source : [Bec03] % 12.28/12.40 % Names : inconsistent_description-logic-Manifest019 [Bec03] % 12.28/12.40 % 12.28/12.40 % Status : Unsatisfiable % 12.28/12.40 % Rating : 0.14 v8.2.0, 0.00 v5.5.0, 0.33 v5.4.0, 0.00 v3.1.0 % 12.28/12.40 % Syntax : Number of formulae : 21 ( 1 unt; 0 def) % 12.28/12.40 % Number of atoms : 86 ( 19 equ) % 12.28/12.40 % Maximal formula atoms : 28 ( 4 avg) % 12.28/12.40 % Number of connectives : 71 ( 6 ~; 11 |; 34 &) % 12.28/12.40 % ( 2 <=>; 18 =>; 0 <=; 0 <~>) % 12.28/12.40 % Maximal formula depth : 17 ( 5 avg) % 12.28/12.40 % Maximal term depth : 1 ( 1 avg) % 12.28/12.40 % Number of predicates : 13 ( 12 usr; 0 prp; 1-2 aty) % 12.28/12.40 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 12.28/12.40 % Number of variables : 46 ( 39 !; 7 ?) % 12.28/12.40 % SPC : FOF_UNS_RFO_SEQ % 12.28/12.40 % 12.28/12.40 % Comments : Sean Bechhofer says there are some errors in the encoding of % 12.28/12.40 % datatypes, so this problem may not be perfect. At least it's % 12.28/12.40 % still representative of the type of reasoning required for OWL. % 12.28/12.40 % : There are 301 possible partitions in the unsatisfiable case % 12.28/12.40 %------------------------------------------------------------------------------ % 12.28/12.40 fof(cUnsatisfiable_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & cUnsatisfiable(A) ) % 12.28/12.40 => cUnsatisfiable(B) ) ). % 12.28/12.40 % 12.28/12.40 fof(cowlNothing_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & cowlNothing(A) ) % 12.28/12.40 => cowlNothing(B) ) ). % 12.28/12.40 % 12.28/12.40 fof(cowlThing_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & cowlThing(A) ) % 12.28/12.40 => cowlThing(B) ) ). % 12.28/12.40 % 12.28/12.40 fof(cp_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & cp(A) ) % 12.28/12.40 => cp(B) ) ). % 12.28/12.40 % 12.28/12.40 fof(cp1_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & cp1(A) ) % 12.28/12.40 => cp1(B) ) ). % 12.28/12.40 % 12.28/12.40 fof(cp2_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & cp2(A) ) % 12.28/12.40 => cp2(B) ) ). % 12.28/12.40 % 12.28/12.40 fof(cp3_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & cp3(A) ) % 12.28/12.40 => cp3(B) ) ). % 12.28/12.40 % 12.28/12.40 fof(cp4_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & cp4(A) ) % 12.28/12.40 => cp4(B) ) ). % 12.28/12.40 % 12.28/12.40 fof(cp5_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & cp5(A) ) % 12.28/12.40 => cp5(B) ) ). % 12.28/12.40 % 12.28/12.40 fof(rr_substitution_1,axiom, % 12.28/12.40 ! [A,B,C] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & rr(A,C) ) % 12.28/12.40 => rr(B,C) ) ). % 12.28/12.40 % 12.28/12.40 fof(rr_substitution_2,axiom, % 12.28/12.40 ! [A,B,C] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & rr(C,A) ) % 12.28/12.40 => rr(C,B) ) ). % 12.28/12.40 % 12.28/12.40 fof(xsd_integer_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & xsd_integer(A) ) % 12.28/12.40 => xsd_integer(B) ) ). % 12.28/12.40 % 12.28/12.40 fof(xsd_string_substitution_1,axiom, % 12.28/12.40 ! [A,B] : % 12.28/12.40 ( ( A = B % 12.28/12.40 & xsd_string(A) ) % 12.28/12.40 => xsd_string(B) ) ). % 12.28/12.40 % 12.28/12.40 %----Thing and Nothing % 12.28/12.40 fof(axiom_0,axiom, % 12.28/12.40 ! [X] : % 12.28/12.40 ( cowlThing(X) % 12.28/12.40 & ~ cowlNothing(X) ) ). % 12.28/12.40 % 12.28/12.40 %----String and Integer disjoint % 12.28/12.40 fof(axiom_1,axiom, % 12.28/12.40 ! [X] : % 12.28/12.40 ( xsd_string(X) % 12.28/12.40 <=> ~ xsd_integer(X) ) ). % 12.28/12.40 % 12.28/12.40 %----Equality cUnsatisfiable % 12.28/12.40 fof(axiom_2,axiom, % 12.28/12.40 ! [X] : % 12.28/12.40 ( cUnsatisfiable(X) % 12.28/12.40 <=> ( ? [Y] : % 12.28/12.40 ( rr(X,Y) % 12.28/12.40 & cp(Y) % 12.28/12.40 & cp1(Y) ) % 12.28/12.40 & ? [Y] : % 12.28/12.40 ( rr(X,Y) % 12.28/12.40 & cp1(Y) ) % 12.28/12.40 & ? [Y] : % 12.28/12.40 ( rr(X,Y) % 12.28/12.40 & cp4(Y) ) % 12.28/12.40 & ! [Y0,Y1,Y2,Y3] : % 12.28/12.40 ( ( rr(X,Y0) % 12.28/12.40 & rr(X,Y1) % 12.28/12.40 & rr(X,Y2) % 12.28/12.40 & rr(X,Y3) ) % 12.28/12.40 => ( Y0 = Y1 % 12.28/12.40 | Y0 = Y2 % 12.28/12.40 | Y0 = Y3 % 12.28/12.40 | Y1 = Y2 % 12.28/12.40 | Y1 = Y3 % 12.28/12.40 | Y2 = Y3 ) ) % 12.28/12.40 & ? [Y] : % 12.28/12.40 ( rr(X,Y) % 12.28/12.40 & cp2(Y) ) % 12.28/12.40 & ? [Y] : % 12.28/12.40 ( rr(X,Y) % 12.28/12.40 & cp3(Y) ) % 12.28/12.40 & ? [Y] : % 12.28/12.40 ( rr(X,Y) % 12.28/12.40 & cp(Y) % 12.28/12.40 & cp3(Y) ) % 12.28/12.40 & ? [Y] : % 12.28/12.40 ( rr(X,Y) % 12.28/12.40 & cp2(Y) % 12.28/12.40 & cp(Y) ) ) ) ). % 12.28/12.40 % 12.28/12.40 %----Super cp1 % 12.28/12.40 fof(axiom_3,axiom, % 12.28/12.40 ! [X] : % 12.28/12.40 ( cp1(X) % 12.28/12.40 => ~ ( cp2(X) % 12.28/12.40 | cp4(X) % 12.28/12.40 | cp5(X) % 12.28/12.40 | cp3(X) ) ) ). % 12.28/12.40 % 12.28/12.40 %----Super cp2 % 12.28/12.40 fof(axiom_4,axiom, % 12.28/12.40 ! [X] : % 12.28/12.40 ( cp2(X) % 12.28/12.40 => ~ ( cp4(X) % 12.28/12.40 | cp5(X) % 12.28/12.40 | cp3(X) ) ) ). % 12.28/12.40 % 12.28/12.40 %----Super cp3 % 12.28/12.40 fof(axiom_5,axiom, % 12.28/12.40 ! [X] : % 12.28/12.40 ( cp3(X) % 12.28/12.40 => ~ ( cp4(X) % 12.28/12.40 | cp5(X) ) ) ). % 12.28/12.40 % 12.28/12.40 %----Super cp4 % 12.28/12.40 fof(axiom_6,axiom, % 12.28/12.40 ! [X] : % 12.28/12.40 ( cp4(X) % 12.28/12.40 => ~ cp5(X) ) ). % 12.28/12.40 % 12.28/12.40 %----i2003_11_14_17_19_21224 % 12.28/12.40 fof(axiom_7,axiom, % 12.28/12.40 cUnsatisfiable(i2003_11_14_17_19_21224) ). % 12.28/12.40 % 12.28/12.40 %------------------------------------------------------------------------------ % 12.28/12.40 %------------------------------------------- % 12.28/12.40 % Proof found % 12.28/12.40 % SZS status Theorem for theBenchmark % 12.28/12.40 % SZS output start Proof % 12.28/12.40 %ClaNum:68(EqnAxiom:26) % 12.28/12.40 %VarNum:357(SingletonVarNum:115) % 12.28/12.40 %MaxLitNum:19 % 12.28/12.40 %MaxfuncDepth:1 % 12.28/12.40 %SharedTerms:2 % 12.28/12.40 [27]P1(a1) % 12.28/12.40 [28]~P2(x281) % 12.28/12.40 [29]P11(x291)+P3(x291) % 12.28/12.40 [30]~P6(x301)+~P4(x301) % 12.28/12.40 [31]~P7(x311)+~P4(x311) % 12.28/12.40 [32]~P8(x321)+~P4(x321) % 12.28/12.40 [33]~P9(x331)+~P4(x331) % 12.28/12.40 [34]~P7(x341)+~P6(x341) % 12.28/12.40 [35]~P8(x351)+~P6(x351) % 12.28/12.40 [36]~P9(x361)+~P6(x361) % 12.28/12.40 [37]~P8(x371)+~P7(x371) % 12.28/12.40 [38]~P9(x381)+~P7(x381) % 12.28/12.40 [39]~P9(x391)+~P8(x391) % 12.28/12.40 [40]~P11(x401)+~P3(x401) % 12.28/12.40 [41]~P1(x411)+P5(f2(x411)) % 12.28/12.40 [42]~P1(x421)+P5(f5(x421)) % 12.28/12.40 [43]~P1(x431)+P5(f10(x431)) % 12.28/12.40 [44]~P1(x441)+P4(f2(x441)) % 12.28/12.40 [45]~P1(x451)+P4(f6(x451)) % 12.28/12.40 [46]~P1(x461)+P6(f7(x461)) % 12.28/12.40 [47]~P1(x471)+P6(f10(x471)) % 12.28/12.40 [48]~P1(x481)+P7(f9(x481)) % 12.28/12.40 [49]~P1(x491)+P7(f5(x491)) % 12.28/12.40 [50]~P1(x501)+P8(f8(x501)) % 12.28/12.40 [51]~P1(x511)+P10(x511,f2(x511)) % 12.28/12.40 [52]~P1(x521)+P10(x521,f6(x521)) % 12.28/12.40 [53]~P1(x531)+P10(x531,f8(x531)) % 12.28/12.40 [54]~P1(x541)+P10(x541,f7(x541)) % 12.28/12.40 [55]~P1(x551)+P10(x551,f9(x551)) % 12.28/12.40 [56]~P1(x561)+P10(x561,f5(x561)) % 12.28/12.40 [57]~P1(x571)+P10(x571,f10(x571)) % 12.28/12.40 [58]E(x583,x581)+E(x584,x581)+E(x584,x583)+~P10(x585,x582)+~P10(x585,x581)+~P10(x585,x583)+~P10(x585,x584)+E(x581,x582)+E(x583,x582)+E(x584,x582)+~P1(x585) % 12.28/12.40 [59]~P7(x593)+~P10(x591,x594)+~P10(x591,x595)+~P10(x591,x598)+~P10(x591,x596)+~P10(x591,x597)+~P10(x591,x593)+~P10(x591,x592)+~P6(x592)+~P4(x594)+P1(x591)+~P5(x592)+~P5(x593)+~P5(x594)+~P4(x595)+~P6(x596)+~P7(x597)+~P8(x598)+~E(f11(x591),f12(x591)) % 12.28/12.40 [60]~P7(x603)+~P10(x601,x604)+~P10(x601,x605)+~P10(x601,x608)+~P10(x601,x606)+~P10(x601,x607)+~P10(x601,x603)+~P10(x601,x602)+~P6(x602)+~P4(x604)+P1(x601)+~P5(x602)+~P5(x603)+~P5(x604)+~P4(x605)+~P6(x606)+~P7(x607)+~P8(x608)+~E(f3(x601),f12(x601)) % 12.28/12.40 [61]~P7(x613)+~P10(x611,x614)+~P10(x611,x615)+~P10(x611,x618)+~P10(x611,x616)+~P10(x611,x617)+~P10(x611,x613)+~P10(x611,x612)+~P6(x612)+~P4(x614)+P1(x611)+~P5(x612)+~P5(x613)+~P5(x614)+~P4(x615)+~P6(x616)+~P7(x617)+~P8(x618)+~E(f3(x611),f11(x611)) % 12.28/12.40 [62]~P7(x623)+~P10(x621,x624)+~P10(x621,x625)+~P10(x621,x628)+~P10(x621,x626)+~P10(x621,x627)+~P10(x621,x623)+~P10(x621,x622)+~P6(x622)+~P4(x624)+P1(x621)+~P5(x622)+~P5(x623)+~P5(x624)+~P4(x625)+~P6(x626)+~P7(x627)+~P8(x628)+~E(f4(x621),f12(x621)) % 12.28/12.40 [63]~P7(x633)+~P10(x631,x634)+~P10(x631,x635)+~P10(x631,x638)+~P10(x631,x636)+~P10(x631,x637)+~P10(x631,x633)+~P10(x631,x632)+~P6(x632)+~P4(x634)+P1(x631)+~P5(x632)+~P5(x633)+~P5(x634)+~P4(x635)+~P6(x636)+~P7(x637)+~P8(x638)+~E(f4(x631),f11(x631)) % 12.28/12.40 [64]~P7(x643)+~P10(x641,x644)+~P10(x641,x645)+~P10(x641,x648)+~P10(x641,x646)+~P10(x641,x647)+~P10(x641,x643)+~P10(x641,x642)+~P6(x642)+~P4(x644)+P1(x641)+~P5(x642)+~P5(x643)+~P5(x644)+~P4(x645)+~P6(x646)+~P7(x647)+~P8(x648)+~E(f4(x641),f3(x641)) % 12.28/12.40 [65]~P7(x653)+~P10(x651,x654)+~P10(x651,x655)+~P10(x651,x658)+~P10(x651,x656)+~P10(x651,x657)+~P10(x651,x653)+~P10(x651,x652)+~P6(x652)+~P4(x654)+P1(x651)+~P5(x652)+~P5(x653)+~P5(x654)+~P4(x655)+~P6(x656)+~P7(x657)+~P8(x658)+P10(x651,f12(x651)) % 12.28/12.40 [66]~P7(x663)+~P10(x661,x664)+~P10(x661,x665)+~P10(x661,x668)+~P10(x661,x666)+~P10(x661,x667)+~P10(x661,x663)+~P10(x661,x662)+~P6(x662)+~P4(x664)+P1(x661)+~P5(x662)+~P5(x663)+~P5(x664)+~P4(x665)+~P6(x666)+~P7(x667)+~P8(x668)+P10(x661,f11(x661)) % 12.28/12.40 [67]~P7(x673)+~P10(x671,x674)+~P10(x671,x675)+~P10(x671,x678)+~P10(x671,x676)+~P10(x671,x677)+~P10(x671,x673)+~P10(x671,x672)+~P6(x672)+~P4(x674)+P1(x671)+~P5(x672)+~P5(x673)+~P5(x674)+~P4(x675)+~P6(x676)+~P7(x677)+~P8(x678)+P10(x671,f3(x671)) % 12.28/12.40 [68]~P7(x683)+~P10(x681,x684)+~P10(x681,x685)+~P10(x681,x688)+~P10(x681,x686)+~P10(x681,x687)+~P10(x681,x683)+~P10(x681,x682)+~P6(x682)+~P4(x684)+P1(x681)+~P5(x682)+~P5(x683)+~P5(x684)+~P4(x685)+~P6(x686)+~P7(x687)+~P8(x688)+P10(x681,f4(x681)) % 12.28/12.40 %EqnAxiom % 12.28/12.40 [1]E(x11,x11) % 12.28/12.40 [2]E(x22,x21)+~E(x21,x22) % 12.28/12.40 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 12.28/12.40 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 12.28/12.40 [5]~E(x51,x52)+E(f5(x51),f5(x52)) % 12.28/12.40 [6]~E(x61,x62)+E(f10(x61),f10(x62)) % 12.28/12.40 [7]~E(x71,x72)+E(f4(x71),f4(x72)) % 12.28/12.40 [8]~E(x81,x82)+E(f6(x81),f6(x82)) % 12.28/12.40 [9]~E(x91,x92)+E(f7(x91),f7(x92)) % 12.28/12.40 [10]~E(x101,x102)+E(f3(x101),f3(x102)) % 12.28/12.40 [11]~E(x111,x112)+E(f9(x111),f9(x112)) % 12.28/12.40 [12]~E(x121,x122)+E(f11(x121),f11(x122)) % 12.28/12.40 [13]~E(x131,x132)+E(f8(x131),f8(x132)) % 12.28/12.40 [14]~E(x141,x142)+E(f12(x141),f12(x142)) % 12.28/12.40 [15]~P1(x151)+P1(x152)+~E(x151,x152) % 12.28/12.40 [16]~P2(x161)+P2(x162)+~E(x161,x162) % 12.28/12.40 [17]~P3(x171)+P3(x172)+~E(x171,x172) % 12.28/12.41 [18]~P11(x181)+P11(x182)+~E(x181,x182) % 12.28/12.41 [19]~P4(x191)+P4(x192)+~E(x191,x192) % 12.28/12.41 [20]~P6(x201)+P6(x202)+~E(x201,x202) % 12.28/12.41 [21]P10(x212,x213)+~E(x211,x212)+~P10(x211,x213) % 12.28/12.41 [22]P10(x223,x222)+~E(x221,x222)+~P10(x223,x221) % 12.28/12.41 [23]~P7(x231)+P7(x232)+~E(x231,x232) % 12.28/12.41 [24]~P5(x241)+P5(x242)+~E(x241,x242) % 12.28/12.41 [25]~P8(x251)+P8(x252)+~E(x251,x252) % 12.28/12.41 [26]~P9(x261)+P9(x262)+~E(x261,x262) % 12.28/12.41 % 12.28/12.41 %------------------------------------------- % 12.28/12.41 cnf(88,plain, % 12.28/12.41 (~E(a1,x881)+P10(x881,f2(x881))), % 12.28/12.41 inference(scs_inference,[],[27,51,15])). % 12.28/12.41 cnf(89,plain, % 12.28/12.41 (P10(a1,f2(a1))), % 12.28/12.41 inference(equality_inference,[],[88])). % 12.28/12.41 cnf(100,plain, % 12.28/12.41 (~E(a1,x1001)+P10(x1001,f8(x1001))), % 12.28/12.41 inference(scs_inference,[],[27,53,15])). % 12.28/12.41 cnf(101,plain, % 12.28/12.41 (P10(a1,f8(a1))), % 12.28/12.41 inference(equality_inference,[],[100])). % 12.28/12.41 cnf(106,plain, % 12.28/12.41 (~E(a1,x1061)+P10(x1061,f7(x1061))), % 12.28/12.41 inference(scs_inference,[],[27,54,15])). % 12.28/12.41 cnf(107,plain, % 12.28/12.41 (P10(a1,f7(a1))), % 12.28/12.41 inference(equality_inference,[],[106])). % 12.28/12.41 cnf(118,plain, % 12.28/12.41 (~E(a1,x1181)+P10(x1181,f5(x1181))), % 12.28/12.41 inference(scs_inference,[],[27,56,15])). % 12.28/12.41 cnf(119,plain, % 12.28/12.41 (P10(a1,f5(a1))), % 12.28/12.41 inference(equality_inference,[],[118])). % 12.28/12.41 cnf(163,plain, % 12.28/12.41 (~P4(x1631)+~E(x1632,x1631)+~P6(x1632)), % 12.28/12.41 inference(scs_inference,[],[30,20])). % 12.28/12.41 cnf(167,plain, % 12.28/12.41 (~P4(f5(a1))), % 12.28/12.41 inference(scs_inference,[],[27,31,49])). % 12.28/12.41 cnf(172,plain, % 12.28/12.41 (~P4(f8(a1))), % 12.28/12.41 inference(scs_inference,[],[27,32,50])). % 12.28/12.41 cnf(186,plain, % 12.28/12.41 (~E(x1861,x1862)+~P7(x1862)+~P6(x1861)), % 12.28/12.41 inference(scs_inference,[],[34,20])). % 12.28/12.41 cnf(194,plain, % 12.28/12.41 (~E(x1941,x1942)+~P8(x1942)+~P6(x1941)), % 12.28/12.41 inference(scs_inference,[],[35,20])). % 12.28/12.41 cnf(202,plain, % 12.28/12.41 (~P8(f5(a1))), % 12.28/12.41 inference(scs_inference,[],[27,37,49])). % 12.28/12.41 cnf(228,plain, % 12.28/12.41 (~E(a1,x2281)+P4(f2(x2281))), % 12.28/12.41 inference(scs_inference,[],[27,44,15])). % 12.28/12.41 cnf(229,plain, % 12.28/12.41 (P4(f2(a1))), % 12.28/12.41 inference(equality_inference,[],[228])). % 12.28/12.41 cnf(233,plain, % 12.28/12.41 (~E(f2(a1),f5(a1))), % 12.28/12.41 inference(scs_inference,[],[27,167,44,19])). % 12.28/12.41 cnf(234,plain, % 12.28/12.41 (~E(f2(a1),f8(a1))), % 12.28/12.41 inference(scs_inference,[],[27,172,44,19])). % 12.28/12.41 cnf(242,plain, % 12.28/12.41 (~E(a1,x2421)+P6(f7(x2421))), % 12.28/12.41 inference(scs_inference,[],[27,46,15])). % 12.28/12.41 cnf(243,plain, % 12.28/12.41 (P6(f7(a1))), % 12.28/12.41 inference(equality_inference,[],[242])). % 12.28/12.41 cnf(244,plain, % 12.28/12.41 (~E(f7(a1),f2(a1))), % 12.28/12.41 inference(scs_inference,[],[229,243,163])). % 12.28/12.41 cnf(498,plain, % 12.28/12.41 (E(f7(a1),f5(a1))+E(f8(a1),f5(a1))+E(f7(a1),f8(a1))), % 12.28/12.41 inference(scs_inference,[],[101,119,107,89,244,233,234,27,58])). % 12.28/12.41 cnf(1117,plain, % 12.28/12.41 (E(f7(a1),f8(a1))+~P7(f5(a1))+E(f8(a1),f5(a1))), % 12.28/12.41 inference(scs_inference,[],[243,498,186])). % 12.28/12.41 cnf(1133,plain, % 12.28/12.41 (~P8(f8(a1))+E(f8(a1),f5(a1))+~P7(f5(a1))), % 12.28/12.41 inference(scs_inference,[],[243,1117,194])). % 12.28/12.41 cnf(1149,plain, % 12.28/12.41 (~P8(f8(a1))+~P7(f5(a1))), % 12.28/12.41 inference(scs_inference,[],[202,1133,25])). % 12.28/12.41 cnf(1165,plain, % 12.28/12.41 (~P7(f5(a1))), % 12.28/12.41 inference(scs_inference,[],[27,1149,50])). % 12.28/12.41 cnf(1166,plain, % 12.28/12.41 ($false), % 12.28/12.41 inference(scs_inference,[],[1165,27,49]), % 12.28/12.41 ['proof']). % 12.28/12.41 % SZS output end Proof % 12.28/12.41 % Total time :3.600000s %------------------------------------------------------------------------------