%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL002-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n026.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:44:42 EDT 2024 % Result : Unsatisfiable 180.94s 181.14s % Output : CNFRefutation 180.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : COL002-1 : TPTP v8.2.0. Released v1.0.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n026.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 : Tue Jun 18 16:17:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.52/0.56 start to proof:theBenchmark % 180.89/181.12 %------------------------------------------- % 180.89/181.12 % File :CSE---1.7 % 180.89/181.12 % Problem :theBenchmark % 180.89/181.12 % Transform :cnf % 180.89/181.12 % Format :tptp:raw % 180.89/181.12 % Command :java -jar mcs_scs.jar %d %s % 180.89/181.12 % 180.89/181.12 % Result :Theorem 180.270000s % 180.89/181.12 % Output :CNFRefutation 180.270000s % 180.89/181.12 %------------------------------------------- % 180.94/181.14 %-------------------------------------------------------------------------- % 180.94/181.14 % File : COL002-1 : TPTP v8.2.0. Released v1.0.0. % 180.94/181.14 % Domain : Combinatory Logic % 180.94/181.14 % Problem : Weak fixed point for S, B, C, and I % 180.94/181.14 % Version : [WM88] (equality) axioms. % 180.94/181.14 % English : The weak fixed point property holds for the set P consisting % 180.94/181.14 % of the combinators S, B, C, and I, where ((Sx)y)z = (xz)(yz), % 180.94/181.14 % ((Bx)y)z = x(yz), ((Cx)y)z = (xz)y, and Ix = x. % 180.94/181.14 % 180.94/181.14 % Refs : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq % 180.94/181.14 % Source : [WM88] % 180.94/181.14 % Names : C1.1 [WM88] % 180.94/181.14 % 180.94/181.14 % Status : Unsatisfiable % 180.94/181.14 % Rating : 0.18 v8.2.0, 0.25 v7.4.0, 0.35 v7.3.0, 0.26 v7.1.0, 0.17 v7.0.0, 0.16 v6.4.0, 0.21 v6.3.0, 0.18 v6.2.0, 0.14 v6.1.0, 0.06 v6.0.0, 0.14 v5.5.0, 0.11 v5.4.0, 0.07 v5.3.0, 0.08 v5.2.0, 0.07 v5.1.0, 0.20 v5.0.0, 0.21 v4.1.0, 0.27 v4.0.1, 0.21 v4.0.0, 0.23 v3.7.0, 0.11 v3.4.0, 0.12 v3.3.0, 0.00 v2.1.0, 0.13 v2.0.0 % 180.94/181.14 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 180.94/181.14 % Number of literals : 5 ( 5 equ; 1 neg) % 180.94/181.14 % Maximal clause size : 1 ( 1 avg) % 180.94/181.14 % Maximal term depth : 4 ( 2 avg) % 180.94/181.14 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 180.94/181.14 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty) % 180.94/181.14 % Number of variables : 11 ( 0 sgn) % 180.94/181.14 % SPC : CNF_UNS_RFO_PEQ_UEQ % 180.94/181.14 % 180.94/181.14 % Comments : % 180.94/181.14 %-------------------------------------------------------------------------- % 180.94/181.14 cnf(s_definition,axiom, % 180.94/181.14 apply(apply(apply(s,X),Y),Z) = apply(apply(X,Z),apply(Y,Z)) ). % 180.94/181.14 % 180.94/181.14 cnf(b_definition,axiom, % 180.94/181.14 apply(apply(apply(b,X),Y),Z) = apply(X,apply(Y,Z)) ). % 180.94/181.14 % 180.94/181.14 cnf(c_definition,axiom, % 180.94/181.14 apply(apply(apply(c,X),Y),Z) = apply(apply(X,Z),Y) ). % 180.94/181.14 % 180.94/181.14 cnf(i_definition,axiom, % 180.94/181.14 apply(i,X) = X ). % 180.94/181.14 % 180.94/181.14 cnf(prove_fixed_point,negated_conjecture, % 180.94/181.14 Y != apply(fixed_pt,Y) ). % 180.94/181.14 % 180.94/181.14 %-------------------------------------------------------------------------- % 180.94/181.14 %------------------------------------------- % 180.94/181.14 % Proof found % 180.94/181.14 % SZS status Theorem for theBenchmark % 180.94/181.14 % SZS output start Proof % 180.97/181.16 %ClaNum:10(EqnAxiom:5) % 180.97/181.16 %VarNum:23(SingletonVarNum:11) % 180.97/181.16 %MaxLitNum:1 % 180.97/181.16 %MaxfuncDepth:3 % 180.97/181.16 %SharedTerms:5 % 180.97/181.16 %goalClause: 10 % 180.97/181.16 %singleGoalClaCount:1 % 180.97/181.16 [6]E(f2(a1,x61),x61) % 180.97/181.16 [10]~E(f2(a5,x101),x101) % 180.97/181.16 [7]E(f2(f2(f2(a3,x71),x72),x73),f2(x71,f2(x72,x73))) % 180.97/181.16 [8]E(f2(f2(f2(a4,x81),x82),x83),f2(f2(x81,x83),x82)) % 180.97/181.16 [9]E(f2(f2(f2(a6,x91),x92),x93),f2(f2(x91,x93),f2(x92,x93))) % 180.97/181.16 %EqnAxiom % 180.97/181.16 [1]E(x11,x11) % 180.97/181.16 [2]E(x22,x21)+~E(x21,x22) % 180.97/181.16 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 180.97/181.16 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 180.97/181.16 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 180.97/181.16 % 180.97/181.16 %------------------------------------------- % 180.97/181.18 cnf(11,plain, % 180.97/181.18 (E(x111,f2(a1,x111))), % 180.97/181.18 inference(scs_inference,[],[6,2])). % 180.97/181.18 cnf(12,plain, % 180.97/181.18 (~E(f2(a5,x121),f2(a1,x121))), % 180.97/181.18 inference(scs_inference,[],[10,6,2,3])). % 180.97/181.18 cnf(14,plain, % 180.97/181.18 (~E(a5,a1)), % 180.97/181.18 inference(scs_inference,[],[10,6,2,3,4])). % 180.97/181.18 cnf(15,plain, % 180.97/181.18 (E(f2(f2(x151,x152),f2(x153,x152)),f2(f2(f2(a6,x151),x153),x152))), % 180.97/181.18 inference(scs_inference,[],[9,2])). % 180.97/181.18 cnf(16,plain, % 180.97/181.18 (~E(f2(a5,f2(a1,x161)),x161)), % 180.97/181.18 inference(scs_inference,[],[10,11,9,2,3])). % 180.97/181.18 cnf(18,plain, % 180.97/181.18 (~E(f2(a1,f2(a5,x181)),x181)), % 180.97/181.18 inference(scs_inference,[],[10,11,9,2,3,5])). % 180.97/181.18 cnf(19,plain, % 180.97/181.18 (E(f2(x191,f2(x192,x193)),f2(f2(f2(a3,x191),x192),x193))), % 180.97/181.18 inference(scs_inference,[],[7,2])). % 180.97/181.18 cnf(20,plain, % 180.97/181.18 (E(f2(f2(x201,x202),x203),f2(f2(f2(a4,x201),x203),x202))), % 180.97/181.18 inference(scs_inference,[],[8,2])). % 180.97/181.18 cnf(21,plain, % 180.97/181.18 (~E(f2(a5,f2(x211,x212)),f2(f2(f2(a3,a1),x211),x212))), % 180.97/181.18 inference(scs_inference,[],[12,7,3])). % 180.97/181.18 cnf(24,plain, % 180.97/181.18 (~E(f2(a5,x241),f2(a1,f2(a1,x241)))), % 180.97/181.18 inference(scs_inference,[],[12,6,3])). % 180.97/181.18 cnf(26,plain, % 180.97/181.18 (~E(a5,f2(a1,a1))), % 180.97/181.18 inference(scs_inference,[],[14,6,3])). % 180.97/181.18 cnf(28,plain, % 180.97/181.18 (~E(f2(a5,f2(a1,f2(a1,x281))),x281)), % 180.97/181.18 inference(scs_inference,[],[16,11,3])). % 180.97/181.18 cnf(30,plain, % 180.97/181.18 (~E(f2(a1,f2(a1,f2(a5,x301))),x301)), % 180.97/181.18 inference(scs_inference,[],[16,11,3,5])). % 180.97/181.18 cnf(31,plain, % 180.97/181.18 (~E(f2(a1,f2(a5,f2(a1,x311))),x311)), % 180.97/181.18 inference(scs_inference,[],[30,5])). % 180.97/181.18 cnf(33,plain, % 180.97/181.18 (~E(f2(a1,f2(a5,x331)),f2(a1,x331))), % 180.97/181.18 inference(scs_inference,[],[18,6,3])). % 180.97/181.18 cnf(35,plain, % 180.97/181.18 (~E(f2(a5,x351),f2(f2(f2(a3,a1),a1),x351))), % 180.97/181.18 inference(scs_inference,[],[24,7,3])). % 180.97/181.18 cnf(37,plain, % 180.97/181.18 (~E(a5,f2(f2(a3,a1),a1))), % 180.97/181.18 inference(scs_inference,[],[24,7,3,4])). % 180.97/181.18 cnf(38,plain, % 180.97/181.18 (~E(f2(a5,x381),f2(a1,f2(a1,f2(a1,x381))))), % 180.97/181.18 inference(scs_inference,[],[24,6,3])). % 180.97/181.18 cnf(40,plain, % 180.97/181.18 (~E(a5,f2(a1,f2(a1,a1)))), % 180.97/181.18 inference(scs_inference,[],[26,6,3])). % 180.97/181.18 cnf(42,plain, % 180.97/181.18 (~E(f2(a1,f2(a1,f2(a5,x421))),f2(a1,x421))), % 180.97/181.18 inference(scs_inference,[],[30,6,3])). % 180.97/181.18 cnf(44,plain, % 180.97/181.18 (~E(f2(a1,f2(a5,x441)),f2(a1,f2(a1,x441)))), % 180.97/181.18 inference(scs_inference,[],[33,6,3])). % 180.97/181.18 cnf(46,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a4,a3),a1),a1))), % 180.97/181.18 inference(scs_inference,[],[37,8,3])). % 180.97/181.18 cnf(48,plain, % 180.97/181.18 (~E(a5,f2(a1,f2(f2(a3,a1),a1)))), % 180.97/181.18 inference(scs_inference,[],[37,6,3])). % 180.97/181.18 cnf(50,plain, % 180.97/181.18 (~E(f2(a5,x501),f2(f2(f2(a3,a1),a1),f2(a1,x501)))), % 180.97/181.18 inference(scs_inference,[],[38,7,3])). % 180.97/181.18 cnf(52,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a3,a1),a1),a1))), % 180.97/181.18 inference(scs_inference,[],[40,7,3])). % 180.97/181.18 cnf(54,plain, % 180.97/181.18 (~E(a5,f2(a1,f2(a1,f2(a1,a1))))), % 180.97/181.18 inference(scs_inference,[],[40,6,3])). % 180.97/181.18 cnf(56,plain, % 180.97/181.18 (~E(f2(a1,f2(a1,f2(a5,x561))),f2(a1,f2(a1,x561)))), % 180.97/181.18 inference(scs_inference,[],[42,6,3])). % 180.97/181.18 cnf(58,plain, % 180.97/181.18 (~E(f2(a1,f2(a5,x581)),f2(f2(f2(a3,a1),a1),x581))), % 180.97/181.18 inference(scs_inference,[],[44,7,3])). % 180.97/181.18 cnf(60,plain, % 180.97/181.18 (~E(f2(a1,f2(a5,x601)),f2(a1,f2(a1,f2(a1,x601))))), % 180.97/181.18 inference(scs_inference,[],[44,6,3])). % 180.97/181.18 cnf(62,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a3,a1),f2(a3,a1)),a1))), % 180.97/181.18 inference(scs_inference,[],[48,7,3])). % 180.97/181.18 cnf(64,plain, % 180.97/181.18 (~E(f2(a5,x641),f2(f2(f2(a4,f2(a3,a1)),f2(a1,x641)),a1))), % 180.97/181.18 inference(scs_inference,[],[50,8,3])). % 180.97/181.18 cnf(66,plain, % 180.97/181.18 (~E(a5,f2(f2(a4,f2(a3,a1)),f2(a1,a1)))), % 180.97/181.18 inference(scs_inference,[],[50,8,3,4])). % 180.97/181.18 cnf(69,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a3,a1),a1),f2(a1,a1)))), % 180.97/181.18 inference(scs_inference,[],[54,7,3])). % 180.97/181.18 cnf(73,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a4,f2(a3,a1)),a1),f2(a3,a1)))), % 180.97/181.18 inference(scs_inference,[],[62,8,3])). % 180.97/181.18 cnf(75,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a4,a4),f2(a1,a1)),f2(a3,a1)))), % 180.97/181.18 inference(scs_inference,[],[66,8,3])). % 180.97/181.18 cnf(77,plain, % 180.97/181.18 (~E(a5,f2(a1,f2(f2(a4,f2(a3,a1)),f2(a1,a1))))), % 180.97/181.18 inference(scs_inference,[],[66,6,3])). % 180.97/181.18 cnf(81,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a4,f2(a3,a1)),f2(a1,a1)),a1))), % 180.97/181.18 inference(scs_inference,[],[69,8,3])). % 180.97/181.18 cnf(89,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a4,f2(a4,a4)),f2(a3,a1)),f2(a1,a1)))), % 180.97/181.18 inference(scs_inference,[],[75,8,3])). % 180.97/181.18 cnf(93,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a3,a1),f2(a4,f2(a3,a1))),f2(a1,a1)))), % 180.97/181.18 inference(scs_inference,[],[77,7,3])). % 180.97/181.18 cnf(103,plain, % 180.97/181.18 (~E(a5,f2(a1,f2(f2(f2(a4,f2(a4,a4)),f2(a3,a1)),f2(a1,a1))))), % 180.97/181.18 inference(scs_inference,[],[89,6,3])). % 180.97/181.18 cnf(107,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a4,f2(a3,a1)),f2(a1,a1)),f2(a4,f2(a3,a1))))), % 180.97/181.18 inference(scs_inference,[],[93,8,3])). % 180.97/181.18 cnf(111,plain, % 180.97/181.18 (~E(a5,f2(f2(f2(a3,a1),f2(f2(a4,f2(a4,a4)),f2(a3,a1))),f2(a1,a1)))), % 180.97/181.18 inference(scs_inference,[],[103,7,3])). % 180.97/181.18 cnf(115,plain, % 180.97/181.18 (E(f2(f2(a1,x1151),x1152),f2(x1151,x1152))), % 180.97/181.18 inference(scs_inference,[],[6,4])). % 180.97/181.18 cnf(116,plain, % 180.97/181.18 (E(f2(x1161,f2(a1,x1162)),f2(x1161,x1162))), % 180.97/181.18 inference(scs_inference,[],[6,4,5])). % 180.97/181.18 cnf(117,plain, % 180.97/181.18 (~E(f2(f2(f2(a4,a3),a1),a1),a5)), % 180.97/181.18 inference(scs_inference,[],[6,46,4,5,2])). % 180.97/181.18 cnf(118,plain, % 180.97/181.18 (~E(f2(a1,a5),f2(f2(f2(a4,a3),a1),a1))), % 180.97/181.18 inference(scs_inference,[],[6,46,11,4,5,2,3])). % 180.97/181.18 cnf(120,plain, % 180.97/181.18 (E(f2(f2(f2(a1,x1201),x1202),x1203),f2(f2(x1201,x1202),x1203))), % 180.97/181.18 inference(scs_inference,[],[115,4])). % 180.97/181.18 cnf(121,plain, % 180.97/181.18 (E(f2(x1211,f2(f2(a1,x1212),x1213)),f2(x1211,f2(x1212,x1213)))), % 180.97/181.18 inference(scs_inference,[],[115,4,5])). % 180.97/181.18 cnf(122,plain, % 180.97/181.18 (~E(f2(f2(f2(a3,a1),a1),a1),a5)), % 180.97/181.18 inference(scs_inference,[],[115,52,4,5,2])). % 180.97/181.18 cnf(123,plain, % 180.97/181.18 (E(f2(f2(a1,a1),x1231),x1231)), % 180.97/181.18 inference(scs_inference,[],[6,115,52,4,5,2,3])). % 180.97/181.18 cnf(125,plain, % 180.97/181.18 (E(f2(f2(x1251,f2(a1,x1252)),x1253),f2(f2(x1251,x1252),x1253))), % 180.97/181.18 inference(scs_inference,[],[116,4])). % 180.97/181.18 cnf(126,plain, % 180.97/181.18 (E(f2(x1261,f2(x1262,f2(a1,x1263))),f2(x1261,f2(x1262,x1263)))), % 180.97/181.18 inference(scs_inference,[],[116,4,5])). % 180.97/181.18 cnf(127,plain, % 180.97/181.18 (~E(f2(f2(f2(a4,a3),a1),a1),f2(a1,a5))), % 180.97/181.18 inference(scs_inference,[],[116,118,4,5,2])). % 180.97/181.18 cnf(128,plain, % 180.97/181.18 (~E(f2(a1,a5),f2(f2(f2(a4,f2(a3,a1)),a1),f2(a3,a1)))), % 180.97/181.18 inference(scs_inference,[],[116,118,73,11,4,5,2,3])). % 180.97/181.18 cnf(131,plain, % 180.97/181.18 (E(f2(x1311,f2(f2(a1,a1),x1312)),f2(x1311,x1312))), % 180.97/181.18 inference(scs_inference,[],[123,4,5])). % 180.97/181.18 cnf(133,plain, % 180.97/181.18 (E(f2(f2(a1,a1),f2(a1,x1331)),x1331)), % 180.97/181.18 inference(scs_inference,[],[6,123,35,4,5,2,3])). % 180.97/181.18 cnf(135,plain, % 180.97/181.18 (E(f2(f2(f2(a1,a1),f2(a1,x1351)),x1352),f2(x1351,x1352))), % 180.97/181.18 inference(scs_inference,[],[133,4])). % 180.97/181.18 cnf(136,plain, % 180.97/181.18 (E(f2(x1361,f2(f2(a1,a1),f2(a1,x1362))),f2(x1361,x1362))), % 180.97/181.18 inference(scs_inference,[],[133,4,5])). % 180.97/181.18 cnf(138,plain, % 180.97/181.18 (~E(f2(a1,a5),f2(f2(f2(a4,f2(a3,a1)),f2(a1,a1)),a1))), % 180.97/181.18 inference(scs_inference,[],[133,28,81,11,4,5,2,3])). % 180.97/181.19 cnf(140,plain, % 180.97/181.19 (E(f2(x1401,x1402),f2(f2(a1,x1401),x1402))), % 180.97/181.19 inference(scs_inference,[],[11,4])). % 180.97/181.19 cnf(141,plain, % 180.97/181.19 (E(f2(x1411,x1412),f2(x1411,f2(a1,x1412)))), % 180.97/181.19 inference(scs_inference,[],[11,4,5])). % 180.97/181.19 cnf(146,plain, % 180.97/181.19 (E(f2(f2(x1461,x1462),x1463),f2(f2(f2(a1,x1461),x1462),x1463))), % 180.97/181.19 inference(scs_inference,[],[140,4])). % 180.97/181.19 cnf(147,plain, % 180.97/181.19 (E(f2(x1471,f2(x1472,x1473)),f2(x1471,f2(f2(a1,x1472),x1473)))), % 180.97/181.19 inference(scs_inference,[],[140,4,5])). % 180.97/181.19 cnf(149,plain, % 180.97/181.19 (~E(f2(f2(a1,a5),f2(x1491,x1492)),f2(f2(f2(a3,a1),x1491),x1492))), % 180.97/181.19 inference(scs_inference,[],[140,128,21,4,5,2,3])). % 180.97/181.19 cnf(151,plain, % 180.97/181.19 (E(f2(f2(x1511,x1512),x1513),f2(f2(x1511,f2(a1,x1512)),x1513))), % 180.97/181.19 inference(scs_inference,[],[141,4])). % 180.97/181.19 cnf(152,plain, % 180.97/181.19 (E(f2(x1521,f2(x1522,x1523)),f2(x1521,f2(x1522,f2(a1,x1523))))), % 180.97/181.19 inference(scs_inference,[],[141,4,5])). % 180.97/181.19 cnf(154,plain, % 180.97/181.19 (~E(f2(f2(f2(a4,a3),a1),f2(a1,a1)),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[141,127,56,4,5,2,3])). % 180.97/181.19 cnf(156,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(f2(a4,a3),a1),f2(a1,a1)))), % 180.97/181.19 inference(scs_inference,[],[154,2])). % 180.97/181.19 cnf(157,plain, % 180.97/181.19 (~E(f2(f2(a1,a5),x1571),f2(f2(f2(a3,a1),f2(a1,a1)),x1571))), % 180.97/181.19 inference(scs_inference,[],[154,131,149,2,3])). % 180.97/181.19 cnf(161,plain, % 180.97/181.19 (~E(a5,f2(f2(f2(a4,a3),a1),f2(a1,a1)))), % 180.97/181.19 inference(scs_inference,[],[6,156,157,2,3])). % 180.97/181.19 cnf(163,plain, % 180.97/181.19 (~E(f2(f2(f2(a4,a3),a1),f2(a1,a1)),a5)), % 180.97/181.19 inference(scs_inference,[],[161,2])). % 180.97/181.19 cnf(167,plain, % 180.97/181.19 (~E(f2(f2(f2(a4,f2(a4,a3)),f2(a1,a1)),a1),a5)), % 180.97/181.19 inference(scs_inference,[],[163,20,138,2,3])). % 180.97/181.19 cnf(170,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a1)),a5)), % 180.97/181.19 inference(scs_inference,[],[7,122,58,2,3])). % 180.97/181.19 cnf(173,plain, % 180.97/181.19 (~E(f2(a1,f2(f2(a1,a1),a1)),a5)), % 180.97/181.19 inference(scs_inference,[],[170,147,64,2,3])). % 180.97/181.19 cnf(175,plain, % 180.97/181.19 (~E(a5,f2(a1,f2(f2(a1,a1),a1)))), % 180.97/181.19 inference(scs_inference,[],[173,2])). % 180.97/181.19 cnf(182,plain, % 180.97/181.19 (~E(a5,f2(f2(f2(a4,f2(a4,a3)),f2(a1,a1)),a1))), % 180.97/181.19 inference(scs_inference,[],[167,2])). % 180.97/181.19 cnf(183,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(a1,f2(f2(a1,a1),a1)))), % 180.97/181.19 inference(scs_inference,[],[175,167,11,2,3])). % 180.97/181.19 cnf(185,plain, % 180.97/181.19 (~E(f2(a1,f2(f2(a1,a1),a1)),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[183,2])). % 180.97/181.19 cnf(186,plain, % 180.97/181.19 (~E(f2(f2(a1,a1),a5),f2(a1,f2(f2(a1,a1),a1)))), % 180.97/181.19 inference(scs_inference,[],[183,140,2,3])). % 180.97/181.19 cnf(189,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a1)),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[185,121,186,2,3])). % 180.97/181.19 cnf(191,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(a1,f2(a1,a1)))), % 180.97/181.19 inference(scs_inference,[],[189,2])). % 180.97/181.19 cnf(192,plain, % 180.97/181.19 (~E(f2(f2(f2(a3,a1),a1),a1),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[189,19,2,3])). % 180.97/181.19 cnf(194,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(f2(a3,a1),a1),a1))), % 180.97/181.19 inference(scs_inference,[],[192,2])). % 180.97/181.19 cnf(195,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a5)),f2(a1,f2(a1,a1)))), % 180.97/181.19 inference(scs_inference,[],[191,192,141,2,3])). % 180.97/181.19 cnf(197,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a1)),f2(a1,f2(a1,a5)))), % 180.97/181.19 inference(scs_inference,[],[195,2])). % 180.97/181.19 cnf(198,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,f2(a1,a5))),f2(a1,f2(a1,a1)))), % 180.97/181.19 inference(scs_inference,[],[195,152,2,3])). % 180.97/181.19 cnf(201,plain, % 180.97/181.19 (~E(f2(f2(f2(a3,a1),a1),a1),f2(a1,f2(a1,a5)))), % 180.97/181.19 inference(scs_inference,[],[197,198,19,2,3])). % 180.97/181.19 cnf(204,plain, % 180.97/181.19 (~E(f2(f2(a1,a1),a5),f2(f2(f2(a3,a1),a1),a1))), % 180.97/181.19 inference(scs_inference,[],[194,201,140,2,3])). % 180.97/181.19 cnf(206,plain, % 180.97/181.19 (~E(f2(f2(f2(a3,a1),a1),a1),f2(f2(a1,a1),a5))), % 180.97/181.19 inference(scs_inference,[],[204,2])). % 180.97/181.19 cnf(207,plain, % 180.97/181.19 (~E(f2(f2(a3,a1),a1),a5)), % 180.97/181.19 inference(scs_inference,[],[8,117,204,2,3])). % 180.97/181.19 cnf(209,plain, % 180.97/181.19 (~E(a1,a5)), % 180.97/181.19 inference(scs_inference,[],[14,2])). % 180.97/181.19 cnf(210,plain, % 180.97/181.19 (~E(f2(f2(f2(a1,a3),a1),a1),a5)), % 180.97/181.19 inference(scs_inference,[],[207,146,14,2,3])). % 180.97/181.19 cnf(212,plain, % 180.97/181.19 (~E(a5,f2(f2(f2(a1,a3),a1),a1))), % 180.97/181.19 inference(scs_inference,[],[210,2])). % 180.97/181.19 cnf(213,plain, % 180.97/181.19 (~E(f2(a1,a1),a5)), % 180.97/181.19 inference(scs_inference,[],[209,210,11,2,3])). % 180.97/181.19 cnf(216,plain, % 180.97/181.19 (~E(f2(f2(a1,a1),a1),a5)), % 180.97/181.19 inference(scs_inference,[],[213,33,140,2,3])). % 180.97/181.19 cnf(218,plain, % 180.97/181.19 (~E(a5,f2(f2(a1,a1),a1))), % 180.97/181.19 inference(scs_inference,[],[216,2])). % 180.97/181.19 cnf(219,plain, % 180.97/181.19 (~E(f2(f2(a1,f2(a1,a1)),a1),a5)), % 180.97/181.19 inference(scs_inference,[],[216,151,2,3])). % 180.97/181.19 cnf(221,plain, % 180.97/181.19 (~E(a5,f2(f2(a1,f2(a1,a1)),a1))), % 180.97/181.19 inference(scs_inference,[],[219,2])). % 180.97/181.19 cnf(225,plain, % 180.97/181.19 (~E(x2251,f2(a5,f2(a1,x2251)))), % 180.97/181.19 inference(scs_inference,[],[16,2])). % 180.97/181.19 cnf(226,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(a1,a1),a1))), % 180.97/181.19 inference(scs_inference,[],[218,16,11,2,3])). % 180.97/181.19 cnf(228,plain, % 180.97/181.19 (~E(f2(f2(a1,a1),a1),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[226,2])). % 180.97/181.19 cnf(229,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a5)),f2(f2(a1,a1),a1))), % 180.97/181.19 inference(scs_inference,[],[226,141,2,3])). % 180.97/181.19 cnf(231,plain, % 180.97/181.19 (~E(f2(f2(a1,a1),a1),f2(a1,f2(a1,a5)))), % 180.97/181.19 inference(scs_inference,[],[229,2])). % 180.97/181.19 cnf(232,plain, % 180.97/181.19 (~E(f2(f2(f2(a4,a1),a1),a1),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[228,229,20,2,3])). % 180.97/181.19 cnf(234,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(f2(a4,a1),a1),a1))), % 180.97/181.19 inference(scs_inference,[],[232,2])). % 180.97/181.19 cnf(235,plain, % 180.97/181.19 (~E(f2(x2351,f2(a1,x2352)),f2(a5,f2(a1,f2(x2351,x2352))))), % 180.97/181.19 inference(scs_inference,[],[225,232,141,2,3])). % 180.97/181.19 cnf(238,plain, % 180.97/181.19 (~E(f2(f2(f2(a1,a1),a1),a1),f2(a1,f2(a1,a5)))), % 180.97/181.19 inference(scs_inference,[],[231,235,146,2,3])). % 180.97/181.19 cnf(241,plain, % 180.97/181.19 (~E(f2(f2(a1,a1),a5),f2(f2(f2(a4,a1),a1),a1))), % 180.97/181.19 inference(scs_inference,[],[234,238,140,2,3])). % 180.97/181.19 cnf(244,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(a1,f2(a1,a1)),a1))), % 180.97/181.19 inference(scs_inference,[],[221,241,11,2,3])). % 180.97/181.19 cnf(246,plain, % 180.97/181.19 (~E(f2(f2(a1,f2(a1,a1)),a1),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[244,2])). % 180.97/181.19 cnf(247,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a5)),f2(f2(a1,f2(a1,a1)),a1))), % 180.97/181.19 inference(scs_inference,[],[244,141,2,3])). % 180.97/181.19 cnf(250,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(f2(a1,a3),a1),a1))), % 180.97/181.19 inference(scs_inference,[],[212,247,11,2,3])). % 180.97/181.19 cnf(252,plain, % 180.97/181.19 (~E(f2(f2(f2(a1,a3),a1),a1),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[250,2])). % 180.97/181.19 cnf(253,plain, % 180.97/181.19 (~E(f2(f2(f2(a4,a1),a1),f2(a1,a1)),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[246,250,20,2,3])). % 180.97/181.19 cnf(255,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(f2(a4,a1),a1),f2(a1,a1)))), % 180.97/181.19 inference(scs_inference,[],[253,2])). % 180.97/181.19 cnf(256,plain, % 180.97/181.19 (~E(f2(f2(a3,a1),a1),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[253,252,120,2,3])). % 180.97/181.19 cnf(258,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(a3,a1),a1))), % 180.97/181.19 inference(scs_inference,[],[256,2])). % 180.97/181.19 cnf(259,plain, % 180.97/181.19 (~E(f2(f2(a3,f2(a1,a1)),a1),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[256,151,2,3])). % 180.97/181.19 cnf(261,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(a3,f2(a1,a1)),a1))), % 180.97/181.19 inference(scs_inference,[],[259,2])). % 180.97/181.19 cnf(262,plain, % 180.97/181.19 (~E(f2(f2(a1,a1),a5),f2(f2(a3,a1),a1))), % 180.97/181.19 inference(scs_inference,[],[258,259,140,2,3])). % 180.97/181.19 cnf(264,plain, % 180.97/181.19 (~E(f2(f2(a3,a1),a1),f2(f2(a1,a1),a5))), % 180.97/181.19 inference(scs_inference,[],[262,2])). % 180.97/181.19 cnf(265,plain, % 180.97/181.19 (~E(f2(f2(f2(a1,a1),a1),a5),f2(f2(a3,a1),a1))), % 180.97/181.19 inference(scs_inference,[],[262,146,2,3])). % 180.97/181.19 cnf(268,plain, % 180.97/181.19 (~E(f2(a1,f2(f2(a3,a1),a1)),f2(f2(a1,a1),a5))), % 180.97/181.19 inference(scs_inference,[],[11,264,265,2,3])). % 180.97/181.19 cnf(271,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a5)),f2(f2(f2(a4,a1),a1),f2(a1,a1)))), % 180.97/181.19 inference(scs_inference,[],[11,255,268,2,3])). % 180.97/181.19 cnf(273,plain, % 180.97/181.19 (~E(f2(f2(f2(a4,a1),a1),f2(a1,a1)),f2(a1,f2(a1,a5)))), % 180.97/181.19 inference(scs_inference,[],[271,2])). % 180.97/181.19 cnf(274,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a5)),f2(f2(a3,f2(a1,a1)),a1))), % 180.97/181.19 inference(scs_inference,[],[11,271,261,2,3])). % 180.97/181.19 cnf(277,plain, % 180.97/181.19 (~E(f2(f2(f2(a4,a1),f2(a1,a1)),f2(a1,a1)),f2(a1,f2(a1,a5)))), % 180.97/181.19 inference(scs_inference,[],[273,274,151,2,3])). % 180.97/181.19 cnf(279,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a5)),f2(f2(f2(a4,a1),f2(a1,a1)),f2(a1,a1)))), % 180.97/181.19 inference(scs_inference,[],[277,2])). % 180.97/181.19 cnf(280,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(f2(a4,f2(a4,a3)),f2(a1,a1)),a1))), % 180.97/181.19 inference(scs_inference,[],[11,277,182,2,3])). % 180.97/181.19 cnf(283,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(f2(f2(a4,a1),f2(a1,a1)),f2(a1,a1)))), % 180.97/181.19 inference(scs_inference,[],[279,280,116,2,3])). % 180.97/181.19 cnf(285,plain, % 180.97/181.19 (~E(f2(f2(f2(a4,a1),f2(a1,a1)),f2(a1,a1)),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[283,2])). % 180.97/181.19 cnf(286,plain, % 180.97/181.19 (~E(f2(a1,a5),f2(a1,a1))), % 180.97/181.19 inference(scs_inference,[],[11,283,26,2,3])). % 180.97/181.19 cnf(289,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a5)),f2(a1,a1))), % 180.97/181.19 inference(scs_inference,[],[11,286,2,3])). % 180.97/181.19 cnf(292,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,f2(a1,a5))),f2(a1,a1))), % 180.97/181.19 inference(scs_inference,[],[11,289,2,3])). % 180.97/181.19 cnf(295,plain, % 180.97/181.19 (~E(f2(f2(f2(a4,a1),f2(a1,a1)),f2(f2(a1,a1),a1)),f2(a1,a5))), % 180.97/181.19 inference(scs_inference,[],[285,292,147,2,3])). % 180.97/181.19 cnf(298,plain, % 180.97/181.19 (~E(f2(a1,f2(a1,a5)),f2(f2(a3,a1),a1))), % 180.97/181.19 inference(scs_inference,[],[11,295,258,2,3])). % 180.97/181.19 cnf(300,plain, % 180.97/181.19 (~E(f2(a1,x3001),f2(a5,x3001))), % 180.97/181.19 inference(scs_inference,[],[12,2])). % 180.97/181.19 cnf(301,plain, % 180.97/181.19 (~E(f2(a5,x3011),f2(a1,f2(f2(a1,a1),f2(a1,x3011))))), % 180.97/181.19 inference(scs_inference,[],[12,136,2,3])). % 180.97/181.19 cnf(304,plain, % 180.97/181.20 (~E(f2(f2(a3,a1),a1),f2(a1,f2(a1,a5)))), % 180.97/181.20 inference(scs_inference,[],[298,2])). % 180.97/181.20 cnf(305,plain, % 180.97/181.20 (~E(f2(a5,f2(x3051,x3052)),f2(a1,f2(x3051,f2(a1,x3052))))), % 180.97/181.20 inference(scs_inference,[],[12,298,126,2,3])). % 180.97/181.20 cnf(309,plain, % 180.97/181.20 (~E(f2(a5,x3091),f2(a1,f2(f2(a1,a1),x3091)))), % 180.97/181.20 inference(scs_inference,[],[12,301,131,2,3])). % 180.97/181.20 cnf(313,plain, % 180.97/181.20 (~E(f2(a1,x3131),f2(a5,f2(f2(a1,a1),f2(a1,x3131))))), % 180.97/181.20 inference(scs_inference,[],[300,309,136,2,3])). % 180.97/181.20 cnf(316,plain, % 180.97/181.20 (~E(f2(a5,f2(f2(a1,a1),f2(a1,x3161))),f2(a1,x3161))), % 180.97/181.20 inference(scs_inference,[],[313,2])). % 180.97/181.20 cnf(317,plain, % 180.97/181.20 (~E(f2(a5,f2(x3171,x3172)),f2(a1,f2(f2(a1,x3171),x3172)))), % 180.97/181.20 inference(scs_inference,[],[12,313,121,2,3])). % 180.97/181.20 cnf(321,plain, % 180.97/181.20 (~E(f2(f2(f2(a4,a3),a1),a1),f2(a1,f2(a1,a5)))), % 180.97/181.20 inference(scs_inference,[],[304,305,20,2,3])). % 180.97/181.20 cnf(324,plain, % 180.97/181.20 (~E(f2(a5,f2(x3241,f2(a1,x3242))),f2(a1,f2(x3241,x3242)))), % 180.97/181.20 inference(scs_inference,[],[12,321,152,2,3])). % 180.97/181.20 cnf(328,plain, % 180.97/181.20 (~E(f2(a5,f2(f2(a1,a1),x3281)),f2(a1,x3281))), % 180.97/181.20 inference(scs_inference,[],[316,324,126,2,3])). % 180.97/181.20 cnf(332,plain, % 180.97/181.20 (~E(f2(f2(f2(a3,a5),x3321),x3322),f2(a1,f2(x3321,x3322)))), % 180.97/181.20 inference(scs_inference,[],[12,328,19,2,3])). % 180.97/181.20 cnf(335,plain, % 180.97/181.20 (~E(f2(a1,f2(x3351,x3352)),f2(f2(f2(a3,a5),x3351),x3352))), % 180.97/181.20 inference(scs_inference,[],[332,2])). % 180.97/181.20 cnf(338,plain, % 180.97/181.20 (~E(f2(a1,f2(f2(a1,x3381),x3382)),f2(a5,f2(x3381,x3382)))), % 180.97/181.20 inference(scs_inference,[],[317,2])). % 180.97/181.20 cnf(355,plain, % 180.97/181.20 (~E(f2(a1,f2(f2(a3,a1),a1)),a5)), % 180.97/181.20 inference(scs_inference,[],[48,2])). % 180.97/181.20 cnf(384,plain, % 180.97/181.20 (~E(f2(a5,f2(f2(a1,a1),x3841)),x3841)), % 180.97/181.20 inference(scs_inference,[],[16,21,147,2,3])). % 180.97/181.20 cnf(387,plain, % 180.97/181.20 (~E(f2(a1,f2(f2(a3,a1),f2(a1,a1))),a5)), % 180.97/181.20 inference(scs_inference,[],[384,355,152,2,3])). % 180.97/181.20 cnf(389,plain, % 180.97/181.20 (~E(a5,f2(a1,f2(f2(a3,a1),f2(a1,a1))))), % 180.97/181.20 inference(scs_inference,[],[387,2])). % 180.97/181.20 cnf(390,plain, % 180.97/181.20 (~E(f2(f2(f2(a3,a5),a1),x3901),x3901)), % 180.97/181.20 inference(scs_inference,[],[16,387,19,2,3])). % 180.97/181.20 cnf(392,plain, % 180.97/181.20 (~E(x3921,f2(f2(f2(a3,a5),a1),x3921))), % 180.97/181.20 inference(scs_inference,[],[390,2])). % 180.97/181.20 cnf(393,plain, % 180.97/181.20 (~E(f2(a1,a5),f2(a1,f2(f2(a3,a1),f2(a1,a1))))), % 180.97/181.20 inference(scs_inference,[],[390,389,11,2,3])). % 180.97/181.20 cnf(396,plain, % 180.97/181.20 (~E(f2(f2(a1,a5),f2(a1,x3961)),x3961)), % 180.97/181.20 inference(scs_inference,[],[16,393,140,2,3])). % 180.97/181.20 cnf(399,plain, % 180.97/181.20 (~E(f2(f2(f2(a6,a1),a1),a5),a5)), % 180.97/181.20 inference(scs_inference,[],[396,15,2,3])). % 180.97/181.20 cnf(402,plain, % 180.97/181.20 (~E(a5,f2(f2(f2(a6,a1),a1),a5))), % 180.97/181.20 inference(scs_inference,[],[399,2])). % 180.97/181.20 cnf(405,plain, % 180.97/181.20 (~E(f2(a1,a5),f2(f2(f2(a6,a1),a1),a5))), % 180.97/181.20 inference(scs_inference,[],[402,60,11,2,3])). % 180.97/181.20 cnf(407,plain, % 180.97/181.20 (~E(f2(f2(f2(a6,a1),a1),a5),f2(a1,a5))), % 180.97/181.20 inference(scs_inference,[],[405,2])). % 180.97/181.20 cnf(408,plain, % 180.97/181.20 (~E(x4081,f2(a5,x4081))), % 180.97/181.20 inference(scs_inference,[],[10,2])). % 180.97/181.20 cnf(409,plain, % 180.97/181.20 (~E(f2(f2(a4,f2(a3,a1)),f2(a1,a1)),a5)), % 180.97/181.20 inference(scs_inference,[],[66,2])). % 180.97/181.20 cnf(410,plain, % 180.97/181.20 (~E(x4101,f2(a5,f2(f2(a1,a1),f2(a1,x4101))))), % 180.97/181.20 inference(scs_inference,[],[408,133,66,2,3])). % 180.97/181.20 cnf(413,plain, % 180.97/181.20 (~E(f2(f2(a4,f2(a1,f2(a3,a1))),f2(a1,a1)),a5)), % 180.97/181.20 inference(scs_inference,[],[409,410,151,2,3])). % 180.97/181.20 cnf(416,plain, % 180.97/181.20 (~E(f2(a1,f2(f2(a1,a5),x4161)),x4161)), % 180.97/181.20 inference(scs_inference,[],[18,413,147,2,3])). % 180.97/181.20 cnf(419,plain, % 180.97/181.20 (~E(f2(f2(a1,a5),f2(a1,a5)),f2(a1,a5))), % 180.97/181.20 inference(scs_inference,[],[407,416,9,2,3])). % 180.97/181.20 cnf(422,plain, % 180.97/181.20 (~E(f2(f2(f2(a4,a1),f2(a1,a5)),a5),f2(a1,a5))), % 180.97/181.20 inference(scs_inference,[],[419,20,2,3])). % 180.97/181.20 cnf(424,plain, % 180.97/181.20 (~E(f2(a1,a5),f2(f2(f2(a4,a1),f2(a1,a5)),a5))), % 180.97/181.20 inference(scs_inference,[],[422,2])). % 180.97/181.20 cnf(455,plain, % 180.97/181.20 (~E(f2(a1,f2(a1,a5)),f2(f2(f2(a4,a1),f2(a1,a5)),a5))), % 180.97/181.20 inference(scs_inference,[],[424,44,141,2,3])). % 180.97/181.20 cnf(457,plain, % 180.97/181.20 (~E(f2(f2(f2(a4,a1),f2(a1,a5)),a5),f2(a1,f2(a1,a5)))), % 180.97/181.20 inference(scs_inference,[],[455,2])). % 180.97/181.20 cnf(485,plain, % 180.97/181.20 (~E(f2(a1,f2(a1,x4851)),f2(f2(a1,a5),x4851))), % 180.97/181.20 inference(scs_inference,[],[24,140,3,2])). % 180.97/181.20 cnf(498,plain, % 180.97/181.20 (~E(f2(a1,f2(a1,x4981)),f2(f2(a1,a5),f2(a1,x4981)))), % 180.97/181.20 inference(scs_inference,[],[485,126,3])). % 180.97/181.20 cnf(508,plain, % 180.97/181.20 (~E(f2(f2(f2(a3,a1),f2(a1,a1)),a1),f2(f2(a1,a1),a5))), % 180.97/181.20 inference(scs_inference,[],[206,151,3])). % 180.97/181.20 cnf(511,plain, % 180.97/181.20 (~E(f2(f2(f2(a3,a1),a1),f2(a5,x5111)),x5111)), % 180.97/181.20 inference(scs_inference,[],[30,508,19,2,3])). % 180.97/181.20 cnf(514,plain, % 180.97/181.20 (~E(f2(f2(f2(a4,a1),a5),a5),f2(a1,f2(a1,a5)))), % 180.97/181.20 inference(scs_inference,[],[511,457,125,2,3])). % 180.97/181.20 cnf(516,plain, % 180.97/181.20 (~E(f2(a1,f2(a1,a5)),f2(f2(f2(a4,a1),a5),a5))), % 180.97/181.20 inference(scs_inference,[],[514,2])). % 180.97/181.20 cnf(540,plain, % 180.97/181.20 (~E(x5401,f2(f2(a1,a1),f2(a5,f2(a1,x5401))))), % 180.97/181.20 inference(scs_inference,[],[31,140,3,2])). % 180.97/181.20 cnf(552,plain, % 180.97/181.20 (~E(f2(a1,x5521),f2(a1,f2(f2(a1,a5),x5521)))), % 180.97/181.20 inference(scs_inference,[],[33,147,3,2])). % 180.97/181.20 cnf(558,plain, % 180.97/181.20 (~E(f2(a1,x5581),f2(f2(f2(a3,a1),a5),x5581))), % 180.97/181.20 inference(scs_inference,[],[33,19,3,2])). % 180.97/181.20 cnf(562,plain, % 180.97/181.20 (~E(f2(f2(a1,a5),f2(a1,x5621)),f2(a1,x5621))), % 180.97/181.20 inference(scs_inference,[],[498,116,3,2])). % 180.97/181.20 cnf(563,plain, % 180.97/181.20 (~E(f2(f2(a1,f2(a1,a5)),f2(a1,x5631)),f2(a1,x5631))), % 180.97/181.20 inference(scs_inference,[],[562,151,3])). % 180.97/181.20 cnf(569,plain, % 180.97/181.20 (~E(f2(a1,x5691),f2(f2(f2(a3,a1),a5),f2(f2(a1,a1),x5691)))), % 180.97/181.20 inference(scs_inference,[],[558,131,3])). % 180.97/181.20 cnf(572,plain, % 180.97/181.20 (~E(f2(f2(f2(a3,a1),a5),f2(f2(a1,a1),x5721)),f2(a1,x5721))), % 180.97/181.20 inference(scs_inference,[],[569,2])). % 180.97/181.20 cnf(573,plain, % 180.97/181.20 (~E(f2(a5,x5731),f2(f2(f2(a3,a1),a1),f2(f2(a1,a1),f2(a1,x5731))))), % 180.97/181.20 inference(scs_inference,[],[35,136,3])). % 180.97/181.20 cnf(577,plain, % 180.97/181.20 (~E(f2(f2(f2(a6,f2(a3,a1)),f2(a1,a1)),a5),f2(a1,a5))), % 180.97/181.20 inference(scs_inference,[],[572,573,15,2,3])). % 180.97/181.20 cnf(580,plain, % 180.97/181.20 (~E(f2(a1,a5),f2(f2(f2(a6,f2(a3,a1)),f2(a1,a1)),a5))), % 180.97/181.20 inference(scs_inference,[],[577,2])). % 180.97/181.20 cnf(613,plain, % 180.97/181.20 (~E(f2(f2(f2(a3,a5),f2(a1,a1)),f2(a1,x6131)),f2(a1,x6131))), % 180.97/181.20 inference(scs_inference,[],[335,136,3,2])). % 180.97/181.20 cnf(631,plain, % 180.97/181.20 (~E(f2(a1,f2(f2(a1,x6311),f2(a1,x6312))),f2(a5,f2(x6311,x6312)))), % 180.97/181.20 inference(scs_inference,[],[338,152,3])). % 180.97/181.20 cnf(634,plain, % 180.97/181.20 (~E(f2(a5,f2(x6341,x6342)),f2(a1,f2(f2(a1,x6341),f2(a1,x6342))))), % 180.97/181.20 inference(scs_inference,[],[631,2])). % 180.97/181.20 cnf(766,plain, % 180.97/181.20 (~E(f2(a1,a5),f2(f2(f2(a4,a1),a5),a5))), % 180.97/181.20 inference(scs_inference,[],[516,116,3])). % 180.97/181.20 cnf(769,plain, % 180.97/181.20 (~E(f2(f2(a1,f2(a1,a5)),x7691),f2(a1,x7691))), % 180.97/181.20 inference(scs_inference,[],[116,563,3])). % 180.97/181.20 cnf(779,plain, % 180.97/181.20 (~E(f2(a1,x7791),f2(f2(a1,a5),x7791))), % 180.97/181.20 inference(scs_inference,[],[769,125,3,2])). % 180.97/181.20 cnf(801,plain, % 180.97/181.20 (~E(f2(f2(f2(a3,a5),f2(a1,a1)),f2(a1,x8011)),f2(a1,f2(a1,x8011)))), % 180.97/181.20 inference(scs_inference,[],[126,613,3])). % 180.97/181.20 cnf(807,plain, % 180.97/181.20 (~E(f2(a1,f2(a1,x8071)),f2(f2(f2(a3,a5),a1),f2(a1,x8071)))), % 180.97/181.20 inference(scs_inference,[],[801,125,3,2])). % 180.97/181.20 cnf(808,plain, % 180.97/181.20 (~E(x8081,f2(f2(f2(a3,a5),a1),f2(f2(a1,a1),f2(a1,x8081))))), % 180.97/181.20 inference(scs_inference,[],[133,392,3])). % 180.97/181.20 cnf(810,plain, % 180.97/181.20 (~E(f2(f2(f2(a3,a5),a1),f2(f2(a1,a1),f2(a1,x8101))),x8101)), % 180.97/181.20 inference(scs_inference,[],[808,2])). % 180.97/181.20 cnf(873,plain, % 180.97/181.20 (~E(f2(f2(f2(a4,a3),a1),f2(a1,f2(a1,a1))),f2(a1,a5))), % 180.97/181.20 inference(scs_inference,[],[154,152,3])). % 180.97/181.20 cnf(876,plain, % 180.97/181.20 (~E(f2(a5,x8761),f2(a1,f2(f2(a1,f2(a1,a1)),f2(a1,x8761))))), % 180.97/181.20 inference(scs_inference,[],[873,634,131,2,3])). % 180.97/181.20 cnf(880,plain, % 180.97/181.20 (~E(f2(f2(f2(a4,a3),a1),f2(f2(a1,a1),a1)),f2(a1,a5))), % 180.97/181.20 inference(scs_inference,[],[154,876,147,2,3])). % 180.97/181.20 cnf(883,plain, % 180.97/181.20 (~E(f2(f2(f2(a6,f2(a4,a3)),f2(a1,a1)),a1),f2(a1,a5))), % 180.97/181.20 inference(scs_inference,[],[880,15,2,3])). % 180.97/181.20 cnf(886,plain, % 180.97/181.20 (~E(f2(f2(f2(a4,a3),f2(a1,a1)),f2(a1,a1)),f2(a1,a5))), % 180.97/181.20 inference(scs_inference,[],[154,883,151,2,3])). % 180.97/181.20 cnf(888,plain, % 180.97/181.20 (~E(f2(a1,a5),f2(f2(f2(a4,a3),f2(a1,a1)),f2(a1,a1)))), % 180.97/181.20 inference(scs_inference,[],[886,2])). % 180.97/181.20 cnf(889,plain, % 180.97/181.20 (~E(f2(a1,x8891),f2(f2(a1,a5),f2(f2(a1,a1),x8891)))), % 180.97/181.20 inference(scs_inference,[],[886,779,131,2,3])). % 180.97/181.20 cnf(893,plain, % 180.97/181.20 (~E(f2(f2(a1,f2(f2(a4,a3),a1)),f2(a1,a1)),f2(a1,a5))), % 180.97/181.20 inference(scs_inference,[],[154,889,140,2,3])). % 180.97/181.20 cnf(896,plain, % 180.97/181.20 (~E(f2(a1,f2(a1,a5)),f2(f2(f2(a4,a3),f2(a1,a1)),f2(a1,a1)))), % 180.97/181.20 inference(scs_inference,[],[888,893,141,2,3])). % 180.97/181.20 cnf(899,plain, % 180.97/181.20 (~E(f2(a1,f2(f2(f2(a4,a3),a1),f2(a1,a1))),f2(a1,a5))), % 180.97/181.20 inference(scs_inference,[],[154,896,11,2,3])). % 180.97/181.20 cnf(902,plain, % 180.97/181.20 (~E(a5,f2(f2(f2(a4,a1),a5),a5))), % 180.97/181.20 inference(scs_inference,[],[766,899,6,2,3])). % 180.97/181.20 cnf(905,plain, % 180.97/181.20 (~E(f2(f2(a1,a1),a5),f2(f2(f2(a4,a3),a1),f2(a1,a1)))), % 180.97/181.20 inference(scs_inference,[],[156,902,140,2,3])). % 180.97/181.20 cnf(908,plain, % 180.97/181.20 (~E(f2(f2(f2(a3,a5),a1),f2(a1,f2(a1,x9081))),x9081)), % 180.97/181.20 inference(scs_inference,[],[905,810,121,2,3])). % 180.97/181.20 cnf(910,plain, % 180.97/181.20 (~E(x9101,f2(f2(f2(a3,a5),a1),f2(a1,f2(a1,x9101))))), % 180.97/181.20 inference(scs_inference,[],[908,2])). % 180.97/181.20 cnf(1070,plain, % 180.97/181.20 (E(f2(f2(f2(f2(a1,a1),f2(a1,x10701)),x10702),x10703),f2(f2(x10701,x10702),x10703))), % 180.97/181.20 inference(scs_inference,[],[135,111,2,4])). % 180.97/181.20 cnf(1081,plain, % 180.97/181.20 (E(f2(f2(f2(f2(f2(a1,a1),f2(a1,x10811)),x10812),x10813),x10814),f2(f2(f2(x10811,x10812),x10813),x10814))), % 180.97/181.20 inference(scs_inference,[],[107,1070,2,4])). % 180.97/181.20 cnf(1216,plain, % 180.97/181.20 (E(f2(a1,f2(x12161,f2(f2(a1,a1),f2(a1,x12162)))),f2(x12161,x12162))), % 180.97/181.20 inference(scs_inference,[],[6,136,1081,807,540,2,5,4,3])). % 180.97/181.20 cnf(1222,plain, % 180.97/181.20 (E(f2(a1,f2(x12221,f2(x12222,f2(a1,x12223)))),f2(x12221,f2(x12222,x12223)))), % 180.97/181.20 inference(scs_inference,[],[6,126,1216,580,910,2,5,4,3])). % 180.97/181.20 cnf(1225,plain, % 180.97/181.20 (~E(x12251,f2(f2(a1,a5),x12251))), % 180.97/181.20 inference(scs_inference,[],[1222,552,2,5])). % 180.97/181.20 cnf(1657,plain, % 180.97/181.20 (E(f2(x16571,x16572),f2(f2(f2(a3,x16571),f2(a1,a1)),f2(a1,x16572)))), % 180.97/181.20 inference(scs_inference,[],[7,136,3,2])). % 180.97/181.20 cnf(1658,plain, % 180.97/181.20 (E(f2(f2(f2(a3,x16581),x16582),f2(a1,x16583)),f2(x16581,f2(x16582,x16583)))), % 180.97/181.20 inference(scs_inference,[],[7,126,3])). % 180.97/181.20 cnf(1753,plain, % 180.97/181.20 ($false), % 180.97/181.20 inference(scs_inference,[],[9,1225,1657,1658,4,5,3]), % 180.97/181.20 ['proof']). % 180.97/181.20 % SZS output end Proof % 180.97/181.20 % Total time :180.270000s %------------------------------------------------------------------------------