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