%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP139-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:39:00 EDT 2024
% Result : Unsatisfiable 281.52s 282.15s
% Output : CNFRefutation 281.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP139-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n018.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu Jun 20 09:40:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 281.52/282.14 %-------------------------------------------
% 281.52/282.14 % File :CSE---1.7
% 281.52/282.14 % Problem :theBenchmark
% 281.52/282.14 % Transform :cnf
% 281.52/282.14 % Format :tptp:raw
% 281.52/282.14 % Command :java -jar mcs_scs.jar %d %s
% 281.52/282.14
% 281.52/282.14 % Result :Theorem 280.880000s
% 281.52/282.14 % Output :CNFRefutation 280.880000s
% 281.52/282.14 %-------------------------------------------
% 281.52/282.15 %--------------------------------------------------------------------------
% 281.52/282.15 % File : GRP139-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 281.52/282.15 % Domain : Group Theory (Lattice Ordered)
% 281.52/282.15 % Problem : Prove greatest lower-bound axiom using the GLB transformation
% 281.52/282.15 % Version : [Fuc94] (equality) axioms.
% 281.52/282.15 % English : This problem proves the original axiom of anti-symmetry from
% 281.52/282.15 % the equational axiomatization.
% 281.52/282.15
% 281.52/282.15 % Refs : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri
% 281.52/282.15 % : [Sch95] Schulz (1995), Explanation Based Learning for Distribu
% 281.52/282.15 % Source : [Sch95]
% 281.52/282.15 % Names : ax_glb1b [Sch95]
% 281.52/282.15
% 281.52/282.15 % Status : Unsatisfiable
% 281.52/282.15 % Rating : 0.00 v8.1.0, 0.05 v7.5.0, 0.04 v7.4.0, 0.09 v7.3.0, 0.05 v7.1.0, 0.06 v7.0.0, 0.11 v6.3.0, 0.18 v6.2.0, 0.21 v6.1.0, 0.06 v6.0.0, 0.10 v5.5.0, 0.05 v5.4.0, 0.00 v5.1.0, 0.07 v4.1.0, 0.09 v4.0.1, 0.07 v4.0.0, 0.08 v3.7.0, 0.00 v3.4.0, 0.12 v3.3.0, 0.00 v2.0.0
% 281.52/282.15 % Syntax : Number of clauses : 18 ( 18 unt; 0 nHn; 3 RR)
% 281.52/282.15 % Number of literals : 18 ( 18 equ; 1 neg)
% 281.52/282.15 % Maximal clause size : 1 ( 1 avg)
% 281.52/282.15 % Maximal term depth : 3 ( 2 avg)
% 281.52/282.15 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 281.52/282.15 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 281.52/282.15 % Number of variables : 33 ( 2 sgn)
% 281.52/282.15 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 281.52/282.15
% 281.52/282.15 % Comments : ORDERING LPO inverse > product > greatest_lower_bound >
% 281.52/282.15 % least_upper_bound > identity > a > b > c
% 281.52/282.15 % : ORDERING LPO greatest_lower_bound > least_upper_bound >
% 281.52/282.15 % inverse > product > identity > a > b > c
% 281.52/282.15 % Bugfixes : v1.2.1 - Duplicate axioms in GRP004-2.ax removed.
% 281.52/282.15 %--------------------------------------------------------------------------
% 281.52/282.15 %----Include equality group theory axioms
% 281.52/282.15 include('Axioms/GRP004-0.ax').
% 281.52/282.15 %----Include Lattice ordered group (equality) axioms
% 281.52/282.15 include('Axioms/GRP004-2.ax').
% 281.52/282.15 %--------------------------------------------------------------------------
% 281.52/282.15 cnf(ax_glb1b_1_1,hypothesis,
% 281.52/282.15 greatest_lower_bound(a,c) = c ).
% 281.52/282.15
% 281.52/282.15 cnf(ax_glb1b_2_2,hypothesis,
% 281.52/282.15 greatest_lower_bound(b,c) = c ).
% 281.52/282.15
% 281.52/282.15 cnf(prove_ax_glb1b,negated_conjecture,
% 281.52/282.15 greatest_lower_bound(greatest_lower_bound(a,b),c) != c ).
% 281.52/282.15
% 281.52/282.15 %--------------------------------------------------------------------------
% 281.52/282.15 %-------------------------------------------
% 281.52/282.15 % Proof found
% 281.52/282.15 % SZS status Theorem for theBenchmark
% 281.52/282.15 % SZS output start Proof
% 281.52/282.16 %ClaNum:28(EqnAxiom:10)
% 281.52/282.16 %VarNum:72(SingletonVarNum:33)
% 281.52/282.16 %MaxLitNum:1
% 281.52/282.16 %MaxfuncDepth:2
% 281.52/282.16 %SharedTerms:11
% 281.52/282.16 %goalClause: 28
% 281.52/282.16 %singleGoalClaCount:1
% 281.52/282.16 [11]E(f4(a1,a2),a2)
% 281.52/282.16 [12]E(f4(a3,a2),a2)
% 281.52/282.16 [28]~E(f4(f4(a1,a3),a2),a2)
% 281.52/282.16 [13]E(f6(a5,x131),x131)
% 281.52/282.16 [14]E(f4(x141,x141),x141)
% 281.52/282.16 [15]E(f7(x151,x151),x151)
% 281.52/282.16 [16]E(f6(f8(x161),x161),a5)
% 281.52/282.16 [17]E(f4(x171,x172),f4(x172,x171))
% 281.52/282.16 [18]E(f7(x181,x182),f7(x182,x181))
% 281.52/282.16 [19]E(f4(x191,f7(x191,x192)),x191)
% 281.52/282.16 [20]E(f7(x201,f4(x201,x202)),x201)
% 281.52/282.16 [21]E(f4(f4(x211,x212),x213),f4(x211,f4(x212,x213)))
% 281.52/282.16 [22]E(f7(f7(x221,x222),x223),f7(x221,f7(x222,x223)))
% 281.52/282.16 [23]E(f6(f6(x231,x232),x233),f6(x231,f6(x232,x233)))
% 281.52/282.16 [24]E(f4(f6(x241,x242),f6(x241,x243)),f6(x241,f4(x242,x243)))
% 281.52/282.16 [25]E(f7(f6(x251,x252),f6(x251,x253)),f6(x251,f7(x252,x253)))
% 281.52/282.16 [26]E(f4(f6(x261,x262),f6(x263,x262)),f6(f4(x261,x263),x262))
% 281.52/282.16 [27]E(f7(f6(x271,x272),f6(x273,x272)),f6(f7(x271,x273),x272))
% 281.52/282.16 %EqnAxiom
% 281.52/282.16 [1]E(x11,x11)
% 281.52/282.16 [2]E(x22,x21)+~E(x21,x22)
% 281.52/282.16 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 281.52/282.16 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43))
% 281.52/282.16 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52))
% 281.52/282.16 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 281.52/282.16 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 281.52/282.16 [8]~E(x81,x82)+E(f7(x81,x83),f7(x82,x83))
% 281.52/282.16 [9]~E(x91,x92)+E(f7(x93,x91),f7(x93,x92))
% 281.52/282.16 [10]~E(x101,x102)+E(f8(x101),f8(x102))
% 281.52/282.16
% 281.52/282.16 %-------------------------------------------
% 281.52/282.17 cnf(29,plain,
% 281.52/282.17 (E(x291,f4(x291,x291))),
% 281.52/282.17 inference(scs_inference,[],[14,2])).
% 281.52/282.17 cnf(32,plain,
% 281.52/282.17 (~E(f4(a1,a3),a2)),
% 281.52/282.17 inference(scs_inference,[],[28,14,2,3,4])).
% 281.52/282.17 cnf(33,plain,
% 281.52/282.17 (E(x331,f7(x331,x331))),
% 281.52/282.17 inference(scs_inference,[],[15,2])).
% 281.52/282.17 cnf(34,plain,
% 281.52/282.17 (~E(f4(f4(a1,a3),a2),f7(a2,a2))),
% 281.52/282.17 inference(scs_inference,[],[28,15,2,3])).
% 281.52/282.17 cnf(36,plain,
% 281.52/282.17 (E(x361,f6(a5,x361))),
% 281.52/282.17 inference(scs_inference,[],[13,2])).
% 281.52/282.17 cnf(37,plain,
% 281.52/282.17 (~E(f4(f4(a1,a3),a2),f6(a5,a2))),
% 281.52/282.17 inference(scs_inference,[],[28,13,2,3])).
% 281.52/282.17 cnf(39,plain,
% 281.52/282.17 (E(f6(x391,f4(x392,x393)),f4(f6(x391,x392),f6(x391,x393)))),
% 281.52/282.17 inference(scs_inference,[],[24,2])).
% 281.52/282.17 cnf(40,plain,
% 281.52/282.17 (E(f6(x401,x402),f6(x401,f4(x402,x402)))),
% 281.52/282.17 inference(scs_inference,[],[29,24,2,3])).
% 281.52/282.17 cnf(43,plain,
% 281.52/282.17 (E(f6(x431,f4(x432,x432)),f6(x431,x432))),
% 281.52/282.17 inference(scs_inference,[],[40,2])).
% 281.52/282.17 cnf(44,plain,
% 281.52/282.17 (E(f4(x441,x442),f4(f6(a5,x441),f6(a5,x442)))),
% 281.52/282.17 inference(scs_inference,[],[39,36,40,2,3])).
% 281.52/282.17 cnf(47,plain,
% 281.52/282.17 (E(f4(f6(a5,x471),f6(a5,x472)),f4(x471,x472))),
% 281.52/282.17 inference(scs_inference,[],[44,2])).
% 281.52/282.17 cnf(48,plain,
% 281.52/282.17 (~E(f4(f4(a1,a3),a2),f6(a5,f4(a2,a2)))),
% 281.52/282.17 inference(scs_inference,[],[43,44,37,2,3])).
% 281.52/282.17 cnf(50,plain,
% 281.52/282.17 (E(f6(x501,f7(x502,x503)),f7(f6(x501,x502),f6(x501,x503)))),
% 281.52/282.17 inference(scs_inference,[],[25,2])).
% 281.52/282.17 cnf(53,plain,
% 281.52/282.17 (E(f6(f4(x531,x532),x533),f4(f6(x531,x533),f6(x532,x533)))),
% 281.52/282.17 inference(scs_inference,[],[26,2])).
% 281.52/282.17 cnf(54,plain,
% 281.52/282.17 (E(f6(x541,x542),f6(f4(x541,x541),x542))),
% 281.52/282.17 inference(scs_inference,[],[29,26,2,3])).
% 281.52/282.17 cnf(57,plain,
% 281.52/282.17 (E(f6(f4(x571,x571),x572),f6(x571,x572))),
% 281.52/282.17 inference(scs_inference,[],[54,2])).
% 281.52/282.17 cnf(60,plain,
% 281.52/282.17 (E(f6(f7(x601,x602),x603),f7(f6(x601,x603),f6(x602,x603)))),
% 281.52/282.17 inference(scs_inference,[],[27,2])).
% 281.52/282.17 cnf(61,plain,
% 281.52/282.17 (~E(f4(f4(a1,a3),a2),f6(f4(a5,a5),f4(a2,a2)))),
% 281.52/282.17 inference(scs_inference,[],[57,48,27,2,3])).
% 281.52/282.17 cnf(64,plain,
% 281.52/282.17 (E(f6(f7(x641,x642),f4(x643,x643)),f7(f6(x641,x643),f6(x642,x643)))),
% 281.52/282.17 inference(scs_inference,[],[60,43,19,2,3])).
% 281.52/282.17 cnf(67,plain,
% 281.52/282.17 (E(f7(f6(x671,x672),f6(x673,x672)),f6(f7(x671,x673),f4(x672,x672)))),
% 281.52/282.17 inference(scs_inference,[],[64,2])).
% 281.52/282.17 cnf(68,plain,
% 281.52/282.17 (E(f6(f4(x681,x681),f7(x682,x683)),f7(f6(x681,x682),f6(x681,x683)))),
% 281.52/282.17 inference(scs_inference,[],[50,57,64,2,3])).
% 281.52/282.17 cnf(71,plain,
% 281.52/282.17 (E(f7(f6(x711,x712),f6(x711,x713)),f6(f4(x711,x711),f7(x712,x713)))),
% 281.52/282.17 inference(scs_inference,[],[68,2])).
% 281.52/282.17 cnf(72,plain,
% 281.52/282.17 (E(f6(x721,x722),f6(f7(x721,x721),f4(x722,x722)))),
% 281.52/282.17 inference(scs_inference,[],[33,67,68,2,3])).
% 281.52/282.17 cnf(76,plain,
% 281.52/282.17 (E(f6(x761,x762),f6(f4(x761,x761),f7(x762,x762)))),
% 281.52/282.17 inference(scs_inference,[],[71,33,72,2,3])).
% 281.52/282.17 cnf(79,plain,
% 281.52/282.17 (E(f6(f4(x791,x791),f7(x792,x792)),f6(x791,x792))),
% 281.52/282.17 inference(scs_inference,[],[76,2])).
% 281.52/282.17 cnf(80,plain,
% 281.52/282.17 (E(f6(x801,f7(x802,x802)),f6(f7(x801,x801),f4(x802,x802)))),
% 281.52/282.17 inference(scs_inference,[],[67,50,76,2,3])).
% 281.52/282.17 cnf(83,plain,
% 281.52/282.17 (E(f6(f7(x831,x831),f4(x832,x832)),f6(x831,f7(x832,x832)))),
% 281.52/282.17 inference(scs_inference,[],[80,2])).
% 281.52/282.17 cnf(84,plain,
% 281.52/282.17 (E(f6(f7(x841,x841),x842),f6(f4(x841,x841),f7(x842,x842)))),
% 281.52/282.17 inference(scs_inference,[],[71,60,80,2,3])).
% 281.52/282.18 cnf(87,plain,
% 281.52/282.18 (E(f6(f4(x871,x871),f7(x872,x872)),f6(f7(x871,x871),x872))),
% 281.52/282.18 inference(scs_inference,[],[84,2])).
% 281.52/282.18 cnf(90,plain,
% 281.52/282.18 (E(x901,f7(x901,f4(x901,x902)))),
% 281.52/282.18 inference(scs_inference,[],[20,2])).
% 281.52/282.18 cnf(93,plain,
% 281.52/282.18 (E(f4(x931,f4(x932,x933)),f4(f4(x931,x932),x933))),
% 281.52/282.18 inference(scs_inference,[],[21,2])).
% 281.52/282.18 cnf(94,plain,
% 281.52/282.18 (E(f6(f4(f7(x941,x942),f7(x941,x942)),f7(x943,x943)),f7(f6(x941,x943),f6(x942,x943)))),
% 281.52/282.18 inference(scs_inference,[],[79,60,21,2,3])).
% 281.52/282.18 cnf(97,plain,
% 281.52/282.18 (E(f7(f6(x971,x972),f6(x973,x972)),f6(f4(f7(x971,x973),f7(x971,x973)),f7(x972,x972)))),
% 281.52/282.18 inference(scs_inference,[],[94,2])).
% 281.52/282.18 cnf(100,plain,
% 281.52/282.18 (E(f7(x1001,f7(x1002,x1003)),f7(f7(x1001,x1002),x1003))),
% 281.52/282.18 inference(scs_inference,[],[22,2])).
% 281.52/282.18 cnf(101,plain,
% 281.52/282.18 (E(f6(x1011,x1012),f6(f4(f7(x1011,x1011),f7(x1011,x1011)),f7(x1012,x1012)))),
% 281.52/282.18 inference(scs_inference,[],[97,33,22,2,3])).
% 281.52/282.18 cnf(104,plain,
% 281.52/282.18 (E(f6(f4(f7(x1041,x1041),f7(x1041,x1041)),f7(x1042,x1042)),f6(x1041,x1042))),
% 281.52/282.18 inference(scs_inference,[],[101,2])).
% 281.52/282.18 cnf(105,plain,
% 281.52/282.18 (E(f7(x1051,x1052),f7(f7(f7(x1051,x1052),x1051),x1052))),
% 281.52/282.18 inference(scs_inference,[],[100,33,101,2,3])).
% 281.52/282.18 cnf(108,plain,
% 281.52/282.18 (E(f7(f7(f7(x1081,x1082),x1081),x1082),f7(x1081,x1082))),
% 281.52/282.18 inference(scs_inference,[],[105,2])).
% 281.52/282.18 cnf(115,plain,
% 281.52/282.18 (E(f6(x1151,f6(x1152,x1153)),f6(f6(x1151,x1152),x1153))),
% 281.52/282.18 inference(scs_inference,[],[23,2])).
% 281.52/282.18 cnf(118,plain,
% 281.52/282.18 (E(a2,f4(a1,a2))),
% 281.52/282.18 inference(scs_inference,[],[11,2])).
% 281.52/282.18 cnf(121,plain,
% 281.52/282.18 (E(a2,f4(a3,a2))),
% 281.52/282.18 inference(scs_inference,[],[12,2])).
% 281.52/282.18 cnf(122,plain,
% 281.52/282.18 (E(f4(a3,a2),f4(a1,a2))),
% 281.52/282.18 inference(scs_inference,[],[118,12,2,3])).
% 281.52/282.18 cnf(123,plain,
% 281.52/282.18 (E(f4(a1,a2),f4(a3,a2))),
% 281.52/282.18 inference(scs_inference,[],[122,2])).
% 281.52/282.18 cnf(126,plain,
% 281.52/282.18 (E(a5,f6(f8(x1261),x1261))),
% 281.52/282.18 inference(scs_inference,[],[16,2])).
% 281.52/282.18 cnf(127,plain,
% 281.52/282.18 (E(f4(f6(a5,a1),f6(a5,a2)),f4(a3,a2))),
% 281.52/282.18 inference(scs_inference,[],[123,47,16,2,3])).
% 281.52/282.18 cnf(129,plain,
% 281.52/282.18 (E(f4(a3,a2),f4(f6(a5,a1),f6(a5,a2)))),
% 281.52/282.18 inference(scs_inference,[],[127,2])).
% 281.52/282.18 cnf(130,plain,
% 281.52/282.18 (E(f4(x1301,x1302),f4(f4(f4(x1301,x1302),x1301),x1302))),
% 281.52/282.18 inference(scs_inference,[],[93,29,127,2,3])).
% 281.52/282.18 cnf(133,plain,
% 281.52/282.18 (E(f4(f4(f4(x1331,x1332),x1331),x1332),f4(x1331,x1332))),
% 281.52/282.18 inference(scs_inference,[],[130,2])).
% 281.52/282.18 cnf(134,plain,
% 281.52/282.18 (E(a2,f4(f6(a5,a1),f6(a5,a2)))),
% 281.52/282.18 inference(scs_inference,[],[129,121,130,2,3])).
% 281.52/282.18 cnf(135,plain,
% 281.52/282.18 (E(f4(f6(a5,a1),f6(a5,a2)),a2)),
% 281.52/282.18 inference(scs_inference,[],[134,2])).
% 281.52/282.18 cnf(136,plain,
% 281.52/282.18 (E(f4(a5,f7(a5,x1361)),f6(f8(x1362),x1362))),
% 281.52/282.18 inference(scs_inference,[],[126,134,19,2,3])).
% 281.52/282.18 cnf(139,plain,
% 281.52/282.18 (~E(f4(f4(a1,a3),a2),f4(f6(a5,a1),f6(a5,a2)))),
% 281.52/282.18 inference(scs_inference,[],[28,135,136,2,3])).
% 281.52/282.18 cnf(140,plain,
% 281.52/282.18 (~E(f4(f4(a1,a3),a2),f6(a5,f4(a1,a2)))),
% 281.52/282.18 inference(scs_inference,[],[39,139,3])).
% 281.52/282.18 cnf(144,plain,
% 281.52/282.18 (E(f4(a3,a2),f4(f4(f4(a1,a2),a1),a2))),
% 281.52/282.18 inference(scs_inference,[],[133,123,3,2])).
% 281.52/282.18 cnf(146,plain,
% 281.52/282.18 (~E(f4(a1,a3),a3)),
% 281.52/282.18 inference(scs_inference,[],[129,139,3,4])).
% 281.52/282.18 cnf(147,plain,
% 281.52/282.18 (~E(f4(f4(a1,a3),a2),f4(a1,a2))),
% 281.52/282.18 inference(scs_inference,[],[36,140,3])).
% 281.52/282.18 cnf(150,plain,
% 281.52/282.18 (E(f7(a5,f4(a5,x1501)),f6(f8(x1502),x1502))),
% 281.52/282.18 inference(scs_inference,[],[126,20,3])).
% 281.52/282.18 cnf(152,plain,
% 281.52/282.18 (E(f6(f8(x1521),x1521),f7(a5,f4(a5,x1522)))),
% 281.52/282.18 inference(scs_inference,[],[126,20,3,2])).
% 281.52/282.18 cnf(154,plain,
% 281.52/282.18 (E(f4(a5,a5),f6(f8(x1541),x1541))),
% 281.52/282.18 inference(scs_inference,[],[126,14,3])).
% 281.52/282.18 cnf(156,plain,
% 281.52/282.18 (E(f6(f8(x1561),x1561),f4(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[126,14,3,2])).
% 281.52/282.18 cnf(157,plain,
% 281.52/282.18 (E(f7(a5,a5),f6(f8(x1571),x1571))),
% 281.52/282.18 inference(scs_inference,[],[126,15,3])).
% 281.52/282.18 cnf(159,plain,
% 281.52/282.18 (E(f6(f8(x1591),x1591),f7(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[126,15,3,2])).
% 281.52/282.18 cnf(162,plain,
% 281.52/282.18 (E(f6(a5,a5),f6(f8(x1621),x1621))),
% 281.52/282.18 inference(scs_inference,[],[126,13,3])).
% 281.52/282.18 cnf(164,plain,
% 281.52/282.18 (E(f6(f8(x1641),x1641),f6(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[126,13,3,2])).
% 281.52/282.18 cnf(167,plain,
% 281.52/282.18 (E(f6(f8(x1671),x1671),f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[104,162,3,2])).
% 281.52/282.18 cnf(174,plain,
% 281.52/282.18 (~E(f4(f4(a1,a3),a2),f4(a2,a1))),
% 281.52/282.18 inference(scs_inference,[],[147,17,3])).
% 281.52/282.18 cnf(180,plain,
% 281.52/282.18 (~E(f4(f4(a1,a3),a2),f4(f6(a5,a2),f6(a5,a1)))),
% 281.52/282.18 inference(scs_inference,[],[47,174,3])).
% 281.52/282.18 cnf(182,plain,
% 281.52/282.18 (~E(f4(f4(a1,a3),a2),f6(a5,f4(a2,a1)))),
% 281.52/282.18 inference(scs_inference,[],[39,180,3])).
% 281.52/282.18 cnf(199,plain,
% 281.52/282.18 (E(f6(a5,f6(f8(x1991),x1991)),f4(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[13,156,3])).
% 281.52/282.18 cnf(201,plain,
% 281.52/282.18 (E(f4(a5,a5),f6(a5,f6(f8(x2011),x2011)))),
% 281.52/282.18 inference(scs_inference,[],[13,156,3,2])).
% 281.52/282.18 cnf(202,plain,
% 281.52/282.18 (E(f6(a5,f6(f8(x2021),x2021)),f7(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[13,159,3])).
% 281.52/282.18 cnf(204,plain,
% 281.52/282.18 (E(f7(a5,a5),f6(a5,f6(f8(x2041),x2041)))),
% 281.52/282.18 inference(scs_inference,[],[13,159,3,2])).
% 281.52/282.18 cnf(205,plain,
% 281.52/282.18 (E(f6(a5,f6(f8(x2051),x2051)),f6(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[13,164,3])).
% 281.52/282.18 cnf(207,plain,
% 281.52/282.18 (E(f6(a5,a5),f6(a5,f6(f8(x2071),x2071)))),
% 281.52/282.18 inference(scs_inference,[],[13,164,3,2])).
% 281.52/282.18 cnf(210,plain,
% 281.52/282.18 (E(f6(f8(x2101),x2101),f6(a5,f4(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[13,154,3,2])).
% 281.52/282.18 cnf(211,plain,
% 281.52/282.18 (E(f6(a5,f7(a5,a5)),f6(f8(x2111),x2111))),
% 281.52/282.18 inference(scs_inference,[],[13,157,3])).
% 281.52/282.18 cnf(213,plain,
% 281.52/282.18 (E(f6(f8(x2131),x2131),f6(a5,f7(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[13,157,3,2])).
% 281.52/282.18 cnf(216,plain,
% 281.52/282.18 (E(f6(f8(x2161),x2161),f6(a5,f6(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[13,162,3,2])).
% 281.52/282.18 cnf(219,plain,
% 281.52/282.18 (E(a5,f6(a5,f6(f8(x2191),x2191)))),
% 281.52/282.18 inference(scs_inference,[],[13,16,3,2])).
% 281.52/282.18 cnf(222,plain,
% 281.52/282.18 (E(f6(f8(x2221),x2221),f4(f4(a5,a5),f4(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[14,154,3,2])).
% 281.52/282.18 cnf(225,plain,
% 281.52/282.18 (E(f6(f8(x2251),x2251),f4(f7(a5,a5),f7(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[14,157,3,2])).
% 281.52/282.18 cnf(228,plain,
% 281.52/282.18 (E(f6(f8(x2281),x2281),f4(f6(a5,a5),f6(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[14,162,3,2])).
% 281.52/282.18 cnf(231,plain,
% 281.52/282.18 (E(f6(f8(x2311),x2311),f7(f4(a5,a5),f4(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[15,154,3,2])).
% 281.52/282.18 cnf(234,plain,
% 281.52/282.18 (E(f6(f8(x2341),x2341),f7(f7(a5,a5),f7(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[15,157,3,2])).
% 281.52/282.18 cnf(237,plain,
% 281.52/282.18 (E(f6(f8(x2371),x2371),f7(f6(a5,a5),f6(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[15,162,3,2])).
% 281.52/282.18 cnf(240,plain,
% 281.52/282.18 (E(f6(f8(x2401),x2401),f6(f7(a5,a5),f4(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[83,211,3,2])).
% 281.52/282.18 cnf(241,plain,
% 281.52/282.18 (E(f4(a5,a5),f7(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[201,202,3])).
% 281.52/282.18 cnf(243,plain,
% 281.52/282.18 (E(f7(a5,a5),f4(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[201,202,3,2])).
% 281.52/282.18 cnf(244,plain,
% 281.52/282.18 (E(f7(f7(f7(a5,a5),a5),a5),f4(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[108,243,3])).
% 281.52/282.18 cnf(247,plain,
% 281.52/282.18 (E(f4(f4(f4(a5,a5),a5),a5),f7(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[133,241,3])).
% 281.52/282.18 cnf(249,plain,
% 281.52/282.18 (E(f7(a5,a5),f4(f4(f4(a5,a5),a5),a5))),
% 281.52/282.18 inference(scs_inference,[],[133,241,3,2])).
% 281.52/282.18 cnf(251,plain,
% 281.52/282.18 (E(f4(f4(f4(a1,a2),a1),a2),a2)),
% 281.52/282.18 inference(scs_inference,[],[144,121,3,2])).
% 281.52/282.18 cnf(252,plain,
% 281.52/282.18 (E(f7(a5,a5),f6(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[204,205,3])).
% 281.52/282.18 cnf(254,plain,
% 281.52/282.18 (E(f6(a5,a5),f7(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[204,205,3,2])).
% 281.52/282.18 cnf(256,plain,
% 281.52/282.18 (E(f4(f4(f4(a5,a5),a5),a5),f6(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[249,254,3,2])).
% 281.52/282.18 cnf(257,plain,
% 281.52/282.18 (E(f4(f4(a5,a5),f4(a5,a5)),f6(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[256,93,3])).
% 281.52/282.18 cnf(259,plain,
% 281.52/282.18 (E(f6(a5,a5),f4(f4(a5,a5),f4(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[257,2])).
% 281.52/282.18 cnf(260,plain,
% 281.52/282.18 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f7(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[104,254,257,2,3])).
% 281.52/282.18 cnf(262,plain,
% 281.52/282.18 (E(f7(a5,a5),f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[260,2])).
% 281.52/282.18 cnf(263,plain,
% 281.52/282.18 (E(f6(f4(f8(x2631),f8(x2631)),f7(x2631,x2631)),a5)),
% 281.52/282.18 inference(scs_inference,[],[16,79,260,2,3])).
% 281.52/282.18 cnf(266,plain,
% 281.52/282.18 (E(a5,f6(f4(f8(x2661),f8(x2661)),f7(x2661,x2661)))),
% 281.52/282.18 inference(scs_inference,[],[263,2])).
% 281.52/282.18 cnf(267,plain,
% 281.52/282.18 (E(f7(f7(f7(a5,a5),a5),a5),f6(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[108,252,263,2,3])).
% 281.52/282.18 cnf(270,plain,
% 281.52/282.18 (E(f6(f8(x2701),x2701),f6(f4(f8(x2702),f8(x2702)),f7(x2702,x2702)))),
% 281.52/282.18 inference(scs_inference,[],[16,266,267,2,3])).
% 281.52/282.18 cnf(271,plain,
% 281.52/282.18 (E(f6(f4(f8(x2711),f8(x2711)),f7(x2711,x2711)),f6(f8(x2712),x2712))),
% 281.52/282.18 inference(scs_inference,[],[270,2])).
% 281.52/282.18 cnf(272,plain,
% 281.52/282.18 (E(f6(a5,a5),f4(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[207,270,199,2,3])).
% 281.52/282.18 cnf(274,plain,
% 281.52/282.18 (E(f4(a5,a5),f6(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[272,2])).
% 281.52/282.18 cnf(275,plain,
% 281.52/282.18 (E(f6(f4(f8(x2751),f8(x2751)),f7(x2751,x2751)),f6(f7(a5,a5),f4(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[271,240,272,2,3])).
% 281.52/282.18 cnf(277,plain,
% 281.52/282.18 (E(f6(f7(a5,a5),f4(a5,a5)),f6(f4(f8(x2771),f8(x2771)),f7(x2771,x2771)))),
% 281.52/282.18 inference(scs_inference,[],[275,2])).
% 281.52/282.18 cnf(278,plain,
% 281.52/282.18 (E(f6(f7(a5,a5),f4(a5,a5)),a5)),
% 281.52/282.18 inference(scs_inference,[],[277,263,3])).
% 281.52/282.18 cnf(280,plain,
% 281.52/282.18 (E(a5,f6(f7(a5,a5),f4(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[277,263,3,2])).
% 281.52/282.18 cnf(281,plain,
% 281.52/282.18 (E(f6(f4(a5,a5),f7(f4(a5,a5),f4(a5,a5))),a5)),
% 281.52/282.18 inference(scs_inference,[],[87,278,3])).
% 281.52/282.18 cnf(284,plain,
% 281.52/282.18 (E(f6(f8(x2841),x2841),f6(f6(a5,a5),a5))),
% 281.52/282.18 inference(scs_inference,[],[115,216,3])).
% 281.52/282.18 cnf(286,plain,
% 281.52/282.18 (E(f6(f6(a5,a5),a5),f6(f8(x2861),x2861))),
% 281.52/282.18 inference(scs_inference,[],[115,216,3,2])).
% 281.52/282.18 cnf(289,plain,
% 281.52/282.18 (E(a5,f6(f6(a5,a5),a5))),
% 281.52/282.18 inference(scs_inference,[],[16,286,3,2])).
% 281.52/282.18 cnf(292,plain,
% 281.52/282.18 (E(f6(f6(a5,f8(x2921)),x2921),a5)),
% 281.52/282.18 inference(scs_inference,[],[219,115,3,2])).
% 281.52/282.18 cnf(293,plain,
% 281.52/282.18 (E(a5,f6(a5,f6(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[289,23,3])).
% 281.52/282.18 cnf(295,plain,
% 281.52/282.18 (E(f6(a5,f6(a5,a5)),a5)),
% 281.52/282.18 inference(scs_inference,[],[289,23,3,2])).
% 281.52/282.18 cnf(297,plain,
% 281.52/282.18 (E(f6(f7(a5,a5),f4(a5,a5)),f6(a5,f6(a5,a5)))),
% 281.52/282.18 inference(scs_inference,[],[280,295,3,2])).
% 281.52/282.18 cnf(300,plain,
% 281.52/282.18 (E(f4(f4(f4(a1,a2),a1),a2),f4(a2,a3))),
% 281.52/282.18 inference(scs_inference,[],[17,144,3,2])).
% 281.52/282.18 cnf(301,plain,
% 281.52/282.18 (E(f4(a2,f4(f4(a1,a2),a1)),f4(a2,a3))),
% 281.52/282.18 inference(scs_inference,[],[17,300,3])).
% 281.52/282.18 cnf(303,plain,
% 281.52/282.18 (E(f4(a2,a3),f4(a2,f4(f4(a1,a2),a1)))),
% 281.52/282.18 inference(scs_inference,[],[301,2])).
% 281.52/282.18 cnf(304,plain,
% 281.52/282.18 (E(f4(a5,f4(f4(a5,a5),a5)),f6(a5,a5))),
% 281.52/282.18 inference(scs_inference,[],[17,256,301,2,3])).
% 281.52/282.18 cnf(306,plain,
% 281.52/282.18 (E(f6(a5,a5),f4(a5,f4(f4(a5,a5),a5)))),
% 281.52/282.18 inference(scs_inference,[],[304,2])).
% 281.52/282.18 cnf(307,plain,
% 281.52/282.18 (E(f4(a3,a2),f4(a2,f4(f4(a1,a2),a1)))),
% 281.52/282.18 inference(scs_inference,[],[17,303,304,2,3])).
% 281.52/282.18 cnf(309,plain,
% 281.52/282.18 (E(f4(a2,f4(f4(a1,a2),a1)),f4(a3,a2))),
% 281.52/282.18 inference(scs_inference,[],[307,2])).
% 281.52/282.18 cnf(310,plain,
% 281.52/282.18 (E(f4(a5,a5),f4(a5,f4(f4(a5,a5),a5)))),
% 281.52/282.18 inference(scs_inference,[],[274,306,307,2,3])).
% 281.52/282.18 cnf(312,plain,
% 281.52/282.18 (E(f4(f4(x3121,x3122),x3123),f4(f4(x3123,x3121),x3122))),
% 281.52/282.18 inference(scs_inference,[],[17,93,310,2,3])).
% 281.52/282.18 cnf(315,plain,
% 281.52/282.18 (E(f4(f4(x3151,x3152),x3153),f4(f4(x3152,x3153),x3151))),
% 281.52/282.18 inference(scs_inference,[],[312,2])).
% 281.52/282.18 cnf(316,plain,
% 281.52/282.18 (E(f6(f7(a5,a5),f4(a5,a5)),f6(f6(a5,a5),a5))),
% 281.52/282.18 inference(scs_inference,[],[297,115,312,2,3])).
% 281.52/282.18 cnf(318,plain,
% 281.52/282.19 (E(f6(f6(a5,a5),a5),f6(f7(a5,a5),f4(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[316,2])).
% 281.52/282.19 cnf(319,plain,
% 281.52/282.19 (E(f4(a5,f4(f4(a5,a5),a5)),f7(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[17,247,316,2,3])).
% 281.52/282.19 cnf(322,plain,
% 281.52/282.19 (E(f6(f6(a5,a5),a5),f6(f4(f8(x3221),f8(x3221)),f7(x3221,x3221)))),
% 281.52/282.19 inference(scs_inference,[],[318,277,319,2,3])).
% 281.52/282.19 cnf(323,plain,
% 281.52/282.19 (E(f6(f4(f8(x3231),f8(x3231)),f7(x3231,x3231)),f6(f6(a5,a5),a5))),
% 281.52/282.19 inference(scs_inference,[],[322,2])).
% 281.52/282.19 cnf(324,plain,
% 281.52/282.19 (E(f4(x3241,x3242),f4(f4(f4(x3242,x3241),x3242),x3241))),
% 281.52/282.19 inference(scs_inference,[],[17,322,130,2,3])).
% 281.52/282.19 cnf(326,plain,
% 281.52/282.19 (E(f4(f4(f4(x3261,x3262),x3261),x3262),f4(x3262,x3261))),
% 281.52/282.19 inference(scs_inference,[],[324,2])).
% 281.52/282.19 cnf(327,plain,
% 281.52/282.19 (E(f4(f7(a5,x3271),a5),f6(f8(x3272),x3272))),
% 281.52/282.19 inference(scs_inference,[],[17,324,136,2,3])).
% 281.52/282.19 cnf(330,plain,
% 281.52/282.19 (E(f4(x3301,f4(x3302,x3303)),f4(x3302,f4(x3303,x3301)))),
% 281.52/282.19 inference(scs_inference,[],[17,327,21,2,3])).
% 281.52/282.19 cnf(333,plain,
% 281.52/282.19 (E(f4(x3331,f4(x3332,x3333)),f4(x3333,f4(x3331,x3332)))),
% 281.52/282.19 inference(scs_inference,[],[330,2])).
% 281.52/282.19 cnf(334,plain,
% 281.52/282.19 (E(f6(f4(f8(x3341),f8(x3341)),f7(x3341,x3341)),f6(a5,f6(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[323,330,23,2,3])).
% 281.52/282.19 cnf(336,plain,
% 281.52/282.19 (E(f6(a5,f6(a5,a5)),f6(f4(f8(x3361),f8(x3361)),f7(x3361,x3361)))),
% 281.52/282.19 inference(scs_inference,[],[334,2])).
% 281.52/282.19 cnf(337,plain,
% 281.52/282.19 (E(f7(a5,f7(f7(a5,a5),a5)),f4(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[18,244,3])).
% 281.52/282.19 cnf(339,plain,
% 281.52/282.19 (E(f4(a5,a5),f7(a5,f7(f7(a5,a5),a5)))),
% 281.52/282.19 inference(scs_inference,[],[337,2])).
% 281.52/282.19 cnf(340,plain,
% 281.52/282.19 (E(f7(f4(a5,x3401),a5),f6(f8(x3402),x3402))),
% 281.52/282.19 inference(scs_inference,[],[18,337,150,2,3])).
% 281.52/282.19 cnf(343,plain,
% 281.52/282.19 (E(f4(f4(f4(f4(a5,a5),f4(a5,a5)),f4(a5,a5)),f4(a5,a5)),f6(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[326,340,257,2,3])).
% 281.52/282.19 cnf(345,plain,
% 281.52/282.19 (E(f6(a5,a5),f4(f4(f4(f4(a5,a5),f4(a5,a5)),f4(a5,a5)),f4(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[343,2])).
% 281.52/282.19 cnf(346,plain,
% 281.52/282.19 (E(f4(f4(a2,f4(a1,a2)),a1),f4(a2,a3))),
% 281.52/282.19 inference(scs_inference,[],[315,300,343,2,3])).
% 281.52/282.19 cnf(349,plain,
% 281.52/282.19 (E(f4(a5,a5),f4(f4(f4(f4(a5,a5),f4(a5,a5)),f4(a5,a5)),f4(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[345,274,346,2,3])).
% 281.52/282.19 cnf(350,plain,
% 281.52/282.19 (E(f4(f4(f4(f4(a5,a5),f4(a5,a5)),f4(a5,a5)),f4(a5,a5)),f4(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[349,2])).
% 281.52/282.19 cnf(351,plain,
% 281.52/282.19 (E(f4(x3511,f4(x3512,x3513)),f4(f4(x3513,x3511),x3512))),
% 281.52/282.19 inference(scs_inference,[],[333,93,349,2,3])).
% 281.52/282.19 cnf(353,plain,
% 281.52/282.19 (E(f4(f4(x3531,x3532),x3533),f4(x3532,f4(x3533,x3531)))),
% 281.52/282.19 inference(scs_inference,[],[351,2])).
% 281.52/282.19 cnf(354,plain,
% 281.52/282.19 (E(f6(a5,a5),f4(f4(a5,f4(a5,a5)),a5))),
% 281.52/282.19 inference(scs_inference,[],[259,351,2,3])).
% 281.52/282.19 cnf(356,plain,
% 281.52/282.19 (E(f4(f4(a5,f4(a5,a5)),a5),f6(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[354,2])).
% 281.52/282.19 cnf(357,plain,
% 281.52/282.19 (E(f4(f4(f4(f4(a5,a5),f4(a5,a5)),f4(a5,a5)),f4(a5,a5)),f7(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[350,354,241,2,3])).
% 281.52/282.19 cnf(359,plain,
% 281.52/282.19 (E(f4(f4(a5,f4(a5,a5)),a5),f7(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[356,254,357,2,3])).
% 281.52/282.19 cnf(361,plain,
% 281.52/282.19 (E(f7(a5,f7(f7(a5,a5),a5)),f6(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[18,359,267,2,3])).
% 281.52/282.19 cnf(364,plain,
% 281.52/282.19 (E(f4(f4(a5,f4(a5,a5)),a5),f4(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[356,361,272,2,3])).
% 281.52/282.19 cnf(366,plain,
% 281.52/282.19 (E(f4(f4(a1,a2),f4(a1,a2)),f4(a2,a3))),
% 281.52/282.19 inference(scs_inference,[],[353,364,301,2,3])).
% 281.52/282.19 cnf(380,plain,
% 281.52/282.19 (E(f6(f6(a5,a5),a5),f4(a5,f7(a5,x3801)))),
% 281.52/282.19 inference(scs_inference,[],[19,289,3,2])).
% 281.52/282.19 cnf(383,plain,
% 281.52/282.19 (E(f6(f4(f8(x3831),f8(x3831)),f7(x3831,x3831)),f4(a5,f7(a5,x3832)))),
% 281.52/282.19 inference(scs_inference,[],[19,266,3,2])).
% 281.52/282.19 cnf(392,plain,
% 281.52/282.19 (E(f6(a5,f6(a5,a5)),f4(a5,f7(a5,x3921)))),
% 281.52/282.19 inference(scs_inference,[],[19,293,3,2])).
% 281.52/282.19 cnf(407,plain,
% 281.52/282.19 (E(f6(f7(a5,a5),f4(a5,a5)),f7(a5,f4(a5,x4071)))),
% 281.52/282.19 inference(scs_inference,[],[20,280,3,2])).
% 281.52/282.19 cnf(410,plain,
% 281.52/282.19 (E(f6(f6(a5,a5),a5),f7(a5,f4(a5,x4101)))),
% 281.52/282.19 inference(scs_inference,[],[20,289,3,2])).
% 281.52/282.19 cnf(413,plain,
% 281.52/282.19 (E(f6(f4(f8(x4131),f8(x4131)),f7(x4131,x4131)),f7(a5,f4(a5,x4132)))),
% 281.52/282.19 inference(scs_inference,[],[20,266,3,2])).
% 281.52/282.19 cnf(422,plain,
% 281.52/282.19 (E(f6(a5,f6(a5,a5)),f7(a5,f4(a5,x4221)))),
% 281.52/282.19 inference(scs_inference,[],[20,293,3,2])).
% 281.52/282.19 cnf(438,plain,
% 281.52/282.19 (E(f6(f6(a5,f8(x4381)),x4381),f4(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[23,199,3])).
% 281.52/282.19 cnf(442,plain,
% 281.52/282.19 (E(f6(f6(a5,f8(x4421)),x4421),f7(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[23,438,202,2,3])).
% 281.52/282.19 cnf(446,plain,
% 281.52/282.19 (E(f6(f6(a5,f8(x4461)),x4461),f6(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[23,442,205,2,3])).
% 281.52/282.19 cnf(462,plain,
% 281.52/282.19 (E(a5,f7(a5,f7(f7(a5,a5),a5)))),
% 281.52/282.19 inference(scs_inference,[],[29,339,3])).
% 281.52/282.19 cnf(474,plain,
% 281.52/282.19 (E(f4(x4741,x4742),f4(x4742,f4(f4(x4741,x4742),x4741)))),
% 281.52/282.19 inference(scs_inference,[],[29,353,3])).
% 281.52/282.19 cnf(478,plain,
% 281.52/282.19 (E(x4781,f4(x4781,f4(f4(x4781,x4781),x4781)))),
% 281.52/282.19 inference(scs_inference,[],[29,474,3])).
% 281.52/282.19 cnf(484,plain,
% 281.52/282.19 (E(x4841,f4(f4(f4(x4841,x4841),x4841),x4841))),
% 281.52/282.19 inference(scs_inference,[],[29,324,3])).
% 281.52/282.19 cnf(489,plain,
% 281.52/282.19 (E(f4(f4(f4(f4(x4891,x4891),f4(x4891,x4891)),f4(x4891,x4891)),f4(x4891,x4891)),x4891)),
% 281.52/282.19 inference(scs_inference,[],[29,484,3,2])).
% 281.52/282.19 cnf(490,plain,
% 281.52/282.19 (E(f4(a1,a2),f4(a2,a3))),
% 281.52/282.19 inference(scs_inference,[],[29,366,3])).
% 281.52/282.19 cnf(492,plain,
% 281.52/282.19 (E(f4(a2,a3),f4(a1,a2))),
% 281.52/282.19 inference(scs_inference,[],[29,366,3,2])).
% 281.52/282.19 cnf(493,plain,
% 281.52/282.19 (~E(f4(f4(a1,a3),a2),f4(a2,a3))),
% 281.52/282.19 inference(scs_inference,[],[492,147,3])).
% 281.52/282.19 cnf(494,plain,
% 281.52/282.19 (~E(f4(f4(a1,a3),a2),f4(f6(a5,a2),f6(a5,a3)))),
% 281.52/282.19 inference(scs_inference,[],[47,493,3])).
% 281.52/282.19 cnf(496,plain,
% 281.52/282.19 (~E(f4(f4(a1,a3),a2),f6(a5,f4(a2,a3)))),
% 281.52/282.19 inference(scs_inference,[],[39,494,3])).
% 281.52/282.19 cnf(505,plain,
% 281.52/282.19 (~E(f4(f4(a1,a3),a2),f4(f4(a1,a2),f4(a1,a2)))),
% 281.52/282.19 inference(scs_inference,[],[366,493,3])).
% 281.52/282.19 cnf(510,plain,
% 281.52/282.19 (~E(f4(a1,a3),f4(f4(f4(f4(a2,a2),f4(a2,a2)),f4(a2,a2)),f4(a2,a2)))),
% 281.52/282.19 inference(scs_inference,[],[32,489,3])).
% 281.52/282.19 cnf(512,plain,
% 281.52/282.19 (~E(f4(a1,a3),f4(f4(f4(a1,a2),a1),a2))),
% 281.52/282.19 inference(scs_inference,[],[32,251,3])).
% 281.52/282.19 cnf(519,plain,
% 281.52/282.19 (~E(f4(a1,a3),f4(f6(a5,a1),f6(a5,a2)))),
% 281.52/282.19 inference(scs_inference,[],[32,135,3])).
% 281.52/282.19 cnf(520,plain,
% 281.52/282.19 (~E(f4(a1,a3),f4(a3,a2))),
% 281.52/282.19 inference(scs_inference,[],[129,519,3])).
% 281.52/282.19 cnf(521,plain,
% 281.52/282.19 (~E(f4(a1,a3),f4(a2,f4(f4(a1,a2),a1)))),
% 281.52/282.19 inference(scs_inference,[],[309,520,3])).
% 281.52/282.19 cnf(522,plain,
% 281.52/282.19 (~E(f4(a1,a3),f4(a2,a3))),
% 281.52/282.19 inference(scs_inference,[],[303,521,3])).
% 281.52/282.19 cnf(527,plain,
% 281.52/282.19 (~E(f4(a1,a3),f4(a2,a2))),
% 281.52/282.19 inference(scs_inference,[],[484,510,3])).
% 281.52/282.19 cnf(529,plain,
% 281.52/282.19 (~E(f4(a1,a3),f4(a2,a1))),
% 281.52/282.19 inference(scs_inference,[],[324,512,3])).
% 281.52/282.19 cnf(537,plain,
% 281.52/282.19 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),a5)),
% 281.52/282.19 inference(scs_inference,[],[33,262,3,2])).
% 281.52/282.19 cnf(550,plain,
% 281.52/282.19 (~E(f4(f4(a1,a3),a2),f7(f7(a2,a2),f7(a2,a2)))),
% 281.52/282.19 inference(scs_inference,[],[34,15,3])).
% 281.52/282.19 cnf(552,plain,
% 281.52/282.19 (E(f6(a5,a5),f6(f4(f8(x5521),f8(x5521)),f7(x5521,x5521)))),
% 281.52/282.19 inference(scs_inference,[],[36,336,3])).
% 281.52/282.19 cnf(554,plain,
% 281.52/282.19 (E(f6(f4(f8(x5541),f8(x5541)),f7(x5541,x5541)),f6(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[36,336,3,2])).
% 281.52/282.19 cnf(555,plain,
% 281.52/282.19 (E(f6(a5,a5),f4(a5,f7(a5,x5551)))),
% 281.52/282.19 inference(scs_inference,[],[36,392,3])).
% 281.52/282.19 cnf(557,plain,
% 281.52/282.19 (E(f4(a5,f7(a5,x5571)),f6(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[36,392,3,2])).
% 281.52/282.19 cnf(558,plain,
% 281.52/282.19 (E(f6(a5,a5),f7(a5,f4(a5,x5581)))),
% 281.52/282.19 inference(scs_inference,[],[36,422,3])).
% 281.52/282.19 cnf(560,plain,
% 281.52/282.19 (E(f7(a5,f4(a5,x5601)),f6(a5,a5))),
% 281.52/282.19 inference(scs_inference,[],[36,422,3,2])).
% 281.52/282.19 cnf(564,plain,
% 281.52/282.19 (E(f6(x5641,x5642),f6(f6(a5,x5641),x5642))),
% 281.52/282.19 inference(scs_inference,[],[36,115,3])).
% 281.52/282.19 cnf(567,plain,
% 281.52/282.19 (E(f6(f6(a5,x5671),x5672),f6(x5671,x5672))),
% 281.52/282.19 inference(scs_inference,[],[36,115,3,2])).
% 281.52/282.19 cnf(571,plain,
% 281.52/282.19 (E(x5711,f6(f6(a5,a5),x5711))),
% 281.52/282.19 inference(scs_inference,[],[36,564,3])).
% 281.52/282.19 cnf(573,plain,
% 281.52/282.19 (E(f6(f6(a5,a5),x5731),x5731)),
% 281.52/282.19 inference(scs_inference,[],[36,564,3,2])).
% 281.52/282.19 cnf(580,plain,
% 281.52/282.19 (~E(f4(f4(a1,a3),a2),f6(f6(a5,a5),f6(a5,a2)))),
% 281.52/282.19 inference(scs_inference,[],[37,573,3])).
% 281.52/282.19 cnf(588,plain,
% 281.52/282.19 (E(f7(a5,a5),f4(a5,f7(a5,x5881)))),
% 281.52/282.19 inference(scs_inference,[],[557,254,3,2])).
% 281.52/282.19 cnf(590,plain,
% 281.52/282.19 (E(f4(f4(a5,a5),f4(a5,a5)),f7(a5,f4(a5,x5901)))),
% 281.52/282.19 inference(scs_inference,[],[560,259,3,2])).
% 281.52/282.19 cnf(593,plain,
% 281.52/282.19 (E(f7(a5,f4(a5,x5931)),f6(f7(a5,a5),a5))),
% 281.52/282.19 inference(scs_inference,[],[40,407,3,2])).
% 281.52/282.19 cnf(594,plain,
% 281.52/282.19 (E(a5,f6(f7(a5,a5),a5))),
% 281.52/282.19 inference(scs_inference,[],[90,593,3])).
% 281.52/282.19 cnf(597,plain,
% 281.52/282.19 (E(f6(f7(a5,a5),a5),a5)),
% 281.52/282.19 inference(scs_inference,[],[90,593,3,2])).
% 281.52/282.19 cnf(598,plain,
% 281.52/282.19 (E(f6(f7(a5,a5),a5),f6(a5,f6(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[40,297,3])).
% 281.52/282.19 cnf(600,plain,
% 281.52/282.19 (E(f6(a5,f6(a5,a5)),f6(f7(a5,a5),a5))),
% 281.52/282.19 inference(scs_inference,[],[40,297,3,2])).
% 281.52/282.19 cnf(618,plain,
% 281.52/282.19 (E(f6(f7(a5,a5),a5),f6(f4(f8(x6181),f8(x6181)),f7(x6181,x6181)))),
% 281.52/282.19 inference(scs_inference,[],[413,593,3,2])).
% 281.52/282.19 cnf(621,plain,
% 281.52/282.19 (E(f6(f8(x6211),x6211),f6(f7(a5,a5),a5))),
% 281.52/282.19 inference(scs_inference,[],[618,271,3,2])).
% 281.52/282.19 cnf(624,plain,
% 281.52/282.19 (E(f6(f6(a5,a5),a5),f6(f7(a5,a5),a5))),
% 281.52/282.19 inference(scs_inference,[],[40,316,3,2])).
% 281.52/282.19 cnf(629,plain,
% 281.52/282.19 (E(f6(f8(x6291),f4(x6291,x6291)),f7(f7(a5,a5),f7(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[43,234,3])).
% 281.52/282.19 cnf(632,plain,
% 281.52/282.19 (E(f7(f7(a5,a5),f7(a5,a5)),f6(f8(x6321),f4(x6321,x6321)))),
% 281.52/282.19 inference(scs_inference,[],[43,234,3,2])).
% 281.52/282.19 cnf(636,plain,
% 281.52/282.19 (E(f4(f7(a5,a5),f7(a5,a5)),f6(f8(x6361),f4(x6361,x6361)))),
% 281.52/282.19 inference(scs_inference,[],[43,225,3,2])).
% 281.52/282.19 cnf(637,plain,
% 281.52/282.19 (E(f6(f6(a5,a5),f4(a5,a5)),f6(f7(a5,a5),a5))),
% 281.52/282.19 inference(scs_inference,[],[43,624,3])).
% 281.52/282.19 cnf(639,plain,
% 281.52/282.19 (E(f6(f7(a5,a5),a5),f6(f6(a5,a5),f4(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[43,624,3,2])).
% 281.52/282.19 cnf(642,plain,
% 281.52/282.19 (E(f6(f6(a5,a5),f4(a5,a5)),f6(f7(a5,a5),f4(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[43,639,3,2])).
% 281.52/282.19 cnf(646,plain,
% 281.52/282.19 (E(f6(f7(a5,a5),a5),f6(f8(x6461),f4(x6461,x6461)))),
% 281.52/282.19 inference(scs_inference,[],[43,621,3,2])).
% 281.52/282.19 cnf(649,plain,
% 281.52/282.19 (E(f6(f8(x6491),f4(x6491,x6491)),f6(f7(a5,a5),f4(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[43,646,3,2])).
% 281.52/282.19 cnf(650,plain,
% 281.52/282.19 (E(f6(f8(x6501),f4(x6501,x6501)),f4(f4(a5,a5),f4(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[43,222,3])).
% 281.52/282.19 cnf(654,plain,
% 281.52/282.19 (E(f6(f8(x6541),f4(x6541,x6541)),f7(f4(a5,a5),f4(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[43,231,3])).
% 281.52/282.19 cnf(657,plain,
% 281.52/282.19 (E(f7(f4(a5,a5),f4(a5,a5)),f6(f8(x6571),f4(x6571,x6571)))),
% 281.52/282.19 inference(scs_inference,[],[43,231,3,2])).
% 281.52/282.19 cnf(658,plain,
% 281.52/282.19 (E(f6(f8(x6581),f4(x6581,x6581)),f4(f6(a5,a5),f6(a5,a5)))),
% 281.52/282.19 inference(scs_inference,[],[43,228,3])).
% 281.52/282.19 cnf(661,plain,
% 281.52/282.19 (E(f4(f6(a5,a5),f6(a5,a5)),f6(f8(x6611),f4(x6611,x6611)))),
% 281.52/282.19 inference(scs_inference,[],[43,228,3,2])).
% 281.52/282.19 cnf(665,plain,
% 281.52/282.19 (E(f7(f6(a5,a5),f6(a5,a5)),f6(f8(x6651),f4(x6651,x6651)))),
% 281.52/282.19 inference(scs_inference,[],[43,237,3,2])).
% 281.52/282.19 cnf(669,plain,
% 281.52/282.19 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f6(f8(x6691),f4(x6691,x6691)))),
% 281.67/282.19 inference(scs_inference,[],[43,167,3,2])).
% 281.67/282.19 cnf(673,plain,
% 281.67/282.19 (E(f6(a5,f7(a5,a5)),f6(f8(x6731),f4(x6731,x6731)))),
% 281.67/282.19 inference(scs_inference,[],[43,213,3,2])).
% 281.67/282.19 cnf(674,plain,
% 281.67/282.19 (E(f6(f8(x6741),f4(x6741,x6741)),f6(a5,f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[43,210,3])).
% 281.67/282.19 cnf(677,plain,
% 281.67/282.19 (E(f6(a5,f4(a5,a5)),f6(f8(x6771),f4(x6771,x6771)))),
% 281.67/282.19 inference(scs_inference,[],[43,210,3,2])).
% 281.67/282.19 cnf(685,plain,
% 281.67/282.19 (E(f7(a5,f4(a5,x6851)),f6(f8(x6852),f4(x6852,x6852)))),
% 281.67/282.19 inference(scs_inference,[],[43,152,3,2])).
% 281.67/282.19 cnf(696,plain,
% 281.67/282.19 (E(f4(a5,f7(a5,x6961)),f6(f6(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[43,380,3,2])).
% 281.67/282.19 cnf(699,plain,
% 281.67/282.19 (E(f7(a5,f4(a5,x6991)),f6(f6(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[43,410,3,2])).
% 281.67/282.19 cnf(702,plain,
% 281.67/282.19 (E(f6(f6(a5,a5),f4(a5,a5)),f4(f4(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[590,699,3,2])).
% 281.67/282.19 cnf(703,plain,
% 281.67/282.19 (E(f6(f6(a5,f8(x7031)),f4(x7031,x7031)),a5)),
% 281.67/282.19 inference(scs_inference,[],[43,292,3])).
% 281.67/282.19 cnf(707,plain,
% 281.67/282.19 (E(a5,f6(f8(x7071),f4(x7071,x7071)))),
% 281.67/282.19 inference(scs_inference,[],[685,90,703,2,3])).
% 281.67/282.19 cnf(710,plain,
% 281.67/282.19 (E(f6(f8(x7101),f4(x7101,x7101)),a5)),
% 281.67/282.19 inference(scs_inference,[],[707,2])).
% 281.67/282.19 cnf(711,plain,
% 281.67/282.19 (E(f6(a5,f4(f6(a5,a5),f6(a5,a5))),a5)),
% 281.67/282.19 inference(scs_inference,[],[43,295,707,2,3])).
% 281.67/282.19 cnf(714,plain,
% 281.67/282.19 (E(f6(f8(x7141),f4(f4(x7141,x7141),f4(x7141,x7141))),a5)),
% 281.67/282.19 inference(scs_inference,[],[43,710,711,2,3])).
% 281.67/282.19 cnf(717,plain,
% 281.67/282.19 (E(f6(f8(x7171),f4(x7171,x7171)),f6(a5,f6(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[43,216,714,2,3])).
% 281.67/282.19 cnf(720,plain,
% 281.67/282.19 (E(f6(a5,f6(a5,a5)),f6(f8(x7201),f4(x7201,x7201)))),
% 281.67/282.19 inference(scs_inference,[],[717,2])).
% 281.67/282.19 cnf(721,plain,
% 281.67/282.19 (E(f6(f6(a5,a5),f4(a5,a5)),f6(f8(x7211),x7211))),
% 281.67/282.19 inference(scs_inference,[],[43,286,717,2,3])).
% 281.67/282.19 cnf(723,plain,
% 281.67/282.19 (E(f6(f8(x7231),x7231),f6(f6(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[721,2])).
% 281.67/282.19 cnf(724,plain,
% 281.67/282.19 (E(f6(f8(x7241),f4(x7241,x7241)),f4(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,156,721,2,3])).
% 281.67/282.19 cnf(728,plain,
% 281.67/282.19 (E(f6(f8(x7281),f4(x7281,x7281)),f6(f6(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[43,723,724,2,3])).
% 281.67/282.19 cnf(732,plain,
% 281.67/282.19 (E(f6(f8(x7321),f4(x7321,x7321)),f7(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,159,728,2,3])).
% 281.67/282.19 cnf(735,plain,
% 281.67/282.19 (E(f7(a5,a5),f6(f8(x7351),f4(x7351,x7351)))),
% 281.67/282.19 inference(scs_inference,[],[732,2])).
% 281.67/282.19 cnf(736,plain,
% 281.67/282.19 (E(f6(f8(x7361),f4(x7361,x7361)),f6(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,164,732,2,3])).
% 281.67/282.19 cnf(739,plain,
% 281.67/282.19 (E(f6(a5,a5),f6(f8(x7391),f4(x7391,x7391)))),
% 281.67/282.19 inference(scs_inference,[],[736,2])).
% 281.67/282.19 cnf(740,plain,
% 281.67/282.19 (E(f6(a5,f4(a5,a5)),f4(f4(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[43,259,736,2,3])).
% 281.67/282.19 cnf(743,plain,
% 281.67/282.19 (E(f6(a5,f4(a5,a5)),f7(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,254,740,2,3])).
% 281.67/282.19 cnf(745,plain,
% 281.67/282.19 (E(f7(a5,a5),f6(a5,f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[743,2])).
% 281.67/282.19 cnf(746,plain,
% 281.67/282.19 (E(f6(a5,f4(f4(a5,a5),f4(a5,a5))),f7(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,743,2,3])).
% 281.67/282.19 cnf(749,plain,
% 281.67/282.19 (E(f6(a5,f4(a5,a5)),f6(f4(f8(x7491),f8(x7491)),f7(x7491,x7491)))),
% 281.67/282.19 inference(scs_inference,[],[43,552,746,2,3])).
% 281.67/282.19 cnf(751,plain,
% 281.67/282.19 (E(f6(f4(f8(x7511),f8(x7511)),f7(x7511,x7511)),f6(a5,f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[749,2])).
% 281.67/282.19 cnf(752,plain,
% 281.67/282.19 (E(f6(f8(x7521),f4(x7521,x7521)),f6(f6(a5,a5),a5))),
% 281.67/282.19 inference(scs_inference,[],[43,749,284,2,3])).
% 281.67/282.19 cnf(755,plain,
% 281.67/282.19 (E(f6(f6(a5,a5),a5),f6(f8(x7551),f4(x7551,x7551)))),
% 281.67/282.19 inference(scs_inference,[],[752,2])).
% 281.67/282.19 cnf(756,plain,
% 281.67/282.19 (E(f6(a5,f4(a5,a5)),f4(a5,f7(a5,x7561)))),
% 281.67/282.19 inference(scs_inference,[],[43,752,555,2,3])).
% 281.67/282.19 cnf(759,plain,
% 281.67/282.19 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f6(f7(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[537,280,756,2,3])).
% 281.67/282.19 cnf(760,plain,
% 281.67/282.19 (E(f6(f7(a5,a5),f4(a5,a5)),f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[759,2])).
% 281.67/282.19 cnf(761,plain,
% 281.67/282.19 (E(f6(a5,f4(a5,a5)),f7(a5,f4(a5,x7611)))),
% 281.67/282.19 inference(scs_inference,[],[43,759,558,2,3])).
% 281.67/282.19 cnf(764,plain,
% 281.67/282.19 (E(f6(f8(x7641),f4(f4(x7641,x7641),f4(x7641,x7641))),f4(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,761,724,2,3])).
% 281.67/282.19 cnf(767,plain,
% 281.67/282.19 (E(f6(f8(x7671),f4(f4(x7671,x7671),f4(x7671,x7671))),f7(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,764,732,2,3])).
% 281.67/282.19 cnf(770,plain,
% 281.67/282.19 (E(f6(f8(x7701),f4(x7701,x7701)),f6(f4(f8(x7702),f8(x7702)),f7(x7702,x7702)))),
% 281.67/282.19 inference(scs_inference,[],[43,767,270,2,3])).
% 281.67/282.19 cnf(773,plain,
% 281.67/282.19 (E(f6(f4(f8(x7731),f8(x7731)),f7(x7731,x7731)),f6(f8(x7732),f4(x7732,x7732)))),
% 281.67/282.19 inference(scs_inference,[],[770,2])).
% 281.67/282.19 cnf(774,plain,
% 281.67/282.19 (E(f6(f7(a5,a5),f4(f4(a5,a5),f4(a5,a5))),a5)),
% 281.67/282.19 inference(scs_inference,[],[43,770,278,2,3])).
% 281.67/282.19 cnf(777,plain,
% 281.67/282.19 (E(f6(f8(x7771),f4(f4(x7771,x7771),f4(x7771,x7771))),f6(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,774,736,2,3])).
% 281.67/282.19 cnf(780,plain,
% 281.67/282.19 (E(f6(f6(a5,a5),f4(a5,a5)),f6(f4(f8(x7801),f8(x7801)),f7(x7801,x7801)))),
% 281.67/282.19 inference(scs_inference,[],[43,777,322,2,3])).
% 281.67/282.19 cnf(782,plain,
% 281.67/282.19 (E(f6(f4(f8(x7821),f8(x7821)),f7(x7821,x7821)),f6(f6(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[780,2])).
% 281.67/282.19 cnf(783,plain,
% 281.67/282.19 (E(f6(f6(a5,f8(x7831)),f4(x7831,x7831)),f4(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,780,438,2,3])).
% 281.67/282.19 cnf(786,plain,
% 281.67/282.19 (E(f4(a5,a5),f6(f6(a5,f8(x7861)),f4(x7861,x7861)))),
% 281.67/282.19 inference(scs_inference,[],[783,2])).
% 281.67/282.19 cnf(787,plain,
% 281.67/282.19 (E(f6(f6(a5,f8(x7871)),f4(x7871,x7871)),f7(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,783,442,2,3])).
% 281.67/282.19 cnf(790,plain,
% 281.67/282.19 (E(f7(a5,a5),f6(f6(a5,f8(x7901)),f4(x7901,x7901)))),
% 281.67/282.19 inference(scs_inference,[],[787,2])).
% 281.67/282.19 cnf(791,plain,
% 281.67/282.19 (E(f6(f6(a5,f8(x7911)),f4(x7911,x7911)),f6(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[43,787,446,2,3])).
% 281.67/282.19 cnf(795,plain,
% 281.67/282.19 (E(f6(a5,f4(a5,a5)),f6(f6(a5,f8(x7951)),f4(x7951,x7951)))),
% 281.67/282.19 inference(scs_inference,[],[43,791,2,3])).
% 281.67/282.19 cnf(797,plain,
% 281.67/282.19 (E(f6(f6(a5,f8(x7971)),f4(x7971,x7971)),f6(a5,f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[795,2])).
% 281.67/282.19 cnf(799,plain,
% 281.67/282.19 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f6(f6(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[642,760,3,2])).
% 281.67/282.19 cnf(801,plain,
% 281.67/282.19 (E(f6(f6(a5,a5),f4(a5,a5)),f6(a5,f6(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[600,639,3,2])).
% 281.67/282.19 cnf(803,plain,
% 281.67/282.19 (E(a5,f6(f6(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[801,295,3,2])).
% 281.67/282.19 cnf(804,plain,
% 281.67/282.19 (E(f6(f4(f8(x8041),f8(x8041)),f7(x8041,x8041)),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[773,629,3])).
% 281.67/282.19 cnf(806,plain,
% 281.67/282.19 (E(f7(f7(a5,a5),f7(a5,a5)),f6(f4(f8(x8061),f8(x8061)),f7(x8061,x8061)))),
% 281.67/282.19 inference(scs_inference,[],[773,629,3,2])).
% 281.67/282.19 cnf(809,plain,
% 281.67/282.19 (E(f6(f6(a5,a5),f4(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[782,806,3,2])).
% 281.67/282.19 cnf(812,plain,
% 281.67/282.19 (E(f6(f7(a5,a5),f4(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[632,649,3,2])).
% 281.67/282.19 cnf(813,plain,
% 281.67/282.19 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f4(f4(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[702,799,3])).
% 281.67/282.19 cnf(816,plain,
% 281.67/282.19 (E(f7(f7(a5,a5),f7(a5,a5)),a5)),
% 281.67/282.19 inference(scs_inference,[],[809,803,3,2])).
% 281.67/282.19 cnf(819,plain,
% 281.67/282.19 (E(f6(f7(a5,a5),f4(a5,a5)),f4(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[636,649,3,2])).
% 281.67/282.19 cnf(821,plain,
% 281.67/282.19 (E(f7(f7(a5,a5),f7(a5,a5)),f4(a5,f7(a5,x8211)))),
% 281.67/282.19 inference(scs_inference,[],[696,809,3,2])).
% 281.67/282.19 cnf(829,plain,
% 281.67/282.19 (E(a5,f7(f4(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[657,710,3,2])).
% 281.67/282.19 cnf(830,plain,
% 281.67/282.19 (E(f4(f6(a5,a5),f6(a5,a5)),a5)),
% 281.67/282.19 inference(scs_inference,[],[661,710,3])).
% 281.67/282.19 cnf(832,plain,
% 281.67/282.19 (E(a5,f4(f6(a5,a5),f6(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[661,710,3,2])).
% 281.67/282.19 cnf(838,plain,
% 281.67/282.19 (E(f6(f7(a5,a5),f4(a5,a5)),f7(a5,a5))),
% 281.67/282.19 inference(scs_inference,[],[735,649,3,2])).
% 281.67/282.19 cnf(840,plain,
% 281.67/282.19 (E(f6(a5,f4(a5,a5)),f6(f7(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[838,745,3,2])).
% 281.67/282.19 cnf(842,plain,
% 281.67/282.19 (E(f7(f7(a5,a5),f7(a5,a5)),f6(a5,f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[812,840,3,2])).
% 281.67/282.19 cnf(844,plain,
% 281.67/282.19 (E(f6(f6(a5,f8(x8441)),f4(x8441,x8441)),f6(f7(a5,a5),f4(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[790,838,3,2])).
% 281.67/282.19 cnf(845,plain,
% 281.67/282.19 (E(f6(f6(a5,f8(x8451)),f4(x8451,x8451)),f4(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.19 inference(scs_inference,[],[819,844,3])).
% 281.67/282.19 cnf(846,plain,
% 281.67/282.19 (E(f4(f7(a5,a5),f7(a5,a5)),f6(f6(a5,f8(x8461)),f4(x8461,x8461)))),
% 281.67/282.19 inference(scs_inference,[],[819,844,3,2])).
% 281.67/282.19 cnf(849,plain,
% 281.67/282.20 (E(a5,f6(a5,f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[677,710,3,2])).
% 281.67/282.20 cnf(855,plain,
% 281.67/282.20 (E(f6(a5,a5),f7(f4(a5,a5),f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[739,654,3])).
% 281.67/282.20 cnf(857,plain,
% 281.67/282.20 (E(f7(f4(a5,a5),f4(a5,a5)),f6(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[739,654,3,2])).
% 281.67/282.20 cnf(862,plain,
% 281.67/282.20 (E(f4(f4(a5,a5),f4(a5,a5)),f6(f6(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[755,650,3,2])).
% 281.67/282.20 cnf(864,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),a5),f4(f4(a5,a5),f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[862,624,3,2])).
% 281.67/282.20 cnf(867,plain,
% 281.67/282.20 (E(a5,f7(f6(a5,a5),f6(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[665,710,3,2])).
% 281.67/282.20 cnf(870,plain,
% 281.67/282.20 (E(f4(f6(a5,a5),f6(a5,a5)),f6(a5,f6(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[720,658,3,2])).
% 281.67/282.20 cnf(873,plain,
% 281.67/282.20 (E(f6(a5,f6(a5,a5)),f4(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[44,870,3,2])).
% 281.67/282.20 cnf(874,plain,
% 281.67/282.20 (E(f6(a5,f7(a5,a5)),a5)),
% 281.67/282.20 inference(scs_inference,[],[673,710,3])).
% 281.67/282.20 cnf(878,plain,
% 281.67/282.20 (E(f7(f4(a5,a5),f4(a5,a5)),f6(f7(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[597,829,3,2])).
% 281.67/282.20 cnf(880,plain,
% 281.67/282.20 (E(f4(f4(a5,a5),f4(a5,a5)),f7(f4(a5,a5),f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[864,878,3,2])).
% 281.67/282.20 cnf(883,plain,
% 281.67/282.20 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f6(a5,f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[669,674,3])).
% 281.67/282.20 cnf(885,plain,
% 281.67/282.20 (E(f6(a5,f4(a5,a5)),f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[669,674,3,2])).
% 281.67/282.20 cnf(897,plain,
% 281.67/282.20 (E(f7(f4(a5,a5),f4(a5,a5)),f7(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[857,254,3])).
% 281.67/282.20 cnf(898,plain,
% 281.67/282.20 (E(f7(a5,a5),f7(f4(a5,a5),f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[857,254,3,2])).
% 281.67/282.20 cnf(899,plain,
% 281.67/282.20 (E(f4(f4(a5,a5),f4(a5,a5)),f7(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[880,897,3])).
% 281.67/282.20 cnf(902,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),a5),f7(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[898,878,3,2])).
% 281.67/282.20 cnf(906,plain,
% 281.67/282.20 (E(f6(a5,f4(a5,a5)),f6(f7(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[902,745,3,2])).
% 281.67/282.20 cnf(908,plain,
% 281.67/282.20 (E(f6(a5,f6(a5,a5)),f6(a5,f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[906,598,3,2])).
% 281.67/282.20 cnf(911,plain,
% 281.67/282.20 (E(f4(f7(a5,a5),f7(a5,a5)),f4(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[786,845,3,2])).
% 281.67/282.20 cnf(914,plain,
% 281.67/282.20 (E(f6(a5,f4(a5,a5)),f4(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[797,846,3,2])).
% 281.67/282.20 cnf(916,plain,
% 281.67/282.20 (E(f4(f7(a5,a5),f7(a5,a5)),f6(f4(f8(x9161),f8(x9161)),f7(x9161,x9161)))),
% 281.67/282.20 inference(scs_inference,[],[751,914,3,2])).
% 281.67/282.20 cnf(918,plain,
% 281.67/282.20 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[842,885,3,2])).
% 281.67/282.20 cnf(919,plain,
% 281.67/282.20 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f4(a5,f7(a5,x9191)))),
% 281.67/282.20 inference(scs_inference,[],[918,821,3])).
% 281.67/282.20 cnf(921,plain,
% 281.67/282.20 (E(a5,f4(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[849,914,3])).
% 281.67/282.20 cnf(922,plain,
% 281.67/282.20 (E(f4(f7(a5,a5),f7(a5,a5)),a5)),
% 281.67/282.20 inference(scs_inference,[],[849,914,3,2])).
% 281.67/282.20 cnf(925,plain,
% 281.67/282.20 (E(f6(a5,a5),f4(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[916,554,3,2])).
% 281.67/282.20 cnf(927,plain,
% 281.67/282.20 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f6(a5,f6(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[908,885,3,2])).
% 281.67/282.20 cnf(928,plain,
% 281.67/282.20 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f4(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[873,927,3])).
% 281.67/282.20 cnf(929,plain,
% 281.67/282.20 (E(f4(a5,a5),f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[873,927,3,2])).
% 281.67/282.20 cnf(932,plain,
% 281.67/282.20 (E(f4(a5,a5),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[929,918,3])).
% 281.67/282.20 cnf(933,plain,
% 281.67/282.20 (E(f7(f7(a5,a5),f7(a5,a5)),f4(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[929,918,3,2])).
% 281.67/282.20 cnf(946,plain,
% 281.67/282.20 (E(f4(f6(a5,a5),f6(a5,a5)),f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[47,929,3])).
% 281.67/282.20 cnf(948,plain,
% 281.67/282.20 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f4(f6(a5,a5),f6(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[47,929,3,2])).
% 281.67/282.20 cnf(964,plain,
% 281.67/282.20 (E(f4(f6(a5,a5),f6(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[47,932,3])).
% 281.67/282.20 cnf(984,plain,
% 281.67/282.20 (E(f6(f8(x9841),x9841),f4(f6(a5,f7(a5,x9842)),f6(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[47,327,3,2])).
% 281.67/282.20 cnf(985,plain,
% 281.67/282.20 (E(f4(f6(a5,a5),f6(a5,a5)),f7(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[47,241,3])).
% 281.67/282.20 cnf(988,plain,
% 281.67/282.20 (~E(f4(f4(a1,a3),a2),f6(f6(a5,a5),f4(a2,a2)))),
% 281.67/282.20 inference(scs_inference,[],[48,567,3])).
% 281.67/282.20 cnf(991,plain,
% 281.67/282.20 (E(f7(f6(a5,a5),f6(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[816,867,3,2])).
% 281.67/282.20 cnf(992,plain,
% 281.67/282.20 (E(f7(f6(a5,a5),f6(a5,a5)),f4(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[933,991,3])).
% 281.67/282.20 cnf(1012,plain,
% 281.67/282.20 (E(f6(f4(a5,a5),a5),a5)),
% 281.67/282.20 inference(scs_inference,[],[53,830,3])).
% 281.67/282.20 cnf(1021,plain,
% 281.67/282.20 (E(f6(f4(a5,a5),a5),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[53,964,3])).
% 281.67/282.20 cnf(1026,plain,
% 281.67/282.20 (E(f6(f4(f7(a5,a5),f7(a5,a5)),f7(a5,a5)),f6(f4(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[53,946,3,2])).
% 281.67/282.20 cnf(1057,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f4(f6(a5,a5),f6(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,948,3])).
% 281.67/282.20 cnf(1060,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f6(f4(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[54,1026,3])).
% 281.67/282.20 cnf(1062,plain,
% 281.67/282.20 (E(f6(f4(a5,a5),a5),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,1026,3,2])).
% 281.67/282.20 cnf(1063,plain,
% 281.67/282.20 (E(f6(a5,a5),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,1062,3])).
% 281.67/282.20 cnf(1065,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f6(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[54,1062,3,2])).
% 281.67/282.20 cnf(1067,plain,
% 281.67/282.20 (E(f4(f7(a5,a5),f7(a5,a5)),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1065,925,3,2])).
% 281.67/282.20 cnf(1068,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),a5)),
% 281.67/282.20 inference(scs_inference,[],[54,537,3])).
% 281.67/282.20 cnf(1073,plain,
% 281.67/282.20 (E(f6(a5,f4(a5,a5)),f6(f8(x10731),f7(x10731,x10731)))),
% 281.67/282.20 inference(scs_inference,[],[54,751,3,2])).
% 281.67/282.20 cnf(1076,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),f4(a5,a5)),f6(f8(x10761),f7(x10761,x10761)))),
% 281.67/282.20 inference(scs_inference,[],[54,782,3,2])).
% 281.67/282.20 cnf(1079,plain,
% 281.67/282.20 (E(f6(f8(x10791),f4(x10791,x10791)),f6(f8(x10792),f7(x10792,x10792)))),
% 281.67/282.20 inference(scs_inference,[],[54,773,3,2])).
% 281.67/282.20 cnf(1082,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),f4(a5,a5)),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,799,3,2])).
% 281.67/282.20 cnf(1084,plain,
% 281.67/282.20 (E(f6(f8(x10841),f4(x10841,x10841)),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1065,739,3,2])).
% 281.67/282.20 cnf(1085,plain,
% 281.67/282.20 (E(f6(f8(x10851),f7(x10851,x10851)),f6(f6(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[54,323,3])).
% 281.67/282.20 cnf(1087,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),a5),f6(f8(x10871),f7(x10871,x10871)))),
% 281.67/282.20 inference(scs_inference,[],[54,323,3,2])).
% 281.67/282.20 cnf(1090,plain,
% 281.67/282.20 (E(f4(a5,f7(a5,x10901)),f6(f8(x10902),f7(x10902,x10902)))),
% 281.67/282.20 inference(scs_inference,[],[54,383,3,2])).
% 281.67/282.20 cnf(1099,plain,
% 281.67/282.20 (E(f6(f8(x10991),f7(x10991,x10991)),f6(f8(x10992),x10992))),
% 281.67/282.20 inference(scs_inference,[],[54,271,3])).
% 281.67/282.20 cnf(1102,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,918,3])).
% 281.67/282.20 cnf(1104,plain,
% 281.67/282.20 (E(f7(f7(a5,a5),f7(a5,a5)),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,918,3,2])).
% 281.67/282.20 cnf(1107,plain,
% 281.67/282.20 (E(f6(a5,f6(a5,a5)),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,927,3,2])).
% 281.67/282.20 cnf(1108,plain,
% 281.67/282.20 (E(f6(f8(x11081),f7(x11081,x11081)),f6(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[54,554,3])).
% 281.67/282.20 cnf(1111,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f4(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[54,928,3])).
% 281.67/282.20 cnf(1113,plain,
% 281.67/282.20 (E(f4(a5,a5),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,928,3,2])).
% 281.67/282.20 cnf(1119,plain,
% 281.67/282.20 (E(f7(f7(a5,a5),f7(a5,a5)),f6(f8(x11191),f7(x11191,x11191)))),
% 281.67/282.20 inference(scs_inference,[],[54,804,3,2])).
% 281.67/282.20 cnf(1122,plain,
% 281.67/282.20 (E(f4(f4(a5,a5),f4(a5,a5)),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,813,3,2])).
% 281.67/282.20 cnf(1125,plain,
% 281.67/282.20 (E(f6(a5,f4(a5,a5)),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,883,3,2])).
% 281.67/282.20 cnf(1131,plain,
% 281.67/282.20 (E(f6(a5,f7(f4(a5,a5),f4(a5,a5))),a5)),
% 281.67/282.20 inference(scs_inference,[],[54,281,3])).
% 281.67/282.20 cnf(1134,plain,
% 281.67/282.20 (E(f6(a5,a5),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,1021,1131,2,3])).
% 281.67/282.20 cnf(1136,plain,
% 281.67/282.20 (E(f7(f7(a5,a5),f7(a5,a5)),f6(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[1134,2])).
% 281.67/282.20 cnf(1137,plain,
% 281.67/282.20 (E(f6(a5,f4(a5,a5)),f6(f6(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1073,1134,1085,2,3])).
% 281.67/282.20 cnf(1139,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),a5),f6(a5,f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1137,2])).
% 281.67/282.20 cnf(1140,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),f4(a5,a5)),f6(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[1076,1108,1137,2,3])).
% 281.67/282.20 cnf(1142,plain,
% 281.67/282.20 (E(f6(a5,a5),f6(f6(a5,a5),f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1140,2])).
% 281.67/282.20 cnf(1143,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),a5),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1125,1139,1140,2,3])).
% 281.67/282.20 cnf(1144,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f6(f6(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1143,2])).
% 281.67/282.20 cnf(1145,plain,
% 281.67/282.20 (E(f6(a5,a5),f6(f7(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1142,637,1143,2,3])).
% 281.67/282.20 cnf(1147,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f6(f8(x11471),f7(x11471,x11471)))),
% 281.67/282.20 inference(scs_inference,[],[1087,1144,1145,2,3])).
% 281.67/282.20 cnf(1148,plain,
% 281.67/282.20 (E(f6(f8(x11481),f7(x11481,x11481)),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1147,2])).
% 281.67/282.20 cnf(1149,plain,
% 281.67/282.20 (E(f4(f7(a5,a5),f7(a5,a5)),f6(f6(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1067,1144,1147,2,3])).
% 281.67/282.20 cnf(1151,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),f4(a5,a5)),f6(f4(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1082,1060,1149,2,3])).
% 281.67/282.20 cnf(1152,plain,
% 281.67/282.20 (E(f6(f4(a5,a5),a5),f6(f6(a5,a5),f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1151,2])).
% 281.67/282.20 cnf(1153,plain,
% 281.67/282.20 (E(f6(f8(x11531),f4(x11531,x11531)),f6(f8(x11532),x11532))),
% 281.67/282.20 inference(scs_inference,[],[1079,1099,1151,2,3])).
% 281.67/282.20 cnf(1155,plain,
% 281.67/282.20 (E(f6(f8(x11551),x11551),f6(f8(x11552),f4(x11552,x11552)))),
% 281.67/282.20 inference(scs_inference,[],[1153,2])).
% 281.67/282.20 cnf(1156,plain,
% 281.67/282.20 (E(f6(f4(a5,a5),a5),f6(f8(x11561),f7(x11561,x11561)))),
% 281.67/282.20 inference(scs_inference,[],[1152,1076,1153,2,3])).
% 281.67/282.20 cnf(1158,plain,
% 281.67/282.20 (E(f6(f8(x11581),x11581),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1084,1155,1156,2,3])).
% 281.67/282.20 cnf(1160,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f6(f8(x11601),x11601))),
% 281.67/282.20 inference(scs_inference,[],[1158,2])).
% 281.67/282.20 cnf(1161,plain,
% 281.67/282.20 (E(f6(f8(x11611),f7(x11611,x11611)),f4(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[1148,1111,1158,2,3])).
% 281.67/282.20 cnf(1162,plain,
% 281.67/282.20 (E(f4(a5,a5),f6(f8(x11621),f7(x11621,x11621)))),
% 281.67/282.20 inference(scs_inference,[],[1161,2])).
% 281.67/282.20 cnf(1163,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f4(f6(a5,f7(a5,x11631)),f6(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1160,984,1161,2,3])).
% 281.67/282.20 cnf(1166,plain,
% 281.67/282.20 (E(f7(f7(a5,a5),f7(a5,a5)),f6(f6(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1104,1144,1163,2,3])).
% 281.67/282.20 cnf(1167,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),a5),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1166,2])).
% 281.67/282.20 cnf(1168,plain,
% 281.67/282.20 (E(f6(a5,f6(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1107,1102,1166,2,3])).
% 281.67/282.20 cnf(1169,plain,
% 281.67/282.20 (E(f7(f7(a5,a5),f7(a5,a5)),f6(a5,f6(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1168,2])).
% 281.67/282.20 cnf(1170,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),a5),f4(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[1167,933,1168,2,3])).
% 281.67/282.20 cnf(1171,plain,
% 281.67/282.20 (E(f4(a5,a5),f6(f6(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1170,2])).
% 281.67/282.20 cnf(1172,plain,
% 281.67/282.20 (E(f7(f7(a5,a5),f7(a5,a5)),f6(f7(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1169,600,1170,2,3])).
% 281.67/282.20 cnf(1173,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),a5),f7(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1172,2])).
% 281.67/282.20 cnf(1174,plain,
% 281.67/282.20 (E(f4(a5,a5),f7(a5,f4(a5,x11741)))),
% 281.67/282.20 inference(scs_inference,[],[1171,410,1172,2,3])).
% 281.67/282.20 cnf(1176,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),a5),f6(f8(x11761),f7(x11761,x11761)))),
% 281.67/282.20 inference(scs_inference,[],[1119,1173,1174,2,3])).
% 281.67/282.20 cnf(1177,plain,
% 281.67/282.20 (E(f6(f8(x11771),f7(x11771,x11771)),f6(f7(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1176,2])).
% 281.67/282.20 cnf(1178,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f4(a5,f7(a5,x11781)))),
% 281.67/282.20 inference(scs_inference,[],[54,1176,919,2,3])).
% 281.67/282.20 cnf(1181,plain,
% 281.67/282.20 (E(f6(f8(x11811),f7(x11811,x11811)),a5)),
% 281.67/282.20 inference(scs_inference,[],[1177,597,1178,2,3])).
% 281.67/282.20 cnf(1183,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f7(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[54,1181,260,2,3])).
% 281.67/282.20 cnf(1185,plain,
% 281.67/282.20 (E(f7(a5,a5),f6(f7(a5,a5),f7(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1183,2])).
% 281.67/282.20 cnf(1186,plain,
% 281.67/282.20 (E(f6(f8(x11861),f7(x11861,x11861)),f6(f7(a5,a5),f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,1183,275,2,3])).
% 281.67/282.20 cnf(1189,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),f7(a5,a5)),f6(f7(a5,a5),f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[54,1186,759,2,3])).
% 281.67/282.20 cnf(1192,plain,
% 281.67/282.20 (E(f4(a5,a5),f6(f4(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1113,1189,1060,2,3])).
% 281.67/282.20 cnf(1194,plain,
% 281.67/282.20 (E(f4(f4(a5,a5),f4(a5,a5)),f4(f6(a5,a5),f6(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1122,1057,1192,2,3])).
% 281.67/282.20 cnf(1196,plain,
% 281.67/282.20 (E(f7(a5,a5),f6(f6(a5,a5),a5))),
% 281.67/282.20 inference(scs_inference,[],[1185,1144,1194,2,3])).
% 281.67/282.20 cnf(1197,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),a5),f7(a5,a5))),
% 281.67/282.20 inference(scs_inference,[],[1196,2])).
% 281.67/282.20 cnf(1277,plain,
% 281.67/282.20 (E(f6(f4(f4(a5,a5),f4(a5,a5)),x12771),f6(f7(a5,a5),x12771))),
% 281.67/282.20 inference(scs_inference,[],[899,10,6])).
% 281.67/282.20 cnf(1302,plain,
% 281.67/282.20 (~E(a3,f4(a1,a3))),
% 281.67/282.20 inference(scs_inference,[],[146,594,9,8,6,7,10,5,4,2])).
% 281.67/282.20 cnf(1303,plain,
% 281.67/282.20 (~E(f6(f6(a5,a5),f4(f4(a1,a3),a2)),a2)),
% 281.67/282.20 inference(scs_inference,[],[28,146,594,571,9,8,6,7,10,5,4,2,3])).
% 281.67/282.20 cnf(1341,plain,
% 281.67/282.20 (~E(f4(a3,f4(f4(a3,a3),a3)),f4(a1,a3))),
% 281.67/282.20 inference(scs_inference,[],[529,1302,832,478,9,8,6,10,7,4,5,2,3])).
% 281.67/282.20 cnf(1387,plain,
% 281.67/282.20 (~E(f4(f4(a1,a2),f4(a1,a2)),f4(f4(a1,a3),a2))),
% 281.67/282.20 inference(scs_inference,[],[921,505,9,6,7,10,4,8,5,2])).
% 281.67/282.20 cnf(1388,plain,
% 281.67/282.20 (E(f7(a5,a5),f6(f8(x13881),f7(x13881,x13881)))),
% 281.67/282.20 inference(scs_inference,[],[921,588,505,1090,9,6,7,10,4,8,5,2,3])).
% 281.67/282.20 cnf(1416,plain,
% 281.67/282.20 (~E(f6(f6(a5,a5),f6(a5,a2)),f4(f4(a1,a3),a2))),
% 281.67/282.20 inference(scs_inference,[],[1068,580,9,6,7,10,8,4,5,2])).
% 281.67/282.20 cnf(1439,plain,
% 281.67/282.20 (E(f7(x14391,a2),f7(x14391,f4(a1,a2)))),
% 281.67/282.20 inference(scs_inference,[],[118,9])).
% 281.67/282.20 cnf(1442,plain,
% 281.67/282.20 (E(f8(a2),f8(f4(a1,a2)))),
% 281.67/282.20 inference(scs_inference,[],[118,9,6,7,10])).
% 281.67/282.20 cnf(1443,plain,
% 281.67/282.20 (E(f7(a2,x14431),f7(f4(a1,a2),x14431))),
% 281.67/282.20 inference(scs_inference,[],[118,9,6,7,10,8])).
% 281.67/282.20 cnf(1445,plain,
% 281.67/282.20 (E(f4(x14451,a2),f4(x14451,f4(a1,a2)))),
% 281.67/282.20 inference(scs_inference,[],[118,9,6,7,10,8,4,5])).
% 281.67/282.20 cnf(1456,plain,
% 281.67/282.20 (~E(f4(f4(a1,a3),f4(a1,a2)),a2)),
% 281.67/282.20 inference(scs_inference,[],[28,1445,550,122,9,7,10,6,4,5,8,2,3])).
% 281.67/282.20 cnf(1458,plain,
% 281.67/282.20 (E(f7(x14581,f4(a1,a2)),f7(x14581,f4(a2,a3)))),
% 281.67/282.20 inference(scs_inference,[],[490,9])).
% 281.67/282.20 cnf(1459,plain,
% 281.67/282.20 (E(f8(f4(a1,a2)),f8(f4(a2,a3)))),
% 281.67/282.20 inference(scs_inference,[],[490,9,10])).
% 281.67/282.20 cnf(1462,plain,
% 281.67/282.20 (E(f4(x14621,f4(a1,a2)),f4(x14621,f4(a2,a3)))),
% 281.67/282.20 inference(scs_inference,[],[490,9,10,6,7,5])).
% 281.67/282.20 cnf(1463,plain,
% 281.67/282.20 (E(f7(f4(a1,a2),x14631),f7(f4(a2,a3),x14631))),
% 281.67/282.20 inference(scs_inference,[],[490,9,10,6,7,5,8])).
% 281.67/282.20 cnf(1466,plain,
% 281.67/282.20 (E(f7(a2,a2),f7(f4(a1,a2),f4(a1,a2)))),
% 281.67/282.20 inference(scs_inference,[],[1439,1443,1456,490,9,10,6,7,5,8,4,2,3])).
% 281.67/282.20 cnf(1476,plain,
% 281.67/282.20 (~E(f6(f6(a5,a5),f4(a2,a2)),f4(f4(a1,a3),a2))),
% 281.67/282.20 inference(scs_inference,[],[988,492,9,6,7,10,8,4,5,2])).
% 281.67/282.20 cnf(1486,plain,
% 281.67/282.20 (E(f7(a2,a2),f7(f4(a1,a2),f4(a2,a3)))),
% 281.67/282.20 inference(scs_inference,[],[1466,1458,496,134,9,6,10,7,8,4,5,2,3])).
% 281.67/282.20 cnf(1506,plain,
% 281.67/282.20 (E(f7(a2,a2),f7(f4(a2,a3),f4(a2,a3)))),
% 281.67/282.20 inference(scs_inference,[],[1486,1463,182,803,9,6,7,10,4,8,5,2,3])).
% 281.67/282.20 cnf(1557,plain,
% 281.67/282.20 (~E(f4(f4(a1,a2),f4(a2,a3)),f4(f4(a1,a3),a2))),
% 281.67/282.20 inference(scs_inference,[],[1462,1387,1341,922,9,10,6,7,8,4,5,2,3])).
% 281.67/282.20 cnf(1567,plain,
% 281.67/282.20 (E(f8(a2),f8(f4(a2,a3)))),
% 281.67/282.20 inference(scs_inference,[],[1442,1459,1557,707,9,10,6,7,4,8,5,2,3])).
% 281.67/282.20 cnf(1579,plain,
% 281.67/282.20 (E(f8(f4(a1,a2)),f8(a2))),
% 281.67/282.20 inference(scs_inference,[],[11,9,10])).
% 281.67/282.20 cnf(1603,plain,
% 281.67/282.20 (E(f4(x16031,a2),f4(x16031,f4(a3,a2)))),
% 281.67/282.20 inference(scs_inference,[],[121,9,10,8,7,6,4,5])).
% 281.67/282.20 cnf(1694,plain,
% 281.67/282.20 (E(f6(x16941,f6(f6(a5,a5),x16942)),f6(x16941,x16942))),
% 281.67/282.20 inference(scs_inference,[],[573,9,8,6,4,10,7])).
% 281.67/282.20 cnf(1723,plain,
% 281.67/282.20 (E(f6(f7(a5,a5),x17231),f6(f6(a5,a5),x17231))),
% 281.67/282.20 inference(scs_inference,[],[252,9,8,4,6])).
% 281.67/282.20 cnf(1753,plain,
% 281.67/282.20 (E(f6(f6(a5,a5),x17531),f6(f4(a5,a5),x17531))),
% 281.67/282.20 inference(scs_inference,[],[272,9,8,7,4,6])).
% 281.67/282.20 cnf(1784,plain,
% 281.67/282.20 (E(f6(f4(a5,a5),x17841),f6(f7(a5,a5),x17841))),
% 281.67/282.20 inference(scs_inference,[],[241,9,8,7,4,10,6])).
% 281.67/282.20 cnf(1797,plain,
% 281.67/282.20 (~E(f6(f4(a5,a5),f6(a5,a2)),f4(f4(a1,a3),a2))),
% 281.67/282.20 inference(scs_inference,[],[1753,1416,1303,710,9,8,7,10,4,6,5,2,3])).
% 281.67/282.20 cnf(1806,plain,
% 281.67/282.20 (~E(f4(f4(a1,a3),a2),f6(f4(a5,a5),f6(a5,a2)))),
% 281.67/282.20 inference(scs_inference,[],[1797,126,9,8,7,10,4,6,5,2])).
% 281.67/282.20 cnf(1809,plain,
% 281.67/282.20 (E(f7(x18091,x18092),f7(x18091,f7(x18092,x18092)))),
% 281.67/282.20 inference(scs_inference,[],[33,9])).
% 281.67/282.20 cnf(1810,plain,
% 281.67/282.20 (E(f7(x18101,x18102),f7(f7(x18101,x18101),x18102))),
% 281.67/282.20 inference(scs_inference,[],[33,9,8])).
% 281.67/282.20 cnf(1813,plain,
% 281.67/282.20 (E(f4(x18131,x18132),f4(f7(x18131,x18131),x18132))),
% 281.67/282.20 inference(scs_inference,[],[33,9,8,7,10,4])).
% 281.67/282.20 cnf(1814,plain,
% 281.67/282.20 (E(f6(x18141,x18142),f6(f7(x18141,x18141),x18142))),
% 281.67/282.20 inference(scs_inference,[],[33,9,8,7,10,4,6])).
% 281.67/282.20 cnf(1836,plain,
% 281.67/282.20 (~E(f4(f7(f4(a1,a3),f4(a1,a3)),a2),a2)),
% 281.67/282.20 inference(scs_inference,[],[28,1813,527,254,9,8,7,10,4,6,5,2,3])).
% 281.67/282.20 cnf(1846,plain,
% 281.67/282.20 (E(f6(a5,a5),f7(f4(a5,a5),f7(f4(a5,a5),f4(a5,a5))))),
% 281.67/282.20 inference(scs_inference,[],[855,1809,1836,36,15,9,8,7,10,4,6,5,2,3])).
% 281.67/282.20 cnf(1849,plain,
% 281.67/282.20 (E(f7(f4(x18491,x18491),x18492),f7(x18491,x18492))),
% 281.67/282.20 inference(scs_inference,[],[14,9,8])).
% 281.67/282.20 cnf(1852,plain,
% 281.67/282.20 (E(f4(f4(x18521,x18521),x18522),f4(x18521,x18522))),
% 281.67/282.20 inference(scs_inference,[],[14,15,9,8,7,10,4])).
% 281.67/282.20 cnf(1854,plain,
% 281.67/282.20 (E(f4(x18541,f4(x18542,x18542)),f4(x18541,x18542))),
% 281.67/282.20 inference(scs_inference,[],[14,15,17,9,8,7,10,4,6,5])).
% 281.67/282.20 cnf(1858,plain,
% 281.67/282.20 (E(f7(x18581,f7(x18582,x18582)),f7(x18581,x18582))),
% 281.67/282.20 inference(scs_inference,[],[15,9])).
% 281.67/282.20 cnf(1859,plain,
% 281.67/282.20 (E(f7(f7(x18591,x18591),x18592),f7(x18591,x18592))),
% 281.67/282.20 inference(scs_inference,[],[15,9,8])).
% 281.67/282.20 cnf(1862,plain,
% 281.67/282.20 (E(f4(f7(x18621,x18621),x18622),f4(x18621,x18622))),
% 281.67/282.20 inference(scs_inference,[],[15,13,9,8,7,10,4])).
% 281.67/282.20 cnf(1863,plain,
% 281.67/282.20 (E(f6(f7(x18631,f4(x18631,x18632)),x18633),f6(x18631,x18633))),
% 281.67/282.20 inference(scs_inference,[],[15,13,20,9,8,7,10,4,6])).
% 281.67/282.20 cnf(1864,plain,
% 281.67/282.20 (E(f4(x18641,f7(x18642,x18642)),f4(x18641,x18642))),
% 281.67/282.20 inference(scs_inference,[],[15,13,20,9,8,7,10,4,6,5])).
% 281.67/282.20 cnf(1872,plain,
% 281.67/282.20 (E(f4(f4(x18721,x18722),x18723),f4(f4(x18722,x18721),x18723))),
% 281.67/282.20 inference(scs_inference,[],[17,9,8,7,10,4])).
% 281.67/282.20 cnf(1873,plain,
% 281.67/282.20 (E(f6(f4(x18731,f7(x18731,x18732)),x18733),f6(x18731,x18733))),
% 281.67/282.20 inference(scs_inference,[],[17,19,9,8,7,10,4,6])).
% 281.67/282.20 cnf(1887,plain,
% 281.67/282.20 (E(f7(x18871,f4(x18872,f7(x18872,x18873))),f7(x18871,x18872))),
% 281.67/282.20 inference(scs_inference,[],[19,9])).
% 281.67/282.20 cnf(1888,plain,
% 281.67/282.20 (E(f7(f4(x18881,f7(x18881,x18882)),x18883),f7(x18881,x18883))),
% 281.67/282.20 inference(scs_inference,[],[19,9,8])).
% 281.67/282.20 cnf(1906,plain,
% 281.67/282.20 (E(f8(x19061),f8(f4(x19061,x19061)))),
% 281.67/282.20 inference(scs_inference,[],[29,9,8,10])).
% 281.67/282.20 cnf(1907,plain,
% 281.67/282.20 (E(f4(x19071,x19072),f4(f4(x19071,x19071),x19072))),
% 281.67/282.20 inference(scs_inference,[],[29,9,8,10,4])).
% 281.67/282.20 cnf(1909,plain,
% 281.67/282.20 (~E(f4(f6(a5,a1),f6(a5,a2)),f4(a1,a3))),
% 281.67/282.20 inference(scs_inference,[],[519,29,9,8,10,4,5,2])).
% 281.67/282.20 cnf(1921,plain,
% 281.67/282.20 (E(f7(f4(a2,a3),f4(a2,a3)),f7(a2,a2))),
% 281.67/282.20 inference(scs_inference,[],[1506,2])).
% 281.67/282.20 cnf(1922,plain,
% 281.67/282.20 (E(f6(f8(x19221),f4(f4(x19221,x19221),f4(x19221,x19221))),f6(f7(a5,a5),f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[43,649,1506,2,3])).
% 281.67/282.20 cnf(1924,plain,
% 281.67/282.20 (E(f7(f4(a1,a2),f4(a2,a3)),f7(a2,a2))),
% 281.67/282.20 inference(scs_inference,[],[1486,2])).
% 281.67/282.20 cnf(1930,plain,
% 281.67/282.20 (E(f8(f4(a2,a3)),f8(a2))),
% 281.67/282.20 inference(scs_inference,[],[1567,2])).
% 281.67/282.20 cnf(1937,plain,
% 281.67/282.20 (E(f6(a5,f4(f7(a5,a5),f7(a5,a5))),a5)),
% 281.67/282.20 inference(scs_inference,[],[43,874,1388,2,3])).
% 281.67/282.20 cnf(1940,plain,
% 281.67/282.20 (E(f6(f4(a5,a5),f4(a5,a5)),a5)),
% 281.67/282.20 inference(scs_inference,[],[43,1012,1277,2,3])).
% 281.67/282.20 cnf(1948,plain,
% 281.67/282.20 (~E(f4(a1,a3),f4(f6(a5,a2),f6(a5,a3)))),
% 281.67/282.20 inference(scs_inference,[],[47,522,1922,2,3])).
% 281.67/282.20 cnf(2061,plain,
% 281.67/282.20 (E(a5,f6(f4(a5,a5),f4(a5,a5)))),
% 281.67/282.20 inference(scs_inference,[],[1940,2])).
% 281.67/282.20 cnf(2188,plain,
% 281.67/282.20 (~E(f4(f4(a1,a3),a2),f4(f4(f4(a1,a2),a1),a2))),
% 281.67/282.20 inference(scs_inference,[],[505,21,1846,2,3])).
% 281.67/282.20 cnf(2238,plain,
% 281.67/282.20 (~E(f4(f4(a1,a3),a2),f7(f7(f7(a2,a2),a2),a2))),
% 281.67/282.20 inference(scs_inference,[],[34,108,1937,2,3])).
% 281.67/282.20 cnf(2262,plain,
% 281.67/282.20 (~E(f4(a1,f4(a3,a2)),a2)),
% 281.67/282.20 inference(scs_inference,[],[28,21,2061,9,7,5,6,8,10,4,3])).
% 281.67/282.20 cnf(2302,plain,
% 281.67/282.20 (~E(f4(a1,f4(a3,a2)),f4(f4(f4(a1,a2),a1),a2))),
% 281.67/282.20 inference(scs_inference,[],[21,1849,2188,9,7,10,6,8,5,4,3])).
% 281.67/282.20 cnf(2322,plain,
% 281.67/282.20 (~E(f4(a1,f4(a3,a2)),f7(f7(f7(a2,a2),a2),a2))),
% 281.67/282.20 inference(scs_inference,[],[21,1852,2238,9,7,5,6,10,8,4,3])).
% 281.67/282.20 cnf(2334,plain,
% 281.67/282.20 (~E(f7(f7(f7(a2,a2),a2),a2),f4(a1,f4(a3,a2)))),
% 281.67/282.20 inference(scs_inference,[],[24,1854,2322,1909,7,9,5,6,10,8,4,3,2])).
% 281.67/282.20 cnf(2342,plain,
% 281.67/282.20 (~E(f7(f7(a2,a2),f7(a2,a2)),f4(a1,f4(a3,a2)))),
% 281.67/282.20 inference(scs_inference,[],[22,1858,2334,5,6,10,9,7,8,4,3])).
% 281.67/282.20 cnf(2344,plain,
% 281.67/282.20 (~E(f4(f4(f4(a1,a2),a1),a2),f4(a1,f4(a3,a2)))),
% 281.67/282.20 inference(scs_inference,[],[22,1858,2334,2302,5,6,10,9,7,8,4,3,2])).
% 281.67/282.20 cnf(2352,plain,
% 281.67/282.20 (~E(f7(a2,f7(a2,f7(a2,a2))),f4(a1,f4(a3,a2)))),
% 281.67/282.20 inference(scs_inference,[],[22,1859,2342,10,9,7,6,5,8,4,3])).
% 281.67/282.20 cnf(2354,plain,
% 281.67/282.20 (~E(f4(f6(a5,a2),f6(a5,a3)),f4(a1,a3))),
% 281.67/282.20 inference(scs_inference,[],[22,1859,1948,2342,10,9,7,6,5,8,4,3,2])).
% 281.67/282.20 cnf(2362,plain,
% 281.67/282.20 (~E(f4(f4(a1,a2),f4(a1,a2)),f4(a1,f4(a3,a2)))),
% 281.67/282.20 inference(scs_inference,[],[21,1862,2344,7,6,5,9,10,4,8,3])).
% 281.67/282.20 cnf(2364,plain,
% 281.67/282.20 (~E(f4(a1,f4(a3,a2)),f7(a2,f7(a2,f7(a2,a2))))),
% 281.67/282.20 inference(scs_inference,[],[21,1862,2344,2352,7,6,5,9,10,4,8,3,2])).
% 281.67/282.20 cnf(2374,plain,
% 281.67/282.20 (~E(f4(a1,f4(a3,a2)),f4(f4(a1,a2),f4(a1,a2)))),
% 281.67/282.20 inference(scs_inference,[],[24,1864,2362,2354,5,9,10,7,6,8,4,3,2])).
% 281.67/282.20 cnf(2382,plain,
% 281.67/282.20 (~E(f4(f4(a3,a2),a1),f4(f4(a1,a2),f4(a1,a2)))),
% 281.67/282.20 inference(scs_inference,[],[17,1921,2374,10,7,6,5,9,4,8,3])).
% 281.67/282.20 cnf(2392,plain,
% 281.67/282.20 (~E(f6(a5,f6(a5,f4(a2,a2))),f4(f4(a1,a3),a2))),
% 281.67/282.20 inference(scs_inference,[],[23,1924,1476,6,5,9,7,10,8,4,3])).
% 281.67/282.20 cnf(2440,plain,
% 281.67/282.20 (~E(f4(f4(a3,a2),a1),f7(a2,f7(a2,f7(a2,a2))))),
% 281.67/282.20 inference(scs_inference,[],[17,1063,2364,7,5,6,10,9,4,8,3])).
% 281.67/282.20 cnf(2451,plain,
% 281.67/282.20 (~E(f7(a2,f7(a2,f7(a2,a2))),f4(f4(a3,a2),a1))),
% 281.67/282.20 inference(scs_inference,[],[16,1162,462,2440,7,10,9,6,5,4,8,3,2])).
% 281.67/282.20 cnf(2471,plain,
% 281.67/282.20 (~E(f4(f4(a1,a2),f4(a1,a2)),f4(f4(a3,a2),a1))),
% 281.67/282.20 inference(scs_inference,[],[18,1906,2451,2382,7,9,5,10,6,4,8,3,2])).
% 281.67/282.20 cnf(2479,plain,
% 281.67/282.20 (~E(f4(a1,f4(a2,f4(a1,a2))),f4(f4(a3,a2),a1))),
% 281.67/282.20 inference(scs_inference,[],[21,1810,2471,10,7,6,5,9,4,8,3])).
% 281.67/282.20 cnf(2491,plain,
% 281.67/282.20 (~E(f4(f4(a3,a2),a1),f4(a1,f4(a2,f4(a1,a2))))),
% 281.67/282.20 inference(scs_inference,[],[13,1814,2479,2392,10,6,7,9,5,4,8,3,2])).
% 281.67/282.20 cnf(2520,plain,
% 281.67/282.20 (~E(a2,f4(a1,f4(a3,a2)))),
% 281.67/282.20 inference(scs_inference,[],[21,1907,2491,2262,10,7,6,5,9,4,8,3,2])).
% 281.67/282.20 cnf(2570,plain,
% 281.67/282.20 (E(f6(x25701,f8(f4(a2,a3))),f6(x25701,f8(a2)))),
% 281.67/282.20 inference(scs_inference,[],[1930,10,7])).
% 281.67/282.20 cnf(2716,plain,
% 281.67/282.20 (~E(f4(a1,f4(a3,a2)),f6(f4(a5,a5),f6(a5,a2)))),
% 281.67/282.20 inference(scs_inference,[],[21,1806,897,10,7,6,5,9,4,8,3])).
% 281.67/282.20 cnf(2728,plain,
% 281.67/282.20 (~E(f6(f4(a5,a5),f6(a5,a2)),f4(a1,f4(a3,a2)))),
% 281.67/282.20 inference(scs_inference,[],[23,1694,2716,911,10,7,5,6,9,4,8,3,2])).
% 281.67/282.20 cnf(2736,plain,
% 281.67/282.20 (~E(f6(f7(a5,a5),f6(a5,a2)),f4(a1,f4(a3,a2)))),
% 281.67/282.20 inference(scs_inference,[],[1784,2728,985,7,10,5,6,9,4,8,3])).
% 281.67/282.20 cnf(2748,plain,
% 281.67/282.20 (~E(f4(a1,f4(a3,a2)),f6(f7(a5,a5),f6(a5,a2)))),
% 281.67/282.20 inference(scs_inference,[],[27,1863,2736,992,7,10,5,6,9,4,8,3,2])).
% 281.67/282.20 cnf(2756,plain,
% 281.67/282.20 (~E(f4(f4(a3,a2),a1),f6(f7(a5,a5),f6(a5,a2)))),
% 281.67/282.20 inference(scs_inference,[],[17,2748,1136,7,10,5,6,9,4,8,3])).
% 281.67/282.20 cnf(2768,plain,
% 281.67/282.20 (~E(f6(f7(a5,a5),f6(a5,a2)),f4(f4(a3,a2),a1))),
% 281.67/282.20 inference(scs_inference,[],[26,1873,2756,1170,7,10,5,6,9,4,8,3,2])).
% 281.67/282.20 cnf(2776,plain,
% 281.67/282.20 (~E(f6(f6(a5,a5),f6(a5,a2)),f4(f4(a3,a2),a1))),
% 281.67/282.20 inference(scs_inference,[],[1723,2768,1197,7,10,5,6,9,4,8,3])).
% 281.67/282.20 cnf(2788,plain,
% 281.67/282.20 (~E(f4(f4(a3,a2),a1),f6(f6(a5,a5),f6(a5,a2)))),
% 281.67/282.20 inference(scs_inference,[],[23,2776,1579,7,10,6,5,9,4,8,3,2])).
% 281.67/282.20 cnf(2927,plain,
% 281.67/282.20 (~E(f4(f4(a1,a3),a2),f7(a2,f7(a2,a2)))),
% 281.67/282.20 inference(scs_inference,[],[34,1858,567,2570,7,5,10,6,9,4,8,2,3])).
% 281.67/282.20 cnf(3110,plain,
% 281.67/282.20 (E(f7(f4(x31101,f7(x31101,x31102)),f4(x31103,f7(x31103,x31104))),f7(x31101,x31103))),
% 281.67/282.20 inference(scs_inference,[],[1887,1888,2927,7,5,10,6,9,4,8,2,3])).
% 281.67/282.20 cnf(3535,plain,
% 281.67/282.20 (~E(f4(f4(a2,a3),a1),f6(f6(a5,a5),f6(a5,a2)))),
% 281.67/282.20 inference(scs_inference,[],[2788,1872,61,2,3])).
% 281.67/282.20 cnf(3697,plain,
% 281.67/282.20 (~E(f4(f4(a2,a3),a1),f6(a5,a2))),
% 281.67/282.20 inference(scs_inference,[],[571,3110,159,3535,6,9,7,5,10,4,8,2,3])).
% 281.67/282.20 cnf(3850,plain,
% 281.67/282.20 ($false),
% 281.67/282.20 inference(scs_inference,[],[118,2520,3697,1603,2,3]),
% 281.67/282.20 ['proof']).
% 281.67/282.20 % SZS output end Proof
% 281.67/282.20 % Total time :280.880000s
%------------------------------------------------------------------------------