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