%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : REL049-1 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 13:54:15 EDT 2024
% Result : Unsatisfiable 63.42s 63.66s
% Output : CNFRefutation 63.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : REL049-1 : TPTP v8.2.0. Released v4.0.0.
% 0.03/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.31 % Computer : n032.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Sun Jun 23 05:23:54 EDT 2024
% 0.11/0.31 % CPUTime :
% 0.16/0.56 start to proof:theBenchmark
% 63.42/63.65 %-------------------------------------------
% 63.42/63.65 % File :CSE---1.7
% 63.42/63.65 % Problem :theBenchmark
% 63.42/63.65 % Transform :cnf
% 63.42/63.65 % Format :tptp:raw
% 63.42/63.65 % Command :java -jar mcs_scs.jar %d %s
% 63.42/63.65
% 63.42/63.65 % Result :Theorem 62.900000s
% 63.42/63.65 % Output :CNFRefutation 62.900000s
% 63.42/63.65 %-------------------------------------------
% 63.42/63.65 %------------------------------------------------------------------------------
% 63.42/63.66 % File : REL049-1 : TPTP v8.2.0. Released v4.0.0.
% 63.42/63.66 % Domain : Relation Algebra
% 63.42/63.66 % Problem : Join splitting
% 63.42/63.66 % Version : [Mad95] (equational) axioms.
% 63.42/63.66 % English : Join can be split into 2 inequations iff the join is on the
% 63.42/63.66 % left hand side of an inequation.
% 63.42/63.66
% 63.42/63.66 % Refs : [Mad95] Maddux (1995), Relation-Algebraic Semantics
% 63.42/63.66 % : [Hoe08] Hoefner (2008), Email to G. Sutcliffe
% 63.42/63.66 % Source : [Hoe08]
% 63.42/63.66 % Names :
% 63.42/63.66
% 63.42/63.66 % Status : Unsatisfiable
% 63.42/63.66 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.06 v6.0.0, 0.10 v5.5.0, 0.05 v5.4.0, 0.00 v4.0.1, 0.07 v4.0.0
% 63.42/63.66 % Syntax : Number of clauses : 16 ( 16 unt; 0 nHn; 3 RR)
% 63.42/63.66 % Number of literals : 16 ( 16 equ; 1 neg)
% 63.42/63.66 % Maximal clause size : 1 ( 1 avg)
% 63.42/63.66 % Maximal term depth : 5 ( 2 avg)
% 63.42/63.66 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 63.42/63.66 % Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% 63.42/63.66 % Number of variables : 25 ( 0 sgn)
% 63.42/63.66 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 63.42/63.66
% 63.42/63.66 % Comments : tptp2X -f tptp:short -t cnf:otter REL049+1.p
% 63.42/63.66 %------------------------------------------------------------------------------
% 63.42/63.66 %----Include axioms of relation algebra
% 63.42/63.66 include('Axioms/REL001-0.ax').
% 63.42/63.66 %------------------------------------------------------------------------------
% 63.42/63.66 cnf(goals_14,negated_conjecture,
% 63.42/63.66 join(sk1,sk2) = sk2 ).
% 63.42/63.66
% 63.42/63.66 cnf(goals_15,negated_conjecture,
% 63.42/63.66 join(sk3,sk2) = sk2 ).
% 63.42/63.66
% 63.42/63.66 cnf(goals_16,negated_conjecture,
% 63.42/63.66 join(join(sk1,sk3),sk2) != sk2 ).
% 63.42/63.66
% 63.42/63.66 %------------------------------------------------------------------------------
% 63.42/63.66 %-------------------------------------------
% 63.42/63.66 % Proof found
% 63.42/63.66 % SZS status Theorem for theBenchmark
% 63.42/63.66 % SZS output start Proof
% 63.42/63.66 %ClaNum:24(EqnAxiom:9)
% 63.42/63.66 %VarNum:49(SingletonVarNum:23)
% 63.42/63.66 %MaxLitNum:1
% 63.42/63.66 %MaxfuncDepth:4
% 63.42/63.66 %SharedTerms:13
% 63.42/63.66 %goalClause: 11 12 24
% 63.42/63.66 %singleGoalClaCount:3
% 63.42/63.66 [11]E(f5(a4,a7),a7)
% 63.42/63.66 [12]E(f5(a8,a7),a7)
% 63.42/63.66 [24]~E(f5(f5(a4,a8),a7),a7)
% 63.42/63.66 [13]E(f2(x131,a6),x131)
% 63.42/63.66 [10]E(f1(f1(x101)),x101)
% 63.42/63.66 [14]E(f5(x141,f3(x141)),a9)
% 63.42/63.66 [18]E(f3(f5(f3(x181),f3(f3(x181)))),a10)
% 63.42/63.66 [15]E(f5(x151,x152),f5(x152,x151))
% 63.42/63.66 [16]E(f5(f1(x161),f1(x162)),f1(f5(x161,x162)))
% 63.42/63.66 [17]E(f2(f1(x171),f1(x172)),f1(f2(x172,x171)))
% 63.42/63.66 [22]E(f5(f2(f1(x221),f3(f2(x221,x222))),f3(x222)),f3(x222))
% 63.42/63.66 [23]E(f5(f3(f5(f3(x231),f3(x232))),f3(f5(f3(x231),x232))),x231)
% 63.42/63.66 [19]E(f5(f5(x191,x192),x193),f5(x191,f5(x192,x193)))
% 63.42/63.66 [20]E(f2(f2(x201,x202),x203),f2(x201,f2(x202,x203)))
% 63.42/63.66 [21]E(f5(f2(x211,x212),f2(x213,x212)),f2(f5(x211,x213),x212))
% 63.42/63.66 %EqnAxiom
% 63.42/63.66 [1]E(x11,x11)
% 63.42/63.66 [2]E(x22,x21)+~E(x21,x22)
% 63.42/63.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 63.42/63.66 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 63.42/63.66 [5]~E(x51,x52)+E(f5(x51,x53),f5(x52,x53))
% 63.42/63.66 [6]~E(x61,x62)+E(f5(x63,x61),f5(x63,x62))
% 63.42/63.66 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 63.42/63.66 [8]~E(x81,x82)+E(f2(x81,x83),f2(x82,x83))
% 63.42/63.66 [9]~E(x91,x92)+E(f2(x93,x91),f2(x93,x92))
% 63.42/63.66
% 63.42/63.66 %-------------------------------------------
% 63.42/63.67 cnf(25,plain,
% 63.42/63.67 (E(a7,f5(a4,a7))),
% 63.42/63.67 inference(scs_inference,[],[11,2])).
% 63.42/63.67 cnf(26,plain,
% 63.42/63.67 (~E(f5(f5(a4,a8),a7),f5(a4,a7))),
% 63.42/63.67 inference(scs_inference,[],[11,24,2,3])).
% 63.42/63.67 cnf(27,plain,
% 63.42/63.67 (~E(f5(a4,a8),a4)),
% 63.42/63.67 inference(scs_inference,[],[11,24,2,3,5])).
% 63.42/63.67 cnf(28,plain,
% 63.42/63.67 (E(a7,f5(a8,a7))),
% 63.42/63.67 inference(scs_inference,[],[12,2])).
% 63.42/63.67 cnf(29,plain,
% 63.42/63.67 (~E(f5(f5(a4,a8),a7),f5(a8,a7))),
% 63.42/63.67 inference(scs_inference,[],[12,24,2,3])).
% 63.42/63.67 cnf(31,plain,
% 63.42/63.67 (E(x311,f2(x311,a6))),
% 63.42/63.67 inference(scs_inference,[],[13,2])).
% 63.42/63.67 cnf(34,plain,
% 63.42/63.67 (E(f3(x341),f5(f2(f1(x342),f3(f2(x342,x341))),f3(x341)))),
% 63.42/63.67 inference(scs_inference,[],[22,2])).
% 63.42/63.67 cnf(35,plain,
% 63.42/63.67 (E(f5(a4,a7),f2(a7,a6))),
% 63.42/63.67 inference(scs_inference,[],[11,31,22,2,3])).
% 63.42/63.67 cnf(37,plain,
% 63.42/63.67 (E(f2(a7,a6),f5(a4,a7))),
% 63.42/63.67 inference(scs_inference,[],[35,2])).
% 63.42/63.67 cnf(38,plain,
% 63.42/63.67 (E(f1(f1(f3(x381))),f5(f2(f1(x382),f3(f2(x382,x381))),f3(x381)))),
% 63.42/63.67 inference(scs_inference,[],[34,35,10,2,3])).
% 63.42/63.67 cnf(40,plain,
% 63.42/63.67 (E(f5(f2(f1(x401),f3(f2(x401,x402))),f3(x402)),f1(f1(f3(x402))))),
% 63.42/63.67 inference(scs_inference,[],[38,2])).
% 63.42/63.67 cnf(41,plain,
% 63.42/63.67 (~E(f5(f5(a4,a8),a7),f2(a7,a6))),
% 63.42/63.67 inference(scs_inference,[],[37,38,26,2,3])).
% 63.42/63.67 cnf(42,plain,
% 63.42/63.67 (E(f2(f5(x421,x422),x423),f5(f2(x421,x423),f2(x422,x423)))),
% 63.42/63.67 inference(scs_inference,[],[21,2])).
% 63.42/63.67 cnf(45,plain,
% 63.42/63.67 (E(f1(f5(x451,x452)),f5(f1(x451),f1(x452)))),
% 63.42/63.67 inference(scs_inference,[],[16,2])).
% 63.42/63.67 cnf(46,plain,
% 63.42/63.67 (E(f5(x461,x462),f5(f2(x461,a6),f2(x462,a6)))),
% 63.42/63.67 inference(scs_inference,[],[42,31,16,2,3])).
% 63.42/63.67 cnf(49,plain,
% 63.42/63.67 (E(f5(f2(x491,a6),f2(x492,a6)),f5(x491,x492))),
% 63.42/63.67 inference(scs_inference,[],[46,2])).
% 63.42/63.67 cnf(50,plain,
% 63.42/63.67 (E(f1(f5(x501,x502)),f5(f2(f1(x501),a6),f2(f1(x502),a6)))),
% 63.42/63.67 inference(scs_inference,[],[45,46,2,3])).
% 63.42/63.67 cnf(52,plain,
% 63.42/63.67 (E(f5(f2(f1(x521),a6),f2(f1(x522),a6)),f1(f5(x521,x522)))),
% 63.42/63.67 inference(scs_inference,[],[50,2])).
% 63.42/63.67 cnf(53,plain,
% 63.42/63.67 (~E(f5(f5(a4,a8),a7),f5(f2(a8,a6),f2(a7,a6)))),
% 63.42/63.67 inference(scs_inference,[],[49,50,29,2,3])).
% 63.42/63.67 cnf(55,plain,
% 63.42/63.67 (E(f1(f2(x551,x552)),f2(f1(x552),f1(x551)))),
% 63.42/63.67 inference(scs_inference,[],[17,2])).
% 63.42/63.67 cnf(56,plain,
% 63.42/63.67 (E(f2(f5(f1(x561),f1(x562)),a6),f1(f5(x561,x562)))),
% 63.42/63.67 inference(scs_inference,[],[52,42,17,2,3])).
% 63.42/63.67 cnf(58,plain,
% 63.42/63.67 (E(f1(f5(x581,x582)),f2(f5(f1(x581),f1(x582)),a6))),
% 63.42/63.67 inference(scs_inference,[],[56,2])).
% 63.42/63.67 cnf(59,plain,
% 63.42/63.67 (~E(f5(f5(a4,a8),a7),f5(f2(f2(a8,a6),a6),f2(f2(a7,a6),a6)))),
% 63.42/63.67 inference(scs_inference,[],[49,56,53,2,3])).
% 63.42/63.67 cnf(61,plain,
% 63.42/63.67 (E(f5(x611,f5(x612,x613)),f5(f5(x611,x612),x613))),
% 63.42/63.67 inference(scs_inference,[],[19,2])).
% 63.42/63.67 cnf(62,plain,
% 63.42/63.67 (~E(f5(f5(a4,a8),a7),f2(f5(f2(a8,a6),f2(a7,a6)),a6))),
% 63.42/63.67 inference(scs_inference,[],[42,59,19,2,3])).
% 63.42/63.67 cnf(64,plain,
% 63.42/63.67 (E(f2(x641,f2(x642,x643)),f2(f2(x641,x642),x643))),
% 63.42/63.67 inference(scs_inference,[],[20,2])).
% 63.42/63.67 cnf(65,plain,
% 63.42/63.67 (E(f5(f2(x651,a6),f2(f5(x652,x653),a6)),f5(f5(x651,x652),x653))),
% 63.42/63.67 inference(scs_inference,[],[61,49,20,2,3])).
% 63.42/63.67 cnf(68,plain,
% 63.42/63.67 (E(f5(f5(x681,x682),x683),f5(f2(x681,a6),f2(f5(x682,x683),a6)))),
% 63.42/63.67 inference(scs_inference,[],[65,2])).
% 63.42/63.67 cnf(71,plain,
% 63.42/63.67 (E(a9,f5(x711,f3(x711)))),
% 63.42/63.67 inference(scs_inference,[],[14,2])).
% 63.42/63.67 cnf(74,plain,
% 63.42/63.67 (E(x741,f5(f3(f5(f3(x741),f3(x742))),f3(f5(f3(x741),x742))))),
% 63.42/63.67 inference(scs_inference,[],[23,2])).
% 63.42/63.67 cnf(75,plain,
% 63.42/63.67 (E(a9,f5(f2(x751,a6),f2(f5(x752,f3(f5(x751,x752))),a6)))),
% 63.42/63.67 inference(scs_inference,[],[68,71,23,2,3])).
% 63.42/63.67 cnf(78,plain,
% 63.42/63.67 (E(f5(f2(x781,a6),f2(f5(x782,f3(f5(x781,x782))),a6)),a9)),
% 63.42/63.67 inference(scs_inference,[],[75,2])).
% 63.42/63.67 cnf(79,plain,
% 63.42/63.67 (E(f2(f1(f2(x791,x792)),a6),f2(f1(x792),f1(x791)))),
% 63.42/63.67 inference(scs_inference,[],[55,75,13,2,3])).
% 63.42/63.67 cnf(81,plain,
% 63.42/63.67 (E(f2(f1(x811),f1(x812)),f2(f1(f2(x812,x811)),a6))),
% 63.42/63.67 inference(scs_inference,[],[79,2])).
% 63.42/63.67 cnf(82,plain,
% 63.42/63.67 (E(f5(f2(x821,f2(x822,x823)),f2(x824,f2(x822,x823))),f2(f2(f5(x821,x824),x822),x823))),
% 63.42/63.67 inference(scs_inference,[],[64,79,21,2,3])).
% 63.42/63.67 cnf(85,plain,
% 63.42/63.67 (E(f2(f2(f5(x851,x852),x853),x854),f5(f2(x851,f2(x853,x854)),f2(x852,f2(x853,x854))))),
% 63.42/63.67 inference(scs_inference,[],[82,2])).
% 63.42/63.67 cnf(86,plain,
% 63.42/63.67 (E(f5(a4,a7),f5(f3(f5(f3(a7),f3(x861))),f3(f5(f3(a7),x861))))),
% 63.42/63.67 inference(scs_inference,[],[11,74,82,2,3])).
% 63.42/63.67 cnf(88,plain,
% 63.42/63.67 (E(f5(f3(f5(f3(a7),f3(x881))),f3(f5(f3(a7),x881))),f5(a4,a7))),
% 63.42/63.67 inference(scs_inference,[],[86,2])).
% 63.42/63.67 cnf(89,plain,
% 63.42/63.67 (E(f1(f1(f1(f2(x891,x892)))),f2(f1(x892),f1(x891)))),
% 63.42/63.67 inference(scs_inference,[],[55,86,10,2,3])).
% 63.42/63.67 cnf(91,plain,
% 63.42/63.67 (E(f2(f1(x911),f1(x912)),f1(f1(f1(f2(x912,x911)))))),
% 63.42/63.67 inference(scs_inference,[],[89,2])).
% 63.42/63.67 cnf(92,plain,
% 63.42/63.67 (~E(f5(f5(a4,a8),a7),f5(f3(f5(f3(a7),f3(x921))),f3(f5(f3(a7),x921))))),
% 63.42/63.67 inference(scs_inference,[],[88,89,26,2,3])).
% 63.42/63.67 cnf(93,plain,
% 63.42/63.67 (E(a10,f3(f5(f3(x931),f3(f3(x931)))))),
% 63.42/63.67 inference(scs_inference,[],[18,2])).
% 63.42/63.67 cnf(96,plain,
% 63.42/63.67 (E(x961,f1(f1(x961)))),
% 63.42/63.67 inference(scs_inference,[],[10,2])).
% 63.42/63.67 cnf(99,plain,
% 63.42/63.67 (E(f5(a4,a7),f1(f1(a7)))),
% 63.42/63.67 inference(scs_inference,[],[11,96,3])).
% 63.42/63.67 cnf(101,plain,
% 63.42/63.67 (E(f1(f1(a7)),f5(a4,a7))),
% 63.42/63.67 inference(scs_inference,[],[11,96,3,2])).
% 63.42/63.67 cnf(102,plain,
% 63.42/63.67 (~E(f5(f5(a4,a8),a7),f1(f1(a7)))),
% 63.42/63.67 inference(scs_inference,[],[101,26,3])).
% 63.42/63.67 cnf(103,plain,
% 63.42/63.67 (~E(f5(f5(a4,a8),a7),f5(f3(f5(f3(a7),x1031)),f3(f5(f3(a7),f3(x1031)))))),
% 63.42/63.67 inference(scs_inference,[],[92,15,3])).
% 63.42/63.67 cnf(105,plain,
% 63.42/63.67 (E(f5(x1051,f5(x1052,f3(f5(x1051,x1052)))),a9)),
% 63.42/63.67 inference(scs_inference,[],[61,14,3])).
% 63.42/63.67 cnf(108,plain,
% 63.42/63.67 (E(a9,f5(x1081,f5(x1082,f3(f5(x1081,x1082)))))),
% 63.42/63.67 inference(scs_inference,[],[61,14,3,2])).
% 63.42/63.67 cnf(111,plain,
% 63.42/63.67 (E(f2(f5(f1(x1111),f1(x1112)),a6),f1(f1(f1(f5(x1111,x1112)))))),
% 63.42/63.67 inference(scs_inference,[],[10,58,3,2])).
% 63.42/63.67 cnf(115,plain,
% 63.42/63.67 (E(f1(f1(a10)),f3(f5(f3(x1151),f3(f3(x1151)))))),
% 63.42/63.67 inference(scs_inference,[],[10,93,3])).
% 63.42/63.67 cnf(118,plain,
% 63.42/63.67 (E(f1(f1(a9)),f5(x1181,f5(x1182,f3(f5(x1181,x1182)))))),
% 63.42/63.67 inference(scs_inference,[],[10,108,3])).
% 63.42/63.67 cnf(120,plain,
% 63.42/63.67 (E(f5(x1201,f5(x1202,f3(f5(x1201,x1202)))),f1(f1(a9)))),
% 63.42/63.67 inference(scs_inference,[],[10,108,3,2])).
% 63.42/63.67 cnf(123,plain,
% 63.42/63.67 (E(f5(f1(x1231),f1(x1232)),f1(f1(f1(f5(x1231,x1232)))))),
% 63.42/63.67 inference(scs_inference,[],[10,45,3,2])).
% 63.42/63.67 cnf(126,plain,
% 63.42/63.67 (E(f2(f2(x1261,x1262),x1263),f1(f1(f2(x1261,f2(x1262,x1263)))))),
% 63.42/63.67 inference(scs_inference,[],[10,64,3,2])).
% 63.42/63.67 cnf(129,plain,
% 63.42/63.67 (E(f5(f2(x1291,a6),f2(f5(x1292,x1293),a6)),f1(f1(f5(f5(x1291,x1292),x1293))))),
% 63.42/63.67 inference(scs_inference,[],[10,68,3,2])).
% 63.42/63.67 cnf(130,plain,
% 63.42/63.67 (E(f1(f1(a9)),f5(x1301,f3(x1301)))),
% 63.42/63.67 inference(scs_inference,[],[10,71,3])).
% 63.42/63.67 cnf(132,plain,
% 63.42/63.67 (E(f5(x1321,f3(x1321)),f1(f1(a9)))),
% 63.42/63.67 inference(scs_inference,[],[10,71,3,2])).
% 63.42/63.67 cnf(135,plain,
% 63.42/63.67 (E(f1(f1(a9)),f1(f1(f5(x1351,f3(x1351)))))),
% 63.42/63.67 inference(scs_inference,[],[10,132,3,2])).
% 63.42/63.67 cnf(136,plain,
% 63.42/63.67 (E(f1(f1(f5(x1361,f5(x1362,x1363)))),f5(f5(x1361,x1362),x1363))),
% 63.42/63.67 inference(scs_inference,[],[10,61,3])).
% 63.42/63.67 cnf(138,plain,
% 63.42/63.67 (E(f5(f5(x1381,x1382),x1383),f1(f1(f5(x1381,f5(x1382,x1383)))))),
% 63.42/63.67 inference(scs_inference,[],[10,61,3,2])).
% 63.42/63.67 cnf(141,plain,
% 63.42/63.67 (E(f5(x1411,f3(x1411)),f1(f1(f1(f1(a9)))))),
% 63.42/63.67 inference(scs_inference,[],[10,130,3,2])).
% 63.42/63.67 cnf(144,plain,
% 63.42/63.67 (E(f5(f2(f1(x1441),a6),f2(f1(x1442),a6)),f1(f1(f1(f5(x1441,x1442)))))),
% 63.42/63.67 inference(scs_inference,[],[10,50,3,2])).
% 63.42/63.67 cnf(150,plain,
% 63.42/63.67 (E(f1(f5(x1501,x1502)),f1(f1(f5(f1(x1501),f1(x1502)))))),
% 63.42/63.67 inference(scs_inference,[],[10,16,3,2])).
% 63.42/63.67 cnf(156,plain,
% 63.42/63.67 (E(f5(x1561,f5(x1562,x1563)),f1(f1(f5(f5(x1561,x1562),x1563))))),
% 63.42/63.67 inference(scs_inference,[],[10,19,3,2])).
% 63.42/63.67 cnf(159,plain,
% 63.42/63.67 (E(f2(x1591,f2(x1592,x1593)),f1(f1(f2(f2(x1591,x1592),x1593))))),
% 63.42/63.67 inference(scs_inference,[],[10,20,3,2])).
% 63.42/63.67 cnf(160,plain,
% 63.42/63.67 (E(f1(f1(f5(x1601,f3(x1601)))),a9)),
% 63.42/63.67 inference(scs_inference,[],[10,14,3])).
% 63.42/63.67 cnf(162,plain,
% 63.42/63.67 (E(a9,f1(f1(f5(x1621,f3(x1621)))))),
% 63.42/63.67 inference(scs_inference,[],[10,14,3,2])).
% 63.42/63.67 cnf(163,plain,
% 63.42/63.67 (E(f2(f2(f2(f5(x1631,x1632),x1633),x1634),a6),f5(f2(x1631,f2(x1633,x1634)),f2(x1632,f2(x1633,x1634))))),
% 63.42/63.67 inference(scs_inference,[],[13,85,3])).
% 63.42/63.67 cnf(165,plain,
% 63.42/63.67 (E(f5(f2(x1651,f2(x1652,x1653)),f2(x1654,f2(x1652,x1653))),f2(f2(f2(f5(x1651,x1654),x1652),x1653),a6))),
% 63.42/63.67 inference(scs_inference,[],[13,85,3,2])).
% 63.42/63.67 cnf(171,plain,
% 63.42/63.67 (E(f1(f1(f2(x1711,f2(x1712,x1713)))),f2(f2(f2(x1711,x1712),x1713),a6))),
% 63.42/63.67 inference(scs_inference,[],[13,126,3,2])).
% 63.42/63.67 cnf(172,plain,
% 63.42/63.67 (E(f2(f5(f5(x1721,x1722),x1723),a6),f1(f1(f5(x1721,f5(x1722,x1723)))))),
% 63.42/63.67 inference(scs_inference,[],[13,138,3])).
% 63.42/63.67 cnf(177,plain,
% 63.42/63.67 (E(f1(f1(f5(f1(x1771),f1(x1772)))),f2(f1(f5(x1771,x1772)),a6))),
% 63.42/63.67 inference(scs_inference,[],[13,150,3,2])).
% 63.42/63.67 cnf(183,plain,
% 63.42/63.67 (E(f1(f1(f2(f2(x1831,x1832),x1833))),f2(f2(x1831,f2(x1832,x1833)),a6))),
% 63.42/63.67 inference(scs_inference,[],[13,159,3,2])).
% 63.42/63.67 cnf(189,plain,
% 63.42/63.67 (E(f1(f1(f5(x1891,f3(x1891)))),f2(f1(f1(a9)),a6))),
% 63.42/63.67 inference(scs_inference,[],[13,135,3,2])).
% 63.42/63.67 cnf(190,plain,
% 63.42/63.67 (E(f2(a9,a6),f1(f1(f5(x1901,f3(x1901)))))),
% 63.42/63.67 inference(scs_inference,[],[13,162,3])).
% 63.42/63.67 cnf(192,plain,
% 63.42/63.67 (E(f1(f1(f5(x1921,f3(x1921)))),f2(a9,a6))),
% 63.42/63.67 inference(scs_inference,[],[13,162,3,2])).
% 63.42/63.67 cnf(193,plain,
% 63.42/63.67 (E(f2(f1(f1(f5(x1931,f3(x1931)))),a6),f2(a9,a6))),
% 63.42/63.67 inference(scs_inference,[],[13,192,3])).
% 63.42/63.67 cnf(196,plain,
% 63.42/63.67 (E(f2(f2(f1(x1961),f1(x1962)),a6),f1(f1(f1(f2(x1962,x1961)))))),
% 63.42/63.67 inference(scs_inference,[],[13,91,193,2,3])).
% 63.42/63.67 cnf(199,plain,
% 63.42/63.67 (E(f2(f5(f2(f1(x1991),a6),f2(f1(x1992),a6)),a6),f1(f5(x1991,x1992)))),
% 63.42/63.67 inference(scs_inference,[],[13,52,196,2,3])).
% 63.42/63.67 cnf(201,plain,
% 63.42/63.67 (E(f1(f5(x2011,x2012)),f2(f5(f2(f1(x2011),a6),f2(f1(x2012),a6)),a6))),
% 63.42/63.67 inference(scs_inference,[],[199,2])).
% 63.42/63.67 cnf(202,plain,
% 63.42/63.67 (E(f2(f5(x2021,f3(x2021)),a6),f1(f1(a9)))),
% 63.42/63.67 inference(scs_inference,[],[13,132,199,2,3])).
% 63.42/63.67 cnf(204,plain,
% 63.42/63.67 (E(f1(f1(a9)),f2(f5(x2041,f3(x2041)),a6))),
% 63.42/63.67 inference(scs_inference,[],[202,2])).
% 63.42/63.67 cnf(205,plain,
% 63.42/63.67 (E(f2(f1(f5(x2051,x2052)),a6),f2(f5(f2(f1(x2051),a6),f2(f1(x2052),a6)),a6))),
% 63.42/63.67 inference(scs_inference,[],[13,201,202,2,3])).
% 63.42/63.67 cnf(207,plain,
% 63.42/63.67 (E(f2(f5(f2(f1(x2071),a6),f2(f1(x2072),a6)),a6),f2(f1(f5(x2071,x2072)),a6))),
% 63.42/63.67 inference(scs_inference,[],[205,2])).
% 63.42/63.67 cnf(208,plain,
% 63.42/63.67 (E(f2(f1(f1(a9)),a6),f2(f5(x2081,f3(x2081)),a6))),
% 63.42/63.67 inference(scs_inference,[],[13,204,205,2,3])).
% 63.42/63.67 cnf(210,plain,
% 63.42/63.68 (E(f2(f5(x2101,f3(x2101)),a6),f2(f1(f1(a9)),a6))),
% 63.42/63.68 inference(scs_inference,[],[208,2])).
% 63.42/63.68 cnf(211,plain,
% 63.42/63.68 (E(f2(f1(f5(x2111,x2112)),a6),f2(f5(f1(x2111),f1(x2112)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,58,208,2,3])).
% 63.42/63.68 cnf(213,plain,
% 63.42/63.68 (E(f2(f5(f1(x2131),f1(x2132)),a6),f2(f1(f5(x2131,x2132)),a6))),
% 63.42/63.68 inference(scs_inference,[],[211,2])).
% 63.42/63.68 cnf(214,plain,
% 63.42/63.68 (E(f2(f2(f5(x2141,f3(x2141)),a6),a6),f2(f1(f1(a9)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,210,211,2,3])).
% 63.42/63.68 cnf(216,plain,
% 63.42/63.68 (E(f2(f1(f1(a9)),a6),f2(f2(f5(x2161,f3(x2161)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[214,2])).
% 63.42/63.68 cnf(217,plain,
% 63.42/63.68 (E(f2(f2(f5(f1(x2171),f1(x2172)),a6),a6),f2(f1(f5(x2171,x2172)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,213,214,2,3])).
% 63.42/63.68 cnf(219,plain,
% 63.42/63.68 (E(f2(f1(f5(x2191,x2192)),a6),f2(f2(f5(f1(x2191),f1(x2192)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[217,2])).
% 63.42/63.68 cnf(220,plain,
% 63.42/63.68 (E(f2(f2(f1(x2201),f1(x2202)),a6),f2(f1(f2(x2202,x2201)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,81,217,2,3])).
% 63.42/63.68 cnf(222,plain,
% 63.42/63.68 (E(f2(f1(f2(x2221,x2222)),a6),f2(f2(f1(x2222),f1(x2221)),a6))),
% 63.42/63.68 inference(scs_inference,[],[220,2])).
% 63.42/63.68 cnf(223,plain,
% 63.42/63.68 (E(f2(a10,a6),f3(f5(f3(x2231),f3(f3(x2231)))))),
% 63.42/63.68 inference(scs_inference,[],[13,93,220,2,3])).
% 63.42/63.68 cnf(225,plain,
% 63.42/63.68 (E(f3(f5(f3(x2251),f3(f3(x2251)))),f2(a10,a6))),
% 63.42/63.68 inference(scs_inference,[],[223,2])).
% 63.42/63.68 cnf(226,plain,
% 63.42/63.68 (E(f2(f2(f1(f2(x2261,x2262)),a6),a6),f2(f2(f1(x2262),f1(x2261)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,222,223,2,3])).
% 63.42/63.68 cnf(229,plain,
% 63.42/63.68 (E(f2(f3(f5(f3(x2291),f3(f3(x2291)))),a6),f2(a10,a6))),
% 63.42/63.68 inference(scs_inference,[],[13,225,226,2,3])).
% 63.42/63.68 cnf(232,plain,
% 63.42/63.68 (E(f2(a9,a6),f5(x2321,f5(x2322,f3(f5(x2321,x2322)))))),
% 63.42/63.68 inference(scs_inference,[],[13,108,229,2,3])).
% 63.42/63.68 cnf(234,plain,
% 63.42/63.68 (E(f5(x2341,f5(x2342,f3(f5(x2341,x2342)))),f2(a9,a6))),
% 63.42/63.68 inference(scs_inference,[],[232,2])).
% 63.42/63.68 cnf(235,plain,
% 63.42/63.68 (E(f2(f3(x2351),a6),f5(f2(f1(x2352),f3(f2(x2352,x2351))),f3(x2351)))),
% 63.42/63.68 inference(scs_inference,[],[13,34,232,2,3])).
% 63.42/63.68 cnf(237,plain,
% 63.42/63.68 (E(f5(f2(f1(x2371),f3(f2(x2371,x2372))),f3(x2372)),f2(f3(x2372),a6))),
% 63.42/63.68 inference(scs_inference,[],[235,2])).
% 63.42/63.68 cnf(238,plain,
% 63.42/63.68 (E(f2(f5(x2381,f5(x2382,f3(f5(x2381,x2382)))),a6),f2(a9,a6))),
% 63.42/63.68 inference(scs_inference,[],[13,234,235,2,3])).
% 63.42/63.68 cnf(241,plain,
% 63.42/63.68 (E(f2(f5(f2(f1(x2411),f3(f2(x2411,x2412))),f3(x2412)),a6),f2(f3(x2412),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,237,238,2,3])).
% 63.42/63.68 cnf(243,plain,
% 63.42/63.68 (E(f2(f3(x2431),a6),f2(f5(f2(f1(x2432),f3(f2(x2432,x2431))),f3(x2431)),a6))),
% 63.42/63.68 inference(scs_inference,[],[241,2])).
% 63.42/63.68 cnf(244,plain,
% 63.42/63.68 (E(f2(f1(f5(x2441,x2442)),a6),f5(f1(x2441),f1(x2442)))),
% 63.42/63.68 inference(scs_inference,[],[13,45,241,2,3])).
% 63.42/63.68 cnf(246,plain,
% 63.42/63.68 (E(f5(f1(x2461),f1(x2462)),f2(f1(f5(x2461,x2462)),a6))),
% 63.42/63.68 inference(scs_inference,[],[244,2])).
% 63.42/63.68 cnf(247,plain,
% 63.42/63.68 (E(f2(f2(f3(x2471),a6),a6),f2(f5(f2(f1(x2472),f3(f2(x2472,x2471))),f3(x2471)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,243,244,2,3])).
% 63.42/63.68 cnf(250,plain,
% 63.42/63.68 (E(f2(f2(x2501,f2(x2502,x2503)),a6),f2(f2(x2501,x2502),x2503))),
% 63.42/63.68 inference(scs_inference,[],[13,64,247,2,3])).
% 63.42/63.68 cnf(252,plain,
% 63.42/63.68 (E(f2(f2(x2521,x2522),x2523),f2(f2(x2521,f2(x2522,x2523)),a6))),
% 63.42/63.68 inference(scs_inference,[],[250,2])).
% 63.42/63.68 cnf(253,plain,
% 63.42/63.68 (E(f2(f5(f2(f1(x2531),f3(f2(x2531,x2532))),f3(x2532)),a6),f1(f1(f3(x2532))))),
% 63.42/63.68 inference(scs_inference,[],[13,40,250,2,3])).
% 63.42/63.68 cnf(256,plain,
% 63.42/63.68 (E(f2(f2(f2(x2561,x2562),x2563),a6),f2(f2(x2561,f2(x2562,x2563)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,252,253,2,3])).
% 63.42/63.68 cnf(258,plain,
% 63.42/63.68 (E(f2(f2(x2581,f2(x2582,x2583)),a6),f2(f2(f2(x2581,x2582),x2583),a6))),
% 63.42/63.68 inference(scs_inference,[],[256,2])).
% 63.42/63.68 cnf(259,plain,
% 63.42/63.68 (E(f2(f5(f5(x2591,x2592),x2593),a6),f5(f2(x2591,a6),f2(f5(x2592,x2593),a6)))),
% 63.42/63.68 inference(scs_inference,[],[13,68,256,2,3])).
% 63.42/63.68 cnf(261,plain,
% 63.42/63.68 (E(f5(f2(x2611,a6),f2(f5(x2612,x2613),a6)),f2(f5(f5(x2611,x2612),x2613),a6))),
% 63.42/63.68 inference(scs_inference,[],[259,2])).
% 63.42/63.68 cnf(262,plain,
% 63.42/63.68 (E(f2(f2(f2(x2621,f2(x2622,x2623)),a6),a6),f2(f2(f2(x2621,x2622),x2623),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,258,259,2,3])).
% 63.42/63.68 cnf(264,plain,
% 63.42/63.68 (E(f2(f2(f2(x2641,x2642),x2643),a6),f2(f2(f2(x2641,f2(x2642,x2643)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[262,2])).
% 63.42/63.68 cnf(265,plain,
% 63.42/63.68 (E(f2(f5(f2(x2651,a6),f2(f5(x2652,x2653),a6)),a6),f2(f5(f5(x2651,x2652),x2653),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,261,262,2,3])).
% 63.42/63.68 cnf(267,plain,
% 63.42/63.68 (E(f2(f5(f5(x2671,x2672),x2673),a6),f2(f5(f2(x2671,a6),f2(f5(x2672,x2673),a6)),a6))),
% 63.42/63.68 inference(scs_inference,[],[265,2])).
% 63.42/63.68 cnf(268,plain,
% 63.42/63.68 (E(f2(a9,a6),f5(x2681,f3(x2681)))),
% 63.42/63.68 inference(scs_inference,[],[13,71,265,2,3])).
% 63.42/63.68 cnf(270,plain,
% 63.42/63.68 (E(f5(x2701,f3(x2701)),f2(a9,a6))),
% 63.42/63.68 inference(scs_inference,[],[268,2])).
% 63.42/63.68 cnf(271,plain,
% 63.42/63.68 (E(f2(f5(x2711,f5(x2712,x2713)),a6),f5(f5(x2711,x2712),x2713))),
% 63.42/63.68 inference(scs_inference,[],[13,61,268,2,3])).
% 63.42/63.68 cnf(273,plain,
% 63.42/63.68 (E(f5(f5(x2731,x2732),x2733),f2(f5(x2731,f5(x2732,x2733)),a6))),
% 63.42/63.68 inference(scs_inference,[],[271,2])).
% 63.42/63.68 cnf(274,plain,
% 63.42/63.68 (E(f2(f5(x2741,f3(x2741)),a6),f2(a9,a6))),
% 63.42/63.68 inference(scs_inference,[],[13,270,271,2,3])).
% 63.42/63.68 cnf(276,plain,
% 63.42/63.68 (E(f2(a9,a6),f2(f5(x2761,f3(x2761)),a6))),
% 63.42/63.68 inference(scs_inference,[],[274,2])).
% 63.42/63.68 cnf(277,plain,
% 63.42/63.68 (E(f2(f5(f5(x2771,x2772),x2773),a6),f2(f5(x2771,f5(x2772,x2773)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,273,274,2,3])).
% 63.42/63.68 cnf(279,plain,
% 63.42/63.68 (E(f2(f5(x2791,f5(x2792,x2793)),a6),f2(f5(f5(x2791,x2792),x2793),a6))),
% 63.42/63.68 inference(scs_inference,[],[277,2])).
% 63.42/63.68 cnf(280,plain,
% 63.42/63.68 (E(f2(f2(a9,a6),a6),f2(f5(x2801,f3(x2801)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,276,277,2,3])).
% 63.42/63.68 cnf(282,plain,
% 63.42/63.68 (E(f2(f5(x2821,f3(x2821)),a6),f2(f2(a9,a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[280,2])).
% 63.42/63.68 cnf(283,plain,
% 63.42/63.68 (E(f2(f2(f5(x2831,f5(x2832,x2833)),a6),a6),f2(f5(f5(x2831,x2832),x2833),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,279,280,2,3])).
% 63.42/63.68 cnf(285,plain,
% 63.42/63.68 (E(f2(f5(f5(x2851,x2852),x2853),a6),f2(f2(f5(x2851,f5(x2852,x2853)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[283,2])).
% 63.42/63.68 cnf(286,plain,
% 63.42/63.68 (E(f2(f2(f5(x2861,f3(x2861)),a6),a6),f2(f2(a9,a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,282,283,2,3])).
% 63.42/63.68 cnf(288,plain,
% 63.42/63.68 (E(f2(f2(a9,a6),a6),f2(f2(f5(x2881,f3(x2881)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[286,2])).
% 63.42/63.68 cnf(289,plain,
% 63.42/63.68 (E(f2(f1(f1(a10)),a6),f3(f5(f3(x2891),f3(f3(x2891)))))),
% 63.42/63.68 inference(scs_inference,[],[13,115,286,2,3])).
% 63.42/63.68 cnf(292,plain,
% 63.42/63.68 (E(f2(f2(f2(a9,a6),a6),a6),f2(f2(f5(x2921,f3(x2921)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,288,289,2,3])).
% 63.42/63.68 cnf(294,plain,
% 63.42/63.68 (E(f2(f2(f5(x2941,f3(x2941)),a6),a6),f2(f2(f2(a9,a6),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[292,2])).
% 63.42/63.68 cnf(295,plain,
% 63.42/63.68 (E(f2(f1(f1(a9)),a6),f5(x2951,f5(x2952,f3(f5(x2951,x2952)))))),
% 63.42/63.68 inference(scs_inference,[],[13,118,292,2,3])).
% 63.42/63.68 cnf(297,plain,
% 63.42/63.68 (E(f5(x2971,f5(x2972,f3(f5(x2971,x2972)))),f2(f1(f1(a9)),a6))),
% 63.42/63.68 inference(scs_inference,[],[295,2])).
% 63.42/63.68 cnf(298,plain,
% 63.42/63.68 (E(f2(f2(a9,a6),a6),f1(f1(f5(x2981,f3(x2981)))))),
% 63.42/63.68 inference(scs_inference,[],[13,295,190,2,3])).
% 63.42/63.68 cnf(300,plain,
% 63.42/63.68 (E(f1(f1(f5(x3001,f3(x3001)))),f2(f2(a9,a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[298,2])).
% 63.42/63.68 cnf(301,plain,
% 63.42/63.68 (E(f2(f2(f2(a9,a6),a6),a6),f1(f1(f5(x3011,f3(x3011)))))),
% 63.42/63.68 inference(scs_inference,[],[13,298,2,3])).
% 63.42/63.68 cnf(303,plain,
% 63.42/63.68 (E(f1(f1(f5(x3031,f3(x3031)))),f2(f2(f2(a9,a6),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[301,2])).
% 63.42/63.68 cnf(304,plain,
% 63.42/63.68 (E(f2(f5(x3041,f5(x3042,f3(f5(x3041,x3042)))),a6),a9)),
% 63.42/63.68 inference(scs_inference,[],[13,301,105,2,3])).
% 63.42/63.68 cnf(307,plain,
% 63.42/63.68 (E(f2(f1(f1(f5(x3071,f3(x3071)))),a6),a9)),
% 63.42/63.68 inference(scs_inference,[],[13,160,304,2,3])).
% 63.42/63.68 cnf(310,plain,
% 63.42/63.68 (E(f2(f5(f2(x3101,f2(x3102,x3103)),f2(x3104,f2(x3102,x3103))),a6),f2(f2(f5(x3101,x3104),x3102),x3103))),
% 63.42/63.68 inference(scs_inference,[],[13,307,82,2,3])).
% 63.42/63.68 cnf(312,plain,
% 63.42/63.68 (E(f2(f2(f5(x3121,x3122),x3123),x3124),f2(f5(f2(x3121,f2(x3123,x3124)),f2(x3122,f2(x3123,x3124))),a6))),
% 63.42/63.68 inference(scs_inference,[],[310,2])).
% 63.42/63.68 cnf(313,plain,
% 63.42/63.68 (E(f2(f2(a9,a6),a6),f5(x3131,f3(x3131)))),
% 63.42/63.68 inference(scs_inference,[],[13,310,268,2,3])).
% 63.42/63.68 cnf(315,plain,
% 63.42/63.68 (E(f5(x3151,f3(x3151)),f2(f2(a9,a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[313,2])).
% 63.42/63.68 cnf(316,plain,
% 63.42/63.68 (E(f2(f2(f2(a9,a6),a6),a6),f5(x3161,f3(x3161)))),
% 63.42/63.68 inference(scs_inference,[],[13,313,2,3])).
% 63.42/63.68 cnf(318,plain,
% 63.42/63.68 (E(f5(x3181,f3(x3181)),f2(f2(f2(a9,a6),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[316,2])).
% 63.42/63.68 cnf(319,plain,
% 63.42/63.68 (E(f2(f2(f2(f2(a9,a6),a6),a6),a6),f5(x3191,f3(x3191)))),
% 63.42/63.68 inference(scs_inference,[],[13,316,2,3])).
% 63.42/63.68 cnf(321,plain,
% 63.42/63.68 (E(f5(x3211,f3(x3211)),f2(f2(f2(f2(a9,a6),a6),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[319,2])).
% 63.42/63.68 cnf(322,plain,
% 63.42/63.68 (E(f2(f5(x3221,f3(x3221)),a6),f2(f2(f2(a9,a6),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,318,319,2,3])).
% 63.42/63.68 cnf(325,plain,
% 63.42/63.68 (E(f2(f5(x3251,f3(x3251)),a6),f2(f2(f2(f2(a9,a6),a6),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,321,322,2,3])).
% 63.42/63.68 cnf(327,plain,
% 63.42/63.68 (E(f2(f2(f2(f2(a9,a6),a6),a6),a6),f2(f5(x3271,f3(x3271)),a6))),
% 63.42/63.68 inference(scs_inference,[],[325,2])).
% 63.42/63.68 cnf(328,plain,
% 63.42/63.68 (E(f2(f2(a9,a6),a6),f5(x3281,f5(x3282,f3(f5(x3281,x3282)))))),
% 63.42/63.68 inference(scs_inference,[],[13,325,232,2,3])).
% 63.42/63.68 cnf(330,plain,
% 63.42/63.68 (E(f5(x3301,f5(x3302,f3(f5(x3301,x3302)))),f2(f2(a9,a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[328,2])).
% 63.42/63.68 cnf(331,plain,
% 63.42/63.68 (E(f2(f2(f2(a9,a6),a6),a6),f5(x3311,f5(x3312,f3(f5(x3311,x3312)))))),
% 63.42/63.68 inference(scs_inference,[],[13,328,2,3])).
% 63.42/63.68 cnf(333,plain,
% 63.42/63.68 (E(f5(x3331,f5(x3332,f3(f5(x3331,x3332)))),f2(f2(f2(a9,a6),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[331,2])).
% 63.42/63.68 cnf(334,plain,
% 63.42/63.68 (E(f2(f5(f2(x3341,a6),f2(f5(x3342,x3343),a6)),a6),f5(f5(x3341,x3342),x3343))),
% 63.42/63.68 inference(scs_inference,[],[13,331,65,2,3])).
% 63.42/63.68 cnf(336,plain,
% 63.42/63.68 (E(f5(f5(x3361,x3362),x3363),f2(f5(f2(x3361,a6),f2(f5(x3362,x3363),a6)),a6))),
% 63.42/63.68 inference(scs_inference,[],[334,2])).
% 63.42/63.68 cnf(337,plain,
% 63.42/63.68 (E(f2(f2(f3(x3371),a6),a6),f5(f2(f1(x3372),f3(f2(x3372,x3371))),f3(x3371)))),
% 63.42/63.68 inference(scs_inference,[],[13,334,235,2,3])).
% 63.42/63.68 cnf(340,plain,
% 63.42/63.68 (E(f2(f2(f2(f3(x3401),a6),a6),a6),f5(f2(f1(x3402),f3(f2(x3402,x3401))),f3(x3401)))),
% 63.42/63.68 inference(scs_inference,[],[13,337,2,3])).
% 63.42/63.68 cnf(342,plain,
% 63.42/63.68 (E(f5(f2(f1(x3421),f3(f2(x3421,x3422))),f3(x3422)),f2(f2(f2(f3(x3422),a6),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[340,2])).
% 63.42/63.68 cnf(343,plain,
% 63.42/63.68 (E(f2(f2(f5(f1(x3431),f1(x3432)),a6),a6),f1(f5(x3431,x3432)))),
% 63.42/63.68 inference(scs_inference,[],[13,340,56,2,3])).
% 63.42/63.68 cnf(346,plain,
% 63.42/63.68 (E(f2(f2(f1(f2(x3461,x3462)),a6),a6),f2(f1(x3462),f1(x3461)))),
% 63.42/63.68 inference(scs_inference,[],[13,343,79,2,3])).
% 63.42/63.68 cnf(349,plain,
% 63.42/63.68 (E(f2(f1(f1(a9)),a6),f5(x3491,f3(x3491)))),
% 63.42/63.68 inference(scs_inference,[],[13,346,130,2,3])).
% 63.42/63.68 cnf(351,plain,
% 63.42/63.68 (E(f5(x3511,f3(x3511)),f2(f1(f1(a9)),a6))),
% 63.42/63.68 inference(scs_inference,[],[349,2])).
% 63.42/63.68 cnf(352,plain,
% 63.42/63.68 (E(f2(f2(f1(f1(a9)),a6),a6),f5(x3521,f3(x3521)))),
% 63.42/63.68 inference(scs_inference,[],[13,349,2,3])).
% 63.42/63.68 cnf(354,plain,
% 63.42/63.68 (E(f5(x3541,f3(x3541)),f2(f2(f1(f1(a9)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[352,2])).
% 63.42/63.68 cnf(355,plain,
% 63.42/63.68 (E(f2(f2(f1(f5(x3551,x3552)),a6),a6),f5(f1(x3551),f1(x3552)))),
% 63.42/63.68 inference(scs_inference,[],[13,352,244,2,3])).
% 63.42/63.68 cnf(357,plain,
% 63.42/63.68 (E(f5(f1(x3571),f1(x3572)),f2(f2(f1(f5(x3571,x3572)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[355,2])).
% 63.42/63.68 cnf(358,plain,
% 63.42/63.68 (E(f2(f5(x3581,f3(x3581)),a6),f2(f2(f1(f1(a9)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,354,355,2,3])).
% 63.42/63.68 cnf(360,plain,
% 63.42/63.68 (E(f2(f2(f1(f1(a9)),a6),a6),f2(f5(x3601,f3(x3601)),a6))),
% 63.42/63.68 inference(scs_inference,[],[358,2])).
% 63.42/63.68 cnf(361,plain,
% 63.42/63.68 (E(f2(f5(f1(x3611),f1(x3612)),a6),f2(f2(f1(f5(x3611,x3612)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,357,358,2,3])).
% 63.42/63.68 cnf(363,plain,
% 63.42/63.68 (E(f2(f2(f1(f5(x3631,x3632)),a6),a6),f2(f5(f1(x3631),f1(x3632)),a6))),
% 63.42/63.68 inference(scs_inference,[],[361,2])).
% 63.42/63.68 cnf(364,plain,
% 63.42/63.68 (E(f2(f2(f2(x3641,f2(x3642,x3643)),a6),a6),f2(f2(x3641,x3642),x3643))),
% 63.42/63.68 inference(scs_inference,[],[13,361,250,2,3])).
% 63.42/63.68 cnf(366,plain,
% 63.42/63.68 (E(f2(f2(x3661,x3662),x3663),f2(f2(f2(x3661,f2(x3662,x3663)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[364,2])).
% 63.42/63.68 cnf(367,plain,
% 63.42/63.68 (E(f2(f2(f5(x3671,f5(x3672,x3673)),a6),a6),f5(f5(x3671,x3672),x3673))),
% 63.42/63.68 inference(scs_inference,[],[13,364,271,2,3])).
% 63.42/63.68 cnf(369,plain,
% 63.42/63.68 (E(f5(f5(x3691,x3692),x3693),f2(f2(f5(x3691,f5(x3692,x3693)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[367,2])).
% 63.42/63.68 cnf(370,plain,
% 63.42/63.68 (E(f2(f2(f5(x3701,f3(x3701)),a6),a6),f2(a9,a6))),
% 63.42/63.68 inference(scs_inference,[],[13,367,274,2,3])).
% 63.42/63.68 cnf(372,plain,
% 63.42/63.68 (E(f2(a9,a6),f2(f2(f5(x3721,f3(x3721)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[370,2])).
% 63.42/63.68 cnf(373,plain,
% 63.42/63.68 (E(f2(f2(f2(f5(x3731,f3(x3731)),a6),a6),a6),f2(a9,a6))),
% 63.42/63.68 inference(scs_inference,[],[13,370,2,3])).
% 63.42/63.68 cnf(376,plain,
% 63.42/63.68 (E(f2(f2(f5(f5(x3761,x3762),x3763),a6),a6),f5(f2(x3761,a6),f2(f5(x3762,x3763),a6)))),
% 63.42/63.68 inference(scs_inference,[],[13,373,259,2,3])).
% 63.42/63.68 cnf(379,plain,
% 63.42/63.68 (E(f2(f2(f5(f2(f1(x3791),f3(f2(x3791,x3792))),f3(x3792)),a6),a6),f2(f3(x3792),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,376,241,2,3])).
% 63.42/63.68 cnf(381,plain,
% 63.42/63.68 (E(f2(f3(x3811),a6),f2(f2(f5(f2(f1(x3812),f3(f2(x3812,x3811))),f3(x3811)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[379,2])).
% 63.42/63.68 cnf(382,plain,
% 63.42/63.68 (E(f2(f2(f5(x3821,f3(x3821)),a6),a6),f1(f1(a9)))),
% 63.42/63.68 inference(scs_inference,[],[13,379,202,2,3])).
% 63.42/63.68 cnf(384,plain,
% 63.42/63.68 (E(f1(f1(a9)),f2(f2(f5(x3841,f3(x3841)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[382,2])).
% 63.42/63.68 cnf(385,plain,
% 63.42/63.68 (E(f2(f2(f2(f1(x3851),f1(x3852)),a6),a6),f2(f1(f2(x3852,x3851)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,382,220,2,3])).
% 63.42/63.68 cnf(387,plain,
% 63.42/63.68 (E(f2(f1(f2(x3871,x3872)),a6),f2(f2(f2(f1(x3872),f1(x3871)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[385,2])).
% 63.42/63.68 cnf(388,plain,
% 63.42/63.68 (E(f2(f2(f2(f2(x3881,x3882),x3883),a6),a6),f2(f2(x3881,f2(x3882,x3883)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,385,256,2,3])).
% 63.42/63.68 cnf(390,plain,
% 63.42/63.68 (E(f2(f2(x3901,f2(x3902,x3903)),a6),f2(f2(f2(f2(x3901,x3902),x3903),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[388,2])).
% 63.42/63.68 cnf(391,plain,
% 63.42/63.68 (E(f2(f2(f5(f5(x3911,x3912),x3913),a6),a6),f2(f5(x3911,f5(x3912,x3913)),a6))),
% 63.42/63.68 inference(scs_inference,[],[13,388,277,2,3])).
% 63.42/63.68 cnf(393,plain,
% 63.42/63.68 (E(f2(f5(x3931,f5(x3932,x3933)),a6),f2(f2(f5(f5(x3931,x3932),x3933),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[391,2])).
% 63.42/63.68 cnf(394,plain,
% 63.42/63.68 (E(f2(f2(a10,a6),a6),f3(f5(f3(x3941),f3(f3(x3941)))))),
% 63.42/63.68 inference(scs_inference,[],[13,391,223,2,3])).
% 63.42/63.68 cnf(397,plain,
% 63.42/63.68 (E(f2(f2(f2(a10,a6),a6),a6),f3(f5(f3(x3971),f3(f3(x3971)))))),
% 63.42/63.68 inference(scs_inference,[],[13,394,2,3])).
% 63.42/63.68 cnf(400,plain,
% 63.42/63.68 (E(f2(a9,a6),f5(f2(x4001,a6),f2(f5(x4002,f3(f5(x4001,x4002))),a6)))),
% 63.42/63.68 inference(scs_inference,[],[13,397,75,2,3])).
% 63.42/63.68 cnf(402,plain,
% 63.42/63.68 (E(f5(f2(x4021,a6),f2(f5(x4022,f3(f5(x4021,x4022))),a6)),f2(a9,a6))),
% 63.42/63.68 inference(scs_inference,[],[400,2])).
% 63.42/63.68 cnf(403,plain,
% 63.42/63.68 (E(f2(f1(f1(f3(x4031))),a6),f5(f2(f1(x4032),f3(f2(x4032,x4031))),f3(x4031)))),
% 63.42/63.68 inference(scs_inference,[],[13,400,38,2,3])).
% 63.42/63.68 cnf(406,plain,
% 63.42/63.68 (E(f2(f1(f5(x4061,x4062)),a6),f5(f2(f1(x4061),a6),f2(f1(x4062),a6)))),
% 63.42/63.68 inference(scs_inference,[],[13,403,50,2,3])).
% 63.42/63.68 cnf(408,plain,
% 63.42/63.68 (E(f5(f2(f1(x4081),a6),f2(f1(x4082),a6)),f2(f1(f5(x4081,x4082)),a6))),
% 63.42/63.68 inference(scs_inference,[],[406,2])).
% 63.42/63.68 cnf(409,plain,
% 63.42/63.68 (E(f2(f2(f1(f5(x4091,x4092)),a6),a6),f5(f2(f1(x4091),a6),f2(f1(x4092),a6)))),
% 63.42/63.68 inference(scs_inference,[],[13,406,2,3])).
% 63.42/63.68 cnf(411,plain,
% 63.42/63.68 (E(f5(f2(f1(x4111),a6),f2(f1(x4112),a6)),f2(f2(f1(f5(x4111,x4112)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[409,2])).
% 63.42/63.68 cnf(412,plain,
% 63.42/63.68 (E(f2(f3(f5(f3(x4121),f3(f3(x4121)))),a6),a10)),
% 63.42/63.68 inference(scs_inference,[],[13,409,18,2,3])).
% 63.42/63.68 cnf(415,plain,
% 63.42/63.68 (E(f2(f5(f2(f1(x4151),f3(f2(x4151,x4152))),f3(x4152)),a6),f3(x4152))),
% 63.42/63.68 inference(scs_inference,[],[13,412,22,2,3])).
% 63.42/63.68 cnf(418,plain,
% 63.42/63.68 (E(f2(f2(f5(f2(f1(x4181),f3(f2(x4181,x4182))),f3(x4182)),a6),a6),f3(x4182))),
% 63.42/63.68 inference(scs_inference,[],[13,415,2,3])).
% 63.42/63.68 cnf(420,plain,
% 63.42/63.68 (E(f3(x4201),f2(f2(f5(f2(f1(x4202),f3(f2(x4202,x4201))),f3(x4201)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[418,2])).
% 63.42/63.68 cnf(421,plain,
% 63.42/63.68 (E(f2(f2(f1(x4211),f1(x4212)),a6),f1(f2(x4212,x4211)))),
% 63.42/63.68 inference(scs_inference,[],[13,418,17,2,3])).
% 63.42/63.68 cnf(424,plain,
% 63.42/63.68 (E(f2(f2(f2(f1(x4241),f1(x4242)),a6),a6),f1(f2(x4242,x4241)))),
% 63.42/63.68 inference(scs_inference,[],[13,421,2,3])).
% 63.42/63.68 cnf(427,plain,
% 63.42/63.68 (E(f2(f5(f5(x4271,x4272),x4273),a6),f5(x4271,f5(x4272,x4273)))),
% 63.42/63.68 inference(scs_inference,[],[13,424,19,2,3])).
% 63.42/63.68 cnf(429,plain,
% 63.42/63.68 (E(f5(x4291,f5(x4292,x4293)),f2(f5(f5(x4291,x4292),x4293),a6))),
% 63.42/63.68 inference(scs_inference,[],[427,2])).
% 63.42/63.68 cnf(430,plain,
% 63.42/63.68 (E(f2(f2(f5(f5(x4301,x4302),x4303),a6),a6),f5(x4301,f5(x4302,x4303)))),
% 63.42/63.68 inference(scs_inference,[],[13,427,2,3])).
% 63.42/63.68 cnf(432,plain,
% 63.42/63.68 (E(f5(x4321,f5(x4322,x4323)),f2(f2(f5(f5(x4321,x4322),x4323),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[430,2])).
% 63.42/63.68 cnf(433,plain,
% 63.42/63.68 (E(f2(f2(f2(x4331,x4332),x4333),a6),f2(x4331,f2(x4332,x4333)))),
% 63.42/63.68 inference(scs_inference,[],[13,430,20,2,3])).
% 63.42/63.68 cnf(435,plain,
% 63.42/63.68 (E(f2(x4351,f2(x4352,x4353)),f2(f2(f2(x4351,x4352),x4353),a6))),
% 63.42/63.68 inference(scs_inference,[],[433,2])).
% 63.42/63.68 cnf(436,plain,
% 63.42/63.68 (E(f2(f2(f2(f2(x4361,x4362),x4363),a6),a6),f2(x4361,f2(x4362,x4363)))),
% 63.42/63.68 inference(scs_inference,[],[13,433,2,3])).
% 63.42/63.68 cnf(438,plain,
% 63.42/63.68 (E(f2(x4381,f2(x4382,x4383)),f2(f2(f2(f2(x4381,x4382),x4383),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[436,2])).
% 63.42/63.68 cnf(439,plain,
% 63.42/63.68 (E(f2(f5(x4391,f3(x4391)),a6),a9)),
% 63.42/63.68 inference(scs_inference,[],[13,436,14,2,3])).
% 63.42/63.68 cnf(441,plain,
% 63.42/63.68 (E(a9,f2(f5(x4411,f3(x4411)),a6))),
% 63.42/63.68 inference(scs_inference,[],[439,2])).
% 63.42/63.68 cnf(442,plain,
% 63.42/63.68 (E(f2(f2(f5(x4421,f3(x4421)),a6),a6),a9)),
% 63.42/63.68 inference(scs_inference,[],[13,439,2,3])).
% 63.42/63.68 cnf(444,plain,
% 63.42/63.68 (E(a9,f2(f2(f5(x4441,f3(x4441)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[442,2])).
% 63.42/63.68 cnf(450,plain,
% 63.42/63.68 (E(f2(f2(a9,a6),a6),a9)),
% 63.42/63.68 inference(scs_inference,[],[330,108,3,2])).
% 63.42/63.68 cnf(453,plain,
% 63.42/63.68 (E(f2(f1(f1(a9)),a6),a9)),
% 63.42/63.68 inference(scs_inference,[],[351,71,3,2])).
% 63.42/63.68 cnf(459,plain,
% 63.42/63.68 (E(f2(f2(f2(a9,a6),a6),a6),a9)),
% 63.42/63.68 inference(scs_inference,[],[333,108,3,2])).
% 63.42/63.68 cnf(470,plain,
% 63.42/63.68 (E(f2(f5(x4701,f3(x4701)),a6),f5(x4702,f3(x4702)))),
% 63.42/63.68 inference(scs_inference,[],[360,354,3,2])).
% 63.42/63.68 cnf(481,plain,
% 63.42/63.68 (E(f2(f2(f2(f2(x4811,x4812),x4813),x4814),a6),f2(x4811,f2(x4812,f2(x4813,x4814))))),
% 63.42/63.68 inference(scs_inference,[],[435,64,3,2])).
% 63.42/63.68 cnf(498,plain,
% 63.42/63.68 (E(f2(f2(f2(a9,f2(a6,a6)),a6),a6),f5(x4981,f3(x4981)))),
% 63.42/63.68 inference(scs_inference,[],[315,366,3,2])).
% 63.42/63.68 cnf(501,plain,
% 63.42/63.68 (E(a9,f2(f2(f2(a9,f2(a6,a6)),a6),a6))),
% 63.42/63.68 inference(scs_inference,[],[14,498,3,2])).
% 63.42/63.68 cnf(504,plain,
% 63.42/63.68 (E(f2(f5(x5041,f3(x5041)),a6),f2(a9,f2(a6,a6)))),
% 63.42/63.68 inference(scs_inference,[],[438,327,3,2])).
% 63.42/63.68 cnf(507,plain,
% 63.42/63.68 (E(f2(f2(f2(a9,a6),a6),a6),f2(a9,a6))),
% 63.42/63.68 inference(scs_inference,[],[372,294,3,2])).
% 63.42/63.68 cnf(516,plain,
% 63.42/63.68 (E(f2(f2(f2(a9,f2(f2(a6,a6),a6)),a6),a6),a9)),
% 63.42/63.68 inference(scs_inference,[],[501,264,3,2])).
% 63.42/63.68 cnf(518,plain,
% 63.42/63.68 (E(f2(f2(f5(x5181,f3(x5181)),a6),a6),f5(x5182,f3(x5182)))),
% 63.42/63.68 inference(scs_inference,[],[14,444,3,2])).
% 63.42/63.68 cnf(522,plain,
% 63.42/63.68 (E(f5(x5221,f3(x5221)),f5(x5222,f5(x5223,f3(f5(x5222,x5223)))))),
% 63.42/63.68 inference(scs_inference,[],[518,432,3,2])).
% 63.42/63.68 cnf(525,plain,
% 63.42/63.68 (E(f5(x5251,f5(x5252,f3(f5(x5251,x5252)))),f2(f5(x5253,f3(x5253)),a6))),
% 63.42/63.68 inference(scs_inference,[],[522,470,3,2])).
% 63.42/63.68 cnf(528,plain,
% 63.42/63.68 (E(f1(f1(f5(f1(x5281),f1(x5282)))),f5(f2(f1(x5281),a6),f2(f1(x5282),a6)))),
% 63.42/63.68 inference(scs_inference,[],[150,52,3,2])).
% 63.42/63.68 cnf(534,plain,
% 63.42/63.68 (E(f2(f2(f2(f3(x5341),a6),a6),a6),f3(x5341))),
% 63.42/63.68 inference(scs_inference,[],[342,34,3,2])).
% 63.42/63.68 cnf(535,plain,
% 63.42/63.68 (E(f1(f1(f2(f3(x5351),f2(a6,a6)))),f3(x5351))),
% 63.42/63.68 inference(scs_inference,[],[534,171,3])).
% 63.42/63.68 cnf(538,plain,
% 63.42/63.68 (E(f2(a9,f2(f2(f2(a6,a6),a6),a6)),a9)),
% 63.42/63.68 inference(scs_inference,[],[516,435,535,2,3])).
% 63.42/63.68 cnf(540,plain,
% 63.42/63.68 (E(a9,f2(a9,f2(f2(f2(a6,a6),a6),a6)))),
% 63.42/63.68 inference(scs_inference,[],[538,2])).
% 63.42/63.68 cnf(541,plain,
% 63.42/63.68 (E(f2(f2(a9,f2(a6,a6)),a6),a9)),
% 63.42/63.68 inference(scs_inference,[],[516,366,538,2,3])).
% 63.42/63.68 cnf(543,plain,
% 63.42/63.68 (E(a9,f2(f2(a9,f2(a6,a6)),a6))),
% 63.42/63.68 inference(scs_inference,[],[541,2])).
% 63.42/63.69 cnf(544,plain,
% 63.42/63.69 (E(f5(x5441,f3(x5441)),f2(a9,f2(f2(f2(a6,a6),a6),a6)))),
% 63.42/63.69 inference(scs_inference,[],[14,540,541,2,3])).
% 63.42/63.69 cnf(545,plain,
% 63.42/63.69 (E(f2(a9,f2(f2(f2(a6,a6),a6),a6)),f5(x5451,f3(x5451)))),
% 63.42/63.69 inference(scs_inference,[],[544,2])).
% 63.42/63.69 cnf(546,plain,
% 63.42/63.69 (E(f5(x5461,f3(x5461)),f2(f2(a9,f2(a6,a6)),a6))),
% 63.42/63.69 inference(scs_inference,[],[14,543,544,2,3])).
% 63.42/63.69 cnf(547,plain,
% 63.42/63.69 (E(f2(f2(a9,f2(a6,a6)),a6),f5(x5471,f3(x5471)))),
% 63.42/63.69 inference(scs_inference,[],[546,2])).
% 63.42/63.69 cnf(548,plain,
% 63.42/63.69 (E(f2(a9,f2(f2(f2(a6,a6),a6),a6)),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[545,351,546,2,3])).
% 63.42/63.69 cnf(550,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f2(a9,f2(f2(f2(a6,a6),a6),a6)))),
% 63.42/63.69 inference(scs_inference,[],[548,2])).
% 63.42/63.69 cnf(551,plain,
% 63.42/63.69 (E(f1(f1(f2(f2(a9,a6),a6))),f5(x5511,f3(x5511)))),
% 63.42/63.69 inference(scs_inference,[],[547,183,548,2,3])).
% 63.42/63.69 cnf(554,plain,
% 63.42/63.69 (E(f2(f2(x5541,f2(x5542,x5543)),a6),f2(x5541,f2(x5542,f2(x5543,a6))))),
% 63.42/63.69 inference(scs_inference,[],[481,390,551,2,3])).
% 63.42/63.69 cnf(556,plain,
% 63.42/63.69 (E(f2(x5561,f2(x5562,f2(x5563,a6))),f2(f2(x5561,f2(x5562,x5563)),a6))),
% 63.42/63.69 inference(scs_inference,[],[554,2])).
% 63.42/63.69 cnf(557,plain,
% 63.42/63.69 (E(f3(x5571),f2(f5(f2(f2(f1(x5572),f3(f2(x5572,x5571))),f2(a6,a6)),f2(f3(x5571),f2(a6,a6))),a6))),
% 63.42/63.69 inference(scs_inference,[],[312,420,554,2,3])).
% 63.42/63.69 cnf(559,plain,
% 63.42/63.69 (E(f2(f5(f2(f2(f1(x5591),f3(f2(x5591,x5592))),f2(a6,a6)),f2(f3(x5592),f2(a6,a6))),a6),f3(x5592))),
% 63.42/63.69 inference(scs_inference,[],[557,2])).
% 63.42/63.69 cnf(560,plain,
% 63.42/63.69 (E(f2(a9,f2(a6,f2(a6,a6))),f5(x5601,f3(x5601)))),
% 63.42/63.69 inference(scs_inference,[],[556,547,557,2,3])).
% 63.42/63.69 cnf(562,plain,
% 63.42/63.69 (E(f5(x5621,f3(x5621)),f2(a9,f2(a6,f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[560,2])).
% 63.42/63.69 cnf(563,plain,
% 63.42/63.69 (E(f5(f5(x5631,x5632),x5633),f5(f2(x5631,f2(a6,a6)),f2(f5(x5632,x5633),f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[369,85,560,2,3])).
% 63.42/63.69 cnf(565,plain,
% 63.42/63.69 (E(f5(f2(x5651,f2(a6,a6)),f2(f5(x5652,x5653),f2(a6,a6))),f5(f5(x5651,x5652),x5653))),
% 63.42/63.69 inference(scs_inference,[],[563,2])).
% 63.42/63.69 cnf(566,plain,
% 63.42/63.69 (E(f1(f1(f5(x5661,f3(x5661)))),f2(f2(a9,f2(a6,a6)),a6))),
% 63.42/63.69 inference(scs_inference,[],[300,252,563,2,3])).
% 63.42/63.69 cnf(568,plain,
% 63.42/63.69 (E(f2(f2(a9,f2(a6,a6)),a6),f1(f1(f5(x5681,f3(x5681)))))),
% 63.42/63.69 inference(scs_inference,[],[566,2])).
% 63.42/63.69 cnf(569,plain,
% 63.42/63.69 (E(f5(f2(x5691,f2(a6,a6)),f2(f5(x5692,f3(f5(x5691,x5692))),f2(a6,a6))),a9)),
% 63.42/63.69 inference(scs_inference,[],[14,565,566,2,3])).
% 63.42/63.69 cnf(572,plain,
% 63.42/63.69 (E(a9,f5(f2(x5721,f2(a6,a6)),f2(f5(x5722,f3(f5(x5721,x5722))),f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[569,2])).
% 63.42/63.69 cnf(573,plain,
% 63.42/63.69 (E(f2(f2(a9,f2(a6,a6)),a6),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[568,189,569,2,3])).
% 63.42/63.69 cnf(575,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f2(f2(a9,f2(a6,a6)),a6))),
% 63.42/63.69 inference(scs_inference,[],[573,2])).
% 63.42/63.69 cnf(576,plain,
% 63.42/63.69 (E(f5(x5761,f3(x5761)),f5(f2(x5762,f2(a6,a6)),f2(f5(x5763,f3(f5(x5762,x5763))),f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[14,572,573,2,3])).
% 63.42/63.69 cnf(577,plain,
% 63.42/63.69 (E(f5(f2(x5771,f2(a6,a6)),f2(f5(x5772,f3(f5(x5771,x5772))),f2(a6,a6))),f5(x5773,f3(x5773)))),
% 63.42/63.69 inference(scs_inference,[],[576,2])).
% 63.42/63.69 cnf(578,plain,
% 63.42/63.69 (E(f5(x5781,f5(x5782,f3(f5(x5781,x5782)))),f2(f2(a9,f2(a6,a6)),a6))),
% 63.42/63.69 inference(scs_inference,[],[297,575,576,2,3])).
% 63.42/63.69 cnf(579,plain,
% 63.42/63.69 (E(f2(f2(a9,f2(a6,a6)),a6),f5(x5791,f5(x5792,f3(f5(x5791,x5792)))))),
% 63.42/63.69 inference(scs_inference,[],[578,2])).
% 63.42/63.69 cnf(580,plain,
% 63.42/63.69 (E(f5(f2(x5801,f2(a6,a6)),f2(f5(x5802,f3(f5(x5801,x5802))),f2(a6,a6))),f2(a9,f2(a6,f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[577,562,578,2,3])).
% 63.42/63.69 cnf(582,plain,
% 63.42/63.69 (E(f2(a9,f2(a6,f2(a6,a6))),f5(f2(x5821,f2(a6,a6)),f2(f5(x5822,f3(f5(x5821,x5822))),f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[580,2])).
% 63.42/63.69 cnf(583,plain,
% 63.42/63.69 (E(f2(f2(a9,f2(a6,a6)),a6),f1(f1(a9)))),
% 63.42/63.69 inference(scs_inference,[],[579,120,580,2,3])).
% 63.42/63.69 cnf(585,plain,
% 63.42/63.69 (E(f1(f1(a9)),f2(f2(a9,f2(a6,a6)),a6))),
% 63.42/63.69 inference(scs_inference,[],[583,2])).
% 63.42/63.69 cnf(586,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f2(f5(f2(x5861,f2(a6,a6)),f2(f3(x5861),f2(a6,a6))),a6))),
% 63.42/63.69 inference(scs_inference,[],[216,312,583,2,3])).
% 63.42/63.69 cnf(588,plain,
% 63.42/63.69 (E(f2(f5(f2(x5881,f2(a6,a6)),f2(f3(x5881),f2(a6,a6))),a6),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[586,2])).
% 63.42/63.69 cnf(589,plain,
% 63.42/63.69 (E(f5(f2(f2(f1(x5891),f3(f2(x5891,x5892))),f2(a6,a6)),f2(f3(x5892),f2(a6,a6))),f3(x5892))),
% 63.42/63.69 inference(scs_inference,[],[559,31,586,2,3])).
% 63.42/63.69 cnf(592,plain,
% 63.42/63.69 (E(f2(f5(f2(x5921,f2(a6,a6)),f2(f3(x5921),f2(a6,a6))),a6),a9)),
% 63.42/63.69 inference(scs_inference,[],[453,588,589,2,3])).
% 63.42/63.69 cnf(593,plain,
% 63.42/63.69 (E(a9,f2(f5(f2(x5931,f2(a6,a6)),f2(f3(x5931),f2(a6,a6))),a6))),
% 63.42/63.69 inference(scs_inference,[],[592,2])).
% 63.42/63.69 cnf(594,plain,
% 63.42/63.69 (E(f2(f1(x5941),f1(x5942)),f2(f2(f2(f1(x5941),f1(x5942)),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[387,81,592,2,3])).
% 63.42/63.69 cnf(597,plain,
% 63.42/63.69 (E(f5(x5971,f3(x5971)),f2(f5(f2(x5972,f2(a6,a6)),f2(f3(x5972),f2(a6,a6))),a6))),
% 63.42/63.69 inference(scs_inference,[],[14,593,594,2,3])).
% 63.42/63.69 cnf(598,plain,
% 63.42/63.69 (E(f2(f5(f2(x5981,f2(a6,a6)),f2(f3(x5981),f2(a6,a6))),a6),f5(x5982,f3(x5982)))),
% 63.42/63.69 inference(scs_inference,[],[597,2])).
% 63.42/63.69 cnf(599,plain,
% 63.42/63.69 (E(f1(f5(x5991,x5992)),f2(f2(f1(f5(x5991,x5992)),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[357,45,597,2,3])).
% 63.42/63.69 cnf(601,plain,
% 63.42/63.69 (E(f2(f2(f1(f5(x6011,x6012)),a6),a6),f1(f5(x6011,x6012)))),
% 63.42/63.69 inference(scs_inference,[],[599,2])).
% 63.42/63.69 cnf(602,plain,
% 63.42/63.69 (E(f2(f5(f2(x6021,f2(a6,a6)),f2(f3(x6021),f2(a6,a6))),a6),f2(f2(a9,a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[598,315,599,2,3])).
% 63.42/63.69 cnf(604,plain,
% 63.42/63.69 (E(f2(f2(a9,a6),a6),f2(f5(f2(x6041,f2(a6,a6)),f2(f3(x6041),f2(a6,a6))),a6))),
% 63.42/63.69 inference(scs_inference,[],[602,2])).
% 63.42/63.69 cnf(605,plain,
% 63.42/63.69 (E(f1(f1(a9)),f2(f2(f2(a9,a6),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[384,294,602,2,3])).
% 63.42/63.69 cnf(607,plain,
% 63.42/63.69 (E(f2(f2(f2(a9,a6),a6),a6),f1(f1(a9)))),
% 63.42/63.69 inference(scs_inference,[],[605,2])).
% 63.42/63.69 cnf(608,plain,
% 63.42/63.69 (E(f2(f2(a9,a6),a6),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[604,588,605,2,3])).
% 63.42/63.69 cnf(610,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f2(f2(a9,a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[608,2])).
% 63.42/63.69 cnf(611,plain,
% 63.42/63.69 (E(f5(f2(x6111,f2(x6112,x6113)),f2(x6114,f2(x6112,x6113))),f2(f2(f2(f5(x6111,x6114),f2(x6112,x6113)),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[165,264,608,2,3])).
% 63.42/63.69 cnf(613,plain,
% 63.42/63.69 (E(f2(f2(f2(f5(x6131,x6132),f2(x6133,x6134)),a6),a6),f5(f2(x6131,f2(x6133,x6134)),f2(x6132,f2(x6133,x6134))))),
% 63.42/63.69 inference(scs_inference,[],[611,2])).
% 63.42/63.69 cnf(614,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f1(f1(f2(a9,f2(a6,a6)))))),
% 63.42/63.69 inference(scs_inference,[],[610,126,611,2,3])).
% 63.42/63.69 cnf(616,plain,
% 63.42/63.69 (E(f1(f1(f2(a9,f2(a6,a6)))),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[614,2])).
% 63.42/63.69 cnf(617,plain,
% 63.42/63.69 (E(f1(f1(a9)),f2(f2(f2(f2(a9,a6),a6),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[585,390,614,2,3])).
% 63.42/63.69 cnf(620,plain,
% 63.42/63.69 (E(f2(a9,f2(a6,a6)),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[616,96,617,2,3])).
% 63.42/63.69 cnf(622,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f2(a9,f2(a6,a6)))),
% 63.42/63.69 inference(scs_inference,[],[620,2])).
% 63.42/63.69 cnf(623,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f2(f2(f2(a9,a6),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[575,258,620,2,3])).
% 63.42/63.69 cnf(625,plain,
% 63.42/63.69 (E(f2(f2(f2(a9,a6),a6),a6),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[623,2])).
% 63.42/63.69 cnf(626,plain,
% 63.42/63.69 (E(f5(x6261,f5(x6262,f3(f5(x6261,x6262)))),f2(a9,f2(a6,a6)))),
% 63.42/63.69 inference(scs_inference,[],[622,297,623,2,3])).
% 63.42/63.69 cnf(627,plain,
% 63.42/63.69 (E(f2(a9,f2(a6,a6)),f5(x6271,f5(x6272,f3(f5(x6271,x6272)))))),
% 63.42/63.69 inference(scs_inference,[],[626,2])).
% 63.42/63.69 cnf(628,plain,
% 63.42/63.69 (E(f2(f2(f2(a9,a6),a6),a6),f2(a9,f2(f2(f2(a6,a6),a6),a6)))),
% 63.42/63.69 inference(scs_inference,[],[625,550,626,2,3])).
% 63.42/63.69 cnf(629,plain,
% 63.42/63.69 (E(f2(a9,f2(f2(f2(a6,a6),a6),a6)),f2(f2(f2(a9,a6),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[628,2])).
% 63.42/63.69 cnf(630,plain,
% 63.42/63.69 (E(f2(f5(x6301,f3(x6301)),a6),f1(f1(f2(f2(a9,a6),a6))))),
% 63.42/63.69 inference(scs_inference,[],[504,159,628,2,3])).
% 63.42/63.69 cnf(633,plain,
% 63.42/63.69 (E(f2(a9,f2(f2(f2(a6,a6),a6),a6)),f2(a9,a6))),
% 63.42/63.69 inference(scs_inference,[],[507,629,630,2,3])).
% 63.42/63.69 cnf(634,plain,
% 63.42/63.69 (E(f2(a9,a6),f2(a9,f2(f2(f2(a6,a6),a6),a6)))),
% 63.42/63.69 inference(scs_inference,[],[633,2])).
% 63.42/63.69 cnf(635,plain,
% 63.42/63.69 (E(f2(a9,f2(a6,a6)),f2(a9,a6))),
% 63.42/63.69 inference(scs_inference,[],[627,234,633,2,3])).
% 63.42/63.69 cnf(637,plain,
% 63.42/63.69 (E(f2(a9,a6),f2(a9,f2(a6,a6)))),
% 63.42/63.69 inference(scs_inference,[],[635,2])).
% 63.42/63.69 cnf(638,plain,
% 63.42/63.69 (E(f5(x6381,f3(x6381)),f1(f1(f5(x6382,f3(x6382)))))),
% 63.42/63.69 inference(scs_inference,[],[14,162,635,2,3])).
% 63.42/63.69 cnf(639,plain,
% 63.42/63.69 (E(f1(f1(f5(x6391,f3(x6391)))),f5(x6392,f3(x6392)))),
% 63.42/63.69 inference(scs_inference,[],[638,2])).
% 63.42/63.69 cnf(640,plain,
% 63.42/63.69 (E(f2(a9,a6),f2(f2(f2(f2(a9,a6),a6),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[637,438,638,2,3])).
% 63.42/63.69 cnf(642,plain,
% 63.42/63.69 (E(f2(f2(f2(f2(a9,a6),a6),a6),a6),f2(a9,a6))),
% 63.42/63.69 inference(scs_inference,[],[640,2])).
% 63.42/63.69 cnf(643,plain,
% 63.42/63.69 (E(f1(f1(f5(x6431,f3(x6431)))),f2(a9,f2(a6,f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[639,562,640,2,3])).
% 63.42/63.69 cnf(645,plain,
% 63.42/63.69 (E(f2(a9,f2(a6,f2(a6,a6))),f1(f1(f5(x6451,f3(x6451)))))),
% 63.42/63.69 inference(scs_inference,[],[643,2])).
% 63.42/63.69 cnf(646,plain,
% 63.42/63.69 (E(f2(f3(x6461),a6),f5(f2(f2(f1(x6462),f3(f2(x6462,x6461))),f2(a6,a6)),f2(f3(x6461),f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[381,85,643,2,3])).
% 63.42/63.69 cnf(648,plain,
% 63.42/63.69 (E(f5(f2(f2(f1(x6481),f3(f2(x6481,x6482))),f2(a6,a6)),f2(f3(x6482),f2(a6,a6))),f2(f3(x6482),a6))),
% 63.42/63.69 inference(scs_inference,[],[646,2])).
% 63.42/63.69 cnf(649,plain,
% 63.42/63.69 (E(f2(a9,f2(a6,f2(a6,a6))),f2(f2(a9,a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[645,300,646,2,3])).
% 63.42/63.69 cnf(651,plain,
% 63.42/63.69 (E(f2(f2(a9,a6),a6),f2(a9,f2(a6,f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[649,2])).
% 63.42/63.69 cnf(652,plain,
% 63.42/63.69 (E(f2(a9,a6),f2(f2(f2(a9,f2(f2(a6,a6),a6)),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[634,435,649,2,3])).
% 63.42/63.69 cnf(655,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f2(a9,f2(a6,f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[651,610,652,2,3])).
% 63.42/63.69 cnf(656,plain,
% 63.42/63.69 (E(f2(a9,f2(a6,f2(a6,a6))),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[655,2])).
% 63.42/63.69 cnf(657,plain,
% 63.42/63.69 (E(f2(f2(a9,a6),a6),f5(f2(x6571,f2(a6,a6)),f2(f5(x6572,f3(f5(x6571,x6572))),f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[582,651,655,2,3])).
% 63.42/63.69 cnf(658,plain,
% 63.42/63.69 (E(f5(f2(x6581,f2(a6,a6)),f2(f5(x6582,f3(f5(x6581,x6582))),f2(a6,a6))),f2(f2(a9,a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[657,2])).
% 63.42/63.69 cnf(659,plain,
% 63.42/63.69 (E(f2(f2(f2(f2(a9,a6),a6),a6),a6),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[656,481,657,2,3])).
% 63.42/63.69 cnf(661,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f2(f2(f2(f2(a9,a6),a6),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[659,2])).
% 63.42/63.69 cnf(662,plain,
% 63.42/63.69 (E(f2(f2(f2(f5(x6621,f5(x6622,x6623)),f2(a6,a6)),a6),a6),f5(f5(x6621,x6622),x6623))),
% 63.42/63.69 inference(scs_inference,[],[613,565,659,2,3])).
% 63.42/63.69 cnf(665,plain,
% 63.42/63.69 (E(f5(f5(x6651,x6652),x6653),f2(f2(f2(f5(x6651,f5(x6652,x6653)),f2(a6,a6)),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[662,2])).
% 63.42/63.69 cnf(666,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f2(a9,a6))),
% 63.42/63.69 inference(scs_inference,[],[661,642,662,2,3])).
% 63.42/63.69 cnf(667,plain,
% 63.42/63.69 (E(f2(a9,a6),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[666,2])).
% 63.42/63.69 cnf(668,plain,
% 63.42/63.69 (E(f2(a9,a6),f1(f1(f2(f2(a9,a6),a6))))),
% 63.42/63.69 inference(scs_inference,[],[637,159,666,2,3])).
% 63.42/63.69 cnf(670,plain,
% 63.42/63.69 (E(f1(f1(f2(f2(a9,a6),a6))),f2(a9,a6))),
% 63.42/63.69 inference(scs_inference,[],[668,2])).
% 63.42/63.69 cnf(671,plain,
% 63.42/63.69 (E(f2(a9,a6),f2(f2(a9,f2(a6,a6)),a6))),
% 63.42/63.69 inference(scs_inference,[],[667,575,668,2,3])).
% 63.42/63.69 cnf(672,plain,
% 63.42/63.69 (E(f2(f2(a9,f2(a6,a6)),a6),f2(a9,a6))),
% 63.42/63.69 inference(scs_inference,[],[671,2])).
% 63.42/63.69 cnf(673,plain,
% 63.42/63.69 (E(f1(f1(f2(f2(a9,a6),a6))),f2(f1(f1(a9)),a6))),
% 63.42/63.69 inference(scs_inference,[],[670,667,671,2,3])).
% 63.42/63.69 cnf(674,plain,
% 63.42/63.69 (E(f2(f1(f1(a9)),a6),f1(f1(f2(f2(a9,a6),a6))))),
% 63.42/63.69 inference(scs_inference,[],[673,2])).
% 63.42/63.69 cnf(675,plain,
% 63.42/63.69 (E(f2(f2(a9,f2(a6,a6)),a6),f2(a9,f2(f2(f2(a6,a6),a6),a6)))),
% 63.42/63.69 inference(scs_inference,[],[672,634,673,2,3])).
% 63.42/63.69 cnf(677,plain,
% 63.42/63.69 (E(f2(f2(f2(a9,a6),a6),a6),f1(f1(f2(f2(a9,a6),a6))))),
% 63.42/63.69 inference(scs_inference,[],[674,625,675,2,3])).
% 63.42/63.69 cnf(678,plain,
% 63.42/63.69 (E(f1(f1(f2(f2(a9,a6),a6))),f2(f2(f2(a9,a6),a6),a6))),
% 63.42/63.69 inference(scs_inference,[],[677,2])).
% 63.42/63.69 cnf(679,plain,
% 63.42/63.69 (E(f2(a9,f2(a6,f2(a6,a6))),f1(f1(f2(f2(a9,a6),a6))))),
% 63.42/63.69 inference(scs_inference,[],[674,656,677,2,3])).
% 63.42/63.69 cnf(680,plain,
% 63.42/63.69 (E(f1(f1(f2(f2(a9,a6),a6))),f2(a9,f2(a6,f2(a6,a6))))),
% 63.42/63.69 inference(scs_inference,[],[679,2])).
% 63.42/63.69 cnf(681,plain,
% 63.42/63.69 (E(f1(f1(f2(f2(a9,a6),a6))),a9)),
% 63.58/63.69 inference(scs_inference,[],[678,459,679,2,3])).
% 63.58/63.69 cnf(682,plain,
% 63.58/63.69 (E(a9,f1(f1(f2(f2(a9,a6),a6))))),
% 63.58/63.69 inference(scs_inference,[],[681,2])).
% 63.58/63.69 cnf(683,plain,
% 63.58/63.69 (E(f1(f1(f2(f2(a9,a6),a6))),f1(f1(a9)))),
% 63.58/63.69 inference(scs_inference,[],[607,678,681,2,3])).
% 63.58/63.69 cnf(685,plain,
% 63.58/63.69 (E(f1(f1(f2(a9,f2(a6,a6)))),a9)),
% 63.58/63.69 inference(scs_inference,[],[453,616,683,2,3])).
% 63.58/63.69 cnf(686,plain,
% 63.58/63.69 (E(a9,f1(f1(f2(a9,f2(a6,a6)))))),
% 63.58/63.69 inference(scs_inference,[],[685,2])).
% 63.58/63.69 cnf(687,plain,
% 63.58/63.69 (E(f1(f1(f5(x6871,f3(x6871)))),f2(a9,f2(a6,a6)))),
% 63.58/63.69 inference(scs_inference,[],[622,189,685,2,3])).
% 63.58/63.69 cnf(688,plain,
% 63.58/63.69 (E(f2(a9,f2(a6,a6)),f1(f1(f5(x6881,f3(x6881)))))),
% 63.58/63.69 inference(scs_inference,[],[687,2])).
% 63.58/63.69 cnf(689,plain,
% 63.58/63.69 (E(f5(x6891,f3(x6891)),f1(f1(f2(a9,f2(a6,a6)))))),
% 63.58/63.69 inference(scs_inference,[],[14,686,687,2,3])).
% 63.58/63.69 cnf(690,plain,
% 63.58/63.69 (E(f1(f1(f2(a9,f2(a6,a6)))),f5(x6901,f3(x6901)))),
% 63.58/63.69 inference(scs_inference,[],[689,2])).
% 63.58/63.69 cnf(691,plain,
% 63.58/63.69 (E(f2(a9,f2(a6,a6)),f5(x6911,f3(x6911)))),
% 63.58/63.69 inference(scs_inference,[],[688,639,689,2,3])).
% 63.58/63.69 cnf(693,plain,
% 63.58/63.69 (E(f5(x6931,f3(x6931)),f2(a9,f2(a6,a6)))),
% 63.58/63.69 inference(scs_inference,[],[691,2])).
% 63.58/63.69 cnf(694,plain,
% 63.58/63.69 (E(f1(f1(f2(a9,f2(a6,a6)))),f2(a9,a6))),
% 63.58/63.69 inference(scs_inference,[],[690,270,691,2,3])).
% 63.58/63.69 cnf(697,plain,
% 63.58/63.69 (E(f2(f5(x6971,f3(x6971)),a6),f2(a9,f2(f2(f2(a6,a6),a6),a6)))),
% 63.58/63.69 inference(scs_inference,[],[550,210,694,2,3])).
% 63.58/63.69 cnf(699,plain,
% 63.58/63.69 (E(f5(f2(x6991,f2(a6,a6)),f2(f5(x6992,f3(f5(x6991,x6992))),f2(a6,a6))),f2(f2(a9,f2(a6,a6)),a6))),
% 63.58/63.69 inference(scs_inference,[],[658,252,697,2,3])).
% 63.58/63.69 cnf(701,plain,
% 63.58/63.69 (E(f2(f2(a9,f2(a6,a6)),a6),f5(f2(x7011,f2(a6,a6)),f2(f5(x7012,f3(f5(x7011,x7012))),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[699,2])).
% 63.58/63.69 cnf(702,plain,
% 63.58/63.69 (E(f2(f1(f5(x7021,x7022)),a6),f2(f5(f2(f1(x7021),f2(a6,a6)),f2(f1(x7022),f2(a6,a6))),a6))),
% 63.58/63.69 inference(scs_inference,[],[219,312,699,2,3])).
% 63.58/63.69 cnf(704,plain,
% 63.58/63.69 (E(f2(f5(f2(f1(x7041),f2(a6,a6)),f2(f1(x7042),f2(a6,a6))),a6),f2(f1(f5(x7041,x7042)),a6))),
% 63.58/63.69 inference(scs_inference,[],[702,2])).
% 63.58/63.69 cnf(705,plain,
% 63.58/63.69 (E(f2(f5(f5(x7051,x7052),x7053),a6),f5(f2(x7051,f2(a6,a6)),f2(f5(x7052,x7053),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[285,85,702,2,3])).
% 63.58/63.69 cnf(707,plain,
% 63.58/63.69 (E(f5(f2(x7071,f2(a6,a6)),f2(f5(x7072,x7073),f2(a6,a6))),f2(f5(f5(x7071,x7072),x7073),a6))),
% 63.58/63.69 inference(scs_inference,[],[705,2])).
% 63.58/63.69 cnf(708,plain,
% 63.58/63.69 (E(f5(f2(f1(x7081),f2(a6,a6)),f2(f1(x7082),f2(a6,a6))),f2(f1(f5(x7081,x7082)),a6))),
% 63.58/63.69 inference(scs_inference,[],[704,31,705,2,3])).
% 63.58/63.69 cnf(710,plain,
% 63.58/63.69 (E(f2(f1(f5(x7101,x7102)),a6),f5(f2(f1(x7101),f2(a6,a6)),f2(f1(x7102),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[708,2])).
% 63.58/63.69 cnf(711,plain,
% 63.58/63.69 (E(f2(f2(a9,f2(a6,a6)),a6),f2(f5(f5(x7111,x7112),f3(f5(x7111,x7112))),a6))),
% 63.58/63.69 inference(scs_inference,[],[701,707,708,2,3])).
% 63.58/63.69 cnf(714,plain,
% 63.58/63.69 (E(f1(f1(f5(f1(x7141),f1(x7142)))),f5(f2(f1(x7141),f2(a6,a6)),f2(f1(x7142),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[177,710,711,2,3])).
% 63.58/63.69 cnf(716,plain,
% 63.58/63.69 (E(f5(f2(f1(x7161),f2(a6,a6)),f2(f1(x7162),f2(a6,a6))),f1(f1(f5(f1(x7161),f1(x7162)))))),
% 63.58/63.69 inference(scs_inference,[],[714,2])).
% 63.58/63.69 cnf(717,plain,
% 63.58/63.69 (E(f5(f1(x7171),f1(x7172)),f5(f2(f1(x7171),f2(a6,a6)),f2(f1(x7172),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[246,710,714,2,3])).
% 63.58/63.69 cnf(719,plain,
% 63.58/63.69 (E(f5(f2(f1(x7191),f2(a6,a6)),f2(f1(x7192),f2(a6,a6))),f5(f1(x7191),f1(x7192)))),
% 63.58/63.69 inference(scs_inference,[],[717,2])).
% 63.58/63.69 cnf(720,plain,
% 63.58/63.69 (E(f5(f2(f1(x7201),f2(a6,a6)),f2(f1(x7202),f2(a6,a6))),f5(f2(f1(x7201),a6),f2(f1(x7202),a6)))),
% 63.58/63.69 inference(scs_inference,[],[716,528,717,2,3])).
% 63.58/63.69 cnf(722,plain,
% 63.58/63.69 (E(f5(f2(f1(x7221),a6),f2(f1(x7222),a6)),f5(f2(f1(x7221),f2(a6,a6)),f2(f1(x7222),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[720,2])).
% 63.58/63.69 cnf(723,plain,
% 63.58/63.69 (E(f5(f2(f1(x7231),f2(a6,a6)),f2(f1(x7232),f2(a6,a6))),f1(f1(f1(f5(x7231,x7232)))))),
% 63.58/63.69 inference(scs_inference,[],[123,719,720,2,3])).
% 63.58/63.69 cnf(725,plain,
% 63.58/63.69 (E(f1(f1(f1(f5(x7251,x7252)))),f5(f2(f1(x7251),f2(a6,a6)),f2(f1(x7252),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[723,2])).
% 63.58/63.69 cnf(726,plain,
% 63.58/63.69 (E(f5(f2(f1(x7261),f2(a6,a6)),f2(f1(x7262),f2(a6,a6))),f2(f2(f1(f5(x7261,x7262)),a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[719,357,723,2,3])).
% 63.58/63.69 cnf(729,plain,
% 63.58/63.69 (E(f2(f5(x7291,f5(x7292,x7293)),a6),f2(f5(f2(f5(x7291,x7292),f2(a6,a6)),f2(x7293,f2(a6,a6))),a6))),
% 63.58/63.69 inference(scs_inference,[],[393,312,726,2,3])).
% 63.58/63.69 cnf(732,plain,
% 63.58/63.69 (E(f5(x7321,f3(x7321)),f5(x7322,f3(x7322)))),
% 63.58/63.69 inference(scs_inference,[],[14,71,729,2,3])).
% 63.58/63.69 cnf(736,plain,
% 63.58/63.69 (E(f5(f5(f5(x7361,x7362),x7363),x7364),f5(f2(x7361,a6),f2(f5(x7362,f5(x7363,x7364)),a6)))),
% 63.58/63.69 inference(scs_inference,[],[129,136,3,2])).
% 63.58/63.69 cnf(745,plain,
% 63.58/63.69 (E(f1(f1(a9)),f2(a9,f2(f2(f2(a6,a6),a6),a6)))),
% 63.58/63.69 inference(scs_inference,[],[629,607,3,2])).
% 63.58/63.69 cnf(751,plain,
% 63.58/63.69 (E(f5(f2(x7511,f2(f2(a6,a6),a6)),f2(f5(x7512,x7513),f2(f2(a6,a6),a6))),f5(f5(x7511,x7512),x7513))),
% 63.58/63.69 inference(scs_inference,[],[665,163,3,2])).
% 63.58/63.69 cnf(764,plain,
% 63.58/63.69 (E(f5(f3(x7641),x7641),f2(a9,f2(a6,a6)))),
% 63.58/63.69 inference(scs_inference,[],[15,693,3])).
% 63.58/63.69 cnf(767,plain,
% 63.58/63.69 (E(f2(a9,f2(a6,a6)),f5(f3(x7671),x7671))),
% 63.58/63.69 inference(scs_inference,[],[15,693,3,2])).
% 63.58/63.69 cnf(768,plain,
% 63.58/63.69 (E(f5(x7681,f3(x7681)),f5(f3(x7682),x7682))),
% 63.58/63.69 inference(scs_inference,[],[767,693,3])).
% 63.58/63.69 cnf(771,plain,
% 63.58/63.69 (E(f2(a9,f2(a6,f2(a6,a6))),a9)),
% 63.58/63.69 inference(scs_inference,[],[680,682,3,2])).
% 63.58/63.69 cnf(772,plain,
% 63.58/63.69 (E(f5(f2(f5(x7721,x7722),f2(f2(a6,a6),a6)),f2(x7723,f2(f2(a6,a6),a6))),f5(f5(x7723,x7721),x7722))),
% 63.58/63.69 inference(scs_inference,[],[15,751,3])).
% 63.58/63.69 cnf(774,plain,
% 63.58/63.69 (E(f5(f5(x7741,x7742),x7743),f5(f2(f5(x7742,x7743),f2(f2(a6,a6),a6)),f2(x7741,f2(f2(a6,a6),a6))))),
% 63.58/63.69 inference(scs_inference,[],[772,2])).
% 63.58/63.69 cnf(775,plain,
% 63.58/63.69 (E(f5(f2(f5(x7751,f3(f5(x7752,x7751))),a6),f2(x7752,a6)),f2(a9,a6))),
% 63.58/63.69 inference(scs_inference,[],[15,402,772,2,3])).
% 63.58/63.69 cnf(778,plain,
% 63.58/63.69 (E(f5(x7781,f5(x7782,x7783)),f5(f2(f5(x7783,x7781),f2(f2(a6,a6),a6)),f2(x7782,f2(f2(a6,a6),a6))))),
% 63.58/63.69 inference(scs_inference,[],[15,774,775,2,3])).
% 63.58/63.69 cnf(781,plain,
% 63.58/63.69 (E(f5(f2(f5(x7811,x7812),f2(f2(a6,a6),a6)),f2(x7813,f2(f2(a6,a6),a6))),f5(x7812,f5(x7813,x7811)))),
% 63.58/63.69 inference(scs_inference,[],[778,2])).
% 63.58/63.69 cnf(782,plain,
% 63.58/63.69 (E(f5(f2(f1(x7821),a6),f2(f1(x7822),a6)),f5(f2(f1(x7822),f2(a6,a6)),f2(f1(x7821),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[15,722,778,2,3])).
% 63.58/63.69 cnf(785,plain,
% 63.58/63.69 (E(f5(f2(x7851,f2(f2(a6,a6),a6)),f2(f5(x7852,x7853),f2(f2(a6,a6),a6))),f5(x7853,f5(x7851,x7852)))),
% 63.58/63.69 inference(scs_inference,[],[15,781,782,2,3])).
% 63.58/63.69 cnf(788,plain,
% 63.58/63.69 (E(f5(f2(f1(x7881),a6),f2(f1(x7882),a6)),f1(f1(f1(f5(x7882,x7881)))))),
% 63.58/63.69 inference(scs_inference,[],[15,144,785,2,3])).
% 63.58/63.69 cnf(790,plain,
% 63.58/63.69 (E(f1(f1(f1(f5(x7901,x7902)))),f5(f2(f1(x7902),a6),f2(f1(x7901),a6)))),
% 63.58/63.69 inference(scs_inference,[],[788,2])).
% 63.58/63.69 cnf(791,plain,
% 63.58/63.69 (E(f2(f5(f1(x7911),f1(x7912)),a6),f5(f2(f1(x7911),f2(a6,a6)),f2(f1(x7912),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[725,111,788,2,3])).
% 63.58/63.69 cnf(793,plain,
% 63.58/63.69 (E(f5(f2(f1(x7931),f2(a6,a6)),f2(f1(x7932),f2(a6,a6))),f2(f5(f1(x7931),f1(x7932)),a6))),
% 63.58/63.69 inference(scs_inference,[],[791,2])).
% 63.58/63.69 cnf(794,plain,
% 63.58/63.69 (E(f5(f1(x7941),f1(x7942)),f5(f2(f1(x7942),a6),f2(f1(x7941),a6)))),
% 63.58/63.69 inference(scs_inference,[],[790,123,791,2,3])).
% 63.58/63.69 cnf(797,plain,
% 63.58/63.69 (E(f5(x7971,f5(f5(x7972,x7973),x7974)),f5(f2(x7972,a6),f2(f5(x7973,f5(x7974,x7971)),a6)))),
% 63.58/63.69 inference(scs_inference,[],[15,736,794,2,3])).
% 63.58/63.69 cnf(800,plain,
% 63.58/63.69 (E(f5(f2(x8001,a6),f2(f5(x8002,f5(x8003,x8004)),a6)),f5(x8004,f5(f5(x8001,x8002),x8003)))),
% 63.58/63.69 inference(scs_inference,[],[797,2])).
% 63.58/63.69 cnf(801,plain,
% 63.58/63.69 (E(f5(f2(f3(x8011),f2(a6,a6)),f2(f2(f1(x8012),f3(f2(x8012,x8011))),f2(a6,a6))),f2(f3(x8011),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,648,797,2,3])).
% 63.58/63.69 cnf(804,plain,
% 63.58/63.69 (E(f5(f2(f5(x8041,f5(x8042,x8043)),a6),f2(x8044,a6)),f5(x8043,f5(f5(x8044,x8041),x8042)))),
% 63.58/63.69 inference(scs_inference,[],[15,800,801,2,3])).
% 63.58/63.69 cnf(806,plain,
% 63.58/63.69 (E(f5(x8061,f5(f5(x8062,x8063),x8064)),f5(f2(f5(x8063,f5(x8064,x8061)),a6),f2(x8062,a6)))),
% 63.58/63.69 inference(scs_inference,[],[804,2])).
% 63.58/63.69 cnf(807,plain,
% 63.58/63.69 (E(f5(f5(x8071,f3(f5(x8072,x8071))),x8072),f2(f5(x8073,f3(x8073)),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,525,804,2,3])).
% 63.58/63.69 cnf(811,plain,
% 63.58/63.69 (E(f5(f5(f5(x8111,x8112),x8113),x8114),f5(f2(f5(x8112,f5(x8113,x8114)),a6),f2(x8111,a6)))),
% 63.58/63.69 inference(scs_inference,[],[15,806,807,2,3])).
% 63.58/63.69 cnf(815,plain,
% 63.58/63.69 (E(f5(f2(f1(x8151),f2(a6,a6)),f2(f1(x8152),f2(a6,a6))),f2(f5(f1(x8152),f1(x8151)),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,793,811,2,3])).
% 63.58/63.69 cnf(817,plain,
% 63.58/63.69 (E(f2(f5(f1(x8171),f1(x8172)),a6),f5(f2(f1(x8172),f2(a6,a6)),f2(f1(x8171),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[815,2])).
% 63.58/63.69 cnf(818,plain,
% 63.58/63.69 (E(f5(x8181,f5(x8182,x8183)),f2(f5(f2(x8182,a6),f2(f5(x8183,x8181),a6)),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,336,815,2,3])).
% 63.58/63.69 cnf(821,plain,
% 63.58/63.69 (E(f2(f5(f2(x8211,a6),f2(f5(x8212,x8213),a6)),a6),f5(x8213,f5(x8211,x8212)))),
% 63.58/63.69 inference(scs_inference,[],[818,2])).
% 63.58/63.69 cnf(822,plain,
% 63.58/63.69 (E(f2(f2(f1(f5(x8221,x8222)),a6),a6),f5(f2(f1(x8222),f2(a6,a6)),f2(f1(x8221),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[817,363,818,2,3])).
% 63.58/63.69 cnf(824,plain,
% 63.58/63.69 (E(f5(f2(f1(x8241),f2(a6,a6)),f2(f1(x8242),f2(a6,a6))),f2(f2(f1(f5(x8242,x8241)),a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[822,2])).
% 63.58/63.69 cnf(825,plain,
% 63.58/63.69 (E(f2(f5(f5(x8251,x8252),x8253),a6),f5(x8253,f5(x8251,x8252)))),
% 63.58/63.69 inference(scs_inference,[],[821,267,822,2,3])).
% 63.58/63.69 cnf(828,plain,
% 63.58/63.69 (E(f5(f2(f1(x8281),f2(a6,a6)),f2(f1(x8282),f2(a6,a6))),f1(f5(x8282,x8281)))),
% 63.58/63.69 inference(scs_inference,[],[601,824,825,2,3])).
% 63.58/63.69 cnf(831,plain,
% 63.58/63.69 (E(f5(f2(f1(x8311),a6),f2(f1(x8312),a6)),f2(f1(f5(x8312,x8311)),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,408,828,2,3])).
% 63.58/63.69 cnf(833,plain,
% 63.58/63.69 (E(f2(f1(f5(x8331,x8332)),a6),f5(f2(f1(x8332),a6),f2(f1(x8331),a6)))),
% 63.58/63.69 inference(scs_inference,[],[831,2])).
% 63.58/63.69 cnf(834,plain,
% 63.58/63.69 (E(f5(f2(f1(x8341),a6),f2(f1(x8342),a6)),f2(f2(f1(f5(x8342,x8341)),a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,411,831,2,3])).
% 63.58/63.69 cnf(837,plain,
% 63.58/63.69 (E(f5(f2(f5(x8371,f3(f5(x8372,x8371))),a6),f2(x8372,a6)),a9)),
% 63.58/63.69 inference(scs_inference,[],[15,78,834,2,3])).
% 63.58/63.69 cnf(839,plain,
% 63.58/63.69 (E(a9,f5(f2(f5(x8391,f3(f5(x8392,x8391))),a6),f2(x8392,a6)))),
% 63.58/63.69 inference(scs_inference,[],[837,2])).
% 63.58/63.69 cnf(840,plain,
% 63.58/63.69 (E(f5(f5(x8401,x8402),x8403),f1(f1(f5(f5(x8403,x8401),x8402))))),
% 63.58/63.69 inference(scs_inference,[],[15,156,837,2,3])).
% 63.58/63.69 cnf(843,plain,
% 63.58/63.69 (E(f1(f1(f5(f5(x8431,x8432),x8433))),f5(f5(x8432,x8433),x8431))),
% 63.58/63.69 inference(scs_inference,[],[840,2])).
% 63.58/63.69 cnf(844,plain,
% 63.58/63.69 (E(f2(f2(a9,a6),a6),f5(f2(f5(x8441,f3(f5(x8442,x8441))),a6),f2(x8442,a6)))),
% 63.58/63.69 inference(scs_inference,[],[450,839,840,2,3])).
% 63.58/63.69 cnf(845,plain,
% 63.58/63.69 (E(f5(f2(f5(x8451,f3(f5(x8452,x8451))),a6),f2(x8452,a6)),f2(f2(a9,a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[844,2])).
% 63.58/63.69 cnf(846,plain,
% 63.58/63.69 (E(f2(a9,f2(a6,a6)),f5(f5(x8461,f3(f5(x8462,x8461))),x8462))),
% 63.58/63.69 inference(scs_inference,[],[843,688,844,2,3])).
% 63.58/63.69 cnf(850,plain,
% 63.58/63.69 (E(f2(a9,f2(a6,f2(a6,a6))),f2(f5(x8501,f3(x8501)),a6))),
% 63.58/63.69 inference(scs_inference,[],[771,441,846,2,3])).
% 63.58/63.69 cnf(851,plain,
% 63.58/63.69 (E(f2(f5(x8511,f3(x8511)),a6),f2(a9,f2(a6,f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[850,2])).
% 63.58/63.69 cnf(852,plain,
% 63.58/63.69 (E(f2(a9,f2(a6,f2(a6,a6))),f5(f5(x8521,f3(f5(x8522,x8521))),x8522))),
% 63.58/63.69 inference(scs_inference,[],[843,645,850,2,3])).
% 63.58/63.69 cnf(855,plain,
% 63.58/63.69 (E(f5(f5(x8551,f3(f5(x8552,x8551))),x8552),f2(a9,f2(a6,f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[852,2])).
% 63.58/63.69 cnf(856,plain,
% 63.58/63.69 (E(f5(f3(x8561),x8561),f5(x8562,f5(x8563,f3(f5(x8562,x8563)))))),
% 63.58/63.69 inference(scs_inference,[],[15,522,852,2,3])).
% 63.58/63.69 cnf(859,plain,
% 63.58/63.69 (E(f5(x8591,f5(x8592,f3(f5(x8591,x8592)))),f5(f3(x8593),x8593))),
% 63.58/63.69 inference(scs_inference,[],[856,2])).
% 63.58/63.69 cnf(860,plain,
% 63.58/63.69 (E(f5(x8601,f5(x8602,f3(f5(x8601,x8602)))),f2(a9,f2(a6,f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[15,855,856,2,3])).
% 63.58/63.69 cnf(864,plain,
% 63.58/63.69 (E(f5(f5(x8641,f3(f5(x8642,x8641))),x8642),f5(f3(x8643),x8643))),
% 63.58/63.69 inference(scs_inference,[],[15,859,860,2,3])).
% 63.58/63.69 cnf(867,plain,
% 63.58/63.69 (E(f5(f3(x8671),x8671),f5(f5(x8672,f3(f5(x8673,x8672))),x8673))),
% 63.58/63.69 inference(scs_inference,[],[864,2])).
% 63.58/63.69 cnf(868,plain,
% 63.58/63.69 (E(f5(f2(f5(x8681,f3(f5(x8682,x8681))),f2(a6,a6)),f2(x8682,f2(a6,a6))),f2(f2(a9,a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,658,864,2,3])).
% 63.58/63.69 cnf(871,plain,
% 63.58/63.69 (E(f5(x8711,f3(x8711)),f5(f5(x8712,f3(f5(x8713,x8712))),x8713))),
% 63.58/63.69 inference(scs_inference,[],[15,867,868,2,3])).
% 63.58/63.69 cnf(875,plain,
% 63.58/63.69 (E(f5(f5(x8751,f3(f5(x8752,x8751))),x8752),f2(f2(a9,a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,330,871,2,3])).
% 63.58/63.69 cnf(879,plain,
% 63.58/63.69 (E(f5(f2(f5(x8791,f3(f5(x8792,x8791))),f2(a6,a6)),f2(x8792,f2(a6,a6))),f5(x8793,f3(x8793)))),
% 63.58/63.69 inference(scs_inference,[],[15,577,875,2,3])).
% 63.58/63.69 cnf(881,plain,
% 63.58/63.69 (E(f5(x8811,f3(x8811)),f5(f2(f5(x8812,f3(f5(x8813,x8812))),f2(a6,a6)),f2(x8813,f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[879,2])).
% 63.58/63.69 cnf(882,plain,
% 63.58/63.69 (E(f2(f2(a9,a6),a6),f2(a9,f2(f2(f2(a6,a6),a6),a6)))),
% 63.58/63.69 inference(scs_inference,[],[450,540,879,2,3])).
% 63.58/63.69 cnf(883,plain,
% 63.58/63.69 (E(f2(a9,f2(f2(f2(a6,a6),a6),a6)),f2(f2(a9,a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[882,2])).
% 63.58/63.69 cnf(884,plain,
% 63.58/63.69 (E(f5(f3(x8841),x8841),f5(f2(f5(x8842,f3(f5(x8843,x8842))),f2(a6,a6)),f2(x8843,f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[15,881,882,2,3])).
% 63.58/63.69 cnf(887,plain,
% 63.58/63.69 (E(f5(f2(f5(x8871,f3(f5(x8872,x8871))),f2(a6,a6)),f2(x8872,f2(a6,a6))),f5(f3(x8873),x8873))),
% 63.58/63.69 inference(scs_inference,[],[884,2])).
% 63.58/63.69 cnf(888,plain,
% 63.58/63.69 (E(f1(f1(a9)),f2(f2(a9,a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[883,745,884,2,3])).
% 63.58/63.69 cnf(889,plain,
% 63.58/63.69 (E(f2(f2(a9,a6),a6),f1(f1(a9)))),
% 63.58/63.69 inference(scs_inference,[],[888,2])).
% 63.58/63.69 cnf(890,plain,
% 63.58/63.69 (E(f5(f2(x8901,f2(a6,a6)),f2(f5(x8902,f3(f5(x8901,x8902))),f2(a6,a6))),f5(f3(x8903),x8903))),
% 63.58/63.69 inference(scs_inference,[],[15,887,888,2,3])).
% 63.58/63.69 cnf(893,plain,
% 63.58/63.69 (E(f5(f2(f5(x8931,f3(f5(x8932,x8931))),a6),f2(x8932,a6)),f1(f1(a9)))),
% 63.58/63.69 inference(scs_inference,[],[845,889,890,2,3])).
% 63.58/63.69 cnf(895,plain,
% 63.58/63.69 (E(f5(f5(x8951,f3(f5(x8952,x8951))),x8952),f2(f2(f2(a9,a6),a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,333,893,2,3])).
% 63.58/63.69 cnf(899,plain,
% 63.58/63.69 (E(f5(f3(x8991),x8991),f2(f2(f2(a9,a6),a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,318,895,2,3])).
% 63.58/63.69 cnf(902,plain,
% 63.58/63.69 (E(f2(f2(f2(a9,a6),a6),a6),f5(f3(x9021),x9021))),
% 63.58/63.69 inference(scs_inference,[],[899,2])).
% 63.58/63.69 cnf(903,plain,
% 63.58/63.69 (E(f5(f3(x9031),x9031),f1(f1(f1(f1(a9)))))),
% 63.58/63.69 inference(scs_inference,[],[15,141,899,2,3])).
% 63.58/63.69 cnf(907,plain,
% 63.58/63.69 (E(f1(f1(f5(x9071,f3(x9071)))),f5(f3(x9072),x9072))),
% 63.58/63.69 inference(scs_inference,[],[902,303,903,2,3])).
% 63.58/63.69 cnf(908,plain,
% 63.58/63.69 (E(f5(f3(x9081),x9081),f1(f1(f5(x9082,f3(x9082)))))),
% 63.58/63.69 inference(scs_inference,[],[907,2])).
% 63.58/63.69 cnf(909,plain,
% 63.58/63.69 (E(f5(f3(x9091),x9091),f2(f2(f2(f2(a9,a6),a6),a6),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,321,907,2,3])).
% 63.58/63.69 cnf(912,plain,
% 63.58/63.69 (E(f2(f2(f2(f2(a9,a6),a6),a6),a6),f5(f3(x9121),x9121))),
% 63.58/63.69 inference(scs_inference,[],[909,2])).
% 63.58/63.69 cnf(913,plain,
% 63.58/63.69 (E(f5(f2(f5(x9131,x9132),a6),f2(x9133,a6)),f1(f1(f5(f5(x9133,x9131),x9132))))),
% 63.58/63.69 inference(scs_inference,[],[15,129,909,2,3])).
% 63.58/63.69 cnf(915,plain,
% 63.58/63.69 (E(f1(f1(f5(f5(x9151,x9152),x9153))),f5(f2(f5(x9152,x9153),a6),f2(x9151,a6)))),
% 63.58/63.69 inference(scs_inference,[],[913,2])).
% 63.58/63.69 cnf(916,plain,
% 63.58/63.69 (E(f2(f1(f1(a9)),a6),f5(f3(x9161),x9161))),
% 63.58/63.69 inference(scs_inference,[],[912,661,913,2,3])).
% 63.58/63.69 cnf(918,plain,
% 63.58/63.69 (E(f5(f3(x9181),x9181),f5(f2(f5(x9182,f3(f5(x9183,x9182))),a6),f2(x9183,a6)))),
% 63.58/63.69 inference(scs_inference,[],[908,915,916,2,3])).
% 63.58/63.69 cnf(922,plain,
% 63.58/63.69 (E(f2(f5(x9221,f3(x9221)),a6),f5(f2(x9222,f2(a6,a6)),f2(f5(x9223,f3(f5(x9222,x9223))),f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[851,582,918,2,3])).
% 63.58/63.69 cnf(923,plain,
% 63.58/63.69 (E(f5(f2(x9231,f2(a6,a6)),f2(f5(x9232,f3(f5(x9231,x9232))),f2(a6,a6))),f2(f5(x9233,f3(x9233)),a6))),
% 63.58/63.69 inference(scs_inference,[],[922,2])).
% 63.58/63.69 cnf(924,plain,
% 63.58/63.69 (E(f5(f3(x9241),x9241),f2(a9,a6))),
% 63.58/63.69 inference(scs_inference,[],[908,192,922,2,3])).
% 63.58/63.69 cnf(927,plain,
% 63.58/63.69 (E(f5(f2(f5(x9271,f3(f5(x9272,x9271))),f2(a6,a6)),f2(x9272,f2(a6,a6))),f2(f5(x9273,f3(x9273)),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,923,924,2,3])).
% 63.58/63.69 cnf(930,plain,
% 63.58/63.69 (E(f2(f2(a9,f2(a6,a6)),a6),f5(f2(f5(x9301,f3(f5(x9302,x9301))),a6),f2(x9302,a6)))),
% 63.58/63.69 inference(scs_inference,[],[568,915,927,2,3])).
% 63.58/63.69 cnf(934,plain,
% 63.58/63.69 (E(f5(f5(x9341,f3(f5(x9342,x9341))),x9342),f1(f1(a9)))),
% 63.58/63.69 inference(scs_inference,[],[15,120,930,2,3])).
% 63.58/63.69 cnf(938,plain,
% 63.58/63.69 (E(f5(f1(x9381),f1(x9382)),f2(f1(f5(x9382,x9381)),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,246,934,2,3])).
% 63.58/63.69 cnf(940,plain,
% 63.58/63.69 (E(f2(f1(f5(x9401,x9402)),a6),f5(f1(x9402),f1(x9401)))),
% 63.58/63.69 inference(scs_inference,[],[938,2])).
% 63.58/63.69 cnf(941,plain,
% 63.58/63.69 (E(f5(x9411,f5(x9412,x9413)),f2(f5(x9412,f5(x9413,x9411)),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,273,938,2,3])).
% 63.58/63.69 cnf(945,plain,
% 63.58/63.69 (E(f2(f5(f2(f1(x9451),a6),f2(f1(x9452),a6)),a6),f5(f1(x9452),f1(x9451)))),
% 63.58/63.69 inference(scs_inference,[],[940,207,941,2,3])).
% 63.58/63.69 cnf(947,plain,
% 63.58/63.69 (E(f5(f1(x9471),f1(x9472)),f2(f5(f2(f1(x9472),a6),f2(f1(x9471),a6)),a6))),
% 63.58/63.69 inference(scs_inference,[],[945,2])).
% 63.58/63.69 cnf(948,plain,
% 63.58/63.69 (E(f1(f1(f5(f1(x9481),f1(x9482)))),f5(f2(f1(x9482),a6),f2(f1(x9481),a6)))),
% 63.58/63.69 inference(scs_inference,[],[833,177,945,2,3])).
% 63.58/63.69 cnf(951,plain,
% 63.58/63.69 (E(f5(f1(x9511),f1(x9512)),f2(f5(f2(f1(x9511),a6),f2(f1(x9512),a6)),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,947,948,2,3])).
% 63.58/63.69 cnf(954,plain,
% 63.58/63.69 (E(f5(f5(x9541,x9542),x9543),f2(f5(f5(x9543,x9541),x9542),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,429,951,2,3])).
% 63.58/63.69 cnf(958,plain,
% 63.58/63.69 (E(f5(f2(f5(x9581,x9582),f2(a6,a6)),f2(x9583,f2(a6,a6))),f2(f5(f5(x9583,x9581),x9582),a6))),
% 63.58/63.69 inference(scs_inference,[],[15,707,954,2,3])).
% 63.58/63.69 cnf(960,plain,
% 63.58/63.69 (E(f2(f5(f5(x9601,x9602),x9603),a6),f5(f2(f5(x9602,x9603),f2(a6,a6)),f2(x9601,f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[958,2])).
% 63.58/63.69 cnf(1255,plain,
% 63.58/63.69 (E(f1(f5(a4,a7)),f1(a7))),
% 63.58/63.69 inference(scs_inference,[],[11,4])).
% 63.58/63.69 cnf(1256,plain,
% 63.58/63.69 (E(f3(f5(a4,a7)),f3(a7))),
% 63.58/63.69 inference(scs_inference,[],[11,4,7])).
% 63.58/63.69 cnf(1258,plain,
% 63.58/63.69 (E(f2(f5(a4,a7),x12581),f2(a7,x12581))),
% 63.58/63.69 inference(scs_inference,[],[11,4,7,6,8])).
% 63.58/63.69 cnf(1259,plain,
% 63.58/63.69 (E(f2(x12591,f5(a4,a7)),f2(x12591,a7))),
% 63.58/63.69 inference(scs_inference,[],[11,4,7,6,8,9])).
% 63.58/63.69 cnf(1260,plain,
% 63.58/63.69 (E(f5(f5(a4,a7),x12601),f5(a7,x12601))),
% 63.58/63.69 inference(scs_inference,[],[11,4,7,6,8,9,5])).
% 63.58/63.69 cnf(1262,plain,
% 63.58/63.69 (~E(f5(f3(f5(f3(f5(a4,a8)),f3(x12621))),f3(f5(f3(f5(a4,a8)),x12621))),a4)),
% 63.58/63.69 inference(scs_inference,[],[11,27,74,4,7,6,8,9,5,2,3])).
% 63.58/63.69 cnf(1264,plain,
% 63.58/63.69 (E(f2(a7,x12641),f2(f5(a4,a7),x12641))),
% 63.58/63.69 inference(scs_inference,[],[25,8])).
% 63.58/63.69 cnf(1266,plain,
% 63.58/63.69 (E(f5(x12661,a7),f5(x12661,f5(a4,a7)))),
% 63.58/63.69 inference(scs_inference,[],[25,8,9,6])).
% 63.58/63.69 cnf(1267,plain,
% 63.58/63.69 (E(f1(a7),f1(f5(a4,a7)))),
% 63.58/63.69 inference(scs_inference,[],[25,8,9,6,4])).
% 63.58/63.69 cnf(1269,plain,
% 63.58/63.69 (E(f5(a7,x12691),f5(f5(a4,a7),x12691))),
% 63.58/63.69 inference(scs_inference,[],[25,8,9,6,4,7,5])).
% 63.58/63.69 cnf(1277,plain,
% 63.58/63.69 (E(f2(x12771,a7),f2(x12771,f5(a8,a7)))),
% 63.58/63.69 inference(scs_inference,[],[28,4,8,6,7,9])).
% 63.58/63.69 cnf(1278,plain,
% 63.58/63.69 (E(f5(a7,x12781),f5(f5(a8,a7),x12781))),
% 63.58/63.69 inference(scs_inference,[],[28,4,8,6,7,9,5])).
% 63.58/63.69 cnf(1279,plain,
% 63.58/63.69 (~E(f2(a7,a6),f5(f5(a4,a8),a7))),
% 63.58/63.69 inference(scs_inference,[],[28,41,4,8,6,7,9,5,2])).
% 63.58/63.69 cnf(1285,plain,
% 63.58/63.69 (E(f1(f1(f5(a4,a7))),f1(f1(a7)))),
% 63.58/63.69 inference(scs_inference,[],[1255,7,6,9,4])).
% 63.58/63.69 cnf(1288,plain,
% 63.58/63.69 (~E(f1(f1(a7)),f5(f5(a4,a8),a7))),
% 63.58/63.69 inference(scs_inference,[],[1255,102,7,6,9,4,8,5,2])).
% 63.58/63.69 cnf(1289,plain,
% 63.58/63.69 (E(f2(f5(a4,a7),f5(a4,a7)),f2(a7,a7))),
% 63.58/63.69 inference(scs_inference,[],[1255,1258,1259,102,7,6,9,4,8,5,2,3])).
% 63.58/63.69 cnf(1292,plain,
% 63.58/63.69 (E(f1(f3(f5(a4,a7))),f1(f3(a7)))),
% 63.58/63.69 inference(scs_inference,[],[1256,4])).
% 63.58/63.69 cnf(1305,plain,
% 63.58/63.69 (E(f2(x13051,f5(f5(a4,a7),x13052)),f2(x13051,f5(a7,x13052)))),
% 63.58/63.69 inference(scs_inference,[],[1260,8,4,7,6,9])).
% 63.58/63.69 cnf(1316,plain,
% 63.58/63.69 (~E(f2(f5(a4,a7),a6),f5(f5(a4,a8),a7))),
% 63.58/63.69 inference(scs_inference,[],[1289,1264,1279,62,6,8,7,9,4,5,2,3])).
% 63.58/63.69 cnf(1324,plain,
% 63.58/63.69 (~E(f5(f5(a4,a8),a7),f2(f5(a4,a7),a6))),
% 63.58/63.69 inference(scs_inference,[],[99,1316,9,7,6,4,8,5,2])).
% 63.58/63.69 cnf(1349,plain,
% 63.58/63.69 (E(f2(f5(x13491,a7),x13492),f2(f5(x13491,f5(a4,a7)),x13492))),
% 63.58/63.69 inference(scs_inference,[],[1266,7,6,4,8])).
% 63.58/63.69 cnf(1351,plain,
% 63.58/63.69 (E(f2(x13511,f5(x13512,a7)),f2(x13511,f5(x13512,f5(a4,a7))))),
% 63.58/63.69 inference(scs_inference,[],[1266,7,6,4,8,5,9])).
% 63.58/63.69 cnf(1353,plain,
% 63.58/63.69 (~E(f5(f5(a4,a8),f5(a4,a7)),f2(f5(a4,a7),a6))),
% 63.58/63.69 inference(scs_inference,[],[1266,1324,103,7,6,4,8,5,9,2,3])).
% 63.58/63.69 cnf(1361,plain,
% 63.58/63.69 (~E(f2(f5(a4,a7),a6),f5(f5(a4,a8),f5(a4,a7)))),
% 63.58/63.69 inference(scs_inference,[],[1269,1353,8,5,4,7,9,6,2])).
% 63.58/63.69 cnf(1372,plain,
% 63.58/63.69 (~E(f2(f5(a4,f5(a4,a7)),a6),f5(f5(a4,a8),f5(a4,a7)))),
% 63.58/63.69 inference(scs_inference,[],[1277,1361,1349,1262,7,9,8,4,6,5,2,3])).
% 63.58/63.69 cnf(1381,plain,
% 63.58/63.69 (E(f5(a7,f3(f5(a8,a7))),f5(x13811,f3(x13811)))),
% 63.58/63.69 inference(scs_inference,[],[1278,732,1372,4,6,8,5,7,9,2,3])).
% 63.58/63.69 cnf(1402,plain,
% 63.58/63.69 (E(f1(f1(a7)),f1(f1(f5(a4,a7))))),
% 63.58/63.69 inference(scs_inference,[],[1267,4])).
% 63.58/63.69 cnf(1445,plain,
% 63.58/63.69 (~E(f1(f1(f5(a4,a7))),f5(f5(a4,a8),a7))),
% 63.58/63.69 inference(scs_inference,[],[768,1288,1402,53,5,7,4,8,9,6,2,3])).
% 63.58/63.69 cnf(1452,plain,
% 63.58/63.69 (~E(f5(f5(a4,a8),a7),f1(f1(f5(a4,a7))))),
% 63.58/63.69 inference(scs_inference,[],[764,1445,8,9,5,4,6,7,2])).
% 63.58/63.69 cnf(1604,plain,
% 63.58/63.69 (~E(f1(f1(f5(a4,a7))),f2(f5(f5(a7,a4),a8),a6))),
% 63.58/63.69 inference(scs_inference,[],[1305,1452,954,6,4,7,9,8,5,3,2])).
% 63.58/63.69 cnf(1726,plain,
% 63.58/63.69 (~E(f2(f5(f5(a7,a4),a8),a6),f1(f1(a7)))),
% 63.58/63.69 inference(scs_inference,[],[1381,1285,1604,4,9,5,6,7,8,3,2])).
% 63.58/63.69 cnf(1744,plain,
% 63.58/63.69 (~E(f1(f1(a7)),f5(f2(f5(a4,a8),f2(a6,a6)),f2(a7,f2(a6,a6))))),
% 63.58/63.69 inference(scs_inference,[],[1726,1292,960,4,9,5,7,8,6,3,2])).
% 63.58/63.69 cnf(1778,plain,
% 63.58/63.69 (~E(f5(f2(f5(a4,a8),f2(a6,a6)),f2(a7,f2(a6,a6))),f5(a4,a7))),
% 63.58/63.69 inference(scs_inference,[],[1351,1744,101,9,5,6,7,8,4,3,2])).
% 63.58/63.69 cnf(1779,plain,
% 63.58/63.69 (E(f2(x17791,f5(a8,a7)),f2(x17791,a7))),
% 63.58/63.69 inference(scs_inference,[],[12,9])).
% 63.58/63.69 cnf(1780,plain,
% 63.58/63.69 (E(f5(f5(a8,a7),x17801),f5(a7,x17801))),
% 63.58/63.69 inference(scs_inference,[],[12,9,5])).
% 63.58/63.69 cnf(1781,plain,
% 63.58/63.69 (E(f5(x17811,f5(a8,a7)),f5(x17811,a7))),
% 63.58/63.69 inference(scs_inference,[],[12,9,5,6])).
% 63.58/63.69 cnf(1794,plain,
% 63.58/63.69 (~E(f2(f5(f5(a7,a4),a8),a6),f5(a4,a7))),
% 63.58/63.69 inference(scs_inference,[],[1779,1778,958,9,5,6,7,8,4,3])).
% 63.58/63.69 cnf(1800,plain,
% 63.58/63.69 (E(f3(f5(f5(a8,a7),x18001)),f3(f5(a7,x18001)))),
% 63.58/63.69 inference(scs_inference,[],[1780,9,5,6,7])).
% 63.58/63.69 cnf(1803,plain,
% 63.58/63.69 (E(f5(f5(a8,a7),f5(a8,a7)),f5(a7,a7))),
% 63.58/63.69 inference(scs_inference,[],[1780,1781,9,5,6,7,8,4,3])).
% 63.58/63.69 cnf(1812,plain,
% 63.58/63.69 (~E(f1(f1(f5(a7,f5(a4,a8)))),f5(a4,a7))),
% 63.58/63.69 inference(scs_inference,[],[1803,1794,172,9,5,6,7,8,4,3])).
% 63.58/63.69 cnf(1975,plain,
% 63.58/63.69 (E(f3(f1(f1(x19751))),f3(x19751))),
% 63.58/63.69 inference(scs_inference,[],[10,7])).
% 63.58/63.69 cnf(1981,plain,
% 63.58/63.69 (~E(f5(a7,f5(a4,a8)),f5(a4,a7))),
% 63.58/63.69 inference(scs_inference,[],[10,1800,1812,7,8,4,9,5,6,3])).
% 63.58/63.69 cnf(1990,plain,
% 63.58/63.69 (~E(f2(f5(a4,f5(a8,a7)),a6),f5(a4,a7))),
% 63.58/63.69 inference(scs_inference,[],[1981,1975,941,7,8,4,9,5,6,3])).
% 63.58/63.69 cnf(2076,plain,
% 63.58/63.69 (E(f2(f2(x20761,a6),x20762),f2(x20761,x20762))),
% 63.58/63.69 inference(scs_inference,[],[13,5,6,7,8])).
% 63.58/63.69 cnf(2105,plain,
% 63.58/63.69 ($false),
% 63.58/63.69 inference(scs_inference,[],[13,2076,1990,1781,5,6,7,8,4,9,3]),
% 63.58/63.69 ['proof']).
% 63.58/63.69 % SZS output end Proof
% 63.58/63.69 % Total time :62.900000s
%------------------------------------------------------------------------------