%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP494-1 : TPTP v8.2.0. Released v2.6.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 06:39:47 EDT 2024 % Result : Unsatisfiable 200.30s 200.68s % Output : CNFRefutation 200.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : GRP494-1 : TPTP v8.2.0. Released v2.6.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n024.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Jun 20 06:56:54 EDT 2024 % 0.13/0.35 % CPUTime : % 0.45/0.59 start to proof:theBenchmark % 200.30/200.64 %------------------------------------------- % 200.30/200.64 % File :CSE---1.7 % 200.30/200.64 % Problem :theBenchmark % 200.30/200.64 % Transform :cnf % 200.30/200.64 % Format :tptp:raw % 200.30/200.64 % Command :java -jar mcs_scs.jar %d %s % 200.30/200.64 % 200.30/200.64 % Result :Theorem 199.630000s % 200.30/200.64 % Output :CNFRefutation 199.630000s % 200.30/200.64 %------------------------------------------- % 200.30/200.68 %-------------------------------------------------------------------------- % 200.30/200.68 % File : GRP494-1 : TPTP v8.2.0. Released v2.6.0. % 200.30/200.68 % Domain : Group Theory % 200.30/200.68 % Problem : Axiom for group theory, in double division and identity, part 2 % 200.30/200.68 % Version : [McC93] (equality) axioms. % 200.30/200.68 % English : % 200.30/200.68 % 200.30/200.68 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 200.30/200.68 % Source : [TPTP] % 200.30/200.68 % Names : % 200.30/200.68 % 200.30/200.68 % Status : Unsatisfiable % 200.30/200.68 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 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.19 v5.5.0, 0.16 v5.4.0, 0.00 v5.1.0, 0.07 v5.0.0, 0.00 v2.6.0 % 200.30/200.68 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 200.30/200.68 % Number of literals : 5 ( 5 equ; 1 neg) % 200.30/200.68 % Maximal clause size : 1 ( 1 avg) % 200.30/200.68 % Maximal term depth : 5 ( 2 avg) % 200.30/200.68 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 200.30/200.68 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 200.30/200.68 % Number of variables : 7 ( 0 sgn) % 200.30/200.68 % SPC : CNF_UNS_RFO_PEQ_UEQ % 200.30/200.68 % 200.30/200.68 % Comments : A UEQ part of GRP079-1 % 200.30/200.68 %-------------------------------------------------------------------------- % 200.30/200.68 cnf(single_axiom,axiom, % 200.30/200.68 double_divide(double_divide(identity,A),double_divide(double_divide(double_divide(B,C),double_divide(identity,identity)),double_divide(A,C))) = B ). % 200.30/200.68 % 200.30/200.68 cnf(multiply,axiom, % 200.30/200.68 multiply(A,B) = double_divide(double_divide(B,A),identity) ). % 200.30/200.68 % 200.30/200.68 cnf(inverse,axiom, % 200.30/200.68 inverse(A) = double_divide(A,identity) ). % 200.30/200.68 % 200.30/200.68 cnf(identity,axiom, % 200.30/200.68 identity = double_divide(A,inverse(A)) ). % 200.30/200.68 % 200.30/200.68 cnf(prove_these_axioms_2,negated_conjecture, % 200.30/200.68 multiply(identity,a2) != a2 ). % 200.30/200.68 % 200.30/200.68 %-------------------------------------------------------------------------- % 200.30/200.68 %------------------------------------------- % 200.30/200.68 % Proof found % 200.30/200.68 % SZS status Theorem for theBenchmark % 200.30/200.68 % SZS output start Proof % 200.36/200.71 %ClaNum:8(EqnAxiom:5) % 200.36/200.71 %VarNum:8(SingletonVarNum:4) % 200.36/200.71 %MaxLitNum:1 % 200.36/200.71 %MaxfuncDepth:3 % 200.36/200.71 %SharedTerms:6 % 200.36/200.71 %goalClause: 8 % 200.36/200.71 %singleGoalClaCount:1 % 200.36/200.71 [8]~E(f2(f2(a3,a1),a1),a3) % 200.36/200.71 [6]E(f2(x61,f2(x61,a1)),a1) % 200.36/200.71 [7]E(f2(f2(a1,x71),f2(f2(f2(x72,x73),f2(a1,a1)),f2(x71,x73))),x72) % 200.36/200.71 %EqnAxiom % 200.36/200.71 [1]E(x11,x11) % 200.36/200.71 [2]E(x22,x21)+~E(x21,x22) % 200.36/200.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 200.36/200.71 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 200.36/200.71 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 200.36/200.71 % 200.36/200.71 %------------------------------------------- % 200.36/200.74 cnf(9,plain, % 200.36/200.74 (E(a1,f2(x91,f2(x91,a1)))), % 200.36/200.74 inference(scs_inference,[],[6,2])). % 200.36/200.74 cnf(10,plain, % 200.36/200.74 (~E(f2(f2(a3,a1),a1),f2(f2(a1,x101),f2(f2(f2(a3,x102),f2(a1,a1)),f2(x101,x102))))), % 200.36/200.74 inference(scs_inference,[],[8,6,7,2,3])). % 200.36/200.74 cnf(12,plain, % 200.36/200.74 (E(x121,f2(f2(a1,x122),f2(f2(f2(x121,x123),f2(a1,a1)),f2(x122,x123))))), % 200.36/200.74 inference(scs_inference,[],[7,2])). % 200.36/200.74 cnf(13,plain, % 200.36/200.74 (E(f2(x131,f2(x131,a1)),f2(x132,f2(x132,a1)))), % 200.36/200.74 inference(scs_inference,[],[9,6,7,2,3])). % 200.36/200.74 cnf(14,plain, % 200.36/200.74 (E(f2(f2(a1,x141),f2(f2(f2(a1,x142),f2(a1,a1)),f2(x141,x142))),f2(x143,f2(x143,a1)))), % 200.36/200.74 inference(scs_inference,[],[7,9,3])). % 200.36/200.74 cnf(16,plain, % 200.36/200.74 (E(f2(x161,f2(x161,a1)),f2(f2(a1,x162),f2(f2(f2(a1,x163),f2(a1,a1)),f2(x162,x163))))), % 200.36/200.74 inference(scs_inference,[],[7,9,3,2])). % 200.36/200.74 cnf(17,plain, % 200.36/200.74 (E(f2(f2(x171,f2(x171,a1)),x172),f2(a1,x172))), % 200.36/200.74 inference(scs_inference,[],[6,4])). % 200.36/200.74 cnf(18,plain, % 200.36/200.74 (E(f2(x181,f2(x182,f2(x182,a1))),f2(x181,a1))), % 200.36/200.74 inference(scs_inference,[],[6,4,5])). % 200.36/200.74 cnf(19,plain, % 200.36/200.74 (~E(f2(f2(a1,x191),f2(f2(f2(a3,x192),f2(a1,a1)),f2(x191,x192))),f2(f2(a3,a1),a1))), % 200.36/200.74 inference(scs_inference,[],[6,10,4,5,2])). % 200.36/200.74 cnf(20,plain, % 200.36/200.74 (~E(f2(f2(a1,x201),f2(f2(f2(f2(f2(a3,a1),a1),x202),f2(a1,a1)),f2(x201,x202))),a3)), % 200.36/200.74 inference(scs_inference,[],[6,12,10,8,4,5,2,3])). % 200.36/200.74 cnf(22,plain, % 200.36/200.74 (E(f2(a1,x221),f2(f2(x222,f2(x222,a1)),x221))), % 200.36/200.74 inference(scs_inference,[],[9,4])). % 200.36/200.74 cnf(23,plain, % 200.36/200.74 (E(f2(x231,a1),f2(x231,f2(x232,f2(x232,a1))))), % 200.36/200.74 inference(scs_inference,[],[9,4,5])). % 200.36/200.74 cnf(24,plain, % 200.36/200.74 (~E(a3,f2(f2(a3,a1),a1))), % 200.36/200.74 inference(scs_inference,[],[8,9,4,5,2])). % 200.36/200.74 cnf(25,plain, % 200.36/200.74 (~E(f2(f2(a3,a1),f2(x251,f2(x251,a1))),a3)), % 200.36/200.74 inference(scs_inference,[],[23,8,3])). % 200.36/200.74 cnf(27,plain, % 200.36/200.74 (~E(a3,f2(f2(a3,a1),f2(x271,f2(x271,a1))))), % 200.36/200.74 inference(scs_inference,[],[23,8,3,2])). % 200.36/200.74 cnf(28,plain, % 200.36/200.74 (E(a1,f2(f2(x281,f2(x281,a1)),f2(a1,a1)))), % 200.36/200.74 inference(scs_inference,[],[22,9,3])). % 200.36/200.74 cnf(31,plain, % 200.36/200.74 (E(f2(a1,x311),f2(f2(f2(x312,f2(x312,a1)),f2(a1,a1)),x311))), % 200.36/200.74 inference(scs_inference,[],[22,9,3,4])). % 200.36/200.74 cnf(32,plain, % 200.36/200.74 (E(f2(x321,a1),f2(x321,f2(f2(x322,f2(x322,a1)),f2(a1,a1))))), % 200.36/200.74 inference(scs_inference,[],[22,9,3,4,5])). % 200.36/200.74 cnf(33,plain, % 200.36/200.74 (~E(f2(f2(a3,a1),f2(f2(x331,f2(x331,a1)),f2(a1,a1))),a3)), % 200.36/200.74 inference(scs_inference,[],[32,8,3])). % 200.36/200.74 cnf(35,plain, % 200.36/200.74 (~E(a3,f2(f2(a3,a1),f2(f2(x351,f2(x351,a1)),f2(a1,a1))))), % 200.36/200.74 inference(scs_inference,[],[32,8,3,2])). % 200.36/200.74 cnf(36,plain, % 200.36/200.74 (E(f2(x361,f2(x361,a1)),f2(f2(x362,f2(x362,a1)),f2(a1,a1)))), % 200.36/200.74 inference(scs_inference,[],[28,6,3])). % 200.36/200.74 cnf(37,plain, % 200.36/200.74 (E(a1,f2(f2(f2(x371,f2(x371,a1)),f2(a1,a1)),f2(a1,a1)))), % 200.36/200.74 inference(scs_inference,[],[31,9,3])). % 200.36/200.74 cnf(40,plain, % 200.36/200.74 (E(f2(a1,x401),f2(f2(f2(f2(x402,f2(x402,a1)),f2(a1,a1)),f2(a1,a1)),x401))), % 200.36/200.74 inference(scs_inference,[],[31,9,3,4])). % 200.36/200.74 cnf(41,plain, % 200.36/200.74 (E(f2(x411,a1),f2(x411,f2(f2(f2(x412,f2(x412,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.74 inference(scs_inference,[],[31,9,3,4,5])). % 200.36/200.74 cnf(42,plain, % 200.36/200.74 (~E(f2(f2(a3,a1),f2(f2(f2(x421,f2(x421,a1)),f2(a1,a1)),f2(a1,a1))),a3)), % 200.36/200.74 inference(scs_inference,[],[41,8,3])). % 200.36/200.74 cnf(44,plain, % 200.36/200.74 (~E(a3,f2(f2(a3,a1),f2(f2(f2(x441,f2(x441,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.74 inference(scs_inference,[],[42,2])). % 200.36/200.74 cnf(45,plain, % 200.36/200.74 (E(f2(x451,f2(x451,a1)),f2(f2(f2(x452,f2(x452,a1)),f2(a1,a1)),f2(a1,a1)))), % 200.36/200.74 inference(scs_inference,[],[37,42,6,2,3])). % 200.36/200.74 cnf(46,plain, % 200.36/200.74 (E(a1,f2(f2(f2(f2(x461,f2(x461,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)))), % 200.36/200.74 inference(scs_inference,[],[40,9,3])). % 200.36/200.74 cnf(49,plain, % 200.36/200.74 (E(f2(x491,f2(x491,a1)),f2(f2(f2(f2(x492,f2(x492,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)))), % 200.36/200.74 inference(scs_inference,[],[46,6,3])). % 200.36/200.74 cnf(50,plain, % 200.36/200.74 (E(f2(a1,a1),f2(f2(x501,f2(x501,a1)),f2(x502,f2(x502,a1))))), % 200.36/200.74 inference(scs_inference,[],[23,22,3])). % 200.36/200.74 cnf(53,plain, % 200.36/200.74 (E(f2(a1,a1),f2(f2(x531,f2(x531,a1)),f2(f2(x532,f2(x532,a1)),f2(a1,a1))))), % 200.36/200.74 inference(scs_inference,[],[32,22,3])). % 200.36/200.74 cnf(56,plain, % 200.36/200.74 (E(f2(a1,a1),f2(f2(f2(x561,f2(x561,a1)),f2(a1,a1)),f2(x562,f2(x562,a1))))), % 200.36/200.74 inference(scs_inference,[],[23,31,3])). % 200.36/200.74 cnf(59,plain, % 200.36/200.74 (E(f2(f2(f2(f2(x591,f2(x591,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(x592,f2(x592,a1)))), % 200.36/200.74 inference(scs_inference,[],[49,2])). % 200.36/200.74 cnf(60,plain, % 200.36/200.74 (E(f2(f2(f2(x601,f2(x601,a1)),f2(a1,a1)),f2(x602,f2(x602,a1))),f2(a1,a1))), % 200.36/200.74 inference(scs_inference,[],[56,2])). % 200.36/200.74 cnf(61,plain, % 200.36/200.74 (E(f2(f2(x611,f2(x611,a1)),f2(a1,a1)),f2(x612,f2(x612,a1)))), % 200.36/200.74 inference(scs_inference,[],[36,2])). % 200.36/200.74 cnf(62,plain, % 200.36/200.74 (E(f2(f2(x621,f2(x621,a1)),f2(a1,a1)),a1)), % 200.36/200.74 inference(scs_inference,[],[6,61,3])). % 200.36/200.74 cnf(64,plain, % 200.36/200.74 (E(f2(f2(f2(x641,f2(x641,a1)),f2(a1,a1)),x642),f2(a1,x642))), % 200.36/200.74 inference(scs_inference,[],[62,4])). % 200.36/200.74 cnf(65,plain, % 200.36/200.74 (E(f2(x651,f2(f2(x652,f2(x652,a1)),f2(a1,a1))),f2(x651,a1))), % 200.36/200.74 inference(scs_inference,[],[62,4,5])). % 200.36/200.74 cnf(66,plain, % 200.36/200.74 (E(f2(f2(f2(x661,f2(x661,a1)),f2(a1,a1)),f2(a1,a1)),f2(x662,f2(x662,a1)))), % 200.36/200.74 inference(scs_inference,[],[45,2])). % 200.36/200.74 cnf(68,plain, % 200.36/200.74 (E(f2(f2(x681,f2(x681,a1)),f2(x682,f2(x682,a1))),f2(a1,a1))), % 200.36/200.74 inference(scs_inference,[],[50,2])). % 200.36/200.74 cnf(69,plain, % 200.36/200.74 (E(f2(f2(x691,f2(x691,a1)),f2(a1,a1)),f2(f2(f2(x692,f2(x692,a1)),f2(a1,a1)),f2(a1,a1)))), % 200.36/200.74 inference(scs_inference,[],[37,62,3])). % 200.36/200.74 cnf(70,plain, % 200.36/200.74 (E(f2(f2(f2(x701,f2(x701,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x702,f2(x702,a1)),f2(a1,a1)))), % 200.36/200.74 inference(scs_inference,[],[69,2])). % 200.36/200.74 cnf(71,plain, % 200.36/200.74 (E(f2(f2(x711,f2(x711,a1)),f2(f2(x712,f2(x712,a1)),f2(a1,a1))),f2(a1,a1))), % 200.36/200.74 inference(scs_inference,[],[53,2])). % 200.36/200.74 cnf(72,plain, % 200.36/200.74 (E(f2(f2(f2(f2(x721,f2(x721,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),a1)), % 200.36/200.74 inference(scs_inference,[],[46,2])). % 200.36/200.74 cnf(73,plain, % 200.36/200.74 (E(f2(f2(f2(f2(x731,f2(x731,a1)),f2(a1,a1)),f2(a1,a1)),x732),f2(a1,x732))), % 200.36/200.74 inference(scs_inference,[],[40,2])). % 200.36/200.74 cnf(74,plain, % 200.36/200.74 (E(f2(x741,f2(f2(f2(x742,f2(x742,a1)),f2(a1,a1)),f2(a1,a1))),f2(x741,a1))), % 200.36/200.74 inference(scs_inference,[],[41,2])). % 200.36/200.74 cnf(75,plain, % 200.36/200.74 (E(f2(f2(f2(x751,f2(x751,a1)),f2(a1,a1)),f2(a1,a1)),a1)), % 200.36/200.74 inference(scs_inference,[],[37,2])). % 200.36/200.74 cnf(76,plain, % 200.36/200.74 (E(f2(f2(x761,f2(x761,a1)),f2(f2(x762,f2(x762,a1)),f2(a1,a1))),f2(f2(x763,f2(x763,a1)),f2(x764,f2(x764,a1))))), % 200.36/200.74 inference(scs_inference,[],[71,50,3])). % 200.36/200.74 cnf(77,plain, % 200.36/200.74 (E(f2(f2(f2(x771,f2(x771,a1)),f2(f2(x772,f2(x772,a1)),f2(a1,a1))),x773),f2(f2(a1,a1),x773))), % 200.36/200.74 inference(scs_inference,[],[71,50,3,4])). % 200.36/200.74 cnf(78,plain, % 200.36/200.74 (E(f2(x781,f2(f2(x782,f2(x782,a1)),f2(f2(x783,f2(x783,a1)),f2(a1,a1)))),f2(x781,f2(a1,a1)))), % 200.36/200.74 inference(scs_inference,[],[71,50,3,4,5])). % 200.36/200.74 cnf(79,plain, % 200.36/200.74 (~E(a3,f2(f2(a1,x791),f2(f2(f2(f2(f2(a3,a1),a1),x792),f2(a1,a1)),f2(x791,x792))))), % 200.36/200.74 inference(scs_inference,[],[71,20,50,3,4,5,2])). % 200.36/200.74 cnf(80,plain, % 200.36/200.74 (E(f2(f2(a1,a1),x801),f2(f2(f2(x802,f2(x802,a1)),f2(f2(x803,f2(x803,a1)),f2(a1,a1))),x801))), % 200.36/200.74 inference(scs_inference,[],[77,2])). % 200.36/200.74 cnf(81,plain, % 200.36/200.74 (~E(f2(f2(a1,x811),f2(f2(f2(a3,x812),f2(a1,a1)),f2(x811,x812))),f2(f2(a3,a1),f2(x813,f2(x813,a1))))), % 200.36/200.74 inference(scs_inference,[],[27,77,12,2,3])). % 200.36/200.74 cnf(83,plain, % 200.36/200.75 (~E(f2(a1,f2(f2(a3,a1),f2(a1,a1))),f2(a3,a1))), % 200.36/200.75 inference(scs_inference,[],[27,77,12,2,3,4])). % 200.36/200.75 cnf(84,plain, % 200.36/200.75 (E(f2(f2(x841,f2(x841,a1)),x842),f2(f2(x843,f2(x843,a1)),x842))), % 200.36/200.75 inference(scs_inference,[],[13,4])). % 200.36/200.75 cnf(85,plain, % 200.36/200.75 (~E(f2(a3,a1),f2(a1,f2(f2(a3,a1),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[13,83,4,2])). % 200.36/200.75 cnf(86,plain, % 200.36/200.75 (E(f2(f2(x861,f2(x861,a1)),f2(f2(x862,f2(x862,a1)),f2(a1,a1))),f2(f2(x863,f2(x863,a1)),f2(f2(x864,f2(x864,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[71,13,83,53,4,2,3])). % 200.36/200.75 cnf(88,plain, % 200.36/200.75 (~E(f2(f2(a1,x881),f2(f2(f2(f2(a3,a1),x882),f2(a1,a1)),f2(x881,x882))),f2(a1,f2(f2(a3,a1),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[85,78,12,2,3])). % 200.36/200.75 cnf(90,plain, % 200.36/200.75 (~E(f2(f2(a3,a1),f2(x901,f2(x901,a1))),f2(f2(a1,x902),f2(f2(f2(a3,x903),f2(a1,a1)),f2(x902,x903))))), % 200.36/200.75 inference(scs_inference,[],[81,2])). % 200.36/200.75 cnf(91,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x911,f2(x911,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x912,f2(x912,a1)),f2(a1,a1)))), % 200.36/200.75 inference(scs_inference,[],[72,81,28,2,3])). % 200.36/200.75 cnf(92,plain, % 200.36/200.75 (E(f2(x921,f2(f2(f2(f2(x922,f2(x922,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),f2(x921,a1))), % 200.36/200.75 inference(scs_inference,[],[72,81,28,2,3,5])). % 200.36/200.75 cnf(93,plain, % 200.36/200.75 (E(f2(x931,a1),f2(x931,f2(f2(f2(f2(x932,f2(x932,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[92,2])). % 200.36/200.75 cnf(94,plain, % 200.36/200.75 (~E(f2(f2(a3,a1),f2(f2(x941,f2(x941,a1)),f2(a1,a1))),f2(f2(a1,x942),f2(f2(f2(a3,x943),f2(a1,a1)),f2(x942,x943))))), % 200.36/200.75 inference(scs_inference,[],[33,92,7,2,3])). % 200.36/200.75 cnf(96,plain, % 200.36/200.75 (E(f2(f2(f2(f2(f2(x961,f2(x961,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x962),f2(a1,x962))), % 200.36/200.75 inference(scs_inference,[],[72,4])). % 200.36/200.75 cnf(97,plain, % 200.36/200.75 (~E(f2(a1,f2(f2(a3,a1),f2(a1,a1))),f2(f2(a1,x971),f2(f2(f2(f2(a3,a1),x972),f2(a1,a1)),f2(x971,x972))))), % 200.36/200.75 inference(scs_inference,[],[72,88,4,2])). % 200.36/200.75 cnf(98,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x981,f2(x981,a1)),f2(a1,a1)),f2(a1,a1)),f2(x982,f2(x982,a1))),f2(a1,a1))), % 200.36/200.75 inference(scs_inference,[],[72,18,73,88,4,2,3])). % 200.36/200.75 cnf(101,plain, % 200.36/200.75 (E(f2(a1,a1),f2(f2(f2(f2(x1011,f2(x1011,a1)),f2(a1,a1)),f2(a1,a1)),f2(x1012,f2(x1012,a1))))), % 200.36/200.75 inference(scs_inference,[],[98,2])). % 200.36/200.75 cnf(103,plain, % 200.36/200.75 (~E(f2(f2(a1,x1031),f2(f2(f2(a3,x1032),f2(a1,a1)),f2(x1031,x1032))),f2(f2(a3,a1),f2(f2(x1033,f2(x1033,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[94,2])). % 200.36/200.75 cnf(104,plain, % 200.36/200.75 (~E(f2(f2(a3,a1),f2(x1041,f2(x1041,a1))),f2(f2(x1042,f2(x1042,a1)),f2(f2(f2(a3,x1043),f2(a1,a1)),f2(f2(a1,a1),x1043))))), % 200.36/200.75 inference(scs_inference,[],[84,90,94,2,3])). % 200.36/200.75 cnf(107,plain, % 200.36/200.75 (E(f2(x1071,f2(f2(x1072,f2(x1072,a1)),x1073)),f2(x1071,f2(a1,x1073)))), % 200.36/200.75 inference(scs_inference,[],[17,84,90,94,2,3,5])). % 200.36/200.75 cnf(108,plain, % 200.36/200.75 (E(f2(a1,x1081),f2(f2(f2(f2(f2(x1082,f2(x1082,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x1081))), % 200.36/200.75 inference(scs_inference,[],[96,2])). % 200.36/200.75 cnf(109,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x1091,f2(x1091,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x1092,f2(x1092,a1)),a1)),a1)), % 200.36/200.75 inference(scs_inference,[],[72,96,107,2,3])). % 200.36/200.75 cnf(111,plain, % 200.36/200.75 (~E(f2(f2(x1111,f2(x1111,a1)),f2(f2(f2(a3,x1112),f2(a1,a1)),f2(f2(a1,a1),x1112))),f2(f2(a3,a1),f2(x1113,f2(x1113,a1))))), % 200.36/200.75 inference(scs_inference,[],[104,2])). % 200.36/200.75 cnf(112,plain, % 200.36/200.75 (E(f2(f2(x1121,f2(x1121,a1)),f2(x1122,f2(x1122,a1))),f2(f2(f2(f2(x1123,f2(x1123,a1)),f2(a1,a1)),f2(a1,a1)),f2(x1124,f2(x1124,a1))))), % 200.36/200.75 inference(scs_inference,[],[68,101,104,2,3])). % 200.36/200.75 cnf(113,plain, % 200.36/200.75 (E(f2(f2(f2(x1131,f2(x1131,a1)),f2(x1132,f2(x1132,a1))),x1133),f2(f2(a1,a1),x1133))), % 200.36/200.75 inference(scs_inference,[],[68,101,104,2,3,4])). % 200.36/200.75 cnf(114,plain, % 200.36/200.75 (E(f2(f2(x1141,f2(x1141,a1)),f2(a1,a1)),f2(f2(f2(f2(x1142,f2(x1142,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)))), % 200.36/200.75 inference(scs_inference,[],[91,2])). % 200.36/200.75 cnf(115,plain, % 200.36/200.75 (~E(a3,f2(f2(f2(x1151,f2(x1151,a1)),f2(x1152,f2(x1152,a1))),f2(f2(f2(f2(f2(a3,a1),a1),x1153),f2(a1,a1)),f2(a1,x1153))))), % 200.36/200.75 inference(scs_inference,[],[91,79,113,2,3])). % 200.36/200.75 cnf(119,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x1191,f2(x1191,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x1192,f2(x1192,a1)),f2(a1,a1))),f2(a1,a1))), % 200.36/200.75 inference(scs_inference,[],[73,65,115,2,3])). % 200.36/200.75 cnf(120,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x1201,f2(x1201,a1)),f2(a1,a1)),f2(a1,a1)),x1202),f2(a1,x1202))), % 200.36/200.75 inference(rename_variables,[],[73])). % 200.36/200.75 cnf(122,plain, % 200.36/200.75 (E(f2(x1221,f2(f2(f2(f2(x1222,f2(x1222,a1)),f2(a1,a1)),f2(a1,a1)),x1223)),f2(x1221,f2(a1,x1223)))), % 200.36/200.75 inference(scs_inference,[],[73,120,65,115,2,3,5])). % 200.36/200.75 cnf(123,plain, % 200.36/200.75 (E(f2(a1,a1),f2(f2(f2(f2(x1231,f2(x1231,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x1232,f2(x1232,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[119,2])). % 200.36/200.75 cnf(124,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x1241,f2(x1241,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(x1242,f2(x1242,a1)),f2(a1,a1)),f2(a1,a1))),f2(a1,a1))), % 200.36/200.75 inference(scs_inference,[],[73,74,119,2,3])). % 200.36/200.75 cnf(127,plain, % 200.36/200.75 (~E(f2(a1,f2(f2(a3,a1),f2(a1,a1))),f2(f2(x1271,f2(x1271,a1)),f2(f2(f2(f2(a3,a1),x1272),f2(a1,a1)),f2(f2(a1,a1),x1272))))), % 200.36/200.75 inference(scs_inference,[],[97,84,3])). % 200.36/200.75 cnf(130,plain, % 200.36/200.75 (E(f2(f2(f2(f2(f2(x1301,f2(x1301,a1)),f2(a1,a1)),f2(a1,a1)),x1302),x1303),f2(f2(a1,x1302),x1303))), % 200.36/200.75 inference(scs_inference,[],[73,97,84,3,4])). % 200.36/200.75 cnf(131,plain, % 200.36/200.75 (E(f2(a1,a1),f2(f2(f2(f2(x1311,f2(x1311,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(x1312,f2(x1312,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[73,124,97,84,3,4,2])). % 200.36/200.75 cnf(133,plain, % 200.36/200.75 (E(f2(f2(f2(x1331,f2(x1331,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,f2(f2(f2(f2(x1332,f2(x1332,a1)),f2(a1,a1)),f2(a1,a1)),a1)))), % 200.36/200.75 inference(scs_inference,[],[73,66,127,2,3])). % 200.36/200.75 cnf(136,plain, % 200.36/200.75 (E(f2(x1361,f2(a1,x1362)),f2(x1361,f2(f2(f2(f2(x1363,f2(x1363,a1)),f2(a1,a1)),f2(a1,a1)),x1362)))), % 200.36/200.75 inference(scs_inference,[],[122,2])). % 200.36/200.75 cnf(137,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x1371,f2(x1371,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a1,x1372),f2(f2(f2(a1,x1373),f2(a1,a1)),f2(x1372,x1373))))), % 200.36/200.75 inference(scs_inference,[],[73,16,122,2,3])). % 200.36/200.75 cnf(140,plain, % 200.36/200.75 (E(f2(x1401,f2(f2(f2(x1402,f2(x1402,a1)),f2(a1,a1)),x1403)),f2(x1401,f2(a1,x1403)))), % 200.36/200.75 inference(scs_inference,[],[73,64,16,122,2,3,5])). % 200.36/200.75 cnf(141,plain, % 200.36/200.75 (~E(f2(f2(x1411,f2(x1411,a1)),f2(f2(f2(a3,x1412),f2(a1,a1)),f2(f2(a1,a1),x1412))),f2(f2(a3,a1),f2(f2(f2(x1413,f2(x1413,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[140,111,3])). % 200.36/200.75 cnf(144,plain, % 200.36/200.75 (~E(f2(f2(a3,a1),f2(f2(f2(x1441,f2(x1441,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(x1442,f2(x1442,a1)),f2(f2(f2(a3,x1443),f2(a1,a1)),f2(f2(a1,a1),x1443))))), % 200.36/200.75 inference(scs_inference,[],[141,2])). % 200.36/200.75 cnf(145,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x1451,f2(x1451,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,f2(f2(f2(f2(x1452,f2(x1452,a1)),f2(a1,a1)),f2(a1,a1)),a1)))), % 200.36/200.75 inference(scs_inference,[],[73,59,141,2,3])). % 200.36/200.75 cnf(148,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x1481,f2(x1481,a1)),f2(a1,a1)),f2(x1482,f2(x1482,a1))),x1483),f2(f2(a1,a1),x1483))), % 200.36/200.75 inference(scs_inference,[],[73,60,59,141,2,3,4])). % 200.36/200.75 cnf(150,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x1501,f2(x1501,a1)),f2(a1,a1)),f2(a1,a1)),a1),f2(a1,f2(f2(f2(f2(x1502,f2(x1502,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[73,93,137,2,3])). % 200.36/200.75 cnf(153,plain, % 200.36/200.75 (~E(f2(a1,f2(f2(a3,a1),f2(a1,a1))),f2(a3,f2(x1531,f2(x1531,a1))))), % 200.36/200.75 inference(scs_inference,[],[83,18,3])). % 200.36/200.75 cnf(155,plain, % 200.36/200.75 (E(f2(x1551,f2(f2(f2(x1552,f2(x1552,a1)),f2(a1,a1)),f2(a1,a1))),f2(x1551,f2(f2(x1553,f2(x1553,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[70,83,18,3,5])). % 200.36/200.75 cnf(156,plain, % 200.36/200.75 (~E(f2(a3,f2(x1561,f2(x1561,a1))),f2(a1,f2(f2(a3,a1),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[70,83,18,3,5,2])). % 200.36/200.75 cnf(161,plain, % 200.36/200.75 (~E(f2(f2(a3,a1),a1),f2(f2(x1611,f2(x1611,a1)),f2(f2(f2(a3,x1612),f2(a1,a1)),f2(f2(a1,a1),x1612))))), % 200.36/200.75 inference(scs_inference,[],[74,144,3])). % 200.36/200.75 cnf(162,plain, % 200.36/200.75 (E(f2(x1621,f2(f2(f2(x1622,f2(x1622,a1)),f2(a1,a1)),f2(a1,a1))),f2(x1621,a1))), % 200.36/200.75 inference(rename_variables,[],[74])). % 200.36/200.75 cnf(163,plain, % 200.36/200.75 (E(f2(f2(x1631,f2(f2(f2(x1632,f2(x1632,a1)),f2(a1,a1)),f2(a1,a1))),x1633),f2(f2(x1631,a1),x1633))), % 200.36/200.75 inference(scs_inference,[],[74,162,144,3,4])). % 200.36/200.75 cnf(164,plain, % 200.36/200.75 (~E(f2(f2(x1641,f2(x1641,a1)),f2(f2(f2(a3,x1642),f2(a1,a1)),f2(f2(a1,a1),x1642))),f2(f2(a3,a1),a1))), % 200.36/200.75 inference(scs_inference,[],[74,162,144,3,4,2])). % 200.36/200.75 cnf(165,plain, % 200.36/200.75 (E(f2(f2(a1,x1651),x1652),f2(f2(f2(f2(f2(x1653,f2(x1653,a1)),f2(a1,a1)),f2(a1,a1)),x1651),x1652))), % 200.36/200.75 inference(scs_inference,[],[130,2])). % 200.36/200.75 cnf(166,plain, % 200.36/200.75 (~E(a3,f2(f2(a3,f2(f2(f2(x1661,f2(x1661,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(x1662,f2(x1662,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[35,130,163,2,3])). % 200.36/200.75 cnf(168,plain, % 200.36/200.75 (~E(f2(f2(a3,f2(f2(f2(x1681,f2(x1681,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(x1682,f2(x1682,a1)),f2(a1,a1))),a3)), % 200.36/200.75 inference(scs_inference,[],[166,2])). % 200.36/200.75 cnf(169,plain, % 200.36/200.75 (E(f2(a1,f2(f2(f2(x1691,f2(x1691,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(f2(f2(f2(x1692,f2(x1692,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),a1))), % 200.36/200.75 inference(scs_inference,[],[74,108,166,2,3])). % 200.36/200.75 cnf(170,plain, % 200.36/200.75 (E(f2(x1701,f2(f2(f2(x1702,f2(x1702,a1)),f2(a1,a1)),f2(a1,a1))),f2(x1701,a1))), % 200.36/200.75 inference(rename_variables,[],[74])). % 200.36/200.75 cnf(172,plain, % 200.36/200.75 (E(f2(x1721,f2(x1722,f2(f2(f2(x1723,f2(x1723,a1)),f2(a1,a1)),f2(a1,a1)))),f2(x1721,f2(x1722,a1)))), % 200.36/200.75 inference(scs_inference,[],[74,170,108,166,2,3,5])). % 200.36/200.75 cnf(173,plain, % 200.36/200.75 (E(f2(x1731,f2(x1732,a1)),f2(x1731,f2(x1732,f2(f2(f2(x1733,f2(x1733,a1)),f2(a1,a1)),f2(a1,a1)))))), % 200.36/200.75 inference(scs_inference,[],[172,2])). % 200.36/200.75 cnf(174,plain, % 200.36/200.75 (~E(f2(f2(a1,f2(f2(x1741,f2(x1741,a1)),f2(a1,a1))),f2(f2(f2(a3,f2(a1,a1)),f2(a1,a1)),a1)),f2(f2(a3,a1),a1))), % 200.36/200.75 inference(scs_inference,[],[19,172,2,3])). % 200.36/200.75 cnf(178,plain, % 200.36/200.75 (~E(a3,f2(f2(a3,f2(f2(f2(x1781,f2(x1781,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(f2(x1782,f2(x1782,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[44,174,163,2,3])). % 200.36/200.75 cnf(180,plain, % 200.36/200.75 (E(f2(f2(f2(x1801,f2(x1801,a1)),f2(a1,a1)),x1802),f2(f2(f2(f2(f2(x1803,f2(x1803,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x1802))), % 200.36/200.75 inference(scs_inference,[],[44,114,174,163,2,3,4])). % 200.36/200.75 cnf(181,plain, % 200.36/200.75 (E(f2(x1811,f2(f2(x1812,f2(x1812,a1)),f2(a1,a1))),f2(x1811,f2(f2(f2(x1813,f2(x1813,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[155,2])). % 200.36/200.75 cnf(182,plain, % 200.36/200.75 (E(f2(a1,f2(f2(f2(x1821,f2(x1821,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(f2(f2(x1822,f2(x1822,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x1823,f2(x1823,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[74,123,155,2,3])). % 200.36/200.75 cnf(184,plain, % 200.36/200.75 (~E(f2(f2(a3,f2(f2(f2(x1841,f2(x1841,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(f2(x1842,f2(x1842,a1)),f2(a1,a1)),f2(a1,a1))),a3)), % 200.36/200.75 inference(scs_inference,[],[178,2])). % 200.36/200.75 cnf(185,plain, % 200.36/200.75 (E(f2(f2(x1851,f2(x1851,a1)),f2(f2(x1852,f2(x1852,a1)),f2(a1,a1))),f2(f2(x1853,f2(x1853,a1)),f2(f2(f2(f2(x1854,f2(x1854,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[76,136,178,2,3])). % 200.36/200.75 cnf(189,plain, % 200.36/200.75 (E(a1,f2(f2(f2(f2(x1891,f2(x1891,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x1892,f2(x1892,a1)),a1)))), % 200.36/200.75 inference(scs_inference,[],[109,2])). % 200.36/200.75 cnf(190,plain, % 200.36/200.75 (~E(f2(a1,f2(f2(a3,a1),f2(a1,a1))),f2(a3,f2(f2(x1901,f2(x1901,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[153,109,107,2,3])). % 200.36/200.75 cnf(193,plain, % 200.36/200.75 (~E(f2(a3,f2(f2(x1931,f2(x1931,a1)),f2(a1,a1))),f2(a1,f2(f2(a3,a1),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[190,2])). % 200.36/200.75 cnf(194,plain, % 200.36/200.75 (E(f2(a1,f2(f2(f2(x1941,f2(x1941,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(f2(f2(x1942,f2(x1942,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(x1943,f2(x1943,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[74,190,131,2,3])). % 200.36/200.75 cnf(197,plain, % 200.36/200.75 (E(f2(f2(f2(f2(f2(x1971,f2(x1971,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x1972),f2(f2(f2(x1973,f2(x1973,a1)),f2(a1,a1)),x1972))), % 200.36/200.75 inference(scs_inference,[],[180,2])). % 200.36/200.75 cnf(198,plain, % 200.36/200.75 (~E(f2(f2(a3,f2(f2(f2(x1981,f2(x1981,a1)),f2(a1,a1)),f2(a1,a1))),a1),a3)), % 200.36/200.75 inference(scs_inference,[],[74,180,184,2,3])). % 200.36/200.75 cnf(200,plain, % 200.36/200.75 (~E(a3,f2(f2(a3,f2(f2(f2(x2001,f2(x2001,a1)),f2(a1,a1)),f2(a1,a1))),a1))), % 200.36/200.75 inference(scs_inference,[],[198,2])). % 200.36/200.75 cnf(201,plain, % 200.36/200.75 (~E(f2(a3,f2(x2011,f2(x2011,a1))),f2(f2(x2012,f2(x2012,a1)),f2(f2(a3,a1),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[156,198,17,2,3])). % 200.36/200.75 cnf(205,plain, % 200.36/200.75 (E(f2(f2(f2(f2(f2(x2051,f2(x2051,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),a1)), % 200.36/200.75 inference(scs_inference,[],[75,197,112,2,3])). % 200.36/200.75 cnf(208,plain, % 200.36/200.75 (~E(f2(f2(x2081,f2(x2081,a1)),f2(f2(a3,a1),f2(a1,a1))),f2(a3,f2(x2082,f2(x2082,a1))))), % 200.36/200.75 inference(scs_inference,[],[201,2])). % 200.36/200.75 cnf(209,plain, % 200.36/200.75 (E(f2(f2(f2(x2091,f2(x2091,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(f2(x2092,f2(x2092,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x2093,f2(x2093,a1)),a1)))), % 200.36/200.75 inference(scs_inference,[],[75,201,189,2,3])). % 200.36/200.75 cnf(210,plain, % 200.36/200.75 (E(f2(f2(f2(f2(f2(f2(x2101,f2(x2101,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x2102),f2(a1,x2102))), % 200.36/200.75 inference(scs_inference,[],[75,205,201,189,2,3,4])). % 200.36/200.75 cnf(211,plain, % 200.36/200.75 (E(f2(a1,x2111),f2(f2(f2(f2(f2(f2(x2112,f2(x2112,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x2111))), % 200.36/200.75 inference(scs_inference,[],[210,2])). % 200.36/200.75 cnf(212,plain, % 200.36/200.75 (~E(f2(a3,f2(f2(x2121,f2(x2121,a1)),f2(a1,a1))),f2(f2(f2(f2(f2(f2(x2122,f2(x2122,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a3,a1),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[210,193,2,3])). % 200.36/200.75 cnf(216,plain, % 200.36/200.75 (E(f2(a1,x2161),f2(f2(f2(f2(f2(f2(x2162,f2(x2162,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x2161))), % 200.36/200.75 inference(rename_variables,[],[211])). % 200.36/200.75 cnf(218,plain, % 200.36/200.75 (E(f2(x2181,f2(a1,x2182)),f2(x2181,f2(f2(f2(f2(f2(f2(x2183,f2(x2183,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x2182)))), % 200.36/200.75 inference(scs_inference,[],[211,216,181,212,2,3,5])). % 200.36/200.75 cnf(220,plain, % 200.36/200.75 (~E(f2(f2(f2(x2201,f2(x2201,a1)),f2(f2(x2202,f2(x2202,a1)),f2(a1,a1))),f2(f2(f2(a3,x2203),f2(a1,a1)),f2(a1,x2203))),f2(f2(a3,a1),f2(f2(x2204,f2(x2204,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[103,80,150,2,3])). % 200.36/200.75 cnf(226,plain, % 200.36/200.75 (E(f2(f2(x2261,f2(x2261,a1)),x2262),f2(f2(f2(x2263,f2(x2263,a1)),f2(a1,a1)),x2262))), % 200.36/200.75 inference(scs_inference,[],[164,220,36,65,2,3,4])). % 200.36/200.75 cnf(228,plain, % 200.36/200.75 (E(f2(f2(x2281,f2(x2281,a1)),f2(f2(x2282,f2(x2282,a1)),f2(a1,a1))),f2(f2(f2(x2283,f2(x2283,a1)),f2(a1,a1)),f2(x2284,f2(x2284,a1))))), % 200.36/200.75 inference(scs_inference,[],[76,226,2,3])). % 200.36/200.75 cnf(234,plain, % 200.36/200.75 (E(f2(f2(f2(x2341,f2(x2341,a1)),f2(a1,a1)),f2(x2342,f2(x2342,a1))),f2(f2(x2343,f2(x2343,a1)),f2(f2(x2344,f2(x2344,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[228,2])). % 200.36/200.75 cnf(235,plain, % 200.36/200.75 (~E(a3,f2(f2(a3,a1),f2(f2(f2(f2(x2351,f2(x2351,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[24,228,92,2,3])). % 200.36/200.75 cnf(237,plain, % 200.36/200.75 (~E(f2(f2(a3,a1),f2(f2(f2(f2(x2371,f2(x2371,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),a3)), % 200.36/200.75 inference(scs_inference,[],[235,2])). % 200.36/200.75 cnf(242,plain, % 200.36/200.75 (E(f2(f2(f2(f2(f2(x2421,f2(x2421,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),a1),f2(a1,f2(f2(f2(x2422,f2(x2422,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[169,2])). % 200.36/200.75 cnf(243,plain, % 200.36/200.75 (~E(f2(f2(f2(f2(f2(x2431,f2(x2431,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a3,a1),f2(a1,a1))),f2(a3,f2(x2432,f2(x2432,a1))))), % 200.36/200.75 inference(scs_inference,[],[208,165,169,2,3])). % 200.36/200.75 cnf(247,plain, % 200.36/200.75 (~E(f2(f2(a3,a1),f2(f2(f2(f2(x2471,f2(x2471,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(a1,x2472),f2(f2(f2(a3,x2473),f2(a1,a1)),f2(x2472,x2473))))), % 200.36/200.75 inference(scs_inference,[],[237,243,7,2,3])). % 200.36/200.75 cnf(250,plain, % 200.36/200.75 (E(f2(x2501,f2(f2(f2(f2(f2(f2(x2502,f2(x2502,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x2503)),f2(x2501,f2(a1,x2503)))), % 200.36/200.75 inference(scs_inference,[],[218,2])). % 200.36/200.75 cnf(251,plain, % 200.36/200.75 (E(f2(f2(f2(x2511,f2(x2511,a1)),f2(f2(x2512,f2(x2512,a1)),f2(a1,a1))),f2(x2513,a1)),f2(f2(a1,a1),f2(x2513,f2(f2(f2(x2514,f2(x2514,a1)),f2(a1,a1)),f2(a1,a1)))))), % 200.36/200.75 inference(scs_inference,[],[77,173,218,2,3])). % 200.36/200.75 cnf(254,plain, % 200.36/200.75 (~E(f2(f2(a1,x2541),f2(f2(f2(a3,x2542),f2(a1,a1)),f2(x2541,x2542))),f2(f2(a3,a1),f2(f2(f2(f2(x2543,f2(x2543,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[247,2])). % 200.36/200.75 cnf(255,plain, % 200.36/200.75 (~E(f2(f2(a3,a1),f2(a1,f2(f2(f2(f2(f2(f2(x2551,f2(x2551,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),a1))),a3)), % 200.36/200.75 inference(scs_inference,[],[25,247,250,2,3])). % 200.36/200.75 cnf(258,plain, % 200.36/200.75 (E(f2(f2(f2(x2581,f2(x2581,a1)),f2(a1,a1)),x2582),f2(f2(x2583,f2(x2583,a1)),x2582))), % 200.36/200.75 inference(scs_inference,[],[25,247,250,61,2,3,4])). % 200.36/200.75 cnf(259,plain, % 200.36/200.75 (E(f2(a1,f2(f2(f2(f2(x2591,f2(x2591,a1)),f2(a1,a1)),f2(a1,a1)),a1)),f2(f2(f2(x2592,f2(x2592,a1)),f2(a1,a1)),f2(a1,a1)))), % 200.36/200.75 inference(scs_inference,[],[133,2])). % 200.36/200.75 cnf(260,plain, % 200.36/200.75 (~E(a3,f2(f2(a3,f2(f2(f2(x2601,f2(x2601,a1)),f2(a1,a1)),f2(a1,a1))),f2(x2602,f2(x2602,a1))))), % 200.36/200.75 inference(scs_inference,[],[200,133,18,2,3])). % 200.36/200.75 cnf(262,plain, % 200.36/200.75 (~E(f2(f2(a3,f2(f2(f2(x2621,f2(x2621,a1)),f2(a1,a1)),f2(a1,a1))),f2(x2622,f2(x2622,a1))),a3)), % 200.36/200.75 inference(scs_inference,[],[260,2])). % 200.36/200.75 cnf(263,plain, % 200.36/200.75 (E(f2(f2(f2(x2631,f2(x2631,a1)),f2(a1,a1)),f2(f2(x2632,f2(x2632,a1)),f2(f2(x2633,f2(x2633,a1)),f2(a1,a1)))),f2(f2(x2634,f2(x2634,a1)),f2(a1,a1)))), % 200.36/200.75 inference(scs_inference,[],[78,258,260,2,3])). % 200.36/200.75 cnf(268,plain, % 200.36/200.75 (E(f2(f2(f2(f2(f2(x2681,f2(x2681,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),a1),f2(f2(f2(f2(x2682,f2(x2682,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x2683,f2(x2683,a1)),f2(a1,a1))))), % 200.36/200.75 inference(scs_inference,[],[242,263,182,2,3])). % 200.36/200.75 cnf(273,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x2731,f2(x2731,a1)),f2(a1,a1)),x2732),x2733),f2(f2(a1,x2732),x2733))), % 200.36/200.75 inference(scs_inference,[],[262,255,64,7,2,3,4])). % 200.36/200.75 cnf(284,plain, % 200.36/200.75 (~E(f2(f2(a3,f2(f2(f2(x2841,f2(x2841,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(x2842,f2(x2842,a1)),f2(a1,a1))),f2(f2(a1,x2843),f2(f2(f2(a3,x2844),f2(a1,a1)),f2(x2843,x2844))))), % 200.36/200.75 inference(scs_inference,[],[168,185,7,2,3])). % 200.36/200.75 cnf(287,plain, % 200.36/200.75 (E(f2(f2(f2(f2(x2871,f2(x2871,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(x2872,f2(x2872,a1)),f2(a1,a1)),f2(a1,a1)))), % 200.36/200.75 inference(scs_inference,[],[259,145,284,2,3])). % 200.36/200.75 cnf(289,plain, % 200.36/200.75 (E(f2(f2(x2891,f2(x2891,a1)),x2892),f2(f2(f2(f2(x2893,f2(x2893,a1)),f2(a1,a1)),f2(a1,a1)),x2892))), % 200.36/200.75 inference(scs_inference,[],[259,145,284,45,2,3,4])). % 200.36/200.75 cnf(290,plain, % 200.36/200.75 (E(f2(f2(f2(x2901,f2(x2901,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(f2(x2902,f2(x2902,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)))), % 200.36/200.75 inference(scs_inference,[],[287,2])). % 200.36/200.75 cnf(291,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x2911,f2(x2911,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(f2(x2912,f2(x2912,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x2913,f2(x2913,a1)),a1)))), % 200.36/200.76 inference(scs_inference,[],[287,209,2,3])). % 200.36/200.76 cnf(293,plain, % 200.36/200.76 (~E(f2(f2(a3,a1),a1),f2(f2(f2(x2931,f2(x2931,a1)),f2(a1,a1)),f2(f2(f2(a3,x2932),f2(a1,a1)),f2(f2(a1,a1),x2932))))), % 200.36/200.76 inference(scs_inference,[],[161,258,3])). % 200.36/200.76 cnf(296,plain, % 200.36/200.76 (E(f2(x2961,f2(f2(f2(x2962,f2(x2962,a1)),f2(a1,a1)),f2(a1,a1))),f2(x2961,f2(f2(f2(f2(x2963,f2(x2963,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[290,161,258,3,5])). % 200.36/200.76 cnf(297,plain, % 200.36/200.76 (~E(f2(f2(f2(x2971,f2(x2971,a1)),f2(a1,a1)),f2(f2(f2(a3,x2972),f2(a1,a1)),f2(f2(a1,a1),x2972))),f2(f2(a3,a1),a1))), % 200.36/200.76 inference(scs_inference,[],[293,2])). % 200.36/200.76 cnf(298,plain, % 200.36/200.76 (E(f2(f2(x2981,f2(x2981,a1)),f2(f2(x2982,f2(x2982,a1)),f2(a1,a1))),f2(f2(f2(f2(x2983,f2(x2983,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x2984,f2(x2984,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[289,86,293,2,3])). % 200.36/200.76 cnf(300,plain, % 200.36/200.76 (E(f2(x3001,f2(f2(f2(f2(x3002,f2(x3002,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),f2(x3001,f2(f2(f2(x3003,f2(x3003,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[296,2])). % 200.36/200.76 cnf(301,plain, % 200.36/200.76 (E(f2(f2(f2(x3011,f2(x3011,a1)),f2(a1,a1)),f2(x3012,f2(x3012,a1))),f2(f2(f2(f2(x3013,f2(x3013,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x3014,f2(x3014,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[234,296,298,2,3])). % 200.36/200.76 cnf(303,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x3031,f2(x3031,a1)),f2(a1,a1)),f2(a1,a1)),x3032),f2(f2(x3033,f2(x3033,a1)),x3032))), % 200.36/200.76 inference(scs_inference,[],[234,296,298,66,2,3,4])). % 200.36/200.76 cnf(304,plain, % 200.36/200.76 (~E(a3,f2(f2(f2(f2(x3041,f2(x3041,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(f2(f2(a3,a1),a1),x3042),f2(a1,a1)),f2(f2(a1,a1),x3042))))), % 200.36/200.76 inference(scs_inference,[],[79,303,3])). % 200.36/200.76 cnf(307,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x3071,f2(x3071,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x3072,f2(x3072,a1)),f2(a1,a1))),f2(f2(f2(x3073,f2(x3073,a1)),f2(a1,a1)),f2(x3074,f2(x3074,a1))))), % 200.36/200.76 inference(scs_inference,[],[79,303,301,3,2])). % 200.36/200.76 cnf(309,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x3091,f2(x3091,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),a1),f2(f2(f2(x3092,f2(x3092,a1)),f2(a1,a1)),f2(x3093,f2(x3093,a1))))), % 200.36/200.76 inference(scs_inference,[],[307,268,304,2,3])). % 200.36/200.76 cnf(311,plain, % 200.36/200.76 (E(f2(x3111,f2(f2(f2(x3112,f2(x3112,a1)),f2(a1,a1)),f2(x3113,f2(x3113,a1)))),f2(x3111,f2(a1,a1)))), % 200.36/200.76 inference(scs_inference,[],[307,268,304,60,2,3,5])). % 200.36/200.76 cnf(312,plain, % 200.36/200.76 (E(f2(x3121,f2(a1,a1)),f2(x3121,f2(f2(f2(x3122,f2(x3122,a1)),f2(a1,a1)),f2(x3123,f2(x3123,a1)))))), % 200.36/200.76 inference(scs_inference,[],[311,2])). % 200.36/200.76 cnf(313,plain, % 200.36/200.76 (~E(f2(f2(a1,a3),f2(a1,a1)),f2(f2(a3,a1),f2(f2(f2(f2(x3131,f2(x3131,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[311,254,2,3])). % 200.36/200.76 cnf(316,plain, % 200.36/200.76 (~E(f2(f2(a3,a1),f2(f2(f2(f2(x3161,f2(x3161,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(a1,a3),f2(a1,a1)))), % 200.36/200.76 inference(scs_inference,[],[313,2])). % 200.36/200.76 cnf(317,plain, % 200.36/200.76 (~E(a3,f2(f2(a1,f2(f2(a3,a1),a1)),f2(a1,a1)))), % 200.36/200.76 inference(scs_inference,[],[79,313,312,2,3])). % 200.36/200.76 cnf(320,plain, % 200.36/200.76 (E(f2(f2(x3201,f2(x3201,a1)),x3202),f2(f2(f2(f2(f2(x3203,f2(x3203,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x3202))), % 200.36/200.76 inference(scs_inference,[],[79,313,312,49,2,3,4])). % 200.36/200.76 cnf(321,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x3211,f2(x3211,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),x3212),f2(f2(x3213,f2(x3213,a1)),x3212))), % 200.36/200.76 inference(scs_inference,[],[320,2])). % 200.36/200.76 cnf(324,plain, % 200.36/200.76 (~E(f2(f2(a1,f2(f2(a3,a1),a1)),f2(a1,a1)),a3)), % 200.36/200.76 inference(scs_inference,[],[317,2])). % 200.36/200.76 cnf(325,plain, % 200.36/200.76 (~E(f2(f2(a3,a1),f2(f2(f2(x3251,f2(x3251,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(a1,a3),f2(a1,a1)))), % 200.36/200.76 inference(scs_inference,[],[317,316,300,2,3])). % 200.36/200.76 cnf(327,plain, % 200.36/200.76 (E(f2(x3271,f2(f2(f2(f2(x3272,f2(x3272,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),f2(x3271,f2(x3273,f2(x3273,a1))))), % 200.36/200.76 inference(scs_inference,[],[317,316,300,59,2,3,5])). % 200.36/200.76 cnf(328,plain, % 200.36/200.76 (E(f2(x3281,f2(x3282,f2(x3282,a1))),f2(x3281,f2(f2(f2(f2(x3283,f2(x3283,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[327,2])). % 200.36/200.76 cnf(329,plain, % 200.36/200.76 (~E(a3,f2(f2(f2(f2(f2(x3291,f2(x3291,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(f2(f2(a3,a1),a1),x3292),f2(a1,a1)),f2(f2(a1,a1),x3292))))), % 200.36/200.76 inference(scs_inference,[],[79,321,327,2,3])). % 200.36/200.76 cnf(332,plain, % 200.36/200.76 (~E(f2(f2(a1,a3),f2(a1,a1)),f2(f2(a3,a1),f2(f2(f2(x3321,f2(x3321,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[325,2])). % 200.36/200.76 cnf(333,plain, % 200.36/200.76 (E(f2(f2(a1,a1),f2(x3331,f2(x3331,a1))),f2(f2(f2(x3332,f2(x3332,a1)),f2(f2(x3333,f2(x3333,a1)),f2(a1,a1))),f2(f2(f2(f2(x3334,f2(x3334,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[80,325,328,2,3])). % 200.36/200.76 cnf(336,plain, % 200.36/200.76 (E(f2(f2(f2(a1,x3361),f2(f2(f2(a1,x3362),f2(a1,a1)),f2(x3361,x3362))),x3363),f2(f2(x3364,f2(x3364,a1)),x3363))), % 200.36/200.76 inference(scs_inference,[],[80,325,328,14,2,3,4])). % 200.36/200.76 cnf(342,plain, % 200.36/200.76 (~E(f2(f2(a1,f2(f2(a3,a1),a1)),f2(a1,a1)),f2(f2(a1,x3421),f2(f2(f2(a3,x3422),f2(a1,a1)),f2(x3421,x3422))))), % 200.36/200.76 inference(scs_inference,[],[324,329,7,2,3])). % 200.36/200.76 cnf(344,plain, % 200.36/200.76 (E(f2(x3441,f2(f2(f2(f2(f2(x3442,f2(x3442,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),f2(x3441,a1))), % 200.36/200.76 inference(scs_inference,[],[324,329,205,7,2,3,5])). % 200.36/200.76 cnf(345,plain, % 200.36/200.76 (E(f2(x3451,a1),f2(x3451,f2(f2(f2(f2(f2(x3452,f2(x3452,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[344,2])). % 200.36/200.76 cnf(346,plain, % 200.36/200.76 (~E(f2(a1,a1),f2(f2(f2(a3,x3461),f2(a1,a1)),f2(f2(f2(a3,a1),a1),x3461)))), % 200.36/200.76 inference(scs_inference,[],[344,342,2,5])). % 200.36/200.76 cnf(350,plain, % 200.36/200.76 (~E(f2(f2(f2(a3,x3501),f2(a1,a1)),f2(f2(f2(a3,a1),a1),x3501)),f2(a1,a1))), % 200.36/200.76 inference(scs_inference,[],[346,2])). % 200.36/200.76 cnf(351,plain, % 200.36/200.76 (E(f2(x3511,f2(x3512,a1)),f2(x3511,f2(x3512,f2(f2(f2(f2(f2(x3513,f2(x3513,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)))))), % 200.36/200.76 inference(scs_inference,[],[345,346,2,5])). % 200.36/200.76 cnf(353,plain, % 200.36/200.76 (E(f2(x3531,a1),f2(x3531,f2(f2(f2(f2(f2(x3532,f2(x3532,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.76 inference(rename_variables,[],[345])). % 200.36/200.76 cnf(354,plain, % 200.36/200.76 (E(f2(f2(x3541,a1),x3542),f2(f2(x3541,f2(f2(f2(f2(f2(x3543,f2(x3543,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),x3542))), % 200.36/200.76 inference(scs_inference,[],[345,353,346,2,5,3,4])). % 200.36/200.76 cnf(356,plain, % 200.36/200.76 (~E(f2(f2(a1,a3),f2(a1,a1)),f2(f2(a3,a1),f2(f2(x3561,f2(x3561,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[332,309,181,2,3])). % 200.36/200.76 cnf(359,plain, % 200.36/200.76 (~E(f2(f2(a3,a1),f2(f2(x3591,f2(x3591,a1)),f2(a1,a1))),f2(f2(a1,a3),f2(a1,a1)))), % 200.36/200.76 inference(scs_inference,[],[356,2])). % 200.36/200.76 cnf(362,plain, % 200.36/200.76 (E(f2(x3621,f2(x3622,f2(f2(f2(f2(f2(x3623,f2(x3623,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)))),f2(x3621,f2(x3622,a1)))), % 200.36/200.76 inference(scs_inference,[],[351,2])). % 200.36/200.76 cnf(363,plain, % 200.36/200.76 (~E(f2(f2(f2(a3,a1),f2(a1,a1)),f2(f2(f2(a3,a1),a1),f2(f2(f2(f2(f2(x3631,f2(x3631,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)))),f2(a1,a1))), % 200.36/200.76 inference(scs_inference,[],[350,351,2,3])). % 200.36/200.76 cnf(369,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x3691,f2(x3691,a1)),f2(a1,a1)),f2(a1,a1)),f2(x3692,f2(x3692,a1))),x3693),f2(f2(a1,a1),x3693))), % 200.36/200.76 inference(scs_inference,[],[359,362,363,98,2,3,4])). % 200.36/200.76 cnf(380,plain, % 200.36/200.76 (~E(f2(f2(f2(x3801,f2(x3801,a1)),f2(a1,a1)),f2(f2(f2(a3,x3802),f2(a1,a1)),f2(f2(a1,a1),x3802))),f2(f2(a3,a1),f2(f2(x3803,f2(x3803,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[297,354,65,2,3])). % 200.36/200.76 cnf(386,plain, % 200.36/200.76 (E(f2(f2(x3861,a1),x3862),f2(f2(x3861,f2(f2(f2(f2(x3863,f2(x3863,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),x3862))), % 200.36/200.76 inference(scs_inference,[],[380,194,93,300,2,3,4])). % 200.36/200.76 cnf(395,plain, % 200.36/200.76 (E(f2(f2(x3951,f2(f2(f2(f2(x3952,f2(x3952,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),x3953),f2(f2(x3951,a1),x3953))), % 200.36/200.76 inference(scs_inference,[],[386,2])). % 200.36/200.76 cnf(421,plain, % 200.36/200.76 (E(f2(f2(a1,x4211),f2(f2(f2(f2(x4212,f2(x4212,a1)),x4213),f2(a1,a1)),f2(x4211,x4213))),a1)), % 200.36/200.76 inference(scs_inference,[],[6,7,107,2,3])). % 200.36/200.76 cnf(424,plain, % 200.36/200.76 (E(f2(f2(x4241,f2(x4241,a1)),f2(f2(x4242,f2(x4242,a1)),f2(a1,a1))),f2(f2(a1,x4243),f2(f2(f2(f2(a1,a1),x4244),f2(a1,a1)),f2(x4243,x4244))))), % 200.36/200.76 inference(scs_inference,[],[71,12,113,2,3])). % 200.36/200.76 cnf(426,plain, % 200.36/200.76 (E(f2(x4261,f2(a1,x4262)),f2(x4261,f2(f2(f2(x4263,f2(x4263,a1)),f2(a1,a1)),x4262)))), % 200.36/200.76 inference(scs_inference,[],[140,2])). % 200.36/200.76 cnf(431,plain, % 200.36/200.76 (E(f2(f2(x4311,f2(f2(f2(x4312,f2(x4312,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(x4311,a1),a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,163,298,2,3])). % 200.36/200.76 cnf(439,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x4391,f2(x4391,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1)),f2(x4392,f2(x4392,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,205,268,2,3])). % 200.36/200.76 cnf(462,plain, % 200.36/200.76 (E(f2(f2(f2(x4621,f2(x4621,a1)),f2(f2(x4622,f2(x4622,a1)),f2(a1,a1))),f2(f2(a1,a1),a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,77,439,2,3])). % 200.36/200.76 cnf(470,plain, % 200.36/200.76 (E(f2(f2(f2(x4701,f2(x4701,a1)),f2(x4702,f2(x4702,a1))),f2(f2(a1,a1),a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,113,333,2,3])). % 200.36/200.76 cnf(481,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x4811,f2(x4811,a1)),f2(a1,a1)),x4812),f2(f2(a1,x4812),a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,273,424,2,3])). % 200.36/200.76 cnf(529,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x5291,f2(x5291,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(f2(x5292,f2(x5292,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(a1,x5293),f2(f2(f2(f2(a1,a1),x5294),f2(a1,a1)),f2(x5293,x5294))))), % 200.36/200.76 inference(scs_inference,[],[12,124,421,2,3])). % 200.36/200.76 cnf(532,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x5321,f2(x5321,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x5322,f2(x5322,a1)),f2(a1,a1))),f2(f2(a1,x5323),f2(f2(f2(f2(a1,a1),x5324),f2(a1,a1)),f2(x5323,x5324))))), % 200.36/200.76 inference(scs_inference,[],[12,119,529,2,3])). % 200.36/200.76 cnf(535,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x5351,f2(x5351,a1)),f2(a1,a1)),f2(a1,a1)),f2(x5352,f2(x5352,a1))),f2(f2(a1,a1),a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,369,532,2,3])). % 200.36/200.76 cnf(539,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x5391,f2(x5391,a1)),f2(a1,a1)),f2(x5392,f2(x5392,a1))),f2(f2(a1,a1),a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,148,535,2,3])). % 200.36/200.76 cnf(543,plain, % 200.36/200.76 (E(f2(f2(x5431,f2(f2(f2(f2(x5432,f2(x5432,a1)),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(x5431,a1),a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,395,539,2,3])). % 200.36/200.76 cnf(547,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x5471,f2(x5471,a1)),f2(a1,a1)),f2(a1,a1)),x5472),f2(f2(a1,x5472),a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,130,543,2,3])). % 200.36/200.76 cnf(577,plain, % 200.36/200.76 (E(f2(f2(f2(x5771,f2(x5771,a1)),f2(a1,a1)),f2(x5772,f2(x5772,a1))),f2(a1,f2(f2(x5773,f2(x5773,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[73,301,251,2,3])). % 200.36/200.76 cnf(585,plain, % 200.36/200.76 (E(f2(f2(f2(a1,x5851),f2(f2(f2(x5852,x5853),f2(a1,a1)),f2(x5851,x5853))),x5854),f2(x5852,x5854))), % 200.36/200.76 inference(scs_inference,[],[6,7,336,577,2,3,5,4])). % 200.36/200.76 cnf(587,plain, % 200.36/200.76 (E(f2(f2(x5871,f2(f2(x5872,f2(x5872,a1)),x5873)),x5874),f2(f2(x5871,f2(a1,x5873)),x5874))), % 200.36/200.76 inference(scs_inference,[],[107,291,2,4])). % 200.36/200.76 cnf(594,plain, % 200.36/200.76 (E(f2(x5941,f2(x5942,a1)),f2(x5941,f2(x5942,f2(x5943,f2(x5943,a1)))))), % 200.36/200.76 inference(scs_inference,[],[23,587,2,4,5])). % 200.36/200.76 cnf(595,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x5951,f2(x5951,a1)),f2(a1,a1)),f2(a1,a1)),f2(x5952,f2(x5952,a1))),f2(f2(a1,a1),a1)),f2(x5953,f2(x5953,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,23,535,587,2,4,5,3])). % 200.36/200.76 cnf(597,plain, % 200.36/200.76 (E(f2(f2(x5971,f2(f2(x5972,f2(x5972,a1)),f2(a1,a1))),x5973),f2(f2(x5971,a1),x5973))), % 200.36/200.76 inference(scs_inference,[],[65,595,2,4])). % 200.36/200.76 cnf(598,plain, % 200.36/200.76 (E(f2(x5981,f2(f2(x5982,f2(x5982,a1)),f2(x5983,f2(x5983,a1)))),f2(x5981,f2(a1,a1)))), % 200.36/200.76 inference(scs_inference,[],[68,65,595,2,4,5])). % 200.36/200.76 cnf(603,plain, % 200.36/200.76 (E(f2(f2(f2(x6031,f2(x6031,a1)),x6032),x6033),f2(f2(a1,x6032),x6033))), % 200.36/200.76 inference(scs_inference,[],[17,598,2,4])). % 200.36/200.76 cnf(604,plain, % 200.36/200.76 (E(f2(x6041,f2(x6042,f2(f2(x6043,f2(x6043,a1)),f2(a1,a1)))),f2(x6041,f2(x6042,a1)))), % 200.36/200.76 inference(scs_inference,[],[65,17,598,2,4,5])). % 200.36/200.76 cnf(605,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x6051,f2(x6051,a1)),f2(a1,a1)),f2(x6052,f2(x6052,a1))),f2(f2(a1,a1),a1)),f2(x6053,f2(x6053,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,65,17,539,598,2,4,5,3])). % 200.36/200.76 cnf(607,plain, % 200.36/200.76 (E(f2(f2(x6071,f2(x6072,f2(x6072,a1))),x6073),f2(f2(x6071,a1),x6073))), % 200.36/200.76 inference(scs_inference,[],[18,597,2,4])). % 200.36/200.76 cnf(613,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x6131,f2(x6131,a1)),f2(x6132,f2(x6132,a1))),x6133),x6134),f2(f2(f2(a1,a1),x6133),x6134))), % 200.36/200.76 inference(scs_inference,[],[113,604,2,4])). % 200.36/200.76 cnf(614,plain, % 200.36/200.76 (E(f2(x6141,f2(x6142,f2(x6143,f2(x6143,a1)))),f2(x6141,f2(x6142,a1)))), % 200.36/200.76 inference(scs_inference,[],[18,113,604,2,4,5])). % 200.36/200.76 cnf(615,plain, % 200.36/200.76 (E(f2(f2(x6151,f2(f2(x6152,f2(x6152,a1)),f2(a1,a1))),f2(f2(x6151,a1),a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,18,113,597,604,2,4,5,3])). % 200.36/200.76 cnf(620,plain, % 200.36/200.76 (E(f2(x6201,f2(f2(f2(x6202,f2(x6202,a1)),f2(x6203,f2(x6203,a1))),x6204)),f2(x6201,f2(f2(a1,a1),x6204)))), % 200.36/200.76 inference(scs_inference,[],[113,140,603,2,4,5])). % 200.36/200.76 cnf(621,plain, % 200.36/200.76 (E(f2(x6211,f2(x6211,f2(f2(x6212,f2(x6212,a1)),f2(a1,a1)))),a1)), % 200.36/200.76 inference(scs_inference,[],[6,113,140,604,603,2,4,5,3])). % 200.36/200.76 cnf(626,plain, % 200.36/200.76 (E(f2(f2(f2(x6261,f2(x6261,a1)),x6262),f2(f2(a1,x6262),a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,140,273,603,605,2,4,5,3])). % 200.36/200.76 cnf(632,plain, % 200.36/200.76 (E(f2(f2(f2(x6321,f2(x6321,a1)),f2(x6322,f2(x6322,a1))),f2(f2(a1,a1),a1)),f2(x6323,f2(x6323,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,258,124,470,613,2,4,5,3])). % 200.36/200.76 cnf(635,plain, % 200.36/200.76 (E(f2(x6351,f2(f2(f2(f2(x6352,f2(x6352,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x6353,f2(x6353,a1)),f2(a1,a1)))),f2(x6351,f2(a1,a1)))), % 200.36/200.76 inference(scs_inference,[],[124,119,632,2,4,5])). % 200.36/200.76 cnf(640,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x6401,f2(x6401,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x6402,f2(x6402,a1)),f2(a1,a1))),x6403),f2(f2(a1,a1),x6403))), % 200.36/200.76 inference(scs_inference,[],[119,635,2,4])). % 200.36/200.76 cnf(642,plain, % 200.36/200.76 (E(f2(f2(f2(x6421,f2(x6421,a1)),f2(f2(x6422,f2(x6422,a1)),f2(a1,a1))),f2(f2(a1,a1),a1)),f2(x6423,f2(x6423,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,119,96,462,635,2,4,5,3])). % 200.36/200.76 cnf(645,plain, % 200.36/200.76 (E(f2(x6451,f2(x6452,f2(f2(x6453,f2(x6453,a1)),f2(x6454,f2(x6454,a1))))),f2(x6451,f2(x6452,f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[189,598,640,2,4,5])). % 200.36/200.76 cnf(650,plain, % 200.36/200.76 (E(f2(f2(x6501,f2(f2(x6502,f2(x6502,a1)),f2(x6503,f2(x6503,a1)))),x6504),f2(f2(x6501,f2(a1,a1)),x6504))), % 200.36/200.76 inference(scs_inference,[],[598,642,2,4])). % 200.36/200.76 cnf(651,plain, % 200.36/200.76 (E(f2(x6511,f2(f2(x6512,f2(f2(x6513,f2(x6513,a1)),f2(a1,a1))),x6514)),f2(x6511,f2(f2(x6512,a1),x6514)))), % 200.36/200.76 inference(scs_inference,[],[598,597,642,2,4,5])). % 200.36/200.76 cnf(658,plain, % 200.36/200.76 (E(f2(f2(a1,x6581),f2(f2(f2(f2(x6582,f2(x6582,a1)),x6583),f2(a1,a1)),f2(x6581,x6583))),f2(x6584,f2(x6584,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,597,604,421,620,2,5,4,3])). % 200.36/200.76 cnf(661,plain, % 200.36/200.76 (E(f2(x6611,f2(x6612,f2(x6612,a1))),f2(x6611,f2(f2(f2(x6613,f2(x6613,a1)),f2(a1,a1)),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[604,45,645,2,4,5])). % 200.36/200.76 cnf(666,plain, % 200.36/200.76 (E(f2(x6661,f2(f2(f2(x6662,f2(x6662,a1)),f2(a1,a1)),f2(a1,a1))),f2(x6661,f2(x6663,f2(x6663,a1))))), % 200.36/200.76 inference(scs_inference,[],[66,650,2,5])). % 200.36/200.76 cnf(690,plain, % 200.36/200.76 (E(f2(f2(x6901,f2(f2(f2(x6902,f2(x6902,a1)),f2(a1,a1)),f2(a1,a1))),f2(f2(x6901,a1),a1)),f2(x6903,f2(x6903,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,84,535,431,651,2,5,4,3])). % 200.36/200.76 cnf(692,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x6921,f2(x6921,a1)),f2(a1,a1)),f2(x6922,f2(x6922,a1))),f2(f2(a1,a1),a1)),x6923),f2(a1,x6923))), % 200.36/200.76 inference(scs_inference,[],[539,690,2,4])). % 200.36/200.76 cnf(698,plain, % 200.36/200.76 (E(f2(x6981,f2(f2(f2(f2(x6982,f2(x6982,a1)),f2(a1,a1)),f2(x6983,f2(x6983,a1))),f2(f2(a1,a1),a1))),f2(x6981,a1))), % 200.36/200.76 inference(scs_inference,[],[539,692,2,5])). % 200.36/200.76 cnf(699,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x6991,f2(x6991,a1)),f2(x6992,f2(x6992,a1))),f2(f2(a1,a1),a1)),x6993),f2(a1,x6993))), % 200.36/200.76 inference(scs_inference,[],[539,470,692,2,5,4])). % 200.36/200.76 cnf(703,plain, % 200.36/200.76 (E(f2(x7031,f2(f2(f2(x7032,f2(x7032,a1)),f2(x7033,f2(x7033,a1))),f2(f2(a1,a1),a1))),f2(x7031,a1))), % 200.36/200.76 inference(scs_inference,[],[470,462,698,2,4,5])). % 200.36/200.76 cnf(704,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x7041,f2(x7041,a1)),f2(a1,a1)),f2(x7042,f2(x7042,a1))),f2(f2(a1,a1),a1)),f2(a1,a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,470,462,692,698,2,4,5,3])). % 200.36/200.76 cnf(716,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x7161,f2(x7161,a1)),f2(x7162,f2(x7162,a1))),f2(f2(a1,a1),a1)),f2(a1,a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,431,547,699,703,2,4,5,3])). % 200.36/200.76 cnf(727,plain, % 200.36/200.76 (E(f2(x7271,f2(f2(x7272,f2(x7272,a1)),f2(a1,a1))),f2(x7271,f2(x7273,f2(x7273,a1))))), % 200.36/200.76 inference(scs_inference,[],[61,439,704,2,4,5])). % 200.36/200.76 cnf(728,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x7281,f2(x7281,a1)),f2(a1,a1)),x7282),f2(f2(a1,x7282),a1)),f2(x7283,f2(x7283,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,61,439,481,704,2,4,5,3])). % 200.36/200.76 cnf(730,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x7301,f2(x7301,a1)),f2(a1,a1)),x7302),f2(f2(a1,x7302),a1)),x7303),f2(a1,x7303))), % 200.36/200.76 inference(scs_inference,[],[481,728,2,4])). % 200.36/200.76 cnf(732,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x7321,f2(x7321,a1)),f2(a1,a1)),f2(x7322,f2(x7322,a1))),f2(f2(a1,a1),a1)),f2(a1,a1)),f2(x7323,f2(x7323,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,439,481,704,728,2,4,5,3])). % 200.36/200.76 cnf(735,plain, % 200.36/200.76 (E(f2(x7351,f2(f2(f2(f2(x7352,f2(x7352,a1)),f2(a1,a1)),x7353),f2(f2(a1,x7353),a1))),f2(x7351,a1))), % 200.36/200.76 inference(scs_inference,[],[481,704,730,2,4,5])). % 200.36/200.76 cnf(742,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x7421,f2(x7421,a1)),f2(a1,a1)),x7422),f2(f2(a1,x7422),a1)),f2(a1,a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,704,730,605,735,2,4,5,3])). % 200.36/200.76 cnf(760,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x7601,f2(x7601,a1)),f2(x7602,f2(x7602,a1))),f2(f2(a1,a1),a1)),f2(a1,a1)),f2(x7603,f2(x7603,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,732,632,716,742,2,4,5,3])). % 200.36/200.76 cnf(763,plain, % 200.36/200.76 (E(f2(x7631,f2(f2(f2(x7632,f2(x7632,a1)),f2(x7633,f2(x7633,a1))),f2(f2(a1,a1),a1))),f2(x7631,f2(x7634,f2(x7634,a1))))), % 200.36/200.76 inference(scs_inference,[],[632,716,760,2,4,5])). % 200.36/200.76 cnf(826,plain, % 200.36/200.76 (E(f2(f2(f2(x8261,f2(x8262,f2(x8262,a1))),x8263),x8264),f2(f2(f2(x8261,a1),x8263),x8264))), % 200.36/200.76 inference(scs_inference,[],[607,763,2,4])). % 200.36/200.76 cnf(838,plain, % 200.36/200.76 (E(f2(x8381,f2(x8381,f2(x8382,f2(x8382,a1)))),a1)), % 200.36/200.76 inference(scs_inference,[],[6,614,661,826,2,4,5,3])). % 200.36/200.76 cnf(889,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x8891,f2(x8891,a1)),x8892),f2(f2(a1,x8892),a1)),x8893),f2(a1,x8893))), % 200.36/200.76 inference(scs_inference,[],[615,626,2,4])). % 200.36/200.76 cnf(894,plain, % 200.36/200.76 (E(f2(x8941,f2(f2(f2(x8942,f2(x8942,a1)),x8943),f2(f2(a1,x8943),a1))),f2(x8941,a1))), % 200.36/200.76 inference(scs_inference,[],[626,889,2,4,5])). % 200.36/200.76 cnf(895,plain, % 200.36/200.76 (E(f2(f2(x8951,f2(f2(x8952,f2(x8952,a1)),f2(a1,a1))),f2(f2(x8951,a1),a1)),f2(x8953,f2(x8953,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,615,626,889,2,4,5,3])). % 200.36/200.76 cnf(899,plain, % 200.36/200.76 (E(f2(f2(f2(x8991,f2(x8991,a1)),x8992),f2(f2(a1,x8992),a1)),f2(x8993,f2(x8993,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,626,889,894,2,4,5,3])). % 200.36/200.76 cnf(903,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x9031,f2(x9031,a1)),x9032),f2(f2(a1,x9032),a1)),f2(a1,a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,889,894,895,2,4,5,3])). % 200.36/200.76 cnf(906,plain, % 200.36/200.76 (E(f2(x9061,f2(x9061,a1)),f2(f2(x9062,f2(f2(x9063,f2(x9063,a1)),f2(a1,a1))),f2(f2(x9062,a1),a1)))), % 200.36/200.76 inference(scs_inference,[],[895,2])). % 200.36/200.76 cnf(913,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x9131,f2(x9131,a1)),x9132),f2(f2(a1,x9132),a1)),f2(a1,a1)),x9133),f2(a1,x9133))), % 200.36/200.76 inference(scs_inference,[],[899,903,2,4])). % 200.36/200.76 cnf(920,plain, % 200.36/200.76 (E(f2(x9201,f2(f2(f2(f2(x9202,f2(x9202,a1)),x9203),f2(f2(a1,x9203),a1)),f2(a1,a1))),f2(x9201,a1))), % 200.36/200.76 inference(scs_inference,[],[903,913,2,4,5])). % 200.36/200.76 cnf(921,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x9211,f2(x9211,a1)),x9212),f2(f2(a1,x9212),a1)),f2(a1,a1)),f2(x9213,f2(x9213,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,903,913,2,4,5,3])). % 200.36/200.76 cnf(925,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x9251,f2(x9251,a1)),x9252),f2(f2(a1,x9252),a1)),f2(a1,a1)),f2(a1,a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,913,920,2,4,5,3])). % 200.36/200.76 cnf(934,plain, % 200.36/200.76 (E(f2(x9341,f2(x9341,a1)),f2(f2(f2(f2(x9342,f2(x9342,a1)),x9343),f2(f2(a1,x9343),a1)),f2(a1,a1)))), % 200.36/200.76 inference(scs_inference,[],[921,2])). % 200.36/200.76 cnf(942,plain, % 200.36/200.76 (E(f2(f2(f2(f2(f2(x9421,f2(x9421,a1)),x9422),f2(f2(a1,x9422),a1)),f2(a1,a1)),f2(a1,a1)),f2(x9423,f2(x9423,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,925,934,2,4,5,3])). % 200.36/200.76 cnf(951,plain, % 200.36/200.76 (E(f2(f2(f2(a1,x9511),f2(f2(f2(x9512,x9513),f2(a1,a1)),f2(x9511,x9513))),f2(x9512,a1)),a1)), % 200.36/200.76 inference(scs_inference,[],[6,942,585,906,2,4,5,3])). % 200.36/200.76 cnf(1066,plain, % 200.36/200.76 (E(f2(x10661,f2(x10661,f2(f2(x10662,f2(x10662,a1)),f2(a1,a1)))),f2(x10663,f2(x10663,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,621,838,2,4,5,3])). % 200.36/200.76 cnf(1070,plain, % 200.36/200.76 (E(f2(x10701,f2(x10701,f2(x10702,f2(x10702,a1)))),f2(x10703,f2(x10703,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,838,1066,2,4,5,3])). % 200.36/200.76 cnf(1311,plain, % 200.36/200.76 (E(f2(f2(f2(a1,x13111),f2(f2(f2(x13112,x13113),f2(a1,a1)),f2(x13111,x13113))),f2(x13112,a1)),f2(x13114,f2(x13114,a1)))), % 200.36/200.76 inference(scs_inference,[],[9,951,2,3])). % 200.36/200.76 cnf(1330,plain, % 200.36/200.76 (E(f2(f2(f2(f2(x13301,f2(x13301,a1)),f2(a1,a1)),x13302),f2(f2(f2(x13303,x13304),f2(a1,a1)),f2(x13302,x13304))),x13303)), % 200.36/200.76 inference(scs_inference,[],[7,273,951,658,2,4,3])). % 200.36/200.76 cnf(1333,plain, % 200.36/200.76 (E(f2(f2(a1,f2(f2(x13331,f2(x13331,a1)),f2(a1,a1))),f2(f2(f2(x13332,x13333),f2(a1,a1)),f2(a1,x13333))),x13332)), % 200.36/200.76 inference(scs_inference,[],[7,597,1311,2,3])). % 200.36/200.76 cnf(1337,plain, % 200.36/200.76 (E(f2(f2(f2(x13371,f2(x13371,a1)),x13372),f2(f2(f2(x13373,x13374),f2(a1,a1)),f2(x13372,x13374))),x13373)), % 200.36/200.76 inference(scs_inference,[],[7,603,1330,2,3])). % 200.36/200.76 cnf(1339,plain, % 200.36/200.76 (E(x13391,f2(f2(f2(x13392,f2(x13392,a1)),x13393),f2(f2(f2(x13391,x13394),f2(a1,a1)),f2(x13393,x13394))))), % 200.36/200.76 inference(scs_inference,[],[1337,2])). % 200.36/200.76 cnf(1347,plain, % 200.36/200.76 (E(f2(f2(a1,f2(f2(x13471,a1),f2(a1,a1))),f2(f2(f2(x13472,f2(x13472,a1)),f2(a1,a1)),f2(a1,a1))),x13471)), % 200.36/200.76 inference(scs_inference,[],[7,666,1333,2,3])). % 200.36/200.76 cnf(1351,plain, % 200.36/200.76 (E(f2(f2(a1,f2(f2(x13511,a1),f2(a1,a1))),f2(f2(x13512,f2(x13512,a1)),f2(a1,a1))),x13511)), % 200.36/200.76 inference(scs_inference,[],[7,727,1347,2,3])). % 200.36/200.76 cnf(1355,plain, % 200.36/200.76 (E(f2(a1,f2(f2(f2(x13551,x13552),f2(a1,a1)),f2(f2(a1,a1),x13552))),x13551)), % 200.36/200.76 inference(scs_inference,[],[7,22,1351,2,3])). % 200.36/200.76 cnf(1371,plain, % 200.36/200.76 (E(f2(f2(a1,x13711),f2(a1,f2(x13711,f2(x13712,a1)))),x13712)), % 200.36/200.76 inference(scs_inference,[],[7,426,1355,2,3])). % 200.36/200.76 cnf(1375,plain, % 200.36/200.76 (E(f2(f2(a1,x13751),f2(f2(f2(x13752,f2(x13751,a1)),f2(a1,a1)),a1)),x13752)), % 200.36/200.76 inference(scs_inference,[],[7,594,1371,2,3])). % 200.36/200.76 cnf(1418,plain, % 200.36/200.76 (~E(f2(a3,a1),f2(f2(x14181,f2(x14181,a1)),f2(f2(a3,a1),f2(a1,a1))))), % 200.36/200.76 inference(scs_inference,[],[85,17,3])). % 200.36/200.76 cnf(1447,plain, % 200.36/200.76 (E(f2(a1,a1),f2(x14471,f2(x14471,a1)))), % 200.36/200.76 inference(scs_inference,[],[1339,1070,3])). % 200.36/200.76 cnf(1451,plain, % 200.36/200.76 (E(f2(x14511,f2(a1,a1)),f2(x14511,f2(x14512,f2(x14512,a1))))), % 200.36/200.76 inference(scs_inference,[],[1447,5])). % 200.36/200.76 cnf(1452,plain, % 200.36/200.76 (E(f2(f2(a1,a1),x14521),f2(f2(x14522,f2(x14522,a1)),x14521))), % 200.36/200.76 inference(scs_inference,[],[1447,5,4])). % 200.36/200.76 cnf(1455,plain, % 200.36/200.76 (~E(f2(f2(a3,a1),a1),f2(f2(a1,f2(f2(a3,a1),f2(a1,a1))),f2(a1,a1)))), % 200.36/200.76 inference(scs_inference,[],[10,1451,3])). % 200.36/200.76 cnf(1462,plain, % 200.36/200.76 (~E(f2(f2(a1,f2(f2(a3,a1),f2(a1,a1))),f2(a1,a1)),f2(f2(a3,a1),a1))), % 200.36/200.76 inference(scs_inference,[],[1455,1418,1452,3,2])). % 200.36/200.76 cnf(1486,plain, % 200.36/200.76 (~E(f2(f2(a1,f2(f2(a3,a1),f2(a1,a1))),f2(a1,a1)),f2(f2(a3,a1),f2(x14861,f2(x14861,a1))))), % 200.36/200.76 inference(scs_inference,[],[18,1462,3])). % 200.36/200.76 cnf(1508,plain, % 200.36/200.76 (~E(f2(f2(a1,f2(f2(a3,a1),f2(a1,a1))),f2(a1,a1)),f2(f2(a3,a1),f2(a1,a1)))), % 200.36/200.76 inference(scs_inference,[],[1486,1451,3])). % 200.36/200.76 cnf(1549,plain, % 200.36/200.76 ($false), % 200.36/200.76 inference(scs_inference,[],[1508,426,1375,3]), % 200.36/200.76 ['proof']). % 200.36/200.76 % SZS output end Proof % 200.36/200.76 % Total time :199.630000s %------------------------------------------------------------------------------