%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG006-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n004.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:35 EDT 2024
% Result : Unsatisfiable 58.78s 58.86s
% Output : CNFRefutation 58.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : RNG006-1 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n004.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:23:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 58.78/58.85 %-------------------------------------------
% 58.78/58.85 % File :CSE---1.7
% 58.78/58.85 % Problem :theBenchmark
% 58.78/58.85 % Transform :cnf
% 58.78/58.85 % Format :tptp:raw
% 58.78/58.85 % Command :java -jar mcs_scs.jar %d %s
% 58.78/58.85
% 58.78/58.85 % Result :Theorem 58.260000s
% 58.78/58.85 % Output :CNFRefutation 58.260000s
% 58.78/58.85 %-------------------------------------------
% 58.78/58.86 %--------------------------------------------------------------------------
% 58.78/58.86 % File : RNG006-1 : TPTP v8.2.0. Released v1.0.0.
% 58.78/58.86 % Domain : Ring Theory
% 58.78/58.86 % Problem : X*(Y+ -Z) = (X*Y) + -(X*Z)
% 58.78/58.86 % Version : [Wos65] axioms : Augmented.
% 58.78/58.86 % English :
% 58.78/58.86
% 58.78/58.86 % Refs : [Wos65] Wos (1965), Unpublished Note
% 58.78/58.86 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 58.78/58.86 % Source : [SPRFN]
% 58.78/58.86 % Names : Problem 25 [Wos65]
% 58.78/58.86
% 58.78/58.86 % Status : Unsatisfiable
% 58.78/58.86 % Rating : 0.00 v8.2.0, 0.08 v8.1.0, 0.00 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.13 v5.3.0, 0.17 v5.2.0, 0.25 v5.1.0, 0.14 v5.0.0, 0.00 v4.0.0, 0.17 v3.5.0, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.2.1, 0.22 v2.2.0, 0.14 v2.1.0, 0.00 v2.0.0
% 58.78/58.86 % Syntax : Number of clauses : 25 ( 11 unt; 0 nHn; 19 RR)
% 58.78/58.86 % Number of literals : 61 ( 2 equ; 37 neg)
% 58.78/58.86 % Maximal clause size : 5 ( 2 avg)
% 58.78/58.86 % Maximal term depth : 2 ( 1 avg)
% 58.78/58.86 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 58.78/58.86 % Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% 58.78/58.86 % Number of variables : 80 ( 0 sgn)
% 58.78/58.86 % SPC : CNF_UNS_RFO_SEQ_HRN
% 58.78/58.86
% 58.78/58.86 % Comments : These are the same axioms as in [MOW76].
% 58.78/58.86 %--------------------------------------------------------------------------
% 58.78/58.86 %----Include ring theory axioms
% 58.78/58.86 include('Axioms/RNG001-0.ax').
% 58.78/58.86 %--------------------------------------------------------------------------
% 58.78/58.86 cnf(product_lemma1,axiom,
% 58.78/58.86 ( ~ product(A,B,C)
% 58.78/58.86 | product(A,additive_inverse(B),additive_inverse(C)) ) ).
% 58.78/58.86
% 58.78/58.86 cnf(product_lemma2,axiom,
% 58.78/58.86 ( ~ product(A,B,C)
% 58.78/58.86 | product(additive_inverse(A),B,additive_inverse(C)) ) ).
% 58.78/58.86
% 58.78/58.86 cnf(product_lemma3,axiom,
% 58.78/58.86 ( ~ product(A,B,C)
% 58.78/58.86 | product(additive_inverse(A),additive_inverse(B),C) ) ).
% 58.78/58.86
% 58.78/58.86 cnf(b_plus_inverse_c,hypothesis,
% 58.78/58.86 sum(b,additive_inverse(c),bS_Ic) ).
% 58.78/58.86
% 58.78/58.86 cnf(a_times_b,hypothesis,
% 58.78/58.86 product(a,b,aPb) ).
% 58.78/58.86
% 58.78/58.86 cnf(a_times_c,hypothesis,
% 58.78/58.86 product(a,c,aPc) ).
% 58.78/58.86
% 58.78/58.86 cnf(aPb_plus_IaPc,hypothesis,
% 58.78/58.86 sum(aPb,additive_inverse(aPc),aPb_S_IaPc) ).
% 58.78/58.86
% 58.78/58.86 cnf(prove_a_times_bS_Ic_is_aPb_S__IaPc,negated_conjecture,
% 58.78/58.86 ~ product(a,bS_Ic,aPb_S_IaPc) ).
% 58.78/58.86
% 58.78/58.86 %--------------------------------------------------------------------------
% 58.78/58.86 %-------------------------------------------
% 58.78/58.86 % Proof found
% 58.78/58.86 % SZS status Theorem for theBenchmark
% 58.78/58.86 % SZS output start Proof
% 58.87/58.87 %ClaNum:39(EqnAxiom:14)
% 58.87/58.87 %VarNum:164(SingletonVarNum:80)
% 58.87/58.87 %MaxLitNum:5
% 58.87/58.87 %MaxfuncDepth:1
% 58.87/58.87 %SharedTerms:15
% 58.87/58.87 %goalClause: 25
% 58.87/58.87 %singleGoalClaCount:1
% 58.87/58.87 [15]P1(a1,a2,a3)
% 58.87/58.87 [16]P1(a1,a9,a4)
% 58.87/58.87 [25]~P1(a1,a10,a5)
% 58.87/58.87 [19]P2(a2,f8(a9),a10)
% 58.87/58.87 [20]P2(a3,f8(a4),a5)
% 58.87/58.87 [17]P2(x171,a6,x171)
% 58.87/58.87 [18]P2(a6,x181,x181)
% 58.87/58.87 [21]P2(x211,f8(x211),a6)
% 58.87/58.87 [22]P2(f8(x221),x221,a6)
% 58.87/58.87 [23]P2(x231,x232,f7(x231,x232))
% 58.87/58.87 [24]P1(x241,x242,f11(x241,x242))
% 58.87/58.87 [26]~P2(x262,x261,x263)+P2(x261,x262,x263)
% 58.87/58.87 [27]~P1(x271,x272,x273)+P1(x271,f8(x272),f8(x273))
% 58.87/58.87 [28]~P1(x281,x282,x283)+P1(f8(x281),x282,f8(x283))
% 58.87/58.87 [29]~P1(x291,x292,x293)+P1(f8(x291),f8(x292),x293)
% 58.87/58.87 [30]~P2(x303,x304,x301)+E(x301,x302)+~P2(x303,x304,x302)
% 58.87/58.87 [31]~P1(x313,x314,x311)+E(x311,x312)+~P1(x313,x314,x312)
% 58.87/58.87 [32]~P2(x326,x324,x321)+P2(x321,x322,x323)+~P2(x324,x322,x325)+~P2(x326,x325,x323)
% 58.87/58.87 [33]~P2(x331,x336,x334)+P2(x331,x332,x333)+~P2(x334,x335,x333)+~P2(x336,x335,x332)
% 58.87/58.87 [34]~P1(x346,x344,x341)+P1(x341,x342,x343)+~P1(x344,x342,x345)+~P1(x346,x345,x343)
% 58.87/58.87 [35]~P1(x351,x356,x354)+P1(x351,x352,x353)+~P1(x354,x355,x353)+~P1(x356,x355,x352)
% 58.87/58.87 [36]~P1(x367,x365,x362)+~P1(x367,x364,x361)+P2(x361,x362,x363)+~P2(x364,x365,x366)+~P1(x367,x366,x363)
% 58.87/58.87 [37]~P1(x375,x377,x372)+~P1(x374,x377,x371)+P2(x371,x372,x373)+~P2(x374,x375,x376)+~P1(x376,x377,x373)
% 58.87/58.87 [38]~P1(x387,x382,x385)+~P1(x386,x382,x384)+P1(x381,x382,x383)+~P2(x384,x385,x383)+~P2(x386,x387,x381)
% 58.87/58.87 [39]~P1(x391,x397,x395)+~P1(x391,x396,x394)+P1(x391,x392,x393)+~P2(x394,x395,x393)+~P2(x396,x397,x392)
% 58.87/58.87 %EqnAxiom
% 58.87/58.87 [1]E(x11,x11)
% 58.87/58.87 [2]E(x22,x21)+~E(x21,x22)
% 58.87/58.87 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.87/58.87 [4]~E(x41,x42)+E(f8(x41),f8(x42))
% 58.87/58.87 [5]~E(x51,x52)+E(f11(x51,x53),f11(x52,x53))
% 58.87/58.87 [6]~E(x61,x62)+E(f11(x63,x61),f11(x63,x62))
% 58.87/58.87 [7]~E(x71,x72)+E(f7(x71,x73),f7(x72,x73))
% 58.87/58.87 [8]~E(x81,x82)+E(f7(x83,x81),f7(x83,x82))
% 58.87/58.87 [9]P1(x92,x93,x94)+~E(x91,x92)+~P1(x91,x93,x94)
% 58.87/58.87 [10]P1(x103,x102,x104)+~E(x101,x102)+~P1(x103,x101,x104)
% 58.87/58.87 [11]P1(x113,x114,x112)+~E(x111,x112)+~P1(x113,x114,x111)
% 58.87/58.87 [12]P2(x122,x123,x124)+~E(x121,x122)+~P2(x121,x123,x124)
% 58.87/58.87 [13]P2(x133,x132,x134)+~E(x131,x132)+~P2(x133,x131,x134)
% 58.87/58.87 [14]P2(x143,x144,x142)+~E(x141,x142)+~P2(x143,x144,x141)
% 58.87/58.87
% 58.87/58.87 %-------------------------------------------
% 58.87/58.88 cnf(40,plain,
% 58.87/58.88 (E(x401,f7(x401,a6))),
% 58.87/58.88 inference(scs_inference,[],[17,23,30])).
% 58.87/58.88 cnf(41,plain,
% 58.87/58.88 (P2(x411,x412,f7(x411,x412))),
% 58.87/58.88 inference(rename_variables,[],[23])).
% 58.87/58.88 cnf(43,plain,
% 58.87/58.88 (P1(x431,f7(x432,a6),f11(x431,x432))),
% 58.87/58.88 inference(scs_inference,[],[17,23,24,30,10])).
% 58.87/58.88 cnf(44,plain,
% 58.87/58.88 (P1(x441,x442,f11(x441,x442))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(45,plain,
% 58.87/58.88 (~E(f11(a1,a10),a5)),
% 58.87/58.88 inference(scs_inference,[],[25,17,23,24,44,30,10,11])).
% 58.87/58.88 cnf(46,plain,
% 58.87/58.88 (P1(x461,x462,f11(x461,x462))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(47,plain,
% 58.87/58.88 (P2(f7(x471,a6),a6,x471)),
% 58.87/58.88 inference(scs_inference,[],[25,17,23,24,44,30,10,11,12])).
% 58.87/58.88 cnf(49,plain,
% 58.87/58.88 (P2(x491,a6,x491)),
% 58.87/58.88 inference(rename_variables,[],[17])).
% 58.87/58.88 cnf(50,plain,
% 58.87/58.88 (P2(x501,f8(x501),f7(a6,a6))),
% 58.87/58.88 inference(scs_inference,[],[25,17,23,24,44,21,30,10,11,12,13,14])).
% 58.87/58.88 cnf(51,plain,
% 58.87/58.88 (P2(x511,f7(a6,a6),x511)),
% 58.87/58.88 inference(scs_inference,[],[25,17,49,23,41,24,44,21,30,10,11,12,13,14,33])).
% 58.87/58.88 cnf(52,plain,
% 58.87/58.88 (P2(x521,x522,f7(x521,x522))),
% 58.87/58.88 inference(rename_variables,[],[23])).
% 58.87/58.88 cnf(54,plain,
% 58.87/58.88 (P1(a6,x541,f7(f11(a6,x541),f11(a6,x541)))),
% 58.87/58.88 inference(scs_inference,[],[25,17,49,23,41,52,24,44,46,21,30,10,11,12,13,14,33,38])).
% 58.87/58.88 cnf(55,plain,
% 58.87/58.88 (P2(x551,x552,f7(x551,x552))),
% 58.87/58.88 inference(rename_variables,[],[23])).
% 58.87/58.88 cnf(56,plain,
% 58.87/58.88 (P2(x561,a6,x561)),
% 58.87/58.88 inference(rename_variables,[],[17])).
% 58.87/58.88 cnf(58,plain,
% 58.87/58.88 (P1(x581,x582,f11(x581,x582))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(60,plain,
% 58.87/58.88 (P1(x601,a6,f7(f11(x601,a6),f11(x601,a6)))),
% 58.87/58.88 inference(scs_inference,[],[25,17,49,56,23,41,52,55,24,44,46,58,21,30,10,11,12,13,14,33,38,39])).
% 58.87/58.88 cnf(62,plain,
% 58.87/58.88 (P2(x621,a6,x621)),
% 58.87/58.88 inference(rename_variables,[],[17])).
% 58.87/58.88 cnf(64,plain,
% 58.87/58.88 (P1(x641,x642,f11(x641,x642))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(66,plain,
% 58.87/58.88 (P2(f11(x661,a6),f11(x661,a6),f11(x661,a6))),
% 58.87/58.88 inference(scs_inference,[],[25,17,49,56,62,23,41,52,55,24,44,46,58,64,21,30,10,11,12,13,14,33,38,39,36])).
% 58.87/58.88 cnf(69,plain,
% 58.87/58.88 (P1(x691,x692,f11(x691,x692))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(70,plain,
% 58.87/58.88 (P2(x701,a6,x701)),
% 58.87/58.88 inference(rename_variables,[],[17])).
% 58.87/58.88 cnf(72,plain,
% 58.87/58.88 (P2(f11(a6,x721),f11(a6,x721),f11(a6,x721))),
% 58.87/58.88 inference(scs_inference,[],[25,17,49,56,62,70,23,41,52,55,24,44,46,58,64,69,21,30,10,11,12,13,14,33,38,39,36,37])).
% 58.87/58.88 cnf(74,plain,
% 58.87/58.88 (P1(x741,x742,f11(x741,x742))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(75,plain,
% 58.87/58.88 (P1(x751,x752,f11(x751,x752))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(79,plain,
% 58.87/58.88 (P1(f7(a6,a6),x791,f11(a6,x791))),
% 58.87/58.88 inference(scs_inference,[],[25,17,49,56,62,70,23,41,52,55,24,44,46,58,64,69,75,21,30,10,11,12,13,14,33,38,39,36,37,2,9])).
% 58.87/58.88 cnf(80,plain,
% 58.87/58.88 (P1(x801,x802,f11(x801,x802))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(81,plain,
% 58.87/58.88 (E(f11(x811,f7(a6,a6)),f11(x811,a6))),
% 58.87/58.88 inference(scs_inference,[],[25,17,49,56,62,70,23,41,52,55,24,44,46,58,64,69,75,80,21,30,10,11,12,13,14,33,38,39,36,37,2,9,31])).
% 58.87/58.88 cnf(82,plain,
% 58.87/58.88 (P1(x821,x822,f11(x821,x822))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(85,plain,
% 58.87/58.88 (P1(f11(x851,x851),x851,f11(x851,f11(x851,x851)))),
% 58.87/58.88 inference(scs_inference,[],[25,17,49,56,62,70,23,41,52,55,24,44,46,58,64,69,75,80,82,74,21,30,10,11,12,13,14,33,38,39,36,37,2,9,31,3,34])).
% 58.87/58.88 cnf(87,plain,
% 58.87/58.88 (P1(x871,x872,f11(x871,x872))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(88,plain,
% 58.87/58.88 (P1(x881,x882,f11(x881,x882))),
% 58.87/58.88 inference(rename_variables,[],[24])).
% 58.87/58.88 cnf(90,plain,
% 58.87/58.88 (P1(x901,f11(x901,x901),f11(f11(x901,x901),x901))),
% 58.87/58.88 inference(scs_inference,[],[25,17,49,56,62,70,23,41,52,55,24,44,46,58,64,69,75,80,82,88,87,74,21,30,10,11,12,13,14,33,38,39,36,37,2,9,31,3,34,35])).
% 58.87/58.88 cnf(96,plain,
% 58.87/58.88 (E(f7(x961,a6),x961)),
% 58.87/58.88 inference(scs_inference,[],[40,2])).
% 58.87/58.88 cnf(97,plain,
% 58.87/58.88 (P2(a6,x971,f7(x971,a6))),
% 58.87/58.88 inference(scs_inference,[],[18,40,2,14])).
% 58.87/58.88 cnf(98,plain,
% 58.87/58.88 (P2(a6,x981,x981)),
% 58.87/58.88 inference(rename_variables,[],[18])).
% 58.87/58.88 cnf(99,plain,
% 58.87/58.88 (~E(f11(a1,a10),f7(a5,a6))),
% 58.87/58.88 inference(scs_inference,[],[18,40,45,2,14,3])).
% 58.87/58.88 cnf(100,plain,
% 58.87/58.88 (P1(f7(a6,a6),f7(a6,a6),f11(a6,a6))),
% 58.87/58.88 inference(scs_inference,[],[79,18,40,81,45,2,14,3,11])).
% 58.87/58.88 cnf(103,plain,
% 58.87/58.88 (E(f8(a6),a6)),
% 58.87/58.88 inference(scs_inference,[],[79,18,98,21,40,81,45,2,14,3,11,30])).
% 58.87/58.88 cnf(104,plain,
% 58.87/58.88 (P2(x1041,f8(x1041),a6)),
% 58.87/58.88 inference(rename_variables,[],[21])).
% 58.87/58.88 cnf(105,plain,
% 58.87/58.88 (P2(a6,x1051,x1051)),
% 58.87/58.88 inference(rename_variables,[],[18])).
% 58.87/58.88 cnf(109,plain,
% 58.87/58.88 (E(x1091,f7(x1091,a6))),
% 58.87/58.88 inference(rename_variables,[],[40])).
% 58.87/58.88 cnf(110,plain,
% 58.87/58.88 (P1(f7(x1101,a6),f11(x1101,x1101),f11(f11(x1101,x1101),x1101))),
% 58.87/58.88 inference(scs_inference,[],[85,90,79,18,98,21,40,109,81,45,2,14,3,11,30,10,9])).
% 58.87/58.88 cnf(112,plain,
% 58.87/58.88 (P2(a6,f7(x1121,a6),x1121)),
% 58.87/58.88 inference(scs_inference,[],[85,90,79,18,98,105,21,40,109,81,45,2,14,3,11,30,10,9,13])).
% 58.87/58.88 cnf(113,plain,
% 58.87/58.88 (P2(a6,x1131,x1131)),
% 58.87/58.88 inference(rename_variables,[],[18])).
% 58.87/58.88 cnf(114,plain,
% 58.87/58.88 (P2(f7(a6,a6),x1141,x1141)),
% 58.87/58.88 inference(scs_inference,[],[85,90,79,18,98,105,113,21,40,109,81,45,2,14,3,11,30,10,9,13,12])).
% 58.87/58.88 cnf(116,plain,
% 58.87/58.88 (P2(f8(a6),f7(a6,a6),a6)),
% 58.87/58.88 inference(scs_inference,[],[85,90,79,18,98,105,113,21,104,51,40,109,81,45,2,14,3,11,30,10,9,13,12,32])).
% 58.87/58.88 cnf(142,plain,
% 58.87/58.88 (E(a6,f8(a6))),
% 58.87/58.88 inference(scs_inference,[],[103,2])).
% 58.87/58.88 cnf(145,plain,
% 58.87/58.88 (E(a6,f8(f7(a6,a6)))),
% 58.87/58.88 inference(scs_inference,[],[21,114,96,99,103,2,3,30])).
% 58.87/58.88 cnf(146,plain,
% 58.87/58.88 (P2(f7(a6,a6),x1461,x1461)),
% 58.87/58.88 inference(rename_variables,[],[114])).
% 58.87/58.88 cnf(149,plain,
% 58.87/58.88 (P1(x1491,f7(a6,a6),f7(f11(x1491,a6),f11(x1491,a6)))),
% 58.87/58.88 inference(scs_inference,[],[60,21,114,96,99,103,40,2,3,30,10])).
% 58.87/58.88 cnf(150,plain,
% 58.87/58.88 (E(x1501,f7(x1501,a6))),
% 58.87/58.88 inference(rename_variables,[],[40])).
% 58.87/58.88 cnf(151,plain,
% 58.87/58.88 (P2(a2,f8(a9),f7(a10,a6))),
% 58.87/58.88 inference(scs_inference,[],[60,19,21,114,96,99,103,40,150,2,3,30,10,14])).
% 58.87/58.88 cnf(152,plain,
% 58.87/58.88 (E(x1521,f7(x1521,a6))),
% 58.87/58.88 inference(rename_variables,[],[40])).
% 58.87/58.88 cnf(153,plain,
% 58.87/58.88 (P2(a2,f7(f8(a9),a6),a10)),
% 58.87/58.88 inference(scs_inference,[],[60,19,21,114,96,99,103,40,150,152,2,3,30,10,14,13])).
% 58.87/58.88 cnf(154,plain,
% 58.87/58.88 (E(x1541,f7(x1541,a6))),
% 58.87/58.88 inference(rename_variables,[],[40])).
% 58.87/58.88 cnf(155,plain,
% 58.87/58.88 (P1(x1551,f7(f7(a6,a6),a6),f11(x1551,a6))),
% 58.87/58.88 inference(scs_inference,[],[60,19,21,114,43,96,99,103,81,40,150,152,2,3,30,10,14,13,11])).
% 58.87/58.88 cnf(157,plain,
% 58.87/58.88 (P1(f7(a6,a6),x1571,f7(f11(a6,x1571),f11(a6,x1571)))),
% 58.87/58.88 inference(scs_inference,[],[54,60,19,21,114,43,96,99,103,81,40,150,152,154,2,3,30,10,14,13,11,9])).
% 58.87/58.88 cnf(158,plain,
% 58.87/58.88 (E(x1581,f7(x1581,a6))),
% 58.87/58.88 inference(rename_variables,[],[40])).
% 58.87/58.88 cnf(159,plain,
% 58.87/58.88 (P2(f7(a2,a6),f8(a9),a10)),
% 58.87/58.88 inference(scs_inference,[],[54,60,19,21,114,43,96,99,103,81,40,150,152,154,158,2,3,30,10,14,13,11,9,12])).
% 58.87/58.88 cnf(161,plain,
% 58.87/58.88 (P2(f7(a6,a6),f7(x1611,a6),x1611)),
% 58.87/58.88 inference(scs_inference,[],[54,60,19,18,21,114,146,43,96,112,99,103,81,40,150,152,154,158,2,3,30,10,14,13,11,9,12,32])).
% 58.87/58.88 cnf(165,plain,
% 58.87/58.88 (P2(a2,a6,f7(a10,a9))),
% 58.87/58.88 inference(scs_inference,[],[54,60,19,18,22,21,114,146,43,96,112,99,103,81,23,40,150,152,154,158,2,3,30,10,14,13,11,9,12,32,33])).
% 58.87/58.88 cnf(177,plain,
% 58.87/58.88 (E(f8(f7(a6,a6)),a6)),
% 58.87/58.88 inference(scs_inference,[],[145,2])).
% 58.87/58.88 cnf(178,plain,
% 58.87/58.88 (E(f7(f11(a6,x1781),f11(a6,x1781)),f11(a6,x1781))),
% 58.87/58.88 inference(scs_inference,[],[157,79,145,2,31])).
% 58.87/58.88 cnf(179,plain,
% 58.87/58.88 (P1(f7(a6,a6),x1791,f11(a6,x1791))),
% 58.87/58.88 inference(rename_variables,[],[79])).
% 58.87/58.88 cnf(181,plain,
% 58.87/58.88 (E(f8(a6),f7(a6,a6))),
% 58.87/58.88 inference(scs_inference,[],[157,79,18,50,145,2,31,30])).
% 58.87/58.88 cnf(185,plain,
% 58.87/58.88 (E(f7(a6,a6),f8(f7(a6,a6)))),
% 58.87/58.88 inference(scs_inference,[],[157,79,18,50,145,96,2,31,30,3])).
% 58.87/58.88 cnf(188,plain,
% 58.87/58.88 (E(x1881,f7(x1881,a6))),
% 58.87/58.88 inference(rename_variables,[],[40])).
% 58.87/58.88 cnf(189,plain,
% 58.87/58.88 (P2(a3,f8(a4),f7(a5,a6))),
% 58.87/58.88 inference(scs_inference,[],[157,79,20,18,50,145,96,40,188,2,31,30,3,13,14])).
% 58.87/58.88 cnf(190,plain,
% 58.87/58.88 (E(x1901,f7(x1901,a6))),
% 58.87/58.88 inference(rename_variables,[],[40])).
% 58.87/58.88 cnf(191,plain,
% 58.87/58.89 (P1(f7(a6,a6),f8(f7(a6,a6)),f11(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[157,79,179,20,18,50,145,96,40,188,2,31,30,3,13,14,10])).
% 58.87/58.89 cnf(193,plain,
% 58.87/58.89 (P1(f7(a1,a6),a9,a4)),
% 58.87/58.89 inference(scs_inference,[],[157,79,179,20,18,50,145,16,96,40,188,190,2,31,30,3,13,14,10,9])).
% 58.87/58.89 cnf(194,plain,
% 58.87/58.89 (E(x1941,f7(x1941,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(196,plain,
% 58.87/58.89 (E(x1961,f7(x1961,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(197,plain,
% 58.87/58.89 (P2(f7(a3,a6),f8(a4),a5)),
% 58.87/58.89 inference(scs_inference,[],[157,79,179,20,18,100,50,145,16,96,40,188,190,194,196,2,31,30,3,13,14,10,9,11,12])).
% 58.87/58.89 cnf(199,plain,
% 58.87/58.89 (P2(a6,f11(a6,x1991),a6)),
% 58.87/58.89 inference(scs_inference,[],[157,79,179,72,20,18,22,100,50,145,16,96,40,188,190,194,196,2,31,30,3,13,14,10,9,11,12,32])).
% 58.87/58.89 cnf(201,plain,
% 58.87/58.89 (P2(f8(x2011),x2011,a6)),
% 58.87/58.89 inference(rename_variables,[],[22])).
% 58.87/58.89 cnf(203,plain,
% 58.87/58.89 (P2(a3,a6,f7(a5,a4))),
% 58.87/58.89 inference(scs_inference,[],[157,79,179,72,20,18,22,201,100,50,145,16,96,23,40,188,190,194,196,2,31,30,3,13,14,10,9,11,12,32,33])).
% 58.87/58.89 cnf(214,plain,
% 58.87/58.89 (E(f8(f7(a6,a6)),f7(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[185,2])).
% 58.87/58.89 cnf(215,plain,
% 58.87/58.89 (E(f11(a6,x2151),f7(f11(a6,x2151),f11(a6,x2151)))),
% 58.87/58.89 inference(scs_inference,[],[72,185,23,2,30])).
% 58.87/58.89 cnf(216,plain,
% 58.87/58.89 (P2(x2161,x2162,f7(x2161,x2162))),
% 58.87/58.89 inference(rename_variables,[],[23])).
% 58.87/58.89 cnf(218,plain,
% 58.87/58.89 (E(a4,f11(f7(a1,a6),a9))),
% 58.87/58.89 inference(scs_inference,[],[193,72,185,24,23,2,30,31])).
% 58.87/58.89 cnf(219,plain,
% 58.87/58.89 (P1(x2191,x2192,f11(x2191,x2192))),
% 58.87/58.89 inference(rename_variables,[],[24])).
% 58.87/58.89 cnf(222,plain,
% 58.87/58.89 (E(x2221,f7(x2221,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(223,plain,
% 58.87/58.89 (P1(f8(a6),x2231,f7(f11(a6,x2231),f11(a6,x2231)))),
% 58.87/58.89 inference(scs_inference,[],[193,54,72,66,185,142,24,23,40,2,30,31,14,9])).
% 58.87/58.89 cnf(225,plain,
% 58.87/58.89 (E(x2251,f7(x2251,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(226,plain,
% 58.87/58.89 (E(f8(a6),f8(f7(a6,a6)))),
% 58.87/58.89 inference(scs_inference,[],[193,54,72,66,185,181,142,24,23,40,222,2,30,31,14,9,13,3])).
% 58.87/58.89 cnf(227,plain,
% 58.87/58.89 (P1(f7(a1,a6),f7(a9,a6),a4)),
% 58.87/58.89 inference(scs_inference,[],[193,54,72,66,185,181,142,24,23,40,222,225,2,30,31,14,9,13,3,10])).
% 58.87/58.89 cnf(228,plain,
% 58.87/58.89 (E(x2281,f7(x2281,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(229,plain,
% 58.87/58.89 (P1(f7(a1,a6),a9,f7(a4,a6))),
% 58.87/58.89 inference(scs_inference,[],[193,54,72,66,185,181,142,24,23,40,222,225,228,2,30,31,14,9,13,3,10,11])).
% 58.87/58.89 cnf(230,plain,
% 58.87/58.89 (E(x2301,f7(x2301,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(233,plain,
% 58.87/58.89 (P1(f7(a1,a6),f7(f11(a9,a6),f11(a9,a6)),f11(a4,a6))),
% 58.87/58.89 inference(scs_inference,[],[193,54,60,72,66,185,181,142,24,219,23,40,222,225,228,230,2,30,31,14,9,13,3,10,11,12,35])).
% 58.87/58.89 cnf(235,plain,
% 58.87/58.89 (P1(x2351,x2352,f11(x2351,x2352))),
% 58.87/58.89 inference(rename_variables,[],[24])).
% 58.87/58.89 cnf(241,plain,
% 58.87/58.89 (P2(f11(a6,x2411),a6,a6)),
% 58.87/58.89 inference(scs_inference,[],[193,54,60,72,66,18,21,185,181,97,142,24,219,23,40,222,225,228,230,2,30,31,14,9,13,3,10,11,12,35,32,33])).
% 58.87/58.89 cnf(244,plain,
% 58.87/58.89 (P2(a4,a4,f11(f7(a1,a6),f7(a9,a9)))),
% 58.87/58.89 inference(scs_inference,[],[193,54,60,72,66,18,21,185,181,97,142,24,219,235,23,216,40,222,225,228,230,2,30,31,14,9,13,3,10,11,12,35,32,33,36])).
% 58.87/58.89 cnf(255,plain,
% 58.87/58.89 (E(f8(f7(a6,a6)),f8(a6))),
% 58.87/58.89 inference(scs_inference,[],[226,2])).
% 58.87/58.89 cnf(257,plain,
% 58.87/58.89 (P2(f11(a6,x2571),f11(a6,x2571),f11(a6,x2571))),
% 58.87/58.89 inference(rename_variables,[],[72])).
% 58.87/58.89 cnf(262,plain,
% 58.87/58.89 (E(f7(x2621,a6),x2621)),
% 58.87/58.89 inference(rename_variables,[],[96])).
% 58.87/58.89 cnf(263,plain,
% 58.87/58.89 (E(f7(a4,a6),f11(f7(a1,a6),a9))),
% 58.87/58.89 inference(scs_inference,[],[233,60,72,18,214,215,226,218,142,96,262,2,13,14,10,9,3])).
% 58.87/58.89 cnf(266,plain,
% 58.87/58.89 (P2(f11(a6,x2661),f11(a6,x2661),f11(a6,x2661))),
% 58.87/58.89 inference(rename_variables,[],[72])).
% 58.87/58.89 cnf(267,plain,
% 58.87/58.89 (P1(f8(a6),x2671,f11(a6,x2671))),
% 58.87/58.89 inference(scs_inference,[],[223,233,60,72,257,18,214,178,215,226,218,142,96,262,2,13,14,10,9,3,12,11])).
% 58.87/58.89 cnf(269,plain,
% 58.87/58.89 (P1(f7(a1,a6),f11(a9,a6),f7(f11(a4,a6),f11(a4,a6)))),
% 58.87/58.89 inference(scs_inference,[],[193,223,233,60,72,257,18,214,149,178,215,226,218,43,142,96,262,2,13,14,10,9,3,12,11,35])).
% 58.87/58.89 cnf(276,plain,
% 58.87/58.89 (P2(f11(a6,x2761),f7(a6,a6),f7(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[193,223,233,60,72,257,266,18,214,149,178,161,215,226,116,218,50,43,142,96,262,2,13,14,10,9,3,12,11,35,32,33])).
% 58.87/58.89 cnf(285,plain,
% 58.87/58.89 (E(f11(f7(a1,a6),a9),f7(a4,a6))),
% 58.87/58.89 inference(scs_inference,[],[263,2])).
% 58.87/58.89 cnf(286,plain,
% 58.87/58.89 (E(a6,f7(f8(a6),a6))),
% 58.87/58.89 inference(scs_inference,[],[21,97,263,2,30])).
% 58.87/58.89 cnf(288,plain,
% 58.87/58.89 (P2(x2881,f8(x2881),a6)),
% 58.87/58.89 inference(rename_variables,[],[21])).
% 58.87/58.89 cnf(290,plain,
% 58.87/58.89 (P2(f7(a6,a6),f8(a6),a6)),
% 58.87/58.89 inference(scs_inference,[],[21,288,97,263,255,2,30,13])).
% 58.87/58.89 cnf(291,plain,
% 58.87/58.89 (P2(x2911,f8(x2911),a6)),
% 58.87/58.89 inference(rename_variables,[],[21])).
% 58.87/58.89 cnf(292,plain,
% 58.87/58.89 (P2(x2921,f8(x2921),f8(a6))),
% 58.87/58.89 inference(scs_inference,[],[21,288,291,97,263,255,142,2,30,13,14])).
% 58.87/58.89 cnf(295,plain,
% 58.87/58.89 (P1(f7(a6,a6),f8(a6),f11(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[269,21,288,291,97,191,263,255,142,96,2,30,13,14,9,10])).
% 58.87/58.89 cnf(296,plain,
% 58.87/58.89 (P1(f7(a6,a6),f7(a6,a6),f7(f11(a6,a6),f11(a6,a6)))),
% 58.87/58.89 inference(scs_inference,[],[269,100,21,288,291,97,191,263,255,215,142,96,2,30,13,14,9,10,11])).
% 58.87/58.89 cnf(298,plain,
% 58.87/58.89 (P2(f8(a6),x2981,x2981)),
% 58.87/58.89 inference(scs_inference,[],[269,100,21,288,291,18,97,191,263,255,215,142,96,2,30,13,14,9,10,11,12])).
% 58.87/58.89 cnf(299,plain,
% 58.87/58.89 (P1(f7(a6,a6),f11(a6,a6),f11(f11(a6,a6),f7(a6,a6)))),
% 58.87/58.89 inference(scs_inference,[],[269,100,21,288,291,24,18,97,191,263,255,215,142,96,2,30,13,14,9,10,11,12,35])).
% 58.87/58.89 cnf(302,plain,
% 58.87/58.89 (P2(a6,a6,f8(a6))),
% 58.87/58.89 inference(scs_inference,[],[269,100,21,288,291,24,18,97,112,23,191,263,255,215,142,96,2,30,13,14,9,10,11,12,35,32])).
% 58.87/58.89 cnf(304,plain,
% 58.87/58.89 (P2(x3041,f8(x3041),a6)),
% 58.87/58.89 inference(rename_variables,[],[21])).
% 58.87/58.89 cnf(307,plain,
% 58.87/58.89 (P2(f8(a6),f8(a6),a6)),
% 58.87/58.89 inference(scs_inference,[],[269,100,21,288,291,304,24,22,18,97,112,23,191,263,255,215,142,96,2,30,13,14,9,10,11,12,35,32,33])).
% 58.87/58.89 cnf(318,plain,
% 58.87/58.89 (E(f7(a6,a6),f8(a6))),
% 58.87/58.89 inference(scs_inference,[],[181,2])).
% 58.87/58.89 cnf(319,plain,
% 58.87/58.89 (E(a6,f8(f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[21,181,298,2,30])).
% 58.87/58.89 cnf(324,plain,
% 58.87/58.89 (E(x3241,f7(x3241,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(325,plain,
% 58.87/58.89 (P1(f7(a6,a6),f7(f7(a6,a6),a6),f11(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[100,72,21,181,40,324,298,2,30,13,10])).
% 58.87/58.89 cnf(326,plain,
% 58.87/58.89 (E(x3261,f7(x3261,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(327,plain,
% 58.87/58.89 (P2(f8(x3271),x3271,f8(a6))),
% 58.87/58.89 inference(scs_inference,[],[100,72,21,22,181,142,40,324,298,2,30,13,10,14])).
% 58.87/58.89 cnf(328,plain,
% 58.87/58.89 (P1(f7(f7(a1,a6),a6),a9,a4)),
% 58.87/58.89 inference(scs_inference,[],[193,100,72,21,22,181,142,40,324,326,298,2,30,13,10,14,9])).
% 58.87/58.89 cnf(329,plain,
% 58.87/58.89 (E(x3291,f7(x3291,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(331,plain,
% 58.87/58.89 (E(x3311,f7(x3311,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(334,plain,
% 58.87/58.89 (P1(f7(a6,a6),a3,f11(f11(a6,a1),a2))),
% 58.87/58.89 inference(scs_inference,[],[193,79,100,72,21,24,22,181,142,40,324,326,329,331,298,15,2,30,13,10,14,9,12,11,35])).
% 58.87/58.89 cnf(338,plain,
% 58.87/58.89 (P2(a6,f8(f8(a6)),a6)),
% 58.87/58.89 inference(scs_inference,[],[193,79,100,72,21,24,22,181,142,40,324,326,329,331,292,298,290,15,2,30,13,10,14,9,12,11,35,32])).
% 58.87/58.89 cnf(341,plain,
% 58.87/58.89 (P2(f8(a3),a5,f8(a4))),
% 58.87/58.89 inference(scs_inference,[],[193,79,100,72,21,24,22,20,18,181,142,40,324,326,329,331,292,298,290,15,2,30,13,10,14,9,12,11,35,32,33])).
% 58.87/58.89 cnf(355,plain,
% 58.87/58.89 (P2(a6,a6,f8(f7(a6,a6)))),
% 58.87/58.89 inference(scs_inference,[],[177,218,18,2,13])).
% 58.87/58.89 cnf(356,plain,
% 58.87/58.89 (P2(a6,x3561,x3561)),
% 58.87/58.89 inference(rename_variables,[],[18])).
% 58.87/58.89 cnf(358,plain,
% 58.87/58.89 (E(x3581,f7(x3581,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(362,plain,
% 58.87/58.89 (E(x3621,f7(x3621,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(364,plain,
% 58.87/58.89 (E(x3641,f7(x3641,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(365,plain,
% 58.87/58.89 (P2(f7(f7(a6,a6),a6),x3651,x3651)),
% 58.87/58.89 inference(scs_inference,[],[79,334,177,267,218,18,114,263,97,40,358,362,364,2,13,9,14,10,11,12])).
% 58.87/58.89 cnf(370,plain,
% 58.87/58.89 (P2(f8(a2),a10,f8(a9))),
% 58.87/58.89 inference(scs_inference,[],[79,334,21,177,267,218,19,22,18,356,114,263,97,40,358,362,364,165,2,13,9,14,10,11,12,32,33])).
% 58.87/58.89 cnf(388,plain,
% 58.87/58.89 (E(f7(f8(x3881),x3881),a6)),
% 58.87/58.89 inference(scs_inference,[],[23,22,286,2,30])).
% 58.87/58.89 cnf(390,plain,
% 58.87/58.89 (P2(x3901,x3902,f7(x3901,x3902))),
% 58.87/58.89 inference(rename_variables,[],[23])).
% 58.87/58.89 cnf(392,plain,
% 58.87/58.89 (P2(f7(a6,a6),f7(a6,a6),f8(f7(a6,a6)))),
% 58.87/58.89 inference(scs_inference,[],[214,114,23,22,286,2,30,13])).
% 58.87/58.89 cnf(396,plain,
% 58.87/58.89 (E(x3961,f7(x3961,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(397,plain,
% 58.87/58.89 (P2(f8(x3971),x3971,f7(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[328,299,214,181,114,23,22,327,318,40,286,2,30,13,9,10,14])).
% 58.87/58.89 cnf(400,plain,
% 58.87/58.89 (P2(f8(a6),f7(x4001,a6),x4001)),
% 58.87/58.89 inference(scs_inference,[],[328,299,214,181,142,114,112,23,22,327,318,40,396,286,295,2,30,13,9,10,14,11,12])).
% 58.87/58.89 cnf(401,plain,
% 58.87/58.89 (P2(a6,x4011,f7(f8(a6),x4011))),
% 58.87/58.89 inference(scs_inference,[],[328,299,214,181,142,21,114,112,23,390,22,18,327,318,40,396,286,295,2,30,13,9,10,14,11,12,32])).
% 58.87/58.89 cnf(403,plain,
% 58.87/58.89 (P2(x4031,f8(x4031),a6)),
% 58.87/58.89 inference(rename_variables,[],[21])).
% 58.87/58.89 cnf(406,plain,
% 58.87/58.89 (P1(f7(a6,a6),a4,f11(f11(a6,a1),a9))),
% 58.87/58.89 inference(scs_inference,[],[79,328,299,214,181,142,21,114,112,23,390,24,22,18,327,318,40,396,286,295,16,2,30,13,9,10,14,11,12,32,35])).
% 58.87/58.89 cnf(410,plain,
% 58.87/58.89 (P2(f7(x4101,a6),f8(a6),x4101)),
% 58.87/58.89 inference(scs_inference,[],[79,328,299,214,181,142,21,403,114,112,23,390,24,22,18,327,318,40,396,286,295,16,2,30,13,9,10,14,11,12,32,35,33])).
% 58.87/58.89 cnf(427,plain,
% 58.87/58.89 (P2(f7(a6,a6),a6,f8(f7(a6,a6)))),
% 58.87/58.89 inference(scs_inference,[],[177,114,23,327,319,2,30,13])).
% 58.87/58.89 cnf(433,plain,
% 58.87/58.89 (E(x4331,f7(x4331,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(434,plain,
% 58.87/58.89 (P1(a1,a2,f7(a3,a6))),
% 58.87/58.89 inference(scs_inference,[],[406,177,318,114,23,227,298,327,15,40,433,319,2,30,13,14,9,10,11])).
% 58.87/58.89 cnf(442,plain,
% 58.87/58.89 (P2(f11(a6,x4421),f8(a6),f8(a6))),
% 58.87/58.89 inference(scs_inference,[],[406,72,177,21,318,114,23,227,292,298,51,327,15,17,40,433,319,2,30,13,14,9,10,11,12,32,33])).
% 58.87/58.89 cnf(454,plain,
% 58.87/58.89 (E(f7(f8(x4541),x4541),f7(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[23,388,397,2,30])).
% 58.87/58.89 cnf(456,plain,
% 58.87/58.89 (P2(x4561,x4562,f7(x4561,x4562))),
% 58.87/58.89 inference(rename_variables,[],[23])).
% 58.87/58.89 cnf(458,plain,
% 58.87/58.89 (P2(f7(a6,a6),f7(a6,a6),f8(a6))),
% 58.87/58.89 inference(scs_inference,[],[214,23,388,292,397,2,30,13])).
% 58.87/58.89 cnf(460,plain,
% 58.87/58.89 (P1(f7(a1,a6),f7(a9,a6),f7(a4,a6))),
% 58.87/58.89 inference(scs_inference,[],[214,229,23,388,292,40,397,2,30,13,10])).
% 58.87/58.89 cnf(462,plain,
% 58.87/58.89 (P1(f8(a6),a3,f11(f11(a6,a1),a2))),
% 58.87/58.89 inference(scs_inference,[],[334,214,318,229,23,388,292,40,397,2,30,13,10,9])).
% 58.87/58.89 cnf(465,plain,
% 58.87/58.89 (P1(a1,a9,f11(f7(a1,a6),a9))),
% 58.87/58.89 inference(scs_inference,[],[334,214,218,318,229,16,23,388,292,298,40,397,2,30,13,10,9,14,11])).
% 58.87/58.89 cnf(466,plain,
% 58.87/58.89 (P2(f8(a6),x4661,f7(x4661,a6))),
% 58.87/58.89 inference(scs_inference,[],[334,214,142,218,318,229,16,23,388,292,298,97,40,397,2,30,13,10,9,14,11,12])).
% 58.87/58.89 cnf(467,plain,
% 58.87/58.89 (P2(f7(a6,a6),f7(f8(a6),a6),a6)),
% 58.87/58.89 inference(scs_inference,[],[334,214,142,218,318,21,229,114,16,23,388,292,298,97,40,397,2,30,13,10,9,14,11,12,33])).
% 58.87/58.89 cnf(470,plain,
% 58.87/58.89 (P2(x4701,f8(x4701),a6)),
% 58.87/58.89 inference(rename_variables,[],[21])).
% 58.87/58.89 cnf(472,plain,
% 58.87/58.89 (P2(a6,a6,f8(f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[334,214,142,218,318,21,470,229,114,16,23,456,388,292,298,97,40,397,400,2,30,13,10,9,14,11,12,33,32])).
% 58.87/58.89 cnf(486,plain,
% 58.87/58.89 (E(a6,f7(f8(a6),f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[21,454,401,2,30])).
% 58.87/58.89 cnf(488,plain,
% 58.87/58.89 (P2(x4881,f8(x4881),a6)),
% 58.87/58.89 inference(rename_variables,[],[21])).
% 58.87/58.89 cnf(491,plain,
% 58.87/58.89 (P2(x4911,f7(a6,a6),f7(x4911,f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[181,21,23,454,401,2,30,3,13])).
% 58.87/58.89 cnf(492,plain,
% 58.87/58.89 (P2(x4921,x4922,f7(x4921,x4922))),
% 58.87/58.89 inference(rename_variables,[],[23])).
% 58.87/58.89 cnf(497,plain,
% 58.87/58.89 (P1(f7(a6,a6),f7(a6,a6),f11(a6,f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[79,110,181,318,21,114,23,454,401,2,30,3,13,14,9,10])).
% 58.87/58.89 cnf(499,plain,
% 58.87/58.89 (P2(f7(a6,a6),f8(f8(a6)),a6)),
% 58.87/58.89 inference(scs_inference,[],[79,110,181,318,21,488,114,23,454,401,2,30,3,13,14,9,10,12])).
% 58.87/58.89 cnf(500,plain,
% 58.87/58.89 (P2(x5001,f8(x5001),a6)),
% 58.87/58.89 inference(rename_variables,[],[21])).
% 58.87/58.89 cnf(506,plain,
% 58.87/58.89 (P2(f7(a6,a6),f8(a6),f7(f8(a6),f7(a6,a6)))),
% 58.87/58.89 inference(scs_inference,[],[79,110,181,318,21,488,500,434,114,23,492,40,454,458,401,203,2,30,3,13,14,9,10,12,11,32,33])).
% 58.87/58.89 cnf(517,plain,
% 58.87/58.89 (E(f7(a6,a6),f7(f7(a6,a6),f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[114,491,486,2,30])).
% 58.87/58.89 cnf(519,plain,
% 58.87/58.89 (P2(f7(a6,a6),x5191,x5191)),
% 58.87/58.89 inference(rename_variables,[],[114])).
% 58.87/58.89 cnf(521,plain,
% 58.87/58.89 (P2(x5211,f8(a6),x5211)),
% 58.87/58.89 inference(scs_inference,[],[318,114,51,491,486,2,30,13])).
% 58.87/58.89 cnf(522,plain,
% 58.87/58.89 (P1(f8(a6),f7(a6,a6),f11(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[100,318,114,51,491,486,2,30,13,9])).
% 58.87/58.89 cnf(523,plain,
% 58.87/58.89 (P2(f8(f7(a6,a6)),a6,f7(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[100,214,318,114,51,17,491,486,2,30,13,9,14])).
% 58.87/58.89 cnf(525,plain,
% 58.87/58.89 (P2(f8(a6),f7(a6,a6),f8(f7(a6,a6)))),
% 58.87/58.89 inference(scs_inference,[],[100,214,318,114,51,17,392,491,486,2,30,13,9,14,12])).
% 58.87/58.89 cnf(528,plain,
% 58.87/58.89 (P1(a1,a9,f7(a4,a6))),
% 58.87/58.89 inference(scs_inference,[],[462,100,214,285,318,114,51,17,40,392,491,465,486,2,30,13,9,14,12,10,11])).
% 58.87/58.89 cnf(529,plain,
% 58.87/58.89 (P2(f7(a6,a6),x5291,f7(f7(x5291,a6),f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[462,100,214,285,318,114,519,23,51,17,40,392,491,465,410,486,2,30,13,9,14,12,10,11,33])).
% 58.87/58.89 cnf(542,plain,
% 58.87/58.89 (E(f7(f8(a6),f7(x5421,a6)),x5421)),
% 58.87/58.89 inference(scs_inference,[],[23,517,400,2,30])).
% 58.87/58.89 cnf(545,plain,
% 58.87/58.89 (P2(f7(a6,a6),a6,f8(a6))),
% 58.87/58.89 inference(scs_inference,[],[177,23,292,517,400,2,30,13])).
% 58.87/58.89 cnf(547,plain,
% 58.87/58.89 (P2(a6,f7(a6,a6),f8(a6))),
% 58.87/58.89 inference(scs_inference,[],[177,23,292,327,517,400,2,30,13,12])).
% 58.87/58.89 cnf(549,plain,
% 58.87/58.89 (P2(f8(f7(a6,a6)),a6,a6)),
% 58.87/58.89 inference(scs_inference,[],[177,23,292,327,17,517,400,2,30,13,12,14])).
% 58.87/58.89 cnf(551,plain,
% 58.87/58.89 (P1(f7(a1,a6),a2,a3)),
% 58.87/58.89 inference(scs_inference,[],[15,177,23,292,327,17,40,517,400,2,30,13,12,14,9])).
% 58.87/58.89 cnf(552,plain,
% 58.87/58.89 (E(x5521,f7(x5521,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(553,plain,
% 58.87/58.89 (P1(f8(a6),f8(a6),f11(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[522,15,177,318,23,292,327,17,40,517,400,2,30,13,12,14,9,10])).
% 58.87/58.89 cnf(556,plain,
% 58.87/58.89 (P1(f8(a6),f11(a6,a6),f11(f11(a6,a6),f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[522,24,15,177,318,23,292,327,17,40,552,517,400,2,30,13,12,14,9,10,11,35])).
% 58.87/58.89 cnf(559,plain,
% 58.87/58.89 (P2(a6,f7(a6,a6),f7(f7(a6,a6),f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[522,24,15,177,318,21,22,23,292,327,17,40,552,517,529,400,2,30,13,12,14,9,10,11,35,32])).
% 58.87/58.89 cnf(579,plain,
% 58.87/58.89 (E(x5791,f7(f7(x5791,a6),a6))),
% 58.87/58.89 inference(scs_inference,[],[112,97,542,2,30])).
% 58.87/58.89 cnf(580,plain,
% 58.87/58.89 (P2(a6,x5801,f7(x5801,a6))),
% 58.87/58.89 inference(rename_variables,[],[97])).
% 58.87/58.89 cnf(583,plain,
% 58.87/58.89 (E(x5831,f7(x5831,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(585,plain,
% 58.87/58.89 (P2(f7(a2,a6),f8(a9),f7(a10,a6))),
% 58.87/58.89 inference(scs_inference,[],[556,181,112,97,40,583,151,542,2,30,13,9,12])).
% 58.87/58.89 cnf(586,plain,
% 58.87/58.89 (E(x5861,f7(x5861,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(588,plain,
% 58.87/58.89 (E(x5881,f7(x5881,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(589,plain,
% 58.87/58.89 (P1(f7(a1,a6),f7(a2,a6),a3)),
% 58.87/58.89 inference(scs_inference,[],[556,551,181,112,97,40,583,586,588,151,542,2,30,13,9,12,14,10])).
% 58.87/58.89 cnf(590,plain,
% 58.87/58.89 (E(x5901,f7(x5901,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(597,plain,
% 58.87/58.89 (P2(f7(a6,a6),f7(f7(x5971,a6),a6),x5971)),
% 58.87/58.89 inference(scs_inference,[],[556,551,181,112,21,114,18,97,580,40,583,586,588,590,151,542,2,30,13,9,12,14,10,11,32,33])).
% 58.87/58.89 cnf(609,plain,
% 58.87/58.89 (E(a6,f7(a6,f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[112,579,491,2,30])).
% 58.87/58.89 cnf(611,plain,
% 58.87/58.89 (P2(a6,f7(x6111,a6),x6111)),
% 58.87/58.89 inference(rename_variables,[],[112])).
% 58.87/58.89 cnf(614,plain,
% 58.87/58.89 (E(x6141,f7(x6141,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(616,plain,
% 58.87/58.89 (E(x6161,f7(x6161,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(618,plain,
% 58.87/58.89 (E(x6181,f7(x6181,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(619,plain,
% 58.87/58.89 (P2(f7(a3,a6),f8(a4),f7(a5,a6))),
% 58.87/58.89 inference(scs_inference,[],[551,112,40,614,616,618,189,579,491,2,30,13,14,9,12])).
% 58.87/58.89 cnf(620,plain,
% 58.87/58.89 (E(x6201,f7(x6201,a6))),
% 58.87/58.89 inference(rename_variables,[],[40])).
% 58.87/58.89 cnf(623,plain,
% 58.87/58.89 (P1(x6231,f8(a6),f11(x6231,a6))),
% 58.87/58.89 inference(scs_inference,[],[551,43,318,112,553,40,614,616,618,620,189,579,491,2,30,13,14,9,12,11,10])).
% 58.87/58.89 cnf(628,plain,
% 58.87/58.89 (P2(x6281,f8(f7(x6281,a6)),f7(a6,a6))),
% 58.87/58.89 inference(scs_inference,[],[193,551,24,43,318,112,611,21,553,97,40,614,616,618,620,189,579,491,2,30,13,14,9,12,11,10,35,32])).
% 58.87/58.89 cnf(632,plain,
% 58.87/58.89 (P2(a6,x6321,f7(f7(x6321,a6),a6))),
% 58.87/58.89 inference(scs_inference,[],[193,551,24,43,318,112,611,21,553,18,97,40,614,616,618,620,189,597,579,491,2,30,13,14,9,12,11,10,35,32,33])).
% 58.87/58.89 cnf(643,plain,
% 58.87/58.89 (E(a6,f7(f7(a6,a6),f8(a6)))),
% 58.87/58.89 inference(scs_inference,[],[161,609,491,2,30])).
% 58.87/58.89 cnf(645,plain,
% 58.87/58.89 (P2(f7(a6,a6),f7(x6451,a6),x6451)),
% 58.87/58.89 inference(rename_variables,[],[161])).
% 58.87/58.89 cnf(649,plain,
% 58.87/58.89 (E(x6491,f7(f7(x6491,a6),a6))),
% 58.87/58.89 inference(rename_variables,[],[579])).
% 58.87/58.89 cnf(651,plain,
% 58.87/58.89 (E(x6511,f7(f7(x6511,a6),a6))),
% 58.87/58.89 inference(rename_variables,[],[579])).
% 58.87/58.89 cnf(652,plain,
% 58.87/58.89 (P1(f7(f7(a1,a6),a6),a2,f7(a3,a6))),
% 58.87/58.89 inference(scs_inference,[],[142,434,161,19,579,649,651,355,159,609,491,2,30,13,12,14,9])).
% 58.87/58.89 cnf(653,plain,
% 58.87/58.89 (E(x6531,f7(f7(x6531,a6),a6))),
% 58.87/58.89 inference(rename_variables,[],[579])).
% 58.87/58.89 cnf(655,plain,
% 58.87/58.89 (E(x6551,f7(f7(x6551,a6),a6))),
% 58.87/58.89 inference(rename_variables,[],[579])).
% 58.87/58.89 cnf(659,plain,
% 58.87/58.89 (P2(f7(a6,a6),f7(x6591,a6),x6591)),
% 58.87/58.89 inference(rename_variables,[],[161])).
% 58.87/58.89 cnf(662,plain,
% 58.87/58.89 (P2(f8(a6),f7(f7(a6,a6),a6),f8(a6))),
% 58.87/58.89 inference(scs_inference,[],[551,142,434,161,645,659,21,19,579,649,651,653,655,355,159,506,547,609,491,2,30,13,12,14,9,10,11,33,32])).
% 58.87/58.89 cnf(671,plain,
% 58.87/58.89 (P2(f7(a3,a6),f7(f8(a4),a6),a5)),
% 58.87/58.89 inference(scs_inference,[],[40,197,643,2,13])).
% 58.87/58.89 cnf(696,plain,
% 58.87/58.89 (P2(f7(x6961,a6),f7(a6,a6),x6961)),
% 58.87/58.89 inference(scs_inference,[],[181,410,81,2,13])).
% 58.87/58.89 cnf(699,plain,
% 58.87/58.89 (E(x6991,f7(f7(x6991,a6),a6))),
% 58.87/58.89 inference(rename_variables,[],[579])).
% 58.87/58.89 cnf(700,plain,
% 58.87/58.89 (P2(f8(f8(a6)),f7(a6,a6),a6)),
% 58.87/58.89 inference(scs_inference,[],[181,318,388,589,579,410,491,497,81,2,13,9,11,14])).
% 58.87/58.89 cnf(706,plain,
% 58.87/58.89 (P2(a6,f7(x7061,a6),f7(f8(a6),x7061))),
% 58.87/58.90 inference(scs_inference,[],[16,181,318,388,112,589,161,579,699,410,401,597,491,497,81,2,13,9,11,14,12,10,32])).
% 58.87/58.90 cnf(707,plain,
% 58.87/58.90 (P2(a6,x7071,f7(f8(a6),x7071))),
% 58.87/58.90 inference(rename_variables,[],[401])).
% 58.87/58.90 cnf(708,plain,
% 58.87/58.90 (P2(a6,f7(x7081,a6),x7081)),
% 58.87/58.90 inference(rename_variables,[],[112])).
% 58.87/58.90 cnf(710,plain,
% 58.87/58.90 (P2(a6,f7(f8(a6),f7(x7101,a6)),x7101)),
% 58.87/58.90 inference(scs_inference,[],[16,181,318,388,112,708,589,161,18,579,699,410,401,707,597,491,497,81,2,13,9,11,14,12,10,32,33])).
% 58.87/58.90 cnf(725,plain,
% 58.87/58.90 (P2(f8(a6),f8(a6),f8(f7(a6,a6)))),
% 58.87/58.90 inference(scs_inference,[],[318,525,13])).
% 58.87/58.90 cnf(727,plain,
% 58.87/58.90 (E(x7271,f7(x7271,a6))),
% 58.87/58.90 inference(rename_variables,[],[40])).
% 58.87/58.90 cnf(731,plain,
% 58.87/58.90 (E(x7311,f7(x7311,a6))),
% 58.87/58.90 inference(rename_variables,[],[40])).
% 58.87/58.90 cnf(740,plain,
% 58.87/58.90 (P2(a6,f7(a5,a6),f7(a3,f8(a4)))),
% 58.87/58.90 inference(scs_inference,[],[652,214,318,460,112,21,327,23,40,727,731,628,521,365,525,619,13,9,12,11,14,10,32,33])).
% 58.87/58.90 cnf(749,plain,
% 58.87/58.90 (P2(f8(a6),x7491,x7491)),
% 58.87/58.90 inference(rename_variables,[],[298])).
% 58.87/58.90 cnf(752,plain,
% 58.87/58.90 (P1(f8(a6),f7(a6,a6),f7(f11(a6,a6),f11(a6,a6)))),
% 58.87/58.90 inference(scs_inference,[],[142,318,298,292,296,523,30,13,9])).
% 58.87/58.90 cnf(754,plain,
% 58.87/58.90 (P2(a6,f8(f8(a6)),f8(a6))),
% 58.87/58.90 inference(scs_inference,[],[142,318,298,292,296,427,338,523,30,13,9,12,14])).
% 58.87/58.90 cnf(757,plain,
% 58.87/58.90 (P2(f7(f8(a6),a6),f7(x7571,a6),x7571)),
% 58.87/58.90 inference(scs_inference,[],[15,142,318,579,298,749,97,112,292,296,427,338,523,30,13,9,12,14,10,32])).
% 58.87/58.90 cnf(758,plain,
% 58.87/58.90 (P2(a6,x7581,f7(x7581,a6))),
% 58.87/58.90 inference(rename_variables,[],[97])).
% 58.87/58.90 cnf(759,plain,
% 58.87/58.90 (P2(f8(a6),x7591,x7591)),
% 58.87/58.90 inference(rename_variables,[],[298])).
% 58.87/58.90 cnf(761,plain,
% 58.87/58.90 (P2(f8(a6),x7611,f7(f7(x7611,a6),a6))),
% 58.87/58.90 inference(scs_inference,[],[15,142,318,579,298,749,759,97,758,112,292,296,427,338,523,30,13,9,12,14,10,32,33])).
% 58.87/58.90 cnf(776,plain,
% 58.87/58.90 (P2(f11(a6,x7761),f8(a6),f7(a6,a6))),
% 58.93/58.90 inference(scs_inference,[],[318,298,50,276,30,13])).
% 58.93/58.90 cnf(779,plain,
% 58.93/58.90 (P1(f8(a6),f8(a6),f7(f11(a6,a6),f11(a6,a6)))),
% 58.93/58.90 inference(scs_inference,[],[752,318,298,50,325,467,276,30,13,9,12,10])).
% 58.93/58.90 cnf(799,plain,
% 58.93/58.90 (E(x7991,f7(f7(x7991,a6),a6))),
% 58.93/58.90 inference(rename_variables,[],[579])).
% 58.93/58.90 cnf(800,plain,
% 58.93/58.90 (P2(f8(a6),a6,f8(f8(a6)))),
% 58.93/58.90 inference(scs_inference,[],[16,181,142,318,302,579,757,472,779,632,30,13,9,11,12])).
% 58.93/58.90 cnf(801,plain,
% 58.93/58.90 (P2(f8(f8(a6)),f7(a6,a6),f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[16,181,142,318,302,579,757,700,472,779,632,30,13,9,11,12,14])).
% 58.93/58.90 cnf(802,plain,
% 58.93/58.90 (P1(a1,f7(f7(a2,a6),a6),f7(a3,a6))),
% 58.93/58.90 inference(scs_inference,[],[16,181,142,434,318,302,579,799,757,700,472,779,632,30,13,9,11,12,14,10])).
% 58.93/58.90 cnf(804,plain,
% 58.93/58.90 (P1(f7(a6,a6),f7(a4,a6),f11(f11(a6,a1),a9))),
% 58.93/58.90 inference(scs_inference,[],[79,24,16,181,142,434,318,528,302,579,799,757,700,472,779,632,30,13,9,11,12,14,10,35])).
% 58.93/58.90 cnf(808,plain,
% 58.93/58.90 (P2(f7(f7(x8081,a6),a6),f8(a6),x8081)),
% 58.93/58.90 inference(scs_inference,[],[79,24,16,181,142,434,318,528,302,161,579,799,410,597,757,700,472,779,632,30,13,9,11,12,14,10,35,32])).
% 58.93/58.90 cnf(824,plain,
% 58.93/58.90 (E(x8241,f7(x8241,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(826,plain,
% 58.93/58.90 (P1(x8261,f8(a6),f7(f11(x8261,a6),a6))),
% 58.93/58.90 inference(scs_inference,[],[804,318,623,40,824,244,13,9,11])).
% 58.93/58.90 cnf(827,plain,
% 58.93/58.90 (E(x8271,f7(x8271,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(828,plain,
% 58.93/58.90 (P2(f7(a4,a6),a4,f11(f7(a1,a6),f7(a9,a9)))),
% 58.93/58.90 inference(scs_inference,[],[804,318,623,40,824,827,244,13,9,11,12])).
% 58.93/58.90 cnf(829,plain,
% 58.93/58.90 (E(x8291,f7(x8291,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(831,plain,
% 58.93/58.90 (P1(a1,f7(a9,a6),a4)),
% 58.93/58.90 inference(scs_inference,[],[804,16,214,318,623,40,824,827,829,244,725,13,9,11,12,14,10])).
% 58.93/58.90 cnf(833,plain,
% 58.93/58.90 (P1(f7(a6,a6),a4,f11(f11(a6,a1),f7(a9,a6)))),
% 58.93/58.90 inference(scs_inference,[],[79,804,24,16,214,318,623,40,824,827,829,244,725,13,9,11,12,14,10,35])).
% 58.93/58.90 cnf(837,plain,
% 58.93/58.90 (P2(f8(a6),a6,f7(f8(a6),f8(a6)))),
% 58.93/58.90 inference(scs_inference,[],[79,804,24,16,214,318,302,623,40,824,827,829,401,244,725,13,9,11,12,14,10,35,32])).
% 58.93/58.90 cnf(838,plain,
% 58.93/58.90 (P2(a6,x8381,f7(f8(a6),x8381))),
% 58.93/58.90 inference(rename_variables,[],[401])).
% 58.93/58.90 cnf(840,plain,
% 58.93/58.90 (P2(a6,f7(f8(a6),f8(a6)),a6)),
% 58.93/58.90 inference(scs_inference,[],[79,804,24,16,214,318,302,623,40,824,827,829,307,401,838,244,725,13,9,11,12,14,10,35,32,33])).
% 58.93/58.90 cnf(843,plain,
% 58.93/58.90 (P1(a4,f8(a6),f11(f7(a1,a6),f11(a9,a6)))),
% 58.93/58.90 inference(scs_inference,[],[193,79,804,24,43,16,214,318,302,623,40,824,827,829,307,401,838,244,725,13,9,11,12,14,10,35,32,33,34])).
% 58.93/58.90 cnf(865,plain,
% 58.93/58.90 (P2(f7(f7(x8651,a6),a6),f7(a6,a6),x8651)),
% 58.93/58.90 inference(scs_inference,[],[181,458,491,808,30,13])).
% 58.93/58.90 cnf(866,plain,
% 58.93/58.90 (P1(f8(a6),a4,f11(f11(a6,a1),f7(a9,a6)))),
% 58.93/58.90 inference(scs_inference,[],[833,181,318,458,491,808,30,13,9])).
% 58.93/58.90 cnf(869,plain,
% 58.93/58.90 (P2(f8(a6),f7(f8(a6),f7(x8691,a6)),x8691)),
% 58.93/58.90 inference(scs_inference,[],[833,181,142,318,579,458,491,808,710,831,30,13,9,11,12])).
% 58.93/58.90 cnf(873,plain,
% 58.93/58.90 (P2(a6,f8(a6),f7(f7(a6,a6),a6))),
% 58.93/58.90 inference(scs_inference,[],[843,833,177,181,142,318,579,307,458,521,491,808,710,761,831,30,13,9,11,12,14,10,32])).
% 58.93/58.90 cnf(876,plain,
% 58.93/58.90 (P2(f7(a6,a6),x8761,f7(x8761,a6))),
% 58.93/58.90 inference(scs_inference,[],[843,833,177,181,142,318,579,307,458,161,298,521,491,808,710,761,831,30,13,9,11,12,14,10,32,33])).
% 58.93/58.90 cnf(890,plain,
% 58.93/58.90 (P2(a6,f8(a6),f7(f7(a6,a6),f8(a6)))),
% 58.93/58.90 inference(scs_inference,[],[318,559,13])).
% 58.93/58.90 cnf(900,plain,
% 58.93/58.90 (P2(a6,x9001,f7(f8(a6),f7(x9001,a6)))),
% 58.93/58.90 inference(scs_inference,[],[142,181,318,229,302,400,579,410,298,808,710,662,559,549,191,13,9,12,14,10,32,33])).
% 58.93/58.90 cnf(910,plain,
% 58.93/58.90 (E(x9101,f7(x9101,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(911,plain,
% 58.93/58.90 (P1(f7(a1,a6),f7(a2,a6),f7(a3,a6))),
% 58.93/58.90 inference(scs_inference,[],[302,589,40,910,585,900,30,13,11])).
% 58.93/58.90 cnf(912,plain,
% 58.93/58.90 (E(x9121,f7(x9121,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(913,plain,
% 58.93/58.90 (P1(f7(a4,a6),f8(a6),f11(f7(a1,a6),f11(a9,a6)))),
% 58.93/58.90 inference(scs_inference,[],[843,302,589,40,910,912,585,900,30,13,11,9])).
% 58.93/58.90 cnf(914,plain,
% 58.93/58.90 (E(x9141,f7(x9141,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(915,plain,
% 58.93/58.90 (P1(f8(a6),f7(a4,a6),f11(f11(a6,a1),f7(a9,a6)))),
% 58.93/58.90 inference(scs_inference,[],[866,843,302,589,40,910,912,914,585,900,30,13,11,9,10])).
% 58.93/58.90 cnf(918,plain,
% 58.93/58.90 (P2(a6,f7(f8(a6),f8(a6)),f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[866,843,142,181,302,589,40,910,912,914,869,585,840,900,30,13,11,9,10,12,14])).
% 58.93/58.90 cnf(923,plain,
% 58.93/58.90 (P2(f8(a6),x9231,f7(f8(a6),f7(x9231,a6)))),
% 58.93/58.90 inference(scs_inference,[],[866,843,142,181,302,589,161,307,696,18,40,910,912,914,865,869,585,840,900,30,13,11,9,10,12,14,32,33])).
% 58.93/58.90 cnf(930,plain,
% 58.93/58.90 (P2(f11(a6,x9301),f7(a6,a6),f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[181,442,13])).
% 58.93/58.90 cnf(934,plain,
% 58.93/58.90 (P2(f7(a6,a6),a6,f7(f8(a6),f8(a6)))),
% 58.93/58.90 inference(scs_inference,[],[913,181,837,915,801,442,13,9,10,14,12])).
% 58.93/58.90 cnf(938,plain,
% 58.93/58.90 (P2(f8(a6),f7(f8(a6),f8(a6)),f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[913,181,302,458,307,876,837,915,801,442,13,9,10,14,12,32,33])).
% 58.93/58.90 cnf(943,plain,
% 58.93/58.90 (P2(f7(a6,a6),f8(a6),f7(f8(a6),f8(a6)))),
% 58.93/58.90 inference(scs_inference,[],[142,934,13])).
% 58.93/58.90 cnf(944,plain,
% 58.93/58.90 (P2(f8(a6),f7(f8(a6),f8(a6)),f7(a6,a6))),
% 58.93/58.90 inference(scs_inference,[],[142,181,938,934,13,14])).
% 58.93/58.90 cnf(960,plain,
% 58.93/58.90 (E(x9601,f7(x9601,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(962,plain,
% 58.93/58.90 (E(x9621,f7(x9621,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(965,plain,
% 58.93/58.90 (E(x9651,f7(x9651,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(966,plain,
% 58.93/58.90 (P1(a1,f7(a2,a6),a3)),
% 58.93/58.90 inference(scs_inference,[],[15,181,831,40,960,962,965,802,943,671,11,9,13,14,10])).
% 58.93/58.90 cnf(967,plain,
% 58.93/58.90 (E(x9671,f7(x9671,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(970,plain,
% 58.93/58.90 (P1(f7(a6,a6),a3,f11(f11(a6,a1),f7(a2,a6)))),
% 58.93/58.90 inference(scs_inference,[],[79,24,15,181,831,40,960,962,965,967,153,802,943,671,11,9,13,14,10,12,35])).
% 58.93/58.90 cnf(974,plain,
% 58.93/58.90 (P2(a6,f8(a6),f7(f8(a6),f7(a6,a6)))),
% 58.93/58.90 inference(scs_inference,[],[79,24,15,181,831,307,40,960,962,965,967,153,802,943,923,671,11,9,13,14,10,12,35,32])).
% 58.93/58.90 cnf(977,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(f8(a6),f8(a6)),a6)),
% 58.93/58.90 inference(scs_inference,[],[79,24,15,181,831,307,458,40,960,962,965,967,153,802,943,923,671,11,9,13,14,10,12,35,32,33])).
% 58.93/58.90 cnf(990,plain,
% 58.93/58.90 (P2(a6,f11(f7(a1,a6),f7(a9,a9)),f7(a4,a4))),
% 58.93/58.90 inference(scs_inference,[],[970,142,181,318,112,579,23,826,944,828,977,800,966,11,9,13,10,14,12,33])).
% 58.93/58.90 cnf(1001,plain,
% 58.93/58.90 (P1(a1,f7(a2,a6),f7(a3,a6))),
% 58.93/58.90 inference(scs_inference,[],[696,40,491,966,30,11])).
% 58.93/58.90 cnf(1003,plain,
% 58.93/58.90 (P2(f7(a6,a6),f8(f8(a6)),f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[142,696,40,491,966,499,30,11,14])).
% 58.93/58.90 cnf(1025,plain,
% 58.93/58.90 (E(x10251,f7(x10251,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(1026,plain,
% 58.93/58.90 (P2(f8(a3),f7(a5,a6),f8(a4))),
% 58.93/58.90 inference(scs_inference,[],[40,1025,465,341,10,13])).
% 58.93/58.90 cnf(1028,plain,
% 58.93/58.90 (P2(f7(a6,a6),f8(f8(a6)),f7(a6,a6))),
% 58.93/58.90 inference(scs_inference,[],[181,40,1025,465,1003,341,10,13,14])).
% 58.93/58.90 cnf(1029,plain,
% 58.93/58.90 (P2(f8(a6),f8(a6),f7(f7(a6,a6),a6))),
% 58.93/58.90 inference(scs_inference,[],[142,181,40,1025,465,873,1003,341,10,13,14,12])).
% 58.93/58.90 cnf(1044,plain,
% 58.93/58.90 (P2(a6,f7(f8(a6),x10441),x10441)),
% 58.93/58.90 inference(scs_inference,[],[142,181,302,400,579,974,706,918,370,13,12,14,33])).
% 58.93/58.90 cnf(1054,plain,
% 58.93/58.90 (E(x10541,f7(x10541,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(1055,plain,
% 58.93/58.90 (P2(f7(f11(a6,x10551),a6),f8(a6),f7(a6,a6))),
% 58.93/58.90 inference(scs_inference,[],[40,1054,776,1026,13,12])).
% 58.93/58.90 cnf(1071,plain,
% 58.93/58.90 (P2(f7(f11(a6,x10711),a6),f7(a6,a6),f7(a6,a6))),
% 58.93/58.90 inference(scs_inference,[],[181,1055,13])).
% 58.93/58.90 cnf(1073,plain,
% 58.93/58.90 (P2(f8(a6),f7(f8(a6),x10731),x10731)),
% 58.93/58.90 inference(scs_inference,[],[142,181,318,1044,1055,13,14,12])).
% 58.93/58.90 cnf(1074,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(a6,a6),f8(f8(a6)))),
% 58.93/58.90 inference(scs_inference,[],[142,181,318,458,298,1044,1028,1055,13,14,12,33])).
% 58.93/58.90 cnf(1083,plain,
% 58.93/58.90 (P2(f7(f11(a6,x10831),a6),f7(a6,a6),f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[181,318,1074,1071,1073,13,12,14])).
% 58.93/58.90 cnf(1084,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(a6,a6),f11(a6,x10841))),
% 58.93/58.90 inference(scs_inference,[],[181,318,161,51,1074,1071,1073,13,12,14,33])).
% 58.93/58.90 cnf(1099,plain,
% 58.93/58.90 (P2(f7(a6,a6),f8(a6),f11(a6,x10991))),
% 58.93/58.90 inference(scs_inference,[],[318,1084,13])).
% 58.93/58.90 cnf(1101,plain,
% 58.93/58.90 (P2(f8(a6),f7(a6,a6),f11(a6,x11011))),
% 58.93/58.90 inference(scs_inference,[],[181,318,1084,754,13,14,12])).
% 58.93/58.90 cnf(1102,plain,
% 58.93/58.90 (P2(f7(f8(a6),a6),f8(a6),f11(a6,x11021))),
% 58.93/58.90 inference(scs_inference,[],[181,318,757,51,1084,1083,754,13,14,12,33])).
% 58.93/58.90 cnf(1116,plain,
% 58.93/58.90 (P2(a6,f8(a6),f11(a6,x11161))),
% 58.93/58.90 inference(scs_inference,[],[318,388,1101,1102,13,12])).
% 58.93/58.90 cnf(1118,plain,
% 58.93/58.90 (P2(a6,f11(a6,x11181),f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[142,318,388,1101,1102,199,13,12,14])).
% 58.93/58.90 cnf(1119,plain,
% 58.93/58.90 (P2(f8(a6),f11(a6,x11191),f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[72,142,318,388,1101,1102,199,13,12,14,32])).
% 58.93/58.90 cnf(1139,plain,
% 58.93/58.90 (P2(a6,f7(a6,a6),f11(a6,x11391))),
% 58.93/58.90 inference(scs_inference,[],[181,1116,13])).
% 58.93/58.90 cnf(1142,plain,
% 58.93/58.90 (P2(f7(a6,a6),f11(a6,x11421),f7(a6,a6))),
% 58.93/58.90 inference(scs_inference,[],[72,181,1029,1119,1116,13,14,12,32])).
% 58.93/58.90 cnf(1144,plain,
% 58.93/58.90 (P2(f7(a6,a6),f11(a6,x11441),a6)),
% 58.93/58.90 inference(scs_inference,[],[72,181,307,458,1099,1029,1119,1116,13,14,12,32,33])).
% 58.93/58.90 cnf(1155,plain,
% 58.93/58.90 (P2(f11(a6,x11551),f8(a6),a6)),
% 58.93/58.90 inference(scs_inference,[],[142,241,13])).
% 58.93/58.90 cnf(1156,plain,
% 58.93/58.90 (P2(f8(a6),f11(a6,x11561),a6)),
% 58.93/58.90 inference(scs_inference,[],[142,318,1144,241,13,12])).
% 58.93/58.90 cnf(1157,plain,
% 58.93/58.90 (P2(f7(a6,a6),f11(a6,x11571),f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[142,318,1142,1144,241,13,12,14])).
% 58.93/58.90 cnf(1163,plain,
% 58.93/58.90 (P2(a6,f11(a6,x11631),f7(a6,a6))),
% 58.93/58.90 inference(scs_inference,[],[181,1118,1155,13,14])).
% 58.93/58.90 cnf(1164,plain,
% 58.93/58.90 (P2(f8(a6),f7(a5,a6),f7(a3,f8(a4)))),
% 58.93/58.90 inference(scs_inference,[],[142,181,740,1118,1155,13,14,12])).
% 58.93/58.90 cnf(1170,plain,
% 58.93/58.90 (P2(f11(a6,x11701),a6,f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[142,181,506,241,13,14])).
% 58.93/58.90 cnf(1171,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(a5,a6),f7(a3,f8(a4)))),
% 58.93/58.90 inference(scs_inference,[],[142,181,1164,506,241,13,14,12])).
% 58.93/58.90 cnf(1176,plain,
% 58.93/58.90 (P2(a6,f8(a6),f8(f8(a6)))),
% 58.93/58.90 inference(scs_inference,[],[142,472,13])).
% 58.93/58.90 cnf(1178,plain,
% 58.93/58.90 (P2(f8(a6),f8(a6),f7(f7(a6,a6),f8(a6)))),
% 58.93/58.90 inference(scs_inference,[],[142,181,890,1170,472,13,14,12])).
% 58.93/58.90 cnf(1179,plain,
% 58.93/58.90 (P2(a6,f7(f7(a6,a6),f8(a6)),a6)),
% 58.93/58.90 inference(scs_inference,[],[302,142,181,307,890,1170,472,13,14,12,33])).
% 58.93/58.90 cnf(1182,plain,
% 58.93/58.90 (P2(f8(a6),f7(a6,a6),f7(f7(a6,a6),f8(a6)))),
% 58.93/58.90 inference(scs_inference,[],[181,1178,13])).
% 58.93/58.90 cnf(1183,plain,
% 58.93/58.90 (P2(a6,f7(f7(a6,a6),f8(a6)),f8(a6))),
% 58.93/58.90 inference(scs_inference,[],[142,181,1178,1179,13,14])).
% 58.93/58.90 cnf(1184,plain,
% 58.93/58.90 (P2(f8(a6),f11(f7(a1,a6),f7(a9,a9)),f7(a4,a4))),
% 58.93/58.90 inference(scs_inference,[],[142,181,1178,990,1179,13,14,12])).
% 58.93/58.90 cnf(1193,plain,
% 58.93/58.90 (P2(f8(a6),f7(f7(a6,a6),f8(a6)),a6)),
% 58.93/58.90 inference(scs_inference,[],[307,181,112,1182,1184,1183,1176,13,14,12,33])).
% 58.93/58.90 cnf(1204,plain,
% 58.93/58.90 (P2(a2,f8(a6),f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[142,165,13])).
% 58.93/58.90 cnf(1213,plain,
% 58.93/58.90 (P2(a2,f7(a6,a6),f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[181,1204,13])).
% 58.93/58.90 cnf(1221,plain,
% 58.93/58.90 (P2(a3,f8(a6),f7(a5,a4))),
% 58.93/58.90 inference(scs_inference,[],[142,203,13])).
% 58.93/58.90 cnf(1228,plain,
% 58.93/58.90 (P2(a3,f7(a6,a6),f7(a5,a4))),
% 58.93/58.90 inference(scs_inference,[],[181,1221,13])).
% 58.93/58.90 cnf(1229,plain,
% 58.93/58.90 (P2(f7(f7(a2,a6),a6),f7(a6,a6),f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[181,579,1213,1221,13,12])).
% 58.93/58.90 cnf(1231,plain,
% 58.93/58.90 (P2(f8(a6),a6,f11(a6,x12311))),
% 58.93/58.90 inference(scs_inference,[],[307,181,18,579,1213,1156,1221,13,12,33])).
% 58.93/58.90 cnf(1235,plain,
% 58.93/58.90 (P2(f7(f7(a2,a6),a6),f8(a6),f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[318,1229,13])).
% 58.93/58.90 cnf(1236,plain,
% 58.93/58.90 (P2(f7(f7(a3,a6),a6),f7(a6,a6),f7(a5,a4))),
% 58.93/58.90 inference(scs_inference,[],[318,579,1229,1228,13,12])).
% 58.93/58.90 cnf(1238,plain,
% 58.93/58.90 (P2(f7(f8(a6),a6),f7(a10,a9),a2)),
% 58.93/58.90 inference(scs_inference,[],[696,757,318,579,1229,1228,13,12,33])).
% 58.93/58.90 cnf(1243,plain,
% 58.93/58.90 (P2(f7(f7(a3,a6),a6),f8(a6),f7(a5,a4))),
% 58.93/58.90 inference(scs_inference,[],[318,1236,13])).
% 58.93/58.90 cnf(1244,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(a10,a9),a2)),
% 58.93/58.90 inference(scs_inference,[],[318,454,1236,1238,13,12])).
% 58.93/58.90 cnf(1249,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(a10,a9),f7(f7(a2,a6),a6))),
% 58.93/58.90 inference(scs_inference,[],[458,400,318,454,579,1171,1236,1238,13,12,33,14])).
% 58.93/58.90 cnf(1254,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(f7(a2,a6),a6),f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[458,318,298,1249,12,33])).
% 58.93/58.90 cnf(1258,plain,
% 58.93/58.90 (P2(f8(a6),f7(f7(a2,a6),a6),f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[318,1254,12])).
% 58.93/58.90 cnf(1259,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(a5,a4),a3)),
% 58.93/58.90 inference(scs_inference,[],[410,161,318,1243,1254,12,33])).
% 58.93/58.90 cnf(1263,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(a5,a4),f7(f7(a3,a6),a6))),
% 58.93/58.90 inference(scs_inference,[],[410,161,318,579,1243,1254,12,33,14])).
% 58.93/58.90 cnf(1268,plain,
% 58.93/58.90 (P2(f7(a6,a6),a2,f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[458,318,298,1244,12,33])).
% 58.93/58.90 cnf(1273,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(f7(a3,a6),a6),f7(a5,a4))),
% 58.93/58.90 inference(scs_inference,[],[458,318,298,1263,12,33])).
% 58.93/58.90 cnf(1278,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(a5,a4),f7(a3,a6))),
% 58.93/58.90 inference(scs_inference,[],[458,400,318,1273,12,33])).
% 58.93/58.90 cnf(1282,plain,
% 58.93/58.90 (P2(f8(a6),f7(a5,a4),f7(a3,a6))),
% 58.93/58.90 inference(scs_inference,[],[318,1278,12])).
% 58.93/58.90 cnf(1283,plain,
% 58.93/58.90 (P2(f8(a6),f7(a10,a9),f7(a2,a6))),
% 58.93/58.90 inference(scs_inference,[],[307,112,318,1258,1278,12,33])).
% 58.93/58.90 cnf(1287,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(a10,a9),f7(a2,a6))),
% 58.93/58.90 inference(scs_inference,[],[181,1283,12])).
% 58.93/58.90 cnf(1288,plain,
% 58.93/58.90 (P2(f8(a6),f7(a3,a6),f7(a5,a4))),
% 58.93/58.90 inference(scs_inference,[],[307,18,181,1282,1283,12,33])).
% 58.93/58.90 cnf(1298,plain,
% 58.93/58.90 (P2(f7(a6,a6),f7(a2,a6),f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[193,458,155,43,298,181,1287,1288,12,35,33])).
% 58.93/58.90 cnf(1302,plain,
% 58.93/58.90 (P2(f8(a6),f7(a2,a6),f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[318,1298,12])).
% 58.93/58.90 cnf(1307,plain,
% 58.93/58.90 (P2(f8(a6),f7(a5,a4),a3)),
% 58.93/58.90 inference(scs_inference,[],[318,1259,12])).
% 58.93/58.90 cnf(1308,plain,
% 58.93/58.90 (P2(f7(a6,a6),a3,f7(a5,a4))),
% 58.93/58.90 inference(scs_inference,[],[458,298,318,1259,12,33])).
% 58.93/58.90 cnf(1312,plain,
% 58.93/58.90 (P2(f8(a6),a2,f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[318,1268,12])).
% 58.93/58.90 cnf(1381,plain,
% 58.93/58.90 (P2(a6,a6,f11(a6,x13811))),
% 58.93/58.90 inference(scs_inference,[],[302,298,181,761,199,12,33])).
% 58.93/58.90 cnf(1395,plain,
% 58.93/58.90 (P2(f8(a6),f7(x13951,a6),f7(f8(a6),x13951))),
% 58.93/58.90 inference(scs_inference,[],[142,706,12])).
% 58.93/58.90 cnf(1417,plain,
% 58.93/58.90 (P2(a6,f7(a10,a9),a2)),
% 58.93/58.90 inference(scs_inference,[],[410,112,181,1193,1235,12,33])).
% 58.93/58.90 cnf(1421,plain,
% 58.93/58.90 (P2(a6,f7(a10,a9),f7(f7(a2,a6),a6))),
% 58.93/58.90 inference(scs_inference,[],[410,112,181,579,1193,1235,12,33,14])).
% 58.93/58.90 cnf(1427,plain,
% 58.93/58.90 (P2(a6,f7(f7(a2,a6),a6),f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[302,298,579,165,1421,12,33])).
% 58.93/58.90 cnf(1433,plain,
% 58.93/58.90 (P2(a6,f7(a10,a9),f7(a2,a6))),
% 58.93/58.90 inference(scs_inference,[],[302,400,579,203,1427,12,33])).
% 58.93/58.90 cnf(1443,plain,
% 58.93/58.90 (P2(a6,a2,f7(a10,a9))),
% 58.93/58.90 inference(scs_inference,[],[302,298,181,1395,1417,12,33])).
% 58.93/58.90 cnf(1486,plain,
% 58.93/58.90 (E(x14861,f7(x14861,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(1487,plain,
% 58.93/58.90 (P2(a6,a6,f7(f11(a6,x14871),a6))),
% 58.93/58.90 inference(scs_inference,[],[40,1486,1381,1157,13,14])).
% 58.93/58.90 cnf(1488,plain,
% 58.93/58.90 (E(x14881,f7(x14881,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(1491,plain,
% 58.93/58.90 (P2(a6,f7(a5,a4),a3)),
% 58.93/58.90 inference(scs_inference,[],[410,112,40,1486,1488,1381,1155,1157,1243,13,14,12,33])).
% 58.93/58.90 cnf(1497,plain,
% 58.93/58.90 (E(x14971,f7(x14971,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(1498,plain,
% 58.93/58.90 (P2(f8(a6),a2,f7(f7(a10,a9),a6))),
% 58.93/58.90 inference(scs_inference,[],[40,1497,1312,1163,13,14])).
% 58.93/58.90 cnf(1499,plain,
% 58.93/58.90 (E(x14991,f7(x14991,a6))),
% 58.93/58.90 inference(rename_variables,[],[40])).
% 58.93/58.90 cnf(1502,plain,
% 58.93/58.90 (P2(a6,a3,f7(a5,a4))),
% 58.93/58.90 inference(scs_inference,[],[302,298,40,1497,1499,1170,1312,1163,1491,13,14,12,33])).
% 58.93/58.90 cnf(1533,plain,
% 58.93/58.90 (P2(a6,f8(a6),f7(f11(a6,x15331),a6))),
% 58.93/58.90 inference(scs_inference,[],[142,1487,13])).
% 58.93/58.90 cnf(1548,plain,
% 58.93/58.90 (P2(a6,f7(f7(a3,a6),a6),f7(a5,a4))),
% 58.93/58.90 inference(scs_inference,[],[579,1502,13])).
% 58.93/58.90 cnf(1557,plain,
% 58.93/58.90 (P2(a6,f7(a5,a4),f7(a3,a6))),
% 58.93/58.90 inference(scs_inference,[],[302,400,181,1548,1498,1533,13,12,33])).
% 58.93/58.90 cnf(1561,plain,
% 58.93/58.90 (P2(f8(a6),a6,f7(f11(a6,x15611),a6))),
% 58.93/58.90 inference(scs_inference,[],[142,1487,12])).
% 58.93/58.90 cnf(1576,plain,
% 58.93/58.90 (P2(a6,f7(a3,a6),f7(a5,a4))),
% 58.93/58.90 inference(scs_inference,[],[302,298,181,1557,1561,12,33])).
% 58.93/58.90 cnf(1622,plain,
% 58.93/58.90 (E(a3,f11(a1,a2))),
% 58.93/58.90 inference(scs_inference,[],[15,24,31])).
% 58.93/58.90 cnf(1623,plain,
% 58.93/58.90 (P1(x16231,x16232,f11(x16231,x16232))),
% 58.93/58.90 inference(rename_variables,[],[24])).
% 58.93/58.90 cnf(1629,plain,
% 58.93/58.90 (P1(x16291,x16292,f11(x16291,x16292))),
% 58.93/58.90 inference(rename_variables,[],[24])).
% 58.93/58.90 cnf(1636,plain,
% 58.93/58.90 (P1(x16361,x16362,f11(x16361,x16362))),
% 58.93/58.90 inference(rename_variables,[],[24])).
% 58.93/58.90 cnf(1637,plain,
% 58.93/58.90 (P2(x16371,x16372,f7(x16371,x16372))),
% 58.93/58.90 inference(rename_variables,[],[23])).
% 58.93/58.90 cnf(1643,plain,
% 58.93/58.90 (E(f11(a1,a2),a3)),
% 58.93/58.90 inference(scs_inference,[],[15,79,157,60,24,1623,1629,1636,23,1637,542,31,3,35,34,36,37,2])).
% 58.93/58.90 cnf(1935,plain,
% 58.93/58.90 (P1(x19351,f7(x19352,a6),f11(x19351,x19352))),
% 58.93/58.90 inference(rename_variables,[],[43])).
% 58.93/58.90 cnf(1937,plain,
% 58.93/58.90 (E(f7(a6,a6),f11(a6,x19371))),
% 58.93/58.90 inference(scs_inference,[],[1576,1231,45,397,966,528,551,43,26,27,28,29,2,31,30])).
% 58.93/58.90 cnf(1940,plain,
% 58.93/58.90 (~E(f7(a5,a6),f11(a1,a10))),
% 58.93/58.90 inference(scs_inference,[],[1576,1231,45,397,966,528,551,43,40,26,27,28,29,2,31,30,3])).
% 58.93/58.90 cnf(1942,plain,
% 58.93/58.90 (P2(f8(a6),f7(a5,a4),f11(a1,a2))),
% 58.93/58.90 inference(scs_inference,[],[1576,1231,45,1622,1307,397,966,528,551,43,40,26,27,28,29,2,31,30,3,14])).
% 58.93/58.90 cnf(1943,plain,
% 58.93/58.90 (P1(f11(a1,a2),f8(a6),f11(a3,a6))),
% 58.93/58.90 inference(scs_inference,[],[1576,1231,45,1622,1307,397,966,528,623,551,43,40,26,27,28,29,2,31,30,3,14,9])).
% 58.93/58.90 cnf(1944,plain,
% 58.93/58.90 (P1(x19441,f8(a6),f11(x19441,a6))),
% 58.93/58.90 inference(rename_variables,[],[623])).
% 58.93/58.90 cnf(1947,plain,
% 58.93/58.90 (~P1(a1,a10,f7(a5,a6))),
% 58.93/58.90 inference(scs_inference,[],[25,1643,1576,1231,45,1622,1307,397,521,966,528,96,623,551,43,40,26,27,28,29,2,31,30,3,14,9,12,11])).
% 58.93/58.90 cnf(1949,plain,
% 58.93/58.90 (P1(f8(a6),f11(a1,a2),f11(a6,a3))),
% 58.93/58.90 inference(scs_inference,[],[25,1643,1576,1231,45,1622,1307,397,521,966,528,96,267,623,551,43,40,26,27,28,29,2,31,30,3,14,9,12,11,10])).
% 58.93/58.90 cnf(1950,plain,
% 58.93/58.90 (P1(f8(a6),x19501,f11(a6,x19501))),
% 58.93/58.90 inference(rename_variables,[],[267])).
% 58.93/58.90 cnf(1952,plain,
% 58.93/58.90 (P2(f7(a10,a9),f8(a6),f7(a2,a6))),
% 58.93/58.90 inference(scs_inference,[],[25,1643,1576,1443,1308,1231,45,1622,1433,1307,1204,397,521,966,528,96,267,623,551,43,40,26,27,28,29,2,31,30,3,14,9,12,11,10,13,32])).
% 58.93/58.90 cnf(1956,plain,
% 58.93/58.90 (P2(f7(a3,a6),f11(a6,a2),f7(a3,a6))),
% 58.93/58.90 inference(scs_inference,[],[25,1643,1576,1302,1443,1308,1231,930,911,1001,45,1622,1298,1433,1307,1204,397,47,521,966,528,96,267,623,551,43,1935,40,26,27,28,29,2,31,30,3,14,9,12,11,10,13,32,33,37])).
% 58.93/58.90 cnf(1958,plain,
% 58.93/58.90 (P2(f7(x19581,a6),a6,x19581)),
% 58.93/58.90 inference(rename_variables,[],[47])).
% 58.93/58.90 cnf(1960,plain,
% 58.93/58.90 (P1(f8(a6),f11(a6,x19601),f11(a6,a6))),
% 58.93/58.90 inference(scs_inference,[],[25,1643,1576,1302,1443,1308,1139,1231,930,911,1001,45,1622,1298,1433,1307,1204,397,47,521,966,528,96,522,267,1950,623,551,66,43,1935,40,26,27,28,29,2,31,30,3,14,9,12,11,10,13,32,33,37,39])).
% 58.93/58.90 cnf(1962,plain,
% 58.93/58.90 (P2(f11(x19621,a6),f11(x19621,a6),f11(x19621,a6))),
% 58.93/58.90 inference(rename_variables,[],[66])).
% 58.93/58.90 cnf(1964,plain,
% 58.93/58.90 (P1(f11(a6,x19641),f8(a6),f11(a6,a6))),
% 58.93/58.90 inference(scs_inference,[],[25,1643,1576,1302,1443,1308,1139,1231,930,911,1001,45,1622,1298,1433,1307,1204,397,47,521,295,966,528,96,522,267,1950,623,1944,551,66,1962,43,1935,40,26,27,28,29,2,31,30,3,14,9,12,11,10,13,32,33,37,39,38])).
% 58.93/58.90 cnf(1970,plain,
% 58.93/58.90 (P2(f7(a3,a6),f11(a1,a6),f7(a3,a6))),
% 58.93/58.90 inference(scs_inference,[],[25,1643,1576,1302,1443,1308,1139,1231,930,911,1001,45,1622,1298,1433,1307,1204,397,47,1958,521,295,966,528,96,522,267,1950,623,1944,551,66,1962,434,24,43,1935,40,26,27,28,29,2,31,30,3,14,9,12,11,10,13,32,33,37,39,38,35,36])).
% 58.93/58.90 cnf(1978,plain,
% 58.93/58.90 (P1(a1,f8(a9),f8(a4))),
% 58.93/58.90 inference(scs_inference,[],[1956,16,26,27])).
% 58.93/58.90 cnf(1984,plain,
% 58.93/58.90 (~P2(f7(a3,a6),f8(a4),f11(a1,a10))),
% 58.93/58.90 inference(scs_inference,[],[1940,1956,619,831,16,26,27,29,28,30])).
% 58.93/58.90 cnf(1986,plain,
% 58.93/58.90 (E(f8(a6),f11(a6,x19861))),
% 58.93/58.90 inference(scs_inference,[],[1940,1956,1937,619,831,16,181,26,27,29,28,30,3])).
% 58.93/58.90 cnf(1987,plain,
% 58.93/58.90 (~P1(f7(a1,a6),a10,a5)),
% 58.93/58.90 inference(scs_inference,[],[25,1940,1956,1937,619,831,96,16,181,26,27,29,28,30,3,9])).
% 58.93/58.90 cnf(1988,plain,
% 58.93/58.90 (E(f7(x19881,a6),x19881)),
% 58.93/58.90 inference(rename_variables,[],[96])).
% 58.93/58.90 cnf(1995,plain,
% 58.93/58.90 (P1(a1,f11(a2,a6),f11(a3,a6))),
% 58.93/58.90 inference(scs_inference,[],[25,1940,1956,1937,1943,1947,619,831,589,1622,96,1988,623,16,114,24,181,26,27,29,28,30,3,9,11,10,32,35])).
% 58.93/58.90 cnf(2050,plain,
% 58.93/58.90 ($false),
% 58.93/58.90 inference(scs_inference,[],[1970,1984,1960,1964,1942,1952,1995,1986,1978,1987,545,1937,1940,1557,1142,1213,466,1949,585,103,1943,1001,96,623,434,16,43,15,26,27,28,29,30,14,9,11,13,10,32,35,33,34,36]),
% 58.93/58.90 ['proof']).
% 58.93/58.90 % SZS output end Proof
% 58.93/58.90 % Total time :58.260000s
%------------------------------------------------------------------------------