%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD009-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n022.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:09 EDT 2024
% Result : Unsatisfiable 116.77s 116.81s
% Output : CNFRefutation 116.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : FLD009-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.35 % Computer : n022.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Jun 19 11:18:09 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.53/0.59 start to proof:theBenchmark
% 116.77/116.80 %-------------------------------------------
% 116.77/116.80 % File :CSE---1.7
% 116.77/116.80 % Problem :theBenchmark
% 116.77/116.80 % Transform :cnf
% 116.77/116.80 % Format :tptp:raw
% 116.77/116.80 % Command :java -jar mcs_scs.jar %d %s
% 116.77/116.80
% 116.77/116.80 % Result :Theorem 116.160000s
% 116.77/116.80 % Output :CNFRefutation 116.160000s
% 116.77/116.80 %-------------------------------------------
% 116.77/116.81 %--------------------------------------------------------------------------
% 116.77/116.81 % File : FLD009-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 116.77/116.81 % Domain : Field Theory (Ordered fields)
% 116.77/116.81 % Problem : Linear equations in the multiplicative group have a solution
% 116.77/116.81 % Version : [Dra93] axioms : Especial.
% 116.77/116.81 % Theorem formulation : Functional with re axiom set.
% 116.77/116.81 % English :
% 116.77/116.81
% 116.77/116.81 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 116.77/116.81 % Source : [Dra93]
% 116.77/116.81 % Names :
% 116.77/116.81
% 116.77/116.81 % Status : Unsatisfiable
% 116.77/116.81 % Rating : 0.17 v8.2.0, 0.29 v8.1.0, 0.14 v7.5.0, 0.33 v7.4.0, 0.17 v7.1.0, 0.50 v6.3.0, 0.29 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.38 v5.4.0, 0.30 v5.2.0, 0.10 v5.1.0, 0.18 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.00 v2.6.0, 0.33 v2.5.0, 0.00 v2.4.0, 0.20 v2.3.0, 0.33 v2.2.1, 0.33 v2.1.0
% 116.77/116.81 % Syntax : Number of clauses : 30 ( 7 unt; 3 nHn; 30 RR)
% 116.77/116.81 % Number of literals : 81 ( 0 equ; 51 neg)
% 116.77/116.81 % Maximal clause size : 5 ( 2 avg)
% 116.77/116.81 % Maximal term depth : 2 ( 1 avg)
% 116.77/116.81 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 116.77/116.81 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 116.77/116.81 % Number of variables : 74 ( 1 sgn)
% 116.77/116.81 % SPC : CNF_UNS_RFO_NEQ_NHN
% 116.77/116.81
% 116.77/116.81 % Comments :
% 116.77/116.81 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 116.77/116.81 %--------------------------------------------------------------------------
% 116.77/116.81 include('Axioms/FLD002-0.ax').
% 116.77/116.81 %--------------------------------------------------------------------------
% 116.77/116.81 cnf(a_is_defined,hypothesis,
% 116.77/116.81 defined(a) ).
% 116.77/116.81
% 116.77/116.81 cnf(b_is_defined,hypothesis,
% 116.77/116.81 defined(b) ).
% 116.77/116.81
% 116.77/116.81 cnf(not_sum_3,negated_conjecture,
% 116.77/116.81 ~ sum(additive_identity,a,additive_identity) ).
% 116.77/116.81
% 116.77/116.81 cnf(not_product_4,negated_conjecture,
% 116.77/116.81 ~ product(a,X,b) ).
% 116.77/116.81
% 116.77/116.81 %--------------------------------------------------------------------------
% 116.77/116.81 %-------------------------------------------
% 116.77/116.81 % Proof found
% 116.77/116.81 % SZS status Theorem for theBenchmark
% 116.77/116.81 % SZS output start Proof
% 116.80/116.82 %ClaNum:30(EqnAxiom:0)
% 116.80/116.82 %VarNum:163(SingletonVarNum:74)
% 116.80/116.82 %MaxLitNum:5
% 116.80/116.82 %MaxfuncDepth:1
% 116.80/116.82 %SharedTerms:10
% 116.80/116.82 %goalClause: 6 7
% 116.80/116.82 %singleGoalClaCount:2
% 116.80/116.82 [1]P1(a1)
% 116.80/116.82 [2]P1(a4)
% 116.80/116.82 [3]P1(a2)
% 116.80/116.82 [4]P1(a5)
% 116.80/116.82 [5]~P2(a1,a1,a4)
% 116.80/116.82 [6]~P2(a1,a2,a1)
% 116.80/116.82 [7]~P3(a2,x71,a5)
% 116.80/116.82 [13]~P1(x131)+P2(a1,x131,x131)
% 116.80/116.82 [14]~P1(x141)+P3(a4,x141,x141)
% 116.80/116.82 [8]~P1(x81)+P1(f6(x81))
% 116.80/116.82 [15]~P1(x151)+P2(f6(x151),x151,a1)
% 116.80/116.82 [22]~P2(x222,x221,x223)+P2(x221,x222,x223)
% 116.80/116.82 [23]~P3(x232,x231,x233)+P3(x231,x232,x233)
% 116.80/116.82 [16]~P1(x161)+P2(a1,x161,a1)+P1(f8(x161))
% 116.80/116.82 [20]~P1(x201)+P3(f8(x201),x201,a4)+P2(a1,x201,a1)
% 116.80/116.82 [19]~P4(x192,x191)+~P4(x191,x192)+P2(a1,x191,x192)
% 116.80/116.82 [10]~P1(x102)+~P1(x101)+P1(f3(x101,x102))
% 116.80/116.82 [11]~P1(x112)+~P1(x111)+P1(f7(x111,x112))
% 116.80/116.82 [17]~P1(x172)+~P1(x171)+P2(x171,x172,f3(x171,x172))
% 116.80/116.82 [18]~P1(x182)+~P1(x181)+P3(x181,x182,f7(x181,x182))
% 116.80/116.82 [12]~P4(x121,x123)+P4(x121,x122)+~P4(x123,x122)
% 116.80/116.82 [9]P4(x92,x91)+~P1(x91)+~P1(x92)+P4(x91,x92)
% 116.80/116.82 [21]~P3(x213,x212,x211)+P4(a1,x211)+~P4(a1,x212)+~P4(a1,x213)
% 116.80/116.82 [24]~P2(x243,x245,x241)+P4(x241,x242)+~P2(x244,x245,x242)+~P4(x243,x244)
% 116.80/116.82 [25]~P2(x251,x256,x254)+P2(x251,x252,x253)+~P2(x254,x255,x253)+~P2(x256,x255,x252)
% 116.80/116.82 [26]~P2(x266,x264,x261)+P2(x261,x262,x263)+~P2(x264,x262,x265)+~P2(x266,x265,x263)
% 116.80/116.82 [27]~P3(x271,x276,x274)+P3(x271,x272,x273)+~P3(x274,x275,x273)+~P3(x276,x275,x272)
% 116.80/116.82 [28]~P3(x286,x284,x281)+P3(x281,x282,x283)+~P3(x284,x282,x285)+~P3(x286,x285,x283)
% 116.80/116.82 [29]~P3(x295,x297,x292)+~P3(x294,x297,x291)+P2(x291,x292,x293)+~P2(x294,x295,x296)+~P3(x296,x297,x293)
% 116.80/116.82 [30]~P3(x307,x302,x305)+~P3(x306,x302,x304)+P3(x301,x302,x303)+~P2(x304,x305,x303)+~P2(x306,x307,x301)
% 116.80/116.82 %EqnAxiom
% 116.80/116.82
% 116.80/116.82 %-------------------------------------------
% 116.80/116.83 cnf(31,plain,
% 116.80/116.83 (~P2(a2,a1,a1)),
% 116.80/116.83 inference(scs_inference,[],[6,22])).
% 116.80/116.83 cnf(33,plain,
% 116.80/116.83 (~P3(x331,a2,a5)),
% 116.80/116.83 inference(scs_inference,[],[6,7,22,23])).
% 116.80/116.83 cnf(35,plain,
% 116.80/116.83 (P4(a1,a1)),
% 116.80/116.83 inference(scs_inference,[],[6,7,1,22,23,9])).
% 116.80/116.83 cnf(40,plain,
% 116.80/116.83 (P4(a4,a4)),
% 116.80/116.83 inference(scs_inference,[],[2,9])).
% 116.80/116.83 cnf(46,plain,
% 116.80/116.83 (~P4(a4,a1)+~P2(a1,x461,a1)+~P2(a1,x461,a4)),
% 116.80/116.83 inference(scs_inference,[],[6,2,5,35,9,19,21,24])).
% 116.80/116.83 cnf(47,plain,
% 116.80/116.83 (P4(a2,a2)),
% 116.80/116.83 inference(scs_inference,[],[3,9])).
% 116.80/116.84 cnf(49,plain,
% 116.80/116.84 (~P2(a4,x491,x492)+~P2(a4,x491,x493)+P4(x492,x493)),
% 116.80/116.84 inference(scs_inference,[],[3,40,9,24])).
% 116.80/116.84 cnf(50,plain,
% 116.80/116.84 (P4(a5,a5)),
% 116.80/116.84 inference(scs_inference,[],[4,9])).
% 116.80/116.84 cnf(52,plain,
% 116.80/116.84 (~P2(a2,x521,x522)+~P2(a2,x521,x523)+P4(x522,x523)),
% 116.80/116.84 inference(scs_inference,[],[4,47,9,24])).
% 116.80/116.84 cnf(60,plain,
% 116.80/116.84 (~P2(a1,x601,x602)+~P2(a1,x601,x603)+P4(x602,x603)),
% 116.80/116.84 inference(scs_inference,[],[35,24])).
% 116.80/116.84 cnf(65,plain,
% 116.80/116.84 (P1(f6(f3(a1,a1)))),
% 116.80/116.84 inference(scs_inference,[],[1,8,10])).
% 116.80/116.84 cnf(97,plain,
% 116.80/116.84 (P3(a4,f6(f6(f3(a1,a1))),f6(f6(f3(a1,a1))))),
% 116.80/116.84 inference(scs_inference,[],[65,14,8])).
% 116.80/116.84 cnf(145,plain,
% 116.80/116.84 (P2(f6(f6(a4)),f6(a4),a1)),
% 116.80/116.84 inference(scs_inference,[],[2,15,8])).
% 116.80/116.84 cnf(146,plain,
% 116.80/116.84 (~P2(f6(a4),a2,f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[6,145,26])).
% 116.80/116.84 cnf(148,plain,
% 116.80/116.84 (~P2(a2,f6(a4),f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[6,145,26,22])).
% 116.80/116.84 cnf(181,plain,
% 116.80/116.84 (P1(f7(f6(a2),f6(a2)))),
% 116.80/116.84 inference(scs_inference,[],[3,11,8])).
% 116.80/116.84 cnf(259,plain,
% 116.80/116.84 (P2(f6(a4),f6(a4),f3(f6(a4),f6(a4)))),
% 116.80/116.84 inference(scs_inference,[],[2,17,8])).
% 116.80/116.84 cnf(275,plain,
% 116.80/116.84 (P3(f6(a2),f6(a2),f7(f6(a2),f6(a2)))),
% 116.80/116.84 inference(scs_inference,[],[3,18,8])).
% 116.80/116.84 cnf(355,plain,
% 116.80/116.84 (~P4(a4,a1)+~P2(a1,a4,a1)),
% 116.80/116.84 inference(scs_inference,[],[2,46,13])).
% 116.80/116.84 cnf(371,plain,
% 116.80/116.84 (~P2(a4,x3711,a4)+~P2(a4,x3711,a1)+~P2(a1,a4,a1)),
% 116.80/116.84 inference(scs_inference,[],[355,49])).
% 116.80/116.84 cnf(481,plain,
% 116.80/116.84 (~P2(x4811,a4,a1)+~P2(a4,x4811,a4)+~P2(a1,a4,a1)),
% 116.80/116.84 inference(scs_inference,[],[371,22])).
% 116.80/116.84 cnf(512,plain,
% 116.80/116.84 (~P2(x5121,a4,a4)+~P2(x5121,a4,a1)+~P2(a1,a4,a1)),
% 116.80/116.84 inference(scs_inference,[],[481,22])).
% 116.80/116.84 cnf(528,plain,
% 116.80/116.84 (~P2(a1,a4,a1)),
% 116.80/116.84 inference(scs_inference,[],[40,512,19])).
% 116.80/116.84 cnf(529,plain,
% 116.80/116.84 (~P2(a4,a1,a1)),
% 116.80/116.84 inference(scs_inference,[],[528,22])).
% 116.80/116.84 cnf(718,plain,
% 116.80/116.84 (P2(a1,f6(a5),f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[4,8,13])).
% 116.80/116.84 cnf(997,plain,
% 116.80/116.84 (P2(a1,f6(a1),f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[1,8,13])).
% 116.80/116.84 cnf(1003,plain,
% 116.80/116.84 (~P2(x10031,a1,a1)+P2(x10031,f6(a1),f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[997,25])).
% 116.80/116.84 cnf(1019,plain,
% 116.80/116.84 (P2(f6(a1),x10191,f6(a1))+~P2(x10191,a1,a1)),
% 116.80/116.84 inference(scs_inference,[],[1003,22])).
% 116.80/116.84 cnf(1035,plain,
% 116.80/116.84 (~P2(f6(a1),f6(f6(a4)),x10351)+P2(x10351,f6(a4),f6(a1))+~P2(a1,a1,a1)),
% 116.80/116.84 inference(scs_inference,[],[145,1019,26])).
% 116.80/116.84 cnf(1066,plain,
% 116.80/116.84 (~P2(f6(a1),f6(f6(a4)),x10661)+P2(x10661,f6(a4),f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[1,1035,13])).
% 116.80/116.84 cnf(1082,plain,
% 116.80/116.84 (~P2(f6(f6(a4)),f6(a1),x10821)+P2(x10821,f6(a4),f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[1066,22])).
% 116.80/116.84 cnf(1134,plain,
% 116.80/116.84 (~P2(a1,a1,x11341)+P2(x11341,f6(a1),f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[997,26])).
% 116.80/116.84 cnf(1547,plain,
% 116.80/116.84 (P2(a1,f6(a2),f6(a2))),
% 116.80/116.84 inference(scs_inference,[],[3,8,13])).
% 116.80/116.84 cnf(1550,plain,
% 116.80/116.84 (~P2(a1,a1,x15501)+P2(x15501,f6(a2),f6(a2))),
% 116.80/116.84 inference(scs_inference,[],[1547,60,26])).
% 116.80/116.84 cnf(1555,plain,
% 116.80/116.84 (~P2(x15551,a1,a1)+P2(x15551,f6(a2),f6(a2))),
% 116.80/116.84 inference(scs_inference,[],[1547,25])).
% 116.80/116.84 cnf(1571,plain,
% 116.80/116.84 (P2(f6(a2),x15711,f6(a2))+~P2(a1,a1,x15711)),
% 116.80/116.84 inference(scs_inference,[],[1550,22])).
% 116.80/116.84 cnf(1759,plain,
% 116.80/116.84 (P3(a4,f6(a5),f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[4,8,14])).
% 116.80/116.84 cnf(1924,plain,
% 116.80/116.84 (P2(f6(f6(a5)),f6(a5),a1)),
% 116.80/116.84 inference(scs_inference,[],[4,8,15])).
% 116.80/116.84 cnf(1925,plain,
% 116.80/116.84 (~P2(f6(a5),a2,f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[6,1924,26])).
% 116.80/116.84 cnf(1927,plain,
% 116.80/116.84 (~P2(a2,f6(a5),f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[6,1924,26,22])).
% 116.80/116.84 cnf(1930,plain,
% 116.80/116.84 (~P2(a1,a1,a2)),
% 116.80/116.84 inference(scs_inference,[],[1927,718,26])).
% 116.80/116.84 cnf(1962,plain,
% 116.80/116.84 (P3(a4,f6(a1),f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[1,8,14])).
% 116.80/116.84 cnf(2009,plain,
% 116.80/116.84 (~P1(f6(a2))+~P3(f7(a2,f6(a2)),f6(a2),a5)),
% 116.80/116.84 inference(scs_inference,[],[7,275,3,27,23,18])).
% 116.80/116.84 cnf(2474,plain,
% 116.80/116.84 (~P2(f6(a4),a4,f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[528,145,26])).
% 116.80/116.84 cnf(2476,plain,
% 116.80/116.84 (~P2(a4,f6(a4),f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[528,145,26,22])).
% 116.80/116.84 cnf(2479,plain,
% 116.80/116.84 (~P2(f6(a5),a4,f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[528,1924,26])).
% 116.80/116.84 cnf(2481,plain,
% 116.80/116.84 (~P2(a4,f6(a5),f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[528,1924,26,22])).
% 116.80/116.84 cnf(2524,plain,
% 116.80/116.84 (~P3(f7(a2,f6(a2)),f6(a2),a5)),
% 116.80/116.84 inference(scs_inference,[],[3,8,2009])).
% 116.80/116.84 cnf(2525,plain,
% 116.80/116.84 (~P3(f6(a2),f7(a2,f6(a2)),a5)),
% 116.80/116.84 inference(scs_inference,[],[2524,23])).
% 116.80/116.84 cnf(2558,plain,
% 116.80/116.84 (P2(f6(f6(a1)),f6(a1),a1)),
% 116.80/116.84 inference(scs_inference,[],[1,8,15])).
% 116.80/116.84 cnf(2559,plain,
% 116.80/116.84 (~P2(f6(a1),a4,f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[528,2558,26])).
% 116.80/116.84 cnf(2561,plain,
% 116.80/116.84 (~P2(a4,f6(a1),f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[528,2558,26,22])).
% 116.80/116.84 cnf(2593,plain,
% 116.80/116.84 (P2(a1,f6(a4),f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[2,8,13])).
% 116.80/116.84 cnf(2609,plain,
% 116.80/116.84 (~P2(f6(f6(a4)),x26091,a4)+~P2(x26091,a1,f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[529,145,26])).
% 116.80/116.84 cnf(2613,plain,
% 116.80/116.84 (~P2(f6(f6(a5)),x26131,a4)+~P2(x26131,a1,f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[529,1924,26])).
% 116.80/116.84 cnf(2617,plain,
% 116.80/116.84 (~P2(f6(f6(a1)),x26171,a4)+~P2(x26171,a1,f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[529,2558,26])).
% 116.80/116.84 cnf(2638,plain,
% 116.80/116.84 (~P2(x26381,f6(f6(a5)),a4)+~P2(x26381,a1,f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[2613,22])).
% 116.80/116.84 cnf(2654,plain,
% 116.80/116.84 (~P2(x26541,f6(f6(a1)),a4)+~P2(x26541,a1,f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[2617,22])).
% 116.80/116.84 cnf(2740,plain,
% 116.80/116.84 (~P2(a2,f6(a1),f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[6,2558,26,22])).
% 116.80/116.84 cnf(2846,plain,
% 116.80/116.84 (P3(a4,f6(a4),f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[2,8,14])).
% 116.80/116.84 cnf(2849,plain,
% 116.80/116.84 (~P3(a1,x28491,a2)+~P3(f6(a4),x28491,f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[148,2593,2846,28,29])).
% 116.80/116.84 cnf(2861,plain,
% 116.80/116.84 (P2(f6(a4),f6(a4),f6(a4))+~P2(a4,a4,a4)),
% 116.80/116.84 inference(scs_inference,[],[2846,29])).
% 116.80/116.84 cnf(2912,plain,
% 116.80/116.84 (~P3(a1,a4,a2)),
% 116.80/116.84 inference(scs_inference,[],[2846,2849,23])).
% 116.80/116.84 cnf(2913,plain,
% 116.80/116.84 (~P3(a4,a1,a2)),
% 116.80/116.84 inference(scs_inference,[],[2912,23])).
% 116.80/116.84 cnf(2947,plain,
% 116.80/116.84 (~P2(f6(f6(a4)),a1,x29471)+P2(x29471,f6(a4),a1)),
% 116.80/116.84 inference(scs_inference,[],[145,2593,26])).
% 116.80/116.84 cnf(2963,plain,
% 116.80/116.84 (~P2(f6(f6(a1)),a1,x29631)+P2(x29631,f6(a1),a1)),
% 116.80/116.84 inference(scs_inference,[],[2558,997,26])).
% 116.80/116.84 cnf(2998,plain,
% 116.80/116.84 (~P2(a1,f6(f6(a4)),x29981)+P2(x29981,f6(a4),a1)),
% 116.80/116.84 inference(scs_inference,[],[2947,22])).
% 116.80/116.84 cnf(3030,plain,
% 116.80/116.84 (~P2(a1,f6(f6(a1)),x30301)+P2(x30301,f6(a1),a1)),
% 116.80/116.84 inference(scs_inference,[],[2963,22])).
% 116.80/116.84 cnf(3371,plain,
% 116.80/116.84 (~P2(x33711,f6(a4),a4)+~P2(a1,x33711,f6(f6(a4)))),
% 116.80/116.84 inference(scs_inference,[],[528,145,25])).
% 116.80/116.84 cnf(3373,plain,
% 116.80/116.84 (~P2(x33731,f6(a4),a4)+~P2(x33731,a1,f6(f6(a4)))),
% 116.80/116.84 inference(scs_inference,[],[528,145,25,22])).
% 116.80/116.84 cnf(3377,plain,
% 116.80/116.84 (~P2(f6(a2),x33771,a1)+~P2(f6(a2),x33771,a2)),
% 116.80/116.84 inference(scs_inference,[],[1547,1930,25])).
% 116.80/116.84 cnf(3379,plain,
% 116.80/116.84 (~P2(f6(a2),x33791,a1)+~P2(x33791,f6(a2),a2)),
% 116.80/116.84 inference(scs_inference,[],[1547,1930,25,22])).
% 116.80/116.84 cnf(3383,plain,
% 116.80/116.84 (~P2(f6(a2),x33831,a1)+~P2(f6(a2),x33831,a4)),
% 116.80/116.84 inference(scs_inference,[],[1547,5,25])).
% 116.80/116.84 cnf(3385,plain,
% 116.80/116.84 (~P2(f6(a2),x33851,a1)+~P2(x33851,f6(a2),a4)),
% 116.80/116.84 inference(scs_inference,[],[1547,5,25,22])).
% 116.80/116.84 cnf(3389,plain,
% 116.80/116.84 (~P2(x33891,f6(a4),a2)+~P2(f6(a4),x33891,a1)),
% 116.80/116.84 inference(scs_inference,[],[146,2593,25])).
% 116.80/116.84 cnf(3397,plain,
% 116.80/116.84 (~P2(x33971,f6(a5),a2)+~P2(f6(a5),x33971,a1)),
% 116.80/116.84 inference(scs_inference,[],[718,1925,25])).
% 116.80/116.84 cnf(3407,plain,
% 116.80/116.84 (~P2(x34071,f6(a4),a4)+~P2(f6(a4),x34071,a1)),
% 116.80/116.84 inference(scs_inference,[],[2593,2474,25])).
% 116.80/116.84 cnf(3417,plain,
% 116.80/116.84 (~P2(x34171,f6(a5),a4)+~P2(f6(a5),x34171,a1)),
% 116.80/116.84 inference(scs_inference,[],[718,2479,25])).
% 116.80/116.84 cnf(3427,plain,
% 116.80/116.84 (~P2(x34271,f6(a1),a4)+~P2(f6(a1),x34271,a1)),
% 116.80/116.84 inference(scs_inference,[],[997,2559,25])).
% 116.80/116.84 cnf(3518,plain,
% 116.80/116.84 (~P2(a4,f6(a4),a2)),
% 116.80/116.84 inference(scs_inference,[],[2,3389,15])).
% 116.80/116.84 cnf(3519,plain,
% 116.80/116.84 (~P2(f6(a4),a4,a2)),
% 116.80/116.84 inference(scs_inference,[],[3518,22])).
% 116.80/116.84 cnf(3525,plain,
% 116.80/116.84 (~P2(f6(a4),x35251,a4)+~P2(f3(f6(a4),f6(a4)),x35251,a2)),
% 116.80/116.84 inference(scs_inference,[],[3519,259,25])).
% 116.80/116.84 cnf(3527,plain,
% 116.80/116.84 (~P2(f6(a4),x35271,a4)+~P2(x35271,f3(f6(a4),f6(a4)),a2)),
% 116.80/116.84 inference(scs_inference,[],[3519,259,25,22])).
% 116.80/116.84 cnf(3576,plain,
% 116.80/116.84 (~P2(a5,f6(a5),a2)),
% 116.80/116.84 inference(scs_inference,[],[4,3397,15])).
% 116.80/116.84 cnf(3577,plain,
% 116.80/116.84 (~P2(f6(a5),a5,a2)),
% 116.80/116.84 inference(scs_inference,[],[3576,22])).
% 116.80/116.84 cnf(3594,plain,
% 116.80/116.84 (~P3(x35941,f6(a4),a5)+~P3(x35941,a4,a2)),
% 116.80/116.84 inference(scs_inference,[],[7,2846,28])).
% 116.80/116.84 cnf(3606,plain,
% 116.80/116.84 (~P3(a4,f7(f6(a4),a2),a5)+~P1(f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[2846,3,33,28,23,18])).
% 116.80/116.84 cnf(3621,plain,
% 116.80/116.84 (~P2(x36211,x36212,a5)+~P2(f6(a5),x36211,x36213)+~P2(x36213,x36212,a2)),
% 116.80/116.84 inference(scs_inference,[],[3577,2525,47,25])).
% 116.80/116.84 cnf(3632,plain,
% 116.80/116.84 (~P3(x36321,a4,x36322)+~P3(x36322,f6(a4),a5)+~P3(x36321,a4,a2)),
% 116.80/116.84 inference(scs_inference,[],[2846,3594,27])).
% 116.80/116.84 cnf(3725,plain,
% 116.80/116.84 (~P2(a4,f6(a4),a4)),
% 116.80/116.84 inference(scs_inference,[],[2,3407,15])).
% 116.80/116.84 cnf(3726,plain,
% 116.80/116.84 (~P2(f6(a4),a4,a4)),
% 116.80/116.84 inference(scs_inference,[],[3725,22])).
% 116.80/116.84 cnf(3728,plain,
% 116.80/116.84 (~P2(a4,a1,x37281)+~P2(x37281,f6(a4),a4)),
% 116.80/116.84 inference(scs_inference,[],[2593,3725,22,25])).
% 116.80/116.84 cnf(3733,plain,
% 116.80/116.84 (~P2(f6(a4),x37331,a4)+~P2(f3(f6(a4),f6(a4)),x37331,a4)),
% 116.80/116.84 inference(scs_inference,[],[3726,259,25])).
% 116.80/116.84 cnf(3735,plain,
% 116.80/116.84 (~P2(x37351,f6(a4),a4)+~P2(f3(f6(a4),f6(a4)),x37351,a4)),
% 116.80/116.84 inference(scs_inference,[],[3726,259,25,22])).
% 116.80/116.84 cnf(3758,plain,
% 116.80/116.84 (~P3(x37581,f6(a5),a5)+~P3(x37581,a4,a2)),
% 116.80/116.84 inference(scs_inference,[],[7,1759,28])).
% 116.80/116.84 cnf(3768,plain,
% 116.80/116.84 (~P3(a4,x37681,a5)+~P3(a2,f6(a5),x37681)),
% 116.80/116.84 inference(scs_inference,[],[1759,33,28,23])).
% 116.80/116.84 cnf(3782,plain,
% 116.80/116.84 (~P2(f6(a4),x37821,a4)+~P2(a4,a1,x37821)),
% 116.80/116.84 inference(scs_inference,[],[3728,22])).
% 116.80/116.84 cnf(3798,plain,
% 116.80/116.84 (~P3(f6(a5),x37981,f6(a5))+~P3(f6(a5),x37981,a5)+~P3(a4,a4,a2)),
% 116.80/116.84 inference(scs_inference,[],[1759,3758,27])).
% 116.80/116.84 cnf(3804,plain,
% 116.80/116.84 (P3(f6(a5),a4,f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[1759,23])).
% 116.80/116.84 cnf(3810,plain,
% 116.80/116.84 (P3(f6(a4),a4,f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[2846,23])).
% 116.80/116.84 cnf(3816,plain,
% 116.80/116.84 (P3(f6(a1),a4,f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[1962,23])).
% 116.80/116.84 cnf(3818,plain,
% 116.80/116.84 (~P3(a1,a4,a4)),
% 116.80/116.84 inference(scs_inference,[],[2561,997,1962,23,29])).
% 116.80/116.84 cnf(3871,plain,
% 116.80/116.84 (~P1(f6(a5))+~P3(a4,f7(a2,f6(a5)),a5)),
% 116.80/116.84 inference(scs_inference,[],[3,3768,18])).
% 116.80/116.84 cnf(3903,plain,
% 116.80/116.84 (~P2(a5,f6(a5),a4)),
% 116.80/116.84 inference(scs_inference,[],[4,3417,15])).
% 116.80/116.84 cnf(3904,plain,
% 116.80/116.84 (~P2(f6(a5),a5,a4)),
% 116.80/116.84 inference(scs_inference,[],[3903,22])).
% 116.80/116.84 cnf(3965,plain,
% 116.80/116.84 (~P2(a1,f6(a1),a4)),
% 116.80/116.84 inference(scs_inference,[],[1,3427,15])).
% 116.80/116.84 cnf(3966,plain,
% 116.80/116.84 (~P2(f6(a1),a1,a4)),
% 116.80/116.84 inference(scs_inference,[],[3965,22])).
% 116.80/116.84 cnf(3974,plain,
% 116.80/116.84 (~P2(f6(a4),x39741,a4)+~P2(f6(a1),f6(f6(a4)),x39741)),
% 116.80/116.84 inference(scs_inference,[],[3966,145,25,22])).
% 116.80/116.84 cnf(4036,plain,
% 116.80/116.84 (~P3(f7(f6(a4),a2),a4,a5)+~P1(f6(a4))),
% 116.80/116.84 inference(scs_inference,[],[3606,23])).
% 116.80/116.84 cnf(4125,plain,
% 116.80/116.84 (~P3(x41251,x41252,a4)+~P3(a1,x41251,x41253)+~P3(x41253,x41252,a2)),
% 116.80/116.84 inference(scs_inference,[],[3577,2912,40,27])).
% 116.80/116.84 cnf(4390,plain,
% 116.80/116.84 (~P2(f6(f6(a5)),x43901,a2)+~P2(x43901,a1,f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[1924,31,26])).
% 116.80/116.84 cnf(4395,plain,
% 116.80/116.84 (~P2(f6(f6(a1)),x43951,a2)+~P2(x43951,a1,f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[31,2558,26])).
% 116.80/116.84 cnf(4397,plain,
% 116.80/116.84 (~P2(x43971,f6(f6(a1)),a2)+~P2(x43971,a1,f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[31,2558,26,22])).
% 116.80/116.84 cnf(4469,plain,
% 116.80/116.84 (~P3(a4,f7(a2,f6(a5)),a5)),
% 116.80/116.84 inference(scs_inference,[],[4,3871,8])).
% 116.80/116.84 cnf(4505,plain,
% 116.80/116.84 (~P3(f7(f6(a4),a2),a4,a5)),
% 116.80/116.84 inference(scs_inference,[],[2,4036,8])).
% 116.80/116.84 cnf(4538,plain,
% 116.80/116.84 (~P2(f6(a1),x45381,a2)+~P2(a1,x45381,f6(f6(a1)))),
% 116.80/116.84 inference(scs_inference,[],[6,2558,25,22])).
% 116.80/116.84 cnf(4543,plain,
% 116.80/116.84 (~P2(f6(a1),f6(f6(a1)),x45431)+~P2(x45431,f6(a1),a4)),
% 116.80/116.84 inference(scs_inference,[],[3966,2558,25])).
% 116.80/116.84 cnf(4545,plain,
% 116.80/116.84 (~P2(f6(a1),x45451,a4)+~P2(f6(a1),f6(f6(a1)),x45451)),
% 116.80/116.84 inference(scs_inference,[],[3966,2558,25,22])).
% 116.80/116.84 cnf(4550,plain,
% 116.80/116.84 (~P2(x45501,f6(a1),a4)+~P2(a1,x45501,f6(f6(a1)))),
% 116.80/116.84 inference(scs_inference,[],[2558,528,25])).
% 116.80/116.84 cnf(4552,plain,
% 116.80/116.84 (~P2(f6(a1),x45521,a4)+~P2(a1,x45521,f6(f6(a1)))),
% 116.80/116.84 inference(scs_inference,[],[2558,528,25,22])).
% 116.80/116.84 cnf(4962,plain,
% 116.80/116.84 (P3(f6(a4),x49621,f6(a4))+~P3(a4,x49621,a4)),
% 116.80/116.84 inference(scs_inference,[],[3810,28])).
% 116.80/116.84 cnf(4964,plain,
% 116.80/116.84 (P3(x49641,f6(a4),f6(a4))+~P3(a4,x49641,a4)),
% 116.80/116.84 inference(scs_inference,[],[3810,28,23])).
% 116.80/116.84 cnf(4988,plain,
% 116.80/116.84 (~P3(a4,x49881,a4)+~P3(a1,x49881,a2)),
% 116.80/116.84 inference(scs_inference,[],[4962,2849])).
% 116.80/116.84 cnf(5444,plain,
% 116.80/116.84 (~P2(x54441,f6(f6(a5)),a2)+~P2(x54441,a1,f6(a5))),
% 116.80/116.84 inference(scs_inference,[],[4390,22])).
% 116.80/116.84 cnf(5460,plain,
% 116.80/116.84 (~P2(f6(a1),x54601,x54602)+~P2(a1,x54601,a2)+~P2(x54602,a1,f6(a1))),
% 116.80/116.84 inference(scs_inference,[],[2558,4395,25])).
% 116.80/116.84 cnf(5508,plain,
% 116.80/116.84 (~P2(x55081,a1,f6(f6(a1)))+~P2(f6(a1),x55081,a2)),
% 116.80/116.84 inference(scs_inference,[],[4538,22])).
% 116.80/116.84 cnf(5544,plain,
% 116.80/116.84 (~P2(x55441,a1,f6(f6(a1)))+~P2(f6(a1),x55441,a4)),
% 116.80/116.84 inference(scs_inference,[],[4552,22])).
% 116.80/116.84 cnf(6474,plain,
% 116.80/116.84 (~P2(x64741,f3(f6(a4),f6(a4)),a4)+~P2(f6(a4),x64741,a4)),
% 116.80/116.84 inference(scs_inference,[],[3733,22])).
% 116.80/116.84 cnf(7628,plain,
% 116.80/116.84 (~P3(a4,a1,a4)),
% 116.80/116.84 inference(scs_inference,[],[3818,23])).
% 116.80/116.84 cnf(8867,plain,
% 116.80/116.84 (~P3(x88671,x88672,a2)+~P3(x88671,x88673,a4)+~P3(x88673,a1,x88672)),
% 116.80/116.84 inference(scs_inference,[],[4505,2913,40,28])).
% 116.80/116.84 cnf(9204,plain,
% 116.80/116.84 (~P3(x92041,x92042,a4)+~P3(a1,x92041,x92043)+~P3(x92043,x92042,a4)),
% 116.80/116.84 inference(scs_inference,[],[3818,3577,4469,27])).
% 116.80/116.84 cnf(9445,plain,
% 116.80/116.84 (~P3(x94451,x94452,a4)+~P3(x94451,x94453,a4)+~P3(x94453,a1,x94452)),
% 116.80/116.85 inference(scs_inference,[],[4505,7628,40,28])).
% 116.80/116.85 cnf(9446,plain,
% 116.80/116.85 (~P2(x94461,x94462,a5)+~P2(f6(a5),x94461,x94463)+~P2(x94463,x94462,a4)),
% 116.80/116.85 inference(scs_inference,[],[3904,4505,47,25])).
% 116.80/116.85 cnf(9758,plain,
% 116.80/116.85 (P2(f6(a1),a1,a1)),
% 116.80/116.85 inference(scs_inference,[],[1,8,15])).
% 116.80/116.85 cnf(9760,plain,
% 116.80/116.85 (P2(a1,a1,a1)),
% 116.80/116.85 inference(scs_inference,[],[1,8,15,13])).
% 116.80/116.85 cnf(9762,plain,
% 116.80/116.85 (P3(a4,a1,a1)),
% 116.80/116.85 inference(scs_inference,[],[1,8,15,13,14])).
% 116.80/116.85 cnf(9764,plain,
% 116.80/116.85 (P2(f6(a4),a1,f6(a4))),
% 116.80/116.85 inference(scs_inference,[],[1,2593,8,15,13,14,22])).
% 116.80/116.85 cnf(9766,plain,
% 116.80/116.85 (P1(f3(a1,a1))),
% 116.80/116.85 inference(scs_inference,[],[1,2593,8,15,13,14,22,10])).
% 116.80/116.85 cnf(9768,plain,
% 116.80/116.85 (P1(f7(a1,a1))),
% 116.80/116.85 inference(scs_inference,[],[1,2593,8,15,13,14,22,10,11])).
% 116.80/116.85 cnf(9770,plain,
% 116.80/116.85 (P2(a1,a1,f3(a1,a1))),
% 116.80/116.85 inference(scs_inference,[],[1,2593,8,15,13,14,22,10,11,17])).
% 116.80/116.85 cnf(9772,plain,
% 116.80/116.85 (P1(f8(a2))),
% 116.80/116.85 inference(scs_inference,[],[6,1,3,2593,8,15,13,14,22,10,11,17,16])).
% 116.80/116.85 cnf(9774,plain,
% 116.80/116.85 (P2(a1,a2,a2)),
% 116.80/116.85 inference(scs_inference,[],[6,1,3,2593,47,8,15,13,14,22,10,11,17,16,19])).
% 116.80/116.85 cnf(9776,plain,
% 116.80/116.85 (P3(f8(a2),a2,a4)),
% 116.80/116.85 inference(scs_inference,[],[6,1,3,2593,47,8,15,13,14,22,10,11,17,16,19,20])).
% 116.80/116.85 cnf(9780,plain,
% 116.80/116.85 (P3(a1,a1,f7(a1,a1))),
% 116.80/116.85 inference(scs_inference,[],[6,1,3,2593,47,8,15,13,14,22,10,11,17,16,19,20,60,18])).
% 116.80/116.85 cnf(9782,plain,
% 116.80/116.85 (P4(a1,f7(a1,a1))),
% 116.80/116.85 inference(scs_inference,[],[6,1,3,2593,47,35,8,15,13,14,22,10,11,17,16,19,20,60,18,21])).
% 116.80/116.85 cnf(9786,plain,
% 116.80/116.85 (~P3(a1,f8(a2),f8(a2))),
% 116.80/116.85 inference(scs_inference,[],[6,7628,1,3,3818,2593,47,35,8,15,13,14,22,10,11,17,16,19,20,60,18,21,28,27])).
% 116.80/116.85 cnf(9788,plain,
% 116.80/116.85 (P2(f6(a1),f6(a4),f6(a4))),
% 116.80/116.85 inference(scs_inference,[],[6,7628,1,3,3818,2593,47,35,8,15,13,14,22,10,11,17,16,19,20,60,18,21,28,27,25])).
% 116.80/116.85 cnf(9790,plain,
% 116.80/116.85 (P2(f7(a1,a1),f7(a1,a1),f7(a1,a1))),
% 116.80/116.85 inference(scs_inference,[],[6,7628,1,3,3818,2593,47,35,8,15,13,14,22,10,11,17,16,19,20,60,18,21,28,27,25,29])).
% 116.80/116.85 cnf(9792,plain,
% 116.80/116.85 (P3(a1,a4,a1)),
% 116.80/116.85 inference(scs_inference,[],[6,7628,1,3,3818,2593,47,35,8,15,13,14,22,10,11,17,16,19,20,60,18,21,28,27,25,29,23])).
% 116.80/116.85 cnf(9801,plain,
% 116.80/116.85 (P2(f6(a5),a5,a1)),
% 116.80/116.85 inference(scs_inference,[],[4,15])).
% 116.80/116.85 cnf(9805,plain,
% 116.87/116.85 (P2(a1,f3(a1,a1),f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9766,4,15,8,13])).
% 116.87/116.85 cnf(9807,plain,
% 116.87/116.85 (P2(a2,a1,a2)),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,4,15,8,13,22])).
% 116.87/116.85 cnf(9809,plain,
% 116.87/116.85 (P3(a2,f8(a2),a4)),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,9776,4,15,8,13,22,23])).
% 116.87/116.85 cnf(9811,plain,
% 116.87/116.85 (P3(a4,f3(a1,a1),f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,9776,4,15,8,13,22,23,14])).
% 116.87/116.85 cnf(9817,plain,
% 116.87/116.85 (P1(f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,9776,4,15,8,13,22,23,14,9204,9445,10])).
% 116.87/116.85 cnf(9819,plain,
% 116.87/116.85 (P2(a5,a5,f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,9776,4,15,8,13,22,23,14,9204,9445,10,17])).
% 116.87/116.85 cnf(9821,plain,
% 116.87/116.85 (P1(f7(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,9776,4,15,8,13,22,23,14,9204,9445,10,17,11])).
% 116.87/116.85 cnf(9823,plain,
% 116.87/116.85 (P1(f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,9776,528,4,2,15,8,13,22,23,14,9204,9445,10,17,11,16])).
% 116.87/116.85 cnf(9825,plain,
% 116.87/116.85 (P2(a1,a5,a5)),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,9776,528,4,2,50,15,8,13,22,23,14,9204,9445,10,17,11,16,19])).
% 116.87/116.85 cnf(9827,plain,
% 116.87/116.85 (P3(f8(a4),a4,a4)),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,9776,528,4,2,50,15,8,13,22,23,14,9204,9445,10,17,11,16,19,20])).
% 116.87/116.85 cnf(9829,plain,
% 116.87/116.85 (P3(a5,a5,f7(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,9776,528,4,2,50,15,8,13,22,23,14,9204,9445,10,17,11,16,19,20,18])).
% 116.87/116.85 cnf(9833,plain,
% 116.87/116.85 (P2(f3(a1,a1),a1,f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9774,9766,9770,9776,528,4,2,50,15,8,13,22,23,14,9204,9445,10,17,11,16,19,20,18,24,26])).
% 116.87/116.85 cnf(9835,plain,
% 116.87/116.85 (~P3(f8(a4),a1,a4)),
% 116.87/116.85 inference(scs_inference,[],[9762,9774,9766,9770,9776,528,7628,4,2,50,15,8,13,22,23,14,9204,9445,10,17,11,16,19,20,18,24,26,28])).
% 116.87/116.85 cnf(9837,plain,
% 116.87/116.85 (P2(a1,f3(a5,a5),f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9762,9774,9766,9770,9776,528,7628,4,2,50,15,8,13,22,23,14,9204,9445,10,17,11,16,19,20,18,24,26,28,25])).
% 116.87/116.85 cnf(9839,plain,
% 116.87/116.85 (P3(f8(a4),a1,a1)),
% 116.87/116.85 inference(scs_inference,[],[9762,9774,9766,9770,9776,528,7628,4,2,50,15,8,13,22,23,14,9204,9445,10,17,11,16,19,20,18,24,26,28,25,27])).
% 116.87/116.85 cnf(9841,plain,
% 116.87/116.85 (~P2(f8(a4),f6(a4),f6(a4))),
% 116.87/116.85 inference(scs_inference,[],[9762,9774,9766,9770,9776,2476,528,7628,4,2,3810,50,15,8,13,22,23,14,9204,9445,10,17,11,16,19,20,18,24,26,28,25,27,29])).
% 116.87/116.85 cnf(9845,plain,
% 116.87/116.85 (~P2(a5,a2,a5)),
% 116.87/116.85 inference(scs_inference,[],[9762,9774,9766,9770,9776,2476,528,7628,4,2,3810,50,15,8,13,22,23,14,9204,9445,10,17,11,16,19,20,18,24,26,28,25,27,29,8867,3621])).
% 116.87/116.85 cnf(9847,plain,
% 116.87/116.85 (P3(f3(a1,a1),a4,f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9792,9762,9774,9766,9770,9776,2476,528,7628,4,2,3810,50,15,8,13,22,23,14,9204,9445,10,17,11,16,19,20,18,24,26,28,25,27,29,8867,3621,30])).
% 116.87/116.85 cnf(9853,plain,
% 116.87/116.85 (P1(f6(a2))),
% 116.87/116.85 inference(scs_inference,[],[3,8])).
% 116.87/116.85 cnf(9855,plain,
% 116.87/116.85 (P2(f6(a2),a2,a1)),
% 116.87/116.85 inference(scs_inference,[],[3,8,15])).
% 116.87/116.85 cnf(9857,plain,
% 116.87/116.85 (P2(a1,f7(a1,a1),f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9768,3,8,15,13])).
% 116.87/116.85 cnf(9859,plain,
% 116.87/116.85 (P3(a4,f8(a4),a4)),
% 116.87/116.85 inference(scs_inference,[],[9768,9827,3,8,15,13,23])).
% 116.87/116.85 cnf(9861,plain,
% 116.87/116.85 (P3(a4,f7(a1,a1),f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9768,9827,3,8,15,13,23,14])).
% 116.87/116.85 cnf(9863,plain,
% 116.87/116.85 (P2(a5,a1,a5)),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9827,3,8,15,13,23,14,22])).
% 116.87/116.85 cnf(9865,plain,
% 116.87/116.85 (~P3(f8(a4),a1,f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9827,3,8,15,13,23,14,22,9445])).
% 116.87/116.85 cnf(9867,plain,
% 116.87/116.85 (~P3(a1,f8(a4),a4)),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9827,9792,3,8,15,13,23,14,22,9445,9204])).
% 116.87/116.85 cnf(9869,plain,
% 116.87/116.85 (P2(a2,a2,f3(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9827,9792,3,8,15,13,23,14,22,9445,9204,17])).
% 116.87/116.85 cnf(9871,plain,
% 116.87/116.85 (P1(f3(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9827,9792,3,8,15,13,23,14,22,9445,9204,17,10])).
% 116.87/116.85 cnf(9873,plain,
% 116.87/116.85 (P1(f7(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9827,9792,3,8,15,13,23,14,22,9445,9204,17,10,11])).
% 116.87/116.85 cnf(9875,plain,
% 116.87/116.85 (P2(a1,a4,a4)),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9827,9792,3,40,8,15,13,23,14,22,9445,9204,17,10,11,19])).
% 116.87/116.85 cnf(9877,plain,
% 116.87/116.85 (P3(a2,a2,f7(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9827,9792,3,40,8,15,13,23,14,22,9445,9204,17,10,11,19,18])).
% 116.87/116.85 cnf(9881,plain,
% 116.87/116.85 (~P3(f8(a4),f8(a4),a1)),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9827,9792,3,3818,40,35,8,15,13,23,14,22,9445,9204,17,10,11,19,18,24,28])).
% 116.87/116.85 cnf(9883,plain,
% 116.87/116.85 (P2(f6(a1),a5,a5)),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9758,9827,9792,3,3818,40,35,8,15,13,23,14,22,9445,9204,17,10,11,19,18,24,28,25])).
% 116.87/116.85 cnf(9885,plain,
% 116.87/116.85 (P3(f8(a4),f3(a1,a1),f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9825,9768,9811,9758,9827,9792,3,3818,40,35,8,15,13,23,14,22,9445,9204,17,10,11,19,18,24,28,25,27])).
% 116.87/116.85 cnf(9892,plain,
% 116.87/116.85 (~P2(f6(a2),a2,a2)),
% 116.87/116.85 inference(scs_inference,[],[9807,9825,9768,9811,9758,9809,9827,9792,33,3,3818,3725,40,35,8,15,13,23,14,22,9445,9204,17,10,11,19,18,24,28,25,27,30,29,3377])).
% 116.87/116.85 cnf(9894,plain,
% 116.87/116.85 (~P2(a2,f6(a2),a2)),
% 116.87/116.85 inference(scs_inference,[],[9807,9825,9768,9811,9758,9809,9827,9792,33,3,3818,3725,40,35,8,15,13,23,14,22,9445,9204,17,10,11,19,18,24,28,25,27,30,29,3377,3379])).
% 116.87/116.85 cnf(9898,plain,
% 116.87/116.85 (~P2(a2,f6(a2),a4)),
% 116.87/116.85 inference(scs_inference,[],[9807,9825,9768,9811,9758,9809,9827,9792,33,3,3818,3725,40,35,8,15,13,23,14,22,9445,9204,17,10,11,19,18,24,28,25,27,30,29,3377,3379,3383,3385])).
% 116.87/116.85 cnf(9904,plain,
% 116.87/116.85 (P2(f6(a4),a4,a1)),
% 116.87/116.85 inference(scs_inference,[],[2,15])).
% 116.87/116.85 cnf(9908,plain,
% 116.87/116.85 (P2(a1,f3(a2,a2),f3(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[9871,2,15,8,13])).
% 116.87/116.85 cnf(9910,plain,
% 116.87/116.85 (P3(a4,f3(a2,a2),f3(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[9871,2,15,8,13,14])).
% 116.87/116.85 cnf(9912,plain,
% 116.87/116.85 (P3(f3(a1,a1),f8(a4),f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9871,9885,2,15,8,13,14,23])).
% 116.87/116.85 cnf(9914,plain,
% 116.87/116.85 (P2(a4,a1,a4)),
% 116.87/116.85 inference(scs_inference,[],[9875,9871,9885,2,15,8,13,14,23,22])).
% 116.87/116.85 cnf(9918,plain,
% 116.87/116.85 (~P3(a1,f8(a4),f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[9875,9871,9869,9885,9827,2,15,8,13,14,23,22,52,9204])).
% 116.87/116.85 cnf(9920,plain,
% 116.87/116.85 (P1(f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9875,9871,9869,9885,9827,2,15,8,13,14,23,22,52,9204,10])).
% 116.87/116.85 cnf(9922,plain,
% 116.87/116.85 (P2(a4,a4,f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9875,9871,9869,9885,9827,2,15,8,13,14,23,22,52,9204,10,17])).
% 116.87/116.85 cnf(9924,plain,
% 116.87/116.85 (P1(f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9875,9871,9869,9885,9827,2,15,8,13,14,23,22,52,9204,10,17,11])).
% 116.87/116.85 cnf(9926,plain,
% 116.87/116.85 (P3(a4,a4,f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9875,9871,9869,9885,9827,2,15,8,13,14,23,22,52,9204,10,17,11,18])).
% 116.87/116.85 cnf(9928,plain,
% 116.87/116.85 (P2(f3(a5,a5),a1,f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9863,9875,9871,9869,9885,9819,9827,2,15,8,13,14,23,22,52,9204,10,17,11,18,26])).
% 116.87/116.85 cnf(9930,plain,
% 116.87/116.85 (P3(f3(a1,a1),f7(a4,a4),f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9863,9875,9871,9869,9885,9819,9847,9827,2,15,8,13,14,23,22,52,9204,10,17,11,18,26,27])).
% 116.87/116.85 cnf(9932,plain,
% 116.87/116.85 (P3(f7(a1,a1),a4,f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9863,9875,9871,9869,9885,9819,9847,9780,9827,9792,2,15,8,13,14,23,22,52,9204,10,17,11,18,26,27,28])).
% 116.87/116.85 cnf(9934,plain,
% 116.87/116.85 (P3(f3(a2,a2),f8(a2),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9863,9875,9871,9869,9885,9819,9847,9780,9809,9827,9792,2,15,8,13,14,23,22,52,9204,10,17,11,18,26,27,28,30])).
% 116.87/116.85 cnf(9936,plain,
% 116.87/116.85 (~P3(f6(a1),a4,a4)),
% 116.87/116.85 inference(scs_inference,[],[9863,9875,9871,9869,9885,9819,9847,9780,9809,9827,9792,3965,2,3816,997,15,8,13,14,23,22,52,9204,10,17,11,18,26,27,28,30,29])).
% 116.87/116.85 cnf(9944,plain,
% 116.87/116.85 (P2(a1,f3(a4,a4),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9920,13])).
% 116.87/116.85 cnf(9946,plain,
% 116.87/116.85 (P3(f7(a4,a4),f3(a1,a1),f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9930,9920,13,23])).
% 116.87/116.85 cnf(9948,plain,
% 116.87/116.85 (P2(f7(a1,a1),a1,f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9930,9857,9920,13,23,22])).
% 116.87/116.85 cnf(9950,plain,
% 116.87/116.85 (P3(a4,f3(a4,a4),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9930,9857,9920,13,23,22,14])).
% 116.87/116.85 cnf(9952,plain,
% 116.87/116.85 (P2(f6(a1),f3(a1,a1),f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9805,9930,9857,9920,9758,13,23,22,14,25])).
% 116.87/116.85 cnf(9954,plain,
% 116.87/116.85 (P3(f8(a4),f7(a1,a1),f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9805,9930,9857,9920,9839,9780,9758,13,23,22,14,25,27])).
% 116.87/116.85 cnf(9956,plain,
% 116.87/116.85 (~P3(f3(a2,a2),a4,a5)),
% 116.87/116.85 inference(scs_inference,[],[9805,9930,9857,9920,9934,9839,9780,9758,9776,33,13,23,22,14,25,27,28])).
% 116.87/116.85 cnf(9959,plain,
% 116.87/116.85 (P3(f3(a4,a4),f7(a1,a1),f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9805,9930,9857,9920,9934,9861,9922,9839,9790,9780,9758,9776,33,13,23,22,14,25,27,28,30])).
% 116.87/116.85 cnf(9967,plain,
% 116.87/116.85 (P2(a1,f7(a4,a4),f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9924,13])).
% 116.87/116.85 cnf(9969,plain,
% 116.87/116.85 (P3(f7(a1,a1),f3(a4,a4),f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9959,9924,13,23])).
% 116.87/116.85 cnf(9971,plain,
% 116.87/116.85 (P2(f3(a2,a2),a1,f3(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[9959,9908,9924,13,23,22])).
% 116.87/116.85 cnf(9973,plain,
% 116.87/116.85 (P3(a4,f7(a4,a4),f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9959,9908,9924,13,23,22,14])).
% 116.87/116.85 cnf(9975,plain,
% 116.87/116.85 (P2(f6(a1),f3(a5,a5),f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9959,9908,9924,9883,9819,13,23,22,14,25])).
% 116.87/116.85 cnf(9977,plain,
% 116.87/116.85 (P3(f8(a4),f7(a4,a4),f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9959,9908,9924,9926,9883,9819,9827,13,23,22,14,25,27])).
% 116.87/116.85 cnf(9979,plain,
% 116.87/116.85 (P3(f7(a4,a4),f3(a4,a4),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9959,9908,9924,9926,9950,9883,9819,9827,13,23,22,14,25,27,28])).
% 116.87/116.85 cnf(9981,plain,
% 116.87/116.85 (P3(f3(a4,a4),f8(a4),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9959,9908,9924,9926,9950,9883,9859,9819,9922,9827,13,23,22,14,25,27,28,30])).
% 116.87/116.85 cnf(9983,plain,
% 116.87/116.85 (P2(f7(a4,a4),a1,f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9914,9959,9908,9924,9926,9950,9883,9859,9819,9922,9827,9792,13,23,22,14,25,27,28,30,29])).
% 116.87/116.85 cnf(9990,plain,
% 116.87/116.85 (P2(a1,f7(a2,a2),f7(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[9873,13])).
% 116.87/116.85 cnf(9992,plain,
% 116.87/116.85 (P3(f3(a4,a4),f7(a4,a4),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9979,9873,13,23])).
% 116.87/116.85 cnf(9994,plain,
% 116.87/116.85 (P2(f3(a5,a5),f6(a1),f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9979,9975,9873,13,23,22])).
% 116.87/116.85 cnf(9996,plain,
% 116.87/116.85 (P3(a4,f3(a5,a5),f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9979,9975,9817,9873,13,23,22,14])).
% 116.87/116.85 cnf(10000,plain,
% 116.87/116.85 (P2(f6(a4),f3(a4,a4),a4)),
% 116.87/116.85 inference(scs_inference,[],[9979,9975,9817,9873,9967,9904,9875,9922,13,23,22,14,60,25])).
% 116.87/116.85 cnf(10002,plain,
% 116.87/116.85 (P3(f8(a4),f3(a4,a4),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9979,9975,9977,9817,9873,9967,9904,9875,9922,13,23,22,14,60,25,27])).
% 116.87/116.85 cnf(10004,plain,
% 116.87/116.85 (P3(f7(a1,a1),f8(a4),f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9969,9979,9975,9981,9977,9817,9873,9967,9904,9875,9922,13,23,22,14,60,25,27,28])).
% 116.87/116.85 cnf(10006,plain,
% 116.87/116.85 (~P3(f6(a4),f8(a4),a1)),
% 116.87/116.85 inference(scs_inference,[],[9969,9979,9867,9975,9981,9977,9817,9873,9967,9904,9875,9859,9922,13,23,22,14,60,25,27,28,30])).
% 116.87/116.85 cnf(10008,plain,
% 116.87/116.85 (~P2(a4,a1,f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9969,9979,9867,9975,9981,9977,9817,9873,9967,9904,9875,9859,9922,13,23,22,14,60,25,27,28,30,3782])).
% 116.87/116.85 cnf(10014,plain,
% 116.87/116.85 (P2(a1,f8(a2),f8(a2))),
% 116.87/116.85 inference(scs_inference,[],[9772,13])).
% 116.87/116.85 cnf(10016,plain,
% 116.87/116.85 (P3(f3(a5,a5),a4,f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9996,9772,13,23])).
% 116.87/116.85 cnf(10018,plain,
% 116.87/116.85 (P2(f7(a2,a2),a1,f7(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[9996,9990,9772,13,23,22])).
% 116.87/116.85 cnf(10020,plain,
% 116.87/116.85 (P3(a4,f8(a2),f8(a2))),
% 116.87/116.85 inference(scs_inference,[],[9996,9990,9772,13,23,22,14])).
% 116.87/116.85 cnf(10022,plain,
% 116.87/116.85 (~P2(f3(a4,a4),a1,a4)),
% 116.87/116.85 inference(scs_inference,[],[9996,9990,9772,10000,9914,3726,13,23,22,14,25])).
% 116.87/116.85 cnf(10024,plain,
% 116.87/116.85 (P3(f8(a4),f3(a5,a5),f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9996,9990,9772,10000,9914,9827,3726,13,23,22,14,25,27])).
% 116.87/116.85 cnf(10026,plain,
% 116.87/116.85 (P3(f7(a1,a1),f7(a4,a4),f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9992,9996,9990,9772,10000,9969,9914,9827,3726,13,23,22,14,25,27,28])).
% 116.87/116.85 cnf(10028,plain,
% 116.87/116.85 (P3(f3(a1,a1),a1,f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[9992,9996,9990,9772,10000,9969,9914,9790,9770,9780,9827,3726,13,23,22,14,25,27,28,30])).
% 116.87/116.85 cnf(10032,plain,
% 116.87/116.85 (~P3(a1,a1,a2)),
% 116.87/116.85 inference(scs_inference,[],[6,9992,9996,9990,9772,10000,9969,9914,9790,9770,9809,9780,9762,9827,3726,13,23,22,14,25,27,28,30,4125,29])).
% 116.87/116.85 cnf(10036,plain,
% 116.87/116.85 (P2(a1,f7(a5,a5),f7(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[9821,13])).
% 116.87/116.85 cnf(10038,plain,
% 116.87/116.85 (P3(f7(a4,a4),f7(a1,a1),f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[10026,9821,13,23])).
% 116.87/116.85 cnf(10040,plain,
% 116.87/116.85 (P2(f8(a2),a1,f8(a2))),
% 116.87/116.85 inference(scs_inference,[],[10026,9821,10014,13,23,22])).
% 116.87/116.85 cnf(10042,plain,
% 116.87/116.85 (P3(a4,f7(a5,a5),f7(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[10026,9821,10014,13,23,22,14])).
% 116.87/116.85 cnf(10046,plain,
% 116.87/116.85 (P2(f6(a1),a4,a4)),
% 116.87/116.85 inference(scs_inference,[],[10026,9821,10014,9788,10000,35,13,23,22,14,24,25])).
% 116.87/116.85 cnf(10048,plain,
% 116.87/116.85 (P3(f8(a4),f3(a2,a2),f3(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[10026,9910,9821,10014,9788,10000,9827,35,13,23,22,14,24,25,27])).
% 116.87/116.85 cnf(10050,plain,
% 116.87/116.85 (P3(f7(a4,a4),f7(a4,a4),f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10026,9973,9910,9821,10014,9788,10000,9926,9827,35,13,23,22,14,24,25,27,28])).
% 116.87/116.85 cnf(10052,plain,
% 116.87/116.85 (~P2(f7(a1,a1),f7(a1,a1),a2)),
% 116.87/116.85 inference(scs_inference,[],[10032,10026,9973,9910,9821,10014,9788,10000,9760,9926,9780,9827,35,13,23,22,14,24,25,27,28,30])).
% 116.87/116.85 cnf(10060,plain,
% 116.87/116.85 (P2(a1,f8(a4),f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[9823,13])).
% 116.87/116.85 cnf(10062,plain,
% 116.87/116.85 (P3(f3(a5,a5),f8(a4),f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[10024,9823,13,23])).
% 116.87/116.85 cnf(10064,plain,
% 116.87/116.85 (P2(f7(a5,a5),a1,f7(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[10024,10036,9823,13,23,22])).
% 116.87/116.85 cnf(10066,plain,
% 116.87/116.85 (P3(a4,f8(a4),f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[10024,10036,9823,13,23,22,14])).
% 116.87/116.85 cnf(10070,plain,
% 116.87/116.85 (~P2(f6(a1),a4,f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10008,10024,10036,9823,10046,9914,35,13,23,22,14,24,26])).
% 116.87/116.85 cnf(10072,plain,
% 116.87/116.85 (P2(f6(a5),f3(a5,a5),a5)),
% 116.87/116.85 inference(scs_inference,[],[10008,10024,10036,9823,10046,9801,9825,9819,9914,35,13,23,22,14,24,26,25])).
% 116.87/116.85 cnf(10074,plain,
% 116.87/116.85 (P3(f3(a5,a5),f7(a4,a4),f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[10008,10016,10024,10036,9823,10046,9801,9825,9926,9819,9914,35,13,23,22,14,24,26,25,27])).
% 116.87/116.85 cnf(10076,plain,
% 116.87/116.85 (P3(f7(a4,a4),f8(a4),f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10008,10016,10024,10036,9823,10046,9801,9825,9859,9926,9819,9914,35,13,23,22,14,24,26,25,27,28])).
% 116.87/116.85 cnf(10078,plain,
% 116.87/116.85 (~P3(f7(a1,a1),a4,a2)),
% 116.87/116.85 inference(scs_inference,[],[9932,10008,10016,10024,10052,10036,9823,10046,9801,9825,9790,9859,9926,9819,9914,35,13,23,22,14,24,26,25,27,28,29])).
% 116.87/116.85 cnf(10080,plain,
% 116.87/116.85 (~P2(a1,f7(a1,a1),a2)),
% 116.87/116.85 inference(scs_inference,[],[9932,10008,10016,10024,10052,10036,9823,10046,9801,9857,9825,9790,9859,9926,9819,9914,9792,35,13,23,22,14,24,26,25,27,28,29,30])).
% 116.87/116.85 cnf(10088,plain,
% 116.87/116.85 (P2(f3(a5,a5),f6(a5),a5)),
% 116.87/116.85 inference(scs_inference,[],[10074,10072,23,22])).
% 116.87/116.85 cnf(10090,plain,
% 116.87/116.85 (P3(a4,f6(a2),f6(a2))),
% 116.87/116.85 inference(scs_inference,[],[10074,9853,10072,23,22,14])).
% 116.87/116.85 cnf(10092,plain,
% 116.87/116.85 (P2(a5,f6(a1),a5)),
% 116.87/116.85 inference(scs_inference,[],[10074,9853,10072,9994,23,22,14,26])).
% 116.87/116.85 cnf(10094,plain,
% 116.87/116.85 (P2(f6(a1),f3(a4,a4),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10074,9853,10072,9994,10046,9922,23,22,14,26,25])).
% 116.87/116.85 cnf(10096,plain,
% 116.87/116.85 (P3(a4,a4,a4)),
% 116.87/116.85 inference(scs_inference,[],[10074,9853,10072,10020,9994,10046,9776,9922,23,22,14,26,25,27])).
% 116.87/116.85 cnf(10098,plain,
% 116.87/116.85 (P3(f8(a2),a2,f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10074,9853,10072,10020,9994,10046,9776,9922,9926,23,22,14,26,25,27,28])).
% 116.87/116.85 cnf(10100,plain,
% 116.87/116.85 (~P3(f3(a1,a1),a1,a2)),
% 116.87/116.85 inference(scs_inference,[],[10074,10028,9853,10072,10020,9994,9833,10052,10046,9776,9922,9926,9780,23,22,14,26,25,27,28,29])).
% 116.87/116.85 cnf(10102,plain,
% 116.87/116.85 (P3(a5,a4,a5)),
% 116.87/116.85 inference(scs_inference,[],[10074,10028,9853,10072,10020,9994,9833,10052,10046,10016,9776,9922,9926,9780,3804,23,22,14,26,25,27,28,29,30])).
% 116.87/116.85 cnf(10110,plain,
% 116.87/116.85 (P3(a4,a5,a5)),
% 116.87/116.85 inference(scs_inference,[],[10102,23])).
% 116.87/116.85 cnf(10112,plain,
% 116.87/116.85 (P2(f8(a4),a1,f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[10102,10060,23,22])).
% 116.87/116.85 cnf(10114,plain,
% 116.87/116.85 (P3(a4,f7(a2,a2),f7(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[10102,10060,9873,23,22,14])).
% 116.87/116.85 cnf(10118,plain,
% 116.87/116.85 (~P2(a1,f6(a2),a1)),
% 116.87/116.85 inference(scs_inference,[],[6,10102,10060,10092,9855,9873,9801,9760,23,22,14,3621,26])).
% 116.87/116.85 cnf(10122,plain,
% 116.87/116.85 (P3(f7(a5,a5),a4,f7(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[6,10102,9936,9829,10060,10092,9855,9873,9801,9760,9809,23,22,14,3621,26,27,28])).
% 116.87/116.85 cnf(10130,plain,
% 116.87/116.85 (P2(f3(a4,a4),a1,f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9944,22])).
% 116.87/116.85 cnf(10132,plain,
% 116.87/116.85 (P3(f3(a2,a2),f8(a4),f3(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[10048,9944,22,23])).
% 116.87/116.85 cnf(10134,plain,
% 116.87/116.85 (P3(a4,a2,a2)),
% 116.87/116.85 inference(scs_inference,[],[10048,9944,3,22,23,14])).
% 116.87/116.85 cnf(10138,plain,
% 116.87/116.85 (~P2(f6(a2),f3(a2,a2),a1)),
% 116.87/116.85 inference(scs_inference,[],[6,10048,9944,10060,9855,9869,3,22,23,14,60,26])).
% 116.87/116.85 cnf(10140,plain,
% 116.87/116.85 (P2(f6(a1),f7(a4,a4),f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[6,10048,9944,9967,10060,9855,9869,9758,3,22,23,14,60,26,25])).
% 116.87/116.85 cnf(10142,plain,
% 116.87/116.85 (P3(f7(a4,a4),a4,f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[6,10048,9944,10096,9967,10060,9855,9869,9758,9926,3,22,23,14,60,26,25,28])).
% 116.87/116.85 cnf(10144,plain,
% 116.87/116.85 (~P3(f7(a1,a1),f8(a4),a2)),
% 116.87/116.85 inference(scs_inference,[],[6,10004,10048,9944,10096,9967,10060,9855,10052,9869,9790,9758,9926,3,22,23,14,60,26,25,28,29])).
% 116.87/116.85 cnf(10156,plain,
% 116.87/116.85 (P3(a2,a4,a2)),
% 116.87/116.85 inference(scs_inference,[],[10134,23])).
% 116.87/116.85 cnf(10158,plain,
% 116.87/116.85 (P2(f7(a4,a4),f6(a1),f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10134,10140,23,22])).
% 116.87/116.85 cnf(10160,plain,
% 116.87/116.85 (~P2(f6(a1),f3(a4,a4),a4)),
% 116.87/116.85 inference(scs_inference,[],[10134,10140,10130,10022,10094,23,22,26])).
% 116.87/116.85 cnf(10162,plain,
% 116.87/116.85 (P2(f3(a4,a4),f3(a1,a1),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10134,10140,10130,10022,10094,9770,23,22,26,25])).
% 116.87/116.85 cnf(10164,plain,
% 116.87/116.85 (~P3(f8(a2),f7(a2,a2),a5)),
% 116.87/116.85 inference(scs_inference,[],[10134,10140,10130,10098,10022,10094,9877,9770,33,23,22,26,25,28])).
% 116.87/116.85 cnf(10165,plain,
% 116.87/116.85 (~P3(x101651,a2,a5)),
% 116.87/116.85 inference(rename_variables,[],[33])).
% 116.87/116.85 cnf(10167,plain,
% 116.87/116.85 (~P2(a2,a2,a5)),
% 116.87/116.85 inference(scs_inference,[],[10134,10140,10130,10098,10022,10094,9877,9770,9922,33,10165,23,22,26,25,28,30])).
% 116.87/116.85 cnf(10177,plain,
% 116.87/116.85 (P2(f3(a1,a1),f3(a4,a4),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10162,22])).
% 116.87/116.85 cnf(10179,plain,
% 116.87/116.85 (P3(f6(a2),a4,f6(a2))),
% 116.87/116.85 inference(scs_inference,[],[10162,10090,22,23])).
% 116.87/116.85 cnf(10181,plain,
% 116.87/116.85 (~P2(f6(a4),a1,f6(a1))),
% 116.87/116.85 inference(scs_inference,[],[10162,10090,10160,9944,10000,22,23,26])).
% 116.87/116.85 cnf(10183,plain,
% 116.87/116.85 (P3(a2,f8(a4),a2)),
% 116.87/116.85 inference(scs_inference,[],[10156,10162,10090,10160,9944,10000,9859,22,23,26,28])).
% 116.87/116.85 cnf(10185,plain,
% 116.87/116.85 (P3(f3(a4,a4),a5,f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[10156,10162,10090,10160,9944,10110,10000,9859,9819,9922,22,23,26,28,30])).
% 116.87/116.85 cnf(10189,plain,
% 116.87/116.85 (P2(f6(a2),a1,f6(a2))),
% 116.87/116.85 inference(scs_inference,[],[9845,10156,10162,10090,10160,9944,10110,10000,9760,9859,9819,9914,9922,22,23,26,28,30,29,1571])).
% 116.87/116.85 cnf(10196,plain,
% 116.87/116.85 (P3(a5,f3(a4,a4),f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[10185,23])).
% 116.87/116.85 cnf(10198,plain,
% 116.87/116.85 (P2(f3(a1,a1),f6(a1),f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[10185,9952,23,22])).
% 116.87/116.85 cnf(10202,plain,
% 116.87/116.85 (~P2(a4,a2,a4)),
% 116.87/116.85 inference(scs_inference,[],[6,10185,9952,9990,9904,35,23,22,24,26])).
% 116.87/116.85 cnf(10204,plain,
% 116.87/116.85 (P2(f6(a5),a5,f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[6,10185,9952,9990,9863,9904,9801,9770,35,23,22,24,26,25])).
% 116.87/116.85 cnf(10206,plain,
% 116.87/116.85 (P3(f7(a2,a2),f8(a4),f7(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[6,10185,10183,9952,9990,9863,9904,9801,9877,9770,35,23,22,24,26,25,28])).
% 116.87/116.85 cnf(10208,plain,
% 116.87/116.85 (~P2(f7(a1,a1),a1,f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[6,9865,10185,10183,9952,9990,9839,9863,10060,9904,9801,9877,9770,9780,35,23,22,24,26,25,28,30])).
% 116.87/116.85 cnf(10210,plain,
% 116.87/116.85 (~P2(f3(a1,a1),a1,a4)),
% 116.87/116.85 inference(scs_inference,[],[6,9865,10185,10183,9952,9990,9839,9863,10060,9904,9801,9877,9770,9780,35,23,22,24,26,25,28,30,9446])).
% 116.87/116.85 cnf(10212,plain,
% 116.87/116.85 (~P2(f3(a1,a1),a1,a2)),
% 116.87/116.85 inference(scs_inference,[],[6,9865,10185,10183,9952,9990,9839,9863,10060,9904,9801,9877,9770,9780,35,23,22,24,26,25,28,30,9446,3621])).
% 116.87/116.85 cnf(10219,plain,
% 116.87/116.85 (P2(a5,f6(a5),f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[10204,22])).
% 116.87/116.85 cnf(10223,plain,
% 116.87/116.85 (~P2(f3(a1,a1),f6(a1),a4)),
% 116.87/116.85 inference(scs_inference,[],[10206,10204,10092,22,23,9446])).
% 116.87/116.85 cnf(10225,plain,
% 116.87/116.85 (~P2(f3(a1,a1),f6(a1),a2)),
% 116.87/116.85 inference(scs_inference,[],[10206,10204,10092,22,23,9446,3621])).
% 116.87/116.85 cnf(10229,plain,
% 116.87/116.85 (P2(f6(a2),f3(a1,a1),f6(a2))),
% 116.87/116.85 inference(scs_inference,[],[10181,10206,10204,10189,9764,9788,10092,9770,22,23,9446,3621,26,25])).
% 116.87/116.85 cnf(10234,plain,
% 116.87/116.85 (~P2(f7(a1,a1),a1,a2)),
% 116.87/116.85 inference(scs_inference,[],[10181,10206,10078,10204,10189,9948,9764,9934,10098,9788,9932,10092,9770,9792,33,22,23,9446,3621,26,25,28,30])).
% 116.87/116.85 cnf(10236,plain,
% 116.87/116.85 (~P2(f6(a4),a1,a1)),
% 116.87/116.85 inference(scs_inference,[],[10181,10206,10078,10204,10189,9948,9764,9934,10098,9788,9932,10092,9770,9792,33,22,23,9446,3621,26,25,28,30,1019])).
% 116.87/116.85 cnf(10245,plain,
% 116.87/116.85 (P3(f8(a4),a4,f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[10066,23])).
% 116.87/116.85 cnf(10247,plain,
% 116.87/116.85 (P2(f3(a1,a1),f6(a2),f6(a2))),
% 116.87/116.85 inference(scs_inference,[],[10229,10066,23,22])).
% 116.87/116.85 cnf(10249,plain,
% 116.87/116.85 (~P2(f6(a4),f3(a1,a1),f6(a1))),
% 116.87/116.85 inference(scs_inference,[],[10177,10229,10066,10160,10000,23,22,26])).
% 116.87/116.85 cnf(10251,plain,
% 116.87/116.85 (P2(f6(a1),f3(a2,a2),f3(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[10177,10229,10066,10160,9908,10000,9758,23,22,26,25])).
% 116.87/116.85 cnf(10253,plain,
% 116.87/116.85 (P3(f6(a2),f8(a4),f6(a2))),
% 116.87/116.85 inference(scs_inference,[],[10177,10229,10066,10179,10160,9908,10000,9758,9859,23,22,26,25,28])).
% 116.87/116.85 cnf(10258,plain,
% 116.87/116.85 (P2(f3(a2,a2),f6(a1),f3(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[10251,22])).
% 116.87/116.85 cnf(10260,plain,
% 116.87/116.85 (P3(f8(a4),f6(a2),f6(a2))),
% 116.87/116.85 inference(scs_inference,[],[10251,10253,22,23])).
% 116.87/116.85 cnf(10262,plain,
% 116.87/116.85 (~P2(a1,a4,f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10251,10070,10253,10046,997,22,23,26])).
% 116.87/116.85 cnf(10264,plain,
% 116.87/116.85 (P2(f3(a1,a1),a1,a1)),
% 116.87/116.85 inference(scs_inference,[],[10251,10247,10070,10253,10046,9855,997,22,23,26,25])).
% 116.87/116.85 cnf(10266,plain,
% 116.87/116.85 (P3(f3(a2,a2),a4,f3(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[10251,10247,10070,10253,10245,10132,10046,9855,997,22,23,26,25,28])).
% 116.87/116.85 cnf(10268,plain,
% 116.87/116.85 (~P3(f3(a1,a1),a4,a4)),
% 116.87/116.85 inference(scs_inference,[],[10198,10251,10247,10070,10223,10253,10245,10132,9847,10046,9855,3816,997,22,23,26,25,28,29])).
% 116.87/116.85 cnf(10274,plain,
% 116.87/116.85 (P3(f3(a4,a4),a4,f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[9950,23])).
% 116.87/116.85 cnf(10276,plain,
% 116.87/116.85 (P2(a1,f3(a1,a1),a1)),
% 116.87/116.85 inference(scs_inference,[],[10264,9950,23,22])).
% 116.87/116.85 cnf(10278,plain,
% 116.87/116.85 (~P2(a1,f7(a1,a1),f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[10208,10264,9950,9948,9857,23,22,26])).
% 116.87/116.85 cnf(10280,plain,
% 116.87/116.85 (P2(f3(a1,a1),f3(a5,a5),f3(a5,a5))),
% 116.87/116.85 inference(scs_inference,[],[10208,10264,9837,9950,9948,9857,23,22,26,25])).
% 116.87/116.85 cnf(10286,plain,
% 116.87/116.85 (~P2(a1,f3(a1,a1),a4)),
% 116.87/116.85 inference(scs_inference,[],[10208,10225,10264,9837,9950,10198,9948,9857,9847,3816,23,22,26,25,29,46,60])).
% 116.87/116.85 cnf(10291,plain,
% 116.87/116.85 (P3(f7(a2,a2),a4,f7(a2,a2))),
% 116.87/116.85 inference(scs_inference,[],[10280,10114,22,23])).
% 116.87/116.85 cnf(10293,plain,
% 116.87/116.85 (~P2(f6(a4),f3(a4,a4),a1)),
% 116.87/116.85 inference(scs_inference,[],[10286,10280,10114,10162,10000,22,23,26])).
% 116.87/116.85 cnf(10295,plain,
% 116.87/116.85 (P2(f6(a1),f6(a2),f6(a2))),
% 116.87/116.85 inference(scs_inference,[],[10286,10280,10114,10162,10247,9952,10000,22,23,26,25])).
% 116.87/116.85 cnf(10297,plain,
% 116.87/116.85 (P2(f7(a4,a4),f7(a4,a4),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10286,10280,9973,10114,10162,10247,9952,9992,10000,9922,22,23,26,25,29])).
% 116.87/116.85 cnf(10304,plain,
% 116.87/116.85 (P3(a1,f3(a1,a1),f7(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[10028,23])).
% 116.87/116.85 cnf(10306,plain,
% 116.87/116.85 (P2(f6(a2),f6(a1),f6(a2))),
% 116.87/116.85 inference(scs_inference,[],[10295,10028,23,22])).
% 116.87/116.85 cnf(10308,plain,
% 116.87/116.85 (~P2(f3(a1,a1),a2,f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[6,10295,10276,10028,23,22,26])).
% 116.87/116.85 cnf(10310,plain,
% 116.87/116.85 (P2(f3(a1,a1),a5,a5)),
% 116.87/116.85 inference(scs_inference,[],[6,10295,10276,10280,10028,10088,23,22,26,25])).
% 116.87/116.85 cnf(10318,plain,
% 116.87/116.85 (P2(a5,f3(a1,a1),a5)),
% 116.87/116.85 inference(scs_inference,[],[10310,22])).
% 116.87/116.85 cnf(10320,plain,
% 116.87/116.85 (P3(f8(a4),a2,a2)),
% 116.87/116.85 inference(scs_inference,[],[10310,10183,22,23])).
% 116.87/116.85 cnf(10322,plain,
% 116.87/116.85 (~P2(f3(a1,a1),f3(a1,a1),a4)),
% 116.87/116.85 inference(scs_inference,[],[10310,10219,10183,3903,22,23,26])).
% 116.87/116.85 cnf(10324,plain,
% 116.87/116.85 (P2(f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 116.87/116.85 inference(scs_inference,[],[10310,10219,10183,3903,22,23,26,25])).
% 116.87/116.85 cnf(10331,plain,
% 116.87/116.85 (P3(f8(a2),a4,f8(a2))),
% 116.87/116.85 inference(scs_inference,[],[10020,23])).
% 116.87/116.85 cnf(10333,plain,
% 116.87/116.85 (P2(f3(a4,a4),f6(a1),f3(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10094,10020,23,22])).
% 116.87/116.85 cnf(10337,plain,
% 116.87/116.85 (~P2(f3(a1,a1),f3(a1,a1),a2)),
% 116.87/116.85 inference(scs_inference,[],[10318,10320,10094,10020,10204,9776,23,22,4125,3621])).
% 116.87/116.85 cnf(10341,plain,
% 116.87/116.85 (P2(f3(a1,a1),f7(a4,a4),f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10236,10318,10320,10094,9833,10020,10264,9967,10276,10204,9776,23,22,4125,3621,26,25])).
% 116.87/116.85 cnf(10345,plain,
% 116.87/116.85 (~P3(f3(a1,a1),f8(a4),a2)),
% 116.87/116.85 inference(scs_inference,[],[10324,9786,10236,10308,10318,10320,9912,10094,9833,10020,10264,9967,10014,10276,10204,9904,9776,23,22,4125,3621,26,25,30,29])).
% 116.87/116.85 cnf(10349,plain,
% 116.87/116.85 (P3(a2,f8(a2),f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[10324,9786,10236,10308,10318,10320,9912,10295,10094,10245,9833,10020,10264,9967,10014,10276,10204,9904,9776,9809,23,22,4125,3621,26,25,30,29,5460,28])).
% 116.87/116.85 cnf(10354,plain,
% 116.87/116.85 (P2(f7(a4,a4),f3(a1,a1),f7(a4,a4))),
% 116.87/116.85 inference(scs_inference,[],[10341,22])).
% 116.87/116.85 cnf(10356,plain,
% 116.87/116.85 (P3(f8(a2),a2,f8(a4))),
% 116.87/116.85 inference(scs_inference,[],[10341,10349,22,23])).
% 116.87/116.85 cnf(10358,plain,
% 116.87/116.85 (~P2(a1,f3(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10341,10349,10318,9801,22,23,3621])).
% 116.87/116.86 cnf(10360,plain,
% 116.87/116.86 (P3(f8(a4),f8(a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10341,10349,10318,10320,9801,22,23,3621,27])).
% 116.87/116.86 cnf(10362,plain,
% 116.87/116.86 (~P2(f3(a1,a1),a2,a1)),
% 116.87/116.86 inference(scs_inference,[],[6,10341,10349,10318,10320,9774,10264,9801,22,23,3621,27,26])).
% 116.87/116.86 cnf(10364,plain,
% 116.87/116.86 (~P2(f6(a1),f3(a2,a2),a5)),
% 116.87/116.86 inference(scs_inference,[],[6,10341,10349,9956,10266,10318,10320,10251,9774,10264,9801,3816,22,23,3621,27,26,30])).
% 116.87/116.86 cnf(10366,plain,
% 116.87/116.86 (P2(f3(a1,a1),f7(a1,a1),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[6,10341,10349,9956,10304,10266,10112,10318,9885,10320,10251,9774,10264,9801,3816,22,23,3621,27,26,30,29])).
% 116.87/116.86 cnf(10372,plain,
% 116.87/116.86 (P3(f8(a2),f3(a2,a2),f3(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[9934,23])).
% 116.87/116.86 cnf(10374,plain,
% 116.87/116.86 (P2(f7(a1,a1),f3(a1,a1),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10366,9934,23,22])).
% 116.87/116.86 cnf(10376,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f7(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[10366,10210,9948,9934,23,22,26])).
% 116.87/116.86 cnf(10378,plain,
% 116.87/116.86 (P2(f3(a1,a1),f7(a5,a5),f7(a5,a5))),
% 116.87/116.86 inference(scs_inference,[],[10366,10210,10036,9948,9934,10264,23,22,26,25])).
% 116.87/116.86 cnf(10380,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f7(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10366,10210,10345,9912,10036,10004,9948,9934,10264,23,22,26,25,30])).
% 116.87/116.86 cnf(10390,plain,
% 116.87/116.86 (P3(a2,f8(a2),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10378,10098,22,23])).
% 116.87/116.86 cnf(10392,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f3(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10374,10378,10212,10098,9833,22,23,26])).
% 116.87/116.86 cnf(10394,plain,
% 116.87/116.86 (P2(f7(a1,a1),f7(a5,a5),f7(a5,a5))),
% 116.87/116.86 inference(scs_inference,[],[10374,10378,10212,10098,9833,22,23,26,25])).
% 116.87/116.86 cnf(10402,plain,
% 116.87/116.86 (P3(a1,f8(a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[9839,23])).
% 116.87/116.86 cnf(10404,plain,
% 116.87/116.86 (P2(f7(a5,a5),f7(a1,a1),f7(a5,a5))),
% 116.87/116.86 inference(scs_inference,[],[10394,9839,23,22])).
% 116.87/116.86 cnf(10406,plain,
% 116.87/116.86 (~P2(a1,f3(a2,a2),a5)),
% 116.87/116.86 inference(scs_inference,[],[10394,10364,9839,10251,997,23,22,26])).
% 116.87/116.86 cnf(10408,plain,
% 116.87/116.86 (P2(f7(a1,a1),f7(a4,a4),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10394,10364,10341,10374,9839,10251,997,23,22,26,25])).
% 116.87/116.86 cnf(10410,plain,
% 116.87/116.86 (~P2(a1,a1,f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10394,9918,10364,10341,10374,9839,10251,9760,997,23,22,26,25,30])).
% 116.87/116.86 cnf(10414,plain,
% 116.87/116.86 (~P3(a2,f8(a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[6,10394,9918,10364,10341,10140,10374,9839,10183,10251,9774,9760,997,23,22,26,25,30,5460,29])).
% 116.87/116.86 cnf(10418,plain,
% 116.87/116.86 (P2(f7(a4,a4),f7(a1,a1),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10408,22])).
% 116.87/116.86 cnf(10422,plain,
% 116.87/116.86 (P2(f7(a1,a1),f3(a4,a4),f3(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10408,10337,10324,10297,9952,22,26,25])).
% 116.87/116.86 cnf(10424,plain,
% 116.87/116.86 (~P2(f8(a4),a1,a1)),
% 116.87/116.86 inference(scs_inference,[],[10408,10360,10337,9881,10402,10324,10297,10112,9952,22,26,25,30])).
% 116.87/116.86 cnf(10433,plain,
% 116.87/116.86 (P2(f3(a4,a4),f7(a1,a1),f3(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10422,22])).
% 116.87/116.86 cnf(10435,plain,
% 116.87/116.86 (~P2(f6(a1),f6(a1),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10422,9841,9788,22,26])).
% 116.87/116.86 cnf(10437,plain,
% 116.87/116.86 (~P3(f6(a4),f8(a4),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10422,9841,10006,10402,9764,9788,10264,22,26,30])).
% 116.87/116.86 cnf(10439,plain,
% 116.87/116.86 (~P3(f3(a4,a4),f7(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10422,9841,10006,10038,10402,9764,10297,9788,10052,10264,22,26,30,29])).
% 116.87/116.86 cnf(10444,plain,
% 116.87/116.86 (P2(a4,f6(a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[10046,22])).
% 116.87/116.86 cnf(10446,plain,
% 116.87/116.86 (~P2(a1,f3(a1,a1),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10278,10366,10046,10276,22,26])).
% 116.87/116.86 cnf(10448,plain,
% 116.87/116.86 (P2(f7(a2,a2),f3(a1,a1),f7(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[10278,10018,10366,10046,10276,9770,22,26,25])).
% 116.87/116.86 cnf(10450,plain,
% 116.87/116.86 (~P3(a4,f3(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[10376,10278,10018,9811,10304,10366,10046,10276,9770,9914,22,26,25,29])).
% 116.87/116.86 cnf(10452,plain,
% 116.87/116.86 (~P2(f6(a1),a4,a1)),
% 116.87/116.86 inference(scs_inference,[],[10376,10278,10018,9811,10304,10366,10046,10276,9770,9914,22,26,25,29,3427])).
% 116.87/116.86 cnf(10464,plain,
% 116.87/116.86 (P3(a4,f8(a4),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10448,10076,10066,9926,22,27])).
% 116.87/116.86 cnf(10466,plain,
% 116.87/116.86 (~P2(a1,f8(a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[10448,10424,10076,10066,10112,10060,9926,22,27,26])).
% 116.87/116.86 cnf(10468,plain,
% 116.87/116.86 (P3(f7(a4,a4),f6(a2),f6(a2))),
% 116.87/116.86 inference(scs_inference,[],[10448,10424,10260,10076,10090,10066,10112,10060,9926,22,27,26,28])).
% 116.87/116.86 cnf(10470,plain,
% 116.87/116.86 (P2(f6(a1),f7(a2,a2),f7(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[10448,10424,10260,10076,10090,10066,9990,10112,10060,9758,9926,22,27,26,28,25])).
% 116.87/116.86 cnf(10476,plain,
% 116.87/116.86 (P3(f8(a4),a4,f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[6,10448,10437,10424,10444,10260,10076,10090,10066,10324,9990,10112,9912,10060,9762,9758,9926,22,27,26,28,25,30,29,23])).
% 116.87/116.86 cnf(10482,plain,
% 116.87/116.86 (P3(f6(a2),f7(a4,a4),f6(a2))),
% 116.87/116.86 inference(scs_inference,[],[10468,23])).
% 116.87/116.86 cnf(10488,plain,
% 116.87/116.86 (~P2(a1,f7(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[10470,10468,10234,9835,9807,10112,9839,9774,9780,23,22,26,30])).
% 116.87/116.86 cnf(10490,plain,
% 116.87/116.86 (~P3(a1,a2,f6(a2))),
% 116.87/116.86 inference(scs_inference,[],[9892,10470,10468,10234,9835,9807,10320,10112,9839,10060,9774,9780,23,22,26,30,29])).
% 116.87/116.86 cnf(10496,plain,
% 116.87/116.86 (P2(f6(a4),f6(a1),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[9788,22])).
% 116.87/116.86 cnf(10498,plain,
% 116.87/116.86 (~P2(a5,f6(a2),a5)),
% 116.87/116.86 inference(scs_inference,[],[10118,9788,9801,22,26])).
% 116.87/116.86 cnf(10502,plain,
% 116.87/116.86 (~P2(f3(a2,a2),f6(a1),a5)),
% 116.87/116.86 inference(scs_inference,[],[10118,10482,10490,10258,9956,10266,9788,10098,9801,3816,22,26,28,30])).
% 116.87/116.86 cnf(10509,plain,
% 116.87/116.86 (P2(a2,f6(a2),a1)),
% 116.87/116.86 inference(scs_inference,[],[9855,22])).
% 116.87/116.86 cnf(10513,plain,
% 116.87/116.86 (~P2(f6(a1),f6(a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10496,10444,146,9875,9855,2561,22,26,25])).
% 116.87/116.86 cnf(10515,plain,
% 116.87/116.86 (~P3(f6(a1),a4,a2)),
% 116.87/116.86 inference(scs_inference,[],[10496,10202,10096,10444,146,9875,9855,2561,22,26,25,29])).
% 116.87/116.86 cnf(10521,plain,
% 116.87/116.86 (P2(f3(a4,a4),f6(a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[10000,22])).
% 116.87/116.86 cnf(10523,plain,
% 116.87/116.86 (~P2(a2,f6(a2),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10410,10509,10189,10000,22,26])).
% 116.87/116.86 cnf(10525,plain,
% 116.87/116.86 (P2(f3(a1,a1),f3(a2,a2),f3(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[10410,10509,10189,9908,10000,10264,22,26,25])).
% 116.87/116.86 cnf(10527,plain,
% 116.87/116.86 (~P3(f6(a2),f8(a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[6,10410,10509,10189,10402,9908,10183,10000,9855,10264,22,26,25,29])).
% 116.87/116.86 cnf(10533,plain,
% 116.87/116.86 (P2(f3(a2,a2),f3(a1,a1),f3(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[10525,22])).
% 116.87/116.86 cnf(10535,plain,
% 116.87/116.86 (~P2(f6(a2),f7(a1,a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[10525,10080,10509,9807,22,26])).
% 116.87/116.86 cnf(10537,plain,
% 116.87/116.86 (P2(f3(a1,a1),a4,a4)),
% 116.87/116.86 inference(scs_inference,[],[10525,10080,10521,10509,10177,9807,22,26,25])).
% 116.87/116.86 cnf(10541,plain,
% 116.87/116.86 (~P3(a4,a4,a1)),
% 116.87/116.86 inference(scs_inference,[],[10525,10452,10080,10521,10527,10306,10509,10177,10253,10096,9807,10046,9855,3816,22,26,25,30,29])).
% 116.87/116.86 cnf(10547,plain,
% 116.87/116.86 (P2(a4,f3(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[10537,22])).
% 116.87/116.86 cnf(10549,plain,
% 116.87/116.86 (~P2(f3(a1,a1),a4,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10537,10444,2561,22,26])).
% 116.87/116.86 cnf(10551,plain,
% 116.87/116.86 (P2(f7(a1,a1),a4,a4)),
% 116.87/116.86 inference(scs_inference,[],[10537,10374,10444,2561,22,26,25])).
% 116.87/116.86 cnf(10553,plain,
% 116.87/116.86 (~P2(f3(a4,a4),f6(a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[10541,10537,10274,10521,10374,10444,2561,3810,22,26,25,30])).
% 116.87/116.86 cnf(10555,plain,
% 116.87/116.86 (~P3(f3(a1,a1),f7(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[10541,10537,10274,10322,9930,10521,10374,10324,10444,2561,3810,22,26,25,30,29])).
% 116.87/116.86 cnf(10562,plain,
% 116.87/116.86 (P2(a4,f7(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[10551,22])).
% 116.87/116.86 cnf(10566,plain,
% 116.87/116.86 (~P2(f7(a4,a4),f7(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[10551,10476,9983,10008,10206,10291,10297,22,27,26])).
% 116.87/116.86 cnf(10568,plain,
% 116.87/116.86 (P2(f6(a1),f8(a2),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10551,10476,9983,10008,10206,10291,10014,10297,9758,22,27,26,25])).
% 116.87/116.86 cnf(10570,plain,
% 116.87/116.86 (~P3(a1,a4,f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10551,10476,9983,10008,10206,10291,10014,10297,10112,9758,9827,22,27,26,25,29])).
% 116.87/116.86 cnf(10580,plain,
% 116.87/116.86 (P2(f8(a2),f6(a1),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10568,22])).
% 116.87/116.86 cnf(10582,plain,
% 116.87/116.86 (~P2(f3(a2,a2),f3(a1,a1),a5)),
% 116.87/116.86 inference(scs_inference,[],[10533,10502,10568,10198,22,26])).
% 116.87/116.86 cnf(10584,plain,
% 116.87/116.86 (~P2(f3(a2,a2),f7(a1,a1),a5)),
% 116.87/116.86 inference(scs_inference,[],[10533,10502,10568,10198,10366,22,26,25])).
% 116.87/116.86 cnf(10586,plain,
% 116.87/116.86 (~P2(a1,a1,f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10533,10502,10568,10570,10198,10366,9760,9792,22,26,25,30])).
% 116.87/116.86 cnf(10588,plain,
% 116.87/116.86 (~P3(f7(a1,a1),a1,a2)),
% 116.87/116.86 inference(scs_inference,[],[6,10533,10502,10568,10562,10570,10198,10366,9762,9760,9792,22,26,25,30,29])).
% 116.87/116.86 cnf(10594,plain,
% 116.87/116.86 (P2(a4,f6(a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[9904,22])).
% 116.87/116.86 cnf(10596,plain,
% 116.87/116.86 (~P3(f7(a4,a4),a2,a1)),
% 116.87/116.86 inference(scs_inference,[],[10414,10356,10390,9904,22,27])).
% 116.87/116.86 cnf(10598,plain,
% 116.87/116.86 (~P2(f3(a4,a4),f6(a4),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10414,10496,10356,10521,10390,9904,2561,22,27,26])).
% 116.87/116.86 cnf(10600,plain,
% 116.87/116.86 (P2(f8(a2),f3(a1,a1),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10414,10496,10040,10356,10521,10390,9904,9770,2561,22,27,26,25])).
% 116.87/116.86 cnf(10604,plain,
% 116.87/116.86 (~P3(a4,a4,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10549,10450,10547,10414,10496,10040,9811,10356,10521,10390,10096,10537,9847,9904,9770,2561,22,27,26,25,30,29])).
% 116.87/116.86 cnf(10613,plain,
% 116.87/116.86 (P2(f3(a1,a1),f8(a2),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10600,22])).
% 116.87/116.86 cnf(10615,plain,
% 116.87/116.86 (P3(a2,f3(a4,a4),f3(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[10600,9910,10372,9809,22,27])).
% 116.87/116.86 cnf(10617,plain,
% 116.87/116.86 (P3(f3(a4,a4),a2,f3(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[10600,9910,10372,10132,10356,9934,9809,22,27,28])).
% 116.87/116.86 cnf(10619,plain,
% 116.87/116.86 (~P2(a4,a1,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10598,10600,10594,9910,10372,10132,10356,9934,9922,9809,22,27,28,26])).
% 116.87/116.86 cnf(10621,plain,
% 116.87/116.86 (P2(f7(a1,a1),a1,a1)),
% 116.87/116.86 inference(scs_inference,[],[10598,10600,10594,10551,9910,10372,10132,10356,9934,9922,9809,22,27,28,26,25])).
% 116.87/116.86 cnf(10623,plain,
% 116.87/116.86 (~P2(f7(a1,a1),a4,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10598,10600,10594,10604,10551,9910,10372,10132,10356,9934,9932,10096,9922,9809,22,27,28,26,25,30])).
% 116.87/116.86 cnf(10625,plain,
% 116.87/116.86 (~P3(f3(a4,a4),a4,a4)),
% 116.87/116.86 inference(scs_inference,[],[10566,10598,10600,10594,10604,10142,10551,9910,10372,10132,10356,9934,9932,10096,10297,9922,9809,22,27,28,26,25,30,29])).
% 116.87/116.86 cnf(10627,plain,
% 116.87/116.86 (P2(f7(a1,a1),f6(a2),f6(a2))),
% 116.87/116.86 inference(scs_inference,[],[10566,10598,10600,10594,10604,10142,10551,9910,10372,10132,10356,9934,9932,10096,10297,9922,9809,22,27,28,26,25,30,29,1555])).
% 116.87/116.86 cnf(10633,plain,
% 116.87/116.86 (P2(f6(a2),f7(a1,a1),f6(a2))),
% 116.87/116.86 inference(scs_inference,[],[10627,22])).
% 116.87/116.86 cnf(10635,plain,
% 116.87/116.86 (~P2(f7(a1,a1),a2,a1)),
% 116.87/116.86 inference(scs_inference,[],[6,10627,10621,9774,22,26])).
% 116.87/116.86 cnf(10637,plain,
% 116.87/116.86 (P2(a4,f6(a4),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[6,10627,10621,10594,10496,9774,997,22,26,25])).
% 116.87/116.86 cnf(10639,plain,
% 116.87/116.86 (~P3(f3(a1,a1),f8(a4),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[6,10627,10621,10547,10566,10594,10496,10464,9859,9774,997,22,26,25,29])).
% 116.87/116.86 cnf(10645,plain,
% 116.87/116.86 (P2(f6(a4),a4,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10637,22])).
% 116.87/116.86 cnf(10649,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f6(a2),a1)),
% 116.87/116.86 inference(scs_inference,[],[10633,10535,10637,10615,10627,10372,10390,22,28,26])).
% 116.87/116.86 cnf(10651,plain,
% 116.87/116.86 (P2(f7(a1,a1),f6(a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10633,10535,10637,10615,10627,10372,10551,10390,22,28,26,25])).
% 116.87/116.86 cnf(10653,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f3(a1,a1),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10639,10633,10535,10637,10615,10627,10372,10551,9912,10324,10390,22,28,26,25,30])).
% 116.87/116.86 cnf(10655,plain,
% 116.87/116.86 (~P3(f6(a2),a4,a1)),
% 116.87/116.86 inference(scs_inference,[],[6,10639,10633,10535,10637,10615,10627,10372,10551,9912,10156,10324,10390,9855,9792,22,28,26,25,30,29])).
% 116.87/116.86 cnf(10657,plain,
% 116.87/116.86 (P3(f3(a2,a2),f7(a4,a4),f3(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[6,10639,10633,10535,10637,10615,10627,10372,10551,9912,10156,10324,10390,9855,9792,22,28,26,25,30,29,23])).
% 116.87/116.86 cnf(10661,plain,
% 116.87/116.86 (P2(f6(a1),f7(a1,a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10651,22])).
% 116.87/116.86 cnf(10663,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f6(a4),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10651,10623,10645,22,26])).
% 116.87/116.86 cnf(10665,plain,
% 116.87/116.86 (P2(f6(a1),f6(a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10651,10623,10645,9788,22,26,25])).
% 116.87/116.86 cnf(10667,plain,
% 116.87/116.86 (~P2(f3(a4,a4),f7(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[10651,10623,10625,10645,10433,10274,9788,9932,22,26,25,30])).
% 116.87/116.86 cnf(10671,plain,
% 116.87/116.86 (P2(a1,f7(a1,a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[10621,22])).
% 116.87/116.86 cnf(10673,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f3(a2,a2),a2)),
% 116.87/116.86 inference(scs_inference,[],[10138,10633,10621,9855,22,26])).
% 116.87/116.86 cnf(10675,plain,
% 116.87/116.86 (P2(f6(a4),a4,f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10138,10633,10621,10645,10547,9952,9855,22,26,25])).
% 116.87/116.86 cnf(10677,plain,
% 116.87/116.86 (~P2(f6(a1),f7(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10515,10138,10661,10633,10621,10645,10547,9952,9932,9855,3816,22,26,25,30])).
% 116.87/116.86 cnf(10679,plain,
% 116.87/116.86 (~P3(f3(a4,a4),f7(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[10515,10138,10661,10050,10633,10621,10566,10645,10547,9952,9932,10297,9855,3816,22,26,25,30,29])).
% 116.87/116.86 cnf(10684,plain,
% 116.87/116.86 (P2(a4,f6(a4),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10675,22])).
% 116.87/116.86 cnf(10686,plain,
% 116.87/116.86 (P3(f8(a4),f7(a5,a5),f7(a5,a5))),
% 116.87/116.86 inference(scs_inference,[],[10675,10042,9827,22,27])).
% 116.87/116.86 cnf(10688,plain,
% 116.87/116.86 (P2(f3(a5,a5),f7(a1,a1),f3(a5,a5))),
% 116.87/116.86 inference(scs_inference,[],[10671,10675,9928,10042,9827,22,27,26])).
% 116.87/116.86 cnf(10690,plain,
% 116.87/116.86 (~P2(f6(a4),f7(a1,a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[10671,10675,9928,10042,10594,529,9827,22,27,26,25])).
% 116.87/116.86 cnf(10692,plain,
% 116.87/116.86 (~P3(f3(a4,a4),f8(a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[10671,10667,10675,9928,10433,10042,9981,10594,10004,529,9827,22,27,26,25,29])).
% 116.87/116.86 cnf(10694,plain,
% 116.87/116.86 (P3(f7(a5,a5),f8(a4),f7(a5,a5))),
% 116.87/116.86 inference(scs_inference,[],[10671,10667,10675,9928,10433,10042,9981,10594,10004,529,9827,22,27,26,25,29,23])).
% 116.87/116.86 cnf(10699,plain,
% 116.87/116.86 (P2(f7(a1,a1),f3(a5,a5),f3(a5,a5))),
% 116.87/116.86 inference(scs_inference,[],[10688,22])).
% 116.87/116.86 cnf(10701,plain,
% 116.87/116.86 (~P2(a4,f3(a1,a1),f3(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10688,10262,10675,10594,22,26])).
% 116.87/116.86 cnf(10703,plain,
% 116.87/116.86 (P2(f7(a1,a1),f3(a2,a2),f3(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[10688,10262,10675,10621,9908,10594,22,26,25])).
% 116.87/116.86 cnf(10711,plain,
% 116.87/116.86 (P2(f3(a2,a2),f7(a1,a1),f3(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[10703,22])).
% 116.87/116.86 cnf(10716,plain,
% 116.87/116.86 (~P2(f7(a1,a1),a2,f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[6,10703,10617,10671,10196,33,22,28,26])).
% 116.87/116.86 cnf(10718,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f6(a4),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[6,10703,10249,10617,10684,10675,10671,10196,33,22,28,26,25])).
% 116.87/116.86 cnf(10722,plain,
% 116.87/116.86 (~P3(f3(a2,a2),f7(a4,a4),a2)),
% 116.87/116.86 inference(scs_inference,[],[6,10703,10249,10673,10692,10617,10684,10657,10333,10026,10675,10671,10196,9981,10521,33,22,28,26,25,30,29])).
% 116.87/116.86 cnf(10729,plain,
% 116.87/116.86 (P2(a5,f6(a5),a1)),
% 116.87/116.86 inference(scs_inference,[],[9801,22])).
% 116.87/116.86 cnf(10733,plain,
% 116.87/116.86 (P2(f7(a1,a1),f8(a2),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10711,10584,10613,10525,10374,9801,22,26,25])).
% 116.87/116.86 cnf(10735,plain,
% 116.87/116.86 (~P2(f3(a2,a2),f7(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10711,10584,10722,10613,10525,10657,10026,10374,9801,22,26,25,30])).
% 116.87/116.86 cnf(10737,plain,
% 116.87/116.86 (P2(f8(a4),f8(a4),f3(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10711,10584,10722,10613,10525,10657,10066,10026,9981,10374,9801,9922,22,26,25,30,29])).
% 116.87/116.86 cnf(10744,plain,
% 116.87/116.86 (P2(f8(a2),f7(a1,a1),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10733,22])).
% 116.87/116.86 cnf(10750,plain,
% 116.87/116.86 (P2(f7(a1,a1),f7(a2,a2),f7(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[10588,10488,10733,10661,10621,9990,10444,9780,22,26,28,25])).
% 116.87/116.86 cnf(10752,plain,
% 116.87/116.86 (~P3(f7(a1,a1),f8(a4),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10588,10488,10733,10562,10661,10566,10621,9990,10464,10444,9859,9780,22,26,28,25,29])).
% 116.87/116.86 cnf(10759,plain,
% 116.87/116.86 (~P2(f6(a4),f6(a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10750,10718,10684,10637,22,26])).
% 116.87/116.86 cnf(10761,plain,
% 116.87/116.86 (P2(f7(a1,a1),a5,a5)),
% 116.87/116.86 inference(scs_inference,[],[10750,10718,10699,10684,10637,10088,22,26,25])).
% 116.87/116.86 cnf(10763,plain,
% 116.87/116.86 (~P2(f8(a4),f8(a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[10750,10718,10699,10737,10692,10360,10684,10637,10088,22,26,25,30])).
% 116.87/116.86 cnf(10772,plain,
% 116.87/116.86 (~P2(a4,a4,a4)),
% 116.87/116.86 inference(scs_inference,[],[10759,2861])).
% 116.87/116.86 cnf(10773,plain,
% 116.87/116.86 (P2(a5,f7(a1,a1),a5)),
% 116.87/116.86 inference(scs_inference,[],[10761,22])).
% 116.87/116.86 cnf(10778,plain,
% 116.87/116.86 (~P2(f7(a1,a1),a1,a4)),
% 116.87/116.86 inference(scs_inference,[],[10761,10729,10617,9969,3903,33,22,28,26])).
% 116.87/116.86 cnf(10780,plain,
% 116.87/116.86 (~P2(f3(a2,a2),a1,a5)),
% 116.87/116.86 inference(scs_inference,[],[10761,10729,9971,10617,9956,10266,9969,3903,9792,33,22,28,26,30])).
% 116.87/116.86 cnf(10791,plain,
% 116.87/116.86 (P2(a1,f6(a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[9758,22])).
% 116.87/116.86 cnf(10793,plain,
% 116.87/116.86 (~P2(f6(a5),a5,f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10690,10773,9758,9801,22,26])).
% 116.87/116.86 cnf(10795,plain,
% 116.87/116.86 (P2(f6(a4),f3(a1,a1),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10690,10773,10684,10645,9788,9758,9801,22,26,25])).
% 116.87/116.86 cnf(10799,plain,
% 116.87/116.86 (~P3(f3(a1,a1),f7(a4,a4),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10100,10690,10773,10653,10675,10684,10645,9930,9807,10324,9788,9762,9758,9801,22,26,25,30,29])).
% 116.87/116.86 cnf(10804,plain,
% 116.87/116.86 (P2(f3(a1,a1),f6(a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10795,22])).
% 116.87/116.86 cnf(10806,plain,
% 116.87/116.86 (~P2(f3(a2,a2),f6(a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10735,10795,10258,10661,22,26])).
% 116.87/116.86 cnf(10808,plain,
% 116.87/116.86 (P2(f7(a1,a1),f8(a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10735,10795,10258,10661,10621,10060,22,26,25])).
% 116.87/116.86 cnf(10810,plain,
% 116.87/116.86 (~P3(f7(a1,a1),a4,f6(a2))),
% 116.87/116.86 inference(scs_inference,[],[10735,10795,10498,10773,10258,10661,10102,10621,10060,22,26,25,29])).
% 116.87/116.86 cnf(10817,plain,
% 116.87/116.86 (P2(f8(a4),f7(a1,a1),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10808,22])).
% 116.87/116.86 cnf(10819,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f3(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[10808,10763,10737,22,26])).
% 116.87/116.86 cnf(10821,plain,
% 116.87/116.86 (P2(f7(a1,a1),a1,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10791,10808,10763,10737,10651,9948,22,26,25])).
% 116.87/116.86 cnf(10823,plain,
% 116.87/116.86 (~P2(f6(a1),a2,f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10791,10808,10763,10737,10651,9948,9774,22,26,25,5460])).
% 116.87/116.86 cnf(10828,plain,
% 116.87/116.86 (P2(a1,f7(a1,a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10821,22])).
% 116.87/116.86 cnf(10830,plain,
% 116.87/116.86 (P3(f7(a5,a5),f7(a4,a4),f7(a5,a5))),
% 116.87/116.86 inference(scs_inference,[],[10821,10694,10476,10122,22,27])).
% 116.87/116.86 cnf(10832,plain,
% 116.87/116.86 (~P2(a1,f6(a1),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10821,10586,10694,10476,10122,10671,22,27,26])).
% 116.87/116.86 cnf(10834,plain,
% 116.87/116.86 (P2(f8(a4),f6(a1),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10817,10821,10586,10694,10476,10122,10671,10112,22,27,26,25])).
% 116.87/116.86 cnf(10843,plain,
% 116.87/116.86 (P2(f6(a1),f8(a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10834,22])).
% 116.87/116.86 cnf(10847,plain,
% 116.87/116.86 (P2(f3(a1,a1),f6(a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10293,10804,10834,10645,10000,22,26,25])).
% 116.87/116.86 cnf(10857,plain,
% 116.87/116.86 (P2(f6(a1),f3(a1,a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10847,22])).
% 116.87/116.86 cnf(10861,plain,
% 116.87/116.86 (P2(f3(a1,a1),f8(a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10847,10843,10584,10703,10711,22,26,25])).
% 116.87/116.86 cnf(10863,plain,
% 116.87/116.86 (~P2(f6(a2),f6(a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[10847,10843,10655,10584,10306,10703,10711,10179,3816,22,26,25,30])).
% 116.87/116.86 cnf(10871,plain,
% 116.87/116.86 (P2(f8(a4),f3(a1,a1),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10861,22])).
% 116.87/116.86 cnf(10877,plain,
% 116.87/116.86 (~P2(a5,f6(a5),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10861,10828,10404,10064,10570,10729,10394,10036,10102,3804,22,26,25,30])).
% 116.87/116.86 cnf(10879,plain,
% 116.87/116.86 (~P3(f7(a1,a1),a4,f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10861,10828,10404,10064,10570,10817,10729,10394,10036,10476,10102,10566,9827,3804,22,26,25,30,29])).
% 116.87/116.86 cnf(10883,plain,
% 116.87/116.86 (P2(f6(a1),a1,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[997,22])).
% 116.87/116.86 cnf(10885,plain,
% 116.87/116.86 (P2(f7(a1,a1),a2,a2)),
% 116.87/116.86 inference(scs_inference,[],[10621,9774,997,22,25])).
% 116.87/116.86 cnf(10887,plain,
% 116.87/116.86 (~P2(a1,f3(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[10819,10422,9857,10621,9774,997,22,25,26])).
% 116.87/116.86 cnf(10893,plain,
% 116.87/116.86 (P2(a2,f7(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10885,22])).
% 116.87/116.86 cnf(10897,plain,
% 116.87/116.86 (P2(a1,f6(a1),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10513,10883,10885,10857,10791,9805,22,26,25])).
% 116.87/116.86 cnf(10899,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f7(a1,a1),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10513,10752,10883,10885,10857,10791,9805,9790,10004,22,26,25,30])).
% 116.87/116.86 cnf(10901,plain,
% 116.87/116.86 (~P3(f7(a4,a4),f3(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10380,10513,10752,10883,10885,10857,10791,9983,9805,10304,9790,9946,10004,22,26,25,30,29])).
% 116.87/116.86 cnf(10903,plain,
% 116.87/116.86 (P2(f6(a1),a1,f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10897,22])).
% 116.87/116.86 cnf(10905,plain,
% 116.87/116.86 (~P2(f6(a1),a2,a1)),
% 116.87/116.86 inference(scs_inference,[],[6,10897,10885,10828,22,25])).
% 116.87/116.86 cnf(10907,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f7(a4,a4),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[6,10899,10897,10885,10418,10828,10408,22,25,26])).
% 116.87/116.86 cnf(10909,plain,
% 116.87/116.86 (~P2(f6(a2),f3(a1,a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[6,10899,10897,10527,10885,10418,10229,10828,10408,10253,9912,22,25,26,30])).
% 116.87/116.86 cnf(10911,plain,
% 116.87/116.86 (~P3(f3(a4,a4),f7(a1,a1),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[6,10899,10897,10527,10885,10418,10229,10038,10828,10408,10253,9912,10297,22,25,26,30,29])).
% 116.87/116.86 cnf(10913,plain,
% 116.87/116.86 (P2(f6(a5),a1,f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[718,22])).
% 116.87/116.86 cnf(10915,plain,
% 116.87/116.86 (~P2(f6(a5),f8(a4),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[10466,10729,718,22,26])).
% 116.87/116.86 cnf(10917,plain,
% 116.87/116.86 (P2(f7(a1,a1),f6(a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10466,10729,10621,2593,718,22,26,25])).
% 116.87/116.86 cnf(10919,plain,
% 116.87/116.86 (~P2(a4,f3(a1,a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[10466,10541,10729,10547,10621,9847,10096,2593,718,22,26,25,30])).
% 116.87/116.86 cnf(10923,plain,
% 116.87/116.86 (~P3(a5,f7(a4,a4),x109231)+P3(a5,x109231,f7(a5,a5))),
% 116.87/116.86 inference(scs_inference,[],[10907,10466,10871,10830,10541,9954,10729,10547,9829,10621,9847,10096,2593,718,22,26,25,30,29,27])).
% 116.87/116.86 cnf(10930,plain,
% 116.87/116.86 (P2(f6(a4),f7(a1,a1),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10917,22])).
% 116.87/116.86 cnf(10932,plain,
% 116.87/116.86 (P2(f7(a1,a1),f3(a1,a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10917,10897,10651,9948,22,25])).
% 116.87/116.86 cnf(10936,plain,
% 116.87/116.86 (~P3(f7(a1,a1),f8(a4),f6(a2))),
% 116.87/116.86 inference(scs_inference,[],[9894,10893,10917,10249,10897,10795,10651,9948,10183,22,25,26,29])).
% 116.87/116.86 cnf(10942,plain,
% 116.87/116.86 (P2(f3(a1,a1),f7(a1,a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10932,22])).
% 116.87/116.86 cnf(10944,plain,
% 116.87/116.86 (~P2(a2,f3(a1,a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10932,2740,10893,22,25])).
% 116.87/116.86 cnf(10946,plain,
% 116.87/116.86 (~P2(f7(a1,a1),a2,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10932,10677,2740,10893,10885,22,25,26])).
% 116.87/116.86 cnf(10954,plain,
% 116.87/116.86 (P2(f7(a1,a1),f6(a5),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[10621,718,25])).
% 116.87/116.86 cnf(10960,plain,
% 116.87/116.86 (~P2(f8(a2),f8(a2),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10911,10823,10942,10763,10433,9959,10885,10408,10356,10621,9776,718,25,26,30,29])).
% 116.87/116.86 cnf(10962,plain,
% 116.87/116.86 (P2(f6(a5),f7(a1,a1),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[10911,10823,10942,10763,10433,9959,10885,10408,10356,10621,9776,718,25,26,30,29,22])).
% 116.87/116.86 cnf(10968,plain,
% 116.87/116.86 (P2(a1,f6(a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10903,10223,10897,10661,10791,9857,26,25])).
% 116.87/116.86 cnf(10970,plain,
% 116.87/116.86 (~P2(f8(a4),f3(a1,a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[10903,10223,9881,10871,10897,10360,10661,10791,9857,9912,26,25,30])).
% 116.87/116.86 cnf(10972,plain,
% 116.87/116.86 (~P3(f6(a1),a4,f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10960,10903,10580,10223,9881,10871,10897,10331,10360,10661,10791,9857,9912,26,25,30,29])).
% 116.87/116.86 cnf(10974,plain,
% 116.87/116.86 (P2(f6(a1),a1,f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10960,10903,10580,10223,9881,10871,10897,10331,10360,10661,10791,9857,9912,26,25,30,29,22])).
% 116.87/116.86 cnf(10976,plain,
% 116.87/116.86 (P2(f3(a1,a1),f7(a1,a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10974,10847,25])).
% 116.87/116.86 cnf(10978,plain,
% 116.87/116.86 (~P2(a1,f7(a4,a4),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10974,10968,10907,10847,10140,25,26])).
% 116.87/116.86 cnf(10980,plain,
% 116.87/116.86 (~P3(f7(a1,a1),a4,f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10930,10974,10759,10968,10907,10847,10140,3810,25,26,29])).
% 116.87/116.86 cnf(10982,plain,
% 116.87/116.86 (P2(f7(a1,a1),f3(a1,a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10930,10974,10759,10968,10907,10847,10140,3810,25,26,29,22])).
% 116.87/116.86 cnf(10987,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f6(a4),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10976,10663,10917,26])).
% 116.87/116.86 cnf(10989,plain,
% 116.87/116.86 (P2(f3(a1,a1),f6(a5),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[10976,10663,10954,10917,26,25])).
% 116.87/116.86 cnf(10991,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f7(a1,a1),f6(a2))),
% 116.87/116.86 inference(scs_inference,[],[10976,10663,10936,10954,10917,9790,10004,26,25,30])).
% 116.87/116.86 cnf(10995,plain,
% 116.87/116.86 (P2(f6(a5),f3(a1,a1),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[10976,10982,10663,10936,10954,10392,10917,10026,9790,10004,9930,26,25,30,29,22])).
% 116.87/116.86 cnf(10997,plain,
% 116.87/116.86 (P2(f6(a1),f6(a5),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[10989,10903,718,25])).
% 116.87/116.86 cnf(10999,plain,
% 116.87/116.86 (P2(f6(a5),f6(a1),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[10989,10962,10913,10968,10903,718,25,26])).
% 116.87/116.86 cnf(11001,plain,
% 116.87/116.86 (~P3(f6(a1),f7(a4,a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10679,10989,10962,10913,10968,10903,10333,9992,10521,718,25,26,30])).
% 116.87/116.86 cnf(11003,plain,
% 116.87/116.86 (~P3(f3(a4,a4),f7(a1,a1),f6(a2))),
% 116.87/116.86 inference(scs_inference,[],[10679,10991,10989,10962,10913,10968,10903,10333,10038,9992,10521,10297,718,25,26,30,29])).
% 116.87/116.86 cnf(11011,plain,
% 116.87/116.86 (P2(f7(a1,a1),f7(a1,a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10887,10665,10968,9944,10821,10264,26,25])).
% 116.87/116.86 cnf(11013,plain,
% 116.87/116.86 (~P3(f7(a1,a1),f3(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[10887,10665,10450,10968,9944,10821,10562,9811,10537,10264,26,25,30])).
% 116.87/116.86 cnf(11015,plain,
% 116.87/116.86 (~P3(f7(a1,a1),a4,f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10887,10665,10960,10450,10744,10968,9944,10821,10562,10331,9811,10537,10264,26,25,30,29])).
% 116.87/116.86 cnf(11017,plain,
% 116.87/116.86 (~P3(f8(a4),a5,x110171)+P3(x110171,a5,f7(a5,a5))),
% 116.87/116.86 inference(scs_inference,[],[10887,10665,10960,10450,10744,10686,10968,9944,10821,10562,10331,9829,9811,10537,10264,26,25,30,29,28])).
% 116.87/116.86 cnf(11024,plain,
% 116.87/116.86 (P2(f6(a1),f7(a1,a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10665,10974,25])).
% 116.87/116.86 cnf(11030,plain,
% 116.87/116.86 (P2(f7(a1,a1),f6(a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10406,11011,10991,10665,10974,10773,10729,9969,25,26,29,22])).
% 116.87/116.86 cnf(11039,plain,
% 116.87/116.86 (P2(f6(a1),f6(a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10677,11011,10976,10903,10828,26,25])).
% 116.87/116.86 cnf(11046,plain,
% 116.87/116.86 (~P2(f6(a5),f3(a5,a5),f3(a2,a2))),
% 116.87/116.86 inference(scs_inference,[],[10780,9928,10072,26])).
% 116.87/116.86 cnf(11048,plain,
% 116.87/116.86 (P2(a5,f6(a5),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10780,10999,9928,10847,10219,10072,26,25])).
% 116.87/116.86 cnf(11050,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f3(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[10780,10555,10999,9928,10847,10219,10374,10026,10072,9930,26,25,30])).
% 116.87/116.86 cnf(11054,plain,
% 116.87/116.86 (P2(f6(a5),a5,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10780,10555,10999,10410,9928,10847,10737,10219,9839,10374,10026,10072,9930,26,25,30,29,22])).
% 116.87/116.86 cnf(11056,plain,
% 116.87/116.86 (~P2(f6(a1),f7(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[11054,10773,9446])).
% 116.87/116.86 cnf(11058,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f6(a1),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10877,11054,11048,10761,10773,9446,26])).
% 116.87/116.86 cnf(11060,plain,
% 116.87/116.86 (P2(f6(a1),a2,a2)),
% 116.87/116.86 inference(scs_inference,[],[10877,11054,11048,11024,10761,10773,10885,9446,26,25])).
% 116.87/116.86 cnf(11066,plain,
% 116.87/116.86 (P2(a2,f6(a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10439,10877,11054,10970,11048,11024,10177,10761,10893,10773,10066,9959,10885,10547,9912,9446,26,25,30,29,22])).
% 116.87/116.86 cnf(11070,plain,
% 116.87/116.86 (P2(f6(a5),a5,f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11039,11054,10092,25])).
% 116.87/116.86 cnf(11074,plain,
% 116.87/116.86 (~P2(f6(a1),f6(a1),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[11058,10879,11039,11054,10092,3816,25,26,30])).
% 116.87/116.86 cnf(11078,plain,
% 116.87/116.86 (P2(a5,f6(a5),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11058,10879,11039,10435,11054,10092,3816,25,26,30,29,22])).
% 116.87/116.86 cnf(11080,plain,
% 116.87/116.86 (P2(f3(a1,a1),a2,a2)),
% 116.87/116.86 inference(scs_inference,[],[11060,10847,25])).
% 116.87/116.86 cnf(11086,plain,
% 116.87/116.86 (P2(a2,f3(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10793,11060,11070,11066,10997,2740,10847,10156,3816,25,26,29,22])).
% 116.87/116.86 cnf(11102,plain,
% 116.87/116.86 (P3(f8(a4),f8(a4),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[9977,10245,10464,28])).
% 116.87/116.86 cnf(11104,plain,
% 116.87/116.86 (~P2(f3(a1,a1),a2,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10944,11080,11086,9977,10245,10464,28,26])).
% 116.87/116.86 cnf(11108,plain,
% 116.87/116.86 (~P3(f3(a1,a1),a4,f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11003,10944,11080,11086,10600,9977,10960,10627,10162,10245,10464,9959,10331,28,26,30,29])).
% 116.87/116.86 cnf(11110,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f7(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[11003,10944,11080,11086,11070,10600,9977,10960,10627,10162,10245,10773,10464,9959,10331,28,26,30,29,9446])).
% 116.87/116.86 cnf(11113,plain,
% 116.87/116.86 (~P2(f3(a4,a4),f6(a4),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11110,10930,10521,26])).
% 116.87/116.86 cnf(11117,plain,
% 116.87/116.86 (~P3(f6(a1),f8(a4),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[11110,10810,11030,11024,10930,10907,10004,9932,10521,3816,26,30,29])).
% 116.87/116.86 cnf(11119,plain,
% 116.87/116.86 (P2(f3(a1,a1),f3(a1,a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10942,10857,10374,25])).
% 116.87/116.86 cnf(11121,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f6(a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[11050,11030,10942,10857,10374,25,26])).
% 116.87/116.86 cnf(11123,plain,
% 116.87/116.86 (~P3(f6(a1),a4,f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[11050,10877,11030,11048,10942,10857,10102,10374,3804,25,26,29])).
% 116.87/116.86 cnf(11128,plain,
% 116.87/116.86 (P2(f6(a1),f3(a1,a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10982,10974,9805,25])).
% 116.87/116.86 cnf(11130,plain,
% 116.87/116.86 (~P2(f6(a4),f7(a1,a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10982,10249,10930,10974,9805,25,26])).
% 116.87/116.86 cnf(11132,plain,
% 116.87/116.86 (~P2(a1,f7(a1,a1),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[11117,10982,10249,10930,10974,9805,10828,10402,10004,25,26,30])).
% 116.87/116.86 cnf(11134,plain,
% 116.87/116.86 (~P3(f3(a4,a4),f7(a1,a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[11117,11110,10982,10249,10930,9954,10974,9805,10737,10828,10402,10004,25,26,30,29])).
% 116.87/116.86 cnf(11136,plain,
% 116.87/116.86 (P2(f3(a1,a1),f6(a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11117,11110,10982,10249,10930,9954,10974,9805,10737,10828,10402,10004,25,26,30,29,22])).
% 116.87/116.86 cnf(11139,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f7(a1,a1),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10793,10989,11070,26])).
% 116.87/116.86 cnf(11141,plain,
% 116.87/116.86 (~P3(f3(a1,a1),f3(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[10901,10793,11080,10989,10354,11070,9946,26,30])).
% 116.87/116.86 cnf(11150,plain,
% 116.87/116.86 (P3(f7(a4,a4),a2,a2)),
% 116.87/116.86 inference(scs_inference,[],[10987,11102,10897,10320,9788,26,28])).
% 116.87/116.86 cnf(11152,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f6(a1),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10987,10980,11136,11102,10897,10320,9788,9847,3816,26,28,30])).
% 116.87/116.86 cnf(11156,plain,
% 116.87/116.86 (P3(a2,f7(a4,a4),a2)),
% 116.87/116.86 inference(scs_inference,[],[10987,10980,11119,11136,11102,10322,10897,10320,9788,9912,9847,3816,26,28,30,29,23])).
% 116.87/116.86 cnf(11160,plain,
% 116.87/116.86 (~P2(f6(a1),f6(a1),a4)),
% 116.87/116.86 inference(scs_inference,[],[10987,10980,11119,11136,11102,10322,11054,10897,10320,9788,9912,9847,10092,3816,26,28,30,29,23,8867,9446])).
% 116.87/116.86 cnf(11166,plain,
% 116.87/116.86 (~P2(f8(a4),f7(a1,a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[11150,11128,10970,10834,9776,4125,26])).
% 116.87/116.86 cnf(11168,plain,
% 116.87/116.86 (P3(f8(a4),f7(a4,a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11150,11156,11128,10970,10834,10356,9776,4125,26,28])).
% 116.87/116.86 cnf(11170,plain,
% 116.87/116.86 (P3(f7(a4,a4),f8(a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11150,11156,11128,10970,10834,10356,10349,9776,4125,26,28,27])).
% 116.87/116.86 cnf(11174,plain,
% 116.87/116.86 (~P2(a2,f3(a1,a1),a5)),
% 116.87/116.86 inference(scs_inference,[],[7,11150,11156,11128,10970,11119,11086,10834,10991,10356,10028,10349,9930,9776,4125,26,28,27,29,30])).
% 116.87/116.86 cnf(11177,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f7(a1,a1),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[10954,10793,11070,26])).
% 116.87/116.86 cnf(11179,plain,
% 116.87/116.86 (P3(a1,f7(a4,a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[11168,10954,10793,11070,10402,26,28])).
% 116.87/116.86 cnf(11181,plain,
% 116.87/116.86 (P3(f7(a4,a4),f7(a4,a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11168,11170,10954,10142,10793,11070,10464,10402,26,28,27])).
% 116.87/116.86 cnf(11187,plain,
% 116.87/116.86 (P3(f7(a4,a4),a1,a1)),
% 116.87/116.86 inference(scs_inference,[],[10596,11168,11170,10954,10158,10142,10793,11150,11070,9869,10566,10464,10509,10390,10402,26,28,27,30,29,23])).
% 116.87/116.86 cnf(11193,plain,
% 116.87/116.86 (~P2(f6(a1),f6(a1),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11139,10903,10828,26])).
% 116.87/116.86 cnf(11195,plain,
% 116.87/116.86 (P2(f6(a4),a4,f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11139,11136,10903,10675,10828,10444,26,25])).
% 116.87/116.86 cnf(11197,plain,
% 116.87/116.86 (P3(f7(a4,a4),a4,f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11139,11181,11136,10142,10903,10675,10828,10444,9926,26,25,28])).
% 116.87/116.86 cnf(11199,plain,
% 116.87/116.86 (P3(a4,f7(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[11139,11181,11136,11102,10142,10903,10675,10828,10444,9859,9926,26,25,28,27])).
% 116.87/116.86 cnf(11201,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f6(a1),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11139,11181,11015,11136,11102,10142,10903,10675,10828,10444,9859,9847,9926,3816,26,25,28,27,30])).
% 116.87/116.86 cnf(11203,plain,
% 116.87/116.86 (~P3(f7(a4,a4),f7(a4,a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[11139,11181,11015,11166,11136,11102,10418,10142,10903,10675,10828,10026,10444,9859,9847,9926,3816,26,25,28,27,30,29])).
% 116.87/116.86 cnf(11207,plain,
% 116.87/116.86 (P3(a4,f7(a4,a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11139,11181,11015,11166,11136,11102,10418,10142,10903,10675,10828,10026,10444,9859,9847,9926,3816,26,25,28,27,30,29,4988,23])).
% 116.87/116.86 cnf(11209,plain,
% 116.87/116.86 (P2(a4,f6(a4),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11139,11181,11015,11166,11136,11102,10418,10142,10903,10675,10828,10026,10444,9859,9847,9926,3816,26,25,28,27,30,29,4988,23,22])).
% 116.87/116.86 cnf(11217,plain,
% 116.87/116.86 (~P3(a1,f7(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[11139,11181,11015,11166,11136,11102,10418,10142,10903,10134,10675,10828,10026,10444,9859,9847,9926,9792,3816,26,25,28,27,30,29,4988,23,22,3632,9445,8867,9204])).
% 116.87/116.86 cnf(11219,plain,
% 116.87/116.86 (P3(f7(a4,a4),a4,a4)),
% 116.87/116.86 inference(scs_inference,[],[11199,23])).
% 116.87/116.86 cnf(11221,plain,
% 116.87/116.86 (~P2(a4,f7(a1,a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[11195,11209,11199,10623,23,26])).
% 116.87/116.86 cnf(11223,plain,
% 116.87/116.86 (P3(f8(a2),f7(a4,a4),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11195,11209,11199,10623,10331,23,26,28])).
% 116.87/116.86 cnf(11225,plain,
% 116.87/116.86 (~P3(f6(a4),f7(a4,a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[10978,11195,11209,11199,10623,9973,10331,10026,23,26,28,29])).
% 116.87/116.86 cnf(11229,plain,
% 116.87/116.86 (P2(a1,f7(a1,a1),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10978,11195,11209,11199,10623,11128,11181,9973,9805,10791,10331,10026,23,26,28,29,21,25])).
% 116.87/116.86 cnf(11236,plain,
% 116.87/116.86 (P3(f7(a4,a4),f8(a2),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11223,23])).
% 116.87/116.86 cnf(11238,plain,
% 116.87/116.86 (P2(f7(a1,a1),a1,f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11223,11229,23,22])).
% 116.87/116.86 cnf(11240,plain,
% 116.87/116.86 (~P2(a4,f7(a1,a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11113,11223,11229,11209,9922,23,22,26])).
% 116.87/116.86 cnf(11242,plain,
% 116.87/116.86 (P2(a2,f6(a2),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11113,11223,11229,11209,10633,10509,9922,23,22,26,25])).
% 116.87/116.86 cnf(11244,plain,
% 116.87/116.86 (P3(f7(a4,a4),a5,a5)),
% 116.87/116.86 inference(scs_inference,[],[11219,11113,11223,11229,11209,10633,10509,10110,9922,23,22,26,25,27])).
% 116.87/116.86 cnf(11246,plain,
% 116.87/116.86 (~P3(f6(a1),a1,f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11219,11113,11177,11223,11229,11209,11119,10633,10509,10028,10110,9922,23,22,26,25,27,29])).
% 116.87/116.86 cnf(11248,plain,
% 116.87/116.86 (P3(f8(a2),f8(a4),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11219,11113,11177,11223,11229,11209,10076,11119,10633,10509,10028,10110,9922,23,22,26,25,27,29,28])).
% 116.87/116.86 cnf(11254,plain,
% 116.87/116.86 (P3(f8(a4),f8(a2),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11248,23])).
% 116.87/116.86 cnf(11256,plain,
% 116.87/116.86 (P2(f6(a2),a2,f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11242,11248,23,22])).
% 116.87/116.86 cnf(11260,plain,
% 116.87/116.86 (P3(a5,f7(a4,a4),a5)),
% 116.87/116.86 inference(scs_inference,[],[11130,11242,11248,11199,10942,10795,10102,23,22,26,28])).
% 116.87/116.86 cnf(11262,plain,
% 116.87/116.86 (P3(a4,a4,f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11130,11242,11248,11207,11219,11199,10942,10795,10245,10102,23,22,26,28,27])).
% 116.87/116.86 cnf(11264,plain,
% 116.87/116.86 (~P2(a1,a2,a5)),
% 116.87/116.86 inference(scs_inference,[],[7,11130,11242,11248,11207,11179,11219,11199,11156,10942,10795,10245,10102,9774,23,22,26,28,27,30])).
% 116.87/116.86 cnf(11269,plain,
% 116.87/116.86 (~P2(a1,a1,f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[7,11130,11236,11242,11248,11207,11179,11219,11199,11156,10942,10795,10245,10960,10102,10297,9774,23,22,26,28,27,30,29,1134])).
% 116.87/116.86 cnf(11277,plain,
% 116.87/116.86 (P2(f6(a1),f6(a1),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10362,11256,11238,11242,10883,11039,26,25])).
% 116.87/116.86 cnf(11279,plain,
% 116.87/116.86 (P3(f8(a4),a5,a5)),
% 116.87/116.86 inference(scs_inference,[],[10362,11256,11244,11238,11207,11242,10883,11039,10110,26,25,28])).
% 116.87/116.86 cnf(11284,plain,
% 116.87/116.86 (P3(x112841,x112842,x112843)+~P2(x112844,x112845,x112841)+~P3(x112845,x112842,x112846)+~P3(x112844,x112842,x112847)+~P2(x112847,x112846,x112843)),
% 116.87/116.86 inference(rename_variables,[],[30])).
% 116.87/116.86 cnf(11287,plain,
% 116.87/116.86 (P3(a5,f8(a4),a5)),
% 116.87/116.86 inference(scs_inference,[],[10362,11134,10164,11254,11256,11244,11238,11207,11242,10883,10871,10130,11039,10960,10551,10098,9959,10110,26,25,28,27,30,29,23])).
% 116.87/116.86 cnf(11289,plain,
% 116.87/116.86 (~P2(x112891,a2,a5)+~P3(f6(a1),f7(a4,a4),x112891)),
% 116.87/116.86 inference(scs_inference,[],[7,10362,11134,10164,11254,11256,11244,11238,11207,11242,10883,11060,10871,10130,11156,11039,10960,10551,10098,9959,10110,26,25,28,27,30,29,23,11284])).
% 116.87/116.86 cnf(11298,plain,
% 116.87/116.86 (P3(f7(a4,a4),f6(a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[7,10167,11287,11256,11219,10318,10356,2846,26,28,27])).
% 116.87/116.86 cnf(11302,plain,
% 116.87/116.86 (~P3(f3(a1,a1),a4,f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[7,10167,11074,11277,11287,10799,11256,11238,11179,11219,10318,10356,10026,3816,2846,26,28,27,30,29])).
% 116.87/116.86 cnf(11304,plain,
% 116.87/116.86 (P3(f6(a4),f7(a4,a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[7,10167,11074,11277,11287,10799,11256,11238,11179,11219,10318,10356,10026,3816,2846,26,28,27,30,29,23])).
% 116.87/116.86 cnf(11312,plain,
% 116.87/116.86 (P3(f6(a1),f7(a4,a4),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[11264,11199,10318,10729,3816,26,28])).
% 116.87/116.86 cnf(11314,plain,
% 116.87/116.86 (P3(f6(a4),f8(a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11264,11304,11197,11199,10318,10729,3816,3810,26,28,27])).
% 116.87/116.86 cnf(11316,plain,
% 116.87/116.86 (P2(f6(a4),f8(a4),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11264,11304,11262,11197,11195,11199,10318,10729,9932,3816,3810,26,28,27,29])).
% 116.87/116.86 cnf(11318,plain,
% 116.87/116.86 (P3(f7(a4,a4),f6(a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[11264,11304,11262,11197,11195,11199,10318,10729,9932,3816,3810,26,28,27,29,23])).
% 116.87/116.86 cnf(11320,plain,
% 116.87/116.86 (P2(f8(a4),f6(a4),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11264,11304,11262,11197,11195,11199,10318,10729,9932,3816,3810,26,28,27,29,23,22])).
% 116.87/116.86 cnf(11325,plain,
% 116.87/116.86 (~P2(f6(a1),a2,a5)),
% 116.87/116.86 inference(scs_inference,[],[7,11264,11279,11304,11262,11197,11195,11199,10318,10729,9932,3816,3810,26,28,27,29,23,22,30,11289])).
% 116.87/116.86 cnf(11329,plain,
% 116.87/116.86 (P3(f8(a4),f6(a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11314,23])).
% 116.87/116.86 cnf(11333,plain,
% 116.87/116.86 (~P3(f8(a2),a5,x113331)),
% 116.87/116.86 inference(scs_inference,[],[7,11152,11314,11279,11277,10349,23,26,27])).
% 116.87/116.86 cnf(11340,plain,
% 116.87/116.86 (~P3(a4,f3(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[7,11298,11152,11314,11279,10759,11277,11080,10183,10349,9912,10297,23,26,27,29,30,4964])).
% 116.87/116.86 cnf(11354,plain,
% 116.87/116.86 (~P3(f6(a1),f8(a4),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11333,11316,11260,10915,11248,10580,10962,11219,10960,10098,33,1759,11017,26,28,27,29])).
% 116.87/116.86 cnf(11358,plain,
% 116.87/116.86 (~P3(a5,f7(a4,a4),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11340,11333,11316,11260,10915,11248,10580,10962,9950,11219,9875,10960,10098,10000,33,1759,11017,26,28,27,29,30,10923])).
% 116.87/116.86 cnf(11360,plain,
% 116.87/116.86 (P3(f6(a5),f7(a4,a4),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[11340,11333,11316,11260,10915,11248,10580,10962,9950,11219,9875,10960,10098,10000,33,1759,11017,26,28,27,29,30,10923,23])).
% 116.87/116.86 cnf(11367,plain,
% 116.87/116.86 (P3(f6(a5),f8(a4),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[11325,11360,11197,11048,9863,3804,26,27])).
% 116.87/116.86 cnf(11371,plain,
% 116.87/116.86 (~P2(f7(a4,a4),f6(a4),a2)),
% 116.87/116.86 inference(scs_inference,[],[11325,11240,11360,11320,10144,11197,11314,11048,11102,9863,9932,9827,3804,26,27,29,30])).
% 116.87/116.86 cnf(11378,plain,
% 116.87/116.86 (~P2(f6(a1),f3(a1,a1),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11201,11277,26])).
% 116.87/116.86 cnf(11380,plain,
% 116.87/116.86 (P3(f8(a4),f6(a1),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[11201,11318,11277,9977,26,27])).
% 116.87/116.86 cnf(11382,plain,
% 116.87/116.86 (~P3(f7(a1,a1),f7(a4,a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11201,11318,9841,11168,11304,11320,11277,9977,26,27,29])).
% 116.87/116.86 cnf(11384,plain,
% 116.87/116.86 (P3(f6(a1),f8(a4),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[11201,11318,9841,11168,11304,11320,11277,9977,26,27,29,23])).
% 116.87/116.86 cnf(11388,plain,
% 116.87/116.86 (P2(f6(a4),f8(a4),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11201,11318,9841,11168,11316,11304,11262,11320,11238,11277,9977,10112,26,27,29,23,21,25])).
% 116.87/116.86 cnf(11390,plain,
% 116.87/116.86 (P2(f8(a4),f6(a4),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11201,11318,9841,11168,11316,11304,11262,11320,11238,11277,9977,10112,26,27,29,23,21,25,22])).
% 116.87/116.86 cnf(11396,plain,
% 116.87/116.86 (P2(a4,f3(a1,a1),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11388,10466,11316,11209,10808,10594,26,25])).
% 116.87/116.86 cnf(11400,plain,
% 116.87/116.86 (P2(f3(a1,a1),a4,f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11160,11388,11380,10466,11316,11209,10808,10737,10594,26,25,29,22])).
% 116.87/116.86 cnf(11407,plain,
% 116.87/116.86 (~P3(f7(a1,a1),f8(a4),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11269,11248,10744,10883,10791,10960,26,29])).
% 116.87/116.86 cnf(11413,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f8(a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[11400,11396,10970,26])).
% 116.87/116.86 cnf(11419,plain,
% 116.87/116.86 (~P2(f6(a5),a5,f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11407,11371,10523,11390,11400,11396,11367,11287,10970,11242,11304,9977,11070,26,25,29,30])).
% 116.87/116.86 cnf(11423,plain,
% 116.87/116.86 (~P3(f3(a1,a1),f3(a4,a4),x114231)+P3(a1,x114231,f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11407,11371,10523,11390,11400,11396,11367,11287,10970,11242,11304,9977,11070,10304,9969,26,25,29,30,3798,27])).
% 116.87/116.86 cnf(11429,plain,
% 116.87/116.86 (~P2(f7(a1,a1),a5,f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10358,11358,11390,11396,11260,9841,11168,11304,10761,9904,10026,26,29,30])).
% 116.87/116.86 cnf(11435,plain,
% 116.87/116.86 (~P2(a5,f6(a5),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11174,11382,11187,11269,11360,11078,11260,11086,11119,10297,26,29,30])).
% 116.87/116.86 cnf(11437,plain,
% 116.87/116.86 (~P2(f6(a4),f3(a1,a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10987,11388,11390,26])).
% 116.87/116.86 cnf(11439,plain,
% 116.87/116.86 (~P3(f7(a1,a1),f8(a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11435,10987,11388,11390,11287,11078,11367,26,29])).
% 116.87/116.86 cnf(11448,plain,
% 116.87/116.86 (~P2(f6(a4),f7(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[10268,11413,10843,11388,11277,10476,3810,26,30])).
% 116.87/116.86 cnf(11450,plain,
% 116.87/116.86 (P3(f8(a4),f8(a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[10268,11413,11170,10843,11388,11207,11277,10476,9859,3810,26,30,28])).
% 116.87/116.86 cnf(11458,plain,
% 116.87/116.86 (P2(a4,f7(a1,a1),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11104,11396,11256,10834,11136,9869,26,25])).
% 116.87/116.86 cnf(11460,plain,
% 116.87/116.86 (~P3(f8(a4),f7(a4,a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[11104,11396,11256,10834,10970,11207,11136,9869,9930,26,25,29])).
% 116.87/116.86 cnf(11462,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f6(a1),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11104,11439,11396,11384,11256,11030,10834,10970,11207,11136,9869,10004,9930,26,25,29,30])).
% 116.87/116.86 cnf(11464,plain,
% 116.87/116.86 (P2(f7(a1,a1),a4,f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11104,11439,11396,11384,11256,11030,10834,10970,11207,11136,9869,10004,9930,26,25,29,30,22])).
% 116.87/116.86 cnf(11471,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f8(a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[11458,11464,11166,26])).
% 116.87/116.86 cnf(11473,plain,
% 116.87/116.86 (P3(f7(a4,a4),f8(a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[11458,11464,11166,11450,11197,10066,26,27])).
% 116.87/116.86 cnf(11477,plain,
% 116.87/116.86 (~P2(f6(a1),f6(a1),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11193,11354,11458,11464,11166,11450,11380,11197,10665,11384,10066,10737,26,27,29,30])).
% 116.87/116.86 cnf(11479,plain,
% 116.87/116.86 (P3(f8(a4),f7(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[11193,11354,11458,11464,11166,11450,11380,11197,10665,11384,10066,10737,26,27,29,30,23])).
% 116.87/116.86 cnf(11483,plain,
% 116.87/116.86 (P3(f7(a4,a4),f7(a4,a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[11056,11479,11458,11197,9973,10645,26,27])).
% 116.87/116.86 cnf(11485,plain,
% 116.87/116.86 (~P3(f7(a4,a4),f8(a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[11056,11479,10919,11473,11458,10354,11197,9973,10645,9912,26,27,29])).
% 116.87/116.86 cnf(11487,plain,
% 116.87/116.86 (~P2(f8(a4),f6(a4),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[11056,11123,11479,10919,11473,11458,10354,11262,11197,9973,10645,10637,9912,3810,26,27,29,30])).
% 116.87/116.86 cnf(11492,plain,
% 116.87/116.86 (~P2(f6(a1),a5,f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11429,11024,10761,26])).
% 116.87/116.86 cnf(11498,plain,
% 116.87/116.86 (P2(f8(a4),a4,f3(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[11464,10817,10737,26])).
% 116.87/116.86 cnf(11502,plain,
% 116.87/116.86 (~P2(a4,f6(a4),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10752,10667,11464,11458,11450,10817,11320,11314,9950,10737,9969,26,29,30])).
% 116.87/116.86 cnf(11504,plain,
% 116.87/116.86 (P2(a4,f8(a4),f3(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[10752,10667,11464,11458,11450,10817,11320,11314,9950,10737,9969,26,29,30,22])).
% 116.87/116.86 cnf(11510,plain,
% 116.87/116.86 (P2(f6(a4),f3(a4,a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11132,11498,11464,11229,11316,10621,26,25])).
% 116.87/116.86 cnf(11514,plain,
% 116.87/116.86 (P2(f3(a4,a4),f6(a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11132,11477,11498,11464,11318,11229,11316,10621,10297,26,25,29,22])).
% 116.87/116.86 cnf(11522,plain,
% 116.87/116.86 (~P3(a4,f7(a4,a4),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10701,11498,11479,9992,11119,10547,26,29])).
% 116.87/116.86 cnf(11524,plain,
% 116.87/116.86 (~P2(f7(a4,a4),a1,a1)),
% 116.87/116.86 inference(scs_inference,[],[10701,11485,11498,11479,9983,10076,9992,11119,10547,10402,26,29,30])).
% 116.87/116.86 cnf(11529,plain,
% 116.87/116.86 (~P2(f6(a4),f8(a4),f7(a4,a4))),
% 116.87/116.86 inference(scs_inference,[],[11487,11510,11514,26])).
% 116.87/116.86 cnf(11537,plain,
% 116.87/116.86 (~P2(a1,f7(a1,a1),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11435,11078,9825,26])).
% 116.87/116.86 cnf(11541,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f6(a2),a1)),
% 116.87/116.86 inference(scs_inference,[],[10863,11435,11312,10306,10247,10482,11078,9825,9930,26,29,30])).
% 116.87/116.86 cnf(11558,plain,
% 116.87/116.86 (~P3(f6(a1),f7(a4,a4),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[10819,11510,10580,11223,11209,10960,26,29])).
% 116.87/116.86 cnf(11563,plain,
% 116.87/116.86 (~P2(f6(a4),f6(a5),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[10954,2481,11209,25])).
% 116.87/116.86 cnf(11580,plain,
% 116.87/116.86 (~P2(f6(a1),f8(a4),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10623,11400,11128,26])).
% 116.87/116.86 cnf(11584,plain,
% 116.87/116.86 (~P2(f8(a4),f6(a4),a4)),
% 116.87/116.86 inference(scs_inference,[],[11217,10410,10623,11400,11179,11128,11207,11304,10594,9770,26,29,30])).
% 116.87/116.86 cnf(11591,plain,
% 116.87/116.86 (~P2(f6(a4),f8(a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11462,10834,11316,26])).
% 116.87/116.86 cnf(11593,plain,
% 116.87/116.86 (~P3(f3(a1,a1),f8(a4),f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11462,10600,11248,10834,11316,10960,26,29])).
% 116.87/116.86 cnf(11605,plain,
% 116.87/116.86 (~P2(f6(a2),f6(a5),f6(a5))),
% 116.87/116.86 inference(scs_inference,[],[10989,11242,1927,25])).
% 116.87/116.86 cnf(11611,plain,
% 116.87/116.86 (~P2(a1,a1,f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[9898,10909,11593,10989,10229,10295,11242,10253,10183,10402,9770,1927,25,26,29,30])).
% 116.87/116.86 cnf(11633,plain,
% 116.87/116.86 (~P3(f3(a4,a4),f8(a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11584,10236,11514,9764,11450,10804,11314,26,29])).
% 116.87/116.86 cnf(11635,plain,
% 116.87/116.86 (~P2(f6(a4),f7(a1,a1),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11584,10236,10437,11514,9764,11450,10930,10804,11314,10004,26,29,30])).
% 116.87/116.86 cnf(11637,plain,
% 116.87/116.86 (~P2(f6(a4),f3(a4,a4),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11121,10333,10000,26])).
% 116.87/116.86 cnf(11641,plain,
% 116.87/116.86 (~P2(a4,a4,f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11121,11537,11633,11473,11229,10333,10000,9932,10297,9792,26,29,30])).
% 116.87/116.86 cnf(11649,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f6(a4),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11635,11419,10613,10917,10930,10204,25,26])).
% 116.87/116.86 cnf(11651,plain,
% 116.87/116.86 (~P3(f3(a4,a4),f7(a4,a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11635,11419,11641,11479,10613,10917,10930,10204,10737,25,26,29])).
% 116.87/116.86 cnf(11653,plain,
% 116.87/116.86 (~P2(f7(a4,a4),f7(a1,a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[11460,11635,11419,11641,11479,10613,10917,11458,10930,9973,10204,10737,10026,25,26,29,30])).
% 116.87/116.86 cnf(11658,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f7(a4,a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[11653,10418,10341,26])).
% 116.87/116.86 cnf(11666,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f8(a4),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11637,11510,10917,26])).
% 116.87/116.86 cnf(11682,plain,
% 116.87/116.86 (~P2(f6(a4),f3(a4,a4),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[10549,11498,11388,26])).
% 116.87/116.86 cnf(11695,plain,
% 116.87/116.86 (~P3(f3(a1,a1),f8(a4),f6(a4))),
% 116.87/116.86 inference(scs_inference,[],[11203,11502,11492,10050,11473,10354,10076,11054,11048,9930,26,30,29])).
% 116.87/116.86 cnf(11697,plain,
% 116.87/116.86 (~P2(f6(a4),f6(a4),x116971)+P2(f3(a4,a4),x116971,f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11203,11502,11492,10050,11514,11473,10354,10076,11054,11390,11048,9930,26,30,29,25])).
% 116.87/116.86 cnf(11700,plain,
% 116.87/116.86 (P2(f6(a2),a2,f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[11086,11256,11119,25])).
% 116.87/116.86 cnf(11702,plain,
% 116.87/116.86 (~P2(f6(a4),f6(a1),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11437,10795,11086,11256,11119,25,26])).
% 116.87/116.86 cnf(11704,plain,
% 116.87/116.86 (~P2(f3(a4,a4),f7(a1,a1),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11437,11633,10795,11086,10433,11256,9981,11119,10004,25,26,30])).
% 116.87/116.86 cnf(11706,plain,
% 116.87/116.86 (P2(a2,f6(a2),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[11437,11633,10795,11086,10433,11256,9981,11119,10004,25,26,30,22])).
% 116.87/116.86 cnf(11711,plain,
% 116.87/116.86 (~P2(a2,f6(a1),a1)),
% 116.87/116.86 inference(scs_inference,[],[10905,11700,11706,26])).
% 116.87/116.86 cnf(11718,plain,
% 116.87/116.86 (P2(a2,f6(a2),f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11706,11128,10229,25])).
% 116.87/116.86 cnf(11720,plain,
% 116.87/116.86 (~P2(a4,f8(a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11704,11706,11504,11128,10817,10229,25,26])).
% 116.87/116.86 cnf(11726,plain,
% 116.87/116.86 (P2(f6(a2),a2,f7(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11695,11704,11706,11236,11504,11128,10817,10158,10229,10253,11256,10183,10960,25,26,30,29,22])).
% 116.87/116.86 cnf(11732,plain,
% 116.87/116.86 (~P2(f8(a4),f7(a1,a1),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11471,11522,11718,11207,10562,10509,10026,26,30])).
% 116.87/116.86 cnf(11745,plain,
% 116.87/116.86 (~P3(f3(a2,a2),f8(a4),a2)),
% 116.87/116.86 inference(scs_inference,[],[10806,11726,10905,11439,11706,10258,10982,10132,11384,9912,10004,26,30,29])).
% 116.87/116.86 cnf(11750,plain,
% 116.87/116.86 (~P2(a5,f6(a5),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11732,10962,10219,26])).
% 116.87/116.86 cnf(11764,plain,
% 116.87/116.86 (~P2(a2,f7(a1,a1),a5)),
% 116.87/116.86 inference(scs_inference,[],[11325,11726,11706,26])).
% 116.87/116.86 cnf(11771,plain,
% 116.87/116.86 (~P2(f3(a1,a1),f8(a4),f6(a1))),
% 116.87/116.86 inference(scs_inference,[],[11682,11510,10804,26])).
% 116.87/116.86 cnf(11773,plain,
% 116.87/116.86 (~P2(f6(a2),a2,f8(a2))),
% 116.87/116.86 inference(scs_inference,[],[11682,11558,11700,11510,10804,11156,10482,26,30])).
% 116.87/116.86 cnf(11779,plain,
% 116.87/116.86 (~P2(f6(a1),f7(a1,a1),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11750,11078,9883,26])).
% 116.87/116.86 cnf(11781,plain,
% 116.87/116.86 (~P2(f3(a2,a2),f3(a1,a1),a2)),
% 116.87/116.86 inference(scs_inference,[],[11750,11745,10533,11078,10132,9883,9912,26,30])).
% 116.87/116.86 cnf(11787,plain,
% 116.87/116.86 (P2(f6(a1),f7(a1,a1),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[10968,10883,11277,25])).
% 116.87/116.86 cnf(11791,plain,
% 116.87/116.86 (~P3(f6(a1),f7(a4,a4),f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11720,11702,11483,11181,10968,9764,10883,11277,10158,25,26,29])).
% 116.87/116.86 cnf(11793,plain,
% 116.87/116.86 (P2(f7(a1,a1),f6(a1),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11720,11702,11483,11181,10968,9764,10883,11277,10158,25,26,29,22])).
% 116.87/116.86 cnf(11798,plain,
% 116.87/116.86 (~P2(f7(a1,a1),f7(a4,a4),a1)),
% 116.87/116.86 inference(scs_inference,[],[11658,11793,10140,26])).
% 116.87/116.86 cnf(11806,plain,
% 116.87/116.86 (P2(f7(a1,a1),f7(a1,a1),f3(a1,a1))),
% 116.87/116.86 inference(scs_inference,[],[11787,10976,10932,25])).
% 116.87/116.86 cnf(11812,plain,
% 116.87/116.86 (~P3(f3(a1,a1),a4,f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[10649,11225,11779,11787,11718,10976,10932,10795,11304,10509,9932,9930,3816,25,26,30,29])).
% 116.87/116.86 cnf(11816,plain,
% 116.87/116.86 (~P2(f3(a4,a4),a1,f8(a4))),
% 116.87/116.86 inference(scs_inference,[],[11651,10823,11700,10130,11706,9992,11179,26,30])).
% 116.87/116.86 cnf(11822,plain,
% 116.87/116.86 (~P2(f3(a5,a5),f6(a5),f3(a2,a2))),
% 116.87/116.87 inference(scs_inference,[],[10582,11013,10995,10088,10304,10028,28,26])).
% 116.87/116.87 cnf(11824,plain,
% 116.87/116.87 (~P2(f7(a1,a1),f7(a1,a1),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11806,10582,11812,11013,10995,10088,10304,10028,9932,28,26,30])).
% 116.87/116.87 cnf(11828,plain,
% 116.87/116.87 (~P2(f6(a1),a5,f3(a2,a2))),
% 116.87/116.87 inference(scs_inference,[],[11046,10997,10072,26])).
% 116.87/116.87 cnf(11830,plain,
% 116.87/116.87 (~P2(f7(a4,a4),f6(a4),f7(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[11046,11302,10997,10476,11390,10072,3810,26,30])).
% 116.87/116.87 cnf(11832,plain,
% 116.87/116.87 (~P3(f3(a1,a1),f8(a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11046,11824,11302,11806,10997,10476,11390,10072,10004,3810,26,30,29])).
% 116.87/116.87 cnf(11836,plain,
% 116.87/116.87 (~P2(f7(a1,a1),f6(a1),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11832,11793,11653,9967,11384,10418,10004,26,30])).
% 116.87/116.87 cnf(11838,plain,
% 116.87/116.87 (~P3(f3(a1,a1),f3(a4,a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11832,11824,11793,11806,11653,9967,11384,10418,9969,10004,26,30,29])).
% 116.87/116.87 cnf(11843,plain,
% 116.87/116.87 (~P2(f6(a1),f7(a4,a4),a1)),
% 116.87/116.87 inference(scs_inference,[],[11798,11128,10341,26])).
% 116.87/116.87 cnf(11845,plain,
% 116.87/116.87 (~P2(f3(a4,a4),f3(a1,a1),a4)),
% 116.87/116.87 inference(scs_inference,[],[11798,10625,10162,11128,10341,10274,9847,26,30])).
% 116.87/116.87 cnf(11851,plain,
% 116.87/116.87 (P2(a1,f3(a1,a1),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[11793,10665,10828,25])).
% 116.87/116.87 cnf(11857,plain,
% 116.87/116.87 (P2(f3(a1,a1),a1,f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[10832,11781,11793,11514,10617,10665,10671,10828,10320,25,26,29,22])).
% 116.87/116.87 cnf(11862,plain,
% 116.87/116.87 (~P2(f8(a4),f6(a1),a1)),
% 116.87/116.87 inference(scs_inference,[],[11857,10424,10871,26])).
% 116.87/116.87 cnf(11864,plain,
% 116.87/116.87 (~P3(f6(a1),f8(a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[10446,11851,11857,10424,10871,10402,9912,26,29])).
% 116.87/116.87 cnf(11870,plain,
% 116.87/116.87 (P2(f6(a4),f8(a4),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[11857,11388,10112,25])).
% 116.87/116.87 cnf(11874,plain,
% 116.87/116.87 (~P2(f6(a5),a5,f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11828,11864,11857,11367,11287,11054,11388,11048,10112,25,26,30])).
% 116.87/116.87 cnf(11876,plain,
% 116.87/116.87 (~P3(f7(a1,a1),f7(a4,a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11836,11828,11864,11857,11030,11367,11287,11054,11388,11312,11048,10112,10026,25,26,30,29])).
% 116.87/116.87 cnf(11878,plain,
% 116.87/116.87 (P2(f8(a4),f6(a4),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[11836,11828,11864,11857,11030,11367,11287,11054,11388,11312,11048,10112,10026,25,26,30,29,22])).
% 116.87/116.87 cnf(11886,plain,
% 116.87/116.87 (~P3(f3(a1,a1),f7(a4,a4),f8(a2))),
% 116.87/116.87 inference(scs_inference,[],[11649,11246,11870,11611,11718,9764,11242,11179,9839,9770,26,30,29])).
% 116.87/116.87 cnf(11892,plain,
% 116.87/116.87 (~P3(f6(a1),f7(a4,a4),f7(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[11878,11001,11830,11580,11870,11857,9977,11179,11304,9930,26,30,29])).
% 116.87/116.87 cnf(11898,plain,
% 116.87/116.87 (~P2(f3(a1,a1),f7(a1,a1),f7(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[11529,11316,10804,26])).
% 116.87/116.87 cnf(11909,plain,
% 116.87/116.87 (~P3(f3(a2,a2),a4,a2)),
% 116.87/116.87 inference(scs_inference,[],[10946,11838,10735,11870,10711,10002,11514,11195,10266,11390,9932,26,30,29])).
% 116.87/116.87 cnf(11911,plain,
% 116.87/116.87 (P2(a1,f3(a1,a1),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[10946,11838,10735,11851,11870,10711,10198,10002,11514,11195,10266,11039,11390,9932,26,30,29,25])).
% 116.87/116.87 cnf(11913,plain,
% 116.87/116.87 (P2(f3(a1,a1),a1,f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[11911,22])).
% 116.87/116.87 cnf(11915,plain,
% 116.87/116.87 (~P2(f3(a1,a1),f7(a1,a1),f8(a2))),
% 116.87/116.87 inference(scs_inference,[],[11911,11378,11857,22,26])).
% 116.87/116.87 cnf(11917,plain,
% 116.87/116.87 (~P2(f3(a2,a2),a1,a2)),
% 116.87/116.87 inference(scs_inference,[],[11909,11911,11378,9971,11857,10266,9792,22,26,30])).
% 116.87/116.87 cnf(11925,plain,
% 116.87/116.87 (P2(a4,f6(a1),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11878,11504,11514,25])).
% 116.87/116.87 cnf(11929,plain,
% 116.87/116.87 (~P2(f3(a1,a1),f6(a1),f6(a2))),
% 116.87/116.87 inference(scs_inference,[],[11898,10936,11878,11504,11136,10633,11514,11384,11242,9912,25,26,30])).
% 116.87/116.87 cnf(11933,plain,
% 116.87/116.87 (P2(f6(a1),a4,f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11898,10936,11878,11504,10744,11136,10633,11514,11223,11384,11242,10960,9912,25,26,30,29,22])).
% 116.87/116.87 cnf(11937,plain,
% 116.87/116.87 (~P2(f3(a1,a1),f8(a4),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[11666,11913,10060,26])).
% 116.87/116.87 cnf(11939,plain,
% 116.87/116.87 (~P3(f6(a1),f6(a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11591,11666,11925,11913,11329,10060,2846,26,29])).
% 116.87/116.87 cnf(11951,plain,
% 116.87/116.87 (P2(f7(a4,a4),f6(a1),a4)),
% 116.87/116.87 inference(scs_inference,[],[11915,11939,11874,11933,11925,11806,11479,11878,11329,11510,9973,11312,11054,26,25,30,29])).
% 116.87/116.87 cnf(11953,plain,
% 116.87/116.87 (P2(f6(a1),f7(a4,a4),a4)),
% 116.87/116.87 inference(scs_inference,[],[11915,11939,11874,11933,11925,11806,11479,11878,11329,11510,9973,11312,11054,26,25,30,29,22])).
% 116.87/116.87 cnf(11959,plain,
% 116.87/116.87 (~P2(f6(a1),f7(a1,a1),f8(a2))),
% 116.87/116.87 inference(scs_inference,[],[11711,11886,11951,11787,11312,9904,10026,26,30])).
% 116.87/116.87 cnf(11969,plain,
% 116.87/116.87 (~P2(f3(a1,a1),f3(a1,a1),f6(a2))),
% 116.87/116.87 inference(scs_inference,[],[11929,9833,10897,26])).
% 116.87/116.87 cnf(11976,plain,
% 116.87/116.87 (P2(f8(a4),f7(a4,a4),f3(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[11953,11925,9922,26])).
% 116.87/116.87 cnf(11980,plain,
% 116.87/116.87 (P2(f7(a4,a4),f8(a4),f3(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[11843,11953,11925,10050,11312,9922,26,29,22])).
% 116.87/116.87 cnf(11999,plain,
% 116.87/116.87 (~P3(f3(a4,a4),f3(a1,a1),f6(a2))),
% 116.87/116.87 inference(scs_inference,[],[11959,11969,10692,11851,10976,10333,9981,9811,11384,9922,26,30,29])).
% 116.87/116.87 cnf(12005,plain,
% 116.87/116.87 (~P2(f7(a4,a4),f8(a4),a4)),
% 116.87/116.87 inference(scs_inference,[],[10772,11933,11951,26])).
% 116.87/116.87 cnf(12017,plain,
% 116.87/116.87 (~P3(f7(a1,a1),f8(a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[10553,10972,11750,11980,11262,11878,11078,11287,11367,10637,3810,26,30,29])).
% 116.87/116.87 cnf(12021,plain,
% 116.87/116.87 (~P2(f3(a1,a1),a1,f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11876,11771,11913,11806,10808,11179,9930,26,30])).
% 116.87/116.87 cnf(12028,plain,
% 116.87/116.87 (~P2(f7(a1,a1),f3(a4,a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11704,10422,10433,26])).
% 116.87/116.87 cnf(12032,plain,
% 116.87/116.87 (~P3(a5,f8(a4),f3(a2,a2))),
% 116.87/116.87 inference(scs_inference,[],[11141,11046,11704,10422,10062,11238,10433,10893,11367,10072,10304,26,30,29])).
% 116.87/116.87 cnf(12039,plain,
% 116.87/116.87 (~P3(f8(a4),f7(a1,a1),a2)),
% 116.87/116.87 inference(scs_inference,[],[10716,12028,11980,11911,10177,10038,9959,26,29])).
% 116.87/116.87 cnf(12047,plain,
% 116.87/116.87 (P2(f7(a4,a4),f3(a1,a1),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11845,11976,11925,11951,11277,10354,26,25])).
% 116.87/116.87 cnf(12053,plain,
% 116.87/116.87 (P2(f3(a1,a1),f7(a4,a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[12017,11845,11816,11976,11925,10360,11951,10130,11277,10354,10274,11320,11314,9792,26,25,30,29,22])).
% 116.87/116.87 cnf(12055,plain,
% 116.87/116.87 (~P2(f3(a1,a1),f3(a4,a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[12028,11913,9944,26])).
% 116.87/116.87 cnf(12061,plain,
% 116.87/116.87 (~P2(f6(a1),f3(a4,a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[12055,11787,10422,26])).
% 116.87/116.87 cnf(12070,plain,
% 116.87/116.87 (~P2(f8(a4),f3(a4,a4),f3(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[12061,11870,11510,26])).
% 116.87/116.87 cnf(12082,plain,
% 116.87/116.87 (~P2(a5,f7(a1,a1),f3(a2,a2))),
% 116.87/116.87 inference(scs_inference,[],[11937,12032,11870,10684,10773,11287,10004,26,30])).
% 116.87/116.87 cnf(12084,plain,
% 116.87/116.87 (P2(f7(a4,a4),a4,f3(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[11937,12032,11976,11473,11870,10684,10773,11102,11287,9981,10004,26,30,29])).
% 116.87/116.87 cnf(12086,plain,
% 116.87/116.87 (P2(a4,f7(a4,a4),f3(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[11937,12032,11976,11473,11870,10684,10773,11102,11287,9981,10004,26,30,29,22])).
% 116.87/116.87 cnf(12090,plain,
% 116.87/116.87 (~P2(f7(a4,a4),f3(a4,a4),f3(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[12070,12047,10177,26])).
% 116.87/116.87 cnf(12092,plain,
% 116.87/116.87 (P2(a1,f7(a4,a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[12070,12053,12047,11229,10177,10408,26,25])).
% 116.87/116.87 cnf(12096,plain,
% 116.87/116.87 (~P3(f7(a4,a4),f7(a4,a4),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[10778,11892,12070,12053,12047,10857,11229,10177,11483,9983,10408,11312,11179,9930,26,25,30,29])).
% 116.87/116.87 cnf(12098,plain,
% 116.87/116.87 (P2(f7(a4,a4),a1,f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[10778,11892,12070,12053,12047,10857,11229,10177,11483,9983,10408,11312,11179,9930,26,25,30,29,22])).
% 116.87/116.87 cnf(12100,plain,
% 116.87/116.87 (~P2(f7(a1,a1),a5,f3(a2,a2))),
% 116.87/116.87 inference(scs_inference,[],[12082,10761,10773,26])).
% 116.87/116.87 cnf(12102,plain,
% 116.87/116.87 (P3(f8(a4),f3(a1,a1),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12098,12082,10942,10761,9946,10773,10304,26,30])).
% 116.87/116.87 cnf(12104,plain,
% 116.87/116.87 (~P2(f6(a4),f7(a4,a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11448,12098,12082,10942,11450,10076,10761,9946,10773,11314,10304,26,30,29])).
% 116.87/116.87 cnf(12106,plain,
% 116.87/116.87 (P3(f3(a1,a1),f8(a4),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[11448,12098,12082,10942,11450,10076,10761,9946,10773,11314,10304,26,30,29,23])).
% 116.87/116.87 cnf(12108,plain,
% 116.87/116.87 (P3(a4,f3(a1,a1),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[11448,12098,12082,11380,10942,11450,10076,10761,9946,10773,11314,10304,26,30,29,23,28])).
% 116.87/116.87 cnf(12110,plain,
% 116.87/116.87 (P3(f3(a1,a1),a4,f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12108,23])).
% 116.87/116.87 cnf(12125,plain,
% 116.87/116.87 (~P2(f3(a4,a4),f7(a4,a4),f3(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[11822,12084,12086,12090,10219,9819,26,25])).
% 116.87/116.87 cnf(12127,plain,
% 116.87/116.87 (P3(f7(a4,a4),f3(a1,a1),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12102,11822,12084,12086,12090,11181,10219,9819,9946,26,25,27])).
% 116.87/116.87 cnf(12129,plain,
% 116.87/116.87 (~P3(f8(a4),f8(a4),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12102,10619,11822,12098,12084,12086,12090,11181,11473,10219,9819,9946,10402,26,25,27,29])).
% 116.87/116.87 cnf(12131,plain,
% 116.87/116.87 (P3(f3(a1,a1),f7(a4,a4),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12102,10619,11822,12098,12084,12086,12090,11181,11473,10219,9819,9946,10402,26,25,27,29,23])).
% 116.87/116.87 cnf(12138,plain,
% 116.87/116.87 (P2(f7(a1,a1),f7(a4,a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[12100,12053,11913,11806,9825,10408,26,25])).
% 116.87/116.87 cnf(12140,plain,
% 116.87/116.87 (~P2(f6(a1),f7(a4,a4),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12096,12131,12100,12053,11913,11806,10050,10341,9825,10408,26,25,30])).
% 116.87/116.87 cnf(12142,plain,
% 116.87/116.87 (~P3(f3(a1,a1),f7(a4,a4),f6(a2))),
% 116.87/116.87 inference(scs_inference,[],[12096,12131,12100,11605,12053,10989,11913,11806,10050,10341,11360,9825,10408,26,25,30,29])).
% 116.87/116.87 cnf(12144,plain,
% 116.87/116.87 (P2(f7(a4,a4),f7(a1,a1),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[12096,12131,12100,11605,12053,10989,11913,11806,10050,10341,11360,9825,10408,26,25,30,29,22])).
% 116.87/116.87 cnf(12146,plain,
% 116.87/116.87 (~P2(f7(a1,a1),f8(a4),f3(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12144,12138,11732,26])).
% 116.87/116.87 cnf(12148,plain,
% 116.87/116.87 (~P2(f6(a1),f6(a1),f6(a2))),
% 116.87/116.87 inference(scs_inference,[],[12127,12144,11999,12138,11732,12108,12084,26,30])).
% 116.87/116.87 cnf(12152,plain,
% 116.87/116.87 (~P2(f3(a4,a4),f8(a4),f3(a4,a4))),
% 116.87/116.87 inference(scs_inference,[],[12125,12092,10130,26])).
% 116.87/116.87 cnf(12160,plain,
% 116.87/116.87 (P2(f7(a4,a4),f6(a1),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[12140,12098,12053,11851,10871,26,25])).
% 116.87/116.87 cnf(12164,plain,
% 116.87/116.87 (P2(f6(a1),f7(a4,a4),f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[12140,12148,12098,12053,11976,11851,11318,11380,10871,26,25,29,22])).
% 116.87/116.87 cnf(12174,plain,
% 116.87/116.87 (~P2(a4,f6(a1),f3(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12146,11870,11209,26])).
% 116.87/116.87 cnf(12191,plain,
% 116.87/116.87 (~P2(f6(a1),a1,f8(a4))),
% 116.87/116.87 inference(scs_inference,[],[11524,11791,11046,12131,11857,10016,9863,10072,9801,11179,3804,26,29,30])).
% 116.87/116.87 cnf(12197,plain,
% 116.87/116.87 (P3(f8(a4),f3(a1,a1),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12152,12160,12086,12127,12098,11980,11024,9979,10002,10304,26,29,30])).
% 116.87/116.87 cnf(12199,plain,
% 116.87/116.87 (P3(f3(a1,a1),f8(a4),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12152,12160,12086,12127,12098,11980,11024,9979,10002,10304,26,29,30,23])).
% 116.87/116.87 cnf(12214,plain,
% 116.87/116.87 (P3(f6(a1),f8(a4),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12191,11108,12199,12102,10861,12098,11793,10360,9954,10402,9932,3816,26,29,30,28])).
% 116.87/116.87 cnf(12218,plain,
% 116.87/116.87 (P3(f8(a4),f6(a1),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12191,11108,12199,12197,12102,12106,12092,9928,10861,12098,11793,10360,9954,10402,9932,10004,3816,26,29,30,28,25,27])).
% 116.87/116.87 cnf(12222,plain,
% 116.87/116.87 (P3(f7(a1,a1),f7(a4,a4),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12104,12199,12110,12053,11479,10795,26,28])).
% 116.87/116.87 cnf(12224,plain,
% 116.87/116.87 (~P2(a5,f7(a4,a4),a5)),
% 116.87/116.87 inference(scs_inference,[],[12104,11874,12199,12110,12138,12053,11479,10795,11070,26,28,25])).
% 116.87/116.87 cnf(12226,plain,
% 116.87/116.87 (P3(f6(a1),f3(a4,a4),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12214,12104,11874,12199,12110,12138,12053,11479,10795,11070,10002,9969,26,28,25,27])).
% 116.87/116.87 cnf(12232,plain,
% 116.87/116.87 (P3(f7(a4,a4),f7(a1,a1),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[10635,12214,12104,12129,11874,12199,12110,12160,12138,12053,11170,11479,10885,10795,11070,10002,11156,9969,10026,26,28,25,27,29,30,23])).
% 116.87/116.87 cnf(12240,plain,
% 116.87/116.87 (P3(f3(a4,a4),f6(a1),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12226,23])).
% 116.87/116.87 cnf(12268,plain,
% 116.87/116.87 (~P3(f7(a1,a1),f6(a1),a2)),
% 116.87/116.87 inference(scs_inference,[],[11221,12039,12224,12218,12232,12164,12214,10843,11380,10092,11066,26,29,30,27])).
% 116.87/116.87 cnf(12274,plain,
% 116.87/116.87 (P3(f3(a4,a4),f6(a1),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12222,12240,11312,27])).
% 116.87/116.87 cnf(12276,plain,
% 116.87/116.87 (~P2(f6(a5),f3(a5,a5),a2)),
% 116.87/116.87 inference(scs_inference,[],[11764,12222,12240,10688,10072,11312,27,26])).
% 116.87/116.87 cnf(12278,plain,
% 116.87/116.87 (P3(f6(a1),f3(a4,a4),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[11764,12222,12240,12226,12232,10688,11318,10072,11312,27,26,28])).
% 116.87/116.87 cnf(12280,plain,
% 116.87/116.87 (~P2(f8(a4),f6(a5),f6(a5))),
% 116.87/116.87 inference(scs_inference,[],[11764,12222,12240,12226,12232,11563,10954,10688,11318,11316,10072,11312,27,26,28,25])).
% 116.87/116.87 cnf(12304,plain,
% 116.87/116.87 (~P3(a5,f8(a4),a2)),
% 116.87/116.87 inference(scs_inference,[],[12276,12280,10997,12160,10062,11367,10072,26,29])).
% 116.87/116.87 cnf(12323,plain,
% 116.87/116.87 (P3(f7(a1,a1),f3(a4,a4),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12278,12222,9979,27])).
% 116.87/116.87 cnf(12325,plain,
% 116.87/116.87 (P3(f3(a4,a4),f3(a1,a1),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12278,12222,12102,12274,9979,9981,27,28])).
% 116.87/116.87 cnf(12327,plain,
% 116.87/116.87 (~P2(a2,f8(a2),a2)),
% 116.87/116.87 inference(scs_inference,[],[11773,12278,12222,12102,12274,10733,11726,9979,9981,27,28,25])).
% 116.87/116.87 cnf(12333,plain,
% 116.87/116.87 (P3(f3(a4,a4),f7(a1,a1),f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12268,11773,11074,12278,12222,12102,12274,12218,10733,11976,11726,10885,11380,11318,11320,9979,9981,27,28,25,29,30,23])).
% 116.87/116.87 cnf(12349,plain,
% 116.87/116.87 (P3(a1,f6(a1),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[11541,12142,12323,12325,12021,9833,11787,11238,10179,9782,12131,10509,11179,9792,23,26,29,30,21,11423])).
% 116.87/116.87 cnf(12354,plain,
% 116.87/116.87 (P3(f6(a1),a1,f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12349,23])).
% 116.87/116.87 cnf(12369,plain,
% 116.87/116.87 (~P2(a2,a2,a2)),
% 116.87/116.87 inference(scs_inference,[],[11917,9869,9807,26])).
% 116.87/116.87 cnf(12377,plain,
% 116.87/116.87 (~P2(f3(a1,a1),f3(a2,a2),a2)),
% 116.87/116.87 inference(scs_inference,[],[12369,11080,9869,26])).
% 116.87/116.87 cnf(12392,plain,
% 116.87/116.87 (P3(f7(a1,a1),a1,f6(a1))),
% 116.87/116.87 inference(scs_inference,[],[12354,12333,12240,12222,11187,27,28])).
% 116.87/116.87 cnf(12398,plain,
% 116.87/116.87 (P3(a1,f7(a1,a1),f7(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12304,12354,12333,12276,12199,12240,12222,10310,10016,11287,11187,10072,3804,27,28,29,30,23])).
% 116.87/116.87 cnf(12465,plain,
% 116.87/116.87 (~P3(f8(a4),f7(a4,a4),f3(a1,a1))),
% 116.87/116.87 inference(scs_inference,[],[12005,12174,12392,12222,11504,12144,11483,9782,10000,35,21,26,29])).
% 116.87/116.87 cnf(12493,plain,
% 116.87/116.87 (~P3(f7(a1,a1),x124931,a4)),
% 116.87/116.87 inference(scs_inference,[],[12327,12465,12377,12398,9994,11933,10703,11229,11199,11312,26,30,29,9204])).
% 116.87/116.87 cnf(12955,plain,
% 116.87/116.87 (P2(f6(a4),f6(f6(a4)),a1)),
% 116.87/116.87 inference(scs_inference,[],[145,181,97,11953,11060,10913,259,5444,5508,5544,11697,13,8,15,23,14,22])).
% 116.87/116.87 cnf(13068,plain,
% 116.87/116.87 ($false),
% 116.87/116.87 inference(scs_inference,[],[4,10000,10444,10913,10521,9764,11857,11953,11060,12493,10907,11333,10718,9772,11862,10553,12955,22,23,2998,3030,2963,2947,6474,4538,4545,4552,4543,4550,4397,4390,4395,3974,3373,3527,3735,3371,3389,3525,1066,2638,2654,1082,2617,2613,2609,18]),
% 116.87/116.87 ['proof']).
% 116.87/116.87 % SZS output end Proof
% 116.87/116.87 % Total time :116.160000s
%------------------------------------------------------------------------------