%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM013+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 : n020.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:44 EDT 2024 % Result : Theorem 116.37s 116.37s % Output : CNFRefutation 116.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : COM013+1 : TPTP v8.2.0. Released v4.0.0. % 0.10/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.31 % Computer : n020.cluster.edu % 0.13/0.31 % Model : x86_64 x86_64 % 0.13/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.31 % Memory : 8042.1875MB % 0.13/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.31 % CPULimit : 300 % 0.13/0.31 % WCLimit : 300 % 0.13/0.31 % DateTime : Thu Jun 20 23:21:09 EDT 2024 % 0.13/0.31 % CPUTime : % 0.18/0.56 start to proof:theBenchmark % 116.37/116.36 %------------------------------------------- % 116.37/116.36 % File :CSE---1.7 % 116.37/116.36 % Problem :theBenchmark % 116.37/116.36 % Transform :cnf % 116.37/116.36 % Format :tptp:raw % 116.37/116.36 % Command :java -jar mcs_scs.jar %d %s % 116.37/116.36 % 116.37/116.36 % Result :Theorem 115.760000s % 116.37/116.36 % Output :CNFRefutation 115.760000s % 116.37/116.36 %------------------------------------------- % 116.37/116.37 %------------------------------------------------------------------------------ % 116.37/116.37 % File : COM013+1 : TPTP v8.2.0. Released v4.0.0. % 116.37/116.37 % Domain : Computing Theory % 116.37/116.37 % Problem : Newman's lemma on rewriting systems 02, 00 expansion % 116.37/116.37 % Version : Especial. % 116.37/116.37 % English : % 116.37/116.37 % 116.37/116.37 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 116.37/116.37 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 116.37/116.37 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 116.37/116.37 % Source : [Pas08] % 116.37/116.37 % Names : newman_02.00 [Pas08] % 116.37/116.37 % 116.37/116.37 % Status : Theorem % 116.37/116.37 % Rating : 0.33 v8.2.0, 0.31 v8.1.0, 0.25 v7.5.0, 0.31 v7.4.0, 0.27 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.12 v6.2.0, 0.28 v6.1.0, 0.37 v6.0.0, 0.35 v5.5.0, 0.37 v5.4.0, 0.39 v5.3.0, 0.37 v5.2.0, 0.15 v5.1.0, 0.24 v5.0.0, 0.38 v4.1.0, 0.48 v4.0.1, 0.61 v4.0.0 % 116.37/116.37 % Syntax : Number of formulae : 15 ( 0 unt; 6 def) % 116.37/116.37 % Number of atoms : 84 ( 1 equ) % 116.37/116.37 % Maximal formula atoms : 10 ( 5 avg) % 116.37/116.37 % Number of connectives : 70 ( 1 ~; 2 |; 35 &) % 116.37/116.37 % ( 6 <=>; 26 =>; 0 <=; 0 <~>) % 116.37/116.37 % Maximal formula depth : 12 ( 7 avg) % 116.37/116.37 % Maximal term depth : 1 ( 1 avg) % 116.37/116.37 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 116.37/116.37 % Number of functors : 1 ( 1 usr; 1 con; 0-0 aty) % 116.37/116.37 % Number of variables : 46 ( 40 !; 6 ?) % 116.37/116.37 % SPC : FOF_THM_RFO_SEQ % 116.37/116.37 % 116.37/116.37 % Comments : Problem generated by the SAD system [VLP07] % 116.37/116.37 %------------------------------------------------------------------------------ % 116.37/116.37 fof(mElmSort,axiom, % 116.37/116.37 ! [W0] : % 116.37/116.37 ( aElement0(W0) % 116.37/116.37 => $true ) ). % 116.37/116.37 % 116.37/116.37 fof(mRelSort,axiom, % 116.37/116.37 ! [W0] : % 116.37/116.37 ( aRewritingSystem0(W0) % 116.37/116.37 => $true ) ). % 116.37/116.37 % 116.37/116.37 fof(mReduct,axiom, % 116.37/116.37 ! [W0,W1] : % 116.37/116.37 ( ( aElement0(W0) % 116.37/116.37 & aRewritingSystem0(W1) ) % 116.37/116.37 => ! [W2] : % 116.37/116.37 ( aReductOfIn0(W2,W0,W1) % 116.37/116.37 => aElement0(W2) ) ) ). % 116.37/116.37 % 116.37/116.37 fof(mWFOrd,axiom, % 116.37/116.37 ! [W0,W1] : % 116.37/116.37 ( ( aElement0(W0) % 116.37/116.37 & aElement0(W1) ) % 116.37/116.37 => ( iLess0(W0,W1) % 116.37/116.37 => $true ) ) ). % 116.37/116.37 % 116.37/116.37 fof(mTCbr,axiom, % 116.37/116.37 ! [W0,W1,W2] : % 116.37/116.37 ( ( aElement0(W0) % 116.37/116.37 & aRewritingSystem0(W1) % 116.37/116.37 & aElement0(W2) ) % 116.37/116.37 => ( sdtmndtplgtdt0(W0,W1,W2) % 116.37/116.37 => $true ) ) ). % 116.37/116.37 % 116.37/116.37 fof(mTCDef,definition, % 116.37/116.37 ! [W0,W1,W2] : % 116.37/116.37 ( ( aElement0(W0) % 116.37/116.37 & aRewritingSystem0(W1) % 116.37/116.37 & aElement0(W2) ) % 116.37/116.37 => ( sdtmndtplgtdt0(W0,W1,W2) % 116.37/116.37 <=> ( aReductOfIn0(W2,W0,W1) % 116.37/116.37 | ? [W3] : % 116.37/116.37 ( aElement0(W3) % 116.37/116.37 & aReductOfIn0(W3,W0,W1) % 116.37/116.37 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 116.37/116.37 % 116.37/116.37 fof(mTCTrans,axiom, % 116.37/116.37 ! [W0,W1,W2,W3] : % 116.37/116.37 ( ( aElement0(W0) % 116.37/116.37 & aRewritingSystem0(W1) % 116.37/116.37 & aElement0(W2) % 116.37/116.37 & aElement0(W3) ) % 116.37/116.37 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 116.37/116.37 & sdtmndtplgtdt0(W2,W1,W3) ) % 116.37/116.37 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 116.37/116.37 % 116.37/116.37 fof(mTCRDef,definition, % 116.37/116.37 ! [W0,W1,W2] : % 116.37/116.37 ( ( aElement0(W0) % 116.37/116.37 & aRewritingSystem0(W1) % 116.37/116.37 & aElement0(W2) ) % 116.37/116.37 => ( sdtmndtasgtdt0(W0,W1,W2) % 116.37/116.37 <=> ( W0 = W2 % 116.37/116.37 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 116.37/116.37 % 116.37/116.37 fof(mTCRTrans,axiom, % 116.37/116.37 ! [W0,W1,W2,W3] : % 116.37/116.37 ( ( aElement0(W0) % 116.37/116.37 & aRewritingSystem0(W1) % 116.37/116.37 & aElement0(W2) % 116.37/116.37 & aElement0(W3) ) % 116.37/116.37 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 116.37/116.37 & sdtmndtasgtdt0(W2,W1,W3) ) % 116.37/116.37 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 116.37/116.37 % 116.37/116.37 fof(mCRDef,definition, % 116.37/116.37 ! [W0] : % 116.37/116.37 ( aRewritingSystem0(W0) % 116.37/116.37 => ( isConfluent0(W0) % 116.37/116.37 <=> ! [W1,W2,W3] : % 116.37/116.37 ( ( aElement0(W1) % 116.37/116.37 & aElement0(W2) % 116.37/116.37 & aElement0(W3) % 116.37/116.37 & sdtmndtasgtdt0(W1,W0,W2) % 116.37/116.37 & sdtmndtasgtdt0(W1,W0,W3) ) % 116.37/116.37 => ? [W4] : % 116.37/116.37 ( aElement0(W4) % 116.37/116.37 & sdtmndtasgtdt0(W2,W0,W4) % 116.37/116.37 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 116.37/116.37 % 116.37/116.37 fof(mWCRDef,definition, % 116.37/116.37 ! [W0] : % 116.37/116.37 ( aRewritingSystem0(W0) % 116.37/116.37 => ( isLocallyConfluent0(W0) % 116.37/116.37 <=> ! [W1,W2,W3] : % 116.37/116.37 ( ( aElement0(W1) % 116.37/116.37 & aElement0(W2) % 116.37/116.37 & aElement0(W3) % 116.37/116.37 & aReductOfIn0(W2,W1,W0) % 116.37/116.37 & aReductOfIn0(W3,W1,W0) ) % 116.37/116.37 => ? [W4] : % 116.37/116.37 ( aElement0(W4) % 116.37/116.37 & sdtmndtasgtdt0(W2,W0,W4) % 116.37/116.37 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 116.37/116.37 % 116.37/116.37 fof(mTermin,definition, % 116.37/116.37 ! [W0] : % 116.37/116.37 ( aRewritingSystem0(W0) % 116.37/116.37 => ( isTerminating0(W0) % 116.37/116.37 <=> ! [W1,W2] : % 116.37/116.37 ( ( aElement0(W1) % 116.37/116.37 & aElement0(W2) ) % 116.37/116.37 => ( sdtmndtplgtdt0(W1,W0,W2) % 116.37/116.37 => iLess0(W2,W1) ) ) ) ) ). % 116.37/116.37 % 116.37/116.37 fof(mNFRDef,definition, % 116.37/116.37 ! [W0,W1] : % 116.37/116.37 ( ( aElement0(W0) % 116.37/116.37 & aRewritingSystem0(W1) ) % 116.37/116.37 => ! [W2] : % 116.37/116.37 ( aNormalFormOfIn0(W2,W0,W1) % 116.37/116.37 <=> ( aElement0(W2) % 116.37/116.37 & sdtmndtasgtdt0(W0,W1,W2) % 116.37/116.37 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 116.37/116.37 % 116.37/116.37 fof(m__587,hypothesis, % 116.37/116.37 ( aRewritingSystem0(xR) % 116.37/116.37 & isTerminating0(xR) ) ). % 116.37/116.37 % 116.37/116.37 fof(m__,conjecture, % 116.37/116.37 ! [W0] : % 116.37/116.37 ( aElement0(W0) % 116.37/116.37 => ( ! [W1] : % 116.37/116.37 ( aElement0(W1) % 116.37/116.37 => ( iLess0(W1,W0) % 116.37/116.37 => ? [W2] : aNormalFormOfIn0(W2,W1,xR) ) ) % 116.37/116.37 => ? [W1] : aNormalFormOfIn0(W1,W0,xR) ) ) ). % 116.37/116.37 % 116.37/116.37 %------------------------------------------------------------------------------ % 116.37/116.37 %------------------------------------------- % 116.37/116.37 % Proof found % 116.37/116.37 % SZS status Theorem for theBenchmark % 116.37/116.37 % SZS output start Proof % 116.37/116.37 %ClaNum:88(EqnAxiom:45) % 116.37/116.37 %VarNum:341(SingletonVarNum:96) % 116.37/116.37 %MaxLitNum:8 % 116.37/116.37 %MaxfuncDepth:1 % 116.37/116.37 %SharedTerms:5 % 116.37/116.37 %goalClause: 46 49 65 % 116.37/116.37 %singleGoalClaCount:2 % 116.37/116.37 [46]P1(a1) % 116.37/116.37 [47]P2(a5) % 116.37/116.37 [48]P5(a5) % 116.37/116.37 [49]~P3(x491,a1,a5) % 116.37/116.37 [50]~P2(x501)+P6(x501)+P1(f6(x501)) % 116.37/116.37 [51]~P2(x511)+P6(x511)+P1(f10(x511)) % 116.37/116.37 [52]~P2(x521)+P6(x521)+P1(f11(x521)) % 116.37/116.37 [53]~P2(x531)+P8(x531)+P1(f12(x531)) % 116.37/116.37 [54]~P2(x541)+P8(x541)+P1(f14(x541)) % 116.37/116.38 [55]~P2(x551)+P8(x551)+P1(f15(x551)) % 116.37/116.38 [56]~P2(x561)+P5(x561)+P1(f2(x561)) % 116.37/116.38 [57]~P2(x571)+P5(x571)+P1(f3(x571)) % 116.37/116.38 [58]~P2(x581)+P5(x581)+~P7(f3(x581),f2(x581)) % 116.37/116.38 [59]~P2(x591)+P6(x591)+P9(f6(x591),x591,f10(x591)) % 116.37/116.38 [60]~P2(x601)+P6(x601)+P9(f6(x601),x601,f11(x601)) % 116.37/116.38 [61]~P2(x611)+P5(x611)+P10(f2(x611),x611,f3(x611)) % 116.37/116.38 [62]~P2(x621)+P8(x621)+P4(f14(x621),f12(x621),x621) % 116.37/116.38 [63]~P2(x631)+P8(x631)+P4(f15(x631),f12(x631),x631) % 116.37/116.38 [65]~P1(x651)+~P7(x651,a1)+P3(f7(x651),x651,a5) % 116.37/116.38 [66]~P4(x661,x662,x663)+P1(x661)+~P1(x662)+~P2(x663) % 116.37/116.38 [67]~P3(x671,x672,x673)+P1(x671)+~P1(x672)+~P2(x673) % 116.37/116.38 [69]~P1(x691)+~P2(x692)+~P3(x693,x691,x692)+P9(x691,x692,x693) % 116.37/116.38 [73]~P3(x734,x731,x732)+~P1(x731)+~P4(x733,x734,x732)+~P2(x732) % 116.37/116.38 [74]~P2(x741)+P6(x741)+~P1(x742)+~P9(f10(x741),x741,x742)+~P9(f11(x741),x741,x742) % 116.37/116.38 [75]~P2(x751)+P8(x751)+~P1(x752)+~P9(f14(x751),x751,x752)+~P9(f15(x751),x751,x752) % 116.37/116.38 [64]~E(x641,x643)+~P1(x643)+~P1(x641)+~P2(x642)+P9(x641,x642,x643) % 116.37/116.38 [70]~P1(x701)+~P1(x703)+~P2(x702)+~P4(x703,x701,x702)+P10(x701,x702,x703) % 116.37/116.38 [71]~P1(x713)+~P1(x711)+~P2(x712)+~P10(x711,x712,x713)+P9(x711,x712,x713) % 116.37/116.38 [68]~P1(x681)+~P1(x682)+~P5(x683)+~P10(x682,x683,x681)+P7(x681,x682)+~P2(x683) % 116.37/116.38 [72]~P1(x722)+~P1(x721)+~P2(x723)+~P9(x721,x723,x722)+E(x721,x722)+P10(x721,x723,x722) % 116.37/116.38 [79]~P1(x791)+~P1(x792)+~P2(x793)+~P10(x792,x793,x791)+P4(x791,x792,x793)+P1(f8(x792,x793,x791)) % 116.37/116.38 [80]~P1(x801)+~P1(x802)+~P2(x803)+~P10(x802,x803,x801)+P4(x801,x802,x803)+P4(f8(x802,x803,x801),x802,x803) % 116.37/116.38 [81]~P1(x811)+~P1(x812)+~P2(x813)+~P10(x812,x813,x811)+P4(x811,x812,x813)+P10(f8(x812,x813,x811),x813,x811) % 116.37/116.38 [82]~P1(x822)+~P1(x821)+~P2(x823)+~P9(x822,x823,x821)+P3(x821,x822,x823)+P4(f4(x822,x823,x821),x821,x823) % 116.37/116.38 [76]~P1(x763)+~P1(x761)+~P2(x762)+~P4(x764,x761,x762)+~P10(x764,x762,x763)+P10(x761,x762,x763)+~P1(x764) % 116.37/116.38 [77]~P1(x773)+~P1(x771)+~P2(x772)+~P10(x774,x772,x773)+~P10(x771,x772,x774)+P10(x771,x772,x773)+~P1(x774) % 116.37/116.38 [78]~P1(x783)+~P1(x781)+~P2(x782)+~P9(x784,x782,x783)+~P9(x781,x782,x784)+P9(x781,x782,x783)+~P1(x784) % 116.37/116.38 [83]~P1(x834)+~P1(x833)+~P1(x832)+~P2(x831)+~P6(x831)+~P9(x832,x831,x834)+~P9(x832,x831,x833)+P1(f9(x831,x832,x833,x834)) % 116.37/116.38 [84]~P1(x844)+~P1(x843)+~P1(x842)+~P2(x841)+~P8(x841)+~P4(x844,x842,x841)+~P4(x843,x842,x841)+P1(f13(x841,x842,x843,x844)) % 116.37/116.38 [85]~P1(x854)+~P1(x853)+~P1(x851)+~P2(x852)+~P6(x852)+~P9(x853,x852,x854)+~P9(x853,x852,x851)+P9(x851,x852,f9(x852,x853,x854,x851)) % 116.37/116.38 [86]~P1(x864)+~P1(x863)+~P1(x861)+~P2(x862)+~P6(x862)+~P9(x863,x862,x864)+~P9(x863,x862,x861)+P9(x861,x862,f9(x862,x863,x861,x864)) % 116.37/116.38 [87]~P1(x874)+~P1(x873)+~P1(x871)+~P2(x872)+~P8(x872)+~P4(x874,x873,x872)+~P4(x871,x873,x872)+P9(x871,x872,f13(x872,x873,x874,x871)) % 116.37/116.38 [88]~P1(x884)+~P1(x883)+~P1(x881)+~P2(x882)+~P8(x882)+~P4(x884,x883,x882)+~P4(x881,x883,x882)+P9(x881,x882,f13(x882,x883,x881,x884)) % 116.37/116.38 %EqnAxiom % 116.37/116.38 [1]E(x11,x11) % 116.37/116.38 [2]E(x22,x21)+~E(x21,x22) % 116.37/116.38 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.37/116.38 [4]~E(x41,x42)+E(f6(x41),f6(x42)) % 116.37/116.38 [5]~E(x51,x52)+E(f10(x51),f10(x52)) % 116.37/116.38 [6]~E(x61,x62)+E(f11(x61),f11(x62)) % 116.37/116.38 [7]~E(x71,x72)+E(f12(x71),f12(x72)) % 116.37/116.38 [8]~E(x81,x82)+E(f14(x81),f14(x82)) % 116.37/116.38 [9]~E(x91,x92)+E(f15(x91),f15(x92)) % 116.37/116.38 [10]~E(x101,x102)+E(f2(x101),f2(x102)) % 116.37/116.38 [11]~E(x111,x112)+E(f3(x111),f3(x112)) % 116.37/116.38 [12]~E(x121,x122)+E(f7(x121),f7(x122)) % 116.37/116.38 [13]~E(x131,x132)+E(f9(x131,x133,x134,x135),f9(x132,x133,x134,x135)) % 116.37/116.38 [14]~E(x141,x142)+E(f9(x143,x141,x144,x145),f9(x143,x142,x144,x145)) % 116.37/116.38 [15]~E(x151,x152)+E(f9(x153,x154,x151,x155),f9(x153,x154,x152,x155)) % 116.37/116.38 [16]~E(x161,x162)+E(f9(x163,x164,x165,x161),f9(x163,x164,x165,x162)) % 116.37/116.38 [17]~E(x171,x172)+E(f13(x171,x173,x174,x175),f13(x172,x173,x174,x175)) % 116.37/116.38 [18]~E(x181,x182)+E(f13(x183,x181,x184,x185),f13(x183,x182,x184,x185)) % 116.37/116.38 [19]~E(x191,x192)+E(f13(x193,x194,x191,x195),f13(x193,x194,x192,x195)) % 116.37/116.38 [20]~E(x201,x202)+E(f13(x203,x204,x205,x201),f13(x203,x204,x205,x202)) % 116.37/116.38 [21]~E(x211,x212)+E(f8(x211,x213,x214),f8(x212,x213,x214)) % 116.37/116.38 [22]~E(x221,x222)+E(f8(x223,x221,x224),f8(x223,x222,x224)) % 116.37/116.38 [23]~E(x231,x232)+E(f8(x233,x234,x231),f8(x233,x234,x232)) % 116.37/116.38 [24]~E(x241,x242)+E(f4(x241,x243,x244),f4(x242,x243,x244)) % 116.37/116.38 [25]~E(x251,x252)+E(f4(x253,x251,x254),f4(x253,x252,x254)) % 116.37/116.38 [26]~E(x261,x262)+E(f4(x263,x264,x261),f4(x263,x264,x262)) % 116.37/116.38 [27]~P1(x271)+P1(x272)+~E(x271,x272) % 116.37/116.38 [28]~P2(x281)+P2(x282)+~E(x281,x282) % 116.37/116.38 [29]~P5(x291)+P5(x292)+~E(x291,x292) % 116.37/116.38 [30]P3(x302,x303,x304)+~E(x301,x302)+~P3(x301,x303,x304) % 116.37/116.38 [31]P3(x313,x312,x314)+~E(x311,x312)+~P3(x313,x311,x314) % 116.37/116.38 [32]P3(x323,x324,x322)+~E(x321,x322)+~P3(x323,x324,x321) % 116.37/116.38 [33]~P6(x331)+P6(x332)+~E(x331,x332) % 116.37/116.38 [34]P4(x342,x343,x344)+~E(x341,x342)+~P4(x341,x343,x344) % 116.37/116.38 [35]P4(x353,x352,x354)+~E(x351,x352)+~P4(x353,x351,x354) % 116.37/116.38 [36]P4(x363,x364,x362)+~E(x361,x362)+~P4(x363,x364,x361) % 116.37/116.38 [37]P10(x372,x373,x374)+~E(x371,x372)+~P10(x371,x373,x374) % 116.37/116.38 [38]P10(x383,x382,x384)+~E(x381,x382)+~P10(x383,x381,x384) % 116.37/116.38 [39]P10(x393,x394,x392)+~E(x391,x392)+~P10(x393,x394,x391) % 116.37/116.38 [40]P9(x402,x403,x404)+~E(x401,x402)+~P9(x401,x403,x404) % 116.37/116.38 [41]P9(x413,x412,x414)+~E(x411,x412)+~P9(x413,x411,x414) % 116.37/116.38 [42]P9(x423,x424,x422)+~E(x421,x422)+~P9(x423,x424,x421) % 116.37/116.38 [43]~P8(x431)+P8(x432)+~E(x431,x432) % 116.37/116.38 [44]P7(x442,x443)+~E(x441,x442)+~P7(x441,x443) % 116.37/116.38 [45]P7(x453,x452)+~E(x451,x452)+~P7(x453,x451) % 116.37/116.38 % 116.37/116.38 %------------------------------------------- % 116.37/116.38 cnf(89,plain, % 116.37/116.38 (~P1(x891)+~P1(x891)+P9(x891,x892,x891)+~P2(x892)), % 116.37/116.38 inference(equality_inference,[],[64])). % 116.37/116.38 cnf(90,plain, % 116.37/116.38 (~P7(a1,a1)), % 116.37/116.38 inference(scs_inference,[],[46,49,65])). % 116.37/116.38 cnf(93,plain, % 116.37/116.38 (P9(a1,a5,a1)), % 116.37/116.38 inference(scs_inference,[],[46,49,47,65,89])). % 116.37/116.38 cnf(127,plain, % 116.37/116.38 (~E(x1271,a1)+P1(x1271)), % 116.37/116.38 inference(scs_inference,[],[46,27,2])). % 116.37/116.38 cnf(173,plain, % 116.37/116.38 (~P10(a1,a5,a1)), % 116.37/116.38 inference(scs_inference,[],[90,48,47,46,44,68])). % 116.37/116.38 cnf(194,plain, % 116.37/116.38 (~E(a5,x1941)+P8(x1941)+P4(f15(a5),f12(a5),a5)), % 116.37/116.38 inference(scs_inference,[],[47,63,43])). % 116.37/116.38 cnf(195,plain, % 116.37/116.38 (P8(a5)+P4(f15(a5),f12(a5),a5)), % 116.37/116.38 inference(equality_inference,[],[194])). % 116.37/116.38 cnf(196,plain, % 116.37/116.38 (P4(f15(a5),x1961,a5)+~E(f12(a5),x1961)+P8(a5)), % 116.37/116.38 inference(scs_inference,[],[195,35])). % 116.37/116.38 cnf(198,plain, % 116.37/116.38 (~E(a1,x1981)+P4(f4(a1,a5,a1),a1,a5)), % 116.37/116.38 inference(scs_inference,[],[49,93,46,47,30,82])). % 116.37/116.38 cnf(199,plain, % 116.37/116.38 (P4(f4(a1,a5,a1),a1,a5)), % 116.37/116.38 inference(equality_inference,[],[198])). % 116.37/116.38 cnf(208,plain, % 116.37/116.38 (P4(f4(a1,a5,a1),x2081,a5)+~E(a1,x2081)), % 116.37/116.38 inference(scs_inference,[],[199,36,35])). % 116.37/116.38 cnf(213,plain, % 116.37/116.38 (P10(a1,a5,f4(a1,a5,a1))+~P1(f4(a1,a5,a1))), % 116.37/116.38 inference(scs_inference,[],[46,47,199,70])). % 116.37/116.38 cnf(223,plain, % 116.37/116.38 (P9(a1,a5,f4(a1,a5,a1))+~P1(f4(a1,a5,a1))), % 116.37/116.38 inference(scs_inference,[],[46,47,213,71])). % 116.37/116.38 cnf(225,plain, % 116.37/116.38 (P9(a1,a5,f4(a1,a5,a1))), % 116.37/116.38 inference(scs_inference,[],[46,47,199,223,66])). % 116.37/116.38 cnf(468,plain, % 116.37/116.38 (P1(f4(a1,a5,a1))), % 116.37/116.38 inference(scs_inference,[],[47,199,127,66])). % 116.37/116.38 cnf(469,plain, % 116.37/116.38 (P10(a1,a5,f4(a1,a5,a1))), % 116.37/116.38 inference(scs_inference,[],[468,213])). % 116.37/116.38 cnf(471,plain, % 116.37/116.38 (~P3(a1,f4(a1,a5,a1),a5)), % 116.37/116.38 inference(scs_inference,[],[468,199,47,73])). % 116.37/116.38 cnf(473,plain, % 116.37/116.38 (P9(f4(a1,a5,a1),a5,f4(a1,a5,a1))), % 116.37/116.38 inference(scs_inference,[],[468,199,47,73,64])). % 116.37/116.38 cnf(476,plain, % 116.37/116.38 (P7(f4(a1,a5,a1),a1)), % 116.37/116.38 inference(scs_inference,[],[46,469,468,47,48,68])). % 116.37/116.38 cnf(478,plain, % 116.37/116.38 (~P10(f4(a1,a5,a1),a5,a1)), % 116.37/116.38 inference(scs_inference,[],[46,469,468,173,47,48,68,77])). % 116.37/116.38 cnf(511,plain, % 116.37/116.38 (P4(f4(a1,a5,f4(a1,a5,a1)),f4(a1,a5,a1),a5)), % 116.37/116.38 inference(scs_inference,[],[49,225,468,47,127,82])). % 116.37/116.38 cnf(527,plain, % 116.37/116.38 (P10(f4(a1,a5,a1),a5,f4(a1,a5,f4(a1,a5,a1)))+~P1(f4(a1,a5,f4(a1,a5,a1)))), % 116.37/116.38 inference(scs_inference,[],[468,47,511,70])). % 116.37/116.38 cnf(535,plain, % 116.37/116.38 (P9(f4(a1,a5,a1),a5,f4(a1,a5,f4(a1,a5,a1)))+~P1(f4(a1,a5,f4(a1,a5,a1)))), % 116.37/116.38 inference(scs_inference,[],[468,47,527,71])). % 116.37/116.38 cnf(549,plain, % 116.37/116.38 (~P3(f4(a1,a5,a1),f4(a1,a5,a1),a5)), % 116.37/116.38 inference(scs_inference,[],[511,468,47,73])). % 116.37/116.38 cnf(1839,plain, % 116.37/116.38 (~E(x18391,x18392)+~P1(f7(x18391))+P1(f7(x18392))), % 116.37/116.38 inference(scs_inference,[],[12,27])). % 116.37/116.38 cnf(1866,plain, % 116.37/116.38 (~E(a5,x18661)+P2(x18661)), % 116.37/116.38 inference(scs_inference,[],[47,28])). % 116.37/116.38 cnf(1870,plain, % 116.37/116.38 (P4(f4(f4(a1,a5,a1),a5,f4(a1,a5,a1)),f4(a1,a5,a1),a5)), % 116.37/116.38 inference(scs_inference,[],[473,549,468,1866,82])). % 116.37/116.38 cnf(1873,plain, % 116.37/116.38 (~P4(a1,f4(a1,a5,a1),a5)), % 116.37/116.38 inference(scs_inference,[],[46,478,468,47,50,70])). % 116.37/116.38 cnf(1921,plain, % 116.37/116.38 (P1(x19211)+~P4(x19211,f4(a1,a5,a1),a5)), % 116.37/116.38 inference(scs_inference,[],[468,47,66])). % 116.37/116.38 cnf(1957,plain, % 116.37/116.38 (P1(x19571)+~P3(x19571,f4(a1,a5,a1),a5)), % 116.37/116.38 inference(scs_inference,[],[468,47,67])). % 116.37/116.38 cnf(2082,plain, % 116.37/116.38 (P1(f7(f4(a1,a5,a1)))), % 116.37/116.38 inference(scs_inference,[],[468,476,1957,65])). % 116.37/116.38 cnf(4844,plain, % 116.37/116.38 (~E(f4(f4(a1,a5,a1),a5,f4(a1,a5,a1)),a1)), % 116.37/116.38 inference(scs_inference,[],[1870,1873,34])). % 116.37/116.38 cnf(4850,plain, % 116.37/116.38 (~P4(x48501,f7(f4(a1,a5,a1)),a5)), % 116.37/116.38 inference(scs_inference,[],[1870,2082,476,471,1873,468,47,34,65,30,89,73])). % 116.37/116.38 cnf(4852,plain, % 116.37/116.38 (P1(f4(f4(a1,a5,a1),a5,f4(a1,a5,a1)))), % 116.37/116.38 inference(scs_inference,[],[1870,2082,476,471,1873,468,47,34,65,30,89,73,1921])). % 116.37/116.38 cnf(4855,plain, % 116.37/116.38 (~E(f4(a1,a5,a1),f7(f4(a1,a5,a1)))), % 116.37/116.38 inference(scs_inference,[],[1870,2082,476,471,1873,468,47,34,65,30,89,73,1921,1839,35])). % 116.37/116.38 cnf(4856,plain, % 116.37/116.38 (P9(f4(a1,a5,a1),a5,f7(f4(a1,a5,a1)))), % 116.37/116.38 inference(scs_inference,[],[1870,2082,476,471,1873,468,47,34,65,30,89,73,1921,1839,35,69])). % 116.37/116.38 cnf(4869,plain, % 116.37/116.38 (P1(f4(a1,a5,f4(a1,a5,a1)))), % 116.37/116.38 inference(scs_inference,[],[511,468,47,66])). % 116.37/116.38 cnf(4873,plain, % 116.37/116.38 (~P10(f4(f4(a1,a5,a1),a5,f4(a1,a5,a1)),a5,a1)), % 116.37/116.38 inference(scs_inference,[],[4852,1870,511,46,468,478,47,66,73,76])). % 116.37/116.38 cnf(4876,plain, % 116.37/116.38 (~P4(x48761,f7(f4(a1,a5,a1)),a5)), % 116.37/116.38 inference(rename_variables,[],[4850])). % 116.37/116.38 cnf(4884,plain, % 116.37/116.38 (P10(f4(a1,a5,a1),a5,f7(f4(a1,a5,a1)))), % 116.37/116.38 inference(scs_inference,[],[4852,4855,4850,4876,4856,2082,1870,511,46,468,478,47,66,73,76,208,527,535,196,89,72])). % 116.37/116.38 cnf(4898,plain, % 116.37/116.38 (~P9(a1,a5,f7(f4(a1,a5,a1)))), % 116.37/116.38 inference(scs_inference,[],[4844,4873,4850,4852,2082,49,46,47,70,72,82])). % 116.37/116.38 cnf(4902,plain, % 116.37/116.38 (~P10(f4(a1,a5,f4(a1,a5,a1)),a5,a1)), % 116.37/116.38 inference(scs_inference,[],[4869,4844,4873,4850,4852,2082,49,511,46,468,478,47,70,72,82,76])). % 116.37/116.38 cnf(4916,plain, % 116.37/116.38 (~P10(a1,a5,f7(f4(a1,a5,a1)))), % 116.37/116.38 inference(scs_inference,[],[4898,4902,4869,2082,46,47,70,71])). % 116.37/116.38 cnf(4937,plain, % 116.37/116.38 ($false), % 116.37/116.38 inference(scs_inference,[],[4916,4884,2082,46,468,47,199,76]), % 116.37/116.38 ['proof']). % 116.37/116.38 % SZS output end Proof % 116.37/116.38 % Total time :115.760000s %------------------------------------------------------------------------------