%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM013+4 : 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 : n017.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 116.31s 116.34s % Output : CNFRefutation 116.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : COM013+4 : 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 : n017.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 : Thu Jun 20 23:21:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 116.28/116.32 %------------------------------------------- % 116.28/116.32 % File :CSE---1.7 % 116.28/116.32 % Problem :theBenchmark % 116.28/116.32 % Transform :cnf % 116.28/116.32 % Format :tptp:raw % 116.28/116.32 % Command :java -jar mcs_scs.jar %d %s % 116.28/116.32 % 116.28/116.32 % Result :Theorem 115.690000s % 116.28/116.32 % Output :CNFRefutation 115.690000s % 116.28/116.32 %------------------------------------------- % 116.31/116.33 %------------------------------------------------------------------------------ % 116.31/116.33 % File : COM013+4 : TPTP v8.2.0. Released v4.0.0. % 116.31/116.33 % Domain : Computing Theory % 116.31/116.33 % Problem : Newman's lemma on rewriting systems 02, 03 expansion % 116.31/116.33 % Version : Especial. % 116.31/116.33 % English : % 116.31/116.33 % 116.31/116.33 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 116.31/116.33 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 116.31/116.33 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 116.31/116.33 % Source : [Pas08] % 116.31/116.33 % Names : newman_02.03 [Pas08] % 116.31/116.33 % 116.31/116.33 % Status : Theorem % 116.31/116.33 % Rating : 0.08 v8.2.0, 0.06 v8.1.0, 0.00 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.17 v6.0.0, 0.22 v5.5.0, 0.11 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.00 v5.1.0, 0.10 v5.0.0, 0.21 v4.1.0, 0.30 v4.0.1, 0.65 v4.0.0 % 116.31/116.33 % Syntax : Number of formulae : 15 ( 0 unt; 6 def) % 116.31/116.33 % Number of atoms : 110 ( 3 equ) % 116.31/116.33 % Maximal formula atoms : 23 ( 7 avg) % 116.31/116.33 % Number of connectives : 98 ( 3 ~; 11 |; 50 &) % 116.31/116.33 % ( 6 <=>; 28 =>; 0 <=; 0 <~>) % 116.31/116.33 % Maximal formula depth : 16 ( 9 avg) % 116.31/116.33 % Maximal term depth : 1 ( 1 avg) % 116.31/116.33 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 116.31/116.33 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 116.31/116.33 % Number of variables : 53 ( 42 !; 11 ?) % 116.31/116.33 % SPC : FOF_THM_RFO_SEQ % 116.31/116.33 % 116.31/116.33 % Comments : Problem generated by the SAD system [VLP07] % 116.31/116.33 %------------------------------------------------------------------------------ % 116.31/116.33 fof(mElmSort,axiom, % 116.31/116.33 ! [W0] : % 116.31/116.33 ( aElement0(W0) % 116.31/116.33 => $true ) ). % 116.31/116.33 % 116.31/116.33 fof(mRelSort,axiom, % 116.31/116.33 ! [W0] : % 116.31/116.33 ( aRewritingSystem0(W0) % 116.31/116.33 => $true ) ). % 116.31/116.33 % 116.31/116.33 fof(mReduct,axiom, % 116.31/116.33 ! [W0,W1] : % 116.31/116.33 ( ( aElement0(W0) % 116.31/116.33 & aRewritingSystem0(W1) ) % 116.31/116.33 => ! [W2] : % 116.31/116.33 ( aReductOfIn0(W2,W0,W1) % 116.31/116.33 => aElement0(W2) ) ) ). % 116.31/116.33 % 116.31/116.33 fof(mWFOrd,axiom, % 116.31/116.33 ! [W0,W1] : % 116.31/116.33 ( ( aElement0(W0) % 116.31/116.33 & aElement0(W1) ) % 116.31/116.33 => ( iLess0(W0,W1) % 116.31/116.33 => $true ) ) ). % 116.31/116.33 % 116.31/116.33 fof(mTCbr,axiom, % 116.31/116.33 ! [W0,W1,W2] : % 116.31/116.33 ( ( aElement0(W0) % 116.31/116.33 & aRewritingSystem0(W1) % 116.31/116.33 & aElement0(W2) ) % 116.31/116.33 => ( sdtmndtplgtdt0(W0,W1,W2) % 116.31/116.33 => $true ) ) ). % 116.31/116.33 % 116.31/116.33 fof(mTCDef,definition, % 116.31/116.33 ! [W0,W1,W2] : % 116.31/116.33 ( ( aElement0(W0) % 116.31/116.33 & aRewritingSystem0(W1) % 116.31/116.33 & aElement0(W2) ) % 116.31/116.33 => ( sdtmndtplgtdt0(W0,W1,W2) % 116.31/116.33 <=> ( aReductOfIn0(W2,W0,W1) % 116.31/116.33 | ? [W3] : % 116.31/116.33 ( aElement0(W3) % 116.31/116.33 & aReductOfIn0(W3,W0,W1) % 116.31/116.33 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 116.31/116.33 % 116.31/116.33 fof(mTCTrans,axiom, % 116.31/116.33 ! [W0,W1,W2,W3] : % 116.31/116.33 ( ( aElement0(W0) % 116.31/116.33 & aRewritingSystem0(W1) % 116.31/116.33 & aElement0(W2) % 116.31/116.33 & aElement0(W3) ) % 116.31/116.33 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 116.31/116.33 & sdtmndtplgtdt0(W2,W1,W3) ) % 116.31/116.33 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 116.31/116.33 % 116.31/116.33 fof(mTCRDef,definition, % 116.31/116.33 ! [W0,W1,W2] : % 116.31/116.33 ( ( aElement0(W0) % 116.31/116.33 & aRewritingSystem0(W1) % 116.31/116.33 & aElement0(W2) ) % 116.31/116.33 => ( sdtmndtasgtdt0(W0,W1,W2) % 116.31/116.33 <=> ( W0 = W2 % 116.31/116.33 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 116.31/116.33 % 116.31/116.33 fof(mTCRTrans,axiom, % 116.31/116.33 ! [W0,W1,W2,W3] : % 116.31/116.33 ( ( aElement0(W0) % 116.31/116.33 & aRewritingSystem0(W1) % 116.31/116.33 & aElement0(W2) % 116.31/116.33 & aElement0(W3) ) % 116.31/116.33 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 116.31/116.33 & sdtmndtasgtdt0(W2,W1,W3) ) % 116.31/116.33 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 116.31/116.33 % 116.31/116.33 fof(mCRDef,definition, % 116.31/116.33 ! [W0] : % 116.31/116.33 ( aRewritingSystem0(W0) % 116.31/116.33 => ( isConfluent0(W0) % 116.31/116.33 <=> ! [W1,W2,W3] : % 116.31/116.33 ( ( aElement0(W1) % 116.31/116.33 & aElement0(W2) % 116.31/116.33 & aElement0(W3) % 116.31/116.33 & sdtmndtasgtdt0(W1,W0,W2) % 116.31/116.33 & sdtmndtasgtdt0(W1,W0,W3) ) % 116.31/116.33 => ? [W4] : % 116.31/116.33 ( aElement0(W4) % 116.31/116.33 & sdtmndtasgtdt0(W2,W0,W4) % 116.31/116.33 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 116.31/116.33 % 116.31/116.33 fof(mWCRDef,definition, % 116.31/116.33 ! [W0] : % 116.31/116.33 ( aRewritingSystem0(W0) % 116.31/116.33 => ( isLocallyConfluent0(W0) % 116.31/116.33 <=> ! [W1,W2,W3] : % 116.31/116.33 ( ( aElement0(W1) % 116.31/116.33 & aElement0(W2) % 116.31/116.33 & aElement0(W3) % 116.31/116.33 & aReductOfIn0(W2,W1,W0) % 116.31/116.33 & aReductOfIn0(W3,W1,W0) ) % 116.31/116.33 => ? [W4] : % 116.31/116.33 ( aElement0(W4) % 116.31/116.33 & sdtmndtasgtdt0(W2,W0,W4) % 116.31/116.33 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 116.31/116.33 % 116.31/116.33 fof(mTermin,definition, % 116.31/116.33 ! [W0] : % 116.31/116.33 ( aRewritingSystem0(W0) % 116.31/116.33 => ( isTerminating0(W0) % 116.31/116.33 <=> ! [W1,W2] : % 116.31/116.33 ( ( aElement0(W1) % 116.31/116.33 & aElement0(W2) ) % 116.31/116.33 => ( sdtmndtplgtdt0(W1,W0,W2) % 116.31/116.33 => iLess0(W2,W1) ) ) ) ) ). % 116.31/116.33 % 116.31/116.33 fof(mNFRDef,definition, % 116.31/116.33 ! [W0,W1] : % 116.31/116.33 ( ( aElement0(W0) % 116.31/116.33 & aRewritingSystem0(W1) ) % 116.31/116.33 => ! [W2] : % 116.31/116.33 ( aNormalFormOfIn0(W2,W0,W1) % 116.31/116.33 <=> ( aElement0(W2) % 116.31/116.33 & sdtmndtasgtdt0(W0,W1,W2) % 116.31/116.33 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 116.31/116.33 % 116.31/116.33 fof(m__587,hypothesis, % 116.31/116.33 ( aRewritingSystem0(xR) % 116.31/116.33 & ! [W0,W1] : % 116.31/116.33 ( ( aElement0(W0) % 116.31/116.33 & aElement0(W1) ) % 116.31/116.33 => ( ( aReductOfIn0(W1,W0,xR) % 116.31/116.34 | ? [W2] : % 116.31/116.34 ( aElement0(W2) % 116.31/116.34 & aReductOfIn0(W2,W0,xR) % 116.31/116.34 & sdtmndtplgtdt0(W2,xR,W1) ) % 116.31/116.34 | sdtmndtplgtdt0(W0,xR,W1) ) % 116.31/116.34 => iLess0(W1,W0) ) ) % 116.31/116.34 & isTerminating0(xR) ) ). % 116.31/116.34 % 116.31/116.34 fof(m__,conjecture, % 116.31/116.34 ! [W0] : % 116.31/116.34 ( aElement0(W0) % 116.31/116.34 => ( ! [W1] : % 116.31/116.34 ( aElement0(W1) % 116.31/116.34 => ( iLess0(W1,W0) % 116.31/116.34 => ? [W2] : % 116.31/116.34 ( aElement0(W2) % 116.31/116.34 & ( W1 = W2 % 116.31/116.34 | ( ( aReductOfIn0(W2,W1,xR) % 116.31/116.34 | ? [W3] : % 116.31/116.34 ( aElement0(W3) % 116.31/116.34 & aReductOfIn0(W3,W1,xR) % 116.31/116.34 & sdtmndtplgtdt0(W3,xR,W2) ) ) % 116.31/116.34 & sdtmndtplgtdt0(W1,xR,W2) ) ) % 116.31/116.34 & sdtmndtasgtdt0(W1,xR,W2) % 116.31/116.34 & ~ ? [W3] : aReductOfIn0(W3,W2,xR) % 116.31/116.34 & aNormalFormOfIn0(W2,W1,xR) ) ) ) % 116.31/116.34 => ? [W1] : % 116.31/116.34 ( ( aElement0(W1) % 116.31/116.34 & ( W0 = W1 % 116.31/116.34 | aReductOfIn0(W1,W0,xR) % 116.31/116.34 | ? [W2] : % 116.31/116.34 ( aElement0(W2) % 116.31/116.34 & aReductOfIn0(W2,W0,xR) % 116.31/116.34 & sdtmndtplgtdt0(W2,xR,W1) ) % 116.31/116.34 | sdtmndtplgtdt0(W0,xR,W1) % 116.31/116.34 | sdtmndtasgtdt0(W0,xR,W1) ) % 116.31/116.34 & ~ ? [W2] : aReductOfIn0(W2,W1,xR) ) % 116.31/116.34 | aNormalFormOfIn0(W1,W0,xR) ) ) ) ). % 116.31/116.34 % 116.31/116.34 %------------------------------------------------------------------------------ % 116.31/116.34 %------------------------------------------- % 116.31/116.34 % Proof found % 116.31/116.34 % SZS status Theorem for theBenchmark % 116.31/116.34 % SZS output start Proof % 116.31/116.34 %ClaNum:105(EqnAxiom:47) % 116.31/116.34 %VarNum:425(SingletonVarNum:117) % 116.31/116.34 %MaxLitNum:8 % 116.31/116.34 %MaxfuncDepth:1 % 116.31/116.34 %SharedTerms:5 % 116.31/116.34 %goalClause: 48 51 60 62 69 70 71 72 77 79 80 81 82 84 92 % 116.31/116.34 %singleGoalClaCount:2 % 116.31/116.34 [48]P1(a1) % 116.31/116.34 [49]P2(a5) % 116.31/116.34 [50]P5(a5) % 116.31/116.34 [51]~P3(x511,a1,a5) % 116.31/116.34 [52]~P2(x521)+P6(x521)+P1(f6(x521)) % 116.31/116.34 [53]~P2(x531)+P6(x531)+P1(f12(x531)) % 116.31/116.34 [54]~P2(x541)+P6(x541)+P1(f13(x541)) % 116.31/116.34 [55]~P2(x551)+P8(x551)+P1(f14(x551)) % 116.31/116.34 [56]~P2(x561)+P8(x561)+P1(f16(x561)) % 116.31/116.34 [57]~P2(x571)+P8(x571)+P1(f17(x571)) % 116.31/116.34 [58]~P2(x581)+P5(x581)+P1(f2(x581)) % 116.31/116.34 [59]~P2(x591)+P5(x591)+P1(f3(x591)) % 116.31/116.34 [60]~P1(x601)+~P7(x601,a1)+P1(f7(x601)) % 116.31/116.34 [61]~P2(x611)+P5(x611)+~P7(f3(x611),f2(x611)) % 116.31/116.34 [62]~P1(x621)+~E(a1,x621)+P4(f8(x621),x621,a5) % 116.31/116.34 [63]~P2(x631)+P6(x631)+P9(f6(x631),x631,f12(x631)) % 116.31/116.34 [64]~P2(x641)+P6(x641)+P9(f6(x641),x641,f13(x641)) % 116.31/116.34 [65]~P2(x651)+P5(x651)+P10(f2(x651),x651,f3(x651)) % 116.31/116.34 [66]~P2(x661)+P8(x661)+P4(f16(x661),f14(x661),x661) % 116.31/116.34 [67]~P2(x671)+P8(x671)+P4(f17(x671),f14(x671),x671) % 116.31/116.34 [69]~P1(x691)+~P7(x691,a1)+P9(x691,a5,f7(x691)) % 116.31/116.34 [70]~P1(x701)+~P7(x701,a1)+P3(f7(x701),x701,a5) % 116.31/116.34 [79]~P1(x791)+~P4(x791,a1,a5)+P4(f8(x791),x791,a5) % 116.31/116.34 [80]~P1(x801)+~P10(a1,a5,x801)+P4(f8(x801),x801,a5) % 116.31/116.34 [81]~P1(x811)+~P9(a1,a5,x811)+P4(f8(x811),x811,a5) % 116.31/116.34 [77]~P1(x771)+~P7(x771,a1)+~P4(x772,f7(x771),a5) % 116.31/116.34 [71]~P1(x711)+~P7(x711,a1)+E(f7(x711),x711)+P10(x711,a5,f7(x711)) % 116.31/116.34 [75]~P1(x752)+~P1(x751)+P7(x751,x752)+~P4(x751,x752,a5) % 116.31/116.34 [76]~P1(x761)+~P1(x762)+P7(x761,x762)+~P10(x762,a5,x761) % 116.31/116.34 [73]~P4(x731,x732,x733)+P1(x731)+~P1(x732)+~P2(x733) % 116.31/116.34 [74]~P3(x741,x742,x743)+P1(x741)+~P1(x742)+~P2(x743) % 116.31/116.34 [83]~P1(x831)+~P2(x832)+~P3(x833,x831,x832)+P9(x831,x832,x833) % 116.31/116.34 [88]~P3(x884,x881,x882)+~P1(x881)+~P4(x883,x884,x882)+~P2(x882) % 116.31/116.34 [72]~P1(x721)+~P7(x721,a1)+E(f7(x721),x721)+P4(f7(x721),x721,a5)+P1(f9(x721)) % 116.31/116.34 [82]~P1(x821)+~P7(x821,a1)+E(f7(x821),x821)+P4(f9(x821),x821,a5)+P4(f7(x821),x821,a5) % 116.31/116.34 [84]~P1(x841)+~P7(x841,a1)+E(f7(x841),x841)+P4(f7(x841),x841,a5)+P10(f9(x841),a5,f7(x841)) % 116.31/116.34 [90]~P2(x901)+P6(x901)+~P1(x902)+~P9(f12(x901),x901,x902)+~P9(f13(x901),x901,x902) % 116.31/116.34 [91]~P2(x911)+P8(x911)+~P1(x912)+~P9(f16(x911),x911,x912)+~P9(f17(x911),x911,x912) % 116.31/116.34 [92]~P1(x921)+~P1(x922)+~P10(x922,a5,x921)+~P4(x922,a1,a5)+P4(f8(x921),x921,a5) % 116.31/116.34 [68]~E(x681,x683)+~P1(x683)+~P1(x681)+~P2(x682)+P9(x681,x682,x683) % 116.31/116.34 [85]~P1(x851)+~P1(x853)+~P2(x852)+~P4(x853,x851,x852)+P10(x851,x852,x853) % 116.31/116.34 [86]~P1(x863)+~P1(x861)+~P2(x862)+~P10(x861,x862,x863)+P9(x861,x862,x863) % 116.31/116.34 [78]~P1(x781)+~P1(x782)+~P5(x783)+~P10(x782,x783,x781)+P7(x781,x782)+~P2(x783) % 116.31/116.34 [87]~P1(x872)+~P1(x871)+~P2(x873)+~P9(x871,x873,x872)+E(x871,x872)+P10(x871,x873,x872) % 116.31/116.34 [89]~P1(x891)+~P1(x892)+P7(x891,x892)+~P1(x893)+~P4(x893,x892,a5)+~P10(x893,a5,x891) % 116.31/116.34 [96]~P1(x961)+~P1(x962)+~P2(x963)+~P10(x962,x963,x961)+P4(x961,x962,x963)+P1(f10(x962,x963,x961)) % 116.31/116.34 [97]~P1(x971)+~P1(x972)+~P2(x973)+~P10(x972,x973,x971)+P4(x971,x972,x973)+P4(f10(x972,x973,x971),x972,x973) % 116.31/116.34 [98]~P1(x981)+~P1(x982)+~P2(x983)+~P10(x982,x983,x981)+P4(x981,x982,x983)+P10(f10(x982,x983,x981),x983,x981) % 116.31/116.34 [99]~P1(x992)+~P1(x991)+~P2(x993)+~P9(x992,x993,x991)+P3(x991,x992,x993)+P4(f4(x992,x993,x991),x991,x993) % 116.31/116.34 [93]~P1(x933)+~P1(x931)+~P2(x932)+~P4(x934,x931,x932)+~P10(x934,x932,x933)+P10(x931,x932,x933)+~P1(x934) % 116.31/116.34 [94]~P1(x943)+~P1(x941)+~P2(x942)+~P10(x944,x942,x943)+~P10(x941,x942,x944)+P10(x941,x942,x943)+~P1(x944) % 116.31/116.34 [95]~P1(x953)+~P1(x951)+~P2(x952)+~P9(x954,x952,x953)+~P9(x951,x952,x954)+P9(x951,x952,x953)+~P1(x954) % 116.31/116.34 [100]~P1(x1004)+~P1(x1003)+~P1(x1002)+~P2(x1001)+~P6(x1001)+~P9(x1002,x1001,x1004)+~P9(x1002,x1001,x1003)+P1(f11(x1001,x1002,x1003,x1004)) % 116.31/116.34 [101]~P1(x1014)+~P1(x1013)+~P1(x1012)+~P2(x1011)+~P8(x1011)+~P4(x1014,x1012,x1011)+~P4(x1013,x1012,x1011)+P1(f15(x1011,x1012,x1013,x1014)) % 116.31/116.34 [102]~P1(x1024)+~P1(x1023)+~P1(x1021)+~P2(x1022)+~P6(x1022)+~P9(x1023,x1022,x1024)+~P9(x1023,x1022,x1021)+P9(x1021,x1022,f11(x1022,x1023,x1024,x1021)) % 116.31/116.34 [103]~P1(x1034)+~P1(x1033)+~P1(x1031)+~P2(x1032)+~P6(x1032)+~P9(x1033,x1032,x1034)+~P9(x1033,x1032,x1031)+P9(x1031,x1032,f11(x1032,x1033,x1031,x1034)) % 116.31/116.34 [104]~P1(x1044)+~P1(x1043)+~P1(x1041)+~P2(x1042)+~P8(x1042)+~P4(x1044,x1043,x1042)+~P4(x1041,x1043,x1042)+P9(x1041,x1042,f15(x1042,x1043,x1044,x1041)) % 116.31/116.34 [105]~P1(x1054)+~P1(x1053)+~P1(x1051)+~P2(x1052)+~P8(x1052)+~P4(x1054,x1053,x1052)+~P4(x1051,x1053,x1052)+P9(x1051,x1052,f15(x1052,x1053,x1051,x1054)) % 116.31/116.34 %EqnAxiom % 116.31/116.34 [1]E(x11,x11) % 116.31/116.34 [2]E(x22,x21)+~E(x21,x22) % 116.31/116.34 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.31/116.34 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 116.31/116.34 [5]~E(x51,x52)+E(f12(x51),f12(x52)) % 116.31/116.34 [6]~E(x61,x62)+E(f13(x61),f13(x62)) % 116.31/116.34 [7]~E(x71,x72)+E(f14(x71),f14(x72)) % 116.31/116.34 [8]~E(x81,x82)+E(f16(x81),f16(x82)) % 116.31/116.34 [9]~E(x91,x92)+E(f17(x91),f17(x92)) % 116.31/116.34 [10]~E(x101,x102)+E(f2(x101),f2(x102)) % 116.31/116.34 [11]~E(x111,x112)+E(f3(x111),f3(x112)) % 116.31/116.34 [12]~E(x121,x122)+E(f7(x121),f7(x122)) % 116.31/116.34 [13]~E(x131,x132)+E(f11(x131,x133,x134,x135),f11(x132,x133,x134,x135)) % 116.31/116.34 [14]~E(x141,x142)+E(f11(x143,x141,x144,x145),f11(x143,x142,x144,x145)) % 116.31/116.34 [15]~E(x151,x152)+E(f11(x153,x154,x151,x155),f11(x153,x154,x152,x155)) % 116.31/116.34 [16]~E(x161,x162)+E(f11(x163,x164,x165,x161),f11(x163,x164,x165,x162)) % 116.31/116.34 [17]~E(x171,x172)+E(f10(x171,x173,x174),f10(x172,x173,x174)) % 116.31/116.34 [18]~E(x181,x182)+E(f10(x183,x181,x184),f10(x183,x182,x184)) % 116.31/116.34 [19]~E(x191,x192)+E(f10(x193,x194,x191),f10(x193,x194,x192)) % 116.31/116.34 [20]~E(x201,x202)+E(f8(x201),f8(x202)) % 116.31/116.34 [21]~E(x211,x212)+E(f15(x211,x213,x214,x215),f15(x212,x213,x214,x215)) % 116.31/116.34 [22]~E(x221,x222)+E(f15(x223,x221,x224,x225),f15(x223,x222,x224,x225)) % 116.31/116.34 [23]~E(x231,x232)+E(f15(x233,x234,x231,x235),f15(x233,x234,x232,x235)) % 116.31/116.34 [24]~E(x241,x242)+E(f15(x243,x244,x245,x241),f15(x243,x244,x245,x242)) % 116.31/116.34 [25]~E(x251,x252)+E(f9(x251),f9(x252)) % 116.31/116.34 [26]~E(x261,x262)+E(f4(x261,x263,x264),f4(x262,x263,x264)) % 116.31/116.34 [27]~E(x271,x272)+E(f4(x273,x271,x274),f4(x273,x272,x274)) % 116.31/116.34 [28]~E(x281,x282)+E(f4(x283,x284,x281),f4(x283,x284,x282)) % 116.31/116.34 [29]~P1(x291)+P1(x292)+~E(x291,x292) % 116.31/116.34 [30]~P2(x301)+P2(x302)+~E(x301,x302) % 116.31/116.34 [31]~P5(x311)+P5(x312)+~E(x311,x312) % 116.31/116.34 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324) % 116.31/116.34 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334) % 116.31/116.34 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341) % 116.31/116.34 [35]~P6(x351)+P6(x352)+~E(x351,x352) % 116.31/116.34 [36]P4(x362,x363,x364)+~E(x361,x362)+~P4(x361,x363,x364) % 116.31/116.34 [37]P4(x373,x372,x374)+~E(x371,x372)+~P4(x373,x371,x374) % 116.31/116.34 [38]P4(x383,x384,x382)+~E(x381,x382)+~P4(x383,x384,x381) % 116.31/116.34 [39]P9(x392,x393,x394)+~E(x391,x392)+~P9(x391,x393,x394) % 116.31/116.34 [40]P9(x403,x402,x404)+~E(x401,x402)+~P9(x403,x401,x404) % 116.31/116.34 [41]P9(x413,x414,x412)+~E(x411,x412)+~P9(x413,x414,x411) % 116.31/116.34 [42]P10(x422,x423,x424)+~E(x421,x422)+~P10(x421,x423,x424) % 116.31/116.34 [43]P10(x433,x432,x434)+~E(x431,x432)+~P10(x433,x431,x434) % 116.31/116.34 [44]P10(x443,x444,x442)+~E(x441,x442)+~P10(x443,x444,x441) % 116.31/116.34 [45]P7(x452,x453)+~E(x451,x452)+~P7(x451,x453) % 116.31/116.34 [46]P7(x463,x462)+~E(x461,x462)+~P7(x463,x461) % 116.31/116.34 [47]~P8(x471)+P8(x472)+~E(x471,x472) % 116.31/116.34 % 116.31/116.34 %------------------------------------------- % 116.31/116.36 cnf(106,plain, % 116.31/116.36 (~P1(a1)+P4(f8(a1),a1,a5)), % 116.31/116.36 inference(equality_inference,[],[62])). % 116.31/116.36 cnf(107,plain, % 116.31/116.36 (~P1(x1071)+~P1(x1071)+P9(x1071,x1072,x1071)+~P2(x1072)), % 116.31/116.36 inference(equality_inference,[],[68])). % 116.31/116.36 cnf(108,plain, % 116.31/116.36 (P4(f8(a1),a1,a5)), % 116.31/116.36 inference(scs_inference,[],[48,106])). % 116.31/116.36 cnf(109,plain, % 116.31/116.36 (~P7(a1,a1)), % 116.31/116.36 inference(scs_inference,[],[48,51,70])). % 116.31/116.36 cnf(112,plain, % 116.31/116.36 (P9(a1,a5,a1)), % 116.31/116.36 inference(scs_inference,[],[48,51,49,70,107])). % 116.31/116.36 cnf(114,plain, % 116.31/116.36 (P9(x1141,a5,a1)+~E(a1,x1141)), % 116.31/116.36 inference(scs_inference,[],[48,51,49,70,107,39])). % 116.31/116.36 cnf(122,plain, % 116.31/116.36 (~P1(f8(a1))+P4(f8(f8(a1)),f8(a1),a5)), % 116.31/116.36 inference(scs_inference,[],[108,79])). % 116.31/116.36 cnf(125,plain, % 116.31/116.36 (P4(f8(a1),x1251,a5)+~E(a1,x1251)), % 116.31/116.36 inference(scs_inference,[],[108,79,36,37])). % 116.31/116.36 cnf(127,plain, % 116.31/116.36 (P7(f8(a1),a1)+~P1(f8(a1))), % 116.31/116.36 inference(scs_inference,[],[48,108,79,36,37,38,75])). % 116.31/116.36 cnf(133,plain, % 116.31/116.36 (P10(a1,a5,f8(a1))+~P1(f8(a1))), % 116.31/116.36 inference(scs_inference,[],[48,108,49,85])). % 116.31/116.36 cnf(136,plain, % 116.31/116.36 (~P1(f8(a1))+~P10(f8(a1),a5,a1)), % 116.31/116.36 inference(scs_inference,[],[48,109,108,89])). % 116.31/116.36 cnf(167,plain, % 116.31/116.36 (~E(f8(a1),a1)+~P1(f8(a1))), % 116.31/116.36 inference(scs_inference,[],[109,127,45])). % 116.31/116.36 cnf(351,plain, % 116.31/116.36 (P1(f8(f8(a1)))+~P1(f8(a1))), % 116.31/116.36 inference(scs_inference,[],[49,122,73])). % 116.31/116.36 cnf(534,plain, % 116.31/116.36 (~E(x5341,a5)+~P2(a5)+P2(x5341)), % 116.31/116.36 inference(scs_inference,[],[49,30,2])). % 116.31/116.36 cnf(536,plain, % 116.31/116.36 (P2(x5361)+~E(x5361,a5)), % 116.31/116.36 inference(scs_inference,[],[49,534])). % 116.31/116.36 cnf(1059,plain, % 116.31/116.36 (~P10(a1,a5,a1)), % 116.31/116.36 inference(scs_inference,[],[109,48,46,76])). % 116.31/116.36 cnf(1442,plain, % 116.31/116.36 (~E(a1,x14421)+P4(f4(a1,a5,a1),a1,a5)), % 116.31/116.36 inference(scs_inference,[],[51,112,48,49,32,99])). % 116.31/116.36 cnf(1443,plain, % 116.31/116.36 (P4(f4(a1,a5,a1),a1,a5)), % 116.31/116.36 inference(equality_inference,[],[1442])). % 116.31/116.36 cnf(1444,plain, % 116.31/116.36 (~P1(f4(a1,a5,a1))+P4(f8(f4(a1,a5,a1)),f4(a1,a5,a1),a5)), % 116.31/116.36 inference(scs_inference,[],[1443,79])). % 116.31/116.36 cnf(1449,plain, % 116.31/116.36 (P7(f4(a1,a5,a1),a1)+~P1(f4(a1,a5,a1))), % 116.31/116.36 inference(scs_inference,[],[48,1443,79,38,36,37,75])). % 116.31/116.36 cnf(1451,plain, % 116.31/116.36 (P10(a1,a5,f4(a1,a5,a1))+~P1(f4(a1,a5,a1))), % 116.31/116.36 inference(scs_inference,[],[48,1443,49,79,38,36,37,75,85])). % 116.31/116.36 cnf(1472,plain, % 116.31/116.36 (~E(f4(a1,a5,a1),a1)+~P1(f4(a1,a5,a1))), % 116.31/116.36 inference(scs_inference,[],[109,1449,45])). % 116.31/116.36 cnf(1488,plain, % 116.31/116.36 (~E(f4(a1,a5,a1),a1)), % 116.31/116.36 inference(scs_inference,[],[1443,48,49,1472,73])). % 116.31/116.36 cnf(1504,plain, % 116.31/116.36 (P9(a1,a5,f4(a1,a5,a1))+~P1(f4(a1,a5,a1))), % 116.31/116.36 inference(scs_inference,[],[48,49,1451,86])). % 116.31/116.36 cnf(1537,plain, % 116.31/116.36 (P9(a1,a5,f4(a1,a5,a1))), % 116.31/116.36 inference(scs_inference,[],[1443,48,49,1504,73])). % 116.31/116.36 cnf(1561,plain, % 116.31/116.36 (P1(f8(f4(a1,a5,a1)))+~P1(f4(a1,a5,a1))), % 116.31/116.36 inference(scs_inference,[],[49,1444,73])). % 116.31/116.36 cnf(1690,plain, % 116.31/116.36 (~P10(a1,a5,x16901)+~E(x16901,a1)), % 116.31/116.36 inference(scs_inference,[],[50,109,49,48,44,78])). % 116.31/116.36 cnf(1707,plain, % 116.31/116.36 (~P10(a1,a5,f8(a1))+P4(f8(f8(a1)),f8(a1),a5)), % 116.31/116.36 inference(scs_inference,[],[108,48,49,80,73])). % 116.31/116.36 cnf(1968,plain, % 116.31/116.36 (P1(f8(a1))), % 116.31/116.36 inference(scs_inference,[],[108,48,536,73])). % 116.31/116.36 cnf(1969,plain, % 116.31/116.36 (P4(f8(f8(a1)),f8(a1),a5)), % 116.31/116.36 inference(scs_inference,[],[1968,122])). % 116.31/116.36 cnf(1970,plain, % 116.31/116.36 (P7(f8(a1),a1)), % 116.31/116.36 inference(scs_inference,[],[1968,127])). % 116.31/116.36 cnf(1971,plain, % 116.31/116.36 (P10(a1,a5,f8(a1))), % 116.31/116.36 inference(scs_inference,[],[1968,133])). % 116.31/116.36 cnf(1972,plain, % 116.31/116.36 (~P10(f8(a1),a5,a1)), % 116.31/116.36 inference(scs_inference,[],[1968,136])). % 116.31/116.36 cnf(1973,plain, % 116.31/116.36 (~E(f8(a1),a1)), % 116.31/116.36 inference(scs_inference,[],[1968,167])). % 116.31/116.36 cnf(1976,plain, % 116.31/116.36 (P1(f8(f8(a1)))), % 116.31/116.36 inference(scs_inference,[],[1968,351])). % 116.31/116.36 cnf(1977,plain, % 116.31/116.36 (~P3(a1,f8(a1),a5)), % 116.31/116.36 inference(scs_inference,[],[108,1968,49,88])). % 116.31/116.36 cnf(1979,plain, % 116.31/116.36 (P9(f8(a1),a5,f8(a1))), % 116.31/116.36 inference(scs_inference,[],[108,1968,49,88,68])). % 116.31/116.36 cnf(1984,plain, % 116.31/116.36 (P4(f8(f8(a1)),f8(a1),a5)), % 116.31/116.36 inference(scs_inference,[],[1971,1707])). % 116.31/116.36 cnf(1989,plain, % 116.31/116.36 (P10(f8(a1),a5,f8(f8(a1)))), % 116.31/116.36 inference(scs_inference,[],[48,1969,1971,1976,1968,49,75,86,85])). % 116.31/116.36 cnf(1997,plain, % 116.31/116.36 (~E(f8(f8(a1)),a1)), % 116.31/116.36 inference(scs_inference,[],[108,48,1969,1971,1976,1968,49,1972,75,86,85,89,93,94,1690])). % 116.31/116.36 cnf(1999,plain, % 116.31/116.36 (P7(f8(a1),x19991)+~E(a1,x19991)), % 116.31/116.36 inference(scs_inference,[],[108,48,1969,1970,1971,1976,1968,49,1972,75,86,85,89,93,94,1690,45,46])). % 116.31/116.36 cnf(2000,plain, % 116.31/116.36 (P4(f8(f8(a1)),x20001,a5)+~E(f8(a1),x20001)), % 116.31/116.36 inference(scs_inference,[],[108,48,1969,1970,1971,1976,1968,49,1972,75,86,85,89,93,94,1690,45,46,37])). % 116.31/116.36 cnf(2010,plain, % 116.31/116.36 (~P3(f8(a1),f8(f8(a1)),a5)), % 116.31/116.36 inference(scs_inference,[],[1984,1976,49,88])). % 116.31/116.36 cnf(2012,plain, % 116.31/116.36 (P9(f8(a1),a5,f8(f8(a1)))), % 116.31/116.36 inference(scs_inference,[],[1984,1976,1968,1989,49,88,86])). % 116.31/116.36 cnf(2026,plain, % 116.31/116.36 (~P3(f8(a1),f8(a1),a5)), % 116.31/116.36 inference(scs_inference,[],[1984,1968,49,88])). % 116.31/116.36 cnf(2075,plain, % 116.31/116.36 (P9(f8(a1),a5,a1)+~P9(f8(f8(a1)),a5,a1)), % 116.31/116.36 inference(scs_inference,[],[48,1968,1976,2012,49,95])). % 116.31/116.36 cnf(2101,plain, % 116.31/116.36 (P9(f8(a1),a5,a1)+~E(a1,f8(f8(a1)))), % 116.31/116.36 inference(scs_inference,[],[2075,114])). % 116.31/116.36 cnf(2117,plain, % 116.31/116.36 (~E(a1,f8(f8(a1)))), % 116.31/116.36 inference(scs_inference,[],[1973,1972,48,1968,49,2101,87])). % 116.31/116.36 cnf(3827,plain, % 116.31/116.36 (~P3(x38271,f8(a1),a5)+~E(x38271,a1)), % 116.31/116.36 inference(scs_inference,[],[1973,1977,1488,2,3,32])). % 116.31/116.36 cnf(3836,plain, % 116.31/116.36 (~P3(x38361,f8(a1),a5)+~E(x38361,f8(a1))), % 116.31/116.36 inference(scs_inference,[],[2026,1997,33,3,32])). % 116.31/116.36 cnf(3851,plain, % 116.31/116.36 (P1(f4(a1,a5,a1))), % 116.31/116.36 inference(scs_inference,[],[48,1443,2010,49,2117,33,3,32,73])). % 116.31/116.36 cnf(3861,plain, % 116.31/116.36 (~P10(f4(a1,a5,a1),a5,a1)), % 116.31/116.36 inference(scs_inference,[],[1984,48,1443,1059,2010,49,2117,33,3,32,73,88,107,75,85,94])). % 116.31/116.36 cnf(3867,plain, % 116.31/116.36 (P4(f8(f4(a1,a5,a1)),f4(a1,a5,a1),a5)), % 116.31/116.36 inference(scs_inference,[],[3851,1444])). % 116.31/116.36 cnf(3869,plain, % 116.31/116.36 (P1(f8(f4(a1,a5,a1)))), % 116.31/116.36 inference(scs_inference,[],[3851,1561])). % 116.31/116.36 cnf(3886,plain, % 116.31/116.36 (P7(f8(f4(a1,a5,a1)),a1)), % 116.31/116.36 inference(scs_inference,[],[1969,48,3867,1443,3851,3869,49,88,75,85,89])). % 116.31/116.36 cnf(3890,plain, % 116.31/116.36 (P10(a1,a5,f8(f4(a1,a5,a1)))), % 116.31/116.36 inference(scs_inference,[],[1969,48,3867,1443,3851,3869,49,3861,88,75,85,89,94,93])). % 116.31/116.36 cnf(7610,plain, % 116.31/116.36 (P4(f8(f4(a1,a5,a1)),x76101,a5)+~E(f4(a1,a5,a1),x76101)), % 116.31/116.36 inference(scs_inference,[],[3867,37])). % 116.31/116.36 cnf(8362,plain, % 116.31/116.36 (~P9(f4(a1,a5,a1),a5,a1)), % 116.31/116.36 inference(scs_inference,[],[48,3861,1488,109,49,3851,75,87])). % 116.31/116.36 cnf(8395,plain, % 116.31/116.36 (~E(a1,x83951)+P1(x83951)), % 116.31/116.36 inference(scs_inference,[],[48,3861,49,3851,75,85,29])). % 116.31/116.36 cnf(8399,plain, % 116.31/116.36 (~P4(a1,f8(a1),a5)), % 116.31/116.36 inference(scs_inference,[],[48,49,1972,3851,1968,76,85])). % 116.31/116.36 cnf(8432,plain, % 116.31/116.36 (~E(f8(a1),x84321)+P1(x84321)), % 116.31/116.36 inference(scs_inference,[],[8362,1968,40,29])). % 116.31/116.36 cnf(8439,plain, % 116.31/116.36 (P1(x84391)+~P4(x84391,f4(a1,a5,a1),a5)), % 116.31/116.36 inference(scs_inference,[],[49,3851,73])). % 116.31/116.36 cnf(9874,plain, % 116.31/116.36 (~P4(x98741,f8(a1),a5)+~E(x98741,a1)), % 116.31/116.36 inference(scs_inference,[],[8399,36])). % 116.31/116.36 cnf(10780,plain, % 116.31/116.36 (P4(f4(a1,a5,f4(a1,a5,a1)),f4(a1,a5,a1),a5)), % 116.31/116.36 inference(scs_inference,[],[3851,49,1537,51,8395,99])). % 116.31/116.36 cnf(10974,plain, % 116.31/116.36 (P1(f8(x109741))+~E(a1,x109741)), % 116.31/116.36 inference(scs_inference,[],[8432,20])). % 116.31/116.36 cnf(11037,plain, % 116.31/116.36 (P4(f4(f8(a1),a5,f8(a1)),f8(a1),a5)), % 116.31/116.36 inference(scs_inference,[],[49,2026,1979,10974,99])). % 116.31/116.36 cnf(11137,plain, % 116.31/116.36 (P1(f7(f8(a1)))), % 116.31/116.36 inference(scs_inference,[],[1968,1999,60])). % 116.31/116.36 cnf(11154,plain, % 116.31/116.36 (P3(f7(f8(a1)),f8(a1),a5)), % 116.31/116.36 inference(scs_inference,[],[1968,1999,70])). % 116.31/116.36 cnf(11162,plain, % 116.31/116.36 (~P4(x111621,f7(f8(a1)),a5)), % 116.31/116.36 inference(scs_inference,[],[1968,1999,77])). % 116.31/116.36 cnf(11170,plain, % 116.31/116.36 (E(f7(f8(a1)),f8(a1))+P10(f8(a1),a5,f7(f8(a1)))), % 116.31/116.36 inference(scs_inference,[],[1968,1999,71])). % 116.31/116.36 cnf(13011,plain, % 116.31/116.36 (~P4(x130111,f7(f8(a1)),a5)), % 116.31/116.36 inference(rename_variables,[],[11162])). % 116.31/116.36 cnf(13015,plain, % 116.31/116.36 (P1(f4(a1,a5,f4(a1,a5,a1)))), % 116.31/116.36 inference(scs_inference,[],[10780,11037,11154,11162,125,3827,9874,3836,8439])). % 116.31/116.36 cnf(13018,plain, % 116.31/116.36 (~P4(x130181,f7(f8(a1)),a5)), % 116.31/116.36 inference(rename_variables,[],[11162])). % 116.31/116.36 cnf(13019,plain, % 116.31/116.36 (P10(f8(a1),a5,f7(f8(a1)))), % 116.31/116.36 inference(scs_inference,[],[10780,11037,11154,11162,13011,125,3827,9874,3836,8439,7610,11170])). % 116.31/116.36 cnf(13021,plain, % 116.31/116.36 (P1(f7(f8(f4(a1,a5,a1))))), % 116.31/116.36 inference(scs_inference,[],[10780,11037,11154,11162,13011,3886,3869,125,3827,9874,3836,8439,7610,11170,2,60])). % 116.31/116.36 cnf(13023,plain, % 116.31/116.36 (~P4(x130231,f7(f8(f4(a1,a5,a1))),a5)), % 116.31/116.36 inference(scs_inference,[],[10780,11037,11154,11162,13011,3886,3869,125,3827,9874,3836,8439,7610,11170,2,60,77])). % 116.31/116.36 cnf(13025,plain, % 116.31/116.36 (P4(f8(f8(f4(a1,a5,a1))),f8(f4(a1,a5,a1)),a5)), % 116.31/116.36 inference(scs_inference,[],[10780,11037,11154,11162,13011,3890,3886,3869,125,3827,9874,3836,8439,7610,11170,2,60,77,80])). % 116.31/116.36 cnf(13036,plain, % 116.31/116.36 (P1(f8(f8(f4(a1,a5,a1))))), % 116.31/116.36 inference(scs_inference,[],[10780,11037,11154,11137,11162,13011,13018,3890,3886,3869,49,125,3827,9874,3836,8439,7610,11170,2,60,77,80,69,62,81,70,73])). % 116.31/116.36 cnf(13135,plain, % 116.31/116.36 (~P4(x131351,f7(f8(f4(a1,a5,a1))),a5)), % 116.31/116.36 inference(rename_variables,[],[13023])). % 116.31/116.36 cnf(13137,plain, % 116.31/116.36 (~P4(x131371,f7(f8(f4(a1,a5,a1))),a5)), % 116.31/116.36 inference(rename_variables,[],[13023])). % 116.31/116.36 cnf(13140,plain, % 116.31/116.36 (~P4(x131401,f7(f8(f4(a1,a5,a1))),a5)), % 116.31/116.36 inference(rename_variables,[],[13023])). % 116.31/116.36 cnf(13143,plain, % 116.31/116.36 (~P4(x131431,f7(f8(f4(a1,a5,a1))),a5)), % 116.31/116.36 inference(rename_variables,[],[13023])). % 116.31/116.36 cnf(13153,plain, % 116.31/116.36 ($false), % 116.31/116.36 inference(scs_inference,[],[13015,13019,13021,13036,13023,13135,13137,13140,13143,13025,11162,11137,3869,108,49,1968,2000,80,81,79,37,88,75,107,92]), % 116.31/116.36 ['proof']). % 116.31/116.36 % SZS output end Proof % 116.31/116.36 % Total time :115.690000s %------------------------------------------------------------------------------