%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM022+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 : n001.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:48 EDT 2024 % Result : Theorem 39.80s 39.86s % Output : CNFRefutation 39.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COM022+1 : TPTP v8.2.0. Released v4.0.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n001.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:13:38 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 39.80/39.85 %------------------------------------------- % 39.80/39.85 % File :CSE---1.7 % 39.80/39.85 % Problem :theBenchmark % 39.80/39.85 % Transform :cnf % 39.80/39.85 % Format :tptp:raw % 39.80/39.85 % Command :java -jar mcs_scs.jar %d %s % 39.80/39.85 % 39.80/39.85 % Result :Theorem 39.230000s % 39.80/39.85 % Output :CNFRefutation 39.230000s % 39.80/39.85 %------------------------------------------- % 39.80/39.85 %------------------------------------------------------------------------------ % 39.80/39.85 % File : COM022+1 : TPTP v8.2.0. Released v4.0.0. % 39.80/39.85 % Domain : Computing Theory % 39.80/39.85 % Problem : Newman's lemma on rewriting systems 03_01_07, 00 expansion % 39.80/39.85 % Version : Especial. % 39.80/39.85 % English : % 39.80/39.85 % 39.80/39.85 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 39.80/39.85 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 39.80/39.85 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 39.80/39.85 % Source : [Pas08] % 39.80/39.85 % Names : newman_03_01_07.00 [Pas08] % 39.80/39.85 % 39.80/39.85 % Status : Theorem % 39.80/39.85 % Rating : 0.22 v8.1.0, 0.14 v7.5.0, 0.19 v7.4.0, 0.20 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.33 v5.4.0, 0.32 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.38 v4.1.0, 0.43 v4.0.1, 0.57 v4.0.0 % 39.80/39.85 % Syntax : Number of formulae : 19 ( 1 unt; 6 def) % 39.80/39.85 % Number of atoms : 115 ( 1 equ) % 39.80/39.85 % Maximal formula atoms : 19 ( 6 avg) % 39.80/39.85 % Number of connectives : 97 ( 1 ~; 2 |; 59 &) % 39.80/39.85 % ( 6 <=>; 29 =>; 0 <=; 0 <~>) % 39.80/39.85 % Maximal formula depth : 18 ( 7 avg) % 39.80/39.85 % Maximal term depth : 1 ( 1 avg) % 39.80/39.85 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 39.80/39.85 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 39.80/39.85 % Number of variables : 54 ( 43 !; 11 ?) % 39.80/39.85 % SPC : FOF_THM_RFO_SEQ % 39.80/39.85 % 39.80/39.85 % Comments : Problem generated by the SAD system [VLP07] % 39.80/39.85 %------------------------------------------------------------------------------ % 39.80/39.85 fof(mElmSort,axiom, % 39.80/39.85 ! [W0] : % 39.80/39.85 ( aElement0(W0) % 39.80/39.85 => $true ) ). % 39.80/39.85 % 39.80/39.85 fof(mRelSort,axiom, % 39.80/39.85 ! [W0] : % 39.80/39.85 ( aRewritingSystem0(W0) % 39.80/39.85 => $true ) ). % 39.80/39.86 % 39.80/39.86 fof(mReduct,axiom, % 39.80/39.86 ! [W0,W1] : % 39.80/39.86 ( ( aElement0(W0) % 39.80/39.86 & aRewritingSystem0(W1) ) % 39.80/39.86 => ! [W2] : % 39.80/39.86 ( aReductOfIn0(W2,W0,W1) % 39.80/39.86 => aElement0(W2) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mWFOrd,axiom, % 39.80/39.86 ! [W0,W1] : % 39.80/39.86 ( ( aElement0(W0) % 39.80/39.86 & aElement0(W1) ) % 39.80/39.86 => ( iLess0(W0,W1) % 39.80/39.86 => $true ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mTCbr,axiom, % 39.80/39.86 ! [W0,W1,W2] : % 39.80/39.86 ( ( aElement0(W0) % 39.80/39.86 & aRewritingSystem0(W1) % 39.80/39.86 & aElement0(W2) ) % 39.80/39.86 => ( sdtmndtplgtdt0(W0,W1,W2) % 39.80/39.86 => $true ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mTCDef,definition, % 39.80/39.86 ! [W0,W1,W2] : % 39.80/39.86 ( ( aElement0(W0) % 39.80/39.86 & aRewritingSystem0(W1) % 39.80/39.86 & aElement0(W2) ) % 39.80/39.86 => ( sdtmndtplgtdt0(W0,W1,W2) % 39.80/39.86 <=> ( aReductOfIn0(W2,W0,W1) % 39.80/39.86 | ? [W3] : % 39.80/39.86 ( aElement0(W3) % 39.80/39.86 & aReductOfIn0(W3,W0,W1) % 39.80/39.86 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mTCTrans,axiom, % 39.80/39.86 ! [W0,W1,W2,W3] : % 39.80/39.86 ( ( aElement0(W0) % 39.80/39.86 & aRewritingSystem0(W1) % 39.80/39.86 & aElement0(W2) % 39.80/39.86 & aElement0(W3) ) % 39.80/39.86 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 39.80/39.86 & sdtmndtplgtdt0(W2,W1,W3) ) % 39.80/39.86 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mTCRDef,definition, % 39.80/39.86 ! [W0,W1,W2] : % 39.80/39.86 ( ( aElement0(W0) % 39.80/39.86 & aRewritingSystem0(W1) % 39.80/39.86 & aElement0(W2) ) % 39.80/39.86 => ( sdtmndtasgtdt0(W0,W1,W2) % 39.80/39.86 <=> ( W0 = W2 % 39.80/39.86 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mTCRTrans,axiom, % 39.80/39.86 ! [W0,W1,W2,W3] : % 39.80/39.86 ( ( aElement0(W0) % 39.80/39.86 & aRewritingSystem0(W1) % 39.80/39.86 & aElement0(W2) % 39.80/39.86 & aElement0(W3) ) % 39.80/39.86 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 39.80/39.86 & sdtmndtasgtdt0(W2,W1,W3) ) % 39.80/39.86 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mCRDef,definition, % 39.80/39.86 ! [W0] : % 39.80/39.86 ( aRewritingSystem0(W0) % 39.80/39.86 => ( isConfluent0(W0) % 39.80/39.86 <=> ! [W1,W2,W3] : % 39.80/39.86 ( ( aElement0(W1) % 39.80/39.86 & aElement0(W2) % 39.80/39.86 & aElement0(W3) % 39.80/39.86 & sdtmndtasgtdt0(W1,W0,W2) % 39.80/39.86 & sdtmndtasgtdt0(W1,W0,W3) ) % 39.80/39.86 => ? [W4] : % 39.80/39.86 ( aElement0(W4) % 39.80/39.86 & sdtmndtasgtdt0(W2,W0,W4) % 39.80/39.86 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mWCRDef,definition, % 39.80/39.86 ! [W0] : % 39.80/39.86 ( aRewritingSystem0(W0) % 39.80/39.86 => ( isLocallyConfluent0(W0) % 39.80/39.86 <=> ! [W1,W2,W3] : % 39.80/39.86 ( ( aElement0(W1) % 39.80/39.86 & aElement0(W2) % 39.80/39.86 & aElement0(W3) % 39.80/39.86 & aReductOfIn0(W2,W1,W0) % 39.80/39.86 & aReductOfIn0(W3,W1,W0) ) % 39.80/39.86 => ? [W4] : % 39.80/39.86 ( aElement0(W4) % 39.80/39.86 & sdtmndtasgtdt0(W2,W0,W4) % 39.80/39.86 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mTermin,definition, % 39.80/39.86 ! [W0] : % 39.80/39.86 ( aRewritingSystem0(W0) % 39.80/39.86 => ( isTerminating0(W0) % 39.80/39.86 <=> ! [W1,W2] : % 39.80/39.86 ( ( aElement0(W1) % 39.80/39.86 & aElement0(W2) ) % 39.80/39.86 => ( sdtmndtplgtdt0(W1,W0,W2) % 39.80/39.86 => iLess0(W2,W1) ) ) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mNFRDef,definition, % 39.80/39.86 ! [W0,W1] : % 39.80/39.86 ( ( aElement0(W0) % 39.80/39.86 & aRewritingSystem0(W1) ) % 39.80/39.86 => ! [W2] : % 39.80/39.86 ( aNormalFormOfIn0(W2,W0,W1) % 39.80/39.86 <=> ( aElement0(W2) % 39.80/39.86 & sdtmndtasgtdt0(W0,W1,W2) % 39.80/39.86 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(mTermNF,axiom, % 39.80/39.86 ! [W0] : % 39.80/39.86 ( ( aRewritingSystem0(W0) % 39.80/39.86 & isTerminating0(W0) ) % 39.80/39.86 => ! [W1] : % 39.80/39.86 ( aElement0(W1) % 39.80/39.86 => ? [W2] : aNormalFormOfIn0(W2,W1,W0) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(m__656,hypothesis, % 39.80/39.86 aRewritingSystem0(xR) ). % 39.80/39.86 % 39.80/39.86 fof(m__656_01,hypothesis, % 39.80/39.86 ( isLocallyConfluent0(xR) % 39.80/39.86 & isTerminating0(xR) ) ). % 39.80/39.86 % 39.80/39.86 fof(m__731,hypothesis, % 39.80/39.86 ( aElement0(xa) % 39.80/39.86 & aElement0(xb) % 39.80/39.86 & aElement0(xc) ) ). % 39.80/39.86 % 39.80/39.86 fof(m__715,hypothesis, % 39.80/39.86 ! [W0,W1,W2] : % 39.80/39.86 ( ( aElement0(W0) % 39.80/39.86 & aElement0(W1) % 39.80/39.86 & aElement0(W2) % 39.80/39.86 & sdtmndtasgtdt0(W0,xR,W1) % 39.80/39.86 & sdtmndtasgtdt0(W0,xR,W2) ) % 39.80/39.86 => ( iLess0(W0,xa) % 39.80/39.86 => ? [W3] : % 39.80/39.86 ( aElement0(W3) % 39.80/39.86 & sdtmndtasgtdt0(W1,xR,W3) % 39.80/39.86 & sdtmndtasgtdt0(W2,xR,W3) ) ) ) ). % 39.80/39.86 % 39.80/39.86 fof(m__,conjecture, % 39.80/39.86 ( ( ( sdtmndtplgtdt0(xa,xR,xb) % 39.80/39.86 & sdtmndtplgtdt0(xa,xR,xc) ) % 39.80/39.86 => ? [W0] : % 39.80/39.86 ( aElement0(W0) % 39.80/39.86 & aReductOfIn0(W0,xa,xR) % 39.80/39.86 & sdtmndtasgtdt0(W0,xR,xb) % 39.80/39.86 & ? [W1] : % 39.80/39.86 ( aElement0(W1) % 39.80/39.86 & aReductOfIn0(W1,xa,xR) % 39.80/39.86 & sdtmndtasgtdt0(W1,xR,xc) % 39.80/39.86 & ? [W2] : % 39.80/39.86 ( aElement0(W2) % 39.80/39.86 & sdtmndtasgtdt0(W0,xR,W2) % 39.80/39.86 & sdtmndtasgtdt0(W1,xR,W2) % 39.80/39.86 & ? [W3] : % 39.80/39.86 ( aNormalFormOfIn0(W3,W2,xR) % 39.80/39.86 & sdtmndtasgtdt0(xb,xR,W3) % 39.80/39.86 & sdtmndtasgtdt0(xc,xR,W3) ) ) ) ) ) % 39.80/39.86 => ( ( sdtmndtasgtdt0(xa,xR,xb) % 39.80/39.86 & sdtmndtasgtdt0(xa,xR,xc) ) % 39.80/39.86 => ? [W0] : % 39.80/39.86 ( aElement0(W0) % 39.80/39.86 & sdtmndtasgtdt0(xb,xR,W0) % 39.80/39.86 & sdtmndtasgtdt0(xc,xR,W0) ) ) ) ). % 39.80/39.86 % 39.80/39.86 %------------------------------------------------------------------------------ % 39.80/39.86 %------------------------------------------- % 39.80/39.86 % Proof found % 39.80/39.86 % SZS status Theorem for theBenchmark % 39.80/39.86 % SZS output start Proof % 39.80/39.86 %ClaNum:112(EqnAxiom:49) % 39.80/39.86 %VarNum:381(SingletonVarNum:106) % 39.80/39.86 %MaxLitNum:8 % 39.80/39.86 %MaxfuncDepth:1 % 39.80/39.86 %SharedTerms:30 % 39.80/39.86 %goalClause: 56 57 78 79 80 84 86 87 88 89 90 91 92 93 94 % 39.80/39.86 %singleGoalClaCount:2 % 39.80/39.86 [50]P1(a1) % 39.80/39.86 [51]P1(a21) % 39.80/39.86 [52]P1(a22) % 39.80/39.86 [53]P2(a2) % 39.80/39.86 [54]P5(a2) % 39.80/39.86 [55]P8(a2) % 39.80/39.86 [56]P9(a1,a2,a21) % 39.80/39.86 [57]P9(a1,a2,a22) % 39.80/39.86 [78]P1(a8)+~P10(a1,a2,a21)+~P10(a1,a2,a22) % 39.80/39.86 [79]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P1(a10) % 39.80/39.86 [80]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P1(a11) % 39.80/39.86 [86]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P3(a8,a1,a2) % 39.80/39.86 [87]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P3(a10,a1,a2) % 39.80/39.86 [88]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P9(a21,a2,a12) % 39.80/39.86 [89]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P9(a22,a2,a12) % 39.80/39.86 [90]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P9(a8,a2,a21) % 39.80/39.86 [91]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P9(a8,a2,a11) % 39.80/39.86 [92]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P9(a10,a2,a22) % 39.80/39.86 [93]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P9(a10,a2,a11) % 39.80/39.86 [94]~P10(a1,a2,a21)+~P10(a1,a2,a22)+P4(a12,a11,a2) % 39.80/39.86 [84]~P1(x841)+~P9(a21,a2,x841)+~P9(a22,a2,x841) % 39.80/39.86 [58]~P2(x581)+P6(x581)+P1(f3(x581)) % 39.80/39.86 [59]~P2(x591)+P6(x591)+P1(f15(x591)) % 39.80/39.86 [60]~P2(x601)+P6(x601)+P1(f16(x601)) % 39.80/39.86 [61]~P2(x611)+P5(x611)+P1(f17(x611)) % 39.80/39.86 [62]~P2(x621)+P5(x621)+P1(f19(x621)) % 39.80/39.86 [63]~P2(x631)+P5(x631)+P1(f20(x631)) % 39.80/39.86 [64]~P2(x641)+P8(x641)+P1(f4(x641)) % 39.80/39.86 [65]~P2(x651)+P8(x651)+P1(f5(x651)) % 39.80/39.86 [66]~P2(x661)+P8(x661)+~P7(f5(x661),f4(x661)) % 39.80/39.86 [67]~P2(x671)+P6(x671)+P9(f3(x671),x671,f15(x671)) % 39.80/39.86 [68]~P2(x681)+P6(x681)+P9(f3(x681),x681,f16(x681)) % 39.80/39.86 [69]~P2(x691)+P8(x691)+P10(f4(x691),x691,f5(x691)) % 39.80/39.86 [70]~P2(x701)+P5(x701)+P3(f19(x701),f17(x701),x701) % 39.80/39.86 [71]~P2(x711)+P5(x711)+P3(f20(x711),f17(x711),x711) % 39.80/39.87 [73]~P1(x732)+~P2(x731)+~P8(x731)+P4(f6(x731,x732),x732,x731) % 39.80/39.87 [74]~P3(x741,x742,x743)+P1(x741)+~P1(x742)+~P2(x743) % 39.80/39.87 [75]~P4(x751,x752,x753)+P1(x751)+~P1(x752)+~P2(x753) % 39.80/39.87 [77]~P1(x771)+~P2(x772)+~P4(x773,x771,x772)+P9(x771,x772,x773) % 39.80/39.87 [85]~P4(x854,x851,x852)+~P1(x851)+~P3(x853,x854,x852)+~P2(x852) % 39.80/39.87 [95]~P2(x951)+P6(x951)+~P1(x952)+~P9(f15(x951),x951,x952)+~P9(f16(x951),x951,x952) % 39.80/39.87 [96]~P2(x961)+P5(x961)+~P1(x962)+~P9(f19(x961),x961,x962)+~P9(f20(x961),x961,x962) % 39.80/39.87 [72]~E(x721,x723)+~P1(x723)+~P1(x721)+~P2(x722)+P9(x721,x722,x723) % 39.80/39.87 [81]~P1(x811)+~P1(x813)+~P2(x812)+~P3(x813,x811,x812)+P10(x811,x812,x813) % 39.80/39.87 [82]~P1(x823)+~P1(x821)+~P2(x822)+~P10(x821,x822,x823)+P9(x821,x822,x823) % 39.80/39.87 [76]~P1(x761)+~P1(x762)+~P8(x763)+~P10(x762,x763,x761)+P7(x761,x762)+~P2(x763) % 39.80/39.87 [83]~P1(x832)+~P1(x831)+~P2(x833)+~P9(x831,x833,x832)+E(x831,x832)+P10(x831,x833,x832) % 39.80/39.87 [100]~P1(x1001)+~P1(x1002)+~P2(x1003)+~P10(x1002,x1003,x1001)+P3(x1001,x1002,x1003)+P1(f13(x1002,x1003,x1001)) % 39.80/39.87 [102]~P1(x1021)+~P1(x1022)+~P2(x1023)+~P10(x1022,x1023,x1021)+P3(x1021,x1022,x1023)+P3(f13(x1022,x1023,x1021),x1022,x1023) % 39.80/39.87 [103]~P1(x1031)+~P1(x1032)+~P2(x1033)+~P10(x1032,x1033,x1031)+P3(x1031,x1032,x1033)+P10(f13(x1032,x1033,x1031),x1033,x1031) % 39.80/39.87 [104]~P1(x1042)+~P1(x1041)+~P2(x1043)+~P9(x1042,x1043,x1041)+P4(x1041,x1042,x1043)+P3(f7(x1042,x1043,x1041),x1041,x1043) % 39.80/39.87 [101]~P1(x1013)+~P1(x1012)+~P1(x1011)+~P9(x1011,a2,x1013)+~P9(x1011,a2,x1012)+~P7(x1011,a1)+P1(f9(x1011,x1012,x1013)) % 39.80/39.87 [105]~P1(x1053)+~P1(x1052)+~P1(x1051)+~P9(x1052,a2,x1053)+~P9(x1052,a2,x1051)+~P7(x1052,a1)+P9(x1051,a2,f9(x1052,x1053,x1051)) % 39.80/39.87 [106]~P1(x1063)+~P1(x1062)+~P1(x1061)+~P9(x1062,a2,x1063)+~P9(x1062,a2,x1061)+~P7(x1062,a1)+P9(x1061,a2,f9(x1062,x1061,x1063)) % 39.80/39.87 [97]~P1(x973)+~P1(x971)+~P2(x972)+~P3(x974,x971,x972)+~P10(x974,x972,x973)+P10(x971,x972,x973)+~P1(x974) % 39.80/39.87 [98]~P1(x983)+~P1(x981)+~P2(x982)+~P10(x984,x982,x983)+~P10(x981,x982,x984)+P10(x981,x982,x983)+~P1(x984) % 39.80/39.87 [99]~P1(x993)+~P1(x991)+~P2(x992)+~P9(x994,x992,x993)+~P9(x991,x992,x994)+P9(x991,x992,x993)+~P1(x994) % 39.80/39.87 [107]~P1(x1074)+~P1(x1073)+~P1(x1072)+~P2(x1071)+~P6(x1071)+~P9(x1072,x1071,x1074)+~P9(x1072,x1071,x1073)+P1(f14(x1071,x1072,x1073,x1074)) % 39.80/39.87 [108]~P1(x1084)+~P1(x1083)+~P1(x1082)+~P2(x1081)+~P5(x1081)+~P3(x1084,x1082,x1081)+~P3(x1083,x1082,x1081)+P1(f18(x1081,x1082,x1083,x1084)) % 39.80/39.87 [109]~P1(x1094)+~P1(x1093)+~P1(x1091)+~P2(x1092)+~P6(x1092)+~P9(x1093,x1092,x1094)+~P9(x1093,x1092,x1091)+P9(x1091,x1092,f14(x1092,x1093,x1094,x1091)) % 39.80/39.87 [110]~P1(x1104)+~P1(x1103)+~P1(x1101)+~P2(x1102)+~P6(x1102)+~P9(x1103,x1102,x1104)+~P9(x1103,x1102,x1101)+P9(x1101,x1102,f14(x1102,x1103,x1101,x1104)) % 39.80/39.87 [111]~P1(x1114)+~P1(x1113)+~P1(x1111)+~P2(x1112)+~P5(x1112)+~P3(x1114,x1113,x1112)+~P3(x1111,x1113,x1112)+P9(x1111,x1112,f18(x1112,x1113,x1114,x1111)) % 39.80/39.87 [112]~P1(x1124)+~P1(x1123)+~P1(x1121)+~P2(x1122)+~P5(x1122)+~P3(x1124,x1123,x1122)+~P3(x1121,x1123,x1122)+P9(x1121,x1122,f18(x1122,x1123,x1121,x1124)) % 39.80/39.87 %EqnAxiom % 39.80/39.87 [1]E(x11,x11) % 39.80/39.87 [2]E(x22,x21)+~E(x21,x22) % 39.80/39.87 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 39.80/39.87 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 39.80/39.87 [5]~E(x51,x52)+E(f15(x51),f15(x52)) % 39.80/39.87 [6]~E(x61,x62)+E(f16(x61),f16(x62)) % 39.80/39.87 [7]~E(x71,x72)+E(f17(x71),f17(x72)) % 39.80/39.87 [8]~E(x81,x82)+E(f19(x81),f19(x82)) % 39.80/39.87 [9]~E(x91,x92)+E(f20(x91),f20(x92)) % 39.80/39.87 [10]~E(x101,x102)+E(f4(x101),f4(x102)) % 39.80/39.87 [11]~E(x111,x112)+E(f5(x111),f5(x112)) % 39.80/39.87 [12]~E(x121,x122)+E(f13(x121,x123,x124),f13(x122,x123,x124)) % 39.80/39.87 [13]~E(x131,x132)+E(f13(x133,x131,x134),f13(x133,x132,x134)) % 39.80/39.87 [14]~E(x141,x142)+E(f13(x143,x144,x141),f13(x143,x144,x142)) % 39.80/39.87 [15]~E(x151,x152)+E(f14(x151,x153,x154,x155),f14(x152,x153,x154,x155)) % 39.80/39.87 [16]~E(x161,x162)+E(f14(x163,x161,x164,x165),f14(x163,x162,x164,x165)) % 39.80/39.87 [17]~E(x171,x172)+E(f14(x173,x174,x171,x175),f14(x173,x174,x172,x175)) % 39.80/39.87 [18]~E(x181,x182)+E(f14(x183,x184,x185,x181),f14(x183,x184,x185,x182)) % 39.80/39.87 [19]~E(x191,x192)+E(f18(x191,x193,x194,x195),f18(x192,x193,x194,x195)) % 39.80/39.87 [20]~E(x201,x202)+E(f18(x203,x201,x204,x205),f18(x203,x202,x204,x205)) % 39.80/39.87 [21]~E(x211,x212)+E(f18(x213,x214,x211,x215),f18(x213,x214,x212,x215)) % 39.80/39.87 [22]~E(x221,x222)+E(f18(x223,x224,x225,x221),f18(x223,x224,x225,x222)) % 39.80/39.87 [23]~E(x231,x232)+E(f9(x231,x233,x234),f9(x232,x233,x234)) % 39.80/39.87 [24]~E(x241,x242)+E(f9(x243,x241,x244),f9(x243,x242,x244)) % 39.80/39.87 [25]~E(x251,x252)+E(f9(x253,x254,x251),f9(x253,x254,x252)) % 39.80/39.87 [26]~E(x261,x262)+E(f6(x261,x263),f6(x262,x263)) % 39.80/39.87 [27]~E(x271,x272)+E(f6(x273,x271),f6(x273,x272)) % 39.80/39.87 [28]~E(x281,x282)+E(f7(x281,x283,x284),f7(x282,x283,x284)) % 39.80/39.87 [29]~E(x291,x292)+E(f7(x293,x291,x294),f7(x293,x292,x294)) % 39.80/39.87 [30]~E(x301,x302)+E(f7(x303,x304,x301),f7(x303,x304,x302)) % 39.80/39.87 [31]~P1(x311)+P1(x312)+~E(x311,x312) % 39.80/39.87 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324) % 39.80/39.87 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334) % 39.80/39.87 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341) % 39.80/39.87 [35]P9(x352,x353,x354)+~E(x351,x352)+~P9(x351,x353,x354) % 39.80/39.87 [36]P9(x363,x362,x364)+~E(x361,x362)+~P9(x363,x361,x364) % 39.80/39.87 [37]P9(x373,x374,x372)+~E(x371,x372)+~P9(x373,x374,x371) % 39.80/39.87 [38]~P2(x381)+P2(x382)+~E(x381,x382) % 39.80/39.87 [39]~P5(x391)+P5(x392)+~E(x391,x392) % 39.80/39.87 [40]~P8(x401)+P8(x402)+~E(x401,x402) % 39.80/39.87 [41]P10(x412,x413,x414)+~E(x411,x412)+~P10(x411,x413,x414) % 39.80/39.87 [42]P10(x423,x422,x424)+~E(x421,x422)+~P10(x423,x421,x424) % 39.80/39.87 [43]P10(x433,x434,x432)+~E(x431,x432)+~P10(x433,x434,x431) % 39.80/39.87 [44]P4(x442,x443,x444)+~E(x441,x442)+~P4(x441,x443,x444) % 39.80/39.87 [45]P4(x453,x452,x454)+~E(x451,x452)+~P4(x453,x451,x454) % 39.80/39.87 [46]P4(x463,x464,x462)+~E(x461,x462)+~P4(x463,x464,x461) % 39.80/39.87 [47]~P6(x471)+P6(x472)+~E(x471,x472) % 39.80/39.87 [48]P7(x482,x483)+~E(x481,x482)+~P7(x481,x483) % 39.80/39.87 [49]P7(x493,x492)+~E(x491,x492)+~P7(x493,x491) % 39.80/39.87 % 39.80/39.87 %------------------------------------------- % 39.80/39.87 cnf(113,plain, % 39.80/39.87 (~P1(x1131)+~P1(x1131)+P9(x1131,x1132,x1131)+~P2(x1132)), % 39.80/39.87 inference(equality_inference,[],[72])). % 39.80/39.87 cnf(114,plain, % 39.80/39.87 (P9(a1,a2,a1)), % 39.80/39.87 inference(scs_inference,[],[50,53,113])). % 39.80/39.87 cnf(116,plain, % 39.80/39.87 (P9(x1161,a2,a21)+~E(a1,x1161)), % 39.80/39.87 inference(scs_inference,[],[56,50,53,113,35])). % 39.80/39.87 cnf(123,plain, % 39.80/39.87 (P9(a22,a2,a22)), % 39.80/39.87 inference(scs_inference,[],[52,53,113])). % 39.80/39.87 cnf(125,plain, % 39.80/39.87 (P9(x1251,a2,a22)+~E(a1,x1251)), % 39.80/39.87 inference(scs_inference,[],[57,52,53,113,35])). % 39.80/39.87 cnf(129,plain, % 39.80/39.87 (P9(a21,a2,a21)), % 39.80/39.87 inference(scs_inference,[],[51,53,113])). % 39.80/39.87 cnf(132,plain, % 39.80/39.87 (~P9(a22,a2,a21)), % 39.80/39.87 inference(scs_inference,[],[114,51,53,113,35,84])). % 39.80/39.87 cnf(137,plain, % 39.80/39.87 (~E(a1,a22)), % 39.80/39.87 inference(scs_inference,[],[56,114,123,51,50,52,53,113,35,84,37,77,99,116])). % 39.80/39.87 cnf(142,plain, % 39.80/39.87 (P10(a1,a2,a22)), % 39.80/39.87 inference(scs_inference,[],[57,132,129,137,50,52,53,35,83])). % 39.80/39.87 cnf(150,plain, % 39.80/39.87 (P7(a22,x1501)+~E(a1,x1501)), % 39.80/39.87 inference(scs_inference,[],[57,132,129,137,55,50,52,53,35,83,41,76,42,43,48,49])). % 39.80/39.87 cnf(158,plain, % 39.80/39.87 (~P10(a1,a2,a21)+P1(a8)), % 39.80/39.87 inference(scs_inference,[],[142,78])). % 39.80/39.87 cnf(159,plain, % 39.80/39.87 (~P10(a1,a2,a21)+P1(a10)), % 39.80/39.87 inference(scs_inference,[],[142,79])). % 39.80/39.87 cnf(160,plain, % 39.80/39.87 (~P10(a1,a2,a21)+P1(a11)), % 39.80/39.87 inference(scs_inference,[],[142,80])). % 39.80/39.87 cnf(161,plain, % 39.80/39.87 (~P10(a1,a2,a21)+P3(a8,a1,a2)), % 39.80/39.87 inference(scs_inference,[],[142,86])). % 39.80/39.87 cnf(162,plain, % 39.80/39.87 (~P10(a1,a2,a21)+P3(a10,a1,a2)), % 39.80/39.87 inference(scs_inference,[],[142,87])). % 39.80/39.87 cnf(163,plain, % 39.80/39.87 (~P10(a1,a2,a21)+P9(a21,a2,a12)), % 39.80/39.87 inference(scs_inference,[],[142,88])). % 39.80/39.87 cnf(164,plain, % 39.80/39.87 (~P10(a1,a2,a21)+P9(a22,a2,a12)), % 39.80/39.87 inference(scs_inference,[],[142,89])). % 39.80/39.87 cnf(169,plain, % 39.80/39.87 (~P10(a1,a2,a21)+P4(a12,a11,a2)), % 39.80/39.87 inference(scs_inference,[],[142,94])). % 39.80/39.87 cnf(178,plain, % 39.80/39.87 (E(a1,a21)+P10(a1,a2,a21)), % 39.80/39.87 inference(scs_inference,[],[56,57,53,50,51,37,36,85,83])). % 39.80/39.87 cnf(217,plain, % 39.80/39.87 (E(a1,a21)+P1(a8)), % 39.80/39.87 inference(scs_inference,[],[158,178])). % 39.80/39.87 cnf(220,plain, % 39.80/39.87 (E(a1,a21)+P1(a11)), % 39.80/39.87 inference(scs_inference,[],[160,178])). % 39.80/39.87 cnf(232,plain, % 39.80/39.87 (E(a1,a21)+P3(a10,a1,a2)), % 39.80/39.87 inference(scs_inference,[],[162,178])). % 39.80/39.87 cnf(235,plain, % 39.80/39.87 (E(a1,a21)+P9(a22,a2,a12)), % 39.80/39.87 inference(scs_inference,[],[164,178])). % 39.80/39.87 cnf(372,plain, % 39.80/39.87 (P4(f6(a2,a21),a21,x3721)+~E(a2,x3721)), % 39.80/39.87 inference(scs_inference,[],[55,51,53,46,73])). % 39.80/39.87 cnf(373,plain, % 39.80/39.87 (P4(f6(a2,a21),a21,a2)), % 39.80/39.87 inference(equality_inference,[],[372])). % 39.80/39.87 cnf(10123,plain, % 39.80/39.87 (~E(a22,a1)), % 39.80/39.87 inference(scs_inference,[],[137,2])). % 39.80/39.87 cnf(10184,plain, % 39.80/39.87 (P1(f6(a2,a21))), % 39.80/39.87 inference(scs_inference,[],[51,373,10123,53,3,75])). % 39.80/39.87 cnf(10188,plain, % 39.80/39.87 (~P4(x101881,f6(a2,a21),a2)+~P3(x101882,x101881,a2)), % 39.80/39.87 inference(scs_inference,[],[51,373,10123,53,3,75,113,85])). % 39.80/39.87 cnf(10341,plain, % 39.80/39.87 (~P3(x103411,f6(a2,f6(a2,a21)),a2)), % 39.80/39.87 inference(scs_inference,[],[55,10184,53,10188,73])). % 39.80/39.87 cnf(10343,plain, % 39.80/39.87 (~P3(x103431,x103432,a2)+~E(x103432,f6(a2,f6(a2,a21)))), % 39.80/39.87 inference(scs_inference,[],[10341,34,33])). % 39.80/39.87 cnf(10397,plain, % 39.80/39.87 (P9(a21,a2,a22)+P1(a8)), % 39.80/39.87 inference(scs_inference,[],[217,125])). % 39.80/39.87 cnf(10398,plain, % 39.80/39.87 (P1(a8)), % 39.80/39.87 inference(scs_inference,[],[123,52,10397,84])). % 39.80/39.87 cnf(10667,plain, % 39.80/39.87 (P9(a21,a2,a22)+P1(a11)), % 39.80/39.87 inference(scs_inference,[],[220,125])). % 39.80/39.87 cnf(10668,plain, % 39.80/39.87 (P1(a11)), % 39.80/39.87 inference(scs_inference,[],[123,52,10667,84])). % 39.80/39.87 cnf(10672,plain, % 39.80/39.87 (~P4(x106721,a11,a2)+~P3(x106722,x106721,a2)), % 39.80/39.87 inference(scs_inference,[],[10668,53,113,36,85])). % 39.80/39.87 cnf(10684,plain, % 39.80/39.87 (~P10(a1,a2,a21)+~P4(a1,a11,a2)), % 39.80/39.87 inference(scs_inference,[],[10672,161])). % 39.80/39.87 cnf(10692,plain, % 39.80/39.87 (E(a1,a21)+~P4(a1,a11,a2)), % 39.80/39.87 inference(scs_inference,[],[10684,178])). % 39.80/39.87 cnf(11445,plain, % 39.80/39.87 (P1(f9(a22,a22,a22))), % 39.80/39.87 inference(scs_inference,[],[123,52,150,101])). % 39.80/39.87 cnf(11449,plain, % 39.80/39.87 (~P4(x114491,f9(a22,a22,a22),a2)+~P3(x114492,x114491,a2)), % 39.80/39.87 inference(scs_inference,[],[11445,53,113,36,85])). % 39.80/39.87 cnf(11458,plain, % 39.80/39.87 (~P3(x114581,f6(a2,f9(a22,a22,a22)),a2)), % 39.80/39.87 inference(scs_inference,[],[11445,55,53,11449,73])). % 39.80/39.87 cnf(11464,plain, % 39.80/39.87 (~P3(x114641,x114642,a2)+~E(x114642,f6(a2,f9(a22,a22,a22)))), % 39.80/39.87 inference(scs_inference,[],[11458,33])). % 39.80/39.87 cnf(11960,plain, % 39.80/39.87 (E(a1,a21)+P1(a10)), % 39.80/39.87 inference(scs_inference,[],[159,178])). % 39.80/39.87 cnf(11964,plain, % 39.80/39.87 (E(a1,a21)+P4(f6(a2,a10),a10,a2)), % 39.80/39.87 inference(scs_inference,[],[55,53,11960,73])). % 39.80/39.87 cnf(12112,plain, % 39.80/39.87 (P9(a21,a2,a22)+P1(a10)), % 39.80/39.87 inference(scs_inference,[],[11960,125])). % 39.80/39.87 cnf(12113,plain, % 39.80/39.87 (P1(a10)), % 39.80/39.87 inference(scs_inference,[],[123,52,12112,84])). % 39.80/39.87 cnf(12117,plain, % 39.80/39.87 (~P4(x121171,a10,a2)+~P3(x121172,x121171,a2)), % 39.80/39.87 inference(scs_inference,[],[12113,53,113,36,85])). % 39.80/39.87 cnf(12319,plain, % 39.80/39.87 (~E(a1,a21)), % 39.80/39.87 inference(scs_inference,[],[123,52,125,84])). % 39.80/39.87 cnf(12320,plain, % 39.80/39.87 (P10(a1,a2,a21)), % 39.80/39.87 inference(scs_inference,[],[12319,178])). % 39.80/39.87 cnf(12321,plain, % 39.80/39.87 (P3(a10,a1,a2)), % 39.80/39.87 inference(scs_inference,[],[12319,232])). % 39.80/39.87 cnf(12322,plain, % 39.80/39.87 (P9(a22,a2,a12)), % 39.80/39.87 inference(scs_inference,[],[12319,235])). % 39.80/39.87 cnf(12341,plain, % 39.80/39.87 (~P4(a1,a11,a2)), % 39.80/39.87 inference(scs_inference,[],[12319,10692])). % 39.80/39.87 cnf(12343,plain, % 39.80/39.87 (P4(f6(a2,a10),a10,a2)), % 39.80/39.87 inference(scs_inference,[],[12319,11964])). % 39.80/39.87 cnf(12358,plain, % 39.80/39.87 (P9(a21,a2,a12)), % 39.80/39.87 inference(scs_inference,[],[12320,163])). % 39.80/39.87 cnf(12364,plain, % 39.80/39.87 (P4(a12,a11,a2)), % 39.80/39.87 inference(scs_inference,[],[12320,169])). % 39.80/39.87 cnf(12404,plain, % 39.80/39.87 ($false), % 39.80/39.87 inference(scs_inference,[],[12321,12364,10398,10668,12343,12322,12341,12358,53,10672,12117,10343,11464,2,84,44,33,74,75]), % 39.80/39.87 ['proof']). % 39.80/39.88 % SZS output end Proof % 39.80/39.88 % Total time :39.230000s %------------------------------------------------------------------------------