%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM458+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 : n022.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:22 EDT 2024 % Result : Theorem 86.89s 86.92s % Output : CNFRefutation 86.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM458+2 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.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 20:24:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 86.81/86.90 %------------------------------------------- % 86.81/86.90 % File :CSE---1.7 % 86.81/86.90 % Problem :theBenchmark % 86.81/86.90 % Transform :cnf % 86.81/86.90 % Format :tptp:raw % 86.81/86.90 % Command :java -jar mcs_scs.jar %d %s % 86.81/86.90 % 86.81/86.90 % Result :Theorem 86.280000s % 86.81/86.90 % Output :CNFRefutation 86.280000s % 86.81/86.90 %------------------------------------------- % 86.89/86.91 %------------------------------------------------------------------------------ % 86.89/86.91 % File : NUM458+2 : TPTP v8.2.0. Released v4.0.0. % 86.89/86.91 % Domain : Number Theory % 86.89/86.91 % Problem : Square root of a prime is irrational 02, 01 expansion % 86.89/86.91 % Version : Especial. % 86.89/86.91 % English : % 86.89/86.91 % 86.89/86.91 % Refs : [LPV06] Lyaletski et al. (2006), SAD as a Mathematical Assista % 86.89/86.91 % : [VLP07] Verchinine et al. (2007), System for Automated Deduction % 86.89/86.91 % : [Pas08] Paskevich (2008), Email to G. Sutcliffe % 86.89/86.91 % Source : [Pas08] % 86.89/86.91 % Names : primes_02.01 [Pas08] % 86.89/86.91 % 86.89/86.91 % Status : Theorem % 86.89/86.91 % Rating : 0.03 v8.1.0, 0.00 v6.4.0, 0.04 v6.3.0, 0.00 v6.1.0, 0.03 v6.0.0, 0.04 v5.5.0, 0.07 v5.4.0, 0.11 v5.3.0, 0.19 v5.2.0, 0.05 v5.1.0, 0.19 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.1, 0.57 v4.0.0 % 86.89/86.91 % Syntax : Number of formulae : 21 ( 2 unt; 2 def) % 86.89/86.91 % Number of atoms : 77 ( 30 equ) % 86.89/86.91 % Maximal formula atoms : 7 ( 3 avg) % 86.89/86.91 % Number of connectives : 58 ( 2 ~; 4 |; 26 &) % 86.89/86.91 % ( 2 <=>; 24 =>; 0 <=; 0 <~>) % 86.89/86.91 % Maximal formula depth : 9 ( 5 avg) % 86.89/86.91 % Maximal term depth : 3 ( 1 avg) % 86.89/86.91 % Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty) % 86.89/86.91 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty) % 86.89/86.91 % Number of variables : 38 ( 36 !; 2 ?) % 86.89/86.91 % SPC : FOF_THM_RFO_SEQ % 86.89/86.91 % 86.89/86.91 % Comments : Problem generated by the SAD system [VLP07] % 86.89/86.91 %------------------------------------------------------------------------------ % 86.89/86.91 fof(mNatSort,axiom, % 86.89/86.91 ! [W0] : % 86.89/86.91 ( aNaturalNumber0(W0) % 86.89/86.91 => $true ) ). % 86.89/86.91 % 86.89/86.91 fof(mSortsC,axiom, % 86.89/86.92 aNaturalNumber0(sz00) ). % 86.89/86.92 % 86.89/86.92 fof(mSortsC_01,axiom, % 86.89/86.92 ( aNaturalNumber0(sz10) % 86.89/86.92 & sz10 != sz00 ) ). % 86.89/86.92 % 86.89/86.92 fof(mSortsB,axiom, % 86.89/86.92 ! [W0,W1] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) ) % 86.89/86.92 => aNaturalNumber0(sdtpldt0(W0,W1)) ) ). % 86.89/86.92 % 86.89/86.92 fof(mSortsB_02,axiom, % 86.89/86.92 ! [W0,W1] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) ) % 86.89/86.92 => aNaturalNumber0(sdtasdt0(W0,W1)) ) ). % 86.89/86.92 % 86.89/86.92 fof(mAddComm,axiom, % 86.89/86.92 ! [W0,W1] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) ) % 86.89/86.92 => sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) ). % 86.89/86.92 % 86.89/86.92 fof(mAddAsso,axiom, % 86.89/86.92 ! [W0,W1,W2] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) % 86.89/86.92 & aNaturalNumber0(W2) ) % 86.89/86.92 => sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) ). % 86.89/86.92 % 86.89/86.92 fof(m_AddZero,axiom, % 86.89/86.92 ! [W0] : % 86.89/86.92 ( aNaturalNumber0(W0) % 86.89/86.92 => ( sdtpldt0(W0,sz00) = W0 % 86.89/86.92 & W0 = sdtpldt0(sz00,W0) ) ) ). % 86.89/86.92 % 86.89/86.92 fof(mMulComm,axiom, % 86.89/86.92 ! [W0,W1] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) ) % 86.89/86.92 => sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) ). % 86.89/86.92 % 86.89/86.92 fof(mMulAsso,axiom, % 86.89/86.92 ! [W0,W1,W2] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) % 86.89/86.92 & aNaturalNumber0(W2) ) % 86.89/86.92 => sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) ). % 86.89/86.92 % 86.89/86.92 fof(m_MulUnit,axiom, % 86.89/86.92 ! [W0] : % 86.89/86.92 ( aNaturalNumber0(W0) % 86.89/86.92 => ( sdtasdt0(W0,sz10) = W0 % 86.89/86.92 & W0 = sdtasdt0(sz10,W0) ) ) ). % 86.89/86.92 % 86.89/86.92 fof(m_MulZero,axiom, % 86.89/86.92 ! [W0] : % 86.89/86.92 ( aNaturalNumber0(W0) % 86.89/86.92 => ( sdtasdt0(W0,sz00) = sz00 % 86.89/86.92 & sz00 = sdtasdt0(sz00,W0) ) ) ). % 86.89/86.92 % 86.89/86.92 fof(mAMDistr,axiom, % 86.89/86.92 ! [W0,W1,W2] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) % 86.89/86.92 & aNaturalNumber0(W2) ) % 86.89/86.92 => ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)) % 86.89/86.92 & sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ). % 86.89/86.92 % 86.89/86.92 fof(mAddCanc,axiom, % 86.89/86.92 ! [W0,W1,W2] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) % 86.89/86.92 & aNaturalNumber0(W2) ) % 86.89/86.92 => ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2) % 86.89/86.92 | sdtpldt0(W1,W0) = sdtpldt0(W2,W0) ) % 86.89/86.92 => W1 = W2 ) ) ). % 86.89/86.92 % 86.89/86.92 fof(mMulCanc,axiom, % 86.89/86.92 ! [W0] : % 86.89/86.92 ( aNaturalNumber0(W0) % 86.89/86.92 => ( W0 != sz00 % 86.89/86.92 => ! [W1,W2] : % 86.89/86.92 ( ( aNaturalNumber0(W1) % 86.89/86.92 & aNaturalNumber0(W2) ) % 86.89/86.92 => ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2) % 86.89/86.92 | sdtasdt0(W1,W0) = sdtasdt0(W2,W0) ) % 86.89/86.92 => W1 = W2 ) ) ) ) ). % 86.89/86.92 % 86.89/86.92 fof(mZeroAdd,axiom, % 86.89/86.92 ! [W0,W1] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) ) % 86.89/86.92 => ( sdtpldt0(W0,W1) = sz00 % 86.89/86.92 => ( W0 = sz00 % 86.89/86.92 & W1 = sz00 ) ) ) ). % 86.89/86.92 % 86.89/86.92 fof(mZeroMul,axiom, % 86.89/86.92 ! [W0,W1] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) ) % 86.89/86.92 => ( sdtasdt0(W0,W1) = sz00 % 86.89/86.92 => ( W0 = sz00 % 86.89/86.92 | W1 = sz00 ) ) ) ). % 86.89/86.92 % 86.89/86.92 fof(mDefLE,definition, % 86.89/86.92 ! [W0,W1] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) ) % 86.89/86.92 => ( sdtlseqdt0(W0,W1) % 86.89/86.92 <=> ? [W2] : % 86.89/86.92 ( aNaturalNumber0(W2) % 86.89/86.92 & sdtpldt0(W0,W2) = W1 ) ) ) ). % 86.89/86.92 % 86.89/86.92 fof(mDefDiff,definition, % 86.89/86.92 ! [W0,W1] : % 86.89/86.92 ( ( aNaturalNumber0(W0) % 86.89/86.92 & aNaturalNumber0(W1) ) % 86.89/86.92 => ( sdtlseqdt0(W0,W1) % 86.89/86.92 => ! [W2] : % 86.89/86.92 ( W2 = sdtmndt0(W1,W0) % 86.89/86.92 <=> ( aNaturalNumber0(W2) % 86.89/86.92 & sdtpldt0(W0,W2) = W1 ) ) ) ) ). % 86.89/86.92 % 86.89/86.92 fof(m__718,hypothesis, % 86.89/86.92 aNaturalNumber0(xm) ). % 86.89/86.92 % 86.89/86.92 fof(m__,conjecture, % 86.89/86.92 ( ? [W0] : % 86.89/86.92 ( aNaturalNumber0(W0) % 86.89/86.92 & sdtpldt0(xm,W0) = xm ) % 86.89/86.92 | sdtlseqdt0(xm,xm) ) ). % 86.89/86.92 % 86.89/86.92 %------------------------------------------------------------------------------ % 86.89/86.92 %------------------------------------------- % 86.89/86.92 % Proof found % 86.89/86.92 % SZS status Theorem for theBenchmark % 86.89/86.92 % SZS output start Proof % 86.89/86.92 %ClaNum:47(EqnAxiom:14) % 86.89/86.92 %VarNum:181(SingletonVarNum:61) % 86.89/86.92 %MaxLitNum:6 % 86.89/86.92 %MaxfuncDepth:2 % 86.89/86.92 %SharedTerms:8 % 86.89/86.92 %goalClause: 19 26 % 86.89/86.92 %singleGoalClaCount:1 % 86.89/86.92 [15]P1(a1) % 86.89/86.92 [16]P1(a6) % 86.89/86.92 [17]P1(a7) % 86.89/86.92 [18]~E(a1,a6) % 86.89/86.92 [19]~P2(a7,a7) % 86.89/86.92 [20]~P1(x201)+E(f2(a1,x201),a1) % 86.89/86.92 [21]~P1(x211)+E(f2(x211,a1),a1) % 86.89/86.92 [22]~P1(x221)+E(f4(a1,x221),x221) % 86.89/86.92 [23]~P1(x231)+E(f2(a6,x231),x231) % 86.89/86.92 [24]~P1(x241)+E(f4(x241,a1),x241) % 86.89/86.92 [25]~P1(x251)+E(f2(x251,a6),x251) % 86.89/86.92 [26]~P1(x261)+~E(f4(a7,x261),a7) % 86.89/86.92 [30]~P1(x302)+~P1(x301)+E(f4(x301,x302),f4(x302,x301)) % 86.89/86.92 [31]~P1(x312)+~P1(x311)+E(f2(x311,x312),f2(x312,x311)) % 86.89/86.92 [32]~P1(x322)+~P1(x321)+P1(f4(x321,x322)) % 86.89/86.92 [33]~P1(x332)+~P1(x331)+P1(f2(x331,x332)) % 86.89/86.92 [27]~P1(x272)+~P1(x271)+E(x271,a1)+~E(f4(x272,x271),a1) % 86.89/86.92 [28]~P1(x282)+~P1(x281)+E(x281,a1)+~E(f4(x281,x282),a1) % 86.89/86.92 [36]~P1(x362)+~P1(x361)+~P2(x361,x362)+P1(f3(x361,x362)) % 86.89/86.92 [42]~P1(x422)+~P1(x421)+~P2(x421,x422)+E(f4(x421,f3(x421,x422)),x422) % 86.89/86.92 [44]~P1(x443)+~P1(x442)+~P1(x441)+E(f4(f4(x441,x442),x443),f4(x441,f4(x442,x443))) % 86.89/86.92 [45]~P1(x453)+~P1(x452)+~P1(x451)+E(f2(f2(x451,x452),x453),f2(x451,f2(x452,x453))) % 86.89/86.92 [46]~P1(x463)+~P1(x462)+~P1(x461)+E(f4(f2(x461,x462),f2(x461,x463)),f2(x461,f4(x462,x463))) % 86.89/86.92 [47]~P1(x472)+~P1(x473)+~P1(x471)+E(f4(f2(x471,x472),f2(x473,x472)),f2(f4(x471,x473),x472)) % 86.89/86.92 [29]~P1(x291)+~P1(x292)+E(x291,a1)+E(x292,a1)+~E(f2(x292,x291),a1) % 86.89/86.92 [34]~P1(x342)+~P1(x341)+~P1(x343)+P2(x341,x342)+~E(f4(x341,x343),x342) % 86.89/86.92 [35]~P1(x353)+~P1(x352)+~P2(x353,x352)+P1(x351)+~E(x351,f5(x352,x353)) % 86.89/86.92 [37]~P1(x372)+~P1(x371)+~P1(x373)+E(x371,x372)+~E(f4(x373,x371),f4(x373,x372)) % 86.89/86.92 [38]~P1(x382)+~P1(x383)+~P1(x381)+E(x381,x382)+~E(f4(x381,x383),f4(x382,x383)) % 86.89/86.92 [41]~P1(x413)+~P1(x411)+~P2(x411,x413)+~E(x412,f5(x413,x411))+E(f4(x411,x412),x413) % 86.89/86.92 [39]~P1(x392)+~P1(x391)+~P1(x393)+E(x391,x392)+~E(f2(x393,x391),f2(x393,x392))+E(x393,a1) % 86.89/86.92 [40]~P1(x402)+~P1(x403)+~P1(x401)+E(x401,x402)+~E(f2(x401,x403),f2(x402,x403))+E(x403,a1) % 86.89/86.92 [43]~P1(x432)+~P1(x433)+~P1(x431)+~P2(x433,x432)+~E(f4(x433,x431),x432)+E(x431,f5(x432,x433)) % 86.89/86.92 %EqnAxiom % 86.89/86.92 [1]E(x11,x11) % 86.89/86.92 [2]E(x22,x21)+~E(x21,x22) % 86.89/86.92 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 86.89/86.92 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 86.89/86.92 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 86.89/86.92 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63)) % 86.89/86.92 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72)) % 86.89/86.92 [8]~E(x81,x82)+E(f3(x81,x83),f3(x82,x83)) % 86.89/86.92 [9]~E(x91,x92)+E(f3(x93,x91),f3(x93,x92)) % 86.89/86.92 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103)) % 86.89/86.92 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112)) % 86.89/86.92 [12]~P1(x121)+P1(x122)+~E(x121,x122) % 86.89/86.92 [13]P2(x132,x133)+~E(x131,x132)+~P2(x131,x133) % 86.89/86.92 [14]P2(x143,x142)+~E(x141,x142)+~P2(x143,x141) % 86.89/86.92 % 86.89/86.92 %------------------------------------------- % 86.89/86.93 cnf(48,plain, % 86.89/86.93 (P2(x481,f4(x481,x482))+~P1(f4(x481,x482))+~P1(x481)+~P1(x482)), % 86.89/86.93 inference(equality_inference,[],[34])). % 86.89/86.93 cnf(49,plain, % 86.89/86.93 (~P2(x491,x492)+~P1(x491)+~P1(x492)+P1(f5(x492,x491))), % 86.89/86.93 inference(equality_inference,[],[35])). % 86.89/86.93 cnf(55,plain, % 86.89/86.93 (~P2(x551,f4(x551,x552))+~P1(f4(x551,x552))+~P1(x551)+~P1(x552)+E(x552,f5(f4(x551,x552),x551))), % 86.89/86.93 inference(equality_inference,[],[43])). % 86.89/86.93 cnf(56,plain, % 86.89/86.93 (P2(a1,f4(a1,a1))+~P1(f4(a1,a1))), % 86.89/86.93 inference(scs_inference,[],[15,48])). % 86.89/86.93 cnf(64,plain, % 86.89/86.93 (~P1(f4(a7,a7))+~E(f4(a7,a7),a7)), % 86.89/86.93 inference(scs_inference,[],[19,17,48,13,14])). % 86.89/86.93 cnf(92,plain, % 86.89/86.93 (E(f2(a1,f4(a7,a7)),a1)), % 86.89/86.93 inference(scs_inference,[],[17,20,32])). % 86.89/86.93 cnf(93,plain, % 86.89/86.93 (E(a1,f2(a1,f4(a7,a7)))), % 86.89/86.93 inference(scs_inference,[],[92,2])). % 86.89/86.93 cnf(111,plain, % 86.89/86.93 (E(f2(f2(a1,f4(a7,a7)),a1),a1)), % 86.89/86.93 inference(scs_inference,[],[93,15,21,12])). % 86.89/86.93 cnf(112,plain, % 86.89/86.93 (E(a1,f2(f2(a1,f4(a7,a7)),a1))), % 86.89/86.93 inference(scs_inference,[],[111,2])). % 86.89/86.93 cnf(130,plain, % 86.89/86.93 (E(f4(a1,f2(a7,a7)),f2(a7,a7))), % 86.89/86.93 inference(scs_inference,[],[17,22,33])). % 86.89/86.93 cnf(131,plain, % 86.89/86.93 (E(f2(a7,a7),f4(a1,f2(a7,a7)))), % 86.89/86.93 inference(scs_inference,[],[130,2])). % 86.89/86.93 cnf(132,plain, % 86.89/86.93 (~P1(f4(a1,f2(a7,a7)))+P1(f2(a7,a7))), % 86.89/86.93 inference(scs_inference,[],[130,2,12])). % 86.89/86.93 cnf(135,plain, % 86.89/86.93 (~P1(f4(a1,f2(a7,a7)))+E(f2(a7,a7),f5(f2(a7,a7),a1))), % 86.89/86.93 inference(scs_inference,[],[15,130,2,12,34,43])). % 86.89/86.93 cnf(137,plain, % 86.89/86.93 (E(f4(a1,f2(a7,a7)),f5(f2(a7,a7),a1))+~P1(f4(a1,f2(a7,a7)))), % 86.89/86.93 inference(scs_inference,[],[15,130,2,12,34,43,3])). % 86.89/86.93 cnf(138,plain, % 86.89/86.93 (P2(f2(f2(a1,f4(a7,a7)),a1),f2(a7,a7))+~P1(f4(a1,f2(a7,a7)))), % 86.89/86.93 inference(scs_inference,[],[15,112,130,2,12,34,43,3,13])). % 86.89/86.93 cnf(139,plain, % 86.89/86.93 (P2(a1,f4(a1,f2(a7,a7)))+~P1(f4(a1,f2(a7,a7)))), % 86.89/86.93 inference(scs_inference,[],[15,112,130,2,12,34,43,3,13,14])). % 86.89/86.93 cnf(144,plain, % 86.89/86.93 (~P1(f2(a7,a7))+P1(f4(a1,f2(a7,a7)))), % 86.89/86.93 inference(scs_inference,[],[131,12])). % 86.89/86.93 cnf(146,plain, % 86.89/86.93 (~P1(f2(a7,a7))+E(f2(a7,a7),f5(f2(a7,a7),a1))), % 86.89/86.93 inference(scs_inference,[],[131,12,132,135])). % 86.89/86.93 cnf(149,plain, % 86.89/86.93 (E(f5(f2(a7,a7),a1),f2(a7,a7))+~P1(f2(a7,a7))), % 86.89/86.93 inference(scs_inference,[],[131,12,132,135,137,138,2])). % 86.89/86.93 cnf(170,plain, % 86.89/86.93 (E(f2(a6,f4(a7,a7)),f4(a7,a7))), % 86.89/86.93 inference(scs_inference,[],[17,23,32])). % 86.89/86.93 cnf(171,plain, % 86.89/86.93 (E(f4(a7,a7),f2(a6,f4(a7,a7)))), % 86.89/86.93 inference(scs_inference,[],[170,2])). % 86.89/86.93 cnf(172,plain, % 86.89/86.93 (~P1(f2(a6,f4(a7,a7)))+P1(f4(a7,a7))), % 86.89/86.93 inference(scs_inference,[],[170,2,12])). % 86.89/86.93 cnf(175,plain, % 86.89/86.93 (E(a7,f5(f4(a7,a7),a7))+~P1(f2(a6,f4(a7,a7)))), % 86.89/86.93 inference(scs_inference,[],[17,170,2,12,48,55])). % 86.89/86.93 cnf(177,plain, % 86.89/86.93 (P2(f5(f4(a7,a7),a7),f4(a7,a7))+~P1(f2(a6,f4(a7,a7)))), % 86.89/86.93 inference(scs_inference,[],[17,170,2,12,48,55,3,13])). % 86.89/86.93 cnf(181,plain, % 86.89/86.93 (~P1(f4(a7,a7))+P1(f2(a6,f4(a7,a7)))), % 86.89/86.93 inference(scs_inference,[],[171,12])). % 86.89/86.93 cnf(182,plain, % 86.89/86.93 (P2(a7,f2(a6,f4(a7,a7)))+~P1(f4(a7,a7))), % 86.89/86.93 inference(scs_inference,[],[17,171,12,34])). % 86.89/86.94 cnf(184,plain, % 86.89/86.94 (~P1(f4(a7,a7))+E(a7,f5(f2(a6,f4(a7,a7)),a7))), % 86.89/86.94 inference(scs_inference,[],[17,171,12,34,43])). % 86.89/86.94 cnf(186,plain, % 86.89/86.94 (P1(f4(a7,a7))+~P1(f4(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[17,171,12,34,43,172])). % 86.89/86.94 cnf(188,plain, % 86.89/86.94 (~P1(f4(a7,a7))+P2(f5(f4(a7,a7),a7),f4(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[17,171,12,34,43,172,175,177])). % 86.89/86.94 cnf(209,plain, % 86.89/86.94 (E(f4(f2(a7,a7),a1),f2(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[17,24,33])). % 86.89/86.94 cnf(210,plain, % 86.89/86.94 (E(f2(a7,a7),f4(f2(a7,a7),a1))), % 86.89/86.94 inference(scs_inference,[],[209,2])). % 86.89/86.94 cnf(211,plain, % 86.89/86.94 (E(f4(f2(a7,a7),a1),f4(a1,f2(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[209,131,2,3])). % 86.89/86.94 cnf(213,plain, % 86.89/86.94 (P2(f2(a7,a7),f2(a7,a7))+~P1(f4(f2(a7,a7),a1))), % 86.89/86.94 inference(scs_inference,[],[15,209,131,2,3,12,34])). % 86.89/86.94 cnf(218,plain, % 86.89/86.94 (~P1(f4(f2(a7,a7),a1))+E(f5(f2(a7,a7),a1),f2(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[15,209,131,2,3,12,34,43,146,149])). % 86.89/86.94 cnf(224,plain, % 86.89/86.94 (E(f4(a1,f2(a7,a7)),f4(f2(a7,a7),a1))), % 86.89/86.94 inference(scs_inference,[],[211,2])). % 86.89/86.94 cnf(226,plain, % 86.89/86.94 (~P1(f2(a7,a7))+P2(f2(a7,a7),f2(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[210,211,2,12,213])). % 86.89/86.94 cnf(236,plain, % 86.89/86.94 (E(f5(f2(a7,a7),a1),f4(a1,f2(a7,a7)))+~P1(f4(f2(a7,a7),a1))), % 86.89/86.94 inference(scs_inference,[],[211,12,139,138,137,2])). % 86.89/86.94 cnf(243,plain, % 86.89/86.94 (~P1(f4(a1,f2(a7,a7)))+P2(f2(a7,a7),f2(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[224,12,218,236,213])). % 86.89/86.94 cnf(249,plain, % 86.89/86.94 (~P2(f2(a7,a7),f2(a7,a7))+~P1(f2(a7,a7))+E(a1,f5(f2(a7,a7),f2(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[17,15,209,224,43])). % 86.89/86.94 cnf(260,plain, % 86.89/86.94 (E(f2(f4(a7,a7),a6),f4(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[17,25,32])). % 86.89/86.94 cnf(261,plain, % 86.89/86.94 (E(f4(a7,a7),f2(f4(a7,a7),a6))), % 86.89/86.94 inference(scs_inference,[],[260,2])). % 86.89/86.94 cnf(262,plain, % 86.89/86.94 (E(f2(a6,f4(a7,a7)),f2(f4(a7,a7),a6))), % 86.89/86.94 inference(scs_inference,[],[170,260,2,3])). % 86.89/86.94 cnf(263,plain, % 86.89/86.94 (~P1(f2(f4(a7,a7),a6))+P1(f4(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[170,260,2,3,12])). % 86.89/86.94 cnf(266,plain, % 86.89/86.94 (E(a7,f5(f4(a7,a7),a7))+~P1(f2(f4(a7,a7),a6))), % 86.89/86.94 inference(scs_inference,[],[17,170,260,2,3,12,48,55])). % 86.89/86.94 cnf(268,plain, % 86.89/86.94 (~P1(f2(f4(a7,a7),a6))+P1(f2(a6,f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[17,170,260,2,3,12,48,55,181])). % 86.89/86.94 cnf(272,plain, % 86.89/86.94 (P2(f5(f4(a7,a7),a7),f2(a6,f4(a7,a7)))+~P1(f2(f4(a7,a7),a6))), % 86.89/86.94 inference(scs_inference,[],[19,17,170,260,2,3,12,48,55,181,182,188,14,13])). % 86.89/86.94 cnf(276,plain, % 86.89/86.94 (~P1(f4(a7,a7))+P1(f2(f4(a7,a7),a6))), % 86.89/86.94 inference(scs_inference,[],[261,262,2,12])). % 86.89/86.94 cnf(292,plain, % 86.89/86.94 (E(f5(f2(f4(a7,a7),a6),a7),a7)+~P1(f2(a6,f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[17,262,261,12,34,43,268,272,2])). % 86.89/86.94 cnf(312,plain, % 86.89/86.94 (~E(f4(a7,f2(a7,a7)),a7)), % 86.89/86.94 inference(scs_inference,[],[17,26,33])). % 86.89/86.94 cnf(439,plain, % 86.89/86.94 (~E(a7,f4(a7,a7))+~P1(f4(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[64,2])). % 86.89/86.94 cnf(471,plain, % 86.89/86.94 (~E(a7,f4(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[17,439,32])). % 86.89/86.94 cnf(472,plain, % 86.89/86.94 (~E(a7,f2(a6,f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[170,471,3])). % 86.89/86.94 cnf(619,plain, % 86.89/86.94 (P1(f4(a1,f2(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[17,144,33])). % 86.89/86.94 cnf(620,plain, % 86.89/86.94 (P1(f2(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[619,132])). % 86.89/86.94 cnf(629,plain, % 86.89/86.94 (P2(f2(a7,a7),f2(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[619,243])). % 86.89/86.94 cnf(651,plain, % 86.89/86.94 (P2(f2(a7,a7),f2(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[620,226])). % 86.89/86.94 cnf(660,plain, % 86.89/86.94 (E(a1,f5(f2(a7,a7),f2(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[620,629,249])). % 86.89/86.94 cnf(685,plain, % 86.89/86.94 (E(f5(f2(a7,a7),f2(a7,a7)),a1)), % 86.89/86.94 inference(scs_inference,[],[660,2])). % 86.89/86.94 cnf(703,plain, % 86.89/86.94 (~P1(f2(f4(a7,a7),a6))+P1(f2(f4(a7,a7),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[263,33])). % 86.89/86.94 cnf(726,plain, % 86.89/86.94 (P1(f2(f4(a7,a7),a6))), % 86.89/86.94 inference(scs_inference,[],[17,276,32])). % 86.89/86.94 cnf(727,plain, % 86.89/86.94 (P1(f4(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[726,263])). % 86.89/86.94 cnf(729,plain, % 86.89/86.94 (E(a7,f5(f4(a7,a7),a7))), % 86.89/86.94 inference(scs_inference,[],[726,266])). % 86.89/86.94 cnf(730,plain, % 86.89/86.94 (P1(f2(a6,f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[726,268])). % 86.89/86.94 cnf(734,plain, % 86.89/86.94 (P2(f5(f4(a7,a7),a7),f2(a6,f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[726,272])). % 86.89/86.94 cnf(738,plain, % 86.89/86.94 (P1(f2(f4(a7,a7),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[726,703])). % 86.89/86.94 cnf(746,plain, % 86.89/86.94 (P1(f4(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[730,172])). % 86.89/86.94 cnf(748,plain, % 86.89/86.94 (E(a7,f5(f4(a7,a7),a7))), % 86.89/86.94 inference(scs_inference,[],[730,175])). % 86.89/86.94 cnf(749,plain, % 86.89/86.94 (P2(f5(f4(a7,a7),a7),f4(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[730,177])). % 86.89/86.94 cnf(753,plain, % 86.89/86.94 (E(a7,f5(f2(a6,f4(a7,a7)),a7))), % 86.89/86.94 inference(scs_inference,[],[727,184])). % 86.89/86.94 cnf(754,plain, % 86.89/86.94 (P1(f4(a7,a7))), % 86.89/86.94 inference(scs_inference,[],[727,186])). % 86.89/86.94 cnf(768,plain, % 86.89/86.94 (E(f5(f2(f4(a7,a7),a6),a7),a7)), % 86.89/86.94 inference(scs_inference,[],[730,292])). % 86.89/86.94 cnf(775,plain, % 86.89/86.94 (P1(f5(f4(a7,a7),a7))), % 86.89/86.94 inference(scs_inference,[],[17,312,734,262,729,2,14,3,12])). % 86.89/86.94 cnf(778,plain, % 86.89/86.94 (P2(f4(a7,a7),f4(f4(a7,a7),f4(a7,a7)))+~P1(f4(f4(a7,a7),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[17,312,727,734,262,729,2,14,3,12,49,48])). % 86.89/86.94 cnf(791,plain, % 86.89/86.94 (E(a1,f5(f4(a1,a1),a1))+~P2(a1,f4(a1,a1))+~P1(f4(a1,a1))), % 86.89/86.94 inference(scs_inference,[],[17,15,753,12,55])). % 86.89/86.94 cnf(1083,plain, % 86.89/86.94 (~P1(f4(f4(a7,a7),f4(a7,a7)))+P2(f2(a6,f4(a7,a7)),f4(f4(a7,a7),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[171,778,13])). % 86.89/86.94 cnf(1295,plain, % 86.89/86.94 (P2(f2(a6,f4(a7,a7)),f4(f4(a7,a7),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[746,1083,32])). % 86.89/86.94 cnf(1296,plain, % 86.89/86.94 (P2(f4(a7,a7),f4(f4(a7,a7),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[1295,170,13])). % 86.89/86.94 cnf(1320,plain, % 86.89/86.94 (E(f2(a6,f4(a7,a7)),f5(f4(f4(a7,a7),f4(a7,a7)),f4(a7,a7)))+~P1(f4(f4(a7,a7),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[727,1296,170,55,2,12,3])). % 86.89/86.94 cnf(1711,plain, % 86.89/86.94 (E(f2(a6,f4(a7,a7)),f5(f4(f4(a7,a7),f4(a7,a7)),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[746,1320,32])). % 86.89/86.94 cnf(1712,plain, % 86.89/86.94 (E(f5(f4(f4(a7,a7),f4(a7,a7)),f4(a7,a7)),f2(a6,f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[1711,2])). % 86.89/86.94 cnf(1713,plain, % 86.89/86.94 (E(f4(a7,a7),f5(f4(f4(a7,a7),f4(a7,a7)),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[171,1711,2,3])). % 86.89/86.94 cnf(1717,plain, % 86.89/86.94 (~E(a7,f5(f4(f4(a7,a7),f4(a7,a7)),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[472,1713,1712,2,3])). % 86.89/86.94 cnf(1816,plain, % 86.89/86.94 (~P1(f4(f4(a7,a7),f4(a7,a7)))+~E(f4(f4(a7,a7),a7),f4(f4(a7,a7),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[746,1296,17,1717,43])). % 86.89/86.94 cnf(1882,plain, % 86.89/86.94 (~E(f4(f4(a7,a7),a7),f4(f4(a7,a7),f4(a7,a7)))), % 86.89/86.94 inference(scs_inference,[],[754,1816,32])). % 86.89/86.94 cnf(2053,plain, % 86.89/86.94 (E(a1,f5(f4(a1,a1),a1))+~P1(f4(a1,a1))), % 86.89/86.94 inference(scs_inference,[],[791,56])). % 86.89/86.94 cnf(2069,plain, % 86.89/86.94 (E(f5(f4(a1,a1),a1),a1)+~P1(f4(a1,a1))), % 86.89/86.94 inference(scs_inference,[],[2053,2])). % 86.89/86.94 cnf(2085,plain, % 86.89/86.94 (E(f5(f4(a1,a1),a1),a1)), % 86.89/86.94 inference(scs_inference,[],[15,2069,32])). % 86.89/86.94 cnf(2087,plain, % 86.89/86.94 (P1(f5(f4(a1,a1),a1))), % 86.89/86.94 inference(scs_inference,[],[15,2085,2,12])). % 86.89/86.94 cnf(2411,plain, % 86.89/86.94 (E(a1,f2(a1,a7))), % 86.89/86.94 inference(scs_inference,[],[17,2,20])). % 86.89/86.94 cnf(2412,plain, % 86.89/86.94 (E(f2(a1,a7),a1)), % 86.89/86.94 inference(scs_inference,[],[2411,2])). % 86.89/86.94 cnf(2414,plain, % 86.89/86.94 (P1(f2(a1,a7))), % 86.89/86.94 inference(scs_inference,[],[15,685,2411,2,3,12])). % 86.89/86.94 cnf(2819,plain, % 86.89/86.94 (~E(f4(a7,f2(f4(a7,a7),f4(a7,a7))),a7)), % 86.89/86.94 inference(scs_inference,[],[738,2414,22,23,24,25,20,21,26])). % 86.89/86.94 cnf(2832,plain, % 86.89/86.94 (P1(f4(f2(a1,a7),f2(a1,a7)))), % 86.89/86.94 inference(scs_inference,[],[2412,738,1882,2414,22,23,24,25,20,21,26,4,5,6,8,9,10,11,7,2,33,32])). % 86.89/86.94 cnf(2877,plain, % 86.89/86.94 (E(f2(a6,a6),a6)), % 86.89/86.94 inference(scs_inference,[],[2087,2832,16,21,26,25])). % 86.89/86.94 cnf(2896,plain, % 86.89/86.94 (P1(f2(a6,a6))), % 86.89/86.94 inference(scs_inference,[],[2087,2832,2819,748,16,620,21,26,25,24,23,20,6,11,22,7,5,9,4,10,8,2,33])). % 86.89/86.94 cnf(2898,plain, % 86.89/86.94 (P1(f4(a6,a6))), % 86.89/86.94 inference(scs_inference,[],[2087,2832,2819,748,16,620,21,26,25,24,23,20,6,11,22,7,5,9,4,10,8,2,33,32])). % 86.89/86.94 cnf(2915,plain, % 86.89/86.94 (~E(f4(a1,a1),f4(a1,a6))), % 86.89/86.94 inference(scs_inference,[],[19,2087,2832,775,2819,749,651,768,748,18,112,16,620,727,15,21,26,25,24,23,20,6,11,22,7,5,9,4,10,8,2,33,32,3,13,14,45,36,44,46,47,42,37])). % 86.89/86.94 cnf(2977,plain, % 86.89/86.94 (P1(f4(f4(a6,a6),f4(a6,a6)))), % 86.89/86.94 inference(scs_inference,[],[2898,2915,2877,26,20,24,25,21,23,22,6,7,11,9,10,8,5,4,2,33,32])). % 86.89/86.94 cnf(3171,plain, % 86.89/86.94 (E(f4(a7,a1),a7)), % 86.89/86.94 inference(scs_inference,[],[2977,15,17,25,26,21,20,22,24])). % 86.89/86.94 cnf(4389,plain, % 86.89/86.94 ($false), % 86.89/86.94 inference(scs_inference,[],[3171,2896,15,20,21,26]), % 86.89/86.94 ['proof']). % 86.89/86.94 % SZS output end Proof % 86.89/86.94 % Total time :86.280000s %------------------------------------------------------------------------------