%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG003-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n003.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 14:00:34 EDT 2024
% Result : Unsatisfiable 59.35s 59.41s
% Output : CNFRefutation 59.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : RNG003-1 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n003.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 : Tue Jun 18 13:31:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.53/0.56 start to proof:theBenchmark
% 59.35/59.40 %-------------------------------------------
% 59.35/59.40 % File :CSE---1.7
% 59.35/59.40 % Problem :theBenchmark
% 59.35/59.40 % Transform :cnf
% 59.35/59.40 % Format :tptp:raw
% 59.35/59.40 % Command :java -jar mcs_scs.jar %d %s
% 59.35/59.40
% 59.35/59.40 % Result :Theorem 58.810000s
% 59.35/59.40 % Output :CNFRefutation 58.810000s
% 59.35/59.40 %-------------------------------------------
% 59.35/59.41 %--------------------------------------------------------------------------
% 59.35/59.41 % File : RNG003-1 : TPTP v8.2.0. Released v1.0.0.
% 59.35/59.41 % Domain : Ring Theory
% 59.35/59.41 % Problem : Left cancellation for addition
% 59.35/59.41 % Version : [MOW76] axioms.
% 59.35/59.41 % English :
% 59.35/59.41
% 59.35/59.41 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 59.35/59.41 % : [OMW76] Overbeek et al. (1976), Complexity and Related Enhance
% 59.35/59.41 % Source : [MOW76]
% 59.35/59.41 % Names : Established lemma [MOW76]
% 59.35/59.41 % : Lemma proved [OMW76]
% 59.35/59.41
% 59.35/59.41 % Status : Unsatisfiable
% 59.35/59.41 % Rating : 0.00 v7.5.0, 0.10 v7.4.0, 0.11 v7.3.0, 0.00 v6.0.0, 0.11 v5.5.0, 0.12 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.00 v2.0.0
% 59.35/59.41 % Syntax : Number of clauses : 20 ( 9 unt; 0 nHn; 14 RR)
% 59.35/59.41 % Number of literals : 53 ( 3 equ; 34 neg)
% 59.35/59.41 % Maximal clause size : 5 ( 2 avg)
% 59.35/59.41 % Maximal term depth : 2 ( 1 avg)
% 59.35/59.41 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 59.35/59.41 % Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% 59.35/59.41 % Number of variables : 71 ( 0 sgn)
% 59.35/59.41 % SPC : CNF_UNS_RFO_SEQ_HRN
% 59.35/59.41
% 59.35/59.41 % Comments :
% 59.35/59.41 %--------------------------------------------------------------------------
% 59.35/59.41 %----Include ring theory axioms
% 59.35/59.41 include('Axioms/RNG001-0.ax').
% 59.35/59.41 %--------------------------------------------------------------------------
% 59.35/59.41 cnf(a_plus_c_is_d,hypothesis,
% 59.35/59.41 sum(a,c,d) ).
% 59.35/59.41
% 59.35/59.41 cnf(b_plus_c_is_d,hypothesis,
% 59.35/59.41 sum(b,c,d) ).
% 59.35/59.41
% 59.35/59.41 cnf(prove_a_equals_b,negated_conjecture,
% 59.35/59.41 a != b ).
% 59.35/59.41
% 59.35/59.41 %--------------------------------------------------------------------------
% 59.35/59.41 %-------------------------------------------
% 59.35/59.41 % Proof found
% 59.35/59.41 % SZS status Theorem for theBenchmark
% 59.35/59.41 % SZS output start Proof
% 59.35/59.41 %ClaNum:34(EqnAxiom:14)
% 59.35/59.41 %VarNum:146(SingletonVarNum:71)
% 59.35/59.41 %MaxLitNum:5
% 59.35/59.41 %MaxfuncDepth:1
% 59.35/59.41 %SharedTerms:8
% 59.35/59.41 %goalClause: 23
% 59.35/59.41 %singleGoalClaCount:1
% 59.35/59.41 [15]P1(a1,a2,a7)
% 59.35/59.41 [16]P1(a3,a2,a7)
% 59.35/59.41 [23]~E(a3,a1)
% 59.35/59.41 [17]P1(x171,a4,x171)
% 59.35/59.41 [18]P1(a4,x181,x181)
% 59.35/59.41 [19]P1(x191,f6(x191),a4)
% 59.35/59.41 [20]P1(f6(x201),x201,a4)
% 59.35/59.41 [21]P1(x211,x212,f5(x211,x212))
% 59.35/59.41 [22]P2(x221,x222,f8(x221,x222))
% 59.35/59.41 [24]~P1(x242,x241,x243)+P1(x241,x242,x243)
% 59.35/59.41 [25]~P1(x253,x254,x251)+E(x251,x252)+~P1(x253,x254,x252)
% 59.35/59.41 [26]~P2(x263,x264,x261)+E(x261,x262)+~P2(x263,x264,x262)
% 59.35/59.41 [27]~P1(x276,x274,x271)+P1(x271,x272,x273)+~P1(x274,x272,x275)+~P1(x276,x275,x273)
% 59.35/59.41 [28]~P1(x281,x286,x284)+P1(x281,x282,x283)+~P1(x284,x285,x283)+~P1(x286,x285,x282)
% 59.35/59.41 [29]~P2(x296,x294,x291)+P2(x291,x292,x293)+~P2(x294,x292,x295)+~P2(x296,x295,x293)
% 59.35/59.41 [30]~P2(x301,x306,x304)+P2(x301,x302,x303)+~P2(x304,x305,x303)+~P2(x306,x305,x302)
% 59.35/59.41 [31]~P2(x317,x315,x312)+~P2(x317,x314,x311)+P1(x311,x312,x313)+~P1(x314,x315,x316)+~P2(x317,x316,x313)
% 59.35/59.41 [32]~P2(x325,x327,x322)+~P2(x324,x327,x321)+P1(x321,x322,x323)+~P1(x324,x325,x326)+~P2(x326,x327,x323)
% 59.35/59.41 [33]~P2(x337,x332,x335)+~P2(x336,x332,x334)+P2(x331,x332,x333)+~P1(x334,x335,x333)+~P1(x336,x337,x331)
% 59.35/59.41 [34]~P2(x341,x347,x345)+~P2(x341,x346,x344)+P2(x341,x342,x343)+~P1(x344,x345,x343)+~P1(x346,x347,x342)
% 59.35/59.41 %EqnAxiom
% 59.35/59.41 [1]E(x11,x11)
% 59.35/59.41 [2]E(x22,x21)+~E(x21,x22)
% 59.35/59.41 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.35/59.41 [4]~E(x41,x42)+E(f6(x41),f6(x42))
% 59.35/59.41 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53))
% 59.35/59.41 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62))
% 59.35/59.41 [7]~E(x71,x72)+E(f5(x71,x73),f5(x72,x73))
% 59.35/59.41 [8]~E(x81,x82)+E(f5(x83,x81),f5(x83,x82))
% 59.35/59.41 [9]P1(x92,x93,x94)+~E(x91,x92)+~P1(x91,x93,x94)
% 59.35/59.41 [10]P1(x103,x102,x104)+~E(x101,x102)+~P1(x103,x101,x104)
% 59.35/59.41 [11]P1(x113,x114,x112)+~E(x111,x112)+~P1(x113,x114,x111)
% 59.35/59.41 [12]P2(x122,x123,x124)+~E(x121,x122)+~P2(x121,x123,x124)
% 59.35/59.41 [13]P2(x133,x132,x134)+~E(x131,x132)+~P2(x133,x131,x134)
% 59.35/59.41 [14]P2(x143,x144,x142)+~E(x141,x142)+~P2(x143,x144,x141)
% 59.35/59.41
% 59.35/59.41 %-------------------------------------------
% 59.41/59.42 cnf(35,plain,
% 59.41/59.42 (E(x351,f5(x351,a4))),
% 59.41/59.42 inference(scs_inference,[],[17,21,25])).
% 59.41/59.42 cnf(36,plain,
% 59.41/59.42 (P1(x361,x362,f5(x361,x362))),
% 59.41/59.42 inference(rename_variables,[],[21])).
% 59.41/59.42 cnf(38,plain,
% 59.41/59.42 (P1(f5(x381,a4),a4,x381)),
% 59.41/59.42 inference(scs_inference,[],[17,21,25,9])).
% 59.41/59.42 cnf(40,plain,
% 59.41/59.42 (P1(x401,a4,x401)),
% 59.41/59.42 inference(rename_variables,[],[17])).
% 59.41/59.42 cnf(41,plain,
% 59.41/59.42 (P1(x411,f6(x411),f5(a4,a4))),
% 59.41/59.42 inference(scs_inference,[],[17,21,19,25,9,10,11])).
% 59.41/59.42 cnf(42,plain,
% 59.41/59.42 (P2(f5(a4,a4),x421,f8(a4,x421))),
% 59.41/59.42 inference(scs_inference,[],[17,21,22,19,25,9,10,11,12])).
% 59.41/59.42 cnf(43,plain,
% 59.41/59.42 (P2(x431,x432,f8(x431,x432))),
% 59.41/59.42 inference(rename_variables,[],[22])).
% 59.41/59.42 cnf(44,plain,
% 59.41/59.42 (P2(x441,f5(a4,a4),f8(x441,a4))),
% 59.41/59.42 inference(scs_inference,[],[17,21,22,43,19,25,9,10,11,12,13])).
% 59.41/59.42 cnf(45,plain,
% 59.41/59.42 (P2(x451,x452,f8(x451,x452))),
% 59.41/59.42 inference(rename_variables,[],[22])).
% 59.41/59.42 cnf(46,plain,
% 59.41/59.42 (P1(x461,f5(a4,a4),x461)),
% 59.41/59.42 inference(scs_inference,[],[17,40,21,36,22,43,19,25,9,10,11,12,13,28])).
% 59.41/59.42 cnf(47,plain,
% 59.41/59.42 (P1(x471,x472,f5(x471,x472))),
% 59.41/59.42 inference(rename_variables,[],[21])).
% 59.41/59.42 cnf(49,plain,
% 59.41/59.42 (P1(f8(x491,a4),f8(x491,a4),f8(x491,a4))),
% 59.41/59.42 inference(scs_inference,[],[17,40,21,36,22,43,45,19,25,9,10,11,12,13,28,31])).
% 59.41/59.42 cnf(52,plain,
% 59.41/59.42 (P2(x521,x522,f8(x521,x522))),
% 59.41/59.42 inference(rename_variables,[],[22])).
% 59.41/59.42 cnf(53,plain,
% 59.41/59.42 (P1(x531,a4,x531)),
% 59.41/59.42 inference(rename_variables,[],[17])).
% 59.41/59.42 cnf(55,plain,
% 59.41/59.42 (P1(f8(a4,x551),f8(a4,x551),f8(a4,x551))),
% 59.41/59.42 inference(scs_inference,[],[17,40,53,21,36,22,43,45,52,19,25,9,10,11,12,13,28,31,32])).
% 59.41/59.42 cnf(58,plain,
% 59.41/59.42 (P2(x581,x582,f8(x581,x582))),
% 59.41/59.42 inference(rename_variables,[],[22])).
% 59.41/59.42 cnf(59,plain,
% 59.41/59.42 (P1(x591,a4,x591)),
% 59.41/59.42 inference(rename_variables,[],[17])).
% 59.41/59.42 cnf(61,plain,
% 59.41/59.42 (P2(a4,x611,f5(f8(a4,x611),f8(a4,x611)))),
% 59.41/59.42 inference(scs_inference,[],[17,40,53,59,21,36,47,22,43,45,52,58,19,25,9,10,11,12,13,28,31,32,33])).
% 59.41/59.42 cnf(62,plain,
% 59.41/59.42 (P1(x621,x622,f5(x621,x622))),
% 59.41/59.42 inference(rename_variables,[],[21])).
% 59.41/59.42 cnf(63,plain,
% 59.41/59.42 (P1(x631,a4,x631)),
% 59.41/59.42 inference(rename_variables,[],[17])).
% 59.41/59.42 cnf(65,plain,
% 59.41/59.42 (P2(x651,x652,f8(x651,x652))),
% 59.41/59.42 inference(rename_variables,[],[22])).
% 59.41/59.42 cnf(67,plain,
% 59.41/59.42 (P2(x671,a4,f5(f8(x671,a4),f8(x671,a4)))),
% 59.41/59.42 inference(scs_inference,[],[17,40,53,59,63,21,36,47,62,22,43,45,52,58,65,19,25,9,10,11,12,13,28,31,32,33,34])).
% 59.41/59.42 cnf(70,plain,
% 59.41/59.42 (P2(x701,x702,f8(x701,x702))),
% 59.41/59.42 inference(rename_variables,[],[22])).
% 59.41/59.43 cnf(71,plain,
% 59.41/59.43 (P2(x711,x712,f8(x711,x712))),
% 59.41/59.43 inference(rename_variables,[],[22])).
% 59.41/59.43 cnf(74,plain,
% 59.41/59.43 (E(f8(f5(a4,a4),x741),f8(a4,x741))),
% 59.41/59.43 inference(scs_inference,[],[17,40,53,59,63,21,36,47,62,22,43,45,52,58,65,71,19,25,9,10,11,12,13,28,31,32,33,34,2,26])).
% 59.41/59.43 cnf(75,plain,
% 59.41/59.43 (P2(x751,x752,f8(x751,x752))),
% 59.41/59.43 inference(rename_variables,[],[22])).
% 59.41/59.43 cnf(78,plain,
% 59.41/59.43 (P2(f5(a4,a4),f5(a4,a4),f8(a4,a4))),
% 59.41/59.43 inference(scs_inference,[],[17,40,53,59,63,21,36,47,62,22,43,45,52,58,65,71,19,25,9,10,11,12,13,28,31,32,33,34,2,26,3,14])).
% 59.41/59.43 cnf(79,plain,
% 59.41/59.43 (P2(f8(x791,x791),x791,f8(x791,f8(x791,x791)))),
% 59.41/59.43 inference(scs_inference,[],[17,40,53,59,63,21,36,47,62,22,43,45,52,58,65,71,75,70,19,25,9,10,11,12,13,28,31,32,33,34,2,26,3,14,29])).
% 59.41/59.43 cnf(81,plain,
% 59.41/59.43 (P2(x811,x812,f8(x811,x812))),
% 59.41/59.43 inference(rename_variables,[],[22])).
% 59.41/59.43 cnf(82,plain,
% 59.41/59.43 (P2(x821,x822,f8(x821,x822))),
% 59.41/59.43 inference(rename_variables,[],[22])).
% 59.41/59.43 cnf(84,plain,
% 59.41/59.43 (P2(x841,f8(x841,x841),f8(f8(x841,x841),x841))),
% 59.41/59.43 inference(scs_inference,[],[17,40,53,59,63,21,36,47,62,22,43,45,52,58,65,71,75,82,81,70,19,25,9,10,11,12,13,28,31,32,33,34,2,26,3,14,29,30])).
% 59.41/59.43 cnf(90,plain,
% 59.41/59.43 (E(f5(x901,a4),x901)),
% 59.41/59.43 inference(scs_inference,[],[35,2])).
% 59.41/59.43 cnf(91,plain,
% 59.41/59.43 (E(f6(a4),a4)),
% 59.41/59.43 inference(scs_inference,[],[35,18,19,2,25])).
% 59.41/59.43 cnf(93,plain,
% 59.41/59.43 (P1(a4,x931,x931)),
% 59.41/59.43 inference(rename_variables,[],[18])).
% 59.41/59.43 cnf(95,plain,
% 59.41/59.43 (P1(f5(a4,a4),x951,x951)),
% 59.41/59.43 inference(scs_inference,[],[35,18,93,19,2,25,9])).
% 59.41/59.43 cnf(96,plain,
% 59.41/59.43 (E(x961,f5(x961,a4))),
% 59.41/59.43 inference(rename_variables,[],[35])).
% 59.41/59.43 cnf(97,plain,
% 59.41/59.43 (P1(a4,x971,f5(x971,a4))),
% 59.41/59.43 inference(scs_inference,[],[35,96,18,93,19,2,25,9,11])).
% 59.41/59.43 cnf(98,plain,
% 59.41/59.43 (P1(a4,x981,x981)),
% 59.41/59.43 inference(rename_variables,[],[18])).
% 59.41/59.43 cnf(103,plain,
% 59.41/59.43 (P1(a4,f5(x1031,a4),x1031)),
% 59.41/59.43 inference(scs_inference,[],[35,96,18,93,98,19,79,84,2,25,9,11,12,13,10])).
% 59.41/59.43 cnf(105,plain,
% 59.41/59.43 (P2(x1051,f5(a4,a4),f5(f8(x1051,a4),a4))),
% 59.41/59.43 inference(scs_inference,[],[35,96,18,93,98,19,79,84,44,2,25,9,11,12,13,10,14])).
% 59.41/59.43 cnf(135,plain,
% 59.41/59.43 (E(f8(a4,a4),f8(a4,f5(a4,a4)))),
% 59.41/59.43 inference(scs_inference,[],[74,78,42,2,26])).
% 59.41/59.43 cnf(138,plain,
% 59.41/59.43 (E(a4,f6(f5(a4,a4)))),
% 59.41/59.43 inference(scs_inference,[],[74,78,19,95,42,2,26,25])).
% 59.41/59.43 cnf(139,plain,
% 59.41/59.43 (P1(f5(a4,a4),x1391,x1391)),
% 59.41/59.43 inference(rename_variables,[],[95])).
% 59.41/59.43 cnf(142,plain,
% 59.41/59.43 (P1(a1,a2,f5(a7,a4))),
% 59.41/59.43 inference(scs_inference,[],[74,35,15,78,19,95,42,2,26,25,11])).
% 59.41/59.43 cnf(143,plain,
% 59.41/59.43 (E(x1431,f5(x1431,a4))),
% 59.41/59.43 inference(rename_variables,[],[35])).
% 59.41/59.43 cnf(144,plain,
% 59.41/59.43 (P1(f5(a1,a4),a2,a7)),
% 59.41/59.43 inference(scs_inference,[],[74,35,143,15,78,19,95,42,2,26,25,11,9])).
% 59.41/59.43 cnf(145,plain,
% 59.41/59.43 (E(x1451,f5(x1451,a4))),
% 59.41/59.43 inference(rename_variables,[],[35])).
% 59.41/59.43 cnf(146,plain,
% 59.41/59.43 (~E(a3,f5(a1,a4))),
% 59.41/59.43 inference(scs_inference,[],[23,74,90,35,143,15,78,19,95,42,2,26,25,11,9,3])).
% 59.41/59.43 cnf(147,plain,
% 59.41/59.43 (E(f5(x1471,a4),x1471)),
% 59.41/59.43 inference(rename_variables,[],[90])).
% 59.41/59.43 cnf(149,plain,
% 59.41/59.43 (E(x1491,f5(x1491,a4))),
% 59.41/59.43 inference(rename_variables,[],[35])).
% 59.41/59.43 cnf(152,plain,
% 59.41/59.43 (P2(f5(a4,a4),f5(a4,a4),f5(f8(a4,a4),a4))),
% 59.41/59.43 inference(scs_inference,[],[23,74,90,147,35,143,145,149,15,78,19,95,42,105,61,2,26,25,11,9,3,12,13,14])).
% 59.41/59.43 cnf(153,plain,
% 59.41/59.43 (E(x1531,f5(x1531,a4))),
% 59.41/59.43 inference(rename_variables,[],[35])).
% 59.41/59.43 cnf(154,plain,
% 59.41/59.43 (P1(a1,f5(a2,a4),a7)),
% 59.41/59.43 inference(scs_inference,[],[23,74,90,147,35,143,145,149,153,15,78,19,95,42,105,61,2,26,25,11,9,3,12,13,14,10])).
% 59.41/59.43 cnf(156,plain,
% 59.41/59.43 (P1(f5(a4,a4),f5(x1561,a4),x1561)),
% 59.41/59.43 inference(scs_inference,[],[23,74,90,147,35,143,145,149,153,15,78,18,19,95,139,42,105,61,103,2,26,25,11,9,3,12,13,14,10,27])).
% 59.41/59.43 cnf(160,plain,
% 59.41/59.43 (P2(f8(a4,a4),f5(a4,a4),f8(f5(a4,a4),f8(a4,a4)))),
% 59.41/59.43 inference(scs_inference,[],[23,74,90,147,35,143,145,149,153,15,78,18,19,95,139,42,105,61,103,22,2,26,25,11,9,3,12,13,14,10,27,29])).
% 59.41/59.43 cnf(180,plain,
% 59.41/59.43 (E(f8(a4,f5(a4,a4)),f8(a4,a4))),
% 59.41/59.43 inference(scs_inference,[],[135,2])).
% 59.41/59.43 cnf(181,plain,
% 59.41/59.43 (E(f8(a4,a4),f8(f5(a4,a4),f5(a4,a4)))),
% 59.41/59.43 inference(scs_inference,[],[135,78,22,2,26])).
% 59.41/59.43 cnf(184,plain,
% 59.41/59.43 (E(f6(a4),f5(a4,a4))),
% 59.41/59.43 inference(scs_inference,[],[135,78,18,41,22,2,26,25])).
% 59.41/59.43 cnf(185,plain,
% 59.41/59.43 (P1(x1851,f6(x1851),f5(a4,a4))),
% 59.41/59.43 inference(rename_variables,[],[41])).
% 59.41/59.43 cnf(186,plain,
% 59.41/59.43 (P1(a4,x1861,x1861)),
% 59.41/59.43 inference(rename_variables,[],[18])).
% 59.41/59.43 cnf(188,plain,
% 59.41/59.43 (P1(a3,a2,f5(a7,a4))),
% 59.41/59.43 inference(scs_inference,[],[135,35,78,16,18,41,22,2,26,25,11])).
% 59.41/59.43 cnf(189,plain,
% 59.41/59.43 (E(x1891,f5(x1891,a4))),
% 59.41/59.43 inference(rename_variables,[],[35])).
% 59.41/59.43 cnf(190,plain,
% 59.41/59.43 (P1(f5(a3,a4),a2,a7)),
% 59.41/59.43 inference(scs_inference,[],[135,35,189,78,16,18,41,22,2,26,25,11,9])).
% 59.41/59.43 cnf(191,plain,
% 59.41/59.43 (E(x1911,f5(x1911,a4))),
% 59.41/59.43 inference(rename_variables,[],[35])).
% 59.41/59.43 cnf(193,plain,
% 59.41/59.43 (E(f5(x1931,a4),x1931)),
% 59.41/59.43 inference(rename_variables,[],[90])).
% 59.41/59.43 cnf(194,plain,
% 59.41/59.43 (P2(f8(a4,a4),a4,f8(f5(a4,a4),f8(a4,a4)))),
% 59.41/59.43 inference(scs_inference,[],[135,91,90,193,35,189,78,16,18,160,41,22,2,26,25,11,9,3,13])).
% 59.41/59.43 cnf(196,plain,
% 59.41/59.43 (P1(a3,f5(a2,a4),a7)),
% 59.41/59.43 inference(scs_inference,[],[135,91,90,193,35,189,191,78,16,18,160,41,22,2,26,25,11,9,3,13,10])).
% 59.41/59.43 cnf(200,plain,
% 59.41/59.43 (P1(f6(a3),a7,a2)),
% 59.41/59.43 inference(scs_inference,[],[135,91,90,193,35,189,191,78,16,20,18,186,160,41,42,22,2,26,25,11,9,3,13,10,14,28])).
% 59.41/59.43 cnf(204,plain,
% 59.41/59.43 (P1(a7,f6(a2),a3)),
% 59.41/59.43 inference(scs_inference,[],[135,91,90,193,35,189,191,78,16,20,18,186,160,41,185,46,42,22,2,26,25,11,9,3,13,10,14,28,27])).
% 59.41/59.43 cnf(218,plain,
% 59.41/59.43 (E(f8(f5(a4,a4),f5(a4,a4)),f8(a4,a4))),
% 59.41/59.43 inference(scs_inference,[],[181,2])).
% 59.41/59.43 cnf(219,plain,
% 59.41/59.43 (E(a4,f5(f6(x2191),x2191))),
% 59.41/59.43 inference(scs_inference,[],[181,20,21,2,25])).
% 59.41/59.43 cnf(222,plain,
% 59.41/59.43 (P1(f6(x2221),x2221,f6(f5(a4,a4)))),
% 59.41/59.43 inference(scs_inference,[],[181,138,20,21,2,25,11])).
% 59.41/59.43 cnf(223,plain,
% 59.41/59.43 (P1(f6(f5(a4,a4)),x2231,x2231)),
% 59.41/59.43 inference(scs_inference,[],[181,138,20,18,21,2,25,11,9])).
% 59.41/59.43 cnf(225,plain,
% 59.41/59.43 (P1(a4,x2251,x2251)),
% 59.41/59.43 inference(rename_variables,[],[18])).
% 59.41/59.43 cnf(226,plain,
% 59.41/59.43 (E(f5(f6(a4),a4),f5(a4,a4))),
% 59.41/59.43 inference(scs_inference,[],[74,181,184,138,90,20,18,21,2,25,11,9,10,3])).
% 59.41/59.43 cnf(227,plain,
% 59.41/59.43 (E(f5(x2271,a4),x2271)),
% 59.41/59.43 inference(rename_variables,[],[90])).
% 59.41/59.43 cnf(229,plain,
% 59.41/59.43 (E(f5(x2291,a4),x2291)),
% 59.41/59.43 inference(rename_variables,[],[90])).
% 59.41/59.43 cnf(232,plain,
% 59.41/59.43 (P1(f6(a4),x2321,x2321)),
% 59.41/59.43 inference(scs_inference,[],[74,181,184,138,90,227,20,18,225,152,42,21,2,25,11,9,10,3,13,14,28])).
% 59.41/59.43 cnf(233,plain,
% 59.41/59.43 (P1(f6(x2331),x2331,a4)),
% 59.41/59.43 inference(rename_variables,[],[20])).
% 59.41/59.43 cnf(244,plain,
% 59.41/59.43 (P2(a4,a4,f8(f5(a4,a4),f5(a4,a4)))),
% 59.41/59.43 inference(scs_inference,[],[74,181,184,138,90,227,229,78,20,233,18,225,19,152,95,42,21,22,2,25,11,9,10,3,13,14,28,27,31,12])).
% 59.41/59.43 cnf(250,plain,
% 59.41/59.43 (E(a4,f6(a4))),
% 59.41/59.43 inference(scs_inference,[],[226,19,18,2,25])).
% 59.41/59.43 cnf(251,plain,
% 59.41/59.43 (P1(a4,x2511,x2511)),
% 59.41/59.43 inference(rename_variables,[],[18])).
% 59.41/59.43 cnf(252,plain,
% 59.41/59.43 (P1(x2521,f6(x2521),a4)),
% 59.41/59.43 inference(rename_variables,[],[19])).
% 59.41/59.43 cnf(254,plain,
% 59.41/59.43 (P1(x2541,f6(x2541),f5(f6(x2542),x2542))),
% 59.41/59.43 inference(scs_inference,[],[226,219,19,252,18,2,25,11])).
% 59.41/59.43 cnf(255,plain,
% 59.41/59.43 (P1(f5(f6(x2551),x2551),x2552,x2552)),
% 59.41/59.43 inference(scs_inference,[],[226,219,19,252,18,251,2,25,11,9])).
% 59.41/59.43 cnf(256,plain,
% 59.41/59.43 (P1(f6(a4),f8(a4,x2561),f8(f5(a4,a4),x2561))),
% 59.41/59.43 inference(scs_inference,[],[74,226,219,19,252,18,251,232,2,25,11,9,10])).
% 59.41/59.43 cnf(258,plain,
% 59.41/59.43 (P1(x2581,f6(f5(a4,a4)),x2581)),
% 59.41/59.43 inference(scs_inference,[],[74,226,219,19,252,18,251,222,232,2,25,11,9,10,28])).
% 59.41/59.43 cnf(280,plain,
% 59.41/59.43 (E(f5(a4,a4),f6(a4))),
% 59.41/59.43 inference(scs_inference,[],[184,2])).
% 59.41/59.43 cnf(281,plain,
% 59.41/59.43 (E(a4,f6(f6(a4)))),
% 59.41/59.43 inference(scs_inference,[],[184,19,232,2,25])).
% 59.41/59.43 cnf(285,plain,
% 59.41/59.43 (E(f6(a4),f6(f5(a4,a4)))),
% 59.41/59.43 inference(scs_inference,[],[91,184,138,19,232,2,25,3])).
% 59.41/59.43 cnf(286,plain,
% 59.41/59.43 (P1(f5(a3,a4),a2,f5(a7,a4))),
% 59.41/59.43 inference(scs_inference,[],[91,184,35,138,19,188,232,2,25,3,9])).
% 59.41/59.43 cnf(316,plain,
% 59.41/59.43 (E(f6(f5(a4,a4)),f6(a4))),
% 59.41/59.43 inference(scs_inference,[],[285,2])).
% 59.41/59.43 cnf(317,plain,
% 59.41/59.43 (E(f8(a4,x3171),f5(f8(a4,x3171),f8(a4,x3171)))),
% 59.41/59.43 inference(scs_inference,[],[285,55,21,2,25])).
% 59.41/59.43 cnf(320,plain,
% 59.41/59.43 (P1(f5(a3,a4),f5(a2,a4),a7)),
% 59.41/59.43 inference(scs_inference,[],[35,285,55,196,21,2,25,9])).
% 59.41/59.43 cnf(321,plain,
% 59.41/59.43 (E(x3211,f5(x3211,a4))),
% 59.41/59.43 inference(rename_variables,[],[35])).
% 59.41/59.43 cnf(322,plain,
% 59.41/59.43 (E(f6(a4),f6(f6(a4)))),
% 59.41/59.43 inference(scs_inference,[],[91,35,285,281,55,196,21,2,25,9,3])).
% 59.41/59.43 cnf(323,plain,
% 59.41/59.43 (P1(a4,f8(a4,f5(a4,a4)),f8(a4,a4))),
% 59.41/59.43 inference(scs_inference,[],[180,91,35,285,281,55,18,196,21,2,25,9,3,11])).
% 59.41/59.43 cnf(324,plain,
% 59.41/59.43 (P1(a4,x3241,x3241)),
% 59.41/59.43 inference(rename_variables,[],[18])).
% 59.41/59.43 cnf(329,plain,
% 59.41/59.43 (P1(f8(a4,x3291),a4,a4)),
% 59.41/59.43 inference(scs_inference,[],[180,91,35,321,285,281,55,19,18,324,196,67,21,2,25,9,3,11,13,10,28])).
% 59.41/59.43 cnf(349,plain,
% 59.41/59.43 (E(f8(x3491,a4),f5(f8(x3491,a4),f8(x3491,a4)))),
% 59.41/59.43 inference(scs_inference,[],[317,49,21,2,25])).
% 59.41/59.43 cnf(353,plain,
% 59.41/59.43 (P1(f5(a4,a4),a4,f6(a4))),
% 59.41/59.43 inference(scs_inference,[],[226,91,317,219,49,38,21,2,25,3,9])).
% 59.41/59.43 cnf(355,plain,
% 59.41/59.43 (P1(f6(x3551),x3551,f5(a4,a4))),
% 59.41/59.43 inference(scs_inference,[],[226,91,35,317,219,49,20,38,21,2,25,3,9,11])).
% 59.41/59.43 cnf(358,plain,
% 59.41/59.43 (P1(a4,x3581,x3581)),
% 59.41/59.43 inference(rename_variables,[],[18])).
% 59.41/59.43 cnf(362,plain,
% 59.41/59.43 (P1(f6(a1),a7,a2)),
% 59.41/59.43 inference(scs_inference,[],[226,91,35,317,219,78,22,49,15,20,18,358,38,21,2,25,3,9,11,10,30,28])).
% 59.41/59.43 cnf(370,plain,
% 59.41/59.43 (P2(a4,f8(a4,a4),f8(f8(a4,a4),f5(a4,a4)))),
% 59.41/59.43 inference(scs_inference,[],[226,91,90,35,317,219,78,22,49,15,20,18,358,38,46,41,21,2,25,3,9,11,10,30,28,27,12])).
% 59.41/59.43 cnf(386,plain,
% 59.41/59.43 (E(f5(a4,a4),f6(f5(a4,a4)))),
% 59.41/59.43 inference(scs_inference,[],[349,223,46,2,25])).
% 59.41/59.43 cnf(388,plain,
% 59.41/59.43 (P1(f6(f5(a4,a4)),x3881,x3881)),
% 59.41/59.43 inference(rename_variables,[],[223])).
% 59.41/59.43 cnf(392,plain,
% 59.41/59.43 (P1(f6(a4),f8(f5(a4,a4),f5(a4,a4)),f8(a4,a4))),
% 59.41/59.43 inference(scs_inference,[],[218,349,223,232,17,46,2,25,9,11])).
% 59.41/59.43 cnf(396,plain,
% 59.41/59.43 (P1(f6(f5(a4,a4)),f5(x3961,a4),x3961)),
% 59.41/59.43 inference(scs_inference,[],[218,226,349,223,388,103,156,232,95,17,46,2,25,9,11,10,28])).
% 59.41/59.43 cnf(407,plain,
% 59.41/59.43 (E(f6(f5(a4,a4)),f5(a4,a4))),
% 59.41/59.43 inference(scs_inference,[],[386,2])).
% 59.41/59.43 cnf(409,plain,
% 59.41/59.43 (P1(x4091,f6(f5(a4,a4)),x4091)),
% 59.41/59.43 inference(rename_variables,[],[258])).
% 59.41/59.43 cnf(410,plain,
% 59.41/59.43 (P1(a4,x4101,x4101)),
% 59.41/59.43 inference(rename_variables,[],[18])).
% 59.41/59.43 cnf(414,plain,
% 59.41/59.43 (P1(f6(a4),f8(a4,f5(a4,a4)),f8(a4,a4))),
% 59.41/59.43 inference(scs_inference,[],[180,386,18,258,232,17,2,25,9,11])).
% 59.41/59.43 cnf(416,plain,
% 59.41/59.43 (P1(f5(a4,a4),f5(a4,a4),f6(a4))),
% 59.41/59.43 inference(scs_inference,[],[180,226,386,156,18,258,232,17,2,25,9,11,10])).
% 59.41/59.43 cnf(417,plain,
% 59.41/59.43 (P1(f5(a4,a4),f5(x4171,a4),x4171)),
% 59.41/59.43 inference(rename_variables,[],[156])).
% 59.41/59.43 cnf(420,plain,
% 59.41/59.43 (P1(f5(a4,a4),f5(x4201,a4),x4201)),
% 59.41/59.43 inference(rename_variables,[],[156])).
% 59.41/59.43 cnf(423,plain,
% 59.41/59.43 (P1(f5(a4,a4),f5(f5(x4231,a4),a4),x4231)),
% 59.41/59.43 inference(scs_inference,[],[180,226,386,156,417,420,18,410,258,409,255,103,232,17,2,25,9,11,10,28,27])).
% 59.41/59.43 cnf(458,plain,
% 59.41/59.44 (E(x4581,f5(f5(x4581,a4),a4))),
% 59.41/59.44 inference(scs_inference,[],[219,103,97,2,25])).
% 59.41/59.44 cnf(461,plain,
% 59.41/59.44 (P2(a4,x4611,f8(f6(a4),x4611))),
% 59.41/59.44 inference(scs_inference,[],[91,219,22,103,97,2,25,12])).
% 59.41/59.44 cnf(462,plain,
% 59.41/59.44 (P2(x4621,x4622,f8(x4621,x4622))),
% 59.41/59.44 inference(rename_variables,[],[22])).
% 59.41/59.44 cnf(464,plain,
% 59.41/59.44 (P2(x4641,a4,f8(x4641,f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[91,219,22,462,103,97,2,25,12,3,13])).
% 59.41/59.44 cnf(465,plain,
% 59.41/59.44 (P2(x4651,x4652,f8(x4651,x4652))),
% 59.41/59.44 inference(rename_variables,[],[22])).
% 59.41/59.44 cnf(467,plain,
% 59.41/59.44 (P1(f5(a4,a4),x4671,x4671)),
% 59.41/59.44 inference(rename_variables,[],[95])).
% 59.41/59.44 cnf(471,plain,
% 59.41/59.44 (P1(f6(f5(a4,a4)),x4711,x4711)),
% 59.41/59.44 inference(rename_variables,[],[223])).
% 59.41/59.44 cnf(472,plain,
% 59.41/59.44 (P2(f5(a4,a4),f8(a4,x4721),f8(f8(a4,a4),x4721))),
% 59.41/59.44 inference(scs_inference,[],[91,281,219,78,22,462,465,42,95,223,103,97,2,25,12,3,13,11,9,10,30])).
% 59.41/59.44 cnf(474,plain,
% 59.41/59.44 (P2(x4741,x4742,f8(x4741,x4742))),
% 59.41/59.44 inference(rename_variables,[],[22])).
% 59.41/59.44 cnf(477,plain,
% 59.41/59.44 (P1(f5(a4,a4),x4771,x4771)),
% 59.41/59.44 inference(rename_variables,[],[95])).
% 59.41/59.44 cnf(478,plain,
% 59.41/59.44 (P1(f6(f5(a4,a4)),x4781,x4781)),
% 59.41/59.44 inference(rename_variables,[],[223])).
% 59.41/59.44 cnf(485,plain,
% 59.41/59.44 (E(f8(a4,x4851),f8(f6(a4),x4851))),
% 59.41/59.44 inference(scs_inference,[],[91,281,219,78,22,462,465,474,42,95,467,477,223,471,478,103,396,97,222,2,25,12,3,13,11,9,10,30,28,27,26])).
% 59.41/59.44 cnf(493,plain,
% 59.41/59.44 (E(f8(a4,a4),f8(f6(a4),f5(a4,a4)))),
% 59.41/59.44 inference(scs_inference,[],[322,44,461,2,26])).
% 59.41/59.44 cnf(494,plain,
% 59.41/59.44 (P2(a4,x4941,f8(f6(a4),x4941))),
% 59.41/59.44 inference(rename_variables,[],[461])).
% 59.41/59.44 cnf(495,plain,
% 59.41/59.44 (P2(x4951,f5(a4,a4),f8(x4951,a4))),
% 59.41/59.44 inference(rename_variables,[],[44])).
% 59.41/59.44 cnf(497,plain,
% 59.41/59.44 (E(f5(a4,a4),f5(f6(x4971),x4971))),
% 59.41/59.44 inference(scs_inference,[],[322,44,255,46,461,2,26,25])).
% 59.41/59.44 cnf(499,plain,
% 59.41/59.44 (P1(f5(f6(x4991),x4991),x4992,x4992)),
% 59.41/59.44 inference(rename_variables,[],[255])).
% 59.41/59.44 cnf(501,plain,
% 59.41/59.44 (P2(f5(a4,a4),x5011,f8(f6(a4),x5011))),
% 59.41/59.44 inference(scs_inference,[],[184,322,44,22,255,46,461,2,26,25,12])).
% 59.41/59.44 cnf(502,plain,
% 59.41/59.44 (P2(x5021,x5022,f8(x5021,x5022))),
% 59.41/59.44 inference(rename_variables,[],[22])).
% 59.41/59.44 cnf(503,plain,
% 59.41/59.44 (E(f5(a4,a4),f6(f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[184,90,281,322,44,22,255,46,461,2,26,25,12,3])).
% 59.41/59.44 cnf(505,plain,
% 59.41/59.44 (P2(x5051,f5(a4,a4),f8(x5051,f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[184,90,281,322,44,22,502,255,46,461,2,26,25,12,3,13])).
% 59.41/59.44 cnf(508,plain,
% 59.41/59.44 (P1(f5(f6(x5081),x5081),x5082,x5082)),
% 59.41/59.44 inference(rename_variables,[],[255])).
% 59.41/59.44 cnf(512,plain,
% 59.41/59.44 (P1(f5(f6(x5121),x5121),x5122,x5122)),
% 59.41/59.44 inference(rename_variables,[],[255])).
% 59.41/59.44 cnf(517,plain,
% 59.41/59.44 (P1(f5(f6(x5171),x5171),x5172,f5(x5172,a4))),
% 59.41/59.44 inference(scs_inference,[],[184,90,281,322,78,44,495,22,502,255,499,508,512,95,46,156,19,461,494,2,26,25,12,3,13,11,9,10,29,28])).
% 59.41/59.44 cnf(518,plain,
% 59.41/59.44 (P1(f5(f6(x5181),x5181),x5182,x5182)),
% 59.41/59.44 inference(rename_variables,[],[255])).
% 59.41/59.44 cnf(519,plain,
% 59.41/59.44 (P1(f5(a4,a4),x5191,x5191)),
% 59.41/59.44 inference(rename_variables,[],[95])).
% 59.41/59.44 cnf(521,plain,
% 59.41/59.44 (P1(f5(f6(x5211),x5211),f5(x5212,a4),x5212)),
% 59.41/59.44 inference(scs_inference,[],[184,90,281,322,78,44,495,22,502,255,499,508,512,518,95,519,46,156,19,461,494,2,26,25,12,3,13,11,9,10,29,28,27])).
% 59.41/59.44 cnf(546,plain,
% 59.41/59.44 (E(f8(a4,a4),f8(f5(a4,a4),f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[497,78,505,2,26])).
% 59.41/59.44 cnf(549,plain,
% 59.41/59.44 (E(f5(f5(x5491,a4),a4),x5491)),
% 59.41/59.44 inference(scs_inference,[],[497,78,95,423,505,2,26,25])).
% 59.41/59.44 cnf(555,plain,
% 59.41/59.44 (E(f5(x5551,a4),x5551)),
% 59.41/59.44 inference(rename_variables,[],[90])).
% 59.41/59.44 cnf(558,plain,
% 59.41/59.44 (P1(f5(x5581,a4),f5(a4,a4),x5581)),
% 59.41/59.44 inference(scs_inference,[],[90,555,497,280,78,44,42,95,46,423,505,2,26,25,12,3,13,11])).
% 59.41/59.44 cnf(559,plain,
% 59.41/59.44 (P1(x5591,f5(a4,a4),x5591)),
% 59.41/59.44 inference(rename_variables,[],[46])).
% 59.41/59.44 cnf(564,plain,
% 59.41/59.44 (P1(f8(a4,x5641),f5(a4,a4),f5(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[90,555,497,280,78,44,55,42,95,223,46,559,423,41,505,2,26,25,12,3,13,11,9,10,28])).
% 59.41/59.44 cnf(577,plain,
% 59.41/59.44 (E(f8(x5771,a4),f8(x5771,f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[546,22,464,2,26])).
% 59.41/59.44 cnf(579,plain,
% 59.41/59.44 (P2(x5791,x5792,f8(x5791,x5792))),
% 59.41/59.44 inference(rename_variables,[],[22])).
% 59.41/59.44 cnf(581,plain,
% 59.41/59.44 (P2(x5811,x5812,f8(f5(x5811,a4),x5812))),
% 59.41/59.44 inference(scs_inference,[],[90,546,22,579,464,2,26,12])).
% 59.41/59.44 cnf(582,plain,
% 59.41/59.44 (P2(x5821,x5822,f8(x5821,x5822))),
% 59.41/59.44 inference(rename_variables,[],[22])).
% 59.41/59.44 cnf(585,plain,
% 59.41/59.44 (P2(x5851,x5852,f8(x5851,f5(x5852,a4)))),
% 59.41/59.44 inference(scs_inference,[],[23,90,546,549,22,579,582,464,2,26,12,3,13])).
% 59.41/59.44 cnf(587,plain,
% 59.41/59.44 (P1(x5871,f6(f5(a4,a4)),f5(x5871,a4))),
% 59.41/59.44 inference(scs_inference,[],[23,90,546,549,22,579,582,258,464,2,26,12,3,13,9])).
% 59.41/59.44 cnf(589,plain,
% 59.41/59.44 (P1(a4,f5(f5(x5891,a4),a4),x5891)),
% 59.41/59.44 inference(scs_inference,[],[23,90,546,549,22,579,582,103,258,464,2,26,12,3,13,9,11])).
% 59.41/59.44 cnf(591,plain,
% 59.41/59.44 (P1(f5(x5911,a4),f6(f5(a4,a4)),x5911)),
% 59.41/59.44 inference(scs_inference,[],[23,90,138,546,549,22,579,582,103,38,258,464,2,26,12,3,13,9,11,10])).
% 59.41/59.44 cnf(594,plain,
% 59.41/59.44 (P1(f5(f6(x5941),x5941),x5942,x5942)),
% 59.41/59.44 inference(rename_variables,[],[255])).
% 59.41/59.44 cnf(595,plain,
% 59.41/59.44 (P1(x5951,a4,x5951)),
% 59.41/59.44 inference(rename_variables,[],[17])).
% 59.41/59.44 cnf(597,plain,
% 59.41/59.44 (P1(a4,a4,f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[23,90,138,546,549,22,579,582,255,594,17,595,103,38,258,232,464,2,26,12,3,13,9,11,10,28,27])).
% 59.41/59.44 cnf(619,plain,
% 59.41/59.44 (P1(f6(a4),f5(x6191,a4),x6191)),
% 59.41/59.44 inference(scs_inference,[],[184,90,493,501,521,464,2,12,13,9])).
% 59.41/59.44 cnf(626,plain,
% 59.41/59.44 (P1(f8(x6261,a4),a4,a4)),
% 59.41/59.44 inference(scs_inference,[],[184,90,493,49,156,223,19,501,521,464,2,12,13,9,11,10,28])).
% 59.41/59.44 cnf(648,plain,
% 59.41/59.44 (E(f6(f6(a4)),f5(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[503,2])).
% 59.41/59.44 cnf(672,plain,
% 59.41/59.44 (P2(x6721,f5(a4,a4),f8(x6721,a4))),
% 59.41/59.44 inference(rename_variables,[],[44])).
% 59.41/59.44 cnf(679,plain,
% 59.41/59.44 (P1(f5(a4,a4),f5(x6791,a4),x6791)),
% 59.41/59.44 inference(rename_variables,[],[156])).
% 59.41/59.44 cnf(680,plain,
% 59.41/59.44 (P1(x6801,a4,f5(x6801,f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[91,386,35,485,44,672,42,156,222,21,2,12,14,13,9,11,10])).
% 59.41/59.44 cnf(685,plain,
% 59.41/59.44 (P1(f6(a4),f5(f5(a4,a4),a4),f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[91,386,35,485,44,672,42,156,679,232,416,222,21,2,12,14,13,9,11,10,28,27])).
% 59.41/59.44 cnf(688,plain,
% 59.41/59.44 (E(a4,f5(a4,f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[91,386,35,485,44,672,42,18,156,679,232,416,222,21,2,12,14,13,9,11,10,28,27,25])).
% 59.41/59.44 cnf(691,plain,
% 59.41/59.44 (E(f6(a4),f5(a4,f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[91,386,35,485,44,672,42,18,156,679,232,416,222,21,2,12,14,13,9,11,10,28,27,25,3])).
% 59.41/59.44 cnf(696,plain,
% 59.41/59.44 (P2(f6(f5(a4,a4)),x6961,f8(a4,x6961))),
% 59.41/59.44 inference(scs_inference,[],[386,577,42,2,12])).
% 59.41/59.44 cnf(703,plain,
% 59.41/59.44 (P1(x7031,f5(a4,a4),f5(x7031,f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[184,386,577,42,223,461,222,21,2,12,13,9,11,10])).
% 59.41/59.44 cnf(704,plain,
% 59.41/59.44 (P1(x7041,x7042,f5(x7041,x7042))),
% 59.41/59.44 inference(rename_variables,[],[21])).
% 59.41/59.44 cnf(708,plain,
% 59.41/59.44 (P1(f6(a4),x7081,f5(x7081,a4))),
% 59.41/59.44 inference(scs_inference,[],[184,386,577,49,42,18,223,38,461,222,21,704,517,2,12,13,9,11,10,28,27])).
% 59.41/59.44 cnf(718,plain,
% 59.41/59.44 (P1(a4,x7181,f5(f6(a4),x7181))),
% 59.41/59.44 inference(scs_inference,[],[91,691,42,464,21,2,12,13,9])).
% 59.41/59.44 cnf(719,plain,
% 59.41/59.44 (P1(x7191,x7192,f5(x7191,x7192))),
% 59.41/59.44 inference(rename_variables,[],[21])).
% 59.41/59.44 cnf(721,plain,
% 59.41/59.44 (P1(x7211,f6(f5(a4,a4)),x7211)),
% 59.41/59.44 inference(rename_variables,[],[258])).
% 59.41/59.44 cnf(727,plain,
% 59.41/59.44 (P1(f5(x7271,a4),f5(f5(a4,a4),a4),x7271)),
% 59.41/59.44 inference(scs_inference,[],[91,691,55,42,396,258,721,558,464,21,719,20,2,12,13,9,11,10,28,27])).
% 59.41/59.44 cnf(731,plain,
% 59.41/59.44 (E(x7311,f5(f6(a4),x7311))),
% 59.41/59.44 inference(scs_inference,[],[91,691,55,42,396,18,258,721,558,464,21,719,20,2,12,13,9,11,10,28,27,25])).
% 59.41/59.44 cnf(735,plain,
% 59.41/59.44 (E(f5(a4,a4),f5(a4,f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[688,18,703,2,25])).
% 59.41/59.44 cnf(739,plain,
% 59.41/59.44 (E(f6(a4),f5(f6(a4),f5(a4,a4)))),
% 59.41/59.44 inference(scs_inference,[],[184,688,731,18,703,2,25,3])).
% 59.41/59.44 cnf(745,plain,
% 59.41/59.44 (P1(f5(a4,a4),x7451,f5(f6(a4),x7451))),
% 59.41/59.44 inference(scs_inference,[],[184,688,731,18,21,581,585,703,2,25,3,12,13,9])).
% 59.41/59.44 cnf(762,plain,
% 59.41/59.44 (E(x7621,f5(x7621,f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[735,17,680,2,25])).
% 59.41/59.44 cnf(765,plain,
% 59.41/59.44 (P2(a4,x7651,f8(f6(a4),f5(x7651,a4)))),
% 59.41/59.44 inference(scs_inference,[],[91,735,17,585,680,2,25,12])).
% 59.41/59.44 cnf(771,plain,
% 59.41/59.44 (P1(f6(a4),f6(a4),a4)),
% 59.41/59.44 inference(scs_inference,[],[91,735,17,232,581,585,41,680,2,25,12,13,9,11])).
% 59.41/59.44 cnf(783,plain,
% 59.41/59.44 (E(f8(x7831,a4),f8(f5(x7831,a4),f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[91,735,55,22,17,95,255,232,581,585,355,41,323,680,2,25,12,13,9,11,10,28,27,26])).
% 59.41/59.44 cnf(796,plain,
% 59.41/59.44 (E(f5(f6(a4),x7961),x7961)),
% 59.41/59.44 inference(scs_inference,[],[731,2])).
% 59.41/59.44 cnf(797,plain,
% 59.41/59.44 (E(x7971,f5(f6(a4),f5(x7971,a4)))),
% 59.41/59.44 inference(scs_inference,[],[731,156,745,2,25])).
% 59.41/59.44 cnf(800,plain,
% 59.41/59.44 (E(f6(a4),f5(f5(a4,a4),f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[184,731,762,156,745,2,25,3])).
% 59.41/59.44 cnf(804,plain,
% 59.41/59.44 (P1(f6(a4),f6(a4),f5(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[184,731,762,156,232,41,745,2,25,3,9,11])).
% 59.41/59.44 cnf(816,plain,
% 59.41/59.44 (E(f5(f6(a4),f5(x8161,a4)),x8161)),
% 59.41/59.44 inference(scs_inference,[],[797,2])).
% 59.41/59.44 cnf(819,plain,
% 59.41/59.44 (P1(f5(a1,a4),f5(a2,a4),a7)),
% 59.41/59.44 inference(scs_inference,[],[23,35,796,797,154,2,3,9])).
% 59.41/59.44 cnf(845,plain,
% 59.41/59.44 (E(f8(a4,x8451),f8(f6(a4),f5(x8451,a4)))),
% 59.41/59.44 inference(scs_inference,[],[739,22,765,2,26])).
% 59.41/59.44 cnf(849,plain,
% 59.41/59.44 (E(x8491,f5(f5(x8491,a4),f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[739,22,38,765,680,2,26,25])).
% 59.41/59.44 cnf(850,plain,
% 59.41/59.44 (P1(x8501,a4,f5(x8501,f6(a4)))),
% 59.41/59.44 inference(rename_variables,[],[680])).
% 59.41/59.44 cnf(854,plain,
% 59.41/59.44 (P1(f5(a4,a4),a4,f5(f6(a4),f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[23,184,816,739,22,38,765,680,850,2,26,25,3,9])).
% 59.41/59.44 cnf(858,plain,
% 59.41/59.44 (P1(a1,f5(a2,a4),f5(a7,a4))),
% 59.41/59.44 inference(scs_inference,[],[23,184,35,816,739,22,38,258,765,680,850,142,2,26,25,3,9,11,10])).
% 59.41/59.44 cnf(860,plain,
% 59.41/59.44 (P1(f5(f5(a4,a4),a4),x8601,x8601)),
% 59.41/59.44 inference(scs_inference,[],[23,184,35,816,739,22,156,38,258,103,765,680,850,142,2,26,25,3,9,11,10,28])).
% 59.41/59.44 cnf(878,plain,
% 59.41/59.44 (E(a4,f5(f6(a4),f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[849,232,680,2,25])).
% 59.41/59.44 cnf(879,plain,
% 59.41/59.44 (P1(x8791,a4,f5(x8791,f6(a4)))),
% 59.41/59.44 inference(rename_variables,[],[680])).
% 59.41/59.44 cnf(880,plain,
% 59.41/59.44 (P1(f6(a4),x8801,x8801)),
% 59.41/59.44 inference(rename_variables,[],[232])).
% 59.41/59.44 cnf(889,plain,
% 59.41/59.44 (P1(f6(a4),x8891,f5(f5(x8891,a4),a4))),
% 59.41/59.44 inference(scs_inference,[],[23,91,849,232,880,18,619,589,680,879,860,2,25,3,9,11,10,28])).
% 59.41/59.44 cnf(898,plain,
% 59.41/59.44 (P1(f5(f5(a1,a4),a4),a2,a7)),
% 59.41/59.44 inference(scs_inference,[],[35,800,144,2,9])).
% 59.41/59.44 cnf(903,plain,
% 59.41/59.44 (P1(f8(x9031,a4),f5(a4,a4),f5(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[184,386,35,800,49,619,41,144,564,2,9,11,10,28])).
% 59.41/59.44 cnf(919,plain,
% 59.41/59.44 (P1(f5(f8(x9191,a4),a4),f5(a4,a4),f5(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[35,878,903,2,9])).
% 59.41/59.44 cnf(940,plain,
% 59.41/59.44 (E(f5(x9401,f6(a4)),x9401)),
% 59.41/59.44 inference(scs_inference,[],[762,2])).
% 59.41/59.44 cnf(942,plain,
% 59.41/59.44 (P1(f6(f6(a4)),x9421,x9421)),
% 59.41/59.44 inference(scs_inference,[],[23,281,762,18,2,3,9])).
% 59.41/59.44 cnf(943,plain,
% 59.41/59.44 (P1(x9431,f6(x9431),f6(f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[23,281,762,18,19,2,3,9,11])).
% 59.41/59.44 cnf(944,plain,
% 59.41/59.44 (P1(x9441,f6(f6(a4)),x9441)),
% 59.41/59.44 inference(scs_inference,[],[23,281,762,17,18,19,2,3,9,11,10])).
% 59.41/59.44 cnf(965,plain,
% 59.41/59.44 (P1(f6(x9651),x9651,f5(f6(x9652),x9652))),
% 59.41/59.44 inference(scs_inference,[],[91,219,783,20,889,2,9,11])).
% 59.41/59.44 cnf(966,plain,
% 59.41/59.44 (P1(x9661,f5(f6(x9662),x9662),x9661)),
% 59.41/59.44 inference(scs_inference,[],[91,219,783,17,20,889,2,9,11,10])).
% 59.41/59.44 cnf(967,plain,
% 59.41/59.44 (P1(f5(a4,a4),a7,f5(a3,a2))),
% 59.41/59.44 inference(scs_inference,[],[91,219,783,156,17,21,20,889,190,2,9,11,10,28])).
% 59.41/59.44 cnf(982,plain,
% 59.41/59.44 (P1(f5(a4,a4),f6(f6(a4)),f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[184,845,232,944,966,2,25,9])).
% 59.41/59.44 cnf(1003,plain,
% 59.41/59.44 (P1(f5(f6(x10031),x10031),f5(a4,a4),f8(x10032,a4))),
% 59.41/59.44 inference(scs_inference,[],[91,521,46,860,942,944,919,9,11,10,28])).
% 59.41/59.44 cnf(1009,plain,
% 59.41/59.44 (P1(x10091,f5(f6(x10092),x10092),x10091)),
% 59.41/59.44 inference(rename_variables,[],[966])).
% 59.41/59.44 cnf(1010,plain,
% 59.41/59.44 (P1(x10101,f6(x10101),f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[184,90,254,966,9,11])).
% 59.41/59.44 cnf(1012,plain,
% 59.41/59.44 (E(f5(x10121,a4),x10121)),
% 59.41/59.44 inference(rename_variables,[],[90])).
% 59.41/59.44 cnf(1013,plain,
% 59.41/59.44 (P1(x10131,f6(a4),x10131)),
% 59.41/59.44 inference(scs_inference,[],[184,90,1012,254,966,1009,9,11,10])).
% 59.41/59.44 cnf(1016,plain,
% 59.41/59.44 (P1(f6(f5(a4,a4)),f8(x10161,a4),f5(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[184,90,1012,396,232,254,966,1009,1003,9,11,10,28])).
% 59.41/59.44 cnf(1028,plain,
% 59.41/59.44 (P1(x10281,f5(f6(x10282),x10282),x10281)),
% 59.41/59.44 inference(rename_variables,[],[966])).
% 59.41/59.44 cnf(1033,plain,
% 59.41/59.44 (P1(f5(a4,a4),f8(x10331,a4),f5(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[91,49,943,966,1028,1016,9,11,10,27])).
% 59.41/59.44 cnf(1042,plain,
% 59.41/59.44 (P1(f5(f5(a3,a4),a4),a2,a7)),
% 59.41/59.44 inference(scs_inference,[],[458,16,9])).
% 59.41/59.44 cnf(1061,plain,
% 59.41/59.44 (P1(f5(a4,a4),f5(f6(a4),f6(a4)),a4)),
% 59.41/59.44 inference(scs_inference,[],[184,458,416,232,943,16,854,392,11,9,10,28])).
% 59.41/59.44 cnf(1081,plain,
% 59.41/59.44 (P1(f6(x10811),x10811,f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[91,90,965,703,9,11])).
% 59.41/59.44 cnf(1084,plain,
% 59.41/59.44 (P1(f5(a4,a4),f5(f8(x10841,a4),a4),f5(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[91,90,35,965,703,1033,9,11,10])).
% 59.41/59.44 cnf(1094,plain,
% 59.41/59.44 (P1(f5(a1,a4),f5(a2,a4),f5(a7,a4))),
% 59.41/59.44 inference(scs_inference,[],[35,819,11])).
% 59.41/59.44 cnf(1095,plain,
% 59.41/59.44 (E(x10951,f5(x10951,a4))),
% 59.41/59.44 inference(rename_variables,[],[35])).
% 59.41/59.44 cnf(1097,plain,
% 59.41/59.44 (P1(f5(f5(a1,a4),a4),f5(a2,a4),a7)),
% 59.41/59.44 inference(scs_inference,[],[91,35,1095,685,819,898,11,9,10])).
% 59.41/59.44 cnf(1099,plain,
% 59.41/59.44 (P1(f5(a4,a4),f5(f6(a4),f5(a4,a4)),f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[91,35,1095,416,46,745,685,819,898,11,9,10,28])).
% 59.41/59.44 cnf(1107,plain,
% 59.41/59.44 (P1(f5(a1,a4),a2,f5(a7,a4))),
% 59.41/59.44 inference(scs_inference,[],[184,90,35,1094,320,414,9,11,10])).
% 59.41/59.44 cnf(1113,plain,
% 59.41/59.44 (P1(f8(x11131,a4),f6(a4),f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[184,90,35,49,396,258,942,1010,1094,320,414,9,11,10,27,28])).
% 59.41/59.44 cnf(1128,plain,
% 59.41/59.44 (P1(f5(a4,a4),f8(a4,x11281),f8(f5(a4,a4),x11281))),
% 59.41/59.44 inference(scs_inference,[],[184,256,9])).
% 59.41/59.44 cnf(1129,plain,
% 59.41/59.44 (P1(f5(f5(a1,a4),a4),f5(a2,a4),f5(a7,a4))),
% 59.41/59.44 inference(scs_inference,[],[184,35,256,1097,9,11])).
% 59.41/59.44 cnf(1131,plain,
% 59.41/59.44 (P1(f8(x11311,a4),f5(a4,a4),f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[184,35,256,1097,1113,9,11,10])).
% 59.41/59.44 cnf(1137,plain,
% 59.41/59.44 (P1(f5(f8(x11371,a4),a4),f5(a4,a4),f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[91,35,1099,1131,11,9])).
% 59.41/59.44 cnf(1141,plain,
% 59.41/59.44 (P1(f5(a4,a4),f6(a4),f6(f6(a4)))),
% 59.41/59.44 inference(scs_inference,[],[91,90,35,416,232,1129,982,1099,1131,11,9,10,28])).
% 59.41/59.44 cnf(1146,plain,
% 59.41/59.44 (P1(f5(f8(x11461,a4),a4),f5(a4,a4),a4)),
% 59.41/59.44 inference(scs_inference,[],[91,386,1137,967,9,11])).
% 59.41/59.44 cnf(1147,plain,
% 59.41/59.44 (P1(f5(a4,a4),f5(a7,a4),f5(a3,a2))),
% 59.41/59.44 inference(scs_inference,[],[91,386,35,1137,967,9,11,10])).
% 59.41/59.44 cnf(1149,plain,
% 59.41/59.44 (P1(f5(a4,a4),f8(f5(a4,a4),x11491),f8(a4,x11491))),
% 59.41/59.44 inference(scs_inference,[],[91,386,35,416,232,1128,1137,967,9,11,10,28])).
% 59.41/59.44 cnf(1158,plain,
% 59.41/59.44 (P1(f6(f5(a4,a4)),f5(a7,a4),f5(a3,a2))),
% 59.41/59.44 inference(scs_inference,[],[386,35,1147,11,9])).
% 59.41/59.44 cnf(1160,plain,
% 59.41/59.44 (P1(f8(a4,x11601),f6(a4),f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[184,386,35,55,1010,1147,1141,11,9,10,28])).
% 59.41/59.44 cnf(1175,plain,
% 59.41/59.44 (P2(f5(a4,a4),f5(a4,a4),f5(f6(a4),f8(a4,a4)))),
% 59.41/59.44 inference(scs_inference,[],[731,78,14])).
% 59.41/59.44 cnf(1197,plain,
% 59.41/59.44 (P1(f5(f6(a4),f5(a1,a4)),a2,a7)),
% 59.41/59.44 inference(scs_inference,[],[797,15,9])).
% 59.41/59.44 cnf(1198,plain,
% 59.41/59.44 (E(x11981,f5(f6(a4),f5(x11981,a4)))),
% 59.41/59.44 inference(rename_variables,[],[797])).
% 59.41/59.44 cnf(1200,plain,
% 59.41/59.44 (E(x12001,f5(f6(a4),f5(x12001,a4)))),
% 59.41/59.44 inference(rename_variables,[],[797])).
% 59.41/59.44 cnf(1201,plain,
% 59.41/59.44 (P1(a1,f5(f6(a4),f5(a2,a4)),a7)),
% 59.41/59.44 inference(scs_inference,[],[797,1198,1200,15,9,11,10])).
% 59.41/59.44 cnf(1218,plain,
% 59.41/59.44 (E(x12181,f5(f5(x12181,a4),f6(a4)))),
% 59.41/59.44 inference(rename_variables,[],[849])).
% 59.41/59.44 cnf(1220,plain,
% 59.41/59.44 (E(x12201,f5(f5(x12201,a4),f6(a4)))),
% 59.41/59.44 inference(rename_variables,[],[849])).
% 59.41/59.44 cnf(1221,plain,
% 59.41/59.44 (P1(a3,f5(f5(a2,a4),f6(a4)),a7)),
% 59.41/59.44 inference(scs_inference,[],[849,1218,1220,16,11,9,10])).
% 59.41/59.44 cnf(1229,plain,
% 59.41/59.44 (E(x12291,f5(x12291,f6(a4)))),
% 59.41/59.44 inference(rename_variables,[],[762])).
% 59.41/59.44 cnf(1231,plain,
% 59.41/59.44 (E(x12311,f5(x12311,f6(a4)))),
% 59.41/59.44 inference(rename_variables,[],[762])).
% 59.41/59.44 cnf(1233,plain,
% 59.41/59.44 (E(x12331,f5(x12331,f6(a4)))),
% 59.41/59.44 inference(rename_variables,[],[762])).
% 59.41/59.44 cnf(1236,plain,
% 59.41/59.44 (P1(f5(a4,a4),f5(f6(a4),f5(x12361,a4)),x12361)),
% 59.41/59.44 inference(scs_inference,[],[762,1229,1231,1233,78,55,95,103,718,14,9,11,10,28])).
% 59.41/59.44 cnf(1251,plain,
% 59.41/59.44 (E(x12511,f5(f5(x12511,a4),f6(a4)))),
% 59.41/59.44 inference(rename_variables,[],[849])).
% 59.41/59.44 cnf(1253,plain,
% 59.41/59.44 (E(x12531,f5(f5(x12531,a4),f6(a4)))),
% 59.41/59.44 inference(rename_variables,[],[849])).
% 59.41/59.44 cnf(1256,plain,
% 59.41/59.44 (P1(a4,f5(f6(a4),f5(x12561,a4)),x12561)),
% 59.41/59.44 inference(scs_inference,[],[849,1251,1253,156,95,15,1236,11,9,10,27])).
% 59.41/59.44 cnf(1257,plain,
% 59.41/59.44 (P1(f5(a4,a4),f5(x12571,a4),x12571)),
% 59.41/59.44 inference(rename_variables,[],[156])).
% 59.41/59.44 cnf(1260,plain,
% 59.41/59.44 (P1(f5(a4,a4),f5(f6(a4),x12601),x12601)),
% 59.41/59.44 inference(scs_inference,[],[849,1251,1253,156,1257,95,18,745,15,1236,11,9,10,27,28])).
% 59.41/59.44 cnf(1266,plain,
% 59.41/59.44 (E(x12661,f5(f5(x12661,a4),f6(a4)))),
% 59.41/59.44 inference(rename_variables,[],[849])).
% 59.41/59.44 cnf(1267,plain,
% 59.41/59.44 (P1(f8(a4,x12671),f6(a4),f5(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[184,849,858,1160,9,11])).
% 59.41/59.44 cnf(1270,plain,
% 59.41/59.44 (P1(x12701,f5(f5(a4,a4),a4),x12701)),
% 59.41/59.44 inference(scs_inference,[],[184,849,1266,591,223,727,1107,858,1160,9,11,10,27])).
% 59.41/59.44 cnf(1274,plain,
% 59.41/59.44 (P1(f5(f6(x12741),x12741),f5(a7,a4),f5(a1,a2))),
% 59.41/59.44 inference(scs_inference,[],[184,849,1266,591,521,223,727,21,1107,858,1160,9,11,10,27,28])).
% 59.41/59.44 cnf(1292,plain,
% 59.41/59.44 (P1(f8(a4,x12921),a4,f6(f5(a4,a4)))),
% 59.41/59.44 inference(scs_inference,[],[138,90,1146,329,9,11])).
% 59.41/59.44 cnf(1308,plain,
% 59.41/59.44 (P1(f8(x13081,a4),a4,f6(f5(a4,a4)))),
% 59.41/59.44 inference(scs_inference,[],[138,626,11])).
% 59.41/59.44 cnf(1309,plain,
% 59.41/59.44 (P1(f5(f5(a7,a4),a4),f6(a2),a3)),
% 59.41/59.44 inference(scs_inference,[],[138,458,626,204,11,9])).
% 59.41/59.44 cnf(1310,plain,
% 59.41/59.44 (E(x13101,f5(f5(x13101,a4),a4))),
% 59.41/59.44 inference(rename_variables,[],[458])).
% 59.41/59.44 cnf(1311,plain,
% 59.41/59.44 (P1(a1,f5(f5(a2,a4),a4),a7)),
% 59.41/59.44 inference(scs_inference,[],[138,458,1310,15,626,204,11,9,10])).
% 59.41/59.44 cnf(1327,plain,
% 59.41/59.44 (P2(f5(f6(x13271),x13271),f5(a4,a4),f8(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[219,44,12])).
% 59.41/59.44 cnf(1329,plain,
% 59.41/59.44 (P2(x13291,f5(f6(x13292),x13292),f8(x13291,a4))),
% 59.41/59.44 inference(scs_inference,[],[219,44,22,12,13])).
% 59.41/59.44 cnf(1331,plain,
% 59.41/59.44 (P1(f5(f6(x13311),x13311),x13312,f5(a4,x13312))),
% 59.41/59.44 inference(scs_inference,[],[219,44,22,21,12,13,9])).
% 59.41/59.44 cnf(1335,plain,
% 59.41/59.44 (P1(f6(a4),f5(x13351,a4),f5(a4,x13351))),
% 59.41/59.44 inference(scs_inference,[],[219,44,22,591,38,396,771,21,12,13,9,10,11,27])).
% 59.41/59.44 cnf(1346,plain,
% 59.41/59.44 (E(x13461,f5(a4,f5(x13461,a4)))),
% 59.41/59.44 inference(scs_inference,[],[521,1331,25])).
% 59.41/59.44 cnf(1349,plain,
% 59.41/59.44 (P2(f6(a4),f5(a4,a4),f8(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[90,521,1327,1331,25,12])).
% 59.41/59.44 cnf(1351,plain,
% 59.41/59.44 (E(f5(x13511,a4),x13511)),
% 59.41/59.44 inference(rename_variables,[],[90])).
% 59.41/59.44 cnf(1353,plain,
% 59.41/59.44 (E(x13531,f5(x13531,a4))),
% 59.41/59.44 inference(rename_variables,[],[35])).
% 59.41/59.44 cnf(1354,plain,
% 59.41/59.44 (P2(x13541,f6(a4),f8(x13541,a4))),
% 59.41/59.44 inference(scs_inference,[],[90,1351,35,521,1327,1329,1331,25,12,14,13])).
% 59.41/59.44 cnf(1357,plain,
% 59.41/59.44 (P1(f6(f5(a4,a4)),x13571,f5(a4,x13571))),
% 59.41/59.44 inference(scs_inference,[],[138,90,1351,35,521,21,1327,1329,1331,25,12,14,13,9])).
% 59.41/59.44 cnf(1359,plain,
% 59.41/59.44 (P1(f6(a3),a7,f5(a2,a4))),
% 59.41/59.44 inference(scs_inference,[],[138,90,1351,35,1353,521,21,200,1327,1329,1331,25,12,14,13,9,11])).
% 59.41/59.44 cnf(1382,plain,
% 59.41/59.44 (P2(f6(f6(a4)),f5(a4,a4),f8(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[281,44,558,1331,25,12])).
% 59.41/59.44 cnf(1393,plain,
% 59.41/59.44 (P1(f6(x13931),f5(x13931,a4),f6(a4))),
% 59.41/59.44 inference(scs_inference,[],[281,35,44,22,558,38,258,396,619,21,1081,1354,1331,25,12,14,13,9,11,10,27])).
% 59.41/59.44 cnf(1406,plain,
% 59.41/59.44 (P2(f6(f5(a4,a4)),f6(a4),f8(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[138,1354,12])).
% 59.41/59.44 cnf(1409,plain,
% 59.41/59.44 (E(x14091,f5(f6(a4),x14091))),
% 59.41/59.44 inference(rename_variables,[],[731])).
% 59.41/59.44 cnf(1410,plain,
% 59.41/59.44 (P2(f6(a4),f6(f5(a4,a4)),f8(a4,a4))),
% 59.41/59.44 inference(scs_inference,[],[138,386,731,44,1349,1354,12,14,13])).
% 59.41/59.44 cnf(1412,plain,
% 59.41/59.44 (E(x14121,f5(f6(a4),x14121))),
% 59.41/59.44 inference(rename_variables,[],[731])).
% 59.41/59.44 cnf(1414,plain,
% 59.41/59.44 (E(x14141,f5(f6(a4),x14141))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(1417,plain,
% 59.41/59.45 (P1(f5(a4,a4),f5(a4,f5(x14171,a4)),x14171)),
% 59.41/59.45 inference(scs_inference,[],[138,386,731,1409,1412,1414,44,49,95,396,16,1349,1357,1354,12,14,13,9,11,10,28])).
% 59.41/59.45 cnf(1428,plain,
% 59.41/59.45 (E(x14281,f5(a4,x14281))),
% 59.41/59.45 inference(scs_inference,[],[223,1357,25])).
% 59.41/59.45 cnf(1431,plain,
% 59.41/59.45 (P2(f5(a4,a4),f6(a4),f8(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[407,223,1406,1357,25,12])).
% 59.41/59.45 cnf(1433,plain,
% 59.41/59.45 (E(x14331,f5(x14331,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1435,plain,
% 59.41/59.45 (E(x14351,f5(x14351,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1436,plain,
% 59.41/59.45 (P1(f6(a1),a7,f5(a2,a4))),
% 59.41/59.45 inference(scs_inference,[],[407,35,1433,1435,223,362,1406,1357,25,12,14,9,11])).
% 59.41/59.45 cnf(1437,plain,
% 59.41/59.45 (E(x14371,f5(x14371,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1443,plain,
% 59.41/59.45 (E(f5(a4,x14431),x14431)),
% 59.41/59.45 inference(scs_inference,[],[407,35,1433,1435,1437,78,22,223,362,1406,1357,25,12,14,9,11,10,30,2])).
% 59.41/59.45 cnf(1444,plain,
% 59.41/59.45 (~E(a3,f5(a4,a1))),
% 59.41/59.45 inference(scs_inference,[],[23,407,35,1433,1435,1437,78,22,223,362,1406,1357,25,12,14,9,11,10,30,2,3])).
% 59.41/59.45 cnf(1463,plain,
% 59.41/59.45 (P2(f6(a4),x14631,f8(a4,x14631))),
% 59.41/59.45 inference(scs_inference,[],[316,696,12])).
% 59.41/59.45 cnf(1465,plain,
% 59.41/59.45 (E(x14651,f5(x14651,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1466,plain,
% 59.41/59.45 (P2(f6(a4),f6(a4),f8(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[316,35,696,1410,12,14,13])).
% 59.41/59.45 cnf(1471,plain,
% 59.41/59.45 (P1(f5(x14711,a4),f6(a4),x14711)),
% 59.41/59.45 inference(scs_inference,[],[648,316,35,1465,591,965,1042,696,1410,12,14,13,9,11,10])).
% 59.41/59.45 cnf(1472,plain,
% 59.41/59.45 (P2(f6(a4),f8(a4,a4),f8(f8(a4,a4),f6(a4)))),
% 59.41/59.45 inference(scs_inference,[],[648,316,35,1465,22,591,965,1042,696,1410,12,14,13,9,11,10,30])).
% 59.41/59.45 cnf(1478,plain,
% 59.41/59.45 (E(x14781,f5(x14781,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1480,plain,
% 59.41/59.45 (P1(f5(f8(a4,x14801),a4),f5(a4,a4),f5(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[386,91,35,1478,564,1472,1466,12,14,11,9])).
% 59.41/59.45 cnf(1493,plain,
% 59.41/59.45 (P1(f5(a4,a4),f8(x14931,a4),f6(f5(a4,a4)))),
% 59.41/59.45 inference(scs_inference,[],[386,1033,11])).
% 59.41/59.45 cnf(1494,plain,
% 59.41/59.45 (P1(f5(f8(a4,x14941),a4),f6(a4),f6(a4))),
% 59.41/59.45 inference(scs_inference,[],[386,35,1033,1160,11,9])).
% 59.41/59.45 cnf(1499,plain,
% 59.41/59.45 (P1(a7,f6(a2),f5(a3,a4))),
% 59.41/59.45 inference(scs_inference,[],[35,204,11])).
% 59.41/59.45 cnf(1500,plain,
% 59.41/59.45 (E(x15001,f5(x15001,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1501,plain,
% 59.41/59.45 (P1(f5(f8(a4,x15011),a4),a4,a4)),
% 59.41/59.45 inference(scs_inference,[],[35,1500,329,204,11,9])).
% 59.41/59.45 cnf(1507,plain,
% 59.41/59.45 (E(x15071,f5(x15071,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1508,plain,
% 59.41/59.45 (P1(f5(f8(x15081,a4),a4),a4,a4)),
% 59.41/59.45 inference(scs_inference,[],[35,1507,626,967,11,9])).
% 59.41/59.45 cnf(1514,plain,
% 59.41/59.45 (P1(f6(a4),f5(a4,a4),f8(x15141,a4))),
% 59.41/59.45 inference(scs_inference,[],[90,184,1003,1113,11,9])).
% 59.41/59.45 cnf(1517,plain,
% 59.41/59.45 (P1(f8(a4,x15171),f5(a4,a4),f6(a4))),
% 59.41/59.45 inference(scs_inference,[],[90,184,1003,1113,1160,11,9,10])).
% 59.41/59.45 cnf(1528,plain,
% 59.41/59.45 (P1(f5(a7,a4),f6(a2),a3)),
% 59.41/59.45 inference(scs_inference,[],[91,35,1160,204,11,9])).
% 59.41/59.45 cnf(1550,plain,
% 59.41/59.45 (E(x15501,f5(x15501,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1553,plain,
% 59.41/59.45 (P1(f5(f6(x15531),x15531),a7,f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[90,35,1550,1221,1274,9,11,10])).
% 59.41/59.45 cnf(1558,plain,
% 59.41/59.45 (P1(f5(f8(a4,x15581),a4),f6(a4),f5(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[386,35,1267,11,9])).
% 59.41/59.45 cnf(1559,plain,
% 59.41/59.45 (E(x15591,f5(x15591,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1560,plain,
% 59.41/59.45 (P1(f5(f6(a4),f5(a1,a4)),f5(a2,a4),a7)),
% 59.41/59.45 inference(scs_inference,[],[386,35,1559,1267,1197,11,9,10])).
% 59.41/59.45 cnf(1573,plain,
% 59.41/59.45 (E(x15731,f5(x15731,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1574,plain,
% 59.41/59.45 (P1(a7,f5(f6(a2),a4),f5(a3,a4))),
% 59.41/59.45 inference(scs_inference,[],[35,1573,1201,1499,11,10])).
% 59.41/59.45 cnf(1582,plain,
% 59.41/59.45 (P1(f6(a4),f5(a7,a4),f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[90,35,1274,1197,11,9])).
% 59.41/59.45 cnf(1589,plain,
% 59.41/59.45 (P1(f6(x15891),f5(x15891,a4),f5(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[184,1393,11])).
% 59.41/59.45 cnf(1592,plain,
% 59.41/59.45 (P1(f6(a4),x15921,f5(a4,x15921))),
% 59.41/59.45 inference(scs_inference,[],[90,184,35,1331,1393,1436,11,10,9])).
% 59.41/59.45 cnf(1600,plain,
% 59.41/59.45 (P1(f5(a4,a4),f5(x16001,a4),f5(a4,x16001))),
% 59.41/59.45 inference(scs_inference,[],[184,35,1335,1309,11,9])).
% 59.41/59.45 cnf(1606,plain,
% 59.41/59.45 (E(x16061,f5(x16061,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1607,plain,
% 59.41/59.45 (P1(f8(x16071,a4),a4,f6(a4))),
% 59.41/59.45 inference(scs_inference,[],[91,35,1113,1311,11,10])).
% 59.41/59.45 cnf(1608,plain,
% 59.41/59.45 (P1(f5(a1,a4),f5(f5(a2,a4),a4),a7)),
% 59.41/59.45 inference(scs_inference,[],[91,35,1606,1113,1311,11,10,9])).
% 59.41/59.45 cnf(1622,plain,
% 59.41/59.45 (P1(f6(a4),a7,f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[90,35,1560,1582,11,10])).
% 59.41/59.45 cnf(1645,plain,
% 59.41/59.45 (E(x16451,f5(x16451,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1646,plain,
% 59.41/59.45 (P1(f5(a7,a4),f5(f6(a2),a4),f5(a3,a4))),
% 59.41/59.45 inference(scs_inference,[],[35,1645,1574,1608,11,9])).
% 59.41/59.45 cnf(1652,plain,
% 59.41/59.45 (P1(f5(a7,a4),f6(a2),f5(a3,a4))),
% 59.41/59.45 inference(scs_inference,[],[90,1646,10])).
% 59.41/59.45 cnf(1658,plain,
% 59.41/59.45 (P1(f6(a4),f5(a4,a4),f5(f8(x16581,a4),a4))),
% 59.41/59.45 inference(scs_inference,[],[35,1514,11])).
% 59.41/59.45 cnf(1666,plain,
% 59.41/59.45 (P1(f8(a4,x16661),a4,f5(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[407,1292,11])).
% 59.41/59.45 cnf(1667,plain,
% 59.41/59.45 (P1(f5(a4,a4),x16671,f5(a4,x16671))),
% 59.41/59.45 inference(scs_inference,[],[407,184,1592,1292,11,9])).
% 59.41/59.45 cnf(1672,plain,
% 59.41/59.45 (P1(f8(x16721,a4),a4,f5(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[407,91,1335,1308,9,11])).
% 59.41/59.45 cnf(1673,plain,
% 59.41/59.45 (P1(f5(f8(a4,x16731),a4),a4,f5(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[407,91,1335,1558,1308,9,11,10])).
% 59.41/59.45 cnf(1676,plain,
% 59.41/59.45 (P1(f5(a4,a4),f8(x16761,a4),f6(a4))),
% 59.41/59.45 inference(scs_inference,[],[316,1493,11])).
% 59.41/59.45 cnf(1677,plain,
% 59.41/59.45 (P1(f6(a4),f5(a7,a4),f5(a3,a2))),
% 59.41/59.45 inference(scs_inference,[],[316,1158,1493,11,9])).
% 59.41/59.45 cnf(1678,plain,
% 59.41/59.45 (P1(x16781,f6(a4),f5(x16781,a4))),
% 59.41/59.45 inference(scs_inference,[],[316,1158,587,1493,11,9,10])).
% 59.41/59.45 cnf(1684,plain,
% 59.41/59.45 (E(x16841,f5(x16841,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(1686,plain,
% 59.41/59.45 (P1(f6(a4),f5(a7,a4),f5(f5(a3,a2),a4))),
% 59.41/59.45 inference(scs_inference,[],[386,35,1684,1676,1677,10,9,11])).
% 59.41/59.45 cnf(1688,plain,
% 59.41/59.45 (P1(f6(a4),f8(x16881,a4),f6(a4))),
% 59.41/59.45 inference(scs_inference,[],[386,35,1684,49,1676,1677,10,9,11,27])).
% 59.41/59.45 cnf(1694,plain,
% 59.41/59.45 (P1(f6(a4),f8(x16941,a4),f5(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[90,184,1686,1688,10,11])).
% 59.41/59.45 cnf(1695,plain,
% 59.41/59.45 (P1(f5(a4,a4),f5(a4,a4),f5(f8(x16951,a4),a4))),
% 59.41/59.45 inference(scs_inference,[],[90,184,1686,1658,1688,10,11,9])).
% 59.41/59.45 cnf(1704,plain,
% 59.41/59.45 (P1(f5(a4,a4),f5(a4,a4),f8(x17041,a4))),
% 59.41/59.45 inference(scs_inference,[],[90,91,35,1695,1694,10,9,11])).
% 59.41/59.45 cnf(1736,plain,
% 59.41/59.45 (E(x17361,f5(f6(a4),f5(x17361,a4)))),
% 59.41/59.45 inference(rename_variables,[],[797])).
% 59.41/59.45 cnf(1741,plain,
% 59.41/59.45 (P1(f5(f6(x17411),x17411),a7,f5(a3,a2))),
% 59.41/59.45 inference(scs_inference,[],[549,797,1736,521,727,21,16,190,10,9,11,28])).
% 59.41/59.45 cnf(1837,plain,
% 59.41/59.45 (P1(a4,a7,f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[549,796,849,200,1393,1553,10,11,9])).
% 59.41/59.45 cnf(1843,plain,
% 59.41/59.45 (E(x18431,f5(f5(x18431,a4),a4))),
% 59.41/59.45 inference(rename_variables,[],[458])).
% 59.41/59.45 cnf(1846,plain,
% 59.41/59.45 (P1(f5(a4,a4),f5(a7,a4),f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[184,458,1843,204,1359,1582,10,11,9])).
% 59.41/59.45 cnf(1860,plain,
% 59.41/59.45 (P1(a4,a7,f5(a3,a2))),
% 59.41/59.45 inference(scs_inference,[],[549,796,458,200,1589,1741,10,11,9])).
% 59.41/59.45 cnf(1910,plain,
% 59.41/59.45 (P1(a4,f5(f6(a4),x19101),x19101)),
% 59.41/59.45 inference(scs_inference,[],[90,1260,9])).
% 59.41/59.45 cnf(1911,plain,
% 59.41/59.45 (E(f5(x19111,a4),x19111)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(1912,plain,
% 59.41/59.45 (E(a7,f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[15,90,1260,21,9,25])).
% 59.41/59.45 cnf(1913,plain,
% 59.41/59.45 (P1(x19131,x19132,f5(x19131,x19132))),
% 59.41/59.45 inference(rename_variables,[],[21])).
% 59.41/59.45 cnf(1916,plain,
% 59.41/59.45 (E(f5(x19161,a4),x19161)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(1917,plain,
% 59.41/59.45 (E(f5(f5(a7,a4),a4),f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[15,549,90,1911,1260,21,1084,9,25,11,3])).
% 59.41/59.45 cnf(1919,plain,
% 59.41/59.45 (P2(a4,f8(a4,x19191),f8(f8(a4,a4),x19191))),
% 59.41/59.45 inference(scs_inference,[],[15,549,90,1911,1916,1260,21,1084,472,9,25,11,3,12])).
% 59.41/59.45 cnf(1920,plain,
% 59.41/59.45 (E(f5(x19201,a4),x19201)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(1921,plain,
% 59.41/59.45 (P2(f6(f6(a4)),a4,f8(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[15,549,90,1911,1916,1920,1382,1260,21,1084,472,9,25,11,3,12,13])).
% 59.41/59.45 cnf(1922,plain,
% 59.41/59.45 (E(f5(x19221,a4),x19221)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(1926,plain,
% 59.41/59.45 (P1(x19261,f5(a4,a4),x19261)),
% 59.41/59.45 inference(rename_variables,[],[46])).
% 59.41/59.45 cnf(1929,plain,
% 59.41/59.45 (P1(a7,f6(a2),a1)),
% 59.41/59.45 inference(scs_inference,[],[15,549,90,1911,1916,1920,1922,46,1926,41,1382,1260,1704,21,1913,1084,472,9,25,11,3,12,13,10,28,27])).
% 59.41/59.45 cnf(1933,plain,
% 59.41/59.45 (E(f5(a1,a2),a7)),
% 59.41/59.45 inference(scs_inference,[],[15,549,90,1911,1916,1920,1922,46,1926,41,1382,1260,1704,21,1913,1084,472,9,25,11,3,12,13,10,28,27,2])).
% 59.41/59.45 cnf(1941,plain,
% 59.41/59.45 (E(f5(x19411,a4),x19411)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(1943,plain,
% 59.41/59.45 (E(f5(x19431,a4),x19431)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(1944,plain,
% 59.41/59.45 (P2(f5(f6(x19441),x19441),a4,f8(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[90,1941,1943,1917,1327,1149,1033,2,9,11,13])).
% 59.41/59.45 cnf(2021,plain,
% 59.41/59.45 (E(x20211,f5(f6(a4),x20211))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2023,plain,
% 59.41/59.45 (E(x20231,f5(f6(a4),x20231))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2025,plain,
% 59.41/59.45 (E(x20251,f5(f6(a4),x20251))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2026,plain,
% 59.41/59.45 (P2(f5(a4,a4),f5(f6(a4),f5(a4,a4)),f8(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[15,731,2021,2023,2025,78,12,9,11,13])).
% 59.41/59.45 cnf(2048,plain,
% 59.41/59.45 (E(x20481,f5(x20481,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(2050,plain,
% 59.41/59.45 (E(x20501,f5(x20501,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(2052,plain,
% 59.41/59.45 (E(x20521,f5(x20521,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(2054,plain,
% 59.41/59.45 (E(x20541,f5(x20541,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(2057,plain,
% 59.41/59.45 (P1(f6(a4),x20571,f5(f6(a4),f5(x20571,a4)))),
% 59.41/59.45 inference(scs_inference,[],[35,2048,2050,2052,2054,619,18,19,1431,1466,1081,1236,1061,9,12,11,13,10,28])).
% 59.41/59.45 cnf(2076,plain,
% 59.41/59.45 (E(f5(x20761,a4),x20761)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(2078,plain,
% 59.41/59.45 (E(x20781,f5(f6(a4),f5(x20781,a4)))),
% 59.41/59.45 inference(rename_variables,[],[797])).
% 59.41/59.45 cnf(2080,plain,
% 59.41/59.45 (E(x20801,f5(f6(a4),f5(x20801,a4)))),
% 59.41/59.45 inference(rename_variables,[],[797])).
% 59.41/59.45 cnf(2083,plain,
% 59.41/59.45 (P1(f5(x20831,a4),f5(f6(a4),f5(a4,a4)),x20831)),
% 59.41/59.45 inference(scs_inference,[],[90,2076,797,2078,2080,38,103,771,1175,2026,12,9,11,13,10])).
% 59.41/59.45 cnf(2122,plain,
% 59.41/59.45 (P1(f5(f5(a4,a4),f6(a4)),f5(x21221,a4),x21221)),
% 59.41/59.45 inference(scs_inference,[],[849,103,9])).
% 59.41/59.45 cnf(2173,plain,
% 59.41/59.45 (E(x21731,f5(f6(a4),x21731))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2175,plain,
% 59.41/59.45 (E(x21751,f5(f6(a4),x21751))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2177,plain,
% 59.41/59.45 (E(x21771,f5(f6(a4),x21771))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2179,plain,
% 59.41/59.45 (E(x21791,f5(f6(a4),x21791))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2181,plain,
% 59.41/59.45 (E(x21811,f5(f6(a4),x21811))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2190,plain,
% 59.41/59.45 (P1(x21901,f5(f5(a4,a4),a4),x21901)),
% 59.41/59.45 inference(rename_variables,[],[1270])).
% 59.41/59.45 cnf(2193,plain,
% 59.41/59.45 (E(f5(f6(a4),f6(a4)),f5(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[15,731,2173,2175,2177,2179,2181,44,1270,2190,46,619,38,42,41,718,2122,9,12,14,11,13,10,28,27,25])).
% 59.41/59.45 cnf(2200,plain,
% 59.41/59.45 (P1(a4,f5(a4,f5(x22001,a4)),x22001)),
% 59.41/59.45 inference(scs_inference,[],[90,2193,1417,2,9])).
% 59.41/59.45 cnf(2203,plain,
% 59.41/59.45 (E(x22031,f5(x22031,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(2205,plain,
% 59.41/59.45 (E(x22051,f5(x22051,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(2207,plain,
% 59.41/59.45 (E(x22071,f5(x22071,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(2210,plain,
% 59.41/59.45 (P1(f5(f6(x22101),x22101),f8(x22102,a4),f6(a4))),
% 59.41/59.45 inference(scs_inference,[],[90,35,2203,2205,2207,2193,46,521,1466,41,1417,1131,1003,1463,2,9,12,11,13,10,28])).
% 59.41/59.45 cnf(2252,plain,
% 59.41/59.45 (E(x22521,f5(x22521,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2254,plain,
% 59.41/59.45 (E(x22541,f5(x22541,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2256,plain,
% 59.41/59.45 (E(x22561,f5(x22561,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2258,plain,
% 59.41/59.45 (E(x22581,f5(x22581,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2260,plain,
% 59.41/59.45 (E(x22601,f5(x22601,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2261,plain,
% 59.41/59.45 (P1(f5(x22611,a4),f5(a4,f6(a4)),x22611)),
% 59.41/59.45 inference(scs_inference,[],[762,2252,2254,2256,2258,2260,44,38,232,42,19,9,12,14,11,13,10])).
% 59.41/59.45 cnf(2303,plain,
% 59.41/59.45 (E(x23031,f5(f5(x23031,a4),a4))),
% 59.41/59.45 inference(rename_variables,[],[458])).
% 59.41/59.45 cnf(2306,plain,
% 59.41/59.45 (P1(f5(f6(x23061),x23061),f5(a3,a2),a7)),
% 59.41/59.45 inference(scs_inference,[],[549,458,2303,521,103,20,1147,2083,1666,9,11,10,28])).
% 59.41/59.45 cnf(2381,plain,
% 59.41/59.45 (E(x23811,f5(x23811,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2383,plain,
% 59.41/59.45 (E(x23831,f5(x23831,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2384,plain,
% 59.41/59.45 (P2(f5(a4,a4),f6(a4),f5(f8(a4,a4),f6(a4)))),
% 59.41/59.45 inference(scs_inference,[],[762,2381,2383,416,1431,12,9,14])).
% 59.41/59.45 cnf(2408,plain,
% 59.41/59.45 (E(x24081,f5(f5(x24081,a4),f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[849])).
% 59.41/59.45 cnf(2410,plain,
% 59.41/59.45 (E(x24101,f5(f5(x24101,a4),f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[849])).
% 59.41/59.45 cnf(2413,plain,
% 59.41/59.45 (P1(f5(f6(x24131),x24131),f5(a1,a2),a7)),
% 59.41/59.45 inference(scs_inference,[],[849,2408,2410,521,619,597,353,626,1274,9,11,10,28])).
% 59.41/59.45 cnf(2472,plain,
% 59.41/59.45 (E(x24721,f5(f6(a4),x24721))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2474,plain,
% 59.41/59.45 (E(x24741,f5(f6(a4),x24741))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2476,plain,
% 59.41/59.45 (E(x24761,f5(f6(a4),x24761))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2478,plain,
% 59.41/59.45 (E(x24781,f5(f6(a4),x24781))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2480,plain,
% 59.41/59.45 (E(x24801,f5(f6(a4),x24801))),
% 59.41/59.45 inference(rename_variables,[],[731])).
% 59.41/59.45 cnf(2483,plain,
% 59.41/59.45 (P1(f5(f6(x24831),x24831),f5(a4,a4),f8(a4,x24832))),
% 59.41/59.45 inference(scs_inference,[],[731,2472,2474,2476,2478,2480,521,17,771,804,1354,1466,1704,1673,12,14,13,9,11,10,28])).
% 59.41/59.45 cnf(2496,plain,
% 59.41/59.45 (E(x24961,f5(f6(a4),f5(x24961,a4)))),
% 59.41/59.45 inference(rename_variables,[],[797])).
% 59.41/59.45 cnf(2498,plain,
% 59.41/59.45 (E(x24981,f5(f6(a4),f5(x24981,a4)))),
% 59.41/59.45 inference(rename_variables,[],[797])).
% 59.41/59.45 cnf(2501,plain,
% 59.41/59.45 (P1(a1,a2,f5(a4,a7))),
% 59.41/59.45 inference(scs_inference,[],[15,797,2496,2498,232,16,196,286,1592,9,11,10,27])).
% 59.41/59.45 cnf(2515,plain,
% 59.41/59.45 (P2(f5(f6(a4),f6(a4)),f5(a4,a4),f8(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[762,1349,12])).
% 59.41/59.45 cnf(2538,plain,
% 59.41/59.45 (E(x25381,f5(f5(x25381,a4),f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[849])).
% 59.41/59.45 cnf(2542,plain,
% 59.41/59.45 (P1(f6(a4),f5(x25421,a4),x25421)),
% 59.41/59.45 inference(rename_variables,[],[619])).
% 59.41/59.45 cnf(2545,plain,
% 59.41/59.45 (P1(x25451,f5(a4,a4),f5(a4,x25451))),
% 59.41/59.45 inference(scs_inference,[],[549,849,2538,558,619,2542,21,2261,1097,626,329,1592,9,11,10,28,27])).
% 59.41/59.45 cnf(2561,plain,
% 59.41/59.45 (E(x25611,f5(f5(x25611,a4),a4))),
% 59.41/59.45 inference(rename_variables,[],[458])).
% 59.41/59.45 cnf(2563,plain,
% 59.41/59.45 (E(x25631,f5(f5(x25631,a4),a4))),
% 59.41/59.45 inference(rename_variables,[],[458])).
% 59.41/59.45 cnf(2571,plain,
% 59.41/59.45 (P1(a7,f6(a2),f5(a4,a1))),
% 59.41/59.45 inference(scs_inference,[],[15,458,2561,2563,396,619,41,626,1274,1672,1837,2545,9,11,10,28,27])).
% 59.41/59.45 cnf(2588,plain,
% 59.41/59.45 (E(f5(x25881,a4),x25881)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(2590,plain,
% 59.41/59.45 (E(f5(x25901,a4),x25901)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(2591,plain,
% 59.41/59.45 (P1(a4,f5(a7,a4),f5(a3,a2))),
% 59.41/59.45 inference(scs_inference,[],[90,2588,2590,1147,2515,2384,12,13,9])).
% 59.41/59.45 cnf(2643,plain,
% 59.41/59.45 (P1(f6(a4),f5(f6(a4),f5(x26431,a4)),x26431)),
% 59.41/59.45 inference(scs_inference,[],[250,61,67,1256,12,13,9])).
% 59.41/59.45 cnf(2672,plain,
% 59.41/59.45 (E(x26721,f5(x26721,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2674,plain,
% 59.41/59.45 (E(x26741,f5(x26741,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2676,plain,
% 59.41/59.45 (E(x26761,f5(x26761,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2679,plain,
% 59.41/59.45 (P1(f5(f6(x26791),x26791),f6(a4),f8(a4,x26792))),
% 59.41/59.45 inference(scs_inference,[],[250,762,2672,2674,2676,521,1013,1354,19,1704,1944,16,244,1494,12,13,14,9,11,10,28])).
% 59.41/59.45 cnf(2688,plain,
% 59.41/59.45 (P1(f6(a4),f5(f6(a4),x26881),x26881)),
% 59.41/59.45 inference(scs_inference,[],[250,1910,1921,370,12,13,9])).
% 59.41/59.45 cnf(2690,plain,
% 59.41/59.45 (E(x26901,f5(f5(x26901,a4),f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[849])).
% 59.41/59.45 cnf(2694,plain,
% 59.41/59.45 (P1(f6(a4),f5(x26941,a4),x26941)),
% 59.41/59.45 inference(rename_variables,[],[619])).
% 59.41/59.45 cnf(2697,plain,
% 59.41/59.45 (P1(x26971,f5(a4,a4),f5(f6(a4),f5(x26971,a4)))),
% 59.41/59.45 inference(scs_inference,[],[250,849,2690,558,619,2694,21,1910,1921,1129,1622,1528,370,2057,12,13,9,11,10,28,27])).
% 59.41/59.45 cnf(2713,plain,
% 59.41/59.45 (P2(a4,f6(a4),f8(f5(a4,a4),f5(a4,a4)))),
% 59.41/59.45 inference(scs_inference,[],[250,244,1919,12,13])).
% 59.41/59.45 cnf(2717,plain,
% 59.41/59.45 (P1(a1,f5(a4,a2),a7)),
% 59.41/59.45 inference(scs_inference,[],[15,250,46,2200,2545,244,1508,1501,1919,12,13,9,11,10,28])).
% 59.41/59.45 cnf(2739,plain,
% 59.41/59.45 (E(x27391,f5(f5(x27391,a4),a4))),
% 59.41/59.45 inference(rename_variables,[],[458])).
% 59.41/59.45 cnf(2741,plain,
% 59.41/59.45 (E(x27411,f5(f5(x27411,a4),a4))),
% 59.41/59.45 inference(rename_variables,[],[458])).
% 59.41/59.45 cnf(2744,plain,
% 59.41/59.45 (P1(f5(f6(x27441),x27441),f8(a4,x27442),a4)),
% 59.41/59.45 inference(scs_inference,[],[250,458,2739,2741,521,619,1436,1528,194,1929,2483,2713,12,13,9,11,10,28])).
% 59.41/59.45 cnf(2747,plain,
% 59.41/59.45 (P1(f6(a4),f5(x27471,a4),x27471)),
% 59.41/59.45 inference(rename_variables,[],[619])).
% 59.41/59.45 cnf(2749,plain,
% 59.41/59.45 (P1(f5(f6(a4),f5(x27491,a4)),f5(a4,a4),x27491)),
% 59.41/59.45 inference(scs_inference,[],[250,458,2739,2741,558,521,619,2747,1436,1528,2643,194,1929,2483,2713,12,13,9,11,10,28,27])).
% 59.41/59.45 cnf(2821,plain,
% 59.41/59.45 (P2(f6(a4),f5(a4,a4),f5(f8(a4,a4),f6(a4)))),
% 59.41/59.45 inference(scs_inference,[],[762,1349,14])).
% 59.41/59.45 cnf(2822,plain,
% 59.41/59.45 (E(x28221,f5(x28221,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2824,plain,
% 59.41/59.45 (E(x28241,f5(x28241,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2826,plain,
% 59.41/59.45 (E(x28261,f5(x28261,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(2831,plain,
% 59.41/59.45 (P1(f6(a4),x28311,x28311)),
% 59.41/59.45 inference(rename_variables,[],[232])).
% 59.41/59.45 cnf(2832,plain,
% 59.41/59.45 (P1(x28321,f5(a4,a4),x28321)),
% 59.41/59.45 inference(rename_variables,[],[46])).
% 59.41/59.45 cnf(2834,plain,
% 59.41/59.45 (P1(f5(f6(a4),x28341),f5(a4,a4),x28341)),
% 59.41/59.45 inference(scs_inference,[],[762,2822,2824,2826,232,2831,46,2832,1010,1349,1081,154,2688,1667,14,9,11,10,28,27])).
% 59.41/59.45 cnf(2880,plain,
% 59.41/59.45 (E(f5(x28801,a4),x28801)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(2886,plain,
% 59.41/59.45 (P1(x28861,a4,f5(a4,x28861))),
% 59.41/59.45 inference(scs_inference,[],[940,90,2880,35,1003,2545,1607,2821,13,9,11,10])).
% 59.41/59.45 cnf(2888,plain,
% 59.41/59.45 (P1(f5(f6(x28881),x28881),f8(a4,x28882),f6(a4))),
% 59.41/59.45 inference(scs_inference,[],[940,90,2880,35,521,232,1003,2545,1607,2821,2679,13,9,11,10,28])).
% 59.41/59.45 cnf(2893,plain,
% 59.41/59.45 (P1(a4,f8(a4,x28931),a4)),
% 59.41/59.45 inference(scs_inference,[],[940,90,2880,35,55,521,232,1003,2545,1607,2821,2679,2744,13,9,11,10,28,27])).
% 59.41/59.45 cnf(2964,plain,
% 59.41/59.45 (P1(a4,f8(x29641,a4),f6(a4))),
% 59.41/59.45 inference(scs_inference,[],[796,2210,9])).
% 59.41/59.45 cnf(3018,plain,
% 59.41/59.45 (E(f5(x30181,a4),x30181)),
% 59.41/59.45 inference(rename_variables,[],[90])).
% 59.41/59.45 cnf(3021,plain,
% 59.41/59.45 (P1(f5(f6(x30211),x30211),f5(a4,x30212),x30212)),
% 59.41/59.45 inference(scs_inference,[],[90,3018,35,521,232,1331,2749,1393,1480,9,11,10,28])).
% 59.41/59.45 cnf(3057,plain,
% 59.41/59.45 (E(x30571,f5(x30571,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(3059,plain,
% 59.41/59.45 (E(x30591,f5(x30591,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(3060,plain,
% 59.41/59.45 (P1(f5(x30601,a4),f5(f6(a4),f6(a4)),x30601)),
% 59.41/59.45 inference(scs_inference,[],[762,3057,3059,1471,1592,903,9,11,10])).
% 59.41/59.45 cnf(3062,plain,
% 59.41/59.45 (P1(f6(a4),f8(a4,x30621),f6(a4))),
% 59.41/59.45 inference(scs_inference,[],[762,3057,3059,55,1471,1592,903,2888,9,11,10,27])).
% 59.41/59.45 cnf(3076,plain,
% 59.41/59.45 (P1(a4,f5(a1,a2),a7)),
% 59.41/59.45 inference(scs_inference,[],[796,2413,9])).
% 59.41/59.45 cnf(3080,plain,
% 59.41/59.45 (E(x30801,f5(f5(x30801,a4),f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[849])).
% 59.41/59.45 cnf(3083,plain,
% 59.41/59.45 (P1(f6(a4),f6(a4),f8(x30831,a4))),
% 59.41/59.45 inference(scs_inference,[],[796,849,3080,619,46,1137,1860,2413,1929,9,11,10,28])).
% 59.41/59.45 cnf(3126,plain,
% 59.41/59.45 (E(x31261,f5(x31261,a4))),
% 59.41/59.45 inference(rename_variables,[],[35])).
% 59.41/59.45 cnf(3131,plain,
% 59.41/59.45 (P1(a7,a4,f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[15,90,35,3126,17,21,1335,2834,1517,9,11,10,27])).
% 59.41/59.45 cnf(3207,plain,
% 59.41/59.45 (E(x32071,f5(x32071,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(3209,plain,
% 59.41/59.45 (E(x32091,f5(x32091,f6(a4)))),
% 59.41/59.45 inference(rename_variables,[],[762])).
% 59.41/59.45 cnf(3212,plain,
% 59.41/59.45 (P1(f5(a1,a4),f5(a4,a2),a7)),
% 59.41/59.45 inference(scs_inference,[],[15,762,3207,3209,558,1704,16,1131,1667,9,11,10,28])).
% 59.41/59.45 cnf(3228,plain,
% 59.41/59.45 (P1(a4,f5(a4,x32281),x32281)),
% 59.41/59.45 inference(scs_inference,[],[796,3021,9])).
% 59.41/59.45 cnf(3252,plain,
% 59.41/59.45 (P1(a4,f8(a4,x32521),f6(a4))),
% 59.41/59.45 inference(scs_inference,[],[549,250,3060,2893,9,11])).
% 59.41/59.45 cnf(3289,plain,
% 59.41/59.45 (E(x32891,f5(a4,f5(x32891,a4)))),
% 59.41/59.45 inference(rename_variables,[],[1346])).
% 59.41/59.45 cnf(3291,plain,
% 59.41/59.45 (E(x32911,f5(a4,f5(x32911,a4)))),
% 59.41/59.45 inference(rename_variables,[],[1346])).
% 59.41/59.45 cnf(3296,plain,
% 59.41/59.45 (P1(f5(f6(x32961),x32961),f5(x32962,a4),x32962)),
% 59.41/59.45 inference(rename_variables,[],[521])).
% 59.41/59.45 cnf(3299,plain,
% 59.41/59.45 (P1(f5(a4,x32991),f5(a4,a4),x32991)),
% 59.41/59.45 inference(scs_inference,[],[1346,3289,3291,521,3296,232,558,16,142,144,1003,3021,9,11,10,28,27])).
% 59.41/59.45 cnf(3340,plain,
% 59.41/59.45 (P2(f5(a4,f5(a4,a4)),f5(a4,a4),f8(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[1428,78,12])).
% 59.41/59.45 cnf(3341,plain,
% 59.41/59.45 (E(x33411,f5(a4,x33411))),
% 59.41/59.45 inference(rename_variables,[],[1428])).
% 59.41/59.45 cnf(3342,plain,
% 59.41/59.45 (P2(f5(a4,a4),f5(a4,f5(a4,a4)),f8(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[1428,3341,78,12,13])).
% 59.41/59.45 cnf(3343,plain,
% 59.41/59.45 (E(x33431,f5(a4,x33431))),
% 59.41/59.45 inference(rename_variables,[],[1428])).
% 59.41/59.45 cnf(3345,plain,
% 59.41/59.45 (E(x33451,f5(a4,x33451))),
% 59.41/59.45 inference(rename_variables,[],[1428])).
% 59.41/59.45 cnf(3347,plain,
% 59.41/59.45 (E(x33471,f5(a4,x33471))),
% 59.41/59.45 inference(rename_variables,[],[1428])).
% 59.41/59.45 cnf(3349,plain,
% 59.41/59.45 (E(x33491,f5(a4,x33491))),
% 59.41/59.45 inference(rename_variables,[],[1428])).
% 59.41/59.45 cnf(3352,plain,
% 59.41/59.45 (P1(f6(a4),f5(a3,a2),a7)),
% 59.41/59.45 inference(scs_inference,[],[15,1428,3341,3343,3345,3347,3349,78,619,46,416,18,967,12,13,14,9,11,10,28])).
% 59.41/59.45 cnf(3371,plain,
% 59.41/59.45 (E(f5(a4,x33711),x33711)),
% 59.41/59.45 inference(rename_variables,[],[1443])).
% 59.41/59.45 cnf(3373,plain,
% 59.41/59.45 (E(f5(a4,x33731),x33731)),
% 59.41/59.45 inference(rename_variables,[],[1443])).
% 59.41/59.45 cnf(3381,plain,
% 59.41/59.45 (P1(f6(a4),f5(a1,a2),f5(a7,a4))),
% 59.41/59.45 inference(scs_inference,[],[940,1443,3371,3373,797,619,232,362,1274,2697,3021,3340,3342,12,13,11,9,10,28])).
% 59.41/59.45 cnf(3434,plain,
% 59.41/59.45 (P1(a4,f5(a3,a2),a7)),
% 59.41/59.45 inference(scs_inference,[],[796,849,2306,3076,11,9])).
% 59.41/59.45 cnf(3447,plain,
% 59.41/59.45 (P1(x34471,f6(a4),f5(a4,x34471))),
% 59.41/59.45 inference(scs_inference,[],[940,250,458,2886,1741,3076,11,9,10])).
% 59.41/59.45 cnf(3586,plain,
% 59.41/59.45 (P1(f5(a4,a2),f5(a1,a4),a7)),
% 59.41/59.45 inference(scs_inference,[],[3212,24])).
% 59.41/59.45 cnf(3588,plain,
% 59.41/59.45 (~E(a1,a3)),
% 59.41/59.45 inference(scs_inference,[],[23,3212,24,2])).
% 59.41/59.45 cnf(3589,plain,
% 59.41/59.45 (~E(f5(a4,a3),a1)),
% 59.41/59.45 inference(scs_inference,[],[23,3212,1428,24,2,3])).
% 59.41/59.45 cnf(3592,plain,
% 59.41/59.45 (P1(x35921,f6(a4),f5(a4,x35921))),
% 59.41/59.45 inference(rename_variables,[],[3447])).
% 59.41/59.45 cnf(3594,plain,
% 59.41/59.45 (~P1(a3,f6(a4),f5(a4,a1))),
% 59.41/59.45 inference(scs_inference,[],[23,3447,3212,1428,1443,24,2,3,25,11])).
% 59.41/59.45 cnf(3595,plain,
% 59.41/59.45 (E(f5(a4,x35951),x35951)),
% 59.41/59.45 inference(rename_variables,[],[1443])).
% 59.41/59.45 cnf(3598,plain,
% 59.41/59.45 (~P1(a3,f5(a4,a4),a1)),
% 59.41/59.45 inference(scs_inference,[],[23,3447,3212,280,1428,1443,3595,24,2,3,25,11,9,10])).
% 59.41/59.45 cnf(3599,plain,
% 59.41/59.45 (~P1(f5(a4,a3),f8(a4,x35991),a1)),
% 59.41/59.45 inference(scs_inference,[],[23,3447,3592,3212,3062,280,1428,1443,3595,24,2,3,25,11,9,10,28])).
% 59.41/59.45 cnf(3600,plain,
% 59.41/59.45 (P1(x36001,f6(a4),f5(a4,x36001))),
% 59.41/59.45 inference(rename_variables,[],[3447])).
% 59.41/59.45 cnf(3602,plain,
% 59.41/59.45 (~P1(a3,f8(x36021,a4),a1)),
% 59.41/59.45 inference(scs_inference,[],[23,3447,3592,3600,3212,3062,3083,280,1428,1443,3595,24,2,3,25,11,9,10,28,27])).
% 59.41/59.45 cnf(3613,plain,
% 59.41/59.45 (P1(f5(a3,a2),a4,a7)),
% 59.41/59.45 inference(scs_inference,[],[3434,24])).
% 59.41/59.45 cnf(3616,plain,
% 59.41/59.45 (~P1(a4,f5(a4,a3),a1)),
% 59.41/59.45 inference(scs_inference,[],[23,146,3434,3228,24,2,25])).
% 59.41/59.45 cnf(3617,plain,
% 59.41/59.45 (P1(a4,f5(a4,x36171),x36171)),
% 59.41/59.45 inference(rename_variables,[],[3228])).
% 59.41/59.45 cnf(3619,plain,
% 59.41/59.45 (~E(f5(a3,a4),a1)),
% 59.41/59.45 inference(scs_inference,[],[23,146,3434,3228,35,24,2,25,3])).
% 59.41/59.45 cnf(3621,plain,
% 59.41/59.45 (P1(f5(a4,a2),f5(a1,a4),f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[23,146,3586,3434,3228,1912,35,24,2,25,3,11])).
% 59.41/59.45 cnf(3624,plain,
% 59.41/59.45 (~P1(a3,f5(a4,a4),f5(a4,a1))),
% 59.41/59.45 inference(scs_inference,[],[23,146,3586,3599,3594,3434,3228,1912,280,1428,35,24,2,25,3,11,9,10])).
% 59.41/59.45 cnf(3625,plain,
% 59.41/59.45 (~P1(f6(a3),f5(a4,a1),f5(a4,a4))),
% 59.41/59.45 inference(scs_inference,[],[23,146,3586,3599,3594,3598,3434,3228,3617,1912,280,1428,19,35,24,2,25,3,11,9,10,28])).
% 59.41/59.45 cnf(3632,plain,
% 59.41/59.45 (P1(f5(a1,a4),f5(a4,a2),f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[3621,24])).
% 59.41/59.45 cnf(3635,plain,
% 59.41/59.45 (~E(f5(a4,a3),f5(a4,a1))),
% 59.41/59.45 inference(scs_inference,[],[1444,3621,1428,24,2,3])).
% 59.41/59.45 cnf(3636,plain,
% 59.41/59.45 (E(x36361,f5(a4,x36361))),
% 59.41/59.45 inference(rename_variables,[],[1428])).
% 59.41/59.45 cnf(3637,plain,
% 59.41/59.45 (~P1(f5(a4,a3),f5(a4,a4),a1)),
% 59.41/59.45 inference(scs_inference,[],[23,1444,3621,3299,1428,24,2,3,25])).
% 59.41/59.45 cnf(3640,plain,
% 59.41/59.45 (~P1(a4,f5(a4,a3),f5(a4,a1))),
% 59.41/59.45 inference(scs_inference,[],[23,1444,3621,3616,3299,1443,1428,24,2,3,25,11])).
% 59.41/59.45 cnf(3641,plain,
% 59.41/59.45 (E(f5(a4,x36411),x36411)),
% 59.41/59.45 inference(rename_variables,[],[1443])).
% 59.41/59.45 cnf(3644,plain,
% 59.41/59.45 (~P1(a4,a3,a1)),
% 59.41/59.45 inference(scs_inference,[],[23,1444,3621,3616,3299,1443,3641,1428,3636,24,2,3,25,11,9,10])).
% 59.41/59.45 cnf(3646,plain,
% 59.41/59.45 (P1(f5(a3,a2),f5(a4,a4),f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[23,1444,3621,3616,3613,3299,3131,2886,1443,3641,1428,3636,24,2,3,25,11,9,10,28])).
% 59.41/59.45 cnf(3649,plain,
% 59.41/59.45 (P1(f5(a4,a4),f5(a1,a2),f5(a3,a2))),
% 59.41/59.45 inference(scs_inference,[],[23,1444,3621,3616,3613,3381,3299,3131,2591,1678,2886,1443,3641,1428,3636,24,2,3,25,11,9,10,28,27])).
% 59.41/59.45 cnf(3662,plain,
% 59.41/59.45 (~E(f5(a4,a1),f5(a4,a3))),
% 59.41/59.45 inference(scs_inference,[],[3646,3635,24,2])).
% 59.41/59.45 cnf(3668,plain,
% 59.41/59.45 (P1(f6(a4),f5(a3,a2),f5(a1,a2))),
% 59.41/59.45 inference(scs_inference,[],[3588,3646,3635,3352,3228,1912,1463,24,2,25,13,11])).
% 59.41/59.45 cnf(3669,plain,
% 59.41/59.45 (P1(f5(a1,a2),f6(a2),f5(a4,a1))),
% 59.41/59.45 inference(scs_inference,[],[3588,3646,3635,3352,2571,3228,1912,1463,24,2,25,13,11,9])).
% 59.41/59.45 cnf(3673,plain,
% 59.41/59.45 (P1(f5(a4,a7),f6(a4),a7)),
% 59.41/59.45 inference(scs_inference,[],[3588,3644,3646,3635,3352,3252,2571,2501,3447,3228,1912,2717,1463,619,24,2,25,13,11,9,28,27])).
% 59.41/59.45 cnf(3685,plain,
% 59.41/59.45 (P1(f5(a1,a2),f5(a4,a4),f5(a3,a2))),
% 59.41/59.45 inference(scs_inference,[],[3649,24])).
% 59.41/59.45 cnf(3688,plain,
% 59.41/59.45 (~P1(f5(a1,a2),f6(a2),f5(a4,a3))),
% 59.41/59.45 inference(scs_inference,[],[3649,3662,3589,3669,24,2,25])).
% 59.41/59.45 cnf(3691,plain,
% 59.41/59.45 (E(f5(a4,x36911),x36911)),
% 59.41/59.45 inference(rename_variables,[],[1443])).
% 59.41/59.45 cnf(3700,plain,
% 59.41/59.45 (~P1(f5(a3,a4),f6(a4),a1)),
% 59.41/59.45 inference(scs_inference,[],[3649,3662,3624,3637,3589,3625,3669,3640,3602,2964,708,1393,1428,1443,3691,38,24,2,25,11,9,10,28,27])).
% 59.41/59.45 cnf(3730,plain,
% 59.41/59.45 ($false),
% 59.41/59.45 inference(scs_inference,[],[3632,3685,3619,3668,3688,3700,3673,1652,1846,3299,1600,1933,280,1912,24,2,25,11,9,10,28,27]),
% 59.41/59.45 ['proof']).
% 59.41/59.45 % SZS output end Proof
% 59.41/59.45 % Total time :58.810000s
%------------------------------------------------------------------------------