%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM464+2 : 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 : n023.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 12:24:24 EDT 2024 % Result : Theorem 1.01s 1.11s % Output : CNFRefutation 1.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : NUM464+2 : TPTP v8.2.0. Released v4.0.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n023.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 02:07:54 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 1.01/1.09 %------------------------------------------- % 1.01/1.09 % File :CSE---1.7 % 1.01/1.09 % Problem :theBenchmark % 1.01/1.09 % Transform :cnf % 1.01/1.09 % Format :tptp:raw % 1.01/1.09 % Command :java -jar mcs_scs.jar %d %s % 1.01/1.09 % 1.01/1.09 % Result :Theorem 0.460000s % 1.01/1.09 % Output :CNFRefutation 0.460000s % 1.01/1.09 %------------------------------------------- % 1.01/1.10 %------------------------------------------------------------------------------ % 1.01/1.10 % File : NUM464+2 : TPTP v8.2.0. Released v4.0.0. % 1.01/1.10 % Domain : Number Theory % 1.01/1.10 % Problem : Square root of a prime is irrational 07_01, 01 expansion % 1.01/1.10 % Version : Especial. % 1.01/1.10 % English : % 1.01/1.10 % 1.01/1.10 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 1.01/1.10 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 1.01/1.10 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 1.01/1.10 % Source : [Pas08] % 1.01/1.10 % Names : primes_07_01.01 [Pas08] % 1.01/1.10 % 1.01/1.10 % Status : Theorem % 1.01/1.10 % Rating : 0.14 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.12 v6.3.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.13 v6.0.0, 0.09 v5.5.0, 0.19 v5.4.0, 0.18 v5.3.0, 0.19 v5.2.0, 0.15 v5.1.0, 0.24 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.1, 0.61 v4.0.0 % 1.01/1.10 % Syntax : Number of formulae : 28 ( 1 unt; 2 def) % 1.01/1.10 % Number of atoms : 121 ( 43 equ) % 1.01/1.10 % Maximal formula atoms : 10 ( 4 avg) % 1.01/1.10 % Number of connectives : 105 ( 12 ~; 7 |; 47 &) % 1.01/1.10 % ( 2 <=>; 37 =>; 0 <=; 0 <~>) % 1.01/1.10 % Maximal formula depth : 11 ( 6 avg) % 1.01/1.10 % Maximal term depth : 3 ( 1 avg) % 1.01/1.10 % Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty) % 1.01/1.10 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty) % 1.01/1.10 % Number of variables : 53 ( 51 !; 2 ?) % 1.01/1.10 % SPC : FOF_THM_RFO_SEQ % 1.01/1.10 % 1.01/1.10 % Comments : Problem generated by the SAD system [VLP07] % 1.01/1.10 %------------------------------------------------------------------------------ % 1.01/1.10 fof(mNatSort,axiom, % 1.01/1.10 ! [W0] : % 1.01/1.10 ( aNaturalNumber0(W0) % 1.01/1.10 => $true ) ). % 1.01/1.10 % 1.01/1.10 fof(mSortsC,axiom, % 1.01/1.10 aNaturalNumber0(sz00) ). % 1.01/1.10 % 1.01/1.10 fof(mSortsC_01,axiom, % 1.01/1.10 ( aNaturalNumber0(sz10) % 1.01/1.10 & sz10 != sz00 ) ). % 1.01/1.10 % 1.01/1.10 fof(mSortsB,axiom, % 1.01/1.10 ! [W0,W1] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) ) % 1.01/1.10 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 1.01/1.10 % 1.01/1.10 fof(mSortsB_02,axiom, % 1.01/1.10 ! [W0,W1] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) ) % 1.01/1.10 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 1.01/1.10 % 1.01/1.10 fof(mAddComm,axiom, % 1.01/1.10 ! [W0,W1] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) ) % 1.01/1.10 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 1.01/1.10 % 1.01/1.10 fof(mAddAsso,axiom, % 1.01/1.10 ! [W0,W1,W2] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) % 1.01/1.10 & aNaturalNumber0(W2) ) % 1.01/1.10 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 1.01/1.10 % 1.01/1.10 fof(m_AddZero,axiom, % 1.01/1.10 ! [W0] : % 1.01/1.10 ( aNaturalNumber0(W0) % 1.01/1.10 => ( sdtpldt0(W0,sz00) = W0 % 1.01/1.10 & W0 = sdtpldt0(sz00,W0) ) ) ). % 1.01/1.10 % 1.01/1.10 fof(mMulComm,axiom, % 1.01/1.10 ! [W0,W1] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) ) % 1.01/1.10 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 1.01/1.10 % 1.01/1.10 fof(mMulAsso,axiom, % 1.01/1.10 ! [W0,W1,W2] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) % 1.01/1.10 & aNaturalNumber0(W2) ) % 1.01/1.10 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 1.01/1.10 % 1.01/1.10 fof(m_MulUnit,axiom, % 1.01/1.10 ! [W0] : % 1.01/1.10 ( aNaturalNumber0(W0) % 1.01/1.10 => ( sdtasdt0(W0,sz10) = W0 % 1.01/1.10 & W0 = sdtasdt0(sz10,W0) ) ) ). % 1.01/1.10 % 1.01/1.10 fof(m_MulZero,axiom, % 1.01/1.10 ! [W0] : % 1.01/1.10 ( aNaturalNumber0(W0) % 1.01/1.10 => ( sdtasdt0(W0,sz00) = sz00 % 1.01/1.10 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 1.01/1.10 % 1.01/1.10 fof(mAMDistr,axiom, % 1.01/1.10 ! [W0,W1,W2] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) % 1.01/1.10 & aNaturalNumber0(W2) ) % 1.01/1.10 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 1.01/1.10 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 1.01/1.10 % 1.01/1.10 fof(mAddCanc,axiom, % 1.01/1.10 ! [W0,W1,W2] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) % 1.01/1.10 & aNaturalNumber0(W2) ) % 1.01/1.10 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 1.01/1.10 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 1.01/1.10 => W1 = W2 ) ) ). % 1.01/1.10 % 1.01/1.10 fof(mMulCanc,axiom, % 1.01/1.10 ! [W0] : % 1.01/1.10 ( aNaturalNumber0(W0) % 1.01/1.10 => ( W0 != sz00 % 1.01/1.10 => ! [W1,W2] : % 1.01/1.10 ( ( aNaturalNumber0(W1) % 1.01/1.10 & aNaturalNumber0(W2) ) % 1.01/1.10 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 1.01/1.10 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 1.01/1.10 => W1 = W2 ) ) ) ) ). % 1.01/1.10 % 1.01/1.10 fof(mZeroAdd,axiom, % 1.01/1.10 ! [W0,W1] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) ) % 1.01/1.10 => ( sdtpldt0(W0,W1) = sz00 % 1.01/1.10 => ( W0 = sz00 % 1.01/1.10 & W1 = sz00 ) ) ) ). % 1.01/1.10 % 1.01/1.10 fof(mZeroMul,axiom, % 1.01/1.10 ! [W0,W1] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) ) % 1.01/1.10 => ( sdtasdt0(W0,W1) = sz00 % 1.01/1.10 => ( W0 = sz00 % 1.01/1.10 | W1 = sz00 ) ) ) ). % 1.01/1.10 % 1.01/1.10 fof(mDefLE,definition, % 1.01/1.10 ! [W0,W1] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) ) % 1.01/1.10 => ( sdtlseqdt0(W0,W1) % 1.01/1.10 <=> ? [W2] : % 1.01/1.10 ( aNaturalNumber0(W2) % 1.01/1.10 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 1.01/1.10 % 1.01/1.10 fof(mDefDiff,definition, % 1.01/1.10 ! [W0,W1] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) ) % 1.01/1.10 => ( sdtlseqdt0(W0,W1) % 1.01/1.10 => ! [W2] : % 1.01/1.10 ( W2 = sdtmndt0(W1,W0) % 1.01/1.10 <=> ( aNaturalNumber0(W2) % 1.01/1.10 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 1.01/1.10 % 1.01/1.10 fof(mLERefl,axiom, % 1.01/1.10 ! [W0] : % 1.01/1.10 ( aNaturalNumber0(W0) % 1.01/1.10 => sdtlseqdt0(W0,W0) ) ). % 1.01/1.10 % 1.01/1.10 fof(mLEAsym,axiom, % 1.01/1.10 ! [W0,W1] : % 1.01/1.10 ( ( aNaturalNumber0(W0) % 1.01/1.10 & aNaturalNumber0(W1) ) % 1.01/1.10 => ( ( sdtlseqdt0(W0,W1) % 1.01/1.11 & sdtlseqdt0(W1,W0) ) % 1.01/1.11 => W0 = W1 ) ) ). % 1.01/1.11 % 1.01/1.11 fof(mLETran,axiom, % 1.01/1.11 ! [W0,W1,W2] : % 1.01/1.11 ( ( aNaturalNumber0(W0) % 1.01/1.11 & aNaturalNumber0(W1) % 1.01/1.11 & aNaturalNumber0(W2) ) % 1.01/1.11 => ( ( sdtlseqdt0(W0,W1) % 1.01/1.11 & sdtlseqdt0(W1,W2) ) % 1.01/1.11 => sdtlseqdt0(W0,W2) ) ) ). % 1.01/1.11 % 1.01/1.11 fof(mLETotal,axiom, % 1.01/1.11 ! [W0,W1] : % 1.01/1.11 ( ( aNaturalNumber0(W0) % 1.01/1.11 & aNaturalNumber0(W1) ) % 1.01/1.11 => ( sdtlseqdt0(W0,W1) % 1.01/1.11 | ( W1 != W0 % 1.01/1.11 & sdtlseqdt0(W1,W0) ) ) ) ). % 1.01/1.11 % 1.01/1.11 fof(mMonAdd,axiom, % 1.01/1.11 ! [W0,W1] : % 1.01/1.11 ( ( aNaturalNumber0(W0) % 1.01/1.11 & aNaturalNumber0(W1) ) % 1.01/1.11 => ( ( W0 != W1 % 1.01/1.11 & sdtlseqdt0(W0,W1) ) % 1.01/1.11 => ! [W2] : % 1.01/1.11 ( aNaturalNumber0(W2) % 1.01/1.11 => ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1) % 1.01/1.11 & sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)) % 1.01/1.11 & sdtpldt0(W0,W2) != sdtpldt0(W1,W2) % 1.01/1.11 & sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ) ). % 1.01/1.11 % 1.01/1.11 fof(mMonMul,axiom, % 1.01/1.11 ! [W0,W1,W2] : % 1.01/1.11 ( ( aNaturalNumber0(W0) % 1.01/1.11 & aNaturalNumber0(W1) % 1.01/1.11 & aNaturalNumber0(W2) ) % 1.01/1.11 => ( ( W0 != sz00 % 1.01/1.11 & W1 != W2 % 1.01/1.11 & sdtlseqdt0(W1,W2) ) % 1.01/1.11 => ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2) % 1.01/1.11 & sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 1.01/1.11 & sdtasdt0(W1,W0) != sdtasdt0(W2,W0) % 1.01/1.11 & sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) ). % 1.01/1.11 % 1.01/1.11 fof(mLENTr,axiom, % 1.01/1.11 ! [W0] : % 1.01/1.11 ( aNaturalNumber0(W0) % 1.01/1.11 => ( W0 = sz00 % 1.01/1.11 | W0 = sz10 % 1.01/1.11 | ( sz10 != W0 % 1.01/1.11 & sdtlseqdt0(sz10,W0) ) ) ) ). % 1.01/1.11 % 1.01/1.11 fof(m__987,hypothesis, % 1.01/1.11 ( aNaturalNumber0(xm) % 1.01/1.11 & aNaturalNumber0(xn) ) ). % 1.01/1.11 % 1.01/1.11 fof(m__,conjecture, % 1.01/1.11 ( xm != sz00 % 1.01/1.11 => ( ? [W0] : % 1.01/1.11 ( aNaturalNumber0(W0) % 1.01/1.11 & sdtpldt0(sz10,W0) = xm ) % 1.01/1.11 | sdtlseqdt0(sz10,xm) ) ) ). % 1.01/1.11 % 1.01/1.11 %------------------------------------------------------------------------------ % 1.01/1.11 %------------------------------------------- % 1.01/1.11 % Proof found % 1.01/1.11 % SZS status Theorem for theBenchmark % 1.01/1.11 % SZS output start Proof % 1.01/1.11 %ClaNum:63(EqnAxiom:14) % 1.01/1.11 %VarNum:263(SingletonVarNum:84) % 1.01/1.11 %MaxLitNum:7 % 1.01/1.11 %MaxfuncDepth:2 % 1.01/1.11 %SharedTerms:11 % 1.01/1.11 %goalClause: 20 21 30 % 1.01/1.11 %singleGoalClaCount:2 % 1.01/1.11 [15]P1(a1) % 1.01/1.11 [16]P1(a6) % 1.01/1.11 [17]P1(a7) % 1.01/1.11 [18]P1(a8) % 1.01/1.11 [19]~E(a1,a6) % 1.01/1.11 [20]~E(a1,a7) % 1.01/1.11 [21]~P2(a6,a7) % 1.01/1.11 [28]~P1(x281)+P2(x281,x281) % 1.01/1.11 [22]~P1(x221)+E(f2(a1,x221),a1) % 1.01/1.11 [23]~P1(x231)+E(f2(x231,a1),a1) % 1.01/1.11 [24]~P1(x241)+E(f4(a1,x241),x241) % 1.01/1.11 [25]~P1(x251)+E(f2(a6,x251),x251) % 1.01/1.11 [26]~P1(x261)+E(f4(x261,a1),x261) % 1.01/1.11 [27]~P1(x271)+E(f2(x271,a6),x271) % 1.01/1.11 [30]~P1(x301)+~E(f4(a6,x301),a7) % 1.01/1.11 [35]~P1(x352)+~P1(x351)+E(f4(x351,x352),f4(x352,x351)) % 1.01/1.11 [36]~P1(x362)+~P1(x361)+E(f2(x361,x362),f2(x362,x361)) % 1.01/1.11 [38]~P1(x382)+~P1(x381)+P1(f4(x381,x382)) % 1.01/1.11 [39]~P1(x392)+~P1(x391)+P1(f2(x391,x392)) % 1.01/1.11 [29]~P1(x291)+E(x291,a6)+P2(a6,x291)+E(x291,a1) % 1.01/1.11 [31]~E(x312,x311)+~P1(x311)+~P1(x312)+P2(x311,x312) % 1.01/1.11 [37]P2(x372,x371)+~P1(x371)+~P1(x372)+P2(x371,x372) % 1.01/1.11 [32]~P1(x322)+~P1(x321)+E(x321,a1)+~E(f4(x322,x321),a1) % 1.01/1.11 [33]~P1(x332)+~P1(x331)+E(x331,a1)+~E(f4(x331,x332),a1) % 1.01/1.11 [43]~P1(x432)+~P1(x431)+~P2(x431,x432)+P1(f3(x431,x432)) % 1.01/1.11 [49]~P1(x492)+~P1(x491)+~P2(x491,x492)+E(f4(x491,f3(x491,x492)),x492) % 1.01/1.11 [56]~P1(x563)+~P1(x562)+~P1(x561)+E(f4(f4(x561,x562),x563),f4(x561,f4(x562,x563))) % 1.01/1.11 [57]~P1(x573)+~P1(x572)+~P1(x571)+E(f2(f2(x571,x572),x573),f2(x571,f2(x572,x573))) % 1.01/1.11 [62]~P1(x623)+~P1(x622)+~P1(x621)+E(f4(f2(x621,x622),f2(x621,x623)),f2(x621,f4(x622,x623))) % 1.01/1.11 [63]~P1(x632)+~P1(x633)+~P1(x631)+E(f4(f2(x631,x632),f2(x633,x632)),f2(f4(x631,x633),x632)) % 1.01/1.11 [41]~P1(x412)+~P1(x411)+~P2(x412,x411)+~P2(x411,x412)+E(x411,x412) % 1.01/1.11 [34]~P1(x341)+~P1(x342)+E(x341,a1)+E(x342,a1)+~E(f2(x342,x341),a1) % 1.01/1.11 [40]~P1(x402)+~P1(x401)+~P1(x403)+P2(x401,x402)+~E(f4(x401,x403),x402) % 1.01/1.11 [42]~P1(x423)+~P1(x422)+~P2(x423,x422)+P1(x421)+~E(x421,f5(x422,x423)) % 1.01/1.11 [44]~P1(x442)+~P1(x441)+~P1(x443)+E(x441,x442)+~E(f4(x443,x441),f4(x443,x442)) % 1.01/1.11 [45]~P1(x452)+~P1(x453)+~P1(x451)+E(x451,x452)+~E(f4(x451,x453),f4(x452,x453)) % 1.01/1.11 [48]~P1(x483)+~P1(x481)+~P2(x481,x483)+~E(x482,f5(x483,x481))+E(f4(x481,x482),x483) % 1.01/1.11 [50]~P1(x502)+~P1(x501)+~P2(x503,x502)+~P2(x501,x503)+P2(x501,x502)+~P1(x503) % 1.01/1.11 [46]~P1(x462)+~P1(x461)+~P1(x463)+E(x461,x462)+~E(f2(x463,x461),f2(x463,x462))+E(x463,a1) % 1.01/1.11 [47]~P1(x472)+~P1(x473)+~P1(x471)+E(x471,x472)+~E(f2(x471,x473),f2(x472,x473))+E(x473,a1) % 1.01/1.11 [51]~P1(x512)+~P1(x513)+~P1(x511)+~P2(x513,x512)+~E(f4(x513,x511),x512)+E(x511,f5(x512,x513)) % 1.01/1.11 [58]~P1(x582)+~P1(x581)+~P1(x583)+~P2(x581,x582)+E(x581,x582)+P2(f4(x583,x581),f4(x583,x582)) % 1.01/1.11 [59]~P1(x592)+~P1(x593)+~P1(x591)+~P2(x591,x592)+E(x591,x592)+P2(f4(x591,x593),f4(x592,x593)) % 1.01/1.11 [60]~P1(x602)+~P1(x601)+~P1(x603)+~P2(x601,x602)+E(x601,x602)+P2(f2(x603,x601),f2(x603,x602))+E(x603,a1) % 1.01/1.11 [61]~P1(x612)+~P1(x613)+~P1(x611)+~P2(x611,x612)+E(x611,x612)+P2(f2(x611,x613),f2(x612,x613))+E(x613,a1) % 1.01/1.11 %EqnAxiom % 1.01/1.11 [1]E(x11,x11) % 1.01/1.11 [2]E(x22,x21)+~E(x21,x22) % 1.01/1.11 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.01/1.11 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 1.01/1.11 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 1.01/1.11 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63)) % 1.01/1.11 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72)) % 1.01/1.11 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83)) % 1.01/1.11 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92)) % 1.01/1.11 [10]~E(x101,x102)+E(f3(x101,x103),f3(x102,x103)) % 1.01/1.11 [11]~E(x111,x112)+E(f3(x113,x111),f3(x113,x112)) % 1.01/1.11 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 1.01/1.11 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133) % 1.01/1.11 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141) % 1.01/1.11 % 1.01/1.11 %------------------------------------------- % 1.01/1.11 cnf(65,plain, % 1.01/1.11 (P2(x651,f4(x651,x652))+~P1(f4(x651,x652))+~P1(x651)+~P1(x652)), % 1.01/1.11 inference(equality_inference,[],[40])). % 1.01/1.11 cnf(66,plain, % 1.01/1.11 (~P2(x661,x662)+~P1(x661)+~P1(x662)+P1(f5(x662,x661))), % 1.01/1.11 inference(equality_inference,[],[42])). % 1.01/1.11 cnf(71,plain, % 1.01/1.11 (~P2(x711,x712)+~P1(x712)+~P1(x711)+E(f4(x711,f5(x712,x711)),x712)), % 1.01/1.11 inference(equality_inference,[],[48])). % 1.01/1.11 cnf(75,plain, % 1.01/1.11 (P2(x751,a1)+~E(a1,x751)), % 1.01/1.11 inference(scs_inference,[],[15,37,13])). % 1.01/1.11 cnf(76,plain, % 1.01/1.11 (P1(f5(a1,a1))), % 1.01/1.11 inference(scs_inference,[],[15,37,13,66])). % 1.01/1.11 cnf(78,plain, % 1.01/1.11 (E(f4(a1,f5(a1,a1)),a1)), % 1.01/1.11 inference(scs_inference,[],[15,37,13,66,71])). % 1.01/1.11 cnf(80,plain, % 1.01/1.11 (E(f5(a1,a1),a1)), % 1.01/1.11 inference(scs_inference,[],[15,37,13,66,71,32])). % 1.01/1.11 cnf(82,plain, % 1.01/1.11 (E(a1,f4(a1,f5(a1,a1)))), % 1.01/1.11 inference(scs_inference,[],[15,37,13,66,71,32,2])). % 1.01/1.11 cnf(85,plain, % 1.01/1.11 (P2(a1,f4(a1,f5(a1,a1)))), % 1.01/1.11 inference(scs_inference,[],[15,37,13,66,71,32,2,3,12,14])). % 1.01/1.11 cnf(86,plain, % 1.01/1.11 (P2(a6,a6)), % 1.01/1.11 inference(scs_inference,[],[15,16,37,13,66,71,32,2,3,12,14,31])). % 1.01/1.11 cnf(111,plain, % 1.01/1.11 (P2(a7,a7)), % 1.01/1.11 inference(scs_inference,[],[21,78,76,82,15,80,85,17,86,16,75,2,14,3,13,71,37,66,40,51,12,65,31])). % 1.01/1.11 cnf(374,plain, % 1.01/1.11 ($false), % 1.01/1.11 inference(scs_inference,[],[20,21,17,111,13,29,2]), % 1.01/1.11 ['proof']). % 1.01/1.11 % SZS output end Proof % 1.01/1.11 % Total time :0.460000s %------------------------------------------------------------------------------