%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP156-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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:03 EDT 2024
% Result : Unsatisfiable 250.01s 250.05s
% Output : CNFRefutation 250.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP156-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n017.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Thu Jun 20 13:26:24 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 250.01/250.04 %-------------------------------------------
% 250.01/250.04 % File :CSE---1.7
% 250.01/250.04 % Problem :theBenchmark
% 250.01/250.04 % Transform :cnf
% 250.01/250.04 % Format :tptp:raw
% 250.01/250.04 % Command :java -jar mcs_scs.jar %d %s
% 250.01/250.04
% 250.01/250.04 % Result :Theorem 249.410000s
% 250.01/250.04 % Output :CNFRefutation 249.410000s
% 250.01/250.04 %-------------------------------------------
% 250.01/250.05 %--------------------------------------------------------------------------
% 250.01/250.05 % File : GRP156-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 250.01/250.05 % Domain : Group Theory (Lattice Ordered)
% 250.01/250.05 % Problem : Prove monotonicity axiom using a transformation
% 250.01/250.05 % Version : [Fuc94] (equality) axioms.
% 250.01/250.05 % English : This problem proves the original monotonicity axiom from the
% 250.01/250.05 % equational axiomatization.
% 250.01/250.05
% 250.01/250.05 % Refs : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri
% 250.01/250.05 % : [Sch95] Schulz (1995), Explanation Based Learning for Distribu
% 250.01/250.05 % Source : [Sch95]
% 250.01/250.05 % Names : ax_mono1c [Sch95]
% 250.01/250.05
% 250.01/250.05 % Status : Unsatisfiable
% 250.01/250.05 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v7.0.0, 0.05 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.0.0, 0.07 v4.1.0, 0.09 v4.0.1, 0.07 v4.0.0, 0.08 v3.7.0, 0.11 v3.4.0, 0.00 v2.0.0
% 250.01/250.05 % Syntax : Number of clauses : 17 ( 17 unt; 0 nHn; 2 RR)
% 250.01/250.05 % Number of literals : 17 ( 17 equ; 1 neg)
% 250.01/250.05 % Maximal clause size : 1 ( 1 avg)
% 250.01/250.05 % Maximal term depth : 3 ( 2 avg)
% 250.01/250.05 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 250.01/250.05 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 250.01/250.05 % Number of variables : 33 ( 2 sgn)
% 250.01/250.05 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 250.01/250.05
% 250.01/250.05 % Comments : ORDERING LPO inverse > product > greatest_lower_bound >
% 250.01/250.05 % least_upper_bound > identity > a > b > c
% 250.01/250.05 % : ORDERING LPO greatest_lower_bound > least_upper_bound >
% 250.01/250.05 % inverse > product > identity > a > b > c
% 250.01/250.05 % Bugfixes : v1.2.1 - Duplicate axioms in GRP004-2.ax removed.
% 250.01/250.05 %--------------------------------------------------------------------------
% 250.01/250.05 %----Include equality group theory axioms
% 250.01/250.05 include('Axioms/GRP004-0.ax').
% 250.01/250.05 %----Include Lattice ordered group (equality) axioms
% 250.01/250.05 include('Axioms/GRP004-2.ax').
% 250.01/250.05 %--------------------------------------------------------------------------
% 250.01/250.05 cnf(ax_mono1c_1,hypothesis,
% 250.01/250.05 least_upper_bound(a,b) = b ).
% 250.01/250.05
% 250.01/250.05 cnf(prove_ax_mono1c,negated_conjecture,
% 250.01/250.05 greatest_lower_bound(multiply(a,c),multiply(b,c)) != multiply(a,c) ).
% 250.01/250.05
% 250.01/250.05 %--------------------------------------------------------------------------
% 250.01/250.05 %-------------------------------------------
% 250.01/250.05 % Proof found
% 250.01/250.05 % SZS status Theorem for theBenchmark
% 250.01/250.05 % SZS output start Proof
% 250.01/250.06 %ClaNum:27(EqnAxiom:10)
% 250.01/250.06 %VarNum:72(SingletonVarNum:33)
% 250.01/250.06 %MaxLitNum:1
% 250.01/250.06 %MaxfuncDepth:2
% 250.01/250.06 %SharedTerms:10
% 250.01/250.06 %goalClause: 27
% 250.01/250.06 %singleGoalClaCount:1
% 250.01/250.06 [11]E(f3(a1,a2),a2)
% 250.01/250.06 [27]~E(f5(f8(a1,a6),f8(a2,a6)),f8(a1,a6))
% 250.01/250.06 [12]E(f8(a4,x121),x121)
% 250.01/250.06 [13]E(f5(x131,x131),x131)
% 250.01/250.06 [14]E(f3(x141,x141),x141)
% 250.01/250.06 [15]E(f8(f7(x151),x151),a4)
% 250.01/250.06 [16]E(f5(x161,x162),f5(x162,x161))
% 250.01/250.06 [17]E(f3(x171,x172),f3(x172,x171))
% 250.01/250.06 [18]E(f5(x181,f3(x181,x182)),x181)
% 250.01/250.06 [19]E(f3(x191,f5(x191,x192)),x191)
% 250.01/250.06 [20]E(f5(f5(x201,x202),x203),f5(x201,f5(x202,x203)))
% 250.01/250.06 [21]E(f3(f3(x211,x212),x213),f3(x211,f3(x212,x213)))
% 250.01/250.06 [22]E(f8(f8(x221,x222),x223),f8(x221,f8(x222,x223)))
% 250.01/250.06 [23]E(f5(f8(x231,x232),f8(x231,x233)),f8(x231,f5(x232,x233)))
% 250.01/250.06 [24]E(f3(f8(x241,x242),f8(x241,x243)),f8(x241,f3(x242,x243)))
% 250.01/250.06 [25]E(f5(f8(x251,x252),f8(x253,x252)),f8(f5(x251,x253),x252))
% 250.01/250.06 [26]E(f3(f8(x261,x262),f8(x263,x262)),f8(f3(x261,x263),x262))
% 250.01/250.06 %EqnAxiom
% 250.01/250.06 [1]E(x11,x11)
% 250.01/250.06 [2]E(x22,x21)+~E(x21,x22)
% 250.01/250.06 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 250.01/250.06 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 250.01/250.06 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 250.01/250.06 [6]~E(x61,x62)+E(f8(x61,x63),f8(x62,x63))
% 250.01/250.06 [7]~E(x71,x72)+E(f8(x73,x71),f8(x73,x72))
% 250.01/250.06 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83))
% 250.01/250.06 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92))
% 250.01/250.06 [10]~E(x101,x102)+E(f7(x101),f7(x102))
% 250.01/250.06
% 250.01/250.06 %-------------------------------------------
% 250.01/250.07 cnf(28,plain,
% 250.01/250.07 (E(x281,f5(x281,x281))),
% 250.01/250.07 inference(scs_inference,[],[13,2])).
% 250.01/250.07 cnf(29,plain,
% 250.01/250.07 (~E(f5(f8(a1,a6),f8(a2,a6)),f5(f8(a1,a6),f8(a1,a6)))),
% 250.01/250.07 inference(scs_inference,[],[27,13,2,3])).
% 250.01/250.07 cnf(31,plain,
% 250.01/250.07 (~E(f8(a2,a6),f8(a1,a6))),
% 250.01/250.07 inference(scs_inference,[],[27,13,2,3,9])).
% 250.01/250.07 cnf(32,plain,
% 250.01/250.07 (~E(a2,a1)),
% 250.01/250.07 inference(scs_inference,[],[27,13,2,3,9,6])).
% 250.01/250.07 cnf(33,plain,
% 250.01/250.07 (E(x331,f3(x331,x331))),
% 250.01/250.08 inference(scs_inference,[],[14,2])).
% 250.01/250.08 cnf(36,plain,
% 250.01/250.08 (E(x361,f8(a4,x361))),
% 250.01/250.08 inference(scs_inference,[],[12,2])).
% 250.01/250.08 cnf(37,plain,
% 250.01/250.08 (~E(f5(f8(a1,a6),f8(a2,a6)),f8(a4,f8(a1,a6)))),
% 250.01/250.08 inference(scs_inference,[],[27,12,2,3])).
% 250.01/250.08 cnf(39,plain,
% 250.01/250.08 (E(f8(x391,f5(x392,x393)),f5(f8(x391,x392),f8(x391,x393)))),
% 250.01/250.08 inference(scs_inference,[],[23,2])).
% 250.01/250.08 cnf(40,plain,
% 250.01/250.08 (E(f8(x401,x402),f8(x401,f5(x402,x402)))),
% 250.01/250.08 inference(scs_inference,[],[28,23,2,3])).
% 250.01/250.08 cnf(43,plain,
% 250.01/250.08 (E(f8(x431,f5(x432,x432)),f8(x431,x432))),
% 250.01/250.08 inference(scs_inference,[],[40,2])).
% 250.01/250.08 cnf(44,plain,
% 250.01/250.08 (~E(f5(f8(a1,a6),f8(a2,a6)),f8(a1,f5(a6,a6)))),
% 250.01/250.08 inference(scs_inference,[],[39,40,29,2,3])).
% 250.01/250.08 cnf(47,plain,
% 250.01/250.08 (E(f8(x471,x472),f8(x471,f3(x472,x472)))),
% 250.01/250.08 inference(scs_inference,[],[33,24,2,3])).
% 250.01/250.08 cnf(50,plain,
% 250.01/250.08 (E(f8(x501,f3(x502,x502)),f8(x501,x502))),
% 250.01/250.08 inference(scs_inference,[],[47,2])).
% 250.01/250.08 cnf(53,plain,
% 250.01/250.08 (E(f8(f5(x531,x532),x533),f5(f8(x531,x533),f8(x532,x533)))),
% 250.01/250.08 inference(scs_inference,[],[25,2])).
% 250.01/250.08 cnf(54,plain,
% 250.01/250.08 (E(f8(x541,x542),f8(f5(x541,x541),x542))),
% 250.01/250.08 inference(scs_inference,[],[28,25,2,3])).
% 250.01/250.08 cnf(57,plain,
% 250.01/250.08 (E(f8(f5(x571,x571),x572),f8(x571,x572))),
% 250.01/250.08 inference(scs_inference,[],[54,2])).
% 250.01/250.08 cnf(58,plain,
% 250.01/250.08 (~E(f5(f8(a1,a6),f8(a2,a6)),f8(f5(a1,a1),a6))),
% 250.01/250.08 inference(scs_inference,[],[53,54,29,2,3])).
% 250.01/250.08 cnf(61,plain,
% 250.01/250.08 (E(f8(x611,x612),f8(f3(x611,x611),x612))),
% 250.01/250.08 inference(scs_inference,[],[33,26,2,3])).
% 250.01/250.08 cnf(64,plain,
% 250.01/250.08 (E(f8(f3(x641,x641),x642),f8(x641,x642))),
% 250.01/250.08 inference(scs_inference,[],[61,2])).
% 250.01/250.08 cnf(67,plain,
% 250.01/250.08 (E(x671,f5(x671,f3(x671,x672)))),
% 250.01/250.08 inference(scs_inference,[],[18,2])).
% 250.01/250.08 cnf(68,plain,
% 250.01/250.08 (E(f5(x681,x682),f5(x681,f5(x682,f5(x681,x682))))),
% 250.01/250.08 inference(scs_inference,[],[28,18,20,2,3])).
% 250.01/250.08 cnf(71,plain,
% 250.01/250.08 (E(f5(x711,f5(x712,f5(x711,x712))),f5(x711,x712))),
% 250.01/250.08 inference(scs_inference,[],[68,2])).
% 250.01/250.08 cnf(72,plain,
% 250.01/250.08 (E(f3(x721,x722),f3(x721,f3(x722,f3(x721,x722))))),
% 250.01/250.08 inference(scs_inference,[],[33,68,21,2,3])).
% 250.01/250.08 cnf(75,plain,
% 250.01/250.08 (E(f3(x751,f3(x752,f3(x751,x752))),f3(x751,x752))),
% 250.01/250.08 inference(scs_inference,[],[72,2])).
% 250.01/250.08 cnf(76,plain,
% 250.01/250.08 (~E(f5(f8(a1,a6),f8(a2,a6)),f8(f8(a4,a1),a6))),
% 250.01/250.08 inference(scs_inference,[],[72,37,22,2,3])).
% 250.01/250.08 cnf(78,plain,
% 250.01/250.08 (E(x781,f3(x781,f5(x781,x782)))),
% 250.01/250.08 inference(scs_inference,[],[19,2])).
% 250.01/250.08 cnf(79,plain,
% 250.01/250.08 (E(f3(a1,f3(a2,f3(a1,a2))),a2)),
% 250.01/250.08 inference(scs_inference,[],[75,19,11,2,3])).
% 250.01/250.08 cnf(81,plain,
% 250.01/250.08 (E(a2,f3(a1,f3(a2,f3(a1,a2))))),
% 250.01/250.08 inference(scs_inference,[],[79,2])).
% 250.01/250.08 cnf(82,plain,
% 250.01/250.08 (E(f8(f7(x821),f5(x821,x821)),a4)),
% 250.01/250.08 inference(scs_inference,[],[43,79,15,2,3])).
% 250.01/250.08 cnf(85,plain,
% 250.01/250.08 (E(a4,f8(f7(x851),f5(x851,x851)))),
% 250.01/250.08 inference(scs_inference,[],[82,2])).
% 250.01/250.08 cnf(86,plain,
% 250.01/250.08 (E(f8(f7(x861),f3(f5(x861,x861),f5(x861,x861))),a4)),
% 250.01/250.08 inference(scs_inference,[],[50,82,2,3])).
% 250.01/250.08 cnf(89,plain,
% 250.01/250.08 (E(f8(f5(f7(x891),f7(x891)),f5(x891,x891)),a4)),
% 250.01/250.08 inference(scs_inference,[],[57,86,82,2,3])).
% 250.01/250.08 cnf(91,plain,
% 250.01/250.08 (E(a4,f8(f5(f7(x911),f7(x911)),f5(x911,x911)))),
% 250.01/250.08 inference(scs_inference,[],[89,2])).
% 250.01/250.08 cnf(92,plain,
% 250.01/250.08 (E(f8(f5(f7(x921),f7(x921)),f5(x921,x921)),f8(f7(x922),f5(x922,x922)))),
% 250.01/250.08 inference(scs_inference,[],[85,89,2,3])).
% 250.01/250.08 cnf(93,plain,
% 250.01/250.08 (E(f8(f7(x931),f5(x931,x931)),f8(f5(f7(x932),f7(x932)),f5(x932,x932)))),
% 250.01/250.08 inference(scs_inference,[],[92,2])).
% 250.01/250.08 cnf(94,plain,
% 250.01/250.08 (E(f8(f3(f7(x941),f7(x941)),f5(x941,x941)),a4)),
% 250.01/250.08 inference(scs_inference,[],[64,92,82,2,3])).
% 250.01/250.08 cnf(96,plain,
% 250.01/250.08 (E(a4,f8(f3(f7(x961),f7(x961)),f5(x961,x961)))),
% 250.01/250.08 inference(scs_inference,[],[94,2])).
% 250.01/250.08 cnf(97,plain,
% 250.01/250.08 (E(f8(f3(f7(x971),f7(x971)),f5(x971,x971)),f8(f7(x972),f5(x972,x972)))),
% 250.01/250.08 inference(scs_inference,[],[85,94,2,3])).
% 250.01/250.08 cnf(98,plain,
% 250.01/250.08 (E(f8(f7(x981),f5(x981,x981)),f8(f3(f7(x982),f7(x982)),f5(x982,x982)))),
% 250.01/250.08 inference(scs_inference,[],[97,2])).
% 250.01/250.08 cnf(101,plain,
% 250.01/250.08 (E(f5(x1011,f5(x1012,x1013)),f5(f5(x1011,x1012),x1013))),
% 250.01/250.08 inference(scs_inference,[],[20,2])).
% 250.01/250.08 cnf(102,plain,
% 250.01/250.08 (E(f8(f7(x1021),f5(f5(x1021,x1021),f5(x1021,x1021))),a4)),
% 250.01/250.08 inference(scs_inference,[],[43,82,20,2,3])).
% 250.01/250.08 cnf(105,plain,
% 250.01/250.08 (E(f8(f7(x1051),f3(x1051,x1051)),a4)),
% 250.01/250.08 inference(scs_inference,[],[50,102,15,2,3])).
% 250.01/250.08 cnf(108,plain,
% 250.01/250.08 (E(a4,f8(f7(x1081),f3(x1081,x1081)))),
% 250.01/250.08 inference(scs_inference,[],[105,2])).
% 250.01/250.08 cnf(109,plain,
% 250.01/250.08 (E(f8(f7(x1091),f3(x1091,x1091)),f8(f5(f7(x1092),f7(x1092)),f5(x1092,x1092)))),
% 250.01/250.08 inference(scs_inference,[],[91,105,2,3])).
% 250.01/250.08 cnf(110,plain,
% 250.01/250.08 (E(f8(f5(f7(x1101),f7(x1101)),f5(x1101,x1101)),f8(f7(x1102),f3(x1102,x1102)))),
% 250.01/250.08 inference(scs_inference,[],[109,2])).
% 250.01/250.08 cnf(111,plain,
% 250.01/250.08 (E(f8(f5(f7(x1111),f7(x1111)),x1111),a4)),
% 250.01/250.08 inference(scs_inference,[],[57,109,15,2,3])).
% 250.01/250.08 cnf(115,plain,
% 250.01/250.08 (E(f8(f3(f7(x1151),f7(x1151)),x1151),a4)),
% 250.01/250.08 inference(scs_inference,[],[64,111,15,2,3])).
% 250.01/250.08 cnf(118,plain,
% 250.01/250.08 (E(a4,f8(f3(f7(x1181),f7(x1181)),x1181))),
% 250.01/250.08 inference(scs_inference,[],[115,2])).
% 250.01/250.08 cnf(119,plain,
% 250.01/250.08 (E(f8(f7(x1191),f5(x1191,x1191)),f8(f7(x1192),f3(x1192,x1192)))),
% 250.01/250.08 inference(scs_inference,[],[110,93,115,2,3])).
% 250.01/250.08 cnf(121,plain,
% 250.01/250.08 (E(f8(f7(x1211),f3(x1211,x1211)),f8(f7(x1212),f5(x1212,x1212)))),
% 250.01/250.08 inference(scs_inference,[],[119,2])).
% 250.01/250.08 cnf(122,plain,
% 250.01/250.08 (E(f3(x1221,f3(x1222,x1223)),f3(f3(x1221,x1222),x1223))),
% 250.01/250.08 inference(scs_inference,[],[21,2])).
% 250.01/250.08 cnf(123,plain,
% 250.01/250.08 (E(f8(f7(x1231),f3(x1231,x1231)),f8(f3(f7(x1232),f7(x1232)),f5(x1232,x1232)))),
% 250.01/250.08 inference(scs_inference,[],[98,121,21,2,3])).
% 250.01/250.08 cnf(125,plain,
% 250.01/250.08 (E(f8(f3(f7(x1251),f7(x1251)),f5(x1251,x1251)),f8(f7(x1252),f3(x1252,x1252)))),
% 250.01/250.08 inference(scs_inference,[],[123,2])).
% 250.01/250.08 cnf(126,plain,
% 250.01/250.08 (E(a2,f3(f3(a1,a2),f3(a1,a2)))),
% 250.01/250.08 inference(scs_inference,[],[122,81,123,2,3])).
% 250.01/250.08 cnf(128,plain,
% 250.01/250.08 (E(f3(f3(a1,a2),f3(a1,a2)),a2)),
% 250.01/250.08 inference(scs_inference,[],[126,2])).
% 250.01/250.08 cnf(132,plain,
% 250.01/250.08 (E(a2,f3(a1,a2))),
% 250.01/250.08 inference(scs_inference,[],[11,2])).
% 250.01/250.08 cnf(133,plain,
% 250.01/250.08 (E(a4,f8(f7(x1331),x1331))),
% 250.01/250.08 inference(scs_inference,[],[15,2])).
% 250.01/250.08 cnf(134,plain,
% 250.01/250.08 (E(f3(a1,a2),f5(a2,f3(a2,x1341)))),
% 250.01/250.08 inference(scs_inference,[],[11,67,3])).
% 250.01/250.08 cnf(136,plain,
% 250.01/250.08 (E(f5(a2,f3(a2,x1361)),f3(a1,a2))),
% 250.01/250.08 inference(scs_inference,[],[11,67,3,2])).
% 250.01/250.08 cnf(137,plain,
% 250.01/250.08 (E(f3(a1,a2),f3(a2,f5(a2,x1371)))),
% 250.01/250.08 inference(scs_inference,[],[11,78,3])).
% 250.01/250.08 cnf(139,plain,
% 250.01/250.08 (E(f3(a2,f5(a2,x1391)),f3(a1,a2))),
% 250.01/250.08 inference(scs_inference,[],[11,78,3,2])).
% 250.01/250.08 cnf(142,plain,
% 250.01/250.08 (E(a2,f8(a4,f3(f3(a1,a2),f3(a1,a2))))),
% 250.01/250.08 inference(scs_inference,[],[12,128,3,2])).
% 250.01/250.08 cnf(143,plain,
% 250.01/250.08 (E(f8(a4,a2),f3(a1,a2))),
% 250.01/250.08 inference(scs_inference,[],[12,132,3])).
% 250.01/250.08 cnf(145,plain,
% 250.01/250.08 (E(f3(a1,a2),f8(a4,a2))),
% 250.01/250.08 inference(scs_inference,[],[12,132,3,2])).
% 250.01/250.08 cnf(146,plain,
% 250.01/250.08 (E(f8(a4,f3(a1,a2)),f8(a4,a2))),
% 250.01/250.08 inference(scs_inference,[],[12,145,3])).
% 250.01/250.08 cnf(148,plain,
% 250.01/250.08 (E(f8(a4,a2),f8(a4,f3(a1,a2)))),
% 250.01/250.08 inference(scs_inference,[],[12,145,3,2])).
% 250.01/250.08 cnf(154,plain,
% 250.01/250.08 (E(f8(a4,f3(a1,a2)),f8(a4,f8(a4,a2)))),
% 250.01/250.08 inference(scs_inference,[],[12,148,3,2])).
% 250.01/250.08 cnf(157,plain,
% 250.01/250.08 (E(f3(a1,a2),f8(a4,f5(a2,f3(a2,x1571))))),
% 250.01/250.08 inference(scs_inference,[],[12,136,3,2])).
% 250.13/250.08 cnf(160,plain,
% 250.13/250.08 (E(f3(a1,a2),f8(a4,f3(a2,f5(a2,x1601))))),
% 250.13/250.08 inference(scs_inference,[],[12,139,3,2])).
% 250.13/250.08 cnf(163,plain,
% 250.13/250.08 (E(f8(f3(f7(x1631),f7(x1631)),f5(x1631,x1631)),f8(a4,a4))),
% 250.13/250.08 inference(scs_inference,[],[12,96,3,2])).
% 250.13/250.08 cnf(164,plain,
% 250.13/250.08 (E(f8(a4,a4),f8(f7(x1641),f3(x1641,x1641)))),
% 250.13/250.08 inference(scs_inference,[],[12,108,3])).
% 250.13/250.08 cnf(172,plain,
% 250.13/250.08 (E(f8(f7(x1721),x1721),f8(a4,a4))),
% 250.13/250.08 inference(scs_inference,[],[12,133,3,2])).
% 250.13/250.08 cnf(175,plain,
% 250.13/250.08 (E(f8(a4,a4),f8(a4,f8(f7(x1751),x1751)))),
% 250.13/250.08 inference(scs_inference,[],[12,172,3,2])).
% 250.13/250.08 cnf(188,plain,
% 250.13/250.08 (E(f8(a4,x1881),f5(x1881,f3(x1881,x1882)))),
% 250.13/250.08 inference(scs_inference,[],[12,67,3])).
% 250.13/250.08 cnf(190,plain,
% 250.13/250.08 (E(f5(x1901,f3(x1901,x1902)),f8(a4,x1901))),
% 250.13/250.08 inference(scs_inference,[],[12,67,3,2])).
% 250.13/250.08 cnf(191,plain,
% 250.13/250.08 (E(f8(a4,x1911),f3(x1911,f5(x1911,x1912)))),
% 250.13/250.08 inference(scs_inference,[],[12,78,3])).
% 250.13/250.08 cnf(193,plain,
% 250.13/250.08 (E(f3(x1931,f5(x1931,x1932)),f8(a4,x1931))),
% 250.13/250.08 inference(scs_inference,[],[12,78,3,2])).
% 250.13/250.08 cnf(196,plain,
% 250.13/250.08 (E(f3(a1,f3(a2,f3(a1,a2))),f8(a4,a2))),
% 250.13/250.08 inference(scs_inference,[],[12,81,3,2])).
% 250.13/250.08 cnf(202,plain,
% 250.13/250.08 (E(f8(f7(x2021),f5(x2021,x2021)),f8(a4,a4))),
% 250.13/250.08 inference(scs_inference,[],[12,85,3,2])).
% 250.13/250.08 cnf(205,plain,
% 250.13/250.08 (E(f8(a4,a4),f8(a4,f8(f7(x2051),f5(x2051,x2051))))),
% 250.13/250.08 inference(scs_inference,[],[12,202,3,2])).
% 250.13/250.08 cnf(206,plain,
% 250.13/250.08 (E(f8(a4,f8(a4,a2)),f3(a1,a2))),
% 250.13/250.08 inference(scs_inference,[],[12,143,3])).
% 250.13/250.08 cnf(208,plain,
% 250.13/250.08 (E(f3(a1,a2),f8(a4,f8(a4,a2)))),
% 250.13/250.08 inference(scs_inference,[],[12,143,3,2])).
% 250.13/250.08 cnf(211,plain,
% 250.13/250.08 (E(f8(a4,a2),f8(a4,f8(a4,f3(a1,a2))))),
% 250.13/250.08 inference(scs_inference,[],[12,146,3,2])).
% 250.13/250.08 cnf(220,plain,
% 250.13/250.08 (E(f3(a1,a2),f8(a4,f8(a4,f8(a4,a2))))),
% 250.13/250.08 inference(scs_inference,[],[12,206,3,2])).
% 250.13/250.08 cnf(226,plain,
% 250.13/250.08 (E(f8(f7(x2261),f3(x2261,x2261)),f8(a4,f8(a4,a4)))),
% 250.13/250.08 inference(scs_inference,[],[12,164,3,2])).
% 250.13/250.08 cnf(227,plain,
% 250.13/250.08 (E(f8(a4,f8(a4,x2271)),f5(x2271,f3(x2271,x2272)))),
% 250.13/250.08 inference(scs_inference,[],[12,188,3])).
% 250.13/250.08 cnf(229,plain,
% 250.13/250.08 (E(f5(x2291,f3(x2291,x2292)),f8(a4,f8(a4,x2291)))),
% 250.13/250.08 inference(scs_inference,[],[12,188,3,2])).
% 250.13/250.08 cnf(232,plain,
% 250.13/250.08 (E(f3(x2321,f5(x2321,x2322)),f8(a4,f8(a4,x2321)))),
% 250.13/250.08 inference(scs_inference,[],[12,191,3,2])).
% 250.13/250.08 cnf(235,plain,
% 250.13/250.08 (E(f5(a2,f3(a2,x2351)),f8(a4,f3(a1,a2)))),
% 250.13/250.08 inference(scs_inference,[],[12,134,3,2])).
% 250.13/250.08 cnf(236,plain,
% 250.13/250.08 (E(f8(a4,f3(a1,a2)),f3(a2,f5(a2,x2361)))),
% 250.13/250.09 inference(scs_inference,[],[12,137,3])).
% 250.13/250.09 cnf(238,plain,
% 250.13/250.09 (E(f3(a2,f5(a2,x2381)),f8(a4,f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[12,137,3,2])).
% 250.13/250.09 cnf(242,plain,
% 250.13/250.09 (E(f8(a4,a2),f3(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[12,126,3])).
% 250.13/250.09 cnf(244,plain,
% 250.13/250.09 (E(f3(f3(a1,a2),f3(a1,a2)),f8(a4,a2))),
% 250.13/250.09 inference(scs_inference,[],[12,126,3,2])).
% 250.13/250.09 cnf(247,plain,
% 250.13/250.09 (E(f3(f3(a1,a2),f3(a1,a2)),f8(a4,f8(a4,a2)))),
% 250.13/250.09 inference(scs_inference,[],[12,242,3,2])).
% 250.13/250.09 cnf(253,plain,
% 250.13/250.09 (E(a4,f8(a4,f8(f7(x2531),f5(x2531,x2531))))),
% 250.13/250.09 inference(scs_inference,[],[12,82,3,2])).
% 250.13/250.09 cnf(254,plain,
% 250.13/250.09 (E(f8(a4,f3(a1,a2)),a2)),
% 250.13/250.09 inference(scs_inference,[],[12,11,3])).
% 250.13/250.09 cnf(256,plain,
% 250.13/250.09 (E(a2,f8(a4,f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[12,11,3,2])).
% 250.13/250.09 cnf(259,plain,
% 250.13/250.09 (E(a2,f8(a4,f8(a4,f3(a1,a2))))),
% 250.13/250.09 inference(scs_inference,[],[12,254,3,2])).
% 250.13/250.09 cnf(262,plain,
% 250.13/250.09 (E(a4,f8(a4,f8(f7(x2621),x2621)))),
% 250.13/250.09 inference(scs_inference,[],[12,15,3,2])).
% 250.13/250.09 cnf(265,plain,
% 250.13/250.09 (E(f8(a4,f8(a4,a2)),f5(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,208,3,2])).
% 250.13/250.09 cnf(266,plain,
% 250.13/250.09 (E(f5(a2,a2),f8(a4,f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,256,3])).
% 250.13/250.09 cnf(268,plain,
% 250.13/250.09 (E(f8(a4,f3(a1,a2)),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[13,256,3,2])).
% 250.13/250.09 cnf(271,plain,
% 250.13/250.09 (E(f8(a4,f8(a4,f3(a1,a2))),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[13,259,3,2])).
% 250.13/250.09 cnf(280,plain,
% 250.13/250.09 (E(f8(a4,f8(f7(x2801),x2801)),f5(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[13,262,3,2])).
% 250.13/250.09 cnf(281,plain,
% 250.13/250.09 (E(f5(a2,a2),f3(a1,a2))),
% 250.13/250.09 inference(scs_inference,[],[13,132,3])).
% 250.13/250.09 cnf(283,plain,
% 250.13/250.09 (E(f3(a1,a2),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[13,132,3,2])).
% 250.13/250.09 cnf(286,plain,
% 250.13/250.09 (E(f5(a2,a2),f5(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,283,3,2])).
% 250.13/250.09 cnf(289,plain,
% 250.13/250.09 (E(f5(f3(a1,a2),f3(a1,a2)),f5(f5(a2,a2),f5(a2,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,286,3,2])).
% 250.13/250.09 cnf(292,plain,
% 250.13/250.09 (E(f8(a4,f3(a1,a2)),f5(f8(a4,a2),f8(a4,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,148,3,2])).
% 250.13/250.09 cnf(295,plain,
% 250.13/250.09 (E(f8(a4,a2),f5(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,145,3,2])).
% 250.13/250.09 cnf(298,plain,
% 250.13/250.09 (E(f5(f3(a1,a2),f3(a1,a2)),f5(f8(a4,a2),f8(a4,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,295,3,2])).
% 250.13/250.09 cnf(301,plain,
% 250.13/250.09 (E(f8(a4,f3(f3(a1,a2),f3(a1,a2))),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[13,142,3,2])).
% 250.13/250.09 cnf(302,plain,
% 250.13/250.09 (E(f5(a4,a4),f8(f3(f7(x3021),f7(x3021)),f5(x3021,x3021)))),
% 250.13/250.09 inference(scs_inference,[],[13,96,3])).
% 250.13/250.09 cnf(304,plain,
% 250.13/250.09 (E(f8(f3(f7(x3041),f7(x3041)),f5(x3041,x3041)),f5(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[13,96,3,2])).
% 250.13/250.09 cnf(307,plain,
% 250.13/250.09 (E(f8(f7(x3071),f3(x3071,x3071)),f5(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[13,108,3,2])).
% 250.13/250.09 cnf(322,plain,
% 250.13/250.09 (E(f8(f3(f7(x3221),f7(x3221)),x3221),f5(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[13,118,3,2])).
% 250.13/250.09 cnf(323,plain,
% 250.13/250.09 (E(f5(x3231,x3231),f5(x3231,f3(x3231,x3232)))),
% 250.13/250.09 inference(scs_inference,[],[13,67,3])).
% 250.13/250.09 cnf(325,plain,
% 250.13/250.09 (E(f5(x3251,f3(x3251,x3252)),f5(x3251,x3251))),
% 250.13/250.09 inference(scs_inference,[],[13,67,3,2])).
% 250.13/250.09 cnf(326,plain,
% 250.13/250.09 (E(f5(x3261,x3261),f3(x3261,f5(x3261,x3262)))),
% 250.13/250.09 inference(scs_inference,[],[13,78,3])).
% 250.13/250.09 cnf(328,plain,
% 250.13/250.09 (E(f3(x3281,f5(x3281,x3282)),f5(x3281,x3281))),
% 250.13/250.09 inference(scs_inference,[],[13,78,3,2])).
% 250.13/250.09 cnf(331,plain,
% 250.13/250.09 (E(f3(a1,f3(a2,f3(a1,a2))),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[13,81,3,2])).
% 250.13/250.09 cnf(335,plain,
% 250.13/250.09 (E(f5(a4,a4),f8(f7(x3351),f5(x3351,x3351)))),
% 250.13/250.09 inference(scs_inference,[],[13,85,3])).
% 250.13/250.09 cnf(337,plain,
% 250.13/250.09 (E(f8(f7(x3371),f5(x3371,x3371)),f5(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[13,85,3,2])).
% 250.13/250.09 cnf(340,plain,
% 250.13/250.09 (E(f5(x3401,f3(x3401,x3402)),f5(f5(x3401,x3401),f5(x3401,x3401)))),
% 250.13/250.09 inference(scs_inference,[],[13,323,3,2])).
% 250.13/250.09 cnf(343,plain,
% 250.13/250.09 (E(f3(x3431,f5(x3431,x3432)),f5(f5(x3431,x3431),f5(x3431,x3431)))),
% 250.13/250.09 inference(scs_inference,[],[13,326,3,2])).
% 250.13/250.09 cnf(346,plain,
% 250.13/250.09 (E(f8(a4,f3(a1,a2)),f5(f5(a2,a2),f5(a2,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,266,3,2])).
% 250.13/250.09 cnf(347,plain,
% 250.13/250.09 (E(f5(f5(a4,a4),f5(a4,a4)),f8(f7(x3471),f5(x3471,x3471)))),
% 250.13/250.09 inference(scs_inference,[],[13,335,3])).
% 250.13/250.09 cnf(350,plain,
% 250.13/250.09 (E(f5(f5(a2,a2),f5(a2,a2)),f3(a1,a2))),
% 250.13/250.09 inference(scs_inference,[],[13,281,3])).
% 250.13/250.09 cnf(352,plain,
% 250.13/250.09 (E(f3(a1,a2),f5(f5(a2,a2),f5(a2,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,281,3,2])).
% 250.13/250.09 cnf(367,plain,
% 250.13/250.09 (E(f3(a1,a2),f5(f8(a4,a2),f8(a4,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,143,3,2])).
% 250.13/250.09 cnf(370,plain,
% 250.13/250.09 (E(f3(f3(a1,a2),f3(a1,a2)),f5(f8(a4,a2),f8(a4,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,242,3,2])).
% 250.13/250.09 cnf(385,plain,
% 250.13/250.09 (E(f5(x3851,f3(x3851,x3852)),f5(f8(a4,x3851),f8(a4,x3851)))),
% 250.13/250.09 inference(scs_inference,[],[13,188,3,2])).
% 250.13/250.09 cnf(388,plain,
% 250.13/250.09 (E(f3(x3881,f5(x3881,x3882)),f5(f8(a4,x3881),f8(a4,x3881)))),
% 250.13/250.09 inference(scs_inference,[],[13,191,3,2])).
% 250.13/250.09 cnf(391,plain,
% 250.13/250.09 (E(f5(a2,f3(a2,x3911)),f5(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,134,3,2])).
% 250.13/250.09 cnf(394,plain,
% 250.13/250.09 (E(f3(a2,f5(a2,x3941)),f5(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,137,3,2])).
% 250.13/250.09 cnf(398,plain,
% 250.13/250.09 (E(f5(a2,a2),f3(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,126,3])).
% 250.13/250.09 cnf(400,plain,
% 250.13/250.09 (E(f3(f3(a1,a2),f3(a1,a2)),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[13,126,3,2])).
% 250.13/250.09 cnf(403,plain,
% 250.13/250.09 (E(f3(f3(a1,a2),f3(a1,a2)),f5(f5(a2,a2),f5(a2,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,398,3,2])).
% 250.13/250.09 cnf(404,plain,
% 250.13/250.09 (E(f5(f3(a1,a2),f3(a1,a2)),a2)),
% 250.13/250.09 inference(scs_inference,[],[13,11,3])).
% 250.13/250.09 cnf(406,plain,
% 250.13/250.09 (E(a2,f5(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[13,11,3,2])).
% 250.13/250.09 cnf(409,plain,
% 250.13/250.09 (E(f5(f3(a1,a2),f3(a1,a2)),f3(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[14,406,3,2])).
% 250.13/250.09 cnf(413,plain,
% 250.13/250.09 (E(f3(a2,a2),f8(a4,f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,256,3])).
% 250.13/250.09 cnf(415,plain,
% 250.13/250.09 (E(f8(a4,f3(a1,a2)),f3(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[14,256,3,2])).
% 250.13/250.09 cnf(418,plain,
% 250.13/250.09 (E(f8(a4,f8(a4,f3(a1,a2))),f3(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[14,259,3,2])).
% 250.13/250.09 cnf(421,plain,
% 250.13/250.09 (E(f5(f3(a1,a2),f3(a1,a2)),f3(f5(a2,a2),f5(a2,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,286,3,2])).
% 250.13/250.09 cnf(427,plain,
% 250.13/250.09 (E(f8(a4,f8(f7(x4271),f5(x4271,x4271))),f3(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[14,253,3,2])).
% 250.13/250.09 cnf(431,plain,
% 250.13/250.09 (E(f3(a2,a2),f3(a1,a2))),
% 250.13/250.09 inference(scs_inference,[],[14,132,3])).
% 250.13/250.09 cnf(433,plain,
% 250.13/250.09 (E(f3(a1,a2),f3(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[14,132,3,2])).
% 250.13/250.09 cnf(442,plain,
% 250.13/250.09 (E(f8(a4,f3(a1,a2)),f3(f8(a4,a2),f8(a4,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,148,3,2])).
% 250.13/250.09 cnf(446,plain,
% 250.13/250.09 (E(f3(a4,a4),f8(f3(f7(x4461),f7(x4461)),f5(x4461,x4461)))),
% 250.13/250.09 inference(scs_inference,[],[14,96,3])).
% 250.13/250.09 cnf(448,plain,
% 250.13/250.09 (E(f8(f3(f7(x4481),f7(x4481)),f5(x4481,x4481)),f3(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[14,96,3,2])).
% 250.13/250.09 cnf(449,plain,
% 250.13/250.09 (E(f3(a4,a4),f8(f7(x4491),f3(x4491,x4491)))),
% 250.13/250.09 inference(scs_inference,[],[14,108,3])).
% 250.13/250.09 cnf(467,plain,
% 250.13/250.09 (E(f3(x4671,x4671),f5(x4671,f3(x4671,x4672)))),
% 250.13/250.09 inference(scs_inference,[],[14,67,3])).
% 250.13/250.09 cnf(469,plain,
% 250.13/250.09 (E(f5(x4691,f3(x4691,x4692)),f3(x4691,x4691))),
% 250.13/250.09 inference(scs_inference,[],[14,67,3,2])).
% 250.13/250.09 cnf(470,plain,
% 250.13/250.09 (E(f3(x4701,x4701),f3(x4701,f5(x4701,x4702)))),
% 250.13/250.09 inference(scs_inference,[],[14,78,3])).
% 250.13/250.09 cnf(472,plain,
% 250.13/250.09 (E(f3(x4721,f5(x4721,x4722)),f3(x4721,x4721))),
% 250.13/250.09 inference(scs_inference,[],[14,78,3,2])).
% 250.13/250.09 cnf(475,plain,
% 250.13/250.09 (E(f3(a1,f3(a2,f3(a1,a2))),f3(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[14,81,3,2])).
% 250.13/250.09 cnf(476,plain,
% 250.13/250.09 (E(f3(a4,a4),f8(f5(f7(x4761),f7(x4761)),f5(x4761,x4761)))),
% 250.13/250.09 inference(scs_inference,[],[14,91,3])).
% 250.13/250.09 cnf(484,plain,
% 250.13/250.09 (E(f5(x4841,f3(x4841,x4842)),f3(f3(x4841,x4841),f3(x4841,x4841)))),
% 250.13/250.09 inference(scs_inference,[],[14,467,3,2])).
% 250.13/250.09 cnf(487,plain,
% 250.13/250.09 (E(f3(x4871,f5(x4871,x4872)),f3(f3(x4871,x4871),f3(x4871,x4871)))),
% 250.13/250.09 inference(scs_inference,[],[14,470,3,2])).
% 250.13/250.09 cnf(493,plain,
% 250.13/250.09 (E(f8(a4,f3(a1,a2)),f3(f3(a2,a2),f3(a2,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,413,3,2])).
% 250.13/250.09 cnf(496,plain,
% 250.13/250.09 (E(f3(a1,a2),f3(f3(a2,a2),f3(a2,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,431,3,2])).
% 250.13/250.09 cnf(502,plain,
% 250.13/250.09 (E(f8(f5(f7(x5021),f7(x5021)),f5(x5021,x5021)),f3(f3(a4,a4),f3(a4,a4)))),
% 250.13/250.09 inference(scs_inference,[],[14,476,3,2])).
% 250.13/250.09 cnf(506,plain,
% 250.13/250.09 (E(f3(f3(a4,a4),f3(a4,a4)),f8(f7(x5061),f3(x5061,x5061)))),
% 250.13/250.09 inference(scs_inference,[],[14,449,3])).
% 250.13/250.09 cnf(509,plain,
% 250.13/250.09 (E(f3(f3(a4,a4),f3(a4,a4)),f8(f3(f7(x5091),f7(x5091)),f5(x5091,x5091)))),
% 250.13/250.09 inference(scs_inference,[],[14,446,3])).
% 250.13/250.09 cnf(514,plain,
% 250.13/250.09 (E(f3(a1,a2),f3(f5(a2,a2),f5(a2,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,281,3,2])).
% 250.13/250.09 cnf(517,plain,
% 250.13/250.09 (E(f3(f5(a2,a2),f5(a2,a2)),f3(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,514,3,2])).
% 250.13/250.09 cnf(520,plain,
% 250.13/250.09 (E(f8(a4,f3(a1,a2)),f3(f5(a2,a2),f5(a2,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,266,3,2])).
% 250.13/250.09 cnf(523,plain,
% 250.13/250.09 (E(f5(x5231,f3(x5231,x5232)),f3(f5(x5231,x5231),f5(x5231,x5231)))),
% 250.13/250.09 inference(scs_inference,[],[14,323,3,2])).
% 250.13/250.09 cnf(526,plain,
% 250.13/250.09 (E(f3(x5261,f5(x5261,x5262)),f3(f5(x5261,x5261),f5(x5261,x5261)))),
% 250.13/250.09 inference(scs_inference,[],[14,326,3,2])).
% 250.13/250.09 cnf(541,plain,
% 250.13/250.09 (E(f8(f3(f7(x5411),f7(x5411)),f5(x5411,x5411)),f3(f5(a4,a4),f5(a4,a4)))),
% 250.13/250.09 inference(scs_inference,[],[14,302,3,2])).
% 250.13/250.09 cnf(542,plain,
% 250.13/250.09 (E(f3(f8(a4,a2),f8(a4,a2)),f3(a1,a2))),
% 250.13/250.09 inference(scs_inference,[],[14,143,3])).
% 250.13/250.09 cnf(544,plain,
% 250.13/250.09 (E(f3(a1,a2),f3(f8(a4,a2),f8(a4,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,143,3,2])).
% 250.13/250.09 cnf(547,plain,
% 250.13/250.09 (E(f3(f8(a4,a2),f8(a4,a2)),f3(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,544,3,2])).
% 250.13/250.09 cnf(562,plain,
% 250.13/250.09 (E(f5(x5621,f3(x5621,x5622)),f3(f8(a4,x5621),f8(a4,x5621)))),
% 250.13/250.09 inference(scs_inference,[],[14,188,3,2])).
% 250.13/250.09 cnf(565,plain,
% 250.13/250.09 (E(f3(x5651,f5(x5651,x5652)),f3(f8(a4,x5651),f8(a4,x5651)))),
% 250.13/250.09 inference(scs_inference,[],[14,191,3,2])).
% 250.13/250.09 cnf(568,plain,
% 250.13/250.09 (E(f5(a2,f3(a2,x5681)),f3(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,134,3,2])).
% 250.13/250.09 cnf(571,plain,
% 250.13/250.09 (E(f3(a2,f5(a2,x5711)),f3(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[14,137,3,2])).
% 250.13/250.09 cnf(575,plain,
% 250.13/250.09 (E(f5(f3(a1,a2),f3(f3(a1,a2),x5751)),f8(a4,a2))),
% 250.13/250.09 inference(scs_inference,[],[244,469,3])).
% 250.13/250.09 cnf(578,plain,
% 250.13/250.09 (E(f8(a4,a2),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[271,211,3])).
% 250.13/250.09 cnf(579,plain,
% 250.13/250.09 (E(f5(a2,a2),f8(a4,a2))),
% 250.13/250.09 inference(scs_inference,[],[271,211,3,2])).
% 250.13/250.09 cnf(580,plain,
% 250.13/250.09 (E(f3(f3(a1,a2),f5(f3(a1,a2),x5801)),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[400,472,3])).
% 250.13/250.09 cnf(586,plain,
% 250.13/250.09 (E(f5(f3(a1,a2),f3(a1,a2)),f8(a4,f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[154,265,3,2])).
% 250.13/250.09 cnf(588,plain,
% 250.13/250.09 (E(f5(f8(a4,a2),f8(a4,a2)),f3(f8(a4,a2),f8(a4,a2)))),
% 250.13/250.09 inference(scs_inference,[],[370,547,3,2])).
% 250.13/250.09 cnf(592,plain,
% 250.13/250.09 (E(f5(a2,f5(a2,f5(a2,a2))),f8(a4,a2))),
% 250.13/250.09 inference(scs_inference,[],[71,579,3])).
% 250.13/250.09 cnf(595,plain,
% 250.13/250.09 (E(f5(f3(a1,a2),f3(f3(a1,a2),x5951)),f3(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[325,409,3])).
% 250.13/250.09 cnf(599,plain,
% 250.13/250.09 (E(f3(f3(a1,a2),f3(a1,a2)),f5(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[421,517,3,2])).
% 250.13/250.09 cnf(600,plain,
% 250.13/250.09 (E(f3(f3(a1,a2),f5(f3(a1,a2),x6001)),f3(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[328,409,3])).
% 250.13/250.09 cnf(604,plain,
% 250.13/250.09 (E(f8(a4,f3(a1,a2)),f3(f3(a1,a2),f3(a1,a2)))),
% 250.13/250.09 inference(scs_inference,[],[586,599,3,2])).
% 250.13/250.09 cnf(605,plain,
% 250.13/250.09 (E(f5(f3(a1,a2),f3(f3(a1,a2),x6051)),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[268,190,3])).
% 250.13/250.09 cnf(607,plain,
% 250.13/250.09 (E(f5(a2,a2),f5(f3(a1,a2),f3(f3(a1,a2),x6071)))),
% 250.13/250.09 inference(scs_inference,[],[268,190,3,2])).
% 250.13/250.09 cnf(609,plain,
% 250.13/250.09 (E(f8(f3(f7(x6091),f7(x6091)),f5(x6091,x6091)),f8(f7(x6092),x6092))),
% 250.13/250.09 inference(scs_inference,[],[15,96,3,2])).
% 250.13/250.09 cnf(612,plain,
% 250.13/250.09 (E(f8(f7(x6121),x6121),f8(f7(x6122),f5(x6122,x6122)))),
% 250.13/250.09 inference(scs_inference,[],[609,98,3,2])).
% 250.13/250.09 cnf(615,plain,
% 250.13/250.09 (E(f8(f5(f7(x6151),f7(x6151)),f5(x6151,x6151)),f8(f7(x6152),x6152))),
% 250.13/250.09 inference(scs_inference,[],[612,93,3,2])).
% 250.13/250.09 cnf(624,plain,
% 250.13/250.09 (E(f3(a4,f5(a4,x6241)),f8(f7(x6242),x6242))),
% 250.13/250.09 inference(scs_inference,[],[15,78,3,2])).
% 250.13/250.09 cnf(625,plain,
% 250.13/250.09 (E(f5(a2,f5(a2,f5(a2,a2))),f3(a1,a2))),
% 250.13/250.09 inference(scs_inference,[],[101,350,3])).
% 250.13/250.09 cnf(627,plain,
% 250.13/250.09 (E(f3(a1,a2),f5(a2,f5(a2,f5(a2,a2))))),
% 250.13/250.09 inference(scs_inference,[],[101,350,3,2])).
% 250.13/250.09 cnf(630,plain,
% 250.13/250.09 (E(f8(f3(f7(x6301),f7(x6301)),f5(x6301,x6301)),f5(a4,f3(a4,x6302)))),
% 250.13/250.09 inference(scs_inference,[],[484,509,3,2])).
% 250.13/250.09 cnf(633,plain,
% 250.13/250.09 (E(f8(f7(x6331),f3(x6331,x6331)),f3(a4,f5(a4,x6332)))),
% 250.13/250.09 inference(scs_inference,[],[487,506,3,2])).
% 250.13/250.09 cnf(636,plain,
% 250.13/250.09 (E(f3(a4,f5(a4,x6361)),f8(f3(f7(x6362),f7(x6362)),f5(x6362,x6362)))),
% 250.13/250.09 inference(scs_inference,[],[125,633,3,2])).
% 250.13/250.09 cnf(637,plain,
% 250.13/250.09 (E(f3(a4,f5(a4,x6371)),f5(a4,f3(a4,x6372)))),
% 250.13/250.09 inference(scs_inference,[],[630,636,3])).
% 250.13/250.09 cnf(651,plain,
% 250.13/250.09 (E(f8(f7(x6511),f5(x6511,x6511)),f3(a4,f5(a4,x6512)))),
% 250.13/250.09 inference(scs_inference,[],[343,347,3,2])).
% 250.13/250.09 cnf(652,plain,
% 250.13/250.09 (E(f5(a2,a2),f3(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[607,595,3])).
% 250.13/250.09 cnf(654,plain,
% 250.13/250.09 (E(f3(a2,a2),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[607,595,3,2])).
% 250.13/250.09 cnf(662,plain,
% 250.13/250.09 (E(f5(f8(a4,a2),f3(f8(a4,a2),x6621)),f3(a1,a2))),
% 250.13/250.09 inference(scs_inference,[],[220,227,3,2])).
% 250.13/250.09 cnf(664,plain,
% 250.13/250.09 (E(f5(a2,a2),f5(f8(a4,a2),f3(f8(a4,a2),x6641)))),
% 250.13/250.09 inference(scs_inference,[],[662,283,3,2])).
% 250.13/250.09 cnf(667,plain,
% 250.13/250.09 (E(f8(a4,f8(a4,f8(a4,a2))),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[664,229,3,2])).
% 250.13/250.09 cnf(672,plain,
% 250.13/250.09 (E(f5(a4,f3(a4,x6721)),f8(f7(x6722),f5(x6722,x6722)))),
% 250.13/250.09 inference(scs_inference,[],[651,637,3,2])).
% 250.13/250.09 cnf(675,plain,
% 250.13/250.09 (E(f3(f3(a1,a2),f5(f3(a1,a2),x6751)),f8(a4,a2))),
% 250.13/250.09 inference(scs_inference,[],[193,146,3])).
% 250.13/250.09 cnf(678,plain,
% 250.13/250.09 (E(f3(f8(a4,a2),f5(f8(a4,a2),x6781)),f5(a2,a2))),
% 250.13/250.09 inference(scs_inference,[],[667,232,3])).
% 250.13/250.09 cnf(680,plain,
% 250.13/250.09 (E(f5(a2,a2),f3(f8(a4,a2),f5(f8(a4,a2),x6801)))),
% 250.13/250.09 inference(scs_inference,[],[678,2])).
% 250.13/250.09 cnf(681,plain,
% 250.13/250.09 (E(f8(a4,a4),f5(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[175,280,678,2,3])).
% 250.13/250.09 cnf(683,plain,
% 250.13/250.09 (E(f5(a4,a4),f8(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[681,2])).
% 250.13/250.09 cnf(684,plain,
% 250.13/250.09 (E(f8(a4,a4),f3(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[205,427,681,2,3])).
% 250.13/250.09 cnf(686,plain,
% 250.13/250.09 (E(f3(a4,a4),f8(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[684,2])).
% 250.13/250.09 cnf(687,plain,
% 250.13/250.09 (E(f5(a4,a4),f3(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[683,684,2,3])).
% 250.13/250.09 cnf(688,plain,
% 250.13/250.09 (E(f3(a4,a4),f5(a4,a4))),
% 250.13/250.09 inference(scs_inference,[],[687,2])).
% 250.13/250.09 cnf(689,plain,
% 250.13/250.09 (E(f5(a2,f3(a2,x6891)),f3(a2,f5(a2,x6892)))),
% 250.19/250.09 inference(scs_inference,[],[235,687,236,2,3])).
% 250.19/250.09 cnf(691,plain,
% 250.19/250.09 (E(f8(a4,f3(f3(a1,a2),f3(a1,a2))),f3(a1,a2))),
% 250.19/250.09 inference(scs_inference,[],[301,689,281,2,3])).
% 250.19/250.09 cnf(692,plain,
% 250.19/250.09 (E(f3(a1,a2),f8(a4,f3(f3(a1,a2),f3(a1,a2))))),
% 250.19/250.09 inference(scs_inference,[],[691,2])).
% 250.19/250.09 cnf(696,plain,
% 250.19/250.09 (E(f3(f5(x6961,x6961),f5(x6961,x6961)),f5(f3(x6961,x6962),x6961))),
% 250.19/250.09 inference(scs_inference,[],[16,523,3,2])).
% 250.19/250.09 cnf(706,plain,
% 250.19/250.09 (E(f5(f8(a4,x7061),f8(a4,x7061)),f5(f3(x7061,x7062),x7061))),
% 250.19/250.09 inference(scs_inference,[],[16,385,3,2])).
% 250.19/250.09 cnf(710,plain,
% 250.19/250.09 (E(f3(f8(a4,x7101),f8(a4,x7101)),f5(f3(x7101,x7102),x7101))),
% 250.19/250.09 inference(scs_inference,[],[16,562,3,2])).
% 250.19/250.09 cnf(716,plain,
% 250.19/250.09 (E(f3(f3(a1,a2),f3(a1,a2)),f5(f3(a2,x7161),a2))),
% 250.19/250.09 inference(scs_inference,[],[16,568,3,2])).
% 250.19/250.09 cnf(718,plain,
% 250.19/250.09 (E(f5(f3(a2,x7181),a2),f8(a4,f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[604,716,3,2])).
% 250.19/250.10 cnf(722,plain,
% 250.19/250.10 (E(f5(f5(x7221,x7222),x7223),f5(f5(x7222,x7223),x7221))),
% 250.19/250.10 inference(scs_inference,[],[16,101,3,2])).
% 250.19/250.10 cnf(726,plain,
% 250.19/250.10 (E(f3(f3(x7261,x7261),f3(x7261,x7261)),f5(f3(x7261,x7262),x7261))),
% 250.19/250.10 inference(scs_inference,[],[16,484,3,2])).
% 250.19/250.10 cnf(736,plain,
% 250.19/250.10 (E(f5(f5(x7361,x7361),f5(x7361,x7361)),f5(f3(x7361,x7362),x7361))),
% 250.19/250.10 inference(scs_inference,[],[16,340,3,2])).
% 250.19/250.10 cnf(739,plain,
% 250.19/250.10 (E(f5(f3(a4,x7391),a4),f8(f3(f7(x7392),f7(x7392)),f5(x7392,x7392)))),
% 250.19/250.10 inference(scs_inference,[],[541,696,3,2])).
% 250.19/250.10 cnf(745,plain,
% 250.19/250.10 (E(f5(a4,a4),f5(f3(a4,x7451),a4))),
% 250.19/250.10 inference(scs_inference,[],[304,739,3,2])).
% 250.19/250.10 cnf(746,plain,
% 250.19/250.10 (E(f5(f3(f8(a4,a2),x7461),f8(a4,a2)),f3(a1,a2))),
% 250.19/250.10 inference(scs_inference,[],[16,662,3])).
% 250.19/250.10 cnf(748,plain,
% 250.19/250.10 (E(f3(a1,a2),f5(f3(f8(a4,a2),x7481),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[746,2])).
% 250.19/250.10 cnf(749,plain,
% 250.19/250.10 (E(f5(f3(x7491,x7492),x7491),f8(a4,f8(a4,x7491)))),
% 250.19/250.10 inference(scs_inference,[],[16,229,746,2,3])).
% 250.19/250.10 cnf(752,plain,
% 250.19/250.10 (E(f8(a4,f8(a4,x7521)),f5(f3(x7521,x7522),x7521))),
% 250.19/250.10 inference(scs_inference,[],[749,2])).
% 250.19/250.10 cnf(753,plain,
% 250.19/250.10 (E(f5(f3(a4,x7531),a4),f8(f7(x7532),f5(x7532,x7532)))),
% 250.19/250.10 inference(scs_inference,[],[16,672,749,2,3])).
% 250.19/250.10 cnf(755,plain,
% 250.19/250.10 (E(f8(f7(x7551),f5(x7551,x7551)),f5(f3(a4,x7552),a4))),
% 250.19/250.10 inference(scs_inference,[],[753,2])).
% 250.19/250.10 cnf(756,plain,
% 250.19/250.10 (E(f5(f3(a2,x7561),a2),f5(f3(a1,a2),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[16,391,753,2,3])).
% 250.19/250.10 cnf(758,plain,
% 250.19/250.10 (E(f5(f3(a1,a2),f3(a1,a2)),f5(f3(a2,x7581),a2))),
% 250.19/250.10 inference(scs_inference,[],[756,2])).
% 250.19/250.10 cnf(759,plain,
% 250.19/250.10 (E(f3(a2,f5(a2,x7591)),f5(f3(a2,x7592),a2))),
% 250.19/250.10 inference(scs_inference,[],[571,716,756,2,3])).
% 250.19/250.10 cnf(761,plain,
% 250.19/250.10 (E(f5(f3(a2,x7611),a2),f3(a1,a2))),
% 250.19/250.10 inference(scs_inference,[],[16,136,759,2,3])).
% 250.19/250.10 cnf(763,plain,
% 250.19/250.10 (E(f3(a1,a2),f5(f3(a2,x7631),a2))),
% 250.19/250.10 inference(scs_inference,[],[761,2])).
% 250.19/250.10 cnf(774,plain,
% 250.19/250.10 (E(f5(f5(x7741,x7742),f3(f5(x7741,x7742),x7743)),f5(x7742,x7741))),
% 250.19/250.10 inference(scs_inference,[],[16,67,3,2])).
% 250.19/250.10 cnf(777,plain,
% 250.19/250.10 (E(f3(f5(x7771,x7772),f5(f5(x7771,x7772),x7773)),f5(x7772,x7771))),
% 250.19/250.10 inference(scs_inference,[],[16,78,3,2])).
% 250.19/250.10 cnf(778,plain,
% 250.19/250.10 (E(f5(f5(a2,f5(a2,a2)),a2),f8(a4,a2))),
% 250.19/250.10 inference(scs_inference,[],[16,592,3])).
% 250.19/250.10 cnf(781,plain,
% 250.19/250.10 (E(f5(f5(a2,f5(a2,a2)),a2),f3(a1,a2))),
% 250.19/250.10 inference(scs_inference,[],[16,625,778,2,3])).
% 250.19/250.10 cnf(783,plain,
% 250.19/250.10 (E(f3(a1,a2),f5(f5(a2,f5(a2,a2)),a2))),
% 250.19/250.10 inference(scs_inference,[],[781,2])).
% 250.19/250.10 cnf(784,plain,
% 250.19/250.10 (E(f3(x7841,f5(x7841,x7842)),f5(f3(x7841,x7843),x7841))),
% 250.19/250.10 inference(scs_inference,[],[526,696,781,2,3])).
% 250.19/250.10 cnf(786,plain,
% 250.19/250.10 (E(f5(f3(x7861,x7862),x7861),f3(x7861,f5(x7861,x7863)))),
% 250.19/250.10 inference(scs_inference,[],[784,2])).
% 250.19/250.10 cnf(787,plain,
% 250.19/250.10 (E(f5(a2,a2),f5(f3(f8(a4,a2),x7871),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[680,784,2,3])).
% 250.19/250.10 cnf(789,plain,
% 250.19/250.10 (E(f5(f3(f8(a4,a2),x7891),f8(a4,a2)),f5(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[787,2])).
% 250.19/250.10 cnf(790,plain,
% 250.19/250.10 (E(f5(x7901,f3(x7901,x7902)),f3(x7901,f5(x7901,x7903)))),
% 250.19/250.10 inference(scs_inference,[],[16,786,787,2,3])).
% 250.19/250.10 cnf(793,plain,
% 250.19/250.10 (E(f3(x7931,f5(x7931,x7932)),f5(x7931,f3(x7931,x7933)))),
% 250.19/250.10 inference(scs_inference,[],[790,2])).
% 250.19/250.10 cnf(794,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x7941),f3(a1,a2)),f5(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[16,790,605,2,3])).
% 250.19/250.10 cnf(796,plain,
% 250.19/250.10 (E(f5(a2,a2),f5(f3(f3(a1,a2),x7961),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[794,2])).
% 250.19/250.10 cnf(797,plain,
% 250.19/250.10 (E(f5(x7971,x7972),f5(x7972,f5(x7971,f5(x7972,x7971))))),
% 250.19/250.10 inference(scs_inference,[],[16,794,68,2,3])).
% 250.19/250.10 cnf(799,plain,
% 250.19/250.10 (E(f5(x7991,f5(x7992,f5(x7991,x7992))),f5(x7992,x7991))),
% 250.19/250.10 inference(scs_inference,[],[797,2])).
% 250.19/250.10 cnf(800,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x8001),f3(a1,a2)),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[16,797,595,2,3])).
% 250.19/250.10 cnf(802,plain,
% 250.19/250.10 (E(f3(a2,a2),f5(f3(f3(a1,a2),x8021),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[800,2])).
% 250.19/250.10 cnf(803,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x8031),f3(a1,a2)),f8(a4,a2))),
% 250.19/250.10 inference(scs_inference,[],[16,800,575,2,3])).
% 250.19/250.10 cnf(805,plain,
% 250.19/250.10 (E(f8(a4,a2),f5(f3(f3(a1,a2),x8051),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[803,2])).
% 250.19/250.10 cnf(806,plain,
% 250.19/250.10 (E(f8(a4,f3(a1,a2)),f5(f3(f3(a1,a2),x8061),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[415,802,803,2,3])).
% 250.19/250.10 cnf(807,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x8071),f3(a1,a2)),f8(a4,f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[806,2])).
% 250.19/250.10 cnf(808,plain,
% 250.19/250.10 (E(f3(a2,f5(a2,x8081)),f5(f3(f3(a1,a2),x8082),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[238,806,2,3])).
% 250.19/250.10 cnf(809,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x8091),f3(a1,a2)),f3(a2,f5(a2,x8092)))),
% 250.19/250.10 inference(scs_inference,[],[808,2])).
% 250.19/250.10 cnf(810,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x8101),f3(a1,a2)),f5(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[292,807,808,2,3])).
% 250.19/250.10 cnf(811,plain,
% 250.19/250.10 (E(f5(f8(a4,a2),f8(a4,a2)),f5(f3(f3(a1,a2),x8111),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[810,2])).
% 250.19/250.10 cnf(812,plain,
% 250.19/250.10 (E(f5(f3(a2,x8121),a2),f5(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[718,268,810,2,3])).
% 250.19/250.10 cnf(813,plain,
% 250.19/250.10 (E(f5(a2,a2),f5(f3(a2,x8131),a2))),
% 250.19/250.10 inference(scs_inference,[],[812,2])).
% 250.19/250.10 cnf(814,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x8141),f3(a1,a2)),f5(f3(a1,a2),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[809,394,812,2,3])).
% 250.19/250.10 cnf(816,plain,
% 250.19/250.10 (E(f5(f3(a1,a2),f3(a1,a2)),f5(f3(f3(a1,a2),x8161),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[814,2])).
% 250.19/250.10 cnf(817,plain,
% 250.19/250.10 (E(f8(a4,f8(a4,f3(a1,a2))),f3(a1,a2))),
% 250.19/250.10 inference(scs_inference,[],[418,814,431,2,3])).
% 250.19/250.10 cnf(818,plain,
% 250.19/250.10 (E(f3(a1,a2),f8(a4,f8(a4,f3(a1,a2))))),
% 250.19/250.10 inference(scs_inference,[],[817,2])).
% 250.19/250.10 cnf(819,plain,
% 250.19/250.10 (E(f5(x8191,f5(x8192,x8193)),f5(x8192,f5(x8193,x8191)))),
% 250.19/250.10 inference(scs_inference,[],[16,817,20,2,3])).
% 250.19/250.10 cnf(822,plain,
% 250.19/250.10 (E(f5(x8221,f5(x8222,x8223)),f5(x8223,f5(x8221,x8222)))),
% 250.19/250.10 inference(scs_inference,[],[819,2])).
% 250.19/250.10 cnf(823,plain,
% 250.19/250.10 (E(f3(a1,a2),f5(f3(f3(a1,a2),x8231),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[818,752,819,2,3])).
% 250.19/250.10 cnf(825,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x8251),f3(a1,a2)),f3(a1,a2))),
% 250.19/250.10 inference(scs_inference,[],[823,2])).
% 250.19/250.10 cnf(826,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x8261),f3(a1,a2)),f5(f5(a2,a2),f5(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[825,352,3])).
% 250.19/250.10 cnf(827,plain,
% 250.19/250.10 (E(f5(f5(a2,a2),f5(a2,a2)),f5(f3(f3(a1,a2),x8271),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[825,352,3,2])).
% 250.19/250.10 cnf(828,plain,
% 250.19/250.10 (E(f3(f3(a2,f3(a1,a2)),a1),f8(a4,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,196,3])).
% 250.19/250.10 cnf(831,plain,
% 250.19/250.10 (E(f3(f3(a2,f3(a1,a2)),a1),f5(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,331,828,2,3])).
% 250.19/250.10 cnf(834,plain,
% 250.19/250.10 (E(f3(f3(a2,f3(a1,a2)),a1),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,475,831,2,3])).
% 250.19/250.10 cnf(837,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[17,367,834,2,3])).
% 250.19/250.10 cnf(840,plain,
% 250.19/250.10 (E(f3(a2,a1),f3(f3(a2,a2),f3(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[17,496,837,2,3])).
% 250.19/250.10 cnf(843,plain,
% 250.19/250.10 (E(f3(f5(x8431,x8432),x8431),f5(x8431,f3(x8431,x8433)))),
% 250.19/250.10 inference(scs_inference,[],[17,793,840,2,3])).
% 250.19/250.10 cnf(846,plain,
% 250.19/250.10 (E(f5(x8461,f3(x8461,x8462)),f3(f5(x8461,x8463),x8461))),
% 250.19/250.10 inference(scs_inference,[],[843,2])).
% 250.19/250.10 cnf(847,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(a2,f5(a2,f5(a2,a2))))),
% 250.19/250.10 inference(scs_inference,[],[17,627,843,2,3])).
% 250.19/250.10 cnf(849,plain,
% 250.19/250.10 (E(f5(a2,f5(a2,f5(a2,a2))),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[847,2])).
% 250.19/250.10 cnf(850,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(f3(f8(a4,a2),x8501),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[17,748,847,2,3])).
% 250.19/250.10 cnf(853,plain,
% 250.19/250.10 (E(f3(a2,a1),f8(a4,f3(f3(a1,a2),f3(a1,a2))))),
% 250.19/250.10 inference(scs_inference,[],[17,692,850,2,3])).
% 250.19/250.10 cnf(856,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(f5(a2,f5(a2,a2)),a2))),
% 250.19/250.10 inference(scs_inference,[],[17,783,853,2,3])).
% 250.19/250.10 cnf(859,plain,
% 250.19/250.10 (E(f3(f5(x8591,x8592),x8591),f5(f8(a4,x8591),f8(a4,x8591)))),
% 250.19/250.10 inference(scs_inference,[],[17,388,856,2,3])).
% 250.19/250.10 cnf(863,plain,
% 250.19/250.10 (E(f3(f5(x8631,x8632),x8631),f3(f8(a4,x8631),f8(a4,x8631)))),
% 250.19/250.10 inference(scs_inference,[],[17,565,859,2,3])).
% 250.19/250.10 cnf(867,plain,
% 250.19/250.10 (E(f3(f5(a4,x8671),a4),f8(f7(x8672),x8672))),
% 250.19/250.10 inference(scs_inference,[],[17,624,863,2,3])).
% 250.19/250.10 cnf(869,plain,
% 250.19/250.10 (E(f8(f7(x8691),x8691),f3(f5(a4,x8692),a4))),
% 250.19/250.10 inference(scs_inference,[],[867,2])).
% 250.19/250.10 cnf(870,plain,
% 250.19/250.10 (E(f3(a4,a4),f5(f3(a4,x8701),a4))),
% 250.19/250.10 inference(scs_inference,[],[688,745,867,2,3])).
% 250.19/250.10 cnf(871,plain,
% 250.19/250.10 (E(f5(f3(a4,x8711),a4),f3(a4,a4))),
% 250.19/250.10 inference(scs_inference,[],[870,2])).
% 250.19/250.10 cnf(872,plain,
% 250.19/250.10 (E(f8(f5(f7(x8721),f7(x8721)),f5(x8721,x8721)),f3(f5(a4,x8722),a4))),
% 250.19/250.10 inference(scs_inference,[],[615,869,870,2,3])).
% 250.19/250.10 cnf(874,plain,
% 250.19/250.10 (E(f3(f5(a4,x8741),a4),f8(f5(f7(x8742),f7(x8742)),f5(x8742,x8742)))),
% 250.19/250.10 inference(scs_inference,[],[872,2])).
% 250.19/250.10 cnf(875,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(f3(a2,x8751),a2))),
% 250.19/250.10 inference(scs_inference,[],[17,763,872,2,3])).
% 250.19/250.10 cnf(877,plain,
% 250.19/250.10 (E(f5(f3(a2,x8771),a2),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[875,2])).
% 250.19/250.10 cnf(878,plain,
% 250.19/250.10 (E(f3(f5(a4,x8781),a4),f3(f3(a4,a4),f3(a4,a4)))),
% 250.19/250.10 inference(scs_inference,[],[502,874,875,2,3])).
% 250.19/250.10 cnf(881,plain,
% 250.19/250.10 (E(f3(a2,a2),f5(f3(a2,x8811),a2))),
% 250.19/250.10 inference(scs_inference,[],[654,813,878,2,3])).
% 250.19/250.10 cnf(882,plain,
% 250.19/250.10 (E(f5(f3(a2,x8821),a2),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[881,2])).
% 250.19/250.10 cnf(883,plain,
% 250.19/250.10 (E(f3(a2,a1),f8(a4,f5(a2,f3(a2,x8831))))),
% 250.19/250.10 inference(scs_inference,[],[17,157,881,2,3])).
% 250.19/250.10 cnf(885,plain,
% 250.19/250.10 (E(f8(a4,f5(a2,f3(a2,x8851))),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[883,2])).
% 250.19/250.10 cnf(886,plain,
% 250.19/250.10 (E(f3(a2,a1),f8(a4,f3(a2,f5(a2,x8861))))),
% 250.19/250.10 inference(scs_inference,[],[17,160,883,2,3])).
% 250.19/250.10 cnf(889,plain,
% 250.19/250.10 (E(f5(a2,f3(a2,x8891)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[885,36,886,2,3])).
% 250.19/250.10 cnf(892,plain,
% 250.19/250.10 (E(f3(a2,a1),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,433,889,2,3])).
% 250.19/250.10 cnf(895,plain,
% 250.19/250.10 (E(f5(a4,f5(a4,f5(a4,a4))),f8(a4,a4))),
% 250.19/250.10 inference(scs_inference,[],[799,683,892,2,3])).
% 250.19/250.10 cnf(897,plain,
% 250.19/250.10 (E(f8(a4,a4),f5(a4,f5(a4,f5(a4,a4))))),
% 250.19/250.10 inference(scs_inference,[],[895,2])).
% 250.19/250.10 cnf(898,plain,
% 250.19/250.10 (E(f5(f5(a2,a2),f3(f5(a2,a2),x8981)),f8(a4,a2))),
% 250.19/250.10 inference(scs_inference,[],[774,579,895,2,3])).
% 250.19/250.10 cnf(901,plain,
% 250.19/250.10 (E(f3(a4,a4),f5(a4,f5(a4,f5(a4,a4))))),
% 250.19/250.10 inference(scs_inference,[],[686,897,898,2,3])).
% 250.19/250.10 cnf(903,plain,
% 250.19/250.10 (E(f3(f3(x9031,x9032),x9033),f3(f3(x9033,x9031),x9032))),
% 250.19/250.10 inference(scs_inference,[],[17,122,901,2,3])).
% 250.19/250.10 cnf(907,plain,
% 250.19/250.10 (E(f3(a2,a1),f8(a4,f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[17,208,903,2,3])).
% 250.19/250.10 cnf(909,plain,
% 250.19/250.10 (E(f8(a4,f8(a4,a2)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[907,2])).
% 250.19/250.10 cnf(910,plain,
% 250.19/250.10 (E(f3(f5(x9101,x9102),x9101),f5(f5(x9101,x9101),f5(x9101,x9101)))),
% 250.19/250.10 inference(scs_inference,[],[17,343,907,2,3])).
% 250.19/250.10 cnf(914,plain,
% 250.19/250.10 (E(f8(a4,f3(a1,a2)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[909,154,910,2,3])).
% 250.19/250.10 cnf(915,plain,
% 250.19/250.10 (E(f3(a2,a1),f8(a4,f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[914,2])).
% 250.19/250.10 cnf(916,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(f5(a2,a2),f5(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[17,352,914,2,3])).
% 250.19/250.10 cnf(918,plain,
% 250.19/250.10 (E(f5(f5(a2,a2),f5(a2,a2)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[916,2])).
% 250.19/250.10 cnf(919,plain,
% 250.19/250.10 (E(f3(a2,a1),f3(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[442,915,916,2,3])).
% 250.19/250.10 cnf(920,plain,
% 250.19/250.10 (E(f3(f8(a4,a2),f8(a4,a2)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[919,2])).
% 250.19/250.10 cnf(921,plain,
% 250.19/250.10 (E(f3(f5(x9211,x9212),x9211),f3(f3(x9211,x9211),f3(x9211,x9211)))),
% 250.19/250.10 inference(scs_inference,[],[17,487,919,2,3])).
% 250.19/250.10 cnf(925,plain,
% 250.19/250.10 (E(f3(a2,a1),f3(f5(a2,a2),f5(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[17,514,921,2,3])).
% 250.19/250.10 cnf(927,plain,
% 250.19/250.10 (E(f3(f5(a2,a2),f5(a2,a2)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[925,2])).
% 250.19/250.10 cnf(928,plain,
% 250.19/250.10 (E(f3(f5(x9281,x9282),x9281),f3(f5(x9281,x9281),f5(x9281,x9281)))),
% 250.19/250.10 inference(scs_inference,[],[17,526,925,2,3])).
% 250.19/250.10 cnf(932,plain,
% 250.19/250.10 (E(f3(a2,a1),f8(a4,f8(a4,f8(a4,a2))))),
% 250.19/250.10 inference(scs_inference,[],[17,220,928,2,3])).
% 250.19/250.10 cnf(934,plain,
% 250.19/250.10 (E(f8(a4,f8(a4,f8(a4,a2))),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[932,2])).
% 250.19/250.10 cnf(935,plain,
% 250.19/250.10 (E(f3(a2,a1),f8(a4,f8(a4,f3(a1,a2))))),
% 250.19/250.10 inference(scs_inference,[],[17,818,932,2,3])).
% 250.19/250.10 cnf(937,plain,
% 250.19/250.10 (E(f8(a4,f8(a4,f3(a1,a2))),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[935,2])).
% 250.19/250.10 cnf(938,plain,
% 250.19/250.10 (E(f3(f3(a1,a2),f3(a1,a2)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[247,909,935,2,3])).
% 250.19/250.10 cnf(939,plain,
% 250.19/250.10 (E(f3(a2,a1),f3(f3(a1,a2),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[938,2])).
% 250.19/250.10 cnf(940,plain,
% 250.19/250.10 (E(f8(a4,a2),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[937,211,938,2,3])).
% 250.19/250.10 cnf(942,plain,
% 250.19/250.10 (E(f3(f5(x9421,x9422),x9421),f8(a4,f8(a4,x9421)))),
% 250.19/250.10 inference(scs_inference,[],[17,232,940,2,3])).
% 250.19/250.10 cnf(945,plain,
% 250.19/250.10 (E(f8(a4,f8(a4,x9451)),f3(f5(x9451,x9452),x9451))),
% 250.19/250.10 inference(scs_inference,[],[942,2])).
% 250.19/250.10 cnf(946,plain,
% 250.19/250.10 (E(f8(f3(f7(x9461),f7(x9461)),f5(x9461,x9461)),f3(f5(a4,x9462),a4))),
% 250.19/250.10 inference(scs_inference,[],[609,869,942,2,3])).
% 250.19/250.10 cnf(948,plain,
% 250.19/250.10 (E(f3(f5(a4,x9481),a4),f8(f3(f7(x9482),f7(x9482)),f5(x9482,x9482)))),
% 250.19/250.10 inference(scs_inference,[],[946,2])).
% 250.19/250.10 cnf(949,plain,
% 250.19/250.10 (E(f8(f7(x9491),f3(x9491,x9491)),f3(f5(a4,x9492),a4))),
% 250.19/250.10 inference(scs_inference,[],[226,945,946,2,3])).
% 250.19/250.10 cnf(951,plain,
% 250.19/250.10 (E(f3(f5(a4,x9511),a4),f8(f7(x9512),f3(x9512,x9512)))),
% 250.19/250.10 inference(scs_inference,[],[949,2])).
% 250.19/250.10 cnf(952,plain,
% 250.19/250.10 (E(f3(f5(a4,x9521),a4),f3(a4,a4))),
% 250.19/250.10 inference(scs_inference,[],[448,948,949,2,3])).
% 250.19/250.10 cnf(955,plain,
% 250.19/250.10 (E(f3(f5(a4,x9551),a4),f5(a4,a4))),
% 250.19/250.10 inference(scs_inference,[],[307,951,952,2,3])).
% 250.19/250.10 cnf(957,plain,
% 250.19/250.10 (E(f5(a4,a4),f3(f5(a4,x9571),a4))),
% 250.19/250.10 inference(scs_inference,[],[955,2])).
% 250.19/250.10 cnf(958,plain,
% 250.19/250.10 (E(f3(f5(a4,x9581),a4),f8(a4,a4))),
% 250.19/250.10 inference(scs_inference,[],[163,948,955,2,3])).
% 250.19/250.10 cnf(961,plain,
% 250.19/250.10 (E(f3(f5(a2,x9611),a2),f8(a4,f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[17,238,958,2,3])).
% 250.19/250.10 cnf(963,plain,
% 250.19/250.10 (E(f8(a4,f3(a1,a2)),f3(f5(a2,x9631),a2))),
% 250.19/250.10 inference(scs_inference,[],[961,2])).
% 250.19/250.10 cnf(964,plain,
% 250.19/250.10 (E(f3(f5(a2,x9641),a2),f3(f3(a1,a2),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[17,571,961,2,3])).
% 250.19/250.10 cnf(967,plain,
% 250.19/250.10 (E(f5(f3(a1,a2),f3(a1,a2)),f3(f5(a2,x9671),a2))),
% 250.19/250.10 inference(scs_inference,[],[963,586,964,2,3])).
% 250.19/250.10 cnf(968,plain,
% 250.19/250.10 (E(f3(f5(a2,x9681),a2),f5(f3(a1,a2),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[967,2])).
% 250.19/250.10 cnf(969,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x9691),f3(a1,a2)),f3(f3(a2,a2),f3(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[493,807,967,2,3])).
% 250.19/250.10 cnf(970,plain,
% 250.19/250.10 (E(f3(f3(a2,a2),f3(a2,a2)),f5(f3(f3(a1,a2),x9701),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[969,2])).
% 250.19/250.10 cnf(971,plain,
% 250.19/250.10 (E(f3(a2,a1),f3(f5(a2,x9711),a2))),
% 250.19/250.10 inference(scs_inference,[],[915,963,969,2,3])).
% 250.19/250.10 cnf(972,plain,
% 250.19/250.10 (E(f3(f5(a2,x9721),a2),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[971,2])).
% 250.19/250.10 cnf(973,plain,
% 250.19/250.10 (E(f3(f5(a2,x9731),a2),f3(a1,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,139,971,2,3])).
% 250.19/250.10 cnf(976,plain,
% 250.19/250.10 (E(f3(a2,f5(a2,x9761)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[17,972,973,2,3])).
% 250.19/250.10 cnf(979,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,283,976,2,3])).
% 250.19/250.10 cnf(982,plain,
% 250.19/250.10 (E(f3(f5(a2,a2),f5(f5(a2,a2),x9821)),f8(a4,a2))),
% 250.19/250.10 inference(scs_inference,[],[777,579,979,2,3])).
% 250.19/250.10 cnf(985,plain,
% 250.19/250.10 (E(f3(f5(a2,x9851),a2),f5(f3(f3(a1,a2),x9852),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[816,968,982,2,3])).
% 250.19/250.10 cnf(986,plain,
% 250.19/250.10 (E(f5(f3(f3(a1,a2),x9861),f3(a1,a2)),f3(f5(a2,x9862),a2))),
% 250.19/250.10 inference(scs_inference,[],[985,2])).
% 250.19/250.10 cnf(987,plain,
% 250.19/250.10 (E(f5(f3(a1,a2),f3(a1,a2)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[289,918,985,2,3])).
% 250.19/250.10 cnf(988,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(f3(a1,a2),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[987,2])).
% 250.19/250.10 cnf(989,plain,
% 250.19/250.10 (E(f5(a2,f5(f5(a2,a2),a2)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[822,849,987,2,3])).
% 250.19/250.10 cnf(991,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(a2,f5(f5(a2,a2),a2)))),
% 250.19/250.10 inference(scs_inference,[],[989,2])).
% 250.19/250.10 cnf(992,plain,
% 250.19/250.10 (E(f8(f7(x9921),f5(x9921,x9921)),f3(f5(a4,x9922),a4))),
% 250.19/250.10 inference(scs_inference,[],[337,957,989,2,3])).
% 250.19/250.10 cnf(993,plain,
% 250.19/250.10 (E(f3(f5(a4,x9931),a4),f8(f7(x9932),f5(x9932,x9932)))),
% 250.19/250.10 inference(scs_inference,[],[992,2])).
% 250.19/250.10 cnf(994,plain,
% 250.19/250.10 (E(f3(a1,a2),f5(a2,f5(f5(a2,a2),a2)))),
% 250.19/250.10 inference(scs_inference,[],[17,991,992,2,3])).
% 250.19/250.10 cnf(997,plain,
% 250.19/250.10 (E(f3(f5(a4,x9971),a4),f5(f3(a4,x9972),a4))),
% 250.19/250.10 inference(scs_inference,[],[755,993,994,2,3])).
% 250.19/250.10 cnf(1000,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(f3(f3(a1,a2),x10001),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[988,816,997,2,3])).
% 250.19/250.10 cnf(1002,plain,
% 250.19/250.10 (E(f5(f3(f8(a4,a2),x10021),f8(a4,a2)),f5(f3(a2,x10022),a2))),
% 250.19/250.10 inference(scs_inference,[],[789,813,1000,2,3])).
% 250.19/250.10 cnf(1003,plain,
% 250.19/250.10 (E(f5(f3(a2,x10031),a2),f5(f3(f8(a4,a2),x10032),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1002,2])).
% 250.19/250.10 cnf(1004,plain,
% 250.19/250.10 (E(f5(f8(a4,a2),f3(f8(a4,a2),x10041)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[190,909,1002,2,3])).
% 250.19/250.10 cnf(1007,plain,
% 250.19/250.10 (E(f3(f3(a2,a2),f3(a2,a2)),f5(f3(f8(a4,a2),x10071),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[726,1003,1004,2,3])).
% 250.19/250.10 cnf(1010,plain,
% 250.19/250.10 (E(f5(f3(f8(a4,a2),x10101),f8(a4,a2)),f3(f3(a2,a2),f3(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1007,2])).
% 250.19/250.10 cnf(1011,plain,
% 250.19/250.10 (E(f5(f5(a4,a4),f5(a4,a4)),f3(a4,a4))),
% 250.19/250.10 inference(scs_inference,[],[736,871,1007,2,3])).
% 250.19/250.10 cnf(1014,plain,
% 250.19/250.10 (E(f3(a4,a4),f5(f5(a4,a4),f5(a4,a4)))),
% 250.19/250.10 inference(scs_inference,[],[1011,2])).
% 250.19/250.10 cnf(1015,plain,
% 250.19/250.10 (E(f5(f8(a4,a2),f8(a4,a2)),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[706,882,1011,2,3])).
% 250.19/250.10 cnf(1018,plain,
% 250.19/250.10 (E(f3(a2,a2),f5(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1015,2])).
% 250.19/250.10 cnf(1019,plain,
% 250.19/250.10 (E(f5(a2,a2),f3(f5(a2,x10191),a2))),
% 250.19/250.10 inference(scs_inference,[],[796,986,1015,2,3])).
% 250.19/250.10 cnf(1021,plain,
% 250.19/250.10 (E(f3(f5(a2,x10211),a2),f5(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[1019,2])).
% 250.19/250.10 cnf(1022,plain,
% 250.19/250.10 (E(f3(f8(a4,a4),f8(a4,a4)),f3(a4,a4))),
% 250.19/250.10 inference(scs_inference,[],[710,871,1019,2,3])).
% 250.19/250.10 cnf(1026,plain,
% 250.19/250.10 (E(f5(f3(a1,a2),f3(a1,a2)),f5(f3(f8(a4,a2),x10261),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[758,1003,1022,2,3])).
% 250.19/250.10 cnf(1028,plain,
% 250.19/250.10 (E(f5(f3(f8(a4,a2),x10281),f8(a4,a2)),f5(f3(a1,a2),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1026,2])).
% 250.19/250.10 cnf(1029,plain,
% 250.19/250.10 (E(f3(f5(a2,x10291),a2),f5(f3(a2,x10292),a2))),
% 250.19/250.10 inference(scs_inference,[],[1021,813,1026,2,3])).
% 250.19/250.10 cnf(1031,plain,
% 250.19/250.10 (E(f5(f3(f8(a4,a2),x10311),f8(a4,a2)),f5(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[298,1028,1029,2,3])).
% 250.19/250.10 cnf(1032,plain,
% 250.19/250.10 (E(f5(f8(a4,a2),f8(a4,a2)),f5(f3(f8(a4,a2),x10321),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1031,2])).
% 250.19/250.10 cnf(1033,plain,
% 250.19/250.10 (E(f3(a2,a2),f3(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[588,1018,1031,2,3])).
% 250.19/250.10 cnf(1034,plain,
% 250.19/250.10 (E(f3(f8(a4,a2),f8(a4,a2)),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[1033,2])).
% 250.19/250.10 cnf(1035,plain,
% 250.19/250.10 (E(f5(f8(a4,a2),f8(a4,a2)),f3(f3(a2,a2),f3(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1032,1010,1033,2,3])).
% 250.19/250.10 cnf(1037,plain,
% 250.19/250.10 (E(f3(f3(a2,a2),f3(a2,a2)),f5(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1035,2])).
% 250.19/250.10 cnf(1038,plain,
% 250.19/250.10 (E(f3(f8(a4,a2),f5(f8(a4,a2),x10381)),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[193,909,1035,2,3])).
% 250.19/250.10 cnf(1040,plain,
% 250.19/250.10 (E(f3(a2,a1),f3(f8(a4,a2),f5(f8(a4,a2),x10401)))),
% 250.19/250.10 inference(scs_inference,[],[1038,2])).
% 250.19/250.10 cnf(1041,plain,
% 250.19/250.10 (E(f3(f3(a2,a2),f3(a2,a2)),f3(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1037,588,1038,2,3])).
% 250.19/250.10 cnf(1043,plain,
% 250.19/250.10 (E(f3(a1,a2),f3(f8(a4,a2),f5(f8(a4,a2),x10431)))),
% 250.19/250.10 inference(scs_inference,[],[17,1040,1041,2,3])).
% 250.19/250.10 cnf(1045,plain,
% 250.19/250.10 (E(f3(f8(a4,a2),f5(f8(a4,a2),x10451)),f3(a1,a2))),
% 250.19/250.10 inference(scs_inference,[],[1043,2])).
% 250.19/250.10 cnf(1046,plain,
% 250.19/250.10 (E(f8(a4,f5(f8(a4,a2),f8(a4,a2))),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[43,909,1043,2,3])).
% 250.19/250.10 cnf(1048,plain,
% 250.19/250.10 (E(f3(a2,a1),f8(a4,f5(f8(a4,a2),f8(a4,a2))))),
% 250.19/250.10 inference(scs_inference,[],[1046,2])).
% 250.19/250.10 cnf(1049,plain,
% 250.19/250.10 (E(f3(f5(f8(a4,a2),x10491),f8(a4,a2)),f3(a1,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,1045,1046,2,3])).
% 250.19/250.10 cnf(1051,plain,
% 250.19/250.10 (E(f3(a1,a2),f3(f5(f8(a4,a2),x10511),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1049,2])).
% 250.19/250.10 cnf(1052,plain,
% 250.19/250.10 (E(f8(f3(f7(x10521),f7(x10521)),f3(x10521,x10521)),f5(a4,a4))),
% 250.19/250.10 inference(scs_inference,[],[322,50,1049,2,3])).
% 250.19/250.10 cnf(1056,plain,
% 250.19/250.10 (E(f3(a2,a1),f3(f5(f8(a4,a2),x10561),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[17,1051,1052,2,3])).
% 250.19/250.10 cnf(1059,plain,
% 250.19/250.10 (E(f8(f5(a4,a4),f8(a4,f8(a4,a2))),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[934,57,1056,2,3])).
% 250.19/250.10 cnf(1061,plain,
% 250.19/250.10 (E(f3(a2,a1),f8(f5(a4,a4),f8(a4,f8(a4,a2))))),
% 250.19/250.10 inference(scs_inference,[],[1059,2])).
% 250.19/250.10 cnf(1062,plain,
% 250.19/250.10 (E(f3(a1,a2),f8(a4,f5(f8(a4,a2),f8(a4,a2))))),
% 250.19/250.10 inference(scs_inference,[],[17,1048,1059,2,3])).
% 250.19/250.10 cnf(1065,plain,
% 250.19/250.10 (E(f3(a1,a2),f8(f5(a4,a4),f8(a4,f8(a4,a2))))),
% 250.19/250.10 inference(scs_inference,[],[17,1061,1062,2,3])).
% 250.19/250.10 cnf(1068,plain,
% 250.19/250.10 (E(f8(f3(a4,a4),f8(a4,f3(a1,a2))),f5(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[271,64,1065,2,3])).
% 250.19/250.10 cnf(1071,plain,
% 250.19/250.10 (E(f3(x10711,x10712),f5(f3(x10712,x10711),f3(f3(x10712,x10711),x10713)))),
% 250.19/250.10 inference(scs_inference,[],[17,67,1068,2,3])).
% 250.19/250.10 cnf(1074,plain,
% 250.19/250.10 (E(f3(x10741,x10742),f3(f3(x10742,x10741),f5(f3(x10742,x10741),x10743)))),
% 250.19/250.10 inference(scs_inference,[],[17,78,1071,2,3])).
% 250.19/250.10 cnf(1077,plain,
% 250.19/250.10 (E(f5(a2,f5(a2,f5(a2,a2))),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[71,652,1074,2,3])).
% 250.19/250.10 cnf(1080,plain,
% 250.19/250.10 (E(f5(f3(a1,a2),f3(f3(a1,a2),x10801)),a2)),
% 250.19/250.10 inference(scs_inference,[],[325,1077,404,2,3])).
% 250.19/250.10 cnf(1083,plain,
% 250.19/250.10 (E(f5(f8(a4,a2),f8(a4,a2)),f5(f5(a2,a2),f5(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[811,826,1080,2,3])).
% 250.19/250.10 cnf(1085,plain,
% 250.19/250.10 (E(f5(f5(a2,a2),f5(a2,a2)),f5(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1083,2])).
% 250.19/250.10 cnf(1086,plain,
% 250.19/250.10 (E(f3(f5(f3(a1,a2),x10861),f3(a1,a2)),f8(a4,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,1083,675,2,3])).
% 250.19/250.10 cnf(1089,plain,
% 250.19/250.10 (E(f5(f5(a2,a2),f5(a2,a2)),f5(f3(f8(a4,a2),x10891),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1085,1032,1086,2,3])).
% 250.19/250.10 cnf(1090,plain,
% 250.19/250.10 (E(f5(f3(f8(a4,a2),x10901),f8(a4,a2)),f5(f5(a2,a2),f5(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1089,2])).
% 250.19/250.10 cnf(1091,plain,
% 250.19/250.10 (E(f8(a4,f3(a1,a2)),f5(f3(f8(a4,a2),x10911),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[346,1089,2,3])).
% 250.19/250.10 cnf(1092,plain,
% 250.19/250.10 (E(f5(f3(f8(a4,a2),x10921),f8(a4,a2)),f8(a4,f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1091,2])).
% 250.19/250.10 cnf(1093,plain,
% 250.19/250.10 (E(f3(f3(a1,a2),f3(a1,a2)),f5(f3(f3(a1,a2),x10931),f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[403,827,1091,2,3])).
% 250.19/250.10 cnf(1095,plain,
% 250.19/250.10 (E(f5(f3(f8(a4,a2),x10951),f8(a4,a2)),f3(f5(a2,a2),f5(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[520,1092,1093,2,3])).
% 250.19/250.10 cnf(1096,plain,
% 250.19/250.10 (E(f3(f5(a2,a2),f5(a2,a2)),f5(f3(f8(a4,a2),x10961),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1095,2])).
% 250.19/250.10 cnf(1097,plain,
% 250.19/250.10 (E(f5(f3(f8(a4,a2),x10971),f8(a4,a2)),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[415,1092,1095,2,3])).
% 250.19/250.10 cnf(1098,plain,
% 250.19/250.10 (E(f3(a2,a2),f5(f3(f8(a4,a2),x10981),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1097,2])).
% 250.19/250.10 cnf(1099,plain,
% 250.19/250.10 (E(f3(f5(a2,a2),f5(a2,a2)),f5(f5(a2,a2),f5(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1090,1096,1097,2,3])).
% 250.19/250.10 cnf(1102,plain,
% 250.19/250.10 (E(f3(a2,a2),f5(f5(a2,a2),f5(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1098,1090,1099,2,3])).
% 250.19/250.10 cnf(1104,plain,
% 250.19/250.10 (E(f5(f5(a2,a2),f5(a2,a2)),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[1102,2])).
% 250.19/250.10 cnf(1105,plain,
% 250.19/250.10 (E(f5(f5(f5(a2,a2),a2),a2),f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[722,918,1102,2,3])).
% 250.19/250.10 cnf(1107,plain,
% 250.19/250.10 (E(f3(a2,a1),f5(f5(f5(a2,a2),a2),a2))),
% 250.19/250.10 inference(scs_inference,[],[1105,2])).
% 250.19/250.10 cnf(1108,plain,
% 250.19/250.10 (E(f3(f5(a2,a2),f5(f5(a2,a2),x11081)),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[1104,328,1105,2,3])).
% 250.19/250.10 cnf(1111,plain,
% 250.19/250.10 (E(f3(a1,a2),f5(f5(f5(a2,a2),a2),a2))),
% 250.19/250.10 inference(scs_inference,[],[17,1107,1108,2,3])).
% 250.19/250.10 cnf(1114,plain,
% 250.19/250.10 (E(f3(a4,a4),f5(f5(f5(a4,a4),a4),a4))),
% 250.19/250.10 inference(scs_inference,[],[1014,101,1111,2,3])).
% 250.19/250.10 cnf(1117,plain,
% 250.19/250.10 (E(f3(f5(f3(a1,a2),x11171),f3(a1,a2)),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,600,1114,2,3])).
% 250.19/250.10 cnf(1120,plain,
% 250.19/250.10 (E(f3(f5(f3(a1,a2),x11201),f3(a1,a2)),f5(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,1117,580,2,3])).
% 250.19/250.10 cnf(1123,plain,
% 250.19/250.10 (E(f3(f3(a2,a2),f3(a2,a2)),f5(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[970,1120,794,2,3])).
% 250.19/250.10 cnf(1126,plain,
% 250.19/250.10 (E(f8(a4,a2),f3(f5(a2,x11261),a2))),
% 250.19/250.10 inference(scs_inference,[],[805,986,1123,2,3])).
% 250.19/250.10 cnf(1129,plain,
% 250.19/250.10 (E(f3(f5(f5(a2,a2),x11291),f5(a2,a2)),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[17,1126,1108,2,3])).
% 250.19/250.10 cnf(1132,plain,
% 250.19/250.10 (E(f3(x11321,x11322),f3(x11322,f3(x11321,f3(x11322,x11321))))),
% 250.19/250.10 inference(scs_inference,[],[17,1129,72,2,3])).
% 250.19/250.10 cnf(1135,plain,
% 250.19/250.10 (E(f3(f3(a2,f3(a1,a2)),a1),a2)),
% 250.19/250.10 inference(scs_inference,[],[17,1132,79,2,3])).
% 250.19/250.10 cnf(1138,plain,
% 250.19/250.10 (E(f5(a2,f3(a2,x11381)),f5(f3(f8(a4,a2),x11382),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[235,1135,1091,2,3])).
% 250.19/250.10 cnf(1140,plain,
% 250.19/250.10 (E(f5(f3(a2,x11401),a2),a2)),
% 250.19/250.10 inference(scs_inference,[],[718,1138,254,2,3])).
% 250.19/250.10 cnf(1141,plain,
% 250.19/250.10 (E(a2,f5(f3(a2,x11411),a2))),
% 250.19/250.10 inference(scs_inference,[],[1140,2])).
% 250.19/250.10 cnf(1142,plain,
% 250.19/250.10 (E(a2,f5(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[292,256,1140,2,3])).
% 250.19/250.10 cnf(1144,plain,
% 250.19/250.10 (E(a2,f3(a2,a1))),
% 250.19/250.10 inference(scs_inference,[],[877,1141,1142,2,3])).
% 250.19/250.10 cnf(1146,plain,
% 250.19/250.10 (E(f3(a2,a1),a2)),
% 250.19/250.10 inference(scs_inference,[],[1144,2])).
% 250.19/250.10 cnf(1184,plain,
% 250.19/250.10 (E(f3(a2,a2),f5(f5(a2,a2),f3(f5(a2,a2),x11841)))),
% 250.19/250.10 inference(scs_inference,[],[18,652,3,2])).
% 250.19/250.10 cnf(1283,plain,
% 250.19/250.10 (E(f3(f8(a4,a2),f8(a4,a2)),a2)),
% 250.19/250.10 inference(scs_inference,[],[920,1146,3])).
% 250.19/250.10 cnf(1284,plain,
% 250.19/250.10 (E(a2,f3(f8(a4,a2),f8(a4,a2)))),
% 250.19/250.10 inference(scs_inference,[],[920,1146,3,2])).
% 250.19/250.10 cnf(1293,plain,
% 250.19/250.10 (E(f3(f5(a2,a2),f5(a2,a2)),a2)),
% 250.19/250.10 inference(scs_inference,[],[927,1146,3])).
% 250.19/250.10 cnf(1304,plain,
% 250.19/250.10 (E(f8(a4,f8(a4,f5(a2,a2))),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[1184,229,3,2])).
% 250.19/250.10 cnf(1305,plain,
% 250.19/250.10 (E(f8(a4,f5(a2,a2)),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[1304,36,3])).
% 250.19/250.10 cnf(1307,plain,
% 250.19/250.10 (E(f3(a2,a2),f8(a4,f5(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1305,2])).
% 250.19/250.10 cnf(1421,plain,
% 250.19/250.10 (~E(f3(f8(a4,a2),f8(a4,a2)),a1)),
% 250.19/250.10 inference(scs_inference,[],[27,32,578,1284,10,4,5,7,8,6,9,2,3])).
% 250.19/250.10 cnf(1429,plain,
% 250.19/250.10 (~E(f8(a1,a6),f8(a2,a6))),
% 250.19/250.10 inference(scs_inference,[],[31,1283,7,4,5,8,10,6,9,2])).
% 250.19/250.10 cnf(1439,plain,
% 250.19/250.10 (~E(f8(a1,f5(a6,a6)),f8(a2,a6))),
% 250.19/250.10 inference(scs_inference,[],[1429,1293,1421,40,4,8,7,5,10,9,6,2,3])).
% 250.19/250.10 cnf(1449,plain,
% 250.19/250.10 (~E(f3(a1,a2),a1)),
% 250.19/250.10 inference(scs_inference,[],[542,1439,940,1421,8,5,4,7,10,6,9,2,3])).
% 250.19/250.10 cnf(1457,plain,
% 250.19/250.10 (~E(a1,f3(a1,a2))),
% 250.19/250.10 inference(scs_inference,[],[1449,1144,5,7,8,4,10,9,6,2])).
% 250.19/250.10 cnf(1477,plain,
% 250.19/250.10 (~E(f5(a1,a1),f3(a1,a2))),
% 250.19/250.10 inference(scs_inference,[],[1457,44,406,28,5,7,8,4,9,10,6,2,3])).
% 250.19/250.10 cnf(1487,plain,
% 250.19/250.10 (~E(f3(a2,a2),a1)),
% 250.19/250.10 inference(scs_inference,[],[1477,1034,1142,1421,7,5,8,4,10,9,6,2,3])).
% 250.19/250.10 cnf(1495,plain,
% 250.19/250.10 (~E(a1,f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[1487,1284,7,5,8,4,10,9,6,2])).
% 250.19/250.10 cnf(1514,plain,
% 250.19/250.10 (~E(f3(a1,a1),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[1495,58,1140,33,7,5,8,4,10,9,6,2,3])).
% 250.19/250.10 cnf(1523,plain,
% 250.19/250.10 (~E(f3(a2,a2),f3(a1,a1))),
% 250.19/250.10 inference(scs_inference,[],[1514,1141,7,5,8,4,9,10,6,2])).
% 250.19/250.10 cnf(1595,plain,
% 250.19/250.10 (E(f5(x15951,a2),f5(x15951,f3(a1,a2)))),
% 250.19/250.10 inference(scs_inference,[],[132,5,7,8,9])).
% 250.19/250.10 cnf(1600,plain,
% 250.19/250.10 (~E(f8(a4,f5(a2,a2)),f3(a1,a1))),
% 250.19/250.10 inference(scs_inference,[],[1307,76,1523,132,5,7,8,9,6,10,4,2,3])).
% 250.19/250.10 cnf(1608,plain,
% 250.19/250.10 (~E(f3(a1,a1),f8(a4,f5(a2,a2)))),
% 250.19/250.10 inference(scs_inference,[],[1600,143,7,5,8,9,6,10,4,2])).
% 250.19/250.10 cnf(1763,plain,
% 250.19/250.10 (E(f3(x17631,x17632),f3(x17631,f3(x17632,x17632)))),
% 250.19/250.10 inference(scs_inference,[],[33,431,7,8,10,5])).
% 250.19/250.10 cnf(1764,plain,
% 250.19/250.10 (E(f5(x17641,x17642),f5(x17641,f3(x17642,x17642)))),
% 250.19/250.10 inference(scs_inference,[],[33,431,7,8,10,5,9])).
% 250.19/250.10 cnf(1788,plain,
% 250.19/250.10 (~E(f5(f8(a1,a6),f3(f8(a2,a6),f8(a2,a6))),f8(a1,a6))),
% 250.19/250.10 inference(scs_inference,[],[27,1764,32,684,7,8,5,10,9,6,4,2,3])).
% 250.19/250.10 cnf(1798,plain,
% 250.19/250.10 (E(f3(a2,a1),f3(f3(a1,a2),f3(f3(a1,a2),f3(a1,a2))))),
% 250.19/250.10 inference(scs_inference,[],[939,1763,1788,1146,7,8,5,10,9,6,4,2,3])).
% 250.19/250.10 cnf(1836,plain,
% 250.19/250.10 (E(f3(x18361,x18362),f3(f5(x18361,x18361),x18362))),
% 250.19/250.10 inference(scs_inference,[],[28,281,7,8,5,9,10,6,4])).
% 250.19/250.10 cnf(1968,plain,
% 250.19/250.10 (~E(f8(a4,f5(a2,a2)),f3(f5(a1,a1),a1))),
% 250.19/250.10 inference(scs_inference,[],[1836,1608,12,8,5,4,9,10,3,2])).
% 250.19/250.10 cnf(2007,plain,
% 250.19/250.10 (~E(f5(a1,a1),f3(a2,a2))),
% 250.19/250.10 inference(scs_inference,[],[431,1477,1836,2,3])).
% 250.19/250.10 cnf(2039,plain,
% 250.19/250.10 (~E(f8(a4,f5(a2,a2)),f5(a1,f3(a1,x20391)))),
% 250.19/250.10 inference(scs_inference,[],[846,1968,1798,2,3])).
% 250.19/250.10 cnf(2110,plain,
% 250.19/250.10 (~E(f8(f5(a1,a2),a6),f8(a1,a6))),
% 250.19/250.10 inference(scs_inference,[],[27,25,17,2007,4,10,8,9,5,2,3])).
% 250.19/250.10 cnf(3209,plain,
% 250.19/250.10 (~E(f5(a1,a2),a1)),
% 250.19/250.10 inference(scs_inference,[],[2110,6])).
% 250.19/250.10 cnf(3239,plain,
% 250.19/250.10 ($false),
% 250.19/250.10 inference(scs_inference,[],[1595,3209,2039,18,2,3]),
% 250.19/250.10 ['proof']).
% 250.19/250.10 % SZS output end Proof
% 250.19/250.10 % Total time :249.410000s
%------------------------------------------------------------------------------