%------------------------------------------------------------------------------
% 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/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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 : Theorem 64.17s 64.34s
% Output : CNFRefutation 64.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : REL049+1 : TPTP v8.2.0. Released v4.0.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n021.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Sun Jun 23 06:14:39 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.50/0.64 start to proof:theBenchmark
% 64.17/64.33 %-------------------------------------------
% 64.17/64.33 % File :CSE---1.7
% 64.17/64.33 % Problem :theBenchmark
% 64.17/64.33 % Transform :cnf
% 64.17/64.33 % Format :tptp:raw
% 64.17/64.33 % Command :java -jar mcs_scs.jar %d %s
% 64.17/64.33
% 64.17/64.33 % Result :Theorem 63.510000s
% 64.17/64.33 % Output :CNFRefutation 63.510000s
% 64.17/64.33 %-------------------------------------------
% 64.17/64.34 %------------------------------------------------------------------------------
% 64.17/64.34 % File : REL049+1 : TPTP v8.2.0. Released v4.0.0.
% 64.17/64.34 % Domain : Relation Algebra
% 64.17/64.34 % Problem : Join splitting
% 64.17/64.34 % Version : [Mad95] (equational) axioms.
% 64.17/64.34 % English : Join can be split into 2 inequations iff the join is on the
% 64.17/64.34 % left hand side of an inequation.
% 64.17/64.34
% 64.17/64.34 % Refs : [Mad95] Maddux (1995), Relation-Algebraic Semantics
% 64.17/64.34 % : [Hoe08] Hoefner (2008), Email to G. Sutcliffe
% 64.17/64.34 % Source : [Hoe08]
% 64.17/64.34 % Names :
% 64.17/64.34
% 64.17/64.34 % Status : Theorem
% 64.17/64.34 % Rating : 0.00 v6.3.0, 0.07 v6.2.0, 0.09 v6.1.0, 0.00 v4.0.0
% 64.17/64.34 % Syntax : Number of formulae : 14 ( 13 unt; 0 def)
% 64.17/64.34 % Number of atoms : 16 ( 16 equ)
% 64.17/64.34 % Maximal formula atoms : 3 ( 1 avg)
% 64.17/64.34 % Number of connectives : 2 ( 0 ~; 0 |; 1 &)
% 64.17/64.34 % ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% 64.17/64.34 % Maximal formula depth : 6 ( 3 avg)
% 64.17/64.34 % Maximal term depth : 5 ( 2 avg)
% 64.17/64.34 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 64.17/64.34 % Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% 64.17/64.34 % Number of variables : 28 ( 28 !; 0 ?)
% 64.17/64.34 % SPC : FOF_THM_RFO_PEQ
% 64.17/64.34
% 64.17/64.34 % Comments :
% 64.17/64.34 %------------------------------------------------------------------------------
% 64.17/64.34 %---Include axioms for relation algebra
% 64.17/64.34 include('Axioms/REL001+0.ax').
% 64.17/64.34 %------------------------------------------------------------------------------
% 64.17/64.34 fof(goals,conjecture,
% 64.17/64.34 ! [X0,X1,X2] :
% 64.17/64.34 ( ( join(X0,X1) = X1
% 64.17/64.34 & join(X2,X1) = X1 )
% 64.17/64.34 => join(join(X0,X2),X1) = X1 ) ).
% 64.17/64.34
% 64.17/64.34 %------------------------------------------------------------------------------
% 64.17/64.34 %-------------------------------------------
% 64.17/64.34 % Proof found
% 64.17/64.34 % SZS status Theorem for theBenchmark
% 64.17/64.34 % SZS output start Proof
% 64.17/64.35 %ClaNum:24(EqnAxiom:9)
% 64.17/64.35 %VarNum:49(SingletonVarNum:23)
% 64.17/64.35 %MaxLitNum:1
% 64.17/64.35 %MaxfuncDepth:4
% 64.17/64.35 %SharedTerms:13
% 64.17/64.35 %goalClause: 11 12 24
% 64.17/64.35 %singleGoalClaCount:3
% 64.17/64.35 [11]E(f6(a4,a5),a5)
% 64.17/64.35 [12]E(f6(a7,a5),a5)
% 64.17/64.35 [24]~E(f6(f6(a4,a7),a5),a5)
% 64.17/64.35 [13]E(f2(x131,a8),x131)
% 64.17/64.35 [10]E(f1(f1(x101)),x101)
% 64.17/64.35 [14]E(f6(x141,f3(x141)),a9)
% 64.17/64.35 [18]E(f3(f6(f3(x181),f3(f3(x181)))),a10)
% 64.17/64.35 [15]E(f6(x151,x152),f6(x152,x151))
% 64.17/64.35 [16]E(f6(f1(x161),f1(x162)),f1(f6(x161,x162)))
% 64.17/64.35 [17]E(f2(f1(x171),f1(x172)),f1(f2(x172,x171)))
% 64.17/64.35 [22]E(f6(f2(f1(x221),f3(f2(x221,x222))),f3(x222)),f3(x222))
% 64.17/64.35 [23]E(f6(f3(f6(f3(x231),f3(x232))),f3(f6(f3(x231),x232))),x231)
% 64.17/64.35 [19]E(f6(f6(x191,x192),x193),f6(x191,f6(x192,x193)))
% 64.17/64.35 [20]E(f2(f2(x201,x202),x203),f2(x201,f2(x202,x203)))
% 64.17/64.35 [21]E(f6(f2(x211,x212),f2(x213,x212)),f2(f6(x211,x213),x212))
% 64.17/64.35 %EqnAxiom
% 64.17/64.35 [1]E(x11,x11)
% 64.17/64.35 [2]E(x22,x21)+~E(x21,x22)
% 64.17/64.35 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 64.17/64.35 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 64.17/64.35 [5]~E(x51,x52)+E(f6(x51,x53),f6(x52,x53))
% 64.17/64.35 [6]~E(x61,x62)+E(f6(x63,x61),f6(x63,x62))
% 64.17/64.35 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 64.17/64.35 [8]~E(x81,x82)+E(f2(x81,x83),f2(x82,x83))
% 64.17/64.35 [9]~E(x91,x92)+E(f2(x93,x91),f2(x93,x92))
% 64.17/64.35
% 64.17/64.35 %-------------------------------------------
% 64.17/64.36 cnf(26,plain,
% 64.17/64.36 (~E(f6(f6(a4,a7),a5),f6(a4,a5))),
% 64.17/64.36 inference(scs_inference,[],[11,24,2,3])).
% 64.17/64.36 cnf(28,plain,
% 64.17/64.36 (E(a5,f6(a7,a5))),
% 64.17/64.36 inference(scs_inference,[],[12,2])).
% 64.17/64.36 cnf(31,plain,
% 64.17/64.36 (E(x311,f2(x311,a8))),
% 64.17/64.36 inference(scs_inference,[],[13,2])).
% 64.17/64.36 cnf(32,plain,
% 64.17/64.36 (~E(f6(f6(a4,a7),a5),f6(a5,a4))),
% 64.17/64.36 inference(scs_inference,[],[26,15,13,2,3])).
% 64.17/64.36 cnf(34,plain,
% 64.17/64.36 (E(f3(x341),f6(f2(f1(x342),f3(f2(x342,x341))),f3(x341)))),
% 64.17/64.36 inference(scs_inference,[],[22,2])).
% 64.17/64.36 cnf(35,plain,
% 64.17/64.36 (E(f6(a4,a5),f2(a5,a8))),
% 64.17/64.36 inference(scs_inference,[],[11,31,22,2,3])).
% 64.17/64.36 cnf(38,plain,
% 64.17/64.36 (E(f1(f1(f3(x381))),f6(f2(f1(x382),f3(f2(x382,x381))),f3(x381)))),
% 64.17/64.36 inference(scs_inference,[],[34,35,10,2,3])).
% 64.17/64.36 cnf(40,plain,
% 64.17/64.36 (E(f6(f2(f1(x401),f3(f2(x401,x402))),f3(x402)),f1(f1(f3(x402))))),
% 64.17/64.36 inference(scs_inference,[],[38,2])).
% 64.17/64.36 cnf(42,plain,
% 64.17/64.36 (E(f2(f6(x421,x422),x423),f6(f2(x421,x423),f2(x422,x423)))),
% 64.17/64.36 inference(scs_inference,[],[21,2])).
% 64.17/64.36 cnf(45,plain,
% 64.17/64.36 (E(f1(f6(x451,x452)),f6(f1(x451),f1(x452)))),
% 64.17/64.36 inference(scs_inference,[],[16,2])).
% 64.17/64.36 cnf(46,plain,
% 64.17/64.36 (E(f6(x461,x462),f6(f2(x461,a8),f2(x462,a8)))),
% 64.17/64.36 inference(scs_inference,[],[42,31,16,2,3])).
% 64.17/64.36 cnf(49,plain,
% 64.17/64.36 (E(f6(f2(x491,a8),f2(x492,a8)),f6(x491,x492))),
% 64.17/64.36 inference(scs_inference,[],[46,2])).
% 64.17/64.36 cnf(50,plain,
% 64.17/64.36 (E(f1(f6(x501,x502)),f6(f2(f1(x501),a8),f2(f1(x502),a8)))),
% 64.17/64.36 inference(scs_inference,[],[45,46,2,3])).
% 64.17/64.36 cnf(52,plain,
% 64.17/64.36 (E(f6(f2(f1(x521),a8),f2(f1(x522),a8)),f1(f6(x521,x522)))),
% 64.17/64.36 inference(scs_inference,[],[50,2])).
% 64.17/64.36 cnf(55,plain,
% 64.17/64.36 (E(f1(f2(x551,x552)),f2(f1(x552),f1(x551)))),
% 64.17/64.36 inference(scs_inference,[],[17,2])).
% 64.17/64.36 cnf(56,plain,
% 64.17/64.36 (E(f2(f6(f1(x561),f1(x562)),a8),f1(f6(x561,x562)))),
% 64.17/64.36 inference(scs_inference,[],[52,42,17,2,3])).
% 64.17/64.36 cnf(58,plain,
% 64.17/64.36 (E(f1(f6(x581,x582)),f2(f6(f1(x581),f1(x582)),a8))),
% 64.17/64.36 inference(scs_inference,[],[56,2])).
% 64.17/64.36 cnf(61,plain,
% 64.17/64.36 (E(f6(x611,f6(x612,x613)),f6(f6(x611,x612),x613))),
% 64.17/64.36 inference(scs_inference,[],[19,2])).
% 64.17/64.36 cnf(64,plain,
% 64.17/64.36 (E(f2(x641,f2(x642,x643)),f2(f2(x641,x642),x643))),
% 64.17/64.36 inference(scs_inference,[],[20,2])).
% 64.17/64.36 cnf(65,plain,
% 64.17/64.36 (E(f6(f2(x651,a8),f2(f6(x652,x653),a8)),f6(f6(x651,x652),x653))),
% 64.17/64.36 inference(scs_inference,[],[61,49,20,2,3])).
% 64.17/64.36 cnf(68,plain,
% 64.17/64.36 (E(f6(f6(x681,x682),x683),f6(f2(x681,a8),f2(f6(x682,x683),a8)))),
% 64.17/64.36 inference(scs_inference,[],[65,2])).
% 64.17/64.36 cnf(69,plain,
% 64.17/64.36 (~E(f6(f6(a4,a7),a5),f6(f2(a5,a8),f2(a4,a8)))),
% 64.17/64.36 inference(scs_inference,[],[49,65,32,2,3])).
% 64.17/64.36 cnf(71,plain,
% 64.17/64.36 (E(a9,f6(x711,f3(x711)))),
% 64.17/64.36 inference(scs_inference,[],[14,2])).
% 64.17/64.36 cnf(72,plain,
% 64.17/64.36 (~E(f6(f6(a4,a7),a5),f2(f6(a5,a4),a8))),
% 64.17/64.36 inference(scs_inference,[],[42,69,14,2,3])).
% 64.17/64.36 cnf(74,plain,
% 64.17/64.36 (E(x741,f6(f3(f6(f3(x741),f3(x742))),f3(f6(f3(x741),x742))))),
% 64.17/64.36 inference(scs_inference,[],[23,2])).
% 64.17/64.36 cnf(75,plain,
% 64.17/64.36 (E(a9,f6(f2(x751,a8),f2(f6(x752,f3(f6(x751,x752))),a8)))),
% 64.17/64.36 inference(scs_inference,[],[68,71,23,2,3])).
% 64.17/64.36 cnf(79,plain,
% 64.17/64.36 (E(f2(f1(f2(x791,x792)),a8),f2(f1(x792),f1(x791)))),
% 64.17/64.36 inference(scs_inference,[],[55,75,13,2,3])).
% 64.17/64.36 cnf(81,plain,
% 64.17/64.36 (E(f2(f1(x811),f1(x812)),f2(f1(f2(x812,x811)),a8))),
% 64.17/64.36 inference(scs_inference,[],[79,2])).
% 64.17/64.36 cnf(82,plain,
% 64.17/64.36 (E(f6(f2(x821,f2(x822,x823)),f2(x824,f2(x822,x823))),f2(f2(f6(x821,x824),x822),x823))),
% 64.17/64.36 inference(scs_inference,[],[64,79,21,2,3])).
% 64.17/64.36 cnf(85,plain,
% 64.17/64.36 (E(f2(f2(f6(x851,x852),x853),x854),f6(f2(x851,f2(x853,x854)),f2(x852,f2(x853,x854))))),
% 64.17/64.36 inference(scs_inference,[],[82,2])).
% 64.17/64.36 cnf(86,plain,
% 64.17/64.36 (E(f6(a4,a5),f6(f3(f6(f3(a5),f3(x861))),f3(f6(f3(a5),x861))))),
% 64.17/64.36 inference(scs_inference,[],[11,74,82,2,3])).
% 64.17/64.36 cnf(89,plain,
% 64.17/64.36 (E(f1(f1(f1(f2(x891,x892)))),f2(f1(x892),f1(x891)))),
% 64.17/64.36 inference(scs_inference,[],[55,86,10,2,3])).
% 64.17/64.36 cnf(91,plain,
% 64.17/64.36 (E(f2(f1(x911),f1(x912)),f1(f1(f1(f2(x912,x911)))))),
% 64.17/64.36 inference(scs_inference,[],[89,2])).
% 64.17/64.36 cnf(93,plain,
% 64.17/64.36 (E(a10,f3(f6(f3(x931),f3(f3(x931)))))),
% 64.17/64.36 inference(scs_inference,[],[18,2])).
% 64.17/64.36 cnf(96,plain,
% 64.17/64.36 (E(x961,f1(f1(x961)))),
% 64.17/64.36 inference(scs_inference,[],[10,2])).
% 64.17/64.36 cnf(105,plain,
% 64.17/64.36 (E(f6(x1051,f6(x1052,f3(f6(x1051,x1052)))),a9)),
% 64.17/64.36 inference(scs_inference,[],[61,14,3])).
% 64.17/64.36 cnf(108,plain,
% 64.17/64.36 (E(a9,f6(x1081,f6(x1082,f3(f6(x1081,x1082)))))),
% 64.17/64.36 inference(scs_inference,[],[61,14,3,2])).
% 64.17/64.36 cnf(111,plain,
% 64.17/64.36 (E(f2(f6(f1(x1111),f1(x1112)),a8),f1(f1(f1(f6(x1111,x1112)))))),
% 64.17/64.36 inference(scs_inference,[],[10,58,3,2])).
% 64.17/64.36 cnf(115,plain,
% 64.17/64.36 (E(f1(f1(a10)),f3(f6(f3(x1151),f3(f3(x1151)))))),
% 64.17/64.36 inference(scs_inference,[],[10,93,3])).
% 64.17/64.36 cnf(118,plain,
% 64.17/64.36 (E(f1(f1(a9)),f6(x1181,f6(x1182,f3(f6(x1181,x1182)))))),
% 64.17/64.36 inference(scs_inference,[],[10,108,3])).
% 64.17/64.36 cnf(120,plain,
% 64.17/64.36 (E(f6(x1201,f6(x1202,f3(f6(x1201,x1202)))),f1(f1(a9)))),
% 64.17/64.36 inference(scs_inference,[],[10,108,3,2])).
% 64.17/64.36 cnf(123,plain,
% 64.17/64.36 (E(f6(f1(x1231),f1(x1232)),f1(f1(f1(f6(x1231,x1232)))))),
% 64.17/64.36 inference(scs_inference,[],[10,45,3,2])).
% 64.17/64.36 cnf(126,plain,
% 64.17/64.36 (E(f2(f2(x1261,x1262),x1263),f1(f1(f2(x1261,f2(x1262,x1263)))))),
% 64.17/64.36 inference(scs_inference,[],[10,64,3,2])).
% 64.17/64.36 cnf(129,plain,
% 64.17/64.36 (E(f6(f2(x1291,a8),f2(f6(x1292,x1293),a8)),f1(f1(f6(f6(x1291,x1292),x1293))))),
% 64.17/64.36 inference(scs_inference,[],[10,68,3,2])).
% 64.17/64.36 cnf(130,plain,
% 64.17/64.36 (E(f1(f1(a9)),f6(x1301,f3(x1301)))),
% 64.17/64.36 inference(scs_inference,[],[10,71,3])).
% 64.17/64.36 cnf(132,plain,
% 64.17/64.37 (E(f6(x1321,f3(x1321)),f1(f1(a9)))),
% 64.17/64.37 inference(scs_inference,[],[10,71,3,2])).
% 64.17/64.37 cnf(135,plain,
% 64.17/64.37 (E(f1(f1(a9)),f1(f1(f6(x1351,f3(x1351)))))),
% 64.17/64.37 inference(scs_inference,[],[10,132,3,2])).
% 64.17/64.37 cnf(136,plain,
% 64.17/64.37 (E(f1(f1(f6(x1361,f6(x1362,x1363)))),f6(f6(x1361,x1362),x1363))),
% 64.17/64.37 inference(scs_inference,[],[10,61,3])).
% 64.17/64.37 cnf(144,plain,
% 64.17/64.37 (E(f6(f2(f1(x1441),a8),f2(f1(x1442),a8)),f1(f1(f1(f6(x1441,x1442)))))),
% 64.17/64.37 inference(scs_inference,[],[10,50,3,2])).
% 64.17/64.37 cnf(150,plain,
% 64.17/64.37 (E(f1(f6(x1501,x1502)),f1(f1(f6(f1(x1501),f1(x1502)))))),
% 64.17/64.37 inference(scs_inference,[],[10,16,3,2])).
% 64.17/64.37 cnf(159,plain,
% 64.17/64.37 (E(f2(x1591,f2(x1592,x1593)),f1(f1(f2(f2(x1591,x1592),x1593))))),
% 64.17/64.37 inference(scs_inference,[],[10,20,3,2])).
% 64.17/64.37 cnf(160,plain,
% 64.17/64.37 (E(f1(f1(f6(x1601,f3(x1601)))),a9)),
% 64.17/64.37 inference(scs_inference,[],[10,14,3])).
% 64.17/64.37 cnf(162,plain,
% 64.17/64.37 (E(a9,f1(f1(f6(x1621,f3(x1621)))))),
% 64.17/64.37 inference(scs_inference,[],[10,14,3,2])).
% 64.17/64.37 cnf(163,plain,
% 64.17/64.37 (E(f2(f2(f2(f6(x1631,x1632),x1633),x1634),a8),f6(f2(x1631,f2(x1633,x1634)),f2(x1632,f2(x1633,x1634))))),
% 64.17/64.37 inference(scs_inference,[],[13,85,3])).
% 64.17/64.37 cnf(165,plain,
% 64.17/64.37 (E(f6(f2(x1651,f2(x1652,x1653)),f2(x1654,f2(x1652,x1653))),f2(f2(f2(f6(x1651,x1654),x1652),x1653),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,85,3,2])).
% 64.17/64.37 cnf(171,plain,
% 64.17/64.37 (E(f1(f1(f2(x1711,f2(x1712,x1713)))),f2(f2(f2(x1711,x1712),x1713),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,126,3,2])).
% 64.17/64.37 cnf(177,plain,
% 64.17/64.37 (E(f1(f1(f6(f1(x1771),f1(x1772)))),f2(f1(f6(x1771,x1772)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,150,3,2])).
% 64.17/64.37 cnf(183,plain,
% 64.17/64.37 (E(f1(f1(f2(f2(x1831,x1832),x1833))),f2(f2(x1831,f2(x1832,x1833)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,159,3,2])).
% 64.17/64.37 cnf(189,plain,
% 64.17/64.37 (E(f1(f1(f6(x1891,f3(x1891)))),f2(f1(f1(a9)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,135,3,2])).
% 64.17/64.37 cnf(190,plain,
% 64.17/64.37 (E(f2(a9,a8),f1(f1(f6(x1901,f3(x1901)))))),
% 64.17/64.37 inference(scs_inference,[],[13,162,3])).
% 64.17/64.37 cnf(192,plain,
% 64.17/64.37 (E(f1(f1(f6(x1921,f3(x1921)))),f2(a9,a8))),
% 64.17/64.37 inference(scs_inference,[],[13,162,3,2])).
% 64.17/64.37 cnf(193,plain,
% 64.17/64.37 (E(f2(f1(f1(f6(x1931,f3(x1931)))),a8),f2(a9,a8))),
% 64.17/64.37 inference(scs_inference,[],[13,192,3])).
% 64.17/64.37 cnf(196,plain,
% 64.17/64.37 (E(f2(f2(f1(x1961),f1(x1962)),a8),f1(f1(f1(f2(x1962,x1961)))))),
% 64.17/64.37 inference(scs_inference,[],[13,91,193,2,3])).
% 64.17/64.37 cnf(199,plain,
% 64.17/64.37 (E(f2(f6(f2(f1(x1991),a8),f2(f1(x1992),a8)),a8),f1(f6(x1991,x1992)))),
% 64.17/64.37 inference(scs_inference,[],[13,52,196,2,3])).
% 64.17/64.37 cnf(201,plain,
% 64.17/64.37 (E(f1(f6(x2011,x2012)),f2(f6(f2(f1(x2011),a8),f2(f1(x2012),a8)),a8))),
% 64.17/64.37 inference(scs_inference,[],[199,2])).
% 64.17/64.37 cnf(202,plain,
% 64.17/64.37 (E(f2(f6(x2021,f3(x2021)),a8),f1(f1(a9)))),
% 64.17/64.37 inference(scs_inference,[],[13,132,199,2,3])).
% 64.17/64.37 cnf(204,plain,
% 64.17/64.37 (E(f1(f1(a9)),f2(f6(x2041,f3(x2041)),a8))),
% 64.17/64.37 inference(scs_inference,[],[202,2])).
% 64.17/64.37 cnf(205,plain,
% 64.17/64.37 (E(f2(f1(f6(x2051,x2052)),a8),f2(f6(f2(f1(x2051),a8),f2(f1(x2052),a8)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,201,202,2,3])).
% 64.17/64.37 cnf(208,plain,
% 64.17/64.37 (E(f2(f1(f1(a9)),a8),f2(f6(x2081,f3(x2081)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,204,205,2,3])).
% 64.17/64.37 cnf(210,plain,
% 64.17/64.37 (E(f2(f6(x2101,f3(x2101)),a8),f2(f1(f1(a9)),a8))),
% 64.17/64.37 inference(scs_inference,[],[208,2])).
% 64.17/64.37 cnf(211,plain,
% 64.17/64.37 (E(f2(f1(f6(x2111,x2112)),a8),f2(f6(f1(x2111),f1(x2112)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,58,208,2,3])).
% 64.17/64.37 cnf(213,plain,
% 64.17/64.37 (E(f2(f6(f1(x2131),f1(x2132)),a8),f2(f1(f6(x2131,x2132)),a8))),
% 64.17/64.37 inference(scs_inference,[],[211,2])).
% 64.17/64.37 cnf(214,plain,
% 64.17/64.37 (E(f2(f2(f6(x2141,f3(x2141)),a8),a8),f2(f1(f1(a9)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,210,211,2,3])).
% 64.17/64.37 cnf(216,plain,
% 64.17/64.37 (E(f2(f1(f1(a9)),a8),f2(f2(f6(x2161,f3(x2161)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[214,2])).
% 64.17/64.37 cnf(217,plain,
% 64.17/64.37 (E(f2(f2(f6(f1(x2171),f1(x2172)),a8),a8),f2(f1(f6(x2171,x2172)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,213,214,2,3])).
% 64.17/64.37 cnf(219,plain,
% 64.17/64.37 (E(f2(f1(f6(x2191,x2192)),a8),f2(f2(f6(f1(x2191),f1(x2192)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[217,2])).
% 64.17/64.37 cnf(220,plain,
% 64.17/64.37 (E(f2(f2(f1(x2201),f1(x2202)),a8),f2(f1(f2(x2202,x2201)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,81,217,2,3])).
% 64.17/64.37 cnf(222,plain,
% 64.17/64.37 (E(f2(f1(f2(x2221,x2222)),a8),f2(f2(f1(x2222),f1(x2221)),a8))),
% 64.17/64.37 inference(scs_inference,[],[220,2])).
% 64.17/64.37 cnf(223,plain,
% 64.17/64.37 (E(f2(a10,a8),f3(f6(f3(x2231),f3(f3(x2231)))))),
% 64.17/64.37 inference(scs_inference,[],[13,93,220,2,3])).
% 64.17/64.37 cnf(225,plain,
% 64.17/64.37 (E(f3(f6(f3(x2251),f3(f3(x2251)))),f2(a10,a8))),
% 64.17/64.37 inference(scs_inference,[],[223,2])).
% 64.17/64.37 cnf(226,plain,
% 64.17/64.37 (E(f2(f2(f1(f2(x2261,x2262)),a8),a8),f2(f2(f1(x2262),f1(x2261)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,222,223,2,3])).
% 64.17/64.37 cnf(229,plain,
% 64.17/64.37 (E(f2(f3(f6(f3(x2291),f3(f3(x2291)))),a8),f2(a10,a8))),
% 64.17/64.37 inference(scs_inference,[],[13,225,226,2,3])).
% 64.17/64.37 cnf(232,plain,
% 64.17/64.37 (E(f2(a9,a8),f6(x2321,f6(x2322,f3(f6(x2321,x2322)))))),
% 64.17/64.37 inference(scs_inference,[],[13,108,229,2,3])).
% 64.17/64.37 cnf(234,plain,
% 64.17/64.37 (E(f6(x2341,f6(x2342,f3(f6(x2341,x2342)))),f2(a9,a8))),
% 64.17/64.37 inference(scs_inference,[],[232,2])).
% 64.17/64.37 cnf(235,plain,
% 64.17/64.37 (E(f2(f3(x2351),a8),f6(f2(f1(x2352),f3(f2(x2352,x2351))),f3(x2351)))),
% 64.17/64.37 inference(scs_inference,[],[13,34,232,2,3])).
% 64.17/64.37 cnf(237,plain,
% 64.17/64.37 (E(f6(f2(f1(x2371),f3(f2(x2371,x2372))),f3(x2372)),f2(f3(x2372),a8))),
% 64.17/64.37 inference(scs_inference,[],[235,2])).
% 64.17/64.37 cnf(238,plain,
% 64.17/64.37 (E(f2(f6(x2381,f6(x2382,f3(f6(x2381,x2382)))),a8),f2(a9,a8))),
% 64.17/64.37 inference(scs_inference,[],[13,234,235,2,3])).
% 64.17/64.37 cnf(241,plain,
% 64.17/64.37 (E(f2(f6(f2(f1(x2411),f3(f2(x2411,x2412))),f3(x2412)),a8),f2(f3(x2412),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,237,238,2,3])).
% 64.17/64.37 cnf(243,plain,
% 64.17/64.37 (E(f2(f3(x2431),a8),f2(f6(f2(f1(x2432),f3(f2(x2432,x2431))),f3(x2431)),a8))),
% 64.17/64.37 inference(scs_inference,[],[241,2])).
% 64.17/64.37 cnf(244,plain,
% 64.17/64.37 (E(f2(f1(f6(x2441,x2442)),a8),f6(f1(x2441),f1(x2442)))),
% 64.17/64.37 inference(scs_inference,[],[13,45,241,2,3])).
% 64.17/64.37 cnf(246,plain,
% 64.17/64.37 (E(f6(f1(x2461),f1(x2462)),f2(f1(f6(x2461,x2462)),a8))),
% 64.17/64.37 inference(scs_inference,[],[244,2])).
% 64.17/64.37 cnf(247,plain,
% 64.17/64.37 (E(f2(f2(f3(x2471),a8),a8),f2(f6(f2(f1(x2472),f3(f2(x2472,x2471))),f3(x2471)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,243,244,2,3])).
% 64.17/64.37 cnf(250,plain,
% 64.17/64.37 (E(f2(f2(x2501,f2(x2502,x2503)),a8),f2(f2(x2501,x2502),x2503))),
% 64.17/64.37 inference(scs_inference,[],[13,64,247,2,3])).
% 64.17/64.37 cnf(252,plain,
% 64.17/64.37 (E(f2(f2(x2521,x2522),x2523),f2(f2(x2521,f2(x2522,x2523)),a8))),
% 64.17/64.37 inference(scs_inference,[],[250,2])).
% 64.17/64.37 cnf(253,plain,
% 64.17/64.37 (E(f2(f6(f2(f1(x2531),f3(f2(x2531,x2532))),f3(x2532)),a8),f1(f1(f3(x2532))))),
% 64.17/64.37 inference(scs_inference,[],[13,40,250,2,3])).
% 64.17/64.37 cnf(256,plain,
% 64.17/64.37 (E(f2(f2(f2(x2561,x2562),x2563),a8),f2(f2(x2561,f2(x2562,x2563)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,252,253,2,3])).
% 64.17/64.37 cnf(258,plain,
% 64.17/64.37 (E(f2(f2(x2581,f2(x2582,x2583)),a8),f2(f2(f2(x2581,x2582),x2583),a8))),
% 64.17/64.37 inference(scs_inference,[],[256,2])).
% 64.17/64.37 cnf(259,plain,
% 64.17/64.37 (E(f2(f6(f6(x2591,x2592),x2593),a8),f6(f2(x2591,a8),f2(f6(x2592,x2593),a8)))),
% 64.17/64.37 inference(scs_inference,[],[13,68,256,2,3])).
% 64.17/64.37 cnf(261,plain,
% 64.17/64.37 (E(f6(f2(x2611,a8),f2(f6(x2612,x2613),a8)),f2(f6(f6(x2611,x2612),x2613),a8))),
% 64.17/64.37 inference(scs_inference,[],[259,2])).
% 64.17/64.37 cnf(262,plain,
% 64.17/64.37 (E(f2(f2(f2(x2621,f2(x2622,x2623)),a8),a8),f2(f2(f2(x2621,x2622),x2623),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,258,259,2,3])).
% 64.17/64.37 cnf(264,plain,
% 64.17/64.37 (E(f2(f2(f2(x2641,x2642),x2643),a8),f2(f2(f2(x2641,f2(x2642,x2643)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[262,2])).
% 64.17/64.37 cnf(265,plain,
% 64.17/64.37 (E(f2(f6(f2(x2651,a8),f2(f6(x2652,x2653),a8)),a8),f2(f6(f6(x2651,x2652),x2653),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,261,262,2,3])).
% 64.17/64.37 cnf(267,plain,
% 64.17/64.37 (E(f2(f6(f6(x2671,x2672),x2673),a8),f2(f6(f2(x2671,a8),f2(f6(x2672,x2673),a8)),a8))),
% 64.17/64.37 inference(scs_inference,[],[265,2])).
% 64.17/64.37 cnf(268,plain,
% 64.17/64.37 (E(f2(a9,a8),f6(x2681,f3(x2681)))),
% 64.17/64.37 inference(scs_inference,[],[13,71,265,2,3])).
% 64.17/64.37 cnf(270,plain,
% 64.17/64.37 (E(f6(x2701,f3(x2701)),f2(a9,a8))),
% 64.17/64.37 inference(scs_inference,[],[268,2])).
% 64.17/64.37 cnf(271,plain,
% 64.17/64.37 (E(f2(f6(x2711,f6(x2712,x2713)),a8),f6(f6(x2711,x2712),x2713))),
% 64.17/64.37 inference(scs_inference,[],[13,61,268,2,3])).
% 64.17/64.37 cnf(273,plain,
% 64.17/64.37 (E(f6(f6(x2731,x2732),x2733),f2(f6(x2731,f6(x2732,x2733)),a8))),
% 64.17/64.37 inference(scs_inference,[],[271,2])).
% 64.17/64.37 cnf(274,plain,
% 64.17/64.37 (E(f2(f6(x2741,f3(x2741)),a8),f2(a9,a8))),
% 64.17/64.37 inference(scs_inference,[],[13,270,271,2,3])).
% 64.17/64.37 cnf(276,plain,
% 64.17/64.37 (E(f2(a9,a8),f2(f6(x2761,f3(x2761)),a8))),
% 64.17/64.37 inference(scs_inference,[],[274,2])).
% 64.17/64.37 cnf(277,plain,
% 64.17/64.37 (E(f2(f6(f6(x2771,x2772),x2773),a8),f2(f6(x2771,f6(x2772,x2773)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,273,274,2,3])).
% 64.17/64.37 cnf(279,plain,
% 64.17/64.37 (E(f2(f6(x2791,f6(x2792,x2793)),a8),f2(f6(f6(x2791,x2792),x2793),a8))),
% 64.17/64.37 inference(scs_inference,[],[277,2])).
% 64.17/64.37 cnf(280,plain,
% 64.17/64.37 (E(f2(f2(a9,a8),a8),f2(f6(x2801,f3(x2801)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,276,277,2,3])).
% 64.17/64.37 cnf(282,plain,
% 64.17/64.37 (E(f2(f6(x2821,f3(x2821)),a8),f2(f2(a9,a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[280,2])).
% 64.17/64.37 cnf(283,plain,
% 64.17/64.37 (E(f2(f2(f6(x2831,f6(x2832,x2833)),a8),a8),f2(f6(f6(x2831,x2832),x2833),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,279,280,2,3])).
% 64.17/64.37 cnf(285,plain,
% 64.17/64.37 (E(f2(f6(f6(x2851,x2852),x2853),a8),f2(f2(f6(x2851,f6(x2852,x2853)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[283,2])).
% 64.17/64.37 cnf(286,plain,
% 64.17/64.37 (E(f2(f2(f6(x2861,f3(x2861)),a8),a8),f2(f2(a9,a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,282,283,2,3])).
% 64.17/64.37 cnf(288,plain,
% 64.17/64.37 (E(f2(f2(a9,a8),a8),f2(f2(f6(x2881,f3(x2881)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[286,2])).
% 64.17/64.37 cnf(289,plain,
% 64.17/64.37 (E(f2(f1(f1(a10)),a8),f3(f6(f3(x2891),f3(f3(x2891)))))),
% 64.17/64.37 inference(scs_inference,[],[13,115,286,2,3])).
% 64.17/64.37 cnf(292,plain,
% 64.17/64.37 (E(f2(f2(f2(a9,a8),a8),a8),f2(f2(f6(x2921,f3(x2921)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,288,289,2,3])).
% 64.17/64.37 cnf(294,plain,
% 64.17/64.37 (E(f2(f2(f6(x2941,f3(x2941)),a8),a8),f2(f2(f2(a9,a8),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[292,2])).
% 64.17/64.37 cnf(295,plain,
% 64.17/64.37 (E(f2(f1(f1(a9)),a8),f6(x2951,f6(x2952,f3(f6(x2951,x2952)))))),
% 64.17/64.37 inference(scs_inference,[],[13,118,292,2,3])).
% 64.17/64.37 cnf(297,plain,
% 64.17/64.37 (E(f6(x2971,f6(x2972,f3(f6(x2971,x2972)))),f2(f1(f1(a9)),a8))),
% 64.17/64.37 inference(scs_inference,[],[295,2])).
% 64.17/64.37 cnf(298,plain,
% 64.17/64.37 (E(f2(f2(a9,a8),a8),f1(f1(f6(x2981,f3(x2981)))))),
% 64.17/64.37 inference(scs_inference,[],[13,295,190,2,3])).
% 64.17/64.37 cnf(300,plain,
% 64.17/64.37 (E(f1(f1(f6(x3001,f3(x3001)))),f2(f2(a9,a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[298,2])).
% 64.17/64.37 cnf(301,plain,
% 64.17/64.37 (E(f2(f2(f2(a9,a8),a8),a8),f1(f1(f6(x3011,f3(x3011)))))),
% 64.17/64.37 inference(scs_inference,[],[13,298,2,3])).
% 64.17/64.37 cnf(304,plain,
% 64.17/64.37 (E(f2(f6(x3041,f6(x3042,f3(f6(x3041,x3042)))),a8),a9)),
% 64.17/64.37 inference(scs_inference,[],[13,301,105,2,3])).
% 64.17/64.37 cnf(307,plain,
% 64.17/64.37 (E(f2(f1(f1(f6(x3071,f3(x3071)))),a8),a9)),
% 64.17/64.37 inference(scs_inference,[],[13,160,304,2,3])).
% 64.17/64.37 cnf(310,plain,
% 64.17/64.37 (E(f2(f6(f2(x3101,f2(x3102,x3103)),f2(x3104,f2(x3102,x3103))),a8),f2(f2(f6(x3101,x3104),x3102),x3103))),
% 64.17/64.37 inference(scs_inference,[],[13,307,82,2,3])).
% 64.17/64.37 cnf(312,plain,
% 64.17/64.37 (E(f2(f2(f6(x3121,x3122),x3123),x3124),f2(f6(f2(x3121,f2(x3123,x3124)),f2(x3122,f2(x3123,x3124))),a8))),
% 64.17/64.37 inference(scs_inference,[],[310,2])).
% 64.17/64.37 cnf(313,plain,
% 64.17/64.37 (E(f2(f2(a9,a8),a8),f6(x3131,f3(x3131)))),
% 64.17/64.37 inference(scs_inference,[],[13,310,268,2,3])).
% 64.17/64.37 cnf(315,plain,
% 64.17/64.37 (E(f6(x3151,f3(x3151)),f2(f2(a9,a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[313,2])).
% 64.17/64.37 cnf(316,plain,
% 64.17/64.37 (E(f2(f2(f2(a9,a8),a8),a8),f6(x3161,f3(x3161)))),
% 64.17/64.37 inference(scs_inference,[],[13,313,2,3])).
% 64.17/64.37 cnf(318,plain,
% 64.17/64.37 (E(f6(x3181,f3(x3181)),f2(f2(f2(a9,a8),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[316,2])).
% 64.17/64.37 cnf(319,plain,
% 64.17/64.37 (E(f2(f2(f2(f2(a9,a8),a8),a8),a8),f6(x3191,f3(x3191)))),
% 64.17/64.37 inference(scs_inference,[],[13,316,2,3])).
% 64.17/64.37 cnf(321,plain,
% 64.17/64.37 (E(f6(x3211,f3(x3211)),f2(f2(f2(f2(a9,a8),a8),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[319,2])).
% 64.17/64.37 cnf(322,plain,
% 64.17/64.37 (E(f2(f6(x3221,f3(x3221)),a8),f2(f2(f2(a9,a8),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,318,319,2,3])).
% 64.17/64.37 cnf(325,plain,
% 64.17/64.37 (E(f2(f6(x3251,f3(x3251)),a8),f2(f2(f2(f2(a9,a8),a8),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,321,322,2,3])).
% 64.17/64.37 cnf(327,plain,
% 64.17/64.37 (E(f2(f2(f2(f2(a9,a8),a8),a8),a8),f2(f6(x3271,f3(x3271)),a8))),
% 64.17/64.37 inference(scs_inference,[],[325,2])).
% 64.17/64.37 cnf(328,plain,
% 64.17/64.37 (E(f2(f2(a9,a8),a8),f6(x3281,f6(x3282,f3(f6(x3281,x3282)))))),
% 64.17/64.37 inference(scs_inference,[],[13,325,232,2,3])).
% 64.17/64.37 cnf(331,plain,
% 64.17/64.37 (E(f2(f2(f2(a9,a8),a8),a8),f6(x3311,f6(x3312,f3(f6(x3311,x3312)))))),
% 64.17/64.37 inference(scs_inference,[],[13,328,2,3])).
% 64.17/64.37 cnf(333,plain,
% 64.17/64.37 (E(f6(x3331,f6(x3332,f3(f6(x3331,x3332)))),f2(f2(f2(a9,a8),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[331,2])).
% 64.17/64.37 cnf(334,plain,
% 64.17/64.37 (E(f2(f6(f2(x3341,a8),f2(f6(x3342,x3343),a8)),a8),f6(f6(x3341,x3342),x3343))),
% 64.17/64.37 inference(scs_inference,[],[13,331,65,2,3])).
% 64.17/64.37 cnf(336,plain,
% 64.17/64.37 (E(f6(f6(x3361,x3362),x3363),f2(f6(f2(x3361,a8),f2(f6(x3362,x3363),a8)),a8))),
% 64.17/64.37 inference(scs_inference,[],[334,2])).
% 64.17/64.37 cnf(337,plain,
% 64.17/64.37 (E(f2(f2(f3(x3371),a8),a8),f6(f2(f1(x3372),f3(f2(x3372,x3371))),f3(x3371)))),
% 64.17/64.37 inference(scs_inference,[],[13,334,235,2,3])).
% 64.17/64.37 cnf(340,plain,
% 64.17/64.37 (E(f2(f2(f2(f3(x3401),a8),a8),a8),f6(f2(f1(x3402),f3(f2(x3402,x3401))),f3(x3401)))),
% 64.17/64.37 inference(scs_inference,[],[13,337,2,3])).
% 64.17/64.37 cnf(342,plain,
% 64.17/64.37 (E(f6(f2(f1(x3421),f3(f2(x3421,x3422))),f3(x3422)),f2(f2(f2(f3(x3422),a8),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[340,2])).
% 64.17/64.37 cnf(343,plain,
% 64.17/64.37 (E(f2(f2(f6(f1(x3431),f1(x3432)),a8),a8),f1(f6(x3431,x3432)))),
% 64.17/64.37 inference(scs_inference,[],[13,340,56,2,3])).
% 64.17/64.37 cnf(346,plain,
% 64.17/64.37 (E(f2(f2(f1(f2(x3461,x3462)),a8),a8),f2(f1(x3462),f1(x3461)))),
% 64.17/64.37 inference(scs_inference,[],[13,343,79,2,3])).
% 64.17/64.37 cnf(349,plain,
% 64.17/64.37 (E(f2(f1(f1(a9)),a8),f6(x3491,f3(x3491)))),
% 64.17/64.37 inference(scs_inference,[],[13,346,130,2,3])).
% 64.17/64.37 cnf(351,plain,
% 64.17/64.37 (E(f6(x3511,f3(x3511)),f2(f1(f1(a9)),a8))),
% 64.17/64.37 inference(scs_inference,[],[349,2])).
% 64.17/64.37 cnf(352,plain,
% 64.17/64.37 (E(f2(f2(f1(f1(a9)),a8),a8),f6(x3521,f3(x3521)))),
% 64.17/64.37 inference(scs_inference,[],[13,349,2,3])).
% 64.17/64.37 cnf(354,plain,
% 64.17/64.37 (E(f6(x3541,f3(x3541)),f2(f2(f1(f1(a9)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[352,2])).
% 64.17/64.37 cnf(355,plain,
% 64.17/64.37 (E(f2(f2(f1(f6(x3551,x3552)),a8),a8),f6(f1(x3551),f1(x3552)))),
% 64.17/64.37 inference(scs_inference,[],[13,352,244,2,3])).
% 64.17/64.37 cnf(357,plain,
% 64.17/64.37 (E(f6(f1(x3571),f1(x3572)),f2(f2(f1(f6(x3571,x3572)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[355,2])).
% 64.17/64.37 cnf(358,plain,
% 64.17/64.37 (E(f2(f6(x3581,f3(x3581)),a8),f2(f2(f1(f1(a9)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,354,355,2,3])).
% 64.17/64.37 cnf(360,plain,
% 64.17/64.37 (E(f2(f2(f1(f1(a9)),a8),a8),f2(f6(x3601,f3(x3601)),a8))),
% 64.17/64.37 inference(scs_inference,[],[358,2])).
% 64.17/64.37 cnf(361,plain,
% 64.17/64.37 (E(f2(f6(f1(x3611),f1(x3612)),a8),f2(f2(f1(f6(x3611,x3612)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,357,358,2,3])).
% 64.17/64.37 cnf(363,plain,
% 64.17/64.37 (E(f2(f2(f1(f6(x3631,x3632)),a8),a8),f2(f6(f1(x3631),f1(x3632)),a8))),
% 64.17/64.37 inference(scs_inference,[],[361,2])).
% 64.17/64.37 cnf(364,plain,
% 64.17/64.37 (E(f2(f2(f2(x3641,f2(x3642,x3643)),a8),a8),f2(f2(x3641,x3642),x3643))),
% 64.17/64.37 inference(scs_inference,[],[13,361,250,2,3])).
% 64.17/64.37 cnf(366,plain,
% 64.17/64.37 (E(f2(f2(x3661,x3662),x3663),f2(f2(f2(x3661,f2(x3662,x3663)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[364,2])).
% 64.17/64.37 cnf(367,plain,
% 64.17/64.37 (E(f2(f2(f6(x3671,f6(x3672,x3673)),a8),a8),f6(f6(x3671,x3672),x3673))),
% 64.17/64.37 inference(scs_inference,[],[13,364,271,2,3])).
% 64.17/64.37 cnf(369,plain,
% 64.17/64.37 (E(f6(f6(x3691,x3692),x3693),f2(f2(f6(x3691,f6(x3692,x3693)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[367,2])).
% 64.17/64.37 cnf(370,plain,
% 64.17/64.37 (E(f2(f2(f6(x3701,f3(x3701)),a8),a8),f2(a9,a8))),
% 64.17/64.37 inference(scs_inference,[],[13,367,274,2,3])).
% 64.17/64.37 cnf(372,plain,
% 64.17/64.37 (E(f2(a9,a8),f2(f2(f6(x3721,f3(x3721)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[370,2])).
% 64.17/64.37 cnf(373,plain,
% 64.17/64.37 (E(f2(f2(f2(f6(x3731,f3(x3731)),a8),a8),a8),f2(a9,a8))),
% 64.17/64.37 inference(scs_inference,[],[13,370,2,3])).
% 64.17/64.37 cnf(376,plain,
% 64.17/64.37 (E(f2(f2(f6(f6(x3761,x3762),x3763),a8),a8),f6(f2(x3761,a8),f2(f6(x3762,x3763),a8)))),
% 64.17/64.37 inference(scs_inference,[],[13,373,259,2,3])).
% 64.17/64.37 cnf(379,plain,
% 64.17/64.37 (E(f2(f2(f6(f2(f1(x3791),f3(f2(x3791,x3792))),f3(x3792)),a8),a8),f2(f3(x3792),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,376,241,2,3])).
% 64.17/64.37 cnf(381,plain,
% 64.17/64.37 (E(f2(f3(x3811),a8),f2(f2(f6(f2(f1(x3812),f3(f2(x3812,x3811))),f3(x3811)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[379,2])).
% 64.17/64.37 cnf(382,plain,
% 64.17/64.37 (E(f2(f2(f6(x3821,f3(x3821)),a8),a8),f1(f1(a9)))),
% 64.17/64.37 inference(scs_inference,[],[13,379,202,2,3])).
% 64.17/64.37 cnf(384,plain,
% 64.17/64.37 (E(f1(f1(a9)),f2(f2(f6(x3841,f3(x3841)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[382,2])).
% 64.17/64.37 cnf(385,plain,
% 64.17/64.37 (E(f2(f2(f2(f1(x3851),f1(x3852)),a8),a8),f2(f1(f2(x3852,x3851)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,382,220,2,3])).
% 64.17/64.37 cnf(387,plain,
% 64.17/64.37 (E(f2(f1(f2(x3871,x3872)),a8),f2(f2(f2(f1(x3872),f1(x3871)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[385,2])).
% 64.17/64.37 cnf(388,plain,
% 64.17/64.37 (E(f2(f2(f2(f2(x3881,x3882),x3883),a8),a8),f2(f2(x3881,f2(x3882,x3883)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,385,256,2,3])).
% 64.17/64.37 cnf(390,plain,
% 64.17/64.37 (E(f2(f2(x3901,f2(x3902,x3903)),a8),f2(f2(f2(f2(x3901,x3902),x3903),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[388,2])).
% 64.17/64.37 cnf(391,plain,
% 64.17/64.37 (E(f2(f2(f6(f6(x3911,x3912),x3913),a8),a8),f2(f6(x3911,f6(x3912,x3913)),a8))),
% 64.17/64.37 inference(scs_inference,[],[13,388,277,2,3])).
% 64.17/64.37 cnf(394,plain,
% 64.17/64.37 (E(f2(f2(a10,a8),a8),f3(f6(f3(x3941),f3(f3(x3941)))))),
% 64.17/64.37 inference(scs_inference,[],[13,391,223,2,3])).
% 64.17/64.37 cnf(397,plain,
% 64.17/64.37 (E(f2(f2(f2(a10,a8),a8),a8),f3(f6(f3(x3971),f3(f3(x3971)))))),
% 64.17/64.37 inference(scs_inference,[],[13,394,2,3])).
% 64.17/64.37 cnf(400,plain,
% 64.17/64.37 (E(f2(a9,a8),f6(f2(x4001,a8),f2(f6(x4002,f3(f6(x4001,x4002))),a8)))),
% 64.17/64.37 inference(scs_inference,[],[13,397,75,2,3])).
% 64.17/64.37 cnf(402,plain,
% 64.17/64.37 (E(f6(f2(x4021,a8),f2(f6(x4022,f3(f6(x4021,x4022))),a8)),f2(a9,a8))),
% 64.17/64.37 inference(scs_inference,[],[400,2])).
% 64.17/64.37 cnf(403,plain,
% 64.17/64.37 (E(f2(f1(f1(f3(x4031))),a8),f6(f2(f1(x4032),f3(f2(x4032,x4031))),f3(x4031)))),
% 64.17/64.37 inference(scs_inference,[],[13,400,38,2,3])).
% 64.17/64.37 cnf(406,plain,
% 64.17/64.37 (E(f2(f1(f6(x4061,x4062)),a8),f6(f2(f1(x4061),a8),f2(f1(x4062),a8)))),
% 64.17/64.37 inference(scs_inference,[],[13,403,50,2,3])).
% 64.17/64.37 cnf(409,plain,
% 64.17/64.37 (E(f2(f2(f1(f6(x4091,x4092)),a8),a8),f6(f2(f1(x4091),a8),f2(f1(x4092),a8)))),
% 64.17/64.37 inference(scs_inference,[],[13,406,2,3])).
% 64.17/64.37 cnf(412,plain,
% 64.17/64.37 (E(f2(f3(f6(f3(x4121),f3(f3(x4121)))),a8),a10)),
% 64.17/64.37 inference(scs_inference,[],[13,409,18,2,3])).
% 64.17/64.37 cnf(415,plain,
% 64.17/64.37 (E(f2(f6(f2(f1(x4151),f3(f2(x4151,x4152))),f3(x4152)),a8),f3(x4152))),
% 64.17/64.37 inference(scs_inference,[],[13,412,22,2,3])).
% 64.17/64.37 cnf(418,plain,
% 64.17/64.37 (E(f2(f2(f6(f2(f1(x4181),f3(f2(x4181,x4182))),f3(x4182)),a8),a8),f3(x4182))),
% 64.17/64.37 inference(scs_inference,[],[13,415,2,3])).
% 64.17/64.37 cnf(420,plain,
% 64.17/64.37 (E(f3(x4201),f2(f2(f6(f2(f1(x4202),f3(f2(x4202,x4201))),f3(x4201)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[418,2])).
% 64.17/64.37 cnf(421,plain,
% 64.17/64.37 (E(f2(f2(f1(x4211),f1(x4212)),a8),f1(f2(x4212,x4211)))),
% 64.17/64.37 inference(scs_inference,[],[13,418,17,2,3])).
% 64.17/64.37 cnf(424,plain,
% 64.17/64.37 (E(f2(f2(f2(f1(x4241),f1(x4242)),a8),a8),f1(f2(x4242,x4241)))),
% 64.17/64.37 inference(scs_inference,[],[13,421,2,3])).
% 64.17/64.37 cnf(427,plain,
% 64.17/64.37 (E(f2(f6(f6(x4271,x4272),x4273),a8),f6(x4271,f6(x4272,x4273)))),
% 64.17/64.37 inference(scs_inference,[],[13,424,19,2,3])).
% 64.17/64.37 cnf(430,plain,
% 64.17/64.37 (E(f2(f2(f6(f6(x4301,x4302),x4303),a8),a8),f6(x4301,f6(x4302,x4303)))),
% 64.17/64.37 inference(scs_inference,[],[13,427,2,3])).
% 64.17/64.37 cnf(432,plain,
% 64.17/64.37 (E(f6(x4321,f6(x4322,x4323)),f2(f2(f6(f6(x4321,x4322),x4323),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[430,2])).
% 64.17/64.37 cnf(433,plain,
% 64.17/64.37 (E(f2(f2(f2(x4331,x4332),x4333),a8),f2(x4331,f2(x4332,x4333)))),
% 64.17/64.37 inference(scs_inference,[],[13,430,20,2,3])).
% 64.17/64.37 cnf(435,plain,
% 64.17/64.37 (E(f2(x4351,f2(x4352,x4353)),f2(f2(f2(x4351,x4352),x4353),a8))),
% 64.17/64.37 inference(scs_inference,[],[433,2])).
% 64.17/64.37 cnf(436,plain,
% 64.17/64.37 (E(f2(f2(f2(f2(x4361,x4362),x4363),a8),a8),f2(x4361,f2(x4362,x4363)))),
% 64.17/64.37 inference(scs_inference,[],[13,433,2,3])).
% 64.17/64.37 cnf(438,plain,
% 64.17/64.37 (E(f2(x4381,f2(x4382,x4383)),f2(f2(f2(f2(x4381,x4382),x4383),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[436,2])).
% 64.17/64.37 cnf(439,plain,
% 64.17/64.37 (E(f2(f6(x4391,f3(x4391)),a8),a9)),
% 64.17/64.37 inference(scs_inference,[],[13,436,14,2,3])).
% 64.17/64.37 cnf(442,plain,
% 64.17/64.37 (E(f2(f2(f6(x4421,f3(x4421)),a8),a8),a9)),
% 64.17/64.37 inference(scs_inference,[],[13,439,2,3])).
% 64.17/64.37 cnf(444,plain,
% 64.17/64.37 (E(a9,f2(f2(f6(x4441,f3(x4441)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[442,2])).
% 64.17/64.37 cnf(453,plain,
% 64.17/64.37 (E(f2(f1(f1(a9)),a8),a9)),
% 64.17/64.37 inference(scs_inference,[],[351,71,3,2])).
% 64.17/64.37 cnf(459,plain,
% 64.17/64.37 (E(f2(f2(f2(a9,a8),a8),a8),a9)),
% 64.17/64.37 inference(scs_inference,[],[333,108,3,2])).
% 64.17/64.37 cnf(470,plain,
% 64.17/64.37 (E(f2(f6(x4701,f3(x4701)),a8),f6(x4702,f3(x4702)))),
% 64.17/64.37 inference(scs_inference,[],[360,354,3,2])).
% 64.17/64.37 cnf(481,plain,
% 64.17/64.37 (E(f2(f2(f2(f2(x4811,x4812),x4813),x4814),a8),f2(x4811,f2(x4812,f2(x4813,x4814))))),
% 64.17/64.37 inference(scs_inference,[],[435,64,3,2])).
% 64.17/64.37 cnf(498,plain,
% 64.17/64.37 (E(f2(f2(f2(a9,f2(a8,a8)),a8),a8),f6(x4981,f3(x4981)))),
% 64.17/64.37 inference(scs_inference,[],[315,366,3,2])).
% 64.17/64.37 cnf(501,plain,
% 64.17/64.37 (E(a9,f2(f2(f2(a9,f2(a8,a8)),a8),a8))),
% 64.17/64.37 inference(scs_inference,[],[14,498,3,2])).
% 64.17/64.37 cnf(504,plain,
% 64.17/64.37 (E(f2(f6(x5041,f3(x5041)),a8),f2(a9,f2(a8,a8)))),
% 64.17/64.37 inference(scs_inference,[],[438,327,3,2])).
% 64.17/64.37 cnf(507,plain,
% 64.17/64.37 (E(f2(f2(f2(a9,a8),a8),a8),f2(a9,a8))),
% 64.17/64.37 inference(scs_inference,[],[372,294,3,2])).
% 64.17/64.37 cnf(516,plain,
% 64.17/64.37 (E(f2(f2(f2(a9,f2(f2(a8,a8),a8)),a8),a8),a9)),
% 64.17/64.37 inference(scs_inference,[],[501,264,3,2])).
% 64.17/64.37 cnf(518,plain,
% 64.17/64.37 (E(f2(f2(f6(x5181,f3(x5181)),a8),a8),f6(x5182,f3(x5182)))),
% 64.17/64.37 inference(scs_inference,[],[14,444,3,2])).
% 64.17/64.37 cnf(522,plain,
% 64.17/64.37 (E(f6(x5221,f3(x5221)),f6(x5222,f6(x5223,f3(f6(x5222,x5223)))))),
% 64.17/64.37 inference(scs_inference,[],[518,432,3,2])).
% 64.17/64.37 cnf(525,plain,
% 64.17/64.37 (E(f6(x5251,f6(x5252,f3(f6(x5251,x5252)))),f2(f6(x5253,f3(x5253)),a8))),
% 64.17/64.37 inference(scs_inference,[],[522,470,3,2])).
% 64.17/64.37 cnf(528,plain,
% 64.17/64.37 (E(f1(f1(f6(f1(x5281),f1(x5282)))),f6(f2(f1(x5281),a8),f2(f1(x5282),a8)))),
% 64.17/64.37 inference(scs_inference,[],[150,52,3,2])).
% 64.17/64.37 cnf(534,plain,
% 64.17/64.37 (E(f2(f2(f2(f3(x5341),a8),a8),a8),f3(x5341))),
% 64.17/64.37 inference(scs_inference,[],[342,34,3,2])).
% 64.17/64.37 cnf(535,plain,
% 64.17/64.37 (E(f1(f1(f2(f3(x5351),f2(a8,a8)))),f3(x5351))),
% 64.17/64.37 inference(scs_inference,[],[534,171,3])).
% 64.17/64.37 cnf(538,plain,
% 64.17/64.37 (E(f2(a9,f2(f2(f2(a8,a8),a8),a8)),a9)),
% 64.17/64.37 inference(scs_inference,[],[516,435,535,2,3])).
% 64.17/64.37 cnf(540,plain,
% 64.17/64.37 (E(a9,f2(a9,f2(f2(f2(a8,a8),a8),a8)))),
% 64.17/64.37 inference(scs_inference,[],[538,2])).
% 64.17/64.37 cnf(541,plain,
% 64.17/64.37 (E(f2(f2(a9,f2(a8,a8)),a8),a9)),
% 64.17/64.37 inference(scs_inference,[],[516,366,538,2,3])).
% 64.17/64.37 cnf(543,plain,
% 64.17/64.37 (E(a9,f2(f2(a9,f2(a8,a8)),a8))),
% 64.17/64.37 inference(scs_inference,[],[541,2])).
% 64.17/64.37 cnf(544,plain,
% 64.17/64.37 (E(f6(x5441,f3(x5441)),f2(a9,f2(f2(f2(a8,a8),a8),a8)))),
% 64.17/64.37 inference(scs_inference,[],[14,540,541,2,3])).
% 64.17/64.37 cnf(545,plain,
% 64.17/64.37 (E(f2(a9,f2(f2(f2(a8,a8),a8),a8)),f6(x5451,f3(x5451)))),
% 64.17/64.37 inference(scs_inference,[],[544,2])).
% 64.17/64.37 cnf(546,plain,
% 64.17/64.37 (E(f6(x5461,f3(x5461)),f2(f2(a9,f2(a8,a8)),a8))),
% 64.17/64.37 inference(scs_inference,[],[14,543,544,2,3])).
% 64.17/64.37 cnf(547,plain,
% 64.17/64.37 (E(f2(f2(a9,f2(a8,a8)),a8),f6(x5471,f3(x5471)))),
% 64.17/64.37 inference(scs_inference,[],[546,2])).
% 64.17/64.37 cnf(548,plain,
% 64.17/64.37 (E(f2(a9,f2(f2(f2(a8,a8),a8),a8)),f2(f1(f1(a9)),a8))),
% 64.17/64.37 inference(scs_inference,[],[545,351,546,2,3])).
% 64.17/64.38 cnf(550,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f2(a9,f2(f2(f2(a8,a8),a8),a8)))),
% 64.17/64.38 inference(scs_inference,[],[548,2])).
% 64.17/64.38 cnf(551,plain,
% 64.17/64.38 (E(f1(f1(f2(f2(a9,a8),a8))),f6(x5511,f3(x5511)))),
% 64.17/64.38 inference(scs_inference,[],[547,183,548,2,3])).
% 64.17/64.38 cnf(554,plain,
% 64.17/64.38 (E(f2(f2(x5541,f2(x5542,x5543)),a8),f2(x5541,f2(x5542,f2(x5543,a8))))),
% 64.17/64.38 inference(scs_inference,[],[481,390,551,2,3])).
% 64.17/64.38 cnf(556,plain,
% 64.17/64.38 (E(f2(x5561,f2(x5562,f2(x5563,a8))),f2(f2(x5561,f2(x5562,x5563)),a8))),
% 64.17/64.38 inference(scs_inference,[],[554,2])).
% 64.17/64.38 cnf(557,plain,
% 64.17/64.38 (E(f3(x5571),f2(f6(f2(f2(f1(x5572),f3(f2(x5572,x5571))),f2(a8,a8)),f2(f3(x5571),f2(a8,a8))),a8))),
% 64.17/64.38 inference(scs_inference,[],[312,420,554,2,3])).
% 64.17/64.38 cnf(559,plain,
% 64.17/64.38 (E(f2(f6(f2(f2(f1(x5591),f3(f2(x5591,x5592))),f2(a8,a8)),f2(f3(x5592),f2(a8,a8))),a8),f3(x5592))),
% 64.17/64.38 inference(scs_inference,[],[557,2])).
% 64.17/64.38 cnf(560,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,f2(a8,a8))),f6(x5601,f3(x5601)))),
% 64.17/64.38 inference(scs_inference,[],[556,547,557,2,3])).
% 64.17/64.38 cnf(562,plain,
% 64.17/64.38 (E(f6(x5621,f3(x5621)),f2(a9,f2(a8,f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[560,2])).
% 64.17/64.38 cnf(563,plain,
% 64.17/64.38 (E(f6(f6(x5631,x5632),x5633),f6(f2(x5631,f2(a8,a8)),f2(f6(x5632,x5633),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[369,85,560,2,3])).
% 64.17/64.38 cnf(565,plain,
% 64.17/64.38 (E(f6(f2(x5651,f2(a8,a8)),f2(f6(x5652,x5653),f2(a8,a8))),f6(f6(x5651,x5652),x5653))),
% 64.17/64.38 inference(scs_inference,[],[563,2])).
% 64.17/64.38 cnf(566,plain,
% 64.17/64.38 (E(f1(f1(f6(x5661,f3(x5661)))),f2(f2(a9,f2(a8,a8)),a8))),
% 64.17/64.38 inference(scs_inference,[],[300,252,563,2,3])).
% 64.17/64.38 cnf(568,plain,
% 64.17/64.38 (E(f2(f2(a9,f2(a8,a8)),a8),f1(f1(f6(x5681,f3(x5681)))))),
% 64.17/64.38 inference(scs_inference,[],[566,2])).
% 64.17/64.38 cnf(569,plain,
% 64.17/64.38 (E(f6(f2(x5691,f2(a8,a8)),f2(f6(x5692,f3(f6(x5691,x5692))),f2(a8,a8))),a9)),
% 64.17/64.38 inference(scs_inference,[],[14,565,566,2,3])).
% 64.17/64.38 cnf(572,plain,
% 64.17/64.38 (E(a9,f6(f2(x5721,f2(a8,a8)),f2(f6(x5722,f3(f6(x5721,x5722))),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[569,2])).
% 64.17/64.38 cnf(573,plain,
% 64.17/64.38 (E(f2(f2(a9,f2(a8,a8)),a8),f2(f1(f1(a9)),a8))),
% 64.17/64.38 inference(scs_inference,[],[568,189,569,2,3])).
% 64.17/64.38 cnf(575,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f2(f2(a9,f2(a8,a8)),a8))),
% 64.17/64.38 inference(scs_inference,[],[573,2])).
% 64.17/64.38 cnf(576,plain,
% 64.17/64.38 (E(f6(x5761,f3(x5761)),f6(f2(x5762,f2(a8,a8)),f2(f6(x5763,f3(f6(x5762,x5763))),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[14,572,573,2,3])).
% 64.17/64.38 cnf(577,plain,
% 64.17/64.38 (E(f6(f2(x5771,f2(a8,a8)),f2(f6(x5772,f3(f6(x5771,x5772))),f2(a8,a8))),f6(x5773,f3(x5773)))),
% 64.17/64.38 inference(scs_inference,[],[576,2])).
% 64.17/64.38 cnf(578,plain,
% 64.17/64.38 (E(f6(x5781,f6(x5782,f3(f6(x5781,x5782)))),f2(f2(a9,f2(a8,a8)),a8))),
% 64.17/64.38 inference(scs_inference,[],[297,575,576,2,3])).
% 64.17/64.38 cnf(579,plain,
% 64.17/64.38 (E(f2(f2(a9,f2(a8,a8)),a8),f6(x5791,f6(x5792,f3(f6(x5791,x5792)))))),
% 64.17/64.38 inference(scs_inference,[],[578,2])).
% 64.17/64.38 cnf(580,plain,
% 64.17/64.38 (E(f6(f2(x5801,f2(a8,a8)),f2(f6(x5802,f3(f6(x5801,x5802))),f2(a8,a8))),f2(a9,f2(a8,f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[577,562,578,2,3])).
% 64.17/64.38 cnf(582,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,f2(a8,a8))),f6(f2(x5821,f2(a8,a8)),f2(f6(x5822,f3(f6(x5821,x5822))),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[580,2])).
% 64.17/64.38 cnf(583,plain,
% 64.17/64.38 (E(f2(f2(a9,f2(a8,a8)),a8),f1(f1(a9)))),
% 64.17/64.38 inference(scs_inference,[],[579,120,580,2,3])).
% 64.17/64.38 cnf(585,plain,
% 64.17/64.38 (E(f1(f1(a9)),f2(f2(a9,f2(a8,a8)),a8))),
% 64.17/64.38 inference(scs_inference,[],[583,2])).
% 64.17/64.38 cnf(586,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f2(f6(f2(x5861,f2(a8,a8)),f2(f3(x5861),f2(a8,a8))),a8))),
% 64.17/64.38 inference(scs_inference,[],[216,312,583,2,3])).
% 64.17/64.38 cnf(588,plain,
% 64.17/64.38 (E(f2(f6(f2(x5881,f2(a8,a8)),f2(f3(x5881),f2(a8,a8))),a8),f2(f1(f1(a9)),a8))),
% 64.17/64.38 inference(scs_inference,[],[586,2])).
% 64.17/64.38 cnf(589,plain,
% 64.17/64.38 (E(f6(f2(f2(f1(x5891),f3(f2(x5891,x5892))),f2(a8,a8)),f2(f3(x5892),f2(a8,a8))),f3(x5892))),
% 64.17/64.38 inference(scs_inference,[],[559,31,586,2,3])).
% 64.17/64.38 cnf(592,plain,
% 64.17/64.38 (E(f2(f6(f2(x5921,f2(a8,a8)),f2(f3(x5921),f2(a8,a8))),a8),a9)),
% 64.17/64.38 inference(scs_inference,[],[453,588,589,2,3])).
% 64.17/64.38 cnf(593,plain,
% 64.17/64.38 (E(a9,f2(f6(f2(x5931,f2(a8,a8)),f2(f3(x5931),f2(a8,a8))),a8))),
% 64.17/64.38 inference(scs_inference,[],[592,2])).
% 64.17/64.38 cnf(594,plain,
% 64.17/64.38 (E(f2(f1(x5941),f1(x5942)),f2(f2(f2(f1(x5941),f1(x5942)),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[387,81,592,2,3])).
% 64.17/64.38 cnf(597,plain,
% 64.17/64.38 (E(f6(x5971,f3(x5971)),f2(f6(f2(x5972,f2(a8,a8)),f2(f3(x5972),f2(a8,a8))),a8))),
% 64.17/64.38 inference(scs_inference,[],[14,593,594,2,3])).
% 64.17/64.38 cnf(598,plain,
% 64.17/64.38 (E(f2(f6(f2(x5981,f2(a8,a8)),f2(f3(x5981),f2(a8,a8))),a8),f6(x5982,f3(x5982)))),
% 64.17/64.38 inference(scs_inference,[],[597,2])).
% 64.17/64.38 cnf(599,plain,
% 64.17/64.38 (E(f1(f6(x5991,x5992)),f2(f2(f1(f6(x5991,x5992)),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[357,45,597,2,3])).
% 64.17/64.38 cnf(602,plain,
% 64.17/64.38 (E(f2(f6(f2(x6021,f2(a8,a8)),f2(f3(x6021),f2(a8,a8))),a8),f2(f2(a9,a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[598,315,599,2,3])).
% 64.17/64.38 cnf(604,plain,
% 64.17/64.38 (E(f2(f2(a9,a8),a8),f2(f6(f2(x6041,f2(a8,a8)),f2(f3(x6041),f2(a8,a8))),a8))),
% 64.17/64.38 inference(scs_inference,[],[602,2])).
% 64.17/64.38 cnf(605,plain,
% 64.17/64.38 (E(f1(f1(a9)),f2(f2(f2(a9,a8),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[384,294,602,2,3])).
% 64.17/64.38 cnf(607,plain,
% 64.17/64.38 (E(f2(f2(f2(a9,a8),a8),a8),f1(f1(a9)))),
% 64.17/64.38 inference(scs_inference,[],[605,2])).
% 64.17/64.38 cnf(608,plain,
% 64.17/64.38 (E(f2(f2(a9,a8),a8),f2(f1(f1(a9)),a8))),
% 64.17/64.38 inference(scs_inference,[],[604,588,605,2,3])).
% 64.17/64.38 cnf(610,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f2(f2(a9,a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[608,2])).
% 64.17/64.38 cnf(611,plain,
% 64.17/64.38 (E(f6(f2(x6111,f2(x6112,x6113)),f2(x6114,f2(x6112,x6113))),f2(f2(f2(f6(x6111,x6114),f2(x6112,x6113)),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[165,264,608,2,3])).
% 64.17/64.38 cnf(613,plain,
% 64.17/64.38 (E(f2(f2(f2(f6(x6131,x6132),f2(x6133,x6134)),a8),a8),f6(f2(x6131,f2(x6133,x6134)),f2(x6132,f2(x6133,x6134))))),
% 64.17/64.38 inference(scs_inference,[],[611,2])).
% 64.17/64.38 cnf(614,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f1(f1(f2(a9,f2(a8,a8)))))),
% 64.17/64.38 inference(scs_inference,[],[610,126,611,2,3])).
% 64.17/64.38 cnf(616,plain,
% 64.17/64.38 (E(f1(f1(f2(a9,f2(a8,a8)))),f2(f1(f1(a9)),a8))),
% 64.17/64.38 inference(scs_inference,[],[614,2])).
% 64.17/64.38 cnf(617,plain,
% 64.17/64.38 (E(f1(f1(a9)),f2(f2(f2(f2(a9,a8),a8),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[585,390,614,2,3])).
% 64.17/64.38 cnf(620,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,a8)),f2(f1(f1(a9)),a8))),
% 64.17/64.38 inference(scs_inference,[],[616,96,617,2,3])).
% 64.17/64.38 cnf(622,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f2(a9,f2(a8,a8)))),
% 64.17/64.38 inference(scs_inference,[],[620,2])).
% 64.17/64.38 cnf(623,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f2(f2(f2(a9,a8),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[575,258,620,2,3])).
% 64.17/64.38 cnf(625,plain,
% 64.17/64.38 (E(f2(f2(f2(a9,a8),a8),a8),f2(f1(f1(a9)),a8))),
% 64.17/64.38 inference(scs_inference,[],[623,2])).
% 64.17/64.38 cnf(626,plain,
% 64.17/64.38 (E(f6(x6261,f6(x6262,f3(f6(x6261,x6262)))),f2(a9,f2(a8,a8)))),
% 64.17/64.38 inference(scs_inference,[],[622,297,623,2,3])).
% 64.17/64.38 cnf(627,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,a8)),f6(x6271,f6(x6272,f3(f6(x6271,x6272)))))),
% 64.17/64.38 inference(scs_inference,[],[626,2])).
% 64.17/64.38 cnf(628,plain,
% 64.17/64.38 (E(f2(f2(f2(a9,a8),a8),a8),f2(a9,f2(f2(f2(a8,a8),a8),a8)))),
% 64.17/64.38 inference(scs_inference,[],[625,550,626,2,3])).
% 64.17/64.38 cnf(629,plain,
% 64.17/64.38 (E(f2(a9,f2(f2(f2(a8,a8),a8),a8)),f2(f2(f2(a9,a8),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[628,2])).
% 64.17/64.38 cnf(630,plain,
% 64.17/64.38 (E(f2(f6(x6301,f3(x6301)),a8),f1(f1(f2(f2(a9,a8),a8))))),
% 64.17/64.38 inference(scs_inference,[],[504,159,628,2,3])).
% 64.17/64.38 cnf(633,plain,
% 64.17/64.38 (E(f2(a9,f2(f2(f2(a8,a8),a8),a8)),f2(a9,a8))),
% 64.17/64.38 inference(scs_inference,[],[507,629,630,2,3])).
% 64.17/64.38 cnf(634,plain,
% 64.17/64.38 (E(f2(a9,a8),f2(a9,f2(f2(f2(a8,a8),a8),a8)))),
% 64.17/64.38 inference(scs_inference,[],[633,2])).
% 64.17/64.38 cnf(635,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,a8)),f2(a9,a8))),
% 64.17/64.38 inference(scs_inference,[],[627,234,633,2,3])).
% 64.17/64.38 cnf(637,plain,
% 64.17/64.38 (E(f2(a9,a8),f2(a9,f2(a8,a8)))),
% 64.17/64.38 inference(scs_inference,[],[635,2])).
% 64.17/64.38 cnf(638,plain,
% 64.17/64.38 (E(f6(x6381,f3(x6381)),f1(f1(f6(x6382,f3(x6382)))))),
% 64.17/64.38 inference(scs_inference,[],[14,162,635,2,3])).
% 64.17/64.38 cnf(639,plain,
% 64.17/64.38 (E(f1(f1(f6(x6391,f3(x6391)))),f6(x6392,f3(x6392)))),
% 64.17/64.38 inference(scs_inference,[],[638,2])).
% 64.17/64.38 cnf(640,plain,
% 64.17/64.38 (E(f2(a9,a8),f2(f2(f2(f2(a9,a8),a8),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[637,438,638,2,3])).
% 64.17/64.38 cnf(642,plain,
% 64.17/64.38 (E(f2(f2(f2(f2(a9,a8),a8),a8),a8),f2(a9,a8))),
% 64.17/64.38 inference(scs_inference,[],[640,2])).
% 64.17/64.38 cnf(643,plain,
% 64.17/64.38 (E(f1(f1(f6(x6431,f3(x6431)))),f2(a9,f2(a8,f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[639,562,640,2,3])).
% 64.17/64.38 cnf(645,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,f2(a8,a8))),f1(f1(f6(x6451,f3(x6451)))))),
% 64.17/64.38 inference(scs_inference,[],[643,2])).
% 64.17/64.38 cnf(646,plain,
% 64.17/64.38 (E(f2(f3(x6461),a8),f6(f2(f2(f1(x6462),f3(f2(x6462,x6461))),f2(a8,a8)),f2(f3(x6461),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[381,85,643,2,3])).
% 64.17/64.38 cnf(648,plain,
% 64.17/64.38 (E(f6(f2(f2(f1(x6481),f3(f2(x6481,x6482))),f2(a8,a8)),f2(f3(x6482),f2(a8,a8))),f2(f3(x6482),a8))),
% 64.17/64.38 inference(scs_inference,[],[646,2])).
% 64.17/64.38 cnf(649,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,f2(a8,a8))),f2(f2(a9,a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[645,300,646,2,3])).
% 64.17/64.38 cnf(651,plain,
% 64.17/64.38 (E(f2(f2(a9,a8),a8),f2(a9,f2(a8,f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[649,2])).
% 64.17/64.38 cnf(652,plain,
% 64.17/64.38 (E(f2(a9,a8),f2(f2(f2(a9,f2(f2(a8,a8),a8)),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[634,435,649,2,3])).
% 64.17/64.38 cnf(655,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f2(a9,f2(a8,f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[651,610,652,2,3])).
% 64.17/64.38 cnf(656,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,f2(a8,a8))),f2(f1(f1(a9)),a8))),
% 64.17/64.38 inference(scs_inference,[],[655,2])).
% 64.17/64.38 cnf(657,plain,
% 64.17/64.38 (E(f2(f2(a9,a8),a8),f6(f2(x6571,f2(a8,a8)),f2(f6(x6572,f3(f6(x6571,x6572))),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[582,651,655,2,3])).
% 64.17/64.38 cnf(658,plain,
% 64.17/64.38 (E(f6(f2(x6581,f2(a8,a8)),f2(f6(x6582,f3(f6(x6581,x6582))),f2(a8,a8))),f2(f2(a9,a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[657,2])).
% 64.17/64.38 cnf(659,plain,
% 64.17/64.38 (E(f2(f2(f2(f2(a9,a8),a8),a8),a8),f2(f1(f1(a9)),a8))),
% 64.17/64.38 inference(scs_inference,[],[656,481,657,2,3])).
% 64.17/64.38 cnf(661,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f2(f2(f2(f2(a9,a8),a8),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[659,2])).
% 64.17/64.38 cnf(662,plain,
% 64.17/64.38 (E(f2(f2(f2(f6(x6621,f6(x6622,x6623)),f2(a8,a8)),a8),a8),f6(f6(x6621,x6622),x6623))),
% 64.17/64.38 inference(scs_inference,[],[613,565,659,2,3])).
% 64.17/64.38 cnf(665,plain,
% 64.17/64.38 (E(f6(f6(x6651,x6652),x6653),f2(f2(f2(f6(x6651,f6(x6652,x6653)),f2(a8,a8)),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[662,2])).
% 64.17/64.38 cnf(666,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f2(a9,a8))),
% 64.17/64.38 inference(scs_inference,[],[661,642,662,2,3])).
% 64.17/64.38 cnf(667,plain,
% 64.17/64.38 (E(f2(a9,a8),f2(f1(f1(a9)),a8))),
% 64.17/64.38 inference(scs_inference,[],[666,2])).
% 64.17/64.38 cnf(668,plain,
% 64.17/64.38 (E(f2(a9,a8),f1(f1(f2(f2(a9,a8),a8))))),
% 64.17/64.38 inference(scs_inference,[],[637,159,666,2,3])).
% 64.17/64.38 cnf(670,plain,
% 64.17/64.38 (E(f1(f1(f2(f2(a9,a8),a8))),f2(a9,a8))),
% 64.17/64.38 inference(scs_inference,[],[668,2])).
% 64.17/64.38 cnf(671,plain,
% 64.17/64.38 (E(f2(a9,a8),f2(f2(a9,f2(a8,a8)),a8))),
% 64.17/64.38 inference(scs_inference,[],[667,575,668,2,3])).
% 64.17/64.38 cnf(672,plain,
% 64.17/64.38 (E(f2(f2(a9,f2(a8,a8)),a8),f2(a9,a8))),
% 64.17/64.38 inference(scs_inference,[],[671,2])).
% 64.17/64.38 cnf(673,plain,
% 64.17/64.38 (E(f1(f1(f2(f2(a9,a8),a8))),f2(f1(f1(a9)),a8))),
% 64.17/64.38 inference(scs_inference,[],[670,667,671,2,3])).
% 64.17/64.38 cnf(674,plain,
% 64.17/64.38 (E(f2(f1(f1(a9)),a8),f1(f1(f2(f2(a9,a8),a8))))),
% 64.17/64.38 inference(scs_inference,[],[673,2])).
% 64.17/64.38 cnf(675,plain,
% 64.17/64.38 (E(f2(f2(a9,f2(a8,a8)),a8),f2(a9,f2(f2(f2(a8,a8),a8),a8)))),
% 64.17/64.38 inference(scs_inference,[],[672,634,673,2,3])).
% 64.17/64.38 cnf(677,plain,
% 64.17/64.38 (E(f2(f2(f2(a9,a8),a8),a8),f1(f1(f2(f2(a9,a8),a8))))),
% 64.17/64.38 inference(scs_inference,[],[674,625,675,2,3])).
% 64.17/64.38 cnf(678,plain,
% 64.17/64.38 (E(f1(f1(f2(f2(a9,a8),a8))),f2(f2(f2(a9,a8),a8),a8))),
% 64.17/64.38 inference(scs_inference,[],[677,2])).
% 64.17/64.38 cnf(679,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,f2(a8,a8))),f1(f1(f2(f2(a9,a8),a8))))),
% 64.17/64.38 inference(scs_inference,[],[674,656,677,2,3])).
% 64.17/64.38 cnf(681,plain,
% 64.17/64.38 (E(f1(f1(f2(f2(a9,a8),a8))),a9)),
% 64.17/64.38 inference(scs_inference,[],[678,459,679,2,3])).
% 64.17/64.38 cnf(683,plain,
% 64.17/64.38 (E(f1(f1(f2(f2(a9,a8),a8))),f1(f1(a9)))),
% 64.17/64.38 inference(scs_inference,[],[607,678,681,2,3])).
% 64.17/64.38 cnf(685,plain,
% 64.17/64.38 (E(f1(f1(f2(a9,f2(a8,a8)))),a9)),
% 64.17/64.38 inference(scs_inference,[],[453,616,683,2,3])).
% 64.17/64.38 cnf(686,plain,
% 64.17/64.38 (E(a9,f1(f1(f2(a9,f2(a8,a8)))))),
% 64.17/64.38 inference(scs_inference,[],[685,2])).
% 64.17/64.38 cnf(687,plain,
% 64.17/64.38 (E(f1(f1(f6(x6871,f3(x6871)))),f2(a9,f2(a8,a8)))),
% 64.17/64.38 inference(scs_inference,[],[622,189,685,2,3])).
% 64.17/64.38 cnf(688,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,a8)),f1(f1(f6(x6881,f3(x6881)))))),
% 64.17/64.38 inference(scs_inference,[],[687,2])).
% 64.17/64.38 cnf(689,plain,
% 64.17/64.38 (E(f6(x6891,f3(x6891)),f1(f1(f2(a9,f2(a8,a8)))))),
% 64.17/64.38 inference(scs_inference,[],[14,686,687,2,3])).
% 64.17/64.38 cnf(690,plain,
% 64.17/64.38 (E(f1(f1(f2(a9,f2(a8,a8)))),f6(x6901,f3(x6901)))),
% 64.17/64.38 inference(scs_inference,[],[689,2])).
% 64.17/64.38 cnf(691,plain,
% 64.17/64.38 (E(f2(a9,f2(a8,a8)),f6(x6911,f3(x6911)))),
% 64.17/64.38 inference(scs_inference,[],[688,639,689,2,3])).
% 64.17/64.38 cnf(694,plain,
% 64.17/64.38 (E(f1(f1(f2(a9,f2(a8,a8)))),f2(a9,a8))),
% 64.17/64.38 inference(scs_inference,[],[690,270,691,2,3])).
% 64.17/64.38 cnf(697,plain,
% 64.17/64.38 (E(f2(f6(x6971,f3(x6971)),a8),f2(a9,f2(f2(f2(a8,a8),a8),a8)))),
% 64.17/64.38 inference(scs_inference,[],[550,210,694,2,3])).
% 64.17/64.38 cnf(699,plain,
% 64.17/64.38 (E(f6(f2(x6991,f2(a8,a8)),f2(f6(x6992,f3(f6(x6991,x6992))),f2(a8,a8))),f2(f2(a9,f2(a8,a8)),a8))),
% 64.17/64.38 inference(scs_inference,[],[658,252,697,2,3])).
% 64.17/64.38 cnf(701,plain,
% 64.17/64.38 (E(f2(f2(a9,f2(a8,a8)),a8),f6(f2(x7011,f2(a8,a8)),f2(f6(x7012,f3(f6(x7011,x7012))),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[699,2])).
% 64.17/64.38 cnf(702,plain,
% 64.17/64.38 (E(f2(f1(f6(x7021,x7022)),a8),f2(f6(f2(f1(x7021),f2(a8,a8)),f2(f1(x7022),f2(a8,a8))),a8))),
% 64.17/64.38 inference(scs_inference,[],[219,312,699,2,3])).
% 64.17/64.38 cnf(704,plain,
% 64.17/64.38 (E(f2(f6(f2(f1(x7041),f2(a8,a8)),f2(f1(x7042),f2(a8,a8))),a8),f2(f1(f6(x7041,x7042)),a8))),
% 64.17/64.38 inference(scs_inference,[],[702,2])).
% 64.17/64.38 cnf(705,plain,
% 64.17/64.38 (E(f2(f6(f6(x7051,x7052),x7053),a8),f6(f2(x7051,f2(a8,a8)),f2(f6(x7052,x7053),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[285,85,702,2,3])).
% 64.17/64.38 cnf(707,plain,
% 64.17/64.38 (E(f6(f2(x7071,f2(a8,a8)),f2(f6(x7072,x7073),f2(a8,a8))),f2(f6(f6(x7071,x7072),x7073),a8))),
% 64.17/64.38 inference(scs_inference,[],[705,2])).
% 64.17/64.38 cnf(708,plain,
% 64.17/64.38 (E(f6(f2(f1(x7081),f2(a8,a8)),f2(f1(x7082),f2(a8,a8))),f2(f1(f6(x7081,x7082)),a8))),
% 64.17/64.38 inference(scs_inference,[],[704,31,705,2,3])).
% 64.17/64.38 cnf(710,plain,
% 64.17/64.38 (E(f2(f1(f6(x7101,x7102)),a8),f6(f2(f1(x7101),f2(a8,a8)),f2(f1(x7102),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[708,2])).
% 64.17/64.38 cnf(711,plain,
% 64.17/64.38 (E(f2(f2(a9,f2(a8,a8)),a8),f2(f6(f6(x7111,x7112),f3(f6(x7111,x7112))),a8))),
% 64.17/64.38 inference(scs_inference,[],[701,707,708,2,3])).
% 64.17/64.38 cnf(714,plain,
% 64.17/64.38 (E(f1(f1(f6(f1(x7141),f1(x7142)))),f6(f2(f1(x7141),f2(a8,a8)),f2(f1(x7142),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[177,710,711,2,3])).
% 64.17/64.38 cnf(716,plain,
% 64.17/64.38 (E(f6(f2(f1(x7161),f2(a8,a8)),f2(f1(x7162),f2(a8,a8))),f1(f1(f6(f1(x7161),f1(x7162)))))),
% 64.17/64.38 inference(scs_inference,[],[714,2])).
% 64.17/64.38 cnf(717,plain,
% 64.17/64.38 (E(f6(f1(x7171),f1(x7172)),f6(f2(f1(x7171),f2(a8,a8)),f2(f1(x7172),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[246,710,714,2,3])).
% 64.17/64.38 cnf(719,plain,
% 64.17/64.38 (E(f6(f2(f1(x7191),f2(a8,a8)),f2(f1(x7192),f2(a8,a8))),f6(f1(x7191),f1(x7192)))),
% 64.17/64.38 inference(scs_inference,[],[717,2])).
% 64.17/64.38 cnf(720,plain,
% 64.17/64.38 (E(f6(f2(f1(x7201),f2(a8,a8)),f2(f1(x7202),f2(a8,a8))),f6(f2(f1(x7201),a8),f2(f1(x7202),a8)))),
% 64.17/64.38 inference(scs_inference,[],[716,528,717,2,3])).
% 64.17/64.38 cnf(722,plain,
% 64.17/64.38 (E(f6(f2(f1(x7221),a8),f2(f1(x7222),a8)),f6(f2(f1(x7221),f2(a8,a8)),f2(f1(x7222),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[720,2])).
% 64.17/64.38 cnf(723,plain,
% 64.17/64.38 (E(f6(f2(f1(x7231),f2(a8,a8)),f2(f1(x7232),f2(a8,a8))),f1(f1(f1(f6(x7231,x7232)))))),
% 64.17/64.38 inference(scs_inference,[],[123,719,720,2,3])).
% 64.17/64.38 cnf(725,plain,
% 64.17/64.38 (E(f1(f1(f1(f6(x7251,x7252)))),f6(f2(f1(x7251),f2(a8,a8)),f2(f1(x7252),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[723,2])).
% 64.17/64.38 cnf(736,plain,
% 64.17/64.38 (E(f6(f6(f6(x7361,x7362),x7363),x7364),f6(f2(x7361,a8),f2(f6(x7362,f6(x7363,x7364)),a8)))),
% 64.17/64.38 inference(scs_inference,[],[129,136,3,2])).
% 64.17/64.38 cnf(751,plain,
% 64.17/64.38 (E(f6(f2(x7511,f2(f2(a8,a8),a8)),f2(f6(x7512,x7513),f2(f2(a8,a8),a8))),f6(f6(x7511,x7512),x7513))),
% 64.17/64.38 inference(scs_inference,[],[665,163,3,2])).
% 64.17/64.38 cnf(772,plain,
% 64.17/64.38 (E(f6(f2(f6(x7721,x7722),f2(f2(a8,a8),a8)),f2(x7723,f2(f2(a8,a8),a8))),f6(f6(x7723,x7721),x7722))),
% 64.17/64.38 inference(scs_inference,[],[15,751,3])).
% 64.17/64.38 cnf(774,plain,
% 64.17/64.38 (E(f6(f6(x7741,x7742),x7743),f6(f2(f6(x7742,x7743),f2(f2(a8,a8),a8)),f2(x7741,f2(f2(a8,a8),a8))))),
% 64.17/64.38 inference(scs_inference,[],[772,2])).
% 64.17/64.38 cnf(775,plain,
% 64.17/64.38 (E(f6(f2(f6(x7751,f3(f6(x7752,x7751))),a8),f2(x7752,a8)),f2(a9,a8))),
% 64.17/64.38 inference(scs_inference,[],[15,402,772,2,3])).
% 64.17/64.38 cnf(778,plain,
% 64.17/64.38 (E(f6(x7781,f6(x7782,x7783)),f6(f2(f6(x7783,x7781),f2(f2(a8,a8),a8)),f2(x7782,f2(f2(a8,a8),a8))))),
% 64.17/64.38 inference(scs_inference,[],[15,774,775,2,3])).
% 64.17/64.38 cnf(781,plain,
% 64.17/64.38 (E(f6(f2(f6(x7811,x7812),f2(f2(a8,a8),a8)),f2(x7813,f2(f2(a8,a8),a8))),f6(x7812,f6(x7813,x7811)))),
% 64.17/64.38 inference(scs_inference,[],[778,2])).
% 64.17/64.38 cnf(782,plain,
% 64.17/64.38 (E(f6(f2(f1(x7821),a8),f2(f1(x7822),a8)),f6(f2(f1(x7822),f2(a8,a8)),f2(f1(x7821),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[15,722,778,2,3])).
% 64.17/64.38 cnf(785,plain,
% 64.17/64.38 (E(f6(f2(x7851,f2(f2(a8,a8),a8)),f2(f6(x7852,x7853),f2(f2(a8,a8),a8))),f6(x7853,f6(x7851,x7852)))),
% 64.17/64.38 inference(scs_inference,[],[15,781,782,2,3])).
% 64.17/64.38 cnf(788,plain,
% 64.17/64.38 (E(f6(f2(f1(x7881),a8),f2(f1(x7882),a8)),f1(f1(f1(f6(x7882,x7881)))))),
% 64.17/64.38 inference(scs_inference,[],[15,144,785,2,3])).
% 64.17/64.38 cnf(790,plain,
% 64.17/64.38 (E(f1(f1(f1(f6(x7901,x7902)))),f6(f2(f1(x7902),a8),f2(f1(x7901),a8)))),
% 64.17/64.38 inference(scs_inference,[],[788,2])).
% 64.17/64.38 cnf(791,plain,
% 64.17/64.38 (E(f2(f6(f1(x7911),f1(x7912)),a8),f6(f2(f1(x7911),f2(a8,a8)),f2(f1(x7912),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[725,111,788,2,3])).
% 64.17/64.38 cnf(793,plain,
% 64.17/64.38 (E(f6(f2(f1(x7931),f2(a8,a8)),f2(f1(x7932),f2(a8,a8))),f2(f6(f1(x7931),f1(x7932)),a8))),
% 64.17/64.38 inference(scs_inference,[],[791,2])).
% 64.17/64.38 cnf(794,plain,
% 64.17/64.38 (E(f6(f1(x7941),f1(x7942)),f6(f2(f1(x7942),a8),f2(f1(x7941),a8)))),
% 64.17/64.38 inference(scs_inference,[],[790,123,791,2,3])).
% 64.17/64.38 cnf(797,plain,
% 64.17/64.38 (E(f6(x7971,f6(f6(x7972,x7973),x7974)),f6(f2(x7972,a8),f2(f6(x7973,f6(x7974,x7971)),a8)))),
% 64.17/64.38 inference(scs_inference,[],[15,736,794,2,3])).
% 64.17/64.38 cnf(800,plain,
% 64.17/64.38 (E(f6(f2(x8001,a8),f2(f6(x8002,f6(x8003,x8004)),a8)),f6(x8004,f6(f6(x8001,x8002),x8003)))),
% 64.17/64.38 inference(scs_inference,[],[797,2])).
% 64.17/64.38 cnf(801,plain,
% 64.17/64.38 (E(f6(f2(f3(x8011),f2(a8,a8)),f2(f2(f1(x8012),f3(f2(x8012,x8011))),f2(a8,a8))),f2(f3(x8011),a8))),
% 64.17/64.38 inference(scs_inference,[],[15,648,797,2,3])).
% 64.17/64.38 cnf(804,plain,
% 64.17/64.38 (E(f6(f2(f6(x8041,f6(x8042,x8043)),a8),f2(x8044,a8)),f6(x8043,f6(f6(x8044,x8041),x8042)))),
% 64.17/64.38 inference(scs_inference,[],[15,800,801,2,3])).
% 64.17/64.38 cnf(806,plain,
% 64.17/64.38 (E(f6(x8061,f6(f6(x8062,x8063),x8064)),f6(f2(f6(x8063,f6(x8064,x8061)),a8),f2(x8062,a8)))),
% 64.17/64.38 inference(scs_inference,[],[804,2])).
% 64.17/64.38 cnf(807,plain,
% 64.17/64.38 (E(f6(f6(x8071,f3(f6(x8072,x8071))),x8072),f2(f6(x8073,f3(x8073)),a8))),
% 64.17/64.38 inference(scs_inference,[],[15,525,804,2,3])).
% 64.17/64.38 cnf(811,plain,
% 64.17/64.38 (E(f6(f6(f6(x8111,x8112),x8113),x8114),f6(f2(f6(x8112,f6(x8113,x8114)),a8),f2(x8111,a8)))),
% 64.17/64.38 inference(scs_inference,[],[15,806,807,2,3])).
% 64.17/64.38 cnf(815,plain,
% 64.17/64.38 (E(f6(f2(f1(x8151),f2(a8,a8)),f2(f1(x8152),f2(a8,a8))),f2(f6(f1(x8152),f1(x8151)),a8))),
% 64.17/64.38 inference(scs_inference,[],[15,793,811,2,3])).
% 64.17/64.38 cnf(817,plain,
% 64.17/64.38 (E(f2(f6(f1(x8171),f1(x8172)),a8),f6(f2(f1(x8172),f2(a8,a8)),f2(f1(x8171),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[815,2])).
% 64.17/64.38 cnf(818,plain,
% 64.17/64.38 (E(f6(x8181,f6(x8182,x8183)),f2(f6(f2(x8182,a8),f2(f6(x8183,x8181),a8)),a8))),
% 64.17/64.38 inference(scs_inference,[],[15,336,815,2,3])).
% 64.17/64.38 cnf(821,plain,
% 64.17/64.38 (E(f2(f6(f2(x8211,a8),f2(f6(x8212,x8213),a8)),a8),f6(x8213,f6(x8211,x8212)))),
% 64.17/64.38 inference(scs_inference,[],[818,2])).
% 64.17/64.38 cnf(822,plain,
% 64.17/64.38 (E(f2(f2(f1(f6(x8221,x8222)),a8),a8),f6(f2(f1(x8222),f2(a8,a8)),f2(f1(x8221),f2(a8,a8))))),
% 64.17/64.38 inference(scs_inference,[],[817,363,818,2,3])).
% 64.17/64.38 cnf(825,plain,
% 64.17/64.38 (E(f2(f6(f6(x8251,x8252),x8253),a8),f6(x8253,f6(x8251,x8252)))),
% 64.17/64.38 inference(scs_inference,[],[821,267,822,2,3])).
% 64.17/64.38 cnf(1232,plain,
% 64.17/64.38 (E(f3(f6(a4,a5)),f3(a5))),
% 64.17/64.38 inference(scs_inference,[],[11,4,7])).
% 64.17/64.38 cnf(1254,plain,
% 64.17/64.38 (E(f6(a5,x12541),f6(f6(a7,a5),x12541))),
% 64.17/64.38 inference(scs_inference,[],[28,9,7,6,4,8,5])).
% 64.17/64.38 cnf(1274,plain,
% 64.17/64.38 (~E(f2(f6(a5,a4),a8),f6(f6(a4,a7),a5))),
% 64.17/64.38 inference(scs_inference,[],[1232,72,9,7,4,8,6,5,2])).
% 64.17/64.38 cnf(1353,plain,
% 64.17/64.38 (E(f2(f6(a5,x13531),x13532),f2(f6(f6(a7,a5),x13531),x13532))),
% 64.17/64.38 inference(scs_inference,[],[1254,7,9,4,8])).
% 64.17/64.38 cnf(1829,plain,
% 64.17/64.38 (E(f2(x18291,f6(a7,a5)),f2(x18291,a5))),
% 64.17/64.38 inference(scs_inference,[],[12,4,9])).
% 64.17/64.38 cnf(1834,plain,
% 64.17/64.38 (~E(f2(f6(f6(a7,a5),a4),a8),f6(f6(a4,a7),a5))),
% 64.17/64.38 inference(scs_inference,[],[12,1353,1274,4,9,6,5,7,8,3])).
% 64.17/64.38 cnf(1843,plain,
% 64.17/64.38 ($false),
% 64.17/64.38 inference(scs_inference,[],[1829,1834,825,61,4,9,6,5,7,8,3]),
% 64.17/64.38 ['proof']).
% 64.17/64.38 % SZS output end Proof
% 64.17/64.38 % Total time :63.510000s
%------------------------------------------------------------------------------