%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD012-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n018.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:11 EDT 2024
% Result : Unsatisfiable 66.84s 66.88s
% Output : CNFRefutation 66.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : FLD012-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n018.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Jun 19 10:58:24 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.52/0.57 start to proof:theBenchmark
% 66.84/66.87 %-------------------------------------------
% 66.84/66.87 % File :CSE---1.7
% 66.84/66.87 % Problem :theBenchmark
% 66.84/66.87 % Transform :cnf
% 66.84/66.87 % Format :tptp:raw
% 66.84/66.87 % Command :java -jar mcs_scs.jar %d %s
% 66.84/66.87
% 66.84/66.87 % Result :Theorem 66.260000s
% 66.84/66.87 % Output :CNFRefutation 66.260000s
% 66.84/66.87 %-------------------------------------------
% 66.84/66.88 %--------------------------------------------------------------------------
% 66.84/66.88 % File : FLD012-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% 66.84/66.88 % Domain : Field Theory (Ordered fields)
% 66.84/66.88 % Problem : Compatibility of operation and inverse in multiplicative group
% 66.84/66.88 % Version : [Dra93] axioms : Especial.
% 66.84/66.88 % Theorem formulation : Relational with re axiom set.
% 66.84/66.88 % English :
% 66.84/66.88
% 66.84/66.88 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 66.84/66.88 % Source : [Dra93]
% 66.84/66.88 % Names :
% 66.84/66.88
% 66.84/66.88 % Status : Unsatisfiable
% 66.84/66.88 % Rating : 0.08 v8.2.0, 0.14 v7.5.0, 0.00 v7.4.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.38 v6.4.0, 0.25 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.30 v5.2.0, 0.20 v5.1.0, 0.36 v5.0.0, 0.50 v4.1.0, 0.38 v4.0.1, 0.40 v4.0.0, 0.29 v3.5.0, 0.43 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.62 v2.6.0, 0.67 v2.5.0, 0.80 v2.4.0, 1.00 v2.3.0, 0.67 v2.2.1, 1.00 v2.1.0
% 66.84/66.88 % Syntax : Number of clauses : 35 ( 12 unt; 3 nHn; 35 RR)
% 66.84/66.88 % Number of literals : 86 ( 0 equ; 52 neg)
% 66.84/66.88 % Maximal clause size : 5 ( 2 avg)
% 66.84/66.88 % Maximal term depth : 2 ( 1 avg)
% 66.84/66.88 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 66.84/66.88 % Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% 66.84/66.88 % Number of variables : 73 ( 0 sgn)
% 66.84/66.88 % SPC : CNF_UNS_RFO_NEQ_NHN
% 66.84/66.88
% 66.84/66.88 % Comments :
% 66.84/66.88 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 66.84/66.88 %--------------------------------------------------------------------------
% 66.84/66.88 include('Axioms/FLD002-0.ax').
% 66.84/66.88 %--------------------------------------------------------------------------
% 66.84/66.88 cnf(a_is_defined,hypothesis,
% 66.84/66.88 defined(a) ).
% 66.84/66.88
% 66.84/66.88 cnf(b_is_defined,hypothesis,
% 66.84/66.88 defined(b) ).
% 66.84/66.88
% 66.84/66.88 cnf(u_is_defined,hypothesis,
% 66.84/66.88 defined(u) ).
% 66.84/66.88
% 66.84/66.88 cnf(v_is_defined,hypothesis,
% 66.84/66.88 defined(v) ).
% 66.84/66.88
% 66.84/66.88 cnf(not_sum_5,negated_conjecture,
% 66.84/66.88 ~ sum(additive_identity,a,additive_identity) ).
% 66.84/66.88
% 66.84/66.88 cnf(not_sum_6,negated_conjecture,
% 66.84/66.88 ~ sum(additive_identity,b,additive_identity) ).
% 66.84/66.88
% 66.84/66.88 cnf(product_7,negated_conjecture,
% 66.84/66.88 product(a,b,u) ).
% 66.84/66.88
% 66.84/66.88 cnf(product_8,negated_conjecture,
% 66.84/66.88 product(multiplicative_inverse(a),multiplicative_inverse(b),v) ).
% 66.84/66.88
% 66.84/66.88 cnf(not_product_9,negated_conjecture,
% 66.84/66.88 ~ product(multiplicative_identity,multiplicative_inverse(u),v) ).
% 66.84/66.88
% 66.84/66.88 %--------------------------------------------------------------------------
% 66.84/66.88 %-------------------------------------------
% 66.84/66.88 % Proof found
% 66.84/66.88 % SZS status Theorem for theBenchmark
% 66.84/66.88 % SZS output start Proof
% 66.84/66.89 %ClaNum:35(EqnAxiom:0)
% 66.84/66.89 %VarNum:162(SingletonVarNum:73)
% 66.84/66.89 %MaxLitNum:5
% 66.84/66.89 %MaxfuncDepth:1
% 66.84/66.89 %SharedTerms:21
% 66.84/66.89 %goalClause: 7 8 10 11 12
% 66.84/66.89 %singleGoalClaCount:5
% 66.84/66.89 [1]P1(a1)
% 66.84/66.89 [2]P1(a4)
% 66.84/66.89 [3]P1(a2)
% 66.84/66.89 [4]P1(a5)
% 66.84/66.89 [5]P1(a7)
% 66.84/66.89 [6]P1(a10)
% 66.84/66.89 [7]P2(a2,a5,a7)
% 66.84/66.89 [9]~P4(a1,a1,a4)
% 66.84/66.89 [10]~P4(a1,a2,a1)
% 66.84/66.89 [11]~P4(a1,a5,a1)
% 66.84/66.89 [8]P2(f8(a2),f8(a5),a10)
% 66.84/66.89 [12]~P2(a4,f8(a7),a10)
% 66.84/66.89 [18]~P1(x181)+P4(a1,x181,x181)
% 66.84/66.89 [19]~P1(x191)+P2(a4,x191,x191)
% 66.84/66.89 [13]~P1(x131)+P1(f6(x131))
% 66.84/66.89 [20]~P1(x201)+P4(f6(x201),x201,a1)
% 66.84/66.89 [27]~P4(x272,x271,x273)+P4(x271,x272,x273)
% 66.84/66.89 [28]~P2(x282,x281,x283)+P2(x281,x282,x283)
% 66.84/66.89 [21]~P1(x211)+P4(a1,x211,a1)+P1(f8(x211))
% 66.84/66.89 [25]~P1(x251)+P2(f8(x251),x251,a4)+P4(a1,x251,a1)
% 66.84/66.89 [24]~P3(x242,x241)+~P3(x241,x242)+P4(a1,x241,x242)
% 66.84/66.89 [15]~P1(x152)+~P1(x151)+P1(f3(x151,x152))
% 66.84/66.89 [16]~P1(x162)+~P1(x161)+P1(f9(x161,x162))
% 66.84/66.89 [22]~P1(x222)+~P1(x221)+P4(x221,x222,f3(x221,x222))
% 66.84/66.89 [23]~P1(x232)+~P1(x231)+P2(x231,x232,f9(x231,x232))
% 66.84/66.89 [17]~P3(x171,x173)+P3(x171,x172)+~P3(x173,x172)
% 66.84/66.89 [14]P3(x142,x141)+~P1(x141)+~P1(x142)+P3(x141,x142)
% 66.84/66.89 [26]~P2(x263,x262,x261)+P3(a1,x261)+~P3(a1,x262)+~P3(a1,x263)
% 66.84/66.89 [29]~P4(x293,x295,x291)+P3(x291,x292)+~P4(x294,x295,x292)+~P3(x293,x294)
% 66.84/66.89 [30]~P4(x301,x306,x304)+P4(x301,x302,x303)+~P4(x304,x305,x303)+~P4(x306,x305,x302)
% 66.84/66.89 [31]~P4(x316,x314,x311)+P4(x311,x312,x313)+~P4(x314,x312,x315)+~P4(x316,x315,x313)
% 66.84/66.89 [32]~P2(x321,x326,x324)+P2(x321,x322,x323)+~P2(x324,x325,x323)+~P2(x326,x325,x322)
% 66.84/66.89 [33]~P2(x336,x334,x331)+P2(x331,x332,x333)+~P2(x334,x332,x335)+~P2(x336,x335,x333)
% 66.84/66.89 [34]~P2(x345,x347,x342)+~P2(x344,x347,x341)+P4(x341,x342,x343)+~P4(x344,x345,x346)+~P2(x346,x347,x343)
% 66.84/66.89 [35]~P2(x357,x352,x355)+~P2(x356,x352,x354)+P2(x351,x352,x353)+~P4(x354,x355,x353)+~P4(x356,x357,x351)
% 66.84/66.89 %EqnAxiom
% 66.84/66.89
% 66.84/66.89 %-------------------------------------------
% 66.84/66.90 cnf(36,plain,
% 66.84/66.90 (~P2(f8(a7),a4,a10)),
% 66.84/66.90 inference(scs_inference,[],[12,28])).
% 66.84/66.90 cnf(38,plain,
% 66.84/66.90 (~P4(a2,a1,a1)),
% 66.84/66.90 inference(scs_inference,[],[10,12,28,27])).
% 66.84/66.90 cnf(40,plain,
% 66.84/66.90 (P3(a1,a1)),
% 66.84/66.90 inference(scs_inference,[],[10,12,1,28,27,14])).
% 66.84/66.90 cnf(42,plain,
% 66.84/66.90 (~P3(a2,a1)+~P3(a1,a2)),
% 66.84/66.90 inference(scs_inference,[],[10,12,1,28,27,14,24])).
% 66.84/66.90 cnf(44,plain,
% 66.84/66.90 (~P2(x441,a2,a2)+P2(x441,a7,a7)),
% 66.84/66.90 inference(scs_inference,[],[7,10,12,1,28,27,14,24,32])).
% 66.84/66.90 cnf(46,plain,
% 66.84/66.90 (P2(a7,x461,a7)+~P2(a5,x461,a5)),
% 66.84/66.90 inference(scs_inference,[],[7,10,12,1,28,27,14,24,32,33])).
% 66.84/66.90 cnf(49,plain,
% 66.84/66.90 (~P4(a5,a1,a1)),
% 66.84/66.90 inference(scs_inference,[],[11,27])).
% 66.84/66.90 cnf(51,plain,
% 66.84/66.90 (P3(a4,a4)),
% 66.84/66.90 inference(scs_inference,[],[11,2,27,14])).
% 66.84/66.90 cnf(55,plain,
% 66.84/66.90 (~P2(x551,f8(a2),f8(a2))+P2(x551,a10,a10)),
% 66.84/66.90 inference(scs_inference,[],[11,8,2,27,14,24,32])).
% 66.84/66.90 cnf(57,plain,
% 66.84/66.90 (P2(a10,x571,a10)+~P2(f8(a5),x571,f8(a5))),
% 66.84/66.90 inference(scs_inference,[],[11,8,2,27,14,24,32,33])).
% 66.84/66.90 cnf(60,plain,
% 66.84/66.90 (P3(a2,a2)),
% 66.84/66.90 inference(scs_inference,[],[3,14])).
% 66.84/66.90 cnf(64,plain,
% 66.84/66.90 (~P2(a1,a1,a4)+~P3(a4,a1)),
% 66.84/66.90 inference(scs_inference,[],[3,9,40,14,24,26])).
% 66.84/66.90 cnf(67,plain,
% 66.84/66.90 (P3(a5,a5)),
% 66.84/66.90 inference(scs_inference,[],[4,14])).
% 66.84/66.90 cnf(72,plain,
% 66.84/66.90 (P3(a7,a7)),
% 66.84/66.90 inference(scs_inference,[],[5,14])).
% 66.84/66.90 cnf(77,plain,
% 66.84/66.90 (P3(a10,a10)),
% 66.84/66.90 inference(scs_inference,[],[6,14])).
% 66.84/66.90 cnf(79,plain,
% 66.84/66.90 (~P4(a7,x791,x792)+~P4(a7,x791,x793)+P3(x792,x793)),
% 66.84/66.90 inference(scs_inference,[],[6,72,14,29])).
% 66.84/66.90 cnf(82,plain,
% 66.84/66.90 (~P4(a2,x821,x822)+~P4(a2,x821,x823)+P3(x822,x823)),
% 66.84/66.90 inference(scs_inference,[],[60,29])).
% 66.84/66.90 cnf(83,plain,
% 66.84/66.90 (~P4(a5,x831,x832)+~P4(a5,x831,x833)+P3(x832,x833)),
% 66.84/66.90 inference(scs_inference,[],[67,29])).
% 66.84/66.90 cnf(92,plain,
% 66.84/66.90 (~P4(a1,x921,x922)+~P4(a1,x921,x923)+P3(x922,x923)),
% 66.84/66.90 inference(scs_inference,[],[40,29])).
% 66.84/66.90 cnf(106,plain,
% 66.84/66.90 (P4(a1,f6(a4),f6(a4))),
% 66.84/66.90 inference(scs_inference,[],[2,18,13])).
% 66.84/66.90 cnf(128,plain,
% 66.84/66.90 (P2(a4,f6(a7),f6(a7))),
% 66.84/66.90 inference(scs_inference,[],[5,19,13])).
% 66.84/66.90 cnf(150,plain,
% 66.84/66.90 (~P3(a2,a1)+~P4(a7,x1501,a1)+~P4(a7,x1501,a2)),
% 66.84/66.90 inference(scs_inference,[],[42,79])).
% 66.84/66.90 cnf(198,plain,
% 66.84/66.90 (P4(f6(f6(a10)),f6(a10),a1)),
% 66.84/66.90 inference(scs_inference,[],[6,20,13])).
% 66.84/66.90 cnf(199,plain,
% 66.84/66.90 (~P4(f6(a10),a5,f6(a10))),
% 66.84/66.90 inference(scs_inference,[],[11,198,31])).
% 66.84/66.90 cnf(204,plain,
% 66.84/66.90 (~P4(f6(a10),a2,f6(a10))),
% 66.84/66.90 inference(scs_inference,[],[10,198,31])).
% 66.84/66.90 cnf(206,plain,
% 66.84/66.90 (~P4(a2,f6(a10),f6(a10))),
% 66.84/66.90 inference(scs_inference,[],[10,198,31,27])).
% 66.84/66.90 cnf(222,plain,
% 66.84/66.90 (~P4(a2,x2221,a4)+~P4(a2,x2221,a1)+~P2(a1,a1,a4)),
% 66.84/66.90 inference(scs_inference,[],[64,82])).
% 66.84/66.90 cnf(238,plain,
% 66.84/66.90 (P2(a7,x2381,a7)+~P2(x2381,a2,a2)),
% 66.84/66.90 inference(scs_inference,[],[44,28])).
% 66.84/66.90 cnf(254,plain,
% 66.84/66.90 (~P2(x2541,a5,a5)+P2(a7,x2541,a7)),
% 66.84/66.90 inference(scs_inference,[],[46,28])).
% 66.84/66.90 cnf(286,plain,
% 66.84/66.90 (P2(a7,a4,a7)),
% 66.84/66.90 inference(scs_inference,[],[3,238,19])).
% 66.84/66.90 cnf(308,plain,
% 66.84/66.90 (P2(x3081,a7,a7)+~P2(x3081,a5,a5)),
% 66.84/66.90 inference(scs_inference,[],[254,28])).
% 66.84/66.90 cnf(355,plain,
% 66.84/66.90 (P2(a4,a7,a7)),
% 66.84/66.90 inference(scs_inference,[],[4,308,19])).
% 66.84/66.90 cnf(404,plain,
% 66.84/66.90 (~P1(f8(a2))+P2(a4,a10,a10)),
% 66.84/66.90 inference(scs_inference,[],[55,19])).
% 66.84/66.90 cnf(420,plain,
% 66.84/66.90 (P2(a4,a10,a10)),
% 66.84/66.90 inference(scs_inference,[],[10,3,404,21])).
% 66.84/66.90 cnf(487,plain,
% 66.84/66.90 (~P2(x4871,f8(a5),f8(a5))+P2(a10,x4871,a10)),
% 66.84/66.90 inference(scs_inference,[],[57,28])).
% 66.84/66.90 cnf(550,plain,
% 66.84/66.90 (~P1(f8(a5))+P2(a10,a4,a10)),
% 66.84/66.90 inference(scs_inference,[],[487,19])).
% 66.84/66.90 cnf(566,plain,
% 66.84/66.90 (P2(a10,a4,a10)),
% 66.84/66.90 inference(scs_inference,[],[11,4,550,21])).
% 66.84/66.90 cnf(913,plain,
% 66.84/66.90 (~P4(x9131,a2,a1)+~P4(a2,x9131,a4)+~P2(a1,a1,a4)),
% 66.84/66.90 inference(scs_inference,[],[222,27])).
% 66.84/66.90 cnf(992,plain,
% 66.84/66.90 (~P2(a4,a10,f8(a7))),
% 66.84/66.90 inference(scs_inference,[],[36,566,420,33])).
% 66.84/66.90 cnf(994,plain,
% 66.84/66.90 (~P2(a10,a4,f8(a7))),
% 66.84/66.90 inference(scs_inference,[],[36,566,420,33,28])).
% 66.84/66.90 cnf(998,plain,
% 66.84/66.90 (~P1(f8(a2))+~P2(f8(a2),f8(a5),f8(a7))),
% 66.84/66.90 inference(scs_inference,[],[8,36,566,420,33,28,32,19])).
% 66.84/66.90 cnf(1001,plain,
% 66.84/66.90 (~P2(f8(a2),x10011,a4)+~P2(x10011,f8(a7),f8(a5))),
% 66.84/66.90 inference(scs_inference,[],[8,12,33])).
% 66.84/66.90 cnf(1006,plain,
% 66.84/66.90 (~P2(f8(a2),x10061,f8(a7))+~P2(x10061,a4,f8(a5))),
% 66.84/66.90 inference(scs_inference,[],[8,36,33])).
% 66.84/66.90 cnf(1011,plain,
% 66.84/66.90 (~P2(a10,x10111,a4)+~P2(x10111,f8(a7),a4)),
% 66.84/66.90 inference(scs_inference,[],[12,566,33])).
% 66.84/66.90 cnf(1041,plain,
% 66.84/66.90 (~P2(f8(a7),x10411,a4)+~P2(a10,x10411,a4)),
% 66.84/66.90 inference(scs_inference,[],[1011,28])).
% 66.84/66.90 cnf(1125,plain,
% 66.84/66.90 (~P2(a10,a7,a4)+P4(a1,a7,a1)),
% 66.84/66.90 inference(scs_inference,[],[5,1041,25])).
% 66.84/66.90 cnf(1141,plain,
% 66.84/66.90 (~P2(a7,a10,a4)+P4(a1,a7,a1)),
% 66.84/66.90 inference(scs_inference,[],[1125,28])).
% 66.84/66.90 cnf(1157,plain,
% 66.84/66.90 (~P2(a7,f8(a2),x11571)+~P2(x11571,f8(a5),a4)+P4(a1,a7,a1)),
% 66.84/66.90 inference(scs_inference,[],[8,1141,32])).
% 66.84/66.90 cnf(1237,plain,
% 66.84/66.90 (~P2(f8(a5),f8(a2),f8(a7))+~P1(f8(a2))),
% 66.84/66.90 inference(scs_inference,[],[998,28])).
% 66.84/66.90 cnf(1269,plain,
% 66.84/66.90 (~P2(f8(a5),f8(a2),f8(a7))),
% 66.84/66.90 inference(scs_inference,[],[10,3,1237,21])).
% 66.84/66.90 cnf(1270,plain,
% 66.84/66.90 (~P2(f8(a2),f8(a5),f8(a7))),
% 66.84/66.90 inference(scs_inference,[],[1269,28])).
% 66.84/66.90 cnf(1383,plain,
% 66.84/66.90 (~P2(f8(a7),x13831,f8(a5))+~P2(f8(a2),x13831,a4)),
% 66.84/66.90 inference(scs_inference,[],[1001,28])).
% 66.84/66.90 cnf(1415,plain,
% 66.84/66.90 (~P2(f8(a2),a2,x14151)+~P2(x14151,a5,f8(a7))+~P2(a7,a4,f8(a5))),
% 66.84/66.90 inference(scs_inference,[],[7,1006,32])).
% 66.84/66.90 cnf(1928,plain,
% 66.84/66.90 (~P4(a7,a2,a7)+~P2(x19281,f8(a5),a4)+~P2(a7,f8(a2),x19281)),
% 66.84/66.90 inference(scs_inference,[],[10,1157,31])).
% 66.84/66.90 cnf(1975,plain,
% 66.84/66.90 (~P2(f8(a2),a7,x19751)+~P2(x19751,f8(a5),a4)+~P4(a7,a2,a7)),
% 66.84/66.90 inference(scs_inference,[],[1928,28])).
% 66.84/66.90 cnf(2006,plain,
% 66.84/66.90 (~P2(f8(a5),x20061,a4)+~P2(f8(a2),a7,x20061)+~P4(a7,a2,a7)),
% 66.84/66.90 inference(scs_inference,[],[1975,28])).
% 66.84/66.90 cnf(2069,plain,
% 66.84/66.90 (~P2(a4,a7,f8(a5))+~P2(x20691,a5,f8(a7))+~P2(f8(a2),a2,x20691)),
% 66.84/66.90 inference(scs_inference,[],[1415,28])).
% 66.84/66.90 cnf(3504,plain,
% 66.84/66.90 (~P4(x35041,x35042,a2)+~P4(f6(a10),x35041,x35043)+~P4(x35043,x35042,f6(a10))),
% 66.84/66.90 inference(scs_inference,[],[204,1269,60,30])).
% 66.84/66.90 cnf(3588,plain,
% 66.84/66.90 (~P2(x35881,f8(a5),a4)+~P2(f8(a7),x35881,f8(a2))),
% 66.84/66.90 inference(scs_inference,[],[8,36,32])).
% 66.84/66.90 cnf(3590,plain,
% 66.84/66.90 (~P2(x35901,f8(a5),a4)+~P2(x35901,f8(a7),f8(a2))),
% 66.84/66.90 inference(scs_inference,[],[8,36,32,28])).
% 66.84/66.90 cnf(3593,plain,
% 66.84/66.90 (~P2(a4,x35931,a4)+~P2(a10,x35931,f8(a7))),
% 66.84/66.90 inference(scs_inference,[],[994,566,32])).
% 66.84/66.90 cnf(3600,plain,
% 66.84/66.90 (~P2(f8(a5),x36001,f8(a5))+~P2(x36001,a10,f8(a7))),
% 66.84/66.90 inference(scs_inference,[],[8,1270,32,28])).
% 66.84/66.90 cnf(3613,plain,
% 66.84/66.90 (~P2(f8(a2),x36131,f8(a7))+~P2(f8(a5),x36132,x36131)+~P2(a4,x36132,a4)),
% 66.84/66.90 inference(scs_inference,[],[8,3593,33])).
% 66.84/66.90 cnf(3626,plain,
% 66.84/66.90 (P2(a5,a2,a7)),
% 66.84/66.90 inference(scs_inference,[],[7,28])).
% 66.84/66.90 cnf(3629,plain,
% 66.84/66.90 (P2(f8(a5),f8(a2),a10)),
% 66.84/66.90 inference(scs_inference,[],[8,28])).
% 66.84/66.90 cnf(3634,plain,
% 66.84/66.90 (P2(f6(a7),a4,f6(a7))),
% 66.84/66.90 inference(scs_inference,[],[128,28])).
% 66.84/66.90 cnf(3685,plain,
% 66.84/66.90 (P4(f6(a10),f6(f6(a10)),a1)),
% 66.84/66.90 inference(scs_inference,[],[198,27])).
% 66.84/66.90 cnf(3689,plain,
% 66.84/66.90 (~P4(f6(f6(a10)),f6(a10),a5)+~P1(f6(a10))),
% 66.84/66.90 inference(scs_inference,[],[198,199,27,30,18])).
% 66.84/66.90 cnf(3694,plain,
% 66.84/66.90 (P4(f6(a4),x36941,f6(a4))+~P4(a1,x36941,a1)),
% 66.84/66.90 inference(scs_inference,[],[106,27,31])).
% 66.84/66.90 cnf(3702,plain,
% 66.84/66.90 (~P4(f6(a10),f6(f6(a10)),a5)+~P1(f6(a10))),
% 66.84/66.90 inference(scs_inference,[],[3689,27])).
% 66.84/66.90 cnf(3711,plain,
% 66.84/66.90 (~P4(f6(f6(a10)),f6(a10),a2)+~P1(f6(a10))),
% 66.84/66.90 inference(scs_inference,[],[3685,204,30,18])).
% 66.84/66.90 cnf(3722,plain,
% 66.84/66.90 (P2(f8(a5),a5,a4)),
% 66.84/66.90 inference(scs_inference,[],[11,4,25])).
% 66.84/66.90 cnf(3729,plain,
% 66.84/66.90 (P2(a5,f8(a5),a4)),
% 66.84/66.90 inference(scs_inference,[],[3722,28])).
% 66.84/66.90 cnf(3731,plain,
% 66.84/66.90 (P2(f8(a2),a2,a4)),
% 66.84/66.90 inference(scs_inference,[],[10,3,3722,28,25])).
% 66.84/66.90 cnf(3733,plain,
% 66.84/66.90 (~P2(a2,f8(a7),f8(a5))),
% 66.84/66.90 inference(scs_inference,[],[10,12,8,3,3722,28,25,33])).
% 66.84/66.90 cnf(3735,plain,
% 66.84/66.90 (~P2(f8(a7),a2,f8(a5))),
% 66.84/66.90 inference(scs_inference,[],[10,12,8,3,3722,28,25,33,1383])).
% 66.84/66.90 cnf(3737,plain,
% 66.84/66.90 (~P2(a5,f8(a7),f8(a2))),
% 66.84/66.90 inference(scs_inference,[],[10,12,8,3,3722,28,25,33,1383,3590])).
% 66.84/66.90 cnf(3739,plain,
% 66.84/66.90 (~P2(f8(a7),a5,f8(a2))),
% 66.84/66.90 inference(scs_inference,[],[10,12,8,3,3722,28,25,33,1383,3590,3588])).
% 66.84/66.91 cnf(3743,plain,
% 66.84/66.91 (P4(a1,a7,a1)+~P2(a7,f8(a2),a5)),
% 66.84/66.91 inference(scs_inference,[],[10,12,8,3,3722,28,25,33,1383,3590,3588,2069,1157])).
% 66.84/66.91 cnf(3749,plain,
% 66.84/66.91 (P2(a2,f8(a2),a4)),
% 66.84/66.91 inference(scs_inference,[],[3731,28])).
% 66.84/66.91 cnf(3761,plain,
% 66.84/66.91 (~P2(f8(a2),a7,a5)+P4(a1,a7,a1)),
% 66.84/66.91 inference(scs_inference,[],[3743,28])).
% 66.84/66.91 cnf(3821,plain,
% 66.84/66.91 (~P2(x38211,x38212,a2)+~P2(f8(a7),x38211,x38213)+~P2(x38213,x38212,f8(a5))),
% 66.84/66.91 inference(scs_inference,[],[206,3735,67,32])).
% 66.84/66.91 cnf(3825,plain,
% 66.84/66.91 (~P2(x38251,x38252,f8(a2))+~P2(x38251,x38253,a5)+~P2(x38253,f8(a7),x38252)),
% 66.84/66.91 inference(scs_inference,[],[3737,206,77,33])).
% 66.84/66.91 cnf(3838,plain,
% 66.84/66.91 (P4(f6(a4),a7,f6(a4))+~P2(f8(a2),a7,a5)),
% 66.84/66.91 inference(scs_inference,[],[3761,3694])).
% 66.84/66.91 cnf(3854,plain,
% 66.84/66.91 (~P4(f6(a10),f6(f6(a10)),a5)),
% 66.84/66.91 inference(scs_inference,[],[6,3702,13])).
% 66.84/66.91 cnf(3870,plain,
% 66.84/66.91 (~P4(f6(a10),f6(f6(a10)),a2)+~P1(f6(a10))),
% 66.84/66.91 inference(scs_inference,[],[3711,27])).
% 66.84/66.91 cnf(4144,plain,
% 66.84/66.91 (~P4(f6(a10),f6(f6(a10)),a2)),
% 66.84/66.91 inference(scs_inference,[],[6,3870,13])).
% 66.84/66.91 cnf(4638,plain,
% 66.84/66.91 (P4(a7,f6(a4),f6(a4))+~P2(f8(a2),a7,a5)),
% 66.84/66.91 inference(scs_inference,[],[3838,27])).
% 66.84/66.91 cnf(6087,plain,
% 66.84/66.91 (~P2(x60871,x60872,f8(a5))+~P2(x60871,x60873,a2)+~P2(x60873,f8(a7),x60872)),
% 66.84/66.91 inference(scs_inference,[],[3733,206,60,33])).
% 66.84/66.91 cnf(6440,plain,
% 66.84/66.91 (~P2(x64401,x64402,a5)+~P2(f8(a7),x64401,x64403)+~P2(x64403,x64402,f8(a2))),
% 66.84/66.91 inference(scs_inference,[],[3739,3737,77,32])).
% 66.84/66.91 cnf(7306,plain,
% 66.84/66.91 (~P4(f6(f6(a10)),f6(a10),a5)),
% 66.84/66.91 inference(scs_inference,[],[3854,27])).
% 66.84/66.91 cnf(7309,plain,
% 66.84/66.91 (~P4(f6(f6(a10)),f6(a10),a2)),
% 66.84/66.91 inference(scs_inference,[],[4144,27])).
% 66.84/66.91 cnf(7311,plain,
% 66.84/66.91 (~P4(f6(a10),x73111,f6(a10))+~P4(a1,x73111,a5)),
% 66.84/66.91 inference(scs_inference,[],[7306,4144,198,27,30])).
% 66.84/66.91 cnf(7318,plain,
% 66.84/66.91 (~P1(f6(a10))+~P4(a1,a1,a2)),
% 66.84/66.91 inference(scs_inference,[],[7309,198,30,27,18])).
% 66.84/66.91 cnf(7357,plain,
% 66.84/66.91 (~P4(x73571,f6(a10),f6(a10))+~P4(a1,x73571,a5)),
% 66.84/66.91 inference(scs_inference,[],[7311,27])).
% 66.84/66.91 cnf(8994,plain,
% 66.84/66.91 (P4(a1,f6(a1),f6(a1))),
% 66.84/66.91 inference(scs_inference,[],[1,13,18])).
% 66.84/66.91 cnf(9045,plain,
% 66.84/66.91 (P4(a1,f6(a7),f6(a7))),
% 66.84/66.91 inference(scs_inference,[],[5,13,18])).
% 66.84/66.91 cnf(9046,plain,
% 66.84/66.91 (P3(f6(a7),f6(a7))),
% 66.84/66.91 inference(scs_inference,[],[9045,92])).
% 66.84/66.91 cnf(9096,plain,
% 66.84/66.91 (P4(f6(f6(a7)),f6(a7),a1)),
% 66.84/66.91 inference(scs_inference,[],[5,13,20])).
% 66.84/66.91 cnf(9097,plain,
% 66.84/66.91 (~P4(f6(a7),a5,f6(a7))),
% 66.84/66.91 inference(scs_inference,[],[11,9096,31])).
% 66.84/66.91 cnf(9099,plain,
% 66.84/66.91 (~P4(a5,f6(a7),f6(a7))),
% 66.84/66.91 inference(scs_inference,[],[11,9096,31,27])).
% 66.84/66.91 cnf(9101,plain,
% 66.84/66.91 (~P4(x91011,f6(a7),a5)+~P4(f6(a7),x91011,a1)),
% 66.84/66.91 inference(scs_inference,[],[11,9045,9096,31,27,30])).
% 66.84/66.91 cnf(9103,plain,
% 66.84/66.91 (~P2(a1,a4,a5)),
% 66.84/66.91 inference(scs_inference,[],[11,3634,9045,9096,31,27,30,34])).
% 66.84/66.91 cnf(9105,plain,
% 66.84/66.91 (~P2(a4,a1,a5)),
% 66.84/66.91 inference(scs_inference,[],[11,3634,9045,9096,31,27,30,34,28])).
% 66.84/66.91 cnf(9123,plain,
% 66.84/66.91 (~P2(x91231,a7,a5)+~P2(x91231,a7,a1)),
% 66.84/66.91 inference(scs_inference,[],[286,9103,33])).
% 66.84/66.91 cnf(9125,plain,
% 66.84/66.91 (~P2(x91251,a7,a5)+~P2(a7,x91251,a1)),
% 66.84/66.91 inference(scs_inference,[],[286,9103,33,28])).
% 66.84/66.91 cnf(9144,plain,
% 66.84/66.91 (~P2(a1,a2,x91441)+~P2(x91441,f8(a2),a5)),
% 66.84/66.91 inference(scs_inference,[],[3749,9103,32])).
% 66.84/66.91 cnf(9146,plain,
% 66.84/66.91 (~P2(a2,a1,x91461)+~P2(x91461,f8(a2),a5)),
% 66.84/66.91 inference(scs_inference,[],[3749,9103,32,28])).
% 66.84/66.91 cnf(9346,plain,
% 66.84/66.91 (~P2(f8(a2),x93461,a5)+~P2(a1,a2,x93461)),
% 66.84/66.91 inference(scs_inference,[],[9144,28])).
% 66.84/66.91 cnf(9362,plain,
% 66.84/66.91 (~P2(f8(a2),x93621,a5)+~P2(a2,a1,x93621)),
% 66.84/66.91 inference(scs_inference,[],[9146,28])).
% 66.84/66.91 cnf(9459,plain,
% 66.84/66.91 (~P4(f6(a7),x94591,x94592)+~P4(f6(a7),x94591,x94593)+P3(x94592,x94593)),
% 66.84/66.91 inference(scs_inference,[],[3735,206,9046,29])).
% 66.84/66.91 cnf(10221,plain,
% 66.84/66.91 (~P4(f6(a4),x102211,a1)+~P4(f6(a4),x102211,a4)),
% 66.84/66.91 inference(scs_inference,[],[9,106,30])).
% 66.84/66.91 cnf(10223,plain,
% 66.84/66.91 (~P4(f6(a4),x102231,a1)+~P4(x102231,f6(a4),a4)),
% 66.84/66.91 inference(scs_inference,[],[9,106,30,27])).
% 66.84/66.91 cnf(10255,plain,
% 66.84/66.91 (P2(a4,a5,a5)),
% 66.84/66.91 inference(scs_inference,[],[5,4,13,19])).
% 66.84/66.91 cnf(10257,plain,
% 66.84/66.91 (P4(f6(a7),a7,a1)),
% 66.84/66.91 inference(scs_inference,[],[5,4,13,19,20])).
% 66.84/66.91 cnf(10259,plain,
% 66.84/66.91 (P4(a1,a7,a7)),
% 66.84/66.91 inference(scs_inference,[],[5,4,13,19,20,18])).
% 66.84/66.91 cnf(10261,plain,
% 66.84/66.91 (P2(a5,a4,a5)),
% 66.84/66.91 inference(scs_inference,[],[5,4,13,19,20,18,28])).
% 66.84/66.91 cnf(10263,plain,
% 66.84/66.91 (P4(f6(a1),a1,f6(a1))),
% 66.84/66.91 inference(scs_inference,[],[8994,5,4,13,19,20,18,28,27])).
% 66.84/66.91 cnf(10265,plain,
% 66.84/66.91 (P1(f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[8994,5,4,13,19,20,18,28,27,15])).
% 66.84/66.91 cnf(10267,plain,
% 66.84/66.91 (P1(f9(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[8994,5,4,13,19,20,18,28,27,15,16])).
% 66.84/66.91 cnf(10269,plain,
% 66.84/66.91 (P4(a7,a7,f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[8994,5,4,13,19,20,18,28,27,15,16,22])).
% 66.84/66.91 cnf(10273,plain,
% 66.84/66.91 (P1(f8(a2))),
% 66.84/66.91 inference(scs_inference,[],[8994,5,4,10,3,13,19,20,18,28,27,15,16,22,79,21])).
% 66.84/66.91 cnf(10275,plain,
% 66.84/66.91 (P2(a7,a7,f9(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[8994,5,4,10,3,13,19,20,18,28,27,15,16,22,79,21,23])).
% 66.84/66.91 cnf(10277,plain,
% 66.84/66.91 (P4(a1,a1,a1)),
% 66.84/66.91 inference(scs_inference,[],[8994,5,4,10,3,40,13,19,20,18,28,27,15,16,22,79,21,23,24])).
% 66.84/66.91 cnf(10279,plain,
% 66.84/66.91 (P2(a4,a4,a4)),
% 66.84/66.91 inference(scs_inference,[],[8994,5,4,10,3,3729,40,13,19,20,18,28,27,15,16,22,79,21,23,24,32])).
% 66.84/66.91 cnf(10281,plain,
% 66.84/66.91 (~P4(f6(a7),a7,a5)),
% 66.84/66.91 inference(scs_inference,[],[8994,9103,3634,5,4,286,10,3,3729,40,13,19,20,18,28,27,15,16,22,79,21,23,24,32,35])).
% 66.84/66.91 cnf(10285,plain,
% 66.84/66.91 (P4(f6(a7),f3(a7,a7),a7)),
% 66.84/66.91 inference(scs_inference,[],[8994,9103,3634,5,4,286,10,3,3729,40,13,19,20,18,28,27,15,16,22,79,21,23,24,32,35,1928,30])).
% 66.84/66.91 cnf(10294,plain,
% 66.84/66.91 (P1(f6(a10))),
% 66.84/66.91 inference(scs_inference,[],[6,13])).
% 66.84/66.91 cnf(10296,plain,
% 66.84/66.91 (P2(a4,f3(a7,a7),f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[10265,6,13,19])).
% 66.84/66.91 cnf(10298,plain,
% 66.84/66.91 (P4(f6(a10),a10,a1)),
% 66.84/66.91 inference(scs_inference,[],[10265,6,13,19,20])).
% 66.84/66.91 cnf(10300,plain,
% 66.84/66.91 (P4(a1,f3(a7,a7),f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[10265,6,13,19,20,18])).
% 66.84/66.91 cnf(10302,plain,
% 66.84/66.91 (P2(f3(a7,a7),a4,f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[10265,6,13,19,20,18,28])).
% 66.84/66.91 cnf(10304,plain,
% 66.84/66.91 (P4(a7,a1,a7)),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,6,13,19,20,18,28,27])).
% 66.84/66.91 cnf(10308,plain,
% 66.84/66.91 (P4(a10,a10,f3(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,6,13,19,20,18,28,27,15,22])).
% 66.84/66.91 cnf(10310,plain,
% 66.84/66.91 (P1(f9(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,6,13,19,20,18,28,27,15,22,16])).
% 66.84/66.91 cnf(10312,plain,
% 66.84/66.91 (P2(a10,a10,f9(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,6,13,19,20,18,28,27,15,22,16,23])).
% 66.84/66.91 cnf(10314,plain,
% 66.84/66.91 (P1(f8(a5))),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,6,4,11,13,19,20,18,28,27,15,22,16,23,21])).
% 66.84/66.91 cnf(10316,plain,
% 66.84/66.91 (P4(a1,a4,a4)),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,6,4,11,51,13,19,20,18,28,27,15,22,16,23,21,24])).
% 66.84/66.91 cnf(10318,plain,
% 66.84/66.91 (P2(f9(a7,a7),a4,f9(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,10275,6,4,286,11,51,13,19,20,18,28,27,15,22,16,23,21,24,33])).
% 66.84/66.91 cnf(10320,plain,
% 66.84/66.91 (P2(a4,f9(a10,a10),f9(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,10275,6,4,286,420,11,51,13,19,20,18,28,27,15,22,16,23,21,24,33,32])).
% 66.84/66.91 cnf(10322,plain,
% 66.84/66.91 (P2(f3(a10,a10),a4,f3(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,10275,6,4,286,420,11,566,51,13,19,20,18,28,27,15,22,16,23,21,24,33,32,35])).
% 66.84/66.91 cnf(10324,plain,
% 66.84/66.91 (~P2(f8(a2),a7,a5)+~P4(a7,a2,a7)),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,10275,6,4,286,420,3722,11,566,51,13,19,20,18,28,27,15,22,16,23,21,24,33,32,35,2006])).
% 66.84/66.91 cnf(10326,plain,
% 66.84/66.91 (P3(f3(a10,a10),f3(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10259,10265,10275,6,4,286,420,3722,11,566,51,77,13,19,20,18,28,27,15,22,16,23,21,24,33,32,35,2006,29])).
% 66.84/66.91 cnf(10330,plain,
% 66.84/66.91 (~P4(a1,a1,a2)),
% 66.84/66.91 inference(scs_inference,[],[10294,7318])).
% 66.84/66.91 cnf(10333,plain,
% 66.84/66.91 (P1(f6(a4))),
% 66.84/66.91 inference(scs_inference,[],[2,13])).
% 66.84/66.91 cnf(10335,plain,
% 66.84/66.91 (P2(a4,f9(a7,a7),f9(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[10267,2,13,19])).
% 66.84/66.91 cnf(10337,plain,
% 66.84/66.91 (P4(f6(a4),a4,a1)),
% 66.84/66.91 inference(scs_inference,[],[10267,2,13,19,20])).
% 66.84/66.91 cnf(10339,plain,
% 66.84/66.91 (P4(a1,f9(a7,a7),f9(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[10267,2,13,19,20,18])).
% 66.84/66.91 cnf(10341,plain,
% 66.84/66.91 (P4(a4,a1,a4)),
% 66.84/66.91 inference(scs_inference,[],[10316,10267,2,13,19,20,18,27])).
% 66.84/66.91 cnf(10345,plain,
% 66.84/66.91 (P1(f3(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10316,10320,10267,2,13,19,20,18,27,28,15])).
% 66.84/66.91 cnf(10347,plain,
% 66.84/66.91 (P1(f9(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10316,10320,10267,2,13,19,20,18,27,28,15,16])).
% 66.84/66.91 cnf(10349,plain,
% 66.84/66.91 (P4(a4,a4,f3(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10316,10320,10267,2,13,19,20,18,27,28,15,16,22])).
% 66.84/66.91 cnf(10353,plain,
% 66.84/66.91 (P2(a4,a4,f9(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10316,10320,10267,2,13,19,20,18,27,28,15,16,22,92,23])).
% 66.84/66.91 cnf(10355,plain,
% 66.84/66.91 (P4(a1,f3(a10,a10),f3(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10316,10326,10320,10267,2,13,19,20,18,27,28,15,16,22,92,23,24])).
% 66.84/66.91 cnf(10357,plain,
% 66.84/66.91 (P4(a1,f3(a4,a4),f3(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10316,10326,10320,10267,2,13,19,20,18,27,28,15,16,22,92,23,24,30])).
% 66.84/66.91 cnf(10361,plain,
% 66.84/66.91 (P2(f8(a2),a7,a5)),
% 66.84/66.91 inference(scs_inference,[],[7,10316,10326,10320,10267,10255,2,3731,51,13,19,20,18,27,28,15,16,22,92,23,24,30,29,32])).
% 66.84/66.91 cnf(10367,plain,
% 66.84/66.91 (~P2(a1,a2,a7)),
% 66.84/66.91 inference(scs_inference,[],[7,10316,10326,10320,10267,10255,2,3731,51,13,19,20,18,27,28,15,16,22,92,23,24,30,29,32,9123,9125,9346])).
% 66.84/66.91 cnf(10369,plain,
% 66.84/66.91 (~P2(a2,a1,a7)),
% 66.84/66.91 inference(scs_inference,[],[7,10316,10326,10320,10267,10255,2,3731,51,13,19,20,18,27,28,15,16,22,92,23,24,30,29,32,9123,9125,9346,9362])).
% 66.84/66.91 cnf(10371,plain,
% 66.84/66.91 (~P4(f6(a4),a4,a4)),
% 66.84/66.91 inference(scs_inference,[],[7,10316,10326,10320,10267,10255,2,3731,51,13,19,20,18,27,28,15,16,22,92,23,24,30,29,32,9123,9125,9346,9362,10221])).
% 66.84/66.91 cnf(10373,plain,
% 66.84/66.91 (~P4(a4,f6(a4),a4)),
% 66.84/66.91 inference(scs_inference,[],[7,10316,10326,10320,10267,10255,2,3731,51,13,19,20,18,27,28,15,16,22,92,23,24,30,29,32,9123,9125,9346,9362,10221,10223])).
% 66.84/66.91 cnf(10375,plain,
% 66.84/66.91 (~P4(a7,a2,a7)),
% 66.84/66.91 inference(scs_inference,[],[7,10316,10326,10320,10267,10255,2,3731,51,13,19,20,18,27,28,15,16,22,92,23,24,30,29,32,9123,9125,9346,9362,10221,10223,10324])).
% 66.84/66.91 cnf(10378,plain,
% 66.84/66.91 (P4(f3(a7,a7),a1,f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[7,10304,10316,10326,10320,10267,10255,10269,2,3722,3731,51,13,19,20,18,27,28,15,16,22,92,23,24,30,29,32,9123,9125,9346,9362,10221,10223,10324,3613,31])).
% 66.84/66.91 cnf(10380,plain,
% 66.84/66.91 (P2(a7,f8(a2),a5)),
% 66.84/66.91 inference(scs_inference,[],[7,10304,10316,10326,10320,10267,10255,10261,10269,2,3626,3722,3731,3749,51,13,19,20,18,27,28,15,16,22,92,23,24,30,29,32,9123,9125,9346,9362,10221,10223,10324,3613,31,33])).
% 66.84/66.91 cnf(10382,plain,
% 66.84/66.91 (P4(a1,a7,a1)),
% 66.84/66.91 inference(scs_inference,[],[7,10304,10316,10326,10320,10267,10255,10261,10269,2,3626,3722,3731,3749,51,13,19,20,18,27,28,15,16,22,92,23,24,30,29,32,9123,9125,9346,9362,10221,10223,10324,3613,31,33,3743])).
% 66.84/66.91 cnf(10385,plain,
% 66.84/66.91 (P4(f6(a4),a7,f6(a4))),
% 66.84/66.91 inference(scs_inference,[],[10361,3838])).
% 66.84/66.91 cnf(10386,plain,
% 66.84/66.91 (P4(a7,f6(a4),f6(a4))),
% 66.84/66.91 inference(scs_inference,[],[10361,4638])).
% 66.84/66.91 cnf(10390,plain,
% 66.84/66.91 (P1(f6(a5))),
% 66.84/66.91 inference(scs_inference,[],[4,13])).
% 66.84/66.91 cnf(10392,plain,
% 66.84/66.91 (P2(a4,f3(a4,a4),f3(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10345,4,13,19])).
% 66.84/66.91 cnf(10394,plain,
% 66.84/66.91 (P4(f6(a5),a5,a1)),
% 66.84/66.91 inference(scs_inference,[],[10345,4,13,19,20])).
% 66.84/66.91 cnf(10396,plain,
% 66.84/66.91 (P4(a1,f8(a2),f8(a2))),
% 66.84/66.91 inference(scs_inference,[],[10345,10273,4,13,19,20,18])).
% 66.84/66.91 cnf(10398,plain,
% 66.84/66.91 (P2(a4,f3(a10,a10),f3(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10322,10345,10273,4,13,19,20,18,28])).
% 66.84/66.91 cnf(10400,plain,
% 66.84/66.91 (P4(a7,a1,a1)),
% 66.84/66.91 inference(scs_inference,[],[10382,10322,10345,10273,4,13,19,20,18,28,27])).
% 66.84/66.91 cnf(10404,plain,
% 66.84/66.91 (P4(a5,a5,f3(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10382,10322,10345,10273,4,13,19,20,18,28,27,15,22])).
% 66.84/66.91 cnf(10406,plain,
% 66.84/66.91 (P1(f9(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10382,10322,10345,10273,4,13,19,20,18,28,27,15,22,16])).
% 66.84/66.91 cnf(10408,plain,
% 66.84/66.91 (P2(a5,a5,f9(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10382,10322,10345,10273,4,13,19,20,18,28,27,15,22,16,23])).
% 66.84/66.91 cnf(10410,plain,
% 66.84/66.91 (P4(a1,a2,a2)),
% 66.84/66.91 inference(scs_inference,[],[10382,10322,10345,10273,4,60,13,19,20,18,28,27,15,22,16,23,24])).
% 66.84/66.91 cnf(10412,plain,
% 66.84/66.91 (~P4(a1,a7,a2)),
% 66.84/66.91 inference(scs_inference,[],[10330,10382,10322,10345,10273,10304,4,60,13,19,20,18,28,27,15,22,16,23,24,31])).
% 66.84/66.91 cnf(10414,plain,
% 66.84/66.91 (P4(a1,f3(a7,a7),a1)),
% 66.84/66.91 inference(scs_inference,[],[10330,10382,10322,10345,10273,10304,10269,4,60,13,19,20,18,28,27,15,22,16,23,24,31,30])).
% 66.84/66.91 cnf(10416,plain,
% 66.84/66.91 (P2(f9(a4,a4),a4,f9(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10330,10382,10322,10345,10273,10353,10279,10304,10269,4,60,13,19,20,18,28,27,15,22,16,23,24,31,30,33])).
% 66.84/66.91 cnf(10418,plain,
% 66.84/66.91 (P2(a4,f9(a4,a4),f9(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10330,10382,10322,10345,10273,10353,10279,10304,10269,4,60,13,19,20,18,28,27,15,22,16,23,24,31,30,33,32])).
% 66.84/66.91 cnf(10420,plain,
% 66.84/66.91 (P2(f3(a5,a5),a4,f3(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10330,10382,10322,10345,10273,10353,10279,10304,10261,10269,4,60,13,19,20,18,28,27,15,22,16,23,24,31,30,33,32,35])).
% 66.84/66.91 cnf(10422,plain,
% 66.84/66.91 (P3(f3(a5,a5),f3(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10330,10382,10322,10345,10273,10353,10279,10304,10261,10269,4,60,13,19,20,18,28,27,15,22,16,23,24,31,30,33,32,35,83])).
% 66.84/66.91 cnf(10428,plain,
% 66.84/66.91 (~P4(a7,a1,a2)),
% 66.84/66.91 inference(scs_inference,[],[10330,10382,10322,10345,10273,10353,10279,10257,10304,10261,10269,4,60,13,19,20,18,28,27,15,22,16,23,24,31,30,33,32,35,83,150,9459,79])).
% 66.84/66.91 cnf(10431,plain,
% 66.84/66.91 (P1(f6(a1))),
% 66.84/66.91 inference(scs_inference,[],[1,13])).
% 66.84/66.91 cnf(10433,plain,
% 66.84/66.91 (P2(a4,f6(a10),f6(a10))),
% 66.84/66.91 inference(scs_inference,[],[10294,1,13,19])).
% 66.84/66.91 cnf(10435,plain,
% 66.84/66.91 (P4(f6(a1),a1,a1)),
% 66.84/66.91 inference(scs_inference,[],[10294,1,13,19,20])).
% 66.84/66.91 cnf(10437,plain,
% 66.84/66.91 (P4(a1,f6(a10),f6(a10))),
% 66.84/66.91 inference(scs_inference,[],[10294,1,13,19,20,18])).
% 66.84/66.91 cnf(10439,plain,
% 66.84/66.91 (P4(a2,a1,a2)),
% 66.84/66.91 inference(scs_inference,[],[10410,10294,1,13,19,20,18,27])).
% 66.84/66.91 cnf(10441,plain,
% 66.84/66.91 (P2(f3(a4,a4),a4,f3(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10410,10392,10294,1,13,19,20,18,27,28])).
% 66.84/66.91 cnf(10443,plain,
% 66.84/66.91 (P1(f3(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10410,10392,10294,1,13,19,20,18,27,28,15])).
% 66.84/66.91 cnf(10445,plain,
% 66.84/66.91 (~P4(a10,f6(a10),a2)),
% 66.84/66.91 inference(scs_inference,[],[10410,10392,10294,10298,1,13,19,20,18,27,28,15,3504])).
% 66.84/66.91 cnf(10447,plain,
% 66.84/66.91 (P1(f9(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10410,10392,10294,10298,1,13,19,20,18,27,28,15,3504,16])).
% 66.84/66.91 cnf(10449,plain,
% 66.84/66.91 (P4(a1,a1,f3(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10410,10392,10294,10298,1,13,19,20,18,27,28,15,3504,16,22])).
% 66.84/66.91 cnf(10451,plain,
% 66.84/66.91 (P2(a1,a1,f9(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10410,10392,10294,10298,1,13,19,20,18,27,28,15,3504,16,22,23])).
% 66.84/66.91 cnf(10453,plain,
% 66.84/66.91 (P4(a1,f3(a5,a5),f3(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10410,10422,10392,10294,10298,1,13,19,20,18,27,28,15,3504,16,22,23,24])).
% 66.84/66.91 cnf(10455,plain,
% 66.84/66.91 (P3(a1,f9(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10410,10422,10392,10294,10298,1,40,13,19,20,18,27,28,15,3504,16,22,23,24,26])).
% 66.84/66.91 cnf(10457,plain,
% 66.84/66.91 (~P4(f6(a4),a4,a2)),
% 66.84/66.91 inference(scs_inference,[],[10341,10410,10422,10392,10294,10298,10337,38,1,40,13,19,20,18,27,28,15,3504,16,22,23,24,26,31])).
% 66.84/66.91 cnf(10459,plain,
% 66.84/66.91 (P4(a7,a2,a2)),
% 66.84/66.91 inference(scs_inference,[],[10341,10400,10410,10422,10392,10294,10298,10337,38,1,40,13,19,20,18,27,28,15,3504,16,22,23,24,26,31,30])).
% 66.84/66.91 cnf(10461,plain,
% 66.84/66.91 (P2(f3(a7,a7),f9(a4,a4),f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[10341,10400,10410,10302,10422,10392,10294,10298,10337,38,10353,1,40,13,19,20,18,27,28,15,3504,16,22,23,24,26,31,30,32])).
% 66.84/66.91 cnf(10463,plain,
% 66.84/66.91 (P2(f9(a4,a4),f3(a7,a7),f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[10341,10400,10410,10302,10422,10296,10392,10294,10298,10337,38,10353,1,40,13,19,20,18,27,28,15,3504,16,22,23,24,26,31,30,32,33])).
% 66.84/66.91 cnf(10465,plain,
% 66.84/66.91 (~P2(a1,a7,a2)),
% 66.84/66.91 inference(scs_inference,[],[10341,10400,10375,10410,10302,10422,10296,10392,10294,10298,10337,38,10353,355,1,40,13,19,20,18,27,28,15,3504,16,22,23,24,26,31,30,32,33,34])).
% 66.84/66.91 cnf(10474,plain,
% 66.84/66.91 (P1(f6(a2))),
% 66.84/66.91 inference(scs_inference,[],[3,13])).
% 66.84/66.91 cnf(10476,plain,
% 66.84/66.91 (P2(a4,f3(a1,a1),f3(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10443,3,13,19])).
% 66.84/66.91 cnf(10478,plain,
% 66.84/66.91 (P4(f6(a2),a2,a1)),
% 66.84/66.91 inference(scs_inference,[],[10443,3,13,19,20])).
% 66.84/66.91 cnf(10480,plain,
% 66.84/66.91 (P4(a1,f3(a1,a1),f3(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10443,3,13,19,20,18])).
% 66.84/66.91 cnf(10482,plain,
% 66.84/66.91 (P2(a4,f3(a5,a5),f3(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10443,10420,3,13,19,20,18,28])).
% 66.84/66.91 cnf(10484,plain,
% 66.84/66.91 (P4(a2,a7,a2)),
% 66.84/66.91 inference(scs_inference,[],[10459,10443,10420,3,13,19,20,18,28,27])).
% 66.84/66.91 cnf(10486,plain,
% 66.84/66.91 (P1(f3(a2,a2))),
% 66.84/66.91 inference(scs_inference,[],[10459,10443,10420,3,13,19,20,18,28,27,15])).
% 66.84/66.91 cnf(10488,plain,
% 66.84/66.91 (P4(a2,a2,f3(a2,a2))),
% 66.84/66.91 inference(scs_inference,[],[10459,10443,10420,3,13,19,20,18,28,27,15,22])).
% 66.84/66.91 cnf(10490,plain,
% 66.84/66.91 (P1(f9(a2,a2))),
% 66.84/66.91 inference(scs_inference,[],[10459,10443,10420,3,13,19,20,18,28,27,15,22,16])).
% 66.84/66.91 cnf(10492,plain,
% 66.84/66.91 (P2(a2,a2,f9(a2,a2))),
% 66.84/66.91 inference(scs_inference,[],[10459,10443,10420,3,13,19,20,18,28,27,15,22,16,23])).
% 66.84/66.91 cnf(10494,plain,
% 66.84/66.91 (P4(a1,a5,a5)),
% 66.84/66.91 inference(scs_inference,[],[10459,10443,10420,3,67,13,19,20,18,28,27,15,22,16,23,24])).
% 66.84/66.91 cnf(10496,plain,
% 66.84/66.91 (~P4(a7,a2,a1)),
% 66.84/66.91 inference(scs_inference,[],[10439,10459,10443,10420,38,3,67,13,19,20,18,28,27,15,22,16,23,24,31])).
% 66.84/66.91 cnf(10498,plain,
% 66.84/66.91 (P4(f6(a1),f3(a7,a7),f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[10439,10459,10300,10443,10420,10435,38,3,67,13,19,20,18,28,27,15,22,16,23,24,31,30])).
% 66.84/66.91 cnf(10500,plain,
% 66.84/66.91 (P2(a4,f9(a5,a5),f9(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10439,10459,10300,10443,10420,10408,10435,10255,38,3,67,13,19,20,18,28,27,15,22,16,23,24,31,30,32])).
% 66.84/66.91 cnf(10502,plain,
% 66.84/66.91 (P2(f3(a2,a2),a5,f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[7,10439,10459,10300,10443,10420,10408,10435,10255,38,10269,3,67,13,19,20,18,28,27,15,22,16,23,24,31,30,32,35])).
% 66.84/66.91 cnf(10504,plain,
% 66.84/66.91 (P4(f9(a1,a1),f9(a1,a1),f9(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[7,10439,10459,10300,10443,10420,10451,10408,10435,10277,10255,38,10269,3,67,13,19,20,18,28,27,15,22,16,23,24,31,30,32,35,34])).
% 66.84/66.91 cnf(10508,plain,
% 66.84/66.91 (P2(a10,a7,a4)),
% 66.84/66.91 inference(scs_inference,[],[7,10439,10459,10300,10443,10420,10451,10408,10435,10277,10255,10361,38,10269,3,3629,3722,67,13,19,20,18,28,27,15,22,16,23,24,31,30,32,35,34,913,33])).
% 66.84/66.91 cnf(10513,plain,
% 66.84/66.91 (P2(a4,f9(a1,a1),f9(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10447,19])).
% 66.84/66.91 cnf(10515,plain,
% 66.84/66.91 (P4(a1,f9(a1,a1),f9(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10447,19,18])).
% 66.84/66.91 cnf(10517,plain,
% 66.84/66.91 (P4(a5,a1,a5)),
% 66.84/66.91 inference(scs_inference,[],[10494,10447,19,18,27])).
% 66.84/66.91 cnf(10519,plain,
% 66.84/66.91 (P2(a7,a10,a4)),
% 66.84/66.91 inference(scs_inference,[],[10494,10508,10447,19,18,27,28])).
% 66.84/66.91 cnf(10521,plain,
% 66.84/66.91 (P3(f3(a2,a2),f3(a2,a2))),
% 66.84/66.91 inference(scs_inference,[],[10494,10508,10447,10488,19,18,27,28,82])).
% 66.84/66.91 cnf(10523,plain,
% 66.84/66.91 (P4(a1,a10,a10)),
% 66.84/66.91 inference(scs_inference,[],[10494,10508,10447,10488,77,19,18,27,28,82,24])).
% 66.84/66.91 cnf(10525,plain,
% 66.84/66.91 (P4(f3(a1,a1),a1,f3(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10494,10508,10449,10447,10480,10488,77,19,18,27,28,82,24,31])).
% 66.84/66.91 cnf(10527,plain,
% 66.84/66.91 (P4(a2,f3(a7,a7),a2)),
% 66.84/66.91 inference(scs_inference,[],[10484,10494,10508,10449,10447,10480,10488,10269,77,19,18,27,28,82,24,31,30])).
% 66.84/66.91 cnf(10529,plain,
% 66.84/66.91 (P2(f3(a10,a10),a7,f3(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10484,10494,10508,10308,10349,10449,10447,10480,10488,10269,77,19,18,27,28,82,24,31,30,35])).
% 66.84/66.91 cnf(10531,plain,
% 66.84/66.91 (P4(f9(a4,a4),f9(a4,a4),f3(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10484,10494,10508,10308,10349,10441,10449,10447,10480,10488,10353,10269,77,19,18,27,28,82,24,31,30,35,34])).
% 66.84/66.91 cnf(10538,plain,
% 66.84/66.91 (P2(a4,f8(a5),f8(a5))),
% 66.84/66.91 inference(scs_inference,[],[10314,19])).
% 66.84/66.91 cnf(10540,plain,
% 66.84/66.91 (P4(a1,f9(a10,a10),f9(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10310,10314,19,18])).
% 66.84/66.91 cnf(10542,plain,
% 66.84/66.91 (P4(a10,a1,a10)),
% 66.84/66.91 inference(scs_inference,[],[10523,10310,10314,19,18,27])).
% 66.84/66.91 cnf(10544,plain,
% 66.84/66.91 (P2(f9(a5,a5),a4,f9(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10523,10500,10310,10314,19,18,27,28])).
% 66.84/66.91 cnf(10546,plain,
% 66.84/66.91 (P4(a1,f3(a2,a2),f3(a2,a2))),
% 66.84/66.91 inference(scs_inference,[],[10523,10500,10521,10310,10314,19,18,27,28,24])).
% 66.84/66.91 cnf(10548,plain,
% 66.84/66.91 (~P4(a1,f6(a2),a7)),
% 66.84/66.91 inference(scs_inference,[],[10496,10523,10478,10500,10521,10310,10314,10277,19,18,27,28,24,31])).
% 66.84/66.91 cnf(10550,plain,
% 66.84/66.91 (P4(a1,f3(a7,a7),f3(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10496,10523,10478,10500,10521,10378,10310,10314,10414,10449,10277,19,18,27,28,24,31,30])).
% 66.84/66.91 cnf(10554,plain,
% 66.84/66.91 (P2(f3(a1,a1),a1,f9(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10496,10523,10504,10478,10500,10521,10378,10310,10314,10433,10414,10449,10277,10341,10451,199,19,18,27,28,24,31,30,34,35])).
% 66.84/66.91 cnf(10560,plain,
% 66.84/66.91 (P2(a4,f6(a4),f6(a4))),
% 66.84/66.91 inference(scs_inference,[],[10333,19])).
% 66.84/66.91 cnf(10562,plain,
% 66.84/66.91 (P4(a1,f9(a4,a4),f9(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10333,10347,19,18])).
% 66.84/66.91 cnf(10564,plain,
% 66.84/66.91 (P4(f3(a10,a10),a1,f3(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10355,10333,10347,19,18,27])).
% 66.84/66.91 cnf(10566,plain,
% 66.84/66.91 (P2(f9(a1,a1),a4,f9(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10355,10513,10333,10347,19,18,27,28])).
% 66.84/66.91 cnf(10570,plain,
% 66.84/66.91 (P4(f3(a5,a5),a1,f3(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10404,10355,10513,10515,10333,10347,10517,19,18,27,28,92,31])).
% 66.84/66.91 cnf(10572,plain,
% 66.84/66.91 (P4(a7,f3(a10,a10),f3(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10404,10355,10513,10515,10333,10347,10517,10400,19,18,27,28,92,31,30])).
% 66.84/66.91 cnf(10576,plain,
% 66.84/66.91 (~P2(a1,a7,f6(a4))),
% 66.84/66.91 inference(scs_inference,[],[10542,10373,10404,10355,10513,10515,10550,10333,10347,10517,10400,10508,40,19,18,27,28,92,31,30,29,34])).
% 66.84/66.91 cnf(10578,plain,
% 66.84/66.91 (P2(f3(a4,a4),f9(a1,a1),f9(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10542,10373,10404,10355,10513,10515,10550,10333,10347,10517,10504,10400,10349,10508,40,19,18,27,28,92,31,30,29,34,35])).
% 66.84/66.91 cnf(10584,plain,
% 66.84/66.91 (P2(a4,f6(a5),f6(a5))),
% 66.84/66.91 inference(scs_inference,[],[10390,19])).
% 66.84/66.91 cnf(10586,plain,
% 66.84/66.91 (P4(a1,f6(a5),f6(a5))),
% 66.84/66.91 inference(scs_inference,[],[10390,19,18])).
% 66.84/66.91 cnf(10588,plain,
% 66.84/66.91 (P4(f3(a4,a4),a1,f3(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10357,10390,19,18,27])).
% 66.84/66.91 cnf(10590,plain,
% 66.84/66.91 (P2(f9(a1,a1),f3(a4,a4),f9(a1,a1))),
% 66.84/66.91 inference(scs_inference,[],[10578,10357,10390,19,18,27,28])).
% 66.84/66.91 cnf(10592,plain,
% 66.84/66.91 (~P4(a2,f3(a7,a7),a1)),
% 66.84/66.91 inference(scs_inference,[],[10578,10357,10390,10527,10378,38,19,18,27,28,31])).
% 66.84/66.91 cnf(10594,plain,
% 66.84/66.91 (P4(f6(a4),f3(a7,a7),f6(a4))),
% 66.84/66.91 inference(scs_inference,[],[10578,10357,10385,10390,10527,10378,38,10269,19,18,27,28,31,30])).
% 66.84/66.91 cnf(10598,plain,
% 66.84/66.91 (P4(f9(a7,a7),f3(a4,a4),f3(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10578,10357,10385,10572,10562,10390,10527,10529,10378,10275,38,10269,40,19,18,27,28,31,30,29,34])).
% 66.84/66.91 cnf(10604,plain,
% 66.84/66.91 (P2(a4,f6(a1),f6(a1))),
% 66.84/66.91 inference(scs_inference,[],[10431,19])).
% 66.84/66.91 cnf(10606,plain,
% 66.84/66.91 (P4(a1,f9(a5,a5),f9(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10406,10431,19,18])).
% 66.84/66.91 cnf(10608,plain,
% 66.84/66.91 (P4(f3(a4,a4),f9(a7,a7),f3(a4,a4))),
% 66.84/66.91 inference(scs_inference,[],[10598,10406,10431,19,18,27])).
% 66.84/66.91 cnf(10610,plain,
% 66.84/66.91 (P2(a5,f3(a2,a2),f3(a7,a7))),
% 66.84/66.91 inference(scs_inference,[],[10598,10502,10406,10431,19,18,27,28])).
% 66.84/66.91 cnf(10612,plain,
% 66.84/66.91 (~P4(f6(a2),a2,a2)),
% 66.84/66.91 inference(scs_inference,[],[10412,10598,10502,10406,10431,10484,10478,19,18,27,28,31])).
% 66.84/66.91 cnf(10614,plain,
% 66.84/66.91 (P4(f6(a1),f3(a5,a5),f3(a5,a5))),
% 66.84/66.91 inference(scs_inference,[],[10412,10598,10453,10502,10406,10431,10484,10478,10435,19,18,27,28,31,30])).
% 66.84/66.91 cnf(10618,plain,
% 66.84/66.91 (P2(f3(a4,a4),a10,f3(a10,a10))),
% 66.84/66.91 inference(scs_inference,[],[10412,10598,10453,10502,10406,10431,10519,10484,10478,10322,10435,10529,6,19,18,27,28,31,30,21,33])).
% 66.84/66.91 cnf(10622,plain,
% 66.84/66.91 (P2(a4,f6(a2),f6(a2))),
% 66.84/66.91 inference(scs_inference,[],[10474,19])).
% 66.84/66.91 cnf(10624,plain,
% 66.84/66.91 (P4(a1,f6(a2),f6(a2))),
% 66.84/66.91 inference(scs_inference,[],[10474,19,18])).
% 66.84/66.92 cnf(10626,plain,
% 66.84/66.92 (P4(f9(a7,a7),a1,f9(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[10339,10474,19,18,27])).
% 66.84/66.92 cnf(10628,plain,
% 66.84/66.92 (P2(a10,f3(a4,a4),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[10339,10618,10474,19,18,27,28])).
% 66.84/66.92 cnf(10630,plain,
% 66.84/66.92 (P4(f3(a2,a2),a1,f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10339,10618,10474,10439,10488,19,18,27,28,31])).
% 66.84/66.92 cnf(10632,plain,
% 66.84/66.92 (P4(a7,f3(a2,a2),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10339,10618,10474,10439,10488,10459,19,18,27,28,31,30])).
% 66.84/66.92 cnf(10634,plain,
% 66.84/66.92 (P2(f9(a7,a7),a10,a7)),
% 66.84/66.92 inference(scs_inference,[],[10339,10618,10474,10439,10488,10519,10459,10275,286,19,18,27,28,31,30,33])).
% 66.84/66.92 cnf(10640,plain,
% 66.84/66.92 (P2(a4,f3(a2,a2),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10486,19])).
% 66.84/66.92 cnf(10642,plain,
% 66.84/66.92 (P4(a1,f9(a2,a2),f9(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10486,10490,19,18])).
% 66.84/66.92 cnf(10644,plain,
% 66.84/66.92 (P4(f3(a7,a7),f6(a4),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[10594,10486,10490,19,18,27])).
% 66.84/66.92 cnf(10646,plain,
% 66.84/66.92 (P2(f6(a4),a4,f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[10594,10486,10490,10560,19,18,27,28])).
% 66.84/66.92 cnf(10648,plain,
% 66.84/66.92 (~P4(f6(a7),f3(a7,a7),a2)),
% 66.84/66.92 inference(scs_inference,[],[10428,10594,10486,10490,10560,10285,10378,19,18,27,28,31])).
% 66.84/66.92 cnf(10650,plain,
% 66.84/66.92 (P4(f6(a7),f6(a4),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[10428,10594,10486,10490,10560,10386,10285,10378,19,18,27,28,31,30])).
% 66.84/66.92 cnf(10656,plain,
% 66.84/66.92 (~P2(f9(a1,a1),f3(a4,a4),a1)+P4(a1,a1,f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[10428,10455,10594,10486,10490,10560,10590,10386,10285,10515,10504,10378,19,18,27,28,31,30,24,29,34])).
% 66.84/66.92 cnf(10659,plain,
% 66.84/66.92 (P2(a4,f8(a2),f8(a2))),
% 66.84/66.92 inference(scs_inference,[],[10273,19])).
% 66.84/66.92 cnf(10661,plain,
% 66.84/66.92 (P4(a1,f8(a5),f8(a5))),
% 66.84/66.92 inference(scs_inference,[],[10273,10314,19,18])).
% 66.84/66.92 cnf(10665,plain,
% 66.84/66.92 (P2(f3(a2,a2),a4,f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10632,10640,10273,10314,19,18,27,28])).
% 66.84/66.92 cnf(10667,plain,
% 66.84/66.92 (~P4(f3(a7,a7),a1,a2)),
% 66.84/66.92 inference(scs_inference,[],[10457,10632,10640,10644,10273,10314,10337,19,18,27,28,31])).
% 66.84/66.92 cnf(10669,plain,
% 66.84/66.92 (P4(f6(a1),f6(a4),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[10457,10632,10640,10644,10498,10273,10314,10337,19,18,27,28,31,30])).
% 66.84/66.92 cnf(10673,plain,
% 66.84/66.92 (~P2(f6(a4),f8(a2),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[10457,10632,10640,10642,10644,10498,9097,10385,10273,10314,10337,10380,40,19,18,27,28,31,30,29,34])).
% 66.84/66.92 cnf(10675,plain,
% 66.84/66.92 (~P2(f8(a7),a7,a4)),
% 66.84/66.92 inference(scs_inference,[],[10457,10632,10640,10642,10644,10498,9097,10385,10273,10314,10337,10380,40,19,18,27,28,31,30,29,34,6440])).
% 66.84/66.92 cnf(10679,plain,
% 66.84/66.92 (P2(f8(a5),f3(a7,a7),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10457,10632,10640,10642,10644,10610,10498,9097,10385,10273,10314,10337,10380,10455,3722,40,19,18,27,28,31,30,29,34,6440,24,32])).
% 66.84/66.92 cnf(10681,plain,
% 66.84/66.92 (P2(f3(a2,a2),f9(a4,a4),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10457,10632,10640,10642,10644,10610,10498,10461,9097,10385,10273,10314,10337,10380,10455,3722,40,19,18,27,28,31,30,29,34,6440,24,32,33])).
% 66.84/66.92 cnf(10687,plain,
% 66.84/66.92 (P4(f9(a10,a10),a1,f9(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[10540,10490,19,27])).
% 66.84/66.92 cnf(10689,plain,
% 66.84/66.92 (P2(f9(a4,a4),f3(a2,a2),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10681,10540,10490,19,27,28])).
% 66.84/66.92 cnf(10693,plain,
% 66.84/66.92 (P4(f3(a2,a2),f3(a7,a7),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10681,10630,10540,10414,10490,19,27,28,92,31])).
% 66.84/66.92 cnf(10697,plain,
% 66.84/66.92 (P4(f6(a7),a1,a1)),
% 66.84/66.92 inference(scs_inference,[],[10681,10630,10540,10606,10650,10414,10490,10337,40,19,27,28,92,31,29,30])).
% 66.84/66.92 cnf(10699,plain,
% 66.84/66.92 (~P2(x106991,a2,a2)+P2(x106991,f9(a2,a2),f9(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10681,10492,10630,10540,10606,10650,10414,10490,10337,40,19,27,28,92,31,29,30,32])).
% 66.84/66.92 cnf(10701,plain,
% 66.84/66.92 (~P2(f6(a4),a10,a1)),
% 66.84/66.92 inference(scs_inference,[],[10681,10492,10646,10630,10540,10606,10650,10576,10414,10490,10337,10508,40,19,27,28,92,31,29,30,32,33])).
% 66.84/66.92 cnf(10703,plain,
% 66.84/66.92 (~P2(a1,a5,f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[10371,10681,10492,10646,10630,10540,10606,10650,10661,10576,10414,10490,10337,10508,3722,40,19,27,28,92,31,29,30,32,33,34])).
% 66.84/66.92 cnf(10707,plain,
% 66.84/66.92 (P2(a4,a1,a1)),
% 66.84/66.92 inference(scs_inference,[],[1,19])).
% 66.84/66.92 cnf(10709,plain,
% 66.84/66.92 (P4(f3(a7,a7),f3(a2,a2),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10693,1,19,27])).
% 66.84/66.92 cnf(10711,plain,
% 66.84/66.92 (P2(f6(a1),a4,f6(a1))),
% 66.84/66.92 inference(scs_inference,[],[10693,10604,1,19,27,28])).
% 66.84/66.92 cnf(10713,plain,
% 66.84/66.92 (~P4(f6(a1),a1,a4)),
% 66.84/66.92 inference(scs_inference,[],[10693,10669,10604,10371,10337,1,19,27,28,31])).
% 66.84/66.92 cnf(10715,plain,
% 66.84/66.92 (P4(f6(a7),f3(a2,a2),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10693,10546,10669,10604,10697,10371,10337,1,19,27,28,31,30])).
% 66.84/66.92 cnf(10717,plain,
% 66.84/66.92 (~P2(a7,a4,a2)),
% 66.84/66.92 inference(scs_inference,[],[10693,10546,10669,10604,10648,10697,10371,10302,10285,10337,3634,1,19,27,28,31,30,34])).
% 66.84/66.92 cnf(10726,plain,
% 66.84/66.92 (P2(a4,a2,a2)),
% 66.84/66.92 inference(scs_inference,[],[3,19])).
% 66.84/66.92 cnf(10728,plain,
% 66.84/66.92 (P4(f6(a5),a1,f6(a5))),
% 66.84/66.92 inference(scs_inference,[],[10586,3,19,27])).
% 66.84/66.92 cnf(10730,plain,
% 66.84/66.92 (P2(a1,a4,a1)),
% 66.84/66.92 inference(scs_inference,[],[10707,10586,3,19,27,28])).
% 66.84/66.92 cnf(10732,plain,
% 66.84/66.92 (~P4(f6(a7),f6(a2),a7)),
% 66.84/66.92 inference(scs_inference,[],[10707,10586,10624,10548,10697,3,19,27,28,31])).
% 66.84/66.92 cnf(10734,plain,
% 66.84/66.92 (P4(f6(a7),f6(a5),f6(a5))),
% 66.84/66.92 inference(scs_inference,[],[10707,10586,10624,10548,10697,3,19,27,28,31,30])).
% 66.84/66.92 cnf(10738,plain,
% 66.84/66.92 (~P2(f3(a4,a4),a1,a2)),
% 66.84/66.92 inference(scs_inference,[],[7,10707,10586,10624,10548,10703,10330,10697,10478,10385,10349,3,19,27,28,31,30,35,34])).
% 66.84/66.92 cnf(10744,plain,
% 66.84/66.92 (P4(f3(a2,a2),f6(a7),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10715,27])).
% 66.84/66.92 cnf(10746,plain,
% 66.84/66.92 (P2(a2,a4,a2)),
% 66.84/66.92 inference(scs_inference,[],[10726,10715,27,28])).
% 66.84/66.92 cnf(10750,plain,
% 66.84/66.92 (~P4(a1,f6(a1),a4)),
% 66.84/66.92 inference(scs_inference,[],[10726,10715,10734,10713,10263,8994,27,28,9459,31])).
% 66.84/66.92 cnf(10754,plain,
% 66.84/66.92 (P2(f3(a4,a4),f9(a4,a4),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[10726,10531,10715,10734,10713,10418,10263,10492,8994,10349,27,28,9459,31,33,35])).
% 66.84/66.92 cnf(10770,plain,
% 66.84/66.92 (P2(f9(a4,a4),f3(a4,a4),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[10754,10614,27,28])).
% 66.84/66.92 cnf(10772,plain,
% 66.84/66.92 (~P4(a1,f3(a7,a7),a2)),
% 66.84/66.92 inference(scs_inference,[],[10754,10667,10614,10300,10378,27,28,31])).
% 66.84/66.92 cnf(10776,plain,
% 66.84/66.92 (P2(a7,f3(a10,a10),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[10754,10667,10614,10628,10300,10396,10392,10378,10519,40,27,28,31,29,32])).
% 66.84/66.92 cnf(10778,plain,
% 66.84/66.92 (P2(f3(a10,a10),f9(a4,a4),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[10754,10667,10614,10628,10300,10396,10392,10378,10519,40,27,28,31,29,32,33])).
% 66.84/66.92 cnf(10785,plain,
% 66.84/66.92 (P4(f9(a4,a4),a1,f9(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[10562,27])).
% 66.84/66.92 cnf(10787,plain,
% 66.84/66.92 (P2(f9(a4,a4),f3(a10,a10),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[10778,10562,27,28])).
% 66.84/66.92 cnf(10789,plain,
% 66.84/66.92 (~P4(a1,a1,f6(a2))),
% 66.84/66.92 inference(scs_inference,[],[10778,10562,10612,10410,27,28,31])).
% 66.84/66.92 cnf(10791,plain,
% 66.84/66.92 (P4(f6(a1),f3(a2,a2),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10778,10709,10562,10612,10498,10410,27,28,31,30])).
% 66.84/66.92 cnf(10793,plain,
% 66.84/66.92 (P2(f9(a4,a4),f9(a1,a1),f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[10778,10770,10709,10562,10612,10578,10498,10410,27,28,31,30,32])).
% 66.84/66.92 cnf(10795,plain,
% 66.84/66.92 (P2(a7,f8(a5),a2)),
% 66.84/66.92 inference(scs_inference,[],[7,10746,10778,10770,10709,10562,10612,10578,10498,10410,3729,27,28,31,30,32,33])).
% 66.84/66.92 cnf(10806,plain,
% 66.84/66.92 (P2(f9(a1,a1),f9(a4,a4),f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[10793,10791,27,28])).
% 66.84/66.92 cnf(10812,plain,
% 66.84/66.92 (P4(f6(a10),f3(a10,a10),a10)),
% 66.84/66.92 inference(scs_inference,[],[10793,10791,10789,10523,10624,10298,10439,10308,10478,27,28,92,31,30])).
% 66.84/66.92 cnf(10814,plain,
% 66.84/66.92 (~P4(a1,f9(a1,a1),a5)),
% 66.84/66.92 inference(scs_inference,[],[10793,10791,10789,10523,10624,10298,10707,10439,10308,10341,10478,9105,10451,27,28,92,31,30,35])).
% 66.84/66.92 cnf(10816,plain,
% 66.84/66.92 (~P2(f3(a1,a1),a4,a2)),
% 66.84/66.92 inference(scs_inference,[],[10793,10791,10772,10789,10523,10624,10730,10550,10298,10707,10439,10308,10302,10341,10478,9105,10451,27,28,92,31,30,35,34])).
% 66.84/66.92 cnf(10823,plain,
% 66.84/66.92 (P4(f3(a10,a10),f6(a10),a10)),
% 66.84/66.92 inference(scs_inference,[],[10812,27])).
% 66.84/66.92 cnf(10825,plain,
% 66.84/66.92 (P2(f6(a5),a4,f6(a5))),
% 66.84/66.92 inference(scs_inference,[],[10584,10812,27,28])).
% 66.84/66.92 cnf(10827,plain,
% 66.84/66.92 (~P4(f6(a10),a10,a2)),
% 66.84/66.92 inference(scs_inference,[],[10445,10584,10812,27,28,31])).
% 66.84/66.92 cnf(10829,plain,
% 66.84/66.92 (P4(f6(a7),f3(a10,a10),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[10445,10584,10812,10572,10257,10355,27,28,31,30])).
% 66.84/66.92 cnf(10831,plain,
% 66.84/66.92 (P2(f9(a7,a7),f9(a10,a10),a4)),
% 66.84/66.92 inference(scs_inference,[],[10445,10584,10812,10634,10572,10257,10312,10355,10519,27,28,31,30,32])).
% 66.84/66.92 cnf(10835,plain,
% 66.84/66.92 (~P4(a10,a1,f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[10445,10584,10812,10634,10542,10572,10257,10312,10355,10730,10519,992,994,566,27,28,31,30,32,33,35])).
% 66.84/66.92 cnf(10841,plain,
% 66.84/66.92 (P4(f3(a10,a10),f6(a7),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[10829,27])).
% 66.84/66.92 cnf(10843,plain,
% 66.84/66.92 (P2(f6(a2),a4,f6(a2))),
% 66.84/66.92 inference(scs_inference,[],[10622,10829,27,28])).
% 66.84/66.92 cnf(10847,plain,
% 66.84/66.92 (P4(f6(a7),a10,a10)),
% 66.84/66.92 inference(scs_inference,[],[10622,10829,10823,10814,10515,10400,27,28,31,30])).
% 66.84/66.92 cnf(10855,plain,
% 66.84/66.92 (P4(a10,f6(a7),a10)),
% 66.84/66.92 inference(scs_inference,[],[10847,27])).
% 66.84/66.92 cnf(10857,plain,
% 66.84/66.92 (P2(f8(a5),a7,a2)),
% 66.84/66.92 inference(scs_inference,[],[10847,10795,27,28])).
% 66.84/66.92 cnf(10859,plain,
% 66.84/66.92 (~P4(f6(a7),a10,f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[10835,10847,10795,10542,27,28,31])).
% 66.84/66.92 cnf(10861,plain,
% 66.84/66.92 (P4(f6(a5),f3(a5,a5),a5)),
% 66.84/66.92 inference(scs_inference,[],[10835,10847,10795,10494,10542,10394,10404,27,28,31,30])).
% 66.84/66.92 cnf(10870,plain,
% 66.84/66.92 (P4(f3(a5,a5),f6(a5),a5)),
% 66.84/66.92 inference(scs_inference,[],[10861,27])).
% 66.84/66.92 cnf(10872,plain,
% 66.84/66.92 (P2(f3(a1,a1),a4,f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[10861,10476,27,28])).
% 66.84/66.92 cnf(10876,plain,
% 66.84/66.92 (~P4(f6(a7),a1,a2)),
% 66.84/66.92 inference(scs_inference,[],[10861,10476,10457,10661,10650,10337,40,27,28,29,31])).
% 66.84/66.92 cnf(10878,plain,
% 66.84/66.92 (P4(f6(a7),a5,a5)),
% 66.84/66.92 inference(scs_inference,[],[10861,10476,10457,10661,10650,10734,10337,40,27,28,29,31,30])).
% 66.84/66.92 cnf(10880,plain,
% 66.84/66.92 (P2(f9(a7,a7),f9(a10,a10),f9(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[10861,10476,10335,10457,10661,10831,10650,10734,10337,10353,40,27,28,29,31,30,33])).
% 66.84/66.92 cnf(10886,plain,
% 66.84/66.92 (P4(a5,f6(a7),a5)),
% 66.84/66.92 inference(scs_inference,[],[10878,27])).
% 66.84/66.92 cnf(10888,plain,
% 66.84/66.92 (P2(f9(a10,a10),f9(a7,a7),f9(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[10880,10878,27,28])).
% 66.84/66.92 cnf(10890,plain,
% 66.84/66.92 (~P4(a1,a2,a7)),
% 66.84/66.92 inference(scs_inference,[],[10880,10878,10375,10259,10459,27,28,31])).
% 66.84/66.92 cnf(10892,plain,
% 66.84/66.92 (P4(f6(a1),a5,a5)),
% 66.84/66.92 inference(scs_inference,[],[10880,10870,10878,10375,10614,10259,10459,27,28,31,30])).
% 66.84/66.92 cnf(10894,plain,
% 66.84/66.92 (P2(f9(a2,a2),f8(a2),a2)),
% 66.84/66.92 inference(scs_inference,[],[10880,10870,10878,10746,10375,10614,10259,10492,10459,3749,27,28,31,30,33])).
% 66.84/66.92 cnf(10896,plain,
% 66.84/66.92 (~P2(a5,a4,a1)),
% 66.84/66.92 inference(scs_inference,[],[10880,10870,10878,10746,10375,10614,10517,49,10259,10492,10730,10459,10261,3749,27,28,31,30,33,34])).
% 66.84/66.92 cnf(10898,plain,
% 66.84/66.92 (~P4(f6(a7),a5,a1)),
% 66.84/66.92 inference(scs_inference,[],[10880,10870,10878,10746,10375,10614,10517,49,10259,10492,10730,10459,10261,3749,27,28,31,30,33,34,9101])).
% 66.84/66.92 cnf(10907,plain,
% 66.84/66.92 (P4(a5,f6(a1),a5)),
% 66.84/66.92 inference(scs_inference,[],[10892,27])).
% 66.84/66.92 cnf(10909,plain,
% 66.84/66.92 (P2(f8(a2),f9(a2,a2),a2)),
% 66.84/66.92 inference(scs_inference,[],[10894,10892,27,28])).
% 66.84/66.92 cnf(10911,plain,
% 66.84/66.92 (~P4(f6(a1),a5,f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[10894,10886,10892,9099,27,28,31])).
% 66.84/66.92 cnf(10913,plain,
% 66.84/66.92 (~P4(f3(a7,a7),f6(a2),a1)),
% 66.84/66.92 inference(scs_inference,[],[10894,10886,10892,10789,9099,10624,10414,27,28,31,30])).
% 66.84/66.92 cnf(10922,plain,
% 66.84/66.92 (P4(f9(a2,a2),a1,f9(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[10642,27])).
% 66.84/66.92 cnf(10924,plain,
% 66.84/66.92 (P2(a1,f3(a1,a1),f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[10554,10642,27,28])).
% 66.84/66.92 cnf(10928,plain,
% 66.84/66.92 (P4(f6(a10),a10,f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[10855,10554,10642,10386,10371,10298,10337,9045,27,28,31,30])).
% 66.84/66.92 cnf(10930,plain,
% 66.84/66.92 (~P4(a5,f6(a1),a1)),
% 66.84/66.92 inference(scs_inference,[],[10896,10907,10855,10554,10642,10711,10386,10371,10298,10337,10261,9045,27,28,31,30,35])).
% 66.84/66.92 cnf(10932,plain,
% 66.84/66.92 (~P2(f6(a2),a4,a7)),
% 66.84/66.92 inference(scs_inference,[],[10896,10907,10855,10554,10642,10548,10711,10843,10386,10371,10298,10624,10730,10337,10261,9045,27,28,31,30,35,34])).
% 66.84/66.92 cnf(10939,plain,
% 66.84/66.92 (P4(a10,f6(a10),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[10928,27])).
% 66.84/66.92 cnf(10941,plain,
% 66.84/66.92 (P2(f8(a2),a4,f8(a2))),
% 66.84/66.92 inference(scs_inference,[],[10928,10659,27,28])).
% 66.84/66.92 cnf(10947,plain,
% 66.84/66.92 (P4(f6(a1),f3(a4,a4),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[10890,10928,10659,10357,10435,10361,10488,10478,27,28,3825,31,30])).
% 66.84/66.92 cnf(10949,plain,
% 66.84/66.92 (P2(a7,a10,f9(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[10890,10928,10659,10357,10880,10634,10435,10361,10312,10488,10478,27,28,3825,31,30,33])).
% 66.84/66.92 cnf(10951,plain,
% 66.84/66.92 (~P4(a1,f3(a1,a1),a2)),
% 66.84/66.92 inference(scs_inference,[],[10890,10816,10928,10872,10659,10357,10480,10880,10634,10435,10361,10312,10488,10478,10730,27,28,3825,31,30,33,35])).
% 66.84/66.92 cnf(10953,plain,
% 66.84/66.92 (~P2(f9(a1,a1),a4,a5)),
% 66.84/66.92 inference(scs_inference,[],[10890,10816,10928,10872,10566,10659,10357,10480,10814,10880,10634,10435,10361,10515,10312,10488,10478,10730,27,28,3825,31,30,33,35,34])).
% 66.84/66.92 cnf(10955,plain,
% 66.84/66.92 (~P2(f9(a7,a7),f3(a10,a10),x109551)+P2(f9(a10,a10),x109551,f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[10890,10888,10816,10928,10872,10787,10566,10659,10357,10480,10814,10880,10634,10435,10361,10515,10312,10488,10478,10730,27,28,3825,31,30,33,35,34,32])).
% 66.84/66.92 cnf(10961,plain,
% 66.84/66.92 (P2(a10,a7,f9(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[10947,10949,27,28])).
% 66.84/66.92 cnf(10963,plain,
% 66.84/66.92 (~P4(f3(a5,a5),f6(a5),a1)),
% 66.84/66.92 inference(scs_inference,[],[10947,10949,10728,10870,49,27,28,31])).
% 66.84/66.92 cnf(10965,plain,
% 66.84/66.92 (~P4(a7,a5,a7)),
% 66.84/66.92 inference(scs_inference,[],[10281,10947,10949,10728,10870,10257,10494,49,27,28,31,30])).
% 66.84/66.92 cnf(10967,plain,
% 66.84/66.92 (~P2(a5,a4,f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[10281,10947,10911,10949,10728,10870,10711,10892,10257,10494,49,10261,27,28,31,30,34])).
% 66.84/66.92 cnf(10974,plain,
% 66.84/66.92 (P4(f9(a5,a5),a1,f9(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[10606,27])).
% 66.84/66.92 cnf(10976,plain,
% 66.84/66.92 (P2(f8(a5),a4,f8(a5))),
% 66.84/66.92 inference(scs_inference,[],[10606,10538,27,28])).
% 66.84/66.92 cnf(10978,plain,
% 66.84/66.92 (~P4(a10,a5,a10)),
% 66.84/66.92 inference(scs_inference,[],[10898,10606,10928,10538,10298,27,28,31])).
% 66.84/66.92 cnf(10980,plain,
% 66.84/66.92 (P4(f6(a7),f6(a7),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[10898,10939,10606,10928,10538,10847,10298,27,28,31,30])).
% 66.84/66.92 cnf(10989,plain,
% 66.84/66.92 (P4(f3(a7,a7),a2,a2)),
% 66.84/66.92 inference(scs_inference,[],[10527,27])).
% 66.84/66.92 cnf(10991,plain,
% 66.84/66.92 (P2(f6(a10),a4,f6(a10))),
% 66.84/66.92 inference(scs_inference,[],[10527,10433,27,28])).
% 66.84/66.92 cnf(10995,plain,
% 66.84/66.92 (P4(f6(a7),f3(a5,a5),f3(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[10878,10527,10433,10612,10404,10459,27,28,31,30])).
% 66.84/66.92 cnf(10997,plain,
% 66.84/66.92 (P2(a2,a10,f8(a5))),
% 66.84/66.92 inference(scs_inference,[],[10976,10878,10527,10433,10612,10857,10404,10459,10519,27,28,31,30,33])).
% 66.84/66.92 cnf(10999,plain,
% 66.84/66.92 (~P4(f3(a1,a1),a1,a2)),
% 66.84/66.92 inference(scs_inference,[],[10976,10525,10816,10878,10872,10527,10433,10612,10857,10404,10459,10730,10519,27,28,31,30,33,35])).
% 66.84/66.92 cnf(11009,plain,
% 66.84/66.92 (P2(a10,a2,f8(a5))),
% 66.84/66.92 inference(scs_inference,[],[10995,10997,27,28])).
% 66.84/66.92 cnf(11011,plain,
% 66.84/66.92 (~P4(f6(a10),f3(a10,a10),f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[10995,10997,10564,10835,10812,27,28,31])).
% 66.84/66.92 cnf(11013,plain,
% 66.84/66.92 (~P4(f3(a7,a7),f3(a7,a7),a2)),
% 66.84/66.92 inference(scs_inference,[],[10995,10997,10564,10835,10812,10414,10,27,28,31,30])).
% 66.84/66.92 cnf(11015,plain,
% 66.84/66.92 (~P4(f3(a10,a10),f6(a10),f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[10995,10991,10997,10564,10823,10835,10812,10322,10414,10,994,27,28,31,30,35])).
% 66.84/66.92 cnf(11017,plain,
% 66.84/66.92 (~P2(f3(a4,a4),f3(a7,a7),a2)),
% 66.84/66.92 inference(scs_inference,[],[10995,10991,10997,10564,10463,10823,10835,10531,10812,10322,10414,10,994,27,28,31,30,35,34])).
% 66.84/66.92 cnf(11025,plain,
% 66.84/66.92 (P2(a10,f9(a7,a7),a7)),
% 66.84/66.92 inference(scs_inference,[],[10669,10634,27,28])).
% 66.84/66.92 cnf(11027,plain,
% 66.84/66.92 (~P4(f3(a1,a1),a2,a7)),
% 66.84/66.92 inference(scs_inference,[],[10989,10890,10669,10550,10634,27,28,30])).
% 66.84/66.92 cnf(11029,plain,
% 66.84/66.92 (~P4(f3(a7,a7),a2,a1)),
% 66.84/66.92 inference(scs_inference,[],[10592,10989,10890,10669,10550,10527,10634,27,28,30,31])).
% 66.84/66.92 cnf(11031,plain,
% 66.84/66.92 (~P2(f6(a1),a4,a4)),
% 66.84/66.92 inference(scs_inference,[],[10592,10989,10890,10713,10669,10263,10550,10527,10634,10711,10730,27,28,30,31,34])).
% 66.84/66.92 cnf(11033,plain,
% 66.84/66.92 (P2(f3(a4,a4),f6(a7),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[10592,10989,10980,10890,10713,10669,10263,10550,10527,10634,10711,10349,10730,128,27,28,30,31,34,35])).
% 66.84/66.92 cnf(11035,plain,
% 66.84/66.92 (P2(f9(a4,a4),f6(a7),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[10592,10989,10980,10890,10713,10770,10669,10263,10550,10527,10634,10711,10349,10730,128,27,28,30,31,34,35,32])).
% 66.84/66.92 cnf(11041,plain,
% 66.84/66.92 (P4(f6(a10),a1,f6(a10))),
% 66.84/66.92 inference(scs_inference,[],[10437,27])).
% 66.84/66.92 cnf(11043,plain,
% 66.84/66.92 (P2(f6(a7),f3(a4,a4),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11033,10437,27,28])).
% 66.84/66.92 cnf(11045,plain,
% 66.84/66.92 (~P4(f6(a7),a2,a1)),
% 66.84/66.92 inference(scs_inference,[],[11033,10496,10437,10989,10285,27,28,31])).
% 66.84/66.92 cnf(11047,plain,
% 66.84/66.92 (P4(f6(a7),a7,a7)),
% 66.84/66.92 inference(scs_inference,[],[11033,10496,10980,10437,10989,10285,27,28,31,30])).
% 66.84/66.92 cnf(11049,plain,
% 66.84/66.92 (~P2(f6(a7),a4,a2)),
% 66.84/66.92 inference(scs_inference,[],[10827,11033,10496,10980,10991,10437,10989,10928,10285,566,27,28,31,30,34])).
% 66.84/66.92 cnf(11055,plain,
% 66.84/66.92 (P4(a7,f6(a7),a7)),
% 66.84/66.92 inference(scs_inference,[],[11047,27])).
% 66.84/66.92 cnf(11057,plain,
% 66.84/66.92 (P2(f6(a7),f9(a4,a4),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11047,11035,27,28])).
% 66.84/66.92 cnf(11059,plain,
% 66.84/66.92 (P4(f6(a7),a2,a2)),
% 66.84/66.92 inference(scs_inference,[],[11047,11035,10459,27,28,30])).
% 66.84/66.92 cnf(11061,plain,
% 66.84/66.92 (~P4(a1,f6(a7),a2)),
% 66.84/66.92 inference(scs_inference,[],[11047,11035,10445,10523,10939,10459,27,28,30,31])).
% 66.84/66.92 cnf(11063,plain,
% 66.84/66.92 (~P4(f6(a7),a7,a2)),
% 66.84/66.92 inference(scs_inference,[],[10717,11047,11035,10445,10523,10939,10459,3634,286,27,28,30,31,35])).
% 66.84/66.92 cnf(11065,plain,
% 66.84/66.92 (~P2(a1,a4,f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[10717,11047,11035,10445,10523,10939,10279,10371,10316,10459,3634,286,27,28,30,31,35,34])).
% 66.84/66.92 cnf(11074,plain,
% 66.84/66.92 (P4(a2,f6(a7),a2)),
% 66.84/66.92 inference(scs_inference,[],[11059,27])).
% 66.84/66.92 cnf(11076,plain,
% 66.84/66.92 (P2(f3(a7,a7),f8(a5),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[11059,10679,27,28])).
% 66.84/66.92 cnf(11080,plain,
% 66.84/66.92 (P4(a10,f6(a10),a1)),
% 66.84/66.92 inference(scs_inference,[],[11015,11059,11041,10823,10572,10679,10939,10697,27,28,31,30])).
% 66.84/66.92 cnf(11082,plain,
% 66.84/66.92 (~P4(f3(a5,a5),f6(a5),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11015,10967,11059,11041,10825,10420,10870,10823,10572,10679,10939,10697,27,28,31,30,35])).
% 66.84/66.92 cnf(11084,plain,
% 66.84/66.92 (P4(f9(a1,a1),f3(a1,a1),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11015,10967,11059,11041,10825,10924,10476,10420,10870,10823,10572,10679,10939,10697,10316,27,28,31,30,35,34])).
% 66.84/66.92 cnf(11093,plain,
% 66.84/66.92 (P4(f3(a1,a1),f9(a1,a1),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11084,27])).
% 66.84/66.92 cnf(11095,plain,
% 66.84/66.92 (P2(f9(a10,a10),f9(a7,a7),a4)),
% 66.84/66.92 inference(scs_inference,[],[11084,10831,27,28])).
% 66.84/66.92 cnf(11097,plain,
% 66.84/66.92 (P4(f6(a7),f3(a7,a7),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11084,11047,10831,10269,27,28,30])).
% 66.84/66.92 cnf(11101,plain,
% 66.84/66.92 (P2(f8(a5),a5,f9(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[7,11084,11029,10961,11059,11009,11047,10831,10269,10478,27,28,30,31,33])).
% 66.84/66.92 cnf(11105,plain,
% 66.84/66.92 (P2(f3(a10,a10),f9(a7,a7),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[7,11084,11013,11029,11025,10961,11059,11009,11047,10308,10831,10610,10404,10269,10478,27,28,30,31,33,34,35])).
% 66.84/66.92 cnf(11111,plain,
% 66.84/66.92 (P4(f3(a7,a7),f6(a7),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11097,27])).
% 66.84/66.92 cnf(11113,plain,
% 66.84/66.92 (P2(f9(a7,a7),f3(a10,a10),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11105,11097,27,28])).
% 66.84/66.92 cnf(11115,plain,
% 66.84/66.92 (~P4(f9(a1,a1),f3(a1,a1),a2)),
% 66.84/66.92 inference(scs_inference,[],[11105,11097,10999,11084,10525,27,28,31])).
% 66.84/66.92 cnf(11117,plain,
% 66.84/66.92 (P4(a10,f6(a10),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11105,11097,10999,11080,11084,10525,11041,10449,27,28,31,30])).
% 66.84/66.92 cnf(11119,plain,
% 66.84/66.92 (~P2(a4,f3(a1,a1),a2)),
% 66.84/66.92 inference(scs_inference,[],[11105,11097,10999,11080,11084,10525,11041,10476,10924,10449,10316,27,28,31,30,34])).
% 66.84/66.92 cnf(11121,plain,
% 66.84/66.92 (~P4(a10,f6(a10),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[11105,11097,10999,11065,11080,11084,10525,11041,10991,10476,10924,10449,10316,566,27,28,31,30,34,35])).
% 66.84/66.92 cnf(11123,plain,
% 66.84/66.92 (P2(f9(a10,a10),f3(a7,a7),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11105,11097,10999,11065,11080,11084,10525,11041,10991,10476,10924,10449,10316,566,27,28,31,30,34,35,10955])).
% 66.84/66.92 cnf(11129,plain,
% 66.84/66.92 (P4(f6(a10),a10,f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11117,27])).
% 66.84/66.92 cnf(11131,plain,
% 66.84/66.92 (P2(f3(a7,a7),f9(a10,a10),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11123,11117,27,28])).
% 66.84/66.92 cnf(11133,plain,
% 66.84/66.92 (P4(a1,a7,f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11123,11117,11055,10382,9045,27,28,30])).
% 66.84/66.92 cnf(11137,plain,
% 66.84/66.92 (~P4(f3(a1,a1),f9(a1,a1),a2)),
% 66.84/66.92 inference(scs_inference,[],[11123,10913,11117,11119,11055,11097,10382,10476,10924,10257,10341,9045,27,28,30,31,35])).
% 66.84/66.92 cnf(11139,plain,
% 66.84/66.92 (~P2(f3(a1,a1),a4,f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[11123,10913,11117,11119,11121,11055,11097,10382,10991,10476,10924,10257,10341,9045,566,27,28,30,31,35,34])).
% 66.84/66.92 cnf(11145,plain,
% 66.84/66.92 (P4(a7,a1,f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11133,27])).
% 66.84/66.92 cnf(11147,plain,
% 66.84/66.92 (P2(a5,f8(a5),f9(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11101,11133,27,28])).
% 66.84/66.92 cnf(11153,plain,
% 66.84/66.92 (~P2(a2,a4,a1)),
% 66.84/66.92 inference(scs_inference,[],[10859,11045,11101,11129,11139,11133,11059,10746,10991,10939,3634,566,27,28,31,35,34])).
% 66.84/66.92 cnf(11162,plain,
% 66.84/66.92 (P4(f8(a5),a1,f8(a5))),
% 66.84/66.92 inference(scs_inference,[],[10661,27])).
% 66.84/66.92 cnf(11168,plain,
% 66.84/66.92 (P2(a2,f9(a4,a4),a2)),
% 66.84/66.92 inference(scs_inference,[],[7,10965,11063,11147,11145,11133,11074,10661,10795,27,31,34,32])).
% 66.84/66.92 cnf(11172,plain,
% 66.84/66.92 (P2(f9(a4,a4),a2,a2)),
% 66.84/66.92 inference(scs_inference,[],[7,10965,11063,11147,11145,11133,11074,10661,10795,1270,27,31,34,32,35,28])).
% 66.84/66.92 cnf(11178,plain,
% 66.84/66.92 (P2(f9(a4,a4),a7,a7)),
% 66.84/66.92 inference(scs_inference,[],[11172,10699,44])).
% 66.84/66.92 cnf(11182,plain,
% 66.84/66.92 (P2(f9(a2,a2),f9(a4,a4),f9(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[11172,10650,10699,44,27,28])).
% 66.84/66.92 cnf(11186,plain,
% 66.84/66.92 (P2(a10,f3(a7,a7),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11168,11172,11113,11025,10776,10650,10997,10699,44,27,28,6087,32])).
% 66.84/66.92 cnf(11188,plain,
% 66.84/66.92 (P2(f8(a5),f9(a4,a4),f8(a5))),
% 66.84/66.92 inference(scs_inference,[],[11168,11172,11113,11025,10776,10650,10997,11009,10699,44,27,28,6087,32,33])).
% 66.84/66.92 cnf(11194,plain,
% 66.84/66.92 (~P2(a2,f9(a4,a4),a1)),
% 66.84/66.92 inference(scs_inference,[],[11168,11172,10701,11113,10592,11025,10776,10461,10457,10650,10669,10997,11009,10385,10527,10337,10519,10699,44,27,28,6087,32,33,31,35,34])).
% 66.84/66.92 cnf(11198,plain,
% 66.84/66.92 (P2(a10,f9(a4,a4),a10)),
% 66.84/66.92 inference(scs_inference,[],[11168,11172,10701,11113,10592,11025,10776,10461,10457,10650,10669,10997,11009,10385,10527,10337,10519,10699,44,27,28,6087,32,33,31,35,34,3600,57])).
% 66.84/66.92 cnf(11206,plain,
% 66.84/66.92 (P4(f6(a5),f6(a7),f6(a5))),
% 66.84/66.92 inference(scs_inference,[],[10734,27])).
% 66.84/66.92 cnf(11208,plain,
% 66.84/66.92 (P2(a7,f9(a4,a4),a7)),
% 66.84/66.92 inference(scs_inference,[],[11178,10734,27,28])).
% 66.84/66.92 cnf(11212,plain,
% 66.84/66.92 (P2(f9(a4,a4),a10,a10)),
% 66.84/66.92 inference(scs_inference,[],[11178,11198,10961,10734,10949,27,28,32,33])).
% 66.84/66.92 cnf(11214,plain,
% 66.84/66.92 (~P4(a7,f6(a2),a7)),
% 66.84/66.92 inference(scs_inference,[],[11178,10732,11198,11145,10961,10734,10949,10624,27,28,32,33,31])).
% 66.84/66.92 cnf(11218,plain,
% 66.84/66.92 (~P2(a1,a1,a2)),
% 66.84/66.92 inference(scs_inference,[],[11153,11178,10732,11198,11145,10961,10734,11074,10949,10707,38,10624,10746,10316,3634,27,28,32,33,31,35,34])).
% 66.84/66.92 cnf(11224,plain,
% 66.84/66.92 (P4(f3(a7,a7),f6(a1),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[10498,27])).
% 66.84/66.92 cnf(11228,plain,
% 66.84/66.92 (P2(f9(a10,a10),f9(a4,a4),f9(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11186,11095,10320,10880,10498,27,28,32])).
% 66.84/66.92 cnf(11232,plain,
% 66.84/66.92 (~P4(a1,f3(a1,a1),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[11186,11095,10675,11121,10320,11117,10880,10498,10523,10275,27,28,32,33,31])).
% 66.84/66.92 cnf(11234,plain,
% 66.84/66.92 (~P4(f9(a1,a1),f3(a1,a1),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[11186,11095,10675,11139,11121,10320,10566,11084,11117,10872,10880,10498,10523,10275,27,28,32,33,31,35])).
% 66.84/66.92 cnf(11236,plain,
% 66.84/66.92 (P4(f3(a10,a10),a7,f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11186,11095,10608,10675,11139,11121,10320,10566,10618,11084,11117,10872,10880,10498,10523,10275,10634,27,28,32,33,31,35,34])).
% 66.84/66.92 cnf(11239,plain,
% 66.84/66.92 (P4(a5,f6(a5),a1)),
% 66.84/66.92 inference(scs_inference,[],[10394,27])).
% 66.84/66.92 cnf(11245,plain,
% 66.84/66.92 (P4(f6(a7),f3(a1,a1),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[7,11228,11208,10369,10847,11117,10394,27,28,32,30])).
% 66.84/66.92 cnf(11247,plain,
% 66.84/66.92 (P2(a4,f9(a4,a4),a4)),
% 66.84/66.92 inference(scs_inference,[],[7,11228,11208,10369,10847,11117,10394,10831,27,28,32,30,33])).
% 66.84/66.92 cnf(11251,plain,
% 66.84/66.92 (~P4(f9(a1,a1),f9(a1,a1),a2)),
% 66.84/66.92 inference(scs_inference,[],[7,11218,11228,11208,10930,10369,10907,10847,11117,10277,10394,10831,10451,27,28,32,30,33,31,35])).
% 66.84/66.92 cnf(11261,plain,
% 66.84/66.92 (P2(f9(a4,a4),a4,a4)),
% 66.84/66.92 inference(scs_inference,[],[11245,11247,27,28])).
% 66.84/66.92 cnf(11263,plain,
% 66.84/66.92 (P2(f9(a4,a4),f8(a5),f8(a5))),
% 66.84/66.92 inference(scs_inference,[],[11245,11247,11172,10997,27,28,32])).
% 66.84/66.92 cnf(11265,plain,
% 66.84/66.92 (P4(a7,f3(a1,a1),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11245,11247,10480,11145,11172,10997,27,28,32,30])).
% 66.84/66.92 cnf(11279,plain,
% 66.84/66.92 (P4(f3(a1,a1),a7,f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11265,27])).
% 66.84/66.92 cnf(11285,plain,
% 66.84/66.92 (P2(f9(a4,a4),f3(a5,a5),f3(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[11261,11263,11265,10482,11188,10795,10857,27,6087,3821,32])).
% 66.84/66.92 cnf(11287,plain,
% 66.84/66.92 (P4(a5,f6(a5),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11261,11263,11265,11206,11239,10482,11188,10795,10857,9045,27,6087,3821,32,30])).
% 66.84/66.92 cnf(11289,plain,
% 66.84/66.92 (P2(f3(a4,a4),a7,f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11261,11263,11265,11206,11239,10482,11105,11188,10529,10795,10275,10857,9045,27,6087,3821,32,30,33])).
% 66.84/66.92 cnf(11291,plain,
% 66.84/66.92 (~P4(a5,f6(a5),a2)),
% 66.84/66.92 inference(scs_inference,[],[11261,11061,11263,11265,11206,11239,10482,11105,11188,10529,10795,10275,10857,9045,27,6087,3821,32,30,33,31])).
% 66.84/66.92 cnf(11295,plain,
% 66.84/66.92 (~P2(a5,a4,f3(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[10367,10963,11261,11061,11263,11265,11206,11239,10482,11105,10825,11188,11055,10529,10795,10275,10857,10730,9045,3626,27,6087,3821,32,30,33,31,35,34])).
% 66.84/66.92 cnf(11297,plain,
% 66.84/66.92 (P2(f3(a5,a5),f9(a4,a4),f3(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[10367,10963,11261,11061,11263,11265,11206,11239,10482,11105,10825,11188,11055,10529,10795,10275,10857,10730,9045,3626,27,6087,3821,32,30,33,31,35,34,28])).
% 66.84/66.92 cnf(11303,plain,
% 66.84/66.92 (P4(f6(a5),a5,f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11287,27])).
% 66.84/66.92 cnf(11305,plain,
% 66.84/66.92 (P2(a7,f3(a4,a4),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11289,11287,27,28])).
% 66.84/66.92 cnf(11307,plain,
% 66.84/66.92 (P2(f8(a2),a2,f9(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11289,11287,11147,10795,10361,27,28,32])).
% 66.84/66.92 cnf(11309,plain,
% 66.84/66.92 (P4(f6(a1),f9(a7,a7),f9(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11289,11287,11147,10339,10435,10795,10361,27,28,32,30])).
% 66.84/66.92 cnf(11311,plain,
% 66.84/66.92 (P2(f9(a5,a5),f9(a4,a4),f9(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[11289,11287,10544,11247,11147,10339,10435,10795,10361,27,28,32,30,33])).
% 66.84/66.92 cnf(11313,plain,
% 66.84/66.92 (~P4(f3(a1,a1),a2,f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11289,11027,11287,10544,11247,11265,11147,10339,11055,10435,10795,10361,27,28,32,30,33,31])).
% 66.84/66.92 cnf(11315,plain,
% 66.84/66.92 (~P4(f6(a5),f3(a5,a5),f3(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[11289,11027,11287,11295,10544,11247,11265,11147,10825,10339,11055,10420,10861,10435,10795,10361,27,28,32,30,33,31,35])).
% 66.84/66.92 cnf(11327,plain,
% 66.84/66.92 (P2(f9(a4,a4),f6(a4),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[11311,11309,10560,11261,27,28,32])).
% 66.84/66.92 cnf(11329,plain,
% 66.84/66.92 (P4(f3(a1,a1),f3(a7,a7),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11311,11309,11279,10560,11261,10269,27,28,32,30])).
% 66.84/66.92 cnf(11331,plain,
% 66.84/66.92 (P2(f9(a4,a4),a5,a5)),
% 66.84/66.92 inference(scs_inference,[],[7,11311,11309,11307,11279,10560,11261,10361,10269,27,28,32,30,33])).
% 66.84/66.92 cnf(11333,plain,
% 66.84/66.92 (~P4(f6(a7),f6(a7),a2)),
% 66.84/66.92 inference(scs_inference,[],[7,11311,11309,11291,11307,11279,11287,10560,11261,10878,10361,10269,27,28,32,30,33,31])).
% 66.84/66.92 cnf(11342,plain,
% 66.84/66.92 (P4(f3(a7,a7),f3(a1,a1),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11329,27])).
% 66.84/66.92 cnf(11346,plain,
% 66.84/66.92 (P2(f9(a10,a10),a7,a10)),
% 66.84/66.92 inference(scs_inference,[],[11329,11212,11327,10888,10634,27,28,32])).
% 66.84/66.92 cnf(11348,plain,
% 66.84/66.92 (P4(f6(a1),f6(a7),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11329,11212,11327,10888,11287,10892,10634,27,28,32,30])).
% 66.84/66.92 cnf(11350,plain,
% 66.84/66.92 (P2(a2,f8(a2),f9(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11329,11212,11327,10888,11307,11287,10909,10894,10892,10634,27,28,32,30,33])).
% 66.84/66.92 cnf(11360,plain,
% 66.84/66.92 (P4(f6(a7),f6(a1),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11348,27])).
% 66.84/66.92 cnf(11362,plain,
% 66.84/66.92 (P2(a7,f9(a10,a10),a10)),
% 66.84/66.92 inference(scs_inference,[],[11348,11346,27,28])).
% 66.84/66.92 cnf(11364,plain,
% 66.84/66.92 (P2(f8(a2),f3(a2,a2),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11348,11346,11186,10679,8,27,28,32])).
% 66.84/66.92 cnf(11366,plain,
% 66.84/66.92 (P4(a7,f3(a7,a7),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11348,11346,11186,10300,10679,10400,8,27,28,32,30])).
% 66.84/66.92 cnf(11368,plain,
% 66.84/66.92 (P2(f9(a7,a7),f9(a4,a4),f9(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11348,11346,10318,11186,10300,11247,10679,10400,8,27,28,32,30,33])).
% 66.84/66.92 cnf(11370,plain,
% 66.84/66.92 (~P4(f6(a5),a5,a2)),
% 66.84/66.92 inference(scs_inference,[],[10876,11348,11346,10318,11303,11186,10300,10517,11247,10679,10400,8,27,28,32,30,33,31])).
% 66.84/66.92 cnf(11374,plain,
% 66.84/66.92 (~P2(f6(a7),f9(a4,a4),f6(a5))),
% 66.84/66.92 inference(scs_inference,[],[10465,11297,10876,11315,11348,11346,10318,11303,10995,11186,10300,10517,11247,10484,10679,10400,10337,355,8,27,28,32,30,33,31,35,34])).
% 66.84/66.92 cnf(11378,plain,
% 66.84/66.92 (P4(f3(a7,a7),a7,f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11366,27])).
% 66.84/66.92 cnf(11382,plain,
% 66.84/66.92 (P2(f9(a4,a4),f8(a2),f8(a2))),
% 66.84/66.92 inference(scs_inference,[],[11368,11366,10659,11261,27,28,32])).
% 66.84/66.92 cnf(11386,plain,
% 66.84/66.92 (~P4(a10,f6(a5),a10)),
% 66.84/66.92 inference(scs_inference,[],[11368,11366,11360,10978,10659,9097,11303,10855,11261,27,28,32,30,31])).
% 66.84/66.92 cnf(11388,plain,
% 66.84/66.92 (~P2(f6(a1),f9(a4,a4),f6(a5))),
% 66.84/66.92 inference(scs_inference,[],[11368,11366,11374,11360,10978,11057,10659,9097,11303,10855,10734,11261,27,28,32,30,31,35])).
% 66.84/66.92 cnf(11390,plain,
% 66.84/66.92 (P4(a10,f3(a10,a10),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11368,11366,11374,11360,11362,11131,10978,11057,10659,9097,11303,10855,10734,11261,27,28,32,30,31,35,34])).
% 66.84/66.92 cnf(11395,plain,
% 66.84/66.92 (P4(f3(a10,a10),a10,f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11390,27])).
% 66.84/66.92 cnf(11397,plain,
% 66.84/66.92 (P2(f3(a2,a2),f8(a2),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11364,11390,27,28])).
% 66.84/66.92 cnf(11399,plain,
% 66.84/66.92 (P2(f8(a2),f9(a4,a4),f8(a2))),
% 66.84/66.92 inference(scs_inference,[],[11364,11382,11390,11350,11307,27,28,32])).
% 66.84/66.92 cnf(11401,plain,
% 66.84/66.92 (~P4(f3(a1,a1),f3(a10,a10),f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[11364,11011,11382,11390,11350,11307,11129,27,28,32,30])).
% 66.84/66.92 cnf(11403,plain,
% 66.84/66.92 (P2(f6(a2),f9(a4,a4),f6(a2))),
% 66.84/66.92 inference(scs_inference,[],[11364,11011,11382,11390,11350,10843,11307,11129,11247,27,28,32,30,33])).
% 66.84/66.92 cnf(11405,plain,
% 66.84/66.92 (P4(f3(a1,a1),f6(a1),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11364,11011,11382,11390,11350,11224,11329,10843,11307,11129,11247,27,28,32,30,33,31])).
% 66.84/66.92 cnf(11407,plain,
% 66.84/66.92 (~P4(f6(a1),f6(a7),a2)),
% 66.84/66.92 inference(scs_inference,[],[11364,11011,11382,11390,11350,11049,11224,11329,11348,10843,11307,11129,11247,10711,3634,27,28,32,30,33,31,35])).
% 66.84/66.92 cnf(11409,plain,
% 66.84/66.92 (P4(f3(a2,a2),a2,f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[11364,11011,11378,11382,11390,11350,11049,11076,11224,11329,11348,10843,11307,11129,11247,10711,10795,3634,27,28,32,30,33,31,35,34])).
% 66.84/66.92 cnf(11413,plain,
% 66.84/66.92 (P4(f6(a1),f3(a1,a1),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11405,27])).
% 66.84/66.92 cnf(11415,plain,
% 66.84/66.92 (P2(f9(a4,a4),f6(a2),f6(a2))),
% 66.84/66.92 inference(scs_inference,[],[11405,11403,27,28])).
% 66.84/66.92 cnf(11417,plain,
% 66.84/66.92 (P4(f6(a1),f3(a10,a10),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11405,11403,11348,10829,27,28,30])).
% 66.84/66.92 cnf(11419,plain,
% 66.84/66.92 (~P2(f6(a7),f3(a2,a2),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[10673,11397,11405,11403,11043,11348,10829,27,28,30,33])).
% 66.84/66.92 cnf(11421,plain,
% 66.84/66.92 (~P4(f3(a10,a10),a1,f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[10673,11397,11405,11395,11403,11043,11015,11348,10829,11080,27,28,30,33,31])).
% 66.84/66.92 cnf(11428,plain,
% 66.84/66.92 (P4(f3(a10,a10),f6(a1),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11417,27])).
% 66.84/66.92 cnf(11430,plain,
% 66.84/66.92 (P2(a5,f9(a4,a4),a5)),
% 66.84/66.92 inference(scs_inference,[],[11417,11331,27,28])).
% 66.84/66.92 cnf(11432,plain,
% 66.84/66.92 (P4(f3(a2,a2),f3(a2,a2),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[11417,11409,11331,10488,27,28,30])).
% 66.84/66.92 cnf(11434,plain,
% 66.84/66.92 (P2(f3(a4,a4),a2,f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[11417,11409,11331,11397,10681,11307,10488,27,28,30,33])).
% 66.84/66.92 cnf(11436,plain,
% 66.84/66.92 (~P4(a7,f6(a5),a7)),
% 66.84/66.92 inference(scs_inference,[],[11417,11409,11331,10965,11397,10681,11303,11055,11307,10488,27,28,30,33,31])).
% 66.84/66.92 cnf(11438,plain,
% 66.84/66.92 (~P2(f3(a2,a2),f9(a4,a4),a7)),
% 66.84/66.92 inference(scs_inference,[],[11417,11409,11331,10965,11397,10681,10375,11168,11303,11055,11307,10488,27,28,30,33,31,34])).
% 66.84/66.92 cnf(11446,plain,
% 66.84/66.92 (P2(a2,f3(a4,a4),f3(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[11434,11409,27,28])).
% 66.84/66.92 cnf(11452,plain,
% 66.84/66.92 (P2(f6(a5),f9(a4,a4),f6(a5))),
% 66.84/66.92 inference(scs_inference,[],[10951,11419,11434,11342,11409,11043,10825,10550,11247,27,28,32,30,33])).
% 66.84/66.92 cnf(11456,plain,
% 66.84/66.92 (P4(f3(a4,a4),f9(a4,a4),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[10951,11419,11434,11413,11342,11137,11350,11093,11397,11409,11043,10825,10550,11247,27,28,32,30,33,31,34])).
% 66.84/66.92 cnf(11462,plain,
% 66.84/66.92 (P4(f9(a4,a4),f3(a4,a4),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11456,27])).
% 66.84/66.92 cnf(11464,plain,
% 66.84/66.92 (P2(f9(a4,a4),f6(a5),f6(a5))),
% 66.84/66.92 inference(scs_inference,[],[11456,11452,27,28])).
% 66.84/66.92 cnf(11466,plain,
% 66.84/66.92 (P2(f9(a4,a4),f6(a10),f6(a10))),
% 66.84/66.92 inference(scs_inference,[],[11456,11452,10433,11261,27,28,32])).
% 66.84/66.92 cnf(11468,plain,
% 66.84/66.92 (P4(f6(a1),a10,a10)),
% 66.84/66.92 inference(scs_inference,[],[11456,11452,11417,10433,10823,11261,27,28,32,30])).
% 66.84/66.92 cnf(11470,plain,
% 66.84/66.92 (~P4(f3(a10,a10),f6(a1),f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[11456,11428,11452,11421,11417,10433,10823,10263,11261,27,28,32,30,31])).
% 66.84/66.92 cnf(11472,plain,
% 66.84/66.92 (~P2(a5,f9(a4,a4),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11456,11082,11428,11452,11421,11417,11297,10433,10870,10823,10263,11261,27,28,32,30,31,34])).
% 66.84/66.92 cnf(11481,plain,
% 66.84/66.92 (P4(a10,f6(a1),a10)),
% 66.84/66.92 inference(scs_inference,[],[11468,27])).
% 66.84/66.92 cnf(11485,plain,
% 66.84/66.92 (P4(f3(a10,a10),f3(a7,a7),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11466,11468,11236,10269,27,28,30])).
% 66.84/66.92 cnf(11487,plain,
% 66.84/66.92 (~P4(f6(a2),f3(a7,a7),f6(a7))),
% 66.84/66.92 inference(scs_inference,[],[11466,11468,11236,11045,10989,10478,10269,27,28,30,31])).
% 66.84/66.92 cnf(11493,plain,
% 66.84/66.92 (~P4(f3(a2,a2),f3(a2,a2),a7)),
% 66.84/66.92 inference(scs_inference,[],[7,11432,11438,11466,11370,11468,11236,11045,11430,11452,10681,10909,10989,11303,10478,10269,27,28,30,31,34,32,35])).
% 66.84/66.92 cnf(11496,plain,
% 66.84/66.92 (P4(f3(a7,a7),f3(a10,a10),f3(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11485,27])).
% 66.84/66.92 cnf(11498,plain,
% 66.84/66.92 (P4(f6(a5),a5,f6(a1))),
% 66.84/66.92 inference(scs_inference,[],[11485,10907,10394,8994,27,30])).
% 66.84/66.92 cnf(11500,plain,
% 66.84/66.92 (~P4(f3(a10,a10),a10,f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[11485,11470,11481,11395,10907,10394,8994,27,30,31])).
% 66.84/66.92 cnf(11504,plain,
% 66.84/66.92 (~P2(f3(a4,a4),f6(a7),a2)),
% 66.84/66.92 inference(scs_inference,[],[11462,11485,11470,11333,11481,11395,11468,11033,11035,10907,10394,8994,10711,994,566,27,30,31,35,34])).
% 66.84/66.92 cnf(11509,plain,
% 66.84/66.92 (P4(a5,f6(a5),f6(a1))),
% 66.84/66.92 inference(scs_inference,[],[11498,27])).
% 66.84/66.92 cnf(11511,plain,
% 66.84/66.92 (P4(f3(a7,a7),a10,a10)),
% 66.84/66.92 inference(scs_inference,[],[11496,11498,10823,27,30])).
% 66.84/66.92 cnf(11513,plain,
% 66.84/66.92 (~P4(f3(a7,a7),f3(a10,a10),f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[11496,11500,11498,11395,10823,27,30,31])).
% 66.84/66.92 cnf(11515,plain,
% 66.84/66.92 (~P4(f9(a1,a1),f9(a1,a1),a5)),
% 66.84/66.92 inference(scs_inference,[],[11496,11500,10953,11498,11395,10566,10504,10823,27,30,31,35])).
% 66.84/66.92 cnf(11522,plain,
% 66.84/66.92 (P4(a10,f3(a7,a7),a10)),
% 66.84/66.92 inference(scs_inference,[],[11511,27])).
% 66.84/66.92 cnf(11526,plain,
% 66.84/66.92 (P4(f6(a7),f6(a1),f6(a1))),
% 66.84/66.92 inference(scs_inference,[],[11509,11511,10604,10878,11261,27,32,30])).
% 66.84/66.92 cnf(11528,plain,
% 66.84/66.92 (P2(a10,a5,f8(a2))),
% 66.84/66.92 inference(scs_inference,[],[11509,11511,11399,11101,10604,10878,11261,8,27,32,30,33])).
% 66.84/66.92 cnf(11530,plain,
% 66.84/66.92 (~P4(a7,f3(a10,a10),f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[11513,11509,11511,11399,11496,11366,11101,10604,10878,11261,8,27,32,30,33,31])).
% 66.84/66.92 cnf(11534,plain,
% 66.84/66.92 (~P2(f3(a2,a2),a4,a7)),
% 66.84/66.92 inference(scs_inference,[],[11513,11493,11509,11511,11031,10665,11399,11432,11496,11366,11101,10604,10878,10825,11261,10261,8,27,32,30,33,31,35,34])).
% 66.84/66.92 cnf(11536,plain,
% 66.84/66.92 (P2(f6(a1),f9(a4,a4),f6(a1))),
% 66.84/66.92 inference(scs_inference,[],[11513,11493,11509,11511,11031,10665,11399,11432,11496,11366,11101,10604,10878,10825,11261,10261,8,27,32,30,33,31,35,34,28])).
% 66.84/66.92 cnf(11543,plain,
% 66.84/66.92 (P4(f6(a1),f6(a7),f6(a1))),
% 66.84/66.92 inference(scs_inference,[],[11526,27])).
% 66.84/66.92 cnf(11547,plain,
% 66.84/66.92 (P2(f3(a1,a1),f9(a4,a4),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11526,11528,10872,11247,27,28,33])).
% 66.84/66.92 cnf(11549,plain,
% 66.84/66.92 (P4(f6(a1),f6(a1),f6(a1))),
% 66.84/66.92 inference(scs_inference,[],[11526,11528,10872,11348,11247,27,28,33,30])).
% 66.84/66.92 cnf(11561,plain,
% 66.84/66.92 (P4(f9(a1,a1),a1,f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[10515,27])).
% 66.84/66.92 cnf(11563,plain,
% 66.84/66.92 (P2(f9(a4,a4),f3(a1,a1),f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11547,10515,27,28])).
% 66.84/66.92 cnf(11565,plain,
% 66.84/66.92 (P4(f3(a7,a7),a1,a1)),
% 66.84/66.92 inference(scs_inference,[],[11547,11511,10515,11080,27,28,30])).
% 66.84/66.92 cnf(11569,plain,
% 66.84/66.92 (~P4(f6(a1),f6(a7),f6(a5))),
% 66.84/66.92 inference(scs_inference,[],[11547,11543,11549,11407,11388,11511,11536,11057,10515,11080,27,28,30,31,35])).
% 66.84/66.92 cnf(11571,plain,
% 66.84/66.92 (~P2(f3(a4,a4),f6(a5),a10)),
% 66.84/66.92 inference(scs_inference,[],[11547,11543,11549,11407,11386,11464,11388,11511,11536,11456,11057,10515,11080,27,28,30,31,35,34])).
% 66.84/66.92 cnf(11576,plain,
% 66.84/66.92 (P4(a1,f6(a7),a1)),
% 66.84/66.92 inference(scs_inference,[],[10697,27])).
% 66.84/66.92 cnf(11578,plain,
% 66.84/66.92 (P4(f3(a7,a7),a7,a1)),
% 66.84/66.92 inference(scs_inference,[],[11565,11378,10304,10697,27,30])).
% 66.84/66.92 cnf(11582,plain,
% 66.84/66.92 (~P2(f3(a4,a4),f9(a1,a1),a2)),
% 66.84/66.92 inference(scs_inference,[],[11251,11487,11565,11522,11378,10793,10578,10304,11456,10928,10697,27,30,31,34])).
% 66.84/66.92 cnf(11584,plain,
% 66.84/66.92 (~P4(f6(a5),f6(a5),a10)),
% 66.84/66.92 inference(scs_inference,[],[11251,11487,11571,11565,11522,11464,11378,10793,10578,10304,11456,10531,10928,10697,27,30,31,34,35])).
% 66.84/66.92 cnf(11590,plain,
% 66.84/66.92 (P4(a7,f3(a7,a7),a1)),
% 66.84/66.92 inference(scs_inference,[],[11578,27])).
% 66.84/66.92 cnf(11594,plain,
% 66.84/66.92 (P4(f9(a1,a1),f6(a7),f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11576,11561,11578,10835,11522,27,30,31])).
% 66.84/66.92 cnf(11604,plain,
% 66.84/66.92 (P4(f6(a7),f9(a1,a1),f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11594,27])).
% 66.84/66.92 cnf(11606,plain,
% 66.84/66.92 (P4(f3(a7,a7),f3(a4,a4),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11594,11565,10357,27,30])).
% 66.84/66.92 cnf(11608,plain,
% 66.84/66.92 (~P4(a7,f3(a1,a1),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[11232,11594,11590,11565,11342,10357,27,30,31])).
% 66.84/66.92 cnf(11618,plain,
% 66.84/66.92 (P4(f3(a4,a4),f3(a7,a7),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11606,27])).
% 66.84/66.92 cnf(11622,plain,
% 66.84/66.92 (~P4(f6(a7),f3(a1,a1),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[11606,11608,11029,11224,11578,11342,10285,27,30,31])).
% 66.84/66.92 cnf(11626,plain,
% 66.84/66.92 (P2(a1,f9(a4,a4),a1)),
% 66.84/66.92 inference(scs_inference,[],[11606,11115,11608,11029,11590,11563,11208,11224,11578,11342,10461,10562,10924,10285,27,30,31,34,35])).
% 66.84/66.92 cnf(11628,plain,
% 66.84/66.92 (P2(f9(a4,a4),a1,a1)),
% 66.84/66.92 inference(scs_inference,[],[11606,11115,11608,11029,11590,11563,11208,11224,11578,11342,10461,10562,10924,10285,27,30,31,34,35,28])).
% 66.84/66.92 cnf(11632,plain,
% 66.84/66.92 (P4(f3(a7,a7),a1,f3(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[10550,27])).
% 66.84/66.92 cnf(11634,plain,
% 66.84/66.92 (P4(a7,f3(a4,a4),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11606,11590,10357,10550,27,30])).
% 66.84/66.92 cnf(11636,plain,
% 66.84/66.92 (P4(f8(a5),f6(a7),f8(a5))),
% 66.84/66.92 inference(scs_inference,[],[11162,11606,11576,11590,10357,10550,27,30,31])).
% 66.84/66.92 cnf(11644,plain,
% 66.84/66.92 (P4(f3(a4,a4),a7,f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11634,27])).
% 66.84/66.92 cnf(11646,plain,
% 66.84/66.92 (P4(f6(a7),f3(a4,a4),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11634,11606,11097,27,30])).
% 66.84/66.92 cnf(11650,plain,
% 66.84/66.92 (~P2(f3(a10,a10),f9(a4,a4),f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[11313,11632,11634,11470,11428,10778,11606,11097,11536,10410,27,30,31,34])).
% 66.84/66.92 cnf(11658,plain,
% 66.84/66.92 (P4(f3(a7,a7),f3(a7,a7),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11636,11378,10269,27,30])).
% 66.84/66.92 cnf(11664,plain,
% 66.84/66.92 (~P4(f3(a10,a10),f6(a7),f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[11636,11650,11584,10841,10689,11493,11481,11509,11378,10778,10531,11057,10269,27,30,31,34,35])).
% 66.84/66.92 cnf(11675,plain,
% 66.84/66.92 (P4(f3(a4,a4),f6(a7),f3(a4,a4))),
% 66.84/66.92 inference(scs_inference,[],[11646,27])).
% 66.84/66.92 cnf(11677,plain,
% 66.84/66.92 (P4(f6(a7),f9(a7,a7),f9(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11646,11309,11526,27,30])).
% 66.84/66.92 cnf(11683,plain,
% 66.84/66.92 (P2(f9(a4,a4),a1,f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11658,11214,11646,11628,10785,10667,11632,11415,11309,11456,11526,10515,10451,27,30,31,34,35])).
% 66.84/66.92 cnf(11685,plain,
% 66.84/66.92 (P2(a1,f9(a4,a4),f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11658,11214,11646,11628,10785,10667,11632,11415,11309,11456,11526,10515,10451,27,30,31,34,35,28])).
% 66.84/66.92 cnf(11692,plain,
% 66.84/66.92 (P4(f3(a7,a7),f3(a5,a5),f3(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[11677,11683,11218,11565,11626,10453,27,33,30])).
% 66.84/66.92 cnf(11694,plain,
% 66.84/66.92 (~P4(f3(a10,a10),f3(a7,a7),f8(a7))),
% 66.84/66.92 inference(scs_inference,[],[11677,11664,11683,11218,11485,11111,11565,11626,10453,27,33,30,31])).
% 66.84/66.92 cnf(11702,plain,
% 66.84/66.92 (P4(f3(a5,a5),f3(a7,a7),f3(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[11692,27])).
% 66.84/66.92 cnf(11704,plain,
% 66.84/66.92 (P2(a1,a4,f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11692,11685,10353,10730,27,33])).
% 66.84/66.92 cnf(11710,plain,
% 66.84/66.92 (P4(f9(a2,a2),f9(a1,a1),f9(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[11692,11685,10922,11082,11584,11498,11182,11468,11509,10404,10353,10730,27,33,30,31,34])).
% 66.84/66.92 cnf(11714,plain,
% 66.84/66.92 (P2(a4,a1,f9(a1,a1))),
% 66.84/66.92 inference(scs_inference,[],[11692,11472,11685,10922,11082,11584,11498,11182,11468,11430,11509,10517,10404,10353,10730,27,33,30,31,34,35,28])).
% 66.84/66.92 cnf(11720,plain,
% 66.84/66.92 (P4(f9(a1,a1),f9(a2,a2),f9(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[11710,27])).
% 66.84/66.92 cnf(11724,plain,
% 66.84/66.92 (P4(f9(a2,a2),f6(a7),f9(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[11702,11710,11315,11594,10861,27,30,31])).
% 66.84/66.92 cnf(11726,plain,
% 66.84/66.92 (~P2(f3(a2,a2),f3(a4,a4),a7)),
% 66.84/66.92 inference(scs_inference,[],[11702,11710,11315,11594,11446,11493,10861,10488,27,30,31,34])).
% 66.84/66.92 cnf(11732,plain,
% 66.84/66.92 (P4(f6(a7),f9(a2,a2),f9(a2,a2))),
% 66.84/66.92 inference(scs_inference,[],[11724,27])).
% 66.84/66.92 cnf(11734,plain,
% 66.84/66.92 (P4(f3(a7,a7),f9(a10,a10),f9(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11724,10540,11565,27,30])).
% 66.84/66.92 cnf(11740,plain,
% 66.84/66.92 (~P4(f9(a1,a1),f3(a2,a2),a7)),
% 66.84/66.92 inference(scs_inference,[],[11724,11436,11704,10963,11534,11692,10546,11464,10540,11565,10665,10870,11456,27,30,31,34,35])).
% 66.84/66.92 cnf(11745,plain,
% 66.84/66.92 (~P4(a5,f3(a5,a5),f3(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[11734,11315,11498,10614,27,30])).
% 66.84/66.92 cnf(11749,plain,
% 66.84/66.92 (~P2(a4,a1,a2)),
% 66.84/66.92 inference(scs_inference,[],[11734,11714,11251,11370,11315,11498,10614,10586,10316,10451,27,30,31,34])).
% 66.84/66.92 cnf(11754,plain,
% 66.84/66.92 (P4(a7,f6(a7),a1)),
% 66.84/66.92 inference(scs_inference,[],[10257,27])).
% 66.84/66.92 cnf(11756,plain,
% 66.84/66.92 (P4(a7,f9(a10,a10),f9(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11734,11366,10257,27,30])).
% 66.84/66.92 cnf(11760,plain,
% 66.84/66.92 (P4(f9(a5,a5),f9(a1,a1),f9(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[10974,11734,11664,10841,11311,11390,11685,11366,10257,27,30,31,34])).
% 66.84/66.92 cnf(11764,plain,
% 66.84/66.92 (P4(f9(a1,a1),f9(a5,a5),f9(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[11760,27])).
% 66.84/66.92 cnf(11766,plain,
% 66.84/66.92 (P2(f9(a4,a4),f9(a1,a1),a1)),
% 66.84/66.92 inference(scs_inference,[],[11760,10416,11714,11628,27,32])).
% 66.84/66.92 cnf(11770,plain,
% 66.84/66.92 (P4(f6(a7),f9(a10,a10),f9(a10,a10))),
% 66.84/66.92 inference(scs_inference,[],[11760,11756,10416,10953,11714,11628,10554,11704,11047,27,32,33,30])).
% 66.84/66.92 cnf(11774,plain,
% 66.84/66.92 (~P2(f3(a1,a1),f9(a4,a4),f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[11760,11234,10750,11756,11754,10416,10953,11714,11628,10806,10554,11704,11360,11084,11547,11047,27,32,33,30,31,34])).
% 66.84/66.92 cnf(11778,plain,
% 66.84/66.92 (P2(f9(a1,a1),f9(a4,a4),a1)),
% 66.84/66.92 inference(scs_inference,[],[11760,11234,10750,11756,11504,11754,11675,10416,10953,11714,11628,10806,10554,11704,11033,11360,11084,11547,11047,11059,27,32,33,30,31,34,35,28])).
% 66.84/66.92 cnf(11786,plain,
% 66.84/66.92 (P2(a1,f3(a4,a4),a1)),
% 66.84/66.92 inference(scs_inference,[],[11770,11766,11194,10590,11350,27,32,33])).
% 66.84/66.92 cnf(11788,plain,
% 66.84/66.92 (P4(f6(a7),f9(a5,a5),f9(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[11764,11770,11766,11194,11604,10590,11350,27,32,33,30])).
% 66.84/66.92 cnf(11790,plain,
% 66.84/66.92 (~P4(f3(a7,a7),f3(a7,a7),a5)),
% 66.84/66.92 inference(scs_inference,[],[11764,11770,11745,11766,11194,11604,10590,11692,11350,27,32,33,30,31])).
% 66.84/66.92 cnf(11792,plain,
% 66.84/66.92 (P2(a1,f3(a4,a4),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11764,11770,11745,11766,11194,11604,11754,11305,10590,11692,11111,11350,11043,27,32,33,30,31,35])).
% 66.84/66.92 cnf(11796,plain,
% 66.84/66.92 (P2(f3(a4,a4),a1,a1)),
% 66.84/66.92 inference(scs_inference,[],[11764,11770,11745,11766,11194,11604,11754,11285,11305,10590,11692,11111,11350,11043,10562,27,32,33,30,31,35,34,28])).
% 66.84/66.92 cnf(11801,plain,
% 66.84/66.92 (P2(f3(a4,a4),a1,f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11788,11792,27,28])).
% 66.84/66.92 cnf(11803,plain,
% 66.84/66.92 (P2(f3(a4,a4),f3(a7,a7),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11788,11796,11792,27,28,32])).
% 66.84/66.92 cnf(11805,plain,
% 66.84/66.92 (P2(f3(a7,a7),f3(a4,a4),f3(a7,a7))),
% 66.84/66.92 inference(scs_inference,[],[11788,11796,11792,11786,27,28,32,33])).
% 66.84/66.92 cnf(11807,plain,
% 66.84/66.92 (P4(a7,f9(a5,a5),f9(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[11788,11796,11792,11786,11754,10606,27,28,32,33,30])).
% 66.84/66.92 cnf(11811,plain,
% 66.84/66.92 (~P4(a1,a1,f6(a4))),
% 66.84/66.92 inference(scs_inference,[],[11774,11788,11796,11792,11786,11421,10564,11754,11417,10606,11626,10449,27,28,32,33,30,31,35])).
% 66.84/66.92 cnf(11813,plain,
% 66.84/66.92 (P4(f9(a1,a1),f8(a2),f8(a2))),
% 66.84/66.92 inference(scs_inference,[],[11774,11788,11796,11792,11786,10941,11421,10564,11754,11417,10606,11704,11626,10449,10396,27,28,32,33,30,31,35,34])).
% 66.84/66.92 cnf(11819,plain,
% 66.84/66.92 (P4(f9(a5,a5),a7,f9(a5,a5))),
% 66.84/66.92 inference(scs_inference,[],[11807,27])).
% 66.84/66.92 cnf(11821,plain,
% 66.84/66.93 (P2(f3(a4,a4),f3(a10,a10),f3(a10,a10))),
% 66.84/66.93 inference(scs_inference,[],[11803,11807,11131,27,32])).
% 66.84/66.93 cnf(11823,plain,
% 66.84/66.93 (P2(f3(a10,a10),f3(a4,a4),f3(a10,a10))),
% 66.84/66.93 inference(scs_inference,[],[11803,11805,11807,11123,11131,27,32,33])).
% 66.84/66.93 cnf(11831,plain,
% 66.84/66.93 (P4(f9(a7,a7),f9(a1,a1),f9(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11803,11805,11807,11813,11017,11646,11604,10785,10626,11368,11123,11131,11576,11685,10527,27,32,33,30,31,35,34])).
% 66.84/66.93 cnf(11837,plain,
% 66.84/66.93 (P4(f9(a1,a1),f9(a7,a7),f9(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11831,27])).
% 66.84/66.93 cnf(11839,plain,
% 66.84/66.93 (P2(f9(a1,a1),f3(a4,a4),a1)),
% 66.84/66.93 inference(scs_inference,[],[11831,11778,11786,10770,27,32])).
% 66.84/66.93 cnf(11841,plain,
% 66.84/66.93 (P2(f9(a1,a1),f9(a4,a4),f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11831,11778,11801,11786,10770,10578,27,32,33])).
% 66.84/66.93 cnf(11843,plain,
% 66.84/66.93 (P4(f9(a5,a5),f3(a7,a7),f9(a5,a5))),
% 66.84/66.93 inference(scs_inference,[],[11831,11819,11778,11801,11786,10770,10578,10269,27,32,33,30])).
% 66.84/66.93 cnf(11849,plain,
% 66.84/66.93 (~P2(f3(a4,a4),f3(a10,a10),f8(a7))),
% 66.84/66.93 inference(scs_inference,[],[11821,11831,10738,11694,11819,11778,11801,11644,11530,11786,10608,11113,10770,11496,10578,10989,10285,10269,27,32,33,30,31,35,34])).
% 66.84/66.93 cnf(11851,plain,
% 66.84/66.93 (P4(a1,a1,f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[11821,11831,10738,11694,11819,11778,11801,11644,11530,11786,10608,11113,10770,11496,10578,10989,10285,10269,27,32,33,30,31,35,34,10656])).
% 66.84/66.93 cnf(11852,plain,
% 66.84/66.93 (P2(f3(a4,a4),f9(a1,a1),a1)),
% 66.84/66.93 inference(scs_inference,[],[11821,11831,10738,11694,11819,11778,11801,11644,11530,11786,10608,11113,10770,11496,10578,10989,10285,10269,27,32,33,30,31,35,34,10656,28])).
% 66.84/66.93 cnf(11857,plain,
% 66.84/66.93 (P2(f9(a4,a4),f9(a1,a1),f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11841,11843,27,28])).
% 66.84/66.93 cnf(11859,plain,
% 66.84/66.93 (P2(a1,f9(a4,a4),f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11841,11843,11852,11803,27,28,33])).
% 66.84/66.93 cnf(11861,plain,
% 66.84/66.93 (P4(f3(a4,a4),f9(a1,a1),f3(a4,a4))),
% 66.84/66.93 inference(scs_inference,[],[11841,11843,11851,11852,10588,11803,27,28,33,30])).
% 66.84/66.93 cnf(11865,plain,
% 66.84/66.93 (~P2(f3(a7,a7),f9(a1,a1),a2)),
% 66.84/66.93 inference(scs_inference,[],[11841,11843,11851,11582,11852,11618,10588,11803,11224,10410,27,28,33,30,31,35])).
% 66.84/66.93 cnf(11870,plain,
% 66.84/66.93 (P2(f9(a4,a4),a1,f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11859,28])).
% 66.84/66.93 cnf(11872,plain,
% 66.84/66.93 (P4(f9(a1,a1),f3(a4,a4),f3(a4,a4))),
% 66.84/66.93 inference(scs_inference,[],[11861,11859,28,27])).
% 66.84/66.93 cnf(11874,plain,
% 66.84/66.93 (P4(f3(a7,a7),f9(a1,a1),f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[11861,11859,11851,11565,28,27,30])).
% 66.84/66.93 cnf(11876,plain,
% 66.84/66.93 (P2(f3(a4,a4),f3(a4,a4),f3(a4,a4))),
% 66.84/66.93 inference(scs_inference,[],[11823,11861,11859,11851,10776,11565,28,27,30,33])).
% 66.84/66.93 cnf(11878,plain,
% 66.84/66.93 (~P4(a1,f3(a2,a2),a7)),
% 66.84/66.93 inference(scs_inference,[],[11823,11861,11740,11859,11851,10546,10776,11565,28,27,30,33,31])).
% 66.84/66.93 cnf(11882,plain,
% 66.84/66.93 (~P2(f3(a10,a10),f3(a4,a4),f8(a7))),
% 66.84/66.93 inference(scs_inference,[],[11823,11861,11740,11849,11859,10398,11851,10546,10776,10628,11390,11565,10349,28,27,30,33,31,35,34])).
% 66.84/66.93 cnf(11886,plain,
% 66.84/66.93 (P4(f9(a1,a1),f3(a7,a7),f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[11874,27])).
% 66.84/66.93 cnf(11888,plain,
% 66.84/66.93 (P2(f3(a7,a7),f3(a4,a4),f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[11874,11857,11839,11683,27,33])).
% 66.84/66.93 cnf(11890,plain,
% 66.84/66.93 (P4(f3(a7,a7),f9(a7,a7),f9(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11874,11837,11857,11839,11683,27,33,30])).
% 66.84/66.93 cnf(11892,plain,
% 66.84/66.93 (P2(f3(a4,a4),f3(a2,a2),f3(a2,a2))),
% 66.84/66.93 inference(scs_inference,[],[11874,11876,11837,11857,11839,11683,11434,27,33,30,32])).
% 66.84/66.93 cnf(11900,plain,
% 66.84/66.93 (P2(f3(a4,a4),f3(a7,a7),f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[11874,11876,11790,11878,11837,10932,11857,11839,11805,11658,10709,11683,11434,10843,11590,11704,10624,27,33,30,32,31,35,34,28])).
% 66.84/66.93 cnf(11906,plain,
% 66.84/66.93 (P2(f3(a2,a2),f3(a4,a4),f3(a2,a2))),
% 66.84/66.93 inference(scs_inference,[],[11892,28])).
% 66.84/66.93 cnf(11910,plain,
% 66.84/66.93 (P4(a7,f9(a2,a2),f9(a2,a2))),
% 66.84/66.93 inference(scs_inference,[],[11890,11892,11732,10642,11754,28,27,30])).
% 66.84/66.93 cnf(11914,plain,
% 66.84/66.93 (~P2(f9(a1,a1),f3(a7,a7),a2)),
% 66.84/66.93 inference(scs_inference,[],[11888,11890,11892,11900,11865,11732,11857,11859,10642,11754,28,27,30,33,32])).
% 66.84/66.93 cnf(11916,plain,
% 66.84/66.93 (P4(f9(a1,a1),a1,f3(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[11886,11888,11890,11892,11900,11865,11732,11857,11859,11632,10642,11754,11084,28,27,30,33,32,31])).
% 66.84/66.93 cnf(11929,plain,
% 66.84/66.93 (P4(f3(a7,a7),f9(a2,a2),f9(a2,a2))),
% 66.84/66.93 inference(scs_inference,[],[11910,11720,11874,27,30])).
% 66.84/66.93 cnf(11931,plain,
% 66.84/66.93 (P2(f3(a7,a7),f3(a4,a4),a1)),
% 66.84/66.93 inference(scs_inference,[],[11910,11720,11888,11876,11839,11874,27,30,32])).
% 66.84/66.93 cnf(11935,plain,
% 66.84/66.93 (P2(f3(a1,a1),f3(a4,a4),f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[11401,11910,11916,11720,11888,11876,11839,11874,11786,11851,10355,27,30,32,31,35])).
% 66.84/66.93 cnf(11939,plain,
% 66.84/66.93 (P2(f3(a4,a4),f3(a7,a7),a1)),
% 66.84/66.93 inference(scs_inference,[],[11401,11870,11910,11916,11720,11888,11790,11876,11839,11874,11786,11801,11851,10355,11456,27,30,32,31,35,34,28])).
% 66.84/66.93 cnf(11942,plain,
% 66.84/66.93 (P2(f3(a4,a4),f3(a1,a1),f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[11935,28])).
% 66.84/66.93 cnf(11946,plain,
% 66.84/66.93 (P2(f9(a1,a1),f3(a7,a7),f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[11929,11935,11939,10554,28,27,33])).
% 66.84/66.93 cnf(11948,plain,
% 66.84/66.93 (P4(f9(a10,a10),f9(a1,a1),f9(a10,a10))),
% 66.84/66.93 inference(scs_inference,[],[11929,11935,11939,10687,10554,11851,28,27,33,30])).
% 66.84/66.93 cnf(11952,plain,
% 66.84/66.93 (P4(f9(a1,a1),a1,a1)),
% 66.84/66.93 inference(scs_inference,[],[11929,11935,11939,11872,10687,10898,10554,11145,10494,11851,28,27,33,30,31,34])).
% 66.84/66.93 cnf(11962,plain,
% 66.84/66.93 (P2(f3(a4,a4),f3(a1,a1),a1)),
% 66.84/66.93 inference(scs_inference,[],[11942,11946,11948,11852,11876,28,27,33])).
% 66.84/66.93 cnf(11964,plain,
% 66.84/66.93 (P4(f9(a1,a1),f6(a7),f6(a7))),
% 66.84/66.93 inference(scs_inference,[],[11942,11946,11948,11952,11852,11133,11876,28,27,33,30])).
% 66.84/66.93 cnf(11966,plain,
% 66.84/66.93 (~P4(a5,f6(a5),f6(a5))),
% 66.84/66.93 inference(scs_inference,[],[11942,11946,11948,11569,11952,11852,11206,11133,11876,11509,28,27,33,30,31])).
% 66.84/66.93 cnf(11970,plain,
% 66.84/66.93 (~P2(f3(a7,a7),f3(a4,a4),f6(a4))),
% 66.84/66.93 inference(scs_inference,[],[11942,11946,11948,11882,11931,11569,11952,11811,11888,11823,11852,11658,11485,11206,11133,11876,11509,28,27,33,30,31,35,34])).
% 66.84/66.93 cnf(11974,plain,
% 66.84/66.93 (P2(f3(a1,a1),f3(a4,a4),a1)),
% 66.84/66.93 inference(scs_inference,[],[11962,28])).
% 66.84/66.93 cnf(11976,plain,
% 66.84/66.93 (P4(f6(a7),f9(a1,a1),f6(a7))),
% 66.84/66.93 inference(scs_inference,[],[11962,11964,28,27])).
% 66.84/66.93 cnf(11978,plain,
% 66.84/66.93 (P4(f9(a1,a1),f3(a2,a2),f3(a2,a2))),
% 66.84/66.93 inference(scs_inference,[],[11962,11964,10715,28,27,30])).
% 66.84/66.93 cnf(11980,plain,
% 66.84/66.93 (P2(f3(a7,a7),f3(a7,a7),f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11962,11964,11946,10715,11857,28,27,30,33])).
% 66.84/66.93 cnf(11991,plain,
% 66.84/66.93 (P4(f3(a2,a2),f9(a1,a1),f3(a2,a2))),
% 66.84/66.93 inference(scs_inference,[],[11978,27])).
% 66.84/66.93 cnf(11995,plain,
% 66.84/66.93 (P4(f3(a5,a5),f9(a1,a1),f3(a5,a5))),
% 66.84/66.93 inference(scs_inference,[],[11978,10570,11821,11900,11105,11851,27,33,30])).
% 66.84/66.93 cnf(11997,plain,
% 66.84/66.93 (P2(f3(a1,a1),f3(a4,a4),f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11978,11974,10570,11821,11900,11859,11105,10754,11851,27,33,30,32])).
% 66.84/66.93 cnf(12001,plain,
% 66.84/66.93 (~P4(f3(a2,a2),f6(a7),a7)),
% 66.84/66.93 inference(scs_inference,[],[11978,11726,11974,11976,11906,10744,10570,11515,11821,11900,11859,11594,11105,10754,11043,11851,27,33,30,32,31,35])).
% 66.84/66.93 cnf(12005,plain,
% 66.84/66.93 (P2(f9(a7,a7),f3(a10,a10),f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[11978,11726,11974,11976,11966,11906,10744,10570,11515,11821,11900,11859,11594,11105,10754,11464,11043,11851,10562,27,33,30,32,31,35,34,28])).
% 66.84/66.93 cnf(12007,plain,
% 66.84/66.93 (P2(f9(a10,a10),f9(a1,a1),f3(a10,a10))),
% 66.84/66.93 inference(scs_inference,[],[11978,11726,11974,11976,11966,11906,10744,10570,11515,11821,11900,11859,11594,11105,10754,11464,11043,11851,10562,27,33,30,32,31,35,34,28,10955])).
% 66.84/66.93 cnf(12010,plain,
% 66.84/66.93 (P2(f3(a4,a4),f3(a1,a1),f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11997,28])).
% 66.84/66.93 cnf(12012,plain,
% 66.84/66.93 (P4(f9(a1,a1),f3(a5,a5),f3(a5,a5))),
% 66.84/66.93 inference(scs_inference,[],[11995,11997,28,27])).
% 66.84/66.93 cnf(12014,plain,
% 66.84/66.93 (P2(f3(a7,a7),a1,f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[11980,11995,11997,11870,10461,28,27,33])).
% 66.84/66.93 cnf(12016,plain,
% 66.84/66.93 (P4(f9(a1,a1),f6(a10),f6(a10))),
% 66.84/66.93 inference(scs_inference,[],[11980,11995,11997,11870,11952,10437,10461,28,27,33,30])).
% 66.84/66.93 cnf(12018,plain,
% 66.84/66.93 (P2(f3(a7,a7),a1,a1)),
% 66.84/66.93 inference(scs_inference,[],[11980,11995,11997,11870,11931,11952,10437,10461,28,27,33,30,32])).
% 66.84/66.93 cnf(12024,plain,
% 66.84/66.93 (P4(f3(a7,a7),f9(a4,a4),f9(a4,a4))),
% 66.84/66.93 inference(scs_inference,[],[11980,11991,11995,11997,11970,12001,11870,10418,11931,11952,11305,10437,11859,11594,10461,10316,10269,28,27,33,30,32,31,35,34])).
% 66.84/66.93 cnf(12038,plain,
% 66.84/66.93 (P2(f3(a10,a10),f3(a7,a7),f3(a10,a10))),
% 66.84/66.93 inference(scs_inference,[],[12007,12024,11946,28,27,33])).
% 66.84/66.93 cnf(12040,plain,
% 66.84/66.93 (P4(f6(a7),f6(a10),f6(a10))),
% 66.84/66.93 inference(scs_inference,[],[12007,12024,12016,11946,11604,28,27,33,30])).
% 66.84/66.93 cnf(12042,plain,
% 66.84/66.93 (P2(f3(a4,a4),a1,f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[12007,12010,12024,12016,11974,11946,11604,11888,28,27,33,30,32])).
% 66.84/66.93 cnf(12048,plain,
% 66.84/66.93 (P4(f8(a5),f9(a1,a1),f8(a5))),
% 66.84/66.93 inference(scs_inference,[],[12007,12010,12012,12024,11914,12016,11974,11886,10976,11980,10963,11946,11604,11162,11888,10870,11704,28,27,33,30,32,31,35,34])).
% 66.84/66.93 cnf(12063,plain,
% 66.84/66.93 (P2(f3(a7,a7),f3(a10,a10),f3(a10,a10))),
% 66.84/66.93 inference(scs_inference,[],[12038,28])).
% 66.84/66.93 cnf(12067,plain,
% 66.84/66.93 (P2(f3(a10,a10),a1,f3(a10,a10))),
% 66.84/66.93 inference(scs_inference,[],[12038,12014,12048,28,27,33])).
% 66.84/66.93 cnf(12069,plain,
% 66.84/66.93 (P4(f9(a1,a1),f3(a7,a7),f6(a7))),
% 66.84/66.93 inference(scs_inference,[],[12038,12014,12048,11964,11886,11111,28,27,33,30])).
% 66.84/66.93 cnf(12071,plain,
% 66.84/66.93 (P2(f3(a7,a7),f9(a1,a1),f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[12038,12014,12048,11964,11886,11111,10451,28,27,33,30,32])).
% 66.84/66.93 cnf(12079,plain,
% 66.84/66.93 (P4(f3(a7,a7),f9(a1,a1),f6(a7))),
% 66.84/66.93 inference(scs_inference,[],[12069,27])).
% 66.84/66.93 cnf(12081,plain,
% 66.84/66.93 (P2(f9(a1,a1),f3(a7,a7),f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[12071,12069,27,28])).
% 66.84/66.93 cnf(12083,plain,
% 66.84/66.93 (P4(f8(a5),f3(a7,a7),f8(a5))),
% 66.84/66.93 inference(scs_inference,[],[12071,12069,12048,11636,27,28,31])).
% 66.84/66.93 cnf(12085,plain,
% 66.84/66.93 (P2(a1,a1,f3(a7,a7))),
% 66.84/66.93 inference(scs_inference,[],[12071,12069,12042,12048,11636,11931,27,28,31,33])).
% 66.84/66.93 cnf(12089,plain,
% 66.84/66.93 (P2(f3(a7,a7),f3(a4,a4),f3(a4,a4))),
% 66.84/66.93 inference(scs_inference,[],[12063,12071,12069,12042,12048,11976,11636,11931,11097,10529,27,28,31,33,30,32])).
% 66.84/66.93 cnf(12104,plain,
% 66.84/66.93 (P4(f3(a7,a7),f6(a7),f6(a7))),
% 66.84/66.93 inference(scs_inference,[],[12089,11622,12079,12083,12085,11658,11084,40,27,28,31,26,30])).
% 66.84/66.93 cnf(12106,plain,
% 66.84/66.93 (P2(f9(a1,a1),a1,f9(a1,a1))),
% 66.84/66.93 inference(scs_inference,[],[12005,12089,11622,12079,12067,12083,12085,11658,11084,40,27,28,31,26,30,33])).
% 66.84/66.93 cnf(12108,plain,
% 66.84/66.93 (P2(f9(a1,a1),f3(a4,a4),f3(a4,a4))),
% 66.84/66.93 inference(scs_inference,[],[12005,12081,12089,11622,12079,12067,12083,12085,11658,11084,40,27,28,31,26,30,33,32])).
% 66.84/66.93 cnf(12134,plain,
% 66.84/66.93 ($false),
% 66.84/66.93 inference(scs_inference,[],[10,11749,12108,12018,12104,12106,12040,11997,12081,12042,12085,12024,10486,11714,11628,11409,10316,27,28,31,30,33,32,35,34,7357,20]),
% 66.84/66.93 ['proof']).
% 66.84/66.93 % SZS output end Proof
% 66.84/66.93 % Total time :66.260000s
%------------------------------------------------------------------------------