%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP154-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 : n020.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:02 EDT 2024
% Result : Unsatisfiable 187.14s 187.52s
% Output : CNFRefutation 187.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : GRP154-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 0.10/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.31 % Computer : n020.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Thu Jun 20 07:47:54 EDT 2024
% 0.11/0.31 % CPUTime :
% 0.17/0.54 start to proof:theBenchmark
% 187.12/187.50 %-------------------------------------------
% 187.12/187.50 % File :CSE---1.7
% 187.12/187.50 % Problem :theBenchmark
% 187.12/187.50 % Transform :cnf
% 187.12/187.50 % Format :tptp:raw
% 187.12/187.50 % Command :java -jar mcs_scs.jar %d %s
% 187.12/187.50
% 187.12/187.50 % Result :Theorem 186.540000s
% 187.12/187.50 % Output :CNFRefutation 186.540000s
% 187.12/187.50 %-------------------------------------------
% 187.14/187.52 %--------------------------------------------------------------------------
% 187.14/187.52 % File : GRP154-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 187.14/187.52 % Domain : Group Theory (Lattice Ordered)
% 187.14/187.52 % Problem : Prove monotonicity axiom using the LUB transformation
% 187.14/187.52 % Version : [Fuc94] (equality) axioms.
% 187.14/187.52 % English : This problem proves the original mononicity axiom from the
% 187.14/187.52 % equational axiomatization.
% 187.14/187.52
% 187.14/187.52 % Refs : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri
% 187.14/187.52 % : [Sch95] Schulz (1995), Explanation Based Learning for Distribu
% 187.14/187.52 % Source : [Sch95]
% 187.14/187.52 % Names : ax_mono1a [Sch95]
% 187.14/187.52
% 187.14/187.52 % Status : Unsatisfiable
% 187.14/187.52 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.06 v6.0.0, 0.10 v5.5.0, 0.05 v5.4.0, 0.00 v5.1.0, 0.07 v5.0.0, 0.14 v4.1.0, 0.18 v4.0.1, 0.14 v4.0.0, 0.15 v3.7.0, 0.11 v3.4.0, 0.00 v2.0.0
% 187.14/187.52 % Syntax : Number of clauses : 17 ( 17 unt; 0 nHn; 2 RR)
% 187.14/187.52 % Number of literals : 17 ( 17 equ; 1 neg)
% 187.14/187.52 % Maximal clause size : 1 ( 1 avg)
% 187.14/187.52 % Maximal term depth : 3 ( 2 avg)
% 187.14/187.52 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 187.14/187.52 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 187.14/187.52 % Number of variables : 33 ( 2 sgn)
% 187.14/187.52 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 187.14/187.52
% 187.14/187.52 % Comments : ORDERING LPO inverse > product > greatest_lower_bound >
% 187.14/187.52 % least_upper_bound > identity > a > b > c
% 187.14/187.52 % : ORDERING LPO greatest_lower_bound > least_upper_bound >
% 187.14/187.52 % inverse > product > identity > a > b > c
% 187.14/187.52 % Bugfixes : v1.2.1 - Duplicate axioms in GRP004-2.ax removed.
% 187.14/187.52 %--------------------------------------------------------------------------
% 187.14/187.52 %----Include equality group theory axioms
% 187.14/187.52 include('Axioms/GRP004-0.ax').
% 187.14/187.52 %----Include Lattice ordered group (equality) axioms
% 187.14/187.52 include('Axioms/GRP004-2.ax').
% 187.14/187.52 %--------------------------------------------------------------------------
% 187.14/187.52 cnf(ax_mono1a_1,hypothesis,
% 187.14/187.52 least_upper_bound(a,b) = b ).
% 187.14/187.52
% 187.14/187.52 cnf(prove_ax_mono1a,negated_conjecture,
% 187.14/187.52 least_upper_bound(multiply(a,c),multiply(b,c)) != multiply(b,c) ).
% 187.14/187.52
% 187.14/187.52 %--------------------------------------------------------------------------
% 187.14/187.52 %-------------------------------------------
% 187.14/187.52 % Proof found
% 187.14/187.52 % SZS status Theorem for theBenchmark
% 187.14/187.52 % SZS output start Proof
% 187.14/187.53 %ClaNum:27(EqnAxiom:10)
% 187.14/187.53 %VarNum:72(SingletonVarNum:33)
% 187.14/187.53 %MaxLitNum:1
% 187.14/187.53 %MaxfuncDepth:2
% 187.14/187.53 %SharedTerms:10
% 187.14/187.53 %goalClause: 27
% 187.14/187.53 %singleGoalClaCount:1
% 187.14/187.53 [11]E(f3(a1,a2),a2)
% 187.14/187.53 [27]~E(f3(f8(a1,a6),f8(a2,a6)),f8(a2,a6))
% 187.14/187.53 [12]E(f8(a4,x121),x121)
% 187.14/187.53 [13]E(f5(x131,x131),x131)
% 187.14/187.53 [14]E(f3(x141,x141),x141)
% 187.14/187.53 [15]E(f8(f7(x151),x151),a4)
% 187.14/187.53 [16]E(f5(x161,x162),f5(x162,x161))
% 187.14/187.53 [17]E(f3(x171,x172),f3(x172,x171))
% 187.14/187.53 [18]E(f5(x181,f3(x181,x182)),x181)
% 187.14/187.53 [19]E(f3(x191,f5(x191,x192)),x191)
% 187.14/187.53 [20]E(f5(f5(x201,x202),x203),f5(x201,f5(x202,x203)))
% 187.14/187.53 [21]E(f3(f3(x211,x212),x213),f3(x211,f3(x212,x213)))
% 187.14/187.53 [22]E(f8(f8(x221,x222),x223),f8(x221,f8(x222,x223)))
% 187.14/187.53 [23]E(f5(f8(x231,x232),f8(x231,x233)),f8(x231,f5(x232,x233)))
% 187.14/187.53 [24]E(f3(f8(x241,x242),f8(x241,x243)),f8(x241,f3(x242,x243)))
% 187.14/187.53 [25]E(f5(f8(x251,x252),f8(x253,x252)),f8(f5(x251,x253),x252))
% 187.14/187.53 [26]E(f3(f8(x261,x262),f8(x263,x262)),f8(f3(x261,x263),x262))
% 187.14/187.53 %EqnAxiom
% 187.14/187.53 [1]E(x11,x11)
% 187.14/187.53 [2]E(x22,x21)+~E(x21,x22)
% 187.14/187.53 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 187.14/187.53 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 187.14/187.53 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 187.14/187.53 [6]~E(x61,x62)+E(f8(x61,x63),f8(x62,x63))
% 187.14/187.53 [7]~E(x71,x72)+E(f8(x73,x71),f8(x73,x72))
% 187.14/187.53 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83))
% 187.14/187.53 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92))
% 187.14/187.53 [10]~E(x101,x102)+E(f7(x101),f7(x102))
% 187.14/187.53
% 187.14/187.53 %-------------------------------------------
% 187.17/187.54 cnf(28,plain,
% 187.17/187.54 (E(x281,f5(x281,x281))),
% 187.17/187.54 inference(scs_inference,[],[13,2])).
% 187.17/187.54 cnf(29,plain,
% 187.17/187.54 (~E(f3(f8(a1,a6),f8(a2,a6)),f5(f8(a2,a6),f8(a2,a6)))),
% 187.17/187.54 inference(scs_inference,[],[27,13,2,3])).
% 187.17/187.54 cnf(31,plain,
% 187.17/187.54 (E(x311,f3(x311,x311))),
% 187.17/187.54 inference(scs_inference,[],[14,2])).
% 187.17/187.54 cnf(32,plain,
% 187.17/187.54 (~E(f3(f8(a1,a6),f8(a2,a6)),f3(f8(a2,a6),f8(a2,a6)))),
% 187.17/187.54 inference(scs_inference,[],[27,14,2,3])).
% 187.17/187.54 cnf(34,plain,
% 187.17/187.54 (~E(f8(a1,a6),f8(a2,a6))),
% 187.17/187.54 inference(scs_inference,[],[27,14,2,3,4])).
% 187.17/187.54 cnf(35,plain,
% 187.17/187.54 (~E(a1,a2)),
% 187.17/187.54 inference(scs_inference,[],[27,14,2,3,4,6])).
% 187.17/187.54 cnf(36,plain,
% 187.17/187.54 (E(x361,f8(a4,x361))),
% 187.17/187.54 inference(scs_inference,[],[12,2])).
% 187.17/187.54 cnf(40,plain,
% 187.17/187.54 (E(f8(x401,x402),f8(x401,f5(x402,x402)))),
% 187.17/187.54 inference(scs_inference,[],[28,23,2,3])).
% 187.17/187.54 cnf(43,plain,
% 187.17/187.54 (E(f8(x431,f5(x432,x432)),f8(x431,x432))),
% 187.17/187.54 inference(scs_inference,[],[40,2])).
% 187.17/187.54 cnf(47,plain,
% 187.17/187.54 (E(f8(x471,x472),f8(x471,f3(x472,x472)))),
% 187.17/187.54 inference(scs_inference,[],[31,24,2,3])).
% 187.17/187.54 cnf(50,plain,
% 187.17/187.54 (E(f8(x501,f3(x502,x502)),f8(x501,x502))),
% 187.17/187.54 inference(scs_inference,[],[47,2])).
% 187.17/187.54 cnf(53,plain,
% 187.17/187.54 (E(f8(f5(x531,x532),x533),f5(f8(x531,x533),f8(x532,x533)))),
% 187.17/187.54 inference(scs_inference,[],[25,2])).
% 187.17/187.54 cnf(54,plain,
% 187.17/187.54 (E(f8(x541,x542),f8(f5(x541,x541),x542))),
% 187.17/187.54 inference(scs_inference,[],[28,25,2,3])).
% 187.17/187.54 cnf(57,plain,
% 187.17/187.54 (E(f8(f5(x571,x571),x572),f8(x571,x572))),
% 187.17/187.54 inference(scs_inference,[],[54,2])).
% 187.17/187.54 cnf(58,plain,
% 187.17/187.54 (~E(f3(f8(a1,a6),f8(a2,a6)),f8(f5(a2,a2),a6))),
% 187.17/187.54 inference(scs_inference,[],[53,54,29,2,3])).
% 187.17/187.54 cnf(60,plain,
% 187.17/187.54 (E(f8(f3(x601,x602),x603),f3(f8(x601,x603),f8(x602,x603)))),
% 187.17/187.54 inference(scs_inference,[],[26,2])).
% 187.17/187.54 cnf(61,plain,
% 187.17/187.54 (E(f8(x611,x612),f8(f3(x611,x611),x612))),
% 187.17/187.54 inference(scs_inference,[],[31,26,2,3])).
% 187.17/187.54 cnf(64,plain,
% 187.17/187.54 (E(f8(f3(x641,x641),x642),f8(x641,x642))),
% 187.17/187.54 inference(scs_inference,[],[61,2])).
% 187.17/187.54 cnf(65,plain,
% 187.17/187.54 (~E(f3(f8(a1,a6),f8(a2,a6)),f8(f3(a2,a2),a6))),
% 187.17/187.55 inference(scs_inference,[],[60,61,32,2,3])).
% 187.17/187.55 cnf(67,plain,
% 187.17/187.55 (E(x671,f5(x671,f3(x671,x672)))),
% 187.17/187.55 inference(scs_inference,[],[18,2])).
% 187.17/187.55 cnf(68,plain,
% 187.17/187.55 (E(f5(x681,x682),f5(x681,f5(x682,f5(x681,x682))))),
% 187.17/187.55 inference(scs_inference,[],[28,18,20,2,3])).
% 187.17/187.55 cnf(71,plain,
% 187.17/187.55 (E(f5(x711,f5(x712,f5(x711,x712))),f5(x711,x712))),
% 187.17/187.55 inference(scs_inference,[],[68,2])).
% 187.17/187.55 cnf(78,plain,
% 187.17/187.55 (E(x781,f3(x781,f5(x781,x782)))),
% 187.17/187.55 inference(scs_inference,[],[19,2])).
% 187.17/187.55 cnf(79,plain,
% 187.17/187.55 (~E(a1,f3(a1,a2))),
% 187.17/187.55 inference(scs_inference,[],[35,19,11,2,3])).
% 187.17/187.55 cnf(80,plain,
% 187.17/187.55 (E(a4,f8(f7(x801),x801))),
% 187.17/187.55 inference(scs_inference,[],[15,2])).
% 187.17/187.55 cnf(83,plain,
% 187.17/187.55 (E(f5(x831,f5(x832,x833)),f5(f5(x831,x832),x833))),
% 187.17/187.55 inference(scs_inference,[],[20,2])).
% 187.17/187.55 cnf(84,plain,
% 187.17/187.55 (E(f5(a4,f3(a4,x841)),f8(f7(x842),x842))),
% 187.17/187.55 inference(scs_inference,[],[80,18,20,2,3])).
% 187.17/187.55 cnf(86,plain,
% 187.17/187.55 (E(f8(f7(x861),x861),f5(a4,f3(a4,x862)))),
% 187.17/187.55 inference(scs_inference,[],[84,2])).
% 187.17/187.55 cnf(87,plain,
% 187.17/187.55 (E(f3(a4,f5(a4,x871)),f8(f7(x872),x872))),
% 187.17/187.55 inference(scs_inference,[],[80,84,19,2,3])).
% 187.17/187.55 cnf(89,plain,
% 187.17/187.55 (E(f8(f7(x891),x891),f3(a4,f5(a4,x892)))),
% 187.17/187.55 inference(scs_inference,[],[87,2])).
% 187.17/187.55 cnf(90,plain,
% 187.17/187.55 (E(f8(f7(x901),f5(x901,x901)),f5(a4,f3(a4,x902)))),
% 187.17/187.55 inference(scs_inference,[],[43,86,87,2,3])).
% 187.17/187.55 cnf(93,plain,
% 187.17/187.55 (E(f5(a4,f3(a4,x931)),f8(f7(x932),f5(x932,x932)))),
% 187.17/187.55 inference(scs_inference,[],[90,2])).
% 187.17/187.55 cnf(94,plain,
% 187.17/187.55 (E(f8(f7(x941),f3(x941,x941)),f3(a4,f5(a4,x942)))),
% 187.17/187.55 inference(scs_inference,[],[50,89,90,2,3])).
% 187.17/187.55 cnf(97,plain,
% 187.17/187.55 (E(f3(a4,f5(a4,x971)),f8(f7(x972),f3(x972,x972)))),
% 187.17/187.55 inference(scs_inference,[],[94,2])).
% 187.17/187.55 cnf(100,plain,
% 187.17/187.55 (E(a4,f8(f7(x1001),f3(x1001,x1001)))),
% 187.17/187.55 inference(scs_inference,[],[78,97,21,2,3])).
% 187.17/187.55 cnf(103,plain,
% 187.17/187.55 (E(f8(f7(x1031),f3(x1031,x1031)),a4)),
% 187.17/187.55 inference(scs_inference,[],[100,2])).
% 187.17/187.55 cnf(104,plain,
% 187.17/187.55 (E(f5(a4,a4),f8(f7(x1041),x1041))),
% 187.17/187.55 inference(scs_inference,[],[80,100,13,2,3])).
% 187.17/187.55 cnf(106,plain,
% 187.17/187.55 (E(f8(f7(x1061),x1061),f5(a4,a4))),
% 187.17/187.55 inference(scs_inference,[],[104,2])).
% 187.17/187.55 cnf(107,plain,
% 187.17/187.55 (E(f8(f5(f7(x1071),f7(x1071)),f3(x1071,x1071)),a4)),
% 187.17/187.55 inference(scs_inference,[],[57,103,104,2,3])).
% 187.17/187.55 cnf(109,plain,
% 187.17/187.55 (E(a4,f8(f5(f7(x1091),f7(x1091)),f3(x1091,x1091)))),
% 187.17/187.55 inference(scs_inference,[],[107,2])).
% 187.17/187.55 cnf(110,plain,
% 187.17/187.55 (E(f8(f3(f7(x1101),f7(x1101)),x1101),f5(a4,a4))),
% 187.17/187.55 inference(scs_inference,[],[64,106,107,2,3])).
% 187.17/187.55 cnf(113,plain,
% 187.17/187.55 (E(f5(a4,a4),f8(f3(f7(x1131),f7(x1131)),x1131))),
% 187.17/187.55 inference(scs_inference,[],[110,2])).
% 187.17/187.55 cnf(114,plain,
% 187.17/187.55 (E(f8(f7(x1141),f3(x1141,x1141)),f8(f5(f7(x1142),f7(x1142)),f3(x1142,x1142)))),
% 187.17/187.55 inference(scs_inference,[],[109,103,110,2,3])).
% 187.17/187.55 cnf(115,plain,
% 187.17/187.55 (E(f8(f5(f7(x1151),f7(x1151)),f3(x1151,x1151)),f8(f7(x1152),f3(x1152,x1152)))),
% 187.17/187.55 inference(scs_inference,[],[114,2])).
% 187.17/187.55 cnf(116,plain,
% 187.17/187.55 (E(f8(f7(x1161),f5(x1161,x1161)),f5(a4,a4))),
% 187.17/187.55 inference(scs_inference,[],[43,106,114,2,3])).
% 187.17/187.55 cnf(119,plain,
% 187.17/187.55 (E(f5(a4,a4),f8(f7(x1191),f5(x1191,x1191)))),
% 187.17/187.55 inference(scs_inference,[],[116,2])).
% 187.17/187.55 cnf(120,plain,
% 187.17/187.55 (E(f8(f7(x1201),f3(x1201,x1201)),f5(a4,f3(a4,x1202)))),
% 187.17/187.55 inference(scs_inference,[],[50,86,116,2,3])).
% 187.17/187.55 cnf(123,plain,
% 187.17/187.55 (E(f5(a4,f3(a4,x1231)),f8(f7(x1232),f3(x1232,x1232)))),
% 187.17/187.55 inference(scs_inference,[],[120,2])).
% 187.17/187.55 cnf(124,plain,
% 187.17/187.55 (E(f8(f5(f7(x1241),f7(x1241)),x1241),f5(a4,a4))),
% 187.17/187.55 inference(scs_inference,[],[57,106,120,2,3])).
% 187.17/187.55 cnf(128,plain,
% 187.17/187.55 (E(f8(f7(x1281),f3(x1281,x1281)),f8(f7(x1282),x1282))),
% 187.17/187.55 inference(scs_inference,[],[103,80,124,2,3])).
% 187.17/187.55 cnf(129,plain,
% 187.17/187.55 (E(f8(f7(x1291),x1291),f8(f7(x1292),f3(x1292,x1292)))),
% 187.17/187.55 inference(scs_inference,[],[128,2])).
% 187.17/187.55 cnf(130,plain,
% 187.17/187.55 (E(f8(f5(f7(x1301),f7(x1301)),f3(x1301,x1301)),f8(f7(x1302),x1302))),
% 187.17/187.55 inference(scs_inference,[],[115,128,2,3])).
% 187.17/187.55 cnf(132,plain,
% 187.17/187.55 (E(f8(f7(x1321),x1321),f8(f5(f7(x1322),f7(x1322)),f3(x1322,x1322)))),
% 187.17/187.55 inference(scs_inference,[],[130,2])).
% 187.17/187.55 cnf(133,plain,
% 187.17/187.55 (E(f5(a4,a4),f5(a4,f3(a4,x1331)))),
% 187.17/187.55 inference(scs_inference,[],[119,130,90,2,3])).
% 187.17/187.55 cnf(135,plain,
% 187.17/187.55 (E(f5(a4,f3(a4,x1351)),f5(a4,a4))),
% 187.17/187.55 inference(scs_inference,[],[133,2])).
% 187.17/187.55 cnf(137,plain,
% 187.17/187.55 (E(f8(x1371,f8(x1372,x1373)),f8(f8(x1371,x1372),x1373))),
% 187.17/187.55 inference(scs_inference,[],[22,2])).
% 187.17/187.55 cnf(140,plain,
% 187.17/187.55 (E(a2,f3(a1,a2))),
% 187.17/187.55 inference(scs_inference,[],[11,2])).
% 187.17/187.55 cnf(141,plain,
% 187.17/187.55 (E(f8(f3(f7(x1411),f7(x1411)),f5(x1411,x1411)),f5(a4,a4))),
% 187.17/187.55 inference(scs_inference,[],[64,116,11,2,3])).
% 187.17/187.55 cnf(143,plain,
% 187.17/187.55 (E(f5(a4,a4),f8(f3(f7(x1431),f7(x1431)),f5(x1431,x1431)))),
% 187.17/187.55 inference(scs_inference,[],[141,2])).
% 187.17/187.55 cnf(144,plain,
% 187.17/187.55 (E(f8(f7(x1441),f5(x1441,x1441)),f8(f5(f7(x1442),f7(x1442)),f3(x1442,x1442)))),
% 187.17/187.55 inference(scs_inference,[],[132,43,141,2,3])).
% 187.17/187.55 cnf(147,plain,
% 187.17/187.55 (E(f8(f5(f7(x1471),f7(x1471)),f3(x1471,x1471)),f8(f7(x1472),f5(x1472,x1472)))),
% 187.17/187.55 inference(scs_inference,[],[144,2])).
% 187.17/187.55 cnf(148,plain,
% 187.17/187.55 (E(f8(f7(x1481),f3(x1481,x1481)),f5(a4,a4))),
% 187.17/187.55 inference(scs_inference,[],[50,106,144,2,3])).
% 187.17/187.55 cnf(151,plain,
% 187.17/187.55 (E(f5(a4,a4),f8(f7(x1511),f3(x1511,x1511)))),
% 187.17/187.55 inference(scs_inference,[],[148,2])).
% 187.17/187.55 cnf(152,plain,
% 187.17/187.55 (E(f8(f7(x1521),x1521),f8(f7(x1522),f5(x1522,x1522)))),
% 187.17/187.55 inference(scs_inference,[],[147,132,148,2,3])).
% 187.17/187.55 cnf(154,plain,
% 187.17/187.55 (E(f8(f7(x1541),f5(x1541,x1541)),f8(f7(x1542),x1542))),
% 187.17/187.55 inference(scs_inference,[],[152,2])).
% 187.17/187.55 cnf(155,plain,
% 187.17/187.55 (E(a4,f8(f7(x1551),f5(x1551,x1551)))),
% 187.17/187.55 inference(scs_inference,[],[147,109,152,2,3])).
% 187.17/187.55 cnf(157,plain,
% 187.17/187.55 (E(f8(f7(x1571),f5(x1571,x1571)),a4)),
% 187.17/187.55 inference(scs_inference,[],[155,2])).
% 187.17/187.55 cnf(158,plain,
% 187.17/187.55 (E(f8(f7(x1581),f5(x1581,x1581)),f8(f7(x1582),f3(x1582,x1582)))),
% 187.17/187.55 inference(scs_inference,[],[129,154,155,2,3])).
% 187.17/187.55 cnf(160,plain,
% 187.17/187.55 (E(f8(f7(x1601),f3(x1601,x1601)),f8(f7(x1602),f5(x1602,x1602)))),
% 187.17/187.55 inference(scs_inference,[],[158,2])).
% 187.17/187.55 cnf(161,plain,
% 187.17/187.55 (E(f8(f7(x1611),f5(x1611,x1611)),f3(a4,f5(a4,x1612)))),
% 187.17/187.55 inference(scs_inference,[],[154,89,158,2,3])).
% 187.17/187.55 cnf(163,plain,
% 187.17/187.55 (E(f3(a4,f5(a4,x1631)),f8(f7(x1632),f5(x1632,x1632)))),
% 187.17/187.55 inference(scs_inference,[],[161,2])).
% 187.17/187.55 cnf(164,plain,
% 187.17/187.55 (E(f5(a4,a4),f8(f5(f7(x1641),f7(x1641)),f3(x1641,x1641)))),
% 187.17/187.55 inference(scs_inference,[],[151,161,114,2,3])).
% 187.17/187.55 cnf(166,plain,
% 187.17/187.55 (E(f8(f5(f7(x1661),f7(x1661)),f3(x1661,x1661)),f5(a4,a4))),
% 187.17/187.55 inference(scs_inference,[],[164,2])).
% 187.17/187.55 cnf(167,plain,
% 187.17/187.55 (E(f5(a4,f3(a4,x1671)),f3(a4,f5(a4,x1672)))),
% 187.17/187.55 inference(scs_inference,[],[123,164,94,2,3])).
% 187.17/187.55 cnf(169,plain,
% 187.17/187.55 (E(f3(a4,f5(a4,x1691)),f5(a4,f3(a4,x1692)))),
% 187.17/187.55 inference(scs_inference,[],[167,2])).
% 187.17/187.55 cnf(170,plain,
% 187.17/187.55 (E(f8(f5(f7(x1701),f7(x1701)),f3(x1701,x1701)),f5(a4,f3(a4,x1702)))),
% 187.17/187.55 inference(scs_inference,[],[115,167,120,2,3])).
% 187.17/187.55 cnf(172,plain,
% 187.17/187.55 (E(f5(a4,f3(a4,x1721)),f8(f5(f7(x1722),f7(x1722)),f3(x1722,x1722)))),
% 187.17/187.55 inference(scs_inference,[],[170,2])).
% 187.17/187.55 cnf(189,plain,
% 187.17/187.55 (E(a4,f8(f3(f7(x1891),f7(x1891)),x1891))),
% 187.17/187.55 inference(scs_inference,[],[64,15,3,2])).
% 187.17/187.55 cnf(192,plain,
% 187.17/187.55 (E(f5(a2,f3(a2,x1921)),f3(a1,a2))),
% 187.17/187.55 inference(scs_inference,[],[11,67,3,2])).
% 187.17/187.55 cnf(193,plain,
% 187.17/187.55 (~E(a1,f5(a2,f3(a2,x1931)))),
% 187.17/187.55 inference(scs_inference,[],[192,79,3])).
% 187.17/187.55 cnf(202,plain,
% 187.17/187.56 (E(f8(f3(f7(x2021),f7(x2021)),f5(x2021,x2021)),f8(a4,f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[12,143,3,2])).
% 187.17/187.56 cnf(205,plain,
% 187.17/187.56 (E(f5(a4,a4),f8(a4,f5(a4,f3(a4,x2051))))),
% 187.17/187.56 inference(scs_inference,[],[12,135,3,2])).
% 187.17/187.56 cnf(211,plain,
% 187.17/187.56 (E(f8(f3(f7(x2111),f7(x2111)),x2111),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[12,189,3,2])).
% 187.17/187.56 cnf(218,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x2181),f5(x2181,x2181))),a4)),
% 187.17/187.56 inference(scs_inference,[],[12,157,3])).
% 187.17/187.56 cnf(220,plain,
% 187.17/187.56 (E(a4,f8(a4,f8(f7(x2201),f5(x2201,x2201))))),
% 187.17/187.56 inference(scs_inference,[],[12,157,3,2])).
% 187.17/187.56 cnf(223,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x2231),f5(x2231,x2231))),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[12,220,3,2])).
% 187.17/187.56 cnf(224,plain,
% 187.17/187.56 (E(f8(a4,a4),f8(f5(f7(x2241),f7(x2241)),f3(x2241,x2241)))),
% 187.17/187.56 inference(scs_inference,[],[12,109,3])).
% 187.17/187.56 cnf(226,plain,
% 187.17/187.56 (E(f8(f5(f7(x2261),f7(x2261)),f3(x2261,x2261)),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[12,109,3,2])).
% 187.17/187.56 cnf(227,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x2271),x2271)),f5(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[12,106,3])).
% 187.17/187.56 cnf(230,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x2301),f3(x2301,x2301))),a4)),
% 187.17/187.56 inference(scs_inference,[],[12,103,3])).
% 187.17/187.56 cnf(232,plain,
% 187.17/187.56 (E(a4,f8(a4,f8(f7(x2321),f3(x2321,x2321))))),
% 187.17/187.56 inference(scs_inference,[],[12,103,3,2])).
% 187.17/187.56 cnf(235,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x2351),f3(x2351,x2351))),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[12,232,3,2])).
% 187.17/187.56 cnf(236,plain,
% 187.17/187.56 (E(f8(a4,a4),f8(f7(x2361),x2361))),
% 187.17/187.56 inference(scs_inference,[],[12,80,3])).
% 187.17/187.56 cnf(238,plain,
% 187.17/187.56 (E(f8(f7(x2381),x2381),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[12,80,3,2])).
% 187.17/187.56 cnf(239,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x2391),x2391)),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[12,238,3])).
% 187.17/187.56 cnf(244,plain,
% 187.17/187.56 (E(f8(f7(x2441),x2441),f8(a4,f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[12,236,3,2])).
% 187.17/187.56 cnf(250,plain,
% 187.17/187.56 (E(f8(f5(f7(x2501),f7(x2501)),f3(x2501,x2501)),f8(a4,f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[12,164,3,2])).
% 187.17/187.56 cnf(251,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x2511),f3(x2511,x2511))),f5(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[12,148,3])).
% 187.17/187.56 cnf(256,plain,
% 187.17/187.56 (E(f5(a4,f3(a4,x2561)),f8(a4,f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[12,133,3,2])).
% 187.17/187.56 cnf(263,plain,
% 187.17/187.56 (E(f8(a4,a4),f8(f7(x2631),f3(x2631,x2631)))),
% 187.17/187.56 inference(scs_inference,[],[12,100,3])).
% 187.17/187.56 cnf(265,plain,
% 187.17/187.56 (E(f8(f7(x2651),f3(x2651,x2651)),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[12,100,3,2])).
% 187.17/187.56 cnf(266,plain,
% 187.17/187.56 (E(f8(a4,f8(a4,a4)),f8(f7(x2661),f3(x2661,x2661)))),
% 187.17/187.56 inference(scs_inference,[],[12,263,3])).
% 187.17/187.56 cnf(268,plain,
% 187.17/187.56 (E(f8(f7(x2681),f3(x2681,x2681)),f8(a4,f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[12,263,3,2])).
% 187.17/187.56 cnf(269,plain,
% 187.17/187.56 (E(f8(a4,a4),f8(f7(x2691),f5(x2691,x2691)))),
% 187.17/187.56 inference(scs_inference,[],[12,155,3])).
% 187.17/187.56 cnf(271,plain,
% 187.17/187.56 (E(f8(f7(x2711),f5(x2711,x2711)),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[12,155,3,2])).
% 187.17/187.56 cnf(272,plain,
% 187.17/187.56 (E(f8(a4,f8(a4,a4)),f8(f7(x2721),f5(x2721,x2721)))),
% 187.17/187.56 inference(scs_inference,[],[12,269,3])).
% 187.17/187.56 cnf(274,plain,
% 187.17/187.56 (E(f8(f7(x2741),f5(x2741,x2741)),f8(a4,f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[12,269,3,2])).
% 187.17/187.56 cnf(275,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x2751),x2751)),a4)),
% 187.17/187.56 inference(scs_inference,[],[12,15,3])).
% 187.17/187.56 cnf(277,plain,
% 187.17/187.56 (E(a4,f8(a4,f8(f7(x2771),x2771)))),
% 187.17/187.56 inference(scs_inference,[],[12,15,3,2])).
% 187.17/187.56 cnf(280,plain,
% 187.17/187.56 (E(f8(f3(f7(x2801),f7(x2801)),f5(x2801,x2801)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[13,143,3,2])).
% 187.17/187.56 cnf(283,plain,
% 187.17/187.56 (E(f8(f7(x2831),f3(x2831,x2831)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[13,151,3,2])).
% 187.17/187.56 cnf(286,plain,
% 187.17/187.56 (E(f8(f7(x2861),f5(x2861,x2861)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[13,119,3,2])).
% 187.17/187.56 cnf(289,plain,
% 187.17/187.56 (E(f8(f7(x2891),f5(x2891,x2891)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[13,269,3,2])).
% 187.17/187.56 cnf(292,plain,
% 187.17/187.56 (E(f8(f7(x2921),f3(x2921,x2921)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[13,263,3,2])).
% 187.17/187.56 cnf(295,plain,
% 187.17/187.56 (E(f8(f7(x2951),x2951),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[13,236,3,2])).
% 187.17/187.56 cnf(298,plain,
% 187.17/187.56 (E(f8(f5(f7(x2981),f7(x2981)),f3(x2981,x2981)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[13,224,3,2])).
% 187.17/187.56 cnf(301,plain,
% 187.17/187.56 (E(f8(f5(f7(x3011),f7(x3011)),f3(x3011,x3011)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[13,164,3,2])).
% 187.17/187.56 cnf(304,plain,
% 187.17/187.56 (E(f5(a4,f3(a4,x3041)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[13,133,3,2])).
% 187.17/187.56 cnf(310,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x3101),x3101)),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[14,277,3,2])).
% 187.17/187.56 cnf(316,plain,
% 187.17/187.56 (E(f8(f3(f7(x3161),f7(x3161)),x3161),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[14,189,3,2])).
% 187.17/187.56 cnf(319,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x3191),f5(x3191,x3191))),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[14,220,3,2])).
% 187.17/187.56 cnf(322,plain,
% 187.17/187.56 (E(f8(a4,f8(f7(x3221),f3(x3221,x3221))),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[14,232,3,2])).
% 187.17/187.56 cnf(325,plain,
% 187.17/187.56 (E(f8(f3(f7(x3251),f7(x3251)),f5(x3251,x3251)),f3(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,143,3,2])).
% 187.17/187.56 cnf(328,plain,
% 187.17/187.56 (E(f8(f7(x3281),f3(x3281,x3281)),f3(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,151,3,2])).
% 187.17/187.56 cnf(332,plain,
% 187.17/187.56 (E(f3(a4,a4),f8(f5(f7(x3321),f7(x3321)),f3(x3321,x3321)))),
% 187.17/187.56 inference(scs_inference,[],[14,109,3])).
% 187.17/187.56 cnf(334,plain,
% 187.17/187.56 (E(f8(f5(f7(x3341),f7(x3341)),f3(x3341,x3341)),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[14,109,3,2])).
% 187.17/187.56 cnf(343,plain,
% 187.17/187.56 (E(f8(f5(f7(x3431),f7(x3431)),f3(x3431,x3431)),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,332,3,2])).
% 187.17/187.56 cnf(346,plain,
% 187.17/187.56 (E(f8(f7(x3461),f5(x3461,x3461)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,269,3,2])).
% 187.17/187.56 cnf(349,plain,
% 187.17/187.56 (E(f8(f7(x3491),f3(x3491,x3491)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,263,3,2])).
% 187.17/187.56 cnf(352,plain,
% 187.17/187.56 (E(f8(f7(x3521),x3521),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,236,3,2])).
% 187.17/187.56 cnf(355,plain,
% 187.17/187.56 (E(f8(f5(f7(x3551),f7(x3551)),f3(x3551,x3551)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,224,3,2])).
% 187.17/187.56 cnf(358,plain,
% 187.17/187.56 (E(f8(f5(f7(x3581),f7(x3581)),f3(x3581,x3581)),f3(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,164,3,2])).
% 187.17/187.56 cnf(361,plain,
% 187.17/187.56 (E(f5(a4,f3(a4,x3611)),f3(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,133,3,2])).
% 187.17/187.56 cnf(365,plain,
% 187.17/187.56 (E(f3(a4,a4),f8(f7(x3651),f3(x3651,x3651)))),
% 187.17/187.56 inference(scs_inference,[],[14,100,3])).
% 187.17/187.56 cnf(367,plain,
% 187.17/187.56 (E(f8(f7(x3671),f3(x3671,x3671)),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[14,100,3,2])).
% 187.17/187.56 cnf(370,plain,
% 187.17/187.56 (E(f8(f7(x3701),f3(x3701,x3701)),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,365,3,2])).
% 187.17/187.56 cnf(371,plain,
% 187.17/187.56 (E(f3(a4,a4),f8(f7(x3711),f5(x3711,x3711)))),
% 187.17/187.56 inference(scs_inference,[],[14,155,3])).
% 187.17/187.56 cnf(376,plain,
% 187.17/187.56 (E(f8(f7(x3761),f5(x3761,x3761)),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[14,371,3,2])).
% 187.17/187.56 cnf(377,plain,
% 187.17/187.56 (E(f5(a4,f3(a4,x3771)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[298,172,3])).
% 187.17/187.56 cnf(379,plain,
% 187.17/187.56 (E(f5(f8(a4,a4),f8(a4,a4)),f5(a4,f3(a4,x3791)))),
% 187.17/187.56 inference(scs_inference,[],[298,172,3,2])).
% 187.17/187.56 cnf(382,plain,
% 187.17/187.56 (E(f3(f8(a4,a4),f8(a4,a4)),f5(a4,f3(a4,x3821)))),
% 187.17/187.56 inference(scs_inference,[],[355,172,3,2])).
% 187.17/187.56 cnf(383,plain,
% 187.17/187.56 (E(f5(a4,a4),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[316,113,3])).
% 187.17/187.56 cnf(385,plain,
% 187.17/187.56 (E(f3(a4,a4),f5(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[316,113,3,2])).
% 187.17/187.56 cnf(386,plain,
% 187.17/187.56 (E(f5(a4,a4),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[211,113,3])).
% 187.17/187.56 cnf(388,plain,
% 187.17/187.56 (E(f8(a4,a4),f5(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[211,113,3,2])).
% 187.17/187.56 cnf(389,plain,
% 187.17/187.56 (E(f5(a4,f5(a4,f5(a4,a4))),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[71,383,3])).
% 187.17/187.56 cnf(392,plain,
% 187.17/187.56 (E(f5(f8(a4,a4),f8(a4,a4)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[304,379,3])).
% 187.17/187.56 cnf(394,plain,
% 187.17/187.56 (E(f5(f5(a4,a4),f5(a4,a4)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[304,379,3,2])).
% 187.17/187.56 cnf(395,plain,
% 187.17/187.56 (E(f8(f3(f7(x3951),f7(x3951)),f5(x3951,x3951)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[280,394,3])).
% 187.17/187.56 cnf(396,plain,
% 187.17/187.56 (E(f5(f8(a4,a4),f8(a4,a4)),f8(f3(f7(x3961),f7(x3961)),f5(x3961,x3961)))),
% 187.17/187.56 inference(scs_inference,[],[280,394,3,2])).
% 187.17/187.56 cnf(399,plain,
% 187.17/187.56 (E(f3(f5(a4,a4),f5(a4,a4)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[325,396,3,2])).
% 187.17/187.56 cnf(402,plain,
% 187.17/187.56 (E(f8(a4,f5(a4,a4)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[256,382,3,2])).
% 187.17/187.56 cnf(403,plain,
% 187.17/187.56 (E(f3(a4,f5(a4,x4031)),f3(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[361,169,3])).
% 187.17/187.56 cnf(405,plain,
% 187.17/187.56 (E(f3(f5(a4,a4),f5(a4,a4)),f3(a4,f5(a4,x4051)))),
% 187.17/187.56 inference(scs_inference,[],[361,169,3,2])).
% 187.17/187.56 cnf(407,plain,
% 187.17/187.56 (E(f3(a4,f5(a4,x4071)),f8(f5(f7(x4072),f7(x4072)),f3(x4072,x4072)))),
% 187.17/187.56 inference(scs_inference,[],[358,405,3,2])).
% 187.17/187.56 cnf(410,plain,
% 187.17/187.56 (E(f5(f5(a4,a4),f5(a4,a4)),f3(a4,f5(a4,x4101)))),
% 187.17/187.56 inference(scs_inference,[],[301,407,3,2])).
% 187.17/187.56 cnf(411,plain,
% 187.17/187.56 (E(f3(a4,f5(a4,x4111)),f8(a4,f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[250,407,3])).
% 187.17/187.56 cnf(413,plain,
% 187.17/187.56 (E(f8(a4,f5(a4,a4)),f3(a4,f5(a4,x4131)))),
% 187.17/187.56 inference(scs_inference,[],[250,407,3,2])).
% 187.17/187.56 cnf(415,plain,
% 187.17/187.56 (E(f8(a4,f5(a4,f3(a4,x4151))),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[385,205,3,2])).
% 187.17/187.56 cnf(416,plain,
% 187.17/187.56 (E(f5(a4,f3(a4,x4161)),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[36,415,3])).
% 187.17/187.56 cnf(418,plain,
% 187.17/187.56 (E(f3(a4,a4),f5(a4,f3(a4,x4181)))),
% 187.17/187.56 inference(scs_inference,[],[416,2])).
% 187.17/187.56 cnf(419,plain,
% 187.17/187.56 (E(f8(f7(x4191),f5(x4191,x4191)),f8(f3(f7(x4192),f7(x4192)),f5(x4192,x4192)))),
% 187.17/187.56 inference(scs_inference,[],[289,396,416,2,3])).
% 187.17/187.56 cnf(420,plain,
% 187.17/187.56 (E(f8(f3(f7(x4201),f7(x4201)),f5(x4201,x4201)),f8(f7(x4202),f5(x4202,x4202)))),
% 187.17/187.56 inference(scs_inference,[],[419,2])).
% 187.17/187.56 cnf(421,plain,
% 187.17/187.56 (E(f3(a4,a4),f8(a4,f5(a4,a4)))),
% 187.17/187.56 inference(scs_inference,[],[418,256,419,2,3])).
% 187.17/187.56 cnf(423,plain,
% 187.17/187.56 (E(f8(a4,f5(a4,a4)),f3(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[421,2])).
% 187.17/187.56 cnf(424,plain,
% 187.17/187.56 (E(f8(a4,a4),f8(a4,f5(a4,f3(a4,x4241))))),
% 187.17/187.56 inference(scs_inference,[],[388,205,421,2,3])).
% 187.17/187.56 cnf(425,plain,
% 187.17/187.56 (E(f8(a4,f5(a4,f3(a4,x4251))),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[424,2])).
% 187.17/187.56 cnf(426,plain,
% 187.17/187.56 (E(f8(f7(x4261),f3(x4261,x4261)),f8(f3(f7(x4262),f7(x4262)),f5(x4262,x4262)))),
% 187.17/187.56 inference(scs_inference,[],[292,396,424,2,3])).
% 187.17/187.56 cnf(427,plain,
% 187.17/187.56 (E(f8(f3(f7(x4271),f7(x4271)),f5(x4271,x4271)),f8(f7(x4272),f3(x4272,x4272)))),
% 187.17/187.56 inference(scs_inference,[],[426,2])).
% 187.17/187.56 cnf(428,plain,
% 187.17/187.56 (E(f5(a4,f3(a4,x4281)),f8(a4,a4))),
% 187.17/187.56 inference(scs_inference,[],[425,36,426,2,3])).
% 187.17/187.57 cnf(430,plain,
% 187.17/187.57 (E(f8(a4,a4),f5(a4,f3(a4,x4301)))),
% 187.17/187.57 inference(scs_inference,[],[428,2])).
% 187.17/187.57 cnf(431,plain,
% 187.17/187.57 (E(f8(f3(f7(x4311),f7(x4311)),f5(x4311,x4311)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[349,427,428,2,3])).
% 187.17/187.57 cnf(433,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f8(f3(f7(x4331),f7(x4331)),f5(x4331,x4331)))),
% 187.17/187.57 inference(scs_inference,[],[431,2])).
% 187.17/187.57 cnf(434,plain,
% 187.17/187.57 (E(f8(f3(f7(x4341),f7(x4341)),f5(x4341,x4341)),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[367,427,431,2,3])).
% 187.17/187.57 cnf(436,plain,
% 187.17/187.57 (E(f3(a4,a4),f8(f3(f7(x4361),f7(x4361)),f5(x4361,x4361)))),
% 187.17/187.57 inference(scs_inference,[],[434,2])).
% 187.17/187.57 cnf(437,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[433,280,434,2,3])).
% 187.17/187.57 cnf(439,plain,
% 187.17/187.57 (E(f5(f5(a4,a4),f5(a4,a4)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[437,2])).
% 187.17/187.57 cnf(440,plain,
% 187.17/187.57 (E(f3(a4,a4),f3(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[436,325,437,2,3])).
% 187.17/187.57 cnf(442,plain,
% 187.17/187.57 (E(f3(f5(a4,a4),f5(a4,a4)),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[440,2])).
% 187.17/187.57 cnf(443,plain,
% 187.17/187.57 (E(f8(a4,a4),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[430,304,440,2,3])).
% 187.17/187.57 cnf(445,plain,
% 187.17/187.57 (E(f5(f5(a4,a4),f5(a4,a4)),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[443,2])).
% 187.17/187.57 cnf(446,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f3(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[433,325,443,2,3])).
% 187.17/187.57 cnf(448,plain,
% 187.17/187.57 (E(f3(f5(a4,a4),f5(a4,a4)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[446,2])).
% 187.17/187.57 cnf(449,plain,
% 187.17/187.57 (E(f3(a4,a4),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[436,280,446,2,3])).
% 187.17/187.57 cnf(452,plain,
% 187.17/187.57 (E(f8(f3(f7(x4521),f7(x4521)),f5(x4521,x4521)),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[420,376,449,2,3])).
% 187.17/187.57 cnf(454,plain,
% 187.17/187.57 (E(f3(f3(a4,a4),f3(a4,a4)),f8(f3(f7(x4541),f7(x4541)),f5(x4541,x4541)))),
% 187.17/187.57 inference(scs_inference,[],[452,2])).
% 187.17/187.57 cnf(455,plain,
% 187.17/187.57 (E(f8(f7(x4551),x4551),f8(f3(f7(x4552),f7(x4552)),f5(x4552,x4552)))),
% 187.17/187.57 inference(scs_inference,[],[295,396,452,2,3])).
% 187.17/187.57 cnf(456,plain,
% 187.17/187.57 (E(f8(f3(f7(x4561),f7(x4561)),f5(x4561,x4561)),f8(f7(x4562),x4562))),
% 187.17/187.57 inference(scs_inference,[],[455,2])).
% 187.17/187.57 cnf(457,plain,
% 187.17/187.57 (E(f3(f3(a4,a4),f3(a4,a4)),f8(a4,f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[454,202,455,2,3])).
% 187.17/187.57 cnf(459,plain,
% 187.17/187.57 (E(f8(a4,f5(a4,a4)),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[457,2])).
% 187.17/187.57 cnf(460,plain,
% 187.17/187.57 (E(f8(f3(f7(x4601),f7(x4601)),f5(x4601,x4601)),a4)),
% 187.17/187.57 inference(scs_inference,[],[15,456,457,2,3])).
% 187.17/187.57 cnf(462,plain,
% 187.17/187.57 (E(a4,f8(f3(f7(x4621),f7(x4621)),f5(x4621,x4621)))),
% 187.17/187.57 inference(scs_inference,[],[460,2])).
% 187.17/187.57 cnf(463,plain,
% 187.17/187.57 (E(f8(f3(f7(x4631),f7(x4631)),f5(x4631,x4631)),f8(a4,f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[244,456,460,2,3])).
% 187.17/187.57 cnf(465,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f8(f3(f7(x4651),f7(x4651)),f5(x4651,x4651)))),
% 187.17/187.57 inference(scs_inference,[],[463,2])).
% 187.17/187.57 cnf(466,plain,
% 187.17/187.57 (E(f8(f3(f7(x4661),f7(x4661)),f5(x4661,x4661)),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[238,456,463,2,3])).
% 187.17/187.57 cnf(468,plain,
% 187.17/187.57 (E(f8(a4,a4),f8(f3(f7(x4681),f7(x4681)),f5(x4681,x4681)))),
% 187.17/187.57 inference(scs_inference,[],[466,2])).
% 187.17/187.57 cnf(469,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f8(a4,f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[465,202,466,2,3])).
% 187.17/187.57 cnf(472,plain,
% 187.17/187.57 (E(f8(a4,a4),f3(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[468,325,469,2,3])).
% 187.17/187.57 cnf(474,plain,
% 187.17/187.57 (E(f3(f5(a4,a4),f5(a4,a4)),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[472,2])).
% 187.17/187.57 cnf(475,plain,
% 187.17/187.57 (E(a4,f8(a4,f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[462,202,472,2,3])).
% 187.17/187.57 cnf(477,plain,
% 187.17/187.57 (E(f8(a4,f5(a4,a4)),a4)),
% 187.17/187.57 inference(scs_inference,[],[475,2])).
% 187.17/187.57 cnf(478,plain,
% 187.17/187.57 (E(f3(f3(a4,a4),f3(a4,a4)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[454,280,475,2,3])).
% 187.17/187.57 cnf(481,plain,
% 187.17/187.57 (E(f3(f5(a4,a4),f5(a4,a4)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[399,392,478,2,3])).
% 187.17/187.57 cnf(483,plain,
% 187.17/187.57 (E(f5(f5(a4,a4),f5(a4,a4)),f8(a4,f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[410,481,411,2,3])).
% 187.17/187.57 cnf(485,plain,
% 187.17/187.57 (E(f8(a4,f5(a4,a4)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[483,2])).
% 187.17/187.57 cnf(486,plain,
% 187.17/187.57 (E(f8(a4,f5(a4,a4)),f3(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[413,483,403,2,3])).
% 187.17/187.57 cnf(488,plain,
% 187.17/187.57 (E(f3(f5(a4,a4),f5(a4,a4)),f8(a4,f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[486,2])).
% 187.17/187.57 cnf(489,plain,
% 187.17/187.57 (E(f8(a4,a4),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[468,486,434,2,3])).
% 187.17/187.57 cnf(492,plain,
% 187.17/187.57 (E(f3(f5(a4,a4),f5(a4,a4)),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[459,488,489,2,3])).
% 187.17/187.57 cnf(494,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[465,280,492,2,3])).
% 187.17/187.57 cnf(497,plain,
% 187.17/187.57 (E(a4,f3(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[462,325,494,2,3])).
% 187.17/187.57 cnf(500,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[433,395,497,2,3])).
% 187.17/187.57 cnf(502,plain,
% 187.17/187.57 (E(f5(f8(a4,a4),f8(a4,a4)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[500,2])).
% 187.17/187.57 cnf(503,plain,
% 187.17/187.57 (E(f3(a4,a4),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[436,500,395,2,3])).
% 187.17/187.57 cnf(505,plain,
% 187.17/187.57 (E(f5(f8(a4,a4),f8(a4,a4)),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[503,2])).
% 187.17/187.57 cnf(506,plain,
% 187.17/187.57 (E(f3(f3(a4,a4),f3(a4,a4)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[454,503,431,2,3])).
% 187.17/187.57 cnf(508,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[506,2])).
% 187.17/187.57 cnf(521,plain,
% 187.17/187.57 (E(f5(f5(x5211,x5212),x5213),f5(f5(x5212,x5213),x5211))),
% 187.17/187.57 inference(scs_inference,[],[16,83,3,2])).
% 187.17/187.57 cnf(524,plain,
% 187.17/187.57 (E(f8(f7(x5241),f5(x5241,x5241)),f5(f3(a4,x5242),a4))),
% 187.17/187.57 inference(scs_inference,[],[16,93,3,2])).
% 187.17/187.57 cnf(527,plain,
% 187.17/187.57 (E(f5(f3(a4,x5271),a4),f8(f7(x5272),f3(x5272,x5272)))),
% 187.17/187.57 inference(scs_inference,[],[160,524,3,2])).
% 187.17/187.57 cnf(530,plain,
% 187.17/187.57 (E(f5(f5(a4,a4),f5(a4,a4)),f5(f3(a4,x5301),a4))),
% 187.17/187.57 inference(scs_inference,[],[283,527,3,2])).
% 187.17/187.57 cnf(531,plain,
% 187.17/187.57 (E(f3(a4,f5(a4,x5311)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[346,163,3])).
% 187.17/187.57 cnf(533,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f3(a4,f5(a4,x5331)))),
% 187.17/187.57 inference(scs_inference,[],[346,163,3,2])).
% 187.17/187.57 cnf(536,plain,
% 187.17/187.57 (E(f5(f3(a4,x5361),a4),f8(f3(f7(x5362),f7(x5362)),f5(x5362,x5362)))),
% 187.17/187.57 inference(scs_inference,[],[420,524,3,2])).
% 187.17/187.57 cnf(553,plain,
% 187.17/187.57 (E(f8(f5(f7(x5531),f7(x5531)),f3(x5531,x5531)),f5(f3(a4,x5532),a4))),
% 187.17/187.57 inference(scs_inference,[],[16,172,3,2])).
% 187.17/187.57 cnf(556,plain,
% 187.17/187.57 (E(f5(f3(a4,x5561),a4),f8(f7(x5562),x5562))),
% 187.17/187.57 inference(scs_inference,[],[553,132,3,2])).
% 187.17/187.57 cnf(559,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f5(f3(a4,x5591),a4))),
% 187.17/187.57 inference(scs_inference,[],[352,556,3,2])).
% 187.17/187.57 cnf(563,plain,
% 187.17/187.57 (E(f3(a4,f5(a4,x5631)),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[343,407,3])).
% 187.17/187.57 cnf(565,plain,
% 187.17/187.57 (E(f3(f3(a4,a4),f3(a4,a4)),f3(a4,f5(a4,x5651)))),
% 187.17/187.57 inference(scs_inference,[],[343,407,3,2])).
% 187.17/187.57 cnf(566,plain,
% 187.17/187.57 (E(f5(f5(a4,f5(a4,a4)),a4),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[16,389,3])).
% 187.17/187.57 cnf(569,plain,
% 187.17/187.57 (E(f5(f3(a4,x5691),a4),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[16,566,377,2,3])).
% 187.17/187.57 cnf(572,plain,
% 187.17/187.57 (E(f5(x5721,x5722),f5(x5722,f5(x5721,f5(x5722,x5721))))),
% 187.17/187.57 inference(scs_inference,[],[16,569,68,2,3])).
% 187.17/187.57 cnf(574,plain,
% 187.17/187.57 (E(f5(x5741,f5(x5742,f5(x5741,x5742))),f5(x5742,x5741))),
% 187.17/187.57 inference(scs_inference,[],[572,2])).
% 187.17/187.57 cnf(575,plain,
% 187.17/187.57 (E(f5(f3(a4,x5751),a4),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[536,572,466,2,3])).
% 187.17/187.57 cnf(578,plain,
% 187.17/187.57 (E(f5(f3(a4,x5781),a4),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[16,575,416,2,3])).
% 187.17/187.57 cnf(581,plain,
% 187.17/187.57 (E(f5(f3(a4,x5811),a4),f3(a4,f5(a4,x5812)))),
% 187.17/187.57 inference(scs_inference,[],[16,578,167,2,3])).
% 187.17/187.57 cnf(583,plain,
% 187.17/187.57 (E(f3(a4,f5(a4,x5831)),f5(f3(a4,x5832),a4))),
% 187.17/187.57 inference(scs_inference,[],[581,2])).
% 187.17/187.57 cnf(584,plain,
% 187.17/187.57 (E(f5(x5841,f5(x5842,x5843)),f5(x5842,f5(x5843,x5841)))),
% 187.17/187.57 inference(scs_inference,[],[16,581,20,2,3])).
% 187.17/187.57 cnf(587,plain,
% 187.17/187.57 (E(f5(x5871,f5(x5872,x5873)),f5(x5873,f5(x5871,x5872)))),
% 187.17/187.57 inference(scs_inference,[],[584,2])).
% 187.17/187.57 cnf(593,plain,
% 187.17/187.57 (E(f8(f7(x5931),f3(x5931,x5931)),f3(f5(a4,x5932),a4))),
% 187.17/187.57 inference(scs_inference,[],[17,97,3,2])).
% 187.17/187.57 cnf(608,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f5(f3(a4,x6081),a4))),
% 187.17/187.57 inference(scs_inference,[],[268,527,3,2])).
% 187.17/187.57 cnf(614,plain,
% 187.17/187.57 (E(f3(f5(a4,x6141),a4),f8(f5(f7(x6142),f7(x6142)),f3(x6142,x6142)))),
% 187.17/187.57 inference(scs_inference,[],[593,115,3,2])).
% 187.17/187.57 cnf(615,plain,
% 187.17/187.57 (E(f3(f5(a4,x6151),a4),f5(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[166,614,3])).
% 187.17/187.57 cnf(617,plain,
% 187.17/187.57 (E(f5(a4,a4),f3(f5(a4,x6171),a4))),
% 187.17/187.57 inference(scs_inference,[],[166,614,3,2])).
% 187.17/187.57 cnf(618,plain,
% 187.17/187.57 (E(f3(f5(a4,x6181),a4),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[334,614,3])).
% 187.17/187.57 cnf(620,plain,
% 187.17/187.57 (E(f3(a4,a4),f3(f5(a4,x6201),a4))),
% 187.17/187.57 inference(scs_inference,[],[334,614,3,2])).
% 187.17/187.57 cnf(621,plain,
% 187.17/187.57 (E(f3(f5(a4,x6211),a4),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[226,614,3])).
% 187.17/187.57 cnf(626,plain,
% 187.17/187.57 (E(f5(a4,f3(a4,x6261)),f3(f5(a4,x6262),a4))),
% 187.17/187.57 inference(scs_inference,[],[17,169,3,2])).
% 187.17/187.57 cnf(641,plain,
% 187.17/187.57 (E(f5(a4,f5(a4,f5(a4,a4))),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[574,386,3])).
% 187.17/187.57 cnf(647,plain,
% 187.17/187.57 (E(f5(a4,f5(f5(a4,a4),a4)),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[587,641,3])).
% 187.17/187.57 cnf(650,plain,
% 187.17/187.57 (E(f3(a4,f5(a4,x6501)),f5(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[17,647,615,2,3])).
% 187.17/187.57 cnf(652,plain,
% 187.17/187.57 (E(f5(a4,a4),f3(a4,f5(a4,x6521)))),
% 187.17/187.57 inference(scs_inference,[],[650,2])).
% 187.17/187.57 cnf(653,plain,
% 187.17/187.57 (E(f3(a4,f5(a4,x6531)),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[17,618,650,2,3])).
% 187.17/187.57 cnf(655,plain,
% 187.17/187.57 (E(f3(a4,a4),f3(a4,f5(a4,x6551)))),
% 187.17/187.57 inference(scs_inference,[],[653,2])).
% 187.17/187.57 cnf(656,plain,
% 187.17/187.57 (E(f3(a4,f5(a4,x6561)),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[17,621,653,2,3])).
% 187.17/187.57 cnf(658,plain,
% 187.17/187.57 (E(f8(a4,a4),f3(a4,f5(a4,x6581)))),
% 187.17/187.57 inference(scs_inference,[],[656,2])).
% 187.17/187.57 cnf(659,plain,
% 187.17/187.57 (E(f3(f5(a4,x6591),a4),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[17,656,531,2,3])).
% 187.17/187.57 cnf(661,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f3(f5(a4,x6611),a4))),
% 187.17/187.57 inference(scs_inference,[],[659,2])).
% 187.17/187.57 cnf(700,plain,
% 187.17/187.57 (E(f5(f5(f5(a4,a4),a4),a4),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[20,445,3])).
% 187.17/187.57 cnf(709,plain,
% 187.17/187.57 (E(f5(f5(a4,f5(a4,a4)),a4),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[521,700,3])).
% 187.17/187.57 cnf(712,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f5(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[533,709,650,2,3])).
% 187.17/187.57 cnf(714,plain,
% 187.17/187.57 (E(f5(a4,a4),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[712,2])).
% 187.17/187.57 cnf(715,plain,
% 187.17/187.57 (E(f3(f3(a4,a4),f3(a4,a4)),f5(f3(a4,x7151),a4))),
% 187.17/187.57 inference(scs_inference,[],[565,583,712,2,3])).
% 187.17/187.57 cnf(718,plain,
% 187.17/187.57 (E(f5(a4,a4),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[652,563,715,2,3])).
% 187.17/187.57 cnf(721,plain,
% 187.17/187.57 (E(f3(a4,a4),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[655,718,531,2,3])).
% 187.17/187.57 cnf(723,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[721,2])).
% 187.17/187.57 cnf(730,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7301)),f3(x7301,x7301)),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[22,235,3])).
% 187.17/187.57 cnf(732,plain,
% 187.17/187.57 (E(f8(a4,a4),f8(f8(a4,f7(x7321)),f3(x7321,x7321)))),
% 187.17/187.57 inference(scs_inference,[],[730,2])).
% 187.17/187.57 cnf(733,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7331)),f3(x7331,x7331)),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[22,322,730,2,3])).
% 187.17/187.57 cnf(735,plain,
% 187.17/187.57 (E(f3(a4,a4),f8(f8(a4,f7(x7351)),f3(x7351,x7351)))),
% 187.17/187.57 inference(scs_inference,[],[733,2])).
% 187.17/187.57 cnf(736,plain,
% 187.17/187.57 (E(f3(f5(a4,a4),f5(a4,a4)),f8(f8(a4,f7(x7361)),f3(x7361,x7361)))),
% 187.17/187.57 inference(scs_inference,[],[474,732,733,2,3])).
% 187.17/187.57 cnf(738,plain,
% 187.17/187.57 (E(f8(a4,f5(a4,a4)),f8(f8(a4,f7(x7381)),f3(x7381,x7381)))),
% 187.17/187.57 inference(scs_inference,[],[423,735,736,2,3])).
% 187.17/187.57 cnf(740,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7401)),f5(x7401,x7401)),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[22,319,738,2,3])).
% 187.17/187.57 cnf(742,plain,
% 187.17/187.57 (E(f3(a4,a4),f8(f8(a4,f7(x7421)),f5(x7421,x7421)))),
% 187.17/187.57 inference(scs_inference,[],[740,2])).
% 187.17/187.57 cnf(743,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7431)),f5(x7431,x7431)),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[22,223,740,2,3])).
% 187.17/187.57 cnf(745,plain,
% 187.17/187.57 (E(f8(a4,a4),f8(f8(a4,f7(x7451)),f5(x7451,x7451)))),
% 187.17/187.57 inference(scs_inference,[],[743,2])).
% 187.17/187.57 cnf(746,plain,
% 187.17/187.57 (E(f3(f5(a4,a4),f5(a4,a4)),f8(f8(a4,f7(x7461)),f5(x7461,x7461)))),
% 187.17/187.57 inference(scs_inference,[],[442,742,743,2,3])).
% 187.17/187.57 cnf(748,plain,
% 187.17/187.57 (E(f8(f7(x7481),f5(x7481,x7481)),f8(f8(a4,f7(x7482)),f5(x7482,x7482)))),
% 187.17/187.57 inference(scs_inference,[],[271,745,746,2,3])).
% 187.17/187.57 cnf(749,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7491)),f5(x7491,x7491)),f8(f7(x7492),f5(x7492,x7492)))),
% 187.17/187.57 inference(scs_inference,[],[748,2])).
% 187.17/187.57 cnf(750,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f5(f3(a4,x7501),a4))),
% 187.17/187.57 inference(scs_inference,[],[22,608,748,2,3])).
% 187.17/187.57 cnf(752,plain,
% 187.17/187.57 (E(f5(f3(a4,x7521),a4),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[750,2])).
% 187.17/187.57 cnf(753,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7531)),f5(x7531,x7531)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[286,749,750,2,3])).
% 187.17/187.57 cnf(755,plain,
% 187.17/187.57 (E(f5(f5(a4,a4),f5(a4,a4)),f8(f8(a4,f7(x7551)),f5(x7551,x7551)))),
% 187.17/187.57 inference(scs_inference,[],[753,2])).
% 187.17/187.57 cnf(756,plain,
% 187.17/187.57 (E(f5(f8(a4,a4),f8(a4,a4)),f3(f5(a4,x7561),a4))),
% 187.17/187.57 inference(scs_inference,[],[505,620,753,2,3])).
% 187.17/187.57 cnf(757,plain,
% 187.17/187.57 (E(f3(f5(a4,x7571),a4),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[756,2])).
% 187.17/187.57 cnf(758,plain,
% 187.17/187.57 (E(f8(a4,f5(a4,a4)),f8(f8(a4,f7(x7581)),f5(x7581,x7581)))),
% 187.17/187.57 inference(scs_inference,[],[485,755,756,2,3])).
% 187.17/187.57 cnf(760,plain,
% 187.17/187.57 (E(f5(f5(a4,a4),f5(a4,a4)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[530,752,758,2,3])).
% 187.17/187.57 cnf(762,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[760,2])).
% 187.17/187.57 cnf(763,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7631)),x7631),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[22,310,760,2,3])).
% 187.17/187.57 cnf(767,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[439,762,763,2,3])).
% 187.17/187.57 cnf(768,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[767,2])).
% 187.17/187.57 cnf(769,plain,
% 187.17/187.57 (E(f8(f7(x7691),f3(x7691,x7691)),f8(f8(a4,f7(x7692)),f3(x7692,x7692)))),
% 187.17/187.57 inference(scs_inference,[],[265,732,767,2,3])).
% 187.17/187.57 cnf(770,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7701)),f3(x7701,x7701)),f8(f7(x7702),f3(x7702,x7702)))),
% 187.17/187.57 inference(scs_inference,[],[769,2])).
% 187.17/187.57 cnf(771,plain,
% 187.17/187.57 (E(f8(a4,f5(a4,a4)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[402,768,769,2,3])).
% 187.17/187.57 cnf(773,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7731)),f3(x7731,x7731)),f8(f7(x7732),f5(x7732,x7732)))),
% 187.17/187.57 inference(scs_inference,[],[770,160,771,2,3])).
% 187.17/187.57 cnf(776,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7761)),f5(x7761,x7761)),f8(a4,f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[274,749,773,2,3])).
% 187.17/187.57 cnf(778,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f8(f8(a4,f7(x7781)),f5(x7781,x7781)))),
% 187.17/187.57 inference(scs_inference,[],[776,2])).
% 187.17/187.57 cnf(779,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7791)),f3(x7791,x7791)),f5(f5(a4,a4),f5(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[283,770,776,2,3])).
% 187.17/187.57 cnf(782,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f8(f8(a4,f7(x7821)),f5(x7821,x7821)))),
% 187.17/187.57 inference(scs_inference,[],[22,778,779,2,3])).
% 187.17/187.57 cnf(784,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7841)),f5(x7841,x7841)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[782,2])).
% 187.17/187.57 cnf(785,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f8(f8(a4,f7(x7851)),f3(x7851,x7851)))),
% 187.17/187.57 inference(scs_inference,[],[723,735,782,2,3])).
% 187.17/187.57 cnf(786,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7861)),f3(x7861,x7861)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[785,2])).
% 187.17/187.57 cnf(787,plain,
% 187.17/187.57 (E(f3(f5(a4,a4),f5(a4,a4)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[448,768,785,2,3])).
% 187.17/187.57 cnf(789,plain,
% 187.17/187.57 (E(f5(f8(a4,a4),f8(a4,a4)),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[502,508,787,2,3])).
% 187.17/187.57 cnf(790,plain,
% 187.17/187.57 (E(f3(f3(a4,a4),f3(a4,a4)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[789,2])).
% 187.17/187.57 cnf(791,plain,
% 187.17/187.57 (E(f5(a4,a4),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[714,768,789,2,3])).
% 187.17/187.57 cnf(792,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f5(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[791,2])).
% 187.17/187.57 cnf(793,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7931)),f3(x7931,x7931)),f5(f3(a4,x7932),a4))),
% 187.17/187.57 inference(scs_inference,[],[786,559,791,2,3])).
% 187.17/187.57 cnf(795,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f5(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[137,792,793,2,3])).
% 187.17/187.57 cnf(797,plain,
% 187.17/187.57 (E(f5(a4,a4),f8(a4,f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[795,2])).
% 187.17/187.57 cnf(798,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x7981)),f5(x7981,x7981)),f5(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[784,792,795,2,3])).
% 187.17/187.57 cnf(799,plain,
% 187.17/187.57 (E(f5(a4,a4),f8(f8(a4,f7(x7991)),f5(x7991,x7991)))),
% 187.17/187.57 inference(scs_inference,[],[798,2])).
% 187.17/187.57 cnf(800,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f8(f3(f7(x8001),f7(x8001)),f5(x8001,x8001)))),
% 187.17/187.57 inference(scs_inference,[],[22,465,798,2,3])).
% 187.17/187.57 cnf(803,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f8(f7(x8031),f5(x8031,x8031)))),
% 187.17/187.57 inference(scs_inference,[],[22,272,800,2,3])).
% 187.17/187.57 cnf(805,plain,
% 187.17/187.57 (E(f8(f7(x8051),f5(x8051,x8051)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[803,2])).
% 187.17/187.57 cnf(806,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f8(f7(x8061),f3(x8061,x8061)))),
% 187.17/187.57 inference(scs_inference,[],[22,266,803,2,3])).
% 187.17/187.57 cnf(808,plain,
% 187.17/187.57 (E(f8(f7(x8081),f3(x8081,x8081)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[806,2])).
% 187.17/187.57 cnf(809,plain,
% 187.17/187.57 (E(f8(f5(f7(x8091),f7(x8091)),f3(x8091,x8091)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[805,147,806,2,3])).
% 187.17/187.57 cnf(811,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f8(f5(f7(x8111),f7(x8111)),f3(x8111,x8111)))),
% 187.17/187.57 inference(scs_inference,[],[809,2])).
% 187.17/187.57 cnf(812,plain,
% 187.17/187.57 (E(f8(f7(x8121),x8121),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[808,129,809,2,3])).
% 187.17/187.57 cnf(815,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[811,298,812,2,3])).
% 187.17/187.57 cnf(817,plain,
% 187.17/187.57 (E(f5(f8(a4,a4),f8(a4,a4)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[815,2])).
% 187.17/187.57 cnf(818,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8181)),f3(x8181,x8181)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[292,770,815,2,3])).
% 187.17/187.57 cnf(820,plain,
% 187.17/187.57 (E(f5(f8(a4,a4),f8(a4,a4)),f8(f8(a4,f7(x8201)),f3(x8201,x8201)))),
% 187.17/187.57 inference(scs_inference,[],[818,2])).
% 187.17/187.57 cnf(821,plain,
% 187.17/187.57 (E(f3(f3(a4,a4),f3(a4,a4)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[790,817,818,2,3])).
% 187.17/187.57 cnf(823,plain,
% 187.17/187.57 (E(f3(f5(a4,x8231),a4),f8(f8(a4,f7(x8232)),f3(x8232,x8232)))),
% 187.17/187.57 inference(scs_inference,[],[820,757,821,2,3])).
% 187.17/187.57 cnf(825,plain,
% 187.17/187.57 (E(f3(a4,f5(a4,x8251)),f8(a4,f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[268,97,823,2,3])).
% 187.17/187.57 cnf(827,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f3(a4,f5(a4,x8271)))),
% 187.17/187.57 inference(scs_inference,[],[825,2])).
% 187.17/187.57 cnf(828,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[334,811,825,2,3])).
% 187.17/187.57 cnf(831,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f3(a4,f5(a4,x8311)))),
% 187.17/187.57 inference(scs_inference,[],[22,827,828,2,3])).
% 187.17/187.57 cnf(833,plain,
% 187.17/187.57 (E(f3(a4,f5(a4,x8331)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[831,2])).
% 187.17/187.57 cnf(834,plain,
% 187.17/187.57 (E(f5(a4,f3(a4,x8341)),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[808,123,831,2,3])).
% 187.17/187.57 cnf(836,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f5(a4,f3(a4,x8361)))),
% 187.17/187.57 inference(scs_inference,[],[834,2])).
% 187.17/187.57 cnf(837,plain,
% 187.17/187.57 (E(f8(a4,a4),f8(f8(a4,a4),a4))),
% 187.17/187.57 inference(scs_inference,[],[658,833,834,2,3])).
% 187.17/187.57 cnf(839,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[837,2])).
% 187.17/187.57 cnf(840,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f3(f5(a4,x8401),a4))),
% 187.17/187.57 inference(scs_inference,[],[836,626,837,2,3])).
% 187.17/187.57 cnf(843,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),f8(f8(a4,f7(x8431)),f3(x8431,x8431)))),
% 187.17/187.57 inference(scs_inference,[],[839,732,840,2,3])).
% 187.17/187.57 cnf(845,plain,
% 187.17/187.57 (E(f5(f3(a4,x8451),a4),a4)),
% 187.17/187.57 inference(scs_inference,[],[527,103,843,2,3])).
% 187.17/187.57 cnf(848,plain,
% 187.17/187.57 (E(f8(f7(x8481),f5(f3(x8481,x8481),f3(x8481,x8481))),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[367,43,845,2,3])).
% 187.17/187.57 cnf(851,plain,
% 187.17/187.57 (E(f8(f7(x8511),f3(f3(x8511,x8511),f3(x8511,x8511))),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[265,50,848,2,3])).
% 187.17/187.57 cnf(854,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8541)),f3(x8541,x8541)),f5(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[22,851,251,2,3])).
% 187.17/187.57 cnf(857,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8571)),x8571),f5(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[22,854,227,2,3])).
% 187.17/187.57 cnf(861,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8611)),x8611),f8(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[22,857,239,2,3])).
% 187.17/187.57 cnf(865,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8651)),f5(x8651,x8651)),a4)),
% 187.17/187.57 inference(scs_inference,[],[22,861,218,2,3])).
% 187.17/187.57 cnf(868,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8681)),f3(x8681,x8681)),a4)),
% 187.17/187.57 inference(scs_inference,[],[22,865,230,2,3])).
% 187.17/187.57 cnf(871,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8711)),x8711),a4)),
% 187.17/187.57 inference(scs_inference,[],[22,868,275,2,3])).
% 187.17/187.57 cnf(875,plain,
% 187.17/187.57 (E(f8(f7(x8751),f3(x8751,x8751)),f8(f8(a4,f7(x8752)),f5(x8752,x8752)))),
% 187.17/187.57 inference(scs_inference,[],[328,871,746,2,3])).
% 187.17/187.57 cnf(876,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8761)),f5(x8761,x8761)),f8(f7(x8762),f3(x8762,x8762)))),
% 187.17/187.57 inference(scs_inference,[],[875,2])).
% 187.17/187.57 cnf(877,plain,
% 187.17/187.57 (E(f8(f8(a4,a4),a4),a4)),
% 187.17/187.57 inference(scs_inference,[],[811,875,107,2,3])).
% 187.17/187.57 cnf(880,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8801)),f5(x8801,x8801)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[876,349,877,2,3])).
% 187.17/187.57 cnf(882,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f8(f8(a4,f7(x8821)),f5(x8821,x8821)))),
% 187.17/187.57 inference(scs_inference,[],[880,2])).
% 187.17/187.57 cnf(883,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8831)),f5(x8831,x8831)),f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[370,876,880,2,3])).
% 187.17/187.57 cnf(885,plain,
% 187.17/187.57 (E(f3(f3(a4,a4),f3(a4,a4)),f8(f8(a4,f7(x8851)),f5(x8851,x8851)))),
% 187.17/187.57 inference(scs_inference,[],[883,2])).
% 187.17/187.57 cnf(886,plain,
% 187.17/187.57 (E(f8(f8(a4,f7(x8861)),f5(x8861,x8861)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[292,876,883,2,3])).
% 187.17/187.57 cnf(889,plain,
% 187.17/187.57 (E(f5(a4,a4),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[799,886,2,3])).
% 187.17/187.57 cnf(891,plain,
% 187.17/187.57 (E(f5(f8(a4,a4),f8(a4,a4)),f5(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[889,2])).
% 187.17/187.57 cnf(892,plain,
% 187.17/187.57 (E(f3(f8(a4,a4),f8(a4,a4)),f8(a4,f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[882,889,776,2,3])).
% 187.17/187.57 cnf(894,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f3(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[892,2])).
% 187.17/187.57 cnf(895,plain,
% 187.17/187.57 (E(f5(f8(a4,a4),f8(a4,a4)),f8(a4,f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[891,797,892,2,3])).
% 187.17/187.57 cnf(896,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f5(f8(a4,a4),f8(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[895,2])).
% 187.17/187.57 cnf(897,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f3(f5(a4,x8971),a4))),
% 187.17/187.57 inference(scs_inference,[],[894,661,895,2,3])).
% 187.17/187.57 cnf(899,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,a4)),f3(a4,a4))),
% 187.17/187.57 inference(scs_inference,[],[896,505,897,2,3])).
% 187.17/187.57 cnf(901,plain,
% 187.17/187.57 (E(f3(f3(a4,a4),f3(a4,a4)),a4)),
% 187.17/187.57 inference(scs_inference,[],[885,899,865,2,3])).
% 187.17/187.57 cnf(903,plain,
% 187.17/187.57 (E(a4,f3(f3(a4,a4),f3(a4,a4)))),
% 187.17/187.57 inference(scs_inference,[],[901,2])).
% 187.17/187.57 cnf(947,plain,
% 187.17/187.57 (E(a4,f3(f5(a4,x9471),a4))),
% 187.17/187.57 inference(scs_inference,[],[28,617,3])).
% 187.17/187.57 cnf(950,plain,
% 187.17/187.57 (E(f5(x9501,x9502),f5(f5(f5(x9501,x9502),x9501),x9502))),
% 187.17/187.57 inference(scs_inference,[],[28,83,3])).
% 187.17/187.57 cnf(957,plain,
% 187.17/187.57 (E(x9571,f5(f5(f5(x9571,x9571),x9571),x9571))),
% 187.17/187.57 inference(scs_inference,[],[28,950,3])).
% 187.17/187.57 cnf(965,plain,
% 187.17/187.57 (E(f5(f5(f5(f5(x9651,x9651),f5(x9651,x9651)),f5(x9651,x9651)),f5(x9651,x9651)),x9651)),
% 187.17/187.57 inference(scs_inference,[],[28,957,3,2])).
% 187.17/187.57 cnf(994,plain,
% 187.17/187.57 (~E(a1,f5(a2,a2))),
% 187.17/187.57 inference(scs_inference,[],[34,57,3,6])).
% 187.17/187.57 cnf(997,plain,
% 187.17/187.57 (~E(a1,f3(a2,a2))),
% 187.17/187.57 inference(scs_inference,[],[34,64,3,6])).
% 187.17/187.57 cnf(1000,plain,
% 187.17/187.57 (~E(f8(a1,a6),f8(a2,f3(a6,a6)))),
% 187.17/187.57 inference(scs_inference,[],[34,50,3])).
% 187.17/187.57 cnf(1018,plain,
% 187.17/187.57 (~E(f8(a1,a6),f3(f8(a2,a6),f8(a2,a6)))),
% 187.17/187.57 inference(scs_inference,[],[34,14,3])).
% 187.17/187.57 cnf(1025,plain,
% 187.17/187.57 (~E(a1,f5(f5(f5(f5(a2,a2),f5(a2,a2)),f5(a2,a2)),f5(a2,a2)))),
% 187.17/187.57 inference(scs_inference,[],[35,965,3])).
% 187.17/187.57 cnf(1212,plain,
% 187.17/187.57 (E(f8(f3(a1,a2),x12121),f8(a2,x12121))),
% 187.17/187.57 inference(scs_inference,[],[11,10,5,7,8,9,4,6])).
% 187.17/187.57 cnf(1253,plain,
% 187.17/187.57 (~E(f8(a2,f3(a6,a6)),f8(a1,a6))),
% 187.17/187.57 inference(scs_inference,[],[1000,947,5,8,9,10,7,4,6,2])).
% 187.17/187.57 cnf(1273,plain,
% 187.17/187.57 (E(f8(a2,x12731),f8(f3(a1,a2),x12731))),
% 187.17/187.57 inference(scs_inference,[],[140,8,5,9,10,7,4,6])).
% 187.17/187.57 cnf(1294,plain,
% 187.17/187.57 (~E(f3(f8(a2,a6),f8(a2,a6)),f8(a1,a6))),
% 187.17/187.57 inference(scs_inference,[],[1018,475,5,8,9,10,7,4,6,2])).
% 187.17/187.57 cnf(1295,plain,
% 187.17/187.57 (~E(f8(f3(a1,a2),f3(a6,a6)),f8(a1,a6))),
% 187.17/187.57 inference(scs_inference,[],[1253,1018,1273,475,5,8,9,10,7,4,6,2,3])).
% 187.17/187.57 cnf(1304,plain,
% 187.17/187.57 (~E(f8(a1,a6),f8(f3(a1,a2),f3(a6,a6)))),
% 187.17/187.57 inference(scs_inference,[],[1295,477,8,9,5,7,10,4,6,2])).
% 187.17/187.57 cnf(1321,plain,
% 187.17/187.57 (E(f8(x13211,f8(a4,x13212)),f8(x13211,x13212))),
% 187.17/187.57 inference(scs_inference,[],[12,5,8,9,10,7])).
% 187.17/187.57 cnf(1384,plain,
% 187.17/187.57 (E(f8(a4,f8(a4,x13841)),x13841)),
% 187.17/187.57 inference(scs_inference,[],[12,1321,58,903,7,9,5,10,8,6,4,2,3])).
% 187.17/187.57 cnf(1394,plain,
% 187.17/187.57 (~E(f8(f3(a1,a1),a6),f8(f3(a1,a2),f3(a6,a6)))),
% 187.17/187.57 inference(scs_inference,[],[1384,1304,65,61,9,10,7,5,8,6,4,2,3])).
% 187.17/187.57 cnf(1538,plain,
% 187.17/187.57 (E(f7(f3(x15381,x15381)),f7(x15381))),
% 187.17/187.57 inference(scs_inference,[],[14,1025,489,2,7,10])).
% 187.17/187.57 cnf(1540,plain,
% 187.17/187.57 (E(f5(x15401,f3(x15402,x15402)),f5(x15401,x15402))),
% 187.17/187.57 inference(scs_inference,[],[14,1025,489,2,7,10,5,9])).
% 187.17/187.57 cnf(1622,plain,
% 187.17/187.57 (E(f8(x16221,x16222),f8(f8(a4,x16221),x16222))),
% 187.17/187.57 inference(scs_inference,[],[994,489,36,2,7,10,5,8,9,6])).
% 187.17/187.57 cnf(1638,plain,
% 187.17/187.57 (E(f3(x16381,x16382),f3(f3(x16381,x16381),x16382))),
% 187.17/187.57 inference(scs_inference,[],[31,80,9,6,4])).
% 187.17/187.57 cnf(1654,plain,
% 187.17/187.57 (~E(f3(f3(f8(a2,a6),f8(a2,a6)),f8(a2,a6)),f8(a1,a6))),
% 187.17/187.57 inference(scs_inference,[],[15,1294,1638,997,9,6,4,2,7,10,5,8,3])).
% 187.17/187.57 cnf(1659,plain,
% 187.17/187.57 (~E(f8(a1,a6),f3(f3(f8(a2,a6),f8(a2,a6)),f8(a2,a6)))),
% 187.17/187.57 inference(scs_inference,[],[1654,36,18,9,6,4,2])).
% 187.17/187.57 cnf(1661,plain,
% 187.17/187.57 (E(f7(x16611),f7(f8(a4,x16611)))),
% 187.17/187.57 inference(scs_inference,[],[1654,36,18,9,6,4,2,7,10])).
% 187.17/187.57 cnf(1726,plain,
% 187.17/187.57 (~E(f8(f8(a4,a1),a6),f3(f3(f8(a2,a6),f8(a2,a6)),f8(a2,a6)))),
% 187.17/187.57 inference(scs_inference,[],[1659,1622,193,16,9,4,2,10,5,8,3])).
% 187.17/187.57 cnf(1729,plain,
% 187.17/187.57 (E(f7(f3(x17291,x17291)),f7(f8(a4,x17291)))),
% 187.17/187.57 inference(scs_inference,[],[1538,1661,1726,2,3])).
% 187.17/187.57 cnf(1995,plain,
% 187.17/187.57 (~E(f3(a1,a1),f3(a1,a2))),
% 187.17/187.57 inference(scs_inference,[],[1394,47,1729,2,3,6])).
% 187.17/187.57 cnf(2297,plain,
% 187.17/187.57 ($false),
% 187.17/187.57 inference(scs_inference,[],[27,26,1540,1995,1212,10,5,8,9,4,7,6,2,3]),
% 187.17/187.57 ['proof']).
% 187.17/187.57 % SZS output end Proof
% 187.17/187.57 % Total time :186.540000s
%------------------------------------------------------------------------------