%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM020+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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:47 EDT 2024 % Result : Theorem 61.13s 61.16s % Output : CNFRefutation 61.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : COM020+1 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/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:10:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.43/0.59 start to proof:theBenchmark % 61.13/61.14 %------------------------------------------- % 61.13/61.14 % File :CSE---1.7 % 61.13/61.14 % Problem :theBenchmark % 61.13/61.14 % Transform :cnf % 61.13/61.14 % Format :tptp:raw % 61.13/61.14 % Command :java -jar mcs_scs.jar %d %s % 61.13/61.14 % 61.13/61.14 % Result :Theorem 60.500000s % 61.13/61.14 % Output :CNFRefutation 60.500000s % 61.13/61.14 %------------------------------------------- % 61.13/61.15 %------------------------------------------------------------------------------ % 61.13/61.15 % File : COM020+1 : TPTP v8.2.0. Released v4.0.0. % 61.13/61.15 % Domain : Computing Theory % 61.13/61.15 % Problem : Newman's lemma on rewriting systems 03_01_05_01, 00 expansion % 61.13/61.15 % Version : Especial. % 61.13/61.15 % English : % 61.13/61.15 % 61.13/61.15 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 61.13/61.15 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 61.13/61.15 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 61.13/61.15 % Source : [Pas08] % 61.13/61.15 % Names : newman_03_01_05_01.00 [Pas08] % 61.13/61.15 % 61.13/61.15 % Status : Theorem % 61.13/61.15 % Rating : 0.25 v8.2.0, 0.28 v8.1.0, 0.25 v7.5.0, 0.31 v7.4.0, 0.23 v7.3.0, 0.21 v7.1.0, 0.13 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.25 v6.2.0, 0.32 v6.1.0, 0.40 v6.0.0, 0.35 v5.5.0, 0.33 v5.4.0, 0.36 v5.3.0, 0.41 v5.2.0, 0.25 v5.1.0, 0.38 v5.0.0, 0.46 v4.1.0, 0.52 v4.0.1, 0.74 v4.0.0 % 61.13/61.15 % Syntax : Number of formulae : 24 ( 2 unt; 6 def) % 61.13/61.15 % Number of atoms : 111 ( 1 equ) % 61.13/61.15 % Maximal formula atoms : 10 ( 4 avg) % 61.13/61.15 % Number of connectives : 88 ( 1 ~; 2 |; 53 &) % 61.13/61.15 % ( 6 <=>; 26 =>; 0 <=; 0 <~>) % 61.13/61.15 % Maximal formula depth : 12 ( 6 avg) % 61.13/61.15 % Maximal term depth : 1 ( 1 avg) % 61.13/61.15 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 61.13/61.15 % Number of functors : 8 ( 8 usr; 8 con; 0-0 aty) % 61.13/61.15 % Number of variables : 50 ( 43 !; 7 ?) % 61.13/61.15 % SPC : FOF_THM_RFO_SEQ % 61.13/61.15 % 61.13/61.15 % Comments : Problem generated by the SAD system [VLP07] % 61.13/61.15 %------------------------------------------------------------------------------ % 61.13/61.15 fof(mElmSort,axiom, % 61.13/61.15 ! [W0] : % 61.13/61.15 ( aElement0(W0) % 61.13/61.15 => $true ) ). % 61.13/61.15 % 61.13/61.15 fof(mRelSort,axiom, % 61.13/61.15 ! [W0] : % 61.13/61.15 ( aRewritingSystem0(W0) % 61.13/61.15 => $true ) ). % 61.13/61.15 % 61.13/61.15 fof(mReduct,axiom, % 61.13/61.15 ! [W0,W1] : % 61.13/61.15 ( ( aElement0(W0) % 61.13/61.15 & aRewritingSystem0(W1) ) % 61.13/61.15 => ! [W2] : % 61.13/61.15 ( aReductOfIn0(W2,W0,W1) % 61.13/61.15 => aElement0(W2) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mWFOrd,axiom, % 61.13/61.15 ! [W0,W1] : % 61.13/61.15 ( ( aElement0(W0) % 61.13/61.15 & aElement0(W1) ) % 61.13/61.15 => ( iLess0(W0,W1) % 61.13/61.15 => $true ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mTCbr,axiom, % 61.13/61.15 ! [W0,W1,W2] : % 61.13/61.15 ( ( aElement0(W0) % 61.13/61.15 & aRewritingSystem0(W1) % 61.13/61.15 & aElement0(W2) ) % 61.13/61.15 => ( sdtmndtplgtdt0(W0,W1,W2) % 61.13/61.15 => $true ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mTCDef,definition, % 61.13/61.15 ! [W0,W1,W2] : % 61.13/61.15 ( ( aElement0(W0) % 61.13/61.15 & aRewritingSystem0(W1) % 61.13/61.15 & aElement0(W2) ) % 61.13/61.15 => ( sdtmndtplgtdt0(W0,W1,W2) % 61.13/61.15 <=> ( aReductOfIn0(W2,W0,W1) % 61.13/61.15 | ? [W3] : % 61.13/61.15 ( aElement0(W3) % 61.13/61.15 & aReductOfIn0(W3,W0,W1) % 61.13/61.15 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mTCTrans,axiom, % 61.13/61.15 ! [W0,W1,W2,W3] : % 61.13/61.15 ( ( aElement0(W0) % 61.13/61.15 & aRewritingSystem0(W1) % 61.13/61.15 & aElement0(W2) % 61.13/61.15 & aElement0(W3) ) % 61.13/61.15 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 61.13/61.15 & sdtmndtplgtdt0(W2,W1,W3) ) % 61.13/61.15 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mTCRDef,definition, % 61.13/61.15 ! [W0,W1,W2] : % 61.13/61.15 ( ( aElement0(W0) % 61.13/61.15 & aRewritingSystem0(W1) % 61.13/61.15 & aElement0(W2) ) % 61.13/61.15 => ( sdtmndtasgtdt0(W0,W1,W2) % 61.13/61.15 <=> ( W0 = W2 % 61.13/61.15 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mTCRTrans,axiom, % 61.13/61.15 ! [W0,W1,W2,W3] : % 61.13/61.15 ( ( aElement0(W0) % 61.13/61.15 & aRewritingSystem0(W1) % 61.13/61.15 & aElement0(W2) % 61.13/61.15 & aElement0(W3) ) % 61.13/61.15 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 61.13/61.15 & sdtmndtasgtdt0(W2,W1,W3) ) % 61.13/61.15 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mCRDef,definition, % 61.13/61.15 ! [W0] : % 61.13/61.15 ( aRewritingSystem0(W0) % 61.13/61.15 => ( isConfluent0(W0) % 61.13/61.15 <=> ! [W1,W2,W3] : % 61.13/61.15 ( ( aElement0(W1) % 61.13/61.15 & aElement0(W2) % 61.13/61.15 & aElement0(W3) % 61.13/61.15 & sdtmndtasgtdt0(W1,W0,W2) % 61.13/61.15 & sdtmndtasgtdt0(W1,W0,W3) ) % 61.13/61.15 => ? [W4] : % 61.13/61.15 ( aElement0(W4) % 61.13/61.15 & sdtmndtasgtdt0(W2,W0,W4) % 61.13/61.15 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mWCRDef,definition, % 61.13/61.15 ! [W0] : % 61.13/61.15 ( aRewritingSystem0(W0) % 61.13/61.15 => ( isLocallyConfluent0(W0) % 61.13/61.15 <=> ! [W1,W2,W3] : % 61.13/61.15 ( ( aElement0(W1) % 61.13/61.15 & aElement0(W2) % 61.13/61.15 & aElement0(W3) % 61.13/61.15 & aReductOfIn0(W2,W1,W0) % 61.13/61.15 & aReductOfIn0(W3,W1,W0) ) % 61.13/61.15 => ? [W4] : % 61.13/61.15 ( aElement0(W4) % 61.13/61.15 & sdtmndtasgtdt0(W2,W0,W4) % 61.13/61.15 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mTermin,definition, % 61.13/61.15 ! [W0] : % 61.13/61.15 ( aRewritingSystem0(W0) % 61.13/61.15 => ( isTerminating0(W0) % 61.13/61.15 <=> ! [W1,W2] : % 61.13/61.15 ( ( aElement0(W1) % 61.13/61.15 & aElement0(W2) ) % 61.13/61.15 => ( sdtmndtplgtdt0(W1,W0,W2) % 61.13/61.15 => iLess0(W2,W1) ) ) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mNFRDef,definition, % 61.13/61.15 ! [W0,W1] : % 61.13/61.15 ( ( aElement0(W0) % 61.13/61.15 & aRewritingSystem0(W1) ) % 61.13/61.15 => ! [W2] : % 61.13/61.15 ( aNormalFormOfIn0(W2,W0,W1) % 61.13/61.15 <=> ( aElement0(W2) % 61.13/61.15 & sdtmndtasgtdt0(W0,W1,W2) % 61.13/61.15 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(mTermNF,axiom, % 61.13/61.15 ! [W0] : % 61.13/61.15 ( ( aRewritingSystem0(W0) % 61.13/61.15 & isTerminating0(W0) ) % 61.13/61.15 => ! [W1] : % 61.13/61.15 ( aElement0(W1) % 61.13/61.15 => ? [W2] : aNormalFormOfIn0(W2,W1,W0) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(m__656,hypothesis, % 61.13/61.15 aRewritingSystem0(xR) ). % 61.13/61.15 % 61.13/61.15 fof(m__656_01,hypothesis, % 61.13/61.15 ( isLocallyConfluent0(xR) % 61.13/61.15 & isTerminating0(xR) ) ). % 61.13/61.15 % 61.13/61.15 fof(m__731,hypothesis, % 61.13/61.15 ( aElement0(xa) % 61.13/61.15 & aElement0(xb) % 61.13/61.15 & aElement0(xc) ) ). % 61.13/61.15 % 61.13/61.15 fof(m__715,hypothesis, % 61.13/61.15 ! [W0,W1,W2] : % 61.13/61.15 ( ( aElement0(W0) % 61.13/61.15 & aElement0(W1) % 61.13/61.15 & aElement0(W2) % 61.13/61.15 & sdtmndtasgtdt0(W0,xR,W1) % 61.13/61.15 & sdtmndtasgtdt0(W0,xR,W2) ) % 61.13/61.15 => ( iLess0(W0,xa) % 61.13/61.15 => ? [W3] : % 61.13/61.15 ( aElement0(W3) % 61.13/61.15 & sdtmndtasgtdt0(W1,xR,W3) % 61.13/61.15 & sdtmndtasgtdt0(W2,xR,W3) ) ) ) ). % 61.13/61.15 % 61.13/61.15 fof(m__731_02,hypothesis, % 61.13/61.15 ( sdtmndtplgtdt0(xa,xR,xb) % 61.13/61.15 & sdtmndtplgtdt0(xa,xR,xc) ) ). % 61.13/61.15 % 61.13/61.15 fof(m__755,hypothesis, % 61.13/61.15 ( aElement0(xu) % 61.13/61.15 & aReductOfIn0(xu,xa,xR) % 61.13/61.15 & sdtmndtasgtdt0(xu,xR,xb) ) ). % 61.13/61.15 % 61.13/61.15 fof(m__779,hypothesis, % 61.13/61.15 ( aElement0(xv) % 61.13/61.15 & aReductOfIn0(xv,xa,xR) % 61.13/61.16 & sdtmndtasgtdt0(xv,xR,xc) ) ). % 61.13/61.16 % 61.13/61.16 fof(m__799,hypothesis, % 61.13/61.16 ( aElement0(xw) % 61.13/61.16 & sdtmndtasgtdt0(xu,xR,xw) % 61.13/61.16 & sdtmndtasgtdt0(xv,xR,xw) ) ). % 61.13/61.16 % 61.13/61.16 fof(m__818,hypothesis, % 61.13/61.16 aNormalFormOfIn0(xd,xw,xR) ). % 61.13/61.16 % 61.13/61.16 fof(m__,conjecture, % 61.13/61.16 ? [W0] : % 61.13/61.16 ( aElement0(W0) % 61.13/61.16 & sdtmndtasgtdt0(xb,xR,W0) % 61.13/61.16 & sdtmndtasgtdt0(xd,xR,W0) ) ). % 61.13/61.16 % 61.13/61.16 %------------------------------------------------------------------------------ % 61.13/61.16 %------------------------------------------- % 61.13/61.16 % Proof found % 61.13/61.16 % SZS status Theorem for theBenchmark % 61.13/61.16 % SZS output start Proof % 61.13/61.16 %ClaNum:110(EqnAxiom:49) % 61.13/61.16 %VarNum:381(SingletonVarNum:106) % 61.13/61.16 %MaxLitNum:8 % 61.13/61.16 %MaxfuncDepth:1 % 61.13/61.16 %SharedTerms:26 % 61.13/61.16 %goalClause: 91 % 61.13/61.16 [50]P1(a1) % 61.13/61.16 [51]P1(a17) % 61.13/61.16 [52]P1(a18) % 61.13/61.16 [53]P1(a19) % 61.13/61.16 [54]P1(a21) % 61.13/61.16 [55]P1(a22) % 61.13/61.16 [56]P2(a2) % 61.13/61.16 [57]P5(a2) % 61.13/61.16 [58]P8(a2) % 61.13/61.16 [59]P3(a19,a1,a2) % 61.13/61.16 [60]P3(a21,a1,a2) % 61.13/61.16 [61]P9(a1,a2,a17) % 61.13/61.16 [62]P9(a1,a2,a18) % 61.13/61.16 [63]P10(a19,a2,a17) % 61.13/61.16 [64]P10(a19,a2,a22) % 61.13/61.16 [65]P10(a21,a2,a18) % 61.13/61.16 [66]P10(a21,a2,a22) % 61.13/61.16 [67]P4(a20,a22,a2) % 61.13/61.16 [91]~P1(x911)+~P10(a17,a2,x911)+~P10(a20,a2,x911) % 61.13/61.16 [68]~P2(x681)+P6(x681)+P1(f3(x681)) % 61.13/61.16 [69]~P2(x691)+P6(x691)+P1(f11(x691)) % 61.13/61.16 [70]~P2(x701)+P6(x701)+P1(f12(x701)) % 61.13/61.16 [71]~P2(x711)+P5(x711)+P1(f13(x711)) % 61.13/61.16 [72]~P2(x721)+P5(x721)+P1(f15(x721)) % 61.13/61.16 [73]~P2(x731)+P5(x731)+P1(f16(x731)) % 61.13/61.16 [74]~P2(x741)+P8(x741)+P1(f4(x741)) % 61.13/61.16 [75]~P2(x751)+P8(x751)+P1(f5(x751)) % 61.13/61.16 [76]~P2(x761)+P8(x761)+~P7(f5(x761),f4(x761)) % 61.13/61.16 [77]~P2(x771)+P6(x771)+P10(f3(x771),x771,f11(x771)) % 61.13/61.16 [78]~P2(x781)+P6(x781)+P10(f3(x781),x781,f12(x781)) % 61.13/61.16 [79]~P2(x791)+P8(x791)+P9(f4(x791),x791,f5(x791)) % 61.13/61.16 [80]~P2(x801)+P5(x801)+P3(f15(x801),f13(x801),x801) % 61.13/61.16 [81]~P2(x811)+P5(x811)+P3(f16(x811),f13(x811),x811) % 61.13/61.16 [83]~P1(x832)+~P2(x831)+~P8(x831)+P4(f6(x831,x832),x832,x831) % 61.13/61.16 [84]~P3(x841,x842,x843)+P1(x841)+~P1(x842)+~P2(x843) % 61.13/61.16 [85]~P4(x851,x852,x853)+P1(x851)+~P1(x852)+~P2(x853) % 61.13/61.16 [87]~P1(x871)+~P2(x872)+~P4(x873,x871,x872)+P10(x871,x872,x873) % 61.13/61.16 [92]~P4(x924,x921,x922)+~P1(x921)+~P3(x923,x924,x922)+~P2(x922) % 61.13/61.16 [93]~P2(x931)+P6(x931)+~P1(x932)+~P10(f11(x931),x931,x932)+~P10(f12(x931),x931,x932) % 61.13/61.16 [94]~P2(x941)+P5(x941)+~P1(x942)+~P10(f15(x941),x941,x942)+~P10(f16(x941),x941,x942) % 61.13/61.16 [82]~E(x821,x823)+~P1(x823)+~P1(x821)+~P2(x822)+P10(x821,x822,x823) % 61.13/61.16 [88]~P1(x881)+~P1(x883)+~P2(x882)+~P3(x883,x881,x882)+P9(x881,x882,x883) % 61.13/61.16 [89]~P1(x893)+~P1(x891)+~P2(x892)+~P9(x891,x892,x893)+P10(x891,x892,x893) % 61.13/61.16 [86]~P1(x861)+~P1(x862)+~P8(x863)+~P9(x862,x863,x861)+P7(x861,x862)+~P2(x863) % 61.13/61.16 [90]~P1(x902)+~P1(x901)+~P2(x903)+~P10(x901,x903,x902)+E(x901,x902)+P9(x901,x903,x902) % 61.13/61.16 [98]~P1(x981)+~P1(x982)+~P2(x983)+~P9(x982,x983,x981)+P3(x981,x982,x983)+P1(f8(x982,x983,x981)) % 61.13/61.16 [100]~P1(x1001)+~P1(x1002)+~P2(x1003)+~P9(x1002,x1003,x1001)+P3(x1001,x1002,x1003)+P3(f8(x1002,x1003,x1001),x1002,x1003) % 61.13/61.16 [101]~P1(x1011)+~P1(x1012)+~P2(x1013)+~P9(x1012,x1013,x1011)+P3(x1011,x1012,x1013)+P9(f8(x1012,x1013,x1011),x1013,x1011) % 61.13/61.16 [102]~P1(x1022)+~P1(x1021)+~P2(x1023)+~P10(x1022,x1023,x1021)+P4(x1021,x1022,x1023)+P3(f7(x1022,x1023,x1021),x1021,x1023) % 61.13/61.16 [99]~P1(x993)+~P1(x992)+~P1(x991)+~P10(x991,a2,x993)+~P10(x991,a2,x992)+~P7(x991,a1)+P1(f9(x991,x992,x993)) % 61.13/61.16 [103]~P1(x1033)+~P1(x1032)+~P1(x1031)+~P10(x1032,a2,x1033)+~P10(x1032,a2,x1031)+~P7(x1032,a1)+P10(x1031,a2,f9(x1032,x1033,x1031)) % 61.13/61.16 [104]~P1(x1043)+~P1(x1042)+~P1(x1041)+~P10(x1042,a2,x1043)+~P10(x1042,a2,x1041)+~P7(x1042,a1)+P10(x1041,a2,f9(x1042,x1041,x1043)) % 61.13/61.16 [95]~P1(x953)+~P1(x951)+~P2(x952)+~P3(x954,x951,x952)+~P9(x954,x952,x953)+P9(x951,x952,x953)+~P1(x954) % 61.13/61.16 [96]~P1(x963)+~P1(x961)+~P2(x962)+~P9(x964,x962,x963)+~P9(x961,x962,x964)+P9(x961,x962,x963)+~P1(x964) % 61.13/61.16 [97]~P1(x973)+~P1(x971)+~P2(x972)+~P10(x974,x972,x973)+~P10(x971,x972,x974)+P10(x971,x972,x973)+~P1(x974) % 61.13/61.16 [105]~P1(x1054)+~P1(x1053)+~P1(x1052)+~P2(x1051)+~P6(x1051)+~P10(x1052,x1051,x1054)+~P10(x1052,x1051,x1053)+P1(f10(x1051,x1052,x1053,x1054)) % 61.13/61.16 [106]~P1(x1064)+~P1(x1063)+~P1(x1062)+~P2(x1061)+~P5(x1061)+~P3(x1064,x1062,x1061)+~P3(x1063,x1062,x1061)+P1(f14(x1061,x1062,x1063,x1064)) % 61.13/61.16 [107]~P1(x1074)+~P1(x1073)+~P1(x1071)+~P2(x1072)+~P6(x1072)+~P10(x1073,x1072,x1074)+~P10(x1073,x1072,x1071)+P10(x1071,x1072,f10(x1072,x1073,x1074,x1071)) % 61.13/61.16 [108]~P1(x1084)+~P1(x1083)+~P1(x1081)+~P2(x1082)+~P6(x1082)+~P10(x1083,x1082,x1084)+~P10(x1083,x1082,x1081)+P10(x1081,x1082,f10(x1082,x1083,x1081,x1084)) % 61.13/61.16 [109]~P1(x1094)+~P1(x1093)+~P1(x1091)+~P2(x1092)+~P5(x1092)+~P3(x1094,x1093,x1092)+~P3(x1091,x1093,x1092)+P10(x1091,x1092,f14(x1092,x1093,x1094,x1091)) % 61.13/61.16 [110]~P1(x1104)+~P1(x1103)+~P1(x1101)+~P2(x1102)+~P5(x1102)+~P3(x1104,x1103,x1102)+~P3(x1101,x1103,x1102)+P10(x1101,x1102,f14(x1102,x1103,x1101,x1104)) % 61.13/61.16 %EqnAxiom % 61.13/61.16 [1]E(x11,x11) % 61.13/61.16 [2]E(x22,x21)+~E(x21,x22) % 61.13/61.16 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 61.13/61.16 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 61.13/61.16 [5]~E(x51,x52)+E(f11(x51),f11(x52)) % 61.13/61.16 [6]~E(x61,x62)+E(f12(x61),f12(x62)) % 61.13/61.16 [7]~E(x71,x72)+E(f13(x71),f13(x72)) % 61.13/61.16 [8]~E(x81,x82)+E(f15(x81),f15(x82)) % 61.13/61.16 [9]~E(x91,x92)+E(f16(x91),f16(x92)) % 61.13/61.16 [10]~E(x101,x102)+E(f4(x101),f4(x102)) % 61.13/61.16 [11]~E(x111,x112)+E(f5(x111),f5(x112)) % 61.13/61.16 [12]~E(x121,x122)+E(f8(x121,x123,x124),f8(x122,x123,x124)) % 61.13/61.16 [13]~E(x131,x132)+E(f8(x133,x131,x134),f8(x133,x132,x134)) % 61.13/61.16 [14]~E(x141,x142)+E(f8(x143,x144,x141),f8(x143,x144,x142)) % 61.13/61.16 [15]~E(x151,x152)+E(f10(x151,x153,x154,x155),f10(x152,x153,x154,x155)) % 61.13/61.16 [16]~E(x161,x162)+E(f10(x163,x161,x164,x165),f10(x163,x162,x164,x165)) % 61.13/61.16 [17]~E(x171,x172)+E(f10(x173,x174,x171,x175),f10(x173,x174,x172,x175)) % 61.13/61.16 [18]~E(x181,x182)+E(f10(x183,x184,x185,x181),f10(x183,x184,x185,x182)) % 61.13/61.16 [19]~E(x191,x192)+E(f14(x191,x193,x194,x195),f14(x192,x193,x194,x195)) % 61.13/61.16 [20]~E(x201,x202)+E(f14(x203,x201,x204,x205),f14(x203,x202,x204,x205)) % 61.13/61.16 [21]~E(x211,x212)+E(f14(x213,x214,x211,x215),f14(x213,x214,x212,x215)) % 61.13/61.16 [22]~E(x221,x222)+E(f14(x223,x224,x225,x221),f14(x223,x224,x225,x222)) % 61.13/61.16 [23]~E(x231,x232)+E(f9(x231,x233,x234),f9(x232,x233,x234)) % 61.13/61.16 [24]~E(x241,x242)+E(f9(x243,x241,x244),f9(x243,x242,x244)) % 61.13/61.16 [25]~E(x251,x252)+E(f9(x253,x254,x251),f9(x253,x254,x252)) % 61.13/61.16 [26]~E(x261,x262)+E(f6(x261,x263),f6(x262,x263)) % 61.13/61.16 [27]~E(x271,x272)+E(f6(x273,x271),f6(x273,x272)) % 61.13/61.16 [28]~E(x281,x282)+E(f7(x281,x283,x284),f7(x282,x283,x284)) % 61.13/61.16 [29]~E(x291,x292)+E(f7(x293,x291,x294),f7(x293,x292,x294)) % 61.13/61.16 [30]~E(x301,x302)+E(f7(x303,x304,x301),f7(x303,x304,x302)) % 61.13/61.16 [31]~P1(x311)+P1(x312)+~E(x311,x312) % 61.13/61.16 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324) % 61.13/61.16 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334) % 61.13/61.16 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341) % 61.13/61.16 [35]P10(x352,x353,x354)+~E(x351,x352)+~P10(x351,x353,x354) % 61.13/61.16 [36]P10(x363,x362,x364)+~E(x361,x362)+~P10(x363,x361,x364) % 61.13/61.16 [37]P10(x373,x374,x372)+~E(x371,x372)+~P10(x373,x374,x371) % 61.13/61.16 [38]~P5(x381)+P5(x382)+~E(x381,x382) % 61.13/61.16 [39]~P2(x391)+P2(x392)+~E(x391,x392) % 61.13/61.16 [40]P9(x402,x403,x404)+~E(x401,x402)+~P9(x401,x403,x404) % 61.13/61.16 [41]P9(x413,x412,x414)+~E(x411,x412)+~P9(x413,x411,x414) % 61.13/61.16 [42]P9(x423,x424,x422)+~E(x421,x422)+~P9(x423,x424,x421) % 61.13/61.16 [43]~P6(x431)+P6(x432)+~E(x431,x432) % 61.13/61.16 [44]P7(x442,x443)+~E(x441,x442)+~P7(x441,x443) % 61.13/61.16 [45]P7(x453,x452)+~E(x451,x452)+~P7(x453,x451) % 61.13/61.16 [46]~P8(x461)+P8(x462)+~E(x461,x462) % 61.13/61.16 [47]P4(x472,x473,x474)+~E(x471,x472)+~P4(x471,x473,x474) % 61.13/61.16 [48]P4(x483,x482,x484)+~E(x481,x482)+~P4(x483,x481,x484) % 61.13/61.16 [49]P4(x493,x494,x492)+~E(x491,x492)+~P4(x493,x494,x491) % 61.13/61.16 % 61.13/61.16 %------------------------------------------- % 61.13/61.17 cnf(111,plain, % 61.13/61.17 (~P1(x1111)+~P1(x1111)+P10(x1111,x1112,x1111)+~P2(x1112)), % 61.13/61.17 inference(equality_inference,[],[82])). % 61.13/61.17 cnf(118,plain, % 61.13/61.17 (P9(a1,a2,a19)), % 61.13/61.17 inference(scs_inference,[],[50,51,53,56,59,61,111,92,89,88])). % 61.13/61.17 cnf(151,plain, % 61.13/61.17 (P7(a19,a1)), % 61.13/61.17 inference(scs_inference,[],[50,55,53,56,118,67,58,92,89,86])). % 61.13/61.17 cnf(20782,plain, % 61.13/61.17 (P10(a22,a2,a20)), % 61.13/61.17 inference(scs_inference,[],[55,67,56,87])). % 61.13/61.17 cnf(20858,plain, % 61.13/61.17 (P1(a20)), % 61.13/61.17 inference(scs_inference,[],[55,67,56,85])). % 61.13/61.17 cnf(20992,plain, % 61.13/61.17 (P10(a19,a2,a20)), % 61.13/61.17 inference(scs_inference,[],[20782,53,55,20858,64,56,97])). % 61.13/61.17 cnf(22426,plain, % 61.13/61.17 (P10(a17,a2,f9(a19,a20,a17))), % 61.13/61.17 inference(scs_inference,[],[51,20992,63,151,20858,53,56,84,103])). % 61.13/61.17 cnf(22430,plain, % 61.13/61.17 (P1(f9(a19,a20,a17))), % 61.13/61.17 inference(scs_inference,[],[51,20992,63,151,20858,53,99])). % 61.13/61.17 cnf(22440,plain, % 61.13/61.17 ($false), % 61.13/61.17 inference(scs_inference,[],[51,22430,22426,20992,63,151,20858,53,56,111,104,91]), % 61.13/61.17 ['proof']). % 61.13/61.19 % SZS output end Proof % 61.13/61.19 % Total time :60.500000s %------------------------------------------------------------------------------