%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM023+1 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n018.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 241.13s 241.10s % Output : CNFRefutation 241.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.11 % Problem : COM023+1 : TPTP v8.2.0. Released v4.0.0. % 0.09/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.09/0.31 % Computer : n018.cluster.edu % 0.09/0.31 % Model : x86_64 x86_64 % 0.09/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.31 % Memory : 8042.1875MB % 0.09/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.31 % CPULimit : 300 % 0.09/0.31 % WCLimit : 300 % 0.09/0.31 % DateTime : Thu Jun 20 23:51:23 EDT 2024 % 0.09/0.31 % CPUTime : % 0.17/0.54 start to proof:theBenchmark % 241.04/241.07 %------------------------------------------- % 241.04/241.07 % File :CSE---1.7 % 241.04/241.07 % Problem :theBenchmark % 241.04/241.07 % Transform :cnf % 241.04/241.07 % Format :tptp:raw % 241.04/241.07 % Command :java -jar mcs_scs.jar %d %s % 241.04/241.07 % 241.04/241.07 % Result :Theorem 240.460000s % 241.04/241.07 % Output :CNFRefutation 240.460000s % 241.04/241.07 %------------------------------------------- % 241.13/241.09 %------------------------------------------------------------------------------ % 241.13/241.09 % File : COM023+1 : TPTP v8.2.0. Released v4.0.0. % 241.13/241.09 % Domain : Computing Theory % 241.13/241.09 % Problem : Newman's lemma on rewriting systems 03_02, 00 expansion % 241.13/241.10 % Version : Especial. % 241.13/241.10 % English : % 241.13/241.10 % 241.13/241.10 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 241.13/241.10 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 241.13/241.10 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 241.13/241.10 % Source : [Pas08] % 241.13/241.10 % Names : newman_03_02.00 [Pas08] % 241.13/241.10 % 241.13/241.10 % Status : Theorem % 241.13/241.10 % Rating : 0.17 v8.2.0, 0.19 v8.1.0, 0.08 v7.5.0, 0.12 v7.4.0, 0.17 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.1.0, 0.17 v6.0.0, 0.13 v5.5.0, 0.15 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.10 v5.1.0, 0.24 v5.0.0, 0.33 v4.1.0, 0.43 v4.0.1, 0.78 v4.0.0 % 241.13/241.10 % Syntax : Number of formulae : 18 ( 2 unt; 6 def) % 241.13/241.10 % Number of atoms : 93 ( 1 equ) % 241.13/241.10 % Maximal formula atoms : 10 ( 5 avg) % 241.13/241.10 % Number of connectives : 76 ( 1 ~; 2 |; 42 &) % 241.13/241.10 % ( 6 <=>; 25 =>; 0 <=; 0 <~>) % 241.13/241.10 % Maximal formula depth : 12 ( 7 avg) % 241.13/241.10 % Maximal term depth : 1 ( 1 avg) % 241.13/241.10 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 241.13/241.10 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 241.13/241.10 % Number of variables : 49 ( 43 !; 6 ?) % 241.13/241.10 % SPC : FOF_THM_RFO_SEQ % 241.13/241.10 % 241.13/241.10 % Comments : Problem generated by the SAD system [VLP07] % 241.13/241.10 %------------------------------------------------------------------------------ % 241.13/241.10 fof(mElmSort,axiom, % 241.13/241.10 ! [W0] : % 241.13/241.10 ( aElement0(W0) % 241.13/241.10 => $true ) ). % 241.13/241.10 % 241.13/241.10 fof(mRelSort,axiom, % 241.13/241.10 ! [W0] : % 241.13/241.10 ( aRewritingSystem0(W0) % 241.13/241.10 => $true ) ). % 241.13/241.10 % 241.13/241.10 fof(mReduct,axiom, % 241.13/241.10 ! [W0,W1] : % 241.13/241.10 ( ( aElement0(W0) % 241.13/241.10 & aRewritingSystem0(W1) ) % 241.13/241.10 => ! [W2] : % 241.13/241.10 ( aReductOfIn0(W2,W0,W1) % 241.13/241.10 => aElement0(W2) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mWFOrd,axiom, % 241.13/241.10 ! [W0,W1] : % 241.13/241.10 ( ( aElement0(W0) % 241.13/241.10 & aElement0(W1) ) % 241.13/241.10 => ( iLess0(W0,W1) % 241.13/241.10 => $true ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mTCbr,axiom, % 241.13/241.10 ! [W0,W1,W2] : % 241.13/241.10 ( ( aElement0(W0) % 241.13/241.10 & aRewritingSystem0(W1) % 241.13/241.10 & aElement0(W2) ) % 241.13/241.10 => ( sdtmndtplgtdt0(W0,W1,W2) % 241.13/241.10 => $true ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mTCDef,definition, % 241.13/241.10 ! [W0,W1,W2] : % 241.13/241.10 ( ( aElement0(W0) % 241.13/241.10 & aRewritingSystem0(W1) % 241.13/241.10 & aElement0(W2) ) % 241.13/241.10 => ( sdtmndtplgtdt0(W0,W1,W2) % 241.13/241.10 <=> ( aReductOfIn0(W2,W0,W1) % 241.13/241.10 | ? [W3] : % 241.13/241.10 ( aElement0(W3) % 241.13/241.10 & aReductOfIn0(W3,W0,W1) % 241.13/241.10 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mTCTrans,axiom, % 241.13/241.10 ! [W0,W1,W2,W3] : % 241.13/241.10 ( ( aElement0(W0) % 241.13/241.10 & aRewritingSystem0(W1) % 241.13/241.10 & aElement0(W2) % 241.13/241.10 & aElement0(W3) ) % 241.13/241.10 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 241.13/241.10 & sdtmndtplgtdt0(W2,W1,W3) ) % 241.13/241.10 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mTCRDef,definition, % 241.13/241.10 ! [W0,W1,W2] : % 241.13/241.10 ( ( aElement0(W0) % 241.13/241.10 & aRewritingSystem0(W1) % 241.13/241.10 & aElement0(W2) ) % 241.13/241.10 => ( sdtmndtasgtdt0(W0,W1,W2) % 241.13/241.10 <=> ( W0 = W2 % 241.13/241.10 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mTCRTrans,axiom, % 241.13/241.10 ! [W0,W1,W2,W3] : % 241.13/241.10 ( ( aElement0(W0) % 241.13/241.10 & aRewritingSystem0(W1) % 241.13/241.10 & aElement0(W2) % 241.13/241.10 & aElement0(W3) ) % 241.13/241.10 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 241.13/241.10 & sdtmndtasgtdt0(W2,W1,W3) ) % 241.13/241.10 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mCRDef,definition, % 241.13/241.10 ! [W0] : % 241.13/241.10 ( aRewritingSystem0(W0) % 241.13/241.10 => ( isConfluent0(W0) % 241.13/241.10 <=> ! [W1,W2,W3] : % 241.13/241.10 ( ( aElement0(W1) % 241.13/241.10 & aElement0(W2) % 241.13/241.10 & aElement0(W3) % 241.13/241.10 & sdtmndtasgtdt0(W1,W0,W2) % 241.13/241.10 & sdtmndtasgtdt0(W1,W0,W3) ) % 241.13/241.10 => ? [W4] : % 241.13/241.10 ( aElement0(W4) % 241.13/241.10 & sdtmndtasgtdt0(W2,W0,W4) % 241.13/241.10 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mWCRDef,definition, % 241.13/241.10 ! [W0] : % 241.13/241.10 ( aRewritingSystem0(W0) % 241.13/241.10 => ( isLocallyConfluent0(W0) % 241.13/241.10 <=> ! [W1,W2,W3] : % 241.13/241.10 ( ( aElement0(W1) % 241.13/241.10 & aElement0(W2) % 241.13/241.10 & aElement0(W3) % 241.13/241.10 & aReductOfIn0(W2,W1,W0) % 241.13/241.10 & aReductOfIn0(W3,W1,W0) ) % 241.13/241.10 => ? [W4] : % 241.13/241.10 ( aElement0(W4) % 241.13/241.10 & sdtmndtasgtdt0(W2,W0,W4) % 241.13/241.10 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mTermin,definition, % 241.13/241.10 ! [W0] : % 241.13/241.10 ( aRewritingSystem0(W0) % 241.13/241.10 => ( isTerminating0(W0) % 241.13/241.10 <=> ! [W1,W2] : % 241.13/241.10 ( ( aElement0(W1) % 241.13/241.10 & aElement0(W2) ) % 241.13/241.10 => ( sdtmndtplgtdt0(W1,W0,W2) % 241.13/241.10 => iLess0(W2,W1) ) ) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mNFRDef,definition, % 241.13/241.10 ! [W0,W1] : % 241.13/241.10 ( ( aElement0(W0) % 241.13/241.10 & aRewritingSystem0(W1) ) % 241.13/241.10 => ! [W2] : % 241.13/241.10 ( aNormalFormOfIn0(W2,W0,W1) % 241.13/241.10 <=> ( aElement0(W2) % 241.13/241.10 & sdtmndtasgtdt0(W0,W1,W2) % 241.13/241.10 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(mTermNF,axiom, % 241.13/241.10 ! [W0] : % 241.13/241.10 ( ( aRewritingSystem0(W0) % 241.13/241.10 & isTerminating0(W0) ) % 241.13/241.10 => ! [W1] : % 241.13/241.10 ( aElement0(W1) % 241.13/241.10 => ? [W2] : aNormalFormOfIn0(W2,W1,W0) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(m__656,hypothesis, % 241.13/241.10 aRewritingSystem0(xR) ). % 241.13/241.10 % 241.13/241.10 fof(m__656_01,hypothesis, % 241.13/241.10 ( isLocallyConfluent0(xR) % 241.13/241.10 & isTerminating0(xR) ) ). % 241.13/241.10 % 241.13/241.10 fof(m__715,hypothesis, % 241.13/241.10 ! [W0,W1,W2] : % 241.13/241.10 ( ( aElement0(W0) % 241.13/241.10 & aElement0(W1) % 241.13/241.10 & aElement0(W2) % 241.13/241.10 & sdtmndtasgtdt0(W0,xR,W1) % 241.13/241.10 & sdtmndtasgtdt0(W0,xR,W2) ) % 241.13/241.10 => ? [W3] : % 241.13/241.10 ( aElement0(W3) % 241.13/241.10 & sdtmndtasgtdt0(W1,xR,W3) % 241.13/241.10 & sdtmndtasgtdt0(W2,xR,W3) ) ) ). % 241.13/241.10 % 241.13/241.10 fof(m__,conjecture, % 241.13/241.10 isConfluent0(xR) ). % 241.13/241.10 % 241.13/241.10 %------------------------------------------------------------------------------ % 241.13/241.10 %------------------------------------------- % 241.13/241.10 % Proof found % 241.13/241.10 % SZS status Theorem for theBenchmark % 241.13/241.10 % SZS output start Proof % 241.13/241.10 %ClaNum:95(EqnAxiom:49) % 241.13/241.10 %VarNum:375(SingletonVarNum:105) % 241.13/241.10 %MaxLitNum:8 % 241.13/241.10 %MaxfuncDepth:1 % 241.13/241.10 %SharedTerms:5 % 241.13/241.10 %goalClause: 53 % 241.13/241.10 %singleGoalClaCount:1 % 241.13/241.10 [50]P1(a1) % 241.13/241.10 [51]P5(a1) % 241.13/241.10 [52]P8(a1) % 241.13/241.10 [53]~P6(a1) % 241.13/241.10 [54]~P1(x541)+P6(x541)+P2(f2(x541)) % 241.13/241.10 [55]~P1(x551)+P6(x551)+P2(f10(x551)) % 241.13/241.10 [56]~P1(x561)+P6(x561)+P2(f11(x561)) % 241.13/241.10 [57]~P1(x571)+P5(x571)+P2(f12(x571)) % 241.13/241.10 [58]~P1(x581)+P5(x581)+P2(f14(x581)) % 241.13/241.10 [59]~P1(x591)+P5(x591)+P2(f15(x591)) % 241.13/241.10 [60]~P1(x601)+P8(x601)+P2(f3(x601)) % 241.13/241.10 [61]~P1(x611)+P8(x611)+P2(f4(x611)) % 241.13/241.10 [62]~P1(x621)+P8(x621)+~P7(f4(x621),f3(x621)) % 241.13/241.10 [63]~P1(x631)+P6(x631)+P9(f2(x631),x631,f10(x631)) % 241.13/241.10 [64]~P1(x641)+P6(x641)+P9(f2(x641),x641,f11(x641)) % 241.13/241.10 [65]~P1(x651)+P8(x651)+P10(f3(x651),x651,f4(x651)) % 241.13/241.10 [66]~P1(x661)+P5(x661)+P3(f14(x661),f12(x661),x661) % 241.13/241.10 [67]~P1(x671)+P5(x671)+P3(f15(x671),f12(x671),x671) % 241.13/241.10 [69]~P2(x692)+~P1(x691)+~P8(x691)+P4(f5(x691,x692),x692,x691) % 241.13/241.10 [70]~P3(x701,x702,x703)+P2(x701)+~P2(x702)+~P1(x703) % 241.13/241.10 [71]~P4(x711,x712,x713)+P2(x711)+~P2(x712)+~P1(x713) % 241.13/241.10 [73]~P2(x731)+~P1(x732)+~P4(x733,x731,x732)+P9(x731,x732,x733) % 241.13/241.10 [77]~P4(x774,x771,x772)+~P2(x771)+~P3(x773,x774,x772)+~P1(x772) % 241.13/241.10 [78]~P1(x781)+P6(x781)+~P2(x782)+~P9(f10(x781),x781,x782)+~P9(f11(x781),x781,x782) % 241.13/241.10 [79]~P1(x791)+P5(x791)+~P2(x792)+~P9(f14(x791),x791,x792)+~P9(f15(x791),x791,x792) % 241.13/241.10 [68]~E(x681,x683)+~P2(x683)+~P2(x681)+~P1(x682)+P9(x681,x682,x683) % 241.13/241.10 [74]~P2(x741)+~P2(x743)+~P1(x742)+~P3(x743,x741,x742)+P10(x741,x742,x743) % 241.13/241.10 [75]~P2(x753)+~P2(x751)+~P1(x752)+~P10(x751,x752,x753)+P9(x751,x752,x753) % 241.16/241.10 [72]~P2(x721)+~P2(x722)+~P8(x723)+~P10(x722,x723,x721)+P7(x721,x722)+~P1(x723) % 241.16/241.10 [76]~P2(x762)+~P2(x761)+~P1(x763)+~P9(x761,x763,x762)+E(x761,x762)+P10(x761,x763,x762) % 241.16/241.10 [83]~P2(x831)+~P2(x832)+~P1(x833)+~P10(x832,x833,x831)+P3(x831,x832,x833)+P2(f7(x832,x833,x831)) % 241.16/241.10 [84]~P2(x843)+~P2(x842)+~P2(x841)+~P9(x841,a1,x843)+~P9(x841,a1,x842)+P2(f8(x841,x842,x843)) % 241.16/241.10 [85]~P2(x851)+~P2(x852)+~P1(x853)+~P10(x852,x853,x851)+P3(x851,x852,x853)+P3(f7(x852,x853,x851),x852,x853) % 241.16/241.10 [86]~P2(x861)+~P2(x862)+~P1(x863)+~P10(x862,x863,x861)+P3(x861,x862,x863)+P10(f7(x862,x863,x861),x863,x861) % 241.16/241.10 [87]~P2(x872)+~P2(x871)+~P1(x873)+~P9(x872,x873,x871)+P4(x871,x872,x873)+P3(f6(x872,x873,x871),x871,x873) % 241.16/241.10 [88]~P2(x883)+~P2(x882)+~P2(x881)+~P9(x882,a1,x883)+~P9(x882,a1,x881)+P9(x881,a1,f8(x882,x883,x881)) % 241.16/241.10 [89]~P2(x893)+~P2(x892)+~P2(x891)+~P9(x892,a1,x893)+~P9(x892,a1,x891)+P9(x891,a1,f8(x892,x891,x893)) % 241.16/241.10 [80]~P2(x803)+~P2(x801)+~P1(x802)+~P3(x804,x801,x802)+~P10(x804,x802,x803)+P10(x801,x802,x803)+~P2(x804) % 241.16/241.10 [81]~P2(x813)+~P2(x811)+~P1(x812)+~P10(x814,x812,x813)+~P10(x811,x812,x814)+P10(x811,x812,x813)+~P2(x814) % 241.16/241.10 [82]~P2(x823)+~P2(x821)+~P1(x822)+~P9(x824,x822,x823)+~P9(x821,x822,x824)+P9(x821,x822,x823)+~P2(x824) % 241.16/241.10 [90]~P2(x904)+~P2(x903)+~P2(x902)+~P1(x901)+~P6(x901)+~P9(x902,x901,x904)+~P9(x902,x901,x903)+P2(f9(x901,x902,x903,x904)) % 241.16/241.10 [91]~P2(x914)+~P2(x913)+~P2(x912)+~P1(x911)+~P5(x911)+~P3(x914,x912,x911)+~P3(x913,x912,x911)+P2(f13(x911,x912,x913,x914)) % 241.16/241.11 [92]~P2(x924)+~P2(x923)+~P2(x921)+~P1(x922)+~P6(x922)+~P9(x923,x922,x924)+~P9(x923,x922,x921)+P9(x921,x922,f9(x922,x923,x924,x921)) % 241.16/241.11 [93]~P2(x934)+~P2(x933)+~P2(x931)+~P1(x932)+~P6(x932)+~P9(x933,x932,x934)+~P9(x933,x932,x931)+P9(x931,x932,f9(x932,x933,x931,x934)) % 241.16/241.11 [94]~P2(x944)+~P2(x943)+~P2(x941)+~P1(x942)+~P5(x942)+~P3(x944,x943,x942)+~P3(x941,x943,x942)+P9(x941,x942,f13(x942,x943,x944,x941)) % 241.16/241.11 [95]~P2(x954)+~P2(x953)+~P2(x951)+~P1(x952)+~P5(x952)+~P3(x954,x953,x952)+~P3(x951,x953,x952)+P9(x951,x952,f13(x952,x953,x951,x954)) % 241.16/241.11 %EqnAxiom % 241.16/241.11 [1]E(x11,x11) % 241.16/241.11 [2]E(x22,x21)+~E(x21,x22) % 241.16/241.11 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 241.16/241.11 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 241.16/241.11 [5]~E(x51,x52)+E(f10(x51),f10(x52)) % 241.16/241.11 [6]~E(x61,x62)+E(f11(x61),f11(x62)) % 241.16/241.11 [7]~E(x71,x72)+E(f12(x71),f12(x72)) % 241.16/241.11 [8]~E(x81,x82)+E(f14(x81),f14(x82)) % 241.16/241.11 [9]~E(x91,x92)+E(f15(x91),f15(x92)) % 241.16/241.11 [10]~E(x101,x102)+E(f3(x101),f3(x102)) % 241.16/241.11 [11]~E(x111,x112)+E(f4(x111),f4(x112)) % 241.16/241.11 [12]~E(x121,x122)+E(f7(x121,x123,x124),f7(x122,x123,x124)) % 241.16/241.11 [13]~E(x131,x132)+E(f7(x133,x131,x134),f7(x133,x132,x134)) % 241.16/241.11 [14]~E(x141,x142)+E(f7(x143,x144,x141),f7(x143,x144,x142)) % 241.16/241.11 [15]~E(x151,x152)+E(f9(x151,x153,x154,x155),f9(x152,x153,x154,x155)) % 241.16/241.11 [16]~E(x161,x162)+E(f9(x163,x161,x164,x165),f9(x163,x162,x164,x165)) % 241.16/241.11 [17]~E(x171,x172)+E(f9(x173,x174,x171,x175),f9(x173,x174,x172,x175)) % 241.16/241.11 [18]~E(x181,x182)+E(f9(x183,x184,x185,x181),f9(x183,x184,x185,x182)) % 241.16/241.11 [19]~E(x191,x192)+E(f13(x191,x193,x194,x195),f13(x192,x193,x194,x195)) % 241.16/241.11 [20]~E(x201,x202)+E(f13(x203,x201,x204,x205),f13(x203,x202,x204,x205)) % 241.16/241.11 [21]~E(x211,x212)+E(f13(x213,x214,x211,x215),f13(x213,x214,x212,x215)) % 241.16/241.11 [22]~E(x221,x222)+E(f13(x223,x224,x225,x221),f13(x223,x224,x225,x222)) % 241.16/241.11 [23]~E(x231,x232)+E(f8(x231,x233,x234),f8(x232,x233,x234)) % 241.16/241.11 [24]~E(x241,x242)+E(f8(x243,x241,x244),f8(x243,x242,x244)) % 241.16/241.11 [25]~E(x251,x252)+E(f8(x253,x254,x251),f8(x253,x254,x252)) % 241.16/241.11 [26]~E(x261,x262)+E(f5(x261,x263),f5(x262,x263)) % 241.16/241.11 [27]~E(x271,x272)+E(f5(x273,x271),f5(x273,x272)) % 241.16/241.11 [28]~E(x281,x282)+E(f6(x281,x283,x284),f6(x282,x283,x284)) % 241.16/241.11 [29]~E(x291,x292)+E(f6(x293,x291,x294),f6(x293,x292,x294)) % 241.16/241.11 [30]~E(x301,x302)+E(f6(x303,x304,x301),f6(x303,x304,x302)) % 241.16/241.11 [31]~P1(x311)+P1(x312)+~E(x311,x312) % 241.16/241.11 [32]~P5(x321)+P5(x322)+~E(x321,x322) % 241.16/241.11 [33]~P8(x331)+P8(x332)+~E(x331,x332) % 241.16/241.11 [34]~P6(x341)+P6(x342)+~E(x341,x342) % 241.16/241.11 [35]P9(x352,x353,x354)+~E(x351,x352)+~P9(x351,x353,x354) % 241.16/241.11 [36]P9(x363,x362,x364)+~E(x361,x362)+~P9(x363,x361,x364) % 241.16/241.11 [37]P9(x373,x374,x372)+~E(x371,x372)+~P9(x373,x374,x371) % 241.16/241.11 [38]~P2(x381)+P2(x382)+~E(x381,x382) % 241.16/241.11 [39]P3(x392,x393,x394)+~E(x391,x392)+~P3(x391,x393,x394) % 241.16/241.11 [40]P3(x403,x402,x404)+~E(x401,x402)+~P3(x403,x401,x404) % 241.16/241.11 [41]P3(x413,x414,x412)+~E(x411,x412)+~P3(x413,x414,x411) % 241.16/241.11 [42]P10(x422,x423,x424)+~E(x421,x422)+~P10(x421,x423,x424) % 241.16/241.11 [43]P10(x433,x432,x434)+~E(x431,x432)+~P10(x433,x431,x434) % 241.16/241.11 [44]P10(x443,x444,x442)+~E(x441,x442)+~P10(x443,x444,x441) % 241.16/241.11 [45]P4(x452,x453,x454)+~E(x451,x452)+~P4(x451,x453,x454) % 241.16/241.11 [46]P4(x463,x462,x464)+~E(x461,x462)+~P4(x463,x461,x464) % 241.16/241.11 [47]P4(x473,x474,x472)+~E(x471,x472)+~P4(x473,x474,x471) % 241.16/241.11 [48]P7(x482,x483)+~E(x481,x482)+~P7(x481,x483) % 241.16/241.11 [49]P7(x493,x492)+~E(x491,x492)+~P7(x493,x491) % 241.16/241.11 % 241.16/241.11 %------------------------------------------- % 241.19/241.12 cnf(96,plain, % 241.19/241.12 (~P2(x961)+~P2(x961)+P9(x961,x962,x961)+~P1(x962)), % 241.19/241.12 inference(equality_inference,[],[68])). % 241.19/241.12 cnf(97,plain, % 241.19/241.12 (P9(x971,a1,x971)+~P2(x971)), % 241.19/241.12 inference(scs_inference,[],[50,96])). % 241.19/241.12 cnf(141,plain, % 241.19/241.12 (~E(x1411,a1)+P1(x1411)), % 241.19/241.12 inference(scs_inference,[],[50,31,2])). % 241.19/241.12 cnf(147,plain, % 241.19/241.12 (~E(a1,x1471)+~P6(x1471)), % 241.19/241.12 inference(scs_inference,[],[53,34,2])). % 241.19/241.12 cnf(150,plain, % 241.19/241.12 (P2(f10(a1))), % 241.19/241.12 inference(scs_inference,[],[50,55,147])). % 241.19/241.12 cnf(154,plain, % 241.19/241.12 (P9(f10(a1),a1,f10(a1))), % 241.19/241.12 inference(scs_inference,[],[50,150,96])). % 241.19/241.12 cnf(243,plain, % 241.19/241.12 (P2(f11(a1))), % 241.19/241.12 inference(scs_inference,[],[50,56,147])). % 241.19/241.12 cnf(250,plain, % 241.19/241.12 (P9(f11(a1),a1,f11(a1))), % 241.19/241.12 inference(scs_inference,[],[50,243,68])). % 241.19/241.12 cnf(550,plain, % 241.19/241.12 (P9(f2(a1),a1,f10(a1))), % 241.19/241.12 inference(scs_inference,[],[50,63,147])). % 241.19/241.12 cnf(572,plain, % 241.19/241.12 (P9(f2(a1),a1,f11(a1))), % 241.19/241.12 inference(scs_inference,[],[50,64,147])). % 241.19/241.12 cnf(1095,plain, % 241.19/241.12 (P9(f10(a1),a1,f8(f10(a1),f10(a1),f10(a1)))), % 241.19/241.12 inference(scs_inference,[],[154,53,50,88,55])). % 241.19/241.12 cnf(1246,plain, % 241.19/241.12 (P2(f2(a1))), % 241.19/241.12 inference(scs_inference,[],[53,141,54])). % 241.19/241.12 cnf(1278,plain, % 241.19/241.12 (P9(f10(a1),a1,f11(a1))+~P2(f8(f10(a1),f10(a1),f10(a1)))+~P9(f8(f10(a1),f10(a1),f10(a1)),a1,f11(a1))), % 241.19/241.12 inference(scs_inference,[],[243,150,50,1095,82])). % 241.19/241.12 cnf(1753,plain, % 241.19/241.12 (~P9(f8(f10(a1),f10(a1),f10(a1)),a1,f11(a1))+~P2(f8(f10(a1),f10(a1),f10(a1)))), % 241.19/241.12 inference(scs_inference,[],[250,53,50,243,1278,78])). % 241.19/241.12 cnf(2533,plain, % 241.19/241.12 (E(f10(x25331),f10(x25332))+~E(x25332,x25331)), % 241.19/241.12 inference(scs_inference,[],[2,5])). % 241.19/241.12 cnf(3823,plain, % 241.19/241.12 (~E(x38231,f10(a1))+P2(x38231)), % 241.19/241.12 inference(scs_inference,[],[150,2,38])). % 241.19/241.12 cnf(7747,plain, % 241.19/241.12 (P2(f8(f10(a1),f10(a1),f10(a1)))), % 241.19/241.12 inference(scs_inference,[],[150,97,84])). % 241.19/241.12 cnf(7954,plain, % 241.19/241.12 (P2(f10(x79541))+~E(a1,x79541)), % 241.19/241.12 inference(scs_inference,[],[3823,2533])). % 241.19/241.12 cnf(8056,plain, % 241.19/241.12 (P9(f11(a1),a1,f8(f2(a1),f10(a1),f11(a1)))), % 241.19/241.12 inference(scs_inference,[],[572,550,1246,243,7954,88])). % 241.19/241.12 cnf(8058,plain, % 241.19/241.12 (P2(f8(f2(a1),f10(a1),f11(a1)))), % 241.19/241.12 inference(scs_inference,[],[572,243,1246,550,7954,84])). % 241.19/241.12 cnf(9550,plain, % 241.19/241.12 (~P9(f8(f10(a1),f10(a1),f10(a1)),a1,f11(a1))), % 241.19/241.12 inference(scs_inference,[],[7747,1753])). % 241.19/241.12 cnf(12100,plain, % 241.19/241.12 (~P9(f10(a1),a1,f8(f2(a1),f10(a1),f11(a1)))), % 241.19/241.12 inference(scs_inference,[],[53,50,8058,8056,78])). % 241.19/241.12 cnf(13520,plain, % 241.19/241.12 ($false), % 241.19/241.12 inference(scs_inference,[],[9550,12100,7747,572,550,243,1246,50,150,75,89]), % 241.19/241.12 ['proof']). % 241.19/241.14 % SZS output end Proof % 241.19/241.14 % Total time :240.460000s %------------------------------------------------------------------------------