%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD029-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n025.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 05:55:18 EDT 2024
% Result : Unsatisfiable 75.59s 75.62s
% Output : CNFRefutation 75.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : FLD029-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.08/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n025.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Jun 19 10:46:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.20/0.58 start to proof:theBenchmark
% 75.59/75.61 %-------------------------------------------
% 75.59/75.61 % File :CSE---1.7
% 75.59/75.61 % Problem :theBenchmark
% 75.59/75.61 % Transform :cnf
% 75.59/75.61 % Format :tptp:raw
% 75.59/75.61 % Command :java -jar mcs_scs.jar %d %s
% 75.59/75.61
% 75.59/75.61 % Result :Theorem 74.980000s
% 75.59/75.61 % Output :CNFRefutation 74.980000s
% 75.59/75.61 %-------------------------------------------
% 75.59/75.62 %--------------------------------------------------------------------------
% 75.59/75.62 % File : FLD029-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 75.59/75.62 % Domain : Field Theory (Ordered fields)
% 75.59/75.62 % Problem : The solution of a multiplicative linear equation is unique
% 75.59/75.62 % Version : [Dra93] axioms : Especial.
% 75.59/75.62 % Theorem formulation : Functional with re axiom set.
% 75.59/75.62 % English :
% 75.59/75.62
% 75.59/75.62 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 75.59/75.62 % Source : [Dra93]
% 75.59/75.62 % Names :
% 75.59/75.62
% 75.59/75.62 % Status : Unsatisfiable
% 75.59/75.62 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.5.0, 0.17 v7.4.0, 0.00 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.20 v5.2.0, 0.10 v5.1.0, 0.27 v5.0.0, 0.36 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0, 0.20 v2.4.0, 0.40 v2.3.0, 0.67 v2.2.1, 0.67 v2.1.0
% 75.59/75.62 % Syntax : Number of clauses : 34 ( 11 unt; 3 nHn; 34 RR)
% 75.59/75.62 % Number of literals : 85 ( 0 equ; 51 neg)
% 75.59/75.62 % Maximal clause size : 5 ( 2 avg)
% 75.59/75.62 % Maximal term depth : 2 ( 1 avg)
% 75.59/75.62 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 75.59/75.62 % Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% 75.59/75.62 % Number of variables : 73 ( 0 sgn)
% 75.59/75.62 % SPC : CNF_UNS_RFO_NEQ_NHN
% 75.59/75.62
% 75.59/75.62 % Comments :
% 75.59/75.62 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 75.59/75.62 %--------------------------------------------------------------------------
% 75.59/75.62 include('Axioms/FLD002-0.ax').
% 75.59/75.62 %--------------------------------------------------------------------------
% 75.59/75.62 cnf(a_is_defined,hypothesis,
% 75.59/75.62 defined(a) ).
% 75.59/75.62
% 75.59/75.62 cnf(b_is_defined,hypothesis,
% 75.59/75.62 defined(b) ).
% 75.59/75.62
% 75.59/75.62 cnf(u_is_defined,hypothesis,
% 75.59/75.62 defined(u) ).
% 75.59/75.62
% 75.59/75.62 cnf(v_is_defined,hypothesis,
% 75.59/75.62 defined(v) ).
% 75.59/75.62
% 75.59/75.62 cnf(not_sum_5,negated_conjecture,
% 75.59/75.62 ~ sum(additive_identity,b,additive_identity) ).
% 75.59/75.62
% 75.59/75.62 cnf(product_6,negated_conjecture,
% 75.59/75.62 product(a,u,b) ).
% 75.59/75.62
% 75.59/75.62 cnf(product_7,negated_conjecture,
% 75.59/75.62 product(a,v,b) ).
% 75.59/75.62
% 75.59/75.62 cnf(not_product_8,negated_conjecture,
% 75.59/75.62 ~ product(multiplicative_identity,u,v) ).
% 75.59/75.62
% 75.59/75.62 %--------------------------------------------------------------------------
% 75.59/75.62 %-------------------------------------------
% 75.59/75.62 % Proof found
% 75.59/75.62 % SZS status Theorem for theBenchmark
% 75.59/75.62 % SZS output start Proof
% 75.59/75.62 %ClaNum:34(EqnAxiom:0)
% 75.59/75.62 %VarNum:162(SingletonVarNum:73)
% 75.59/75.62 %MaxLitNum:5
% 75.59/75.62 %MaxfuncDepth:1
% 75.59/75.62 %SharedTerms:17
% 75.59/75.62 %goalClause: 7 8 10 11
% 75.59/75.62 %singleGoalClaCount:4
% 75.59/75.62 [1]P1(a1)
% 75.59/75.62 [2]P1(a4)
% 75.59/75.63 [3]P1(a2)
% 75.59/75.63 [4]P1(a5)
% 75.59/75.63 [5]P1(a7)
% 75.59/75.63 [6]P1(a10)
% 75.59/75.63 [7]P2(a2,a7,a5)
% 75.59/75.63 [8]P2(a2,a10,a5)
% 75.59/75.63 [9]~P4(a1,a1,a4)
% 75.59/75.63 [10]~P4(a1,a5,a1)
% 75.59/75.63 [11]~P2(a4,a7,a10)
% 75.59/75.63 [17]~P1(x171)+P4(a1,x171,x171)
% 75.59/75.63 [18]~P1(x181)+P2(a4,x181,x181)
% 75.59/75.63 [12]~P1(x121)+P1(f6(x121))
% 75.59/75.63 [19]~P1(x191)+P4(f6(x191),x191,a1)
% 75.59/75.63 [26]~P4(x262,x261,x263)+P4(x261,x262,x263)
% 75.59/75.63 [27]~P2(x272,x271,x273)+P2(x271,x272,x273)
% 75.59/75.63 [20]~P1(x201)+P4(a1,x201,a1)+P1(f9(x201))
% 75.59/75.63 [24]~P1(x241)+P2(f9(x241),x241,a4)+P4(a1,x241,a1)
% 75.59/75.63 [23]~P3(x232,x231)+~P3(x231,x232)+P4(a1,x231,x232)
% 75.59/75.63 [14]~P1(x142)+~P1(x141)+P1(f3(x141,x142))
% 75.59/75.63 [15]~P1(x152)+~P1(x151)+P1(f8(x151,x152))
% 75.59/75.63 [21]~P1(x212)+~P1(x211)+P4(x211,x212,f3(x211,x212))
% 75.59/75.63 [22]~P1(x222)+~P1(x221)+P2(x221,x222,f8(x221,x222))
% 75.59/75.63 [16]~P3(x161,x163)+P3(x161,x162)+~P3(x163,x162)
% 75.59/75.63 [13]P3(x132,x131)+~P1(x131)+~P1(x132)+P3(x131,x132)
% 75.59/75.63 [25]~P2(x253,x252,x251)+P3(a1,x251)+~P3(a1,x252)+~P3(a1,x253)
% 75.59/75.63 [28]~P4(x283,x285,x281)+P3(x281,x282)+~P4(x284,x285,x282)+~P3(x283,x284)
% 75.59/75.63 [29]~P4(x291,x296,x294)+P4(x291,x292,x293)+~P4(x294,x295,x293)+~P4(x296,x295,x292)
% 75.59/75.63 [30]~P4(x306,x304,x301)+P4(x301,x302,x303)+~P4(x304,x302,x305)+~P4(x306,x305,x303)
% 75.59/75.63 [31]~P2(x311,x316,x314)+P2(x311,x312,x313)+~P2(x314,x315,x313)+~P2(x316,x315,x312)
% 75.59/75.63 [32]~P2(x326,x324,x321)+P2(x321,x322,x323)+~P2(x324,x322,x325)+~P2(x326,x325,x323)
% 75.59/75.63 [33]~P2(x335,x337,x332)+~P2(x334,x337,x331)+P4(x331,x332,x333)+~P4(x334,x335,x336)+~P2(x336,x337,x333)
% 75.59/75.63 [34]~P2(x347,x342,x345)+~P2(x346,x342,x344)+P2(x341,x342,x343)+~P4(x344,x345,x343)+~P4(x346,x347,x341)
% 75.59/75.63 %EqnAxiom
% 75.59/75.63
% 75.59/75.63 %-------------------------------------------
% 75.59/75.64 cnf(35,plain,
% 75.59/75.64 (~P2(a7,a4,a10)),
% 75.59/75.64 inference(scs_inference,[],[11,27])).
% 75.59/75.64 cnf(37,plain,
% 75.59/75.64 (~P4(a5,a1,a1)),
% 75.59/75.64 inference(scs_inference,[],[10,11,27,26])).
% 75.59/75.64 cnf(39,plain,
% 75.59/75.64 (P3(a1,a1)),
% 75.59/75.64 inference(scs_inference,[],[10,11,1,27,26,13])).
% 75.59/75.64 cnf(43,plain,
% 75.59/75.64 (~P2(x431,a2,a2)+P2(x431,a5,a5)),
% 75.59/75.64 inference(scs_inference,[],[7,10,11,1,27,26,13,23,31])).
% 75.59/75.64 cnf(45,plain,
% 75.59/75.64 (P2(a5,x451,a5)+~P2(a7,x451,a7)),
% 75.59/75.64 inference(scs_inference,[],[7,10,11,1,27,26,13,23,31,32])).
% 75.59/75.64 cnf(48,plain,
% 75.59/75.64 (P3(a4,a4)),
% 75.59/75.64 inference(scs_inference,[],[2,13])).
% 75.59/75.64 cnf(52,plain,
% 75.59/75.64 (~P2(a1,a1,a4)+~P3(a4,a1)),
% 75.59/75.64 inference(scs_inference,[],[2,9,39,13,23,25])).
% 75.59/75.64 cnf(55,plain,
% 75.59/75.64 (P3(a2,a2)),
% 75.59/75.64 inference(scs_inference,[],[3,13])).
% 75.59/75.64 cnf(57,plain,
% 75.59/75.64 (P2(a5,x571,a5)+~P2(a10,x571,a10)),
% 75.59/75.64 inference(scs_inference,[],[8,3,13,32])).
% 75.59/75.64 cnf(60,plain,
% 75.59/75.64 (P3(a5,a5)),
% 75.59/75.64 inference(scs_inference,[],[4,13])).
% 75.59/75.64 cnf(62,plain,
% 75.59/75.64 (P4(a5,a5,a5)+~P4(a2,a2,a2)),
% 75.59/75.64 inference(scs_inference,[],[7,4,13,33])).
% 75.59/75.64 cnf(65,plain,
% 75.59/75.64 (P3(a7,a7)),
% 75.59/75.64 inference(scs_inference,[],[5,13])).
% 75.59/75.64 cnf(68,plain,
% 75.59/75.64 (P3(a10,a10)),
% 75.59/75.64 inference(scs_inference,[],[6,13])).
% 75.59/75.64 cnf(70,plain,
% 75.59/75.64 (~P4(a7,x701,x702)+~P4(a7,x701,x703)+P3(x702,x703)),
% 75.59/75.64 inference(scs_inference,[],[6,65,13,28])).
% 75.59/75.64 cnf(72,plain,
% 75.59/75.64 (~P4(a4,x721,x722)+~P4(a4,x721,x723)+P3(x722,x723)),
% 75.59/75.64 inference(scs_inference,[],[48,28])).
% 75.59/75.64 cnf(73,plain,
% 75.59/75.64 (~P4(a2,x731,x732)+~P4(a2,x731,x733)+P3(x732,x733)),
% 75.59/75.64 inference(scs_inference,[],[55,28])).
% 75.59/75.64 cnf(83,plain,
% 75.59/75.64 (~P4(a1,x831,x832)+~P4(a1,x831,x833)+P3(x832,x833)),
% 75.59/75.64 inference(scs_inference,[],[39,28])).
% 75.59/75.64 cnf(161,plain,
% 75.59/75.64 (P4(f6(f6(a4)),f6(a4),a1)),
% 75.59/75.64 inference(scs_inference,[],[2,19,12])).
% 75.59/75.64 cnf(164,plain,
% 75.59/75.64 (~P4(a5,f6(a4),f6(a4))),
% 75.59/75.64 inference(scs_inference,[],[10,161,30,26])).
% 75.59/75.64 cnf(181,plain,
% 75.59/75.64 (~P4(a4,x1811,a4)+~P4(a4,x1811,a1)+~P2(a1,a1,a4)),
% 75.59/75.64 inference(scs_inference,[],[52,72])).
% 75.59/75.64 cnf(197,plain,
% 75.59/75.64 (P2(a5,x1971,a5)+~P2(x1971,a2,a2)),
% 75.59/75.64 inference(scs_inference,[],[43,27])).
% 75.59/75.64 cnf(213,plain,
% 75.59/75.64 (~P2(x2131,a7,a7)+P2(a5,x2131,a5)),
% 75.59/75.64 inference(scs_inference,[],[45,27])).
% 75.59/75.64 cnf(229,plain,
% 75.59/75.64 (~P2(x2291,a10,a10)+P2(a5,x2291,a5)),
% 75.59/75.64 inference(scs_inference,[],[57,27])).
% 75.59/75.64 cnf(261,plain,
% 75.59/75.64 (P2(a5,a4,a5)),
% 75.59/75.64 inference(scs_inference,[],[3,197,18])).
% 75.59/75.64 cnf(269,plain,
% 75.59/75.64 (P2(a5,x2691,a5)+~P2(a4,x2691,a4)),
% 75.59/75.64 inference(scs_inference,[],[261,32])).
% 75.59/75.64 cnf(285,plain,
% 75.59/75.64 (P2(x2851,a5,a5)+~P2(x2851,a7,a7)),
% 75.59/75.64 inference(scs_inference,[],[213,27])).
% 75.59/75.64 cnf(301,plain,
% 75.59/75.64 (P2(x3011,a5,a5)+~P2(x3011,a10,a10)),
% 75.59/75.64 inference(scs_inference,[],[229,27])).
% 75.59/75.64 cnf(347,plain,
% 75.59/75.64 (~P2(x3471,a4,a4)+P2(a5,x3471,a5)),
% 75.59/75.64 inference(scs_inference,[],[269,27])).
% 75.59/75.64 cnf(363,plain,
% 75.59/75.64 (P2(a4,a5,a5)),
% 75.59/75.64 inference(scs_inference,[],[5,285,18])).
% 75.59/75.64 cnf(364,plain,
% 75.59/75.64 (P4(a5,a5,a5)+~P4(a4,a4,a4)),
% 75.59/75.64 inference(scs_inference,[],[363,33])).
% 75.59/75.64 cnf(381,plain,
% 75.59/75.64 (~P2(a10,x3811,a10)+P2(x3811,a5,a5)),
% 75.59/75.64 inference(scs_inference,[],[301,27])).
% 75.59/75.64 cnf(943,plain,
% 75.59/75.64 (P4(a1,f6(a5),f6(a5))),
% 75.59/75.64 inference(scs_inference,[],[4,12,17])).
% 75.59/75.64 cnf(1090,plain,
% 75.59/75.64 (P4(a1,f6(a7),f6(a7))),
% 75.59/75.64 inference(scs_inference,[],[5,12,17])).
% 75.59/75.64 cnf(1095,plain,
% 75.59/75.64 (~P4(a1,f6(a1),a1)+P4(f6(a1),f6(a7),f6(a7))),
% 75.59/75.64 inference(scs_inference,[],[1,1090,83,29,19,26])).
% 75.59/75.64 cnf(1146,plain,
% 75.59/75.64 (P4(f6(a7),f6(a1),f6(a7))+~P4(a1,f6(a1),a1)),
% 75.59/75.64 inference(scs_inference,[],[1095,26])).
% 75.59/75.64 cnf(1177,plain,
% 75.59/75.64 (P4(f6(a7),x11771,f6(a7))+~P4(f6(a1),x11771,f6(a1))+~P4(a1,f6(a1),a1)),
% 75.59/75.64 inference(scs_inference,[],[1146,30])).
% 75.59/75.64 cnf(1209,plain,
% 75.59/75.64 (~P4(x12091,f6(a1),f6(a1))+P4(f6(a7),x12091,f6(a7))+~P4(a1,f6(a1),a1)),
% 75.59/75.64 inference(scs_inference,[],[1177,26])).
% 75.59/75.64 cnf(1353,plain,
% 75.59/75.64 (P4(a1,f6(a4),f6(a4))),
% 75.59/75.64 inference(scs_inference,[],[2,12,17])).
% 75.59/75.64 cnf(1389,plain,
% 75.59/75.64 (P2(a4,f6(a4),f6(a4))),
% 75.59/75.64 inference(scs_inference,[],[2,12,18])).
% 75.59/75.64 cnf(2666,plain,
% 75.59/75.64 (P2(a4,f6(a7),f6(a7))),
% 75.59/75.64 inference(scs_inference,[],[5,12,18])).
% 75.59/75.64 cnf(2749,plain,
% 75.59/75.64 (P4(a1,f6(a1),f6(a1))),
% 75.59/75.64 inference(scs_inference,[],[1,12,17])).
% 75.59/75.64 cnf(2750,plain,
% 75.59/75.64 (P3(f6(a1),f6(a1))),
% 75.59/75.64 inference(scs_inference,[],[2749,83])).
% 75.59/75.64 cnf(2755,plain,
% 75.59/75.64 (~P4(x27551,a1,a1)+P4(x27551,f6(a1),f6(a1))),
% 75.59/75.64 inference(scs_inference,[],[2749,29])).
% 75.59/75.64 cnf(2771,plain,
% 75.59/75.64 (P4(f6(a1),x27711,f6(a1))+~P4(x27711,a1,a1)),
% 75.59/75.64 inference(scs_inference,[],[2755,26])).
% 75.59/75.64 cnf(2913,plain,
% 75.59/75.64 (P4(f6(f6(a7)),f6(a7),a1)),
% 75.59/75.64 inference(scs_inference,[],[5,12,19])).
% 75.59/75.64 cnf(2914,plain,
% 75.59/75.64 (~P4(f6(a7),a5,f6(a7))),
% 75.59/75.64 inference(scs_inference,[],[10,2913,30])).
% 75.59/75.64 cnf(2916,plain,
% 75.59/75.64 (~P4(a5,f6(a7),f6(a7))),
% 75.59/75.64 inference(scs_inference,[],[10,2913,30,26])).
% 75.59/75.64 cnf(3236,plain,
% 75.59/75.64 (~P2(x32361,a5,a10)+~P2(x32361,a2,a4)),
% 75.59/75.64 inference(scs_inference,[],[7,11,32])).
% 75.59/75.64 cnf(3240,plain,
% 75.59/75.64 (~P2(f9(a2),a5,a10)+P4(a1,a2,a1)),
% 75.59/75.64 inference(scs_inference,[],[7,11,3,32,27,24])).
% 75.59/75.64 cnf(3271,plain,
% 75.59/75.64 (~P2(a10,x32711,a2)+~P2(a5,x32711,a4)+~P2(a2,a5,a10)),
% 75.59/75.64 inference(scs_inference,[],[8,3236,31])).
% 75.59/75.64 cnf(3351,plain,
% 75.59/75.64 (~P2(a5,f9(a2),a10)+P4(a1,a2,a1)),
% 75.59/75.64 inference(scs_inference,[],[3240,27])).
% 75.59/75.64 cnf(3367,plain,
% 75.59/75.64 (~P4(a2,a5,a2)+~P2(a5,f9(a2),a10)),
% 75.59/75.64 inference(scs_inference,[],[10,3351,30])).
% 75.59/75.64 cnf(3383,plain,
% 75.59/75.64 (~P2(f9(a2),a5,a10)+~P4(a2,a5,a2)),
% 75.59/75.64 inference(scs_inference,[],[3367,27])).
% 75.59/75.64 cnf(3399,plain,
% 75.59/75.64 (~P2(f9(a2),a2,x33991)+~P2(x33991,a10,a10)+~P4(a2,a5,a2)),
% 75.59/75.64 inference(scs_inference,[],[8,3383,31])).
% 75.59/75.64 cnf(3479,plain,
% 75.59/75.64 (~P2(x34791,a5,a4)+~P2(a10,x34791,a2)+~P2(a2,a5,a10)),
% 75.59/75.64 inference(scs_inference,[],[3271,27])).
% 75.59/75.64 cnf(3544,plain,
% 75.59/75.64 (~P4(f6(a5),x35441,a5)+~P4(f6(a5),x35441,a1)),
% 75.59/75.64 inference(scs_inference,[],[943,10,29])).
% 75.59/75.64 cnf(3546,plain,
% 75.59/75.64 (~P4(f6(a5),x35461,a5)+~P4(x35461,f6(a5),a1)),
% 75.59/75.64 inference(scs_inference,[],[943,10,29,26])).
% 75.59/75.64 cnf(3561,plain,
% 75.59/75.64 (~P4(a7,f6(a7),a5)+~P4(a7,f6(a7),a1)),
% 75.59/75.64 inference(scs_inference,[],[5,1090,2914,29,19,26])).
% 75.59/75.64 cnf(3574,plain,
% 75.59/75.64 (~P4(f6(a5),a5,a5)),
% 75.59/75.64 inference(scs_inference,[],[4,3544,19])).
% 75.59/75.64 cnf(3575,plain,
% 75.59/75.64 (~P4(a5,f6(a5),a5)),
% 75.59/75.64 inference(scs_inference,[],[3574,26])).
% 75.59/75.64 cnf(3580,plain,
% 75.59/75.64 (~P4(x35801,f6(a5),a5)+~P4(x35801,a1,a5)),
% 75.59/75.64 inference(scs_inference,[],[943,3575,30])).
% 75.59/75.64 cnf(3585,plain,
% 75.59/75.64 (~P4(a5,a1,x35851)+~P4(x35851,f6(a5),a5)),
% 75.59/75.64 inference(scs_inference,[],[943,3575,29])).
% 75.59/75.64 cnf(3587,plain,
% 75.59/75.64 (~P4(a1,a5,x35871)+~P4(x35871,f6(a5),a5)),
% 75.59/75.64 inference(scs_inference,[],[943,3575,29,26])).
% 75.59/75.64 cnf(3590,plain,
% 75.59/75.64 (~P2(x35901,a10,f6(a5))+~P4(x35901,a2,a2)),
% 75.59/75.64 inference(scs_inference,[],[8,3574,33])).
% 75.59/75.64 cnf(3605,plain,
% 75.59/75.64 (~P2(x36051,a4,f6(a5))+~P4(x36051,a5,a5)),
% 75.59/75.64 inference(scs_inference,[],[261,3574,33])).
% 75.59/75.64 cnf(3660,plain,
% 75.59/75.64 (P4(f6(a5),a1,f6(a5))),
% 75.59/75.64 inference(scs_inference,[],[943,26])).
% 75.59/75.64 cnf(3662,plain,
% 75.59/75.64 (~P4(a1,x36621,a5)+~P4(f6(a5),x36621,a5)),
% 75.59/75.64 inference(scs_inference,[],[943,3574,26,29])).
% 75.59/75.64 cnf(3666,plain,
% 75.59/75.64 (P4(f6(a1),a1,f6(a1))),
% 75.59/75.64 inference(scs_inference,[],[2749,26])).
% 75.59/75.64 cnf(3673,plain,
% 75.59/75.64 (P4(f6(a7),a1,f6(a7))),
% 75.59/75.64 inference(scs_inference,[],[1090,26])).
% 75.59/75.64 cnf(3677,plain,
% 75.59/75.65 (P4(f6(a4),a1,f6(a4))),
% 75.59/75.65 inference(scs_inference,[],[1353,26])).
% 75.59/75.65 cnf(3690,plain,
% 75.59/75.65 (P4(f6(a4),f6(f6(a4)),a1)),
% 75.59/75.65 inference(scs_inference,[],[161,26])).
% 75.59/75.65 cnf(3738,plain,
% 75.59/75.65 (~P4(f6(a5),x37381,a5)+~P4(a5,a1,x37381)),
% 75.59/75.65 inference(scs_inference,[],[3585,26])).
% 75.59/75.65 cnf(3754,plain,
% 75.59/75.65 (~P4(f3(a1,a5),f6(a5),a5)),
% 75.59/75.65 inference(scs_inference,[],[4,1,3587,21])).
% 75.59/75.65 cnf(3755,plain,
% 75.59/75.65 (~P4(x37551,f6(a5),a5)+~P4(x37551,a1,f3(a1,a5))),
% 75.59/75.65 inference(scs_inference,[],[943,3754,30])).
% 75.59/75.65 cnf(3760,plain,
% 75.59/75.65 (P2(a10,a2,a5)),
% 75.59/75.65 inference(scs_inference,[],[8,3660,3754,29,27])).
% 75.59/75.65 cnf(3763,plain,
% 75.59/75.65 (P2(a7,a2,a5)),
% 75.59/75.65 inference(scs_inference,[],[7,27])).
% 75.59/75.65 cnf(3765,plain,
% 75.59/75.65 (P2(a10,a5,x37651)+~P2(a5,a7,x37651)),
% 75.59/75.65 inference(scs_inference,[],[7,3760,27,31])).
% 75.59/75.65 cnf(3770,plain,
% 75.59/75.65 (P2(f6(a4),a4,f6(a4))),
% 75.59/75.65 inference(scs_inference,[],[1389,27])).
% 75.59/75.65 cnf(3772,plain,
% 75.59/75.65 (~P2(a1,a4,a5)),
% 75.59/75.65 inference(scs_inference,[],[164,1389,1353,27,33])).
% 75.59/75.65 cnf(3774,plain,
% 75.59/75.65 (~P2(a2,x37741,a1)+~P2(x37741,a4,a10)),
% 75.59/75.65 inference(scs_inference,[],[8,164,1389,1353,27,33,32])).
% 75.59/75.65 cnf(3776,plain,
% 75.59/75.65 (P2(a7,a5,x37761)+~P2(a5,a10,x37761)),
% 75.59/75.65 inference(scs_inference,[],[8,164,3763,1389,1353,27,33,32,31])).
% 75.59/75.65 cnf(3779,plain,
% 75.59/75.65 (P2(f6(a7),a4,f6(a7))),
% 75.59/75.65 inference(scs_inference,[],[2666,27])).
% 75.59/75.65 cnf(3800,plain,
% 75.59/75.65 (P2(a10,a5,f8(a5,a7))),
% 75.59/75.65 inference(scs_inference,[],[5,4,3765,22])).
% 75.59/75.65 cnf(3803,plain,
% 75.59/75.65 (P2(a7,a5,f8(a5,a7))),
% 75.59/75.65 inference(scs_inference,[],[8,3763,3800,27,31])).
% 75.59/75.65 cnf(3808,plain,
% 75.59/75.65 (P2(a5,a7,f8(a5,a7))),
% 75.59/75.65 inference(scs_inference,[],[3803,27])).
% 75.59/75.65 cnf(3842,plain,
% 75.59/75.65 (~P2(a4,x38421,a10)+~P2(a2,x38421,a1)),
% 75.59/75.65 inference(scs_inference,[],[3774,27])).
% 75.59/75.65 cnf(3858,plain,
% 75.59/75.65 (P2(a7,a5,f8(a5,a10))),
% 75.59/75.65 inference(scs_inference,[],[6,4,3776,22])).
% 75.59/75.65 cnf(3859,plain,
% 75.59/75.65 (P2(a5,a7,f8(a5,a10))),
% 75.59/75.65 inference(scs_inference,[],[3858,27])).
% 75.59/75.65 cnf(3863,plain,
% 75.59/75.65 (P2(a10,a5,f8(a5,a10))),
% 75.59/75.65 inference(scs_inference,[],[363,3858,27,31,3765])).
% 75.59/75.65 cnf(3873,plain,
% 75.59/75.65 (P2(a5,a10,f8(a5,a10))),
% 75.59/75.65 inference(scs_inference,[],[3863,27])).
% 75.59/75.65 cnf(3898,plain,
% 75.59/75.65 (~P2(a10,x38981,f6(a5))+~P4(x38981,a2,a2)),
% 75.59/75.65 inference(scs_inference,[],[3590,27])).
% 75.59/75.65 cnf(3978,plain,
% 75.59/75.65 (~P2(a4,x39781,f6(a5))+~P4(x39781,a5,a5)),
% 75.59/75.65 inference(scs_inference,[],[3605,27])).
% 75.59/75.65 cnf(4170,plain,
% 75.59/75.65 (~P4(x41701,f6(a5),a5)+~P4(a1,x41701,a5)),
% 75.59/75.65 inference(scs_inference,[],[3662,26])).
% 75.59/75.65 cnf(4226,plain,
% 75.59/75.65 (~P4(f6(a5),f3(a5,a1),a5)),
% 75.59/75.65 inference(scs_inference,[],[1,4,3738,21])).
% 75.59/75.65 cnf(4664,plain,
% 75.59/75.65 (~P4(f6(a7),a7,a5)+~P4(a7,f6(a7),a1)),
% 75.59/75.65 inference(scs_inference,[],[3561,26])).
% 75.59/75.65 cnf(4837,plain,
% 75.59/75.65 (~P4(f6(a7),x48371,a5)+~P4(a1,a7,x48371)+~P4(a7,f6(a7),a1)),
% 75.59/75.65 inference(scs_inference,[],[3673,4664,30])).
% 75.59/75.65 cnf(5492,plain,
% 75.59/75.65 (~P4(f6(a1),x54921,a5)+~P4(f6(a1),x54921,a1)),
% 75.59/75.65 inference(scs_inference,[],[2749,10,29])).
% 75.59/75.65 cnf(5495,plain,
% 75.59/75.65 (~P4(f6(a1),x54951,a1)+~P4(f6(a1),x54951,a4)),
% 75.59/75.65 inference(scs_inference,[],[2749,9,29])).
% 75.59/75.65 cnf(5508,plain,
% 75.59/75.65 (~P4(f6(a1),a1,a5)),
% 75.59/75.65 inference(scs_inference,[],[1,5492,19])).
% 75.59/75.65 cnf(5580,plain,
% 75.59/75.65 (~P4(x55801,f6(a1),a4)+~P4(f6(a1),x55801,a1)),
% 75.59/75.65 inference(scs_inference,[],[5495,26])).
% 75.59/75.65 cnf(5596,plain,
% 75.59/75.65 (~P4(a1,f6(a1),a4)),
% 75.59/75.65 inference(scs_inference,[],[1,5580,19])).
% 75.59/75.65 cnf(5597,plain,
% 75.59/75.65 (~P4(f6(a1),a1,a4)),
% 75.59/75.65 inference(scs_inference,[],[2749,3666,5596,29])).
% 75.59/75.65 cnf(5638,plain,
% 75.59/75.65 (~P4(f6(a1),x56381,a5)+~P4(a1,a1,x56381)),
% 75.59/75.65 inference(scs_inference,[],[3666,5508,30])).
% 75.59/75.65 cnf(5676,plain,
% 75.59/75.65 (~P4(x56761,f6(a1),a5)+~P4(a1,a1,x56761)),
% 75.59/75.65 inference(scs_inference,[],[5638,26])).
% 75.59/75.65 cnf(5708,plain,
% 75.59/75.65 (~P4(f3(a1,a1),f6(a1),a5)),
% 75.59/75.65 inference(scs_inference,[],[1,5676,21])).
% 75.59/75.65 cnf(6171,plain,
% 75.59/75.65 (~P2(f6(a7),a5,f6(a7))+~P2(a10,a1,a10)),
% 75.59/75.65 inference(scs_inference,[],[2916,3779,363,1090,31,33,381])).
% 75.59/75.65 cnf(6287,plain,
% 75.59/75.65 (~P2(a4,a5,a4)+~P2(a10,a1,a10)),
% 75.59/75.65 inference(scs_inference,[],[3779,6171,32])).
% 75.59/75.65 cnf(6307,plain,
% 75.59/75.65 (~P2(a5,a4,a4)+~P2(a10,a1,a10)),
% 75.59/75.65 inference(scs_inference,[],[6287,27])).
% 75.59/75.65 cnf(6323,plain,
% 75.59/75.65 (~P2(a4,x63231,a4)+~P2(a5,x63231,a4)+~P2(a10,a1,a10)),
% 75.59/75.65 inference(scs_inference,[],[261,6307,31])).
% 75.59/75.65 cnf(6876,plain,
% 75.59/75.65 (P4(f6(a5),x68761,f6(a5))+~P4(a1,x68761,a1)),
% 75.59/75.65 inference(scs_inference,[],[3660,30])).
% 75.59/75.65 cnf(6881,plain,
% 75.59/75.65 (P4(f6(a1),x68811,f6(a1))+~P4(a1,x68811,a1)),
% 75.59/75.65 inference(scs_inference,[],[3666,30])).
% 75.59/75.65 cnf(6883,plain,
% 75.59/75.65 (P4(x68831,f6(a1),f6(a1))+~P4(a1,x68831,a1)),
% 75.59/75.65 inference(scs_inference,[],[3666,30,26])).
% 75.59/75.65 cnf(6892,plain,
% 75.59/75.65 (~P4(x68921,x68922,f3(a5,a1))+~P4(f6(a5),x68922,a5)+~P4(a1,x68921,a1)),
% 75.59/75.65 inference(scs_inference,[],[4226,6876,29])).
% 75.59/75.65 cnf(7136,plain,
% 75.59/75.65 (P4(a1,a1,a1)),
% 75.59/75.65 inference(scs_inference,[],[3690,1353,29])).
% 75.59/75.65 cnf(7684,plain,
% 75.59/75.65 (~P2(a4,a1,a5)),
% 75.59/75.65 inference(scs_inference,[],[3772,27])).
% 75.59/75.65 cnf(7726,plain,
% 75.59/75.65 (~P4(f6(a1),f3(a1,a1),a5)),
% 75.59/75.65 inference(scs_inference,[],[5708,26])).
% 75.59/75.65 cnf(7890,plain,
% 75.59/75.65 (~P4(f6(a4),x78901,a5)+~P4(x78901,f6(a4),a1)),
% 75.59/75.65 inference(scs_inference,[],[3677,164,30])).
% 75.59/75.65 cnf(7892,plain,
% 75.59/75.65 (~P4(x78921,f6(a4),a5)+~P4(x78921,f6(a4),a1)),
% 75.59/75.65 inference(scs_inference,[],[3677,164,30,26])).
% 75.59/75.65 cnf(7907,plain,
% 75.59/75.65 (~P4(f6(a4),x79071,a1)+~P4(f6(a4),x79071,a5)),
% 75.59/75.65 inference(scs_inference,[],[7890,26])).
% 75.59/75.65 cnf(7914,plain,
% 75.59/75.65 (P1(f6(a10))),
% 75.59/75.65 inference(scs_inference,[],[6,12])).
% 75.59/75.65 cnf(7916,plain,
% 75.59/75.65 (P2(a4,a10,a10)),
% 75.59/75.65 inference(scs_inference,[],[6,12,18])).
% 75.59/75.65 cnf(7918,plain,
% 75.59/75.65 (~P2(a2,a10,a1)),
% 75.59/75.65 inference(scs_inference,[],[6,12,18,3842])).
% 75.59/75.65 cnf(7920,plain,
% 75.59/75.65 (P4(a1,a10,a10)),
% 75.59/75.65 inference(scs_inference,[],[6,12,18,3842,17])).
% 75.59/75.65 cnf(7922,plain,
% 75.59/75.65 (P2(a10,a4,a10)),
% 75.59/75.65 inference(scs_inference,[],[6,12,18,3842,17,27])).
% 75.59/75.65 cnf(7924,plain,
% 75.59/75.65 (P4(a10,a1,a10)),
% 75.59/75.65 inference(scs_inference,[],[6,12,18,3842,17,27,26])).
% 75.59/75.65 cnf(7926,plain,
% 75.59/75.65 (P4(f6(a10),a10,a1)),
% 75.59/75.65 inference(scs_inference,[],[6,12,18,3842,17,27,26,19])).
% 75.59/75.65 cnf(7928,plain,
% 75.59/75.65 (P1(f3(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[6,12,18,3842,17,27,26,19,14])).
% 75.59/75.65 cnf(7930,plain,
% 75.59/75.65 (P1(f8(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[6,12,18,3842,17,27,26,19,14,15])).
% 75.59/75.65 cnf(7932,plain,
% 75.59/75.65 (P2(a10,a10,f8(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[6,12,18,3842,17,27,26,19,14,15,22])).
% 75.59/75.65 cnf(7934,plain,
% 75.59/75.65 (P1(f9(a5))),
% 75.59/75.65 inference(scs_inference,[],[6,4,10,12,18,3842,17,27,26,19,14,15,22,20])).
% 75.59/75.65 cnf(7936,plain,
% 75.59/75.65 (P2(f9(a5),a5,a4)),
% 75.59/75.65 inference(scs_inference,[],[6,4,10,12,18,3842,17,27,26,19,14,15,22,20,24])).
% 75.59/75.65 cnf(7938,plain,
% 75.59/75.65 (P4(a10,a10,f3(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[6,4,10,12,18,3842,17,27,26,19,14,15,22,20,24,21])).
% 75.59/75.65 cnf(7940,plain,
% 75.59/75.65 (P4(a1,a5,a5)),
% 75.59/75.65 inference(scs_inference,[],[6,4,10,60,12,18,3842,17,27,26,19,14,15,22,20,24,21,23])).
% 75.59/75.65 cnf(7942,plain,
% 75.59/75.65 (~P4(f6(a5),a1,a1)),
% 75.59/75.65 inference(scs_inference,[],[6,3574,4,10,60,12,18,3842,17,27,26,19,14,15,22,20,24,21,23,29])).
% 75.59/75.65 cnf(7944,plain,
% 75.59/75.65 (~P2(a10,a2,a1)),
% 75.59/75.65 inference(scs_inference,[],[7684,6,3760,3574,4,10,60,12,18,3842,17,27,26,19,14,15,22,20,24,21,23,29,31])).
% 75.59/75.65 cnf(7946,plain,
% 75.59/75.65 (~P4(a1,f6(a5),a1)),
% 75.59/75.65 inference(scs_inference,[],[7684,6,3760,3574,4,10,3660,943,60,12,18,3842,17,27,26,19,14,15,22,20,24,21,23,29,31,30])).
% 75.59/75.65 cnf(7952,plain,
% 75.59/75.65 (P2(f3(a10,a10),a4,f3(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[7684,6,3760,3574,4,10,3660,943,60,68,12,18,3842,17,27,26,19,14,15,22,20,24,21,23,29,31,30,28,3479,34])).
% 75.59/75.65 cnf(7956,plain,
% 75.59/75.65 (P2(a4,f3(a10,a10),f3(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[7928,18])).
% 75.59/75.65 cnf(7958,plain,
% 75.59/75.65 (P1(f6(a2))),
% 75.59/75.65 inference(scs_inference,[],[7928,3,18,12])).
% 75.59/75.65 cnf(7960,plain,
% 75.59/75.65 (P4(a1,f3(a10,a10),f3(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[7928,3,18,12,17])).
% 75.59/75.65 cnf(7962,plain,
% 75.59/75.65 (P4(a5,a1,a5)),
% 75.59/75.65 inference(scs_inference,[],[7940,7928,3,18,12,17,26])).
% 75.59/75.65 cnf(7964,plain,
% 75.59/75.65 (P2(a5,f9(a5),a4)),
% 75.59/75.65 inference(scs_inference,[],[7940,7928,7936,3,18,12,17,26,27])).
% 75.59/75.65 cnf(7966,plain,
% 75.59/75.65 (P4(f6(a2),a2,a1)),
% 75.59/75.65 inference(scs_inference,[],[7940,7928,7936,3,18,12,17,26,27,19])).
% 75.59/75.65 cnf(7968,plain,
% 75.59/75.65 (P1(f3(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[7940,7928,7936,3,18,12,17,26,27,19,14])).
% 75.59/75.65 cnf(7970,plain,
% 75.59/75.65 (P1(f8(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[7940,7928,7936,3,18,12,17,26,27,19,14,15])).
% 75.59/75.65 cnf(7972,plain,
% 75.59/75.65 (P2(a2,a2,f8(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[7940,7928,7936,3,18,12,17,26,27,19,14,15,22])).
% 75.59/75.65 cnf(7974,plain,
% 75.59/75.65 (P4(a2,a2,f3(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[7940,7928,7936,3,18,12,17,26,27,19,14,15,22,21])).
% 75.59/75.65 cnf(7976,plain,
% 75.59/75.65 (P4(a1,a7,a7)),
% 75.59/75.65 inference(scs_inference,[],[7940,7928,7936,3,65,18,12,17,26,27,19,14,15,22,21,23])).
% 75.59/75.65 cnf(7980,plain,
% 75.59/75.65 (~P2(a10,a4,a7)),
% 75.59/75.65 inference(scs_inference,[],[7916,7922,7940,7942,7928,7926,7936,11,3,65,18,12,17,26,27,19,14,15,22,21,23,29,31])).
% 75.59/75.65 cnf(7982,plain,
% 75.59/75.65 (~P4(f6(a10),a10,f6(a5))),
% 75.59/75.65 inference(scs_inference,[],[7916,7922,7924,7940,7942,7928,7926,7936,11,3,65,18,12,17,26,27,19,14,15,22,21,23,29,31,30])).
% 75.59/75.65 cnf(7984,plain,
% 75.59/75.65 (P3(f3(a2,a2),f3(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[7916,7922,7924,7940,7942,7928,7926,7936,11,3,65,55,18,12,17,26,27,19,14,15,22,21,23,29,31,30,28])).
% 75.59/75.65 cnf(7988,plain,
% 75.59/75.65 (~P2(a4,a10,a7)),
% 75.59/75.65 inference(scs_inference,[],[7916,7922,7924,7940,7942,7928,7926,7936,11,3,35,65,55,18,12,17,26,27,19,14,15,22,21,23,29,31,30,28,6323,32])).
% 75.59/75.65 cnf(7990,plain,
% 75.59/75.65 (~P2(a4,a1,f6(a5))),
% 75.59/75.65 inference(scs_inference,[],[7916,7922,7924,7940,7942,7928,7926,7936,11,3,35,65,55,18,12,17,26,27,19,14,15,22,21,23,29,31,30,28,6323,32,3978])).
% 75.59/75.65 cnf(7996,plain,
% 75.59/75.65 (P2(a4,f8(a10,a10),f8(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[7930,5,12,18])).
% 75.59/75.65 cnf(7998,plain,
% 75.59/75.65 (P4(a1,f8(a10,a10),f8(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[7930,5,12,18,17])).
% 75.59/75.65 cnf(8000,plain,
% 75.59/75.65 (P4(a7,a1,a7)),
% 75.59/75.65 inference(scs_inference,[],[7976,7930,5,12,18,17,26])).
% 75.59/75.65 cnf(8002,plain,
% 75.59/75.65 (P4(f6(a7),a7,a1)),
% 75.59/75.65 inference(scs_inference,[],[7976,7930,5,12,18,17,26,19])).
% 75.59/75.65 cnf(8004,plain,
% 75.59/75.65 (P2(f8(a10,a10),a4,f8(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[7976,7930,5,12,18,17,26,19,27])).
% 75.59/75.65 cnf(8006,plain,
% 75.59/75.65 (P1(f3(a7,a7))),
% 75.59/75.65 inference(scs_inference,[],[7976,7930,5,12,18,17,26,19,27,14])).
% 75.59/75.65 cnf(8008,plain,
% 75.59/75.65 (P1(f8(a7,a7))),
% 75.59/75.65 inference(scs_inference,[],[7976,7930,5,12,18,17,26,19,27,14,15])).
% 75.59/75.65 cnf(8010,plain,
% 75.59/75.65 (P2(a7,a7,f8(a7,a7))),
% 75.59/75.65 inference(scs_inference,[],[7976,7930,5,12,18,17,26,19,27,14,15,22])).
% 75.59/75.65 cnf(8014,plain,
% 75.59/75.65 (P4(a7,a7,f3(a7,a7))),
% 75.59/75.65 inference(scs_inference,[],[7976,7930,5,12,18,17,26,19,27,14,15,22,83,21])).
% 75.59/75.65 cnf(8016,plain,
% 75.59/75.65 (P4(a1,f3(a2,a2),f3(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[7976,7984,7930,5,12,18,17,26,19,27,14,15,22,83,21,23])).
% 75.59/75.65 cnf(8020,plain,
% 75.59/75.65 (~P2(f9(a5),a1,a4)),
% 75.59/75.65 inference(scs_inference,[],[7976,7984,7930,7964,7684,2914,5,1090,261,12,18,17,26,19,27,14,15,22,83,21,23,29,32])).
% 75.59/75.65 cnf(8022,plain,
% 75.59/75.65 (P2(a2,f8(a7,a7),f8(a5,a7))),
% 75.59/75.65 inference(scs_inference,[],[7,7976,7984,7930,7964,7684,3808,2914,5,1090,261,12,18,17,26,19,27,14,15,22,83,21,23,29,32,31])).
% 75.59/75.65 cnf(8024,plain,
% 75.59/75.65 (~P4(a2,f6(a5),a2)),
% 75.59/75.65 inference(scs_inference,[],[7,7976,7984,7946,7930,7964,7966,7684,3808,2914,5,1090,261,12,18,17,26,19,27,14,15,22,83,21,23,29,32,31,30])).
% 75.59/75.65 cnf(8028,plain,
% 75.59/75.65 (P3(f3(a7,a7),f3(a7,a7))),
% 75.59/75.65 inference(scs_inference,[],[7,7976,7984,7946,7930,7964,7966,7684,3808,2914,5,1090,261,12,18,17,26,19,27,14,15,22,83,21,23,29,32,31,30,1177,70])).
% 75.59/75.65 cnf(8033,plain,
% 75.59/75.65 (P2(a4,f8(a2,a2),f8(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[7970,18])).
% 75.59/75.65 cnf(8037,plain,
% 75.59/75.65 (P4(a1,f8(a2,a2),f8(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[7970,2,18,12,17])).
% 75.59/75.65 cnf(8039,plain,
% 75.59/75.65 (P2(f8(a7,a7),a2,f8(a5,a7))),
% 75.59/75.65 inference(scs_inference,[],[7970,8022,2,18,12,17,27])).
% 75.59/75.65 cnf(8043,plain,
% 75.59/75.65 (P4(f6(a4),a4,a1)),
% 75.59/75.65 inference(scs_inference,[],[7960,7970,8022,2,18,12,17,27,26,19])).
% 75.59/75.65 cnf(8047,plain,
% 75.59/75.65 (P1(f8(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[7960,7970,8022,2,18,12,17,27,26,19,14,15])).
% 75.59/75.65 cnf(8049,plain,
% 75.59/75.65 (P2(a4,a4,f8(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[7960,7970,8022,2,18,12,17,27,26,19,14,15,22])).
% 75.59/75.65 cnf(8051,plain,
% 75.59/75.65 (P4(a4,a4,f3(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[7960,7970,8022,2,18,12,17,27,26,19,14,15,22,21])).
% 75.59/75.65 cnf(8053,plain,
% 75.59/75.65 (P4(a1,f3(a7,a7),f3(a7,a7))),
% 75.59/75.65 inference(scs_inference,[],[7960,8028,7970,8022,2,18,12,17,27,26,19,14,15,22,21,23])).
% 75.59/75.65 cnf(8055,plain,
% 75.59/75.65 (~P4(f6(a5),f6(a7),f6(a7))),
% 75.59/75.65 inference(scs_inference,[],[7960,8028,7970,8022,8002,7942,2,18,12,17,27,26,19,14,15,22,21,23,29])).
% 75.59/75.65 cnf(8057,plain,
% 75.59/75.65 (P2(f3(a10,a10),f8(a4,a4),f3(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[7960,7952,8028,7970,8022,8002,7942,2,18,12,17,27,26,19,14,15,22,21,23,29,31])).
% 75.59/75.65 cnf(8067,plain,
% 75.59/75.65 (P3(f3(a4,a4),f3(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[8000,7960,7952,8028,7970,8022,8002,7942,3772,9,2,3770,18,12,17,27,26,19,14,15,22,21,23,29,31,30,34,7907,24,72])).
% 75.59/75.65 cnf(8071,plain,
% 75.59/75.65 (P1(f6(a1))),
% 75.59/75.65 inference(scs_inference,[],[1,12])).
% 75.59/75.65 cnf(8073,plain,
% 75.59/75.65 (P2(a4,f3(a7,a7),f3(a7,a7))),
% 75.59/75.65 inference(scs_inference,[],[8006,1,12,18])).
% 75.59/75.65 cnf(8075,plain,
% 75.59/75.65 (P4(a1,f6(a10),f6(a10))),
% 75.59/75.65 inference(scs_inference,[],[8006,7914,1,12,18,17])).
% 75.59/75.65 cnf(8077,plain,
% 75.59/75.65 (P4(f6(a1),a1,a1)),
% 75.59/75.65 inference(scs_inference,[],[8006,7914,1,12,18,17,19])).
% 75.59/75.65 cnf(8081,plain,
% 75.59/75.65 (P4(f8(a10,a10),a1,f8(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[8057,7998,8006,7914,1,12,18,17,19,27,26])).
% 75.59/75.65 cnf(8083,plain,
% 75.59/75.65 (P1(f3(a1,a1))),
% 75.59/75.65 inference(scs_inference,[],[8057,7998,8006,7914,1,12,18,17,19,27,26,14])).
% 75.59/75.65 cnf(8085,plain,
% 75.59/75.65 (P1(f8(a1,a1))),
% 75.59/75.65 inference(scs_inference,[],[8057,7998,8006,7914,1,12,18,17,19,27,26,14,15])).
% 75.59/75.65 cnf(8087,plain,
% 75.59/75.65 (P2(a1,a1,f8(a1,a1))),
% 75.59/75.65 inference(scs_inference,[],[8057,7998,8006,7914,1,12,18,17,19,27,26,14,15,22])).
% 75.59/75.65 cnf(8089,plain,
% 75.59/75.65 (P4(a1,a1,f3(a1,a1))),
% 75.59/75.65 inference(scs_inference,[],[8057,7998,8006,7914,1,12,18,17,19,27,26,14,15,22,21])).
% 75.59/75.65 cnf(8091,plain,
% 75.59/75.65 (P4(a1,f3(a4,a4),f3(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[8057,8067,7998,8006,7914,1,12,18,17,19,27,26,14,15,22,21,23])).
% 75.59/75.65 cnf(8093,plain,
% 75.59/75.65 (~P4(f6(a5),f6(a4),f6(a4))),
% 75.59/75.65 inference(scs_inference,[],[8057,8067,7998,8006,7914,8043,7942,1,12,18,17,19,27,26,14,15,22,21,23,29])).
% 75.59/75.65 cnf(8095,plain,
% 75.59/75.65 (P2(f8(a10,a10),f8(a4,a4),f8(a10,a10))),
% 75.59/75.65 inference(scs_inference,[],[8004,8057,8067,7998,8006,7914,8049,8043,7942,1,12,18,17,19,27,26,14,15,22,21,23,29,31])).
% 75.59/75.65 cnf(8097,plain,
% 75.59/75.65 (P3(a1,f8(a1,a1))),
% 75.59/75.65 inference(scs_inference,[],[8004,8057,8067,7998,8006,7914,8049,8043,7942,1,39,12,18,17,19,27,26,14,15,22,21,23,29,31,25])).
% 75.59/75.65 cnf(8103,plain,
% 75.59/75.65 (P4(f8(a1,a1),f8(a1,a1),f8(a1,a1))),
% 75.59/75.65 inference(scs_inference,[],[8004,8057,8067,7998,8006,7914,8049,8043,8000,7942,8002,7136,1,39,12,18,17,19,27,26,14,15,22,21,23,29,31,25,30,16,33])).
% 75.59/75.65 cnf(8109,plain,
% 75.59/75.65 (P2(a4,f3(a1,a1),f3(a1,a1))),
% 75.59/75.65 inference(scs_inference,[],[8083,18])).
% 75.59/75.65 cnf(8111,plain,
% 75.59/75.65 (P1(f6(a5))),
% 75.59/75.65 inference(scs_inference,[],[8083,4,18,12])).
% 75.59/75.65 cnf(8113,plain,
% 75.59/75.65 (P4(a1,f3(a1,a1),f3(a1,a1))),
% 75.59/75.65 inference(scs_inference,[],[8083,4,18,12,17])).
% 75.59/75.65 cnf(8117,plain,
% 75.59/75.65 (P4(f6(a5),a5,a1)),
% 75.59/75.65 inference(scs_inference,[],[8053,8083,4,18,12,17,26,19])).
% 75.59/75.65 cnf(8121,plain,
% 75.59/75.65 (P1(f3(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8053,8095,8083,4,18,12,17,26,19,27,14])).
% 75.59/75.65 cnf(8123,plain,
% 75.59/75.65 (P1(f8(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8053,8095,8083,4,18,12,17,26,19,27,14,15])).
% 75.59/75.65 cnf(8125,plain,
% 75.59/75.65 (P2(a5,a5,f8(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8053,8095,8083,4,18,12,17,26,19,27,14,15,22])).
% 75.59/75.65 cnf(8127,plain,
% 75.59/75.65 (P4(a5,a5,f3(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8053,8095,8083,4,18,12,17,26,19,27,14,15,22,21])).
% 75.59/75.65 cnf(8129,plain,
% 75.59/75.65 (P4(a1,a4,a4)),
% 75.59/75.65 inference(scs_inference,[],[8053,8095,8083,4,48,18,12,17,26,19,27,14,15,22,21,23])).
% 75.59/75.65 cnf(8131,plain,
% 75.59/75.65 (P4(f6(a1),a10,a10)),
% 75.59/75.65 inference(scs_inference,[],[7920,8053,8095,8083,8077,4,48,18,12,17,26,19,27,14,15,22,21,23,29])).
% 75.59/75.65 cnf(8133,plain,
% 75.59/75.65 (~P2(f8(a4,a4),a10,a7)),
% 75.59/75.65 inference(scs_inference,[],[7920,7988,8053,8095,8083,8077,8049,7916,4,48,18,12,17,26,19,27,14,15,22,21,23,29,31])).
% 75.59/75.65 cnf(8135,plain,
% 75.59/75.65 (~P4(a1,a1,f6(a5))),
% 75.59/75.65 inference(scs_inference,[],[7920,7988,8053,8095,8083,7982,8075,8077,8049,7926,7916,4,48,18,12,17,26,19,27,14,15,22,21,23,29,31,30])).
% 75.59/75.65 cnf(8137,plain,
% 75.59/75.65 (P2(f3(a5,a5),f9(a5),f3(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[7920,7988,8053,8095,8083,8051,7982,8075,8077,8049,7926,7964,7916,4,48,18,12,17,26,19,27,14,15,22,21,23,29,31,30,34])).
% 75.59/75.65 cnf(8143,plain,
% 75.59/75.65 (P2(a4,f3(a5,a5),f3(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8121,18])).
% 75.59/75.65 cnf(8145,plain,
% 75.59/75.65 (P4(a1,f3(a5,a5),f3(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8121,18,17])).
% 75.59/75.65 cnf(8147,plain,
% 75.59/75.65 (P2(f9(a5),f3(a5,a5),f3(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[8121,8137,18,17,27])).
% 75.59/75.65 cnf(8149,plain,
% 75.59/75.65 (P4(a4,a1,a4)),
% 75.59/75.65 inference(scs_inference,[],[8129,8121,8137,18,17,27,26])).
% 75.59/75.65 cnf(8151,plain,
% 75.59/75.65 (P4(a1,a2,a2)),
% 75.59/75.65 inference(scs_inference,[],[8129,8121,8137,55,18,17,27,26,23])).
% 75.59/75.65 cnf(8155,plain,
% 75.59/75.65 (~P4(f6(a5),f3(a5,a5),a1)),
% 75.59/75.65 inference(scs_inference,[],[8129,8135,8121,8137,8127,8117,10,943,55,18,17,27,26,23,29,30])).
% 75.59/75.65 cnf(8162,plain,
% 75.59/75.65 (P4(a1,f8(a5,a5),f8(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8123,17])).
% 75.59/75.65 cnf(8164,plain,
% 75.59/75.65 (P2(a4,f8(a5,a5),f8(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8123,17,18])).
% 75.59/75.65 cnf(8166,plain,
% 75.59/75.65 (P2(f3(a5,a5),a4,f3(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8123,8143,17,18,27])).
% 75.59/75.65 cnf(8168,plain,
% 75.59/75.65 (P4(a2,a1,a2)),
% 75.59/75.65 inference(scs_inference,[],[8151,8123,8143,17,18,27,26])).
% 75.59/75.65 cnf(8170,plain,
% 75.59/75.65 (P4(f6(a1),a2,a2)),
% 75.59/75.65 inference(scs_inference,[],[8151,8123,8143,8077,17,18,27,26,29])).
% 75.59/75.65 cnf(8172,plain,
% 75.59/75.65 (P2(f8(a4,a4),f3(a5,a5),f3(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8151,8123,8143,8077,8049,17,18,27,26,29,32])).
% 75.59/75.65 cnf(8181,plain,
% 75.59/75.65 (P2(a4,f9(a5),f9(a5))),
% 75.59/75.65 inference(scs_inference,[],[7934,18])).
% 75.59/75.65 cnf(8183,plain,
% 75.59/75.65 (P4(a1,f9(a5),f9(a5))),
% 75.59/75.65 inference(scs_inference,[],[7934,18,17])).
% 75.59/75.65 cnf(8185,plain,
% 75.59/75.65 (P2(f3(a5,a5),f8(a4,a4),f3(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8172,7934,18,17,27])).
% 75.59/75.65 cnf(8187,plain,
% 75.59/75.65 (P4(f3(a2,a2),a1,f3(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[8172,8016,7934,18,17,27,26])).
% 75.59/75.65 cnf(8191,plain,
% 75.59/75.65 (P2(f8(a4,a4),f8(a5,a5),f8(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8172,8016,8164,8162,7934,8049,18,17,27,26,83,32])).
% 75.59/75.65 cnf(8193,plain,
% 75.59/75.65 (P4(f6(a1),f3(a2,a2),f3(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[8172,8016,8164,8162,7934,8077,8049,18,17,27,26,83,32,29])).
% 75.59/75.65 cnf(8195,plain,
% 75.59/75.65 (P2(a4,f3(a4,a4),f3(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[8172,8016,8147,8164,8162,7934,8077,8049,18,17,27,26,83,32,29,31])).
% 75.59/75.65 cnf(8197,plain,
% 75.59/75.65 (~P4(f6(a2),a2,f6(a5))),
% 75.59/75.65 inference(scs_inference,[],[8168,8172,8016,8147,8164,8162,7934,7966,8135,8077,8049,18,17,27,26,83,32,29,31,30])).
% 75.59/75.65 cnf(8203,plain,
% 75.59/75.65 (P4(a1,a1,f8(a1,a1))+~P4(a2,x82031,f8(a1,a1))+~P4(a2,x82031,a1)),
% 75.59/75.65 inference(scs_inference,[],[8168,8172,8016,8147,8164,8162,8145,7934,8097,7966,8135,8077,8049,39,18,17,27,26,83,32,29,31,30,28,23,73])).
% 75.59/75.65 cnf(8204,plain,
% 75.59/75.65 (P4(a1,f6(a2),f6(a2))),
% 75.59/75.65 inference(scs_inference,[],[7958,17])).
% 75.59/75.65 cnf(8206,plain,
% 75.59/75.65 (P2(a4,f6(a2),f6(a2))),
% 75.59/75.65 inference(scs_inference,[],[7958,17,18])).
% 75.59/75.65 cnf(8208,plain,
% 75.59/75.65 (P2(f8(a5,a5),f8(a4,a4),f8(a5,a5))),
% 75.59/75.65 inference(scs_inference,[],[8191,7958,17,18,27])).
% 75.59/75.65 cnf(8210,plain,
% 75.59/75.65 (P4(f3(a1,a1),a1,f3(a1,a1))),
% 75.59/75.65 inference(scs_inference,[],[8191,8113,7958,17,18,27,26])).
% 75.59/75.65 cnf(8212,plain,
% 75.59/75.65 (~P4(a1,f3(a1,a1),a5)),
% 75.59/75.65 inference(scs_inference,[],[8191,8113,7958,7726,8077,17,18,27,26,29])).
% 75.59/75.65 cnf(8223,plain,
% 75.59/75.65 (P2(a4,f3(a2,a2),f3(a2,a2))),
% 75.59/75.65 inference(scs_inference,[],[7968,18])).
% 75.59/75.65 cnf(8225,plain,
% 75.59/75.65 (P4(a1,f8(a7,a7),f8(a7,a7))),
% 75.59/75.65 inference(scs_inference,[],[7968,8008,18,17])).
% 75.59/75.65 cnf(8227,plain,
% 75.59/75.65 (P2(f3(a4,a4),a4,f3(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[8195,7968,8008,18,17,27])).
% 75.59/75.65 cnf(8229,plain,
% 75.59/75.65 (P4(f3(a4,a4),a1,f3(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[8091,8195,7968,8008,18,17,27,26])).
% 75.59/75.65 cnf(8231,plain,
% 75.59/75.65 (P2(f8(a4,a4),f3(a4,a4),f3(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[8091,8195,7968,8008,8049,18,17,27,26,32])).
% 75.59/75.65 cnf(8232,plain,
% 75.59/75.65 (~P2(x82321,x82322,x82323)+~P2(x82324,x82323,x82325)+P2(x82326,x82322,x82325)+~P2(x82324,x82321,x82326)),
% 75.59/75.65 inference(rename_variables,[],[32])).
% 75.59/75.65 cnf(8233,plain,
% 75.59/75.65 (P4(f6(a1),f3(a4,a4),f3(a4,a4))),
% 75.59/75.65 inference(scs_inference,[],[8091,8195,7968,8008,8049,8077,18,17,27,26,32,29])).
% 75.59/75.65 cnf(8235,plain,
% 75.59/75.65 (P4(f8(a4,a4),f8(a4,a4),f3(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8091,8195,7968,8008,8051,8049,8077,18,17,27,26,32,29,33])).
% 75.59/75.66 cnf(8239,plain,
% 75.59/75.66 (~P2(f9(a5),a2,x82391)+P2(x82391,a7,a4)),
% 75.59/75.66 inference(scs_inference,[],[7,8091,8195,7968,8008,8170,7918,8051,7936,8117,8049,8077,8,18,17,27,26,32,29,33,34,8232])).
% 75.59/75.66 cnf(8246,plain,
% 75.59/75.66 (P4(a1,f8(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8047,17])).
% 75.59/75.66 cnf(8248,plain,
% 75.59/75.66 (P2(a4,f8(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8047,17,18])).
% 75.59/75.66 cnf(8250,plain,
% 75.59/75.66 (P2(f3(a4,a4),f8(a4,a4),f3(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8231,8047,17,18,27])).
% 75.59/75.66 cnf(8252,plain,
% 75.59/75.66 (P4(f3(a4,a4),f6(a1),f3(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8231,8233,8047,17,18,27,26])).
% 75.59/75.66 cnf(8254,plain,
% 75.59/75.66 (P2(f8(a4,a4),f3(a2,a2),f3(a2,a2))),
% 75.59/75.66 inference(scs_inference,[],[8231,8233,8223,8047,8049,17,18,27,26,32])).
% 75.59/75.66 cnf(8255,plain,
% 75.59/75.66 (~P2(x82551,x82552,x82553)+P2(x82554,x82555,x82553)+~P2(x82556,x82555,x82552)+~P2(x82551,x82556,x82554)),
% 75.59/75.66 inference(rename_variables,[],[32])).
% 75.59/75.66 cnf(8256,plain,
% 75.59/75.66 (P4(f6(a1),f8(a7,a7),f8(a7,a7))),
% 75.59/75.66 inference(scs_inference,[],[8231,8233,8223,8225,8047,8077,8049,17,18,27,26,32,29])).
% 75.59/75.66 cnf(8258,plain,
% 75.59/75.66 (P2(f9(a5),a4,f9(a5))),
% 75.59/75.66 inference(scs_inference,[],[8231,8233,8223,8225,8047,8181,7936,7964,8077,8049,17,18,27,26,32,29,31])).
% 75.59/75.66 cnf(8260,plain,
% 75.59/75.66 (P2(f3(a2,a2),a7,f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[7,8231,8233,8223,8225,8047,8181,7974,7936,8127,7964,8077,8049,17,18,27,26,32,29,31,34])).
% 75.59/75.66 cnf(8262,plain,
% 75.59/75.66 (~P2(a2,x82621,a4)+~P2(x82621,a1,a7)),
% 75.59/75.66 inference(scs_inference,[],[7,8231,8233,8223,8225,8047,8181,7974,7936,7684,8127,7964,8077,8049,17,18,27,26,32,29,31,34,8255])).
% 75.59/75.66 cnf(8266,plain,
% 75.59/75.66 (P2(a4,f6(a1),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[8071,18])).
% 75.59/75.66 cnf(8268,plain,
% 75.59/75.66 (P4(a1,f8(a1,a1),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8071,8085,18,17])).
% 75.59/75.66 cnf(8270,plain,
% 75.59/75.66 (P2(f3(a2,a2),f8(a4,a4),f3(a2,a2))),
% 75.59/75.66 inference(scs_inference,[],[8254,8071,8085,18,17,27])).
% 75.59/75.66 cnf(8274,plain,
% 75.59/75.66 (~P4(a1,f6(a5),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[8254,8256,8071,8085,7946,8077,3660,18,17,27,26,29])).
% 75.59/75.66 cnf(8276,plain,
% 75.59/75.66 (~P2(a4,a5,a1)),
% 75.59/75.66 inference(scs_inference,[],[8254,8256,8071,8085,8258,8020,7946,7936,8077,3660,18,17,27,26,29,31])).
% 75.59/75.66 cnf(8284,plain,
% 75.59/75.66 (P2(a4,f6(a5),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8111,18])).
% 75.59/75.66 cnf(8286,plain,
% 75.59/75.66 (P2(a7,f3(a2,a2),f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8260,8111,18,27])).
% 75.59/75.66 cnf(8288,plain,
% 75.59/75.66 (P4(f8(a1,a1),a1,f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8260,8268,8111,18,27,26])).
% 75.59/75.66 cnf(8290,plain,
% 75.59/75.66 (P2(f8(a4,a4),f3(a7,a7),f3(a7,a7))),
% 75.59/75.66 inference(scs_inference,[],[8260,8268,8073,8111,8049,18,27,26,32])).
% 75.59/75.66 cnf(8292,plain,
% 75.59/75.66 (P4(f6(a1),f8(a1,a1),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8260,8268,8073,8111,8049,8077,18,27,26,32,29])).
% 75.59/75.66 cnf(8299,plain,
% 75.59/75.66 (P2(a4,f6(a10),f6(a10))),
% 75.59/75.66 inference(scs_inference,[],[7914,18])).
% 75.59/75.66 cnf(8303,plain,
% 75.59/75.66 (P4(f8(a1,a1),f6(a1),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8290,8292,7914,18,27,26])).
% 75.59/75.66 cnf(8307,plain,
% 75.59/75.66 (P2(f8(a4,a4),f3(a1,a1),f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8290,8292,8183,8109,7914,8049,18,27,26,83,32])).
% 75.59/75.66 cnf(8309,plain,
% 75.59/75.66 (P4(f6(a1),f9(a5),f9(a5))),
% 75.59/75.66 inference(scs_inference,[],[8290,8292,8183,8109,7914,8049,8077,18,27,26,83,32,29])).
% 75.59/75.66 cnf(8313,plain,
% 75.59/75.66 (~P2(a1,a4,f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8290,8292,8183,8109,8093,2750,7914,8049,8077,1353,3770,18,27,26,83,32,29,28,33])).
% 75.59/75.66 cnf(8320,plain,
% 75.59/75.66 (P2(a4,f8(a7,a7),f8(a7,a7))),
% 75.59/75.66 inference(scs_inference,[],[8008,18])).
% 75.59/75.66 cnf(8322,plain,
% 75.59/75.66 (P2(f3(a1,a1),f8(a4,a4),f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8307,8008,18,27])).
% 75.59/75.66 cnf(8324,plain,
% 75.59/75.66 (P4(f9(a5),f6(a1),f9(a5))),
% 75.59/75.66 inference(scs_inference,[],[8307,8309,8008,18,27,26])).
% 75.59/75.66 cnf(8326,plain,
% 75.59/75.66 (~P4(f3(a1,a1),f6(a1),a4)),
% 75.59/75.66 inference(scs_inference,[],[8307,8309,8089,8008,5596,2749,18,27,26,29])).
% 75.59/75.66 cnf(8328,plain,
% 75.59/75.66 (~P2(f9(a5),f8(a5,a5),a1)),
% 75.59/75.66 inference(scs_inference,[],[8276,8307,8309,8089,8008,8125,7936,5596,2749,18,27,26,29,32])).
% 75.59/75.66 cnf(8340,plain,
% 75.59/75.66 (P2(f8(a7,a7),a4,f8(a7,a7))),
% 75.59/75.66 inference(scs_inference,[],[8320,27])).
% 75.59/75.66 cnf(8342,plain,
% 75.59/75.66 (P2(a4,f8(a1,a1),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8320,8085,27,18])).
% 75.59/75.66 cnf(8346,plain,
% 75.59/75.66 (P2(f9(a5),f8(a4,a4),f9(a5))),
% 75.59/75.66 inference(scs_inference,[],[8320,8204,8258,8085,8049,27,18,26,31])).
% 75.59/75.66 cnf(8348,plain,
% 75.59/75.66 (P4(f6(a1),f6(a2),f6(a2))),
% 75.59/75.66 inference(scs_inference,[],[8320,8204,8258,8085,8049,8077,27,18,26,31,29])).
% 75.59/75.66 cnf(8350,plain,
% 75.59/75.66 (P2(f8(a4,a4),f8(a7,a7),f8(a7,a7))),
% 75.59/75.66 inference(scs_inference,[],[8320,8204,8258,8085,8049,8077,27,18,26,31,29,32])).
% 75.59/75.66 cnf(8352,plain,
% 75.59/75.66 (~P4(f6(a1),f6(a5),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[8274,8320,8204,8258,8085,8049,8077,943,27,18,26,31,29,32,30])).
% 75.59/75.66 cnf(8354,plain,
% 75.59/75.66 (P2(f3(a4,a4),f8(a1,a1),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8274,8320,8204,8103,8258,8085,8051,8049,8077,943,27,18,26,31,29,32,30,34])).
% 75.59/75.66 cnf(8360,plain,
% 75.59/75.66 (P2(a4,a2,a2)),
% 75.59/75.66 inference(scs_inference,[],[3,18])).
% 75.59/75.66 cnf(8362,plain,
% 75.59/75.66 (P2(f8(a1,a1),f3(a4,a4),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8354,3,18,27])).
% 75.59/75.66 cnf(8364,plain,
% 75.59/75.66 (P4(f6(a2),f6(a1),f6(a2))),
% 75.59/75.66 inference(scs_inference,[],[8354,8348,3,18,27,26])).
% 75.59/75.66 cnf(8368,plain,
% 75.59/75.66 (P2(f8(a4,a4),f6(a1),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[8354,8266,8340,8348,8049,3,18,27,26,31,32])).
% 75.59/75.66 cnf(8370,plain,
% 75.59/75.66 (P4(f6(a1),f3(a10,a10),f3(a10,a10))),
% 75.59/75.66 inference(scs_inference,[],[8354,8266,8340,8348,7938,8131,8049,3,18,27,26,31,32,29])).
% 75.59/75.66 cnf(8372,plain,
% 75.59/75.66 (~P4(f6(a1),f6(a5),a1)),
% 75.59/75.66 inference(scs_inference,[],[8354,8266,8340,8348,7938,8131,7946,8049,8077,3,943,18,27,26,31,32,29,30])).
% 75.59/75.66 cnf(8376,plain,
% 75.59/75.66 (P4(a1,a4,a1)+P1(f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[8354,8266,8340,8348,8352,7938,8131,8149,7946,8049,8077,3,2,943,18,27,26,31,32,29,30,33,20])).
% 75.59/75.66 cnf(8382,plain,
% 75.59/75.66 (P2(a2,a4,a2)),
% 75.59/75.66 inference(scs_inference,[],[8360,27])).
% 75.59/75.66 cnf(8384,plain,
% 75.59/75.66 (P2(a4,a7,a7)),
% 75.59/75.66 inference(scs_inference,[],[8360,5,27,18])).
% 75.59/75.66 cnf(8388,plain,
% 75.59/75.66 (~P2(f8(a4,a4),a5,a1)),
% 75.59/75.66 inference(scs_inference,[],[8360,8370,8346,8020,7936,5,27,18,26,31])).
% 75.59/75.66 cnf(8390,plain,
% 75.59/75.66 (~P4(a5,f6(a10),f6(a10))),
% 75.59/75.66 inference(scs_inference,[],[8360,8370,8346,8020,7926,7936,37,5,27,18,26,31,29])).
% 75.59/75.66 cnf(8392,plain,
% 75.59/75.66 (~P4(f6(a1),a1,f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8360,8370,8346,8197,8348,8020,7926,7966,7936,37,5,27,18,26,31,29,30])).
% 75.59/75.66 cnf(8394,plain,
% 75.59/75.66 (~P2(a1,a2,f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8360,8370,8346,8197,7944,8348,8020,7920,7926,7966,8117,7936,37,3760,5,27,18,26,31,29,30,34])).
% 75.59/75.66 cnf(8400,plain,
% 75.59/75.66 (P2(a4,a4,a4)),
% 75.59/75.66 inference(scs_inference,[],[2,18])).
% 75.59/75.66 cnf(8402,plain,
% 75.59/75.66 (P2(a7,a4,a7)),
% 75.59/75.66 inference(scs_inference,[],[8384,2,18,27])).
% 75.59/75.66 cnf(8404,plain,
% 75.59/75.66 (P4(f3(a2,a2),f6(a1),f3(a2,a2))),
% 75.59/75.66 inference(scs_inference,[],[8384,8193,2,18,27,26])).
% 75.59/75.66 cnf(8408,plain,
% 75.59/75.66 (P2(a2,f8(a4,a4),a2)),
% 75.59/75.66 inference(scs_inference,[],[8382,8384,8193,8225,8049,2,18,27,26,83,31])).
% 75.59/75.66 cnf(8410,plain,
% 75.59/75.66 (P2(f8(a4,a4),a7,a7)),
% 75.59/75.66 inference(scs_inference,[],[8382,8384,8193,8225,8049,2,18,27,26,83,31,32])).
% 75.59/75.66 cnf(8412,plain,
% 75.59/75.66 (P4(f6(a1),f8(a2,a2),f8(a2,a2))),
% 75.59/75.66 inference(scs_inference,[],[8382,8384,8193,8037,8225,8077,8049,2,18,27,26,83,31,32,29])).
% 75.59/75.66 cnf(8414,plain,
% 75.59/75.66 (P2(f3(a1,a1),a1,f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8382,8384,8193,8037,8087,8225,8103,8089,8077,8049,2,18,27,26,83,31,32,29,34])).
% 75.59/75.66 cnf(8416,plain,
% 75.59/75.66 (P2(a5,f8(a4,a4),a5)),
% 75.59/75.66 inference(scs_inference,[],[8382,8384,8193,8037,8087,8225,8103,8089,8077,8049,2,18,27,26,83,31,32,29,34,213])).
% 75.59/75.66 cnf(8422,plain,
% 75.59/75.66 (P2(f8(a1,a1),a4,f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8342,27])).
% 75.59/75.66 cnf(8424,plain,
% 75.59/75.66 (P2(a4,a1,a1)),
% 75.59/75.66 inference(scs_inference,[],[8342,1,27,18])).
% 75.59/75.66 cnf(8428,plain,
% 75.59/75.66 (P2(f8(a1,a1),f8(a4,a4),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8362,8250,8342,8412,1,27,18,26,32])).
% 75.59/75.66 cnf(8432,plain,
% 75.59/75.66 (P4(f6(a1),f8(a5,a5),f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8362,8250,8342,8412,8388,8410,8162,8077,3763,1,27,18,26,32,31,29])).
% 75.59/75.66 cnf(8434,plain,
% 75.59/75.66 (P4(a1,f8(a1,a1),a1)),
% 75.59/75.66 inference(scs_inference,[],[8362,8250,8342,8412,8388,8410,8162,8087,8149,8077,3763,1,27,18,26,32,31,29,33])).
% 75.59/75.66 cnf(8438,plain,
% 75.59/75.66 (~P4(a1,f8(a1,a1),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8362,8250,8342,8412,8388,8410,8288,8162,8135,8087,8149,8077,3763,3,1,27,18,26,32,31,29,33,24,30])).
% 75.59/75.66 cnf(8447,plain,
% 75.59/75.66 (P2(a1,a4,a1)),
% 75.59/75.66 inference(scs_inference,[],[8424,27])).
% 75.59/75.66 cnf(8449,plain,
% 75.59/75.66 (P4(f8(a1,a1),a1,a1)),
% 75.59/75.66 inference(scs_inference,[],[8424,8434,27,26])).
% 75.59/75.66 cnf(8451,plain,
% 75.59/75.66 (~P4(a1,f6(a1),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8424,8434,8438,8303,27,26,29])).
% 75.59/75.66 cnf(8455,plain,
% 75.59/75.66 (~P2(a5,a1,f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8402,8424,8434,8438,8328,8303,7980,8410,7936,27,26,29,32,31])).
% 75.59/75.66 cnf(8457,plain,
% 75.59/75.66 (~P4(f6(a1),f8(a1,a1),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8402,8424,8434,8438,8328,8303,7980,8410,8268,7936,8077,27,26,29,32,31,30])).
% 75.59/75.66 cnf(8461,plain,
% 75.59/75.66 (~P4(a10,a1,a7)),
% 75.59/75.66 inference(scs_inference,[],[8402,8424,8434,8438,8328,8303,7980,8410,7924,8268,7922,8051,8135,7936,8077,27,26,29,32,31,30,33,34])).
% 75.59/75.66 cnf(8468,plain,
% 75.59/75.66 (P2(f8(a4,a4),f8(a1,a1),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8428,27])).
% 75.59/75.66 cnf(8472,plain,
% 75.59/75.66 (~P4(f6(a5),f8(a1,a1),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8428,8432,8449,7942,27,26,29])).
% 75.59/75.66 cnf(8474,plain,
% 75.59/75.66 (~P2(a4,f6(a5),a1)),
% 75.59/75.66 inference(scs_inference,[],[8428,8432,8449,8400,8284,7990,7942,27,26,29,31])).
% 75.59/75.66 cnf(8476,plain,
% 75.59/75.66 (P2(f8(a5,a7),f8(a4,a4),f8(a5,a7))),
% 75.59/75.66 inference(scs_inference,[],[8428,8432,8039,8449,8408,8400,8284,7990,7942,27,26,29,31,32])).
% 75.59/75.66 cnf(8478,plain,
% 75.59/75.66 (~P4(f6(a1),a10,a7)),
% 75.59/75.66 inference(scs_inference,[],[8461,8428,8432,8039,8449,8408,8400,8284,7990,8131,7924,7942,27,26,29,31,32,30])).
% 75.59/75.66 cnf(8480,plain,
% 75.59/75.66 (~P4(f8(a1,a1),a1,f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8461,8428,8432,8039,8449,8408,8400,8284,7990,8131,8129,7924,8424,8087,7942,27,26,29,31,32,30,34])).
% 75.59/75.66 cnf(8488,plain,
% 75.59/75.66 (P4(f3(a5,a5),a1,f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8033,8145,27,26])).
% 75.59/75.66 cnf(8490,plain,
% 75.59/75.66 (~P4(f6(a1),f6(a5),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8033,8372,8449,8145,3660,27,26,29])).
% 75.59/75.66 cnf(8494,plain,
% 75.59/75.66 (~P2(a5,f8(a4,a4),a1)),
% 75.59/75.66 inference(scs_inference,[],[8208,8033,8372,8455,8416,8449,8145,8125,3660,27,26,29,32,31])).
% 75.59/75.66 cnf(8496,plain,
% 75.59/75.66 (~P4(a7,a1,a10)),
% 75.59/75.66 inference(scs_inference,[],[8447,8208,8033,8372,8455,8416,8402,8449,8145,8000,8125,35,3660,27,26,29,32,31,34])).
% 75.59/75.66 cnf(8501,plain,
% 75.59/75.66 (P2(f6(a2),a4,f6(a2))),
% 75.59/75.66 inference(scs_inference,[],[8206,27])).
% 75.59/75.66 cnf(8503,plain,
% 75.59/75.66 (P4(f8(a4,a4),a1,f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8206,8246,27,26])).
% 75.59/75.66 cnf(8507,plain,
% 75.59/75.66 (~P2(a5,a4,a1)),
% 75.59/75.66 inference(scs_inference,[],[8496,8206,8494,8447,8246,8449,7924,8049,27,26,29,31])).
% 75.59/75.66 cnf(8516,plain,
% 75.59/75.66 (P2(a1,f3(a1,a1),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8414,27])).
% 75.59/75.66 cnf(8520,plain,
% 75.59/75.66 (P4(f8(a1,a1),f3(a7,a7),f3(a7,a7))),
% 75.59/75.66 inference(scs_inference,[],[8414,8053,8075,8449,27,26,29])).
% 75.59/75.66 cnf(8522,plain,
% 75.59/75.66 (~P4(f6(a5),a1,f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8414,8472,8053,8075,8434,8449,3660,27,26,29,30])).
% 75.59/75.66 cnf(8524,plain,
% 75.59/75.66 (P2(f8(a2,a2),f8(a4,a4),f8(a2,a2))),
% 75.59/75.66 inference(scs_inference,[],[8414,8472,8408,8053,8075,7972,8434,8449,3660,27,26,29,30,32])).
% 75.59/75.66 cnf(8526,plain,
% 75.59/75.66 (P2(a2,f8(a5,a10),f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[7,8414,8472,8408,8053,8075,7972,8434,8449,8125,3858,3660,27,26,29,30,32,31])).
% 75.59/75.66 cnf(8528,plain,
% 75.59/75.66 (~P2(a1,f6(a5),a5)),
% 75.59/75.66 inference(scs_inference,[],[7,8414,8472,8474,8408,8053,8075,8284,7972,8434,8449,8149,8125,8117,3858,3660,27,26,29,30,32,31,34])).
% 75.59/75.66 cnf(8543,plain,
% 75.59/75.66 (P4(f6(a1),f3(a7,a7),f3(a7,a7))),
% 75.59/75.66 inference(scs_inference,[],[8520,8524,8292,27,26,29])).
% 75.59/75.66 cnf(8547,plain,
% 75.59/75.66 (~P2(f8(a5,a5),f9(a5),a1)),
% 75.59/75.66 inference(scs_inference,[],[7,8507,8520,8524,8526,8455,8292,7964,8125,27,26,29,32,31])).
% 75.59/75.66 cnf(8549,plain,
% 75.59/75.66 (~P2(a1,a5,f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[7,8507,8520,8524,8526,8455,8276,8292,8129,7964,8125,8117,363,27,26,29,32,31,34])).
% 75.59/75.66 cnf(8558,plain,
% 75.59/75.66 (~P4(f8(a1,a1),f8(a1,a1),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8476,8480,8543,8288,8434,27,26,29])).
% 75.59/75.66 cnf(8562,plain,
% 75.59/75.66 (~P2(a1,f9(a5),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[7,8476,8480,8543,8388,8288,8447,8360,7684,8434,7936,27,26,29,31,32])).
% 75.59/75.66 cnf(8564,plain,
% 75.59/75.66 (~P4(f8(a1,a1),f3(a1,a1),a5)),
% 75.59/75.66 inference(scs_inference,[],[7,8476,8480,8543,8212,8388,8288,8447,8113,8360,7684,8434,8449,7936,27,26,29,31,32,30])).
% 75.59/75.66 cnf(8566,plain,
% 75.59/75.66 (~P2(a1,f6(a10),a5)),
% 75.59/75.66 inference(scs_inference,[],[7,8476,8480,8543,8299,8390,8212,8388,8288,8447,8113,8360,7684,8434,8129,8449,7936,27,26,29,31,32,30,33])).
% 75.59/75.66 cnf(8573,plain,
% 75.59/75.66 (P2(f6(a1),f8(a4,a4),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[8368,27])).
% 75.59/75.66 cnf(8575,plain,
% 75.59/75.66 (P4(f8(a5,a5),a1,f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8368,8162,27,26])).
% 75.59/75.66 cnf(8577,plain,
% 75.59/75.66 (P4(f8(a1,a1),f3(a10,a10),f3(a10,a10))),
% 75.59/75.66 inference(scs_inference,[],[8368,7960,8162,8449,27,26,29])).
% 75.59/75.66 cnf(8579,plain,
% 75.59/75.66 (P2(f8(a5,a7),a2,f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8368,7960,8162,8449,8125,3808,3763,27,26,29,32])).
% 75.59/75.66 cnf(8581,plain,
% 75.59/75.66 (~P4(a1,a10,a7)),
% 75.59/75.66 inference(scs_inference,[],[8478,8368,7960,8162,8131,8449,8125,3808,3763,2749,27,26,29,32,30])).
% 75.59/75.66 cnf(8583,plain,
% 75.59/75.66 (P2(a2,f8(a7,a7),f8(a5,a10))),
% 75.59/75.66 inference(scs_inference,[],[7,8478,8368,8010,7960,8162,8131,8449,8125,3808,3859,3763,2749,27,26,29,32,30,31])).
% 75.59/75.66 cnf(8585,plain,
% 75.59/75.66 (P2(f3(a1,a1),f3(a1,a1),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[7,8478,8368,8516,8010,7960,8162,8103,8089,8131,8449,8125,3808,3859,3763,2749,27,26,29,32,30,31,34])).
% 75.59/75.66 cnf(8589,plain,
% 75.59/75.66 (P2(a2,f8(a5,a7),f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8579,27])).
% 75.59/75.66 cnf(8595,plain,
% 75.59/75.66 (~P4(f6(a10),f3(a10,a10),a7)),
% 75.59/75.66 inference(scs_inference,[],[8581,8577,8490,8579,8303,7938,8292,7926,27,26,29,30])).
% 75.59/75.66 cnf(8597,plain,
% 75.59/75.66 (P2(f8(a7,a7),f8(a2,a2),f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8581,8577,8490,8579,8303,7938,8039,8292,7972,7926,27,26,29,30,31])).
% 75.59/75.66 cnf(8601,plain,
% 75.59/75.66 (~P2(f8(a1,a1),f8(a4,a4),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[7,8581,8577,8457,8490,8573,8579,8428,8303,7938,8039,8455,8292,7972,7926,27,26,29,30,31,32,33])).
% 75.59/75.66 cnf(8605,plain,
% 75.59/75.66 (P2(f8(a2,a2),f8(a7,a7),f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8597,27])).
% 75.59/75.66 cnf(8609,plain,
% 75.59/75.66 (~P4(f3(a1,a1),f6(a1),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8597,8451,8037,8089,2749,27,26,29])).
% 75.59/75.66 cnf(8613,plain,
% 75.59/75.66 (~P4(f8(a1,a1),a10,a7)),
% 75.59/75.66 inference(scs_inference,[],[8597,8562,8451,8248,8581,8346,8037,7920,8089,8449,2749,27,26,29,31,30])).
% 75.59/75.66 cnf(8619,plain,
% 75.59/75.66 (P2(f3(a2,a2),a4,f3(a2,a2))),
% 75.59/75.66 inference(scs_inference,[],[8597,8394,8422,8558,8562,8451,8248,8382,8581,8346,8579,8037,7920,7974,8103,8089,8449,2749,27,26,29,31,30,33,32,34])).
% 75.59/75.66 cnf(8621,plain,
% 75.59/75.66 (P2(f8(a7,a7),a2,f8(a5,a10))),
% 75.59/75.66 inference(scs_inference,[],[8583,27])).
% 75.59/75.66 cnf(8623,plain,
% 75.59/75.66 (P4(f9(a5),a1,f9(a5))),
% 75.59/75.66 inference(scs_inference,[],[8583,8183,27,26])).
% 75.59/75.66 cnf(8625,plain,
% 75.59/75.66 (P4(f8(a1,a1),f8(a10,a10),f8(a10,a10))),
% 75.59/75.66 inference(scs_inference,[],[8583,7998,8183,8449,27,26,29])).
% 75.59/75.66 cnf(8629,plain,
% 75.59/75.66 (P2(f8(a5,a5),a4,f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8605,8522,8583,8340,7998,8183,8089,8449,3660,27,26,29,30,32])).
% 75.59/75.66 cnf(8631,plain,
% 75.59/75.66 (~P2(a4,f3(a1,a1),a5)),
% 75.59/75.66 inference(scs_inference,[],[8605,8564,8522,8583,8109,8340,8516,7998,8183,8089,8129,8449,3660,27,26,29,30,32,33])).
% 75.59/75.66 cnf(8637,plain,
% 75.59/75.66 (P2(f3(a7,a7),a4,f3(a7,a7))),
% 75.59/75.66 inference(scs_inference,[],[8073,27])).
% 75.59/75.66 cnf(8641,plain,
% 75.59/75.66 (P4(f8(a1,a1),f3(a5,a5),f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8625,8073,8145,8449,27,26,29])).
% 75.59/75.66 cnf(8645,plain,
% 75.59/75.66 (~P2(a1,a5,f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8625,8547,8631,8073,8307,8248,8145,8447,7964,8449,27,26,29,31,32])).
% 75.59/75.66 cnf(8650,plain,
% 75.59/75.66 (P2(f8(a5,a10),a2,f8(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8526,27])).
% 75.59/75.66 cnf(8652,plain,
% 75.59/75.66 (P4(f3(a5,a5),f8(a1,a1),f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8641,8526,27,26])).
% 75.59/75.66 cnf(8656,plain,
% 75.59/75.66 (~P2(f3(a1,a1),f3(a1,a1),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8641,8322,8601,8585,8526,8581,7920,8089,27,26,29,32])).
% 75.59/75.66 cnf(8660,plain,
% 75.59/75.66 (~P2(a2,a7,f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[7,8641,8322,8392,8601,8585,8526,8631,8581,7920,8360,8089,3666,27,26,29,32,30,31])).
% 75.59/75.66 cnf(8666,plain,
% 75.59/75.66 (P2(f3(a1,a1),a4,f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8109,27])).
% 75.59/75.66 cnf(8668,plain,
% 75.59/75.66 (P4(a2,f6(a1),a2)),
% 75.59/75.66 inference(scs_inference,[],[8109,8170,27,26])).
% 75.59/75.66 cnf(8670,plain,
% 75.59/75.66 (P4(f8(a1,a1),f8(a7,a7),f8(a7,a7))),
% 75.59/75.66 inference(scs_inference,[],[8109,8225,8170,8449,27,26,29])).
% 75.59/75.66 cnf(8672,plain,
% 75.59/75.66 (~P4(f8(a1,a1),f3(a1,a1),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8480,8109,8288,8225,8170,8089,8449,27,26,29,30])).
% 75.59/75.66 cnf(8674,plain,
% 75.59/75.66 (P2(a4,f8(a4,a4),a4)),
% 75.59/75.66 inference(scs_inference,[],[8480,8109,8416,8288,8225,8170,8089,7936,8449,27,26,29,30,32])).
% 75.59/75.66 cnf(8676,plain,
% 75.59/75.66 (P2(f8(a4,a4),f8(a5,a10),f8(a5,a10))),
% 75.59/75.66 inference(scs_inference,[],[8350,8621,8480,8109,8416,8288,8225,8170,8089,7936,8449,27,26,29,30,32,31])).
% 75.59/75.66 cnf(8684,plain,
% 75.59/75.66 (P2(f8(a5,a10),f8(a4,a4),f8(a5,a10))),
% 75.59/75.66 inference(scs_inference,[],[8676,27])).
% 75.59/75.66 cnf(8690,plain,
% 75.59/75.66 (P2(f6(a2),f8(a4,a4),f6(a2))),
% 75.59/75.66 inference(scs_inference,[],[8670,8676,8674,8668,8024,8501,27,26,29,32])).
% 75.59/75.66 cnf(8692,plain,
% 75.59/75.66 (~P2(a5,a4,f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[7,8670,8676,8660,8674,8668,8024,8501,8402,27,26,29,32,31])).
% 75.59/75.66 cnf(8703,plain,
% 75.59/75.66 (P4(a10,f6(a1),a10)),
% 75.59/75.66 inference(scs_inference,[],[8690,8131,27,26])).
% 75.59/75.66 cnf(8705,plain,
% 75.59/75.66 (~P4(f6(a2),a2,a4)),
% 75.59/75.66 inference(scs_inference,[],[8690,8348,5597,8131,7966,27,26,29])).
% 75.59/75.66 cnf(8709,plain,
% 75.59/75.66 (~P2(f8(a4,a4),f8(a1,a1),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8656,8690,8474,8674,8585,8307,8348,5597,8424,8131,7966,27,26,29,31,32])).
% 75.59/75.66 cnf(8718,plain,
% 75.59/75.66 (P2(f6(a1),a4,f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[8266,27])).
% 75.59/75.66 cnf(8720,plain,
% 75.59/75.66 (P4(a2,f6(a2),a1)),
% 75.59/75.66 inference(scs_inference,[],[8266,7966,27,26])).
% 75.59/75.66 cnf(8722,plain,
% 75.59/75.66 (P4(f8(a1,a1),f3(a2,a2),f3(a2,a2))),
% 75.59/75.66 inference(scs_inference,[],[8266,8016,7966,8449,27,26,29])).
% 75.59/75.66 cnf(8724,plain,
% 75.59/75.66 (~P4(a1,a7,a10)),
% 75.59/75.66 inference(scs_inference,[],[8461,8266,8016,8000,7976,7966,8449,27,26,29,30])).
% 75.59/75.66 cnf(8737,plain,
% 75.59/75.66 (P2(f6(a10),a4,f6(a10))),
% 75.59/75.66 inference(scs_inference,[],[8299,27])).
% 75.59/75.66 cnf(8739,plain,
% 75.59/75.66 (P4(f3(a2,a2),f8(a1,a1),f3(a2,a2))),
% 75.59/75.66 inference(scs_inference,[],[8722,8299,27,26])).
% 75.59/75.66 cnf(8741,plain,
% 75.59/75.66 (P4(f8(a1,a1),f8(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8722,8299,8246,8449,27,26,29])).
% 75.59/75.66 cnf(8743,plain,
% 75.59/75.66 (~P2(f8(a5,a5),f9(a5),f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8722,8692,8299,8246,8125,7964,8449,27,26,29,31])).
% 75.59/75.66 cnf(8747,plain,
% 75.59/75.66 (~P2(f3(a1,a1),a4,a5)),
% 75.59/75.66 inference(scs_inference,[],[8722,8692,8720,8666,8451,8364,8212,8299,8246,8113,8447,8125,7964,8449,27,26,29,31,30,33])).
% 75.59/75.66 cnf(8751,plain,
% 75.59/75.66 (P2(f8(a4,a4),a4,f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8722,8692,8720,8666,8451,8364,8212,8299,8246,8400,8113,8447,8125,7964,8449,8049,27,26,29,31,30,33,8203,32])).
% 75.59/75.66 cnf(8755,plain,
% 75.59/75.66 (P2(f8(a4,a4),f9(a5),f9(a5))),
% 75.59/75.66 inference(scs_inference,[],[8346,27])).
% 75.59/75.66 cnf(8757,plain,
% 75.59/75.66 (P4(f8(a4,a4),f8(a1,a1),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8741,8346,27,26])).
% 75.59/75.66 cnf(8774,plain,
% 75.59/75.66 (P2(f8(a4,a4),a2,a2)),
% 75.59/75.66 inference(scs_inference,[],[8408,27])).
% 75.59/75.66 cnf(8776,plain,
% 75.59/75.66 (P4(a10,f6(a10),a1)),
% 75.59/75.66 inference(scs_inference,[],[8408,7926,27,26])).
% 75.59/75.66 cnf(8782,plain,
% 75.59/75.66 (P2(f8(a4,a4),a4,a4)),
% 75.59/75.66 inference(scs_inference,[],[8613,8755,8720,8408,8000,7942,7926,7936,27,26,29,30,31])).
% 75.59/75.66 cnf(8784,plain,
% 75.59/75.66 (~P2(f3(a1,a1),f8(a4,a4),a5)),
% 75.59/75.66 inference(scs_inference,[],[8613,8751,8755,8692,8322,8720,8408,8000,7942,7926,7936,27,26,29,30,31,32])).
% 75.59/75.66 cnf(8786,plain,
% 75.59/75.66 (P4(f8(a1,a1),f3(a4,a4),f3(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8613,8751,8755,8741,8231,8692,8322,8720,8408,8362,8000,7942,7926,7936,27,26,29,30,31,32,33])).
% 75.59/75.66 cnf(8788,plain,
% 75.59/75.66 (P2(f8(a4,a4),a5,a5)),
% 75.59/75.66 inference(scs_inference,[],[8613,8751,8755,8741,8231,8692,8322,8720,8408,8362,8000,7942,7926,7936,27,26,29,30,31,32,33,43])).
% 75.59/75.66 cnf(8794,plain,
% 75.59/75.66 (P2(a7,f8(a4,a4),a7)),
% 75.59/75.66 inference(scs_inference,[],[8410,27])).
% 75.59/75.66 cnf(8796,plain,
% 75.59/75.66 (P4(f3(a4,a4),f8(a1,a1),f3(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8786,8410,27,26])).
% 75.59/75.66 cnf(8804,plain,
% 75.59/75.66 (~P2(a4,f6(a5),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8786,8709,8782,8776,8724,8372,8703,8402,8410,8284,7980,8131,27,26,29,32,30,31])).
% 75.59/75.66 cnf(8806,plain,
% 75.59/75.66 (~P4(f3(a1,a1),a1,a5)),
% 75.59/75.66 inference(scs_inference,[],[8786,8709,8747,8782,8776,8210,8724,8372,8666,8703,8402,8410,8284,7980,8131,8447,27,26,29,32,30,31,34])).
% 75.59/75.66 cnf(8812,plain,
% 75.59/75.66 (P2(f6(a5),a4,f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8284,27])).
% 75.59/75.66 cnf(8814,plain,
% 75.59/75.66 (P4(a4,f6(a4),a1)),
% 75.59/75.66 inference(scs_inference,[],[8284,8043,27,26])).
% 75.59/75.66 cnf(8818,plain,
% 75.59/75.66 (~P2(a1,f8(a4,a4),a5)),
% 75.59/75.66 inference(scs_inference,[],[8507,8461,8782,8776,7938,8284,8447,8043,27,26,29,32])).
% 75.59/75.66 cnf(8826,plain,
% 75.59/75.66 (~P4(a4,f6(a4),a5)),
% 75.59/75.66 inference(scs_inference,[],[8549,8507,8757,8024,8774,7962,8461,8692,8782,8776,7938,8284,8447,8043,261,27,26,29,32,33,34,31,7892])).
% 75.59/75.66 cnf(8831,plain,
% 75.59/75.66 (P4(a7,f6(a7),a1)),
% 75.59/75.66 inference(scs_inference,[],[8002,26])).
% 75.59/75.66 cnf(8835,plain,
% 75.59/75.66 (~P4(f6(a5),a4,a4)),
% 75.59/75.66 inference(scs_inference,[],[8814,7976,7942,8002,26,4837,29])).
% 75.59/75.66 cnf(8837,plain,
% 75.59/75.66 (P2(f8(a4,a4),f8(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8814,8248,8782,7976,7942,8002,26,4837,29,31])).
% 75.59/75.66 cnf(8848,plain,
% 75.59/75.66 (P4(a5,f6(a5),a1)),
% 75.59/75.66 inference(scs_inference,[],[8117,26])).
% 75.59/75.66 cnf(8850,plain,
% 75.59/75.66 (P4(f8(a1,a1),f6(a2),f6(a2))),
% 75.59/75.66 inference(scs_inference,[],[8204,8117,8449,26,29])).
% 75.59/75.66 cnf(8852,plain,
% 75.59/75.66 (~P2(a4,f8(a1,a1),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8804,8342,8204,8400,8117,8449,26,29,31])).
% 75.59/75.66 cnf(8854,plain,
% 75.59/75.66 (~P2(a5,f8(a4,a4),f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8837,8784,8804,8342,8204,8416,8400,8117,8449,26,29,31,32])).
% 75.59/75.66 cnf(8856,plain,
% 75.59/75.66 (~P4(f8(a1,a1),f6(a5),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[8837,8784,8804,8274,8342,8204,8416,8400,8117,8449,943,26,29,31,32,30])).
% 75.59/75.66 cnf(8871,plain,
% 75.59/75.66 (P4(f3(a5,a5),f6(a5),a5)),
% 75.59/75.66 inference(scs_inference,[],[8743,8831,8850,8852,8848,8812,8014,8496,8666,7962,8127,8284,7964,26,29,31,32,30])).
% 75.59/75.66 cnf(8875,plain,
% 75.59/75.66 (~P4(f3(a5,a5),a1,a5)),
% 75.59/75.66 inference(scs_inference,[],[8743,8645,8831,8850,8852,8848,8575,8812,8014,8496,8666,7962,8127,8284,8125,7964,26,29,31,32,30,34,3580])).
% 75.59/75.66 cnf(8877,plain,
% 75.59/75.66 (~P4(a5,a1,f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8743,8645,8831,8850,8852,8848,8575,8812,8014,8496,8666,7962,8127,8284,8125,7964,26,29,31,32,30,34,3580,3585])).
% 75.59/75.66 cnf(8879,plain,
% 75.59/75.66 (~P4(a1,a5,f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8743,8645,8831,8850,8852,8848,8575,8812,8014,8496,8666,7962,8127,8284,8125,7964,26,29,31,32,30,34,3580,3585,3587])).
% 75.59/75.66 cnf(8881,plain,
% 75.59/75.66 (~P4(a1,f3(a5,a5),a5)),
% 75.59/75.66 inference(scs_inference,[],[8743,8645,8831,8850,8852,8848,8575,8812,8014,8496,8666,7962,8127,8284,8125,7964,26,29,31,32,30,34,3580,3585,3587,4170])).
% 75.59/75.66 cnf(8883,plain,
% 75.59/75.66 (~P4(f3(a5,a5),a1,f3(a1,a5))),
% 75.59/75.66 inference(scs_inference,[],[8743,8645,8831,8850,8852,8848,8575,8812,8014,8496,8666,7962,8127,8284,8125,7964,26,29,31,32,30,34,3580,3585,3587,4170,3755])).
% 75.59/75.66 cnf(8887,plain,
% 75.59/75.66 (P4(f6(a5),f3(a5,a5),a5)),
% 75.59/75.66 inference(scs_inference,[],[8871,26])).
% 75.59/75.66 cnf(8889,plain,
% 75.59/75.66 (~P4(f6(a5),f3(a5,a5),f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8871,3574,26,29])).
% 75.59/75.66 cnf(8895,plain,
% 75.59/75.66 (~P4(f8(a1,a1),a1,a4)),
% 75.59/75.66 inference(scs_inference,[],[8705,8871,8549,8850,8812,8299,8782,7966,7936,3574,26,29,31,32,30])).
% 75.59/75.66 cnf(8897,plain,
% 75.59/75.66 (~P2(f8(a4,a4),f3(a1,a1),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8705,8672,8871,8549,8850,8812,8299,8246,8307,8782,8516,7966,7936,3574,26,29,31,32,30,33])).
% 75.59/75.66 cnf(8901,plain,
% 75.59/75.66 (~P4(f3(a5,a5),f6(a5),a1)),
% 75.59/75.66 inference(scs_inference,[],[8705,8672,8871,8818,8549,8850,8848,8812,8299,8246,8307,8416,8782,7962,8516,7966,7936,3574,26,29,31,32,30,33,34,3546])).
% 75.59/75.66 cnf(8905,plain,
% 75.59/75.66 (~P4(f8(a1,a1),f3(a5,a5),f3(a5,a1))),
% 75.59/75.66 inference(scs_inference,[],[8705,8672,8871,8818,8549,8850,8848,8812,8299,8246,8307,8416,8782,7962,8434,8516,7966,7936,3574,26,29,31,32,30,33,34,3546,27,6892])).
% 75.59/75.66 cnf(8909,plain,
% 75.59/75.66 (P4(a1,f6(a1),a1)),
% 75.59/75.66 inference(scs_inference,[],[8077,26])).
% 75.59/75.66 cnf(8911,plain,
% 75.59/75.66 (~P4(a5,f6(a1),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[2914,8077,26,1209])).
% 75.59/75.66 cnf(8915,plain,
% 75.59/75.66 (~P2(f9(a5),f3(a1,a1),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8877,8854,8488,8109,7964,2914,8077,26,1209,29,31])).
% 75.59/75.66 cnf(8919,plain,
% 75.59/75.66 (~P4(f6(a1),a5,f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8877,8879,8854,8747,8488,8382,8109,7940,7964,2914,8077,3763,26,1209,29,31,32,30])).
% 75.59/75.66 cnf(8921,plain,
% 75.59/75.66 (~P2(f3(a1,a1),a4,f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8877,8879,8854,8747,8488,8382,8109,7940,8135,8447,8089,7964,2914,8077,3763,26,1209,29,31,32,30,33])).
% 75.59/75.66 cnf(8923,plain,
% 75.59/75.66 (~P4(a4,f6(a4),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8877,8879,8854,8313,8747,8488,8814,8382,8109,7940,8400,8135,8447,8089,7964,2914,8077,3763,3770,26,1209,29,31,32,30,33,34])).
% 75.59/75.66 cnf(8927,plain,
% 75.59/75.66 (P4(f6(a1),f6(a7),f6(a7))),
% 75.59/75.66 inference(scs_inference,[],[8909,1095])).
% 75.59/75.66 cnf(8931,plain,
% 75.59/75.66 (~P4(f3(a5,a5),f6(a1),a5)),
% 75.59/75.66 inference(scs_inference,[],[8909,8875,8488,29])).
% 75.59/75.66 cnf(8933,plain,
% 75.59/75.66 (~P2(f3(a1,a1),f8(a4,a4),f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8909,8875,8921,8488,8812,8782,29,31])).
% 75.59/75.66 cnf(8935,plain,
% 75.59/75.66 (P4(a5,f8(a1,a1),a5)),
% 75.59/75.66 inference(scs_inference,[],[8909,8875,8887,8921,8652,8488,8812,8782,29,31,30])).
% 75.59/75.66 cnf(8939,plain,
% 75.59/75.66 (P4(f8(a1,a1),a5,a5)),
% 75.59/75.66 inference(scs_inference,[],[8909,8911,8875,8887,8921,8652,8741,8368,8488,8812,8782,29,31,30,33,26])).
% 75.59/75.66 cnf(8945,plain,
% 75.59/75.66 (~P4(f6(a5),f6(a1),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[8927,8055,29])).
% 75.59/75.66 cnf(8949,plain,
% 75.59/75.66 (~P2(f6(a5),a4,f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8927,8933,8055,8804,8812,8674,8424,8087,29,31,32])).
% 75.59/75.66 cnf(8953,plain,
% 75.59/75.66 (~P2(f6(a1),a4,f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8927,8933,8081,8055,8804,8909,8812,8674,8424,8087,3779,29,31,32,30,33])).
% 75.59/75.66 cnf(8955,plain,
% 75.59/75.66 (P4(f6(a1),f8(a10,a10),f8(a10,a10))),
% 75.59/75.66 inference(scs_inference,[],[8927,8933,8081,8055,8804,8909,8812,8674,8424,8087,3779,29,31,32,30,33,26])).
% 75.59/75.66 cnf(8962,plain,
% 75.59/75.66 (~P2(f6(a5),a4,f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[8953,8162,8812,8400,8449,29,32])).
% 75.59/75.66 cnf(8964,plain,
% 75.59/75.66 (~P4(f8(a1,a1),a5,a1)),
% 75.59/75.66 inference(scs_inference,[],[8901,8953,8641,8871,8162,8812,8400,8449,29,32,30])).
% 75.59/75.66 cnf(8966,plain,
% 75.59/75.66 (~P2(f3(a5,a5),a4,f3(a5,a1))),
% 75.59/75.66 inference(scs_inference,[],[8901,8905,8953,8166,8422,8641,8871,8162,8812,8400,8449,29,32,30,33])).
% 75.59/75.66 cnf(8968,plain,
% 75.59/75.66 (~P2(f6(a4),f6(a5),f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[8901,8528,8905,8953,8166,8422,8641,8871,8162,8812,8400,8043,8284,8449,29,32,30,33,34])).
% 75.59/75.66 cnf(8974,plain,
% 75.59/75.66 (~P4(f6(a1),f3(a5,a5),f3(a5,a1))),
% 75.59/75.66 inference(scs_inference,[],[8901,8528,8905,8953,8166,8422,8909,8641,8871,8887,8162,8151,8812,8400,8043,8284,8449,29,32,30,33,34,3898,26,6892])).
% 75.59/75.66 cnf(8978,plain,
% 75.59/75.66 (~P4(f3(a5,a5),f6(a5),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8901,8449,3660,29])).
% 75.59/75.66 cnf(8984,plain,
% 75.59/75.66 (P4(f3(a4,a4),f6(a4),a4)),
% 75.59/75.66 inference(scs_inference,[],[7,8962,8718,8660,8901,8814,8774,8782,8051,8149,8449,3660,29,31,32,30])).
% 75.59/75.66 cnf(8988,plain,
% 75.59/75.66 (P4(f6(a4),f3(a4,a4),a4)),
% 75.59/75.66 inference(scs_inference,[],[7,8897,8962,8718,8660,8901,8503,8814,8774,8307,8782,8051,8149,8516,8449,3660,29,31,32,30,34,26])).
% 75.59/75.66 cnf(8995,plain,
% 75.59/75.66 (~P4(f6(a5),f3(a4,a4),f3(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8984,8835,29])).
% 75.59/75.66 cnf(8999,plain,
% 75.59/75.66 (~P4(f3(a1,a1),a1,a4)),
% 75.59/75.66 inference(scs_inference,[],[8326,8984,8852,8835,8210,8909,8674,8284,29,31,30])).
% 75.59/75.66 cnf(9001,plain,
% 75.59/75.66 (~P2(a2,a7,f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[7,8326,8919,8984,8852,8835,8260,8210,8909,7974,8674,8284,29,31,30,33])).
% 75.59/75.66 cnf(9003,plain,
% 75.59/75.66 (~P4(a5,f8(a1,a1),f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[7,8326,8919,8984,8935,8854,8852,8835,8260,8210,8428,8909,7974,8416,8674,8284,29,31,30,33,34])).
% 75.59/75.66 cnf(9010,plain,
% 75.59/75.66 (~P4(f8(a1,a1),a4,f3(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[8895,8984,8814,29])).
% 75.59/75.66 cnf(9012,plain,
% 75.59/75.66 (~P2(a5,f8(a4,a4),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[7,9001,8895,8794,8984,8814,29,31])).
% 75.59/75.66 cnf(9016,plain,
% 75.59/75.66 (~P4(a5,a5,a5)),
% 75.59/75.66 inference(scs_inference,[],[7,8881,9001,8895,8915,8794,8984,8751,8755,8848,8887,8814,29,31,32,30])).
% 75.59/75.66 cnf(9018,plain,
% 75.59/75.66 (~P4(a5,a5,f3(a5,a1))),
% 75.59/75.66 inference(scs_inference,[],[7,8881,9001,8966,8895,8915,8794,8984,8751,8755,8848,8887,8814,8127,261,29,31,32,30,34])).
% 75.59/75.66 cnf(9020,plain,
% 75.59/75.66 (~P4(a4,a4,a4)),
% 75.59/75.66 inference(scs_inference,[],[7,8881,9001,8966,8895,8915,8794,8984,8751,8755,8848,8887,8814,8127,261,29,31,32,30,34,364])).
% 75.59/75.66 cnf(9024,plain,
% 75.59/75.66 (~P4(a2,a2,a2)),
% 75.59/75.66 inference(scs_inference,[],[9016,62])).
% 75.59/75.66 cnf(9027,plain,
% 75.59/75.66 (P4(a4,f8(a1,a1),a4)),
% 75.59/75.66 inference(scs_inference,[],[9016,8988,8796,8939,29,30])).
% 75.59/75.66 cnf(9029,plain,
% 75.59/75.66 (~P2(f6(a1),f8(a4,a4),a5)),
% 75.59/75.66 inference(scs_inference,[],[9016,9012,8988,8796,8939,8573,8837,29,30,32])).
% 75.59/75.66 cnf(9031,plain,
% 75.59/75.66 (~P2(f8(a1,a1),a5,a5)),
% 75.59/75.66 inference(scs_inference,[],[9016,9012,8988,8796,8939,8788,8573,8837,8757,29,30,32,33])).
% 75.59/75.66 cnf(9033,plain,
% 75.59/75.66 (~P4(a5,f8(a1,a1),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[9016,9012,8988,8796,8939,8788,8935,8573,8837,8757,8428,8416,29,30,32,33,34])).
% 75.59/75.66 cnf(9039,plain,
% 75.59/75.66 (P4(f8(a1,a1),a4,a4)),
% 75.59/75.66 inference(scs_inference,[],[9016,9012,8988,8796,8939,8788,8935,8573,8837,8757,8428,8416,29,30,32,33,34,285,301,26])).
% 75.59/75.66 cnf(9043,plain,
% 75.59/75.66 (~P2(f8(a1,a1),a2,a2)),
% 75.59/75.66 inference(scs_inference,[],[7,9016,9012,8988,8796,8939,8788,8935,8573,8837,8757,8428,8416,29,30,32,33,34,285,301,26,181,31])).
% 75.59/75.66 cnf(9045,plain,
% 75.59/75.66 (~P4(a4,f8(a1,a1),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9020,9039,29])).
% 75.59/75.66 cnf(9047,plain,
% 75.59/75.66 (~P2(a4,a5,f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9020,9039,8631,8400,363,29,31])).
% 75.59/75.66 cnf(9049,plain,
% 75.59/75.66 (~P4(f8(a1,a1),f3(a4,a4),a4)),
% 75.59/75.66 inference(scs_inference,[],[9020,9039,8631,8400,8051,363,29,31,30])).
% 75.59/75.66 cnf(9051,plain,
% 75.59/75.66 (~P2(f8(a4,a4),f8(a4,a4),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9020,9031,9039,8631,8788,8400,8051,363,29,31,30,32])).
% 75.59/75.66 cnf(9053,plain,
% 75.59/75.66 (~P2(f3(a2,a2),a7,f3(a5,a1))),
% 75.59/75.66 inference(scs_inference,[],[7,9020,9031,9039,9018,8631,8788,7974,8400,8051,363,29,31,30,32,33])).
% 75.59/75.66 cnf(9055,plain,
% 75.59/75.66 (~P4(f6(a5),a1,f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[7,9020,9031,9039,9018,8949,8631,8788,7974,8812,8400,8051,8447,363,3660,29,31,30,32,33,34])).
% 75.59/75.66 cnf(9057,plain,
% 75.59/75.66 (~P4(f8(a1,a1),a4,f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9049,9039,8051,29])).
% 75.59/75.66 cnf(9059,plain,
% 75.59/75.66 (~P2(f3(a4,a4),a5,f3(a5,a1))),
% 75.59/75.66 inference(scs_inference,[],[9049,8966,8137,9039,8051,7936,29,31])).
% 75.59/75.66 cnf(9061,plain,
% 75.59/75.66 (~P2(f3(a4,a4),f8(a1,a1),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9051,9049,8966,8354,8137,9039,8428,8051,7936,29,31,32])).
% 75.59/75.66 cnf(9063,plain,
% 75.59/75.66 (~P4(a5,a1,f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9051,8978,9049,8966,8354,8137,9039,8428,8848,8127,8051,7936,29,31,32,30])).
% 75.59/75.66 cnf(9067,plain,
% 75.59/75.66 (~P4(f6(a2),a2,a5)),
% 75.59/75.66 inference(scs_inference,[],[9051,8995,8978,9049,8966,8818,8147,8354,8137,8690,9039,8309,8408,8428,8848,8127,7966,8051,7936,29,31,32,30,33,34])).
% 75.59/75.66 cnf(9071,plain,
% 75.59/75.66 (~P4(f8(a1,a1),a5,f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9003,8935,8939,8303,29,30])).
% 75.59/75.66 cnf(9073,plain,
% 75.59/75.66 (~P2(f3(a1,a1),a1,f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9003,9051,8414,8935,8939,8303,8307,29,30,31])).
% 75.59/75.66 cnf(9077,plain,
% 75.59/75.66 (~P2(a4,f8(a4,a4),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9003,9045,9027,9051,8962,8718,8414,8935,8939,8303,8428,8307,8782,8674,29,30,31,32,33])).
% 75.59/75.66 cnf(9079,plain,
% 75.59/75.66 (~P4(f8(a1,a1),f8(a1,a1),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9061,9003,9045,9027,9051,8962,8718,8414,8468,8935,8939,8303,8235,8428,8307,8782,8674,29,30,31,32,33,34])).
% 75.59/75.66 cnf(9081,plain,
% 75.59/75.66 (~P4(a4,f6(a4),f6(a4))),
% 75.59/75.66 inference(scs_inference,[],[9020,8988,29])).
% 75.59/75.66 cnf(9083,plain,
% 75.59/75.66 (~P2(f8(a4,a4),f6(a1),a5)),
% 75.59/75.66 inference(scs_inference,[],[9029,9020,8988,8573,8368,29,32])).
% 75.59/75.66 cnf(9085,plain,
% 75.59/75.66 (~P4(f8(a1,a1),a1,a5)),
% 75.59/75.66 inference(scs_inference,[],[9029,9067,9020,8850,8988,8573,8368,7966,29,32,30])).
% 75.59/75.66 cnf(9087,plain,
% 75.59/75.66 (~P2(a4,f8(a1,a1),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9029,9067,9077,9020,8850,8988,8573,8342,8368,8400,7966,29,32,30,31])).
% 75.59/75.66 cnf(9089,plain,
% 75.59/75.66 (~P2(f3(a4,a4),a4,a4)),
% 75.59/75.66 inference(scs_inference,[],[9029,9067,9077,9049,8227,9020,8850,8988,8786,8573,8422,8342,8368,8400,7966,29,32,30,31,33])).
% 75.59/75.66 cnf(9094,plain,
% 75.59/75.66 (~P4(f3(a4,a4),f6(a1),a4)),
% 75.59/75.66 inference(scs_inference,[],[9010,8252,8786,29])).
% 75.59/75.66 cnf(9096,plain,
% 75.59/75.66 (~P2(f3(a5,a5),f8(a4,a4),f3(a5,a1))),
% 75.59/75.66 inference(scs_inference,[],[9010,8252,8166,8966,8786,8674,29,31])).
% 75.59/75.66 cnf(9098,plain,
% 75.59/75.66 (~P2(f3(a1,a1),a1,a4)),
% 75.59/75.66 inference(scs_inference,[],[9010,9073,8252,8166,8966,8751,8786,8307,8674,29,31,32])).
% 75.59/75.66 cnf(9100,plain,
% 75.59/75.66 (~P4(a1,a4,f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9057,9010,9073,8252,8166,8966,8751,9039,8786,8268,8307,8674,29,31,32,30])).
% 75.59/75.66 cnf(9102,plain,
% 75.59/75.66 (~P2(f3(a2,a2),a4,a2)),
% 75.59/75.66 inference(scs_inference,[],[9024,9057,9010,9073,8252,8166,8966,8751,9039,8786,8382,8268,7974,8307,8674,29,31,32,30,33])).
% 75.59/75.66 cnf(9104,plain,
% 75.59/75.66 (~P2(f8(a1,a1),f8(a1,a1),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9024,9057,9010,9073,9087,8252,9027,8166,8966,8751,9039,8741,8786,8382,8342,8268,7974,8307,8674,29,31,32,30,33,34])).
% 75.59/75.66 cnf(9107,plain,
% 75.59/75.66 (~P4(a4,a1,a1)),
% 75.59/75.66 inference(scs_inference,[],[9081,1353,29])).
% 75.59/75.66 cnf(9109,plain,
% 75.59/75.66 (~P4(f6(a1),f3(a4,a4),a4)),
% 75.59/75.66 inference(scs_inference,[],[9094,9081,8252,8233,1353,29,30])).
% 75.59/75.66 cnf(9111,plain,
% 75.59/75.66 (~P2(f3(a4,a4),f8(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9094,9081,9089,8252,8233,8782,1353,29,30,31])).
% 75.59/75.66 cnf(9113,plain,
% 75.59/75.66 (~P2(f3(a1,a1),f3(a1,a1),a4)),
% 75.59/75.66 inference(scs_inference,[],[9094,9081,9089,9077,8252,8233,8585,8322,8782,1353,29,30,31,32])).
% 75.59/75.66 cnf(9115,plain,
% 75.59/75.66 (~P2(f3(a1,a1),f3(a1,a1),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9079,9094,9081,9089,9077,8252,8233,8585,8322,8113,8516,8782,1353,29,30,31,32,33])).
% 75.59/75.66 cnf(9117,plain,
% 75.59/75.66 (~P4(f3(a2,a2),f6(a1),a2)),
% 75.59/75.66 inference(scs_inference,[],[9079,9094,9081,9089,9102,8619,8404,9077,8252,8233,8585,8718,8322,8113,8516,8782,1353,29,30,31,32,33,34])).
% 75.59/75.66 cnf(9119,plain,
% 75.59/75.66 (P1(f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9107,8376,26])).
% 75.59/75.66 cnf(9120,plain,
% 75.59/75.66 (P4(a1,f9(a4),f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9119,17])).
% 75.59/75.66 cnf(9122,plain,
% 75.59/75.66 (P2(a4,f9(a4),f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9119,17,18])).
% 75.59/75.66 cnf(9124,plain,
% 75.59/75.66 (P2(f9(a4),a4,f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9119,17,18,27])).
% 75.59/75.66 cnf(9126,plain,
% 75.59/75.66 (P4(f9(a4),a1,f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9119,17,18,27,26])).
% 75.59/75.66 cnf(9130,plain,
% 75.59/75.66 (~P4(a4,a7,a7)),
% 75.59/75.66 inference(scs_inference,[],[9119,9107,8831,39,17,18,27,26,28,29])).
% 75.59/75.66 cnf(9132,plain,
% 75.59/75.66 (~P2(f9(a5),f3(a5,a5),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9111,9119,8185,9107,8147,8831,39,17,18,27,26,28,29,32])).
% 75.59/75.66 cnf(9134,plain,
% 75.59/75.66 (~P4(f3(a4,a4),a1,a4)),
% 75.59/75.66 inference(scs_inference,[],[9111,9119,8185,8229,9107,9094,8147,8831,8909,39,17,18,27,26,28,29,32,30])).
% 75.59/75.66 cnf(9136,plain,
% 75.59/75.66 (~P2(f8(a4,a4),a5,f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[9111,9083,9119,8185,8229,9107,9094,8147,8831,8837,8788,8909,39,17,18,27,26,28,29,32,30,31])).
% 75.59/75.66 cnf(9138,plain,
% 75.59/75.66 (~P4(f8(a4,a4),f8(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9111,9083,9119,8185,8229,9107,9094,8147,8831,8837,8788,8909,8235,39,17,18,27,26,28,29,32,30,31,34])).
% 75.59/75.66 cnf(9142,plain,
% 75.59/75.66 (P4(f8(a1,a1),f9(a4),f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9120,8449,29])).
% 75.59/75.66 cnf(9144,plain,
% 75.59/75.66 (~P2(a4,f6(a1),a5)),
% 75.59/75.66 inference(scs_inference,[],[9120,9136,8751,8368,8449,29,31])).
% 75.59/75.66 cnf(9146,plain,
% 75.59/75.66 (~P2(f8(a1,a1),f8(a1,a1),a4)),
% 75.59/75.66 inference(scs_inference,[],[9104,9120,9136,8468,8751,8368,8449,29,31,32])).
% 75.59/75.66 cnf(9148,plain,
% 75.59/75.66 (~P4(a1,f3(a4,a4),a4)),
% 75.59/75.66 inference(scs_inference,[],[9104,9120,9109,9136,8468,8233,8751,8368,8449,2749,29,31,32,30])).
% 75.59/75.66 cnf(9150,plain,
% 75.59/75.66 (~P2(f3(a4,a4),a4,f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9104,9138,9120,9109,9136,8468,8233,8751,8368,8235,8449,2749,29,31,32,30,33])).
% 75.59/75.66 cnf(9152,plain,
% 75.59/75.66 (~P4(f8(a1,a1),f8(a1,a1),a4)),
% 75.59/75.66 inference(scs_inference,[],[9104,9138,9120,9109,9136,9098,8414,8468,8233,8751,8368,8113,8235,8087,8449,2749,29,31,32,30,33,34])).
% 75.59/75.66 cnf(9154,plain,
% 75.59/75.66 (P4(f9(a4),f8(a1,a1),f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9104,9138,9120,9109,9136,9098,8414,8468,8233,8751,8368,8113,8235,8087,8449,2749,29,31,32,30,33,34,26])).
% 75.59/75.66 cnf(9156,plain,
% 75.59/75.66 (~P4(f3(a2,a2),a1,a2)),
% 75.59/75.66 inference(scs_inference,[],[9117,8668,2749,29])).
% 75.59/75.66 cnf(9158,plain,
% 75.59/75.66 (~P2(a5,f8(a4,a4),f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[9132,9117,8668,8248,7936,2749,29,31])).
% 75.59/75.66 cnf(9160,plain,
% 75.59/75.66 (~P2(a7,f3(a2,a2),a5)),
% 75.59/75.66 inference(scs_inference,[],[9132,9117,8286,8270,8668,8248,7936,2749,29,31,32])).
% 75.59/75.66 cnf(9164,plain,
% 75.59/75.66 (~P2(f8(a1,a1),a4,a4)),
% 75.59/75.66 inference(scs_inference,[],[9132,9117,9152,8286,8270,8187,8722,8668,8248,8422,8103,7936,2749,29,31,32,30,33])).
% 75.59/75.66 cnf(9166,plain,
% 75.59/75.66 (~P4(f3(a5,a5),f8(a1,a1),f3(a5,a1))),
% 75.59/75.66 inference(scs_inference,[],[9096,9132,9117,9152,8286,8270,8187,8722,8185,8652,8668,8248,8422,8103,8428,7936,2749,29,31,32,30,33,34])).
% 75.59/75.66 cnf(9168,plain,
% 75.59/75.66 (P4(f6(a1),f9(a4),f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9120,8077,29])).
% 75.59/75.66 cnf(9170,plain,
% 75.59/75.66 (~P2(f8(a4,a4),f8(a1,a1),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9120,9077,8468,8248,8077,29,31])).
% 75.59/75.66 cnf(9172,plain,
% 75.59/75.66 (~P2(a4,f3(a5,a5),a5)),
% 75.59/75.66 inference(scs_inference,[],[9160,9120,8286,9077,8468,8384,8248,8077,29,31,32])).
% 75.59/75.66 cnf(9174,plain,
% 75.59/75.66 (~P4(f3(a2,a2),f8(a1,a1),a2)),
% 75.59/75.66 inference(scs_inference,[],[9156,9160,9120,8739,8286,9077,8288,8468,8384,8248,8077,29,31,32,30])).
% 75.59/75.66 cnf(9178,plain,
% 75.59/75.66 (~P4(f3(a4,a4),f8(a1,a1),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9130,9156,9160,9120,8739,8796,8250,8286,9111,9077,8288,8468,8384,9039,8248,8428,8077,29,31,32,30,33,34])).
% 75.59/75.66 cnf(9180,plain,
% 75.59/75.66 (~P2(f9(a5),a2,f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9130,9156,9160,9120,8739,8796,8250,8286,9111,9077,8288,8468,8384,9039,8248,8428,8077,29,31,32,30,33,34,8239])).
% 75.59/75.66 cnf(9182,plain,
% 75.59/75.66 (~P4(a7,a4,a7)),
% 75.59/75.66 inference(scs_inference,[],[9130,9156,9160,9120,8739,8796,8250,8286,9111,9077,8288,8468,8384,9039,8248,8428,8077,29,31,32,30,33,34,8239,26])).
% 75.59/75.66 cnf(9184,plain,
% 75.59/75.66 (P4(f9(a4),f6(a1),f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9168,26])).
% 75.59/75.66 cnf(9186,plain,
% 75.59/75.66 (~P4(f3(a1,a1),a4,f3(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9168,8999,8984,8814,26,29])).
% 75.59/75.66 cnf(9190,plain,
% 75.59/75.66 (~P2(f8(a4,a4),f8(a4,a4),f3(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9150,9168,9180,8999,8984,8354,8147,8837,8814,8751,26,29,31,32])).
% 75.59/75.66 cnf(9192,plain,
% 75.59/75.66 (~P4(a1,a5,f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9071,9150,9168,9180,8999,8984,8354,8147,8939,8268,8837,8814,8751,26,29,31,32,30])).
% 75.59/75.66 cnf(9194,plain,
% 75.59/75.66 (~P2(a1,a7,a4)),
% 75.59/75.66 inference(scs_inference,[],[9182,9071,9150,9168,9180,8999,8984,8354,8503,8147,8939,8268,8410,8837,8814,8751,26,29,31,32,30,33])).
% 75.59/75.66 cnf(9196,plain,
% 75.59/75.66 (~P4(a4,a4,f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9182,9071,9150,9168,9180,8999,8984,8354,8503,8147,8939,8268,8410,8837,8814,8751,8400,8051,26,29,31,32,30,33,34])).
% 75.59/75.66 cnf(9198,plain,
% 75.59/75.66 (~P4(f8(a1,a1),f3(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9178,26])).
% 75.59/75.66 cnf(9200,plain,
% 75.59/75.66 (~P4(f3(a4,a4),f6(a1),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9178,8796,8303,26,29])).
% 75.59/75.66 cnf(9202,plain,
% 75.59/75.66 (~P2(f8(a4,a4),f3(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9178,9190,8796,8231,8303,8837,26,29,31])).
% 75.59/75.66 cnf(9204,plain,
% 75.59/75.66 (~P4(f6(a1),f3(a2,a2),a2)),
% 75.59/75.66 inference(scs_inference,[],[9178,9190,9117,8404,8193,8796,8231,8303,8837,26,29,31,30])).
% 75.59/75.66 cnf(9206,plain,
% 75.59/75.66 (P2(f9(a4),f8(a4,a4),f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9178,9190,9124,9117,8404,8193,8796,8231,8303,8837,8674,26,29,31,30,32])).
% 75.59/75.66 cnf(9208,plain,
% 75.59/75.66 (~P2(a5,a4,f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[9178,9190,9124,8889,9117,8404,8193,8796,8231,8166,8303,8887,8837,8812,8674,26,29,31,30,32,33])).
% 75.59/75.66 cnf(9212,plain,
% 75.59/75.66 (P2(f8(a4,a4),f9(a4),f9(a4))),
% 75.59/75.66 inference(scs_inference,[],[9178,9190,9124,8889,9160,9117,8404,8193,8796,8231,8286,8166,8303,8887,8837,7976,8812,8674,26,29,31,30,32,33,34,27])).
% 75.59/75.66 cnf(9217,plain,
% 75.59/75.66 (~P2(f3(a5,a5),f9(a5),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9190,8172,8137,8037,8449,29,31])).
% 75.59/75.66 cnf(9219,plain,
% 75.59/75.66 (~P2(f9(a5),a2,a1)),
% 75.59/75.66 inference(scs_inference,[],[7,9194,9190,8172,8137,8037,7936,8449,29,31,32])).
% 75.59/75.66 cnf(9221,plain,
% 75.59/75.66 (~P4(f3(a4,a4),a1,f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[7,9194,9200,9190,8229,8172,8137,8037,8909,7936,8449,29,31,32,30])).
% 75.59/75.66 cnf(9223,plain,
% 75.59/75.66 (~P2(f3(a2,a2),f8(a4,a4),a2)),
% 75.59/75.66 inference(scs_inference,[],[7,9194,9200,9024,9190,8229,8172,8137,8037,8408,8909,7974,7936,8449,29,31,32,30,33])).
% 75.59/75.66 cnf(9225,plain,
% 75.59/75.66 (~P4(a5,f8(a1,a1),f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[7,9194,9200,9158,9024,9190,8229,8172,8137,8037,8935,8408,8909,8416,7974,8428,7936,8449,29,31,32,30,33,34])).
% 75.59/75.66 cnf(9229,plain,
% 75.59/75.66 (~P4(a1,f3(a5,a5),f3(a1,a5))),
% 75.59/75.66 inference(scs_inference,[],[8883,26])).
% 75.59/75.66 cnf(9231,plain,
% 75.59/75.66 (~P4(f3(a1,a1),f6(a4),a1)),
% 75.59/75.66 inference(scs_inference,[],[8883,9186,8091,8988,26,29])).
% 75.59/75.66 cnf(9233,plain,
% 75.59/75.66 (~P2(f8(a1,a1),f8(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9115,8883,9186,8091,8988,8322,8585,26,29,31])).
% 75.59/75.66 cnf(9235,plain,
% 75.59/75.66 (~P2(a2,a4,f3(a2,a2))),
% 75.59/75.66 inference(scs_inference,[],[9115,8883,9186,9223,8091,8988,8322,8585,8382,8674,26,29,31,32])).
% 75.59/75.66 cnf(9237,plain,
% 75.59/75.66 (~P4(f6(a1),a5,a1)),
% 75.59/75.66 inference(scs_inference,[],[9115,8883,8964,9186,9223,8091,8988,8322,8585,8939,8382,8292,8674,26,29,31,32,30])).
% 75.59/75.66 cnf(9239,plain,
% 75.59/75.66 (~P2(a4,f3(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9115,9198,8883,8964,9186,9223,8195,8091,8988,8322,8585,8939,8382,8362,9039,8292,8674,26,29,31,32,30,33])).
% 75.59/75.66 cnf(9245,plain,
% 75.59/75.66 (~P2(a4,f8(a4,a4),f3(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9202,9166,8652,8288,8248,8782,29,31])).
% 75.59/75.66 cnf(9249,plain,
% 75.59/75.66 (~P2(f3(a2,a2),a7,a5)),
% 75.59/75.66 inference(scs_inference,[],[9202,9166,9200,8794,9158,8260,8252,8233,8652,8288,8248,8782,29,31,30,32])).
% 75.59/75.66 cnf(9254,plain,
% 75.59/75.66 (~P4(a4,a10,a10)),
% 75.59/75.66 inference(scs_inference,[],[9107,8776,29])).
% 75.59/75.66 cnf(9256,plain,
% 75.59/75.66 (~P2(f8(a4,a4),a5,f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[9172,9107,8776,8788,8248,29,31])).
% 75.59/75.66 cnf(9258,plain,
% 75.59/75.66 (~P4(f3(a4,a4),f3(a1,a1),a4)),
% 75.59/75.66 inference(scs_inference,[],[9134,9172,9107,8229,8776,8788,8248,8089,29,31,30])).
% 75.59/75.66 cnf(9260,plain,
% 75.59/75.66 (~P2(f8(a1,a1),f3(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9233,9134,9172,9107,8250,8229,8776,8788,8362,8248,8089,29,31,30,32])).
% 75.59/75.66 cnf(9262,plain,
% 75.59/75.66 (~P2(f6(a4),f8(a4,a4),a1)),
% 75.59/75.66 inference(scs_inference,[],[9233,9134,9172,9107,8250,8229,8984,8776,8788,8362,8248,8674,8089,29,31,30,32,33])).
% 75.59/75.66 cnf(9264,plain,
% 75.59/75.66 (~P4(f6(a1),f8(a1,a1),a4)),
% 75.59/75.66 inference(scs_inference,[],[9233,9134,9164,9172,9107,8250,8229,8984,8718,8776,8788,8422,8362,8248,8292,8674,8089,29,31,30,32,33,34])).
% 75.59/75.66 cnf(9266,plain,
% 75.59/75.66 (~P4(f3(a4,a4),f6(a4),f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[9264,8984,8233,29])).
% 75.59/75.66 cnf(9268,plain,
% 75.59/75.66 (~P2(f8(a1,a1),a4,f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9170,9264,8984,8468,8233,8422,29,31])).
% 75.59/75.66 cnf(9272,plain,
% 75.59/75.66 (~P2(f3(a1,a1),f9(a5),a4)),
% 75.59/75.66 inference(scs_inference,[],[9170,9264,8856,9047,8666,8984,8468,8233,8422,8848,7936,3666,29,31,30,32])).
% 75.59/75.66 cnf(9274,plain,
% 75.59/75.66 (~P2(f3(a4,a4),a2,a2)),
% 75.59/75.66 inference(scs_inference,[],[9170,9264,8856,9047,9024,8666,8984,8468,8233,8774,8422,8848,8235,7936,3666,29,31,30,32,33])).
% 75.59/75.66 cnf(9276,plain,
% 75.59/75.66 (~P2(f6(a1),f3(a4,a4),f8(a4,a4))),
% 75.59/75.66 inference(scs_inference,[],[9170,9260,9264,8856,9047,9024,8666,8984,8741,8303,8468,8233,8774,8422,8848,8362,8235,7936,3666,29,31,30,32,33,34])).
% 75.59/75.66 cnf(9278,plain,
% 75.59/75.66 (~P4(a10,a4,a10)),
% 75.59/75.66 inference(scs_inference,[],[9254,26])).
% 75.59/75.66 cnf(9280,plain,
% 75.59/75.66 (~P4(f6(a5),f3(a5,a5),f6(a1))),
% 75.59/75.66 inference(scs_inference,[],[9254,8155,8488,8077,26,29])).
% 75.59/75.66 cnf(9284,plain,
% 75.59/75.66 (~P2(a5,a1,a2)),
% 75.59/75.66 inference(scs_inference,[],[9254,9219,9178,8155,8796,8488,8091,8424,7936,8077,26,29,30,31])).
% 75.59/75.66 cnf(9286,plain,
% 75.59/75.66 (~P2(f3(a5,a5),f8(a4,a4),a5)),
% 75.59/75.66 inference(scs_inference,[],[9254,9219,9178,8155,9158,8796,8185,8488,8091,8837,8424,7936,8077,26,29,30,31,32])).
% 75.59/75.66 cnf(9288,plain,
% 75.59/75.66 (~P2(f8(a1,a1),a10,a4)),
% 75.59/75.66 inference(scs_inference,[],[9254,9219,9178,8155,9158,8796,8185,8488,8091,7916,9039,8837,8424,7936,8077,26,29,30,31,32,33])).
% 75.59/75.66 cnf(9290,plain,
% 75.59/75.66 (~P4(f3(a4,a4),f8(a1,a1),a4)),
% 75.59/75.66 inference(scs_inference,[],[9254,9219,9089,9178,8155,8227,9158,8796,8185,8488,8091,7916,9039,8422,8837,8424,7936,8077,26,29,30,31,32,33,34])).
% 75.59/75.66 cnf(9295,plain,
% 75.59/75.66 (P4(f8(a1,a1),f9(a5),f9(a5))),
% 75.59/75.66 inference(scs_inference,[],[8183,8449,29])).
% 75.59/75.66 cnf(9297,plain,
% 75.59/75.66 (~P4(f3(a1,a1),a1,f6(a5))),
% 75.59/75.66 inference(scs_inference,[],[8609,8210,8183,8909,8449,29,30])).
% 75.59/75.66 cnf(9299,plain,
% 75.59/75.66 (~P2(a4,a4,f8(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8609,9170,8210,8183,8909,8751,8449,29,30,31])).
% 75.59/75.66 cnf(9301,plain,
% 75.59/75.66 (~P2(f8(a4,a4),f3(a5,a5),f3(a5,a1))),
% 75.59/75.66 inference(scs_inference,[],[9053,8609,9170,8254,8210,8260,8183,8909,8751,8449,29,30,31,32])).
% 75.59/75.66 cnf(9303,plain,
% 75.59/75.66 (P4(f9(a5),f8(a1,a1),f9(a5))),
% 75.59/75.66 inference(scs_inference,[],[9053,8609,9170,8254,8210,8260,8183,8909,8751,8449,29,30,31,32,26])).
% 75.59/75.66 cnf(9311,plain,
% 75.59/75.66 (~P4(f6(a4),f8(a1,a1),f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8974,9258,9027,8984,26,29])).
% 75.59/75.66 cnf(9313,plain,
% 75.59/75.66 (~P4(f6(a4),f3(a4,a4),f3(a1,a1))),
% 75.59/75.66 inference(scs_inference,[],[8974,9258,9231,9027,8984,8043,26,29,30])).
% 75.59/75.66 cnf(9315,plain,
% 75.59/75.66 (~P2(f8(a1,a1),f8(a4,a4),a4)),
% 75.59/75.66 inference(scs_inference,[],[8974,9113,9258,9231,9027,8322,8585,8984,8043,26,29,30,31])).
% 75.59/75.66 cnf(9317,plain,
% 75.59/75.66 (~P2(a7,a1,a4)),
% 75.59/75.66 inference(scs_inference,[],[7,9284,8974,9113,9258,9231,9027,8322,8585,8984,8382,8043,26,29,30,31,32])).
% 75.59/75.66 cnf(9325,plain,
% 75.59/75.66 (~P4(f8(a1,a1),f3(a5,a5),f3(a1,a5))),
% 75.59/75.66 inference(scs_inference,[],[9229,8641,8268,29])).
% 75.59/75.66 cnf(9327,plain,
% 75.59/75.66 (~P4(f6(a4),f3(a4,a4),a1)),
% 75.59/75.66 inference(scs_inference,[],[9229,9107,8229,8988,8641,8268,29,30])).
% 75.59/75.66 cnf(9329,plain,
% 75.59/75.66 (~P2(f3(a5,a5),f9(a5),a4)),
% 75.59/75.66 inference(scs_inference,[],[9217,9229,9107,8346,8229,8988,8641,8268,8248,29,30,31])).
% 75.59/75.66 cnf(9331,plain,
% 75.59/75.66 (~P2(a2,a7,f3(a5,a5))),
% 75.59/75.66 inference(scs_inference,[],[7,9217,9286,9229,8794,9107,8346,8229,8988,8641,8268,8248,29,30,31,32])).
% 75.59/75.66 cnf(9338,plain,
% 75.59/75.66 (~P4(f8(a4,a4),a1,a1)),
% 75.59/75.66 inference(scs_inference,[],[9138,8246,29])).
% 75.59/75.66 cnf(9342,plain,
% 75.59/75.66 (~P2(f8(a4,a4),f3(a5,a5),a5)),
% 75.59/75.66 inference(scs_inference,[],[9278,9256,9138,8172,8703,8246,8837,29,30,31])).
% 75.59/75.66 cnf(9344,plain,
% 75.59/75.66 (~P2(f8(a4,a4),a2,f3(a2,a2))),
% 75.59/75.66 inference(scs_inference,[],[7,9278,9249,9256,9138,8172,8703,8246,8788,8837,29,30,31,32])).
% 75.59/75.66 cnf(9346,plain,
% 75.59/75.67 (~P2(f3(a5,a5),a4,a5)),
% 75.59/75.67 inference(scs_inference,[],[7,9278,9249,9256,8881,9138,8172,8166,8703,8145,8246,8788,8837,8447,29,30,31,32,33])).
% 75.59/75.67 cnf(9348,plain,
% 75.59/75.67 (~P2(f6(a1),a7,a5)),
% 75.59/75.67 inference(scs_inference,[],[7,9278,9249,9256,9331,8881,9138,8172,8166,8703,8145,8246,8788,8170,8127,8837,8447,29,30,31,32,33,34])).
% 75.59/75.67 cnf(9350,plain,
% 75.59/75.67 (~P4(a1,a4,a1)),
% 75.59/75.67 inference(scs_inference,[],[7,9278,9249,9256,9331,8881,9138,8172,8166,8703,8145,8246,8788,8170,8127,8837,8447,29,30,31,32,33,34,6881])).
% 75.59/75.67 cnf(9352,plain,
% 75.59/75.67 (P2(f9(a4),a4,a4)),
% 75.59/75.67 inference(scs_inference,[],[7,9278,9249,9256,9331,8881,9138,8172,8166,8703,8145,8246,8788,8170,8127,8837,8447,2,29,30,31,32,33,34,6881,24])).
% 75.59/75.67 cnf(9354,plain,
% 75.59/75.67 (P2(a5,f9(a4),a5)),
% 75.59/75.67 inference(scs_inference,[],[7,9278,9249,9256,9331,8881,9138,8172,8166,8703,8145,8246,8788,8170,8127,8837,8447,2,29,30,31,32,33,34,6881,24,347])).
% 75.59/75.67 cnf(9356,plain,
% 75.59/75.67 (P2(a4,f9(a4),a4)),
% 75.59/75.67 inference(scs_inference,[],[7,9278,9249,9256,9331,8881,9138,8172,8166,8703,8145,8246,8788,8170,8127,8837,8447,2,29,30,31,32,33,34,6881,24,347,27])).
% 75.59/75.67 cnf(9360,plain,
% 75.59/75.67 (P2(f9(a4),a5,a5)),
% 75.59/75.67 inference(scs_inference,[],[9354,27])).
% 75.59/75.67 cnf(9362,plain,
% 75.59/75.67 (~P4(a10,f6(a10),a4)),
% 75.59/75.67 inference(scs_inference,[],[9350,9354,7920,8776,27,29])).
% 75.59/75.67 cnf(9364,plain,
% 75.59/75.67 (~P2(f9(a4),f8(a4,a4),f3(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9350,9239,9354,9356,7920,8776,8248,27,29,31])).
% 75.59/75.67 cnf(9366,plain,
% 75.59/75.67 (~P4(f6(a1),a4,a1)),
% 75.59/75.67 inference(scs_inference,[],[9350,9239,9354,9356,7920,8776,8129,8248,8077,27,29,31,30])).
% 75.59/75.67 cnf(9368,plain,
% 75.59/75.67 (~P2(f9(a4),f3(a4,a4),f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9350,9239,9354,9356,7920,8776,8129,8248,8077,27,29,31,30,32])).
% 75.59/75.67 cnf(9372,plain,
% 75.59/75.67 (~P4(f6(a1),f9(a4),f3(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9350,9239,9325,9354,9356,9168,9206,8573,8166,7920,8776,8641,8129,8422,8248,8077,27,29,31,30,32,33,34])).
% 75.59/75.67 cnf(9378,plain,
% 75.59/75.67 (~P4(a4,f6(a1),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9362,9313,8252,8988,26,29])).
% 75.59/75.67 cnf(9380,plain,
% 75.59/75.67 (~P2(a7,a1,f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9317,9352,9362,9313,8252,8988,8447,26,29,31])).
% 75.59/75.67 cnf(9382,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f8(a4,a4),a1)),
% 75.59/75.67 inference(scs_inference,[],[9317,9352,9362,9313,9338,8503,8252,8741,8988,8447,26,29,31,30])).
% 75.59/75.67 cnf(9386,plain,
% 75.59/75.67 (~P4(f9(a4),f6(a4),a5)),
% 75.59/75.67 inference(scs_inference,[],[9317,8826,9352,9362,9313,9338,9164,8503,8252,8741,8988,8447,261,3770,26,29,31,30,32,33])).
% 75.59/75.67 cnf(9393,plain,
% 75.59/75.67 (~P2(f9(a4),a5,f3(a5,a5))),
% 75.59/75.67 inference(scs_inference,[],[9342,9360,9212,9338,8831,29,31])).
% 75.59/75.67 cnf(9395,plain,
% 75.59/75.67 (~P4(f8(a4,a4),f8(a1,a1),a1)),
% 75.59/75.67 inference(scs_inference,[],[9342,9360,9212,9338,8757,8831,8288,29,31,30])).
% 75.59/75.67 cnf(9397,plain,
% 75.59/75.67 (~P2(f9(a4),a2,f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[7,9342,9348,9360,9212,9338,8757,8831,8288,29,31,30,32])).
% 75.59/75.67 cnf(9399,plain,
% 75.59/75.67 (~P2(f8(a1,a1),f6(a1),f6(a5))),
% 75.59/75.67 inference(scs_inference,[],[7,9342,9348,9360,9212,8945,9338,8757,8266,8831,8288,9039,29,31,30,32,33])).
% 75.59/75.67 cnf(9401,plain,
% 75.59/75.67 (P2(f3(a5,a5),f9(a4),f3(a5,a5))),
% 75.59/75.67 inference(scs_inference,[],[7,9342,9348,9360,9212,8945,9338,9354,8757,8266,8831,8288,9039,8127,29,31,30,32,33,34])).
% 75.59/75.67 cnf(9403,plain,
% 75.59/75.67 (P2(f9(a4),f3(a5,a5),f3(a5,a5))),
% 75.59/75.67 inference(scs_inference,[],[7,9342,9348,9360,9212,8945,9338,9354,8757,8266,8831,8288,9039,8127,29,31,30,32,33,34,27])).
% 75.59/75.67 cnf(9405,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f3(a4,a4),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9372,8786,8292,29])).
% 75.59/75.67 cnf(9407,plain,
% 75.59/75.67 (~P2(f9(a4),f3(a5,a5),f3(a5,a1))),
% 75.59/75.67 inference(scs_inference,[],[9301,9403,9372,9212,8786,8292,29,31])).
% 75.59/75.67 cnf(9409,plain,
% 75.59/75.67 (~P4(a4,a1,f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9301,9266,9403,9372,9212,8786,8814,8292,8051,29,31,30])).
% 75.59/75.67 cnf(9413,plain,
% 75.59/75.67 (~P2(f9(a4),a4,f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9301,9266,9146,9403,9372,9057,9142,9212,9356,9352,8786,8342,8814,8292,8422,8051,29,31,30,32,33])).
% 75.59/75.67 cnf(9415,plain,
% 75.59/75.67 (~P4(f9(a4),a1,f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9301,9266,9146,9403,9372,9126,9057,9142,9124,9212,9356,9352,8786,8342,8814,8292,8422,8051,8447,29,31,30,32,33,34])).
% 75.59/75.67 cnf(9422,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f9(a4),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9401,9407,9033,9415,9403,9126,9142,8303,2749,29,31,30])).
% 75.59/75.67 cnf(9424,plain,
% 75.59/75.67 (~P2(f3(a2,a2),f9(a4),a2)),
% 75.59/75.67 inference(scs_inference,[],[9401,9407,9033,9415,9235,9403,9126,8619,9142,9352,8303,2749,29,31,30,32])).
% 75.59/75.67 cnf(9428,plain,
% 75.59/75.67 (~P4(f9(a4),f8(a1,a1),f3(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[8931,9401,9364,9407,9033,9415,9235,9154,9403,9126,8619,9354,9142,9206,9352,8303,8871,8428,2749,29,31,30,32,33,34])).
% 75.59/75.67 cnf(9430,plain,
% 75.59/75.67 (~P4(f8(a4,a4),a2,a2)),
% 75.59/75.67 inference(scs_inference,[],[9338,8720,29])).
% 75.59/75.67 cnf(9432,plain,
% 75.59/75.67 (~P2(f9(a4),a5,f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9144,9122,9360,9338,8720,29,31])).
% 75.59/75.67 cnf(9436,plain,
% 75.59/75.67 (~P2(f3(a5,a5),f9(a4),a5)),
% 75.59/75.67 inference(scs_inference,[],[9174,9208,9144,9122,9401,9360,9124,8739,9338,8016,8720,29,31,30,32])).
% 75.59/75.67 cnf(9438,plain,
% 75.59/75.67 (~P2(f3(a4,a4),f9(a4),f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9174,9196,9208,9144,9122,9401,9360,9124,8739,9338,8016,9356,8720,8051,29,31,30,32,33])).
% 75.59/75.67 cnf(9440,plain,
% 75.59/75.67 (~P4(f9(a4),f9(a4),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9174,9196,9208,9393,9144,9122,9401,9360,9124,8739,9338,8016,9356,8720,8127,8051,29,31,30,32,33,34])).
% 75.59/75.67 cnf(9446,plain,
% 75.59/75.67 (~P2(a2,f8(a4,a4),f3(a2,a2))),
% 75.59/75.67 inference(scs_inference,[],[9405,9344,9120,8408,8774,8449,29,31])).
% 75.59/75.67 cnf(9448,plain,
% 75.59/75.67 (~P4(f6(a5),f8(a1,a1),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9405,9344,9237,9120,8408,8939,8774,8117,8449,29,31,30])).
% 75.59/75.67 cnf(9450,plain,
% 75.59/75.67 (~P2(f8(a4,a4),f3(a4,a4),a4)),
% 75.59/75.67 inference(scs_inference,[],[9245,9405,9344,9237,9120,8231,8250,8408,8939,8774,8117,8449,29,31,30,32])).
% 75.59/75.67 cnf(9452,plain,
% 75.59/75.67 (~P2(f9(a4),a4,f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9245,9405,9344,9378,9237,9184,9120,8231,8718,8250,9352,8408,8939,8774,8117,8449,29,31,30,32,33])).
% 75.59/75.67 cnf(9454,plain,
% 75.59/75.67 (~P4(f9(a4),f9(a4),f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9245,9405,9438,9344,9378,9237,9184,9122,9120,8231,8718,8250,9352,8408,8939,8774,8051,8117,8449,29,31,30,32,33,34])).
% 75.59/75.67 cnf(9456,plain,
% 75.59/75.67 (~P4(f6(a4),f3(a4,a4),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9327,8229,8077,29])).
% 75.59/75.67 cnf(9458,plain,
% 75.59/75.67 (~P2(a4,f9(a4),f3(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9450,9327,8229,9356,8782,8077,29,31])).
% 75.59/75.67 cnf(9460,plain,
% 75.59/75.67 (~P4(f6(a1),f9(a4),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9450,9327,9415,9126,9168,8229,9356,8782,8077,29,31,30])).
% 75.59/75.67 cnf(9464,plain,
% 75.59/75.67 (~P2(f9(a4),a4,f3(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9450,9327,8737,9372,9415,9126,9168,9124,8229,9356,8718,8782,8077,29,31,30,32,33])).
% 75.59/75.67 cnf(9466,plain,
% 75.59/75.67 (~P2(f8(a1,a1),f3(a5,a5),f6(a5))),
% 75.59/75.67 inference(scs_inference,[],[9450,9327,8737,9372,9415,9172,9126,9168,8143,9124,9027,8229,9356,8718,8871,8782,8077,29,31,30,32,33,34])).
% 75.59/75.67 cnf(9474,plain,
% 75.59/75.67 (~P2(f8(a4,a4),f9(a4),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9268,9440,7956,9142,9352,8751,29,31,32])).
% 75.59/75.67 cnf(9476,plain,
% 75.59/75.67 (~P4(f3(a4,a4),f3(a1,a1),f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9268,9221,9440,7956,9142,8229,9352,8751,8089,29,31,32,30])).
% 75.59/75.67 cnf(9478,plain,
% 75.59/75.67 (~P2(f6(a4),a4,a1)),
% 75.59/75.67 inference(scs_inference,[],[9268,9221,9440,7956,9142,8227,8229,9352,8984,8751,8089,8049,29,31,32,30,33])).
% 75.59/75.67 cnf(9480,plain,
% 75.59/75.67 (~P4(a2,f6(a1),f3(a2,a2))),
% 75.59/75.67 inference(scs_inference,[],[9268,9221,9446,9440,7956,9142,8227,8668,8573,8229,9352,8408,8984,8751,8089,8049,29,31,32,30,33,34])).
% 75.59/75.67 cnf(9484,plain,
% 75.59/75.67 (~P4(a2,a1,f3(a2,a2))),
% 75.59/75.67 inference(scs_inference,[],[9480,8404,2749,29])).
% 75.59/75.67 cnf(9486,plain,
% 75.59/75.67 (~P2(f9(a5),a5,f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9299,9480,8181,8404,7936,2749,29,31])).
% 75.59/75.67 cnf(9488,plain,
% 75.59/75.67 (~P4(a5,a4,f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9386,9299,9480,8181,8404,7962,8814,7936,2749,29,31,30])).
% 75.59/75.67 cnf(9490,plain,
% 75.59/75.67 (~P2(f3(a1,a1),f9(a5),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9386,9272,9299,9480,8181,8404,8109,7962,9356,8814,7936,2749,29,31,30,32])).
% 75.59/75.67 cnf(9492,plain,
% 75.59/75.67 (~P4(f9(a4),f6(a4),f6(a5))),
% 75.59/75.67 inference(scs_inference,[],[9386,8923,9272,9299,9480,8181,8404,8109,7962,9356,8814,9352,8812,7936,3770,2749,29,31,30,32,33])).
% 75.59/75.67 cnf(9494,plain,
% 75.59/75.67 (~P4(f3(a1,a1),f3(a4,a4),f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9476,9386,8923,9272,9299,9480,8181,8404,8109,7962,9356,8814,9352,8812,7936,3770,2749,29,31,30,32,33,26])).
% 75.59/75.67 cnf(9501,plain,
% 75.59/75.67 (~P2(f3(a1,a1),a1,f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9474,8414,7946,8307,8449,3660,29,31])).
% 75.59/75.67 cnf(9522,plain,
% 75.59/75.67 (~P2(f9(a4),f8(a4,a4),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9085,9422,9413,9440,7996,9206,9142,9168,8666,8103,8585,8288,9352,8428,31,29,30,32,33])).
% 75.59/75.67 cnf(9524,plain,
% 75.59/75.67 (~P2(a1,f9(a5),f6(a4))),
% 75.59/75.67 inference(scs_inference,[],[9085,9422,9329,9413,9440,7996,9206,8137,9142,9168,8666,8488,8103,8585,8288,8984,9352,8428,31,29,30,32,33,34])).
% 75.59/75.67 cnf(9526,plain,
% 75.59/75.67 (~P4(f9(a4),a1,a1)),
% 75.59/75.67 inference(scs_inference,[],[9085,9422,9329,9413,9440,7996,9206,8137,9142,9168,8666,8488,8103,8585,8288,8984,9352,8428,31,29,30,32,33,34,2755])).
% 75.59/75.67 cnf(9528,plain,
% 75.59/75.67 (~P4(a1,f9(a4),a1)),
% 75.59/75.67 inference(scs_inference,[],[9085,9422,9329,9413,9440,7996,9206,8137,9142,9168,8666,8488,8103,8585,8288,8984,9352,8428,31,29,30,32,33,34,2755,6883])).
% 75.59/75.67 cnf(9530,plain,
% 75.59/75.67 (P2(f8(a10,a10),f9(a4),f8(a10,a10))),
% 75.59/75.67 inference(scs_inference,[],[9085,9422,9329,9413,9440,7996,9206,8137,9142,9168,8666,8488,8103,8585,8288,8984,9352,8428,31,29,30,32,33,34,2755,6883,27])).
% 75.59/75.67 cnf(9534,plain,
% 75.59/75.67 (~P2(f9(a5),f3(a5,a5),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9043,9458,8181,8147,27,31])).
% 75.59/75.67 cnf(9536,plain,
% 75.59/75.67 (~P4(f6(a5),f6(a1),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9043,9055,9458,8181,8210,8147,8077,27,31,29])).
% 75.59/75.67 cnf(9542,plain,
% 75.59/75.67 (~P2(a4,a1,f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9043,9055,9492,9522,9382,9458,8181,8210,8147,8354,8129,8424,8814,8087,8428,8077,3660,27,31,29,32,30,33])).
% 75.59/75.67 cnf(9546,plain,
% 75.59/75.67 (~P2(a4,f3(a4,a4),a4)),
% 75.59/75.67 inference(scs_inference,[],[9464,8195,9352,31])).
% 75.59/75.67 cnf(9552,plain,
% 75.59/75.67 (~P4(a1,a2,f3(a2,a2))),
% 75.59/75.67 inference(scs_inference,[],[9484,9526,9464,8629,8195,8168,8831,8151,9356,9352,31,29,32,30])).
% 75.59/75.67 cnf(9554,plain,
% 75.59/75.67 (~P2(f3(a4,a4),f8(a4,a4),a4)),
% 75.59/75.67 inference(scs_inference,[],[9484,9526,9290,9464,8629,8195,8168,8796,8250,8831,8151,9356,9352,8428,31,29,32,30,33])).
% 75.59/75.67 cnf(9565,plain,
% 75.59/75.67 (~P2(f9(a4),f3(a5,a5),a5)),
% 75.59/75.67 inference(scs_inference,[],[9059,9256,9403,9212,27,31])).
% 75.59/75.67 cnf(9569,plain,
% 75.59/75.67 (~P4(a1,f8(a4,a4),a1)),
% 75.59/75.67 inference(scs_inference,[],[9059,9395,9526,9256,9403,9212,8757,8246,8776,27,31,29,30])).
% 75.59/75.67 cnf(9571,plain,
% 75.59/75.67 (~P2(f8(a4,a4),f9(a4),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9059,9395,9452,9526,9256,9403,9212,9124,8757,8246,8776,27,31,29,30,32])).
% 75.59/75.67 cnf(9573,plain,
% 75.59/75.67 (~P4(f9(a4),f8(a1,a1),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9059,9395,9452,9526,9256,9154,9403,9212,9124,8757,8246,8776,8422,27,31,29,30,32,34])).
% 75.59/75.67 cnf(9575,plain,
% 75.59/75.67 (~P2(f8(a1,a1),a2,f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9059,9395,9452,9430,9526,9256,9154,9403,9212,9124,8757,8246,8776,8360,9039,8422,27,31,29,30,32,34,33])).
% 75.59/75.67 cnf(9579,plain,
% 75.59/75.67 (~P2(f9(a5),a5,f3(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9546,8181,7936,31])).
% 75.59/75.67 cnf(9583,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f9(a4),a1)),
% 75.59/75.67 inference(scs_inference,[],[9528,9546,8181,9120,8720,8151,7936,8449,31,29,30])).
% 75.59/75.67 cnf(9585,plain,
% 75.59/75.67 (~P2(a4,a4,f3(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9528,9546,9554,8181,9120,8720,8151,8400,8674,7936,8449,31,29,30,32])).
% 75.59/75.67 cnf(9595,plain,
% 75.59/75.67 (~P2(a5,f9(a4),f3(a5,a5))),
% 75.59/75.67 inference(scs_inference,[],[9534,9122,7936,31])).
% 75.59/75.67 cnf(9597,plain,
% 75.59/75.67 (~P4(a1,a1,f6(a4))),
% 75.59/75.67 inference(scs_inference,[],[9534,9148,9122,8091,8988,7936,31,29])).
% 75.59/75.67 cnf(9601,plain,
% 75.59/75.67 (~P2(a2,a10,f3(a5,a5))),
% 75.59/75.67 inference(scs_inference,[],[8,9534,9148,9346,9526,9122,9126,8091,9168,7922,8988,7936,31,29,30,32])).
% 75.59/75.67 cnf(9607,plain,
% 75.59/75.67 (~P2(f8(a4,a4),f3(a2,a2),a2)),
% 75.59/75.67 inference(scs_inference,[],[9344,8254,8837,31])).
% 75.59/75.67 cnf(9609,plain,
% 75.59/75.67 (~P4(f8(a4,a4),f8(a1,a1),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9344,9138,8254,8741,8837,31,29])).
% 75.59/75.67 cnf(9611,plain,
% 75.59/75.67 (~P4(f8(a1,a1),a5,f3(a5,a5))),
% 75.59/75.67 inference(scs_inference,[],[9225,9344,9138,8254,8935,8741,8939,8837,31,29,30])).
% 75.59/75.67 cnf(9613,plain,
% 75.59/75.67 (~P2(a4,f3(a5,a5),f3(a5,a1))),
% 75.59/75.67 inference(scs_inference,[],[9225,9053,9344,8223,9138,8254,8260,8935,8741,8939,8837,31,29,30,32])).
% 75.59/75.67 cnf(9615,plain,
% 75.59/75.67 (~P4(f8(a4,a4),f8(a4,a4),a4)),
% 75.59/75.67 inference(scs_inference,[],[9225,9585,9053,9344,8223,9138,8254,8260,8935,8741,8939,8235,8837,8751,31,29,30,32,34])).
% 75.59/75.67 cnf(9622,plain,
% 75.59/75.67 (~P2(f9(a4),f8(a4,a4),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9571,9212,9206,31])).
% 75.59/75.67 cnf(9624,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f6(a5),a1)),
% 75.59/75.67 inference(scs_inference,[],[9611,9571,9212,9206,8145,8887,31,29])).
% 75.59/75.67 cnf(9628,plain,
% 75.59/75.67 (~P2(f8(a1,a1),a10,f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9288,9611,9571,9100,9212,9206,8145,8342,8887,8129,9356,8077,31,29,30,32])).
% 75.59/75.67 cnf(9630,plain,
% 75.59/75.67 (~P4(a1,f6(a4),a1)),
% 75.59/75.67 inference(scs_inference,[],[9288,9611,9571,9100,9478,9212,9206,8145,8342,8887,8129,9356,8447,8077,1353,3770,31,29,30,32,34])).
% 75.59/75.67 cnf(9636,plain,
% 75.59/75.67 (~P4(f9(a4),f6(a1),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9573,9486,9154,8147,8354,8303,31,29])).
% 75.59/75.67 cnf(9638,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f9(a4),f3(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9428,9573,9486,9154,8147,9142,8354,8303,31,29,30])).
% 75.59/75.67 cnf(9640,plain,
% 75.59/75.67 (~P2(f3(a4,a4),a4,f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9428,9573,9486,9464,9154,8227,8147,9142,8354,8303,8400,31,29,30,32])).
% 75.59/75.67 cnf(9652,plain,
% 75.59/75.67 (~P4(f6(a10),f6(a4),f6(a10))),
% 75.59/75.67 inference(scs_inference,[],[9630,8206,9526,8776,8720,9352,31,29,30])).
% 75.59/75.67 cnf(9654,plain,
% 75.59/75.67 (~P2(f3(a5,a5),f9(a5),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9630,9640,8206,8258,9526,8137,8776,8720,9352,31,29,30,32])).
% 75.59/75.67 cnf(9658,plain,
% 75.59/75.67 (~P2(a5,a4,f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9630,9280,9640,9346,8206,8258,9526,8137,8652,8166,8776,8720,8887,8812,8422,9352,31,29,30,32,34,33])).
% 75.59/75.67 cnf(9662,plain,
% 75.59/75.67 (~P2(f3(a4,a4),f6(a1),f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9276,27])).
% 75.59/75.67 cnf(9668,plain,
% 75.59/75.67 (~P4(f8(a1,a1),a5,f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9276,9613,9624,9652,8075,8286,8384,8848,7926,8449,27,31,29,30])).
% 75.59/75.67 cnf(9670,plain,
% 75.59/75.67 (~P2(f3(a1,a1),f8(a4,a4),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9276,9622,9613,9624,9652,8075,8286,8322,8384,8848,7926,8837,8449,27,31,29,30,32])).
% 75.59/75.67 cnf(9672,plain,
% 75.59/75.67 (~P4(f9(a5),f9(a5),f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[9276,9622,9613,9579,9624,9652,8075,8286,8322,8384,8848,7926,8837,8051,7936,8449,27,31,29,30,32,34])).
% 75.59/75.67 cnf(9674,plain,
% 75.59/75.67 (~P2(f3(a4,a4),f9(a5),f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[9276,9622,9613,9579,9624,9652,8755,8075,8286,8322,8384,8848,7926,8837,8235,8051,7936,8449,27,31,29,30,32,34,33])).
% 75.59/75.67 cnf(9676,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f8(a4,a4),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9609,9276,9622,9613,9579,9624,9652,8755,8075,8286,8322,8384,8848,7926,8837,8235,8051,7936,8449,27,31,29,30,32,34,33,26])).
% 75.59/75.67 cnf(9678,plain,
% 75.59/75.67 (~P2(f3(a4,a4),f6(a1),a4)),
% 75.59/75.67 inference(scs_inference,[],[9662,8573,8248,31])).
% 75.59/75.67 cnf(9686,plain,
% 75.59/75.67 (~P2(f6(a1),a10,a5)),
% 75.59/75.67 inference(scs_inference,[],[8,9601,9662,9597,8637,9480,8668,8573,8434,8170,8248,9356,8127,8089,31,29,30,32,34])).
% 75.59/75.67 cnf(9688,plain,
% 75.59/75.67 (~P2(f8(a1,a1),f9(a4),a5)),
% 75.59/75.67 inference(scs_inference,[],[8,9601,9488,9662,9597,8637,9480,9122,8668,8573,8434,8170,9039,8248,9356,8127,8089,31,29,30,32,34,33])).
% 75.59/75.67 cnf(9692,plain,
% 75.59/75.67 (~P2(f9(a5),f3(a1,a1),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9490,27])).
% 75.59/75.67 cnf(9694,plain,
% 75.59/75.67 (P2(a2,f8(a10,a10),f8(a5,a10))),
% 75.59/75.67 inference(scs_inference,[],[8,9490,3873,7932,27,31])).
% 75.59/75.67 cnf(9696,plain,
% 75.59/75.67 (~P4(f9(a5),f8(a1,a1),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[8,9490,9672,9295,3873,7932,27,31,29])).
% 75.59/75.67 cnf(9700,plain,
% 75.59/75.67 (~P2(a4,a5,f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[8,9490,9672,9063,9432,9295,9360,9122,7940,7962,3873,7932,27,31,29,30,32])).
% 75.59/75.67 cnf(9706,plain,
% 75.59/75.67 (P2(f8(a10,a10),a2,f8(a5,a10))),
% 75.59/75.67 inference(scs_inference,[],[9694,27])).
% 75.59/75.67 cnf(9708,plain,
% 75.59/75.67 (~P2(f8(a1,a1),x97081,f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[9674,9694,8354,27,31])).
% 75.59/75.67 cnf(9710,plain,
% 75.59/75.67 (~P4(f9(a5),f6(a1),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9674,9694,9672,8309,8354,27,31,29])).
% 75.59/75.67 cnf(9712,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f9(a5),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9696,9674,9694,9303,9295,9672,8309,8354,27,31,29,30])).
% 75.59/75.67 cnf(9714,plain,
% 75.59/75.67 (~P2(a2,a4,f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[8,9686,9696,9674,9694,9303,9295,9672,8309,7916,8354,27,31,29,30,32])).
% 75.59/75.67 cnf(9716,plain,
% 75.59/75.67 (~P4(f3(a4,a4),f6(a1),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[8,9686,9696,9674,9694,9303,9640,9295,9672,8309,8227,8252,8718,7916,8354,27,31,29,30,32,34])).
% 75.59/75.67 cnf(9718,plain,
% 75.59/75.67 (~P2(f9(a5),a4,f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[8,9686,9696,9674,9694,9303,9640,9295,9672,8258,8309,8227,8252,8718,7916,8354,8422,27,31,29,30,32,34,33])).
% 75.59/75.67 cnf(9720,plain,
% 75.59/75.67 (~P4(f9(a5),a1,a1)),
% 75.59/75.67 inference(scs_inference,[],[8,9686,9696,9674,9694,9303,9640,9295,9672,8258,8309,8227,8252,8718,7916,8354,8422,27,31,29,30,32,34,33,2755])).
% 75.59/75.67 cnf(9722,plain,
% 75.59/75.67 (~P4(a1,f9(a5),a1)),
% 75.59/75.67 inference(scs_inference,[],[8,9686,9696,9674,9694,9303,9640,9295,9672,8258,8309,8227,8252,8718,7916,8354,8422,27,31,29,30,32,34,33,2755,6883])).
% 75.59/75.67 cnf(9732,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f9(a5),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9424,9192,9710,8324,9295,7940,8089,27,29,30])).
% 75.59/75.67 cnf(9734,plain,
% 75.59/75.67 (P2(f8(a5,a10),f9(a4),f8(a5,a10))),
% 75.59/75.67 inference(scs_inference,[],[9530,9424,9192,9710,8324,9694,9295,7940,8089,27,29,30,32])).
% 75.59/75.67 cnf(9738,plain,
% 75.59/75.67 (~P2(f9(a5),a4,f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9530,9424,9192,9710,9542,8324,9694,9295,8258,7940,8718,8837,8248,8089,27,29,30,32,31,33])).
% 75.59/75.67 cnf(9740,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f8(a1,a1),f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[9530,9424,9708,9192,9710,9542,8324,9694,9295,8258,7940,8103,8718,8837,8248,8422,8089,27,29,30,32,31,33,34])).
% 75.59/75.67 cnf(9743,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f6(a4),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9530,9424,9311,9708,9192,9710,9542,8324,9694,9295,8258,7940,8103,8718,8837,8248,8422,8089,27,29,30,32,31,33,34,26])).
% 75.59/75.67 cnf(9745,plain,
% 75.59/75.67 (P2(f9(a4),f8(a5,a10),f8(a5,a10))),
% 75.59/75.67 inference(scs_inference,[],[9734,27])).
% 75.59/75.67 cnf(9747,plain,
% 75.59/75.67 (~P4(f9(a5),a7,a7)),
% 75.59/75.67 inference(scs_inference,[],[9720,9734,8831,27,29])).
% 75.59/75.67 cnf(9749,plain,
% 75.59/75.67 (~P4(f9(a5),f3(a1,a1),a1)),
% 75.59/75.67 inference(scs_inference,[],[9720,9734,8623,8831,8089,27,29,30])).
% 75.59/75.67 cnf(9751,plain,
% 75.59/75.67 (~P2(f9(a4),f3(a4,a4),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9720,9654,9734,8623,9403,8137,8831,8089,27,29,30,32])).
% 75.59/75.67 cnf(9753,plain,
% 75.59/75.67 (P2(f8(a10,a10),f8(a2,a2),f8(a5,a5))),
% 75.59/75.67 inference(scs_inference,[],[9720,9706,9654,9734,8650,8623,9403,7972,8137,8831,8089,27,29,30,32,31])).
% 75.59/75.67 cnf(9755,plain,
% 75.59/75.67 (~P2(a1,a4,f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9720,9615,9706,9654,9734,8650,8623,9403,7972,8137,8831,8246,8751,8782,8089,27,29,30,32,31,33])).
% 75.59/75.67 cnf(9757,plain,
% 75.59/75.67 (~P4(f9(a5),a1,f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9720,9615,9706,9654,9718,9734,8650,8623,9403,7972,8137,8258,8831,8246,8751,8782,8447,8089,27,29,30,32,31,33,34])).
% 75.59/75.67 cnf(9764,plain,
% 75.59/75.67 (~P4(f8(a1,a1),a1,f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[9380,9740,9303,8268,27,29])).
% 75.59/75.67 cnf(9766,plain,
% 75.59/75.67 (~P4(a1,f8(a4,a4),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9676,9380,9740,9303,8268,8741,27,29,30])).
% 75.59/75.67 cnf(9768,plain,
% 75.59/75.67 (~P2(a5,f8(a4,a4),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9676,9380,9740,9688,9303,9354,9212,8268,8741,27,29,30,32])).
% 75.59/75.67 cnf(9772,plain,
% 75.59/75.67 (~P2(f9(a5),f8(a4,a4),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9676,9380,9712,9740,9688,9700,9303,9295,9354,8346,9212,8268,8384,8741,8428,3763,27,29,30,32,31,33])).
% 75.59/75.67 cnf(9774,plain,
% 75.59/75.67 (~P2(a1,f8(a4,a4),a4)),
% 75.59/75.67 inference(scs_inference,[],[9676,9380,9315,9712,9740,9688,9700,9303,9295,9354,8346,9027,9212,8268,8384,8741,8428,3763,27,29,30,32,31,33,34])).
% 75.59/75.67 cnf(9778,plain,
% 75.59/75.67 (~P4(f3(a4,a4),a1,f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9753,9716,9184,2749,27,29])).
% 75.59/75.67 cnf(9782,plain,
% 75.59/75.67 (~P2(f9(a5),f3(a5,a5),a4)),
% 75.59/75.67 inference(scs_inference,[],[9753,9716,8875,9458,9401,9184,8488,8147,8641,2749,27,29,30,32])).
% 75.59/75.67 cnf(9788,plain,
% 75.59/75.67 (~P4(f9(a5),f6(a1),f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9753,9692,9772,9716,8875,9458,8324,9401,9184,8346,8488,9122,8147,8250,8641,8252,8573,7936,2749,27,29,30,32,31,33,34])).
% 75.59/75.67 cnf(9795,plain,
% 75.59/75.67 (~P4(f8(a4,a4),a1,f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9466,9609,9720,8503,8776,8434,27,29,30])).
% 75.59/75.67 cnf(9797,plain,
% 75.59/75.67 (~P2(f8(a4,a4),f9(a5),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9466,9738,9609,9720,8755,8503,8258,8776,8434,27,29,30,32])).
% 75.59/75.67 cnf(9799,plain,
% 75.59/75.67 (~P2(a4,f8(a1,a1),a4)),
% 75.59/75.67 inference(scs_inference,[],[9466,9738,9609,9299,9720,8755,8503,8258,8342,8776,8434,8400,27,29,30,32,31])).
% 75.59/75.67 cnf(9803,plain,
% 75.59/75.67 (~P4(f6(a1),f9(a4),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[10,9466,9636,9738,9609,9299,9720,8755,8503,9027,8258,8342,8776,8434,8424,8400,27,29,30,32,31,33,26])).
% 75.59/75.67 cnf(9811,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f6(a1),f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[9764,8623,8077,29])).
% 75.59/75.67 cnf(9817,plain,
% 75.59/75.67 (~P2(f3(a4,a4),f8(a1,a1),a4)),
% 75.59/75.67 inference(scs_inference,[],[9766,9764,9799,9714,8623,8195,8368,8246,8718,8354,8077,29,30,32,31])).
% 75.59/75.67 cnf(9826,plain,
% 75.59/75.67 (~P4(f9(a5),f8(a1,a1),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9732,9303,9295,29])).
% 75.59/75.67 cnf(9830,plain,
% 75.59/75.67 (~P2(f3(a1,a1),f9(a4),f6(a5))),
% 75.59/75.67 inference(scs_inference,[],[9732,9778,8949,9303,9295,8666,8091,8229,9352,29,30,32])).
% 75.59/75.67 cnf(9832,plain,
% 75.59/75.67 (~P2(a4,f6(a1),a2)),
% 75.59/75.67 inference(scs_inference,[],[9397,9732,9778,8949,9303,9295,8666,8266,8091,8229,9352,29,30,32,31])).
% 75.59/75.67 cnf(9834,plain,
% 75.59/75.67 (~P2(f9(a5),f8(a4,a4),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9397,9732,9778,8949,9303,9295,8666,8266,8091,8346,8229,9352,8428,29,30,32,31,33])).
% 75.59/75.67 cnf(9838,plain,
% 75.59/75.67 (~P4(f9(a5),a2,a2)),
% 75.59/75.67 inference(scs_inference,[],[9720,8720,29])).
% 75.59/75.67 cnf(9842,plain,
% 75.59/75.67 (~P2(f8(a4,a4),a4,a1)),
% 75.59/75.67 inference(scs_inference,[],[9788,9755,9720,8324,8183,8720,8751,8400,29,30,32])).
% 75.59/75.67 cnf(9844,plain,
% 75.59/75.67 (~P2(f8(a4,a4),f6(a1),f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[9788,9797,9755,9720,8324,8183,8368,8720,8837,8751,8400,29,30,32,31])).
% 75.59/75.67 cnf(9846,plain,
% 75.59/75.67 (~P2(a4,a4,f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9788,9797,9456,9755,9720,8324,8183,8368,8227,8720,8988,8837,8751,8400,3770,29,30,32,31,33])).
% 75.59/75.67 cnf(9848,plain,
% 75.59/75.67 (~P4(a1,a1,f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9788,9797,9456,9755,9720,8324,8183,8368,8227,8720,8988,8837,8751,8400,8447,7136,3770,29,30,32,31,33,34])).
% 75.59/75.67 cnf(9854,plain,
% 75.59/75.67 (~P4(a1,f9(a4),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9803,9811,8183,9168,8449,2749,29,30])).
% 75.59/75.67 cnf(9856,plain,
% 75.59/75.67 (~P2(a4,f6(a1),f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[9803,9811,9834,8183,9168,8266,8573,8449,2749,29,30,32])).
% 75.59/75.67 cnf(9862,plain,
% 75.59/75.67 (~P4(a4,f8(a1,a1),a1)),
% 75.59/75.67 inference(scs_inference,[],[9454,9803,9811,9834,9842,9832,8757,8183,9206,9168,8266,8718,8573,8248,8422,8782,8449,2749,29,30,32,31,33,34])).
% 75.59/75.67 cnf(9872,plain,
% 75.59/75.67 (~P2(a4,f9(a5),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9826,9844,9749,8340,9303,8181,8210,8309,9356,8782,8449,30,29,32,31])).
% 75.59/75.67 cnf(9876,plain,
% 75.59/75.67 (~P2(f8(a1,a1),f9(a4),f6(a5))),
% 75.59/75.67 inference(scs_inference,[],[9757,9826,9436,9844,9749,8340,9401,9303,8181,8210,8309,8652,8871,8043,8087,8424,9356,8782,8449,30,29,32,31,33,34])).
% 75.59/75.67 cnf(9878,plain,
% 75.59/75.67 (P2(f9(a4),f8(a7,a7),f8(a7,a7))),
% 75.59/75.67 inference(scs_inference,[],[9757,9826,9436,9844,9749,8340,9401,9303,8181,8210,8309,8652,8871,8043,8087,8424,9356,8782,8449,30,29,32,31,33,34,27])).
% 75.59/75.67 cnf(9882,plain,
% 75.59/75.67 (~P4(a4,a5,a5)),
% 75.59/75.67 inference(scs_inference,[],[9399,9107,8848,27,29])).
% 75.59/75.67 cnf(9888,plain,
% 75.59/75.67 (P2(f9(a4),f8(a5,a7),f8(a5,a7))),
% 75.59/75.67 inference(scs_inference,[],[9399,9878,9795,9658,8039,9107,8503,7922,8848,8089,8,27,29,30,32,31])).
% 75.59/75.67 cnf(9892,plain,
% 75.59/75.67 (~P2(f8(a1,a1),f3(a5,a5),f6(a4))),
% 75.59/75.67 inference(scs_inference,[],[9399,9878,9795,9782,9658,9676,8039,9107,8503,9295,7922,8147,8848,8988,8741,8751,8422,8089,8,27,29,30,32,31,33,34])).
% 75.59/75.67 cnf(9894,plain,
% 75.59/75.67 (P2(f8(a5,a7),f9(a4),f8(a5,a7))),
% 75.59/75.67 inference(scs_inference,[],[9888,27])).
% 75.59/75.67 cnf(9896,plain,
% 75.59/75.67 (~P4(a1,f3(a1,a1),f6(a4))),
% 75.59/75.67 inference(scs_inference,[],[9743,9888,8113,8449,27,29])).
% 75.59/75.67 cnf(9902,plain,
% 75.59/75.67 (~P2(f6(a1),a4,f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[9743,9774,9888,9856,9366,8113,8266,9039,8043,8718,8837,8674,8449,27,29,30,32,31])).
% 75.59/75.67 cnf(9906,plain,
% 75.59/75.67 (~P2(f6(a4),a4,f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9743,9678,9774,9888,9856,9366,9476,8368,8227,8113,8266,8984,9039,8043,8718,8235,8837,8674,8049,8449,27,29,30,32,31,34,33])).
% 75.59/75.67 cnf(9910,plain,
% 75.59/75.67 (~P4(a4,f8(a1,a1),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9862,9262,8288,8077,27,29])).
% 75.59/75.67 cnf(9912,plain,
% 75.59/75.67 (~P4(a4,f6(a4),f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9862,9262,9848,8288,8814,8077,3677,27,29,30])).
% 75.59/75.67 cnf(9914,plain,
% 75.59/75.67 (~P2(f3(a1,a1),a4,f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9862,9262,9848,9622,8322,8288,8814,8248,8077,3677,27,29,30,32])).
% 75.59/75.67 cnf(9918,plain,
% 75.59/75.67 (~P4(a1,f6(a4),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9862,9262,9575,9906,9848,9622,8322,8408,8288,8814,8248,8447,8077,1353,3770,3677,27,29,30,32,31,34])).
% 75.59/75.67 cnf(9920,plain,
% 75.59/75.67 (~P4(f3(a1,a1),f3(a4,a4),a4)),
% 75.59/75.67 inference(scs_inference,[],[9494,9862,9262,9575,9906,9848,9622,8322,8408,8288,8250,8814,8248,8447,8077,1353,3770,3677,27,29,30,32,31,34,33])).
% 75.59/75.67 cnf(9928,plain,
% 75.59/75.67 (~P2(a4,f3(a1,a1),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9670,9409,9526,8109,8149,8322,8002,8089,29,30,32])).
% 75.59/75.67 cnf(9943,plain,
% 75.59/75.67 (~P4(f6(a1),f8(a4,a4),a1)),
% 75.59/75.67 inference(scs_inference,[],[9569,9764,9295,8103,8246,8077,29,30])).
% 75.59/75.67 cnf(9945,plain,
% 75.59/75.67 (~P2(a4,f9(a4),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9569,9914,9764,9122,9295,9124,8103,8246,8077,29,30,32])).
% 75.59/75.67 cnf(9947,plain,
% 75.59/75.67 (~P2(f8(a1,a1),f3(a4,a4),a4)),
% 75.59/75.67 inference(scs_inference,[],[9817,9569,9914,9764,9122,9295,9124,8103,8354,8246,8362,8077,29,30,32,31])).
% 75.59/75.67 cnf(9949,plain,
% 75.59/75.67 (~P4(f8(a1,a1),f6(a1),f8(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9817,9569,9914,9764,9268,9122,9295,9124,8103,8303,8354,8246,8362,8718,8422,8077,29,30,32,31,34])).
% 75.59/75.67 cnf(9951,plain,
% 75.59/75.67 (~P2(f3(a1,a1),a4,f6(a4))),
% 75.59/75.67 inference(scs_inference,[],[9817,9569,9896,9914,9764,9268,8666,9122,9295,9124,8103,8303,8113,8354,8246,8362,8718,8422,8447,8077,29,30,32,31,34,33])).
% 75.59/75.67 cnf(9960,plain,
% 75.59/75.67 (~P4(f6(a1),f9(a4),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9460,8566,9154,8292,27,29])).
% 75.59/75.67 cnf(9962,plain,
% 75.59/75.67 (~P4(a1,a4,f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9460,8566,9910,9154,9027,8292,8129,27,29,30])).
% 75.59/75.67 cnf(9964,plain,
% 75.59/75.67 (~P2(f6(a1),a4,a4)),
% 75.59/75.67 inference(scs_inference,[],[9460,8566,9910,9846,9154,9027,8292,8129,8718,8400,27,29,30,32])).
% 75.59/75.67 cnf(9973,plain,
% 75.59/75.67 (~P4(f9(a5),a5,a5)),
% 75.59/75.67 inference(scs_inference,[],[9720,8848,29])).
% 75.59/75.67 cnf(9977,plain,
% 75.59/75.67 (~P2(f9(a4),f3(a1,a1),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9928,9174,9720,8168,8109,7974,8848,9352,29,30,32])).
% 75.59/75.67 cnf(9997,plain,
% 75.59/75.67 (~P2(a1,a4,f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[8595,9368,9552,9838,9565,9274,9403,9126,9212,8382,7976,8151,8871,7926,8354,8751,8449,29,30,32,31,34,33])).
% 75.59/75.67 cnf(9999,plain,
% 75.59/75.67 (~P4(f3(a1,a1),f6(a4),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9918,8089,1353,29])).
% 75.59/75.67 cnf(10003,plain,
% 75.59/75.67 (P2(f8(a5,a10),f9(a5),a7)),
% 75.59/75.67 inference(scs_inference,[],[9918,9862,8402,9027,9039,7964,8089,3858,1353,29,30,32])).
% 75.59/75.67 cnf(10007,plain,
% 75.59/75.67 (~P4(f9(a4),f6(a1),f3(a4,a4))),
% 75.59/75.67 inference(scs_inference,[],[9607,9918,9862,9364,9184,8402,9206,8360,9027,9039,8573,7964,8782,8089,3858,1353,29,30,32,31,34])).
% 75.59/75.67 cnf(10009,plain,
% 75.59/75.67 (~P2(a5,a4,f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9607,9918,9862,9364,8978,9184,8402,9206,8166,8360,9027,8871,8812,9039,8573,7964,8782,8089,3858,1353,29,30,32,31,34,33])).
% 75.59/75.67 cnf(10011,plain,
% 75.59/75.67 (P2(f9(a5),f8(a5,a10),a7)),
% 75.59/75.67 inference(scs_inference,[],[9607,9918,9862,9364,8978,9184,8402,9206,8166,8360,9027,8871,8812,9039,8573,7964,8782,8089,3858,1353,29,30,32,31,34,33,27])).
% 75.59/75.67 cnf(10014,plain,
% 75.59/75.67 (~P2(f9(a5),a1,f6(a4))),
% 75.59/75.67 inference(scs_inference,[],[9524,27])).
% 75.59/75.67 cnf(10016,plain,
% 75.59/75.67 (~P4(f8(a4,a4),a10,a10)),
% 75.59/75.67 inference(scs_inference,[],[9524,9338,8776,27,29])).
% 75.59/75.67 cnf(10020,plain,
% 75.59/75.67 (~P2(a4,f3(a1,a1),f6(a4))),
% 75.59/75.67 inference(scs_inference,[],[9524,9951,9156,8187,9338,8109,8666,8776,8089,27,29,30,32])).
% 75.59/75.67 cnf(10022,plain,
% 75.59/75.67 (~P2(f9(a5),f8(a5,a10),a10)),
% 75.59/75.67 inference(scs_inference,[],[9524,9951,10011,9156,8133,8187,9338,8755,8109,8666,8776,8089,27,29,30,32,31])).
% 75.59/75.67 cnf(10024,plain,
% 75.59/75.67 (~P2(f8(a4,a4),f3(a4,a4),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9524,9638,9951,10011,9156,8133,8187,9338,8231,8755,8109,8666,8776,8741,8362,8089,27,29,30,32,31,33])).
% 75.59/75.67 cnf(10030,plain,
% 75.59/75.67 (~P4(a7,f6(a7),f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[9722,8831,7976,29])).
% 75.59/75.67 cnf(10036,plain,
% 75.59/75.67 (~P2(f9(a4),a10,a7)),
% 75.59/75.67 inference(scs_inference,[],[11,9722,9872,9912,8831,7976,7916,8266,8984,8988,9356,29,30,32,31])).
% 75.59/75.67 cnf(10038,plain,
% 75.59/75.67 (~P4(f6(a1),a1,f9(a5))),
% 75.59/75.67 inference(scs_inference,[],[11,9722,9872,9912,9902,8831,7976,7916,8266,8984,8988,8718,9356,8447,3666,29,30,32,31,34])).
% 75.59/75.67 cnf(10052,plain,
% 75.59/75.67 (~P4(a4,a1,f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[10007,9962,8252,8814,8043,2749,29,30])).
% 75.59/75.67 cnf(10060,plain,
% 75.59/75.67 (~P4(a4,f8(a5,a10),f8(a5,a10))),
% 75.59/75.67 inference(scs_inference,[],[9747,9595,10014,10007,9962,9964,10003,8181,8252,7962,9354,8814,8043,8127,9352,7936,1389,2749,29,30,32,31,34,33])).
% 75.59/75.67 cnf(10062,plain,
% 75.59/75.67 (~P2(f9(a4),f3(a1,a1),f6(a5))),
% 75.59/75.67 inference(scs_inference,[],[9830,9747,9595,10014,10007,9962,9964,10003,8181,8252,7962,9354,8814,8043,8127,9352,7936,1389,2749,29,30,32,31,34,33,27])).
% 75.59/75.67 cnf(10068,plain,
% 75.59/75.67 (~P2(f8(a4,a4),f9(a5),a1)),
% 75.59/75.67 inference(scs_inference,[],[9949,9997,10016,8755,8131,8258,8909,8288,29,30,32])).
% 75.59/75.67 cnf(10070,plain,
% 75.59/75.67 (~P2(f8(a5,a10),f9(a5),a10)),
% 75.59/75.67 inference(scs_inference,[],[9949,9997,10016,10036,9745,10003,8755,8131,8258,8909,8288,29,30,32,31])).
% 75.59/75.67 cnf(10072,plain,
% 75.59/75.67 (~P4(f3(a4,a4),f8(a1,a1),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9949,10024,9997,10016,10036,9745,10003,8231,8755,8131,8258,8757,8909,8288,8362,29,30,32,31,34])).
% 75.59/75.67 cnf(10074,plain,
% 75.59/75.67 (~P2(a1,f8(a5,a10),a4)),
% 75.59/75.67 inference(scs_inference,[],[9949,10024,9997,10016,10060,10036,9745,10003,8231,8755,9120,8131,8258,8757,8909,8288,8362,29,30,32,31,34,33])).
% 75.59/75.67 cnf(10078,plain,
% 75.59/75.67 (~P4(a1,f9(a4),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[10030,9960,8183,9168,8831,2749,29,30])).
% 75.59/75.67 cnf(10084,plain,
% 75.59/75.67 (~P2(a1,a1,a5)),
% 75.59/75.67 inference(scs_inference,[],[9501,10074,9668,10030,9960,8210,8414,8183,9168,8831,8424,8674,8447,2749,29,30,32,31,33])).
% 75.59/75.67 cnf(10091,plain,
% 75.59/75.67 (~P4(f3(a4,a4),f6(a4),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9943,10052,8503,8984,8077,3677,29,30])).
% 75.59/75.67 cnf(10093,plain,
% 75.59/75.67 (P2(a4,f8(a5,a10),f8(a5,a7))),
% 75.59/75.67 inference(scs_inference,[],[9943,10052,10011,8503,3808,8984,7964,8077,3677,29,30,32])).
% 75.59/75.67 cnf(10101,plain,
% 75.59/75.67 (~P4(f6(a1),f6(a5),f3(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[10084,9536,10062,10072,9943,10052,10011,8195,8503,8939,8909,3808,8284,9027,8087,8984,8362,7964,9352,8077,3677,29,30,32,31,34,33,26])).
% 75.59/75.67 cnf(10103,plain,
% 75.59/75.67 (P2(f8(a5,a10),a4,f8(a5,a7))),
% 75.59/75.67 inference(scs_inference,[],[10084,9536,10062,10072,9943,10052,10011,8195,8503,8939,8909,3808,8284,9027,8087,8984,8362,7964,9352,8077,3677,29,30,32,31,34,33,26,27])).
% 75.59/75.67 cnf(10109,plain,
% 75.59/75.67 (~P4(f8(a1,a1),a4,f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[9751,9973,10091,8786,8887,8984,27,29,30])).
% 75.59/75.67 cnf(10111,plain,
% 75.59/75.67 (~P2(f9(a5),f8(a5,a7),a10)),
% 75.59/75.67 inference(scs_inference,[],[9751,9973,10022,10091,10093,8786,8258,8887,8984,27,29,30,32])).
% 75.59/75.67 cnf(10113,plain,
% 75.59/75.67 (P2(f8(a5,a10),f8(a4,a4),f8(a5,a7))),
% 75.59/75.67 inference(scs_inference,[],[9751,9973,10022,10103,10091,10093,8684,8786,8258,8887,8984,8751,27,29,30,32,31])).
% 75.59/75.67 cnf(10125,plain,
% 75.59/75.67 (~P2(f3(a1,a1),f3(a1,a1),a5)),
% 75.59/75.67 inference(scs_inference,[],[9999,9768,10113,10038,8623,8210,8585,8322,8814,8449,27,29,30,32])).
% 75.59/75.67 cnf(10131,plain,
% 75.59/75.67 (~P2(f6(a1),a2,a4)),
% 75.59/75.67 inference(scs_inference,[],[9999,9768,10070,9947,10113,10038,8955,10060,9706,8623,8210,8585,8755,8322,8292,9027,8814,8362,8449,27,29,30,32,31,34,33])).
% 75.59/75.67 cnf(10139,plain,
% 75.59/75.67 (P2(f8(a5,a7),f9(a4),f8(a5,a10))),
% 75.59/75.67 inference(scs_inference,[],[9892,10078,10103,9778,9734,9154,9120,9122,8503,8235,27,29,30,32])).
% 75.59/75.67 cnf(10141,plain,
% 75.59/75.67 (~P2(f8(a4,a4),f3(a1,a1),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9892,9945,10078,10103,9778,9734,9154,9120,9122,8503,8307,8235,8248,27,29,30,32,31])).
% 75.59/75.67 cnf(10147,plain,
% 75.59/75.67 (P2(f9(a4),f8(a5,a7),f8(a5,a10))),
% 75.59/75.67 inference(scs_inference,[],[10139,27])).
% 75.59/75.67 cnf(10149,plain,
% 75.59/75.67 (~P4(a4,f6(a7),f6(a7))),
% 75.59/75.67 inference(scs_inference,[],[10139,9107,8002,27,29])).
% 75.59/75.67 cnf(10171,plain,
% 75.59/75.67 (~P2(f8(a1,a1),a4,a5)),
% 75.59/75.67 inference(scs_inference,[],[8968,10131,9920,10125,10149,8927,8233,8585,8666,8266,8988,8674,27,29,30,32,31])).
% 75.59/75.67 cnf(10181,plain,
% 75.59/75.67 (P2(f8(a5,a7),f9(a5),a7)),
% 75.59/75.67 inference(scs_inference,[],[9583,9597,10103,10003,9126,8181,8848,8077,3660,29,30,32])).
% 75.59/75.67 cnf(10189,plain,
% 75.59/75.67 (P2(f9(a5),f8(a5,a7),a7)),
% 75.59/75.67 inference(scs_inference,[],[10141,10147,9583,10020,9597,10103,10060,10003,9126,8181,9142,8503,8307,8516,8848,8400,8077,1389,3660,29,30,32,31,34,33,27])).
% 75.59/75.67 cnf(10191,plain,
% 75.59/75.67 (~P2(f3(a1,a1),f9(a4),f9(a4))),
% 75.59/75.67 inference(scs_inference,[],[9977,27])).
% 75.59/75.67 cnf(10197,plain,
% 75.59/75.67 (~P2(a2,a7,f8(a1,a1))),
% 75.59/75.67 inference(scs_inference,[],[9977,10009,9882,9174,8402,8668,8887,7974,7,27,29,30,32])).
% 75.59/75.67 cnf(10208,plain,
% 75.59/75.67 (~P4(f3(a1,a1),f6(a5),a1)),
% 75.59/75.67 inference(scs_inference,[],[8806,7940,8117,29])).
% 75.59/75.67 cnf(10218,plain,
% 75.59/75.67 (~P2(a4,f8(a4,a4),f6(a1))),
% 75.59/75.67 inference(scs_inference,[],[10111,10109,8806,10191,9854,10171,10189,9894,9120,7940,9122,8292,9039,8117,8718,8428,8674,8422,8449,29,30,32,31,34,33])).
% 75.59/75.67 cnf(10230,plain,
% 75.59/75.67 (P2(a7,f9(a4),a7)),
% 75.59/75.67 inference(scs_inference,[],[9297,10068,10208,10139,10189,10011,8210,8113,8424,8782,8077,3660,31,29,30,32])).
% 75.59/75.67 cnf(10240,plain,
% 75.59/75.67 (~P2(a1,x102401,a7)+~P2(a2,x102401,a4)),
% 75.59/75.67 inference(scs_inference,[],[8262,27])).
% 75.59/75.67 cnf(10261,plain,
% 75.59/75.67 (~P2(f8(a4,a4),f6(a1),a4)),
% 75.59/75.67 inference(scs_inference,[],[9204,10197,10101,10218,8589,10181,8210,8170,8368,7974,8848,8573,31,29,30,32])).
% 75.59/75.67 cnf(10269,plain,
% 75.59/75.67 (P1(f9(a2))),
% 75.59/75.67 inference(scs_inference,[],[9204,10197,10101,10218,8589,10181,8210,8170,8368,7974,8848,8573,3,31,29,30,32,2771,6881,24,20])).
% 75.59/75.67 cnf(10271,plain,
% 75.59/75.67 (~P4(a2,a5,a2)),
% 75.59/75.67 inference(scs_inference,[],[9204,10197,10101,10218,8589,10181,8210,8170,7916,8368,7974,8848,8573,3,31,29,30,32,2771,6881,24,20,3399])).
% 75.59/75.67 cnf(10275,plain,
% 75.59/75.67 (~P2(a5,f9(a2),a10)),
% 75.59/75.67 inference(scs_inference,[],[9204,9876,10197,10101,10218,10230,8589,10181,8210,8170,7916,8368,7974,8848,8573,3,31,29,30,32,2771,6881,24,20,3399,34,3351])).
% 75.59/75.67 cnf(10276,plain,
% 75.59/75.67 (P2(a2,f9(a2),a4)),
% 75.59/75.67 inference(scs_inference,[],[9204,9876,10197,10101,10218,10230,8589,10181,8210,8170,7916,8368,7974,8848,8573,3,31,29,30,32,2771,6881,24,20,3399,34,3351,27])).
% 75.59/75.67 cnf(10278,plain,
% 75.59/75.67 (P4(a1,f9(a2),f9(a2))),
% 75.59/75.67 inference(scs_inference,[],[9204,9876,10197,10101,10218,10230,8589,10181,8210,8170,7916,8368,7974,8848,8573,3,31,29,30,32,2771,6881,24,20,3399,34,3351,27,17])).
% 75.59/75.67 cnf(10289,plain,
% 75.59/75.67 (P2(a4,f9(a2),f9(a2))),
% 75.59/75.67 inference(scs_inference,[],[9628,10269,10278,10276,10240,27,26,18])).
% 75.59/75.67 cnf(10317,plain,
% 75.59/75.67 ($false),
% 75.59/75.67 inference(scs_inference,[],[10271,9448,10275,10261,10289,10276,10278,8774,8434,7922,3760,8077,3660,26,27,31,29,30,32]),
% 75.59/75.67 ['proof']).
% 75.59/75.67 % SZS output end Proof
% 75.59/75.67 % Total time :74.980000s
%------------------------------------------------------------------------------