%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : RNG095+2 : 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 14:01:03 EDT 2024 % Result : Theorem 58.87s 59.00s % Output : CNFRefutation 58.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : RNG095+2 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.32 % Computer : n018.cluster.edu % 0.10/0.32 % Model : x86_64 x86_64 % 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.32 % Memory : 8042.1875MB % 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.32 % CPULimit : 300 % 0.10/0.32 % WCLimit : 300 % 0.10/0.32 % DateTime : Tue Jun 18 13:53:23 EDT 2024 % 0.10/0.32 % CPUTime : % 0.17/0.53 start to proof:theBenchmark % 58.87/58.98 %------------------------------------------- % 58.87/58.98 % File :CSE---1.7 % 58.87/58.98 % Problem :theBenchmark % 58.87/58.98 % Transform :cnf % 58.87/58.98 % Format :tptp:raw % 58.87/58.98 % Command :java -jar mcs_scs.jar %d %s % 58.87/58.98 % 58.87/58.98 % Result :Theorem 58.380000s % 58.87/58.99 % Output :CNFRefutation 58.380000s % 58.87/58.99 %------------------------------------------- % 58.87/58.99 %------------------------------------------------------------------------------ % 58.87/58.99 % File : RNG095+2 : TPTP v8.2.0. Released v4.0.0. % 58.87/58.99 % Domain : Ring Theory % 58.87/58.99 % Problem : Chinese remainder theorem in a ring 05_01, 01 expansion % 58.87/58.99 % Version : Especial. % 58.87/58.99 % English : % 58.87/58.99 % 58.87/58.99 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 58.87/58.99 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 58.87/58.99 % Source : [Pas08] % 58.87/58.99 % Names : chines_05_01.01 [Pas08] % 58.87/58.99 % 58.87/58.99 % Status : Theorem % 58.87/58.99 % Rating : 0.17 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.13 v7.3.0, 0.14 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.12 v6.1.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.29 v5.3.0, 0.33 v5.2.0, 0.20 v5.1.0, 0.29 v5.0.0, 0.33 v4.1.0, 0.43 v4.0.1, 0.74 v4.0.0 % 58.87/58.99 % Syntax : Number of formulae : 31 ( 3 unt; 4 def) % 58.87/58.99 % Number of atoms : 121 ( 26 equ) % 58.87/58.99 % Maximal formula atoms : 14 ( 3 avg) % 58.87/58.99 % Number of connectives : 91 ( 1 ~; 1 |; 45 &) % 58.87/58.99 % ( 6 <=>; 38 =>; 0 <=; 0 <~>) % 58.87/58.99 % Maximal formula depth : 13 ( 5 avg) % 58.87/58.99 % Maximal term depth : 3 ( 1 avg) % 58.87/58.99 % Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty) % 58.87/58.99 % Number of functors : 11 ( 11 usr; 6 con; 0-2 aty) % 58.87/58.99 % Number of variables : 65 ( 59 !; 6 ?) % 58.87/58.99 % SPC : FOF_THM_RFO_SEQ % 58.87/58.99 % 58.87/58.99 % Comments : Problem generated by the SAD system [VLP07] % 58.87/58.99 %------------------------------------------------------------------------------ % 58.87/58.99 fof(mElmSort,axiom, % 58.87/58.99 ! [W0] : % 58.87/58.99 ( aElement0(W0) % 58.87/58.99 => $true ) ). % 58.87/58.99 % 58.87/59.00 fof(mSortsC,axiom, % 58.87/59.00 aElement0(sz00) ). % 58.87/59.00 % 58.87/59.00 fof(mSortsC_01,axiom, % 58.87/59.00 aElement0(sz10) ). % 58.87/59.00 % 58.87/59.00 fof(mSortsU,axiom, % 58.87/59.00 ! [W0] : % 58.87/59.00 ( aElement0(W0) % 58.87/59.00 => aElement0(smndt0(W0)) ) ). % 58.87/59.00 % 58.87/59.00 fof(mSortsB,axiom, % 58.87/59.00 ! [W0,W1] : % 58.87/59.00 ( ( aElement0(W0) % 58.87/59.00 & aElement0(W1) ) % 58.87/59.00 => aElement0(sdtpldt0(W0,W1)) ) ). % 58.87/59.00 % 58.87/59.00 fof(mSortsB_02,axiom, % 58.87/59.00 ! [W0,W1] : % 58.87/59.00 ( ( aElement0(W0) % 58.87/59.00 & aElement0(W1) ) % 58.87/59.00 => aElement0(sdtasdt0(W0,W1)) ) ). % 58.87/59.00 % 58.87/59.00 fof(mAddComm,axiom, % 58.87/59.00 ! [W0,W1] : % 58.87/59.00 ( ( aElement0(W0) % 58.87/59.00 & aElement0(W1) ) % 58.87/59.00 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 58.87/59.00 % 58.87/59.00 fof(mAddAsso,axiom, % 58.87/59.00 ! [W0,W1,W2] : % 58.87/59.00 ( ( aElement0(W0) % 58.87/59.00 & aElement0(W1) % 58.87/59.00 & aElement0(W2) ) % 58.87/59.00 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 58.87/59.00 % 58.87/59.00 fof(mAddZero,axiom, % 58.87/59.00 ! [W0] : % 58.87/59.00 ( aElement0(W0) % 58.87/59.00 => ( sdtpldt0(W0,sz00) = W0 % 58.87/59.00 & W0 = sdtpldt0(sz00,W0) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mAddInvr,axiom, % 58.87/59.00 ! [W0] : % 58.87/59.00 ( aElement0(W0) % 58.87/59.00 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 58.87/59.00 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mMulComm,axiom, % 58.87/59.00 ! [W0,W1] : % 58.87/59.00 ( ( aElement0(W0) % 58.87/59.00 & aElement0(W1) ) % 58.87/59.00 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 58.87/59.00 % 58.87/59.00 fof(mMulAsso,axiom, % 58.87/59.00 ! [W0,W1,W2] : % 58.87/59.00 ( ( aElement0(W0) % 58.87/59.00 & aElement0(W1) % 58.87/59.00 & aElement0(W2) ) % 58.87/59.00 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 58.87/59.00 % 58.87/59.00 fof(mMulUnit,axiom, % 58.87/59.00 ! [W0] : % 58.87/59.00 ( aElement0(W0) % 58.87/59.00 => ( sdtasdt0(W0,sz10) = W0 % 58.87/59.00 & W0 = sdtasdt0(sz10,W0) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mAMDistr,axiom, % 58.87/59.00 ! [W0,W1,W2] : % 58.87/59.00 ( ( aElement0(W0) % 58.87/59.00 & aElement0(W1) % 58.87/59.00 & aElement0(W2) ) % 58.87/59.00 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 58.87/59.00 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mMulMnOne,axiom, % 58.87/59.00 ! [W0] : % 58.87/59.00 ( aElement0(W0) % 58.87/59.00 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 58.87/59.00 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mMulZero,axiom, % 58.87/59.00 ! [W0] : % 58.87/59.00 ( aElement0(W0) % 58.87/59.00 => ( sdtasdt0(W0,sz00) = sz00 % 58.87/59.00 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mCancel,axiom, % 58.87/59.00 ! [W0,W1] : % 58.87/59.00 ( ( aElement0(W0) % 58.87/59.00 & aElement0(W1) ) % 58.87/59.00 => ( sdtasdt0(W0,W1) = sz00 % 58.87/59.00 => ( W0 = sz00 % 58.87/59.00 | W1 = sz00 ) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mUnNeZr,axiom, % 58.87/59.00 sz10 != sz00 ). % 58.87/59.00 % 58.87/59.00 fof(mSetSort,axiom, % 58.87/59.00 ! [W0] : % 58.87/59.00 ( aSet0(W0) % 58.87/59.00 => $true ) ). % 58.87/59.00 % 58.87/59.00 fof(mEOfElem,axiom, % 58.87/59.00 ! [W0] : % 58.87/59.00 ( aSet0(W0) % 58.87/59.00 => ! [W1] : % 58.87/59.00 ( aElementOf0(W1,W0) % 58.87/59.00 => aElement0(W1) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mSetEq,axiom, % 58.87/59.00 ! [W0,W1] : % 58.87/59.00 ( ( aSet0(W0) % 58.87/59.00 & aSet0(W1) ) % 58.87/59.00 => ( ( ! [W2] : % 58.87/59.00 ( aElementOf0(W2,W0) % 58.87/59.00 => aElementOf0(W2,W1) ) % 58.87/59.00 & ! [W2] : % 58.87/59.00 ( aElementOf0(W2,W1) % 58.87/59.00 => aElementOf0(W2,W0) ) ) % 58.87/59.00 => W0 = W1 ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mDefSSum,definition, % 58.87/59.00 ! [W0,W1] : % 58.87/59.00 ( ( aSet0(W0) % 58.87/59.00 & aSet0(W1) ) % 58.87/59.00 => ! [W2] : % 58.87/59.00 ( W2 = sdtpldt1(W0,W1) % 58.87/59.00 <=> ( aSet0(W2) % 58.87/59.00 & ! [W3] : % 58.87/59.00 ( aElementOf0(W3,W2) % 58.87/59.00 <=> ? [W4,W5] : % 58.87/59.00 ( aElementOf0(W4,W0) % 58.87/59.00 & aElementOf0(W5,W1) % 58.87/59.00 & sdtpldt0(W4,W5) = W3 ) ) ) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mDefSInt,definition, % 58.87/59.00 ! [W0,W1] : % 58.87/59.00 ( ( aSet0(W0) % 58.87/59.00 & aSet0(W1) ) % 58.87/59.00 => ! [W2] : % 58.87/59.00 ( W2 = sdtasasdt0(W0,W1) % 58.87/59.00 <=> ( aSet0(W2) % 58.87/59.00 & ! [W3] : % 58.87/59.00 ( aElementOf0(W3,W2) % 58.87/59.00 <=> ( aElementOf0(W3,W0) % 58.87/59.00 & aElementOf0(W3,W1) ) ) ) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mDefIdeal,definition, % 58.87/59.00 ! [W0] : % 58.87/59.00 ( aIdeal0(W0) % 58.87/59.00 <=> ( aSet0(W0) % 58.87/59.00 & ! [W1] : % 58.87/59.00 ( aElementOf0(W1,W0) % 58.87/59.00 => ( ! [W2] : % 58.87/59.00 ( aElementOf0(W2,W0) % 58.87/59.00 => aElementOf0(sdtpldt0(W1,W2),W0) ) % 58.87/59.00 & ! [W2] : % 58.87/59.00 ( aElement0(W2) % 58.87/59.00 => aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(mIdeSum,axiom, % 58.87/59.00 ! [W0,W1] : % 58.87/59.00 ( ( aIdeal0(W0) % 58.87/59.00 & aIdeal0(W1) ) % 58.87/59.00 => aIdeal0(sdtpldt1(W0,W1)) ) ). % 58.87/59.00 % 58.87/59.00 fof(mIdeInt,axiom, % 58.87/59.00 ! [W0,W1] : % 58.87/59.00 ( ( aIdeal0(W0) % 58.87/59.00 & aIdeal0(W1) ) % 58.87/59.00 => aIdeal0(sdtasasdt0(W0,W1)) ) ). % 58.87/59.00 % 58.87/59.00 fof(mDefMod,definition, % 58.87/59.00 ! [W0,W1,W2] : % 58.87/59.00 ( ( aElement0(W0) % 58.87/59.00 & aElement0(W1) % 58.87/59.00 & aIdeal0(W2) ) % 58.87/59.00 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 58.87/59.00 <=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(m__1205,hypothesis, % 58.87/59.00 ( aSet0(xI) % 58.87/59.00 & ! [W0] : % 58.87/59.00 ( aElementOf0(W0,xI) % 58.87/59.00 => ( ! [W1] : % 58.87/59.00 ( aElementOf0(W1,xI) % 58.87/59.00 => aElementOf0(sdtpldt0(W0,W1),xI) ) % 58.87/59.00 & ! [W1] : % 58.87/59.00 ( aElement0(W1) % 58.87/59.00 => aElementOf0(sdtasdt0(W1,W0),xI) ) ) ) % 58.87/59.00 & aIdeal0(xI) % 58.87/59.00 & aSet0(xJ) % 58.87/59.00 & ! [W0] : % 58.87/59.00 ( aElementOf0(W0,xJ) % 58.87/59.00 => ( ! [W1] : % 58.87/59.00 ( aElementOf0(W1,xJ) % 58.87/59.00 => aElementOf0(sdtpldt0(W0,W1),xJ) ) % 58.87/59.00 & ! [W1] : % 58.87/59.00 ( aElement0(W1) % 58.87/59.00 => aElementOf0(sdtasdt0(W1,W0),xJ) ) ) ) % 58.87/59.00 & aIdeal0(xJ) ) ). % 58.87/59.00 % 58.87/59.00 fof(m__1205_03,hypothesis, % 58.87/59.00 ! [W0] : % 58.87/59.00 ( aElement0(W0) % 58.87/59.00 => ( ? [W1,W2] : % 58.87/59.00 ( aElementOf0(W1,xI) % 58.87/59.00 & aElementOf0(W2,xJ) % 58.87/59.00 & sdtpldt0(W1,W2) = W0 ) % 58.87/59.00 & aElementOf0(W0,sdtpldt1(xI,xJ)) ) ) ). % 58.87/59.00 % 58.87/59.00 fof(m__1217,hypothesis, % 58.87/59.00 ( aElement0(xx) % 58.87/59.00 & aElement0(xy) ) ). % 58.87/59.00 % 58.87/59.00 fof(m__,conjecture, % 58.87/59.00 ? [W0,W1] : % 58.87/59.00 ( aElementOf0(W0,xI) % 58.87/59.00 & aElementOf0(W1,xJ) % 58.87/59.00 & sdtpldt0(W0,W1) = sz10 ) ). % 58.87/59.00 % 58.87/59.00 %------------------------------------------------------------------------------ % 58.87/59.00 %------------------------------------------- % 58.87/59.00 % Proof found % 58.87/59.00 % SZS status Theorem for theBenchmark % 58.87/59.00 % SZS output start Proof % 58.87/59.00 %ClaNum:120(EqnAxiom:49) % 58.87/59.00 %VarNum:448(SingletonVarNum:138) % 58.87/59.00 %MaxLitNum:8 % 58.87/59.00 %MaxfuncDepth:2 % 58.87/59.00 %SharedTerms:17 % 58.87/59.00 %goalClause: 87 % 58.87/59.00 [50]P1(a1) % 58.87/59.00 [51]P1(a20) % 58.87/59.00 [52]P1(a21) % 58.87/59.00 [53]P1(a24) % 58.87/59.00 [54]P2(a22) % 58.87/59.00 [55]P2(a23) % 58.87/59.00 [56]P3(a22) % 58.87/59.00 [57]P3(a23) % 58.87/59.00 [58]~E(a1,a20) % 58.87/59.00 [59]~P3(x591)+P2(x591) % 58.87/59.00 [60]~P1(x601)+P1(f2(x601)) % 58.87/59.00 [61]~P1(x611)+E(f3(a1,x611),a1) % 58.87/59.00 [62]~P1(x621)+E(f3(x621,a1),a1) % 58.87/59.00 [63]~P1(x631)+E(f18(a1,x631),x631) % 58.87/59.00 [64]~P1(x641)+E(f3(a20,x641),x641) % 58.87/59.00 [65]~P1(x651)+E(f18(x651,a1),x651) % 58.87/59.00 [66]~P1(x661)+E(f3(x661,a20),x661) % 58.87/59.00 [67]~P1(x671)+P4(f4(x671),a22) % 58.87/59.00 [68]~P1(x681)+P4(f7(x681),a23) % 58.87/59.00 [77]~P1(x771)+P4(x771,f19(a22,a23)) % 58.87/59.00 [69]~P1(x691)+E(f18(f2(x691),x691),a1) % 58.87/59.00 [70]~P1(x701)+E(f18(x701,f2(x701)),a1) % 58.87/59.00 [71]~P1(x711)+E(f3(x711,f2(a20)),f2(x711)) % 58.87/59.00 [72]~P1(x721)+E(f3(f2(a20),x721),f2(x721)) % 58.87/59.00 [75]~P1(x751)+E(f18(f4(x751),f7(x751)),x751) % 58.87/59.00 [73]~P2(x731)+P3(x731)+P4(f8(x731),x731) % 58.87/59.00 [74]~P4(x741,x742)+P1(x741)+~P2(x742) % 58.87/59.00 [78]~P1(x782)+~P1(x781)+E(f18(x781,x782),f18(x782,x781)) % 58.87/59.00 [79]~P1(x792)+~P1(x791)+E(f3(x791,x792),f3(x792,x791)) % 58.87/59.00 [83]~P1(x832)+~P1(x831)+P1(f18(x831,x832)) % 58.87/59.00 [84]~P1(x842)+~P1(x841)+P1(f3(x841,x842)) % 58.87/59.00 [85]~P3(x852)+~P3(x851)+P3(f19(x851,x852)) % 58.87/59.00 [86]~P3(x862)+~P3(x861)+P3(f17(x861,x862)) % 58.87/59.00 [87]~P4(x872,a23)+~P4(x871,a22)+~E(f18(x871,x872),a20) % 58.87/59.00 [88]~P1(x881)+~P4(x882,a22)+P4(f3(x881,x882),a22) % 58.87/59.00 [89]~P1(x891)+~P4(x892,a23)+P4(f3(x891,x892),a23) % 58.87/59.00 [93]~P4(x931,a22)+~P4(x932,a22)+P4(f18(x931,x932),a22) % 58.87/59.00 [94]~P4(x941,a23)+~P4(x942,a23)+P4(f18(x941,x942),a23) % 58.87/59.00 [82]~P2(x821)+P3(x821)+P4(f6(x821),x821)+P1(f5(x821)) % 58.87/59.00 [103]~P2(x1031)+P3(x1031)+P1(f5(x1031))+~P4(f18(f8(x1031),f6(x1031)),x1031) % 58.87/59.00 [106]~P2(x1061)+P3(x1061)+P4(f6(x1061),x1061)+~P4(f3(f5(x1061),f8(x1061)),x1061) % 58.87/59.00 [110]~P2(x1101)+P3(x1101)+~P4(f18(f8(x1101),f6(x1101)),x1101)+~P4(f3(f5(x1101),f8(x1101)),x1101) % 58.87/59.00 [80]~P2(x803)+~P2(x802)+P2(x801)+~E(x801,f19(x802,x803)) % 58.87/59.00 [81]~P2(x813)+~P2(x812)+P2(x811)+~E(x811,f17(x812,x813)) % 58.87/59.00 [92]~P1(x921)+~P3(x923)+~P4(x922,x923)+P4(f3(x921,x922),x923) % 58.87/59.00 [95]~P3(x953)+~P4(x951,x953)+~P4(x952,x953)+P4(f18(x951,x952),x953) % 58.87/59.00 [98]~P1(x983)+~P1(x982)+~P1(x981)+E(f18(f18(x981,x982),x983),f18(x981,f18(x982,x983))) % 58.87/59.00 [99]~P1(x993)+~P1(x992)+~P1(x991)+E(f3(f3(x991,x992),x993),f3(x991,f3(x992,x993))) % 58.87/59.00 [104]~P1(x1043)+~P1(x1042)+~P1(x1041)+E(f18(f3(x1041,x1042),f3(x1041,x1043)),f3(x1041,f18(x1042,x1043))) % 58.87/59.00 [105]~P1(x1052)+~P1(x1053)+~P1(x1051)+E(f18(f3(x1051,x1052),f3(x1053,x1052)),f3(f18(x1051,x1053),x1052)) % 58.87/59.00 [76]~P1(x761)+~P1(x762)+E(x761,a1)+E(x762,a1)+~E(f3(x762,x761),a1) % 58.87/59.00 [96]~P2(x962)+~P2(x961)+E(x961,x962)+P4(f9(x961,x962),x961)+P4(f10(x961,x962),x962) % 58.87/59.00 [100]~P2(x1002)+~P2(x1001)+E(x1001,x1002)+P4(f9(x1001,x1002),x1001)+~P4(f10(x1001,x1002),x1001) % 58.87/59.00 [101]~P2(x1012)+~P2(x1011)+E(x1011,x1012)+P4(f10(x1011,x1012),x1012)+~P4(f9(x1011,x1012),x1012) % 58.87/59.00 [107]~P2(x1072)+~P2(x1071)+E(x1071,x1072)+~P4(f9(x1071,x1072),x1072)+~P4(f10(x1071,x1072),x1071) % 58.87/59.00 [108]~P1(x1082)+~P1(x1081)+~P3(x1083)+P5(x1081,x1082,x1083)+~P4(f18(x1081,f2(x1082)),x1083) % 58.87/59.00 [109]~P1(x1092)+~P1(x1091)+~P3(x1093)+~P5(x1091,x1092,x1093)+P4(f18(x1091,f2(x1092)),x1093) % 58.87/59.00 [90]~P2(x904)+~P2(x902)+~P4(x901,x903)+P4(x901,x902)+~E(x903,f17(x904,x902)) % 58.87/59.00 [91]~P2(x914)+~P2(x912)+~P4(x911,x913)+P4(x911,x912)+~E(x913,f17(x912,x914)) % 58.87/59.00 [117]~P2(x1172)+~P2(x1171)+~P4(x1174,x1173)+~E(x1173,f19(x1171,x1172))+P4(f12(x1171,x1172,x1173,x1174),x1171) % 58.87/59.00 [118]~P2(x1182)+~P2(x1181)+~P4(x1184,x1183)+~E(x1183,f19(x1181,x1182))+P4(f13(x1181,x1182,x1183,x1184),x1182) % 58.87/59.00 [120]~P2(x1202)+~P2(x1201)+~P4(x1204,x1203)+~E(x1203,f19(x1201,x1202))+E(f18(f12(x1201,x1202,x1203,x1204),f13(x1201,x1202,x1203,x1204)),x1204) % 58.87/59.00 [111]~P2(x1111)+~P2(x1113)+~P2(x1112)+P4(f11(x1112,x1113,x1111),x1111)+P4(f14(x1112,x1113,x1111),x1112)+E(x1111,f19(x1112,x1113)) % 58.87/59.00 [112]~P2(x1121)+~P2(x1123)+~P2(x1122)+P4(f11(x1122,x1123,x1121),x1121)+P4(f15(x1122,x1123,x1121),x1123)+E(x1121,f19(x1122,x1123)) % 58.87/59.00 [113]~P2(x1131)+~P2(x1133)+~P2(x1132)+P4(f16(x1132,x1133,x1131),x1131)+P4(f16(x1132,x1133,x1131),x1133)+E(x1131,f17(x1132,x1133)) % 58.87/59.00 [114]~P2(x1141)+~P2(x1143)+~P2(x1142)+P4(f16(x1142,x1143,x1141),x1141)+P4(f16(x1142,x1143,x1141),x1142)+E(x1141,f17(x1142,x1143)) % 58.87/59.00 [116]~P2(x1161)+~P2(x1163)+~P2(x1162)+P4(f11(x1162,x1163,x1161),x1161)+E(x1161,f19(x1162,x1163))+E(f18(f14(x1162,x1163,x1161),f15(x1162,x1163,x1161)),f11(x1162,x1163,x1161)) % 58.87/59.00 [97]~P2(x974)+~P2(x973)+~P4(x971,x974)+~P4(x971,x973)+P4(x971,x972)+~E(x972,f17(x973,x974)) % 58.87/59.00 [119]~P2(x1191)+~P2(x1193)+~P2(x1192)+~P4(f16(x1192,x1193,x1191),x1191)+~P4(f16(x1192,x1193,x1191),x1193)+~P4(f16(x1192,x1193,x1191),x1192)+E(x1191,f17(x1192,x1193)) % 58.87/59.00 [102]~P2(x1024)+~P2(x1023)+~P4(x1026,x1024)+~P4(x1025,x1023)+P4(x1021,x1022)+~E(x1022,f19(x1023,x1024))+~E(f18(x1025,x1026),x1021) % 58.87/59.00 [115]~P2(x1151)+~P2(x1153)+~P2(x1152)+~P4(x1155,x1153)+~P4(x1154,x1152)+~P4(f11(x1152,x1153,x1151),x1151)+E(x1151,f19(x1152,x1153))+~E(f18(x1154,x1155),f11(x1152,x1153,x1151)) % 58.87/59.00 %EqnAxiom % 58.87/59.00 [1]E(x11,x11) % 58.87/59.00 [2]E(x22,x21)+~E(x21,x22) % 58.87/59.00 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.87/59.00 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 58.87/59.00 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53)) % 58.87/59.00 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62)) % 58.87/59.00 [7]~E(x71,x72)+E(f19(x71,x73),f19(x72,x73)) % 58.87/59.00 [8]~E(x81,x82)+E(f19(x83,x81),f19(x83,x82)) % 58.87/59.00 [9]~E(x91,x92)+E(f18(x91,x93),f18(x92,x93)) % 58.87/59.00 [10]~E(x101,x102)+E(f18(x103,x101),f18(x103,x102)) % 58.87/59.00 [11]~E(x111,x112)+E(f13(x111,x113,x114,x115),f13(x112,x113,x114,x115)) % 58.87/59.00 [12]~E(x121,x122)+E(f13(x123,x121,x124,x125),f13(x123,x122,x124,x125)) % 58.87/59.00 [13]~E(x131,x132)+E(f13(x133,x134,x131,x135),f13(x133,x134,x132,x135)) % 58.87/59.00 [14]~E(x141,x142)+E(f13(x143,x144,x145,x141),f13(x143,x144,x145,x142)) % 58.87/59.00 [15]~E(x151,x152)+E(f16(x151,x153,x154),f16(x152,x153,x154)) % 58.87/59.00 [16]~E(x161,x162)+E(f16(x163,x161,x164),f16(x163,x162,x164)) % 58.87/59.00 [17]~E(x171,x172)+E(f16(x173,x174,x171),f16(x173,x174,x172)) % 58.87/59.00 [18]~E(x181,x182)+E(f11(x181,x183,x184),f11(x182,x183,x184)) % 58.87/59.00 [19]~E(x191,x192)+E(f11(x193,x191,x194),f11(x193,x192,x194)) % 58.87/59.00 [20]~E(x201,x202)+E(f11(x203,x204,x201),f11(x203,x204,x202)) % 58.87/59.00 [21]~E(x211,x212)+E(f4(x211),f4(x212)) % 58.87/59.00 [22]~E(x221,x222)+E(f7(x221),f7(x222)) % 58.87/59.00 [23]~E(x231,x232)+E(f14(x231,x233,x234),f14(x232,x233,x234)) % 58.87/59.00 [24]~E(x241,x242)+E(f14(x243,x241,x244),f14(x243,x242,x244)) % 58.87/59.00 [25]~E(x251,x252)+E(f14(x253,x254,x251),f14(x253,x254,x252)) % 58.87/59.00 [26]~E(x261,x262)+E(f10(x261,x263),f10(x262,x263)) % 58.87/59.00 [27]~E(x271,x272)+E(f10(x273,x271),f10(x273,x272)) % 58.87/59.00 [28]~E(x281,x282)+E(f9(x281,x283),f9(x282,x283)) % 58.87/59.00 [29]~E(x291,x292)+E(f9(x293,x291),f9(x293,x292)) % 58.87/59.00 [30]~E(x301,x302)+E(f17(x301,x303),f17(x302,x303)) % 58.87/59.00 [31]~E(x311,x312)+E(f17(x313,x311),f17(x313,x312)) % 58.87/59.00 [32]~E(x321,x322)+E(f15(x321,x323,x324),f15(x322,x323,x324)) % 58.87/59.00 [33]~E(x331,x332)+E(f15(x333,x331,x334),f15(x333,x332,x334)) % 58.87/59.01 [34]~E(x341,x342)+E(f15(x343,x344,x341),f15(x343,x344,x342)) % 58.87/59.01 [35]~E(x351,x352)+E(f12(x351,x353,x354,x355),f12(x352,x353,x354,x355)) % 58.87/59.01 [36]~E(x361,x362)+E(f12(x363,x361,x364,x365),f12(x363,x362,x364,x365)) % 58.87/59.01 [37]~E(x371,x372)+E(f12(x373,x374,x371,x375),f12(x373,x374,x372,x375)) % 58.87/59.01 [38]~E(x381,x382)+E(f12(x383,x384,x385,x381),f12(x383,x384,x385,x382)) % 58.87/59.01 [39]~E(x391,x392)+E(f5(x391),f5(x392)) % 58.87/59.01 [40]~E(x401,x402)+E(f8(x401),f8(x402)) % 58.87/59.01 [41]~E(x411,x412)+E(f6(x411),f6(x412)) % 58.87/59.01 [42]~P1(x421)+P1(x422)+~E(x421,x422) % 58.87/59.01 [43]P4(x432,x433)+~E(x431,x432)+~P4(x431,x433) % 58.87/59.01 [44]P4(x443,x442)+~E(x441,x442)+~P4(x443,x441) % 58.87/59.01 [45]~P2(x451)+P2(x452)+~E(x451,x452) % 58.87/59.01 [46]~P3(x461)+P3(x462)+~E(x461,x462) % 58.87/59.01 [47]P5(x472,x473,x474)+~E(x471,x472)+~P5(x471,x473,x474) % 58.87/59.01 [48]P5(x483,x482,x484)+~E(x481,x482)+~P5(x483,x481,x484) % 58.87/59.01 [49]P5(x493,x494,x492)+~E(x491,x492)+~P5(x493,x494,x491) % 58.87/59.01 % 58.87/59.01 %------------------------------------------- % 58.93/59.01 cnf(123,plain, % 58.93/59.01 (P4(x1231,x1232)+~P2(x1233)+~P2(x1232)+~P4(x1231,f17(x1233,x1232))), % 58.93/59.01 inference(equality_inference,[],[90])). % 58.93/59.01 cnf(125,plain, % 58.93/59.01 (~P4(x1251,x1252)+~P2(x1253)+~P4(x1251,x1253)+~P2(x1252)+P4(x1251,f17(x1252,x1253))), % 58.93/59.01 inference(equality_inference,[],[97])). % 58.93/59.01 cnf(126,plain, % 58.93/59.01 (~P2(x1261)+~P2(x1262)+~P4(x1263,f19(x1262,x1261))+P4(f12(x1262,x1261,f19(x1262,x1261),x1263),x1262)), % 58.93/59.01 inference(equality_inference,[],[117])). % 58.93/59.01 cnf(127,plain, % 58.93/59.01 (~P2(x1271)+~P2(x1272)+~P4(x1273,f19(x1272,x1271))+P4(f13(x1272,x1271,f19(x1272,x1271),x1273),x1271)), % 58.93/59.01 inference(equality_inference,[],[118])). % 58.93/59.01 cnf(129,plain, % 58.93/59.01 (~P4(x1291,f17(a22,a22))+P4(x1291,a22)), % 58.93/59.01 inference(scs_inference,[],[54,123])). % 58.93/59.01 cnf(140,plain, % 58.93/59.01 (E(a1,f3(a1,a21))), % 58.93/59.01 inference(scs_inference,[],[52,2,61])). % 58.93/59.01 cnf(141,plain, % 58.93/59.01 (E(f3(a1,a21),a1)), % 58.93/59.01 inference(scs_inference,[],[140,2])). % 58.93/59.01 cnf(142,plain, % 58.93/59.01 (P1(f3(a1,a21))), % 58.93/59.01 inference(scs_inference,[],[140,50,2,42])). % 58.93/59.01 cnf(147,plain, % 58.93/59.01 (P4(f4(f2(a21)),a22)), % 58.93/59.01 inference(scs_inference,[],[52,67,60])). % 58.93/59.01 cnf(197,plain, % 58.93/59.01 (P4(f4(f2(a21)),f17(a22,a22))), % 58.93/59.01 inference(scs_inference,[],[54,147,125])). % 58.93/59.01 cnf(379,plain, % 58.93/59.01 (P4(f2(a1),f19(a22,a23))), % 58.93/59.01 inference(scs_inference,[],[50,77,60])). % 58.93/59.01 cnf(401,plain, % 58.93/59.01 (E(f2(f3(a1,a21)),f2(a1))), % 58.93/59.01 inference(scs_inference,[],[140,4,2])). % 58.93/59.02 cnf(407,plain, % 58.93/59.02 (~P1(f2(f3(a1,a21)))+P1(f2(a1))), % 58.93/59.02 inference(scs_inference,[],[379,401,2,43,46,45,44,42])). % 58.93/59.02 cnf(557,plain, % 58.93/59.02 (~P3(f17(a22,a22))+P4(f3(a24,f4(f2(a21))),a22)), % 58.93/59.02 inference(scs_inference,[],[53,197,129,92])). % 58.93/59.02 cnf(1173,plain, % 58.93/59.02 (P4(f3(a24,f4(f2(a21))),a22)), % 58.93/59.02 inference(scs_inference,[],[56,557,86])). % 58.93/59.02 cnf(3849,plain, % 58.93/59.02 (~E(a20,a1)), % 58.93/59.02 inference(scs_inference,[],[1173,54,58,74,2])). % 58.93/59.02 cnf(4699,plain, % 58.93/59.02 (P4(f13(a22,a23,f19(a22,a23),f2(a1)),a23)), % 58.93/59.02 inference(scs_inference,[],[57,379,54,59,127])). % 58.93/59.02 cnf(4764,plain, % 58.93/59.02 (P4(f12(a22,a23,f19(a22,a23),f2(a1)),a22)), % 58.93/59.02 inference(scs_inference,[],[57,379,54,59,126])). % 58.93/59.02 cnf(4853,plain, % 58.93/59.02 (P1(f2(f3(a1,a21)))), % 58.93/59.02 inference(scs_inference,[],[140,50,60,42])). % 58.93/59.02 cnf(4854,plain, % 58.93/59.02 (P1(f2(a1))), % 58.93/59.02 inference(scs_inference,[],[4853,407])). % 58.93/59.02 cnf(4858,plain, % 58.93/59.02 (E(f18(a1,f2(a1)),f2(a1))), % 58.93/59.02 inference(scs_inference,[],[50,60,63])). % 58.93/59.02 cnf(5209,plain, % 58.93/59.02 (E(f3(a1,f2(a1)),a1)), % 58.93/59.02 inference(scs_inference,[],[50,60,61])). % 58.93/59.02 cnf(5342,plain, % 58.93/59.02 (~E(a20,f3(a1,f2(a1)))), % 58.93/59.02 inference(scs_inference,[],[5209,3849,3])). % 58.93/59.02 cnf(5347,plain, % 58.93/59.02 (~P1(f3(a1,f2(a1)))+~E(a20,f18(a1,f3(a1,f2(a1))))), % 58.93/59.02 inference(scs_inference,[],[5342,3,63])). % 58.93/59.02 cnf(5424,plain, % 58.93/59.02 (~E(f18(a1,f3(a1,f2(a1))),a20)+~P1(f3(a1,f2(a1)))), % 58.93/59.02 inference(scs_inference,[],[5347,2])). % 58.93/59.02 cnf(5444,plain, % 58.93/59.02 (~E(f18(a1,f3(a1,f2(a1))),a20)), % 58.93/59.02 inference(scs_inference,[],[4854,50,5424,84])). % 58.93/59.02 cnf(5454,plain, % 58.93/59.02 (~E(x54541,a20)+~E(f18(a1,f3(a1,f2(a1))),x54541)), % 58.93/59.02 inference(scs_inference,[],[5444,3])). % 58.93/59.02 cnf(5466,plain, % 58.93/59.02 (~E(f18(a1,a1),a20)), % 58.93/59.02 inference(scs_inference,[],[5209,5454,10])). % 58.93/59.02 cnf(5467,plain, % 58.93/59.02 (~E(a20,f18(a1,a1))), % 58.93/59.02 inference(scs_inference,[],[5466,2])). % 58.93/59.02 cnf(5471,plain, % 58.93/59.02 (~E(x54711,f18(a1,a1))+~E(a20,x54711)), % 58.93/59.02 inference(scs_inference,[],[5467,3])). % 58.93/59.02 cnf(5472,plain, % 58.93/59.02 (~P1(f18(a1,a1))+~E(a20,f3(f18(a1,a1),a20))), % 58.93/59.02 inference(scs_inference,[],[5467,3,66])). % 58.93/59.02 cnf(5542,plain, % 58.93/59.02 (~E(f3(f18(a1,a1),a20),a20)+~P1(f18(a1,a1))), % 58.93/59.02 inference(scs_inference,[],[5472,2])). % 58.93/59.02 cnf(5543,plain, % 58.93/59.02 (~E(f3(f18(a1,a1),a20),a20)), % 58.93/59.02 inference(scs_inference,[],[50,5542,83])). % 58.93/59.02 cnf(5545,plain, % 58.93/59.02 (~E(x55451,a20)+~E(f3(f18(a1,a1),a20),x55451)), % 58.93/59.02 inference(scs_inference,[],[5543,2,3])). % 58.93/59.02 cnf(5548,plain, % 58.93/59.02 (~E(f18(a1,a1),x55481)+~E(f3(x55481,a20),a20)), % 58.93/59.02 inference(scs_inference,[],[5545,5])). % 58.93/59.02 cnf(5554,plain, % 58.93/59.02 (~E(f3(a1,a20),a20)), % 58.93/59.02 inference(scs_inference,[],[50,5548,63])). % 58.93/59.02 cnf(5555,plain, % 58.93/59.02 (~E(a20,f3(a1,a20))), % 58.93/59.02 inference(scs_inference,[],[5554,2])). % 58.93/59.02 cnf(5556,plain, % 58.93/59.02 (~E(x55561,a20)+~E(f3(a1,a20),x55561)), % 58.93/59.02 inference(scs_inference,[],[5554,2,3])). % 58.93/59.02 cnf(5559,plain, % 58.93/59.02 (~E(f3(f3(a1,a21),a20),a20)), % 58.93/59.02 inference(scs_inference,[],[140,5556,5])). % 58.93/59.02 cnf(5562,plain, % 58.93/59.02 (~P1(f3(a1,a20))+~E(a20,f18(f3(a1,a20),a1))), % 58.93/59.02 inference(scs_inference,[],[5555,5559,2,3,65])). % 58.93/59.02 cnf(5571,plain, % 58.93/59.02 (~E(x55711,a20)+~E(f3(f3(a1,a21),a20),x55711)), % 58.93/59.02 inference(scs_inference,[],[5559,3])). % 58.93/59.02 cnf(5633,plain, % 58.93/59.02 (~E(f3(a1,f3(a21,a20)),a20)), % 58.93/59.02 inference(scs_inference,[],[51,52,50,5571,99])). % 58.93/59.02 cnf(5635,plain, % 58.93/59.02 (~E(x56351,a20)+~E(f3(a1,f3(a21,a20)),x56351)), % 58.93/59.02 inference(scs_inference,[],[5633,2,3])). % 58.93/59.02 cnf(5672,plain, % 58.93/59.02 (~E(f3(f3(a1,a21),f3(a21,a20)),a20)), % 58.93/59.02 inference(scs_inference,[],[140,5635,5])). % 58.93/59.02 cnf(5673,plain, % 58.93/59.02 (~E(a20,f3(f3(a1,a21),f3(a21,a20)))), % 58.93/59.02 inference(scs_inference,[],[5672,2])). % 58.93/59.02 cnf(5678,plain, % 58.93/59.02 (~E(x56781,f3(f3(a1,a21),f3(a21,a20)))+~E(a20,x56781)), % 58.93/59.02 inference(scs_inference,[],[5673,3])). % 58.93/59.02 cnf(5704,plain, % 58.93/59.02 (~E(a20,f18(f3(a1,a20),a1))), % 58.93/59.02 inference(scs_inference,[],[51,50,5562,84])). % 58.93/59.02 cnf(5705,plain, % 58.93/59.02 (~E(f18(f3(a1,a20),a1),a20)), % 58.93/59.02 inference(scs_inference,[],[5704,2])). % 58.93/59.02 cnf(5707,plain, % 58.93/59.02 (~E(x57071,f3(a1,a20))+~E(a20,f18(x57071,a1))), % 58.93/59.02 inference(scs_inference,[],[5704,2,3,9])). % 58.93/59.02 cnf(5723,plain, % 58.93/59.02 (~E(x57231,a20)+~E(f18(f3(a1,a20),a1),x57231)), % 58.93/59.02 inference(scs_inference,[],[5705,3])). % 58.93/59.02 cnf(5738,plain, % 58.93/59.02 (~E(a20,f18(f3(f3(a1,a21),a20),a1))), % 58.93/59.02 inference(scs_inference,[],[141,5707,5])). % 58.93/59.02 cnf(5750,plain, % 58.93/59.02 (~E(x57501,a20)+~E(a20,f18(f3(f3(a1,a21),x57501),a1))), % 58.93/59.02 inference(scs_inference,[],[5738,3,9,6])). % 58.93/59.02 cnf(5754,plain, % 58.93/59.02 (~E(x57541,f18(f3(a1,a20),a1))+~E(x57541,a20)), % 58.93/59.02 inference(scs_inference,[],[5723,2])). % 58.93/59.02 cnf(5755,plain, % 58.93/59.02 (~P1(f3(a1,a20))+~E(f18(a1,f3(a1,a20)),a20)), % 58.93/59.02 inference(scs_inference,[],[50,5754,78])). % 58.93/59.02 cnf(5757,plain, % 58.93/59.02 (~E(f18(a1,f3(a1,a20)),a20)), % 58.93/59.02 inference(scs_inference,[],[51,50,5755,84])). % 58.93/59.02 cnf(5759,plain, % 58.93/59.02 (~E(x57591,a20)+~E(f18(a1,f3(a1,a20)),x57591)), % 58.93/59.02 inference(scs_inference,[],[5757,2,3])). % 58.93/59.02 cnf(5762,plain, % 58.93/59.02 (~E(f18(f3(a1,a21),f3(a1,a20)),a20)), % 58.93/59.02 inference(scs_inference,[],[140,5759,9])). % 58.93/59.02 cnf(5763,plain, % 58.93/59.02 (~E(a20,f18(f3(a1,a21),f3(a1,a20)))), % 58.93/59.02 inference(scs_inference,[],[5762,2])). % 58.93/59.02 cnf(5768,plain, % 58.93/59.02 (~E(x57681,f3(a1,a20))+~E(a20,f18(f3(a1,a21),x57681))), % 58.93/59.02 inference(scs_inference,[],[5763,3,10])). % 58.93/59.02 cnf(5873,plain, % 58.93/59.02 (~E(a20,f3(f3(f3(a1,a21),a21),a20))), % 58.93/59.02 inference(scs_inference,[],[51,52,142,5678,99])). % 58.93/59.02 cnf(5876,plain, % 58.93/59.02 (~E(x58761,f3(f3(a1,a21),a21))+~E(a20,f3(x58761,a20))), % 58.93/59.02 inference(scs_inference,[],[5873,2,3,5])). % 58.93/59.02 cnf(5980,plain, % 58.93/59.02 (~E(a20,f18(f3(a1,a21),f3(f3(a1,a21),a20)))), % 58.93/59.02 inference(scs_inference,[],[141,5768,5])). % 58.93/59.02 cnf(5984,plain, % 58.93/59.02 (~E(x59841,a20)+~E(a20,f18(f3(a1,a21),f3(f3(a1,a21),x59841)))), % 58.93/59.02 inference(scs_inference,[],[5980,2,3,10,6])). % 58.93/59.02 cnf(6033,plain, % 58.93/59.02 (~E(a20,f3(f3(a21,f3(a1,a21)),a20))), % 58.93/59.02 inference(scs_inference,[],[142,52,5876,79])). % 58.93/59.02 cnf(6036,plain, % 58.93/59.02 (~E(x60361,f3(a21,f3(a1,a21)))+~E(a20,f3(x60361,a20))), % 58.93/59.02 inference(scs_inference,[],[6033,2,3,5])). % 58.93/59.02 cnf(6125,plain, % 58.93/59.02 (~E(a20,f3(f3(a21,a1),a20))), % 58.93/59.02 inference(scs_inference,[],[140,6036,6])). % 58.93/59.02 cnf(6126,plain, % 58.93/59.02 (~E(f3(f3(a21,a1),a20),a20)), % 58.93/59.02 inference(scs_inference,[],[6125,2])). % 58.93/59.02 cnf(6136,plain, % 58.93/59.02 (~E(x61361,a20)+~E(f3(f3(a21,a1),a20),x61361)), % 58.93/59.02 inference(scs_inference,[],[6126,3])). % 58.93/59.02 cnf(6141,plain, % 58.93/59.02 (~E(f3(a21,f3(a1,a20)),a20)), % 58.93/59.02 inference(scs_inference,[],[51,50,52,6136,99])). % 58.93/59.02 cnf(6143,plain, % 58.93/59.02 (~E(x61431,a20)+~E(f3(a21,f3(a1,a20)),x61431)), % 58.93/59.02 inference(scs_inference,[],[6141,2,3])). % 58.93/59.02 cnf(6146,plain, % 58.93/59.02 (~E(f3(a1,a20),x61461)+~E(f3(a21,x61461),a20)), % 58.93/59.02 inference(scs_inference,[],[6143,6])). % 58.93/59.02 cnf(6150,plain, % 58.93/59.02 (~E(f3(a21,a1),a20)), % 58.93/59.02 inference(scs_inference,[],[51,6146,61])). % 58.93/59.02 cnf(6151,plain, % 58.93/59.02 (~E(a20,f3(a21,a1))), % 58.93/59.02 inference(scs_inference,[],[6150,2])). % 58.93/59.02 cnf(6152,plain, % 58.93/59.02 (~E(x61521,a20)+~E(f3(a21,a1),x61521)), % 58.93/59.02 inference(scs_inference,[],[6150,2,3])). % 58.93/59.02 cnf(6155,plain, % 58.93/59.02 (~E(f3(a21,f3(a1,a21)),a20)), % 58.93/59.02 inference(scs_inference,[],[140,6152,6])). % 58.93/59.02 cnf(6157,plain, % 58.93/59.02 (~E(x61571,f3(a21,a1))+~E(a20,x61571)), % 58.93/59.02 inference(scs_inference,[],[6151,6155,2,3])). % 58.93/59.02 cnf(6330,plain, % 58.93/59.02 (P4(f4(a20),a22)), % 58.93/59.02 inference(scs_inference,[],[51,67])). % 58.93/59.02 cnf(6332,plain, % 58.93/59.02 (P4(f7(a20),a23)), % 58.93/59.02 inference(scs_inference,[],[51,67,68])). % 58.93/59.02 cnf(6334,plain, % 58.93/59.02 (E(f3(a1,a20),a1)), % 58.93/59.02 inference(scs_inference,[],[51,67,68,61])). % 58.93/59.02 cnf(6382,plain, % 58.93/59.02 (P1(f2(a20))), % 58.93/59.02 inference(scs_inference,[],[51,5209,67,68,61,62,77,4,21,22,39,40,41,69,70,7,8,26,27,28,29,30,31,71,72,15,16,17,18,19,20,23,24,25,32,33,34,11,12,13,14,35,36,37,38,60])). % 58.93/59.02 cnf(6384,plain, % 58.93/59.02 (E(f18(f4(a20),f7(a20)),a20)), % 58.93/59.02 inference(scs_inference,[],[51,5209,67,68,61,62,77,4,21,22,39,40,41,69,70,7,8,26,27,28,29,30,31,71,72,15,16,17,18,19,20,23,24,25,32,33,34,11,12,13,14,35,36,37,38,60,75])). % 58.93/59.02 cnf(6388,plain, % 58.93/59.02 (E(f18(a1,a20),a20)), % 58.93/59.02 inference(scs_inference,[],[51,5209,67,68,61,62,77,4,21,22,39,40,41,69,70,7,8,26,27,28,29,30,31,71,72,15,16,17,18,19,20,23,24,25,32,33,34,11,12,13,14,35,36,37,38,60,75,66,63])). % 58.93/59.02 cnf(6390,plain, % 58.93/59.02 (E(f18(a20,a1),a20)), % 58.93/59.02 inference(scs_inference,[],[51,5209,67,68,61,62,77,4,21,22,39,40,41,69,70,7,8,26,27,28,29,30,31,71,72,15,16,17,18,19,20,23,24,25,32,33,34,11,12,13,14,35,36,37,38,60,75,66,63,65])). % 58.93/59.02 cnf(6394,plain, % 58.93/59.02 (E(f3(x63941,f3(a1,f2(a1))),f3(x63941,a1))), % 58.93/59.02 inference(scs_inference,[],[51,4854,5209,67,68,61,62,77,4,21,22,39,40,41,69,70,7,8,26,27,28,29,30,31,71,72,15,16,17,18,19,20,23,24,25,32,33,34,11,12,13,14,35,36,37,38,60,75,66,63,65,64,6])). % 58.93/59.02 cnf(6396,plain, % 58.93/59.02 (E(f18(f3(a1,f2(a1)),x63961),f18(a1,x63961))), % 58.93/59.02 inference(scs_inference,[],[51,4854,5209,67,68,61,62,77,4,21,22,39,40,41,69,70,7,8,26,27,28,29,30,31,71,72,15,16,17,18,19,20,23,24,25,32,33,34,11,12,13,14,35,36,37,38,60,75,66,63,65,64,6,10,9])). % 58.93/59.02 cnf(6411,plain, % 58.93/59.02 (P1(f3(a20,a20))), % 58.93/59.02 inference(scs_inference,[],[51,4858,4764,4699,4854,5209,57,67,68,61,62,77,4,21,22,39,40,41,69,70,7,8,26,27,28,29,30,31,71,72,15,16,17,18,19,20,23,24,25,32,33,34,11,12,13,14,35,36,37,38,60,75,66,63,65,64,6,10,9,5,2,85,86,89,94,88,83,84])). % 58.93/59.02 cnf(6526,plain, % 58.93/59.02 ($false), % 58.93/59.02 inference(scs_inference,[],[6411,6334,6330,6382,6388,6390,6332,6384,6394,6396,53,6157,5471,61,62,70,21,39,7,71,72,36,37,16,77,25,34,11,13,41,69,8,33,5984,68,67,20,38,26,29,30,17,19,24,32,5750,4,22,40,31,15,14,35,28,23,27,18,12,60,75,66,63,65,64,6,10,9,5,2,87]), % 58.93/59.02 ['proof']). % 58.93/59.02 % SZS output end Proof % 58.93/59.02 % Total time :58.380000s %------------------------------------------------------------------------------