%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT381+3 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n025.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:19:17 EDT 2024 % Result : Theorem 2.25s 2.34s % Output : CNFRefutation 2.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : LAT381+3 : TPTP v8.2.0. Released v4.0.0. % 0.00/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.09/0.30 % Computer : n025.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Fri Jun 21 19:52:54 EDT 2024 % 0.09/0.30 % CPUTime : % 0.15/0.54 start to proof:theBenchmark % 2.25/2.33 %------------------------------------------- % 2.25/2.33 % File :CSE---1.7 % 2.25/2.33 % Problem :theBenchmark % 2.25/2.33 % Transform :cnf % 2.25/2.33 % Format :tptp:raw % 2.25/2.33 % Command :java -jar mcs_scs.jar %d %s % 2.25/2.33 % 2.25/2.33 % Result :Theorem 1.750000s % 2.25/2.33 % Output :CNFRefutation 1.750000s % 2.25/2.33 %------------------------------------------- % 2.25/2.33 %------------------------------------------------------------------------------ % 2.25/2.33 % File : LAT381+3 : TPTP v8.2.0. Released v4.0.0. % 2.25/2.33 % Domain : Lattice Theory % 2.25/2.33 % Problem : Tarski-Knaster fixed point theorem 01, 02 expansion % 2.25/2.33 % Version : Especial. % 2.25/2.33 % English : % 2.25/2.33 % 2.25/2.33 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 2.25/2.33 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 2.25/2.33 % : [VL+08] Verchinine et al. (2008), On Correctness of Mathematic % 2.25/2.33 % Source : [Pas08] % 2.25/2.33 % Names : tarski_01.02 [Pas08] % 2.25/2.33 % 2.25/2.33 % Status : Theorem % 2.25/2.33 % Rating : 0.06 v8.2.0, 0.08 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.03 v7.1.0, 0.00 v6.2.0, 0.04 v6.1.0, 0.13 v6.0.0, 0.09 v5.5.0, 0.04 v5.4.0, 0.07 v5.3.0, 0.11 v5.2.0, 0.05 v5.1.0, 0.19 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.1, 0.61 v4.0.0 % 2.25/2.33 % Syntax : Number of formulae : 17 ( 2 unt; 6 def) % 2.25/2.33 % Number of atoms : 86 ( 2 equ) % 2.25/2.33 % Maximal formula atoms : 22 ( 5 avg) % 2.25/2.33 % Number of connectives : 70 ( 1 ~; 2 |; 28 &) % 2.25/2.33 % ( 6 <=>; 33 =>; 0 <=; 0 <~>) % 2.25/2.33 % Maximal formula depth : 18 ( 7 avg) % 2.25/2.33 % Maximal term depth : 1 ( 1 avg) % 2.25/2.33 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 2.25/2.33 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 2.25/2.33 % Number of variables : 40 ( 39 !; 1 ?) % 2.25/2.33 % SPC : FOF_THM_RFO_SEQ % 2.25/2.33 % 2.25/2.33 % Comments : Problem generated by the SAD system [VLP07] % 2.25/2.33 %------------------------------------------------------------------------------ % 2.25/2.33 fof(mSetSort,axiom, % 2.25/2.33 ! [W0] : % 2.25/2.33 ( aSet0(W0) % 2.25/2.33 => $true ) ). % 2.25/2.33 % 2.25/2.33 fof(mElmSort,axiom, % 2.25/2.33 ! [W0] : % 2.25/2.33 ( aElement0(W0) % 2.25/2.33 => $true ) ). % 2.25/2.33 % 2.25/2.33 fof(mEOfElem,axiom, % 2.25/2.33 ! [W0] : % 2.25/2.33 ( aSet0(W0) % 2.25/2.33 => ! [W1] : % 2.25/2.33 ( aElementOf0(W1,W0) % 2.25/2.33 => aElement0(W1) ) ) ). % 2.25/2.33 % 2.25/2.33 fof(mDefEmpty,definition, % 2.25/2.33 ! [W0] : % 2.25/2.33 ( aSet0(W0) % 2.25/2.33 => ( isEmpty0(W0) % 2.25/2.33 <=> ~ ? [W1] : aElementOf0(W1,W0) ) ) ). % 2.25/2.33 % 2.25/2.33 fof(mDefSub,definition, % 2.25/2.33 ! [W0] : % 2.25/2.33 ( aSet0(W0) % 2.25/2.33 => ! [W1] : % 2.25/2.33 ( aSubsetOf0(W1,W0) % 2.25/2.33 <=> ( aSet0(W1) % 2.25/2.33 & ! [W2] : % 2.25/2.33 ( aElementOf0(W2,W1) % 2.25/2.33 => aElementOf0(W2,W0) ) ) ) ) ). % 2.25/2.33 % 2.25/2.33 fof(mLessRel,axiom, % 2.25/2.33 ! [W0,W1] : % 2.25/2.33 ( ( aElement0(W0) % 2.25/2.33 & aElement0(W1) ) % 2.25/2.33 => ( sdtlseqdt0(W0,W1) % 2.25/2.33 => $true ) ) ). % 2.25/2.33 % 2.25/2.33 fof(mARefl,axiom, % 2.25/2.33 ! [W0] : % 2.25/2.33 ( aElement0(W0) % 2.25/2.33 => sdtlseqdt0(W0,W0) ) ). % 2.25/2.33 % 2.25/2.33 fof(mASymm,axiom, % 2.25/2.33 ! [W0,W1] : % 2.25/2.33 ( ( aElement0(W0) % 2.25/2.33 & aElement0(W1) ) % 2.25/2.33 => ( ( sdtlseqdt0(W0,W1) % 2.25/2.33 & sdtlseqdt0(W1,W0) ) % 2.25/2.33 => W0 = W1 ) ) ). % 2.25/2.33 % 2.25/2.33 fof(mTrans,axiom, % 2.25/2.33 ! [W0,W1,W2] : % 2.25/2.33 ( ( aElement0(W0) % 2.25/2.33 & aElement0(W1) % 2.25/2.33 & aElement0(W2) ) % 2.25/2.33 => ( ( sdtlseqdt0(W0,W1) % 2.25/2.33 & sdtlseqdt0(W1,W2) ) % 2.25/2.33 => sdtlseqdt0(W0,W2) ) ) ). % 2.25/2.33 % 2.25/2.33 fof(mDefLB,definition, % 2.25/2.33 ! [W0] : % 2.25/2.33 ( aSet0(W0) % 2.25/2.33 => ! [W1] : % 2.25/2.33 ( aSubsetOf0(W1,W0) % 2.25/2.33 => ! [W2] : % 2.25/2.33 ( aLowerBoundOfIn0(W2,W1,W0) % 2.25/2.33 <=> ( aElementOf0(W2,W0) % 2.25/2.33 & ! [W3] : % 2.25/2.33 ( aElementOf0(W3,W1) % 2.25/2.33 => sdtlseqdt0(W2,W3) ) ) ) ) ) ). % 2.25/2.33 % 2.25/2.33 fof(mDefUB,definition, % 2.25/2.33 ! [W0] : % 2.25/2.33 ( aSet0(W0) % 2.25/2.33 => ! [W1] : % 2.25/2.33 ( aSubsetOf0(W1,W0) % 2.25/2.33 => ! [W2] : % 2.25/2.33 ( aUpperBoundOfIn0(W2,W1,W0) % 2.25/2.33 <=> ( aElementOf0(W2,W0) % 2.25/2.33 & ! [W3] : % 2.25/2.33 ( aElementOf0(W3,W1) % 2.25/2.33 => sdtlseqdt0(W3,W2) ) ) ) ) ) ). % 2.25/2.33 % 2.25/2.33 fof(mDefInf,definition, % 2.25/2.33 ! [W0] : % 2.25/2.33 ( aSet0(W0) % 2.25/2.33 => ! [W1] : % 2.25/2.33 ( aSubsetOf0(W1,W0) % 2.25/2.33 => ! [W2] : % 2.25/2.33 ( aInfimumOfIn0(W2,W1,W0) % 2.25/2.33 <=> ( aElementOf0(W2,W0) % 2.25/2.33 & aLowerBoundOfIn0(W2,W1,W0) % 2.25/2.34 & ! [W3] : % 2.25/2.34 ( aLowerBoundOfIn0(W3,W1,W0) % 2.25/2.34 => sdtlseqdt0(W3,W2) ) ) ) ) ) ). % 2.25/2.34 % 2.25/2.34 fof(mDefSup,definition, % 2.25/2.34 ! [W0] : % 2.25/2.34 ( aSet0(W0) % 2.25/2.34 => ! [W1] : % 2.25/2.34 ( aSubsetOf0(W1,W0) % 2.25/2.34 => ! [W2] : % 2.25/2.34 ( aSupremumOfIn0(W2,W1,W0) % 2.25/2.34 <=> ( aElementOf0(W2,W0) % 2.25/2.34 & aUpperBoundOfIn0(W2,W1,W0) % 2.25/2.34 & ! [W3] : % 2.25/2.34 ( aUpperBoundOfIn0(W3,W1,W0) % 2.25/2.34 => sdtlseqdt0(W2,W3) ) ) ) ) ) ). % 2.25/2.34 % 2.25/2.34 fof(m__725,hypothesis, % 2.25/2.34 aSet0(xT) ). % 2.25/2.34 % 2.25/2.34 fof(m__725_01,hypothesis, % 2.25/2.34 ( aSet0(xS) % 2.25/2.34 & ! [W0] : % 2.25/2.34 ( aElementOf0(W0,xS) % 2.25/2.34 => aElementOf0(W0,xT) ) % 2.25/2.34 & aSubsetOf0(xS,xT) ) ). % 2.25/2.34 % 2.25/2.34 fof(m__744,hypothesis, % 2.25/2.34 ( aElementOf0(xu,xT) % 2.25/2.34 & aElementOf0(xu,xT) % 2.25/2.34 & ! [W0] : % 2.25/2.34 ( aElementOf0(W0,xS) % 2.25/2.34 => sdtlseqdt0(W0,xu) ) % 2.25/2.34 & aUpperBoundOfIn0(xu,xS,xT) % 2.25/2.34 & ! [W0] : % 2.25/2.34 ( ( ( aElementOf0(W0,xT) % 2.25/2.34 & ! [W1] : % 2.25/2.34 ( aElementOf0(W1,xS) % 2.25/2.34 => sdtlseqdt0(W1,W0) ) ) % 2.25/2.34 | aUpperBoundOfIn0(W0,xS,xT) ) % 2.25/2.34 => sdtlseqdt0(xu,W0) ) % 2.25/2.34 & aSupremumOfIn0(xu,xS,xT) % 2.25/2.34 & aElementOf0(xv,xT) % 2.25/2.34 & aElementOf0(xv,xT) % 2.25/2.34 & ! [W0] : % 2.25/2.34 ( aElementOf0(W0,xS) % 2.25/2.34 => sdtlseqdt0(W0,xv) ) % 2.25/2.34 & aUpperBoundOfIn0(xv,xS,xT) % 2.25/2.34 & ! [W0] : % 2.25/2.34 ( ( ( aElementOf0(W0,xT) % 2.25/2.34 & ! [W1] : % 2.25/2.34 ( aElementOf0(W1,xS) % 2.25/2.34 => sdtlseqdt0(W1,W0) ) ) % 2.25/2.34 | aUpperBoundOfIn0(W0,xS,xT) ) % 2.25/2.34 => sdtlseqdt0(xv,W0) ) % 2.25/2.34 & aSupremumOfIn0(xv,xS,xT) ) ). % 2.25/2.34 % 2.25/2.34 fof(m__,conjecture, % 2.25/2.34 xu = xv ). % 2.25/2.34 % 2.25/2.34 %------------------------------------------------------------------------------ % 2.25/2.34 %------------------------------------------- % 2.25/2.34 % Proof found % 2.25/2.34 % SZS status Theorem for theBenchmark % 2.25/2.34 % SZS output start Proof % 2.25/2.34 %ClaNum:89(EqnAxiom:41) % 2.25/2.34 %VarNum:283(SingletonVarNum:87) % 2.25/2.34 %MaxLitNum:6 % 2.25/2.34 %MaxfuncDepth:1 % 2.25/2.34 %SharedTerms:14 % 2.25/2.34 %goalClause: 52 % 2.25/2.34 %singleGoalClaCount:1 % 2.25/2.34 [42]P1(a1) % 2.25/2.34 [43]P1(a2) % 2.25/2.34 [44]P2(a11,a1) % 2.25/2.34 [46]P2(a12,a1) % 2.25/2.34 [47]P6(a2,a1) % 2.25/2.34 [48]P7(a11,a2,a1) % 2.25/2.34 [49]P7(a12,a2,a1) % 2.25/2.34 [50]P8(a11,a2,a1) % 2.25/2.34 [51]P8(a12,a2,a1) % 2.25/2.34 [52]~E(a12,a11) % 2.25/2.34 [53]~P3(x531)+P9(x531,x531) % 2.25/2.34 [55]~P2(x551,a2)+P2(x551,a1) % 2.25/2.34 [56]~P2(x561,a2)+P9(x561,a11) % 2.25/2.34 [57]~P2(x571,a2)+P9(x571,a12) % 2.25/2.34 [70]P9(a11,x701)+~P7(x701,a2,a1) % 2.25/2.34 [71]P9(a12,x711)+~P7(x711,a2,a1) % 2.25/2.34 [54]~P1(x541)+P10(x541)+P2(f3(x541),x541) % 2.25/2.34 [61]~P2(x611,a1)+P9(a11,x611)+P2(f4(x611),a2) % 2.25/2.34 [62]~P2(x621,a1)+P9(a12,x621)+P2(f10(x621),a2) % 2.25/2.34 [64]~P2(x641,a1)+~P9(f4(x641),x641)+P9(a11,x641) % 2.25/2.34 [65]~P2(x651,a1)+~P9(f10(x651),x651)+P9(a12,x651) % 2.25/2.34 [58]~P6(x581,x582)+P1(x581)+~P1(x582) % 2.25/2.34 [59]~P2(x591,x592)+P3(x591)+~P1(x592) % 2.25/2.34 [60]~P10(x601)+~P1(x601)+~P2(x602,x601) % 2.25/2.34 [67]~P1(x671)+~P1(x672)+P6(x671,x672)+P2(f5(x672,x671),x671) % 2.25/2.34 [69]~P1(x691)+~P1(x692)+P6(x691,x692)+~P2(f5(x692,x691),x692) % 2.25/2.34 [66]~P1(x662)+~P6(x663,x662)+P2(x661,x662)+~P2(x661,x663) % 2.25/2.34 [72]~P1(x722)+~P4(x721,x723,x722)+P2(x721,x722)+~P6(x723,x722) % 2.25/2.34 [73]~P1(x732)+~P7(x731,x733,x732)+P2(x731,x732)+~P6(x733,x732) % 2.25/2.34 [74]~P1(x742)+~P5(x741,x743,x742)+P2(x741,x742)+~P6(x743,x742) % 2.25/2.34 [75]~P1(x752)+~P8(x751,x753,x752)+P2(x751,x752)+~P6(x753,x752) % 2.25/2.34 [78]~P1(x783)+~P6(x782,x783)+~P5(x781,x782,x783)+P4(x781,x782,x783) % 2.25/2.34 [79]~P1(x793)+~P6(x792,x793)+~P8(x791,x792,x793)+P7(x791,x792,x793) % 2.25/2.34 [63]~P3(x632)+~P3(x631)+~P9(x632,x631)+~P9(x631,x632)+E(x631,x632) % 2.25/2.34 [82]~P1(x823)+~P2(x821,x823)+~P6(x822,x823)+P4(x821,x822,x823)+P2(f6(x823,x822,x821),x822) % 2.25/2.34 [83]~P1(x833)+~P2(x831,x833)+~P6(x832,x833)+P7(x831,x832,x833)+P2(f7(x833,x832,x831),x832) % 2.25/2.34 [84]~P1(x843)+~P2(x841,x843)+~P6(x842,x843)+P4(x841,x842,x843)+~P9(x841,f6(x843,x842,x841)) % 2.25/2.34 [85]~P1(x853)+~P2(x851,x853)+~P6(x852,x853)+P7(x851,x852,x853)+~P9(f7(x853,x852,x851),x851) % 2.25/2.34 [76]~P6(x764,x763)+~P4(x761,x764,x763)+P9(x761,x762)+~P2(x762,x764)+~P1(x763) % 2.25/2.34 [77]~P6(x774,x773)+~P7(x772,x774,x773)+P9(x771,x772)+~P2(x771,x774)+~P1(x773) % 2.25/2.34 [80]~P7(x802,x804,x803)+~P8(x801,x804,x803)+P9(x801,x802)+~P6(x804,x803)+~P1(x803) % 2.25/2.34 [81]~P4(x811,x814,x813)+~P5(x812,x814,x813)+P9(x811,x812)+~P6(x814,x813)+~P1(x813) % 2.25/2.34 [68]~P3(x682)+~P3(x681)+~P9(x683,x682)+~P9(x681,x683)+P9(x681,x682)+~P3(x683) % 2.25/2.34 [86]~P1(x863)+~P2(x861,x863)+~P6(x862,x863)+~P4(x861,x862,x863)+P5(x861,x862,x863)+P4(f8(x863,x862,x861),x862,x863) % 2.25/2.34 [87]~P1(x873)+~P2(x871,x873)+~P6(x872,x873)+~P7(x871,x872,x873)+P8(x871,x872,x873)+P7(f9(x873,x872,x871),x872,x873) % 2.25/2.34 [88]~P1(x883)+~P2(x881,x883)+~P6(x882,x883)+~P7(x881,x882,x883)+P8(x881,x882,x883)+~P9(x881,f9(x883,x882,x881)) % 2.25/2.34 [89]~P1(x893)+~P2(x891,x893)+~P6(x892,x893)+~P4(x891,x892,x893)+P5(x891,x892,x893)+~P9(f8(x893,x892,x891),x891) % 2.25/2.34 %EqnAxiom % 2.25/2.34 [1]E(x11,x11) % 2.25/2.34 [2]E(x22,x21)+~E(x21,x22) % 2.25/2.34 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.25/2.34 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 2.25/2.34 [5]~E(x51,x52)+E(f4(x51),f4(x52)) % 2.25/2.34 [6]~E(x61,x62)+E(f10(x61),f10(x62)) % 2.25/2.34 [7]~E(x71,x72)+E(f8(x71,x73,x74),f8(x72,x73,x74)) % 2.25/2.34 [8]~E(x81,x82)+E(f8(x83,x81,x84),f8(x83,x82,x84)) % 2.25/2.34 [9]~E(x91,x92)+E(f8(x93,x94,x91),f8(x93,x94,x92)) % 2.25/2.34 [10]~E(x101,x102)+E(f9(x101,x103,x104),f9(x102,x103,x104)) % 2.25/2.34 [11]~E(x111,x112)+E(f9(x113,x111,x114),f9(x113,x112,x114)) % 2.25/2.34 [12]~E(x121,x122)+E(f9(x123,x124,x121),f9(x123,x124,x122)) % 2.25/2.34 [13]~E(x131,x132)+E(f5(x131,x133),f5(x132,x133)) % 2.25/2.34 [14]~E(x141,x142)+E(f5(x143,x141),f5(x143,x142)) % 2.25/2.34 [15]~E(x151,x152)+E(f7(x151,x153,x154),f7(x152,x153,x154)) % 2.25/2.34 [16]~E(x161,x162)+E(f7(x163,x161,x164),f7(x163,x162,x164)) % 2.25/2.34 [17]~E(x171,x172)+E(f7(x173,x174,x171),f7(x173,x174,x172)) % 2.25/2.34 [18]~E(x181,x182)+E(f6(x181,x183,x184),f6(x182,x183,x184)) % 2.25/2.34 [19]~E(x191,x192)+E(f6(x193,x191,x194),f6(x193,x192,x194)) % 2.25/2.34 [20]~E(x201,x202)+E(f6(x203,x204,x201),f6(x203,x204,x202)) % 2.25/2.34 [21]~P1(x211)+P1(x212)+~E(x211,x212) % 2.25/2.34 [22]P9(x222,x223)+~E(x221,x222)+~P9(x221,x223) % 2.25/2.34 [23]P9(x233,x232)+~E(x231,x232)+~P9(x233,x231) % 2.25/2.34 [24]P2(x242,x243)+~E(x241,x242)+~P2(x241,x243) % 2.25/2.34 [25]P2(x253,x252)+~E(x251,x252)+~P2(x253,x251) % 2.25/2.34 [26]P5(x262,x263,x264)+~E(x261,x262)+~P5(x261,x263,x264) % 2.25/2.34 [27]P5(x273,x272,x274)+~E(x271,x272)+~P5(x273,x271,x274) % 2.25/2.34 [28]P5(x283,x284,x282)+~E(x281,x282)+~P5(x283,x284,x281) % 2.25/2.34 [29]P6(x292,x293)+~E(x291,x292)+~P6(x291,x293) % 2.25/2.34 [30]P6(x303,x302)+~E(x301,x302)+~P6(x303,x301) % 2.25/2.34 [31]P4(x312,x313,x314)+~E(x311,x312)+~P4(x311,x313,x314) % 2.25/2.34 [32]P4(x323,x322,x324)+~E(x321,x322)+~P4(x323,x321,x324) % 2.25/2.34 [33]P4(x333,x334,x332)+~E(x331,x332)+~P4(x333,x334,x331) % 2.25/2.34 [34]P7(x342,x343,x344)+~E(x341,x342)+~P7(x341,x343,x344) % 2.25/2.34 [35]P7(x353,x352,x354)+~E(x351,x352)+~P7(x353,x351,x354) % 2.25/2.34 [36]P7(x363,x364,x362)+~E(x361,x362)+~P7(x363,x364,x361) % 2.25/2.34 [37]~P3(x371)+P3(x372)+~E(x371,x372) % 2.25/2.34 [38]P8(x382,x383,x384)+~E(x381,x382)+~P8(x381,x383,x384) % 2.25/2.34 [39]P8(x393,x392,x394)+~E(x391,x392)+~P8(x393,x391,x394) % 2.25/2.34 [40]P8(x403,x404,x402)+~E(x401,x402)+~P8(x403,x404,x401) % 2.25/2.34 [41]~P10(x411)+P10(x412)+~E(x411,x412) % 2.25/2.34 % 2.25/2.34 %------------------------------------------- % 2.25/2.34 cnf(92,plain, % 2.25/2.34 (P9(a12,a11)), % 2.25/2.34 inference(scs_inference,[],[48,70,71])). % 2.25/2.34 cnf(108,plain, % 2.25/2.34 (P9(a11,a12)), % 2.25/2.34 inference(scs_inference,[],[49,70])). % 2.25/2.34 cnf(159,plain, % 2.25/2.34 (~P3(a11)+~E(a12,x1591)+~P3(a12)), % 2.25/2.34 inference(scs_inference,[],[52,92,108,49,46,43,22,63])). % 2.25/2.34 cnf(161,plain, % 2.25/2.34 (~P3(a11)+~P3(a12)), % 2.25/2.34 inference(equality_inference,[],[159])). % 2.25/2.34 cnf(720,plain, % 2.25/2.34 (~E(a12,x7201)+P3(x7201)), % 2.25/2.34 inference(scs_inference,[],[46,42,37,59])). % 2.25/2.34 cnf(721,plain, % 2.25/2.34 (P3(a12)), % 2.25/2.34 inference(equality_inference,[],[720])). % 2.25/2.34 cnf(722,plain, % 2.25/2.34 (~P3(a11)), % 2.25/2.34 inference(scs_inference,[],[721,161])). % 2.25/2.34 cnf(735,plain, % 2.25/2.34 ($false), % 2.25/2.34 inference(scs_inference,[],[722,44,42,59]), % 2.25/2.34 ['proof']). % 2.25/2.34 % SZS output end Proof % 2.25/2.34 % Total time :1.750000s %------------------------------------------------------------------------------