%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ129+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 : 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 13:42:25 EDT 2024 % Result : Theorem 58.72s 58.84s % Output : CNFRefutation 58.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PUZ129+2 : 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.13/0.34 % Computer : n024.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 : Tue Jun 18 10:01:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.21/0.56 start to proof:theBenchmark % 58.72/58.83 %------------------------------------------- % 58.72/58.83 % File :CSE---1.7 % 58.72/58.83 % Problem :theBenchmark % 58.72/58.83 % Transform :cnf % 58.72/58.83 % Format :tptp:raw % 58.72/58.83 % Command :java -jar mcs_scs.jar %d %s % 58.72/58.83 % 58.72/58.83 % Result :Theorem 58.140000s % 58.72/58.83 % Output :CNFRefutation 58.140000s % 58.72/58.83 %------------------------------------------- % 58.72/58.83 %------------------------------------------------------------------------------ % 58.72/58.83 % File : PUZ129+2 : TPTP v8.2.0. Released v4.0.0. % 58.72/58.83 % Domain : Puzzles % 58.72/58.83 % Problem : The grocer is not a cyclist % 58.72/58.83 % Version : Especial. % 58.72/58.83 % Theorem formulation : Converted from ACE by the APE [FKK08]. % 58.72/58.83 % English : If every honest and industrious person is healthy, and no grocer % 58.72/58.83 % is healthy, and every industrious grocer is honest, and every % 58.72/58.83 % cyclist is industrious, and every unhealthy cyclist is dishonest, % 58.72/58.84 % and no healthy person is unhealthy, and no honest person is % 58.72/58.84 % dishonest, and every grocer is a person, and every cyclist is a % 58.72/58.84 % person then no grocer is a cyclist. % 58.72/58.84 % 58.72/58.84 % Refs : [FKK08] Fuchs et al. (2008), Attempto Controlled English for K % 58.72/58.84 % Source : [TPTP] % 58.72/58.84 % Names : % 58.72/58.84 % 58.72/58.84 % Status : Theorem % 58.72/58.84 % Rating : 0.14 v8.2.0, 0.11 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.03 v7.3.0, 0.14 v7.1.0, 0.09 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.04 v6.2.0, 0.12 v6.1.0, 0.20 v6.0.0, 0.13 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.22 v5.2.0, 0.10 v5.0.0, 0.04 v4.1.0, 0.09 v4.0.0 % 58.72/58.84 % Syntax : Number of formulae : 1 ( 0 unt; 0 def) % 58.72/58.84 % Number of atoms : 36 ( 10 equ) % 58.72/58.84 % Maximal formula atoms : 36 ( 36 avg) % 58.72/58.84 % Number of connectives : 39 ( 4 ~; 0 |; 24 &) % 58.72/58.84 % ( 0 <=>; 11 =>; 0 <=; 0 <~>) % 58.72/58.84 % Maximal formula depth : 14 ( 14 avg) % 58.72/58.84 % Maximal term depth : 1 ( 1 avg) % 58.72/58.84 % Number of predicates : 5 ( 4 usr; 0 prp; 1-3 aty) % 58.72/58.84 % Number of functors : 6 ( 6 usr; 6 con; 0-0 aty) % 58.72/58.84 % Number of variables : 20 ( 10 !; 10 ?) % 58.72/58.84 % SPC : FOF_THM_RFO_SEQ % 58.72/58.84 % 58.72/58.84 % Comments : % 58.72/58.84 %------------------------------------------------------------------------------ % 58.72/58.84 fof(prove,conjecture, % 58.72/58.84 ( ( ! [A] : % 58.72/58.84 ( ( person(A) % 58.72/58.84 & property1(A,honest,pos) % 58.72/58.84 & property1(A,industrious,pos) ) % 58.72/58.84 => ? [B] : % 58.72/58.84 ( property1(B,healthy,pos) % 58.72/58.84 & A = B ) ) % 58.72/58.84 & ! [C] : % 58.72/58.84 ( grocer(C) % 58.72/58.84 => ~ ? [D] : % 58.72/58.84 ( property1(D,healthy,pos) % 58.72/58.84 & C = D ) ) % 58.72/58.84 & ! [E] : % 58.72/58.84 ( ( grocer(E) % 58.72/58.84 & property1(E,industrious,pos) ) % 58.72/58.84 => ? [F] : % 58.72/58.84 ( property1(F,honest,pos) % 58.72/58.84 & E = F ) ) % 58.72/58.84 & ! [G] : % 58.72/58.84 ( cyclist(G) % 58.72/58.84 => ? [H] : % 58.72/58.84 ( property1(H,industrious,pos) % 58.72/58.84 & G = H ) ) % 58.72/58.84 & ! [I] : % 58.72/58.84 ( ( cyclist(I) % 58.72/58.84 & property1(I,unhealthy,pos) ) % 58.72/58.84 => ? [J] : % 58.72/58.84 ( property1(J,dishonest,pos) % 58.72/58.84 & I = J ) ) % 58.72/58.84 & ! [K] : % 58.72/58.84 ( ( person(K) % 58.72/58.84 & property1(K,healthy,pos) ) % 58.72/58.84 => ~ ? [L] : % 58.72/58.84 ( property1(L,unhealthy,pos) % 58.72/58.84 & K = L ) ) % 58.72/58.84 & ! [M] : % 58.72/58.84 ( ( person(M) % 58.72/58.84 & property1(M,honest,pos) ) % 58.72/58.84 => ~ ? [N] : % 58.72/58.84 ( property1(N,dishonest,pos) % 58.72/58.84 & M = N ) ) % 58.72/58.84 & ! [O] : % 58.72/58.84 ( grocer(O) % 58.72/58.84 => ? [P] : % 58.72/58.84 ( person(P) % 58.72/58.84 & O = P ) ) % 58.72/58.84 & ! [Q] : % 58.72/58.84 ( cyclist(Q) % 58.72/58.84 => ? [R] : % 58.72/58.84 ( person(R) % 58.72/58.84 & Q = R ) ) ) % 58.72/58.84 => ! [S] : % 58.72/58.84 ( grocer(S) % 58.72/58.84 => ~ ? [T] : % 58.72/58.84 ( cyclist(T) % 58.72/58.84 & S = T ) ) ) ). % 58.72/58.84 % 58.72/58.84 %------------------------------------------------------------------------------ % 58.72/58.84 %------------------------------------------- % 58.72/58.84 % Proof found % 58.72/58.84 % SZS status Theorem for theBenchmark % 58.72/58.84 % SZS output start Proof % 58.72/58.84 %ClaNum:35(EqnAxiom:16) % 58.72/58.84 %VarNum:52(SingletonVarNum:18) % 58.72/58.84 %MaxLitNum:5 % 58.72/58.84 %MaxfuncDepth:1 % 58.72/58.84 %SharedTerms:14 % 58.72/58.84 %goalClause: 17 18 19 20 % 58.72/58.84 %singleGoalClaCount:4 % 58.72/58.84 [17]E(a1,a2) % 58.72/58.84 [18]P1(a5000) % 58.72/58.84 [19]P3(a2) % 58.72/58.84 [20]P2(a1) % 58.72/58.84 [21]~P2(x211)+E(f4(x211),x211)+~P1(a5000) % 58.72/58.84 [22]~P3(x221)+E(f7(x221),x221)+~P1(a5000) % 58.72/58.84 [23]~P2(x231)+E(f9(x231),x231)+~P1(a5000) % 58.72/58.84 [24]~P3(x241)+P4(f7(x241))+~P1(a5000) % 58.72/58.84 [25]~P2(x251)+P4(f9(x251))+~P1(a5000) % 58.72/58.85 [26]~P2(x261)+P5(f4(x261),a10,a13)+~P1(a5000) % 58.72/58.85 [28]~P3(x281)+E(f5(x281),x281)+~P5(x281,a10,a13)+~P1(a5000) % 58.72/58.85 [29]~P2(x291)+E(f8(x291),x291)+~P5(x291,a14,a13)+~P1(a5000) % 58.72/58.85 [30]~P3(x301)+~P5(x301,a10,a13)+P5(f5(x301),a12,a13)+~P1(a5000) % 58.72/58.85 [31]~P2(x311)+~P5(x311,a14,a13)+P5(f8(x311),a3,a13)+~P1(a5000) % 58.72/58.85 [27]~P3(x271)+~E(x271,x272)+~P5(x272,a11,a13)+~P1(a5000) % 58.72/58.85 [34]~P4(x341)+E(f6(x341),x341)+~P5(x341,a12,a13)+~P5(x341,a10,a13)+~P1(a5000) % 58.72/58.85 [35]~P4(x351)+~P5(x351,a12,a13)+~P5(x351,a10,a13)+P5(f6(x351),a11,a13)+~P1(a5000) % 58.72/58.85 [32]~P4(x321)+~E(x321,x322)+~P5(x322,a14,a13)+~P5(x321,a11,a13)+~P1(a5000) % 58.72/58.85 [33]~P4(x331)+~E(x331,x332)+~P5(x332,a3,a13)+~P5(x331,a12,a13)+~P1(a5000) % 58.72/58.85 %EqnAxiom % 58.72/58.85 [1]E(x11,x11) % 58.72/58.85 [2]E(x22,x21)+~E(x21,x22) % 58.72/58.85 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.72/58.85 [4]~E(x41,x42)+E(f4(x41),f4(x42)) % 58.72/58.85 [5]~E(x51,x52)+E(f7(x51),f7(x52)) % 58.72/58.85 [6]~E(x61,x62)+E(f9(x61),f9(x62)) % 58.72/58.85 [7]~E(x71,x72)+E(f6(x71),f6(x72)) % 58.72/58.85 [8]~E(x81,x82)+E(f8(x81),f8(x82)) % 58.72/58.85 [9]~E(x91,x92)+E(f5(x91),f5(x92)) % 58.72/58.85 [10]~P1(x101)+P1(x102)+~E(x101,x102) % 58.72/58.85 [11]~P3(x111)+P3(x112)+~E(x111,x112) % 58.72/58.85 [12]~P2(x121)+P2(x122)+~E(x121,x122) % 58.72/58.85 [13]P5(x132,x133,x134)+~E(x131,x132)+~P5(x131,x133,x134) % 58.72/58.85 [14]P5(x143,x142,x144)+~E(x141,x142)+~P5(x143,x141,x144) % 58.72/58.85 [15]P5(x153,x154,x152)+~E(x151,x152)+~P5(x153,x154,x151) % 58.72/58.85 [16]~P4(x161)+P4(x162)+~E(x161,x162) % 58.72/58.85 % 58.72/58.85 %------------------------------------------- % 58.72/58.86 cnf(36,plain, % 58.72/58.86 (~P3(x361)+~P5(x361,a11,a13)+~P1(a5000)), % 58.72/58.86 inference(equality_inference,[],[27])). % 58.72/58.86 cnf(38,plain, % 58.72/58.86 (~P4(x381)+~P5(x381,a3,a13)+~P5(x381,a12,a13)+~P1(a5000)), % 58.72/58.86 inference(equality_inference,[],[33])). % 58.72/58.86 cnf(39,plain, % 58.72/58.86 (~P3(x391)+~P5(x391,a11,a13)), % 58.72/58.86 inference(scs_inference,[],[18,36])). % 58.72/58.86 cnf(41,plain, % 58.72/58.86 (~P4(x411)+~P5(x411,a3,a13)+~P5(x411,a12,a13)), % 58.72/58.86 inference(scs_inference,[],[18,38])). % 58.72/58.86 cnf(42,plain, % 58.72/58.86 (E(a2,a1)), % 58.72/58.86 inference(scs_inference,[],[17,2])). % 58.72/58.86 cnf(43,plain, % 58.72/58.86 (E(f4(a1),a1)), % 58.72/58.86 inference(scs_inference,[],[17,18,20,2,21])). % 58.72/58.86 cnf(45,plain, % 58.72/58.86 (E(f7(a2),a2)), % 58.72/58.86 inference(scs_inference,[],[17,18,19,20,2,21,22])). % 58.72/58.86 cnf(47,plain, % 58.72/58.86 (E(f9(a1),a1)), % 58.72/58.86 inference(scs_inference,[],[17,18,19,20,2,21,22,23])). % 58.72/58.86 cnf(49,plain, % 58.72/58.86 (P3(a1)), % 58.72/58.86 inference(scs_inference,[],[17,18,19,20,2,21,22,23,11])). % 58.72/58.86 cnf(50,plain, % 58.72/58.86 (P2(a2)), % 58.72/58.86 inference(scs_inference,[],[17,18,19,20,2,21,22,23,11,12])). % 58.72/58.86 cnf(51,plain, % 58.72/58.86 (~P5(a1,a11,a13)), % 58.72/58.86 inference(scs_inference,[],[17,18,19,20,2,21,22,23,11,12,27])). % 58.72/58.86 cnf(58,plain, % 58.72/58.86 (~P2(x581)+E(f4(x581),x581)), % 58.72/58.86 inference(scs_inference,[],[18,21])). % 58.72/58.86 cnf(59,plain, % 58.72/58.86 (~P3(x591)+E(f7(x591),x591)), % 58.72/58.86 inference(scs_inference,[],[18,22])). % 58.72/58.86 cnf(60,plain, % 58.72/58.86 (~P2(x601)+E(f9(x601),x601)), % 58.72/58.86 inference(scs_inference,[],[18,23])). % 58.72/58.86 cnf(61,plain, % 58.72/58.86 (~P3(x611)+P4(f7(x611))), % 58.72/58.86 inference(scs_inference,[],[18,24])). % 58.72/58.86 cnf(62,plain, % 58.72/58.86 (~P2(x621)+P4(f9(x621))), % 58.72/58.86 inference(scs_inference,[],[18,25])). % 58.72/58.86 cnf(63,plain, % 58.72/58.86 (~P2(x631)+P5(f4(x631),a10,a13)), % 58.72/58.86 inference(scs_inference,[],[18,26])). % 58.72/58.86 cnf(64,plain, % 58.72/58.86 (~P3(x641)+~E(x641,x642)+~P5(x642,a11,a13)), % 58.72/58.86 inference(scs_inference,[],[18,27])). % 58.72/58.86 cnf(65,plain, % 58.72/58.86 (~P3(x651)+E(f5(x651),x651)+~P5(x651,a10,a13)), % 58.72/58.86 inference(scs_inference,[],[18,28])). % 58.72/58.86 cnf(66,plain, % 58.72/58.86 (~P2(x661)+E(f8(x661),x661)+~P5(x661,a14,a13)), % 58.72/58.86 inference(scs_inference,[],[18,29])). % 58.72/58.86 cnf(67,plain, % 58.72/58.86 (~P3(x671)+~P5(x671,a10,a13)+P5(f5(x671),a12,a13)), % 58.72/58.86 inference(scs_inference,[],[18,30])). % 58.72/58.86 cnf(70,plain, % 58.72/58.86 (~P4(x701)+~E(x701,x702)+~P5(x702,a3,a13)+~P5(x701,a12,a13)), % 58.72/58.86 inference(scs_inference,[],[18,33])). % 58.72/58.86 cnf(71,plain, % 58.72/58.86 (~P4(x711)+E(f6(x711),x711)+~P5(x711,a12,a13)+~P5(x711,a10,a13)), % 58.72/58.86 inference(scs_inference,[],[18,34])). % 58.72/58.86 cnf(72,plain, % 58.72/58.86 (~P4(x721)+~P5(x721,a12,a13)+~P5(x721,a10,a13)+P5(f6(x721),a11,a13)), % 58.72/58.86 inference(scs_inference,[],[18,35])). % 58.72/58.86 cnf(73,plain, % 58.72/58.86 (E(a1,f4(a1))), % 58.72/58.86 inference(scs_inference,[],[43,2])). % 58.72/58.86 cnf(74,plain, % 58.72/58.86 (P3(f4(a1))), % 58.72/58.86 inference(scs_inference,[],[43,49,2,11])). % 58.72/58.86 cnf(75,plain, % 58.72/58.86 (P2(f4(a1))), % 58.72/58.86 inference(scs_inference,[],[20,43,49,2,11,12])). % 58.72/58.86 cnf(82,plain, % 58.72/58.86 (E(a2,f7(a2))), % 58.72/58.86 inference(scs_inference,[],[45,2])). % 58.72/58.86 cnf(85,plain, % 58.72/58.86 (E(a2,f4(a1))), % 58.72/58.86 inference(scs_inference,[],[19,42,45,73,50,2,11,12,3])). % 58.72/58.86 cnf(88,plain, % 58.72/58.86 (E(a1,f9(a1))), % 58.72/58.86 inference(scs_inference,[],[47,2])). % 58.72/58.86 cnf(89,plain, % 58.72/58.86 (P3(f9(a1))), % 58.72/58.86 inference(scs_inference,[],[47,49,2,11])). % 58.72/58.86 cnf(90,plain, % 58.72/58.86 (P2(f9(a1))), % 58.72/58.86 inference(scs_inference,[],[20,47,49,2,11,12])). % 58.72/58.86 cnf(91,plain, % 58.72/58.86 (E(f9(a1),a2)), % 58.72/58.86 inference(scs_inference,[],[17,20,47,49,2,11,12,3])). % 58.72/58.86 cnf(95,plain, % 58.72/58.86 (E(a2,f9(a1))), % 58.72/58.86 inference(scs_inference,[],[91,2])). % 58.72/58.86 cnf(96,plain, % 58.72/58.86 (E(a1,f7(a2))), % 58.72/58.86 inference(scs_inference,[],[17,82,91,2,3])). % 58.72/58.86 cnf(99,plain, % 58.72/58.86 (E(f7(a2),a1)), % 58.72/58.86 inference(scs_inference,[],[96,2])). % 58.72/58.86 cnf(115,plain, % 58.72/58.86 (E(f4(a1),f7(a2))), % 58.72/58.86 inference(scs_inference,[],[96,43,3])). % 58.72/58.86 cnf(122,plain, % 58.72/58.86 (~P4(f9(a1))+P4(a2)), % 58.72/58.86 inference(scs_inference,[],[91,16])). % 58.72/58.86 cnf(177,plain, % 58.72/58.86 (E(f7(a2),f9(a1))), % 58.72/58.86 inference(scs_inference,[],[45,95,3])). % 58.72/58.86 cnf(183,plain, % 58.72/58.86 (P4(a2)), % 58.72/58.86 inference(scs_inference,[],[20,122,62])). % 58.72/58.86 cnf(216,plain, % 58.72/58.86 (E(f4(f4(a1)),f4(a1))), % 58.72/58.86 inference(scs_inference,[],[20,58,4])). % 58.72/58.86 cnf(220,plain, % 58.72/58.86 (E(a2,f4(f4(a1)))), % 58.72/58.86 inference(scs_inference,[],[85,216,74,75,2,11,12,3])). % 58.72/58.86 cnf(225,plain, % 58.72/58.86 (E(a1,f4(f4(a1)))), % 58.72/58.86 inference(scs_inference,[],[17,220,2,3])). % 58.72/58.86 cnf(230,plain, % 58.72/58.86 (E(f9(f9(a1)),f9(a1))), % 58.72/58.86 inference(scs_inference,[],[20,60,6])). % 58.72/58.86 cnf(234,plain, % 58.72/58.86 (E(a1,f9(f9(a1)))), % 58.72/58.86 inference(scs_inference,[],[89,88,230,90,2,11,12,3])). % 58.72/58.86 cnf(241,plain, % 58.72/58.86 (E(f4(a1),f9(f9(a1)))), % 58.72/58.86 inference(scs_inference,[],[43,225,234,2,3])). % 58.72/58.86 cnf(253,plain, % 58.72/58.86 (E(f9(f9(a1)),f4(a1))), % 58.72/58.86 inference(scs_inference,[],[241,2])). % 58.72/58.86 cnf(281,plain, % 58.72/58.86 (E(f7(a2),f9(f9(a1)))), % 58.72/58.86 inference(scs_inference,[],[99,234,3])). % 58.72/58.86 cnf(291,plain, % 58.72/58.86 (P5(f4(a2),a10,a13)), % 58.72/58.86 inference(scs_inference,[],[17,20,63,12])). % 58.72/58.86 cnf(310,plain, % 58.72/58.86 (P5(x3101,a10,a13)+~E(f4(a2),x3101)), % 58.72/58.86 inference(scs_inference,[],[291,13])). % 58.72/58.86 cnf(311,plain, % 58.72/58.86 (~E(f4(a2),a2)+P5(f5(a2),a12,a13)), % 58.72/58.86 inference(scs_inference,[],[19,291,13,67])). % 58.72/58.86 cnf(338,plain, % 58.72/58.86 (P5(f5(a2),a12,a13)), % 58.72/58.86 inference(scs_inference,[],[50,311,58])). % 58.72/58.86 cnf(339,plain, % 58.72/58.86 (P5(x3391,a12,a13)+~E(f5(a2),x3391)), % 58.72/58.86 inference(scs_inference,[],[338,13])). % 58.72/58.86 cnf(346,plain, % 58.72/58.86 (~P3(f5(a2))+~E(a12,a11)), % 58.72/58.86 inference(scs_inference,[],[338,14,39])). % 58.72/58.86 cnf(356,plain, % 58.72/58.86 (~E(a11,a12)+~P3(f5(a2))), % 58.72/58.86 inference(scs_inference,[],[346,2])). % 58.72/58.86 cnf(372,plain, % 58.72/58.86 (~E(a2,f5(a2))+~E(a11,a12)), % 58.72/58.86 inference(scs_inference,[],[19,356,11])). % 58.72/58.86 cnf(404,plain, % 58.72/58.86 (~E(f5(a2),a2)+~E(a11,a12)), % 58.72/58.86 inference(scs_inference,[],[372,2])). % 58.72/58.86 cnf(3760,plain, % 58.72/58.86 (~P5(f4(a1),a11,a13)), % 58.72/58.86 inference(scs_inference,[],[51,43,13])). % 58.72/58.86 cnf(3765,plain, % 58.72/58.86 (~P5(f9(f9(a1)),a11,a13)), % 58.72/58.86 inference(scs_inference,[],[253,3760,13])). % 58.72/58.86 cnf(3772,plain, % 58.72/58.86 (~P5(f7(a2),a11,a13)), % 58.72/58.86 inference(scs_inference,[],[281,3765,13])). % 58.72/58.86 cnf(5082,plain, % 58.72/58.86 (E(f7(a1),f7(a2))), % 58.72/58.86 inference(scs_inference,[],[17,49,50,58,59,60,5])). % 58.72/58.86 cnf(5084,plain, % 58.72/58.86 (E(f6(a1),f6(a2))), % 58.72/58.86 inference(scs_inference,[],[17,49,50,58,59,60,5,6,7])). % 58.72/58.86 cnf(5089,plain, % 58.72/58.86 (P5(a2,a10,a13)), % 58.72/58.86 inference(scs_inference,[],[17,49,50,20,58,59,60,5,6,7,8,9,63,310])). % 58.72/58.86 cnf(5092,plain, % 58.72/58.86 (E(a2,f4(a2))), % 58.72/58.86 inference(scs_inference,[],[17,49,50,20,58,59,60,5,6,7,8,9,63,310,62,2])). % 58.72/58.86 cnf(5095,plain, % 58.72/58.86 (E(f4(a1),f4(a2))), % 58.72/58.86 inference(scs_inference,[],[17,49,50,20,58,59,60,5,6,7,8,9,63,310,62,2,61,4])). % 58.72/58.86 cnf(5096,plain, % 58.72/58.86 (P5(f7(a2),a10,a13)), % 58.72/58.86 inference(scs_inference,[],[17,115,49,50,20,58,59,60,5,6,7,8,9,63,310,62,2,61,4,13])). % 58.72/58.86 cnf(5100,plain, % 58.72/58.86 (E(f7(a2),f9(a2))), % 58.72/58.86 inference(scs_inference,[],[17,90,115,177,49,50,20,19,58,59,60,5,6,7,8,9,63,310,62,2,61,4,13,65,12,3])). % 58.72/58.86 cnf(5105,plain, % 58.72/58.86 (P5(a2,a12,a13)), % 58.72/58.86 inference(scs_inference,[],[17,90,115,89,177,49,50,20,19,58,59,60,5,6,7,8,9,63,310,62,2,61,4,13,65,12,3,11,404,39,339])). % 58.72/58.86 cnf(5108,plain, % 58.72/58.86 (~P5(a2,a3,a13)), % 58.72/58.86 inference(scs_inference,[],[17,90,115,89,177,183,49,50,20,19,58,59,60,5,6,7,8,9,63,310,62,2,61,4,13,65,12,3,11,404,39,339,66,41])). % 58.72/58.86 cnf(5147,plain, % 58.72/58.86 (P5(f6(a2),a11,a13)), % 58.72/58.86 inference(scs_inference,[],[17,5089,5105,5108,5082,5095,5092,74,75,3772,183,42,5,9,8,7,6,2,339,13,12,3,11,14,70,72])). % 58.72/58.86 cnf(5149,plain, % 58.72/58.86 (E(f6(a2),a2)), % 58.72/58.86 inference(scs_inference,[],[17,5089,5105,5108,5082,5095,5092,74,75,3772,183,42,5,9,8,7,6,2,339,13,12,3,11,14,70,72,71])). % 58.72/58.86 cnf(5183,plain, % 58.72/58.86 (E(a2,f6(a2))), % 58.72/58.86 inference(scs_inference,[],[5149,2])). % 58.72/58.86 cnf(5185,plain, % 58.72/58.86 (E(f6(a1),a2)), % 58.72/58.86 inference(scs_inference,[],[5084,5149,5100,5096,2,13,3])). % 58.72/58.86 cnf(5199,plain, % 58.72/58.86 ($false), % 58.72/58.86 inference(scs_inference,[],[5185,5183,5147,19,2,64]), % 58.72/58.86 ['proof']). % 58.72/58.86 % SZS output end Proof % 58.72/58.86 % Total time :58.140000s %------------------------------------------------------------------------------