%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG002-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 : n010.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:33 EDT 2024
% Result : Unsatisfiable 60.18s 60.42s
% Output : CNFRefutation 60.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : RNG002-1 : TPTP v8.2.0. Released v1.0.0.
% 0.11/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n010.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Jun 18 14:06:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.54/0.58 start to proof:theBenchmark
% 60.18/60.41 %-------------------------------------------
% 60.18/60.41 % File :CSE---1.7
% 60.18/60.41 % Problem :theBenchmark
% 60.18/60.41 % Transform :cnf
% 60.18/60.41 % Format :tptp:raw
% 60.18/60.41 % Command :java -jar mcs_scs.jar %d %s
% 60.18/60.41
% 60.18/60.41 % Result :Theorem 59.650000s
% 60.18/60.41 % Output :CNFRefutation 59.650000s
% 60.18/60.41 %-------------------------------------------
% 60.18/60.42 %--------------------------------------------------------------------------
% 60.18/60.42 % File : RNG002-1 : TPTP v8.2.0. Released v1.0.0.
% 60.18/60.42 % Domain : Ring Theory
% 60.18/60.42 % Problem : Right cancellation for addition
% 60.18/60.42 % Version : [MOW76] axioms.
% 60.18/60.42 % English :
% 60.18/60.42
% 60.18/60.42 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 60.18/60.42 % : [OMW76] Overbeek et al. (1976), Complexity and Related Enhance
% 60.18/60.42 % Source : [MOW76]
% 60.18/60.42 % Names : Established lemma [MOW76]
% 60.18/60.42 % : Lemma proved [OMW76]
% 60.18/60.42
% 60.18/60.42 % Status : Unsatisfiable
% 60.18/60.42 % Rating : 0.06 v8.2.0, 0.00 v7.5.0, 0.10 v7.4.0, 0.11 v7.3.0, 0.00 v5.5.0, 0.06 v5.4.0, 0.00 v5.3.0, 0.08 v5.2.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.00 v2.0.0
% 60.18/60.42 % Syntax : Number of clauses : 20 ( 9 unt; 0 nHn; 14 RR)
% 60.18/60.42 % Number of literals : 53 ( 3 equ; 34 neg)
% 60.18/60.42 % Maximal clause size : 5 ( 2 avg)
% 60.18/60.42 % Maximal term depth : 2 ( 1 avg)
% 60.18/60.42 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 60.18/60.42 % Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% 60.18/60.42 % Number of variables : 71 ( 0 sgn)
% 60.18/60.42 % SPC : CNF_UNS_RFO_SEQ_HRN
% 60.18/60.42
% 60.18/60.42 % Comments :
% 60.18/60.42 %--------------------------------------------------------------------------
% 60.18/60.42 %----Include ring theory axioms
% 60.18/60.42 include('Axioms/RNG001-0.ax').
% 60.18/60.42 %--------------------------------------------------------------------------
% 60.18/60.42 cnf(a_plus_b_is_d,hypothesis,
% 60.18/60.42 sum(a,b,d) ).
% 60.18/60.42
% 60.18/60.42 cnf(a_plus_c_is_d,hypothesis,
% 60.18/60.42 sum(a,c,d) ).
% 60.18/60.42
% 60.18/60.42 cnf(prove_b_equals_c,negated_conjecture,
% 60.18/60.42 b != c ).
% 60.18/60.42
% 60.18/60.42 %--------------------------------------------------------------------------
% 60.18/60.42 %-------------------------------------------
% 60.18/60.42 % Proof found
% 60.18/60.42 % SZS status Theorem for theBenchmark
% 60.18/60.42 % SZS output start Proof
% 60.18/60.43 %ClaNum:34(EqnAxiom:14)
% 60.18/60.43 %VarNum:146(SingletonVarNum:71)
% 60.18/60.43 %MaxLitNum:5
% 60.18/60.43 %MaxfuncDepth:1
% 60.18/60.43 %SharedTerms:8
% 60.18/60.43 %goalClause: 23
% 60.18/60.43 %singleGoalClaCount:1
% 60.18/60.43 [15]P1(a1,a2,a6)
% 60.18/60.43 [16]P1(a1,a7,a6)
% 60.18/60.43 [23]~E(a7,a2)
% 60.18/60.43 [17]P1(x171,a3,x171)
% 60.18/60.43 [18]P1(a3,x181,x181)
% 60.18/60.43 [19]P1(x191,f5(x191),a3)
% 60.18/60.43 [20]P1(f5(x201),x201,a3)
% 60.18/60.43 [21]P1(x211,x212,f4(x211,x212))
% 60.18/60.43 [22]P2(x221,x222,f8(x221,x222))
% 60.18/60.43 [24]~P1(x242,x241,x243)+P1(x241,x242,x243)
% 60.18/60.43 [25]~P1(x253,x254,x251)+E(x251,x252)+~P1(x253,x254,x252)
% 60.18/60.43 [26]~P2(x263,x264,x261)+E(x261,x262)+~P2(x263,x264,x262)
% 60.18/60.43 [27]~P1(x276,x274,x271)+P1(x271,x272,x273)+~P1(x274,x272,x275)+~P1(x276,x275,x273)
% 60.18/60.43 [28]~P1(x281,x286,x284)+P1(x281,x282,x283)+~P1(x284,x285,x283)+~P1(x286,x285,x282)
% 60.18/60.43 [29]~P2(x296,x294,x291)+P2(x291,x292,x293)+~P2(x294,x292,x295)+~P2(x296,x295,x293)
% 60.18/60.43 [30]~P2(x301,x306,x304)+P2(x301,x302,x303)+~P2(x304,x305,x303)+~P2(x306,x305,x302)
% 60.18/60.43 [31]~P2(x317,x315,x312)+~P2(x317,x314,x311)+P1(x311,x312,x313)+~P1(x314,x315,x316)+~P2(x317,x316,x313)
% 60.18/60.43 [32]~P2(x325,x327,x322)+~P2(x324,x327,x321)+P1(x321,x322,x323)+~P1(x324,x325,x326)+~P2(x326,x327,x323)
% 60.18/60.43 [33]~P2(x337,x332,x335)+~P2(x336,x332,x334)+P2(x331,x332,x333)+~P1(x334,x335,x333)+~P1(x336,x337,x331)
% 60.18/60.43 [34]~P2(x341,x347,x345)+~P2(x341,x346,x344)+P2(x341,x342,x343)+~P1(x344,x345,x343)+~P1(x346,x347,x342)
% 60.18/60.43 %EqnAxiom
% 60.18/60.43 [1]E(x11,x11)
% 60.18/60.43 [2]E(x22,x21)+~E(x21,x22)
% 60.18/60.43 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.18/60.43 [4]~E(x41,x42)+E(f5(x41),f5(x42))
% 60.18/60.43 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53))
% 60.18/60.43 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62))
% 60.18/60.43 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73))
% 60.18/60.43 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82))
% 60.18/60.43 [9]P1(x92,x93,x94)+~E(x91,x92)+~P1(x91,x93,x94)
% 60.18/60.43 [10]P1(x103,x102,x104)+~E(x101,x102)+~P1(x103,x101,x104)
% 60.18/60.43 [11]P1(x113,x114,x112)+~E(x111,x112)+~P1(x113,x114,x111)
% 60.18/60.43 [12]P2(x122,x123,x124)+~E(x121,x122)+~P2(x121,x123,x124)
% 60.18/60.43 [13]P2(x133,x132,x134)+~E(x131,x132)+~P2(x133,x131,x134)
% 60.18/60.43 [14]P2(x143,x144,x142)+~E(x141,x142)+~P2(x143,x144,x141)
% 60.18/60.43
% 60.18/60.43 %-------------------------------------------
% 60.28/60.44 cnf(35,plain,
% 60.28/60.44 (E(x351,f4(x351,a3))),
% 60.28/60.44 inference(scs_inference,[],[17,21,25])).
% 60.28/60.44 cnf(36,plain,
% 60.28/60.44 (P1(x361,x362,f4(x361,x362))),
% 60.28/60.44 inference(rename_variables,[],[21])).
% 60.28/60.44 cnf(38,plain,
% 60.28/60.44 (P1(f4(x381,a3),a3,x381)),
% 60.28/60.44 inference(scs_inference,[],[17,21,25,9])).
% 60.28/60.44 cnf(40,plain,
% 60.28/60.44 (P1(x401,a3,x401)),
% 60.28/60.44 inference(rename_variables,[],[17])).
% 60.28/60.44 cnf(41,plain,
% 60.28/60.44 (P1(x411,f5(x411),f4(a3,a3))),
% 60.28/60.44 inference(scs_inference,[],[17,21,19,25,9,10,11])).
% 60.28/60.44 cnf(42,plain,
% 60.28/60.44 (P2(f4(a3,a3),x421,f8(a3,x421))),
% 60.28/60.44 inference(scs_inference,[],[17,21,22,19,25,9,10,11,12])).
% 60.28/60.44 cnf(43,plain,
% 60.28/60.44 (P2(x431,x432,f8(x431,x432))),
% 60.28/60.44 inference(rename_variables,[],[22])).
% 60.28/60.44 cnf(44,plain,
% 60.28/60.44 (P2(x441,f4(a3,a3),f8(x441,a3))),
% 60.28/60.44 inference(scs_inference,[],[17,21,22,43,19,25,9,10,11,12,13])).
% 60.28/60.44 cnf(45,plain,
% 60.28/60.44 (P2(x451,x452,f8(x451,x452))),
% 60.28/60.44 inference(rename_variables,[],[22])).
% 60.28/60.44 cnf(46,plain,
% 60.28/60.44 (P1(x461,f4(a3,a3),x461)),
% 60.28/60.44 inference(scs_inference,[],[17,40,21,36,22,43,19,25,9,10,11,12,13,28])).
% 60.28/60.44 cnf(47,plain,
% 60.28/60.44 (P1(x471,x472,f4(x471,x472))),
% 60.28/60.44 inference(rename_variables,[],[21])).
% 60.28/60.45 cnf(49,plain,
% 60.28/60.45 (P1(f8(x491,a3),f8(x491,a3),f8(x491,a3))),
% 60.28/60.45 inference(scs_inference,[],[17,40,21,36,22,43,45,19,25,9,10,11,12,13,28,31])).
% 60.28/60.45 cnf(52,plain,
% 60.28/60.45 (P2(x521,x522,f8(x521,x522))),
% 60.28/60.45 inference(rename_variables,[],[22])).
% 60.28/60.45 cnf(53,plain,
% 60.28/60.45 (P1(x531,a3,x531)),
% 60.28/60.45 inference(rename_variables,[],[17])).
% 60.28/60.45 cnf(55,plain,
% 60.28/60.45 (P1(f8(a3,x551),f8(a3,x551),f8(a3,x551))),
% 60.28/60.45 inference(scs_inference,[],[17,40,53,21,36,22,43,45,52,19,25,9,10,11,12,13,28,31,32])).
% 60.28/60.45 cnf(58,plain,
% 60.28/60.45 (P2(x581,x582,f8(x581,x582))),
% 60.28/60.45 inference(rename_variables,[],[22])).
% 60.28/60.45 cnf(59,plain,
% 60.28/60.45 (P1(x591,a3,x591)),
% 60.28/60.45 inference(rename_variables,[],[17])).
% 60.28/60.45 cnf(61,plain,
% 60.28/60.45 (P2(a3,x611,f4(f8(a3,x611),f8(a3,x611)))),
% 60.28/60.45 inference(scs_inference,[],[17,40,53,59,21,36,47,22,43,45,52,58,19,25,9,10,11,12,13,28,31,32,33])).
% 60.28/60.45 cnf(62,plain,
% 60.28/60.45 (P1(x621,x622,f4(x621,x622))),
% 60.28/60.45 inference(rename_variables,[],[21])).
% 60.28/60.45 cnf(63,plain,
% 60.28/60.45 (P1(x631,a3,x631)),
% 60.28/60.45 inference(rename_variables,[],[17])).
% 60.28/60.45 cnf(65,plain,
% 60.28/60.45 (P2(x651,x652,f8(x651,x652))),
% 60.28/60.45 inference(rename_variables,[],[22])).
% 60.28/60.45 cnf(70,plain,
% 60.28/60.45 (P2(x701,x702,f8(x701,x702))),
% 60.28/60.45 inference(rename_variables,[],[22])).
% 60.28/60.45 cnf(71,plain,
% 60.28/60.45 (P2(x711,x712,f8(x711,x712))),
% 60.28/60.45 inference(rename_variables,[],[22])).
% 60.28/60.45 cnf(74,plain,
% 60.28/60.45 (E(f8(f4(a3,a3),x741),f8(a3,x741))),
% 60.28/60.45 inference(scs_inference,[],[17,40,53,59,63,21,36,47,62,22,43,45,52,58,65,71,19,25,9,10,11,12,13,28,31,32,33,34,2,26])).
% 60.28/60.45 cnf(75,plain,
% 60.28/60.45 (P2(x751,x752,f8(x751,x752))),
% 60.28/60.45 inference(rename_variables,[],[22])).
% 60.28/60.45 cnf(78,plain,
% 60.28/60.45 (P2(f4(a3,a3),f4(a3,a3),f8(a3,a3))),
% 60.28/60.45 inference(scs_inference,[],[17,40,53,59,63,21,36,47,62,22,43,45,52,58,65,71,19,25,9,10,11,12,13,28,31,32,33,34,2,26,3,14])).
% 60.28/60.45 cnf(79,plain,
% 60.28/60.45 (P2(f8(x791,x791),x791,f8(x791,f8(x791,x791)))),
% 60.28/60.45 inference(scs_inference,[],[17,40,53,59,63,21,36,47,62,22,43,45,52,58,65,71,75,70,19,25,9,10,11,12,13,28,31,32,33,34,2,26,3,14,29])).
% 60.28/60.45 cnf(81,plain,
% 60.28/60.45 (P2(x811,x812,f8(x811,x812))),
% 60.28/60.45 inference(rename_variables,[],[22])).
% 60.28/60.45 cnf(82,plain,
% 60.28/60.45 (P2(x821,x822,f8(x821,x822))),
% 60.28/60.45 inference(rename_variables,[],[22])).
% 60.28/60.45 cnf(84,plain,
% 60.28/60.45 (P2(x841,f8(x841,x841),f8(f8(x841,x841),x841))),
% 60.28/60.45 inference(scs_inference,[],[17,40,53,59,63,21,36,47,62,22,43,45,52,58,65,71,75,82,81,70,19,25,9,10,11,12,13,28,31,32,33,34,2,26,3,14,29,30])).
% 60.28/60.45 cnf(90,plain,
% 60.28/60.45 (E(f4(x901,a3),x901)),
% 60.28/60.45 inference(scs_inference,[],[35,2])).
% 60.28/60.45 cnf(93,plain,
% 60.28/60.45 (~E(a7,f4(a2,a3))),
% 60.28/60.45 inference(scs_inference,[],[23,35,84,2,12,3])).
% 60.28/60.45 cnf(94,plain,
% 60.28/60.45 (E(f5(a3),a3)),
% 60.28/60.45 inference(scs_inference,[],[23,35,18,19,84,2,12,3,25])).
% 60.28/60.45 cnf(95,plain,
% 60.28/60.45 (P1(x951,f5(x951),a3)),
% 60.28/60.45 inference(rename_variables,[],[19])).
% 60.28/60.45 cnf(96,plain,
% 60.28/60.45 (P1(a3,x961,x961)),
% 60.28/60.45 inference(rename_variables,[],[18])).
% 60.28/60.45 cnf(99,plain,
% 60.28/60.45 (P1(a3,x991,x991)),
% 60.28/60.45 inference(rename_variables,[],[18])).
% 60.28/60.45 cnf(100,plain,
% 60.28/60.45 (E(x1001,f4(x1001,a3))),
% 60.28/60.45 inference(rename_variables,[],[35])).
% 60.28/60.45 cnf(101,plain,
% 60.28/60.45 (P1(f4(a3,a3),x1011,x1011)),
% 60.28/60.45 inference(scs_inference,[],[23,35,100,18,96,99,19,84,2,12,3,25,10,9])).
% 60.28/60.45 cnf(102,plain,
% 60.28/60.45 (E(x1021,f4(x1021,a3))),
% 60.28/60.45 inference(rename_variables,[],[35])).
% 60.28/60.45 cnf(105,plain,
% 60.28/60.45 (P1(a3,x1051,f4(x1051,a3))),
% 60.28/60.45 inference(scs_inference,[],[23,35,100,102,18,96,99,19,79,84,2,12,3,25,10,9,13,11])).
% 60.28/60.45 cnf(106,plain,
% 60.28/60.45 (P1(a3,x1061,x1061)),
% 60.28/60.45 inference(rename_variables,[],[18])).
% 60.28/60.45 cnf(107,plain,
% 60.28/60.45 (P1(f5(a3),f4(a3,a3),a3)),
% 60.28/60.45 inference(scs_inference,[],[23,35,100,102,18,96,99,106,19,95,79,84,46,2,12,3,25,10,9,13,11,27])).
% 60.28/60.45 cnf(135,plain,
% 60.28/60.45 (E(f8(a3,x1351),f8(f4(a3,a3),x1351))),
% 60.28/60.45 inference(scs_inference,[],[74,2])).
% 60.28/60.45 cnf(136,plain,
% 60.28/60.45 (E(f8(a3,a3),f8(a3,f4(a3,a3)))),
% 60.28/60.45 inference(scs_inference,[],[74,78,42,2,26])).
% 60.28/60.45 cnf(137,plain,
% 60.28/60.45 (P2(f4(a3,a3),x1371,f8(a3,x1371))),
% 60.28/60.45 inference(rename_variables,[],[42])).
% 60.28/60.45 cnf(140,plain,
% 60.28/60.45 (E(x1401,f4(x1401,a3))),
% 60.28/60.45 inference(rename_variables,[],[35])).
% 60.28/60.45 cnf(142,plain,
% 60.28/60.45 (E(f4(x1421,a3),x1421)),
% 60.28/60.45 inference(rename_variables,[],[90])).
% 60.28/60.45 cnf(143,plain,
% 60.28/60.45 (P2(f4(a3,a3),f4(a3,a3),f4(f8(a3,a3),a3))),
% 60.28/60.45 inference(scs_inference,[],[90,74,94,35,140,55,78,42,2,26,10,3,14])).
% 60.28/60.45 cnf(144,plain,
% 60.28/60.45 (E(x1441,f4(x1441,a3))),
% 60.28/60.45 inference(rename_variables,[],[35])).
% 60.28/60.45 cnf(145,plain,
% 60.28/60.45 (E(a3,f5(f4(a3,a3)))),
% 60.28/60.45 inference(scs_inference,[],[90,74,94,35,140,55,19,78,101,42,2,26,10,3,14,25])).
% 60.28/60.45 cnf(147,plain,
% 60.28/60.45 (P1(x1471,f5(x1471),a3)),
% 60.28/60.46 inference(rename_variables,[],[19])).
% 60.28/60.46 cnf(149,plain,
% 60.28/60.46 (P2(f4(a3,a3),x1491,f4(f8(a3,x1491),f8(a3,x1491)))),
% 60.28/60.46 inference(scs_inference,[],[90,74,94,35,140,144,55,19,78,101,42,61,2,26,10,3,14,25,12])).
% 60.28/60.46 cnf(150,plain,
% 60.28/60.46 (E(x1501,f4(x1501,a3))),
% 60.28/60.46 inference(rename_variables,[],[35])).
% 60.28/60.46 cnf(151,plain,
% 60.28/60.46 (P2(f4(a3,a3),x1511,f8(a3,f4(x1511,a3)))),
% 60.28/60.46 inference(scs_inference,[],[90,142,74,94,35,140,144,55,19,78,101,42,137,61,2,26,10,3,14,25,12,13])).
% 60.28/60.46 cnf(154,plain,
% 60.28/60.46 (E(x1541,f4(x1541,a3))),
% 60.28/60.46 inference(rename_variables,[],[35])).
% 60.28/60.46 cnf(157,plain,
% 60.28/60.46 (P1(f8(a3,x1571),a3,a3)),
% 60.28/60.46 inference(scs_inference,[],[90,142,74,94,35,140,144,150,154,55,19,147,78,101,42,137,61,2,26,10,3,14,25,12,13,9,11,28])).
% 60.28/60.46 cnf(160,plain,
% 60.28/60.46 (P1(a3,f8(a3,x1601),a3)),
% 60.28/60.46 inference(scs_inference,[],[90,142,74,94,35,140,144,150,154,55,20,19,147,78,101,42,137,61,2,26,10,3,14,25,12,13,9,11,28,27])).
% 60.28/60.46 cnf(164,plain,
% 60.28/60.46 (P2(f8(a3,a3),f4(a3,a3),f8(f4(a3,a3),f8(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[90,142,74,94,35,140,144,150,154,55,20,19,147,78,101,42,137,61,22,2,26,10,3,14,25,12,13,9,11,28,27,29])).
% 60.28/60.46 cnf(178,plain,
% 60.28/60.46 (E(f8(a3,f4(a3,a3)),f8(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[136,2])).
% 60.28/60.46 cnf(179,plain,
% 60.28/60.46 (E(f8(a3,a3),f8(f4(a3,a3),f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[136,78,22,2,26])).
% 60.28/60.46 cnf(182,plain,
% 60.28/60.46 (P2(f4(a3,a3),x1821,f8(f4(a3,a3),f4(x1821,a3)))),
% 60.28/60.46 inference(scs_inference,[],[136,135,78,151,22,2,26,14])).
% 60.28/60.46 cnf(184,plain,
% 60.28/60.46 (E(f5(a3),f4(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[136,135,18,78,41,151,22,2,26,14,25])).
% 60.28/60.46 cnf(185,plain,
% 60.28/60.46 (P1(x1851,f5(x1851),f4(a3,a3))),
% 60.28/60.46 inference(rename_variables,[],[41])).
% 60.28/60.46 cnf(189,plain,
% 60.28/60.46 (E(f4(x1891,a3),x1891)),
% 60.28/60.46 inference(rename_variables,[],[90])).
% 60.28/60.46 cnf(191,plain,
% 60.28/60.46 (P1(f8(a3,x1911),f8(a3,x1911),f8(a3,x1911))),
% 60.28/60.46 inference(rename_variables,[],[55])).
% 60.28/60.46 cnf(192,plain,
% 60.28/60.46 (E(f4(f5(a3),a3),f4(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[136,135,90,189,55,18,78,41,151,22,2,26,14,25,12,10,3])).
% 60.28/60.46 cnf(193,plain,
% 60.28/60.46 (E(f4(x1931,a3),x1931)),
% 60.28/60.46 inference(rename_variables,[],[90])).
% 60.28/60.46 cnf(194,plain,
% 60.28/60.46 (P1(a1,a7,f4(a6,a3))),
% 60.28/60.46 inference(scs_inference,[],[136,135,90,189,35,55,16,18,78,41,151,22,2,26,14,25,12,10,3,11])).
% 60.28/60.46 cnf(196,plain,
% 60.28/60.46 (P2(f8(a3,a3),a3,f8(f4(a3,a3),f8(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[136,135,90,189,193,35,55,16,18,78,164,41,151,22,2,26,14,25,12,10,3,11,13])).
% 60.28/60.46 cnf(199,plain,
% 60.28/60.46 (P1(f8(a3,x1991),f8(a3,x1991),f8(a3,x1991))),
% 60.28/60.46 inference(rename_variables,[],[55])).
% 60.28/60.46 cnf(200,plain,
% 60.28/60.46 (P1(f8(a3,x2001),f4(a3,a3),f4(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[136,135,90,189,193,35,55,191,199,16,18,78,164,41,185,151,22,2,26,14,25,12,10,3,11,13,9,28])).
% 60.28/60.46 cnf(203,plain,
% 60.28/60.46 (P1(a3,f4(x2031,a3),x2031)),
% 60.28/60.46 inference(scs_inference,[],[136,135,90,189,193,35,55,191,199,16,18,19,20,78,164,41,185,151,38,22,2,26,14,25,12,10,3,11,13,9,28,27])).
% 60.28/60.46 cnf(219,plain,
% 60.28/60.46 (P2(a3,x2191,f8(f4(a3,a3),f4(x2191,a3)))),
% 60.28/60.46 inference(scs_inference,[],[179,90,182,2,12])).
% 60.28/60.46 cnf(220,plain,
% 60.28/60.46 (E(f4(x2201,a3),x2201)),
% 60.28/60.46 inference(rename_variables,[],[90])).
% 60.28/60.46 cnf(221,plain,
% 60.28/60.46 (E(f8(x2211,a3),f4(f8(x2211,a3),f8(x2211,a3)))),
% 60.28/60.46 inference(scs_inference,[],[179,90,49,182,21,2,12,25])).
% 60.28/60.46 cnf(227,plain,
% 60.28/60.46 (P1(f8(x2271,a3),f8(x2271,a3),f8(x2271,a3))),
% 60.28/60.46 inference(rename_variables,[],[49])).
% 60.28/60.46 cnf(229,plain,
% 60.28/60.46 (P1(f8(x2291,a3),f8(x2291,a3),f8(x2291,a3))),
% 60.28/60.46 inference(rename_variables,[],[49])).
% 60.28/60.46 cnf(230,plain,
% 60.28/60.46 (P1(a1,a2,f4(a6,a3))),
% 60.28/60.46 inference(scs_inference,[],[179,90,35,49,227,15,182,21,44,2,12,25,14,10,9,11])).
% 60.28/60.46 cnf(232,plain,
% 60.28/60.46 (P2(f4(a3,a3),a3,f4(f8(a3,a3),a3))),
% 60.28/60.46 inference(scs_inference,[],[179,90,220,35,49,227,15,182,143,21,44,2,12,25,14,10,9,11,13])).
% 60.28/60.46 cnf(234,plain,
% 60.28/60.46 (P1(f8(x2341,a3),a3,a3)),
% 60.28/60.46 inference(scs_inference,[],[179,90,220,35,49,227,229,15,19,182,143,21,44,2,12,25,14,10,9,11,13,28])).
% 60.28/60.46 cnf(249,plain,
% 60.28/60.46 (E(f4(a3,a3),f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[184,2])).
% 60.28/60.46 cnf(250,plain,
% 60.28/60.46 (E(f8(a3,x2501),f4(f8(a3,x2501),f8(a3,x2501)))),
% 60.28/60.46 inference(scs_inference,[],[184,42,149,2,26])).
% 60.28/60.46 cnf(253,plain,
% 60.28/60.46 (E(f5(a3),f5(f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[184,94,145,42,149,2,26,3])).
% 60.28/60.46 cnf(256,plain,
% 60.28/60.46 (P1(a1,f4(a7,a3),a6)),
% 60.28/60.46 inference(scs_inference,[],[184,94,145,90,35,42,16,149,232,2,26,3,12,10])).
% 60.28/60.46 cnf(257,plain,
% 60.28/60.46 (E(x2571,f4(x2571,a3))),
% 60.28/60.46 inference(rename_variables,[],[35])).
% 60.28/60.46 cnf(258,plain,
% 60.28/60.46 (P2(f4(a3,a3),f4(a3,a3),f4(f8(a3,a3),f8(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[184,94,221,145,90,35,42,78,16,149,232,2,26,3,12,10,14])).
% 60.28/60.46 cnf(260,plain,
% 60.28/60.46 (P1(a3,f8(a3,f4(a3,a3)),f8(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[178,184,94,221,145,90,35,42,78,16,18,149,232,2,26,3,12,10,14,11])).
% 60.28/60.46 cnf(262,plain,
% 60.28/60.46 (P1(f4(a1,a3),a7,a6)),
% 60.28/60.46 inference(scs_inference,[],[178,184,94,221,145,90,35,257,42,78,16,18,149,232,2,26,3,12,10,14,11,9])).
% 60.28/60.46 cnf(285,plain,
% 60.28/60.46 (E(a3,f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[94,2])).
% 60.28/60.46 cnf(286,plain,
% 60.28/60.46 (E(f8(a3,x2861),f8(f4(a3,a3),f4(x2861,a3)))),
% 60.28/60.46 inference(scs_inference,[],[94,42,182,2,26])).
% 60.28/60.46 cnf(289,plain,
% 60.28/60.46 (E(a3,f4(f5(a3),a3))),
% 60.28/60.46 inference(scs_inference,[],[94,42,19,182,105,2,26,25])).
% 60.28/60.46 cnf(290,plain,
% 60.28/60.46 (P1(a3,x2901,f4(x2901,a3))),
% 60.28/60.46 inference(rename_variables,[],[105])).
% 60.28/60.46 cnf(291,plain,
% 60.28/60.46 (P1(x2911,f5(x2911),a3)),
% 60.28/60.46 inference(rename_variables,[],[19])).
% 60.28/60.46 cnf(293,plain,
% 60.28/60.46 (E(f4(a3,a3),f5(f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[94,249,253,42,19,182,105,2,26,25,3])).
% 60.28/60.46 cnf(294,plain,
% 60.28/60.46 (P1(a1,f4(a2,a3),a6)),
% 60.28/60.46 inference(scs_inference,[],[94,249,253,35,42,19,15,182,105,2,26,25,3,10])).
% 60.28/60.46 cnf(295,plain,
% 60.28/60.46 (E(x2951,f4(x2951,a3))),
% 60.28/60.46 inference(rename_variables,[],[35])).
% 60.28/60.46 cnf(296,plain,
% 60.28/60.46 (P2(f5(a3),x2961,f8(a3,x2961))),
% 60.28/60.46 inference(scs_inference,[],[94,249,253,35,42,19,15,182,105,2,26,25,3,10,12])).
% 60.28/60.46 cnf(297,plain,
% 60.28/60.46 (P2(f5(a3),f4(a3,a3),f8(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[178,94,249,253,35,42,19,15,182,105,2,26,25,3,10,12,14])).
% 60.28/60.46 cnf(299,plain,
% 60.28/60.46 (P1(f4(a1,a3),a2,a6)),
% 60.28/60.46 inference(scs_inference,[],[178,94,249,253,145,35,295,42,19,291,15,182,105,2,26,25,3,10,12,14,11,9])).
% 60.28/60.46 cnf(301,plain,
% 60.28/60.46 (P2(f4(a3,a3),f5(a3),f8(a3,f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[178,94,249,253,145,35,295,42,19,291,15,182,105,2,26,25,3,10,12,14,11,9,13])).
% 60.28/60.46 cnf(302,plain,
% 60.28/60.46 (P2(f4(a3,a3),x3021,f8(a3,x3021))),
% 60.28/60.46 inference(rename_variables,[],[42])).
% 60.28/60.46 cnf(303,plain,
% 60.28/60.46 (P2(f4(a3,a3),f8(x3031,a3),f8(f8(a3,x3031),f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[178,94,249,253,145,35,295,42,302,22,19,291,15,182,105,44,2,26,25,3,10,12,14,11,9,13,30])).
% 60.28/60.46 cnf(310,plain,
% 60.28/60.46 (P1(x3101,f5(x3101),a3)),
% 60.28/60.46 inference(rename_variables,[],[19])).
% 60.28/60.46 cnf(312,plain,
% 60.28/60.46 (P1(a3,f5(f5(a3)),a3)),
% 60.28/60.46 inference(scs_inference,[],[178,94,249,253,145,35,295,42,302,22,19,291,310,15,18,41,182,105,290,203,44,2,26,25,3,10,12,14,11,9,13,30,28,27])).
% 60.28/60.46 cnf(332,plain,
% 60.28/60.46 (E(f8(f5(a3),x3321),f8(a3,x3321))),
% 60.28/60.46 inference(scs_inference,[],[293,22,296,2,26])).
% 60.28/60.46 cnf(334,plain,
% 60.28/60.46 (P2(x3341,x3342,f8(x3341,x3342))),
% 60.28/60.46 inference(rename_variables,[],[22])).
% 60.28/60.46 cnf(336,plain,
% 60.28/60.46 (P1(f5(f5(a3)),f4(a3,a3),a3)),
% 60.28/60.46 inference(scs_inference,[],[184,293,22,20,296,2,26,10])).
% 60.28/60.46 cnf(337,plain,
% 60.28/60.46 (P1(f5(x3371),x3371,a3)),
% 60.28/60.46 inference(rename_variables,[],[20])).
% 60.28/60.46 cnf(338,plain,
% 60.28/60.46 (E(f8(a3,x3381),f8(a3,f4(x3381,a3)))),
% 60.28/60.46 inference(scs_inference,[],[184,74,293,286,22,20,296,2,26,10,3])).
% 60.28/60.46 cnf(340,plain,
% 60.28/60.46 (P2(f5(a3),f4(a3,a3),f4(f8(a3,a3),f8(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[184,74,293,250,286,22,20,297,296,2,26,10,3,14])).
% 60.28/60.46 cnf(343,plain,
% 60.28/60.46 (P1(x3431,f5(x3431),f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[184,74,293,250,286,285,78,22,19,20,297,296,2,26,10,3,14,12,11])).
% 60.28/60.46 cnf(346,plain,
% 60.28/60.46 (P1(x3461,f5(x3461),a3)),
% 60.28/60.46 inference(rename_variables,[],[19])).
% 60.28/60.46 cnf(347,plain,
% 60.28/60.46 (P2(f4(a3,a3),f8(a3,x3471),f8(f8(a3,a3),x3471))),
% 60.28/60.46 inference(scs_inference,[],[184,74,293,250,286,285,78,42,22,334,19,20,297,296,2,26,10,3,14,12,11,13,9,30])).
% 60.28/60.46 cnf(351,plain,
% 60.28/60.46 (P1(f5(a3),f5(a3),a3)),
% 60.28/60.46 inference(scs_inference,[],[184,74,293,250,286,285,78,42,22,334,19,346,20,337,18,297,296,2,26,10,3,14,12,11,13,9,30,28])).
% 60.28/60.46 cnf(366,plain,
% 60.28/60.46 (P1(f4(a3,a3),x3661,x3661)),
% 60.28/60.46 inference(rename_variables,[],[101])).
% 60.28/60.46 cnf(369,plain,
% 60.28/60.46 (P1(f4(a3,a3),x3691,x3691)),
% 60.28/60.46 inference(rename_variables,[],[101])).
% 60.28/60.46 cnf(370,plain,
% 60.28/60.46 (P2(f4(a3,a3),f5(a3),f8(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[178,192,101,366,19,301,2,25,10,14])).
% 60.28/60.46 cnf(371,plain,
% 60.28/60.46 (P1(f4(a3,a3),f8(a3,f4(a3,a3)),f8(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[178,192,101,366,369,19,301,2,25,10,14,11])).
% 60.28/60.46 cnf(372,plain,
% 60.28/60.46 (P1(f4(a3,a3),x3721,x3721)),
% 60.28/60.46 inference(rename_variables,[],[101])).
% 60.28/60.46 cnf(374,plain,
% 60.28/60.46 (P2(x3741,f5(f4(a3,a3)),f8(x3741,a3))),
% 60.28/60.46 inference(scs_inference,[],[178,192,293,42,44,101,366,369,19,301,2,25,10,14,11,12,13])).
% 60.28/60.46 cnf(375,plain,
% 60.28/60.46 (P1(f5(f4(a3,a3)),x3751,x3751)),
% 60.28/60.46 inference(scs_inference,[],[178,192,293,42,44,101,366,369,372,19,301,2,25,10,14,11,12,13,9])).
% 60.28/60.46 cnf(397,plain,
% 60.28/60.46 (E(f5(f4(a3,a3)),f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[253,2])).
% 60.28/60.46 cnf(398,plain,
% 60.28/60.46 (E(f4(f4(x3981,a3),a3),x3981)),
% 60.28/60.46 inference(scs_inference,[],[253,105,203,2,25])).
% 60.28/60.46 cnf(399,plain,
% 60.28/60.46 (P1(a3,x3991,f4(x3991,a3))),
% 60.28/60.46 inference(rename_variables,[],[105])).
% 60.28/60.46 cnf(402,plain,
% 60.28/60.46 (P1(f4(a3,a3),f4(a3,a3),f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[23,184,253,101,105,203,2,25,3,10])).
% 60.28/60.46 cnf(403,plain,
% 60.28/60.46 (P1(f4(a3,a3),x4031,x4031)),
% 60.28/60.46 inference(rename_variables,[],[101])).
% 60.28/60.46 cnf(407,plain,
% 60.28/60.46 (P1(f4(a3,a3),x4071,x4071)),
% 60.28/60.46 inference(rename_variables,[],[101])).
% 60.28/60.46 cnf(408,plain,
% 60.28/60.46 (P2(f4(a3,a3),f4(a3,a3),f8(f5(a3),a3))),
% 60.28/60.46 inference(scs_inference,[],[23,184,253,35,44,297,101,403,105,203,2,25,3,10,14,11,12])).
% 60.28/60.46 cnf(412,plain,
% 60.28/60.46 (P1(f4(f5(a3),a3),x4121,f4(x4121,a3))),
% 60.28/60.46 inference(scs_inference,[],[23,184,289,253,35,44,42,297,101,403,105,399,203,2,25,3,10,14,11,12,13,9])).
% 60.28/60.46 cnf(413,plain,
% 60.28/60.46 (P1(f4(a3,a3),a3,f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[23,184,289,253,35,44,42,297,101,403,407,105,399,17,20,203,2,25,3,10,14,11,12,13,9,28])).
% 60.28/60.46 cnf(416,plain,
% 60.28/60.46 (P1(x4161,a3,x4161)),
% 60.28/60.46 inference(rename_variables,[],[17])).
% 60.28/60.46 cnf(418,plain,
% 60.28/60.46 (P1(a3,a3,f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[23,184,289,253,35,44,42,297,101,403,407,19,105,399,17,416,20,18,203,2,25,3,10,14,11,12,13,9,28,27])).
% 60.28/60.46 cnf(427,plain,
% 60.28/60.46 (E(x4271,f4(f4(x4271,a3),a3))),
% 60.28/60.46 inference(scs_inference,[],[398,2])).
% 60.28/60.46 cnf(428,plain,
% 60.28/60.46 (P1(x4281,f4(f5(a3),a3),x4281)),
% 60.28/60.46 inference(scs_inference,[],[289,398,17,2,10])).
% 60.28/60.46 cnf(432,plain,
% 60.28/60.46 (P2(a3,f5(a3),f8(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[289,90,35,398,19,17,370,2,10,14,11,12])).
% 60.28/60.46 cnf(433,plain,
% 60.28/60.46 (E(f4(x4331,a3),x4331)),
% 60.28/60.46 inference(rename_variables,[],[90])).
% 60.28/60.46 cnf(436,plain,
% 60.28/60.46 (P1(f8(a3,a3),a3,f8(a3,f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[178,289,90,433,35,398,19,17,370,408,2,10,14,11,12,13,9])).
% 60.28/60.46 cnf(441,plain,
% 60.28/60.46 (P1(x4411,f5(x4411),a3)),
% 60.28/60.46 inference(rename_variables,[],[19])).
% 60.28/60.46 cnf(443,plain,
% 60.28/60.46 (P1(f5(a3),f5(a3),f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[178,289,90,433,35,398,101,19,441,17,18,370,408,413,2,10,14,11,12,13,9,28,27])).
% 60.28/60.46 cnf(446,plain,
% 60.28/60.46 (P2(x4461,f8(a3,a3),x4462)+~P2(f8(x4461,a3),f5(a3),x4462)),
% 60.28/60.46 inference(scs_inference,[],[178,289,90,433,35,398,22,101,19,441,17,18,370,408,413,2,10,14,11,12,13,9,28,27,30])).
% 60.28/60.46 cnf(464,plain,
% 60.28/60.46 (P2(f5(f4(a3,a3)),f5(a3),f8(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[192,293,35,332,22,203,370,432,446,2,14,10,12])).
% 60.28/60.46 cnf(465,plain,
% 60.28/60.46 (P1(f5(x4651),x4651,f5(f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[192,145,293,35,332,22,20,203,370,432,446,2,14,10,12,11])).
% 60.28/60.46 cnf(488,plain,
% 60.28/60.46 (P2(f4(a3,a3),x4881,f8(f5(a3),x4881))),
% 60.28/60.46 inference(scs_inference,[],[184,338,22,2,12])).
% 60.28/60.46 cnf(489,plain,
% 60.28/60.46 (P2(x4891,x4892,f8(x4891,x4892))),
% 60.28/60.46 inference(rename_variables,[],[22])).
% 60.28/60.46 cnf(491,plain,
% 60.28/60.46 (P1(a3,x4911,f4(x4911,a3))),
% 60.28/60.46 inference(rename_variables,[],[105])).
% 60.28/60.46 cnf(494,plain,
% 60.28/60.46 (P2(x4941,f4(a3,a3),f8(x4941,f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[184,338,22,489,105,17,2,12,10,11,13])).
% 60.28/60.46 cnf(497,plain,
% 60.28/60.46 (P1(f4(a3,a3),f4(x4971,a3),x4971)),
% 60.28/60.46 inference(scs_inference,[],[184,289,338,22,489,101,18,105,491,17,2,12,10,11,13,9,28])).
% 60.28/60.46 cnf(501,plain,
% 60.28/60.46 (P2(f8(a3,a3),f4(a3,a3),f8(f5(a3),f8(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[184,289,338,78,22,489,101,18,105,491,17,2,12,10,11,13,9,28,29])).
% 60.28/60.46 cnf(517,plain,
% 60.28/60.46 (E(f8(a3,a3),f8(f5(a3),f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[221,78,488,2,26])).
% 60.28/60.46 cnf(520,plain,
% 60.28/60.46 (P2(f4(a3,a3),f4(a3,a3),f8(f5(a3),f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[184,221,78,488,494,2,26,12])).
% 60.28/60.46 cnf(522,plain,
% 60.28/60.46 (P1(x5221,f5(f4(a3,a3)),x5221)),
% 60.28/60.46 inference(scs_inference,[],[184,293,221,78,46,488,494,2,26,12,10])).
% 60.28/60.46 cnf(525,plain,
% 60.28/60.46 (P2(f5(a3),f4(a3,a3),f8(a3,f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[184,293,221,78,428,46,296,488,494,2,26,12,10,11,13])).
% 60.28/60.46 cnf(528,plain,
% 60.28/60.46 (P1(x5281,f5(x5281),f5(a3))),
% 60.28/60.46 inference(rename_variables,[],[343])).
% 60.28/60.46 cnf(529,plain,
% 60.28/60.46 (P1(f8(a3,x5291),f5(a3),f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[184,293,221,55,78,428,343,528,46,296,488,494,2,26,12,10,11,13,9,28])).
% 60.28/60.46 cnf(544,plain,
% 60.28/60.46 (E(f8(a3,a3),f8(f4(a3,a3),f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[517,78,494,2,26])).
% 60.28/60.46 cnf(547,plain,
% 60.28/60.46 (E(f4(f4(a3,a3),x5471),x5471)),
% 60.28/60.46 inference(scs_inference,[],[517,78,21,101,494,2,26,25])).
% 60.28/60.46 cnf(549,plain,
% 60.28/60.46 (P1(x5491,x5492,f4(x5491,x5492))),
% 60.28/60.46 inference(rename_variables,[],[21])).
% 60.28/60.46 cnf(552,plain,
% 60.28/60.46 (P1(x5521,f4(a3,a3),f4(x5521,f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[23,184,517,78,21,549,101,494,2,26,25,3,10])).
% 60.28/60.46 cnf(553,plain,
% 60.28/60.46 (P1(x5531,x5532,f4(x5531,x5532))),
% 60.28/60.46 inference(rename_variables,[],[21])).
% 60.28/60.46 cnf(556,plain,
% 60.28/60.46 (P1(f4(a3,a3),x5561,f4(f5(a3),x5561))),
% 60.28/60.46 inference(scs_inference,[],[23,184,517,78,21,549,553,46,101,494,2,26,25,3,10,11,9])).
% 60.28/60.46 cnf(557,plain,
% 60.28/60.46 (P1(x5571,x5572,f4(x5571,x5572))),
% 60.28/60.46 inference(rename_variables,[],[21])).
% 60.28/60.46 cnf(558,plain,
% 60.28/60.46 (P1(a3,x5581,f4(a3,f4(x5581,a3)))),
% 60.28/60.46 inference(scs_inference,[],[23,184,517,78,18,21,549,553,557,203,46,101,494,2,26,25,3,10,11,9,28])).
% 60.28/60.46 cnf(578,plain,
% 60.28/60.46 (E(x5781,f4(f4(a3,a3),x5781))),
% 60.28/60.46 inference(scs_inference,[],[547,2])).
% 60.28/60.46 cnf(579,plain,
% 60.28/60.46 (E(f4(f5(x5791),x5791),a3)),
% 60.28/60.46 inference(scs_inference,[],[547,21,20,2,25])).
% 60.28/60.46 cnf(581,plain,
% 60.28/60.46 (P1(x5811,x5812,f4(x5811,x5812))),
% 60.28/60.46 inference(rename_variables,[],[21])).
% 60.28/60.46 cnf(586,plain,
% 60.28/60.46 (P1(f5(f4(a3,a3)),f4(x5861,a3),x5861)),
% 60.28/60.46 inference(scs_inference,[],[184,145,427,547,21,203,443,16,20,2,25,10,11,9])).
% 60.28/60.46 cnf(587,plain,
% 60.28/60.46 (P1(a3,x5871,f4(f4(a3,a3),x5871))),
% 60.28/60.46 inference(scs_inference,[],[184,145,427,547,18,21,581,203,101,443,16,20,2,25,10,11,9,28])).
% 60.28/60.46 cnf(589,plain,
% 60.28/60.46 (P1(a3,x5891,x5891)),
% 60.28/60.46 inference(rename_variables,[],[18])).
% 60.28/60.46 cnf(590,plain,
% 60.28/60.46 (P1(x5901,x5902,f4(x5901,x5902))),
% 60.28/60.46 inference(rename_variables,[],[21])).
% 60.28/60.46 cnf(592,plain,
% 60.28/60.46 (P1(f4(f4(a3,a3),a3),f4(x5921,a3),x5921)),
% 60.28/60.46 inference(scs_inference,[],[184,145,427,547,18,589,21,581,590,203,101,443,16,20,497,2,25,10,11,9,28,27])).
% 60.28/60.46 cnf(609,plain,
% 60.28/60.46 (E(f4(a3,a3),f4(a3,f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[544,18,552,2,25])).
% 60.28/60.46 cnf(611,plain,
% 60.28/60.46 (P1(a3,x6111,x6111)),
% 60.28/60.46 inference(rename_variables,[],[18])).
% 60.28/60.46 cnf(613,plain,
% 60.28/60.46 (E(f5(a3),f4(a3,f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[184,544,18,552,2,25,3])).
% 60.28/60.46 cnf(615,plain,
% 60.28/60.46 (E(x6151,f4(x6151,a3))),
% 60.28/60.46 inference(rename_variables,[],[35])).
% 60.28/60.46 cnf(618,plain,
% 60.28/60.46 (E(x6181,f4(x6181,a3))),
% 60.28/60.46 inference(rename_variables,[],[35])).
% 60.28/60.46 cnf(619,plain,
% 60.28/60.46 (P2(f4(f5(a3),a3),f4(a3,a3),f8(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[184,289,35,615,544,49,42,432,18,552,2,25,3,14,12,10,13])).
% 60.28/60.46 cnf(621,plain,
% 60.28/60.46 (P1(f5(f4(a3,a3)),x6211,x6211)),
% 60.28/60.46 inference(rename_variables,[],[375])).
% 60.28/60.46 cnf(626,plain,
% 60.28/60.46 (P1(a3,x6261,x6261)),
% 60.28/60.46 inference(rename_variables,[],[18])).
% 60.28/60.46 cnf(627,plain,
% 60.28/60.46 (P1(x6271,f4(a3,a3),x6271)),
% 60.28/60.46 inference(rename_variables,[],[46])).
% 60.28/60.46 cnf(629,plain,
% 60.28/60.46 (P1(f4(x6291,a3),f4(a3,a3),x6291)),
% 60.28/60.46 inference(scs_inference,[],[184,289,35,615,618,544,49,42,432,18,611,626,46,627,203,375,621,552,2,25,3,14,12,10,13,11,9,28,27])).
% 60.28/60.46 cnf(641,plain,
% 60.28/60.46 (E(f4(f4(a3,a3),a3),f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[609,428,592,2,25])).
% 60.28/60.46 cnf(650,plain,
% 60.28/60.46 (P1(f4(a3,a3),f5(f5(a3)),f4(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[184,145,35,609,22,428,351,41,375,592,2,25,14,10,11,9])).
% 60.28/60.46 cnf(668,plain,
% 60.28/60.46 (E(f4(a3,a3),f4(f5(a3),f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[613,46,556,2,25])).
% 60.28/60.46 cnf(670,plain,
% 60.28/60.46 (P1(x6701,f4(a3,a3),x6701)),
% 60.28/60.46 inference(rename_variables,[],[46])).
% 60.28/60.46 cnf(672,plain,
% 60.28/60.46 (E(f5(a3),f4(f5(a3),f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[184,613,46,556,2,25,3])).
% 60.28/60.46 cnf(673,plain,
% 60.28/60.46 (P1(f4(x6731,a3),f4(f5(a3),a3),x6731)),
% 60.28/60.46 inference(scs_inference,[],[184,289,613,46,38,556,2,25,3,10])).
% 60.28/60.46 cnf(675,plain,
% 60.28/60.46 (P1(f4(f5(a3),a3),f4(x6751,a3),x6751)),
% 60.28/60.46 inference(scs_inference,[],[184,289,613,203,46,351,38,556,2,25,3,10,11,9])).
% 60.28/60.46 cnf(678,plain,
% 60.28/60.46 (P1(a3,x6781,x6781)),
% 60.28/60.46 inference(rename_variables,[],[18])).
% 60.28/60.46 cnf(680,plain,
% 60.28/60.46 (P1(x6801,f4(a3,a3),f4(x6801,a3))),
% 60.28/60.46 inference(scs_inference,[],[184,289,613,203,18,678,46,670,351,105,38,556,2,25,3,10,11,9,28,27])).
% 60.28/60.46 cnf(696,plain,
% 60.28/60.46 (E(a3,f4(a3,f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[668,203,552,2,25])).
% 60.28/60.46 cnf(730,plain,
% 60.28/60.46 (P1(f4(f4(a1,a3),a3),a2,a6)),
% 60.28/60.46 inference(scs_inference,[],[184,145,427,672,38,522,15,2,10,11,9])).
% 60.28/60.46 cnf(747,plain,
% 60.28/60.46 (E(a3,f4(f4(a3,a3),f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[696,497,552,2,25])).
% 60.28/60.46 cnf(782,plain,
% 60.28/60.46 (P1(x7821,a3,x7821)),
% 60.28/60.46 inference(rename_variables,[],[17])).
% 60.28/60.46 cnf(784,plain,
% 60.28/60.46 (E(f5(a3),f4(a3,f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[94,641,17,558,2,25,3])).
% 60.28/60.46 cnf(786,plain,
% 60.28/60.46 (E(x7861,f4(f4(x7861,a3),a3))),
% 60.28/60.46 inference(rename_variables,[],[427])).
% 60.28/60.46 cnf(788,plain,
% 60.28/60.46 (E(x7881,f4(f4(x7881,a3),a3))),
% 60.28/60.46 inference(rename_variables,[],[427])).
% 60.28/60.46 cnf(789,plain,
% 60.28/60.46 (P1(f4(f4(a1,a3),a3),a7,a6)),
% 60.28/60.46 inference(scs_inference,[],[94,427,786,788,641,17,16,15,558,2,25,3,10,11,9])).
% 60.28/60.46 cnf(791,plain,
% 60.28/60.46 (P1(x7911,f5(a3),x7911)),
% 60.28/60.46 inference(scs_inference,[],[94,427,786,788,641,17,782,428,203,16,15,558,2,25,3,10,11,9,28])).
% 60.28/60.46 cnf(792,plain,
% 60.28/60.46 (P1(a3,f4(x7921,a3),x7921)),
% 60.28/60.46 inference(rename_variables,[],[203])).
% 60.28/60.46 cnf(793,plain,
% 60.28/60.46 (P1(x7931,a3,x7931)),
% 60.28/60.46 inference(rename_variables,[],[17])).
% 60.28/60.46 cnf(795,plain,
% 60.28/60.46 (P1(f4(x7951,a3),f4(f4(a3,a3),a3),x7951)),
% 60.28/60.46 inference(scs_inference,[],[94,427,786,788,641,17,782,793,428,203,792,629,16,15,558,2,25,3,10,11,9,28,27])).
% 60.28/60.46 cnf(803,plain,
% 60.28/60.46 (E(x8031,f4(f4(x8031,a3),a3))),
% 60.28/60.46 inference(rename_variables,[],[427])).
% 60.28/60.46 cnf(804,plain,
% 60.28/60.46 (P1(f4(f4(a1,a3),a3),a7,f4(a6,a3))),
% 60.28/60.46 inference(scs_inference,[],[293,427,803,784,15,107,194,2,10,11,9])).
% 60.28/60.46 cnf(806,plain,
% 60.28/60.46 (P1(f4(x8061,a3),f5(a3),x8061)),
% 60.28/60.46 inference(scs_inference,[],[293,427,803,784,428,38,203,15,107,194,2,10,11,9,28])).
% 60.28/60.46 cnf(808,plain,
% 60.28/60.46 (P1(f4(x8081,a3),a3,x8081)),
% 60.28/60.46 inference(rename_variables,[],[38])).
% 60.28/60.46 cnf(810,plain,
% 60.28/60.46 (P1(f4(a3,a3),a3,f4(f5(a3),f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[293,427,803,784,428,38,808,203,15,107,194,556,2,10,11,9,28,27])).
% 60.28/60.46 cnf(817,plain,
% 60.28/60.46 (E(a3,f4(f4(a3,a3),f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[747,46,587,2,25])).
% 60.28/60.46 cnf(818,plain,
% 60.28/60.46 (P1(a3,x8181,f4(f4(a3,a3),x8181))),
% 60.28/60.46 inference(rename_variables,[],[587])).
% 60.28/60.46 cnf(819,plain,
% 60.28/60.46 (P1(x8191,f4(a3,a3),x8191)),
% 60.28/60.46 inference(rename_variables,[],[46])).
% 60.28/60.46 cnf(821,plain,
% 60.28/60.46 (E(f5(a3),f4(f4(a3,a3),f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[94,747,46,587,2,25,3])).
% 60.28/60.46 cnf(823,plain,
% 60.28/60.46 (E(x8231,f4(f4(x8231,a3),a3))),
% 60.28/60.46 inference(rename_variables,[],[427])).
% 60.28/60.46 cnf(831,plain,
% 60.28/60.46 (P1(x8311,f4(a3,a3),x8311)),
% 60.28/60.46 inference(rename_variables,[],[46])).
% 60.28/60.46 cnf(833,plain,
% 60.28/60.46 (P1(a3,f4(x8331,a3),f4(f4(a3,a3),x8331))),
% 60.28/60.46 inference(scs_inference,[],[192,94,427,823,747,497,46,819,831,101,375,795,230,299,587,818,2,25,3,10,9,11,28,27])).
% 60.28/60.46 cnf(839,plain,
% 60.28/60.46 (E(x8391,f4(a3,f4(x8391,a3)))),
% 60.28/60.46 inference(scs_inference,[],[821,18,558,2,25])).
% 60.28/60.46 cnf(843,plain,
% 60.28/60.46 (E(x8431,f4(f4(x8431,a3),a3))),
% 60.28/60.46 inference(rename_variables,[],[427])).
% 60.28/60.46 cnf(844,plain,
% 60.28/60.46 (P1(f4(a1,a3),a7,f4(f4(a6,a3),a3))),
% 60.28/60.46 inference(scs_inference,[],[427,843,821,18,262,558,2,25,10,11])).
% 60.28/60.46 cnf(857,plain,
% 60.28/60.46 (P1(f8(a3,x8571),f5(f4(a3,a3)),a3)),
% 60.28/60.46 inference(scs_inference,[],[145,817,157,2,10])).
% 60.28/60.46 cnf(858,plain,
% 60.28/60.46 (P1(f8(a3,x8581),a3,f5(f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[145,817,157,2,10,11])).
% 60.28/60.46 cnf(874,plain,
% 60.28/60.46 (P1(f8(x8741,a3),f4(f5(a3),a3),a3)),
% 60.28/60.46 inference(scs_inference,[],[23,289,839,234,2,3,10])).
% 60.28/60.46 cnf(876,plain,
% 60.28/60.46 (E(x8761,f4(x8761,a3))),
% 60.28/60.46 inference(rename_variables,[],[35])).
% 60.28/60.46 cnf(879,plain,
% 60.28/60.46 (P1(f5(f4(a3,a3)),a6,f4(a1,a2))),
% 60.28/60.46 inference(scs_inference,[],[23,289,35,876,839,586,21,256,234,299,2,3,10,11,9,28])).
% 60.28/60.46 cnf(889,plain,
% 60.28/60.46 (E(f5(a3),f4(f5(x8891),x8891))),
% 60.28/60.46 inference(scs_inference,[],[94,579,2,3])).
% 60.28/60.46 cnf(890,plain,
% 60.28/60.46 (P1(a1,f4(a2,a3),f4(a6,a3))),
% 60.28/60.46 inference(scs_inference,[],[94,35,579,230,2,3,10])).
% 60.28/60.46 cnf(891,plain,
% 60.28/60.46 (E(x8911,f4(x8911,a3))),
% 60.28/60.46 inference(rename_variables,[],[35])).
% 60.28/60.46 cnf(893,plain,
% 60.28/60.46 (P1(f4(a1,a3),a7,f4(a6,a3))),
% 60.28/60.46 inference(scs_inference,[],[94,293,35,891,579,194,230,200,2,3,10,11,9])).
% 60.28/60.46 cnf(897,plain,
% 60.28/60.46 (P1(a3,x8971,x8971)),
% 60.28/60.46 inference(rename_variables,[],[18])).
% 60.28/60.46 cnf(900,plain,
% 60.28/60.46 (P1(f5(a3),f4(x9001,a3),x9001)),
% 60.28/60.46 inference(scs_inference,[],[94,293,35,891,579,418,428,18,897,592,203,194,230,200,2,3,10,11,9,28,27])).
% 60.28/60.46 cnf(905,plain,
% 60.28/60.46 (P1(a3,f4(f8(a3,x9051),a3),a3)),
% 60.28/60.46 inference(scs_inference,[],[35,889,160,2,10])).
% 60.28/60.46 cnf(906,plain,
% 60.28/60.46 (E(x9061,f4(x9061,a3))),
% 60.28/60.46 inference(rename_variables,[],[35])).
% 60.28/60.46 cnf(907,plain,
% 60.28/60.46 (P1(a3,f8(a3,x9071),f5(f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[145,35,889,160,2,10,11])).
% 60.28/60.46 cnf(913,plain,
% 60.28/60.46 (P1(f5(a3),a3,f4(f4(a3,a3),f5(a3)))),
% 60.28/60.46 inference(scs_inference,[],[145,35,906,889,418,402,17,294,160,810,587,2,10,11,9,28,27])).
% 60.28/60.46 cnf(919,plain,
% 60.28/60.46 (P1(f8(x9191,a3),a3,f5(f4(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[145,250,234,2,10,11])).
% 60.28/60.46 cnf(937,plain,
% 60.28/60.46 (P2(f5(a3),f5(a3),f8(a3,a3))),
% 60.28/60.46 inference(scs_inference,[],[397,286,464,2,12])).
% 60.28/60.46 cnf(938,plain,
% 60.28/60.46 (P2(x9381,f5(a3),f8(x9381,a3))),
% 60.28/60.46 inference(scs_inference,[],[397,286,464,374,2,12,13])).
% 60.28/60.46 cnf(942,plain,
% 60.28/60.46 (P1(f5(a3),x9421,x9421)),
% 60.28/60.46 inference(scs_inference,[],[293,397,427,286,464,374,375,680,294,2,12,13,10,11,9])).
% 60.28/60.46 cnf(955,plain,
% 60.28/60.46 (P2(f4(a3,a3),f5(a3),f8(f5(a3),a3))),
% 60.28/60.46 inference(scs_inference,[],[184,938,12])).
% 60.28/60.46 cnf(958,plain,
% 60.28/60.46 (E(x9581,f4(f4(x9581,a3),a3))),
% 60.28/60.46 inference(rename_variables,[],[427])).
% 60.28/60.46 cnf(961,plain,
% 60.28/60.46 (P1(f4(a3,a3),x9611,f4(x9611,a3))),
% 60.28/60.46 inference(scs_inference,[],[184,192,427,958,412,194,256,938,12,10,11,9])).
% 60.28/60.46 cnf(979,plain,
% 60.28/60.46 (P1(f5(a3),x9791,f4(x9791,a3))),
% 60.28/60.46 inference(scs_inference,[],[293,90,35,412,937,942,200,14,10,11,9])).
% 60.28/60.46 cnf(981,plain,
% 60.28/60.46 (P1(a3,a3,f8(a3,x9811))),
% 60.28/60.46 inference(scs_inference,[],[293,90,35,418,900,412,937,942,200,905,14,10,11,9,28])).
% 60.28/60.46 cnf(996,plain,
% 60.28/60.46 (P2(f4(a3,a3),f4(a3,a3),f4(f4(a3,a3),f8(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[578,78,46,552,25,14])).
% 60.28/60.46 cnf(997,plain,
% 60.28/60.46 (E(x9971,f4(f4(a3,a3),x9971))),
% 60.28/60.46 inference(rename_variables,[],[578])).
% 60.28/60.46 cnf(999,plain,
% 60.28/60.46 (E(x9991,f4(f4(a3,a3),x9991))),
% 60.28/60.46 inference(rename_variables,[],[578])).
% 60.28/60.46 cnf(1001,plain,
% 60.28/60.46 (E(x10011,f4(f4(a3,a3),x10011))),
% 60.28/60.46 inference(rename_variables,[],[578])).
% 60.28/60.46 cnf(1008,plain,
% 60.28/60.46 (P1(x10081,f4(f4(a3,a3),a3),x10081)),
% 60.28/60.46 inference(scs_inference,[],[578,997,999,1001,78,55,49,38,46,629,203,556,552,25,14,10,11,9,28,27])).
% 60.28/60.46 cnf(1053,plain,
% 60.28/60.46 (E(x10531,f4(f5(a3),f4(x10531,a3)))),
% 60.28/60.46 inference(scs_inference,[],[497,556,25])).
% 60.28/60.46 cnf(1056,plain,
% 60.28/60.46 (P2(f4(a3,a3),f5(a3),f4(f4(a3,a3),f8(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[578,370,497,556,25,14])).
% 60.28/60.46 cnf(1057,plain,
% 60.28/60.46 (E(x10571,f4(f4(a3,a3),x10571))),
% 60.28/60.46 inference(rename_variables,[],[578])).
% 60.28/60.46 cnf(1062,plain,
% 60.28/60.46 (P1(a1,a2,f4(f4(a3,a3),a6))),
% 60.28/60.46 inference(scs_inference,[],[398,578,1057,370,497,592,673,556,15,25,14,10,9,11])).
% 60.28/60.46 cnf(1077,plain,
% 60.28/60.46 (E(x10771,f4(f4(a3,a3),x10771))),
% 60.28/60.46 inference(rename_variables,[],[578])).
% 60.28/60.46 cnf(1078,plain,
% 60.28/60.46 (P1(a1,f4(f4(a3,a3),a2),a6)),
% 60.28/60.46 inference(scs_inference,[],[23,578,1077,1053,22,15,2,3,14,10])).
% 60.28/60.46 cnf(1079,plain,
% 60.28/60.46 (E(x10791,f4(f4(a3,a3),x10791))),
% 60.28/60.46 inference(rename_variables,[],[578])).
% 60.28/60.46 cnf(1084,plain,
% 60.28/60.46 (P1(f5(a3),f4(f4(a3,a3),f5(a3)),f5(a3))),
% 60.28/60.46 inference(scs_inference,[],[23,398,578,1077,1079,1053,22,351,418,795,15,16,913,2,3,14,10,9,11,28])).
% 60.28/60.46 cnf(1091,plain,
% 60.28/60.46 (P2(f5(a3),f4(a3,a3),f4(f4(a3,a3),f8(a3,a3)))),
% 60.28/60.46 inference(scs_inference,[],[578,297,14])).
% 60.28/60.46 cnf(1093,plain,
% 60.28/60.46 (P1(a3,f5(f4(a3,a3)),f8(a3,x10931))),
% 60.28/60.46 inference(scs_inference,[],[145,578,297,981,14,10])).
% 60.28/60.46 cnf(1094,plain,
% 60.28/60.46 (P1(x10941,f5(a3),f4(x10941,a3))),
% 60.28/60.46 inference(scs_inference,[],[398,145,578,297,806,981,14,10,9])).
% 60.28/60.46 cnf(1125,plain,
% 60.28/60.46 (E(f4(x11251,a3),x11251)),
% 60.28/60.46 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1127,plain,
% 60.28/60.47 (E(f4(x11271,a3),x11271)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1128,plain,
% 60.28/60.47 (P1(f5(f5(a3)),a3,a3)),
% 60.28/60.47 inference(scs_inference,[],[90,1125,1127,494,488,336,12,13,10])).
% 60.28/60.47 cnf(1132,plain,
% 60.28/60.47 (P1(f5(x11321),x11321,f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[398,397,90,1125,1127,494,488,791,465,336,12,13,10,9,11])).
% 60.28/60.47 cnf(1133,plain,
% 60.28/60.47 (P1(f4(f5(a3),a3),a6,f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[398,397,90,1125,1127,494,675,488,791,21,465,336,299,12,13,10,9,11,28])).
% 60.28/60.47 cnf(1137,plain,
% 60.28/60.47 (E(f8(x11371,a3),f8(x11371,f5(a3)))),
% 60.28/60.47 inference(scs_inference,[],[398,397,90,1125,1127,22,494,675,488,791,21,465,336,299,12,13,10,9,11,28,26])).
% 60.28/60.47 cnf(1149,plain,
% 60.28/60.47 (P1(f5(f4(a3,a3)),a3,f8(a3,x11491))),
% 60.28/60.47 inference(scs_inference,[],[145,427,1137,981,299,2,10,9])).
% 60.28/60.47 cnf(1162,plain,
% 60.28/60.47 (E(x11621,f4(f4(x11621,a3),f5(a3)))),
% 60.28/60.47 inference(scs_inference,[],[629,552,25])).
% 60.28/60.47 cnf(1165,plain,
% 60.28/60.47 (P2(a3,f5(a3),f8(a3,f4(a3,a3)))),
% 60.28/60.47 inference(scs_inference,[],[90,629,301,552,25,12])).
% 60.28/60.47 cnf(1166,plain,
% 60.28/60.47 (E(f4(x11661,a3),x11661)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1168,plain,
% 60.28/60.47 (E(f4(x11681,a3),x11681)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1170,plain,
% 60.28/60.47 (E(x11701,f4(x11701,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1172,plain,
% 60.28/60.47 (E(f4(x11721,a3),x11721)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1180,plain,
% 60.28/60.47 (P1(f5(a3),a3,f4(f5(a3),f5(a3)))),
% 60.28/60.47 inference(scs_inference,[],[90,1166,1168,1172,35,1170,629,418,619,938,301,981,556,371,200,552,25,12,13,14,10,9,11,28,27])).
% 60.28/60.47 cnf(1186,plain,
% 60.28/60.47 (E(f4(x11861,a3),x11861)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1187,plain,
% 60.28/60.47 (P2(f5(a3),a3,f8(a3,f5(a3)))),
% 60.28/60.47 inference(scs_inference,[],[23,90,1186,1162,525,1056,2,3,12,13])).
% 60.28/60.47 cnf(1190,plain,
% 60.28/60.47 (E(x11901,f4(x11901,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1192,plain,
% 60.28/60.47 (E(x11921,f4(x11921,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1195,plain,
% 60.28/60.47 (P1(f5(a3),f4(f5(a3),f5(a3)),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[23,90,1186,35,1190,1192,1162,351,418,525,1056,230,789,730,1180,2,3,12,13,10,9,11,28])).
% 60.28/60.47 cnf(1201,plain,
% 60.28/60.47 (P2(a3,f5(a3),f8(f5(a3),a3))),
% 60.28/60.47 inference(scs_inference,[],[90,955,12])).
% 60.28/60.47 cnf(1202,plain,
% 60.28/60.47 (E(f4(x12021,a3),x12021)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1207,plain,
% 60.28/60.47 (P1(f5(f4(a3,a3)),f8(a3,x12071),a3)),
% 60.28/60.47 inference(scs_inference,[],[90,1202,145,35,340,955,160,893,12,13,10,9])).
% 60.28/60.47 cnf(1213,plain,
% 60.28/60.47 (E(f4(x12131,a3),x12131)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1217,plain,
% 60.28/60.47 (E(x12171,f4(x12171,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1220,plain,
% 60.28/60.47 (P1(f5(x12201),x12201,f4(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[90,1213,184,35,1217,1091,234,804,1132,258,12,13,10,9,11])).
% 60.28/60.47 cnf(1224,plain,
% 60.28/60.47 (P2(a3,f4(a3,a3),f8(f5(a3),f5(a3)))),
% 60.28/60.47 inference(scs_inference,[],[90,520,12])).
% 60.28/60.47 cnf(1225,plain,
% 60.28/60.47 (E(f4(x12251,a3),x12251)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1228,plain,
% 60.28/60.47 (P1(f8(a3,x12281),f4(a3,a3),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[90,1225,184,996,529,520,12,13,10])).
% 60.28/60.47 cnf(1236,plain,
% 60.28/60.47 (E(f4(x12361,a3),x12361)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1239,plain,
% 60.28/60.47 (P1(a3,f5(f5(a3)),f4(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[90,1236,184,35,650,879,501,1187,12,13,10,9])).
% 60.28/60.47 cnf(1245,plain,
% 60.28/60.47 (P2(a3,f8(a3,x12451),f8(f8(a3,a3),x12451))),
% 60.28/60.47 inference(scs_inference,[],[90,347,12])).
% 60.28/60.47 cnf(1248,plain,
% 60.28/60.47 (P1(f8(a3,x12481),f5(a3),a3)),
% 60.28/60.47 inference(scs_inference,[],[397,90,184,857,1201,347,12,13,10])).
% 60.28/60.47 cnf(1255,plain,
% 60.28/60.47 (P1(f8(x12551,a3),f5(a3),a3)),
% 60.28/60.47 inference(scs_inference,[],[90,874,10])).
% 60.28/60.47 cnf(1262,plain,
% 60.28/60.47 (P1(a3,f5(a3),f8(a3,x12621))),
% 60.28/60.47 inference(scs_inference,[],[397,1093,10])).
% 60.28/60.47 cnf(1263,plain,
% 60.28/60.47 (P1(f5(a3),a6,f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[397,879,1093,10,9])).
% 60.28/60.47 cnf(1266,plain,
% 60.28/60.47 (P1(f5(a3),f4(a1,a2),a6)),
% 60.28/60.47 inference(scs_inference,[],[397,35,351,18,879,1078,1093,10,9,11,28])).
% 60.28/60.47 cnf(1271,plain,
% 60.28/60.47 (E(x12711,f4(x12711,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1272,plain,
% 60.28/60.47 (P1(f4(f8(a3,x12721),a3),f5(a3),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[35,1271,529,1133,10,9])).
% 60.28/60.47 cnf(1280,plain,
% 60.28/60.47 (E(x12801,f4(x12801,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1283,plain,
% 60.28/60.47 (P1(f5(a3),f4(f5(a3),f5(a3)),f4(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[184,35,1280,1078,1195,844,10,9,11])).
% 60.28/60.47 cnf(1288,plain,
% 60.28/60.47 (P1(f5(a3),f4(a6,a3),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[35,1263,10])).
% 60.28/60.47 cnf(1289,plain,
% 60.28/60.47 (E(x12891,f4(x12891,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1293,plain,
% 60.28/60.47 (P1(f5(a3),f4(f4(a1,a2),a3),a6)),
% 60.28/60.47 inference(scs_inference,[],[184,35,1289,351,18,1084,1263,10,9,11,28])).
% 60.28/60.47 cnf(1299,plain,
% 60.28/60.47 (P1(f5(a3),f4(a1,a2),f4(a6,a3))),
% 60.28/60.47 inference(scs_inference,[],[293,184,35,913,1266,1228,10,9,11])).
% 60.28/60.47 cnf(1303,plain,
% 60.28/60.47 (P1(f5(a3),f4(f4(a1,a2),a3),f4(a6,a3))),
% 60.28/60.47 inference(scs_inference,[],[35,1299,10])).
% 60.28/60.47 cnf(1304,plain,
% 60.28/60.47 (E(x13041,f4(x13041,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1305,plain,
% 60.28/60.47 (P1(f5(a3),f4(a6,a3),f4(f4(a1,a2),a3))),
% 60.28/60.47 inference(scs_inference,[],[35,1304,1288,1299,10,11])).
% 60.28/60.47 cnf(1310,plain,
% 60.28/60.47 (P1(a1,f4(a2,a3),f4(f4(a3,a3),a6))),
% 60.28/60.47 inference(scs_inference,[],[35,1062,10])).
% 60.28/60.47 cnf(1312,plain,
% 60.28/60.47 (P1(f4(a3,a3),f4(f4(a1,a2),a3),a6)),
% 60.28/60.47 inference(scs_inference,[],[184,35,1293,1062,10,9])).
% 60.28/60.47 cnf(1317,plain,
% 60.28/60.47 (P1(f4(a3,a3),f4(a1,a2),a6)),
% 60.28/60.47 inference(scs_inference,[],[90,1312,10])).
% 60.28/60.47 cnf(1323,plain,
% 60.28/60.47 (P1(f4(f8(a3,x13231),a3),f4(a3,a3),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[184,1272,10])).
% 60.28/60.47 cnf(1324,plain,
% 60.28/60.47 (P1(f4(a3,a3),f4(f4(a1,a2),a3),f4(a6,a3))),
% 60.28/60.47 inference(scs_inference,[],[184,1303,1272,10,9])).
% 60.28/60.47 cnf(1329,plain,
% 60.28/60.47 (P1(f8(x13291,a3),f4(a3,a3),a3)),
% 60.28/60.47 inference(scs_inference,[],[184,1255,10])).
% 60.28/60.47 cnf(1330,plain,
% 60.28/60.47 (P1(f8(a3,x13301),a3,f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[397,184,858,1255,10,11])).
% 60.28/60.47 cnf(1334,plain,
% 60.28/60.47 (P2(a3,f8(x13341,a3),f8(f8(a3,x13341),f4(a3,a3)))),
% 60.28/60.47 inference(scs_inference,[],[90,303,12])).
% 60.28/60.47 cnf(1335,plain,
% 60.28/60.47 (E(f4(x13351,a3),x13351)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1337,plain,
% 60.28/60.47 (E(f4(x13371,a3),x13371)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1338,plain,
% 60.28/60.47 (P1(x13381,a3,f4(x13381,f5(a3)))),
% 60.28/60.47 inference(scs_inference,[],[90,1335,1337,552,303,1224,12,13,10])).
% 60.28/60.47 cnf(1348,plain,
% 60.28/60.47 (P1(f4(a3,a3),f4(a6,a3),f4(f4(a1,a2),a3))),
% 60.28/60.47 inference(scs_inference,[],[184,1305,1262,10,9])).
% 60.28/60.47 cnf(1349,plain,
% 60.28/60.47 (P1(f8(x13491,a3),f4(a3,a3),f5(f4(a3,a3)))),
% 60.28/60.47 inference(scs_inference,[],[184,145,1305,1329,1262,10,9,11])).
% 60.28/60.47 cnf(1353,plain,
% 60.28/60.47 (E(f4(x13531,a3),x13531)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1354,plain,
% 60.28/60.47 (P1(f4(a1,a3),f4(a2,a3),f4(f4(a3,a3),a6))),
% 60.28/60.47 inference(scs_inference,[],[90,35,1348,1310,10,9])).
% 60.28/60.47 cnf(1356,plain,
% 60.28/60.47 (P1(f4(a3,a3),f4(a6,a3),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[90,1353,35,1348,1310,10,9,11])).
% 60.28/60.47 cnf(1360,plain,
% 60.28/60.47 (P1(f4(a3,a3),a6,f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[90,1356,10])).
% 60.28/60.47 cnf(1362,plain,
% 60.28/60.47 (P1(f5(a3),a3,f8(a3,x13621))),
% 60.28/60.47 inference(scs_inference,[],[397,90,1356,1149,10,9])).
% 60.28/60.47 cnf(1363,plain,
% 60.28/60.47 (P1(f8(x13631,a3),f4(a3,a3),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[397,90,1356,1349,1149,10,9,11])).
% 60.28/60.47 cnf(1364,plain,
% 60.28/60.47 (P1(f5(a3),f8(a3,x13641),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[397,90,351,418,1356,1349,1149,10,9,11,28])).
% 60.28/60.47 cnf(1369,plain,
% 60.28/60.47 (P1(f4(f8(x13691,a3),a3),f4(a3,a3),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[90,35,1354,1363,10,9])).
% 60.28/60.47 cnf(1371,plain,
% 60.28/60.47 (P1(f8(x13711,a3),f4(a3,a3),f4(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[90,184,35,1354,1363,10,9,11])).
% 60.28/60.47 cnf(1372,plain,
% 60.28/60.47 (P1(f5(a3),f5(a3),f8(a3,x13721))),
% 60.28/60.47 inference(scs_inference,[],[90,184,35,351,18,1354,1363,1364,10,9,11,28])).
% 60.28/60.47 cnf(1387,plain,
% 60.28/60.47 (P1(f5(a3),f8(a3,x13871),a3)),
% 60.28/60.47 inference(scs_inference,[],[397,293,1371,1207,10,9])).
% 60.28/60.47 cnf(1388,plain,
% 60.28/60.47 (P1(f4(f8(x13881,a3),a3),f4(a3,a3),f4(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[397,293,184,1371,1369,1207,10,9,11])).
% 60.28/60.47 cnf(1391,plain,
% 60.28/60.47 (P1(f5(a3),f4(a3,a3),f8(a3,x13911))),
% 60.28/60.47 inference(scs_inference,[],[184,1372,10])).
% 60.28/60.47 cnf(1392,plain,
% 60.28/60.47 (P1(f4(a3,a3),f5(a3),f8(a3,x13921))),
% 60.28/60.47 inference(scs_inference,[],[184,1372,10,9])).
% 60.28/60.47 cnf(1393,plain,
% 60.28/60.47 (P1(a3,f8(a3,x13931),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[397,184,1372,907,10,9,11])).
% 60.28/60.47 cnf(1398,plain,
% 60.28/60.47 (P1(f4(a3,a3),f4(a3,a3),f8(a3,x13981))),
% 60.28/60.47 inference(scs_inference,[],[184,427,1360,1391,10,9])).
% 60.28/60.47 cnf(1399,plain,
% 60.28/60.47 (P1(f8(x13991,a3),a3,f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[397,184,427,1360,1391,919,10,9,11])).
% 60.28/60.47 cnf(1436,plain,
% 60.28/60.47 (P1(f4(a3,a3),a3,f8(a3,x14361))),
% 60.28/60.47 inference(scs_inference,[],[90,1398,10])).
% 60.28/60.47 cnf(1460,plain,
% 60.28/60.47 (E(f4(x14601,a3),x14601)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1462,plain,
% 60.28/60.47 (E(f4(x14621,a3),x14621)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(1465,plain,
% 60.28/60.47 (P1(f4(a3,a3),a3,f4(f5(a3),f4(a3,a3)))),
% 60.28/60.47 inference(scs_inference,[],[90,1460,1462,1008,38,556,1324,1283,1323,10,11,9,27])).
% 60.28/60.47 cnf(1486,plain,
% 60.28/60.47 (E(x14861,f4(x14861,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1490,plain,
% 60.28/60.47 (P1(f4(a3,a3),f8(a3,x14901),f4(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[184,35,1486,55,1248,1393,10,11,9,27])).
% 60.28/60.47 cnf(1504,plain,
% 60.28/60.47 (P1(f5(a3),f8(a3,x15041),f4(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[90,184,1388,1364,10,11])).
% 60.28/60.47 cnf(1519,plain,
% 60.28/60.47 (P1(a3,f4(a1,a2),a6)),
% 60.28/60.47 inference(scs_inference,[],[90,145,35,1317,1255,1364,10,11,9])).
% 60.28/60.47 cnf(1523,plain,
% 60.28/60.47 (P1(f8(x15231,a3),f5(f4(a3,a3)),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[145,1399,10])).
% 60.28/60.47 cnf(1526,plain,
% 60.28/60.47 (P1(a3,a6,f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[90,145,35,1360,1262,1399,10,11,9])).
% 60.28/60.47 cnf(1531,plain,
% 60.28/60.47 (E(x15311,f4(x15311,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1534,plain,
% 60.28/60.47 (P1(f4(a3,a3),f8(a3,x15341),a3)),
% 60.28/60.47 inference(scs_inference,[],[184,35,1531,1362,1387,1490,10,11,9])).
% 60.28/60.47 cnf(1558,plain,
% 60.28/60.47 (P1(f8(x15581,a3),f5(a3),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[397,1523,10])).
% 60.28/60.47 cnf(1561,plain,
% 60.28/60.47 (P1(f4(a3,a3),f8(a3,x15611),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[397,184,35,1364,1526,1523,10,11,9])).
% 60.28/60.47 cnf(1624,plain,
% 60.28/60.47 (E(x16241,f4(f4(x16241,a3),a3))),
% 60.28/60.47 inference(rename_variables,[],[427])).
% 60.28/60.47 cnf(1625,plain,
% 60.28/60.47 (P1(x16251,f5(x16251),f4(f4(a3,a3),a3))),
% 60.28/60.47 inference(scs_inference,[],[427,1624,19,157,10,11])).
% 60.28/60.47 cnf(1643,plain,
% 60.28/60.47 (E(x16431,f4(a3,f4(x16431,a3)))),
% 60.28/60.47 inference(rename_variables,[],[839])).
% 60.28/60.47 cnf(1645,plain,
% 60.28/60.47 (E(x16451,f4(a3,f4(x16451,a3)))),
% 60.28/60.47 inference(rename_variables,[],[839])).
% 60.28/60.47 cnf(1646,plain,
% 60.28/60.47 (P1(f4(a3,f4(a3,a3)),a3,f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[839,1643,1645,351,418,10,11,9])).
% 60.28/60.47 cnf(1648,plain,
% 60.28/60.47 (P1(a3,a3,f5(f5(a3)))),
% 60.28/60.47 inference(scs_inference,[],[839,1643,1645,351,418,942,312,10,11,9,28])).
% 60.28/60.47 cnf(1661,plain,
% 60.28/60.47 (P2(f4(f4(a3,a3),f5(a3)),f4(a3,a3),f8(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[578,297,12])).
% 60.28/60.47 cnf(1662,plain,
% 60.28/60.47 (E(x16621,f4(f4(a3,a3),x16621))),
% 60.28/60.47 inference(rename_variables,[],[578])).
% 60.28/60.47 cnf(1663,plain,
% 60.28/60.47 (P2(f4(a3,a3),f4(f4(a3,a3),f5(a3)),f8(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[578,1662,370,297,12,13])).
% 60.28/60.47 cnf(1682,plain,
% 60.28/60.47 (E(x16821,f4(x16821,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1684,plain,
% 60.28/60.47 (E(x16841,f4(x16841,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1686,plain,
% 60.28/60.47 (E(x16861,f4(x16861,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1688,plain,
% 60.28/60.47 (E(x16881,f4(x16881,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1691,plain,
% 60.28/60.47 (P1(f4(f5(a3),a3),a6,f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[35,1682,1684,1686,1688,370,675,343,1372,296,21,336,262,12,13,10,11,9,28])).
% 60.28/60.47 cnf(1699,plain,
% 60.28/60.47 (E(x16991,f4(x16991,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1701,plain,
% 60.28/60.47 (E(x17011,f4(x17011,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1703,plain,
% 60.28/60.47 (E(x17031,f4(x17031,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(1706,plain,
% 60.28/60.47 (P1(a3,f4(a3,a3),f5(f5(a3)))),
% 60.28/60.47 inference(scs_inference,[],[90,35,1699,1701,1703,418,942,938,1372,558,529,1239,1663,12,13,10,11,9,28])).
% 60.28/60.47 cnf(1715,plain,
% 60.28/60.47 (P2(f4(f4(a3,a3),f5(a3)),a3,f8(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[90,1661,13])).
% 60.28/60.47 cnf(1802,plain,
% 60.28/60.47 (E(x18021,f4(f4(x18021,a3),a3))),
% 60.28/60.47 inference(rename_variables,[],[427])).
% 60.28/60.47 cnf(1803,plain,
% 60.28/60.47 (P1(f5(a3),a6,f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[90,427,1387,1691,11,9])).
% 60.28/60.47 cnf(1805,plain,
% 60.28/60.47 (P1(f5(a3),f4(a1,a7),a6)),
% 60.28/60.47 inference(scs_inference,[],[90,427,351,18,1387,1691,11,9,28])).
% 60.28/60.47 cnf(1808,plain,
% 60.28/60.47 (P1(f5(a3),f4(f4(a6,a3),a3),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[90,427,1802,351,18,1387,1691,11,9,28,10])).
% 60.28/60.47 cnf(1814,plain,
% 60.28/60.47 (P1(a3,a3,f4(f5(a3),f4(a3,a3)))),
% 60.28/60.47 inference(scs_inference,[],[90,427,1519,1465,11,9])).
% 60.28/60.47 cnf(1816,plain,
% 60.28/60.47 (P1(f5(a3),f4(a1,a7),f4(a6,a3))),
% 60.28/60.47 inference(scs_inference,[],[90,427,351,203,1519,1808,1465,11,9,28])).
% 60.28/60.47 cnf(1822,plain,
% 60.28/60.47 (P1(f5(a3),f4(a6,a3),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[427,351,18,1534,1816,11,28])).
% 60.28/60.47 cnf(1830,plain,
% 60.28/60.47 (E(a6,f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[15,21,25])).
% 60.28/60.47 cnf(1831,plain,
% 60.28/60.47 (P1(x18311,x18312,f4(x18311,x18312))),
% 60.28/60.47 inference(rename_variables,[],[21])).
% 60.28/60.47 cnf(1835,plain,
% 60.28/60.47 (P1(a6,f5(a2),a1)),
% 60.28/60.47 inference(scs_inference,[],[15,398,1008,1625,21,25,3,27])).
% 60.28/60.47 cnf(1843,plain,
% 60.28/60.47 (E(f4(a1,a2),a6)),
% 60.28/60.47 inference(scs_inference,[],[15,398,1008,46,1625,21,1831,25,3,27,28,2])).
% 60.28/60.47 cnf(1890,plain,
% 60.28/60.47 (E(x18901,f4(a3,f4(x18901,a3)))),
% 60.28/60.47 inference(rename_variables,[],[839])).
% 60.28/60.47 cnf(1893,plain,
% 60.28/60.47 (E(x18931,f4(a3,f4(x18931,a3)))),
% 60.28/60.47 inference(rename_variables,[],[839])).
% 60.28/60.47 cnf(1896,plain,
% 60.28/60.47 (P1(a6,f4(f4(a3,a3),a3),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[15,285,839,1890,1893,1008,1715,21,219,12,10,13,9,11,27])).
% 60.28/60.47 cnf(2009,plain,
% 60.28/60.47 (P2(a3,f8(a3,a3),f8(f4(a3,a3),f8(a3,a3)))),
% 60.28/60.47 inference(scs_inference,[],[15,285,17,1338,260,1165,1128,1646,196,12,10,13,9,11,28,446])).
% 60.28/60.47 cnf(2054,plain,
% 60.28/60.47 (P1(f5(a3),f4(x20541,a3),f4(f4(a3,a3),x20541))),
% 60.28/60.47 inference(scs_inference,[],[285,833,1648,2009,12,10,9])).
% 60.28/60.47 cnf(2075,plain,
% 60.28/60.47 (P1(a3,f5(a3),f4(f5(a3),f4(a3,a3)))),
% 60.28/60.47 inference(scs_inference,[],[285,1814,1245,12,10])).
% 60.28/60.47 cnf(2076,plain,
% 60.28/60.47 (P1(f5(a3),f4(a3,a3),f5(f5(a3)))),
% 60.28/60.47 inference(scs_inference,[],[285,1706,1814,1245,12,10,9])).
% 60.28/60.47 cnf(2095,plain,
% 60.28/60.47 (P1(a6,a3,f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[398,1896,10])).
% 60.28/60.47 cnf(2158,plain,
% 60.28/60.47 (E(x21581,f4(x21581,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(2160,plain,
% 60.28/60.47 (E(x21601,f4(x21601,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(2162,plain,
% 60.28/60.47 (E(x21621,f4(x21621,a3))),
% 60.28/60.47 inference(rename_variables,[],[35])).
% 60.28/60.47 cnf(2163,plain,
% 60.28/60.47 (P1(f4(f5(x21631),a3),x21631,a3)),
% 60.28/60.47 inference(scs_inference,[],[285,35,2158,2160,2162,937,20,1248,1330,1334,12,13,10,11,9])).
% 60.28/60.47 cnf(2200,plain,
% 60.28/60.47 (E(x22001,f4(f4(a3,a3),x22001))),
% 60.28/60.47 inference(rename_variables,[],[578])).
% 60.28/60.47 cnf(2202,plain,
% 60.28/60.47 (E(x22021,f4(f4(a3,a3),x22021))),
% 60.28/60.47 inference(rename_variables,[],[578])).
% 60.28/60.47 cnf(2204,plain,
% 60.28/60.47 (E(x22041,f4(f4(a3,a3),x22041))),
% 60.28/60.47 inference(rename_variables,[],[578])).
% 60.28/60.47 cnf(2206,plain,
% 60.28/60.47 (E(x22061,f4(f4(a3,a3),x22061))),
% 60.28/60.47 inference(rename_variables,[],[578])).
% 60.28/60.47 cnf(2207,plain,
% 60.28/60.47 (P1(f4(f4(a3,a3),f5(a3)),f4(x22071,a3),x22071)),
% 60.28/60.47 inference(scs_inference,[],[578,2200,2202,2204,2206,900,937,19,296,262,14,13,10,11,9])).
% 60.28/60.47 cnf(2222,plain,
% 60.28/60.47 (P1(a6,f5(a3),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[285,2095,10])).
% 60.28/60.47 cnf(2239,plain,
% 60.28/60.47 (P1(f5(a3),f4(f4(a3,a3),f4(a3,a3)),a3)),
% 60.28/60.47 inference(scs_inference,[],[398,285,427,1008,351,2054,2207,2163,2222,10,11,9,28])).
% 60.28/60.47 cnf(2328,plain,
% 60.28/60.47 (P1(f4(f5(a3),a3),f5(a3),f8(x23281,a3))),
% 60.28/60.47 inference(scs_inference,[],[285,90,675,46,1369,2076,2239,2075,10,11,9,28])).
% 60.28/60.47 cnf(2351,plain,
% 60.28/60.47 (P1(f5(a3),f5(a3),f8(x23511,a3))),
% 60.28/60.47 inference(scs_inference,[],[285,90,2328,436,10,9])).
% 60.28/60.47 cnf(2542,plain,
% 60.28/60.47 (P1(f4(a6,a3),f5(a3),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[1822,24])).
% 60.28/60.47 cnf(2544,plain,
% 60.28/60.47 (~E(a2,a7)),
% 60.28/60.47 inference(scs_inference,[],[23,1822,24,2])).
% 60.28/60.47 cnf(2548,plain,
% 60.28/60.47 (~E(f4(a7,a3),a2)),
% 60.28/60.47 inference(scs_inference,[],[23,1822,806,35,24,2,25,3])).
% 60.28/60.47 cnf(2550,plain,
% 60.28/60.47 (P1(f5(a3),f4(a1,a2),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[23,1822,1803,1830,806,35,24,2,25,3,10])).
% 60.28/60.47 cnf(2551,plain,
% 60.28/60.47 (~P1(f4(a7,a3),f5(a3),f4(a2,a3))),
% 60.28/60.47 inference(scs_inference,[],[23,1822,1803,1830,806,90,35,24,2,25,3,10,11])).
% 60.28/60.47 cnf(2553,plain,
% 60.28/60.47 (~P1(a7,f8(x25531,a3),a2)),
% 60.28/60.47 inference(scs_inference,[],[23,2351,1822,1803,1094,1830,806,90,35,24,2,25,3,10,11,27])).
% 60.28/60.47 cnf(2556,plain,
% 60.28/60.47 (P1(f5(a3),f8(x25561,a3),f5(a3))),
% 60.28/60.47 inference(scs_inference,[],[23,2351,1822,1558,1803,1094,1830,806,90,35,24,2,25,3,10,11,27,28])).
% 60.28/60.47 cnf(2557,plain,
% 60.28/60.47 (P1(f5(a3),f5(a3),f8(x25571,a3))),
% 60.28/60.47 inference(rename_variables,[],[2351])).
% 60.28/60.47 cnf(2559,plain,
% 60.28/60.47 (P2(f8(x25591,a3),f5(a3),f8(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[23,2351,2557,1822,1558,1803,1094,1830,806,937,49,90,35,24,2,25,3,10,11,27,28,33])).
% 60.28/60.47 cnf(2560,plain,
% 60.28/60.47 (P1(f8(x25601,a3),f8(x25601,a3),f8(x25601,a3))),
% 60.28/60.47 inference(rename_variables,[],[49])).
% 60.28/60.47 cnf(2562,plain,
% 60.28/60.47 (P2(f5(a3),f8(x25621,a3),f8(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[23,2351,2557,1822,1558,1803,1094,1830,806,937,49,2560,90,35,24,2,25,3,10,11,27,28,33,34])).
% 60.28/60.47 cnf(2574,plain,
% 60.28/60.47 (P1(f4(a1,a2),f5(a3),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2550,24])).
% 60.28/60.47 cnf(2576,plain,
% 60.28/60.47 (~E(f4(a2,a3),a7)),
% 60.28/60.47 inference(scs_inference,[],[93,2550,24,2])).
% 60.28/60.47 cnf(2577,plain,
% 60.28/60.47 (~P1(f4(a2,a3),f5(a3),a7)),
% 60.28/60.47 inference(scs_inference,[],[2544,93,2550,806,24,2,25])).
% 60.28/60.47 cnf(2581,plain,
% 60.28/60.47 (P1(f5(a3),f4(a1,a7),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[2544,93,2550,2551,1805,1830,249,806,24,2,25,10,11])).
% 60.28/60.47 cnf(2584,plain,
% 60.28/60.47 (~P1(a7,f5(a3),a2)),
% 60.28/60.47 inference(scs_inference,[],[2544,93,2550,2551,2556,2553,1805,1094,1830,249,806,90,24,2,25,10,11,9,27])).
% 60.28/60.47 cnf(2602,plain,
% 60.28/60.47 (P1(f4(a1,a7),f5(a3),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[2581,24])).
% 60.28/60.47 cnf(2605,plain,
% 60.28/60.47 (~P1(f5(a3),a7,a2)),
% 60.28/60.47 inference(scs_inference,[],[2548,2581,979,24,2,25])).
% 60.28/60.47 cnf(2608,plain,
% 60.28/60.47 (P1(f5(a6),f4(a1,a2),f4(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[2548,2581,1220,979,1830,24,2,25,10])).
% 60.28/60.47 cnf(2610,plain,
% 60.28/60.47 (~P1(f4(a2,a3),f5(a3),f4(a7,a3))),
% 60.28/60.47 inference(scs_inference,[],[2548,2581,2577,1220,979,1830,90,24,2,25,10,11])).
% 60.28/60.47 cnf(2612,plain,
% 60.28/60.47 (P1(a6,f5(a3),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2548,2574,2581,2577,1220,979,1843,1830,90,24,2,25,10,11,9])).
% 60.28/60.47 cnf(2613,plain,
% 60.28/60.47 (P1(f4(a1,a7),f8(x26131,a3),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2548,2542,2574,2581,2577,1220,979,2556,1843,1830,90,24,2,25,10,11,9,27])).
% 60.28/60.47 cnf(2631,plain,
% 60.28/60.47 (P1(f8(x26311,a3),f4(a1,a7),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2613,24])).
% 60.28/60.47 cnf(2633,plain,
% 60.28/60.47 (~P1(f5(a3),f4(a7,a3),a2)),
% 60.28/60.47 inference(scs_inference,[],[23,2613,900,24,25])).
% 60.28/60.47 cnf(2636,plain,
% 60.28/60.47 (~P1(f4(a2,a3),f4(a3,a3),f4(a7,a3))),
% 60.28/60.47 inference(scs_inference,[],[23,2613,2610,900,249,24,25,10])).
% 60.28/60.47 cnf(2637,plain,
% 60.28/60.47 (P1(f4(a1,a7),f5(a3),a6)),
% 60.28/60.47 inference(scs_inference,[],[23,2613,2602,2610,1843,900,249,24,25,10,11])).
% 60.28/60.47 cnf(2638,plain,
% 60.28/60.47 (~P1(f4(a3,a3),a7,a2)),
% 60.28/60.47 inference(scs_inference,[],[23,2613,2602,2610,2605,1843,900,249,24,25,10,11,9])).
% 60.28/60.47 cnf(2639,plain,
% 60.28/60.47 (P1(f4(a1,a2),f8(x26391,a3),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[23,2613,2602,2610,2605,2581,1843,900,249,24,25,10,11,9,27])).
% 60.28/60.47 cnf(2641,plain,
% 60.28/60.47 (P1(a6,f4(a3,a3),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[23,2613,2602,2610,2612,2605,2581,1504,1843,900,249,24,25,10,11,9,27,28])).
% 60.28/60.47 cnf(2651,plain,
% 60.28/60.47 (P1(f8(x26511,a3),f4(a1,a2),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[2639,24])).
% 60.28/60.47 cnf(2653,plain,
% 60.28/60.47 (~P1(f5(a3),a2,a7)),
% 60.28/60.47 inference(scs_inference,[],[2576,2639,979,24,25])).
% 60.28/60.47 cnf(2654,plain,
% 60.28/60.47 (P1(f5(a3),x26541,f4(x26541,a3))),
% 60.28/60.47 inference(rename_variables,[],[979])).
% 60.28/60.47 cnf(2656,plain,
% 60.28/60.47 (~P1(a7,f4(a3,a3),a2)),
% 60.28/60.47 inference(scs_inference,[],[2576,2639,2584,979,249,24,25,10])).
% 60.28/60.47 cnf(2657,plain,
% 60.28/60.47 (~P1(f5(a3),f4(a7,a3),f4(a2,a3))),
% 60.28/60.47 inference(scs_inference,[],[2633,2576,2639,2584,979,249,90,24,25,10,11])).
% 60.28/60.47 cnf(2659,plain,
% 60.28/60.47 (P1(a6,f8(x26591,a3),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[2633,2576,2639,2584,979,1843,249,90,24,25,10,11,9])).
% 60.28/60.47 cnf(2660,plain,
% 60.28/60.47 (~P1(a2,f5(a3),f4(a7,a3))),
% 60.28/60.47 inference(scs_inference,[],[2633,2576,2639,2584,979,2654,1843,806,249,90,24,25,10,11,9,28])).
% 60.28/60.47 cnf(2676,plain,
% 60.28/60.47 (P1(f4(a1,a2),f5(a6),f4(a3,a3))),
% 60.28/60.47 inference(scs_inference,[],[2608,24])).
% 60.28/60.47 cnf(2678,plain,
% 60.28/60.47 (~P1(f5(a3),f4(a2,a3),a7)),
% 60.28/60.47 inference(scs_inference,[],[2608,2544,900,24,25])).
% 60.28/60.47 cnf(2681,plain,
% 60.28/60.47 (~P1(a2,f4(a3,a3),f4(a7,a3))),
% 60.28/60.47 inference(scs_inference,[],[2608,2660,2544,900,249,24,25,10])).
% 60.28/60.47 cnf(2682,plain,
% 60.28/60.47 (P1(f8(x26821,a3),f4(a1,a2),a6)),
% 60.28/60.47 inference(scs_inference,[],[2608,2651,2660,2544,900,1843,249,24,25,10,11])).
% 60.28/60.47 cnf(2683,plain,
% 60.28/60.47 (~P1(f4(a3,a3),f4(a7,a3),f4(a2,a3))),
% 60.28/60.47 inference(scs_inference,[],[2608,2651,2657,2660,2544,900,1843,249,24,25,10,11,9])).
% 60.28/60.47 cnf(2684,plain,
% 60.28/60.47 (~P1(f4(a3,a3),f4(a2,a3),f4(a7,a3))),
% 60.28/60.47 inference(scs_inference,[],[2636,2608,2651,2657,2660,2544,961,680,900,1843,249,24,25,10,11,9,27])).
% 60.28/60.47 cnf(2688,plain,
% 60.28/60.47 (P1(f4(a3,a3),f4(a6,a3),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2636,2608,2631,2651,2657,2660,2544,1816,1392,961,680,900,1843,249,24,25,10,11,9,27,28])).
% 60.28/60.47 cnf(2697,plain,
% 60.28/60.47 (P1(f4(a6,a3),f4(a3,a3),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2688,24])).
% 60.28/60.47 cnf(2699,plain,
% 60.28/60.47 (~P1(a3,a7,a2)),
% 60.28/60.47 inference(scs_inference,[],[2688,2548,105,24,25])).
% 60.28/60.47 cnf(2702,plain,
% 60.28/60.47 (P1(f8(x27021,a3),a6,a6)),
% 60.28/60.47 inference(scs_inference,[],[2688,2682,2548,1843,105,24,25,10])).
% 60.28/60.47 cnf(2703,plain,
% 60.28/60.47 (P1(f4(a1,a2),f4(a3,a3),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2688,2641,2682,2548,1830,1843,105,24,25,10,9])).
% 60.28/60.47 cnf(2706,plain,
% 60.28/60.47 (P1(f4(a1,a2),f4(a1,a2),f4(a6,a6))),
% 60.28/60.47 inference(scs_inference,[],[2688,2656,2641,2659,2682,2548,1830,1843,105,21,90,24,25,10,9,11,27])).
% 60.28/60.47 cnf(2710,plain,
% 60.28/60.47 (P1(a6,f8(a3,x27101),a6)),
% 60.28/60.47 inference(scs_inference,[],[2688,2656,2641,2659,2682,2637,2548,1392,1830,1843,105,21,90,24,25,10,9,11,27,28])).
% 60.28/60.47 cnf(2729,plain,
% 60.28/60.47 (P1(f4(a3,a3),f4(a1,a2),f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2703,24])).
% 60.28/60.47 cnf(2731,plain,
% 60.28/60.47 (~P1(a2,f5(a3),a7)),
% 60.28/60.47 inference(scs_inference,[],[2703,2576,1094,24,25])).
% 60.28/60.47 cnf(2734,plain,
% 60.28/60.47 (P2(f4(a1,a2),f5(a3),f8(a6,a3))),
% 60.28/60.47 inference(scs_inference,[],[2703,2576,1094,1830,938,24,25,12])).
% 60.28/60.47 cnf(2735,plain,
% 60.28/60.47 (P2(x27351,f5(a3),f8(x27351,a3))),
% 60.28/60.47 inference(rename_variables,[],[938])).
% 60.28/60.47 cnf(2736,plain,
% 60.28/60.47 (P2(f5(a3),f4(a1,a2),f8(a3,a6))),
% 60.28/60.47 inference(scs_inference,[],[2703,2576,1094,1830,296,938,24,25,12,13])).
% 60.28/60.47 cnf(2737,plain,
% 60.28/60.47 (P2(f5(a3),x27371,f8(a3,x27371))),
% 60.28/60.47 inference(rename_variables,[],[296])).
% 60.28/60.47 cnf(2740,plain,
% 60.28/60.47 (P1(f8(x27401,a3),a6,f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[2699,2703,2702,2576,1094,1830,296,938,90,24,25,12,13,10,11])).
% 60.28/60.47 cnf(2748,plain,
% 60.28/60.47 (P1(f8(a3,a3),f8(a6,a3),f8(a6,a3))),
% 60.28/60.47 inference(scs_inference,[],[2699,2703,2676,2706,2678,2702,2559,2576,1094,979,806,1830,296,249,938,2735,90,24,25,12,13,10,11,9,27,28,32])).
% 60.28/60.47 cnf(2752,plain,
% 60.28/60.47 (P1(f8(a3,a6),f8(a3,a3),f8(a3,a6))),
% 60.28/60.47 inference(scs_inference,[],[2699,2703,2676,2706,2678,2702,2710,2559,2576,1094,979,2562,806,1830,296,2737,249,938,2735,90,24,25,12,13,10,11,9,27,28,32,31])).
% 60.28/60.47 cnf(2770,plain,
% 60.28/60.47 (P1(f8(a6,a3),f8(a3,a3),f8(a6,a3))),
% 60.28/60.47 inference(scs_inference,[],[2748,24])).
% 60.28/60.47 cnf(2775,plain,
% 60.28/60.47 (P1(f4(a1,a7),a3,f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[23,2748,2602,94,497,24,25,10])).
% 60.28/60.47 cnf(2778,plain,
% 60.28/60.47 (~P1(f4(a3,a3),a2,a7)),
% 60.28/60.47 inference(scs_inference,[],[23,2748,2638,2653,2602,94,497,249,90,24,25,10,11,9])).
% 60.28/60.47 cnf(2779,plain,
% 60.28/60.47 (~P1(f5(a3),f4(a2,a3),f4(a7,a3))),
% 60.28/60.47 inference(scs_inference,[],[23,2748,2638,2681,2653,2602,680,942,94,497,249,90,24,25,10,11,9,27])).
% 60.28/60.47 cnf(2787,plain,
% 60.28/60.47 (P2(f4(a6,a6),f5(a3),f8(a6,a3))),
% 60.28/60.47 inference(scs_inference,[],[23,2729,2748,2734,2638,2681,2653,2602,2608,2706,680,942,94,497,249,49,90,24,25,10,11,9,27,28,30,33])).
% 60.28/60.47 cnf(2800,plain,
% 60.28/60.47 (~P1(a2,f4(a3,a3),a7)),
% 60.28/60.47 inference(scs_inference,[],[2752,2731,249,24,10])).
% 60.28/60.47 cnf(2801,plain,
% 60.28/60.47 (~P1(f4(a7,a3),f4(a3,a3),a2)),
% 60.28/60.47 inference(scs_inference,[],[2752,2731,2656,249,90,24,10,9])).
% 60.28/60.47 cnf(2804,plain,
% 60.28/60.47 (P1(a1,a2,f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2752,2731,2775,1835,2656,1220,2641,1843,249,90,24,10,9,11,27])).
% 60.28/60.47 cnf(2807,plain,
% 60.28/60.47 (P1(f4(a6,a3),f8(a3,x28071),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[2697,2752,2731,2775,1835,2656,1220,2641,1436,1843,249,90,24,10,9,11,27,28])).
% 60.28/60.47 cnf(2817,plain,
% 60.28/60.47 (P1(f8(a3,x28171),f4(a6,a3),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[2807,24])).
% 60.28/60.47 cnf(2821,plain,
% 60.28/60.47 (P1(f4(a1,a2),a3,f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2807,2787,2574,2736,94,24,12,13,10])).
% 60.28/60.47 cnf(2824,plain,
% 60.28/60.47 (~P1(a3,f4(a2,a3),f4(a7,a3))),
% 60.28/60.47 inference(scs_inference,[],[2779,2778,2807,2787,2574,2736,94,285,90,24,12,13,10,11,9])).
% 60.28/60.47 cnf(2825,plain,
% 60.28/60.47 (~P1(f5(a1),f4(a1,a7),a7)),
% 60.28/60.47 inference(scs_inference,[],[2779,2778,2807,2787,2804,2574,2736,1220,94,285,90,24,12,13,10,11,9,27])).
% 60.28/60.47 cnf(2828,plain,
% 60.28/60.47 (~P1(f8(a3,x28281),a2,f4(a7,a3))),
% 60.28/60.47 inference(scs_inference,[],[2683,2779,2778,2807,2787,2804,2574,2736,1490,1220,961,94,285,90,24,12,13,10,11,9,27,28])).
% 60.28/60.47 cnf(2841,plain,
% 60.28/60.47 (E(f4(x28411,a3),x28411)),
% 60.28/60.47 inference(rename_variables,[],[90])).
% 60.28/60.47 cnf(2842,plain,
% 60.28/60.47 (P1(f8(a3,x28421),f4(a6,a3),a6)),
% 60.28/60.47 inference(scs_inference,[],[2817,2821,2828,1843,90,24,10,11])).
% 60.28/60.47 cnf(2848,plain,
% 60.28/60.47 (P1(f8(a3,x28481),a6,f4(a1,a7))),
% 60.28/60.47 inference(scs_inference,[],[2817,2801,2821,2828,2800,1391,1094,1843,38,90,2841,24,10,11,9,27,28])).
% 60.28/60.47 cnf(2862,plain,
% 60.28/60.47 (~P1(f5(a1),f4(a1,a7),f4(a7,a3))),
% 60.28/60.47 inference(scs_inference,[],[2842,2848,2825,1830,90,24,10,11])).
% 60.28/60.47 cnf(2864,plain,
% 60.28/60.47 (P1(f8(a6,a3),f4(a6,a3),f4(a1,a2))),
% 60.28/60.47 inference(scs_inference,[],[2770,2842,2848,2825,2740,1830,90,24,10,11,27])).
% 60.28/60.47 cnf(2868,plain,
% 60.28/60.47 (~P1(f8(a3,x28681),a7,f4(a2,a3))),
% 60.28/60.47 inference(scs_inference,[],[2684,2770,2842,2848,2825,2740,1561,979,1830,90,24,10,11,27,28])).
% 60.28/60.47 cnf(2906,plain,
% 60.28/60.47 ($false),
% 60.28/60.47 inference(scs_inference,[],[2864,2824,2862,2868,890,1220,961,1843,20,21,90,24,10,11,27,28]),
% 60.28/60.47 ['proof']).
% 60.28/60.47 % SZS output end Proof
% 60.28/60.47 % Total time :59.650000s
%------------------------------------------------------------------------------