%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD069-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n015.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:36 EDT 2024
% Result : Unsatisfiable 152.87s 153.50s
% Output : CNFRefutation 152.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : FLD069-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.00/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.10/0.29 % Computer : n015.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Wed Jun 19 11:51:24 EDT 2024
% 0.10/0.29 % CPUTime :
% 0.15/0.48 start to proof:theBenchmark
% 152.87/153.49 %-------------------------------------------
% 152.87/153.49 % File :CSE---1.7
% 152.87/153.49 % Problem :theBenchmark
% 152.87/153.49 % Transform :cnf
% 152.87/153.49 % Format :tptp:raw
% 152.87/153.49 % Command :java -jar mcs_scs.jar %d %s
% 152.87/153.49
% 152.87/153.49 % Result :Theorem 152.370000s
% 152.87/153.49 % Output :CNFRefutation 152.370000s
% 152.87/153.49 %-------------------------------------------
% 152.87/153.49 %--------------------------------------------------------------------------
% 152.87/153.49 % File : FLD069-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 152.87/153.49 % Domain : Field Theory (Ordered fields)
% 152.87/153.49 % Problem : If b > 0 and a >= 0, then a + b not 0
% 152.87/153.49 % Version : [Dra93] axioms : Especial.
% 152.87/153.50 % Theorem formulation : Functional with glxx axiom set.
% 152.87/153.50 % English :
% 152.87/153.50
% 152.87/153.50 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 152.87/153.50 % Source : [Dra93]
% 152.87/153.50 % Names :
% 152.87/153.50
% 152.87/153.50 % Status : Unsatisfiable
% 152.87/153.50 % Rating : 0.00 v7.5.0, 0.17 v7.4.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.20 v5.2.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.14 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.29 v3.4.0, 0.25 v3.3.0, 0.33 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0, 0.20 v2.3.0, 0.33 v2.2.1, 0.67 v2.1.0
% 152.87/153.50 % Syntax : Number of clauses : 33 ( 9 unt; 3 nHn; 33 RR)
% 152.87/153.50 % Number of literals : 79 ( 0 equ; 45 neg)
% 152.87/153.50 % Maximal clause size : 4 ( 2 avg)
% 152.87/153.50 % Maximal term depth : 3 ( 1 avg)
% 152.87/153.50 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 152.87/153.50 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 152.87/153.50 % Number of variables : 50 ( 0 sgn)
% 152.87/153.50 % SPC : CNF_UNS_RFO_NEQ_NHN
% 152.87/153.50
% 152.87/153.50 % Comments :
% 152.87/153.50 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 152.87/153.50 %--------------------------------------------------------------------------
% 152.87/153.50 include('Axioms/FLD001-0.ax').
% 152.87/153.50 %--------------------------------------------------------------------------
% 152.87/153.50 cnf(a_is_defined,hypothesis,
% 152.87/153.50 defined(a) ).
% 152.87/153.50
% 152.87/153.50 cnf(b_is_defined,hypothesis,
% 152.87/153.50 defined(b) ).
% 152.87/153.50
% 152.87/153.50 cnf(less_or_equal_3,negated_conjecture,
% 152.87/153.50 less_or_equal(additive_identity,a) ).
% 152.87/153.50
% 152.87/153.50 cnf(less_or_equal_4,negated_conjecture,
% 152.87/153.50 less_or_equal(additive_identity,b) ).
% 152.87/153.50
% 152.87/153.50 cnf(b_not_equal_to_additive_identity_5,negated_conjecture,
% 152.87/153.50 ~ equalish(b,additive_identity) ).
% 152.87/153.50
% 152.87/153.50 cnf(add_equals_additive_identity_6,negated_conjecture,
% 152.87/153.50 equalish(add(a,b),additive_identity) ).
% 152.87/153.50
% 152.87/153.50 %--------------------------------------------------------------------------
% 152.87/153.50 %-------------------------------------------
% 152.87/153.50 % Proof found
% 152.87/153.50 % SZS status Theorem for theBenchmark
% 152.87/153.50 % SZS output start Proof
% 152.87/153.50 %ClaNum:33(EqnAxiom:0)
% 152.87/153.50 %VarNum:128(SingletonVarNum:50)
% 152.87/153.50 %MaxLitNum:4
% 152.87/153.50 %MaxfuncDepth:2
% 152.87/153.50 %SharedTerms:14
% 152.87/153.50 %goalClause: 5 6 7 9
% 152.87/153.50 %singleGoalClaCount:4
% 152.87/153.50 [1]P1(a1)
% 152.87/153.50 [2]P1(a4)
% 152.87/153.50 [3]P1(a2)
% 152.87/153.50 [4]P1(a5)
% 152.87/153.50 [5]P2(a1,a2)
% 152.87/153.50 [6]P2(a1,a5)
% 152.87/153.50 [8]~P3(a1,a4)
% 152.87/153.50 [9]~P3(a5,a1)
% 152.87/153.50 [7]P3(f3(a2,a5),a1)
% 152.87/153.50 [11]~P1(x111)+P3(x111,x111)
% 152.87/153.50 [10]~P1(x101)+P1(f6(x101))
% 152.87/153.50 [15]~P1(x151)+P3(f3(a1,x151),x151)
% 152.87/153.50 [16]~P1(x161)+P3(f8(a4,x161),x161)
% 152.87/153.50 [19]~P1(x191)+P3(f3(x191,f6(x191)),a1)
% 152.87/153.50 [13]~P3(x132,x131)+P3(x131,x132)
% 152.87/153.50 [12]~P1(x121)+P3(x121,a1)+P1(f7(x121))
% 152.87/153.50 [24]~P1(x241)+P3(x241,a1)+P3(f8(x241,f7(x241)),a4)
% 152.87/153.50 [21]~P2(x212,x211)+~P2(x211,x212)+P3(x211,x212)
% 152.87/153.50 [17]~P1(x172)+~P1(x171)+P1(f3(x171,x172))
% 152.87/153.50 [18]~P1(x182)+~P1(x181)+P1(f8(x181,x182))
% 152.87/153.50 [25]~P2(a1,x252)+~P2(a1,x251)+P2(a1,f8(x251,x252))
% 152.87/153.50 [26]~P1(x262)+~P1(x261)+P3(f3(x261,x262),f3(x262,x261))
% 152.87/153.50 [27]~P1(x272)+~P1(x271)+P3(f8(x271,x272),f8(x272,x271))
% 152.87/153.50 [20]~P3(x201,x203)+P3(x201,x202)+~P3(x203,x202)
% 152.87/153.50 [22]~P2(x223,x222)+P2(x221,x222)+~P3(x223,x221)
% 152.87/153.50 [23]~P2(x231,x233)+P2(x231,x232)+~P2(x233,x232)
% 152.87/153.50 [28]~P1(x282)+~P3(x281,x283)+P3(f3(x281,x282),f3(x283,x282))
% 152.87/153.50 [29]~P1(x292)+~P3(x291,x293)+P3(f8(x291,x292),f8(x293,x292))
% 152.87/153.50 [30]~P1(x302)+~P2(x301,x303)+P2(f3(x301,x302),f3(x303,x302))
% 152.87/153.50 [14]P2(x142,x141)+~P1(x141)+~P1(x142)+P2(x141,x142)
% 152.87/153.50 [31]~P1(x313)+~P1(x312)+~P1(x311)+P3(f3(x311,f3(x312,x313)),f3(f3(x311,x312),x313))
% 152.87/153.50 [32]~P1(x323)+~P1(x322)+~P1(x321)+P3(f8(x321,f8(x322,x323)),f8(f8(x321,x322),x323))
% 152.87/153.50 [33]~P1(x333)+~P1(x332)+~P1(x331)+P3(f3(f8(x331,x332),f8(x333,x332)),f8(f3(x331,x333),x332))
% 152.87/153.50 %EqnAxiom
% 152.87/153.50
% 152.87/153.50 %-------------------------------------------
% 152.87/153.51 cnf(34,plain,
% 152.87/153.51 (~P3(a1,a5)),
% 152.87/153.51 inference(scs_inference,[],[9,13])).
% 152.87/153.51 cnf(36,plain,
% 152.87/153.51 (~P2(a5,a1)),
% 152.87/153.51 inference(scs_inference,[],[6,9,13,21])).
% 152.87/153.51 cnf(37,plain,
% 152.87/153.51 (~P2(x371,x372)+P3(x371,x372)+~P2(x372,x371)),
% 152.87/153.51 inference(rename_variables,[],[21])).
% 152.87/153.51 cnf(38,plain,
% 152.87/153.51 (~P3(a5,f3(a2,a5))),
% 152.87/153.51 inference(scs_inference,[],[6,9,7,13,21,20])).
% 152.87/153.51 cnf(40,plain,
% 152.87/153.51 (P2(a1,a1)),
% 152.87/153.51 inference(scs_inference,[],[6,9,7,1,13,21,20,14])).
% 152.87/153.51 cnf(42,plain,
% 152.87/153.51 (P3(a1,a2)+~P2(a2,a1)),
% 152.87/153.51 inference(scs_inference,[],[5,6,9,7,1,13,21,20,14,37])).
% 152.87/153.51 cnf(46,plain,
% 152.87/153.51 (~P3(f3(a2,a5),a5)),
% 152.87/153.51 inference(scs_inference,[],[38,13])).
% 152.87/153.51 cnf(48,plain,
% 152.87/153.51 (P3(a1,a1)),
% 152.87/153.51 inference(scs_inference,[],[38,40,13,21])).
% 152.87/153.51 cnf(50,plain,
% 152.87/153.51 (P2(a4,a4)),
% 152.87/153.51 inference(scs_inference,[],[38,2,40,13,21,14])).
% 152.87/153.51 cnf(52,plain,
% 152.87/153.51 (~P2(f3(a2,a5),x521)+P2(a1,x521)),
% 152.87/153.51 inference(scs_inference,[],[7,38,2,40,13,21,14,22])).
% 152.87/153.51 cnf(54,plain,
% 152.87/153.51 (~P3(a4,a1)),
% 152.87/153.51 inference(scs_inference,[],[8,13])).
% 152.87/153.51 cnf(58,plain,
% 152.87/153.51 (P2(a2,a2)),
% 152.87/153.51 inference(scs_inference,[],[3,8,50,13,21,14])).
% 152.87/153.51 cnf(60,plain,
% 152.87/153.51 (P3(a2,a2)),
% 152.87/153.51 inference(scs_inference,[],[58,21])).
% 152.87/153.51 cnf(62,plain,
% 152.87/153.52 (P2(a5,a5)),
% 152.87/153.52 inference(scs_inference,[],[58,4,21,14])).
% 152.87/153.52 cnf(64,plain,
% 152.87/153.52 (P3(a5,a5)),
% 152.87/153.52 inference(scs_inference,[],[62,21])).
% 152.87/153.52 cnf(66,plain,
% 152.87/153.52 (P1(f6(f7(a5)))),
% 152.87/153.52 inference(scs_inference,[],[9,4,10,12])).
% 152.87/153.52 cnf(73,plain,
% 152.87/153.52 (P3(f3(a1,f6(a1)),f6(a1))),
% 152.87/153.52 inference(scs_inference,[],[1,15,10])).
% 152.87/153.52 cnf(74,plain,
% 152.87/153.52 (~P3(x741,f3(a1,f6(a1)))+P3(x741,f6(a1))),
% 152.87/153.52 inference(scs_inference,[],[73,20])).
% 152.87/153.52 cnf(76,plain,
% 152.87/153.52 (~P3(a1,f3(a1,f6(a1)))+P2(f6(a1),a2)),
% 152.87/153.52 inference(scs_inference,[],[5,73,20,22])).
% 152.87/153.52 cnf(79,plain,
% 152.87/153.52 (P3(f8(a4,f6(a4)),f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[2,16,10])).
% 152.87/153.52 cnf(87,plain,
% 152.87/153.52 (~P1(f6(a1))+P2(f6(a1),f3(a2,f6(a1)))),
% 152.87/153.52 inference(scs_inference,[],[5,73,22,30])).
% 152.87/153.52 cnf(92,plain,
% 152.87/153.52 (P3(f3(f6(a1),f6(f6(a1))),a1)),
% 152.87/153.52 inference(scs_inference,[],[1,19,10])).
% 152.87/153.52 cnf(99,plain,
% 152.87/153.52 (P2(a1,f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[4,58,52,30])).
% 152.87/153.52 cnf(102,plain,
% 152.87/153.52 (~P2(f3(a2,a5),a1)+P3(f3(a2,a5),f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[7,99,21,20])).
% 152.87/153.52 cnf(111,plain,
% 152.87/153.52 (~P3(f3(a1,f6(a1)),a1)+P2(f6(a1),a2)),
% 152.87/153.52 inference(scs_inference,[],[76,13])).
% 152.87/153.52 cnf(124,plain,
% 152.87/153.52 (~P3(a4,f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[54,7,20])).
% 152.87/153.52 cnf(133,plain,
% 152.87/153.52 (~P3(a1,f3(a2,a5))+P3(f3(a2,a5),f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[40,102,22])).
% 152.87/153.52 cnf(152,plain,
% 152.87/153.52 (P2(a1,f8(a2,a2))),
% 152.87/153.52 inference(scs_inference,[],[5,40,25,23])).
% 152.87/153.52 cnf(192,plain,
% 152.87/153.52 (P3(f3(a1,f6(a4)),f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[2,10,15])).
% 152.87/153.52 cnf(193,plain,
% 152.87/153.52 (~P3(x1931,f3(a1,f6(a4)))+P3(x1931,f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[192,20])).
% 152.87/153.52 cnf(198,plain,
% 152.87/153.52 (~P1(f3(a1,f6(a4)))+P3(f8(a4,f3(a1,f6(a4))),f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[193,16])).
% 152.87/153.52 cnf(205,plain,
% 152.87/153.52 (~P1(f6(a4))+P3(f8(a4,f3(a1,f6(a4))),f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[1,198,17])).
% 152.87/153.52 cnf(206,plain,
% 152.87/153.52 (P3(f6(a4),f8(a4,f3(a1,f6(a4))))+~P1(f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[205,13])).
% 152.87/153.52 cnf(213,plain,
% 152.87/153.52 (P1(f6(f3(a4,a4)))),
% 152.87/153.52 inference(scs_inference,[],[2,10,17])).
% 152.87/153.52 cnf(214,plain,
% 152.87/153.52 (P2(f6(f3(a4,a4)),f6(f3(a4,a4)))),
% 152.87/153.52 inference(scs_inference,[],[213,14])).
% 152.87/153.52 cnf(216,plain,
% 152.87/153.52 (P3(f3(a1,f6(a2)),f6(a2))),
% 152.87/153.52 inference(scs_inference,[],[3,10,15])).
% 152.87/153.52 cnf(219,plain,
% 152.87/153.52 (~P3(x2191,f3(a1,f6(a2)))+P3(x2191,f6(a2))),
% 152.87/153.52 inference(scs_inference,[],[214,216,21,20])).
% 152.87/153.52 cnf(224,plain,
% 152.87/153.52 (~P1(f3(a1,f6(a2)))+P3(f8(a4,f3(a1,f6(a2))),f6(a2))),
% 152.87/153.52 inference(scs_inference,[],[219,16])).
% 152.87/153.52 cnf(225,plain,
% 152.87/153.52 (~P2(f3(a1,f6(a2)),x2251)+P2(f6(a2),x2251)),
% 152.87/153.52 inference(scs_inference,[],[216,22])).
% 152.87/153.52 cnf(235,plain,
% 152.87/153.52 (~P1(f6(a2))+P3(f8(a4,f3(a1,f6(a2))),f6(a2))),
% 152.87/153.52 inference(scs_inference,[],[1,224,17])).
% 152.87/153.52 cnf(236,plain,
% 152.87/153.52 (P3(f6(a2),f8(a4,f3(a1,f6(a2))))+~P1(f6(a2))),
% 152.87/153.52 inference(scs_inference,[],[235,13])).
% 152.87/153.52 cnf(251,plain,
% 152.87/153.52 (P3(f3(f6(a4),f6(f6(a4))),a1)),
% 152.87/153.52 inference(scs_inference,[],[2,10,19])).
% 152.87/153.52 cnf(252,plain,
% 152.87/153.52 (~P3(a5,f3(f6(a4),f6(f6(a4))))),
% 152.87/153.52 inference(scs_inference,[],[9,251,20])).
% 152.87/153.52 cnf(260,plain,
% 152.87/153.52 (P1(f6(f3(a2,a2)))),
% 152.87/153.52 inference(scs_inference,[],[3,10,17])).
% 152.87/153.52 cnf(263,plain,
% 152.87/153.52 (P1(f6(f8(a4,a4)))),
% 152.87/153.52 inference(scs_inference,[],[2,10,18])).
% 152.87/153.52 cnf(271,plain,
% 152.87/153.52 (P1(f6(f8(a2,a2)))),
% 152.87/153.52 inference(scs_inference,[],[3,10,18])).
% 152.87/153.52 cnf(277,plain,
% 152.87/153.52 (P2(f6(a1),f3(a2,f6(a1)))),
% 152.87/153.52 inference(scs_inference,[],[1,10,87])).
% 152.87/153.52 cnf(322,plain,
% 152.87/153.52 (P3(f6(a4),f8(a4,f3(a1,f6(a4))))),
% 152.87/153.52 inference(scs_inference,[],[2,10,206])).
% 152.87/153.52 cnf(323,plain,
% 152.87/153.52 (~P2(f6(a4),x3231)+P2(f8(a4,f3(a1,f6(a4))),x3231)),
% 152.87/153.52 inference(scs_inference,[],[322,22])).
% 152.87/153.52 cnf(405,plain,
% 152.87/153.52 (P3(f6(a2),f8(a4,f3(a1,f6(a2))))),
% 152.87/153.52 inference(scs_inference,[],[3,10,236])).
% 152.87/153.52 cnf(406,plain,
% 152.87/153.52 (~P2(f6(a2),x4061)+P2(f8(a4,f3(a1,f6(a2))),x4061)),
% 152.87/153.52 inference(scs_inference,[],[405,22])).
% 152.87/153.52 cnf(432,plain,
% 152.87/153.52 (P1(f6(f7(a4)))),
% 152.87/153.52 inference(scs_inference,[],[54,2,10,12])).
% 152.87/153.52 cnf(440,plain,
% 152.87/153.52 (P1(f3(f6(a4),f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[2,10,17])).
% 152.87/153.52 cnf(441,plain,
% 152.87/153.52 (P2(f3(f6(a4),f6(a4)),f3(f6(a4),f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[440,14])).
% 152.87/153.52 cnf(443,plain,
% 152.87/153.52 (P2(f3(a2,f6(f6(f7(a5)))),f3(a2,f6(f6(f7(a5)))))),
% 152.87/153.52 inference(scs_inference,[],[66,58,10,30])).
% 152.87/153.52 cnf(446,plain,
% 152.87/153.52 (P3(f3(f3(a2,a5),f6(a4)),f3(a1,f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[2,7,10,28])).
% 152.87/153.52 cnf(447,plain,
% 152.87/153.52 (P3(f3(f3(a2,a5),f6(a4)),f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[192,446,20])).
% 152.87/153.52 cnf(457,plain,
% 152.87/153.52 (~P2(f3(f3(a2,a5),f6(a4)),x4571)+P2(f8(a4,f3(a1,f6(a4))),x4571)),
% 152.87/153.52 inference(scs_inference,[],[447,22,323])).
% 152.87/153.52 cnf(462,plain,
% 152.87/153.52 (~P3(x4621,f3(f3(a2,a5),f6(a4)))+P3(x4621,f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[447,20])).
% 152.87/153.52 cnf(467,plain,
% 152.87/153.52 (~P3(x4671,f3(f3(a2,a5),f6(a4)))+P3(x4671,f3(a1,f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[446,20])).
% 152.87/153.52 cnf(533,plain,
% 152.87/153.52 (P2(f3(a1,f6(a4)),f3(a2,f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[2,5,10,30])).
% 152.87/153.52 cnf(534,plain,
% 152.87/153.52 (P2(f6(a4),f3(a2,f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[192,533,22])).
% 152.87/153.52 cnf(574,plain,
% 152.87/153.52 (P3(f3(f3(f6(a1),f6(f6(a1))),f6(a4)),f3(a1,f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[2,92,10,28])).
% 152.87/153.52 cnf(652,plain,
% 152.87/153.52 (P3(f7(a5),f7(a5))),
% 152.87/153.52 inference(scs_inference,[],[9,4,11,12])).
% 152.87/153.52 cnf(664,plain,
% 152.87/153.52 (P3(f3(a2,a2),f3(a2,a2))),
% 152.87/153.52 inference(scs_inference,[],[3,11,28])).
% 152.87/153.52 cnf(673,plain,
% 152.87/153.52 (P3(f3(a2,a5),f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[7,13,133])).
% 152.87/153.52 cnf(676,plain,
% 152.87/153.52 (~P2(a5,f3(a2,a5))+~P2(f3(a2,a5),a5)),
% 152.87/153.52 inference(scs_inference,[],[46,673,22,21])).
% 152.87/153.52 cnf(732,plain,
% 152.87/153.52 (P2(f3(a2,a5),a2)),
% 152.87/153.52 inference(scs_inference,[],[7,5,13,22])).
% 152.87/153.52 cnf(741,plain,
% 152.87/153.52 (P3(a4,f3(a1,a4))),
% 152.87/153.52 inference(scs_inference,[],[2,13,15])).
% 152.87/153.52 cnf(742,plain,
% 152.87/153.52 (P2(f3(a1,a4),a4)),
% 152.87/153.52 inference(scs_inference,[],[50,741,22])).
% 152.87/153.52 cnf(767,plain,
% 152.87/153.52 (P3(a4,f8(a4,a4))),
% 152.87/153.52 inference(scs_inference,[],[2,13,16])).
% 152.87/153.52 cnf(866,plain,
% 152.87/153.52 (P3(f3(a1,f6(a2)),f3(a1,f6(a2)))),
% 152.87/153.52 inference(scs_inference,[],[216,13,20])).
% 152.87/153.52 cnf(874,plain,
% 152.87/153.52 (P3(a1,f3(a4,f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[2,13,19])).
% 152.87/153.52 cnf(875,plain,
% 152.87/153.52 (P2(f3(a4,f6(a4)),a2)),
% 152.87/153.52 inference(scs_inference,[],[5,874,22])).
% 152.87/153.52 cnf(900,plain,
% 152.87/153.52 (P3(f6(a4),f3(f3(a2,a5),f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[446,13,193])).
% 152.87/153.52 cnf(901,plain,
% 152.87/153.52 (P2(f3(f3(a2,a5),f6(a4)),f3(a2,f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[534,900,22])).
% 152.87/153.52 cnf(903,plain,
% 152.87/153.52 (P3(f8(a4,f6(a4)),f3(f3(a2,a5),f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[534,79,900,22,20])).
% 152.87/153.52 cnf(917,plain,
% 152.87/153.52 (~P3(x9171,f8(a4,f6(a4)))+P3(x9171,f3(f3(a2,a5),f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[903,20])).
% 152.87/153.52 cnf(929,plain,
% 152.87/153.52 (~P1(f6(a4))+P3(f8(f6(a4),a4),f3(f3(a2,a5),f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[2,917,27])).
% 152.87/153.52 cnf(932,plain,
% 152.87/153.52 (P3(f8(f6(a4),a4),f6(a4))+~P1(f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[929,462])).
% 152.87/153.52 cnf(933,plain,
% 152.87/153.52 (P3(f6(a4),f8(f6(a4),a4))+~P1(f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[932,13])).
% 152.87/153.52 cnf(984,plain,
% 152.87/153.52 (P2(f3(a4,f6(a4)),a5)),
% 152.87/153.52 inference(scs_inference,[],[6,874,22])).
% 152.87/153.52 cnf(992,plain,
% 152.87/153.52 (P3(f3(a4,f6(a4)),a5)+~P2(a5,f3(a4,f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[984,21])).
% 152.87/153.52 cnf(997,plain,
% 152.87/153.52 (~P2(a5,f3(a4,f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[34,874,992,20])).
% 152.87/153.52 cnf(1007,plain,
% 152.87/153.52 (P2(f3(a4,f6(a4)),a1)),
% 152.87/153.52 inference(scs_inference,[],[40,874,22])).
% 152.87/153.52 cnf(1016,plain,
% 152.87/153.52 (P2(f3(a4,f6(a4)),f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[99,1007,23])).
% 152.87/153.52 cnf(1031,plain,
% 152.87/153.52 (~P2(x10311,f3(a4,f6(a4)))+P2(x10311,f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[1016,23])).
% 152.87/153.52 cnf(1041,plain,
% 152.87/153.52 (~P1(f6(a4))+P2(f3(f3(a1,a4),f6(a4)),f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[742,1031,30])).
% 152.87/153.52 cnf(1044,plain,
% 152.87/153.52 (P2(f3(f3(a1,a4),f6(a4)),a2)+~P1(f6(a4))),
% 152.87/153.52 inference(scs_inference,[],[732,1041,23])).
% 152.87/153.52 cnf(1045,plain,
% 152.87/153.52 (P2(f3(f3(a1,a4),f6(a4)),a2)),
% 152.87/153.52 inference(scs_inference,[],[2,1044,10])).
% 152.87/153.52 cnf(1114,plain,
% 152.87/153.52 (P3(f3(a1,a4),f3(f3(a2,a5),a4))),
% 152.87/153.52 inference(scs_inference,[],[7,2,13,28])).
% 152.87/153.52 cnf(1115,plain,
% 152.87/153.52 (P2(f3(f3(a2,a5),a4),a4)),
% 152.87/153.52 inference(scs_inference,[],[742,1114,22])).
% 152.87/153.52 cnf(1117,plain,
% 152.87/153.52 (P3(a4,f3(f3(a2,a5),a4))),
% 152.87/153.52 inference(scs_inference,[],[742,741,1114,22,20])).
% 152.87/153.52 cnf(1150,plain,
% 152.87/153.52 (P3(f6(a2),f3(a1,f6(a2)))),
% 152.87/153.52 inference(scs_inference,[],[866,13,219])).
% 152.87/153.52 cnf(1168,plain,
% 152.87/153.52 (P3(f8(a1,a4),f8(f3(a2,a5),a4))),
% 152.87/153.52 inference(scs_inference,[],[7,2,13,29])).
% 152.87/153.52 cnf(1177,plain,
% 152.87/153.52 (~P3(x11771,f8(a1,a4))+P3(x11771,f8(f3(a2,a5),a4))),
% 152.87/153.52 inference(scs_inference,[],[1168,20])).
% 152.87/153.52 cnf(1183,plain,
% 152.87/153.52 (P3(f8(f3(a2,a5),a4),x11831)+~P3(x11831,f8(a1,a4))),
% 152.87/153.52 inference(scs_inference,[],[1177,13])).
% 152.87/153.52 cnf(1318,plain,
% 152.87/153.52 (P1(f7(a5))),
% 152.87/153.52 inference(scs_inference,[],[34,4,13,12])).
% 152.87/153.52 cnf(1319,plain,
% 152.87/153.52 (P2(f7(a5),f7(a5))),
% 152.87/153.52 inference(scs_inference,[],[1318,14])).
% 152.87/153.52 cnf(1321,plain,
% 152.87/153.52 (P2(f3(a2,a5),a5)),
% 152.87/153.52 inference(scs_inference,[],[7,6,13,22])).
% 152.87/153.52 cnf(1322,plain,
% 152.87/153.52 (~P2(a5,f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[1321,676])).
% 152.87/153.52 cnf(1328,plain,
% 152.87/153.52 (P3(f8(a5,f7(a5)),a4)),
% 152.87/153.52 inference(scs_inference,[],[34,4,13,24])).
% 152.87/153.52 cnf(1329,plain,
% 152.87/153.52 (~P3(a1,f8(a5,f7(a5)))),
% 152.87/153.52 inference(scs_inference,[],[8,1328,20])).
% 152.87/153.52 cnf(1331,plain,
% 152.87/153.52 (~P3(f8(a5,f7(a5)),a1)),
% 152.87/153.52 inference(scs_inference,[],[8,1328,20,13])).
% 152.87/153.52 cnf(1395,plain,
% 152.87/153.52 (P3(f8(a4,a4),f8(a4,a4))),
% 152.87/153.52 inference(scs_inference,[],[2,13,27])).
% 152.87/153.52 cnf(1398,plain,
% 152.87/153.52 (P3(f8(f8(a4,a4),a4),f8(a4,f8(a4,a4)))),
% 152.87/153.52 inference(scs_inference,[],[2,13,32])).
% 152.87/153.52 cnf(1407,plain,
% 152.87/153.52 (~P3(x14071,f8(f8(a4,a4),a4))+P3(x14071,f8(a4,f8(a4,a4)))),
% 152.87/153.52 inference(scs_inference,[],[1398,20])).
% 152.87/153.52 cnf(1517,plain,
% 152.87/153.52 (P3(f8(a5,f7(a5)),f3(a1,a4))),
% 152.87/153.52 inference(scs_inference,[],[1328,741,20])).
% 152.87/153.52 cnf(1520,plain,
% 152.87/153.52 (P3(f8(a5,f7(a5)),f8(a4,a4))),
% 152.87/153.52 inference(scs_inference,[],[1328,767,20])).
% 152.87/153.52 cnf(1522,plain,
% 152.87/153.52 (P3(f8(a5,f7(a5)),f3(f3(a2,a5),a4))),
% 152.87/153.52 inference(scs_inference,[],[1328,1117,20])).
% 152.87/153.52 cnf(1542,plain,
% 152.87/153.52 (~P3(a1,f8(a4,a4))),
% 152.87/153.52 inference(scs_inference,[],[1520,1329,13,20])).
% 152.87/153.52 cnf(1543,plain,
% 152.87/153.52 (~P3(f8(a4,a4),a1)),
% 152.87/153.52 inference(scs_inference,[],[1542,13])).
% 152.87/153.52 cnf(1548,plain,
% 152.87/153.52 (~P3(f8(a4,a4),f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[1542,7,13,20])).
% 152.87/153.52 cnf(1573,plain,
% 152.87/153.52 (~P2(a2,a1)+P3(f3(a1,a5),f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[4,42,28])).
% 152.87/153.52 cnf(1574,plain,
% 152.87/153.52 (~P2(a2,f3(a4,f6(a4)))+P3(f3(a1,a5),f3(a2,a5))),
% 152.87/153.52 inference(scs_inference,[],[1007,1573,23])).
% 152.87/153.52 cnf(1575,plain,
% 152.87/153.52 (~P2(a2,f3(a4,f6(a4)))+P3(f3(a2,a5),f3(a1,a5))),
% 152.87/153.52 inference(scs_inference,[],[1574,13])).
% 152.87/153.52 cnf(1576,plain,
% 152.87/153.52 (~P2(a2,f3(a4,f6(a4)))+~P3(f3(a1,a5),a5)),
% 152.87/153.52 inference(scs_inference,[],[46,1575,20])).
% 152.87/153.52 cnf(1577,plain,
% 152.87/153.52 (~P2(a2,f3(a4,f6(a4)))),
% 152.87/153.52 inference(scs_inference,[],[4,1576,15])).
% 152.87/153.52 cnf(1581,plain,
% 152.87/153.52 (P3(f3(a1,f7(a5)),f7(a5))),
% 152.87/153.52 inference(scs_inference,[],[9,4,15,12])).
% 152.87/153.52 cnf(1582,plain,
% 152.87/153.52 (~P2(f3(a1,f7(a5)),x15821)+P2(f7(a5),x15821)),
% 152.87/153.52 inference(scs_inference,[],[1581,22])).
% 152.87/153.52 cnf(1589,plain,
% 152.87/153.52 (P2(f7(a5),f3(a2,f7(a5)))),
% 152.87/153.52 inference(scs_inference,[],[5,1318,1582,30])).
% 152.87/153.52 cnf(1595,plain,
% 152.87/153.52 (~P3(x15951,f3(a1,f7(a5)))+P3(x15951,f7(a5))),
% 152.87/153.52 inference(scs_inference,[],[1581,20])).
% 152.87/153.52 cnf(1600,plain,
% 152.87/153.52 (P3(f3(f7(a5),a1),f7(a5))),
% 152.87/153.52 inference(scs_inference,[],[1,1318,1595,26])).
% 152.87/153.52 cnf(1609,plain,
% 152.87/153.52 (~P3(x16091,f3(f7(a5),a1))+P3(x16091,f7(a5))),
% 152.87/153.52 inference(scs_inference,[],[1600,20])).
% 152.87/153.52 cnf(1618,plain,
% 152.87/153.52 (P3(f7(a5),x16181)+~P3(x16181,f3(f7(a5),a1))),
% 152.87/153.52 inference(scs_inference,[],[1609,13])).
% 152.87/153.52 cnf(1620,plain,
% 152.87/153.52 (P3(f7(a5),f3(f7(a5),a1))),
% 152.87/153.52 inference(scs_inference,[],[652,1,1618,28])).
% 152.87/153.52 cnf(1673,plain,
% 152.87/153.52 (P3(f3(f3(a1,a4),a4),f3(a4,a4))),
% 152.87/153.52 inference(scs_inference,[],[2,15,28])).
% 152.87/153.52 cnf(1682,plain,
% 152.87/153.52 (~P3(x16821,f3(f3(a1,a4),a4))+P3(x16821,f3(a4,a4))),
% 152.87/153.52 inference(scs_inference,[],[1673,20])).
% 152.87/153.52 cnf(1687,plain,
% 152.87/153.52 (P3(f3(a4,a4),x16871)+~P3(x16871,f3(f3(a1,a4),a4))),
% 152.87/153.52 inference(scs_inference,[],[1682,13])).
% 152.87/153.52 cnf(1712,plain,
% 152.87/153.52 (P3(f3(a1,f3(a4,a4)),f3(a4,a4))),
% 152.87/153.52 inference(scs_inference,[],[2,15,17])).
% 152.87/153.52 cnf(1713,plain,
% 152.87/153.52 (~P2(f3(a1,f3(a4,a4)),x17131)+P2(f3(a4,a4),x17131)),
% 152.87/153.52 inference(scs_inference,[],[1712,22])).
% 152.87/153.52 cnf(1721,plain,
% 152.87/153.52 (~P3(x17211,f3(a1,f3(a4,a4)))+P3(x17211,f3(a4,a4))),
% 152.87/153.52 inference(scs_inference,[],[1712,20])).
% 152.87/153.52 cnf(1727,plain,
% 152.87/153.52 (P3(f3(a4,a4),x17271)+~P3(x17271,f3(a1,f3(a4,a4)))),
% 152.87/153.52 inference(scs_inference,[],[1721,13])).
% 152.87/153.52 cnf(1747,plain,
% 152.87/153.53 (P2(f3(f7(a5),a1),f7(a5))),
% 152.87/153.53 inference(scs_inference,[],[1319,1620,22])).
% 152.87/153.53 cnf(1791,plain,
% 152.87/153.53 (P3(f3(a1,f8(a4,a4)),f8(a4,a4))),
% 152.87/153.53 inference(scs_inference,[],[2,15,18])).
% 152.87/153.53 cnf(1792,plain,
% 152.87/153.53 (~P2(f3(a1,f8(a4,a4)),x17921)+P2(f8(a4,a4),x17921)),
% 152.87/153.53 inference(scs_inference,[],[1791,22])).
% 152.87/153.53 cnf(1826,plain,
% 152.87/153.53 (P3(f3(a1,f7(a5)),f3(f7(a5),a1))),
% 152.87/153.53 inference(scs_inference,[],[1581,1620,20])).
% 152.87/153.53 cnf(1877,plain,
% 152.87/153.53 (P3(f3(a1,f7(a4)),f7(a4))),
% 152.87/153.53 inference(scs_inference,[],[54,2,15,12])).
% 152.87/153.53 cnf(1878,plain,
% 152.87/153.53 (~P2(f3(a1,f7(a4)),x18781)+P2(f7(a4),x18781)),
% 152.87/153.53 inference(scs_inference,[],[1877,22])).
% 152.87/153.53 cnf(1886,plain,
% 152.87/153.53 (~P3(x18861,f3(a1,f7(a4)))+P3(x18861,f7(a4))),
% 152.87/153.53 inference(scs_inference,[],[1877,20])).
% 152.87/153.53 cnf(1984,plain,
% 152.87/153.53 (~P3(a1,f3(a1,f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[1542,1791,20])).
% 152.87/153.53 cnf(1986,plain,
% 152.87/153.53 (~P3(f3(a1,f8(a4,a4)),a1)),
% 152.87/153.53 inference(scs_inference,[],[1542,1791,20,13])).
% 152.87/153.53 cnf(1992,plain,
% 152.87/153.53 (P3(f3(f8(a4,a4),a4),f3(a4,a4))),
% 152.87/153.53 inference(scs_inference,[],[2,16,28])).
% 152.87/153.53 cnf(2007,plain,
% 152.87/153.53 (P3(f8(a4,f7(a5)),f7(a5))),
% 152.87/153.53 inference(scs_inference,[],[9,4,16,12])).
% 152.87/153.53 cnf(2016,plain,
% 152.87/153.53 (~P3(x20161,f8(a4,f7(a5)))+P3(x20161,f7(a5))),
% 152.87/153.53 inference(scs_inference,[],[2007,20])).
% 152.87/153.53 cnf(2022,plain,
% 152.87/153.53 (P3(f8(f7(a5),a4),f7(a5))),
% 152.87/153.53 inference(scs_inference,[],[2,1318,2016,27])).
% 152.87/153.53 cnf(2080,plain,
% 152.87/153.53 (P3(f8(a4,f7(a5)),f3(f7(a5),a1))),
% 152.87/153.53 inference(scs_inference,[],[2007,1620,20])).
% 152.87/153.53 cnf(2090,plain,
% 152.87/153.53 (~P3(x20901,f8(a4,f7(a5)))+P3(x20901,f3(f7(a5),a1))),
% 152.87/153.53 inference(scs_inference,[],[2080,20])).
% 152.87/153.53 cnf(2096,plain,
% 152.87/153.53 (P3(f8(f7(a5),a4),f3(f7(a5),a1))),
% 152.87/153.53 inference(scs_inference,[],[2022,1620,20])).
% 152.87/153.53 cnf(2113,plain,
% 152.87/153.53 (~P3(x21131,f8(a4,f7(a5)))+P3(f7(a5),x21131)),
% 152.87/153.53 inference(scs_inference,[],[2090,1618])).
% 152.87/153.53 cnf(2114,plain,
% 152.87/153.53 (P3(f7(a5),f8(f7(a5),a4))),
% 152.87/153.53 inference(scs_inference,[],[2,1318,2113,27])).
% 152.87/153.53 cnf(2117,plain,
% 152.87/153.53 (P3(f3(a1,f7(a5)),f8(f7(a5),a4))),
% 152.87/153.53 inference(scs_inference,[],[1589,1581,2114,22,20])).
% 152.87/153.53 cnf(2138,plain,
% 152.87/153.53 (~P3(x21381,f3(a1,f7(a5)))+P3(x21381,f8(f7(a5),a4))),
% 152.87/153.53 inference(scs_inference,[],[2117,20])).
% 152.87/153.53 cnf(2145,plain,
% 152.87/153.53 (P3(f3(f7(a5),a1),f8(f7(a5),a4))),
% 152.87/153.53 inference(scs_inference,[],[1,1318,2138,26])).
% 152.87/153.53 cnf(2235,plain,
% 152.87/153.53 (P3(f3(a1,a1),a1)),
% 152.87/153.53 inference(scs_inference,[],[432,1,10,15])).
% 152.87/153.53 cnf(2237,plain,
% 152.87/153.53 (P3(f8(a4,a1),a1)),
% 152.87/153.53 inference(scs_inference,[],[432,1,10,15,16])).
% 152.87/153.53 cnf(2241,plain,
% 152.87/153.53 (P3(f7(a5),f3(a1,f7(a5)))),
% 152.87/153.53 inference(scs_inference,[],[432,1826,1318,1,10,15,16,19,1618])).
% 152.87/153.53 cnf(2245,plain,
% 152.87/153.53 (P1(f3(f7(a5),f7(a5)))),
% 152.87/153.53 inference(scs_inference,[],[1517,432,1826,1318,1,10,15,16,19,1618,13,17])).
% 152.87/153.53 cnf(2247,plain,
% 152.87/153.53 (P1(f8(f7(a5),f7(a5)))),
% 152.87/153.53 inference(scs_inference,[],[1517,432,1826,1318,1,10,15,16,19,1618,13,17,18])).
% 152.87/153.53 cnf(2249,plain,
% 152.87/153.53 (P1(f7(a4))),
% 152.87/153.53 inference(scs_inference,[],[1517,432,1826,54,1318,1,2,10,15,16,19,1618,13,17,18,12])).
% 152.87/153.53 cnf(2255,plain,
% 152.87/153.53 (P3(f8(a4,f7(a4)),a4)),
% 152.87/153.53 inference(scs_inference,[],[1517,432,1826,54,1318,1,2,10,15,16,19,1618,13,17,18,12,26,27,24])).
% 152.87/153.53 cnf(2257,plain,
% 152.87/153.53 (P2(a1,f8(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[6,1517,432,1826,54,1318,1,2,10,15,16,19,1618,13,17,18,12,26,27,24,25])).
% 152.87/153.53 cnf(2261,plain,
% 152.87/153.53 (~P3(f3(a4,f6(a4)),a5)),
% 152.87/153.53 inference(scs_inference,[],[6,1517,1016,432,1826,54,1322,1318,1,2,10,15,16,19,1618,13,17,18,12,26,27,24,25,30,22])).
% 152.87/153.53 cnf(2265,plain,
% 152.87/153.53 (P3(f3(a1,f3(a1,a1)),f3(f3(a1,a1),a1))),
% 152.87/153.53 inference(scs_inference,[],[6,2145,1517,2096,1016,432,1826,54,1322,1318,1,2,10,15,16,19,1618,13,17,18,12,26,27,24,25,30,22,20,31])).
% 152.87/153.53 cnf(2269,plain,
% 152.87/153.53 (P3(f3(f8(a1,a1),f8(a1,a1)),f8(f3(a1,a1),a1))),
% 152.87/153.53 inference(scs_inference,[],[6,2145,1517,2096,1016,432,1826,54,1322,1318,1,2,10,15,16,19,1618,13,17,18,12,26,27,24,25,30,22,20,31,32,33])).
% 152.87/153.53 cnf(2271,plain,
% 152.87/153.53 (P2(f7(a5),f3(a5,f7(a5)))),
% 152.87/153.53 inference(scs_inference,[],[6,2145,1517,2096,1016,432,1826,54,1322,1318,1,2,10,15,16,19,1618,13,17,18,12,26,27,24,25,30,22,20,31,32,33,1582])).
% 152.87/153.53 cnf(2285,plain,
% 152.87/153.53 (P3(f3(a1,a5),a5)),
% 152.87/153.53 inference(scs_inference,[],[4,15])).
% 152.87/153.53 cnf(2287,plain,
% 152.87/153.53 (P3(f8(a4,f7(a4)),f7(a4))),
% 152.87/153.53 inference(scs_inference,[],[2249,4,15,16])).
% 152.87/153.53 cnf(2295,plain,
% 152.87/153.53 (P3(a1,f3(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[2249,2235,2245,2080,4,15,16,10,19,1618,13])).
% 152.87/153.53 cnf(2301,plain,
% 152.87/153.53 (P2(a1,f8(f8(a5,a5),f8(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2249,2235,2257,2245,2080,4,15,16,10,19,1618,13,29,27,25])).
% 152.87/153.53 cnf(2305,plain,
% 152.87/153.53 (P1(f8(f7(a4),f7(a4)))),
% 152.87/153.53 inference(scs_inference,[],[2249,2235,2257,2245,2080,4,15,16,10,19,1618,13,29,27,25,26,18])).
% 152.87/153.53 cnf(2317,plain,
% 152.87/153.53 (P3(f8(a4,f7(a4)),f3(f3(a2,a5),a4))),
% 152.87/153.53 inference(scs_inference,[],[6,2249,2235,2257,2271,2241,2245,2255,1117,1319,2080,1747,4,15,16,10,19,1618,13,29,27,25,26,18,17,28,30,22,23,20])).
% 152.87/153.53 cnf(2321,plain,
% 152.87/153.53 (P3(f3(f8(a5,a5),f8(a5,a5)),f8(f3(a5,a5),a5))),
% 152.87/153.53 inference(scs_inference,[],[6,2249,2235,2257,2271,2241,2245,2255,1117,1319,2080,1747,4,15,16,10,19,1618,13,29,27,25,26,18,17,28,30,22,23,20,32,33])).
% 152.87/153.53 cnf(2325,plain,
% 152.87/153.53 (P2(f7(a4),f3(a5,f7(a4)))),
% 152.87/153.53 inference(scs_inference,[],[6,2249,2235,2257,2271,2241,2245,2255,1117,1319,2080,1747,4,15,16,10,19,1618,13,29,27,25,26,18,17,28,30,22,23,20,32,33,31,1878])).
% 152.87/153.53 cnf(2327,plain,
% 152.87/153.53 (P3(f3(f3(a1,a1),f7(a4)),f7(a4))),
% 152.87/153.53 inference(scs_inference,[],[6,2249,2235,2257,2271,2241,2245,2255,1117,1319,2080,1747,4,15,16,10,19,1618,13,29,27,25,26,18,17,28,30,22,23,20,32,33,31,1878,1886])).
% 152.87/153.53 cnf(2335,plain,
% 152.87/153.53 (P3(f8(a4,a5),a5)),
% 152.87/153.53 inference(scs_inference,[],[4,16])).
% 152.87/153.53 cnf(2337,plain,
% 152.87/153.53 (P3(f3(a1,a2),a2)),
% 152.87/153.53 inference(scs_inference,[],[4,3,16,15])).
% 152.87/153.53 cnf(2341,plain,
% 152.87/153.53 (P3(f3(a1,f6(a1)),a1)),
% 152.87/153.53 inference(scs_inference,[],[2305,1,4,3,16,15,10,19])).
% 152.87/153.53 cnf(2343,plain,
% 152.87/153.53 (P3(a1,f8(a4,a1))),
% 152.87/153.53 inference(scs_inference,[],[2237,2305,1,4,3,16,15,10,19,13])).
% 152.87/153.53 cnf(2345,plain,
% 152.87/153.53 (P2(a1,f8(f8(a2,a2),f8(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[2237,2305,152,1,4,3,16,15,10,19,13,25])).
% 152.87/153.53 cnf(2347,plain,
% 152.87/153.53 (P3(f8(a1,a1),f8(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[2237,2305,152,1,4,3,16,15,10,19,13,25,27])).
% 152.87/153.53 cnf(2351,plain,
% 152.87/153.53 (P1(f8(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[2237,2305,152,2249,1,4,3,16,15,10,19,13,25,27,29,18])).
% 152.87/153.53 cnf(2353,plain,
% 152.87/153.53 (P3(f3(a5,a5),f3(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[2237,2305,152,2249,1,4,3,16,15,10,19,13,25,27,29,18,26])).
% 152.87/153.53 cnf(2355,plain,
% 152.87/153.53 (P1(f3(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[2237,2305,152,2249,1,4,3,16,15,10,19,13,25,27,29,18,26,17])).
% 152.87/153.53 cnf(2357,plain,
% 152.87/153.53 (P3(f3(f8(a4,a1),f7(a4)),f3(a1,f7(a4)))),
% 152.87/153.53 inference(scs_inference,[],[2237,2305,152,2249,1,4,3,16,15,10,19,13,25,27,29,18,26,17,28])).
% 152.87/153.53 cnf(2359,plain,
% 152.87/153.53 (P2(f3(a1,a1),f3(a5,a1))),
% 152.87/153.53 inference(scs_inference,[],[6,2237,2305,152,2249,1,4,3,16,15,10,19,13,25,27,29,18,26,17,28,30])).
% 152.87/153.53 cnf(2363,plain,
% 152.87/153.53 (P3(f8(a4,a1),f3(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[6,2237,2295,2305,152,2249,1,4,3,16,15,10,19,13,25,27,29,18,26,17,28,30,22,20])).
% 152.87/153.53 cnf(2365,plain,
% 152.87/153.53 (P3(f8(a2,f8(a2,a2)),f8(f8(a2,a2),a2))),
% 152.87/153.53 inference(scs_inference,[],[6,2237,2295,2305,152,2249,1,4,3,16,15,10,19,13,25,27,29,18,26,17,28,30,22,20,32])).
% 152.87/153.53 cnf(2367,plain,
% 152.87/153.53 (P3(f3(f8(a2,a2),f8(a2,a2)),f8(f3(a2,a2),a2))),
% 152.87/153.53 inference(scs_inference,[],[6,2237,2295,2305,152,2249,1,4,3,16,15,10,19,13,25,27,29,18,26,17,28,30,22,20,32,33])).
% 152.87/153.53 cnf(2369,plain,
% 152.87/153.53 (P3(f3(a2,f3(a2,a2)),f3(f3(a2,a2),a2))),
% 152.87/153.53 inference(scs_inference,[],[6,2237,2295,2305,152,2249,1,4,3,16,15,10,19,13,25,27,29,18,26,17,28,30,22,20,32,33,31])).
% 152.87/153.53 cnf(2371,plain,
% 152.87/153.53 (P3(f3(f8(a4,a1),f7(a4)),f7(a4))),
% 152.87/153.53 inference(scs_inference,[],[6,2237,2295,2305,152,2249,1,4,3,16,15,10,19,13,25,27,29,18,26,17,28,30,22,20,32,33,31,1886])).
% 152.87/153.53 cnf(2378,plain,
% 152.87/153.53 (P2(f6(a1),a2)),
% 152.87/153.53 inference(scs_inference,[],[2341,111])).
% 152.87/153.53 cnf(2384,plain,
% 152.87/153.53 (P3(f3(a1,f3(a1,a1)),f3(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[2355,15])).
% 152.87/153.53 cnf(2386,plain,
% 152.87/153.53 (P3(f8(a4,f3(a1,a1)),f3(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[2355,15,16])).
% 152.87/153.53 cnf(2388,plain,
% 152.87/153.53 (P1(f6(f3(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2355,15,16,10])).
% 152.87/153.53 cnf(2392,plain,
% 152.87/153.53 (P3(f3(a1,a1),f8(a4,a1))),
% 152.87/153.53 inference(scs_inference,[],[2355,2363,15,16,10,19,13])).
% 152.87/153.53 cnf(2394,plain,
% 152.87/153.53 (P2(a1,f8(f3(a2,a5),f3(a2,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2355,2363,99,15,16,10,19,13,25])).
% 152.87/153.53 cnf(2396,plain,
% 152.87/153.53 (P1(f8(f3(a1,a1),f3(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2355,2363,99,15,16,10,19,13,25,18])).
% 152.87/153.53 cnf(2402,plain,
% 152.87/153.53 (P1(f3(f3(a1,a1),f3(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2355,2347,2363,99,15,16,10,19,13,25,18,29,26,17])).
% 152.87/153.53 cnf(2408,plain,
% 152.87/153.53 (P2(f3(a1,f3(a1,a1)),f3(a5,f3(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[6,2355,2347,2363,99,15,16,10,19,13,25,18,29,26,17,27,28,30])).
% 152.87/153.53 cnf(2410,plain,
% 152.87/153.53 (P2(f8(a4,a1),a5)),
% 152.87/153.53 inference(scs_inference,[],[6,2355,2347,2363,2343,99,15,16,10,19,13,25,18,29,26,17,27,28,30,22])).
% 152.87/153.53 cnf(2412,plain,
% 152.87/153.53 (~P3(f8(a4,a1),f3(a1,f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[6,2355,2347,2363,2343,1984,99,15,16,10,19,13,25,18,29,26,17,27,28,30,22,20])).
% 152.87/153.53 cnf(2426,plain,
% 152.87/153.53 (P3(f8(a4,f8(a1,a1)),f8(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[2351,16])).
% 152.87/153.53 cnf(2428,plain,
% 152.87/153.53 (P3(f3(a1,f8(a1,a1)),f8(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[2351,16,15])).
% 152.87/153.53 cnf(2430,plain,
% 152.87/153.53 (P1(f6(f8(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2351,16,15,10])).
% 152.87/153.53 cnf(2432,plain,
% 152.87/153.53 (P3(f3(f8(a1,a1),f6(f8(a1,a1))),a1)),
% 152.87/153.53 inference(scs_inference,[],[2351,16,15,10,19])).
% 152.87/153.53 cnf(2434,plain,
% 152.87/153.53 (P3(a5,f3(a1,a5))),
% 152.87/153.53 inference(scs_inference,[],[2351,2285,16,15,10,19,13])).
% 152.87/153.53 cnf(2436,plain,
% 152.87/153.53 (P2(a1,f8(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[2351,2285,40,16,15,10,19,13,25])).
% 152.87/153.53 cnf(2444,plain,
% 152.87/153.53 (P1(f8(f8(a1,a1),f8(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2351,2353,2285,40,16,15,10,19,13,25,26,29,27,18])).
% 152.87/153.53 cnf(2446,plain,
% 152.87/153.53 (P1(f3(f8(a1,a1),f8(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2351,2353,2285,40,16,15,10,19,13,25,26,29,27,18,17])).
% 152.87/153.53 cnf(2450,plain,
% 152.87/153.53 (P2(f3(a1,f8(a1,a1)),f3(a5,f8(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[6,2351,2353,2285,40,16,15,10,19,13,25,26,29,27,18,17,28,30])).
% 152.87/153.53 cnf(2452,plain,
% 152.87/153.53 (P2(f8(a4,a1),f3(a5,a1))),
% 152.87/153.53 inference(scs_inference,[],[6,2351,2353,2392,2285,2359,40,16,15,10,19,13,25,26,29,27,18,17,28,30,22])).
% 152.87/153.53 cnf(2454,plain,
% 152.87/153.53 (P3(f3(a1,f3(a1,a1)),f8(a4,a1))),
% 152.87/153.53 inference(scs_inference,[],[6,2351,2353,2392,2285,2359,2384,40,16,15,10,19,13,25,26,29,27,18,17,28,30,22,20])).
% 152.87/153.53 cnf(2463,plain,
% 152.87/153.53 (P3(f3(a1,a4),a4)),
% 152.87/153.53 inference(scs_inference,[],[2,15])).
% 152.87/153.53 cnf(2465,plain,
% 152.87/153.53 (P3(f8(a4,a2),a2)),
% 152.87/153.53 inference(scs_inference,[],[3,2,15,16])).
% 152.87/153.53 cnf(2469,plain,
% 152.87/153.53 (P3(f3(a5,f6(a5)),a1)),
% 152.87/153.53 inference(scs_inference,[],[2402,4,3,2,15,16,10,19])).
% 152.87/153.53 cnf(2471,plain,
% 152.87/153.53 (P3(a5,f8(a4,a5))),
% 152.87/153.53 inference(scs_inference,[],[2335,2402,4,3,2,15,16,10,19,13])).
% 152.87/153.53 cnf(2473,plain,
% 152.87/153.53 (P2(a1,f8(f8(a1,a1),f8(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2335,2436,2402,4,3,2,15,16,10,19,13,25])).
% 152.87/153.53 cnf(2475,plain,
% 152.87/153.53 (P3(f8(a5,a5),f8(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[2335,2436,2402,4,3,2,15,16,10,19,13,25,27])).
% 152.87/153.53 cnf(2477,plain,
% 152.87/153.53 (P1(f3(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[2335,2436,2402,4,3,2,15,16,10,19,13,25,27,17])).
% 152.87/153.53 cnf(2479,plain,
% 152.87/153.53 (P1(f8(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[2335,2436,2402,4,3,2,15,16,10,19,13,25,27,17,18])).
% 152.87/153.53 cnf(2483,plain,
% 152.87/153.53 (P3(f3(f8(a4,a5),f3(a1,a1)),f3(a5,f3(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2335,2436,2402,2355,4,3,2,15,16,10,19,13,25,27,17,18,26,28])).
% 152.87/153.53 cnf(2485,plain,
% 152.87/153.53 (P2(f3(a1,a5),f3(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[6,2335,2436,2402,2355,4,3,2,15,16,10,19,13,25,27,17,18,26,28,30])).
% 152.87/153.53 cnf(2489,plain,
% 152.87/153.53 (~P3(f3(a4,f6(a4)),f8(a4,a5))),
% 152.87/153.53 inference(scs_inference,[],[6,2335,2436,2454,2402,2261,2408,2355,4,3,2,15,16,10,19,13,25,27,17,18,26,28,30,22,20])).
% 152.87/153.53 cnf(2495,plain,
% 152.87/153.53 (P3(f8(a4,f8(a5,a5)),f8(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[2479,16])).
% 152.87/153.53 cnf(2497,plain,
% 152.87/153.53 (P3(f3(a1,f8(a5,a5)),f8(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[2479,16,15])).
% 152.87/153.53 cnf(2499,plain,
% 152.87/153.53 (P1(f6(f8(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2479,16,15,10])).
% 152.87/153.53 cnf(2503,plain,
% 152.87/153.53 (P3(a2,f3(a1,a2))),
% 152.87/153.53 inference(scs_inference,[],[2479,2337,16,15,10,19,13])).
% 152.87/153.53 cnf(2505,plain,
% 152.87/153.53 (P3(f8(f3(a1,a4),f8(a5,a5)),f8(a4,f8(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2463,2479,2337,16,15,10,19,13,29])).
% 152.87/153.53 cnf(2507,plain,
% 152.87/153.53 (P1(f3(f8(a5,a5),f8(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2463,2479,2337,16,15,10,19,13,29,17])).
% 152.87/153.53 cnf(2513,plain,
% 152.87/153.53 (P1(f8(f8(a5,a5),f8(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2463,2479,2337,16,15,10,19,13,29,17,26,27,18])).
% 152.87/153.53 cnf(2515,plain,
% 152.87/153.53 (P3(f3(f3(a1,a4),f8(a5,a5)),f3(a4,f8(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2463,2479,2337,16,15,10,19,13,29,17,26,27,18,28])).
% 152.87/153.53 cnf(2517,plain,
% 152.87/153.53 (P2(f3(a1,f8(a5,a5)),f3(a5,f8(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[6,2463,2479,2337,16,15,10,19,13,29,17,26,27,18,28,30])).
% 152.87/153.53 cnf(2519,plain,
% 152.87/153.53 (P2(a5,f3(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[6,2463,2479,2485,2337,2285,16,15,10,19,13,29,17,26,27,18,28,30,22])).
% 152.87/153.53 cnf(2521,plain,
% 152.87/153.53 (~P2(f3(a5,a5),f3(a4,f6(a4)))),
% 152.87/153.53 inference(scs_inference,[],[6,2463,2479,2485,2337,2285,997,16,15,10,19,13,29,17,26,27,18,28,30,22,23])).
% 152.87/153.53 cnf(2531,plain,
% 152.87/153.53 (P3(f3(a1,f3(a5,a5)),f3(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[2477,15])).
% 152.87/153.53 cnf(2533,plain,
% 152.87/153.53 (P3(f8(a4,f3(a5,a5)),f3(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[2477,15,16])).
% 152.87/153.53 cnf(2535,plain,
% 152.87/153.53 (P1(f6(f3(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2477,15,16,10])).
% 152.87/153.53 cnf(2537,plain,
% 152.87/153.53 (P3(f3(f3(a5,a5),f6(f3(a5,a5))),a1)),
% 152.87/153.53 inference(scs_inference,[],[2477,15,16,10,19])).
% 152.87/153.53 cnf(2539,plain,
% 152.87/153.53 (P3(a2,f8(a4,a2))),
% 152.87/153.53 inference(scs_inference,[],[2477,2465,15,16,10,19,13])).
% 152.87/153.53 cnf(2543,plain,
% 152.87/153.53 (P1(f3(f3(a5,a5),f3(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2475,2477,2465,15,16,10,19,13,29,17])).
% 152.87/153.53 cnf(2545,plain,
% 152.87/153.53 (P1(f8(f3(a5,a5),f3(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2475,2477,2465,15,16,10,19,13,29,17,18])).
% 152.87/153.53 cnf(2551,plain,
% 152.87/153.53 (P2(f3(a1,f3(a5,a5)),f3(a5,f3(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[6,2475,2477,2465,15,16,10,19,13,29,17,18,27,28,30])).
% 152.87/153.53 cnf(2555,plain,
% 152.87/153.53 (P2(a1,f3(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[6,2475,2477,2519,2471,2465,15,16,10,19,13,29,17,18,27,28,30,22,23])).
% 152.87/153.53 cnf(2557,plain,
% 152.87/153.53 (~P3(f3(a1,a1),f3(a1,f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[6,2475,2477,2519,2471,2465,2412,2363,15,16,10,19,13,29,17,18,27,28,30,22,23,20])).
% 152.87/153.53 cnf(2567,plain,
% 152.87/153.53 (P3(f8(a4,a4),a4)),
% 152.87/153.53 inference(scs_inference,[],[2,16])).
% 152.87/153.53 cnf(2569,plain,
% 152.87/153.53 (P1(f6(f6(f8(a5,a5))))),
% 152.87/153.53 inference(scs_inference,[],[2499,2,16,10])).
% 152.87/153.53 cnf(2571,plain,
% 152.87/153.53 (P3(f3(a2,f6(a2)),a1)),
% 152.87/153.53 inference(scs_inference,[],[2499,3,2,16,10,19])).
% 152.87/153.53 cnf(2573,plain,
% 152.87/153.53 (P3(f7(a4),f3(f3(a1,a1),f7(a4)))),
% 152.87/153.53 inference(scs_inference,[],[2327,2499,3,2,16,10,19,13])).
% 152.87/153.53 cnf(2575,plain,
% 152.87/153.53 (P1(f8(a2,a2))),
% 152.87/153.53 inference(scs_inference,[],[2327,2499,3,2,16,10,19,13,18])).
% 152.87/153.53 cnf(2577,plain,
% 152.87/153.53 (P1(f3(a2,a2))),
% 152.87/153.53 inference(scs_inference,[],[2327,2499,3,2,16,10,19,13,18,17])).
% 152.87/153.53 cnf(2579,plain,
% 152.87/153.53 (P3(f8(a2,a2),f8(a2,a2))),
% 152.87/153.53 inference(scs_inference,[],[2327,2499,3,2,16,10,19,13,18,17,27])).
% 152.87/153.53 cnf(2583,plain,
% 152.87/153.53 (P2(f3(a1,a2),f3(a5,a2))),
% 152.87/153.53 inference(scs_inference,[],[6,2539,2327,2499,2477,3,2,16,10,19,13,18,17,27,28,30])).
% 152.87/153.53 cnf(2589,plain,
% 152.87/153.53 (P3(f8(f3(a1,a4),f8(a5,a5)),f8(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[6,2539,2327,2495,2531,2499,2521,2505,2551,2477,3,2,16,10,19,13,18,17,27,28,30,22,23,20])).
% 152.87/153.53 cnf(2591,plain,
% 152.87/153.53 (P3(f3(a1,f8(a2,a2)),f8(a2,a2))),
% 152.87/153.53 inference(scs_inference,[],[6,2539,2327,2495,2531,2499,2521,2505,2551,2477,3,2,16,10,19,13,18,17,27,28,30,22,23,20,15])).
% 152.87/153.53 cnf(2605,plain,
% 152.87/153.53 (P3(f3(a1,f3(a2,a2)),f3(a2,a2))),
% 152.87/153.53 inference(scs_inference,[],[2575,2577,16,15])).
% 152.87/153.53 cnf(2607,plain,
% 152.87/153.53 (P1(f6(f6(f3(a5,a5))))),
% 152.87/153.53 inference(scs_inference,[],[2575,2577,2535,16,15,10])).
% 152.87/153.53 cnf(2609,plain,
% 152.87/153.53 (P3(f3(f8(a2,a2),f6(f8(a2,a2))),a1)),
% 152.87/153.53 inference(scs_inference,[],[2575,2577,2535,16,15,10,19])).
% 152.87/153.53 cnf(2611,plain,
% 152.87/153.53 (P3(f8(a5,a5),f8(f3(a1,a4),f8(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2575,2577,2589,2535,16,15,10,19,13])).
% 152.87/153.53 cnf(2615,plain,
% 152.87/153.53 (P3(f8(f8(a4,a4),f8(a2,a2)),f8(a4,f8(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[2567,2575,2577,2589,2535,16,15,10,19,13,26,29])).
% 152.87/153.53 cnf(2617,plain,
% 152.87/153.53 (P1(f8(f8(a2,a2),f8(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[2567,2575,2577,2589,2535,16,15,10,19,13,26,29,18])).
% 152.87/153.53 cnf(2619,plain,
% 152.87/153.53 (P1(f3(f8(a2,a2),f8(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[2567,2575,2577,2589,2535,16,15,10,19,13,26,29,18,17])).
% 152.87/153.53 cnf(2625,plain,
% 152.87/153.53 (P2(f3(a1,f8(a2,a2)),f3(a5,f8(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[6,2567,2575,2577,2589,2535,16,15,10,19,13,26,29,18,17,27,28,30])).
% 152.87/153.53 cnf(2627,plain,
% 152.87/153.53 (P2(a2,f3(a5,a2))),
% 152.87/153.53 inference(scs_inference,[],[6,2567,2575,2577,2583,2589,2535,2337,16,15,10,19,13,26,29,18,17,27,28,30,22])).
% 152.87/153.53 cnf(2635,plain,
% 152.87/153.53 (P3(f8(a4,f3(a2,a2)),f3(a2,a2))),
% 152.87/153.53 inference(scs_inference,[],[2577,16])).
% 152.87/153.53 cnf(2639,plain,
% 152.87/153.53 (P3(f3(f3(a2,a2),f6(f3(a2,a2))),a1)),
% 152.87/153.53 inference(scs_inference,[],[2619,2577,16,10,19])).
% 152.87/153.53 cnf(2641,plain,
% 152.87/153.53 (P3(f7(a4),f3(f8(a4,a1),f7(a4)))),
% 152.87/153.53 inference(scs_inference,[],[2371,2619,2577,16,10,19,13])).
% 152.87/153.53 cnf(2645,plain,
% 152.87/153.53 (P1(f8(f3(a2,a2),f3(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[2371,2533,2619,2521,2577,16,10,19,13,22,18])).
% 152.87/153.53 cnf(2649,plain,
% 152.87/153.53 (P1(f3(f3(a2,a2),f3(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[2503,2371,2533,2619,2521,2577,16,10,19,13,22,18,29,17])).
% 152.87/153.53 cnf(2653,plain,
% 152.87/153.53 (P2(f6(a1),f3(a5,a2))),
% 152.87/153.53 inference(scs_inference,[],[2627,2503,2371,2533,2619,2378,2521,2577,16,10,19,13,22,18,29,17,27,23])).
% 152.87/153.53 cnf(2655,plain,
% 152.87/153.53 (P3(f3(a2,f3(a2,a2)),f3(f3(a1,a2),f3(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[2627,2503,2371,2533,2619,2378,2521,2577,16,10,19,13,22,18,29,17,27,23,28])).
% 152.87/153.53 cnf(2665,plain,
% 152.87/153.53 (P3(f3(a4,f6(a4)),a1)),
% 152.87/153.53 inference(scs_inference,[],[2645,2,10,19])).
% 152.87/153.53 cnf(2667,plain,
% 152.87/153.53 (P3(a1,f3(a2,a5))),
% 152.87/153.53 inference(scs_inference,[],[7,2645,2,10,19,13])).
% 152.87/153.53 cnf(2671,plain,
% 152.87/153.53 (P1(f8(a4,a4))),
% 152.87/153.53 inference(scs_inference,[],[7,2645,2325,2573,2,10,19,13,22,18])).
% 152.87/153.53 cnf(2673,plain,
% 152.87/153.53 (P1(f3(a4,a4))),
% 152.87/153.53 inference(scs_inference,[],[7,2645,2325,2573,2,10,19,13,22,18,17])).
% 152.87/153.53 cnf(2677,plain,
% 152.87/153.53 (P2(f3(a4,f6(a4)),f3(a5,a2))),
% 152.87/153.53 inference(scs_inference,[],[7,2645,2325,2573,2627,875,2,10,19,13,22,18,17,27,23])).
% 152.87/153.53 cnf(2679,plain,
% 152.87/153.53 (~P3(a1,f8(a4,a5))),
% 152.87/153.53 inference(scs_inference,[],[7,2645,2325,2573,2489,2627,875,2,10,19,13,22,18,17,27,23,20])).
% 152.87/153.53 cnf(2681,plain,
% 152.87/153.53 (P3(f8(a4,f8(a4,a4)),f8(a4,a4))),
% 152.87/153.53 inference(scs_inference,[],[7,2645,2325,2573,2489,2627,875,2,10,19,13,22,18,17,27,23,20,16])).
% 152.87/153.53 cnf(2689,plain,
% 152.87/153.53 (P3(f8(f3(a2,a5),f8(a2,a2)),f8(a1,f8(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[7,2645,2325,2573,2489,2627,1543,875,2575,2,10,19,13,22,18,17,27,23,20,16,12,24,26,29])).
% 152.87/153.53 cnf(2693,plain,
% 152.87/153.53 (P3(f8(a4,f3(a4,a4)),f3(a4,a4))),
% 152.87/153.53 inference(scs_inference,[],[2673,16])).
% 152.87/153.53 cnf(2697,plain,
% 152.87/153.53 (P3(f3(f8(a4,a4),f6(f8(a4,a4))),a1)),
% 152.87/153.53 inference(scs_inference,[],[2671,2673,2649,16,10,19])).
% 152.87/153.53 cnf(2699,plain,
% 152.87/153.53 (P3(f8(a4,a4),f8(a4,f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2671,2673,2681,2649,16,10,19,13])).
% 152.87/153.53 cnf(2703,plain,
% 152.87/153.53 (P1(f7(f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2671,2673,2681,2649,2465,1543,1577,16,10,19,13,22,12])).
% 152.87/153.53 cnf(2705,plain,
% 152.87/153.53 (P1(f8(f8(a4,a4),f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2671,2673,2681,2649,2465,1543,1577,16,10,19,13,22,12,18])).
% 152.87/153.53 cnf(2707,plain,
% 152.87/153.53 (P3(f8(f3(a2,a5),f8(a4,a4)),f8(a1,f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[7,2671,2673,2681,2649,2465,1543,1577,16,10,19,13,22,12,18,29])).
% 152.87/153.53 cnf(2709,plain,
% 152.87/153.53 (P1(f3(f8(a4,a4),f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[7,2671,2673,2681,2649,2465,1543,1577,16,10,19,13,22,12,18,29,17])).
% 152.87/153.53 cnf(2717,plain,
% 152.87/153.53 (P3(f3(f3(a2,a5),f8(a4,a4)),f3(a1,f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[7,2667,2671,2673,2679,2681,2649,2465,2627,1045,1543,1577,16,10,19,13,22,12,18,29,17,27,23,20,28])).
% 152.87/153.53 cnf(2719,plain,
% 152.87/153.53 (P2(f3(f6(a1),f8(a4,a4)),f3(f3(a5,a2),f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[7,2667,2671,2673,2653,2679,2681,2649,2465,2627,1045,1543,1577,16,10,19,13,22,12,18,29,17,27,23,20,28,30])).
% 152.87/153.53 cnf(2730,plain,
% 152.87/153.53 (P1(f6(f7(f8(a4,a4))))),
% 152.87/153.53 inference(scs_inference,[],[2703,10])).
% 152.87/153.53 cnf(2732,plain,
% 152.87/153.53 (P3(f3(f3(a4,a4),f6(f3(a4,a4))),a1)),
% 152.87/153.53 inference(scs_inference,[],[2703,2673,10,19])).
% 152.87/153.53 cnf(2734,plain,
% 152.87/153.53 (P3(f8(a1,a1),f3(a1,f8(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2428,2703,2673,10,19,13])).
% 152.87/153.53 cnf(2736,plain,
% 152.87/153.53 (P2(a1,f3(a5,a2))),
% 152.87/153.53 inference(scs_inference,[],[2428,2677,2665,2703,2673,10,19,13,22])).
% 152.87/153.53 cnf(2738,plain,
% 152.87/153.53 (P2(a1,f8(f3(a5,a2),f3(a5,a2)))),
% 152.87/153.53 inference(scs_inference,[],[2428,2677,2665,2703,2673,10,19,13,22,25])).
% 152.87/153.53 cnf(2740,plain,
% 152.87/153.53 (P1(f8(f3(a4,a4),f3(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2428,2677,2665,2703,2673,10,19,13,22,25,18])).
% 152.87/153.53 cnf(2742,plain,
% 152.87/153.53 (P3(f8(f3(a2,a5),f3(a4,a4)),f8(a1,f3(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[7,2428,2677,2665,2703,2673,10,19,13,22,25,18,29])).
% 152.87/153.53 cnf(2744,plain,
% 152.87/153.53 (P1(f3(f3(a4,a4),f3(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[7,2428,2677,2665,2703,2673,10,19,13,22,25,18,29,17])).
% 152.87/153.53 cnf(2750,plain,
% 152.87/153.53 (P3(f3(f3(a2,a5),f3(a4,a4)),f3(a1,f3(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[7,2428,2677,2665,2703,2699,2301,1548,2673,1007,10,19,13,22,25,18,29,17,23,20,28])).
% 152.87/153.53 cnf(2762,plain,
% 152.87/153.53 (P2(f3(a2,a5),f3(a5,a2))),
% 152.87/153.53 inference(scs_inference,[],[2497,2740,2627,732,10,13,23])).
% 152.87/153.53 cnf(2764,plain,
% 152.87/153.53 (P3(f3(a1,f8(a5,a5)),f8(f3(a1,a4),f8(a5,a5)))),
% 152.87/153.53 inference(scs_inference,[],[2497,2740,2611,2627,732,10,13,23,20])).
% 152.87/153.53 cnf(2774,plain,
% 152.87/153.53 (~P3(f8(a4,f8(a4,a4)),a1)),
% 152.87/153.53 inference(scs_inference,[],[2605,2744,2699,1543,10,13,20])).
% 152.87/153.53 cnf(2782,plain,
% 152.87/153.53 (P3(f3(a1,a1),f8(a4,f3(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2386,2705,10,13])).
% 152.87/153.53 cnf(2784,plain,
% 152.87/153.53 (P3(f8(a4,f8(a1,a1)),f3(a1,f8(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2386,2426,2734,2705,10,13,20])).
% 152.87/153.53 cnf(2792,plain,
% 152.87/153.53 (P3(f7(a4),f8(a4,f7(a4)))),
% 152.87/153.53 inference(scs_inference,[],[2287,2709,10,13])).
% 152.87/153.53 cnf(2798,plain,
% 152.87/153.53 (P3(f3(f3(a2,a5),f8(a2,a2)),f3(a1,f8(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[7,2287,2557,2345,2782,2709,2575,1007,10,13,23,20,28])).
% 152.87/153.53 cnf(2806,plain,
% 152.87/153.53 (P1(f6(f8(f8(a2,a2),f8(a2,a2))))),
% 152.87/153.53 inference(scs_inference,[],[2617,10])).
% 152.87/153.53 cnf(2808,plain,
% 152.87/153.53 (P3(f3(a2,a2),f8(a4,f3(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[2635,2617,10,13])).
% 152.87/153.53 cnf(2819,plain,
% 152.87/153.53 (P3(f3(a4,a4),f8(a4,f3(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2693,2545,10,13])).
% 152.87/153.53 cnf(2831,plain,
% 152.87/153.53 (P3(a1,f3(a1,f6(a1)))),
% 152.87/153.53 inference(scs_inference,[],[2341,2543,10,13])).
% 152.87/153.53 cnf(2833,plain,
% 152.87/153.53 (P3(f7(a4),f3(f3(a2,a5),a4))),
% 152.87/153.53 inference(scs_inference,[],[2341,2792,2317,2543,10,13,20])).
% 152.87/153.53 cnf(2835,plain,
% 152.87/153.53 (P3(a1,f6(a1))),
% 152.87/153.53 inference(scs_inference,[],[2341,2792,2317,2543,10,13,20,74])).
% 152.87/153.53 cnf(2842,plain,
% 152.87/153.53 (P2(f6(a1),a2)),
% 152.87/153.53 inference(scs_inference,[],[2831,76])).
% 152.87/153.53 cnf(2844,plain,
% 152.87/153.53 (P1(f6(f3(f8(a5,a5),f8(a5,a5))))),
% 152.87/153.53 inference(scs_inference,[],[2507,10])).
% 152.87/153.53 cnf(2846,plain,
% 152.87/153.53 (P3(f6(a1),a1)),
% 152.87/153.53 inference(scs_inference,[],[2835,2507,10,13])).
% 152.87/153.53 cnf(2856,plain,
% 152.87/153.53 (P3(a1,f3(a5,f6(a5)))),
% 152.87/153.53 inference(scs_inference,[],[2469,2513,10,13])).
% 152.87/153.53 cnf(2860,plain,
% 152.87/153.53 (P3(f3(a5,f6(a5)),f6(a1))),
% 152.87/153.53 inference(scs_inference,[],[2469,2831,2513,10,13,20,74])).
% 152.87/153.53 cnf(2868,plain,
% 152.87/153.53 (P3(f6(a1),f3(a5,f6(a5)))),
% 152.87/153.53 inference(scs_inference,[],[2860,2444,10,13])).
% 152.87/153.53 cnf(2872,plain,
% 152.87/153.53 (~P3(f3(a5,f6(a5)),f8(a4,a5))),
% 152.87/153.53 inference(scs_inference,[],[2860,2394,2856,2444,2679,1007,10,13,23,20])).
% 152.87/153.53 cnf(2874,plain,
% 152.87/153.53 (P3(f3(f6(a1),f8(a4,a4)),f3(a1,f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2846,2860,2394,2856,2444,2679,2671,1007,10,13,23,20,28])).
% 152.87/153.53 cnf(2876,plain,
% 152.87/153.53 (P2(f3(f6(a1),f8(a4,a4)),f3(a2,f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2842,2846,2860,2394,2856,2444,2679,2671,1007,10,13,23,20,28,30])).
% 152.87/153.53 cnf(2885,plain,
% 152.87/153.53 (P3(a1,f3(a2,f6(a2)))),
% 152.87/153.53 inference(scs_inference,[],[2571,2388,10,13])).
% 152.87/153.53 cnf(2897,plain,
% 152.87/153.53 (P3(f3(f3(a2,a5),a4),f7(a4))),
% 152.87/153.53 inference(scs_inference,[],[2833,2396,10,13])).
% 152.87/153.53 cnf(2901,plain,
% 152.87/153.53 (~P3(f6(a1),f8(a4,a5))),
% 152.87/153.53 inference(scs_inference,[],[2872,2819,2833,2396,2860,2673,10,13,29,20])).
% 152.87/153.53 cnf(2911,plain,
% 152.87/153.53 (P3(f3(f3(a2,a5),a4),f3(f8(a4,a1),f7(a4)))),
% 152.87/153.53 inference(scs_inference,[],[2897,2641,2269,2430,10,13,20])).
% 152.87/153.53 cnf(2920,plain,
% 152.87/153.53 (P3(f3(f3(a1,a1),a1),f3(a1,f3(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2265,2446,10,13])).
% 152.87/153.53 cnf(2946,plain,
% 152.87/153.53 (P2(f8(a1,a1),f3(a5,f8(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[2321,2450,2247,2428,10,13,22])).
% 152.87/153.53 cnf(2950,plain,
% 152.87/153.53 (P2(f3(a1,f3(a4,a4)),f3(f8(f3(a5,a2),f3(a5,a2)),f3(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2738,2808,2321,2450,2247,2428,2673,10,13,22,28,30])).
% 152.87/153.53 cnf(2971,plain,
% 152.87/153.53 (P2(f3(a1,f8(a4,a4)),f3(f3(a5,a2),f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2367,2874,2719,263,10,13,22])).
% 152.87/153.53 cnf(2993,plain,
% 152.87/153.53 (P1(f6(a1))),
% 152.87/153.53 inference(scs_inference,[],[1,10])).
% 152.87/153.53 cnf(2995,plain,
% 152.87/153.53 (P3(f3(f3(a2,a2),a2),f3(a2,f3(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[1,2369,10,13])).
% 152.87/153.53 cnf(3001,plain,
% 152.87/153.53 (P1(f3(f6(a1),f6(a1)))),
% 152.87/153.53 inference(scs_inference,[],[1,2369,10,13,26,18,17])).
% 152.87/153.53 cnf(3009,plain,
% 152.87/153.53 (P2(a1,f3(a5,f8(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[1,2369,2971,2579,2946,2436,1791,10,13,26,18,17,27,22,29,23])).
% 152.87/153.53 cnf(3015,plain,
% 152.87/153.53 (P3(f8(a4,f6(a1)),f6(a1))),
% 152.87/153.53 inference(scs_inference,[],[1,2369,2971,2410,2579,2946,2436,1791,10,13,26,18,17,27,22,29,23,28,30,16])).
% 152.87/153.53 cnf(3023,plain,
% 152.87/153.53 (P1(f6(f6(a1)))),
% 152.87/153.53 inference(scs_inference,[],[2993,10])).
% 152.87/153.53 cnf(3025,plain,
% 152.87/153.53 (P3(f6(a1),f8(a4,f6(a1)))),
% 152.87/153.53 inference(scs_inference,[],[2993,3015,10,13])).
% 152.87/153.53 cnf(3044,plain,
% 152.87/153.53 (P3(f8(a5,a1),f8(a5,a1))),
% 152.87/153.53 inference(scs_inference,[],[1,3001,2365,64,10,13,29])).
% 152.87/153.53 cnf(3048,plain,
% 152.87/153.53 (~P3(f8(a4,f6(a1)),f8(a4,a5))),
% 152.87/153.53 inference(scs_inference,[],[1,3001,3025,3009,2365,2901,64,1007,10,13,29,23,20])).
% 152.87/153.53 cnf(3083,plain,
% 152.87/153.53 (~P2(f3(a5,a5),a1)),
% 152.87/153.53 inference(scs_inference,[],[1,3044,2764,2517,3023,2519,36,10,13,22,29,23])).
% 152.87/153.53 cnf(3097,plain,
% 152.87/153.53 (~P3(a1,f3(a5,a5))),
% 152.87/153.53 inference(scs_inference,[],[3083,2784,271,40,10,13,22])).
% 152.87/153.53 cnf(3107,plain,
% 152.87/153.53 (P3(f3(f3(a1,a2),f3(a2,a2)),f3(a2,f3(a2,a2)))),
% 152.87/153.53 inference(scs_inference,[],[2655,213,10,13])).
% 152.87/153.53 cnf(3109,plain,
% 152.87/153.53 (P2(f3(a1,f8(a4,a4)),f3(a2,f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2655,2876,2874,213,10,13,22])).
% 152.87/153.53 cnf(3113,plain,
% 152.87/153.53 (P3(f8(f6(a1),a1),f8(a1,a1))),
% 152.87/153.53 inference(scs_inference,[],[1,2655,2876,2846,2471,2874,252,213,10,13,22,20,29])).
% 152.87/153.53 cnf(3124,plain,
% 152.87/153.53 (P3(f8(a1,a1),f8(f6(a1),a1))),
% 152.87/153.53 inference(scs_inference,[],[3113,260,10,13])).
% 152.87/153.53 cnf(3128,plain,
% 152.87/153.53 (P3(f8(f6(a1),a1),f3(a1,f8(a1,a1)))),
% 152.87/153.53 inference(scs_inference,[],[3113,2734,2993,260,10,13,29,20])).
% 152.87/153.53 cnf(3130,plain,
% 152.87/153.53 (P3(f3(f8(f6(a1),a1),f6(a1)),f3(f8(a1,a1),f6(a1)))),
% 152.87/153.53 inference(scs_inference,[],[3113,2734,2993,260,10,13,29,20,28])).
% 152.87/153.53 cnf(3141,plain,
% 152.87/153.53 (P3(f3(a1,f8(a4,a4)),f3(f3(a2,a5),f8(a4,a4)))),
% 152.87/153.53 inference(scs_inference,[],[2717,66,10,13])).
% 152.87/153.53 cnf(3143,plain,
% 152.87/153.53 (P3(f8(a2,a1),f8(f8(a4,a2),a1))),
% 152.87/153.53 inference(scs_inference,[],[1,2717,2539,66,10,13,29])).
% 152.87/153.53 cnf(3145,plain,
% 152.87/153.53 (~P3(f3(a1,a5),f3(a2,a5))),
% 152.87/153.53 inference(scs_inference,[],[1,2717,2539,2434,38,66,10,13,29,20])).
% 152.87/153.53 cnf(3147,plain,
% 152.87/153.54 (P3(f3(a2,a1),f3(f8(a4,a2),a1))),
% 152.87/153.54 inference(scs_inference,[],[1,2717,2539,2434,38,66,10,13,29,20,28])).
% 152.87/153.54 cnf(3149,plain,
% 152.87/153.54 (P2(f3(a1,a1),f3(f3(a5,a2),a1))),
% 152.87/153.54 inference(scs_inference,[],[1,2717,2736,2539,2434,38,66,10,13,29,20,28,30])).
% 152.87/153.54 cnf(3155,plain,
% 152.87/153.54 (~P2(a2,a1)),
% 152.87/153.54 inference(scs_inference,[],[3145,1573])).
% 152.87/153.54 cnf(3156,plain,
% 152.87/153.54 (P1(f6(a5))),
% 152.87/153.54 inference(scs_inference,[],[4,10])).
% 152.87/153.54 cnf(3158,plain,
% 152.87/153.54 (P3(f3(f8(a4,a2),a1),f3(a2,a1))),
% 152.87/153.54 inference(scs_inference,[],[3147,4,10,13])).
% 152.87/153.54 cnf(3160,plain,
% 152.87/153.54 (P1(f8(f6(a5),f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[3147,4,10,13,18])).
% 152.87/153.54 cnf(3162,plain,
% 152.87/153.54 (P1(f3(f6(a5),f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[3147,4,10,13,18,17])).
% 152.87/153.54 cnf(3168,plain,
% 152.87/153.54 (P3(f3(a2,a1),f3(a2,a1))),
% 152.87/153.54 inference(scs_inference,[],[3124,3147,2993,4,10,13,18,17,27,29,20])).
% 152.87/153.54 cnf(3170,plain,
% 152.87/153.54 (P3(f3(f8(a1,a1),f6(a1)),f3(f8(f6(a1),a1),f6(a1)))),
% 152.87/153.54 inference(scs_inference,[],[3124,3147,2993,4,10,13,18,17,27,29,20,28])).
% 152.87/153.54 cnf(3174,plain,
% 152.87/153.54 (P3(f3(a1,f6(a5)),f6(a5))),
% 152.87/153.54 inference(scs_inference,[],[3124,3149,3147,2993,4,10,13,18,17,27,29,20,28,30,15])).
% 152.87/153.54 cnf(3176,plain,
% 152.87/153.54 (P3(f8(a4,f6(a5)),f6(a5))),
% 152.87/153.54 inference(scs_inference,[],[3124,3149,3147,2993,4,10,13,18,17,27,29,20,28,30,15,16])).
% 152.87/153.54 cnf(3178,plain,
% 152.87/153.54 (P3(f3(f6(a5),f6(f6(a5))),a1)),
% 152.87/153.54 inference(scs_inference,[],[3124,3149,3147,2993,4,10,13,18,17,27,29,20,28,30,15,16,19])).
% 152.87/153.54 cnf(3185,plain,
% 152.87/153.54 (P1(f6(f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[3156,10])).
% 152.87/153.54 cnf(3187,plain,
% 152.87/153.54 (P3(f6(a5),f3(a1,f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[3156,3174,10,13])).
% 152.87/153.54 cnf(3189,plain,
% 152.87/153.54 (~P3(a1,a2)),
% 152.87/153.54 inference(scs_inference,[],[3155,3156,3174,40,10,13,22])).
% 152.87/153.54 cnf(3193,plain,
% 152.87/153.54 (~P2(f3(a5,a2),a1)),
% 152.87/153.54 inference(scs_inference,[],[1,3155,3168,3156,3174,2627,40,10,13,22,29,23])).
% 152.87/153.54 cnf(3207,plain,
% 152.87/153.54 (~P2(a2,a1)),
% 152.87/153.54 inference(scs_inference,[],[3189,42])).
% 152.87/153.54 cnf(3208,plain,
% 152.87/153.54 (P1(f6(a4))),
% 152.87/153.54 inference(scs_inference,[],[2,10])).
% 152.87/153.54 cnf(3210,plain,
% 152.87/153.54 (P3(f6(a5),f8(a4,f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[2,3176,10,13])).
% 152.87/153.54 cnf(3216,plain,
% 152.87/153.54 (P3(f8(a4,f6(a5)),f3(a1,f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[2,3176,3187,3109,3141,3156,10,13,22,29,20])).
% 152.87/153.54 cnf(3218,plain,
% 152.87/153.54 (P3(f3(f8(a4,f6(a5)),f6(a5)),f3(f6(a5),f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[2,3176,3187,3109,3141,3156,10,13,22,29,20,28])).
% 152.87/153.54 cnf(3232,plain,
% 152.87/153.54 (P3(f8(f6(a4),a4),f3(f3(a2,a5),f6(a4)))),
% 152.87/153.54 inference(scs_inference,[],[3208,929])).
% 152.87/153.54 cnf(3233,plain,
% 152.87/153.54 (P3(f8(f6(a4),a4),f6(a4))),
% 152.87/153.54 inference(scs_inference,[],[3208,932])).
% 152.87/153.54 cnf(3234,plain,
% 152.87/153.54 (P3(f6(a4),f8(f6(a4),a4))),
% 152.87/153.54 inference(scs_inference,[],[3208,933])).
% 152.87/153.54 cnf(3239,plain,
% 152.87/153.54 (P2(f3(f3(a1,a4),f6(a4)),f3(a2,a5))),
% 152.87/153.54 inference(scs_inference,[],[3208,1041])).
% 152.87/153.54 cnf(3265,plain,
% 152.87/153.54 (P1(f6(f6(a4)))),
% 152.87/153.54 inference(scs_inference,[],[3208,10])).
% 152.87/153.54 cnf(3267,plain,
% 152.87/153.54 (P3(f8(f8(a4,a2),a1),f8(a2,a1))),
% 152.87/153.54 inference(scs_inference,[],[3208,3143,10,13])).
% 152.87/153.54 cnf(3269,plain,
% 152.87/153.54 (~P3(a1,f3(a5,a2))),
% 152.87/153.54 inference(scs_inference,[],[3208,3143,3193,40,10,13,22])).
% 152.87/153.54 cnf(3271,plain,
% 152.87/153.54 (P3(f8(a1,a4),f8(a1,a4))),
% 152.87/153.54 inference(scs_inference,[],[2,3208,3143,3193,48,40,10,13,22,29])).
% 152.87/153.54 cnf(3275,plain,
% 152.87/153.54 (P3(f3(a1,a4),f3(a1,a4))),
% 152.87/153.54 inference(scs_inference,[],[2,3208,3143,3193,48,1986,3141,40,10,13,22,29,20,28])).
% 152.87/153.54 cnf(3277,plain,
% 152.87/153.54 (P2(f3(f3(a2,a5),a4),f3(f3(a5,a2),a4))),
% 152.87/153.54 inference(scs_inference,[],[2,3208,3143,3193,2762,48,1986,3141,40,10,13,22,29,20,28,30])).
% 152.87/153.54 cnf(3287,plain,
% 152.87/153.54 (P3(f3(a1,f3(a4,a4)),f3(f3(a2,a5),f3(a4,a4)))),
% 152.87/153.54 inference(scs_inference,[],[3265,2750,10,13])).
% 152.87/153.54 cnf(3295,plain,
% 152.87/153.54 (P3(f3(f3(a1,a4),a4),f3(f3(a1,a4),a4))),
% 152.87/153.54 inference(scs_inference,[],[2,3275,3239,3267,3265,2750,3143,1322,10,13,22,29,20,28])).
% 152.87/153.54 cnf(3307,plain,
% 152.87/153.54 (P1(f6(f3(f6(a5),f6(a5))))),
% 152.87/153.54 inference(scs_inference,[],[3162,10])).
% 152.87/153.54 cnf(3313,plain,
% 152.87/153.54 (~P3(f3(a5,f6(a5)),f3(a5,a2))),
% 152.87/153.54 inference(scs_inference,[],[2,3269,3128,3271,3162,2856,10,13,29,20])).
% 152.87/153.54 cnf(3334,plain,
% 152.87/153.54 (P3(f3(f8(f6(a4),a4),f6(a4)),f3(f6(a4),f6(a4)))),
% 152.87/153.54 inference(scs_inference,[],[3233,3216,3160,3234,3208,10,13,29,20,28])).
% 152.87/153.54 cnf(3345,plain,
% 152.87/153.54 (P3(f8(f3(a4,f6(a4)),a4),f8(a1,a4))),
% 152.87/153.54 inference(scs_inference,[],[2,2911,3185,2665,10,13,29])).
% 152.87/153.54 cnf(3347,plain,
% 152.87/153.54 (~P3(f6(a1),f3(a5,a2))),
% 152.87/153.54 inference(scs_inference,[],[2,3313,2911,3185,2665,2860,10,13,29,20])).
% 152.87/153.54 cnf(3366,plain,
% 152.87/153.54 (P1(f6(a2))),
% 152.87/153.54 inference(scs_inference,[],[3,10])).
% 152.87/153.54 cnf(3368,plain,
% 152.87/153.54 (P3(f8(a4,f8(a2,a2)),f8(f8(a4,a4),f8(a2,a2)))),
% 152.87/153.54 inference(scs_inference,[],[2615,3,10,13])).
% 152.87/153.54 cnf(3372,plain,
% 152.87/153.54 (P1(f3(f6(a2),f6(a2)))),
% 152.87/153.54 inference(scs_inference,[],[2615,3,10,13,26,17])).
% 152.87/153.54 cnf(3374,plain,
% 152.87/153.54 (P1(f8(f6(a2),f6(a2)))),
% 152.87/153.54 inference(scs_inference,[],[2615,3,10,13,26,17,18])).
% 152.87/153.54 cnf(3382,plain,
% 152.87/153.54 (~P2(f3(a5,a2),f6(a1))),
% 152.87/153.54 inference(scs_inference,[],[3347,3158,2615,3277,2897,2653,3208,3,10,13,26,17,18,27,22,29,21])).
% 152.87/153.54 cnf(3388,plain,
% 152.87/153.54 (P3(f8(a4,f6(a2)),f6(a2))),
% 152.87/153.54 inference(scs_inference,[],[3347,3158,2995,2615,3277,2897,2369,2653,3208,3,10,13,26,17,18,27,22,29,21,20,28,16])).
% 152.87/153.54 cnf(3398,plain,
% 152.87/153.54 (P1(f6(f6(a2)))),
% 152.87/153.54 inference(scs_inference,[],[3366,10])).
% 152.87/153.54 cnf(3400,plain,
% 152.87/153.54 (P3(f6(a2),f8(a4,f6(a2)))),
% 152.87/153.54 inference(scs_inference,[],[3366,3388,10,13])).
% 152.87/153.54 cnf(3402,plain,
% 152.87/153.54 (P3(f8(f3(a1,f6(a1)),a4),f8(a1,a4))),
% 152.87/153.54 inference(scs_inference,[],[2,3366,3388,2341,10,13,29])).
% 152.87/153.54 cnf(3406,plain,
% 152.87/153.54 (P3(f3(f3(a1,f6(a1)),a4),f3(a1,a4))),
% 152.87/153.54 inference(scs_inference,[],[2,3366,3388,3189,2341,2885,10,13,29,20,28])).
% 152.87/153.54 cnf(3421,plain,
% 152.87/153.54 (P3(f8(f6(a5),f6(a2)),f8(f8(a4,f6(a5)),f6(a2)))),
% 152.87/153.54 inference(scs_inference,[],[3372,3210,2689,3366,10,13,29])).
% 152.87/153.54 cnf(3429,plain,
% 152.87/153.54 (~P3(x34291,f3(a5,a2))+~P2(x34291,f6(a1))),
% 152.87/153.54 inference(scs_inference,[],[2,3382,3372,3210,3368,2689,2359,2615,3366,10,13,29,20,28,30,22])).
% 152.87/153.54 cnf(3442,plain,
% 152.87/153.54 (P3(f8(f3(a2,f6(a2)),a4),f8(a1,a4))),
% 152.87/153.54 inference(scs_inference,[],[2,3287,2707,2950,3374,2571,10,13,22,29])).
% 152.87/153.54 cnf(3444,plain,
% 152.87/153.54 (~P3(f6(a1),f3(a5,a5))),
% 152.87/153.54 inference(scs_inference,[],[2,3287,2707,2950,3374,3097,2571,2835,10,13,22,29,20])).
% 152.87/153.54 cnf(3446,plain,
% 152.87/153.54 (P3(f3(f3(a2,f6(a2)),a4),f3(a1,a4))),
% 152.87/153.54 inference(scs_inference,[],[2,3287,2707,2950,3374,3097,2571,2835,10,13,22,29,20,28])).
% 152.87/153.54 cnf(3459,plain,
% 152.87/153.54 (P3(f3(f3(a1,a1),a1),f3(a1,a1))),
% 152.87/153.54 inference(scs_inference,[],[3400,2920,2742,3398,2384,3366,10,13,29,20])).
% 152.87/153.54 cnf(3469,plain,
% 152.87/153.54 (P3(f3(a1,a1),f3(f3(a1,a1),a1))),
% 152.87/153.54 inference(scs_inference,[],[3459,13])).
% 152.87/153.54 cnf(3473,plain,
% 152.87/153.54 (P3(f8(f8(a4,f7(a4)),a2),f8(a4,a2))),
% 152.87/153.54 inference(scs_inference,[],[3,3459,2325,2255,2833,13,22,29])).
% 152.87/153.54 cnf(3477,plain,
% 152.87/153.54 (P3(f3(f8(a4,f7(a4)),a2),f3(a4,a2))),
% 152.87/153.54 inference(scs_inference,[],[3,3444,3459,2325,2255,2833,2868,13,22,29,20,28])).
% 152.87/153.54 cnf(3481,plain,
% 152.87/153.54 (P3(a2,a1)+P1(f7(a2))),
% 152.87/153.54 inference(scs_inference,[],[3,3444,3459,2325,2255,2833,2868,13,22,29,20,28,21,12])).
% 152.87/153.54 cnf(3485,plain,
% 152.87/153.54 (P3(f8(f3(a1,a1),f6(a2)),f8(f3(f3(a1,a1),a1),f6(a2)))),
% 152.87/153.54 inference(scs_inference,[],[3469,2483,3366,13,29])).
% 152.87/153.54 cnf(3487,plain,
% 152.87/153.54 (~P3(f3(f3(a1,a1),a1),f3(a1,f8(a4,a4)))),
% 152.87/153.54 inference(scs_inference,[],[3469,2483,2557,3366,13,29,20])).
% 152.87/153.54 cnf(3499,plain,
% 152.87/153.54 (~P3(f3(a1,a1),f3(a5,a2))),
% 152.87/153.54 inference(scs_inference,[],[3,2515,3269,1395,2295,13,29,20])).
% 152.87/153.54 cnf(3591,plain,
% 152.87/153.54 (P2(f3(a1,a2),f3(f8(f8(a2,a2),f8(a2,a2)),a2))),
% 152.87/153.54 inference(scs_inference,[],[3,3446,2345,13,30])).
% 152.87/153.54 cnf(3602,plain,
% 152.87/153.54 (P2(a2,f3(f8(f8(a2,a2),f8(a2,a2)),a2))),
% 152.87/153.54 inference(scs_inference,[],[3473,3591,2337,13,22])).
% 152.87/153.54 cnf(3616,plain,
% 152.87/153.54 (~P3(f3(f3(a2,a5),a4),f3(a2,a5))),
% 152.87/153.54 inference(scs_inference,[],[3345,3602,3207,124,1117,13,23,20])).
% 152.87/153.54 cnf(3626,plain,
% 152.87/153.54 (P2(f3(a5,f6(a5)),f8(f3(a2,a5),f3(a2,a5)))),
% 152.87/153.54 inference(scs_inference,[],[3402,2394,2856,13,22])).
% 152.87/153.54 cnf(3628,plain,
% 152.87/153.54 (P2(f6(a1),f3(f8(f8(a2,a2),f8(a2,a2)),a2))),
% 152.87/153.54 inference(scs_inference,[],[3402,2394,3602,2842,2856,13,22,23])).
% 152.87/153.54 cnf(3636,plain,
% 152.87/153.54 (P1(f7(a2))),
% 152.87/153.54 inference(scs_inference,[],[3189,3481,13])).
% 152.87/153.54 cnf(3637,plain,
% 152.87/153.54 (P3(f7(a2),f7(a2))),
% 152.87/153.54 inference(scs_inference,[],[3636,11])).
% 152.87/153.54 cnf(3641,plain,
% 152.87/153.54 (P3(f8(a4,f7(a2)),f7(a2))),
% 152.87/153.54 inference(scs_inference,[],[3636,11,15,16])).
% 152.87/153.54 cnf(3643,plain,
% 152.87/153.54 (P3(f3(f7(a2),f6(f7(a2))),a1)),
% 152.87/153.54 inference(scs_inference,[],[3636,11,15,16,19])).
% 152.87/153.54 cnf(3645,plain,
% 152.87/153.54 (P1(f6(f7(a2)))),
% 152.87/153.54 inference(scs_inference,[],[3636,11,15,16,19,10])).
% 152.87/153.54 cnf(3653,plain,
% 152.87/153.54 (P1(f8(f7(a2),f7(a2)))),
% 152.87/153.54 inference(scs_inference,[],[3636,3406,11,15,16,19,10,13,26,17,18])).
% 152.87/153.54 cnf(3659,plain,
% 152.87/153.54 (~P3(f7(a4),f3(a2,a5))),
% 152.87/153.54 inference(scs_inference,[],[4,3636,3616,3406,60,2897,11,15,16,19,10,13,26,17,18,27,29,20])).
% 152.87/153.54 cnf(3663,plain,
% 152.87/153.54 (P2(f3(a1,a5),f3(f8(f8(a1,a1),f8(a1,a1)),a5))),
% 152.87/153.54 inference(scs_inference,[],[4,3636,3616,3626,3406,2473,60,2897,11,15,16,19,10,13,26,17,18,27,29,20,21,30])).
% 152.87/153.54 cnf(3686,plain,
% 152.87/153.54 (P3(f7(a2),f8(a4,f7(a2)))),
% 152.87/153.54 inference(scs_inference,[],[3641,3653,10,13])).
% 152.87/153.54 cnf(3694,plain,
% 152.87/153.54 (~P3(f8(a4,f7(a4)),f3(a2,a5))),
% 152.87/153.54 inference(scs_inference,[],[4,3637,3641,3653,3663,3659,2792,2285,10,13,28,22,29,20])).
% 152.87/153.54 cnf(3704,plain,
% 152.87/153.54 (P3(f3(f7(a2),f6(a4)),f3(f8(a4,f7(a2)),f6(a4)))),
% 152.87/153.54 inference(scs_inference,[],[3686,3442,3645,3208,10,13,28])).
% 152.87/153.54 cnf(3722,plain,
% 152.87/153.54 (P2(a1,f3(f8(f8(a2,a2),f8(a2,a2)),a2))),
% 152.87/153.54 inference(scs_inference,[],[4,3477,3628,664,2846,13,28,22])).
% 152.87/153.54 cnf(3795,plain,
% 152.87/153.54 (P3(f3(f6(a4),f6(a4)),f3(f8(f6(a4),a4),f6(a4)))),
% 152.87/153.54 inference(scs_inference,[],[3334,13])).
% 152.87/153.54 cnf(3824,plain,
% 152.87/153.54 (P3(f3(f6(a5),f6(a5)),f3(f8(a4,f6(a5)),f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[3218,13])).
% 152.87/153.54 cnf(3855,plain,
% 152.87/153.54 (P3(f8(f3(f3(a1,a1),a1),f6(a2)),f8(f3(a1,a1),f6(a2)))),
% 152.87/153.54 inference(scs_inference,[],[3485,13])).
% 152.87/153.54 cnf(3889,plain,
% 152.87/153.54 (P3(f8(f8(a4,f6(a5)),f6(a2)),f8(f6(a5),f6(a2)))),
% 152.87/153.54 inference(scs_inference,[],[3421,13])).
% 152.87/153.54 cnf(3919,plain,
% 152.87/153.54 (P3(f3(f8(a4,f7(a2)),f6(a4)),f3(f7(a2),f6(a4)))),
% 152.87/153.54 inference(scs_inference,[],[3704,13])).
% 152.87/153.54 cnf(3988,plain,
% 152.87/153.54 (P3(a1,f3(f8(a1,a1),f6(f8(a1,a1))))),
% 152.87/153.54 inference(scs_inference,[],[2432,13])).
% 152.87/153.54 cnf(4008,plain,
% 152.87/153.54 (P3(a1,f3(f3(a5,a5),f6(f3(a5,a5))))),
% 152.87/153.54 inference(scs_inference,[],[2537,13])).
% 152.87/153.54 cnf(4017,plain,
% 152.87/153.54 (~P3(f3(f8(a1,a1),f6(f8(a1,a1))),f8(a4,a5))),
% 152.87/153.54 inference(scs_inference,[],[2609,3988,2679,13,20])).
% 152.87/153.54 cnf(4030,plain,
% 152.87/153.54 (P2(a1,f3(a5,f8(a5,a5)))),
% 152.87/153.54 inference(scs_inference,[],[2639,2495,2611,2517,2257,2497,13,20,22,23])).
% 152.87/153.54 cnf(4045,plain,
% 152.87/153.54 (P3(a1,f3(f8(a4,a4),f6(f8(a4,a4))))),
% 152.87/153.54 inference(scs_inference,[],[2697,13])).
% 152.87/153.54 cnf(4060,plain,
% 152.87/153.54 (P3(a1,f3(f3(a4,a4),f6(f3(a4,a4))))),
% 152.87/153.54 inference(scs_inference,[],[2732,13])).
% 152.87/153.54 cnf(4071,plain,
% 152.87/153.54 (~P3(f3(f3(a5,a5),f6(f3(a5,a5))),f3(a5,a5))),
% 152.87/153.54 inference(scs_inference,[],[3178,4008,3097,13,20])).
% 152.87/153.54 cnf(4095,plain,
% 152.87/153.54 (~P3(f3(f3(a2,a5),a4),a1)),
% 152.87/153.54 inference(scs_inference,[],[3643,1522,1331,13,20])).
% 152.87/153.54 cnf(4101,plain,
% 152.87/153.54 (P3(f8(a2,a2),f3(a1,f8(a2,a2)))),
% 152.87/153.54 inference(scs_inference,[],[2591,13])).
% 152.87/153.54 cnf(4103,plain,
% 152.87/153.54 (P3(f8(a4,f6(a2)),f3(a1,f6(a2)))),
% 152.87/153.54 inference(scs_inference,[],[2591,3388,1150,13,20])).
% 152.87/153.54 cnf(4114,plain,
% 152.87/153.54 (P3(f8(f8(a2,a2),f6(a5)),f8(f3(a1,f8(a2,a2)),f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[4101,4103,4095,2911,3156,13,28,20,29])).
% 152.87/153.54 cnf(4132,plain,
% 152.87/153.54 (~P3(f7(a4),a1)),
% 152.87/153.54 inference(scs_inference,[],[4114,4095,2897,13,20])).
% 152.87/153.54 cnf(4134,plain,
% 152.87/153.54 (P1(f7(f7(a4)))),
% 152.87/153.54 inference(scs_inference,[],[4114,4095,2897,2249,13,20,12])).
% 152.87/153.54 cnf(4202,plain,
% 152.87/153.54 (P3(f3(f3(a1,a2),f3(a2,a2)),f3(f3(a2,a2),a2))),
% 152.87/153.54 inference(scs_inference,[],[3107,2798,2369,13,20])).
% 152.87/153.54 cnf(4212,plain,
% 152.87/153.54 (~P3(f8(a4,f7(a4)),a1)),
% 152.87/153.54 inference(scs_inference,[],[40,4202,4132,2792,3366,13,30,20])).
% 152.87/153.54 cnf(4214,plain,
% 152.87/153.54 (P2(f6(a2),f3(a1,f6(a2)))),
% 152.87/153.54 inference(scs_inference,[],[40,4202,4132,2792,3366,13,30,20,225])).
% 152.87/153.54 cnf(4265,plain,
% 152.87/153.54 (P2(f3(a1,f8(a4,a4)),f3(a1,f8(a4,a4)))),
% 152.87/153.54 inference(scs_inference,[],[40,2357,2671,13,30])).
% 152.87/153.54 cnf(4288,plain,
% 152.87/153.54 (P3(f3(a4,a4),f3(f8(a4,a4),a4))),
% 152.87/153.54 inference(scs_inference,[],[1992,13])).
% 152.87/153.54 cnf(4306,plain,
% 152.87/153.54 (P3(f8(f3(a4,a4),f8(a2,a2)),f8(f3(f8(a4,a4),a4),f8(a2,a2)))),
% 152.87/153.54 inference(scs_inference,[],[4288,4071,4045,2384,3269,2575,13,28,20,21,29])).
% 152.87/153.54 cnf(4332,plain,
% 152.87/153.54 (P3(f8(f3(f8(a4,a4),a4),f8(a2,a2)),f8(f3(a4,a4),f8(a2,a2)))),
% 152.87/153.54 inference(scs_inference,[],[4306,2730,574,4134,901,193,457,15,11,16,19,13])).
% 152.87/153.54 cnf(4336,plain,
% 152.87/153.54 (P2(a1,f8(f3(f8(f8(a2,a2),f8(a2,a2)),a2),f3(f8(f8(a2,a2),f8(a2,a2)),a2)))),
% 152.87/153.54 inference(scs_inference,[],[4306,2730,574,3722,4134,901,193,457,15,11,16,19,13,10,25])).
% 152.87/153.54 cnf(4348,plain,
% 152.87/153.54 (P2(f3(a1,f6(f7(f8(a4,a4)))),f3(a1,f6(f7(f8(a4,a4)))))),
% 152.87/153.54 inference(scs_inference,[],[40,4306,2730,574,3722,4134,2347,901,193,457,15,11,16,19,13,10,25,26,28,17,18,27,30])).
% 152.87/153.54 cnf(4376,plain,
% 152.87/153.54 (P3(f3(a4,a4),f3(f3(a2,a5),f3(a4,a4)))),
% 152.87/153.54 inference(scs_inference,[],[2679,2750,3109,3232,2950,13,467,1792,1713,1727])).
% 152.87/153.54 cnf(4388,plain,
% 152.87/153.54 (~P3(a5,f8(a4,a1))),
% 152.87/153.54 inference(scs_inference,[],[1007,9,2237,2679,3271,3295,2452,2473,2750,3109,3232,2950,13,467,1792,1713,1727,1721,1687,1183,23,22,20])).
% 152.87/153.54 cnf(4390,plain,
% 152.87/153.54 (P2(f7(a2),f7(a2))),
% 152.87/153.54 inference(scs_inference,[],[1007,9,3636,2237,2679,3271,3295,2452,2473,2750,3109,3232,2950,13,467,1792,1713,1727,1721,1687,1183,23,22,20,14])).
% 152.87/153.54 cnf(4420,plain,
% 152.87/153.54 (P2(f6(a2),f6(a2))),
% 152.87/153.54 inference(scs_inference,[],[1007,36,3366,216,405,2285,3659,2738,4265,3345,4214,4348,13,1792,1183,406,1886,1177,22,23,20,21,14])).
% 152.87/153.54 cnf(4448,plain,
% 152.87/153.54 (P2(f6(a1),f6(a1))),
% 152.87/153.54 inference(scs_inference,[],[1007,2993,2285,2897,34,3269,1115,4030,3402,4420,443,13,406,1183,1177,22,21,23,20,14])).
% 152.87/153.54 cnf(4534,plain,
% 152.87/153.54 (~P3(f3(a5,a2),f3(a1,a1))),
% 152.87/153.54 inference(scs_inference,[],[3499,13])).
% 152.87/153.54 cnf(4542,plain,
% 152.87/153.54 (P2(f3(a4,a4),f3(a4,a4))),
% 152.87/153.54 inference(scs_inference,[],[6,1007,79,2673,322,2835,3499,2436,13,23,22,20,14])).
% 152.87/153.54 cnf(4576,plain,
% 152.87/153.54 (P2(a1,f3(a2,f6(a1)))),
% 152.87/153.54 inference(scs_inference,[],[277,2337,3189,2846,3444,13,74,20,22])).
% 152.87/153.54 cnf(4616,plain,
% 152.87/153.54 (~P3(a5,f3(a1,f6(a1)))),
% 152.87/153.54 inference(scs_inference,[],[1007,9,2355,2846,2782,2359,4212,2555,13,20,23,22,14,74])).
% 152.87/153.54 cnf(4647,plain,
% 152.87/153.54 (P2(f3(a5,f6(a5)),a5)),
% 152.87/153.54 inference(scs_inference,[],[6,1007,2363,2782,2856,2557,4576,13,20,23,22])).
% 152.87/153.54 cnf(4661,plain,
% 152.87/153.54 (~P3(f3(f3(a1,a1),a1),f3(f3(a2,a5),f8(a4,a4)))),
% 152.87/153.54 inference(scs_inference,[],[2717,3487,4095,13,20])).
% 152.87/153.54 cnf(4679,plain,
% 152.87/153.54 (~P3(f3(a5,a2),f3(a1,f6(a1)))),
% 152.87/153.54 inference(scs_inference,[],[3347,13,74])).
% 152.87/153.54 cnf(4685,plain,
% 152.87/153.54 (P2(f3(a1,f6(a1)),a5)),
% 152.87/153.54 inference(scs_inference,[],[6,7,1007,2885,2831,3347,4336,13,74,20,23,22])).
% 152.87/153.54 cnf(4733,plain,
% 152.87/153.54 (~P3(a1,f8(a4,a2))),
% 152.87/153.54 inference(scs_inference,[],[3189,2465,4017,13,20])).
% 152.87/153.54 cnf(4804,plain,
% 152.87/153.54 (P2(f3(f6(a5),f6(a5)),f3(f6(a5),f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[2505,2611,3686,3162,3694,4390,13,20,22,14])).
% 152.87/153.54 cnf(4832,plain,
% 152.87/153.54 (~P3(a1,f8(a4,f3(a5,a5)))),
% 152.87/153.54 inference(scs_inference,[],[3097,2533,3048,13,20])).
% 152.87/153.54 cnf(4859,plain,
% 152.87/153.54 (~P3(a5,f3(a1,f3(a1,a1)))),
% 152.87/153.54 inference(scs_inference,[],[4388,2454,4733,13,20])).
% 152.87/153.54 cnf(4989,plain,
% 152.87/153.54 (~P3(a5,f3(a5,f6(a5)))),
% 152.87/153.54 inference(scs_inference,[],[9,2469,2872,13,20])).
% 152.87/153.54 cnf(5087,plain,
% 152.87/153.54 (~P3(f3(a5,a2),f3(f3(a1,a1),a1))),
% 152.87/153.54 inference(scs_inference,[],[4534,3459,2774,13,1407,20])).
% 152.87/153.54 cnf(5327,plain,
% 152.87/153.54 (P2(f6(f6(f8(a5,a5))),f6(f6(f8(a5,a5))))),
% 152.87/153.54 inference(scs_inference,[],[6,3485,4060,4685,4616,3855,2569,13,20,21,22,14])).
% 152.87/153.54 cnf(5361,plain,
% 152.87/153.54 (P2(f6(f6(f3(a5,a5))),f6(f6(f3(a5,a5))))),
% 152.87/153.54 inference(scs_inference,[],[152,2625,3421,2591,5327,4832,3889,2607,13,20,21,22,23,14])).
% 152.87/153.54 cnf(5401,plain,
% 152.87/153.54 (P2(f6(f3(f8(a5,a5),f8(a5,a5))),f6(f3(f8(a5,a5),f8(a5,a5))))),
% 152.87/153.54 inference(scs_inference,[],[1581,4542,2241,5361,4679,4376,2844,13,20,21,22,14])).
% 152.87/153.54 cnf(5433,plain,
% 152.87/153.54 (P2(f6(f8(f8(a2,a2),f8(a2,a2))),f6(f8(f8(a2,a2),f8(a2,a2))))),
% 152.87/153.54 inference(scs_inference,[],[441,3704,5401,4661,3795,3919,2806,13,20,21,22,14])).
% 152.87/153.54 cnf(5480,plain,
% 152.87/153.54 (P2(f6(f3(f6(a5),f6(a5))),f6(f3(f6(a5),f6(a5))))),
% 152.87/153.54 inference(scs_inference,[],[3334,3795,5433,4859,3824,3307,4804,13,20,21,22,14])).
% 152.87/153.54 cnf(5502,plain,
% 152.87/153.54 (~P2(f3(a2,a5),f6(a1))),
% 152.87/153.54 inference(scs_inference,[],[3,4,3429,26])).
% 152.87/153.54 cnf(5509,plain,
% 152.87/153.54 (~P2(a1,f6(a1))),
% 152.87/153.54 inference(scs_inference,[],[2667,3130,3170,4647,5502,4989,13,20,21,22])).
% 152.87/153.54 cnf(5549,plain,
% 152.87/153.54 ($false),
% 152.87/153.54 inference(scs_inference,[],[4448,2846,4306,5509,5480,5087,4332,13,20,21,22]),
% 152.87/153.54 ['proof']).
% 152.87/153.54 % SZS output end Proof
% 152.87/153.54 % Total time :152.370000s
%------------------------------------------------------------------------------