%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP168-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 : n023.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:06 EDT 2024
% Result : Unsatisfiable 86.61s 86.65s
% Output : CNFRefutation 86.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP168-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n023.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Thu Jun 20 10:41:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.53/0.57 start to proof:theBenchmark
% 86.61/86.64 %-------------------------------------------
% 86.61/86.64 % File :CSE---1.7
% 86.61/86.64 % Problem :theBenchmark
% 86.61/86.64 % Transform :cnf
% 86.61/86.64 % Format :tptp:raw
% 86.61/86.64 % Command :java -jar mcs_scs.jar %d %s
% 86.61/86.64
% 86.61/86.64 % Result :Theorem 86.040000s
% 86.61/86.64 % Output :CNFRefutation 86.040000s
% 86.61/86.64 %-------------------------------------------
% 86.61/86.65 %--------------------------------------------------------------------------
% 86.61/86.65 % File : GRP168-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 86.61/86.65 % Domain : Group Theory (Lattice Ordered)
% 86.61/86.65 % Problem : Inner group automorphisms are order preserving
% 86.61/86.65 % Version : [Fuc94] (equality) axioms.
% 86.61/86.65 % English :
% 86.61/86.65
% 86.61/86.65 % Refs : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri
% 86.61/86.65 % : [Sch95] Schulz (1995), Explanation Based Learning for Distribu
% 86.61/86.65 % : [Dah95] Dahn (1995), Email to G. Sutcliffe
% 86.61/86.65 % Source : [Sch95]
% 86.61/86.65 % Names : p01a [Sch95]
% 86.61/86.65
% 86.61/86.65 % Status : Unsatisfiable
% 86.61/86.65 % Rating : 0.05 v8.2.0, 0.08 v8.1.0, 0.10 v7.5.0, 0.12 v7.4.0, 0.13 v7.3.0, 0.11 v7.1.0, 0.06 v7.0.0, 0.16 v6.3.0, 0.24 v6.2.0, 0.29 v6.1.0, 0.19 v6.0.0, 0.24 v5.5.0, 0.16 v5.4.0, 0.13 v5.3.0, 0.17 v5.2.0, 0.14 v5.1.0, 0.13 v5.0.0, 0.14 v4.1.0, 0.09 v4.0.1, 0.14 v4.0.0, 0.15 v3.7.0, 0.11 v3.4.0, 0.12 v3.3.0, 0.14 v3.2.0, 0.07 v3.1.0, 0.11 v2.7.0, 0.00 v2.1.0, 0.14 v2.0.0
% 86.61/86.65 % Syntax : Number of clauses : 17 ( 17 unt; 0 nHn; 2 RR)
% 86.61/86.65 % Number of literals : 17 ( 17 equ; 1 neg)
% 86.61/86.65 % Maximal clause size : 1 ( 1 avg)
% 86.61/86.65 % Maximal term depth : 4 ( 2 avg)
% 86.61/86.65 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 86.61/86.65 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 86.61/86.65 % Number of variables : 33 ( 2 sgn)
% 86.61/86.65 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 86.61/86.65
% 86.61/86.65 % Comments : ORDERING LPO inverse > product > greatest_lower_bound >
% 86.61/86.65 % least_upper_bound > identity > a > b > c
% 86.61/86.65 % : ORDERING LPO greatest_lower_bound > least_upper_bound >
% 86.61/86.65 % inverse > product > identity > a > b > c
% 86.61/86.65 % : [Dah95] says "Not difficult by monotony. Sometimes useful
% 86.61/86.65 % for transforming inequalities."
% 86.61/86.65 % Bugfixes : v1.2.1 - Duplicate axioms in GRP004-2.ax removed.
% 86.61/86.65 %--------------------------------------------------------------------------
% 86.61/86.65 %----Include equality group theory axioms
% 86.61/86.65 include('Axioms/GRP004-0.ax').
% 86.61/86.65 %----Include Lattice ordered group (equality) axioms
% 86.61/86.65 include('Axioms/GRP004-2.ax').
% 86.61/86.65 %--------------------------------------------------------------------------
% 86.61/86.65 cnf(p01a_1,hypothesis,
% 86.61/86.65 least_upper_bound(a,b) = b ).
% 86.61/86.65
% 86.61/86.65 cnf(prove_p01a,negated_conjecture,
% 86.61/86.65 least_upper_bound(multiply(inverse(c),multiply(a,c)),multiply(inverse(c),multiply(b,c))) != multiply(inverse(c),multiply(b,c)) ).
% 86.61/86.65
% 86.61/86.65 %--------------------------------------------------------------------------
% 86.61/86.65 %-------------------------------------------
% 86.61/86.65 % Proof found
% 86.61/86.65 % SZS status Theorem for theBenchmark
% 86.61/86.65 % SZS output start Proof
% 86.61/86.66 %ClaNum:27(EqnAxiom:10)
% 86.61/86.66 %VarNum:72(SingletonVarNum:33)
% 86.61/86.66 %MaxLitNum:1
% 86.61/86.66 %MaxfuncDepth:3
% 86.61/86.66 %SharedTerms:13
% 86.61/86.66 %goalClause: 27
% 86.61/86.66 %singleGoalClaCount:1
% 86.61/86.66 [11]E(f3(a1,a2),a2)
% 86.61/86.66 [27]~E(f3(f8(f7(a6),f8(a1,a6)),f8(f7(a6),f8(a2,a6))),f8(f7(a6),f8(a2,a6)))
% 86.61/86.66 [12]E(f8(a4,x121),x121)
% 86.61/86.66 [13]E(f5(x131,x131),x131)
% 86.61/86.66 [14]E(f3(x141,x141),x141)
% 86.61/86.66 [15]E(f8(f7(x151),x151),a4)
% 86.61/86.66 [16]E(f5(x161,x162),f5(x162,x161))
% 86.61/86.66 [17]E(f3(x171,x172),f3(x172,x171))
% 86.61/86.66 [18]E(f5(x181,f3(x181,x182)),x181)
% 86.61/86.66 [19]E(f3(x191,f5(x191,x192)),x191)
% 86.61/86.66 [20]E(f5(f5(x201,x202),x203),f5(x201,f5(x202,x203)))
% 86.61/86.66 [21]E(f3(f3(x211,x212),x213),f3(x211,f3(x212,x213)))
% 86.61/86.66 [22]E(f8(f8(x221,x222),x223),f8(x221,f8(x222,x223)))
% 86.61/86.66 [23]E(f5(f8(x231,x232),f8(x231,x233)),f8(x231,f5(x232,x233)))
% 86.61/86.66 [24]E(f3(f8(x241,x242),f8(x241,x243)),f8(x241,f3(x242,x243)))
% 86.61/86.66 [25]E(f5(f8(x251,x252),f8(x253,x252)),f8(f5(x251,x253),x252))
% 86.61/86.66 [26]E(f3(f8(x261,x262),f8(x263,x262)),f8(f3(x261,x263),x262))
% 86.61/86.66 %EqnAxiom
% 86.61/86.66 [1]E(x11,x11)
% 86.61/86.66 [2]E(x22,x21)+~E(x21,x22)
% 86.61/86.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 86.61/86.66 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 86.61/86.66 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 86.61/86.66 [6]~E(x61,x62)+E(f8(x61,x63),f8(x62,x63))
% 86.61/86.66 [7]~E(x71,x72)+E(f8(x73,x71),f8(x73,x72))
% 86.61/86.66 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83))
% 86.61/86.66 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92))
% 86.61/86.66 [10]~E(x101,x102)+E(f7(x101),f7(x102))
% 86.61/86.66
% 86.61/86.66 %-------------------------------------------
% 86.61/86.67 cnf(28,plain,
% 86.61/86.67 (E(x281,f5(x281,x281))),
% 86.61/86.67 inference(scs_inference,[],[13,2])).
% 86.61/86.67 cnf(29,plain,
% 86.61/86.67 (E(f5(f5(f8(x291,x292),f8(x291,x293)),f5(f8(x291,x292),f8(x291,x293))),f8(x291,f5(x292,x293)))),
% 86.61/86.67 inference(scs_inference,[],[13,23,2,3])).
% 86.61/86.67 cnf(31,plain,
% 86.61/86.67 (E(f8(x311,f5(x312,x313)),f5(f5(f8(x311,x312),f8(x311,x313)),f5(f8(x311,x312),f8(x311,x313))))),
% 86.61/86.67 inference(scs_inference,[],[29,2])).
% 86.61/86.67 cnf(32,plain,
% 86.61/86.67 (E(f3(f3(f8(x321,x322),f8(x321,x323)),f3(f8(x321,x322),f8(x321,x323))),f8(x321,f3(x322,x323)))),
% 86.61/86.67 inference(scs_inference,[],[29,14,24,2,3])).
% 86.61/86.67 cnf(34,plain,
% 86.61/86.67 (E(f8(x341,f3(x342,x343)),f3(f3(f8(x341,x342),f8(x341,x343)),f3(f8(x341,x342),f8(x341,x343))))),
% 86.61/86.67 inference(scs_inference,[],[32,2])).
% 86.61/86.67 cnf(35,plain,
% 86.61/86.67 (E(f8(x351,x352),f8(f5(x351,x351),x352))),
% 86.61/86.67 inference(scs_inference,[],[28,32,25,2,3])).
% 86.61/86.67 cnf(38,plain,
% 86.61/86.67 (E(f8(f5(x381,x381),x382),f8(x381,x382))),
% 86.61/86.67 inference(scs_inference,[],[35,2])).
% 86.61/86.67 cnf(39,plain,
% 86.61/86.67 (E(f5(f5(f8(x391,x392),f8(x391,x393)),f5(f8(x391,x392),f8(x391,x393))),f8(f5(x391,x391),f5(x392,x393)))),
% 86.61/86.67 inference(scs_inference,[],[35,29,2,3])).
% 86.61/86.67 cnf(41,plain,
% 86.61/86.67 (E(f8(f5(x411,x411),f5(x412,x413)),f5(f5(f8(x411,x412),f8(x411,x413)),f5(f8(x411,x412),f8(x411,x413))))),
% 86.61/86.67 inference(scs_inference,[],[39,2])).
% 86.61/86.67 cnf(44,plain,
% 86.61/86.67 (E(x441,f8(a4,x441))),
% 86.61/86.67 inference(scs_inference,[],[12,2])).
% 86.61/86.67 cnf(45,plain,
% 86.61/86.67 (E(f8(f5(f5(x451,x451),f5(x451,x451)),f5(x452,x453)),f5(f5(f8(x451,x452),f8(x451,x453)),f5(f8(x451,x452),f8(x451,x453))))),
% 86.61/86.67 inference(scs_inference,[],[41,38,12,2,3])).
% 86.61/86.67 cnf(47,plain,
% 86.61/86.67 (E(f5(f5(f8(x471,x472),f8(x471,x473)),f5(f8(x471,x472),f8(x471,x473))),f8(f5(f5(x471,x471),f5(x471,x471)),f5(x472,x473)))),
% 86.61/86.67 inference(scs_inference,[],[45,2])).
% 86.61/86.67 cnf(48,plain,
% 86.61/86.67 (E(f5(x481,x482),f5(f5(f8(a4,x481),f8(a4,x482)),f5(f8(a4,x481),f8(a4,x482))))),
% 86.61/86.67 inference(scs_inference,[],[31,44,45,2,3])).
% 86.61/86.67 cnf(51,plain,
% 86.61/86.67 (E(f5(f5(f8(a4,x511),f8(a4,x512)),f5(f8(a4,x511),f8(a4,x512))),f5(x511,x512))),
% 86.61/86.67 inference(scs_inference,[],[48,2])).
% 86.61/86.67 cnf(52,plain,
% 86.61/86.67 (E(f5(f8(x521,x522),f8(x521,x523)),f8(f5(f5(x521,x521),f5(x521,x521)),f5(x522,x523)))),
% 86.61/86.67 inference(scs_inference,[],[47,28,48,2,3])).
% 86.61/86.67 cnf(54,plain,
% 86.61/86.67 (E(f8(f5(f5(x541,x541),f5(x541,x541)),f5(x542,x543)),f5(f8(x541,x542),f8(x541,x543)))),
% 86.61/86.67 inference(scs_inference,[],[52,2])).
% 86.61/86.67 cnf(55,plain,
% 86.61/86.67 (E(f3(x551,x552),f3(f3(f8(a4,x551),f8(a4,x552)),f3(f8(a4,x551),f8(a4,x552))))),
% 86.61/86.67 inference(scs_inference,[],[34,44,52,2,3])).
% 86.61/86.67 cnf(58,plain,
% 86.61/86.67 (E(f3(f3(f8(a4,x581),f8(a4,x582)),f3(f8(a4,x581),f8(a4,x582))),f3(x581,x582))),
% 86.61/86.67 inference(scs_inference,[],[55,2])).
% 86.61/86.67 cnf(59,plain,
% 86.61/86.67 (E(f8(f5(a4,a4),f5(x591,x592)),f5(x591,x592))),
% 86.61/86.67 inference(scs_inference,[],[51,41,55,2,3])).
% 86.61/86.67 cnf(62,plain,
% 86.61/86.67 (E(f5(x621,x622),f8(f5(a4,a4),f5(x621,x622)))),
% 86.61/86.67 inference(scs_inference,[],[59,2])).
% 86.61/86.67 cnf(63,plain,
% 86.61/86.67 (E(f8(x631,f5(x632,x633)),f8(f5(f5(x631,x631),f5(x631,x631)),f5(x632,x633)))),
% 86.61/86.67 inference(scs_inference,[],[47,31,59,2,3])).
% 86.61/86.67 cnf(65,plain,
% 86.61/86.67 (E(f8(f5(f5(x651,x651),f5(x651,x651)),f5(x652,x653)),f8(x651,f5(x652,x653)))),
% 86.61/86.67 inference(scs_inference,[],[63,2])).
% 86.61/86.67 cnf(66,plain,
% 86.61/86.67 (E(f8(f5(f5(f5(x661,x661),f5(x661,x661)),f5(f5(x661,x661),f5(x661,x661))),f5(x662,x663)),f5(f8(x661,x662),f8(x661,x663)))),
% 86.61/86.67 inference(scs_inference,[],[54,38,63,2,3])).
% 86.61/86.67 cnf(68,plain,
% 86.61/86.67 (E(f5(f8(x681,x682),f8(x681,x683)),f8(f5(f5(f5(x681,x681),f5(x681,x681)),f5(f5(x681,x681),f5(x681,x681))),f5(x682,x683)))),
% 86.61/86.67 inference(scs_inference,[],[66,2])).
% 86.61/86.67 cnf(69,plain,
% 86.61/86.67 (E(f8(f5(f5(x691,x691),f5(x691,x691)),f5(x692,x693)),f8(f5(a4,a4),f5(f8(x691,x692),f8(x691,x693))))),
% 86.61/86.67 inference(scs_inference,[],[62,54,66,2,3])).
% 86.61/86.67 cnf(71,plain,
% 86.61/86.67 (E(f8(f5(a4,a4),f5(f8(x711,x712),f8(x711,x713))),f8(f5(f5(x711,x711),f5(x711,x711)),f5(x712,x713)))),
% 86.61/86.67 inference(scs_inference,[],[69,2])).
% 86.61/86.67 cnf(72,plain,
% 86.61/86.67 (E(f5(f8(x721,x722),f8(x721,x723)),f8(f5(x721,x721),f5(x722,x723)))),
% 86.61/86.67 inference(scs_inference,[],[68,65,69,2,3])).
% 86.61/86.67 cnf(74,plain,
% 86.61/86.67 (E(f8(f5(x741,x741),f5(x742,x743)),f5(f8(x741,x742),f8(x741,x743)))),
% 86.61/86.67 inference(scs_inference,[],[72,2])).
% 86.61/86.67 cnf(75,plain,
% 86.61/86.67 (E(f8(f5(a4,a4),f5(f8(x751,x752),f8(x751,x753))),f8(x751,f5(x752,x753)))),
% 86.61/86.67 inference(scs_inference,[],[71,65,72,2,3])).
% 86.61/86.67 cnf(77,plain,
% 86.61/86.67 (E(f8(x771,f5(x772,x773)),f8(f5(a4,a4),f5(f8(x771,x772),f8(x771,x773))))),
% 86.61/86.67 inference(scs_inference,[],[75,2])).
% 86.61/86.67 cnf(78,plain,
% 86.61/86.67 (E(f5(f8(a4,x781),f8(a4,x782)),f5(x781,x782))),
% 86.61/86.67 inference(scs_inference,[],[51,28,75,2,3])).
% 86.61/86.67 cnf(80,plain,
% 86.61/86.67 (E(f5(x801,x802),f5(f8(a4,x801),f8(a4,x802)))),
% 86.61/86.67 inference(scs_inference,[],[78,2])).
% 86.61/86.67 cnf(81,plain,
% 86.61/86.67 (E(f8(x811,f5(x812,x813)),f5(f8(a4,f8(x811,x812)),f8(a4,f8(x811,x813))))),
% 86.61/86.67 inference(scs_inference,[],[74,77,78,2,3])).
% 86.61/86.67 cnf(83,plain,
% 86.61/86.67 (E(f5(f8(a4,f8(x831,x832)),f8(a4,f8(x831,x833))),f8(x831,f5(x832,x833)))),
% 86.61/86.67 inference(scs_inference,[],[81,2])).
% 86.61/86.67 cnf(84,plain,
% 86.61/86.67 (E(f8(f5(x841,x841),f5(x842,x843)),f5(f8(a4,f8(x841,x842)),f8(a4,f8(x841,x843))))),
% 86.61/86.67 inference(scs_inference,[],[80,74,81,2,3])).
% 86.61/86.67 cnf(86,plain,
% 86.61/86.67 (E(f5(f8(a4,f8(x861,x862)),f8(a4,f8(x861,x863))),f8(f5(x861,x861),f5(x862,x863)))),
% 86.61/86.67 inference(scs_inference,[],[84,2])).
% 86.61/86.67 cnf(87,plain,
% 86.61/86.67 (E(f5(x871,x872),f8(f5(f5(f5(a4,a4),f5(a4,a4)),f5(f5(a4,a4),f5(a4,a4))),f5(x871,x872)))),
% 86.61/86.67 inference(scs_inference,[],[68,80,84,2,3])).
% 86.61/86.67 cnf(89,plain,
% 86.61/86.67 (E(f8(f5(f5(f5(a4,a4),f5(a4,a4)),f5(f5(a4,a4),f5(a4,a4))),f5(x891,x892)),f5(x891,x892))),
% 86.61/86.67 inference(scs_inference,[],[87,2])).
% 86.61/86.67 cnf(90,plain,
% 86.61/86.67 (E(f8(f5(f5(a4,a4),f5(a4,a4)),f5(f8(x901,x902),f8(x901,x903))),f8(f5(x901,x901),f5(x902,x903)))),
% 86.61/86.67 inference(scs_inference,[],[86,54,87,2,3])).
% 86.61/86.67 cnf(92,plain,
% 86.61/86.67 (E(f8(f5(x921,x921),f5(x922,x923)),f8(f5(f5(a4,a4),f5(a4,a4)),f5(f8(x921,x922),f8(x921,x923))))),
% 86.61/86.67 inference(scs_inference,[],[90,2])).
% 86.61/86.67 cnf(93,plain,
% 86.61/86.67 (E(f8(f5(f5(f5(a4,a4),f5(a4,a4)),f5(f5(a4,a4),f5(a4,a4))),f5(x931,x932)),f8(a4,f5(x931,x932)))),
% 86.61/86.67 inference(scs_inference,[],[89,44,90,2,3])).
% 86.61/86.67 cnf(95,plain,
% 86.61/86.67 (E(f8(a4,f5(x951,x952)),f8(f5(f5(f5(a4,a4),f5(a4,a4)),f5(f5(a4,a4),f5(a4,a4))),f5(x951,x952)))),
% 86.61/86.67 inference(scs_inference,[],[93,2])).
% 86.61/86.67 cnf(96,plain,
% 86.61/86.67 (E(f8(f5(x961,x961),f3(x962,x963)),f3(f3(f8(x961,x962),f8(x961,x963)),f3(f8(x961,x962),f8(x961,x963))))),
% 86.61/86.67 inference(scs_inference,[],[34,38,93,2,3])).
% 86.61/86.67 cnf(99,plain,
% 86.61/86.67 (E(f3(f3(f8(x991,x992),f8(x991,x993)),f3(f8(x991,x992),f8(x991,x993))),f8(f5(x991,x991),f3(x992,x993)))),
% 86.61/86.67 inference(scs_inference,[],[96,2])).
% 86.61/86.67 cnf(100,plain,
% 86.61/86.67 (E(f8(f5(x1001,x1001),f5(x1002,x1003)),f8(a4,f5(f8(x1001,x1002),f8(x1001,x1003))))),
% 86.61/86.67 inference(scs_inference,[],[92,65,96,2,3])).
% 86.61/86.67 cnf(102,plain,
% 86.61/86.67 (E(f8(a4,f5(f8(x1021,x1022),f8(x1021,x1023))),f8(f5(x1021,x1021),f5(x1022,x1023)))),
% 86.61/86.67 inference(scs_inference,[],[100,2])).
% 86.61/86.67 cnf(103,plain,
% 86.61/86.67 (E(f5(f8(a4,f8(x1031,x1032)),f8(a4,f8(x1031,x1033))),f8(f5(f5(x1031,x1031),f5(x1031,x1031)),f5(x1032,x1033)))),
% 86.61/86.67 inference(scs_inference,[],[83,100,63,2,3])).
% 86.61/86.67 cnf(105,plain,
% 86.61/86.67 (E(f8(f5(f5(x1051,x1051),f5(x1051,x1051)),f5(x1052,x1053)),f5(f8(a4,f8(x1051,x1052)),f8(a4,f8(x1051,x1053))))),
% 86.61/86.67 inference(scs_inference,[],[103,2])).
% 86.61/86.67 cnf(106,plain,
% 86.61/86.67 (E(f8(a4,f5(f8(a4,x1061),f8(a4,x1062))),f5(x1061,x1062))),
% 86.61/86.67 inference(scs_inference,[],[102,103,59,2,3])).
% 86.61/86.67 cnf(109,plain,
% 86.61/86.67 (E(f5(x1091,x1092),f8(a4,f5(f8(a4,x1091),f8(a4,x1092))))),
% 86.61/86.67 inference(scs_inference,[],[106,2])).
% 86.61/86.67 cnf(110,plain,
% 86.61/86.67 (E(f8(a4,f5(x1101,x1102)),f5(f8(f5(a4,a4),x1101),f8(f5(a4,a4),x1102)))),
% 86.61/86.67 inference(scs_inference,[],[95,54,106,2,3])).
% 86.61/86.67 cnf(112,plain,
% 86.61/86.67 (E(f5(f8(f5(a4,a4),x1121),f8(f5(a4,a4),x1122)),f8(a4,f5(x1121,x1122)))),
% 86.61/86.67 inference(scs_inference,[],[110,2])).
% 86.61/86.67 cnf(113,plain,
% 86.61/86.67 (E(f8(f5(x1131,x1131),f5(x1132,x1133)),f5(f8(f5(a4,a4),f8(x1131,x1132)),f8(f5(a4,a4),f8(x1131,x1133))))),
% 86.61/86.67 inference(scs_inference,[],[92,74,110,2,3])).
% 86.61/86.67 cnf(115,plain,
% 86.61/86.67 (E(f5(f8(f5(a4,a4),f8(x1151,x1152)),f8(f5(a4,a4),f8(x1151,x1153))),f8(f5(x1151,x1151),f5(x1152,x1153)))),
% 86.61/86.67 inference(scs_inference,[],[113,2])).
% 86.61/86.67 cnf(116,plain,
% 86.61/86.67 (E(f8(f5(f5(x1161,x1161),f5(x1161,x1161)),f5(x1162,x1163)),f8(f5(f5(a4,a4),f5(a4,a4)),f5(f8(x1161,x1162),f8(x1161,x1163))))),
% 86.61/86.67 inference(scs_inference,[],[105,113,52,2,3])).
% 86.61/86.67 cnf(118,plain,
% 86.61/86.67 (E(f8(f5(f5(a4,a4),f5(a4,a4)),f5(f8(x1181,x1182),f8(x1181,x1183))),f8(f5(f5(x1181,x1181),f5(x1181,x1181)),f5(x1182,x1183)))),
% 86.61/86.67 inference(scs_inference,[],[116,2])).
% 86.61/86.67 cnf(119,plain,
% 86.61/86.67 (E(f5(f8(f5(a4,a4),f8(x1191,x1192)),f8(f5(a4,a4),f8(x1191,x1193))),f5(f8(x1191,x1192),f8(x1191,x1193)))),
% 86.61/86.67 inference(scs_inference,[],[115,74,116,2,3])).
% 86.61/86.67 cnf(121,plain,
% 86.61/86.67 (E(f5(f8(x1211,x1212),f8(x1211,x1213)),f5(f8(f5(a4,a4),f8(x1211,x1212)),f8(f5(a4,a4),f8(x1211,x1213))))),
% 86.61/86.67 inference(scs_inference,[],[119,2])).
% 86.61/86.67 cnf(122,plain,
% 86.61/86.67 (E(f8(f5(f5(a4,a4),f5(a4,a4)),f5(f8(x1221,x1222),f8(x1221,x1223))),f8(x1221,f5(x1222,x1223)))),
% 86.61/86.67 inference(scs_inference,[],[118,65,119,2,3])).
% 86.61/86.67 cnf(124,plain,
% 86.61/86.67 (E(f8(x1241,f5(x1242,x1243)),f8(f5(f5(a4,a4),f5(a4,a4)),f5(f8(x1241,x1242),f8(x1241,x1243))))),
% 86.61/86.67 inference(scs_inference,[],[122,2])).
% 86.61/86.67 cnf(125,plain,
% 86.61/86.67 (E(f5(f8(x1251,x1252),f8(x1251,x1253)),f8(f5(f5(a4,a4),f5(a4,a4)),f5(f8(x1251,x1252),f8(x1251,x1253))))),
% 86.61/86.67 inference(scs_inference,[],[121,122,72,2,3])).
% 86.61/86.67 cnf(127,plain,
% 86.61/86.67 (E(f8(f5(f5(a4,a4),f5(a4,a4)),f5(f8(x1271,x1272),f8(x1271,x1273))),f5(f8(x1271,x1272),f8(x1271,x1273)))),
% 86.61/86.67 inference(scs_inference,[],[125,2])).
% 86.61/86.67 cnf(128,plain,
% 86.61/86.67 (E(f8(x1281,f5(x1282,x1283)),f8(a4,f5(f8(x1281,x1282),f8(x1281,x1283))))),
% 86.61/86.67 inference(scs_inference,[],[124,65,125,2,3])).
% 86.61/86.67 cnf(130,plain,
% 86.61/86.67 (E(f8(a4,f5(f8(x1301,x1302),f8(x1301,x1303))),f8(x1301,f5(x1302,x1303)))),
% 86.61/86.67 inference(scs_inference,[],[128,2])).
% 86.61/86.67 cnf(131,plain,
% 86.61/86.67 (E(f8(f5(f5(a4,a4),f5(a4,a4)),f5(f8(a4,x1311),f8(a4,x1312))),f5(x1311,x1312))),
% 86.61/86.67 inference(scs_inference,[],[127,128,78,2,3])).
% 86.61/86.67 cnf(134,plain,
% 86.61/86.67 (E(f5(x1341,x1342),f8(f5(f5(a4,a4),f5(a4,a4)),f5(f8(a4,x1341),f8(a4,x1342))))),
% 86.61/86.67 inference(scs_inference,[],[131,2])).
% 86.61/86.67 cnf(135,plain,
% 86.61/86.67 (E(f5(f8(f5(a4,a4),f8(x1351,x1352)),f8(f5(a4,a4),f8(x1351,x1353))),f8(x1351,f5(x1352,x1353)))),
% 86.61/86.67 inference(scs_inference,[],[130,112,131,2,3])).
% 86.61/86.67 cnf(138,plain,
% 86.61/86.67 (E(f5(x1381,x1382),f8(f5(f5(a4,a4),f5(a4,a4)),f5(x1381,x1382)))),
% 86.61/86.67 inference(scs_inference,[],[134,118,135,2,3])).
% 86.61/86.67 cnf(140,plain,
% 86.61/86.67 (E(f8(f5(f5(a4,a4),f5(a4,a4)),f5(x1401,x1402)),f5(x1401,x1402))),
% 86.61/86.67 inference(scs_inference,[],[138,2])).
% 86.61/86.67 cnf(143,plain,
% 86.61/86.67 (E(f8(f3(x1431,x1432),x1433),f3(f8(x1431,x1433),f8(x1432,x1433)))),
% 86.61/86.67 inference(scs_inference,[],[26,2])).
% 86.61/86.67 cnf(144,plain,
% 86.61/86.67 (E(f8(f5(f5(a4,a4),f5(a4,a4)),f5(x1441,x1442)),f8(a4,f5(f8(a4,x1441),f8(a4,x1442))))),
% 86.61/86.67 inference(scs_inference,[],[140,109,26,2,3])).
% 86.61/86.67 cnf(146,plain,
% 86.61/86.67 (E(f8(a4,f5(f8(a4,x1461),f8(a4,x1462))),f8(f5(f5(a4,a4),f5(a4,a4)),f5(x1461,x1462)))),
% 86.61/86.67 inference(scs_inference,[],[144,2])).
% 86.61/86.67 cnf(147,plain,
% 86.61/86.67 (E(f5(f8(f5(a4,a4),f8(a4,x1471)),f8(f5(a4,a4),f8(a4,x1472))),f5(x1471,x1472))),
% 86.61/86.67 inference(scs_inference,[],[115,144,59,2,3])).
% 86.61/86.67 cnf(150,plain,
% 86.61/86.67 (E(f5(x1501,x1502),f5(f8(f5(a4,a4),f8(a4,x1501)),f8(f5(a4,a4),f8(a4,x1502))))),
% 86.61/86.67 inference(scs_inference,[],[147,2])).
% 86.61/86.67 cnf(151,plain,
% 86.61/86.67 (E(f8(f5(f5(a4,a4),f5(a4,a4)),f5(f5(x1511,x1512),x1513)),f5(x1511,f5(x1512,x1513)))),
% 86.61/86.67 inference(scs_inference,[],[140,147,20,2,3])).
% 86.61/86.67 cnf(154,plain,
% 86.61/86.67 (E(f5(x1541,f5(x1542,x1543)),f8(f5(f5(a4,a4),f5(a4,a4)),f5(f5(x1541,x1542),x1543)))),
% 86.61/86.67 inference(scs_inference,[],[151,2])).
% 86.61/86.67 cnf(155,plain,
% 86.61/86.67 (E(f8(a4,f5(f8(a4,f5(x1551,x1552)),f8(a4,x1553))),f5(x1551,f5(x1552,x1553)))),
% 86.61/86.67 inference(scs_inference,[],[146,151,2,3])).
% 86.61/86.67 cnf(158,plain,
% 86.61/86.67 (E(f5(x1581,f5(x1582,x1583)),f8(a4,f5(f8(a4,f5(x1581,x1582)),f8(a4,x1583))))),
% 86.61/86.67 inference(scs_inference,[],[155,2])).
% 86.61/86.67 cnf(161,plain,
% 86.61/86.67 (E(x1611,f5(x1611,f3(x1611,x1612)))),
% 86.61/86.67 inference(scs_inference,[],[18,2])).
% 86.61/86.67 cnf(162,plain,
% 86.61/86.67 (E(f5(x1621,f5(x1622,x1623)),f8(f5(a4,a4),f5(f5(x1621,x1622),x1623)))),
% 86.61/86.67 inference(scs_inference,[],[158,102,18,2,3])).
% 86.61/86.67 cnf(164,plain,
% 86.61/86.67 (E(f8(f5(a4,a4),f5(f5(x1641,x1642),x1643)),f5(x1641,f5(x1642,x1643)))),
% 86.61/86.67 inference(scs_inference,[],[162,2])).
% 86.61/86.67 cnf(165,plain,
% 86.61/86.67 (E(x1651,f8(f5(a4,a4),f5(x1651,f3(x1651,x1652))))),
% 86.61/86.67 inference(scs_inference,[],[161,62,162,2,3])).
% 86.61/86.67 cnf(167,plain,
% 86.61/86.67 (E(f8(f5(a4,a4),f5(x1671,f3(x1671,x1672))),x1671)),
% 86.61/86.67 inference(scs_inference,[],[165,2])).
% 86.61/86.67 cnf(168,plain,
% 86.61/86.67 (E(f8(f5(a4,a4),f5(f5(f5(f8(a4,x1681),f8(a4,x1682)),f8(a4,x1681)),f8(a4,x1682))),f5(x1681,x1682))),
% 86.61/86.67 inference(scs_inference,[],[164,51,165,2,3])).
% 86.61/86.67 cnf(170,plain,
% 86.61/86.67 (E(f5(x1701,x1702),f8(f5(a4,a4),f5(f5(f5(f8(a4,x1701),f8(a4,x1702)),f8(a4,x1701)),f8(a4,x1702))))),
% 86.61/86.67 inference(scs_inference,[],[168,2])).
% 86.61/86.67 cnf(171,plain,
% 86.61/86.67 (E(f8(f5(a4,a4),f5(f3(a1,a2),f3(f3(a1,a2),x1711))),a2)),
% 86.61/86.67 inference(scs_inference,[],[167,168,11,2,3])).
% 86.61/86.67 cnf(173,plain,
% 86.61/86.67 (E(a2,f8(f5(a4,a4),f5(f3(a1,a2),f3(f3(a1,a2),x1731))))),
% 86.61/86.67 inference(scs_inference,[],[171,2])).
% 86.61/86.67 cnf(174,plain,
% 86.61/86.67 (E(f5(x1741,f5(x1742,x1743)),f5(f8(a4,f5(x1741,x1742)),f8(a4,x1743)))),
% 86.61/86.67 inference(scs_inference,[],[154,54,171,2,3])).
% 86.61/86.67 cnf(176,plain,
% 86.61/86.68 (E(f5(f8(a4,f5(x1761,x1762)),f8(a4,x1763)),f5(x1761,f5(x1762,x1763)))),
% 86.61/86.68 inference(scs_inference,[],[174,2])).
% 86.61/86.68 cnf(177,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(f5(f5(f8(x1771,x1772),f8(x1771,x1773)),f8(x1771,x1772)),f8(x1771,x1773))),f8(f5(x1771,x1771),f5(x1772,x1773)))),
% 86.61/86.68 inference(scs_inference,[],[164,174,39,2,3])).
% 86.61/86.68 cnf(179,plain,
% 86.61/86.68 (E(f8(f5(x1791,x1791),f5(x1792,x1793)),f8(f5(a4,a4),f5(f5(f5(f8(x1791,x1792),f8(x1791,x1793)),f8(x1791,x1792)),f8(x1791,x1793))))),
% 86.61/86.68 inference(scs_inference,[],[177,2])).
% 86.61/86.68 cnf(180,plain,
% 86.61/86.68 (E(f5(x1801,x1802),f5(f5(f5(f8(a4,x1801),f8(a4,x1802)),f8(a4,x1801)),f8(a4,x1802)))),
% 86.61/86.68 inference(scs_inference,[],[170,177,59,2,3])).
% 86.61/86.68 cnf(182,plain,
% 86.61/86.68 (E(f5(f5(f5(f8(a4,x1821),f8(a4,x1822)),f8(a4,x1821)),f8(a4,x1822)),f5(x1821,x1822))),
% 86.61/86.68 inference(scs_inference,[],[180,2])).
% 86.61/86.68 cnf(183,plain,
% 86.61/86.68 (E(f8(f5(x1831,x1831),f5(x1832,x1833)),f5(f5(f5(f8(x1831,x1832),f8(x1831,x1833)),f8(x1831,x1832)),f8(x1831,x1833)))),
% 86.61/86.68 inference(scs_inference,[],[179,180,59,2,3])).
% 86.61/86.68 cnf(185,plain,
% 86.61/86.68 (E(f5(f5(f5(f8(x1851,x1852),f8(x1851,x1853)),f8(x1851,x1852)),f8(x1851,x1853)),f8(f5(x1851,x1851),f5(x1852,x1853)))),
% 86.61/86.68 inference(scs_inference,[],[183,2])).
% 86.61/86.68 cnf(186,plain,
% 86.61/86.68 (E(a2,f5(f3(a1,a2),f3(f3(a1,a2),x1861)))),
% 86.61/86.68 inference(scs_inference,[],[173,183,59,2,3])).
% 86.61/86.68 cnf(188,plain,
% 86.61/86.68 (E(f5(f3(a1,a2),f3(f3(a1,a2),x1881)),a2)),
% 86.61/86.68 inference(scs_inference,[],[186,2])).
% 86.61/86.68 cnf(189,plain,
% 86.61/86.68 (E(f5(f5(f5(f8(x1891,x1892),f8(x1891,x1893)),f8(x1891,x1892)),f8(x1891,x1893)),f5(f8(x1891,x1892),f8(x1891,x1893)))),
% 86.61/86.68 inference(scs_inference,[],[185,74,186,2,3])).
% 86.61/86.68 cnf(191,plain,
% 86.61/86.68 (E(f5(f8(x1911,x1912),f8(x1911,x1913)),f5(f5(f5(f8(x1911,x1912),f8(x1911,x1913)),f8(x1911,x1912)),f8(x1911,x1913)))),
% 86.61/86.68 inference(scs_inference,[],[189,2])).
% 86.61/86.68 cnf(192,plain,
% 86.61/86.68 (E(f5(f5(f5(f8(x1921,x1922),f8(x1921,x1923)),f8(x1921,x1922)),f8(x1921,x1923)),f8(a4,f5(f8(x1921,x1922),f8(x1921,x1923))))),
% 86.61/86.68 inference(scs_inference,[],[185,189,100,2,3])).
% 86.61/86.68 cnf(195,plain,
% 86.61/86.68 (E(f5(f8(x1951,x1952),f8(x1951,x1953)),f8(f5(a4,a4),f5(f5(f5(f8(x1951,x1952),f8(x1951,x1953)),f8(x1951,x1952)),f8(x1951,x1953))))),
% 86.61/86.68 inference(scs_inference,[],[191,62,192,2,3])).
% 86.61/86.68 cnf(197,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(f5(f5(f8(x1971,x1972),f8(x1971,x1973)),f8(x1971,x1972)),f8(x1971,x1973))),f5(f8(x1971,x1972),f8(x1971,x1973)))),
% 86.61/86.68 inference(scs_inference,[],[195,2])).
% 86.61/86.68 cnf(199,plain,
% 86.61/86.68 (E(x1991,f3(x1991,f5(x1991,x1992)))),
% 86.61/86.68 inference(scs_inference,[],[19,2])).
% 86.61/86.68 cnf(200,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(a2,f3(a2,x2001))),f5(f3(a1,a2),f3(f3(a1,a2),x2002)))),
% 86.61/86.68 inference(scs_inference,[],[167,186,19,2,3])).
% 86.61/86.68 cnf(202,plain,
% 86.61/86.68 (E(f5(f3(a1,a2),f3(f3(a1,a2),x2021)),f8(f5(a4,a4),f5(a2,f3(a2,x2022))))),
% 86.61/86.68 inference(scs_inference,[],[200,2])).
% 86.61/86.68 cnf(203,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(f8(a4,f5(x2031,x2032)),f8(a4,x2033))),f5(x2031,f5(x2032,x2033)))),
% 86.61/86.68 inference(scs_inference,[],[71,200,151,2,3])).
% 86.61/86.68 cnf(206,plain,
% 86.61/86.68 (E(f5(x2061,f5(x2062,x2063)),f8(f5(a4,a4),f5(f8(a4,f5(x2061,x2062)),f8(a4,x2063))))),
% 86.61/86.68 inference(scs_inference,[],[203,2])).
% 86.61/86.68 cnf(207,plain,
% 86.61/86.68 (E(f5(f3(a1,a2),f3(f3(a1,a2),x2071)),f5(f8(a4,a2),f8(a4,f3(a2,x2072))))),
% 86.61/86.68 inference(scs_inference,[],[202,74,203,2,3])).
% 86.61/86.68 cnf(209,plain,
% 86.61/86.68 (E(f5(f8(a4,a2),f8(a4,f3(a2,x2091))),f5(f3(a1,a2),f3(f3(a1,a2),x2092)))),
% 86.61/86.68 inference(scs_inference,[],[207,2])).
% 86.61/86.68 cnf(210,plain,
% 86.61/86.68 (E(f5(x2101,f5(x2102,x2103)),f8(a4,f5(f5(x2101,x2102),x2103)))),
% 86.61/86.68 inference(scs_inference,[],[206,207,75,2,3])).
% 86.61/86.68 cnf(212,plain,
% 86.61/86.68 (E(f8(a4,f5(f5(x2121,x2122),x2123)),f5(x2121,f5(x2122,x2123)))),
% 86.61/86.68 inference(scs_inference,[],[210,2])).
% 86.61/86.68 cnf(213,plain,
% 86.61/86.68 (E(f3(x2131,x2132),f3(x2131,f3(x2132,f5(f3(x2131,x2132),x2133))))),
% 86.61/86.68 inference(scs_inference,[],[199,210,21,2,3])).
% 86.61/86.68 cnf(216,plain,
% 86.61/86.68 (E(f3(x2161,f3(x2162,f5(f3(x2161,x2162),x2163))),f3(x2161,x2162))),
% 86.61/86.68 inference(scs_inference,[],[213,2])).
% 86.61/86.68 cnf(217,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(f5(f5(f8(x2171,x2172),f8(x2171,x2173)),f8(x2171,x2172)),f8(x2171,x2173))),f8(x2171,f5(x2172,x2173)))),
% 86.61/86.68 inference(scs_inference,[],[197,213,23,2,3])).
% 86.61/86.68 cnf(219,plain,
% 86.61/86.68 (E(f8(x2191,f5(x2192,x2193)),f8(f5(a4,a4),f5(f5(f5(f8(x2191,x2192),f8(x2191,x2193)),f8(x2191,x2192)),f8(x2191,x2193))))),
% 86.61/86.68 inference(scs_inference,[],[217,2])).
% 86.61/86.68 cnf(220,plain,
% 86.61/86.68 (E(f3(a1,f3(a2,f5(f3(a1,a2),x2201))),a2)),
% 86.61/86.68 inference(scs_inference,[],[216,217,11,2,3])).
% 86.61/86.68 cnf(222,plain,
% 86.61/86.68 (E(a2,f3(a1,f3(a2,f5(f3(a1,a2),x2221))))),
% 86.61/86.68 inference(scs_inference,[],[220,2])).
% 86.61/86.68 cnf(223,plain,
% 86.61/86.68 (E(f8(x2231,f5(x2232,x2233)),f5(f5(f5(f8(x2231,x2232),f8(x2231,x2233)),f8(x2231,x2232)),f8(x2231,x2233)))),
% 86.61/86.68 inference(scs_inference,[],[219,220,59,2,3])).
% 86.61/86.68 cnf(225,plain,
% 86.61/86.68 (E(f5(f5(f5(f8(x2251,x2252),f8(x2251,x2253)),f8(x2251,x2252)),f8(x2251,x2253)),f8(x2251,f5(x2252,x2253)))),
% 86.61/86.68 inference(scs_inference,[],[223,2])).
% 86.61/86.68 cnf(226,plain,
% 86.61/86.68 (E(f8(f3(x2261,x2261),x2262),f8(x2261,f3(x2262,x2262)))),
% 86.61/86.68 inference(scs_inference,[],[143,223,24,2,3])).
% 86.61/86.68 cnf(229,plain,
% 86.61/86.68 (E(f8(x2291,f3(x2292,x2292)),f8(f3(x2291,x2291),x2292))),
% 86.61/86.68 inference(scs_inference,[],[226,2])).
% 86.61/86.68 cnf(230,plain,
% 86.61/86.68 (E(f5(f5(f5(f8(x2301,x2302),f8(x2301,x2303)),f8(x2301,x2302)),f8(x2301,x2303)),f8(f5(a4,a4),f5(f8(x2301,x2302),f8(x2301,x2303))))),
% 86.61/86.68 inference(scs_inference,[],[225,77,226,2,3])).
% 86.61/86.68 cnf(232,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(f8(x2321,x2322),f8(x2321,x2323))),f5(f5(f5(f8(x2321,x2322),f8(x2321,x2323)),f8(x2321,x2322)),f8(x2321,x2323)))),
% 86.61/86.68 inference(scs_inference,[],[230,2])).
% 86.61/86.68 cnf(235,plain,
% 86.61/86.68 (E(f8(x2351,f8(x2352,x2353)),f8(f8(x2351,x2352),x2353))),
% 86.61/86.68 inference(scs_inference,[],[22,2])).
% 86.61/86.68 cnf(236,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(f8(a4,x2361),f8(a4,x2362))),f5(x2361,x2362))),
% 86.61/86.68 inference(scs_inference,[],[232,182,22,2,3])).
% 86.61/86.68 cnf(239,plain,
% 86.61/86.68 (E(f5(x2391,x2392),f8(f5(a4,a4),f5(f8(a4,x2391),f8(a4,x2392))))),
% 86.61/86.68 inference(scs_inference,[],[236,2])).
% 86.61/86.68 cnf(240,plain,
% 86.61/86.68 (E(f8(x2401,f3(f8(x2402,x2403),f8(x2402,x2403))),f8(f8(f3(x2401,x2401),x2402),x2403))),
% 86.61/86.68 inference(scs_inference,[],[235,229,236,2,3])).
% 86.61/86.68 cnf(244,plain,
% 86.61/86.68 (E(f5(f8(a4,a2),f8(a4,f3(a2,x2441))),f8(f5(a4,a4),f5(a2,f3(a2,x2442))))),
% 86.61/86.68 inference(scs_inference,[],[209,202,240,2,3])).
% 86.61/86.68 cnf(246,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(a2,f3(a2,x2461))),f5(f8(a4,a2),f8(a4,f3(a2,x2462))))),
% 86.61/86.68 inference(scs_inference,[],[244,2])).
% 86.61/86.68 cnf(247,plain,
% 86.61/86.68 (E(f3(a1,a2),f8(f5(a4,a4),f5(a2,f3(a2,x2471))))),
% 86.61/86.68 inference(scs_inference,[],[161,202,244,2,3])).
% 86.61/86.68 cnf(250,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(a2,f3(a2,x2501))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[247,2])).
% 86.61/86.68 cnf(251,plain,
% 86.61/86.68 (E(f5(x2511,x2512),f5(f8(a4,f8(a4,x2511)),f8(a4,f8(a4,x2512))))),
% 86.61/86.68 inference(scs_inference,[],[239,74,247,2,3])).
% 86.61/86.68 cnf(253,plain,
% 86.61/86.68 (E(f5(f8(a4,f8(a4,x2531)),f8(a4,f8(a4,x2532))),f5(x2531,x2532))),
% 86.61/86.68 inference(scs_inference,[],[251,2])).
% 86.61/86.68 cnf(256,plain,
% 86.61/86.68 (E(a4,f8(f7(x2561),x2561))),
% 86.61/86.68 inference(scs_inference,[],[15,2])).
% 86.61/86.68 cnf(257,plain,
% 86.61/86.68 (E(f5(f5(f5(f8(x2571,x2572),f8(x2571,x2573)),f8(x2571,x2572)),f8(x2571,x2573)),f8(f5(f5(x2571,x2571),f5(x2571,x2571)),f5(x2572,x2573)))),
% 86.61/86.68 inference(scs_inference,[],[225,63,15,2,3])).
% 86.61/86.68 cnf(259,plain,
% 86.61/86.68 (E(f8(f5(f5(x2591,x2591),f5(x2591,x2591)),f5(x2592,x2593)),f5(f5(f5(f8(x2591,x2592),f8(x2591,x2593)),f8(x2591,x2592)),f8(x2591,x2593)))),
% 86.61/86.68 inference(scs_inference,[],[257,2])).
% 86.61/86.68 cnf(272,plain,
% 86.61/86.68 (E(x2721,f3(x2721,x2721))),
% 86.61/86.68 inference(scs_inference,[],[14,2])).
% 86.61/86.68 cnf(273,plain,
% 86.61/86.68 (E(f8(f5(f5(x2731,x2731),f5(x2731,x2731)),f5(x2732,x2733)),f8(a4,f5(f8(x2731,x2732),f8(x2731,x2733))))),
% 86.61/86.68 inference(scs_inference,[],[259,192,14,2,3])).
% 86.61/86.68 cnf(276,plain,
% 86.61/86.68 (E(f3(f8(x2761,x2762),f8(x2761,x2763)),f8(f5(x2761,x2761),f3(x2762,x2763)))),
% 86.61/86.68 inference(scs_inference,[],[272,99,273,2,3])).
% 86.61/86.68 cnf(278,plain,
% 86.61/86.68 (E(f8(f5(x2781,x2781),f3(x2782,x2783)),f3(f8(x2781,x2782),f8(x2781,x2783)))),
% 86.61/86.68 inference(scs_inference,[],[276,2])).
% 86.61/86.68 cnf(279,plain,
% 86.61/86.68 (E(f3(f8(a4,x2791),f8(a4,x2792)),f3(x2791,x2792))),
% 86.61/86.68 inference(scs_inference,[],[58,272,276,2,3])).
% 86.61/86.68 cnf(281,plain,
% 86.61/86.68 (E(f3(x2811,x2812),f3(f8(a4,x2811),f8(a4,x2812)))),
% 86.61/86.68 inference(scs_inference,[],[279,2])).
% 86.61/86.68 cnf(282,plain,
% 86.61/86.68 (E(a2,f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[222,216,279,2,3])).
% 86.61/86.68 cnf(284,plain,
% 86.61/86.68 (E(f8(f5(x2841,x2842),x2843),f5(f8(x2841,x2843),f8(x2842,x2843)))),
% 86.61/86.68 inference(scs_inference,[],[25,2])).
% 86.61/86.68 cnf(285,plain,
% 86.61/86.68 (E(f8(f5(x2851,x2851),f3(x2852,x2853)),f3(f8(a4,f8(x2851,x2852)),f8(a4,f8(x2851,x2853))))),
% 86.61/86.68 inference(scs_inference,[],[278,281,25,2,3])).
% 86.61/86.68 cnf(287,plain,
% 86.61/86.68 (E(f3(f8(a4,f8(x2871,x2872)),f8(a4,f8(x2871,x2873))),f8(f5(x2871,x2871),f3(x2872,x2873)))),
% 86.61/86.68 inference(scs_inference,[],[285,2])).
% 86.61/86.68 cnf(288,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(x2881,x2882)),f5(x2881,f5(x2882,f5(x2881,x2882))))),
% 86.61/86.68 inference(scs_inference,[],[284,176,285,2,3])).
% 86.61/86.68 cnf(291,plain,
% 86.61/86.68 (E(f5(x2911,f5(x2912,f5(x2911,x2912))),f8(f5(a4,a4),f5(x2911,x2912)))),
% 86.61/86.68 inference(scs_inference,[],[288,2])).
% 86.61/86.68 cnf(292,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(f8(x2921,x2922),f8(x2921,x2923))),f8(f5(x2921,x2921),f3(x2922,x2923)))),
% 86.61/86.68 inference(scs_inference,[],[287,278,288,2,3])).
% 86.61/86.68 cnf(294,plain,
% 86.61/86.68 (E(f8(f5(x2941,x2941),f3(x2942,x2943)),f8(f5(a4,a4),f3(f8(x2941,x2942),f8(x2941,x2943))))),
% 86.61/86.68 inference(scs_inference,[],[292,2])).
% 86.61/86.68 cnf(295,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f8(a4,x2951)),f5(x2951,x2951))),
% 86.61/86.68 inference(scs_inference,[],[253,284,292,2,3])).
% 86.61/86.68 cnf(298,plain,
% 86.61/86.68 (E(f5(x2981,x2981),f8(f5(a4,a4),f8(a4,x2981)))),
% 86.61/86.68 inference(scs_inference,[],[295,2])).
% 86.61/86.68 cnf(299,plain,
% 86.61/86.68 (E(f8(a4,f5(f5(x2991,x2992),f5(x2991,x2992))),f8(f5(a4,a4),f5(x2991,x2992)))),
% 86.61/86.68 inference(scs_inference,[],[291,212,295,2,3])).
% 86.61/86.68 cnf(302,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(x3021,x3022)),f8(a4,f5(f5(x3021,x3022),f5(x3021,x3022))))),
% 86.61/86.68 inference(scs_inference,[],[299,2])).
% 86.61/86.68 cnf(303,plain,
% 86.61/86.68 (E(f5(x3031,x3031),f8(f5(a4,a4),f8(a4,f8(f5(a4,a4),f8(a4,x3031)))))),
% 86.61/86.68 inference(scs_inference,[],[150,298,299,2,3])).
% 86.61/86.68 cnf(306,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f8(a4,f8(f5(a4,a4),f8(a4,x3061)))),f5(x3061,x3061))),
% 86.61/86.68 inference(scs_inference,[],[303,2])).
% 86.61/86.68 cnf(307,plain,
% 86.61/86.68 (E(f5(a2,f5(f3(a2,x3071),f5(a2,f3(a2,x3071)))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[250,291,303,2,3])).
% 86.61/86.68 cnf(310,plain,
% 86.61/86.68 (E(x3101,f3(f8(a4,x3101),f8(a4,f5(x3101,x3102))))),
% 86.61/86.68 inference(scs_inference,[],[199,281,307,2,3])).
% 86.61/86.68 cnf(312,plain,
% 86.61/86.68 (E(f3(f8(a4,x3121),f8(a4,f5(x3121,x3122))),x3121)),
% 86.61/86.68 inference(scs_inference,[],[310,2])).
% 86.61/86.68 cnf(313,plain,
% 86.61/86.68 (E(f3(f3(f8(a4,a1),f8(a4,a2)),f3(f8(a4,a1),f8(a4,a2))),a2)),
% 86.61/86.68 inference(scs_inference,[],[58,310,11,2,3])).
% 86.61/86.68 cnf(315,plain,
% 86.61/86.68 (E(a2,f3(f3(f8(a4,a1),f8(a4,a2)),f3(f8(a4,a1),f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[313,2])).
% 86.61/86.68 cnf(316,plain,
% 86.61/86.68 (E(f3(f8(a4,a4),f8(a4,f5(a4,x3161))),f8(f7(x3162),x3162))),
% 86.61/86.68 inference(scs_inference,[],[312,256,313,2,3])).
% 86.61/86.68 cnf(318,plain,
% 86.61/86.68 (E(f8(f7(x3181),x3181),f3(f8(a4,a4),f8(a4,f5(a4,x3182))))),
% 86.61/86.68 inference(scs_inference,[],[316,2])).
% 86.61/86.68 cnf(319,plain,
% 86.61/86.68 (E(a2,f8(f5(a4,a4),f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[315,99,316,2,3])).
% 86.61/86.68 cnf(321,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(a1,a2)),a2)),
% 86.61/86.68 inference(scs_inference,[],[319,2])).
% 86.61/86.68 cnf(322,plain,
% 86.61/86.68 (E(f3(f8(a4,a2),f8(a4,f5(a2,x3221))),f8(f5(a4,a4),f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[312,319,2,3])).
% 86.61/86.68 cnf(324,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(a1,a2)),f3(f8(a4,a2),f8(a4,f5(a2,x3241))))),
% 86.61/86.68 inference(scs_inference,[],[322,2])).
% 86.61/86.68 cnf(325,plain,
% 86.61/86.68 (E(f3(f8(a4,f8(a4,a1)),f8(a4,f8(a4,a2))),a2)),
% 86.61/86.68 inference(scs_inference,[],[321,287,322,2,3])).
% 86.61/86.68 cnf(327,plain,
% 86.61/86.68 (E(a2,f3(f8(a4,f8(a4,a1)),f8(a4,f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[325,2])).
% 86.61/86.68 cnf(328,plain,
% 86.61/86.68 (E(f8(a4,f8(x3281,x3282)),f8(f5(x3281,x3281),f3(x3282,x3282)))),
% 86.61/86.68 inference(scs_inference,[],[272,287,325,2,3])).
% 86.61/86.68 cnf(332,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(a1,a2)),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[321,282,328,2,3])).
% 86.61/86.68 cnf(333,plain,
% 86.61/86.68 (E(f3(a1,a2),f8(f5(a4,a4),f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[332,2])).
% 86.61/86.68 cnf(334,plain,
% 86.61/86.68 (E(a2,f8(a4,f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[315,332,32,2,3])).
% 86.61/86.68 cnf(336,plain,
% 86.61/86.68 (E(f8(a4,f3(a1,a2)),a2)),
% 86.61/86.68 inference(scs_inference,[],[334,2])).
% 86.61/86.68 cnf(337,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(a2,f3(a2,x3371))),f8(f5(a4,a4),f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[333,250,334,2,3])).
% 86.61/86.68 cnf(338,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(a1,a2)),f8(f5(a4,a4),f5(a2,f3(a2,x3381))))),
% 86.61/86.68 inference(scs_inference,[],[337,2])).
% 86.61/86.68 cnf(339,plain,
% 86.61/86.68 (E(f3(a1,a2),f3(f8(a4,a2),f8(a4,f5(a2,x3391))))),
% 86.61/86.68 inference(scs_inference,[],[324,333,337,2,3])).
% 86.61/86.68 cnf(340,plain,
% 86.61/86.68 (E(f3(f8(a4,a2),f8(a4,f5(a2,x3401))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[339,2])).
% 86.61/86.68 cnf(341,plain,
% 86.61/86.68 (E(f8(a4,f3(a1,a2)),f3(f8(a4,f8(a4,a1)),f8(a4,f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[336,327,339,2,3])).
% 86.61/86.68 cnf(343,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(a1,a2)),f5(f8(a4,a2),f8(a4,f3(a2,x3431))))),
% 86.61/86.68 inference(scs_inference,[],[338,246,341,2,3])).
% 86.61/86.68 cnf(345,plain,
% 86.61/86.68 (E(f5(f8(a4,a2),f8(a4,f3(a2,x3451))),f8(f5(a4,a4),f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[343,2])).
% 86.61/86.68 cnf(346,plain,
% 86.61/86.68 (E(f3(f8(a4,a2),f8(a4,f5(a2,x3461))),f3(f8(a4,a1),f8(a4,a2)))),
% 86.61/86.68 inference(scs_inference,[],[340,281,343,2,3])).
% 86.61/86.68 cnf(348,plain,
% 86.61/86.68 (E(f3(f8(a4,a1),f8(a4,a2)),f3(f8(a4,a2),f8(a4,f5(a2,x3481))))),
% 86.61/86.68 inference(scs_inference,[],[346,2])).
% 86.61/86.68 cnf(349,plain,
% 86.61/86.68 (E(f5(f8(a4,a2),f8(a4,f3(a2,x3491))),f3(f8(a4,a2),f8(a4,f5(a2,x3492))))),
% 86.61/86.68 inference(scs_inference,[],[345,324,346,2,3])).
% 86.61/86.68 cnf(350,plain,
% 86.61/86.68 (E(f3(f8(a4,a2),f8(a4,f5(a2,x3501))),f5(f8(a4,a2),f8(a4,f3(a2,x3502))))),
% 86.61/86.68 inference(scs_inference,[],[349,2])).
% 86.61/86.68 cnf(351,plain,
% 86.61/86.68 (E(f5(f8(a4,a2),f8(a4,f3(a2,x3511))),a2)),
% 86.61/86.68 inference(scs_inference,[],[345,321,349,2,3])).
% 86.61/86.68 cnf(352,plain,
% 86.61/86.68 (E(a2,f5(f8(a4,a2),f8(a4,f3(a2,x3521))))),
% 86.61/86.68 inference(scs_inference,[],[351,2])).
% 86.61/86.68 cnf(353,plain,
% 86.61/86.68 (E(f3(f8(a4,a1),f8(a4,a2)),f5(f8(a4,a2),f8(a4,f3(a2,x3531))))),
% 86.61/86.68 inference(scs_inference,[],[348,350,351,2,3])).
% 86.61/86.68 cnf(356,plain,
% 86.61/86.68 (E(f8(a4,f3(a1,a2)),f5(f8(a4,a2),f8(a4,f3(a2,x3561))))),
% 86.61/86.68 inference(scs_inference,[],[352,336,353,2,3])).
% 86.61/86.68 cnf(357,plain,
% 86.61/86.68 (E(f5(f8(a4,a2),f8(a4,f3(a2,x3571))),f8(a4,f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[356,2])).
% 86.61/86.68 cnf(358,plain,
% 86.61/86.68 (E(f5(f3(a1,a2),f3(f3(a1,a2),x3581)),f8(a4,f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[188,356,334,2,3])).
% 86.61/86.68 cnf(359,plain,
% 86.61/86.68 (E(f8(a4,f3(a1,a2)),f5(f3(a1,a2),f3(f3(a1,a2),x3591)))),
% 86.61/86.68 inference(scs_inference,[],[358,2])).
% 86.61/86.68 cnf(361,plain,
% 86.61/86.68 (E(f3(x3611,f3(x3612,x3613)),f3(f3(x3611,x3612),x3613))),
% 86.61/86.68 inference(scs_inference,[],[21,2])).
% 86.61/86.68 cnf(362,plain,
% 86.61/86.68 (E(f8(a4,f3(a1,a2)),f8(f5(a4,a4),f5(a2,f3(a2,x3621))))),
% 86.61/86.68 inference(scs_inference,[],[359,202,21,2,3])).
% 86.61/86.68 cnf(365,plain,
% 86.61/86.68 (E(a2,f3(f3(a1,a2),f5(f3(a1,a2),x3651)))),
% 86.61/86.68 inference(scs_inference,[],[361,222,362,2,3])).
% 86.61/86.68 cnf(367,plain,
% 86.61/86.68 (E(f3(f3(a1,a2),f5(f3(a1,a2),x3671)),a2)),
% 86.61/86.68 inference(scs_inference,[],[365,2])).
% 86.61/86.68 cnf(368,plain,
% 86.61/86.68 (E(f3(f8(a4,x3681),f3(f8(a4,x3682),f3(f8(a4,x3681),f8(a4,x3682)))),f3(x3681,x3682))),
% 86.61/86.68 inference(scs_inference,[],[361,58,365,2,3])).
% 86.61/86.68 cnf(371,plain,
% 86.61/86.68 (E(f3(f3(a1,a2),f5(f3(a1,a2),x3711)),f5(f8(a4,a2),f8(a4,f3(a2,x3712))))),
% 86.61/86.68 inference(scs_inference,[],[367,352,368,2,3])).
% 86.61/86.68 cnf(373,plain,
% 86.61/86.68 (E(f8(f7(x3731),x3731),f8(f5(a4,a4),f3(a4,f5(a4,x3732))))),
% 86.61/86.68 inference(scs_inference,[],[318,371,276,2,3])).
% 86.61/86.68 cnf(376,plain,
% 86.61/86.68 (E(f3(a1,a2),f3(f8(a4,f8(a4,a1)),f8(a4,f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[11,327,373,2,3])).
% 86.61/86.68 cnf(377,plain,
% 86.61/86.68 (E(f3(f8(a4,f8(a4,a1)),f8(a4,f8(a4,a2))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[376,2])).
% 86.61/86.68 cnf(378,plain,
% 86.61/86.68 (E(f3(a1,a2),f5(a2,f3(a2,x3781)))),
% 86.61/86.68 inference(scs_inference,[],[11,161,376,2,3])).
% 86.61/86.68 cnf(380,plain,
% 86.61/86.68 (E(f5(a2,f3(a2,x3801)),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[378,2])).
% 86.61/86.68 cnf(381,plain,
% 86.61/86.68 (E(f3(a1,a2),f3(a2,f5(a2,x3811)))),
% 86.61/86.68 inference(scs_inference,[],[11,199,378,2,3])).
% 86.61/86.68 cnf(383,plain,
% 86.61/86.68 (E(f3(a2,f5(a2,x3831)),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[381,2])).
% 86.61/86.68 cnf(384,plain,
% 86.61/86.68 (E(f3(a1,a2),f5(f8(a4,a2),f8(a4,f3(a2,x3841))))),
% 86.61/86.68 inference(scs_inference,[],[11,352,381,2,3])).
% 86.61/86.68 cnf(385,plain,
% 86.61/86.68 (E(f5(f8(a4,a2),f8(a4,f3(a2,x3851))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[384,2])).
% 86.61/86.68 cnf(386,plain,
% 86.61/86.68 (E(f3(a1,a2),f5(a2,a2))),
% 86.61/86.68 inference(scs_inference,[],[11,28,384,2,3])).
% 86.61/86.68 cnf(388,plain,
% 86.61/86.68 (E(f5(a2,a2),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[386,2])).
% 86.61/86.68 cnf(389,plain,
% 86.61/86.68 (E(f3(a1,a2),f3(a2,a2))),
% 86.61/86.68 inference(scs_inference,[],[11,272,386,2,3])).
% 86.61/86.68 cnf(391,plain,
% 86.61/86.68 (E(f3(a2,a2),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[389,2])).
% 86.61/86.68 cnf(392,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f8(a4,f8(f5(a4,a4),f8(a4,a2)))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[306,388,389,2,3])).
% 86.61/86.68 cnf(394,plain,
% 86.61/86.68 (E(f3(a1,a2),f8(f5(a4,a4),f8(a4,f8(f5(a4,a4),f8(a4,a2)))))),
% 86.61/86.68 inference(scs_inference,[],[392,2])).
% 86.61/86.68 cnf(395,plain,
% 86.61/86.68 (E(f3(a2,f3(a2,f5(f3(a2,a2),x3951))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[391,216,392,2,3])).
% 86.61/86.68 cnf(398,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(f8(a4,a1),f8(a4,a2))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[377,278,395,2,3])).
% 86.61/86.68 cnf(400,plain,
% 86.61/86.68 (E(f3(a1,a2),f8(f5(a4,a4),f3(f8(a4,a1),f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[398,2])).
% 86.61/86.68 cnf(401,plain,
% 86.61/86.68 (E(f8(f5(f5(f5(a4,a4),f5(a4,a4)),f5(f5(a4,a4),f5(a4,a4))),f5(a2,a2)),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[89,388,398,2,3])).
% 86.61/86.68 cnf(403,plain,
% 86.61/86.68 (E(f3(a1,a2),f8(f5(f5(f5(a4,a4),f5(a4,a4)),f5(f5(a4,a4),f5(a4,a4))),f5(a2,a2)))),
% 86.61/86.68 inference(scs_inference,[],[401,2])).
% 86.61/86.68 cnf(404,plain,
% 86.61/86.68 (E(f5(f8(a4,a2),f8(a4,f3(a2,x4041))),f8(f5(a4,a4),f3(f8(a4,a1),f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[400,385,401,2,3])).
% 86.61/86.68 cnf(405,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(f8(a4,a1),f8(a4,a2))),f5(f8(a4,a2),f8(a4,f3(a2,x4051))))),
% 86.61/86.68 inference(scs_inference,[],[404,2])).
% 86.61/86.68 cnf(406,plain,
% 86.61/86.68 (E(f5(a2,f3(a2,x4061)),f8(f5(f5(f5(a4,a4),f5(a4,a4)),f5(f5(a4,a4),f5(a4,a4))),f5(a2,a2)))),
% 86.61/86.68 inference(scs_inference,[],[403,380,404,2,3])).
% 86.61/86.68 cnf(408,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(f8(a4,a1),f8(a4,a2))),f8(a4,f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[357,405,406,2,3])).
% 86.61/86.68 cnf(410,plain,
% 86.61/86.68 (E(f8(a4,f3(a1,a2)),f8(f5(a4,a4),f3(f8(a4,a1),f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[408,2])).
% 86.61/86.68 cnf(411,plain,
% 86.61/86.68 (E(f3(a2,f5(a2,x4111)),f8(f5(a4,a4),f3(f8(a4,a1),f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[383,400,408,2,3])).
% 86.61/86.68 cnf(412,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(f8(a4,a1),f8(a4,a2))),f3(a2,f5(a2,x4121)))),
% 86.61/86.68 inference(scs_inference,[],[411,2])).
% 86.61/86.68 cnf(413,plain,
% 86.61/86.68 (E(f3(a1,a2),f8(f8(f5(a4,a4),a4),f8(f5(a4,a4),f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[394,235,411,2,3])).
% 86.61/86.68 cnf(415,plain,
% 86.61/86.68 (E(f8(f8(f5(a4,a4),a4),f8(f5(a4,a4),f8(a4,a2))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[413,2])).
% 86.61/86.68 cnf(416,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(a1,a2)),f3(a2,f5(a2,x4161)))),
% 86.61/86.68 inference(scs_inference,[],[294,412,413,2,3])).
% 86.61/86.68 cnf(418,plain,
% 86.61/86.68 (E(f3(a2,f5(a2,x4181)),f8(f5(a4,a4),f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[416,2])).
% 86.61/86.68 cnf(419,plain,
% 86.61/86.68 (E(f8(f8(f5(a4,a4),a4),f8(f5(a4,a4),f8(a4,a2))),a2)),
% 86.61/86.68 inference(scs_inference,[],[11,415,416,2,3])).
% 86.61/86.68 cnf(421,plain,
% 86.61/86.68 (E(f3(a2,f5(a2,x4211)),f8(f5(a4,a4),f5(a2,f3(a2,x4212))))),
% 86.61/86.68 inference(scs_inference,[],[418,338,419,2,3])).
% 86.61/86.68 cnf(422,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(a2,f3(a2,x4221))),f3(a2,f5(a2,x4222)))),
% 86.61/86.68 inference(scs_inference,[],[421,2])).
% 86.61/86.68 cnf(423,plain,
% 86.61/86.68 (E(f8(a4,f3(a1,a2)),f3(a2,f5(a2,x4231)))),
% 86.61/86.68 inference(scs_inference,[],[410,412,421,2,3])).
% 86.61/86.68 cnf(425,plain,
% 86.61/86.68 (E(f8(f8(f5(a4,a4),a4),f8(f5(a4,a4),f8(a4,a2))),f8(f5(a4,a4),f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[415,333,423,2,3])).
% 86.61/86.68 cnf(426,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(a1,a2)),f8(f8(f5(a4,a4),a4),f8(f5(a4,a4),f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[425,2])).
% 86.61/86.68 cnf(427,plain,
% 86.61/86.68 (E(f3(a2,f5(a2,x4271)),f3(f8(a4,a2),f8(a4,f5(a2,x4272))))),
% 86.61/86.68 inference(scs_inference,[],[418,324,425,2,3])).
% 86.61/86.68 cnf(428,plain,
% 86.61/86.68 (E(f3(f8(a4,a2),f8(a4,f5(a2,x4281))),f3(a2,f5(a2,x4282)))),
% 86.61/86.68 inference(scs_inference,[],[427,2])).
% 86.61/86.68 cnf(429,plain,
% 86.61/86.68 (E(f5(f5(f5(f8(a4,a2),f8(a4,a2)),f8(a4,a2)),f8(a4,a2)),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[182,388,427,2,3])).
% 86.61/86.68 cnf(431,plain,
% 86.61/86.68 (E(f3(a1,a2),f5(f5(f5(f8(a4,a2),f8(a4,a2)),f8(a4,a2)),f8(a4,a2)))),
% 86.61/86.68 inference(scs_inference,[],[429,2])).
% 86.61/86.68 cnf(432,plain,
% 86.61/86.68 (E(f3(f8(a4,a1),f8(a4,a2)),f3(a2,f5(a2,x4321)))),
% 86.61/86.68 inference(scs_inference,[],[428,348,429,2,3])).
% 86.61/86.68 cnf(434,plain,
% 86.61/86.68 (E(f3(a2,f5(a2,x4341)),f3(f8(a4,a1),f8(a4,a2)))),
% 86.61/86.68 inference(scs_inference,[],[432,2])).
% 86.61/86.68 cnf(435,plain,
% 86.61/86.68 (E(f3(a1,a2),f8(f5(a4,a4),f5(a2,a2)))),
% 86.61/86.68 inference(scs_inference,[],[431,185,432,2,3])).
% 86.61/86.68 cnf(437,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(a2,a2)),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[435,2])).
% 86.61/86.68 cnf(438,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(a2,f3(a2,x4381))),f3(f8(a4,a1),f8(a4,a2)))),
% 86.61/86.68 inference(scs_inference,[],[434,422,435,2,3])).
% 86.61/86.68 cnf(440,plain,
% 86.61/86.68 (E(f3(f8(a4,a1),f8(a4,a2)),f8(f5(a4,a4),f5(a2,f3(a2,x4401))))),
% 86.61/86.68 inference(scs_inference,[],[438,2])).
% 86.61/86.68 cnf(441,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(a2,a2)),a2)),
% 86.61/86.68 inference(scs_inference,[],[11,437,438,2,3])).
% 86.61/86.68 cnf(442,plain,
% 86.61/86.68 (E(a2,f8(f5(a4,a4),f5(a2,a2)))),
% 86.61/86.68 inference(scs_inference,[],[441,2])).
% 86.61/86.68 cnf(443,plain,
% 86.61/86.68 (E(f5(f8(a4,f8(a4,a2)),f8(a4,f8(a4,a2))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[437,86,441,2,3])).
% 86.61/86.68 cnf(445,plain,
% 86.61/86.68 (E(f3(a1,a2),f5(f8(a4,f8(a4,a2)),f8(a4,f8(a4,a2))))),
% 86.61/86.68 inference(scs_inference,[],[443,2])).
% 86.61/86.68 cnf(446,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f3(a1,a2)),f8(f8(f8(f5(a4,a4),a4),f5(a4,a4)),f8(a4,a2)))),
% 86.61/86.68 inference(scs_inference,[],[426,235,443,2,3])).
% 86.61/86.68 cnf(448,plain,
% 86.61/86.68 (E(f8(f8(f8(f5(a4,a4),a4),f5(a4,a4)),f8(a4,a2)),f8(f5(a4,a4),f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[446,2])).
% 86.61/86.68 cnf(449,plain,
% 86.61/86.68 (E(f3(a1,a2),f8(f5(a4,a4),f8(a4,f8(a4,f8(a4,a2)))))),
% 86.61/86.68 inference(scs_inference,[],[445,298,446,2,3])).
% 86.61/86.68 cnf(451,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f8(a4,f8(a4,f8(a4,a2)))),f3(a1,a2))),
% 86.61/86.68 inference(scs_inference,[],[449,2])).
% 86.61/86.68 cnf(452,plain,
% 86.61/86.68 (E(f8(f8(f8(f5(a4,a4),a4),f5(a4,a4)),f8(a4,a2)),f8(f5(a4,a4),f5(a2,f3(a2,x4521))))),
% 86.61/86.68 inference(scs_inference,[],[448,338,449,2,3])).
% 86.61/86.68 cnf(453,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f5(a2,f3(a2,x4531))),f8(f8(f8(f5(a4,a4),a4),f5(a4,a4)),f8(a4,a2)))),
% 86.61/86.68 inference(scs_inference,[],[452,2])).
% 86.61/86.68 cnf(454,plain,
% 86.61/86.68 (E(f8(f5(a4,a4),f8(a4,f8(a4,f8(a4,a2)))),a2)),
% 86.61/86.68 inference(scs_inference,[],[11,451,452,2,3])).
% 86.61/86.68 cnf(456,plain,
% 86.61/86.68 (E(f3(f8(a4,a1),f8(a4,a2)),f8(f8(f8(f5(a4,a4),a4),f5(a4,a4)),f8(a4,a2)))),
% 86.61/86.68 inference(scs_inference,[],[440,453,454,2,3])).
% 86.61/86.68 cnf(458,plain,
% 86.61/86.68 (E(f8(f8(f8(f5(a4,a4),a4),f5(a4,a4)),f8(a4,a2)),f3(f8(a4,a1),f8(a4,a2)))),
% 86.61/86.68 inference(scs_inference,[],[456,2])).
% 86.61/86.68 cnf(459,plain,
% 86.61/86.68 (E(a2,f8(a4,f5(f5(a2,a2),f5(a2,a2))))),
% 86.61/86.68 inference(scs_inference,[],[302,442,456,2,3])).
% 86.61/86.68 cnf(462,plain,
% 86.61/86.68 (E(f8(f8(f8(f5(a4,a4),a4),f5(a4,a4)),f8(a4,a2)),f3(f8(a4,a2),f8(a4,f5(a2,x4621))))),
% 86.61/86.68 inference(scs_inference,[],[458,348,459,2,3])).
% 86.61/86.68 cnf(464,plain,
% 86.61/86.68 (E(f8(f3(a4,a4),f8(x4641,x4642)),f8(f5(x4641,x4641),f3(x4642,x4642)))),
% 86.61/86.68 inference(scs_inference,[],[143,287,462,2,3])).
% 86.61/86.68 cnf(468,plain,
% 86.61/86.68 (E(f3(a1,a2),f8(a4,a2))),
% 86.61/86.68 inference(scs_inference,[],[11,44,464,2,3])).
% 86.61/86.68 cnf(1262,plain,
% 86.61/86.68 (E(f5(x12621,x12621),f3(x12621,x12621))),
% 86.61/86.68 inference(scs_inference,[],[13,272,3])).
% 86.61/86.68 cnf(1344,plain,
% 86.61/86.68 (~E(f8(f7(a6),f8(a2,a6)),f3(f8(f7(a6),f8(a1,a6)),f8(f7(a6),f8(a2,a6))))),
% 86.61/86.68 inference(scs_inference,[],[27,1262,10,4,5,6,7,8,9,2])).
% 86.61/86.68 cnf(1743,plain,
% 86.61/86.68 (E(f8(a2,x17431),f8(f3(a1,a2),x17431))),
% 86.61/86.68 inference(scs_inference,[],[282,7,6])).
% 86.61/86.68 cnf(1744,plain,
% 86.61/86.68 (E(f3(x17441,a2),f3(x17441,f3(a1,a2)))),
% 86.61/86.68 inference(scs_inference,[],[282,7,6,5])).
% 86.61/86.68 cnf(1756,plain,
% 86.61/86.68 (E(f8(x17561,f8(a2,x17562)),f8(x17561,f8(f3(a1,a2),x17562)))),
% 86.61/86.68 inference(scs_inference,[],[1743,7])).
% 86.61/86.68 cnf(1773,plain,
% 86.61/86.68 (~E(f8(f7(a6),f8(f3(a1,a2),a6)),f3(f8(f7(a6),f8(a1,a6)),f8(f7(a6),f8(a2,a6))))),
% 86.61/86.68 inference(scs_inference,[],[1744,1756,1344,7,5,6,4,10,8,9,3])).
% 86.61/86.68 cnf(1923,plain,
% 86.61/86.68 (E(f8(f3(a1,a2),x19231),f8(f8(a4,a2),x19231))),
% 86.61/86.68 inference(scs_inference,[],[468,7,6])).
% 86.61/86.68 cnf(1924,plain,
% 86.61/86.68 (E(f3(x19241,f3(a1,a2)),f3(x19241,f8(a4,a2)))),
% 86.61/86.68 inference(scs_inference,[],[468,7,6,5])).
% 86.61/86.68 cnf(1936,plain,
% 86.61/86.68 (E(f8(x19361,f8(f3(a1,a2),x19362)),f8(x19361,f8(f8(a4,a2),x19362)))),
% 86.61/86.68 inference(scs_inference,[],[1923,7])).
% 86.61/86.68 cnf(1955,plain,
% 86.61/86.68 (~E(f3(f8(f7(a6),f8(a1,a6)),f8(f7(a6),f8(a2,a6))),f8(f7(a6),f8(f8(a4,a2),a6)))),
% 86.61/86.68 inference(scs_inference,[],[1924,1936,1773,7,5,6,4,10,8,9,3,2])).
% 86.61/86.68 cnf(2222,plain,
% 86.61/86.68 (E(f8(f3(a1,a2),x22221),f8(a2,x22221))),
% 86.61/86.68 inference(scs_inference,[],[11,5,10,6])).
% 86.61/86.68 cnf(2305,plain,
% 86.61/86.68 (E(f8(f8(a4,x23051),x23052),f8(x23051,x23052))),
% 86.61/86.68 inference(scs_inference,[],[12,9,8,5,6])).
% 86.61/86.68 cnf(2337,plain,
% 86.61/86.68 (E(f8(x23371,f8(f8(a4,x23372),x23373)),f8(x23371,f8(x23372,x23373)))),
% 86.61/86.68 inference(scs_inference,[],[2305,9,8,5,10,6,7])).
% 86.61/86.68 cnf(2500,plain,
% 86.61/86.68 (E(f7(f3(x25001,f5(x25001,x25002))),f7(x25001))),
% 86.61/86.68 inference(scs_inference,[],[19,6,7,4,9,8,5,10])).
% 86.61/86.68 cnf(2561,plain,
% 86.61/86.68 (~E(f8(f7(a6),f8(f8(a4,a2),a6)),f8(f7(a6),f3(f8(a1,a6),f8(a2,a6))))),
% 86.61/86.68 inference(scs_inference,[],[24,1955,3,7,2])).
% 86.61/86.68 cnf(2623,plain,
% 86.61/86.68 (~E(f8(a2,a6),f3(f8(a1,a6),f8(a2,a6)))),
% 86.61/86.68 inference(scs_inference,[],[2500,2337,2561,6,3,2,7])).
% 86.61/86.68 cnf(2624,plain,
% 86.61/86.68 (~E(f3(f8(a1,a6),f8(a2,a6)),f8(a2,a6))),
% 86.61/86.68 inference(scs_inference,[],[2623,2])).
% 86.61/86.68 cnf(2629,plain,
% 86.61/86.68 ($false),
% 86.61/86.68 inference(scs_inference,[],[2624,26,2222,3]),
% 86.61/86.68 ['proof']).
% 86.61/86.68 % SZS output end Proof
% 86.61/86.68 % Total time :86.040000s
%------------------------------------------------------------------------------