%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM016+1 : 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 : n028.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 04:52:45 EDT 2024 % Result : Theorem 58.64s 58.69s % Output : CNFRefutation 58.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : COM016+1 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 00:00:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.48/0.57 start to proof:theBenchmark % 58.64/58.67 %------------------------------------------- % 58.64/58.67 % File :CSE---1.7 % 58.64/58.67 % Problem :theBenchmark % 58.64/58.67 % Transform :cnf % 58.64/58.67 % Format :tptp:raw % 58.64/58.67 % Command :java -jar mcs_scs.jar %d %s % 58.64/58.67 % 58.64/58.67 % Result :Theorem 58.040000s % 58.64/58.67 % Output :CNFRefutation 58.040000s % 58.64/58.67 %------------------------------------------- % 58.64/58.68 %------------------------------------------------------------------------------ % 58.64/58.68 % File : COM016+1 : TPTP v8.2.0. Released v4.0.0. % 58.64/58.68 % Domain : Computing Theory % 58.64/58.68 % Problem : Newman's lemma on rewriting systems 03_01_01, 00 expansion % 58.64/58.68 % Version : Especial. % 58.64/58.68 % English : % 58.64/58.68 % 58.64/58.68 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 58.64/58.68 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 58.64/58.68 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 58.64/58.68 % Source : [Pas08] % 58.64/58.68 % Names : newman_03_01_01.00 [Pas08] % 58.64/58.68 % 58.64/58.68 % Status : Theorem % 58.64/58.68 % Rating : 0.17 v8.2.0, 0.19 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.20 v7.3.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.25 v5.3.0, 0.26 v5.2.0, 0.15 v5.1.0, 0.24 v5.0.0, 0.29 v4.1.0, 0.35 v4.0.1, 0.57 v4.0.0 % 58.64/58.68 % Syntax : Number of formulae : 20 ( 1 unt; 6 def) % 58.64/58.68 % Number of atoms : 101 ( 1 equ) % 58.64/58.68 % Maximal formula atoms : 10 ( 5 avg) % 58.64/58.68 % Number of connectives : 82 ( 1 ~; 2 |; 47 &) % 58.64/58.68 % ( 6 <=>; 26 =>; 0 <=; 0 <~>) % 58.64/58.68 % Maximal formula depth : 12 ( 6 avg) % 58.64/58.68 % Maximal term depth : 1 ( 1 avg) % 58.64/58.68 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 58.64/58.68 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 58.64/58.68 % Number of variables : 50 ( 43 !; 7 ?) % 58.64/58.68 % SPC : FOF_THM_RFO_SEQ % 58.64/58.68 % 58.64/58.68 % Comments : Problem generated by the SAD system [VLP07] % 58.64/58.68 %------------------------------------------------------------------------------ % 58.64/58.68 fof(mElmSort,axiom, % 58.64/58.68 ! [W0] : % 58.64/58.68 ( aElement0(W0) % 58.64/58.68 => $true ) ). % 58.64/58.68 % 58.64/58.68 fof(mRelSort,axiom, % 58.64/58.68 ! [W0] : % 58.64/58.68 ( aRewritingSystem0(W0) % 58.64/58.68 => $true ) ). % 58.64/58.68 % 58.64/58.68 fof(mReduct,axiom, % 58.64/58.68 ! [W0,W1] : % 58.64/58.68 ( ( aElement0(W0) % 58.64/58.68 & aRewritingSystem0(W1) ) % 58.64/58.68 => ! [W2] : % 58.64/58.68 ( aReductOfIn0(W2,W0,W1) % 58.64/58.68 => aElement0(W2) ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mWFOrd,axiom, % 58.64/58.68 ! [W0,W1] : % 58.64/58.68 ( ( aElement0(W0) % 58.64/58.68 & aElement0(W1) ) % 58.64/58.68 => ( iLess0(W0,W1) % 58.64/58.68 => $true ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mTCbr,axiom, % 58.64/58.68 ! [W0,W1,W2] : % 58.64/58.68 ( ( aElement0(W0) % 58.64/58.68 & aRewritingSystem0(W1) % 58.64/58.68 & aElement0(W2) ) % 58.64/58.68 => ( sdtmndtplgtdt0(W0,W1,W2) % 58.64/58.68 => $true ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mTCDef,definition, % 58.64/58.68 ! [W0,W1,W2] : % 58.64/58.68 ( ( aElement0(W0) % 58.64/58.68 & aRewritingSystem0(W1) % 58.64/58.68 & aElement0(W2) ) % 58.64/58.68 => ( sdtmndtplgtdt0(W0,W1,W2) % 58.64/58.68 <=> ( aReductOfIn0(W2,W0,W1) % 58.64/58.68 | ? [W3] : % 58.64/58.68 ( aElement0(W3) % 58.64/58.68 & aReductOfIn0(W3,W0,W1) % 58.64/58.68 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mTCTrans,axiom, % 58.64/58.68 ! [W0,W1,W2,W3] : % 58.64/58.68 ( ( aElement0(W0) % 58.64/58.68 & aRewritingSystem0(W1) % 58.64/58.68 & aElement0(W2) % 58.64/58.68 & aElement0(W3) ) % 58.64/58.68 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 58.64/58.68 & sdtmndtplgtdt0(W2,W1,W3) ) % 58.64/58.68 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mTCRDef,definition, % 58.64/58.68 ! [W0,W1,W2] : % 58.64/58.68 ( ( aElement0(W0) % 58.64/58.68 & aRewritingSystem0(W1) % 58.64/58.68 & aElement0(W2) ) % 58.64/58.68 => ( sdtmndtasgtdt0(W0,W1,W2) % 58.64/58.68 <=> ( W0 = W2 % 58.64/58.68 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mTCRTrans,axiom, % 58.64/58.68 ! [W0,W1,W2,W3] : % 58.64/58.68 ( ( aElement0(W0) % 58.64/58.68 & aRewritingSystem0(W1) % 58.64/58.68 & aElement0(W2) % 58.64/58.68 & aElement0(W3) ) % 58.64/58.68 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 58.64/58.68 & sdtmndtasgtdt0(W2,W1,W3) ) % 58.64/58.68 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mCRDef,definition, % 58.64/58.68 ! [W0] : % 58.64/58.68 ( aRewritingSystem0(W0) % 58.64/58.68 => ( isConfluent0(W0) % 58.64/58.68 <=> ! [W1,W2,W3] : % 58.64/58.68 ( ( aElement0(W1) % 58.64/58.68 & aElement0(W2) % 58.64/58.68 & aElement0(W3) % 58.64/58.68 & sdtmndtasgtdt0(W1,W0,W2) % 58.64/58.68 & sdtmndtasgtdt0(W1,W0,W3) ) % 58.64/58.68 => ? [W4] : % 58.64/58.68 ( aElement0(W4) % 58.64/58.68 & sdtmndtasgtdt0(W2,W0,W4) % 58.64/58.68 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mWCRDef,definition, % 58.64/58.68 ! [W0] : % 58.64/58.68 ( aRewritingSystem0(W0) % 58.64/58.68 => ( isLocallyConfluent0(W0) % 58.64/58.68 <=> ! [W1,W2,W3] : % 58.64/58.68 ( ( aElement0(W1) % 58.64/58.68 & aElement0(W2) % 58.64/58.68 & aElement0(W3) % 58.64/58.68 & aReductOfIn0(W2,W1,W0) % 58.64/58.68 & aReductOfIn0(W3,W1,W0) ) % 58.64/58.68 => ? [W4] : % 58.64/58.68 ( aElement0(W4) % 58.64/58.68 & sdtmndtasgtdt0(W2,W0,W4) % 58.64/58.68 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mTermin,definition, % 58.64/58.68 ! [W0] : % 58.64/58.68 ( aRewritingSystem0(W0) % 58.64/58.68 => ( isTerminating0(W0) % 58.64/58.68 <=> ! [W1,W2] : % 58.64/58.68 ( ( aElement0(W1) % 58.64/58.68 & aElement0(W2) ) % 58.64/58.68 => ( sdtmndtplgtdt0(W1,W0,W2) % 58.64/58.68 => iLess0(W2,W1) ) ) ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mNFRDef,definition, % 58.64/58.68 ! [W0,W1] : % 58.64/58.68 ( ( aElement0(W0) % 58.64/58.68 & aRewritingSystem0(W1) ) % 58.64/58.68 => ! [W2] : % 58.64/58.68 ( aNormalFormOfIn0(W2,W0,W1) % 58.64/58.68 <=> ( aElement0(W2) % 58.64/58.68 & sdtmndtasgtdt0(W0,W1,W2) % 58.64/58.68 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 58.64/58.68 % 58.64/58.68 fof(mTermNF,axiom, % 58.64/58.68 ! [W0] : % 58.64/58.68 ( ( aRewritingSystem0(W0) % 58.64/58.68 & isTerminating0(W0) ) % 58.64/58.68 => ! [W1] : % 58.64/58.68 ( aElement0(W1) % 58.64/58.68 => ? [W2] : aNormalFormOfIn0(W2,W1,W0) ) ) ). % 58.64/58.68 % 58.64/58.68 fof(m__656,hypothesis, % 58.64/58.68 aRewritingSystem0(xR) ). % 58.64/58.68 % 58.64/58.68 fof(m__656_01,hypothesis, % 58.64/58.69 ( isLocallyConfluent0(xR) % 58.64/58.69 & isTerminating0(xR) ) ). % 58.64/58.69 % 58.64/58.69 fof(m__731,hypothesis, % 58.64/58.69 ( aElement0(xa) % 58.64/58.69 & aElement0(xb) % 58.64/58.69 & aElement0(xc) ) ). % 58.64/58.69 % 58.64/58.69 fof(m__715,hypothesis, % 58.64/58.69 ! [W0,W1,W2] : % 58.64/58.69 ( ( aElement0(W0) % 58.64/58.69 & aElement0(W1) % 58.64/58.69 & aElement0(W2) % 58.64/58.69 & sdtmndtasgtdt0(W0,xR,W1) % 58.64/58.69 & sdtmndtasgtdt0(W0,xR,W2) ) % 58.64/58.69 => ( iLess0(W0,xa) % 58.64/58.69 => ? [W3] : % 58.64/58.69 ( aElement0(W3) % 58.64/58.69 & sdtmndtasgtdt0(W1,xR,W3) % 58.64/58.69 & sdtmndtasgtdt0(W2,xR,W3) ) ) ) ). % 58.64/58.69 % 58.64/58.69 fof(m__731_02,hypothesis, % 58.64/58.69 ( sdtmndtplgtdt0(xa,xR,xb) % 58.64/58.69 & sdtmndtplgtdt0(xa,xR,xc) ) ). % 58.64/58.69 % 58.64/58.69 fof(m__,conjecture, % 58.64/58.69 ? [W0] : % 58.64/58.69 ( aElement0(W0) % 58.64/58.69 & aReductOfIn0(W0,xa,xR) % 58.64/58.69 & sdtmndtasgtdt0(W0,xR,xb) ) ). % 58.64/58.69 % 58.64/58.69 %------------------------------------------------------------------------------ % 58.64/58.69 %------------------------------------------- % 58.64/58.69 % Proof found % 58.64/58.69 % SZS status Theorem for theBenchmark % 58.64/58.69 % SZS output start Proof % 58.64/58.69 %ClaNum:100(EqnAxiom:49) % 58.64/58.69 %VarNum:381(SingletonVarNum:106) % 58.64/58.69 %MaxLitNum:8 % 58.64/58.69 %MaxfuncDepth:1 % 58.64/58.69 %SharedTerms:12 % 58.64/58.69 %goalClause: 81 % 58.64/58.69 [50]P1(a1) % 58.64/58.69 [51]P1(a17) % 58.64/58.69 [52]P1(a18) % 58.64/58.69 [53]P2(a2) % 58.64/58.69 [54]P5(a2) % 58.64/58.69 [55]P8(a2) % 58.64/58.69 [56]P9(a1,a2,a17) % 58.64/58.69 [57]P9(a1,a2,a18) % 58.64/58.69 [81]~P1(x811)+~P3(x811,a1,a2)+~P10(x811,a2,a17) % 58.64/58.69 [58]~P2(x581)+P6(x581)+P1(f3(x581)) % 58.64/58.69 [59]~P2(x591)+P6(x591)+P1(f11(x591)) % 58.64/58.69 [60]~P2(x601)+P6(x601)+P1(f12(x601)) % 58.64/58.69 [61]~P2(x611)+P5(x611)+P1(f13(x611)) % 58.64/58.69 [62]~P2(x621)+P5(x621)+P1(f15(x621)) % 58.64/58.69 [63]~P2(x631)+P5(x631)+P1(f16(x631)) % 58.64/58.69 [64]~P2(x641)+P8(x641)+P1(f4(x641)) % 58.64/58.69 [65]~P2(x651)+P8(x651)+P1(f5(x651)) % 58.64/58.69 [66]~P2(x661)+P8(x661)+~P7(f5(x661),f4(x661)) % 58.64/58.69 [67]~P2(x671)+P6(x671)+P10(f3(x671),x671,f11(x671)) % 58.64/58.69 [68]~P2(x681)+P6(x681)+P10(f3(x681),x681,f12(x681)) % 58.64/58.69 [69]~P2(x691)+P8(x691)+P9(f4(x691),x691,f5(x691)) % 58.64/58.69 [70]~P2(x701)+P5(x701)+P3(f15(x701),f13(x701),x701) % 58.64/58.69 [71]~P2(x711)+P5(x711)+P3(f16(x711),f13(x711),x711) % 58.64/58.69 [73]~P1(x732)+~P2(x731)+~P8(x731)+P4(f6(x731,x732),x732,x731) % 58.64/58.69 [74]~P3(x741,x742,x743)+P1(x741)+~P1(x742)+~P2(x743) % 58.64/58.69 [75]~P4(x751,x752,x753)+P1(x751)+~P1(x752)+~P2(x753) % 58.64/58.69 [77]~P1(x771)+~P2(x772)+~P4(x773,x771,x772)+P10(x771,x772,x773) % 58.64/58.69 [82]~P4(x824,x821,x822)+~P1(x821)+~P3(x823,x824,x822)+~P2(x822) % 58.64/58.69 [83]~P2(x831)+P6(x831)+~P1(x832)+~P10(f11(x831),x831,x832)+~P10(f12(x831),x831,x832) % 58.64/58.69 [84]~P2(x841)+P5(x841)+~P1(x842)+~P10(f15(x841),x841,x842)+~P10(f16(x841),x841,x842) % 58.64/58.69 [72]~E(x721,x723)+~P1(x723)+~P1(x721)+~P2(x722)+P10(x721,x722,x723) % 58.64/58.69 [78]~P1(x781)+~P1(x783)+~P2(x782)+~P3(x783,x781,x782)+P9(x781,x782,x783) % 58.64/58.69 [79]~P1(x793)+~P1(x791)+~P2(x792)+~P9(x791,x792,x793)+P10(x791,x792,x793) % 58.64/58.69 [76]~P1(x761)+~P1(x762)+~P8(x763)+~P9(x762,x763,x761)+P7(x761,x762)+~P2(x763) % 58.64/58.69 [80]~P1(x802)+~P1(x801)+~P2(x803)+~P10(x801,x803,x802)+E(x801,x802)+P9(x801,x803,x802) % 58.64/58.69 [88]~P1(x881)+~P1(x882)+~P2(x883)+~P9(x882,x883,x881)+P3(x881,x882,x883)+P1(f8(x882,x883,x881)) % 58.64/58.69 [90]~P1(x901)+~P1(x902)+~P2(x903)+~P9(x902,x903,x901)+P3(x901,x902,x903)+P3(f8(x902,x903,x901),x902,x903) % 58.64/58.69 [91]~P1(x911)+~P1(x912)+~P2(x913)+~P9(x912,x913,x911)+P3(x911,x912,x913)+P9(f8(x912,x913,x911),x913,x911) % 58.64/58.69 [92]~P1(x922)+~P1(x921)+~P2(x923)+~P10(x922,x923,x921)+P4(x921,x922,x923)+P3(f7(x922,x923,x921),x921,x923) % 58.64/58.69 [89]~P1(x893)+~P1(x892)+~P1(x891)+~P10(x891,a2,x893)+~P10(x891,a2,x892)+~P7(x891,a1)+P1(f9(x891,x892,x893)) % 58.64/58.69 [93]~P1(x933)+~P1(x932)+~P1(x931)+~P10(x932,a2,x933)+~P10(x932,a2,x931)+~P7(x932,a1)+P10(x931,a2,f9(x932,x933,x931)) % 58.64/58.69 [94]~P1(x943)+~P1(x942)+~P1(x941)+~P10(x942,a2,x943)+~P10(x942,a2,x941)+~P7(x942,a1)+P10(x941,a2,f9(x942,x941,x943)) % 58.64/58.69 [85]~P1(x853)+~P1(x851)+~P2(x852)+~P3(x854,x851,x852)+~P9(x854,x852,x853)+P9(x851,x852,x853)+~P1(x854) % 58.64/58.69 [86]~P1(x863)+~P1(x861)+~P2(x862)+~P9(x864,x862,x863)+~P9(x861,x862,x864)+P9(x861,x862,x863)+~P1(x864) % 58.64/58.69 [87]~P1(x873)+~P1(x871)+~P2(x872)+~P10(x874,x872,x873)+~P10(x871,x872,x874)+P10(x871,x872,x873)+~P1(x874) % 58.64/58.69 [95]~P1(x954)+~P1(x953)+~P1(x952)+~P2(x951)+~P6(x951)+~P10(x952,x951,x954)+~P10(x952,x951,x953)+P1(f10(x951,x952,x953,x954)) % 58.64/58.69 [96]~P1(x964)+~P1(x963)+~P1(x962)+~P2(x961)+~P5(x961)+~P3(x964,x962,x961)+~P3(x963,x962,x961)+P1(f14(x961,x962,x963,x964)) % 58.64/58.69 [97]~P1(x974)+~P1(x973)+~P1(x971)+~P2(x972)+~P6(x972)+~P10(x973,x972,x974)+~P10(x973,x972,x971)+P10(x971,x972,f10(x972,x973,x974,x971)) % 58.64/58.69 [98]~P1(x984)+~P1(x983)+~P1(x981)+~P2(x982)+~P6(x982)+~P10(x983,x982,x984)+~P10(x983,x982,x981)+P10(x981,x982,f10(x982,x983,x981,x984)) % 58.64/58.69 [99]~P1(x994)+~P1(x993)+~P1(x991)+~P2(x992)+~P5(x992)+~P3(x994,x993,x992)+~P3(x991,x993,x992)+P10(x991,x992,f14(x992,x993,x994,x991)) % 58.64/58.69 [100]~P1(x1004)+~P1(x1003)+~P1(x1001)+~P2(x1002)+~P5(x1002)+~P3(x1004,x1003,x1002)+~P3(x1001,x1003,x1002)+P10(x1001,x1002,f14(x1002,x1003,x1001,x1004)) % 58.64/58.69 %EqnAxiom % 58.64/58.69 [1]E(x11,x11) % 58.64/58.69 [2]E(x22,x21)+~E(x21,x22) % 58.64/58.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.64/58.69 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 58.64/58.69 [5]~E(x51,x52)+E(f11(x51),f11(x52)) % 58.64/58.69 [6]~E(x61,x62)+E(f12(x61),f12(x62)) % 58.64/58.69 [7]~E(x71,x72)+E(f13(x71),f13(x72)) % 58.64/58.69 [8]~E(x81,x82)+E(f15(x81),f15(x82)) % 58.64/58.69 [9]~E(x91,x92)+E(f16(x91),f16(x92)) % 58.64/58.69 [10]~E(x101,x102)+E(f4(x101),f4(x102)) % 58.64/58.69 [11]~E(x111,x112)+E(f5(x111),f5(x112)) % 58.64/58.69 [12]~E(x121,x122)+E(f8(x121,x123,x124),f8(x122,x123,x124)) % 58.64/58.69 [13]~E(x131,x132)+E(f8(x133,x131,x134),f8(x133,x132,x134)) % 58.64/58.69 [14]~E(x141,x142)+E(f8(x143,x144,x141),f8(x143,x144,x142)) % 58.64/58.69 [15]~E(x151,x152)+E(f10(x151,x153,x154,x155),f10(x152,x153,x154,x155)) % 58.64/58.69 [16]~E(x161,x162)+E(f10(x163,x161,x164,x165),f10(x163,x162,x164,x165)) % 58.64/58.69 [17]~E(x171,x172)+E(f10(x173,x174,x171,x175),f10(x173,x174,x172,x175)) % 58.64/58.69 [18]~E(x181,x182)+E(f10(x183,x184,x185,x181),f10(x183,x184,x185,x182)) % 58.64/58.69 [19]~E(x191,x192)+E(f14(x191,x193,x194,x195),f14(x192,x193,x194,x195)) % 58.64/58.69 [20]~E(x201,x202)+E(f14(x203,x201,x204,x205),f14(x203,x202,x204,x205)) % 58.64/58.69 [21]~E(x211,x212)+E(f14(x213,x214,x211,x215),f14(x213,x214,x212,x215)) % 58.64/58.69 [22]~E(x221,x222)+E(f14(x223,x224,x225,x221),f14(x223,x224,x225,x222)) % 58.64/58.69 [23]~E(x231,x232)+E(f9(x231,x233,x234),f9(x232,x233,x234)) % 58.64/58.69 [24]~E(x241,x242)+E(f9(x243,x241,x244),f9(x243,x242,x244)) % 58.64/58.69 [25]~E(x251,x252)+E(f9(x253,x254,x251),f9(x253,x254,x252)) % 58.64/58.69 [26]~E(x261,x262)+E(f6(x261,x263),f6(x262,x263)) % 58.64/58.69 [27]~E(x271,x272)+E(f6(x273,x271),f6(x273,x272)) % 58.64/58.69 [28]~E(x281,x282)+E(f7(x281,x283,x284),f7(x282,x283,x284)) % 58.64/58.69 [29]~E(x291,x292)+E(f7(x293,x291,x294),f7(x293,x292,x294)) % 58.64/58.69 [30]~E(x301,x302)+E(f7(x303,x304,x301),f7(x303,x304,x302)) % 58.64/58.69 [31]~P1(x311)+P1(x312)+~E(x311,x312) % 58.64/58.69 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324) % 58.64/58.69 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334) % 58.64/58.69 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341) % 58.64/58.69 [35]P10(x352,x353,x354)+~E(x351,x352)+~P10(x351,x353,x354) % 58.64/58.69 [36]P10(x363,x362,x364)+~E(x361,x362)+~P10(x363,x361,x364) % 58.64/58.69 [37]P10(x373,x374,x372)+~E(x371,x372)+~P10(x373,x374,x371) % 58.64/58.69 [38]~P2(x381)+P2(x382)+~E(x381,x382) % 58.64/58.69 [39]~P5(x391)+P5(x392)+~E(x391,x392) % 58.64/58.69 [40]~P8(x401)+P8(x402)+~E(x401,x402) % 58.64/58.69 [41]P9(x412,x413,x414)+~E(x411,x412)+~P9(x411,x413,x414) % 58.64/58.69 [42]P9(x423,x422,x424)+~E(x421,x422)+~P9(x423,x421,x424) % 58.64/58.69 [43]P9(x433,x434,x432)+~E(x431,x432)+~P9(x433,x434,x431) % 58.64/58.69 [44]P7(x442,x443)+~E(x441,x442)+~P7(x441,x443) % 58.64/58.69 [45]P7(x453,x452)+~E(x451,x452)+~P7(x453,x451) % 58.64/58.69 [46]~P6(x461)+P6(x462)+~E(x461,x462) % 58.64/58.69 [47]P4(x472,x473,x474)+~E(x471,x472)+~P4(x471,x473,x474) % 58.64/58.69 [48]P4(x483,x482,x484)+~E(x481,x482)+~P4(x483,x481,x484) % 58.64/58.69 [49]P4(x493,x494,x492)+~E(x491,x492)+~P4(x493,x494,x491) % 58.64/58.69 % 58.64/58.69 %------------------------------------------- % 58.64/58.70 cnf(101,plain, % 58.64/58.70 (~P1(x1011)+~P1(x1011)+P10(x1011,x1012,x1011)+~P2(x1012)), % 58.64/58.70 inference(equality_inference,[],[72])). % 58.64/58.70 cnf(104,plain, % 58.64/58.70 (P10(a1,a2,a17)), % 58.64/58.70 inference(scs_inference,[],[50,51,53,56,101,79])). % 58.64/58.70 cnf(106,plain, % 58.64/58.70 (P7(a17,a1)), % 58.64/58.70 inference(scs_inference,[],[50,51,53,55,56,101,79,76])). % 58.64/58.70 cnf(122,plain, % 58.64/58.70 (P7(a18,a1)), % 58.64/58.70 inference(scs_inference,[],[50,52,57,55,53,79,76])). % 58.64/58.70 cnf(125,plain, % 58.64/58.70 (P7(a17,x1251)+~E(a1,x1251)), % 58.64/58.70 inference(scs_inference,[],[50,52,57,106,55,53,79,76,44,45])). % 58.64/58.70 cnf(136,plain, % 58.64/58.70 (P7(a18,x1361)+~E(a1,x1361)), % 58.64/58.70 inference(scs_inference,[],[122,45])). % 58.64/58.70 cnf(152,plain, % 58.64/58.70 (~P4(x1521,a1,a2)+~P3(x1522,x1521,a2)), % 58.64/58.70 inference(scs_inference,[],[50,53,82])). % 58.64/58.70 cnf(155,plain, % 58.64/58.70 (~P4(x1551,a17,a2)+~P3(x1552,x1551,a2)), % 58.64/58.70 inference(scs_inference,[],[51,53,82])). % 58.64/58.70 cnf(158,plain, % 58.64/58.70 (~P4(x1581,a18,a2)+~P3(x1582,x1581,a2)), % 58.64/58.70 inference(scs_inference,[],[52,53,82])). % 58.64/58.70 cnf(161,plain, % 58.64/58.70 (P10(a17,a2,a17)), % 58.64/58.70 inference(scs_inference,[],[51,53,72])). % 58.64/58.70 cnf(172,plain, % 58.64/58.70 (P10(a18,a2,a18)), % 58.64/58.70 inference(scs_inference,[],[52,53,72])). % 58.64/58.70 cnf(275,plain, % 58.64/58.70 (~E(x2751,a1)+P1(x2751)), % 58.64/58.70 inference(scs_inference,[],[50,31,2])). % 58.64/58.70 cnf(337,plain, % 58.64/58.70 (P4(f6(a2,x3371),x3371,a2)+~E(x3371,a1)), % 58.64/58.70 inference(scs_inference,[],[55,53,275,73])). % 58.64/58.70 cnf(338,plain, % 58.64/58.70 (P4(f6(a2,a1),a1,a2)), % 58.64/58.70 inference(equality_inference,[],[337])). % 58.64/58.70 cnf(339,plain, % 58.64/58.70 (~P3(x3391,f6(a2,a1),a2)), % 58.64/58.70 inference(scs_inference,[],[338,152])). % 58.64/58.70 cnf(1069,plain, % 58.64/58.70 (P1(f6(a2,a1))), % 58.64/58.70 inference(scs_inference,[],[53,338,275,75])). % 58.64/58.70 cnf(1071,plain, % 58.64/58.70 (~P4(x10711,f6(a2,a1),a2)+~P3(x10712,x10711,a2)), % 58.64/58.70 inference(scs_inference,[],[1069,53,82])). % 58.64/58.70 cnf(1080,plain, % 58.64/58.70 (P4(f6(a2,a1),f6(a2,a1),a2)), % 58.64/58.70 inference(scs_inference,[],[1069,53,339,72,92])). % 58.64/58.70 cnf(1137,plain, % 58.64/58.70 (~P3(x11371,f6(a2,a1),a2)), % 58.64/58.70 inference(rename_variables,[],[339])). % 58.64/58.70 cnf(1139,plain, % 58.64/58.70 (~P9(f6(a2,a1),a2,a17)), % 58.64/58.70 inference(scs_inference,[],[51,1080,1069,338,339,1137,53,90,1071,152,33])). % 58.64/58.70 cnf(1384,plain, % 58.64/58.70 (P1(f9(a17,a17,a17))), % 58.64/58.70 inference(scs_inference,[],[161,51,125,89])). % 58.64/58.70 cnf(1386,plain, % 58.64/58.70 (~P4(x13861,f9(a17,a17,a17),a2)+~P3(x13862,x13861,a2)), % 58.64/58.70 inference(scs_inference,[],[1384,53,82])). % 58.64/58.70 cnf(1488,plain, % 58.64/58.70 (P1(f9(a18,a18,a18))), % 58.64/58.70 inference(scs_inference,[],[172,52,136,89])). % 58.64/58.70 cnf(1490,plain, % 58.64/58.70 (~P4(x14901,f9(a18,a18,a18),a2)+~P3(x14902,x14901,a2)), % 58.64/58.70 inference(scs_inference,[],[1488,53,82])). % 58.64/58.70 cnf(4495,plain, % 58.64/58.70 (~P3(a17,a1,a2)), % 58.64/58.70 inference(scs_inference,[],[51,161,81])). % 58.64/58.70 cnf(4530,plain, % 58.64/58.70 (P1(x45301)+~P4(x45301,a17,a2)), % 58.64/58.70 inference(scs_inference,[],[51,53,75])). % 58.64/58.70 cnf(7702,plain, % 58.64/58.70 (P1(f6(a2,a17))), % 58.64/58.70 inference(scs_inference,[],[51,55,53,4530,73])). % 58.64/58.70 cnf(7708,plain, % 58.64/58.70 (~P4(x77081,f6(a2,a17),a2)+~P3(x77082,x77081,a2)), % 58.64/58.70 inference(scs_inference,[],[7702,53,101,36,75,82])). % 58.64/58.70 cnf(7761,plain, % 58.64/58.70 (P4(f6(a2,a17),a17,a2)), % 58.64/58.70 inference(scs_inference,[],[51,338,55,53,50,77,73])). % 58.64/58.70 cnf(7763,plain, % 58.64/58.70 (P1(f8(a1,a2,a17))), % 58.64/58.70 inference(scs_inference,[],[51,4495,56,338,55,53,50,77,73,88])). % 58.64/58.70 cnf(7765,plain, % 58.64/58.70 (P9(f8(a1,a2,a17),a2,a17)), % 58.64/58.70 inference(scs_inference,[],[51,4495,56,338,55,53,50,77,73,88,91])). % 58.64/58.70 cnf(7767,plain, % 58.64/58.70 (P3(f8(a1,a2,a17),a1,a2)), % 58.64/58.70 inference(scs_inference,[],[51,4495,56,338,55,53,50,77,73,88,91,90])). % 58.64/58.70 cnf(7769,plain, % 58.64/58.70 (~P4(a1,a17,a2)), % 58.64/58.70 inference(scs_inference,[],[51,4495,56,338,55,53,50,77,73,88,91,90,155])). % 58.64/58.70 cnf(7783,plain, % 58.64/58.70 (~P10(f8(a1,a2,a17),a2,a17)), % 58.64/58.70 inference(scs_inference,[],[51,4495,56,338,55,53,50,77,73,88,91,90,155,158,7708,1386,1490,152,59,81])). % 58.64/58.70 cnf(7814,plain, % 58.64/58.70 ($false), % 58.64/58.70 inference(scs_inference,[],[51,7769,7763,7765,7783,7761,7767,1139,104,53,50,47,35,41,101,82,78,79]), % 58.64/58.70 ['proof']). % 58.72/58.70 % SZS output end Proof % 58.72/58.70 % Total time :58.040000s %------------------------------------------------------------------------------