%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : BOO021-1 : TPTP v8.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n008.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 04:35:50 EDT 2024 % Result : Unsatisfiable 182.51s 182.68s % Output : CNFRefutation 182.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : BOO021-1 : TPTP v8.2.0. Released v2.2.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n008.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Jun 18 19:59:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.48/0.57 start to proof:theBenchmark % 182.51/182.64 %------------------------------------------- % 182.51/182.64 % File :CSE---1.7 % 182.51/182.64 % Problem :theBenchmark % 182.51/182.64 % Transform :cnf % 182.51/182.64 % Format :tptp:raw % 182.51/182.64 % Command :java -jar mcs_scs.jar %d %s % 182.51/182.64 % 182.51/182.64 % Result :Theorem 181.930000s % 182.51/182.64 % Output :CNFRefutation 181.930000s % 182.51/182.64 %------------------------------------------- % 182.51/182.67 %-------------------------------------------------------------------------- % 182.51/182.67 % File : BOO021-1 : TPTP v8.2.0. Released v2.2.0. % 182.51/182.68 % Domain : Boolean Algebra % 182.51/182.68 % Problem : A Basis for Boolean Algebra % 182.51/182.68 % Version : [MP96] (equality) axioms. % 182.51/182.68 % English : This theorem starts with a (self-dual independent) basis_ % 182.51/182.68 % for Boolean algebra and derives commutativity of product. % 182.51/182.68 % 182.51/182.68 % Refs : [McC98] McCune (1998), Email to G. Sutcliffe % 182.51/182.68 % : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq % 182.51/182.68 % Source : [McC98] % 182.51/182.68 % Names : DUAL-BA-1 [MP96] % 182.51/182.68 % 182.51/182.68 % Status : Unsatisfiable % 182.51/182.68 % Rating : 0.00 v7.5.0, 0.04 v7.3.0, 0.05 v7.1.0, 0.06 v7.0.0, 0.05 v6.4.0, 0.11 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.06 v6.0.0, 0.10 v5.5.0, 0.16 v5.4.0, 0.13 v5.3.0, 0.08 v5.2.0, 0.07 v5.1.0, 0.20 v5.0.0, 0.14 v4.1.0, 0.09 v4.0.1, 0.14 v4.0.0, 0.15 v3.7.0, 0.00 v3.3.0, 0.07 v3.1.0, 0.11 v2.7.0, 0.00 v2.2.1 % 182.51/182.68 % Syntax : Number of clauses : 7 ( 7 unt; 0 nHn; 1 RR) % 182.51/182.68 % Number of literals : 7 ( 7 equ; 1 neg) % 182.51/182.68 % Maximal clause size : 1 ( 1 avg) % 182.51/182.68 % Maximal term depth : 3 ( 2 avg) % 182.51/182.68 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 182.51/182.68 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty) % 182.51/182.68 % Number of variables : 12 ( 2 sgn) % 182.51/182.68 % SPC : CNF_UNS_RFO_PEQ_UEQ % 182.51/182.68 % 182.51/182.68 % Comments : The other part of this problem is to prove associativity. % 182.51/182.68 %-------------------------------------------------------------------------- % 182.51/182.68 %----Boolean Algebra: % 182.51/182.68 cnf(multiply_add,axiom, % 182.51/182.68 multiply(add(X,Y),Y) = Y ). % 182.51/182.68 % 182.51/182.68 cnf(multiply_add_property,axiom, % 182.51/182.68 multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)) ). % 182.51/182.68 % 182.51/182.68 cnf(additive_inverse,axiom, % 182.51/182.68 add(X,inverse(X)) = n1 ). % 182.51/182.68 % 182.51/182.68 cnf(add_multiply,axiom, % 182.51/182.68 add(multiply(X,Y),Y) = Y ). % 182.51/182.68 % 182.51/182.68 cnf(add_multiply_property,axiom, % 182.51/182.68 add(X,multiply(Y,Z)) = multiply(add(Y,X),add(Z,X)) ). % 182.51/182.68 % 182.51/182.68 cnf(multiplicative_inverse,axiom, % 182.51/182.68 multiply(X,inverse(X)) = n0 ). % 182.51/182.68 % 182.51/182.68 %----Denial of conclusion: % 182.51/182.68 cnf(prove_commutativity_of_multiply,negated_conjecture, % 182.51/182.68 multiply(b,a) != multiply(a,b) ). % 182.51/182.68 % 182.51/182.68 %-------------------------------------------------------------------------- % 182.51/182.68 %------------------------------------------- % 182.51/182.68 % Proof found % 182.51/182.68 % SZS status Theorem for theBenchmark % 182.51/182.68 % SZS output start Proof % 182.60/182.70 %ClaNum:15(EqnAxiom:8) % 182.60/182.70 %VarNum:26(SingletonVarNum:12) % 182.60/182.70 %MaxLitNum:1 % 182.60/182.70 %MaxfuncDepth:2 % 182.60/182.70 %SharedTerms:7 % 182.60/182.70 %goalClause: 15 % 182.60/182.70 %singleGoalClaCount:1 % 182.60/182.70 [15]~E(f6(a4,a3),f6(a3,a4)) % 182.60/182.70 [9]E(f2(x91,f1(x91)),a5) % 182.60/182.70 [10]E(f6(x101,f1(x101)),a7) % 182.60/182.70 [11]E(f2(f6(x111,x112),x112),x112) % 182.60/182.70 [12]E(f6(f2(x121,x122),x122),x122) % 182.60/182.70 [13]E(f6(f2(x131,x132),f2(x133,x132)),f2(x132,f6(x131,x133))) % 182.60/182.70 [14]E(f2(f6(x141,x142),f6(x143,x142)),f6(x142,f2(x141,x143))) % 182.60/182.70 %EqnAxiom % 182.60/182.70 [1]E(x11,x11) % 182.60/182.70 [2]E(x22,x21)+~E(x21,x22) % 182.60/182.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 182.60/182.70 [4]~E(x41,x42)+E(f1(x41),f1(x42)) % 182.60/182.70 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53)) % 182.60/182.70 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62)) % 182.60/182.70 [7]~E(x71,x72)+E(f6(x71,x73),f6(x72,x73)) % 182.60/182.70 [8]~E(x81,x82)+E(f6(x83,x81),f6(x83,x82)) % 182.60/182.70 % 182.60/182.70 %------------------------------------------- % 182.64/182.74 cnf(17,plain, % 182.64/182.74 (~E(f6(a4,a3),f2(f6(x171,f6(a3,a4)),f6(a3,a4)))), % 182.64/182.74 inference(scs_inference,[],[15,13,11,2,3])). % 182.64/182.74 cnf(20,plain, % 182.64/182.74 (~E(f6(a4,a3),f6(f2(x201,f6(a3,a4)),f6(a3,a4)))), % 182.64/182.74 inference(scs_inference,[],[15,14,12,2,3])). % 182.64/182.74 cnf(22,plain, % 182.64/182.74 (E(a5,f2(x221,f1(x221)))), % 182.64/182.74 inference(scs_inference,[],[9,2])). % 182.64/182.74 cnf(23,plain, % 182.64/182.74 (E(a7,f6(x231,f1(x231)))), % 182.64/182.74 inference(scs_inference,[],[10,2])). % 182.64/182.74 cnf(24,plain, % 182.64/182.74 (E(f2(f6(x241,a5),a5),f2(x242,f1(x242)))), % 182.64/182.74 inference(scs_inference,[],[22,10,11,2,3])). % 182.64/182.74 cnf(26,plain, % 182.64/182.74 (E(f2(x261,f1(x261)),f2(f6(x262,a5),a5))), % 182.64/182.74 inference(scs_inference,[],[24,2])). % 182.64/182.74 cnf(32,plain, % 182.64/182.74 (E(x321,f2(f6(x322,x321),x321))), % 182.64/182.74 inference(scs_inference,[],[11,2])). % 182.64/182.74 cnf(35,plain, % 182.64/182.74 (E(x351,f6(f2(x352,x351),x351))), % 182.64/182.74 inference(scs_inference,[],[12,2])). % 182.64/182.74 cnf(36,plain, % 182.64/182.74 (E(f2(x361,f1(x361)),f2(x362,f1(x362)))), % 182.64/182.74 inference(scs_inference,[],[22,9,12,2,3])). % 182.64/182.74 cnf(41,plain, % 182.64/182.74 (E(f6(f2(x411,a5),a5),f2(x412,f1(x412)))), % 182.64/182.74 inference(scs_inference,[],[12,22,3])). % 182.64/182.74 cnf(43,plain, % 182.64/182.74 (E(f2(x431,f1(x431)),f6(f2(x432,a5),a5))), % 182.64/182.74 inference(scs_inference,[],[12,22,3,2])). % 182.64/182.74 cnf(44,plain, % 182.64/182.74 (E(f2(f6(x441,a5),a5),f6(f2(x442,a5),a5))), % 182.64/182.74 inference(scs_inference,[],[24,43,3])). % 182.64/182.74 cnf(47,plain, % 182.64/182.74 (E(f2(f6(x471,a5),a5),f2(f6(x472,a5),a5))), % 182.64/182.74 inference(scs_inference,[],[24,26,3])). % 182.64/182.74 cnf(59,plain, % 182.64/182.74 (E(f2(f2(x591,f1(x591)),x592),f2(a5,x592))), % 182.64/182.74 inference(scs_inference,[],[9,4,5])). % 182.64/182.74 cnf(60,plain, % 182.64/182.74 (E(f2(x601,f2(x602,f1(x602))),f2(x601,a5))), % 182.64/182.74 inference(scs_inference,[],[9,4,5,6])). % 182.64/182.74 cnf(63,plain, % 182.64/182.74 (~E(f2(f6(x631,f6(a3,a4)),f6(a3,a4)),f6(a4,a3))), % 182.64/182.74 inference(scs_inference,[],[9,17,4,5,6,7,8,2])). % 182.64/182.74 cnf(69,plain, % 182.64/182.74 (E(f2(x691,x692),f2(f6(f2(x693,x691),x691),x692))), % 182.64/182.74 inference(scs_inference,[],[35,8,7,4,5])). % 182.64/182.74 cnf(71,plain, % 182.64/182.74 (~E(f6(f2(x711,f6(a3,a4)),f6(a3,a4)),f6(a4,a3))), % 182.64/182.74 inference(scs_inference,[],[35,20,8,7,4,5,6,2])). % 182.64/182.74 cnf(72,plain, % 182.64/182.74 (E(f2(f2(x721,f1(x721)),f1(a5)),a5)), % 182.64/182.74 inference(scs_inference,[],[9,35,20,59,8,7,4,5,6,2,3])). % 182.64/182.74 cnf(77,plain, % 182.64/182.74 (E(f2(x771,x772),f2(f2(f6(x773,x771),x771),x772))), % 182.64/182.74 inference(scs_inference,[],[32,8,6,5])). % 182.64/182.74 cnf(85,plain, % 182.64/182.74 (E(f6(f6(x851,f1(x851)),x852),f6(a7,x852))), % 182.64/182.74 inference(scs_inference,[],[10,8,4,7])). % 182.64/182.74 cnf(87,plain, % 182.64/182.74 (E(f2(f6(x871,f1(x871)),x872),f2(a7,x872))), % 182.64/182.74 inference(scs_inference,[],[10,8,4,7,6,5])). % 182.64/182.74 cnf(90,plain, % 182.64/182.74 (E(f2(a7,x901),f2(f6(x902,f1(x902)),x901))), % 182.64/182.74 inference(scs_inference,[],[23,5])). % 182.64/182.74 cnf(98,plain, % 182.64/182.74 (E(f6(f2(f6(x981,x982),x982),x983),f6(x982,x983))), % 182.64/182.74 inference(scs_inference,[],[11,7])). % 182.64/182.74 cnf(99,plain, % 182.64/182.74 (E(f1(f2(f6(x991,x992),x992)),f1(x992))), % 182.64/182.74 inference(scs_inference,[],[11,7,4])). % 182.64/182.74 cnf(109,plain, % 182.64/182.74 (E(f1(f6(f2(x1091,x1092),x1092)),f1(x1092))), % 182.64/182.74 inference(scs_inference,[],[12,8,7,6,4])). % 182.64/182.74 cnf(110,plain, % 182.64/182.74 (E(f2(f6(f2(x1101,x1102),x1102),x1103),f2(x1102,x1103))), % 182.64/182.74 inference(scs_inference,[],[12,8,7,6,4,5])). % 182.64/182.74 cnf(114,plain, % 182.64/182.74 (~E(f6(a4,a3),f6(f6(a3,a4),f6(a3,a4)))), % 182.64/182.74 inference(scs_inference,[],[71,98,12,8,7,6,4,5,3,2])). % 182.64/182.74 cnf(115,plain, % 182.64/182.74 (E(f2(a5,x1151),f2(f2(x1152,f1(x1152)),x1151))), % 182.64/182.74 inference(scs_inference,[],[22,5])). % 182.64/182.74 cnf(119,plain, % 182.64/182.74 (E(f2(x1191,a5),f2(x1191,f2(x1192,f1(x1192))))), % 182.64/182.74 inference(scs_inference,[],[22,5,8,4,7,6])). % 182.64/182.74 cnf(130,plain, % 182.64/182.74 (~E(f2(f6(a3,a4),f6(a3,a4)),f6(a4,a3))), % 182.64/182.74 inference(scs_inference,[],[63,110,3])). % 182.64/182.74 cnf(133,plain, % 182.64/182.74 (~E(f6(a4,a3),f2(f6(a3,a4),f6(a3,a4)))), % 182.64/182.74 inference(scs_inference,[],[63,110,3,2])). % 182.64/182.74 cnf(137,plain, % 182.64/182.74 (E(f6(f6(x1371,f1(x1371)),f1(a7)),a7)), % 182.64/182.74 inference(scs_inference,[],[10,85,3])). % 182.64/182.74 cnf(162,plain, % 182.64/182.74 (~E(f6(a4,a3),f6(a4,f2(a3,a3)))), % 182.64/182.74 inference(scs_inference,[],[14,130,3,2])). % 182.64/182.74 cnf(166,plain, % 182.64/182.74 (E(f2(f2(x1661,f1(x1661)),f1(a5)),f6(f2(x1662,a5),a5))), % 182.64/182.74 inference(scs_inference,[],[72,35,3])). % 182.64/182.74 cnf(183,plain, % 182.64/182.74 (~E(f2(f6(x1831,f6(a4,a3)),f6(a4,a3)),f6(f6(a3,a4),f6(a3,a4)))), % 182.64/182.74 inference(scs_inference,[],[32,114,3])). % 182.64/182.74 cnf(186,plain, % 182.64/182.74 (~E(f2(f6(a4,a3),f6(a4,a3)),f6(f6(a3,a4),f6(a3,a4)))), % 182.64/182.74 inference(scs_inference,[],[183,110,3])). % 182.64/182.74 cnf(190,plain, % 182.64/182.74 (~E(f2(f6(x1901,f6(a4,a3)),f6(a4,a3)),f2(f6(a3,a4),f6(a3,a4)))), % 182.64/182.74 inference(scs_inference,[],[32,133,186,2,3])). % 182.64/182.74 cnf(193,plain, % 182.64/182.74 (~E(f2(f6(a4,a3),f6(a4,a3)),f2(f6(a3,a4),f6(a3,a4)))), % 182.64/182.74 inference(scs_inference,[],[190,110,2,3])). % 182.64/182.74 cnf(196,plain, % 182.64/182.74 (~E(f2(f6(a3,a4),f6(a3,a4)),f2(f6(a4,a3),f6(a4,a3)))), % 182.64/182.74 inference(scs_inference,[],[193,2])). % 182.64/182.74 cnf(197,plain, % 182.64/182.74 (~E(f2(f6(x1971,f6(a4,a3)),f6(a4,a3)),f6(a4,f2(a3,a3)))), % 182.64/182.74 inference(scs_inference,[],[32,162,193,2,3])). % 182.64/182.74 cnf(200,plain, % 182.64/182.74 (~E(f6(a4,f2(a3,a3)),f2(f6(a4,a3),f6(a4,a3)))), % 182.64/182.74 inference(scs_inference,[],[196,197,14,2,3])). % 182.64/182.74 cnf(203,plain, % 182.64/182.74 (~E(f2(f6(x2031,f6(a4,a3)),f6(a4,a3)),f6(a3,a4))), % 182.64/182.74 inference(scs_inference,[],[32,200,15,2,3])). % 182.64/182.74 cnf(215,plain, % 182.64/182.74 (~E(f2(f6(a4,a3),f6(a4,a3)),f6(a3,a4))), % 182.64/182.74 inference(scs_inference,[],[203,110,3])). % 182.64/182.74 cnf(255,plain, % 182.64/182.74 (E(f2(f6(x2551,f1(x2551)),f1(a7)),f2(x2552,f1(x2552)))), % 182.64/182.74 inference(scs_inference,[],[36,87,3])). % 182.64/182.74 cnf(291,plain, % 182.64/182.74 (E(f2(f6(x2911,a5),a5),f2(f6(f2(x2912,x2913),x2913),f1(x2913)))), % 182.64/182.74 inference(scs_inference,[],[69,24,3])). % 182.64/182.74 cnf(297,plain, % 182.64/182.74 (E(f6(f2(x2971,a5),a5),f2(f2(f6(x2972,x2973),x2973),f1(x2973)))), % 182.64/182.74 inference(scs_inference,[],[77,41,3])). % 182.64/182.74 cnf(332,plain, % 182.64/182.74 (E(f2(f6(x3321,a5),a5),f6(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[98,44,3])). % 182.64/182.74 cnf(348,plain, % 182.64/182.74 (E(f2(f2(x3481,f1(x3481)),f1(a5)),f6(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[98,166,3])). % 182.64/182.74 cnf(357,plain, % 182.64/182.74 (E(f2(a5,f1(a5)),f6(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[348,115,3])). % 182.64/182.74 cnf(367,plain, % 182.64/182.74 (~E(f6(a3,a4),f6(a3,f2(a4,a4)))), % 182.64/182.74 inference(scs_inference,[],[215,14,3,2])). % 182.64/182.74 cnf(381,plain, % 182.64/182.74 (E(f2(f6(x3811,a5),a5),f2(f2(f6(x3812,x3813),x3813),f1(x3813)))), % 182.64/182.74 inference(scs_inference,[],[297,44,3])). % 182.64/182.74 cnf(385,plain, % 182.64/182.74 (E(f2(f6(x3851,a5),f2(x3852,f1(x3852))),f6(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[332,60,3])). % 182.64/182.74 cnf(392,plain, % 182.64/182.74 (E(f2(f6(x3921,f1(x3921)),f1(a7)),f6(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[357,255,3])). % 182.64/182.74 cnf(394,plain, % 182.64/182.74 (E(f2(a7,f1(a7)),f6(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[392,90,3])). % 182.64/182.74 cnf(396,plain, % 182.64/182.74 (E(a5,f6(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[394,22,3])). % 182.64/182.74 cnf(398,plain, % 182.64/182.74 (E(f2(x3981,a5),f2(x3981,f6(a5,a5)))), % 182.64/182.74 inference(scs_inference,[],[394,22,3,6])). % 182.64/182.74 cnf(399,plain, % 182.64/182.74 (E(f2(a5,x3991),f2(f6(a5,a5),x3991))), % 182.64/182.74 inference(scs_inference,[],[394,22,3,6,5])). % 182.64/182.74 cnf(400,plain, % 182.64/182.74 (E(f6(a5,x4001),f6(f6(a5,a5),x4001))), % 182.64/182.74 inference(scs_inference,[],[394,22,3,6,5,7])). % 182.64/182.74 cnf(402,plain, % 182.64/182.74 (E(f1(a5),f1(f6(a5,a5)))), % 182.64/182.74 inference(scs_inference,[],[394,22,3,6,5,7,8,4])). % 182.64/182.74 cnf(405,plain, % 182.64/182.74 (E(f2(a5,x4051),f2(f6(f6(a5,a5),a5),x4051))), % 182.64/182.74 inference(scs_inference,[],[396,400,3,5])). % 182.64/182.74 cnf(410,plain, % 182.64/182.74 (E(f2(a5,a5),f2(f6(a5,a5),f6(a5,a5)))), % 182.64/182.74 inference(scs_inference,[],[398,399,3])). % 182.64/182.74 cnf(422,plain, % 182.64/182.74 (E(f2(a5,a5),f2(f6(x4221,a5),a5))), % 182.64/182.74 inference(scs_inference,[],[47,405,3])). % 182.64/182.74 cnf(425,plain, % 182.64/182.74 (E(f2(a5,f2(x4251,f1(x4251))),f6(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[399,385,3])). % 182.64/182.74 cnf(428,plain, % 182.64/182.74 (E(f2(a5,a5),f2(f6(f2(x4281,x4282),x4282),f1(x4282)))), % 182.64/182.74 inference(scs_inference,[],[422,291,3])). % 182.64/182.74 cnf(430,plain, % 182.64/182.74 (E(f2(a5,a5),f6(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[425,119,3])). % 182.64/182.74 cnf(432,plain, % 182.64/182.74 (E(f2(f2(a5,a5),x4321),f2(f6(a5,a5),x4321))), % 182.64/182.74 inference(scs_inference,[],[425,119,3,5])). % 182.64/182.74 cnf(445,plain, % 182.64/182.74 (E(f2(a5,a5),f2(f2(f6(x4451,x4452),x4452),f1(x4452)))), % 182.64/182.74 inference(scs_inference,[],[422,381,3])). % 182.64/182.74 cnf(574,plain, % 182.64/182.74 (E(f1(f6(a5,a5)),f1(a5))), % 182.64/182.74 inference(scs_inference,[],[402,2])). % 182.64/182.74 cnf(578,plain, % 182.64/182.74 (~E(a3,f2(a3,a3))), % 182.64/182.74 inference(scs_inference,[],[162,8])). % 182.64/182.74 cnf(586,plain, % 182.64/182.74 (E(f2(f6(f2(x5861,x5862),x5862),f1(x5862)),f2(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[428,367,8,2])). % 182.64/182.74 cnf(592,plain, % 182.64/182.74 (E(f2(f2(f6(x5921,x5922),x5922),f1(x5922)),f2(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[445,2])). % 182.64/182.74 cnf(598,plain, % 182.64/182.74 (E(f6(a5,a5),f2(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[430,2])). % 182.64/182.74 cnf(612,plain, % 182.64/182.74 (E(f6(a5,a5),a5)), % 182.64/182.74 inference(scs_inference,[],[396,2])). % 182.64/182.74 cnf(642,plain, % 182.64/182.74 (E(f2(f6(x6421,f2(f2(a5,a5),x6422)),f2(f2(a5,a5),x6422)),f2(f6(a5,a5),x6422))), % 182.64/182.74 inference(scs_inference,[],[11,432,137,2,3])). % 182.64/182.74 cnf(687,plain, % 182.64/182.74 (E(f2(f6(a5,a5),f6(a5,a5)),f2(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[410,2])). % 182.64/182.74 cnf(904,plain, % 182.64/182.74 (E(f2(f6(x9041,f1(f2(f6(x9042,x9043),x9043))),f1(f2(f6(x9042,x9043),x9043))),f1(x9043))), % 182.64/182.74 inference(scs_inference,[],[11,99,642,2,3])). % 182.64/182.74 cnf(907,plain, % 182.64/182.74 (E(f2(f6(x9071,f1(f6(f2(x9072,x9073),x9073))),f1(f6(f2(x9072,x9073),x9073))),f1(x9073))), % 182.64/182.74 inference(scs_inference,[],[11,904,109,2,3])). % 182.64/182.74 cnf(910,plain, % 182.64/182.74 (E(f2(f6(x9101,f2(f6(f2(x9102,x9103),x9103),f1(x9103))),f2(f6(f2(x9102,x9103),x9103),f1(x9103))),f2(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[11,907,586,2,3])). % 182.64/182.74 cnf(913,plain, % 182.64/182.74 (E(f2(f6(x9131,f2(f2(f6(x9132,x9133),x9133),f1(x9133))),f2(f2(f6(x9132,x9133),x9133),f1(x9133))),f2(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[11,910,592,2,3])). % 182.64/182.74 cnf(916,plain, % 182.64/182.74 (E(f2(f6(x9161,f6(a5,a5)),f6(a5,a5)),f2(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[11,913,598,2,3])). % 182.64/182.74 cnf(919,plain, % 182.64/182.74 (E(f2(f6(x9191,f1(f6(a5,a5))),f1(f6(a5,a5))),f1(a5))), % 182.64/182.74 inference(scs_inference,[],[11,574,916,2,3])). % 182.64/182.74 cnf(922,plain, % 182.64/182.74 (E(f2(f6(x9221,f2(f6(x9222,f6(a5,a5)),f6(a5,a5))),f2(f6(x9222,f6(a5,a5)),f6(a5,a5))),f2(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[11,916,919,2,3])). % 182.64/182.74 cnf(925,plain, % 182.64/182.74 (E(f2(f6(x9251,f2(f6(a5,a5),f6(a5,a5))),f2(f6(a5,a5),f6(a5,a5))),f2(a5,a5))), % 182.64/182.74 inference(scs_inference,[],[11,687,922,2,3])). % 182.64/182.74 cnf(928,plain, % 182.64/182.74 (E(f2(f6(x9281,f6(a5,a5)),f6(a5,a5)),a5)), % 182.64/182.74 inference(scs_inference,[],[11,612,925,2,3])). % 182.64/182.74 cnf(1329,plain, % 182.64/182.74 (E(a5,f2(f6(x13291,f6(a5,a5)),f6(a5,a5)))), % 182.64/182.74 inference(scs_inference,[],[928,2])). % 182.64/182.74 cnf(1694,plain, % 182.64/182.74 ($false), % 182.64/182.74 inference(scs_inference,[],[578,1329,110,32,5,6,4,7,8,3]), % 182.64/182.74 ['proof']). % 182.64/182.74 % SZS output end Proof % 182.64/182.74 % Total time :181.930000s %------------------------------------------------------------------------------