%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN007-5 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n028.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 07:26:50 EDT 2024
% Result : Unsatisfiable 249.39s 249.38s
% Output : CNFRefutation 249.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : HEN007-5 : TPTP v8.2.0. Released v1.0.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n028.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Sat Jun 22 05:35:54 EDT 2024
% 0.12/0.32 % CPUTime :
% 0.49/0.56 start to proof:theBenchmark
% 249.39/249.36 %-------------------------------------------
% 249.39/249.36 % File :CSE---1.7
% 249.39/249.36 % Problem :theBenchmark
% 249.39/249.36 % Transform :cnf
% 249.39/249.36 % Format :tptp:raw
% 249.39/249.36 % Command :java -jar mcs_scs.jar %d %s
% 249.39/249.36
% 249.39/249.36 % Result :Theorem 248.790000s
% 249.39/249.36 % Output :CNFRefutation 248.790000s
% 249.39/249.36 %-------------------------------------------
% 249.39/249.37 %--------------------------------------------------------------------------
% 249.39/249.37 % File : HEN007-5 : TPTP v8.2.0. Released v1.0.0.
% 249.39/249.37 % Domain : Henkin Models
% 249.39/249.37 % Problem : X <= Y => Z/Y <= Z/X
% 249.39/249.37 % Version : [MOW76] (equality) axioms : Reduced & Augmented > Complete.
% 249.39/249.37 % English :
% 249.39/249.37
% 249.39/249.37 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 249.39/249.37 % Source : [ANL]
% 249.39/249.37 % Names : hp7.ver3.in [ANL]
% 249.39/249.38
% 249.39/249.38 % Status : Unsatisfiable
% 249.39/249.38 % Rating : 0.07 v8.2.0, 0.06 v8.1.0, 0.11 v7.5.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.09 v7.0.0, 0.00 v6.4.0, 0.14 v6.3.0, 0.10 v6.2.0, 0.30 v6.1.0, 0.18 v6.0.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.11 v5.3.0, 0.20 v5.2.0, 0.12 v5.1.0, 0.22 v5.0.0, 0.20 v4.1.0, 0.22 v4.0.1, 0.25 v4.0.0, 0.14 v3.7.0, 0.00 v3.3.0, 0.11 v3.2.0, 0.00 v2.0.0
% 249.39/249.38 % Syntax : Number of clauses : 8 ( 6 unt; 0 nHn; 4 RR)
% 249.39/249.38 % Number of literals : 12 ( 12 equ; 5 neg)
% 249.39/249.38 % Maximal clause size : 3 ( 1 avg)
% 249.39/249.38 % Maximal term depth : 4 ( 1 avg)
% 249.39/249.38 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 249.39/249.38 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% 249.39/249.38 % Number of variables : 12 ( 3 sgn)
% 249.39/249.38 % SPC : CNF_UNS_RFO_PEQ_NUE
% 249.39/249.38
% 249.39/249.38 % Comments : less_equal replaced by divides
% 249.39/249.38 %--------------------------------------------------------------------------
% 249.39/249.38 %----Include Henkin model axioms, for the equality formulation with
% 249.39/249.38 %----less_equals removed.
% 249.39/249.38 include('Axioms/HEN003-0.ax').
% 249.39/249.38 %--------------------------------------------------------------------------
% 249.39/249.38 cnf(transitivity_of_divide_to_zero,axiom,
% 249.39/249.38 ( divide(X,Y) != zero
% 249.39/249.38 | divide(Y,Z) != zero
% 249.39/249.38 | divide(X,Z) = zero ) ).
% 249.39/249.38
% 249.39/249.38 cnf(a_divide_b_is_zero,hypothesis,
% 249.39/249.38 divide(a,b) = zero ).
% 249.39/249.38
% 249.39/249.38 cnf(prove_property_of_divide2,negated_conjecture,
% 249.39/249.38 divide(divide(c,b),divide(c,a)) != zero ).
% 249.39/249.38
% 249.39/249.38 %--------------------------------------------------------------------------
% 249.39/249.38 %-------------------------------------------
% 249.39/249.38 % Proof found
% 249.39/249.38 % SZS status Theorem for theBenchmark
% 249.39/249.38 % SZS output start Proof
% 249.42/249.38 %ClaNum:13(EqnAxiom:5)
% 249.42/249.38 %VarNum:24(SingletonVarNum:12)
% 249.42/249.38 %MaxLitNum:3
% 249.42/249.38 %MaxfuncDepth:3
% 249.42/249.38 %SharedTerms:11
% 249.42/249.38 %goalClause: 11
% 249.42/249.38 %singleGoalClaCount:1
% 249.42/249.38 [6]E(f3(a1,a2),a5)
% 249.42/249.38 [11]~E(f3(f3(a4,a2),f3(a4,a1)),a5)
% 249.42/249.38 [7]E(f3(x71,a6),a5)
% 249.42/249.38 [8]E(f3(a5,x81),a5)
% 249.42/249.38 [9]E(f3(f3(x91,x92),x91),a5)
% 249.42/249.38 [10]E(f3(f3(f3(x101,x102),f3(x103,x102)),f3(f3(x101,x103),x102)),a5)
% 249.42/249.38 [12]E(x121,x122)+~E(f3(x122,x121),a5)+~E(f3(x121,x122),a5)
% 249.42/249.38 [13]~E(f3(x131,x133),a5)+E(f3(x131,x132),a5)+~E(f3(x133,x132),a5)
% 249.42/249.38 %EqnAxiom
% 249.42/249.38 [1]E(x11,x11)
% 249.42/249.38 [2]E(x22,x21)+~E(x21,x22)
% 249.42/249.38 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 249.42/249.39 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 249.42/249.39 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 249.42/249.39
% 249.42/249.39 %-------------------------------------------
% 249.42/249.40 cnf(14,plain,
% 249.42/249.40 (E(a5,f3(x141,a6))),
% 249.42/249.40 inference(scs_inference,[],[7,2])).
% 249.42/249.40 cnf(15,plain,
% 249.42/249.40 (E(a5,f3(a5,x151))),
% 249.42/249.40 inference(scs_inference,[],[7,8,9,2,12])).
% 249.42/249.40 cnf(19,plain,
% 249.42/249.40 (~E(f3(f3(a4,a2),f3(a4,a1)),f3(x191,a6))),
% 249.42/249.40 inference(scs_inference,[],[11,7,8,9,2,12,3])).
% 249.42/249.40 cnf(21,plain,
% 249.42/249.40 (E(a5,f3(a1,a2))),
% 249.42/249.40 inference(scs_inference,[],[6,2])).
% 249.42/249.40 cnf(22,plain,
% 249.42/249.40 (E(f3(f3(f3(x221,x222),f3(x223,x222)),f3(x221,x223)),a5)),
% 249.42/249.40 inference(scs_inference,[],[6,10,9,2,13])).
% 249.42/249.40 cnf(28,plain,
% 249.42/249.40 (E(a5,f3(f3(f3(x281,x282),f3(x283,x282)),f3(x281,x283)))),
% 249.42/249.40 inference(scs_inference,[],[22,2])).
% 249.42/249.40 cnf(29,plain,
% 249.42/249.40 (E(f3(f3(f3(x291,x292),f3(x293,x292)),x291),a5)),
% 249.42/249.40 inference(scs_inference,[],[22,9,2,13])).
% 249.42/249.40 cnf(32,plain,
% 249.42/249.40 (E(a5,f3(f3(a5,x321),f3(x322,x321)))),
% 249.42/249.40 inference(scs_inference,[],[22,8,9,2,13,12])).
% 249.42/249.40 cnf(37,plain,
% 249.42/249.40 (E(f3(f3(a5,x371),f3(x372,x371)),a5)),
% 249.42/249.40 inference(scs_inference,[],[32,2])).
% 249.42/249.40 cnf(38,plain,
% 249.42/249.40 (E(f3(f3(f3(f3(f3(x381,x382),f3(x383,x382)),x384),f3(x385,x384)),f3(x381,x383)),a5)),
% 249.42/249.40 inference(scs_inference,[],[32,29,22,2,13])).
% 249.42/249.40 cnf(39,plain,
% 249.42/249.40 (E(f3(f3(f3(x391,x392),f3(x393,x392)),x391),a5)),
% 249.42/249.40 inference(rename_variables,[],[29])).
% 249.42/249.40 cnf(41,plain,
% 249.42/249.40 (E(f3(f3(f3(x411,x412),f3(x413,x412)),x411),f3(f3(a5,x414),f3(x415,x414)))),
% 249.42/249.40 inference(scs_inference,[],[32,29,39,22,2,13,3])).
% 249.42/249.40 cnf(42,plain,
% 249.42/249.40 (E(f3(x421,x422),f3(f3(x421,x423),f3(x422,x423)))+~E(f3(f3(x421,x422),f3(f3(x421,x423),f3(x422,x423))),a5)),
% 249.42/249.40 inference(scs_inference,[],[32,29,39,22,2,13,3,12])).
% 249.42/249.40 cnf(44,plain,
% 249.42/249.40 (E(f3(f3(a5,x441),f3(x442,x441)),f3(f3(f3(x443,x444),f3(x445,x444)),x443))),
% 249.42/249.40 inference(scs_inference,[],[41,2])).
% 249.42/249.40 cnf(45,plain,
% 249.42/249.40 (E(f3(f3(a5,f3(x451,x452)),f3(x453,x454)),a5)),
% 249.42/249.40 inference(scs_inference,[],[41,38,37,2,13])).
% 249.42/249.40 cnf(46,plain,
% 249.42/249.40 (E(f3(f3(a5,x461),f3(x462,x461)),a5)),
% 249.42/249.40 inference(rename_variables,[],[37])).
% 249.42/249.40 cnf(48,plain,
% 249.42/249.40 (E(f3(a5,f3(x481,x482)),f3(f3(f3(a5,f3(x481,x482)),x482),f3(x481,x482)))),
% 249.42/249.40 inference(scs_inference,[],[41,38,37,46,29,2,13,12])).
% 249.42/249.40 cnf(50,plain,
% 249.42/249.40 (E(f3(f3(a5,x501),f3(x502,x501)),a5)),
% 249.42/249.40 inference(rename_variables,[],[37])).
% 249.42/249.40 cnf(53,plain,
% 249.42/249.40 (E(f3(a5,f3(x531,x532)),f3(f3(a5,x533),f3(f3(x531,x532),x533)))),
% 249.42/249.40 inference(scs_inference,[],[11,41,38,37,46,50,29,2,13,12,3,42])).
% 249.42/249.40 cnf(57,plain,
% 249.42/249.40 (E(f3(f3(a5,f3(x571,x572)),x573),a5)),
% 249.42/249.40 inference(scs_inference,[],[48,45,29,2,13])).
% 249.42/249.40 cnf(58,plain,
% 249.42/249.40 (E(f3(f3(a5,f3(x581,x582)),f3(x583,x584)),a5)),
% 249.42/249.40 inference(rename_variables,[],[45])).
% 249.42/249.40 cnf(60,plain,
% 249.42/249.40 (E(f3(a5,f3(x601,x602)),f3(f3(f3(a5,f3(x601,x602)),x603),f3(x604,x603)))),
% 249.42/249.40 inference(scs_inference,[],[48,45,58,29,2,13,12])).
% 249.42/249.40 cnf(66,plain,
% 249.42/249.40 (E(f3(f3(f3(a5,f3(x661,x662)),x663),f3(x664,x663)),f3(a5,f3(x661,x662)))),
% 249.42/249.40 inference(scs_inference,[],[60,2])).
% 249.42/249.40 cnf(67,plain,
% 249.42/249.40 (E(f3(a5,f3(x671,x672)),f3(f3(a5,f3(x671,x672)),x673))),
% 249.42/249.40 inference(scs_inference,[],[60,57,9,2,12])).
% 249.42/249.40 cnf(73,plain,
% 249.42/249.40 (E(f3(f3(a5,f3(x731,x732)),x733),f3(a5,f3(x731,x732)))),
% 249.42/249.40 inference(scs_inference,[],[67,2])).
% 249.42/249.40 cnf(74,plain,
% 249.42/249.40 (E(f3(a5,x741),f3(f3(a5,x741),x741))),
% 249.42/249.40 inference(scs_inference,[],[67,37,9,2,12])).
% 249.42/249.40 cnf(78,plain,
% 249.42/249.40 (~E(f3(f3(a4,a2),f3(a4,a1)),f3(a5,f3(x781,x782)))),
% 249.42/249.40 inference(scs_inference,[],[67,37,19,9,2,12,3])).
% 249.42/249.40 cnf(81,plain,
% 249.42/249.40 (~E(f3(a4,a2),a5)),
% 249.42/249.40 inference(scs_inference,[],[67,37,19,9,2,12,3,4])).
% 249.42/249.40 cnf(86,plain,
% 249.42/249.40 (E(f3(f3(x861,x862),x863),f3(f3(x861,x863),f3(x862,x863)))+~E(f3(f3(f3(x861,x862),x863),f3(f3(x861,x863),f3(x862,x863))),a5)),
% 249.42/249.40 inference(scs_inference,[],[74,66,78,10,2,3,4,12])).
% 249.42/249.40 cnf(90,plain,
% 249.42/249.40 (E(f3(f3(f3(f3(a5,x901),f3(f3(x902,x903),x901)),x904),f3(x905,x904)),f3(f3(f3(f3(a5,x901),f3(f3(x902,x903),x901)),f3(x905,x904)),f3(x904,f3(x905,x904))))),
% 249.42/249.40 inference(scs_inference,[],[74,66,38,57,78,10,2,3,4,12,13])).
% 249.42/249.40 cnf(91,plain,
% 249.42/249.40 (E(f3(f3(a5,x911),f3(f3(x912,x913),x911)),f3(a5,f3(x912,x913)))),
% 249.42/249.40 inference(scs_inference,[],[53,2])).
% 249.42/249.40 cnf(92,plain,
% 249.42/249.40 (~E(f3(f3(a4,a2),f3(a4,a1)),f3(f3(a5,f3(x921,x922)),x923))),
% 249.42/249.40 inference(scs_inference,[],[11,53,57,2,3])).
% 249.42/249.40 cnf(93,plain,
% 249.42/249.40 (~E(f3(a4,a2),f3(a5,f3(x931,x932)))),
% 249.42/249.40 inference(scs_inference,[],[11,53,57,2,3,4])).
% 249.42/249.40 cnf(94,plain,
% 249.42/249.40 (E(f3(f3(f3(a5,x941),f3(x942,x941)),x943),a5)),
% 249.42/249.40 inference(scs_inference,[],[11,53,57,29,8,2,3,4,13])).
% 249.42/249.40 cnf(100,plain,
% 249.42/249.40 (E(f3(f3(a5,x1001),f3(x1002,x1001)),f3(f3(a5,f3(x1002,x1001)),f3(x1001,f3(x1002,x1001))))),
% 249.42/249.40 inference(scs_inference,[],[11,53,57,29,8,2,3,4,13,12,86])).
% 249.42/249.40 cnf(102,plain,
% 249.42/249.40 (E(f3(f3(a5,x1021),f3(x1022,x1021)),f3(f3(f3(a5,x1021),x1023),f3(f3(x1022,x1021),x1023)))),
% 249.42/249.40 inference(scs_inference,[],[94,42])).
% 249.42/249.40 cnf(106,plain,
% 249.42/249.40 (~E(f3(a4,a2),f3(f3(a5,f3(x1061,x1062)),x1063))),
% 249.42/249.40 inference(scs_inference,[],[100,73,94,93,42,2,3])).
% 249.42/249.40 cnf(108,plain,
% 249.42/249.40 (~E(a4,f3(a5,f3(x1081,x1082)))),
% 249.42/249.40 inference(scs_inference,[],[100,73,94,93,42,2,3,4])).
% 249.42/249.40 cnf(110,plain,
% 249.42/249.40 (~E(a4,f3(f3(a5,x1101),f3(f3(x1102,x1103),x1101)))),
% 249.42/249.40 inference(scs_inference,[],[102,91,108,2,3])).
% 249.42/249.40 cnf(112,plain,
% 249.42/249.40 (E(a5,f3(f3(f3(f3(f3(x1121,x1122),f3(x1123,x1122)),x1124),f3(x1125,x1124)),f3(x1121,x1123)))),
% 249.42/249.40 inference(scs_inference,[],[38,2])).
% 249.42/249.40 cnf(119,plain,
% 249.42/249.40 (~E(f3(a4,a2),f3(f3(f3(a4,a1),x1191),f3(x1192,x1191)))),
% 249.42/249.40 inference(scs_inference,[],[57,41,92,2,3,4])).
% 249.42/249.40 cnf(128,plain,
% 249.42/249.40 (E(a5,f3(f3(f3(x1281,x1282),f3(x1283,x1282)),x1281))),
% 249.42/249.40 inference(scs_inference,[],[29,2])).
% 249.42/249.40 cnf(129,plain,
% 249.42/249.40 (~E(a4,f3(f3(a5,f3(x1291,x1292)),f3(x1293,f3(x1291,x1292))))),
% 249.42/249.40 inference(scs_inference,[],[100,29,110,2,3])).
% 249.42/249.40 cnf(132,plain,
% 249.42/249.40 (E(a5,f3(f3(f3(x1321,x1322),f3(x1323,x1322)),f3(f3(x1321,x1323),x1322)))),
% 249.42/249.40 inference(scs_inference,[],[10,2])).
% 249.42/249.40 cnf(133,plain,
% 249.42/249.40 (~E(a4,a5)),
% 249.42/249.40 inference(scs_inference,[],[32,129,10,2,3])).
% 249.42/249.40 cnf(135,plain,
% 249.42/249.40 (E(a5,f3(f3(x1351,x1352),x1351))),
% 249.42/249.40 inference(scs_inference,[],[9,2])).
% 249.42/249.40 cnf(138,plain,
% 249.42/249.40 (~E(f3(a4,a2),f3(f3(a4,x1381),f3(a1,x1381)))),
% 249.42/249.40 inference(scs_inference,[],[11,22,3,4])).
% 249.42/249.40 cnf(139,plain,
% 249.42/249.40 (~E(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x1391))),
% 249.42/249.41 inference(scs_inference,[],[11,8,3])).
% 249.42/249.41 cnf(141,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),f3(a4,a1)),f3(f3(x1411,x1412),x1411))),
% 249.42/249.41 inference(scs_inference,[],[11,9,3])).
% 249.42/249.41 cnf(146,plain,
% 249.42/249.41 (~E(f3(a4,a2),f3(f3(a4,a1),x1461))),
% 249.42/249.41 inference(scs_inference,[],[141,4])).
% 249.42/249.41 cnf(153,plain,
% 249.42/249.41 (~E(a4,f3(a4,a1))),
% 249.42/249.41 inference(scs_inference,[],[146,4])).
% 249.42/249.41 cnf(169,plain,
% 249.42/249.41 (E(f3(a1,a2),f3(f3(f3(f3(f3(x1691,x1692),f3(x1693,x1692)),x1694),f3(x1695,x1694)),f3(x1691,x1693)))),
% 249.42/249.41 inference(scs_inference,[],[6,112,3])).
% 249.42/249.41 cnf(173,plain,
% 249.42/249.41 (E(f3(x1731,a6),f3(f3(f3(f3(f3(x1732,x1733),f3(x1734,x1733)),x1735),f3(x1736,x1735)),f3(x1732,x1734)))),
% 249.42/249.41 inference(scs_inference,[],[7,112,3])).
% 249.42/249.41 cnf(177,plain,
% 249.42/249.41 (E(f3(a5,x1771),f3(f3(f3(f3(f3(x1772,x1773),f3(x1774,x1773)),x1775),f3(x1776,x1775)),f3(x1772,x1774)))),
% 249.42/249.41 inference(scs_inference,[],[8,112,3])).
% 249.42/249.41 cnf(181,plain,
% 249.42/249.41 (E(f3(f3(f3(f3(x1811,x1812),f3(x1813,x1812)),x1814),f3(x1811,x1813)),a5)),
% 249.42/249.41 inference(scs_inference,[],[9,22,13])).
% 249.42/249.41 cnf(185,plain,
% 249.42/249.41 (~E(f3(a4,a2),f3(f3(f3(a4,x1851),f3(a1,x1851)),x1852))),
% 249.42/249.41 inference(scs_inference,[],[9,11,22,13,3,4])).
% 249.42/249.41 cnf(188,plain,
% 249.42/249.41 (~E(a4,f3(f3(a4,x1881),f3(a1,x1881)))),
% 249.42/249.41 inference(scs_inference,[],[185,4])).
% 249.42/249.41 cnf(190,plain,
% 249.42/249.41 (E(a5,f3(f3(f3(f3(x1901,x1902),f3(x1903,x1902)),x1904),f3(x1901,x1903)))),
% 249.42/249.41 inference(scs_inference,[],[181,185,4,2])).
% 249.42/249.41 cnf(191,plain,
% 249.42/249.41 (E(f3(f3(a1,x1911),a2),a5)),
% 249.42/249.41 inference(scs_inference,[],[9,181,6,185,4,2,13])).
% 249.42/249.41 cnf(198,plain,
% 249.42/249.41 (E(a5,f3(f3(a1,x1981),a2))),
% 249.42/249.41 inference(scs_inference,[],[191,2])).
% 249.42/249.41 cnf(199,plain,
% 249.42/249.41 (E(f3(f3(f3(a1,x1991),x1992),a2),a5)),
% 249.42/249.41 inference(scs_inference,[],[9,191,2,13])).
% 249.42/249.41 cnf(206,plain,
% 249.42/249.41 (E(a5,f3(f3(f3(a1,x2061),x2062),a2))),
% 249.42/249.41 inference(scs_inference,[],[199,2])).
% 249.42/249.41 cnf(207,plain,
% 249.42/249.41 (E(f3(f3(a5,x2071),x2072),a5)),
% 249.42/249.41 inference(scs_inference,[],[9,199,8,2,13])).
% 249.42/249.41 cnf(208,plain,
% 249.42/249.41 (E(f3(f3(x2081,x2082),x2081),a5)),
% 249.42/249.41 inference(rename_variables,[],[9])).
% 249.42/249.41 cnf(210,plain,
% 249.42/249.41 (E(f3(f3(a5,x2101),x2102),f3(a5,x2101))),
% 249.42/249.41 inference(scs_inference,[],[9,208,199,8,2,13,12])).
% 249.42/249.41 cnf(218,plain,
% 249.42/249.41 (E(f3(f3(a5,x2181),x2182),a5)),
% 249.42/249.41 inference(rename_variables,[],[207])).
% 249.42/249.41 cnf(221,plain,
% 249.42/249.41 (E(f3(f3(f3(a5,x2211),x2212),x2213),a5)),
% 249.42/249.41 inference(scs_inference,[],[9,210,207,218,42,2,13])).
% 249.42/249.41 cnf(222,plain,
% 249.42/249.41 (E(f3(f3(x2221,x2222),x2221),a5)),
% 249.42/249.41 inference(rename_variables,[],[9])).
% 249.42/249.41 cnf(224,plain,
% 249.42/249.41 (E(f3(f3(f3(a5,x2241),x2242),x2243),f3(f3(a5,x2241),x2242))),
% 249.42/249.41 inference(scs_inference,[],[9,222,210,207,218,42,2,13,12])).
% 249.42/249.41 cnf(232,plain,
% 249.42/249.41 (E(f3(f3(a5,x2321),x2322),f3(f3(a5,x2322),f3(x2321,x2322)))),
% 249.42/249.41 inference(scs_inference,[],[221,86])).
% 249.42/249.41 cnf(233,plain,
% 249.42/249.41 (E(f3(f3(f3(a5,x2331),x2332),x2333),a5)),
% 249.42/249.41 inference(rename_variables,[],[221])).
% 249.42/249.41 cnf(235,plain,
% 249.42/249.41 (E(f3(f3(a5,x2351),x2352),f3(f3(f3(a5,x2351),x2353),f3(x2352,x2353)))),
% 249.42/249.41 inference(scs_inference,[],[221,233,86,42])).
% 249.42/249.41 cnf(236,plain,
% 249.42/249.41 (E(f3(f3(f3(a5,x2361),x2362),x2363),a5)),
% 249.42/249.41 inference(rename_variables,[],[221])).
% 249.42/249.41 cnf(238,plain,
% 249.42/249.41 (E(f3(f3(a5,x2381),x2382),f3(f3(f3(a5,x2381),x2382),x2383))),
% 249.42/249.41 inference(scs_inference,[],[224,221,233,86,42,2])).
% 249.42/249.41 cnf(239,plain,
% 249.42/249.41 (E(f3(f3(a5,x2391),x2392),f3(f3(f3(f3(a5,x2391),x2392),x2393),f3(x2394,x2393)))),
% 249.42/249.41 inference(scs_inference,[],[224,29,221,233,236,86,42,2,12])).
% 249.42/249.41 cnf(248,plain,
% 249.42/249.41 (E(f3(f3(f3(f3(a5,x2481),x2482),x2483),f3(x2484,x2483)),f3(f3(a5,x2481),x2482))),
% 249.42/249.41 inference(scs_inference,[],[239,2])).
% 249.42/249.41 cnf(249,plain,
% 249.42/249.41 (E(f3(f3(a5,x2491),x2492),f3(f3(f3(f3(a5,x2491),x2493),f3(x2492,x2493)),x2494))),
% 249.42/249.41 inference(scs_inference,[],[239,181,221,2,12])).
% 249.42/249.41 cnf(256,plain,
% 249.42/249.41 (~E(f3(a4,a2),f3(a5,x2561))),
% 249.42/249.41 inference(scs_inference,[],[239,181,221,141,2,12,3,4])).
% 249.42/249.41 cnf(258,plain,
% 249.42/249.41 (E(f3(a5,x2581),f3(f3(f3(f3(a5,x2582),f3(x2581,x2582)),x2583),f3(x2584,x2583)))),
% 249.42/249.41 inference(scs_inference,[],[249,38,207,2,12])).
% 249.42/249.41 cnf(270,plain,
% 249.42/249.41 (~E(a4,f3(f3(a2,x2701),f3(x2702,x2701)))),
% 249.42/249.41 inference(scs_inference,[],[235,41,106,2,3,4])).
% 249.42/249.41 cnf(272,plain,
% 249.42/249.41 (E(f3(f3(f3(f3(a5,x2721),f3(x2722,x2721)),x2723),f3(x2724,x2723)),f3(a5,x2722))),
% 249.42/249.41 inference(scs_inference,[],[258,2])).
% 249.42/249.41 cnf(284,plain,
% 249.42/249.41 (E(f3(f3(a5,x2841),f3(x2842,x2841)),f3(f3(a5,x2842),x2841))),
% 249.42/249.41 inference(scs_inference,[],[232,2])).
% 249.42/249.41 cnf(289,plain,
% 249.42/249.41 (E(a5,f3(f3(f3(a5,x2891),x2892),x2893))),
% 249.42/249.41 inference(scs_inference,[],[221,2])).
% 249.42/249.41 cnf(291,plain,
% 249.42/249.41 (~E(f3(a4,a2),f3(f3(a5,x2911),x2912))),
% 249.42/249.41 inference(scs_inference,[],[11,221,2,3,4])).
% 249.42/249.41 cnf(292,plain,
% 249.42/249.41 (E(f3(f3(f3(f3(a5,x2921),x2922),x2923),f3(a4,a1)),a5)),
% 249.42/249.41 inference(scs_inference,[],[9,11,221,2,3,4,13])).
% 249.42/249.41 cnf(296,plain,
% 249.42/249.41 (~E(a4,f3(a5,x2961))),
% 249.42/249.41 inference(scs_inference,[],[291,4])).
% 249.42/249.41 cnf(298,plain,
% 249.42/249.41 (E(a5,f3(f3(f3(f3(a5,x2981),x2982),x2983),f3(a4,a1)))),
% 249.42/249.41 inference(scs_inference,[],[292,291,4,2])).
% 249.42/249.41 cnf(299,plain,
% 249.42/249.41 (E(f3(a5,x2991),f3(f3(f3(a5,x2991),x2992),f3(x2993,x2992)))),
% 249.42/249.41 inference(scs_inference,[],[29,292,207,291,4,2,12])).
% 249.42/249.41 cnf(303,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),f3(a4,a1)),f3(f3(f3(f3(a5,x3031),x3032),x3033),f3(a4,a1)))),
% 249.42/249.41 inference(scs_inference,[],[11,29,292,207,291,4,2,12,3])).
% 249.42/249.41 cnf(304,plain,
% 249.42/249.41 (~E(f3(a4,a2),f3(f3(f3(a5,x3041),x3042),x3043))),
% 249.42/249.41 inference(scs_inference,[],[303,4])).
% 249.42/249.41 cnf(306,plain,
% 249.42/249.41 (E(f3(a5,x3061),f3(f3(f3(a5,x3062),f3(x3061,x3062)),x3063))),
% 249.42/249.41 inference(scs_inference,[],[299,181,207,303,4,2,12])).
% 249.42/249.41 cnf(310,plain,
% 249.42/249.41 (~E(a4,f3(f3(a5,x3101),x3102))),
% 249.42/249.41 inference(scs_inference,[],[304,4])).
% 249.42/249.41 cnf(312,plain,
% 249.42/249.41 (E(f3(f3(f3(a5,x3121),f3(x3122,x3121)),x3123),f3(a5,x3122))),
% 249.42/249.41 inference(scs_inference,[],[306,304,4,2])).
% 249.42/249.41 cnf(314,plain,
% 249.42/249.41 (E(a5,f3(f3(a5,x3141),x3142))),
% 249.42/249.41 inference(scs_inference,[],[207,2])).
% 249.42/249.41 cnf(316,plain,
% 249.42/249.41 (E(f3(f3(f3(x3161,f3(x3162,x3163)),f3(x3163,f3(x3162,x3163))),f3(x3161,x3162)),a5)),
% 249.42/249.41 inference(scs_inference,[],[10,22,13])).
% 249.42/249.41 cnf(325,plain,
% 249.42/249.41 (E(a5,f3(f3(f3(x3251,f3(x3252,x3253)),f3(x3253,f3(x3252,x3253))),f3(x3251,x3252)))),
% 249.42/249.41 inference(scs_inference,[],[316,2])).
% 249.42/249.41 cnf(326,plain,
% 249.42/249.41 (E(f3(f3(f3(f3(x3261,x3262),x3263),f3(f3(x3264,x3262),x3263)),f3(x3261,x3264)),a5)),
% 249.42/249.41 inference(scs_inference,[],[10,316,181,2,13])).
% 249.42/249.41 cnf(338,plain,
% 249.42/249.41 (~E(a6,f3(a4,a1))),
% 249.42/249.41 inference(scs_inference,[],[19,2,5])).
% 249.42/249.41 cnf(339,plain,
% 249.42/249.41 (E(f3(f3(x3391,a6),x3392),f3(a5,x3392))),
% 249.42/249.41 inference(scs_inference,[],[14,2,4])).
% 249.42/249.41 cnf(340,plain,
% 249.42/249.41 (E(f3(a5,x3401),f3(f3(x3402,a6),x3401))),
% 249.42/249.41 inference(scs_inference,[],[339,2])).
% 249.42/249.41 cnf(341,plain,
% 249.42/249.41 (E(f3(f3(f3(f3(a1,x3411),x3412),f3(x3413,x3412)),a2),a5)),
% 249.42/249.41 inference(scs_inference,[],[199,22,339,2,13])).
% 249.42/249.41 cnf(349,plain,
% 249.42/249.41 (E(a5,f3(f3(f3(f3(a1,x3491),x3492),f3(x3493,x3492)),a2))),
% 249.42/249.41 inference(scs_inference,[],[341,2])).
% 249.42/249.41 cnf(350,plain,
% 249.42/249.41 (E(f3(f3(f3(f3(a5,x3501),x3502),f3(x3503,x3502)),x3504),a5)),
% 249.42/249.41 inference(scs_inference,[],[22,221,341,2,13])).
% 249.42/249.41 cnf(356,plain,
% 249.42/249.41 (E(a5,f3(f3(f3(f3(a5,x3561),x3562),f3(x3563,x3562)),x3564))),
% 249.42/249.41 inference(scs_inference,[],[350,2])).
% 249.42/249.41 cnf(357,plain,
% 249.42/249.41 (E(f3(f3(f3(f3(f3(a5,x3571),x3572),x3573),f3(x3574,x3573)),f3(a4,a1)),a5)),
% 249.42/249.41 inference(scs_inference,[],[22,350,292,2,13])).
% 249.42/249.41 cnf(361,plain,
% 249.42/249.41 (E(a5,f3(f3(f3(f3(f3(a5,x3611),x3612),x3613),f3(x3614,x3613)),f3(a4,a1)))),
% 249.42/249.41 inference(scs_inference,[],[357,2])).
% 249.42/249.41 cnf(362,plain,
% 249.42/249.41 (~E(f3(x3621,a6),f3(f3(a4,a2),f3(a4,a1)))),
% 249.42/249.41 inference(scs_inference,[],[11,14,2,3])).
% 249.42/249.41 cnf(365,plain,
% 249.42/249.41 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),a5),a5)),
% 249.42/249.41 inference(scs_inference,[],[11,8,2,12])).
% 249.42/249.41 cnf(366,plain,
% 249.42/249.41 (E(f3(x3661,f3(a5,x3662)),f3(x3661,a5))),
% 249.42/249.41 inference(scs_inference,[],[15,2,5])).
% 249.42/249.41 cnf(367,plain,
% 249.42/249.41 (E(f3(x3671,a5),f3(x3671,f3(a5,x3672)))),
% 249.42/249.41 inference(scs_inference,[],[366,2])).
% 249.42/249.41 cnf(369,plain,
% 249.42/249.41 (E(f3(f3(f3(a5,x3691),x3692),f3(x3693,x3692)),f3(f3(f3(f3(a5,x3691),x3692),x3694),f3(f3(x3693,x3692),x3694)))),
% 249.42/249.41 inference(scs_inference,[],[356,2,42])).
% 249.42/249.41 cnf(371,plain,
% 249.42/249.41 (E(f3(a5,x3711),f3(f3(f3(f3(x3712,x3713),f3(x3714,x3713)),f3(x3712,x3714)),x3711))),
% 249.42/249.41 inference(scs_inference,[],[22,2,4])).
% 249.42/249.41 cnf(372,plain,
% 249.42/249.41 (E(f3(f3(f3(f3(x3721,x3722),f3(x3723,x3722)),f3(x3721,x3723)),x3724),f3(a5,x3724))),
% 249.42/249.41 inference(scs_inference,[],[371,2])).
% 249.42/249.41 cnf(373,plain,
% 249.42/249.41 (E(a5,f3(f3(f3(f3(f3(f3(x3731,x3732),x3733),f3(f3(x3734,x3732),x3733)),x3735),f3(x3736,x3735)),f3(x3731,x3734)))),
% 249.42/249.41 inference(scs_inference,[],[22,38,2,13])).
% 249.42/249.41 cnf(374,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),f3(f3(a4,x3741),f3(a1,x3741))),a5)),
% 249.42/249.41 inference(scs_inference,[],[22,11,13])).
% 249.42/249.41 cnf(377,plain,
% 249.42/249.41 (E(f3(x3771,a5),f3(x3771,f3(f3(f3(x3772,x3773),f3(x3774,x3773)),f3(x3772,x3774))))),
% 249.42/249.41 inference(scs_inference,[],[22,2,5])).
% 249.42/249.41 cnf(378,plain,
% 249.42/249.41 (E(f3(x3781,f3(f3(f3(x3782,x3783),f3(x3784,x3783)),f3(x3782,x3784))),f3(x3781,a5))),
% 249.42/249.41 inference(scs_inference,[],[377,2])).
% 249.42/249.41 cnf(379,plain,
% 249.42/249.41 (~E(f3(a4,f3(a1,x3791)),a5)),
% 249.42/249.41 inference(scs_inference,[],[191,81,377,2,13])).
% 249.42/249.41 cnf(381,plain,
% 249.42/249.41 (~E(f3(a5,x3811),f3(f3(a4,a2),f3(a4,a1)))),
% 249.42/249.41 inference(scs_inference,[],[11,15,2,3])).
% 249.42/249.41 cnf(382,plain,
% 249.42/249.41 (~E(a5,f3(a4,a2))),
% 249.42/249.41 inference(scs_inference,[],[381,4])).
% 249.42/249.41 cnf(384,plain,
% 249.42/249.41 (~E(f3(a4,f3(f3(a1,x3841),x3842)),a5)),
% 249.42/249.41 inference(scs_inference,[],[199,381,81,4,13])).
% 249.42/249.41 cnf(386,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),a5),a5)),
% 249.42/249.41 inference(scs_inference,[],[15,11,2,13])).
% 249.42/249.41 cnf(387,plain,
% 249.42/249.41 (~E(f3(a4,f3(f3(f3(a1,x3871),x3872),f3(x3873,x3872))),a5)),
% 249.42/249.41 inference(scs_inference,[],[341,81,13])).
% 249.42/249.41 cnf(389,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),f3(f3(a5,x3891),x3892)),a5)),
% 249.42/249.41 inference(scs_inference,[],[11,221,13])).
% 249.42/249.41 cnf(393,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),f3(a5,x3931)),a5)),
% 249.42/249.41 inference(scs_inference,[],[11,207,13])).
% 249.42/249.41 cnf(397,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),f3(f3(f3(a4,a1),x3971),f3(x3972,x3971))),a5)),
% 249.42/249.41 inference(scs_inference,[],[11,29,13])).
% 249.42/249.41 cnf(401,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),f3(f3(f3(a5,x4011),x4012),f3(x4013,x4012))),a5)),
% 249.42/249.41 inference(scs_inference,[],[11,350,13])).
% 249.42/249.41 cnf(405,plain,
% 249.42/249.41 (~E(f3(a4,a1),a5)),
% 249.42/249.41 inference(scs_inference,[],[6,81,13])).
% 249.42/249.41 cnf(408,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),f3(f3(a4,a1),x4081)),a5)),
% 249.42/249.41 inference(scs_inference,[],[11,9,13])).
% 249.42/249.41 cnf(418,plain,
% 249.42/249.41 (~E(f3(a4,f3(f3(a5,x4181),x4182)),a5)),
% 249.42/249.41 inference(scs_inference,[],[81,221,13])).
% 249.42/249.41 cnf(422,plain,
% 249.42/249.41 (~E(a4,f3(a1,x4221))),
% 249.42/249.41 inference(scs_inference,[],[81,191,221,13,3,4])).
% 249.42/249.41 cnf(424,plain,
% 249.42/249.41 (~E(f3(a4,f3(a5,x4241)),a5)),
% 249.42/249.41 inference(scs_inference,[],[81,207,13])).
% 249.42/249.41 cnf(428,plain,
% 249.42/249.41 (~E(a4,f3(f3(a1,x4281),x4282))),
% 249.42/249.41 inference(scs_inference,[],[81,199,207,13,3,4])).
% 249.42/249.41 cnf(430,plain,
% 249.42/249.41 (~E(f3(a4,f3(f3(a2,x4301),f3(x4302,x4301))),a5)),
% 249.42/249.41 inference(scs_inference,[],[81,29,13])).
% 249.42/249.41 cnf(434,plain,
% 249.42/249.41 (~E(a4,f3(f3(f3(a1,x4341),x4342),f3(x4343,x4342)))),
% 249.42/249.41 inference(scs_inference,[],[81,341,29,13,3,4])).
% 249.42/249.41 cnf(439,plain,
% 249.42/249.41 (~E(f3(a4,a2),f3(f3(f3(x4391,x4392),f3(x4393,x4392)),f3(x4391,x4393)))),
% 249.42/249.41 inference(scs_inference,[],[81,22,350,13,3])).
% 249.42/249.41 cnf(441,plain,
% 249.42/249.41 (~E(f3(a4,a5),a5)),
% 249.42/249.41 inference(scs_inference,[],[81,8,13])).
% 249.42/249.41 cnf(446,plain,
% 249.42/249.41 (~E(f3(a4,f3(a2,x4461)),a5)),
% 249.42/249.41 inference(scs_inference,[],[81,9,13])).
% 249.42/249.41 cnf(475,plain,
% 249.42/249.41 (~E(a4,f3(a2,x4751))),
% 249.42/249.41 inference(scs_inference,[],[81,9,3,4])).
% 249.42/249.41 cnf(480,plain,
% 249.42/249.41 (E(f3(f3(a5,x4801),x4802),f3(a5,x4803))),
% 249.42/249.41 inference(scs_inference,[],[221,207,12])).
% 249.42/249.41 cnf(484,plain,
% 249.42/249.41 (E(f3(a5,x4841),f3(f3(a5,x4842),x4843))),
% 249.42/249.41 inference(scs_inference,[],[221,207,12,2])).
% 249.42/249.41 cnf(486,plain,
% 249.42/249.41 (E(f3(f3(a5,x4861),x4862),f3(f3(f3(a5,x4863),x4864),f3(x4865,x4864)))),
% 249.42/249.41 inference(scs_inference,[],[221,350,12])).
% 249.42/249.41 cnf(490,plain,
% 249.42/249.41 (E(f3(f3(f3(a5,x4901),x4902),f3(x4903,x4902)),f3(f3(a5,x4904),x4905))),
% 249.42/249.41 inference(scs_inference,[],[221,350,12,2])).
% 249.42/249.41 cnf(495,plain,
% 249.42/249.41 (~E(f3(a4,a2),f3(f3(f3(a4,a1),x4951),a5))),
% 249.42/249.41 inference(scs_inference,[],[119,367,3])).
% 249.42/249.41 cnf(506,plain,
% 249.42/249.41 (~E(a4,f3(f3(f3(x5061,x5062),f3(x5063,x5062)),f3(x5061,x5063)))),
% 249.42/249.41 inference(scs_inference,[],[133,22,3])).
% 249.42/249.41 cnf(507,plain,
% 249.42/249.41 (~E(a4,f3(f3(f3(x5071,x5072),f3(x5073,x5072)),x5071))),
% 249.42/249.41 inference(scs_inference,[],[133,29,3])).
% 249.42/249.41 cnf(509,plain,
% 249.42/249.41 (~E(a4,f3(f3(f3(f3(f3(x5091,x5092),f3(x5093,x5092)),x5094),f3(x5095,x5094)),f3(x5091,x5093)))),
% 249.42/249.41 inference(scs_inference,[],[133,38,3])).
% 249.42/249.41 cnf(511,plain,
% 249.42/249.41 (~E(a4,f3(x5111,a6))),
% 249.42/249.41 inference(scs_inference,[],[173,509,3])).
% 249.42/249.41 cnf(527,plain,
% 249.42/249.41 (~E(a4,f3(f3(x5271,x5272),x5271))),
% 249.42/249.41 inference(scs_inference,[],[133,9,3])).
% 249.42/249.41 cnf(535,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),f3(a4,a1)),f3(f3(x5351,a6),x5352))),
% 249.42/249.41 inference(scs_inference,[],[139,339,3])).
% 249.42/249.41 cnf(573,plain,
% 249.42/249.41 (E(f3(a5,x5731),f3(f3(f3(a5,x5732),x5733),f3(x5734,x5733)))),
% 249.42/249.41 inference(scs_inference,[],[207,350,12])).
% 249.42/249.41 cnf(577,plain,
% 249.42/249.41 (E(f3(f3(f3(a5,x5771),x5772),f3(x5773,x5772)),f3(a5,x5774))),
% 249.42/249.41 inference(scs_inference,[],[207,350,12,2])).
% 249.42/249.41 cnf(595,plain,
% 249.42/249.41 (~E(f3(a4,a2),f3(f3(x5951,a6),x5952))),
% 249.42/249.41 inference(scs_inference,[],[256,339,3])).
% 249.42/249.41 cnf(601,plain,
% 249.42/249.41 (~E(a4,f3(f3(a2,x6011),a5))),
% 249.42/249.41 inference(scs_inference,[],[270,367,3])).
% 249.42/249.41 cnf(620,plain,
% 249.42/249.41 (~E(a4,f3(f3(x6201,a6),x6202))),
% 249.42/249.41 inference(scs_inference,[],[296,339,3])).
% 249.42/249.41 cnf(628,plain,
% 249.42/249.41 (~E(a4,f3(f3(f3(f3(a5,x6281),x6282),x6283),f3(x6284,x6283)))),
% 249.42/249.41 inference(scs_inference,[],[310,248,3])).
% 249.42/249.41 cnf(647,plain,
% 249.42/249.41 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),f3(f3(a5,x6471),x6472)),a5)),
% 249.42/249.41 inference(scs_inference,[],[365,221,13])).
% 249.42/249.41 cnf(652,plain,
% 249.42/249.41 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x6521)),a5)),
% 249.42/249.41 inference(scs_inference,[],[365,207,13])).
% 249.42/249.41 cnf(656,plain,
% 249.42/249.41 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),f3(f3(f3(a5,x6561),x6562),f3(x6563,x6562))),a5)),
% 249.42/249.41 inference(scs_inference,[],[365,350,13])).
% 249.42/249.41 cnf(663,plain,
% 249.42/249.41 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),a5),f3(x6631,a6))),
% 249.42/249.41 inference(scs_inference,[],[365,7,3])).
% 249.42/249.41 cnf(664,plain,
% 249.42/249.41 (~E(a5,a6)),
% 249.42/249.41 inference(scs_inference,[],[365,7,3,5])).
% 249.42/249.41 cnf(686,plain,
% 249.42/249.41 (~E(f3(f3(a4,a2),f3(f3(a4,x6861),f3(a1,x6861))),f3(a1,a2))),
% 249.42/249.41 inference(scs_inference,[],[374,6,3])).
% 249.42/249.41 cnf(690,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(a4,x6901),f3(a1,x6901))),f3(x6902,a6))),
% 249.42/249.42 inference(scs_inference,[],[374,7,3])).
% 249.42/249.42 cnf(696,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(a4,x6961),f3(a1,x6961))),f3(f3(x6962,x6963),x6962))),
% 249.42/249.42 inference(scs_inference,[],[374,9,3])).
% 249.42/249.42 cnf(697,plain,
% 249.42/249.42 (~E(f3(f3(a4,x6971),f3(a1,x6971)),a4)),
% 249.42/249.42 inference(scs_inference,[],[374,9,3,5])).
% 249.42/249.42 cnf(701,plain,
% 249.42/249.42 (~E(f3(a4,f3(a1,x7011)),f3(f3(a1,x7012),a2))),
% 249.42/249.42 inference(scs_inference,[],[379,191,3])).
% 249.42/249.42 cnf(719,plain,
% 249.42/249.42 (~E(a4,f3(f3(f3(a1,x7191),f3(x7192,x7191)),x7193))),
% 249.42/249.42 inference(scs_inference,[],[379,181,3,4])).
% 249.42/249.42 cnf(721,plain,
% 249.42/249.42 (~E(f3(a4,f3(a1,x7211)),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[379,6,3])).
% 249.42/249.42 cnf(722,plain,
% 249.42/249.42 (~E(f3(a4,f3(a1,x7221)),f3(a5,x7222))),
% 249.42/249.42 inference(scs_inference,[],[379,8,3])).
% 249.42/249.42 cnf(726,plain,
% 249.42/249.42 (~E(f3(a4,f3(a1,x7261)),f3(x7262,a6))),
% 249.42/249.42 inference(scs_inference,[],[379,7,3])).
% 249.42/249.42 cnf(727,plain,
% 249.42/249.42 (~E(f3(a1,x7271),a6)),
% 249.42/249.42 inference(scs_inference,[],[379,7,3,5])).
% 249.42/249.42 cnf(742,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a1,x7421),x7422)),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[384,6,3])).
% 249.42/249.42 cnf(745,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a1,x7451),x7452)),f3(f3(x7453,x7454),x7453))),
% 249.42/249.42 inference(scs_inference,[],[384,9,3])).
% 249.42/249.42 cnf(747,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a1,x7471),x7472)),f3(x7473,a6))),
% 249.42/249.42 inference(scs_inference,[],[384,7,3])).
% 249.42/249.42 cnf(748,plain,
% 249.42/249.42 (~E(f3(f3(a1,x7481),x7482),a6)),
% 249.42/249.42 inference(scs_inference,[],[384,7,3,5])).
% 249.42/249.42 cnf(751,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),a5),f3(f3(a1,x7511),a2))),
% 249.42/249.42 inference(scs_inference,[],[386,191,3])).
% 249.42/249.42 cnf(770,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),a5),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[386,6,3])).
% 249.42/249.42 cnf(772,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),a5),f3(a5,x7721))),
% 249.42/249.42 inference(scs_inference,[],[386,8,3])).
% 249.42/249.42 cnf(775,plain,
% 249.42/249.42 (~E(a5,a4)),
% 249.42/249.42 inference(scs_inference,[],[386,9,3,5])).
% 249.42/249.42 cnf(776,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),a5),f3(x7761,a6))),
% 249.42/249.42 inference(scs_inference,[],[386,7,3])).
% 249.42/249.42 cnf(789,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(f3(a1,x7891),x7892),f3(x7893,x7892))),f3(f3(x7894,x7895),x7894))),
% 249.42/249.42 inference(scs_inference,[],[387,9,3])).
% 249.42/249.42 cnf(791,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(f3(a1,x7911),x7912),f3(x7913,x7912))),f3(x7914,a6))),
% 249.42/249.42 inference(scs_inference,[],[387,7,3])).
% 249.42/249.42 cnf(805,plain,
% 249.42/249.42 (~E(f3(f3(a5,x8051),x8052),a4)),
% 249.42/249.42 inference(scs_inference,[],[389,9,3,5])).
% 249.42/249.42 cnf(807,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(a5,x8071),x8072)),f3(x8073,a6))),
% 249.42/249.42 inference(scs_inference,[],[389,7,3])).
% 249.42/249.42 cnf(808,plain,
% 249.42/249.42 (~E(f3(f3(a5,x8081),x8082),a6)),
% 249.42/249.42 inference(scs_inference,[],[389,7,3,5])).
% 249.42/249.42 cnf(829,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(a5,x8291)),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[393,6,3])).
% 249.42/249.42 cnf(834,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(a5,x8341)),f3(x8342,a6))),
% 249.42/249.42 inference(scs_inference,[],[393,7,3])).
% 249.42/249.42 cnf(835,plain,
% 249.42/249.42 (~E(f3(a5,x8351),a6)),
% 249.42/249.42 inference(scs_inference,[],[393,7,3,5])).
% 249.42/249.42 cnf(837,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(a5,x8371)),f3(a5,x8372))),
% 249.42/249.42 inference(scs_inference,[],[393,8,3])).
% 249.42/249.42 cnf(846,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(f3(a4,a1),x8461),f3(x8462,x8461))),f3(f3(x8463,x8464),x8463))),
% 249.42/249.42 inference(scs_inference,[],[397,9,3])).
% 249.42/249.42 cnf(859,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(f3(a5,x8591),x8592),f3(x8593,x8592))),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[401,6,3])).
% 249.42/249.42 cnf(864,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(f3(a5,x8641),x8642),f3(x8643,x8642))),f3(x8644,a6))),
% 249.42/249.42 inference(scs_inference,[],[401,7,3])).
% 249.42/249.42 cnf(872,plain,
% 249.42/249.42 (~E(f3(a4,a1),f3(f3(f3(a1,x8721),x8722),a2))),
% 249.42/249.42 inference(scs_inference,[],[405,199,3])).
% 249.42/249.42 cnf(877,plain,
% 249.42/249.42 (~E(f3(a4,a1),f3(f3(a5,x8771),x8772))),
% 249.42/249.42 inference(scs_inference,[],[405,207,3])).
% 249.42/249.42 cnf(879,plain,
% 249.42/249.42 (~E(f3(a4,a1),f3(f3(f3(x8791,x8792),f3(x8793,x8792)),f3(x8791,x8793)))),
% 249.42/249.42 inference(scs_inference,[],[405,22,3])).
% 249.42/249.42 cnf(881,plain,
% 249.42/249.42 (~E(f3(f3(a4,a1),f3(f3(f3(a5,x8811),f3(x8812,x8811)),f3(a5,x8812))),a5)),
% 249.42/249.42 inference(scs_inference,[],[292,879,12])).
% 249.42/249.42 cnf(889,plain,
% 249.42/249.42 (~E(f3(a4,a1),f3(f3(f3(f3(f3(x8891,x8892),f3(x8893,x8892)),x8894),f3(x8895,x8894)),f3(x8891,x8893)))),
% 249.42/249.42 inference(scs_inference,[],[405,38,3])).
% 249.42/249.42 cnf(891,plain,
% 249.42/249.42 (~E(f3(a4,a1),f3(a5,x8911))),
% 249.42/249.42 inference(scs_inference,[],[177,889,3])).
% 249.42/249.42 cnf(894,plain,
% 249.42/249.42 (~E(f3(a4,a1),f3(x8941,a6))),
% 249.42/249.42 inference(scs_inference,[],[173,889,3])).
% 249.42/249.42 cnf(908,plain,
% 249.42/249.42 (~E(f3(a4,a1),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[405,6,3])).
% 249.42/249.42 cnf(923,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(a4,a1),x9231)),f3(f3(x9232,x9233),x9232))),
% 249.42/249.42 inference(scs_inference,[],[408,9,3])).
% 249.42/249.42 cnf(926,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(a4,a1),x9261)),f3(x9262,a6))),
% 249.42/249.42 inference(scs_inference,[],[408,7,3])).
% 249.42/249.42 cnf(929,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(a4,a1),x9291)),f3(a5,x9292))),
% 249.42/249.42 inference(scs_inference,[],[408,8,3])).
% 249.42/249.42 cnf(937,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a5,x9371),x9372)),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[418,6,3])).
% 249.42/249.42 cnf(941,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a5,x9411),x9412)),f3(x9413,a6))),
% 249.42/249.42 inference(scs_inference,[],[418,7,3])).
% 249.42/249.42 cnf(967,plain,
% 249.42/249.42 (~E(f3(a4,f3(a5,x9671)),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[424,6,3])).
% 249.42/249.42 cnf(973,plain,
% 249.42/249.42 (~E(f3(a4,f3(a5,x9731)),f3(a5,x9732))),
% 249.42/249.42 inference(scs_inference,[],[424,8,3])).
% 249.42/249.42 cnf(987,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a2,x9871),f3(x9872,x9871))),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[430,6,3])).
% 249.42/249.42 cnf(989,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a2,x9891),f3(x9892,x9891))),f3(f3(x9893,x9894),x9893))),
% 249.42/249.42 inference(scs_inference,[],[430,9,3])).
% 249.42/249.42 cnf(991,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a2,x9911),f3(x9912,x9911))),f3(x9913,a6))),
% 249.42/249.42 inference(scs_inference,[],[430,7,3])).
% 249.42/249.42 cnf(992,plain,
% 249.42/249.42 (~E(f3(f3(a2,x9921),f3(x9922,x9921)),a6)),
% 249.42/249.42 inference(scs_inference,[],[430,7,3,5])).
% 249.42/249.42 cnf(998,plain,
% 249.42/249.42 (~E(a4,f3(f3(f3(a1,x9981),x9982),a5))),
% 249.42/249.42 inference(scs_inference,[],[434,367,3])).
% 249.42/249.42 cnf(1026,plain,
% 249.42/249.42 (~E(f3(a4,a5),f3(f3(f3(x10261,x10262),f3(x10263,x10262)),f3(x10261,x10263)))),
% 249.42/249.42 inference(scs_inference,[],[441,22,3])).
% 249.42/249.42 cnf(1032,plain,
% 249.42/249.42 (~E(f3(a4,a5),f3(f3(f3(f3(f3(x10321,x10322),f3(x10323,x10322)),x10324),f3(x10325,x10324)),f3(x10321,x10323)))),
% 249.42/249.42 inference(scs_inference,[],[441,38,3])).
% 249.42/249.42 cnf(1034,plain,
% 249.42/249.42 (~E(f3(a4,a5),f3(a5,x10341))),
% 249.42/249.42 inference(scs_inference,[],[177,1032,3])).
% 249.42/249.42 cnf(1037,plain,
% 249.42/249.42 (~E(f3(a4,a5),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[169,1032,3])).
% 249.42/249.42 cnf(1044,plain,
% 249.42/249.42 (~E(f3(a4,a5),f3(f3(f3(f3(x10441,x10442),x10443),f3(f3(x10444,x10442),x10443)),f3(x10441,x10444)))),
% 249.42/249.42 inference(scs_inference,[],[441,326,3])).
% 249.42/249.42 cnf(1046,plain,
% 249.42/249.42 (~E(f3(a4,a5),f3(f3(f3(f3(x10461,x10462),f3(x10463,x10462)),x10464),f3(x10461,x10463)))),
% 249.42/249.42 inference(scs_inference,[],[441,181,3])).
% 249.42/249.42 cnf(1050,plain,
% 249.42/249.42 (~E(f3(a4,a5),f3(x10501,a6))),
% 249.42/249.42 inference(scs_inference,[],[441,7,3])).
% 249.42/249.42 cnf(1052,plain,
% 249.42/249.42 (~E(f3(a4,a5),f3(f3(x10521,x10522),x10521))),
% 249.42/249.42 inference(scs_inference,[],[441,9,3])).
% 249.42/249.42 cnf(1058,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(f3(a2,x10581),x10582),f3(x10583,x10582))),a5)),
% 249.42/249.42 inference(scs_inference,[],[446,29,13])).
% 249.42/249.42 cnf(1061,plain,
% 249.42/249.42 (~E(f3(a4,f3(a2,x10611)),f3(f3(a1,x10612),a2))),
% 249.42/249.42 inference(scs_inference,[],[446,191,29,13,3])).
% 249.42/249.42 cnf(1063,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a2,x10631),x10632)),a5)),
% 249.42/249.42 inference(scs_inference,[],[446,9,13])).
% 249.42/249.42 cnf(1087,plain,
% 249.42/249.42 (~E(f3(a4,a2),f3(f3(f3(a4,a1),x10871),f3(a5,x10872)))),
% 249.42/249.42 inference(scs_inference,[],[495,366,3])).
% 249.42/249.42 cnf(1121,plain,
% 249.42/249.42 (~E(a4,f3(f3(a2,x11211),f3(a5,x11212)))),
% 249.42/249.42 inference(scs_inference,[],[601,366,3])).
% 249.42/249.42 cnf(1132,plain,
% 249.42/249.42 (~E(a4,f3(f3(f3(f3(a5,x11321),x11322),f3(x11323,x11324)),a5))),
% 249.42/249.42 inference(scs_inference,[],[628,377,3])).
% 249.42/249.42 cnf(1146,plain,
% 249.42/249.42 (~E(f3(f3(a5,x11461),x11462),f3(a4,a2))),
% 249.42/249.42 inference(scs_inference,[],[647,9,3,5])).
% 249.42/249.42 cnf(1164,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x11641)),f3(f3(a5,x11642),x11643))),
% 249.42/249.42 inference(scs_inference,[],[652,207,3])).
% 249.42/249.42 cnf(1170,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x11701)),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[652,6,3])).
% 249.42/249.42 cnf(1172,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x11721)),f3(x11722,a6))),
% 249.42/249.42 inference(scs_inference,[],[652,7,3])).
% 249.42/249.42 cnf(1174,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x11741)),f3(f3(x11742,x11743),x11742))),
% 249.42/249.42 inference(scs_inference,[],[652,9,3])).
% 249.42/249.42 cnf(1177,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x11771)),f3(a5,x11772))),
% 249.42/249.42 inference(scs_inference,[],[652,8,3])).
% 249.42/249.42 cnf(1179,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),f3(f3(f3(a5,x11791),x11792),f3(x11793,x11792))),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[656,6,3])).
% 249.42/249.42 cnf(1229,plain,
% 249.42/249.42 (~E(f3(a4,f3(a1,x12291)),f3(f3(x12292,a6),x12293))),
% 249.42/249.42 inference(scs_inference,[],[722,339,3])).
% 249.42/249.42 cnf(1265,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),a5),f3(f3(x12651,a6),x12652))),
% 249.42/249.42 inference(scs_inference,[],[772,339,3])).
% 249.42/249.42 cnf(1310,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(a5,x13101)),f3(f3(x13102,a6),x13103))),
% 249.42/249.42 inference(scs_inference,[],[837,339,3])).
% 249.42/249.42 cnf(1340,plain,
% 249.42/249.42 (~E(f3(a4,a1),f3(f3(f3(f3(a5,x13401),x13402),x13403),f3(x13404,x13403)))),
% 249.42/249.42 inference(scs_inference,[],[877,248,3])).
% 249.42/249.42 cnf(1349,plain,
% 249.42/249.42 (~E(f3(f3(a4,a1),f3(a5,x13491)),a5)),
% 249.42/249.42 inference(scs_inference,[],[881,207,13])).
% 249.42/249.42 cnf(1359,plain,
% 249.42/249.42 (~E(f3(f3(a4,a1),a5),a5)),
% 249.42/249.42 inference(scs_inference,[],[881,8,13])).
% 249.42/249.42 cnf(1362,plain,
% 249.42/249.42 (~E(f3(f3(a4,a1),f3(f3(f3(a5,x13621),f3(x13622,x13621)),f3(a5,x13622))),f3(x13623,a6))),
% 249.42/249.42 inference(scs_inference,[],[881,7,8,13,3])).
% 249.42/249.42 cnf(1363,plain,
% 249.42/249.42 (~E(f3(f3(f3(a5,x13631),f3(x13632,x13631)),f3(a5,x13632)),a6)),
% 249.42/249.42 inference(scs_inference,[],[881,7,8,13,3,5])).
% 249.42/249.42 cnf(1364,plain,
% 249.42/249.42 (~E(f3(a6,f3(a4,a1)),a5)),
% 249.42/249.42 inference(scs_inference,[],[881,7,8,338,13,3,5,12])).
% 249.42/249.42 cnf(1369,plain,
% 249.42/249.42 (~E(f3(a4,f3(a4,a1)),a5)),
% 249.42/249.42 inference(scs_inference,[],[881,9,153,3,5,12])).
% 249.42/249.42 cnf(1372,plain,
% 249.42/249.42 (~E(f3(f3(a4,a1),f3(f3(f3(a5,x13721),f3(x13722,x13721)),f3(a5,x13722))),f3(a5,x13723))),
% 249.42/249.42 inference(scs_inference,[],[881,8,3])).
% 249.42/249.42 cnf(1381,plain,
% 249.42/249.42 (~E(f3(a4,a1),f3(f3(x13811,a6),x13812))),
% 249.42/249.42 inference(scs_inference,[],[891,339,3])).
% 249.42/249.42 cnf(1403,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(a4,a1),x14031)),f3(f3(x14032,a6),x14033))),
% 249.42/249.42 inference(scs_inference,[],[929,339,3])).
% 249.42/249.42 cnf(1430,plain,
% 249.42/249.42 (~E(f3(a4,f3(a5,x14301)),f3(f3(x14302,a6),x14303))),
% 249.42/249.42 inference(scs_inference,[],[973,339,3])).
% 249.42/249.42 cnf(1456,plain,
% 249.42/249.42 (~E(a4,f3(f3(f3(a1,x14561),x14562),f3(a5,x14563)))),
% 249.42/249.42 inference(scs_inference,[],[998,366,3])).
% 249.42/249.42 cnf(1482,plain,
% 249.42/249.42 (~E(f3(a4,a5),f3(f3(x14821,a6),x14822))),
% 249.42/249.42 inference(scs_inference,[],[1034,339,3])).
% 249.42/249.42 cnf(1502,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(f3(a2,x15021),x15022),f3(x15023,x15022))),f3(f3(x15024,x15025),x15024))),
% 249.42/249.42 inference(scs_inference,[],[1058,9,3])).
% 249.42/249.42 cnf(1507,plain,
% 249.42/249.42 (~E(f3(a4,f3(a2,x15071)),f3(a5,a2))),
% 249.42/249.42 inference(scs_inference,[],[1061,340,3])).
% 249.42/249.42 cnf(1526,plain,
% 249.42/249.42 (~E(a4,f3(f3(f3(f3(a5,x15261),x15262),f3(x15263,x15264)),f3(a5,x15265)))),
% 249.42/249.42 inference(scs_inference,[],[1132,366,3])).
% 249.42/249.42 cnf(1538,plain,
% 249.42/249.42 (E(f3(f3(a1,a2),x15381),f3(a5,x15381))),
% 249.42/249.42 inference(scs_inference,[],[6,1381,42,4])).
% 249.42/249.42 cnf(1539,plain,
% 249.42/249.42 (E(f3(x15391,f3(a1,a2)),f3(x15391,a5))),
% 249.42/249.42 inference(scs_inference,[],[6,1381,42,4,5])).
% 249.42/249.42 cnf(1540,plain,
% 249.42/249.42 (~E(a6,a5)),
% 249.42/249.42 inference(scs_inference,[],[6,664,1381,42,4,5,2])).
% 249.42/249.42 cnf(1541,plain,
% 249.42/249.42 (~E(f3(a6,a5),a5)),
% 249.42/249.42 inference(scs_inference,[],[6,664,1359,1381,7,42,4,5,2,13])).
% 249.42/249.42 cnf(1554,plain,
% 249.42/249.42 (E(f3(f3(f3(a1,a2),x15541),x15542),f3(f3(a5,x15541),x15542))),
% 249.42/249.42 inference(scs_inference,[],[1538,1482,42,4])).
% 249.42/249.42 cnf(1555,plain,
% 249.42/249.42 (E(f3(x15551,f3(f3(a1,a2),x15552)),f3(x15551,f3(a5,x15552)))),
% 249.42/249.42 inference(scs_inference,[],[1538,1482,42,4,5])).
% 249.42/249.42 cnf(1556,plain,
% 249.42/249.42 (~E(a5,f3(a6,a5))),
% 249.42/249.42 inference(scs_inference,[],[1541,1538,1482,42,4,5,2])).
% 249.42/249.42 cnf(1557,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a4,x15571),f3(a1,x15571))),a5)),
% 249.42/249.42 inference(scs_inference,[],[1541,1538,1482,697,29,42,4,5,2,12])).
% 249.42/249.42 cnf(1562,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a2),a5),f3(f3(f3(a4,a2),a6),f3(a5,a6))),a5)),
% 249.42/249.42 inference(scs_inference,[],[1265,42])).
% 249.42/249.42 cnf(1565,plain,
% 249.42/249.42 (E(f3(f3(x15651,f3(a1,a2)),x15652),f3(f3(x15651,a5),x15652))),
% 249.42/249.42 inference(scs_inference,[],[1539,1265,42,4])).
% 249.42/249.42 cnf(1566,plain,
% 249.42/249.42 (E(f3(x15661,f3(x15662,f3(a1,a2))),f3(x15661,f3(x15662,a5)))),
% 249.42/249.42 inference(scs_inference,[],[1539,1265,42,4,5])).
% 249.42/249.42 cnf(1567,plain,
% 249.42/249.42 (~E(f3(a1,a2),f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[1037,1539,1265,42,4,5,2])).
% 249.42/249.42 cnf(1577,plain,
% 249.42/249.42 (E(f3(x15771,f3(f3(a5,x15772),x15773)),f3(x15771,f3(a5,x15774)))),
% 249.42/249.42 inference(scs_inference,[],[480,595,42,4,5])).
% 249.42/249.42 cnf(1578,plain,
% 249.42/249.42 (~E(f3(a1,a2),f3(a4,a1))),
% 249.42/249.42 inference(scs_inference,[],[908,480,595,42,4,5,2])).
% 249.42/249.42 cnf(1582,plain,
% 249.42/249.42 (~E(a5,f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[6,908,1556,1567,480,595,8,42,4,5,2,12,3])).
% 249.42/249.42 cnf(1583,plain,
% 249.42/249.42 (E(f3(f3(a5,x15831),x15832),f3(f3(f3(a5,x15833),x15834),x15832))),
% 249.42/249.42 inference(scs_inference,[],[484,4])).
% 249.42/249.42 cnf(1584,plain,
% 249.42/249.42 (E(f3(x15841,f3(a5,x15842)),f3(x15841,f3(f3(a5,x15843),x15844)))),
% 249.42/249.42 inference(scs_inference,[],[484,4,5])).
% 249.42/249.42 cnf(1585,plain,
% 249.42/249.42 (~E(f3(x15851,a6),f3(a4,a1))),
% 249.42/249.42 inference(scs_inference,[],[894,484,4,5,2])).
% 249.42/249.42 cnf(1586,plain,
% 249.42/249.42 (~E(f3(f3(a4,a5),a5),a5)),
% 249.42/249.42 inference(scs_inference,[],[894,1582,484,8,4,5,2,12])).
% 249.42/249.42 cnf(1589,plain,
% 249.42/249.42 (~E(a5,f3(a4,a1))),
% 249.42/249.42 inference(scs_inference,[],[6,894,1578,1582,484,8,4,5,2,12,3])).
% 249.42/249.42 cnf(1590,plain,
% 249.42/249.42 (E(f3(f3(f3(f3(a5,x15901),x15902),f3(x15903,x15902)),x15904),f3(f3(a5,x15905),x15904))),
% 249.42/249.42 inference(scs_inference,[],[577,4])).
% 249.42/249.42 cnf(1591,plain,
% 249.42/249.42 (E(f3(x15911,f3(f3(f3(a5,x15912),x15913),f3(x15914,x15913))),f3(x15911,f3(a5,x15915)))),
% 249.42/249.42 inference(scs_inference,[],[577,4,5])).
% 249.42/249.42 cnf(1592,plain,
% 249.42/249.42 (~E(f3(x15921,a6),f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[1050,577,4,5,2])).
% 249.42/249.42 cnf(1593,plain,
% 249.42/249.42 (~E(f3(f3(f3(a5,x15931),x15932),f3(x15933,x15932)),f3(a4,a1))),
% 249.42/249.42 inference(scs_inference,[],[1050,1585,577,486,4,5,2,3])).
% 249.42/249.42 cnf(1599,plain,
% 249.42/249.42 (E(f3(a5,x15991),f3(f3(f3(x15992,x15993),x15992),x15991))),
% 249.42/249.42 inference(scs_inference,[],[135,4])).
% 249.42/249.42 cnf(1600,plain,
% 249.42/249.42 (E(f3(x16001,a5),f3(x16001,f3(f3(x16002,x16003),x16002)))),
% 249.42/249.42 inference(scs_inference,[],[135,4,5])).
% 249.42/249.42 cnf(1604,plain,
% 249.42/249.42 (~E(f3(x16041,a6),f3(a4,a5))),
% 249.42/249.42 inference(rename_variables,[],[1592])).
% 249.42/249.42 cnf(1606,plain,
% 249.42/249.42 (~E(f3(a5,x16061),f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[1592,1604,422,312,135,221,4,5,2,12,3])).
% 249.42/249.42 cnf(1609,plain,
% 249.42/249.42 (E(f3(f3(a5,x16091),x16092),f3(f3(f3(f3(a5,x16093),x16094),f3(x16095,x16094)),x16092))),
% 249.42/249.42 inference(scs_inference,[],[573,4])).
% 249.42/249.42 cnf(1610,plain,
% 249.42/249.42 (E(f3(x16101,f3(a5,x16102)),f3(x16101,f3(f3(f3(a5,x16103),x16104),f3(x16105,x16104))))),
% 249.42/249.42 inference(scs_inference,[],[573,4,5])).
% 249.42/249.42 cnf(1612,plain,
% 249.42/249.42 (~E(f3(f3(a4,a5),f3(a5,x16121)),a5)),
% 249.42/249.42 inference(scs_inference,[],[1606,475,573,207,4,5,2,12])).
% 249.42/249.42 cnf(1615,plain,
% 249.42/249.42 (~E(f3(f3(f3(x16151,x16152),x16151),x16153),f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[1606,475,1599,573,207,4,5,2,12,3])).
% 249.42/249.42 cnf(1620,plain,
% 249.42/249.42 (E(f3(a5,x16201),f3(f3(f3(a5,x16202),x16203),x16201))),
% 249.42/249.42 inference(scs_inference,[],[314,4])).
% 249.42/249.42 cnf(1621,plain,
% 249.42/249.42 (E(f3(x16211,a5),f3(x16211,f3(f3(a5,x16212),x16213)))),
% 249.42/249.42 inference(scs_inference,[],[314,4,5])).
% 249.42/249.42 cnf(1622,plain,
% 249.42/249.42 (~E(f3(x16221,a6),a4)),
% 249.42/249.42 inference(scs_inference,[],[511,314,4,5,2])).
% 249.42/249.42 cnf(1627,plain,
% 249.42/249.42 (~E(f3(f3(f3(a5,x16271),x16272),x16273),f3(a4,a2))),
% 249.42/249.42 inference(scs_inference,[],[511,1146,1615,1583,314,29,4,5,2,12,3])).
% 249.42/249.42 cnf(1629,plain,
% 249.42/249.42 (E(f3(a5,x16291),f3(f3(a1,a2),x16291))),
% 249.42/249.42 inference(scs_inference,[],[21,4])).
% 249.42/249.42 cnf(1630,plain,
% 249.42/249.42 (E(f3(x16301,a5),f3(x16301,f3(a1,a2)))),
% 249.42/249.42 inference(scs_inference,[],[21,4,5])).
% 249.42/249.42 cnf(1632,plain,
% 249.42/249.42 (~E(f3(f3(f3(f3(x16321,x16322),f3(x16323,x16322)),x16324),f3(x16321,x16323)),f3(a4,a1))),
% 249.42/249.42 inference(scs_inference,[],[1589,727,190,21,4,5,2,3])).
% 249.42/249.42 cnf(1636,plain,
% 249.42/249.42 (E(f3(x16361,f3(a5,x16362)),f3(x16361,f3(f3(a1,a2),x16362)))),
% 249.42/249.42 inference(scs_inference,[],[1629,5])).
% 249.42/249.42 cnf(1638,plain,
% 249.42/249.42 (E(f3(f3(a5,x16381),x16382),f3(f3(f3(a1,a2),x16381),x16382))),
% 249.42/249.42 inference(scs_inference,[],[835,1629,5,2,4])).
% 249.42/249.42 cnf(1641,plain,
% 249.42/249.42 (E(f3(x16411,f3(x16412,a6)),f3(x16411,a5))),
% 249.42/249.42 inference(scs_inference,[],[7,5])).
% 249.42/249.42 cnf(1643,plain,
% 249.42/249.42 (E(f3(f3(x16431,a5),x16432),f3(f3(x16431,f3(a1,a2)),x16432))),
% 249.42/249.42 inference(scs_inference,[],[7,770,1630,5,2,4])).
% 249.42/249.42 cnf(1645,plain,
% 249.42/249.42 (~E(f3(a6,f3(a5,x16451)),a5)),
% 249.42/249.42 inference(scs_inference,[],[7,770,1630,1349,298,664,5,2,4,3,13])).
% 249.42/249.42 cnf(1648,plain,
% 249.42/249.42 (E(f3(x16481,f3(x16482,f3(x16483,a6))),f3(x16481,f3(x16482,a5)))),
% 249.42/249.42 inference(scs_inference,[],[1641,5])).
% 249.42/249.42 cnf(1649,plain,
% 249.42/249.42 (~E(f3(x16491,a6),f3(f3(a4,a2),a5))),
% 249.42/249.42 inference(scs_inference,[],[776,1641,5,2])).
% 249.42/249.42 cnf(1650,plain,
% 249.42/249.42 (E(f3(f3(x16501,f3(x16502,a6)),x16503),f3(f3(x16501,a5),x16503))),
% 249.42/249.42 inference(scs_inference,[],[776,1641,5,2,4])).
% 249.42/249.42 cnf(1651,plain,
% 249.42/249.42 (~E(a6,f3(x16511,a6))),
% 249.42/249.42 inference(scs_inference,[],[7,1540,776,1641,5,2,4,3])).
% 249.42/249.42 cnf(1652,plain,
% 249.42/249.42 (E(f3(x16521,f3(x16522,a5)),f3(x16521,f3(x16522,f3(a1,a2))))),
% 249.42/249.42 inference(scs_inference,[],[1630,5])).
% 249.42/249.42 cnf(1653,plain,
% 249.42/249.42 (~E(f3(x16531,a6),a6)),
% 249.42/249.42 inference(scs_inference,[],[1651,1630,5,2])).
% 249.42/249.42 cnf(1654,plain,
% 249.42/249.42 (E(f3(a5,x16541),f3(f3(f3(a1,x16542),a2),x16541))),
% 249.42/249.42 inference(scs_inference,[],[1651,1630,198,5,2,4])).
% 249.42/249.42 cnf(1656,plain,
% 249.42/249.42 (~E(f3(a4,f3(a4,a6)),a5)),
% 249.42/249.42 inference(scs_inference,[],[1622,1651,349,775,1630,198,9,5,2,4,3,12])).
% 249.42/249.42 cnf(1660,plain,
% 249.42/249.42 (E(f3(x16601,a5),f3(x16601,f3(x16602,a6)))),
% 249.42/249.42 inference(scs_inference,[],[14,5])).
% 249.42/249.42 cnf(1661,plain,
% 249.42/249.42 (~E(f3(x16611,a6),f3(f3(a4,a2),f3(a5,x16612)))),
% 249.42/249.42 inference(scs_inference,[],[834,14,5,2])).
% 249.42/249.42 cnf(1662,plain,
% 249.42/249.42 (E(f3(f3(a5,x16621),x16622),f3(f3(f3(x16623,a6),x16621),x16622))),
% 249.42/249.42 inference(scs_inference,[],[834,14,340,5,2,4])).
% 249.42/249.42 cnf(1667,plain,
% 249.42/249.42 (~E(f3(a6,f3(a4,a1)),f3(x16671,a6))),
% 249.42/249.42 inference(scs_inference,[],[7,1653,834,1364,14,340,221,5,2,4,12,3])).
% 249.42/249.42 cnf(1669,plain,
% 249.42/249.42 (E(f3(x16691,f3(x16692,a5)),f3(x16691,f3(x16692,f3(x16693,a6))))),
% 249.42/249.42 inference(scs_inference,[],[1660,5])).
% 249.42/249.42 cnf(1670,plain,
% 249.42/249.42 (~E(f3(x16701,a6),f3(a6,f3(a4,a1)))),
% 249.42/249.42 inference(scs_inference,[],[1667,1660,5,2])).
% 249.42/249.42 cnf(1671,plain,
% 249.42/249.42 (E(f3(f3(x16711,a5),x16712),f3(f3(x16711,f3(x16713,a6)),x16712))),
% 249.42/249.42 inference(scs_inference,[],[1667,1660,5,2,4])).
% 249.42/249.42 cnf(1672,plain,
% 249.42/249.42 (~E(f3(f3(a4,f3(a2,x16721)),f3(a5,a2)),a5)),
% 249.42/249.42 inference(scs_inference,[],[1667,1507,1660,207,5,2,4,12])).
% 249.42/249.42 cnf(1675,plain,
% 249.42/249.42 (~E(a5,f3(f3(a4,a2),a5))),
% 249.42/249.42 inference(scs_inference,[],[7,1667,1507,1649,1660,207,5,2,4,12,3])).
% 249.42/249.42 cnf(1676,plain,
% 249.42/249.42 (E(f3(x16761,a6),a5)),
% 249.42/249.42 inference(rename_variables,[],[7])).
% 249.42/249.42 cnf(1677,plain,
% 249.42/249.42 (~E(f3(a6,f3(a4,a6)),a5)),
% 249.42/249.42 inference(scs_inference,[],[7,1676,1667,1507,1649,1660,1656,207,5,2,4,12,3,13])).
% 249.42/249.42 cnf(1680,plain,
% 249.42/249.42 (E(f3(x16801,a5),f3(x16801,f3(f3(a1,x16802),a2)))),
% 249.42/249.42 inference(scs_inference,[],[198,5])).
% 249.42/249.42 cnf(1682,plain,
% 249.42/249.42 (E(f3(f3(x16821,f3(a5,x16822)),x16823),f3(f3(x16821,a5),x16823))),
% 249.42/249.42 inference(scs_inference,[],[726,198,366,5,2,4])).
% 249.42/249.42 cnf(1687,plain,
% 249.42/249.42 (~E(f3(a4,f3(a4,a1)),f3(x16871,a6))),
% 249.42/249.42 inference(scs_inference,[],[7,726,1369,1670,198,366,221,5,2,4,12,3])).
% 249.42/249.42 cnf(1688,plain,
% 249.42/249.42 (E(f3(x16881,f3(a5,x16882)),f3(x16881,f3(f3(x16883,a6),x16882)))),
% 249.42/249.42 inference(scs_inference,[],[340,5])).
% 249.42/249.42 cnf(1690,plain,
% 249.42/249.42 (E(f3(f3(x16901,a5),x16902),f3(f3(x16901,f3(a5,x16903)),x16902))),
% 249.42/249.42 inference(scs_inference,[],[1687,340,367,5,2,4])).
% 249.42/249.42 cnf(1694,plain,
% 249.42/249.42 (~E(a5,f3(f3(a4,a2),f3(a5,x16941)))),
% 249.42/249.42 inference(scs_inference,[],[7,1687,1661,1677,340,367,8,5,2,4,12,3])).
% 249.42/249.42 cnf(1696,plain,
% 249.42/249.42 (E(f3(x16961,f3(x16962,f3(a5,x16963))),f3(x16961,f3(x16962,a5)))),
% 249.42/249.42 inference(scs_inference,[],[366,5])).
% 249.42/249.42 cnf(1698,plain,
% 249.42/249.42 (E(f3(f3(f3(x16981,a6),x16982),x16983),f3(f3(a5,x16982),x16983))),
% 249.42/249.42 inference(scs_inference,[],[829,366,339,5,2,4])).
% 249.42/249.42 cnf(1717,plain,
% 249.42/249.42 (~E(f3(a1,a2),f3(a4,f3(a1,x17171)))),
% 249.42/249.42 inference(scs_inference,[],[721,339,5,2])).
% 249.42/249.42 cnf(1718,plain,
% 249.42/249.42 (E(f3(f3(f3(a5,x17181),x17182),x17183),f3(a5,x17183))),
% 249.42/249.42 inference(scs_inference,[],[721,339,207,5,2,4])).
% 249.42/249.42 cnf(1725,plain,
% 249.42/249.42 (E(f3(x17251,f3(f3(x17252,x17253),x17252)),f3(x17251,a5))),
% 249.42/249.42 inference(scs_inference,[],[9,5])).
% 249.42/249.42 cnf(1726,plain,
% 249.42/249.42 (E(f3(f3(f3(a1,x17261),a2),x17262),f3(a5,x17262))),
% 249.42/249.42 inference(scs_inference,[],[9,191,5,4])).
% 249.42/249.42 cnf(1728,plain,
% 249.42/249.42 (~E(f3(a5,f3(x17281,x17282)),f3(a4,a1))),
% 249.42/249.42 inference(scs_inference,[],[967,1593,1718,9,191,5,4,2,3])).
% 249.42/249.42 cnf(1733,plain,
% 249.42/249.42 (E(f3(x17331,f3(f3(a5,x17332),x17333)),f3(x17331,a5))),
% 249.42/249.42 inference(scs_inference,[],[207,5])).
% 249.42/249.42 cnf(1741,plain,
% 249.42/249.42 (~E(f3(f3(a4,x17411),f3(a1,x17411)),f3(a4,a2))),
% 249.42/249.42 inference(scs_inference,[],[138,191,5,2])).
% 249.42/249.42 cnf(1742,plain,
% 249.42/249.42 (~E(f3(a5,a5),f3(a4,a1))),
% 249.42/249.42 inference(scs_inference,[],[1728,138,1725,191,5,2,3])).
% 249.42/249.42 cnf(1752,plain,
% 249.42/249.42 (~E(f3(f3(a4,a5),f3(a1,f3(a1,a2))),f3(a4,a2))),
% 249.42/249.42 inference(scs_inference,[],[1741,527,1565,2,3])).
% 249.42/249.42 cnf(1761,plain,
% 249.42/249.42 (~E(a6,f3(f3(a2,x17611),f3(x17612,x17611)))),
% 249.42/249.42 inference(scs_inference,[],[992,2])).
% 249.42/249.42 cnf(1765,plain,
% 249.42/249.42 (E(f3(x17651,a6),a5)),
% 249.42/249.42 inference(rename_variables,[],[7])).
% 249.42/249.42 cnf(1767,plain,
% 249.42/249.42 (~E(f3(a6,f3(f3(a4,x17671),f3(a1,x17671))),a5)),
% 249.42/249.42 inference(scs_inference,[],[1742,992,1620,1557,7,1765,2,3,12,13])).
% 249.42/249.42 cnf(1770,plain,
% 249.42/249.42 (~E(a5,f3(f3(a4,a5),a5))),
% 249.42/249.42 inference(scs_inference,[],[1586,2])).
% 249.42/249.42 cnf(1777,plain,
% 249.42/249.42 (~E(a5,f3(f3(a4,a2),f3(a4,a1)))),
% 249.42/249.42 inference(scs_inference,[],[8,428,362,2,3])).
% 249.42/249.42 cnf(1780,plain,
% 249.42/249.42 (~E(f3(a6,f3(f3(a1,x17801),x17802)),a5)),
% 249.42/249.42 inference(scs_inference,[],[8,428,748,362,7,2,3,12])).
% 249.42/249.42 cnf(1783,plain,
% 249.42/249.42 (~E(f3(f3(x17831,a6),x17832),a4)),
% 249.42/249.42 inference(scs_inference,[],[620,2])).
% 249.42/249.42 cnf(1784,plain,
% 249.42/249.42 (~E(a6,f3(f3(a2,a2),a5))),
% 249.42/249.42 inference(scs_inference,[],[1761,620,1680,2,3])).
% 249.42/249.42 cnf(1787,plain,
% 249.42/249.42 (~E(f3(f3(a2,a2),a5),a6)),
% 249.42/249.42 inference(scs_inference,[],[1784,2])).
% 249.42/249.42 cnf(1788,plain,
% 249.42/249.42 (~E(f3(f3(f3(a1,x17881),a2),a5),f3(a4,a1))),
% 249.42/249.42 inference(scs_inference,[],[1784,1654,1742,2,3])).
% 249.42/249.42 cnf(1790,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a4,a6),f3(x17901,a6))),a5)),
% 249.42/249.42 inference(scs_inference,[],[1784,1783,1654,1742,29,2,3,12])).
% 249.42/249.42 cnf(1798,plain,
% 249.42/249.42 (~E(a6,f3(f3(a5,x17981),x17982))),
% 249.42/249.42 inference(scs_inference,[],[808,2])).
% 249.42/249.42 cnf(1799,plain,
% 249.42/249.42 (~E(a4,f3(f3(a4,a5),f3(a1,f3(a1,a2))))),
% 249.42/249.42 inference(scs_inference,[],[808,188,1566,2,3])).
% 249.42/249.42 cnf(1802,plain,
% 249.42/249.42 (~E(f3(a6,f3(f3(a5,x18021),x18022)),a5)),
% 249.42/249.42 inference(scs_inference,[],[808,188,1566,221,2,3,12])).
% 249.42/249.42 cnf(1806,plain,
% 249.42/249.42 (~E(a5,f3(f3(a4,a5),f3(a5,x18061)))),
% 249.42/249.42 inference(scs_inference,[],[1612,2])).
% 249.42/249.42 cnf(1823,plain,
% 249.42/249.42 (~E(f3(a6,f3(f3(a4,a6),f3(x18231,a6))),a5)),
% 249.42/249.42 inference(scs_inference,[],[805,1806,1121,1790,1638,7,8,2,3,12,13])).
% 249.42/249.42 cnf(1831,plain,
% 249.42/249.42 (~E(f3(f3(a5,x18311),f3(a5,x18312)),f3(a4,a1))),
% 249.42/249.42 inference(scs_inference,[],[1645,1632,1590,2,3])).
% 249.42/249.42 cnf(1837,plain,
% 249.42/249.42 (~E(f3(a5,x18371),f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x18372)))),
% 249.42/249.42 inference(scs_inference,[],[1177,2])).
% 249.42/249.42 cnf(1838,plain,
% 249.42/249.42 (~E(f3(f3(a2,a2),f3(f3(x18381,x18382),x18381)),a6)),
% 249.42/249.42 inference(scs_inference,[],[1787,1177,1600,2,3])).
% 249.42/249.42 cnf(1840,plain,
% 249.42/249.42 (~E(f3(x18401,a6),f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x18402)))),
% 249.42/249.42 inference(scs_inference,[],[1172,2])).
% 249.42/249.42 cnf(1841,plain,
% 249.42/249.42 (~E(f3(f3(a5,x18411),f3(f3(a1,a2),x18412)),f3(a4,a1))),
% 249.42/249.42 inference(scs_inference,[],[1831,1172,1636,2,3])).
% 249.42/249.42 cnf(1843,plain,
% 249.42/249.42 (~E(f3(f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x18431)),f3(a5,x18432)),a5)),
% 249.42/249.42 inference(scs_inference,[],[1831,1172,1837,1636,207,2,3,12])).
% 249.42/249.42 cnf(1856,plain,
% 249.42/249.42 (~E(f3(f3(f3(f3(a4,a2),a5),f3(a4,a1)),f3(a5,x18561)),a5)),
% 249.42/249.42 inference(scs_inference,[],[1770,1170,439,1843,1696,10,8,2,3,12,13])).
% 249.42/249.42 cnf(1860,plain,
% 249.42/249.42 (~E(f3(f3(f3(x18601,x18602),f3(x18603,x18602)),f3(x18601,x18603)),f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[1026,2])).
% 249.42/249.42 cnf(1864,plain,
% 249.42/249.42 (~E(f3(f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x18641)),f3(f3(a5,x18642),a6)),a5)),
% 249.42/249.42 inference(scs_inference,[],[1026,1840,1841,284,221,2,3,12])).
% 249.42/249.42 cnf(1868,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a2),a5),f3(a5,x18681)),a5)),
% 249.42/249.42 inference(scs_inference,[],[9,1026,1840,1841,1856,284,221,2,3,12,13])).
% 249.42/249.42 cnf(1872,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a2),f3(a1,a2)),f3(a5,x18721)),a5)),
% 249.42/249.42 inference(scs_inference,[],[1087,1868,1643,2,3])).
% 249.42/249.42 cnf(1878,plain,
% 249.42/249.42 (~E(f3(f3(a5,f3(x18781,a2)),f3(a1,x18781)),f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[1860,1310,1554,2,3])).
% 249.42/249.42 cnf(1880,plain,
% 249.42/249.42 (~E(f3(f3(f3(x18801,x18802),f3(x18803,x18802)),f3(x18801,x18803)),f3(a4,a5))),
% 249.42/249.42 inference(rename_variables,[],[1860])).
% 249.42/249.42 cnf(1885,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a1),a2),f3(a5,x18851)),a5)),
% 249.42/249.42 inference(scs_inference,[],[1860,1880,1310,1872,1554,181,10,2,3,12,13])).
% 249.42/249.42 cnf(1889,plain,
% 249.42/249.42 (~E(f3(f3(a5,a5),f3(a1,a5)),f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[1878,751,1682,2,3])).
% 249.42/249.42 cnf(1907,plain,
% 249.42/249.42 (~E(f3(f3(a5,a5),f3(a1,f3(a1,a2))),f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[1889,1229,1652,2,3])).
% 249.42/249.42 cnf(1914,plain,
% 249.42/249.42 (~E(f3(f3(x19141,a6),x19142),f3(a4,f3(a5,x19143)))),
% 249.42/249.42 inference(scs_inference,[],[1430,2])).
% 249.42/249.42 cnf(1933,plain,
% 249.42/249.42 (~E(f3(f3(f3(a5,a6),x19331),x19332),f3(a4,f3(a5,x19333)))),
% 249.42/249.42 inference(scs_inference,[],[1914,701,238,2,3])).
% 249.42/249.42 cnf(1948,plain,
% 249.42/249.42 (~E(f3(f3(f3(x19481,a6),a5),f3(a1,f3(a1,a2))),f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[506,1907,1662,2,3])).
% 249.42/249.42 cnf(1955,plain,
% 249.42/249.42 (~E(a6,f3(f3(f3(x19551,a6),x19552),x19553))),
% 249.42/249.42 inference(scs_inference,[],[1798,1363,1698,2,3])).
% 249.42/249.42 cnf(1958,plain,
% 249.42/249.42 (~E(f3(f3(f3(x19581,x19582),f3(x19583,x19582)),x19581),f3(f3(a4,a2),f3(a4,a1)))),
% 249.42/249.42 inference(scs_inference,[],[1777,1456,128,2,3])).
% 249.42/249.42 cnf(1965,plain,
% 249.42/249.42 (~E(a5,f3(f3(a4,f3(a2,x19651)),f3(a5,a2)))),
% 249.42/249.42 inference(scs_inference,[],[1672,2])).
% 249.42/249.42 cnf(1972,plain,
% 249.42/249.42 (~E(a5,f3(f3(f3(a4,a1),a2),f3(a5,x19721)))),
% 249.42/249.42 inference(scs_inference,[],[1885,2])).
% 249.42/249.42 cnf(1987,plain,
% 249.42/249.42 (~E(f3(x19871,a6),f3(f3(f3(a4,a1),a2),f3(a5,x19872)))),
% 249.42/249.42 inference(scs_inference,[],[14,1972,1752,2,3])).
% 249.42/249.42 cnf(1994,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a1),a2),f3(a5,x19941)),f3(x19942,a6))),
% 249.42/249.42 inference(scs_inference,[],[1987,2])).
% 249.42/249.42 cnf(2000,plain,
% 249.42/249.42 (~E(f3(x20001,a6),f3(f3(a4,a2),f3(f3(a4,a1),x20002)))),
% 249.42/249.42 inference(scs_inference,[],[926,2])).
% 249.42/249.42 cnf(2001,plain,
% 249.42/249.42 (~E(f3(x20011,a6),f3(a4,a2))),
% 249.42/249.42 inference(scs_inference,[],[14,926,382,2,3])).
% 249.42/249.42 cnf(2002,plain,
% 249.42/249.42 (~E(f3(x20021,a6),f3(f3(f3(a4,a2),f3(a4,a1)),a5))),
% 249.42/249.42 inference(scs_inference,[],[663,2])).
% 249.42/249.42 cnf(2003,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a1),a2),f3(f3(x20031,a6),x20032)),f3(x20033,a6))),
% 249.42/249.42 inference(scs_inference,[],[1994,663,1688,2,3])).
% 249.42/249.42 cnf(2006,plain,
% 249.42/249.42 (~E(f3(x20061,a6),f3(f3(a4,a2),f3(f3(a5,x20062),x20063)))),
% 249.42/249.42 inference(scs_inference,[],[807,2])).
% 249.42/249.42 cnf(2007,plain,
% 249.42/249.42 (~E(f3(x20071,a6),f3(a6,a5))),
% 249.42/249.42 inference(scs_inference,[],[14,807,1556,2,3])).
% 249.42/249.42 cnf(2014,plain,
% 249.42/249.42 (~E(f3(a6,a5),f3(x20141,a6))),
% 249.42/249.42 inference(scs_inference,[],[2007,2])).
% 249.42/249.42 cnf(2022,plain,
% 249.42/249.42 (~E(f3(x20221,a6),f3(f3(a4,a2),f3(f3(a4,x20222),f3(a1,x20222))))),
% 249.42/249.42 inference(scs_inference,[],[690,2])).
% 249.42/249.42 cnf(2032,plain,
% 249.42/249.42 (~E(f3(a6,f3(f3(a5,x20321),x20322)),f3(x20323,a6))),
% 249.42/249.42 inference(scs_inference,[],[2014,1788,1864,1621,10,2,13,3])).
% 249.42/249.42 cnf(2042,plain,
% 249.42/249.42 (~E(f3(x20421,a6),f3(a4,f3(f3(a2,x20422),f3(x20423,x20422))))),
% 249.42/249.42 inference(scs_inference,[],[991,2])).
% 249.42/249.42 cnf(2043,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a2,a2),a5)),f3(x20431,a6))),
% 249.42/249.42 inference(scs_inference,[],[991,1566,2,3])).
% 249.42/249.42 cnf(2046,plain,
% 249.42/249.42 (~E(f3(x20461,a6),f3(a4,f3(f3(a1,x20462),x20463)))),
% 249.42/249.42 inference(scs_inference,[],[747,2])).
% 249.42/249.42 cnf(2049,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(a4,a6),a5)),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[941,686,1648,2,3])).
% 249.42/249.42 cnf(2053,plain,
% 249.42/249.42 (~E(f3(a5,x20531),f3(f3(a4,a2),a5))),
% 249.42/249.42 inference(scs_inference,[],[15,2049,1675,2,3])).
% 249.42/249.42 cnf(2056,plain,
% 249.42/249.42 (~E(f3(f3(a4,a2),f3(f3(f3(a4,a2),a6),f3(a5,a6))),a5)),
% 249.42/249.42 inference(scs_inference,[],[15,1717,2049,1562,1675,9,2,3,12,13])).
% 249.42/249.42 cnf(2063,plain,
% 249.42/249.42 (~E(f3(a4,f3(f3(a2,x20631),a5)),f3(a1,a2))),
% 249.42/249.42 inference(scs_inference,[],[2032,987,2056,1696,9,2,13,3])).
% 249.42/249.42 cnf(2071,plain,
% 249.42/249.42 (~E(f3(x20711,a6),f3(a4,f3(f3(a2,a2),a5)))),
% 249.42/249.42 inference(scs_inference,[],[2043,2])).
% 249.42/249.42 cnf(2077,plain,
% 249.42/249.42 (~E(f3(a1,a2),f3(a4,f3(f3(a2,x20771),a5)))),
% 249.42/249.42 inference(scs_inference,[],[2063,2])).
% 249.42/249.42 cnf(2078,plain,
% 249.42/249.42 (~E(f3(a6,f3(f3(a2,x20781),x20782)),a5)),
% 249.42/249.42 inference(scs_inference,[],[2063,1063,7,2,13])).
% 249.42/249.42 cnf(2081,plain,
% 249.42/249.42 (~E(f3(a5,x20811),f3(f3(a4,a2),f3(a5,x20812)))),
% 249.42/249.42 inference(scs_inference,[],[15,2063,1694,1063,7,2,13,3])).
% 249.42/249.42 cnf(2085,plain,
% 249.42/249.42 (~E(f3(a1,a2),f3(a4,f3(f3(a1,x20851),x20852)))),
% 249.42/249.42 inference(scs_inference,[],[742,2])).
% 249.42/249.42 cnf(2090,plain,
% 249.42/249.42 (~E(f3(a5,x20901),f3(f3(a4,a5),f3(a5,x20902)))),
% 249.42/249.42 inference(scs_inference,[],[15,937,1806,2,3])).
% 249.42/249.42 cnf(2091,plain,
% 249.42/249.42 (~E(f3(f3(a4,a5),f3(a5,x20911)),f3(a5,x20912))),
% 249.42/249.42 inference(scs_inference,[],[2090,2])).
% 249.42/249.42 cnf(2096,plain,
% 249.42/249.42 (~E(f3(f3(x20961,x20962),x20961),f3(f3(f3(a4,a2),f3(a4,a1)),f3(a5,x20963)))),
% 249.42/249.42 inference(scs_inference,[],[1174,2])).
% 249.42/249.42 cnf(2097,plain,
% 249.42/249.42 (~E(f3(a5,x20971),f3(f3(a4,a5),a5))),
% 249.42/249.42 inference(scs_inference,[],[15,1174,1770,2,3])).
% 249.42/249.42 cnf(2098,plain,
% 249.42/249.42 (~E(f3(a6,f3(a2,x20981)),a5)),
% 249.42/249.42 inference(scs_inference,[],[15,1174,1770,446,7,2,3,13])).
% 249.42/249.42 cnf(2101,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a5),f3(a5,x21011)),f3(a5,x21012)),a5)),
% 249.42/249.42 inference(scs_inference,[],[15,2091,1174,1770,446,207,7,2,3,13,12])).
% 249.42/249.42 cnf(2105,plain,
% 249.42/249.42 (~E(f3(f3(a4,a5),a5),f3(a5,x21051))),
% 249.42/249.42 inference(scs_inference,[],[2097,2])).
% 249.42/249.42 cnf(2107,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a5),f3(a5,x21071)),f3(a5,x21072)),a5)),
% 249.42/249.42 inference(rename_variables,[],[2101])).
% 249.42/249.42 cnf(2109,plain,
% 249.42/249.42 (~E(f3(f3(f3(a4,a5),a5),f3(a5,x21091)),a5)),
% 249.42/249.42 inference(scs_inference,[],[2097,2101,2107,1610,10,2,3,13])).
% 249.42/249.42 cnf(2114,plain,
% 249.42/249.42 (~E(f3(f3(a5,a1),a5),f3(a4,a5))),
% 249.42/249.42 inference(scs_inference,[],[2098,1889,284,2,3])).
% 249.42/249.42 cnf(2120,plain,
% 249.42/249.42 (~E(a5,f3(f3(f3(a4,a5),a5),f3(a5,x21201)))),
% 249.42/249.42 inference(scs_inference,[],[2109,2])).
% 249.42/249.42 cnf(2121,plain,
% 249.42/249.42 (~E(f3(f3(a4,f3(a5,x21211)),a5),f3(a5,x21212))),
% 249.42/249.42 inference(scs_inference,[],[2105,2109,1690,2,3])).
% 249.42/249.42 cnf(2126,plain,
% 249.42/249.42 (~E(f3(a5,x21261),f3(f3(a4,f3(a5,x21262)),a5))),
% 249.42/249.42 inference(scs_inference,[],[2121,2])).
% 249.42/249.42 cnf(2127,plain,
% 249.42/249.42 (~E(f3(f3(f3(a5,x21271),x21272),x21273),f3(f3(f3(a4,a5),a5),f3(a5,x21274)))),
% 249.42/249.42 inference(scs_inference,[],[2120,2121,289,2,3])).
% 249.42/249.42 cnf(2128,plain,
% 249.42/249.43 (~E(f3(f3(f3(a4,a2),f3(a5,x21281)),f3(a5,x21282)),a5)),
% 249.42/249.43 inference(scs_inference,[],[2081,2120,2121,289,207,2,3,12])).
% 249.42/249.43 cnf(2133,plain,
% 249.42/249.43 (~E(f3(f3(f3(a4,a2),f3(a4,a1)),f3(f3(a1,a2),x21331)),f3(f3(a5,x21332),x21333))),
% 249.42/249.43 inference(scs_inference,[],[2128,1164,1636,2,3])).
% 249.42/249.43 cnf(2167,plain,
% 249.42/249.43 (~E(f3(f3(a2,a2),f3(a5,x21671)),a6)),
% 249.42/249.43 inference(scs_inference,[],[1526,1838,1591,2,3])).
% 249.42/249.43 cnf(2170,plain,
% 249.42/249.43 (~E(a6,f3(f3(a2,a2),f3(a5,x21701)))),
% 249.42/249.43 inference(scs_inference,[],[2167,2])).
% 249.42/249.43 cnf(2175,plain,
% 249.42/249.43 (~E(f3(f3(f3(a1,x21751),x21752),a2),f3(a4,a1))),
% 249.42/249.43 inference(scs_inference,[],[872,2])).
% 249.42/249.43 cnf(2191,plain,
% 249.42/249.43 (~E(a6,f3(f3(a2,a2),f3(f3(a1,a2),x21911)))),
% 249.42/249.43 inference(scs_inference,[],[2170,507,1555,1058,7,2,13,3])).
% 249.42/249.43 cnf(2198,plain,
% 249.42/249.43 (~E(f3(a5,a2),f3(a4,a1))),
% 249.42/249.43 inference(scs_inference,[],[2175,1726,1799,2,3])).
% 249.42/249.43 cnf(2210,plain,
% 249.42/249.43 (~E(f3(f3(f3(a4,f3(a5,x22101)),a5),f3(a5,x22102)),a5)),
% 249.42/249.43 inference(scs_inference,[],[2198,2126,719,1599,207,2,3,12])).
% 249.42/249.43 cnf(2227,plain,
% 249.42/249.43 (~E(f3(f3(a4,f3(a5,x22271)),f3(a5,x22272)),a5)),
% 249.42/249.43 inference(scs_inference,[],[1955,2210,9,2,13])).
% 249.42/249.43 cnf(2230,plain,
% 249.42/249.43 (~E(f3(a6,f3(f3(a4,a6),a5)),a5)),
% 249.42/249.43 inference(scs_inference,[],[1955,1823,2210,1648,9,2,13,3])).
% 249.42/249.43 cnf(2233,plain,
% 249.42/249.43 (~E(a5,f3(f3(a4,f3(a5,x22331)),f3(a5,x22332)))),
% 249.42/249.43 inference(scs_inference,[],[2227,2])).
% 249.42/249.43 cnf(2237,plain,
% 249.42/249.43 (~E(f3(a6,a1),a5)),
% 249.42/249.43 inference(scs_inference,[],[2227,1146,44,405,7,2,3,13])).
% 249.42/249.43 cnf(2240,plain,
% 249.42/249.43 (~E(a5,f3(a6,a1))),
% 249.42/249.43 inference(scs_inference,[],[2237,2])).
% 249.42/249.43 cnf(2245,plain,
% 249.42/249.43 (~E(a5,f3(a6,f3(f3(a4,a6),a5)))),
% 249.42/249.43 inference(scs_inference,[],[2230,2])).
% 249.42/249.43 cnf(2247,plain,
% 249.42/249.43 (~E(f3(f3(a6,a1),a5),a5)),
% 249.42/249.43 inference(scs_inference,[],[2240,2230,361,8,2,3,12])).
% 249.42/249.43 cnf(2250,plain,
% 249.42/249.43 (~E(a5,f3(f3(a6,a1),a5))),
% 249.42/249.43 inference(scs_inference,[],[2247,2])).
% 249.42/249.43 cnf(2251,plain,
% 249.42/249.43 (~E(f3(f3(a6,a1),f3(f3(x22511,x22512),x22511)),a5)),
% 249.42/249.43 inference(scs_inference,[],[2247,1600,2,3])).
% 249.42/249.43 cnf(2253,plain,
% 249.42/249.43 (~E(a5,f3(f3(a6,a1),f3(f3(x22531,x22532),x22531)))),
% 249.42/249.43 inference(scs_inference,[],[2251,2])).
% 249.42/249.43 cnf(2257,plain,
% 249.42/249.43 (~E(f3(a6,f3(f3(x22571,x22572),x22571)),a5)),
% 249.42/249.43 inference(scs_inference,[],[2250,2251,9,8,2,12,13])).
% 249.42/249.43 cnf(2260,plain,
% 249.42/249.43 (~E(f3(a1,a2),f3(f3(a6,a1),a5))),
% 249.42/249.43 inference(scs_inference,[],[21,2250,2251,9,8,2,12,13,3])).
% 249.42/249.43 cnf(2266,plain,
% 249.42/249.43 (~E(f3(a6,a2),a5)),
% 249.42/249.43 inference(scs_inference,[],[2260,1372,81,207,7,2,12,13])).
% 249.42/249.43 cnf(2269,plain,
% 249.42/249.43 (~E(f3(a1,a2),f3(f3(a6,a1),f3(f3(x22691,x22692),x22691)))),
% 249.42/249.43 inference(scs_inference,[],[21,2260,2253,1372,81,207,7,2,12,13,3])).
% 249.42/249.43 cnf(2270,plain,
% 249.42/249.43 (~E(a5,f3(a6,a2))),
% 249.42/249.43 inference(scs_inference,[],[2266,2])).
% 249.42/249.43 cnf(2271,plain,
% 249.42/249.43 (~E(f3(a1,a2),f3(a6,f3(f3(a4,a6),a5)))),
% 249.42/249.43 inference(scs_inference,[],[21,2266,2245,2,3])).
% 249.42/249.43 cnf(2272,plain,
% 249.42/249.43 (~E(f3(f3(a6,a2),a5),a5)),
% 249.42/249.43 inference(scs_inference,[],[21,2266,2245,8,2,3,12])).
% 249.42/249.43 cnf(2275,plain,
% 249.42/249.43 (~E(a5,f3(f3(a6,a2),a5))),
% 249.42/249.43 inference(scs_inference,[],[2272,2])).
% 249.42/249.43 cnf(2276,plain,
% 249.42/249.43 (~E(f3(a1,a2),f3(a6,a2))),
% 249.42/249.43 inference(scs_inference,[],[21,2270,2272,2,3])).
% 249.42/249.43 cnf(2277,plain,
% 249.42/249.43 (~E(f3(a6,a2),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2276,2])).
% 249.42/249.43 cnf(2281,plain,
% 249.42/249.43 (~E(f3(a1,a2),f3(f3(a6,a2),a5))),
% 249.42/249.43 inference(scs_inference,[],[21,2276,2275,8,2,12,3])).
% 249.42/249.43 cnf(2282,plain,
% 249.42/249.43 (~E(f3(f3(a6,a2),a5),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2281,2])).
% 249.42/249.43 cnf(2292,plain,
% 249.42/249.43 (~E(f3(f3(a6,a1),f3(f3(x22921,x22922),x22921)),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2269,2])).
% 249.42/249.43 cnf(2293,plain,
% 249.42/249.43 (~E(f3(f3(a6,a2),f3(f3(a1,x22931),a2)),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2282,2269,1680,2,3])).
% 249.42/249.43 cnf(2296,plain,
% 249.42/249.43 (~E(f3(a1,a2),f3(f3(a4,f3(a2,x22961)),f3(a5,a2)))),
% 249.42/249.43 inference(scs_inference,[],[21,2293,1965,2,3])).
% 249.42/249.43 cnf(2297,plain,
% 249.42/249.43 (~E(f3(f3(a6,a2),f3(a1,a2)),a5)+~E(f3(f3(a1,a2),f3(a6,a2)),a5)),
% 249.42/249.43 inference(scs_inference,[],[21,2277,2293,1965,2,3,12])).
% 249.42/249.43 cnf(2300,plain,
% 249.42/249.43 (~E(f3(f3(a4,f3(a2,x23001)),f3(a5,a2)),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2296,2])).
% 249.42/249.43 cnf(2301,plain,
% 249.42/249.43 (~E(f3(a6,f3(f3(a4,a2),a5)),a5)),
% 249.42/249.43 inference(scs_inference,[],[2296,1767,1566,2,3])).
% 249.42/249.43 cnf(2304,plain,
% 249.42/249.43 (~E(f3(a6,f3(f3(a4,a6),a5)),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2271,2])).
% 249.42/249.43 cnf(2305,plain,
% 249.42/249.43 (~E(f3(a1,a2),f3(f3(a4,f3(a5,x23051)),f3(a5,x23052)))),
% 249.42/249.43 inference(scs_inference,[],[21,2271,2233,2,3])).
% 249.42/249.43 cnf(2306,plain,
% 249.42/249.43 (~E(f3(f3(a4,f3(a5,x23061)),f3(a5,x23062)),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2305,2])).
% 249.42/249.43 cnf(2307,plain,
% 249.42/249.43 (~E(f3(f3(a4,a5),f3(a5,a2)),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2300,2305,1650,2,3])).
% 249.42/249.43 cnf(2311,plain,
% 249.42/249.43 (~E(f3(f3(a4,a5),f3(f3(x23111,a6),a2)),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2307,1688,2,3])).
% 249.42/249.43 cnf(2320,plain,
% 249.42/249.43 (~E(f3(f3(a4,a5),f3(a5,x23201)),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2306,2311,1682,2,3])).
% 249.42/249.43 cnf(2324,plain,
% 249.42/249.43 (~E(f3(f3(a4,a5),f3(f3(a5,x23241),x23242)),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2320,1584,2,3])).
% 249.42/249.43 cnf(2327,plain,
% 249.42/249.43 (~E(f3(f3(a4,a5),a5),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2324,1733,2,3])).
% 249.42/249.43 cnf(2331,plain,
% 249.42/249.43 (~E(f3(f3(f3(x23311,x23312),f3(x23313,x23312)),f3(x23311,x23313)),f3(f3(a6,a1),f3(f3(x23314,x23315),x23314)))),
% 249.42/249.43 inference(scs_inference,[],[2327,2253,28,2,3])).
% 249.42/249.43 cnf(2339,plain,
% 249.42/249.43 (~E(f3(f3(a6,a1),f3(a5,x23391)),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2292,2301,1577,2,3])).
% 249.42/249.43 cnf(2343,plain,
% 249.42/249.43 (~E(f3(f3(a6,a1),f3(f3(f3(a5,x23431),x23432),f3(x23433,x23432))),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2339,1610,2,3])).
% 249.42/249.43 cnf(2346,plain,
% 249.42/249.43 (~E(f3(a6,f3(f3(a4,a6),f3(a1,a2))),f3(a1,a2))),
% 249.42/249.43 inference(scs_inference,[],[2304,2191,1652,2,3])).
% 249.42/249.43 cnf(2349,plain,
% 249.42/249.43 (~E(f3(f3(a5,a5),x23491),f3(a4,a1))),
% 249.42/249.43 inference(scs_inference,[],[2346,1831,284,2,3])).
% 249.42/249.43 cnf(2359,plain,
% 249.42/249.43 (~E(a5,f3(a6,f3(f3(x23591,x23592),x23591)))),
% 249.42/249.43 inference(scs_inference,[],[2257,2])).
% 249.42/249.43 cnf(2388,plain,
% 249.42/249.43 (~E(f3(f3(f3(a5,x23881),x23882),x23883),f3(f3(a4,a2),a5))),
% 249.42/249.43 inference(scs_inference,[],[2053,1780,1620,2,3])).
% 249.42/249.43 cnf(2397,plain,
% 249.42/249.43 (~E(f3(f3(f3(a4,a2),f3(f3(a4,a1),x23971)),f3(a5,a6)),a5)),
% 249.42/249.43 inference(scs_inference,[],[2000,1802,207,2,12])).
% 249.42/249.43 cnf(2401,plain,
% 249.42/249.43 (~E(f3(f3(f3(a1,a2),a5),x24011),f3(a4,a1))),
% 249.42/249.43 inference(scs_inference,[],[2349,2000,1802,1638,207,2,12,3])).
% 249.42/249.43 cnf(2404,plain,
% 249.42/249.43 (~E(f3(a4,a1),f3(f3(f3(a1,a2),a5),x24041))),
% 249.42/249.43 inference(scs_inference,[],[2401,2])).
% 249.42/249.43 cnf(2409,plain,
% 249.42/249.43 (~E(f3(f3(f3(x24091,a6),a1),a5),f3(a4,a5))),
% 249.42/249.43 inference(scs_inference,[],[2114,2401,2388,1662,350,2,12,3])).
% 249.42/249.43 cnf(2416,plain,
% 249.42/249.43 (~E(f3(a4,a1),f3(f3(f3(a1,a2),f3(a1,a2)),x24161))),
% 249.42/249.43 inference(scs_inference,[],[2409,2404,2002,1565,207,2,12,3])).
% 249.42/249.43 cnf(2427,plain,
% 249.42/249.43 (~E(f3(f3(f3(a4,f3(a4,a1)),a2),f3(a5,a6)),a5)),
% 249.42/249.43 inference(scs_inference,[],[2416,2006,1933,2397,486,350,10,2,12,3,13])).
% 249.42/249.43 cnf(2436,plain,
% 249.42/249.43 (~E(f3(f3(a4,f3(a4,a1)),f3(a5,a6)),a5)),
% 249.42/249.43 inference(scs_inference,[],[2022,2078,2427,207,9,2,12,13])).
% 249.42/249.43 cnf(2441,plain,
% 249.42/249.43 (~E(a5,f3(f3(a4,f3(a4,a1)),f3(a5,a6)))),
% 249.42/249.43 inference(scs_inference,[],[2436,2])).
% 249.42/249.43 cnf(2453,plain,
% 249.42/249.43 (~E(f3(f3(f3(x24531,x24532),f3(x24533,x24532)),f3(x24531,x24533)),f3(f3(a4,f3(a4,a1)),f3(a5,a6)))),
% 249.42/249.43 inference(scs_inference,[],[28,2441,2071,1948,207,2,12,3])).
% 249.42/249.43 cnf(2465,plain,
% 249.42/249.43 (~E(f3(f3(f3(x24651,x24652),f3(x24653,x24652)),f3(x24651,x24653)),f3(a6,f3(f3(x24654,x24655),x24654)))),
% 249.42/249.43 inference(scs_inference,[],[28,2042,2359,2343,207,2,12,3])).
% 249.42/249.43 cnf(2470,plain,
% 249.42/249.43 (~E(f3(f3(a6,a2),f3(a1,a2)),a5)),
% 249.42/249.43 inference(scs_inference,[],[1538,8,2297,3])).
% 249.42/249.43 cnf(2471,plain,
% 249.42/249.43 (~E(a5,f3(f3(a6,a2),f3(a1,a2)))),
% 249.42/249.43 inference(scs_inference,[],[2470,2])).
% 249.42/249.43 cnf(2472,plain,
% 249.42/249.43 (~E(f3(f3(f3(a6,a2),f3(a1,a2)),a5),a5)),
% 249.42/249.43 inference(scs_inference,[],[2470,8,2,12])).
% 249.42/249.43 cnf(2481,plain,
% 249.42/249.43 (~E(f3(f3(f3(x24811,x24812),f3(x24813,x24812)),f3(x24811,x24813)),f3(f3(a6,a2),f3(a1,a2)))),
% 249.42/249.43 inference(scs_inference,[],[28,2471,2046,2472,207,2,12,3])).
% 249.42/249.43 cnf(2482,plain,
% 249.42/249.43 (~E(f3(f3(a6,a2),f3(a1,a2)),f3(f3(f3(x24821,x24822),f3(x24823,x24822)),f3(x24821,x24823)))),
% 249.42/249.43 inference(scs_inference,[],[2481,2])).
% 249.42/249.43 cnf(2488,plain,
% 249.42/249.43 (~E(f3(x24881,a6),f3(f3(a4,a2),f3(f3(f3(a5,x24882),x24883),f3(x24884,x24883))))),
% 249.42/249.43 inference(scs_inference,[],[864,2])).
% 249.42/249.43 cnf(2501,plain,
% 249.42/249.43 (~E(f3(x25011,a6),f3(f3(a4,a1),f3(f3(f3(a5,x25012),f3(x25013,x25012)),f3(a5,x25013))))),
% 249.42/249.43 inference(scs_inference,[],[1362,2])).
% 249.42/249.43 cnf(2509,plain,
% 249.42/249.43 (~E(f3(x25091,a6),f3(f3(f3(a4,a1),a2),f3(f3(x25092,a6),x25093)))),
% 249.42/249.43 inference(scs_inference,[],[2003,2])).
% 249.42/249.43 cnf(2564,plain,
% 249.42/249.43 (~E(f3(f3(a4,a5),f3(f3(f3(a4,a5),a5),f3(a4,a5))),a5)),
% 249.42/249.43 inference(scs_inference,[],[29,859,1052,2,12])).
% 249.42/249.43 cnf(2580,plain,
% 249.42/249.43 (~E(f3(x25801,a6),f3(a4,f3(f3(f3(a1,x25802),x25803),f3(x25804,x25803))))),
% 249.42/249.43 inference(scs_inference,[],[791,2])).
% 249.42/249.43 cnf(2584,plain,
% 249.42/249.43 (~E(f3(a4,a1),f3(f3(f3(f3(a5,x25841),x25842),f3(x25843,a6)),f3(x25844,a5)))),
% 249.55/249.43 inference(scs_inference,[],[791,1340,2564,1669,9,2,13,3])).
% 249.55/249.43 cnf(2588,plain,
% 249.55/249.43 (~E(f3(a5,x25881),f3(f3(a4,a1),f3(f3(f3(a5,x25882),f3(x25883,x25882)),f3(a5,x25883))))),
% 249.55/249.43 inference(scs_inference,[],[2584,2501,480,2,3])).
% 249.55/249.43 cnf(2615,plain,
% 249.55/249.43 (~E(f3(f3(a5,x26151),x26152),f3(f3(a4,a1),f3(f3(f3(a5,x26153),f3(x26154,x26153)),f3(a5,x26154))))),
% 249.55/249.43 inference(scs_inference,[],[1046,2588,484,2,3])).
% 249.55/249.43 cnf(2623,plain,
% 249.55/249.43 (~E(f3(f3(x26231,x26232),x26231),f3(f3(a4,a2),f3(f3(a4,a1),x26233)))),
% 249.55/249.43 inference(scs_inference,[],[923,2])).
% 249.55/249.43 cnf(2702,plain,
% 249.55/249.43 (~E(f3(f3(x27021,x27022),x27021),f3(f3(a4,a2),f3(f3(a4,x27023),f3(a1,x27023))))),
% 249.55/249.43 inference(scs_inference,[],[696,2])).
% 249.55/249.43 cnf(2706,plain,
% 249.55/249.43 (E(f3(x27061,f3(f3(f3(x27062,x27063),f3(x27064,x27063)),x27062)),f3(x27061,f3(f3(a5,x27065),f3(x27066,x27065))))),
% 249.55/249.43 inference(scs_inference,[],[41,5])).
% 249.55/249.43 cnf(2707,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(x27071,x27072),f3(x27073,x27072)),x27071),x27074),f3(f3(f3(a5,x27075),f3(x27076,x27075)),x27074))),
% 249.55/249.43 inference(scs_inference,[],[41,5,4])).
% 249.55/249.43 cnf(2709,plain,
% 249.55/249.43 (~E(f3(f3(a4,a2),f3(f3(a4,a1),x27091)),f3(f3(x27092,a6),x27093))),
% 249.55/249.43 inference(rename_variables,[],[1403])).
% 249.55/249.43 cnf(2715,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(a5,x27151),x27152),x27153),f3(x27154,x27153)),a4),a5)),
% 249.55/249.43 inference(scs_inference,[],[41,1627,1403,2709,369,357,9,5,4,42,2,3,13])).
% 249.55/249.43 cnf(2727,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x27271),x27272),x27273),f3(f3(x27274,x27272),x27273)),f3(f3(f3(a5,x27271),x27272),f3(x27274,x27272)))),
% 249.55/249.43 inference(scs_inference,[],[369,2])).
% 249.55/249.43 cnf(2732,plain,
% 249.55/249.43 (E(f3(f3(f3(a5,x27321),x27322),f3(x27323,x27322)),f3(f3(f3(a5,x27321),f3(x27323,x27322)),f3(x27322,f3(x27323,x27322))))),
% 249.55/249.43 inference(scs_inference,[],[350,369,2001,2453,2,4,5,86])).
% 249.55/249.43 cnf(2739,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(x27391,x27392),f3(x27393,x27392)),x27394),f3(f3(x27391,x27393),x27394)),a5),a5)),
% 249.55/249.43 inference(scs_inference,[],[22,350,292,377,369,894,2001,2453,2,4,5,86,12,3])).
% 249.55/249.43 cnf(2742,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(f3(x27421,x27422),x27423),f3(f3(x27424,x27422),x27423)),x27425),f3(x27426,x27425)),f3(x27421,x27424)),a5)),
% 249.55/249.43 inference(scs_inference,[],[373,2])).
% 249.55/249.43 cnf(2750,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(x27501,x27502),f3(x27501,x27503)),f3(f3(x27503,x27502),f3(x27501,x27503))),a5),a5)),
% 249.55/249.43 inference(scs_inference,[],[10,377,357,2003,1958,1340,373,2,4,5,12,3])).
% 249.55/249.43 cnf(2753,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x27531),f3(f3(x27532,x27533),x27531)),f3(x27534,x27535)),f3(x27535,f3(x27534,x27535))),f3(f3(f3(f3(a5,x27531),f3(f3(x27532,x27533),x27531)),x27535),f3(x27534,x27535)))),
% 249.55/249.43 inference(scs_inference,[],[90,2])).
% 249.55/249.43 cnf(2758,plain,
% 249.55/249.43 (E(f3(a5,x27581),f3(f3(f3(f3(f3(a5,x27582),x27583),f3(f3(x27581,x27582),x27583)),x27584),f3(x27585,x27584)))),
% 249.55/249.43 inference(scs_inference,[],[207,923,2623,2742,90,2,5,4,12])).
% 249.55/249.43 cnf(2780,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(f3(x27801,x27802),f3(x27803,x27802)),x27804),f3(f3(x27801,x27803),x27804)),x27805),a5),a5)),
% 249.55/249.43 inference(scs_inference,[],[377,181,2715,2481,2000,2,4,5,3])).
% 249.55/249.43 cnf(2791,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x27911),x27912),f3(x27913,x27914)),a5),f3(f3(a5,x27911),x27912))),
% 249.55/249.43 inference(scs_inference,[],[377,248,2750,2482,2488,2,5,4,3])).
% 249.55/249.43 cnf(2802,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(f3(x28021,x28022),f3(x28023,x28022)),f3(x28021,x28023)))),
% 249.55/249.43 inference(scs_inference,[],[6,28,2739,2096,2509,2,4,5,3])).
% 249.55/249.43 cnf(2812,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(x28121,x28122),f3(x28123,x28122)),f3(x28121,x28123)),f3(f3(f3(x28124,x28125),f3(x28126,x28125)),f3(x28124,x28126))),f3(a5,a5))),
% 249.55/249.43 inference(scs_inference,[],[378,372,2780,2580,2126,2,4,5,3])).
% 249.55/249.43 cnf(2816,plain,
% 249.55/249.43 (~E(f3(a4,a2),f3(f3(f3(f3(a4,a1),x28161),f3(x28162,x28161)),x28163))),
% 249.55/249.43 inference(scs_inference,[],[2812,846,2,4])).
% 249.55/249.43 cnf(2820,plain,
% 249.55/249.43 (E(f3(f3(f3(a5,x28201),f3(x28202,x28203)),a5),f3(f3(a5,x28204),x28205))),
% 249.55/249.43 inference(scs_inference,[],[377,490,2046,2812,846,2,4,5,3])).
% 249.55/249.43 cnf(2847,plain,
% 249.55/249.43 (E(a5,f3(f3(x28471,a6),x28472))),
% 249.55/249.43 inference(scs_inference,[],[15,340,2802,2127,2,4,3])).
% 249.55/249.43 cnf(2851,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(a5,x28511),x28512),f3(f3(x28513,x28511),x28512)),x28514),f3(x28515,x28514)),f3(a5,x28513))),
% 249.55/249.43 inference(scs_inference,[],[2758,789,4,2])).
% 249.55/249.43 cnf(2856,plain,
% 249.55/249.43 (E(f3(f3(a5,x28561),f3(f3(f3(x28562,x28563),f3(x28564,x28563)),f3(x28562,x28564))),f3(f3(f3(x28565,a6),x28561),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1662,2791,1502,2,4,3])).
% 249.55/249.43 cnf(2862,plain,
% 249.55/249.43 (E(f3(f3(a5,x28621),f3(f3(f3(x28622,x28623),f3(x28624,x28623)),f3(x28622,x28624))),f3(f3(f3(f3(a5,x28621),a5),x28625),f3(x28626,x28625)))),
% 249.55/249.43 inference(scs_inference,[],[378,239,2820,989,4,2,3])).
% 249.55/249.43 cnf(2865,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x28651),a5),x28652),f3(x28653,x28652)),f3(f3(a5,x28651),f3(f3(f3(x28654,x28655),f3(x28656,x28655)),f3(x28654,x28656))))),
% 249.55/249.43 inference(scs_inference,[],[2862,2])).
% 249.55/249.43 cnf(2868,plain,
% 249.55/249.43 (E(f3(f3(a5,x28681),f3(f3(f3(x28682,x28683),f3(x28684,x28683)),f3(x28682,x28684))),f3(f3(a5,a5),f3(x28681,a5)))),
% 249.55/249.43 inference(scs_inference,[],[378,232,2862,745,2,4,3])).
% 249.55/249.43 cnf(2874,plain,
% 249.55/249.43 (E(f3(f3(a5,f3(x28741,x28742)),a5),f3(f3(a5,f3(f3(x28741,x28743),f3(x28742,x28743))),f3(x28741,x28742)))),
% 249.55/249.43 inference(scs_inference,[],[377,284,2868,2816,4,2,3])).
% 249.55/249.43 cnf(2880,plain,
% 249.55/249.43 (E(a5,f3(f3(f3(f3(a5,x28801),f3(x28802,x28801)),x28803),f3(x28804,x28803)))),
% 249.55/249.43 inference(scs_inference,[],[15,258,2874,2331,2,4,3])).
% 249.55/249.43 cnf(2889,plain,
% 249.55/249.43 (E(f3(f3(a1,a2),f3(f3(f3(x28891,x28892),f3(x28893,x28892)),f3(x28891,x28893))),f3(a5,a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1538,2880,2702,2,4,3])).
% 249.55/249.43 cnf(2894,plain,
% 249.55/249.43 (E(f3(a5,a5),f3(f3(a1,a2),f3(f3(f3(x28941,x28942),f3(x28943,x28942)),f3(x28941,x28943))))),
% 249.55/249.43 inference(scs_inference,[],[2889,2615,4,2])).
% 249.55/249.43 cnf(2895,plain,
% 249.55/249.43 (E(a5,f3(f3(a1,a2),x28951))),
% 249.55/249.43 inference(scs_inference,[],[15,1629,2889,2615,4,2,3])).
% 249.55/249.43 cnf(2900,plain,
% 249.55/249.43 (E(f3(f3(a1,a2),x29001),a5)),
% 249.55/249.43 inference(scs_inference,[],[2895,2465,4,2])).
% 249.55/249.43 cnf(2901,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(a1,x29011),f3(a2,x29011)))),
% 249.55/249.43 inference(scs_inference,[],[2895,2465,4,2,42])).
% 249.55/249.43 cnf(2938,plain,
% 249.55/249.43 (E(f3(f3(f3(a1,a2),x29381),f3(f3(f3(x29382,x29383),f3(x29384,x29383)),f3(x29382,x29384))),f3(f3(a5,x29381),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1554,2901,2,3])).
% 249.55/249.43 cnf(2942,plain,
% 249.55/249.43 (E(f3(f3(x29421,f3(a1,a2)),f3(f3(f3(x29422,x29423),f3(x29424,x29423)),f3(x29422,x29424))),f3(f3(x29421,a5),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1565,2938,2,3])).
% 249.55/249.43 cnf(2946,plain,
% 249.55/249.43 (E(f3(f3(x29461,f3(x29462,a6)),f3(f3(f3(x29463,x29464),f3(x29465,x29464)),f3(x29463,x29465))),f3(f3(x29461,a5),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1650,2942,2,3])).
% 249.55/249.43 cnf(2954,plain,
% 249.55/249.43 (E(f3(f3(f3(x29541,a6),x29542),f3(f3(f3(x29543,x29544),f3(x29545,x29544)),f3(x29543,x29545))),f3(f3(a5,x29542),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1698,2946,2,3])).
% 249.55/249.43 cnf(2963,plain,
% 249.55/249.43 (E(f3(f3(a5,x29631),f3(f3(f3(x29632,x29633),f3(x29634,x29633)),f3(x29632,x29634))),f3(f3(f3(f3(a5,x29635),x29636),f3(x29637,x29636)),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1609,2954,2,3])).
% 249.55/249.43 cnf(2970,plain,
% 249.55/249.43 (E(f3(f3(x29701,a6),x29702),a5)),
% 249.55/249.43 inference(scs_inference,[],[2847,2])).
% 249.55/249.43 cnf(2971,plain,
% 249.55/249.43 (E(f3(x29711,a6),f3(f3(x29711,x29712),f3(a6,x29712)))),
% 249.55/249.43 inference(scs_inference,[],[2847,2,42])).
% 249.55/249.43 cnf(2979,plain,
% 249.55/249.43 (E(f3(f3(x29791,x29792),a6),f3(f3(x29791,a6),f3(x29792,a6)))),
% 249.55/249.43 inference(scs_inference,[],[2971,2970,2,86])).
% 249.55/249.43 cnf(2988,plain,
% 249.55/249.43 (E(f3(f3(x29881,a6),f3(x29882,a6)),f3(f3(x29881,x29882),a6))),
% 249.55/249.43 inference(scs_inference,[],[2979,2])).
% 249.55/249.43 cnf(2989,plain,
% 249.55/249.43 (E(f3(x29891,f3(f3(f3(x29892,x29893),f3(x29894,x29893)),f3(x29892,x29894))),f3(x29891,f3(f3(x29895,x29896),x29895)))),
% 249.55/249.43 inference(scs_inference,[],[378,1600,2979,2,3])).
% 249.55/249.43 cnf(3003,plain,
% 249.55/249.43 (E(f3(x30031,f3(f3(f3(x30032,x30033),f3(x30034,x30033)),f3(x30032,x30034))),f3(x30031,f3(f3(a1,x30035),a2)))),
% 249.55/249.43 inference(scs_inference,[],[378,1680,2989,2,3])).
% 249.55/249.43 cnf(3006,plain,
% 249.55/249.43 (E(f3(x30061,f3(f3(f3(x30062,x30063),f3(x30064,x30063)),f3(x30062,x30064))),f3(x30061,f3(a1,a2)))),
% 249.55/249.43 inference(scs_inference,[],[378,1630,2706,2,3])).
% 249.55/249.43 cnf(3009,plain,
% 249.55/249.43 (E(f3(x30091,f3(f3(f3(x30092,x30093),f3(x30094,x30093)),f3(x30092,x30094))),f3(x30091,f3(x30095,a6)))),
% 249.55/249.43 inference(scs_inference,[],[378,1660,3006,2,3])).
% 249.55/249.43 cnf(3012,plain,
% 249.55/249.43 (E(f3(f3(x30121,a5),f3(f3(f3(x30122,x30123),f3(x30124,x30123)),f3(x30122,x30124))),f3(f3(x30121,f3(a1,a2)),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1643,3009,2,3])).
% 249.55/249.43 cnf(3016,plain,
% 249.55/249.43 (E(f3(f3(x30161,a5),f3(f3(f3(x30162,x30163),f3(x30164,x30163)),f3(x30162,x30164))),f3(f3(x30161,f3(x30165,a6)),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1671,2707,2,3])).
% 249.55/249.43 cnf(3024,plain,
% 249.55/249.43 (E(f3(f3(f3(a5,x30241),f3(x30242,x30243)),f3(x30243,f3(x30242,x30243))),f3(f3(f3(a5,x30241),x30243),f3(x30242,x30243)))),
% 249.55/249.43 inference(scs_inference,[],[2732,2])).
% 249.55/249.43 cnf(3029,plain,
% 249.55/249.43 (E(f3(a5,f3(f3(f3(x30291,x30292),f3(x30293,x30292)),f3(x30291,x30293))),f3(f3(f3(x30294,x30295),x30294),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1599,3003,2,3])).
% 249.55/249.43 cnf(3041,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(x30411,x30412),f3(x30411,x30413)),f3(f3(x30413,x30412),f3(x30411,x30413))),f3(f3(f3(x30414,x30415),f3(x30416,x30415)),f3(x30414,x30416))),a5)),
% 249.55/249.43 inference(scs_inference,[],[378,2750,3012,2,3])).
% 249.55/249.43 cnf(3046,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(x30461,x30462),f3(x30461,x30463)),f3(f3(x30463,x30462),f3(x30461,x30463))),f3(f3(x30461,x30462),f3(x30463,x30462))),f3(f3(f3(x30461,x30462),f3(x30461,x30463)),f3(f3(x30463,x30462),f3(x30461,x30463))))),
% 249.55/249.43 inference(scs_inference,[],[9,378,2739,2963,3041,2,3,12])).
% 249.55/249.43 cnf(3054,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x30541),f3(x30542,x30541)),f3(x30543,x30544)),a5),f3(a5,x30542))),
% 249.55/249.43 inference(scs_inference,[],[377,272,3046,2,3])).
% 249.55/249.43 cnf(3058,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(f3(x30581,f3(x30582,x30583)),f3(x30583,f3(x30582,x30583))),f3(x30581,x30582)))),
% 249.55/249.43 inference(scs_inference,[],[6,325,3054,2,3])).
% 249.55/249.43 cnf(3060,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(f3(f3(x30601,x30602),f3(x30603,x30602)),x30604),f3(x30601,x30603)))),
% 249.55/249.43 inference(scs_inference,[],[6,190,3058,2,3])).
% 249.55/249.43 cnf(3062,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(f3(f3(a5,x30621),x30622),x30623),f3(a4,a1)))),
% 249.55/249.43 inference(scs_inference,[],[6,298,3060,2,3])).
% 249.55/249.43 cnf(3064,plain,
% 249.55/249.43 (E(f3(f3(a5,x30641),f3(f3(f3(x30642,x30643),f3(x30644,x30643)),f3(x30642,x30644))),f3(f3(f3(f3(a5,x30641),x30645),f3(a5,x30645)),x30646))),
% 249.55/249.43 inference(scs_inference,[],[378,249,3062,2,3])).
% 249.55/249.43 cnf(3068,plain,
% 249.55/249.43 (E(f3(f3(a5,x30681),f3(f3(f3(x30682,x30683),f3(x30684,x30683)),f3(x30682,x30684))),f3(f3(f3(a5,x30681),a5),x30685))),
% 249.55/249.43 inference(scs_inference,[],[378,238,3064,2,3])).
% 249.55/249.43 cnf(3072,plain,
% 249.55/249.43 (E(f3(a5,f3(f3(f3(x30721,x30722),f3(x30723,x30722)),f3(x30721,x30723))),f3(f3(f3(f3(x30724,x30725),f3(x30726,x30725)),f3(x30724,x30726)),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,371,3068,2,3])).
% 249.55/249.43 cnf(3077,plain,
% 249.55/249.43 (E(f3(a5,f3(f3(f3(x30771,x30772),f3(x30773,x30772)),f3(x30771,x30773))),f3(f3(f3(a5,x30774),f3(a5,x30774)),x30775))),
% 249.55/249.43 inference(scs_inference,[],[378,306,2856,2,3])).
% 249.55/249.43 cnf(3081,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(f3(f3(a5,x30811),x30812),f3(x30813,x30812)),x30814))),
% 249.55/249.43 inference(scs_inference,[],[6,356,3077,2,3])).
% 249.55/249.43 cnf(3083,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(f3(f3(a1,x30831),x30832),f3(x30833,x30832)),a2))),
% 249.55/249.43 inference(scs_inference,[],[6,349,3081,2,3])).
% 249.55/249.43 cnf(3085,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(f3(a1,x30851),x30852),a2))),
% 249.55/249.43 inference(scs_inference,[],[6,206,3083,2,3])).
% 249.55/249.43 cnf(3087,plain,
% 249.55/249.43 (E(f3(f3(a5,f3(x30871,x30872)),a5),f3(f3(f3(x30873,x30874),f3(x30875,x30874)),x30873))),
% 249.55/249.43 inference(scs_inference,[],[377,44,3085,2,3])).
% 249.55/249.43 cnf(3091,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(f3(x30911,x30912),f3(x30913,x30912)),f3(f3(x30911,x30913),x30912)))),
% 249.55/249.43 inference(scs_inference,[],[6,132,3087,2,3])).
% 249.55/249.43 cnf(3093,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(f3(x30931,x30932),f3(x30933,x30932)),x30931))),
% 249.55/249.43 inference(scs_inference,[],[6,128,3091,2,3])).
% 249.55/249.43 cnf(3095,plain,
% 249.55/249.43 (E(f3(f3(f3(a5,x30951),f3(x30952,x30953)),a5),f3(a5,x30954))),
% 249.55/249.43 inference(scs_inference,[],[377,577,3093,2,3])).
% 249.55/249.43 cnf(3099,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(x30991,x30992),x30991))),
% 249.55/249.43 inference(scs_inference,[],[6,135,3095,2,3])).
% 249.55/249.43 cnf(3101,plain,
% 249.55/249.43 (E(f3(f3(f3(a1,x31011),a2),f3(f3(f3(x31012,x31013),f3(x31014,x31013)),f3(x31012,x31014))),f3(a5,a5))),
% 249.55/249.43 inference(scs_inference,[],[378,1726,3099,2,3])).
% 249.55/249.43 cnf(3105,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x31051),f3(x31052,x31051)),f3(x31053,x31054)),f3(f3(f3(x31055,x31056),f3(x31057,x31056)),f3(x31055,x31057))),f3(a5,x31052))),
% 249.55/249.43 inference(scs_inference,[],[378,3054,3101,2,3])).
% 249.55/249.43 cnf(3108,plain,
% 249.55/249.43 (E(f3(f3(f3(a5,x31081),f3(x31082,x31083)),f3(f3(f3(x31084,x31085),f3(x31086,x31085)),f3(x31084,x31086))),f3(a5,x31087))),
% 249.55/249.43 inference(scs_inference,[],[378,3095,3105,2,3])).
% 249.55/249.43 cnf(3111,plain,
% 249.55/249.43 (E(a5,f3(f3(a1,x31111),f3(a2,x31111)))),
% 249.55/249.43 inference(scs_inference,[],[21,2901,3108,2,3])).
% 249.55/249.43 cnf(3113,plain,
% 249.55/249.43 (E(f3(a5,f3(f3(f3(x31131,x31132),f3(x31133,x31132)),f3(x31131,x31133))),f3(f3(f3(f3(f3(a5,x31134),x31135),f3(f3(a5,x31134),x31135)),x31136),f3(x31137,x31136)))),
% 249.55/249.43 inference(scs_inference,[],[378,2758,3111,2,3])).
% 249.55/249.43 cnf(3116,plain,
% 249.55/249.43 (E(f3(a2,a6),f3(a1,a6))),
% 249.55/249.43 inference(scs_inference,[],[378,2758,2970,3111,2,3,12])).
% 249.55/249.43 cnf(3120,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x31201),x31202),f3(x31203,x31204)),f3(f3(f3(x31205,x31206),f3(x31207,x31206)),f3(x31205,x31207))),f3(f3(a5,x31201),x31202))),
% 249.55/249.43 inference(scs_inference,[],[378,2791,3116,2,3])).
% 249.55/249.43 cnf(3124,plain,
% 249.55/249.43 (E(f3(f3(f3(a5,x31241),f3(x31242,x31243)),f3(f3(f3(x31244,x31245),f3(x31246,x31245)),f3(x31244,x31246))),f3(f3(a5,x31247),x31248))),
% 249.55/249.43 inference(scs_inference,[],[378,2820,3120,2,3])).
% 249.55/249.43 cnf(3127,plain,
% 249.55/249.43 (E(f3(f3(a5,f3(x31271,x31272)),f3(f3(f3(x31273,x31274),f3(x31275,x31274)),f3(x31273,x31275))),f3(f3(a5,f3(f3(x31271,x31276),f3(x31272,x31276))),f3(x31271,x31272)))),
% 249.55/249.43 inference(scs_inference,[],[378,2874,3124,2,3])).
% 249.55/249.43 cnf(3130,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x31301),a6),x31302),f3(x31303,x31302)),f3(f3(a5,a6),f3(x31301,a6)))),
% 249.55/249.43 inference(scs_inference,[],[248,2979,3127,2,3])).
% 249.55/249.43 cnf(3133,plain,
% 249.55/249.43 (E(f3(f3(a5,a6),f3(x31331,a6)),f3(f3(f3(f3(a5,x31331),a6),x31332),f3(x31333,x31332)))),
% 249.55/249.43 inference(scs_inference,[],[3130,2])).
% 249.55/249.43 cnf(3140,plain,
% 249.55/249.43 (E(f3(a1,a2),f3(f3(a1,a2),x31401))),
% 249.55/249.43 inference(scs_inference,[],[6,2895,3113,2,3])).
% 249.55/249.43 cnf(3142,plain,
% 249.55/249.43 (E(a5,f3(f3(f3(f3(f3(a5,x31421),x31422),f3(f3(a5,x31421),x31422)),x31423),f3(x31424,x31423)))),
% 249.55/249.43 inference(scs_inference,[],[15,3113,3140,2,3])).
% 249.55/249.43 cnf(3153,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(a5,x31531),x31532),f3(f3(a5,x31531),x31532)),x31533),f3(x31534,x31533)),a5)),
% 249.55/249.43 inference(scs_inference,[],[3142,2])).
% 249.55/249.43 cnf(3206,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(a5,x32061),x32062),f3(f3(x32063,x32061),x32062)),f3(x32064,x32065)),a5),f3(a5,x32063))),
% 249.55/249.43 inference(scs_inference,[],[377,2851,3016,2,3])).
% 249.55/249.43 cnf(3210,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(a5,x32101),x32102),f3(f3(x32103,x32101),x32102)),f3(x32104,x32105)),f3(f3(f3(x32106,x32107),f3(x32108,x32107)),f3(x32106,x32108))),f3(a5,x32103))),
% 249.55/249.43 inference(scs_inference,[],[378,3206,2,3])).
% 249.55/249.43 cnf(3213,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x32131),f3(f3(x32132,x32133),x32131)),f3(x32134,a5)),a5),f3(f3(f3(f3(a5,x32131),f3(f3(x32132,x32133),x32131)),a5),f3(x32134,a5)))),
% 249.55/249.43 inference(scs_inference,[],[367,3210,2753,2,3])).
% 249.55/249.43 cnf(3217,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x32171),f3(x32172,x32173)),f3(x32174,x32172)),a5),f3(f3(f3(a5,x32171),f3(x32172,x32173)),f3(f3(x32174,x32173),f3(x32172,x32173))))),
% 249.55/249.43 inference(scs_inference,[],[377,2727,3213,2,3])).
% 249.55/249.43 cnf(3222,plain,
% 249.55/249.43 (E(f3(f3(f3(a5,x32221),f3(x32222,a5)),a5),f3(f3(f3(a5,x32221),a5),f3(x32222,a5)))),
% 249.55/249.43 inference(scs_inference,[],[367,3024,3217,2,3])).
% 249.55/249.43 cnf(3226,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x32261),f3(x32262,x32263)),f3(x32264,x32262)),f3(f3(f3(x32265,x32266),f3(x32267,x32266)),f3(x32265,x32267))),f3(f3(f3(a5,x32261),f3(x32262,x32263)),f3(f3(x32264,x32263),f3(x32262,x32263))))),
% 249.55/249.43 inference(scs_inference,[],[378,3217,3222,2,3])).
% 249.55/249.43 cnf(3229,plain,
% 249.55/249.43 (E(f3(f3(f3(a5,x32291),f3(x32292,a5)),f3(f3(f3(x32293,x32294),f3(x32295,x32294)),f3(x32293,x32295))),f3(f3(f3(a5,x32291),a5),f3(x32292,a5)))),
% 249.55/249.43 inference(scs_inference,[],[378,3222,3226,2,3])).
% 249.55/249.43 cnf(3232,plain,
% 249.55/249.43 (E(f3(f3(a5,a6),a5),f3(f3(f3(f3(a5,a5),a6),x32321),f3(x32322,x32321)))),
% 249.55/249.43 inference(scs_inference,[],[367,3133,3229,2,3])).
% 249.55/249.43 cnf(3235,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,a5),a6),x32351),f3(x32352,x32351)),f3(f3(a5,a6),a5))),
% 249.55/249.43 inference(scs_inference,[],[3232,2])).
% 249.55/249.43 cnf(3236,plain,
% 249.55/249.43 (E(f3(f3(a5,a6),f3(f3(f3(x32361,x32362),f3(x32363,x32362)),f3(x32361,x32363))),f3(f3(f3(f3(a5,a5),a6),x32364),f3(x32365,x32364)))),
% 249.55/249.43 inference(scs_inference,[],[378,3232,2,3])).
% 249.55/249.43 cnf(3239,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,a5),a6),f3(x32391,x32392)),a5),f3(f3(a5,a6),a5))),
% 249.55/249.43 inference(scs_inference,[],[377,3236,3235,2,3])).
% 249.55/249.43 cnf(3243,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,a5),a6),f3(x32431,x32432)),f3(f3(f3(x32433,x32434),f3(x32435,x32434)),f3(x32433,x32435))),f3(f3(a5,a6),a5))),
% 249.55/249.43 inference(scs_inference,[],[378,3239,2,3])).
% 249.55/249.43 cnf(3246,plain,
% 249.55/249.43 (E(f3(f3(x32461,a6),a5),f3(f3(x32461,a5),a6))),
% 249.55/249.43 inference(scs_inference,[],[367,3243,2988,2,3])).
% 249.55/249.43 cnf(3250,plain,
% 249.55/249.43 (E(f3(f3(x32501,a6),f3(f3(f3(x32502,x32503),f3(x32504,x32503)),f3(x32502,x32504))),f3(f3(x32501,a5),a6))),
% 249.55/249.43 inference(scs_inference,[],[378,3246,2,3])).
% 249.55/249.43 cnf(3253,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(a5,x32531),x32532),f3(f3(a5,x32531),x32532)),f3(x32533,x32534)),a5),a5)),
% 249.55/249.43 inference(scs_inference,[],[377,3250,3153,2,3])).
% 249.55/249.43 cnf(3267,plain,
% 249.55/249.43 (E(f3(a5,f3(f3(f3(x32671,x32672),f3(x32673,x32672)),f3(x32671,x32673))),f3(f3(a1,a2),f3(f3(f3(x32674,x32675),f3(x32676,x32675)),f3(x32674,x32676))))),
% 249.55/249.43 inference(scs_inference,[],[378,2894,3072,2,3])).
% 249.55/249.43 cnf(3270,plain,
% 249.55/249.43 (E(a5,f3(f3(f3(f3(x32701,x32702),f3(x32703,x32702)),f3(x32701,x32703)),a5))),
% 249.55/249.43 inference(scs_inference,[],[15,3072,3267,2,3])).
% 249.55/249.43 cnf(3274,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(a5,x32741),a5),f3(x32742,x32743)),a5),f3(f3(a5,x32741),f3(f3(f3(x32744,x32745),f3(x32746,x32745)),f3(x32744,x32746))))),
% 249.55/249.43 inference(scs_inference,[],[377,2865,3029,2,3])).
% 249.55/249.43 cnf(3278,plain,
% 249.55/249.43 (E(a5,f3(f3(f3(x32781,x32782),x32781),a5))),
% 249.55/249.43 inference(scs_inference,[],[15,3029,3274,2,3])).
% 249.55/249.43 cnf(3351,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(a5,x33511),x33512),f3(f3(a5,x33511),x33512)),f3(x33513,x33514)),x33515),a5)),
% 249.55/249.43 inference(scs_inference,[],[8,3253,1229,42,13])).
% 249.55/249.43 cnf(3382,plain,
% 249.55/249.43 (~E(f3(f3(a4,a5),f3(f3(f3(f3(a5,x33821),x33822),f3(f3(a5,x33821),x33822)),f3(a5,a5))),a5)),
% 249.55/249.43 inference(scs_inference,[],[9,1044,3351,3041,535,42,13,12])).
% 249.55/249.43 cnf(3404,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(x34041,x34042),f3(x34041,x34043)),f3(f3(x34043,x34042),f3(x34041,x34043))),x34044),a5)),
% 249.55/249.43 inference(scs_inference,[],[8,2750,13])).
% 249.55/249.43 cnf(3903,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(x39031,x39032),f3(x39033,x39032)),f3(x39031,x39033)),a5),a5)),
% 249.55/249.43 inference(scs_inference,[],[3270,2])).
% 249.55/249.43 cnf(3913,plain,
% 249.55/249.43 (E(f3(f3(f3(x39131,x39132),x39131),a5),a5)),
% 249.55/249.43 inference(scs_inference,[],[3278,2])).
% 249.55/249.43 cnf(3919,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(x39191,x39192),f3(x39193,x39192)),f3(x39191,x39193)),x39194),a5)),
% 249.55/249.43 inference(scs_inference,[],[2085,3903,3278,2900,8,2,5,4,12,13])).
% 249.55/249.43 cnf(3924,plain,
% 249.55/249.43 (E(a5,f3(f3(f3(f3(x39241,x39242),f3(x39243,x39242)),f3(x39241,x39243)),x39244))),
% 249.55/249.43 inference(scs_inference,[],[3919,2])).
% 249.55/249.43 cnf(3926,plain,
% 249.55/249.43 (E(f3(f3(f3(f3(f3(x39261,x39262),f3(x39263,x39262)),f3(x39261,x39263)),x39264),x39265),f3(a5,x39265))),
% 249.55/249.43 inference(scs_inference,[],[3919,2,5,4])).
% 249.55/249.43 cnf(3938,plain,
% 249.55/249.43 (E(f3(f3(f3(x39381,x39382),x39381),x39383),a5)),
% 249.55/249.43 inference(scs_inference,[],[2077,3924,3913,3351,2900,8,2,5,4,12,13])).
% 249.55/249.43 cnf(4482,plain,
% 249.55/249.43 ($false),
% 249.55/249.43 inference(scs_inference,[],[1179,2133,3382,3926,3404,3938,7,5,4,2,13,12]),
% 249.55/249.43 ['proof']).
% 249.55/249.43 % SZS output end Proof
% 249.55/249.43 % Total time :248.790000s
%------------------------------------------------------------------------------