%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD052-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 : n008.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:28 EDT 2024
% Result : Unsatisfiable 128.97s 129.01s
% Output : CNFRefutation 129.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : FLD052-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.35 % Computer : n008.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Wed Jun 19 11:47:54 EDT 2024
% 0.12/0.35 % CPUTime :
% 0.56/0.59 start to proof:theBenchmark
% 128.97/128.99 %-------------------------------------------
% 128.97/128.99 % File :CSE---1.7
% 128.97/129.00 % Problem :theBenchmark
% 128.97/129.00 % Transform :cnf
% 128.97/129.00 % Format :tptp:raw
% 128.97/129.00 % Command :java -jar mcs_scs.jar %d %s
% 128.97/129.00
% 128.97/129.00 % Result :Theorem 128.360000s
% 128.97/129.00 % Output :CNFRefutation 128.360000s
% 128.97/129.00 %-------------------------------------------
% 128.97/129.00 %--------------------------------------------------------------------------
% 128.97/129.01 % File : FLD052-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% 128.97/129.01 % Domain : Field Theory (Ordered fields)
% 128.97/129.01 % Problem : Fraction calculation, part 6
% 128.97/129.01 % Version : [Dra93] axioms : Especial.
% 128.97/129.01 % Theorem formulation : Relational with re axiom set.
% 128.97/129.01 % English :
% 128.97/129.01
% 128.97/129.01 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 128.97/129.01 % Source : [Dra93]
% 128.97/129.01 % Names :
% 128.97/129.01
% 128.97/129.01 % Status : Unsatisfiable
% 128.97/129.01 % Rating : 0.58 v8.2.0, 0.57 v8.1.0, 0.29 v7.5.0, 0.50 v7.4.0, 0.33 v7.3.0, 0.50 v7.2.0, 0.67 v7.0.0, 0.62 v6.3.0, 0.57 v6.2.0, 0.44 v6.1.0, 0.29 v6.0.0, 0.43 v5.5.0, 0.50 v5.4.0, 0.60 v5.2.0, 0.70 v5.1.0, 0.73 v5.0.0, 0.93 v4.1.0, 0.75 v4.0.1, 0.80 v4.0.0, 0.43 v3.4.0, 0.50 v3.3.0, 0.33 v3.2.0, 0.67 v3.1.0, 0.50 v2.7.0, 0.88 v2.6.0, 0.67 v2.5.0, 1.00 v2.1.0
% 128.97/129.01 % Syntax : Number of clauses : 48 ( 25 unt; 3 nHn; 48 RR)
% 128.97/129.01 % Number of literals : 99 ( 0 equ; 52 neg)
% 128.97/129.01 % Maximal clause size : 5 ( 2 avg)
% 128.97/129.01 % Maximal term depth : 2 ( 1 avg)
% 128.97/129.01 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 128.97/129.01 % Number of functors : 18 ( 18 usr; 14 con; 0-2 aty)
% 128.97/129.01 % Number of variables : 73 ( 0 sgn)
% 128.97/129.01 % SPC : CNF_UNS_RFO_NEQ_NHN
% 128.97/129.01
% 128.97/129.01 % Comments :
% 128.97/129.01 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 128.97/129.01 %--------------------------------------------------------------------------
% 128.97/129.01 include('Axioms/FLD002-0.ax').
% 128.97/129.01 %--------------------------------------------------------------------------
% 128.97/129.01 cnf(a_is_defined,hypothesis,
% 128.97/129.01 defined(a) ).
% 128.97/129.01
% 128.97/129.01 cnf(b_is_defined,hypothesis,
% 128.97/129.01 defined(b) ).
% 128.97/129.01
% 128.97/129.01 cnf(c_is_defined,hypothesis,
% 128.97/129.01 defined(c) ).
% 128.97/129.01
% 128.97/129.01 cnf(d_is_defined,hypothesis,
% 128.97/129.01 defined(d) ).
% 128.97/129.01
% 128.97/129.01 cnf(u_is_defined,hypothesis,
% 128.97/129.01 defined(u) ).
% 128.97/129.01
% 128.97/129.01 cnf(v_is_defined,hypothesis,
% 128.97/129.01 defined(v) ).
% 128.97/129.01
% 128.97/129.01 cnf(k_is_defined,hypothesis,
% 128.97/129.01 defined(k) ).
% 128.97/129.01
% 128.97/129.01 cnf(l_is_defined,hypothesis,
% 128.97/129.01 defined(l) ).
% 128.97/129.01
% 128.97/129.01 cnf(p_is_defined,hypothesis,
% 128.97/129.01 defined(p) ).
% 128.97/129.01
% 128.97/129.01 cnf(q_is_defined,hypothesis,
% 128.97/129.01 defined(q) ).
% 128.97/129.01
% 128.97/129.01 cnf(s_is_defined,hypothesis,
% 128.97/129.01 defined(s) ).
% 128.97/129.01
% 128.97/129.01 cnf(t_is_defined,hypothesis,
% 128.97/129.01 defined(t) ).
% 128.97/129.01
% 128.97/129.01 cnf(not_sum_13,negated_conjecture,
% 128.97/129.01 ~ sum(additive_identity,b,additive_identity) ).
% 128.97/129.01
% 128.97/129.01 cnf(not_sum_14,negated_conjecture,
% 128.97/129.01 ~ sum(additive_identity,d,additive_identity) ).
% 128.97/129.01
% 128.97/129.01 cnf(product_15,negated_conjecture,
% 128.97/129.01 product(a,multiplicative_inverse(b),s) ).
% 128.97/129.01
% 128.97/129.01 cnf(product_16,negated_conjecture,
% 128.97/129.01 product(c,multiplicative_inverse(d),t) ).
% 128.97/129.01
% 128.97/129.01 cnf(sum_17,negated_conjecture,
% 128.97/129.01 sum(s,t,u) ).
% 128.97/129.01
% 128.97/129.01 cnf(product_18,negated_conjecture,
% 128.97/129.01 product(a,d,p) ).
% 128.97/129.01
% 128.97/129.01 cnf(product_19,negated_conjecture,
% 128.97/129.01 product(b,c,q) ).
% 128.97/129.01
% 128.97/129.01 cnf(sum_20,negated_conjecture,
% 128.97/129.01 sum(p,q,k) ).
% 128.97/129.01
% 128.97/129.01 cnf(product_21,negated_conjecture,
% 128.97/129.01 product(b,d,l) ).
% 128.97/129.01
% 128.97/129.01 cnf(not_product_22,negated_conjecture,
% 128.97/129.01 ~ product(k,multiplicative_inverse(l),u) ).
% 128.97/129.01
% 128.97/129.01 %--------------------------------------------------------------------------
% 128.97/129.01 %-------------------------------------------
% 128.97/129.01 % Proof found
% 128.97/129.01 % SZS status Theorem for theBenchmark
% 128.97/129.01 % SZS output start Proof
% 128.97/129.01 %ClaNum:48(EqnAxiom:0)
% 128.97/129.01 %VarNum:162(SingletonVarNum:73)
% 128.97/129.01 %MaxLitNum:5
% 128.97/129.01 %MaxfuncDepth:1
% 128.97/129.01 %SharedTerms:42
% 128.97/129.01 %goalClause: 15 16 17 18 19 20 21 23 24 25
% 128.97/129.01 %singleGoalClaCount:10
% 128.97/129.01 [1]P1(a1)
% 128.97/129.01 [2]P1(a4)
% 128.97/129.01 [3]P1(a2)
% 128.97/129.01 [4]P1(a5)
% 128.97/129.01 [5]P1(a7)
% 128.97/129.01 [6]P1(a8)
% 128.97/129.01 [7]P1(a11)
% 128.97/129.01 [8]P1(a18)
% 128.97/129.01 [9]P1(a9)
% 128.97/129.01 [10]P1(a10)
% 128.97/129.01 [11]P1(a12)
% 128.97/129.01 [12]P1(a15)
% 128.97/129.01 [13]P1(a16)
% 128.97/129.01 [14]P1(a17)
% 128.97/129.01 [15]P2(a12,a15,a9)
% 128.97/129.01 [16]P2(a16,a17,a11)
% 128.97/129.01 [17]P3(a2,a8,a12)
% 128.97/129.01 [18]P3(a5,a7,a15)
% 128.97/129.01 [19]P3(a5,a8,a10)
% 128.97/129.01 [22]~P2(a1,a1,a4)
% 128.97/129.01 [23]~P2(a1,a5,a1)
% 128.97/129.01 [24]~P2(a1,a8,a1)
% 128.97/129.01 [20]P3(a2,f13(a5),a16)
% 128.97/129.01 [21]P3(a7,f13(a8),a17)
% 128.97/129.01 [25]~P3(a9,f13(a10),a11)
% 128.97/129.01 [31]~P1(x311)+P2(a1,x311,x311)
% 128.97/129.01 [32]~P1(x321)+P3(a4,x321,x321)
% 128.97/129.01 [26]~P1(x261)+P1(f6(x261))
% 128.97/129.01 [33]~P1(x331)+P2(f6(x331),x331,a1)
% 128.97/129.01 [40]~P2(x402,x401,x403)+P2(x401,x402,x403)
% 128.97/129.01 [41]~P3(x412,x411,x413)+P3(x411,x412,x413)
% 128.97/129.01 [34]~P1(x341)+P2(a1,x341,a1)+P1(f13(x341))
% 128.97/129.01 [38]~P1(x381)+P3(f13(x381),x381,a4)+P2(a1,x381,a1)
% 128.97/129.01 [37]~P4(x372,x371)+~P4(x371,x372)+P2(a1,x371,x372)
% 128.97/129.01 [28]~P1(x282)+~P1(x281)+P1(f3(x281,x282))
% 128.97/129.01 [29]~P1(x292)+~P1(x291)+P1(f14(x291,x292))
% 128.97/129.01 [35]~P1(x352)+~P1(x351)+P2(x351,x352,f3(x351,x352))
% 128.97/129.01 [36]~P1(x362)+~P1(x361)+P3(x361,x362,f14(x361,x362))
% 128.97/129.01 [30]~P4(x301,x303)+P4(x301,x302)+~P4(x303,x302)
% 128.97/129.01 [27]P4(x272,x271)+~P1(x271)+~P1(x272)+P4(x271,x272)
% 128.97/129.01 [39]~P3(x393,x392,x391)+P4(a1,x391)+~P4(a1,x392)+~P4(a1,x393)
% 128.97/129.01 [42]~P2(x423,x425,x421)+P4(x421,x422)+~P2(x424,x425,x422)+~P4(x423,x424)
% 128.97/129.01 [43]~P2(x431,x436,x434)+P2(x431,x432,x433)+~P2(x434,x435,x433)+~P2(x436,x435,x432)
% 128.97/129.01 [44]~P2(x446,x444,x441)+P2(x441,x442,x443)+~P2(x444,x442,x445)+~P2(x446,x445,x443)
% 128.97/129.01 [45]~P3(x451,x456,x454)+P3(x451,x452,x453)+~P3(x454,x455,x453)+~P3(x456,x455,x452)
% 128.97/129.01 [46]~P3(x466,x464,x461)+P3(x461,x462,x463)+~P3(x464,x462,x465)+~P3(x466,x465,x463)
% 128.97/129.01 [47]~P3(x475,x477,x472)+~P3(x474,x477,x471)+P2(x471,x472,x473)+~P2(x474,x475,x476)+~P3(x476,x477,x473)
% 128.97/129.01 [48]~P3(x487,x482,x485)+~P3(x486,x482,x484)+P3(x481,x482,x483)+~P2(x484,x485,x483)+~P2(x486,x487,x481)
% 128.97/129.01 %EqnAxiom
% 128.97/129.01
% 128.97/129.01 %-------------------------------------------
% 129.05/129.03 cnf(49,plain,
% 129.05/129.03 (~P2(a5,a1,a1)),
% 129.05/129.03 inference(scs_inference,[],[23,40])).
% 129.05/129.03 cnf(51,plain,
% 129.05/129.03 (~P3(f13(a10),a9,a11)),
% 129.05/129.03 inference(scs_inference,[],[23,25,40,41])).
% 129.05/129.03 cnf(53,plain,
% 129.05/129.03 (P4(a1,a1)),
% 129.05/129.03 inference(scs_inference,[],[23,25,1,40,41,27])).
% 129.05/129.03 cnf(58,plain,
% 129.05/129.03 (~P2(a8,a1,a1)),
% 129.05/129.03 inference(scs_inference,[],[24,40])).
% 129.05/129.03 cnf(60,plain,
% 129.05/129.03 (P4(a4,a4)),
% 129.05/129.03 inference(scs_inference,[],[24,2,40,27])).
% 129.05/129.03 cnf(64,plain,
% 129.05/129.03 (P3(a15,x641,a15)+~P3(a7,x641,a7)),
% 129.05/129.03 inference(scs_inference,[],[18,24,2,40,27,37,46])).
% 129.05/129.03 cnf(67,plain,
% 129.05/129.03 (P4(a2,a2)),
% 129.05/129.03 inference(scs_inference,[],[3,27])).
% 129.05/129.03 cnf(74,plain,
% 129.05/129.03 (P4(a5,a5)),
% 129.05/129.03 inference(scs_inference,[],[4,27])).
% 129.05/129.03 cnf(76,plain,
% 129.05/129.03 (~P3(x761,a2,a2)+P3(x761,a16,a16)),
% 129.05/129.03 inference(scs_inference,[],[20,4,27,45])).
% 129.05/129.03 cnf(81,plain,
% 129.05/129.03 (P4(a7,a7)),
% 129.05/129.03 inference(scs_inference,[],[5,27])).
% 129.05/129.03 cnf(83,plain,
% 129.05/129.03 (~P2(x831,a12,a12)+P2(x831,a9,a9)),
% 129.05/129.03 inference(scs_inference,[],[15,5,27,43])).
% 129.05/129.03 cnf(88,plain,
% 129.05/129.03 (P4(a8,a8)),
% 129.05/129.03 inference(scs_inference,[],[6,27])).
% 129.05/129.03 cnf(90,plain,
% 129.05/129.03 (~P2(x901,a16,a16)+P2(x901,a11,a11)),
% 129.05/129.03 inference(scs_inference,[],[16,6,27,43])).
% 129.05/129.03 cnf(97,plain,
% 129.05/129.03 (~P3(x971,a5,a5)+P3(x971,a10,a10)),
% 129.05/129.03 inference(scs_inference,[],[19,7,27,45])).
% 129.05/129.03 cnf(102,plain,
% 129.05/129.03 (P4(a18,a18)),
% 129.05/129.03 inference(scs_inference,[],[8,27])).
% 129.05/129.03 cnf(104,plain,
% 129.05/129.03 (P3(a12,x1041,a12)+~P3(a8,x1041,a8)),
% 129.05/129.03 inference(scs_inference,[],[17,8,27,46])).
% 129.05/129.03 cnf(112,plain,
% 129.05/129.03 (P4(a10,a10)),
% 129.05/129.03 inference(scs_inference,[],[10,27])).
% 129.05/129.03 cnf(114,plain,
% 129.05/129.03 (P3(a17,x1141,a17)+~P3(f13(a8),x1141,f13(a8))),
% 129.05/129.03 inference(scs_inference,[],[21,10,27,46])).
% 129.05/129.03 cnf(118,plain,
% 129.05/129.03 (P2(a9,x1181,a9)+~P2(a15,x1181,a15)),
% 129.05/129.03 inference(scs_inference,[],[15,21,18,10,27,46,45,44])).
% 129.05/129.03 cnf(121,plain,
% 129.05/129.03 (P4(a12,a12)),
% 129.05/129.03 inference(scs_inference,[],[11,27])).
% 129.05/129.03 cnf(123,plain,
% 129.05/129.03 (P3(a10,x1231,a10)+~P3(a8,x1231,a8)),
% 129.05/129.03 inference(scs_inference,[],[19,11,27,46])).
% 129.05/129.03 cnf(126,plain,
% 129.05/129.03 (P4(a15,a15)),
% 129.05/129.03 inference(scs_inference,[],[12,27])).
% 129.05/129.03 cnf(128,plain,
% 129.05/129.03 (~P3(x1281,a2,a2)+P3(x1281,a12,a12)),
% 129.05/129.03 inference(scs_inference,[],[17,12,27,45])).
% 129.05/129.03 cnf(133,plain,
% 129.05/129.03 (P4(a16,a16)),
% 129.05/129.03 inference(scs_inference,[],[13,27])).
% 129.05/129.03 cnf(135,plain,
% 129.05/129.03 (~P3(x1351,a5,a5)+P3(x1351,a15,a15)),
% 129.05/129.03 inference(scs_inference,[],[18,13,27,45])).
% 129.05/129.03 cnf(140,plain,
% 129.05/129.03 (P4(a17,a17)),
% 129.05/129.03 inference(scs_inference,[],[14,27])).
% 129.05/129.03 cnf(150,plain,
% 129.05/129.03 (P2(a10,a10,a10)+~P2(a5,a5,a5)),
% 129.05/129.03 inference(scs_inference,[],[19,47])).
% 129.05/129.03 cnf(153,plain,
% 129.05/129.03 (P1(f6(f3(a4,a4)))),
% 129.05/129.03 inference(scs_inference,[],[2,26,28])).
% 129.05/129.03 cnf(156,plain,
% 129.05/129.03 (~P3(a15,x1561,a15)+~P3(a12,x1561,a12)+P3(a9,x1561,a9)),
% 129.05/129.03 inference(scs_inference,[],[15,20,140,48])).
% 129.05/129.03 cnf(177,plain,
% 129.05/129.03 (P2(a1,f6(a7),f6(a7))),
% 129.05/129.03 inference(scs_inference,[],[5,31,26])).
% 129.05/129.03 cnf(178,plain,
% 129.05/129.03 (P4(f6(a7),f6(a7))),
% 129.05/129.03 inference(scs_inference,[],[177,53,42])).
% 129.05/129.03 cnf(268,plain,
% 129.05/129.03 (~P3(a17,x2681,a17)+~P3(a16,x2681,a16)+P3(a11,x2681,a11)),
% 129.05/129.03 inference(scs_inference,[],[16,178,48])).
% 129.05/129.03 cnf(277,plain,
% 129.05/129.03 (P2(f6(f6(a11)),f6(a11),a1)),
% 129.05/129.03 inference(scs_inference,[],[7,33,26])).
% 129.05/129.03 cnf(280,plain,
% 129.05/129.03 (~P2(a5,f6(a11),f6(a11))),
% 129.05/129.03 inference(scs_inference,[],[23,277,44,40])).
% 129.05/129.03 cnf(285,plain,
% 129.05/129.03 (~P2(a8,f6(a11),f6(a11))),
% 129.05/129.03 inference(scs_inference,[],[24,277,44,40])).
% 129.05/129.03 cnf(365,plain,
% 129.05/129.03 (~P3(x3651,a7,a7)+P3(a15,x3651,a15)),
% 129.05/129.03 inference(scs_inference,[],[64,41])).
% 129.05/129.03 cnf(381,plain,
% 129.05/129.03 (P3(a16,x3811,a16)+~P3(x3811,a2,a2)),
% 129.05/129.03 inference(scs_inference,[],[76,41])).
% 129.05/129.03 cnf(413,plain,
% 129.05/129.03 (P2(a9,x4131,a9)+~P2(x4131,a12,a12)),
% 129.05/129.03 inference(scs_inference,[],[83,40])).
% 129.05/129.03 cnf(445,plain,
% 129.05/129.03 (P2(a11,x4451,a11)+~P2(x4451,a16,a16)),
% 129.05/129.03 inference(scs_inference,[],[90,40])).
% 129.05/129.03 cnf(477,plain,
% 129.05/129.03 (P3(a10,x4771,a10)+~P3(x4771,a5,a5)),
% 129.05/129.03 inference(scs_inference,[],[97,41])).
% 129.05/129.03 cnf(509,plain,
% 129.05/129.03 (~P3(x5091,a8,a8)+P3(a12,x5091,a12)),
% 129.05/129.03 inference(scs_inference,[],[104,41])).
% 129.05/129.03 cnf(525,plain,
% 129.05/129.03 (~P3(x5251,a8,a8)+P3(a10,x5251,a10)),
% 129.05/129.03 inference(scs_inference,[],[123,41])).
% 129.05/129.03 cnf(541,plain,
% 129.05/129.03 (P3(a12,x5411,a12)+~P3(x5411,a2,a2)),
% 129.05/129.03 inference(scs_inference,[],[128,41])).
% 129.05/129.03 cnf(573,plain,
% 129.05/129.03 (P3(a15,x5731,a15)+~P3(x5731,a5,a5)),
% 129.05/129.03 inference(scs_inference,[],[135,41])).
% 129.05/129.03 cnf(733,plain,
% 129.05/129.03 (P3(a16,a4,a16)),
% 129.05/129.03 inference(scs_inference,[],[3,381,32])).
% 129.05/129.03 cnf(734,plain,
% 129.05/129.03 (P3(a11,a4,a11)+~P3(a17,a4,a17)),
% 129.05/129.03 inference(scs_inference,[],[733,268])).
% 129.05/129.03 cnf(739,plain,
% 129.05/129.03 (P3(a16,x7391,a16)+~P3(a4,x7391,a4)),
% 129.05/129.03 inference(scs_inference,[],[733,46])).
% 129.05/129.03 cnf(755,plain,
% 129.05/129.03 (P2(a9,a1,a9)),
% 129.05/129.03 inference(scs_inference,[],[11,413,31])).
% 129.05/129.03 cnf(766,plain,
% 129.05/129.03 (P2(a9,x7661,a9)+~P2(a1,x7661,a1)),
% 129.05/129.03 inference(scs_inference,[],[755,44])).
% 129.05/129.03 cnf(796,plain,
% 129.05/129.03 (P2(a11,a1,a11)),
% 129.05/129.03 inference(scs_inference,[],[13,445,31])).
% 129.05/129.03 cnf(804,plain,
% 129.05/129.03 (P2(a11,x8041,a11)+~P2(a1,x8041,a1)),
% 129.05/129.03 inference(scs_inference,[],[796,44])).
% 129.05/129.03 cnf(836,plain,
% 129.05/129.03 (P3(a10,a4,a10)),
% 129.05/129.03 inference(scs_inference,[],[4,477,32])).
% 129.05/129.03 cnf(856,plain,
% 129.05/129.03 (P3(x8561,a12,a12)+~P3(x8561,a8,a8)),
% 129.05/129.03 inference(scs_inference,[],[509,41])).
% 129.05/129.03 cnf(872,plain,
% 129.05/129.03 (P3(x8721,a10,a10)+~P3(x8721,a8,a8)),
% 129.05/129.03 inference(scs_inference,[],[525,41])).
% 129.05/129.03 cnf(888,plain,
% 129.05/129.03 (P3(a12,a4,a12)),
% 129.05/129.03 inference(scs_inference,[],[3,541,32])).
% 129.05/129.03 cnf(889,plain,
% 129.05/129.03 (P3(a9,a4,a9)+~P3(a15,a4,a15)),
% 129.05/129.03 inference(scs_inference,[],[888,156])).
% 129.05/129.03 cnf(910,plain,
% 129.05/129.03 (P3(a15,a4,a15)),
% 129.05/129.03 inference(scs_inference,[],[4,573,32])).
% 129.05/129.03 cnf(911,plain,
% 129.05/129.03 (P3(a9,a4,a9)),
% 129.05/129.03 inference(scs_inference,[],[910,889])).
% 129.05/129.03 cnf(923,plain,
% 129.05/129.03 (~P1(f13(a10))+~P3(f14(f13(a10),a9),a4,a11)),
% 129.05/129.03 inference(scs_inference,[],[51,911,9,45,41,36])).
% 129.05/129.03 cnf(926,plain,
% 129.05/129.03 (P3(a9,x9261,a9)+~P3(a4,x9261,a4)),
% 129.05/129.03 inference(scs_inference,[],[911,46])).
% 129.05/129.03 cnf(974,plain,
% 129.05/129.03 (~P3(a17,a4,a17)+P3(a4,a11,a11)),
% 129.05/129.03 inference(scs_inference,[],[734,41])).
% 129.05/129.03 cnf(1005,plain,
% 129.05/129.03 (~P3(x10051,a4,a4)+P3(a16,x10051,a16)),
% 129.05/129.03 inference(scs_inference,[],[739,41])).
% 129.05/129.03 cnf(1148,plain,
% 129.05/129.03 (P3(a4,a12,a12)),
% 129.05/129.03 inference(scs_inference,[],[6,856,32])).
% 129.05/129.03 cnf(1170,plain,
% 129.05/129.03 (P3(a4,a10,a10)),
% 129.05/129.03 inference(scs_inference,[],[6,872,32])).
% 129.05/129.03 cnf(1254,plain,
% 129.05/129.03 (~P3(x12541,a4,a4)+P3(a9,x12541,a9)),
% 129.05/129.03 inference(scs_inference,[],[926,41])).
% 129.05/129.03 cnf(1286,plain,
% 129.05/129.03 (~P3(f13(a8),a4,f13(a8))+P3(a4,a11,a11)),
% 129.05/129.03 inference(scs_inference,[],[974,114])).
% 129.05/129.03 cnf(1306,plain,
% 129.05/129.03 (P3(x13061,a16,a16)+~P3(x13061,a4,a4)),
% 129.05/129.03 inference(scs_inference,[],[1005,41])).
% 129.05/129.03 cnf(1428,plain,
% 129.05/129.03 (P3(x14281,a9,a9)+~P3(x14281,a4,a4)),
% 129.05/129.03 inference(scs_inference,[],[1254,41])).
% 129.05/129.03 cnf(1490,plain,
% 129.05/129.03 (P3(a4,a16,a16)),
% 129.05/129.03 inference(scs_inference,[],[2,1306,32])).
% 129.05/129.03 cnf(1510,plain,
% 129.05/129.03 (P3(a4,a9,a9)),
% 129.05/129.03 inference(scs_inference,[],[2,1428,32])).
% 129.05/129.03 cnf(2009,plain,
% 129.05/129.03 (~P3(a4,f13(a8),f13(a8))+P3(a4,a11,a11)),
% 129.05/129.03 inference(scs_inference,[],[1286,41])).
% 129.05/129.03 cnf(2122,plain,
% 129.05/129.03 (~P1(f13(a8))+P3(a4,a11,a11)),
% 129.05/129.03 inference(scs_inference,[],[2009,32])).
% 129.05/129.03 cnf(2140,plain,
% 129.05/129.03 (P3(a4,a11,a11)),
% 129.05/129.03 inference(scs_inference,[],[24,6,2122,34])).
% 129.05/129.03 cnf(3630,plain,
% 129.05/129.03 (~P2(f6(a7),x36301,a8)+~P2(f6(a7),x36301,a1)),
% 129.05/129.03 inference(scs_inference,[],[24,177,43])).
% 129.05/129.03 cnf(3635,plain,
% 129.05/129.03 (~P2(f6(a7),x36351,a5)+~P2(f6(a7),x36351,a1)),
% 129.05/129.03 inference(scs_inference,[],[23,177,43])).
% 129.05/129.03 cnf(3649,plain,
% 129.05/129.03 (~P2(f6(a7),a7,a8)),
% 129.05/129.03 inference(scs_inference,[],[5,3630,33])).
% 129.05/129.03 cnf(3650,plain,
% 129.05/129.03 (~P2(a7,f6(a7),a8)),
% 129.05/129.03 inference(scs_inference,[],[3649,40])).
% 129.05/129.03 cnf(3652,plain,
% 129.05/129.03 (~P2(a1,x36521,a8)+~P2(f6(a7),a7,x36521)),
% 129.05/129.03 inference(scs_inference,[],[3649,177,40,44])).
% 129.05/129.03 cnf(3673,plain,
% 129.05/129.03 (~P2(a1,a1,a8)),
% 129.05/129.03 inference(scs_inference,[],[5,3652,33])).
% 129.05/129.03 cnf(3721,plain,
% 129.05/129.03 (~P2(f6(a7),a7,a5)),
% 129.05/129.03 inference(scs_inference,[],[5,3635,33])).
% 129.05/129.03 cnf(3722,plain,
% 129.05/129.03 (~P2(a7,f6(a7),a5)),
% 129.05/129.03 inference(scs_inference,[],[3721,40])).
% 129.05/129.03 cnf(3740,plain,
% 129.05/129.03 (P3(f13(a5),a2,a16)),
% 129.05/129.03 inference(scs_inference,[],[20,41])).
% 129.05/129.03 cnf(3748,plain,
% 129.05/129.03 (P3(a8,a2,a12)),
% 129.05/129.03 inference(scs_inference,[],[17,41])).
% 129.05/129.03 cnf(3755,plain,
% 129.05/129.03 (P3(f13(a8),a7,a17)),
% 129.05/129.03 inference(scs_inference,[],[21,41])).
% 129.05/129.03 cnf(3762,plain,
% 129.05/129.03 (P3(a7,a5,a15)),
% 129.05/129.03 inference(scs_inference,[],[18,41])).
% 129.05/129.03 cnf(3769,plain,
% 129.05/129.03 (P3(a8,a5,a10)),
% 129.05/129.03 inference(scs_inference,[],[19,41])).
% 129.05/129.03 cnf(3774,plain,
% 129.05/129.03 (P3(a11,a4,a11)),
% 129.05/129.03 inference(scs_inference,[],[2140,41])).
% 129.05/129.03 cnf(3789,plain,
% 129.05/129.03 (P2(a15,a12,a9)),
% 129.05/129.03 inference(scs_inference,[],[15,40])).
% 129.05/129.03 cnf(3794,plain,
% 129.05/129.03 (P2(a17,a16,a11)),
% 129.05/129.03 inference(scs_inference,[],[16,40])).
% 129.05/129.03 cnf(3799,plain,
% 129.05/129.03 (P2(a1,a9,a9)),
% 129.05/129.03 inference(scs_inference,[],[755,40])).
% 129.05/129.03 cnf(3801,plain,
% 129.05/129.03 (~P3(a1,a1,x38011)+P4(a1,x38011)),
% 129.05/129.04 inference(scs_inference,[],[755,53,40,39])).
% 129.05/129.04 cnf(3808,plain,
% 129.05/129.04 (~P2(a9,x38081,a8)+~P2(a9,x38081,a1)),
% 129.05/129.04 inference(scs_inference,[],[24,796,3799,40,43])).
% 129.05/129.04 cnf(3813,plain,
% 129.05/129.04 (P4(a1,f14(a1,a1))),
% 129.05/129.04 inference(scs_inference,[],[1,3801,36])).
% 129.05/129.04 cnf(3814,plain,
% 129.05/129.04 (P2(f6(a11),f6(f6(a11)),a1)),
% 129.05/129.04 inference(scs_inference,[],[277,40])).
% 129.05/129.04 cnf(3821,plain,
% 129.05/129.04 (P2(f6(a7),a1,f6(a7))),
% 129.05/129.04 inference(scs_inference,[],[177,40])).
% 129.05/129.04 cnf(3838,plain,
% 129.05/129.04 (~P2(a7,f6(a7),x38381)+~P2(x38381,a1,a8)),
% 129.05/129.04 inference(scs_inference,[],[3650,3821,43])).
% 129.05/129.04 cnf(3843,plain,
% 129.05/129.04 (~P2(a7,f6(a7),x38431)+~P2(x38431,a1,a5)),
% 129.05/129.04 inference(scs_inference,[],[3722,3821,43])).
% 129.05/129.04 cnf(3864,plain,
% 129.05/129.04 (~P2(a9,x38641,a1)+~P2(a9,x38641,a4)),
% 129.05/129.04 inference(scs_inference,[],[3799,22,43])).
% 129.05/129.04 cnf(3896,plain,
% 129.05/129.04 (P3(f13(a8),a8,a4)),
% 129.05/129.04 inference(scs_inference,[],[24,6,38])).
% 129.05/129.04 cnf(3898,plain,
% 129.05/129.04 (P3(a8,f13(a8),a4)),
% 129.05/129.04 inference(scs_inference,[],[24,6,38,41])).
% 129.05/129.04 cnf(3900,plain,
% 129.05/129.04 (P2(a4,a4,a4)+~P2(f13(a8),f13(a8),f13(a8))),
% 129.05/129.04 inference(scs_inference,[],[24,6,38,41,47])).
% 129.05/129.04 cnf(3909,plain,
% 129.05/129.04 (P3(f13(a5),a5,a4)),
% 129.05/129.04 inference(scs_inference,[],[23,4,38])).
% 129.05/129.04 cnf(3911,plain,
% 129.05/129.04 (P3(a5,f13(a5),a4)),
% 129.05/129.04 inference(scs_inference,[],[23,4,38,41])).
% 129.05/129.04 cnf(3916,plain,
% 129.05/129.04 (P2(a4,a4,a4)+~P2(a5,a5,a5)),
% 129.05/129.04 inference(scs_inference,[],[3911,47])).
% 129.05/129.04 cnf(3924,plain,
% 129.05/129.04 (P2(a4,a4,a4)+~P2(f13(a5),f13(a5),f13(a5))),
% 129.05/129.04 inference(scs_inference,[],[3909,47])).
% 129.05/129.04 cnf(3959,plain,
% 129.05/129.04 (~P2(a2,x39591,x39592)+~P2(a2,x39591,x39593)+~P3(a16,a9,a4)+P4(x39592,x39593)),
% 129.05/129.04 inference(scs_inference,[],[67,20,285,3774,51,46,42])).
% 129.05/129.04 cnf(4052,plain,
% 129.05/129.04 (~P2(x40521,a9,a1)+~P2(a9,x40521,a8)),
% 129.05/129.04 inference(scs_inference,[],[3808,40])).
% 129.05/129.04 cnf(4116,plain,
% 129.05/129.04 (~P2(x41161,a9,a4)+~P2(a9,x41161,a1)),
% 129.05/129.04 inference(scs_inference,[],[3864,40])).
% 129.05/129.04 cnf(4256,plain,
% 129.05/129.04 (~P2(x42561,a9,a8)+~P2(x42561,a9,a1)),
% 129.05/129.04 inference(scs_inference,[],[4052,40])).
% 129.05/129.04 cnf(4320,plain,
% 129.05/129.04 (~P2(x43201,a9,a1)+~P2(x43201,a9,a4)),
% 129.05/129.04 inference(scs_inference,[],[4116,40])).
% 129.05/129.04 cnf(4367,plain,
% 129.05/129.04 (~P2(f6(a9),a9,a8)),
% 129.05/129.04 inference(scs_inference,[],[9,4256,33])).
% 129.05/129.04 cnf(4441,plain,
% 129.05/129.04 (~P2(a9,x44411,a4)+~P2(x44411,a9,a1)),
% 129.05/129.04 inference(scs_inference,[],[4320,40])).
% 129.05/129.04 cnf(4489,plain,
% 129.05/129.04 (~P2(a9,f6(a9),a4)),
% 129.05/129.04 inference(scs_inference,[],[9,4441,33])).
% 129.05/129.04 cnf(4503,plain,
% 129.05/129.04 (~P2(a1,x45031,a4)+~P2(a9,f6(a9),x45031)),
% 129.05/129.04 inference(scs_inference,[],[4489,3799,44])).
% 129.05/129.04 cnf(4593,plain,
% 129.05/129.04 (~P2(f6(a7),a7,x45931)+~P2(x45931,a1,a8)),
% 129.05/129.04 inference(scs_inference,[],[3838,40])).
% 129.05/129.04 cnf(4609,plain,
% 129.05/129.04 (~P2(f6(a7),a7,x46091)+~P2(x46091,a1,a5)),
% 129.05/129.04 inference(scs_inference,[],[3843,40])).
% 129.05/129.04 cnf(4801,plain,
% 129.05/129.04 (~P2(a15,f6(a9),a15)+~P2(a1,a9,a4)),
% 129.05/129.04 inference(scs_inference,[],[4503,118])).
% 129.05/129.04 cnf(4897,plain,
% 129.05/129.04 (~P1(f6(a7))+~P2(f3(f6(a7),a7),a1,a8)),
% 129.05/129.04 inference(scs_inference,[],[5,4593,35])).
% 129.05/129.04 cnf(4913,plain,
% 129.05/129.04 (~P2(a1,a1,a5)),
% 129.05/129.04 inference(scs_inference,[],[5,4609,33])).
% 129.05/129.04 cnf(5105,plain,
% 129.05/129.04 (~P2(f6(a9),a15,a15)+~P2(a1,a9,a4)),
% 129.05/129.04 inference(scs_inference,[],[4801,40])).
% 129.05/129.04 cnf(5185,plain,
% 129.05/129.04 (~P2(x51851,a9,a15)+~P2(x51851,a12,f6(a9))+~P2(a1,a9,a4)),
% 129.05/129.04 inference(scs_inference,[],[15,5105,44])).
% 129.05/129.04 cnf(5345,plain,
% 129.05/129.04 (~P2(f3(f6(a7),a7),a1,a8)),
% 129.05/129.04 inference(scs_inference,[],[5,4897,26])).
% 129.05/129.04 cnf(5425,plain,
% 129.05/129.04 (~P3(x54251,a9,a8)+~P3(x54252,a9,f6(a9))+~P2(x54252,a4,x54251)),
% 129.05/129.04 inference(scs_inference,[],[4367,280,1510,60,47])).
% 129.05/129.04 cnf(7348,plain,
% 129.05/129.04 (P3(a12,x73481,a12)+~P3(a2,x73481,a2)),
% 129.05/129.04 inference(scs_inference,[],[3748,46])).
% 129.05/129.04 cnf(7353,plain,
% 129.05/129.04 (P3(a17,x73531,a17)+~P3(a7,x73531,a7)),
% 129.05/129.04 inference(scs_inference,[],[3755,46])).
% 129.05/129.04 cnf(7387,plain,
% 129.05/129.04 (P3(a4,x73871,a4)+~P3(f13(a5),x73871,f13(a5))),
% 129.05/129.04 inference(scs_inference,[],[3911,46])).
% 129.05/129.04 cnf(7414,plain,
% 129.05/129.04 (P3(a4,x74141,a4)+~P3(a8,x74141,a8)),
% 129.05/129.04 inference(scs_inference,[],[3896,46])).
% 129.05/129.04 cnf(7433,plain,
% 129.05/129.04 (P3(a4,x74331,a4)+~P3(a5,x74331,a5)),
% 129.05/129.04 inference(scs_inference,[],[3909,46])).
% 129.05/129.04 cnf(7479,plain,
% 129.05/129.04 (~P3(a2,a4,x74791)+~P3(x74791,a12,a2)+P3(a12,a12,a12)),
% 129.05/129.04 inference(scs_inference,[],[1148,7348,45])).
% 129.05/129.04 cnf(7511,plain,
% 129.05/129.04 (~P3(x75111,a7,a7)+P3(a17,x75111,a17)),
% 129.05/129.04 inference(scs_inference,[],[7353,41])).
% 129.05/129.04 cnf(7525,plain,
% 129.05/129.04 (~P2(x75251,x75252,a1)+~P2(x75251,x75253,a1)+~P2(x75253,a8,x75252)),
% 129.05/129.04 inference(scs_inference,[],[24,49,60,44])).
% 129.05/129.04 cnf(7538,plain,
% 129.05/129.04 (P1(f6(a16))),
% 129.05/129.04 inference(scs_inference,[],[13,26])).
% 129.05/129.04 cnf(7540,plain,
% 129.05/129.04 (P2(a1,a16,a16)),
% 129.05/129.04 inference(scs_inference,[],[13,26,31])).
% 129.05/129.04 cnf(7544,plain,
% 129.05/129.04 (P2(f6(a16),a16,a1)),
% 129.05/129.04 inference(scs_inference,[],[13,4489,26,31,40,33])).
% 129.05/129.04 cnf(7546,plain,
% 129.05/129.04 (P3(a4,a18,a18)),
% 129.05/129.04 inference(scs_inference,[],[13,8,4489,26,31,40,33,32])).
% 129.05/129.04 cnf(7548,plain,
% 129.05/129.04 (P1(f3(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[13,8,4489,26,31,40,33,32,28])).
% 129.05/129.04 cnf(7550,plain,
% 129.05/129.04 (P1(f14(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[13,8,4489,26,31,40,33,32,28,29])).
% 129.05/129.04 cnf(7552,plain,
% 129.05/129.04 (P1(f13(a5))),
% 129.05/129.04 inference(scs_inference,[],[13,8,4489,4,23,26,31,40,33,32,28,29,34])).
% 129.05/129.04 cnf(7554,plain,
% 129.05/129.04 (~P2(a16,a8,a16)),
% 129.05/129.04 inference(scs_inference,[],[13,8,4489,4,23,26,31,40,33,32,28,29,34,7525])).
% 129.05/129.04 cnf(7556,plain,
% 129.05/129.04 (P3(a16,a16,f14(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[13,8,4489,4,23,26,31,40,33,32,28,29,34,7525,36])).
% 129.05/129.04 cnf(7558,plain,
% 129.05/129.04 (P2(a16,a16,f3(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[13,8,4489,4,23,26,31,40,33,32,28,29,34,7525,36,35])).
% 129.05/129.04 cnf(7560,plain,
% 129.05/129.04 (P2(a1,a15,a15)),
% 129.05/129.04 inference(scs_inference,[],[126,13,8,4489,4,23,26,31,40,33,32,28,29,34,7525,36,35,37])).
% 129.05/129.04 cnf(7564,plain,
% 129.05/129.04 (~P2(a16,a5,a16)),
% 129.05/129.04 inference(scs_inference,[],[126,13,8,4489,4,23,26,31,40,33,32,28,29,34,7525,36,35,37,27,44])).
% 129.05/129.04 cnf(7566,plain,
% 129.05/129.04 (~P2(a8,f6(a16),f6(a16))),
% 129.05/129.04 inference(scs_inference,[],[126,13,8,58,4489,4,23,26,31,40,33,32,28,29,34,7525,36,35,37,27,44,43])).
% 129.05/129.04 cnf(7568,plain,
% 129.05/129.04 (P4(f3(a16,a16),f3(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[133,126,13,8,58,4489,4,23,26,31,40,33,32,28,29,34,7525,36,35,37,27,44,43,42])).
% 129.05/129.04 cnf(7570,plain,
% 129.05/129.04 (P3(f3(a16,a16),a4,f3(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[133,126,13,8,58,4489,4,23,733,26,31,40,33,32,28,29,34,7525,36,35,37,27,44,43,42,48])).
% 129.05/129.04 cnf(7576,plain,
% 129.05/129.04 (P1(f6(a15))),
% 129.05/129.04 inference(scs_inference,[],[12,26])).
% 129.05/129.04 cnf(7578,plain,
% 129.05/129.04 (P2(a1,f6(a16),f6(a16))),
% 129.05/129.04 inference(scs_inference,[],[7538,12,26,31])).
% 129.05/129.04 cnf(7580,plain,
% 129.05/129.04 (P2(f6(a15),a15,a1)),
% 129.05/129.04 inference(scs_inference,[],[7538,12,26,31,33])).
% 129.05/129.04 cnf(7582,plain,
% 129.05/129.04 (~P2(a8,a16,a16)),
% 129.05/129.04 inference(scs_inference,[],[7554,7538,12,26,31,33,40])).
% 129.05/129.04 cnf(7584,plain,
% 129.05/129.04 (P3(a4,f6(a16),f6(a16))),
% 129.05/129.04 inference(scs_inference,[],[7554,7538,12,26,31,33,40,32])).
% 129.05/129.04 cnf(7586,plain,
% 129.05/129.04 (P1(f13(a8))),
% 129.05/129.04 inference(scs_inference,[],[7554,7538,12,6,24,26,31,33,40,32,34])).
% 129.05/129.04 cnf(7588,plain,
% 129.05/129.04 (P1(f14(a15,a15))),
% 129.05/129.04 inference(scs_inference,[],[7554,7538,12,6,24,26,31,33,40,32,34,29])).
% 129.05/129.04 cnf(7590,plain,
% 129.05/129.04 (~P2(a15,a8,a15)),
% 129.05/129.04 inference(scs_inference,[],[7554,7538,12,6,24,26,31,33,40,32,34,29,7525])).
% 129.05/129.04 cnf(7592,plain,
% 129.05/129.04 (P1(f3(a15,a15))),
% 129.05/129.04 inference(scs_inference,[],[7554,7538,12,6,24,26,31,33,40,32,34,29,7525,28])).
% 129.05/129.04 cnf(7594,plain,
% 129.05/129.04 (P3(a15,a15,f14(a15,a15))),
% 129.05/129.04 inference(scs_inference,[],[7554,7538,12,6,24,26,31,33,40,32,34,29,7525,28,36])).
% 129.05/129.04 cnf(7596,plain,
% 129.05/129.04 (P2(a1,f3(a16,a16),f3(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[7554,7568,7538,12,6,24,26,31,33,40,32,34,29,7525,28,36,37])).
% 129.05/129.04 cnf(7598,plain,
% 129.05/129.04 (P2(a15,a15,f3(a15,a15))),
% 129.05/129.04 inference(scs_inference,[],[7554,7568,7538,12,6,24,26,31,33,40,32,34,29,7525,28,36,37,35])).
% 129.05/129.04 cnf(7604,plain,
% 129.05/129.04 (P2(f6(a16),f3(a16,a16),a16)),
% 129.05/129.04 inference(scs_inference,[],[7540,7554,7568,7558,7538,7556,7544,12,1490,6,24,733,26,31,33,40,32,34,29,7525,28,36,37,35,45,46,43])).
% 129.05/129.04 cnf(7606,plain,
% 129.05/129.04 (P4(f3(a15,a15),f3(a15,a15))),
% 129.05/129.04 inference(scs_inference,[],[7540,7554,7568,7558,7538,7556,7544,126,12,1490,6,24,733,26,31,33,40,32,34,29,7525,28,36,37,35,45,46,43,42])).
% 129.05/129.04 cnf(7615,plain,
% 129.05/129.04 (P1(f6(a17))),
% 129.05/129.04 inference(scs_inference,[],[14,26])).
% 129.05/129.04 cnf(7617,plain,
% 129.05/129.04 (P2(a1,f14(a16,a16),f14(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[7550,14,26,31])).
% 129.05/129.04 cnf(7619,plain,
% 129.05/129.04 (~P2(a5,a16,a16)),
% 129.05/129.04 inference(scs_inference,[],[7564,7550,14,26,31,40])).
% 129.05/129.04 cnf(7621,plain,
% 129.05/129.04 (P2(f6(a17),a17,a1)),
% 129.05/129.04 inference(scs_inference,[],[7564,7550,14,26,31,40,33])).
% 129.05/129.04 cnf(7625,plain,
% 129.05/129.04 (P1(f14(a17,a17))),
% 129.05/129.04 inference(scs_inference,[],[7564,7548,7550,14,26,31,40,33,32,29])).
% 129.05/129.04 cnf(7627,plain,
% 129.05/129.04 (~P2(a17,a8,a17)),
% 129.05/129.04 inference(scs_inference,[],[7564,7548,7550,14,26,31,40,33,32,29,7525])).
% 129.05/129.04 cnf(7629,plain,
% 129.05/129.04 (P3(a17,a17,f14(a17,a17))),
% 129.05/129.04 inference(scs_inference,[],[7564,7548,7550,14,26,31,40,33,32,29,7525,36])).
% 129.05/129.04 cnf(7631,plain,
% 129.05/129.04 (P1(f3(a17,a17))),
% 129.05/129.04 inference(scs_inference,[],[7564,7548,7550,14,26,31,40,33,32,29,7525,36,28])).
% 129.05/129.04 cnf(7633,plain,
% 129.05/129.04 (P2(a17,a17,f3(a17,a17))),
% 129.05/129.04 inference(scs_inference,[],[7564,7548,7550,14,26,31,40,33,32,29,7525,36,28,35])).
% 129.05/129.04 cnf(7635,plain,
% 129.05/129.04 (P2(a1,f3(a15,a15),f3(a15,a15))),
% 129.05/129.04 inference(scs_inference,[],[7564,7606,7548,7550,14,26,31,40,33,32,29,7525,36,28,35,37])).
% 129.05/129.04 cnf(7637,plain,
% 129.05/129.04 (~P2(f3(a16,a16),a5,f3(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[7564,7606,7548,7550,7604,14,26,31,40,33,32,29,7525,36,28,35,37,44])).
% 129.05/129.04 cnf(7639,plain,
% 129.05/129.04 (P2(f6(a15),f3(a15,a15),a15)),
% 129.05/129.04 inference(scs_inference,[],[7564,7560,7606,7548,7550,7604,7598,7580,14,26,31,40,33,32,29,7525,36,28,35,37,44,43])).
% 129.05/129.04 cnf(7649,plain,
% 129.05/129.04 (P1(f6(a18))),
% 129.05/129.04 inference(scs_inference,[],[7631,8,31,26])).
% 129.05/129.04 cnf(7651,plain,
% 129.05/129.04 (P2(f6(a18),a18,a1)),
% 129.05/129.04 inference(scs_inference,[],[7631,8,31,26,33])).
% 129.05/129.04 cnf(7653,plain,
% 129.05/129.04 (~P2(a8,a15,a15)),
% 129.05/129.04 inference(scs_inference,[],[7590,7631,8,31,26,33,40])).
% 129.05/129.04 cnf(7657,plain,
% 129.05/129.04 (~P2(a18,a8,a18)),
% 129.05/129.04 inference(scs_inference,[],[7590,7631,8,31,26,33,40,32,7525])).
% 129.05/129.04 cnf(7659,plain,
% 129.05/129.04 (P3(a18,a18,f14(a18,a18))),
% 129.05/129.04 inference(scs_inference,[],[7590,7631,8,31,26,33,40,32,7525,36])).
% 129.05/129.04 cnf(7661,plain,
% 129.05/129.04 (P1(f14(a18,a18))),
% 129.05/129.04 inference(scs_inference,[],[7590,7631,8,31,26,33,40,32,7525,36,29])).
% 129.05/129.04 cnf(7663,plain,
% 129.05/129.04 (P1(f3(a18,a18))),
% 129.05/129.04 inference(scs_inference,[],[7590,7631,8,31,26,33,40,32,7525,36,29,28])).
% 129.05/129.04 cnf(7665,plain,
% 129.05/129.04 (P2(a18,a18,f3(a18,a18))),
% 129.05/129.04 inference(scs_inference,[],[7590,7631,8,31,26,33,40,32,7525,36,29,28,35])).
% 129.05/129.04 cnf(7667,plain,
% 129.05/129.04 (P2(a1,a17,a17)),
% 129.05/129.04 inference(scs_inference,[],[7590,7631,140,8,31,26,33,40,32,7525,36,29,28,35,37])).
% 129.05/129.04 cnf(7671,plain,
% 129.05/129.04 (~P2(a18,a5,a18)),
% 129.05/129.04 inference(scs_inference,[],[7590,7546,7631,140,8,23,31,26,33,40,32,7525,36,29,28,35,37,45,44])).
% 129.05/129.04 cnf(7673,plain,
% 129.05/129.04 (~P2(a8,f6(a15),f6(a15))),
% 129.05/129.04 inference(scs_inference,[],[7590,7546,7631,7639,140,8,23,31,26,33,40,32,7525,36,29,28,35,37,45,44,43])).
% 129.05/129.04 cnf(7684,plain,
% 129.05/129.04 (P1(f6(a2))),
% 129.05/129.04 inference(scs_inference,[],[3,26])).
% 129.05/129.04 cnf(7686,plain,
% 129.05/129.04 (P2(a1,f14(a18,a18),f14(a18,a18))),
% 129.05/129.04 inference(scs_inference,[],[7661,3,26,31])).
% 129.05/129.04 cnf(7688,plain,
% 129.05/129.04 (~P2(a8,a17,a17)),
% 129.05/129.04 inference(scs_inference,[],[7627,7661,3,26,31,40])).
% 129.05/129.04 cnf(7690,plain,
% 129.05/129.04 (P2(f6(a2),a2,a1)),
% 129.05/129.04 inference(scs_inference,[],[7627,7661,3,26,31,40,33])).
% 129.05/129.04 cnf(7692,plain,
% 129.05/129.04 (P3(a4,f13(a5),f13(a5))),
% 129.05/129.04 inference(scs_inference,[],[7627,7661,7552,3,26,31,40,33,32])).
% 129.05/129.04 cnf(7694,plain,
% 129.05/129.04 (P1(f14(a2,a2))),
% 129.05/129.04 inference(scs_inference,[],[7627,7661,7552,3,26,31,40,33,32,29])).
% 129.05/129.04 cnf(7696,plain,
% 129.05/129.04 (P3(a2,a2,f14(a2,a2))),
% 129.05/129.04 inference(scs_inference,[],[7627,7661,7552,3,26,31,40,33,32,29,36])).
% 129.05/129.04 cnf(7698,plain,
% 129.05/129.04 (~P2(a2,a8,a2)),
% 129.05/129.04 inference(scs_inference,[],[7627,7661,7552,3,26,31,40,33,32,29,36,7525])).
% 129.05/129.04 cnf(7700,plain,
% 129.05/129.04 (P1(f3(a2,a2))),
% 129.05/129.04 inference(scs_inference,[],[7627,7661,7552,3,26,31,40,33,32,29,36,7525,28])).
% 129.05/129.04 cnf(7702,plain,
% 129.05/129.04 (P2(a2,a2,f3(a2,a2))),
% 129.05/129.04 inference(scs_inference,[],[7627,7661,7552,3,26,31,40,33,32,29,36,7525,28,35])).
% 129.05/129.04 cnf(7704,plain,
% 129.05/129.04 (P2(a1,a12,a12)),
% 129.05/129.04 inference(scs_inference,[],[7627,7661,7552,121,3,26,31,40,33,32,29,36,7525,28,35,37])).
% 129.05/129.04 cnf(7706,plain,
% 129.05/129.04 (P3(a4,a4,a4)),
% 129.05/129.04 inference(scs_inference,[],[7627,7661,7552,3909,121,3,26,31,40,33,32,29,36,7525,28,35,37,45])).
% 129.05/129.04 cnf(7708,plain,
% 129.05/129.04 (P2(f6(a17),f3(a17,a17),a17)),
% 129.05/129.04 inference(scs_inference,[],[7627,7667,7661,7552,7633,7621,3909,121,3,26,31,40,33,32,29,36,7525,28,35,37,45,43])).
% 129.05/129.04 cnf(7712,plain,
% 129.05/129.04 (~P2(f3(a16,a16),a8,f3(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[7627,7667,7661,7552,7633,7621,7554,7604,3909,121,3,26,31,40,33,32,29,36,7525,28,35,37,45,43,3959,44])).
% 129.05/129.04 cnf(7716,plain,
% 129.05/129.04 (P2(a1,f6(a15),f6(a15))),
% 129.05/129.04 inference(scs_inference,[],[7576,31])).
% 129.05/129.04 cnf(7718,plain,
% 129.05/129.04 (P1(f6(a11))),
% 129.05/129.04 inference(scs_inference,[],[7576,7,31,26])).
% 129.05/129.04 cnf(7720,plain,
% 129.05/129.04 (P2(f6(a11),a11,a1)),
% 129.05/129.04 inference(scs_inference,[],[7576,7,31,26,33])).
% 129.05/129.04 cnf(7728,plain,
% 129.05/129.04 (~P2(a11,a8,a11)),
% 129.05/129.04 inference(scs_inference,[],[7657,7576,7,31,26,33,40,32,36,7525])).
% 129.05/129.04 cnf(7730,plain,
% 129.05/129.04 (P1(f3(a11,a11))),
% 129.05/129.04 inference(scs_inference,[],[7657,7576,7,31,26,33,40,32,36,7525,28])).
% 129.05/129.04 cnf(7732,plain,
% 129.05/129.04 (P1(f14(a11,a11))),
% 129.05/129.04 inference(scs_inference,[],[7657,7576,7,31,26,33,40,32,36,7525,28,29])).
% 129.05/129.04 cnf(7734,plain,
% 129.05/129.04 (P2(a11,a11,f3(a11,a11))),
% 129.05/129.04 inference(scs_inference,[],[7657,7576,7,31,26,33,40,32,36,7525,28,29,35])).
% 129.05/129.04 cnf(7736,plain,
% 129.05/129.04 (P2(a1,a4,a4)),
% 129.05/129.04 inference(scs_inference,[],[7657,7576,7,60,31,26,33,40,32,36,7525,28,29,35,37])).
% 129.05/129.04 cnf(7740,plain,
% 129.05/129.04 (P2(a1,a1,a1)),
% 129.05/129.04 inference(scs_inference,[],[7657,7576,7578,7544,3774,7,60,31,26,33,40,32,36,7525,28,29,35,37,46,43])).
% 129.05/129.04 cnf(7742,plain,
% 129.05/129.04 (P3(f3(a2,a2),f13(a5),f3(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[7657,7576,7702,7578,7558,7544,3774,7,60,20,31,26,33,40,32,36,7525,28,29,35,37,46,43,48])).
% 129.05/129.04 cnf(7753,plain,
% 129.05/129.04 (P1(f6(a10))),
% 129.05/129.04 inference(scs_inference,[],[10,26])).
% 129.05/129.04 cnf(7757,plain,
% 129.05/129.04 (~P2(a8,a2,a2)),
% 129.05/129.04 inference(scs_inference,[],[7698,7732,10,26,31,40])).
% 129.05/129.04 cnf(7759,plain,
% 129.05/129.04 (P2(f6(a10),a10,a1)),
% 129.05/129.04 inference(scs_inference,[],[7698,7732,10,26,31,40,33])).
% 129.05/129.04 cnf(7763,plain,
% 129.05/129.04 (~P2(a10,a8,a10)),
% 129.05/129.04 inference(scs_inference,[],[7698,7732,10,26,31,40,33,32,7525])).
% 129.05/129.04 cnf(7765,plain,
% 129.05/129.04 (P1(f3(a10,a10))),
% 129.05/129.04 inference(scs_inference,[],[7698,7732,10,26,31,40,33,32,7525,28])).
% 129.05/129.04 cnf(7767,plain,
% 129.05/129.04 (P3(a10,a10,f14(a10,a10))),
% 129.05/129.04 inference(scs_inference,[],[7698,7732,10,26,31,40,33,32,7525,28,36])).
% 129.05/129.04 cnf(7769,plain,
% 129.05/129.04 (P1(f14(a10,a10))),
% 129.05/129.04 inference(scs_inference,[],[7698,7732,10,26,31,40,33,32,7525,28,36,29])).
% 129.05/129.04 cnf(7771,plain,
% 129.05/129.04 (P2(a10,a10,f3(a10,a10))),
% 129.05/129.04 inference(scs_inference,[],[7698,7732,10,26,31,40,33,32,7525,28,36,29,35])).
% 129.05/129.04 cnf(7773,plain,
% 129.05/129.04 (P2(a1,a8,a8)),
% 129.05/129.04 inference(scs_inference,[],[7698,7732,10,88,26,31,40,33,32,7525,28,36,29,35,37])).
% 129.05/129.04 cnf(7783,plain,
% 129.05/129.04 (P3(f3(a10,a10),a4,f3(a10,a10))),
% 129.05/129.04 inference(scs_inference,[],[7698,7688,7732,7686,7708,7734,836,10,53,88,796,26,31,40,33,32,7525,28,36,29,35,37,44,42,43,38,48])).
% 129.05/129.04 cnf(7787,plain,
% 129.05/129.04 (P2(a1,f14(a10,a10),f14(a10,a10))),
% 129.05/129.04 inference(scs_inference,[],[7769,31])).
% 129.05/129.04 cnf(7789,plain,
% 129.05/129.04 (P1(f6(a12))),
% 129.05/129.04 inference(scs_inference,[],[7769,11,31,26])).
% 129.05/129.04 cnf(7791,plain,
% 129.05/129.04 (P2(f6(a12),a12,a1)),
% 129.05/129.04 inference(scs_inference,[],[7769,11,31,26,33])).
% 129.05/129.04 cnf(7795,plain,
% 129.05/129.04 (P3(a4,f14(a10,a10),f14(a10,a10))),
% 129.05/129.04 inference(scs_inference,[],[7763,7769,11,31,26,33,40,32])).
% 129.05/129.04 cnf(7797,plain,
% 129.05/129.04 (P1(f3(a12,a12))),
% 129.05/129.04 inference(scs_inference,[],[7763,7769,11,31,26,33,40,32,28])).
% 129.05/129.04 cnf(7799,plain,
% 129.05/129.04 (P3(a12,a12,f14(a12,a12))),
% 129.05/129.04 inference(scs_inference,[],[7763,7769,11,31,26,33,40,32,28,36])).
% 129.05/129.04 cnf(7801,plain,
% 129.05/129.04 (~P2(a12,a8,a12)),
% 129.05/129.04 inference(scs_inference,[],[7763,7769,11,31,26,33,40,32,28,36,7525])).
% 129.05/129.04 cnf(7803,plain,
% 129.05/129.04 (P1(f14(a12,a12))),
% 129.05/129.04 inference(scs_inference,[],[7763,7769,11,31,26,33,40,32,28,36,7525,29])).
% 129.05/129.04 cnf(7805,plain,
% 129.05/129.04 (P2(a12,a12,f3(a12,a12))),
% 129.05/129.04 inference(scs_inference,[],[7763,7769,11,31,26,33,40,32,28,36,7525,29,35])).
% 129.05/129.04 cnf(7807,plain,
% 129.05/129.04 (P2(a1,a5,a5)),
% 129.05/129.04 inference(scs_inference,[],[7763,7769,11,74,31,26,33,40,32,28,36,7525,29,35,37])).
% 129.05/129.04 cnf(7809,plain,
% 129.05/129.04 (~P2(a2,a5,a2)),
% 129.05/129.04 inference(scs_inference,[],[7763,7769,7690,11,23,74,31,26,33,40,32,28,36,7525,29,35,37,44])).
% 129.05/129.04 cnf(7811,plain,
% 129.05/129.04 (~P2(a8,f6(a18),f6(a18))),
% 129.05/129.04 inference(scs_inference,[],[7763,7769,7651,7690,58,11,23,74,31,26,33,40,32,28,36,7525,29,35,37,44,43])).
% 129.05/129.04 cnf(7820,plain,
% 129.05/129.04 (P1(f6(a4))),
% 129.05/129.04 inference(scs_inference,[],[2,26])).
% 129.05/129.04 cnf(7822,plain,
% 129.05/129.04 (P2(a1,f14(a12,a12),f14(a12,a12))),
% 129.05/129.04 inference(scs_inference,[],[7803,2,26,31])).
% 129.05/129.04 cnf(7826,plain,
% 129.05/129.04 (P2(f6(a4),a4,a1)),
% 129.05/129.04 inference(scs_inference,[],[7671,7803,2,26,31,40,33])).
% 129.05/129.04 cnf(7830,plain,
% 129.05/129.04 (P3(a4,a4,f14(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7671,7803,2,26,31,40,33,32,36])).
% 129.05/129.04 cnf(7832,plain,
% 129.05/129.04 (P1(f14(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7671,7803,2,26,31,40,33,32,36,29])).
% 129.05/129.04 cnf(7834,plain,
% 129.05/129.04 (P1(f3(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7671,7803,2,26,31,40,33,32,36,29,28])).
% 129.05/129.04 cnf(7836,plain,
% 129.05/129.04 (P2(a4,a4,f3(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7671,7803,2,26,31,40,33,32,36,29,28,35])).
% 129.05/129.04 cnf(7838,plain,
% 129.05/129.04 (P2(a1,a7,a7)),
% 129.05/129.04 inference(scs_inference,[],[7671,7803,2,81,26,31,40,33,32,36,29,28,35,37])).
% 129.05/129.04 cnf(7840,plain,
% 129.05/129.04 (~P2(f3(a15,a15),a8,f3(a15,a15))),
% 129.05/129.04 inference(scs_inference,[],[7671,7803,7590,7639,2,81,26,31,40,33,32,36,29,28,35,37,44])).
% 129.05/129.04 cnf(7851,plain,
% 129.05/129.04 (P2(a1,f3(a4,a4),f3(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7834,31])).
% 129.05/129.04 cnf(7853,plain,
% 129.05/129.04 (P1(f6(a7))),
% 129.05/129.04 inference(scs_inference,[],[7834,5,31,26])).
% 129.05/129.04 cnf(7855,plain,
% 129.05/129.04 (P2(f6(a7),a7,a1)),
% 129.05/129.04 inference(scs_inference,[],[7834,5,31,26,33])).
% 129.05/129.04 cnf(7859,plain,
% 129.05/129.04 (P3(a4,f3(a4,a4),f3(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7801,7834,5,31,26,33,40,32])).
% 129.05/129.04 cnf(7861,plain,
% 129.05/129.04 (P1(f14(a7,a7))),
% 129.05/129.04 inference(scs_inference,[],[7801,7834,5,31,26,33,40,32,29])).
% 129.05/129.04 cnf(7863,plain,
% 129.05/129.04 (P1(f3(a7,a7))),
% 129.05/129.04 inference(scs_inference,[],[7801,7834,5,31,26,33,40,32,29,28])).
% 129.05/129.04 cnf(7865,plain,
% 129.05/129.04 (P3(a7,a7,f14(a7,a7))),
% 129.05/129.04 inference(scs_inference,[],[7801,7834,5,31,26,33,40,32,29,28,36])).
% 129.05/129.04 cnf(7867,plain,
% 129.05/129.04 (P2(a7,a7,f3(a7,a7))),
% 129.05/129.04 inference(scs_inference,[],[7801,7834,5,31,26,33,40,32,29,28,36,35])).
% 129.05/129.04 cnf(7869,plain,
% 129.05/129.04 (P2(a1,a18,a18)),
% 129.05/129.04 inference(scs_inference,[],[7801,7834,5,102,31,26,33,40,32,29,28,36,35,37])).
% 129.05/129.04 cnf(7873,plain,
% 129.05/129.04 (P2(a1,f3(a18,a18),f3(a18,a18))),
% 129.05/129.04 inference(scs_inference,[],[7801,7795,7665,7834,7830,5,102,31,26,33,40,32,29,28,36,35,37,46,43])).
% 129.05/129.04 cnf(7875,plain,
% 129.05/129.04 (P3(f3(a4,a4),a4,f3(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7801,7795,7665,7834,7836,7830,7706,5,102,31,26,33,40,32,29,28,36,35,37,46,43,48])).
% 129.05/129.04 cnf(7887,plain,
% 129.05/129.04 (P1(f6(a9))),
% 129.05/129.04 inference(scs_inference,[],[9,26])).
% 129.05/129.04 cnf(7889,plain,
% 129.05/129.04 (P2(a1,f14(a4,a4),f14(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7832,9,26,31])).
% 129.05/129.04 cnf(7893,plain,
% 129.05/129.04 (P2(f6(a9),a9,a1)),
% 129.05/129.04 inference(scs_inference,[],[7809,7832,9,26,31,40,33])).
% 129.05/129.04 cnf(7895,plain,
% 129.05/129.04 (P3(a4,f14(a4,a4),f14(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7809,7832,9,26,31,40,33,32])).
% 129.05/129.04 cnf(7897,plain,
% 129.05/129.04 (P1(f3(a9,a9))),
% 129.05/129.04 inference(scs_inference,[],[7809,7832,9,26,31,40,33,32,28])).
% 129.05/129.04 cnf(7899,plain,
% 129.05/129.04 (P3(a9,a9,f14(a9,a9))),
% 129.05/129.04 inference(scs_inference,[],[7809,7832,9,26,31,40,33,32,28,36])).
% 129.05/129.04 cnf(7901,plain,
% 129.05/129.04 (P2(a9,a9,f3(a9,a9))),
% 129.05/129.04 inference(scs_inference,[],[7809,7832,9,26,31,40,33,32,28,36,35])).
% 129.05/129.04 cnf(7903,plain,
% 129.05/129.04 (P1(f14(a9,a9))),
% 129.05/129.04 inference(scs_inference,[],[7809,7832,9,26,31,40,33,32,28,36,35,29])).
% 129.05/129.04 cnf(7905,plain,
% 129.05/129.04 (P2(a1,a10,a10)),
% 129.05/129.04 inference(scs_inference,[],[7809,7832,9,112,26,31,40,33,32,28,36,35,29,37])).
% 129.05/129.04 cnf(7907,plain,
% 129.05/129.04 (P3(f3(a4,a4),f14(a4,a4),f3(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7809,7832,7875,7830,9,112,26,31,40,33,32,28,36,35,29,37,45])).
% 129.05/129.04 cnf(7909,plain,
% 129.05/129.04 (P2(a1,f3(a12,a12),f3(a12,a12))),
% 129.05/129.04 inference(scs_inference,[],[7809,7805,7832,7875,7704,7830,9,112,26,31,40,33,32,28,36,35,29,37,45,43])).
% 129.05/129.04 cnf(7917,plain,
% 129.05/129.04 (P2(a1,f14(a9,a9),f14(a9,a9))),
% 129.05/129.04 inference(scs_inference,[],[7903,31])).
% 129.05/129.04 cnf(7919,plain,
% 129.05/129.04 (P1(f6(a5))),
% 129.05/129.04 inference(scs_inference,[],[7903,4,31,26])).
% 129.05/129.04 cnf(7921,plain,
% 129.05/129.04 (P2(f6(a5),a5,a1)),
% 129.05/129.04 inference(scs_inference,[],[7903,4,31,26,33])).
% 129.05/129.04 cnf(7923,plain,
% 129.05/129.04 (~P2(a5,f3(a16,a16),f3(a16,a16))),
% 129.05/129.04 inference(scs_inference,[],[7637,7903,4,31,26,33,40])).
% 129.05/129.04 cnf(7927,plain,
% 129.05/129.04 (P3(a5,a5,f14(a5,a5))),
% 129.05/129.04 inference(scs_inference,[],[7637,7903,4,31,26,33,40,32,36])).
% 129.05/129.04 cnf(7929,plain,
% 129.05/129.04 (P2(a5,a5,f3(a5,a5))),
% 129.05/129.04 inference(scs_inference,[],[7637,7903,4,31,26,33,40,32,36,35])).
% 129.05/129.04 cnf(7931,plain,
% 129.05/129.04 (P1(f3(a5,a5))),
% 129.05/129.04 inference(scs_inference,[],[7637,7903,4,31,26,33,40,32,36,35,28])).
% 129.05/129.04 cnf(7933,plain,
% 129.05/129.04 (P1(f14(a5,a5))),
% 129.05/129.04 inference(scs_inference,[],[7637,7903,4,31,26,33,40,32,36,35,28,29])).
% 129.05/129.04 cnf(7935,plain,
% 129.05/129.04 (P2(a1,a2,a2)),
% 129.05/129.04 inference(scs_inference,[],[7637,7903,4,67,31,26,33,40,32,36,35,28,29,37])).
% 129.05/129.04 cnf(7937,plain,
% 129.05/129.04 (~P2(a16,f6(a16),a5)),
% 129.05/129.04 inference(scs_inference,[],[7637,7903,7558,7604,4,67,31,26,33,40,32,36,35,28,29,37,44])).
% 129.05/129.04 cnf(7939,plain,
% 129.05/129.04 (P2(a1,f3(a5,a5),f3(a5,a5))),
% 129.05/129.04 inference(scs_inference,[],[7807,7637,7903,7558,7604,4,67,31,26,33,40,32,36,35,28,29,37,44,43])).
% 129.05/129.04 cnf(7946,plain,
% 129.05/129.04 (P1(f6(a1))),
% 129.05/129.04 inference(scs_inference,[],[1,26])).
% 129.05/129.04 cnf(7948,plain,
% 129.05/129.04 (~P2(a8,f3(a15,a15),f3(a15,a15))),
% 129.05/129.04 inference(scs_inference,[],[7840,1,26,40])).
% 129.05/129.04 cnf(7952,plain,
% 129.05/129.04 (P2(f6(a1),a1,a1)),
% 129.05/129.04 inference(scs_inference,[],[7933,7840,1,26,40,31,33])).
% 129.05/129.04 cnf(7954,plain,
% 129.05/129.04 (P3(a4,f3(a5,a5),f3(a5,a5))),
% 129.05/129.04 inference(scs_inference,[],[7931,7933,7840,1,26,40,31,33,32])).
% 129.05/129.04 cnf(7956,plain,
% 129.05/129.04 (~P2(a5,a8,a5)),
% 129.05/129.04 inference(scs_inference,[],[7931,7933,7840,7921,1,26,40,31,33,32,7525])).
% 129.05/129.04 cnf(7958,plain,
% 129.05/129.04 (P2(a1,a1,f3(a1,a1))),
% 129.05/129.04 inference(scs_inference,[],[7931,7933,7840,7921,1,26,40,31,33,32,7525,35])).
% 129.05/129.04 cnf(7960,plain,
% 129.05/129.04 (P1(f3(a1,a1))),
% 129.05/129.04 inference(scs_inference,[],[7931,7933,7840,7921,1,26,40,31,33,32,7525,35,28])).
% 129.05/129.04 cnf(7962,plain,
% 129.05/129.04 (P1(f14(a1,a1))),
% 129.05/129.04 inference(scs_inference,[],[7931,7933,7840,7921,1,26,40,31,33,32,7525,35,28,29])).
% 129.05/129.04 cnf(7964,plain,
% 129.05/129.04 (P3(a1,a1,f14(a1,a1))),
% 129.05/129.04 inference(scs_inference,[],[7931,7933,7840,7921,1,26,40,31,33,32,7525,35,28,29,36])).
% 129.05/129.04 cnf(7966,plain,
% 129.05/129.04 (~P2(a10,a5,a10)),
% 129.05/129.04 inference(scs_inference,[],[7759,7931,7933,7840,7921,1,23,26,40,31,33,32,7525,35,28,29,36,44])).
% 129.05/129.04 cnf(7968,plain,
% 129.05/129.04 (P4(f3(a7,a7),f3(a7,a7))),
% 129.05/129.04 inference(scs_inference,[],[7759,7867,7931,7933,7840,7921,1,23,81,26,40,31,33,32,7525,35,28,29,36,44,42])).
% 129.05/129.04 cnf(7970,plain,
% 129.05/129.04 (~P2(a8,f6(a10),f6(a10))),
% 129.05/129.04 inference(scs_inference,[],[7759,7867,7931,7933,7840,7921,58,1,23,81,26,40,31,33,32,7525,35,28,29,36,44,42,43])).
% 129.05/129.04 cnf(7972,plain,
% 129.05/129.04 (P2(f14(a1,a1),f14(a1,a1),f14(a1,a1))),
% 129.05/129.04 inference(scs_inference,[],[7740,7759,7867,7931,7933,7840,7921,58,1,23,81,26,40,31,33,32,7525,35,28,29,36,44,42,43,47])).
% 129.05/129.04 cnf(7976,plain,
% 129.05/129.04 (P3(f3(a9,a9),a4,f3(a9,a9))),
% 129.05/129.04 inference(scs_inference,[],[7740,7759,7867,7931,7933,7840,7901,7921,58,1,23,81,911,3813,26,40,31,33,32,7525,35,28,29,36,44,42,43,47,37,48])).
% 129.05/129.04 cnf(7982,plain,
% 129.05/129.04 (P2(f6(a8),a8,a1)),
% 129.05/129.04 inference(scs_inference,[],[7966,6,40,33])).
% 129.05/129.04 cnf(7984,plain,
% 129.05/129.04 (P1(f6(a8))),
% 129.05/129.04 inference(scs_inference,[],[7966,6,40,33,26])).
% 129.05/129.04 cnf(7986,plain,
% 129.05/129.04 (P2(a1,f3(a1,a1),f3(a1,a1))),
% 129.05/129.04 inference(scs_inference,[],[7966,7960,6,40,33,26,31])).
% 129.05/129.04 cnf(7988,plain,
% 129.05/129.04 (P3(a4,f3(a1,a1),f3(a1,a1))),
% 129.05/129.04 inference(scs_inference,[],[7966,7960,6,40,33,26,31,32])).
% 129.05/129.04 cnf(7990,plain,
% 129.05/129.04 (~P2(f6(a1),a8,a1)),
% 129.05/129.04 inference(scs_inference,[],[7966,7960,7952,7773,6,40,33,26,31,32,7525])).
% 129.05/129.04 cnf(7992,plain,
% 129.05/129.04 (P1(f3(a8,a8))),
% 129.05/129.04 inference(scs_inference,[],[7966,7960,7952,7773,6,40,33,26,31,32,7525,28])).
% 129.05/129.04 cnf(7994,plain,
% 129.05/129.04 (P2(a8,a8,f3(a8,a8))),
% 129.05/129.04 inference(scs_inference,[],[7966,7960,7952,7773,6,40,33,26,31,32,7525,28,35])).
% 129.05/129.04 cnf(7996,plain,
% 129.05/129.04 (P3(a8,a8,f14(a8,a8))),
% 129.05/129.04 inference(scs_inference,[],[7966,7960,7952,7773,6,40,33,26,31,32,7525,28,35,36])).
% 129.05/129.04 cnf(7998,plain,
% 129.05/129.04 (P1(f14(a8,a8))),
% 129.05/129.04 inference(scs_inference,[],[7966,7960,7952,7773,6,40,33,26,31,32,7525,28,35,36,29])).
% 129.05/129.04 cnf(8000,plain,
% 129.05/129.04 (P2(a1,f3(a7,a7),f3(a7,a7))),
% 129.05/129.04 inference(scs_inference,[],[7966,7968,7960,7952,7773,6,40,33,26,31,32,7525,28,35,36,29,37])).
% 129.05/129.04 cnf(8002,plain,
% 129.05/129.04 (P2(f6(a15),a15,f3(a1,a1))),
% 129.05/129.04 inference(scs_inference,[],[7966,7968,7960,7716,7952,7958,7580,7773,6,40,33,26,31,32,7525,28,35,36,29,37,44])).
% 129.05/129.04 cnf(8006,plain,
% 129.05/129.04 (~P2(a8,f6(a12),f6(a12))),
% 129.05/129.04 inference(scs_inference,[],[7966,7968,7791,7939,7960,7716,7952,7958,7580,7773,58,53,6,40,33,26,31,32,7525,28,35,36,29,37,44,42,43])).
% 129.05/129.04 cnf(8021,plain,
% 129.05/129.04 (P2(a1,f14(a1,a1),f14(a1,a1))),
% 129.05/129.04 inference(scs_inference,[],[7962,31])).
% 129.05/129.04 cnf(8027,plain,
% 129.05/129.04 (~P2(f6(a8),f3(a8,a8),a1)),
% 129.05/129.04 inference(scs_inference,[],[7956,7962,7994,7982,31,40,32,7525])).
% 129.05/129.04 cnf(8029,plain,
% 129.05/129.04 (P3(f14(a4,a4),a4,f14(a4,a4))),
% 129.05/129.04 inference(scs_inference,[],[7956,7895,7962,7994,7982,7830,31,40,32,7525,46])).
% 129.05/129.04 cnf(8033,plain,
% 129.05/129.04 (P2(a1,f3(a10,a10),f3(a10,a10))),
% 129.05/129.04 inference(scs_inference,[],[7905,7956,7895,7962,7994,7982,7771,7952,7830,58,31,40,32,7525,46,44,43])).
% 129.05/129.04 cnf(8035,plain,
% 129.05/129.04 (~P3(a1,a4,a5)),
% 129.05/129.04 inference(scs_inference,[],[7905,7956,7895,7962,7923,7994,7982,7596,7570,7771,7952,7830,58,31,40,32,7525,46,44,43,47])).
% 129.05/129.04 cnf(8037,plain,
% 129.05/129.05 (~P3(a4,a1,a5)),
% 129.05/129.05 inference(scs_inference,[],[7905,7956,7895,7962,7923,7994,7982,7596,7570,7771,7952,7830,58,31,40,32,7525,46,44,43,47,41])).
% 129.05/129.05 cnf(8043,plain,
% 129.05/129.05 (~P2(a8,f3(a16,a16),f3(a16,a16))),
% 129.05/129.05 inference(scs_inference,[],[7712,40])).
% 129.05/129.05 cnf(8045,plain,
% 129.05/129.05 (P2(a1,f14(a8,a8),f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[7998,7712,40,31])).
% 129.05/129.05 cnf(8047,plain,
% 129.05/129.05 (P3(a4,f14(a8,a8),f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[7998,7712,40,31,32])).
% 129.05/129.05 cnf(8049,plain,
% 129.05/129.05 (~P2(a9,a8,a9)),
% 129.05/129.05 inference(scs_inference,[],[7998,7712,7893,40,31,32,7525])).
% 129.05/129.05 cnf(8051,plain,
% 129.05/129.05 (~P2(a7,a5,a7)),
% 129.05/129.05 inference(scs_inference,[],[7998,7712,7893,7855,23,40,31,32,7525,44])).
% 129.05/129.05 cnf(8053,plain,
% 129.05/129.05 (~P2(a8,f6(a9),f6(a9))),
% 129.05/129.05 inference(scs_inference,[],[7998,7712,7893,7855,58,23,40,31,32,7525,44,43])).
% 129.05/129.05 cnf(8060,plain,
% 129.05/129.05 (P2(a1,f13(a8),f13(a8))),
% 129.05/129.05 inference(scs_inference,[],[7586,31])).
% 129.05/129.05 cnf(8062,plain,
% 129.05/129.05 (~P2(a8,a9,a9)),
% 129.05/129.05 inference(scs_inference,[],[8049,7586,31,40])).
% 129.05/129.05 cnf(8064,plain,
% 129.05/129.05 (P3(a4,f13(a8),f13(a8))),
% 129.05/129.05 inference(scs_inference,[],[8049,7586,31,40,32])).
% 129.05/129.05 cnf(8066,plain,
% 129.05/129.05 (~P2(a7,a8,a7)),
% 129.05/129.05 inference(scs_inference,[],[8049,7586,7855,31,40,32,7525])).
% 129.05/129.05 cnf(8068,plain,
% 129.05/129.05 (P3(a4,a17,a17)),
% 129.05/129.05 inference(scs_inference,[],[8049,7586,7855,3755,31,40,32,7525,45])).
% 129.05/129.05 cnf(8070,plain,
% 129.05/129.05 (P2(f3(a1,a1),a15,a15)),
% 129.05/129.05 inference(scs_inference,[],[8049,7586,8002,7598,7855,3755,7639,31,40,32,7525,45,44])).
% 129.05/129.05 cnf(8072,plain,
% 129.05/129.05 (P2(f6(a18),f3(a18,a18),a18)),
% 129.05/129.05 inference(scs_inference,[],[7869,8049,7586,8002,7651,7665,7598,7855,3755,7639,31,40,32,7525,45,44,43])).
% 129.05/129.05 cnf(8083,plain,
% 129.05/129.05 (~P2(a5,a7,a7)),
% 129.05/129.05 inference(scs_inference,[],[8051,40])).
% 129.05/129.05 cnf(8089,plain,
% 129.05/129.05 (~P2(a1,f6(a8),a1)),
% 129.05/129.05 inference(scs_inference,[],[8051,7588,7592,7982,7740,40,31,32,7525])).
% 129.05/129.05 cnf(8093,plain,
% 129.05/129.05 (P2(a1,f3(a2,a2),f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[7935,7653,8051,7588,7592,8070,7982,7702,7740,40,31,32,7525,44,43])).
% 129.05/129.05 cnf(8101,plain,
% 129.05/129.05 (~P2(a8,a7,a7)),
% 129.05/129.05 inference(scs_inference,[],[8066,7615,31,40])).
% 129.05/129.05 cnf(8105,plain,
% 129.05/129.05 (~P2(a8,a8,a8)),
% 129.05/129.05 inference(scs_inference,[],[8066,7615,7982,31,40,32,7525])).
% 129.05/129.05 cnf(8107,plain,
% 129.05/129.05 (~P2(f3(a18,a18),a8,f3(a18,a18))),
% 129.05/129.05 inference(scs_inference,[],[8066,7615,8072,7657,7982,31,40,32,7525,44])).
% 129.05/129.05 cnf(8109,plain,
% 129.05/129.05 (P2(f6(a1),a7,a7)),
% 129.05/129.05 inference(scs_inference,[],[7838,8066,7615,8072,7657,7952,7982,31,40,32,7525,44,43])).
% 129.05/129.05 cnf(8126,plain,
% 129.05/129.05 (~P2(a4,a8,a4)),
% 129.05/129.05 inference(scs_inference,[],[8027,7625,7649,7826,40,31,32,7525])).
% 129.05/129.05 cnf(8130,plain,
% 129.05/129.05 (~P2(f3(a18,a18),a5,f3(a18,a18))),
% 129.05/129.05 inference(scs_inference,[],[7873,8027,7625,7649,7671,8072,7826,53,40,31,32,7525,42,44])).
% 129.05/129.05 cnf(8140,plain,
% 129.05/129.05 (P3(f14(a12,a12),a4,f14(a12,a12))),
% 129.05/129.05 inference(scs_inference,[],[8083,7873,7742,8027,8093,8043,7625,7649,8109,7799,7671,8072,7826,7836,53,888,40,31,32,7525,42,44,43,47,41,5425,46])).
% 129.05/129.05 cnf(8142,plain,
% 129.05/129.05 (P3(f3(a8,a8),a5,f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[8083,7873,7742,8027,8093,8043,7625,7649,8109,7799,7671,7994,8072,3769,7826,7771,7836,53,888,40,31,32,7525,42,44,43,47,41,5425,46,48])).
% 129.05/129.05 cnf(8148,plain,
% 129.05/129.05 (P2(a1,f6(a2),f6(a2))),
% 129.05/129.05 inference(scs_inference,[],[8126,7684,40,31])).
% 129.05/129.05 cnf(8152,plain,
% 129.05/129.05 (~P2(f6(a8),a1,a1)),
% 129.05/129.05 inference(scs_inference,[],[8126,7663,7684,7773,7982,40,31,32,7525])).
% 129.05/129.05 cnf(8154,plain,
% 129.05/129.05 (P3(f13(a8),a8,f14(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[8126,7663,7684,8064,3896,7773,7982,7830,40,31,32,7525,46])).
% 129.05/129.05 cnf(8160,plain,
% 129.05/129.05 (P2(f6(a2),f3(a2,a2),a2)),
% 129.05/129.05 inference(scs_inference,[],[8126,7851,7986,7663,7684,8064,7935,7690,3896,7958,7773,7982,7702,7830,53,40,31,32,7525,46,42,44,43])).
% 129.05/129.05 cnf(8171,plain,
% 129.05/129.05 (~P2(f3(a2,a2),a8,f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[8107,7694,8160,7698,31,40,32,44])).
% 129.05/129.05 cnf(8173,plain,
% 129.05/129.05 (~P2(f6(a8),f6(a11),f6(a11))),
% 129.05/129.05 inference(scs_inference,[],[8107,7694,8160,8152,7698,7720,31,40,32,44,43])).
% 129.05/129.05 cnf(8183,plain,
% 129.05/129.05 (P3(a4,f3(a2,a2),f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[7990,7700,7718,40,31,32])).
% 129.05/129.05 cnf(8185,plain,
% 129.05/129.05 (~P2(f3(a17,a17),a8,f3(a17,a17))),
% 129.05/129.05 inference(scs_inference,[],[7990,7700,7718,7627,7708,40,31,32,44])).
% 129.05/129.05 cnf(8187,plain,
% 129.05/129.05 (~P2(f6(a8),f6(a12),f6(a12))),
% 129.05/129.05 inference(scs_inference,[],[7990,7700,7718,7627,7791,7708,8152,40,31,32,44,43])).
% 129.05/129.05 cnf(8191,plain,
% 129.05/129.05 (~P3(x81911,a7,a7)+P3(x81911,f14(a7,a7),f14(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[7865,7990,7700,7718,7627,7791,7708,8152,13,40,31,32,44,43,34,45])).
% 129.05/129.05 cnf(8193,plain,
% 129.05/129.05 (P2(a1,f3(a11,a11),f3(a11,a11))),
% 129.05/129.05 inference(scs_inference,[],[7730,31])).
% 129.05/129.05 cnf(8201,plain,
% 129.05/129.05 (P2(f6(a1),f3(a7,a7),f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[8130,7730,7867,7986,8109,7958,31,40,32,44,43])).
% 129.05/129.05 cnf(8208,plain,
% 129.05/129.05 (~P2(a8,f3(a2,a2),f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[8171,40])).
% 129.05/129.05 cnf(8210,plain,
% 129.05/129.05 (P2(a1,f6(a10),f6(a10))),
% 129.05/129.05 inference(scs_inference,[],[8171,7753,40,31])).
% 129.05/129.05 cnf(8212,plain,
% 129.05/129.05 (P3(a4,f6(a10),f6(a10))),
% 129.05/129.05 inference(scs_inference,[],[8171,7753,40,31,32])).
% 129.05/129.05 cnf(8214,plain,
% 129.05/129.05 (~P2(f3(a2,a2),a5,f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[8171,7753,7809,8160,40,31,32,44])).
% 129.05/129.05 cnf(8216,plain,
% 129.05/129.05 (P2(a1,f3(a9,a9),f3(a9,a9))),
% 129.05/129.05 inference(scs_inference,[],[8171,7753,7809,8160,7901,3799,40,31,32,44,43])).
% 129.05/129.05 cnf(8220,plain,
% 129.05/129.05 (P3(f3(a1,a1),a1,f14(a1,a1))),
% 129.05/129.05 inference(scs_inference,[],[8171,8142,7753,7809,8160,7972,7901,7964,7958,3799,40,31,32,44,43,45,48])).
% 129.05/129.05 cnf(8225,plain,
% 129.05/129.05 (P2(a1,f6(a12),f6(a12))),
% 129.05/129.05 inference(scs_inference,[],[7789,31])).
% 129.05/129.05 cnf(8227,plain,
% 129.05/129.05 (~P2(a8,f3(a17,a17),f3(a17,a17))),
% 129.05/129.05 inference(scs_inference,[],[8185,7789,31,40])).
% 129.05/129.05 cnf(8229,plain,
% 129.05/129.05 (P3(a4,f3(a10,a10),f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[8185,7765,7789,31,40,32])).
% 129.05/129.05 cnf(8231,plain,
% 129.05/129.05 (~P2(f6(a5),f3(a5,a5),a1)),
% 129.05/129.05 inference(scs_inference,[],[8185,7765,7789,7929,7921,23,31,40,32,44])).
% 129.05/129.05 cnf(8233,plain,
% 129.05/129.05 (P2(a1,f3(a8,a8),f3(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[8185,7765,7789,7929,7994,7921,7773,23,31,40,32,44,43])).
% 129.05/129.05 cnf(8235,plain,
% 129.05/129.05 (P3(f3(a4,a4),a17,f3(a17,a17))),
% 129.05/129.05 inference(scs_inference,[],[8185,7765,7789,8068,7929,7994,7921,7633,7773,7836,23,31,40,32,44,43,48])).
% 129.05/129.05 cnf(8243,plain,
% 129.05/129.05 (P2(a1,f6(a4),f6(a4))),
% 129.05/129.05 inference(scs_inference,[],[8214,7820,40,31])).
% 129.05/129.05 cnf(8251,plain,
% 129.05/129.05 (~P2(a16,f6(a16),a8)),
% 129.05/129.05 inference(scs_inference,[],[7909,8214,7797,7820,7899,8043,7558,7604,53,911,40,31,32,46,42,44])).
% 129.05/129.05 cnf(8253,plain,
% 129.05/129.05 (P2(f6(a10),f3(a10,a10),a10)),
% 129.05/129.05 inference(scs_inference,[],[7909,8214,7797,7820,7899,7905,8043,7759,7558,7604,7771,53,911,40,31,32,46,42,44,43])).
% 129.05/129.05 cnf(8266,plain,
% 129.05/129.05 (P3(a4,f6(a7),f6(a7))),
% 129.05/129.05 inference(scs_inference,[],[7853,7861,8173,31,40,32])).
% 129.05/129.05 cnf(8270,plain,
% 129.05/129.05 (~P2(f3(a10,a10),a8,f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[8193,7853,7861,8173,8253,7763,53,31,40,32,42,44])).
% 129.05/129.05 cnf(8272,plain,
% 129.05/129.05 (~P2(a8,f6(a1),f6(a1))),
% 129.05/129.05 inference(scs_inference,[],[8101,8193,7853,7861,8173,8253,7763,8109,53,31,40,32,42,44,43])).
% 129.05/129.05 cnf(8274,plain,
% 129.05/129.05 (P3(f3(a8,a8),a2,f3(a12,a12))),
% 129.05/129.05 inference(scs_inference,[],[8101,8193,7853,7861,8173,8253,7763,7805,3748,8109,7994,53,31,40,32,42,44,43,48])).
% 129.05/129.05 cnf(8282,plain,
% 129.05/129.05 (P2(a1,f6(a9),f6(a9))),
% 129.05/129.05 inference(scs_inference,[],[7811,7887,40,31])).
% 129.05/129.05 cnf(8284,plain,
% 129.05/129.05 (P3(a4,f3(a7,a7),f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[7811,7863,7887,40,31,32])).
% 129.05/129.05 cnf(8286,plain,
% 129.05/129.05 (~P2(f3(a10,a10),a5,f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[7811,7863,7887,7966,8253,40,31,32,44])).
% 129.05/129.05 cnf(8288,plain,
% 129.05/129.05 (~P2(f6(a8),f6(a18),f6(a18))),
% 129.05/129.05 inference(scs_inference,[],[7811,7863,7887,7966,8253,8152,7651,40,31,32,44,43])).
% 129.05/129.05 cnf(8296,plain,
% 129.05/129.05 (P2(a1,f6(a5),f6(a5))),
% 129.05/129.05 inference(scs_inference,[],[7919,31])).
% 129.05/129.05 cnf(8298,plain,
% 129.05/129.05 (~P2(a8,f3(a10,a10),f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[8270,7919,31,40])).
% 129.05/129.05 cnf(8302,plain,
% 129.05/129.05 (~P2(f6(a1),f6(a1),a5)),
% 129.05/129.05 inference(scs_inference,[],[8270,7897,7919,8083,8109,31,40,32,44])).
% 129.05/129.05 cnf(8304,plain,
% 129.05/129.05 (P2(f6(a12),a9,a15)),
% 129.05/129.05 inference(scs_inference,[],[15,8270,7897,7919,8083,7791,7560,8109,31,40,32,44,43])).
% 129.05/129.05 cnf(8308,plain,
% 129.05/129.05 (P2(f14(a4,a4),f14(a4,a4),f3(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[15,8270,7897,7919,7907,8083,7895,7791,7560,8109,7836,31,40,32,44,43,5185,47])).
% 129.05/129.05 cnf(8314,plain,
% 129.05/129.05 (P2(a1,f6(a1),f6(a1))),
% 129.05/129.05 inference(scs_inference,[],[8286,7946,40,31])).
% 129.05/129.05 cnf(8316,plain,
% 129.05/129.05 (P3(a4,f6(a1),f6(a1))),
% 129.05/129.05 inference(scs_inference,[],[8286,7946,40,31,32])).
% 129.05/129.05 cnf(8318,plain,
% 129.05/129.05 (P2(a15,a1,a15)),
% 129.05/129.05 inference(scs_inference,[],[8286,7946,8304,755,40,31,32,44])).
% 129.05/129.05 cnf(8320,plain,
% 129.05/129.05 (P2(f3(a1,a1),f3(a15,a15),f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[8286,7946,8304,8070,7598,755,40,31,32,44,43])).
% 129.05/129.05 cnf(8330,plain,
% 129.05/129.05 (P2(a1,f6(a8),f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[7984,31])).
% 129.05/129.05 cnf(8334,plain,
% 129.05/129.05 (P3(a4,f6(a8),f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[7984,8187,31,40,32])).
% 129.05/129.05 cnf(8336,plain,
% 129.05/129.05 (P2(f6(a17),a11,a16)),
% 129.05/129.05 inference(scs_inference,[],[7984,8187,7621,7540,3794,31,40,32,43])).
% 129.05/129.05 cnf(8348,plain,
% 129.05/129.05 (P2(a1,f13(a5),f13(a5))),
% 129.05/129.05 inference(scs_inference,[],[8231,7552,40,31])).
% 129.05/129.05 cnf(8350,plain,
% 129.05/129.05 (P3(a4,f3(a8,a8),f3(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[8231,7992,7552,40,31,32])).
% 129.05/129.05 cnf(8352,plain,
% 129.05/129.05 (P2(f6(a9),f3(a9,a9),a9)),
% 129.05/129.05 inference(scs_inference,[],[8231,7992,7552,7893,7901,3799,40,31,32,43])).
% 129.05/129.05 cnf(8356,plain,
% 129.05/129.05 (~P2(f3(a9,a9),a8,f3(a9,a9))),
% 129.05/129.05 inference(scs_inference,[],[8231,8284,7992,7552,8049,8037,7893,7901,3799,40,31,32,43,45,44])).
% 129.05/129.05 cnf(8365,plain,
% 129.05/129.05 (P3(a4,f14(a5,a5),f14(a5,a5))),
% 129.05/129.05 inference(scs_inference,[],[8288,7933,7649,31,40,32])).
% 129.05/129.05 cnf(8369,plain,
% 129.05/129.05 (~P2(a12,f6(a12),a8)),
% 129.05/129.05 inference(scs_inference,[],[15,8233,8288,8062,8304,7933,7649,53,31,40,32,42,44])).
% 129.05/129.05 cnf(8371,plain,
% 129.05/129.05 (P2(f3(a1,a1),a9,a9)),
% 129.05/129.05 inference(scs_inference,[],[15,8233,8288,8062,8304,7933,7649,8070,3789,53,31,40,32,42,44,43])).
% 129.05/129.05 cnf(8375,plain,
% 129.05/129.05 (P3(f3(a5,a5),a7,f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[15,8233,8288,8062,8304,7933,7649,7929,8070,7598,18,3789,53,31,40,32,42,44,43,27,48])).
% 129.05/129.05 cnf(8380,plain,
% 129.05/129.05 (~P2(a8,f3(a9,a9),f3(a9,a9))),
% 129.05/129.05 inference(scs_inference,[],[8356,40])).
% 129.05/129.05 cnf(8386,plain,
% 129.05/129.05 (P2(a16,a1,a16)),
% 129.05/129.05 inference(scs_inference,[],[8216,8336,8356,7684,53,796,40,32,42,44])).
% 129.05/129.05 cnf(8388,plain,
% 129.05/129.05 (P2(f6(a15),a9,a12)),
% 129.05/129.05 inference(scs_inference,[],[8216,8336,8356,7684,7704,7580,3789,53,796,40,32,42,44,43])).
% 129.05/129.05 cnf(8397,plain,
% 129.05/129.05 (P3(a4,f6(a11),f6(a11))),
% 129.05/129.05 inference(scs_inference,[],[7566,7718,40,32])).
% 129.05/129.05 cnf(8399,plain,
% 129.05/129.05 (P2(f3(a1,a1),f3(a9,a9),f3(a9,a9))),
% 129.05/129.05 inference(scs_inference,[],[7566,8371,7718,7901,40,32,43])).
% 129.05/129.05 cnf(8418,plain,
% 129.05/129.05 (P2(a12,a1,a12)),
% 129.05/129.05 inference(scs_inference,[],[7970,8388,7820,755,40,32,44])).
% 129.05/129.05 cnf(8426,plain,
% 129.05/129.05 (P3(f3(a7,a7),a5,f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[7970,8302,8388,8316,7550,7820,3762,7867,7598,7836,755,40,32,44,47,41,27,48])).
% 129.05/129.05 cnf(8432,plain,
% 129.05/129.05 (P3(a4,f6(a9),f6(a9))),
% 129.05/129.05 inference(scs_inference,[],[8006,7887,40,32])).
% 129.05/129.05 cnf(8438,plain,
% 129.05/129.05 (~P3(a4,a1,a8)),
% 129.05/129.05 inference(scs_inference,[],[8418,8006,8318,7887,7590,7805,910,40,32,44,47,41])).
% 129.05/129.05 cnf(8447,plain,
% 129.05/129.05 (P3(a4,f6(a5),f6(a5))),
% 129.05/129.05 inference(scs_inference,[],[8053,7919,40,32])).
% 129.05/129.05 cnf(8449,plain,
% 129.05/129.05 (~P2(f6(a1),f6(a1),f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[8053,7919,8152,7952,40,32,44])).
% 129.05/129.05 cnf(8453,plain,
% 129.05/129.05 (~P3(a5,a1,a8)),
% 129.05/129.05 inference(scs_inference,[],[8000,7948,8053,8426,7919,8152,7952,40,32,44,47,41])).
% 129.05/129.05 cnf(8471,plain,
% 129.05/129.05 (P3(a4,a2,a2)),
% 129.05/129.05 inference(scs_inference,[],[8272,3,40,32])).
% 129.05/129.05 cnf(8488,plain,
% 129.05/129.05 (P3(a4,a7,a7)),
% 129.05/129.05 inference(scs_inference,[],[7937,5,40,32])).
% 129.05/129.05 cnf(8490,plain,
% 129.05/129.05 (P3(f13(a8),a12,a2)),
% 129.05/129.05 inference(scs_inference,[],[8471,7937,3896,3748,5,40,32,45])).
% 129.05/129.05 cnf(8496,plain,
% 129.05/129.05 (~P2(a2,f6(a8),a2)),
% 129.05/129.05 inference(scs_inference,[],[8471,7822,8089,7937,7659,7690,3896,3748,7952,5,40,32,45,43,39,44])).
% 129.05/129.05 cnf(8498,plain,
% 129.05/129.05 (P3(a17,a4,a17)),
% 129.05/129.05 inference(scs_inference,[],[8471,7822,8089,7937,7659,7690,3896,3748,7952,5,40,32,45,43,39,44,7511])).
% 129.05/129.05 cnf(8504,plain,
% 129.05/129.05 (P3(a4,a5,a5)),
% 129.05/129.05 inference(scs_inference,[],[8369,4,40,32])).
% 129.05/129.05 cnf(8508,plain,
% 129.05/129.05 (~P2(f3(a2,a2),f6(a8),f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[8498,8369,8496,8235,8160,4,40,32,46,44])).
% 129.05/129.05 cnf(8516,plain,
% 129.05/129.05 (P3(a4,a1,a1)),
% 129.05/129.05 inference(scs_inference,[],[8508,1,40,32])).
% 129.05/129.05 cnf(8518,plain,
% 129.05/129.05 (P3(f14(a4,a4),a2,a2)),
% 129.05/129.05 inference(scs_inference,[],[8508,8490,8154,3748,1,40,32,46])).
% 129.05/129.05 cnf(8520,plain,
% 129.05/129.05 (~P2(f14(a1,a1),a1,a8)),
% 129.05/129.05 inference(scs_inference,[],[8508,8438,8490,8154,7736,3748,7964,1,40,32,46,48])).
% 129.05/129.05 cnf(8522,plain,
% 129.05/129.05 (P3(f14(a4,a4),a16,a16)),
% 129.05/129.05 inference(scs_inference,[],[8508,8438,8490,8154,7736,3748,7964,1,40,32,46,48,76])).
% 129.05/129.05 cnf(8524,plain,
% 129.05/129.05 (P3(f14(a4,a4),a12,a12)),
% 129.05/129.05 inference(scs_inference,[],[8508,8438,8490,8154,7736,3748,7964,1,40,32,46,48,76,128])).
% 129.05/129.05 cnf(8526,plain,
% 129.05/129.05 (~P3(x85261,a8,a8)+P3(x85261,a4,a4)),
% 129.05/129.05 inference(scs_inference,[],[8508,8438,8490,8154,7736,3748,7964,3898,1,40,32,46,48,76,128,45])).
% 129.05/129.05 cnf(8544,plain,
% 129.05/129.05 (P3(a4,a8,a8)),
% 129.05/129.05 inference(scs_inference,[],[6,32])).
% 129.05/129.05 cnf(8554,plain,
% 129.05/129.05 (P3(f3(a4,a4),a2,f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[8516,8518,8520,8308,3673,7732,7702,7836,6,32,40,47,41,27,48])).
% 129.05/129.05 cnf(8560,plain,
% 129.05/129.05 (P3(f3(a4,a4),a16,f3(a16,a16))),
% 129.05/129.05 inference(scs_inference,[],[8554,8251,7742,20,40,45])).
% 129.05/129.05 cnf(8562,plain,
% 129.05/129.05 (~P3(f3(a4,a4),a8,a8)),
% 129.05/129.05 inference(scs_inference,[],[8105,8544,8554,8251,7742,7836,20,40,45,47])).
% 129.05/129.05 cnf(8564,plain,
% 129.05/129.05 (~P2(f14(a1,a1),a1,a5)),
% 129.05/129.05 inference(scs_inference,[],[8105,8544,8554,8251,8516,7742,8037,7736,7964,7836,20,40,45,47,48])).
% 129.05/129.05 cnf(8568,plain,
% 129.05/129.05 (~P3(a4,a4,f3(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[8105,8544,8554,8251,8516,7742,8037,7736,7964,7836,20,40,45,47,48,41,46])).
% 129.05/129.05 cnf(8589,plain,
% 129.05/129.05 (~P2(a17,f6(a8),a17)),
% 129.05/129.05 inference(scs_inference,[],[7787,8522,8564,8568,8089,7859,7875,7621,7556,53,40,42,45,46,44])).
% 129.05/129.05 cnf(8591,plain,
% 129.05/129.05 (~P3(a1,a12,a8)),
% 129.05/129.05 inference(scs_inference,[],[7757,7787,8060,8522,8564,8568,8089,7859,7875,8490,7621,7556,53,40,42,45,46,44,47])).
% 129.05/129.05 cnf(8593,plain,
% 129.05/129.05 (~P3(a5,f3(a4,a4),a5)),
% 129.05/129.05 inference(scs_inference,[],[7757,7787,8060,8522,8564,8568,8089,7859,7875,8490,7621,7556,53,40,42,45,46,44,47,7433])).
% 129.05/129.05 cnf(8599,plain,
% 129.05/129.05 (P2(a1,a10,a1)+P1(f13(a10))),
% 129.05/129.05 inference(scs_inference,[],[7757,7787,8060,8522,8564,8568,7889,8089,7859,7875,8490,7621,7556,7544,10,53,40,42,45,46,44,47,7433,41,48,34])).
% 129.05/129.05 cnf(8601,plain,
% 129.05/129.05 (~P3(a12,a1,a8)),
% 129.05/129.05 inference(scs_inference,[],[8591,41])).
% 129.05/129.05 cnf(8603,plain,
% 129.05/129.05 (~P2(f6(a8),a17,a17)),
% 129.05/129.05 inference(scs_inference,[],[8591,8589,41,40])).
% 129.05/129.05 cnf(8607,plain,
% 129.05/129.05 (~P3(f3(a4,a4),f14(a4,a4),a4)),
% 129.05/129.05 inference(scs_inference,[],[8591,7917,8589,8029,8568,7907,53,41,40,42,46])).
% 129.05/129.05 cnf(8611,plain,
% 129.05/129.05 (~P2(f3(a17,a17),f6(a8),f3(a17,a17))),
% 129.05/129.05 inference(scs_inference,[],[8591,7917,8589,8029,8568,8518,7907,7696,7708,53,41,40,42,46,45,44])).
% 129.05/129.05 cnf(8613,plain,
% 129.05/129.05 (~P2(a4,a4,a4)),
% 129.05/129.05 inference(scs_inference,[],[8591,7917,8589,8029,8105,8568,8518,7907,7696,8544,7708,53,41,40,42,46,45,44,47])).
% 129.05/129.05 cnf(8620,plain,
% 129.05/129.05 (~P2(f13(a8),f13(a8),f13(a8))),
% 129.05/129.05 inference(scs_inference,[],[8613,3900])).
% 129.05/129.05 cnf(8621,plain,
% 129.05/129.05 (~P2(a5,a5,a5)),
% 129.05/129.05 inference(scs_inference,[],[8613,3916])).
% 129.05/129.05 cnf(8622,plain,
% 129.05/129.05 (~P2(f13(a5),f13(a5),f13(a5))),
% 129.05/129.05 inference(scs_inference,[],[8613,3924])).
% 129.05/129.05 cnf(8624,plain,
% 129.05/129.05 (~P3(f3(a4,a4),a5,a5)),
% 129.05/129.05 inference(scs_inference,[],[8593,41])).
% 129.05/129.05 cnf(8628,plain,
% 129.05/129.05 (P2(f3(a16,a16),a1,f3(a16,a16))),
% 129.05/129.05 inference(scs_inference,[],[8593,8611,8386,7558,41,40,44])).
% 129.05/129.05 cnf(8630,plain,
% 129.05/129.05 (~P3(f3(a4,a4),f6(a1),f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[8449,8593,8611,8386,8316,7558,7836,41,40,44,47])).
% 129.05/129.05 cnf(8632,plain,
% 129.05/129.05 (P3(f3(a4,a4),a7,f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[8449,8593,8611,8386,8488,8316,7867,7558,7836,41,40,44,47,48])).
% 129.05/129.05 cnf(8644,plain,
% 129.05/129.05 (~P2(a18,f6(a8),a18)),
% 129.05/129.05 inference(scs_inference,[],[8607,8496,8089,7651,41,40,44])).
% 129.05/129.05 cnf(8646,plain,
% 129.05/129.05 (~P3(f3(a4,a4),f13(a8),f13(a8))),
% 129.05/129.05 inference(scs_inference,[],[8620,8607,8496,8064,8089,7651,7836,41,40,44,47])).
% 129.05/129.05 cnf(8648,plain,
% 129.05/129.05 (~P3(a1,a4,a4)),
% 129.05/129.05 inference(scs_inference,[],[8620,8607,8496,8064,7706,8089,8568,7651,7736,7836,41,40,44,47,48])).
% 129.05/129.05 cnf(8650,plain,
% 129.05/129.05 (~P3(a1,a8,a8)),
% 129.05/129.05 inference(scs_inference,[],[8620,8607,8496,8064,7706,8089,8568,7651,7736,7836,41,40,44,47,48,8526])).
% 129.05/129.05 cnf(8665,plain,
% 129.05/129.05 (~P3(a4,a1,a4)),
% 129.05/129.05 inference(scs_inference,[],[8648,41])).
% 129.05/129.05 cnf(8669,plain,
% 129.05/129.05 (~P3(a4,a4,a1)),
% 129.05/129.05 inference(scs_inference,[],[8648,8644,7706,41,40,46])).
% 129.05/129.05 cnf(8671,plain,
% 129.05/129.05 (P3(f3(a4,a4),a15,f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[8648,8644,8632,7706,8426,3762,41,40,46,45])).
% 129.05/129.05 cnf(8673,plain,
% 129.05/129.05 (~P2(f3(a18,a18),f6(a8),f3(a18,a18))),
% 129.05/129.05 inference(scs_inference,[],[8648,8644,8632,8072,7706,8426,3762,41,40,46,45,44])).
% 129.05/129.05 cnf(8675,plain,
% 129.05/129.05 (~P3(a1,a2,a8)),
% 129.05/129.05 inference(scs_inference,[],[7582,8648,8348,8644,8632,3740,8072,7706,8426,3762,41,40,46,45,44,47])).
% 129.05/129.05 cnf(8677,plain,
% 129.05/129.05 (~P3(a8,a1,a8)),
% 129.05/129.05 inference(scs_inference,[],[7582,8648,8348,8644,8632,3740,8072,7706,8426,3762,41,40,46,45,44,47,7414])).
% 129.05/129.05 cnf(8679,plain,
% 129.05/129.05 (~P3(a5,a1,a5)),
% 129.05/129.05 inference(scs_inference,[],[7582,8648,8348,8644,8632,3740,8072,7706,8426,3762,41,40,46,45,44,47,7414,7433])).
% 129.05/129.05 cnf(8685,plain,
% 129.05/129.05 (~P3(a2,a1,a8)),
% 129.05/129.05 inference(scs_inference,[],[8675,41])).
% 129.05/129.05 cnf(8689,plain,
% 129.05/129.05 (P3(f13(a8),f14(a8,a8),a8)),
% 129.05/129.05 inference(scs_inference,[],[8675,8673,7996,8544,3896,41,40,45])).
% 129.05/129.05 cnf(8691,plain,
% 129.05/129.05 (~P3(f13(a8),a8,a1)),
% 129.05/129.05 inference(scs_inference,[],[8650,8675,8673,7996,8544,3896,41,40,45,46])).
% 129.05/129.05 cnf(8693,plain,
% 129.05/129.05 (~P2(f3(a16,a16),f6(a5),f3(a16,a16))),
% 129.05/129.05 inference(scs_inference,[],[8650,8675,8673,8628,7637,7996,8544,7921,3896,41,40,45,46,44])).
% 129.05/129.05 cnf(8703,plain,
% 129.05/129.05 (~P2(f6(a5),f3(a16,a16),f3(a16,a16))),
% 129.05/129.05 inference(scs_inference,[],[8679,8693,41,40])).
% 129.05/129.05 cnf(8705,plain,
% 129.05/129.05 (~P3(f13(a8),a8,f3(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[8679,8562,8693,8689,7996,41,40,46])).
% 129.05/129.05 cnf(8707,plain,
% 129.05/129.05 (~P2(a10,f6(a8),a10)),
% 129.05/129.05 inference(scs_inference,[],[8679,8562,8693,8689,8089,7996,7759,41,40,46,44])).
% 129.05/129.05 cnf(8709,plain,
% 129.05/129.05 (~P3(f3(a4,a4),f13(a5),f13(a5))),
% 129.05/129.05 inference(scs_inference,[],[8679,8622,8562,8693,8689,7692,8089,7996,7759,7836,41,40,46,44,47])).
% 129.05/129.05 cnf(8711,plain,
% 129.05/129.05 (P3(f3(a4,a4),a10,f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[8679,8622,8562,8693,8689,7692,8089,7996,7759,1170,7771,7836,41,40,46,44,47,48])).
% 129.05/129.05 cnf(8724,plain,
% 129.05/129.05 (~P3(f14(a8,a8),a1,f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[8677,8630,8707,8148,8689,53,41,40,42,46])).
% 129.05/129.05 cnf(8726,plain,
% 129.05/129.05 (~P2(f3(a10,a10),f6(a8),f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[8677,8630,8707,8148,8689,8253,53,41,40,42,46,44])).
% 129.05/129.05 cnf(8728,plain,
% 129.05/129.05 (~P3(f3(a4,a4),a1,a5)),
% 129.05/129.05 inference(scs_inference,[],[8677,8630,8707,8148,8689,4913,8516,8253,7836,53,41,40,42,46,44,47])).
% 129.05/129.05 cnf(8730,plain,
% 129.05/129.05 (~P3(a1,a4,f6(a4))),
% 129.05/129.05 inference(scs_inference,[],[8677,8669,8630,8707,8148,8689,4913,8516,8253,7826,7706,7736,7836,53,41,40,42,46,44,47,48])).
% 129.05/129.05 cnf(8740,plain,
% 129.05/129.05 (~P3(a4,f14(a4,a4),a1)),
% 129.05/129.05 inference(scs_inference,[],[8726,8646,8691,8064,8154,41,40,46])).
% 129.05/129.05 cnf(8742,plain,
% 129.05/129.05 (P2(f3(a1,a1),a12,a12)),
% 129.05/129.05 inference(scs_inference,[],[8726,8646,8691,8002,8064,8388,8154,3789,41,40,46,44])).
% 129.05/129.05 cnf(8744,plain,
% 129.05/129.05 (~P3(f6(a1),a5,a8)),
% 129.05/129.05 inference(scs_inference,[],[8726,8646,8691,8201,7948,8002,8064,8388,8154,8426,3789,41,40,46,44,47])).
% 129.05/129.05 cnf(8758,plain,
% 129.05/129.05 (~P2(a7,f6(a8),a7)),
% 129.05/129.05 inference(scs_inference,[],[8728,8447,8140,7673,7855,8089,7830,41,40,45,46,44])).
% 129.05/129.05 cnf(8767,plain,
% 129.05/129.05 (~P2(f6(a8),a7,a7)),
% 129.05/129.05 inference(scs_inference,[],[8709,8758,41,40])).
% 129.05/129.05 cnf(8769,plain,
% 129.05/129.05 (P2(f6(a16),a11,a17)),
% 129.05/129.05 inference(scs_inference,[],[8709,8758,7667,7544,16,41,40,43])).
% 129.05/129.05 cnf(8777,plain,
% 129.05/129.05 (~P3(a1,f14(a8,a8),f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[8724,41])).
% 129.05/129.05 cnf(8779,plain,
% 129.05/129.05 (~P2(a8,a11,a11)),
% 129.05/129.05 inference(scs_inference,[],[8724,7728,41,40])).
% 129.05/129.05 cnf(8783,plain,
% 129.05/129.05 (~P2(f14(a1,a1),a1,a4)),
% 129.05/129.05 inference(scs_inference,[],[8724,7617,8665,7728,8516,7952,7736,7964,41,40,43,48])).
% 129.05/129.05 cnf(8795,plain,
% 129.05/129.05 (P3(f3(a15,a15),a4,f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[8740,8783,8243,8671,53,910,41,40,42,46])).
% 129.05/129.05 cnf(8797,plain,
% 129.05/129.05 (P3(f3(a4,a4),a11,f3(a11,a11))),
% 129.05/129.05 inference(scs_inference,[],[8740,8783,8243,8671,7734,2140,7836,53,910,41,40,42,46,48])).
% 129.05/129.05 cnf(8803,plain,
% 129.05/129.05 (~P3(a8,f13(a8),f3(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[8705,41])).
% 129.05/129.05 cnf(8809,plain,
% 129.05/129.05 (P2(a17,a1,a17)),
% 129.05/129.05 inference(scs_inference,[],[8705,8797,8296,8769,3774,53,796,41,42,46,44])).
% 129.05/129.05 cnf(8811,plain,
% 129.05/129.05 (~P3(f3(a8,a8),f13(a8),a4)),
% 129.05/129.05 inference(scs_inference,[],[8613,8705,8797,8296,8769,7994,3774,3898,53,796,41,42,46,44,47])).
% 129.05/129.05 cnf(8813,plain,
% 129.05/129.05 (~P3(a1,a8,f14(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[8613,8705,8797,8296,8060,8769,8308,8154,7994,3774,3898,53,796,41,42,46,44,47,48])).
% 129.05/129.05 cnf(8819,plain,
% 129.05/129.05 (~P3(a4,a1,f6(a4))),
% 129.05/129.05 inference(scs_inference,[],[8730,41])).
% 129.05/129.05 cnf(8821,plain,
% 129.05/129.05 (~P3(a8,a4,f3(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[8730,8811,8064,3898,41,46])).
% 129.05/129.05 cnf(8823,plain,
% 129.05/129.05 (P2(f3(a17,a17),a1,f3(a17,a17))),
% 129.05/129.05 inference(scs_inference,[],[8809,8730,8811,8064,7633,3898,41,46,44])).
% 129.05/129.05 cnf(8825,plain,
% 129.05/129.05 (~P3(f3(a5,a5),f13(a5),a4)),
% 129.05/129.05 inference(scs_inference,[],[8809,8730,8811,8613,8064,7929,7633,3898,3911,41,46,44,47])).
% 129.05/129.05 cnf(8827,plain,
% 129.05/129.05 (~P3(f6(a4),f14(a8,a8),a1)),
% 129.05/129.05 inference(scs_inference,[],[8809,8730,8811,8777,8047,8613,8045,8064,7929,7633,7826,3898,3911,41,46,44,47,48])).
% 129.05/129.05 cnf(8831,plain,
% 129.05/129.05 (P3(f13(a8),a4,f13(a8))),
% 129.05/129.05 inference(scs_inference,[],[8809,8730,8811,8777,8047,8613,8045,7718,8064,7929,7633,3896,7826,3898,3911,41,46,44,47,48,27,45])).
% 129.05/129.05 cnf(8835,plain,
% 129.05/129.05 (~P3(f13(a5),f3(a5,a5),a4)),
% 129.05/129.05 inference(scs_inference,[],[8825,41])).
% 129.05/129.05 cnf(8837,plain,
% 129.05/129.05 (P3(f13(a8),a10,a5)),
% 129.05/129.05 inference(scs_inference,[],[8825,3769,8504,3896,41,45])).
% 129.05/129.05 cnf(8841,plain,
% 129.05/129.05 (~P3(f3(a1,a1),a4,a8)),
% 129.05/129.05 inference(scs_inference,[],[8825,8380,7976,8399,8777,8689,3769,8504,7996,3896,41,45,46,47])).
% 129.05/129.05 cnf(8845,plain,
% 129.05/129.05 (~P2(a1,f14(a1,a1),f6(a4))),
% 129.05/129.05 inference(scs_inference,[],[8825,8819,8380,7976,8399,8777,8689,3769,8504,7996,8516,3896,7736,7964,41,45,46,47,48,40])).
% 129.05/129.05 cnf(8853,plain,
% 129.05/129.05 (~P3(f14(a4,a4),f13(a8),a1)),
% 129.05/129.05 inference(scs_inference,[],[8827,8813,8029,3896,41,46])).
% 129.05/129.05 cnf(8858,plain,
% 129.05/129.05 (~P3(a4,a8,f3(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[8821,41])).
% 129.05/129.05 cnf(8860,plain,
% 129.05/129.05 (~P3(a5,a4,f3(a5,a5))),
% 129.05/129.05 inference(scs_inference,[],[8821,8825,7692,3911,41,46])).
% 129.05/129.05 cnf(8862,plain,
% 129.05/129.05 (~P2(a8,f6(a8),a8)),
% 129.05/129.05 inference(scs_inference,[],[8821,8825,7692,7982,8089,3911,41,46,44])).
% 129.05/129.05 cnf(8868,plain,
% 129.05/129.05 (~P3(a1,a10,a8)),
% 129.05/129.05 inference(scs_inference,[],[8821,8298,8711,7851,8825,7865,7692,7982,8089,3911,41,46,44,40,39,47])).
% 129.05/129.05 cnf(8873,plain,
% 129.05/129.05 (~P3(f13(a8),a10,a1)),
% 129.05/129.05 inference(scs_inference,[],[8868,8837,8035,836,41,46])).
% 129.05/129.05 cnf(8875,plain,
% 129.05/129.05 (~P2(f6(a5),a1,a1)),
% 129.05/129.05 inference(scs_inference,[],[8868,8837,8035,7807,7921,836,23,41,46,44])).
% 129.05/129.05 cnf(8877,plain,
% 129.05/129.05 (~P2(a1,f6(a5),a1)),
% 129.05/129.05 inference(scs_inference,[],[8868,8837,8035,7807,7921,836,23,41,46,44,40])).
% 129.05/129.05 cnf(8886,plain,
% 129.05/129.05 (~P3(a4,f13(a8),a1)),
% 129.05/129.05 inference(scs_inference,[],[8853,8225,8813,7895,8154,53,41,42,46])).
% 129.05/129.05 cnf(8896,plain,
% 129.05/129.05 (~P3(f14(a4,a4),a5,a1)),
% 129.05/129.05 inference(scs_inference,[],[8841,8873,8314,3769,8154,53,41,42,45])).
% 129.05/129.05 cnf(8898,plain,
% 129.05/129.05 (~P3(a4,a5,a1)),
% 129.05/129.05 inference(scs_inference,[],[8841,8873,8314,8837,3769,8064,8154,53,41,42,45,46])).
% 129.05/129.05 cnf(8906,plain,
% 129.05/129.05 (~P2(a2,f6(a5),a2)),
% 129.05/129.05 inference(scs_inference,[],[8898,8877,7690,41,44])).
% 129.05/129.05 cnf(8914,plain,
% 129.05/129.05 (~P3(a4,a5,f3(a5,a5))),
% 129.05/129.05 inference(scs_inference,[],[8860,41])).
% 129.05/129.05 cnf(8916,plain,
% 129.05/129.05 (P3(a17,a10,a15)),
% 129.05/129.05 inference(scs_inference,[],[8860,8837,3762,21,41,46])).
% 129.05/129.05 cnf(8920,plain,
% 129.05/129.05 (~P2(a1,f6(a8),f6(a1))),
% 129.05/129.05 inference(scs_inference,[],[8860,7990,8837,7773,3762,7982,21,41,46,44,40])).
% 129.05/129.05 cnf(8933,plain,
% 129.05/129.05 (P3(f13(a5),f14(a5,a5),a5)),
% 129.05/129.05 inference(scs_inference,[],[8886,7927,8504,3909,41,45])).
% 129.05/129.05 cnf(8935,plain,
% 129.05/129.05 (~P3(a1,f13(a8),a4)),
% 129.05/129.05 inference(scs_inference,[],[8803,8886,7927,7773,8504,3909,3898,7836,41,45,48])).
% 129.05/129.05 cnf(8939,plain,
% 129.05/129.05 (~P2(f3(a2,a2),f6(a5),f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[8601,8803,8906,8886,7927,8220,8160,7773,8504,3909,3898,7836,41,45,48,46,44])).
% 129.05/129.05 cnf(8948,plain,
% 129.05/129.05 (~P2(f6(a5),f3(a2,a2),f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[8939,8896,41,40])).
% 129.05/129.05 cnf(8950,plain,
% 129.05/129.05 (~P3(f13(a5),a5,f3(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[8624,8939,8896,8933,7927,41,40,46])).
% 129.05/129.05 cnf(8952,plain,
% 129.05/129.05 (~P2(f6(a1),f6(a1),f6(a5))),
% 129.05/129.05 inference(scs_inference,[],[8624,8939,8896,8933,8875,7927,7952,41,40,46,44])).
% 129.05/129.05 cnf(8960,plain,
% 129.05/129.05 (~P3(a5,f13(a5),f3(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[8950,41])).
% 129.05/129.05 cnf(8973,plain,
% 129.05/129.05 (~P3(a5,f6(a1),a8)),
% 129.05/129.05 inference(scs_inference,[],[8744,41])).
% 129.05/129.05 cnf(8975,plain,
% 129.05/129.05 (~P3(a8,a4,a1)),
% 129.05/129.05 inference(scs_inference,[],[8744,8935,8064,3898,41,46])).
% 129.05/129.05 cnf(8984,plain,
% 129.05/129.05 (~P3(a4,a8,a1)),
% 129.05/129.05 inference(scs_inference,[],[8975,41])).
% 129.05/129.05 cnf(9001,plain,
% 129.05/129.05 (~P3(f13(a8),f3(a8,a8),a4)),
% 129.05/129.05 inference(scs_inference,[],[8811,41])).
% 129.05/129.05 cnf(9003,plain,
% 129.05/129.05 (~P3(f3(a4,a4),f6(a1),f6(a5))),
% 129.05/129.05 inference(scs_inference,[],[8952,8811,8316,7836,41,47])).
% 129.05/129.05 cnf(9012,plain,
% 129.05/129.05 (~P3(a1,a7,a8)),
% 129.05/129.05 inference(scs_inference,[],[9003,7939,8375,7948,41,47])).
% 129.05/129.05 cnf(9014,plain,
% 129.05/129.05 (~P3(a1,a8,f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[8984,9003,7939,8375,7948,8544,7982,7736,41,47,48])).
% 129.05/129.05 cnf(9023,plain,
% 129.05/129.05 (~P3(a1,f13(a5),a4)),
% 129.05/129.05 inference(scs_inference,[],[9012,8960,7807,3911,7836,41,48])).
% 129.05/129.05 cnf(9031,plain,
% 129.05/129.05 (~P3(f13(a8),f14(a8,a8),f3(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[9014,8858,7996,3896,41,46])).
% 129.05/129.05 cnf(9035,plain,
% 129.05/129.05 (~P2(f6(a1),f14(a1,a1),f6(a4))),
% 129.05/129.05 inference(scs_inference,[],[9014,8858,8845,8021,7907,7996,3896,7952,41,46,45,44])).
% 129.05/129.05 cnf(9050,plain,
% 129.05/129.05 (P2(f3(a15,a15),a1,f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[8914,9031,9035,8432,8665,8318,7598,7387,41,40,45,44])).
% 129.05/129.05 cnf(9070,plain,
% 129.05/129.05 (~P3(a1,f14(a5,a5),a5)),
% 129.05/129.05 inference(scs_inference,[],[8621,9023,8348,8933,41,47])).
% 129.05/129.05 cnf(9079,plain,
% 129.05/129.05 (P2(f6(a1),f3(a10,a10),f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[9070,8033,7952,41,43])).
% 129.05/129.05 cnf(9086,plain,
% 129.05/129.05 (~P3(f13(a5),a4,a1)),
% 129.05/129.05 inference(scs_inference,[],[8365,9070,8935,8933,41,46])).
% 129.05/129.05 cnf(9093,plain,
% 129.05/129.05 (~P3(a4,f13(a5),a1)),
% 129.05/129.05 inference(scs_inference,[],[9086,41])).
% 129.05/129.05 cnf(9097,plain,
% 129.05/129.05 (~P2(a17,f6(a17),a8)),
% 129.05/129.05 inference(scs_inference,[],[8835,9086,7954,8779,8336,3794,41,46,44])).
% 129.05/129.05 cnf(9108,plain,
% 129.05/129.05 (~P3(a10,f6(a1),f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[8973,9097,8873,8689,8837,41,40,46])).
% 129.05/129.05 cnf(9115,plain,
% 129.05/129.05 (~P2(a10,f6(a5),a10)),
% 129.05/129.05 inference(scs_inference,[],[9108,8877,7759,41,44])).
% 129.05/129.05 cnf(9117,plain,
% 129.05/129.05 (~P2(f6(a5),a10,a10)),
% 129.05/129.05 inference(scs_inference,[],[9108,8877,7759,41,44,40])).
% 129.05/129.05 cnf(9124,plain,
% 129.05/129.05 (~P3(a8,a1,f14(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[8813,41])).
% 129.05/129.05 cnf(9134,plain,
% 129.05/129.05 (~P3(a1,f14(a8,a8),a8)),
% 129.05/129.05 inference(scs_inference,[],[9115,8453,9031,8060,8253,8689,8837,7994,46,44,48])).
% 129.05/129.05 cnf(9138,plain,
% 129.05/129.05 (~P2(f6(a5),f3(a10,a10),f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[9115,8453,9031,8060,8253,8689,8837,7994,46,44,48,41,40])).
% 129.05/129.05 cnf(9145,plain,
% 129.05/129.05 (P2(a1,a10,f3(a10,a10))+P1(f13(a10))),
% 129.05/129.05 inference(scs_inference,[],[7771,8033,8599,44])).
% 129.05/129.05 cnf(9150,plain,
% 129.05/129.05 (~P3(a1,a16,f6(a5))),
% 129.05/129.05 inference(scs_inference,[],[9134,8920,8560,8330,8703,7851,7952,41,44,47])).
% 129.05/129.05 cnf(9160,plain,
% 129.05/129.05 (~P3(f6(a1),a4,f6(a5))),
% 129.05/129.05 inference(scs_inference,[],[9138,9150,9079,7783,41,47])).
% 129.05/129.05 cnf(9169,plain,
% 129.05/129.05 (~P3(f14(a5,a5),a1,f14(a5,a5))),
% 129.05/129.05 inference(scs_inference,[],[9160,8679,8933,41,46])).
% 129.05/129.05 cnf(9175,plain,
% 129.05/129.05 (~P3(a1,f14(a5,a5),f14(a5,a5))),
% 129.05/129.05 inference(scs_inference,[],[9169,41])).
% 129.05/129.05 cnf(9177,plain,
% 129.05/129.05 (P3(a5,a16,a2)),
% 129.05/129.05 inference(scs_inference,[],[9169,8471,3740,3911,41,45])).
% 129.05/129.05 cnf(9179,plain,
% 129.05/129.05 (P2(f6(a1),f3(a15,a15),f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[9169,7635,8471,3740,7952,3911,41,45,43])).
% 129.05/129.05 cnf(9181,plain,
% 129.05/129.05 (~P3(f3(a8,a8),f13(a8),x91811)+P3(x91811,a10,f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[9169,7635,8142,8471,3740,8837,7952,3911,41,45,43,46])).
% 129.05/129.05 cnf(9187,plain,
% 129.05/129.05 (~P3(f13(a5),a5,a1)),
% 129.05/129.05 inference(scs_inference,[],[9175,7927,8933,46,41])).
% 129.05/129.05 cnf(9194,plain,
% 129.05/129.05 (~P3(f3(a4,a4),a10,a10)),
% 129.05/129.05 inference(scs_inference,[],[8593,8837,46,41])).
% 129.05/129.05 cnf(9203,plain,
% 129.05/129.05 (P3(f3(a10,a10),a16,f3(a12,a12))),
% 129.05/129.05 inference(scs_inference,[],[9177,8274,8142,46])).
% 129.05/129.05 cnf(9208,plain,
% 129.05/129.05 (~P2(a5,f6(a5),a5)),
% 129.05/129.05 inference(scs_inference,[],[8877,7921,44])).
% 129.05/129.05 cnf(9217,plain,
% 129.05/129.05 (P3(f3(a12,a12),a4,f3(a12,a12))),
% 129.05/129.05 inference(scs_inference,[],[9203,733,46])).
% 129.05/129.05 cnf(9224,plain,
% 129.05/129.05 (~P3(a1,a8,a4)),
% 129.05/129.05 inference(scs_inference,[],[9124,8544,7830,46,41])).
% 129.05/129.05 cnf(9229,plain,
% 129.05/129.05 (~P3(a4,f3(a10,a10),a10)),
% 129.05/129.05 inference(scs_inference,[],[9194,8711,7859,46])).
% 129.05/129.05 cnf(9231,plain,
% 129.05/129.05 (~P2(a7,f6(a5),a7)),
% 129.05/129.05 inference(scs_inference,[],[9194,8711,7859,8877,7855,46,44])).
% 129.05/129.05 cnf(9233,plain,
% 129.05/129.05 (~P3(f3(a10,a10),a4,a10)),
% 129.05/129.05 inference(scs_inference,[],[9194,8711,7859,8877,7855,46,44,41])).
% 129.05/129.05 cnf(9235,plain,
% 129.05/129.05 (~P2(f6(a5),a7,a7)),
% 129.05/129.05 inference(scs_inference,[],[9194,8711,7859,8877,7855,46,44,41,40])).
% 129.05/129.05 cnf(9239,plain,
% 129.05/129.05 (~P3(f6(a1),a4,a8)),
% 129.05/129.05 inference(scs_inference,[],[9179,9194,8795,8711,7859,7948,8877,8490,7855,46,44,41,40,7479,47])).
% 129.05/129.05 cnf(9243,plain,
% 129.05/129.05 (~P3(a4,f6(a1),a8)),
% 129.05/129.05 inference(scs_inference,[],[9239,41])).
% 129.05/129.05 cnf(9245,plain,
% 129.05/129.05 (~P3(a1,f3(a10,a10),f6(a10))),
% 129.05/129.05 inference(scs_inference,[],[9229,9239,8229,8253,7736,41,48])).
% 129.05/129.05 cnf(9253,plain,
% 129.05/129.05 (~P3(a8,f6(a1),f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[9245,9243,8689,3896,41,46])).
% 129.05/129.05 cnf(9255,plain,
% 129.05/129.05 (P3(f3(a5,a5),a16,f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[9245,9243,9177,7929,8689,7702,3896,41,46,48])).
% 129.05/129.05 cnf(9260,plain,
% 129.05/129.05 (~P3(f6(a1),a8,f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[9253,41])).
% 129.05/129.05 cnf(9264,plain,
% 129.05/129.05 (~P3(f13(a8),f14(a8,a8),a1)),
% 129.05/129.05 inference(scs_inference,[],[9253,8984,7787,7996,3896,7952,41,43,46])).
% 129.05/129.05 cnf(9266,plain,
% 129.05/129.05 (~P2(a10,a10,a10)),
% 129.05/129.05 inference(scs_inference,[],[9233,9253,8984,7787,7996,7771,3896,836,7952,41,43,46,48])).
% 129.05/129.05 cnf(9271,plain,
% 129.05/129.05 (~P2(a5,a5,a5)),
% 129.05/129.05 inference(scs_inference,[],[9266,150])).
% 129.05/129.05 cnf(9276,plain,
% 129.05/129.05 (~P3(a4,a8,f6(a1))),
% 129.05/129.05 inference(scs_inference,[],[9260,9264,8047,7996,41,46])).
% 129.05/129.05 cnf(9296,plain,
% 129.05/129.05 (P3(f13(a5),a15,a7)),
% 129.05/129.05 inference(scs_inference,[],[8488,18,3909,45])).
% 129.05/129.05 cnf(9300,plain,
% 129.05/129.05 (P3(f3(a4,a4),a12,f3(a12,a12))),
% 129.05/129.05 inference(scs_inference,[],[9276,8488,8524,8308,7805,8154,18,3898,3909,45,46,48])).
% 129.05/129.05 cnf(9302,plain,
% 129.05/129.05 (~P3(f14(a4,a4),a8,f6(a1))),
% 129.05/129.05 inference(scs_inference,[],[9276,8488,8524,8308,7805,8154,18,3898,3909,45,46,48,41])).
% 129.05/129.05 cnf(9307,plain,
% 129.05/129.05 (~P2(f3(a10,a10),a10,f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[9266,8253,44])).
% 129.05/129.05 cnf(9309,plain,
% 129.05/129.05 (P3(f3(a2,a2),a8,f3(a12,a12))),
% 129.05/129.05 inference(scs_inference,[],[9300,9266,8554,8253,17,44,46])).
% 129.05/129.05 cnf(9311,plain,
% 129.05/129.05 (~P2(a10,f3(a10,a10),f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[9300,9266,8554,8253,17,44,46,40])).
% 129.05/129.05 cnf(9318,plain,
% 129.05/129.05 (~P3(f13(a8),f3(a10,a10),a5)),
% 129.05/129.05 inference(scs_inference,[],[9309,9229,9217,3769,3898,45,46])).
% 129.05/129.05 cnf(9323,plain,
% 129.05/129.05 (~P3(a10,a4,f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[9318,9233,7706,836,41,46])).
% 129.05/129.05 cnf(9332,plain,
% 129.05/129.05 (~P3(a4,a10,f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[9323,41])).
% 129.05/129.05 cnf(9336,plain,
% 129.05/129.05 (~P3(a10,f14(a4,a4),f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[9323,9311,9079,7830,836,41,44,46])).
% 129.05/129.05 cnf(9343,plain,
% 129.05/129.05 (~P3(f14(a4,a4),a10,f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[9336,41])).
% 129.05/129.05 cnf(9345,plain,
% 129.05/129.05 (P2(f3(a9,a9),a1,f3(a9,a9))),
% 129.05/129.05 inference(scs_inference,[],[9336,7901,755,41,44])).
% 129.05/129.05 cnf(9347,plain,
% 129.05/129.05 (~P3(f14(a5,a5),f3(a4,a4),f14(a5,a5))),
% 129.05/129.05 inference(scs_inference,[],[9336,8593,7901,8933,755,41,44,46])).
% 129.05/129.05 cnf(9351,plain,
% 129.05/129.05 (~P3(f3(a8,a8),f13(a8),f14(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[9336,9332,8593,1170,7901,7771,8933,7736,755,41,44,46,48,9181])).
% 129.05/129.05 cnf(9370,plain,
% 129.05/129.05 (~P3(f14(a4,a4),a8,f3(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[9347,9351,8029,8877,7982,3898,41,44,46])).
% 129.05/129.05 cnf(9374,plain,
% 129.05/129.05 (~P3(f3(a5,a5),a5,f14(a5,a5))),
% 129.05/129.05 inference(scs_inference,[],[9347,9351,8365,8029,8877,7929,7927,7982,3898,7836,41,44,46,48,47])).
% 129.05/129.05 cnf(9385,plain,
% 129.05/129.05 (~P2(a4,a4,f14(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[9370,9307,9351,7905,7994,7771,3898,41,44,48])).
% 129.05/129.05 cnf(9387,plain,
% 129.05/129.05 (~P3(a1,a15,f6(a5))),
% 129.05/129.05 inference(scs_inference,[],[9370,9296,9307,9235,9351,8348,7905,7994,7771,3898,41,44,48,47])).
% 129.05/129.05 cnf(9389,plain,
% 129.05/129.05 (~P2(a1,a10,f3(a10,a10))),
% 129.05/129.05 inference(scs_inference,[],[9370,9296,9307,9235,9351,8348,7905,7994,7771,3898,41,44,48,47,40])).
% 129.05/129.05 cnf(9393,plain,
% 129.05/129.05 (P1(f13(a10))),
% 129.05/129.05 inference(scs_inference,[],[9370,9296,9307,9235,9351,9309,8348,7905,7994,7771,3898,41,44,48,47,40,46,9145])).
% 129.05/129.05 cnf(9394,plain,
% 129.05/129.05 (P2(a1,f13(a10),f13(a10))),
% 129.05/129.05 inference(scs_inference,[],[9370,9296,9307,9235,9351,9309,8348,7905,7994,7771,3898,41,44,48,47,40,46,9145,31])).
% 129.05/129.05 cnf(9396,plain,
% 129.05/129.05 (P3(a4,f13(a10),f13(a10))),
% 129.05/129.05 inference(scs_inference,[],[9370,9296,9307,9235,9351,9309,8348,7905,7994,7771,3898,41,44,48,47,40,46,9145,31,32])).
% 129.05/129.05 cnf(9400,plain,
% 129.05/129.05 (~P3(f14(f13(a10),a9),a4,a11)),
% 129.05/129.05 inference(scs_inference,[],[9393,923])).
% 129.05/129.05 cnf(9411,plain,
% 129.05/129.05 (~P2(f3(a9,a9),f6(a8),f3(a9,a9))),
% 129.05/129.05 inference(scs_inference,[],[9374,9345,8356,7982,41,44])).
% 129.05/129.05 cnf(9413,plain,
% 129.05/129.05 (~P2(f6(a8),f3(a9,a9),f3(a9,a9))),
% 129.05/129.05 inference(scs_inference,[],[9374,9345,8356,7982,41,44,40])).
% 129.05/129.05 cnf(9437,plain,
% 129.05/129.05 (P3(f3(a7,a7),f13(a8),f3(a17,a17))),
% 129.05/129.05 inference(scs_inference,[],[9387,7867,7633,21,41,48])).
% 129.05/129.05 cnf(9441,plain,
% 129.05/129.05 (~P3(f3(a5,a5),f13(a5),f14(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[9385,9387,9296,7865,7867,7633,7929,3911,21,41,48,45,47])).
% 129.05/129.05 cnf(9454,plain,
% 129.05/129.05 (~P3(f14(a4,a4),a5,f3(a5,a5))),
% 129.05/129.05 inference(scs_inference,[],[9441,8029,3911,41,46])).
% 129.05/129.05 cnf(9456,plain,
% 129.05/129.05 (~P3(a1,a4,f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[9441,9411,9345,7976,8029,3911,41,46,47])).
% 129.05/129.05 cnf(9460,plain,
% 129.05/129.05 (P2(f6(a1),f3(a8,a8),f3(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[9441,9411,9093,8266,8233,9345,7976,8029,7952,3911,41,46,47,45,43])).
% 129.05/129.05 cnf(9462,plain,
% 129.05/129.05 (~P2(f3(a1,a1),f3(a1,a1),f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[9441,9411,9413,9093,8266,8233,8399,9345,7976,8029,7952,3911,41,46,47,45,43,44])).
% 129.05/129.05 cnf(9468,plain,
% 129.05/129.05 (~P2(a5,f6(a8),a5)),
% 129.05/129.05 inference(scs_inference,[],[9454,8089,7921,41,44])).
% 129.05/129.05 cnf(9470,plain,
% 129.05/129.05 (~P3(a4,f3(a4,a4),f14(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[9454,9343,8229,8711,8089,7921,41,44,46])).
% 129.05/129.05 cnf(9472,plain,
% 129.05/129.05 (~P3(a1,f13(a8),a8)),
% 129.05/129.05 inference(scs_inference,[],[9437,9454,8227,9343,8000,8229,8711,8089,7921,41,44,46,47])).
% 129.05/129.05 cnf(9481,plain,
% 129.05/129.05 (~P3(f14(a4,a4),a4,f3(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[9470,8029,7706,41,46])).
% 129.05/129.05 cnf(9488,plain,
% 129.05/129.05 (~P3(f13(a8),f14(a8,a8),f6(a1))),
% 129.05/129.05 inference(scs_inference,[],[9456,9302,8154,7996,41,46])).
% 129.05/129.05 cnf(9499,plain,
% 129.05/129.05 (~P3(a4,f3(a8,a8),a8)),
% 129.05/129.05 inference(scs_inference,[],[9481,9001,8831,3896,41,46])).
% 129.05/129.05 cnf(9509,plain,
% 129.05/129.05 (~P2(f6(a1),a10,a1)),
% 129.05/129.05 inference(scs_inference,[],[9488,9389,9079,7771,41,44])).
% 129.05/129.05 cnf(9511,plain,
% 129.05/129.05 (P3(f3(a2,a2),a4,f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[9488,9389,9255,9079,7771,733,41,44,46])).
% 129.05/129.05 cnf(9529,plain,
% 129.05/129.05 (~P3(f3(a10,a10),f13(a5),a8)),
% 129.05/129.05 inference(scs_inference,[],[9499,8142,3911,41,45])).
% 129.05/129.05 cnf(9531,plain,
% 129.05/129.05 (~P3(f3(a4,a4),f3(a1,a1),f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[9462,9499,7988,8142,3911,7836,41,45,47])).
% 129.05/129.05 cnf(9540,plain,
% 129.05/129.05 (P3(a7,a4,a7)),
% 129.05/129.05 inference(scs_inference,[],[9531,9296,910,41,46])).
% 129.05/129.05 cnf(9542,plain,
% 129.05/129.05 (~P3(f3(a5,a5),a8,a10)),
% 129.05/129.05 inference(scs_inference,[],[9531,9266,9296,7929,19,910,41,46,47])).
% 129.05/129.05 cnf(9553,plain,
% 129.05/129.05 (P3(a8,a17,a7)),
% 129.05/129.05 inference(scs_inference,[],[9529,3755,8488,3898,41,45])).
% 129.05/129.05 cnf(9557,plain,
% 129.05/129.05 (~P3(f13(a8),a10,f3(a5,a5))),
% 129.05/129.05 inference(scs_inference,[],[9529,9509,8860,3755,8488,7905,7759,8837,836,3898,41,45,44,46])).
% 129.05/129.05 cnf(9559,plain,
% 129.05/129.05 (P3(f3(a7,a7),a4,f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[9540,9529,9509,8860,3755,8488,7905,7759,7867,8837,836,3898,41,45,44,46,48])).
% 129.05/129.05 cnf(9561,plain,
% 129.05/129.05 (~P3(a1,a4,f6(a5))),
% 129.05/129.05 inference(scs_inference,[],[9540,9529,9509,8948,9511,8860,8093,3755,8488,7905,7759,7867,8837,836,3898,41,45,44,46,48,47])).
% 129.05/129.05 cnf(9572,plain,
% 129.05/129.05 (P3(f14(a4,a4),a17,a17)),
% 129.05/129.05 inference(scs_inference,[],[9553,9542,7873,3755,8154,7952,41,43,46])).
% 129.05/129.05 cnf(9574,plain,
% 129.05/129.05 (P3(f3(a8,a8),a17,f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[9553,9542,7873,3755,8154,7867,7994,7952,41,43,46,48])).
% 129.05/129.05 cnf(9582,plain,
% 129.05/129.05 (~P3(f13(a8),a1,a8)),
% 129.05/129.05 inference(scs_inference,[],[9472,41])).
% 129.05/129.05 cnf(9584,plain,
% 129.05/129.05 (P3(a10,a17,a15)),
% 129.05/129.05 inference(scs_inference,[],[18,9472,9553,19,41,46])).
% 129.05/129.05 cnf(9586,plain,
% 129.05/129.05 (P3(f3(a10,a10),a17,f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[18,9472,9553,7598,7771,19,41,46,48])).
% 129.05/129.05 cnf(9590,plain,
% 129.05/129.05 (~P3(a1,a16,a8)),
% 129.05/129.05 inference(scs_inference,[],[18,9472,8208,9553,7939,9255,7594,7598,7771,19,41,46,48,45,47])).
% 129.05/129.05 cnf(9596,plain,
% 129.05/129.05 (P3(f14(a4,a4),a15,a15)),
% 129.05/129.05 inference(scs_inference,[],[9590,9572,8916,41,45])).
% 129.05/129.05 cnf(9600,plain,
% 129.05/129.05 (~P3(f3(a4,a4),f14(a4,a4),f14(a4,a4))),
% 129.05/129.05 inference(scs_inference,[],[9590,9572,9481,9413,8352,8916,7907,8029,7901,41,45,44,46])).
% 129.05/129.05 cnf(9617,plain,
% 129.05/129.05 (~P3(a12,a1,f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[9600,9596,8685,7594,8490,8689,41,45,46])).
% 129.05/129.05 cnf(9641,plain,
% 129.05/129.05 (~P3(a1,a15,f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[9617,8767,9389,8348,9296,7905,7771,41,44,47])).
% 129.05/129.05 cnf(9643,plain,
% 129.05/129.05 (~P2(a1,a10,a1)),
% 129.05/129.05 inference(scs_inference,[],[9617,8767,9389,8348,9296,7905,7771,41,44,47,40])).
% 129.05/129.05 cnf(9645,plain,
% 129.05/129.05 (P3(f13(a10),a10,a4)),
% 129.05/129.05 inference(scs_inference,[],[9617,8767,9389,8348,9296,7905,7771,10,41,44,47,40,38])).
% 129.05/129.05 cnf(9656,plain,
% 129.05/129.05 (P3(f3(a17,a17),a8,f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[9641,9559,9437,3896,41,46])).
% 129.05/129.05 cnf(9658,plain,
% 129.05/129.05 (~P2(f13(a10),f13(a10),f13(a10))),
% 129.05/129.05 inference(scs_inference,[],[9645,9641,9559,8613,9437,3896,41,46,47])).
% 129.05/129.05 cnf(9665,plain,
% 129.05/129.05 (~P2(a2,a10,a2)),
% 129.05/129.05 inference(scs_inference,[],[9643,9561,7690,41,44])).
% 129.05/129.05 cnf(9671,plain,
% 129.05/129.05 (~P3(a1,a8,x96711)+P2(f3(a7,a7),x96711,f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[9656,9643,9561,9540,8823,7865,7690,41,44,46,40,47])).
% 129.05/129.05 cnf(9678,plain,
% 129.05/129.05 (~P3(f13(a10),a10,a1)),
% 129.05/129.05 inference(scs_inference,[],[9557,8669,9643,9645,7905,7759,836,41,44,46])).
% 129.05/129.05 cnf(9682,plain,
% 129.05/129.05 (~P2(a1,f6(a10),a1)),
% 129.05/129.05 inference(scs_inference,[],[9658,9557,8669,9643,9645,7905,7759,9396,836,7836,41,44,46,47,40])).
% 129.05/129.05 cnf(9700,plain,
% 129.05/129.05 (~P3(a1,a4,f6(a10))),
% 129.05/129.05 inference(scs_inference,[],[9678,9665,9233,7783,8033,8160,8253,41,44,48])).
% 129.05/129.05 cnf(9725,plain,
% 129.05/129.05 (P3(f3(a7,a7),f14(a4,a4),f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[9700,9656,9437,8154,41,45])).
% 129.05/129.05 cnf(9727,plain,
% 129.05/129.05 (~P3(f13(a10),a5,a1)),
% 129.05/129.05 inference(scs_inference,[],[19,9700,9224,9656,9437,9645,8154,41,45,46])).
% 129.05/129.05 cnf(9736,plain,
% 129.05/129.05 (P3(a15,f13(a5),a7)),
% 129.05/129.05 inference(scs_inference,[],[9727,9682,9540,7651,3762,3911,41,44,46])).
% 129.05/129.05 cnf(9740,plain,
% 129.05/129.05 (P3(f14(a4,a4),a7,a7)),
% 129.05/129.05 inference(scs_inference,[],[9727,9682,9596,9540,7651,3762,3911,41,44,46,40,45])).
% 129.05/129.05 cnf(9744,plain,
% 129.05/129.05 (P3(a15,f14(a4,a4),a15)),
% 129.05/129.05 inference(scs_inference,[],[9727,9682,9586,9596,9540,7651,3762,3911,41,44,46,40,45,47,365])).
% 129.05/129.05 cnf(9748,plain,
% 129.05/129.05 (P3(f14(a4,a4),f14(a7,a7),f14(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[9740,8191])).
% 129.05/129.05 cnf(9750,plain,
% 129.05/129.05 (P3(a17,f14(a4,a4),a17)),
% 129.05/129.05 inference(scs_inference,[],[9740,8191,7511])).
% 129.05/129.05 cnf(9754,plain,
% 129.05/129.05 (P3(f3(a15,a15),f14(a4,a4),f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[9740,9744,9351,8671,8191,7511,41,46])).
% 129.05/129.05 cnf(9756,plain,
% 129.05/129.05 (~P3(a1,f14(a4,a4),a8)),
% 129.05/129.05 inference(scs_inference,[],[9740,9744,9351,8671,7590,8318,8191,7511,41,46,47])).
% 129.05/129.05 cnf(9758,plain,
% 129.05/129.05 (P3(f3(a15,a15),f13(a5),f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[9740,9744,9736,9351,8671,7590,8318,7867,7598,8191,7511,41,46,47,48])).
% 129.05/129.05 cnf(9769,plain,
% 129.05/129.05 (~P3(a1,a8,f6(a5))),
% 129.05/129.05 inference(scs_inference,[],[19,9750,9756,9117,8235,7639,7948,7807,7598,41,44,46,47])).
% 129.05/129.05 cnf(9781,plain,
% 129.05/129.05 (~P3(f13(a5),a10,f3(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[19,9769,8858,3909,41,46])).
% 129.05/129.05 cnf(9783,plain,
% 129.05/129.05 (~P3(f3(a1,a1),f14(a4,a4),a8)),
% 129.05/129.05 inference(scs_inference,[],[19,9754,9769,8320,8858,7948,3909,41,46,47])).
% 129.05/129.05 cnf(9792,plain,
% 129.05/129.05 (~P3(f14(a4,a4),f3(a1,a1),a8)),
% 129.05/129.05 inference(scs_inference,[],[9783,41])).
% 129.05/129.05 cnf(9805,plain,
% 129.05/129.05 (P3(a7,f14(a4,a4),a7)),
% 129.05/129.05 inference(scs_inference,[],[9781,9750,9553,41,46])).
% 129.05/129.05 cnf(9820,plain,
% 129.05/129.05 (~P2(f3(a15,a15),f6(a8),f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[7840,9050,7982,44])).
% 129.05/129.05 cnf(9824,plain,
% 129.05/129.05 (~P2(f6(a8),f3(a15,a15),f3(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[19,7840,9276,9050,7982,3909,44,46,40])).
% 129.05/129.05 cnf(9830,plain,
% 129.05/129.05 (~P3(a1,a5,f6(a4))),
% 129.05/129.05 inference(scs_inference,[],[19,9748,9187,7840,9276,9050,8348,8308,7982,7826,3909,44,46,40,41,47,48])).
% 129.05/129.05 cnf(9837,plain,
% 129.05/129.05 (~P2(a2,f6(a10),a2)),
% 129.05/129.05 inference(scs_inference,[],[9830,9682,7690,41,44])).
% 129.05/129.05 cnf(9839,plain,
% 129.05/129.05 (~P3(a1,a17,a8)),
% 129.05/129.05 inference(scs_inference,[],[9830,9584,9682,7653,7690,7905,41,44,47])).
% 129.05/129.05 cnf(9852,plain,
% 129.05/129.05 (~P3(a17,a1,a8)),
% 129.05/129.05 inference(scs_inference,[],[9839,41])).
% 129.05/129.05 cnf(9856,plain,
% 129.05/129.05 (P3(f14(a17,a17),f14(a4,a4),f14(a17,a17))),
% 129.05/129.05 inference(scs_inference,[],[9839,9837,9750,7629,8160,41,44,46])).
% 129.05/129.05 cnf(9858,plain,
% 129.05/129.05 (~P3(a1,f14(a4,a4),f6(a5))),
% 129.05/129.05 inference(scs_inference,[],[9839,9837,9805,9235,7838,9750,7629,8160,41,44,46,47])).
% 129.05/129.05 cnf(9860,plain,
% 129.05/129.05 (~P2(f6(a10),f3(a2,a2),f3(a2,a2))),
% 129.05/129.05 inference(scs_inference,[],[9839,9837,9805,9235,7838,9750,7629,8160,41,44,46,47,40])).
% 129.05/129.05 cnf(9867,plain,
% 129.05/129.05 (~P3(a7,a1,f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[9852,9858,3755,8689,41,46])).
% 129.05/129.05 cnf(9874,plain,
% 129.05/129.05 (~P2(a7,f6(a10),a7)),
% 129.05/129.05 inference(scs_inference,[],[9867,9682,7855,41,44])).
% 129.05/129.05 cnf(9893,plain,
% 129.05/129.05 (P3(f13(a10),a15,a17)),
% 129.05/129.05 inference(scs_inference,[],[9584,8068,9645,45])).
% 129.05/129.05 cnf(9899,plain,
% 129.05/129.05 (~P2(a18,a10,a18)),
% 129.05/129.05 inference(scs_inference,[],[9643,7651,44])).
% 129.05/129.05 cnf(9916,plain,
% 129.05/129.05 (~P3(a1,f13(a5),a5)),
% 129.05/129.05 inference(scs_inference,[],[20,9899,7619,9856,7935,8072,8029,44,46,47])).
% 129.05/129.05 cnf(9920,plain,
% 129.05/129.05 (~P3(f13(a5),a1,a5)),
% 129.05/129.05 inference(scs_inference,[],[20,9899,7619,9856,7935,8072,8029,44,46,47,40,41])).
% 129.05/129.05 cnf(9931,plain,
% 129.05/129.05 (~P3(a4,a1,f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[9582,8831,8689,46])).
% 129.05/129.05 cnf(9964,plain,
% 129.05/129.05 (P3(f14(a15,a15),f14(a4,a4),f14(a15,a15))),
% 129.05/129.05 inference(scs_inference,[],[8603,8809,7621,9744,7594,44,46])).
% 129.05/129.05 cnf(9966,plain,
% 129.05/129.05 (~P2(f14(a1,a1),a1,f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[9931,8603,8809,7621,9744,7594,8516,7964,7736,44,46,48])).
% 129.05/129.05 cnf(9975,plain,
% 129.05/129.05 (~P2(a7,a10,a7)),
% 129.05/129.05 inference(scs_inference,[],[9966,9643,7855,40,44])).
% 129.05/129.05 cnf(9979,plain,
% 129.05/129.05 (P2(f6(a7),f3(a7,a7),a7)),
% 129.05/129.05 inference(scs_inference,[],[9966,9792,7838,9643,7855,8154,8689,7867,40,44,46,43])).
% 129.05/129.05 cnf(9981,plain,
% 129.05/129.05 (~P3(f3(a1,a1),a8,f14(a8,a8))),
% 129.05/129.05 inference(scs_inference,[],[9966,9792,7838,9643,7855,8154,8689,7867,40,44,46,43,41])).
% 129.05/129.05 cnf(9991,plain,
% 129.05/129.05 (~P2(f3(a7,a7),a10,f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[9975,9979,40,44])).
% 129.05/129.05 cnf(9993,plain,
% 129.05/129.05 (~P3(a1,f13(a5),a10)),
% 129.05/129.05 inference(scs_inference,[],[9975,9979,9758,9050,40,44,47])).
% 129.05/129.05 cnf(9995,plain,
% 129.05/129.05 (~P3(a1,a8,a10)),
% 129.05/129.05 inference(scs_inference,[],[9975,9979,9758,9050,40,44,47,9671])).
% 129.05/129.05 cnf(10003,plain,
% 129.05/129.05 (~P2(a10,f3(a7,a7),f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[9991,40])).
% 129.05/129.05 cnf(10007,plain,
% 129.05/129.05 (~P2(f3(a16,a16),f6(a8),f3(a16,a16))),
% 129.05/129.05 inference(scs_inference,[],[9995,9991,7712,8628,7982,40,41,44])).
% 129.05/129.05 cnf(10011,plain,
% 129.05/129.05 (~P3(a1,f14(a4,a4),f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[9995,9991,9964,9820,7712,9754,8628,9050,8029,7982,40,41,44,46,47])).
% 129.05/129.05 cnf(10020,plain,
% 129.05/129.05 (~P2(f3(a7,a7),f6(a5),f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[10007,10011,9231,9979,40,41,44])).
% 129.05/129.05 cnf(10024,plain,
% 129.05/129.05 (~P3(f6(a1),f13(a5),a10)),
% 129.05/129.05 inference(scs_inference,[],[10007,10003,10011,9231,9179,9979,9758,9177,733,40,41,44,46,47])).
% 129.05/129.05 cnf(10026,plain,
% 129.05/129.05 (~P3(a1,a5,a4)),
% 129.05/129.05 inference(scs_inference,[],[10007,10003,10011,9231,8950,9179,9979,9758,8348,9177,3909,7836,733,40,41,44,46,47,48])).
% 129.05/129.05 cnf(10028,plain,
% 129.05/129.05 (~P2(f6(a5),f3(a7,a7),f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[10020,40])).
% 129.05/129.05 cnf(10032,plain,
% 129.05/129.05 (~P2(f3(a7,a7),f6(a10),f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[10026,10020,9874,9979,40,41,44])).
% 129.05/129.05 cnf(10034,plain,
% 129.05/129.05 (~P3(a4,a8,f3(a1,a1))),
% 129.05/129.05 inference(scs_inference,[],[10026,9981,10020,9874,8047,9979,7996,40,41,44,46])).
% 129.05/129.05 cnf(10041,plain,
% 129.05/129.05 (~P2(f6(a10),f3(a7,a7),f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[10032,40])).
% 129.05/129.05 cnf(10045,plain,
% 129.05/129.05 (~P2(a12,f6(a8),a12)),
% 129.05/129.05 inference(scs_inference,[],[10032,10024,7801,8418,7982,40,41,44])).
% 129.05/129.05 cnf(10049,plain,
% 129.05/129.05 (~P3(a1,a8,f6(a10))),
% 129.05/129.05 inference(scs_inference,[],[10032,10024,7801,7909,8418,7982,7952,40,41,44,43,9671])).
% 129.05/129.05 cnf(10061,plain,
% 129.05/129.05 (~P2(f3(a7,a7),a5,f3(a7,a7))),
% 129.05/129.05 inference(scs_inference,[],[10034,10045,8051,9979,40,41,44])).
% 129.05/129.05 cnf(10065,plain,
% 129.05/129.05 (~P3(f3(a1,a1),f14(a4,a4),f6(a8))),
% 129.05/129.05 inference(scs_inference,[],[21,10034,10045,9824,8051,8320,9754,9805,9979,8154,40,41,44,46,47])).
% 129.05/129.06 cnf(10071,plain,
% 129.05/129.06 (~P2(a5,f3(a7,a7),f3(a7,a7))),
% 129.05/129.06 inference(scs_inference,[],[10061,40])).
% 129.05/129.06 cnf(10075,plain,
% 129.05/129.06 (~P2(f3(a7,a7),a8,f3(a7,a7))),
% 129.05/129.06 inference(scs_inference,[],[10065,10061,8066,9979,40,41,44])).
% 129.05/129.06 cnf(10083,plain,
% 129.05/129.06 (~P2(a8,f3(a7,a7),f3(a7,a7))),
% 129.05/129.06 inference(scs_inference,[],[10075,40])).
% 129.05/129.06 cnf(10099,plain,
% 129.05/129.06 (~P3(a1,a8,a5)),
% 129.05/129.06 inference(scs_inference,[],[10049,10061,8758,9736,8318,41,47,9671])).
% 129.05/129.06 cnf(10106,plain,
% 129.05/129.06 (~P2(a5,f6(a10),a5)),
% 129.05/129.06 inference(scs_inference,[],[10099,9682,7921,41,44])).
% 129.05/129.06 cnf(10108,plain,
% 129.05/129.06 (~P3(f6(a1),a17,a8)),
% 129.05/129.06 inference(scs_inference,[],[10099,10083,9574,9460,9682,7921,41,44,47])).
% 129.05/129.06 cnf(10148,plain,
% 129.05/129.06 (~P3(a10,a5,a1)),
% 129.05/129.06 inference(scs_inference,[],[9993,10108,9824,7639,7598,836,3911,41,44,46])).
% 129.05/129.06 cnf(10157,plain,
% 129.05/129.06 (~P3(a5,a10,a1)),
% 129.05/129.06 inference(scs_inference,[],[10148,41])).
% 129.05/129.06 cnf(10196,plain,
% 129.05/129.06 (~P3(a1,a4,a10)),
% 129.05/129.06 inference(scs_inference,[],[9323,7905,7771,836,48])).
% 129.05/129.06 cnf(10198,plain,
% 129.05/129.06 (~P3(a4,a1,a10)),
% 129.05/129.06 inference(scs_inference,[],[9323,7905,7771,836,48,41])).
% 129.05/129.06 cnf(10202,plain,
% 129.05/129.06 (~P3(f13(a8),a1,a5)),
% 129.05/129.06 inference(scs_inference,[],[8742,9323,8388,7905,3769,7771,836,3898,48,41,44,46])).
% 129.05/129.06 cnf(10209,plain,
% 129.05/129.06 (P3(a5,a4,a5)),
% 129.05/129.06 inference(scs_inference,[],[10202,8837,836,41,46])).
% 129.05/129.06 cnf(10213,plain,
% 129.05/129.06 (~P2(a1,f14(a1,a1),a10)),
% 129.05/129.06 inference(scs_inference,[],[10198,10202,8516,8837,7964,7736,836,41,46,48,40])).
% 129.05/129.06 cnf(10220,plain,
% 129.05/129.06 (~P3(f14(a5,a5),a4,a1)),
% 129.05/129.06 inference(scs_inference,[],[10209,9920,9233,8142,8933,46,45])).
% 129.05/129.06 cnf(10231,plain,
% 129.05/129.06 (~P3(a8,a5,a1)),
% 129.05/129.06 inference(scs_inference,[],[10196,10220,10209,3769,41,46])).
% 129.05/129.06 cnf(10233,plain,
% 129.05/129.06 (~P3(a1,f3(a2,a2),f6(a10))),
% 129.05/129.06 inference(scs_inference,[],[10196,10220,9860,8183,10209,3769,7736,41,46,47])).
% 129.05/129.06 cnf(10239,plain,
% 129.05/129.06 (~P3(a5,a8,a1)),
% 129.05/129.06 inference(scs_inference,[],[10231,41])).
% 129.05/129.06 cnf(10243,plain,
% 129.05/129.06 (~P3(a1,f14(a4,a4),a5)),
% 129.05/129.06 inference(scs_inference,[],[10231,10071,9725,10099,8000,10209,3896,41,46,47])).
% 129.05/129.06 cnf(10254,plain,
% 129.05/129.06 (~P3(f6(a1),a17,f6(a5))),
% 129.05/129.06 inference(scs_inference,[],[10233,10028,8314,9574,9460,10209,7927,7952,41,46,43,47])).
% 129.05/129.06 cnf(10263,plain,
% 129.05/129.06 (~P3(a8,a5,f3(a10,a10))),
% 129.05/129.06 inference(scs_inference,[],[10243,9323,10209,3769,41,46])).
% 129.05/129.06 cnf(10265,plain,
% 129.05/129.06 (P3(f3(a5,a5),a4,f3(a5,a5))),
% 129.05/129.06 inference(scs_inference,[],[10243,9323,10209,3769,7929,41,46,48])).
% 129.05/129.06 cnf(10274,plain,
% 129.05/129.06 (~P3(f13(a8),f14(a10,a10),a1)),
% 129.05/129.06 inference(scs_inference,[],[10254,10157,7767,8837,41,46])).
% 129.05/129.06 cnf(10298,plain,
% 129.05/129.06 (P2(f6(a5),f3(a5,a5),a5)),
% 129.05/129.06 inference(scs_inference,[],[10274,9916,7807,7921,10209,7929,3911,41,46,43])).
% 129.05/129.06 cnf(10307,plain,
% 129.05/129.06 (~P3(a1,a15,a8)),
% 129.05/129.06 inference(scs_inference,[],[10263,9893,7688,9394,41,47])).
% 129.05/129.06 cnf(10311,plain,
% 129.05/129.06 (~P3(a8,f14(a5,a5),a1)),
% 129.05/129.06 inference(scs_inference,[],[10263,10148,9893,7688,8809,7791,9394,7927,3769,41,47,44,46])).
% 129.05/129.06 cnf(10320,plain,
% 129.05/129.06 (~P3(a4,f3(a5,a5),a5)),
% 129.05/129.06 inference(scs_inference,[],[9271,10307,10298,10265,8860,7954,41,44,46])).
% 129.05/129.06 cnf(10322,plain,
% 129.05/129.06 (~P3(f6(a1),f13(a5),f6(a10))),
% 129.05/129.06 inference(scs_inference,[],[9271,10307,10298,10265,10041,8860,7954,9179,9758,41,44,46,47])).
% 129.05/129.06 cnf(10333,plain,
% 129.05/129.06 (~P3(a1,f3(a5,a5),f6(a5))),
% 129.05/129.06 inference(scs_inference,[],[10322,10320,10106,10298,7954,7736,41,44,48])).
% 129.05/129.06 cnf(10343,plain,
% 129.05/129.06 (~P3(a4,a10,a1)),
% 129.05/129.06 inference(scs_inference,[],[10333,10239,8504,19,41,46])).
% 129.05/129.06 cnf(10356,plain,
% 129.05/129.06 (P3(a10,a16,a12)),
% 129.05/129.06 inference(scs_inference,[],[10343,9468,10298,3748,9177,3769,41,44,46])).
% 129.05/129.06 cnf(10368,plain,
% 129.05/129.06 (P3(f13(a10),a12,a16)),
% 129.05/129.06 inference(scs_inference,[],[10356,10311,9208,10298,1490,9645,41,44,45])).
% 129.05/129.06 cnf(10492,plain,
% 129.05/129.06 (P2(f6(a8),f3(a8,a8),a8)),
% 129.05/129.06 inference(scs_inference,[],[9557,10265,9645,7773,7994,7982,46,43])).
% 129.05/129.06 cnf(10494,plain,
% 129.05/129.06 (~P3(f6(a1),f14(a4,a4),a8)),
% 129.05/129.06 inference(scs_inference,[],[10083,9725,9557,10265,8201,9645,7773,7994,7982,46,43,47])).
% 129.05/129.06 cnf(10503,plain,
% 129.05/129.06 (~P3(f6(a1),a4,a5)),
% 129.05/129.06 inference(scs_inference,[],[10494,10071,9559,8201,41,47])).
% 129.05/129.06 cnf(10591,plain,
% 129.05/129.06 (~P3(f14(a4,a4),f6(a1),f6(a8))),
% 129.05/129.06 inference(scs_inference,[],[9824,9179,9754,47,41])).
% 129.05/129.06 cnf(10596,plain,
% 129.05/129.06 (~P2(f6(a1),a10,f3(a10,a10))),
% 129.05/129.06 inference(scs_inference,[],[9307,9079,7771,44])).
% 129.05/129.06 cnf(10609,plain,
% 129.05/129.06 (~P2(f6(a8),f3(a8,a8),f3(a8,a8))),
% 129.05/129.06 inference(scs_inference,[],[10591,8862,8334,10492,7830,44,46,41,40])).
% 129.05/129.06 cnf(10637,plain,
% 129.05/129.06 (~P2(a8,a10,a8)),
% 129.05/129.06 inference(scs_inference,[],[9643,7982,44])).
% 129.05/129.06 cnf(10653,plain,
% 129.05/129.06 (~P2(f3(a8,a8),a8,f3(a8,a8))),
% 129.05/129.06 inference(scs_inference,[],[10637,10609,9511,9309,10492,7994,3898,44,46,43])).
% 129.05/129.06 cnf(10666,plain,
% 129.05/129.06 (~P2(f6(a1),a10,f6(a1))),
% 129.05/129.06 inference(scs_inference,[],[10653,10596,9079,7771,40,44])).
% 129.05/129.06 cnf(10705,plain,
% 129.05/129.06 (~P3(a11,a4,f14(f13(a10),a9))),
% 129.05/129.06 inference(scs_inference,[],[10666,9400,153,7919,7706,9682,8877,3774,3814,33,26,31,40,32,28,29,36,7525,38,35,34,45,44,46])).
% 129.05/129.06 cnf(10778,plain,
% 129.05/129.06 (~P3(f6(a10),a4,a1)),
% 129.05/129.06 inference(scs_inference,[],[285,277,3909,7736,7952,8933,8253,8504,49,7830,9682,3774,8089,8033,8397,7783,9323,7984,10503,10705,40,41,766,804,38,43,46,45,44,47,48])).
% 129.05/129.06 cnf(10820,plain,
% 129.05/129.06 (P2(a8,f6(a8),a1)),
% 129.05/129.06 inference(scs_inference,[],[7982,40])).
% 129.05/129.06 cnf(10926,plain,
% 129.05/129.06 (~P2(a10,f6(a10),f6(a10))),
% 129.05/129.06 inference(scs_inference,[],[8516,7830,8253,8220,7773,9394,9266,9658,9931,41,40,45,44,43])).
% 129.05/129.06 cnf(10935,plain,
% 129.05/129.06 (P3(a10,f13(a10),a4)),
% 129.05/129.06 inference(scs_inference,[],[9645,41])).
% 129.05/129.06 cnf(10937,plain,
% 129.05/129.06 (P2(a10,f6(a10),a1)),
% 129.05/129.06 inference(scs_inference,[],[9645,7759,41,40])).
% 129.05/129.06 cnf(10981,plain,
% 129.05/129.06 (~P2(a5,f6(a7),f6(a7))),
% 129.05/129.06 inference(scs_inference,[],[7830,8348,7692,9979,8083,8350,9499,41,40,45,43])).
% 129.05/129.06 cnf(11317,plain,
% 129.05/129.06 (P3(f6(a10),a4,f6(a10))),
% 129.05/129.06 inference(scs_inference,[],[8212,7686,40,41])).
% 129.05/129.06 cnf(11323,plain,
% 129.05/129.06 (~P3(a4,f6(a10),a1)),
% 129.05/129.06 inference(scs_inference,[],[8212,7686,10820,8210,7970,10926,10778,40,41,44,43,46])).
% 129.05/129.06 cnf(11348,plain,
% 129.05/129.06 (~P3(a15,f13(a10),a17)),
% 129.05/129.06 inference(scs_inference,[],[16,15,25,7736,7830,8253,7759,8212,8210,10368,10926,8266,10778,10213,11317,11323,10981,10937,40,41,44,45,43,46,47,48])).
% 129.05/129.06 cnf(11380,plain,
% 129.05/129.06 ($false),
% 129.05/129.06 inference(scs_inference,[],[10492,8498,8233,7584,10820,8916,5345,8282,8053,11348,10935,40,41,44,43,46]),
% 129.05/129.06 ['proof']).
% 129.05/129.06 % SZS output end Proof
% 129.05/129.06 % Total time :128.360000s
%------------------------------------------------------------------------------