%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG037-2 : 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 : n006.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:47 EDT 2024
% Result : Unsatisfiable 59.45s 59.47s
% Output : CNFRefutation 59.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : RNG037-2 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n006.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Tue Jun 18 14:50:09 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.49/0.59 start to proof:theBenchmark
% 59.45/59.46 %-------------------------------------------
% 59.45/59.46 % File :CSE---1.7
% 59.45/59.46 % Problem :theBenchmark
% 59.45/59.46 % Transform :cnf
% 59.45/59.46 % Format :tptp:raw
% 59.45/59.46 % Command :java -jar mcs_scs.jar %d %s
% 59.45/59.46
% 59.45/59.46 % Result :Theorem 58.840000s
% 59.45/59.46 % Output :CNFRefutation 58.840000s
% 59.45/59.46 %-------------------------------------------
% 59.45/59.47 %--------------------------------------------------------------------------
% 59.45/59.47 % File : RNG037-2 : TPTP v8.2.0. Released v1.0.0.
% 59.45/59.47 % Domain : Ring Theory
% 59.45/59.47 % Problem : (X* -Y) + (X*Y) = additive_identity
% 59.45/59.47 % Version : [Wos65] axioms : Reduced > Incomplete.
% 59.45/59.47 % English :
% 59.45/59.47
% 59.45/59.47 % Refs : [Wos65] Wos (1965), Unpublished Note
% 59.45/59.47 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 59.45/59.47 % Source : [SPRFN]
% 59.45/59.47 % Names : Problem 24 [Wos65]
% 59.45/59.47 % : wos24 [WM76]
% 59.45/59.47
% 59.45/59.47 % Status : Unsatisfiable
% 59.45/59.47 % Rating : 0.09 v8.2.0, 0.14 v8.1.0, 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.11 v5.3.0, 0.20 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.14 v3.4.0, 0.20 v3.3.0, 0.00 v2.7.0, 0.12 v2.6.0, 0.14 v2.4.0, 0.14 v2.3.0, 0.14 v2.2.1, 0.22 v2.2.0, 0.11 v2.1.0, 0.14 v2.0.0
% 59.45/59.47 % Syntax : Number of clauses : 29 ( 9 unt; 0 nHn; 21 RR)
% 59.45/59.47 % Number of literals : 77 ( 0 equ; 49 neg)
% 59.45/59.47 % Maximal clause size : 5 ( 2 avg)
% 59.45/59.47 % Maximal term depth : 2 ( 1 avg)
% 59.45/59.47 % Number of predicates : 3 ( 3 usr; 0 prp; 2-3 aty)
% 59.45/59.47 % Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% 59.45/59.47 % Number of variables : 103 ( 2 sgn)
% 59.45/59.47 % SPC : CNF_UNS_RFO_NEQ_HRN
% 59.45/59.47
% 59.45/59.47 % Comments :
% 59.45/59.47 %--------------------------------------------------------------------------
% 59.45/59.47 %----Don't Include ring theory axioms
% 59.45/59.47 %include('Axioms/RNG001-0.ax').
% 59.45/59.47 %--------------------------------------------------------------------------
% 59.45/59.47 %----Equality axioms for additive operator
% 59.45/59.47 cnf(additive_inverse_substitution,axiom,
% 59.45/59.47 ( ~ equalish(X,Y)
% 59.45/59.47 | equalish(additive_inverse(X),additive_inverse(Y)) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(add_substitution1,axiom,
% 59.45/59.47 ( ~ equalish(X,Y)
% 59.45/59.47 | equalish(add(X,W),add(Y,W)) ) ).
% 59.45/59.47
% 59.45/59.47 %----This axiom omited in this version
% 59.45/59.47 %input_clause(add_substitution2,axiom,
% 59.45/59.47 % [--equalish(X,Y),
% 59.45/59.47 % ++equalish(add(W,X),add(W,Y))]).
% 59.45/59.47
% 59.45/59.47 cnf(sum_substitution1,axiom,
% 59.45/59.47 ( ~ equalish(X,Y)
% 59.45/59.47 | ~ sum(X,W,Z)
% 59.45/59.47 | sum(Y,W,Z) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(sum_substitution2,axiom,
% 59.45/59.47 ( ~ equalish(X,Y)
% 59.45/59.47 | ~ sum(W,X,Z)
% 59.45/59.47 | sum(W,Y,Z) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(sum_substitution3,axiom,
% 59.45/59.47 ( ~ equalish(X,Y)
% 59.45/59.47 | ~ sum(W,Z,X)
% 59.45/59.47 | sum(W,Z,Y) ) ).
% 59.45/59.47
% 59.45/59.47 %----Equality axioms for multiplicative operator
% 59.45/59.47 cnf(multiply_substitution1,axiom,
% 59.45/59.47 ( ~ equalish(X,Y)
% 59.45/59.47 | equalish(multiply(X,W),multiply(Y,W)) ) ).
% 59.45/59.47
% 59.45/59.47 %----This axiom omited in this version
% 59.45/59.47 %input_clause(multiply_substitution2,axiom,
% 59.45/59.47 % [--equalish(X,Y),
% 59.45/59.47 % ++equalish(multiply(W,X),multiply(W,Y))]).
% 59.45/59.47
% 59.45/59.47 cnf(product_substitution1,axiom,
% 59.45/59.47 ( ~ equalish(X,Y)
% 59.45/59.47 | ~ product(X,W,Z)
% 59.45/59.47 | product(Y,W,Z) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(product_substitution2,axiom,
% 59.45/59.47 ( ~ equalish(X,Y)
% 59.45/59.47 | ~ product(W,X,Z)
% 59.45/59.47 | product(W,Y,Z) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(product_substitution3,axiom,
% 59.45/59.47 ( ~ equalish(X,Y)
% 59.45/59.47 | ~ product(W,Z,X)
% 59.45/59.47 | product(W,Z,Y) ) ).
% 59.45/59.47
% 59.45/59.47 %----Not used in this version
% 59.45/59.47 %input_clause(additive_identity1,axiom,
% 59.45/59.47 % [++sum(additive_identity,X,X)]).
% 59.45/59.47
% 59.45/59.47 cnf(additive_identity2,axiom,
% 59.45/59.47 sum(X,additive_identity,X) ).
% 59.45/59.47
% 59.45/59.47 cnf(closure_of_multiplication,axiom,
% 59.45/59.47 product(X,Y,multiply(X,Y)) ).
% 59.45/59.47
% 59.45/59.47 cnf(closure_of_addition,axiom,
% 59.45/59.47 sum(X,Y,add(X,Y)) ).
% 59.45/59.47
% 59.45/59.47 %----Not used in this version
% 59.45/59.47 %input_clause(additive_inverse1,axiom,
% 59.45/59.47 % [++sum(additive_inverse(X),X,additive_identity)]).
% 59.45/59.47
% 59.45/59.47 cnf(additive_inverse2,axiom,
% 59.45/59.47 sum(X,additive_inverse(X),additive_identity) ).
% 59.45/59.47
% 59.45/59.47 cnf(associativity_of_addition1,axiom,
% 59.45/59.47 ( ~ sum(X,Y,U)
% 59.45/59.47 | ~ sum(Y,Z,V)
% 59.45/59.47 | ~ sum(U,Z,W)
% 59.45/59.47 | sum(X,V,W) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(associativity_of_addition2,axiom,
% 59.45/59.47 ( ~ sum(X,Y,U)
% 59.45/59.47 | ~ sum(Y,Z,V)
% 59.45/59.47 | ~ sum(X,V,W)
% 59.45/59.47 | sum(U,Z,W) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(commutativity_of_addition,axiom,
% 59.45/59.47 ( ~ sum(X,Y,Z)
% 59.45/59.47 | sum(Y,X,Z) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(associativity_of_multiplication1,axiom,
% 59.45/59.47 ( ~ product(X,Y,U)
% 59.45/59.47 | ~ product(Y,Z,V)
% 59.45/59.47 | ~ product(U,Z,W)
% 59.45/59.47 | product(X,V,W) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(associativity_of_multiplication2,axiom,
% 59.45/59.47 ( ~ product(X,Y,U)
% 59.45/59.47 | ~ product(Y,Z,V)
% 59.45/59.47 | ~ product(X,V,W)
% 59.45/59.47 | product(U,Z,W) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(distributivity1,axiom,
% 59.45/59.47 ( ~ product(X,Y,V1)
% 59.45/59.47 | ~ product(X,Z,V2)
% 59.45/59.47 | ~ sum(Y,Z,V3)
% 59.45/59.47 | ~ product(X,V3,V4)
% 59.45/59.47 | sum(V1,V2,V4) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(distributivity2,axiom,
% 59.45/59.47 ( ~ product(X,Y,V1)
% 59.45/59.47 | ~ product(X,Z,V2)
% 59.45/59.47 | ~ sum(Y,Z,V3)
% 59.45/59.47 | ~ sum(V1,V2,V4)
% 59.45/59.47 | product(X,V3,V4) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(distributivity3,axiom,
% 59.45/59.47 ( ~ product(Y,X,V1)
% 59.45/59.47 | ~ product(Z,X,V2)
% 59.45/59.47 | ~ sum(Y,Z,V3)
% 59.45/59.47 | ~ product(V3,X,V4)
% 59.45/59.47 | sum(V1,V2,V4) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(distributivity4,axiom,
% 59.45/59.47 ( ~ product(Y,X,V1)
% 59.45/59.47 | ~ product(Z,X,V2)
% 59.45/59.47 | ~ sum(Y,Z,V3)
% 59.45/59.47 | ~ sum(V1,V2,V4)
% 59.45/59.47 | product(V3,X,V4) ) ).
% 59.45/59.47
% 59.45/59.47 %----Equality axioms for operators
% 59.45/59.47 cnf(addition_is_well_defined,axiom,
% 59.45/59.47 ( ~ sum(X,Y,U)
% 59.45/59.47 | ~ sum(X,Y,V)
% 59.45/59.47 | equalish(U,V) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(multiplication_is_well_defined,axiom,
% 59.45/59.47 ( ~ product(X,Y,U)
% 59.45/59.47 | ~ product(X,Y,V)
% 59.45/59.47 | equalish(U,V) ) ).
% 59.45/59.47
% 59.45/59.47 cnf(multiplicative_identity1,axiom,
% 59.45/59.47 product(additive_identity,X,additive_identity) ).
% 59.45/59.47
% 59.45/59.47 cnf(multiplicative_identity2,axiom,
% 59.45/59.47 product(X,additive_identity,additive_identity) ).
% 59.45/59.47
% 59.45/59.47 cnf(a_times_b,hypothesis,
% 59.45/59.47 product(a,b,d) ).
% 59.45/59.47
% 59.45/59.47 cnf(a_inverse_times_b,hypothesis,
% 59.45/59.47 product(a,additive_inverse(b),c) ).
% 59.45/59.47
% 59.45/59.47 cnf(prove_sum_is_additive_identity,negated_conjecture,
% 59.45/59.47 ~ sum(c,d,additive_identity) ).
% 59.45/59.47
% 59.45/59.47 %--------------------------------------------------------------------------
% 59.45/59.47 %-------------------------------------------
% 59.45/59.47 % Proof found
% 59.45/59.47 % SZS status Theorem for theBenchmark
% 59.45/59.47 % SZS output start Proof
% 59.45/59.48 %ClaNum:29(EqnAxiom:0)
% 59.45/59.48 %VarNum:208(SingletonVarNum:103)
% 59.45/59.48 %MaxLitNum:5
% 59.45/59.48 %MaxfuncDepth:1
% 59.45/59.48 %SharedTerms:9
% 59.45/59.48 %goalClause: 9
% 59.45/59.48 %singleGoalClaCount:1
% 59.45/59.48 [1]P1(a1,a2,a6)
% 59.45/59.48 [9]~P3(a7,a6,a3)
% 59.45/59.48 [5]P1(a1,f5(a2),a7)
% 59.45/59.48 [2]P1(x21,a3,a3)
% 59.45/59.48 [3]P1(a3,x31,a3)
% 59.45/59.48 [4]P3(x41,a3,x41)
% 59.45/59.48 [6]P3(x61,f5(x61),a3)
% 59.45/59.48 [7]P3(x71,x72,f4(x71,x72))
% 59.45/59.48 [8]P1(x81,x82,f8(x81,x82))
% 59.45/59.48 [10]~P2(x101,x102)+P2(f5(x101),f5(x102))
% 59.45/59.48 [13]~P3(x132,x131,x133)+P3(x131,x132,x133)
% 59.45/59.48 [11]~P2(x111,x113)+P2(f4(x111,x112),f4(x113,x112))
% 59.45/59.48 [12]~P2(x121,x123)+P2(f8(x121,x122),f8(x123,x122))
% 59.45/59.48 [14]~P3(x141,x142,x144)+P3(x141,x142,x143)+~P2(x144,x143)
% 59.45/59.48 [15]~P3(x151,x154,x153)+P3(x151,x152,x153)+~P2(x154,x152)
% 59.45/59.48 [16]~P3(x164,x162,x163)+P3(x161,x162,x163)+~P2(x164,x161)
% 59.45/59.48 [17]~P1(x171,x172,x174)+P1(x171,x172,x173)+~P2(x174,x173)
% 59.45/59.48 [18]~P1(x181,x184,x183)+P1(x181,x182,x183)+~P2(x184,x182)
% 59.45/59.48 [19]~P1(x194,x192,x193)+P1(x191,x192,x193)+~P2(x194,x191)
% 59.45/59.48 [20]~P3(x203,x204,x201)+P2(x201,x202)+~P3(x203,x204,x202)
% 59.45/59.48 [21]~P1(x213,x214,x211)+P2(x211,x212)+~P1(x213,x214,x212)
% 59.45/59.48 [22]~P3(x226,x224,x221)+P3(x221,x222,x223)+~P3(x224,x222,x225)+~P3(x226,x225,x223)
% 59.45/59.48 [23]~P3(x231,x236,x234)+P3(x231,x232,x233)+~P3(x234,x235,x233)+~P3(x236,x235,x232)
% 59.45/59.48 [24]~P1(x246,x244,x241)+P1(x241,x242,x243)+~P1(x244,x242,x245)+~P1(x246,x245,x243)
% 59.45/59.48 [25]~P1(x251,x256,x254)+P1(x251,x252,x253)+~P1(x254,x255,x253)+~P1(x256,x255,x252)
% 59.45/59.48 [26]~P1(x267,x265,x262)+~P1(x267,x264,x261)+P3(x261,x262,x263)+~P3(x264,x265,x266)+~P1(x267,x266,x263)
% 59.45/59.48 [27]~P1(x275,x277,x272)+~P1(x274,x277,x271)+P3(x271,x272,x273)+~P3(x274,x275,x276)+~P1(x276,x277,x273)
% 59.45/59.48 [28]~P1(x287,x282,x285)+~P1(x286,x282,x284)+P1(x281,x282,x283)+~P3(x284,x285,x283)+~P3(x286,x287,x281)
% 59.45/59.48 [29]~P1(x291,x297,x295)+~P1(x291,x296,x294)+P1(x291,x292,x293)+~P3(x294,x295,x293)+~P3(x296,x297,x292)
% 59.45/59.48 %EqnAxiom
% 59.45/59.48
% 59.45/59.48 %-------------------------------------------
% 59.45/59.49 cnf(30,plain,
% 59.45/59.49 (~P3(a6,a7,a3)),
% 59.45/59.49 inference(scs_inference,[],[9,13])).
% 59.45/59.49 cnf(34,plain,
% 59.45/59.49 (P2(f8(x341,a3),a3)),
% 59.45/59.49 inference(scs_inference,[],[9,4,8,2,13,20,21])).
% 59.45/59.49 cnf(35,plain,
% 59.45/59.49 (P1(x351,a3,a3)),
% 59.45/59.49 inference(rename_variables,[],[2])).
% 59.45/59.49 cnf(36,plain,
% 59.45/59.49 (P1(x361,x362,f8(x361,x362))),
% 59.45/59.49 inference(rename_variables,[],[8])).
% 59.45/59.49 cnf(38,plain,
% 59.45/59.49 (~P3(a3,a6,f5(a7))),
% 59.45/59.49 inference(scs_inference,[],[9,4,8,2,6,13,20,21,22])).
% 59.45/59.49 cnf(40,plain,
% 59.45/59.49 (P3(x401,a3,x401)),
% 59.45/59.49 inference(rename_variables,[],[4])).
% 59.45/59.49 cnf(42,plain,
% 59.45/59.49 (P3(x421,f4(a3,a3),x421)),
% 59.45/59.49 inference(scs_inference,[],[9,4,40,7,8,2,6,13,20,21,22,23])).
% 59.45/59.49 cnf(43,plain,
% 59.45/59.49 (P3(x431,x432,f4(x431,x432))),
% 59.45/59.49 inference(rename_variables,[],[7])).
% 59.45/59.49 cnf(45,plain,
% 59.45/59.49 (P1(f8(x451,a3),a3,f8(x451,a3))),
% 59.45/59.49 inference(scs_inference,[],[9,4,40,7,8,36,2,35,6,13,20,21,22,23,24])).
% 59.45/59.49 cnf(46,plain,
% 59.45/59.49 (P1(x461,x462,f8(x461,x462))),
% 59.45/59.49 inference(rename_variables,[],[8])).
% 59.45/59.49 cnf(47,plain,
% 59.45/59.49 (P1(x471,x472,f8(x471,x472))),
% 59.45/59.49 inference(rename_variables,[],[8])).
% 59.45/59.49 cnf(52,plain,
% 59.45/59.49 (P1(x521,x522,f8(x521,x522))),
% 59.45/59.49 inference(rename_variables,[],[8])).
% 59.45/59.49 cnf(55,plain,
% 59.45/59.49 (P3(f8(x551,a3),f8(x551,a3),f8(x551,a3))),
% 59.45/59.49 inference(scs_inference,[],[9,4,40,7,8,36,47,52,46,2,35,6,13,20,21,22,23,24,25,26])).
% 59.45/59.49 cnf(58,plain,
% 59.45/59.49 (P1(x581,x582,f8(x581,x582))),
% 59.45/59.49 inference(rename_variables,[],[8])).
% 59.45/59.49 cnf(59,plain,
% 59.45/59.49 (P3(x591,a3,x591)),
% 59.45/59.49 inference(rename_variables,[],[4])).
% 59.45/59.49 cnf(64,plain,
% 59.45/59.49 (P1(x641,x642,f8(x641,x642))),
% 59.45/59.49 inference(rename_variables,[],[8])).
% 59.45/59.49 cnf(65,plain,
% 59.45/59.49 (P3(x651,a3,x651)),
% 59.45/59.49 inference(rename_variables,[],[4])).
% 59.45/59.49 cnf(67,plain,
% 59.45/59.49 (P1(a3,x671,f4(f8(a3,x671),f8(a3,x671)))),
% 59.45/59.49 inference(scs_inference,[],[9,4,40,59,65,7,43,8,36,47,52,58,64,46,2,35,6,13,20,21,22,23,24,25,26,27,28])).
% 59.45/59.49 cnf(68,plain,
% 59.45/59.49 (P3(x681,x682,f4(x681,x682))),
% 59.45/59.49 inference(rename_variables,[],[7])).
% 59.45/59.49 cnf(69,plain,
% 59.45/59.49 (P3(x691,a3,x691)),
% 59.45/59.49 inference(rename_variables,[],[4])).
% 59.45/59.49 cnf(71,plain,
% 59.45/59.49 (P1(x711,x712,f8(x711,x712))),
% 59.45/59.49 inference(rename_variables,[],[8])).
% 59.45/59.49 cnf(73,plain,
% 59.45/59.49 (P1(x731,a3,f4(f8(x731,a3),f8(x731,a3)))),
% 59.45/59.49 inference(scs_inference,[],[9,4,40,59,65,69,7,43,68,8,36,47,52,58,64,71,46,2,35,6,13,20,21,22,23,24,25,26,27,28,29])).
% 59.45/59.49 cnf(74,plain,
% 59.45/59.49 (P3(x741,x742,f4(x741,x742))),
% 59.45/59.49 inference(rename_variables,[],[7])).
% 59.45/59.49 cnf(75,plain,
% 59.45/59.49 (P3(x751,a3,x751)),
% 59.45/59.49 inference(rename_variables,[],[4])).
% 59.45/59.49 cnf(77,plain,
% 59.45/59.49 (P1(x771,x772,f8(x771,x772))),
% 59.45/59.49 inference(rename_variables,[],[8])).
% 59.45/59.49 cnf(79,plain,
% 59.45/59.49 (P3(f8(x791,a3),a3,a3)),
% 59.45/59.49 inference(scs_inference,[],[9,4,40,59,65,69,75,7,43,68,8,36,47,52,58,64,71,46,2,35,6,13,20,21,22,23,24,25,26,27,28,29,14])).
% 59.45/59.49 cnf(80,plain,
% 59.45/59.49 (P3(x801,a3,x801)),
% 59.45/59.49 inference(rename_variables,[],[4])).
% 59.45/59.49 cnf(82,plain,
% 59.45/59.49 (P3(x821,a3,f4(x821,f8(x822,a3)))),
% 59.45/59.49 inference(scs_inference,[],[9,4,40,59,65,69,75,7,43,68,74,8,36,47,52,58,64,71,46,2,35,6,13,20,21,22,23,24,25,26,27,28,29,14,15])).
% 59.45/59.49 cnf(85,plain,
% 59.45/59.49 (P3(a3,a3,f8(x851,a3))),
% 59.45/59.49 inference(scs_inference,[],[9,4,40,59,65,69,75,80,7,43,68,74,8,36,47,52,58,64,71,46,2,35,6,13,20,21,22,23,24,25,26,27,28,29,14,15,16])).
% 59.45/59.49 cnf(88,plain,
% 59.45/59.49 (P1(x881,a3,f8(x881,f8(x882,a3)))),
% 59.45/59.49 inference(scs_inference,[],[9,4,40,59,65,69,75,80,7,43,68,74,8,36,47,52,58,64,71,77,46,2,35,6,13,20,21,22,23,24,25,26,27,28,29,14,15,16,18])).
% 59.45/59.49 cnf(89,plain,
% 59.45/59.49 (P1(x891,x892,f8(x891,x892))),
% 59.45/59.49 inference(rename_variables,[],[8])).
% 59.45/59.49 cnf(91,plain,
% 59.45/59.49 (P1(a3,x911,f8(f8(x912,a3),x911))),
% 59.45/59.49 inference(scs_inference,[],[9,4,40,59,65,69,75,80,7,43,68,74,8,36,47,52,58,64,71,77,89,46,2,35,6,13,20,21,22,23,24,25,26,27,28,29,14,15,16,18,19])).
% 59.45/59.49 cnf(94,plain,
% 59.45/59.49 (~P3(a6,a3,f5(a7))),
% 59.45/59.49 inference(scs_inference,[],[38,13])).
% 59.45/59.49 cnf(96,plain,
% 59.45/59.49 (P2(x961,f4(x961,f4(a3,a3)))),
% 59.45/59.49 inference(scs_inference,[],[42,38,7,13,20])).
% 59.45/59.49 cnf(99,plain,
% 59.45/59.49 (P2(f8(x991,f8(x992,a3)),a3)),
% 59.45/59.49 inference(scs_inference,[],[42,38,88,7,2,13,20,21])).
% 59.45/59.49 cnf(102,plain,
% 59.45/59.49 (P3(f8(x1021,a3),f4(a3,a3),a3)),
% 59.45/59.49 inference(scs_inference,[],[42,38,88,34,7,2,13,20,21,14])).
% 59.45/59.49 cnf(103,plain,
% 59.45/59.49 (P3(x1031,f4(a3,a3),x1031)),
% 59.45/59.49 inference(rename_variables,[],[42])).
% 59.45/59.49 cnf(105,plain,
% 59.45/59.49 (P3(a3,f4(a3,a3),f8(x1051,a3))),
% 59.45/59.49 inference(scs_inference,[],[42,103,38,88,34,7,2,13,20,21,14,16])).
% 59.45/59.49 cnf(106,plain,
% 59.45/59.49 (P3(x1061,f4(a3,a3),x1061)),
% 59.45/59.49 inference(rename_variables,[],[42])).
% 59.45/59.49 cnf(108,plain,
% 59.45/59.49 (P3(f8(x1081,a3),f4(f8(x1081,a3),f4(a3,a3)),f8(x1081,a3))),
% 59.45/59.49 inference(scs_inference,[],[42,103,38,55,88,34,7,2,13,20,21,14,16,15])).
% 59.45/59.49 cnf(110,plain,
% 59.45/59.49 (P1(f8(x1101,a3),x1102,f8(x1101,a3))),
% 59.45/59.49 inference(scs_inference,[],[42,103,38,55,88,45,34,3,7,2,13,20,21,14,16,15,24])).
% 59.45/59.49 cnf(112,plain,
% 59.45/59.49 (P3(a3,f8(x1121,a3),f4(f8(x1121,a3),f8(x1122,a3)))),
% 59.45/59.49 inference(scs_inference,[],[42,103,82,85,38,55,88,45,34,3,7,2,13,20,21,14,16,15,24,23])).
% 59.45/59.49 cnf(115,plain,
% 59.45/59.49 (~P3(f4(a3,a3),a6,f5(a7))),
% 59.45/59.49 inference(scs_inference,[],[9,42,103,106,82,85,38,55,88,45,34,3,7,2,6,13,20,21,14,16,15,24,23,22])).
% 59.45/59.49 cnf(132,plain,
% 59.45/59.49 (~P3(a6,f4(a3,a3),f5(a7))),
% 59.45/59.49 inference(scs_inference,[],[115,13])).
% 59.45/59.49 cnf(134,plain,
% 59.45/59.49 (P1(f4(f8(x1341,a3),f4(a3,a3)),x1342,f8(x1341,a3))),
% 59.45/59.49 inference(scs_inference,[],[115,96,110,13,19])).
% 59.45/59.49 cnf(135,plain,
% 59.45/59.49 (P2(x1351,f4(x1351,f4(a3,a3)))),
% 59.45/59.49 inference(rename_variables,[],[96])).
% 59.45/59.49 cnf(137,plain,
% 59.45/59.49 (P1(f8(x1371,a3),x1372,f4(f8(x1371,a3),f4(a3,a3)))),
% 59.45/59.49 inference(scs_inference,[],[115,96,135,110,13,19,17])).
% 59.45/59.49 cnf(138,plain,
% 59.45/59.49 (P2(x1381,f4(x1381,f4(a3,a3)))),
% 59.45/59.49 inference(rename_variables,[],[96])).
% 59.45/59.49 cnf(140,plain,
% 59.45/59.49 (P2(f8(x1401,a3),f4(a3,f8(x1402,a3)))),
% 59.45/59.49 inference(scs_inference,[],[85,115,82,96,135,110,13,19,17,20])).
% 59.45/59.49 cnf(141,plain,
% 59.45/59.49 (P3(x1411,a3,f4(x1411,f8(x1412,a3)))),
% 59.45/59.49 inference(rename_variables,[],[82])).
% 59.45/59.49 cnf(143,plain,
% 59.45/59.49 (P2(f8(x1431,a3),f8(f8(x1431,a3),x1432))),
% 59.45/59.49 inference(scs_inference,[],[85,115,82,96,135,110,8,13,19,17,20,21])).
% 59.45/59.49 cnf(144,plain,
% 59.45/59.49 (P1(x1441,x1442,f8(x1441,x1442))),
% 59.45/59.49 inference(rename_variables,[],[8])).
% 59.45/59.50 cnf(146,plain,
% 59.45/59.50 (P3(f4(a3,f4(a3,a3)),a3,f8(x1461,a3))),
% 59.45/59.50 inference(scs_inference,[],[85,115,82,96,135,138,110,8,13,19,17,20,21,16])).
% 59.45/59.50 cnf(147,plain,
% 59.45/59.50 (P2(x1471,f4(x1471,f4(a3,a3)))),
% 59.45/59.50 inference(rename_variables,[],[96])).
% 59.45/59.50 cnf(149,plain,
% 59.45/59.50 (P3(a3,a3,f4(f8(x1491,a3),f4(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[85,115,82,96,135,138,147,110,8,13,19,17,20,21,16,14])).
% 59.45/59.50 cnf(150,plain,
% 59.45/59.50 (P2(x1501,f4(x1501,f4(a3,a3)))),
% 59.45/59.50 inference(rename_variables,[],[96])).
% 59.45/59.50 cnf(156,plain,
% 59.45/59.50 (P1(f8(x1561,a3),x1562,f8(x1561,a3))),
% 59.45/59.50 inference(rename_variables,[],[110])).
% 59.45/59.50 cnf(157,plain,
% 59.45/59.50 (P1(x1571,x1572,f8(x1571,x1572))),
% 59.45/59.50 inference(rename_variables,[],[8])).
% 59.45/59.50 cnf(159,plain,
% 59.45/59.50 (P1(f8(f8(x1591,a3),f8(x1592,a3)),x1593,a3)),
% 59.45/59.50 inference(scs_inference,[],[85,115,82,96,135,138,147,150,110,156,91,1,8,144,3,13,19,17,20,21,16,14,15,25,24])).
% 59.45/59.50 cnf(161,plain,
% 59.45/59.50 (P1(a3,x1611,f8(f8(x1612,a3),x1611))),
% 59.45/59.50 inference(rename_variables,[],[91])).
% 59.45/59.50 cnf(163,plain,
% 59.45/59.50 (P3(f8(x1631,a3),f4(a3,a3),f4(a3,f8(x1632,a3)))),
% 59.45/59.50 inference(scs_inference,[],[85,115,82,141,42,96,135,138,147,150,110,156,91,1,8,144,3,13,19,17,20,21,16,14,15,25,24,22])).
% 59.45/59.50 cnf(167,plain,
% 59.45/59.50 (P3(a3,f8(x1671,a3),a3)),
% 59.45/59.50 inference(scs_inference,[],[85,115,79,82,141,42,96,135,138,147,150,110,156,91,1,8,144,3,13,19,17,20,21,16,14,15,25,24,22,23])).
% 59.45/59.50 cnf(168,plain,
% 59.45/59.50 (P3(a3,a3,f8(x1681,a3))),
% 59.45/59.50 inference(rename_variables,[],[85])).
% 59.45/59.50 cnf(170,plain,
% 59.45/59.50 (P1(x1701,f8(x1702,a3),f8(x1702,a3))),
% 59.45/59.50 inference(scs_inference,[],[85,168,115,79,82,141,42,96,135,138,147,150,110,156,91,1,8,144,2,3,13,19,17,20,21,16,14,15,25,24,22,23,29])).
% 59.45/59.50 cnf(177,plain,
% 59.45/59.50 (P1(f8(x1771,a3),a3,f8(f8(x1772,a3),a3))),
% 59.45/59.50 inference(scs_inference,[],[85,168,115,79,82,141,42,55,96,135,138,147,150,110,156,91,161,1,8,144,157,2,3,4,13,19,17,20,21,16,14,15,25,24,22,23,29,27,28])).
% 59.45/59.50 cnf(184,plain,
% 59.45/59.50 (P1(a3,x1841,f4(f8(x1842,a3),f4(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[34,137,19])).
% 59.45/59.50 cnf(185,plain,
% 59.45/59.50 (P2(f8(x1851,a3),a3)),
% 59.45/59.50 inference(rename_variables,[],[34])).
% 59.45/59.50 cnf(187,plain,
% 59.45/59.50 (P1(f4(f8(x1871,a3),f4(a3,a3)),x1872,a3)),
% 59.45/59.50 inference(scs_inference,[],[34,185,134,137,19,17])).
% 59.45/59.50 cnf(188,plain,
% 59.45/59.50 (P2(f8(x1881,a3),a3)),
% 59.45/59.50 inference(rename_variables,[],[34])).
% 59.45/59.50 cnf(190,plain,
% 59.45/59.50 (P2(f4(a3,f8(x1901,a3)),f8(x1902,a3))),
% 59.45/59.50 inference(scs_inference,[],[163,42,34,185,134,137,19,17,20])).
% 59.45/59.50 cnf(191,plain,
% 59.45/59.50 (P3(x1911,f4(a3,a3),x1911)),
% 59.45/59.50 inference(rename_variables,[],[42])).
% 59.45/59.50 cnf(196,plain,
% 59.45/59.50 (P2(f8(x1961,a3),f8(x1962,a3))),
% 59.45/59.50 inference(scs_inference,[],[163,42,191,99,34,185,134,137,170,19,17,20,14,21])).
% 59.45/59.50 cnf(197,plain,
% 59.45/59.50 (P1(x1971,f8(x1972,a3),f8(x1972,a3))),
% 59.45/59.50 inference(rename_variables,[],[170])).
% 59.45/59.50 cnf(198,plain,
% 59.45/59.50 (P1(f4(f8(x1981,a3),f4(a3,a3)),x1982,f8(x1981,a3))),
% 59.45/59.50 inference(rename_variables,[],[134])).
% 59.45/59.50 cnf(200,plain,
% 59.45/59.50 (P3(a3,f4(f8(x2001,a3),f4(a3,a3)),f8(x2001,a3))),
% 59.45/59.50 inference(scs_inference,[],[108,163,42,191,99,34,185,188,134,137,170,19,17,20,14,21,16])).
% 59.45/59.50 cnf(201,plain,
% 59.45/59.50 (P2(f8(x2011,a3),a3)),
% 59.45/59.50 inference(rename_variables,[],[34])).
% 59.45/59.50 cnf(206,plain,
% 59.45/59.50 (P1(f8(x2061,a3),x2062,a3)),
% 59.45/59.50 inference(scs_inference,[],[108,163,112,42,191,99,34,185,188,201,134,137,170,197,159,19,17,20,14,21,16,15,24])).
% 59.45/59.50 cnf(207,plain,
% 59.45/59.50 (P1(f8(f8(x2071,a3),f8(x2072,a3)),x2073,a3)),
% 59.45/59.50 inference(rename_variables,[],[159])).
% 59.45/59.50 cnf(208,plain,
% 59.45/59.50 (P1(x2081,f8(x2082,a3),f8(x2082,a3))),
% 59.45/59.50 inference(rename_variables,[],[170])).
% 59.45/59.50 cnf(210,plain,
% 59.45/59.50 (P3(f8(x2101,a3),f8(x2102,a3),f8(x2101,a3))),
% 59.45/59.50 inference(scs_inference,[],[85,108,163,112,167,42,191,99,34,185,188,201,134,137,170,197,159,19,17,20,14,21,16,15,24,22])).
% 59.45/59.50 cnf(212,plain,
% 59.45/59.50 (P3(a3,f4(f8(x2121,a3),f8(x2122,a3)),f8(x2121,a3))),
% 59.45/59.50 inference(scs_inference,[],[85,108,163,112,167,42,191,99,34,185,188,201,55,134,137,170,197,159,19,17,20,14,21,16,15,24,22,23])).
% 59.45/59.50 cnf(214,plain,
% 59.45/59.50 (P3(a3,a3,f8(x2141,a3))),
% 59.45/59.50 inference(rename_variables,[],[85])).
% 59.45/59.50 cnf(219,plain,
% 59.45/59.50 (P1(x2191,f8(x2192,a3),f8(x2192,a3))),
% 59.45/59.50 inference(rename_variables,[],[170])).
% 59.45/59.50 cnf(222,plain,
% 59.45/59.50 (P1(x2221,f8(x2222,a3),f8(x2222,a3))),
% 59.45/59.50 inference(rename_variables,[],[170])).
% 59.45/59.50 cnf(227,plain,
% 59.45/59.50 (P1(f8(x2271,a3),f8(x2272,a3),f4(f8(x2272,a3),f8(x2273,a3)))),
% 59.45/59.50 inference(scs_inference,[],[85,214,108,163,112,167,82,42,191,99,34,185,188,201,55,134,198,137,170,197,208,219,222,159,207,7,3,19,17,20,14,21,16,15,24,22,23,26,27,28])).
% 59.45/59.50 cnf(233,plain,
% 59.45/59.50 (P2(f8(x2331,a3),a3)),
% 59.45/59.50 inference(rename_variables,[],[34])).
% 59.45/59.50 cnf(235,plain,
% 59.45/59.50 (P1(f8(x2351,a3),a3,f8(x2352,a3))),
% 59.45/59.50 inference(scs_inference,[],[34,227,196,177,19,17])).
% 59.45/59.50 cnf(241,plain,
% 59.45/59.50 (P2(a3,f8(x2411,a3))),
% 59.45/59.50 inference(scs_inference,[],[102,42,34,233,227,196,177,19,17,18,20])).
% 59.45/59.50 cnf(244,plain,
% 59.45/59.50 (P2(f4(f8(x2441,a3),f8(x2442,a3)),a3)),
% 59.45/59.50 inference(scs_inference,[],[102,42,34,233,227,196,206,177,19,17,18,20,21])).
% 59.45/59.50 cnf(245,plain,
% 59.45/59.50 (P1(f8(x2451,a3),x2452,a3)),
% 59.45/59.50 inference(rename_variables,[],[206])).
% 59.45/59.50 cnf(248,plain,
% 59.45/59.50 (P2(f8(x2481,a3),f8(f8(x2481,a3),x2482))),
% 59.45/59.50 inference(rename_variables,[],[143])).
% 59.45/59.50 cnf(251,plain,
% 59.45/59.50 (P2(f8(x2511,a3),f8(f8(x2511,a3),x2512))),
% 59.45/59.50 inference(rename_variables,[],[143])).
% 59.45/59.50 cnf(253,plain,
% 59.45/59.50 (P3(f8(x2531,a3),f8(f8(x2532,a3),x2533),f8(x2531,a3))),
% 59.45/59.50 inference(scs_inference,[],[102,105,210,42,34,233,143,248,251,227,196,206,177,19,17,18,20,21,14,16,15])).
% 59.45/59.50 cnf(256,plain,
% 59.45/59.50 (P1(a3,f4(f8(x2561,a3),f8(x2562,a3)),f8(x2561,a3))),
% 59.45/59.50 inference(scs_inference,[],[102,105,210,42,34,233,143,248,251,227,196,67,206,177,170,19,17,18,20,21,14,16,15,25])).
% 59.45/59.50 cnf(258,plain,
% 59.45/59.50 (P1(x2581,f8(x2582,a3),f8(x2582,a3))),
% 59.45/59.50 inference(rename_variables,[],[170])).
% 59.45/59.50 cnf(260,plain,
% 59.45/59.50 (P1(f4(f8(x2601,a3),f8(x2602,a3)),f8(x2601,a3),a3)),
% 59.45/59.50 inference(scs_inference,[],[102,105,210,42,34,233,143,248,251,227,196,67,206,245,177,170,19,17,18,20,21,14,16,15,25,24])).
% 59.45/59.50 cnf(263,plain,
% 59.45/59.50 (P1(f8(x2631,a3),f8(x2632,a3),f4(f8(x2632,a3),f8(x2633,a3)))),
% 59.45/59.50 inference(rename_variables,[],[227])).
% 59.45/59.50 cnf(266,plain,
% 59.45/59.50 (P3(x2661,a3,x2661)),
% 59.45/59.50 inference(rename_variables,[],[4])).
% 59.45/59.50 cnf(277,plain,
% 59.45/59.50 (P1(x2771,f8(x2772,a3),f8(x2772,a3))),
% 59.45/59.50 inference(rename_variables,[],[170])).
% 59.45/59.50 cnf(279,plain,
% 59.45/59.50 (P3(f8(x2791,a3),f4(f8(x2792,a3),f8(x2793,a3)),f8(x2791,a3))),
% 59.45/59.50 inference(scs_inference,[],[102,105,85,210,200,108,42,34,233,143,248,251,227,263,196,67,187,206,245,177,170,258,277,6,4,266,19,17,18,20,21,14,16,15,25,24,22,23,29,26])).
% 59.45/59.50 cnf(288,plain,
% 59.45/59.50 (P1(f4(f8(x2881,a3),f8(x2882,a3)),f8(x2881,a3),f8(x2883,a3))),
% 59.45/59.50 inference(scs_inference,[],[260,241,17])).
% 59.45/59.50 cnf(290,plain,
% 59.45/59.50 (P1(x2901,f8(x2902,a3),f4(f8(x2901,a3),f8(x2901,a3)))),
% 59.45/59.50 inference(scs_inference,[],[73,260,241,17,18])).
% 59.45/59.50 cnf(293,plain,
% 59.45/59.50 (P2(f8(x2931,a3),f4(a3,f8(x2932,a3)))),
% 59.45/59.50 inference(rename_variables,[],[140])).
% 59.45/59.50 cnf(295,plain,
% 59.45/59.50 (P2(f8(x2951,a3),f4(a3,f4(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[105,102,140,73,260,241,7,17,18,16,20])).
% 59.45/59.50 cnf(298,plain,
% 59.45/59.50 (P3(f8(x2981,a3),f4(a3,a3),f8(x2982,a3))),
% 59.45/59.50 inference(scs_inference,[],[105,102,163,190,140,73,260,241,7,17,18,16,20,14])).
% 59.45/59.50 cnf(301,plain,
% 59.45/59.50 (P2(f4(f8(x3011,a3),f4(a3,a3)),f8(x3012,a3))),
% 59.45/59.50 inference(scs_inference,[],[105,102,163,190,140,73,184,260,241,170,7,17,18,16,20,14,21])).
% 59.45/59.50 cnf(303,plain,
% 59.45/59.50 (P1(a3,x3031,f4(f8(x3032,a3),f4(a3,a3)))),
% 59.45/59.50 inference(rename_variables,[],[184])).
% 59.45/59.50 cnf(307,plain,
% 59.45/59.50 (P3(f8(x3071,a3),f8(f8(x3072,a3),x3073),f8(x3071,a3))),
% 59.45/59.50 inference(rename_variables,[],[253])).
% 59.45/59.50 cnf(309,plain,
% 59.45/59.50 (P1(x3091,f4(f8(x3092,a3),f4(a3,a3)),a3)),
% 59.45/59.50 inference(scs_inference,[],[105,102,253,163,190,140,293,73,184,303,260,241,170,7,17,18,16,20,14,21,15,25])).
% 59.45/59.50 cnf(310,plain,
% 59.45/59.50 (P1(a3,x3101,f4(f8(x3102,a3),f4(a3,a3)))),
% 59.45/59.50 inference(rename_variables,[],[184])).
% 59.45/59.50 cnf(311,plain,
% 59.45/59.50 (P1(x3111,a3,f4(f8(x3111,a3),f8(x3111,a3)))),
% 59.45/59.50 inference(rename_variables,[],[73])).
% 59.45/59.50 cnf(317,plain,
% 59.45/59.50 (P1(f4(f8(x3171,a3),f8(x3171,a3)),x3172,a3)),
% 59.45/59.50 inference(scs_inference,[],[105,102,253,307,163,167,190,140,293,73,311,184,303,310,260,241,170,7,17,18,16,20,14,21,15,25,22,24])).
% 59.45/59.50 cnf(319,plain,
% 59.45/59.50 (P3(a3,f8(x3191,a3),f8(x3192,a3))),
% 59.45/59.50 inference(scs_inference,[],[105,102,85,253,307,212,163,167,279,190,140,293,73,311,184,303,310,260,241,170,7,17,18,16,20,14,21,15,25,22,24,23])).
% 59.45/59.50 cnf(329,plain,
% 59.45/59.50 (P1(f4(f8(x3291,a3),f8(x3291,a3)),x3292,f8(x3293,a3))),
% 59.45/59.50 inference(scs_inference,[],[256,241,317,19,17])).
% 59.45/59.50 cnf(333,plain,
% 59.45/59.50 (P3(a3,f4(a3,a3),f8(x3331,f8(x3332,a3)))),
% 59.45/59.50 inference(scs_inference,[],[42,256,235,99,241,317,19,17,18,16])).
% 59.45/59.50 cnf(334,plain,
% 59.45/59.50 (P3(x3341,f4(a3,a3),x3341)),
% 59.45/59.50 inference(rename_variables,[],[42])).
% 59.45/59.50 cnf(336,plain,
% 59.45/59.50 (P2(f8(x3361,a3),f8(f8(x3362,a3),f8(x3363,a3)))),
% 59.45/59.50 inference(scs_inference,[],[42,256,235,99,241,317,88,19,17,18,16,21])).
% 59.45/59.50 cnf(339,plain,
% 59.45/59.50 (P3(f4(f8(x3391,a3),f4(a3,a3)),f4(a3,a3),f8(x3392,a3))),
% 59.45/59.50 inference(scs_inference,[],[42,334,256,235,99,241,301,317,88,19,17,18,16,21,14])).
% 59.45/59.50 cnf(342,plain,
% 59.45/59.50 (P3(f8(x3421,a3),f4(a3,f4(a3,a3)),f8(x3421,a3))),
% 59.45/59.50 inference(scs_inference,[],[210,42,334,256,235,99,241,295,301,317,88,19,17,18,16,21,14,15])).
% 59.45/59.50 cnf(345,plain,
% 59.45/59.50 (P1(x3451,f8(x3452,a3),a3)),
% 59.45/59.50 inference(scs_inference,[],[210,42,334,256,235,99,241,290,295,301,317,88,19,17,18,16,21,14,15,25])).
% 59.45/59.50 cnf(347,plain,
% 59.45/59.50 (P1(x3471,f8(x3472,a3),f4(f8(x3471,a3),f8(x3471,a3)))),
% 59.45/59.50 inference(rename_variables,[],[290])).
% 59.45/59.50 cnf(352,plain,
% 59.45/59.50 (P1(a3,f4(f8(x3521,a3),f8(x3522,a3)),f8(x3521,a3))),
% 59.45/59.50 inference(rename_variables,[],[256])).
% 59.45/59.50 cnf(362,plain,
% 59.45/59.50 (P3(f8(x3621,a3),f8(x3621,a3),f4(f8(x3622,a3),f4(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[105,210,42,334,298,256,352,235,99,241,4,290,347,295,288,301,317,88,184,6,7,19,17,18,16,21,14,15,25,24,22,23,26])).
% 59.45/59.50 cnf(373,plain,
% 59.45/59.50 (P1(a3,a3,f8(x3731,a3))),
% 59.45/59.50 inference(scs_inference,[],[235,34,19])).
% 59.45/59.50 cnf(376,plain,
% 59.45/59.50 (P1(x3761,f4(f8(x3762,a3),f4(a3,a3)),f8(x3763,a3))),
% 59.45/59.50 inference(scs_inference,[],[235,34,241,309,19,17])).
% 59.45/59.50 cnf(378,plain,
% 59.45/59.50 (P3(a3,f4(a3,a3),f4(f8(x3781,a3),f8(x3782,a3)))),
% 59.45/59.50 inference(scs_inference,[],[42,235,34,241,309,244,19,17,16])).
% 59.45/59.50 cnf(379,plain,
% 59.45/59.50 (P3(x3791,f4(a3,a3),x3791)),
% 59.45/59.50 inference(rename_variables,[],[42])).
% 59.45/59.50 cnf(382,plain,
% 59.45/59.50 (P3(x3821,f4(a3,a3),x3821)),
% 59.45/59.50 inference(rename_variables,[],[42])).
% 59.45/59.50 cnf(384,plain,
% 59.45/59.50 (P2(f8(x3841,a3),f4(f8(x3842,a3),f4(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[42,379,235,34,241,309,244,137,19,17,16,14,21])).
% 59.45/59.50 cnf(398,plain,
% 59.45/59.50 (P3(a3,f8(x3981,f8(x3982,a3)),a3)),
% 59.45/59.50 inference(scs_inference,[],[105,102,85,319,42,379,382,333,256,235,34,241,329,336,309,244,137,7,19,17,16,14,21,15,22,25,23])).
% 59.45/59.50 cnf(408,plain,
% 59.45/59.50 (P2(x4081,f4(x4081,f4(a3,a3)))),
% 59.45/59.50 inference(rename_variables,[],[96])).
% 59.45/59.50 cnf(410,plain,
% 59.45/59.50 (P1(x4101,f8(x4102,a3),f8(x4103,a3))),
% 59.45/59.50 inference(scs_inference,[],[5,345,241,96,19,17])).
% 59.45/59.50 cnf(416,plain,
% 59.45/59.50 (P2(f8(x4161,a3),f4(f8(x4162,a3),f4(a3,a3)))),
% 59.45/59.50 inference(rename_variables,[],[384])).
% 59.45/59.50 cnf(419,plain,
% 59.45/59.50 (P2(f8(x4191,a3),f4(f8(x4192,a3),f4(a3,a3)))),
% 59.45/59.50 inference(rename_variables,[],[384])).
% 59.45/59.50 cnf(421,plain,
% 59.45/59.50 (P2(a7,f8(a1,f5(a2)))),
% 59.45/59.50 inference(scs_inference,[],[102,319,5,345,241,384,416,96,408,8,19,17,18,16,15,21])).
% 59.45/59.50 cnf(422,plain,
% 59.45/59.50 (P1(x4221,x4222,f8(x4221,x4222))),
% 59.45/59.50 inference(rename_variables,[],[8])).
% 59.45/59.50 cnf(429,plain,
% 59.45/59.50 (P1(x4291,f8(x4292,a3),a3)),
% 59.45/59.50 inference(rename_variables,[],[345])).
% 59.45/59.50 cnf(431,plain,
% 59.45/59.50 (P3(f8(x4311,a3),f8(x4312,a3),a3)),
% 59.45/59.50 inference(scs_inference,[],[105,102,319,342,146,79,5,345,88,241,384,416,419,96,408,8,19,17,18,16,15,21,14,24,23])).
% 59.45/59.50 cnf(435,plain,
% 59.45/59.50 (P1(x4351,f8(x4352,a3),a3)),
% 59.45/59.50 inference(rename_variables,[],[345])).
% 59.45/59.50 cnf(436,plain,
% 59.45/59.50 (P1(x4361,f8(x4362,a3),f8(x4362,a3))),
% 59.45/59.50 inference(rename_variables,[],[170])).
% 59.45/59.50 cnf(440,plain,
% 59.45/59.50 (P3(x4401,x4402,f4(x4401,x4402))),
% 59.45/59.50 inference(rename_variables,[],[7])).
% 59.45/59.50 cnf(447,plain,
% 59.45/59.50 (P3(f8(x4471,a3),x4472,a3)+~P3(f4(a3,a3),x4472,f5(a3))),
% 59.45/59.50 inference(scs_inference,[],[105,102,319,342,146,79,5,345,429,435,88,170,436,6,241,384,416,419,96,408,8,422,7,440,19,17,18,16,15,21,14,24,23,25,27,28,22])).
% 59.45/59.50 cnf(455,plain,
% 59.45/59.50 (P2(f8(x4551,a3),f8(f8(x4551,a3),x4552))),
% 59.45/59.50 inference(rename_variables,[],[143])).
% 59.45/59.50 cnf(457,plain,
% 59.45/59.50 (P1(f8(x4571,a3),x4572,f8(x4573,a3))),
% 59.45/59.50 inference(scs_inference,[],[235,206,241,143,19,17])).
% 59.45/59.50 cnf(460,plain,
% 59.45/59.50 (P3(x4601,f4(a3,a3),x4601)),
% 59.45/59.50 inference(rename_variables,[],[42])).
% 59.45/59.50 cnf(462,plain,
% 59.45/59.50 (P3(f8(a1,f5(a2)),f4(a3,a3),a7)),
% 59.45/59.50 inference(scs_inference,[],[42,460,235,206,241,421,143,19,17,14,16])).
% 59.45/59.50 cnf(469,plain,
% 59.45/59.50 (P3(x4691,a3,f4(x4691,f8(x4692,a3)))),
% 59.45/59.50 inference(rename_variables,[],[82])).
% 59.45/59.50 cnf(470,plain,
% 59.45/59.50 (P3(a3,f4(a3,a3),f8(x4701,a3))),
% 59.45/59.50 inference(rename_variables,[],[105])).
% 59.45/59.50 cnf(476,plain,
% 59.45/59.50 (P1(f8(x4761,a3),x4762,f4(f8(x4763,a3),f4(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[105,319,42,460,79,82,5,235,206,256,329,184,88,2,241,421,143,455,19,17,14,16,15,23,25,24])).
% 59.45/59.50 cnf(484,plain,
% 59.45/59.50 (P1(f8(x4841,a3),f4(f8(x4842,a3),f4(a3,a3)),f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[105,470,319,42,460,79,82,469,5,235,206,256,3,329,309,184,88,2,241,421,143,455,7,19,17,14,16,15,23,25,24,29,28])).
% 59.45/59.50 cnf(497,plain,
% 59.45/59.50 (P2(f8(x4971,a3),f8(a3,f8(x4972,a3)))),
% 59.45/59.50 inference(scs_inference,[],[373,187,241,88,17,21])).
% 59.45/59.50 cnf(498,plain,
% 59.45/59.50 (P1(x4981,a3,f8(x4981,f8(x4982,a3)))),
% 59.45/59.50 inference(rename_variables,[],[88])).
% 59.45/59.50 cnf(513,plain,
% 59.45/59.50 (P3(f8(x5131,a3),a3,f8(x5132,a3))),
% 59.45/59.50 inference(scs_inference,[],[102,319,42,431,5,373,187,8,241,295,190,140,88,498,17,21,14,16,15,25,23])).
% 59.45/59.50 cnf(526,plain,
% 59.45/59.50 (P1(a3,x5261,f8(x5262,a3))),
% 59.45/59.50 inference(scs_inference,[],[301,184,17])).
% 59.45/59.50 cnf(532,plain,
% 59.45/59.50 (P2(a3,f4(f8(x5321,a3),f8(x5321,a3)))),
% 59.45/59.50 inference(scs_inference,[],[345,301,336,184,290,17,18,21])).
% 59.45/59.50 cnf(535,plain,
% 59.45/59.50 (P3(a3,f4(a3,a3),f4(a3,f8(x5351,a3)))),
% 59.45/59.50 inference(scs_inference,[],[105,345,301,336,140,184,290,17,18,21,14])).
% 59.45/59.50 cnf(560,plain,
% 59.45/59.50 (P2(x5601,f4(x5601,f4(a3,a3)))),
% 59.45/59.50 inference(rename_variables,[],[96])).
% 59.45/59.50 cnf(562,plain,
% 59.45/59.50 (P1(x5621,a3,f8(x5622,a3))),
% 59.45/59.50 inference(scs_inference,[],[5,34,410,96,17,18])).
% 59.45/59.50 cnf(565,plain,
% 59.45/59.50 (P2(a3,f8(x5651,f8(x5652,a3)))),
% 59.45/59.50 inference(scs_inference,[],[5,34,410,2,96,88,17,18,21])).
% 59.45/59.50 cnf(570,plain,
% 59.45/59.50 (P3(x5701,f8(a1,f5(a2)),f4(x5701,a7))),
% 59.45/59.50 inference(scs_inference,[],[102,5,34,410,2,96,7,421,88,532,17,18,21,14,15])).
% 59.45/59.50 cnf(579,plain,
% 59.45/59.50 (P1(x5791,f4(a3,a3),f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[105,102,85,535,5,34,410,2,96,560,7,421,88,484,532,17,18,21,14,15,16,23,25])).
% 59.45/59.50 cnf(606,plain,
% 59.45/59.50 (P2(f8(x6061,a3),f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[329,579,21])).
% 59.45/59.50 cnf(607,plain,
% 59.45/59.50 (P1(x6071,f4(a3,a3),f4(a3,a3))),
% 59.45/59.50 inference(rename_variables,[],[579])).
% 59.45/59.50 cnf(608,plain,
% 59.45/59.50 (P1(f4(f8(x6081,a3),f8(x6081,a3)),x6082,f8(x6083,a3))),
% 59.45/59.50 inference(rename_variables,[],[329])).
% 59.45/59.50 cnf(618,plain,
% 59.45/59.50 (~P3(f4(a6,a7),f4(a3,a3),a3)),
% 59.45/59.50 inference(scs_inference,[],[30,319,298,102,462,570,329,336,579,497,565,21,14,16,15,23])).
% 59.45/59.50 cnf(622,plain,
% 59.45/59.50 (P1(x6221,f4(a3,a3),f4(a3,a3))),
% 59.45/59.50 inference(rename_variables,[],[579])).
% 59.45/59.50 cnf(625,plain,
% 59.45/59.50 (P1(f8(x6251,a3),x6252,f4(f8(a3,a3),f8(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[30,319,298,102,462,570,5,376,329,187,8,336,579,607,497,565,67,21,14,16,15,23,25,24])).
% 59.45/59.50 cnf(627,plain,
% 59.45/59.50 (P1(x6271,f4(f8(x6272,a3),f4(a3,a3)),f8(x6273,a3))),
% 59.45/59.50 inference(rename_variables,[],[376])).
% 59.45/59.50 cnf(631,plain,
% 59.45/59.50 (P1(x6311,f4(f8(x6312,a3),f4(a3,a3)),f8(x6313,a3))),
% 59.45/59.50 inference(rename_variables,[],[376])).
% 59.45/59.50 cnf(632,plain,
% 59.45/59.50 (P3(x6321,x6322,f4(x6321,x6322))),
% 59.45/59.50 inference(rename_variables,[],[7])).
% 59.45/59.50 cnf(634,plain,
% 59.45/59.50 (P3(f8(x6341,a3),f8(x6341,a3),f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[30,319,298,102,462,570,5,376,627,329,608,187,7,632,8,336,579,607,622,497,565,67,21,14,16,15,23,25,24,26,27])).
% 59.45/59.50 cnf(640,plain,
% 59.45/59.50 (~P3(f4(a3,a3),f4(a6,a7),a3)),
% 59.45/59.50 inference(scs_inference,[],[30,319,298,102,462,570,5,376,627,329,608,187,7,632,8,336,579,607,622,497,565,67,21,14,16,15,23,25,24,26,27,13])).
% 59.45/59.50 cnf(642,plain,
% 59.45/59.50 (P1(x6421,f4(f8(x6422,a3),f4(a3,a3)),f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[30,319,298,102,462,570,5,376,627,631,329,608,187,7,632,8,336,579,607,622,497,565,67,21,14,16,15,23,25,24,26,27,13,17])).
% 59.45/59.50 cnf(644,plain,
% 59.45/59.50 (P2(f8(x6441,a3),f4(f8(a3,a3),f8(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[376,625,21])).
% 59.45/59.50 cnf(648,plain,
% 59.45/59.50 (P3(a3,f4(a3,a3),f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[105,376,625,606,21,14])).
% 59.45/59.50 cnf(649,plain,
% 59.45/59.50 (P2(f8(x6491,a3),f4(a3,a3))),
% 59.45/59.50 inference(rename_variables,[],[606])).
% 59.45/59.50 cnf(651,plain,
% 59.45/59.50 (P3(f4(a3,a3),f4(a3,a3),f8(x6511,a3))),
% 59.45/59.50 inference(scs_inference,[],[105,298,376,625,606,649,21,14,16])).
% 59.45/59.50 cnf(679,plain,
% 59.45/59.50 (P2(a3,f4(f8(x6791,a3),f8(x6792,a3)))),
% 59.45/59.50 inference(scs_inference,[],[79,82,410,384,295,17,18,20])).
% 59.45/59.50 cnf(680,plain,
% 59.45/59.50 (P3(x6801,a3,f4(x6801,f8(x6802,a3)))),
% 59.45/59.50 inference(rename_variables,[],[82])).
% 59.45/59.50 cnf(682,plain,
% 59.45/59.50 (P2(a3,f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[79,82,410,206,384,295,579,17,18,20,21])).
% 59.45/59.50 cnf(684,plain,
% 59.45/59.50 (P1(f8(x6841,a3),x6842,a3)),
% 59.45/59.50 inference(rename_variables,[],[206])).
% 59.45/59.50 cnf(693,plain,
% 59.45/59.50 (P3(f4(a3,a3),f8(x6931,a3),f8(x6932,a3))),
% 59.45/59.50 inference(scs_inference,[],[298,102,79,82,651,410,206,384,295,644,579,532,17,18,20,21,14,16,15,23])).
% 59.45/59.50 cnf(705,plain,
% 59.45/59.50 (P1(f8(x7051,a3),x7052,a3)),
% 59.45/59.50 inference(rename_variables,[],[206])).
% 59.45/59.50 cnf(720,plain,
% 59.45/59.50 (P1(f4(a3,a3),x7201,f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[105,298,102,79,42,431,82,680,651,5,410,206,684,705,3,634,345,2,457,8,384,295,91,88,644,579,642,532,17,18,20,21,14,16,15,23,24,25,29,26,27,28])).
% 59.45/59.50 cnf(727,plain,
% 59.45/59.50 (P1(x7271,f8(x7272,a3),f4(a3,f4(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[410,295,17])).
% 59.45/59.50 cnf(736,plain,
% 59.45/59.50 (P3(f8(x7361,a3),f4(a3,a3),f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[102,410,295,336,682,290,17,18,21,14])).
% 59.45/59.50 cnf(740,plain,
% 59.45/59.50 (P3(f8(x7401,a3),f4(f8(x7402,a3),f8(x7403,a3)),a3)),
% 59.45/59.50 inference(scs_inference,[],[105,102,79,410,295,336,682,679,290,17,18,21,14,16,15])).
% 59.45/59.50 cnf(744,plain,
% 59.45/59.50 (P1(x7441,f8(x7442,a3),f8(x7443,a3))),
% 59.45/59.50 inference(rename_variables,[],[410])).
% 59.45/59.50 cnf(746,plain,
% 59.45/59.50 (P1(f8(x7461,a3),x7462,f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[105,102,79,5,410,744,206,8,295,336,720,682,679,290,17,18,21,14,16,15,25,24])).
% 59.45/59.50 cnf(764,plain,
% 59.45/59.50 (P1(f4(a3,a3),x7641,a3)),
% 59.45/59.50 inference(scs_inference,[],[3,682,19])).
% 59.45/59.50 cnf(766,plain,
% 59.45/59.50 (P1(a3,x7661,f4(a3,a3))),
% 59.45/59.50 inference(scs_inference,[],[3,682,19,17])).
% 59.45/59.50 cnf(768,plain,
% 59.45/59.50 (P2(a3,f4(f8(x7681,a3),f4(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[3,184,682,19,17,21])).
% 59.45/59.50 cnf(776,plain,
% 59.45/59.50 (P3(f8(x7761,a3),f8(x7762,f8(x7763,a3)),a3)),
% 59.45/59.50 inference(scs_inference,[],[298,102,79,3,184,682,497,565,19,17,21,14,16,15])).
% 59.45/59.50 cnf(801,plain,
% 59.45/59.50 (P1(a3,x8011,f4(f8(x8012,a3),f8(x8013,a3)))),
% 59.45/59.50 inference(scs_inference,[],[3,457,140,679,19,17])).
% 59.45/59.50 cnf(803,plain,
% 59.45/59.50 (P2(a3,f8(f8(x8031,a3),x8032))),
% 59.45/59.50 inference(scs_inference,[],[3,457,140,91,679,19,17,21])).
% 59.45/59.50 cnf(808,plain,
% 59.45/59.50 (P3(f8(x8081,a3),f4(f8(x8082,a3),f4(a3,a3)),a3)),
% 59.45/59.50 inference(scs_inference,[],[102,79,3,457,140,91,679,768,19,17,21,14,15])).
% 59.45/59.50 cnf(817,plain,
% 59.45/59.50 (P3(f8(x8171,a3),f8(x8171,a3),f4(a3,f4(a3,a3)))),
% 59.45/59.50 inference(scs_inference,[],[298,102,79,5,7,329,3,457,140,91,143,679,67,768,727,19,17,21,14,15,16,24,27])).
% 59.45/59.50 cnf(823,plain,
% 59.45/59.51 (P1(x8231,f8(x8232,a3),f8(x8233,f8(x8234,a3)))),
% 59.45/59.51 inference(scs_inference,[],[345,565,17])).
% 59.45/59.51 cnf(825,plain,
% 59.45/59.51 (P2(f8(x8251,a3),f8(x8252,f8(x8253,a3)))),
% 59.45/59.51 inference(scs_inference,[],[329,345,565,17,21])).
% 59.45/59.51 cnf(828,plain,
% 59.45/59.51 (P3(f8(x8281,a3),f8(f8(x8282,a3),x8283),a3)),
% 59.45/59.51 inference(scs_inference,[],[79,329,345,565,803,17,21,15])).
% 59.45/59.51 cnf(832,plain,
% 59.45/59.51 (P1(f8(x8321,a3),x8322,f8(f8(x8323,a3),f8(x8324,a3)))),
% 59.45/59.51 inference(scs_inference,[],[105,79,329,345,410,457,91,565,803,17,21,15,16,24])).
% 59.45/59.51 cnf(855,plain,
% 59.45/59.51 (P1(f4(a3,a3),x8551,f8(x8552,a3))),
% 59.45/59.51 inference(scs_inference,[],[457,606,19])).
% 59.45/59.51 cnf(858,plain,
% 59.45/59.51 (P1(f8(x8581,a3),x8582,f4(a3,f8(x8583,a3)))),
% 59.45/59.51 inference(scs_inference,[],[457,140,606,19,17])).
% 59.45/59.51 cnf(924,plain,
% 59.45/59.51 (P1(f8(x9241,a3),x9242,f4(f8(x9243,a3),f8(x9244,a3)))),
% 59.45/59.51 inference(scs_inference,[],[526,206,679,19,17])).
% 59.45/59.51 cnf(926,plain,
% 59.45/59.51 (P2(f8(x9261,a3),f8(f8(x9262,a3),x9263))),
% 59.45/59.51 inference(scs_inference,[],[526,206,679,91,19,17,21])).
% 59.45/59.51 cnf(946,plain,
% 59.45/59.51 (P1(x9461,f4(a3,a3),a3)),
% 59.45/59.51 inference(scs_inference,[],[682,2,18])).
% 59.45/59.51 cnf(948,plain,
% 59.45/59.51 (P1(x9481,a3,f4(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[682,2,18,17])).
% 59.45/59.51 cnf(950,plain,
% 59.45/59.51 (P2(a3,f4(a3,f8(x9501,a3)))),
% 59.45/59.51 inference(scs_inference,[],[682,2,858,18,17,21])).
% 59.45/59.51 cnf(975,plain,
% 59.45/59.51 (P2(f8(x9751,a3),f4(f8(x9752,a3),f8(x9753,a3)))),
% 59.45/59.51 inference(scs_inference,[],[679,825,457,345,924,19,17,21])).
% 59.45/59.51 cnf(1047,plain,
% 59.45/59.51 (P2(f8(x10471,a3),f4(f8(a3,x10472),f8(a3,x10472)))),
% 59.45/59.51 inference(scs_inference,[],[679,295,457,526,2,67,19,17,21])).
% 59.45/59.51 cnf(1116,plain,
% 59.45/59.51 (P1(x11161,f4(a3,a3),f8(x11162,a3))),
% 59.45/59.51 inference(scs_inference,[],[682,562,18])).
% 59.45/59.51 cnf(1122,plain,
% 59.45/59.51 (P1(x11221,f4(a3,a3),a3)),
% 59.45/59.51 inference(rename_variables,[],[946])).
% 59.45/59.51 cnf(1128,plain,
% 59.45/59.51 (P3(f4(a3,a3),f4(a3,a3),a3)),
% 59.45/59.51 inference(scs_inference,[],[85,682,140,562,410,579,946,1122,924,18,17,21,25,27])).
% 59.45/59.51 cnf(1133,plain,
% 59.45/59.51 (P3(f4(a3,a3),a3,f8(x11331,a3))),
% 59.45/59.51 inference(scs_inference,[],[105,85,682,140,562,410,579,946,1122,924,18,17,21,25,27,23])).
% 59.45/59.51 cnf(1146,plain,
% 59.45/59.51 (P1(x11461,f8(x11462,a3),f4(a3,f8(x11463,a3)))),
% 59.45/59.51 inference(scs_inference,[],[825,140,410,18,17])).
% 59.45/59.51 cnf(1167,plain,
% 59.45/59.51 (P2(f4(a3,a3),f8(x11671,a3))),
% 59.45/59.51 inference(scs_inference,[],[803,295,562,579,1116,18,17,21])).
% 59.45/59.51 cnf(1185,plain,
% 59.45/59.51 (P1(x11851,f8(x11852,a3),f4(f8(a3,x11853),f8(a3,x11853)))),
% 59.45/59.51 inference(scs_inference,[],[679,410,2,1047,18,17])).
% 59.45/59.51 cnf(1202,plain,
% 59.45/59.51 (P2(f4(a3,a3),f4(f8(x12021,a3),f4(a3,a3)))),
% 59.45/59.51 inference(scs_inference,[],[803,579,2,476,18,21])).
% 59.45/59.51 cnf(1203,plain,
% 59.45/59.51 (P1(f8(x12031,a3),x12032,f4(f8(x12033,a3),f4(a3,a3)))),
% 59.45/59.51 inference(rename_variables,[],[476])).
% 59.45/59.51 cnf(1204,plain,
% 59.45/59.51 (P1(x12041,f4(a3,a3),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[579])).
% 59.45/59.51 cnf(1207,plain,
% 59.45/59.51 (P1(x12071,x12072,f8(x12071,x12072))),
% 59.45/59.51 inference(rename_variables,[],[8])).
% 59.45/59.51 cnf(1208,plain,
% 59.45/59.51 (P1(x12081,f4(a3,a3),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[579])).
% 59.45/59.51 cnf(1212,plain,
% 59.45/59.51 (P1(x12121,f4(a3,a3),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[579])).
% 59.45/59.51 cnf(1214,plain,
% 59.45/59.51 (P3(f4(a3,a3),f4(a3,a3),f4(f8(x12141,a3),f4(a3,a3)))),
% 59.45/59.51 inference(scs_inference,[],[42,803,5,579,1204,1208,1212,2,476,1203,8,1207,18,21,25,24,26])).
% 59.45/59.51 cnf(1216,plain,
% 59.45/59.51 (P1(x12161,f4(a3,a3),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[579])).
% 59.45/59.51 cnf(1217,plain,
% 59.45/59.51 (P1(x12171,f4(a3,a3),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[579])).
% 59.45/59.51 cnf(1218,plain,
% 59.45/59.51 (P3(x12181,f4(a3,a3),x12181)),
% 59.45/59.51 inference(rename_variables,[],[42])).
% 59.45/59.51 cnf(1220,plain,
% 59.45/59.51 (P1(f8(x12201,a3),f4(a3,a3),f4(f4(a3,a3),f4(a3,a3)))),
% 59.45/59.51 inference(scs_inference,[],[105,42,7,803,5,579,1204,1208,1212,1217,1216,2,476,1203,8,1207,18,21,25,24,26,28])).
% 59.45/59.51 cnf(1222,plain,
% 59.45/59.51 (P1(x12221,f4(a3,a3),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[579])).
% 59.45/59.51 cnf(1233,plain,
% 59.45/59.51 (P1(x12331,f4(a3,a3),f4(f8(x12332,a3),f4(a3,a3)))),
% 59.45/59.51 inference(scs_inference,[],[105,85,42,1218,7,803,5,579,1204,1208,1212,1217,1222,1216,410,2,476,1203,8,1207,1185,18,21,25,24,26,28,27,16,17])).
% 59.45/59.51 cnf(1237,plain,
% 59.45/59.51 (P2(f4(a3,a3),f8(f8(x12371,a3),f4(a3,a3)))),
% 59.45/59.51 inference(scs_inference,[],[950,579,2,91,18,21])).
% 59.45/59.51 cnf(1268,plain,
% 59.45/59.51 (P3(f4(a3,a3),f4(f8(x12681,a3),f4(a3,a3)),f8(x12682,a3))),
% 59.45/59.51 inference(scs_inference,[],[339,825,526,1214,17,23])).
% 59.45/59.51 cnf(1292,plain,
% 59.45/59.51 (P2(f4(a3,a3),f8(f8(x12921,a3),f8(x12922,a3)))),
% 59.45/59.51 inference(scs_inference,[],[579,562,1047,832,17,21])).
% 59.45/59.51 cnf(1319,plain,
% 59.45/59.51 (P2(f4(a3,a3),f4(f8(x13191,a3),f8(x13192,a3)))),
% 59.45/59.51 inference(scs_inference,[],[579,801,1292,17,21])).
% 59.45/59.51 cnf(1344,plain,
% 59.45/59.51 (P2(a3,f4(f8(a3,x13441),f8(a3,x13441)))),
% 59.45/59.51 inference(scs_inference,[],[565,3,526,295,67,19,17,21])).
% 59.45/59.51 cnf(1347,plain,
% 59.45/59.51 (P1(a3,f8(x13471,a3),f4(f8(x13472,a3),a3))),
% 59.45/59.51 inference(scs_inference,[],[105,7,565,3,526,295,67,19,17,21,29])).
% 59.45/59.51 cnf(1384,plain,
% 59.45/59.51 (P3(x13841,f8(a1,f5(a2)),f4(x13841,a7))),
% 59.45/59.51 inference(rename_variables,[],[570])).
% 59.45/59.51 cnf(1390,plain,
% 59.45/59.51 (P3(a3,f4(a3,a7),f4(a3,a7))),
% 59.45/59.51 inference(scs_inference,[],[570,1384,319,618,6,241,16,22,23])).
% 59.45/59.51 cnf(1422,plain,
% 59.45/59.51 (~P3(f4(a3,a3),f4(a7,a6),a3)),
% 59.45/59.51 inference(scs_inference,[],[9,42,7,23,13])).
% 59.45/59.51 cnf(1474,plain,
% 59.45/59.51 (~P3(a3,f4(a6,f8(x14741,a3)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[94,79,7,23,13])).
% 59.45/59.51 cnf(1482,plain,
% 59.45/59.51 (~P3(a3,f4(a3,a6),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1474,82,7,23,13])).
% 59.45/59.51 cnf(1484,plain,
% 59.45/59.51 (~P3(f8(x14841,a3),x14842,a7)+~P3(x14842,a6,f8(x14843,a3))),
% 59.45/59.51 inference(scs_inference,[],[9,1474,82,431,7,23,13,22])).
% 59.45/59.51 cnf(1498,plain,
% 59.45/59.51 (~P3(x14981,f8(x14982,a3),a7)+~P3(x14981,a6,f4(f8(x14983,a3),f4(a3,a3)))),
% 59.45/59.51 inference(scs_inference,[],[9,85,808,1390,7,23,22,13])).
% 59.45/59.51 cnf(1506,plain,
% 59.45/59.51 (~P3(f4(a7,a6),a3,a3)),
% 59.45/59.51 inference(scs_inference,[],[9,4,7,23])).
% 59.45/59.51 cnf(1510,plain,
% 59.45/59.51 (~P3(a3,f4(a7,a6),a3)),
% 59.45/59.51 inference(scs_inference,[],[9,4,7,23,13])).
% 59.45/59.51 cnf(1619,plain,
% 59.45/59.51 (P2(f8(x16191,a3),f8(a3,x16192))),
% 59.45/59.51 inference(scs_inference,[],[526,8,21])).
% 59.45/59.51 cnf(1625,plain,
% 59.45/59.51 (P3(a3,f4(a3,a3),f8(a3,x16251))),
% 59.45/59.51 inference(scs_inference,[],[105,526,8,1047,21,17,14])).
% 59.45/59.51 cnf(1627,plain,
% 59.45/59.51 (P3(a3,f8(a3,x16271),f8(x16272,a3))),
% 59.45/59.51 inference(scs_inference,[],[105,319,526,8,1047,21,17,14,15])).
% 59.45/59.51 cnf(1629,plain,
% 59.45/59.51 (P3(f8(a3,x16291),f4(a3,a3),f8(x16292,a3))),
% 59.45/59.51 inference(scs_inference,[],[105,319,298,526,8,1047,21,17,14,15,16])).
% 59.45/59.51 cnf(1645,plain,
% 59.45/59.51 (P1(a3,x16451,f8(a3,x16452))),
% 59.45/59.51 inference(scs_inference,[],[526,1619,17])).
% 59.45/59.51 cnf(1650,plain,
% 59.45/59.51 (P1(x16501,a3,a3)),
% 59.45/59.51 inference(rename_variables,[],[2])).
% 59.45/59.51 cnf(1652,plain,
% 59.45/59.51 (P1(x16521,f8(a3,x16522),f8(a3,x16522))),
% 59.45/59.51 inference(scs_inference,[],[1625,526,2,1650,579,1619,17,24,29])).
% 59.45/59.51 cnf(1684,plain,
% 59.45/59.51 (P1(x16841,f8(a3,x16842),f8(x16843,a3))),
% 59.45/59.51 inference(scs_inference,[],[410,1619,18])).
% 59.45/59.51 cnf(1685,plain,
% 59.45/59.51 (P2(f8(x16851,a3),f8(a3,x16852))),
% 59.45/59.51 inference(rename_variables,[],[1619])).
% 59.45/59.51 cnf(1687,plain,
% 59.45/59.51 (P1(x16871,f8(x16872,a3),f8(a3,x16873))),
% 59.45/59.51 inference(scs_inference,[],[410,1619,1685,18,17])).
% 59.45/59.51 cnf(1690,plain,
% 59.45/59.51 (P1(f8(x16901,a3),x16902,f8(a3,x16903))),
% 59.45/59.51 inference(scs_inference,[],[410,457,1619,1685,1645,18,17,24])).
% 59.45/59.51 cnf(1711,plain,
% 59.45/59.51 (P1(f8(a3,x17111),x17112,f8(x17113,a3))),
% 59.45/59.51 inference(scs_inference,[],[457,1619,19])).
% 59.45/59.51 cnf(1723,plain,
% 59.45/59.51 (P2(x17231,f4(x17231,f4(a3,a3)))),
% 59.45/59.51 inference(rename_variables,[],[96])).
% 59.45/59.51 cnf(1726,plain,
% 59.45/59.51 (P2(x17261,f4(x17261,f4(a3,a3)))),
% 59.45/59.51 inference(rename_variables,[],[96])).
% 59.45/59.51 cnf(1728,plain,
% 59.45/59.51 (P2(a6,f8(a1,a2))),
% 59.45/59.51 inference(scs_inference,[],[1,96,1723,8,19,18,21])).
% 59.45/59.51 cnf(1729,plain,
% 59.45/59.51 (P1(x17291,x17292,f8(x17291,x17292))),
% 59.45/59.51 inference(rename_variables,[],[8])).
% 59.45/59.51 cnf(1739,plain,
% 59.45/59.51 (P1(x17391,x17392,f8(x17391,x17392))),
% 59.45/59.51 inference(rename_variables,[],[8])).
% 59.45/59.51 cnf(1740,plain,
% 59.45/59.51 (P3(x17401,x17402,f4(x17401,x17402))),
% 59.45/59.51 inference(rename_variables,[],[7])).
% 59.45/59.51 cnf(1744,plain,
% 59.45/59.51 (P3(x17441,x17442,f4(x17441,x17442))),
% 59.45/59.51 inference(rename_variables,[],[7])).
% 59.45/59.51 cnf(1746,plain,
% 59.45/59.51 (P3(a6,f4(a3,a3),f8(a1,a2))),
% 59.45/59.51 inference(scs_inference,[],[1,42,96,1723,1726,562,8,1729,1739,7,1740,1687,19,18,21,17,24,26,27,14])).
% 59.45/59.51 cnf(1749,plain,
% 59.45/59.51 (P3(x17491,f8(a1,a2),f4(x17491,a6))),
% 59.45/59.51 inference(scs_inference,[],[1,42,96,1723,1726,562,8,1729,1739,7,1740,1744,1687,19,18,21,17,24,26,27,14,15])).
% 59.45/59.51 cnf(1757,plain,
% 59.45/59.51 (~P3(f8(x17571,a3),f8(a1,a2),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1,1482,105,570,85,42,96,1723,1726,562,8,1729,1739,7,1740,1744,1687,19,18,21,17,24,26,27,14,15,16,22,23])).
% 59.45/59.51 cnf(1770,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f8(x17701,a3),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1757,13])).
% 59.45/59.51 cnf(1772,plain,
% 59.45/59.51 (~P3(f4(f4(a3,a3),a7),f8(a1,a2),a3)),
% 59.45/59.51 inference(scs_inference,[],[1422,1749,1757,7,13,23])).
% 59.45/59.51 cnf(1790,plain,
% 59.45/59.51 (~P3(f4(f8(a1,a2),f8(x17901,a3)),f4(a3,a3),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,105,82,1772,13,23])).
% 59.45/59.51 cnf(1807,plain,
% 59.45/59.51 (P2(x18071,f4(x18071,f4(a3,a3)))),
% 59.45/59.51 inference(rename_variables,[],[96])).
% 59.45/59.51 cnf(1811,plain,
% 59.45/59.51 (P3(f4(a3,f4(a3,a3)),f8(x18111,a3),f8(x18112,a3))),
% 59.45/59.51 inference(scs_inference,[],[319,298,1790,96,1807,1202,13,14,15,16])).
% 59.45/59.51 cnf(1815,plain,
% 59.45/59.51 (P3(x18151,a3,f4(x18151,f8(x18152,a3)))),
% 59.45/59.51 inference(rename_variables,[],[82])).
% 59.45/59.51 cnf(1816,plain,
% 59.45/59.51 (P3(a3,f8(x18161,a3),f8(x18162,a3))),
% 59.45/59.51 inference(rename_variables,[],[319])).
% 59.45/59.51 cnf(1818,plain,
% 59.45/59.51 (~P3(f4(f8(a1,a2),f8(x18181,a3)),f8(x18182,a3),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,319,1816,298,431,82,1815,1790,96,1807,1202,13,14,15,16,22,23])).
% 59.45/59.51 cnf(1840,plain,
% 59.45/59.51 (P3(f8(x18401,a3),f4(f4(a3,a3),f4(a3,a3)),f8(x18402,a3))),
% 59.45/59.51 inference(scs_inference,[],[298,1818,96,1047,13,14,15])).
% 59.45/59.51 cnf(1845,plain,
% 59.45/59.51 (~P3(f4(f8(a1,a2),f8(x18451,a3)),a3,f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,298,319,85,82,1818,96,565,1047,13,14,15,16,23])).
% 59.45/59.51 cnf(1865,plain,
% 59.45/59.51 (P3(f8(x18651,a3),f4(f8(x18652,a3),f8(x18653,a3)),f8(x18654,a3))),
% 59.45/59.51 inference(scs_inference,[],[319,513,1845,679,140,13,14,15])).
% 59.45/59.51 cnf(1869,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f4(a3,a3),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,319,513,42,651,1845,679,140,13,14,15,16,23])).
% 59.45/59.51 cnf(1894,plain,
% 59.45/59.51 (~P3(f4(a3,a3),f8(a1,a2),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1869,13])).
% 59.45/59.51 cnf(1896,plain,
% 59.45/59.51 (P3(f8(x18961,a3),f4(a3,a3),f8(a3,x18962))),
% 59.45/59.51 inference(scs_inference,[],[298,1869,1619,13,14])).
% 59.45/59.51 cnf(1899,plain,
% 59.45/59.51 (P3(f8(x18991,a3),f8(x18992,f8(x18993,a3)),f8(x18994,a3))),
% 59.45/59.51 inference(scs_inference,[],[298,513,1869,565,1619,13,14,15])).
% 59.45/59.51 cnf(1901,plain,
% 59.45/59.51 (~P3(f8(a1,a2),a3,f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,298,513,42,1133,1869,565,1619,13,14,15,23])).
% 59.45/59.51 cnf(1916,plain,
% 59.45/59.51 (~P3(a3,f8(a1,a2),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1901,13])).
% 59.45/59.51 cnf(1918,plain,
% 59.45/59.51 (P3(f8(x19181,a3),f8(f8(x19182,a3),x19183),f8(x19184,a3))),
% 59.45/59.51 inference(scs_inference,[],[513,1901,803,13,15])).
% 59.45/59.51 cnf(1924,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f4(f8(x19241,a3),f4(a3,a3)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1,1770,513,42,1268,1901,803,345,1687,13,15,25,23])).
% 59.45/59.51 cnf(1942,plain,
% 59.45/59.51 (P3(f8(x19421,a3),f4(a3,f8(x19422,a3)),f8(x19423,a3))),
% 59.45/59.51 inference(scs_inference,[],[513,1924,950,13,15])).
% 59.45/59.51 cnf(1960,plain,
% 59.45/59.51 (P3(f8(x19601,a3),f4(f8(a3,x19602),f8(a3,x19602)),f8(x19603,a3))),
% 59.45/59.51 inference(scs_inference,[],[513,1344,15])).
% 59.45/59.51 cnf(1998,plain,
% 59.45/59.51 (P2(a3,f8(a3,x19981))),
% 59.45/59.51 inference(scs_inference,[],[2,1645,21])).
% 59.45/59.51 cnf(2000,plain,
% 59.45/59.51 (P1(x20001,a3,a3)),
% 59.45/59.51 inference(rename_variables,[],[2])).
% 59.45/59.51 cnf(2002,plain,
% 59.45/59.51 (P1(x20021,a3,f8(a3,x20022))),
% 59.45/59.51 inference(scs_inference,[],[2,2000,1645,21,17])).
% 59.45/59.51 cnf(2004,plain,
% 59.45/59.51 (P1(a6,f4(a3,a3),f8(a3,x20041))),
% 59.45/59.51 inference(scs_inference,[],[1,2,2000,946,1645,21,17,24])).
% 59.45/59.51 cnf(2012,plain,
% 59.45/59.51 (P3(f8(x20121,a3),f8(a3,x20122),f8(x20123,a3))),
% 59.45/59.51 inference(scs_inference,[],[1,1894,513,1746,2,2000,946,7,1645,21,17,24,23,13,15])).
% 59.45/59.51 cnf(2031,plain,
% 59.45/59.51 (~P3(f4(a3,a6),f4(a3,a3),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1916,1746,562,410,7,1347,25,23])).
% 59.45/59.51 cnf(2052,plain,
% 59.45/59.51 (P3(f8(x20521,a3),f4(a3,f4(a3,a3)),f8(x20522,a3))),
% 59.45/59.51 inference(scs_inference,[],[1811,817,23])).
% 59.45/59.51 cnf(2065,plain,
% 59.45/59.51 (P3(f8(a1,a2),f4(a3,a3),a6)),
% 59.45/59.51 inference(scs_inference,[],[42,1728,16])).
% 59.45/59.51 cnf(2104,plain,
% 59.45/59.51 (P1(x21041,f8(x21042,a3),f4(f8(x21043,a3),a3))),
% 59.45/59.51 inference(scs_inference,[],[105,562,946,7,29])).
% 59.45/59.51 cnf(2115,plain,
% 59.45/59.51 (P1(x21151,a3,a3)),
% 59.45/59.51 inference(rename_variables,[],[2])).
% 59.45/59.51 cnf(2118,plain,
% 59.45/59.51 (P3(a3,a3,f8(a3,x21181))),
% 59.45/59.51 inference(scs_inference,[],[105,85,82,562,2,2115,410,946,948,7,1645,29,27,28,26])).
% 59.45/59.51 cnf(2123,plain,
% 59.45/59.51 (P2(f8(x21231,a3),f4(f8(x21232,a3),a3))),
% 59.45/59.51 inference(scs_inference,[],[410,2104,21])).
% 59.45/59.51 cnf(2129,plain,
% 59.45/59.51 (P1(x21291,a3,a3)),
% 59.45/59.51 inference(rename_variables,[],[2])).
% 59.45/59.51 cnf(2142,plain,
% 59.45/59.51 (P3(f8(x21421,a3),f4(f8(x21422,a3),a3),f8(x21423,a3))),
% 59.45/59.51 inference(scs_inference,[],[1,105,319,298,513,562,2,2129,410,948,7,2104,21,17,25,28,14,15,16,23])).
% 59.45/59.51 cnf(2177,plain,
% 59.45/59.51 (P1(x21771,f8(a3,x21772),a3)),
% 59.45/59.51 inference(scs_inference,[],[345,1619,18])).
% 59.45/59.51 cnf(2180,plain,
% 59.45/59.51 (P2(a3,f4(f8(x21801,a3),a3))),
% 59.45/59.51 inference(scs_inference,[],[345,1619,2104,18,21])).
% 59.45/59.51 cnf(2468,plain,
% 59.45/59.51 (P3(x24681,f4(a3,a3),x24681)),
% 59.45/59.51 inference(rename_variables,[],[42])).
% 59.45/59.51 cnf(2470,plain,
% 59.45/59.51 (P3(x24701,f8(x24702,a3),x24701)),
% 59.45/59.51 inference(scs_inference,[],[42,2468,1167,2123,14,15])).
% 59.45/59.51 cnf(2488,plain,
% 59.45/59.51 (P3(x24881,f8(x24882,a3),x24881)),
% 59.45/59.51 inference(rename_variables,[],[2470])).
% 59.45/59.51 cnf(2490,plain,
% 59.45/59.51 (~P3(a6,a7,f4(f8(x24901,a3),f4(a3,a3)))),
% 59.45/59.51 inference(scs_inference,[],[2470,1498,13])).
% 59.45/59.51 cnf(2492,plain,
% 59.45/59.51 (~P3(a6,f4(f8(x24921,a3),f4(a3,a3)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[94,808,2470,2488,1498,13,23])).
% 59.45/59.51 cnf(2499,plain,
% 59.45/59.51 (P3(x24991,f4(f8(x24992,a3),f4(a3,a3)),x24991)),
% 59.45/59.51 inference(scs_inference,[],[42,2492,1202,13,15])).
% 59.45/59.51 cnf(2501,plain,
% 59.45/59.51 (~P3(a6,f8(x25011,f8(x25012,a3)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[94,42,776,2492,2470,1202,13,15,23])).
% 59.45/59.51 cnf(2522,plain,
% 59.45/59.51 (P3(x25221,f4(f4(a3,a3),f4(a3,a3)),x25221)),
% 59.45/59.51 inference(scs_inference,[],[42,2501,96,13,15])).
% 59.45/59.51 cnf(2523,plain,
% 59.45/59.51 (P2(x25231,f4(x25231,f4(a3,a3)))),
% 59.45/59.51 inference(rename_variables,[],[96])).
% 59.45/59.51 cnf(2525,plain,
% 59.45/59.51 (P3(f4(x25251,f4(a3,a3)),f4(a3,a3),x25251)),
% 59.45/59.51 inference(scs_inference,[],[42,2501,96,2523,13,15,16])).
% 59.45/59.51 cnf(2528,plain,
% 59.45/59.51 (~P3(a6,f4(f8(x25281,a3),f8(x25282,a3)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[94,42,740,2501,2470,96,2523,13,15,16,23])).
% 59.45/59.51 cnf(2549,plain,
% 59.45/59.51 (P3(x25491,f4(a3,a3),x25491)),
% 59.45/59.51 inference(rename_variables,[],[42])).
% 59.45/59.51 cnf(2551,plain,
% 59.45/59.51 (P3(x25511,f8(f8(x25512,a3),f4(a3,a3)),x25511)),
% 59.45/59.51 inference(scs_inference,[],[42,2549,2525,2528,1237,13,20,15])).
% 59.45/59.51 cnf(2556,plain,
% 59.45/59.51 (~P3(a6,f8(f8(x25561,a3),x25562),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[94,42,2549,828,2525,2528,2470,1344,1237,13,20,15,16,23])).
% 59.45/59.51 cnf(2585,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f4(f8(x25851,a3),f8(x25852,a3)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,1865,2556,2470,345,579,2123,1220,13,18,25,23])).
% 59.45/59.51 cnf(2600,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f8(x26001,f8(x26002,a3)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,1899,2585,2470,13,23])).
% 59.45/59.51 cnf(2618,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f8(a3,x26181),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,2012,2600,2470,13,23])).
% 59.45/59.51 cnf(2622,plain,
% 59.45/59.51 (~P3(a3,x26221,a6)+~P3(x26221,a7,a3)),
% 59.45/59.51 inference(scs_inference,[],[1770,2490,2012,149,2600,2470,13,23,22])).
% 59.45/59.51 cnf(2631,plain,
% 59.45/59.51 (~P3(f8(a3,x26311),f8(a1,a2),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[2618,13])).
% 59.45/59.51 cnf(2633,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f4(a3,f8(x26331,a3)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,1942,2618,2470,13,23])).
% 59.45/59.51 cnf(2643,plain,
% 59.45/59.51 (P3(x26431,f8(f8(x26432,a3),f8(x26433,a3)),x26431)),
% 59.45/59.51 inference(scs_inference,[],[42,2633,1292,13,15])).
% 59.45/59.51 cnf(2645,plain,
% 59.45/59.51 (P3(f8(a3,x26451),f4(a3,a3),a3)),
% 59.45/59.51 inference(scs_inference,[],[42,2633,1292,1998,13,15,16])).
% 59.45/59.51 cnf(2648,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f8(f8(x26481,a3),x26482),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,42,1918,2633,2470,1292,1998,13,15,16,23])).
% 59.45/59.51 cnf(2662,plain,
% 59.45/59.51 (~P3(a3,f5(a7),a6)),
% 59.45/59.51 inference(scs_inference,[],[6,2622,13])).
% 59.45/59.51 cnf(2665,plain,
% 59.45/59.51 (~P3(f5(f8(a1,a2)),f5(a7),f4(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[2065,2648,2662,6,13,22])).
% 59.45/59.51 cnf(2668,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f4(f8(a3,x26681),f8(a3,x26681)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,2065,1960,2648,2662,2470,6,13,22,23])).
% 59.45/59.51 cnf(2675,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f4(a3,f4(a3,a3)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,2052,2665,2470,13,23])).
% 59.45/59.51 cnf(2684,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f4(f8(x26841,a3),a3),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,2142,2675,2470,13,23])).
% 59.45/59.51 cnf(2693,plain,
% 59.45/59.51 (~P3(f8(a1,a2),f4(f4(a3,a3),f4(a3,a3)),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,1840,2668,2470,13,23])).
% 59.45/59.51 cnf(2702,plain,
% 59.45/59.51 (~P3(f4(a7,a6),f4(f8(x27021,a3),f4(a3,a3)),a3)),
% 59.45/59.51 inference(scs_inference,[],[9,2499,2693,7,13,23])).
% 59.45/59.51 cnf(2711,plain,
% 59.45/59.51 (~P3(f4(a7,a6),f8(f8(x27111,a3),f4(a3,a3)),a3)),
% 59.45/59.51 inference(scs_inference,[],[9,2551,2684,7,13,23])).
% 59.45/59.51 cnf(2720,plain,
% 59.45/59.51 (P3(x27201,f4(f8(x27202,a3),f8(x27203,a3)),x27201)),
% 59.45/59.51 inference(scs_inference,[],[42,2702,1319,13,15])).
% 59.45/59.51 cnf(2725,plain,
% 59.45/59.51 (~P3(f4(a7,a6),f4(f4(a3,a3),f4(a3,a3)),a3)),
% 59.45/59.51 inference(scs_inference,[],[9,42,2522,2702,1319,7,2180,13,15,16,23])).
% 59.45/59.51 cnf(2741,plain,
% 59.45/59.51 (~P3(f4(a7,a6),f8(f8(x27411,a3),f8(x27412,a3)),a3)),
% 59.45/59.51 inference(scs_inference,[],[9,2643,2725,7,13,23])).
% 59.45/59.51 cnf(2750,plain,
% 59.45/59.51 (~P3(f4(a7,a6),f8(x27501,a3),a3)),
% 59.45/59.51 inference(scs_inference,[],[9,2470,2711,7,13,23])).
% 59.45/59.51 cnf(2759,plain,
% 59.45/59.51 (~P3(f4(a7,a6),f4(f8(x27591,a3),f8(x27592,a3)),a3)),
% 59.45/59.51 inference(scs_inference,[],[9,2720,2741,7,13,23])).
% 59.45/59.51 cnf(2768,plain,
% 59.45/59.51 (~P3(f4(f4(a7,a6),f8(x27681,a3)),f4(a3,a3),a3)),
% 59.45/59.51 inference(scs_inference,[],[82,378,2759,13,23])).
% 59.45/59.51 cnf(2777,plain,
% 59.45/59.51 (~P3(f8(x27771,a3),x27772,a6)+~P3(x27772,a7,f8(x27771,a3))),
% 59.45/59.51 inference(scs_inference,[],[2490,2768,362,13,22])).
% 59.45/59.51 cnf(2786,plain,
% 59.45/59.51 (~P3(f8(x27861,a3),f4(a7,a6),a3)),
% 59.45/59.51 inference(scs_inference,[],[2750,13])).
% 59.45/59.51 cnf(2790,plain,
% 59.45/59.51 (~P3(f4(a3,a3),x27901,a6)+~P3(x27901,a7,f4(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[2490,2750,1214,13,447,22])).
% 59.45/59.51 cnf(2876,plain,
% 59.45/59.51 (P2(f8(x28761,a3),f4(a3,f8(x28762,a3)))),
% 59.45/59.51 inference(rename_variables,[],[140])).
% 59.45/59.51 cnf(2878,plain,
% 59.45/59.51 (P3(f4(a3,a3),f4(a3,f8(x28781,a3)),f8(x28782,a3))),
% 59.45/59.51 inference(scs_inference,[],[693,140,2876,14,15])).
% 59.45/59.51 cnf(2881,plain,
% 59.45/59.51 (P2(f4(a3,a3),f8(x28811,f8(x28812,a3)))),
% 59.45/59.51 inference(scs_inference,[],[693,140,2876,766,823,14,15,21])).
% 59.45/59.51 cnf(2922,plain,
% 59.45/59.51 (P2(f4(a3,a3),f8(a3,x29221))),
% 59.45/59.51 inference(scs_inference,[],[693,825,926,720,1652,14,15,21])).
% 59.45/59.51 cnf(2923,plain,
% 59.45/59.51 (P1(x29231,f8(a3,x29232),f8(a3,x29232))),
% 59.45/59.51 inference(rename_variables,[],[1652])).
% 59.45/59.51 cnf(2924,plain,
% 59.45/59.51 (P1(f4(a3,a3),x29241,f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[720])).
% 59.45/59.51 cnf(2933,plain,
% 59.45/59.51 (P3(f4(a3,a3),f4(a3,a3),f8(a3,x29331))),
% 59.45/59.51 inference(scs_inference,[],[1770,693,651,2065,2878,825,926,720,2924,1237,1652,2923,14,15,21,16,17,23,27])).
% 59.45/59.51 cnf(2990,plain,
% 59.45/59.51 (P2(f4(a3,a3),f4(a3,f8(x29901,a3)))),
% 59.45/59.51 inference(scs_inference,[],[693,975,766,1047,1146,14,15,21])).
% 59.45/59.51 cnf(3016,plain,
% 59.45/59.51 (P3(f8(a1,a2),f8(a1,a2),f4(a6,a6))),
% 59.45/59.51 inference(scs_inference,[],[693,1749,1047,295,1728,15,14,16])).
% 59.45/59.51 cnf(3021,plain,
% 59.45/59.51 (P2(f4(a3,a3),f4(f8(a3,x30211),f8(a3,x30211)))),
% 59.45/59.51 inference(scs_inference,[],[693,1749,720,1047,1319,295,1185,1728,15,14,16,17,21])).
% 59.45/59.51 cnf(3045,plain,
% 59.45/59.51 (P3(f4(a3,a3),f8(x30451,a3),a3)),
% 59.45/59.51 inference(scs_inference,[],[693,720,34,2881,17,14])).
% 59.45/59.51 cnf(3048,plain,
% 59.45/59.51 (P3(f4(a3,a3),f8(a3,x30481),f8(x30482,a3))),
% 59.45/59.51 inference(scs_inference,[],[693,720,34,1619,2881,17,14,15])).
% 59.45/59.51 cnf(3051,plain,
% 59.45/59.51 (P3(f8(a3,x30511),f8(x30512,a3),f8(x30513,a3))),
% 59.45/59.51 inference(scs_inference,[],[693,720,34,1619,2881,2922,17,14,15,16])).
% 59.45/59.51 cnf(3057,plain,
% 59.45/59.51 (~P3(a6,f8(a3,x30571),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1770,693,2065,720,34,1619,2104,2881,2922,17,14,15,16,21,23])).
% 59.45/59.51 cnf(3094,plain,
% 59.45/59.51 (P3(f4(a3,a3),f8(x30941,a3),f8(a3,x30942))),
% 59.45/59.51 inference(scs_inference,[],[693,1619,2990,16,14])).
% 59.45/59.51 cnf(3110,plain,
% 59.45/59.51 (P3(f8(x31101,a3),f8(a3,x31102),a3)),
% 59.45/59.51 inference(scs_inference,[],[398,102,693,1998,2922,3021,16,14,15])).
% 59.45/59.51 cnf(3153,plain,
% 59.45/59.51 (~P3(f4(a3,a3),x31531,a6)+~P3(x31531,a7,f8(x31532,a3))),
% 59.45/59.51 inference(scs_inference,[],[2490,102,693,384,3021,14,15,22])).
% 59.45/59.51 cnf(3348,plain,
% 59.45/59.51 (P1(f4(a3,a3),x33481,f8(a3,x33482))),
% 59.45/59.51 inference(scs_inference,[],[720,2922,17])).
% 59.45/59.51 cnf(3393,plain,
% 59.45/59.51 (P3(f4(a3,a3),f8(a1,a2),f4(a3,a6))),
% 59.45/59.51 inference(scs_inference,[],[1749,682,16])).
% 59.45/59.51 cnf(3491,plain,
% 59.45/59.51 (P3(f8(a3,x34911),f8(a1,a2),f4(a3,a6))),
% 59.45/59.51 inference(scs_inference,[],[1749,1998,16])).
% 59.45/59.51 cnf(3541,plain,
% 59.45/59.51 (P3(f8(x35411,a3),f8(a1,a2),f4(a3,a6))),
% 59.45/59.51 inference(scs_inference,[],[1749,241,16])).
% 59.45/59.51 cnf(3788,plain,
% 59.45/59.51 (P1(x37881,f4(a3,a3),f4(f8(x37882,a3),f4(a3,a3)))),
% 59.45/59.51 inference(rename_variables,[],[1233])).
% 59.45/59.51 cnf(3794,plain,
% 59.45/59.51 (~P3(f8(a3,x37941),x37942,a6)+~P3(x37942,a7,f8(a3,x37941))),
% 59.45/59.51 inference(scs_inference,[],[2490,1202,2004,1233,3788,7,18,21,27,22])).
% 59.45/59.51 cnf(3805,plain,
% 59.45/59.51 (P3(f8(a1,a2),f8(x38051,a3),f4(a3,a6))),
% 59.45/59.51 inference(scs_inference,[],[3541,13])).
% 59.45/59.51 cnf(3807,plain,
% 59.45/59.51 (P2(f8(a3,x38071),f8(a3,x38072))),
% 59.45/59.51 inference(scs_inference,[],[3348,3541,2002,13,21])).
% 59.45/59.51 cnf(3808,plain,
% 59.45/59.51 (P1(x38081,a3,f8(a3,x38082))),
% 59.45/59.51 inference(rename_variables,[],[2002])).
% 59.45/59.51 cnf(3809,plain,
% 59.45/59.51 (P1(f4(a3,a3),x38091,f8(a3,x38092))),
% 59.45/59.51 inference(rename_variables,[],[3348])).
% 59.45/59.51 cnf(3815,plain,
% 59.45/59.51 (~P2(f8(a3,x38151),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[2631,3348,2786,3541,3110,2002,13,21,14,15])).
% 59.45/59.51 cnf(3816,plain,
% 59.45/59.51 (P3(f8(x38161,a3),f8(a3,x38162),a3)),
% 59.45/59.51 inference(rename_variables,[],[3110])).
% 59.45/59.51 cnf(3818,plain,
% 59.45/59.51 (~P2(f8(x38181,a3),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[2631,3348,2786,3541,3110,3816,2750,2002,13,21,14,15,16])).
% 59.45/59.51 cnf(3822,plain,
% 59.45/59.51 (P3(f8(x38221,a3),f8(a3,x38222),f8(a3,x38222))),
% 59.45/59.51 inference(scs_inference,[],[2631,3348,2786,3094,3541,3110,3816,2750,2002,736,13,21,14,15,16,23])).
% 59.45/59.51 cnf(3824,plain,
% 59.45/59.51 (P1(f8(a3,x38241),f8(a3,x38242),f8(a3,x38243))),
% 59.45/59.51 inference(scs_inference,[],[2631,3348,3809,2786,3094,3541,3110,3816,2750,2177,2002,3808,736,13,21,14,15,16,23,24])).
% 59.45/59.51 cnf(3826,plain,
% 59.45/59.51 (P1(x38261,f8(a3,x38262),a3)),
% 59.45/59.51 inference(rename_variables,[],[2177])).
% 59.45/59.51 cnf(3827,plain,
% 59.45/59.51 (P1(f4(a3,a3),x38271,f8(a3,x38272))),
% 59.45/59.51 inference(rename_variables,[],[3348])).
% 59.45/59.51 cnf(3829,plain,
% 59.45/59.51 (P3(f8(a3,x38291),a3,f8(x38292,a3))),
% 59.45/59.51 inference(scs_inference,[],[2631,3348,3809,2786,3094,3541,3110,3816,2750,2118,2177,1627,2002,3808,736,13,21,14,15,16,23,24,22])).
% 59.45/59.51 cnf(3830,plain,
% 59.45/59.51 (P3(a3,a3,f8(a3,x38301))),
% 59.45/59.51 inference(rename_variables,[],[2118])).
% 59.45/59.51 cnf(3832,plain,
% 59.45/59.51 (P3(f8(a3,x38321),f8(a3,x38321),a3)),
% 59.45/59.51 inference(scs_inference,[],[2631,3348,3809,3827,2786,3094,2933,3541,3110,3816,2750,2118,2177,3826,1627,2002,3808,736,13,21,14,15,16,23,24,22,27])).
% 59.45/59.51 cnf(3833,plain,
% 59.45/59.51 (P1(f4(a3,a3),x38331,f8(a3,x38332))),
% 59.45/59.51 inference(rename_variables,[],[3348])).
% 59.45/59.51 cnf(3834,plain,
% 59.45/59.51 (P1(f4(a3,a3),x38341,f8(a3,x38342))),
% 59.45/59.51 inference(rename_variables,[],[3348])).
% 59.45/59.51 cnf(3835,plain,
% 59.45/59.51 (P1(x38351,f8(a3,x38352),a3)),
% 59.45/59.51 inference(rename_variables,[],[2177])).
% 59.45/59.51 cnf(3837,plain,
% 59.45/59.51 (P3(f8(a3,x38371),f8(a3,x38372),f8(a3,x38372))),
% 59.45/59.51 inference(scs_inference,[],[2631,3348,3809,3827,3834,3833,2786,3094,2933,3541,3110,3816,2750,2118,2177,3826,1627,2002,3808,736,13,21,14,15,16,23,24,22,27,26])).
% 59.45/59.51 cnf(3840,plain,
% 59.45/59.51 (P3(f4(a3,a3),f8(x38401,a3),f8(a3,x38402))),
% 59.45/59.51 inference(rename_variables,[],[3094])).
% 59.45/59.51 cnf(3842,plain,
% 59.45/59.51 (P1(f4(a6,a6),f8(a3,x38421),f8(a3,x38422))),
% 59.45/59.51 inference(scs_inference,[],[2631,3348,3809,3827,3834,3833,2786,3094,2933,3541,3110,3816,2750,2118,3830,3016,2177,3826,3835,1627,2002,3808,736,13,21,14,15,16,23,24,22,27,26,28])).
% 59.45/59.51 cnf(3846,plain,
% 59.45/59.51 (~P3(f4(a3,a3),f8(x38461,a3),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[2631,3348,3809,3827,3834,3833,2786,3094,3840,2933,3541,3110,3816,2750,2118,3830,3016,2177,3826,3835,1627,2002,3808,736,13,21,14,15,16,23,24,22,27,26,28,20])).
% 59.45/59.51 cnf(3858,plain,
% 59.45/59.51 (P3(f8(a3,x38581),f8(a3,x38582),f8(a3,x38581))),
% 59.45/59.51 inference(scs_inference,[],[3837,13])).
% 59.45/59.51 cnf(3860,plain,
% 59.45/59.51 (~P3(f8(x38601,a3),f8(a3,x38602),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[3815,3822,3837,13,20])).
% 59.45/59.51 cnf(3861,plain,
% 59.45/59.51 (P3(f8(x38611,a3),f8(a3,x38612),f8(a3,x38612))),
% 59.45/59.51 inference(rename_variables,[],[3822])).
% 59.45/59.51 cnf(3863,plain,
% 59.45/59.51 (~P1(f4(a6,a6),f8(a3,x38631),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[3815,3842,3822,3837,13,20,21])).
% 59.45/59.51 cnf(3869,plain,
% 59.45/59.51 (~P2(f5(a7),a6)),
% 59.45/59.51 inference(scs_inference,[],[9,3815,3842,3822,3837,6,7,13,20,21,14,15])).
% 59.45/59.51 cnf(3872,plain,
% 59.45/59.51 (~P2(f4(a7,a6),f4(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[9,3846,3815,3842,3822,3837,6,2470,7,13,20,21,14,15,16])).
% 59.45/59.51 cnf(3873,plain,
% 59.45/59.51 (~P3(f4(a3,a3),f8(x38731,a3),f4(a7,a6))),
% 59.45/59.51 inference(rename_variables,[],[3846])).
% 59.45/59.51 cnf(3877,plain,
% 59.45/59.51 (P3(f8(a1,a2),f8(x38771,a3),f4(a3,a6))),
% 59.45/59.51 inference(rename_variables,[],[3805])).
% 59.45/59.51 cnf(3881,plain,
% 59.45/59.51 (P1(f4(a6,a6),f8(a3,x38811),f8(a3,x38812))),
% 59.45/59.51 inference(rename_variables,[],[3842])).
% 59.45/59.51 cnf(3884,plain,
% 59.45/59.51 (~P3(f8(a3,a3),a3,f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[9,3805,3846,3873,3815,3842,3822,3861,3837,3824,3832,2618,634,6,2470,7,13,20,21,14,15,16,23,25,22])).
% 59.45/59.51 cnf(3890,plain,
% 59.45/59.51 (P1(x38901,f8(a3,x38902),a3)),
% 59.45/59.51 inference(rename_variables,[],[2177])).
% 59.45/59.51 cnf(3895,plain,
% 59.45/59.51 (P3(f8(x38951,a3),f8(a3,x38952),f8(a3,x38952))),
% 59.45/59.51 inference(rename_variables,[],[3822])).
% 59.45/59.51 cnf(3899,plain,
% 59.45/59.51 (P1(f4(a6,a6),f8(a3,x38991),f8(a3,x38992))),
% 59.45/59.51 inference(rename_variables,[],[3842])).
% 59.45/59.51 cnf(3902,plain,
% 59.45/59.51 (~P3(f8(a3,x39021),f8(a3,x39022),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[9,3805,3877,3846,3873,3815,3842,3881,3899,3822,3861,3895,3837,3824,3832,1510,2618,3348,2177,3890,634,6,2470,345,7,42,13,20,21,14,15,16,23,25,22,27,26,29,28])).
% 59.45/59.51 cnf(3907,plain,
% 59.45/59.51 (P1(x39071,f8(a3,x39072),f8(a3,x39073))),
% 59.45/59.51 inference(scs_inference,[],[9,3805,3877,3846,3873,3815,3842,3881,3899,3822,3861,3895,3837,3807,3824,3832,1510,2618,3348,2177,3890,634,1687,6,2470,345,7,42,13,20,21,14,15,16,23,25,22,27,26,29,28,18])).
% 59.45/59.51 cnf(3909,plain,
% 59.45/59.51 (P2(f8(a3,x39091),f8(a3,x39092))),
% 59.45/59.51 inference(rename_variables,[],[3807])).
% 59.45/59.51 cnf(3911,plain,
% 59.45/59.51 (P1(f8(a3,x39111),x39112,f8(a3,x39113))),
% 59.45/59.51 inference(scs_inference,[],[9,3805,3877,3846,3873,3815,3842,3881,3899,3822,3861,3895,3837,3807,3909,3824,3832,1510,2618,3348,2177,3890,634,1690,1687,6,2470,345,7,42,13,20,21,14,15,16,23,25,22,27,26,29,28,18,19])).
% 59.45/59.51 cnf(3919,plain,
% 59.45/59.51 (P3(f8(a1,a2),f8(a3,x39191),f4(a3,a6))),
% 59.45/59.51 inference(scs_inference,[],[3491,13])).
% 59.45/59.51 cnf(3921,plain,
% 59.45/59.51 (~P3(f4(a7,a6),a3,f4(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[3872,3491,4,13,20])).
% 59.45/59.51 cnf(3922,plain,
% 59.45/59.51 (P3(x39221,a3,x39221)),
% 59.45/59.51 inference(rename_variables,[],[4])).
% 59.45/59.51 cnf(3924,plain,
% 59.45/59.51 (~P1(f8(a3,x39241),x39242,f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[3872,3818,3911,3491,4,13,20,21])).
% 59.45/59.51 cnf(3925,plain,
% 59.45/59.51 (P1(f8(a3,x39251),x39252,f8(a3,x39253))),
% 59.45/59.51 inference(rename_variables,[],[3911])).
% 59.45/59.51 cnf(3928,plain,
% 59.45/59.51 (~P2(a3,f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[3872,3818,3911,3491,3045,3846,4,13,20,21,14])).
% 59.45/59.51 cnf(3929,plain,
% 59.45/59.51 (P3(f4(a3,a3),f8(x39291,a3),a3)),
% 59.45/59.51 inference(rename_variables,[],[3045])).
% 59.45/59.51 cnf(3931,plain,
% 59.45/59.51 (~P2(f4(a3,a3),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[3872,3818,3911,3491,3045,3846,2786,2645,4,13,20,21,14,15])).
% 59.45/59.51 cnf(3935,plain,
% 59.45/59.51 (~P2(f4(a7,a6),f8(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[3872,3818,3911,3884,3491,3045,3846,2786,2645,4,3922,13,20,21,14,15,16])).
% 59.45/59.51 cnf(3936,plain,
% 59.45/59.51 (P3(x39361,a3,x39361)),
% 59.45/59.51 inference(rename_variables,[],[4])).
% 59.45/59.51 cnf(3938,plain,
% 59.45/59.51 (~P3(a7,a6,f4(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[9,3872,3818,3911,3884,3491,3045,3929,3846,2786,2645,4,3922,2470,13,20,21,14,15,16,23])).
% 59.45/59.51 cnf(3942,plain,
% 59.45/59.51 (~P3(a7,f4(a3,a6),a3)),
% 59.45/59.51 inference(scs_inference,[],[9,3872,3818,3911,3884,3491,3045,3929,3846,2786,2645,4,3922,3936,2470,7,13,20,21,14,15,16,23,22])).
% 59.45/59.51 cnf(3946,plain,
% 59.45/59.51 (~P1(f8(a3,x39461),f8(a3,x39462),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[9,3872,3818,3911,3858,3884,3491,3045,3929,3846,2786,618,2645,746,2177,4,3922,3936,2470,7,13,20,21,14,15,16,23,22,27])).
% 59.45/59.51 cnf(3947,plain,
% 59.45/59.51 (P3(f8(a3,x39471),f8(a3,x39472),f8(a3,x39471))),
% 59.45/59.51 inference(rename_variables,[],[3858])).
% 59.45/59.51 cnf(3952,plain,
% 59.45/59.51 (P3(f8(a3,x39521),f8(a3,x39522),f8(a3,x39521))),
% 59.45/59.51 inference(rename_variables,[],[3858])).
% 59.45/59.51 cnf(3956,plain,
% 59.45/59.51 (~P3(f8(a3,x39561),f8(a3,x39561),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[9,3872,3818,3911,3925,3858,3947,3952,3884,3491,3045,3929,3846,3907,2786,618,2645,764,746,2177,4,3922,3936,2470,7,13,20,21,14,15,16,23,22,27,26,29])).
% 59.45/59.51 cnf(3959,plain,
% 59.45/59.51 (P1(f8(a3,x39591),x39592,f8(a3,x39593))),
% 59.45/59.51 inference(rename_variables,[],[3911])).
% 59.45/59.51 cnf(3961,plain,
% 59.45/59.51 (~P3(f8(x39611,a3),f8(x39611,a3),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[9,3872,3863,3818,3911,3925,3858,3947,3952,3884,3491,3045,3929,3846,3907,2786,618,2645,1684,3016,764,746,2177,4,3922,3936,2470,7,13,20,21,14,15,16,23,22,27,26,29,28])).
% 59.45/59.51 cnf(3964,plain,
% 59.45/59.51 (~P2(f8(a3,x39641),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[9,3872,3863,3818,3911,3925,3959,3858,3947,3952,3884,3491,3045,3929,3846,3907,2786,618,2645,1684,3016,764,746,2177,4,3922,3936,2470,7,13,20,21,14,15,16,23,22,27,26,29,28,17])).
% 59.45/59.51 cnf(3970,plain,
% 59.45/59.51 (P3(f8(a3,x39701),f8(x39702,a3),a3)),
% 59.45/59.51 inference(scs_inference,[],[3110,13])).
% 59.45/59.51 cnf(3972,plain,
% 59.45/59.51 (~P3(f8(a3,x39721),a3,f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3964,3829,3110,13,20])).
% 59.45/59.51 cnf(3973,plain,
% 59.45/59.51 (P3(f8(a3,x39731),a3,f8(x39732,a3))),
% 59.45/59.51 inference(rename_variables,[],[3829])).
% 59.45/59.51 cnf(3976,plain,
% 59.45/59.51 (~P1(f8(x39761,a3),x39762,f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[3931,3964,3829,3110,746,13,20,21])).
% 59.45/59.51 cnf(3978,plain,
% 59.45/59.51 (~P2(f8(x39781,a3),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3931,3956,3964,3829,3051,3110,746,13,20,21,14])).
% 59.45/59.51 cnf(3979,plain,
% 59.45/59.51 (~P3(f8(a3,x39791),f8(a3,x39791),f4(a6,a7))),
% 59.45/59.51 inference(rename_variables,[],[3956])).
% 59.45/59.51 cnf(3982,plain,
% 59.45/59.51 (~P2(f5(a7),f4(a3,a6))),
% 59.45/59.51 inference(scs_inference,[],[3931,3942,3956,3964,3829,3051,3110,746,6,13,20,21,14,15])).
% 59.45/59.51 cnf(3985,plain,
% 59.45/59.51 (~P2(f4(a6,a7),f8(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[3931,3942,3956,3979,3964,3829,3051,3110,746,6,2470,13,20,21,14,15,16])).
% 59.45/59.51 cnf(3986,plain,
% 59.45/59.51 (~P3(f8(a3,x39861),f8(a3,x39861),f4(a6,a7))),
% 59.45/59.51 inference(rename_variables,[],[3956])).
% 59.45/59.51 cnf(3991,plain,
% 59.45/59.51 (P3(f8(a3,x39911),a3,f8(x39912,a3))),
% 59.45/59.51 inference(rename_variables,[],[3829])).
% 59.45/59.51 cnf(3994,plain,
% 59.45/59.51 (~P3(f8(x39941,a3),f8(x39942,a3),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3931,3942,3956,3979,3986,3964,3829,3973,3048,3051,1896,3832,3110,2786,746,6,2470,13,20,21,14,15,16,23,22])).
% 59.45/59.51 cnf(3998,plain,
% 59.45/59.51 (~P1(f4(a3,a6),f8(a3,x39981),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3931,3942,3919,3956,3979,3986,3964,3829,3973,3048,3051,1896,3911,3832,3110,3907,2786,746,6,2470,13,20,21,14,15,16,23,22,27])).
% 59.45/59.51 cnf(3999,plain,
% 59.45/59.51 (P3(f8(a1,a2),f8(a3,x39991),f4(a3,a6))),
% 59.45/59.51 inference(rename_variables,[],[3919])).
% 59.45/59.51 cnf(4000,plain,
% 59.45/59.51 (P1(f8(a3,x40001),x40002,f8(a3,x40003))),
% 59.45/59.51 inference(rename_variables,[],[3911])).
% 59.45/59.51 cnf(4001,plain,
% 59.45/59.51 (P1(x40011,f8(a3,x40012),f8(a3,x40013))),
% 59.45/59.51 inference(rename_variables,[],[3907])).
% 59.45/59.51 cnf(4004,plain,
% 59.45/59.51 (P1(f8(a3,x40041),x40042,f8(a3,x40043))),
% 59.45/59.51 inference(rename_variables,[],[3911])).
% 59.45/59.51 cnf(4008,plain,
% 59.45/59.51 (~P3(f8(a3,x40081),f8(a3,x40082),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3931,3942,3919,3999,3956,3979,3986,3964,3946,3829,3973,3991,3048,3051,1896,3911,4000,4004,3832,3110,3907,4001,2786,1711,746,6,2470,13,20,21,14,15,16,23,22,27,26,28])).
% 59.45/59.51 cnf(4011,plain,
% 59.45/59.51 (P1(x40111,f8(a3,x40112),f8(a3,x40113))),
% 59.45/59.51 inference(rename_variables,[],[3907])).
% 59.45/59.51 cnf(4012,plain,
% 59.45/59.51 (P1(f8(a3,x40121),x40122,f8(a3,x40123))),
% 59.45/59.51 inference(rename_variables,[],[3911])).
% 59.45/59.51 cnf(4014,plain,
% 59.45/59.51 (~P1(x40141,f8(a3,x40142),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[3931,3942,3919,3999,3924,3956,3979,3986,3964,3946,3829,3973,3991,3048,3051,1896,3911,4000,4004,4012,3832,3110,3907,4001,4011,2786,1711,746,6,2470,13,20,21,14,15,16,23,22,27,26,28,24])).
% 59.45/59.51 cnf(4021,plain,
% 59.45/59.51 (P3(f4(a3,a3),f8(a3,x40211),a3)),
% 59.45/59.51 inference(scs_inference,[],[2645,13])).
% 59.45/59.51 cnf(4026,plain,
% 59.45/59.51 (~P1(f4(a3,a3),x40261,f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3935,3978,3348,2645,4,13,20,21])).
% 59.45/59.51 cnf(4027,plain,
% 59.45/59.51 (P1(f4(a3,a3),x40271,f8(a3,x40272))),
% 59.45/59.51 inference(rename_variables,[],[3348])).
% 59.45/59.51 cnf(4033,plain,
% 59.45/59.51 (P3(x40331,f8(x40332,a3),x40331)),
% 59.45/59.51 inference(rename_variables,[],[2470])).
% 59.45/59.51 cnf(4036,plain,
% 59.45/59.51 (P3(f8(a3,x40361),a3,f8(x40362,a3))),
% 59.45/59.51 inference(rename_variables,[],[3829])).
% 59.45/59.51 cnf(4037,plain,
% 59.45/59.51 (~P3(f8(x40371,a3),f8(x40371,a3),f4(a7,a6))),
% 59.45/59.51 inference(rename_variables,[],[3961])).
% 59.45/59.51 cnf(4040,plain,
% 59.45/59.51 (P1(x40401,f8(a3,x40402),f4(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[3935,3961,3978,3829,1869,3348,2118,2645,2002,948,2065,4,2470,720,13,20,21,14,16,23,25])).
% 59.45/59.51 cnf(4050,plain,
% 59.45/59.51 (P1(f8(a3,x40501),x40502,f8(a3,x40503))),
% 59.45/59.51 inference(rename_variables,[],[3911])).
% 59.45/59.51 cnf(4051,plain,
% 59.45/59.51 (~P3(f8(x40511,a3),f8(x40511,a3),f4(a7,a6))),
% 59.45/59.51 inference(rename_variables,[],[3961])).
% 59.45/59.51 cnf(4052,plain,
% 59.45/59.51 (P3(f8(a3,x40521),f8(x40522,a3),a3)),
% 59.45/59.51 inference(rename_variables,[],[3970])).
% 59.45/59.51 cnf(4060,plain,
% 59.45/59.51 (~P2(f5(a6),a7)),
% 59.45/59.51 inference(scs_inference,[],[3935,3961,4037,4051,3978,3921,3970,4052,3829,4036,1869,30,3911,3348,4027,2118,2645,2002,948,2065,4,6,2470,4033,720,13,20,21,14,16,23,25,22,27,26,15])).
% 59.45/59.51 cnf(4064,plain,
% 59.45/59.51 (P1(f8(a3,x40641),x40642,f8(a3,x40643))),
% 59.45/59.51 inference(rename_variables,[],[3911])).
% 59.45/59.51 cnf(4066,plain,
% 59.45/59.51 (~P3(f8(a3,x40661),f8(x40662,a3),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[3935,3976,3998,3961,4037,4051,3978,3921,3970,4052,3829,4036,1869,30,1896,3911,4050,4064,3348,4027,855,2118,2645,2002,948,2065,4,6,2470,4033,720,13,20,21,14,16,23,25,22,27,26,15,24,28])).
% 59.45/59.51 cnf(4072,plain,
% 59.45/59.51 (P3(f4(a3,a3),a3,f8(a3,x40721))),
% 59.45/59.51 inference(scs_inference,[],[1625,13])).
% 59.45/59.51 cnf(4076,plain,
% 59.45/59.51 (~P1(x40761,f8(a3,x40762),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3985,3928,4021,1625,1684,13,20,21])).
% 59.45/59.51 cnf(4077,plain,
% 59.45/59.51 (P1(x40771,f8(a3,x40772),f8(x40773,a3))),
% 59.45/59.51 inference(rename_variables,[],[1684])).
% 59.45/59.51 cnf(4079,plain,
% 59.45/59.51 (~P2(a3,f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3985,3928,3994,4021,3970,1625,1684,13,20,21,14])).
% 59.45/59.51 cnf(4081,plain,
% 59.45/59.51 (P3(f8(a3,x40811),f8(x40812,a3),a3)),
% 59.45/59.51 inference(rename_variables,[],[3970])).
% 59.45/59.51 cnf(4083,plain,
% 59.45/59.51 (~P2(f4(a3,a3),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3985,4026,3928,4040,3994,4021,3970,1625,1684,13,20,21,14,17])).
% 59.45/59.51 cnf(4084,plain,
% 59.45/59.51 (P1(x40841,f8(a3,x40842),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[4040])).
% 59.45/59.51 cnf(4085,plain,
% 59.45/59.51 (~P1(f4(a3,a3),x40851,f4(a6,a7))),
% 59.45/59.51 inference(rename_variables,[],[4026])).
% 59.45/59.51 cnf(4091,plain,
% 59.45/59.51 (~P3(a7,f8(a1,a2),f8(x40911,a3))),
% 59.45/59.51 inference(scs_inference,[],[3938,3985,4026,3928,4040,3902,3994,4021,3970,1625,1684,736,2065,2470,13,20,21,14,17,16,23])).
% 59.45/59.51 cnf(4093,plain,
% 59.45/59.51 (~P1(x40931,f8(x40932,a3),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3938,3985,4026,4085,3928,4040,4084,3902,3994,4021,3970,1625,1684,4077,736,2065,2470,13,20,21,14,17,16,23,24])).
% 59.45/59.51 cnf(4094,plain,
% 59.45/59.51 (P1(x40941,f8(a3,x40942),f8(x40943,a3))),
% 59.45/59.51 inference(rename_variables,[],[1684])).
% 59.45/59.51 cnf(4095,plain,
% 59.45/59.51 (~P1(f4(a3,a3),x40951,f4(a6,a7))),
% 59.45/59.51 inference(rename_variables,[],[4026])).
% 59.45/59.51 cnf(4098,plain,
% 59.45/59.51 (P1(x40981,f4(a3,a3),f8(x40982,a3))),
% 59.45/59.51 inference(rename_variables,[],[1116])).
% 59.45/59.51 cnf(4099,plain,
% 59.45/59.51 (~P1(f4(a3,a3),x40991,f4(a6,a7))),
% 59.45/59.51 inference(rename_variables,[],[4026])).
% 59.45/59.51 cnf(4101,plain,
% 59.45/59.51 (~P3(a7,f4(a3,a6),f4(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[3938,3985,4026,4085,4095,3928,4040,4084,3902,3994,4021,3970,1625,1684,4077,736,1116,2065,4,2470,7,13,20,21,14,17,16,23,24,25,22])).
% 59.45/59.51 cnf(4102,plain,
% 59.45/59.51 (P3(x41021,a3,x41021)),
% 59.45/59.51 inference(rename_variables,[],[4])).
% 59.45/59.51 cnf(4105,plain,
% 59.45/59.51 (~P1(a6,f4(a3,a3),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[3938,3985,4026,4085,4095,3928,4040,4084,3860,3902,3994,4021,3970,1625,1684,4077,736,1116,4098,2004,2065,4,4102,2470,7,13,20,21,14,17,16,23,24,25,22,27])).
% 59.45/59.51 cnf(4107,plain,
% 59.45/59.51 (~P3(f8(x41071,a3),f8(a3,x41072),f4(a7,a6))),
% 59.45/59.51 inference(rename_variables,[],[3860])).
% 59.45/59.51 cnf(4111,plain,
% 59.45/59.51 (~P1(x41111,a3,f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[3938,3985,4026,4085,4095,3928,4040,4084,3860,4107,3902,3994,4021,3970,4081,1625,1684,4077,4094,736,1116,4098,2004,2065,4,4102,2470,7,13,20,21,14,17,16,23,24,25,22,27,26])).
% 59.45/59.51 cnf(4115,plain,
% 59.45/59.51 (P1(x41151,f8(a3,x41152),f8(x41153,a3))),
% 59.45/59.51 inference(rename_variables,[],[1684])).
% 59.45/59.51 cnf(4117,plain,
% 59.45/59.51 (~P3(f8(a3,x41171),f4(a3,a3),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3938,3985,4026,4085,4095,4099,3928,4040,4084,3860,4107,3902,3994,4021,3970,4081,1625,1684,4077,4094,736,3348,1116,4098,2004,2065,4,4102,2470,7,13,20,21,14,17,16,23,24,25,22,27,26,29])).
% 59.45/59.51 cnf(4119,plain,
% 59.45/59.51 (P1(x41191,f8(a3,x41192),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[4040])).
% 59.45/59.51 cnf(4121,plain,
% 59.45/59.51 (~P1(f4(a3,a3),x41211,f4(a6,a7))),
% 59.45/59.51 inference(rename_variables,[],[4026])).
% 59.45/59.51 cnf(4123,plain,
% 59.45/59.51 (~P3(f4(a3,a3),f8(x41231,a3),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[3938,3985,4026,4085,4095,4099,4121,3928,4040,4084,4119,3860,4107,3902,3994,4021,3970,4081,1625,1684,4077,4094,4115,736,3348,1116,4098,2004,2065,4,4102,2470,7,13,20,21,14,17,16,23,24,25,22,27,26,29,28])).
% 59.45/59.51 cnf(4128,plain,
% 59.45/59.51 (P3(f8(a1,a2),f4(a3,a3),f4(a3,a6))),
% 59.45/59.51 inference(scs_inference,[],[3393,13])).
% 59.45/59.51 cnf(4135,plain,
% 59.45/59.51 (~P1(f4(a3,a3),x41351,f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[4117,3818,132,3393,855,1746,42,13,16,14,21])).
% 59.45/59.51 cnf(4136,plain,
% 59.45/59.51 (P1(f4(a3,a3),x41361,f8(x41362,a3))),
% 59.45/59.51 inference(rename_variables,[],[855])).
% 59.45/59.51 cnf(4143,plain,
% 59.45/59.51 (P1(x41431,f8(a3,x41432),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[4040])).
% 59.45/59.51 cnf(4150,plain,
% 59.45/59.51 (P3(f8(a3,a3),f8(x41501,a3),f8(a3,x41502))),
% 59.45/59.51 inference(scs_inference,[],[4076,4117,3982,4008,4072,4040,3818,3822,3048,132,3829,3907,3393,855,634,4,1746,42,13,16,14,21,20,24,22,23])).
% 59.45/59.51 cnf(4151,plain,
% 59.45/59.51 (P3(f8(x41511,a3),f8(x41511,a3),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[634])).
% 59.45/59.51 cnf(4163,plain,
% 59.45/59.51 (~P3(f4(a3,a3),f4(a3,a3),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[4105,4076,4117,3982,4008,4072,4040,4143,3818,3822,3048,640,132,3829,3907,3393,855,4136,634,4151,2177,746,1116,2065,4,1746,42,13,16,14,21,20,24,22,23,28,26,29])).
% 59.45/59.51 cnf(4179,plain,
% 59.45/59.51 (~P2(f4(a6,a7),f4(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[4123,4150,2470,13,16])).
% 59.45/59.51 cnf(4188,plain,
% 59.45/59.51 (~P3(f4(a3,a3),f4(a3,a3),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[1,3869,4079,4123,4150,1128,30,2470,7,13,16,14,21,20])).
% 59.45/59.51 cnf(4190,plain,
% 59.45/59.51 (P1(a1,f4(a3,a3),f8(a3,x41901))),
% 59.45/59.51 inference(scs_inference,[],[1,3869,4079,4123,4150,1128,30,2002,948,2470,7,13,16,14,21,20,25])).
% 59.45/59.51 cnf(4196,plain,
% 59.45/59.51 (~P1(a1,f4(a3,a3),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[1,4163,3869,4079,4123,4150,4014,1128,4040,30,648,2002,948,2470,7,13,16,14,21,20,25,22,24])).
% 59.45/59.51 cnf(4198,plain,
% 59.45/59.51 (P1(x41981,f8(a3,x41982),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[4040])).
% 59.45/59.51 cnf(4201,plain,
% 59.45/59.51 (P3(f8(a1,a2),f8(x42011,a3),f4(a3,a6))),
% 59.45/59.51 inference(rename_variables,[],[3805])).
% 59.45/59.51 cnf(4206,plain,
% 59.45/59.51 (P1(x42061,f8(a3,x42062),f4(a3,a3))),
% 59.45/59.51 inference(rename_variables,[],[4040])).
% 59.45/59.51 cnf(4207,plain,
% 59.45/59.51 (P1(f8(x42071,a3),x42072,f8(a3,x42073))),
% 59.45/59.51 inference(rename_variables,[],[1690])).
% 59.45/59.51 cnf(4214,plain,
% 59.45/59.51 (~P1(f8(x42141,a3),x42142,f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[1,4128,4163,3869,4079,4123,4150,3972,4093,4014,4117,1128,3805,4201,1901,1629,4040,4198,4206,3970,30,648,1690,4207,2002,1684,764,948,2470,7,13,16,14,21,20,25,22,24,23,26,28,27])).
% 59.45/59.51 cnf(4227,plain,
% 59.45/59.51 (P3(f4(a3,a3),f8(a1,a2),a6)),
% 59.45/59.51 inference(scs_inference,[],[2065,13])).
% 59.45/59.51 cnf(4233,plain,
% 59.45/59.51 (P3(x42331,a3,x42331)),
% 59.45/59.51 inference(rename_variables,[],[4])).
% 59.45/59.51 cnf(4235,plain,
% 59.45/59.51 (~P1(a3,a2,f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[1,4179,4214,3964,2002,2065,4,206,13,21,20,25])).
% 59.45/59.51 cnf(4241,plain,
% 59.45/59.51 (~P1(x42411,f8(x42412,a3),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[1,4179,4188,4214,4135,3964,2933,4040,736,1711,2002,2065,4,206,13,21,20,25,22,24])).
% 59.45/59.51 cnf(4245,plain,
% 59.45/59.51 (P3(x42451,a3,x42451)),
% 59.45/59.51 inference(rename_variables,[],[4])).
% 59.45/59.51 cnf(4246,plain,
% 59.45/59.51 (P3(x42461,x42462,f4(x42461,x42462))),
% 59.45/59.51 inference(rename_variables,[],[7])).
% 59.45/59.51 cnf(4253,plain,
% 59.45/59.51 (P1(a1,f4(a3,a3),f8(a3,x42531))),
% 59.45/59.51 inference(rename_variables,[],[4190])).
% 59.45/59.51 cnf(4264,plain,
% 59.45/59.51 (~P3(f8(a1,a2),a7,f4(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[1,4179,4188,4196,4214,4066,4190,4253,4135,4111,3964,2933,3045,4040,736,1711,2002,946,2065,4,4233,4245,206,7,4246,13,21,20,25,22,24,23,28,27,29,3153,2790])).
% 59.45/59.51 cnf(4277,plain,
% 59.45/59.51 (P3(a3,x42771,x42771)),
% 59.45/59.51 inference(scs_inference,[],[4,13])).
% 59.45/59.51 cnf(4279,plain,
% 59.45/59.51 (~P2(f5(a7),f8(a1,a2))),
% 59.45/59.51 inference(scs_inference,[],[1916,4,13,15])).
% 59.45/59.51 cnf(4282,plain,
% 59.45/59.51 (P3(x42821,x42822,f4(x42821,x42822))),
% 59.45/59.51 inference(rename_variables,[],[7])).
% 59.45/59.51 cnf(4286,plain,
% 59.45/59.51 (~P3(a3,f8(a3,x42861),f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[4060,3978,1916,1627,94,4,7,5,13,15,14,21,20])).
% 59.45/59.51 cnf(4294,plain,
% 59.45/59.51 (P3(f8(a3,a3),f4(a3,a6),a6)),
% 59.45/59.51 inference(scs_inference,[],[1,4227,4235,4060,2031,3978,4128,1916,3491,1627,634,94,4,3,7,5,13,15,14,21,20,22,24,23])).
% 59.45/59.51 cnf(4307,plain,
% 59.45/59.51 (P1(a1,f8(a1,a2),f8(a1,a6))),
% 59.45/59.51 inference(scs_inference,[],[1,4227,4235,4241,4060,4101,2031,3978,4128,1916,3491,4190,1627,634,1687,2177,94,4,6,2470,766,8,3,1746,7,5,13,15,14,21,20,22,24,23,28,27,29])).
% 59.45/59.51 cnf(4312,plain,
% 59.45/59.51 (~P3(f4(a3,a6),a7,f8(a3,a3))),
% 59.45/59.51 inference(scs_inference,[],[1,4227,4235,4241,4060,4101,2031,3978,4128,1916,3491,4190,1627,634,1687,2177,94,4,6,2470,766,8,3,1746,7,5,13,15,14,21,20,22,24,23,28,27,29,3794])).
% 59.45/59.51 cnf(4314,plain,
% 59.45/59.51 (~P2(a7,f5(a6))),
% 59.45/59.51 inference(scs_inference,[],[1,4227,4235,4241,4060,4101,2031,3978,4128,1916,3491,4190,1627,634,1687,2177,94,4,6,2470,766,8,3,1746,7,5,13,15,14,21,20,22,24,23,28,27,29,3794,17])).
% 59.45/59.51 cnf(4318,plain,
% 59.45/59.51 (~P1(a1,f4(a2,a3),f5(a7))),
% 59.45/59.51 inference(scs_inference,[],[1,4227,4235,4241,4060,4101,3057,2031,3978,4128,1916,3491,4190,1627,634,1687,2177,2002,94,4,6,2470,766,8,3,1746,7,4282,5,13,15,14,21,20,22,24,23,28,27,29,3794,17,25,26])).
% 59.45/59.51 cnf(4329,plain,
% 59.45/59.51 (P3(a3,x43291,x43291)),
% 59.45/59.51 inference(rename_variables,[],[4277])).
% 59.45/59.51 cnf(4334,plain,
% 59.45/59.51 (~P3(f4(a6,a7),a3,f8(a3,x43341))),
% 59.45/59.51 inference(scs_inference,[],[4277,4329,4083,4294,4091,4286,3815,4227,1116,4,42,13,21,20,22,23])).
% 59.45/59.51 cnf(4335,plain,
% 59.45/59.51 (P3(a3,x43351,x43351)),
% 59.45/59.51 inference(rename_variables,[],[4277])).
% 59.45/59.51 cnf(4338,plain,
% 59.45/59.51 (~P1(a3,x43381,f4(a6,a7))),
% 59.45/59.51 inference(scs_inference,[],[4277,4329,4335,4083,4294,4091,4286,3815,4227,1645,1116,4,3,42,13,21,20,22,23,26])).
% 59.45/59.51 cnf(4343,plain,
% 59.45/59.51 (~P1(f5(a1),a2,a7)),
% 59.45/59.51 inference(scs_inference,[],[4277,4329,4335,4083,4264,4294,4091,4286,3815,4227,1645,1116,4,6,766,8,3,42,13,21,20,22,23,26,27])).
% 59.45/59.51 cnf(4353,plain,
% 59.45/59.51 (P3(f5(x43531),x43531,a3)),
% 59.45/59.51 inference(scs_inference,[],[6,13])).
% 59.45/59.51 cnf(4355,plain,
% 59.45/59.51 (~P2(f5(a3),f4(a7,a6))),
% 59.45/59.51 inference(scs_inference,[],[1506,6,13,16])).
% 59.45/59.51 cnf(4390,plain,
% 59.45/59.52 (P3(f8(x43901,a3),x43902,x43902)),
% 59.45/59.52 inference(scs_inference,[],[2470,13])).
% 59.45/59.52 cnf(4392,plain,
% 59.45/59.52 (~P3(a3,f5(a3),f4(a7,a6))),
% 59.45/59.52 inference(scs_inference,[],[4355,4277,2470,13,20])).
% 59.45/59.52 cnf(4393,plain,
% 59.45/59.52 (P3(a3,x43931,x43931)),
% 59.45/59.52 inference(rename_variables,[],[4277])).
% 59.45/59.52 cnf(4395,plain,
% 59.45/59.52 (P3(f5(x43951),x43951,f8(a3,x43952))),
% 59.45/59.52 inference(scs_inference,[],[4355,4353,4277,4393,2118,2470,13,20,22])).
% 59.45/59.52 cnf(4396,plain,
% 59.45/59.52 (P3(a3,x43961,x43961)),
% 59.45/59.52 inference(rename_variables,[],[4277])).
% 59.45/59.52 cnf(4398,plain,
% 59.45/59.52 (~P3(f5(x43981),x43981,f4(a7,a6))),
% 59.45/59.52 inference(scs_inference,[],[4355,4353,4277,4393,4396,1510,2118,2470,13,20,22,23])).
% 59.45/59.52 cnf(4401,plain,
% 59.45/59.52 (~P3(f8(x44011,a3),f5(a6),a7)),
% 59.45/59.52 inference(scs_inference,[],[4355,4353,4277,4393,4396,1510,2118,2470,13,20,22,23,1484])).
% 59.45/59.52 cnf(4405,plain,
% 59.45/59.52 (P3(f8(a1,a6),f8(a3,x44051),f8(a1,a6))),
% 59.45/59.52 inference(scs_inference,[],[1,4355,4353,4318,4307,4277,4393,4396,1510,2118,1645,4,2470,13,20,22,23,1484,25,27])).
% 59.45/59.52 cnf(4412,plain,
% 59.45/59.52 (P3(f5(x44121),x44121,f8(a3,x44122))),
% 59.45/59.52 inference(rename_variables,[],[4395])).
% 59.45/59.52 cnf(4415,plain,
% 59.45/59.52 (P3(f5(x44151),x44151,f8(a3,x44152))),
% 59.45/59.52 inference(rename_variables,[],[4395])).
% 59.45/59.52 cnf(4417,plain,
% 59.45/59.52 (P3(x44171,f5(x44171),f8(a3,x44172))),
% 59.45/59.52 inference(scs_inference,[],[4395,4412,4415,2777,3794,13])).
% 59.45/59.52 cnf(4424,plain,
% 59.45/59.52 (P3(a3,x44241,x44241)),
% 59.45/59.52 inference(rename_variables,[],[4277])).
% 59.45/59.52 cnf(4426,plain,
% 59.45/59.52 (~P3(f8(x44261,a3),f5(a7),f8(a1,a2))),
% 59.45/59.52 inference(scs_inference,[],[4279,4392,4390,4395,4412,4415,4334,4277,2777,3794,13,16,15,20])).
% 59.45/59.52 cnf(4427,plain,
% 59.45/59.52 (P3(f8(x44271,a3),x44272,x44272)),
% 59.45/59.52 inference(rename_variables,[],[4390])).
% 59.45/59.52 cnf(4434,plain,
% 59.45/59.52 (P3(f8(x44341,a3),x44342,x44342)),
% 59.45/59.52 inference(rename_variables,[],[4390])).
% 59.45/59.52 cnf(4437,plain,
% 59.45/59.52 (~P3(a3,a3,f4(a6,a7))),
% 59.45/59.52 inference(scs_inference,[],[4398,4279,4392,4390,4427,4434,4395,4412,4415,4401,4334,4338,4277,4424,4072,3,42,2777,3794,13,16,15,20,22,23,29])).
% 59.45/59.52 cnf(4453,plain,
% 59.45/59.52 (P3(f8(x44531,a3),x44532,x44532)),
% 59.45/59.52 inference(rename_variables,[],[4390])).
% 59.45/59.52 cnf(4458,plain,
% 59.45/59.52 (P3(f8(x44581,a3),x44582,x44582)),
% 59.45/59.52 inference(rename_variables,[],[4390])).
% 59.45/59.52 cnf(4462,plain,
% 59.45/59.52 (P3(x44621,f5(x44621),f8(a3,x44622))),
% 59.45/59.52 inference(rename_variables,[],[4417])).
% 59.45/59.52 cnf(4466,plain,
% 59.45/59.52 (P3(f8(x44661,a3),x44662,x44662)),
% 59.45/59.52 inference(rename_variables,[],[4390])).
% 59.45/59.52 cnf(4467,plain,
% 59.45/59.52 (P3(x44671,f5(x44671),f8(a3,x44672))),
% 59.45/59.52 inference(rename_variables,[],[4417])).
% 59.45/59.52 cnf(4471,plain,
% 59.45/59.52 (P1(x44711,f8(a3,x44712),f8(a3,x44713))),
% 59.45/59.52 inference(rename_variables,[],[3907])).
% 59.45/59.52 cnf(4473,plain,
% 59.45/59.52 (~P3(f8(a3,x44731),a6,f4(a3,a6))),
% 59.45/59.52 inference(scs_inference,[],[1,4314,4417,4462,4467,4426,4437,4312,4405,4390,4453,4458,4466,4395,3907,4471,5,3794,13,20,22,23,26,29])).
% 59.45/59.52 cnf(4474,plain,
% 59.45/59.52 (P3(f8(x44741,a3),x44742,x44742)),
% 59.45/59.52 inference(rename_variables,[],[4390])).
% 59.45/59.52 cnf(4478,plain,
% 59.45/59.52 (P3(f8(x44781,a3),x44782,x44782)),
% 59.45/59.52 inference(rename_variables,[],[4390])).
% 59.45/59.52 cnf(4485,plain,
% 59.45/59.52 (~P3(a6,a6,x44851)+P1(f4(a1,a1),a2,x44851)),
% 59.45/59.52 inference(scs_inference,[],[1,4314,4417,4462,4467,4426,4437,4312,4343,4405,4390,4453,4458,4466,4474,4478,4395,3907,4471,7,5,3794,13,20,22,23,26,29,15,25,14,28])).
% 59.45/59.52 cnf(4489,plain,
% 59.45/59.52 (P3(x44891,x44892,f4(x44891,x44892))),
% 59.45/59.52 inference(rename_variables,[],[7])).
% 59.45/59.52 cnf(4493,plain,
% 59.45/59.52 ($false),
% 59.45/59.52 inference(scs_inference,[],[4473,1998,1749,7,4489,4485,13,16]),
% 59.45/59.52 ['proof']).
% 59.45/59.52 % SZS output end Proof
% 59.45/59.52 % Total time :58.840000s
%------------------------------------------------------------------------------