%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM017+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 : n024.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:46 EDT 2024 % Result : Theorem 60.92s 61.53s % Output : CNFRefutation 60.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : COM017+1 : TPTP v8.2.0. Released v4.0.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n024.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:38:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 60.92/61.51 %------------------------------------------- % 60.92/61.51 % File :CSE---1.7 % 60.92/61.51 % Problem :theBenchmark % 60.92/61.51 % Transform :cnf % 60.92/61.51 % Format :tptp:raw % 60.92/61.51 % Command :java -jar mcs_scs.jar %d %s % 60.92/61.51 % 60.92/61.51 % Result :Theorem 60.370000s % 60.92/61.51 % Output :CNFRefutation 60.370000s % 60.92/61.51 %------------------------------------------- % 60.92/61.52 %------------------------------------------------------------------------------ % 60.92/61.52 % File : COM017+1 : TPTP v8.2.0. Released v4.0.0. % 60.92/61.52 % Domain : Computing Theory % 60.92/61.52 % Problem : Newman's lemma on rewriting systems 03_01_03, 00 expansion % 60.92/61.52 % Version : Especial. % 60.92/61.52 % English : % 60.92/61.52 % 60.92/61.52 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 60.92/61.52 % : [PV+07] Paskevich et al. (2007), Reasoning Inside a Formula an % 60.92/61.52 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 60.92/61.52 % Source : [Pas08] % 60.92/61.52 % Names : newman_03_01_03.00 [Pas08] % 60.92/61.52 % 60.92/61.52 % Status : Theorem % 60.92/61.52 % Rating : 0.14 v8.2.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.13 v7.3.0, 0.14 v7.1.0, 0.09 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.12 v6.2.0, 0.16 v6.1.0, 0.20 v6.0.0, 0.13 v5.5.0, 0.15 v5.4.0, 0.21 v5.3.0, 0.30 v5.2.0, 0.15 v5.1.0, 0.24 v5.0.0, 0.33 v4.1.0, 0.39 v4.0.1, 0.70 v4.0.0 % 60.92/61.52 % Syntax : Number of formulae : 22 ( 1 unt; 6 def) % 60.92/61.52 % Number of atoms : 107 ( 1 equ) % 60.92/61.52 % Maximal formula atoms : 10 ( 4 avg) % 60.92/61.52 % Number of connectives : 86 ( 1 ~; 2 |; 51 &) % 60.92/61.52 % ( 6 <=>; 26 =>; 0 <=; 0 <~>) % 60.92/61.52 % Maximal formula depth : 12 ( 6 avg) % 60.92/61.52 % Maximal term depth : 1 ( 1 avg) % 60.92/61.52 % Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty) % 60.92/61.52 % Number of functors : 6 ( 6 usr; 6 con; 0-0 aty) % 60.92/61.52 % Number of variables : 50 ( 43 !; 7 ?) % 60.92/61.52 % SPC : FOF_THM_RFO_SEQ % 60.92/61.52 % 60.92/61.52 % Comments : Problem generated by the SAD system [VLP07] % 60.92/61.52 %------------------------------------------------------------------------------ % 60.92/61.52 fof(mElmSort,axiom, % 60.92/61.52 ! [W0] : % 60.92/61.52 ( aElement0(W0) % 60.92/61.52 => $true ) ). % 60.92/61.52 % 60.92/61.52 fof(mRelSort,axiom, % 60.92/61.52 ! [W0] : % 60.92/61.52 ( aRewritingSystem0(W0) % 60.92/61.52 => $true ) ). % 60.92/61.52 % 60.92/61.52 fof(mReduct,axiom, % 60.92/61.52 ! [W0,W1] : % 60.92/61.52 ( ( aElement0(W0) % 60.92/61.52 & aRewritingSystem0(W1) ) % 60.92/61.52 => ! [W2] : % 60.92/61.52 ( aReductOfIn0(W2,W0,W1) % 60.92/61.52 => aElement0(W2) ) ) ). % 60.92/61.52 % 60.92/61.52 fof(mWFOrd,axiom, % 60.92/61.52 ! [W0,W1] : % 60.92/61.52 ( ( aElement0(W0) % 60.92/61.52 & aElement0(W1) ) % 60.92/61.52 => ( iLess0(W0,W1) % 60.92/61.52 => $true ) ) ). % 60.92/61.52 % 60.92/61.52 fof(mTCbr,axiom, % 60.92/61.52 ! [W0,W1,W2] : % 60.92/61.52 ( ( aElement0(W0) % 60.92/61.52 & aRewritingSystem0(W1) % 60.92/61.52 & aElement0(W2) ) % 60.92/61.52 => ( sdtmndtplgtdt0(W0,W1,W2) % 60.92/61.52 => $true ) ) ). % 60.92/61.52 % 60.92/61.52 fof(mTCDef,definition, % 60.92/61.52 ! [W0,W1,W2] : % 60.92/61.52 ( ( aElement0(W0) % 60.92/61.52 & aRewritingSystem0(W1) % 60.92/61.52 & aElement0(W2) ) % 60.92/61.52 => ( sdtmndtplgtdt0(W0,W1,W2) % 60.92/61.52 <=> ( aReductOfIn0(W2,W0,W1) % 60.92/61.52 | ? [W3] : % 60.92/61.52 ( aElement0(W3) % 60.92/61.52 & aReductOfIn0(W3,W0,W1) % 60.92/61.52 & sdtmndtplgtdt0(W3,W1,W2) ) ) ) ) ). % 60.92/61.52 % 60.92/61.52 fof(mTCTrans,axiom, % 60.92/61.52 ! [W0,W1,W2,W3] : % 60.92/61.52 ( ( aElement0(W0) % 60.92/61.52 & aRewritingSystem0(W1) % 60.92/61.52 & aElement0(W2) % 60.92/61.52 & aElement0(W3) ) % 60.92/61.52 => ( ( sdtmndtplgtdt0(W0,W1,W2) % 60.92/61.52 & sdtmndtplgtdt0(W2,W1,W3) ) % 60.92/61.52 => sdtmndtplgtdt0(W0,W1,W3) ) ) ). % 60.92/61.52 % 60.92/61.52 fof(mTCRDef,definition, % 60.92/61.52 ! [W0,W1,W2] : % 60.92/61.52 ( ( aElement0(W0) % 60.92/61.52 & aRewritingSystem0(W1) % 60.92/61.52 & aElement0(W2) ) % 60.92/61.52 => ( sdtmndtasgtdt0(W0,W1,W2) % 60.92/61.52 <=> ( W0 = W2 % 60.92/61.52 | sdtmndtplgtdt0(W0,W1,W2) ) ) ) ). % 60.92/61.52 % 60.92/61.52 fof(mTCRTrans,axiom, % 60.92/61.52 ! [W0,W1,W2,W3] : % 60.92/61.52 ( ( aElement0(W0) % 60.92/61.52 & aRewritingSystem0(W1) % 60.92/61.52 & aElement0(W2) % 60.92/61.52 & aElement0(W3) ) % 60.92/61.52 => ( ( sdtmndtasgtdt0(W0,W1,W2) % 60.92/61.52 & sdtmndtasgtdt0(W2,W1,W3) ) % 60.92/61.52 => sdtmndtasgtdt0(W0,W1,W3) ) ) ). % 60.92/61.52 % 60.92/61.52 fof(mCRDef,definition, % 60.92/61.52 ! [W0] : % 60.92/61.52 ( aRewritingSystem0(W0) % 60.92/61.52 => ( isConfluent0(W0) % 60.92/61.53 <=> ! [W1,W2,W3] : % 60.92/61.53 ( ( aElement0(W1) % 60.92/61.53 & aElement0(W2) % 60.92/61.53 & aElement0(W3) % 60.92/61.53 & sdtmndtasgtdt0(W1,W0,W2) % 60.92/61.53 & sdtmndtasgtdt0(W1,W0,W3) ) % 60.92/61.53 => ? [W4] : % 60.92/61.53 ( aElement0(W4) % 60.92/61.53 & sdtmndtasgtdt0(W2,W0,W4) % 60.92/61.53 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 60.92/61.53 % 60.92/61.53 fof(mWCRDef,definition, % 60.92/61.53 ! [W0] : % 60.92/61.53 ( aRewritingSystem0(W0) % 60.92/61.53 => ( isLocallyConfluent0(W0) % 60.92/61.53 <=> ! [W1,W2,W3] : % 60.92/61.53 ( ( aElement0(W1) % 60.92/61.53 & aElement0(W2) % 60.92/61.53 & aElement0(W3) % 60.92/61.53 & aReductOfIn0(W2,W1,W0) % 60.92/61.53 & aReductOfIn0(W3,W1,W0) ) % 60.92/61.53 => ? [W4] : % 60.92/61.53 ( aElement0(W4) % 60.92/61.53 & sdtmndtasgtdt0(W2,W0,W4) % 60.92/61.53 & sdtmndtasgtdt0(W3,W0,W4) ) ) ) ) ). % 60.92/61.53 % 60.92/61.53 fof(mTermin,definition, % 60.92/61.53 ! [W0] : % 60.92/61.53 ( aRewritingSystem0(W0) % 60.92/61.53 => ( isTerminating0(W0) % 60.92/61.53 <=> ! [W1,W2] : % 60.92/61.53 ( ( aElement0(W1) % 60.92/61.53 & aElement0(W2) ) % 60.92/61.53 => ( sdtmndtplgtdt0(W1,W0,W2) % 60.92/61.53 => iLess0(W2,W1) ) ) ) ) ). % 60.92/61.53 % 60.92/61.53 fof(mNFRDef,definition, % 60.92/61.53 ! [W0,W1] : % 60.92/61.53 ( ( aElement0(W0) % 60.92/61.53 & aRewritingSystem0(W1) ) % 60.92/61.53 => ! [W2] : % 60.92/61.53 ( aNormalFormOfIn0(W2,W0,W1) % 60.92/61.53 <=> ( aElement0(W2) % 60.92/61.53 & sdtmndtasgtdt0(W0,W1,W2) % 60.92/61.53 & ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ) ). % 60.92/61.53 % 60.92/61.53 fof(mTermNF,axiom, % 60.92/61.53 ! [W0] : % 60.92/61.53 ( ( aRewritingSystem0(W0) % 60.92/61.53 & isTerminating0(W0) ) % 60.92/61.53 => ! [W1] : % 60.92/61.53 ( aElement0(W1) % 60.92/61.53 => ? [W2] : aNormalFormOfIn0(W2,W1,W0) ) ) ). % 60.92/61.53 % 60.92/61.53 fof(m__656,hypothesis, % 60.92/61.53 aRewritingSystem0(xR) ). % 60.92/61.53 % 60.92/61.53 fof(m__656_01,hypothesis, % 60.92/61.53 ( isLocallyConfluent0(xR) % 60.92/61.53 & isTerminating0(xR) ) ). % 60.92/61.53 % 60.92/61.53 fof(m__731,hypothesis, % 60.92/61.53 ( aElement0(xa) % 60.92/61.53 & aElement0(xb) % 60.92/61.53 & aElement0(xc) ) ). % 60.92/61.53 % 60.92/61.53 fof(m__715,hypothesis, % 60.92/61.53 ! [W0,W1,W2] : % 60.92/61.53 ( ( aElement0(W0) % 60.92/61.53 & aElement0(W1) % 60.92/61.53 & aElement0(W2) % 60.92/61.53 & sdtmndtasgtdt0(W0,xR,W1) % 60.92/61.53 & sdtmndtasgtdt0(W0,xR,W2) ) % 60.92/61.53 => ( iLess0(W0,xa) % 60.92/61.53 => ? [W3] : % 60.92/61.53 ( aElement0(W3) % 60.92/61.53 & sdtmndtasgtdt0(W1,xR,W3) % 60.92/61.53 & sdtmndtasgtdt0(W2,xR,W3) ) ) ) ). % 60.92/61.53 % 60.92/61.53 fof(m__731_02,hypothesis, % 60.92/61.53 ( sdtmndtplgtdt0(xa,xR,xb) % 60.92/61.53 & sdtmndtplgtdt0(xa,xR,xc) ) ). % 60.92/61.53 % 60.92/61.53 fof(m__755,hypothesis, % 60.92/61.53 ( aElement0(xu) % 60.92/61.53 & aReductOfIn0(xu,xa,xR) % 60.92/61.53 & sdtmndtasgtdt0(xu,xR,xb) ) ). % 60.92/61.53 % 60.92/61.53 fof(m__779,hypothesis, % 60.92/61.53 ( aElement0(xv) % 60.92/61.53 & aReductOfIn0(xv,xa,xR) % 60.92/61.53 & sdtmndtasgtdt0(xv,xR,xc) ) ). % 60.92/61.53 % 60.92/61.53 fof(m__,conjecture, % 60.92/61.53 ? [W0] : % 60.92/61.53 ( aElement0(W0) % 60.92/61.53 & sdtmndtasgtdt0(xu,xR,W0) % 60.92/61.53 & sdtmndtasgtdt0(xv,xR,W0) ) ). % 60.92/61.53 % 60.92/61.53 %------------------------------------------------------------------------------ % 60.92/61.53 %------------------------------------------- % 60.92/61.53 % Proof found % 60.92/61.53 % SZS status Theorem for theBenchmark % 60.92/61.53 % SZS output start Proof % 60.92/61.53 %ClaNum:106(EqnAxiom:49) % 60.92/61.53 %VarNum:381(SingletonVarNum:106) % 60.92/61.53 %MaxLitNum:8 % 60.92/61.53 %MaxfuncDepth:1 % 60.92/61.53 %SharedTerms:20 % 60.92/61.53 %goalClause: 87 % 60.92/61.53 [50]P1(a1) % 60.92/61.53 [51]P1(a17) % 60.92/61.53 [52]P1(a18) % 60.92/61.53 [53]P1(a19) % 60.92/61.53 [54]P1(a20) % 60.92/61.53 [55]P2(a2) % 60.92/61.53 [56]P5(a2) % 60.92/61.53 [57]P8(a2) % 60.92/61.53 [58]P3(a19,a1,a2) % 60.92/61.53 [59]P3(a20,a1,a2) % 60.92/61.53 [60]P9(a1,a2,a17) % 60.92/61.53 [61]P9(a1,a2,a18) % 60.92/61.53 [62]P10(a19,a2,a17) % 60.92/61.53 [63]P10(a20,a2,a18) % 60.92/61.53 [87]~P1(x871)+~P10(a19,a2,x871)+~P10(a20,a2,x871) % 60.92/61.53 [64]~P2(x641)+P6(x641)+P1(f3(x641)) % 60.92/61.53 [65]~P2(x651)+P6(x651)+P1(f11(x651)) % 60.92/61.53 [66]~P2(x661)+P6(x661)+P1(f12(x661)) % 60.92/61.53 [67]~P2(x671)+P5(x671)+P1(f13(x671)) % 60.92/61.53 [68]~P2(x681)+P5(x681)+P1(f15(x681)) % 60.92/61.53 [69]~P2(x691)+P5(x691)+P1(f16(x691)) % 60.92/61.53 [70]~P2(x701)+P8(x701)+P1(f4(x701)) % 60.92/61.53 [71]~P2(x711)+P8(x711)+P1(f5(x711)) % 60.92/61.53 [72]~P2(x721)+P8(x721)+~P7(f5(x721),f4(x721)) % 60.92/61.53 [73]~P2(x731)+P6(x731)+P10(f3(x731),x731,f11(x731)) % 60.92/61.53 [74]~P2(x741)+P6(x741)+P10(f3(x741),x741,f12(x741)) % 60.92/61.53 [75]~P2(x751)+P8(x751)+P9(f4(x751),x751,f5(x751)) % 60.92/61.53 [76]~P2(x761)+P5(x761)+P3(f15(x761),f13(x761),x761) % 60.92/61.53 [77]~P2(x771)+P5(x771)+P3(f16(x771),f13(x771),x771) % 60.92/61.53 [79]~P1(x792)+~P2(x791)+~P8(x791)+P4(f6(x791,x792),x792,x791) % 60.92/61.53 [80]~P3(x801,x802,x803)+P1(x801)+~P1(x802)+~P2(x803) % 60.92/61.53 [81]~P4(x811,x812,x813)+P1(x811)+~P1(x812)+~P2(x813) % 60.92/61.53 [83]~P1(x831)+~P2(x832)+~P4(x833,x831,x832)+P10(x831,x832,x833) % 60.92/61.53 [88]~P4(x884,x881,x882)+~P1(x881)+~P3(x883,x884,x882)+~P2(x882) % 60.92/61.53 [89]~P2(x891)+P6(x891)+~P1(x892)+~P10(f11(x891),x891,x892)+~P10(f12(x891),x891,x892) % 60.92/61.53 [90]~P2(x901)+P5(x901)+~P1(x902)+~P10(f15(x901),x901,x902)+~P10(f16(x901),x901,x902) % 60.92/61.53 [78]~E(x781,x783)+~P1(x783)+~P1(x781)+~P2(x782)+P10(x781,x782,x783) % 60.92/61.53 [84]~P1(x841)+~P1(x843)+~P2(x842)+~P3(x843,x841,x842)+P9(x841,x842,x843) % 60.92/61.53 [85]~P1(x853)+~P1(x851)+~P2(x852)+~P9(x851,x852,x853)+P10(x851,x852,x853) % 60.92/61.53 [82]~P1(x821)+~P1(x822)+~P8(x823)+~P9(x822,x823,x821)+P7(x821,x822)+~P2(x823) % 60.92/61.53 [86]~P1(x862)+~P1(x861)+~P2(x863)+~P10(x861,x863,x862)+E(x861,x862)+P9(x861,x863,x862) % 60.92/61.53 [94]~P1(x941)+~P1(x942)+~P2(x943)+~P9(x942,x943,x941)+P3(x941,x942,x943)+P1(f8(x942,x943,x941)) % 60.92/61.53 [96]~P1(x961)+~P1(x962)+~P2(x963)+~P9(x962,x963,x961)+P3(x961,x962,x963)+P3(f8(x962,x963,x961),x962,x963) % 60.92/61.53 [97]~P1(x971)+~P1(x972)+~P2(x973)+~P9(x972,x973,x971)+P3(x971,x972,x973)+P9(f8(x972,x973,x971),x973,x971) % 60.92/61.53 [98]~P1(x982)+~P1(x981)+~P2(x983)+~P10(x982,x983,x981)+P4(x981,x982,x983)+P3(f7(x982,x983,x981),x981,x983) % 60.92/61.53 [95]~P1(x953)+~P1(x952)+~P1(x951)+~P10(x951,a2,x953)+~P10(x951,a2,x952)+~P7(x951,a1)+P1(f9(x951,x952,x953)) % 60.92/61.53 [99]~P1(x993)+~P1(x992)+~P1(x991)+~P10(x992,a2,x993)+~P10(x992,a2,x991)+~P7(x992,a1)+P10(x991,a2,f9(x992,x993,x991)) % 60.92/61.53 [100]~P1(x1003)+~P1(x1002)+~P1(x1001)+~P10(x1002,a2,x1003)+~P10(x1002,a2,x1001)+~P7(x1002,a1)+P10(x1001,a2,f9(x1002,x1001,x1003)) % 60.92/61.53 [91]~P1(x913)+~P1(x911)+~P2(x912)+~P3(x914,x911,x912)+~P9(x914,x912,x913)+P9(x911,x912,x913)+~P1(x914) % 60.92/61.53 [92]~P1(x923)+~P1(x921)+~P2(x922)+~P9(x924,x922,x923)+~P9(x921,x922,x924)+P9(x921,x922,x923)+~P1(x924) % 60.92/61.53 [93]~P1(x933)+~P1(x931)+~P2(x932)+~P10(x934,x932,x933)+~P10(x931,x932,x934)+P10(x931,x932,x933)+~P1(x934) % 60.92/61.53 [101]~P1(x1014)+~P1(x1013)+~P1(x1012)+~P2(x1011)+~P6(x1011)+~P10(x1012,x1011,x1014)+~P10(x1012,x1011,x1013)+P1(f10(x1011,x1012,x1013,x1014)) % 60.92/61.53 [102]~P1(x1024)+~P1(x1023)+~P1(x1022)+~P2(x1021)+~P5(x1021)+~P3(x1024,x1022,x1021)+~P3(x1023,x1022,x1021)+P1(f14(x1021,x1022,x1023,x1024)) % 60.92/61.53 [103]~P1(x1034)+~P1(x1033)+~P1(x1031)+~P2(x1032)+~P6(x1032)+~P10(x1033,x1032,x1034)+~P10(x1033,x1032,x1031)+P10(x1031,x1032,f10(x1032,x1033,x1034,x1031)) % 60.92/61.53 [104]~P1(x1044)+~P1(x1043)+~P1(x1041)+~P2(x1042)+~P6(x1042)+~P10(x1043,x1042,x1044)+~P10(x1043,x1042,x1041)+P10(x1041,x1042,f10(x1042,x1043,x1041,x1044)) % 60.92/61.53 [105]~P1(x1054)+~P1(x1053)+~P1(x1051)+~P2(x1052)+~P5(x1052)+~P3(x1054,x1053,x1052)+~P3(x1051,x1053,x1052)+P10(x1051,x1052,f14(x1052,x1053,x1054,x1051)) % 60.92/61.53 [106]~P1(x1064)+~P1(x1063)+~P1(x1061)+~P2(x1062)+~P5(x1062)+~P3(x1064,x1063,x1062)+~P3(x1061,x1063,x1062)+P10(x1061,x1062,f14(x1062,x1063,x1061,x1064)) % 60.92/61.53 %EqnAxiom % 60.92/61.53 [1]E(x11,x11) % 60.92/61.53 [2]E(x22,x21)+~E(x21,x22) % 60.92/61.53 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 60.92/61.53 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 60.92/61.53 [5]~E(x51,x52)+E(f11(x51),f11(x52)) % 60.92/61.53 [6]~E(x61,x62)+E(f12(x61),f12(x62)) % 60.92/61.53 [7]~E(x71,x72)+E(f13(x71),f13(x72)) % 60.92/61.53 [8]~E(x81,x82)+E(f15(x81),f15(x82)) % 60.92/61.53 [9]~E(x91,x92)+E(f16(x91),f16(x92)) % 60.92/61.53 [10]~E(x101,x102)+E(f4(x101),f4(x102)) % 60.92/61.53 [11]~E(x111,x112)+E(f5(x111),f5(x112)) % 60.92/61.53 [12]~E(x121,x122)+E(f8(x121,x123,x124),f8(x122,x123,x124)) % 60.92/61.53 [13]~E(x131,x132)+E(f8(x133,x131,x134),f8(x133,x132,x134)) % 60.92/61.53 [14]~E(x141,x142)+E(f8(x143,x144,x141),f8(x143,x144,x142)) % 60.92/61.53 [15]~E(x151,x152)+E(f10(x151,x153,x154,x155),f10(x152,x153,x154,x155)) % 60.92/61.53 [16]~E(x161,x162)+E(f10(x163,x161,x164,x165),f10(x163,x162,x164,x165)) % 60.92/61.53 [17]~E(x171,x172)+E(f10(x173,x174,x171,x175),f10(x173,x174,x172,x175)) % 60.92/61.53 [18]~E(x181,x182)+E(f10(x183,x184,x185,x181),f10(x183,x184,x185,x182)) % 60.92/61.53 [19]~E(x191,x192)+E(f14(x191,x193,x194,x195),f14(x192,x193,x194,x195)) % 60.92/61.53 [20]~E(x201,x202)+E(f14(x203,x201,x204,x205),f14(x203,x202,x204,x205)) % 60.92/61.53 [21]~E(x211,x212)+E(f14(x213,x214,x211,x215),f14(x213,x214,x212,x215)) % 60.92/61.53 [22]~E(x221,x222)+E(f14(x223,x224,x225,x221),f14(x223,x224,x225,x222)) % 60.92/61.53 [23]~E(x231,x232)+E(f9(x231,x233,x234),f9(x232,x233,x234)) % 60.92/61.53 [24]~E(x241,x242)+E(f9(x243,x241,x244),f9(x243,x242,x244)) % 60.92/61.53 [25]~E(x251,x252)+E(f9(x253,x254,x251),f9(x253,x254,x252)) % 60.92/61.53 [26]~E(x261,x262)+E(f6(x261,x263),f6(x262,x263)) % 60.92/61.53 [27]~E(x271,x272)+E(f6(x273,x271),f6(x273,x272)) % 60.92/61.53 [28]~E(x281,x282)+E(f7(x281,x283,x284),f7(x282,x283,x284)) % 60.92/61.53 [29]~E(x291,x292)+E(f7(x293,x291,x294),f7(x293,x292,x294)) % 60.92/61.53 [30]~E(x301,x302)+E(f7(x303,x304,x301),f7(x303,x304,x302)) % 60.92/61.53 [31]~P1(x311)+P1(x312)+~E(x311,x312) % 60.92/61.53 [32]P3(x322,x323,x324)+~E(x321,x322)+~P3(x321,x323,x324) % 60.92/61.53 [33]P3(x333,x332,x334)+~E(x331,x332)+~P3(x333,x331,x334) % 60.92/61.53 [34]P3(x343,x344,x342)+~E(x341,x342)+~P3(x343,x344,x341) % 60.92/61.53 [35]P10(x352,x353,x354)+~E(x351,x352)+~P10(x351,x353,x354) % 60.92/61.53 [36]P10(x363,x362,x364)+~E(x361,x362)+~P10(x363,x361,x364) % 60.92/61.53 [37]P10(x373,x374,x372)+~E(x371,x372)+~P10(x373,x374,x371) % 60.92/61.53 [38]~P5(x381)+P5(x382)+~E(x381,x382) % 60.92/61.53 [39]~P2(x391)+P2(x392)+~E(x391,x392) % 60.92/61.53 [40]P4(x402,x403,x404)+~E(x401,x402)+~P4(x401,x403,x404) % 60.92/61.53 [41]P4(x413,x412,x414)+~E(x411,x412)+~P4(x413,x411,x414) % 60.92/61.53 [42]P4(x423,x424,x422)+~E(x421,x422)+~P4(x423,x424,x421) % 60.92/61.53 [43]P9(x432,x433,x434)+~E(x431,x432)+~P9(x431,x433,x434) % 60.92/61.53 [44]P9(x443,x442,x444)+~E(x441,x442)+~P9(x443,x441,x444) % 60.92/61.53 [45]P9(x453,x454,x452)+~E(x451,x452)+~P9(x453,x454,x451) % 60.92/61.53 [46]~P8(x461)+P8(x462)+~E(x461,x462) % 60.92/61.53 [47]~P6(x471)+P6(x472)+~E(x471,x472) % 60.92/61.53 [48]P7(x482,x483)+~E(x481,x482)+~P7(x481,x483) % 60.92/61.53 [49]P7(x493,x492)+~E(x491,x492)+~P7(x493,x491) % 60.92/61.53 % 60.92/61.53 %------------------------------------------- % 60.92/61.53 cnf(107,plain, % 60.92/61.53 (~P1(x1071)+~P1(x1071)+P10(x1071,x1072,x1071)+~P2(x1072)), % 60.92/61.53 inference(equality_inference,[],[78])). % 60.92/61.53 cnf(108,plain, % 60.92/61.53 (~P10(a20,a2,a17)), % 60.92/61.53 inference(scs_inference,[],[51,62,87])). % 60.92/61.53 cnf(114,plain, % 60.92/61.53 (P10(a1,a2,a1)), % 60.92/61.53 inference(scs_inference,[],[50,51,54,62,63,55,87,35,37,83,107])). % 60.92/61.53 cnf(116,plain, % 60.92/61.53 (~P4(a1,a1,a2)), % 60.92/61.53 inference(scs_inference,[],[50,51,54,62,63,55,58,87,35,37,83,107,88])). % 60.92/61.53 cnf(118,plain, % 60.92/61.53 (P10(a1,a2,a17)), % 60.92/61.53 inference(scs_inference,[],[50,51,54,62,63,55,58,60,87,35,37,83,107,88,85])). % 60.92/61.53 cnf(120,plain, % 60.92/61.53 (P9(a1,a2,a19)), % 60.92/61.53 inference(scs_inference,[],[50,51,53,54,62,63,55,58,60,87,35,37,83,107,88,85,84])). % 60.92/61.53 cnf(122,plain, % 60.92/61.53 (P7(a17,a1)), % 60.92/61.53 inference(scs_inference,[],[50,51,53,54,62,63,55,57,58,60,87,35,37,83,107,88,85,84,82])). % 60.92/61.54 cnf(124,plain, % 60.92/61.54 (~P10(a18,a2,a17)), % 60.92/61.54 inference(scs_inference,[],[50,51,52,53,54,62,63,55,57,58,60,87,35,37,83,107,88,85,84,82,93])). % 60.92/61.54 cnf(145,plain, % 60.92/61.54 (P9(a1,a2,a20)), % 60.92/61.54 inference(scs_inference,[],[50,108,118,124,52,54,59,61,55,35,83,88,85,84])). % 60.92/61.54 cnf(147,plain, % 60.92/61.54 (P7(a18,a1)), % 60.92/61.54 inference(scs_inference,[],[50,108,118,124,52,54,59,61,57,55,35,83,88,85,84,82])). % 60.92/61.54 cnf(163,plain, % 60.92/61.54 (P10(a1,a2,a19)), % 60.92/61.54 inference(scs_inference,[],[50,53,55,120,59,88,85])). % 60.92/61.54 cnf(165,plain, % 60.92/61.54 (P7(a19,a1)), % 60.92/61.54 inference(scs_inference,[],[50,53,55,120,57,59,88,85,82])). % 60.92/61.54 cnf(181,plain, % 60.92/61.54 (P10(a1,a2,a20)), % 60.92/61.54 inference(scs_inference,[],[50,54,55,58,145,88,85])). % 60.92/61.54 cnf(183,plain, % 60.92/61.54 (P7(a20,a1)), % 60.92/61.54 inference(scs_inference,[],[50,54,55,58,145,57,88,85,82])). % 60.92/61.54 cnf(197,plain, % 60.92/61.54 (~P4(a1,a17,a2)), % 60.92/61.54 inference(scs_inference,[],[51,55,58,88])). % 60.92/61.54 cnf(226,plain, % 60.92/61.54 (P10(a19,a2,a19)), % 60.92/61.54 inference(scs_inference,[],[181,53,163,55,36,35,37,78])). % 60.92/61.54 cnf(232,plain, % 60.92/61.54 (~P10(a20,a2,a19)), % 60.92/61.54 inference(scs_inference,[],[53,226,87])). % 60.92/61.54 cnf(246,plain, % 60.92/61.54 (P10(a17,a2,a17)), % 60.92/61.54 inference(scs_inference,[],[51,163,226,55,36,37,78])). % 60.92/61.54 cnf(252,plain, % 60.92/61.54 (P10(a19,a2,a1)+~P10(a17,a2,a1)), % 60.92/61.54 inference(scs_inference,[],[50,63,62,51,53,52,54,163,226,120,55,36,37,78,86,92,93])). % 60.92/61.54 cnf(259,plain, % 60.92/61.54 (P10(a18,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[108,52,226,246,55,35,36,37,78])). % 60.92/61.54 cnf(281,plain, % 60.92/61.54 (P10(a20,a2,a20)), % 60.92/61.54 inference(scs_inference,[],[54,55,78])). % 60.92/61.54 cnf(320,plain, % 60.92/61.54 (P10(a19,a2,a18)+~P10(a17,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[52,62,51,53,55,93])). % 60.92/61.54 cnf(364,plain, % 60.92/61.54 (P10(a19,a2,a20)+~P10(a17,a2,a20)), % 60.92/61.54 inference(scs_inference,[],[54,62,51,53,55,93])). % 60.92/61.54 cnf(408,plain, % 60.92/61.54 (~E(a19,a18)), % 60.92/61.54 inference(scs_inference,[],[124,62,35])). % 60.92/61.54 cnf(413,plain, % 60.92/61.54 (~E(a17,a18)), % 60.92/61.54 inference(scs_inference,[],[124,246,35])). % 60.92/61.54 cnf(437,plain, % 60.92/61.54 (~P10(a18,a2,a19)), % 60.92/61.54 inference(scs_inference,[],[232,63,53,54,52,55,37,93])). % 60.92/61.54 cnf(487,plain, % 60.92/61.54 (~E(a20,x4871)+P1(x4871)), % 60.92/61.54 inference(scs_inference,[],[50,55,59,31,80])). % 60.92/61.54 cnf(489,plain, % 60.92/61.54 (~E(x4891,a2)+~P5(a2)+P5(x4891)), % 60.92/61.54 inference(scs_inference,[],[56,38,2])). % 60.92/61.54 cnf(491,plain, % 60.92/61.54 (P5(x4911)+~E(x4911,a2)), % 60.92/61.54 inference(scs_inference,[],[56,489])). % 60.92/61.54 cnf(493,plain, % 60.92/61.54 (~E(x4931,a2)+~P2(a2)+P2(x4931)), % 60.92/61.54 inference(scs_inference,[],[55,39,2])). % 60.92/61.54 cnf(495,plain, % 60.92/61.54 (P2(x4951)+~E(x4951,a2)), % 60.92/61.54 inference(scs_inference,[],[55,493])). % 60.92/61.54 cnf(501,plain, % 60.92/61.54 (~E(x5011,a2)+~P8(a2)+P8(x5011)), % 60.92/61.54 inference(scs_inference,[],[57,46,2])). % 60.92/61.54 cnf(503,plain, % 60.92/61.54 (P8(x5031)+~E(x5031,a2)), % 60.92/61.54 inference(scs_inference,[],[57,501])). % 60.92/61.54 cnf(589,plain, % 60.92/61.54 (P10(a20,a2,f14(a2,a1,a20,a20))), % 60.92/61.54 inference(scs_inference,[],[56,59,50,55,487,106])). % 60.92/61.54 cnf(597,plain, % 60.92/61.54 (P1(f14(a2,a1,a20,a20))), % 60.92/61.54 inference(scs_inference,[],[56,59,50,55,487,102])). % 60.92/61.54 cnf(600,plain, % 60.92/61.54 (~P10(f14(a2,a1,a20,a20),a2,a17)), % 60.92/61.54 inference(scs_inference,[],[108,51,54,597,589,58,55,88,93])). % 60.92/61.54 cnf(641,plain, % 60.92/61.54 (P10(a1,a2,f14(a2,a1,a20,a20))), % 60.92/61.54 inference(scs_inference,[],[589,50,181,54,597,55,93])). % 60.92/61.54 cnf(694,plain, % 60.92/61.54 (P9(a1,a2,f14(a2,a1,a20,a20))), % 60.92/61.54 inference(scs_inference,[],[600,50,118,641,597,55,35,86])). % 60.92/61.54 cnf(783,plain, % 60.92/61.54 (P10(a19,a2,f14(a2,a1,a19,a19))), % 60.92/61.54 inference(scs_inference,[],[50,58,53,55,491,105])). % 60.92/61.54 cnf(803,plain, % 60.92/61.54 (~P1(f14(a2,a1,a19,a19))+P10(a19,a2,a1)+~P10(f14(a2,a1,a19,a19),a2,a1)), % 60.92/61.54 inference(scs_inference,[],[50,53,783,55,93])). % 60.92/61.54 cnf(970,plain, % 60.92/61.54 (P10(a1,a2,f14(a2,a1,a19,a19))+~P1(f14(a2,a1,a19,a19))), % 60.92/61.54 inference(scs_inference,[],[50,163,783,53,55,93])). % 60.92/61.54 cnf(1365,plain, % 60.92/61.54 (~E(a2,x13651)+P2(x13651)), % 60.92/61.54 inference(scs_inference,[],[495,2])). % 60.92/61.54 cnf(1428,plain, % 60.92/61.54 (P4(f6(a2,a1),a1,a2)), % 60.92/61.54 inference(scs_inference,[],[50,55,503,79])). % 60.92/61.54 cnf(1616,plain, % 60.92/61.54 (P9(a19,a2,a18)+~P10(a17,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[53,52,408,55,86,320])). % 60.92/61.54 cnf(1621,plain, % 60.92/61.54 (~P10(a17,a2,a18)+P9(a17,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[51,52,413,55,86])). % 60.92/61.54 cnf(1668,plain, % 60.92/61.54 (~P4(a18,a17,a2)+P9(a19,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[51,55,1616,83])). % 60.92/61.54 cnf(1699,plain, % 60.92/61.54 (~P10(a17,a2,a18)+P7(a18,a17)), % 60.92/61.54 inference(scs_inference,[],[55,52,51,57,1621,82])). % 60.92/61.54 cnf(1715,plain, % 60.92/61.54 (~P4(a18,a17,a2)+P7(a18,a17)), % 60.92/61.54 inference(scs_inference,[],[51,55,1699,83])). % 60.92/61.54 cnf(1731,plain, % 60.92/61.54 (~P4(x17311,a17,a2)+~E(x17311,a18)+P7(a18,a17)), % 60.92/61.54 inference(scs_inference,[],[1715,40])). % 60.92/61.54 cnf(1877,plain, % 60.92/61.54 (P10(a19,a2,a18)+~P4(a18,a17,a2)), % 60.92/61.54 inference(scs_inference,[],[52,53,55,1668,85])). % 60.92/61.54 cnf(1925,plain, % 60.92/61.54 (~P4(a18,a17,a2)), % 60.92/61.54 inference(scs_inference,[],[63,52,1877,87])). % 60.92/61.54 cnf(2749,plain, % 60.92/61.54 (P2(x27491)+~E(x27492,x27491)+~E(a2,x27492)), % 60.92/61.54 inference(scs_inference,[],[1365,3])). % 60.92/61.54 cnf(2765,plain, % 60.92/61.54 (P1(f6(a2,a1))+~E(x27651,a2)+~E(a2,x27651)), % 60.92/61.54 inference(scs_inference,[],[50,1428,2749,81])). % 60.92/61.54 cnf(2781,plain, % 60.92/61.54 (P10(f6(a2,a1),a2,f6(a2,a1))+~E(a2,x27811)+~E(x27811,a2)), % 60.92/61.54 inference(scs_inference,[],[55,2765,107])). % 60.92/61.54 cnf(2797,plain, % 60.92/61.54 (~E(a2,x27971)+P10(f6(a2,a1),a2,f6(a2,a1))), % 60.92/61.54 inference(scs_inference,[],[2781,2])). % 60.92/61.54 cnf(2798,plain, % 60.92/61.54 (P10(f6(a2,a1),a2,f6(a2,a1))), % 60.92/61.54 inference(equality_inference,[],[2797])). % 60.92/61.54 cnf(2996,plain, % 60.92/61.54 (~E(a1,f6(a2,a1))), % 60.92/61.54 inference(scs_inference,[],[1428,116,2,40])). % 60.92/61.54 cnf(3701,plain, % 60.92/61.54 (~E(x37011,a1)+P9(x37011,a2,f14(a2,a1,a20,a20))), % 60.92/61.54 inference(scs_inference,[],[694,2,43])). % 60.92/61.54 cnf(4264,plain, % 60.92/61.54 (P1(f6(a2,a1))), % 60.92/61.54 inference(scs_inference,[],[50,1428,55,81])). % 60.92/61.54 cnf(4266,plain, % 60.92/61.54 (~P4(a1,f6(a2,a1),a2)), % 60.92/61.54 inference(scs_inference,[],[50,1428,59,55,81,88])). % 60.92/61.54 cnf(5592,plain, % 60.92/61.54 (~P10(a19,a2,a20)), % 60.92/61.54 inference(scs_inference,[],[281,54,87])). % 60.92/61.54 cnf(5601,plain, % 60.92/61.54 (P9(a1,a2,f6(a2,a1))), % 60.92/61.54 inference(scs_inference,[],[50,2996,4264,2798,181,281,1428,55,54,87,35,83,88,98,86])). % 60.92/61.54 cnf(5603,plain, % 60.92/61.54 (P1(f9(a18,a18,a18))), % 60.92/61.54 inference(scs_inference,[],[50,2996,147,4264,259,2798,181,281,1428,55,52,54,87,35,83,88,98,86,95])). % 60.92/61.54 cnf(5605,plain, % 60.92/61.54 (P10(a18,a2,f9(a18,a18,a18))), % 60.92/61.54 inference(scs_inference,[],[50,2996,147,4264,259,2798,181,281,1428,55,52,54,87,35,83,88,98,86,95,99])). % 60.92/61.54 cnf(5607,plain, % 60.92/61.54 (~P10(a18,a2,a1)), % 60.92/61.54 inference(scs_inference,[],[50,437,2996,147,4264,163,259,2798,181,281,1428,55,52,53,54,87,35,83,88,98,86,95,99,93])). % 60.92/61.54 cnf(5609,plain, % 60.92/61.54 (P1(f14(a2,a1,a19,a19))), % 60.92/61.54 inference(scs_inference,[],[50,437,2996,147,4264,163,259,2798,181,281,56,1428,58,55,52,53,54,87,35,83,88,98,86,95,99,93,102])). % 60.92/61.54 cnf(5613,plain, % 60.92/61.54 (P10(a17,a2,f9(a17,a17,a17))), % 60.92/61.54 inference(scs_inference,[],[50,437,2996,122,147,4264,163,259,2798,181,246,281,56,1428,58,51,55,52,53,54,87,35,83,88,98,86,95,99,93,102,64,100])). % 60.92/61.54 cnf(5622,plain, % 60.92/61.54 (~P10(a17,a2,a20)), % 60.92/61.54 inference(scs_inference,[],[5592,364])). % 60.92/61.54 cnf(5623,plain, % 60.92/61.54 (P10(a19,a2,a1)+~P10(f14(a2,a1,a19,a19),a2,a1)), % 60.92/61.54 inference(scs_inference,[],[5609,803])). % 60.92/61.54 cnf(5626,plain, % 60.92/61.54 (P10(a1,a2,f14(a2,a1,a19,a19))), % 60.92/61.54 inference(scs_inference,[],[5609,970])). % 60.92/61.54 cnf(5635,plain, % 60.92/61.54 (~P10(a19,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[63,52,87])). % 60.92/61.54 cnf(5640,plain, % 60.92/61.54 (P3(f7(a1,a2,a1),a1,a2)), % 60.92/61.54 inference(scs_inference,[],[50,5607,5603,5605,116,114,63,55,52,87,37,107,98])). % 60.92/61.54 cnf(5642,plain, % 60.92/61.54 (P1(f9(a19,a19,a19))), % 60.92/61.54 inference(scs_inference,[],[50,5607,5603,5605,116,226,114,165,63,55,52,53,87,37,107,98,95])). % 60.92/61.54 cnf(5644,plain, % 60.92/61.54 (P10(a19,a2,f9(a19,a19,a19))), % 60.92/61.54 inference(scs_inference,[],[50,5607,5603,5605,116,226,114,165,63,55,52,53,87,37,107,98,95,100])). % 60.92/61.54 cnf(5647,plain, % 60.92/61.54 (P4(f6(a2,a17),a17,a2)), % 60.92/61.54 inference(scs_inference,[],[50,5607,5603,5605,4266,116,226,114,165,63,57,51,55,52,53,87,37,107,98,95,100,42,79])). % 60.92/61.54 cnf(5653,plain, % 60.92/61.54 (P10(a20,a2,f9(a20,a20,a20))), % 60.92/61.54 inference(scs_inference,[],[50,5607,5603,5605,4266,183,116,226,281,114,165,63,57,51,55,52,53,54,87,37,107,98,95,100,42,79,81,88,99])). % 60.92/61.54 cnf(5661,plain, % 60.92/61.54 (~P10(a17,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[5635,320])). % 60.92/61.54 cnf(5663,plain, % 60.92/61.54 (~P10(a19,a2,f14(a2,a1,a20,a20))), % 60.92/61.54 inference(scs_inference,[],[589,597,87])). % 60.92/61.54 cnf(5671,plain, % 60.92/61.54 (P10(a18,a2,f9(a20,a18,a18))), % 60.92/61.54 inference(scs_inference,[],[50,5640,5647,183,63,589,51,55,52,597,54,87,80,83,84,99])). % 60.92/61.54 cnf(5673,plain, % 60.92/61.54 (P10(a1,a2,f9(a19,a19,a19))), % 60.92/61.54 inference(scs_inference,[],[50,5644,5642,5640,5647,183,163,63,589,51,55,52,597,53,54,87,80,83,84,99,93])). % 60.92/61.54 cnf(5678,plain, % 60.92/61.54 (P1(f9(a17,a17,a17))), % 60.92/61.54 inference(scs_inference,[],[50,5644,5642,5640,5647,197,183,122,163,246,63,589,51,55,52,597,53,54,87,80,83,84,99,93,1731,40,95])). % 60.92/61.54 cnf(5680,plain, % 60.92/61.54 (P10(a17,a2,f9(a19,a17,a17))), % 60.92/61.54 inference(scs_inference,[],[50,5644,5642,5640,5647,197,183,122,163,246,165,62,63,589,51,55,52,597,53,54,87,80,83,84,99,93,1731,40,95,100])). % 60.92/61.54 cnf(5685,plain, % 60.92/61.54 (~P10(a20,a2,f9(a19,a19,a19))), % 60.92/61.54 inference(scs_inference,[],[5644,5642,87])). % 60.92/61.54 cnf(5705,plain, % 60.92/61.54 (~P9(a17,a2,a20)), % 60.92/61.54 inference(scs_inference,[],[5622,5653,51,55,54,87,85])). % 60.92/61.54 cnf(5715,plain, % 60.92/61.54 (~P9(a19,a2,a20)), % 60.92/61.54 inference(scs_inference,[],[5680,5592,5661,55,53,54,37,85])). % 60.92/61.54 cnf(5730,plain, % 60.92/61.54 (~P9(a19,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[5635,5647,1925,55,52,53,40,85])). % 60.92/61.54 cnf(5733,plain, % 60.92/61.54 (~P9(a19,a2,a1)), % 60.92/61.54 inference(scs_inference,[],[50,5715,5601,5635,5647,1925,145,55,52,53,54,40,85,45,92])). % 60.92/61.54 cnf(5740,plain, % 60.92/61.54 (~P10(a17,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[5730,1616])). % 60.92/61.54 cnf(5744,plain, % 60.92/61.54 (~P9(a17,a2,a1)), % 60.92/61.54 inference(scs_inference,[],[50,5733,5705,145,51,55,54,43,92])). % 60.92/61.54 cnf(5757,plain, % 60.92/61.54 (~P9(a17,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[5740,51,55,52,85])). % 60.92/61.54 cnf(5760,plain, % 60.92/61.54 (P4(f6(a2,a18),a18,a2)), % 60.92/61.54 inference(scs_inference,[],[5740,5744,57,51,55,52,85,43,79])). % 60.92/61.54 cnf(5772,plain, % 60.92/61.54 (~P10(a17,a2,a18)), % 60.92/61.54 inference(scs_inference,[],[5757,1621])). % 60.92/61.54 cnf(5780,plain, % 60.92/61.54 (~E(a19,a1)), % 60.92/61.54 inference(scs_inference,[],[5757,5678,5760,5663,55,52,597,53,107,88,44,85,3701])). % 60.92/61.54 cnf(5788,plain, % 60.92/61.54 (~P10(a19,a2,a1)), % 60.92/61.54 inference(scs_inference,[],[50,5772,5780,5613,5733,55,53,37,86])). % 60.92/61.54 cnf(5796,plain, % 60.92/61.54 (~P10(a17,a2,a1)), % 60.92/61.54 inference(scs_inference,[],[5788,252])). % 60.92/61.54 cnf(5797,plain, % 60.92/61.54 (~P10(f14(a2,a1,a19,a19),a2,a1)), % 60.92/61.54 inference(scs_inference,[],[5788,5623])). % 60.92/61.54 cnf(5803,plain, % 60.92/61.54 (~E(a1,f14(a2,a1,a19,a19))), % 60.92/61.54 inference(scs_inference,[],[5797,114,35])). % 60.92/61.54 cnf(5832,plain, % 60.92/61.54 (P1(f9(a19,a17,a17))), % 60.92/61.54 inference(scs_inference,[],[50,5626,5671,5803,5607,5609,165,62,51,55,53,37,86,43,95])). % 60.92/61.54 cnf(5849,plain, % 60.92/61.54 (P4(f6(a2,a19),a19,a2)), % 60.92/61.54 inference(scs_inference,[],[57,55,53,79])). % 60.92/61.54 cnf(5851,plain, % 60.92/61.54 (P1(f6(a2,a19))), % 60.92/61.54 inference(scs_inference,[],[57,55,53,79,81])). % 60.92/61.54 cnf(5855,plain, % 60.92/61.54 (~P10(f9(a19,a17,a17),a2,a1)), % 60.92/61.54 inference(scs_inference,[],[50,5832,5796,5680,57,51,55,53,79,81,83,93])). % 60.92/61.54 cnf(5871,plain, % 60.92/61.54 (~P10(a20,a2,a1)), % 60.92/61.54 inference(scs_inference,[],[50,5851,5673,5855,5849,5685,5642,114,55,53,54,35,107,88,98,93])). % 60.92/61.54 cnf(6359,plain, % 60.92/61.54 (P1(f9(a20,a20,a18))), % 60.92/61.54 inference(scs_inference,[],[52,183,281,63,54,95])). % 60.92/61.54 cnf(6395,plain, % 60.92/61.54 (P10(a20,a2,f9(a20,a20,a18))), % 60.92/61.54 inference(scs_inference,[],[52,6359,183,281,63,55,54,107,100])). % 60.92/61.54 cnf(6424,plain, % 60.92/61.54 (P10(a19,a2,f14(a2,a1,a19,a20))), % 60.92/61.54 inference(scs_inference,[],[53,56,59,58,57,55,50,54,82,106])). % 60.92/61.54 cnf(6431,plain, % 60.92/61.54 (P1(f14(a2,a1,a19,a20))), % 60.92/61.54 inference(scs_inference,[],[53,6395,5871,226,56,165,62,59,58,51,55,50,54,37,100,102])). % 60.92/61.54 cnf(6433,plain, % 60.92/61.54 (~P10(a20,a2,f14(a2,a1,a19,a20))), % 60.92/61.54 inference(scs_inference,[],[53,6395,6424,5871,226,56,165,62,59,58,51,55,50,54,37,100,102,87])). % 60.92/61.54 cnf(6442,plain, % 60.92/61.54 ($false), % 60.92/61.54 inference(scs_inference,[],[53,6431,6433,56,59,58,55,50,54,78,105]), % 60.92/61.54 ['proof']). % 60.92/61.54 % SZS output end Proof % 60.92/61.54 % Total time :60.370000s %------------------------------------------------------------------------------