%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG005-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 : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:00:35 EDT 2024
% Result : Unsatisfiable 60.10s 60.39s
% Output : CNFRefutation 60.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.09 % Problem : RNG005-2 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.07/0.28 % Computer : n032.cluster.edu
% 0.07/0.28 % Model : x86_64 x86_64
% 0.07/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.28 % Memory : 8042.1875MB
% 0.07/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.28 % CPULimit : 300
% 0.07/0.28 % WCLimit : 300
% 0.07/0.28 % DateTime : Tue Jun 18 14:27:38 EDT 2024
% 0.07/0.28 % CPUTime :
% 0.12/0.45 start to proof:theBenchmark
% 60.10/60.38 %-------------------------------------------
% 60.10/60.38 % File :CSE---1.7
% 60.10/60.38 % Problem :theBenchmark
% 60.10/60.38 % Transform :cnf
% 60.10/60.38 % Format :tptp:raw
% 60.10/60.38 % Command :java -jar mcs_scs.jar %d %s
% 60.10/60.38
% 60.10/60.38 % Result :Theorem 59.730000s
% 60.10/60.38 % Output :CNFRefutation 59.730000s
% 60.10/60.38 %-------------------------------------------
% 60.10/60.39 %--------------------------------------------------------------------------
% 60.10/60.39 % File : RNG005-2 : TPTP v8.2.0. Released v1.0.0.
% 60.10/60.39 % Domain : Ring Theory
% 60.10/60.39 % Problem : (-X*Y) + (X*Y) = additive_identity
% 60.10/60.39 % Version : [Wos65] axioms : Reduced > Incomplete.
% 60.10/60.39 % English :
% 60.10/60.39
% 60.10/60.39 % Refs : [Wos65] Wos (1965), Unpublished Note
% 60.10/60.39 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 60.10/60.39 % Source : [SPRFN]
% 60.10/60.39 % Names : Problem 23 [Wos65]
% 60.10/60.39 % : wos23 [WM76]
% 60.10/60.39
% 60.10/60.39 % Status : Unsatisfiable
% 60.10/60.39 % 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.00 v2.2.1, 0.33 v2.2.0, 0.22 v2.1.0, 0.14 v2.0.0
% 60.10/60.39 % Syntax : Number of clauses : 31 ( 11 unt; 0 nHn; 21 RR)
% 60.10/60.39 % Number of literals : 79 ( 0 equ; 49 neg)
% 60.10/60.39 % Maximal clause size : 5 ( 2 avg)
% 60.10/60.39 % Maximal term depth : 2 ( 1 avg)
% 60.10/60.39 % Number of predicates : 3 ( 3 usr; 0 prp; 2-3 aty)
% 60.10/60.39 % Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% 60.10/60.39 % Number of variables : 105 ( 2 sgn)
% 60.10/60.39 % SPC : CNF_UNS_RFO_NEQ_HRN
% 60.10/60.39
% 60.10/60.39 % Comments :
% 60.10/60.39 %--------------------------------------------------------------------------
% 60.10/60.39 %----Include ring theory axioms
% 60.10/60.39 %include('Axioms/RNG001-0.ax').
% 60.10/60.39 %--------------------------------------------------------------------------
% 60.10/60.39 cnf(additive_inverse_substitution,axiom,
% 60.10/60.39 ( ~ equalish(X,Y)
% 60.10/60.39 | equalish(additive_inverse(X),additive_inverse(Y)) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(add_substitution1,axiom,
% 60.10/60.39 ( ~ equalish(X,Y)
% 60.10/60.39 | equalish(add(X,W),add(Y,W)) ) ).
% 60.10/60.39
% 60.10/60.39 %----This axiom omited in this version
% 60.10/60.39 %input_clause(add_substitution2,axiom,
% 60.10/60.39 % [--equalish(X,Y),
% 60.10/60.39 % ++equalish(add(W,X),add(W,Y))]).
% 60.10/60.39
% 60.10/60.39 cnf(sum_substitution1,axiom,
% 60.10/60.39 ( ~ equalish(X,Y)
% 60.10/60.39 | ~ sum(X,W,Z)
% 60.10/60.39 | sum(Y,W,Z) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(sum_substitution2,axiom,
% 60.10/60.39 ( ~ equalish(X,Y)
% 60.10/60.39 | ~ sum(W,X,Z)
% 60.10/60.39 | sum(W,Y,Z) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(sum_substitution3,axiom,
% 60.10/60.39 ( ~ equalish(X,Y)
% 60.10/60.39 | ~ sum(W,Z,X)
% 60.10/60.39 | sum(W,Z,Y) ) ).
% 60.10/60.39
% 60.10/60.39 %----Equality axioms for multiplicative operator
% 60.10/60.39 cnf(multiply_substitution1,axiom,
% 60.10/60.39 ( ~ equalish(X,Y)
% 60.10/60.39 | equalish(multiply(X,W),multiply(Y,W)) ) ).
% 60.10/60.39
% 60.10/60.39 %----This axiom omited in this version
% 60.10/60.39 %input_clause(multiply_substitution2,axiom,
% 60.10/60.39 % [--equalish(X,Y),
% 60.10/60.39 % ++equalish(multiply(W,X),multiply(W,Y))]).
% 60.10/60.39
% 60.10/60.39 cnf(product_substitution1,axiom,
% 60.10/60.39 ( ~ equalish(X,Y)
% 60.10/60.39 | ~ product(X,W,Z)
% 60.10/60.39 | product(Y,W,Z) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(product_substitution2,axiom,
% 60.10/60.39 ( ~ equalish(X,Y)
% 60.10/60.39 | ~ product(W,X,Z)
% 60.10/60.39 | product(W,Y,Z) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(product_substitution3,axiom,
% 60.10/60.39 ( ~ equalish(X,Y)
% 60.10/60.39 | ~ product(W,Z,X)
% 60.10/60.39 | product(W,Z,Y) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(additive_identity1,axiom,
% 60.10/60.39 sum(additive_identity,X,X) ).
% 60.10/60.39
% 60.10/60.39 cnf(additive_identity2,axiom,
% 60.10/60.39 sum(X,additive_identity,X) ).
% 60.10/60.39
% 60.10/60.39 cnf(closure_of_multiplication,axiom,
% 60.10/60.39 product(X,Y,multiply(X,Y)) ).
% 60.10/60.39
% 60.10/60.39 cnf(closure_of_addition,axiom,
% 60.10/60.39 sum(X,Y,add(X,Y)) ).
% 60.10/60.39
% 60.10/60.39 cnf(left_inverse,axiom,
% 60.10/60.39 sum(additive_inverse(X),X,additive_identity) ).
% 60.10/60.39
% 60.10/60.39 cnf(right_inverse,axiom,
% 60.10/60.39 sum(X,additive_inverse(X),additive_identity) ).
% 60.10/60.39
% 60.10/60.39 cnf(associativity_of_addition1,axiom,
% 60.10/60.39 ( ~ sum(X,Y,U)
% 60.10/60.39 | ~ sum(Y,Z,V)
% 60.10/60.39 | ~ sum(U,Z,W)
% 60.10/60.39 | sum(X,V,W) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(associativity_of_addition2,axiom,
% 60.10/60.39 ( ~ sum(X,Y,U)
% 60.10/60.39 | ~ sum(Y,Z,V)
% 60.10/60.39 | ~ sum(X,V,W)
% 60.10/60.39 | sum(U,Z,W) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(commutativity_of_addition,axiom,
% 60.10/60.39 ( ~ sum(X,Y,Z)
% 60.10/60.39 | sum(Y,X,Z) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(associativity_of_multiplication1,axiom,
% 60.10/60.39 ( ~ product(X,Y,U)
% 60.10/60.39 | ~ product(Y,Z,V)
% 60.10/60.39 | ~ product(U,Z,W)
% 60.10/60.39 | product(X,V,W) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(associativity_of_multiplication2,axiom,
% 60.10/60.39 ( ~ product(X,Y,U)
% 60.10/60.39 | ~ product(Y,Z,V)
% 60.10/60.39 | ~ product(X,V,W)
% 60.10/60.39 | product(U,Z,W) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(distributivity1,axiom,
% 60.10/60.39 ( ~ product(X,Y,V1)
% 60.10/60.39 | ~ product(X,Z,V2)
% 60.10/60.39 | ~ sum(Y,Z,V3)
% 60.10/60.39 | ~ product(X,V3,V4)
% 60.10/60.39 | sum(V1,V2,V4) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(distributivity2,axiom,
% 60.10/60.39 ( ~ product(X,Y,V1)
% 60.10/60.39 | ~ product(X,Z,V2)
% 60.10/60.39 | ~ sum(Y,Z,V3)
% 60.10/60.39 | ~ sum(V1,V2,V4)
% 60.10/60.39 | product(X,V3,V4) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(distributivity3,axiom,
% 60.10/60.39 ( ~ product(Y,X,V1)
% 60.10/60.39 | ~ product(Z,X,V2)
% 60.10/60.39 | ~ sum(Y,Z,V3)
% 60.10/60.39 | ~ product(V3,X,V4)
% 60.10/60.39 | sum(V1,V2,V4) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(distributivity4,axiom,
% 60.10/60.39 ( ~ product(Y,X,V1)
% 60.10/60.39 | ~ product(Z,X,V2)
% 60.10/60.39 | ~ sum(Y,Z,V3)
% 60.10/60.39 | ~ sum(V1,V2,V4)
% 60.10/60.39 | product(V3,X,V4) ) ).
% 60.10/60.39
% 60.10/60.39 %-----Equality axioms for operators
% 60.10/60.39 cnf(addition_is_well_defined,axiom,
% 60.10/60.39 ( ~ sum(X,Y,U)
% 60.10/60.39 | ~ sum(X,Y,V)
% 60.10/60.39 | equalish(U,V) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(multiplication_is_well_defined,axiom,
% 60.10/60.39 ( ~ product(X,Y,U)
% 60.10/60.39 | ~ product(X,Y,V)
% 60.10/60.39 | equalish(U,V) ) ).
% 60.10/60.39
% 60.10/60.39 cnf(multiplicative_identity1,axiom,
% 60.10/60.39 product(additive_identity,X,additive_identity) ).
% 60.10/60.39
% 60.10/60.39 cnf(multiplicative_identity2,axiom,
% 60.10/60.39 product(X,additive_identity,additive_identity) ).
% 60.10/60.39
% 60.10/60.39 cnf(a_times_b,hypothesis,
% 60.10/60.39 product(a,b,d) ).
% 60.10/60.39
% 60.10/60.39 cnf(a_inverse_times_b,hypothesis,
% 60.10/60.39 product(additive_inverse(a),b,c) ).
% 60.10/60.39
% 60.10/60.39 cnf(prove_sum_is_additive_identity,negated_conjecture,
% 60.10/60.39 ~ sum(c,d,additive_identity) ).
% 60.10/60.39
% 60.10/60.39 %--------------------------------------------------------------------------
% 60.10/60.39 %-------------------------------------------
% 60.10/60.39 % Proof found
% 60.10/60.39 % SZS status Theorem for theBenchmark
% 60.10/60.39 % SZS output start Proof
% 60.10/60.39 %ClaNum:31(EqnAxiom:0)
% 60.10/60.39 %VarNum:212(SingletonVarNum:105)
% 60.10/60.39 %MaxLitNum:5
% 60.10/60.39 %MaxfuncDepth:1
% 60.10/60.39 %SharedTerms:9
% 60.10/60.39 %goalClause: 11
% 60.10/60.39 %singleGoalClaCount:1
% 60.10/60.39 [1]P1(a1,a2,a6)
% 60.10/60.39 [11]~P3(a7,a6,a3)
% 60.10/60.39 [6]P1(f5(a1),a2,a7)
% 60.10/60.39 [2]P1(x21,a3,a3)
% 60.10/60.39 [3]P1(a3,x31,a3)
% 60.10/60.39 [4]P3(x41,a3,x41)
% 60.10/60.39 [5]P3(a3,x51,x51)
% 60.10/60.39 [7]P3(x71,f5(x71),a3)
% 60.10/60.39 [8]P3(f5(x81),x81,a3)
% 60.10/60.39 [9]P3(x91,x92,f4(x91,x92))
% 60.10/60.39 [10]P1(x101,x102,f8(x101,x102))
% 60.10/60.39 [12]~P2(x121,x122)+P2(f5(x121),f5(x122))
% 60.10/60.39 [15]~P3(x152,x151,x153)+P3(x151,x152,x153)
% 60.10/60.39 [13]~P2(x131,x133)+P2(f4(x131,x132),f4(x133,x132))
% 60.10/60.39 [14]~P2(x141,x143)+P2(f8(x141,x142),f8(x143,x142))
% 60.10/60.39 [16]~P3(x161,x162,x164)+P3(x161,x162,x163)+~P2(x164,x163)
% 60.10/60.39 [17]~P3(x171,x174,x173)+P3(x171,x172,x173)+~P2(x174,x172)
% 60.10/60.39 [18]~P3(x184,x182,x183)+P3(x181,x182,x183)+~P2(x184,x181)
% 60.10/60.39 [19]~P1(x191,x192,x194)+P1(x191,x192,x193)+~P2(x194,x193)
% 60.10/60.39 [20]~P1(x201,x204,x203)+P1(x201,x202,x203)+~P2(x204,x202)
% 60.10/60.39 [21]~P1(x214,x212,x213)+P1(x211,x212,x213)+~P2(x214,x211)
% 60.10/60.39 [22]~P3(x223,x224,x221)+P2(x221,x222)+~P3(x223,x224,x222)
% 60.10/60.39 [23]~P1(x233,x234,x231)+P2(x231,x232)+~P1(x233,x234,x232)
% 60.10/60.39 [24]~P3(x246,x244,x241)+P3(x241,x242,x243)+~P3(x244,x242,x245)+~P3(x246,x245,x243)
% 60.10/60.39 [25]~P3(x251,x256,x254)+P3(x251,x252,x253)+~P3(x254,x255,x253)+~P3(x256,x255,x252)
% 60.10/60.39 [26]~P1(x266,x264,x261)+P1(x261,x262,x263)+~P1(x264,x262,x265)+~P1(x266,x265,x263)
% 60.10/60.39 [27]~P1(x271,x276,x274)+P1(x271,x272,x273)+~P1(x274,x275,x273)+~P1(x276,x275,x272)
% 60.10/60.39 [28]~P1(x287,x285,x282)+~P1(x287,x284,x281)+P3(x281,x282,x283)+~P3(x284,x285,x286)+~P1(x287,x286,x283)
% 60.10/60.39 [29]~P1(x295,x297,x292)+~P1(x294,x297,x291)+P3(x291,x292,x293)+~P3(x294,x295,x296)+~P1(x296,x297,x293)
% 60.10/60.39 [30]~P1(x307,x302,x305)+~P1(x306,x302,x304)+P1(x301,x302,x303)+~P3(x304,x305,x303)+~P3(x306,x307,x301)
% 60.10/60.39 [31]~P1(x311,x317,x315)+~P1(x311,x316,x314)+P1(x311,x312,x313)+~P3(x314,x315,x313)+~P3(x316,x317,x312)
% 60.10/60.39 %EqnAxiom
% 60.10/60.39
% 60.10/60.39 %-------------------------------------------
% 60.10/60.41 cnf(32,plain,
% 60.10/60.41 (~P3(a6,a7,a3)),
% 60.10/60.41 inference(scs_inference,[],[11,15])).
% 60.10/60.41 cnf(36,plain,
% 60.10/60.41 (P2(f8(x361,a3),a3)),
% 60.10/60.41 inference(scs_inference,[],[11,4,10,2,15,22,23])).
% 60.10/60.41 cnf(37,plain,
% 60.10/60.41 (P1(x371,a3,a3)),
% 60.10/60.41 inference(rename_variables,[],[2])).
% 60.10/60.41 cnf(38,plain,
% 60.10/60.41 (P1(x381,x382,f8(x381,x382))),
% 60.10/60.41 inference(rename_variables,[],[10])).
% 60.10/60.41 cnf(40,plain,
% 60.10/60.41 (~P3(a3,a6,f5(a7))),
% 60.10/60.41 inference(scs_inference,[],[11,4,10,2,7,15,22,23,24])).
% 60.10/60.41 cnf(42,plain,
% 60.10/60.41 (P3(x421,a3,x421)),
% 60.10/60.41 inference(rename_variables,[],[4])).
% 60.10/60.41 cnf(44,plain,
% 60.10/60.41 (P3(x441,f4(a3,a3),x441)),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,9,10,2,7,15,22,23,24,25])).
% 60.10/60.41 cnf(45,plain,
% 60.10/60.41 (P3(x451,x452,f4(x451,x452))),
% 60.10/60.41 inference(rename_variables,[],[9])).
% 60.10/60.41 cnf(47,plain,
% 60.10/60.41 (P1(f8(x471,a3),a3,f8(x471,a3))),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,9,10,38,2,37,7,15,22,23,24,25,26])).
% 60.10/60.41 cnf(48,plain,
% 60.10/60.41 (P1(x481,x482,f8(x481,x482))),
% 60.10/60.41 inference(rename_variables,[],[10])).
% 60.10/60.41 cnf(49,plain,
% 60.10/60.41 (P1(x491,x492,f8(x491,x492))),
% 60.10/60.41 inference(rename_variables,[],[10])).
% 60.10/60.41 cnf(50,plain,
% 60.10/60.41 (P1(x501,a3,a3)),
% 60.10/60.41 inference(rename_variables,[],[2])).
% 60.10/60.41 cnf(52,plain,
% 60.10/60.41 (P1(x521,f8(x521,x521),f8(f8(x521,x521),x521))),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,9,10,38,49,48,2,37,7,15,22,23,24,25,26,27])).
% 60.10/60.41 cnf(54,plain,
% 60.10/60.41 (P1(x541,x542,f8(x541,x542))),
% 60.10/60.41 inference(rename_variables,[],[10])).
% 60.10/60.41 cnf(57,plain,
% 60.10/60.41 (P3(f8(x571,a3),f8(x571,a3),f8(x571,a3))),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,9,10,38,49,54,48,2,37,7,15,22,23,24,25,26,27,28])).
% 60.10/60.41 cnf(60,plain,
% 60.10/60.41 (P1(x601,x602,f8(x601,x602))),
% 60.10/60.41 inference(rename_variables,[],[10])).
% 60.10/60.41 cnf(61,plain,
% 60.10/60.41 (P3(x611,a3,x611)),
% 60.10/60.41 inference(rename_variables,[],[4])).
% 60.10/60.41 cnf(63,plain,
% 60.10/60.41 (P3(f8(a3,x631),f8(a3,x631),f8(a3,x631))),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,61,9,10,38,49,54,60,48,2,37,7,15,22,23,24,25,26,27,28,29])).
% 60.10/60.41 cnf(66,plain,
% 60.10/60.41 (P1(x661,x662,f8(x661,x662))),
% 60.10/60.41 inference(rename_variables,[],[10])).
% 60.10/60.41 cnf(67,plain,
% 60.10/60.41 (P3(x671,a3,x671)),
% 60.10/60.41 inference(rename_variables,[],[4])).
% 60.10/60.41 cnf(69,plain,
% 60.10/60.41 (P1(x691,a3,f8(a3,a3))),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,61,67,5,9,10,38,49,54,60,66,48,2,37,50,7,15,22,23,24,25,26,27,28,29,30])).
% 60.10/60.41 cnf(70,plain,
% 60.10/60.41 (P3(a3,x701,x701)),
% 60.10/60.41 inference(rename_variables,[],[5])).
% 60.10/60.41 cnf(71,plain,
% 60.10/60.41 (P3(x711,a3,x711)),
% 60.10/60.41 inference(rename_variables,[],[4])).
% 60.10/60.41 cnf(72,plain,
% 60.10/60.41 (P1(x721,x722,f8(x721,x722))),
% 60.10/60.41 inference(rename_variables,[],[10])).
% 60.10/60.41 cnf(74,plain,
% 60.10/60.41 (P1(x741,a3,f4(f8(x741,a3),f8(x741,a3)))),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,61,67,71,5,9,45,10,38,49,54,60,66,72,48,2,37,50,7,15,22,23,24,25,26,27,28,29,30,31])).
% 60.10/60.41 cnf(76,plain,
% 60.10/60.41 (P3(x761,a3,x761)),
% 60.10/60.41 inference(rename_variables,[],[4])).
% 60.10/60.41 cnf(78,plain,
% 60.10/60.41 (P1(x781,x782,f8(x781,x782))),
% 60.10/60.41 inference(rename_variables,[],[10])).
% 60.10/60.41 cnf(80,plain,
% 60.10/60.41 (P3(f8(x801,a3),a3,a3)),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,61,67,71,76,5,9,45,10,38,49,54,60,66,72,48,2,37,50,7,15,22,23,24,25,26,27,28,29,30,31,16])).
% 60.10/60.41 cnf(83,plain,
% 60.10/60.41 (P3(a3,a3,f8(x831,a3))),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,61,67,71,76,5,70,9,45,10,38,49,54,60,66,72,48,2,37,50,7,15,22,23,24,25,26,27,28,29,30,31,16,17])).
% 60.10/60.41 cnf(86,plain,
% 60.10/60.41 (P1(x861,a3,f8(x861,f8(x862,a3)))),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,61,67,71,76,5,70,9,45,10,38,49,54,60,66,72,78,48,2,37,50,7,15,22,23,24,25,26,27,28,29,30,31,16,17,20])).
% 60.10/60.41 cnf(87,plain,
% 60.10/60.41 (P1(x871,x872,f8(x871,x872))),
% 60.10/60.41 inference(rename_variables,[],[10])).
% 60.10/60.41 cnf(89,plain,
% 60.10/60.41 (P1(a3,x891,f8(f8(x892,a3),x891))),
% 60.10/60.41 inference(scs_inference,[],[11,4,42,61,67,71,76,5,70,9,45,10,38,49,54,60,66,72,78,87,48,2,37,50,7,15,22,23,24,25,26,27,28,29,30,31,16,17,20,21])).
% 60.10/60.41 cnf(92,plain,
% 60.10/60.41 (~P3(a6,a3,f5(a7))),
% 60.10/60.41 inference(scs_inference,[],[40,15])).
% 60.10/60.41 cnf(94,plain,
% 60.10/60.41 (P3(a3,f4(a3,a3),f8(x941,a3))),
% 60.10/60.41 inference(scs_inference,[],[44,40,36,15,18])).
% 60.10/60.41 cnf(95,plain,
% 60.10/60.41 (P3(x951,f4(a3,a3),x951)),
% 60.10/60.41 inference(rename_variables,[],[44])).
% 60.10/60.41 cnf(97,plain,
% 60.10/60.41 (P2(f8(x971,f8(x972,a3)),f8(a3,a3))),
% 60.10/60.41 inference(scs_inference,[],[44,40,86,69,36,15,18,23])).
% 60.10/60.41 cnf(100,plain,
% 60.10/60.41 (P3(f8(x1001,a3),f4(a3,a3),a3)),
% 60.10/60.41 inference(scs_inference,[],[44,95,40,86,69,36,15,18,23,16])).
% 60.10/60.41 cnf(101,plain,
% 60.10/60.41 (P3(x1011,f4(a3,a3),x1011)),
% 60.10/60.41 inference(rename_variables,[],[44])).
% 60.10/60.41 cnf(103,plain,
% 60.10/60.41 (P2(f5(f4(a3,a3)),a3)),
% 60.10/60.41 inference(scs_inference,[],[44,95,101,40,86,69,36,8,15,18,23,16,22])).
% 60.10/60.41 cnf(105,plain,
% 60.10/60.41 (P3(x1051,f4(a3,a3),x1051)),
% 60.10/60.41 inference(rename_variables,[],[44])).
% 60.10/60.41 cnf(107,plain,
% 60.10/60.41 (~P3(f4(a3,a3),a6,f5(a7))),
% 60.10/60.41 inference(scs_inference,[],[44,95,101,105,40,86,69,36,8,5,15,18,23,16,22,24])).
% 60.10/60.41 cnf(111,plain,
% 60.10/60.41 (P1(f8(x1111,a3),x1112,f8(x1111,a3))),
% 60.10/60.41 inference(scs_inference,[],[44,95,101,105,40,86,47,69,36,3,8,5,15,18,23,16,22,24,26])).
% 60.10/60.41 cnf(113,plain,
% 60.10/60.41 (P3(a3,f8(x1131,a3),a3)),
% 60.10/60.41 inference(scs_inference,[],[44,95,101,105,80,83,40,86,47,69,36,3,8,5,15,18,23,16,22,24,26,25])).
% 60.10/60.41 cnf(114,plain,
% 60.10/60.41 (P3(a3,a3,f8(x1141,a3))),
% 60.10/60.41 inference(rename_variables,[],[83])).
% 60.10/60.41 cnf(119,plain,
% 60.10/60.41 (P1(f8(x1191,a3),f8(f8(x1191,a3),f8(x1191,a3)),f8(a3,a3))),
% 60.10/60.41 inference(scs_inference,[],[44,95,101,105,80,83,114,40,52,86,47,69,36,3,8,5,15,18,23,16,22,24,26,25,31,19])).
% 60.10/60.41 cnf(129,plain,
% 60.10/60.41 (~P3(a6,f4(a3,a3),f5(a7))),
% 60.10/60.41 inference(scs_inference,[],[107,15])).
% 60.10/60.41 cnf(131,plain,
% 60.10/60.41 (P1(a3,f8(f8(x1311,a3),f8(x1311,a3)),f8(a3,a3))),
% 60.10/60.41 inference(scs_inference,[],[107,36,119,15,21])).
% 60.10/60.41 cnf(132,plain,
% 60.10/60.41 (P2(f8(x1321,a3),a3)),
% 60.10/60.41 inference(rename_variables,[],[36])).
% 60.10/60.41 cnf(135,plain,
% 60.10/60.41 (P2(f8(x1351,f8(x1352,a3)),f8(a3,a3))),
% 60.10/60.41 inference(rename_variables,[],[97])).
% 60.10/60.41 cnf(137,plain,
% 60.10/60.41 (P1(f8(x1371,a3),f8(f8(x1371,a3),f8(x1371,a3)),a3)),
% 60.10/60.41 inference(scs_inference,[],[107,36,132,97,119,15,21,20,19])).
% 60.10/60.41 cnf(140,plain,
% 60.10/60.41 (P3(f8(a3,a3),f4(a3,a3),f8(x1401,f8(x1402,a3)))),
% 60.10/60.41 inference(scs_inference,[],[107,44,36,132,97,135,119,15,21,20,19,18])).
% 60.10/60.41 cnf(141,plain,
% 60.10/60.41 (P3(x1411,f4(a3,a3),x1411)),
% 60.10/60.41 inference(rename_variables,[],[44])).
% 60.10/60.41 cnf(143,plain,
% 60.10/60.41 (P3(f8(x1431,f8(x1432,a3)),f4(a3,a3),f8(a3,a3))),
% 60.10/60.41 inference(scs_inference,[],[107,44,141,36,132,97,135,119,15,21,20,19,18,16])).
% 60.10/60.41 cnf(147,plain,
% 60.10/60.41 (P1(f8(x1471,a3),x1472,f8(x1471,a3))),
% 60.10/60.41 inference(rename_variables,[],[111])).
% 60.10/60.41 cnf(149,plain,
% 60.10/60.41 (P2(f8(x1491,a3),f4(a3,f4(a3,a3)))),
% 60.10/60.41 inference(scs_inference,[],[94,107,44,141,36,132,97,135,119,111,9,15,21,20,19,18,16,23,22])).
% 60.10/60.41 cnf(150,plain,
% 60.10/60.41 (P3(x1501,x1502,f4(x1501,x1502))),
% 60.10/60.41 inference(rename_variables,[],[9])).
% 60.10/60.41 cnf(153,plain,
% 60.10/60.41 (P1(f8(x1531,a3),x1532,f8(x1531,a3))),
% 60.10/60.41 inference(rename_variables,[],[111])).
% 60.10/60.41 cnf(156,plain,
% 60.10/60.41 (P3(f8(x1561,a3),f8(x1562,a3),f8(x1561,a3))),
% 60.10/60.41 inference(scs_inference,[],[94,107,113,44,141,83,36,132,97,135,119,111,147,1,9,10,15,21,20,19,18,16,23,22,27,24])).
% 60.10/60.41 cnf(158,plain,
% 60.10/60.41 (P1(f8(a3,a3),a3,f8(x1581,a3))),
% 60.10/60.41 inference(scs_inference,[],[94,107,113,44,141,83,36,132,97,135,119,111,147,153,74,1,9,10,15,21,20,19,18,16,23,22,27,24,26])).
% 60.10/60.41 cnf(159,plain,
% 60.10/60.41 (P1(f8(x1591,a3),x1592,f8(x1591,a3))),
% 60.10/60.41 inference(rename_variables,[],[111])).
% 60.10/60.41 cnf(162,plain,
% 60.10/60.41 (P3(f8(x1621,a3),f8(x1622,a3),f8(x1622,a3))),
% 60.10/60.41 inference(scs_inference,[],[94,107,113,44,141,80,83,36,132,97,135,119,111,147,153,74,1,9,10,15,21,20,19,18,16,23,22,27,24,26,25])).
% 60.10/60.41 cnf(165,plain,
% 60.10/60.41 (P1(f8(x1651,a3),x1652,f8(x1651,a3))),
% 60.10/60.41 inference(rename_variables,[],[111])).
% 60.10/60.41 cnf(168,plain,
% 60.10/60.41 (P1(x1681,f8(x1682,a3),f8(x1682,a3))),
% 60.10/60.41 inference(scs_inference,[],[94,107,113,44,141,80,83,36,132,97,135,119,111,147,153,159,74,1,9,150,10,2,15,21,20,19,18,16,23,22,27,24,26,25,28,31])).
% 60.10/60.41 cnf(180,plain,
% 60.10/60.41 (P3(a3,f4(a3,f4(a3,a3)),a3)),
% 60.10/60.41 inference(scs_inference,[],[94,107,113,44,141,80,83,57,36,132,97,135,119,111,147,153,159,165,89,74,1,9,150,10,86,2,4,15,21,20,19,18,16,23,22,27,24,26,25,28,31,30,29,17])).
% 60.10/60.41 cnf(182,plain,
% 60.10/60.41 (P1(x1821,f8(x1822,a3),a3)),
% 60.10/60.41 inference(scs_inference,[],[36,168,19])).
% 60.10/60.41 cnf(183,plain,
% 60.10/60.41 (P2(f8(x1831,a3),a3)),
% 60.10/60.41 inference(rename_variables,[],[36])).
% 60.10/60.41 cnf(188,plain,
% 60.10/60.41 (P1(x1881,a3,f8(x1882,a3))),
% 60.10/60.41 inference(scs_inference,[],[156,36,183,168,149,19,17,20])).
% 60.10/60.41 cnf(189,plain,
% 60.10/60.41 (P2(f8(x1891,a3),a3)),
% 60.10/60.41 inference(rename_variables,[],[36])).
% 60.10/60.41 cnf(192,plain,
% 60.10/60.41 (P2(f8(x1921,a3),a3)),
% 60.10/60.41 inference(rename_variables,[],[36])).
% 60.10/60.41 cnf(194,plain,
% 60.10/60.41 (P2(f8(x1941,a3),f8(x1942,a3))),
% 60.10/60.41 inference(scs_inference,[],[143,156,36,183,189,168,149,111,19,17,20,16,23])).
% 60.10/60.41 cnf(195,plain,
% 60.10/60.41 (P1(f8(x1951,a3),x1952,f8(x1951,a3))),
% 60.10/60.42 inference(rename_variables,[],[111])).
% 60.10/60.42 cnf(196,plain,
% 60.10/60.42 (P1(x1961,f8(x1962,a3),f8(x1962,a3))),
% 60.10/60.42 inference(rename_variables,[],[168])).
% 60.10/60.42 cnf(201,plain,
% 60.10/60.42 (P2(f8(a3,a3),f8(x2011,f8(x2012,a3)))),
% 60.10/60.42 inference(scs_inference,[],[143,140,156,44,36,183,189,192,168,149,111,19,17,20,16,23,18,22])).
% 60.10/60.42 cnf(202,plain,
% 60.10/60.42 (P3(x2021,f4(a3,a3),x2021)),
% 60.10/60.42 inference(rename_variables,[],[44])).
% 60.10/60.42 cnf(206,plain,
% 60.10/60.42 (P1(x2061,f8(x2062,a3),f8(x2062,a3))),
% 60.10/60.42 inference(rename_variables,[],[168])).
% 60.10/60.42 cnf(208,plain,
% 60.10/60.42 (P3(f8(a3,a3),a3,f8(x2081,f8(x2082,a3)))),
% 60.10/60.42 inference(scs_inference,[],[143,140,156,44,202,36,183,189,192,168,196,149,158,111,89,4,19,17,20,16,23,18,22,26,24])).
% 60.10/60.42 cnf(213,plain,
% 60.10/60.42 (P1(f8(x2131,a3),x2132,f8(x2131,a3))),
% 60.10/60.42 inference(rename_variables,[],[111])).
% 60.10/60.42 cnf(216,plain,
% 60.10/60.42 (P3(f8(a3,f8(x2161,a3)),f8(a3,a3),f8(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[143,140,156,44,202,36,183,189,192,168,196,63,149,158,111,195,6,89,10,4,19,17,20,16,23,18,22,26,24,27,25])).
% 60.10/60.42 cnf(217,plain,
% 60.10/60.42 (P3(f8(x2171,f8(x2172,a3)),f4(a3,a3),f8(a3,a3))),
% 60.10/60.42 inference(rename_variables,[],[143])).
% 60.10/60.42 cnf(222,plain,
% 60.10/60.42 (P3(f8(x2221,a3),f8(x2222,a3),f8(x2221,a3))),
% 60.10/60.42 inference(rename_variables,[],[156])).
% 60.10/60.42 cnf(224,plain,
% 60.10/60.42 (P1(f8(x2241,a3),f8(a3,a3),f4(a3,f8(x2241,a3)))),
% 60.10/60.42 inference(scs_inference,[],[143,217,140,156,44,202,36,183,189,192,168,196,63,149,158,137,111,195,213,6,89,69,9,10,4,19,17,20,16,23,18,22,26,24,27,25,29,31])).
% 60.10/60.42 cnf(225,plain,
% 60.10/60.42 (P3(x2251,x2252,f4(x2251,x2252))),
% 60.10/60.42 inference(rename_variables,[],[9])).
% 60.10/60.42 cnf(226,plain,
% 60.10/60.42 (P3(f8(x2261,f8(x2262,a3)),f4(a3,a3),f8(a3,a3))),
% 60.10/60.42 inference(rename_variables,[],[143])).
% 60.10/60.42 cnf(227,plain,
% 60.10/60.42 (P1(f8(x2271,a3),x2272,f8(x2271,a3))),
% 60.10/60.42 inference(rename_variables,[],[111])).
% 60.10/60.42 cnf(231,plain,
% 60.10/60.42 (P1(x2311,f8(x2312,a3),f8(x2312,a3))),
% 60.10/60.42 inference(rename_variables,[],[168])).
% 60.10/60.42 cnf(232,plain,
% 60.10/60.42 (P1(x2321,f8(x2322,a3),f8(x2322,a3))),
% 60.10/60.42 inference(rename_variables,[],[168])).
% 60.10/60.42 cnf(235,plain,
% 60.10/60.42 (P1(f8(a3,a3),f8(x2351,a3),f4(f8(x2351,a3),f8(x2351,a3)))),
% 60.10/60.42 inference(scs_inference,[],[143,217,226,140,156,222,44,202,36,183,189,192,168,196,206,232,231,63,149,158,137,111,195,213,227,6,89,69,9,225,10,4,19,17,20,16,23,18,22,26,24,27,25,29,31,28,30])).
% 60.10/60.42 cnf(240,plain,
% 60.10/60.42 (P1(a3,f8(x2401,a3),f4(f8(x2401,a3),f8(x2401,a3)))),
% 60.10/60.42 inference(scs_inference,[],[36,235,21])).
% 60.10/60.42 cnf(241,plain,
% 60.10/60.42 (P2(f8(x2411,a3),a3)),
% 60.10/60.42 inference(rename_variables,[],[36])).
% 60.10/60.42 cnf(243,plain,
% 60.10/60.42 (P1(a3,f8(f8(x2431,a3),f8(x2431,a3)),f8(x2432,a3))),
% 60.10/60.42 inference(scs_inference,[],[36,235,194,131,21,19])).
% 60.10/60.42 cnf(246,plain,
% 60.10/60.42 (P1(f8(a3,a3),a3,f4(f8(x2461,a3),f8(x2461,a3)))),
% 60.10/60.42 inference(scs_inference,[],[36,241,235,194,131,21,19,20])).
% 60.10/60.42 cnf(247,plain,
% 60.10/60.42 (P2(f8(x2471,a3),a3)),
% 60.10/60.42 inference(rename_variables,[],[36])).
% 60.10/60.42 cnf(252,plain,
% 60.10/60.42 (P3(a3,f4(a3,a3),f5(f4(a3,a3)))),
% 60.10/60.42 inference(scs_inference,[],[216,44,36,241,247,235,194,131,103,21,19,20,17,18])).
% 60.10/60.42 cnf(253,plain,
% 60.10/60.42 (P3(x2531,f4(a3,a3),x2531)),
% 60.10/60.42 inference(rename_variables,[],[44])).
% 60.10/60.42 cnf(255,plain,
% 60.10/60.42 (P2(f4(f8(x2551,a3),f8(x2551,a3)),a3)),
% 60.10/60.42 inference(scs_inference,[],[216,44,36,241,247,235,194,131,182,103,21,19,20,17,18,23])).
% 60.10/60.42 cnf(256,plain,
% 60.10/60.42 (P1(x2561,f8(x2562,a3),a3)),
% 60.10/60.42 inference(rename_variables,[],[182])).
% 60.10/60.42 cnf(258,plain,
% 60.10/60.42 (P2(a3,f8(x2581,a3))),
% 60.10/60.42 inference(scs_inference,[],[100,216,44,253,36,241,247,235,194,131,182,103,21,19,20,17,18,23,22])).
% 60.10/60.42 cnf(259,plain,
% 60.10/60.42 (P3(x2591,f4(a3,a3),x2591)),
% 60.10/60.42 inference(rename_variables,[],[44])).
% 60.10/60.42 cnf(261,plain,
% 60.10/60.42 (P1(f8(a3,a3),f4(f8(a3,a3),f8(a3,a3)),a3)),
% 60.10/60.42 inference(scs_inference,[],[100,216,44,253,36,241,247,235,194,131,182,256,103,21,19,20,17,18,23,22,27])).
% 60.10/60.42 cnf(262,plain,
% 60.10/60.42 (P1(f8(a3,a3),f8(x2621,a3),f4(f8(x2621,a3),f8(x2621,a3)))),
% 60.10/60.42 inference(rename_variables,[],[235])).
% 60.10/60.42 cnf(263,plain,
% 60.10/60.42 (P1(x2631,f8(x2632,a3),a3)),
% 60.10/60.42 inference(rename_variables,[],[182])).
% 60.10/60.42 cnf(265,plain,
% 60.10/60.42 (P1(f4(f8(x2651,a3),f8(x2651,a3)),f8(x2652,a3),f8(x2653,a3))),
% 60.10/60.42 inference(scs_inference,[],[100,216,44,253,36,241,247,235,262,194,131,182,256,263,188,103,21,19,20,17,18,23,22,27,26])).
% 60.10/60.42 cnf(269,plain,
% 60.10/60.42 (P3(f8(x2691,a3),f4(a3,a3),f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[100,94,216,44,253,259,5,36,241,247,235,262,194,131,182,256,263,188,103,21,19,20,17,18,23,22,27,26,24])).
% 60.10/60.42 cnf(273,plain,
% 60.10/60.42 (P3(f8(a3,f8(x2731,a3)),a3,a3)),
% 60.10/60.42 inference(scs_inference,[],[100,94,216,44,253,259,5,36,241,247,235,262,194,131,182,256,263,188,103,21,19,20,17,18,23,22,27,26,24,25])).
% 60.10/60.42 cnf(295,plain,
% 60.10/60.42 (P2(f8(x2951,a3),a3)),
% 60.10/60.42 inference(rename_variables,[],[36])).
% 60.10/60.42 cnf(297,plain,
% 60.10/60.42 (P1(f8(a3,a3),f4(f8(a3,a3),f8(a3,a3)),f8(x2971,a3))),
% 60.10/60.42 inference(scs_inference,[],[36,224,261,258,21,19])).
% 60.10/60.42 cnf(299,plain,
% 60.10/60.42 (P3(f8(x2991,a3),f8(x2992,f8(x2993,a3)),f8(x2991,a3))),
% 60.10/60.42 inference(scs_inference,[],[156,36,201,224,261,258,21,19,17])).
% 60.10/60.42 cnf(300,plain,
% 60.10/60.42 (P3(f8(x3001,a3),f8(x3002,a3),f8(x3001,a3))),
% 60.10/60.42 inference(rename_variables,[],[156])).
% 60.10/60.42 cnf(303,plain,
% 60.10/60.42 (P3(x3031,f4(a3,a3),x3031)),
% 60.10/60.42 inference(rename_variables,[],[44])).
% 60.10/60.42 cnf(306,plain,
% 60.10/60.42 (P2(f8(x3061,a3),a3)),
% 60.10/60.42 inference(rename_variables,[],[36])).
% 60.10/60.42 cnf(308,plain,
% 60.10/60.42 (P2(f4(a3,f8(x3081,a3)),a3)),
% 60.10/60.42 inference(scs_inference,[],[156,44,36,295,201,224,261,255,258,182,21,19,17,16,20,23])).
% 60.10/60.42 cnf(309,plain,
% 60.10/60.42 (P1(x3091,f8(x3092,a3),a3)),
% 60.10/60.42 inference(rename_variables,[],[182])).
% 60.10/60.42 cnf(311,plain,
% 60.10/60.42 (P3(a3,f8(x3111,a3),f8(x3112,a3))),
% 60.10/60.42 inference(scs_inference,[],[156,300,44,36,295,306,201,224,261,255,258,182,21,19,17,16,20,23,18])).
% 60.10/60.42 cnf(314,plain,
% 60.10/60.42 (P2(f8(x3141,a3),f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,156,300,44,5,36,295,306,201,224,261,255,258,182,21,19,17,16,20,23,18,22])).
% 60.10/60.42 cnf(315,plain,
% 60.10/60.42 (P3(a3,x3151,x3151)),
% 60.10/60.42 inference(rename_variables,[],[5])).
% 60.10/60.42 cnf(323,plain,
% 60.10/60.42 (P1(f8(x3231,a3),f8(a3,a3),f4(a3,f8(x3231,a3)))),
% 60.10/60.42 inference(rename_variables,[],[224])).
% 60.10/60.42 cnf(324,plain,
% 60.10/60.42 (P1(x3241,f8(x3242,a3),a3)),
% 60.10/60.42 inference(rename_variables,[],[182])).
% 60.10/60.42 cnf(326,plain,
% 60.10/60.42 (P3(a3,f8(a3,a3),f8(x3261,f8(x3262,a3)))),
% 60.10/60.42 inference(scs_inference,[],[94,156,300,83,208,44,303,7,8,5,36,295,306,201,224,261,255,258,182,309,21,19,17,16,20,23,18,22,24,27,25])).
% 60.10/60.42 cnf(329,plain,
% 60.10/60.42 (P1(f8(x3291,a3),f8(x3292,a3),f4(f8(x3292,a3),f8(x3292,a3)))),
% 60.10/60.42 inference(scs_inference,[],[94,156,300,83,208,44,303,7,8,5,36,295,306,201,224,261,240,255,258,182,309,324,4,21,19,17,16,20,23,18,22,24,27,25,30])).
% 60.10/60.42 cnf(336,plain,
% 60.10/60.42 (P1(a3,x3361,a3)),
% 60.10/60.42 inference(rename_variables,[],[3])).
% 60.10/60.42 cnf(338,plain,
% 60.10/60.42 (P3(a3,f4(a3,f8(x3381,a3)),a3)),
% 60.10/60.42 inference(scs_inference,[],[94,156,300,113,83,208,44,303,7,8,5,315,36,295,306,201,224,323,261,240,255,258,182,309,324,89,3,336,4,21,19,17,16,20,23,18,22,24,27,25,30,31,29])).
% 60.10/60.42 cnf(349,plain,
% 60.10/60.42 (P2(f8(x3491,a3),a3)),
% 60.10/60.42 inference(rename_variables,[],[36])).
% 60.10/60.42 cnf(355,plain,
% 60.10/60.42 (P2(f8(x3551,a3),f4(a3,a3))),
% 60.10/60.42 inference(rename_variables,[],[314])).
% 60.10/60.42 cnf(360,plain,
% 60.10/60.42 (P2(f4(f8(x3601,a3),f8(x3601,a3)),f8(x3602,a3))),
% 60.10/60.42 inference(scs_inference,[],[44,36,349,297,329,314,246,308,188,21,16,19,20,23])).
% 60.10/60.42 cnf(363,plain,
% 60.10/60.42 (P3(f4(a3,a3),f4(a3,a3),a3)),
% 60.10/60.42 inference(scs_inference,[],[100,44,36,349,297,329,314,355,246,308,188,21,16,19,20,23,18])).
% 60.10/60.42 cnf(366,plain,
% 60.10/60.42 (P1(f8(x3661,a3),f8(x3662,a3),f8(f8(a3,a3),f8(x3663,a3)))),
% 60.10/60.42 inference(scs_inference,[],[100,44,36,349,297,329,314,355,246,308,86,182,188,21,16,19,20,23,18,26])).
% 60.10/60.42 cnf(370,plain,
% 60.10/60.42 (P3(a3,f8(x3701,f8(x3702,a3)),f8(x3703,a3))),
% 60.10/60.42 inference(scs_inference,[],[100,156,83,326,44,36,349,297,329,314,355,246,308,86,182,188,21,16,19,20,23,18,26,25])).
% 60.10/60.42 cnf(395,plain,
% 60.10/60.42 (P1(f8(x3951,f8(x3952,a3)),x3953,f8(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[201,111,21])).
% 60.10/60.42 cnf(396,plain,
% 60.10/60.42 (P1(f8(x3961,a3),x3962,f8(x3961,a3))),
% 60.10/60.42 inference(rename_variables,[],[111])).
% 60.10/60.42 cnf(398,plain,
% 60.10/60.42 (P3(a3,f4(a3,f4(a3,a3)),f8(x3981,a3))),
% 60.10/60.42 inference(scs_inference,[],[311,201,149,111,21,17])).
% 60.10/60.42 cnf(401,plain,
% 60.10/60.42 (P3(f8(x4011,a3),f4(a3,a3),f8(x4012,a3))),
% 60.10/60.42 inference(scs_inference,[],[311,100,201,149,258,111,21,17,16])).
% 60.10/60.42 cnf(404,plain,
% 60.10/60.42 (P2(f8(x4041,f8(x4042,a3)),f8(a3,a3))),
% 60.10/60.42 inference(rename_variables,[],[97])).
% 60.10/60.42 cnf(406,plain,
% 60.10/60.42 (P1(a3,f8(a3,a3),f8(x4061,a3))),
% 60.10/60.42 inference(scs_inference,[],[311,100,243,201,97,404,149,258,111,366,21,17,16,19,20])).
% 60.10/60.42 cnf(409,plain,
% 60.10/60.42 (P3(f8(x4091,a3),f8(x4092,f8(x4093,a3)),f8(x4094,a3))),
% 60.10/60.42 inference(scs_inference,[],[299,311,100,243,201,97,404,194,149,258,111,366,21,17,16,19,20,18])).
% 60.10/60.42 cnf(412,plain,
% 60.10/60.42 (P2(f8(x4121,a3),f8(f8(x4121,a3),f8(x4122,a3)))),
% 60.10/60.42 inference(scs_inference,[],[299,311,100,243,201,97,404,194,149,258,111,396,366,86,21,17,16,19,20,18,23])).
% 60.10/60.42 cnf(416,plain,
% 60.10/60.42 (P2(f5(a3),a3)),
% 60.10/60.42 inference(scs_inference,[],[299,311,100,243,5,201,97,404,194,149,258,7,111,396,366,86,21,17,16,19,20,18,23,22])).
% 60.10/60.42 cnf(424,plain,
% 60.10/60.42 (P3(a3,f8(x4241,f8(x4242,a3)),a3)),
% 60.10/60.42 inference(scs_inference,[],[299,311,100,113,243,5,201,97,404,194,149,258,7,111,396,366,52,168,86,21,17,16,19,20,18,23,22,26,24])).
% 60.10/60.42 cnf(445,plain,
% 60.10/60.42 (P1(f8(x4451,a3),x4452,f8(x4453,a3))),
% 60.10/60.42 inference(scs_inference,[],[194,111,21])).
% 60.10/60.42 cnf(451,plain,
% 60.10/60.42 (P1(a3,f8(f8(x4511,a3),f8(x4511,a3)),f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[409,243,97,194,111,314,21,17,19])).
% 60.10/60.42 cnf(454,plain,
% 60.10/60.42 (P3(f4(f8(x4541,a3),f8(x4541,a3)),f4(a3,a3),f8(x4542,a3))),
% 60.10/60.42 inference(scs_inference,[],[409,44,243,97,194,111,360,314,21,17,19,16])).
% 60.10/60.42 cnf(457,plain,
% 60.10/60.42 (P3(f8(x4571,f8(x4572,a3)),f8(x4573,a3),f8(x4573,a3))),
% 60.10/60.42 inference(scs_inference,[],[162,409,44,243,201,97,194,111,360,314,21,17,19,16,18])).
% 60.10/60.42 cnf(458,plain,
% 60.10/60.42 (P3(f8(x4581,a3),f8(x4582,a3),f8(x4582,a3))),
% 60.10/60.42 inference(rename_variables,[],[162])).
% 60.10/60.42 cnf(460,plain,
% 60.10/60.42 (P2(a7,f8(f5(a1),a2))),
% 60.10/60.42 inference(scs_inference,[],[162,409,44,6,243,201,97,194,111,360,314,10,21,17,19,16,18,23])).
% 60.10/60.42 cnf(461,plain,
% 60.10/60.42 (P1(x4611,x4612,f8(x4611,x4612))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(463,plain,
% 60.10/60.42 (P1(f8(x4631,a3),x4632,f8(f8(x4633,a3),f8(a3,a3)))),
% 60.10/60.42 inference(scs_inference,[],[162,409,44,6,243,201,97,194,111,395,360,314,10,89,21,17,19,16,18,23,26])).
% 60.10/60.42 cnf(468,plain,
% 60.10/60.42 (P3(a3,f8(x4681,a3),f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,162,83,269,409,44,6,243,201,97,194,111,395,360,314,10,89,21,17,19,16,18,23,26,25])).
% 60.10/60.42 cnf(471,plain,
% 60.10/60.42 (P3(f4(a3,a3),f8(x4711,a3),f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,162,458,83,269,409,44,6,243,201,97,194,111,395,360,314,10,89,21,17,19,16,18,23,26,25,24])).
% 60.10/60.42 cnf(479,plain,
% 60.10/60.42 (P1(f8(x4791,a3),x4792,f8(x4791,a3))),
% 60.10/60.42 inference(rename_variables,[],[111])).
% 60.10/60.42 cnf(480,plain,
% 60.10/60.42 (P1(x4801,a3,a3)),
% 60.10/60.42 inference(rename_variables,[],[2])).
% 60.10/60.42 cnf(482,plain,
% 60.10/60.42 (P1(f4(a3,a3),a3,f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,162,458,83,269,409,44,6,243,201,97,194,111,479,395,360,314,74,10,461,89,2,480,21,17,19,16,18,23,26,25,24,27,31,30])).
% 60.10/60.42 cnf(493,plain,
% 60.10/60.42 (P1(a3,x4931,f8(f8(x4932,a3),f8(a3,a3)))),
% 60.10/60.42 inference(scs_inference,[],[36,463,21])).
% 60.10/60.42 cnf(496,plain,
% 60.10/60.42 (P3(f5(a3),f4(a3,a3),a3)),
% 60.10/60.42 inference(scs_inference,[],[44,36,416,463,21,16])).
% 60.10/60.42 cnf(497,plain,
% 60.10/60.42 (P3(x4971,f4(a3,a3),x4971)),
% 60.10/60.42 inference(rename_variables,[],[44])).
% 60.10/60.42 cnf(499,plain,
% 60.10/60.42 (P3(f5(f5(a3)),a3,a3)),
% 60.10/60.42 inference(scs_inference,[],[44,8,36,416,463,21,16,17])).
% 60.10/60.42 cnf(504,plain,
% 60.10/60.42 (P2(f8(f8(x5041,a3),f8(a3,a3)),f8(x5042,a3))),
% 60.10/60.42 inference(scs_inference,[],[44,8,258,36,416,482,463,445,21,16,17,20,23])).
% 60.10/60.42 cnf(505,plain,
% 60.10/60.42 (P1(f8(x5051,a3),x5052,f8(x5053,a3))),
% 60.10/60.42 inference(rename_variables,[],[445])).
% 60.10/60.42 cnf(507,plain,
% 60.10/60.42 (P3(f4(a3,f4(a3,a3)),f8(x5071,a3),f8(x5072,a3))),
% 60.10/60.42 inference(scs_inference,[],[156,44,8,149,258,36,416,482,463,445,21,16,17,20,23,18])).
% 60.10/60.42 cnf(510,plain,
% 60.10/60.42 (P1(f8(f8(x5101,a3),f8(a3,a3)),a2,f8(x5102,a3))),
% 60.10/60.42 inference(scs_inference,[],[156,44,8,6,149,258,36,416,482,463,445,505,21,16,17,20,23,18,26])).
% 60.10/60.42 cnf(514,plain,
% 60.10/60.42 (P3(a3,f5(f4(a3,a3)),f8(x5141,a3))),
% 60.10/60.42 inference(scs_inference,[],[156,83,401,252,44,8,6,149,258,36,416,482,463,445,505,21,16,17,20,23,18,26,25])).
% 60.10/60.42 cnf(520,plain,
% 60.10/60.42 (P3(f8(x5201,a3),f8(x5202,a3),a3)),
% 60.10/60.42 inference(scs_inference,[],[94,156,83,401,471,252,44,497,8,6,149,258,36,416,482,463,445,505,406,168,21,16,17,20,23,18,26,25,27,24])).
% 60.10/60.42 cnf(530,plain,
% 60.10/60.42 (~P1(x5301,x5302,f5(a3))+P1(x5301,x5302,a3)),
% 60.10/60.42 inference(scs_inference,[],[94,156,83,401,471,252,363,44,497,8,5,6,149,258,36,416,482,463,445,505,406,74,168,2,21,16,17,20,23,18,26,25,27,24,29,30,19])).
% 60.10/60.42 cnf(542,plain,
% 60.10/60.42 (P1(x5421,x5422,f8(x5421,x5422))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(544,plain,
% 60.10/60.42 (P1(a3,x5441,f8(x5442,a3))),
% 60.10/60.42 inference(scs_inference,[],[258,265,255,10,3,21,20,19])).
% 60.10/60.42 cnf(546,plain,
% 60.10/60.42 (P3(f5(a7),f8(f5(a1),a2),a3)),
% 60.10/60.42 inference(scs_inference,[],[8,258,265,255,10,3,460,21,20,19,17])).
% 60.10/60.42 cnf(549,plain,
% 60.10/60.42 (P3(a7,f4(a3,a3),f8(f5(a1),a2))),
% 60.10/60.42 inference(scs_inference,[],[44,8,258,265,255,10,3,460,21,20,19,17,16])).
% 60.10/60.42 cnf(556,plain,
% 60.10/60.42 (P1(a3,x5561,f8(f8(x5562,a3),f8(a3,a3)))),
% 60.10/60.42 inference(rename_variables,[],[493])).
% 60.10/60.42 cnf(558,plain,
% 60.10/60.42 (P1(f8(x5581,a3),x5582,a3)),
% 60.10/60.42 inference(scs_inference,[],[156,44,8,201,258,243,265,255,10,542,3,493,460,21,20,19,17,16,18,23,26])).
% 60.10/60.42 cnf(559,plain,
% 60.10/60.42 (P1(a3,x5591,a3)),
% 60.10/60.42 inference(rename_variables,[],[3])).
% 60.10/60.42 cnf(560,plain,
% 60.10/60.42 (P1(x5601,x5602,f8(x5601,x5602))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(562,plain,
% 60.10/60.42 (P3(f8(x5621,a3),f8(x5622,a3),f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,156,471,44,8,5,201,258,243,265,255,10,542,3,493,460,21,20,19,17,16,18,23,26,24])).
% 60.10/60.42 cnf(565,plain,
% 60.10/60.42 (P3(f4(a3,a3),a3,f8(x5651,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,156,471,363,44,8,5,201,258,243,265,255,10,542,3,493,460,21,20,19,17,16,18,23,26,24,25])).
% 60.10/60.42 cnf(567,plain,
% 60.10/60.42 (P1(x5671,f8(x5672,a3),f8(x5673,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,156,471,363,44,8,5,201,258,243,265,255,10,542,560,3,493,460,445,21,20,19,17,16,18,23,26,24,25,27])).
% 60.10/60.42 cnf(569,plain,
% 60.10/60.42 (P1(f8(x5691,a3),x5692,f8(x5693,a3))),
% 60.10/60.42 inference(rename_variables,[],[445])).
% 60.10/60.42 cnf(572,plain,
% 60.10/60.42 (P3(a3,f8(x5721,a3),f4(a3,a3))),
% 60.10/60.42 inference(rename_variables,[],[468])).
% 60.10/60.42 cnf(580,plain,
% 60.10/60.42 (P1(f4(a3,a3),x5801,f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,156,468,572,471,363,44,8,5,201,258,243,265,255,10,542,560,3,559,9,493,556,460,445,569,2,21,20,19,17,16,18,23,26,24,25,27,31,28,30])).
% 60.10/60.42 cnf(587,plain,
% 60.10/60.42 (P1(f8(x5871,a3),x5872,f8(a3,x5872))),
% 60.10/60.42 inference(scs_inference,[],[258,10,21])).
% 60.10/60.42 cnf(588,plain,
% 60.10/60.42 (P1(x5881,x5882,f8(x5881,x5882))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(590,plain,
% 60.10/60.42 (P1(x5901,a3,f4(a3,f4(a3,a3)))),
% 60.10/60.42 inference(scs_inference,[],[149,258,10,588,21,19])).
% 60.10/60.42 cnf(592,plain,
% 60.10/60.42 (P1(x5921,x5922,f8(x5921,x5922))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(594,plain,
% 60.10/60.42 (P1(x5941,a3,f8(x5941,f5(a3)))),
% 60.10/60.42 inference(scs_inference,[],[149,258,416,10,588,592,21,19,20])).
% 60.10/60.42 cnf(595,plain,
% 60.10/60.42 (P1(x5951,x5952,f8(x5951,x5952))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(601,plain,
% 60.10/60.42 (P1(a3,x6011,a3)),
% 60.10/60.42 inference(rename_variables,[],[3])).
% 60.10/60.42 cnf(602,plain,
% 60.10/60.42 (P1(x6021,x6022,f8(x6021,x6022))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(605,plain,
% 60.10/60.42 (P1(x6051,x6052,f8(x6051,x6052))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(606,plain,
% 60.10/60.42 (P1(x6061,f8(x6062,a3),f8(x6063,a3))),
% 60.10/60.42 inference(rename_variables,[],[567])).
% 60.10/60.42 cnf(609,plain,
% 60.10/60.42 (P1(x6091,x6092,f8(x6091,x6092))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(610,plain,
% 60.10/60.42 (P1(x6101,f8(x6102,a3),f8(x6103,a3))),
% 60.10/60.42 inference(rename_variables,[],[567])).
% 60.10/60.42 cnf(612,plain,
% 60.10/60.42 (P3(f5(a7),f8(f5(a1),a2),f8(x6121,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,156,549,8,6,149,258,412,416,10,588,592,595,602,605,3,567,606,21,19,20,18,23,26,27,25])).
% 60.10/60.42 cnf(615,plain,
% 60.10/60.42 (P3(f8(x6151,a3),f8(x6152,a3),f4(a3,f4(a3,a3)))),
% 60.10/60.42 inference(scs_inference,[],[94,156,471,549,8,6,149,258,412,416,10,588,592,595,602,605,3,9,567,606,21,19,20,18,23,26,27,25,24])).
% 60.10/60.42 cnf(618,plain,
% 60.10/60.42 (P1(a3,f4(a3,a3),f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,156,468,471,549,8,6,149,258,412,416,10,588,592,595,602,605,3,601,9,567,606,610,21,19,20,18,23,26,27,25,24,31])).
% 60.10/60.42 cnf(621,plain,
% 60.10/60.42 (P1(a3,x6211,a3)),
% 60.10/60.42 inference(rename_variables,[],[3])).
% 60.10/60.42 cnf(623,plain,
% 60.10/60.42 (P1(f8(x6231,a3),x6232,f8(f4(a3,a3),x6232))),
% 60.10/60.42 inference(scs_inference,[],[94,156,468,471,549,8,6,5,149,258,412,416,10,588,592,595,602,605,609,3,601,621,9,567,606,610,21,19,20,18,23,26,27,25,24,31,30])).
% 60.10/60.42 cnf(633,plain,
% 60.10/60.42 (P1(f8(x6331,a3),x6332,f8(f8(x6333,a3),x6332))),
% 60.10/60.42 inference(scs_inference,[],[194,10,21])).
% 60.10/60.42 cnf(634,plain,
% 60.10/60.42 (P1(x6341,x6342,f8(x6341,x6342))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(637,plain,
% 60.10/60.42 (P3(x6371,f4(a3,a3),x6371)),
% 60.10/60.42 inference(rename_variables,[],[44])).
% 60.10/60.42 cnf(640,plain,
% 60.10/60.42 (P1(x6401,x6402,f8(x6401,x6402))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(643,plain,
% 60.10/60.42 (P1(x6431,x6432,f8(x6431,x6432))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(645,plain,
% 60.10/60.42 (P3(a3,f4(a3,a3),f4(a3,f8(x6451,a3)))),
% 60.10/60.42 inference(scs_inference,[],[44,637,201,308,194,504,10,634,640,21,16,20,19,18])).
% 60.10/60.42 cnf(646,plain,
% 60.10/60.42 (P3(x6461,f4(a3,a3),x6461)),
% 60.10/60.42 inference(rename_variables,[],[44])).
% 60.10/60.42 cnf(648,plain,
% 60.10/60.42 (P2(f8(f8(x6481,a3),x6482),f8(a3,x6482))),
% 60.10/60.42 inference(scs_inference,[],[44,637,201,308,194,504,10,634,640,643,587,21,16,20,19,18,23])).
% 60.10/60.42 cnf(650,plain,
% 60.10/60.42 (P1(x6501,x6502,f8(x6501,x6502))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(654,plain,
% 60.10/60.42 (P1(x6541,x6542,f8(x6541,x6542))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(660,plain,
% 60.10/60.42 (P3(a7,a3,f8(f5(a1),a2))),
% 60.10/60.42 inference(scs_inference,[],[44,637,546,6,7,201,308,194,5,504,10,634,640,643,650,654,3,587,590,21,16,20,19,18,23,26,27,25])).
% 60.10/60.42 cnf(664,plain,
% 60.10/60.42 (P3(f5(f8(x6641,a3)),a3,a3)),
% 60.10/60.42 inference(scs_inference,[],[565,44,637,646,546,6,7,201,8,308,194,5,504,10,634,640,643,650,654,3,587,590,21,16,20,19,18,23,26,27,25,24])).
% 60.10/60.42 cnf(680,plain,
% 60.10/60.42 (P1(f8(a3,f8(a3,a3)),a2,f8(x6801,a3))),
% 60.10/60.42 inference(scs_inference,[],[510,648,21])).
% 60.10/60.42 cnf(687,plain,
% 60.10/60.42 (P1(x6871,f8(x6872,a3),f8(x6873,a3))),
% 60.10/60.42 inference(rename_variables,[],[567])).
% 60.10/60.42 cnf(689,plain,
% 60.10/60.42 (P3(f4(a3,a3),f4(a3,a3),f8(x6891,a3))),
% 60.10/60.42 inference(scs_inference,[],[363,201,258,36,510,567,648,21,19,20,16])).
% 60.10/60.42 cnf(695,plain,
% 60.10/60.42 (P1(f8(x6951,a3),x6952,f8(f4(a3,a3),x6952))),
% 60.10/60.42 inference(rename_variables,[],[623])).
% 60.10/60.42 cnf(696,plain,
% 60.10/60.42 (P1(x6961,f8(x6962,a3),f8(x6963,a3))),
% 60.10/60.42 inference(rename_variables,[],[567])).
% 60.10/60.42 cnf(699,plain,
% 60.10/60.42 (P1(f8(x6991,a3),x6992,f8(f4(a3,a3),x6992))),
% 60.10/60.42 inference(rename_variables,[],[623])).
% 60.10/60.42 cnf(701,plain,
% 60.10/60.42 (P1(x7011,f8(x7012,a3),f8(x7013,a3))),
% 60.10/60.42 inference(rename_variables,[],[567])).
% 60.10/60.42 cnf(703,plain,
% 60.10/60.42 (P1(x7031,f4(a3,a3),f8(f4(a3,a3),f4(a3,a3)))),
% 60.10/60.42 inference(scs_inference,[],[401,363,201,258,36,510,567,687,696,10,618,623,695,699,648,21,19,20,16,18,23,26,27])).
% 60.10/60.42 cnf(707,plain,
% 60.10/60.42 (P3(f8(x7071,a3),a3,f8(x7072,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,401,565,363,201,258,36,5,510,567,687,696,10,618,623,695,699,648,21,19,20,16,18,23,26,27,24])).
% 60.10/60.42 cnf(708,plain,
% 60.10/60.42 (P3(a3,x7081,x7081)),
% 60.10/60.42 inference(rename_variables,[],[5])).
% 60.10/60.42 cnf(710,plain,
% 60.10/60.42 (P3(a7,f8(x7101,a3),f8(f5(a1),a2))),
% 60.10/60.42 inference(scs_inference,[],[94,401,565,363,612,201,258,7,36,5,708,510,567,687,696,10,618,623,695,699,648,21,19,20,16,18,23,26,27,24,25])).
% 60.10/60.42 cnf(714,plain,
% 60.10/60.42 (P1(x7141,f4(a3,a3),f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,401,565,363,612,562,201,258,7,36,5,708,510,567,687,696,701,10,618,623,695,699,648,21,19,20,16,18,23,26,27,24,25,31])).
% 60.10/60.42 cnf(736,plain,
% 60.10/60.42 (P1(x7361,f8(x7362,a3),f8(x7363,f8(x7364,a3)))),
% 60.10/60.42 inference(scs_inference,[],[201,567,19])).
% 60.10/60.42 cnf(737,plain,
% 60.10/60.42 (P1(x7371,f8(x7372,a3),f8(x7373,a3))),
% 60.10/60.42 inference(rename_variables,[],[567])).
% 60.10/60.42 cnf(740,plain,
% 60.10/60.42 (P1(x7401,x7402,f8(x7401,x7402))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(742,plain,
% 60.10/60.42 (P3(f8(f5(a1),a2),f4(a3,a3),a7)),
% 60.10/60.42 inference(scs_inference,[],[44,201,460,567,10,19,20,18])).
% 60.10/60.42 cnf(743,plain,
% 60.10/60.42 (P3(x7431,f4(a3,a3),x7431)),
% 60.10/60.42 inference(rename_variables,[],[44])).
% 60.10/60.42 cnf(745,plain,
% 60.10/60.42 (P2(f8(x7451,f4(a3,a3)),f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[44,201,460,567,10,740,714,19,20,18,23])).
% 60.10/60.42 cnf(746,plain,
% 60.10/60.42 (P1(x7461,f4(a3,a3),f4(a3,a3))),
% 60.10/60.42 inference(rename_variables,[],[714])).
% 60.10/60.42 cnf(747,plain,
% 60.10/60.42 (P1(x7471,x7472,f8(x7471,x7472))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(749,plain,
% 60.10/60.42 (P1(a7,f8(x7491,a3),f8(f5(a1),f5(a3)))),
% 60.10/60.42 inference(scs_inference,[],[44,6,201,460,567,10,740,714,594,182,19,20,18,23,26])).
% 60.10/60.42 cnf(757,plain,
% 60.10/60.42 (P3(f4(a3,a3),f8(x7571,a3),f8(x7572,a3))),
% 60.10/60.42 inference(scs_inference,[],[401,44,689,6,201,460,567,10,740,747,714,746,594,182,19,20,18,23,26,27,25])).
% 60.10/60.42 cnf(766,plain,
% 60.10/60.42 (P1(x7661,f8(x7662,a3),f8(x7663,a3))),
% 60.10/60.42 inference(rename_variables,[],[567])).
% 60.10/60.42 cnf(767,plain,
% 60.10/60.42 (P3(f8(x7671,a3),f8(x7672,a3),f8(x7671,a3))),
% 60.10/60.42 inference(rename_variables,[],[156])).
% 60.10/60.42 cnf(774,plain,
% 60.10/60.42 (P3(f8(x7741,f4(a3,a3)),f4(a3,a3),f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,401,156,767,565,44,743,689,6,201,460,9,567,737,766,10,740,747,714,746,594,587,182,19,20,18,23,26,27,25,24,28,29,16])).
% 60.10/60.42 cnf(778,plain,
% 60.10/60.42 (P3(f5(a3),f4(a3,a3),f8(x7781,a3))),
% 60.10/60.42 inference(scs_inference,[],[496,258,16])).
% 60.10/60.42 cnf(784,plain,
% 60.10/60.42 (P2(f8(x7841,a3),f4(a3,f4(a3,a3)))),
% 60.10/60.42 inference(rename_variables,[],[149])).
% 60.10/60.42 cnf(788,plain,
% 60.10/60.42 (P1(x7881,f8(x7882,a3),f8(x7883,a3))),
% 60.10/60.42 inference(rename_variables,[],[567])).
% 60.10/60.42 cnf(793,plain,
% 60.10/60.42 (P1(f8(x7931,a3),x7932,f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[401,496,258,149,784,314,510,567,788,10,633,580,16,19,20,23,18,26])).
% 60.10/60.42 cnf(795,plain,
% 60.10/60.42 (P1(x7951,f8(x7952,a3),f8(x7953,a3))),
% 60.10/60.42 inference(rename_variables,[],[567])).
% 60.10/60.42 cnf(796,plain,
% 60.10/60.42 (P1(x7961,x7962,f8(x7961,x7962))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(806,plain,
% 60.10/60.42 (P3(a7,f8(x8061,a3),a7)),
% 60.10/60.42 inference(scs_inference,[],[401,507,496,471,615,742,258,149,784,314,510,567,788,795,10,796,633,749,580,16,19,20,23,18,26,27,25,24])).
% 60.10/60.42 cnf(814,plain,
% 60.10/60.42 (P1(a3,x8141,f8(x8142,f8(x8143,a3)))),
% 60.10/60.42 inference(scs_inference,[],[201,544,19])).
% 60.10/60.42 cnf(815,plain,
% 60.10/60.42 (P1(a3,x8151,f8(x8152,a3))),
% 60.10/60.42 inference(rename_variables,[],[544])).
% 60.10/60.42 cnf(817,plain,
% 60.10/60.42 (P2(a3,f8(x8171,f8(x8172,a3)))),
% 60.10/60.42 inference(scs_inference,[],[201,3,736,544,19,23])).
% 60.10/60.42 cnf(818,plain,
% 60.10/60.42 (P1(x8181,f8(x8182,a3),f8(x8183,f8(x8184,a3)))),
% 60.10/60.42 inference(rename_variables,[],[736])).
% 60.10/60.42 cnf(819,plain,
% 60.10/60.42 (P1(a3,x8191,a3)),
% 60.10/60.42 inference(rename_variables,[],[3])).
% 60.10/60.42 cnf(826,plain,
% 60.10/60.42 (P1(a3,x8261,a3)),
% 60.10/60.42 inference(rename_variables,[],[3])).
% 60.10/60.42 cnf(830,plain,
% 60.10/60.42 (P1(x8301,f8(x8302,a3),f8(x8303,f8(x8304,a3)))),
% 60.10/60.42 inference(rename_variables,[],[736])).
% 60.10/60.42 cnf(833,plain,
% 60.10/60.42 (P3(a3,a3,f8(x8331,a3))),
% 60.10/60.42 inference(rename_variables,[],[83])).
% 60.10/60.42 cnf(837,plain,
% 60.10/60.42 (P1(a3,x8371,a3)),
% 60.10/60.42 inference(rename_variables,[],[3])).
% 60.10/60.42 cnf(843,plain,
% 60.10/60.42 (P1(a3,x8431,a3)),
% 60.10/60.42 inference(rename_variables,[],[3])).
% 60.10/60.42 cnf(845,plain,
% 60.10/60.42 (P1(f8(x8451,f8(x8452,a3)),x8453,a3)),
% 60.10/60.42 inference(scs_inference,[],[94,401,83,833,44,645,6,201,9,3,819,826,837,843,745,736,818,830,544,815,89,182,19,23,18,26,27,25,31,29,21])).
% 60.10/60.42 cnf(849,plain,
% 60.10/60.42 (P3(f8(x8491,a3),x8492,a3)+~P3(f4(a3,a3),x8492,f5(a3))),
% 60.10/60.42 inference(scs_inference,[],[94,401,83,833,363,44,645,6,7,201,9,3,819,826,837,843,745,736,818,830,544,815,89,182,19,23,18,26,27,25,31,29,21,16,24])).
% 60.10/60.42 cnf(856,plain,
% 60.10/60.42 (P2(f8(x8561,a3),f4(a3,a3))),
% 60.10/60.42 inference(rename_variables,[],[314])).
% 60.10/60.42 cnf(858,plain,
% 60.10/60.42 (P1(x8581,f4(a3,a3),f8(x8582,a3))),
% 60.10/60.42 inference(scs_inference,[],[314,856,680,567,19,20])).
% 60.10/60.42 cnf(861,plain,
% 60.10/60.42 (P2(f8(x8611,a3),f8(x8612,f8(x8613,a3)))),
% 60.10/60.42 inference(scs_inference,[],[314,856,680,567,736,19,20,23])).
% 60.10/60.42 cnf(864,plain,
% 60.10/60.42 (P1(f8(x8641,a3),x8642,f8(x8643,f8(x8644,a3)))),
% 60.10/60.42 inference(scs_inference,[],[314,856,680,567,10,736,814,19,20,23,26])).
% 60.10/60.42 cnf(867,plain,
% 60.10/60.42 (P1(x8671,x8672,f8(x8671,x8672))),
% 60.10/60.42 inference(rename_variables,[],[10])).
% 60.10/60.42 cnf(869,plain,
% 60.10/60.42 (P1(x8691,f4(a3,a3),a3)),
% 60.10/60.42 inference(scs_inference,[],[314,856,680,567,10,867,558,736,814,451,19,20,23,26,27])).
% 60.10/60.42 cnf(883,plain,
% 60.10/60.42 (P3(a3,f8(f5(a1),a2),a7)),
% 60.10/60.42 inference(scs_inference,[],[460,5,17])).
% 60.10/60.42 cnf(886,plain,
% 60.10/60.42 (P1(a3,x8861,f8(f4(a3,a3),x8861))),
% 60.10/60.42 inference(scs_inference,[],[460,36,5,623,17,21])).
% 60.10/60.42 cnf(889,plain,
% 60.10/60.42 (P1(f8(x8891,f8(x8892,a3)),x8893,f8(x8894,a3))),
% 60.10/60.42 inference(scs_inference,[],[194,460,36,5,395,623,17,21,19])).
% 60.10/60.42 cnf(893,plain,
% 60.10/60.42 (P1(f8(x8931,a3),x8932,f8(a3,x8932))),
% 60.10/60.42 inference(rename_variables,[],[587])).
% 60.10/60.42 cnf(899,plain,
% 60.10/60.42 (P3(f5(a3),a3,f8(x8991,a3))),
% 60.10/60.42 inference(scs_inference,[],[83,499,194,6,460,7,36,5,395,623,587,893,17,21,19,23,26,25])).
% 60.10/60.42 cnf(922,plain,
% 60.10/60.42 (P1(f4(a3,f4(a3,a3)),x9221,f8(x9222,a3))),
% 60.10/60.42 inference(scs_inference,[],[149,445,21])).
% 60.10/60.42 cnf(923,plain,
% 60.10/60.42 (P2(f8(x9231,a3),f4(a3,f4(a3,a3)))),
% 60.10/60.42 inference(rename_variables,[],[149])).
% 60.10/60.42 cnf(925,plain,
% 60.10/60.42 (P1(a3,x9251,f4(a3,f4(a3,a3)))),
% 60.10/60.42 inference(scs_inference,[],[149,923,544,445,21,19])).
% 60.10/60.42 cnf(928,plain,
% 60.10/60.42 (P2(a3,f8(f8(x9281,a3),x9282))),
% 60.10/60.42 inference(scs_inference,[],[149,923,3,544,89,445,21,19,23])).
% 60.10/60.42 cnf(935,plain,
% 60.10/60.42 (P3(f5(f5(a3)),a3,f8(x9351,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,496,8,6,149,923,3,544,89,445,587,21,19,23,26,25])).
% 60.10/60.42 cnf(965,plain,
% 60.10/60.42 (P3(f8(f8(x9651,a3),x9652),f4(a3,a3),f8(x9653,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,83,496,817,3,928,17,21,16,18])).
% 60.10/60.42 cnf(967,plain,
% 60.10/60.42 (P1(a3,x9671,f4(a3,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,83,496,817,314,3,544,928,17,21,16,18,19])).
% 60.10/60.42 cnf(971,plain,
% 60.10/60.42 (P1(f8(x9711,a3),x9712,f8(x9713,a3))),
% 60.10/60.42 inference(rename_variables,[],[445])).
% 60.10/60.42 cnf(981,plain,
% 60.10/60.42 (P3(f5(a7),a7,f8(x9811,a3))),
% 60.10/60.42 inference(scs_inference,[],[94,311,83,496,806,8,6,817,314,3,544,623,445,971,10,858,928,17,21,16,18,19,23,26,27,25])).
% 60.10/60.42 cnf(1002,plain,
% 60.10/60.42 (P1(f8(x10021,f8(x10022,a3)),x10023,f8(a3,x10023))),
% 60.10/60.42 inference(scs_inference,[],[360,5,861,587,17,21])).
% 60.10/60.42 cnf(1007,plain,
% 60.10/60.42 (P1(a3,x10071,f8(f8(x10072,a3),x10073))),
% 60.10/60.42 inference(scs_inference,[],[496,360,5,861,3,587,928,17,21,16,19])).
% 60.10/60.42 cnf(1009,plain,
% 60.10/60.42 (P2(f8(a3,x10091),f8(x10092,a3))),
% 60.10/60.42 inference(scs_inference,[],[496,360,5,861,3,587,445,928,17,21,16,19,23])).
% 60.10/60.42 cnf(1010,plain,
% 60.10/60.42 (P1(f8(x10101,a3),x10102,f8(x10103,a3))),
% 60.10/60.42 inference(rename_variables,[],[445])).
% 60.10/60.42 cnf(1020,plain,
% 60.10/60.42 (P3(f5(a3),f8(x10201,a3),f8(x10202,a3))),
% 60.10/60.42 inference(scs_inference,[],[83,496,935,7,360,5,6,861,3,587,445,1010,10,928,869,17,21,16,19,23,26,27,25])).
% 60.10/60.42 cnf(1064,plain,
% 60.10/60.42 (P3(a3,a3,f5(a3))),
% 60.10/60.42 inference(scs_inference,[],[5,416,17])).
% 60.10/60.42 cnf(1067,plain,
% 60.10/60.42 (P1(f4(a3,a3),x10671,f8(x10672,a3))),
% 60.10/60.42 inference(scs_inference,[],[5,416,314,445,17,21])).
% 60.10/60.42 cnf(1070,plain,
% 60.10/60.42 (P2(f8(x10701,a3),f8(a3,x10702))),
% 60.10/60.42 inference(scs_inference,[],[5,416,314,445,587,17,21,23])).
% 60.10/60.42 cnf(1073,plain,
% 60.10/60.42 (P1(a3,x10731,f8(a3,x10732))),
% 60.10/60.42 inference(scs_inference,[],[5,416,314,544,445,587,17,21,23,19])).
% 60.10/60.42 cnf(1079,plain,
% 60.10/60.43 (P3(f5(a3),f8(x10791,f8(x10792,a3)),f5(a3))),
% 60.10/60.43 inference(scs_inference,[],[424,5,6,416,314,544,445,587,623,17,21,23,19,26,24])).
% 60.10/60.43 cnf(1085,plain,
% 60.10/60.43 (P3(x10851,x10852,f4(x10851,x10852))),
% 60.10/60.43 inference(rename_variables,[],[9])).
% 60.10/60.43 cnf(1086,plain,
% 60.10/60.43 (P1(a3,x10861,f8(x10862,a3))),
% 60.10/60.43 inference(rename_variables,[],[544])).
% 60.10/60.43 cnf(1092,plain,
% 60.10/60.43 (P1(a3,x10921,f8(x10922,a3))),
% 60.10/60.43 inference(rename_variables,[],[544])).
% 60.10/60.43 cnf(1097,plain,
% 60.10/60.43 (P1(a3,x10971,f8(x10972,a3))),
% 60.10/60.43 inference(rename_variables,[],[544])).
% 60.10/60.43 cnf(1107,plain,
% 60.10/60.43 (P3(f8(a3,f5(a1)),f4(a3,a3),f8(x11071,a3))),
% 60.10/60.43 inference(scs_inference,[],[94,401,565,162,83,424,252,5,6,9,1085,416,314,544,1086,1092,1097,3,445,587,623,182,1007,703,17,21,23,19,26,24,25,31,30,29,28,16,18])).
% 60.10/60.43 cnf(1111,plain,
% 60.10/60.43 (P1(f4(a3,f4(a3,a3)),x11111,f8(a3,x11111))),
% 60.10/60.43 inference(scs_inference,[],[565,149,928,587,17,21])).
% 60.10/60.43 cnf(1114,plain,
% 60.10/60.43 (P3(a3,f4(a3,a3),f8(a3,x11141))),
% 60.10/60.43 inference(scs_inference,[],[94,565,149,928,587,1070,17,21,16])).
% 60.10/60.43 cnf(1115,plain,
% 60.10/60.43 (P2(f8(x11151,a3),f8(a3,x11152))),
% 60.10/60.43 inference(rename_variables,[],[1070])).
% 60.10/60.43 cnf(1117,plain,
% 60.10/60.43 (P3(f8(a3,x11171),f4(a3,a3),f8(x11172,a3))),
% 60.10/60.43 inference(scs_inference,[],[94,401,565,149,928,587,1070,1115,17,21,16,18])).
% 60.10/60.43 cnf(1127,plain,
% 60.10/60.43 (P3(f8(a3,f5(a1)),f8(x11271,a3),f8(x11271,a3))),
% 60.10/60.43 inference(scs_inference,[],[94,401,565,1107,63,6,149,928,587,623,793,1070,1115,17,21,16,18,23,26,25])).
% 60.10/60.43 cnf(1131,plain,
% 60.10/60.43 (P1(a3,x11311,a3)),
% 60.10/60.43 inference(rename_variables,[],[3])).
% 60.10/60.43 cnf(1133,plain,
% 60.10/60.43 (P3(f5(a3),f5(a3),f5(a3))),
% 60.10/60.43 inference(scs_inference,[],[94,401,565,1107,1064,4,63,6,149,928,3,587,623,793,1070,1115,17,21,16,18,23,26,25,31,29])).
% 60.10/60.43 cnf(1136,plain,
% 60.10/60.43 (P1(f5(a3),x11361,f5(a3))),
% 60.10/60.43 inference(scs_inference,[],[94,401,565,1107,1064,4,63,6,149,928,3,1131,587,623,793,1070,1115,17,21,16,18,23,26,25,31,29,30])).
% 60.10/60.43 cnf(1138,plain,
% 60.10/60.43 (P3(f8(x11381,a3),f8(x11381,a3),f8(a3,x11382))),
% 60.10/60.43 inference(scs_inference,[],[94,401,565,162,1107,1064,4,63,6,149,928,544,3,1131,587,623,793,1070,1115,1073,17,21,16,18,23,26,25,31,29,30,28])).
% 60.10/60.43 cnf(1144,plain,
% 60.10/60.43 (P3(a3,f8(a3,x11441),f8(x11442,a3))),
% 60.10/60.43 inference(scs_inference,[],[311,1070,17])).
% 60.10/60.43 cnf(1149,plain,
% 60.10/60.43 (P2(f8(x11491,a3),f8(f4(a3,a3),x11492))),
% 60.10/60.43 inference(scs_inference,[],[311,928,544,445,623,1070,17,21,23])).
% 60.10/60.43 cnf(1152,plain,
% 60.10/60.43 (P1(f5(a3),x11521,a3)),
% 60.10/60.43 inference(scs_inference,[],[311,416,928,544,445,623,1136,1070,17,21,23,19])).
% 60.10/60.43 cnf(1158,plain,
% 60.10/60.43 (P3(a3,f5(a3),f8(x11581,a3))),
% 60.10/60.43 inference(scs_inference,[],[311,370,1079,7,6,416,928,544,445,623,925,1136,1070,17,21,23,19,26,25])).
% 60.10/60.43 cnf(1166,plain,
% 60.10/60.43 (P1(f8(a3,x11661),x11662,f8(a3,x11661))),
% 60.10/60.43 inference(scs_inference,[],[311,370,1079,1114,7,6,416,928,544,3,445,623,793,925,558,580,1136,1070,17,21,23,19,26,25,31,30])).
% 60.10/60.43 cnf(1177,plain,
% 60.10/60.43 (P3(f8(f4(a3,a3),x11771),f4(a3,a3),f8(x11772,a3))),
% 60.10/60.43 inference(scs_inference,[],[94,311,401,370,162,1079,1114,7,6,416,928,544,3,445,567,623,793,925,558,580,1136,1070,17,21,23,19,26,25,31,30,28,16,18])).
% 60.10/60.43 cnf(1182,plain,
% 60.10/60.43 (P3(f8(x11821,a3),f8(x11822,a3),f8(x11823,a3))),
% 60.10/60.43 inference(scs_inference,[],[409,504,17])).
% 60.10/60.43 cnf(1185,plain,
% 60.10/60.43 (P2(a3,f8(f4(a3,a3),x11851))),
% 60.10/60.43 inference(scs_inference,[],[409,504,3,886,17,23])).
% 60.10/60.43 cnf(1188,plain,
% 60.10/60.43 (P1(a3,x11881,f8(f4(a3,a3),x11882))),
% 60.10/60.43 inference(scs_inference,[],[409,504,3,544,886,1149,17,23,19])).
% 60.10/60.43 cnf(1195,plain,
% 60.10/60.43 (P3(f4(a3,a3),f8(a3,x11951),f8(x11952,a3))),
% 60.10/60.43 inference(scs_inference,[],[401,409,565,1114,504,6,3,544,182,886,590,1149,17,23,19,26,25])).
% 60.10/60.43 cnf(1198,plain,
% 60.10/60.43 (P3(a3,a3,f8(a3,x11981))),
% 60.10/60.43 inference(scs_inference,[],[401,409,565,156,1114,504,6,3,544,182,886,590,1073,1149,17,23,19,26,25,28])).
% 60.10/60.43 cnf(1225,plain,
% 60.10/60.43 (P3(f4(a3,a3),f8(x12251,a3),a3)),
% 60.10/60.43 inference(scs_inference,[],[311,565,496,520,6,314,544,587,736,922,1007,1185,17,21,16,23,26,25])).
% 60.10/60.43 cnf(1245,plain,
% 60.10/60.43 (P1(f8(a3,x12451),x12452,f8(a3,x12452))),
% 60.10/60.43 inference(scs_inference,[],[707,928,587,1070,17,21])).
% 60.10/60.43 cnf(1246,plain,
% 60.10/60.43 (P2(f8(x12461,a3),f8(a3,x12462))),
% 60.10/60.43 inference(rename_variables,[],[1070])).
% 60.10/60.43 cnf(1248,plain,
% 60.10/60.43 (P1(f8(x12481,a3),a3,f8(a3,x12482))),
% 60.10/60.43 inference(scs_inference,[],[707,928,587,1070,1246,17,21,19])).
% 60.10/60.43 cnf(1250,plain,
% 60.10/60.43 (P1(f8(x12501,a3),x12502,f8(a3,x12502))),
% 60.10/60.43 inference(rename_variables,[],[587])).
% 60.10/60.43 cnf(1262,plain,
% 60.10/60.43 (P1(a3,x12621,f5(a3))),
% 60.10/60.43 inference(scs_inference,[],[94,757,707,6,9,928,587,1250,1070,1246,182,633,858,1136,703,17,21,19,23,27,24,26])).
% 60.10/60.43 cnf(1266,plain,
% 60.10/60.43 (P3(f5(f5(a7)),f8(x12661,a3),a7)),
% 60.10/60.43 inference(scs_inference,[],[94,757,707,612,883,8,6,9,928,587,1250,1070,1246,182,633,858,1136,703,17,21,19,23,27,24,26,25])).
% 60.10/60.43 cnf(1283,plain,
% 60.10/60.43 (P2(f8(x12831,a3),f8(f4(a3,a3),x12832))),
% 60.10/60.43 inference(rename_variables,[],[1149])).
% 60.10/60.43 cnf(1288,plain,
% 60.10/60.43 (P2(a3,f8(a3,x12881))),
% 60.10/60.43 inference(scs_inference,[],[311,587,1149,1283,845,1002,17,21,23])).
% 60.10/60.43 cnf(1291,plain,
% 60.10/60.43 (P1(f8(x12911,a3),x12912,f8(a3,f8(a3,x12912)))),
% 60.10/60.43 inference(scs_inference,[],[311,587,1149,1283,845,567,1002,1111,17,21,23,26])).
% 60.10/60.43 cnf(1295,plain,
% 60.10/60.43 (P3(f5(a7),a7,f4(a3,a3))),
% 60.10/60.43 inference(scs_inference,[],[311,806,981,562,587,1149,1283,845,567,1002,1111,17,21,23,26,25])).
% 60.10/60.43 cnf(1299,plain,
% 60.10/60.43 (P3(f5(a3),f4(a3,a3),f8(a3,x12991))),
% 60.10/60.43 inference(scs_inference,[],[311,496,806,981,562,587,1149,1283,845,567,1002,1111,17,21,23,26,25,16])).
% 60.10/60.43 cnf(1311,plain,
% 60.10/60.43 (P2(a3,f4(a3,a3))),
% 60.10/60.43 inference(scs_inference,[],[707,544,1185,182,580,17,21,23])).
% 60.10/60.43 cnf(1312,plain,
% 60.10/60.43 (P1(f4(a3,a3),x13121,f4(a3,a3))),
% 60.10/60.43 inference(rename_variables,[],[580])).
% 60.10/60.43 cnf(1319,plain,
% 60.10/60.43 (P3(f8(x13191,a3),f8(a3,x13192),f8(x13193,a3))),
% 60.10/60.43 inference(scs_inference,[],[401,707,1114,6,544,1185,182,10,580,736,17,21,23,26,25])).
% 60.10/60.43 cnf(1326,plain,
% 60.10/60.43 (P3(f5(a3),f4(a3,a3),f4(a3,a3))),
% 60.10/60.43 inference(scs_inference,[],[401,707,496,1114,6,544,1185,182,10,580,1312,736,2,17,21,23,26,25,31,16])).
% 60.10/60.43 cnf(1335,plain,
% 60.10/60.43 (P1(f8(a3,x13351),x13352,f8(x13353,a3))),
% 60.10/60.43 inference(scs_inference,[],[544,1288,21])).
% 60.10/60.43 cnf(1337,plain,
% 60.10/60.43 (P2(f8(x13371,a3),f8(f8(x13372,a3),x13373))),
% 60.10/60.43 inference(scs_inference,[],[544,1007,1288,21,23])).
% 60.10/60.43 cnf(1342,plain,
% 60.10/60.43 (P1(x13421,f4(a3,a3),f8(x13422,a3))),
% 60.10/60.43 inference(rename_variables,[],[858])).
% 60.10/60.43 cnf(1347,plain,
% 60.10/60.43 (P1(f8(x13471,a3),a2,f8(a3,x13472))),
% 60.10/60.43 inference(scs_inference,[],[11,44,883,6,544,858,1007,1073,10,1288,21,23,27,24,26])).
% 60.10/60.43 cnf(1349,plain,
% 60.10/60.43 (P1(a3,x13491,f8(x13492,a3))),
% 60.10/60.43 inference(rename_variables,[],[544])).
% 60.10/60.43 cnf(1351,plain,
% 60.10/60.43 (P3(f4(a3,a3),a3,a3)),
% 60.10/60.43 inference(scs_inference,[],[11,565,44,113,520,883,6,544,858,1007,1073,10,1288,21,23,27,24,26,25])).
% 60.10/60.43 cnf(1360,plain,
% 60.10/60.43 (~P3(a6,f8(f5(a1),a2),f4(a3,a3))),
% 60.10/60.43 inference(scs_inference,[],[11,94,565,44,113,520,883,6,9,544,1349,858,1342,1007,1073,10,1288,21,23,27,24,26,25,30,15])).
% 60.10/60.43 cnf(1370,plain,
% 60.10/60.43 (P2(a3,f4(a3,f4(a3,a3)))),
% 60.10/60.43 inference(scs_inference,[],[3,1185,925,21,23])).
% 60.10/60.43 cnf(1383,plain,
% 60.10/60.43 (P3(a3,f8(x13831,a3),f4(f8(x13832,a3),f5(a3)))),
% 60.10/60.43 inference(scs_inference,[],[11,83,113,1158,883,6,9,3,1185,587,925,858,714,1245,21,23,24,27,26,25])).
% 60.10/60.43 cnf(1384,plain,
% 60.10/60.43 (P3(x13841,x13842,f4(x13841,x13842))),
% 60.10/60.43 inference(rename_variables,[],[9])).
% 60.10/60.43 cnf(1386,plain,
% 60.10/60.43 (P1(f8(x13861,a3),x13862,f4(a3,f8(x13863,a3)))),
% 60.10/60.43 inference(scs_inference,[],[11,94,83,113,1158,883,6,9,1384,3,1185,587,925,1067,858,714,1245,21,23,24,27,26,25,30])).
% 60.10/60.43 cnf(1390,plain,
% 60.10/60.43 (P3(f5(a3),f5(a3),a3)),
% 60.10/60.43 inference(scs_inference,[],[11,94,689,83,113,1158,883,6,9,1384,3,1185,587,925,1067,1136,858,714,1152,1245,21,23,24,27,26,25,30,28])).
% 60.10/60.43 cnf(1395,plain,
% 60.10/60.43 (~P3(a6,f8(f5(a1),a2),f8(x13951,a3))),
% 60.10/60.43 inference(scs_inference,[],[11,94,689,83,113,1158,883,6,9,1384,3,1185,587,925,1067,1136,858,714,1152,1245,21,23,24,27,26,25,30,28,15])).
% 60.10/60.43 cnf(1403,plain,
% 60.10/60.43 (P1(f8(a3,x14031),x14032,a3)),
% 60.10/60.43 inference(scs_inference,[],[3,1288,21])).
% 60.10/60.43 cnf(1405,plain,
% 60.10/60.43 (P2(f8(x14051,a3),f5(a3))),
% 60.10/60.43 inference(scs_inference,[],[3,1288,188,1136,21,23])).
% 60.10/60.43 cnf(1406,plain,
% 60.10/60.43 (P1(f5(a3),x14061,f5(a3))),
% 60.10/60.43 inference(rename_variables,[],[1136])).
% 60.10/60.43 cnf(1407,plain,
% 60.10/60.43 (P1(x14071,a3,f8(x14072,a3))),
% 60.10/60.43 inference(rename_variables,[],[188])).
% 60.10/60.43 cnf(1411,plain,
% 60.10/60.43 (P1(x14111,a3,f8(x14112,a3))),
% 60.10/60.43 inference(rename_variables,[],[188])).
% 60.10/60.43 cnf(1416,plain,
% 60.10/60.43 (P1(f8(x14161,a3),x14162,f5(a3))),
% 60.10/60.43 inference(scs_inference,[],[1395,507,612,6,3,1288,188,1407,1411,1136,1406,594,21,23,27,24,26])).
% 60.10/60.43 cnf(1420,plain,
% 60.10/60.43 (P3(f5(a7),f8(f5(a1),a2),f4(a3,a3))),
% 60.10/60.43 inference(scs_inference,[],[1395,507,612,981,562,710,6,3,1288,188,1407,1411,1136,1406,594,21,23,27,24,26,25])).
% 60.10/60.43 cnf(1424,plain,
% 60.10/60.43 (~P3(f5(a7),f4(a3,f4(a3,a3)),a6)),
% 60.10/60.43 inference(scs_inference,[],[1395,507,612,981,562,710,6,3,1288,188,1407,1411,1136,1406,594,21,23,27,24,26,25,15])).
% 60.10/60.43 cnf(1426,plain,
% 60.10/60.43 (P3(a3,f4(a3,a3),f5(a3))),
% 60.10/60.43 inference(scs_inference,[],[1395,94,507,612,981,562,710,6,3,1288,188,1407,1411,1136,1406,594,21,23,27,24,26,25,15,16])).
% 60.10/60.43 cnf(1432,plain,
% 60.10/60.43 (P1(f5(a3),x14321,f8(x14322,a3))),
% 60.10/60.43 inference(scs_inference,[],[445,1405,21])).
% 60.10/60.43 cnf(1435,plain,
% 60.10/60.43 (P2(f8(x14351,a3),f4(f8(a3,a3),f8(a3,a3)))),
% 60.10/60.43 inference(scs_inference,[],[544,445,74,1405,21,23])).
% 60.10/60.43 cnf(1436,plain,
% 60.10/60.43 (P1(x14361,a3,f4(f8(x14361,a3),f8(x14361,a3)))),
% 60.10/60.43 inference(rename_variables,[],[74])).
% 60.10/60.43 cnf(1437,plain,
% 60.10/60.43 (P1(a3,x14371,f8(x14372,a3))),
% 60.10/60.43 inference(rename_variables,[],[544])).
% 60.10/60.43 cnf(1454,plain,
% 60.10/60.43 (P1(f8(x14541,a3),x14542,f4(f8(x14543,a3),f8(x14544,a3)))),
% 60.10/60.43 inference(scs_inference,[],[1395,94,401,83,520,1420,1383,6,544,1437,9,445,1067,858,188,10,74,1436,1405,21,23,24,27,26,25,30])).
% 60.10/60.43 cnf(1462,plain,
% 60.10/60.43 (~P3(f5(a7),f8(x14621,a3),a6)),
% 60.10/60.43 inference(scs_inference,[],[1395,94,401,689,83,520,1420,1383,6,544,1437,9,445,1067,858,188,10,74,1436,1405,21,23,24,27,26,25,30,28,15])).
% 60.10/60.43 cnf(1464,plain,
% 60.10/60.43 (P3(a3,f4(a3,a3),f4(f8(a3,a3),f8(a3,a3)))),
% 60.10/60.43 inference(scs_inference,[],[1395,94,401,689,83,520,1420,1383,6,544,1437,9,445,1067,858,188,10,74,1436,1405,21,23,24,27,26,25,30,28,15,16])).
% 60.10/60.43 cnf(1471,plain,
% 60.10/60.43 (P1(f4(a3,a3),x14711,a3)),
% 60.10/60.43 inference(scs_inference,[],[3,1311,21])).
% 60.10/60.43 cnf(1476,plain,
% 60.10/60.43 (P2(f8(a3,x14761),f4(a3,a3))),
% 60.10/60.43 inference(scs_inference,[],[3,544,587,1311,793,1435,21,19,23])).
% 60.10/60.43 cnf(1486,plain,
% 60.10/60.43 (P3(f8(x14861,a3),a3,f4(a3,a3))),
% 60.10/60.43 inference(scs_inference,[],[1395,757,707,612,113,562,6,3,544,587,1311,793,858,736,1435,21,19,23,24,26,25])).
% 60.10/60.43 cnf(1490,plain,
% 60.10/60.43 (P3(f5(a3),f5(a3),f8(x14901,a3))),
% 60.10/60.43 inference(scs_inference,[],[1395,757,689,707,612,113,562,6,3,544,587,1311,793,1136,858,736,1435,1432,21,19,23,24,26,25,28])).
% 60.10/60.43 cnf(1495,plain,
% 60.10/60.43 (~P3(f5(a7),f4(a3,a3),a6)),
% 60.10/60.43 inference(scs_inference,[],[1395,757,689,707,612,113,562,6,3,544,587,1311,793,1136,858,736,1435,1432,21,19,23,24,26,25,28,15])).
% 60.10/60.43 cnf(1506,plain,
% 60.10/60.43 (P2(a3,f5(a3))),
% 60.10/60.43 inference(scs_inference,[],[565,3,587,1337,1262,1370,17,21,23])).
% 60.10/60.43 cnf(1517,plain,
% 60.10/60.43 (P3(f4(a3,a3),f8(x15171,a3),f4(f8(x15172,a3),f5(a3)))),
% 60.10/60.43 inference(scs_inference,[],[1395,565,83,1158,6,5,3,9,587,1337,1262,1370,1416,17,21,23,24,26,25])).
% 60.10/60.43 cnf(1531,plain,
% 60.10/60.43 (P3(f4(a3,a3),f5(a3),f8(x15311,a3))),
% 60.10/60.43 inference(scs_inference,[],[565,1506,17])).
% 60.10/60.43 cnf(1536,plain,
% 60.10/60.43 (P2(f8(x15361,a3),f4(a3,f8(x15362,a3)))),
% 60.10/60.43 inference(scs_inference,[],[565,445,1386,1435,1506,17,21,23])).
% 60.10/60.43 cnf(1544,plain,
% 60.10/60.43 (P1(a3,x15441,f8(x15442,a3))),
% 60.10/60.43 inference(rename_variables,[],[544])).
% 60.10/60.43 cnf(1551,plain,
% 60.10/60.43 (P3(f4(a3,f8(x15511,a3)),f4(a3,a3),f8(x15512,a3))),
% 60.10/60.43 inference(scs_inference,[],[1395,401,565,778,1464,1420,6,544,445,1188,1386,1435,1506,17,21,23,24,26,25,15,18])).
% 60.10/60.43 cnf(1553,plain,
% 60.10/60.43 (P1(a3,x15531,f4(a3,f8(x15532,a3)))),
% 60.10/60.43 inference(scs_inference,[],[1395,401,565,778,1464,1420,6,544,1544,445,1188,1386,1435,1506,17,21,23,24,26,25,15,18,19])).
% 60.10/60.43 cnf(1563,plain,
% 60.10/60.43 (P2(a3,f4(f8(a3,a3),f8(a3,a3)))),
% 60.10/60.43 inference(scs_inference,[],[707,3,1370,74,1506,17,21,23])).
% 60.10/60.43 cnf(1565,plain,
% 60.10/60.43 (P1(a3,x15651,a3)),
% 60.10/60.43 inference(rename_variables,[],[3])).
% 60.10/60.43 cnf(1567,plain,
% 60.10/60.43 (P1(f5(a1),a3,f4(a3,a3))),
% 60.10/60.43 inference(scs_inference,[],[707,6,3,1370,869,714,74,1506,17,21,23,27])).
% 60.10/60.43 cnf(1583,plain,
% 60.10/60.43 (~P3(f5(a7),f8(x15831,f8(x15832,a3)),a6)),
% 60.10/60.43 inference(scs_inference,[],[1395,689,457,707,612,1158,6,3,1565,9,1370,869,714,74,1506,1553,17,21,23,27,24,25,28,15])).
% 60.10/60.43 cnf(1597,plain,
% 60.10/60.43 (P2(f8(x15971,a3),f4(f8(x15972,a3),f8(x15973,a3)))),
% 60.10/60.43 inference(scs_inference,[],[707,445,1454,1536,1563,17,21,23])).
% 60.10/60.43 cnf(1605,plain,
% 60.10/60.43 (P3(a3,f4(a3,a3),f8(x16051,a3))),
% 60.10/60.43 inference(rename_variables,[],[94])).
% 60.10/60.43 cnf(1611,plain,
% 60.10/60.43 (P3(f4(f8(x16111,a3),f8(x16112,a3)),f4(a3,a3),f8(x16113,a3))),
% 60.10/60.43 inference(scs_inference,[],[1395,94,1605,401,707,454,1182,1517,1420,445,1454,1536,1563,17,21,23,24,25,15,16,18])).
% 60.10/60.43 cnf(1626,plain,
% 60.10/60.43 (P2(f8(x16261,a3),f4(f8(x16262,a3),f8(x16263,a3)))),
% 60.10/60.43 inference(rename_variables,[],[1597])).
% 60.10/60.43 cnf(1637,plain,
% 60.10/60.43 (~P3(f5(a7),a3,a6)),
% 60.10/60.43 inference(scs_inference,[],[1395,311,44,612,360,861,5,445,1597,1626,17,16,21,18,24])).
% 60.10/60.43 cnf(1652,plain,
% 60.10/60.43 (P3(a3,f8(x16521,a3),f8(a3,x16522))),
% 60.10/60.43 inference(scs_inference,[],[311,1637,1070,15,16])).
% 60.10/60.43 cnf(1657,plain,
% 60.10/60.43 (~P3(f8(f8(x16571,a3),x16572),f5(a7),a6)),
% 60.10/60.43 inference(scs_inference,[],[1395,311,965,1637,1420,817,1070,15,16,18,24])).
% 60.10/60.43 cnf(1686,plain,
% 60.10/60.43 (P2(f5(a3),f8(x16861,a3))),
% 60.10/60.43 inference(scs_inference,[],[311,1657,928,149,1136,1432,15,16,18,23])).
% 60.10/60.43 cnf(1689,plain,
% 60.10/60.43 (~P3(f8(a3,f5(a1)),f5(a7),a6)),
% 60.10/60.43 inference(scs_inference,[],[1395,311,612,1127,1657,928,149,1136,1432,15,16,18,23,24])).
% 60.10/60.43 cnf(1704,plain,
% 60.10/60.43 (~P3(f8(a3,x17041),f5(a7),a6)),
% 60.10/60.43 inference(scs_inference,[],[1395,311,1117,1689,1420,1185,1149,15,16,18,24])).
% 60.10/60.43 cnf(1707,plain,
% 60.10/60.43 (P3(a3,f4(f8(x17071,a3),f4(a3,a3)),f8(x17072,a3))),
% 60.10/60.43 inference(scs_inference,[],[1395,311,401,1117,1689,1420,1185,1149,9,15,16,18,24,25])).
% 60.10/60.43 cnf(1717,plain,
% 60.10/60.43 (P3(f8(a3,x17171),f8(x17172,a3),f8(x17173,a3))),
% 60.10/60.43 inference(scs_inference,[],[311,1704,1288,1337,15,16,18])).
% 60.10/60.43 cnf(1719,plain,
% 60.10/60.43 (P2(f4(a3,a3),f5(a3))),
% 60.10/60.43 inference(scs_inference,[],[311,1704,1288,714,1136,1337,15,16,18,23])).
% 60.10/60.43 cnf(1720,plain,
% 60.10/60.43 (P1(f5(a3),x17201,f5(a3))),
% 60.10/60.43 inference(rename_variables,[],[1136])).
% 60.10/60.43 cnf(1721,plain,
% 60.10/60.43 (P1(x17211,f4(a3,a3),f4(a3,a3))),
% 60.10/60.43 inference(rename_variables,[],[714])).
% 60.10/60.43 cnf(1725,plain,
% 60.10/60.43 (P1(x17251,f4(a3,a3),f4(a3,a3))),
% 60.10/60.43 inference(rename_variables,[],[714])).
% 60.10/60.43 cnf(1727,plain,
% 60.24/60.43 (~P3(f5(f5(a3)),f5(a7),a6)),
% 60.24/60.43 inference(scs_inference,[],[1395,311,935,546,1704,6,1288,714,1721,1136,1337,10,15,16,18,23,27,24])).
% 60.24/60.43 cnf(1730,plain,
% 60.24/60.43 (P1(f4(a3,a3),x17301,f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[1395,311,935,546,1704,6,1288,1067,714,1721,1725,1136,1720,1337,10,15,16,18,23,27,24,26])).
% 60.24/60.43 cnf(1731,plain,
% 60.24/60.43 (P1(f5(a3),x17311,f5(a3))),
% 60.24/60.43 inference(rename_variables,[],[1136])).
% 60.24/60.43 cnf(1732,plain,
% 60.24/60.43 (P1(x17321,f4(a3,a3),f4(a3,a3))),
% 60.24/60.43 inference(rename_variables,[],[714])).
% 60.24/60.43 cnf(1734,plain,
% 60.24/60.43 (P3(f4(a3,a3),f4(a3,a3),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[1395,311,689,935,546,1704,6,1288,1067,714,1721,1725,1732,1136,1720,1731,1337,10,15,16,18,23,27,24,26,28])).
% 60.24/60.43 cnf(1748,plain,
% 60.24/60.43 (P3(a3,f8(x17481,a3),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[311,1727,1405,15,16])).
% 60.24/60.43 cnf(1753,plain,
% 60.24/60.43 (P2(f4(a3,a3),a3)),
% 60.24/60.43 inference(scs_inference,[],[311,1727,714,1152,1405,1563,15,16,18,23])).
% 60.24/60.43 cnf(1755,plain,
% 60.24/60.43 (P1(x17551,f4(a3,a3),f4(a3,a3))),
% 60.24/60.43 inference(rename_variables,[],[714])).
% 60.24/60.43 cnf(1761,plain,
% 60.24/60.43 (~P3(f8(f4(a3,a3),x17611),f5(a7),a6)),
% 60.24/60.43 inference(scs_inference,[],[1395,311,1177,1420,1727,6,714,1755,1152,1405,703,1563,15,16,18,23,27,24])).
% 60.24/60.43 cnf(1775,plain,
% 60.24/60.43 (~P3(a6,f8(f5(a1),a2),f8(a3,x17751))),
% 60.24/60.43 inference(scs_inference,[],[1395,311,1144,1761,5,1536,15,16,24])).
% 60.24/60.43 cnf(1779,plain,
% 60.24/60.43 (P3(f5(f5(a7)),a3,a7)),
% 60.24/60.43 inference(scs_inference,[],[1395,311,1144,546,883,1761,8,5,1536,15,16,24,25])).
% 60.24/60.43 cnf(1783,plain,
% 60.24/60.43 (~P3(f8(f5(a1),a2),a6,f8(a3,x17831))),
% 60.24/60.43 inference(scs_inference,[],[1775,15])).
% 60.24/60.43 cnf(1788,plain,
% 60.24/60.43 (~P3(a6,f8(f5(a1),a2),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[1395,311,1158,1775,5,1597,15,16,24])).
% 60.24/60.43 cnf(1790,plain,
% 60.24/60.43 (P3(a3,x17901,x17901)),
% 60.24/60.43 inference(rename_variables,[],[5])).
% 60.24/60.43 cnf(1792,plain,
% 60.24/60.43 (P3(f5(f5(a7)),f4(a3,a3),a7)),
% 60.24/60.43 inference(scs_inference,[],[1395,311,1158,1295,1775,8,5,1790,1597,15,16,24,25])).
% 60.24/60.43 cnf(1799,plain,
% 60.24/60.43 (P2(f4(a3,a3),f8(x17991,a3))),
% 60.24/60.43 inference(scs_inference,[],[1788,714,889,15,23])).
% 60.24/60.43 cnf(1801,plain,
% 60.24/60.43 (P1(x18011,f4(a3,a3),f4(a3,a3))),
% 60.24/60.43 inference(rename_variables,[],[714])).
% 60.24/60.43 cnf(1803,plain,
% 60.24/60.43 (~P3(f8(a3,f8(x18031,a3)),f5(a6),a7)),
% 60.24/60.43 inference(scs_inference,[],[11,273,1788,8,714,889,15,23,24])).
% 60.24/60.43 cnf(1806,plain,
% 60.24/60.43 (P1(f4(a3,a3),x18061,f8(a3,f8(x18062,a3)))),
% 60.24/60.43 inference(scs_inference,[],[11,273,1788,8,1067,714,1801,889,1002,15,23,24,26])).
% 60.24/60.43 cnf(1811,plain,
% 60.24/60.43 (~P3(f5(a6),f8(a3,f8(x18111,a3)),a7)),
% 60.24/60.43 inference(scs_inference,[],[1803,15])).
% 60.24/60.43 cnf(1815,plain,
% 60.24/60.43 (~P3(f8(x18151,a3),f5(a6),a7)),
% 60.24/60.43 inference(scs_inference,[],[11,806,80,1803,8,460,15,18,24])).
% 60.24/60.43 cnf(1819,plain,
% 60.24/60.43 (~P3(f5(a6),f8(x18191,a3),a7)),
% 60.24/60.43 inference(scs_inference,[],[1815,15])).
% 60.24/60.43 cnf(1827,plain,
% 60.24/60.43 (~P3(a7,a3,f5(a6))),
% 60.24/60.43 inference(scs_inference,[],[1811,370,806,1815,861,1347,587,15,21,23,24])).
% 60.24/60.43 cnf(1836,plain,
% 60.24/60.43 (P3(f8(a3,x18361),f8(a3,x18361),f8(x18362,a3))),
% 60.24/60.43 inference(scs_inference,[],[1811,370,806,1815,861,1347,445,587,714,9,1416,15,21,23,24,26,28])).
% 60.24/60.43 cnf(1851,plain,
% 60.24/60.43 (P2(f8(a3,x18511),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[1827,1347,149,1416,15,21,23])).
% 60.24/60.43 cnf(1854,plain,
% 60.24/60.43 (~P3(f8(x18541,f4(a3,a3)),f5(a7),a6)),
% 60.24/60.43 inference(scs_inference,[],[1360,774,1420,1827,1347,149,1416,15,21,23,24])).
% 60.24/60.43 cnf(1860,plain,
% 60.24/60.43 (~P3(f8(x18601,a3),f8(f5(a1),a2),f5(a6))),
% 60.24/60.43 inference(scs_inference,[],[1360,83,774,883,1420,1827,1347,149,714,1416,633,15,21,23,24,26,25])).
% 60.24/60.43 cnf(1869,plain,
% 60.24/60.43 (P2(f4(a3,a3),f8(a3,f4(a3,a3)))),
% 60.24/60.43 inference(scs_inference,[],[1860,714,1002,15,23])).
% 60.24/60.43 cnf(1873,plain,
% 60.24/60.43 (~P3(f5(f8(x18731,a3)),f5(a6),a7)),
% 60.24/60.43 inference(scs_inference,[],[11,664,1860,8,714,1002,15,23,24])).
% 60.24/60.43 cnf(1879,plain,
% 60.24/60.43 (P1(f8(a3,x18791),a2,f8(a3,x18792))),
% 60.24/60.43 inference(scs_inference,[],[1854,1347,1070,15,21])).
% 60.24/60.43 cnf(1885,plain,
% 60.24/60.43 (~P3(f8(f5(a1),a2),a3,f5(a6))),
% 60.24/60.43 inference(scs_inference,[],[1819,468,742,1854,1347,1070,623,15,21,23,24])).
% 60.24/60.43 cnf(1892,plain,
% 60.24/60.43 (P3(f8(a3,x18921),f8(a3,x18921),a3)),
% 60.24/60.43 inference(scs_inference,[],[1819,468,742,1854,1347,558,1070,793,567,9,623,15,21,23,24,26,28])).
% 60.24/60.43 cnf(1899,plain,
% 60.24/60.43 (~P3(f5(f5(a3)),f5(a6),a7)),
% 60.24/60.43 inference(scs_inference,[],[11,499,1885,8,15,24])).
% 60.24/60.43 cnf(1903,plain,
% 60.24/60.43 (~P3(f5(a6),f5(f8(x19031,a3)),a7)),
% 60.24/60.43 inference(scs_inference,[],[1873,15])).
% 60.24/60.43 cnf(1918,plain,
% 60.24/60.43 (P3(f8(a3,x19181),f8(a3,x19181),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[1395,1551,1420,1873,1347,793,714,1149,9,633,864,15,21,23,24,26,28])).
% 60.24/60.43 cnf(1927,plain,
% 60.24/60.43 (P1(f8(a3,x19271),x19272,f8(a3,x19271))),
% 60.24/60.43 inference(rename_variables,[],[1166])).
% 60.24/60.43 cnf(1933,plain,
% 60.24/60.43 (~P3(f4(f8(x19331,a3),f8(x19332,a3)),f5(a7),a6)),
% 60.24/60.43 inference(scs_inference,[],[1395,1611,1420,1899,745,1166,1927,1002,15,21,23,24])).
% 60.24/60.43 cnf(1942,plain,
% 60.24/60.43 (P1(f4(a3,a3),a2,f8(a3,x19421))),
% 60.24/60.43 inference(scs_inference,[],[1933,1347,314,15,21])).
% 60.24/60.43 cnf(1948,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f5(a6),a7)),
% 60.24/60.43 inference(scs_inference,[],[11,1351,1933,8,1347,314,864,15,21,23,24])).
% 60.24/60.43 cnf(1955,plain,
% 60.24/60.43 (P3(f8(a3,x19551),f8(a3,x19551),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[11,1351,1933,8,1347,714,314,1416,9,864,1386,15,21,23,24,26,28])).
% 60.24/60.43 cnf(1960,plain,
% 60.24/60.43 (~P3(f5(a6),f4(a3,a3),a7)),
% 60.24/60.43 inference(scs_inference,[],[1948,15])).
% 60.24/60.43 cnf(1962,plain,
% 60.24/60.43 (~P3(f8(a3,a3),f5(a6),f8(f5(a1),a2))),
% 60.24/60.43 inference(scs_inference,[],[1783,1948,208,8,15,24])).
% 60.24/60.43 cnf(1976,plain,
% 60.24/60.43 (~P3(f8(f5(a1),a2),f4(a3,a3),f5(a6))),
% 60.24/60.43 inference(scs_inference,[],[1960,44,742,1962,1347,1337,1386,15,21,23,24])).
% 60.24/60.43 cnf(1990,plain,
% 60.24/60.43 (~P3(f8(x19901,a3),a6,f5(a7))),
% 60.24/60.43 inference(scs_inference,[],[11,1266,1976,8,15,24])).
% 60.24/60.43 cnf(1997,plain,
% 60.24/60.43 (P1(f5(a3),a2,f8(a3,x19971))),
% 60.24/60.43 inference(scs_inference,[],[1990,1347,1405,15,21])).
% 60.24/60.43 cnf(2003,plain,
% 60.24/60.43 (~P3(f4(f5(a7),f8(x20031,a3)),f4(a3,a3),a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,401,1990,1347,9,1405,1454,15,21,23,25])).
% 60.24/60.43 cnf(2025,plain,
% 60.24/60.43 (~P3(f4(f5(a7),f5(a3)),f4(a3,a3),a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,409,778,2003,1347,1070,9,1536,1291,15,21,18,23,25])).
% 60.24/60.43 cnf(2044,plain,
% 60.24/60.43 (~P3(f5(a6),f4(a3,a3),f8(f5(a1),a2))),
% 60.24/60.43 inference(scs_inference,[],[1960,409,883,2025,1347,5,1405,1597,15,21,18,24])).
% 60.24/60.43 cnf(2056,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f5(a6),f8(f5(a1),a2))),
% 60.24/60.43 inference(scs_inference,[],[2044,15])).
% 60.24/60.43 cnf(2058,plain,
% 60.24/60.43 (~P3(f4(a6,a7),f8(x20581,a3),a3)),
% 60.24/60.43 inference(scs_inference,[],[32,806,2044,9,15,25])).
% 60.24/60.43 cnf(2068,plain,
% 60.24/60.43 (~P3(f8(x20681,a3),f4(a6,a7),a3)),
% 60.24/60.43 inference(scs_inference,[],[2058,15])).
% 60.24/60.43 cnf(2070,plain,
% 60.24/60.43 (~P3(f4(f5(a7),f5(a3)),a3,a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,899,2058,9,15,25])).
% 60.24/60.43 cnf(2074,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f4(a6,a7),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[1462,899,2058,9,15,25,849])).
% 60.24/60.43 cnf(2079,plain,
% 60.24/60.43 (~P3(f4(a6,a7),f4(a3,a3),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[2074,15])).
% 60.24/60.43 cnf(2081,plain,
% 60.24/60.43 (~P3(f4(a7,a6),f4(a3,a3),a3)),
% 60.24/60.43 inference(scs_inference,[],[11,44,2074,9,15,25])).
% 60.24/60.43 cnf(2091,plain,
% 60.24/60.43 (~P3(f5(a3),f8(x20911,f8(x20912,a3)),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[2079,44,1079,2070,15,24])).
% 60.24/60.43 cnf(2099,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f4(a7,a6),a3)),
% 60.24/60.43 inference(scs_inference,[],[2081,15])).
% 60.24/60.43 cnf(2101,plain,
% 60.24/60.43 (P1(x21011,f4(a3,a3),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[2081,714,1719,15,19])).
% 60.24/60.43 cnf(2103,plain,
% 60.24/60.43 (P2(f4(a3,a3),f8(a3,f8(x21031,a3)))),
% 60.24/60.43 inference(scs_inference,[],[2081,714,1719,1806,15,19,23])).
% 60.24/60.43 cnf(2107,plain,
% 60.24/60.43 (~P3(f4(f5(a7),f5(a3)),f8(x21071,a3),a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,1020,2081,714,9,1719,1806,15,19,23,25])).
% 60.24/60.43 cnf(2121,plain,
% 60.24/60.43 (P1(f5(a1),f5(a3),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[2091,6,714,2101,15,27])).
% 60.24/60.43 cnf(2125,plain,
% 60.24/60.43 (~P3(f4(f5(a7),f8(a3,x21251)),f4(a3,a3),a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,1117,2091,6,714,9,2101,15,27,25])).
% 60.24/60.43 cnf(2137,plain,
% 60.24/60.43 (~P3(f4(f5(a7),f8(x21371,a3)),f8(x21372,a3),a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,1182,2125,9,15,25])).
% 60.24/60.43 cnf(2146,plain,
% 60.24/60.43 (~P3(f5(a7),f5(f4(a3,a3)),a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,514,2107,4,15,25])).
% 60.24/60.43 cnf(2155,plain,
% 60.24/60.43 (~P3(f5(f5(a7)),f8(x21551,a3),f5(a6))),
% 60.24/60.43 inference(scs_inference,[],[1903,1779,2137,7,15,24])).
% 60.24/60.43 cnf(2158,plain,
% 60.24/60.43 (~P3(f4(a6,f5(a3)),f4(a3,a3),f5(a7))),
% 60.24/60.43 inference(scs_inference,[],[92,1903,496,1779,2137,7,9,15,24,25])).
% 60.24/60.43 cnf(2164,plain,
% 60.24/60.43 (~P3(f5(a6),f8(x21641,a3),f8(f5(a1),a2))),
% 60.24/60.43 inference(scs_inference,[],[1819,883,2158,5,15,24])).
% 60.24/60.43 cnf(2167,plain,
% 60.24/60.43 (~P3(f4(f5(a7),f8(x21671,a3)),f8(a3,x21672),a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,1819,1319,883,2158,5,9,15,24,25])).
% 60.24/60.43 cnf(2172,plain,
% 60.24/60.43 (~P3(f8(x21721,a3),f5(a6),f8(f5(a1),a2))),
% 60.24/60.43 inference(scs_inference,[],[2164,15])).
% 60.24/60.43 cnf(2174,plain,
% 60.24/60.43 (~P3(a7,f5(f5(a6)),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[2056,660,2164,8,15,24])).
% 60.24/60.43 cnf(2183,plain,
% 60.24/60.43 (~P3(a7,f5(f5(a6)),f8(x21831,a3))),
% 60.24/60.43 inference(scs_inference,[],[2172,660,2146,8,15,24])).
% 60.24/60.43 cnf(2194,plain,
% 60.24/60.43 (P1(x21941,f4(a3,a3),f8(a3,f4(a3,a3)))),
% 60.24/60.43 inference(scs_inference,[],[2155,714,1869,15,19])).
% 60.24/60.43 cnf(2216,plain,
% 60.24/60.43 (~P3(f4(a6,a7),f4(a3,a3),a3)),
% 60.24/60.43 inference(scs_inference,[],[2079,1064,2174,6,714,5,2194,15,27,24])).
% 60.24/60.43 cnf(2219,plain,
% 60.24/60.43 (~P3(f4(f5(a7),f8(a3,x22191)),f8(x22192,a3),a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,2079,1717,1064,2174,6,714,5,9,2194,15,27,24,25])).
% 60.24/60.43 cnf(2242,plain,
% 60.24/60.43 (~P3(a7,a6,f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[2056,660,2216,7,15,24])).
% 60.24/60.43 cnf(2260,plain,
% 60.24/60.43 (~P3(f5(f5(a7)),a3,f5(a6))),
% 60.24/60.43 inference(scs_inference,[],[1811,370,1266,2167,15,24])).
% 60.24/60.43 cnf(2265,plain,
% 60.24/60.43 (~P3(f5(a7),f4(f8(x22651,a3),f4(a3,a3)),a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,1811,370,1707,1266,2167,4,15,24,25])).
% 60.24/60.43 cnf(2272,plain,
% 60.24/60.43 (P1(x22721,f4(a3,a3),f8(a3,f8(x22722,a3)))),
% 60.24/60.43 inference(scs_inference,[],[2219,714,2103,15,19])).
% 60.24/60.43 cnf(2274,plain,
% 60.24/60.43 (~P3(f5(f5(a7)),f4(a3,a3),f5(a6))),
% 60.24/60.43 inference(scs_inference,[],[1960,44,1792,2219,714,2103,15,19,24])).
% 60.24/60.43 cnf(2280,plain,
% 60.24/60.43 (P1(x22801,f5(a3),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[92,1960,44,180,1792,2219,714,4,2103,1734,15,19,24,25,31])).
% 60.24/60.43 cnf(2295,plain,
% 60.24/60.43 (~P3(f4(a6,f5(a7)),a7,f5(a7))),
% 60.24/60.43 inference(scs_inference,[],[129,1295,2260,6,714,9,2272,15,27,25])).
% 60.24/60.43 cnf(2314,plain,
% 60.24/60.43 (~P3(a7,a6,f8(x23141,a3))),
% 60.24/60.43 inference(scs_inference,[],[2172,660,2295,7,15,24])).
% 60.24/60.43 cnf(2317,plain,
% 60.24/60.43 (~P3(f4(a6,a7),f4(a3,a3),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[1360,2172,549,660,2295,7,9,15,24,25])).
% 60.24/60.43 cnf(2321,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f4(a6,a7),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[2317,15])).
% 60.24/60.43 cnf(2323,plain,
% 60.24/60.43 (~P3(f4(a6,a7),f8(x23231,a3),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[1360,710,2317,9,15,25])).
% 60.24/60.43 cnf(2329,plain,
% 60.24/60.43 (~P3(f8(x23291,a3),f4(a6,a7),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[2323,15])).
% 60.24/60.43 cnf(2331,plain,
% 60.24/60.43 (~P3(f4(a6,a7),a3,f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[1360,660,2323,9,15,25])).
% 60.24/60.43 cnf(2339,plain,
% 60.24/60.43 (~P3(a6,f5(f4(a3,a3)),f5(a7))),
% 60.24/60.43 inference(scs_inference,[],[92,44,2242,7,15,25])).
% 60.24/60.43 cnf(2348,plain,
% 60.24/60.43 (~P3(a3,f4(a6,a7),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[2331,15])).
% 60.24/60.43 cnf(2350,plain,
% 60.24/60.43 (~P3(f4(a7,a6),a3,a3)),
% 60.24/60.43 inference(scs_inference,[],[11,2331,4,9,15,25])).
% 60.24/60.43 cnf(2361,plain,
% 60.24/60.43 (~P3(f4(f5(a7),f5(a3)),f5(a3),a6)),
% 60.24/60.43 inference(scs_inference,[],[1462,2339,1490,9,15,25])).
% 60.24/60.43 cnf(2368,plain,
% 60.24/60.43 (~P3(a3,f4(a7,a6),a3)),
% 60.24/60.43 inference(scs_inference,[],[2350,15])).
% 60.24/60.43 cnf(2374,plain,
% 60.24/60.43 (~P3(a7,x23741,f8(x23742,a3))+~P3(x23741,f5(a6),f8(x23743,a3))),
% 60.24/60.43 inference(scs_inference,[],[1462,2172,710,2350,1836,9,15,25,24])).
% 60.24/60.43 cnf(2389,plain,
% 60.24/60.43 (P1(x23891,f8(x23892,a3),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[2361,714,1799,15,20])).
% 60.24/60.43 cnf(2391,plain,
% 60.24/60.43 (P2(f4(a3,a3),f8(a3,x23911))),
% 60.24/60.43 inference(scs_inference,[],[2361,714,1073,1799,15,20,23])).
% 60.24/60.43 cnf(2392,plain,
% 60.24/60.43 (P1(a3,x23921,f8(a3,x23922))),
% 60.24/60.43 inference(rename_variables,[],[1073])).
% 60.24/60.43 cnf(2393,plain,
% 60.24/60.43 (P1(x23931,f4(a3,a3),f4(a3,a3))),
% 60.24/60.43 inference(rename_variables,[],[714])).
% 60.24/60.43 cnf(2395,plain,
% 60.24/60.43 (P1(x23951,f8(a3,x23952),f8(a3,x23952))),
% 60.24/60.43 inference(scs_inference,[],[2361,714,2393,1073,1942,1799,15,20,23,27])).
% 60.24/60.43 cnf(2397,plain,
% 60.24/60.43 (P1(f4(a3,a3),x23971,f8(a3,x23972))),
% 60.24/60.43 inference(scs_inference,[],[2361,714,2393,1067,1073,2392,1942,1799,15,20,23,27,26])).
% 60.24/60.43 cnf(2398,plain,
% 60.24/60.43 (P1(a3,x23981,f8(a3,x23982))),
% 60.24/60.43 inference(rename_variables,[],[1073])).
% 60.24/60.43 cnf(2399,plain,
% 60.24/60.43 (P1(x23991,f4(a3,a3),f4(a3,a3))),
% 60.24/60.43 inference(rename_variables,[],[714])).
% 60.24/60.43 cnf(2404,plain,
% 60.24/60.43 (P3(f4(a3,a3),f4(a3,a3),f8(a3,x24041))),
% 60.24/60.43 inference(scs_inference,[],[92,689,2361,714,2393,2399,1067,1073,2392,2398,1942,1799,4,338,15,20,23,27,26,25,28])).
% 60.24/60.43 cnf(2407,plain,
% 60.24/60.43 (P1(x24071,f4(a3,a3),f4(a3,a3))),
% 60.24/60.43 inference(rename_variables,[],[714])).
% 60.24/60.43 cnf(2409,plain,
% 60.24/60.43 (P1(x24091,f4(a3,a3),f8(a3,x24092))),
% 60.24/60.43 inference(scs_inference,[],[92,689,2361,714,2393,2399,2407,1067,1073,2392,2398,1942,1799,4,338,15,20,23,27,26,25,28,19])).
% 60.24/60.43 cnf(2418,plain,
% 60.24/60.43 (P1(f5(a1),f8(a3,x24181),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[2274,6,714,2409,15,27])).
% 60.24/60.43 cnf(2471,plain,
% 60.24/60.43 (~P3(f4(a6,a7),f4(a3,a3),f8(x24711,a3))),
% 60.24/60.43 inference(scs_inference,[],[2079,1748,2183,5,15,24])).
% 60.24/60.43 cnf(2475,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f4(a6,a7),f8(x24751,a3))),
% 60.24/60.43 inference(scs_inference,[],[2471,15])).
% 60.24/60.43 cnf(2487,plain,
% 60.24/60.43 (~P3(f5(a3),f5(a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[2079,44,2265,1133,15,24])).
% 60.24/60.43 cnf(2528,plain,
% 60.24/60.43 (~P3(a6,a7,f8(x25281,a3))),
% 60.24/60.43 inference(scs_inference,[],[2314,15])).
% 60.24/60.43 cnf(2538,plain,
% 60.24/60.43 (P2(a6,f8(a1,a2))),
% 60.24/60.43 inference(scs_inference,[],[1,10,23])).
% 60.24/60.43 cnf(2539,plain,
% 60.24/60.43 (P1(x25391,x25392,f8(x25391,x25392))),
% 60.24/60.43 inference(rename_variables,[],[10])).
% 60.24/60.43 cnf(2541,plain,
% 60.24/60.43 (P3(f8(a1,a2),f4(a3,a3),a6)),
% 60.24/60.43 inference(scs_inference,[],[1,44,10,23,18])).
% 60.24/60.43 cnf(2542,plain,
% 60.24/60.43 (P3(x25421,f4(a3,a3),x25421)),
% 60.24/60.43 inference(rename_variables,[],[44])).
% 60.24/60.43 cnf(2544,plain,
% 60.24/60.43 (P3(a6,f4(a3,a3),f8(a1,a2))),
% 60.24/60.43 inference(scs_inference,[],[1,44,2542,10,23,18,16])).
% 60.24/60.43 cnf(2552,plain,
% 60.24/60.43 (P3(x25521,x25522,f4(x25521,x25522))),
% 60.24/60.43 inference(rename_variables,[],[9])).
% 60.24/60.43 cnf(2554,plain,
% 60.24/60.43 (P1(a1,a3,f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[1,11,44,2542,714,182,869,590,10,9,23,18,16,26,25,27])).
% 60.24/60.43 cnf(2559,plain,
% 60.24/60.43 (P1(x25591,x25592,f8(x25591,x25592))),
% 60.24/60.43 inference(rename_variables,[],[10])).
% 60.24/60.43 cnf(2560,plain,
% 60.24/60.43 (P3(x25601,x25602,f4(x25601,x25602))),
% 60.24/60.43 inference(rename_variables,[],[9])).
% 60.24/60.43 cnf(2568,plain,
% 60.24/60.43 (P3(f5(a6),f8(a1,a2),a3)),
% 60.24/60.43 inference(scs_inference,[],[1,11,44,2542,714,182,869,590,8,10,2539,2559,9,2552,2560,23,18,16,26,25,27,29,28,15,17])).
% 60.24/60.43 cnf(2578,plain,
% 60.24/60.43 (P3(f5(a6),f8(a1,a2),f8(x25781,a3))),
% 60.24/60.43 inference(scs_inference,[],[1,94,2544,182,594,8,26,25])).
% 60.24/60.43 cnf(2581,plain,
% 60.24/60.43 (P1(a1,f5(a3),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[1,94,2544,714,182,2101,594,8,26,25,27])).
% 60.24/60.43 cnf(2599,plain,
% 60.24/60.43 (P3(a3,f8(a1,a2),a6)),
% 60.24/60.43 inference(scs_inference,[],[5,2538,17])).
% 60.24/60.43 cnf(2606,plain,
% 60.24/60.43 (~P3(a3,f8(a1,a2),f5(a7))),
% 60.24/60.43 inference(scs_inference,[],[1,92,2568,869,86,7,5,2538,17,26,25])).
% 60.24/60.43 cnf(2609,plain,
% 60.24/60.43 (~P3(f8(a1,a2),f8(a3,f8(x26091,a3)),f5(a7))),
% 60.24/60.43 inference(scs_inference,[],[1,92,1583,2568,2541,869,86,7,5,1918,2538,17,26,25,24])).
% 60.24/60.43 cnf(2635,plain,
% 60.24/60.43 (~P3(f4(f5(a7),f5(a6)),f8(a1,a2),a6)),
% 60.24/60.43 inference(scs_inference,[],[1,1462,2578,2609,714,10,9,15,26,25])).
% 60.24/60.43 cnf(2725,plain,
% 60.24/60.43 (~P3(f8(a1,a2),f8(f5(a1),a2),f8(a3,x27251))),
% 60.24/60.43 inference(scs_inference,[],[1395,398,1144,2599,2635,1070,1506,15,18,16,24])).
% 60.24/60.43 cnf(2728,plain,
% 60.24/60.43 (P1(a1,f8(a3,x27281),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[1,1395,398,1144,2599,2635,714,1070,1506,2409,15,18,16,24,27])).
% 60.24/60.43 cnf(2749,plain,
% 60.24/60.43 (~P3(f8(a1,a2),f8(f5(a1),a2),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[1395,398,1158,2599,2725,1405,15,16,24])).
% 60.24/60.43 cnf(2774,plain,
% 60.24/60.43 (~P3(f8(a1,a2),f4(a3,a3),f5(a7))),
% 60.24/60.43 inference(scs_inference,[],[1495,44,2541,2749,15,24])).
% 60.24/60.43 cnf(2791,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f8(a1,a2),f5(a7))),
% 60.24/60.43 inference(scs_inference,[],[2774,15])).
% 60.24/60.43 cnf(2793,plain,
% 60.24/60.43 (~P3(f5(f4(a3,a3)),f4(a6,a7),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[2348,2774,103,15,18])).
% 60.24/60.43 cnf(2795,plain,
% 60.24/60.43 (P1(f8(a3,x27951),f8(x27952,a3),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[2348,2774,103,1997,1136,567,15,18,26])).
% 60.24/60.43 cnf(2819,plain,
% 60.24/60.43 (~P3(a3,f4(a6,a7),a3)),
% 60.24/60.43 inference(scs_inference,[],[2068,2793,258,15,18])).
% 60.24/60.43 cnf(2822,plain,
% 60.24/60.43 (~P3(f5(a7),f4(a3,f4(a3,a3)),f8(a1,a2))),
% 60.24/60.43 inference(scs_inference,[],[2068,1424,2599,2793,258,5,15,18,24])).
% 60.24/60.43 cnf(2838,plain,
% 60.24/60.43 (~P3(f4(f8(x28381,a3),f8(x28381,a3)),f4(a6,a7),a3)),
% 60.24/60.43 inference(scs_inference,[],[2068,2822,360,15,18])).
% 60.24/60.43 cnf(2885,plain,
% 60.24/60.43 (~P3(f4(a6,a7),a3,a3)),
% 60.24/60.43 inference(scs_inference,[],[2819,15])).
% 60.24/60.43 cnf(3030,plain,
% 60.24/60.43 (~P3(f5(a3),f4(a6,a7),a3)),
% 60.24/60.43 inference(scs_inference,[],[2068,2838,1686,15,18])).
% 60.24/60.43 cnf(3068,plain,
% 60.24/60.43 (~P3(f4(a6,a7),f5(a3),a3)),
% 60.24/60.43 inference(scs_inference,[],[3030,15])).
% 60.24/60.43 cnf(3448,plain,
% 60.24/60.43 (P1(x34481,f5(a3),a3)),
% 60.24/60.43 inference(scs_inference,[],[2280,530])).
% 60.24/60.43 cnf(3450,plain,
% 60.24/60.43 (P3(f4(a3,a3),a3,f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[1426,2280,530,15])).
% 60.24/60.43 cnf(3452,plain,
% 60.24/60.43 (~P2(a3,f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[2329,1486,1426,2280,530,15,17])).
% 60.24/60.43 cnf(3453,plain,
% 60.24/60.43 (P3(f8(x34531,a3),a3,f4(a3,a3))),
% 60.24/60.43 inference(rename_variables,[],[1486])).
% 60.24/60.43 cnf(3455,plain,
% 60.24/60.43 (P1(x34551,f5(a3),f8(a3,x34552))),
% 60.24/60.43 inference(scs_inference,[],[2329,1486,1426,1851,2395,2280,530,15,17,20])).
% 60.24/60.43 cnf(3456,plain,
% 60.24/60.43 (P1(x34561,f8(a3,x34562),f8(a3,x34562))),
% 60.24/60.43 inference(rename_variables,[],[2395])).
% 60.24/60.43 cnf(3458,plain,
% 60.24/60.43 (P2(f5(a3),f8(a3,x34581))),
% 60.24/60.43 inference(scs_inference,[],[2329,1486,1426,1851,2397,1730,2395,2280,530,15,17,20,23])).
% 60.24/60.43 cnf(3459,plain,
% 60.24/60.43 (P1(f4(a3,a3),x34591,f5(a3))),
% 60.24/60.43 inference(rename_variables,[],[1730])).
% 60.24/60.43 cnf(3461,plain,
% 60.24/60.43 (P1(f5(a3),a3,f8(a3,x34611))),
% 60.24/60.43 inference(scs_inference,[],[2329,1486,1426,1248,1851,2397,1730,2395,2280,530,15,17,20,23,21])).
% 60.24/60.43 cnf(3465,plain,
% 60.24/60.43 (P3(f8(x34651,a3),a3,f8(a3,x34652))),
% 60.24/60.43 inference(scs_inference,[],[2329,1486,3453,1426,2391,1248,1851,2397,1730,2395,2280,530,15,17,20,23,21,16])).
% 60.24/60.43 cnf(3467,plain,
% 60.24/60.43 (~P2(f8(x34671,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[2329,1486,3453,1426,2391,1248,1851,2331,2397,1730,2395,2280,530,15,17,20,23,21,16,18])).
% 60.24/60.43 cnf(3469,plain,
% 60.24/60.43 (P1(a1,a3,f8(a3,x34691))),
% 60.24/60.43 inference(scs_inference,[],[2329,2554,1486,3453,1426,2391,1248,1851,2331,2397,1730,2395,2280,530,15,17,20,23,21,16,18,19])).
% 60.24/60.43 cnf(3472,plain,
% 60.24/60.43 (P1(f4(a3,a3),x34721,f8(a3,x34722))),
% 60.24/60.43 inference(rename_variables,[],[2397])).
% 60.24/60.43 cnf(3475,plain,
% 60.24/60.43 (P3(f8(x34751,a3),f5(a3),f8(a3,x34752))),
% 60.24/60.43 inference(scs_inference,[],[2329,2554,1486,3453,1426,2404,2391,1248,1851,2331,2397,1730,3459,2395,2280,530,15,17,20,23,21,16,18,19,26,25])).
% 60.24/60.43 cnf(3477,plain,
% 60.24/60.43 (P1(a1,f8(a3,x34771),f8(a3,x34772))),
% 60.24/60.43 inference(scs_inference,[],[2329,2554,1486,3453,1426,2404,2391,1248,1851,2331,2397,3472,1730,3459,2395,3456,2280,530,15,17,20,23,21,16,18,19,26,25,27])).
% 60.24/60.43 cnf(3478,plain,
% 60.24/60.43 (P1(f4(a3,a3),x34781,f8(a3,x34782))),
% 60.24/60.43 inference(rename_variables,[],[2397])).
% 60.24/60.43 cnf(3481,plain,
% 60.24/60.43 (P3(f8(a3,x34811),a3,f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[2329,2554,1486,3453,1426,2404,2391,1652,1248,1851,2331,2397,3472,1730,3459,2395,3456,2280,530,15,17,20,23,21,16,18,19,26,25,27,24])).
% 60.24/60.43 cnf(3484,plain,
% 60.24/60.43 (P1(a1,f8(x34841,a3),f8(a3,x34842))),
% 60.24/60.43 inference(scs_inference,[],[2329,2554,2728,1486,3453,1426,2404,2391,1652,1248,1851,2331,2397,3472,1836,1730,3459,2395,3456,2280,530,15,17,20,23,21,16,18,19,26,25,27,24,31])).
% 60.24/60.43 cnf(3487,plain,
% 60.24/60.43 (P1(f8(a3,x34871),x34872,f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[2329,2554,2728,1486,3453,1426,1955,2404,2391,1652,1248,1851,2331,2397,3472,3478,1836,1730,3459,2395,3456,2280,530,15,17,20,23,21,16,18,19,26,25,27,24,31,30])).
% 60.24/60.43 cnf(3491,plain,
% 60.24/60.43 (~P1(f8(a3,x34911),f5(a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[2487,2329,2554,2728,1486,3453,1426,2795,1955,2404,2391,1652,1248,1851,2331,2397,3472,3478,1836,1730,3459,2395,3456,2280,530,15,17,20,23,21,16,18,19,26,25,27,24,31,30,28])).
% 60.24/60.43 cnf(3492,plain,
% 60.24/60.43 (P1(f8(a3,x34921),f8(x34922,a3),f5(a3))),
% 60.24/60.43 inference(rename_variables,[],[2795])).
% 60.24/60.43 cnf(3493,plain,
% 60.24/60.43 (P3(f8(a3,x34931),f8(a3,x34931),f5(a3))),
% 60.24/60.43 inference(rename_variables,[],[1955])).
% 60.24/60.43 cnf(3495,plain,
% 60.24/60.43 (~P1(f5(a3),f8(x34951,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[2487,2329,2554,2728,1486,3453,1426,2795,3492,1955,3493,2404,2391,1652,1248,1851,2331,2397,3472,3478,1836,1730,3459,2395,3456,2280,530,15,17,20,23,21,16,18,19,26,25,27,24,31,30,28,29])).
% 60.24/60.43 cnf(3498,plain,
% 60.24/60.43 (~P3(f4(a3,a3),a3,f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[2487,2329,2554,2728,1486,3453,1426,2795,3492,1955,3493,2404,2391,1652,1248,1851,2331,1351,2397,3472,3478,1836,1730,3459,2395,3456,2280,530,15,17,20,23,21,16,18,19,26,25,27,24,31,30,28,29,22])).
% 60.24/60.43 cnf(3500,plain,
% 60.24/60.43 (P3(f5(a3),f8(x35001,a3),f8(a3,x35002))),
% 60.24/60.43 inference(scs_inference,[],[3475,15])).
% 60.24/60.43 cnf(3503,plain,
% 60.24/60.43 (P3(f8(x35031,a3),f5(a3),f8(a3,x35032))),
% 60.24/60.43 inference(rename_variables,[],[3475])).
% 60.24/60.43 cnf(3504,plain,
% 60.24/60.43 (~P2(f8(x35041,a3),f4(a6,a7))),
% 60.24/60.43 inference(rename_variables,[],[3467])).
% 60.24/60.43 cnf(3506,plain,
% 60.24/60.43 (~P1(f8(a3,x35061),f4(a3,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3467,3491,3475,1719,15,22,20])).
% 60.24/60.43 cnf(3508,plain,
% 60.24/60.43 (~P2(f5(a7),a6)),
% 60.24/60.43 inference(scs_inference,[],[11,3467,3491,3475,1719,7,15,22,20,17])).
% 60.24/60.43 cnf(3511,plain,
% 60.24/60.43 (~P1(x35111,f5(a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[11,3467,3504,3455,3491,3475,1719,7,15,22,20,17,23])).
% 60.24/60.43 cnf(3513,plain,
% 60.24/60.43 (P1(x35131,f5(a3),f8(a3,x35132))),
% 60.24/60.43 inference(rename_variables,[],[3455])).
% 60.24/60.43 cnf(3515,plain,
% 60.24/60.43 (~P1(f4(a3,a3),f8(x35151,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[11,3467,3504,3455,3491,3495,3475,1719,7,15,22,20,17,23,21])).
% 60.24/60.43 cnf(3520,plain,
% 60.24/60.43 (~P2(f5(a6),a7)),
% 60.24/60.43 inference(scs_inference,[],[11,3467,3504,3455,3491,3495,3475,1719,7,8,9,15,22,20,17,23,21,16,18])).
% 60.24/60.43 cnf(3523,plain,
% 60.24/60.43 (~P2(f8(a3,x35231),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[11,3467,3504,3455,3513,3491,3495,3475,1719,7,8,9,15,22,20,17,23,21,16,18,19])).
% 60.24/60.43 cnf(3524,plain,
% 60.24/60.43 (P1(x35241,f5(a3),f8(a3,x35242))),
% 60.24/60.43 inference(rename_variables,[],[3455])).
% 60.24/60.43 cnf(3527,plain,
% 60.24/60.43 (~P1(f8(a3,x35271),f5(a3),f4(a6,a7))),
% 60.24/60.43 inference(rename_variables,[],[3491])).
% 60.24/60.43 cnf(3528,plain,
% 60.24/60.43 (P1(x35281,f5(a3),f8(a3,x35282))),
% 60.24/60.43 inference(rename_variables,[],[3455])).
% 60.24/60.43 cnf(3529,plain,
% 60.24/60.43 (P1(x35291,f5(a3),f8(a3,x35292))),
% 60.24/60.43 inference(rename_variables,[],[3455])).
% 60.24/60.43 cnf(3532,plain,
% 60.24/60.43 (P3(f8(x35321,a3),f5(a3),f8(a3,x35322))),
% 60.24/60.43 inference(rename_variables,[],[3475])).
% 60.24/60.43 cnf(3535,plain,
% 60.24/60.43 (P1(f5(a3),f8(a3,x35351),f8(a3,x35352))),
% 60.24/60.43 inference(scs_inference,[],[11,3467,3504,3455,3513,3524,3529,3528,3491,3495,3475,3503,2475,1195,1719,7,8,9,15,22,20,17,23,21,16,18,19,26,25,27])).
% 60.24/60.43 cnf(3538,plain,
% 60.24/60.43 (P1(x35381,f5(a3),f8(a3,x35382))),
% 60.24/60.43 inference(rename_variables,[],[3455])).
% 60.24/60.43 cnf(3540,plain,
% 60.24/60.43 (~P3(f8(a3,x35401),f8(x35402,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[11,3467,3504,3455,3513,3524,3529,3528,3491,3495,3475,3503,3532,3068,2475,1195,1892,1719,7,8,9,15,22,20,17,23,21,16,18,19,26,25,27,24])).
% 60.24/60.43 cnf(3541,plain,
% 60.24/60.43 (P3(f8(x35411,a3),f5(a3),f8(a3,x35412))),
% 60.24/60.43 inference(rename_variables,[],[3475])).
% 60.24/60.43 cnf(3544,plain,
% 60.24/60.43 (P1(x35441,f5(a3),f8(a3,x35442))),
% 60.24/60.43 inference(rename_variables,[],[3455])).
% 60.24/60.43 cnf(3545,plain,
% 60.24/60.43 (P1(x35451,f5(a3),f8(a3,x35452))),
% 60.24/60.43 inference(rename_variables,[],[3455])).
% 60.24/60.43 cnf(3547,plain,
% 60.24/60.43 (~P3(f8(a3,x35471),f8(a3,x35472),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[11,3467,3504,3455,3513,3524,3529,3538,3545,3544,3528,3491,3527,3495,3475,3503,3532,3541,3068,2475,1195,1892,1719,1133,7,8,9,15,22,20,17,23,21,16,18,19,26,25,27,24,31,30])).
% 60.24/60.43 cnf(3561,plain,
% 60.24/60.43 (P3(a3,f8(a3,x35611),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[3481,15])).
% 60.24/60.43 cnf(3563,plain,
% 60.24/60.43 (~P3(f5(a3),f8(x35631,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3523,3500,3481,15,22])).
% 60.24/60.43 cnf(3564,plain,
% 60.24/60.43 (~P2(f8(a3,x35641),f4(a6,a7))),
% 60.24/60.43 inference(rename_variables,[],[3523])).
% 60.24/60.43 cnf(3566,plain,
% 60.24/60.43 (P3(f8(x35661,a3),f4(a3,a3),f8(a3,x35662))),
% 60.24/60.43 inference(scs_inference,[],[3523,3500,3465,3481,1311,15,22,17])).
% 60.24/60.43 cnf(3568,plain,
% 60.24/60.43 (P1(x35681,f8(a3,x35682),f8(a3,x35683))),
% 60.24/60.43 inference(scs_inference,[],[3523,3500,3458,3465,3481,3455,1311,15,22,17,20])).
% 60.24/60.43 cnf(3573,plain,
% 60.24/60.43 (P1(f8(a3,x35731),a3,f8(a3,x35732))),
% 60.24/60.43 inference(scs_inference,[],[3523,3564,3500,3458,3465,3477,3461,3481,3455,1311,15,22,17,20,23,21])).
% 60.24/60.43 cnf(3575,plain,
% 60.24/60.43 (~P2(f5(a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3523,3564,3500,3458,3465,3477,3450,3461,3481,3498,3455,1311,15,22,17,20,23,21,16])).
% 60.24/60.43 cnf(3577,plain,
% 60.24/60.43 (P3(f8(a3,x35771),f8(x35772,a3),f8(a3,x35773))),
% 60.24/60.43 inference(scs_inference,[],[3523,3564,3500,3458,3465,3477,3450,3461,3481,3498,3455,1311,15,22,17,20,23,21,16,18])).
% 60.24/60.43 cnf(3579,plain,
% 60.24/60.43 (P1(f5(a3),a3,f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[3523,3564,3500,3458,3465,3477,3450,3461,3481,1476,3498,3455,1311,15,22,17,20,23,21,16,18,19])).
% 60.24/60.43 cnf(3584,plain,
% 60.24/60.43 (~P1(x35841,f5(a3),f4(a6,a7))),
% 60.24/60.43 inference(rename_variables,[],[3511])).
% 60.24/60.43 cnf(3587,plain,
% 60.24/60.43 (~P3(f8(a3,x35871),f8(x35872,a3),f4(a6,a7))),
% 60.24/60.43 inference(rename_variables,[],[3540])).
% 60.24/60.43 cnf(3593,plain,
% 60.24/60.43 (P1(x35931,f8(x35932,a3),f4(a3,a3))),
% 60.24/60.43 inference(rename_variables,[],[2389])).
% 60.24/60.43 cnf(3596,plain,
% 60.24/60.43 (~P3(f8(a3,x35961),f8(x35962,a3),f4(a6,a7))),
% 60.24/60.43 inference(rename_variables,[],[3540])).
% 60.24/60.43 cnf(3597,plain,
% 60.24/60.43 (P3(f5(a3),f8(x35971,a3),f8(a3,x35972))),
% 60.24/60.43 inference(rename_variables,[],[3500])).
% 60.24/60.43 cnf(3599,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f4(a3,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3506,3523,3564,3511,3584,3540,3587,3500,3535,3458,3465,3477,3450,3461,3481,2581,1198,1138,1476,1879,3498,3455,3448,1311,2389,1133,15,22,17,20,23,21,16,18,19,26,25,27,24,31])).
% 60.24/60.43 cnf(3602,plain,
% 60.24/60.43 (~P3(f8(a3,x36021),f4(a3,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3506,3515,3523,3564,3511,3584,3540,3587,3500,3535,3458,3465,3477,3450,3461,3481,2581,1326,1198,1138,1476,1879,3498,3455,3448,1311,2389,3593,1133,15,22,17,20,23,21,16,18,19,26,25,27,24,31,30])).
% 60.24/60.43 cnf(3607,plain,
% 60.24/60.43 (~P1(a1,f8(x36071,a3),f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3506,3515,3523,3564,3511,3584,3540,3587,3500,3597,3535,3458,3465,3477,3450,3461,3481,2099,2581,1326,1198,1138,1476,1879,3498,3455,3448,1311,2389,3593,1133,182,15,22,17,20,23,21,16,18,19,26,25,27,24,31,30,28])).
% 60.24/60.43 cnf(3608,plain,
% 60.24/60.43 (P3(f5(a3),f8(x36081,a3),f8(a3,x36082))),
% 60.24/60.43 inference(rename_variables,[],[3500])).
% 60.24/60.43 cnf(3611,plain,
% 60.24/60.43 (~P1(f8(a3,x36111),a2,f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3506,3515,3523,3564,3511,3584,3540,3587,3596,3500,3597,3608,3535,3458,3465,3477,3450,3461,3481,2099,2581,1326,1198,1138,1476,1879,3498,3455,3448,1311,1997,2389,3593,1133,182,15,22,17,20,23,21,16,18,19,26,25,27,24,31,30,28,29])).
% 60.24/60.43 cnf(3616,plain,
% 60.24/60.43 (P3(f4(a3,a3),f8(x36161,a3),f8(a3,x36162))),
% 60.24/60.43 inference(scs_inference,[],[3566,15])).
% 60.24/60.43 cnf(3618,plain,
% 60.24/60.43 (~P3(f8(x36181,a3),f4(a3,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3566,3467,15,22])).
% 60.24/60.43 cnf(3619,plain,
% 60.24/60.43 (P3(f8(x36191,a3),f4(a3,a3),f8(a3,x36192))),
% 60.24/60.43 inference(rename_variables,[],[3566])).
% 60.24/60.43 cnf(3622,plain,
% 60.24/60.43 (~P1(a1,f5(a3),f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3566,3607,3467,1686,15,22,20])).
% 60.24/60.43 cnf(3623,plain,
% 60.24/60.43 (~P1(a1,f8(x36231,a3),f4(a7,a6))),
% 60.24/60.43 inference(rename_variables,[],[3607])).
% 60.24/60.43 cnf(3625,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f8(a3,x36251),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3599,3566,3607,3467,1686,1476,15,22,20,17])).
% 60.24/60.43 cnf(3627,plain,
% 60.24/60.43 (~P1(f8(a3,x36271),x36272,f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3599,3566,3575,3607,3467,3487,1686,1476,15,22,20,17,23])).
% 60.24/60.43 cnf(3635,plain,
% 60.24/60.43 (~P2(f4(a6,a7),f4(a3,a3))),
% 60.24/60.43 inference(scs_inference,[],[3599,3566,3575,3607,3611,2606,3467,3487,1686,1476,2599,44,15,22,20,17,23,21,16,18])).
% 60.24/60.43 cnf(3638,plain,
% 60.24/60.43 (~P2(f8(a3,x36381),f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3599,3568,3566,3575,3607,3623,3611,2606,3467,3487,1686,1476,2599,44,15,22,20,17,23,21,16,18,19])).
% 60.24/60.43 cnf(3639,plain,
% 60.24/60.43 (~P1(a1,f8(x36391,a3),f4(a7,a6))),
% 60.24/60.43 inference(rename_variables,[],[3607])).
% 60.24/60.43 cnf(3640,plain,
% 60.24/60.43 (P1(x36401,f8(a3,x36402),f8(a3,x36403))),
% 60.24/60.43 inference(rename_variables,[],[3568])).
% 60.24/60.43 cnf(3644,plain,
% 60.24/60.43 (P1(x36441,f8(a3,x36442),f8(a3,x36443))),
% 60.24/60.43 inference(rename_variables,[],[3568])).
% 60.24/60.43 cnf(3653,plain,
% 60.24/60.43 (~P1(a1,f8(x36531,a3),f4(a7,a6))),
% 60.24/60.43 inference(rename_variables,[],[3607])).
% 60.24/60.43 cnf(3656,plain,
% 60.24/60.43 (P1(x36561,f8(a3,x36562),f8(a3,x36563))),
% 60.24/60.43 inference(rename_variables,[],[3568])).
% 60.24/60.43 cnf(3658,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f8(a3,x36581),f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3599,3568,3640,3644,3656,3566,3619,3563,3575,3607,3623,3639,3653,3611,3561,2606,2121,3515,3467,3487,3450,2321,1326,1686,1476,2389,2101,2599,5,44,15,22,20,17,23,21,16,18,19,26,25,24,31,30])).
% 60.24/60.43 cnf(3661,plain,
% 60.24/60.43 (P1(x36611,f8(a3,x36612),f8(a3,x36613))),
% 60.24/60.43 inference(rename_variables,[],[3568])).
% 60.24/60.43 cnf(3664,plain,
% 60.24/60.43 (~P1(x36641,f8(a3,x36642),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3599,3547,3568,3640,3644,3656,3661,3566,3619,3563,3575,3577,3607,3623,3639,3653,3611,3561,2606,2121,3515,3467,3487,3450,2321,1326,1686,1476,2389,2101,2599,5,44,15,22,20,17,23,21,16,18,19,26,25,24,31,30,28])).
% 60.24/60.43 cnf(3667,plain,
% 60.24/60.43 (P1(x36671,f8(a3,x36672),f8(a3,x36673))),
% 60.24/60.43 inference(rename_variables,[],[3568])).
% 60.24/60.43 cnf(3670,plain,
% 60.24/60.43 (P1(x36701,f8(a3,x36702),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[3599,3547,3568,3640,3644,3656,3661,3667,3566,3619,3563,3575,3577,3607,3623,3639,3653,3611,3561,2606,2121,3515,3467,3487,3450,2321,1326,1686,1476,3448,2389,2101,1262,2599,5,44,15,22,20,17,23,21,16,18,19,26,25,24,31,30,28,27])).
% 60.24/60.43 cnf(3674,plain,
% 60.24/60.43 (P1(x36741,f8(a3,x36742),a3)),
% 60.24/60.43 inference(scs_inference,[],[3599,3547,3568,3640,3644,3656,3661,3667,3566,3619,3563,3575,3577,3607,3623,3639,3653,3611,3561,2606,2121,3515,3467,3487,3450,2321,1326,1686,1476,3448,2389,2101,1262,2599,5,44,15,22,20,17,23,21,16,18,19,26,25,24,31,30,28,27,530])).
% 60.24/60.43 cnf(3676,plain,
% 60.24/60.43 (P3(f8(x36761,a3),f8(a3,x36762),f8(a3,x36763))),
% 60.24/60.43 inference(scs_inference,[],[3577,15])).
% 60.24/60.43 cnf(3678,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f8(x36781,a3),f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3638,3616,3577,15,22])).
% 60.24/60.43 cnf(3679,plain,
% 60.24/60.43 (~P2(f8(a3,x36791),f4(a7,a6))),
% 60.24/60.43 inference(rename_variables,[],[3638])).
% 60.24/60.43 cnf(3681,plain,
% 60.24/60.43 (~P2(f4(a3,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3638,3616,3577,2329,269,15,22,17])).
% 60.24/60.43 cnf(3682,plain,
% 60.24/60.43 (P3(f8(x36821,a3),f4(a3,a3),f4(a3,a3))),
% 60.24/60.43 inference(rename_variables,[],[269])).
% 60.24/60.43 cnf(3684,plain,
% 60.24/60.43 (P1(x36841,f8(x36842,a3),f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[3638,3616,3670,3577,2329,269,1009,15,22,17,20])).
% 60.24/60.43 cnf(3685,plain,
% 60.24/60.43 (P1(x36851,f8(a3,x36852),f5(a3))),
% 60.24/60.43 inference(rename_variables,[],[3670])).
% 60.24/60.43 cnf(3687,plain,
% 60.24/60.43 (P1(f8(x36871,a3),x36872,f8(a3,x36873))),
% 60.24/60.43 inference(scs_inference,[],[3638,3616,3670,3577,2329,269,1009,1166,15,22,17,20,21])).
% 60.24/60.43 cnf(3690,plain,
% 60.24/60.43 (~P1(f8(a3,x36901),a3,f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3638,3679,3616,3670,3573,3577,2329,269,1009,1166,15,22,17,20,21,23])).
% 60.24/60.43 cnf(3691,plain,
% 60.24/60.43 (P1(f8(a3,x36911),a3,f8(a3,x36912))),
% 60.24/60.43 inference(rename_variables,[],[3573])).
% 60.24/60.43 cnf(3695,plain,
% 60.24/60.43 (P3(f8(x36951,a3),f8(x36952,a3),f8(a3,x36953))),
% 60.24/60.43 inference(scs_inference,[],[3638,3679,3616,3670,3573,3577,2329,269,1009,129,1166,2544,15,22,17,20,21,23,16,18])).
% 60.24/60.43 cnf(3696,plain,
% 60.24/60.43 (P3(f8(a3,x36961),f8(x36962,a3),f8(a3,x36963))),
% 60.24/60.43 inference(rename_variables,[],[3577])).
% 60.24/60.43 cnf(3698,plain,
% 60.24/60.43 (~P2(f4(a3,a3),f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3638,3679,3616,3670,3573,3622,3577,2329,269,1009,129,2581,1166,2544,15,22,17,20,21,23,16,18,19])).
% 60.24/60.43 cnf(3701,plain,
% 60.24/60.43 (~P1(f8(a3,x37011),x37012,f4(a6,a7))),
% 60.24/60.43 inference(rename_variables,[],[3627])).
% 60.24/60.43 cnf(3703,plain,
% 60.24/60.43 (~P3(a6,a7,f8(a3,x37031))),
% 60.24/60.43 inference(scs_inference,[],[3627,3638,3679,3579,3616,3670,3573,3622,2528,3577,3696,2329,269,1009,3455,129,2581,1166,2544,806,15,22,17,20,21,23,16,18,19,26,25])).
% 60.24/60.43 cnf(3707,plain,
% 60.24/60.43 (~P1(f4(a3,a3),a3,f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3627,3664,3638,3679,3579,3616,3670,3573,3691,3622,2528,3577,3696,2329,2418,269,1009,3455,129,2581,1166,2544,806,15,22,17,20,21,23,16,18,19,26,25,27])).
% 60.24/60.43 cnf(3715,plain,
% 60.24/60.43 (~P3(f5(a3),f4(a3,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3627,3664,3625,3638,3679,3579,3616,3670,3685,3573,3691,3622,2528,3511,3577,3696,3481,2329,2418,269,3682,1009,3455,129,2581,1166,2544,806,15,22,17,20,21,23,16,18,19,26,25,27,24,31])).
% 60.24/60.43 cnf(3720,plain,
% 60.24/60.43 (~P1(f5(a1),a3,f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3627,3664,3625,3638,3679,3579,3616,3670,3685,3573,3691,3622,2528,3511,3577,3696,3481,2329,2418,269,3682,2121,1009,3599,3455,129,2581,1390,1166,2544,806,15,22,17,20,21,23,16,18,19,26,25,27,24,31,28])).
% 60.24/60.43 cnf(3725,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f8(x37251,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3627,3701,3664,3625,3638,3679,3579,3616,3670,3685,3573,3691,3622,2528,3511,3577,3696,3481,2329,2418,269,3682,2121,1020,1531,1009,3599,3455,129,2581,1390,1730,1335,1166,2544,806,15,22,17,20,21,23,16,18,19,26,25,27,24,31,28,29,30])).
% 60.24/60.43 cnf(3730,plain,
% 60.24/60.43 (P3(f8(x37301,a3),a3,f5(a3))),
% 60.24/60.43 inference(scs_inference,[],[1748,15])).
% 60.24/60.43 cnf(3732,plain,
% 60.24/60.43 (~P3(f8(x37321,a3),f8(x37322,a3),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3695,3523,1748,15,22])).
% 60.24/60.43 cnf(3735,plain,
% 60.24/60.43 (~P1(f5(a1),a3,f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3698,3695,1567,3523,1748,15,22,23])).
% 60.24/60.43 cnf(3737,plain,
% 60.24/60.43 (~P1(f4(a3,a3),a3,f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3698,3695,3690,1567,3523,1748,1799,15,22,23,21])).
% 60.24/60.43 cnf(3738,plain,
% 60.24/60.43 (~P1(f8(a3,x37381),a3,f4(a7,a6))),
% 60.24/60.43 inference(rename_variables,[],[3690])).
% 60.24/60.43 cnf(3739,plain,
% 60.24/60.43 (P2(f4(a3,a3),f8(x37391,a3))),
% 60.24/60.43 inference(rename_variables,[],[1799])).
% 60.24/60.43 cnf(3741,plain,
% 60.24/60.43 (~P1(f8(a3,x37411),f4(a3,a3),f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3698,3695,3690,3738,1567,1753,3523,1748,1799,15,22,23,21,20])).
% 60.24/60.43 cnf(3743,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f4(a3,a3),f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3698,3658,3695,3690,3738,1567,1753,3523,1748,1799,3739,15,22,23,21,20,17])).
% 60.24/60.43 cnf(3744,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f8(a3,x37441),f4(a7,a6))),
% 60.24/60.43 inference(rename_variables,[],[3658])).
% 60.24/60.43 cnf(3747,plain,
% 60.24/60.43 (~P2(a3,f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3698,3658,3744,3695,3690,3738,1567,1753,3523,1748,1225,1799,3739,15,22,23,21,20,17,16])).
% 60.24/60.43 cnf(3748,plain,
% 60.24/60.43 (~P3(f4(a3,a3),f8(a3,x37481),f4(a7,a6))),
% 60.24/60.43 inference(rename_variables,[],[3658])).
% 60.24/60.43 cnf(3754,plain,
% 60.24/60.43 (~P2(f5(a3),f4(a7,a6))),
% 60.24/60.43 inference(scs_inference,[],[3698,3715,3658,3744,3684,3695,3690,3738,1567,1753,3523,3607,1748,1225,1799,3739,44,15,22,23,21,20,17,16,18,19])).
% 60.24/60.43 cnf(3759,plain,
% 60.24/60.43 (P1(f8(x37591,a3),x37592,f8(a3,x37593))),
% 60.24/60.43 inference(rename_variables,[],[3687])).
% 60.24/60.43 cnf(3769,plain,
% 60.24/60.43 (~P3(a3,f8(a3,x37691),f4(a6,a7))),
% 60.24/60.43 inference(scs_inference,[],[3698,3715,3658,3744,3748,3687,3759,3684,3695,3674,3690,3738,3469,1567,1753,3523,3607,3561,1748,1734,1225,1195,1799,3739,3566,44,15,22,23,21,20,17,16,18,19,26,25,27,24])).
% 60.24/60.43 cnf(3791,plain,
% 60.24/60.43 (P3(f4(a3,a3),f5(a3),f8(a3,x37911))),
% 60.24/60.43 inference(scs_inference,[],[1299,15])).
% 60.24/60.43 cnf(3795,plain,
% 60.24/60.43 (P3(f5(a3),a3,f8(a3,x37951))),
% 60.24/60.43 inference(scs_inference,[],[3681,1486,1299,1753,15,22,17])).
% 60.24/60.43 cnf(3797,plain,
% 60.24/60.43 (P1(f8(a3,x37971),f8(a1,a2),f8(a3,a6))),
% 60.24/60.43 inference(scs_inference,[],[3681,1486,2538,1299,1753,1245,15,22,17,20])).
% 60.24/60.43 cnf(3800,plain,
% 60.24/60.43 (~P1(x38001,f8(a3,x38002),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3681,3638,3568,1486,2538,1299,1753,1245,15,22,17,20,23])).
% 60.24/60.44 cnf(3801,plain,
% 60.24/60.44 (P1(x38011,f8(a3,x38012),f8(a3,x38013))),
% 60.24/60.44 inference(rename_variables,[],[3568])).
% 60.24/60.44 cnf(3803,plain,
% 60.24/60.44 (P1(f8(a1,a2),x38031,f8(a6,x38031))),
% 60.24/60.44 inference(scs_inference,[],[3681,3638,3568,1486,2538,1299,1753,1245,10,15,22,17,20,23,21])).
% 60.24/60.44 cnf(3806,plain,
% 60.24/60.44 (~P2(f8(x38061,a3),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3681,3678,3638,3568,1486,2538,1299,1753,1195,1245,10,15,22,17,20,23,21,16])).
% 60.24/60.44 cnf(3808,plain,
% 60.24/60.44 (~P3(f4(a3,a3),f8(x38081,a3),f4(a7,a6))),
% 60.24/60.44 inference(rename_variables,[],[3678])).
% 60.24/60.44 cnf(3810,plain,
% 60.24/60.44 (~P2(a7,f5(a6))),
% 60.24/60.44 inference(scs_inference,[],[3681,3678,3638,3568,1486,2538,1299,1753,1819,1195,1245,806,10,15,22,17,20,23,21,16,18])).
% 60.24/60.44 cnf(3814,plain,
% 60.24/60.44 (P1(f8(x38141,a3),x38142,f8(a3,x38143))),
% 60.24/60.44 inference(rename_variables,[],[3687])).
% 60.24/60.44 cnf(3817,plain,
% 60.24/60.44 (P3(f5(a3),f8(a3,x38171),f5(a3))),
% 60.24/60.44 inference(scs_inference,[],[3681,3678,3741,3730,3638,3568,3687,1486,2538,1198,1299,1753,899,3487,1819,1195,1245,806,10,15,22,17,20,23,21,16,18,26,25])).
% 60.24/60.44 cnf(3820,plain,
% 60.24/60.44 (P1(x38201,f8(a3,x38202),f4(a3,a3))),
% 60.24/60.44 inference(scs_inference,[],[3681,3678,3741,3730,3638,3568,3801,3687,1486,2538,1198,1299,1753,899,3674,3487,1819,1195,1245,967,806,10,15,22,17,20,23,21,16,18,26,25,27])).
% 60.24/60.44 cnf(3821,plain,
% 60.24/60.44 (P1(a3,x38211,f4(a3,a3))),
% 60.24/60.44 inference(rename_variables,[],[967])).
% 60.24/60.44 cnf(3822,plain,
% 60.24/60.44 (P1(x38221,f8(a3,x38222),f8(a3,x38223))),
% 60.24/60.44 inference(rename_variables,[],[3568])).
% 60.24/60.44 cnf(3825,plain,
% 60.24/60.44 (P3(f8(a3,x38251),f8(a3,x38251),f4(a3,a3))),
% 60.24/60.44 inference(rename_variables,[],[1918])).
% 60.24/60.44 cnf(3832,plain,
% 60.24/60.44 (~P3(f8(a3,x38321),f4(a3,a3),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3681,3678,3808,3741,3737,3730,3638,3568,3801,3822,3687,3814,1486,2538,1198,1299,1753,899,3674,3487,1819,1918,3825,1195,1245,967,3821,806,10,15,22,17,20,23,21,16,18,26,25,27,24,31,30])).
% 60.24/60.44 cnf(3844,plain,
% 60.24/60.44 (P3(f8(a3,x38441),f5(a3),f5(a3))),
% 60.24/60.44 inference(scs_inference,[],[3817,15])).
% 60.24/60.44 cnf(3847,plain,
% 60.24/60.44 (P3(f4(a3,a3),f5(a3),f8(a3,x38471))),
% 60.24/60.44 inference(rename_variables,[],[3791])).
% 60.24/60.44 cnf(3856,plain,
% 60.24/60.44 (P3(x38561,a3,x38561)),
% 60.24/60.44 inference(rename_variables,[],[4])).
% 60.24/60.44 cnf(3862,plain,
% 60.24/60.44 (P1(f8(a1,a2),x38621,f8(a6,x38621))),
% 60.24/60.44 inference(rename_variables,[],[3803])).
% 60.24/60.44 cnf(3865,plain,
% 60.24/60.44 (~P3(a6,a7,f5(a3))),
% 60.24/60.44 inference(scs_inference,[],[3747,3803,3618,3707,3806,3791,3769,3817,3795,3703,2885,1403,967,5,4,3856,44,15,22,23,17,16,18,26,25])).
% 60.24/60.44 cnf(3866,plain,
% 60.24/60.44 (P3(f5(a3),a3,f8(a3,x38661))),
% 60.24/60.44 inference(rename_variables,[],[3795])).
% 60.24/60.44 cnf(3867,plain,
% 60.24/60.44 (P3(x38671,a3,x38671)),
% 60.24/60.44 inference(rename_variables,[],[4])).
% 60.24/60.44 cnf(3870,plain,
% 60.24/60.44 (P1(x38701,f8(a3,x38702),f4(a3,a3))),
% 60.24/60.44 inference(rename_variables,[],[3820])).
% 60.24/60.44 cnf(3872,plain,
% 60.24/60.44 (~P3(f5(a7),f5(a6),f4(a3,a3))),
% 60.24/60.44 inference(scs_inference,[],[3747,3720,3803,3618,3820,3707,3806,3791,3769,3817,3795,3703,2791,2885,2568,1403,967,5,4,3856,3867,44,15,22,23,17,16,18,26,25,27,24])).
% 60.24/60.44 cnf(3875,plain,
% 60.24/60.44 (~P3(f8(a3,x38751),f8(a3,x38752),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3747,3720,3803,3800,3618,3820,3707,3806,3791,3769,3817,3795,3866,3703,2791,2885,3573,3687,2568,1403,967,5,4,3856,3867,44,15,22,23,17,16,18,26,25,27,24,31])).
% 60.24/60.44 cnf(3879,plain,
% 60.24/60.44 (~P1(x38791,f8(a3,x38792),f4(a7,a6))),
% 60.24/60.44 inference(rename_variables,[],[3800])).
% 60.24/60.44 cnf(3881,plain,
% 60.24/60.44 (~P3(f5(a3),f4(a3,a3),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3747,3720,3803,3800,3879,3618,3820,3870,3707,3806,3791,3847,3769,3817,3795,3866,3703,2791,2885,3684,3573,3687,2568,1403,967,5,4,3856,3867,44,15,22,23,17,16,18,26,25,27,24,31,30])).
% 60.24/60.44 cnf(3891,plain,
% 60.24/60.44 (~P1(f5(a3),x38911,f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3747,3720,3803,3862,3800,3879,3618,3820,3870,3707,3806,3732,3791,3847,3769,3817,3795,3866,3703,2791,2885,3684,3573,2368,3687,1351,2568,1403,1471,2409,967,5,4,3856,3867,44,15,22,23,17,16,18,26,25,27,24,31,30,28,29])).
% 60.24/60.44 cnf(3897,plain,
% 60.24/60.44 (~P3(a3,f5(a6),a7)),
% 60.24/60.44 inference(scs_inference,[],[3520,3795,5,15,22])).
% 60.24/60.44 cnf(3898,plain,
% 60.24/60.44 (P3(a3,x38981,x38981)),
% 60.24/60.44 inference(rename_variables,[],[5])).
% 60.24/60.44 cnf(3901,plain,
% 60.24/60.44 (P1(f8(a1,a2),x39011,f8(a6,x39011))),
% 60.24/60.44 inference(rename_variables,[],[3803])).
% 60.24/60.44 cnf(3907,plain,
% 60.24/60.44 (P1(f8(a6,a1),a3,f4(a3,a3))),
% 60.24/60.44 inference(scs_inference,[],[3520,3832,3803,3901,3820,3806,3795,3469,5,44,15,22,23,18,26])).
% 60.24/60.44 cnf(3910,plain,
% 60.24/60.44 (P1(x39101,f8(a3,x39102),f4(a3,a3))),
% 60.24/60.44 inference(rename_variables,[],[3820])).
% 60.24/60.44 cnf(3912,plain,
% 60.24/60.44 (~P3(f5(a3),a3,f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3520,3832,3875,3844,3803,3901,3820,3806,3795,3469,5,44,15,22,23,18,26,25])).
% 60.24/60.44 cnf(3913,plain,
% 60.24/60.44 (~P3(f8(a3,x39131),f8(a3,x39132),f4(a7,a6))),
% 60.24/60.44 inference(rename_variables,[],[3875])).
% 60.24/60.44 cnf(3915,plain,
% 60.24/60.44 (~P1(f4(a3,a3),f8(a1,a2),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3520,3832,3875,3891,3797,3844,3803,3901,3820,3910,3806,3795,3469,5,44,15,22,23,18,26,25,27])).
% 60.24/60.44 cnf(3933,plain,
% 60.24/60.44 (~P2(f4(a7,a6),f4(a3,a3))),
% 60.24/60.44 inference(scs_inference,[],[3520,3725,3832,3875,3913,3891,3797,3844,3743,3803,3901,3820,3910,3806,3795,3469,2606,2242,1717,1295,2121,1490,806,5,3898,44,9,15,22,23,18,26,25,27,24,28,29,17,16])).
% 60.24/60.44 cnf(3946,plain,
% 60.24/60.44 (P3(f4(a3,a3),f5(a3),f4(a3,a3))),
% 60.24/60.44 inference(scs_inference,[],[1326,15])).
% 60.24/60.44 cnf(3952,plain,
% 60.24/60.44 (~P2(f4(a7,a6),f5(a3))),
% 60.24/60.44 inference(scs_inference,[],[3754,3635,3881,3907,3561,1326,44,15,22,23,18])).
% 60.24/60.44 cnf(3958,plain,
% 60.24/60.44 (P3(f8(a3,x39581),f8(a3,x39582),f5(a3))),
% 60.24/60.44 inference(scs_inference,[],[3915,3754,3635,3881,3907,3817,1652,3481,3561,1326,1262,44,15,22,23,18,26,25])).
% 60.24/60.44 cnf(3959,plain,
% 60.24/60.44 (P3(f5(a3),f8(a3,x39591),f5(a3))),
% 60.24/60.44 inference(rename_variables,[],[3817])).
% 60.24/60.44 cnf(3962,plain,
% 60.24/60.44 (P1(f8(a6,a1),f5(a3),f4(a3,a3))),
% 60.24/60.44 inference(scs_inference,[],[3915,3754,3635,3881,3907,3817,3670,1652,3820,3481,3561,1326,1262,44,15,22,23,18,26,25,27])).
% 60.24/60.44 cnf(3963,plain,
% 60.24/60.44 (P1(x39631,f8(a3,x39632),f4(a3,a3))),
% 60.24/60.44 inference(rename_variables,[],[3820])).
% 60.24/60.44 cnf(3964,plain,
% 60.24/60.44 (P1(x39641,f8(a3,x39642),f5(a3))),
% 60.24/60.44 inference(rename_variables,[],[3670])).
% 60.24/60.44 cnf(3966,plain,
% 60.24/60.44 (~P3(f5(a6),a6,f4(a6,a7))),
% 60.24/60.44 inference(scs_inference,[],[3915,3754,3635,3881,3907,3602,3817,3670,1652,3820,3481,3561,1326,2578,2541,1262,44,15,22,23,18,26,25,27,24])).
% 60.24/60.44 cnf(3970,plain,
% 60.24/60.44 (~P3(f5(a3),f5(a3),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3915,3754,3635,3735,3881,3907,3602,3817,3670,3964,1652,3820,3481,3561,1326,1892,2578,2541,1262,44,15,22,23,18,26,25,27,24,31])).
% 60.24/60.44 cnf(3979,plain,
% 60.24/60.44 (~P1(x39791,f5(a3),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3915,3754,3635,3735,3881,3907,3602,3817,3959,3670,3964,1652,3820,3963,3481,3561,1326,1892,2578,2397,2541,2280,1432,1262,44,15,22,23,18,26,25,27,24,31,30,28])).
% 60.24/60.44 cnf(3987,plain,
% 60.24/60.44 (P3(f8(a3,x39871),a3,f8(x39872,a3))),
% 60.24/60.44 inference(scs_inference,[],[1144,15])).
% 60.24/60.44 cnf(3997,plain,
% 60.24/60.44 (~P1(x39971,f5(a3),f4(a7,a6))),
% 60.24/60.44 inference(rename_variables,[],[3979])).
% 60.24/60.44 cnf(4002,plain,
% 60.24/60.44 (~P1(f4(a3,a3),f8(x40021,a3),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3933,3979,3997,3946,3962,3872,3484,3803,3467,3684,1144,2554,1295,5,15,22,23,26,25,27])).
% 60.24/60.44 cnf(4032,plain,
% 60.24/60.44 (P3(f8(a1,a2),f5(a6),a3)),
% 60.24/60.44 inference(scs_inference,[],[2568,15])).
% 60.24/60.44 cnf(4036,plain,
% 60.24/60.44 (~P1(a1,a2,f5(a7))),
% 60.24/60.44 inference(scs_inference,[],[3452,3508,2568,1,15,22,23])).
% 60.24/60.44 cnf(4038,plain,
% 60.24/60.44 (~P1(f8(a6,a1),f4(a3,a3),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3452,3508,4002,3962,3820,2568,1,15,22,23,26])).
% 60.24/60.44 cnf(4048,plain,
% 60.24/60.44 (~P3(f8(a3,x40481),f8(x40482,a3),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3452,3508,4002,3912,3966,3987,3962,3800,3958,1997,3820,2568,5,1,15,22,23,26,25,27,24])).
% 60.24/60.44 cnf(4051,plain,
% 60.24/60.44 (~P1(x40511,f8(x40512,a3),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[3452,3508,4002,3970,3912,3966,3987,3962,3800,3958,1319,3670,1997,3820,2568,5,1,15,22,23,26,25,27,24,28])).
% 60.24/60.44 cnf(4065,plain,
% 60.24/60.44 (P3(f8(a1,a2),f5(a6),f8(x40651,a3))),
% 60.24/60.44 inference(scs_inference,[],[2578,15])).
% 60.24/60.44 cnf(4067,plain,
% 60.24/60.44 (~P3(a7,f8(x40671,a3),f5(a6))),
% 60.24/60.44 inference(scs_inference,[],[3810,2578,806,15,22])).
% 60.24/60.44 cnf(4072,plain,
% 60.24/60.44 (P3(f5(a3),f8(a3,x40721),f8(a3,x40721))),
% 60.24/60.44 inference(scs_inference,[],[3810,3695,3523,3469,1020,2578,806,15,22,23,25])).
% 60.24/60.44 cnf(4075,plain,
% 60.24/60.44 (P1(x40751,f8(a3,x40752),f8(x40753,a3))),
% 60.24/60.44 inference(scs_inference,[],[3810,3695,3523,3573,3469,1020,3684,2578,1432,806,15,22,23,25,27])).
% 60.24/60.44 cnf(4078,plain,
% 60.24/60.44 (P1(f8(a3,x40781),a3,f8(a3,x40782))),
% 60.24/60.44 inference(rename_variables,[],[3573])).
% 60.24/60.44 cnf(4093,plain,
% 60.24/60.44 (~P3(a7,f8(a1,a2),f8(x40931,a3))),
% 60.24/60.44 inference(scs_inference,[],[3810,4032,4038,4048,3695,3523,3573,4078,3469,2606,269,1836,1020,3674,3684,2578,2101,1432,806,15,22,23,25,27,24,31,29,2374])).
% 60.24/60.44 cnf(4109,plain,
% 60.24/60.44 (~P3(f8(a1,a2),f5(a6),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[4065,4072,3638,15,22])).
% 60.24/60.44 cnf(4115,plain,
% 60.24/60.44 (~P1(x41151,a3,f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[4075,4065,4072,4051,3698,3638,3907,3674,15,22,23,26])).
% 60.24/60.44 cnf(4117,plain,
% 60.24/60.44 (~P1(x41171,f8(x41172,a3),f4(a7,a6))),
% 60.24/60.44 inference(rename_variables,[],[4051])).
% 60.24/60.44 cnf(4121,plain,
% 60.24/60.44 (P3(x41211,a3,x41211)),
% 60.24/60.44 inference(rename_variables,[],[4])).
% 60.24/60.44 cnf(4129,plain,
% 60.24/60.44 (~P3(f8(x41291,a3),f8(x41291,a3),f4(a7,a6))),
% 60.24/60.44 inference(scs_inference,[],[4075,4065,4072,4093,3897,4051,4117,3698,4036,3638,4032,3958,3987,3469,3907,3674,2568,10,4,4121,15,22,23,26,25,24,31,30])).
% 60.24/60.44 cnf(4171,plain,
% 60.24/60.44 ($false),
% 60.24/60.44 inference(scs_inference,[],[3952,4109,4129,4115,4067,3865,3575,4065,3484,3676,1734,1918,3684,981,1471,1262,7,806,5,4,6,1,15,22,23,25,24,30,28,29]),
% 60.24/60.44 ['proof']).
% 60.24/60.44 % SZS output end Proof
% 60.24/60.44 % Total time :59.730000s
%------------------------------------------------------------------------------