%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG006-2 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n003.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 64.91s 64.94s
% Output : CNFRefutation 65.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : RNG006-2 : TPTP v8.2.0. Released v1.0.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n003.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jun 18 14:40:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.53 start to proof:theBenchmark
% 64.91/64.92 %-------------------------------------------
% 64.91/64.92 % File :CSE---1.7
% 64.91/64.92 % Problem :theBenchmark
% 64.91/64.92 % Transform :cnf
% 64.91/64.92 % Format :tptp:raw
% 64.91/64.92 % Command :java -jar mcs_scs.jar %d %s
% 64.91/64.92
% 64.91/64.92 % Result :Theorem 64.360000s
% 64.91/64.92 % Output :CNFRefutation 64.360000s
% 64.91/64.92 %-------------------------------------------
% 64.91/64.93 %--------------------------------------------------------------------------
% 64.91/64.93 % File : RNG006-2 : TPTP v8.2.0. Released v1.0.0.
% 64.91/64.93 % Domain : Ring Theory
% 64.91/64.93 % Problem : X*(Y+ -Z) = (X*Y) + -(X*Z)
% 64.91/64.93 % Version : [Wos65] axioms : Reduced & Augmented > Incomplete.
% 64.91/64.93 % English :
% 64.91/64.93
% 64.91/64.93 % Refs : [Wos65] Wos (1965), Unpublished Note
% 64.91/64.93 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 64.91/64.93 % Source : [SPRFN]
% 64.91/64.93 % Names : Problem 25 [Wos65]
% 64.91/64.93 % : wos25 [WM76]
% 64.91/64.93
% 64.91/64.93 % Status : Unsatisfiable
% 64.91/64.93 % 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.14 v6.0.0, 0.22 v5.5.0, 0.06 v5.4.0, 0.11 v5.3.0, 0.25 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.29 v2.2.1, 0.33 v2.2.0, 0.22 v2.1.0, 0.14 v2.0.0
% 64.91/64.93 % Syntax : Number of clauses : 36 ( 13 unt; 0 nHn; 26 RR)
% 64.91/64.93 % Number of literals : 87 ( 0 equ; 52 neg)
% 64.91/64.93 % Maximal clause size : 5 ( 2 avg)
% 64.91/64.93 % Maximal term depth : 2 ( 1 avg)
% 64.91/64.93 % Number of predicates : 3 ( 3 usr; 0 prp; 2-3 aty)
% 64.91/64.93 % Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% 64.91/64.93 % Number of variables : 114 ( 2 sgn)
% 64.91/64.93 % SPC : CNF_UNS_RFO_NEQ_HRN
% 64.91/64.93
% 64.91/64.93 % Comments : These are the same axioms as in [MOW76].
% 64.91/64.93 %--------------------------------------------------------------------------
% 64.91/64.93 %----Include ring theory axioms
% 64.91/64.93 %include('Axioms/RNG001-0.ax').
% 64.91/64.93 %--------------------------------------------------------------------------
% 64.91/64.93 %----Equality axioms for additive operator
% 64.91/64.93 cnf(additive_inverse_substitution,axiom,
% 64.91/64.93 ( ~ equalish(X,Y)
% 64.91/64.93 | equalish(additive_inverse(X),additive_inverse(Y)) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(add_substitution1,axiom,
% 64.91/64.93 ( ~ equalish(X,Y)
% 64.91/64.93 | equalish(add(X,W),add(Y,W)) ) ).
% 64.91/64.93
% 64.91/64.93 %----This axiom omited in this version
% 64.91/64.93 %input_clause(add_substitution2,axiom,
% 64.91/64.93 % [--equalish(X,Y),
% 64.91/64.93 % ++equalish(add(W,X),add(W,Y))]).
% 64.91/64.93
% 64.91/64.93 cnf(sum_substitution1,axiom,
% 64.91/64.93 ( ~ equalish(X,Y)
% 64.91/64.93 | ~ sum(X,W,Z)
% 64.91/64.93 | sum(Y,W,Z) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(sum_substitution2,axiom,
% 64.91/64.93 ( ~ equalish(X,Y)
% 64.91/64.93 | ~ sum(W,X,Z)
% 64.91/64.93 | sum(W,Y,Z) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(sum_substitution3,axiom,
% 64.91/64.93 ( ~ equalish(X,Y)
% 64.91/64.93 | ~ sum(W,Z,X)
% 64.91/64.93 | sum(W,Z,Y) ) ).
% 64.91/64.93
% 64.91/64.93 %----Equality axioms for multiplicative operator
% 64.91/64.93 cnf(multiply_substitution1,axiom,
% 64.91/64.93 ( ~ equalish(X,Y)
% 64.91/64.93 | equalish(multiply(X,W),multiply(Y,W)) ) ).
% 64.91/64.93
% 64.91/64.93 %----This axiom omited in this version
% 64.91/64.93 %input_clause(multiply_substitution2,axiom,
% 64.91/64.93 % [--equalish(X,Y),
% 64.91/64.93 % ++equalish(multiply(W,X),multiply(W,Y))]).
% 64.91/64.93
% 64.91/64.93 cnf(product_substitution1,axiom,
% 64.91/64.93 ( ~ equalish(X,Y)
% 64.91/64.93 | ~ product(X,W,Z)
% 64.91/64.93 | product(Y,W,Z) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(product_substitution2,axiom,
% 64.91/64.93 ( ~ equalish(X,Y)
% 64.91/64.93 | ~ product(W,X,Z)
% 64.91/64.93 | product(W,Y,Z) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(product_substitution3,axiom,
% 64.91/64.93 ( ~ equalish(X,Y)
% 64.91/64.93 | ~ product(W,Z,X)
% 64.91/64.93 | product(W,Z,Y) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(additive_identity1,axiom,
% 64.91/64.93 sum(additive_identity,X,X) ).
% 64.91/64.93
% 64.91/64.93 cnf(additive_identity2,axiom,
% 64.91/64.93 sum(X,additive_identity,X) ).
% 64.91/64.93
% 64.91/64.93 cnf(closure_of_multiplication,axiom,
% 64.91/64.93 product(X,Y,multiply(X,Y)) ).
% 64.91/64.93
% 64.91/64.93 cnf(closure_of_addition,axiom,
% 64.91/64.93 sum(X,Y,add(X,Y)) ).
% 64.91/64.93
% 64.91/64.93 cnf(left_inverse,axiom,
% 64.91/64.93 sum(additive_inverse(X),X,additive_identity) ).
% 64.91/64.93
% 64.91/64.93 cnf(right_inverse,axiom,
% 64.91/64.93 sum(X,additive_inverse(X),additive_identity) ).
% 64.91/64.93
% 64.91/64.93 cnf(associativity_of_addition1,axiom,
% 64.91/64.93 ( ~ sum(X,Y,U)
% 64.91/64.93 | ~ sum(Y,Z,V)
% 64.91/64.93 | ~ sum(U,Z,W)
% 64.91/64.93 | sum(X,V,W) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(associativity_of_addition2,axiom,
% 64.91/64.93 ( ~ sum(X,Y,U)
% 64.91/64.93 | ~ sum(Y,Z,V)
% 64.91/64.93 | ~ sum(X,V,W)
% 64.91/64.93 | sum(U,Z,W) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(commutativity_of_addition,axiom,
% 64.91/64.93 ( ~ sum(X,Y,Z)
% 64.91/64.93 | sum(Y,X,Z) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(associativity_of_multiplication1,axiom,
% 64.91/64.93 ( ~ product(X,Y,U)
% 64.91/64.93 | ~ product(Y,Z,V)
% 64.91/64.93 | ~ product(U,Z,W)
% 64.91/64.93 | product(X,V,W) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(associativity_of_multiplication2,axiom,
% 64.91/64.93 ( ~ product(X,Y,U)
% 64.91/64.93 | ~ product(Y,Z,V)
% 64.91/64.93 | ~ product(X,V,W)
% 64.91/64.93 | product(U,Z,W) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(distributivity1,axiom,
% 64.91/64.93 ( ~ product(X,Y,V1)
% 64.91/64.93 | ~ product(X,Z,V2)
% 64.91/64.93 | ~ sum(Y,Z,V3)
% 64.91/64.93 | ~ product(X,V3,V4)
% 64.91/64.93 | sum(V1,V2,V4) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(distributivity2,axiom,
% 64.91/64.93 ( ~ product(X,Y,V1)
% 64.91/64.93 | ~ product(X,Z,V2)
% 64.91/64.93 | ~ sum(Y,Z,V3)
% 64.91/64.93 | ~ sum(V1,V2,V4)
% 64.91/64.93 | product(X,V3,V4) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(distributivity3,axiom,
% 64.91/64.93 ( ~ product(Y,X,V1)
% 64.91/64.93 | ~ product(Z,X,V2)
% 64.91/64.93 | ~ sum(Y,Z,V3)
% 64.91/64.93 | ~ product(V3,X,V4)
% 64.91/64.93 | sum(V1,V2,V4) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(distributivity4,axiom,
% 64.91/64.93 ( ~ product(Y,X,V1)
% 64.91/64.93 | ~ product(Z,X,V2)
% 64.91/64.93 | ~ sum(Y,Z,V3)
% 64.91/64.93 | ~ sum(V1,V2,V4)
% 64.91/64.93 | product(V3,X,V4) ) ).
% 64.91/64.93
% 64.91/64.93 %-----Equality axioms for operators
% 64.91/64.93 cnf(addition_is_well_defined,axiom,
% 64.91/64.93 ( ~ sum(X,Y,U)
% 64.91/64.93 | ~ sum(X,Y,V)
% 64.91/64.93 | equalish(U,V) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(multiplication_is_well_defined,axiom,
% 64.91/64.93 ( ~ product(X,Y,U)
% 64.91/64.93 | ~ product(X,Y,V)
% 64.91/64.93 | equalish(U,V) ) ).
% 64.91/64.93
% 64.91/64.93 cnf(multiplicative_identity1,axiom,
% 64.91/64.93 product(additive_identity,X,additive_identity) ).
% 64.91/64.93
% 64.91/64.93 cnf(multiplicative_identity2,axiom,
% 64.91/64.93 product(X,additive_identity,additive_identity) ).
% 64.91/64.93
% 64.91/64.93 cnf(product_lemma1,axiom,
% 64.91/64.93 ( ~ product(A,B,C)
% 64.91/64.93 | product(A,additive_inverse(B),additive_inverse(C)) ) ).
% 64.91/64.93
% 64.91/64.94 cnf(product_lemma2,axiom,
% 64.91/64.94 ( ~ product(A,B,C)
% 64.91/64.94 | product(additive_inverse(A),B,additive_inverse(C)) ) ).
% 64.91/64.94
% 64.91/64.94 cnf(product_lemma3,axiom,
% 64.91/64.94 ( ~ product(A,B,C)
% 64.91/64.94 | product(additive_inverse(A),additive_inverse(B),C) ) ).
% 64.91/64.94
% 64.91/64.94 cnf(b_plus_inverse_c,hypothesis,
% 64.91/64.94 sum(b,additive_inverse(c),bS_Ic) ).
% 64.91/64.94
% 64.91/64.94 cnf(a_times_b,hypothesis,
% 64.91/64.94 product(a,b,aPb) ).
% 64.91/64.94
% 64.91/64.94 cnf(a_times_c,hypothesis,
% 64.91/64.94 product(a,c,aPc) ).
% 64.91/64.94
% 64.91/64.94 cnf(aPb_plus_IaPc,hypothesis,
% 64.91/64.94 sum(aPb,additive_inverse(aPc),aPb_S_IaPc) ).
% 64.91/64.94
% 64.91/64.94 cnf(prove_a_times_bS_Ic_is_aPb_S__IaPc,negated_conjecture,
% 64.91/64.94 ~ product(a,bS_Ic,aPb_S_IaPc) ).
% 64.91/64.94
% 64.91/64.94 %--------------------------------------------------------------------------
% 64.91/64.94 %-------------------------------------------
% 64.91/64.94 % Proof found
% 64.91/64.94 % SZS status Theorem for theBenchmark
% 64.91/64.94 % SZS output start Proof
% 64.91/64.94 %ClaNum:36(EqnAxiom:0)
% 64.91/64.94 %VarNum:230(SingletonVarNum:114)
% 64.91/64.94 %MaxLitNum:5
% 64.91/64.94 %MaxfuncDepth:1
% 64.91/64.94 %SharedTerms:15
% 64.91/64.94 %goalClause: 13
% 64.91/64.94 %singleGoalClaCount:1
% 64.91/64.94 [1]P1(a1,a2,a3)
% 64.91/64.94 [2]P1(a1,a9,a4)
% 64.91/64.94 [13]~P1(a1,a10,a5)
% 64.91/64.94 [7]P3(a2,f8(a9),a10)
% 64.91/64.94 [8]P3(a3,f8(a4),a5)
% 64.91/64.94 [3]P1(x31,a6,a6)
% 64.91/64.94 [4]P1(a6,x41,a6)
% 64.91/64.94 [5]P3(x51,a6,x51)
% 64.91/64.94 [6]P3(a6,x61,x61)
% 64.91/64.94 [9]P3(x91,f8(x91),a6)
% 64.91/64.94 [10]P3(f8(x101),x101,a6)
% 64.91/64.94 [11]P3(x111,x112,f7(x111,x112))
% 64.91/64.94 [12]P1(x121,x122,f11(x121,x122))
% 64.91/64.94 [14]~P2(x141,x142)+P2(f8(x141),f8(x142))
% 64.91/64.94 [17]~P3(x172,x171,x173)+P3(x171,x172,x173)
% 64.91/64.94 [15]~P2(x151,x153)+P2(f7(x151,x152),f7(x153,x152))
% 64.91/64.94 [16]~P2(x161,x163)+P2(f11(x161,x162),f11(x163,x162))
% 64.91/64.94 [18]~P1(x181,x182,x183)+P1(x181,f8(x182),f8(x183))
% 64.91/64.94 [19]~P1(x191,x192,x193)+P1(f8(x191),x192,f8(x193))
% 64.91/64.94 [20]~P1(x201,x202,x203)+P1(f8(x201),f8(x202),x203)
% 64.91/64.94 [21]~P3(x211,x212,x214)+P3(x211,x212,x213)+~P2(x214,x213)
% 64.91/64.94 [22]~P3(x221,x224,x223)+P3(x221,x222,x223)+~P2(x224,x222)
% 64.91/64.94 [23]~P3(x234,x232,x233)+P3(x231,x232,x233)+~P2(x234,x231)
% 64.91/64.94 [24]~P1(x241,x242,x244)+P1(x241,x242,x243)+~P2(x244,x243)
% 64.91/64.94 [25]~P1(x251,x254,x253)+P1(x251,x252,x253)+~P2(x254,x252)
% 64.91/64.94 [26]~P1(x264,x262,x263)+P1(x261,x262,x263)+~P2(x264,x261)
% 64.91/64.94 [27]~P3(x273,x274,x271)+P2(x271,x272)+~P3(x273,x274,x272)
% 64.91/64.94 [28]~P1(x283,x284,x281)+P2(x281,x282)+~P1(x283,x284,x282)
% 64.91/64.94 [29]~P3(x296,x294,x291)+P3(x291,x292,x293)+~P3(x294,x292,x295)+~P3(x296,x295,x293)
% 64.91/64.94 [30]~P3(x301,x306,x304)+P3(x301,x302,x303)+~P3(x304,x305,x303)+~P3(x306,x305,x302)
% 64.91/64.94 [31]~P1(x316,x314,x311)+P1(x311,x312,x313)+~P1(x314,x312,x315)+~P1(x316,x315,x313)
% 64.91/64.94 [32]~P1(x321,x326,x324)+P1(x321,x322,x323)+~P1(x324,x325,x323)+~P1(x326,x325,x322)
% 64.91/64.94 [33]~P1(x337,x335,x332)+~P1(x337,x334,x331)+P3(x331,x332,x333)+~P3(x334,x335,x336)+~P1(x337,x336,x333)
% 64.91/64.94 [34]~P1(x345,x347,x342)+~P1(x344,x347,x341)+P3(x341,x342,x343)+~P3(x344,x345,x346)+~P1(x346,x347,x343)
% 64.91/64.94 [35]~P1(x357,x352,x355)+~P1(x356,x352,x354)+P1(x351,x352,x353)+~P3(x354,x355,x353)+~P3(x356,x357,x351)
% 64.91/64.94 [36]~P1(x361,x367,x365)+~P1(x361,x366,x364)+P1(x361,x362,x363)+~P3(x364,x365,x363)+~P3(x366,x367,x362)
% 64.91/64.94 %EqnAxiom
% 64.91/64.94
% 64.91/64.94 %-------------------------------------------
% 64.91/64.95 cnf(39,plain,
% 64.91/64.95 (P2(f11(x391,a6),a6)),
% 64.91/64.95 inference(scs_inference,[],[5,12,3,27,28])).
% 64.91/64.95 cnf(40,plain,
% 64.91/64.95 (P1(x401,a6,a6)),
% 64.91/64.95 inference(rename_variables,[],[3])).
% 64.91/64.95 cnf(41,plain,
% 64.91/64.95 (P1(x411,x412,f11(x411,x412))),
% 64.91/64.95 inference(rename_variables,[],[12])).
% 64.91/64.95 cnf(43,plain,
% 64.91/64.95 (P1(f11(x431,a6),a6,f11(x431,a6))),
% 64.91/64.95 inference(scs_inference,[],[5,12,41,3,40,27,28,31])).
% 64.91/64.95 cnf(44,plain,
% 64.91/64.95 (P1(x441,x442,f11(x441,x442))),
% 64.91/64.95 inference(rename_variables,[],[12])).
% 64.91/64.95 cnf(45,plain,
% 64.91/64.95 (P1(x451,x452,f11(x451,x452))),
% 64.91/64.95 inference(rename_variables,[],[12])).
% 64.91/64.95 cnf(46,plain,
% 64.91/64.95 (P1(x461,a6,a6)),
% 64.91/64.95 inference(rename_variables,[],[3])).
% 64.91/64.95 cnf(48,plain,
% 64.91/64.95 (P1(x481,f11(x481,x481),f11(f11(x481,x481),x481))),
% 64.91/64.95 inference(scs_inference,[],[5,12,41,45,44,3,40,27,28,31,32])).
% 64.91/64.95 cnf(50,plain,
% 64.91/64.95 (P1(x501,x502,f11(x501,x502))),
% 64.91/64.95 inference(rename_variables,[],[12])).
% 64.91/64.95 cnf(53,plain,
% 64.91/64.95 (P3(x531,f7(a6,a6),x531)),
% 64.91/64.95 inference(scs_inference,[],[5,11,12,41,45,44,3,40,27,28,31,32,30])).
% 64.91/64.95 cnf(54,plain,
% 64.91/64.95 (P3(x541,x542,f7(x541,x542))),
% 64.91/64.95 inference(rename_variables,[],[11])).
% 64.91/64.95 cnf(56,plain,
% 64.91/64.95 (P1(x561,a6,f11(a6,a6))),
% 64.91/64.95 inference(scs_inference,[],[5,6,11,12,41,45,50,44,3,40,46,27,28,31,32,30,35])).
% 64.91/64.95 cnf(57,plain,
% 64.91/64.95 (P3(a6,x571,x571)),
% 64.91/64.95 inference(rename_variables,[],[6])).
% 64.91/64.95 cnf(58,plain,
% 64.91/64.95 (P3(x581,a6,x581)),
% 64.91/64.95 inference(rename_variables,[],[5])).
% 64.91/64.95 cnf(59,plain,
% 64.91/64.95 (P1(x591,x592,f11(x591,x592))),
% 64.91/64.95 inference(rename_variables,[],[12])).
% 64.91/64.95 cnf(61,plain,
% 64.91/64.95 (P3(f11(x611,a6),f11(x611,a6),f11(x611,a6))),
% 64.91/64.95 inference(scs_inference,[],[5,58,6,11,12,41,45,50,59,44,3,40,46,27,28,31,32,30,35,33])).
% 64.91/64.95 cnf(64,plain,
% 64.91/64.95 (P1(x641,x642,f11(x641,x642))),
% 64.91/64.95 inference(rename_variables,[],[12])).
% 64.91/64.95 cnf(65,plain,
% 64.91/64.95 (P3(x651,a6,x651)),
% 64.91/64.95 inference(rename_variables,[],[5])).
% 64.91/64.95 cnf(67,plain,
% 64.91/64.95 (P3(f11(a6,x671),f11(a6,x671),f11(a6,x671))),
% 64.91/64.95 inference(scs_inference,[],[5,58,65,6,11,12,41,45,50,59,64,44,3,40,46,27,28,31,32,30,35,33,34])).
% 64.91/64.95 cnf(70,plain,
% 64.91/64.95 (P1(x701,x702,f11(x701,x702))),
% 64.91/64.95 inference(rename_variables,[],[12])).
% 64.91/64.95 cnf(71,plain,
% 64.91/64.95 (P3(x711,a6,x711)),
% 64.91/64.95 inference(rename_variables,[],[5])).
% 64.91/64.95 cnf(73,plain,
% 64.91/64.95 (P1(x731,a6,f7(f11(x731,a6),f11(x731,a6)))),
% 64.91/64.95 inference(scs_inference,[],[5,58,65,71,6,11,54,12,41,45,50,59,64,70,44,3,40,46,27,28,31,32,30,35,33,34,36])).
% 64.91/64.95 cnf(75,plain,
% 64.91/64.95 (P3(x751,a6,x751)),
% 64.91/64.95 inference(rename_variables,[],[5])).
% 64.91/64.95 cnf(77,plain,
% 64.91/64.95 (P1(x771,x772,f11(x771,x772))),
% 64.91/64.95 inference(rename_variables,[],[12])).
% 64.91/64.95 cnf(79,plain,
% 64.91/64.95 (P1(x791,a6,f11(x791,f11(x792,a6)))),
% 64.91/64.95 inference(scs_inference,[],[5,58,65,71,6,11,54,12,41,45,50,59,64,70,77,44,3,40,46,27,28,31,32,30,35,33,34,36,25])).
% 64.91/64.95 cnf(80,plain,
% 64.91/64.95 (P1(x801,x802,f11(x801,x802))),
% 64.91/64.95 inference(rename_variables,[],[12])).
% 64.91/64.95 cnf(82,plain,
% 64.91/64.95 (P1(a6,x821,f11(f11(x822,a6),x821))),
% 64.91/64.95 inference(scs_inference,[],[5,58,65,71,6,11,54,12,41,45,50,59,64,70,77,80,44,3,40,46,27,28,31,32,30,35,33,34,36,25,26])).
% 64.91/64.95 cnf(85,plain,
% 64.91/64.95 (P3(f11(x851,a6),a6,a6)),
% 64.91/64.95 inference(scs_inference,[],[5,58,65,71,75,6,11,54,12,41,45,50,59,64,70,77,80,44,3,40,46,27,28,31,32,30,35,33,34,36,25,26,21])).
% 64.91/64.95 cnf(88,plain,
% 64.91/64.95 (P3(a6,a6,f11(x881,a6))),
% 64.91/64.95 inference(scs_inference,[],[5,58,65,71,75,6,57,11,54,12,41,45,50,59,64,70,77,80,44,3,40,46,27,28,31,32,30,35,33,34,36,25,26,21,22])).
% 64.91/64.95 cnf(91,plain,
% 64.91/64.95 (P3(a6,f7(a6,a6),f11(x911,a6))),
% 64.91/64.95 inference(scs_inference,[],[53,39,23])).
% 64.91/64.95 cnf(92,plain,
% 64.91/64.96 (P3(x921,f7(a6,a6),x921)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(94,plain,
% 64.91/64.96 (P2(f8(f7(a6,a6)),a6)),
% 64.91/64.96 inference(scs_inference,[],[53,92,39,10,23,27])).
% 64.91/64.96 cnf(95,plain,
% 64.91/64.96 (P3(f8(x951),x951,a6)),
% 64.91/64.96 inference(rename_variables,[],[10])).
% 64.91/64.96 cnf(96,plain,
% 64.91/64.96 (P3(x961,f7(a6,a6),x961)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(98,plain,
% 64.91/64.96 (P2(f11(x981,f11(x982,a6)),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[79,56,53,92,39,10,23,27,28])).
% 64.91/64.96 cnf(101,plain,
% 64.91/64.96 (P3(f11(x1011,a6),f7(a6,a6),a6)),
% 64.91/64.96 inference(scs_inference,[],[79,56,53,92,96,39,10,23,27,28,21])).
% 64.91/64.96 cnf(102,plain,
% 64.91/64.96 (P3(x1021,f7(a6,a6),x1021)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(104,plain,
% 64.91/64.96 (P3(f7(a6,a6),a6,a6)),
% 64.91/64.96 inference(scs_inference,[],[79,56,53,92,96,39,9,10,23,27,28,21,22])).
% 64.91/64.96 cnf(105,plain,
% 64.91/64.96 (P3(x1051,f8(x1051),a6)),
% 64.91/64.96 inference(rename_variables,[],[9])).
% 64.91/64.96 cnf(107,plain,
% 64.91/64.96 (P3(f8(a6),f8(f7(a6,a6)),a6)),
% 64.91/64.96 inference(scs_inference,[],[79,56,53,92,96,102,39,9,105,10,95,23,27,28,21,22,29])).
% 64.91/64.96 cnf(112,plain,
% 64.91/64.96 (P3(a6,f11(x1121,a6),a6)),
% 64.91/64.96 inference(scs_inference,[],[79,56,53,92,96,102,39,9,105,10,95,85,88,23,27,28,21,22,29,30])).
% 64.91/64.96 cnf(115,plain,
% 64.91/64.96 (P1(f11(x1151,a6),x1152,f11(x1151,a6))),
% 64.91/64.96 inference(scs_inference,[],[79,43,56,53,92,96,102,39,4,9,105,10,95,85,88,23,27,28,21,22,29,30,31])).
% 64.91/64.96 cnf(127,plain,
% 64.91/64.96 (P3(x1271,a6,x1271)),
% 64.91/64.96 inference(rename_variables,[],[5])).
% 64.91/64.96 cnf(129,plain,
% 64.91/64.96 (P1(f11(x1291,a6),f11(f11(x1291,a6),f11(x1291,a6)),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[48,5,98,23,24])).
% 64.91/64.96 cnf(130,plain,
% 64.91/64.96 (P2(f11(x1301,f11(x1302,a6)),f11(a6,a6))),
% 64.91/64.96 inference(rename_variables,[],[98])).
% 64.91/64.96 cnf(131,plain,
% 64.91/64.96 (P1(x1311,f11(x1311,x1311),f11(f11(x1311,x1311),x1311))),
% 64.91/64.96 inference(rename_variables,[],[48])).
% 64.91/64.96 cnf(134,plain,
% 64.91/64.96 (P3(x1341,a6,x1341)),
% 64.91/64.96 inference(rename_variables,[],[5])).
% 64.91/64.96 cnf(136,plain,
% 64.91/64.96 (P2(f11(x1361,a6),f7(f11(x1361,a6),f11(x1361,a6)))),
% 64.91/64.96 inference(scs_inference,[],[48,61,5,127,98,130,11,23,24,21,27])).
% 64.91/64.96 cnf(139,plain,
% 64.91/64.96 (P2(f11(x1391,a6),f11(f11(x1391,a6),f11(x1392,a6)))),
% 64.91/64.96 inference(scs_inference,[],[48,115,79,61,5,127,98,130,11,23,24,21,27,28])).
% 64.91/64.96 cnf(141,plain,
% 64.91/64.96 (P1(f11(x1411,a6),x1412,f11(x1411,a6))),
% 64.91/64.96 inference(rename_variables,[],[115])).
% 64.91/64.96 cnf(146,plain,
% 64.91/64.96 (P1(f11(x1461,a6),x1462,f11(x1461,a6))),
% 64.91/64.96 inference(rename_variables,[],[115])).
% 64.91/64.96 cnf(150,plain,
% 64.91/64.96 (P3(f8(x1501),x1501,a6)),
% 64.91/64.96 inference(rename_variables,[],[10])).
% 64.91/64.96 cnf(153,plain,
% 64.91/64.96 (P3(f8(a6),a6,f11(x1531,a6))),
% 64.91/64.96 inference(scs_inference,[],[48,115,141,79,61,5,127,134,98,130,91,107,2,11,12,10,150,23,24,21,27,28,22,32,29,30])).
% 64.91/64.96 cnf(156,plain,
% 64.91/64.96 (P1(f11(f11(a6,a6),a6),x1561,a6)),
% 64.91/64.96 inference(scs_inference,[],[48,131,115,141,146,79,61,5,127,134,98,130,91,107,2,11,12,10,150,4,23,24,21,27,28,22,32,29,30,31])).
% 64.91/64.96 cnf(161,plain,
% 64.91/64.96 (P1(x1611,f11(x1612,a6),f11(x1612,a6))),
% 64.91/64.96 inference(scs_inference,[],[48,131,115,141,146,79,61,5,127,134,98,130,91,107,2,11,12,3,10,150,88,4,23,24,21,27,28,22,32,29,30,31,36])).
% 64.91/64.96 cnf(171,plain,
% 64.91/64.96 (P1(a6,f11(f11(x1711,a6),f11(x1711,a6)),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[129,39,26])).
% 64.91/64.96 cnf(175,plain,
% 64.91/64.96 (P3(x1751,a6,x1751)),
% 64.91/64.96 inference(rename_variables,[],[5])).
% 64.91/64.96 cnf(181,plain,
% 64.91/64.96 (P2(a6,f11(x1811,a6))),
% 64.91/64.96 inference(scs_inference,[],[129,82,101,94,5,53,98,39,26,23,24,27])).
% 64.91/64.96 cnf(185,plain,
% 64.91/64.96 (P3(x1851,a6,x1851)),
% 64.91/64.96 inference(rename_variables,[],[5])).
% 64.91/64.96 cnf(187,plain,
% 64.91/64.96 (P2(f11(a6,a6),f11(x1871,a6))),
% 64.91/64.96 inference(scs_inference,[],[129,82,115,101,94,5,175,53,98,39,26,23,24,27,21,28])).
% 64.91/64.96 cnf(188,plain,
% 64.91/64.96 (P1(f11(x1881,a6),x1882,f11(x1881,a6))),
% 64.91/64.96 inference(rename_variables,[],[115])).
% 64.91/64.96 cnf(193,plain,
% 64.91/64.96 (P1(f11(x1931,a6),f11(x1932,a6),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[129,82,115,188,61,101,94,5,175,161,139,53,98,39,26,23,24,27,21,28,22,32])).
% 64.91/64.96 cnf(195,plain,
% 64.91/64.96 (P1(f11(x1951,a6),x1952,f11(x1951,a6))),
% 64.91/64.96 inference(rename_variables,[],[115])).
% 64.91/64.96 cnf(197,plain,
% 64.91/64.96 (P3(f11(x1971,a6),a6,f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[129,82,115,188,61,101,94,91,5,175,185,161,139,53,6,98,39,26,23,24,27,21,28,22,32,29])).
% 64.91/64.96 cnf(201,plain,
% 64.91/64.96 (P3(f11(x2011,a6),a6,f11(x2012,a6))),
% 64.91/64.96 inference(scs_inference,[],[129,82,115,188,61,101,94,91,88,5,175,185,104,161,139,53,6,98,39,26,23,24,27,21,28,22,32,29,30])).
% 64.91/64.96 cnf(205,plain,
% 64.91/64.96 (P1(x2051,a6,a6)),
% 64.91/64.96 inference(rename_variables,[],[3])).
% 64.91/64.96 cnf(212,plain,
% 64.91/64.96 (P1(f7(a6,a6),a6,f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[129,156,82,115,188,195,79,61,101,94,91,88,5,175,185,104,161,139,53,6,98,11,39,3,205,26,23,24,27,21,28,22,32,29,30,31,36,35])).
% 64.91/64.96 cnf(226,plain,
% 64.91/64.96 (P1(f11(x2261,a6),f7(f11(x2262,a6),f11(x2262,a6)),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[193,136,25])).
% 64.91/64.96 cnf(227,plain,
% 64.91/64.96 (P2(f11(x2271,a6),f7(f11(x2271,a6),f11(x2271,a6)))),
% 64.91/64.96 inference(rename_variables,[],[136])).
% 64.91/64.96 cnf(229,plain,
% 64.91/64.96 (P1(f7(f11(x2291,a6),f11(x2291,a6)),f11(x2292,a6),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[193,136,227,25,26])).
% 64.91/64.96 cnf(232,plain,
% 64.91/64.96 (P3(f11(x2321,a6),f11(a6,a6),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[193,61,187,136,227,25,26,23])).
% 64.91/64.96 cnf(233,plain,
% 64.91/64.96 (P3(f11(x2331,a6),f11(x2331,a6),f11(x2331,a6))),
% 64.91/64.96 inference(rename_variables,[],[61])).
% 64.91/64.96 cnf(235,plain,
% 64.91/64.96 (P2(f11(x2351,a6),f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[193,61,91,187,136,227,6,25,26,23,27])).
% 64.91/64.96 cnf(238,plain,
% 64.91/64.96 (P1(f11(x2381,a6),f11(x2382,a6),f11(x2383,a6))),
% 64.91/64.96 inference(scs_inference,[],[193,61,91,187,136,227,6,25,26,23,27,24])).
% 64.91/64.96 cnf(241,plain,
% 64.91/64.96 (P3(f11(x2411,a6),f11(x2411,a6),f11(x2411,a6))),
% 64.91/64.96 inference(rename_variables,[],[61])).
% 64.91/64.96 cnf(246,plain,
% 64.91/64.96 (P2(f7(a6,a6),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[193,212,56,61,233,241,91,187,136,227,6,25,26,23,27,24,21,22,28])).
% 64.91/64.96 cnf(247,plain,
% 64.91/64.96 (P1(x2471,a6,f11(a6,a6))),
% 64.91/64.96 inference(rename_variables,[],[56])).
% 64.91/64.96 cnf(249,plain,
% 64.91/64.96 (P1(a6,f7(a6,a6),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[193,212,82,56,247,61,233,241,91,187,136,227,6,25,26,23,27,24,21,22,28,32])).
% 64.91/64.96 cnf(284,plain,
% 64.91/64.96 (P2(f11(x2841,a6),f7(a6,a6))),
% 64.91/64.96 inference(rename_variables,[],[235])).
% 64.91/64.96 cnf(286,plain,
% 64.91/64.96 (P1(f7(a6,a6),f7(f11(x2861,a6),f11(x2861,a6)),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[226,229,235,284,25,26])).
% 64.91/64.96 cnf(287,plain,
% 64.91/64.96 (P2(f11(x2871,a6),f7(a6,a6))),
% 64.91/64.96 inference(rename_variables,[],[235])).
% 64.91/64.96 cnf(289,plain,
% 64.91/64.96 (P2(f8(a6),a6)),
% 64.91/64.96 inference(scs_inference,[],[226,229,5,235,284,10,25,26,27])).
% 64.91/64.96 cnf(291,plain,
% 64.91/64.96 (P3(x2911,a6,x2911)),
% 64.91/64.96 inference(rename_variables,[],[5])).
% 64.91/64.96 cnf(294,plain,
% 64.91/64.96 (P2(f11(x2941,a6),f7(a6,a6))),
% 64.91/64.96 inference(rename_variables,[],[235])).
% 64.91/64.96 cnf(296,plain,
% 64.91/64.96 (P1(f11(x2961,a6),f7(f11(x2962,a6),f11(x2962,a6)),f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[226,229,61,5,235,284,287,294,10,25,26,27,23,24])).
% 64.91/64.96 cnf(299,plain,
% 64.91/64.96 (P3(f11(x2991,a6),f11(a6,a6),a6)),
% 64.91/64.96 inference(scs_inference,[],[226,229,61,101,5,246,235,284,287,294,10,25,26,27,23,24,22])).
% 64.91/64.96 cnf(304,plain,
% 64.91/64.96 (P2(f11(a6,a6),f11(f11(x3041,a6),f7(a6,a6)))),
% 64.91/64.96 inference(scs_inference,[],[226,229,249,82,61,101,5,291,246,235,284,287,294,10,25,26,27,23,24,22,21,28])).
% 64.91/64.96 cnf(325,plain,
% 64.91/64.96 (P1(f11(x3251,a6),f11(x3252,a6),f11(x3253,a6))),
% 64.91/64.96 inference(rename_variables,[],[238])).
% 64.91/64.96 cnf(327,plain,
% 64.91/64.96 (P1(f11(f11(x3271,a6),f7(a6,a6)),f11(x3272,a6),f11(x3273,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,325,304,25,26])).
% 64.91/64.96 cnf(328,plain,
% 64.91/64.96 (P1(f11(x3281,a6),f11(x3282,a6),f11(x3283,a6))),
% 64.91/64.96 inference(rename_variables,[],[238])).
% 64.91/64.96 cnf(331,plain,
% 64.91/64.96 (P3(f11(x3311,a6),f11(x3311,a6),f11(x3311,a6))),
% 64.91/64.96 inference(rename_variables,[],[61])).
% 64.91/64.96 cnf(334,plain,
% 64.91/64.96 (P1(f11(x3341,a6),f11(x3342,a6),f11(x3343,a6))),
% 64.91/64.96 inference(rename_variables,[],[238])).
% 64.91/64.96 cnf(337,plain,
% 64.91/64.96 (P3(f11(x3371,a6),f11(x3371,a6),f11(x3371,a6))),
% 64.91/64.96 inference(rename_variables,[],[61])).
% 64.91/64.96 cnf(342,plain,
% 64.91/64.96 (P2(f11(x3421,a6),f11(x3422,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,325,328,334,115,61,331,337,304,25,26,23,24,21,22,28])).
% 64.91/64.96 cnf(343,plain,
% 64.91/64.96 (P1(f11(x3431,a6),x3432,f11(x3431,a6))),
% 64.91/64.96 inference(rename_variables,[],[115])).
% 64.91/64.96 cnf(345,plain,
% 64.91/64.96 (P1(f11(x3451,a6),f11(a6,a6),f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,325,328,334,115,343,286,296,61,331,337,304,25,26,23,24,21,22,28,32])).
% 64.91/64.96 cnf(349,plain,
% 64.91/64.96 (P3(a6,f11(x3491,a6),f11(x3492,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,325,328,334,115,343,286,296,61,331,337,88,201,304,25,26,23,24,21,22,28,32,30])).
% 64.91/64.96 cnf(376,plain,
% 64.91/64.96 (P1(f11(x3761,a6),f7(a6,a6),f11(x3762,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,235,25])).
% 64.91/64.96 cnf(377,plain,
% 64.91/64.96 (P2(f11(x3771,a6),f7(a6,a6))),
% 64.91/64.96 inference(rename_variables,[],[235])).
% 64.91/64.96 cnf(379,plain,
% 64.91/64.96 (P2(f11(x3791,a6),f8(a6))),
% 64.91/64.96 inference(scs_inference,[],[238,153,5,235,25,27])).
% 64.91/64.96 cnf(384,plain,
% 64.91/64.96 (P3(f11(x3841,a6),f7(a6,a6),f11(x3842,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,171,153,91,5,181,235,25,27,26,23])).
% 64.91/64.96 cnf(387,plain,
% 64.91/64.96 (P2(f11(x3871,a6),f7(a6,a6))),
% 64.91/64.96 inference(rename_variables,[],[235])).
% 64.91/64.96 cnf(389,plain,
% 64.91/64.96 (P3(f8(a6),f11(x3891,a6),f11(x3892,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,171,153,91,5,181,235,377,25,27,26,23,24,22])).
% 64.91/64.96 cnf(393,plain,
% 64.91/64.96 (P3(f11(a6,x3931),f11(a6,x3931),f11(a6,x3931))),
% 64.91/64.96 inference(rename_variables,[],[67])).
% 64.91/64.96 cnf(395,plain,
% 64.91/64.96 (P2(f11(x3951,a6),f11(f11(x3952,a6),f11(x3953,a6)))),
% 64.91/64.96 inference(scs_inference,[],[238,171,67,153,91,5,181,235,377,387,12,25,27,26,23,24,22,21,28])).
% 64.91/64.96 cnf(398,plain,
% 64.91/64.96 (P1(f11(x3981,a6),f7(a6,a6),f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,171,296,67,153,91,5,181,235,377,387,12,25,27,26,23,24,22,21,28,32])).
% 64.91/64.96 cnf(400,plain,
% 64.91/64.96 (P1(f11(x4001,a6),f11(x4002,a6),f11(x4003,a6))),
% 64.91/64.96 inference(rename_variables,[],[238])).
% 64.91/64.96 cnf(406,plain,
% 64.91/64.96 (P3(f7(a6,a6),f11(x4061,a6),f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,171,296,67,393,153,91,201,112,5,197,181,235,377,387,12,25,27,26,23,24,22,21,28,32,30,29])).
% 64.91/64.96 cnf(408,plain,
% 64.91/64.96 (P1(f7(a6,a6),f11(x4081,a6),f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,400,345,171,296,67,393,153,91,201,112,5,197,181,235,377,387,12,25,27,26,23,24,22,21,28,32,30,29,31])).
% 64.91/64.96 cnf(418,plain,
% 64.91/64.96 (P2(f11(x4181,a6),f7(f8(a6),a6))),
% 64.91/64.96 inference(scs_inference,[],[153,11,27])).
% 64.91/64.96 cnf(421,plain,
% 64.91/64.96 (P1(f11(f11(x4211,a6),f11(x4212,a6)),x4213,f11(x4214,a6))),
% 64.91/64.96 inference(scs_inference,[],[115,153,395,11,27,26])).
% 64.91/64.96 cnf(422,plain,
% 64.91/64.96 (P2(f11(x4221,a6),f11(f11(x4222,a6),f11(x4223,a6)))),
% 64.91/64.96 inference(rename_variables,[],[395])).
% 64.91/64.96 cnf(425,plain,
% 64.91/64.96 (P2(f11(x4251,a6),f11(f11(x4252,a6),f11(x4253,a6)))),
% 64.91/64.96 inference(rename_variables,[],[395])).
% 64.91/64.96 cnf(426,plain,
% 64.91/64.96 (P3(f11(a6,x4261),f11(a6,x4261),f11(a6,x4261))),
% 64.91/64.96 inference(rename_variables,[],[67])).
% 64.91/64.96 cnf(428,plain,
% 64.91/64.96 (P1(f11(x4281,a6),x4282,f11(f11(x4283,a6),f11(x4284,a6)))),
% 64.91/64.96 inference(scs_inference,[],[115,153,67,395,422,425,11,27,26,23,24])).
% 64.91/64.96 cnf(429,plain,
% 64.91/64.96 (P2(f11(x4291,a6),f11(f11(x4292,a6),f11(x4293,a6)))),
% 64.91/64.96 inference(rename_variables,[],[395])).
% 64.91/64.96 cnf(432,plain,
% 64.91/64.96 (P2(f11(x4321,a6),f11(f11(x4322,a6),f11(x4323,a6)))),
% 64.91/64.96 inference(rename_variables,[],[395])).
% 64.91/64.96 cnf(438,plain,
% 64.91/64.96 (P2(f11(x4381,a6),f11(f11(x4381,a6),x4382))),
% 64.91/64.96 inference(scs_inference,[],[115,153,67,426,395,422,425,429,432,11,12,27,26,23,24,21,22,28])).
% 64.91/64.96 cnf(439,plain,
% 64.91/64.96 (P1(x4391,x4392,f11(x4391,x4392))),
% 64.91/64.96 inference(rename_variables,[],[12])).
% 64.91/64.96 cnf(442,plain,
% 64.91/64.96 (P3(f8(x4421),x4421,a6)),
% 64.91/64.96 inference(rename_variables,[],[10])).
% 64.91/64.96 cnf(444,plain,
% 64.91/64.96 (P3(f8(f8(a6)),f11(x4441,a6),f11(x4442,a6))),
% 64.91/64.96 inference(scs_inference,[],[115,153,67,426,10,442,88,112,395,422,425,429,432,11,12,27,26,23,24,21,22,28,29,30])).
% 64.91/64.96 cnf(447,plain,
% 64.91/64.96 (P1(f7(a6,a6),x4471,f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[115,408,153,67,426,10,442,88,112,395,422,425,429,432,11,12,27,26,23,24,21,22,28,29,30,31])).
% 64.91/64.96 cnf(456,plain,
% 64.91/64.96 (P1(f7(a6,a6),f11(x4561,a6),f11(f7(a6,a6),f8(a6)))),
% 64.91/64.96 inference(scs_inference,[],[115,408,82,212,153,67,426,10,442,88,112,53,299,395,422,425,429,432,11,12,439,27,26,23,24,21,22,28,29,30,31,34,36])).
% 64.91/64.96 cnf(466,plain,
% 64.91/64.96 (P1(f11(f11(x4661,a6),x4662),x4663,f11(x4661,a6))),
% 64.91/64.96 inference(scs_inference,[],[115,438,26])).
% 64.91/64.96 cnf(467,plain,
% 64.91/64.96 (P2(f11(x4671,a6),f11(f11(x4671,a6),x4672))),
% 64.91/64.96 inference(rename_variables,[],[438])).
% 64.91/64.96 cnf(470,plain,
% 64.91/64.96 (P2(f11(x4701,a6),f11(f11(x4701,a6),x4702))),
% 64.91/64.96 inference(rename_variables,[],[438])).
% 64.91/64.96 cnf(471,plain,
% 64.91/64.96 (P3(f11(a6,x4711),f11(a6,x4711),f11(a6,x4711))),
% 64.91/64.96 inference(rename_variables,[],[67])).
% 64.91/64.96 cnf(473,plain,
% 64.91/64.96 (P1(f11(x4731,a6),x4732,f11(f11(x4731,a6),x4733))),
% 64.91/64.96 inference(scs_inference,[],[115,67,438,467,470,26,23,24])).
% 64.91/64.96 cnf(474,plain,
% 64.91/64.96 (P2(f11(x4741,a6),f11(f11(x4741,a6),x4742))),
% 64.91/64.96 inference(rename_variables,[],[438])).
% 64.91/64.96 cnf(479,plain,
% 64.91/64.96 (P3(f11(a6,a6),f11(f11(a6,a6),x4791),f11(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[115,67,471,6,94,438,467,470,474,26,23,24,21,22])).
% 64.91/64.96 cnf(487,plain,
% 64.91/64.96 (P3(f7(a6,a6),a6,f11(x4871,a6))),
% 64.91/64.96 inference(scs_inference,[],[115,238,67,471,91,10,9,6,94,456,438,467,470,474,26,23,24,21,22,32,30])).
% 64.91/64.96 cnf(489,plain,
% 64.91/64.96 (P3(x4891,f8(x4891),a6)),
% 64.91/64.96 inference(rename_variables,[],[9])).
% 64.91/64.96 cnf(491,plain,
% 64.91/64.96 (P3(f11(x4911,a6),f8(a6),f11(x4911,a6))),
% 64.91/64.96 inference(scs_inference,[],[115,238,153,67,471,91,10,9,489,6,94,456,438,467,470,474,26,23,24,21,22,32,30,29])).
% 64.91/64.96 cnf(494,plain,
% 64.91/64.96 (P1(f11(a6,a6),a6,f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[115,56,79,238,447,153,67,471,91,10,9,489,6,94,456,438,467,470,474,26,23,24,21,22,32,30,29,31])).
% 64.91/64.96 cnf(511,plain,
% 64.91/64.96 (P2(f11(x5111,a6),f7(f8(a6),a6))),
% 64.91/64.96 inference(rename_variables,[],[418])).
% 64.91/64.96 cnf(514,plain,
% 64.91/64.96 (P2(f11(x5141,a6),f7(f8(a6),a6))),
% 64.91/64.96 inference(rename_variables,[],[418])).
% 64.91/64.96 cnf(517,plain,
% 64.91/64.96 (P3(x5171,f7(a6,a6),x5171)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(519,plain,
% 64.91/64.96 (P2(f11(x5191,a6),f11(f11(x5192,a6),x5193))),
% 64.91/64.96 inference(scs_inference,[],[238,473,53,94,418,511,25,26,23,28])).
% 64.91/64.96 cnf(520,plain,
% 64.91/64.96 (P1(f11(x5201,a6),x5202,f11(f11(x5201,a6),x5203))),
% 64.91/64.96 inference(rename_variables,[],[473])).
% 64.91/64.96 cnf(523,plain,
% 64.91/64.96 (P2(f11(x5231,a6),f7(f8(a6),a6))),
% 64.91/64.96 inference(rename_variables,[],[418])).
% 64.91/64.96 cnf(526,plain,
% 64.91/64.96 (P3(x5261,f7(a6,a6),x5261)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(530,plain,
% 64.91/64.96 (P3(f11(a6,x5301),f11(a6,x5301),f11(a6,x5301))),
% 64.91/64.96 inference(rename_variables,[],[67])).
% 64.91/64.96 cnf(536,plain,
% 64.91/64.96 (P3(f11(x5361,a6),f7(a6,a6),f8(a6))),
% 64.91/64.96 inference(scs_inference,[],[238,473,153,67,53,517,526,9,94,6,418,511,514,523,289,11,25,26,23,28,24,21,22,30,29])).
% 64.91/64.96 cnf(543,plain,
% 64.91/64.96 (P1(f11(x5431,a6),f11(x5432,a6),f11(x5433,a6))),
% 64.91/64.96 inference(rename_variables,[],[238])).
% 64.91/64.96 cnf(545,plain,
% 64.91/64.96 (P1(f8(a6),f11(x5451,a6),f8(a6))),
% 64.91/64.96 inference(scs_inference,[],[238,543,473,520,447,153,67,53,517,526,9,94,6,418,511,514,523,289,11,25,26,23,28,24,21,22,30,29,31,35])).
% 64.91/64.96 cnf(549,plain,
% 64.91/64.96 (P3(f8(a6),f8(a6),f8(a6))),
% 64.91/64.96 inference(scs_inference,[],[238,543,473,520,447,153,67,530,53,517,526,9,94,6,418,511,514,523,289,11,25,26,23,28,24,21,22,30,29,31,35,33])).
% 64.91/64.96 cnf(557,plain,
% 64.91/64.96 (P2(f11(x5571,a6),f8(a6))),
% 64.91/64.96 inference(rename_variables,[],[379])).
% 64.91/64.96 cnf(559,plain,
% 64.91/64.96 (P1(f8(a6),f11(x5591,a6),f11(x5592,a6))),
% 64.91/64.96 inference(scs_inference,[],[238,379,557,25,26])).
% 64.91/64.96 cnf(560,plain,
% 64.91/64.96 (P2(f11(x5601,a6),f8(a6))),
% 64.91/64.96 inference(rename_variables,[],[379])).
% 64.91/64.96 cnf(565,plain,
% 64.91/64.96 (P1(f11(x5651,a6),f11(x5652,a6),f8(a6))),
% 64.91/64.96 inference(scs_inference,[],[238,201,379,557,560,136,25,26,23,24])).
% 64.91/64.96 cnf(588,plain,
% 64.91/64.96 (P2(f11(f11(x5881,a6),f11(x5882,a6)),f11(x5883,a6))),
% 64.91/64.96 inference(scs_inference,[],[428,115,28])).
% 64.91/64.96 cnf(591,plain,
% 64.91/64.96 (P1(f11(f11(x5911,a6),f11(x5912,a6)),x5913,f8(a6))),
% 64.91/64.96 inference(scs_inference,[],[421,428,115,379,28,24])).
% 64.91/64.96 cnf(592,plain,
% 64.91/64.96 (P2(f11(x5921,a6),f8(a6))),
% 64.91/64.96 inference(rename_variables,[],[379])).
% 64.91/64.96 cnf(598,plain,
% 64.91/64.96 (P3(x5981,f7(a6,a6),x5981)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(607,plain,
% 64.91/64.96 (P1(f11(f11(x6071,a6),f11(x6072,a6)),x6073,f11(x6074,a6))),
% 64.91/64.96 inference(rename_variables,[],[421])).
% 64.91/64.96 cnf(612,plain,
% 64.91/64.96 (P3(f11(x6121,a6),f7(a6,a6),f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[421,428,115,494,153,91,53,598,201,232,6,342,418,379,592,235,28,24,26,23,21,22,32,30,29])).
% 64.91/64.96 cnf(621,plain,
% 64.91/64.96 (P1(f8(a6),f7(a6,a6),f8(a6))),
% 64.91/64.96 inference(scs_inference,[],[421,607,428,376,115,466,447,494,153,91,53,598,201,232,6,342,536,418,379,592,235,28,24,26,23,21,22,32,30,29,31,35])).
% 64.91/64.96 cnf(635,plain,
% 64.91/64.96 (P3(x6351,f7(a6,a6),x6351)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(640,plain,
% 64.91/64.96 (P2(f11(x6401,a6),f7(f11(x6401,a6),f11(x6401,a6)))),
% 64.91/64.96 inference(rename_variables,[],[136])).
% 64.91/64.96 cnf(643,plain,
% 64.91/64.96 (P3(x6431,f7(a6,a6),x6431)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(645,plain,
% 64.91/64.96 (P3(f8(a6),f7(f11(x6451,a6),f11(x6451,a6)),f11(x6452,a6))),
% 64.91/64.96 inference(scs_inference,[],[327,376,447,53,635,389,246,136,640,379,98,25,23,24,26,21,22])).
% 64.91/64.96 cnf(654,plain,
% 64.91/64.96 (P3(x6541,f7(a6,a6),x6541)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(663,plain,
% 64.91/64.96 (P3(f11(x6631,a6),f11(x6631,a6),f8(a6))),
% 64.91/64.96 inference(scs_inference,[],[327,376,421,115,56,447,591,398,153,91,53,635,643,654,389,6,246,136,640,379,98,11,25,23,24,26,21,22,32,30,29,31,33])).
% 64.91/64.96 cnf(673,plain,
% 64.91/64.96 (P2(f11(f11(x6731,a6),f11(x6732,a6)),a6)),
% 64.91/64.96 inference(scs_inference,[],[428,156,28])).
% 64.91/64.96 cnf(675,plain,
% 64.91/64.96 (P1(f11(x6751,a6),x6752,f11(f11(x6753,a6),f11(x6754,a6)))),
% 64.91/64.96 inference(rename_variables,[],[428])).
% 64.91/64.96 cnf(677,plain,
% 64.91/64.96 (P1(f11(a6,a6),x6771,f7(a6,a6))),
% 64.91/64.96 inference(scs_inference,[],[428,447,156,246,28,26])).
% 64.91/64.96 cnf(679,plain,
% 64.91/64.96 (P3(f7(a6,a6),f7(a6,a6),f11(x6791,a6))),
% 64.91/64.96 inference(scs_inference,[],[428,447,156,53,246,235,28,26,23])).
% 64.91/64.96 cnf(688,plain,
% 64.91/64.96 (P3(f8(x6881),x6881,a6)),
% 64.91/64.96 inference(rename_variables,[],[10])).
% 64.91/64.96 cnf(698,plain,
% 64.91/64.96 (P1(f8(a6),x6981,f8(a6))),
% 64.91/64.96 inference(scs_inference,[],[428,675,421,447,545,621,156,153,88,53,201,10,688,342,289,246,235,519,28,26,23,24,21,22,32,30,31])).
% 64.91/64.96 cnf(716,plain,
% 64.91/64.96 (P2(f11(x7161,a6),f8(a6))),
% 64.91/64.96 inference(rename_variables,[],[379])).
% 64.91/64.96 cnf(719,plain,
% 64.91/64.96 (P3(x7191,f7(a6,a6),x7191)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(722,plain,
% 64.91/64.96 (P3(x7221,f7(a6,a6),x7221)),
% 64.91/64.96 inference(rename_variables,[],[53])).
% 64.91/64.96 cnf(724,plain,
% 64.91/64.97 (P3(f8(a6),f8(a6),f11(x7241,a6))),
% 64.91/64.97 inference(scs_inference,[],[376,238,565,389,53,719,289,379,716,588,136,25,24,26,23,21,22])).
% 64.91/64.97 cnf(735,plain,
% 64.91/64.97 (P1(f11(x7351,a6),x7352,f11(x7353,a6))),
% 64.91/64.97 inference(scs_inference,[],[376,238,447,115,565,473,389,53,719,9,6,645,289,379,716,588,136,25,24,26,23,21,22,32,30,31])).
% 64.91/64.97 cnf(738,plain,
% 64.91/64.97 (P3(f11(x7381,a6),f11(x7381,a6),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[376,238,447,115,565,473,677,389,53,719,722,9,6,645,289,379,716,588,136,25,24,26,23,21,22,32,30,31,33])).
% 64.91/64.97 cnf(755,plain,
% 64.91/64.97 (P2(f11(f11(x7551,a6),f11(x7552,a6)),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[327,428,677,39,25,28])).
% 64.91/64.97 cnf(789,plain,
% 64.91/64.97 (P1(f11(f11(x7891,a6),f11(x7892,a6)),x7893,f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[421,235,24])).
% 64.91/64.97 cnf(795,plain,
% 64.91/64.97 (P1(f7(a6,a6),x7951,f11(x7952,a6))),
% 64.91/64.97 inference(scs_inference,[],[421,201,235,418,755,24,23,26])).
% 64.91/64.97 cnf(796,plain,
% 64.91/64.97 (P2(f11(f11(x7961,a6),f11(x7962,a6)),f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[755])).
% 64.91/64.97 cnf(802,plain,
% 64.91/64.97 (P3(x8021,a6,x8021)),
% 64.91/64.97 inference(rename_variables,[],[5])).
% 64.91/64.97 cnf(808,plain,
% 64.91/64.97 (P3(f11(x8081,a6),f11(x8082,a6),f11(x8083,a6))),
% 64.91/64.97 inference(scs_inference,[],[421,153,201,389,491,5,802,9,235,418,755,796,519,24,23,26,22,21,29,30])).
% 64.91/64.97 cnf(826,plain,
% 64.91/64.97 (P1(a6,x8261,f11(x8262,a6))),
% 64.91/64.97 inference(scs_inference,[],[327,421,53,379,235,673,25,24,23,26])).
% 64.91/64.97 cnf(829,plain,
% 64.91/64.97 (P3(f8(x8291),x8291,f11(x8292,a6))),
% 64.91/64.97 inference(scs_inference,[],[327,421,10,53,181,379,235,673,25,24,23,26,21])).
% 64.91/64.97 cnf(834,plain,
% 64.91/64.97 (P1(f11(a6,a6),x8341,f11(f11(x8342,a6),x8343))),
% 64.91/64.97 inference(scs_inference,[],[327,421,56,82,473,384,10,53,679,181,379,235,673,25,24,23,26,21,30,31])).
% 64.91/64.97 cnf(839,plain,
% 64.91/64.97 (P2(f11(x8391,a6),f7(a6,f7(a6,a6)))),
% 64.91/64.97 inference(scs_inference,[],[91,11,27])).
% 64.91/64.97 cnf(842,plain,
% 64.91/64.97 (P2(f7(a6,a6),f11(x8421,a6))),
% 64.91/64.97 inference(scs_inference,[],[447,795,91,11,27,28])).
% 64.91/64.97 cnf(850,plain,
% 64.91/64.97 (P1(f11(x8501,a6),x8502,f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[327,447,795,91,389,11,235,27,28,22,24,26])).
% 64.91/64.97 cnf(855,plain,
% 64.91/64.97 (P3(a6,f7(a6,a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[327,447,795,91,201,389,11,379,235,519,27,28,22,24,26,23,21])).
% 64.91/64.97 cnf(870,plain,
% 64.91/64.97 (P3(f8(a6),f11(x8701,a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[327,447,56,82,795,698,91,201,389,10,9,663,11,479,379,235,519,27,28,22,24,26,23,21,29,30,31,34])).
% 64.91/64.97 cnf(879,plain,
% 64.91/64.97 (P1(f11(f11(x8791,a6),f11(x8792,a6)),x8793,a6)),
% 64.91/64.97 inference(scs_inference,[],[421,39,24])).
% 64.91/64.97 cnf(933,plain,
% 64.91/64.97 (P3(a6,a6,f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[6,289,22])).
% 64.91/64.97 cnf(967,plain,
% 64.91/64.97 (P3(f8(a6),f7(a6,a6),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[88,389,6,9,519,197,588,829,22,21,29,30])).
% 64.91/64.97 cnf(985,plain,
% 64.91/64.97 (P2(f8(a6),f11(x9851,a6))),
% 64.91/64.97 inference(scs_inference,[],[5,829,27])).
% 64.91/64.97 cnf(992,plain,
% 64.91/64.97 (P2(f8(a6),f11(f11(x9921,a6),x9922))),
% 64.91/64.97 inference(scs_inference,[],[559,565,834,5,39,829,27,25,28])).
% 64.91/64.97 cnf(996,plain,
% 64.91/64.97 (P1(f8(a6),x9961,f11(x9962,a6))),
% 64.91/64.97 inference(scs_inference,[],[559,466,565,834,5,39,379,829,27,25,28,26])).
% 64.91/64.97 cnf(997,plain,
% 64.91/64.97 (P2(f11(x9971,a6),f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[379])).
% 64.91/64.97 cnf(1000,plain,
% 64.91/64.97 (P3(a6,f8(a6),f11(x10001,a6))),
% 64.91/64.97 inference(scs_inference,[],[559,466,565,834,349,5,39,379,997,829,27,25,28,26,22])).
% 64.91/64.97 cnf(1034,plain,
% 64.91/64.97 (P2(f8(f7(a6,a6)),f11(x10341,a6))),
% 64.91/64.97 inference(scs_inference,[],[53,829,27])).
% 64.91/64.97 cnf(1058,plain,
% 64.91/64.97 (P1(x10581,f11(x10582,a6),f11(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[56,181,25])).
% 64.91/64.97 cnf(1060,plain,
% 64.91/64.97 (P2(f11(a6,a6),f11(x10601,f11(x10602,a6)))),
% 64.91/64.97 inference(scs_inference,[],[56,79,181,25,28])).
% 64.91/64.97 cnf(1064,plain,
% 64.91/64.97 (P3(x10641,a6,x10641)),
% 64.91/64.97 inference(rename_variables,[],[5])).
% 64.91/64.97 cnf(1072,plain,
% 64.91/64.97 (P3(f8(a3),a5,f8(a4))),
% 64.91/64.97 inference(scs_inference,[],[56,79,349,5,1064,10,6,181,8,839,673,1034,25,28,23,22,21,30])).
% 64.91/64.97 cnf(1076,plain,
% 64.91/64.97 (P1(x10761,f11(x10762,a6),f7(f11(a6,a6),f11(a6,a6)))),
% 64.91/64.97 inference(scs_inference,[],[56,79,88,349,5,1064,10,6,11,181,8,839,673,1034,25,28,23,22,21,30,36])).
% 64.91/64.97 cnf(1077,plain,
% 64.91/64.97 (P3(x10771,x10772,f7(x10771,x10772))),
% 64.91/64.97 inference(rename_variables,[],[11])).
% 64.91/64.97 cnf(1082,plain,
% 64.91/64.97 (P3(f8(a6),f8(a6),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[327,56,591,735,789,79,88,349,5,1064,10,6,11,181,8,839,673,1034,25,28,23,22,21,30,36,31,33])).
% 64.91/64.97 cnf(1086,plain,
% 64.91/64.97 (P3(a6,a6,f11(x10861,a6))),
% 64.91/64.97 inference(rename_variables,[],[88])).
% 64.91/64.97 cnf(1088,plain,
% 64.91/64.97 (P1(f11(x10881,a6),x10882,f7(f11(x10883,a6),f11(x10883,a6)))),
% 64.91/64.97 inference(scs_inference,[],[327,56,591,735,826,789,79,88,1086,349,5,1064,10,6,11,1077,181,8,839,673,1034,25,28,23,22,21,30,36,31,33,35])).
% 64.91/64.97 cnf(1101,plain,
% 64.91/64.97 (P3(f11(x11011,f11(x11012,a6)),a6,f11(x11013,a6))),
% 64.91/64.97 inference(scs_inference,[],[56,1088,201,349,519,1060,28,22,23])).
% 64.91/64.97 cnf(1107,plain,
% 64.91/64.97 (P3(f8(a2),a10,f8(a9))),
% 64.91/64.97 inference(scs_inference,[],[56,1088,201,349,5,10,6,7,519,1034,1060,28,22,23,21,30])).
% 64.91/64.97 cnf(1124,plain,
% 64.91/64.97 (P2(f8(a6),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[591,789,28])).
% 64.91/64.97 cnf(1127,plain,
% 64.91/64.97 (P1(f7(a6,a6),x11271,f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[591,789,755,28,26])).
% 64.91/64.97 cnf(1128,plain,
% 64.91/64.97 (P2(f11(f11(x11281,a6),f11(x11282,a6)),f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[755])).
% 64.91/64.97 cnf(1134,plain,
% 64.91/64.97 (P3(f7(a6,a6),f11(x11341,a6),a6)),
% 64.91/64.97 inference(scs_inference,[],[591,82,789,9,755,1128,1034,28,26,24,22])).
% 64.91/64.97 cnf(1140,plain,
% 64.91/64.97 (P3(f8(a6),f8(a6),a6)),
% 64.91/64.97 inference(scs_inference,[],[591,82,789,549,53,9,289,755,1128,1034,28,26,24,22,23,21])).
% 64.91/64.97 cnf(1142,plain,
% 64.91/64.97 (P3(f7(a6,a6),f8(a6),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[591,82,789,549,53,9,289,755,1128,1034,1082,28,26,24,22,23,21,29])).
% 64.91/64.97 cnf(1157,plain,
% 64.91/64.97 (P1(a6,x11571,f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[826,591,79,673,28,26])).
% 64.91/64.97 cnf(1179,plain,
% 64.91/64.97 (P1(f7(a6,a6),x11791,f11(x11792,a6))),
% 64.91/64.97 inference(rename_variables,[],[795])).
% 64.91/64.97 cnf(1181,plain,
% 64.91/64.97 (P1(f7(a6,a6),x11811,a6)),
% 64.91/64.97 inference(scs_inference,[],[795,1179,79,39,28,24])).
% 64.91/64.97 cnf(1185,plain,
% 64.91/64.97 (P2(f11(x11851,a6),f7(f8(a6),a6))),
% 64.91/64.97 inference(rename_variables,[],[418])).
% 64.91/64.97 cnf(1194,plain,
% 64.91/64.97 (P1(f8(a6),x11941,a6)),
% 64.91/64.97 inference(scs_inference,[],[795,1179,591,879,79,88,349,10,6,39,418,1185,1107,28,24,22,21,30,31])).
% 64.91/64.97 cnf(1207,plain,
% 64.91/64.97 (P2(f11(x12071,a6),f11(f7(a6,a6),x12072))),
% 64.91/64.97 inference(scs_inference,[],[795,12,28])).
% 64.91/64.97 cnf(1210,plain,
% 64.91/64.97 (P1(f7(a6,a6),x12101,f7(f11(x12102,a6),f11(x12102,a6)))),
% 64.91/64.97 inference(scs_inference,[],[795,136,12,28,24])).
% 64.91/64.97 cnf(1222,plain,
% 64.91/64.97 (P3(f11(a6,x12221),f11(a6,x12221),f11(a6,x12221))),
% 64.91/64.97 inference(rename_variables,[],[67])).
% 64.91/64.97 cnf(1228,plain,
% 64.91/64.97 (P1(f8(a6),x12281,f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[795,591,789,88,349,201,67,1222,136,12,1060,1101,28,24,23,22,21,29,30,31])).
% 64.91/64.97 cnf(1236,plain,
% 64.91/64.97 (P1(a6,x12361,f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[826,698,235,992,26,24])).
% 64.91/64.97 cnf(1239,plain,
% 64.91/64.97 (P2(f11(x12391,a6),f7(f11(x12392,a6),f11(x12392,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,795,698,1210,235,992,26,24,28])).
% 64.91/64.97 cnf(1258,plain,
% 64.91/64.97 (P2(f11(x12581,a6),f11(a6,x12582))),
% 64.91/64.97 inference(scs_inference,[],[826,12,839,24,28])).
% 64.91/64.97 cnf(1261,plain,
% 64.91/64.97 (P3(f11(a6,x12611),a6,f11(x12612,a6))),
% 64.91/64.97 inference(scs_inference,[],[826,201,12,839,24,28,23])).
% 64.91/64.97 cnf(1278,plain,
% 64.91/64.97 (P1(f7(a6,a6),x12781,f11(f11(x12782,a6),x12783))),
% 64.91/64.97 inference(scs_inference,[],[795,519,24])).
% 64.91/64.97 cnf(1284,plain,
% 64.91/64.97 (P3(a6,a6,f11(a6,x12841))),
% 64.91/64.97 inference(scs_inference,[],[795,88,10,519,1124,1258,24,22,21])).
% 64.91/64.97 cnf(1300,plain,
% 64.91/64.97 (P3(a6,f11(a6,x13001),f11(x13002,a6))),
% 64.91/64.97 inference(scs_inference,[],[826,349,519,1258,24,22])).
% 64.91/64.97 cnf(1308,plain,
% 64.91/64.97 (P2(f7(a6,a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[447,1127,28])).
% 64.91/64.97 cnf(1309,plain,
% 64.91/64.97 (P1(f7(a6,a6),x13091,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1127])).
% 64.91/64.97 cnf(1313,plain,
% 64.91/64.97 (P3(f7(a6,a6),a6,f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[447,698,1127,5,992,28,24,21])).
% 64.91/64.97 cnf(1316,plain,
% 64.91/64.97 (P3(f7(a6,a6),f7(a6,a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[447,698,1127,1309,88,5,992,28,24,21,33])).
% 64.91/64.97 cnf(1336,plain,
% 64.91/64.97 (P1(a6,x13361,f11(x13362,f11(x13363,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,1060,24])).
% 64.91/64.97 cnf(1353,plain,
% 64.91/64.97 (P2(f11(x13531,a6),f11(x13532,f11(x13533,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,1336,28])).
% 64.91/64.97 cnf(1382,plain,
% 64.91/64.97 (P2(f11(x13821,a6),f8(f7(a6,a6)))),
% 64.91/64.97 inference(scs_inference,[],[829,53,27])).
% 64.91/64.97 cnf(1384,plain,
% 64.91/64.97 (P3(f8(x13841),x13841,f11(x13842,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1386,plain,
% 64.91/64.97 (P1(a6,x13861,f11(a6,x13862))),
% 64.91/64.97 inference(scs_inference,[],[826,829,53,1258,27,24])).
% 64.91/64.97 cnf(1389,plain,
% 64.91/64.97 (P3(f8(f7(a6,a6)),f11(x13891,a6),f11(x13892,a6))),
% 64.91/64.97 inference(scs_inference,[],[826,829,1384,53,842,1258,27,24,22])).
% 64.91/64.97 cnf(1390,plain,
% 64.91/64.97 (P3(f8(x13901),x13901,f11(x13902,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1392,plain,
% 64.91/64.97 (P3(f8(x13921),x13921,f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[826,829,1384,1390,53,842,379,1258,27,24,22,21])).
% 64.91/64.97 cnf(1395,plain,
% 64.91/64.97 (P3(f11(x13951,a6),x13952,f8(f8(x13952)))),
% 64.91/64.97 inference(scs_inference,[],[826,829,1384,1390,10,53,5,842,379,1258,27,24,22,21,29])).
% 64.91/64.97 cnf(1397,plain,
% 64.91/64.97 (P3(f8(x13971),x13971,f11(x13972,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1399,plain,
% 64.91/64.97 (P3(f8(x13991),f7(x13991,a6),f11(x13992,a6))),
% 64.91/64.97 inference(scs_inference,[],[826,829,1384,1390,1397,10,201,53,5,11,842,379,1258,27,24,22,21,29,30])).
% 64.91/64.97 cnf(1400,plain,
% 64.91/64.97 (P3(x14001,x14002,f7(x14001,x14002))),
% 64.91/64.97 inference(rename_variables,[],[11])).
% 64.91/64.97 cnf(1401,plain,
% 64.91/64.97 (P3(f8(x14011),x14011,f11(x14012,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1403,plain,
% 64.91/64.97 (P1(f11(x14031,a6),x14032,f11(a6,x14033))),
% 64.91/64.97 inference(scs_inference,[],[826,447,829,1384,1390,1397,10,201,53,5,11,842,379,1258,27,24,22,21,29,30,31])).
% 64.91/64.97 cnf(1404,plain,
% 64.91/64.97 (P1(a6,x14041,f11(x14042,a6))),
% 64.91/64.97 inference(rename_variables,[],[826])).
% 64.91/64.97 cnf(1406,plain,
% 64.91/64.97 (P3(f11(x14061,a6),f11(x14061,a6),f11(a6,x14062))),
% 64.91/64.97 inference(scs_inference,[],[826,1404,447,829,1384,1390,1397,88,10,201,53,5,11,842,379,1258,27,24,22,21,29,30,31,34])).
% 64.91/64.97 cnf(1409,plain,
% 64.91/64.97 (P3(x14091,x14092,f7(x14091,x14092))),
% 64.91/64.97 inference(rename_variables,[],[11])).
% 64.91/64.97 cnf(1410,plain,
% 64.91/64.97 (P3(f8(x14101),x14101,f11(x14102,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1413,plain,
% 64.91/64.97 (P1(f11(x14131,a6),x14132,f7(f8(a6),f11(x14133,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,1404,447,698,1157,829,1384,1390,1397,1401,1410,88,10,201,53,5,11,1400,1409,842,379,1258,27,24,22,21,29,30,31,34,36,35])).
% 64.91/64.97 cnf(1418,plain,
% 64.91/64.97 (P2(f11(a6,a6),f7(f8(a6),f11(x14181,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,1404,447,698,56,1157,829,1384,1390,1397,1401,1410,88,10,201,53,5,11,1400,1409,842,379,1258,27,24,22,21,29,30,31,34,36,35,28])).
% 64.91/64.97 cnf(1424,plain,
% 64.91/64.97 (P2(f11(x14241,a6),f7(f8(x14242),x14242))),
% 64.91/64.97 inference(scs_inference,[],[829,11,27])).
% 64.91/64.97 cnf(1425,plain,
% 64.91/64.97 (P3(x14251,x14252,f7(x14251,x14252))),
% 64.91/64.97 inference(rename_variables,[],[11])).
% 64.91/64.97 cnf(1430,plain,
% 64.91/64.97 (P1(a6,x14301,f11(x14302,a6))),
% 64.91/64.97 inference(rename_variables,[],[826])).
% 64.91/64.97 cnf(1433,plain,
% 64.91/64.97 (P3(f8(x14331),x14331,f11(x14332,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1435,plain,
% 64.91/64.97 (P3(f8(x14351),x14351,f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[826,829,1433,201,11,235,1418,27,23,24,22,21])).
% 64.91/64.97 cnf(1440,plain,
% 64.91/64.97 (P3(f8(x14401),x14401,f11(x14402,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1446,plain,
% 64.91/64.97 (P1(f11(x14461,a6),x14462,f7(f8(a6),f11(x14463,a6)))),
% 64.91/64.97 inference(rename_variables,[],[1413])).
% 64.91/64.97 cnf(1453,plain,
% 64.91/64.97 (P2(f11(x14531,a6),f7(f8(a6),f11(x14532,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,1430,56,1413,1446,829,1433,1440,88,201,11,1425,197,235,1418,27,23,24,22,21,29,30,33,34,28])).
% 64.91/64.97 cnf(1456,plain,
% 64.91/64.97 (P2(a6,f8(f7(a6,a6)))),
% 64.91/64.97 inference(scs_inference,[],[10,53,27])).
% 64.91/64.97 cnf(1457,plain,
% 64.91/64.97 (P3(x14571,f7(a6,a6),x14571)),
% 64.91/64.97 inference(rename_variables,[],[53])).
% 64.91/64.97 cnf(1458,plain,
% 64.91/64.97 (P3(f8(x14581),x14581,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(1462,plain,
% 64.91/64.97 (P3(f8(a6),f11(x14621,a6),a6)),
% 64.91/64.97 inference(scs_inference,[],[826,10,1458,53,181,27,26,22])).
% 64.91/64.97 cnf(1463,plain,
% 64.91/64.97 (P3(f8(x14631),x14631,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(1466,plain,
% 64.91/64.97 (P2(f11(x14661,a6),f7(f8(x14662),x14662))),
% 64.91/64.97 inference(rename_variables,[],[1424])).
% 64.91/64.97 cnf(1476,plain,
% 64.91/64.97 (P3(f7(a6,a6),f8(a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[826,10,1458,1463,88,53,1457,9,6,181,1316,1424,1466,27,26,22,24,21,29,30])).
% 64.91/64.97 cnf(1487,plain,
% 64.91/64.97 (P2(f11(x14871,a6),f8(f8(a6)))),
% 64.91/64.97 inference(scs_inference,[],[201,1395,27])).
% 64.91/64.97 cnf(1494,plain,
% 64.91/64.97 (P3(f8(x14941),x14941,f11(x14942,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1496,plain,
% 64.91/64.97 (P3(f8(x14961),x14961,f7(a6,f7(a6,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,829,1494,201,839,1395,1382,1308,27,24,22,21])).
% 64.91/64.97 cnf(1500,plain,
% 64.91/64.97 (P3(f8(x15001),x15001,f11(x15002,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1506,plain,
% 64.91/64.97 (P1(f11(x15061,a6),x15062,f8(f7(a6,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,447,829,1494,1500,201,536,839,1395,1382,1308,27,24,22,21,29,30,31])).
% 64.91/64.97 cnf(1517,plain,
% 64.91/64.97 (P2(a6,f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[10,5,27])).
% 64.91/64.97 cnf(1519,plain,
% 64.91/64.97 (P3(f8(x15191),x15191,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(1528,plain,
% 64.91/64.97 (P3(f8(x15281),x15281,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(1530,plain,
% 64.91/64.97 (P3(f8(x15301),x15301,f11(f11(x15302,a6),x15303))),
% 64.91/64.97 inference(scs_inference,[],[826,10,1519,829,384,5,842,839,519,1487,27,23,24,22,21])).
% 64.91/64.97 cnf(1534,plain,
% 64.91/64.97 (P3(f8(x15341),x15341,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(1541,plain,
% 64.91/64.97 (P1(f11(x15411,a6),x15412,f8(f8(a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,447,10,1519,1528,1534,829,384,5,9,842,839,519,1487,1476,27,23,24,22,21,29,30,31])).
% 64.91/64.97 cnf(1542,plain,
% 64.91/64.97 (P1(a6,x15421,f11(x15422,a6))),
% 64.91/64.97 inference(rename_variables,[],[826])).
% 64.91/64.97 cnf(1544,plain,
% 64.91/64.97 (P3(f11(x15441,a6),f11(x15441,a6),f8(f7(a6,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,1542,447,1506,10,1519,1528,1534,829,88,384,5,9,842,839,519,1487,1476,27,23,24,22,21,29,30,31,34])).
% 64.91/64.97 cnf(1553,plain,
% 64.91/64.97 (P2(a6,f7(f8(x15531),x15531))),
% 64.91/64.97 inference(scs_inference,[],[10,11,27])).
% 64.91/64.97 cnf(1559,plain,
% 64.91/64.97 (P3(f8(x15591),x15591,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(1561,plain,
% 64.91/64.97 (P3(f8(x15611),x15611,f11(x15612,f11(x15613,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,10,829,11,1353,27,26,22,21])).
% 64.91/64.97 cnf(1567,plain,
% 64.91/64.97 (P3(f11(x15671,a6),f11(x15671,a6),f8(f8(a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,1541,10,1559,829,88,11,1353,1261,27,26,22,21,30,34])).
% 64.91/64.97 cnf(1571,plain,
% 64.91/64.97 (P3(f8(x15711),x15711,f8(f7(a6,a6)))),
% 64.91/64.97 inference(scs_inference,[],[10,1456,21])).
% 64.91/64.97 cnf(1590,plain,
% 64.91/64.97 (P2(a6,f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[10,1435,27])).
% 64.91/64.97 cnf(1596,plain,
% 64.91/64.97 (P3(f8(x15961),x15961,f7(f8(a6),f11(x15962,a6)))),
% 64.91/64.97 inference(scs_inference,[],[10,829,384,1435,519,1453,27,23,21])).
% 64.91/64.97 cnf(1609,plain,
% 64.91/64.97 (P2(f11(x16091,a6),f7(f8(x16092),x16092))),
% 64.91/64.97 inference(rename_variables,[],[1424])).
% 64.91/64.97 cnf(1611,plain,
% 64.91/64.97 (P3(f8(x16111),x16111,f7(f8(x16112),x16112))),
% 64.91/64.97 inference(scs_inference,[],[829,384,1424,1609,23,21])).
% 64.91/64.97 cnf(1627,plain,
% 64.91/64.97 (P2(a6,f11(f11(x16271,a6),x16272))),
% 64.91/64.97 inference(scs_inference,[],[10,1530,27])).
% 64.91/64.97 cnf(1638,plain,
% 64.91/64.97 (P3(f8(x16381),x16381,f7(f11(x16382,a6),f11(x16382,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,10,829,384,1530,1353,1239,27,26,23,22,21])).
% 64.91/64.97 cnf(1648,plain,
% 64.91/64.97 (P3(f8(x16481),x16481,f11(x16482,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1650,plain,
% 64.91/64.97 (P3(f8(x16501),x16501,f11(f7(a6,a6),x16502))),
% 64.91/64.97 inference(scs_inference,[],[829,1648,1207,1553,22,21])).
% 64.91/64.97 cnf(1663,plain,
% 64.91/64.97 (P2(a6,f7(a6,f7(a6,a6)))),
% 64.91/64.97 inference(scs_inference,[],[10,1496,27])).
% 64.91/64.97 cnf(1672,plain,
% 64.91/64.97 (P3(f8(x16721),x16721,f11(a6,x16722))),
% 64.91/64.97 inference(scs_inference,[],[10,829,384,1496,1453,1258,27,23,22,21])).
% 64.91/64.97 cnf(1684,plain,
% 64.91/64.97 (P3(f8(x16841),x16841,f8(f8(a6)))),
% 64.91/64.97 inference(scs_inference,[],[829,1487,21])).
% 64.91/64.97 cnf(1729,plain,
% 64.91/64.97 (P2(a6,f11(x17291,f11(x17292,a6)))),
% 64.91/64.97 inference(scs_inference,[],[10,1561,27])).
% 64.91/64.97 cnf(1746,plain,
% 64.91/64.97 (P3(f11(x17461,a6),a6,f11(a6,x17462))),
% 64.91/64.97 inference(scs_inference,[],[829,201,1672,29])).
% 64.91/64.97 cnf(1760,plain,
% 64.91/64.97 (P3(f11(a6,x17601),f7(a6,a6),f11(x17602,a6))),
% 64.91/64.97 inference(scs_inference,[],[826,10,384,1650,1258,27,26,23])).
% 64.91/64.97 cnf(1764,plain,
% 64.91/64.97 (P3(f8(x17641),x17641,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(1766,plain,
% 64.91/64.97 (P3(a6,f7(a6,a6),f11(a6,x17661))),
% 64.91/64.97 inference(scs_inference,[],[826,10,1764,384,1650,1672,1258,27,26,23,22,29])).
% 64.91/64.97 cnf(1798,plain,
% 64.91/64.97 (P3(f8(x17981),x17981,f11(x17982,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(1801,plain,
% 64.91/64.97 (P3(f8(a6),f11(a6,x18011),f11(x18012,a6))),
% 64.91/64.97 inference(scs_inference,[],[829,1798,201,384,1650,1766,29,30])).
% 64.91/64.97 cnf(1806,plain,
% 64.91/64.97 (P2(a6,f11(a6,x18061))),
% 64.91/64.97 inference(scs_inference,[],[10,1672,27])).
% 64.91/64.97 cnf(1813,plain,
% 64.91/64.97 (P3(f8(a6),f11(a6,x18131),a6)),
% 64.91/64.97 inference(scs_inference,[],[826,879,10,1672,27,26,24,22])).
% 64.91/64.97 cnf(1830,plain,
% 64.91/64.97 (P2(a6,f8(f8(a6)))),
% 64.91/64.97 inference(scs_inference,[],[10,1684,27])).
% 64.91/64.97 cnf(1961,plain,
% 64.91/64.97 (P2(f11(a6,x19611),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[1672,1392,27])).
% 64.91/64.97 cnf(1962,plain,
% 64.91/64.97 (P3(f8(x19621),x19621,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(1964,plain,
% 64.91/64.97 (P3(f11(x19641,a6),f7(a6,a6),f11(a6,x19642))),
% 64.91/64.97 inference(scs_inference,[],[1672,1392,1034,27,23])).
% 64.91/64.97 cnf(1965,plain,
% 64.91/64.97 (P3(f8(x19651),x19651,f11(a6,x19652))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(1968,plain,
% 64.91/64.97 (P3(f8(x19681),x19681,f11(a6,x19682))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(1970,plain,
% 64.91/64.97 (P3(f11(a6,x19701),f7(a6,a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[1672,1965,1968,1392,1962,1571,342,1034,27,23,22,29])).
% 64.91/64.97 cnf(1992,plain,
% 64.91/64.97 (P2(f11(a6,x19921),f11(x19922,a6))),
% 64.91/64.97 inference(scs_inference,[],[1672,829,27])).
% 64.91/64.97 cnf(1995,plain,
% 64.91/64.97 (P3(f7(a6,a6),a6,f11(a6,x19951))),
% 64.91/64.97 inference(scs_inference,[],[1672,829,1124,27,23])).
% 64.91/64.97 cnf(1996,plain,
% 64.91/64.97 (P3(f8(x19961),x19961,f11(a6,x19962))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(1998,plain,
% 64.91/64.97 (P3(f8(a6),f11(x19981,a6),f11(a6,x19982))),
% 64.91/64.97 inference(scs_inference,[],[1672,1996,829,181,1124,27,23,22])).
% 64.91/64.97 cnf(1999,plain,
% 64.91/64.97 (P3(f8(x19991),x19991,f11(a6,x19992))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2001,plain,
% 64.91/64.97 (P3(f11(a6,x20011),a6,a6)),
% 64.91/64.97 inference(scs_inference,[],[1672,1996,1999,829,10,1392,181,1124,27,23,22,29])).
% 64.91/64.97 cnf(2003,plain,
% 64.91/64.97 (P3(f8(x20031),x20031,f11(a6,x20032))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2006,plain,
% 64.91/64.97 (P3(a6,f8(a6),f11(a6,x20061))),
% 64.91/64.97 inference(scs_inference,[],[1672,1996,1999,2003,829,10,1392,933,181,1124,27,23,22,29,30])).
% 64.91/64.97 cnf(2018,plain,
% 64.91/64.97 (P3(f8(x20181),x20181,f11(a6,x20182))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2020,plain,
% 64.91/64.97 (P2(f11(a6,x20201),a6)),
% 64.91/64.97 inference(scs_inference,[],[1672,2018,10,842,22,27])).
% 64.91/64.97 cnf(2038,plain,
% 64.91/64.97 (P3(f8(x20381),x20381,f11(x20382,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(2040,plain,
% 64.91/64.97 (P2(a3,f11(a1,a2))),
% 64.91/64.97 inference(scs_inference,[],[1,829,12,2020,22,28])).
% 64.91/64.97 cnf(2041,plain,
% 64.91/64.97 (P1(x20411,x20412,f11(x20411,x20412))),
% 64.91/64.97 inference(rename_variables,[],[12])).
% 64.91/64.97 cnf(2055,plain,
% 64.91/64.97 (P1(x20551,x20552,f11(x20551,x20552))),
% 64.91/64.97 inference(rename_variables,[],[12])).
% 64.91/64.97 cnf(2056,plain,
% 64.91/64.97 (P3(x20561,x20562,f7(x20561,x20562))),
% 64.91/64.97 inference(rename_variables,[],[11])).
% 64.91/64.97 cnf(2062,plain,
% 64.91/64.97 (P3(a3,f7(a6,a6),f11(a1,a2))),
% 64.91/64.97 inference(scs_inference,[],[1,826,56,1336,79,829,2038,201,53,11,2056,12,2041,2055,1995,2020,22,28,32,30,31,33,34,21])).
% 64.91/64.97 cnf(2063,plain,
% 64.91/64.97 (P3(x20631,f7(a6,a6),x20631)),
% 64.91/64.97 inference(rename_variables,[],[53])).
% 64.91/64.97 cnf(2065,plain,
% 64.91/64.97 (P3(f11(a1,a2),f7(a6,a6),a3)),
% 64.91/64.97 inference(scs_inference,[],[1,826,56,1336,79,829,2038,201,53,2063,11,2056,12,2041,2055,1995,2020,22,28,32,30,31,33,34,21,23])).
% 64.91/64.97 cnf(2081,plain,
% 64.91/64.97 (P3(f8(x20811),x20811,f11(a6,x20812))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2086,plain,
% 64.91/64.97 (P1(a1,f11(a6,a6),f11(x20861,a6))),
% 64.91/64.97 inference(scs_inference,[],[1,1058,1672,2081,1530,161,289,22,27,32])).
% 64.91/64.97 cnf(2091,plain,
% 64.91/64.97 (P3(f8(x20911),x20911,f11(a6,x20912))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2098,plain,
% 64.91/64.97 (P3(f11(a6,x20981),a6,f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[1,1058,79,1672,2081,2091,1392,1530,1435,11,161,3,289,7,22,27,32,30,31,29])).
% 64.91/64.97 cnf(2118,plain,
% 64.91/64.97 (P3(f8(x21181),x21181,f11(a6,x21182))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2124,plain,
% 64.91/64.97 (P3(f8(x21241),x21241,f11(a6,x21242))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2128,plain,
% 64.91/64.97 (P1(x21281,a6,f11(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[56])).
% 64.91/64.97 cnf(2139,plain,
% 64.91/64.97 (P1(f11(a6,x21391),x21392,f11(a6,x21391))),
% 64.91/64.97 inference(scs_inference,[],[1,735,56,2128,79,1672,2118,2124,1392,1435,1561,985,1406,1076,2001,22,27,30,32,31,29,35])).
% 64.91/64.97 cnf(2159,plain,
% 64.91/64.97 (P1(f7(a6,a6),x21591,f11(a6,x21592))),
% 64.91/64.97 inference(scs_inference,[],[447,1278,1181,10,1806,1992,22,28,24])).
% 64.91/64.97 cnf(2191,plain,
% 64.91/64.97 (P3(f8(x21911),x21911,f11(a6,x21912))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2196,plain,
% 64.91/64.97 (P1(f7(a6,a6),x21961,f7(f11(x21962,a6),f11(x21962,a6)))),
% 64.91/64.97 inference(rename_variables,[],[1210])).
% 64.91/64.97 cnf(2206,plain,
% 64.91/64.97 (P3(f8(x22061),x22061,f11(a6,x22062))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2210,plain,
% 64.91/64.97 (P3(f8(x22101),x22101,f11(a6,x22102))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2211,plain,
% 64.91/64.97 (P3(f8(x22111),x22111,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(2216,plain,
% 64.91/64.97 (P1(f7(a6,a6),x22161,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[447])).
% 64.91/64.97 cnf(2226,plain,
% 64.91/64.97 (~P1(f8(a1),a2,f8(a3))+P1(f11(a6,x22261),a2,f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[1,447,2216,996,56,1210,2196,1181,48,1672,2191,2206,2210,1392,2211,1561,1611,88,39,1456,73,1970,22,24,28,27,32,30,29,33,26,31,34,35])).
% 64.91/64.97 cnf(2235,plain,
% 64.91/64.97 (P3(f8(x22351),x22351,f11(a6,x22352))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2237,plain,
% 64.91/64.97 (P2(f7(a6,a6),a6)),
% 64.91/64.97 inference(scs_inference,[],[447,1181,1672,379,22,28])).
% 64.91/64.97 cnf(2238,plain,
% 64.91/64.97 (P1(f7(a6,a6),x22381,a6)),
% 64.91/64.97 inference(rename_variables,[],[1181])).
% 64.91/64.97 cnf(2246,plain,
% 64.91/64.97 (P3(f8(x22461),x22461,f11(a6,x22462))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2253,plain,
% 64.91/64.97 (P3(f7(a6,a6),f7(a6,a6),a6)),
% 64.91/64.97 inference(scs_inference,[],[447,1181,2238,1672,2235,2246,1392,1611,1596,88,379,1553,2098,22,28,24,27,30,29,33])).
% 64.91/64.97 cnf(2272,plain,
% 64.91/64.97 (P3(f8(a3),f11(a1,a2),f11(x22721,a6))),
% 64.91/64.97 inference(scs_inference,[],[829,2040,22])).
% 64.91/64.97 cnf(2290,plain,
% 64.91/64.97 (P3(f8(a6),f8(a6),f11(a6,x22901))),
% 64.91/64.97 inference(scs_inference,[],[1181,1672,1517,1663,24,22])).
% 64.91/64.97 cnf(2291,plain,
% 64.91/64.97 (P3(f8(x22911),x22911,f11(a6,x22912))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2301,plain,
% 64.91/64.97 (P3(f8(x23011),x23011,f11(a6,x23012))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2310,plain,
% 64.91/64.97 (~P1(f8(a1),a2,f8(a3))+P1(f11(a6,x23101),a2,f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[1,1157,1181,1672,2291,2301,1392,1435,1596,1638,444,3,1517,1663,1567,24,22,27,30,29,33,34,35])).
% 64.91/64.97 cnf(2319,plain,
% 64.91/64.97 (P3(f8(x23191),x23191,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(2323,plain,
% 64.91/64.97 (P3(f8(f8(a3)),f11(x23231,a6),f11(a1,a2))),
% 64.91/64.97 inference(scs_inference,[],[1181,10,2319,6,1830,1961,2272,22,24,30])).
% 64.91/64.97 cnf(2350,plain,
% 64.91/64.97 (P1(f7(a6,a6),x23501,f11(x23502,f11(x23503,a6)))),
% 64.91/64.97 inference(scs_inference,[],[1181,1672,1638,1308,1729,27,22,24])).
% 64.91/64.97 cnf(2390,plain,
% 64.91/64.97 (P3(f8(a3),f11(a1,a2),a6)),
% 64.91/64.97 inference(scs_inference,[],[10,2040,22])).
% 64.91/64.97 cnf(2408,plain,
% 64.91/64.97 (P3(f8(x24081),x24081,f11(a6,x24082))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2412,plain,
% 64.91/64.97 (P3(f8(x24121),x24121,f11(a6,x24122))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2415,plain,
% 64.91/64.97 (P1(f11(a6,x24151),x24152,a6)),
% 64.91/64.97 inference(scs_inference,[],[1157,1194,1672,2408,2412,1392,1650,1496,9,1258,27,22,29,35])).
% 64.91/64.97 cnf(2453,plain,
% 64.91/64.97 (P3(f8(a6),f7(a6,a6),f11(a6,x24531))),
% 64.91/64.97 inference(scs_inference,[],[1672,1496,1590,27,22])).
% 64.91/64.97 cnf(2454,plain,
% 64.91/64.97 (P3(f8(x24541),x24541,f11(a6,x24542))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2460,plain,
% 64.91/64.97 (P3(f11(a6,x24601),a6,f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[826,56,2350,1672,2454,1392,1496,201,1590,27,22,31,29])).
% 64.91/64.97 cnf(2491,plain,
% 64.91/64.97 (P3(f8(a6),f11(a6,x24911),f11(a6,x24912))),
% 64.91/64.97 inference(scs_inference,[],[1672,1571,1806,27,22])).
% 64.91/64.97 cnf(2526,plain,
% 64.91/64.97 (P3(f8(a6),f8(f7(a6,a6)),f11(a6,x25261))),
% 64.91/64.97 inference(scs_inference,[],[1672,1684,1456,27,22])).
% 64.91/64.97 cnf(2527,plain,
% 64.91/64.97 (P3(f8(x25271),x25271,f11(a6,x25272))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(2529,plain,
% 64.91/64.97 (P3(f11(a6,x25291),x25292,f8(f8(x25292)))),
% 64.91/64.97 inference(scs_inference,[],[1672,2527,1435,53,1684,1456,27,22,29])).
% 64.91/64.97 cnf(2605,plain,
% 64.91/64.97 (P2(f7(a6,a6),f11(a6,x26051))),
% 64.91/64.97 inference(scs_inference,[],[1435,1672,27])).
% 64.91/64.97 cnf(2631,plain,
% 64.91/64.97 (P3(f8(a6),f11(x26311,a6),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[1435,1561,181,27,22])).
% 64.91/64.97 cnf(2632,plain,
% 64.91/64.97 (P3(f8(x26321),x26321,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2636,plain,
% 64.91/64.97 (P3(f8(x26361),x26361,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2639,plain,
% 64.91/64.97 (P3(a6,f8(a6),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[1435,2632,2636,1392,1561,1611,181,933,27,22,29,30])).
% 64.91/64.97 cnf(2754,plain,
% 64.91/64.97 (P3(f8(x27541),x27541,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2758,plain,
% 64.91/64.97 (P3(f8(x27581),x27581,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2762,plain,
% 64.91/64.97 (P3(f8(x27621),x27621,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2767,plain,
% 64.91/64.97 (P3(f8(x27671),x27671,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2769,plain,
% 64.91/64.97 (~P1(a1,f8(a2),f8(a3))+P1(a1,f7(a6,a6),a6)),
% 64.91/64.97 inference(scs_inference,[],[1,1435,2754,2758,2762,2767,10,1392,1611,1638,985,11,8,2529,27,22,29,30,35,36])).
% 64.91/64.97 cnf(2775,plain,
% 64.91/64.97 (P3(f8(x27751),x27751,f11(f7(a6,a6),x27752))),
% 64.91/64.97 inference(rename_variables,[],[1650])).
% 64.91/64.97 cnf(2778,plain,
% 64.91/64.97 (P3(f8(x27781),x27781,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2782,plain,
% 64.91/64.97 (P3(f8(x27821),x27821,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2786,plain,
% 64.91/64.97 (P3(f8(x27861),x27861,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2789,plain,
% 64.91/64.97 (~P1(a1,f8(a2),f8(a3))+P1(a1,f7(a6,a6),f11(a6,x27891))),
% 64.91/64.97 inference(scs_inference,[],[1,1435,2778,2782,2786,1672,1392,1650,2775,1258,9,2526,27,22,29,30,36])).
% 64.91/64.97 cnf(2807,plain,
% 64.91/64.97 (P3(x28071,f7(a6,a6),x28071)),
% 64.91/64.97 inference(rename_variables,[],[53])).
% 64.91/64.97 cnf(2808,plain,
% 64.91/64.97 (P3(f8(x28081),x28081,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2810,plain,
% 64.91/64.97 (P3(f8(a6),f11(a6,x28101),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[1435,2808,1806,53,27,22])).
% 64.91/64.97 cnf(2811,plain,
% 64.91/64.97 (P3(f8(x28111),x28111,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2815,plain,
% 64.91/64.97 (P3(f8(x28151),x28151,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2818,plain,
% 64.91/64.97 (~P1(a1,f8(a2),f8(a3))+P1(a1,f7(a6,a6),f11(x28181,a6))),
% 64.91/64.97 inference(scs_inference,[],[1,1435,2808,2811,2815,829,1806,53,2807,5,27,22,29,36])).
% 64.91/64.97 cnf(2844,plain,
% 64.91/64.97 (P3(a3,a6,f11(a1,a2))),
% 64.91/64.97 inference(scs_inference,[],[5,2040,21])).
% 64.91/64.97 cnf(2845,plain,
% 64.91/64.97 (P3(x28451,a6,x28451)),
% 64.91/64.97 inference(rename_variables,[],[5])).
% 64.91/64.97 cnf(2847,plain,
% 64.91/64.97 (P3(f11(a1,a2),a6,a3)),
% 64.91/64.97 inference(scs_inference,[],[5,2845,2040,21,23])).
% 64.91/64.97 cnf(2878,plain,
% 64.91/64.97 (P2(f7(a6,a6),f8(f8(a6)))),
% 64.91/64.97 inference(scs_inference,[],[1435,1684,27])).
% 64.91/64.97 cnf(2882,plain,
% 64.91/64.97 (P3(f8(x28821),x28821,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2886,plain,
% 64.91/64.97 (P3(f8(x28861),x28861,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(2889,plain,
% 64.91/64.97 (~P1(a1,f8(a2),f8(a3))+P1(a1,f7(a6,a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[1,1435,2882,2886,1392,1456,9,6,1684,27,22,29,36])).
% 64.91/64.97 cnf(2965,plain,
% 64.91/64.97 (P3(x29651,x29652,f7(x29651,x29652))),
% 64.91/64.97 inference(rename_variables,[],[11])).
% 64.91/64.97 cnf(2966,plain,
% 64.91/64.97 (P3(a6,f7(a6,a6),f11(x29661,a6))),
% 64.91/64.97 inference(rename_variables,[],[91])).
% 64.91/64.97 cnf(2968,plain,
% 64.91/64.97 (P1(f11(x29681,a6),x29682,f7(f11(x29683,a6),f11(x29684,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,795,91,2966,384,11,2965,2878,22,30,35])).
% 64.91/64.97 cnf(2982,plain,
% 64.91/64.97 (P1(a6,x29821,f7(f11(x29822,a6),f11(x29823,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,56,2968,28,24])).
% 64.91/64.97 cnf(3007,plain,
% 64.91/64.97 (P3(f11(a6,x30071),f11(x30072,a6),f11(x30073,a6))),
% 64.91/64.97 inference(scs_inference,[],[1258,808,23])).
% 64.91/64.97 cnf(3010,plain,
% 64.91/64.97 (P2(f11(x30101,a6),f7(f11(x30102,a6),f11(x30103,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,2982,1258,808,23,28])).
% 64.91/64.97 cnf(3011,plain,
% 64.91/64.97 (P1(a6,x30111,f7(f11(x30112,a6),f11(x30113,a6)))),
% 64.91/64.97 inference(rename_variables,[],[2982])).
% 64.91/64.97 cnf(3014,plain,
% 64.91/64.97 (P3(f8(x30141),x30141,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(3016,plain,
% 64.91/64.97 (P3(f7(a6,a6),f11(x30161,a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[826,2982,1435,3014,1258,1392,1627,808,23,28,22,29])).
% 64.91/64.97 cnf(3018,plain,
% 64.91/64.97 (P3(f8(x30181),x30181,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(3026,plain,
% 64.91/64.97 (P3(f8(x30261),x30261,f7(f11(x30262,a6),f11(x30263,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,2982,3011,1435,3014,1530,88,1258,1392,1627,808,23,28,22,29,33,21])).
% 64.91/64.97 cnf(3029,plain,
% 64.91/64.97 (P2(f7(a6,a6),f7(f11(x30291,a6),f11(x30292,a6)))),
% 64.91/64.97 inference(scs_inference,[],[826,2982,3011,1435,3014,3018,1530,88,1258,1392,1627,808,23,28,22,29,33,21,27])).
% 64.91/64.97 cnf(3049,plain,
% 64.91/64.97 (P3(f8(x30491),x30491,f7(f11(x30492,a6),f11(x30493,a6)))),
% 64.91/64.97 inference(rename_variables,[],[3026])).
% 64.91/64.97 cnf(3052,plain,
% 64.91/64.97 (P3(f8(x30521),x30521,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(3056,plain,
% 64.91/64.97 (P3(f8(x30561),x30561,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(3057,plain,
% 64.91/64.97 (P3(f8(x30571),x30571,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3061,plain,
% 64.91/64.97 (P3(f8(x30611),x30611,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(3063,plain,
% 64.91/64.97 (~P1(a1,f8(a2),f8(a3))+P1(a1,a6,f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[1,795,447,10,3052,3056,3061,487,1392,3057,1395,3026,3049,3029,26,23,24,27,22,29,35,36])).
% 64.91/64.97 cnf(3145,plain,
% 64.91/64.97 (P3(f8(x31451),x31451,f11(x31452,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(3147,plain,
% 64.91/64.97 (P3(f11(x31471,a6),f11(x31472,a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[829,3145,1424,1392,808,11,23,30,29])).
% 64.91/64.97 cnf(3274,plain,
% 64.91/64.97 (P3(f8(x32741),x32741,f11(a6,x32742))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(3276,plain,
% 64.91/64.97 (P3(f11(a6,x32761),f11(x32762,a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[1453,1672,3274,1392,2237,808,23,22,29])).
% 64.91/64.97 cnf(3473,plain,
% 64.91/64.97 (P3(a6,a3,f11(a1,a2))),
% 64.91/64.97 inference(scs_inference,[],[6,2040,21])).
% 64.91/64.97 cnf(3500,plain,
% 64.91/64.97 (P3(f8(a3),f11(a1,a2),f11(a6,x35001))),
% 64.91/64.97 inference(scs_inference,[],[1672,2040,22])).
% 64.91/64.97 cnf(3576,plain,
% 64.91/64.97 (P2(a4,f11(a1,a9))),
% 64.91/64.97 inference(scs_inference,[],[2,12,28])).
% 64.91/64.97 cnf(3577,plain,
% 64.91/64.97 (P1(x35771,x35772,f11(x35771,x35772))),
% 64.91/64.97 inference(rename_variables,[],[12])).
% 64.91/64.97 cnf(3579,plain,
% 64.91/64.97 (P3(f8(a4),f11(a1,a9),f11(a6,x35791))),
% 64.91/64.97 inference(scs_inference,[],[2,1672,12,28,22])).
% 64.91/64.97 cnf(3580,plain,
% 64.91/64.97 (P3(f8(x35801),x35801,f11(a6,x35802))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(3586,plain,
% 64.91/64.97 (P3(f8(x35861),x35861,f11(a6,x35862))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(3598,plain,
% 64.91/64.97 (P1(x35981,x35982,f11(x35981,x35982))),
% 64.91/64.97 inference(rename_variables,[],[12])).
% 64.91/64.97 cnf(3599,plain,
% 64.91/64.97 (P3(x35991,x35992,f7(x35991,x35992))),
% 64.91/64.97 inference(rename_variables,[],[11])).
% 64.91/64.97 cnf(3605,plain,
% 64.91/64.97 (P3(a6,a4,f11(a1,a9))),
% 64.91/64.97 inference(scs_inference,[],[2,826,56,1336,79,1672,3580,201,6,5,12,3577,3598,11,3599,28,22,23,30,31,32,34,33,21])).
% 64.91/64.97 cnf(3608,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,f11(a6,x36081),f11(x36082,a6))),
% 64.91/64.97 inference(scs_inference,[],[2,826,56,1336,79,1672,3580,3586,829,201,6,5,12,3577,3598,11,3599,28,22,23,30,31,32,34,33,21,36])).
% 64.91/64.97 cnf(3610,plain,
% 64.91/64.97 (P3(f8(x36101),x36101,f11(a6,x36102))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(3612,plain,
% 64.91/64.97 (~P1(f8(a1),a9,f8(a4))+P1(f11(a6,x36121),a9,f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[2,826,56,1336,79,1672,3580,3586,3610,829,1435,201,6,5,12,3577,3598,11,3599,28,22,23,30,31,32,34,33,21,36,35])).
% 64.91/64.97 cnf(3620,plain,
% 64.91/64.97 (P1(x36201,a6,f11(x36201,f11(x36202,a6)))),
% 64.91/64.97 inference(rename_variables,[],[79])).
% 64.91/64.97 cnf(3627,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,f11(a6,x36271),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[2,56,79,3620,1672,1435,1389,3,1544,30,31,32,36])).
% 64.91/64.97 cnf(3663,plain,
% 64.91/64.97 (P3(f8(a4),f11(a1,a9),f11(x36631,a6))),
% 64.91/64.97 inference(scs_inference,[],[1207,829,808,3576,23,22])).
% 64.91/64.97 cnf(3664,plain,
% 64.91/64.97 (P3(f8(x36641),x36641,f11(x36642,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(3666,plain,
% 64.91/64.97 (P3(f11(a6,x36661),f11(x36662,a6),f11(a6,x36661))),
% 64.91/64.97 inference(scs_inference,[],[1207,829,808,1998,3576,23,22,29])).
% 64.91/64.97 cnf(3671,plain,
% 64.91/64.97 (P3(f8(x36711),x36711,f11(x36712,a6))),
% 64.91/64.97 inference(rename_variables,[],[829])).
% 64.91/64.97 cnf(3678,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,f11(x36781,a6),a6)),
% 64.91/64.97 inference(scs_inference,[],[2,1207,829,3664,3671,10,808,1998,73,11,3,3576,3605,23,22,29,30,31,36])).
% 64.91/64.97 cnf(3685,plain,
% 64.91/64.97 (P2(f8(a6),f11(a6,x36851))),
% 64.91/64.97 inference(scs_inference,[],[1392,1672,27])).
% 64.91/64.97 cnf(3713,plain,
% 64.91/64.97 (P2(f8(a6),f11(x37131,f11(x37132,a6)))),
% 64.91/64.97 inference(scs_inference,[],[1392,1561,27])).
% 64.91/64.97 cnf(3714,plain,
% 64.91/64.97 (P3(f8(x37141),x37141,f11(x37142,f11(x37143,a6)))),
% 64.91/64.97 inference(rename_variables,[],[1561])).
% 64.91/64.97 cnf(3720,plain,
% 64.91/64.97 (P3(f8(x37201),x37201,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3724,plain,
% 64.91/64.97 (P3(f8(x37241),x37241,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3728,plain,
% 64.91/64.97 (P3(f8(x37281),x37281,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3734,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,f8(a6),f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[2,235,1392,3720,3724,3728,1435,839,1561,3714,808,53,1760,3,27,23,22,29,30,31,36])).
% 64.91/64.97 cnf(3763,plain,
% 64.91/64.97 (P3(f8(x37631),x37631,f7(f8(a6),f11(x37632,a6)))),
% 64.91/64.97 inference(rename_variables,[],[1596])).
% 64.91/64.97 cnf(3766,plain,
% 64.91/64.97 (P3(f8(x37661),x37661,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3769,plain,
% 64.91/64.97 (P3(f8(x37691),x37691,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3773,plain,
% 64.91/64.97 (P3(f8(x37731),x37731,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3776,plain,
% 64.91/64.97 (P3(f8(a6),f11(a6,x37761),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[1392,3766,3769,3773,2020,1596,3763,384,53,1766,3713,27,23,22,29,30])).
% 64.91/64.97 cnf(3777,plain,
% 64.91/64.97 (P3(f8(x37771),x37771,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3780,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,f8(a6),a6)),
% 64.91/64.97 inference(scs_inference,[],[2,1392,3766,3769,3773,3777,10,2020,1596,3763,384,53,1766,3713,27,23,22,29,30,36])).
% 64.91/64.97 cnf(3789,plain,
% 64.91/64.97 (P3(f8(x37891),x37891,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(3792,plain,
% 64.91/64.97 (P3(f8(x37921),x37921,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(3795,plain,
% 64.91/64.97 (P3(f8(x37951),x37951,f7(a6,a6))),
% 64.91/64.97 inference(rename_variables,[],[1435])).
% 64.91/64.97 cnf(3798,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,f7(a6,a6),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[2,379,1435,3789,3792,3795,1392,11,3713,3605,23,22,30,36])).
% 64.91/64.97 cnf(3807,plain,
% 64.91/64.97 (P3(f8(x38071),x38071,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(3809,plain,
% 64.91/64.97 (P3(f8(a4),f11(a1,a9),a6)),
% 64.91/64.97 inference(scs_inference,[],[10,3807,3576,3713,23,22])).
% 64.91/64.97 cnf(3810,plain,
% 64.91/64.97 (P3(f8(x38101),x38101,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(3813,plain,
% 64.91/64.97 (P3(f8(x38131),x38131,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(3816,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,a6,f7(a6,a6))),
% 64.91/64.97 inference(scs_inference,[],[2,10,3807,3810,3813,1435,6,3576,3713,3579,23,22,30,36])).
% 64.91/64.97 cnf(3824,plain,
% 64.91/64.97 (P3(f11(a6,x38241),a6,f11(a6,x38242))),
% 64.91/64.97 inference(scs_inference,[],[1672,3685,23])).
% 64.91/64.97 cnf(3825,plain,
% 64.91/64.97 (P3(f8(x38251),x38251,f11(a6,x38252))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(3828,plain,
% 64.91/64.97 (P3(f8(x38281),x38281,f11(a6,x38282))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(3831,plain,
% 64.91/64.97 (P3(f8(x38311),x38311,f11(a6,x38312))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(3834,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,f11(a6,x38341),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[2,1672,3825,3828,3831,1392,11,3685,3605,23,22,30,36])).
% 64.91/64.97 cnf(3866,plain,
% 64.91/64.97 (P3(f8(x38661),x38661,f11(a6,x38662))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(3869,plain,
% 64.91/64.97 (P3(f8(x38691),x38691,f11(a6,x38692))),
% 64.91/64.97 inference(rename_variables,[],[1672])).
% 64.91/64.97 cnf(3871,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,f11(a6,x38711),a6)),
% 64.91/64.97 inference(scs_inference,[],[2,1672,3866,3869,10,3713,3824,23,30,36])).
% 64.91/64.97 cnf(3879,plain,
% 64.91/64.97 (P2(f8(a6),f7(f8(x38791),x38791))),
% 64.91/64.97 inference(scs_inference,[],[1392,1611,27])).
% 64.91/64.97 cnf(3904,plain,
% 64.91/64.97 (P2(f8(a6),f11(f7(a6,a6),x39041))),
% 64.91/64.97 inference(scs_inference,[],[1392,1650,27])).
% 64.91/64.97 cnf(3908,plain,
% 64.91/64.97 (P3(f8(x39081),x39081,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3911,plain,
% 64.91/64.97 (P3(f8(x39111),x39111,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3913,plain,
% 64.91/64.97 (P3(f8(a3),f11(a1,a2),f8(a6))),
% 64.91/64.97 inference(scs_inference,[],[1392,3908,3911,1650,2605,53,2062,3879,27,23,22,30])).
% 64.91/64.97 cnf(3914,plain,
% 64.91/64.97 (P3(f8(x39141),x39141,f8(a6))),
% 64.91/64.97 inference(rename_variables,[],[1392])).
% 64.91/64.97 cnf(3917,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,f8(a6),f11(a6,x39171))),
% 64.91/64.97 inference(scs_inference,[],[2,1392,3908,3911,3914,1672,1650,2605,53,2062,3879,27,23,22,30,36])).
% 64.91/64.97 cnf(4005,plain,
% 64.91/64.97 (P1(f8(a6),x40051,f11(a6,x40052))),
% 64.91/64.97 inference(scs_inference,[],[698,3685,24])).
% 64.91/64.97 cnf(4187,plain,
% 64.91/64.97 (~P1(a1,f8(a9),f8(a4))+P1(a1,f11(x41871,a6),f11(a6,x41872))),
% 64.91/64.97 inference(scs_inference,[],[2,829,1672,36])).
% 64.91/64.97 cnf(4195,plain,
% 64.91/64.97 (P3(f8(x41951),x41951,a6)),
% 64.91/64.97 inference(rename_variables,[],[10])).
% 64.91/64.97 cnf(4197,plain,
% 64.91/64.97 (P3(f8(a6),f11(a1,a9),f11(a1,a9))),
% 64.91/64.97 inference(scs_inference,[],[10,4195,3879,3605,23,30])).
% 64.91/64.97 cnf(4226,plain,
% 64.91/64.98 (~P1(a1,f8(a9),f8(a4))+P1(a1,f11(x42261,a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[2,829,1392,36])).
% 64.91/64.98 cnf(4249,plain,
% 64.91/64.98 (P3(a4,a6,f11(a1,a9))),
% 64.91/64.98 inference(scs_inference,[],[5,3576,21])).
% 64.91/64.98 cnf(4252,plain,
% 64.91/64.98 (P2(f8(a6),f7(a6,f7(a6,a6)))),
% 64.91/64.98 inference(scs_inference,[],[1392,5,1496,3576,21,27])).
% 64.91/64.98 cnf(4274,plain,
% 64.91/64.98 (P3(f11(a1,a2),f11(x42741,a6),f11(a1,a2))),
% 64.91/64.98 inference(scs_inference,[],[808,3010,2323,23,29])).
% 64.91/64.98 cnf(4280,plain,
% 64.91/64.98 (P3(f8(x42801),x42801,f11(a6,x42802))),
% 64.91/64.98 inference(rename_variables,[],[1672])).
% 64.91/64.98 cnf(4282,plain,
% 64.91/64.98 (~P1(f8(a1),a9,f8(a4))+P1(f11(a6,x42821),a9,f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[2,1672,4280,1392,1530,808,3010,2323,23,29,36,35])).
% 64.91/64.98 cnf(4288,plain,
% 64.91/64.98 (P3(f8(x42881),x42881,a6)),
% 64.91/64.98 inference(rename_variables,[],[10])).
% 64.91/64.98 cnf(4291,plain,
% 64.91/64.98 (P3(f8(x42911),x42911,a6)),
% 64.91/64.98 inference(rename_variables,[],[10])).
% 64.91/64.98 cnf(4294,plain,
% 64.91/64.98 (~P1(a1,f8(a9),f8(a4))+P1(a1,a6,f11(a6,x42941))),
% 64.91/64.98 inference(scs_inference,[],[2,10,4288,4291,1672,6,3913,4252,23,30,36])).
% 64.91/64.98 cnf(4322,plain,
% 64.91/64.98 (P3(f8(x43221),x43221,a6)),
% 64.91/64.98 inference(rename_variables,[],[10])).
% 64.91/64.98 cnf(4325,plain,
% 64.91/64.98 (~P1(a1,f8(a9),f8(a4))+P1(a1,a6,f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[2,10,4322,1392,6,4197,30,36])).
% 64.91/64.98 cnf(4335,plain,
% 64.91/64.98 (~P1(a1,f8(a9),f8(a4))+P1(a1,a6,f11(x43351,a6))),
% 64.91/64.98 inference(scs_inference,[],[2,10,829,36])).
% 64.91/64.98 cnf(4347,plain,
% 64.91/64.98 (P3(f8(x43471),x43471,f7(a6,a6))),
% 64.91/64.98 inference(rename_variables,[],[1435])).
% 64.91/64.98 cnf(4350,plain,
% 64.91/64.98 (P3(f8(x43501),x43501,f7(a6,a6))),
% 64.91/64.98 inference(rename_variables,[],[1435])).
% 64.91/64.98 cnf(4354,plain,
% 64.91/64.98 (P3(f8(x43541),x43541,f7(a6,a6))),
% 64.91/64.98 inference(rename_variables,[],[1435])).
% 64.91/64.98 cnf(4356,plain,
% 64.91/64.98 (~P1(a1,f8(a9),f8(a4))+P1(a1,f7(a6,a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[2,2237,1435,4347,4350,4354,91,10,11,3904,22,23,29,36])).
% 64.91/64.98 cnf(4393,plain,
% 64.91/64.98 (P3(f8(a3),f11(a1,a2),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[1435,2040,22])).
% 64.91/64.98 cnf(4397,plain,
% 64.91/64.98 (P3(f8(a4),f11(a1,a9),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[1435,3576,22])).
% 64.91/64.98 cnf(4402,plain,
% 64.91/64.98 (P3(f11(a1,a2),f8(a3),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4393,17])).
% 64.91/64.98 cnf(4404,plain,
% 64.91/64.98 (P1(f8(x44041),f8(a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[4393,3,17,20])).
% 64.91/64.98 cnf(4406,plain,
% 64.91/64.98 (P1(f8(x44061),a6,f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4393,3,17,20,19])).
% 64.91/64.98 cnf(4408,plain,
% 64.91/64.98 (P1(f11(a6,x44081),f8(x44082),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4393,2415,3,17,20,19,18])).
% 64.91/64.98 cnf(4410,plain,
% 64.91/64.98 (~P2(f11(a1,a10),a5)),
% 64.91/64.98 inference(scs_inference,[],[13,4393,2415,3,12,17,20,19,18,24])).
% 64.91/64.98 cnf(4414,plain,
% 64.91/64.98 (P3(x44141,a6,x44141)),
% 64.91/64.98 inference(rename_variables,[],[5])).
% 64.91/64.98 cnf(4416,plain,
% 64.91/64.98 (~P2(a5,f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[13,4393,2415,3,12,5,4414,17,20,19,18,24,27,23])).
% 64.91/64.98 cnf(4417,plain,
% 64.91/64.98 (P3(x44171,a6,x44171)),
% 64.91/64.98 inference(rename_variables,[],[5])).
% 64.91/64.98 cnf(4419,plain,
% 64.91/64.98 (P3(f7(a6,a6),f11(a6,x44191),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4393,3776,2639,2415,3,12,5,4414,17,20,19,18,24,27,23,29])).
% 64.91/64.98 cnf(4421,plain,
% 64.91/64.98 (~P3(f11(a1,a10),f11(a6,x44211),a5)),
% 64.91/64.98 inference(scs_inference,[],[13,4393,3776,2639,2001,2415,3,12,5,4414,4417,17,20,19,18,24,27,23,29,30])).
% 64.91/64.98 cnf(4424,plain,
% 64.91/64.98 (P1(f11(a6,x44241),f11(a6,a6),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4393,3776,2639,2086,4005,2001,2415,1228,3,12,5,4414,4417,17,20,19,18,24,27,23,29,30,31])).
% 64.91/64.98 cnf(4425,plain,
% 64.91/64.98 (P1(f8(a6),x44251,f11(a6,x44252))),
% 64.91/64.98 inference(rename_variables,[],[4005])).
% 64.91/64.98 cnf(4426,plain,
% 64.91/64.98 (P1(f8(a6),x44261,f7(a6,a6))),
% 64.91/64.98 inference(rename_variables,[],[1228])).
% 64.91/64.98 cnf(4428,plain,
% 64.91/64.98 (P1(f11(a6,x44281),f11(x44282,a6),f11(a6,x44283))),
% 64.91/64.98 inference(scs_inference,[],[13,4393,3776,2639,2086,4005,2001,2415,1228,1386,3,12,5,4414,4417,17,20,19,18,24,27,23,29,30,31,32])).
% 64.91/64.98 cnf(4429,plain,
% 64.91/64.98 (P1(f11(a6,x44291),x44292,a6)),
% 64.91/64.98 inference(rename_variables,[],[2415])).
% 64.91/64.98 cnf(4432,plain,
% 64.91/64.98 (P1(a1,f8(a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4393,3776,3276,2639,2086,4005,2001,2415,1228,1386,3,12,5,4414,4417,17,20,19,18,24,27,23,29,30,31,32,36])).
% 64.91/64.98 cnf(4435,plain,
% 64.91/64.98 (P1(a1,f11(a6,a6),f11(x44351,a6))),
% 64.91/64.98 inference(rename_variables,[],[2086])).
% 64.91/64.98 cnf(4437,plain,
% 64.91/64.98 (P1(f11(a1,a2),f11(x44371,a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4393,4274,3776,3276,2639,2460,2086,4005,2001,2415,4429,1228,1386,1058,3,12,5,4414,4417,17,20,19,18,24,27,23,29,30,31,32,36,35])).
% 64.91/64.98 cnf(4440,plain,
% 64.91/64.98 (P1(x44401,f11(x44402,a6),f11(a6,a6))),
% 64.91/64.98 inference(rename_variables,[],[1058])).
% 64.91/64.98 cnf(4443,plain,
% 64.91/64.98 (P3(f11(a6,x44431),f7(a6,a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[13,4393,4274,3776,3276,2639,2460,2086,4005,4425,2001,2415,4429,1228,4426,1386,1058,1194,3,12,5,4414,4417,17,20,19,18,24,27,23,29,30,31,32,36,35,33])).
% 64.91/64.98 cnf(4445,plain,
% 64.91/64.98 (P1(f8(a6),x44451,f11(a6,x44452))),
% 64.91/64.98 inference(rename_variables,[],[4005])).
% 64.91/64.98 cnf(4448,plain,
% 64.91/64.98 (P3(f11(x44481,a6),f11(a6,x44482),f11(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4393,4274,3776,3276,2639,2460,2086,4435,4005,4425,4445,2001,2415,4429,1228,4426,1386,1058,4440,1194,3,12,5,4414,4417,11,17,20,19,18,24,27,23,29,30,31,32,36,35,33,34])).
% 64.91/64.98 cnf(4453,plain,
% 64.91/64.98 (P3(f11(a1,a9),f8(a4),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4397,17])).
% 64.91/64.98 cnf(4455,plain,
% 64.91/64.98 (P1(f8(x44551),f8(x44552),f11(x44551,x44552))),
% 64.91/64.98 inference(scs_inference,[],[4397,12,17,20])).
% 64.91/64.98 cnf(4457,plain,
% 64.91/64.98 (P1(f8(a1),a9,f8(a4))),
% 64.91/64.98 inference(scs_inference,[],[4397,12,2,17,20,19])).
% 64.91/64.98 cnf(4459,plain,
% 64.91/64.98 (P1(x44591,f8(a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4397,3,12,2,17,20,19,18])).
% 64.91/64.98 cnf(4461,plain,
% 64.91/64.98 (~P3(a5,a6,f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[4397,4416,3,12,5,2,17,20,19,18,27])).
% 64.91/64.98 cnf(4464,plain,
% 64.91/64.98 (P3(a6,f11(a1,a9),a4)),
% 64.91/64.98 inference(scs_inference,[],[4397,4416,3,9,12,5,53,2,17,20,19,18,27,29])).
% 64.91/64.98 cnf(4468,plain,
% 64.91/64.98 (P3(a3,f8(a3),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4397,4402,4416,2844,3,9,12,5,53,6,2,17,20,19,18,27,29,30])).
% 64.91/64.98 cnf(4471,plain,
% 64.91/64.98 (P1(f11(a6,x44711),f8(a6),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4397,4402,4432,4416,2844,1386,1236,3,9,12,5,53,6,2,17,20,19,18,27,29,30,31])).
% 64.91/64.98 cnf(4475,plain,
% 64.91/64.98 (P1(f11(a6,x44751),f7(a6,a6),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4397,4402,4432,4424,4428,4416,2844,1386,1236,3,9,12,5,53,6,2,17,20,19,18,27,29,30,31,32])).
% 64.91/64.98 cnf(4476,plain,
% 64.91/64.98 (P1(f11(a6,x44761),f11(a6,a6),f7(a6,a6))),
% 64.91/64.98 inference(rename_variables,[],[4424])).
% 64.91/64.98 cnf(4479,plain,
% 64.91/64.98 (P1(f11(a1,a2),f11(a6,a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[4397,4402,4432,4424,4448,4428,4437,4416,1140,2844,1386,1236,3,9,12,5,53,6,2,17,20,19,18,27,29,30,31,32,36])).
% 64.91/64.98 cnf(4483,plain,
% 64.91/64.98 (P1(f7(a1,a1),f8(a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[4397,4402,4432,4424,4448,4428,4437,4416,1140,2844,1386,1236,3,9,12,5,53,6,11,2,17,20,19,18,27,29,30,31,32,36,35])).
% 64.91/64.98 cnf(4486,plain,
% 64.91/64.98 (P3(a6,f11(a6,x44861),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4397,4402,4432,4424,4448,4428,4437,4404,4416,2810,1140,2844,4005,1228,1386,1236,3,9,12,5,53,6,11,2,17,20,19,18,27,29,30,31,32,36,35,33])).
% 64.91/64.98 cnf(4488,plain,
% 64.91/64.98 (P1(f8(a6),x44881,f11(a6,x44882))),
% 64.91/64.98 inference(rename_variables,[],[4005])).
% 64.91/64.98 cnf(4491,plain,
% 64.91/64.98 (P3(f11(a6,x44911),f7(a6,a6),f11(a6,x44912))),
% 64.91/64.98 inference(scs_inference,[],[4397,4402,4432,4424,4476,4448,4428,4437,4404,4416,2810,1140,2844,4005,4488,2159,1228,1386,1236,3,9,12,5,53,6,11,2,17,20,19,18,27,29,30,31,32,36,35,33,34])).
% 64.91/64.98 cnf(4496,plain,
% 64.91/64.98 (P1(f11(a6,x44961),a9,f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4397,4402,4432,4424,4476,4448,4428,4437,4404,4416,2810,1140,2844,4005,4488,2159,1228,1386,1236,3,9,12,5,53,6,11,2,17,20,19,18,27,29,30,31,32,36,35,33,34,4282])).
% 64.91/64.98 cnf(4497,plain,
% 64.91/64.98 (P1(f11(a6,x44971),a9,f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4397,4402,4432,4424,4476,4448,4428,4437,4404,4416,2810,1140,2844,4005,4488,2159,1228,1386,1236,3,9,12,5,53,6,11,2,17,20,19,18,27,29,30,31,32,36,35,33,34,4282,3612])).
% 64.91/64.98 cnf(4498,plain,
% 64.91/64.98 (~P1(f8(a1),f8(a10),a5)),
% 64.91/64.98 inference(scs_inference,[],[4397,4402,4432,4424,4476,4448,4410,4428,4437,4404,4416,2810,1140,2844,4005,4488,2159,1228,1386,1236,3,9,12,5,53,6,11,2,17,20,19,18,27,29,30,31,32,36,35,33,34,4282,3612,28])).
% 64.91/64.98 cnf(4501,plain,
% 64.91/64.98 (P3(f11(a6,x45011),f7(a6,a6),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4419,17])).
% 64.91/64.98 cnf(4503,plain,
% 64.91/64.98 (P1(f8(x45031),f8(a6),f11(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4419,56,17,20])).
% 64.91/64.98 cnf(4505,plain,
% 64.91/64.98 (P1(f8(a1),a2,f8(a3))),
% 64.91/64.98 inference(scs_inference,[],[4419,56,1,17,20,19])).
% 64.91/64.98 cnf(4507,plain,
% 64.91/64.98 (P1(a1,f8(a9),f8(a4))),
% 64.91/64.98 inference(scs_inference,[],[4419,56,2,1,17,20,19,18])).
% 64.91/64.98 cnf(4512,plain,
% 64.91/64.98 (~P3(a5,f11(a6,x45121),f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[4461,4419,4410,1284,5,53,56,2,1,17,20,19,18,27,29])).
% 64.91/64.98 cnf(4513,plain,
% 64.91/64.98 (P3(x45131,a6,x45131)),
% 64.91/64.98 inference(rename_variables,[],[5])).
% 64.91/64.98 cnf(4516,plain,
% 64.91/64.98 (P3(a6,x45161,x45161)),
% 64.91/64.98 inference(rename_variables,[],[6])).
% 64.91/64.98 cnf(4523,plain,
% 64.91/64.98 (~P3(f11(a6,x45231),f11(a1,a10),a5)),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35])).
% 64.91/64.98 cnf(4528,plain,
% 64.91/64.98 (P1(a1,f11(x45281,a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678])).
% 64.91/64.98 cnf(4529,plain,
% 64.91/64.98 (P1(a1,f11(a6,x45291),a6)),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678,3871])).
% 64.91/64.98 cnf(4530,plain,
% 64.91/64.98 (P1(a1,a6,f11(a6,x45301))),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678,3871,4294])).
% 64.91/64.98 cnf(4531,plain,
% 64.91/64.98 (P1(a1,a6,f11(x45311,a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678,3871,4294,4335])).
% 64.91/64.98 cnf(4532,plain,
% 64.91/64.98 (P1(f11(a6,x45321),a2,f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678,3871,4294,4335,2226])).
% 64.91/64.98 cnf(4533,plain,
% 64.91/64.98 (P1(a1,f11(a6,x45331),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678,3871,4294,4335,2226,3834])).
% 64.91/64.98 cnf(4534,plain,
% 64.91/64.98 (P1(a1,f8(a6),f11(a6,x45341))),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678,3871,4294,4335,2226,3834,3917])).
% 64.91/64.98 cnf(4536,plain,
% 64.91/64.98 (P1(a1,f11(a6,x45361),f11(x45362,a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678,3871,4294,4335,2226,3834,3917,4226,3608])).
% 64.91/64.98 cnf(4538,plain,
% 64.91/64.98 (P1(a1,f11(x45381,a6),f11(a6,x45382))),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678,3871,4294,4335,2226,3834,3917,4226,3608,3734,4187])).
% 64.91/64.98 cnf(4539,plain,
% 64.91/64.98 (P1(f11(a6,x45391),a2,f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678,3871,4294,4335,2226,3834,3917,4226,3608,3734,4187,2310])).
% 64.91/64.98 cnf(4540,plain,
% 64.91/64.98 (P1(a1,f11(a6,x45401),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[13,4455,4453,4498,4461,4419,4406,4249,4410,1284,1386,12,5,4513,53,6,4516,56,2,1,17,20,19,18,27,29,30,36,35,3678,3871,4294,4335,2226,3834,3917,4226,3608,3734,4187,2310,3627])).
% 64.91/64.98 cnf(4569,plain,
% 64.91/64.98 (P1(a1,f8(a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[4507,3780])).
% 64.91/64.98 cnf(4570,plain,
% 64.91/64.98 (P1(a1,f7(a6,a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4507,3798])).
% 64.91/64.98 cnf(4571,plain,
% 64.91/64.98 (P1(a1,a6,f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4507,3816])).
% 64.91/64.98 cnf(4578,plain,
% 64.91/64.98 (P1(a1,a6,f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4507,4325])).
% 64.91/64.98 cnf(4579,plain,
% 64.91/64.98 (P1(a1,f7(a6,a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[4507,4356])).
% 64.91/64.98 cnf(4581,plain,
% 64.91/64.98 (P3(f7(a6,a6),f11(a6,x45811),f11(a6,x45812))),
% 64.91/64.98 inference(scs_inference,[],[4491,17])).
% 64.91/64.98 cnf(4583,plain,
% 64.91/64.98 (P1(f8(a1),f8(a6),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4571,4491,17,20])).
% 64.91/64.98 cnf(4585,plain,
% 64.91/64.98 (P1(f8(a1),f7(a6,a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4571,4579,4491,17,20,19])).
% 64.91/64.98 cnf(4587,plain,
% 64.91/64.98 (P1(a1,f8(a2),f8(a3))),
% 64.91/64.98 inference(scs_inference,[],[4571,4579,4491,1,17,20,19,18])).
% 64.91/64.98 cnf(4589,plain,
% 64.91/64.98 (P3(f7(a6,a6),f11(a1,a2),f11(a1,a2))),
% 64.91/64.98 inference(scs_inference,[],[4571,4579,4468,4491,2390,2844,1,17,20,19,18,29])).
% 64.91/64.98 cnf(4591,plain,
% 64.91/64.98 (~P3(a5,f11(x45911,a6),f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[4571,4579,4512,4468,4491,2390,1746,2844,5,1,17,20,19,18,29,30])).
% 64.91/64.98 cnf(4595,plain,
% 64.91/64.98 (P1(f8(x45951),f11(a6,x45952),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4571,4579,4503,4539,4512,4468,4491,2390,1746,2844,4005,5,1,17,20,19,18,29,30,32])).
% 64.91/64.98 cnf(4599,plain,
% 64.91/64.98 (P3(f7(a6,a6),f8(a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[4569,4570,4571,4579,4503,4539,4512,4468,4491,2390,855,1746,2844,4005,5,1,17,20,19,18,29,30,32,33])).
% 64.91/64.98 cnf(4602,plain,
% 64.91/64.98 (P1(a1,f7(a6,a6),f11(x46021,a6))),
% 64.91/64.98 inference(scs_inference,[],[4569,4570,4571,4579,4503,4539,4512,4468,4491,2390,855,1746,2844,4005,5,1,17,20,19,18,29,30,32,33,2789,2818])).
% 64.91/64.98 cnf(4603,plain,
% 64.91/64.98 (P1(f8(a4),f8(a6),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4569,4570,4571,4579,4507,4503,4539,4540,4512,4468,4491,2390,855,1746,2844,4005,5,1,17,20,19,18,29,30,32,33,2789,2818,31])).
% 64.91/64.98 cnf(4633,plain,
% 64.91/64.98 (P1(a1,f7(a6,a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[4587,2769])).
% 64.91/64.98 cnf(4636,plain,
% 64.91/64.98 (P1(a1,f7(a6,a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4587,2889])).
% 64.91/64.98 cnf(4641,plain,
% 64.91/64.98 (P1(a1,a6,f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4587,3063])).
% 64.91/64.98 cnf(4667,plain,
% 64.91/64.98 (P3(f7(a6,a6),f11(a6,x46671),a6)),
% 64.91/64.98 inference(scs_inference,[],[4443,17])).
% 64.91/64.98 cnf(4669,plain,
% 64.91/64.98 (P1(f8(a1),f8(a6),f11(a6,x46691))),
% 64.91/64.98 inference(scs_inference,[],[4530,4443,17,20])).
% 64.91/64.98 cnf(4671,plain,
% 64.91/64.98 (P1(f8(a1),f11(x46711,a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4528,4530,4443,17,20,19])).
% 64.91/64.98 cnf(4674,plain,
% 64.91/64.98 (P3(x46741,f7(a6,a6),x46741)),
% 64.91/64.98 inference(rename_variables,[],[53])).
% 64.91/64.98 cnf(4676,plain,
% 64.91/64.98 (~P3(a5,f8(a6),f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[4591,4528,4530,4443,3016,4416,53,4674,17,20,19,27,29])).
% 64.91/64.98 cnf(4680,plain,
% 64.91/64.98 (P3(f11(a6,x46801),f11(a1,a2),f11(a1,a2))),
% 64.91/64.98 inference(scs_inference,[],[4589,4591,4501,4528,4530,4443,3016,4416,53,4674,17,20,19,27,29,30])).
% 64.91/64.98 cnf(4686,plain,
% 64.91/64.98 (P1(f8(a1),a6,f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4589,4583,4585,4599,4595,4591,4501,4528,4530,4479,4443,3016,967,4455,4416,53,4674,17,20,19,27,29,30,32,36])).
% 64.91/64.98 cnf(4712,plain,
% 64.91/64.98 (P3(f11(a1,a2),f11(a6,x47121),f11(a1,a2))),
% 64.91/64.98 inference(scs_inference,[],[4680,17])).
% 64.91/64.98 cnf(4714,plain,
% 64.91/64.98 (P1(f8(a1),f8(a6),f11(x47141,a6))),
% 64.91/64.98 inference(scs_inference,[],[4680,4531,17,20])).
% 64.91/64.98 cnf(4718,plain,
% 64.91/64.98 (P3(f7(a6,a6),f11(a1,a9),a4)),
% 64.91/64.98 inference(scs_inference,[],[4680,4529,4531,4464,4599,4197,17,20,19,30])).
% 64.91/64.98 cnf(4720,plain,
% 64.91/64.98 (P1(f8(a4),f11(a6,x47201),a6)),
% 64.91/64.98 inference(scs_inference,[],[4680,4603,4529,4531,4464,2290,4599,2253,4197,17,20,19,30,36])).
% 64.91/64.98 cnf(4722,plain,
% 64.91/64.98 (P1(f11(a1,a2),f11(a6,a6),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4680,4603,4529,4531,4464,1142,2290,4599,4424,4437,2253,4197,17,20,19,30,36,35])).
% 64.91/64.98 cnf(4726,plain,
% 64.91/64.98 (P3(f11(a6,x47261),f11(a6,x47261),f11(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4680,4603,4538,4529,4531,4464,1142,2290,4599,4424,4437,2253,4197,1058,11,17,20,19,30,36,35,34])).
% 64.91/64.98 cnf(4752,plain,
% 64.91/64.98 (P3(f11(a1,a9),f7(a6,a6),a4)),
% 64.91/64.98 inference(scs_inference,[],[4718,17])).
% 64.91/64.98 cnf(4754,plain,
% 64.91/64.98 (P1(f8(a1),f8(a9),a4)),
% 64.91/64.98 inference(scs_inference,[],[4718,2,17,20])).
% 64.91/64.98 cnf(4759,plain,
% 64.91/64.98 (P3(a4,f8(a4),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4718,1316,4410,4453,6,2,17,20,27,29])).
% 64.91/64.98 cnf(4765,plain,
% 64.91/64.98 (P1(f8(a3),f11(a6,x47651),a6)),
% 64.91/64.98 inference(scs_inference,[],[4718,4633,4587,4421,4595,1316,1746,4410,4453,5,6,2,17,20,27,29,30,31])).
% 64.91/64.98 cnf(4768,plain,
% 64.91/64.98 (P1(f11(a1,a2),f7(a6,a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4722,4718,4633,4587,4421,4471,4595,4459,1316,1746,4410,4453,5,6,2,17,20,27,29,30,31,32])).
% 64.91/64.98 cnf(4772,plain,
% 64.91/64.98 (P1(f8(a4),f11(a6,a6),f11(a6,x47721))),
% 64.91/64.98 inference(scs_inference,[],[4722,4718,4726,4720,4633,4587,4421,4471,4595,4459,1316,1746,4410,4453,1284,5,6,2,17,20,27,29,30,31,32,36])).
% 64.91/64.98 cnf(4775,plain,
% 64.91/64.98 (P1(f7(a1,a1),a6,f11(a6,x47751))),
% 64.91/64.98 inference(scs_inference,[],[4722,4718,4726,4720,4641,4633,4587,4421,4471,4595,4459,1316,2290,1746,4410,4453,1284,5,6,11,2,17,20,27,29,30,31,32,36,35])).
% 64.91/64.98 cnf(4778,plain,
% 64.91/64.98 (P3(f7(a6,a6),f8(a6),f11(a6,x47781))),
% 64.91/64.98 inference(scs_inference,[],[4722,4718,4726,4720,4641,4633,4587,4421,4532,4471,2631,4595,4459,1316,2290,1746,4410,4453,1284,2159,1228,5,6,11,2,17,20,27,29,30,31,32,36,35,34])).
% 64.91/64.98 cnf(4784,plain,
% 64.91/64.98 (P3(f11(a6,x47841),f11(a6,x47842),f11(a6,x47841))),
% 64.91/64.98 inference(scs_inference,[],[4722,4718,4712,4726,4720,4641,4633,4587,4421,4532,4471,2631,4595,4428,4459,1316,2290,1746,4410,4453,1284,2139,2159,1228,5,6,11,2,17,20,27,29,30,31,32,36,35,34,33])).
% 64.91/64.98 cnf(4792,plain,
% 64.91/64.98 (P1(f8(a1),f8(a2),a3)),
% 64.91/64.98 inference(scs_inference,[],[4784,1,17,20])).
% 64.91/64.98 cnf(4794,plain,
% 64.91/64.98 (P3(f11(a1,a9),f8(a4),f11(a6,x47941))),
% 64.91/64.98 inference(scs_inference,[],[4759,4784,2006,3605,1,17,20,29])).
% 64.91/64.98 cnf(4796,plain,
% 64.91/64.98 (P3(a4,f8(a6),a4)),
% 64.91/64.98 inference(scs_inference,[],[4752,4759,4784,2006,4249,855,3605,1,17,20,29,30])).
% 64.91/64.98 cnf(4798,plain,
% 64.91/64.98 (P1(a4,a6,f11(x47981,a6))),
% 64.91/64.98 inference(scs_inference,[],[4754,4752,4759,4784,4714,2006,4406,4249,855,3605,1,17,20,29,30,31])).
% 64.91/64.98 cnf(4807,plain,
% 64.91/64.98 (P3(f11(a6,x48071),f11(a6,x48071),a6)),
% 64.91/64.98 inference(scs_inference,[],[4754,4752,4768,4759,4784,4772,4714,4775,4483,4457,4475,2453,2006,4712,4406,4249,855,933,1058,3605,1,17,20,29,30,31,32,35,33])).
% 64.91/64.98 cnf(4825,plain,
% 64.91/64.98 (P3(f8(a6),a4,a4)),
% 64.91/64.98 inference(scs_inference,[],[4796,17])).
% 64.91/64.98 cnf(4829,plain,
% 64.91/64.98 (~P3(a6,a5,f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[4796,4798,4416,6,17,20,27])).
% 64.91/64.98 cnf(4830,plain,
% 64.91/64.98 (P3(a6,x48301,x48301)),
% 64.91/64.98 inference(rename_variables,[],[6])).
% 64.91/64.98 cnf(4832,plain,
% 64.91/64.98 (~P3(f11(a6,x48321),a5,f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[4796,4807,4798,4523,4416,6,4830,17,20,27,30])).
% 64.91/64.98 cnf(4836,plain,
% 64.91/64.98 (P3(f11(a1,a9),f8(a4),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4796,4807,4798,4523,4641,4507,4416,9,12,6,4830,17,20,27,30,33])).
% 64.91/64.98 cnf(4866,plain,
% 64.91/64.98 (P3(f8(a4),f11(a1,a9),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4836,17])).
% 64.91/64.98 cnf(4868,plain,
% 64.91/64.98 (~P2(f7(a6,a5),f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[4829,4836,11,17,21])).
% 64.91/64.98 cnf(4869,plain,
% 64.91/64.98 (P3(x48691,x48692,f7(x48691,x48692))),
% 64.91/64.98 inference(rename_variables,[],[11])).
% 64.91/64.98 cnf(4871,plain,
% 64.91/64.98 (~P1(f8(a1),f8(a10),f7(a6,a5))),
% 64.91/64.98 inference(scs_inference,[],[4829,4836,4455,11,17,21,28])).
% 64.91/64.98 cnf(4875,plain,
% 64.91/64.98 (P3(x48751,a6,x48751)),
% 64.91/64.98 inference(rename_variables,[],[5])).
% 64.91/64.98 cnf(4877,plain,
% 64.91/64.98 (~P3(f7(a6,a5),f11(a6,x48771),f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[4829,4836,4455,1284,5,4875,11,17,21,28,27,29])).
% 64.91/64.98 cnf(4878,plain,
% 64.91/64.98 (P3(x48781,a6,x48781)),
% 64.91/64.98 inference(rename_variables,[],[5])).
% 64.91/64.98 cnf(4883,plain,
% 64.91/64.98 (P1(f8(a3),f8(a6),f11(a6,x48831))),
% 64.91/64.98 inference(scs_inference,[],[4829,4836,4669,4505,104,4459,4455,1284,5,4875,4878,11,17,21,28,27,29,30,31])).
% 64.91/64.98 cnf(4887,plain,
% 64.91/64.98 (P1(f8(a3),f11(a6,x48871),a6)),
% 64.91/64.98 inference(rename_variables,[],[4765])).
% 64.91/64.98 cnf(4888,plain,
% 64.91/64.98 (P1(x48881,f11(x48882,a6),f11(x48882,a6))),
% 64.91/64.98 inference(rename_variables,[],[161])).
% 64.91/64.98 cnf(4890,plain,
% 64.91/64.98 (P1(f8(a3),f11(a6,a6),f11(a6,x48901))),
% 64.91/64.98 inference(scs_inference,[],[4829,4836,4765,4887,4669,4505,3666,104,4459,4455,1284,161,5,4875,4878,11,17,21,28,27,29,30,31,32,36])).
% 64.91/64.98 cnf(4893,plain,
% 64.91/64.98 (P1(f8(a3),f11(a6,x48931),a6)),
% 64.91/64.98 inference(rename_variables,[],[4765])).
% 64.91/64.98 cnf(4895,plain,
% 64.91/64.98 (P1(f11(a6,x48951),f11(a6,a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4829,4836,4765,4887,4893,4669,4505,3666,4722,3500,104,4459,855,4455,1284,161,5,4875,4878,11,17,21,28,27,29,30,31,32,36,35])).
% 64.91/64.98 cnf(4898,plain,
% 64.91/64.98 (P3(f11(a6,x48981),f11(a6,x48981),f11(x48982,a6))),
% 64.91/64.98 inference(scs_inference,[],[4829,4836,4765,4887,4893,4669,4505,3666,4722,4538,3500,104,4459,855,4455,1284,161,4888,5,4875,4878,11,4869,17,21,28,27,29,30,31,32,36,35,34])).
% 64.91/64.98 cnf(4907,plain,
% 64.91/64.98 (P3(f11(a6,x49071),f8(a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[1813,17])).
% 64.91/64.98 cnf(4909,plain,
% 64.91/64.98 (~P2(f11(a1,a10),f7(a6,a5))),
% 64.91/64.98 inference(scs_inference,[],[4871,1813,4455,17,24])).
% 64.91/64.98 cnf(4912,plain,
% 64.91/64.98 (~P3(a6,f7(a6,a5),f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[4871,4868,1813,4455,6,17,24,27])).
% 64.91/64.98 cnf(4913,plain,
% 64.91/64.98 (P3(a6,x49131,x49131)),
% 64.91/64.98 inference(rename_variables,[],[6])).
% 64.91/64.98 cnf(4915,plain,
% 64.91/64.98 (P3(a6,f11(a6,x49151),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4871,4868,1813,4807,2460,4455,6,17,24,27,29])).
% 64.91/64.98 cnf(4918,plain,
% 64.91/64.98 (P3(a4,f8(a4),f11(a6,x49181))),
% 64.91/64.98 inference(scs_inference,[],[4871,4868,4794,1813,4807,2460,4249,4455,6,4913,17,24,27,29,30])).
% 64.91/64.98 cnf(4921,plain,
% 64.91/64.98 (P1(f11(a6,x49211),f7(a6,a6),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4871,4868,4794,4636,1813,4807,4408,2460,1403,4249,4455,6,4913,17,24,27,29,30,31])).
% 64.91/64.98 cnf(4922,plain,
% 64.91/64.98 (P1(f11(x49221,a6),x49222,f11(a6,x49223))),
% 64.91/64.98 inference(rename_variables,[],[1403])).
% 64.91/64.98 cnf(4925,plain,
% 64.91/64.98 (P1(f8(a3),f7(a6,a6),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4871,4868,4890,4794,4636,4497,1813,4807,4408,2460,1403,4249,4455,6,4913,17,24,27,29,30,31,32])).
% 64.91/64.98 cnf(4926,plain,
% 64.91/64.98 (P1(f11(a6,x49261),a9,f7(a6,a6))),
% 64.91/64.98 inference(rename_variables,[],[4497])).
% 64.91/64.98 cnf(4927,plain,
% 64.91/64.98 (P1(f8(a3),f11(a6,a6),f11(a6,x49271))),
% 64.91/64.98 inference(rename_variables,[],[4890])).
% 64.91/64.98 cnf(4929,plain,
% 64.91/64.98 (P1(f8(a3),a6,f11(x49291,a6))),
% 64.91/64.98 inference(scs_inference,[],[4871,4898,4868,4890,4883,4794,4636,4497,1813,4807,4408,2460,1140,1403,4249,4455,6,4913,17,24,27,29,30,31,32,36])).
% 64.91/64.98 cnf(4932,plain,
% 64.91/64.98 (P1(f7(a1,a1),f7(a6,a6),a6)),
% 64.91/64.98 inference(scs_inference,[],[4871,4898,4868,4890,4883,4794,4636,4497,1813,4807,4408,2460,1140,1403,4249,4455,6,4913,11,17,24,27,29,30,31,32,36,35])).
% 64.91/64.98 cnf(4933,plain,
% 64.91/64.98 (P3(x49331,x49332,f7(x49331,x49332))),
% 64.91/64.98 inference(rename_variables,[],[11])).
% 64.91/64.98 cnf(4935,plain,
% 64.91/64.98 (P3(f7(a6,a6),f11(a6,x49351),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4871,4898,4868,4890,4927,4883,4794,4636,4497,1813,4807,4408,4402,2460,4722,1140,1403,4249,4455,1127,6,4913,11,17,24,27,29,30,31,32,36,35,34])).
% 64.91/64.98 cnf(4938,plain,
% 64.91/64.98 (P3(f7(a6,a6),f7(a6,a6),f11(a6,x49381))),
% 64.91/64.98 inference(scs_inference,[],[4871,4898,4868,4890,4927,4883,4794,4636,4497,4926,1813,4807,4408,4402,2460,4722,1140,1403,4922,4249,4455,1127,6,4913,11,4933,17,24,27,29,30,31,32,36,35,34,33])).
% 64.91/64.98 cnf(4943,plain,
% 64.91/64.98 (P3(f11(x49431,a6),f11(a6,x49432),f11(x49433,a6))),
% 64.91/64.98 inference(scs_inference,[],[3007,17])).
% 64.91/64.98 cnf(4948,plain,
% 64.91/64.98 (~P3(f11(a1,a10),f7(a6,a6),f7(a6,a5))),
% 64.91/64.98 inference(scs_inference,[],[4909,3007,12,53,17,28,27])).
% 64.91/64.98 cnf(4951,plain,
% 64.91/64.98 (P3(f11(a6,x49511),f11(a1,a9),a4)),
% 64.91/64.98 inference(scs_inference,[],[4909,4866,4918,3007,4796,12,53,17,28,27,29])).
% 64.91/64.98 cnf(4953,plain,
% 64.91/64.98 (~P3(f8(a6),f11(a1,a10),a5)),
% 64.91/64.98 inference(scs_inference,[],[4909,4866,4907,4918,3007,4832,4796,12,53,6,17,28,27,29,30])).
% 64.91/64.98 cnf(4957,plain,
% 64.91/64.98 (P1(f8(a3),f11(a6,x49571),f11(a6,x49571))),
% 64.91/64.98 inference(scs_inference,[],[4909,4866,4925,4938,4907,4918,3007,4832,4796,12,53,6,17,28,27,29,30,36])).
% 64.91/64.98 cnf(4972,plain,
% 64.91/64.98 (P3(f11(a1,a9),f11(a6,x49721),a4)),
% 64.91/64.98 inference(scs_inference,[],[4951,17])).
% 64.91/64.98 cnf(4974,plain,
% 64.91/64.98 (~P3(a3,f8(a4),f11(a1,a10))),
% 64.91/64.98 inference(scs_inference,[],[4951,4416,8,17,27])).
% 64.91/64.98 cnf(4976,plain,
% 64.91/64.98 (~P3(f11(a1,a10),f8(a6),f7(a6,a5))),
% 64.91/64.98 inference(scs_inference,[],[4948,4951,4416,855,5,8,17,27,29])).
% 64.91/64.98 cnf(4977,plain,
% 64.91/64.98 (P3(x49771,a6,x49771)),
% 64.91/64.98 inference(rename_variables,[],[5])).
% 64.91/64.98 cnf(4979,plain,
% 64.91/64.98 (~P3(f11(a1,a10),f11(a6,x49791),f7(a6,a5))),
% 64.91/64.98 inference(scs_inference,[],[4948,4951,2098,4416,855,5,4977,8,17,27,29,30])).
% 64.91/64.98 cnf(4982,plain,
% 64.91/64.98 (P1(a4,f8(a6),f7(a6,a6))),
% 64.91/64.98 inference(scs_inference,[],[4948,4951,4686,4754,4404,2098,4416,855,5,4977,8,17,27,29,30,31])).
% 64.91/64.98 cnf(4985,plain,
% 64.91/64.98 (P1(f8(a3),f11(a6,x49851),f8(a6))),
% 64.91/64.98 inference(scs_inference,[],[4948,4951,4895,4929,4686,4754,4404,2098,4416,855,1386,5,4977,8,17,27,29,30,31,32])).
% 64.91/64.98 cnf(5007,plain,
% 64.91/64.98 (P3(f11(a6,x50071),f8(a6),f11(a6,x50072))),
% 64.91/64.98 inference(scs_inference,[],[2491,17])).
% 65.09/64.98 cnf(5009,plain,
% 65.09/64.98 (P3(a4,f11(a6,x50091),a4)),
% 65.09/64.98 inference(scs_inference,[],[4972,4943,2491,17,29])).
% 65.09/64.98 cnf(5011,plain,
% 65.09/64.98 (P3(f11(x50111,a6),f11(a6,x50112),f11(x50113,a6))),
% 65.09/64.98 inference(rename_variables,[],[4943])).
% 65.09/64.98 cnf(5013,plain,
% 65.09/64.98 (P3(f11(a6,x50131),f8(a6),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[4972,4943,4935,2491,4501,17,29,30])).
% 65.09/64.98 cnf(5015,plain,
% 65.09/64.98 (P1(a1,f8(a6),f11(x50151,a6))),
% 65.09/64.98 inference(scs_inference,[],[4972,4943,4935,2491,4929,4587,4501,4406,17,29,30,32])).
% 65.09/64.98 cnf(5018,plain,
% 65.09/64.98 (P1(f8(a3),f11(x50181,a6),f11(a6,x50182))),
% 65.09/64.98 inference(scs_inference,[],[4972,4985,4943,5011,4935,2491,4929,4587,4501,4406,2290,17,29,30,32,36])).
% 65.09/64.98 cnf(5023,plain,
% 65.09/64.98 (P1(f11(a6,x50231),f11(a6,x50232),f7(a6,a6))),
% 65.09/64.98 inference(scs_inference,[],[4972,4985,4943,5011,4935,4778,2491,4929,4587,4501,967,4595,4406,2290,1127,17,29,30,32,36,35])).
% 65.09/64.98 cnf(5030,plain,
% 65.09/64.98 (P3(f11(a6,x50301),f11(a6,x50301),f11(a6,x50302))),
% 65.09/64.98 inference(scs_inference,[],[4972,4985,4943,5011,4935,4778,4602,4533,4534,2491,4929,4775,4587,4501,4530,967,4595,4406,2290,1127,11,17,29,30,32,36,35,33,34])).
% 65.09/64.98 cnf(5044,plain,
% 65.09/64.98 (P3(f11(a6,x50441),a4,a4)),
% 65.09/64.98 inference(scs_inference,[],[5009,17])).
% 65.09/64.98 cnf(5054,plain,
% 65.09/64.98 (P1(a4,f7(a6,a6),a6)),
% 65.09/64.98 inference(scs_inference,[],[5009,4953,4982,4979,1134,1462,2253,1082,53,6,17,29,30,36])).
% 65.09/64.98 cnf(5056,plain,
% 65.09/64.98 (P1(f7(a1,a1),f8(a6),f11(a6,x50561))),
% 65.09/64.98 inference(scs_inference,[],[5030,5015,5009,4953,4982,4979,1134,1462,2253,1082,53,6,11,17,29,30,36,35])).
% 65.09/64.98 cnf(5061,plain,
% 65.09/64.98 (P1(f8(a4),f7(a6,a6),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5030,5015,5009,4953,4982,4979,1134,1462,2253,1082,53,6,11,17,29,30,36,35,19])).
% 65.09/64.98 cnf(5082,plain,
% 65.09/64.98 (P3(f11(a6,x50821),f8(a6),f11(x50822,a6))),
% 65.09/64.98 inference(scs_inference,[],[1801,17])).
% 65.09/64.98 cnf(5084,plain,
% 65.09/64.98 (~P3(f11(a1,a10),f11(x50841,a6),f7(a6,a5))),
% 65.09/64.98 inference(scs_inference,[],[4976,1801,1000,5,17,29])).
% 65.09/64.98 cnf(5087,plain,
% 65.09/64.98 (P1(f11(a6,x50871),f8(a6),f11(a6,x50872))),
% 65.09/64.98 inference(scs_inference,[],[5056,4976,1801,1000,4775,4404,5,17,29,31])).
% 65.09/64.98 cnf(5090,plain,
% 65.09/64.98 (P1(a4,f11(a6,x50901),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5054,5056,4976,1801,1000,4775,4404,4459,2159,5,17,29,31,32])).
% 65.09/64.98 cnf(5099,plain,
% 65.09/64.98 (P1(a4,f7(a6,a6),f11(x50991,a6))),
% 65.09/64.98 inference(scs_inference,[],[5061,5054,5056,4976,4581,870,1801,1000,5009,4921,4772,4775,4404,4459,2159,5,17,29,31,32,36,35])).
% 65.09/64.98 cnf(5102,plain,
% 65.09/64.98 (P3(f11(a6,x51021),f11(a6,x51022),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5061,5054,5056,4976,5007,5013,4581,870,1801,1000,5009,4921,4772,4775,4404,4459,2290,2159,5,17,29,31,32,36,35,30])).
% 65.09/64.98 cnf(5116,plain,
% 65.09/64.98 (P3(f11(a1,a9),f8(a4),a6)),
% 65.09/64.98 inference(scs_inference,[],[3809,17])).
% 65.09/64.98 cnf(5118,plain,
% 65.09/64.98 (P3(f11(x51181,a6),a4,a4)),
% 65.09/64.98 inference(scs_inference,[],[5082,4825,3809,5044,17,29])).
% 65.09/64.98 cnf(5121,plain,
% 65.09/64.98 (~P3(f7(a6,a6),a5,f11(a1,a10))),
% 65.09/64.98 inference(scs_inference,[],[5082,4974,4825,3809,1072,5044,4468,17,29,30])).
% 65.09/64.98 cnf(5123,plain,
% 65.09/64.98 (P1(f11(a6,x51231),f11(x51232,a6),f7(a6,a6))),
% 65.09/64.98 inference(scs_inference,[],[5082,5087,4974,5023,4825,3809,1072,5044,4468,1058,17,29,30,31])).
% 65.09/64.98 cnf(5125,plain,
% 65.09/64.98 (P1(f11(a6,x51251),f8(a6),f11(a6,x51252))),
% 65.09/64.98 inference(rename_variables,[],[5087])).
% 65.09/64.98 cnf(5128,plain,
% 65.09/64.98 (P1(f11(a6,x51281),f11(a6,x51282),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5082,5087,5125,4974,4496,5023,4825,3809,1072,5044,4468,4005,1058,17,29,30,31,32])).
% 65.09/64.98 cnf(5159,plain,
% 65.09/64.98 (P3(a4,f11(x51591,a6),a4)),
% 65.09/64.98 inference(scs_inference,[],[5118,17])).
% 65.09/64.98 cnf(5161,plain,
% 65.09/64.98 (~P3(f11(a1,a10),f11(a1,a9),a3)),
% 65.09/64.98 inference(scs_inference,[],[5116,5118,4974,5,17,29])).
% 65.09/64.98 cnf(5164,plain,
% 65.09/64.98 (P3(f11(x51641,a6),f11(a6,x51642),f11(a6,x51642))),
% 65.09/64.98 inference(scs_inference,[],[5116,5118,4974,4918,5,17,29,30])).
% 65.09/64.98 cnf(5166,plain,
% 65.09/64.98 (P1(a4,f11(x51661,a6),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5116,5118,5099,3147,4974,4918,679,5,17,29,30,36])).
% 65.09/64.98 cnf(5170,plain,
% 65.09/64.98 (P3(f11(a6,x51701),f11(a6,x51701),f7(a6,a6))),
% 65.09/64.98 inference(scs_inference,[],[5116,5123,5118,5099,3147,5087,4974,4918,679,724,5,17,29,30,36,33])).
% 65.09/64.98 cnf(5174,plain,
% 65.09/64.98 (P1(a4,f11(a6,a6),f11(a6,x51741))),
% 65.09/64.98 inference(scs_inference,[],[5116,5123,5118,5099,3147,5087,4974,4972,4918,4491,679,724,161,5,17,29,30,36,33,35])).
% 65.09/64.98 cnf(5200,plain,
% 65.09/64.98 (P3(f11(a1,a9),f8(a4),f11(x52001,a6))),
% 65.09/64.98 inference(scs_inference,[],[3663,17])).
% 65.09/64.98 cnf(5202,plain,
% 65.09/64.98 (~P3(f11(a1,a10),a4,a3)),
% 65.09/64.98 inference(scs_inference,[],[5161,3663,4718,53,17,29])).
% 65.09/64.98 cnf(5205,plain,
% 65.09/64.98 (P3(f11(a1,a9),f8(a6),a4)),
% 65.09/64.98 inference(scs_inference,[],[5161,5116,4866,4464,3663,4718,53,17,29,30])).
% 65.09/64.98 cnf(5207,plain,
% 65.09/64.98 (P1(f11(a6,x52071),f11(a6,x52072),f11(a6,x52073))),
% 65.09/64.98 inference(scs_inference,[],[5161,5128,5116,5018,4883,4866,4464,3663,4718,53,17,29,30,31])).
% 65.09/64.98 cnf(5211,plain,
% 65.09/64.98 (P1(a4,f7(a6,a6),f7(a6,a6))),
% 65.09/64.98 inference(scs_inference,[],[5161,5170,5174,5128,5116,5018,4883,4866,4464,3663,4718,53,17,29,30,31,36])).
% 65.09/64.98 cnf(5212,plain,
% 65.09/64.98 (P1(a4,f11(a6,a6),f11(a6,x52121))),
% 65.09/64.98 inference(rename_variables,[],[5174])).
% 65.09/64.98 cnf(5214,plain,
% 65.09/64.98 (P3(f11(a6,x52141),f11(a6,x52141),f7(a6,a6))),
% 65.09/64.98 inference(rename_variables,[],[5170])).
% 65.09/64.98 cnf(5216,plain,
% 65.09/64.98 (P1(f7(a4,a4),f11(a6,a6),f7(a6,a6))),
% 65.09/64.98 inference(scs_inference,[],[5161,5170,5214,5174,5212,5128,5116,5018,4883,4866,4464,3663,4718,53,11,17,29,30,31,36,35])).
% 65.09/64.98 cnf(5217,plain,
% 65.09/64.98 (P1(a4,f11(a6,a6),f11(a6,x52171))),
% 65.09/64.98 inference(rename_variables,[],[5174])).
% 65.09/64.98 cnf(5220,plain,
% 65.09/64.98 (P1(f8(a1),f7(a6,a6),f11(a6,x52201))),
% 65.09/64.98 inference(scs_inference,[],[5161,5170,5214,5174,5212,5217,5128,5116,5018,4883,4866,4464,3663,4754,4718,4595,53,11,17,29,30,31,36,35,32])).
% 65.09/64.98 cnf(5236,plain,
% 65.09/64.98 (P3(f8(a6),f11(a1,a9),a4)),
% 65.09/64.98 inference(scs_inference,[],[5205,17])).
% 65.09/64.98 cnf(5238,plain,
% 65.09/64.98 (P3(f11(x52381,a6),f11(a1,a9),a4)),
% 65.09/64.98 inference(scs_inference,[],[5205,5200,3579,4972,17,29])).
% 65.09/64.98 cnf(5244,plain,
% 65.09/64.98 (P1(f11(a6,x52441),f7(a6,a6),f11(a6,x52442))),
% 65.09/64.98 inference(scs_inference,[],[5205,5200,5207,5121,1313,5099,3579,4972,1403,6,17,29,30,31])).
% 65.09/64.98 cnf(5249,plain,
% 65.09/64.98 (P1(a4,f7(a6,a6),f11(a6,x52491))),
% 65.09/64.98 inference(scs_inference,[],[5205,5211,5200,5207,5121,1313,5099,5159,4475,3579,4972,4938,1403,6,17,29,30,31,35])).
% 65.09/64.98 cnf(5276,plain,
% 65.09/64.98 (P3(f11(a1,a9),f11(x52761,a6),a4)),
% 65.09/64.98 inference(scs_inference,[],[5238,17])).
% 65.09/64.98 cnf(5278,plain,
% 65.09/64.98 (P2(f11(a6,x52781),f11(a6,x52782))),
% 65.09/64.98 inference(scs_inference,[],[5244,5238,2139,17,28])).
% 65.09/64.98 cnf(5281,plain,
% 65.09/64.98 (~P3(f7(a6,a5),f8(a6),f11(a1,a10))),
% 65.09/64.98 inference(scs_inference,[],[5244,5238,4877,4915,2139,5,17,28,29])).
% 65.09/64.98 cnf(5282,plain,
% 65.09/64.98 (P3(a6,f11(a6,x52821),f8(a6))),
% 65.09/64.98 inference(rename_variables,[],[4915])).
% 65.09/64.98 cnf(5285,plain,
% 65.09/64.98 (P3(f7(a6,a6),a4,a4)),
% 65.09/64.98 inference(scs_inference,[],[5244,5238,4877,4915,4581,2139,5,17,28,29,30])).
% 65.09/64.98 cnf(5290,plain,
% 65.09/64.98 (P1(a4,f8(a6),f11(a6,x52901))),
% 65.09/64.98 inference(scs_inference,[],[5244,5238,5249,4877,4915,4581,2139,1127,5,17,28,29,30,32])).
% 65.09/64.98 cnf(5294,plain,
% 65.09/64.98 (P1(f7(a4,a4),f8(a6),f11(a6,x52941))),
% 65.09/64.98 inference(scs_inference,[],[5244,5238,5249,5216,4877,4915,5282,4581,1766,2139,1127,3,5,17,28,29,30,32,36])).
% 65.09/64.98 cnf(5315,plain,
% 65.09/64.98 (P3(f11(x53151,a6),f8(a6),f7(a6,a6))),
% 65.09/64.98 inference(scs_inference,[],[2631,17])).
% 65.09/64.98 cnf(5319,plain,
% 65.09/64.98 (P2(f11(a6,x53191),f11(a6,x53192))),
% 65.09/64.98 inference(rename_variables,[],[5278])).
% 65.09/64.98 cnf(5321,plain,
% 65.09/64.98 (P3(a6,f11(a6,x53211),f11(a6,x53212))),
% 65.09/64.98 inference(scs_inference,[],[5278,5319,1300,2631,850,17,26,21])).
% 65.09/64.98 cnf(5323,plain,
% 65.09/64.98 (P2(f11(a6,x53231),f11(a6,x53232))),
% 65.09/64.98 inference(rename_variables,[],[5278])).
% 65.09/64.98 cnf(5325,plain,
% 65.09/64.98 (P3(f11(a6,x53251),f11(a6,x53252),f11(a6,x53253))),
% 65.09/64.98 inference(scs_inference,[],[5278,5319,5323,1300,5030,2631,850,17,26,21,23])).
% 65.09/64.98 cnf(5331,plain,
% 65.09/64.98 (P3(a6,f11(a6,x53311),a6)),
% 65.09/64.98 inference(scs_inference,[],[5278,5319,5323,1300,5164,5030,4667,4486,2631,2847,4974,850,6,17,26,21,23,29,30])).
% 65.09/64.98 cnf(5332,plain,
% 65.09/64.98 (P3(f7(a6,a6),f11(a6,x53321),a6)),
% 65.09/64.98 inference(rename_variables,[],[4667])).
% 65.09/64.98 cnf(5334,plain,
% 65.09/64.98 (P3(f11(x53341,a6),f11(a6,x53342),f11(a6,x53342))),
% 65.09/64.98 inference(rename_variables,[],[5164])).
% 65.09/64.98 cnf(5336,plain,
% 65.09/64.98 (P1(a3,f8(a6),f7(a6,a6))),
% 65.09/64.98 inference(scs_inference,[],[5278,5319,5323,1300,5164,5030,4792,4686,4667,4486,2631,2847,4974,4404,850,6,17,26,21,23,29,30,31])).
% 65.09/64.98 cnf(5337,plain,
% 65.09/64.98 (P1(f8(x53371),f8(a6),a6)),
% 65.09/64.98 inference(rename_variables,[],[4404])).
% 65.09/64.98 cnf(5343,plain,
% 65.09/64.98 (P1(a4,f11(x53431,a6),f8(a6))),
% 65.09/64.98 inference(rename_variables,[],[5166])).
% 65.09/64.98 cnf(5344,plain,
% 65.09/64.98 (P3(f11(x53441,a6),f11(a6,x53442),f11(a6,x53442))),
% 65.09/64.98 inference(rename_variables,[],[5164])).
% 65.09/64.98 cnf(5346,plain,
% 65.09/64.98 (P1(a4,f8(a6),a6)),
% 65.09/64.98 inference(scs_inference,[],[5278,5319,5323,5290,5166,1300,5164,5334,5030,4792,4686,4667,5332,4471,4486,2631,2847,5118,4974,4754,4404,5337,1140,850,6,17,26,21,23,29,30,31,32,36,35])).
% 65.09/64.98 cnf(5351,plain,
% 65.09/64.98 (P1(f7(a4,a4),f11(a6,x53511),f7(a6,a6))),
% 65.09/64.98 inference(scs_inference,[],[5278,5319,5323,5290,5166,1300,5216,5164,5334,5030,4792,4686,4667,5332,4471,4486,2631,2847,5118,4974,4754,4404,5337,1140,850,6,17,26,21,23,29,30,31,32,36,35,25])).
% 65.09/64.98 cnf(5352,plain,
% 65.09/64.98 (P2(f11(a6,x53521),f11(a6,x53522))),
% 65.09/64.98 inference(rename_variables,[],[5278])).
% 65.09/64.98 cnf(5354,plain,
% 65.09/64.98 (P3(f11(x53541,a6),f11(a6,x53542),f11(a6,x53543))),
% 65.09/64.98 inference(scs_inference,[],[5278,5319,5323,5352,5290,5166,1300,5216,5164,5334,5344,5030,4792,4686,4667,5332,4471,4486,2631,2847,5118,4974,4754,4404,5337,1140,850,6,17,26,21,23,29,30,31,32,36,35,25,22])).
% 65.09/64.98 cnf(5359,plain,
% 65.09/64.98 (~P1(a1,f7(a10,a9),a3)),
% 65.09/64.98 inference(scs_inference,[],[5285,5281,5278,5319,5323,5352,5290,5166,5343,1300,5202,5216,5164,5334,5344,5030,4792,4686,4667,5332,4471,4486,2631,2847,5118,4974,4754,4404,5337,1140,850,12,6,11,2,17,26,21,23,29,30,31,32,36,35,25,22,34,33])).
% 65.09/64.98 cnf(5372,plain,
% 65.09/64.98 (P3(f11(a6,x53721),f11(x53722,a6),f11(a6,x53723))),
% 65.09/64.98 inference(scs_inference,[],[5354,17])).
% 65.09/64.98 cnf(5374,plain,
% 65.09/64.98 (~P2(a2,f7(a10,a9))),
% 65.09/64.98 inference(scs_inference,[],[5354,5359,1,17,25])).
% 65.09/64.98 cnf(5376,plain,
% 65.09/64.98 (P3(f7(a6,a6),f11(a1,a9),f11(a1,a9))),
% 65.09/64.98 inference(scs_inference,[],[5354,5359,5236,2639,3605,1,17,25,29])).
% 65.09/64.98 cnf(5378,plain,
% 65.09/64.98 (~P3(f8(a5),f11(a1,a10),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5354,5359,5236,4676,2639,3605,9,6,1,17,25,29,30])).
% 65.09/64.98 cnf(5388,plain,
% 65.09/64.98 (P1(f7(a3,a3),f8(a6),a6)),
% 65.09/64.98 inference(scs_inference,[],[5351,5315,5354,5336,5359,5294,5236,4676,3016,2639,2253,3605,9,6,11,1,17,25,29,30,36,35])).
% 65.09/64.98 cnf(5406,plain,
% 65.09/64.98 (P3(f7(a6,a6),f11(x54061,a6),f11(a6,x54062))),
% 65.09/64.98 inference(scs_inference,[],[1964,17])).
% 65.09/64.98 cnf(5408,plain,
% 65.09/64.98 (~P3(a2,f7(a6,a6),f7(a10,a9))),
% 65.09/64.98 inference(scs_inference,[],[5374,1964,53,17,27])).
% 65.09/64.98 cnf(5409,plain,
% 65.09/64.98 (P3(x54091,f7(a6,a6),x54091)),
% 65.09/64.98 inference(rename_variables,[],[53])).
% 65.09/64.98 cnf(5411,plain,
% 65.09/64.98 (~P2(f7(a10,a9),a2)),
% 65.09/64.98 inference(scs_inference,[],[5374,1964,53,5409,17,27,23])).
% 65.09/64.98 cnf(5412,plain,
% 65.09/64.98 (P3(x54121,f7(a6,a6),x54121)),
% 65.09/64.98 inference(rename_variables,[],[53])).
% 65.09/64.98 cnf(5418,plain,
% 65.09/64.98 (P3(f11(x54181,a6),a4,f11(a1,a9))),
% 65.09/64.98 inference(scs_inference,[],[5376,5374,5315,5084,738,1964,5236,53,5409,5412,17,27,23,29,30])).
% 65.09/64.98 cnf(5420,plain,
% 65.09/64.98 (P1(f7(a3,a3),f11(a6,a6),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5376,5388,5374,5315,5084,738,1964,5236,4503,4459,53,5409,5412,17,27,23,29,30,32])).
% 65.09/64.98 cnf(5424,plain,
% 65.09/64.98 (P3(a3,f8(a3),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5376,5388,5374,5315,5084,4578,738,1964,5236,4587,4503,4459,9,53,5409,5412,1,17,27,23,29,30,32,33])).
% 65.09/64.98 cnf(5451,plain,
% 65.09/64.98 (P3(a4,f11(x54511,a6),f11(a1,a9))),
% 65.09/64.98 inference(scs_inference,[],[5418,17])).
% 65.09/64.98 cnf(5453,plain,
% 65.09/64.98 (~P3(f7(a10,a9),f7(a6,a6),a2)),
% 65.09/64.98 inference(scs_inference,[],[5418,5411,53,17,27])).
% 65.09/64.98 cnf(5454,plain,
% 65.09/64.98 (P3(x54541,f7(a6,a6),x54541)),
% 65.09/64.98 inference(rename_variables,[],[53])).
% 65.09/64.98 cnf(5456,plain,
% 65.09/64.98 (~P3(a2,f8(a6),f7(a10,a9))),
% 65.09/64.98 inference(scs_inference,[],[5408,5418,5411,1316,53,5454,17,27,29])).
% 65.09/64.98 cnf(5459,plain,
% 65.09/64.98 (P3(f11(x54591,a6),f11(a1,a9),f11(a1,a9))),
% 65.09/64.98 inference(scs_inference,[],[5408,5418,5411,5376,612,1316,53,5454,17,27,29,30])).
% 65.09/64.98 cnf(5461,plain,
% 65.09/64.98 (P1(f8(a1),a6,f11(x54611,a6))),
% 65.09/64.98 inference(scs_inference,[],[5408,5418,5411,5376,612,4929,4505,1316,3,53,5454,17,27,29,30,32])).
% 65.09/64.98 cnf(5464,plain,
% 65.09/64.98 (P1(f7(a3,a3),f11(a6,x54641),f7(a6,a6))),
% 65.09/64.98 inference(scs_inference,[],[5408,5420,5372,5418,5411,5376,612,4929,4505,1316,1082,3,53,5454,17,27,29,30,32,36])).
% 65.09/64.98 cnf(5484,plain,
% 65.09/64.98 (P3(f11(a1,a9),f11(x54841,a6),f11(a1,a9))),
% 65.09/64.98 inference(scs_inference,[],[5459,17])).
% 65.09/64.98 cnf(5489,plain,
% 65.09/64.98 (P3(f11(a6,x54891),f11(a1,a9),f11(a1,a9))),
% 65.09/64.98 inference(scs_inference,[],[5459,5411,5406,5376,5,17,27,29])).
% 65.09/64.98 cnf(5492,plain,
% 65.09/64.98 (~P3(f8(a2),f7(a10,a9),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5456,5459,5411,5406,5376,9,5,6,17,27,29,30])).
% 65.09/64.98 cnf(5496,plain,
% 65.09/64.98 (P1(f11(a6,x54961),x54962,f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5456,5459,5220,4671,5411,5406,5376,2159,9,5,6,17,27,29,30,31])).
% 65.09/64.98 cnf(5504,plain,
% 65.09/64.98 (P1(f11(a1,a9),f8(a6),f11(x55041,a6))),
% 65.09/64.98 inference(scs_inference,[],[5456,5459,5464,5220,4671,5411,5406,5372,5082,5376,5087,679,4459,2159,9,5,6,17,27,29,30,31,36,35])).
% 65.09/64.98 cnf(5519,plain,
% 65.09/64.98 (P3(a4,f11(a6,x55191),f11(a1,a9))),
% 65.09/64.98 inference(scs_inference,[],[5484,5489,5451,5424,5325,2006,3473,17,29,30])).
% 65.09/64.98 cnf(5522,plain,
% 65.09/64.98 (P3(f11(a6,x55221),f11(a6,x55222),f11(a6,x55223))),
% 65.09/64.98 inference(rename_variables,[],[5325])).
% 65.09/64.98 cnf(5524,plain,
% 65.09/64.98 (P1(f11(a6,x55241),x55242,f11(a6,x55243))),
% 65.09/64.98 inference(scs_inference,[],[5484,5489,5496,5451,5424,5325,4957,2006,4883,3473,17,29,30,31])).
% 65.09/64.98 cnf(5527,plain,
% 65.09/64.98 (P1(f7(a1,a1),f8(a6),f7(a6,a6))),
% 65.09/64.98 inference(scs_inference,[],[5484,5489,5496,5451,5424,4932,5325,4957,2006,4883,3473,1236,4459,17,29,30,31,32])).
% 65.09/64.98 cnf(5537,plain,
% 65.09/64.98 (P3(f11(a1,a2),f8(a3),f11(x55371,a6))),
% 65.09/64.98 inference(scs_inference,[],[5484,5489,5496,5504,5451,5424,4932,5325,5522,4957,4531,1813,2006,4883,4587,3473,1236,4459,1058,9,12,17,29,30,31,32,36,33])).
% 65.09/64.98 cnf(5555,plain,
% 65.09/64.98 (P3(f11(a6,x55551),a4,f11(a1,a9))),
% 65.09/64.98 inference(scs_inference,[],[5519,17])).
% 65.09/64.98 cnf(5560,plain,
% 65.09/64.98 (~P3(f7(a2,a6),f11(a6,x55601),f7(a10,a9))),
% 65.09/64.98 inference(scs_inference,[],[5519,5492,5453,5102,1399,4938,53,17,29,30])).
% 65.09/64.98 cnf(5564,plain,
% 65.09/64.98 (P1(f8(a1),f11(x55641,a6),f11(a6,x55642))),
% 65.09/64.98 inference(scs_inference,[],[5519,5492,5453,5102,5018,1399,4505,4938,161,53,17,29,30,32])).
% 65.09/64.98 cnf(5573,plain,
% 65.09/64.98 (P1(f11(a1,a9),f8(a6),f11(a6,x55731))),
% 65.09/64.98 inference(scs_inference,[],[5524,5519,5492,5453,5378,5321,5346,5102,5018,1399,4505,4938,4455,1157,161,9,53,17,29,30,32,34,35])).
% 65.09/64.98 cnf(5597,plain,
% 65.09/64.98 (P3(f11(x55971,a6),f11(a1,a2),a3)),
% 65.09/64.98 inference(scs_inference,[],[5537,1998,4393,5374,2065,5,17,27,29])).
% 65.09/64.98 cnf(5599,plain,
% 65.09/64.98 (~P3(f11(a6,x55991),f11(a1,a10),f7(a6,a5))),
% 65.09/64.98 inference(scs_inference,[],[5537,5331,4912,1998,4393,5374,2065,5,6,17,27,29,30])).
% 65.09/64.98 cnf(5607,plain,
% 65.09/64.98 (P3(f11(a6,x56071),f11(a6,x56072),a6)),
% 65.09/64.98 inference(scs_inference,[],[5573,5564,5537,5331,4912,5354,5346,1998,5205,4393,5374,2065,4005,5,6,17,27,29,30,36,34])).
% 65.09/64.98 cnf(5612,plain,
% 65.09/64.98 (P1(f11(a1,a9),f11(a6,x56121),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[13,5573,5564,5555,5537,5331,5090,4912,5524,5354,5346,5013,4536,1998,5205,4393,5374,2065,4005,5,6,17,27,29,30,36,34,32,35])).
% 65.09/64.98 cnf(5617,plain,
% 65.09/64.98 (P3(f11(a1,a2),f11(x56171,a6),a3)),
% 65.09/64.98 inference(scs_inference,[],[5597,17])).
% 65.09/64.98 cnf(5619,plain,
% 65.09/64.98 (~P3(f7(a10,a9),f11(a6,x56191),f7(a2,a6))),
% 65.09/64.98 inference(scs_inference,[],[5560,5597,5607,5,17,29])).
% 65.09/64.98 cnf(5620,plain,
% 65.09/64.98 (P3(f11(a6,x56201),f11(a6,x56202),a6)),
% 65.09/64.98 inference(rename_variables,[],[5607])).
% 65.09/64.98 cnf(5623,plain,
% 65.09/64.98 (P3(f11(a1,a2),f8(a3),f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5560,5597,5607,5424,2847,5,6,17,29,30])).
% 65.09/64.98 cnf(5626,plain,
% 65.09/64.98 (P1(f7(a1,a1),a6,f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5560,5597,5607,5527,5424,2847,4404,4459,5,6,17,29,30,32])).
% 65.09/64.98 cnf(5630,plain,
% 65.09/64.98 (P1(f11(a1,a9),a6,f8(a6))),
% 65.09/64.98 inference(scs_inference,[],[5612,5560,5597,5607,5620,5527,5424,2847,4404,549,4459,5,6,17,29,30,32,36])).
% 65.09/64.98 cnf(5634,plain,
% 65.09/64.98 (P3(f8(a3),f11(a1,a10),f8(a4))),
% 65.09/64.98 inference(scs_inference,[],[5612,5560,5597,5607,5620,5527,5424,2847,4507,1107,4404,549,4587,4459,12,5,6,17,29,30,32,36,33])).
% 65.09/64.98 cnf(5661,plain,
% 65.09/64.98 (P3(x56611,f7(a6,a6),x56611)),
% 65.09/64.98 inference(rename_variables,[],[53])).
% 65.09/64.98 cnf(5670,plain,
% 65.09/64.98 (P1(f8(a1),f11(a6,a6),f11(x56701,a6))),
% 65.09/64.98 inference(scs_inference,[],[5634,5619,5617,5484,5504,5161,4714,406,4792,4406,4503,4455,53,17,29,31,30,32])).
% 65.09/64.98 cnf(5677,plain,
% 65.09/64.98 (P3(f8(a6),f11(x56771,a6),f8(a6))),
% 65.09/64.98 inference(rename_variables,[],[870])).
% 65.09/64.98 cnf(5686,plain,
% 65.09/64.98 (~P2(f7(a10,a9),f7(a2,a6))),
% 65.09/64.98 inference(scs_inference,[],[5634,5626,5630,5619,5617,5276,5484,5504,5321,5161,4714,870,5677,406,4792,5524,4406,4503,4455,1058,53,5661,17,29,31,30,32,36,35,20,21])).
% 65.09/64.98 cnf(5716,plain,
% 65.09/64.98 ($false),
% 65.09/64.98 inference(scs_inference,[],[5623,5670,5686,5599,5461,5607,4953,4915,4669,1760,5634,2040,5,6,8,17,27,29,30,33,23]),
% 65.09/64.98 ['proof']).
% 65.09/64.98 % SZS output end Proof
% 65.09/64.98 % Total time :64.360000s
%------------------------------------------------------------------------------