%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM436+3 : 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 : n029.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:15 EDT 2024 % Result : Theorem 2.11s 2.19s % Output : CNFRefutation 2.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM436+3 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.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 : Sat Jun 22 19:51:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.50/0.57 start to proof:theBenchmark % 2.11/2.17 %------------------------------------------- % 2.11/2.17 % File :CSE---1.7 % 2.11/2.17 % Problem :theBenchmark % 2.11/2.17 % Transform :cnf % 2.11/2.17 % Format :tptp:raw % 2.11/2.17 % Command :java -jar mcs_scs.jar %d %s % 2.11/2.17 % 2.11/2.17 % Result :Theorem 1.580000s % 2.11/2.17 % Output :CNFRefutation 1.580000s % 2.11/2.17 %------------------------------------------- % 2.11/2.18 %------------------------------------------------------------------------------ % 2.11/2.18 % File : NUM436+3 : TPTP v8.2.0. Released v4.0.0. % 2.11/2.18 % Domain : Number Theory % 2.11/2.18 % Problem : Fuerstenberg's infinitude of primes 06_03, 02 expansion % 2.11/2.18 % Version : Especial. % 2.11/2.18 % English : % 2.11/2.18 % 2.11/2.18 % Refs : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 2.11/2.18 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 2.11/2.18 % Source : [Pas08] % 2.11/2.18 % Names : fuerst_06_03.02 [Pas08] % 2.11/2.18 % 2.11/2.18 % Status : Theorem % 2.11/2.18 % Rating : 0.28 v8.2.0, 0.25 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.20 v7.3.0, 0.28 v7.1.0, 0.30 v7.0.0, 0.27 v6.4.0, 0.31 v6.3.0, 0.33 v6.2.0, 0.32 v6.1.0, 0.40 v6.0.0, 0.35 v5.5.0, 0.52 v5.4.0, 0.54 v5.3.0, 0.56 v5.2.0, 0.50 v5.1.0, 0.57 v5.0.0, 0.58 v4.1.0, 0.65 v4.0.1, 0.83 v4.0.0 % 2.11/2.18 % Syntax : Number of formulae : 27 ( 2 unt; 2 def) % 2.11/2.18 % Number of atoms : 104 ( 34 equ) % 2.11/2.18 % Maximal formula atoms : 8 ( 3 avg) % 2.11/2.18 % Number of connectives : 85 ( 8 ~; 5 |; 47 &) % 2.11/2.18 % ( 2 <=>; 23 =>; 0 <=; 0 <~>) % 2.11/2.18 % Maximal formula depth : 11 ( 5 avg) % 2.11/2.18 % Maximal term depth : 3 ( 1 avg) % 2.11/2.18 % Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty) % 2.11/2.18 % Number of functors : 10 ( 10 usr; 7 con; 0-2 aty) % 2.11/2.18 % Number of variables : 44 ( 40 !; 4 ?) % 2.11/2.18 % SPC : FOF_THM_RFO_SEQ % 2.11/2.18 % 2.11/2.18 % Comments : Problem generated by the SAD system [VLP07] % 2.11/2.18 %------------------------------------------------------------------------------ % 2.11/2.18 fof(mIntegers,axiom, % 2.11/2.18 ! [W0] : % 2.11/2.18 ( aInteger0(W0) % 2.11/2.18 => $true ) ). % 2.11/2.18 % 2.11/2.18 fof(mIntZero,axiom, % 2.11/2.18 aInteger0(sz00) ). % 2.11/2.18 % 2.11/2.18 fof(mIntOne,axiom, % 2.11/2.18 aInteger0(sz10) ). % 2.11/2.18 % 2.11/2.18 fof(mIntNeg,axiom, % 2.11/2.18 ! [W0] : % 2.11/2.18 ( aInteger0(W0) % 2.11/2.18 => aInteger0(smndt0(W0)) ) ). % 2.11/2.18 % 2.11/2.18 fof(mIntPlus,axiom, % 2.11/2.18 ! [W0,W1] : % 2.11/2.18 ( ( aInteger0(W0) % 2.11/2.18 & aInteger0(W1) ) % 2.11/2.18 => aInteger0(sdtpldt0(W0,W1)) ) ). % 2.11/2.18 % 2.11/2.18 fof(mIntMult,axiom, % 2.11/2.18 ! [W0,W1] : % 2.11/2.18 ( ( aInteger0(W0) % 2.11/2.18 & aInteger0(W1) ) % 2.11/2.18 => aInteger0(sdtasdt0(W0,W1)) ) ). % 2.11/2.18 % 2.11/2.18 fof(mAddAsso,axiom, % 2.11/2.18 ! [W0,W1,W2] : % 2.11/2.18 ( ( aInteger0(W0) % 2.11/2.18 & aInteger0(W1) % 2.11/2.18 & aInteger0(W2) ) % 2.11/2.18 => sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) ). % 2.11/2.18 % 2.11/2.18 fof(mAddComm,axiom, % 2.11/2.18 ! [W0,W1] : % 2.11/2.18 ( ( aInteger0(W0) % 2.11/2.18 & aInteger0(W1) ) % 2.11/2.18 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 2.11/2.18 % 2.11/2.18 fof(mAddZero,axiom, % 2.11/2.18 ! [W0] : % 2.11/2.18 ( aInteger0(W0) % 2.11/2.18 => ( sdtpldt0(W0,sz00) = W0 % 2.11/2.18 & W0 = sdtpldt0(sz00,W0) ) ) ). % 2.11/2.18 % 2.11/2.18 fof(mAddNeg,axiom, % 2.11/2.18 ! [W0] : % 2.11/2.18 ( aInteger0(W0) % 2.11/2.18 => ( sdtpldt0(W0,smndt0(W0)) = sz00 % 2.11/2.18 & sz00 = sdtpldt0(smndt0(W0),W0) ) ) ). % 2.11/2.18 % 2.11/2.18 fof(mMulAsso,axiom, % 2.11/2.18 ! [W0,W1,W2] : % 2.11/2.18 ( ( aInteger0(W0) % 2.11/2.18 & aInteger0(W1) % 2.11/2.18 & aInteger0(W2) ) % 2.11/2.18 => sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) ). % 2.11/2.18 % 2.11/2.18 fof(mMulComm,axiom, % 2.11/2.18 ! [W0,W1] : % 2.11/2.18 ( ( aInteger0(W0) % 2.11/2.18 & aInteger0(W1) ) % 2.11/2.18 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 2.11/2.18 % 2.11/2.18 fof(mMulOne,axiom, % 2.11/2.18 ! [W0] : % 2.11/2.18 ( aInteger0(W0) % 2.11/2.18 => ( sdtasdt0(W0,sz10) = W0 % 2.11/2.18 & W0 = sdtasdt0(sz10,W0) ) ) ). % 2.11/2.18 % 2.11/2.18 fof(mDistrib,axiom, % 2.11/2.18 ! [W0,W1,W2] : % 2.11/2.18 ( ( aInteger0(W0) % 2.11/2.18 & aInteger0(W1) % 2.11/2.18 & aInteger0(W2) ) % 2.11/2.18 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 2.11/2.18 & sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) ). % 2.11/2.18 % 2.11/2.18 fof(mMulZero,axiom, % 2.11/2.18 ! [W0] : % 2.11/2.18 ( aInteger0(W0) % 2.11/2.18 => ( sdtasdt0(W0,sz00) = sz00 % 2.11/2.18 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 2.11/2.18 % 2.11/2.18 fof(mMulMinOne,axiom, % 2.11/2.18 ! [W0] : % 2.11/2.18 ( aInteger0(W0) % 2.11/2.18 => ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0) % 2.11/2.18 & smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) ). % 2.11/2.18 % 2.11/2.18 fof(mZeroDiv,axiom, % 2.11/2.18 ! [W0,W1] : % 2.11/2.18 ( ( aInteger0(W0) % 2.11/2.18 & aInteger0(W1) ) % 2.11/2.18 => ( sdtasdt0(W0,W1) = sz00 % 2.11/2.18 => ( W0 = sz00 % 2.11/2.18 | W1 = sz00 ) ) ) ). % 2.11/2.18 % 2.11/2.18 fof(mDivisor,definition, % 2.11/2.18 ! [W0] : % 2.11/2.18 ( aInteger0(W0) % 2.11/2.18 => ! [W1] : % 2.11/2.18 ( aDivisorOf0(W1,W0) % 2.11/2.18 <=> ( aInteger0(W1) % 2.11/2.18 & W1 != sz00 % 2.11/2.18 & ? [W2] : % 2.11/2.18 ( aInteger0(W2) % 2.11/2.18 & sdtasdt0(W1,W2) = W0 ) ) ) ) ). % 2.11/2.18 % 2.11/2.18 fof(mEquMod,definition, % 2.11/2.18 ! [W0,W1,W2] : % 2.11/2.18 ( ( aInteger0(W0) % 2.11/2.18 & aInteger0(W1) % 2.11/2.18 & aInteger0(W2) % 2.11/2.18 & W2 != sz00 ) % 2.11/2.18 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 2.11/2.18 <=> aDivisorOf0(W2,sdtpldt0(W0,smndt0(W1))) ) ) ). % 2.11/2.18 % 2.11/2.18 fof(mEquModRef,axiom, % 2.11/2.18 ! [W0,W1] : % 2.11/2.18 ( ( aInteger0(W0) % 2.11/2.18 & aInteger0(W1) % 2.11/2.18 & W1 != sz00 ) % 2.11/2.19 => sdteqdtlpzmzozddtrp0(W0,W0,W1) ) ). % 2.11/2.19 % 2.11/2.19 fof(mEquModSym,axiom, % 2.11/2.19 ! [W0,W1,W2] : % 2.11/2.19 ( ( aInteger0(W0) % 2.11/2.19 & aInteger0(W1) % 2.11/2.19 & aInteger0(W2) % 2.11/2.19 & W2 != sz00 ) % 2.11/2.19 => ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 2.11/2.19 => sdteqdtlpzmzozddtrp0(W1,W0,W2) ) ) ). % 2.11/2.19 % 2.11/2.19 fof(mEquModTrn,axiom, % 2.11/2.19 ! [W0,W1,W2,W3] : % 2.11/2.19 ( ( aInteger0(W0) % 2.11/2.19 & aInteger0(W1) % 2.11/2.19 & aInteger0(W2) % 2.11/2.19 & W2 != sz00 % 2.11/2.19 & aInteger0(W3) ) % 2.11/2.19 => ( ( sdteqdtlpzmzozddtrp0(W0,W1,W2) % 2.11/2.19 & sdteqdtlpzmzozddtrp0(W1,W3,W2) ) % 2.11/2.19 => sdteqdtlpzmzozddtrp0(W0,W3,W2) ) ) ). % 2.11/2.19 % 2.11/2.19 fof(m__979,hypothesis, % 2.11/2.19 ( aInteger0(xa) % 2.11/2.19 & aInteger0(xb) % 2.11/2.19 & aInteger0(xp) % 2.11/2.19 & xp != sz00 % 2.11/2.19 & aInteger0(xq) % 2.11/2.19 & xq != sz00 ) ). % 2.11/2.19 % 2.11/2.19 fof(m__1003,hypothesis, % 2.11/2.19 ( sdtasdt0(xp,xq) != sz00 % 2.11/2.19 & ? [W0] : % 2.11/2.19 ( aInteger0(W0) % 2.11/2.19 & sdtasdt0(sdtasdt0(xp,xq),W0) = sdtpldt0(xa,smndt0(xb)) ) % 2.11/2.19 & aDivisorOf0(sdtasdt0(xp,xq),sdtpldt0(xa,smndt0(xb))) % 2.11/2.19 & sdteqdtlpzmzozddtrp0(xa,xb,sdtasdt0(xp,xq)) ) ). % 2.11/2.19 % 2.11/2.19 fof(m__1032,hypothesis, % 2.11/2.19 ( aInteger0(xm) % 2.11/2.19 & sdtasdt0(sdtasdt0(xp,xq),xm) = sdtpldt0(xa,smndt0(xb)) ) ). % 2.11/2.19 % 2.11/2.19 fof(m__1071,hypothesis, % 2.11/2.19 ( sdtasdt0(xp,sdtasdt0(xq,xm)) = sdtpldt0(xa,smndt0(xb)) % 2.11/2.19 & sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,sdtasdt0(xp,xm)) ) ). % 2.11/2.19 % 2.11/2.19 fof(m__,conjecture, % 2.11/2.19 ( ( ? [W0] : % 2.11/2.19 ( aInteger0(W0) % 2.11/2.19 & sdtasdt0(xp,W0) = sdtpldt0(xa,smndt0(xb)) ) % 2.11/2.19 | aDivisorOf0(xp,sdtpldt0(xa,smndt0(xb))) % 2.11/2.19 | sdteqdtlpzmzozddtrp0(xa,xb,xp) ) % 2.11/2.19 & ( ? [W0] : % 2.11/2.19 ( aInteger0(W0) % 2.11/2.19 & sdtasdt0(xq,W0) = sdtpldt0(xa,smndt0(xb)) ) % 2.11/2.19 | aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb))) % 2.11/2.19 | sdteqdtlpzmzozddtrp0(xa,xb,xq) ) ) ). % 2.11/2.19 % 2.11/2.19 %------------------------------------------------------------------------------ % 2.11/2.19 %------------------------------------------- % 2.11/2.19 % Proof found % 2.11/2.19 % SZS status Theorem for theBenchmark % 2.11/2.19 % SZS output start Proof % 2.11/2.19 %ClaNum:72(EqnAxiom:16) % 2.11/2.19 %VarNum:185(SingletonVarNum:65) % 2.11/2.19 %MaxLitNum:8 % 2.11/2.19 %MaxfuncDepth:2 % 2.11/2.19 %SharedTerms:37 % 2.11/2.19 %goalClause: 58 59 60 63 64 65 66 67 68 % 2.11/2.19 [17]P1(a1) % 2.11/2.19 [18]P1(a7) % 2.11/2.19 [19]P1(a8) % 2.11/2.19 [20]P1(a9) % 2.11/2.19 [21]P1(a10) % 2.11/2.19 [22]P1(a12) % 2.11/2.19 [23]P1(a11) % 2.11/2.19 [24]P1(a2) % 2.11/2.19 [31]~E(a1,a10) % 2.11/2.19 [32]~E(a1,a12) % 2.11/2.19 [30]P3(a8,a9,f4(a10,a12)) % 2.11/2.19 [33]~E(f4(a10,a12),a1) % 2.11/2.19 [25]E(f4(a12,f4(a10,a11)),f6(a8,f5(a9))) % 2.11/2.19 [26]E(f4(a10,f4(a12,a11)),f6(a8,f5(a9))) % 2.11/2.19 [27]E(f4(f4(a10,a12),a11),f6(a8,f5(a9))) % 2.11/2.19 [28]E(f4(f4(a10,a12),a2),f6(a8,f5(a9))) % 2.11/2.19 [29]P2(f4(a10,a12),f6(a8,f5(a9))) % 2.11/2.19 [68]~P3(a8,a9,a10)+~P3(a8,a9,a12) % 2.11/2.19 [65]~P2(a10,f6(a8,f5(a9)))+~P2(a12,f6(a8,f5(a9))) % 2.11/2.19 [66]~P3(a8,a9,a10)+~P2(a12,f6(a8,f5(a9))) % 2.11/2.19 [67]~P3(a8,a9,a12)+~P2(a10,f6(a8,f5(a9))) % 2.11/2.19 [34]~P1(x341)+P1(f5(x341)) % 2.11/2.19 [35]~P1(x351)+E(f4(a1,x351),a1) % 2.11/2.19 [36]~P1(x361)+E(f4(x361,a1),a1) % 2.11/2.19 [37]~P1(x371)+E(f6(a1,x371),x371) % 2.11/2.19 [38]~P1(x381)+E(f4(a7,x381),x381) % 2.11/2.19 [39]~P1(x391)+E(f6(x391,a1),x391) % 2.11/2.19 [40]~P1(x401)+E(f4(x401,a7),x401) % 2.11/2.19 [41]~P1(x411)+E(f6(f5(x411),x411),a1) % 2.11/2.19 [42]~P1(x421)+E(f6(x421,f5(x421)),a1) % 2.11/2.19 [43]~P1(x431)+E(f4(x431,f5(a7)),f5(x431)) % 2.11/2.19 [44]~P1(x441)+E(f4(f5(a7),x441),f5(x441)) % 2.11/2.19 [59]~P1(x591)+~E(f4(a10,x591),f6(a8,f5(a9)))+~P2(a12,f6(a8,f5(a9))) % 2.11/2.19 [60]~P1(x601)+~E(f4(a12,x601),f6(a8,f5(a9)))+~P2(a10,f6(a8,f5(a9))) % 2.11/2.19 [63]~P1(x631)+~P3(a8,a9,a12)+~E(f4(a10,x631),f6(a8,f5(a9))) % 2.11/2.19 [64]~P1(x641)+~P3(a8,a9,a10)+~E(f4(a12,x641),f6(a8,f5(a9))) % 2.11/2.19 [45]~P2(x451,x452)+~P1(x452)+~E(x451,a1) % 2.11/2.19 [46]~P2(x461,x462)+P1(x461)+~P1(x462) % 2.11/2.19 [48]~P1(x482)+~P1(x481)+E(f6(x481,x482),f6(x482,x481)) % 2.11/2.19 [49]~P1(x492)+~P1(x491)+E(f4(x491,x492),f4(x492,x491)) % 2.11/2.19 [50]~P1(x502)+~P1(x501)+P1(f6(x501,x502)) % 2.11/2.19 [51]~P1(x512)+~P1(x511)+P1(f4(x511,x512)) % 2.11/2.19 [52]~P1(x521)+~P2(x522,x521)+P1(f3(x521,x522)) % 2.11/2.19 [55]~P1(x552)+~P2(x551,x552)+E(f4(x551,f3(x552,x551)),x552) % 2.11/2.19 [54]~P1(x541)+~P1(x542)+P3(x542,x542,x541)+E(x541,a1) % 2.11/2.19 [58]~P1(x581)+~P1(x582)+~E(f4(a12,x582),f6(a8,f5(a9)))+~E(f4(a10,x581),f6(a8,f5(a9))) % 2.11/2.19 [56]~P1(x563)+~P1(x562)+~P1(x561)+E(f6(f6(x561,x562),x563),f6(x561,f6(x562,x563))) % 2.11/2.19 [57]~P1(x573)+~P1(x572)+~P1(x571)+E(f4(f4(x571,x572),x573),f4(x571,f4(x572,x573))) % 2.11/2.19 [61]~P1(x613)+~P1(x612)+~P1(x611)+E(f6(f4(x611,x612),f4(x611,x613)),f4(x611,f6(x612,x613))) % 2.11/2.19 [62]~P1(x622)+~P1(x623)+~P1(x621)+E(f6(f4(x621,x622),f4(x623,x622)),f4(f6(x621,x623),x622)) % 2.11/2.19 [47]~P1(x471)+~P1(x472)+E(x471,a1)+E(x472,a1)+~E(f4(x472,x471),a1) % 2.11/2.19 [71]~P1(x711)+~P1(x712)+~P1(x713)+~P3(x713,x712,x711)+P3(x712,x713,x711)+E(x711,a1) % 2.11/2.19 [53]~P1(x532)+~P1(x533)+~P1(x531)+P2(x531,x532)+E(x531,a1)+~E(f4(x531,x533),x532) % 2.11/2.19 [69]~P1(x693)+~P1(x692)+~P1(x691)+P3(x692,x693,x691)+E(x691,a1)+~P2(x691,f6(x692,f5(x693))) % 2.11/2.19 [70]~P1(x701)+~P1(x703)+~P1(x702)+~P3(x702,x703,x701)+E(x701,a1)+P2(x701,f6(x702,f5(x703))) % 2.11/2.19 [72]~P1(x723)+~P1(x721)+~P1(x722)+~P3(x724,x723,x721)+~P3(x722,x724,x721)+P3(x722,x723,x721)+~P1(x724)+E(x721,a1) % 2.11/2.19 %EqnAxiom % 2.11/2.19 [1]E(x11,x11) % 2.11/2.19 [2]E(x22,x21)+~E(x21,x22) % 2.11/2.19 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.11/2.19 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43)) % 2.11/2.19 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52)) % 2.11/2.19 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63)) % 2.11/2.19 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72)) % 2.11/2.19 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 2.11/2.19 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 2.11/2.19 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 2.11/2.19 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 2.11/2.19 [12]P3(x122,x123,x124)+~E(x121,x122)+~P3(x121,x123,x124) % 2.11/2.19 [13]P3(x133,x132,x134)+~E(x131,x132)+~P3(x133,x131,x134) % 2.11/2.19 [14]P3(x143,x144,x142)+~E(x141,x142)+~P3(x143,x144,x141) % 2.11/2.19 [15]P2(x152,x153)+~E(x151,x152)+~P2(x151,x153) % 2.11/2.19 [16]P2(x163,x162)+~E(x161,x162)+~P2(x163,x161) % 2.11/2.19 % 2.11/2.19 %------------------------------------------- % 2.11/2.19 cnf(75,plain, % 2.11/2.19 (E(f6(a8,f5(a9)),f4(a10,f4(a12,a11)))), % 2.11/2.19 inference(scs_inference,[],[26,2])). % 2.11/2.19 cnf(76,plain, % 2.11/2.19 (P2(f4(a10,a12),f4(a10,f4(a12,a11)))), % 2.11/2.19 inference(scs_inference,[],[26,29,2,16])). % 2.11/2.19 cnf(90,plain, % 2.11/2.19 (~P1(f4(a12,a11))+~P1(f4(a10,a11))+~E(f4(a10,a12),x901)), % 2.11/2.19 inference(scs_inference,[],[75,25,26,76,30,2,3,64,15,14,16,58])). % 2.11/2.19 cnf(93,plain, % 2.11/2.19 (~P1(f4(a12,a11))+~P1(f4(a10,a11))), % 2.11/2.19 inference(equality_inference,[],[90])). % 2.11/2.19 cnf(571,plain, % 2.11/2.19 (~P1(f4(a10,a11))), % 2.11/2.19 inference(scs_inference,[],[23,22,93,51])). % 2.11/2.19 cnf(572,plain, % 2.11/2.19 ($false), % 2.11/2.19 inference(scs_inference,[],[571,21,23,51]), % 2.11/2.19 ['proof']). % 2.11/2.19 % SZS output end Proof % 2.11/2.19 % Total time :1.580000s %------------------------------------------------------------------------------