%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD047-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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:26 EDT 2024
% Result : Unsatisfiable 72.87s 73.00s
% Output : CNFRefutation 72.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : FLD047-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.10/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n017.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Wed Jun 19 10:43:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.18/0.55 start to proof:theBenchmark
% 72.87/72.99 %-------------------------------------------
% 72.87/72.99 % File :CSE---1.7
% 72.87/72.99 % Problem :theBenchmark
% 72.87/72.99 % Transform :cnf
% 72.87/72.99 % Format :tptp:raw
% 72.87/72.99 % Command :java -jar mcs_scs.jar %d %s
% 72.87/72.99
% 72.87/72.99 % Result :Theorem 72.390000s
% 72.87/72.99 % Output :CNFRefutation 72.390000s
% 72.87/72.99 %-------------------------------------------
% 72.87/73.00 %--------------------------------------------------------------------------
% 72.87/73.00 % File : FLD047-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% 72.87/73.00 % Domain : Field Theory (Ordered fields)
% 72.87/73.00 % Problem : Fraction calculation, part 1
% 72.87/73.00 % Version : [Dra93] axioms : Especial.
% 72.87/73.00 % Theorem formulation : Relational with re axiom set.
% 72.87/73.00 % English :
% 72.87/73.00
% 72.87/73.00 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 72.87/73.00 % Source : [Dra93]
% 72.87/73.00 % Names :
% 72.87/73.00
% 72.87/73.00 % Status : Unsatisfiable
% 72.87/73.00 % Rating : 0.17 v8.2.0, 0.29 v8.1.0, 0.14 v7.5.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.38 v6.3.0, 0.29 v6.2.0, 0.33 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.40 v5.3.0, 0.50 v5.2.0, 0.30 v5.1.0, 0.36 v5.0.0, 0.71 v4.1.0, 0.50 v4.0.1, 0.40 v4.0.0, 0.29 v3.4.0, 0.50 v3.3.0, 0.33 v2.7.0, 0.50 v2.6.0, 0.67 v2.5.0, 0.60 v2.4.0, 0.80 v2.3.0, 1.00 v2.1.0
% 72.87/73.00 % Syntax : Number of clauses : 38 ( 15 unt; 3 nHn; 38 RR)
% 72.87/73.00 % Number of literals : 89 ( 0 equ; 52 neg)
% 72.87/73.00 % Maximal clause size : 5 ( 2 avg)
% 72.87/73.00 % Maximal term depth : 2 ( 1 avg)
% 72.87/73.00 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 72.87/73.00 % Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% 72.87/73.00 % Number of variables : 73 ( 0 sgn)
% 72.87/73.00 % SPC : CNF_UNS_RFO_NEQ_NHN
% 72.87/73.00
% 72.87/73.00 % Comments :
% 72.87/73.00 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 72.87/73.00 %--------------------------------------------------------------------------
% 72.87/73.00 include('Axioms/FLD002-0.ax').
% 72.87/73.00 %--------------------------------------------------------------------------
% 72.87/73.00 cnf(a_is_defined,hypothesis,
% 72.87/73.00 defined(a) ).
% 72.87/73.00
% 72.87/73.00 cnf(b_is_defined,hypothesis,
% 72.87/73.00 defined(b) ).
% 72.87/73.00
% 72.87/73.00 cnf(c_is_defined,hypothesis,
% 72.87/73.00 defined(c) ).
% 72.87/73.00
% 72.87/73.00 cnf(u_is_defined,hypothesis,
% 72.87/73.00 defined(u) ).
% 72.87/73.00
% 72.87/73.00 cnf(s_is_defined,hypothesis,
% 72.87/73.00 defined(s) ).
% 72.87/73.00
% 72.87/73.00 cnf(t_is_defined,hypothesis,
% 72.87/73.00 defined(t) ).
% 72.87/73.00
% 72.87/73.00 cnf(not_sum_7,negated_conjecture,
% 72.87/73.00 ~ sum(additive_identity,b,additive_identity) ).
% 72.87/73.00
% 72.87/73.00 cnf(not_sum_8,negated_conjecture,
% 72.87/73.00 ~ sum(additive_identity,c,additive_identity) ).
% 72.87/73.00
% 72.87/73.00 cnf(product_9,negated_conjecture,
% 72.87/73.00 product(a,multiplicative_inverse(b),u) ).
% 72.87/73.00
% 72.87/73.00 cnf(product_10,negated_conjecture,
% 72.87/73.00 product(a,c,s) ).
% 72.87/73.00
% 72.87/73.00 cnf(product_11,negated_conjecture,
% 72.87/73.00 product(b,c,t) ).
% 72.87/73.00
% 72.87/73.00 cnf(not_product_12,negated_conjecture,
% 72.87/73.00 ~ product(s,multiplicative_inverse(t),u) ).
% 72.87/73.00
% 72.87/73.00 %--------------------------------------------------------------------------
% 72.87/73.00 %-------------------------------------------
% 72.87/73.00 % Proof found
% 72.87/73.00 % SZS status Theorem for theBenchmark
% 72.87/73.00 % SZS output start Proof
% 72.87/73.00 %ClaNum:38(EqnAxiom:0)
% 72.87/73.00 %VarNum:162(SingletonVarNum:73)
% 72.87/73.00 %MaxLitNum:5
% 72.87/73.00 %MaxfuncDepth:1
% 72.87/73.00 %SharedTerms:25
% 72.87/73.00 %goalClause: 9 10 11 13 14 15
% 72.87/73.00 %singleGoalClaCount:6
% 72.87/73.00 [1]P1(a1)
% 72.87/73.00 [2]P1(a4)
% 72.87/73.00 [3]P1(a2)
% 72.87/73.00 [4]P1(a5)
% 72.87/73.00 [5]P1(a7)
% 72.87/73.00 [6]P1(a8)
% 72.87/73.00 [7]P1(a9)
% 72.87/73.00 [8]P1(a12)
% 72.87/73.00 [9]P2(a2,a7,a9)
% 72.97/73.00 [10]P2(a5,a7,a12)
% 72.97/73.00 [12]~P4(a1,a1,a4)
% 72.97/73.00 [13]~P4(a1,a5,a1)
% 72.97/73.00 [14]~P4(a1,a7,a1)
% 72.97/73.00 [11]P2(a2,f10(a5),a8)
% 72.97/73.00 [15]~P2(a9,f10(a12),a8)
% 72.97/73.00 [21]~P1(x211)+P4(a1,x211,x211)
% 72.97/73.00 [22]~P1(x221)+P2(a4,x221,x221)
% 72.97/73.01 [16]~P1(x161)+P1(f6(x161))
% 72.97/73.01 [23]~P1(x231)+P4(f6(x231),x231,a1)
% 72.97/73.01 [30]~P4(x302,x301,x303)+P4(x301,x302,x303)
% 72.97/73.01 [31]~P2(x312,x311,x313)+P2(x311,x312,x313)
% 72.97/73.01 [24]~P1(x241)+P4(a1,x241,a1)+P1(f10(x241))
% 72.97/73.01 [28]~P1(x281)+P2(f10(x281),x281,a4)+P4(a1,x281,a1)
% 72.97/73.01 [27]~P3(x272,x271)+~P3(x271,x272)+P4(a1,x271,x272)
% 72.97/73.01 [18]~P1(x182)+~P1(x181)+P1(f3(x181,x182))
% 72.97/73.01 [19]~P1(x192)+~P1(x191)+P1(f11(x191,x192))
% 72.97/73.01 [25]~P1(x252)+~P1(x251)+P4(x251,x252,f3(x251,x252))
% 72.97/73.01 [26]~P1(x262)+~P1(x261)+P2(x261,x262,f11(x261,x262))
% 72.97/73.01 [20]~P3(x201,x203)+P3(x201,x202)+~P3(x203,x202)
% 72.97/73.01 [17]P3(x172,x171)+~P1(x171)+~P1(x172)+P3(x171,x172)
% 72.97/73.01 [29]~P2(x293,x292,x291)+P3(a1,x291)+~P3(a1,x292)+~P3(a1,x293)
% 72.97/73.01 [32]~P4(x323,x325,x321)+P3(x321,x322)+~P4(x324,x325,x322)+~P3(x323,x324)
% 72.97/73.01 [33]~P4(x331,x336,x334)+P4(x331,x332,x333)+~P4(x334,x335,x333)+~P4(x336,x335,x332)
% 72.97/73.01 [34]~P4(x346,x344,x341)+P4(x341,x342,x343)+~P4(x344,x342,x345)+~P4(x346,x345,x343)
% 72.97/73.01 [35]~P2(x351,x356,x354)+P2(x351,x352,x353)+~P2(x354,x355,x353)+~P2(x356,x355,x352)
% 72.97/73.01 [36]~P2(x366,x364,x361)+P2(x361,x362,x363)+~P2(x364,x362,x365)+~P2(x366,x365,x363)
% 72.97/73.01 [37]~P2(x375,x377,x372)+~P2(x374,x377,x371)+P4(x371,x372,x373)+~P4(x374,x375,x376)+~P2(x376,x377,x373)
% 72.97/73.01 [38]~P2(x387,x382,x385)+~P2(x386,x382,x384)+P2(x381,x382,x383)+~P4(x384,x385,x383)+~P4(x386,x387,x381)
% 72.97/73.01 %EqnAxiom
% 72.97/73.01
% 72.97/73.01 %-------------------------------------------
% 72.97/73.02 cnf(39,plain,
% 72.97/73.02 (~P2(f10(a12),a9,a8)),
% 72.97/73.02 inference(scs_inference,[],[15,31])).
% 72.97/73.02 cnf(41,plain,
% 72.97/73.02 (~P4(a5,a1,a1)),
% 72.97/73.02 inference(scs_inference,[],[13,15,31,30])).
% 72.97/73.02 cnf(43,plain,
% 72.97/73.02 (P3(a1,a1)),
% 72.97/73.02 inference(scs_inference,[],[13,15,1,31,30,17])).
% 72.97/73.02 cnf(49,plain,
% 72.97/73.02 (P2(a9,x491,a9)+~P2(a7,x491,a7)),
% 72.97/73.02 inference(scs_inference,[],[9,13,15,1,31,30,17,27,35,36])).
% 72.97/73.02 cnf(52,plain,
% 72.97/73.02 (~P4(a7,a1,a1)),
% 72.97/73.02 inference(scs_inference,[],[14,30])).
% 72.97/73.02 cnf(54,plain,
% 72.97/73.02 (P3(a4,a4)),
% 72.97/73.02 inference(scs_inference,[],[14,2,30,17])).
% 72.97/73.02 cnf(59,plain,
% 72.97/73.02 (P3(a2,a2)),
% 72.97/73.02 inference(scs_inference,[],[3,17])).
% 72.97/73.02 cnf(66,plain,
% 72.97/73.02 (P3(a5,a5)),
% 72.97/73.02 inference(scs_inference,[],[4,17])).
% 72.97/73.02 cnf(68,plain,
% 72.97/73.02 (P2(a12,x681,a12)+~P2(a7,x681,a7)),
% 72.97/73.02 inference(scs_inference,[],[10,4,17,36])).
% 72.97/73.02 cnf(71,plain,
% 72.97/73.02 (P3(a7,a7)),
% 72.97/73.02 inference(scs_inference,[],[5,17])).
% 72.97/73.02 cnf(73,plain,
% 72.97/73.02 (P2(a8,x731,a8)+~P2(f10(a5),x731,f10(a5))),
% 72.97/73.02 inference(scs_inference,[],[11,5,17,36])).
% 72.97/73.02 cnf(80,plain,
% 72.97/73.02 (P3(a8,a8)),
% 72.97/73.02 inference(scs_inference,[],[6,17])).
% 72.97/73.02 cnf(82,plain,
% 72.97/73.02 (~P2(x821,a5,a5)+P2(x821,a12,a12)),
% 72.97/73.02 inference(scs_inference,[],[10,6,17,35])).
% 72.97/73.02 cnf(87,plain,
% 72.97/73.02 (P3(a9,a9)),
% 72.97/73.02 inference(scs_inference,[],[7,17])).
% 72.97/73.02 cnf(89,plain,
% 72.97/73.02 (~P2(x891,a2,a2)+P2(x891,a8,a8)),
% 72.97/73.02 inference(scs_inference,[],[11,7,17,35])).
% 72.97/73.02 cnf(94,plain,
% 72.97/73.02 (P3(a12,a12)),
% 72.97/73.02 inference(scs_inference,[],[8,17])).
% 72.97/73.02 cnf(105,plain,
% 72.97/73.02 (~P4(a2,x1051,x1052)+~P4(a2,x1051,x1053)+P3(x1052,x1053)),
% 72.97/73.02 inference(scs_inference,[],[59,32])).
% 72.97/73.02 cnf(106,plain,
% 72.97/73.02 (~P4(a5,x1061,x1062)+~P4(a5,x1061,x1063)+P3(x1062,x1063)),
% 72.97/73.02 inference(scs_inference,[],[66,32])).
% 72.97/73.02 cnf(107,plain,
% 72.97/73.02 (~P4(a7,x1071,x1072)+~P4(a7,x1071,x1073)+P3(x1072,x1073)),
% 72.97/73.02 inference(scs_inference,[],[71,32])).
% 72.97/73.02 cnf(109,plain,
% 72.97/73.02 (~P4(a9,x1091,x1092)+~P4(a9,x1091,x1093)+P3(x1092,x1093)),
% 72.97/73.02 inference(scs_inference,[],[87,32])).
% 72.97/73.02 cnf(112,plain,
% 72.97/73.02 (~P4(a4,x1121,x1122)+~P4(a4,x1121,x1123)+P3(x1122,x1123)),
% 72.97/73.02 inference(scs_inference,[],[54,32])).
% 72.97/73.02 cnf(119,plain,
% 72.97/73.02 (~P4(a1,x1191,x1192)+~P4(a1,x1191,x1193)+P3(x1192,x1193)),
% 72.97/73.02 inference(scs_inference,[],[43,32])).
% 72.97/73.02 cnf(127,plain,
% 72.97/73.02 (P4(a1,f6(a4),f6(a4))),
% 72.97/73.02 inference(scs_inference,[],[2,21,16])).
% 72.97/73.02 cnf(197,plain,
% 72.97/73.02 (P4(f6(f6(a9)),f6(a9),a1)),
% 72.97/73.02 inference(scs_inference,[],[7,23,16])).
% 72.97/73.02 cnf(198,plain,
% 72.97/73.02 (~P4(f6(a9),a7,f6(a9))),
% 72.97/73.02 inference(scs_inference,[],[14,197,34])).
% 72.97/73.02 cnf(200,plain,
% 72.97/73.02 (~P4(a7,f6(a9),f6(a9))),
% 72.97/73.02 inference(scs_inference,[],[14,197,34,30])).
% 72.97/73.02 cnf(237,plain,
% 72.97/73.02 (~P2(x2371,a7,a7)+P2(a9,x2371,a9)),
% 72.97/73.02 inference(scs_inference,[],[49,31])).
% 72.97/73.02 cnf(253,plain,
% 72.97/73.02 (~P2(x2531,a7,a7)+P2(a12,x2531,a12)),
% 72.97/73.02 inference(scs_inference,[],[68,31])).
% 72.97/73.02 cnf(269,plain,
% 72.97/73.02 (P2(a12,x2691,a12)+~P2(x2691,a5,a5)),
% 72.97/73.02 inference(scs_inference,[],[82,31])).
% 72.97/73.02 cnf(301,plain,
% 72.97/73.02 (P2(a8,x3011,a8)+~P2(x3011,a2,a2)),
% 72.97/73.02 inference(scs_inference,[],[89,31])).
% 72.97/73.02 cnf(380,plain,
% 72.97/73.02 (P2(x3801,a9,a9)+~P2(x3801,a7,a7)),
% 72.97/73.02 inference(scs_inference,[],[237,31])).
% 72.97/73.02 cnf(396,plain,
% 72.97/73.02 (P2(x3961,a12,a12)+~P2(x3961,a7,a7)),
% 72.97/73.02 inference(scs_inference,[],[253,31])).
% 72.97/73.02 cnf(412,plain,
% 72.97/73.02 (P2(a12,a4,a12)),
% 72.97/73.02 inference(scs_inference,[],[4,269,22])).
% 72.97/73.02 cnf(420,plain,
% 72.97/73.02 (P2(a12,x4201,a12)+~P2(a4,x4201,a4)),
% 72.97/73.02 inference(scs_inference,[],[412,36])).
% 72.97/73.02 cnf(436,plain,
% 72.97/73.02 (P2(a8,a4,a8)),
% 72.97/73.02 inference(scs_inference,[],[3,301,22])).
% 72.97/73.02 cnf(444,plain,
% 72.97/73.02 (P2(a8,x4441,a8)+~P2(a4,x4441,a4)),
% 72.97/73.02 inference(scs_inference,[],[436,36])).
% 72.97/73.02 cnf(464,plain,
% 72.97/73.02 (P2(a4,a9,a9)),
% 72.97/73.02 inference(scs_inference,[],[5,380,22])).
% 72.97/73.02 cnf(486,plain,
% 72.97/73.02 (P2(a4,a12,a12)),
% 72.97/73.02 inference(scs_inference,[],[5,396,22])).
% 72.97/73.02 cnf(538,plain,
% 72.97/73.02 (~P2(x5381,a4,a4)+P2(a12,x5381,a12)),
% 72.97/73.02 inference(scs_inference,[],[420,31])).
% 72.97/73.02 cnf(584,plain,
% 72.97/73.02 (~P2(x5841,a4,a4)+P2(a8,x5841,a8)),
% 72.97/73.02 inference(scs_inference,[],[444,31])).
% 72.97/73.02 cnf(706,plain,
% 72.97/73.02 (P2(x7061,a8,a8)+~P2(x7061,a4,a4)),
% 72.97/73.02 inference(scs_inference,[],[584,31])).
% 72.97/73.02 cnf(722,plain,
% 72.97/73.02 (P2(a4,a8,a8)),
% 72.97/73.02 inference(scs_inference,[],[2,706,22])).
% 72.97/73.02 cnf(810,plain,
% 72.97/73.02 (~P2(a8,x8101,a9)+~P2(x8101,f10(a12),a4)),
% 72.97/73.02 inference(scs_inference,[],[15,436,36])).
% 72.97/73.02 cnf(812,plain,
% 72.97/73.02 (~P2(x8121,a8,a9)+~P2(x8121,f10(a12),a4)),
% 72.97/73.02 inference(scs_inference,[],[15,436,36,31])).
% 72.97/73.02 cnf(844,plain,
% 72.97/73.02 (~P2(f10(a12),x8441,a4)+~P2(a8,x8441,a9)),
% 72.97/73.02 inference(scs_inference,[],[810,31])).
% 72.97/73.02 cnf(860,plain,
% 72.97/73.02 (~P2(f10(a12),x8601,a4)+~P2(x8601,a8,a9)),
% 72.97/73.02 inference(scs_inference,[],[812,31])).
% 72.97/73.02 cnf(876,plain,
% 72.97/73.02 (~P2(a8,a12,a9)+P4(a1,a12,a1)),
% 72.97/73.02 inference(scs_inference,[],[8,844,28])).
% 72.97/73.02 cnf(892,plain,
% 72.97/73.02 (~P2(a12,a8,a9)+P4(a1,a12,a1)),
% 72.97/73.02 inference(scs_inference,[],[876,31])).
% 72.97/73.02 cnf(908,plain,
% 72.97/73.02 (~P2(a12,a2,x9081)+~P2(x9081,f10(a5),a9)+P4(a1,a12,a1)),
% 72.97/73.02 inference(scs_inference,[],[11,892,35])).
% 72.97/73.02 cnf(1622,plain,
% 72.97/73.02 (~P4(a12,a7,a12)+~P2(x16221,f10(a5),a9)+~P2(a12,a2,x16221)),
% 72.97/73.02 inference(scs_inference,[],[14,908,34])).
% 72.97/73.02 cnf(1670,plain,
% 72.97/73.02 (~P4(a7,a12,a12)+~P2(x16701,f10(a5),a9)+~P2(a12,a2,x16701)),
% 72.97/73.02 inference(scs_inference,[],[1622,30])).
% 72.97/73.02 cnf(1937,plain,
% 72.97/73.02 (~P2(a4,x19371,f10(a12))+~P2(x19371,a9,a8)),
% 72.97/73.02 inference(scs_inference,[],[39,722,36])).
% 72.97/73.02 cnf(1941,plain,
% 72.97/73.02 (~P2(a4,a8,f10(a12))+~P2(a9,a4,a4)),
% 72.97/73.02 inference(scs_inference,[],[39,722,36,73,584])).
% 72.97/73.02 cnf(1991,plain,
% 72.97/73.02 (~P2(x19911,a4,f10(a12))+~P2(x19911,a9,a8)),
% 72.97/73.02 inference(scs_inference,[],[1937,31])).
% 72.97/73.02 cnf(2007,plain,
% 72.97/73.02 (~P2(a8,a4,f10(a12))+~P2(a9,a4,a4)),
% 72.97/73.02 inference(scs_inference,[],[1941,31])).
% 72.97/73.02 cnf(2039,plain,
% 72.97/73.02 (~P2(a7,x20391,a4)+~P2(a9,x20391,f10(a12))+~P2(a2,a9,a8)),
% 72.97/73.02 inference(scs_inference,[],[9,1991,35])).
% 72.97/73.02 cnf(2055,plain,
% 72.97/73.02 (~P2(a4,x20551,a4)+~P2(a8,x20551,f10(a12))+~P2(a9,a4,a4)),
% 72.97/73.02 inference(scs_inference,[],[436,2007,35])).
% 72.97/73.02 cnf(2167,plain,
% 72.97/73.02 (~P2(x21671,a9,f10(a12))+~P2(a7,x21671,a4)+~P2(a2,a9,a8)),
% 72.97/73.02 inference(scs_inference,[],[2039,31])).
% 72.97/73.02 cnf(2183,plain,
% 72.97/73.02 (~P2(a4,a9,a4)+~P2(a8,x21831,f10(a12))+~P2(a4,x21831,a4)),
% 72.97/73.02 inference(scs_inference,[],[2055,31])).
% 72.97/73.02 cnf(2262,plain,
% 72.97/73.02 (~P2(x22621,a9,a4)+~P2(x22621,a4,a4)+~P2(a8,a9,f10(a12))),
% 72.97/73.02 inference(scs_inference,[],[464,2183,36])).
% 72.97/73.02 cnf(2278,plain,
% 72.97/73.02 (~P2(a9,a8,f10(a12))+~P2(x22781,a4,a4)+~P2(x22781,a9,a4)),
% 72.97/73.02 inference(scs_inference,[],[2262,31])).
% 72.97/73.02 cnf(2294,plain,
% 72.97/73.02 (~P2(a4,x22941,a4)+~P2(a9,a8,f10(a12))+~P2(x22941,a9,a4)),
% 72.97/73.02 inference(scs_inference,[],[2278,31])).
% 72.97/73.02 cnf(3321,plain,
% 72.97/73.02 (~P4(f6(a4),x33211,a5)+~P4(f6(a4),x33211,a1)),
% 72.97/73.02 inference(scs_inference,[],[13,127,33])).
% 72.97/73.02 cnf(3398,plain,
% 72.97/73.02 (~P4(f6(a4),a4,a5)),
% 72.97/73.02 inference(scs_inference,[],[2,3321,23])).
% 72.97/73.02 cnf(3399,plain,
% 72.97/73.02 (~P4(a4,f6(a4),a5)),
% 72.97/73.02 inference(scs_inference,[],[3398,30])).
% 72.97/73.02 cnf(3655,plain,
% 72.97/73.02 (P2(a7,a2,a9)),
% 72.97/73.02 inference(scs_inference,[],[9,31])).
% 72.97/73.02 cnf(3660,plain,
% 72.97/73.02 (P2(a7,a5,a12)),
% 72.97/73.02 inference(scs_inference,[],[10,31])).
% 72.97/73.02 cnf(3665,plain,
% 72.97/73.02 (P2(f10(a5),a2,a8)),
% 72.97/73.02 inference(scs_inference,[],[11,31])).
% 72.97/73.02 cnf(3670,plain,
% 72.97/73.02 (P2(a9,a4,a9)),
% 72.97/73.02 inference(scs_inference,[],[464,31])).
% 72.97/73.02 cnf(3710,plain,
% 72.97/73.02 (P4(f6(a4),a1,f6(a4))),
% 72.97/73.02 inference(scs_inference,[],[127,30])).
% 72.97/73.02 cnf(3712,plain,
% 72.97/73.02 (P4(f6(a4),x37121,f6(a4))+~P4(a1,x37121,a1)),
% 72.97/73.02 inference(scs_inference,[],[127,30,34])).
% 72.97/73.02 cnf(3721,plain,
% 72.97/73.02 (~P4(a4,f6(a4),x37211)+~P4(x37211,a1,a5)),
% 72.97/73.02 inference(scs_inference,[],[3399,3710,33])).
% 72.97/73.02 cnf(3838,plain,
% 72.97/73.02 (~P4(f6(a4),a4,x38381)+~P4(x38381,a1,a5)),
% 72.97/73.02 inference(scs_inference,[],[3721,30])).
% 72.97/73.02 cnf(4721,plain,
% 72.97/73.02 (P2(a2,a12,x47211)+~P2(a9,a5,x47211)),
% 72.97/73.02 inference(scs_inference,[],[9,3660,35])).
% 72.97/73.02 cnf(4743,plain,
% 72.97/73.02 (P2(a2,a12,f11(a9,a5))),
% 72.97/73.02 inference(scs_inference,[],[4,7,4721,26])).
% 72.97/73.02 cnf(4744,plain,
% 72.97/73.02 (P2(a12,a2,f11(a9,a5))),
% 72.97/73.02 inference(scs_inference,[],[4743,31])).
% 72.97/73.02 cnf(4746,plain,
% 72.97/73.02 (P2(a4,f11(a9,a5),f11(a9,a5))),
% 72.97/73.02 inference(scs_inference,[],[486,4743,31,35])).
% 72.97/73.02 cnf(4748,plain,
% 72.97/73.02 (~P4(a7,a12,a12)+~P2(f11(a9,a5),f10(a5),a9)),
% 72.97/73.02 inference(scs_inference,[],[486,4743,31,35,1670])).
% 72.97/73.02 cnf(4755,plain,
% 72.97/73.02 (P4(a1,a12,a1)+~P2(f11(a9,a5),f10(a5),a9)),
% 72.97/73.02 inference(scs_inference,[],[4746,4744,31,908])).
% 72.97/73.02 cnf(4760,plain,
% 72.97/73.02 (~P4(a12,a7,a12)+~P2(f11(a9,a5),f10(a5),a9)),
% 72.97/73.02 inference(scs_inference,[],[4744,1622])).
% 72.97/73.02 cnf(4768,plain,
% 72.97/73.02 (P2(f10(a5),f11(a9,a5),x47681)+~P2(a8,a12,x47681)),
% 72.97/73.02 inference(scs_inference,[],[3665,4743,35])).
% 72.97/73.02 cnf(4770,plain,
% 72.97/73.02 (P2(f11(a9,a5),f10(a5),x47701)+~P2(a8,a12,x47701)),
% 72.97/73.02 inference(scs_inference,[],[3665,4743,35,31])).
% 72.97/73.02 cnf(4773,plain,
% 72.97/73.02 (P4(f11(a9,a5),f11(a9,a5),f11(a9,a5))+~P4(a12,a12,a12)),
% 72.97/73.02 inference(scs_inference,[],[4744,37])).
% 72.97/73.02 cnf(4845,plain,
% 72.97/73.02 (~P2(f11(a9,a5),f10(a5),a9)+~P2(a12,f10(a12),a4)),
% 72.97/73.02 inference(scs_inference,[],[11,4744,35,812])).
% 72.97/73.02 cnf(4847,plain,
% 72.97/73.02 (~P2(f11(a9,a5),f10(a5),a9)+~P2(f10(a12),a12,a4)),
% 72.97/73.02 inference(scs_inference,[],[11,4744,35,812,860])).
% 72.97/73.02 cnf(5825,plain,
% 72.97/73.02 (~P4(a7,a12,a12)+~P2(a8,a12,a9)),
% 72.97/73.02 inference(scs_inference,[],[4748,4770])).
% 72.97/73.02 cnf(5841,plain,
% 72.97/73.02 (~P4(a12,a7,a12)+~P2(a8,a12,a9)),
% 72.97/73.02 inference(scs_inference,[],[5825,30])).
% 72.97/73.02 cnf(5857,plain,
% 72.97/73.02 (~P2(x58571,a7,a7)+~P4(a5,x58571,a5)+~P2(a8,a12,a9)),
% 72.97/73.02 inference(scs_inference,[],[10,5841,37])).
% 72.97/73.02 cnf(5873,plain,
% 72.97/73.02 (~P2(f10(a5),f11(a9,a5),a9)+P4(a1,a12,a1)),
% 72.97/73.02 inference(scs_inference,[],[4755,31])).
% 72.97/73.02 cnf(5889,plain,
% 72.97/73.02 (~P2(f10(a5),f11(a9,a5),a9)+~P4(a12,a7,a12)),
% 72.97/73.02 inference(scs_inference,[],[4760,31])).
% 72.97/73.02 cnf(6001,plain,
% 72.97/73.02 (~P2(f10(a5),f11(a9,a5),a9)+P4(f6(a4),a12,f6(a4))),
% 72.97/73.02 inference(scs_inference,[],[5873,3712])).
% 72.97/73.02 cnf(6017,plain,
% 72.97/73.02 (~P4(a7,a12,a12)+~P2(f10(a5),f11(a9,a5),a9)),
% 72.97/73.02 inference(scs_inference,[],[5889,30])).
% 72.97/73.02 cnf(6143,plain,
% 72.97/73.02 (~P2(x61431,a7,a7)+~P4(x61431,a5,a5)+~P2(f10(a5),f11(a9,a5),a9)),
% 72.97/73.02 inference(scs_inference,[],[10,6017,37])).
% 72.97/73.02 cnf(6350,plain,
% 72.97/73.02 (~P2(f10(a5),f11(a9,a5),a9)+~P2(a12,f10(a12),a4)),
% 72.97/73.02 inference(scs_inference,[],[4845,31])).
% 72.97/73.02 cnf(6366,plain,
% 72.97/73.02 (~P2(f10(a5),f11(a9,a5),a9)+~P2(f10(a12),a12,a4)),
% 72.97/73.02 inference(scs_inference,[],[4847,31])).
% 72.97/73.02 cnf(6696,plain,
% 72.97/73.02 (~P2(f10(a5),x66961,a9)+~P2(x66961,f10(a12),a2)),
% 72.97/73.02 inference(scs_inference,[],[3665,15,36])).
% 72.97/73.02 cnf(8008,plain,
% 72.97/73.02 (P4(f6(a4),a12,f6(a4))+~P2(a8,a12,a9)),
% 72.97/73.02 inference(scs_inference,[],[6001,4768])).
% 72.97/73.02 cnf(8900,plain,
% 72.97/73.02 (~P4(f6(a4),x89001,a1)+~P4(f6(a4),x89001,a4)),
% 72.97/73.02 inference(scs_inference,[],[12,127,33])).
% 72.97/73.02 cnf(8911,plain,
% 72.97/73.02 (~P4(x89111,x89112,a1)+~P4(x89111,x89113,a1)+~P4(x89113,a7,x89112)),
% 72.97/73.02 inference(scs_inference,[],[14,200,87,34])).
% 72.97/73.02 cnf(8915,plain,
% 72.97/73.02 (~P4(x89151,f6(a4),a4)+~P4(f6(a4),x89151,a1)),
% 72.97/73.02 inference(scs_inference,[],[8900,30])).
% 72.97/73.02 cnf(8932,plain,
% 72.97/73.02 (P1(f6(a8))),
% 72.97/73.02 inference(scs_inference,[],[6,16])).
% 72.97/73.02 cnf(8934,plain,
% 72.97/73.02 (P4(f6(a8),a8,a1)),
% 72.97/73.02 inference(scs_inference,[],[6,16,23])).
% 72.97/73.02 cnf(8938,plain,
% 72.97/73.02 (P2(a2,a4,a2)),
% 72.97/73.02 inference(scs_inference,[],[6,3,16,23,22,31])).
% 72.97/73.02 cnf(8940,plain,
% 72.97/73.02 (P4(a1,a8,a8)),
% 72.97/73.02 inference(scs_inference,[],[6,3,16,23,22,31,21])).
% 72.97/73.02 cnf(8942,plain,
% 72.97/73.02 (P4(a8,f6(a8),a1)),
% 72.97/73.02 inference(scs_inference,[],[6,3,16,23,22,31,21,30])).
% 72.97/73.02 cnf(8946,plain,
% 72.97/73.02 (P1(f11(a8,a8))),
% 72.97/73.02 inference(scs_inference,[],[6,3,16,23,22,31,21,30,18,19])).
% 72.97/73.02 cnf(8948,plain,
% 72.97/73.02 (P1(f10(a5))),
% 72.97/73.02 inference(scs_inference,[],[6,3,4,13,16,23,22,31,21,30,18,19,24])).
% 72.97/73.02 cnf(8950,plain,
% 72.97/73.02 (P2(f10(a5),a5,a4)),
% 72.97/73.02 inference(scs_inference,[],[6,3,4,13,16,23,22,31,21,30,18,19,24,28])).
% 72.97/73.02 cnf(8952,plain,
% 72.97/73.03 (~P4(a8,a7,a8)),
% 72.97/73.03 inference(scs_inference,[],[6,3,4,13,16,23,22,31,21,30,18,19,24,28,8911])).
% 72.97/73.03 cnf(8954,plain,
% 72.97/73.03 (P4(a8,a8,f3(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[6,3,4,13,16,23,22,31,21,30,18,19,24,28,8911,25])).
% 72.97/73.03 cnf(8956,plain,
% 72.97/73.03 (P4(a1,a1,a1)),
% 72.97/73.03 inference(scs_inference,[],[6,3,4,13,43,16,23,22,31,21,30,18,19,24,28,8911,25,27])).
% 72.97/73.03 cnf(8958,plain,
% 72.97/73.03 (P2(a8,a8,f11(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[6,3,4,13,43,16,23,22,31,21,30,18,19,24,28,8911,25,27,26])).
% 72.97/73.03 cnf(8960,plain,
% 72.97/73.03 (P4(a8,a1,a8)),
% 72.97/73.03 inference(scs_inference,[],[6,3,4,13,43,16,23,22,31,21,30,18,19,24,28,8911,25,27,26,33])).
% 72.97/73.03 cnf(8964,plain,
% 72.97/73.03 (P2(f11(a8,a8),a4,f11(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[436,6,3,4,13,43,16,23,22,31,21,30,18,19,24,28,8911,25,27,26,33,34,36])).
% 72.97/73.03 cnf(8966,plain,
% 72.97/73.03 (P3(f3(a8,a8),f3(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[436,6,3,4,13,43,80,16,23,22,31,21,30,18,19,24,28,8911,25,27,26,33,34,36,32])).
% 72.97/73.03 cnf(8970,plain,
% 72.97/73.03 (P2(f3(a8,a8),a4,f3(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[722,436,6,3,4,13,43,80,16,23,22,31,21,30,18,19,24,28,8911,25,27,26,33,34,36,32,35,38])).
% 72.97/73.03 cnf(8972,plain,
% 72.97/73.03 (~P2(a1,a4,a7)),
% 72.97/73.03 inference(scs_inference,[],[722,436,6,3,4,13,43,80,16,23,22,31,21,30,18,19,24,28,8911,25,27,26,33,34,36,32,35,38,37])).
% 72.97/73.03 cnf(8978,plain,
% 72.97/73.03 (P1(f6(a12))),
% 72.97/73.03 inference(scs_inference,[],[8,16])).
% 72.97/73.03 cnf(8980,plain,
% 72.97/73.03 (P4(f6(a12),a12,a1)),
% 72.97/73.03 inference(scs_inference,[],[8,16,23])).
% 72.97/73.03 cnf(8982,plain,
% 72.97/73.03 (P2(a4,f6(a8),f6(a8))),
% 72.97/73.03 inference(scs_inference,[],[8932,8,16,23,22])).
% 72.97/73.03 cnf(8984,plain,
% 72.97/73.03 (P2(a4,f3(a8,a8),f3(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[8970,8932,8,16,23,22,31])).
% 72.97/73.03 cnf(8986,plain,
% 72.97/73.03 (P4(a12,f6(a12),a1)),
% 72.97/73.03 inference(scs_inference,[],[8970,8932,8,16,23,22,31,30])).
% 72.97/73.03 cnf(8988,plain,
% 72.97/73.03 (P4(a1,f6(a8),f6(a8))),
% 72.97/73.03 inference(scs_inference,[],[8970,8932,8,16,23,22,31,30,21])).
% 72.97/73.03 cnf(8990,plain,
% 72.97/73.03 (P1(f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[8970,8932,8,16,23,22,31,30,21,18])).
% 72.97/73.03 cnf(8992,plain,
% 72.97/73.03 (P1(f11(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[8970,8932,8,16,23,22,31,30,21,18,19])).
% 72.97/73.03 cnf(8994,plain,
% 72.97/73.03 (P2(f10(a7),a7,a4)),
% 72.97/73.03 inference(scs_inference,[],[8970,8932,8,5,14,16,23,22,31,30,21,18,19,28])).
% 72.97/73.03 cnf(8996,plain,
% 72.97/73.03 (P1(f10(a7))),
% 72.97/73.03 inference(scs_inference,[],[8970,8932,8,5,14,16,23,22,31,30,21,18,19,28,24])).
% 72.97/73.03 cnf(9000,plain,
% 72.97/73.03 (P4(a12,a12,f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[8970,8932,8942,8,5,14,16,23,22,31,30,21,18,19,28,24,8911,25])).
% 72.97/73.03 cnf(9002,plain,
% 72.97/73.03 (P2(a12,a12,f11(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[8970,8932,8942,8,5,14,16,23,22,31,30,21,18,19,28,24,8911,25,26])).
% 72.97/73.03 cnf(9004,plain,
% 72.97/73.03 (P4(a1,f3(a8,a8),f3(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[8966,8970,8932,8942,8,5,14,16,23,22,31,30,21,18,19,28,24,8911,25,26,27])).
% 72.97/73.03 cnf(9008,plain,
% 72.97/73.03 (P3(f3(a12,a12),f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[8966,8970,8932,8942,8,5,14,94,16,23,22,31,30,21,18,19,28,24,8911,25,26,27,119,32])).
% 72.97/73.03 cnf(9010,plain,
% 72.97/73.03 (P2(a9,a5,f11(a9,a5))),
% 72.97/73.03 inference(scs_inference,[],[9,8966,8970,8932,8942,4743,8,5,3660,14,94,16,23,22,31,30,21,18,19,28,24,8911,25,26,27,119,32,36])).
% 72.97/73.03 cnf(9012,plain,
% 72.97/73.03 (P2(a4,f11(a12,a12),f11(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[9,8966,8970,8932,8942,486,4743,8,5,3660,14,94,16,23,22,31,30,21,18,19,28,24,8911,25,26,27,119,32,36,35])).
% 72.97/73.03 cnf(9025,plain,
% 72.97/73.03 (P1(f6(a9))),
% 72.97/73.03 inference(scs_inference,[],[7,16])).
% 72.97/73.03 cnf(9027,plain,
% 72.97/73.03 (P4(f6(a9),a9,a1)),
% 72.97/73.03 inference(scs_inference,[],[7,16,23])).
% 72.97/73.03 cnf(9029,plain,
% 72.97/73.03 (P2(a4,f10(a5),f10(a5))),
% 72.97/73.03 inference(scs_inference,[],[8948,7,16,23,22])).
% 72.97/73.03 cnf(9031,plain,
% 72.97/73.03 (P2(f11(a12,a12),a4,f11(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[9012,8948,7,16,23,22,31])).
% 72.97/73.03 cnf(9033,plain,
% 72.97/73.03 (P4(a1,f11(a8,a8),f11(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[9012,8946,8948,7,16,23,22,31,21])).
% 72.97/73.03 cnf(9035,plain,
% 72.97/73.03 (P4(f3(a8,a8),a1,f3(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[9004,9012,8946,8948,7,16,23,22,31,21,30])).
% 72.97/73.03 cnf(9037,plain,
% 72.97/73.03 (P1(f3(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9004,9012,8946,8948,7,16,23,22,31,21,30,18])).
% 72.97/73.03 cnf(9039,plain,
% 72.97/73.03 (P1(f11(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9004,9012,8946,8948,7,16,23,22,31,21,30,18,19])).
% 72.97/73.03 cnf(9041,plain,
% 72.97/73.03 (P4(a9,a9,f3(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9004,9012,8946,8948,7,16,23,22,31,21,30,18,19,25])).
% 72.97/73.03 cnf(9045,plain,
% 72.97/73.03 (P4(a1,f3(a12,a12),f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[9008,9004,9012,8946,8948,8980,7,16,23,22,31,21,30,18,19,25,8911,27])).
% 72.97/73.03 cnf(9047,plain,
% 72.97/73.03 (P2(a9,a9,f11(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9008,9004,9012,8946,8948,8980,7,16,23,22,31,21,30,18,19,25,8911,27,26])).
% 72.97/73.03 cnf(9049,plain,
% 72.97/73.03 (P2(a4,a4,a4)),
% 72.97/73.03 inference(scs_inference,[],[9008,9004,9012,8946,8948,8950,8980,7,16,23,22,31,21,30,18,19,25,8911,27,26,35])).
% 72.97/73.03 cnf(9051,plain,
% 72.97/73.03 (P2(a8,a5,a2)),
% 72.97/73.03 inference(scs_inference,[],[8938,9008,9004,9012,8946,8948,8950,8980,7,11,16,23,22,31,21,30,18,19,25,8911,27,26,35,36])).
% 72.97/73.03 cnf(9053,plain,
% 72.97/73.03 (P3(f3(a9,a9),f3(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[8938,9008,9004,9012,8946,8948,8950,8980,7,11,16,23,22,31,21,30,18,19,25,8911,27,26,35,36,109])).
% 72.97/73.03 cnf(9060,plain,
% 72.97/73.03 (P1(f6(a2))),
% 72.97/73.03 inference(scs_inference,[],[3,16])).
% 72.97/73.03 cnf(9062,plain,
% 72.97/73.03 (P4(f6(a2),a2,a1)),
% 72.97/73.03 inference(scs_inference,[],[3,16,23])).
% 72.97/73.03 cnf(9064,plain,
% 72.97/73.03 (P2(a4,f6(a12),f6(a12))),
% 72.97/73.03 inference(scs_inference,[],[8978,3,16,23,22])).
% 72.97/73.03 cnf(9066,plain,
% 72.97/73.03 (P2(a5,a8,a2)),
% 72.97/73.03 inference(scs_inference,[],[9051,8978,3,16,23,22,31])).
% 72.97/73.03 cnf(9068,plain,
% 72.97/73.03 (P4(f3(a12,a12),a1,f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[9051,9045,8978,3,16,23,22,31,30])).
% 72.97/73.03 cnf(9070,plain,
% 72.97/73.03 (P4(a1,f6(a12),f6(a12))),
% 72.97/73.03 inference(scs_inference,[],[9051,9045,8978,3,16,23,22,31,30,21])).
% 72.97/73.03 cnf(9074,plain,
% 72.97/73.03 (P1(f11(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[9051,9045,8978,3,16,23,22,31,30,21,18,19])).
% 72.97/73.03 cnf(9076,plain,
% 72.97/73.03 (P4(a2,a2,f3(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[9051,9045,8978,3,16,23,22,31,30,21,18,19,25])).
% 72.97/73.03 cnf(9080,plain,
% 72.97/73.03 (P2(a2,a2,f11(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[9051,9045,8978,8986,3,16,23,22,31,30,21,18,19,25,8911,26])).
% 72.97/73.03 cnf(9082,plain,
% 72.97/73.03 (P4(a1,f3(a9,a9),f3(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9051,9053,9045,8978,8986,3,16,23,22,31,30,21,18,19,25,8911,26,27])).
% 72.97/73.03 cnf(9084,plain,
% 72.97/73.03 (~P4(a7,a12,a12)),
% 72.97/73.03 inference(scs_inference,[],[9051,9053,9045,8978,8986,52,3,16,23,22,31,30,21,18,19,25,8911,26,27,33])).
% 72.97/73.03 cnf(9086,plain,
% 72.97/73.03 (P2(f11(a9,a9),a4,f11(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9051,9053,9045,8978,9047,8986,52,3670,3,16,23,22,31,30,21,18,19,25,8911,26,27,33,36])).
% 72.97/73.03 cnf(9090,plain,
% 72.97/73.03 (P2(f3(a8,a8),a5,f3(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[9051,9053,9045,8978,8954,9047,8986,52,3670,464,3,16,23,22,31,30,21,18,19,25,8911,26,27,33,36,35,38])).
% 72.97/73.03 cnf(9092,plain,
% 72.97/73.03 (P3(f3(a2,a2),f3(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[9051,9053,9045,8978,8954,9047,8986,52,3670,464,3,16,23,22,31,30,21,18,19,25,8911,26,27,33,36,35,38,105])).
% 72.97/73.03 cnf(9098,plain,
% 72.97/73.03 (P1(f6(a5))),
% 72.97/73.03 inference(scs_inference,[],[4,16])).
% 72.97/73.03 cnf(9100,plain,
% 72.97/73.03 (P4(f6(a5),a5,a1)),
% 72.97/73.03 inference(scs_inference,[],[4,16,23])).
% 72.97/73.03 cnf(9102,plain,
% 72.97/73.03 (P2(a4,f11(a2,a2),f11(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[9074,4,16,23,22])).
% 72.97/73.03 cnf(9104,plain,
% 72.97/73.03 (P2(a7,f10(a7),a4)),
% 72.97/73.03 inference(scs_inference,[],[8994,9074,4,16,23,22,31])).
% 72.97/73.03 cnf(9106,plain,
% 72.97/73.03 (P4(a1,f11(a2,a2),f11(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[8994,9074,4,16,23,22,31,21])).
% 72.97/73.03 cnf(9108,plain,
% 72.97/73.03 (P4(f3(a9,a9),a1,f3(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[8994,9074,9082,4,16,23,22,31,21,30])).
% 72.97/73.03 cnf(9110,plain,
% 72.97/73.03 (P1(f3(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[8994,9074,9082,4,16,23,22,31,21,30,18])).
% 72.97/73.03 cnf(9112,plain,
% 72.97/73.03 (P1(f11(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[8994,9074,9082,4,16,23,22,31,21,30,18,19])).
% 72.97/73.03 cnf(9114,plain,
% 72.97/73.03 (P4(a5,a5,f3(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[8994,9074,9082,4,16,23,22,31,21,30,18,19,25])).
% 72.97/73.03 cnf(9116,plain,
% 72.97/73.03 (~P4(a9,a7,a9)),
% 72.97/73.03 inference(scs_inference,[],[8994,9074,9082,9027,4,16,23,22,31,21,30,18,19,25,8911])).
% 72.97/73.03 cnf(9118,plain,
% 72.97/73.03 (P4(a1,f3(a2,a2),f3(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[8994,9092,9074,9082,9027,4,16,23,22,31,21,30,18,19,25,8911,27])).
% 72.97/73.03 cnf(9120,plain,
% 72.97/73.03 (P2(a5,a5,f11(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[8994,9092,9074,9082,9027,4,16,23,22,31,21,30,18,19,25,8911,27,26])).
% 72.97/73.03 cnf(9122,plain,
% 72.97/73.03 (~P4(f6(a5),f3(a5,a5),a1)),
% 72.97/73.03 inference(scs_inference,[],[8994,9092,9074,9082,9027,4,13,16,23,22,31,21,30,18,19,25,8911,27,26,34])).
% 72.97/73.03 cnf(9124,plain,
% 72.97/73.03 (~P4(a5,f6(a2),f6(a2))),
% 72.97/73.03 inference(scs_inference,[],[8994,9092,9074,9082,9027,9062,41,4,13,16,23,22,31,21,30,18,19,25,8911,27,26,34,33])).
% 72.97/73.03 cnf(9126,plain,
% 72.97/73.03 (P2(a12,a8,a9)),
% 72.97/73.03 inference(scs_inference,[],[9066,8994,9092,9074,9082,9027,9062,41,3660,4,3655,13,16,23,22,31,21,30,18,19,25,8911,27,26,34,33,36])).
% 72.97/73.03 cnf(9128,plain,
% 72.97/73.03 (P2(a4,f3(a2,a2),f3(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[9066,8994,8984,9092,9074,9082,9090,9027,9062,41,3660,4,3655,13,16,23,22,31,21,30,18,19,25,8911,27,26,34,33,36,35])).
% 72.97/73.03 cnf(9130,plain,
% 72.97/73.03 (P3(f3(a5,a5),f3(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[9066,8994,8984,9092,9074,9082,9090,9027,9062,41,3660,4,3655,13,16,23,22,31,21,30,18,19,25,8911,27,26,34,33,36,35,106])).
% 72.97/73.03 cnf(9136,plain,
% 72.97/73.03 (P4(a1,a12,a1)),
% 72.97/73.03 inference(scs_inference,[],[9126,892])).
% 72.97/73.03 cnf(9137,plain,
% 72.97/73.03 (P1(f6(a7))),
% 72.97/73.03 inference(scs_inference,[],[5,16])).
% 72.97/73.03 cnf(9139,plain,
% 72.97/73.03 (P4(f6(a7),a7,a1)),
% 72.97/73.03 inference(scs_inference,[],[5,16,23])).
% 72.97/73.03 cnf(9141,plain,
% 72.97/73.03 (P2(a4,f3(a12,a12),f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[8990,5,16,23,22])).
% 72.97/73.03 cnf(9143,plain,
% 72.97/73.03 (P2(a8,a12,a9)),
% 72.97/73.03 inference(scs_inference,[],[9126,8990,5,16,23,22,31])).
% 72.97/73.03 cnf(9145,plain,
% 72.97/73.03 (P4(f11(a8,a8),a1,f11(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[9126,9033,8990,5,16,23,22,31,30])).
% 72.97/73.03 cnf(9147,plain,
% 72.97/73.03 (P4(a1,f11(a12,a12),f11(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[9126,9033,8990,8992,5,16,23,22,31,30,21])).
% 72.97/73.03 cnf(9149,plain,
% 72.97/73.03 (P1(f3(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9126,9033,8990,8992,5,16,23,22,31,30,21,18])).
% 72.97/73.03 cnf(9151,plain,
% 72.97/73.03 (P1(f11(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9126,9033,8990,8992,5,16,23,22,31,30,21,18,19])).
% 72.97/73.03 cnf(9153,plain,
% 72.97/73.03 (P4(a7,a7,f3(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9126,9033,8990,8992,5,16,23,22,31,30,21,18,19,25])).
% 72.97/73.03 cnf(9155,plain,
% 72.97/73.03 (~P4(a5,a7,a5)),
% 72.97/73.03 inference(scs_inference,[],[9126,9033,8990,8992,9100,5,16,23,22,31,30,21,18,19,25,8911])).
% 72.97/73.03 cnf(9157,plain,
% 72.97/73.03 (P2(a7,a7,f11(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9126,9033,8990,8992,9100,5,16,23,22,31,30,21,18,19,25,8911,26])).
% 72.97/73.03 cnf(9159,plain,
% 72.97/73.03 (P4(a1,f3(a5,a5),f3(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[9126,9130,9033,8990,8992,9100,5,16,23,22,31,30,21,18,19,25,8911,26,27])).
% 72.97/73.03 cnf(9161,plain,
% 72.97/73.03 (~P4(a1,f6(a5),a1)),
% 72.97/73.03 inference(scs_inference,[],[8956,9126,9130,9033,8990,8992,9100,5,13,16,23,22,31,30,21,18,19,25,8911,26,27,34])).
% 72.97/73.03 cnf(9163,plain,
% 72.97/73.03 (P2(f11(a2,a2),a4,f11(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[8956,9126,9130,9033,8990,8992,9080,9100,8938,5,13,16,23,22,31,30,21,18,19,25,8911,26,27,34,36])).
% 72.97/73.03 cnf(9167,plain,
% 72.97/73.03 (P4(f6(a4),a12,f6(a4))),
% 72.97/73.03 inference(scs_inference,[],[8956,9116,9126,9130,9033,8990,8992,9080,9100,8960,8938,5,13,16,23,22,31,30,21,18,19,25,8911,26,27,34,36,37,8008])).
% 72.97/73.03 cnf(9168,plain,
% 72.97/73.03 (P3(f3(a7,a7),f3(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[8956,9116,9126,9130,9033,8990,8992,9080,9100,8960,8938,5,13,16,23,22,31,30,21,18,19,25,8911,26,27,34,36,37,8008,107])).
% 72.97/73.03 cnf(9170,plain,
% 72.97/73.03 (~P4(a5,x91701,a5)+~P2(x91701,a7,a7)),
% 72.97/73.03 inference(scs_inference,[],[8956,9116,9126,9130,9033,8990,8992,9080,9100,8960,8938,5,13,16,23,22,31,30,21,18,19,25,8911,26,27,34,36,37,8008,107,5857])).
% 72.97/73.03 cnf(9174,plain,
% 72.97/73.03 (P4(a1,a12,a1)),
% 72.97/73.03 inference(scs_inference,[],[9143,876])).
% 72.97/73.03 cnf(9175,plain,
% 72.97/73.03 (P1(f6(a1))),
% 72.97/73.03 inference(scs_inference,[],[1,16])).
% 72.97/73.03 cnf(9177,plain,
% 72.97/73.03 (P4(f6(a1),a1,a1)),
% 72.97/73.03 inference(scs_inference,[],[1,16,23])).
% 72.97/73.03 cnf(9179,plain,
% 72.97/73.03 (P2(a4,f10(a7),f10(a7))),
% 72.97/73.03 inference(scs_inference,[],[8996,1,16,23,22])).
% 72.97/73.03 cnf(9181,plain,
% 72.97/73.03 (P2(a5,a9,f11(a9,a5))),
% 72.97/73.03 inference(scs_inference,[],[9010,8996,1,16,23,22,31])).
% 72.97/73.03 cnf(9183,plain,
% 72.97/73.03 (P4(a1,f10(a7),f10(a7))),
% 72.97/73.03 inference(scs_inference,[],[9010,8996,1,16,23,22,31,21])).
% 72.97/73.03 cnf(9185,plain,
% 72.97/73.03 (P4(a12,a1,a1)),
% 72.97/73.03 inference(scs_inference,[],[9136,9010,8996,1,16,23,22,31,21,30])).
% 72.97/73.03 cnf(9187,plain,
% 72.97/73.03 (P1(f3(a1,a1))),
% 72.97/73.03 inference(scs_inference,[],[9136,9010,8996,1,16,23,22,31,21,30,18])).
% 72.97/73.03 cnf(9189,plain,
% 72.97/73.03 (P1(f11(a1,a1))),
% 72.97/73.03 inference(scs_inference,[],[9136,9010,8996,1,16,23,22,31,21,30,18,19])).
% 72.97/73.03 cnf(9191,plain,
% 72.97/73.03 (P4(a1,a1,f3(a1,a1))),
% 72.97/73.03 inference(scs_inference,[],[9136,9010,8996,1,16,23,22,31,21,30,18,19,25])).
% 72.97/73.03 cnf(9193,plain,
% 72.97/73.03 (~P4(a7,a7,a7)),
% 72.97/73.03 inference(scs_inference,[],[9136,9010,8996,9139,1,16,23,22,31,21,30,18,19,25,8911])).
% 72.97/73.03 cnf(9195,plain,
% 72.97/73.03 (P4(a1,f3(a7,a7),f3(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9136,9010,9168,8996,9139,1,16,23,22,31,21,30,18,19,25,8911,27])).
% 72.97/73.03 cnf(9197,plain,
% 72.97/73.03 (P2(a1,a1,f11(a1,a1))),
% 72.97/73.03 inference(scs_inference,[],[9136,9010,9168,8996,9139,1,16,23,22,31,21,30,18,19,25,8911,27,26])).
% 72.97/73.03 cnf(9214,plain,
% 72.97/73.03 (P1(f6(a4))),
% 72.97/73.03 inference(scs_inference,[],[2,16])).
% 72.97/73.03 cnf(9216,plain,
% 72.97/73.03 (P4(f6(a4),a4,a1)),
% 72.97/73.03 inference(scs_inference,[],[2,16,23])).
% 72.97/73.03 cnf(9218,plain,
% 72.97/73.03 (P2(a4,f3(a1,a1),f3(a1,a1))),
% 72.97/73.03 inference(scs_inference,[],[9187,2,16,23,22])).
% 72.97/73.03 cnf(9220,plain,
% 72.97/73.03 (P2(f3(a12,a12),a4,f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[9187,9141,2,16,23,22,31])).
% 72.97/73.03 cnf(9222,plain,
% 72.97/73.03 (P4(f3(a5,a5),a1,f3(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[9187,9141,9159,2,16,23,22,31,30])).
% 72.97/73.03 cnf(9224,plain,
% 72.97/73.03 (P4(a1,f3(a1,a1),f3(a1,a1))),
% 72.97/73.03 inference(scs_inference,[],[9187,9141,9159,2,16,23,22,31,30,21])).
% 72.97/73.03 cnf(9226,plain,
% 72.97/73.03 (P1(f3(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9187,9141,9159,2,16,23,22,31,30,21,18])).
% 72.97/73.03 cnf(9228,plain,
% 72.97/73.03 (P1(f11(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9187,9141,9159,2,16,23,22,31,30,21,18,19])).
% 72.97/73.03 cnf(9232,plain,
% 72.97/73.03 (P4(a4,a4,f3(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9187,9141,9159,9147,2,16,23,22,31,30,21,18,19,119,25])).
% 72.97/73.03 cnf(9234,plain,
% 72.97/73.03 (~P4(a2,a7,a2)),
% 72.97/73.03 inference(scs_inference,[],[9187,9141,9159,9147,9062,2,16,23,22,31,30,21,18,19,119,25,8911])).
% 72.97/73.03 cnf(9236,plain,
% 72.97/73.03 (P2(a4,a4,f11(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9187,9141,9159,9147,9062,2,16,23,22,31,30,21,18,19,119,25,8911,26])).
% 72.97/73.03 cnf(9238,plain,
% 72.97/73.03 (P4(a1,a2,a2)),
% 72.97/73.03 inference(scs_inference,[],[9187,9141,9159,9147,9062,2,59,16,23,22,31,30,21,18,19,119,25,8911,26,27])).
% 72.97/73.03 cnf(9242,plain,
% 72.97/73.03 (P4(a1,f3(a12,a12),a1)),
% 72.97/73.03 inference(scs_inference,[],[9174,9187,9141,9159,9147,9106,9000,9062,2,43,59,16,23,22,31,30,21,18,19,119,25,8911,26,27,32,33])).
% 72.97/73.03 cnf(9244,plain,
% 72.97/73.03 (P4(f3(a1,a1),a1,f3(a1,a1))),
% 72.97/73.03 inference(scs_inference,[],[9174,9187,9141,9159,9147,9106,9191,9000,9062,2,43,59,16,23,22,31,30,21,18,19,119,25,8911,26,27,32,33,34])).
% 72.97/73.03 cnf(9246,plain,
% 72.97/73.03 (P2(f10(a5),f11(a9,a5),a9)),
% 72.97/73.03 inference(scs_inference,[],[9174,9181,9187,9141,9159,9147,9106,9191,9000,9062,8950,464,2,43,59,16,23,22,31,30,21,18,19,119,25,8911,26,27,32,33,34,35])).
% 72.97/73.03 cnf(9250,plain,
% 72.97/73.03 (~P4(f6(a4),a4,a4)),
% 72.97/73.03 inference(scs_inference,[],[9174,9181,9187,9141,9159,9147,9106,9191,9000,9062,8950,464,2,43,59,16,23,22,31,30,21,18,19,119,25,8911,26,27,32,33,34,35,6696,8900])).
% 72.97/73.03 cnf(9254,plain,
% 72.97/73.03 (~P4(x92541,a5,a5)+~P2(x92541,a7,a7)),
% 72.97/73.03 inference(scs_inference,[],[9174,9181,9187,9141,9159,9147,9106,9191,9000,9062,8950,464,2,43,59,16,23,22,31,30,21,18,19,119,25,8911,26,27,32,33,34,35,6696,8900,6350,6366,6143])).
% 72.97/73.03 cnf(9255,plain,
% 72.97/73.03 (P3(f3(a4,a4),f3(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9174,9181,9187,9141,9159,9147,9106,9191,9000,9062,8950,464,2,43,59,16,23,22,31,30,21,18,19,119,25,8911,26,27,32,33,34,35,6696,8900,6350,6366,6143,112])).
% 72.97/73.03 cnf(9257,plain,
% 72.97/73.03 (P2(f11(a4,a4),a4,f11(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9174,9181,9187,9141,9159,9147,9106,9191,9000,9049,9062,8950,464,2,43,59,16,23,22,31,30,21,18,19,119,25,8911,26,27,32,33,34,35,6696,8900,6350,6366,6143,112,36])).
% 72.97/73.03 cnf(9268,plain,
% 72.97/73.03 (P4(a1,a12,a1)),
% 72.97/73.03 inference(scs_inference,[],[9246,5873])).
% 72.97/73.03 cnf(9270,plain,
% 72.97/73.03 (P2(a4,f6(a9),f6(a9))),
% 72.97/73.03 inference(scs_inference,[],[9025,22])).
% 72.97/73.03 cnf(9274,plain,
% 72.97/73.03 (P4(a1,f6(a9),f6(a9))),
% 72.97/73.03 inference(scs_inference,[],[9128,9025,22,31,21])).
% 72.97/73.03 cnf(9276,plain,
% 72.97/73.03 (P4(a2,a1,a2)),
% 72.97/73.03 inference(scs_inference,[],[9238,9128,9025,22,31,21,30])).
% 72.97/73.03 cnf(9280,plain,
% 72.97/73.03 (P4(a1,f3(a4,a4),f3(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9238,9242,9255,9128,9025,22,31,21,30,8911,27])).
% 72.97/73.03 cnf(9284,plain,
% 72.97/73.03 (P4(a12,a8,a8)),
% 72.97/73.03 inference(scs_inference,[],[8940,9185,9238,9242,9255,9128,9224,9025,43,22,31,21,30,8911,27,32,33])).
% 72.97/73.03 cnf(9286,plain,
% 72.97/73.03 (P4(f3(a1,a1),a8,a8)),
% 72.97/73.03 inference(scs_inference,[],[8940,9185,9238,9242,9255,9128,9224,9025,9191,43,22,31,21,30,8911,27,32,33,34])).
% 72.97/73.03 cnf(9288,plain,
% 72.97/73.03 (P2(a4,f11(a4,a4),f11(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[8940,9185,9238,9242,9255,9128,9224,9025,9236,9191,9049,43,22,31,21,30,8911,27,32,33,34,35])).
% 72.97/73.03 cnf(9290,plain,
% 72.97/73.03 (P2(a9,f10(a7),a2)),
% 72.97/73.03 inference(scs_inference,[],[9,8940,9185,9238,9242,9255,9128,9224,9025,9236,9191,9104,8938,9049,43,22,31,21,30,8911,27,32,33,34,35,36])).
% 72.97/73.03 cnf(9292,plain,
% 72.97/73.03 (~P2(a1,a7,f6(a4))),
% 72.97/73.03 inference(scs_inference,[],[9,8940,9185,9238,9250,9242,9255,9128,9224,9025,9183,9236,8994,9191,9104,8938,9049,43,22,31,21,30,8911,27,32,33,34,35,36,37])).
% 72.97/73.03 cnf(9300,plain,
% 72.97/73.03 (P2(a4,f3(a9,a9),f3(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9037,22])).
% 72.97/73.03 cnf(9302,plain,
% 72.97/73.03 (P2(f3(a1,a1),a4,f3(a1,a1))),
% 72.97/73.03 inference(scs_inference,[],[9218,9037,22,31])).
% 72.97/73.03 cnf(9304,plain,
% 72.97/73.03 (P4(a1,f11(a9,a9),f11(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9218,9037,9039,22,31,21])).
% 72.97/73.03 cnf(9306,plain,
% 72.97/73.03 (P4(a8,a12,a8)),
% 72.97/73.03 inference(scs_inference,[],[9284,9218,9037,9039,22,31,21,30])).
% 72.97/73.03 cnf(9310,plain,
% 72.97/73.03 (P4(a1,a5,a5)),
% 72.97/73.03 inference(scs_inference,[],[9284,9218,9037,9039,9216,66,22,31,21,30,8911,27])).
% 72.97/73.03 cnf(9312,plain,
% 72.97/73.03 (~P4(a5,f6(a1),f6(a1))),
% 72.97/73.03 inference(scs_inference,[],[9284,9177,9218,9037,9039,9216,41,66,22,31,21,30,8911,27,33])).
% 72.97/73.03 cnf(9314,plain,
% 72.97/73.03 (P4(a2,a12,a2)),
% 72.97/73.03 inference(scs_inference,[],[9268,9276,9284,9177,9218,9037,9039,9216,41,66,22,31,21,30,8911,27,33,34])).
% 72.97/73.03 cnf(9316,plain,
% 72.97/73.03 (P2(f11(a8,a8),f11(a4,a4),f11(a8,a8))),
% 72.97/73.03 inference(scs_inference,[],[9268,9276,9284,8964,9177,9218,9037,9039,9216,9236,41,66,22,31,21,30,8911,27,33,34,35])).
% 72.97/73.03 cnf(9320,plain,
% 72.97/73.03 (P2(f3(a9,a9),f10(a7),f3(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[9268,9276,9284,8964,9177,9288,9218,9037,9039,9290,9041,9216,9236,9076,41,66,22,31,21,30,8911,27,33,34,35,36,38])).
% 72.97/73.03 cnf(9328,plain,
% 72.97/73.03 (P2(a4,f6(a2),f6(a2))),
% 72.97/73.03 inference(scs_inference,[],[9060,22])).
% 72.97/73.03 cnf(9332,plain,
% 72.97/73.03 (P4(a1,f6(a2),f6(a2))),
% 72.97/73.03 inference(scs_inference,[],[9316,9060,22,31,21])).
% 72.97/73.03 cnf(9334,plain,
% 72.97/73.03 (P4(a5,a1,a5)),
% 72.97/73.03 inference(scs_inference,[],[9310,9316,9060,22,31,21,30])).
% 72.97/73.03 cnf(9336,plain,
% 72.97/73.03 (P4(a1,a7,a7)),
% 72.97/73.03 inference(scs_inference,[],[9310,9316,9060,71,22,31,21,30,27])).
% 72.97/73.03 cnf(9338,plain,
% 72.97/73.03 (P4(a8,f3(a12,a12),a8)),
% 72.97/73.03 inference(scs_inference,[],[9306,9310,9316,9060,9000,71,22,31,21,30,27,33])).
% 72.97/73.03 cnf(9342,plain,
% 72.97/73.03 (~P2(a12,a7,a7)),
% 72.97/73.03 inference(scs_inference,[],[9,9306,9310,9314,9316,9060,9177,9000,9116,13,71,22,31,21,30,27,33,34,37])).
% 72.97/73.03 cnf(9346,plain,
% 72.97/73.03 (P2(f10(a7),a7,f11(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9,9306,9310,9314,9316,9060,9179,9177,9000,9116,9104,8994,9236,13,71,22,31,21,30,27,33,34,37,2167,36])).
% 72.97/73.03 cnf(9350,plain,
% 72.97/73.03 (P2(a4,f6(a5),f6(a5))),
% 72.97/73.03 inference(scs_inference,[],[9098,22])).
% 72.97/73.03 cnf(9352,plain,
% 72.97/73.03 (P2(f10(a7),f3(a9,a9),f3(a2,a2))),
% 72.97/73.03 inference(scs_inference,[],[9320,9098,22,31])).
% 72.97/73.03 cnf(9354,plain,
% 72.97/73.03 (P4(a1,f6(a5),f6(a5))),
% 72.97/73.03 inference(scs_inference,[],[9320,9098,22,31,21])).
% 72.97/73.03 cnf(9356,plain,
% 72.97/73.03 (P4(a7,a1,a7)),
% 72.97/73.03 inference(scs_inference,[],[9336,9320,9098,22,31,21,30])).
% 72.97/73.03 cnf(9358,plain,
% 72.97/73.03 (P4(a1,a9,a9)),
% 72.97/73.03 inference(scs_inference,[],[9336,9320,9098,87,22,31,21,30,27])).
% 72.97/73.03 cnf(9360,plain,
% 72.97/73.03 (P4(f6(a8),a8,f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[9336,9320,9098,9338,8934,9045,87,22,31,21,30,27,33])).
% 72.97/73.03 cnf(9362,plain,
% 72.97/73.03 (P4(f3(a1,a1),a7,a7)),
% 72.97/73.03 inference(scs_inference,[],[9336,9320,9098,9338,8934,9045,9191,87,22,31,21,30,27,33,34])).
% 72.97/73.03 cnf(9364,plain,
% 72.97/73.03 (P2(a9,f11(a4,a4),a9)),
% 72.97/73.03 inference(scs_inference,[],[9,9336,9320,9098,9346,9338,8934,9045,9290,9191,87,22,31,21,30,27,33,34,35])).
% 72.97/73.03 cnf(9366,plain,
% 72.97/73.03 (P2(f11(a9,a5),f11(a4,a4),f11(a9,a5))),
% 72.97/73.03 inference(scs_inference,[],[9,9336,9320,9098,9346,9338,8934,9045,9181,9290,9191,87,22,31,21,30,27,33,34,35,36])).
% 72.97/73.03 cnf(9374,plain,
% 72.97/73.03 (P2(a4,f3(a5,a5),f3(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[9110,22])).
% 72.97/73.03 cnf(9378,plain,
% 72.97/73.03 (P4(a1,f11(a5,a5),f11(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[9366,9110,9112,22,31,21])).
% 72.97/73.03 cnf(9380,plain,
% 72.97/73.03 (P4(a9,a1,a9)),
% 72.97/73.03 inference(scs_inference,[],[9358,9366,9110,9112,22,31,21,30])).
% 72.97/73.03 cnf(9382,plain,
% 72.97/73.03 (P4(a1,a4,a4)),
% 72.97/73.03 inference(scs_inference,[],[9358,9366,9110,9112,54,22,31,21,30,27])).
% 72.97/73.03 cnf(9384,plain,
% 72.97/73.03 (P4(a12,a9,a9)),
% 72.97/73.03 inference(scs_inference,[],[9358,9366,9110,9112,9185,54,22,31,21,30,27,33])).
% 72.97/73.03 cnf(9386,plain,
% 72.97/73.03 (P4(a7,a12,a7)),
% 72.97/73.03 inference(scs_inference,[],[9356,9358,9366,9110,9112,9174,9185,54,22,31,21,30,27,33,34])).
% 72.97/73.03 cnf(9388,plain,
% 72.97/73.03 (P2(f11(a9,a9),f11(a4,a4),f11(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9356,9358,9366,9110,9112,9364,9174,9185,9047,54,22,31,21,30,27,33,34,36])).
% 72.97/73.03 cnf(9397,plain,
% 72.97/73.03 (P2(a4,f6(a7),f6(a7))),
% 72.97/73.03 inference(scs_inference,[],[9137,22])).
% 72.97/73.03 cnf(9401,plain,
% 72.97/73.03 (P4(a1,f6(a7),f6(a7))),
% 72.97/73.03 inference(scs_inference,[],[9388,9137,22,31,21])).
% 72.97/73.03 cnf(9403,plain,
% 72.97/73.03 (P4(a4,a1,a4)),
% 72.97/73.03 inference(scs_inference,[],[9382,9388,9137,22,31,21,30])).
% 72.97/73.03 cnf(9405,plain,
% 72.97/73.03 (P4(a1,a12,a12)),
% 72.97/73.03 inference(scs_inference,[],[9382,9388,9137,94,22,31,21,30,27])).
% 72.97/73.03 cnf(9409,plain,
% 72.97/73.03 (P4(f3(a12,a12),f3(a12,a12),f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[9382,9388,9378,9137,9360,9338,43,94,22,31,21,30,27,32,34])).
% 72.97/73.03 cnf(9425,plain,
% 72.97/73.03 (P2(a4,f3(a7,a7),f3(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9149,22])).
% 72.97/73.03 cnf(9429,plain,
% 72.97/73.03 (P4(a1,f11(a7,a7),f11(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9374,9149,9151,22,31,21])).
% 72.97/73.03 cnf(9431,plain,
% 72.97/73.03 (P4(a12,a1,a12)),
% 72.97/73.03 inference(scs_inference,[],[9405,9374,9149,9151,22,31,21,30])).
% 72.97/73.03 cnf(9439,plain,
% 72.97/73.03 (P4(f3(a4,a4),a1,f3(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9403,9405,9362,9374,9304,9149,9151,9332,9232,9139,43,22,31,21,30,119,8911,32,34])).
% 72.97/73.03 cnf(9441,plain,
% 72.97/73.03 (P4(f6(a12),a9,a9)),
% 72.97/73.03 inference(scs_inference,[],[9403,9405,9362,9374,9304,9149,9151,9332,9384,9232,8980,9358,9139,43,22,31,21,30,119,8911,32,34,33])).
% 72.97/73.03 cnf(9451,plain,
% 72.97/73.03 (~P4(a4,f6(a4),a4)),
% 72.97/73.03 inference(scs_inference,[],[9216,8915])).
% 72.97/73.03 cnf(9453,plain,
% 72.97/73.03 (P2(a4,f6(a1),f6(a1))),
% 72.97/73.03 inference(scs_inference,[],[9175,9216,8915,22])).
% 72.97/73.03 cnf(9457,plain,
% 72.97/73.03 (P4(a1,f6(a1),f6(a1))),
% 72.97/73.03 inference(scs_inference,[],[9425,9175,9216,8915,22,31,21])).
% 72.97/73.03 cnf(9459,plain,
% 72.97/73.03 (P4(f11(a7,a7),a1,f11(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9425,9429,9175,9216,8915,22,31,21,30])).
% 72.97/73.03 cnf(9461,plain,
% 72.97/73.03 (P4(a12,f3(a12,a12),a12)),
% 72.97/73.03 inference(scs_inference,[],[9431,9425,9429,9175,9242,9216,8915,22,31,21,30,34])).
% 72.97/73.03 cnf(9463,plain,
% 72.97/73.03 (P4(f3(a1,a1),f3(a7,a7),f3(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9431,9425,9429,9175,9362,9153,9242,9216,8915,22,31,21,30,34,33])).
% 72.97/73.03 cnf(9465,plain,
% 72.97/73.03 (P2(f3(a8,a8),a12,f3(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9431,9425,9429,9175,9143,9362,9153,9041,9242,8954,9216,8915,22,31,21,30,34,33,38])).
% 72.97/73.03 cnf(9467,plain,
% 72.97/73.03 (~P2(a12,f10(a5),a7)),
% 72.97/73.03 inference(scs_inference,[],[8952,9431,9425,9429,9175,9143,9362,9314,9153,9041,9242,8954,9216,11,8915,22,31,21,30,34,33,38,37])).
% 72.97/73.03 cnf(9476,plain,
% 72.97/73.03 (P2(a4,f6(a4),f6(a4))),
% 72.97/73.03 inference(scs_inference,[],[9214,22])).
% 72.97/73.03 cnf(9478,plain,
% 72.97/73.03 (P2(a12,f3(a8,a8),f3(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9465,9214,22,31])).
% 72.97/73.03 cnf(9480,plain,
% 72.97/73.03 (P4(a1,f11(a4,a4),f11(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9465,9214,9228,22,31,21])).
% 72.97/73.03 cnf(9482,plain,
% 72.97/73.03 (P4(f3(a7,a7),f3(a1,a1),f3(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9463,9465,9214,9228,22,31,21,30])).
% 72.97/73.03 cnf(9484,plain,
% 72.97/73.03 (P4(f6(a4),f3(a12,a12),f6(a4))),
% 72.97/73.03 inference(scs_inference,[],[9463,9465,9214,9228,9461,9167,22,31,21,30,34])).
% 72.97/73.03 cnf(9490,plain,
% 72.97/73.03 (P2(f3(a4,a4),f3(a12,a12),f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[9409,9463,9465,9214,9228,9461,9167,9274,9141,9027,198,9232,412,22,31,21,30,34,33,36,38])).
% 72.97/73.03 cnf(9501,plain,
% 72.97/73.03 (P2(a4,f3(a4,a4),f3(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9226,22])).
% 72.97/73.03 cnf(9503,plain,
% 72.97/73.03 (P2(f3(a12,a12),f3(a4,a4),f3(a12,a12))),
% 72.97/73.03 inference(scs_inference,[],[9490,9226,22,31])).
% 72.97/73.03 cnf(9505,plain,
% 72.97/73.03 (P4(a1,f11(a1,a1),f11(a1,a1))),
% 72.97/73.03 inference(scs_inference,[],[9490,9226,9189,22,31,21])).
% 72.97/73.03 cnf(9507,plain,
% 72.97/73.03 (P4(a9,f6(a12),a9)),
% 72.97/73.03 inference(scs_inference,[],[9490,9441,9226,9189,22,31,21,30])).
% 72.97/73.03 cnf(9511,plain,
% 72.97/73.03 (P4(f6(a8),a8,a12)),
% 72.97/73.03 inference(scs_inference,[],[9490,9441,9480,9226,9189,9405,9306,8934,43,22,31,21,30,32,33])).
% 72.97/73.03 cnf(9513,plain,
% 72.97/73.03 (P4(f3(a7,a7),a1,f3(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9490,9482,9441,9480,9226,9244,9189,9405,9306,8934,43,22,31,21,30,32,33,34])).
% 72.97/73.03 cnf(9524,plain,
% 72.97/73.03 (P2(a4,f11(a5,a5),f11(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[9112,22])).
% 72.97/73.03 cnf(9526,plain,
% 72.97/73.03 (P2(f3(a4,a4),a4,f3(a4,a4))),
% 72.97/73.03 inference(scs_inference,[],[9501,9112,22,31])).
% 72.97/73.03 cnf(9528,plain,
% 72.97/73.03 (P4(a1,f10(a5),f10(a5))),
% 72.97/73.03 inference(scs_inference,[],[9501,8948,9112,22,31,21])).
% 72.97/73.03 cnf(9530,plain,
% 72.97/73.03 (P4(f3(a12,a12),f6(a4),f6(a4))),
% 72.97/73.03 inference(scs_inference,[],[9484,9501,8948,9112,22,31,21,30])).
% 72.97/73.03 cnf(9532,plain,
% 72.97/73.03 (P4(a2,f3(a12,a12),a2)),
% 72.97/73.03 inference(scs_inference,[],[9484,9501,8948,9112,9461,9314,22,31,21,30,34])).
% 72.97/73.03 cnf(9534,plain,
% 72.97/73.03 (P4(f6(a12),f3(a9,a9),f3(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9484,9501,9441,8948,9112,9461,9314,9041,22,31,21,30,34,33])).
% 72.97/73.03 cnf(9544,plain,
% 72.97/73.03 (P2(a4,f11(a7,a7),f11(a7,a7))),
% 72.97/73.03 inference(scs_inference,[],[9151,22])).
% 72.97/73.03 cnf(9546,plain,
% 72.97/73.03 (P2(f11(a5,a5),a4,f11(a5,a5))),
% 72.97/73.03 inference(scs_inference,[],[9524,9151,22,31])).
% 72.97/73.03 cnf(9548,plain,
% 72.97/73.03 (P4(f3(a9,a9),f6(a12),f3(a9,a9))),
% 72.97/73.03 inference(scs_inference,[],[9534,9524,9151,22,31,30])).
% 72.97/73.03 cnf(9552,plain,
% 72.97/73.03 (P4(a1,f6(a12),a1)),
% 72.97/73.03 inference(scs_inference,[],[9507,9534,9524,9151,9027,9116,22,31,30,33,34])).
% 72.97/73.03 cnf(9556,plain,
% 72.97/73.03 (P2(f3(a4,a4),f11(a4,a4),f3(a4,a4))),
% 72.97/73.04 inference(scs_inference,[],[9526,9507,9534,9524,9151,9027,9116,9236,2,22,31,30,33,34,28,35])).
% 72.97/73.04 cnf(9566,plain,
% 72.97/73.04 (P2(f11(a4,a4),f3(a4,a4),f3(a4,a4))),
% 72.97/73.04 inference(scs_inference,[],[9556,9189,22,31])).
% 72.97/73.04 cnf(9568,plain,
% 72.97/73.04 (P4(f6(a12),a1,a1)),
% 72.97/73.04 inference(scs_inference,[],[9556,9552,9189,22,31,30])).
% 72.97/73.04 cnf(9570,plain,
% 72.97/73.04 (~P4(f6(a7),f3(a7,a7),a1)),
% 72.97/73.04 inference(scs_inference,[],[9556,9552,9189,9153,9139,22,31,30,8911])).
% 72.97/73.04 cnf(9572,plain,
% 72.97/73.04 (P2(f3(a12,a12),f11(a4,a4),f3(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[9556,9552,9503,9189,9153,9139,22,31,30,8911,36])).
% 72.97/73.04 cnf(9576,plain,
% 72.97/73.04 (P4(f3(a7,a7),f6(a12),f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[9556,9552,9513,9334,9503,9189,9153,9139,41,22,31,30,8911,36,33,34])).
% 72.97/73.04 cnf(9578,plain,
% 72.97/73.04 (P2(f3(a12,a12),a8,f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[9556,9552,9513,9334,9503,9189,9126,9153,9000,9041,9139,41,22,31,30,8911,36,33,34,38])).
% 72.97/73.04 cnf(9580,plain,
% 72.97/73.04 (~P2(x95801,a1,a1)+P2(x95801,f11(a1,a1),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9556,9552,9513,9197,9334,9503,9189,9126,9153,9000,9041,9139,41,22,31,30,8911,36,33,34,38,35])).
% 72.97/73.04 cnf(9584,plain,
% 72.97/73.04 (P2(a4,a5,a5)),
% 72.97/73.04 inference(scs_inference,[],[4,22])).
% 72.97/73.04 cnf(9586,plain,
% 72.97/73.04 (P2(f11(a4,a4),f3(a12,a12),f3(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[9572,4,22,31])).
% 72.97/73.04 cnf(9588,plain,
% 72.97/73.04 (P4(f6(a7),a1,f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[9572,9401,4,22,31,30])).
% 72.97/73.04 cnf(9590,plain,
% 72.97/73.04 (P2(f10(a5),f11(a5,a5),a5)),
% 72.97/73.04 inference(scs_inference,[],[9572,9401,9120,8950,4,22,31,30,35])).
% 72.97/73.04 cnf(9592,plain,
% 72.97/73.04 (P4(f6(a12),f6(a7),f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[9572,9401,9568,9120,8950,4,22,31,30,35,33])).
% 72.97/73.04 cnf(9594,plain,
% 72.97/73.04 (P4(f3(a2,a2),f3(a12,a12),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9572,9401,9568,9532,9120,9076,8950,4,22,31,30,35,33,34])).
% 72.97/73.04 cnf(9596,plain,
% 72.97/73.04 (P2(a5,a4,a5)),
% 72.97/73.04 inference(scs_inference,[],[9572,9401,9546,9568,9532,9120,9076,8950,4,22,31,30,35,33,34,36])).
% 72.97/73.04 cnf(9602,plain,
% 72.97/73.04 (P2(a4,a7,a7)),
% 72.97/73.04 inference(scs_inference,[],[5,22])).
% 72.97/73.04 cnf(9604,plain,
% 72.97/73.04 (P2(f6(a4),a4,f6(a4))),
% 72.97/73.04 inference(scs_inference,[],[9476,5,22,31])).
% 72.97/73.04 cnf(9608,plain,
% 72.97/73.04 (P2(f11(a4,a4),f3(a9,a9),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[9594,9586,9476,9578,5,22,31,30,35])).
% 72.97/73.04 cnf(9610,plain,
% 72.97/73.04 (P2(a12,f10(a7),a5)),
% 72.97/73.04 inference(scs_inference,[],[9596,9594,9586,9476,9578,9104,5,10,22,31,30,35,36])).
% 72.97/73.04 cnf(9612,plain,
% 72.97/73.04 (P4(f3(a12,a12),a12,a12)),
% 72.97/73.04 inference(scs_inference,[],[9596,9594,9586,9476,9578,9461,9000,9104,5,10,22,31,30,35,36,34])).
% 72.97/73.04 cnf(9614,plain,
% 72.97/73.04 (P4(f6(a12),f6(a1),f6(a1))),
% 72.97/73.04 inference(scs_inference,[],[9596,9594,9586,9457,9476,9578,9568,9461,9000,9104,5,10,22,31,30,35,36,34,33])).
% 72.97/73.04 cnf(9616,plain,
% 72.97/73.04 (P2(f3(a5,a5),a8,f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9596,9594,9586,9457,9476,9578,9568,9461,9114,9066,9000,9076,9104,5,10,22,31,30,35,36,34,33,38])).
% 72.97/73.04 cnf(9622,plain,
% 72.97/73.04 (~P4(a5,a4,a5)),
% 72.97/73.04 inference(scs_inference,[],[9155,9596,9594,9586,9457,9476,9578,9568,9461,9114,9066,9000,9076,9104,5,10,43,22,31,30,35,36,34,33,38,37,32,9170])).
% 72.97/73.04 cnf(9624,plain,
% 72.97/73.04 (~P4(a4,a5,a5)),
% 72.97/73.04 inference(scs_inference,[],[9155,9596,9594,9586,9457,9476,9578,9568,9461,9114,9066,9000,9076,9104,5,10,43,22,31,30,35,36,34,33,38,37,32,9170,9254])).
% 72.97/73.04 cnf(9628,plain,
% 72.97/73.04 (P2(a4,a1,a1)),
% 72.97/73.04 inference(scs_inference,[],[1,22])).
% 72.97/73.04 cnf(9632,plain,
% 72.97/73.04 (P4(f10(a5),a1,f10(a5))),
% 72.97/73.04 inference(scs_inference,[],[9602,9528,1,22,31,30])).
% 72.97/73.04 cnf(9636,plain,
% 72.97/73.04 (P2(f11(a4,a4),f3(a2,a2),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9602,9608,9528,9320,1,43,22,31,30,32,35])).
% 72.97/73.04 cnf(9640,plain,
% 72.97/73.04 (P4(f6(a12),f10(a5),f10(a5))),
% 72.97/73.04 inference(scs_inference,[],[9602,9608,9528,9312,9614,9320,9568,1,43,22,31,30,32,35,34,33])).
% 72.97/73.04 cnf(9644,plain,
% 72.97/73.04 (P2(f3(a4,a4),a7,f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[9602,9608,9528,9312,9614,9320,9568,9157,9153,9232,1,43,22,31,30,32,35,34,33,36,38])).
% 72.97/73.04 cnf(9652,plain,
% 72.97/73.04 (P2(a1,a4,a1)),
% 72.97/73.04 inference(scs_inference,[],[9628,31])).
% 72.97/73.04 cnf(9656,plain,
% 72.97/73.04 (P3(f6(a12),f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[9628,9576,9070,31,30,119])).
% 72.97/73.04 cnf(9658,plain,
% 72.97/73.04 (P2(f11(a4,a4),f3(a7,a7),f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[9628,9566,9576,9644,9070,31,30,119,35])).
% 72.97/73.04 cnf(9660,plain,
% 72.97/73.04 (P4(f3(a2,a2),a1,f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9628,9566,9576,9644,9070,9594,9068,31,30,119,35,34])).
% 72.97/73.04 cnf(9662,plain,
% 72.97/73.04 (P4(f3(a12,a12),a9,a9)),
% 72.97/73.04 inference(scs_inference,[],[9628,9566,9576,9644,9612,9070,9594,9068,9384,31,30,119,35,34,33])).
% 72.97/73.04 cnf(9664,plain,
% 72.97/73.04 (P2(f3(a4,a4),a1,a1)),
% 72.97/73.04 inference(scs_inference,[],[9628,9566,9576,9644,9612,9070,9594,9068,9384,8956,9232,31,30,119,35,34,33,38])).
% 72.97/73.04 cnf(9668,plain,
% 72.97/73.04 (P2(f3(a4,a4),f11(a1,a1),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9,9628,9566,9576,9644,9612,9070,9594,9068,9532,9384,8956,9116,9232,31,30,119,35,34,33,38,37,9580])).
% 72.97/73.04 cnf(9675,plain,
% 72.97/73.04 (P4(f6(a7),f6(a12),f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[9658,9592,31,30])).
% 72.97/73.04 cnf(9679,plain,
% 72.97/73.04 (P2(f11(a4,a4),f11(a1,a1),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9658,9668,9592,9566,9568,9336,31,30,8911,35])).
% 72.97/73.04 cnf(9681,plain,
% 72.97/73.04 (P4(f6(a2),a2,f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9658,9668,9592,9332,9566,9062,9191,9568,9336,31,30,8911,35,34])).
% 72.97/73.04 cnf(9683,plain,
% 72.97/73.04 (P4(f11(a7,a7),f3(a1,a1),f11(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[9658,9668,9459,9592,9332,9566,9062,9191,9568,9336,31,30,8911,35,34,33])).
% 72.97/73.04 cnf(9691,plain,
% 72.97/73.04 (P2(f11(a1,a1),f11(a4,a4),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9679,31])).
% 72.97/73.04 cnf(9693,plain,
% 72.97/73.04 (P4(f3(a1,a1),f11(a7,a7),f11(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[9679,9683,31,30])).
% 72.97/73.04 cnf(9695,plain,
% 72.97/73.04 (~P4(f6(a7),a1,a1)),
% 72.97/73.04 inference(scs_inference,[],[9679,9683,9336,9139,31,30,8911])).
% 72.97/73.04 cnf(9699,plain,
% 72.97/73.04 (P4(f3(a12,a12),a8,a8)),
% 72.97/73.04 inference(scs_inference,[],[9652,9679,9683,9284,9197,9336,9139,9000,31,30,8911,36,34])).
% 72.97/73.04 cnf(9701,plain,
% 72.97/73.04 (P4(a12,f10(a5),f10(a5))),
% 72.97/73.04 inference(scs_inference,[],[9652,9679,9683,9640,9284,9197,8986,9528,9336,9139,9000,31,30,8911,36,34,33])).
% 72.97/73.04 cnf(9703,plain,
% 72.97/73.04 (~P2(f3(a12,a12),a4,a7)),
% 72.97/73.04 inference(scs_inference,[],[9084,9652,9679,9683,9640,9612,9284,9197,8986,9528,9336,9139,9000,412,31,30,8911,36,34,33,37])).
% 72.97/73.04 cnf(9710,plain,
% 72.97/73.04 (P4(a8,f6(a8),a12)),
% 72.97/73.04 inference(scs_inference,[],[9636,9511,31,30])).
% 72.97/73.04 cnf(9712,plain,
% 72.97/73.04 (P4(f11(a8,a8),a12,f11(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9636,9145,9511,9268,31,30,34])).
% 72.97/73.04 cnf(9714,plain,
% 72.97/73.04 (P4(f6(a1),f3(a2,a2),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9636,9145,9511,9118,9268,9177,31,30,34,33])).
% 72.97/73.04 cnf(9718,plain,
% 72.97/73.04 (~P4(f10(a5),a4,a4)),
% 72.97/73.04 inference(scs_inference,[],[9624,9636,9145,9511,9703,9118,9220,9584,9409,9268,9177,8950,31,30,34,33,38,37])).
% 72.97/73.04 cnf(9724,plain,
% 72.97/73.04 (P2(f6(a2),a4,f6(a2))),
% 72.97/73.04 inference(scs_inference,[],[9328,31])).
% 72.97/73.04 cnf(9726,plain,
% 72.97/73.04 (P4(f3(a2,a2),f6(a1),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9328,9714,31,30])).
% 72.97/73.04 cnf(9728,plain,
% 72.97/73.04 (P4(f3(a1,a1),f3(a12,a12),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9328,9714,9681,9532,31,30,34])).
% 72.97/73.04 cnf(9732,plain,
% 72.97/73.04 (P2(f3(a4,a4),a1,f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9328,9714,9681,9664,9505,9614,9439,9532,9197,31,30,34,33,38])).
% 72.97/73.04 cnf(9734,plain,
% 72.97/73.04 (~P2(a1,a1,f6(a5))),
% 72.97/73.04 inference(scs_inference,[],[9328,9714,9681,9664,9505,9614,9161,9439,9532,9197,31,30,34,33,38,37])).
% 72.97/73.04 cnf(9743,plain,
% 72.97/73.04 (P2(f6(a5),a4,f6(a5))),
% 72.97/73.04 inference(scs_inference,[],[9350,31])).
% 72.97/73.04 cnf(9745,plain,
% 72.97/73.04 (P4(f3(a12,a12),f3(a1,a1),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9728,9350,31,30])).
% 72.97/73.04 cnf(9749,plain,
% 72.97/73.04 (P4(f11(a7,a7),f3(a12,a12),f11(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[9728,9350,9683,9401,31,30,119,34])).
% 72.97/73.04 cnf(9751,plain,
% 72.97/73.04 (P4(f3(a1,a1),a12,a12)),
% 72.97/73.04 inference(scs_inference,[],[9728,9350,9710,9286,9683,9401,31,30,119,34,33])).
% 72.97/73.04 cnf(9755,plain,
% 72.97/73.04 (P4(f11(a1,a1),f11(a1,a1),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9728,9350,9732,9710,9286,8972,9683,9220,9401,9652,9242,9439,9197,31,30,119,34,33,38,37])).
% 72.97/73.04 cnf(9764,plain,
% 72.97/73.04 (P2(f6(a7),a4,f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[9397,31])).
% 72.97/73.04 cnf(9766,plain,
% 72.97/73.04 (P4(f3(a12,a12),f11(a7,a7),f11(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[9749,9397,31,30])).
% 72.97/73.04 cnf(9768,plain,
% 72.97/73.04 (P4(f3(a2,a2),f6(a12),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9749,9397,9660,9552,31,30,34])).
% 72.97/73.04 cnf(9770,plain,
% 72.97/73.04 (P4(f3(a1,a1),f10(a5),f10(a5))),
% 72.97/73.04 inference(scs_inference,[],[9749,9397,9660,9751,9701,9552,31,30,34,33])).
% 72.97/73.04 cnf(9772,plain,
% 72.97/73.04 (~P4(f3(a12,a12),a1,a7)),
% 72.97/73.04 inference(scs_inference,[],[9749,9397,9660,9751,9701,9703,9068,9220,9652,9552,31,30,34,33,38])).
% 72.97/73.04 cnf(9779,plain,
% 72.97/73.04 (P2(a8,f3(a5,a5),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9616,31])).
% 72.97/73.04 cnf(9781,plain,
% 72.97/73.04 (P4(a12,f11(a8,a8),f11(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9712,9616,31,30])).
% 72.97/73.04 cnf(9783,plain,
% 72.97/73.04 (P2(f11(a4,a4),f11(a7,a7),f11(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[9712,9544,9616,9236,31,30,36])).
% 72.97/73.04 cnf(9785,plain,
% 72.97/73.04 (P4(f11(a8,a8),f3(a12,a12),f11(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9712,9544,9616,9000,9236,31,30,36,33])).
% 72.97/73.04 cnf(9787,plain,
% 72.97/73.04 (P2(f3(a9,a9),f11(a4,a4),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[9712,9544,9616,9364,9041,9000,9236,31,30,36,33,38])).
% 72.97/73.04 cnf(9800,plain,
% 72.97/73.04 (P2(f10(a5),a5,f11(a4,a4))),
% 72.97/73.04 inference(scs_inference,[],[9785,9783,8956,9029,9139,8950,9236,31,30,8911,36])).
% 72.97/73.04 cnf(9802,plain,
% 72.97/73.04 (P4(f3(a12,a12),f10(a5),f10(a5))),
% 72.97/73.04 inference(scs_inference,[],[9785,9783,9745,9770,8956,9029,9139,8950,9236,31,30,8911,36,33])).
% 72.97/73.04 cnf(9804,plain,
% 72.97/73.04 (P4(f10(a5),a12,f10(a5))),
% 72.97/73.04 inference(scs_inference,[],[9785,9783,9745,9632,9770,9136,8956,9029,9139,8950,9236,31,30,8911,36,33,34])).
% 72.97/73.04 cnf(9811,plain,
% 72.97/73.04 (P2(a5,f10(a5),f11(a4,a4))),
% 72.97/73.04 inference(scs_inference,[],[9800,31])).
% 72.97/73.04 cnf(9813,plain,
% 72.97/73.04 (P4(f10(a5),f3(a12,a12),f10(a5))),
% 72.97/73.04 inference(scs_inference,[],[9802,9800,31,30])).
% 72.97/73.04 cnf(9815,plain,
% 72.97/73.04 (P4(f3(a1,a1),f11(a8,a8),f11(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9802,9800,9781,9751,31,30,33])).
% 72.97/73.04 cnf(9817,plain,
% 72.97/73.04 (P4(f3(a8,a8),a12,f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9802,9800,9781,9035,9751,9174,31,30,33,34])).
% 72.97/73.04 cnf(9819,plain,
% 72.97/73.04 (~P4(a1,a12,a7)),
% 72.97/73.04 inference(scs_inference,[],[9802,9800,9781,9035,9751,8972,9174,9652,412,31,30,33,34,38])).
% 72.97/73.04 cnf(9821,plain,
% 72.97/73.04 (~P2(a5,a4,f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[9802,9800,9122,9743,9781,9035,9751,8972,9174,9100,9652,412,31,30,33,34,38,37])).
% 72.97/73.04 cnf(9826,plain,
% 72.97/73.04 (P2(f6(a9),a4,f6(a9))),
% 72.97/73.04 inference(scs_inference,[],[9270,31])).
% 72.97/73.04 cnf(9828,plain,
% 72.97/73.04 (P4(f11(a8,a8),f3(a1,a1),f11(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9815,9270,31,30])).
% 72.97/73.04 cnf(9832,plain,
% 72.97/73.04 (P4(f3(a8,a8),f3(a12,a12),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9815,9817,9292,9604,9270,8994,9000,31,30,36,33])).
% 72.97/73.04 cnf(9834,plain,
% 72.97/73.04 (P4(a12,a12,a12)),
% 72.97/73.04 inference(scs_inference,[],[9815,9817,9292,9604,9270,9511,9306,8994,9000,31,30,36,33,34])).
% 72.97/73.04 cnf(9836,plain,
% 72.97/73.04 (~P4(f11(a1,a1),f11(a1,a1),f6(a5))),
% 72.97/73.04 inference(scs_inference,[],[9815,9817,9292,9734,9604,9270,9511,9306,8956,9197,8994,9000,31,30,36,33,34,38])).
% 72.97/73.04 cnf(9838,plain,
% 72.97/73.04 (~P2(a12,a4,a7)),
% 72.97/73.04 inference(scs_inference,[],[9819,9815,9817,9292,9734,9604,9270,9511,9405,9306,8956,9197,8994,9652,9000,412,31,30,36,33,34,38,37])).
% 72.97/73.04 cnf(9840,plain,
% 72.97/73.04 (P4(f11(a9,a5),f11(a9,a5),f11(a9,a5))),
% 72.97/73.04 inference(scs_inference,[],[9819,9815,9817,9292,9734,9604,9270,9511,9405,9306,8956,9197,8994,9652,9000,412,31,30,36,33,34,38,37,4773])).
% 72.97/73.04 cnf(9849,plain,
% 72.97/73.04 (P2(f6(a1),a4,f6(a1))),
% 72.97/73.04 inference(scs_inference,[],[9453,31])).
% 72.97/73.04 cnf(9851,plain,
% 72.97/73.04 (P4(f3(a12,a12),f3(a8,a8),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9832,9453,31,30])).
% 72.97/73.04 cnf(9853,plain,
% 72.97/73.04 (P2(f11(a4,a4),f11(a5,a5),f11(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[9832,9453,9811,9120,9590,31,30,36])).
% 72.97/73.04 cnf(9855,plain,
% 72.97/73.04 (P4(f6(a12),a12,a12)),
% 72.97/73.04 inference(scs_inference,[],[9834,9832,9453,9811,9120,9590,9405,8980,31,30,36,33])).
% 72.97/73.04 cnf(9857,plain,
% 72.97/73.04 (P4(f3(a5,a5),a12,f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[9834,9832,9222,9453,9811,9120,9590,9405,9268,8980,31,30,36,33,34])).
% 72.97/73.04 cnf(9859,plain,
% 72.97/73.04 (P2(a12,a8,f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[9834,9832,9222,9453,9811,9120,9590,9126,9405,9268,8980,9041,31,30,36,33,34,38])).
% 72.97/73.04 cnf(9867,plain,
% 72.97/73.04 (P2(f11(a5,a5),f11(a4,a4),f11(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[9853,31])).
% 72.97/73.04 cnf(9869,plain,
% 72.97/73.04 (P4(a12,f3(a5,a5),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[9853,9857,31,30])).
% 72.97/73.04 cnf(9871,plain,
% 72.97/73.04 (P2(a7,f3(a2,a2),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[9853,9857,9300,9352,9104,31,30,35])).
% 72.97/73.04 cnf(9873,plain,
% 72.97/73.04 (P4(f6(a12),f6(a8),f6(a8))),
% 72.97/73.04 inference(scs_inference,[],[9853,9857,8988,9300,9352,9568,9104,31,30,35,33])).
% 72.97/73.04 cnf(9875,plain,
% 72.97/73.04 (P4(f3(a1,a1),f6(a8),f6(a8))),
% 72.97/73.04 inference(scs_inference,[],[9853,9857,8988,9300,9352,9568,9191,9104,31,30,35,33,34])).
% 72.97/73.04 cnf(9877,plain,
% 72.97/73.04 (~P4(f3(a1,a1),a12,a7)),
% 72.97/73.04 inference(scs_inference,[],[9838,9853,9857,8988,9300,9302,9352,9751,9568,9191,9104,412,31,30,35,33,34,38])).
% 72.97/73.04 cnf(9879,plain,
% 72.97/73.04 (P4(f3(a2,a2),f3(a9,a9),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9838,9853,9857,9859,8988,9300,9302,9352,9616,9751,9568,9191,9104,412,31,30,35,33,34,38,37])).
% 72.97/73.04 cnf(9884,plain,
% 72.97/73.04 (P2(f3(a2,a2),a7,f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[9871,31])).
% 72.97/73.04 cnf(9886,plain,
% 72.97/73.04 (P4(f3(a9,a9),f3(a2,a2),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9879,9871,31,30])).
% 72.97/73.04 cnf(9888,plain,
% 72.97/73.04 (P2(f11(a1,a1),a1,f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9879,9871,9732,9668,9197,31,30,36])).
% 72.97/73.04 cnf(9890,plain,
% 72.97/73.04 (P4(f6(a12),f3(a5,a5),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[9879,9869,9871,9855,9732,9668,9197,31,30,36,33])).
% 72.97/73.04 cnf(9892,plain,
% 72.97/73.04 (P4(f6(a8),a8,f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9879,9869,9871,9875,9855,9360,9732,9728,9668,9197,31,30,36,33,34])).
% 72.97/73.04 cnf(9894,plain,
% 72.97/73.04 (~P4(a5,a1,f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[9879,9869,9871,9875,9855,9821,9360,9596,9732,9334,9728,9668,9197,9652,31,30,36,33,34,38])).
% 72.97/73.04 cnf(9903,plain,
% 72.97/73.04 (P2(a1,f11(a1,a1),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9888,31])).
% 72.97/73.04 cnf(9905,plain,
% 72.97/73.04 (P4(f3(a5,a5),f6(a12),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[9890,9888,31,30])).
% 72.97/73.04 cnf(9907,plain,
% 72.97/73.04 (~P2(f11(a4,a4),a5,f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[9890,9888,9811,9821,8950,31,30,35])).
% 72.97/73.04 cnf(9909,plain,
% 72.97/73.04 (P2(f11(a4,a4),f11(a2,a2),f11(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[9890,9888,9102,9811,9821,8950,9236,31,30,35,36])).
% 72.97/73.04 cnf(9911,plain,
% 72.97/73.04 (P4(f6(a12),f3(a1,a1),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9890,9888,9873,9892,9102,9811,9821,8950,9236,31,30,35,36,33])).
% 72.97/73.04 cnf(9913,plain,
% 72.97/73.04 (P4(f3(a9,a9),f3(a12,a12),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[9890,9888,9873,9892,9108,9102,9811,9821,9242,8950,9236,31,30,35,36,33,34])).
% 72.97/73.04 cnf(9915,plain,
% 72.97/73.04 (P2(f3(a1,a1),a1,f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9890,9888,9873,9892,9108,9102,9755,9811,9821,9242,9191,9197,8950,9236,31,30,35,36,33,34,38])).
% 72.97/73.04 cnf(9922,plain,
% 72.97/73.04 (P4(f3(a12,a12),f3(a9,a9),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[9913,9909,31,30])).
% 72.97/73.04 cnf(9924,plain,
% 72.97/73.04 (P2(f11(a1,a1),f11(a1,a1),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9913,9909,9888,9197,31,30,35])).
% 72.97/73.04 cnf(9926,plain,
% 72.97/73.04 (P2(a5,f11(a4,a4),a5)),
% 72.97/73.04 inference(scs_inference,[],[9913,9909,9867,9888,9590,9197,31,30,35,36])).
% 72.97/73.04 cnf(9928,plain,
% 72.97/73.04 (P4(f6(a1),f3(a7,a7),f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[9913,9909,9867,9195,9888,9590,9177,9197,31,30,35,36,33])).
% 72.97/73.04 cnf(9932,plain,
% 72.97/73.04 (P2(f3(a4,a4),a8,f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9913,9909,9867,9195,9193,9888,9362,8954,9590,9177,9232,9197,722,31,30,35,36,33,34,38])).
% 72.97/73.04 cnf(9934,plain,
% 72.97/73.04 (~P2(a1,a1,f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[9913,9909,9867,9695,9195,9280,9193,9888,9362,9664,8954,9590,9177,9232,9197,722,31,30,35,36,33,34,38,37])).
% 72.97/73.04 cnf(9939,plain,
% 72.97/73.04 (P2(a1,f3(a1,a1),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9915,31])).
% 72.97/73.04 cnf(9943,plain,
% 72.97/73.04 (P2(a2,f11(a4,a4),a2)),
% 72.97/73.04 inference(scs_inference,[],[9928,9915,9926,9051,31,30,36])).
% 72.97/73.04 cnf(9945,plain,
% 72.97/73.04 (P4(f6(a12),f11(a8,a8),f11(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9928,9915,9926,9911,9815,9051,31,30,36,33])).
% 72.97/73.04 cnf(9947,plain,
% 72.97/73.04 (P4(f3(a1,a1),a12,f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9928,9915,9926,9911,9815,9681,9051,9314,31,30,36,33,34])).
% 72.97/73.04 cnf(9954,plain,
% 72.97/73.04 (P2(f11(a4,a4),a2,a2)),
% 72.97/73.04 inference(scs_inference,[],[9943,31])).
% 72.97/73.04 cnf(9960,plain,
% 72.97/73.04 (P2(f11(a1,a1),f3(a1,a1),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9924,9945,9939,9943,9888,9185,9139,31,30,8911,36])).
% 72.97/73.04 cnf(9962,plain,
% 72.97/73.04 (P4(f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9924,9945,9939,9943,9875,9888,9892,9185,9139,31,30,8911,36,33])).
% 72.97/73.04 cnf(9964,plain,
% 72.97/73.04 (P4(f11(a7,a7),f6(a12),f11(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[9924,9945,9939,9943,9875,9459,9888,9892,9552,9185,9139,31,30,8911,36,33,34])).
% 72.97/73.04 cnf(9970,plain,
% 72.97/73.04 (P2(a8,f11(a4,a4),a8)),
% 72.97/73.04 inference(scs_inference,[],[9924,9945,9939,9943,9826,9836,9875,9459,9888,9892,9755,8972,9027,9552,9185,9139,3670,31,30,8911,36,33,34,38,37,301])).
% 72.97/73.04 cnf(9972,plain,
% 72.97/73.04 (P2(f11(a4,a4),a8,a8)),
% 72.97/73.04 inference(scs_inference,[],[9924,9945,9939,9943,9826,9836,9875,9459,9888,9892,9755,8972,9027,9552,9185,9139,3670,31,30,8911,36,33,34,38,37,301,89])).
% 72.97/73.04 cnf(9978,plain,
% 72.97/73.04 (P2(f3(a1,a1),f11(a1,a1),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9960,31])).
% 72.97/73.04 cnf(9984,plain,
% 72.97/73.04 (P2(f3(a8,a8),f11(a4,a4),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9,9960,9964,9954,9970,9932,31,30,35,36])).
% 72.97/73.04 cnf(9986,plain,
% 72.97/73.04 (P4(f6(a12),f3(a8,a8),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9,9960,9964,9954,9970,9932,9004,9568,31,30,35,36,33])).
% 72.97/73.04 cnf(9990,plain,
% 72.97/73.04 (P2(f3(a5,a5),f11(a4,a4),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[9,9960,9964,9877,9954,9970,9932,9855,9004,9926,9114,9386,9568,31,30,35,36,33,34,38])).
% 72.97/73.04 cnf(9998,plain,
% 72.97/73.04 (P4(f3(a8,a8),f6(a12),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[9984,9986,31,30])).
% 72.97/73.04 cnf(10000,plain,
% 72.97/73.04 (P2(f11(a4,a4),a5,a5)),
% 72.97/73.04 inference(scs_inference,[],[9984,9986,9800,9926,9811,31,30,36])).
% 72.97/73.04 cnf(10002,plain,
% 72.97/73.04 (P4(f6(a8),f3(a8,a8),a8)),
% 72.97/73.04 inference(scs_inference,[],[9984,9986,9800,9699,9360,8954,9926,9811,31,30,36,33])).
% 72.97/73.04 cnf(10004,plain,
% 72.97/73.04 (P4(a9,a12,a9)),
% 72.97/73.04 inference(scs_inference,[],[9984,9986,9380,9800,9699,9360,8954,9926,9136,9811,31,30,36,33,34])).
% 72.97/73.04 cnf(10006,plain,
% 72.97/73.04 (P2(f3(a4,a4),f3(a1,a1),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[9984,9986,9962,9380,9800,9699,9218,9360,8954,9926,9136,9811,9232,31,30,36,33,34,38])).
% 72.97/73.04 cnf(10010,plain,
% 72.97/73.04 (P2(f11(a4,a4),a12,a12)),
% 72.97/73.04 inference(scs_inference,[],[9984,9990,9986,9894,9962,9380,9800,9699,9218,9360,8954,9926,9114,9136,9811,9232,31,30,36,33,34,38,37,82])).
% 72.97/73.04 cnf(10017,plain,
% 72.97/73.04 (P2(f3(a1,a1),f3(a4,a4),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10006,31])).
% 72.97/73.04 cnf(10019,plain,
% 72.97/73.04 (P4(f3(a8,a8),f6(a8),a8)),
% 72.97/73.04 inference(scs_inference,[],[10006,10002,31,30])).
% 72.97/73.04 cnf(10021,plain,
% 72.97/73.04 (P2(f11(a4,a4),f11(a12,a12),f11(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[10006,10002,10010,9002,31,30,35])).
% 72.97/73.04 cnf(10023,plain,
% 72.97/73.04 (P4(f6(a12),a8,a8)),
% 72.97/73.04 inference(scs_inference,[],[10006,10002,10010,9002,9873,31,30,35,33])).
% 72.97/73.04 cnf(10025,plain,
% 72.97/73.04 (P4(a8,f6(a12),a8)),
% 72.97/73.04 inference(scs_inference,[],[10006,9998,10002,10010,9002,9873,31,30,35,33,34])).
% 72.97/73.04 cnf(10027,plain,
% 72.97/73.04 (~P4(f11(a4,a4),f11(a4,a4),f11(a4,a4))),
% 72.97/73.04 inference(scs_inference,[],[10006,9907,9998,10002,10000,10010,9002,9873,9114,31,30,35,33,34,38])).
% 72.97/73.04 cnf(10029,plain,
% 72.97/73.04 (P4(f3(a1,a1),f11(a1,a1),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10006,9907,9998,10002,10000,10010,9002,9939,9873,9439,9114,31,30,35,33,34,38,37])).
% 72.97/73.04 cnf(10038,plain,
% 72.97/73.04 (P4(f11(a1,a1),f3(a1,a1),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10021,10029,31,30])).
% 72.97/73.04 cnf(10040,plain,
% 72.97/73.04 (P2(f10(a7),a4,f10(a7))),
% 72.97/73.04 inference(scs_inference,[],[10021,10029,9179,8994,9104,31,30,35])).
% 72.97/73.04 cnf(10044,plain,
% 72.97/73.04 (P2(f11(a1,a1),f3(a4,a4),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10017,10021,10029,9960,9033,9179,9177,8994,9104,31,30,35,33,36])).
% 72.97/73.04 cnf(10046,plain,
% 72.97/73.04 (P4(f11(a8,a8),f11(a1,a1),f11(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[10017,10021,10029,9828,9960,9033,9179,9177,8994,9104,31,30,35,33,36,34])).
% 72.97/73.04 cnf(10050,plain,
% 72.97/73.04 (~P2(f11(a1,a1),f11(a4,a4),f6(a5))),
% 72.97/73.04 inference(scs_inference,[],[10017,10021,10029,9828,9691,9960,9743,9033,9836,9179,9596,9755,8972,9100,9177,8994,9104,31,30,35,33,36,34,38,37])).
% 72.97/73.04 cnf(10059,plain,
% 72.97/73.04 (P2(f11(a4,a4),f3(a5,a5),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[10046,9990,30,31])).
% 72.97/73.04 cnf(10061,plain,
% 72.97/73.04 (P2(f3(a12,a12),f3(a8,a8),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10046,9990,9932,9578,9503,30,31,35])).
% 72.97/73.04 cnf(10065,plain,
% 72.97/73.04 (P4(f11(a1,a1),f11(a7,a7),f11(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[10038,10046,9990,9877,9932,9693,9578,9503,9751,30,31,35,34,33])).
% 72.97/73.04 cnf(10067,plain,
% 72.97/73.04 (~P2(a12,a5,f11(a4,a4))),
% 72.97/73.04 inference(scs_inference,[],[10027,10038,10046,9804,9990,9877,9932,9693,9800,9578,9503,9751,30,31,35,34,33,37])).
% 72.97/73.04 cnf(10076,plain,
% 72.97/73.04 (P2(f3(a8,a8),f3(a12,a12),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10061,10065,30,31])).
% 72.97/73.04 cnf(10078,plain,
% 72.97/73.04 (P2(f11(a4,a4),f10(a7),f10(a7))),
% 72.97/73.04 inference(scs_inference,[],[10061,10065,10040,9346,9104,30,31,36])).
% 72.97/73.04 cnf(10080,plain,
% 72.97/73.04 (P4(f3(a2,a2),a12,f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10061,10065,10040,9660,9346,9268,9104,30,31,36,34])).
% 72.97/73.04 cnf(10082,plain,
% 72.97/73.04 (P4(f3(a12,a12),f3(a5,a5),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[10061,10065,10040,9660,9869,9346,9612,9268,9104,30,31,36,34,33])).
% 72.97/73.04 cnf(10086,plain,
% 72.97/73.04 (~P4(f11(a1,a1),f11(a1,a1),f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[10061,10065,10040,9718,9934,9660,9869,9346,9612,9183,9268,8956,8994,9104,9197,30,31,36,34,33,37,38])).
% 72.97/73.04 cnf(10090,plain,
% 72.97/73.04 (P2(f10(a7),f11(a4,a4),f10(a7))),
% 72.97/73.04 inference(scs_inference,[],[10082,10078,30,31])).
% 72.97/73.04 cnf(10092,plain,
% 72.97/73.04 (P2(f11(a4,a4),a4,a4)),
% 72.97/73.04 inference(scs_inference,[],[10082,10078,8994,30,31,35])).
% 72.97/73.04 cnf(10094,plain,
% 72.97/73.04 (P4(f3(a7,a7),a12,f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[10082,10078,9947,9482,8994,30,31,35,34])).
% 72.97/73.04 cnf(10098,plain,
% 72.97/73.04 (P4(f3(a9,a9),f3(a9,a9),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10082,10078,9947,10061,9082,9482,9409,9185,8994,30,31,35,34,33,37])).
% 72.97/73.04 cnf(10102,plain,
% 72.97/73.04 (P2(a12,f11(a4,a4),a12)),
% 72.97/73.04 inference(scs_inference,[],[10082,10078,9849,9947,10061,9082,9482,9409,8972,9185,9177,8994,9652,30,31,35,34,33,37,38,538])).
% 72.97/73.04 cnf(10109,plain,
% 72.97/73.04 (P2(a4,f11(a4,a4),a4)),
% 72.97/73.04 inference(scs_inference,[],[10080,10092,30,31])).
% 72.97/73.04 cnf(10111,plain,
% 72.97/73.04 (~P2(a7,a12,a7)),
% 72.97/73.04 inference(scs_inference,[],[10,10080,10092,9342,3660,30,31,36])).
% 72.97/73.04 cnf(10113,plain,
% 72.97/73.04 (P2(f11(a4,a4),f6(a7),f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[10,10080,10092,9342,9397,3660,30,31,36,35])).
% 72.97/73.04 cnf(10115,plain,
% 72.97/73.04 (P4(f6(a4),a4,f3(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[10,10080,10092,9530,9342,9397,9068,9216,3660,30,31,36,35,34])).
% 72.97/73.04 cnf(10117,plain,
% 72.97/73.04 (P4(f6(a2),f3(a2,a2),a2)),
% 72.97/73.04 inference(scs_inference,[],[10,10080,10092,9530,9342,9397,9238,9068,9062,9076,9216,3660,30,31,36,35,34,33])).
% 72.97/73.04 cnf(10121,plain,
% 72.97/73.04 (P2(a4,a1,f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10,9451,10080,10092,9530,9342,9397,9604,9238,9505,9068,9628,9062,9076,9216,9403,9197,3660,30,31,36,35,34,33,37,38])).
% 72.97/73.04 cnf(10123,plain,
% 72.97/73.04 (~P4(f3(a12,a12),a1,a5)),
% 72.97/73.04 inference(scs_inference,[],[10,9451,10080,10092,9530,9342,9397,9604,9238,9505,9068,9628,9062,9076,9216,9403,9197,3660,30,31,36,35,34,33,37,38,3838])).
% 72.97/73.04 cnf(10127,plain,
% 72.97/73.04 (~P4(f6(a12),f6(a7),a1)),
% 72.97/73.04 inference(scs_inference,[],[10,9451,10080,10092,9530,9342,9397,9604,9238,9505,9068,9628,9062,9076,9216,9403,9568,9139,9197,3660,30,31,36,35,34,33,37,38,3838,2294,8911])).
% 72.97/73.04 cnf(10131,plain,
% 72.97/73.04 (P4(a4,f6(a4),f3(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[10115,30])).
% 72.97/73.04 cnf(10135,plain,
% 72.97/73.04 (P2(f3(a9,a9),f3(a4,a4),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10076,10113,10115,9503,30,31,36])).
% 72.97/73.04 cnf(10137,plain,
% 72.97/73.04 (P2(f10(a5),a12,a7)),
% 72.97/73.04 inference(scs_inference,[],[10,10076,10113,10115,9503,9602,8950,30,31,36,35])).
% 72.97/73.04 cnf(10139,plain,
% 72.97/73.04 (P4(a2,f6(a1),a2)),
% 72.97/73.04 inference(scs_inference,[],[10,10076,10113,10115,10117,9726,9503,9602,8950,30,31,36,35,34])).
% 72.97/73.04 cnf(10141,plain,
% 72.97/73.04 (P4(f6(a8),a8,f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10,10076,10113,10115,10117,10025,9726,9070,9503,8934,9602,8950,30,31,36,35,34,33])).
% 72.97/73.04 cnf(10143,plain,
% 72.97/73.04 (~P2(a7,a4,f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[10,10076,9570,10113,10115,10117,10025,9764,9726,9070,9503,8934,9602,8950,9139,9652,30,31,36,35,34,33,37])).
% 72.97/73.04 cnf(10155,plain,
% 72.97/73.04 (P4(a8,f6(a8),f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10141,30])).
% 72.97/73.04 cnf(10157,plain,
% 72.97/73.04 (P2(f3(a4,a4),f3(a9,a9),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10135,10141,30,31])).
% 72.97/73.04 cnf(10161,plain,
% 72.97/73.04 (P2(f11(a4,a4),f6(a2),f6(a2))),
% 72.97/73.04 inference(scs_inference,[],[10135,10102,10141,10137,9328,10092,30,31,36,35])).
% 72.97/73.04 cnf(10163,plain,
% 72.97/73.04 (P4(f6(a7),a12,f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[10135,10102,10141,10137,9675,9328,9588,10092,8980,30,31,36,35,34])).
% 72.97/73.04 cnf(10165,plain,
% 72.97/73.04 (P4(f3(a1,a1),f6(a12),f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10135,10102,10141,10137,9675,9328,9588,9875,10092,8980,30,31,36,35,34,33])).
% 72.97/73.04 cnf(10167,plain,
% 72.97/73.04 (~P2(f6(a1),f11(a4,a4),a7)),
% 72.97/73.04 inference(scs_inference,[],[10135,10102,10141,10137,10139,9675,9234,9328,9588,9943,9875,10092,8980,30,31,36,35,34,33,37])).
% 72.97/73.04 cnf(10169,plain,
% 72.97/73.04 (P2(f3(a7,a7),f3(a2,a2),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10135,10102,10141,10137,10139,10098,9675,9234,9328,9588,9943,9875,10092,9871,9153,8980,30,31,36,35,34,33,37,38])).
% 72.97/73.04 cnf(10173,plain,
% 72.97/73.04 (P4(f6(a12),f3(a1,a1),f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10165,30])).
% 72.97/73.04 cnf(10177,plain,
% 72.97/73.04 (P2(f11(a4,a4),a1,f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10169,10165,10121,9257,9679,30,31,36])).
% 72.97/73.04 cnf(10179,plain,
% 72.97/73.04 (P2(f3(a4,a4),f3(a2,a2),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10157,10169,10165,10121,9257,9679,9320,30,31,36,35])).
% 72.97/73.04 cnf(10183,plain,
% 72.97/73.04 (P4(f6(a12),f6(a12),f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10157,10169,10165,10121,10127,10155,10023,9257,9679,9592,9320,30,31,36,35,34,33])).
% 72.97/73.04 cnf(10185,plain,
% 72.97/73.04 (~P2(f6(a12),f11(a4,a4),a7)),
% 72.97/73.04 inference(scs_inference,[],[10157,10169,10165,10121,10127,10155,10023,9257,8952,9970,9679,10025,9592,9320,30,31,36,35,34,33,37])).
% 72.97/73.04 cnf(10189,plain,
% 72.97/73.04 (P4(a12,f6(a7),f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[10163,30])).
% 72.97/73.04 cnf(10191,plain,
% 72.97/73.04 (P2(f3(a2,a2),f3(a4,a4),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10179,10163,30,31])).
% 72.97/73.04 cnf(10193,plain,
% 72.97/73.04 (P2(f3(a8,a8),f3(a5,a5),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10179,10163,9779,9932,30,31,36])).
% 72.97/73.04 cnf(10195,plain,
% 72.97/73.04 (P4(f3(a5,a5),f3(a1,a1),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[10179,10163,10173,9779,9905,9932,30,31,36,34])).
% 72.97/73.04 cnf(10197,plain,
% 72.97/73.04 (P4(f6(a8),f6(a12),f6(a8))),
% 72.97/73.04 inference(scs_inference,[],[10179,10163,10173,9779,9905,10155,10141,9932,9873,30,31,36,34,33])).
% 72.97/73.04 cnf(10199,plain,
% 72.97/73.04 (~P2(f3(a1,a1),f11(a1,a1),f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[10179,10086,10163,10173,9779,9905,9978,10155,9962,10141,9932,9873,30,31,36,34,33,37])).
% 72.97/73.04 cnf(10206,plain,
% 72.97/73.04 (P4(f3(a1,a1),f3(a5,a5),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[10195,30])).
% 72.97/73.04 cnf(10208,plain,
% 72.97/73.04 (P2(f3(a5,a5),f3(a8,a8),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10193,10195,30,31])).
% 72.97/73.04 cnf(10210,plain,
% 72.97/73.04 (P2(f6(a9),f11(a4,a4),f6(a9))),
% 72.97/73.04 inference(scs_inference,[],[10193,10195,10109,9826,30,31,36])).
% 72.97/73.04 cnf(10212,plain,
% 72.97/73.04 (P2(f11(a4,a4),f6(a5),f6(a5))),
% 72.97/73.04 inference(scs_inference,[],[10193,10195,10109,9350,9826,10092,30,31,36,35])).
% 72.97/73.04 cnf(10214,plain,
% 72.97/73.04 (P4(f6(a12),a12,f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10193,10195,10109,10173,9350,9826,9947,10092,30,31,36,35,34])).
% 72.97/73.04 cnf(10227,plain,
% 72.97/73.04 (P4(a12,f6(a12),f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10214,30])).
% 72.97/73.04 cnf(10229,plain,
% 72.97/73.04 (P2(f6(a2),f11(a4,a4),f6(a2))),
% 72.97/73.04 inference(scs_inference,[],[10161,10214,30,31])).
% 72.97/73.04 cnf(10231,plain,
% 72.97/73.04 (P2(f11(a4,a4),a7,a7)),
% 72.97/73.04 inference(scs_inference,[],[10,10161,10214,10137,9800,30,31,36])).
% 72.97/73.04 cnf(10233,plain,
% 72.97/73.04 (P2(a4,f11(a1,a1),a1)),
% 72.97/73.04 inference(scs_inference,[],[10,10161,10214,10177,10137,10109,9800,9628,30,31,36,35])).
% 72.97/73.04 cnf(10235,plain,
% 72.97/73.04 (P4(f6(a12),a1,f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10,10161,10214,10177,10137,10109,9431,9800,9628,30,31,36,35,34])).
% 72.97/73.04 cnf(10247,plain,
% 72.97/73.04 (P4(a12,f3(a7,a7),f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[10094,30])).
% 72.97/73.04 cnf(10251,plain,
% 72.97/73.04 (P2(a1,f3(a4,a4),a1)),
% 72.97/73.04 inference(scs_inference,[],[10210,10233,10094,10044,30,31,36])).
% 72.97/73.04 cnf(10253,plain,
% 72.97/73.04 (P2(f11(a4,a4),a1,a1)),
% 72.97/73.04 inference(scs_inference,[],[10210,10233,10094,10044,10092,30,31,36,35])).
% 72.97/73.04 cnf(10255,plain,
% 72.97/73.04 (P4(f6(a12),f3(a12,a12),f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10210,10233,10235,10094,10044,9242,10092,30,31,36,35,34])).
% 72.97/73.04 cnf(10257,plain,
% 72.97/73.04 (P4(f11(a1,a1),f3(a5,a5),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[10206,10210,10233,10235,10094,10044,10038,9242,10092,30,31,36,35,34,33])).
% 72.97/73.04 cnf(10267,plain,
% 72.97/73.04 (P4(f3(a5,a5),f11(a1,a1),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[10257,30])).
% 72.97/73.04 cnf(10269,plain,
% 72.97/73.04 (P2(f6(a5),f11(a4,a4),f6(a5))),
% 72.97/73.04 inference(scs_inference,[],[10257,10212,30,31])).
% 72.97/73.04 cnf(10271,plain,
% 72.97/73.04 (P4(f3(a12,a12),f3(a7,a7),f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[10257,10212,9745,9463,30,31,33])).
% 72.97/73.04 cnf(10273,plain,
% 72.97/73.04 (P2(f6(a1),f11(a4,a4),f6(a1))),
% 72.97/73.04 inference(scs_inference,[],[10257,10212,9849,9745,9463,10109,30,31,33,36])).
% 72.97/73.04 cnf(10275,plain,
% 72.97/73.04 (P2(f11(a4,a4),f6(a4),f6(a4))),
% 72.97/73.04 inference(scs_inference,[],[10257,10212,9476,9849,9745,9463,10109,10092,30,31,33,36,35])).
% 72.97/73.04 cnf(10277,plain,
% 72.97/73.04 (P4(f6(a8),f3(a12,a12),f6(a8))),
% 72.97/73.04 inference(scs_inference,[],[10257,10212,10255,10197,9476,9849,9745,9463,10109,10092,30,31,33,36,35,34])).
% 72.97/73.04 cnf(10284,plain,
% 72.97/73.04 (P4(f3(a7,a7),f3(a12,a12),f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[10271,30])).
% 72.97/73.04 cnf(10286,plain,
% 72.97/73.04 (P2(a1,f11(a4,a4),a1)),
% 72.97/73.04 inference(scs_inference,[],[10271,10253,30,31])).
% 72.97/73.04 cnf(10294,plain,
% 72.97/73.04 (P4(f3(a12,a12),a12,f3(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[11,10271,10253,10067,10131,10139,9167,9234,9290,9120,3660,15,30,31,33,36,35,34])).
% 72.97/73.04 cnf(10298,plain,
% 72.97/73.04 (~P4(a1,f6(a1),a7)),
% 72.97/73.04 inference(scs_inference,[],[11,10271,10253,10273,10167,10067,10131,10139,9167,8952,9234,9457,9290,9120,3660,15,30,31,33,36,35,34,37,38])).
% 72.97/73.04 cnf(10301,plain,
% 72.97/73.04 (P4(f3(a12,a12),f6(a8),f6(a8))),
% 72.97/73.04 inference(scs_inference,[],[10277,30])).
% 72.97/73.04 cnf(10305,plain,
% 72.97/73.04 (P4(f6(a12),f3(a12,a12),a12)),
% 72.97/73.04 inference(scs_inference,[],[10275,10277,10294,10255,9855,30,31,33])).
% 72.97/73.04 cnf(10307,plain,
% 72.97/73.04 (P2(f11(a4,a4),f11(a1,a1),a1)),
% 72.97/73.04 inference(scs_inference,[],[10275,10277,10294,10253,10255,9257,9855,10233,30,31,33,36])).
% 72.97/73.04 cnf(10309,plain,
% 72.97/73.04 (P2(a7,f10(a7),f11(a4,a4))),
% 72.97/73.04 inference(scs_inference,[],[10090,10275,10277,10294,10253,10255,9288,9257,9855,10233,9104,30,31,33,36,35])).
% 72.97/73.04 cnf(10311,plain,
% 72.97/73.04 (P4(f6(a8),a12,f6(a8))),
% 72.97/73.04 inference(scs_inference,[],[10090,10275,10277,10294,10253,10255,9288,9257,9855,10233,9104,30,31,33,36,35,34])).
% 72.97/73.04 cnf(10313,plain,
% 72.97/73.04 (~P2(f3(a12,a12),f11(a9,a5),a7)),
% 72.97/73.04 inference(scs_inference,[],[10090,10275,10277,10294,9813,10253,10255,9288,9257,9246,9855,10233,9116,9104,30,31,33,36,35,34,37])).
% 72.97/73.04 cnf(10320,plain,
% 72.97/73.04 (P4(f3(a12,a12),f6(a12),a12)),
% 72.97/73.04 inference(scs_inference,[],[10305,30])).
% 72.97/73.04 cnf(10322,plain,
% 72.97/73.04 (P2(f11(a1,a1),f11(a4,a4),a1)),
% 72.97/73.04 inference(scs_inference,[],[10307,10305,30,31])).
% 72.97/73.04 cnf(10324,plain,
% 72.97/73.04 (P4(f3(a12,a12),f6(a12),f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10307,10305,10227,9612,30,31,33])).
% 72.97/73.04 cnf(10326,plain,
% 72.97/73.04 (P2(f3(a1,a1),f11(a4,a4),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10307,10305,10227,9302,9612,10109,30,31,33,36])).
% 72.97/73.04 cnf(10334,plain,
% 72.97/73.04 (~P4(a1,a1,f6(a5))),
% 72.97/73.04 inference(scs_inference,[],[11,10050,10307,10305,10227,10004,9302,9453,9507,9276,8952,9612,10109,9755,10092,30,31,33,36,35,34,37,38])).
% 72.97/73.04 cnf(10338,plain,
% 72.97/73.04 (P2(f11(a4,a4),f3(a1,a1),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10326,10311,30,31])).
% 72.97/73.04 cnf(10340,plain,
% 72.97/73.04 (P4(f3(a12,a12),f6(a7),f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[10326,10320,10311,10189,9592,30,31,33])).
% 72.97/73.04 cnf(10342,plain,
% 72.97/73.04 (P2(a1,f11(a4,a4),f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10326,10322,10320,10311,10307,10177,10189,9592,30,31,33,36])).
% 72.97/73.04 cnf(10344,plain,
% 72.97/73.04 (P2(a1,a1,a1)),
% 72.97/73.04 inference(scs_inference,[],[10326,10322,10320,10311,9903,10307,10177,10189,9592,30,31,33,36,35])).
% 72.97/73.04 cnf(10346,plain,
% 72.97/73.04 (P4(f6(a12),f3(a12,a12),f3(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[10326,10322,10324,10320,10311,9903,10307,10177,10189,10305,10294,9592,30,31,33,36,35,34])).
% 72.97/73.04 cnf(10348,plain,
% 72.97/73.04 (~P2(f3(a7,a7),f10(a7),f6(a2))),
% 72.97/73.04 inference(scs_inference,[],[10326,9124,10322,10324,10320,10311,10247,9903,10307,10177,10189,10305,10294,9592,9610,30,31,33,36,35,34,37])).
% 72.97/73.04 cnf(10352,plain,
% 72.97/73.04 (P4(f3(a12,a12),f6(a12),f3(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[10346,30])).
% 72.97/73.04 cnf(10354,plain,
% 72.97/73.04 (P2(a1,a4,f11(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10346,10121,30,31])).
% 72.97/73.04 cnf(10356,plain,
% 72.97/73.04 (P4(f3(a12,a12),f3(a12,a12),a12)),
% 72.97/73.04 inference(scs_inference,[],[10346,10320,10121,9461,30,31,33])).
% 72.97/73.04 cnf(10358,plain,
% 72.97/73.04 (P2(a1,f11(a1,a1),a1)),
% 72.97/73.04 inference(scs_inference,[],[10344,10286,10346,10320,10121,10307,9461,30,31,33,36])).
% 72.97/73.04 cnf(10360,plain,
% 72.97/73.04 (P2(a7,a2,f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10344,10286,10346,10320,10121,9859,10307,9066,9461,3660,30,31,33,36,35])).
% 72.97/73.04 cnf(10362,plain,
% 72.97/73.04 (P4(a12,f6(a12),a12)),
% 72.97/73.04 inference(scs_inference,[],[10344,10286,10346,10183,10320,10121,9859,10307,9066,9461,3660,30,31,33,36,35,34])).
% 72.97/73.04 cnf(10364,plain,
% 72.97/73.04 (~P2(a5,f11(a4,a4),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[10344,10269,10286,10346,10183,10320,9122,10121,9859,10307,9066,9461,9100,3660,30,31,33,36,35,34,37])).
% 72.97/73.04 cnf(10372,plain,
% 72.97/73.04 (P4(f6(a7),f3(a12,a12),f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[10340,30])).
% 72.97/73.04 cnf(10376,plain,
% 72.97/73.04 (P4(f6(a12),f6(a4),f6(a4))),
% 72.97/73.04 inference(scs_inference,[],[10358,10340,9530,10346,30,31,33])).
% 72.97/73.04 cnf(10378,plain,
% 72.97/73.04 (P2(f11(a4,a4),f6(a12),f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10358,10340,9530,9064,10346,10092,30,31,33,35])).
% 72.97/73.04 cnf(10380,plain,
% 72.97/73.04 (P4(a12,f6(a12),f3(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[10352,10356,10358,10340,10324,9530,9064,10346,10092,30,31,33,35,34])).
% 72.97/73.04 cnf(10382,plain,
% 72.97/73.04 (P4(f3(a8,a8),f11(a1,a1),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[10352,10356,10358,10340,10342,9984,10324,9530,9035,9064,10346,10092,30,31,33,35,34,37])).
% 72.97/73.04 cnf(10391,plain,
% 72.97/73.04 (P4(f11(a1,a1),f3(a8,a8),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[10382,30])).
% 72.97/73.04 cnf(10393,plain,
% 72.97/73.04 (P2(f6(a12),f11(a4,a4),f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10382,10378,30,31])).
% 72.97/73.04 cnf(10397,plain,
% 72.97/73.04 (~P2(f6(a2),a7,f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[10382,10309,10348,10378,10380,10229,9851,9986,30,31,33,36])).
% 72.97/73.04 cnf(10401,plain,
% 72.97/73.04 (P4(a12,f3(a12,a12),f3(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[10382,10309,10348,10378,10380,10143,10229,9851,10356,9658,9986,10294,30,31,33,36,35,34])).
% 72.97/73.04 cnf(10409,plain,
% 72.97/73.04 (P4(f6(a4),f6(a12),f6(a4))),
% 72.97/73.04 inference(scs_inference,[],[10376,30])).
% 72.97/73.04 cnf(10411,plain,
% 72.97/73.04 (P2(a2,a7,f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10376,10360,30,31])).
% 72.97/73.04 cnf(10413,plain,
% 72.97/73.04 (P4(f11(a1,a1),a8,a8)),
% 72.97/73.04 inference(scs_inference,[],[10391,10376,10019,10360,30,31,33])).
% 72.97/73.04 cnf(10415,plain,
% 72.97/73.04 (P2(a1,f3(a1,a1),a1)),
% 72.97/73.04 inference(scs_inference,[],[10391,10376,10019,10358,10360,9960,30,31,33,36])).
% 72.97/73.04 cnf(10431,plain,
% 72.97/73.04 (P4(a8,f11(a1,a1),a8)),
% 72.97/73.04 inference(scs_inference,[],[10413,30])).
% 72.97/73.04 cnf(10433,plain,
% 72.97/73.04 (P2(a7,f3(a4,a4),f3(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[10413,9644,30,31])).
% 72.97/73.04 cnf(10435,plain,
% 72.97/73.04 (P4(a12,f11(a7,a7),f11(a7,a7))),
% 72.97/73.04 inference(scs_inference,[],[10413,10401,9766,9644,30,31,33])).
% 72.97/73.04 cnf(10437,plain,
% 72.97/73.04 (P4(f3(a1,a1),f11(a2,a2),f11(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10413,10401,9766,9644,9106,9191,30,31,33,34])).
% 72.97/73.04 cnf(10439,plain,
% 72.97/73.04 (P4(f11(a1,a1),f11(a2,a2),f11(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10413,10401,9766,9163,10354,9644,9106,9191,30,31,33,34,37])).
% 72.97/73.04 cnf(10447,plain,
% 72.97/73.04 (P4(f11(a2,a2),f3(a1,a1),f11(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10437,30])).
% 72.97/73.04 cnf(10449,plain,
% 72.97/73.04 (P2(a5,f3(a8,a8),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10437,9090,30,31])).
% 72.97/73.04 cnf(10451,plain,
% 72.97/73.04 (P4(f3(a9,a9),a12,f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10437,9913,9090,10356,30,31,33])).
% 72.97/73.04 cnf(10453,plain,
% 72.97/73.04 (P2(f11(a1,a1),f3(a4,a4),a1)),
% 72.97/73.04 inference(scs_inference,[],[10437,10251,9501,9913,9090,10356,10354,30,31,33,36])).
% 72.97/73.04 cnf(10455,plain,
% 72.97/73.04 (P4(f6(a4),a4,f6(a12))),
% 72.97/73.04 inference(scs_inference,[],[10437,10376,10251,9501,9913,9090,10115,10356,10354,10255,30,31,33,36,34])).
% 72.97/73.04 cnf(10457,plain,
% 72.97/73.04 (P4(f11(a1,a1),f11(a12,a12),f11(a12,a12))),
% 72.97/73.04 inference(scs_inference,[],[10437,9031,10376,10251,9501,9913,9090,9147,10115,10356,10354,10255,30,31,33,36,34,37])).
% 72.97/73.04 cnf(10469,plain,
% 72.97/73.04 (P4(f11(a2,a2),a1,f11(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10439,10447,10453,9244,30,31,34])).
% 72.97/73.04 cnf(10471,plain,
% 72.97/73.04 (P4(f6(a12),f11(a2,a2),f11(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10439,10447,10453,10437,9244,9911,30,31,34,33])).
% 72.97/73.04 cnf(10473,plain,
% 72.97/73.04 (P2(f3(a9,a9),f10(a7),a2)),
% 72.97/73.04 inference(scs_inference,[],[10439,10447,10453,10411,10437,9244,10309,9911,9943,30,31,34,33,36])).
% 72.97/73.04 cnf(10475,plain,
% 72.97/73.04 (P2(f3(a4,a4),a2,a2)),
% 72.97/73.04 inference(scs_inference,[],[10439,10447,10453,10411,10437,10157,9244,10309,9911,9943,30,31,34,33,36,35])).
% 72.97/73.04 cnf(10481,plain,
% 72.97/73.04 (P2(a8,f3(a4,a4),a8)),
% 72.97/73.04 inference(scs_inference,[],[10439,10447,10334,10453,10397,10411,10437,10269,10157,9244,9354,10231,10286,10309,9911,9943,9153,30,31,34,33,36,35,38,37,301])).
% 72.97/73.04 cnf(10483,plain,
% 72.97/73.04 (P2(f3(a4,a4),a8,a8)),
% 72.97/73.04 inference(scs_inference,[],[10439,10447,10334,10453,10397,10411,10437,10269,10157,9244,9354,10231,10286,10309,9911,9943,9153,30,31,34,33,36,35,38,37,301,89])).
% 72.97/73.04 cnf(10491,plain,
% 72.97/73.04 (P2(f10(a7),f3(a9,a9),a2)),
% 72.97/73.04 inference(scs_inference,[],[10457,10473,30,31])).
% 72.97/73.04 cnf(10493,plain,
% 72.97/73.04 (P4(f10(a5),f6(a12),f10(a5))),
% 72.97/73.04 inference(scs_inference,[],[10457,10473,10380,9813,9804,30,31,34])).
% 72.97/73.04 cnf(10495,plain,
% 72.97/73.04 (P4(a12,f11(a9,a9),f11(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10457,10473,10380,9813,9304,9804,9185,30,31,34,33])).
% 72.97/73.04 cnf(10497,plain,
% 72.97/73.04 (P2(f11(a8,a8),f3(a4,a4),f11(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[10457,10473,10481,10380,9813,9304,8958,9804,9185,30,31,34,33,36])).
% 72.97/73.04 cnf(10499,plain,
% 72.97/73.04 (P2(f3(a4,a4),a9,a9)),
% 72.97/73.04 inference(scs_inference,[],[10457,10473,10481,10483,10380,9813,9304,8958,9804,9143,9185,30,31,34,33,36,35])).
% 72.97/73.04 cnf(10510,plain,
% 72.97/73.04 (P4(f10(a5),f3(a1,a1),f10(a5))),
% 72.97/73.04 inference(scs_inference,[],[10497,10435,10493,10173,30,31,34])).
% 72.97/73.04 cnf(10512,plain,
% 72.97/73.04 (P4(a12,f3(a1,a1),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10497,10435,10493,10401,10173,9745,30,31,34,33])).
% 72.97/73.04 cnf(10514,plain,
% 72.97/73.04 (P2(f11(a1,a1),f3(a1,a1),a1)),
% 72.97/73.04 inference(scs_inference,[],[10497,10435,10493,10338,10415,10401,10342,10173,9745,30,31,34,33,36])).
% 72.97/73.04 cnf(10516,plain,
% 72.97/73.04 (P2(f3(a4,a4),f11(a9,a5),f11(a9,a5))),
% 72.97/73.04 inference(scs_inference,[],[10497,10435,10493,10499,10338,10415,10401,9010,10342,10173,9745,30,31,34,33,36,35])).
% 72.97/73.04 cnf(10518,plain,
% 72.97/73.04 (~P4(a5,f11(a1,a1),f3(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[10497,10435,10364,10493,10499,10338,10415,10401,9010,10342,10173,9745,9334,9926,30,31,34,33,36,35,38])).
% 72.97/73.04 cnf(10522,plain,
% 72.97/73.04 (P4(f11(a2,a2),f6(a12),f11(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10471,30])).
% 72.97/73.04 cnf(10524,plain,
% 72.97/73.04 (P2(f11(a9,a5),f3(a4,a4),f11(a9,a5))),
% 72.97/73.04 inference(scs_inference,[],[10471,10516,30,31])).
% 72.97/73.04 cnf(10526,plain,
% 72.97/73.04 (P4(f11(a2,a2),a12,f11(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10471,10516,10469,9174,30,31,34])).
% 72.97/73.04 cnf(10530,plain,
% 72.97/73.04 (P2(f3(a7,a7),a2,f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10471,10433,10516,10469,10475,10227,10360,9174,30,31,34,33,36])).
% 72.97/73.04 cnf(10532,plain,
% 72.97/73.04 (P2(f3(a4,a4),f11(a2,a2),f11(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10471,10433,10516,10469,10475,10227,10360,9174,9080,30,31,34,33,36,35])).
% 72.97/73.04 cnf(10547,plain,
% 72.97/73.04 (P4(f11(a9,a9),a12,f11(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10495,30])).
% 72.97/73.04 cnf(10551,plain,
% 72.97/73.04 (P4(f3(a1,a1),f6(a12),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10532,10495,10362,9947,30,31,34])).
% 72.97/73.04 cnf(10553,plain,
% 72.97/73.04 (P4(f6(a12),f11(a5,a5),f11(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[10532,10495,10362,9378,9947,9568,30,31,34,33])).
% 72.97/73.04 cnf(10555,plain,
% 72.97/73.04 (P2(a9,f3(a4,a4),a9)),
% 72.97/73.04 inference(scs_inference,[],[10532,10524,10495,10362,9378,9947,9246,9568,30,31,34,33,36])).
% 72.97/73.04 cnf(10557,plain,
% 72.97/73.04 (P2(f11(a1,a1),f11(a1,a1),a1)),
% 72.97/73.04 inference(scs_inference,[],[10532,10524,10495,10514,10362,9915,9378,9947,10344,9246,9568,30,31,34,33,36,35])).
% 72.97/73.04 cnf(10564,plain,
% 72.97/73.04 (P4(f11(a5,a5),f6(a12),f11(a5,a5))),
% 72.97/73.04 inference(scs_inference,[],[10553,30])).
% 72.97/73.04 cnf(10568,plain,
% 72.97/73.04 (P4(f10(a5),f11(a1,a1),f10(a5))),
% 72.97/73.04 inference(scs_inference,[],[10553,10530,10510,10029,30,31,34])).
% 72.97/73.04 cnf(10570,plain,
% 72.97/73.04 (P4(a12,f6(a12),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10553,10530,10510,10512,10362,10029,10173,30,31,34,33])).
% 72.97/73.04 cnf(10574,plain,
% 72.97/73.04 (P2(f3(a1,a1),f11(a1,a1),a1)),
% 72.97/73.04 inference(scs_inference,[],[10111,10553,10530,10557,10510,10512,10010,9903,10362,9915,10029,10173,10137,30,31,34,33,36,35])).
% 72.97/73.04 cnf(10590,plain,
% 72.97/73.04 (P4(f11(a9,a9),a1,f11(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10568,10547,10475,9431,30,31,34])).
% 72.97/73.04 cnf(10592,plain,
% 72.97/73.04 (P4(f3(a9,a9),f3(a1,a1),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10568,10570,10547,10451,9548,10475,9431,30,31,34,33])).
% 72.97/73.04 cnf(10594,plain,
% 72.97/73.04 (P2(f3(a2,a2),f10(a5),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[10568,10570,10547,10451,9548,10475,9090,9431,9984,9811,30,31,34,33,36])).
% 72.97/73.04 cnf(10600,plain,
% 72.97/73.04 (P4(f3(a1,a1),f3(a9,a9),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10592,30])).
% 72.97/73.04 cnf(10602,plain,
% 72.97/73.04 (P2(f10(a5),f3(a2,a2),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[10592,10594,30,31])).
% 72.97/73.04 cnf(10604,plain,
% 72.97/73.04 (P4(f3(a2,a2),f3(a1,a1),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10592,10594,9879,30,31,34])).
% 72.97/73.04 cnf(10606,plain,
% 72.97/73.04 (P4(a12,f6(a4),f6(a4))),
% 72.97/73.04 inference(scs_inference,[],[10592,10594,9879,10401,9530,30,31,34,33])).
% 72.97/73.04 cnf(10608,plain,
% 72.97/73.04 (P2(f11(a9,a9),f3(a4,a4),f11(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10592,10594,10555,9879,10401,9530,9047,30,31,34,33,36])).
% 72.97/73.04 cnf(10612,plain,
% 72.97/73.04 (P4(f11(a9,a9),f11(a1,a1),f11(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10592,10594,10555,10590,9086,10185,9879,10324,10401,9572,9530,10393,10354,9047,30,31,34,33,36,38,37])).
% 72.97/73.04 cnf(10615,plain,
% 72.97/73.04 (P4(f3(a1,a1),f3(a2,a2),f3(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10604,30])).
% 72.97/73.04 cnf(10621,plain,
% 72.97/73.04 (P4(f3(a12,a12),f3(a12,a12),f3(a1,a1))),
% 72.97/73.04 inference(scs_inference,[],[10604,10608,10606,10455,10570,10352,10356,30,31,34,33])).
% 72.97/73.04 cnf(10623,plain,
% 72.97/73.04 (P2(f3(a8,a8),f3(a4,a4),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[10604,10608,10602,10606,10191,10455,10570,10352,10356,30,31,34,33,36])).
% 72.97/73.04 cnf(10636,plain,
% 72.97/73.04 (P2(f3(a4,a4),f3(a8,a8),f3(a8,a8))),
% 72.97/73.04 inference(scs_inference,[],[10612,10623,30,31])).
% 72.97/73.04 cnf(10638,plain,
% 72.97/73.04 (P4(f11(a9,a9),f6(a12),f11(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10612,10623,10547,10362,30,31,34])).
% 72.97/73.04 cnf(10640,plain,
% 72.97/73.04 (P4(f6(a7),f3(a1,a1),f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[10612,10621,10623,10372,10547,10362,30,31,34,33])).
% 72.97/73.04 cnf(10642,plain,
% 72.97/73.04 (P2(f3(a2,a2),f11(a4,a4),a2)),
% 72.97/73.04 inference(scs_inference,[],[10612,10621,10623,10372,9884,10473,10547,10309,10362,30,31,34,33,35])).
% 72.97/73.04 cnf(10646,plain,
% 72.97/73.04 (~P2(a1,a4,a4)),
% 72.97/73.04 inference(scs_inference,[],[10612,10621,10623,10199,10372,9884,9622,10473,10574,10551,10547,10309,10362,9596,9401,9334,30,31,34,33,35,38,37])).
% 72.97/73.04 cnf(10651,plain,
% 72.97/73.04 (P4(f6(a12),f11(a9,a9),f11(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10638,30])).
% 72.97/73.04 cnf(10653,plain,
% 72.97/73.04 (P2(f11(a4,a4),f3(a2,a2),a2)),
% 72.97/73.04 inference(scs_inference,[],[10638,10642,30,31])).
% 72.97/73.04 cnf(10655,plain,
% 72.97/73.04 (P4(f11(a2,a2),f3(a12,a12),f11(a2,a2))),
% 72.97/73.04 inference(scs_inference,[],[10638,10642,10522,10526,10305,30,31,34])).
% 72.97/73.04 cnf(10659,plain,
% 72.97/73.04 (P2(f3(a5,a5),f3(a8,a8),a2)),
% 72.97/73.04 inference(scs_inference,[],[10638,10642,10522,10526,10208,10413,10155,10305,9984,30,31,34,33,35])).
% 72.97/73.04 cnf(10663,plain,
% 72.97/73.04 (P4(f3(a9,a9),a2,a2)),
% 72.97/73.04 inference(scs_inference,[],[10646,10638,10642,10522,10526,10208,9787,9886,10413,9826,10155,10305,9984,9027,3670,30,31,34,33,35,38,37])).
% 72.97/73.04 cnf(10671,plain,
% 72.97/73.04 (P4(f6(a7),f11(a1,a1),f6(a7))),
% 72.97/73.04 inference(scs_inference,[],[10655,10659,10640,10029,31,30,34])).
% 72.97/73.04 cnf(10675,plain,
% 72.97/73.04 (P2(a8,f3(a5,a5),a2)),
% 72.97/73.04 inference(scs_inference,[],[10655,10653,10659,10663,9972,10640,10600,9779,10029,31,30,34,33,36])).
% 72.97/73.04 cnf(10681,plain,
% 72.97/73.04 (P2(f3(a5,a5),a8,a2)),
% 72.97/73.04 inference(scs_inference,[],[10675,31])).
% 72.97/73.04 cnf(10685,plain,
% 72.97/73.04 (P4(a2,f6(a12),a2)),
% 72.97/73.04 inference(scs_inference,[],[10671,10675,9768,10117,31,30,34])).
% 72.97/73.04 cnf(10689,plain,
% 72.97/73.04 (P2(a8,a12,f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10671,10675,9922,9768,10663,10411,10117,10137,11,31,30,34,33,36])).
% 72.97/73.04 cnf(10691,plain,
% 72.97/73.04 (P2(f3(a1,a1),f3(a8,a8),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10671,10675,9922,9768,10663,10621,10411,10117,10098,10061,10137,11,31,30,34,33,36,38])).
% 72.97/73.04 cnf(10705,plain,
% 72.97/73.04 (P2(f3(a8,a8),f3(a1,a1),f3(a9,a9))),
% 72.97/73.04 inference(scs_inference,[],[10691,31])).
% 72.97/73.04 cnf(10709,plain,
% 72.97/73.04 (P4(f3(a1,a1),a9,a9)),
% 72.97/73.04 inference(scs_inference,[],[10691,10685,9662,10621,31,30,34])).
% 72.97/73.04 cnf(10722,plain,
% 72.97/73.05 (P4(f11(a5,a5),f3(a12,a12),f11(a5,a5))),
% 72.97/73.05 inference(scs_inference,[],[10709,10564,9732,10255,31,30,34])).
% 72.97/73.05 cnf(10732,plain,
% 72.97/73.05 (P4(f3(a12,a12),f11(a5,a5),f11(a5,a5))),
% 72.97/73.05 inference(scs_inference,[],[10722,9064,31,30])).
% 72.97/73.05 cnf(10734,plain,
% 72.97/73.05 (P4(a2,f3(a1,a1),a2)),
% 72.97/73.05 inference(scs_inference,[],[10722,10604,10117,9064,31,30,34])).
% 72.97/73.05 cnf(10736,plain,
% 72.97/73.05 (P4(f3(a1,a1),f11(a9,a9),f11(a9,a9))),
% 72.97/73.05 inference(scs_inference,[],[10722,10651,10604,10165,10117,9064,31,30,34,33])).
% 72.97/73.05 cnf(10738,plain,
% 72.97/73.05 (P2(f3(a5,a5),f3(a9,a9),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10722,10689,10651,10681,10604,10165,10117,9064,4743,31,30,34,33,35])).
% 72.97/73.05 cnf(10745,plain,
% 72.97/73.05 (P2(f3(a9,a9),f3(a5,a5),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10738,31])).
% 72.97/73.05 cnf(10749,plain,
% 72.97/73.05 (P4(f3(a1,a1),f11(a5,a5),f11(a5,a5))),
% 72.97/73.05 inference(scs_inference,[],[10732,10736,10738,10621,31,30,34])).
% 72.97/73.05 cnf(10751,plain,
% 72.97/73.05 (P4(f3(a12,a12),a1,a1)),
% 72.97/73.05 inference(scs_inference,[],[10732,10736,10738,10301,10621,8934,31,30,34,33])).
% 72.97/73.05 cnf(10753,plain,
% 72.97/73.05 (P2(a2,f3(a1,a1),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10705,10732,10736,10738,10301,10659,10621,8934,31,30,34,33,36])).
% 72.97/73.05 cnf(10755,plain,
% 72.97/73.05 (P2(f10(a5),f11(a9,a5),f3(a9,a9))),
% 72.97/73.05 inference(scs_inference,[],[10705,10732,10736,10738,10301,10689,10659,10621,8934,4743,3665,31,30,34,33,36,35])).
% 72.97/73.05 cnf(10769,plain,
% 72.97/73.05 (P4(a1,f6(a12),f3(a12,a12))),
% 72.97/73.05 inference(scs_inference,[],[10749,10755,10751,9070,10352,9139,31,30,8911,34])).
% 72.97/73.05 cnf(10771,plain,
% 72.97/73.05 (P4(f3(a12,a12),f11(a9,a9),f11(a9,a9))),
% 72.97/73.05 inference(scs_inference,[],[10749,10755,10751,10495,10651,9070,10352,10320,9139,31,30,8911,34,33])).
% 72.97/73.05 cnf(10773,plain,
% 72.97/73.05 (P2(a8,f3(a1,a1),f3(a9,a9))),
% 72.97/73.05 inference(scs_inference,[],[10749,10755,10753,10751,10495,10651,9070,10352,10320,9139,3665,31,30,8911,34,33,36])).
% 72.97/73.05 cnf(10779,plain,
% 72.97/73.05 (P2(f3(a1,a1),a8,f3(a9,a9))),
% 72.97/73.05 inference(scs_inference,[],[10773,31])).
% 72.97/73.05 cnf(10783,plain,
% 72.97/73.05 (P4(f6(a12),f11(a1,a1),f6(a12))),
% 72.97/73.05 inference(scs_inference,[],[10771,10773,10431,10141,31,30,34])).
% 72.97/73.05 cnf(10785,plain,
% 72.97/73.05 (P4(f11(a1,a1),f3(a2,a2),f3(a2,a2))),
% 72.97/73.05 inference(scs_inference,[],[10771,10773,10615,10431,10141,10038,31,30,34,33])).
% 72.97/73.05 cnf(10796,plain,
% 72.97/73.05 (P2(f3(a1,a1),a2,f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10753,31])).
% 72.97/73.05 cnf(10798,plain,
% 72.97/73.05 (P4(f3(a2,a2),f11(a1,a1),f3(a2,a2))),
% 72.97/73.05 inference(scs_inference,[],[10785,10753,31,30])).
% 72.97/73.05 cnf(10800,plain,
% 72.97/73.05 (P4(f3(a12,a12),f11(a1,a1),f3(a12,a12))),
% 72.97/73.05 inference(scs_inference,[],[10785,10783,10769,10753,31,30,34])).
% 72.97/73.05 cnf(10802,plain,
% 72.97/73.05 (P4(f3(a12,a12),f3(a4,a4),f3(a4,a4))),
% 72.97/73.05 inference(scs_inference,[],[10785,10783,10769,10753,9280,10751,31,30,34,33])).
% 72.97/73.05 cnf(10804,plain,
% 72.97/73.05 (P2(f3(a2,a2),f3(a1,a1),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10785,10783,10769,10705,10753,10208,9280,10738,10751,31,30,34,33,36])).
% 72.97/73.05 cnf(10816,plain,
% 72.97/73.05 (P4(f11(a1,a1),f3(a12,a12),f3(a12,a12))),
% 72.97/73.05 inference(scs_inference,[],[10800,10804,31,30])).
% 72.97/73.05 cnf(10818,plain,
% 72.97/73.05 (P4(f6(a4),f11(a1,a1),f6(a4))),
% 72.97/73.05 inference(scs_inference,[],[10800,10804,10409,10783,31,30,34])).
% 72.97/73.05 cnf(10820,plain,
% 72.97/73.05 (P4(f3(a12,a12),f6(a9),f6(a9))),
% 72.97/73.05 inference(scs_inference,[],[10800,10804,10409,10783,9274,10751,31,30,34,33])).
% 72.97/73.05 cnf(10824,plain,
% 72.97/73.05 (P2(a5,f3(a9,a9),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10800,10779,10804,10796,10409,10783,10449,9274,10705,10751,9051,31,30,34,33,36,35])).
% 72.97/73.05 cnf(10828,plain,
% 72.97/73.05 (P4(f11(a9,a5),a1,f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10798,10800,10779,10804,10796,10409,10646,10783,10449,9274,10705,10751,10514,9051,10354,8956,31,30,34,33,36,35,38,37])).
% 72.97/73.05 cnf(10845,plain,
% 72.97/73.05 (P2(a8,f3(a4,a4),f3(a8,a8))),
% 72.97/73.05 inference(scs_inference,[],[9932,31])).
% 72.97/73.05 cnf(10847,plain,
% 72.97/73.05 (P4(f3(a4,a4),f3(a12,a12),f3(a4,a4))),
% 72.97/73.05 inference(scs_inference,[],[10802,9932,31,30])).
% 72.97/73.05 cnf(10849,plain,
% 72.97/73.05 (P4(f11(a9,a5),a12,f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10802,10828,9932,9268,31,30,34])).
% 72.97/73.05 cnf(10851,plain,
% 72.97/73.05 (P4(f11(a1,a1),f3(a4,a4),f3(a4,a4))),
% 72.97/73.05 inference(scs_inference,[],[10802,10816,10828,9932,9268,31,30,34,33])).
% 72.97/73.05 cnf(10859,plain,
% 72.97/73.05 (P2(a8,f3(a12,a12),f3(a9,a9))),
% 72.97/73.05 inference(scs_inference,[],[10851,9578,30,31])).
% 72.97/73.05 cnf(10861,plain,
% 72.97/73.05 (P4(f3(a7,a7),f11(a1,a1),f3(a7,a7))),
% 72.97/73.05 inference(scs_inference,[],[10851,10284,10800,9578,30,31,34])).
% 72.97/73.05 cnf(10863,plain,
% 72.97/73.05 (P4(f11(a1,a1),f6(a9),f6(a9))),
% 72.97/73.05 inference(scs_inference,[],[10851,10820,10284,10800,10816,9578,30,31,34,33])).
% 72.97/73.05 cnf(10865,plain,
% 72.97/73.05 (P4(f3(a8,a8),f3(a9,a9),f3(a8,a8))),
% 72.97/73.05 inference(scs_inference,[],[10847,10851,10820,10636,10284,10800,10816,10061,9578,30,31,34,33,37])).
% 72.97/73.05 cnf(10887,plain,
% 72.97/73.05 (P2(a12,f3(a2,a2),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10861,9478,10745,10193,9290,30,31,35])).
% 72.97/73.05 cnf(10889,plain,
% 72.97/73.05 (P4(f3(a8,a8),f3(a1,a1),f3(a8,a8))),
% 72.97/73.05 inference(scs_inference,[],[10861,10865,9478,10745,10193,10592,9290,30,31,35,34])).
% 72.97/73.05 cnf(10899,plain,
% 72.97/73.05 (P2(f3(a2,a2),a12,f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10889,10887,30,31])).
% 72.97/73.05 cnf(10901,plain,
% 72.97/73.05 (P2(a8,f3(a8,a8),f11(a8,a8))),
% 72.97/73.05 inference(scs_inference,[],[10889,10845,10887,10497,8958,30,31,35])).
% 72.97/73.05 cnf(10903,plain,
% 72.97/73.05 (P4(f11(a5,a5),f11(a1,a1),f11(a5,a5))),
% 72.97/73.05 inference(scs_inference,[],[10889,10845,10887,10497,10722,10800,8958,30,31,35,34])).
% 72.97/73.05 cnf(10905,plain,
% 72.97/73.05 (P4(f11(a1,a1),a1,a1)),
% 72.97/73.05 inference(scs_inference,[],[10889,10845,10863,10887,10497,10722,10800,8958,9027,30,31,35,34,33])).
% 72.97/73.05 cnf(10907,plain,
% 72.97/73.05 (P2(f3(a2,a2),f3(a4,a4),a2)),
% 72.97/73.05 inference(scs_inference,[],[10889,10845,10863,10887,10497,10722,10800,10659,9616,8958,9027,30,31,35,34,33,36])).
% 72.97/73.05 cnf(10918,plain,
% 72.97/73.05 (P2(f3(a8,a8),a8,f11(a8,a8))),
% 72.97/73.05 inference(scs_inference,[],[10903,10901,30,31])).
% 72.97/73.05 cnf(10920,plain,
% 72.97/73.05 (P4(f3(a4,a4),f6(a12),f3(a4,a4))),
% 72.97/73.05 inference(scs_inference,[],[10903,10901,10847,10769,9439,30,31,34])).
% 72.97/73.05 cnf(10924,plain,
% 72.97/73.05 (P2(a2,f3(a12,a12),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10903,10824,10859,10901,10905,10847,10769,9382,9066,9439,30,31,34,33,36])).
% 72.97/73.05 cnf(10937,plain,
% 72.97/73.05 (P4(f11(a1,a1),f3(a9,a9),f3(a9,a9))),
% 72.97/73.05 inference(scs_inference,[],[10818,10907,10298,10905,9082,9457,30,31,34,33])).
% 72.97/73.05 cnf(10939,plain,
% 72.97/73.05 (P4(f11(a8,a8),f3(a9,a9),f11(a8,a8))),
% 72.97/73.05 inference(scs_inference,[],[10818,10907,10918,10298,10889,10779,10905,9082,9457,30,31,34,33,37])).
% 72.97/73.05 cnf(10948,plain,
% 72.97/73.05 (P2(f3(a12,a12),a2,f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10937,10924,30,31])).
% 72.97/73.05 cnf(10950,plain,
% 72.97/73.05 (P2(f11(a4,a4),f6(a8),f6(a8))),
% 72.97/73.05 inference(scs_inference,[],[10937,10924,8982,10092,30,31,35])).
% 72.97/73.05 cnf(10952,plain,
% 72.97/73.05 (P4(a2,f11(a1,a1),a2)),
% 72.97/73.05 inference(scs_inference,[],[10937,10924,10685,10783,8982,10092,30,31,35,34])).
% 72.97/73.05 cnf(10970,plain,
% 72.97/73.05 (P4(f11(a1,a1),f6(a2),f6(a2))),
% 72.97/73.05 inference(scs_inference,[],[9772,10950,10313,10948,10939,10924,9332,10905,9356,30,31,35,34,33])).
% 72.97/73.05 cnf(10979,plain,
% 72.97/73.05 (P4(f6(a2),f11(a1,a1),f6(a2))),
% 72.97/73.05 inference(scs_inference,[],[10970,30])).
% 72.97/73.05 cnf(10981,plain,
% 72.97/73.05 (P2(f11(a1,a1),a4,a1)),
% 72.97/73.05 inference(scs_inference,[],[10970,10233,30,31])).
% 72.97/73.05 cnf(10983,plain,
% 72.97/73.05 (P4(f11(a9,a5),f6(a12),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10970,10849,10362,10233,30,31,34])).
% 72.97/73.05 cnf(10994,plain,
% 72.97/73.05 (P4(f6(a12),f11(a9,a5),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10983,30])).
% 72.97/73.05 cnf(10996,plain,
% 72.97/73.05 (P2(f10(a7),a12,a5)),
% 72.97/73.05 inference(scs_inference,[],[10983,9610,30,31])).
% 72.97/73.05 cnf(10998,plain,
% 72.97/73.05 (P4(f11(a9,a5),f3(a12,a12),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10983,10828,9610,9242,30,31,34])).
% 72.97/73.05 cnf(11000,plain,
% 72.97/73.05 (P4(f6(a2),a2,f11(a1,a1))),
% 72.97/73.05 inference(scs_inference,[],[10983,10952,10828,9610,9062,9242,9505,30,31,34,33])).
% 72.97/73.05 cnf(11002,plain,
% 72.97/73.05 (P4(f6(a2),a1,f6(a2))),
% 72.97/73.05 inference(scs_inference,[],[10979,10983,10981,10952,10828,9724,9610,9062,9242,9505,30,31,34,33,37])).
% 72.97/73.05 cnf(11004,plain,
% 72.97/73.05 (P2(f3(a2,a2),f3(a12,a12),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10979,10983,10981,10952,10828,9724,9840,10924,9610,9076,9062,9242,9505,30,31,34,33,37,38])).
% 72.97/73.05 cnf(11013,plain,
% 72.97/73.05 (P2(f3(a12,a12),f3(a2,a2),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[11004,10998,30,31])).
% 72.97/73.05 cnf(11017,plain,
% 72.97/73.05 (P4(f11(a1,a1),f6(a8),f6(a8))),
% 72.97/73.05 inference(scs_inference,[],[10123,11004,10998,8988,10905,9334,30,31,34,33])).
% 72.97/73.05 cnf(11019,plain,
% 72.97/73.05 (P2(a5,f3(a8,a8),a2)),
% 72.97/73.05 inference(scs_inference,[],[10123,11004,10998,10996,10491,9478,8988,10905,9334,30,31,34,33,36])).
% 72.97/73.05 cnf(11027,plain,
% 72.97/73.05 (P4(a1,f11(a9,a5),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[10123,11004,10998,10518,10994,11000,10996,10491,10050,10229,10267,9478,9990,9656,8988,9691,9943,10905,9334,30,31,34,33,36,32,37,38,27])).
% 72.97/73.05 cnf(11031,plain,
% 72.97/73.05 (P4(f6(a8),f11(a1,a1),f6(a8))),
% 72.97/73.05 inference(scs_inference,[],[11017,30])).
% 72.97/73.05 cnf(11033,plain,
% 72.97/73.05 (P2(f3(a8,a8),a5,a2)),
% 72.97/73.05 inference(scs_inference,[],[11017,11019,30,31])).
% 72.97/73.05 cnf(11035,plain,
% 72.97/73.05 (P4(f3(a4,a4),a12,f3(a4,a4))),
% 72.97/73.05 inference(scs_inference,[],[11017,11019,10920,10214,30,31,34])).
% 72.97/73.05 cnf(11037,plain,
% 72.97/73.05 (P4(f3(a12,a12),f11(a12,a12),f11(a12,a12))),
% 72.97/73.05 inference(scs_inference,[],[11017,11019,10920,9147,10214,10751,30,31,34,33])).
% 72.97/73.05 cnf(11050,plain,
% 72.97/73.05 (P4(f6(a2),f6(a12),f6(a2))),
% 72.97/73.05 inference(scs_inference,[],[11037,11013,11002,10899,10313,8982,9552,30,31,35,34])).
% 72.97/73.05 cnf(11052,plain,
% 72.97/73.05 (P4(f6(a12),f11(a12,a12),f11(a12,a12))),
% 72.97/73.05 inference(scs_inference,[],[11037,11013,11002,10899,10313,10346,8982,9552,30,31,35,34,33])).
% 72.97/73.05 cnf(11059,plain,
% 72.97/73.05 (P4(f11(a12,a12),f6(a12),f11(a12,a12))),
% 72.97/73.05 inference(scs_inference,[],[11052,30])).
% 72.97/73.05 cnf(11061,plain,
% 72.97/73.05 (P2(f11(a9,a5),f10(a5),a9)),
% 72.97/73.05 inference(scs_inference,[],[11052,9246,30,31])).
% 72.97/73.05 cnf(11065,plain,
% 72.97/73.05 (P4(a12,f11(a1,a1),a12)),
% 72.97/73.05 inference(scs_inference,[],[11052,11031,10059,10364,9710,9246,9811,30,31,35,34])).
% 72.97/73.05 cnf(11080,plain,
% 72.97/73.05 (P4(a1,a12,a1)),
% 72.97/73.05 inference(scs_inference,[],[11061,4755])).
% 72.97/73.05 cnf(11085,plain,
% 72.97/73.05 (P4(f11(a12,a12),a1,f11(a12,a12))),
% 72.97/73.05 inference(scs_inference,[],[11059,11035,10235,9590,30,31,34])).
% 72.97/73.05 cnf(11087,plain,
% 72.97/73.05 (P4(f6(a2),a2,f3(a12,a12))),
% 72.97/73.05 inference(scs_inference,[],[11059,11035,11000,10816,10235,9532,9590,30,31,34,33])).
% 72.97/73.05 cnf(11108,plain,
% 72.97/73.05 (P2(f10(a5),a4,f10(a5))),
% 72.97/73.05 inference(scs_inference,[],[11050,9029,30,31])).
% 72.97/73.05 cnf(11127,plain,
% 72.97/73.05 (P2(a5,f10(a5),a4)),
% 72.97/73.05 inference(scs_inference,[],[11087,8950,30,31])).
% 72.97/73.05 cnf(11131,plain,
% 72.97/73.05 (P4(f11(a1,a1),f11(a9,a5),f11(a9,a5))),
% 72.97/73.05 inference(scs_inference,[],[11087,11027,10004,11065,10905,8950,30,31,34,33])).
% 72.97/73.05 cnf(11133,plain,
% 72.97/73.05 (P2(f10(a5),f11(a4,a4),f10(a5))),
% 72.97/73.05 inference(scs_inference,[],[11108,11087,11027,10004,11065,10109,10905,8950,30,31,34,33,36])).
% 72.97/73.05 cnf(11145,plain,
% 72.97/73.05 (P4(f11(a12,a12),a12,f11(a12,a12))),
% 72.97/73.05 inference(scs_inference,[],[11131,11133,11085,11080,30,31,34])).
% 72.97/73.05 cnf(11147,plain,
% 72.97/73.05 (P2(a2,f10(a5),f3(a8,a8))),
% 72.97/73.05 inference(scs_inference,[],[11131,11133,11127,11085,11080,8970,11033,30,31,34,36])).
% 72.97/73.05 cnf(11164,plain,
% 72.97/73.05 (P4(f3(a12,a12),f3(a1,a1),f3(a12,a12))),
% 72.97/73.05 inference(scs_inference,[],[11145,11147,10734,11087,30,31,34])).
% 72.97/73.05 cnf(11180,plain,
% 72.97/73.05 ($false),
% 72.97/73.05 inference(scs_inference,[],[11164,9467,10137,30,31]),
% 72.97/73.05 ['proof']).
% 72.97/73.05 % SZS output end Proof
% 72.97/73.05 % Total time :72.390000s
%------------------------------------------------------------------------------