%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG005-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n016.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.25s 59.33s
% Output : CNFRefutation 59.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : RNG005-1 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n016.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jun 18 13:17:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.51/0.58 start to proof:theBenchmark
% 59.25/59.32 %-------------------------------------------
% 59.25/59.32 % File :CSE---1.7
% 59.25/59.32 % Problem :theBenchmark
% 59.25/59.32 % Transform :cnf
% 59.25/59.32 % Format :tptp:raw
% 59.25/59.32 % Command :java -jar mcs_scs.jar %d %s
% 59.25/59.32
% 59.25/59.32 % Result :Theorem 58.710000s
% 59.25/59.32 % Output :CNFRefutation 58.710000s
% 59.25/59.32 %-------------------------------------------
% 59.25/59.33 %--------------------------------------------------------------------------
% 59.25/59.33 % File : RNG005-1 : TPTP v8.2.0. Released v1.0.0.
% 59.25/59.33 % Domain : Ring Theory
% 59.25/59.33 % Problem : (-X*Y) + (X*Y) = additive_identity
% 59.25/59.33 % Version : [Wos65] axioms.
% 59.25/59.33 % English :
% 59.25/59.33
% 59.25/59.33 % Refs : [Wos65] Wos (1965), Unpublished Note
% 59.25/59.33 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 59.25/59.33 % Source : [SPRFN]
% 59.25/59.33 % Names : Problem 23 [Wos65]
% 59.25/59.33
% 59.25/59.33 % Status : Unsatisfiable
% 59.25/59.33 % Rating : 0.06 v8.2.0, 0.00 v7.4.0, 0.11 v7.3.0, 0.00 v6.0.0, 0.11 v5.5.0, 0.19 v5.4.0, 0.13 v5.3.0, 0.25 v5.2.0, 0.12 v5.1.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.2.1, 0.22 v2.2.0, 0.14 v2.1.0, 0.00 v2.0.0
% 59.25/59.33 % Syntax : Number of clauses : 20 ( 9 unt; 0 nHn; 14 RR)
% 59.25/59.33 % Number of literals : 53 ( 2 equ; 34 neg)
% 59.25/59.33 % Maximal clause size : 5 ( 2 avg)
% 59.25/59.33 % Maximal term depth : 2 ( 1 avg)
% 59.25/59.33 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 59.25/59.33 % Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% 59.25/59.33 % Number of variables : 71 ( 0 sgn)
% 59.25/59.33 % SPC : CNF_UNS_RFO_SEQ_HRN
% 59.25/59.33
% 59.25/59.33 % Comments : These are the same axioms as in [MOW76].
% 59.25/59.33 %--------------------------------------------------------------------------
% 59.25/59.33 %----Include ring theory axioms
% 59.25/59.33 include('Axioms/RNG001-0.ax').
% 59.25/59.33 %--------------------------------------------------------------------------
% 59.25/59.33 cnf(a_times_b,hypothesis,
% 59.25/59.33 product(a,b,d) ).
% 59.25/59.33
% 59.25/59.33 cnf(a_inverse_times_b,hypothesis,
% 59.25/59.33 product(additive_inverse(a),b,c) ).
% 59.25/59.33
% 59.25/59.33 cnf(prove_sum_is_additive_id,negated_conjecture,
% 59.25/59.33 ~ sum(c,d,additive_identity) ).
% 59.25/59.33
% 59.25/59.33 %--------------------------------------------------------------------------
% 59.25/59.33 %-------------------------------------------
% 59.25/59.33 % Proof found
% 59.25/59.33 % SZS status Theorem for theBenchmark
% 59.25/59.33 % SZS output start Proof
% 59.25/59.33 %ClaNum:34(EqnAxiom:14)
% 59.25/59.33 %VarNum:146(SingletonVarNum:71)
% 59.25/59.33 %MaxLitNum:5
% 59.25/59.33 %MaxfuncDepth:1
% 59.25/59.33 %SharedTerms:9
% 59.25/59.33 %goalClause: 23
% 59.25/59.33 %singleGoalClaCount:1
% 59.25/59.33 [15]P1(a1,a2,a6)
% 59.25/59.33 [23]~P2(a7,a6,a3)
% 59.25/59.33 [18]P1(f5(a1),a2,a7)
% 59.25/59.33 [16]P2(x161,a3,x161)
% 59.25/59.33 [17]P2(a3,x171,x171)
% 59.25/59.33 [19]P2(x191,f5(x191),a3)
% 59.25/59.33 [20]P2(f5(x201),x201,a3)
% 59.25/59.33 [21]P2(x211,x212,f4(x211,x212))
% 59.25/59.33 [22]P1(x221,x222,f8(x221,x222))
% 59.25/59.33 [24]~P2(x242,x241,x243)+P2(x241,x242,x243)
% 59.25/59.33 [25]~P2(x253,x254,x251)+E(x251,x252)+~P2(x253,x254,x252)
% 59.25/59.33 [26]~P1(x263,x264,x261)+E(x261,x262)+~P1(x263,x264,x262)
% 59.25/59.33 [27]~P2(x276,x274,x271)+P2(x271,x272,x273)+~P2(x274,x272,x275)+~P2(x276,x275,x273)
% 59.25/59.33 [28]~P2(x281,x286,x284)+P2(x281,x282,x283)+~P2(x284,x285,x283)+~P2(x286,x285,x282)
% 59.25/59.33 [29]~P1(x296,x294,x291)+P1(x291,x292,x293)+~P1(x294,x292,x295)+~P1(x296,x295,x293)
% 59.25/59.33 [30]~P1(x301,x306,x304)+P1(x301,x302,x303)+~P1(x304,x305,x303)+~P1(x306,x305,x302)
% 59.25/59.33 [31]~P1(x317,x315,x312)+~P1(x317,x314,x311)+P2(x311,x312,x313)+~P2(x314,x315,x316)+~P1(x317,x316,x313)
% 59.25/59.33 [32]~P1(x325,x327,x322)+~P1(x324,x327,x321)+P2(x321,x322,x323)+~P2(x324,x325,x326)+~P1(x326,x327,x323)
% 59.25/59.33 [33]~P1(x337,x332,x335)+~P1(x336,x332,x334)+P1(x331,x332,x333)+~P2(x334,x335,x333)+~P2(x336,x337,x331)
% 59.25/59.33 [34]~P1(x341,x347,x345)+~P1(x341,x346,x344)+P1(x341,x342,x343)+~P2(x344,x345,x343)+~P2(x346,x347,x342)
% 59.25/59.33 %EqnAxiom
% 59.25/59.33 [1]E(x11,x11)
% 59.25/59.33 [2]E(x22,x21)+~E(x21,x22)
% 59.25/59.33 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.25/59.33 [4]~E(x41,x42)+E(f5(x41),f5(x42))
% 59.25/59.33 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53))
% 59.25/59.33 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62))
% 59.25/59.33 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73))
% 59.25/59.33 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82))
% 59.25/59.33 [9]P1(x92,x93,x94)+~E(x91,x92)+~P1(x91,x93,x94)
% 59.25/59.33 [10]P1(x103,x102,x104)+~E(x101,x102)+~P1(x103,x101,x104)
% 59.25/59.33 [11]P1(x113,x114,x112)+~E(x111,x112)+~P1(x113,x114,x111)
% 59.25/59.33 [12]P2(x122,x123,x124)+~E(x121,x122)+~P2(x121,x123,x124)
% 59.25/59.33 [13]P2(x133,x132,x134)+~E(x131,x132)+~P2(x133,x131,x134)
% 59.33/59.33 [14]P2(x143,x144,x142)+~E(x141,x142)+~P2(x143,x144,x141)
% 59.33/59.33
% 59.33/59.33 %-------------------------------------------
% 59.33/59.35 cnf(35,plain,
% 59.33/59.35 (~P2(a6,a7,a3)),
% 59.33/59.35 inference(scs_inference,[],[23,24])).
% 59.33/59.35 cnf(37,plain,
% 59.33/59.35 (~E(f5(a6),a7)),
% 59.33/59.35 inference(scs_inference,[],[23,20,24,12])).
% 59.33/59.35 cnf(39,plain,
% 59.33/59.35 (E(x391,f4(x391,a3))),
% 59.33/59.35 inference(scs_inference,[],[23,16,21,20,24,12,25])).
% 59.33/59.35 cnf(40,plain,
% 59.33/59.35 (P2(x401,x402,f4(x401,x402))),
% 59.33/59.35 inference(rename_variables,[],[21])).
% 59.33/59.35 cnf(42,plain,
% 59.33/59.35 (P1(f4(x421,a3),x422,f8(x421,x422))),
% 59.33/59.35 inference(scs_inference,[],[23,16,21,22,20,24,12,25,9])).
% 59.33/59.35 cnf(43,plain,
% 59.33/59.35 (P1(x431,x432,f8(x431,x432))),
% 59.33/59.35 inference(rename_variables,[],[22])).
% 59.33/59.35 cnf(44,plain,
% 59.33/59.35 (P1(x441,f4(x442,a3),f8(x441,x442))),
% 59.33/59.35 inference(scs_inference,[],[23,16,21,22,43,20,24,12,25,9,10])).
% 59.33/59.35 cnf(45,plain,
% 59.33/59.35 (P1(x451,x452,f8(x451,x452))),
% 59.33/59.35 inference(rename_variables,[],[22])).
% 59.33/59.35 cnf(46,plain,
% 59.33/59.35 (P1(x461,x462,f4(f8(x461,x462),a3))),
% 59.33/59.35 inference(scs_inference,[],[23,16,21,22,43,45,20,24,12,25,9,10,11])).
% 59.33/59.35 cnf(48,plain,
% 59.33/59.35 (P2(a3,x481,x481)),
% 59.33/59.35 inference(rename_variables,[],[17])).
% 59.33/59.35 cnf(49,plain,
% 59.33/59.35 (P2(a3,f8(x491,x492),f4(f8(x491,x492),a3))),
% 59.33/59.35 inference(scs_inference,[],[23,16,17,48,21,22,43,45,20,24,12,25,9,10,11,13,14])).
% 59.33/59.35 cnf(51,plain,
% 59.33/59.35 (P2(f8(x511,x512),f4(a3,a3),f8(x511,x512))),
% 59.33/59.35 inference(scs_inference,[],[23,16,17,48,21,40,22,43,45,20,24,12,25,9,10,11,13,14,28])).
% 59.33/59.35 cnf(52,plain,
% 59.33/59.35 (P2(x521,x522,f4(x521,x522))),
% 59.33/59.35 inference(rename_variables,[],[21])).
% 59.33/59.35 cnf(54,plain,
% 59.33/59.35 (P2(x541,a3,x541)),
% 59.33/59.35 inference(rename_variables,[],[16])).
% 59.33/59.35 cnf(57,plain,
% 59.33/59.35 (P1(x571,x572,f8(x571,x572))),
% 59.33/59.35 inference(rename_variables,[],[22])).
% 59.33/59.35 cnf(59,plain,
% 59.33/59.35 (P2(f8(x591,a3),f8(x591,a3),f8(x591,a3))),
% 59.33/59.35 inference(scs_inference,[],[23,16,54,17,48,21,40,22,43,45,57,20,24,12,25,9,10,11,13,14,28,29,31])).
% 59.33/59.35 cnf(62,plain,
% 59.33/59.35 (P1(x621,x622,f8(x621,x622))),
% 59.33/59.35 inference(rename_variables,[],[22])).
% 59.33/59.35 cnf(63,plain,
% 59.33/59.35 (P2(x631,a3,x631)),
% 59.33/59.35 inference(rename_variables,[],[16])).
% 59.33/59.35 cnf(65,plain,
% 59.33/59.35 (P2(f8(a3,x651),f8(a3,x651),f8(a3,x651))),
% 59.33/59.35 inference(scs_inference,[],[23,16,54,63,17,48,21,40,22,43,45,57,62,20,24,12,25,9,10,11,13,14,28,29,31,32])).
% 59.33/59.35 cnf(68,plain,
% 59.33/59.35 (P1(x681,x682,f8(x681,x682))),
% 59.33/59.35 inference(rename_variables,[],[22])).
% 59.33/59.35 cnf(69,plain,
% 59.33/59.35 (P2(x691,a3,x691)),
% 59.33/59.35 inference(rename_variables,[],[16])).
% 59.33/59.35 cnf(71,plain,
% 59.33/59.35 (P1(a3,x711,f4(f8(a3,x711),f8(a3,x711)))),
% 59.33/59.35 inference(scs_inference,[],[23,16,54,63,69,17,48,21,40,52,22,43,45,57,62,68,20,24,12,25,9,10,11,13,14,28,29,31,32,33])).
% 59.33/59.35 cnf(72,plain,
% 59.33/59.35 (P2(x721,x722,f4(x721,x722))),
% 59.33/59.35 inference(rename_variables,[],[21])).
% 59.33/59.35 cnf(73,plain,
% 59.33/59.35 (P2(x731,a3,x731)),
% 59.33/59.35 inference(rename_variables,[],[16])).
% 59.33/59.35 cnf(75,plain,
% 59.33/59.35 (P1(x751,x752,f8(x751,x752))),
% 59.33/59.35 inference(rename_variables,[],[22])).
% 59.33/59.35 cnf(77,plain,
% 59.33/59.35 (P1(x771,a3,f4(f8(x771,a3),f8(x771,a3)))),
% 59.33/59.35 inference(scs_inference,[],[23,16,54,63,69,73,17,48,21,40,52,72,22,43,45,57,62,68,75,20,24,12,25,9,10,11,13,14,28,29,31,32,33,34])).
% 59.33/59.35 cnf(79,plain,
% 59.33/59.35 (P2(x791,a3,x791)),
% 59.33/59.35 inference(rename_variables,[],[16])).
% 59.33/59.35 cnf(81,plain,
% 59.33/59.35 (P1(x811,x812,f8(x811,x812))),
% 59.33/59.35 inference(rename_variables,[],[22])).
% 59.33/59.35 cnf(84,plain,
% 59.33/59.35 (E(f8(a3,x841),f4(f8(a3,x841),f8(a3,x841)))),
% 59.33/59.35 inference(scs_inference,[],[23,16,54,63,69,73,17,48,21,40,52,72,22,43,45,57,62,68,75,81,20,24,12,25,9,10,11,13,14,28,29,31,32,33,34,2,26])).
% 59.33/59.35 cnf(87,plain,
% 59.33/59.35 (~P2(a3,a6,f5(a7))),
% 59.33/59.35 inference(scs_inference,[],[23,16,54,63,69,73,79,17,48,21,40,52,72,22,43,45,57,62,68,75,81,19,20,24,12,25,9,10,11,13,14,28,29,31,32,33,34,2,26,27])).
% 59.33/59.35 cnf(96,plain,
% 59.33/59.35 (~P2(a6,a3,f5(a7))),
% 59.33/59.35 inference(scs_inference,[],[87,24])).
% 59.33/59.35 cnf(98,plain,
% 59.33/59.35 (E(f4(x981,a3),x981)),
% 59.33/59.35 inference(scs_inference,[],[87,39,24,2])).
% 59.33/59.35 cnf(99,plain,
% 59.33/59.35 (~E(f5(a6),f4(a7,a3))),
% 59.33/59.35 inference(scs_inference,[],[37,87,39,24,2,3])).
% 59.33/59.35 cnf(100,plain,
% 59.33/59.35 (E(f8(x1001,a3),f4(f8(x1001,a3),f8(x1001,a3)))),
% 59.33/59.35 inference(scs_inference,[],[59,37,87,39,21,24,2,3,25])).
% 59.33/59.35 cnf(101,plain,
% 59.33/59.35 (P2(x1011,x1012,f4(x1011,x1012))),
% 59.33/59.35 inference(rename_variables,[],[21])).
% 59.33/59.35 cnf(103,plain,
% 59.33/59.35 (P1(f4(a3,a3),x1031,f4(f8(a3,x1031),f8(a3,x1031)))),
% 59.33/59.35 inference(scs_inference,[],[59,37,87,42,39,84,21,24,2,3,25,11])).
% 59.33/59.35 cnf(105,plain,
% 59.33/59.35 (P2(f8(a3,x1051),f4(a3,a3),f4(f8(a3,x1051),f8(a3,x1051)))),
% 59.33/59.35 inference(scs_inference,[],[59,51,37,87,42,39,84,21,24,2,3,25,11,14])).
% 59.33/59.35 cnf(108,plain,
% 59.33/59.35 (P2(f8(x1081,a3),f8(x1081,a3),f8(x1081,a3))),
% 59.33/59.35 inference(rename_variables,[],[59])).
% 59.33/59.35 cnf(109,plain,
% 59.33/59.35 (E(f8(a3,x1091),f4(f8(a3,x1091),f8(a3,x1091)))),
% 59.33/59.35 inference(rename_variables,[],[84])).
% 59.33/59.35 cnf(110,plain,
% 59.33/59.35 (P2(f4(f8(a3,a3),f8(a3,a3)),f8(a3,a3),f8(a3,a3))),
% 59.33/59.35 inference(scs_inference,[],[59,108,51,37,87,42,39,84,109,21,24,2,3,25,11,14,13,12])).
% 59.33/59.35 cnf(111,plain,
% 59.33/59.35 (P2(f8(x1111,a3),f8(x1111,a3),f8(x1111,a3))),
% 59.33/59.35 inference(rename_variables,[],[59])).
% 59.33/59.35 cnf(113,plain,
% 59.33/59.35 (P2(f8(x1131,a3),f4(f8(x1131,a3),f8(x1131,a3)),f8(x1131,a3))),
% 59.33/59.35 inference(scs_inference,[],[59,108,111,51,37,87,42,39,84,109,21,101,24,2,3,25,11,14,13,12,28])).
% 59.33/59.35 cnf(116,plain,
% 59.33/59.35 (P2(f8(x1161,a3),f5(f8(x1161,a3)),f8(x1161,a3))),
% 59.33/59.35 inference(scs_inference,[],[59,108,111,51,37,87,42,39,84,109,21,101,19,16,24,2,3,25,11,14,13,12,28,27])).
% 59.33/59.35 cnf(120,plain,
% 59.33/59.35 (P1(x1201,x1202,f4(f8(x1201,a3),f8(x1201,a3)))+~E(a3,x1202)),
% 59.33/59.35 inference(scs_inference,[],[59,108,111,51,37,87,42,39,84,109,77,21,101,19,16,24,2,3,25,11,14,13,12,28,27,10])).
% 59.33/59.35 cnf(121,plain,
% 59.33/59.35 (P1(x1211,x1212,f4(f8(a3,x1212),f8(a3,x1212)))+~E(a3,x1211)),
% 59.33/59.35 inference(scs_inference,[],[59,108,111,51,37,87,42,39,84,109,71,77,21,101,19,16,24,2,3,25,11,14,13,12,28,27,10,9])).
% 59.33/59.35 cnf(132,plain,
% 59.33/59.35 (P1(x1321,f4(a3,a3),f4(f8(x1321,a3),f8(x1321,a3)))),
% 59.33/59.35 inference(scs_inference,[],[39,120])).
% 59.33/59.35 cnf(133,plain,
% 59.33/59.35 (E(x1331,f4(x1331,a3))),
% 59.33/59.35 inference(rename_variables,[],[39])).
% 59.33/59.35 cnf(134,plain,
% 59.33/59.35 (E(f4(f8(x1341,a3),f8(x1341,a3)),f8(x1341,a3))),
% 59.33/59.35 inference(scs_inference,[],[100,39,120,2])).
% 59.33/59.35 cnf(135,plain,
% 59.33/59.35 (E(f4(f8(a3,x1351),f8(a3,x1351)),f8(a3,x1351))),
% 59.33/59.35 inference(scs_inference,[],[103,100,42,39,120,2,26])).
% 59.33/59.35 cnf(138,plain,
% 59.33/59.35 (E(f8(x1381,a3),a3)),
% 59.33/59.35 inference(scs_inference,[],[116,103,100,42,39,19,120,2,26,25])).
% 59.33/59.35 cnf(141,plain,
% 59.33/59.35 (E(f4(f8(x1411,a3),a3),a3)),
% 59.33/59.35 inference(scs_inference,[],[116,103,98,100,42,39,19,120,2,26,25,3])).
% 59.33/59.35 cnf(142,plain,
% 59.33/59.35 (E(f4(x1421,a3),x1421)),
% 59.33/59.35 inference(rename_variables,[],[98])).
% 59.33/59.35 cnf(143,plain,
% 59.33/59.35 (P1(x1431,f4(x1432,a3),f8(f4(x1431,a3),x1432))),
% 59.33/59.35 inference(scs_inference,[],[116,103,44,98,142,100,42,39,19,120,2,26,25,3,9])).
% 59.33/59.35 cnf(145,plain,
% 59.33/59.35 (P1(f5(a1),a2,f4(a7,a3))),
% 59.33/59.35 inference(scs_inference,[],[116,103,44,98,142,100,18,42,39,133,19,120,2,26,25,3,9,11])).
% 59.33/59.35 cnf(146,plain,
% 59.33/59.35 (E(x1461,f4(x1461,a3))),
% 59.33/59.35 inference(rename_variables,[],[39])).
% 59.33/59.35 cnf(148,plain,
% 59.33/59.35 (P2(f8(x1481,x1482),f4(a3,a3),f8(x1481,x1482))),
% 59.33/59.35 inference(rename_variables,[],[51])).
% 59.33/59.35 cnf(149,plain,
% 59.33/59.35 (P1(f5(a1),f4(a2,a3),a7)),
% 59.33/59.35 inference(scs_inference,[],[116,51,103,44,98,142,100,18,42,39,133,146,19,120,2,26,25,3,9,11,14,10])).
% 59.33/59.35 cnf(151,plain,
% 59.33/59.35 (P2(f8(a3,x1511),a3,f4(f8(a3,x1511),f8(a3,x1511)))),
% 59.33/59.35 inference(scs_inference,[],[116,51,103,44,98,142,105,100,18,42,39,133,146,19,120,2,26,25,3,9,11,14,10,13])).
% 59.33/59.35 cnf(153,plain,
% 59.33/59.35 (P2(f4(f8(x1531,a3),f8(x1531,a3)),f4(a3,a3),f8(x1531,a3))),
% 59.33/59.35 inference(scs_inference,[],[116,51,148,103,44,98,142,105,100,18,42,39,133,146,19,120,2,26,25,3,9,11,14,10,13,12])).
% 59.33/59.35 cnf(155,plain,
% 59.33/59.35 (P2(f8(a3,x1551),f4(f8(a3,x1551),f8(a3,x1551)),f8(a3,x1551))),
% 59.33/59.35 inference(scs_inference,[],[65,116,51,148,103,44,98,142,105,100,18,42,39,133,146,21,19,120,2,26,25,3,9,11,14,10,13,12,28])).
% 59.33/59.35 cnf(158,plain,
% 59.33/59.35 (P2(a3,f8(a3,x1581),a3)),
% 59.33/59.35 inference(scs_inference,[],[65,116,51,148,103,44,98,142,105,100,18,42,39,133,146,20,21,19,120,2,26,25,3,9,11,14,10,13,12,28,27])).
% 59.33/59.35 cnf(170,plain,
% 59.33/59.35 (E(a3,f8(x1701,a3))),
% 59.33/59.35 inference(scs_inference,[],[138,2])).
% 59.33/59.35 cnf(171,plain,
% 59.33/59.35 (E(a3,f8(a3,x1711))),
% 59.33/59.35 inference(scs_inference,[],[158,138,17,2,25])).
% 59.33/59.35 cnf(172,plain,
% 59.33/59.35 (P2(a3,x1721,x1721)),
% 59.33/59.35 inference(rename_variables,[],[17])).
% 59.33/59.35 cnf(174,plain,
% 59.33/59.35 (E(f4(f8(x1741,a3),f8(x1741,a3)),a3)),
% 59.33/59.35 inference(scs_inference,[],[158,134,138,17,2,25,3])).
% 59.33/59.35 cnf(175,plain,
% 59.33/59.35 (E(f8(x1751,a3),a3)),
% 59.33/59.35 inference(rename_variables,[],[138])).
% 59.33/59.35 cnf(176,plain,
% 59.33/59.35 (P1(f4(f5(a1),a3),a2,f4(a7,a3))),
% 59.33/59.35 inference(scs_inference,[],[158,134,145,138,17,39,2,25,3,9])).
% 59.33/59.35 cnf(178,plain,
% 59.33/59.35 (P1(x1781,a3,a3)),
% 59.33/59.35 inference(scs_inference,[],[158,134,46,145,138,141,17,39,2,25,3,9,11])).
% 59.33/59.35 cnf(180,plain,
% 59.33/59.35 (P2(f8(a3,a3),f8(a3,a3),a3)),
% 59.33/59.35 inference(scs_inference,[],[65,158,134,46,145,138,175,141,17,39,2,25,3,9,11,14])).
% 59.33/59.35 cnf(182,plain,
% 59.33/59.35 (E(f8(x1821,a3),a3)),
% 59.33/59.35 inference(rename_variables,[],[138])).
% 59.33/59.35 cnf(183,plain,
% 59.33/59.35 (P1(x1831,a3,f8(f4(x1831,a3),f8(x1832,a3)))),
% 59.33/59.35 inference(scs_inference,[],[65,158,134,46,143,145,138,175,141,17,39,2,25,3,9,11,14,10])).
% 59.33/59.35 cnf(185,plain,
% 59.33/59.35 (P2(f4(f8(a3,a3),f8(a3,a3)),a3,f8(a3,a3))),
% 59.33/59.35 inference(scs_inference,[],[65,110,158,134,46,143,145,138,175,182,141,17,39,2,25,3,9,11,14,10,13])).
% 59.33/59.35 cnf(186,plain,
% 59.33/59.35 (E(f8(x1861,a3),a3)),
% 59.33/59.35 inference(rename_variables,[],[138])).
% 59.33/59.35 cnf(187,plain,
% 59.33/59.35 (P2(a3,f4(f8(x1871,a3),f8(x1871,a3)),f8(x1871,a3))),
% 59.33/59.35 inference(scs_inference,[],[65,110,113,158,134,46,143,145,138,175,182,186,141,17,39,2,25,3,9,11,14,10,13,12])).
% 59.33/59.35 cnf(189,plain,
% 59.33/59.35 (P2(f8(a3,a3),f4(f8(a3,a3),a3),f8(a3,a3))),
% 59.33/59.35 inference(scs_inference,[],[65,110,113,158,134,46,143,49,151,145,138,175,182,186,141,17,39,2,25,3,9,11,14,10,13,12,28])).
% 59.33/59.35 cnf(193,plain,
% 59.33/59.35 (~P2(f8(a3,x1931),a6,f5(a7))),
% 59.33/59.35 inference(scs_inference,[],[87,65,110,113,158,134,46,143,49,151,145,138,175,182,186,141,17,172,39,2,25,3,9,11,14,10,13,12,28,27])).
% 59.33/59.35 cnf(196,plain,
% 59.33/59.35 (P1(f8(x1961,a3),x1962,f4(f8(a3,x1962),f8(a3,x1962)))),
% 59.33/59.35 inference(scs_inference,[],[87,65,110,113,158,134,46,143,49,151,145,138,175,182,186,141,17,172,39,2,25,3,9,11,14,10,13,12,28,27,121])).
% 59.33/59.35 cnf(197,plain,
% 59.33/59.35 (P1(x1971,f8(x1972,a3),f4(f8(x1971,a3),f8(x1971,a3)))),
% 59.33/59.35 inference(scs_inference,[],[87,65,110,113,158,134,46,143,49,151,145,138,175,182,186,141,17,172,39,2,25,3,9,11,14,10,13,12,28,27,121,120])).
% 59.33/59.35 cnf(208,plain,
% 59.33/59.35 (P1(x2081,f8(a3,x2082),f4(f8(x2081,a3),f8(x2081,a3)))),
% 59.33/59.35 inference(scs_inference,[],[171,121,120])).
% 59.33/59.35 cnf(210,plain,
% 59.33/59.35 (E(f8(x2101,x2102),f8(f4(x2101,a3),x2102))),
% 59.33/59.35 inference(scs_inference,[],[44,174,171,143,121,120,2,26])).
% 59.33/59.35 cnf(213,plain,
% 59.33/59.35 (E(f4(f5(x2131),x2131),a3)),
% 59.33/59.35 inference(scs_inference,[],[44,174,171,143,21,20,121,120,2,26,25])).
% 59.33/59.35 cnf(217,plain,
% 59.33/59.35 (E(f4(f8(x2171,a3),f8(x2171,a3)),f8(x2172,a3))),
% 59.33/59.36 inference(scs_inference,[],[44,174,170,171,143,21,20,121,120,2,26,25,3])).
% 59.33/59.36 cnf(218,plain,
% 59.33/59.36 (P1(f4(f5(a1),a3),f4(a2,a3),a7)),
% 59.33/59.36 inference(scs_inference,[],[44,174,170,171,149,143,39,21,20,121,120,2,26,25,3,9])).
% 59.33/59.36 cnf(220,plain,
% 59.33/59.36 (P1(x2201,f4(a3,a3),a3)),
% 59.33/59.36 inference(scs_inference,[],[44,174,170,171,149,143,138,39,21,20,121,120,2,26,25,3,9,11])).
% 59.33/59.36 cnf(221,plain,
% 59.33/59.36 (P1(x2211,f4(x2212,a3),f8(x2211,x2212))),
% 59.33/59.36 inference(rename_variables,[],[44])).
% 59.33/59.36 cnf(225,plain,
% 59.33/59.36 (P2(f4(f8(x2251,a3),f8(x2251,a3)),a3,f8(x2251,a3))),
% 59.33/59.36 inference(scs_inference,[],[189,153,44,183,174,170,171,149,143,98,138,39,21,20,121,120,2,26,25,3,9,11,14,10,13])).
% 59.33/59.36 cnf(227,plain,
% 59.33/59.36 (P2(f8(x2271,a3),f4(f8(x2272,a3),f8(x2272,a3)),f8(x2272,a3))),
% 59.33/59.36 inference(scs_inference,[],[189,153,187,44,183,174,170,171,149,143,98,138,39,21,20,121,120,2,26,25,3,9,11,14,10,13,12])).
% 59.33/59.36 cnf(228,plain,
% 59.33/59.36 (P1(x2281,a3,f4(f8(a3,a3),f8(a3,a3)))),
% 59.33/59.36 inference(scs_inference,[],[189,153,187,44,221,196,183,174,170,171,178,149,143,98,138,39,21,20,121,120,2,26,25,3,9,11,14,10,13,12,30])).
% 59.33/59.36 cnf(229,plain,
% 59.33/59.36 (P1(x2291,a3,a3)),
% 59.33/59.36 inference(rename_variables,[],[178])).
% 59.33/59.36 cnf(230,plain,
% 59.33/59.36 (P1(x2301,f4(x2302,a3),f8(x2301,x2302))),
% 59.33/59.36 inference(rename_variables,[],[44])).
% 59.33/59.36 cnf(235,plain,
% 59.33/59.36 (P1(x2351,a3,a3)),
% 59.33/59.36 inference(rename_variables,[],[178])).
% 59.33/59.36 cnf(237,plain,
% 59.33/59.36 (P2(f8(a3,a3),a3,a3)),
% 59.33/59.36 inference(scs_inference,[],[189,153,187,158,44,221,230,196,180,183,174,170,171,178,229,149,143,98,138,39,21,20,121,120,2,26,25,3,9,11,14,10,13,12,30,29,28])).
% 59.33/59.36 cnf(238,plain,
% 59.33/59.36 (P2(a3,f8(a3,x2381),a3)),
% 59.33/59.36 inference(rename_variables,[],[158])).
% 59.33/59.36 cnf(242,plain,
% 59.33/59.36 (P1(f8(a3,a3),a3,f8(a3,a3))),
% 59.33/59.36 inference(scs_inference,[],[189,153,187,158,238,44,221,230,196,180,185,183,174,170,171,178,229,235,149,143,98,138,39,21,20,121,120,2,26,25,3,9,11,14,10,13,12,30,29,28,27,33])).
% 59.33/59.36 cnf(252,plain,
% 59.33/59.36 (E(f8(x2521,x2522),f8(x2521,f4(x2522,a3)))),
% 59.33/59.36 inference(scs_inference,[],[44,210,22,2,26])).
% 59.33/59.36 cnf(255,plain,
% 59.33/59.36 (E(f4(f5(x2551),x2551),f8(a3,x2552))),
% 59.33/59.36 inference(scs_inference,[],[44,210,213,22,171,2,26,3])).
% 59.33/59.36 cnf(256,plain,
% 59.33/59.36 (P1(f8(f4(a3,a3),a3),a3,f8(a3,a3))),
% 59.33/59.36 inference(scs_inference,[],[44,210,242,213,22,171,2,26,3,9])).
% 59.33/59.36 cnf(257,plain,
% 59.33/59.36 (E(f8(x2571,x2572),f8(f4(x2571,a3),x2572))),
% 59.33/59.36 inference(rename_variables,[],[210])).
% 59.33/59.36 cnf(258,plain,
% 59.33/59.36 (P1(a3,f8(x2581,a3),f8(a3,a3))),
% 59.33/59.36 inference(scs_inference,[],[44,210,135,197,242,213,22,171,2,26,3,9,11])).
% 59.33/59.36 cnf(262,plain,
% 59.33/59.36 (P2(f8(a3,x2621),f8(a3,x2621),f8(a3,x2621))),
% 59.33/59.36 inference(rename_variables,[],[65])).
% 59.33/59.36 cnf(263,plain,
% 59.33/59.36 (E(f8(x2631,x2632),f8(f4(x2631,a3),x2632))),
% 59.33/59.36 inference(rename_variables,[],[210])).
% 59.33/59.36 cnf(265,plain,
% 59.33/59.36 (P2(f8(a3,x2651),f8(a3,x2651),f8(a3,x2651))),
% 59.33/59.36 inference(rename_variables,[],[65])).
% 59.33/59.36 cnf(266,plain,
% 59.33/59.36 (E(f8(x2661,x2662),f8(f4(x2661,a3),x2662))),
% 59.33/59.36 inference(rename_variables,[],[210])).
% 59.33/59.36 cnf(267,plain,
% 59.33/59.36 (P1(x2671,a3,f8(x2671,f5(a3)))),
% 59.33/59.36 inference(scs_inference,[],[65,262,44,210,257,263,135,197,242,213,22,171,2,26,3,9,11,14,12,10])).
% 59.33/59.36 cnf(268,plain,
% 59.33/59.36 (P1(x2681,f4(x2682,a3),f8(x2681,x2682))),
% 59.33/59.36 inference(rename_variables,[],[44])).
% 59.33/59.36 cnf(271,plain,
% 59.33/59.36 (P2(f8(a3,x2711),f8(a3,x2711),f8(a3,x2711))),
% 59.33/59.36 inference(rename_variables,[],[65])).
% 59.33/59.36 cnf(273,plain,
% 59.33/59.36 (P1(f4(a3,a3),f8(f4(a3,a3),a3),a3)),
% 59.33/59.36 inference(scs_inference,[],[65,262,265,44,268,210,257,263,266,135,197,220,242,213,22,171,2,26,3,9,11,14,12,10,13,30])).
% 59.33/59.36 cnf(274,plain,
% 59.33/59.36 (P1(x2741,f4(x2742,a3),f8(x2741,x2742))),
% 59.33/59.36 inference(rename_variables,[],[44])).
% 59.33/59.36 cnf(275,plain,
% 59.33/59.36 (P1(x2751,f4(x2752,a3),f8(x2751,x2752))),
% 59.33/59.36 inference(rename_variables,[],[44])).
% 59.33/59.36 cnf(278,plain,
% 59.33/59.36 (P1(f8(x2781,a3),x2782,f4(f8(x2781,a3),f8(x2781,a3)))),
% 59.33/59.36 inference(scs_inference,[],[65,262,265,44,268,275,210,257,263,266,135,197,208,220,242,213,22,42,171,2,26,3,9,11,14,12,10,13,30,29])).
% 59.33/59.36 cnf(280,plain,
% 59.33/59.36 (P1(x2801,f4(x2802,a3),f8(x2801,x2802))),
% 59.33/59.36 inference(rename_variables,[],[44])).
% 59.33/59.36 cnf(287,plain,
% 59.33/59.36 (P2(f8(x2871,a3),f8(a3,x2872),f8(x2871,a3))),
% 59.33/59.36 inference(scs_inference,[],[65,262,265,271,227,158,44,268,275,210,257,263,266,135,197,208,220,242,225,213,22,42,171,2,26,3,9,11,14,12,10,13,30,29,28,27])).
% 59.33/59.36 cnf(289,plain,
% 59.33/59.36 (P1(f8(x2891,a3),f8(x2891,a3),f8(x2891,a3))),
% 59.33/59.36 inference(scs_inference,[],[65,262,265,271,227,187,158,44,268,275,210,257,263,266,135,197,208,220,242,225,213,22,178,42,171,2,26,3,9,11,14,12,10,13,30,29,28,27,34])).
% 59.33/59.36 cnf(293,plain,
% 59.33/59.36 (P2(f8(x2931,x2932),f8(x2931,x2932),f8(x2931,x2933))+~P2(f4(x2932,a3),f4(x2932,a3),f4(x2933,a3))),
% 59.33/59.36 inference(scs_inference,[],[65,262,265,271,227,187,158,44,268,275,280,274,210,257,263,266,135,197,208,220,242,225,213,22,178,42,171,2,26,3,9,11,14,12,10,13,30,29,28,27,34,31])).
% 59.33/59.36 cnf(299,plain,
% 59.33/59.36 (E(f8(a3,x2991),a3)),
% 59.33/59.36 inference(scs_inference,[],[171,2])).
% 59.33/59.36 cnf(300,plain,
% 59.33/59.36 (E(f4(a3,a3),f8(x3001,a3))),
% 59.33/59.36 inference(scs_inference,[],[170,171,98,2,3])).
% 59.33/59.36 cnf(303,plain,
% 59.33/59.36 (E(x3031,f4(x3031,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(304,plain,
% 59.33/59.36 (P1(f8(x3041,a3),f4(x3042,a3),f8(a3,x3042))),
% 59.33/59.36 inference(scs_inference,[],[170,171,39,44,98,2,3,11,9])).
% 59.33/59.36 cnf(305,plain,
% 59.33/59.36 (P1(x3051,f4(x3052,a3),f8(x3051,x3052))),
% 59.33/59.36 inference(rename_variables,[],[44])).
% 59.33/59.36 cnf(307,plain,
% 59.33/59.36 (E(x3071,f4(x3071,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(309,plain,
% 59.33/59.36 (E(x3091,f4(x3091,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(310,plain,
% 59.33/59.36 (P1(x3101,f4(f4(x3102,a3),a3),f8(x3101,x3102))),
% 59.33/59.36 inference(scs_inference,[],[59,170,171,39,303,307,309,44,305,98,2,3,11,9,14,12,10])).
% 59.33/59.36 cnf(311,plain,
% 59.33/59.36 (E(x3111,f4(x3111,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(319,plain,
% 59.33/59.36 (P1(f8(x3191,a3),f8(x3191,a3),f8(x3191,a3))),
% 59.33/59.36 inference(rename_variables,[],[289])).
% 59.33/59.36 cnf(321,plain,
% 59.33/59.36 (P2(f4(f8(a3,a3),f8(a3,a3)),a3,a3)),
% 59.33/59.36 inference(scs_inference,[],[110,59,237,170,171,39,303,307,309,311,44,305,278,289,256,228,273,98,2,3,11,9,14,12,10,13,30,29,28])).
% 59.33/59.36 cnf(323,plain,
% 59.33/59.36 (P2(a3,f4(f8(a3,x3231),f8(a3,x3231)),a3)),
% 59.33/59.36 inference(scs_inference,[],[155,110,59,237,158,170,171,39,303,307,309,311,44,305,278,289,256,228,273,98,2,3,11,9,14,12,10,13,30,29,28,27])).
% 59.33/59.36 cnf(326,plain,
% 59.33/59.36 (P1(a3,f8(a3,a3),a3)),
% 59.33/59.36 inference(scs_inference,[],[155,110,59,237,158,170,171,39,303,307,309,311,44,305,278,289,319,256,228,273,180,98,2,3,11,9,14,12,10,13,30,29,28,27,33])).
% 59.33/59.36 cnf(334,plain,
% 59.33/59.36 (E(f8(x3341,f4(x3342,a3)),f8(x3341,x3342))),
% 59.33/59.36 inference(scs_inference,[],[252,2])).
% 59.33/59.36 cnf(335,plain,
% 59.33/59.36 (E(f8(f4(x3351,a3),f4(x3352,a3)),f8(x3351,x3352))),
% 59.33/59.36 inference(scs_inference,[],[143,252,310,2,26])).
% 59.33/59.36 cnf(340,plain,
% 59.33/59.36 (P1(x3401,f4(a3,a3),f4(f8(x3401,a3),f8(x3401,a3)))),
% 59.33/59.36 inference(rename_variables,[],[132])).
% 59.33/59.36 cnf(341,plain,
% 59.33/59.36 (E(f8(a3,x3411),f8(a3,x3412))),
% 59.33/59.36 inference(scs_inference,[],[171,132,143,252,310,299,2,26,9,3])).
% 59.33/59.36 cnf(342,plain,
% 59.33/59.36 (P1(x3421,f4(a3,a3),f8(a3,x3422))),
% 59.33/59.36 inference(scs_inference,[],[171,132,220,143,252,310,299,2,26,9,3,11])).
% 59.33/59.36 cnf(344,plain,
% 59.33/59.36 (E(x3441,f4(x3441,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(345,plain,
% 59.33/59.36 (P2(f8(a3,x3451),f4(f8(x3452,a3),f8(x3452,a3)),f8(x3452,a3))),
% 59.33/59.36 inference(scs_inference,[],[187,51,171,39,132,220,143,252,310,299,2,26,9,3,11,14,12])).
% 59.33/59.36 cnf(347,plain,
% 59.33/59.36 (E(x3471,f4(x3471,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(350,plain,
% 59.33/59.36 (P1(x3501,f8(f4(a3,a3),f4(a3,a3)),a3)),
% 59.33/59.36 inference(scs_inference,[],[187,51,171,39,344,347,132,340,220,143,22,252,310,299,2,26,9,3,11,14,12,10,13,30])).
% 59.33/59.36 cnf(354,plain,
% 59.33/59.36 (P2(f8(x3541,a3),f8(x3542,a3),f8(x3542,a3))),
% 59.33/59.36 inference(scs_inference,[],[59,227,187,51,171,39,344,347,132,340,220,143,22,252,310,299,2,26,9,3,11,14,12,10,13,30,28])).
% 59.33/59.36 cnf(375,plain,
% 59.33/59.36 (E(f8(x3751,x3752),f8(f4(x3751,a3),f4(x3752,a3)))),
% 59.33/59.36 inference(scs_inference,[],[335,2])).
% 59.33/59.36 cnf(376,plain,
% 59.33/59.36 (E(f5(a3),a3)),
% 59.33/59.36 inference(scs_inference,[],[16,20,335,2,25])).
% 59.33/59.36 cnf(380,plain,
% 59.33/59.36 (E(f8(x3801,a3),f8(f8(x3801,a3),f8(x3801,a3)))),
% 59.33/59.36 inference(scs_inference,[],[16,289,20,22,335,2,25,26])).
% 59.33/59.36 cnf(381,plain,
% 59.33/59.36 (P1(x3811,x3812,f8(x3811,x3812))),
% 59.33/59.36 inference(rename_variables,[],[22])).
% 59.33/59.36 cnf(384,plain,
% 59.33/59.36 (E(x3841,f4(x3841,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(385,plain,
% 59.33/59.36 (E(f8(a3,x3851),f8(x3852,a3))),
% 59.33/59.36 inference(scs_inference,[],[170,16,289,20,39,22,335,299,2,25,26,11,3])).
% 59.33/59.36 cnf(387,plain,
% 59.33/59.36 (E(x3871,f4(x3871,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(389,plain,
% 59.33/59.36 (E(x3891,f4(x3891,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(391,plain,
% 59.33/59.36 (E(x3911,f4(x3911,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(393,plain,
% 59.33/59.36 (E(x3931,f4(x3931,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(396,plain,
% 59.33/59.36 (P1(f8(x3961,a3),f8(a3,x3962),f8(a3,x3962))),
% 59.33/59.36 inference(scs_inference,[],[65,170,16,289,304,20,39,384,387,389,391,393,22,335,299,2,25,26,11,3,9,14,12,10,13,30])).
% 59.33/59.36 cnf(397,plain,
% 59.33/59.36 (P1(f8(x3971,a3),f4(x3972,a3),f8(a3,x3972))),
% 59.33/59.36 inference(rename_variables,[],[304])).
% 59.33/59.36 cnf(408,plain,
% 59.33/59.36 (P2(f8(a3,x4081),f8(a3,x4081),f8(a3,x4081))),
% 59.33/59.36 inference(rename_variables,[],[65])).
% 59.33/59.36 cnf(410,plain,
% 59.33/59.36 (P2(f8(a3,x4101),f8(a3,x4101),f8(f8(a3,a3),x4101))),
% 59.33/59.36 inference(scs_inference,[],[65,408,187,321,170,16,289,304,397,20,39,384,387,389,391,393,22,381,44,335,258,299,2,25,26,11,3,9,14,12,10,13,30,29,28,31,32])).
% 59.33/59.36 cnf(427,plain,
% 59.33/59.36 (E(f8(a3,x4271),f4(f5(x4272),x4272))),
% 59.33/59.36 inference(scs_inference,[],[255,2])).
% 59.33/59.36 cnf(428,plain,
% 59.33/59.36 (E(f8(a3,x4281),f8(f8(x4282,a3),x4281))),
% 59.33/59.36 inference(scs_inference,[],[304,44,255,2,26])).
% 59.33/59.36 cnf(431,plain,
% 59.33/59.36 (E(f5(a3),f8(x4311,a3))),
% 59.33/59.36 inference(scs_inference,[],[170,304,44,255,376,2,26,3])).
% 59.33/59.36 cnf(433,plain,
% 59.33/59.36 (E(x4331,f4(x4331,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(434,plain,
% 59.33/59.36 (P1(f4(f8(x4341,a3),a3),f4(x4342,a3),f8(a3,x4342))),
% 59.33/59.36 inference(scs_inference,[],[170,304,39,433,44,255,376,2,26,3,11,9])).
% 59.33/59.36 cnf(435,plain,
% 59.33/59.36 (E(x4351,f4(x4351,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(437,plain,
% 59.33/59.36 (E(x4371,f4(x4371,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(438,plain,
% 59.33/59.36 (P2(f4(f8(x4381,a3),a3),f8(a3,x4382),f8(x4381,a3))),
% 59.33/59.36 inference(scs_inference,[],[287,170,304,39,433,435,437,44,255,376,2,26,3,11,9,14,12])).
% 59.33/59.36 cnf(439,plain,
% 59.33/59.36 (E(x4391,f4(x4391,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(441,plain,
% 59.33/59.36 (E(x4411,f4(x4411,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(444,plain,
% 59.33/59.36 (P1(f8(x4441,a3),f8(f8(x4441,a3),f8(x4441,a3)),f8(x4441,a3))),
% 59.33/59.36 inference(scs_inference,[],[287,170,289,304,39,433,435,437,439,441,22,44,255,376,2,26,3,11,9,14,12,10,13,30])).
% 59.33/59.36 cnf(447,plain,
% 59.33/59.36 (P2(f8(a3,x4471),f8(x4472,a3),f8(x4472,a3))),
% 59.33/59.36 inference(scs_inference,[],[65,287,345,170,289,304,39,433,435,437,439,441,22,44,255,376,2,26,3,11,9,14,12,10,13,30,28])).
% 59.33/59.36 cnf(450,plain,
% 59.33/59.36 (P2(f8(a3,a3),a3,f8(x4501,a3))),
% 59.33/59.36 inference(scs_inference,[],[227,65,287,345,321,170,16,289,304,39,433,435,437,439,441,22,44,255,376,2,26,3,11,9,14,12,10,13,30,28,27])).
% 59.33/59.36 cnf(454,plain,
% 59.33/59.36 (P2(f8(a3,a3),f8(a3,a3),f8(a3,x4541))),
% 59.33/59.36 inference(scs_inference,[],[227,65,287,345,321,170,16,289,304,39,433,435,437,439,441,22,44,342,255,376,2,26,3,11,9,14,12,10,13,30,28,27,32])).
% 59.33/59.36 cnf(474,plain,
% 59.33/59.36 (E(f8(x4741,a3),f4(a3,a3))),
% 59.33/59.36 inference(scs_inference,[],[300,2])).
% 59.33/59.36 cnf(479,plain,
% 59.33/59.36 (E(x4791,f4(x4791,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(481,plain,
% 59.33/59.36 (E(x4811,f4(x4811,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(482,plain,
% 59.33/59.36 (E(f5(a3),f8(a3,x4821))),
% 59.33/59.36 inference(scs_inference,[],[450,171,16,39,479,396,300,376,2,25,11,9,3])).
% 59.33/59.36 cnf(484,plain,
% 59.33/59.36 (E(x4841,f4(x4841,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(486,plain,
% 59.33/59.36 (E(x4861,f4(x4861,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(488,plain,
% 59.33/59.36 (E(x4881,f4(x4881,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(502,plain,
% 59.33/59.36 (P1(f8(a3,x5021),f8(a3,a3),f8(a3,x5021))),
% 59.33/59.36 inference(scs_inference,[],[227,354,454,410,438,450,171,16,289,39,479,481,484,486,488,396,278,300,376,2,25,11,9,3,14,12,10,13,30,27,28,33])).
% 59.33/59.36 cnf(514,plain,
% 59.33/59.36 (E(f8(a3,x5141),f8(f8(x5142,a3),f4(x5141,a3)))),
% 59.33/59.36 inference(scs_inference,[],[304,22,380,2,26])).
% 59.33/59.36 cnf(515,plain,
% 59.33/59.36 (P1(x5151,x5152,f8(x5151,x5152))),
% 59.33/59.36 inference(rename_variables,[],[22])).
% 59.33/59.36 cnf(517,plain,
% 59.33/59.36 (P1(f8(x5171,a3),x5172,f8(a3,x5172))),
% 59.33/59.36 inference(scs_inference,[],[170,304,22,515,380,2,26,9])).
% 59.33/59.36 cnf(518,plain,
% 59.33/59.36 (P1(x5181,x5182,f8(x5181,x5182))),
% 59.33/59.36 inference(rename_variables,[],[22])).
% 59.33/59.36 cnf(521,plain,
% 59.33/59.36 (P1(x5211,a3,f8(x5212,a3))),
% 59.33/59.36 inference(scs_inference,[],[170,304,22,515,178,375,380,2,26,9,3,11])).
% 59.33/59.36 cnf(522,plain,
% 59.33/59.36 (P2(a3,f8(a3,x5221),f8(x5222,a3))),
% 59.33/59.36 inference(scs_inference,[],[158,170,304,22,515,178,375,380,2,26,9,3,11,14])).
% 59.33/59.36 cnf(523,plain,
% 59.33/59.36 (P2(f4(f8(x5231,x5232),a3),f4(a3,a3),f8(x5231,x5232))),
% 59.33/59.36 inference(scs_inference,[],[51,158,170,304,22,515,178,39,375,380,2,26,9,3,11,14,12])).
% 59.33/59.36 cnf(524,plain,
% 59.33/59.36 (E(x5241,f4(x5241,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(525,plain,
% 59.33/59.36 (P1(x5251,f8(x5252,a3),f8(x5251,a3))),
% 59.33/59.36 inference(scs_inference,[],[51,158,170,304,22,515,518,178,39,375,380,2,26,9,3,11,14,12,10])).
% 59.33/59.36 cnf(526,plain,
% 59.33/59.36 (P1(x5261,x5262,f8(x5261,x5262))),
% 59.33/59.36 inference(rename_variables,[],[22])).
% 59.33/59.36 cnf(529,plain,
% 59.33/59.36 (P1(f8(a3,x5291),x5292,f4(f8(x5293,a3),f8(x5293,a3)))),
% 59.33/59.36 inference(scs_inference,[],[51,158,170,304,22,515,518,526,178,39,524,278,375,380,2,26,9,3,11,14,12,10,13,29])).
% 59.33/59.36 cnf(530,plain,
% 59.33/59.36 (P1(f8(x5301,a3),x5302,f4(f8(x5301,a3),f8(x5301,a3)))),
% 59.33/59.36 inference(rename_variables,[],[278])).
% 59.33/59.36 cnf(531,plain,
% 59.33/59.36 (P1(x5311,x5312,f8(x5311,x5312))),
% 59.33/59.36 inference(rename_variables,[],[22])).
% 59.33/59.36 cnf(533,plain,
% 59.33/59.36 (P2(a3,a3,f8(x5331,a3))),
% 59.33/59.36 inference(scs_inference,[],[187,51,158,450,321,170,304,22,515,518,526,178,39,524,278,375,380,2,26,9,3,11,14,12,10,13,29,28])).
% 59.33/59.36 cnf(534,plain,
% 59.33/59.36 (P2(a3,f4(f8(x5341,a3),f8(x5341,a3)),f8(x5341,a3))),
% 59.33/59.36 inference(rename_variables,[],[187])).
% 59.33/59.36 cnf(537,plain,
% 59.33/59.36 (P1(x5371,x5372,f8(x5371,x5372))),
% 59.33/59.36 inference(rename_variables,[],[22])).
% 59.33/59.36 cnf(539,plain,
% 59.33/59.36 (P1(f8(x5391,a3),f4(x5392,a3),f8(a3,x5392))),
% 59.33/59.36 inference(rename_variables,[],[304])).
% 59.33/59.36 cnf(542,plain,
% 59.33/59.36 (P2(x5421,x5422,f4(x5421,x5422))),
% 59.33/59.36 inference(rename_variables,[],[21])).
% 59.33/59.36 cnf(556,plain,
% 59.33/59.36 (P1(f8(x5561,a3),f4(x5562,a3),f8(a3,x5562))),
% 59.33/59.36 inference(rename_variables,[],[304])).
% 59.33/59.36 cnf(559,plain,
% 59.33/59.36 (P1(f8(x5591,a3),f4(a3,a3),f8(x5591,a3))),
% 59.33/59.36 inference(scs_inference,[],[187,534,65,153,51,158,450,321,170,304,539,556,22,515,518,526,531,537,396,178,21,542,39,524,278,530,220,375,380,2,26,9,3,11,14,12,10,13,29,28,30,27,31,34,32,33])).
% 59.33/59.36 cnf(564,plain,
% 59.33/59.36 (E(f8(a3,x5641),f4(f8(x5642,a3),f8(x5642,a3)))),
% 59.33/59.36 inference(scs_inference,[],[304,278,428,2,26])).
% 59.33/59.36 cnf(567,plain,
% 59.33/59.36 (E(a3,f4(f5(x5671),x5671))),
% 59.33/59.36 inference(scs_inference,[],[171,304,278,427,428,2,26,3])).
% 59.33/59.36 cnf(569,plain,
% 59.33/59.36 (P1(x5691,a3,f8(a3,x5692))),
% 59.33/59.36 inference(scs_inference,[],[171,304,178,278,427,428,2,26,3,11])).
% 59.33/59.36 cnf(570,plain,
% 59.33/59.36 (P1(f8(a3,x5701),x5702,f8(a3,x5702))),
% 59.33/59.36 inference(scs_inference,[],[171,304,22,178,278,427,428,2,26,3,11,9])).
% 59.33/59.36 cnf(571,plain,
% 59.33/59.36 (P1(x5711,x5712,f8(x5711,x5712))),
% 59.33/59.36 inference(rename_variables,[],[22])).
% 59.33/59.36 cnf(573,plain,
% 59.33/59.36 (P2(f8(a3,x5731),f8(a3,x5732),a3)),
% 59.33/59.36 inference(scs_inference,[],[158,171,304,22,178,278,427,428,2,26,3,11,9,14,12])).
% 59.33/59.36 cnf(574,plain,
% 59.33/59.36 (P1(x5741,f8(a3,x5742),f8(x5741,a3))),
% 59.33/59.36 inference(scs_inference,[],[158,171,304,22,571,178,278,427,428,2,26,3,11,9,14,12,10])).
% 59.33/59.36 cnf(580,plain,
% 59.33/59.36 (P1(x5801,a3,a3)),
% 59.33/59.36 inference(rename_variables,[],[178])).
% 59.33/59.36 cnf(594,plain,
% 59.33/59.36 (P1(x5941,f8(x5942,a3),f8(x5942,a3))),
% 59.33/59.36 inference(scs_inference,[],[193,227,158,454,450,533,171,17,304,22,571,178,580,342,39,278,427,428,267,2,26,3,11,9,14,12,10,13,29,30,28,27,34])).
% 59.33/59.36 cnf(604,plain,
% 59.33/59.36 (E(f8(x6041,a3),f4(f8(x6042,a3),f8(x6042,a3)))),
% 59.33/59.36 inference(scs_inference,[],[217,2])).
% 59.33/59.36 cnf(605,plain,
% 59.33/59.36 (E(f8(a3,x6051),f8(f8(x6052,a3),f8(a3,x6051)))),
% 59.33/59.36 inference(scs_inference,[],[396,22,217,2,26])).
% 59.33/59.36 cnf(606,plain,
% 59.33/59.36 (P1(x6061,x6062,f8(x6061,x6062))),
% 59.33/59.36 inference(rename_variables,[],[22])).
% 59.33/59.36 cnf(609,plain,
% 59.33/59.36 (E(x6091,f4(x6091,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(611,plain,
% 59.33/59.36 (E(x6111,f4(x6111,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(614,plain,
% 59.33/59.36 (E(a3,f8(x6141,a3))),
% 59.33/59.36 inference(rename_variables,[],[170])).
% 59.33/59.36 cnf(617,plain,
% 59.33/59.36 (P2(f8(x6171,a3),f8(a3,x6172),a3)),
% 59.33/59.36 inference(scs_inference,[],[158,454,170,614,396,22,502,39,609,611,217,514,2,26,11,9,3,14,12])).
% 59.33/59.36 cnf(618,plain,
% 59.33/59.36 (P1(x6181,f8(x6182,a3),a3)),
% 59.33/59.36 inference(scs_inference,[],[158,454,170,614,396,22,178,502,39,609,611,217,514,2,26,11,9,3,14,12,10])).
% 59.33/59.36 cnf(620,plain,
% 59.33/59.36 (P2(f8(a3,a3),a3,f8(a3,x6201))),
% 59.33/59.36 inference(scs_inference,[],[158,454,450,170,614,396,22,178,502,39,609,611,217,514,2,26,11,9,3,14,12,10,13,28])).
% 59.33/59.36 cnf(621,plain,
% 59.33/59.36 (P2(a3,f8(a3,x6211),a3)),
% 59.33/59.36 inference(rename_variables,[],[158])).
% 59.33/59.36 cnf(624,plain,
% 59.33/59.36 (P1(x6241,f8(a3,f8(a3,x6242)),f8(a3,x6242))),
% 59.33/59.36 inference(scs_inference,[],[158,454,450,170,614,396,44,22,178,502,42,39,609,611,217,514,2,26,11,9,3,14,12,10,13,28,30])).
% 59.33/59.36 cnf(631,plain,
% 59.33/59.36 (P1(x6311,x6312,f8(x6311,x6312))),
% 59.33/59.36 inference(rename_variables,[],[22])).
% 59.33/59.36 cnf(633,plain,
% 59.33/59.36 (P1(f8(x6331,a3),f8(a3,x6332),f8(a3,x6332))),
% 59.33/59.36 inference(rename_variables,[],[396])).
% 59.33/59.36 cnf(638,plain,
% 59.33/59.36 (P1(f8(x6381,a3),f8(a3,x6382),f8(a3,x6382))),
% 59.33/59.36 inference(rename_variables,[],[396])).
% 59.33/59.36 cnf(640,plain,
% 59.33/59.36 (P1(f8(x6401,a3),f8(a3,a3),f8(x6401,a3))),
% 59.33/59.36 inference(scs_inference,[],[158,621,454,450,170,614,396,633,638,44,22,606,631,178,502,42,39,609,611,522,326,217,514,2,26,11,9,3,14,12,10,13,28,30,27,31,32,33])).
% 59.33/59.36 cnf(647,plain,
% 59.33/59.36 (E(f4(f8(x6471,a3),f8(x6471,a3)),f8(a3,x6472))),
% 59.33/59.36 inference(scs_inference,[],[564,2])).
% 59.33/59.36 cnf(648,plain,
% 59.33/59.36 (E(f8(x6481,a3),f8(x6482,a3))),
% 59.33/59.36 inference(scs_inference,[],[22,564,521,2,26])).
% 59.33/59.36 cnf(652,plain,
% 59.33/59.36 (P1(f8(a3,x6521),f4(x6522,a3),f8(a3,x6522))),
% 59.33/59.36 inference(scs_inference,[],[171,44,22,564,521,2,26,9])).
% 59.33/59.36 cnf(653,plain,
% 59.33/59.36 (P1(x6531,f4(x6532,a3),f8(x6531,x6532))),
% 59.33/59.36 inference(rename_variables,[],[44])).
% 59.33/59.36 cnf(657,plain,
% 59.33/59.36 (E(x6571,f4(x6571,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(659,plain,
% 59.33/59.36 (E(x6591,f4(x6591,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(662,plain,
% 59.33/59.36 (P1(x6621,f8(a3,x6622),a3)),
% 59.33/59.36 inference(scs_inference,[],[454,533,171,44,22,178,559,39,657,659,564,605,521,2,26,9,3,11,14,12,10])).
% 59.33/59.36 cnf(666,plain,
% 59.33/59.36 (P1(x6661,f4(x6662,a3),f8(x6661,x6662))),
% 59.33/59.36 inference(rename_variables,[],[44])).
% 59.33/59.36 cnf(668,plain,
% 59.33/59.36 (P2(a3,a3,f8(a3,x6681))),
% 59.33/59.36 inference(scs_inference,[],[454,158,533,450,171,304,44,653,22,178,559,39,657,659,594,564,605,521,2,26,9,3,11,14,12,10,13,29,28])).
% 59.33/59.36 cnf(675,plain,
% 59.33/59.36 (P1(f8(x6751,a3),f4(x6752,a3),f8(a3,x6752))),
% 59.33/59.36 inference(rename_variables,[],[304])).
% 59.33/59.36 cnf(677,plain,
% 59.33/59.36 (P1(x6771,f8(a3,x6772),f8(a3,x6772))),
% 59.33/59.36 inference(scs_inference,[],[454,158,533,450,171,304,396,44,653,22,178,559,39,657,659,278,594,564,605,521,2,26,9,3,11,14,12,10,13,29,28,30,34])).
% 59.33/59.36 cnf(679,plain,
% 59.33/59.36 (P2(f8(a3,x6791),f8(a3,x6791),f8(f8(a3,x6792),x6791))),
% 59.33/59.36 inference(scs_inference,[],[454,158,533,450,171,304,675,396,44,653,666,22,178,559,39,657,659,278,594,564,605,521,2,26,9,3,11,14,12,10,13,29,28,30,34,32])).
% 59.33/59.36 cnf(690,plain,
% 59.33/59.36 (E(f8(x6901,a3),f8(a3,x6902))),
% 59.33/59.36 inference(scs_inference,[],[385,2])).
% 59.33/59.36 cnf(691,plain,
% 59.33/59.36 (E(a3,f8(x6911,f5(a3)))),
% 59.33/59.36 inference(scs_inference,[],[178,385,267,2,26])).
% 59.33/59.36 cnf(694,plain,
% 59.33/59.36 (E(f4(f5(a3),a3),f8(x6941,a3))),
% 59.33/59.36 inference(scs_inference,[],[178,385,431,267,98,2,26,3])).
% 59.33/59.36 cnf(696,plain,
% 59.33/59.36 (P1(x6961,f8(f4(a3,a3),f4(a3,a3)),f8(a3,x6962))),
% 59.33/59.36 inference(scs_inference,[],[171,178,350,385,431,267,98,2,26,3,11])).
% 59.33/59.36 cnf(697,plain,
% 59.33/59.36 (P1(f4(f8(x6971,a3),a3),f4(a3,a3),f8(x6971,a3))),
% 59.33/59.36 inference(scs_inference,[],[171,178,350,559,39,385,431,267,98,2,26,3,11,9])).
% 59.33/59.36 cnf(698,plain,
% 59.33/59.36 (E(x6981,f4(x6981,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(700,plain,
% 59.33/59.36 (E(x7001,f4(x7001,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(701,plain,
% 59.33/59.36 (P2(f4(f8(a3,a3),a3),a3,f8(x7011,a3))),
% 59.33/59.36 inference(scs_inference,[],[450,171,178,350,559,39,698,700,385,431,267,98,2,26,3,11,9,14,12])).
% 59.33/59.36 cnf(702,plain,
% 59.33/59.36 (E(x7021,f4(x7021,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(704,plain,
% 59.33/59.36 (E(x7041,f4(x7041,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(708,plain,
% 59.33/59.36 (P1(f4(x7081,a3),x7082,f8(x7081,x7082))),
% 59.33/59.36 inference(rename_variables,[],[42])).
% 59.33/59.36 cnf(709,plain,
% 59.33/59.36 (P1(x7091,a3,a3)),
% 59.33/59.36 inference(rename_variables,[],[178])).
% 59.33/59.36 cnf(715,plain,
% 59.33/59.36 (P1(f8(x7151,a3),f4(x7152,a3),f8(a3,x7152))),
% 59.33/59.36 inference(rename_variables,[],[304])).
% 59.33/59.36 cnf(717,plain,
% 59.33/59.36 (P2(f8(a3,x7171),a3,a3)),
% 59.33/59.36 inference(scs_inference,[],[450,573,158,171,304,178,44,502,350,559,529,42,39,698,700,702,704,385,431,267,98,2,26,3,11,9,14,12,10,13,29,30,28])).
% 59.33/59.36 cnf(720,plain,
% 59.33/59.36 (P2(a3,a3,f8(x7201,f8(x7202,a3)))),
% 59.33/59.36 inference(scs_inference,[],[450,573,158,533,171,304,178,709,44,502,350,559,529,42,708,39,698,700,702,704,385,431,267,98,2,26,3,11,9,14,12,10,13,29,30,28,31])).
% 59.33/59.36 cnf(722,plain,
% 59.33/59.36 (P1(x7221,a3,a3)),
% 59.33/59.36 inference(rename_variables,[],[178])).
% 59.33/59.36 cnf(723,plain,
% 59.33/59.36 (P1(x7231,a3,a3)),
% 59.33/59.36 inference(rename_variables,[],[178])).
% 59.33/59.36 cnf(730,plain,
% 59.33/59.36 (P1(f8(x7301,a3),a3,f4(a3,a3))),
% 59.33/59.36 inference(scs_inference,[],[187,454,450,573,158,533,171,304,715,178,709,723,722,44,502,22,350,559,529,42,708,21,39,698,700,702,704,385,431,267,98,2,26,3,11,9,14,12,10,13,29,30,28,31,32,33])).
% 59.33/59.36 cnf(736,plain,
% 59.33/59.36 (E(f5(f8(a3,x7361)),f5(a3))),
% 59.33/59.36 inference(scs_inference,[],[171,4,2])).
% 59.33/59.36 cnf(741,plain,
% 59.33/59.36 (P1(x7411,f4(a3,a3),f4(f8(a3,x7412),a3))),
% 59.33/59.36 inference(scs_inference,[],[178,342,39,694,183,2,26,11])).
% 59.33/59.36 cnf(742,plain,
% 59.33/59.36 (E(x7421,f4(x7421,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(744,plain,
% 59.33/59.36 (E(x7441,f4(x7441,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(745,plain,
% 59.33/59.36 (E(f5(f8(a3,x7451)),f8(a3,x7452))),
% 59.33/59.36 inference(scs_inference,[],[178,342,640,39,742,694,736,482,183,2,26,11,9,3])).
% 59.33/59.36 cnf(748,plain,
% 59.33/59.36 (E(x7481,f4(x7481,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(749,plain,
% 59.33/59.36 (P1(x7491,f4(f4(a3,a3),a3),f8(a3,x7492))),
% 59.33/59.36 inference(scs_inference,[],[573,171,178,342,640,39,742,744,748,694,736,482,183,2,26,11,9,3,14,12,10])).
% 59.33/59.36 cnf(750,plain,
% 59.33/59.36 (E(x7501,f4(x7501,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(753,plain,
% 59.33/59.36 (P2(a3,f4(f8(a3,a3),f8(a3,a3)),f8(x7531,a3))),
% 59.33/59.36 inference(scs_inference,[],[187,450,573,447,171,16,178,342,640,39,742,744,748,750,694,736,482,183,2,26,11,9,3,14,12,10,13,28])).
% 59.33/59.36 cnf(754,plain,
% 59.33/59.36 (P2(x7541,a3,x7541)),
% 59.33/59.36 inference(rename_variables,[],[16])).
% 59.33/59.36 cnf(765,plain,
% 59.33/59.36 (P2(f4(a3,a3),f4(a3,a3),f4(a3,a3))),
% 59.33/59.36 inference(scs_inference,[],[187,450,573,447,171,16,754,304,44,178,502,342,640,39,742,744,748,750,677,525,694,736,482,730,183,2,26,11,9,3,14,12,10,13,28,29,30,31])).
% 59.33/59.36 cnf(780,plain,
% 59.33/59.36 (E(f8(a3,x7801),f5(f8(a3,x7802)))),
% 59.33/59.36 inference(scs_inference,[],[745,2])).
% 59.33/59.36 cnf(781,plain,
% 59.33/59.36 (E(f8(x7811,a3),f4(f8(a3,a3),a3))),
% 59.33/59.36 inference(scs_inference,[],[450,21,745,2,25])).
% 59.33/59.36 cnf(784,plain,
% 59.33/59.36 (E(f8(a3,a3),f4(f8(a3,x7841),a3))),
% 59.33/59.36 inference(scs_inference,[],[450,304,21,741,745,2,25,26])).
% 59.33/59.36 cnf(786,plain,
% 59.33/59.36 (P1(f8(x7861,a3),f4(x7862,a3),f8(a3,x7862))),
% 59.33/59.36 inference(rename_variables,[],[304])).
% 59.33/59.36 cnf(788,plain,
% 59.33/59.36 (P1(f4(f4(x7881,a3),a3),x7882,f8(x7881,x7882))),
% 59.33/59.36 inference(scs_inference,[],[450,304,42,21,39,741,745,2,25,26,9])).
% 59.33/59.36 cnf(789,plain,
% 59.33/59.36 (E(x7891,f4(x7891,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(790,plain,
% 59.33/59.36 (E(f5(a3),f4(f5(x7901),x7901))),
% 59.33/59.36 inference(scs_inference,[],[450,304,42,21,39,741,745,567,376,2,25,26,9,3])).
% 59.33/59.36 cnf(791,plain,
% 59.33/59.36 (P1(x7911,a3,f4(f8(a3,x7912),a3))),
% 59.33/59.36 inference(scs_inference,[],[450,304,569,42,21,39,789,741,745,567,376,2,25,26,9,3,11])).
% 59.33/59.36 cnf(792,plain,
% 59.33/59.36 (E(x7921,f4(x7921,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(794,plain,
% 59.33/59.36 (E(x7941,f4(x7941,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(795,plain,
% 59.33/59.36 (P2(f8(a3,x7951),a3,f8(x7952,a3))),
% 59.33/59.36 inference(scs_inference,[],[450,533,620,171,304,569,42,21,39,789,792,741,745,567,376,2,25,26,9,3,11,14,12])).
% 59.33/59.36 cnf(797,plain,
% 59.33/59.36 (E(x7971,f4(x7971,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(800,plain,
% 59.33/59.36 (P2(f8(x8001,a3),f5(f8(a3,a3)),a3)),
% 59.33/59.36 inference(scs_inference,[],[450,533,620,617,171,19,17,304,559,569,42,21,39,789,792,794,797,741,745,567,376,2,25,26,9,3,11,14,12,10,13,27])).
% 59.33/59.36 cnf(808,plain,
% 59.33/59.36 (P2(f8(a3,x8081),f8(x8082,a3),f8(x8083,a3))),
% 59.33/59.36 inference(scs_inference,[],[450,573,533,620,617,171,19,17,304,786,44,559,569,42,21,39,789,792,794,797,749,741,745,567,376,2,25,26,9,3,11,14,12,10,13,27,30,28])).
% 59.33/59.36 cnf(836,plain,
% 59.33/59.36 (E(f8(x8361,f8(x8362,a3)),a3)),
% 59.33/59.36 inference(scs_inference,[],[22,618,781,2,26])).
% 59.33/59.36 cnf(837,plain,
% 59.33/59.36 (P1(x8371,f8(x8372,a3),a3)),
% 59.33/59.36 inference(rename_variables,[],[618])).
% 59.33/59.36 cnf(838,plain,
% 59.33/59.36 (P1(x8381,x8382,f8(x8381,x8382))),
% 59.33/59.36 inference(rename_variables,[],[22])).
% 59.33/59.36 cnf(840,plain,
% 59.33/59.36 (E(f4(f5(x8401),x8401),f8(x8402,a3))),
% 59.33/59.36 inference(scs_inference,[],[170,22,618,781,213,2,26,3])).
% 59.33/59.36 cnf(843,plain,
% 59.33/59.36 (P1(x8431,f8(x8432,a3),f8(a3,x8433))),
% 59.33/59.36 inference(scs_inference,[],[171,170,22,618,837,143,781,213,2,26,3,9,11])).
% 59.33/59.36 cnf(845,plain,
% 59.33/59.36 (P2(f4(f8(a3,a3),a3),a3,f8(a3,x8451))),
% 59.33/59.36 inference(scs_inference,[],[620,617,171,170,22,618,837,39,143,781,213,2,26,3,9,11,14,12])).
% 59.33/59.36 cnf(846,plain,
% 59.33/59.36 (E(x8461,f4(x8461,a3))),
% 59.33/59.36 inference(rename_variables,[],[39])).
% 59.33/59.36 cnf(847,plain,
% 59.33/59.36 (P1(x8471,f4(f8(x8472,a3),a3),a3)),
% 59.33/59.36 inference(scs_inference,[],[620,617,171,170,22,618,837,39,846,143,781,213,2,26,3,9,11,14,12,10])).
% 59.33/59.36 cnf(854,plain,
% 59.33/59.36 (P1(f4(a3,a3),a3,f4(a3,a3))),
% 59.33/59.36 inference(scs_inference,[],[620,617,701,171,170,178,22,838,444,618,837,529,39,846,143,781,730,213,2,26,3,9,11,14,12,10,13,30,29])).
% 59.33/59.36 cnf(855,plain,
% 59.33/59.36 (P1(x8551,a3,a3)),
% 59.33/59.36 inference(rename_variables,[],[178])).
% 59.33/59.36 cnf(857,plain,
% 59.33/59.36 (P2(f8(a3,x8571),f8(a3,x8572),f8(x8573,a3))),
% 59.33/59.36 inference(scs_inference,[],[573,533,620,617,701,171,170,178,22,838,444,618,837,529,39,846,143,781,730,213,2,26,3,9,11,14,12,10,13,30,29,28])).
% 59.33/59.36 cnf(858,plain,
% 59.33/59.36 (P2(f8(a3,x8581),f8(a3,x8582),a3)),
% 59.33/59.36 inference(rename_variables,[],[573])).
% 59.33/59.36 cnf(860,plain,
% 59.33/59.36 (P2(a3,a3,f4(f8(a3,x8601),a3))),
% 59.33/59.36 inference(scs_inference,[],[573,858,533,620,617,701,171,170,178,855,22,838,444,618,837,529,39,846,143,781,791,730,213,2,26,3,9,11,14,12,10,13,30,29,28,32])).
% 59.33/59.36 cnf(876,plain,
% 59.33/59.37 (E(f8(x8761,a3),f4(f5(x8762),x8762))),
% 59.33/59.37 inference(scs_inference,[],[840,2])).
% 59.33/59.37 cnf(877,plain,
% 59.33/59.37 (E(a3,f4(f8(a3,x8771),a3))),
% 59.33/59.37 inference(scs_inference,[],[178,840,791,2,26])).
% 59.33/59.37 cnf(881,plain,
% 59.33/59.37 (E(x8811,f4(x8811,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(883,plain,
% 59.33/59.37 (E(x8831,f4(x8831,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(884,plain,
% 59.33/59.37 (E(f8(x8841,f8(x8842,a3)),f8(a3,x8843))),
% 59.33/59.37 inference(scs_inference,[],[171,178,640,517,39,881,840,836,791,2,26,9,11,3])).
% 59.33/59.37 cnf(886,plain,
% 59.33/59.37 (P2(f4(f8(x8861,a3),a3),f8(a3,x8862),a3)),
% 59.33/59.37 inference(scs_inference,[],[617,323,171,178,640,517,39,881,883,840,836,791,2,26,9,11,3,14,12])).
% 59.33/59.37 cnf(887,plain,
% 59.33/59.37 (E(x8871,f4(x8871,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(895,plain,
% 59.33/59.37 (P2(f8(a3,x8951),f8(a3,x8952),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[227,153,573,617,51,323,321,171,17,178,640,517,21,39,881,883,887,840,836,791,2,26,9,11,3,14,12,10,13,27,28])).
% 59.33/59.37 cnf(922,plain,
% 59.33/59.37 (E(f8(x9221,f8(x9222,a3)),f8(x9223,a3))),
% 59.33/59.37 inference(scs_inference,[],[170,884,836,2,3])).
% 59.33/59.37 cnf(924,plain,
% 59.33/59.37 (E(x9241,f4(x9241,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(925,plain,
% 59.33/59.37 (P1(f4(f8(a3,x9251),a3),x9252,f8(a3,x9252))),
% 59.33/59.37 inference(scs_inference,[],[170,570,39,924,884,836,2,3,11,9])).
% 59.33/59.37 cnf(926,plain,
% 59.33/59.37 (E(x9261,f4(x9261,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(928,plain,
% 59.33/59.37 (P1(x9281,f8(a3,x9282),f8(a3,x9283))),
% 59.33/59.37 inference(scs_inference,[],[321,171,170,569,570,39,924,884,836,2,3,11,9,14,10])).
% 59.33/59.37 cnf(929,plain,
% 59.33/59.37 (P2(f8(a3,x9291),a3,f8(a3,x9292))),
% 59.33/59.37 inference(scs_inference,[],[668,321,171,170,569,570,39,924,884,836,2,3,11,9,14,10,12])).
% 59.33/59.37 cnf(934,plain,
% 59.33/59.37 (P2(f8(x9341,a3),f4(f8(x9342,a3),f8(x9342,a3)),f8(x9342,a3))),
% 59.33/59.37 inference(rename_variables,[],[227])).
% 59.33/59.37 cnf(936,plain,
% 59.33/59.37 (P1(x9361,f4(f8(x9362,a3),f8(x9362,a3)),f8(a3,x9363))),
% 59.33/59.37 inference(scs_inference,[],[227,668,321,765,895,171,170,304,624,569,570,529,39,924,926,884,836,2,3,11,9,14,10,12,13,27,30])).
% 59.33/59.37 cnf(941,plain,
% 59.33/59.37 (P2(f8(x9411,a3),a3,f8(a3,x9412))),
% 59.33/59.37 inference(scs_inference,[],[227,934,620,668,321,765,895,171,170,304,624,569,570,529,39,924,926,884,836,2,3,11,9,14,10,12,13,27,30,28])).
% 59.33/59.37 cnf(962,plain,
% 59.33/59.37 (E(f8(x9621,a3),f8(x9622,f8(x9623,a3)))),
% 59.33/59.37 inference(scs_inference,[],[922,2])).
% 59.33/59.37 cnf(963,plain,
% 59.33/59.37 (E(f8(a3,x9631),f8(x9632,f4(a3,a3)))),
% 59.33/59.37 inference(scs_inference,[],[342,22,922,2,26])).
% 59.33/59.37 cnf(964,plain,
% 59.33/59.37 (P1(x9641,x9642,f8(x9641,x9642))),
% 59.33/59.37 inference(rename_variables,[],[22])).
% 59.33/59.37 cnf(967,plain,
% 59.33/59.37 (E(x9671,f4(x9671,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(968,plain,
% 59.33/59.37 (E(a3,f5(f8(a3,x9681)))),
% 59.33/59.37 inference(scs_inference,[],[171,342,22,652,39,922,780,2,26,9,3])).
% 59.33/59.37 cnf(970,plain,
% 59.33/59.37 (P1(x9701,f8(x9702,a3),f4(f8(x9702,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[171,342,22,594,652,39,967,922,780,2,26,9,3,11])).
% 59.33/59.37 cnf(971,plain,
% 59.33/59.37 (E(x9711,f4(x9711,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(973,plain,
% 59.33/59.37 (E(x9731,f4(x9731,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(975,plain,
% 59.33/59.37 (E(x9751,f4(x9751,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(976,plain,
% 59.33/59.37 (P2(f8(a3,x9761),f4(f8(a3,x9762),f8(a3,x9762)),a3)),
% 59.33/59.37 inference(scs_inference,[],[323,765,171,342,22,662,594,652,39,967,971,973,922,780,2,26,9,3,11,14,10,12])).
% 59.33/59.37 cnf(981,plain,
% 59.33/59.37 (P1(x9811,x9812,f8(x9811,x9812))),
% 59.33/59.37 inference(rename_variables,[],[22])).
% 59.33/59.37 cnf(984,plain,
% 59.33/59.37 (P1(x9841,x9842,f8(x9841,x9842))),
% 59.33/59.37 inference(rename_variables,[],[22])).
% 59.33/59.37 cnf(986,plain,
% 59.33/59.37 (P1(x9861,f4(a3,a3),f8(a3,x9862))),
% 59.33/59.37 inference(rename_variables,[],[342])).
% 59.33/59.37 cnf(988,plain,
% 59.33/59.37 (P2(f8(x9881,a3),a3,f8(x9882,a3))),
% 59.33/59.37 inference(scs_inference,[],[227,323,765,321,808,795,171,342,569,22,964,981,662,594,652,39,967,971,973,975,922,780,2,26,9,3,11,14,10,12,13,30,29,28])).
% 59.33/59.37 cnf(989,plain,
% 59.33/59.37 (P2(f8(x9891,a3),f4(f8(x9892,a3),f8(x9892,a3)),f8(x9892,a3))),
% 59.33/59.37 inference(rename_variables,[],[227])).
% 59.33/59.37 cnf(993,plain,
% 59.33/59.37 (P1(x9931,x9932,f8(x9931,x9932))),
% 59.33/59.37 inference(rename_variables,[],[22])).
% 59.33/59.37 cnf(995,plain,
% 59.33/59.37 (P1(x9951,f4(a3,a3),f8(a3,x9952))),
% 59.33/59.37 inference(rename_variables,[],[342])).
% 59.33/59.37 cnf(998,plain,
% 59.33/59.37 (P1(x9981,x9982,f8(x9981,x9982))),
% 59.33/59.37 inference(rename_variables,[],[22])).
% 59.33/59.37 cnf(1005,plain,
% 59.33/59.37 (~P1(x10051,f4(f8(x10052,a3),f8(x10052,a3)),a3)+P1(x10051,f8(x10052,a3),f8(x10051,f8(x10053,a3)))),
% 59.33/59.37 inference(scs_inference,[],[227,989,533,323,765,321,808,795,171,16,342,986,995,569,22,964,981,984,993,998,662,594,652,39,967,971,973,975,922,780,2,26,9,3,11,14,10,12,13,30,29,28,32,31,33,293,34])).
% 59.33/59.37 cnf(1010,plain,
% 59.33/59.37 (E(f8(x10101,f8(a3,x10102)),a3)),
% 59.33/59.37 inference(scs_inference,[],[22,662,963,2,26])).
% 59.33/59.37 cnf(1012,plain,
% 59.33/59.37 (P1(x10121,x10122,f8(x10121,x10122))),
% 59.33/59.37 inference(rename_variables,[],[22])).
% 59.33/59.37 cnf(1015,plain,
% 59.33/59.37 (E(x10151,f4(x10151,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1020,plain,
% 59.33/59.37 (E(x10201,f4(x10201,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1022,plain,
% 59.33/59.37 (E(x10221,f4(x10221,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1024,plain,
% 59.33/59.37 (E(x10241,f4(x10241,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1026,plain,
% 59.33/59.37 (E(x10261,f4(x10261,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1033,plain,
% 59.33/59.37 (P1(x10331,a3,f8(f8(a3,x10332),f8(x10333,a3)))),
% 59.33/59.37 inference(scs_inference,[],[227,533,765,753,808,857,171,342,22,1012,618,594,517,662,730,39,1015,1020,1022,1024,1026,963,962,2,26,11,3,9,14,10,12,13,28,30])).
% 59.33/59.37 cnf(1034,plain,
% 59.33/59.37 (P1(x10341,f8(x10342,a3),a3)),
% 59.33/59.37 inference(rename_variables,[],[618])).
% 59.33/59.37 cnf(1041,plain,
% 59.33/59.37 (P1(x10411,f4(a3,a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[227,533,765,753,808,857,895,171,342,22,1012,618,1034,594,517,521,662,730,39,1015,1020,1022,1024,1026,963,962,2,26,11,3,9,14,10,12,13,28,30,29,34])).
% 59.33/59.37 cnf(1061,plain,
% 59.33/59.37 (E(f8(x10611,f8(a3,x10612)),f8(x10611,a3))),
% 59.33/59.37 inference(scs_inference,[],[22,574,784,2,26])).
% 59.33/59.37 cnf(1063,plain,
% 59.33/59.37 (P1(x10631,x10632,f8(x10631,x10632))),
% 59.33/59.37 inference(rename_variables,[],[22])).
% 59.33/59.37 cnf(1065,plain,
% 59.33/59.37 (E(f8(x10651,f8(a3,x10652)),f8(a3,x10653))),
% 59.33/59.37 inference(scs_inference,[],[171,22,574,784,1010,2,26,3])).
% 59.33/59.37 cnf(1066,plain,
% 59.33/59.37 (P1(f4(f4(a3,a3),a3),a3,f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[171,22,854,39,574,784,1010,2,26,3,9])).
% 59.33/59.37 cnf(1067,plain,
% 59.33/59.37 (E(x10671,f4(x10671,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1068,plain,
% 59.33/59.37 (P1(x10681,a3,f4(f8(x10682,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[171,22,521,854,39,1067,574,784,1010,2,26,3,9,11])).
% 59.33/59.37 cnf(1069,plain,
% 59.33/59.37 (E(x10691,f4(x10691,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1071,plain,
% 59.33/59.37 (P1(x10711,f8(a3,x10712),f8(x10713,a3))),
% 59.33/59.37 inference(scs_inference,[],[800,171,22,521,854,39,1067,574,784,1010,2,26,3,9,11,14,10])).
% 59.33/59.37 cnf(1072,plain,
% 59.33/59.37 (P2(f4(f8(a3,x10721),a3),a3,a3)),
% 59.33/59.37 inference(scs_inference,[],[717,800,171,22,521,854,39,1067,1069,574,784,1010,2,26,3,9,11,14,10,12])).
% 59.33/59.37 cnf(1075,plain,
% 59.33/59.37 (P1(f4(a3,a3),f8(x10751,a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[717,845,800,171,22,618,521,730,854,39,1067,1069,574,784,1010,2,26,3,9,11,14,10,12,13,29])).
% 59.33/59.37 cnf(1083,plain,
% 59.33/59.37 (P1(x10831,a3,f8(f8(a3,x10832),f8(a3,x10833)))),
% 59.33/59.37 inference(scs_inference,[],[573,717,116,845,800,171,17,342,22,1063,618,521,662,730,854,39,1067,1069,574,784,1010,2,26,3,9,11,14,10,12,13,29,28,30])).
% 59.33/59.37 cnf(1096,plain,
% 59.33/59.37 (E(f8(a3,x10961),f4(f8(a3,x10962),a3))),
% 59.33/59.37 inference(scs_inference,[],[569,791,1061,2,26])).
% 59.33/59.37 cnf(1099,plain,
% 59.33/59.37 (E(f8(x10991,f8(a3,x10992)),f8(x10993,a3))),
% 59.33/59.37 inference(scs_inference,[],[170,569,791,1061,1010,2,26,3])).
% 59.33/59.37 cnf(1100,plain,
% 59.33/59.37 (P1(f4(a1,a3),a2,a6)),
% 59.33/59.37 inference(scs_inference,[],[170,569,15,791,39,1061,1010,2,26,3,9])).
% 59.33/59.37 cnf(1101,plain,
% 59.33/59.37 (E(x11011,f4(x11011,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1102,plain,
% 59.33/59.37 (P1(x11021,f8(x11022,a3),f4(f8(a3,x11023),a3))),
% 59.33/59.37 inference(scs_inference,[],[170,569,843,15,791,39,1101,1061,1010,2,26,3,9,11])).
% 59.33/59.37 cnf(1103,plain,
% 59.33/59.37 (E(x11031,f4(x11031,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1105,plain,
% 59.33/59.37 (E(x11051,f4(x11051,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1110,plain,
% 59.33/59.37 (P2(f8(x11101,a3),f5(a3),a3)),
% 59.33/59.37 inference(scs_inference,[],[533,753,929,988,171,170,19,17,569,843,15,791,39,1101,1103,1105,1061,1010,2,26,3,9,11,14,12,10,13,27])).
% 59.33/59.37 cnf(1112,plain,
% 59.33/59.37 (P2(a3,x11121,x11121)),
% 59.33/59.37 inference(rename_variables,[],[17])).
% 59.33/59.37 cnf(1114,plain,
% 59.33/59.37 (P1(f8(a3,x11141),a3,f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[533,753,929,988,171,170,19,17,342,569,843,15,854,791,39,1101,1103,1105,1041,1061,1010,2,26,3,9,11,14,12,10,13,27,29])).
% 59.33/59.37 cnf(1117,plain,
% 59.33/59.37 (P2(a3,f8(a3,x11171),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[533,158,51,753,929,988,171,170,19,17,1112,342,569,843,15,854,791,39,1101,1103,1105,1041,1061,1010,2,26,3,9,11,14,12,10,13,27,29,28])).
% 59.33/59.37 cnf(1121,plain,
% 59.33/59.37 (P1(x11211,f8(x11212,a3),f8(f8(a3,x11213),f8(x11212,a3)))),
% 59.33/59.37 inference(scs_inference,[],[533,158,51,753,929,988,171,170,19,17,1112,342,569,22,594,843,15,854,791,39,1101,1103,1105,1041,1061,1010,2,26,3,9,11,14,12,10,13,27,29,28,30])).
% 59.33/59.37 cnf(1125,plain,
% 59.33/59.37 (P1(x11251,f8(x11252,a3),f4(f8(a3,x11253),f8(a3,x11253)))),
% 59.33/59.37 inference(scs_inference,[],[533,158,51,753,929,988,171,170,19,17,1112,342,569,22,594,843,21,15,854,791,39,1101,1103,1105,1041,1061,1010,2,26,3,9,11,14,12,10,13,27,29,28,30,34])).
% 59.33/59.37 cnf(1142,plain,
% 59.33/59.37 (E(f8(x11421,a3),f4(f8(a3,x11422),a3))),
% 59.33/59.37 inference(scs_inference,[],[521,791,1065,2,26])).
% 59.33/59.37 cnf(1148,plain,
% 59.33/59.37 (E(x11481,f4(x11481,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1150,plain,
% 59.33/59.37 (E(x11501,f4(x11501,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1152,plain,
% 59.33/59.37 (E(x11521,f4(x11521,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1153,plain,
% 59.33/59.37 (P1(f5(a1),f4(a2,a3),f4(a7,a3))),
% 59.33/59.37 inference(scs_inference,[],[941,171,521,218,145,791,18,39,1148,1150,1152,1065,375,2,26,3,9,11,14,10])).
% 59.33/59.37 cnf(1154,plain,
% 59.33/59.37 (E(x11541,f4(x11541,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1155,plain,
% 59.33/59.37 (P2(f4(f8(a3,x11551),a3),f8(x11552,a3),f8(x11553,a3))),
% 59.33/59.37 inference(scs_inference,[],[808,941,171,521,218,145,791,18,39,1148,1150,1152,1154,1065,375,2,26,3,9,11,14,10,12])).
% 59.33/59.37 cnf(1156,plain,
% 59.33/59.37 (E(x11561,f4(x11561,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1159,plain,
% 59.33/59.37 (P2(f8(x11591,a3),a3,a3)),
% 59.33/59.37 inference(scs_inference,[],[533,808,941,895,171,16,521,218,145,791,18,39,1148,1150,1152,1154,1156,1065,375,2,26,3,9,11,14,10,12,13,27])).
% 59.33/59.37 cnf(1160,plain,
% 59.33/59.37 (P2(x11601,a3,x11601)),
% 59.33/59.37 inference(rename_variables,[],[16])).
% 59.33/59.37 cnf(1162,plain,
% 59.33/59.37 (P1(f8(a3,x11621),f4(a3,a3),f8(x11622,a3))),
% 59.33/59.37 inference(scs_inference,[],[533,808,941,895,171,16,342,521,218,145,791,18,39,1148,1150,1152,1154,1156,1071,1065,375,2,26,3,9,11,14,10,12,13,27,29])).
% 59.33/59.37 cnf(1165,plain,
% 59.33/59.37 (P1(x11651,f4(a3,a3),f8(a3,x11652))),
% 59.33/59.37 inference(rename_variables,[],[342])).
% 59.33/59.37 cnf(1167,plain,
% 59.33/59.37 (P2(a3,f8(x11671,a3),f8(x11672,a3))),
% 59.33/59.37 inference(scs_inference,[],[533,158,808,941,795,895,171,16,342,521,218,145,791,18,39,1148,1150,1152,1154,1156,1071,1065,375,2,26,3,9,11,14,10,12,13,27,29,28])).
% 59.33/59.37 cnf(1170,plain,
% 59.33/59.37 (P1(x11701,f8(a3,x11702),f8(f8(a3,x11703),f8(x11704,a3)))),
% 59.33/59.37 inference(scs_inference,[],[533,158,808,941,795,895,171,16,342,1165,521,22,218,843,145,791,18,39,1148,1150,1152,1154,1156,1071,1065,375,2,26,3,9,11,14,10,12,13,27,29,28,30])).
% 59.33/59.37 cnf(1174,plain,
% 59.33/59.37 (P1(x11741,f8(x11742,a3),f8(x11743,a3))),
% 59.33/59.37 inference(scs_inference,[],[533,158,808,941,795,895,171,16,1160,342,1165,521,22,178,218,843,145,791,18,39,1148,1150,1152,1154,1156,1071,1065,375,2,26,3,9,11,14,10,12,13,27,29,28,30,34])).
% 59.33/59.37 cnf(1178,plain,
% 59.33/59.37 (P2(f8(x11781,a3),f8(x11781,a3),f8(a3,x11782))),
% 59.33/59.37 inference(scs_inference,[],[533,158,808,941,795,895,171,16,1160,342,1165,521,569,22,178,218,843,145,791,18,39,1148,1150,1152,1154,1156,1071,1065,375,2,26,3,9,11,14,10,12,13,27,29,28,30,34,32])).
% 59.33/59.37 cnf(1186,plain,
% 59.33/59.37 (E(f8(x11861,a3),f8(x11862,f8(a3,x11863)))),
% 59.33/59.37 inference(scs_inference,[],[1099,2])).
% 59.33/59.37 cnf(1188,plain,
% 59.33/59.37 (P1(x11881,f8(x11882,a3),f4(f8(x11882,a3),a3))),
% 59.33/59.37 inference(rename_variables,[],[970])).
% 59.33/59.37 cnf(1190,plain,
% 59.33/59.37 (E(a3,f8(f8(x11901,a3),x11902))),
% 59.33/59.37 inference(scs_inference,[],[171,618,970,1099,428,2,26,3])).
% 59.33/59.37 cnf(1193,plain,
% 59.33/59.37 (E(x11931,f4(x11931,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1195,plain,
% 59.33/59.37 (E(x11951,f4(x11951,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1197,plain,
% 59.33/59.37 (E(x11971,f4(x11971,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1199,plain,
% 59.33/59.37 (E(x11991,f4(x11991,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1201,plain,
% 59.33/59.37 (E(x12011,f4(x12011,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1214,plain,
% 59.33/59.37 (P2(x12141,x12142,f4(x12141,x12142))),
% 59.33/59.37 inference(rename_variables,[],[21])).
% 59.33/59.37 cnf(1220,plain,
% 59.33/59.37 (P1(x12201,f8(x12202,a3),f4(f8(x12203,a3),f8(x12203,a3)))),
% 59.33/59.37 inference(scs_inference,[],[533,227,857,895,1178,1155,171,696,618,21,1214,521,22,149,145,44,570,1075,970,1188,39,1193,1195,1197,1199,1201,1099,428,2,26,3,9,11,14,12,10,13,27,29,28,30,34])).
% 59.33/59.37 cnf(1223,plain,
% 59.33/59.37 (P2(f8(x12231,a3),f8(x12231,a3),a3)),
% 59.33/59.37 inference(scs_inference,[],[533,227,857,895,1178,1155,171,696,618,21,1214,521,22,178,149,145,44,570,1075,970,1188,39,1193,1195,1197,1199,1201,1099,428,2,26,3,9,11,14,12,10,13,27,29,28,30,34,32])).
% 59.33/59.37 cnf(1236,plain,
% 59.33/59.37 (E(f8(a3,x12361),f4(f8(x12362,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[569,1068,790,2,26])).
% 59.33/59.37 cnf(1237,plain,
% 59.33/59.37 (P1(x12371,a3,f4(f8(x12372,a3),a3))),
% 59.33/59.37 inference(rename_variables,[],[1068])).
% 59.33/59.37 cnf(1243,plain,
% 59.33/59.37 (E(x12431,f4(x12431,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1244,plain,
% 59.33/59.37 (P1(a1,a2,f4(a6,a3))),
% 59.33/59.37 inference(scs_inference,[],[171,569,15,1068,39,1243,1100,1186,790,2,26,3,9,11])).
% 59.33/59.37 cnf(1245,plain,
% 59.33/59.37 (E(x12451,f4(x12451,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1247,plain,
% 59.33/59.37 (E(x12471,f4(x12471,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1248,plain,
% 59.33/59.37 (P1(a1,f4(a2,a3),a6)),
% 59.33/59.37 inference(scs_inference,[],[988,171,569,15,1068,39,1243,1245,1247,1100,1186,790,2,26,3,9,11,14,10])).
% 59.33/59.37 cnf(1249,plain,
% 59.33/59.37 (E(x12491,f4(x12491,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1250,plain,
% 59.33/59.37 (P2(f4(f8(a3,x12501),a3),a3,f8(a3,x12502))),
% 59.33/59.37 inference(scs_inference,[],[929,988,171,569,15,1068,39,1243,1245,1247,1249,1100,1186,790,2,26,3,9,11,14,10,12])).
% 59.33/59.37 cnf(1251,plain,
% 59.33/59.37 (E(x12511,f4(x12511,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1254,plain,
% 59.33/59.37 (P2(a3,f4(f8(x12541,a3),f8(x12541,a3)),a3)),
% 59.33/59.37 inference(scs_inference,[],[227,929,988,1117,1223,171,569,15,1068,39,1243,1245,1247,1249,1251,1100,1186,790,2,26,3,9,11,14,10,12,13,27])).
% 59.33/59.37 cnf(1262,plain,
% 59.33/59.37 (P2(a3,f4(a3,a3),f8(x12621,a3))),
% 59.33/59.37 inference(scs_inference,[],[533,227,808,929,988,1117,1223,171,696,569,15,44,1068,1237,39,1243,1245,1247,1249,1251,1100,1186,790,2,26,3,9,11,14,10,12,13,27,29,28])).
% 59.33/59.37 cnf(1264,plain,
% 59.33/59.37 (P2(a3,a3,f8(x12641,a3))),
% 59.33/59.37 inference(rename_variables,[],[533])).
% 59.33/59.37 cnf(1271,plain,
% 59.33/59.37 (P2(a3,a3,f4(f8(x12711,a3),f8(x12711,a3)))),
% 59.33/59.37 inference(scs_inference,[],[533,1264,227,808,929,988,1117,1223,171,696,618,569,22,15,44,570,1068,1237,39,1243,1245,1247,1249,1251,1100,1220,1186,790,2,26,3,9,11,14,10,12,13,27,29,28,30,32])).
% 59.33/59.37 cnf(1283,plain,
% 59.33/59.37 (E(f4(f8(a3,x12831),a3),f8(a3,x12832))),
% 59.33/59.37 inference(scs_inference,[],[1096,2])).
% 59.33/59.37 cnf(1284,plain,
% 59.33/59.37 (E(f4(a3,a3),f4(f4(a3,a3),f4(a3,a3)))),
% 59.33/59.37 inference(scs_inference,[],[765,21,1096,2,25])).
% 59.33/59.37 cnf(1285,plain,
% 59.33/59.37 (P2(x12851,x12852,f4(x12851,x12852))),
% 59.33/59.37 inference(rename_variables,[],[21])).
% 59.33/59.37 cnf(1287,plain,
% 59.33/59.37 (E(f4(a7,a3),f8(f5(a1),a2))),
% 59.33/59.37 inference(scs_inference,[],[765,176,21,42,1096,2,25,26])).
% 59.33/59.37 cnf(1290,plain,
% 59.33/59.37 (E(a3,f8(x12901,f4(a3,a3)))),
% 59.33/59.37 inference(scs_inference,[],[765,170,176,21,42,1096,252,2,25,26,3])).
% 59.33/59.37 cnf(1304,plain,
% 59.33/59.37 (P2(f8(a3,a3),f8(f8(a3,x13041),a3),a3)),
% 59.33/59.37 inference(scs_inference,[],[765,668,753,323,617,679,170,16,19,176,350,21,1075,208,42,39,1096,252,2,25,26,3,9,11,14,12,10,13,27,28])).
% 59.33/59.37 cnf(1308,plain,
% 59.33/59.37 (P1(x13081,f4(f8(a3,a3),f8(a3,a3)),a3)),
% 59.33/59.37 inference(scs_inference,[],[765,668,753,323,617,679,170,16,19,176,350,21,662,278,1075,208,42,39,1096,252,2,25,26,3,9,11,14,12,10,13,27,28,30])).
% 59.33/59.37 cnf(1310,plain,
% 59.33/59.37 (P1(x13101,f8(a3,x13102),a3)),
% 59.33/59.37 inference(rename_variables,[],[662])).
% 59.33/59.37 cnf(1313,plain,
% 59.33/59.37 (P1(x13131,f4(a3,a3),f4(f8(a3,x13132),f8(a3,x13132)))),
% 59.33/59.37 inference(scs_inference,[],[765,668,753,323,617,679,170,16,19,176,350,21,1285,342,662,278,1075,208,42,39,1096,252,2,25,26,3,9,11,14,12,10,13,27,28,30,34])).
% 59.33/59.37 cnf(1316,plain,
% 59.33/59.37 (P2(a3,a3,f4(f8(a3,x13161),f8(a3,x13161)))),
% 59.33/59.37 inference(scs_inference,[],[765,668,753,323,617,679,170,16,19,176,350,21,1285,342,662,1310,278,1075,208,42,39,1096,252,1125,2,25,26,3,9,11,14,12,10,13,27,28,30,34,32])).
% 59.33/59.37 cnf(1328,plain,
% 59.33/59.37 (P1(x13281,f8(a3,a3),f8(x13281,f8(x13282,a3)))),
% 59.33/59.37 inference(scs_inference,[],[1308,1005])).
% 59.33/59.37 cnf(1331,plain,
% 59.33/59.37 (E(a7,f8(f5(a1),a2))),
% 59.33/59.37 inference(scs_inference,[],[149,44,1284,1308,1005,2,26])).
% 59.33/59.37 cnf(1334,plain,
% 59.33/59.37 (E(a3,f4(f4(a3,a3),f4(a3,a3)))),
% 59.33/59.37 inference(scs_inference,[],[149,44,39,1284,1308,1005,2,26,3])).
% 59.33/59.37 cnf(1335,plain,
% 59.33/59.37 (E(x13351,f4(x13351,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1339,plain,
% 59.33/59.37 (E(x13391,f4(x13391,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1341,plain,
% 59.33/59.37 (E(x13411,f4(x13411,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1343,plain,
% 59.33/59.37 (P2(f4(f8(x13431,a3),a3),a3,f8(a3,x13432))),
% 59.33/59.37 inference(scs_inference,[],[941,795,170,149,44,1075,183,39,1335,1339,1341,1284,1308,1005,2,26,3,9,11,14,13,12])).
% 59.33/59.37 cnf(1370,plain,
% 59.33/59.37 (E(f8(f5(a1),a2),f4(a7,a3))),
% 59.33/59.37 inference(scs_inference,[],[1287,2])).
% 59.33/59.37 cnf(1371,plain,
% 59.33/59.37 (E(f4(a3,a3),f8(a3,x13711))),
% 59.33/59.37 inference(scs_inference,[],[1075,843,1287,2,26])).
% 59.33/59.37 cnf(1374,plain,
% 59.33/59.37 (E(a3,f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1075,843,1287,968,736,2,26,3])).
% 59.33/59.37 cnf(1377,plain,
% 59.33/59.37 (E(x13771,f4(x13771,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1379,plain,
% 59.33/59.37 (E(x13791,f4(x13791,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1381,plain,
% 59.33/59.37 (E(x13811,f4(x13811,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1382,plain,
% 59.33/59.37 (P1(f8(x13821,a3),f8(x13822,a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[895,170,1075,652,843,730,1162,39,1377,1379,1287,968,736,2,26,3,9,11,14,10])).
% 59.33/59.37 cnf(1383,plain,
% 59.33/59.37 (P2(f4(f8(x13831,a3),a3),a3,f8(x13832,a3))),
% 59.33/59.37 inference(scs_inference,[],[988,895,170,1075,652,843,730,1162,39,1377,1379,1381,1287,968,736,2,26,3,9,11,14,10,12])).
% 59.33/59.37 cnf(1386,plain,
% 59.33/59.37 (P2(a3,f4(a3,a3),a3)),
% 59.33/59.37 inference(scs_inference,[],[51,929,988,895,1304,170,1075,652,843,730,1162,39,1377,1379,1381,1287,968,736,2,26,3,9,11,14,10,12,13,27])).
% 59.33/59.37 cnf(1389,plain,
% 59.33/59.37 (P2(f4(a3,a3),a3,a3)),
% 59.33/59.37 inference(scs_inference,[],[765,51,929,988,895,1304,170,19,1075,652,843,730,1162,39,1377,1379,1381,1287,968,736,2,26,3,9,11,14,10,12,13,27,28])).
% 59.33/59.37 cnf(1395,plain,
% 59.33/59.37 (P2(f4(a3,a3),f4(a3,a3),a3)),
% 59.33/59.37 inference(scs_inference,[],[765,51,929,988,895,1304,170,19,1075,662,278,652,843,730,1162,39,1377,1379,1381,1287,968,736,2,26,3,9,11,14,10,12,13,27,28,30,32])).
% 59.33/59.37 cnf(1398,plain,
% 59.33/59.37 (P1(f4(a3,a3),f8(x13981,a3),f4(a3,a3))),
% 59.33/59.37 inference(rename_variables,[],[1075])).
% 59.33/59.37 cnf(1400,plain,
% 59.33/59.37 (P1(f4(a3,a3),f8(x14001,a3),f4(f4(a3,a3),f4(a3,a3)))),
% 59.33/59.37 inference(scs_inference,[],[765,51,929,988,895,1304,170,19,21,1075,1398,662,278,652,843,730,1162,39,1377,1379,1381,1287,968,736,2,26,3,9,11,14,10,12,13,27,28,30,32,33])).
% 59.33/59.37 cnf(1404,plain,
% 59.33/59.37 (P1(x14041,f5(a3),f4(f8(x14041,a3),f8(x14041,a3)))),
% 59.33/59.37 inference(scs_inference,[],[765,51,929,988,895,1304,170,19,21,1075,1398,662,278,652,843,730,1162,39,1377,1379,1381,1287,968,736,2,26,3,9,11,14,10,12,13,27,28,30,32,33,121,120])).
% 59.33/59.37 cnf(1412,plain,
% 59.33/59.37 (E(f8(a3,x14121),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1371,2])).
% 59.33/59.37 cnf(1413,plain,
% 59.33/59.37 (E(f8(a3,a3),f4(f8(a3,x14131),f8(a3,x14131)))),
% 59.33/59.37 inference(scs_inference,[],[304,1371,1313,2,26])).
% 59.33/59.37 cnf(1417,plain,
% 59.33/59.37 (~E(f5(a6),f8(f5(a1),a2))),
% 59.33/59.37 inference(scs_inference,[],[304,1370,99,1371,1313,2,26,3])).
% 59.33/59.37 cnf(1419,plain,
% 59.33/59.37 (E(x14191,f4(x14191,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1421,plain,
% 59.33/59.37 (E(x14211,f4(x14211,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1423,plain,
% 59.33/59.37 (E(x14231,f4(x14231,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1425,plain,
% 59.33/59.37 (P2(f4(f8(a3,x14251),a3),a3,f8(x14252,a3))),
% 59.33/59.37 inference(scs_inference,[],[988,795,1167,170,304,730,1114,39,1419,1421,1423,1370,99,1371,1313,2,26,3,9,11,14,13,12])).
% 59.33/59.37 cnf(1426,plain,
% 59.33/59.37 (E(x14261,f4(x14261,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1429,plain,
% 59.33/59.37 (P2(f5(f8(x14291,a3)),a3,a3)),
% 59.33/59.37 inference(scs_inference,[],[533,988,795,1167,170,16,20,304,730,928,1114,39,1419,1421,1423,1426,1370,99,1371,1313,2,26,3,9,11,14,13,12,10,27])).
% 59.33/59.37 cnf(1433,plain,
% 59.33/59.37 (P2(f4(a3,a3),a3,f8(x14331,a3))),
% 59.33/59.37 inference(scs_inference,[],[533,988,795,1167,1262,1395,170,16,20,304,730,928,1114,39,1419,1421,1423,1426,1370,99,1371,1313,2,26,3,9,11,14,13,12,10,27,28])).
% 59.33/59.37 cnf(1452,plain,
% 59.33/59.37 (E(f4(a3,a3),f4(f8(x14521,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[1075,970,1413,2,26])).
% 59.33/59.37 cnf(1455,plain,
% 59.33/59.37 (E(f8(x14551,f8(x14552,a3)),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1075,1374,970,1413,836,2,26,3])).
% 59.33/59.37 cnf(1457,plain,
% 59.33/59.37 (E(x14571,f4(x14571,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1459,plain,
% 59.33/59.37 (E(x14591,f4(x14591,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1461,plain,
% 59.33/59.37 (E(x14611,f4(x14611,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1463,plain,
% 59.33/59.37 (E(x14631,f4(x14631,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1465,plain,
% 59.33/59.37 (E(x14651,f4(x14651,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1468,plain,
% 59.33/59.37 (P2(f4(a3,a3),f8(a3,x14681),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[857,895,1167,1117,1075,854,1162,1374,970,39,1457,1459,1461,1463,1465,1382,1413,836,2,26,3,9,11,14,12,10,13,27])).
% 59.33/59.37 cnf(1474,plain,
% 59.33/59.37 (P1(f8(x14741,a3),f4(a7,a3),f8(a3,a2))),
% 59.33/59.37 inference(scs_inference,[],[765,857,895,1167,1117,1433,176,304,1075,570,854,1162,1374,970,39,1457,1459,1461,1463,1465,1382,1413,836,2,26,3,9,11,14,12,10,13,27,28,30])).
% 59.33/59.37 cnf(1478,plain,
% 59.33/59.37 (P2(f4(a3,a3),f4(a3,a3),f8(a3,x14781))),
% 59.33/59.37 inference(scs_inference,[],[765,857,895,1167,1117,1433,176,304,1075,570,854,843,1162,1374,970,39,1457,1459,1461,1463,1465,1382,1413,836,2,26,3,9,11,14,12,10,13,27,28,30,32])).
% 59.33/59.37 cnf(1489,plain,
% 59.33/59.37 (E(f8(f5(a1),a2),a7)),
% 59.33/59.37 inference(scs_inference,[],[1331,2])).
% 59.33/59.37 cnf(1490,plain,
% 59.33/59.37 (E(f4(a3,a3),f8(f8(a3,x14901),f8(x14902,a3)))),
% 59.33/59.37 inference(scs_inference,[],[1075,1121,1331,2,26])).
% 59.33/59.37 cnf(1493,plain,
% 59.33/59.37 (E(f8(x14931,f8(a3,x14932)),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1075,1374,1121,1331,1010,2,26,3])).
% 59.33/59.37 cnf(1497,plain,
% 59.33/59.37 (E(x14971,f4(x14971,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1498,plain,
% 59.33/59.37 (P2(a3,f4(a3,a3),f4(f8(x14981,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[1262,170,1075,42,1374,39,1497,1121,143,1331,1010,2,26,3,9,11,14])).
% 59.33/59.37 cnf(1499,plain,
% 59.33/59.37 (E(x14991,f4(x14991,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1500,plain,
% 59.33/59.37 (P1(f8(a3,x15001),f8(x15002,a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1262,170,1075,42,1114,1374,39,1497,1121,143,1331,1010,2,26,3,9,11,14,10])).
% 59.33/59.37 cnf(1503,plain,
% 59.33/59.37 (P2(f8(x15031,a3),f4(a3,a3),f8(x15032,a3))),
% 59.33/59.37 inference(scs_inference,[],[1262,170,1075,42,1114,1374,39,1497,1499,1121,143,1331,1010,2,26,3,9,11,14,10,13,12])).
% 59.33/59.37 cnf(1504,plain,
% 59.33/59.37 (P2(f8(a3,x15041),f4(a3,a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1262,895,1468,170,1075,42,1114,1374,39,1497,1499,1121,143,1331,1010,2,26,3,9,11,14,10,13,12,28])).
% 59.33/59.37 cnf(1510,plain,
% 59.33/59.37 (P2(f4(a3,a3),f4(a3,a3),f8(x15101,a3))),
% 59.33/59.37 inference(scs_inference,[],[765,1262,895,1468,170,1075,517,42,1114,1374,1071,39,1497,1499,1121,143,1331,1010,2,26,3,9,11,14,10,13,12,28,30,32])).
% 59.33/59.37 cnf(1521,plain,
% 59.33/59.37 (E(f4(a3,a3),f8(f4(a3,a3),f8(x15211,a3)))),
% 59.33/59.37 inference(scs_inference,[],[1075,1328,1490,2,26])).
% 59.33/59.37 cnf(1523,plain,
% 59.33/59.37 (P1(f4(a3,a3),f8(x15231,a3),f4(a3,a3))),
% 59.33/59.37 inference(rename_variables,[],[1075])).
% 59.33/59.37 cnf(1525,plain,
% 59.33/59.37 (E(f4(f8(x15251,a3),f8(x15251,a3)),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1075,1374,1328,1490,174,2,26,3])).
% 59.33/59.37 cnf(1526,plain,
% 59.33/59.37 (P1(f4(a1,a3),a2,f4(a6,a3))),
% 59.33/59.37 inference(scs_inference,[],[1075,1374,39,1244,1328,1490,174,2,26,3,9])).
% 59.33/59.37 cnf(1527,plain,
% 59.33/59.37 (E(x15271,f4(x15271,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1529,plain,
% 59.33/59.37 (E(x15291,f4(x15291,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1532,plain,
% 59.33/59.37 (P2(f8(x15321,a3),f8(a3,x15322),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1117,717,1254,170,1075,1162,1374,39,1527,1244,1328,1490,174,2,26,3,9,11,14,13,12])).
% 59.33/59.37 cnf(1543,plain,
% 59.33/59.37 (P2(f4(a3,a3),f4(a3,a3),f4(f8(x15431,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[765,51,1117,717,1254,1478,170,304,1075,1523,570,1162,1374,1153,1100,970,39,1527,1529,1244,1328,1490,174,2,26,3,9,11,14,13,12,10,28,30,32])).
% 59.33/59.37 cnf(1556,plain,
% 59.33/59.37 (E(f4(a3,a3),f4(f8(a3,x15561),a3))),
% 59.33/59.37 inference(scs_inference,[],[1075,1521,1102,2,26])).
% 59.33/59.37 cnf(1559,plain,
% 59.33/59.37 (E(f8(a3,x15591),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1075,1374,1521,1102,299,2,26,3])).
% 59.33/59.37 cnf(1561,plain,
% 59.33/59.37 (E(x15611,f4(x15611,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1563,plain,
% 59.33/59.37 (E(x15631,f4(x15631,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1566,plain,
% 59.33/59.37 (E(x15661,f4(x15661,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1568,plain,
% 59.33/59.37 (E(x15681,f4(x15681,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1571,plain,
% 59.33/59.37 (P2(f4(a3,a3),f4(f8(x15711,a3),a3),f8(x15711,a3))),
% 59.33/59.37 inference(scs_inference,[],[523,1395,976,1543,170,1075,1374,1114,1382,39,1561,1563,1566,1568,1500,1521,1102,299,2,26,3,9,11,14,12,10,13,28])).
% 59.33/59.37 cnf(1587,plain,
% 59.33/59.37 (E(f4(f8(x15871,a3),a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1452,2])).
% 59.33/59.37 cnf(1588,plain,
% 59.33/59.37 (E(f4(a3,a3),f4(f8(x15881,a3),f8(x15881,a3)))),
% 59.33/59.37 inference(scs_inference,[],[1075,1452,1220,2,26])).
% 59.33/59.37 cnf(1591,plain,
% 59.33/59.37 (E(f4(f8(x15911,a3),a3),f8(x15912,a3))),
% 59.33/59.37 inference(scs_inference,[],[170,1075,1452,1220,141,2,26,3])).
% 59.33/59.37 cnf(1593,plain,
% 59.33/59.37 (E(x15931,f4(x15931,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1594,plain,
% 59.33/59.37 (P1(x15941,f4(f8(a3,a3),f8(a3,a3)),f8(x15942,a3))),
% 59.33/59.37 inference(scs_inference,[],[170,1075,1308,39,1474,1452,1220,141,2,26,3,9,11])).
% 59.33/59.37 cnf(1596,plain,
% 59.33/59.37 (E(x15961,f4(x15961,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1597,plain,
% 59.33/59.37 (P1(f4(a1,a3),f4(a2,a3),a6)),
% 59.33/59.37 inference(scs_inference,[],[1433,170,1075,1308,1100,39,1593,1596,1474,1452,1220,141,2,26,3,9,11,14,10])).
% 59.33/59.37 cnf(1598,plain,
% 59.33/59.37 (E(x15981,f4(x15981,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1599,plain,
% 59.33/59.37 (P2(f4(f4(a3,a3),a3),a3,f8(x15991,a3))),
% 59.33/59.37 inference(scs_inference,[],[1433,170,1075,1308,1100,39,1593,1596,1598,1474,1452,1220,141,2,26,3,9,11,14,10,12])).
% 59.33/59.37 cnf(1602,plain,
% 59.33/59.37 (P2(f4(a3,a3),f8(a3,x16021),f8(a3,x16022))),
% 59.33/59.37 inference(scs_inference,[],[929,1433,1250,1571,170,1075,1308,1100,39,1593,1596,1598,1474,1452,1220,141,2,26,3,9,11,14,10,12,13,28])).
% 59.33/59.37 cnf(1622,plain,
% 59.33/59.37 (E(f8(x16221,a3),f4(f8(a3,x16222),f8(a3,x16222)))),
% 59.33/59.37 inference(scs_inference,[],[559,1588,1313,2,26])).
% 59.33/59.37 cnf(1623,plain,
% 59.33/59.37 (P1(x16231,f4(a3,a3),f4(f8(a3,x16232),f8(a3,x16232)))),
% 59.33/59.37 inference(rename_variables,[],[1313])).
% 59.33/59.37 cnf(1630,plain,
% 59.33/59.37 (E(x16301,f4(x16301,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1632,plain,
% 59.33/59.37 (E(x16321,f4(x16321,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1633,plain,
% 59.33/59.37 (P2(f4(f8(x16331,a3),a3),f8(x16331,a3),a3)),
% 59.33/59.37 inference(scs_inference,[],[1223,1478,170,559,1153,39,1630,1632,334,1588,1404,1417,1313,2,26,3,9,11,14,12])).
% 59.33/59.37 cnf(1634,plain,
% 59.33/59.37 (E(x16341,f4(x16341,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1636,plain,
% 59.33/59.37 (E(x16361,f4(x16361,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1639,plain,
% 59.33/59.37 (P2(f4(a3,a3),f8(x16391,a3),f8(a3,x16392))),
% 59.33/59.37 inference(scs_inference,[],[941,1223,1478,1383,1571,170,559,1153,1500,39,1630,1632,1634,1636,334,1588,1404,1417,1313,2,26,3,9,11,14,12,10,13,28])).
% 59.33/59.37 cnf(1643,plain,
% 59.33/59.37 (P1(f4(a7,a3),f4(a3,a3),f8(x16431,a3))),
% 59.33/59.37 inference(scs_inference,[],[941,1223,1478,1383,1571,170,176,559,1153,1500,39,1630,1632,1634,1636,334,1588,1594,1404,1417,1313,1623,2,26,3,9,11,14,12,10,13,28,29])).
% 59.33/59.37 cnf(1656,plain,
% 59.33/59.37 (E(f4(f8(a3,x16561),a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1556,2])).
% 59.33/59.37 cnf(1657,plain,
% 59.33/59.37 (E(a7,f8(f5(a1),f4(a2,a3)))),
% 59.33/59.37 inference(scs_inference,[],[149,22,1556,2,26])).
% 59.33/59.37 cnf(1658,plain,
% 59.33/59.37 (P1(x16581,x16582,f8(x16581,x16582))),
% 59.33/59.37 inference(rename_variables,[],[22])).
% 59.33/59.37 cnf(1660,plain,
% 59.33/59.37 (E(a3,f4(f8(a3,x16601),f8(a3,x16601)))),
% 59.33/59.37 inference(scs_inference,[],[170,149,22,1556,1622,2,26,3])).
% 59.33/59.37 cnf(1663,plain,
% 59.33/59.37 (E(x16631,f4(x16631,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1665,plain,
% 59.33/59.37 (E(x16651,f4(x16651,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1666,plain,
% 59.33/59.37 (P1(x16661,f8(x16662,a3),f4(f8(x16663,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[170,149,1382,22,1068,39,1663,1643,1556,1622,2,26,3,9,11,10])).
% 59.33/59.37 cnf(1667,plain,
% 59.33/59.37 (P2(f8(x16671,a3),f4(f8(x16672,a3),f8(x16672,a3)),a3)),
% 59.33/59.37 inference(scs_inference,[],[1254,170,149,1382,22,1068,39,1663,1643,1556,1622,2,26,3,9,11,10,12])).
% 59.33/59.37 cnf(1669,plain,
% 59.33/59.37 (E(x16691,f4(x16691,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1672,plain,
% 59.33/59.37 (P2(f4(a3,a3),a3,f8(a3,x16721))),
% 59.33/59.37 inference(scs_inference,[],[941,1254,1478,1504,1072,1571,170,149,1382,22,1068,39,1663,1665,1669,1643,1556,1622,2,26,3,9,11,10,12,14,13,28])).
% 59.33/59.37 cnf(1677,plain,
% 59.33/59.37 (P1(a7,a3,f8(f5(a1),f8(x16771,a3)))),
% 59.33/59.37 inference(scs_inference,[],[941,1254,1478,1504,1072,1571,170,149,1382,22,44,1068,39,1663,1665,1669,1643,1556,1622,2,26,3,9,11,10,12,14,13,28,29])).
% 59.33/59.37 cnf(1689,plain,
% 59.33/59.37 (P2(f4(a3,a3),f4(a3,a3),f4(f8(x16891,a3),f8(x16891,a3)))),
% 59.33/59.37 inference(scs_inference,[],[533,941,1254,1478,1504,1072,1571,170,21,149,697,730,278,342,1382,22,1658,44,1068,741,39,1663,1665,1669,1643,1556,1622,2,26,3,9,11,10,12,14,13,28,29,30,32,31])).
% 59.33/59.37 cnf(1692,plain,
% 59.33/59.37 (E(f5(a3),f8(x16921,f8(x16922,a3)))),
% 59.33/59.37 inference(scs_inference,[],[1455,2])).
% 59.33/59.37 cnf(1693,plain,
% 59.33/59.37 (E(f4(a3,a3),f8(f8(a3,x16931),f8(a3,x16932)))),
% 59.33/59.37 inference(scs_inference,[],[730,1455,1083,2,26])).
% 59.33/59.37 cnf(1696,plain,
% 59.33/59.37 (E(f8(x16961,a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[730,604,1455,1525,1083,2,26,3])).
% 59.33/59.37 cnf(1699,plain,
% 59.33/59.37 (E(x16991,f4(x16991,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1700,plain,
% 59.33/59.37 (P1(x17001,f4(f8(x17002,a3),a3),f8(x17003,a3))),
% 59.33/59.37 inference(scs_inference,[],[170,730,847,39,1597,604,1455,1525,1083,2,26,3,9,11])).
% 59.33/59.37 cnf(1702,plain,
% 59.33/59.37 (E(x17021,f4(x17021,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1703,plain,
% 59.33/59.37 (P2(f8(x17031,a3),f5(a3),f8(x17032,a3))),
% 59.33/59.37 inference(scs_inference,[],[1478,1110,170,730,847,39,1699,1597,604,1455,1525,1083,2,26,3,9,11,12,14])).
% 59.33/59.37 cnf(1705,plain,
% 59.33/59.37 (E(x17051,f4(x17051,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1711,plain,
% 59.33/59.37 (P1(a7,f4(a3,a3),f8(f5(a1),f8(a3,x17111)))),
% 59.33/59.37 inference(scs_inference,[],[153,1478,1510,1110,1689,170,149,730,44,847,1071,741,39,1699,1702,1705,1597,604,1455,1525,1083,2,26,3,9,11,12,14,10,13,28,29])).
% 59.33/59.37 cnf(1730,plain,
% 59.33/59.37 (E(f4(a3,a3),f4(f8(a3,x17301),f8(a3,x17301)))),
% 59.33/59.37 inference(scs_inference,[],[1075,1693,1125,2,26])).
% 59.33/59.37 cnf(1734,plain,
% 59.33/59.37 (E(x17341,f4(x17341,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1735,plain,
% 59.33/59.37 (E(f5(a3),f8(x17351,f4(a3,a3)))),
% 59.33/59.37 inference(scs_inference,[],[1075,39,1693,1526,1290,1125,376,2,26,9,3])).
% 59.33/59.37 cnf(1736,plain,
% 59.33/59.37 (P1(x17361,f4(a3,a3),f8(x17362,a3))),
% 59.33/59.37 inference(scs_inference,[],[170,1075,220,39,1693,1526,1290,1125,376,2,26,9,3,11])).
% 59.33/59.37 cnf(1738,plain,
% 59.33/59.37 (E(x17381,f4(x17381,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1739,plain,
% 59.33/59.37 (P1(f4(a1,a3),f4(a2,a3),f4(a6,a3))),
% 59.33/59.37 inference(scs_inference,[],[1503,170,1075,220,39,1734,1738,1693,1526,1290,1125,376,2,26,9,3,11,14,10])).
% 59.33/59.37 cnf(1762,plain,
% 59.33/59.37 (E(f4(a3,a3),f8(f8(x17621,a3),f5(a3)))),
% 59.33/59.37 inference(scs_inference,[],[730,1730,267,2,26])).
% 59.33/59.37 cnf(1765,plain,
% 59.33/59.37 (E(f4(a3,a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[730,1730,1525,267,2,26,3])).
% 59.33/59.37 cnf(1769,plain,
% 59.33/59.37 (E(x17691,f4(x17691,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1771,plain,
% 59.33/59.37 (E(x17711,f4(x17711,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1773,plain,
% 59.33/59.37 (E(x17731,f4(x17731,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1774,plain,
% 59.33/59.37 (P2(f8(x17741,a3),f4(a3,a3),a3)),
% 59.33/59.37 inference(scs_inference,[],[1386,170,730,1500,39,1769,1771,1739,1730,1525,267,2,26,3,9,11,10,12])).
% 59.33/59.37 cnf(1776,plain,
% 59.33/59.37 (E(x17761,f4(x17761,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1779,plain,
% 59.33/59.37 (P2(a3,f4(f8(a3,x17791),a3),f8(x17792,a3))),
% 59.33/59.37 inference(scs_inference,[],[1386,1468,1425,860,170,730,1500,39,1769,1771,1773,1776,1739,1730,1525,267,2,26,3,9,11,10,12,14,13,28])).
% 59.33/59.37 cnf(1798,plain,
% 59.33/59.37 (E(f8(f5(a1),f4(a2,a3)),a7)),
% 59.33/59.37 inference(scs_inference,[],[1657,2])).
% 59.33/59.37 cnf(1799,plain,
% 59.33/59.37 (E(a3,f8(f4(a3,a3),x17991))),
% 59.33/59.37 inference(scs_inference,[],[171,1657,210,2,3])).
% 59.33/59.37 cnf(1802,plain,
% 59.33/59.37 (E(x18021,f4(x18021,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1805,plain,
% 59.33/59.37 (P2(f8(a3,x18051),f4(a3,a3),f8(x18052,a3))),
% 59.33/59.37 inference(scs_inference,[],[1262,171,928,39,1802,1657,1711,210,2,3,9,11,12])).
% 59.33/59.37 cnf(1806,plain,
% 59.33/59.37 (P1(f8(x18061,a3),f8(a3,x18062),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1262,171,730,928,39,1802,1657,1711,210,2,3,9,11,12,10])).
% 59.33/59.37 cnf(1812,plain,
% 59.33/59.37 (P1(a7,x18121,f8(f5(a1),f8(a2,x18121)))),
% 59.33/59.37 inference(scs_inference,[],[765,1262,1433,1254,171,21,149,730,42,22,928,39,1802,1657,1711,210,2,3,9,11,12,10,14,13,28,29])).
% 59.33/59.37 cnf(1858,plain,
% 59.33/59.37 (E(f5(a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1765,2])).
% 59.33/59.37 cnf(1859,plain,
% 59.33/59.37 (P1(f4(a7,a3),x18591,f8(f5(a1),f8(a2,x18591)))),
% 59.33/59.37 inference(scs_inference,[],[39,1765,1812,2,9])).
% 59.33/59.37 cnf(1860,plain,
% 59.33/59.37 (E(x18601,f4(x18601,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1862,plain,
% 59.33/59.37 (E(x18621,f4(x18621,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1864,plain,
% 59.33/59.37 (E(x18641,f4(x18641,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1865,plain,
% 59.33/59.37 (P2(f4(f8(x18651,a3),a3),f5(a3),a3)),
% 59.33/59.37 inference(scs_inference,[],[1110,1736,39,1860,1862,1864,1765,1806,1812,2,9,11,10,12])).
% 59.33/59.37 cnf(1866,plain,
% 59.33/59.37 (E(x18661,f4(x18661,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1868,plain,
% 59.33/59.37 (E(x18681,f4(x18681,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1872,plain,
% 59.33/59.37 (P1(f4(x18721,a3),x18722,f8(x18721,x18722))),
% 59.33/59.37 inference(rename_variables,[],[42])).
% 59.33/59.37 cnf(1879,plain,
% 59.33/59.37 (E(f8(a7,x18791),f8(f5(a1),f8(a2,x18791)))),
% 59.33/59.37 inference(scs_inference,[],[1110,1602,149,1075,304,42,1872,662,1736,1328,39,1860,1862,1864,1866,1868,1765,1806,1812,2,9,11,10,12,14,13,29,30,26])).
% 59.33/59.37 cnf(1889,plain,
% 59.33/59.37 (E(f8(x18891,a3),f8(f8(x18892,a3),f5(a3)))),
% 59.33/59.37 inference(scs_inference,[],[474,1735,1762,2,3])).
% 59.33/59.37 cnf(1890,plain,
% 59.33/59.37 (P1(f5(a3),f8(x18901,a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1075,474,1735,1765,1762,2,3,9])).
% 59.33/59.37 cnf(1891,plain,
% 59.33/59.37 (P1(f4(a3,a3),f8(x18911,a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1075,474,1735,1765,1762,2,3,9,11])).
% 59.33/59.37 cnf(1892,plain,
% 59.33/59.37 (P2(f5(a3),f4(a3,a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[765,1075,474,1735,1765,1762,2,3,9,11,12])).
% 59.33/59.37 cnf(1893,plain,
% 59.33/59.37 (P1(x18931,f5(a3),f8(a3,x18932))),
% 59.33/59.37 inference(scs_inference,[],[765,1075,342,474,1735,1765,1762,2,3,9,11,12,10])).
% 59.33/59.37 cnf(1894,plain,
% 59.33/59.37 (P2(f4(a3,a3),f4(a3,a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[765,1075,342,474,1735,1765,1762,2,3,9,11,12,10,14])).
% 59.33/59.37 cnf(1896,plain,
% 59.33/59.37 (P2(f5(a3),f4(a3,a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[765,1075,342,474,1735,1765,1762,2,3,9,11,12,10,14,13,27])).
% 59.33/59.37 cnf(1902,plain,
% 59.33/59.37 (P1(x19021,f8(x19022,a3),f4(f8(x19023,a3),f8(x19023,a3)))),
% 59.33/59.37 inference(rename_variables,[],[1220])).
% 59.33/59.37 cnf(1905,plain,
% 59.33/59.37 (P1(f5(a1),f4(f8(x19051,a3),f8(x19051,a3)),a3)),
% 59.33/59.37 inference(scs_inference,[],[765,21,149,1075,42,618,342,474,1735,1765,1762,1220,1902,2,3,9,11,12,10,14,13,27,28,29,30])).
% 59.33/59.37 cnf(1909,plain,
% 59.33/59.37 (P1(x19091,f5(a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[765,21,149,1075,42,618,342,474,1735,1765,1762,1220,1902,1041,2,3,9,11,12,10,14,13,27,28,29,30,34])).
% 59.33/59.37 cnf(1911,plain,
% 59.33/59.37 (P1(a3,f5(a3),a3)),
% 59.33/59.37 inference(scs_inference,[],[765,1110,21,149,1075,42,618,342,474,1735,1765,1762,1220,1902,1041,2,3,9,11,12,10,14,13,27,28,29,30,34,33])).
% 59.33/59.37 cnf(1914,plain,
% 59.33/59.37 (P2(f5(a3),f5(a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[765,1110,21,149,1075,42,618,342,474,1735,1765,1762,1220,1902,1041,2,3,9,11,12,10,14,13,27,28,29,30,34,33,32])).
% 59.33/59.37 cnf(1923,plain,
% 59.33/59.37 (E(x19231,f4(x19231,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1925,plain,
% 59.33/59.37 (E(x19251,f4(x19251,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1927,plain,
% 59.33/59.37 (E(x19271,f4(x19271,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1929,plain,
% 59.33/59.37 (P1(f4(a7,a3),f8(x19291,a3),f8(f5(a1),f8(a2,a3)))),
% 59.33/59.37 inference(scs_inference,[],[1503,886,170,39,1923,1925,1493,1806,1859,1890,2,9,11,12,14,10])).
% 59.33/59.37 cnf(1933,plain,
% 59.33/59.37 (P1(f5(a3),f4(a3,a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1503,886,170,304,39,1923,1925,1927,1493,1806,1859,1890,1891,2,9,11,12,14,10,13,29])).
% 59.33/59.37 cnf(1937,plain,
% 59.33/59.37 (P1(f5(a1),f4(f8(a3,x19371),f8(a3,x19371)),a3)),
% 59.33/59.37 inference(scs_inference,[],[1503,886,170,149,304,662,39,1923,1925,1927,1125,1493,1806,1859,1890,1891,2,9,11,12,14,10,13,29,30])).
% 59.33/59.37 cnf(1941,plain,
% 59.33/59.37 (P1(f8(x19411,a3),f5(a3),f8(x19411,a3))),
% 59.33/59.37 inference(scs_inference,[],[1503,886,170,149,304,1703,662,39,1923,1925,1927,1125,1493,1806,1859,1890,1891,1893,1909,2,9,11,12,14,10,13,29,30,33])).
% 59.33/59.37 cnf(1955,plain,
% 59.33/59.37 (P1(a1,f4(a2,a3),f4(a6,a3))),
% 59.33/59.37 inference(scs_inference,[],[170,39,1591,1248,1911,2,9,11])).
% 59.33/59.37 cnf(1956,plain,
% 59.33/59.37 (E(x19561,f4(x19561,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1958,plain,
% 59.33/59.37 (E(x19581,f4(x19581,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1960,plain,
% 59.33/59.37 (E(x19601,f4(x19601,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1962,plain,
% 59.33/59.37 (E(x19621,f4(x19621,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(1965,plain,
% 59.33/59.37 (P2(f4(a3,a3),f5(a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1159,1468,1639,1896,170,39,1956,1958,1960,1962,1591,1894,1248,1911,2,9,11,14,12,10,13,28])).
% 59.33/59.37 cnf(1975,plain,
% 59.33/59.37 (P1(f5(a3),f8(x19751,a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1159,1468,1639,1896,170,149,1075,342,44,1666,39,1956,1958,1960,1962,1591,1894,1248,1313,1911,2,9,11,14,12,10,13,28,29,30,33])).
% 59.33/59.37 cnf(1983,plain,
% 59.33/59.37 (E(f8(a3,x19831),f4(f4(a3,a3),f4(a3,a3)))),
% 59.33/59.37 inference(scs_inference,[],[1412,1142,1284,2,3])).
% 59.33/59.37 cnf(2014,plain,
% 59.33/59.37 (E(x20141,f4(x20141,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2017,plain,
% 59.33/59.37 (E(x20171,f4(x20171,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2019,plain,
% 59.33/59.37 (E(x20191,f4(x20191,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2023,plain,
% 59.33/59.37 (P1(a7,f8(x20231,a3),f8(f5(a1),f8(a3,x20232)))),
% 59.33/59.37 inference(scs_inference,[],[1468,1389,1672,170,149,44,1102,39,2014,2017,2019,1236,1905,1597,1933,2,9,11,14,10,12,13,29])).
% 59.33/59.37 cnf(2038,plain,
% 59.33/59.37 (E(x20381,f4(x20381,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2039,plain,
% 59.33/59.37 (P1(x20391,f4(a3,a3),f4(f4(a3,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[39,2038,1622,1041,1941,2,9,11])).
% 59.33/59.37 cnf(2043,plain,
% 59.33/59.37 (P2(f8(a3,x20431),f4(f8(x20432,a3),f8(x20432,a3)),a3)),
% 59.33/59.37 inference(scs_inference,[],[1110,1254,171,854,39,2038,1622,1041,1941,2,9,11,14,10,12])).
% 59.33/59.37 cnf(2045,plain,
% 59.33/59.37 (P2(f8(a3,x20451),f5(a3),f8(a3,x20451))),
% 59.33/59.37 inference(scs_inference,[],[1110,1254,1389,1914,171,854,39,2038,1622,1041,1941,2,9,11,14,10,12,13,27])).
% 59.33/59.37 cnf(2060,plain,
% 59.33/59.37 (E(f4(f8(x20601,a3),a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1587,514,1765,2,3])).
% 59.33/59.37 cnf(2062,plain,
% 59.33/59.37 (P1(f8(x20621,a3),x20622,f8(a3,x20623))),
% 59.33/59.37 inference(scs_inference,[],[1075,278,1587,647,1588,514,1765,2,3,9,11])).
% 59.33/59.37 cnf(2064,plain,
% 59.33/59.37 (P2(a3,a3,f4(f5(x20641),x20641))),
% 59.33/59.37 inference(scs_inference,[],[533,1075,278,876,1587,647,1588,514,1765,2,3,9,11,14])).
% 59.33/59.37 cnf(2084,plain,
% 59.33/59.37 (E(x20841,f4(x20841,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2088,plain,
% 59.33/59.37 (E(x20881,f4(x20881,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2089,plain,
% 59.33/59.37 (P2(f4(f4(a3,a3),a3),a3,a3)),
% 59.33/59.37 inference(scs_inference,[],[1389,1667,170,39,2084,2088,1525,1937,1041,1975,2,9,11,14,10,12])).
% 59.33/59.37 cnf(2090,plain,
% 59.33/59.37 (E(x20901,f4(x20901,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2097,plain,
% 59.33/59.37 (P1(f4(a3,a3),x20971,f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[668,51,1389,1532,1667,170,570,39,2084,2088,2090,1498,1525,1937,1806,1041,1975,2,9,11,14,10,12,13,28,29])).
% 59.33/59.37 cnf(2099,plain,
% 59.33/59.37 (P1(f8(a3,x20991),x20992,f8(a3,x20992))),
% 59.33/59.37 inference(rename_variables,[],[570])).
% 59.33/59.37 cnf(2105,plain,
% 59.33/59.37 (P1(f8(x21051,a3),x21052,f8(x21051,a3))),
% 59.33/59.37 inference(scs_inference,[],[668,857,51,1389,1532,1667,170,149,570,2099,22,39,2084,2088,2090,1498,1525,1937,1806,1041,1975,1909,2,9,11,14,10,12,13,28,29,30,33])).
% 59.33/59.37 cnf(2115,plain,
% 59.33/59.37 (E(x21151,f4(x21151,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2117,plain,
% 59.33/59.37 (E(x21171,f4(x21171,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2120,plain,
% 59.33/59.37 (E(x21201,f4(x21201,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2122,plain,
% 59.33/59.37 (E(x21221,f4(x21221,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2129,plain,
% 59.33/59.37 (P1(f8(x21291,a3),f4(f8(x21292,a3),f8(x21292,a3)),a3)),
% 59.33/59.37 inference(scs_inference,[],[1532,1602,321,170,1308,278,529,696,39,2115,2117,2120,2122,736,1526,1893,1891,2,9,11,14,10,12,13,29,30])).
% 59.33/59.37 cnf(2143,plain,
% 59.33/59.37 (E(f8(f8(a3,x21431),x21432),f8(a3,x21432))),
% 59.33/59.37 inference(scs_inference,[],[42,925,1879,2129,1005,2,26])).
% 59.33/59.37 cnf(2145,plain,
% 59.33/59.37 (P1(f4(x21451,a3),x21452,f8(x21451,x21452))),
% 59.33/59.37 inference(rename_variables,[],[42])).
% 59.33/59.37 cnf(2147,plain,
% 59.33/59.37 (E(f4(f8(a3,x21471),a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[42,925,1656,1765,1879,2129,1005,2,26,3])).
% 59.33/59.37 cnf(2148,plain,
% 59.33/59.37 (P1(f4(a3,a3),x21481,f8(f8(a3,x21482),x21481))),
% 59.33/59.37 inference(scs_inference,[],[42,2145,925,1656,1765,1879,2129,1005,2,26,3,9])).
% 59.33/59.37 cnf(2152,plain,
% 59.33/59.37 (P2(a3,a3,f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[668,42,2145,434,925,1656,1559,1765,1879,2129,1005,2,26,3,9,11,14])).
% 59.33/59.37 cnf(2157,plain,
% 59.33/59.37 (P2(f5(a3),f8(a3,x21571),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[765,668,158,171,42,2145,434,1066,925,1656,1559,1490,1765,1879,2129,1005,2,26,3,9,11,14,10,13,12,27])).
% 59.33/59.37 cnf(2177,plain,
% 59.33/59.37 (E(f8(x21771,f4(a3,a3)),f8(x21772,a3))),
% 59.33/59.37 inference(scs_inference,[],[42,1736,1889,2,26])).
% 59.33/59.37 cnf(2181,plain,
% 59.33/59.37 (P1(f4(f8(x21811,a3),a3),x21812,f8(a3,x21813))),
% 59.33/59.37 inference(scs_inference,[],[42,1736,39,2062,1889,2,26,9])).
% 59.33/59.37 cnf(2207,plain,
% 59.33/59.37 (P1(f4(f4(a3,a3),a3),x22071,f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[39,2097,1983,2,9])).
% 59.33/59.37 cnf(2208,plain,
% 59.33/59.37 (E(x22081,f4(x22081,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2209,plain,
% 59.33/59.37 (P1(f8(x22091,a3),x22092,f4(f8(a3,x22093),a3))),
% 59.33/59.37 inference(scs_inference,[],[39,2208,2062,2097,1983,2,9,11])).
% 59.33/59.37 cnf(2210,plain,
% 59.33/59.37 (E(x22101,f4(x22101,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2212,plain,
% 59.33/59.37 (P1(f8(a3,x22121),f8(a3,x22122),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1386,171,1114,39,2208,2062,2097,1983,2,9,11,14,10])).
% 59.33/59.37 cnf(2216,plain,
% 59.33/59.37 (P1(a3,a3,f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[1386,1774,171,1308,1114,521,39,2208,2210,2062,2097,1983,2,9,11,14,10,12,13,29])).
% 59.33/59.37 cnf(2236,plain,
% 59.33/59.37 (E(f8(f8(x22361,a3),x22362),f8(a3,x22363))),
% 59.33/59.37 inference(scs_inference,[],[42,2060,2181,2,26])).
% 59.33/59.37 cnf(2238,plain,
% 59.33/59.37 (P1(f4(x22381,a3),x22382,f8(x22381,x22382))),
% 59.33/59.37 inference(rename_variables,[],[42])).
% 59.33/59.37 cnf(2240,plain,
% 59.33/59.37 (E(f8(x22401,a3),f4(f4(a3,a3),f4(a3,a3)))),
% 59.33/59.37 inference(scs_inference,[],[42,474,1284,2060,2181,2,26,3])).
% 59.33/59.37 cnf(2241,plain,
% 59.33/59.37 (P1(f8(a3,x22411),x22412,f8(f8(a3,x22413),x22412))),
% 59.33/59.37 inference(scs_inference,[],[42,2238,1283,474,1284,2060,2181,2,26,3,9])).
% 59.33/59.37 cnf(2243,plain,
% 59.33/59.37 (P1(f8(a3,x22431),f4(a3,a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[42,2238,652,1283,1696,474,1284,2060,2181,2,26,3,9,11])).
% 59.33/59.37 cnf(2245,plain,
% 59.33/59.37 (E(f8(x22451,a3),f5(a3))),
% 59.33/59.37 inference(rename_variables,[],[1696])).
% 59.33/59.37 cnf(2252,plain,
% 59.33/59.37 (P2(f8(a3,x22521),f5(a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[765,941,808,42,2238,652,342,1283,1696,2245,1693,474,1284,2060,2181,2,26,3,9,11,14,10,12,13,28])).
% 59.33/59.37 cnf(2274,plain,
% 59.33/59.37 (E(f8(a3,x22741),f8(f8(a3,x22742),x22741))),
% 59.33/59.37 inference(scs_inference,[],[2143,2])).
% 59.33/59.37 cnf(2275,plain,
% 59.33/59.37 (P1(f4(f8(x22751,a3),a3),x22752,f8(x22751,a3))),
% 59.33/59.37 inference(scs_inference,[],[39,2105,2143,2,9])).
% 59.33/59.37 cnf(2276,plain,
% 59.33/59.37 (E(x22761,f4(x22761,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2278,plain,
% 59.33/59.37 (E(x22781,f4(x22781,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2281,plain,
% 59.33/59.37 (E(x22811,f4(x22811,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2289,plain,
% 59.33/59.37 (P1(a3,a3,f8(x22891,f8(a3,x22892)))),
% 59.33/59.37 inference(scs_inference,[],[345,1672,321,1633,2157,170,1308,569,39,2276,2278,2281,1244,1933,2105,2143,788,2,9,11,14,10,12,13,27,29])).
% 59.33/59.37 cnf(2305,plain,
% 59.33/59.37 (E(f8(f4(a3,a3),x23051),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[42,2147,2207,2,26])).
% 59.33/59.37 cnf(2310,plain,
% 59.33/59.37 (E(x23101,f4(x23101,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2312,plain,
% 59.33/59.37 (E(x23121,f4(x23121,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2314,plain,
% 59.33/59.37 (E(x23141,f4(x23141,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2316,plain,
% 59.33/59.37 (E(x23161,f4(x23161,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2328,plain,
% 59.33/59.37 (P1(f8(a3,x23281),x23282,f8(a3,x23281))),
% 59.33/59.37 inference(scs_inference,[],[1478,1639,1072,1805,170,149,278,42,521,2062,39,2310,2312,2314,2316,1955,2097,1890,2147,1083,2207,2212,2,26,9,11,14,10,12,13,29,30,33])).
% 59.33/59.37 cnf(2335,plain,
% 59.33/59.37 (E(a3,f8(f8(a3,x23351),x23352))),
% 59.33/59.37 inference(scs_inference,[],[171,2177,2274,2,3])).
% 59.33/59.37 cnf(2339,plain,
% 59.33/59.37 (P1(x23391,a3,f4(f5(x23392),x23392))),
% 59.33/59.37 inference(scs_inference,[],[171,42,521,1287,427,2177,2274,2,3,9,11])).
% 59.33/59.37 cnf(2340,plain,
% 59.33/59.37 (P1(x23401,a3,f8(x23402,a3))),
% 59.33/59.37 inference(rename_variables,[],[521])).
% 59.33/59.37 cnf(2341,plain,
% 59.33/59.37 (E(f8(a3,x23411),f4(f5(x23412),x23412))),
% 59.33/59.37 inference(rename_variables,[],[427])).
% 59.33/59.37 cnf(2346,plain,
% 59.33/59.37 (P2(f8(x23461,a3),f4(a3,a3),f4(a3,a3))),
% 59.33/59.37 inference(scs_inference,[],[765,941,171,42,521,652,1287,300,427,2341,2177,2274,2,3,9,11,14,10,12])).
% 59.33/59.37 cnf(2348,plain,
% 59.33/59.37 (P1(a7,f4(a3,a3),f8(f5(a1),f4(a3,a3)))),
% 59.33/59.37 inference(scs_inference,[],[765,941,171,149,42,521,652,44,1287,300,427,2341,2039,2177,2274,2,3,9,11,14,10,12,13,29])).
% 59.33/59.37 cnf(2356,plain,
% 59.33/59.37 (P1(a3,x23561,a3)),
% 59.33/59.37 inference(scs_inference,[],[765,941,1395,171,149,42,521,2340,652,44,1287,300,427,2341,2097,2039,2177,267,2274,2,3,9,11,14,10,12,13,29,30,33])).
% 59.33/59.37 cnf(2368,plain,
% 59.33/59.37 (E(x23681,f4(x23681,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2370,plain,
% 59.33/59.37 (E(x23701,f4(x23701,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2373,plain,
% 59.33/59.37 (E(x23731,f4(x23731,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2374,plain,
% 59.33/59.37 (P2(f8(x23741,a3),f4(f8(a3,x23742),f8(a3,x23742)),a3)),
% 59.33/59.37 inference(scs_inference,[],[323,1429,170,39,2368,2370,2105,1975,2328,2240,2,9,11,14,10,12])).
% 59.33/59.37 cnf(2379,plain,
% 59.33/59.37 (P1(f8(x23791,a3),x23792,f4(f8(x23791,a3),f8(x23791,a3)))),
% 59.33/59.37 inference(rename_variables,[],[278])).
% 59.33/59.37 cnf(2386,plain,
% 59.33/59.37 (P1(f5(a3),x23861,f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[323,1805,1429,170,149,1894,278,2379,618,39,2368,2370,2373,2105,2097,1975,2328,2240,1400,2,9,11,14,10,12,13,29,30,33])).
% 59.33/59.37 cnf(2398,plain,
% 59.33/59.37 (E(x23981,f4(x23981,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2399,plain,
% 59.33/59.37 (P1(f4(a3,a3),x23991,f4(f4(a3,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[39,2398,2097,2236,2243,2,9,11])).
% 59.33/59.37 cnf(2400,plain,
% 59.33/59.37 (E(x24001,f4(x24001,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2403,plain,
% 59.33/59.37 (E(x24031,f4(x24031,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2405,plain,
% 59.33/59.37 (P2(f4(f8(x24051,a3),a3),f4(a3,a3),a3)),
% 59.33/59.37 inference(scs_inference,[],[976,1774,1250,171,39,2398,2400,2403,2097,1891,2236,2243,2,9,11,14,10,13,12])).
% 59.33/59.37 cnf(2409,plain,
% 59.33/59.37 (P1(x24091,f4(f8(a3,a3),f8(a3,a3)),a3)),
% 59.33/59.37 inference(rename_variables,[],[1308])).
% 59.33/59.37 cnf(2417,plain,
% 59.33/59.37 (P2(a3,a3,f4(f4(a3,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[976,1774,1250,171,21,1308,2409,278,521,662,39,2398,2400,2403,2097,1891,2236,2243,788,1929,2,9,11,14,10,13,12,29,30,31])).
% 59.33/59.37 cnf(2422,plain,
% 59.33/59.37 (E(f4(a3,a3),f8(f4(a3,a3),x24221))),
% 59.33/59.37 inference(scs_inference,[],[2305,2])).
% 59.33/59.37 cnf(2423,plain,
% 59.33/59.37 (E(a3,f4(f4(a3,a3),a3))),
% 59.33/59.37 inference(scs_inference,[],[1308,2305,2399,2,26])).
% 59.33/59.37 cnf(2425,plain,
% 59.33/59.37 (P1(x24251,f4(f8(a3,a3),f8(a3,a3)),a3)),
% 59.33/59.37 inference(rename_variables,[],[1308])).
% 59.33/59.37 cnf(2427,plain,
% 59.33/59.37 (P1(f8(x24271,a3),x24272,a3)),
% 59.33/59.37 inference(scs_inference,[],[170,1308,2356,2305,2399,2,26,9])).
% 59.33/59.37 cnf(2429,plain,
% 59.33/59.37 (E(x24291,f4(x24291,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2431,plain,
% 59.33/59.37 (E(x24311,f4(x24311,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2432,plain,
% 59.33/59.37 (P1(x24321,f4(f5(a3),a3),f5(a3))),
% 59.33/59.37 inference(scs_inference,[],[1914,170,1308,39,2429,2431,1890,1909,2356,2305,2399,2,26,9,11,14,10])).
% 59.33/59.37 cnf(2433,plain,
% 59.33/59.37 (E(x24331,f4(x24331,a3))),
% 59.33/59.37 inference(rename_variables,[],[39])).
% 59.33/59.37 cnf(2437,plain,
% 59.33/59.37 (P1(a3,a3,f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[1343,1805,1914,170,1308,2425,521,39,2429,2431,2433,1890,1909,2356,2386,2305,2399,2,26,9,11,14,10,12,13,29])).
% 59.33/59.38 cnf(2462,plain,
% 59.33/59.38 (P2(f8(x24621,a3),a3,f8(x24622,a3))),
% 59.33/59.38 inference(rename_variables,[],[988])).
% 59.33/59.38 cnf(2465,plain,
% 59.33/59.38 (P2(f8(x24651,f8(x24652,a3)),a3,f8(x24653,a3))),
% 59.33/59.38 inference(scs_inference,[],[988,2462,42,529,843,135,255,962,1334,2,9,11,14,10,12])).
% 59.33/59.38 cnf(2468,plain,
% 59.33/59.38 (P2(f5(a3),f4(a3,a3),a3)),
% 59.33/59.38 inference(scs_inference,[],[153,988,2462,1395,1896,20,42,529,843,135,255,1371,962,1334,2,9,11,14,10,12,13,27])).
% 59.33/59.38 cnf(2471,plain,
% 59.33/59.38 (P1(a7,a3,f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[153,988,2462,1395,1896,20,149,42,529,843,135,255,1371,962,1334,2432,2339,2,9,11,14,10,12,13,27,29])).
% 59.33/59.38 cnf(2484,plain,
% 59.33/59.38 (P1(f8(a3,x24841),x24842,a3)),
% 59.33/59.38 inference(scs_inference,[],[171,2356,2423,2,9])).
% 59.33/59.38 cnf(2486,plain,
% 59.33/59.38 (E(x24861,f4(x24861,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2488,plain,
% 59.33/59.38 (P1(a3,f8(a3,x24881),f4(a3,a3))),
% 59.33/59.38 inference(scs_inference,[],[1667,171,39,2328,2356,2216,2423,2,9,11,14,10])).
% 59.33/59.38 cnf(2492,plain,
% 59.33/59.38 (P1(a3,f8(f4(a3,a3),f4(a3,a3)),f4(a3,a3))),
% 59.33/59.38 inference(scs_inference,[],[1667,1343,1914,171,1308,696,39,2486,2097,2328,2356,2216,2423,2,9,11,14,10,12,13,29])).
% 59.33/59.38 cnf(2508,plain,
% 59.33/59.38 (E(x25081,f4(x25081,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2510,plain,
% 59.33/59.38 (E(x25101,f4(x25101,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2511,plain,
% 59.33/59.38 (P2(f5(a3),f4(a3,a3),f4(f5(a3),a3))),
% 59.33/59.38 inference(scs_inference,[],[1896,39,2508,2510,1893,2386,1799,2,9,11,14])).
% 59.33/59.38 cnf(2512,plain,
% 59.33/59.38 (E(x25121,f4(x25121,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2513,plain,
% 59.33/59.38 (P1(a3,f8(x25131,a3),f4(a3,a3))),
% 59.33/59.38 inference(scs_inference,[],[1896,170,39,2508,2510,1893,2386,2216,1799,2,9,11,14,10])).
% 59.33/59.38 cnf(2514,plain,
% 59.33/59.38 (P2(f4(f5(a3),a3),f4(a3,a3),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[1896,170,39,2508,2510,2512,1893,2386,2216,1799,2,9,11,14,10,12])).
% 59.33/59.38 cnf(2532,plain,
% 59.33/59.38 (E(f8(f8(x25321,a3),x25322),f8(x25321,a3))),
% 59.33/59.38 inference(scs_inference,[],[42,2275,1190,2,26])).
% 59.33/59.38 cnf(2534,plain,
% 59.33/59.38 (P1(f4(x25341,a3),x25342,f8(x25341,x25342))),
% 59.33/59.38 inference(rename_variables,[],[42])).
% 59.33/59.38 cnf(2536,plain,
% 59.33/59.38 (E(f8(x25361,a3),f8(f4(a3,a3),x25362))),
% 59.33/59.38 inference(scs_inference,[],[42,474,2275,2422,1190,2,26,3])).
% 59.33/59.38 cnf(2537,plain,
% 59.33/59.38 (P1(f8(x25371,a3),x25372,f8(f5(a3),x25372))),
% 59.33/59.38 inference(scs_inference,[],[42,2534,840,474,2275,2422,1190,2,26,3,9])).
% 59.33/59.38 cnf(2540,plain,
% 59.33/59.38 (P1(f8(x25401,a3),x25402,f8(x25403,a3))),
% 59.33/59.38 inference(scs_inference,[],[278,42,2534,840,217,474,2275,2422,1190,2,26,3,9,11])).
% 59.33/59.38 cnf(2544,plain,
% 59.33/59.38 (P1(x25441,f8(x25442,f8(a3,x25443)),a3)),
% 59.33/59.38 inference(scs_inference,[],[533,278,42,2534,618,840,1186,217,474,2275,2422,1190,2,26,3,9,11,14,10])).
% 59.33/59.38 cnf(2546,plain,
% 59.33/59.38 (P2(f8(a3,x25461),f4(a3,a3),f8(a3,x25462))),
% 59.33/59.38 inference(scs_inference,[],[533,1478,278,42,2534,618,840,1186,217,474,1371,2275,2422,1190,2,26,3,9,11,14,10,12])).
% 59.33/59.38 cnf(2568,plain,
% 59.33/59.38 (E(f4(a3,a3),f4(f5(x25681),x25681))),
% 59.33/59.38 inference(scs_inference,[],[730,2532,2339,2,26])).
% 59.33/59.38 cnf(2569,plain,
% 59.33/59.38 (P1(x25691,a3,f4(f5(x25692),x25692))),
% 59.33/59.38 inference(rename_variables,[],[2339])).
% 59.33/59.38 cnf(2572,plain,
% 59.33/59.38 (E(x25721,f4(x25721,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2574,plain,
% 59.33/59.38 (E(x25741,f4(x25741,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2576,plain,
% 59.33/59.38 (E(x25761,f4(x25761,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2578,plain,
% 59.33/59.38 (E(x25781,f4(x25781,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2584,plain,
% 59.33/59.38 (P2(f4(a3,a3),f4(a3,a3),f4(f5(x25841),x25841))),
% 59.33/59.38 inference(scs_inference,[],[857,1262,1110,1250,1892,170,730,39,2572,2574,2576,2578,1891,2212,2427,2532,2511,2339,2569,2,26,9,11,14,10,12,13,28,32])).
% 59.33/59.38 cnf(2600,plain,
% 59.33/59.38 (P1(f4(a7,a3),a3,f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[39,2471,2568,2,9])).
% 59.33/59.38 cnf(2601,plain,
% 59.33/59.38 (E(x26011,f4(x26011,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2603,plain,
% 59.33/59.38 (E(x26031,f4(x26031,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2606,plain,
% 59.33/59.38 (E(x26061,f4(x26061,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2613,plain,
% 59.33/59.38 (P1(a3,f8(f4(a3,a3),f4(a3,a3)),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[1774,1599,1965,2514,2584,171,1308,350,39,2601,2603,2606,2386,2243,2471,2568,2,9,11,14,10,12,13,28,29])).
% 59.33/59.38 cnf(2627,plain,
% 59.33/59.38 (E(f8(a3,x26271),f4(f8(a3,x26272),f8(a3,x26272)))),
% 59.33/59.38 inference(scs_inference,[],[1412,1730,2536,2,3])).
% 59.33/59.38 cnf(2630,plain,
% 59.33/59.38 (E(f8(a3,x26301),f4(f8(x26302,a3),f8(x26302,a3)))),
% 59.33/59.38 inference(rename_variables,[],[564])).
% 59.33/59.38 cnf(2631,plain,
% 59.33/59.38 (P1(x26311,a3,f4(f8(x26312,a3),f8(x26312,a3)))),
% 59.33/59.38 inference(scs_inference,[],[730,521,564,2630,1412,1730,2536,2,3,9,11])).
% 59.33/59.38 cnf(2633,plain,
% 59.33/59.38 (E(f8(a3,x26331),f4(f8(x26332,a3),f8(x26332,a3)))),
% 59.33/59.38 inference(rename_variables,[],[564])).
% 59.33/59.38 cnf(2636,plain,
% 59.33/59.38 (E(f8(a3,x26361),f4(f8(x26362,a3),f8(x26362,a3)))),
% 59.33/59.38 inference(rename_variables,[],[564])).
% 59.33/59.38 cnf(2639,plain,
% 59.33/59.38 (E(f8(a3,x26391),f4(f8(x26392,a3),f8(x26392,a3)))),
% 59.33/59.38 inference(rename_variables,[],[564])).
% 59.33/59.38 cnf(2640,plain,
% 59.33/59.38 (P2(f4(f8(x26401,a3),f8(x26401,a3)),a3,f8(x26402,a3))),
% 59.33/59.38 inference(scs_inference,[],[795,988,730,521,1382,564,2630,2633,2636,2639,1412,1730,2536,2,3,9,11,14,10,12])).
% 59.33/59.38 cnf(2655,plain,
% 59.33/59.38 (P1(a3,x26551,f8(x26552,a3))),
% 59.33/59.38 inference(scs_inference,[],[170,39,2356,2484,2627,2,9,11])).
% 59.33/59.38 cnf(2657,plain,
% 59.33/59.38 (P1(a7,f8(x26571,a3),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[2043,170,39,2356,2471,2484,2627,2,9,11,14,10])).
% 59.33/59.38 cnf(2670,plain,
% 59.33/59.38 (P1(f8(a3,x26701),a3,f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[171,2437,2335,2,9])).
% 59.33/59.38 cnf(2671,plain,
% 59.33/59.38 (P1(a3,x26711,f8(a3,x26712))),
% 59.33/59.38 inference(scs_inference,[],[171,2356,2437,2335,2,9,11])).
% 59.33/59.38 cnf(2673,plain,
% 59.33/59.38 (P1(a7,f8(a3,x26731),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[2043,171,2356,2471,2437,2335,2,9,11,14,10])).
% 59.33/59.38 cnf(2675,plain,
% 59.33/59.38 (E(x26751,f4(x26751,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2676,plain,
% 59.33/59.38 (P2(f5(a3),f4(f4(a3,a3),a3),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[2043,1896,2157,171,2356,39,2675,2471,2437,2335,2,9,11,14,10,12,13])).
% 59.33/59.38 cnf(2697,plain,
% 59.33/59.38 (E(f8(a3,x26971),f4(f4(a3,a3),a3))),
% 59.33/59.38 inference(scs_inference,[],[2062,2039,1660,2,26])).
% 59.33/59.38 cnf(2699,plain,
% 59.33/59.38 (P1(f8(x26991,a3),x26992,f8(a3,x26993))),
% 59.33/59.38 inference(rename_variables,[],[2062])).
% 59.33/59.38 cnf(2702,plain,
% 59.33/59.38 (P1(f8(x27021,a3),x27022,f8(a3,x27023))),
% 59.33/59.38 inference(rename_variables,[],[2062])).
% 59.33/59.38 cnf(2703,plain,
% 59.33/59.38 (P1(f8(a3,x27031),x27032,f8(a3,x27033))),
% 59.33/59.38 inference(scs_inference,[],[2062,2699,529,2039,647,604,1660,2,26,9,11])).
% 59.33/59.38 cnf(2709,plain,
% 59.33/59.38 (P2(f4(f8(x27091,a3),f8(x27091,a3)),a3,f8(a3,x27092))),
% 59.33/59.38 inference(scs_inference,[],[941,988,2062,2699,529,618,2039,647,604,1660,2,26,9,11,14,10,12])).
% 59.33/59.38 cnf(2711,plain,
% 59.33/59.38 (P2(a3,f8(x27111,a3),f4(a3,a3))),
% 59.33/59.38 inference(scs_inference,[],[941,988,1117,2062,2699,529,618,2039,922,647,604,1660,2,26,9,11,14,10,12,13])).
% 59.33/59.38 cnf(2719,plain,
% 59.33/59.38 (P1(f8(x27191,a3),x27192,f8(a3,x27193))),
% 59.33/59.38 inference(rename_variables,[],[2062])).
% 59.33/59.38 cnf(2722,plain,
% 59.33/59.38 (P1(f8(x27221,a3),x27222,f8(a3,x27223))),
% 59.33/59.38 inference(rename_variables,[],[2062])).
% 59.33/59.38 cnf(2725,plain,
% 59.33/59.38 (P2(f8(a3,x27251),f8(a3,x27251),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[941,988,808,1117,1110,17,149,15,2062,2699,2702,2719,2722,278,529,618,2039,922,647,604,1909,2209,2676,1660,2,26,9,11,14,10,12,13,28,29,30,32])).
% 59.33/59.38 cnf(2738,plain,
% 59.33/59.38 (E(a6,f8(a1,a2))),
% 59.33/59.38 inference(scs_inference,[],[1100,42,2697,2,26])).
% 59.33/59.38 cnf(2739,plain,
% 59.33/59.38 (P1(f4(x27391,a3),x27392,f8(x27391,x27392))),
% 59.33/59.38 inference(rename_variables,[],[42])).
% 59.33/59.38 cnf(2741,plain,
% 59.33/59.38 (E(f4(a6,a3),f8(a1,a2))),
% 59.33/59.38 inference(scs_inference,[],[1100,42,98,2697,2,26,3])).
% 59.33/59.38 cnf(2743,plain,
% 59.33/59.38 (P1(f8(x27431,a3),a3,f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[170,1100,42,98,2437,2697,2,26,3,9])).
% 59.33/59.38 cnf(2745,plain,
% 59.33/59.38 (E(x27451,f4(x27451,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2747,plain,
% 59.33/59.38 (P1(a3,f8(x27471,a3),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[1865,170,1100,42,39,98,1909,2437,2697,2,26,3,9,11,14,10])).
% 59.33/59.38 cnf(2755,plain,
% 59.33/59.38 (P1(f4(x27551,a3),x27552,f8(x27551,x27552))),
% 59.33/59.38 inference(rename_variables,[],[42])).
% 59.33/59.38 cnf(2756,plain,
% 59.33/59.38 (P1(x27561,a3,f8(a3,x27562))),
% 59.33/59.38 inference(rename_variables,[],[569])).
% 59.33/59.38 cnf(2759,plain,
% 59.33/59.38 (P1(f8(x27591,a3),x27592,f8(a3,x27593))),
% 59.33/59.38 inference(rename_variables,[],[2062])).
% 59.33/59.38 cnf(2763,plain,
% 59.33/59.38 (P2(x27631,x27632,f4(x27631,x27632))),
% 59.33/59.38 inference(rename_variables,[],[21])).
% 59.33/59.38 cnf(2773,plain,
% 59.33/59.38 (P2(a6,a6,f8(a1,f4(a2,a2)))),
% 59.33/59.38 inference(scs_inference,[],[765,857,1110,1892,1865,1779,17,170,21,2763,149,2062,2759,1100,278,569,2756,42,2739,2755,39,2745,98,1909,2437,267,2697,2,26,3,9,11,14,10,12,13,28,29,30,33,32,31])).
% 59.33/59.38 cnf(2777,plain,
% 59.33/59.38 (E(f8(a1,a2),f4(a6,a3))),
% 59.33/59.38 inference(scs_inference,[],[2741,2])).
% 59.33/59.38 cnf(2778,plain,
% 59.33/59.38 (E(f8(a3,x27781),f8(f8(a3,x27782),x27783))),
% 59.33/59.38 inference(scs_inference,[],[2062,2241,2741,2,26])).
% 59.33/59.38 cnf(2782,plain,
% 59.33/59.38 (E(f4(f8(a1,a2),a3),f4(a6,a3))),
% 59.33/59.38 inference(scs_inference,[],[2062,98,2241,2741,2,26,3])).
% 59.33/59.38 cnf(2785,plain,
% 59.33/59.38 (E(x27851,f4(x27851,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2789,plain,
% 59.33/59.38 (P1(a3,f8(a3,x27891),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[1865,171,2062,39,2785,98,2212,2437,2540,2241,2741,2,26,3,9,11,14,10])).
% 59.33/59.38 cnf(2814,plain,
% 59.33/59.38 (E(f8(a3,x28141),f8(f5(a3),x28142))),
% 59.33/59.38 inference(scs_inference,[],[2062,2537,2782,2,26])).
% 59.33/59.38 cnf(2817,plain,
% 59.33/59.38 (E(a6,f4(f8(a1,a2),a3))),
% 59.33/59.38 inference(scs_inference,[],[2062,39,2537,2782,2,26,3])).
% 59.33/59.38 cnf(2848,plain,
% 59.33/59.38 (E(f8(a1,a2),a6)),
% 59.33/59.38 inference(scs_inference,[],[2738,2])).
% 59.33/59.38 cnf(2849,plain,
% 59.33/59.38 (E(a3,f8(f5(a3),x28491))),
% 59.33/59.38 inference(scs_inference,[],[171,2738,2814,2,3])).
% 59.33/59.38 cnf(2853,plain,
% 59.33/59.38 (E(x28531,f4(x28531,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2856,plain,
% 59.33/59.38 (E(x28561,f4(x28561,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2858,plain,
% 59.33/59.38 (E(x28581,f4(x28581,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2861,plain,
% 59.33/59.38 (P2(f4(a3,a3),f5(a3),a3)),
% 59.33/59.38 inference(scs_inference,[],[1110,1571,1429,2045,2252,171,39,2853,2856,2858,2488,2513,2492,2738,2814,2,3,9,11,14,10,12,13,28])).
% 59.33/59.38 cnf(2880,plain,
% 59.33/59.38 (P1(f8(a3,x28801),x28802,f8(x28803,a3))),
% 59.33/59.38 inference(scs_inference,[],[170,2484,2492,2817,2,9,11])).
% 59.33/59.38 cnf(2883,plain,
% 59.33/59.38 (P1(f4(a7,a3),f8(x28831,a3),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[2045,170,39,2484,2600,2492,2817,2,9,11,14,10])).
% 59.33/59.38 cnf(2902,plain,
% 59.33/59.38 (E(x29021,f4(x29021,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2903,plain,
% 59.33/59.38 (P1(f8(x29031,a3),x29032,f4(f8(x29033,a3),a3))),
% 59.33/59.38 inference(scs_inference,[],[39,2902,2540,2348,2778,2,9,11])).
% 59.33/59.38 cnf(2904,plain,
% 59.33/59.38 (E(x29041,f4(x29041,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2906,plain,
% 59.33/59.38 (E(x29061,f4(x29061,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2909,plain,
% 59.33/59.38 (P1(f4(a7,a3),f8(a3,x29091),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[2157,2546,171,39,2902,2904,2906,2540,2600,2348,2778,2,9,11,14,12,10])).
% 59.33/59.38 cnf(2935,plain,
% 59.33/59.38 (E(x29351,f4(x29351,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2937,plain,
% 59.33/59.38 (E(x29371,f4(x29371,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2939,plain,
% 59.33/59.38 (E(x29391,f4(x29391,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2941,plain,
% 59.33/59.38 (P2(f4(f5(a3),a3),f4(a3,a3),a3)),
% 59.33/59.38 inference(scs_inference,[],[2546,2468,170,39,2935,2937,2939,2655,1033,2703,691,2,9,11,14,10,12])).
% 59.33/59.38 cnf(2950,plain,
% 59.33/59.38 (E(f8(x29501,a3),f4(f4(a3,a3),a3))),
% 59.33/59.38 inference(scs_inference,[],[521,2399,2849,2,26])).
% 59.33/59.38 cnf(2952,plain,
% 59.33/59.38 (P1(x29521,a3,f8(x29522,a3))),
% 59.33/59.38 inference(rename_variables,[],[521])).
% 59.33/59.38 cnf(2955,plain,
% 59.33/59.38 (E(x29551,f4(x29551,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2966,plain,
% 59.33/59.38 (P1(f5(a1),f8(a3,x29661),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[2465,2405,720,171,149,1100,521,2952,42,1893,1909,39,2955,2399,2544,2657,2880,2849,2,26,9,11,14,10,12,13,29,30])).
% 59.33/59.38 cnf(2977,plain,
% 59.33/59.38 (E(x29771,f4(x29771,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2979,plain,
% 59.33/59.38 (E(x29791,f4(x29791,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2987,plain,
% 59.33/59.38 (P1(x29871,a3,f8(x29872,a3))),
% 59.33/59.38 inference(rename_variables,[],[521])).
% 59.33/59.38 cnf(2990,plain,
% 59.33/59.38 (P2(f8(x29901,a3),f8(x29901,a3),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[533,2089,2374,1316,170,521,2987,178,2386,39,2977,2979,2657,2673,2883,1859,2950,2,9,11,14,10,12,13,29,31])).
% 59.33/59.38 cnf(2997,plain,
% 59.33/59.38 (E(x29971,f4(x29971,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(2999,plain,
% 59.33/59.38 (E(x29991,f4(x29991,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(3005,plain,
% 59.33/59.38 (P1(f8(x30051,a3),f4(a3,a3),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[2089,2374,1316,171,521,342,2386,39,2997,2999,2671,2883,2909,877,2,9,11,14,10,12,13,29])).
% 59.33/59.38 cnf(3017,plain,
% 59.33/59.38 (E(x30171,f4(x30171,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(3020,plain,
% 59.33/59.38 (P2(f5(a3),f4(a3,a3),f8(x30201,a3))),
% 59.33/59.38 inference(scs_inference,[],[2468,170,39,3017,2673,2023,1290,2,9,11,14])).
% 59.33/59.38 cnf(3036,plain,
% 59.33/59.38 (E(x30361,f4(x30361,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(3038,plain,
% 59.33/59.38 (E(x30381,f4(x30381,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(3041,plain,
% 59.33/59.38 (E(x30411,f4(x30411,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(3045,plain,
% 59.33/59.38 (P1(a3,f4(a3,a3),f5(a3))),
% 59.33/59.38 inference(scs_inference,[],[2346,2468,2417,171,178,342,2386,39,3036,3038,3041,2703,2909,2966,968,2,9,11,14,10,12,13,29])).
% 59.33/59.38 cnf(3078,plain,
% 59.33/59.38 (E(x30781,f4(x30781,a3))),
% 59.33/59.38 inference(rename_variables,[],[39])).
% 59.33/59.38 cnf(3080,plain,
% 59.33/59.38 (P1(x30801,f8(x30802,a3),f8(x30801,f5(a3)))),
% 59.47/59.38 inference(scs_inference,[],[2941,170,39,2883,267,2613,9,11,14,10])).
% 59.47/59.38 cnf(3081,plain,
% 59.47/59.38 (P2(f4(f4(a3,a3),a3),f5(a3),a3)),
% 59.47/59.38 inference(scs_inference,[],[2861,2941,170,39,3078,2883,267,2613,9,11,14,10,12])).
% 59.47/59.38 cnf(3095,plain,
% 59.47/59.38 (E(x30951,f4(x30951,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3096,plain,
% 59.47/59.38 (P2(f4(a3,a3),f5(a3),f8(a3,x30961))),
% 59.47/59.38 inference(scs_inference,[],[2861,171,39,2909,2289,9,11,14])).
% 59.47/59.38 cnf(3101,plain,
% 59.47/59.38 (P2(a3,f8(x31011,f8(x31012,a3)),f8(x31013,a3))),
% 59.47/59.38 inference(scs_inference,[],[533,808,720,2861,2773,171,39,3095,2909,267,2289,9,11,14,10,12,13,28])).
% 59.47/59.38 cnf(3137,plain,
% 59.47/59.38 (E(x31371,f4(x31371,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3143,plain,
% 59.47/59.38 (P1(a3,x31431,f4(a3,a3))),
% 59.47/59.38 inference(scs_inference,[],[1271,2990,2941,171,2062,618,2097,39,3137,2613,2339,2789,9,11,14,10,12,13,29])).
% 59.47/59.38 cnf(3157,plain,
% 59.47/59.38 (P1(f8(x31571,a3),x31572,f8(a3,x31573))),
% 59.47/59.38 inference(rename_variables,[],[2062])).
% 59.47/59.38 cnf(3158,plain,
% 59.47/59.38 (E(f8(a3,x31581),f5(f8(a3,x31582)))),
% 59.47/59.38 inference(rename_variables,[],[780])).
% 59.47/59.38 cnf(3159,plain,
% 59.47/59.38 (P1(x31591,a3,f5(f8(a3,x31592)))),
% 59.47/59.38 inference(scs_inference,[],[2062,521,780,3158,98,2741,3,9,11])).
% 59.47/59.38 cnf(3161,plain,
% 59.47/59.38 (E(f8(a3,x31611),f5(f8(a3,x31612)))),
% 59.47/59.38 inference(rename_variables,[],[780])).
% 59.47/59.38 cnf(3164,plain,
% 59.47/59.38 (E(f8(a3,x31641),f5(f8(a3,x31642)))),
% 59.47/59.38 inference(rename_variables,[],[780])).
% 59.47/59.38 cnf(3166,plain,
% 59.47/59.38 (P1(x31661,f8(x31662,a3),f8(a3,x31663))),
% 59.47/59.38 inference(rename_variables,[],[843])).
% 59.47/59.38 cnf(3167,plain,
% 59.47/59.38 (E(f8(a3,x31671),f5(f8(a3,x31672)))),
% 59.47/59.38 inference(rename_variables,[],[780])).
% 59.47/59.38 cnf(3170,plain,
% 59.47/59.38 (E(f8(a3,x31701),f5(f8(a3,x31702)))),
% 59.47/59.38 inference(rename_variables,[],[780])).
% 59.47/59.38 cnf(3174,plain,
% 59.47/59.38 (P1(f8(a3,x31741),x31742,f4(a3,a3))),
% 59.47/59.38 inference(scs_inference,[],[1510,941,1167,2062,3157,843,3166,521,2097,780,3158,3161,3164,3167,3170,98,2741,3,9,11,14,10,12,13,29])).
% 59.47/59.38 cnf(3187,plain,
% 59.47/59.38 (P1(f4(a3,a3),x31871,f8(a3,x31872))),
% 59.47/59.38 inference(scs_inference,[],[2097,2471,1331,1371,9,11])).
% 59.47/59.38 cnf(3191,plain,
% 59.47/59.38 (P1(x31911,f8(a3,x31912),f4(a3,a3))),
% 59.47/59.38 inference(scs_inference,[],[1167,2097,2471,1041,1331,1096,1371,9,11,14,10])).
% 59.47/59.38 cnf(3197,plain,
% 59.47/59.38 (P2(f5(a7),f8(f5(a1),f4(a2,a3)),f8(x31971,a3))),
% 59.47/59.38 inference(scs_inference,[],[1167,1262,895,51,20,2097,2471,1041,1798,1331,1099,1096,1371,9,11,14,10,12,13,28])).
% 59.47/59.38 cnf(3212,plain,
% 59.47/59.38 (~E(a6,f5(a7))),
% 59.47/59.38 inference(scs_inference,[],[96,16,170,39,2544,2670,9,11,14])).
% 59.47/59.38 cnf(3221,plain,
% 59.47/59.38 (P1(f8(a3,x32211),x32212,f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[96,2640,3101,3197,16,19,17,170,2356,569,2386,39,2544,2670,2743,9,11,14,10,12,13,28,29])).
% 59.47/59.38 cnf(3232,plain,
% 59.47/59.38 (P2(f8(a3,x32321),a3,f8(a3,x32322))),
% 59.47/59.38 inference(rename_variables,[],[929])).
% 59.47/59.38 cnf(3233,plain,
% 59.47/59.38 (E(f8(x32331,f8(x32332,a3)),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1455])).
% 59.47/59.38 cnf(3234,plain,
% 59.47/59.38 (P1(x32341,f5(a3),a3)),
% 59.47/59.38 inference(scs_inference,[],[929,18,2097,662,1657,1455,3233,300,9,11,14,10])).
% 59.47/59.38 cnf(3236,plain,
% 59.47/59.38 (E(f8(x32361,f8(x32362,a3)),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1455])).
% 59.47/59.38 cnf(3237,plain,
% 59.47/59.38 (P2(f5(a3),a3,f8(a3,x32371))),
% 59.47/59.38 inference(scs_inference,[],[929,3232,18,2097,662,1657,1455,3233,3236,300,9,11,14,10,12])).
% 59.47/59.38 cnf(3259,plain,
% 59.47/59.38 (E(f4(a3,a3),f8(f8(a3,x32591),x32592))),
% 59.47/59.38 inference(scs_inference,[],[2097,2148,26])).
% 59.47/59.38 cnf(3263,plain,
% 59.47/59.38 (E(x32631,f4(x32631,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3265,plain,
% 59.47/59.38 (E(x32651,f4(x32651,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3271,plain,
% 59.47/59.38 (P2(a3,f5(a3),f8(a3,x32711))),
% 59.47/59.38 inference(scs_inference,[],[2640,3101,3081,3237,171,2097,2152,39,3263,3265,2148,2747,2743,3005,26,9,11,10,14,12,13,28])).
% 59.47/59.38 cnf(3295,plain,
% 59.47/59.38 (E(f8(x32951,a3),f8(f8(a3,x32952),x32953))),
% 59.47/59.38 inference(scs_inference,[],[474,3259,2,3])).
% 59.47/59.38 cnf(3296,plain,
% 59.47/59.38 (P1(f5(a3),x32961,a3)),
% 59.47/59.38 inference(scs_inference,[],[2484,1493,474,3259,2,3,9])).
% 59.47/59.38 cnf(3298,plain,
% 59.47/59.38 (E(f8(x32981,f8(a3,x32982)),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1493])).
% 59.47/59.38 cnf(3299,plain,
% 59.47/59.38 (P1(f8(x32991,a3),x32992,f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[2062,2484,1493,3298,474,3259,2,3,9,11])).
% 59.47/59.38 cnf(3301,plain,
% 59.47/59.38 (E(f8(x33011,f8(a3,x33012)),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1493])).
% 59.47/59.38 cnf(3304,plain,
% 59.47/59.38 (E(f8(x33041,f8(a3,x33042)),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1493])).
% 59.47/59.38 cnf(3307,plain,
% 59.47/59.38 (P2(f5(a3),a3,f8(x33071,a3))),
% 59.47/59.38 inference(scs_inference,[],[795,1262,2062,2484,1071,1493,3298,3301,3304,1142,474,3259,2,3,9,11,10,14,12])).
% 59.47/59.38 cnf(3331,plain,
% 59.47/59.38 (E(x33311,f4(x33311,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3333,plain,
% 59.47/59.38 (E(x33331,f4(x33331,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3335,plain,
% 59.47/59.38 (E(x33351,f4(x33351,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3337,plain,
% 59.47/59.38 (E(x33371,f4(x33371,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3338,plain,
% 59.47/59.38 (P2(f4(f5(a3),a3),a3,f8(a3,x33381))),
% 59.47/59.38 inference(scs_inference,[],[3237,39,3331,3333,3335,3337,2789,3045,3174,3295,2,9,11,10,14,12])).
% 59.47/59.38 cnf(3359,plain,
% 59.47/59.38 (E(x33591,f4(x33591,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3361,plain,
% 59.47/59.38 (E(x33611,f4(x33611,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3363,plain,
% 59.47/59.38 (E(x33631,f4(x33631,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3365,plain,
% 59.47/59.38 (E(x33651,f4(x33651,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3369,plain,
% 59.47/59.38 (P2(a3,f4(f5(a3),a3),f8(a3,x33691))),
% 59.47/59.38 inference(scs_inference,[],[2725,3271,3338,171,39,3359,3361,3363,3365,3045,3174,3187,2064,9,11,10,14,12,13,28])).
% 59.47/59.38 cnf(3376,plain,
% 59.47/59.38 (P1(a3,x33761,f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[2725,3271,3338,171,149,2062,618,2386,44,39,3359,3361,3363,3365,1700,3045,3174,3187,2064,9,11,10,14,12,13,28,30,29])).
% 59.47/59.38 cnf(3384,plain,
% 59.47/59.38 (P1(f8(x33841,f8(x33842,a3)),x33843,f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[2386,1692,1412,2422,3,9])).
% 59.47/59.38 cnf(3385,plain,
% 59.47/59.38 (P1(f4(a3,a3),x33851,f8(x33852,a3))),
% 59.47/59.38 inference(scs_inference,[],[2097,2386,1692,1412,300,2422,3,9,11])).
% 59.47/59.38 cnf(3388,plain,
% 59.47/59.38 (P2(f8(x33881,x33882),f4(a3,a3),f8(x33881,x33882))),
% 59.47/59.38 inference(rename_variables,[],[51])).
% 59.47/59.38 cnf(3393,plain,
% 59.47/59.38 (P2(a7,f4(a3,a3),a7)),
% 59.47/59.38 inference(scs_inference,[],[765,617,51,3388,2097,2386,1909,1489,1692,1236,1412,300,2422,3,9,11,10,14,12,13,27])).
% 59.47/59.38 cnf(3398,plain,
% 59.47/59.38 (P1(a6,f8(x33981,a3),f8(a1,f8(a3,x33982)))),
% 59.47/59.38 inference(scs_inference,[],[765,1262,617,51,3388,20,1100,2097,843,2386,42,1909,1489,1692,1236,1412,300,2422,3,9,11,10,14,12,13,27,28,29])).
% 59.47/59.38 cnf(3432,plain,
% 59.47/59.38 (P1(x34321,a3,f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[2062,569,1696,9,11])).
% 59.47/59.38 cnf(3434,plain,
% 59.47/59.38 (E(f8(x34341,a3),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1696])).
% 59.47/59.38 cnf(3437,plain,
% 59.47/59.38 (P2(f8(a3,x34371),f8(x34372,a3),f8(x34373,a3))),
% 59.47/59.38 inference(rename_variables,[],[808])).
% 59.47/59.38 cnf(3440,plain,
% 59.47/59.38 (E(f8(x34401,a3),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1696])).
% 59.47/59.38 cnf(3443,plain,
% 59.47/59.38 (P2(f5(a7),a7,f8(x34431,a3))),
% 59.47/59.38 inference(scs_inference,[],[808,3437,1262,1167,3393,20,2062,569,1893,790,1696,3434,3440,9,11,10,14,12,13,28])).
% 59.47/59.38 cnf(3461,plain,
% 59.47/59.38 (E(x34611,f4(x34611,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3463,plain,
% 59.47/59.38 (E(x34631,f4(x34631,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3465,plain,
% 59.47/59.38 (P2(a7,f4(a3,a3),f4(a7,a3))),
% 59.47/59.38 inference(scs_inference,[],[3393,171,39,3461,3463,2631,3187,3221,9,11,10,14])).
% 59.47/59.38 cnf(3466,plain,
% 59.47/59.38 (E(x34661,f4(x34661,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3467,plain,
% 59.47/59.38 (P2(f4(a7,a3),f4(a3,a3),a7)),
% 59.47/59.38 inference(scs_inference,[],[3393,171,39,3461,3463,3466,2631,3187,3221,9,11,10,14,12])).
% 59.47/59.38 cnf(3470,plain,
% 59.47/59.38 (P2(f4(a7,a3),f4(a3,a3),f4(a7,a3))),
% 59.47/59.38 inference(scs_inference,[],[765,2709,3393,171,39,3461,3463,3466,2631,3187,3221,9,11,10,14,12,13,27])).
% 59.47/59.38 cnf(3641,plain,
% 59.47/59.38 (P1(f8(x36411,a3),x36412,f8(a3,x36413))),
% 59.47/59.38 inference(rename_variables,[],[2062])).
% 59.47/59.38 cnf(3642,plain,
% 59.47/59.38 (E(f8(a3,x36421),f4(f5(x36422),x36422))),
% 59.47/59.38 inference(rename_variables,[],[427])).
% 59.47/59.38 cnf(3647,plain,
% 59.47/59.38 (E(f8(a3,x36471),f4(f5(x36472),x36472))),
% 59.47/59.38 inference(rename_variables,[],[427])).
% 59.47/59.38 cnf(3649,plain,
% 59.47/59.38 (P2(f8(a3,x36491),a3,f8(x36492,a3))),
% 59.47/59.38 inference(rename_variables,[],[795])).
% 59.47/59.38 cnf(3650,plain,
% 59.47/59.38 (E(f8(a3,x36501),f4(f5(x36502),x36502))),
% 59.47/59.38 inference(rename_variables,[],[427])).
% 59.47/59.38 cnf(3653,plain,
% 59.47/59.38 (E(f8(a3,x36531),f4(f5(x36532),x36532))),
% 59.47/59.38 inference(rename_variables,[],[427])).
% 59.47/59.38 cnf(3654,plain,
% 59.47/59.38 (P2(f4(f5(x36541),x36541),a3,f8(x36542,a3))),
% 59.47/59.38 inference(scs_inference,[],[795,3649,1167,2062,3641,1174,427,3642,3647,3650,3653,9,11,10,14,13,12])).
% 59.47/59.38 cnf(3672,plain,
% 59.47/59.38 (E(x36721,f4(x36721,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3674,plain,
% 59.47/59.38 (E(x36741,f4(x36741,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3677,plain,
% 59.47/59.38 (E(x36771,f4(x36771,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3681,plain,
% 59.47/59.38 (P2(f5(a7),f4(a7,a3),f8(x36811,a3))),
% 59.47/59.38 inference(scs_inference,[],[1503,2861,3369,3470,3443,171,39,3672,3674,3677,3191,3159,3385,3465,9,11,10,14,13,12,28])).
% 59.47/59.38 cnf(3701,plain,
% 59.47/59.38 (E(f8(x37011,a3),f4(f5(x37012),x37012))),
% 59.47/59.38 inference(rename_variables,[],[876])).
% 59.47/59.38 cnf(3704,plain,
% 59.47/59.38 (E(f8(x37041,a3),f4(f5(x37042),x37042))),
% 59.47/59.38 inference(rename_variables,[],[876])).
% 59.47/59.38 cnf(3712,plain,
% 59.47/59.38 (P2(a7,f8(x37121,a3),f4(a7,a3))),
% 59.47/59.38 inference(scs_inference,[],[929,1262,808,3681,19,17,2427,342,662,876,3701,3704,9,11,10,14,13,12,28])).
% 59.47/59.38 cnf(3786,plain,
% 59.47/59.38 (E(x37861,f4(x37861,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3792,plain,
% 59.47/59.38 (E(x37921,f4(x37921,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3794,plain,
% 59.47/59.38 (E(x37941,f4(x37941,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(3797,plain,
% 59.47/59.38 (P1(x37971,f8(a3,x37972),f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[3467,3712,171,2540,39,3786,3792,3794,310,3376,3432,1677,12,26,9,14,11,10])).
% 59.47/59.38 cnf(3945,plain,
% 59.47/59.38 (P2(f4(a7,a3),f8(x39451,a3),f4(a7,a3))),
% 59.47/59.38 inference(scs_inference,[],[3712,2039,2386,39,26,12])).
% 59.47/59.38 cnf(3948,plain,
% 59.47/59.38 (P1(f5(a3),x39481,f8(x39482,a3))),
% 59.47/59.38 inference(scs_inference,[],[3712,170,2039,2386,39,3296,2289,26,12,9,11])).
% 59.47/59.38 cnf(3968,plain,
% 59.47/59.38 (P2(f5(a3),f8(a3,x39681),f8(x39682,a3))),
% 59.47/59.38 inference(scs_inference,[],[857,1493,12])).
% 59.47/59.38 cnf(3970,plain,
% 59.47/59.38 (E(f8(x39701,f8(a3,x39702)),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1493])).
% 59.47/59.38 cnf(3973,plain,
% 59.47/59.38 (E(f8(x39731,f8(a3,x39732)),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1493])).
% 59.47/59.38 cnf(3974,plain,
% 59.47/59.38 (P1(x39741,f4(a3,a3),f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[857,342,529,1493,3970,3973,12,9,11])).
% 59.47/59.38 cnf(4051,plain,
% 59.47/59.38 (E(f8(a3,x40511),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1559])).
% 59.47/59.38 cnf(4054,plain,
% 59.47/59.38 (E(f8(a3,x40541),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[1559])).
% 59.47/59.38 cnf(4057,plain,
% 59.47/59.38 (P2(a3,f4(a3,a3),f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[1262,617,936,1559,4051,4054,2903,9,12,11,14])).
% 59.47/59.38 cnf(4171,plain,
% 59.47/59.38 (P1(x41711,f8(x41712,a3),f4(a3,a3))),
% 59.47/59.38 inference(scs_inference,[],[857,1110,1041,482,1142,300,2148,3384,9,12,11,14,10])).
% 59.47/59.38 cnf(4213,plain,
% 59.47/59.38 (P1(f4(a3,a3),x42131,a3)),
% 59.47/59.38 inference(scs_inference,[],[2427,474,9])).
% 59.47/59.38 cnf(4215,plain,
% 59.47/59.38 (P2(f4(a3,a3),f4(f8(x42151,a3),f8(x42151,a3)),a3)),
% 59.47/59.38 inference(scs_inference,[],[1667,2427,474,9,12])).
% 59.47/59.38 cnf(4217,plain,
% 59.47/59.38 (P1(x42171,a3,f4(a3,a3))),
% 59.47/59.38 inference(scs_inference,[],[1667,2427,521,474,9,12,11])).
% 59.47/59.38 cnf(4220,plain,
% 59.47/59.38 (P2(f8(x42201,a3),a3,f4(a3,a3))),
% 59.47/59.38 inference(scs_inference,[],[988,1667,2427,521,1909,790,474,9,12,11,10,14])).
% 59.47/59.38 cnf(4222,plain,
% 59.47/59.38 (P2(f8(x42221,x42222),f8(a3,x42223),f8(x42221,x42222))),
% 59.47/59.38 inference(scs_inference,[],[988,51,1667,2427,521,1909,790,474,1371,9,12,11,10,14,13])).
% 59.47/59.38 cnf(4258,plain,
% 59.47/59.38 (P2(f8(a3,x42581),a3,f4(a3,a3))),
% 59.47/59.38 inference(scs_inference,[],[795,976,2386,1735,1412,1170,9,12,11,10,14])).
% 59.47/59.38 cnf(4291,plain,
% 59.47/59.38 (E(f8(a3,x42911),f8(x42912,f5(a3)))),
% 59.47/59.38 inference(scs_inference,[],[569,267,26])).
% 59.47/59.38 cnf(4335,plain,
% 59.47/59.38 (E(x43351,f4(x43351,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(4341,plain,
% 59.47/59.38 (P2(f5(a7),f4(a7,a3),a3)),
% 59.47/59.38 inference(scs_inference,[],[573,3712,3654,3443,3968,4215,171,1071,39,4335,3080,2289,3398,4291,2,26,9,12,10,14,13,28])).
% 59.47/59.38 cnf(4365,plain,
% 59.47/59.38 (P2(f4(a7,a3),f5(a7),a3)),
% 59.47/59.38 inference(scs_inference,[],[4341,24])).
% 59.47/59.38 cnf(4368,plain,
% 59.47/59.38 (~E(f8(a1,a2),f5(a7))),
% 59.47/59.38 inference(scs_inference,[],[4341,3212,2738,24,2,3])).
% 59.47/59.38 cnf(4369,plain,
% 59.47/59.38 (~P1(f4(a1,a3),f4(a2,a3),f5(a7))),
% 59.47/59.38 inference(scs_inference,[],[4341,3212,2738,1597,24,2,3,26])).
% 59.47/59.38 cnf(4371,plain,
% 59.47/59.38 (~P1(a1,f4(a2,a3),f5(a7))),
% 59.47/59.38 inference(scs_inference,[],[4341,3212,2738,1597,39,24,2,3,26,9])).
% 59.47/59.38 cnf(4372,plain,
% 59.47/59.38 (E(x43721,f4(x43721,a3))),
% 59.47/59.38 inference(rename_variables,[],[39])).
% 59.47/59.38 cnf(4373,plain,
% 59.47/59.38 (P2(f4(a6,a3),f8(a3,x43731),f8(a1,a2))),
% 59.47/59.38 inference(scs_inference,[],[4341,3212,4222,2777,2738,1597,39,24,2,3,26,9,12])).
% 59.47/59.38 cnf(4377,plain,
% 59.47/59.38 (~P2(a7,a6,f8(a3,x43771))),
% 59.47/59.38 inference(scs_inference,[],[23,4341,3212,4222,2777,2738,299,1597,39,4372,24,2,3,26,9,12,10,14])).
% 59.47/59.38 cnf(4378,plain,
% 59.47/59.38 (~P2(a7,f8(a1,a2),a3)),
% 59.47/59.38 inference(scs_inference,[],[23,4341,3212,4222,2777,2848,2738,299,1597,39,4372,24,2,3,26,9,12,10,14,13])).
% 59.47/59.38 cnf(4379,plain,
% 59.47/59.38 (P2(f5(a7),a7,f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[23,4341,3212,4222,4057,2777,2848,2738,299,1597,3467,39,4372,24,2,3,26,9,12,10,14,13,28])).
% 59.47/59.38 cnf(4381,plain,
% 59.47/59.38 (P2(f5(a3),f5(a3),f4(a3,a3))),
% 59.47/59.38 inference(scs_inference,[],[23,4341,3212,4222,4057,3096,2711,2777,2848,2738,299,1597,3467,39,4372,24,2,3,26,9,12,10,14,13,28,27])).
% 59.47/59.38 cnf(4382,plain,
% 59.47/59.38 (P2(f4(a3,a3),f5(a3),f8(a3,x43821))),
% 59.47/59.38 inference(rename_variables,[],[3096])).
% 59.47/59.38 cnf(4386,plain,
% 59.47/59.38 (P1(x43861,f8(x43862,a3),f4(a3,a3))),
% 59.47/59.38 inference(rename_variables,[],[4171])).
% 59.47/59.38 cnf(4389,plain,
% 59.47/59.38 (P1(f5(a3),x43891,f4(a3,a3))),
% 59.47/59.38 inference(scs_inference,[],[23,4341,3212,4213,4222,4171,4057,3096,2711,2777,2848,4217,3797,3376,2738,299,1597,1153,3467,39,4372,24,2,3,26,9,12,10,14,13,28,27,30,29])).
% 59.47/59.38 cnf(4393,plain,
% 59.47/59.38 (P1(f4(a3,a3),x43931,f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[23,4341,3212,4213,4222,4171,4057,3096,2711,2777,2848,4217,3797,3376,2738,2152,299,1597,1153,3467,765,39,4372,24,2,3,26,9,12,10,14,13,28,27,30,29,33])).
% 59.47/59.38 cnf(4395,plain,
% 59.47/59.38 (P2(f4(a3,a3),f8(x43951,a3),f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[23,4341,3212,4213,4258,4222,4171,4386,3948,4057,3096,2711,2777,2848,4217,3974,3797,3376,2738,2152,299,1597,1153,3467,765,39,4372,24,2,3,26,9,12,10,14,13,28,27,30,29,33,31])).
% 59.47/59.38 cnf(4399,plain,
% 59.47/59.38 (P1(x43991,f4(a3,a3),f5(a3))),
% 59.47/59.38 inference(rename_variables,[],[3974])).
% 59.47/59.38 cnf(4409,plain,
% 59.47/59.38 (P1(f4(a1,a3),f4(a2,a3),f8(a1,a2))),
% 59.47/59.38 inference(scs_inference,[],[23,4341,3212,4213,4258,4222,4171,4386,3948,4057,3096,4382,2711,2777,2848,37,4217,3974,4399,3797,3376,2738,2152,299,1597,1153,3467,1736,16,765,39,4372,24,2,3,26,9,12,10,14,13,28,27,30,29,33,31,32,25,11])).
% 59.47/59.38 cnf(4413,plain,
% 59.47/59.38 (P2(f8(a3,x44131),f4(a6,a3),f8(a1,a2))),
% 59.47/59.38 inference(scs_inference,[],[4373,24])).
% 59.47/59.38 cnf(4415,plain,
% 59.47/59.38 (~E(f5(a7),f8(a1,a2))),
% 59.47/59.38 inference(scs_inference,[],[4373,4368,24,2])).
% 59.47/59.38 cnf(4416,plain,
% 59.47/59.38 (~P2(f4(a6,a3),f8(a3,x44161),f5(a7))),
% 59.47/59.38 inference(scs_inference,[],[4373,4368,24,2,25])).
% 59.47/59.38 cnf(4418,plain,
% 59.47/59.38 (~E(f4(a6,a3),f5(a7))),
% 59.47/59.38 inference(scs_inference,[],[4373,4368,2777,24,2,25,3])).
% 59.47/59.38 cnf(4419,plain,
% 59.47/59.38 (~P1(f5(a1),f4(a2,a3),f5(a6))),
% 59.47/59.38 inference(scs_inference,[],[4373,4368,99,2777,1153,24,2,25,3,26])).
% 59.47/59.38 cnf(4427,plain,
% 59.47/59.38 (~P2(f4(a3,a3),f5(a7),a6)),
% 59.47/59.38 inference(scs_inference,[],[23,4373,4368,4365,4378,4377,648,99,2777,3465,2741,1153,98,24,2,25,3,26,12,14,13,28])).
% 59.47/59.38 cnf(4429,plain,
% 59.47/59.38 (~P2(f8(x44291,a3),f5(a6),a7)),
% 59.47/59.38 inference(scs_inference,[],[23,4373,4368,4365,4378,4377,648,99,2777,3465,2741,1159,1153,98,20,24,2,25,3,26,12,14,13,28,27])).
% 59.47/59.38 cnf(4432,plain,
% 59.47/59.38 (~P2(f8(a1,a2),f4(a3,a3),f5(a7))),
% 59.47/59.38 inference(scs_inference,[],[23,4409,4373,4369,4368,4365,4378,4377,648,99,3143,2777,3465,2741,1159,1153,98,20,16,24,2,25,3,26,12,14,13,28,27,33])).
% 59.47/59.38 cnf(4434,plain,
% 59.47/59.38 (P2(x44341,a3,x44341)),
% 59.47/59.38 inference(rename_variables,[],[16])).
% 59.47/59.38 cnf(4441,plain,
% 59.47/59.38 (P1(x44411,a3,f4(a3,a3))),
% 59.47/59.38 inference(rename_variables,[],[4217])).
% 59.47/59.38 cnf(4444,plain,
% 59.47/59.38 (P2(f5(a3),f5(a3),f8(x44441,a3))),
% 59.47/59.38 inference(scs_inference,[],[23,4409,4373,4369,4368,4365,4378,4377,648,99,3143,2777,4217,3974,3299,3465,2741,1159,1244,1153,98,1736,20,16,4434,17,569,24,2,25,3,26,12,14,13,28,27,33,31,34,32])).
% 59.47/59.38 cnf(4452,plain,
% 59.47/59.38 (P1(f8(a1,a2),f5(a3),f4(a3,a3))),
% 59.47/59.38 inference(scs_inference,[],[23,4409,4373,4369,4368,4365,4378,4377,648,99,3143,2777,4217,4441,3974,3234,3299,3465,2741,1159,1244,1153,98,1736,20,16,4434,17,569,24,2,25,3,26,12,14,13,28,27,33,31,34,32,30,29])).
% 59.47/59.38 cnf(4456,plain,
% 59.47/59.38 (P2(f8(x44561,a3),f4(a3,a3),f5(a3))),
% 59.47/59.38 inference(scs_inference,[],[4395,24])).
% 59.47/59.38 cnf(4459,plain,
% 59.47/59.38 (~P2(f5(a7),a3,f8(a1,a2))),
% 59.47/59.38 inference(scs_inference,[],[4395,4415,4418,16,24,2,25])).
% 59.47/59.38 cnf(4460,plain,
% 59.47/59.38 (P2(x44601,a3,x44601)),
% 59.47/59.38 inference(rename_variables,[],[16])).
% 59.47/59.38 cnf(4476,plain,
% 59.47/59.38 (~P2(f4(a7,a3),f4(a3,a3),f5(a6))),
% 59.47/59.38 inference(scs_inference,[],[23,4432,4395,4415,4418,4381,4419,4444,4429,4220,341,3020,1858,3143,3307,4217,376,1153,16,4460,17,24,2,25,12,14,13,28,27,33,34])).
% 59.47/59.38 cnf(4520,plain,
% 59.47/59.38 (P2(f5(x45201),x45201,a3)),
% 59.47/59.38 inference(rename_variables,[],[20])).
% 59.47/59.38 cnf(4523,plain,
% 59.47/59.38 ($false),
% 59.47/59.38 inference(scs_inference,[],[23,4427,4413,4393,4476,4379,4416,4456,4459,4371,690,35,4452,4389,3945,99,3376,2777,1858,4368,3974,1955,1248,2356,18,20,4520,16,19,178,149,24,2,25,9,12,14,13,28,27,30,33,31,32]),
% 59.47/59.38 ['proof']).
% 59.47/59.38 % SZS output end Proof
% 59.47/59.38 % Total time :58.710000s
%------------------------------------------------------------------------------