%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM027-1 : TPTP v8.2.0. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n028.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 12:23:01 EDT 2024
% Result : Unsatisfiable 63.06s 63.18s
% Output : CNFRefutation 63.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : NUM027-1 : TPTP v8.2.0. Bugfixed v4.0.0.
% 0.03/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.31 % Computer : n028.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Sat Jun 22 23:29:09 EDT 2024
% 0.10/0.31 % CPUTime :
% 0.16/0.54 start to proof:theBenchmark
% 63.06/63.17 %-------------------------------------------
% 63.06/63.17 % File :CSE---1.7
% 63.06/63.17 % Problem :theBenchmark
% 63.06/63.17 % Transform :cnf
% 63.06/63.17 % Format :tptp:raw
% 63.06/63.17 % Command :java -jar mcs_scs.jar %d %s
% 63.06/63.17
% 63.06/63.17 % Result :Theorem 62.550000s
% 63.06/63.17 % Output :CNFRefutation 62.550000s
% 63.06/63.17 %-------------------------------------------
% 63.06/63.17 %--------------------------------------------------------------------------
% 63.06/63.17 % File : NUM027-1 : TPTP v8.2.0. Bugfixed v4.0.0.
% 63.06/63.17 % Domain : Number Theory
% 63.06/63.17 % Problem : If a >= b and b*c <= a*c, then c = 0
% 63.06/63.17 % Version : [LS74] axioms : Incomplete > Reduced > Incomplete.
% 63.06/63.17 % English :
% 63.06/63.17
% 63.06/63.17 % Refs : [LS74] Lawrence & Starkey (1974), Experimental Tests of Resol
% 63.06/63.17 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 63.06/63.17 % Source : [SPRFN]
% 63.06/63.18 % Names : ls87 [LS74]
% 63.06/63.18 % : ls87 [WM76]
% 63.06/63.18
% 63.06/63.18 % Status : Unsatisfiable
% 63.06/63.18 % Rating : 0.00 v7.0.0, 0.12 v6.3.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.0
% 63.06/63.18 % Syntax : Number of clauses : 21 ( 10 unt; 2 nHn; 13 RR)
% 63.06/63.18 % Number of literals : 36 ( 0 equ; 17 neg)
% 63.06/63.18 % Maximal clause size : 3 ( 1 avg)
% 63.06/63.18 % Maximal term depth : 4 ( 1 avg)
% 63.06/63.18 % Number of predicates : 2 ( 2 usr; 0 prp; 2-2 aty)
% 63.06/63.18 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 63.06/63.18 % Number of variables : 36 ( 3 sgn)
% 63.06/63.18 % SPC : CNF_UNS_RFO_NEQ_NHN
% 63.06/63.18
% 63.06/63.18 % Comments : The surplus transitivity axiom is removed.
% 63.06/63.18 % Bugfixes : v4.0.0 - Bugfix in NUM001-0.ax
% 63.06/63.18 %--------------------------------------------------------------------------
% 63.06/63.18 %----Include recursive function + and * axioms
% 63.06/63.18 include('Axioms/NUM001-0.ax').
% 63.06/63.18 %----Include recursive function less axioms
% 63.06/63.18 include('Axioms/NUM001-1.ax').
% 63.06/63.18 %--------------------------------------------------------------------------
% 63.06/63.18 cnf(reflexivity,axiom,
% 63.06/63.18 equalish(X,X) ).
% 63.06/63.18
% 63.06/63.18 cnf(symmetry,axiom,
% 63.06/63.18 ( ~ equalish(X,Y)
% 63.06/63.18 | equalish(Y,X) ) ).
% 63.06/63.18
% 63.06/63.18 cnf(transitivity,axiom,
% 63.06/63.18 ( ~ equalish(X,Y)
% 63.06/63.18 | ~ equalish(Y,Z)
% 63.06/63.18 | equalish(X,Z) ) ).
% 63.06/63.18
% 63.06/63.18 cnf(equality_preserved_over_times,axiom,
% 63.06/63.18 ( ~ equalish(A,B)
% 63.06/63.18 | equalish(multiply(A,C),multiply(B,C)) ) ).
% 63.06/63.18
% 63.06/63.18 cnf(not_less_and_equal,axiom,
% 63.06/63.18 ( ~ less(A,B)
% 63.06/63.18 | ~ equalish(A,B) ) ).
% 63.06/63.18
% 63.06/63.18 cnf(numbers_either_less_or_equal,axiom,
% 63.06/63.18 ( less(A,B)
% 63.06/63.18 | equalish(B,A)
% 63.06/63.18 | less(B,A) ) ).
% 63.06/63.18
% 63.06/63.18 cnf(number_not_less_than_itself,axiom,
% 63.06/63.18 ~ less(A,A) ).
% 63.06/63.18
% 63.06/63.18 cnf(zero_is_the_first_number,axiom,
% 63.06/63.18 ~ equalish(successor(A),n0) ).
% 63.06/63.18
% 63.06/63.18 cnf(multiply_lemma,axiom,
% 63.06/63.18 ( ~ less(A,B)
% 63.06/63.18 | equalish(C,n0)
% 63.06/63.18 | less(multiply(A,C),multiply(B,C)) ) ).
% 63.06/63.18
% 63.06/63.18 cnf(b_not_less_than_a,hypothesis,
% 63.06/63.18 ~ less(b,a) ).
% 63.06/63.18
% 63.06/63.18 cnf(b_times_c_less_than_a_times_c,hypothesis,
% 63.06/63.18 less(multiply(b,c),multiply(a,c)) ).
% 63.06/63.18
% 63.06/63.18 cnf(prove_c_is_0,negated_conjecture,
% 63.06/63.18 ~ equalish(c,n0) ).
% 63.06/63.18
% 63.06/63.18 %--------------------------------------------------------------------------
% 63.06/63.18 %-------------------------------------------
% 63.06/63.18 % Proof found
% 63.06/63.18 % SZS status Theorem for theBenchmark
% 63.06/63.18 % SZS output start Proof
% 63.06/63.18 %ClaNum:21(EqnAxiom:0)
% 63.06/63.18 %VarNum:75(SingletonVarNum:36)
% 63.06/63.18 %MaxLitNum:3
% 63.06/63.18 %MaxfuncDepth:3
% 63.06/63.18 %SharedTerms:9
% 63.06/63.18 %goalClause: 7
% 63.06/63.18 %singleGoalClaCount:1
% 63.06/63.18 [7]~P1(a6,a1)
% 63.06/63.18 [8]~P2(a5,a4)
% 63.06/63.18 [4]P2(f2(a5,a6),f2(a4,a6))
% 63.06/63.18 [1]P1(x11,x11)
% 63.06/63.18 [9]~P2(x91,x91)
% 63.06/63.18 [2]P1(f2(x21,a1),a1)
% 63.06/63.18 [3]P1(f3(x31,a1),x31)
% 63.06/63.18 [10]~P1(f7(x101),a1)
% 63.06/63.18 [5]P1(f3(x51,f7(x52)),f7(f3(x51,x52)))
% 63.06/63.18 [6]P1(f2(x61,f7(x62)),f3(f2(x61,x62),x61))
% 63.06/63.18 [11]~P1(x112,x111)+P1(x111,x112)
% 63.06/63.18 [13]~P2(x131,x132)+~P1(x131,x132)
% 63.06/63.18 [14]~P1(x141,x142)+P1(f7(x141),f7(x142))
% 63.06/63.18 [15]P1(x151,x152)+~P1(f7(x151),f7(x152))
% 63.06/63.18 [21]~P2(x212,x211)+P1(f3(f7(f8(x211,x212)),x212),x211)
% 63.06/63.18 [18]~P1(x181,x183)+P1(f2(x181,x182),f2(x183,x182))
% 63.06/63.18 [19]P2(x191,x192)+~P1(f3(f7(x193),x191),x192)
% 63.06/63.18 [12]P2(x121,x122)+P2(x122,x121)+P1(x121,x122)
% 63.06/63.18 [16]~P1(x161,x163)+P1(x161,x162)+~P1(x163,x162)
% 63.06/63.18 [17]~P2(x173,x172)+P2(x171,x172)+~P2(x171,x173)
% 63.06/63.18 [20]~P2(x202,x203)+P2(f2(x202,x201),f2(x203,x201))+P1(x201,a1)
% 63.06/63.18 %EqnAxiom
% 63.06/63.18
% 63.13/63.18 %-------------------------------------------
% 63.13/63.19 cnf(24,plain,
% 63.13/63.19 (~P2(f3(x241,a1),x241)),
% 63.13/63.19 inference(scs_inference,[],[7,3,11,13])).
% 63.13/63.19 cnf(26,plain,
% 63.13/63.19 (P2(x261,f3(f7(x262),x261))),
% 63.13/63.19 inference(scs_inference,[],[7,1,3,11,13,19])).
% 63.13/63.19 cnf(29,plain,
% 63.13/63.19 (P2(f2(a5,a6),f3(f7(x291),f2(a4,a6)))),
% 63.13/63.19 inference(scs_inference,[],[7,1,3,4,11,13,19,17])).
% 63.13/63.19 cnf(31,plain,
% 63.13/63.19 (P1(a4,a5)+P2(a4,a5)),
% 63.13/63.19 inference(scs_inference,[],[7,1,3,8,4,11,13,19,17,12])).
% 63.13/63.19 cnf(35,plain,
% 63.13/63.19 (~P1(a1,f7(x351))),
% 63.13/63.19 inference(scs_inference,[],[10,6,13,11])).
% 63.13/63.19 cnf(37,plain,
% 63.13/63.19 (P2(f7(x371),f7(f3(f7(x372),x371)))),
% 63.13/63.19 inference(scs_inference,[],[10,6,5,13,11,19])).
% 63.13/63.19 cnf(40,plain,
% 63.13/63.19 (P1(f2(a1,f7(x401)),f2(a1,x401))),
% 63.13/63.19 inference(scs_inference,[],[10,6,5,3,13,11,19,16])).
% 63.13/63.19 cnf(44,plain,
% 63.13/63.19 (~P2(f3(f7(x441),x442),x442)),
% 63.13/63.19 inference(scs_inference,[],[10,9,26,6,5,3,13,11,19,16,17])).
% 63.13/63.19 cnf(49,plain,
% 63.13/63.19 (~P2(f2(a1,f7(x491)),f2(a1,x491))),
% 63.13/63.19 inference(scs_inference,[],[40,13])).
% 63.13/63.19 cnf(51,plain,
% 63.13/63.19 (P2(a1,f7(x511))),
% 63.13/63.19 inference(scs_inference,[],[40,3,13,19])).
% 63.13/63.19 cnf(54,plain,
% 63.13/63.19 (P1(f2(a1,f7(a1)),a1)),
% 63.13/63.19 inference(scs_inference,[],[40,2,3,13,19,16])).
% 63.13/63.19 cnf(58,plain,
% 63.13/63.19 (P2(f2(a5,a6),f3(f7(x581),f3(f7(x582),f2(a4,a6))))),
% 63.13/63.19 inference(scs_inference,[],[40,29,2,26,3,13,19,16,17])).
% 63.13/63.19 cnf(63,plain,
% 63.13/63.19 (~P2(f2(a1,f7(a1)),a1)),
% 63.13/63.19 inference(scs_inference,[],[54,13])).
% 63.13/63.19 cnf(65,plain,
% 63.13/63.19 (P1(f2(a1,f7(f7(a1))),a1)),
% 63.13/63.19 inference(scs_inference,[],[54,40,13,16])).
% 63.13/63.19 cnf(68,plain,
% 63.13/63.19 (~P2(f3(f7(x681),f3(f7(x682),x683)),x683)),
% 63.13/63.19 inference(scs_inference,[],[54,40,44,26,13,16,17])).
% 63.13/63.19 cnf(75,plain,
% 63.13/63.19 (P1(f2(a1,f7(f7(x751))),f3(f2(a1,x751),a1))),
% 63.13/63.19 inference(scs_inference,[],[65,40,6,13,16])).
% 63.13/63.19 cnf(79,plain,
% 63.13/63.19 (P1(x791,f3(f7(x792),f3(f7(x793),x791)))+P2(x791,f3(f7(x792),f3(f7(x793),x791)))),
% 63.13/63.19 inference(scs_inference,[],[65,40,68,6,13,16,12])).
% 63.13/63.19 cnf(83,plain,
% 63.13/63.19 (P1(f2(a1,f7(f7(x831))),f2(a1,x831))),
% 63.13/63.19 inference(scs_inference,[],[75,3,13,16])).
% 63.13/63.19 cnf(86,plain,
% 63.13/63.19 (P2(a1,f3(f7(x861),f7(x862)))),
% 63.13/63.19 inference(scs_inference,[],[75,51,26,3,13,16,17])).
% 63.13/63.19 cnf(93,plain,
% 63.13/63.19 (P2(a1,f3(f7(x931),f3(f7(x932),f7(x933))))),
% 63.13/63.19 inference(scs_inference,[],[83,26,86,13,17])).
% 63.13/63.19 cnf(102,plain,
% 63.13/63.19 (~P2(f2(x1021,a1),a1)),
% 63.13/63.19 inference(scs_inference,[],[2,13])).
% 63.13/63.19 cnf(115,plain,
% 63.13/63.19 (P2(a1,f2(x1151,a1))+P1(f2(a1,f7(f7(a1))),f2(x1151,a1))),
% 63.13/63.19 inference(scs_inference,[],[65,102,12,13,16])).
% 63.13/63.19 cnf(117,plain,
% 63.13/63.19 (P1(a5,a4)+P2(a4,a5)),
% 63.13/63.19 inference(scs_inference,[],[31,11])).
% 63.13/63.19 cnf(118,plain,
% 63.13/63.19 (P1(a5,a4)+P1(f3(f7(f8(a5,a4)),a4),a5)),
% 63.13/63.19 inference(scs_inference,[],[117,21])).
% 63.13/63.19 cnf(119,plain,
% 63.13/63.19 (P1(f7(f2(f3(x1191,a1),x1192)),f7(f2(x1191,x1192)))),
% 63.13/63.19 inference(scs_inference,[],[3,14,18])).
% 63.13/63.19 cnf(120,plain,
% 63.13/63.19 (P1(f2(f3(x1201,a1),x1202),f2(x1201,x1202))),
% 63.13/63.19 inference(scs_inference,[],[119,15])).
% 63.13/63.19 cnf(124,plain,
% 63.13/63.19 (P1(f3(f2(a1,f7(a1)),a1),a1)),
% 63.13/63.19 inference(scs_inference,[],[3,54,119,15,13,16])).
% 63.13/63.20 cnf(130,plain,
% 63.13/63.20 (~P2(f2(f3(x1301,a1),x1302),f2(x1301,x1302))),
% 63.13/63.20 inference(scs_inference,[],[120,13])).
% 63.13/63.20 cnf(132,plain,
% 63.13/63.20 (P1(f3(f2(a1,f7(x1321)),a1),f2(a1,x1321))),
% 63.13/63.20 inference(scs_inference,[],[3,40,120,13,16])).
% 63.13/63.20 cnf(138,plain,
% 63.13/63.20 (~P2(f3(f2(a1,f7(x1381)),a1),f2(a1,x1381))),
% 63.13/63.20 inference(scs_inference,[],[132,13])).
% 63.13/63.20 cnf(140,plain,
% 63.13/63.20 (P1(f3(f2(f3(x1401,a1),x1402),a1),f2(x1401,x1402))),
% 63.13/63.20 inference(scs_inference,[],[3,132,120,13,16])).
% 63.13/63.20 cnf(147,plain,
% 63.13/63.20 (P1(f3(f3(x1471,f7(x1472)),a1),f7(f3(x1471,x1472)))),
% 63.13/63.20 inference(scs_inference,[],[3,140,5,13,16])).
% 63.13/63.20 cnf(154,plain,
% 63.13/63.20 (P1(f3(f2(x1541,a1),a1),a1)),
% 63.13/63.20 inference(scs_inference,[],[3,124,2,13,16])).
% 63.13/63.20 cnf(157,plain,
% 63.13/63.20 (P1(a1,f3(f2(a1,f7(a1)),a1))+P2(a1,f3(f2(a1,f7(a1)),a1))),
% 63.13/63.20 inference(scs_inference,[],[3,124,2,13,16,12])).
% 63.13/63.20 cnf(161,plain,
% 63.13/63.20 (P1(f3(f3(f2(x1611,a1),a1),a1),a1)),
% 63.13/63.20 inference(scs_inference,[],[3,147,154,13,16])).
% 63.13/63.20 cnf(169,plain,
% 63.13/63.20 (P1(f3(f2(x1691,f7(x1692)),a1),f3(f2(x1691,x1692),x1691))),
% 63.13/63.20 inference(scs_inference,[],[3,161,6,13,16])).
% 63.13/63.20 cnf(175,plain,
% 63.13/63.20 (~P2(f3(f2(x1751,f7(x1752)),a1),f3(f2(x1751,x1752),x1751))),
% 63.13/63.20 inference(scs_inference,[],[169,13])).
% 63.13/63.20 cnf(179,plain,
% 63.13/63.20 (~P2(f3(f2(x1791,a1),a1),a1)),
% 63.13/63.20 inference(scs_inference,[],[154,13])).
% 63.13/63.20 cnf(183,plain,
% 63.13/63.20 (P2(a1,f3(f2(x1831,a1),a1))+P1(f3(a1,a1),f3(f2(x1831,a1),a1))),
% 63.13/63.20 inference(scs_inference,[],[3,154,13,12,16])).
% 63.13/63.20 cnf(187,plain,
% 63.13/63.20 (P1(f2(x1871,a1),f2(a1,f7(f7(a1))))+P2(a1,f2(x1871,a1))),
% 63.13/63.20 inference(scs_inference,[],[115,11])).
% 63.13/63.20 cnf(198,plain,
% 63.13/63.20 (~P2(f2(x1981,a1),f2(a1,f7(f7(a1))))+P2(a1,f2(x1981,a1))),
% 63.13/63.20 inference(scs_inference,[],[187,13])).
% 63.13/63.20 cnf(199,plain,
% 63.13/63.20 (~P2(f3(f7(x1991),f3(x1992,a1)),x1992)),
% 63.13/63.20 inference(scs_inference,[],[24,26,17])).
% 63.13/63.20 cnf(206,plain,
% 63.13/63.20 (P2(a1,f3(f7(x2061),f3(a1,a1)))+P1(f2(a1,f7(a1)),f3(f7(x2061),f3(a1,a1)))),
% 63.13/63.20 inference(scs_inference,[],[24,54,26,17,12,13,16])).
% 63.13/63.20 cnf(208,plain,
% 63.13/63.20 (P2(a1,f2(x2081,a1))+~P1(f3(f7(x2082),f2(x2081,a1)),f2(a1,f7(f7(a1))))),
% 63.13/63.20 inference(scs_inference,[],[198,19])).
% 63.13/63.20 cnf(210,plain,
% 63.13/63.20 (P1(f2(a1,f7(a1)),f3(f2(a1,f7(a1)),a1))+P2(a1,f3(f2(a1,f7(a1)),a1))),
% 63.13/63.20 inference(scs_inference,[],[54,157,16])).
% 63.13/63.20 cnf(219,plain,
% 63.13/63.20 (P1(f3(f2(x2191,a1),a1),f3(a1,a1))+P2(a1,f3(f2(x2191,a1),a1))),
% 63.13/63.20 inference(scs_inference,[],[183,11])).
% 63.13/63.20 cnf(221,plain,
% 63.13/63.20 (P1(f2(a1,f7(f7(a1))),f3(a1,a1))+P2(a1,f3(f2(a1,a1),a1))),
% 63.13/63.20 inference(scs_inference,[],[75,219,16])).
% 63.13/63.20 cnf(229,plain,
% 63.13/63.20 (P2(f2(a1,x2291),f3(f7(x2292),f2(a1,f7(x2291))))+P1(f2(a1,f7(x2291)),f3(f7(x2292),f2(a1,f7(x2291))))),
% 63.13/63.20 inference(scs_inference,[],[49,40,26,17,12,13,16])).
% 63.13/63.20 cnf(231,plain,
% 63.13/63.20 (P1(f3(a1,a1),f2(a1,f7(f7(a1))))+P2(a1,f3(f2(a1,a1),a1))),
% 63.13/63.20 inference(scs_inference,[],[221,11])).
% 63.13/63.20 cnf(232,plain,
% 63.13/63.20 (~P2(f3(a1,a1),f2(a1,f7(f7(a1))))+P2(a1,f3(f2(a1,a1),a1))),
% 63.13/63.20 inference(scs_inference,[],[231,13])).
% 63.13/63.20 cnf(233,plain,
% 63.13/63.20 (P2(a1,f3(f2(a1,a1),a1))+~P1(f3(f7(x2331),f3(a1,a1)),f2(a1,f7(f7(a1))))),
% 63.13/63.20 inference(scs_inference,[],[232,19])).
% 63.13/63.20 cnf(235,plain,
% 63.13/63.20 (P2(a1,f3(f7(x2351),f3(f7(x2352),a1)))+P1(f2(a1,f7(a1)),f3(f7(x2351),f3(f7(x2352),a1)))),
% 63.13/63.20 inference(scs_inference,[],[54,79,16])).
% 63.13/63.20 cnf(243,plain,
% 63.13/63.20 (P2(a1,f3(f7(x2431),f2(a1,f7(a1))))+P1(f2(a1,f7(a1)),f3(f7(x2431),f2(a1,f7(a1))))),
% 63.13/63.20 inference(scs_inference,[],[63,54,26,17,12,13,16])).
% 63.13/63.20 cnf(258,plain,
% 63.13/63.20 (P1(f3(f7(x2581),f3(a1,a1)),f2(a1,f7(a1)))+P2(a1,f3(f7(x2581),f3(a1,a1)))),
% 63.13/63.20 inference(scs_inference,[],[206,11])).
% 63.13/63.20 cnf(267,plain,
% 63.13/63.20 (P2(a1,f3(f7(x2671),f2(x2672,a1)))+P1(f2(a1,f7(a1)),f3(f7(x2671),f2(x2672,a1)))),
% 63.13/63.20 inference(scs_inference,[],[102,54,26,17,12,13,16])).
% 63.13/63.20 cnf(270,plain,
% 63.13/63.20 (P1(f2(f3(a1,a1),f7(a1)),a1)),
% 63.13/63.20 inference(scs_inference,[],[120,54,16])).
% 63.13/63.20 cnf(278,plain,
% 63.13/63.20 (P1(f2(f3(a1,a1),f7(x2781)),f2(a1,x2781))),
% 63.13/63.20 inference(scs_inference,[],[120,40,16])).
% 63.13/63.20 cnf(285,plain,
% 63.13/63.20 (P1(f2(f3(a1,a1),f7(f7(x2851))),f2(a1,x2851))),
% 63.13/63.20 inference(scs_inference,[],[120,83,16])).
% 63.13/63.20 cnf(288,plain,
% 63.13/63.20 (~P1(f2(a1,f7(f7(a1))),f3(f7(x2881),f3(a1,a1)))+P2(a1,f3(f2(a1,a1),a1))),
% 63.13/63.20 inference(scs_inference,[],[233,11])).
% 63.13/63.20 cnf(291,plain,
% 63.13/63.20 (P1(f2(f3(a1,a1),f7(f7(a1))),a1)),
% 63.13/63.20 inference(scs_inference,[],[120,65,285,13,16])).
% 63.13/63.20 cnf(298,plain,
% 63.13/63.20 (P1(f2(f3(a1,a1),f7(f7(x2981))),f3(f2(a1,x2981),a1))),
% 63.13/63.20 inference(scs_inference,[],[120,75,291,13,16])).
% 63.13/63.20 cnf(306,plain,
% 63.13/63.20 (P1(f2(f3(f3(a1,a1),a1),f7(a1)),a1)),
% 63.13/63.20 inference(scs_inference,[],[120,270,298,13,16])).
% 63.13/63.20 cnf(313,plain,
% 63.13/63.20 (P1(f2(f3(f3(a1,a1),a1),f7(x3131)),f2(a1,x3131))),
% 63.13/63.20 inference(scs_inference,[],[120,278,306,13,16])).
% 63.13/63.20 cnf(316,plain,
% 63.13/63.20 (P1(a1,f2(f3(f3(a1,a1),a1),f7(a1)))+P2(a1,f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.20 inference(scs_inference,[],[120,278,306,13,16,12])).
% 63.13/63.20 cnf(321,plain,
% 63.13/63.20 (P1(f2(f3(f3(f3(a1,a1),a1),a1),f7(x3211)),f2(a1,x3211))),
% 63.13/63.20 inference(scs_inference,[],[120,313,13,16])).
% 63.13/63.20 cnf(329,plain,
% 63.13/63.20 (P1(f2(f3(f3(a1,a1),a1),f7(f7(a1))),a1)),
% 63.13/63.20 inference(scs_inference,[],[120,321,291,13,16])).
% 63.13/63.20 cnf(334,plain,
% 63.13/63.20 (P1(f3(f7(x3341),f2(x3342,a1)),f2(a1,f7(a1)))+P2(a1,f3(f7(x3341),f2(x3342,a1)))),
% 63.13/63.20 inference(scs_inference,[],[267,11])).
% 63.13/63.20 cnf(337,plain,
% 63.13/63.20 (P1(f2(f3(f3(a1,a1),a1),f7(f7(x3371))),f2(a1,x3371))),
% 63.13/63.20 inference(scs_inference,[],[120,329,285,13,16])).
% 63.13/63.20 cnf(345,plain,
% 63.13/63.20 (P1(f2(f3(f3(f3(a1,a1),a1),a1),f7(a1)),a1)),
% 63.13/63.20 inference(scs_inference,[],[120,337,306,13,16])).
% 63.13/63.20 cnf(353,plain,
% 63.13/63.20 (P1(f2(f3(x3531,a1),f7(x3532)),f3(f2(x3531,x3532),x3531))),
% 63.13/63.20 inference(scs_inference,[],[120,345,6,13,16])).
% 63.13/63.20 cnf(360,plain,
% 63.13/63.20 (~P2(f2(f3(x3601,a1),f7(x3602)),f3(f2(x3601,x3602),x3601))),
% 63.13/63.20 inference(scs_inference,[],[353,13])).
% 63.13/63.20 cnf(362,plain,
% 63.13/63.20 (P1(f2(f3(f3(x3621,a1),a1),f7(x3622)),f3(f2(x3621,x3622),x3621))),
% 63.13/63.20 inference(scs_inference,[],[120,353,13,16])).
% 63.13/63.20 cnf(374,plain,
% 63.13/63.20 (P2(a1,f2(f3(f3(a1,a1),a1),f7(a1)))+P1(f7(a1),f7(f2(f3(f3(a1,a1),a1),f7(a1))))),
% 63.13/63.20 inference(scs_inference,[],[316,14])).
% 63.13/63.20 cnf(375,plain,
% 63.13/63.20 (~P2(f3(f7(x3751),f2(f3(x3752,a1),x3753)),f2(x3752,x3753))),
% 63.13/63.20 inference(scs_inference,[],[130,26,17])).
% 63.13/63.20 cnf(384,plain,
% 63.13/63.20 (P1(f3(f7(x3841),f3(f7(x3842),a1)),f2(a1,f7(a1)))+P2(a1,f3(f7(x3841),f3(f7(x3842),a1)))),
% 63.13/63.20 inference(scs_inference,[],[235,11])).
% 63.13/63.20 cnf(385,plain,
% 63.13/63.20 (P2(a1,f3(f7(x3851),f2(a1,f7(a1))))),
% 63.13/63.20 inference(scs_inference,[],[26,243,13])).
% 63.13/63.20 cnf(429,plain,
% 63.13/63.20 (~P2(f7(x4291),a1)),
% 63.13/63.20 inference(scs_inference,[],[51,9,17])).
% 63.13/63.20 cnf(433,plain,
% 63.13/63.20 (~P2(f2(a4,a6),f2(a5,a6))),
% 63.13/63.20 inference(scs_inference,[],[4,9,17])).
% 63.13/63.20 cnf(452,plain,
% 63.13/63.20 (~P2(f3(f7(x4521),f3(f2(x4522,a1),a1)),a1)),
% 63.13/63.20 inference(scs_inference,[],[179,26,17])).
% 63.13/63.20 cnf(478,plain,
% 63.13/63.20 (P2(a1,f3(f7(x4781),f3(f7(x4782),f3(a1,a1))))+P1(f2(a1,f7(a1)),f3(f7(x4781),f3(f7(x4782),f3(a1,a1))))),
% 63.13/63.20 inference(scs_inference,[],[199,54,26,17,12,13,16])).
% 63.13/63.20 cnf(511,plain,
% 63.13/63.20 (P2(f2(a1,x5111),f3(f7(x5112),f2(a1,f7(x5111))))),
% 63.13/63.20 inference(scs_inference,[],[26,229,13])).
% 63.13/63.20 cnf(546,plain,
% 63.13/63.20 (P2(f3(f2(x5461,x5462),x5461),f3(f7(x5463),f2(f3(x5461,a1),f7(x5462))))+P1(f2(f3(x5461,a1),f7(x5462)),f3(f7(x5463),f2(f3(x5461,a1),f7(x5462))))),
% 63.13/63.20 inference(scs_inference,[],[360,353,26,17,12,13,16])).
% 63.13/63.20 cnf(549,plain,
% 63.13/63.20 (P1(f3(f7(x5491),f3(f7(x5492),f3(a1,a1))),f2(a1,f7(a1)))+P2(a1,f3(f7(x5491),f3(f7(x5492),f3(a1,a1))))),
% 63.13/63.20 inference(scs_inference,[],[478,11])).
% 63.13/63.20 cnf(553,plain,
% 63.13/63.20 (P2(f3(f7(x5531),f3(a1,a1)),f2(a1,f7(a1)))+P2(a1,f3(f7(x5532),f3(f7(x5531),f3(a1,a1))))),
% 63.13/63.20 inference(scs_inference,[],[549,19])).
% 63.13/63.20 cnf(562,plain,
% 63.13/63.20 (~P2(a4,a5)),
% 63.13/63.20 inference(scs_inference,[],[433,7,20])).
% 63.13/63.20 cnf(564,plain,
% 63.13/63.20 (P1(a4,a5)),
% 63.13/63.20 inference(scs_inference,[],[433,7,8,20,12])).
% 63.13/63.20 cnf(566,plain,
% 63.13/63.20 (P1(a5,a4)),
% 63.13/63.20 inference(scs_inference,[],[562,117])).
% 63.13/63.20 cnf(577,plain,
% 63.13/63.20 (P2(a5,f3(f7(x5771),a4))+P1(a4,f3(f7(x5771),a4))),
% 63.13/63.20 inference(scs_inference,[],[564,562,26,17,12,13,16])).
% 63.13/63.20 cnf(580,plain,
% 63.13/63.20 (P2(a5,f3(f7(x5801),a4))),
% 63.13/63.20 inference(scs_inference,[],[26,577,13])).
% 63.13/63.20 cnf(604,plain,
% 63.13/63.20 (P1(f3(a5,a1),a4)),
% 63.13/63.20 inference(scs_inference,[],[3,566,16])).
% 63.13/63.20 cnf(609,plain,
% 63.13/63.20 (P1(a4,f3(a5,a1))+P2(a4,f3(a5,a1))),
% 63.13/63.20 inference(scs_inference,[],[3,566,16,13,12])).
% 63.13/63.20 cnf(611,plain,
% 63.13/63.20 (P1(a4,f3(a5,a1))+P2(f2(a4,a6),f2(f3(a5,a1),a6))),
% 63.13/63.20 inference(scs_inference,[],[7,609,20])).
% 63.13/63.20 cnf(612,plain,
% 63.13/63.20 (P1(f3(a4,a1),a5)),
% 63.13/63.20 inference(scs_inference,[],[3,564,16])).
% 63.13/63.20 cnf(615,plain,
% 63.13/63.20 (~P2(f3(a4,a1),a5)),
% 63.13/63.20 inference(scs_inference,[],[3,564,16,13])).
% 63.13/63.20 cnf(620,plain,
% 63.13/63.20 (P1(f3(f3(a5,a1),a1),a4)),
% 63.13/63.20 inference(scs_inference,[],[3,604,16])).
% 63.13/63.20 cnf(627,plain,
% 63.13/63.20 (P2(f2(a4,a6),f2(f3(a5,a1),a6))+P1(f7(a4),f7(f3(a5,a1)))),
% 63.13/63.20 inference(scs_inference,[],[611,14])).
% 63.13/63.20 cnf(628,plain,
% 63.13/63.20 (P1(f3(f3(a4,a1),a1),a5)),
% 63.13/63.20 inference(scs_inference,[],[3,612,16])).
% 63.13/63.20 cnf(644,plain,
% 63.13/63.20 (P1(f3(f3(f3(a4,a1),a1),a1),a5)),
% 63.13/63.20 inference(scs_inference,[],[3,628,16])).
% 63.13/63.20 cnf(652,plain,
% 63.13/63.20 (P1(f7(f3(a5,a1)),f7(a4))+P2(f2(a4,a6),f2(f3(a5,a1),a6))),
% 63.13/63.20 inference(scs_inference,[],[627,11])).
% 63.13/63.20 cnf(653,plain,
% 63.13/63.20 (~P2(f7(f3(a5,a1)),f7(a4))+P2(f2(a4,a6),f2(f3(a5,a1),a6))),
% 63.13/63.20 inference(scs_inference,[],[652,13])).
% 63.13/63.20 cnf(654,plain,
% 63.13/63.20 (P2(f2(a4,a6),f2(f3(a5,a1),a6))+~P1(f3(f7(x6541),f7(f3(a5,a1))),f7(a4))),
% 63.13/63.20 inference(scs_inference,[],[653,19])).
% 63.13/63.20 cnf(661,plain,
% 63.13/63.20 (~P1(f7(a4),f3(f7(x6611),f7(f3(a5,a1))))+P2(f2(a4,a6),f2(f3(a5,a1),a6))),
% 63.13/63.20 inference(scs_inference,[],[654,11])).
% 63.13/63.20 cnf(668,plain,
% 63.13/63.20 (~P1(f3(f2(x6681,x6682),x6681),f3(f7(x6683),f2(f3(x6681,a1),f7(x6682))))+P1(f2(f3(x6681,a1),f7(x6682)),f3(f7(x6683),f2(f3(x6681,a1),f7(x6682))))),
% 63.13/63.20 inference(scs_inference,[],[546,13])).
% 63.13/63.20 cnf(669,plain,
% 63.13/63.20 (~P1(f3(f7(x6691),f2(f3(x6692,a1),f7(x6693))),f3(f2(x6692,x6693),x6692))+P1(f2(f3(x6692,a1),f7(x6693)),f3(f7(x6691),f2(f3(x6692,a1),f7(x6693))))),
% 63.13/63.20 inference(scs_inference,[],[668,11])).
% 63.13/63.20 cnf(671,plain,
% 63.13/63.20 (~P2(a1,f3(f2(a1,f7(a1)),a1))),
% 63.13/63.20 inference(scs_inference,[],[124,11,13])).
% 63.13/63.20 cnf(672,plain,
% 63.13/63.20 (P1(a1,f3(f2(a1,f7(a1)),a1))),
% 63.13/63.20 inference(scs_inference,[],[671,157])).
% 63.13/63.20 cnf(673,plain,
% 63.13/63.20 (P1(f2(a1,f7(a1)),f3(f2(a1,f7(a1)),a1))),
% 63.13/63.20 inference(scs_inference,[],[671,210])).
% 63.13/63.20 cnf(674,plain,
% 63.13/63.20 (~P2(f7(x6741),f3(f2(a1,f7(a1)),a1))),
% 63.13/63.20 inference(scs_inference,[],[51,671,17])).
% 63.13/63.20 cnf(678,plain,
% 63.13/63.20 (P2(f3(f2(a1,f7(a1)),a1),f7(x6781))+P1(f2(f3(a1,a1),f7(f7(a1))),f7(x6781))),
% 63.13/63.20 inference(scs_inference,[],[353,51,671,17,12,16])).
% 63.13/63.20 cnf(708,plain,
% 63.13/63.20 (P1(f7(x7081),f2(f3(a1,a1),f7(f7(a1))))+P2(f3(f2(a1,f7(a1)),a1),f7(x7081))),
% 63.13/63.20 inference(scs_inference,[],[678,11])).
% 63.13/63.20 cnf(709,plain,
% 63.13/63.20 (P2(f3(f2(a1,f7(a1)),a1),f7(x7091))),
% 63.13/63.20 inference(scs_inference,[],[291,10,708,16])).
% 63.13/63.20 cnf(710,plain,
% 63.13/63.20 (~P2(f7(x7101),f2(a1,f7(a1)))),
% 63.13/63.20 inference(scs_inference,[],[709,24,17])).
% 63.13/63.20 cnf(726,plain,
% 63.13/63.20 (P2(f2(a1,a1),f7(x7261))+P1(f3(f2(a1,f7(a1)),a1),f7(x7261))),
% 63.13/63.20 inference(scs_inference,[],[132,709,138,17,12,13,16])).
% 63.13/63.20 cnf(730,plain,
% 63.13/63.20 (P2(f2(a1,a1),f7(x7301))),
% 63.13/63.20 inference(scs_inference,[],[709,726,13])).
% 63.13/63.20 cnf(735,plain,
% 63.13/63.20 (~P2(f7(x7351),f3(f2(a1,a1),a1))),
% 63.13/63.20 inference(scs_inference,[],[175,709,17])).
% 63.13/63.20 cnf(742,plain,
% 63.13/63.20 (P2(f3(f2(a1,a1),a1),f7(x7421))+P1(f2(f3(a1,a1),f7(a1)),f7(x7421))),
% 63.13/63.20 inference(scs_inference,[],[175,353,709,17,12,13,16])).
% 63.13/63.20 cnf(746,plain,
% 63.13/63.20 (P1(f7(x7461),f2(f3(a1,a1),f7(a1)))+P2(f3(f2(a1,a1),a1),f7(x7461))),
% 63.13/63.20 inference(scs_inference,[],[742,11])).
% 63.13/63.20 cnf(747,plain,
% 63.13/63.20 (P2(f3(f2(a1,a1),a1),f7(x7471))),
% 63.13/63.20 inference(scs_inference,[],[270,10,746,16])).
% 63.13/63.20 cnf(751,plain,
% 63.13/63.20 (P1(f7(a1),f7(f3(f2(x7511,a1),a1)))),
% 63.13/63.20 inference(scs_inference,[],[154,11,14])).
% 63.13/63.20 cnf(752,plain,
% 63.13/63.20 (P1(a1,f3(f2(x7521,a1),a1))),
% 63.13/63.20 inference(scs_inference,[],[751,15])).
% 63.13/63.20 cnf(756,plain,
% 63.13/63.20 (P1(f3(f2(x7561,a1),a1),f3(f2(x7562,a1),a1))),
% 63.13/63.20 inference(scs_inference,[],[154,751,15,13,16])).
% 63.13/63.20 cnf(763,plain,
% 63.13/63.20 (P1(f3(f2(x7631,a1),a1),f2(x7632,a1))),
% 63.13/63.20 inference(scs_inference,[],[140,756,13,16])).
% 63.13/63.20 cnf(769,plain,
% 63.13/63.20 (P1(a1,f2(x7691,a1))),
% 63.13/63.20 inference(scs_inference,[],[140,763,752,13,16])).
% 63.13/63.20 cnf(776,plain,
% 63.13/63.20 (~P2(a1,f2(x7761,a1))),
% 63.13/63.20 inference(scs_inference,[],[769,13])).
% 63.13/63.20 cnf(778,plain,
% 63.13/63.20 (P1(f2(f3(a1,a1),f7(a1)),f2(x7781,a1))),
% 63.13/63.20 inference(scs_inference,[],[353,769,763,13,16])).
% 63.13/63.20 cnf(782,plain,
% 63.13/63.20 (P1(f2(a1,f7(f7(a1))),f2(x7821,a1))),
% 63.13/63.20 inference(scs_inference,[],[353,769,763,13,16,115])).
% 63.13/63.20 cnf(784,plain,
% 63.13/63.20 (P1(f2(x7841,a1),f2(a1,f7(f7(a1))))),
% 63.13/63.20 inference(scs_inference,[],[353,769,763,13,16,115,187])).
% 63.13/63.20 cnf(786,plain,
% 63.13/63.20 (~P2(f2(x7861,a1),f2(a1,f7(f7(a1))))),
% 63.13/63.20 inference(scs_inference,[],[353,769,763,13,16,115,187,198])).
% 63.13/63.20 cnf(790,plain,
% 63.13/63.20 (~P1(f2(a1,f7(f7(a1))),f3(f7(x7901),f2(x7902,a1)))),
% 63.13/63.20 inference(scs_inference,[],[353,769,763,13,16,115,187,198,208,11])).
% 63.13/63.20 cnf(796,plain,
% 63.13/63.20 (P1(f2(f3(f3(a1,a1),a1),f7(a1)),f2(x7961,a1))),
% 63.13/63.20 inference(scs_inference,[],[120,385,778,776,13,17,16])).
% 63.13/63.20 cnf(802,plain,
% 63.13/63.20 (~P2(f2(a1,f7(f7(a1))),f2(x8021,a1))),
% 63.13/63.20 inference(scs_inference,[],[782,13])).
% 63.13/63.20 cnf(804,plain,
% 63.13/63.20 (~P2(f7(x8041),f2(x8042,a1))),
% 63.13/63.20 inference(scs_inference,[],[782,51,776,13,17])).
% 63.13/63.20 cnf(820,plain,
% 63.13/63.20 (~P2(a1,f3(f2(x8201,a1),a1))),
% 63.13/63.20 inference(scs_inference,[],[752,13])).
% 63.13/63.20 cnf(825,plain,
% 63.13/63.20 (~P1(f2(a1,f7(f7(a1))),f3(f7(x8251),f3(a1,a1)))),
% 63.13/63.20 inference(scs_inference,[],[140,752,778,13,16,288])).
% 63.13/63.20 cnf(828,plain,
% 63.13/63.20 (P1(f3(f2(a1,a1),a1),f3(a1,a1))),
% 63.13/63.20 inference(scs_inference,[],[140,752,778,13,16,288,183,219])).
% 63.13/63.20 cnf(830,plain,
% 63.13/63.20 (P1(f2(a1,f7(f7(a1))),f3(a1,a1))),
% 63.13/63.20 inference(scs_inference,[],[140,752,778,13,16,288,183,219,221])).
% 63.13/63.20 cnf(831,plain,
% 63.13/63.20 (P1(f3(a1,a1),f2(a1,f7(f7(a1))))),
% 63.13/63.20 inference(scs_inference,[],[140,752,778,13,16,288,183,219,221,231])).
% 63.13/63.20 cnf(832,plain,
% 63.13/63.20 (~P2(f3(a1,a1),f2(a1,f7(f7(a1))))),
% 63.13/63.20 inference(scs_inference,[],[140,752,778,13,16,288,183,219,221,231,232])).
% 63.13/63.20 cnf(833,plain,
% 63.13/63.20 (~P1(f3(f7(x8331),f3(a1,a1)),f2(a1,f7(f7(a1))))),
% 63.13/63.20 inference(scs_inference,[],[140,752,778,13,16,288,183,219,221,231,232,233])).
% 63.13/63.20 cnf(838,plain,
% 63.13/63.20 (P1(f3(f2(x8381,a1),a1),f3(a1,a1))),
% 63.13/63.20 inference(scs_inference,[],[820,219])).
% 63.13/63.20 cnf(840,plain,
% 63.13/63.20 (P1(f3(a1,a1),f3(f2(x8401,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[820,219,183])).
% 63.13/63.21 cnf(844,plain,
% 63.13/63.21 (~P2(f3(f7(x8441),f2(a1,f7(a1))),f3(f2(x8442,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[385,828,820,219,183,13,17])).
% 63.13/63.21 cnf(846,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[353,385,828,820,219,183,13,17,16])).
% 63.13/63.21 cnf(863,plain,
% 63.13/63.21 (~P2(f3(f2(x8631,a1),a1),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[838,13])).
% 63.13/63.21 cnf(865,plain,
% 63.13/63.21 (P1(f3(f2(x8651,a1),a1),f2(a1,f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[838,831,13,16])).
% 63.13/63.21 cnf(868,plain,
% 63.13/63.21 (~P2(f2(a1,f7(f7(a1))),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[830,13])).
% 63.13/63.21 cnf(870,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f2(a1,f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[278,830,784,13,16])).
% 63.13/63.21 cnf(876,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f3(f2(x8761,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[846,870,840,13,16])).
% 63.13/63.21 cnf(887,plain,
% 63.13/63.21 (P1(f3(f2(a1,f7(a1)),a1),f2(x8871,a1))),
% 63.13/63.21 inference(scs_inference,[],[169,763,865,13,16])).
% 63.13/63.21 cnf(894,plain,
% 63.13/63.21 (P1(f3(f2(a1,f7(a1)),a1),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[169,838,840,13,16])).
% 63.13/63.21 cnf(911,plain,
% 63.13/63.21 (P2(f3(f2(a1,a1),a1),f2(f3(a1,a1),f7(a1)))+P1(f3(f2(a1,f7(a1)),a1),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[169,876,13,12,16])).
% 63.13/63.21 cnf(916,plain,
% 63.13/63.21 (~P1(f3(f2(a1,a1),a1),f2(f3(a1,a1),f7(a1)))+P1(f3(f2(a1,f7(a1)),a1),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[911,13])).
% 63.13/63.21 cnf(917,plain,
% 63.13/63.21 (P1(f3(f2(a1,f7(a1)),a1),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[353,916,11])).
% 63.13/63.21 cnf(940,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(f7(a1))),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[298,838,16])).
% 63.13/63.21 cnf(946,plain,
% 63.13/63.21 (P1(f3(a1,a1),f2(f3(a1,a1),f7(f7(a1))))+P2(f3(a1,a1),f2(f3(a1,a1),f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[298,838,16,13,12])).
% 63.13/63.21 cnf(948,plain,
% 63.13/63.21 (P2(f3(a1,a1),f2(f3(a1,a1),f7(f7(a1))))+P1(f2(f3(a1,a1),f7(a1)),f2(f3(a1,a1),f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[846,946,16])).
% 63.13/63.21 cnf(949,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f2(f3(a1,a1),f7(f7(a1))))+~P1(f3(a1,a1),f2(f3(a1,a1),f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[948,13])).
% 63.13/63.21 cnf(968,plain,
% 63.13/63.21 (P1(f2(a1,x9681),f2(f3(f2(x9682,a1),a1),x9681))),
% 63.13/63.21 inference(scs_inference,[],[154,11,18])).
% 63.13/63.21 cnf(969,plain,
% 63.13/63.21 (~P2(f2(a1,x9691),f2(f3(f2(x9692,a1),a1),x9691))),
% 63.13/63.21 inference(scs_inference,[],[968,13])).
% 63.13/63.21 cnf(971,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(x9711)),f2(f3(f2(x9712,a1),a1),x9711))),
% 63.13/63.21 inference(scs_inference,[],[278,968,13,16])).
% 63.13/63.21 cnf(983,plain,
% 63.13/63.21 (P1(f2(f3(f3(a1,a1),a1),f7(a1)),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[362,838,16])).
% 63.13/63.21 cnf(989,plain,
% 63.13/63.21 (P1(f3(a1,a1),f2(f3(f3(a1,a1),a1),f7(a1)))+P2(f3(a1,a1),f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[362,838,16,13,12])).
% 63.13/63.21 cnf(991,plain,
% 63.13/63.21 (P2(f3(a1,a1),f2(f3(f3(a1,a1),a1),f7(a1)))+P1(f2(f3(a1,a1),f7(a1)),f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[846,989,16])).
% 63.13/63.21 cnf(995,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f2(f3(f3(a1,a1),a1),f7(a1)))+~P1(f3(a1,a1),f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[991,13])).
% 63.13/63.21 cnf(1001,plain,
% 63.13/63.21 (~P1(f3(a1,a1),f2(f3(f3(a1,a1),a1),f7(a1)))+~P2(f2(f3(a1,a1),f7(a1)),f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[995,13])).
% 63.13/63.21 cnf(1002,plain,
% 63.13/63.21 (~P2(f2(f3(a1,a1),f7(a1)),f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[983,1001,11])).
% 63.13/63.21 cnf(1003,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[130,1002,12])).
% 63.13/63.21 cnf(1006,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f2(f3(a1,a1),f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[940,11,949])).
% 63.13/63.21 cnf(1010,plain,
% 63.13/63.21 (~P1(f7(a1),f7(a6))),
% 63.13/63.21 inference(scs_inference,[],[7,11,15])).
% 63.13/63.21 cnf(1011,plain,
% 63.13/63.21 (~P1(f7(a6),f7(a1))),
% 63.13/63.21 inference(scs_inference,[],[1010,11])).
% 63.13/63.21 cnf(1013,plain,
% 63.13/63.21 (~P1(x10131,f3(f7(x10132),x10131))),
% 63.13/63.21 inference(scs_inference,[],[37,13,14])).
% 63.13/63.21 cnf(1015,plain,
% 63.13/63.21 (~P1(x10151,f3(f7(x10152),x10151))),
% 63.13/63.21 inference(rename_variables,[],[1013])).
% 63.13/63.21 cnf(1018,plain,
% 63.13/63.21 (~P1(x10181,f3(f7(x10182),x10181))),
% 63.13/63.21 inference(rename_variables,[],[1013])).
% 63.13/63.21 cnf(1020,plain,
% 63.13/63.21 (~P1(f3(f2(x10201,x10202),x10201),f3(f7(x10203),f2(f3(x10201,a1),f7(x10202))))),
% 63.13/63.21 inference(scs_inference,[],[1013,1015,1018,669,546,668])).
% 63.13/63.21 cnf(1021,plain,
% 63.13/63.21 (~P1(x10211,f3(f7(x10212),x10211))),
% 63.13/63.21 inference(rename_variables,[],[1013])).
% 63.13/63.21 cnf(1023,plain,
% 63.13/63.21 (~P1(f3(f7(x10231),x10232),x10232)),
% 63.13/63.21 inference(scs_inference,[],[1013,1015,1018,1021,669,546,668,11])).
% 63.13/63.21 cnf(1039,plain,
% 63.13/63.21 (~P1(f3(f7(x10391),f3(f2(x10392,a1),a1)),a1)),
% 63.13/63.21 inference(scs_inference,[],[154,13,19])).
% 63.13/63.21 cnf(1042,plain,
% 63.13/63.21 (P2(a1,f3(f7(x10421),f3(f2(x10422,a1),a1)))),
% 63.13/63.21 inference(scs_inference,[],[452,1039,11,12])).
% 63.13/63.21 cnf(1047,plain,
% 63.13/63.21 (~P1(f3(f7(x10471),a4),a5)),
% 63.13/63.21 inference(scs_inference,[],[580,13,11])).
% 63.13/63.21 cnf(1048,plain,
% 63.13/63.21 (P1(a5,a4)),
% 63.13/63.21 inference(scs_inference,[],[1047,118])).
% 63.13/63.21 cnf(1077,plain,
% 63.13/63.21 (~P1(a6,f3(f2(x10771,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1011,154,14,16])).
% 63.13/63.21 cnf(1078,plain,
% 63.13/63.21 (~P1(f3(f2(x10781,a1),a1),a6)),
% 63.13/63.21 inference(scs_inference,[],[1077,11])).
% 63.13/63.21 cnf(1086,plain,
% 63.13/63.21 (P2(f2(x10861,a6),f2(f3(f7(x10862),x10861),a6))),
% 63.13/63.21 inference(scs_inference,[],[1,7,19,20])).
% 63.13/63.21 cnf(1087,plain,
% 63.13/63.21 (~P2(f2(f3(f7(x10871),f3(x10872,a1)),a6),f2(x10872,a6))),
% 63.13/63.21 inference(scs_inference,[],[1086,130,17])).
% 63.13/63.21 cnf(1104,plain,
% 63.13/63.21 (~P2(f2(f3(f2(x11041,a1),a1),x11042),f2(a1,x11042))),
% 63.13/63.21 inference(scs_inference,[],[154,18,13])).
% 63.13/63.21 cnf(1105,plain,
% 63.13/63.21 (P1(f2(f3(f2(x11051,a1),a1),x11052),f2(a1,x11052))),
% 63.13/63.21 inference(scs_inference,[],[969,1104,12])).
% 63.13/63.21 cnf(1111,plain,
% 63.13/63.21 (P1(f2(a4,x11111),f2(f3(a5,a1),x11111))),
% 63.13/63.21 inference(scs_inference,[],[604,18,11])).
% 63.13/63.21 cnf(1112,plain,
% 63.13/63.21 (~P2(f2(a4,x11121),f2(f3(a5,a1),x11121))),
% 63.13/63.21 inference(scs_inference,[],[1111,13])).
% 63.13/63.21 cnf(1119,plain,
% 63.13/63.21 (P1(a4,f3(a5,a1))),
% 63.13/63.21 inference(scs_inference,[],[140,1111,13,16,661,611])).
% 63.13/63.21 cnf(1120,plain,
% 63.13/63.21 (P1(f7(a4),f7(f3(a5,a1)))),
% 63.13/63.21 inference(scs_inference,[],[140,1111,13,16,661,611,627])).
% 63.13/63.21 cnf(1123,plain,
% 63.13/63.21 (~P1(f3(f7(x11231),f7(f3(a5,a1))),f7(a4))),
% 63.13/63.21 inference(scs_inference,[],[140,1111,13,16,661,611,627,652,653,654])).
% 63.13/63.21 cnf(1162,plain,
% 63.13/63.21 (P1(a5,f3(f7(x11621),f3(a4,a1)))+P2(a5,f3(f7(x11621),f3(a4,a1)))),
% 63.13/63.21 inference(scs_inference,[],[615,26,17,12])).
% 63.13/63.21 cnf(1168,plain,
% 63.13/63.21 (P1(f3(f7(x11681),f3(a4,a1)),a5)+P2(a5,f3(f7(x11681),f3(a4,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1162,11])).
% 63.13/63.21 cnf(1169,plain,
% 63.13/63.21 (P1(f3(f3(a5,a1),a1),a5)),
% 63.13/63.21 inference(scs_inference,[],[620,564,16])).
% 63.13/63.21 cnf(1186,plain,
% 63.13/63.21 (P2(a5,f3(f7(x11861),f3(a4,a1)))),
% 63.13/63.21 inference(scs_inference,[],[615,1168,19])).
% 63.13/63.21 cnf(1187,plain,
% 63.13/63.21 (P1(f3(f3(a4,a1),a1),a4)),
% 63.13/63.21 inference(scs_inference,[],[628,566,16])).
% 63.13/63.21 cnf(1227,plain,
% 63.13/63.21 (~P2(f3(f3(f3(a4,a1),a1),a1),a4)),
% 63.13/63.21 inference(scs_inference,[],[644,566,1086,433,17,16,13])).
% 63.13/63.21 cnf(1232,plain,
% 63.13/63.21 (P1(a4,f3(f3(f3(a4,a1),a1),a1))+P2(a4,f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1227,12])).
% 63.13/63.21 cnf(1236,plain,
% 63.13/63.21 (P2(a4,f3(f3(f3(a4,a1),a1),a1))+P1(f3(a5,a1),f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[604,1227,12,13,16])).
% 63.13/63.21 cnf(1248,plain,
% 63.13/63.21 (P1(a1,f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[672,894,16])).
% 63.13/63.21 cnf(1250,plain,
% 63.13/63.21 (~P2(a1,f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[672,894,16,13])).
% 63.13/63.21 cnf(1253,plain,
% 63.13/63.21 (P1(a1,f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[672,917,16])).
% 63.13/63.21 cnf(1255,plain,
% 63.13/63.21 (~P2(a1,f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[672,917,16,13])).
% 63.13/63.21 cnf(1257,plain,
% 63.13/63.21 (P1(f3(f2(x12571,a1),a1),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[154,1253,16])).
% 63.13/63.21 cnf(1262,plain,
% 63.13/63.21 (P1(a1,f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[672,3,16])).
% 63.13/63.21 cnf(1265,plain,
% 63.13/63.21 (~P2(a1,f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[672,3,16,13])).
% 63.13/63.21 cnf(1268,plain,
% 63.13/63.21 (P1(f3(f2(x12681,a1),a1),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[154,1262,16])).
% 63.13/63.21 cnf(1270,plain,
% 63.13/63.21 (~P2(f3(f2(x12701,a1),a1),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[154,1262,16,13])).
% 63.13/63.21 cnf(1273,plain,
% 63.13/63.21 (P1(f2(a1,f7(a1)),f2(x12731,a1))),
% 63.13/63.21 inference(scs_inference,[],[673,887,16])).
% 63.13/63.21 cnf(1280,plain,
% 63.13/63.21 (P1(f2(a1,f7(a1)),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[673,894,16])).
% 63.13/63.21 cnf(1284,plain,
% 63.13/63.21 (P1(f3(a1,a1),f2(a1,f7(a1)))+P2(f3(a1,a1),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[673,894,16,13,12])).
% 63.13/63.21 cnf(1288,plain,
% 63.13/63.21 (~P2(f2(a1,f7(a1)),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[673,917,16,13])).
% 63.13/63.21 cnf(1290,plain,
% 63.13/63.21 (P2(f3(a1,a1),f2(a1,f7(a1)))+P1(f3(a1,a1),f3(f2(a1,f7(a1)),a1))),
% 63.13/63.21 inference(scs_inference,[],[673,1284,16])).
% 63.13/63.21 cnf(1311,plain,
% 63.13/63.21 (~P2(f3(f7(x13111),f7(x13112)),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[710,26,17])).
% 63.13/63.21 cnf(1321,plain,
% 63.13/63.21 (P1(a5,f3(a5,a1))),
% 63.13/63.21 inference(scs_inference,[],[566,1119,16])).
% 63.13/63.21 cnf(1323,plain,
% 63.13/63.21 (~P2(a5,f3(a5,a1))),
% 63.13/63.21 inference(scs_inference,[],[566,1119,16,13])).
% 63.13/63.21 cnf(1326,plain,
% 63.13/63.21 (P1(f3(f3(f3(a4,a1),a1),a1),f3(a5,a1))),
% 63.13/63.21 inference(scs_inference,[],[644,1321,16])).
% 63.13/63.21 cnf(1330,plain,
% 63.13/63.21 (P1(f3(a5,a1),f3(f3(f3(a4,a1),a1),a1))+P2(f3(a5,a1),f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[644,1321,16,13,12])).
% 63.13/63.21 cnf(1340,plain,
% 63.13/63.21 (P2(f3(f2(a1,a1),a1),f3(f7(x13401),f7(x13402)))+P1(f3(f2(a1,f7(a1)),a1),f3(f7(x13401),f7(x13402)))),
% 63.13/63.21 inference(scs_inference,[],[735,169,26,17,12,13,16])).
% 63.13/63.21 cnf(1348,plain,
% 63.13/63.21 (~P2(a1,f2(a1,f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[752,865,16,13])).
% 63.13/63.21 cnf(1361,plain,
% 63.13/63.21 (P1(a4,f3(f3(f3(a4,a1),a1),a1))+P2(f3(a5,a1),f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1119,1330,16])).
% 63.13/63.21 cnf(1377,plain,
% 63.13/63.21 (~P2(a4,f3(f3(f3(a4,a1),a1),a1))+P2(f3(a5,a1),f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1361,13])).
% 63.13/63.21 cnf(1389,plain,
% 63.13/63.21 (~P1(f3(a5,a1),f3(f3(f3(a4,a1),a1),a1))+~P2(a4,f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1377,13])).
% 63.13/63.21 cnf(1390,plain,
% 63.13/63.21 (~P2(a4,f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1326,1389,11])).
% 63.13/63.21 cnf(1391,plain,
% 63.13/63.21 (P1(a4,f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1390,1232])).
% 63.13/63.21 cnf(1392,plain,
% 63.13/63.21 (P1(f3(a5,a1),f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1390,1236])).
% 63.13/63.21 cnf(1397,plain,
% 63.13/63.21 (P2(f2(a1,a1),f3(f7(x13971),f7(x13972)))+P1(f2(f3(a1,a1),f7(a1)),f3(f7(x13971),f7(x13972)))),
% 63.13/63.21 inference(scs_inference,[],[776,278,86,17,12,16])).
% 63.13/63.21 cnf(1407,plain,
% 63.13/63.21 (~P2(f3(a5,a1),f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1392,13])).
% 63.13/63.21 cnf(1412,plain,
% 63.13/63.21 (P1(a5,f3(f3(f3(a4,a1),a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[776,566,1391,1392,26,13,17,16])).
% 63.13/63.21 cnf(1424,plain,
% 63.13/63.21 (P2(f2(a1,a1),f3(f7(x14241),f3(f7(x14242),f7(x14243))))+P1(f2(f3(a1,a1),f7(a1)),f3(f7(x14241),f3(f7(x14242),f7(x14243))))),
% 63.13/63.21 inference(scs_inference,[],[776,278,1412,93,13,17,12,16])).
% 63.13/63.21 cnf(1428,plain,
% 63.13/63.21 (P1(f2(x14281,a1),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[784,40,16])).
% 63.13/63.21 cnf(1431,plain,
% 63.13/63.21 (~P2(f2(x14311,a1),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[784,40,16,13])).
% 63.13/63.21 cnf(1438,plain,
% 63.13/63.21 (~P1(f2(a1,a1),f3(f7(x14381),f7(x14382)))+P1(f2(f3(a1,a1),f7(a1)),f3(f7(x14381),f7(x14382)))),
% 63.13/63.21 inference(scs_inference,[],[1397,13])).
% 63.13/63.21 cnf(1439,plain,
% 63.13/63.21 (P1(f2(x14391,a1),f3(f2(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[784,75,16])).
% 63.13/63.21 cnf(1442,plain,
% 63.13/63.21 (~P2(f2(x14421,a1),f3(f2(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[784,75,16,13])).
% 63.13/63.21 cnf(1445,plain,
% 63.13/63.21 (P1(f2(x14451,a1),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[784,830,16])).
% 63.13/63.21 cnf(1447,plain,
% 63.13/63.21 (~P2(f2(x14471,a1),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[784,830,16,13])).
% 63.13/63.21 cnf(1449,plain,
% 63.13/63.21 (P1(f3(a1,a1),f2(x14491,a1))+P2(f3(a1,a1),f2(x14491,a1))),
% 63.13/63.21 inference(scs_inference,[],[784,830,16,13,12])).
% 63.13/63.21 cnf(1451,plain,
% 63.13/63.21 (P1(f3(a1,a1),f2(x14511,a1))+P1(f3(f7(f8(f2(x14511,a1),f3(a1,a1))),f3(a1,a1)),f2(x14511,a1))),
% 63.13/63.21 inference(scs_inference,[],[1449,21])).
% 63.13/63.21 cnf(1452,plain,
% 63.13/63.21 (P1(f2(x14521,a1),f2(x14522,a1))),
% 63.13/63.21 inference(scs_inference,[],[784,782,16])).
% 63.13/63.21 cnf(1454,plain,
% 63.13/63.21 (~P2(f2(x14541,a1),f2(x14542,a1))),
% 63.13/63.21 inference(scs_inference,[],[784,782,16,13])).
% 63.13/63.21 cnf(1460,plain,
% 63.13/63.21 (~P2(f2(x14601,a1),f3(f2(a1,f7(a1)),a1))),
% 63.13/63.21 inference(scs_inference,[],[784,6,16,13])).
% 63.13/63.21 cnf(1491,plain,
% 63.13/63.21 (P2(f2(a1,f7(f7(a1))),f3(f7(x14911),f2(x14912,a1)))),
% 63.13/63.21 inference(scs_inference,[],[786,790,26,17,12])).
% 63.13/63.21 cnf(1493,plain,
% 63.13/63.21 (~P2(f3(f7(x14931),f2(x14932,a1)),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1491,49,17])).
% 63.13/63.21 cnf(1507,plain,
% 63.13/63.21 (~P2(f2(f3(f3(a1,a1),a1),f7(a1)),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[796,1428,16,13])).
% 63.13/63.21 cnf(1512,plain,
% 63.13/63.21 (~P2(f3(f7(x15121),f2(x15122,a1)),f2(x15123,a1))),
% 63.13/63.21 inference(scs_inference,[],[802,1491,17])).
% 63.13/63.21 cnf(1527,plain,
% 63.13/63.21 (~P1(f3(f2(a1,a1),a1),f3(f7(x15271),f7(x15272)))+P1(f3(f2(a1,f7(a1)),a1),f3(f7(x15271),f7(x15272)))),
% 63.13/63.21 inference(scs_inference,[],[1340,13])).
% 63.13/63.21 cnf(1533,plain,
% 63.13/63.21 (P1(f3(a1,a1),f2(x15331,a1))),
% 63.13/63.21 inference(scs_inference,[],[784,833,1451,16])).
% 63.13/63.21 cnf(1534,plain,
% 63.13/63.21 (~P2(f3(a1,a1),f2(x15341,a1))),
% 63.13/63.21 inference(scs_inference,[],[1533,13])).
% 63.13/63.21 cnf(1539,plain,
% 63.13/63.21 (~P2(f3(f7(x15391),f7(x15392)),f3(f2(x15393,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[820,86,17])).
% 63.13/63.21 cnf(1547,plain,
% 63.13/63.21 (~P2(f3(f7(x15471),a1),f3(f2(x15472,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[820,26,17])).
% 63.13/63.21 cnf(1550,plain,
% 63.13/63.21 (P1(f3(f2(x15501,a1),a1),f3(f7(x15502),a1))+P2(f3(f2(x15501,a1),a1),f3(f7(x15502),a1))),
% 63.13/63.21 inference(scs_inference,[],[820,26,17,12])).
% 63.13/63.21 cnf(1554,plain,
% 63.13/63.21 (P2(f3(f2(a1,a1),a1),f3(f7(x15541),a1))+P1(f3(f2(a1,f7(a1)),a1),f3(f7(x15541),a1))),
% 63.13/63.21 inference(scs_inference,[],[820,169,26,17,12,13,16])).
% 63.13/63.21 cnf(1569,plain,
% 63.13/63.21 (P1(f3(f7(x15691),a1),f3(f2(a1,f7(a1)),a1))+P2(f3(f2(a1,a1),a1),f3(f7(x15691),a1))),
% 63.13/63.21 inference(scs_inference,[],[1554,11])).
% 63.13/63.21 cnf(1570,plain,
% 63.13/63.21 (~P1(f3(f2(a1,a1),a1),f3(f7(x15701),a1))+P1(f3(f7(x15701),a1),f3(f2(a1,f7(a1)),a1))),
% 63.13/63.21 inference(scs_inference,[],[1569,13])).
% 63.13/63.21 cnf(1571,plain,
% 63.13/63.21 (P1(f3(a1,a1),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[831,40,16])).
% 63.13/63.21 cnf(1574,plain,
% 63.13/63.21 (~P2(f3(a1,a1),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[831,40,16,13])).
% 63.13/63.21 cnf(1576,plain,
% 63.13/63.21 (P1(f3(a1,a1),f3(f2(a1,f7(a1)),a1))),
% 63.13/63.21 inference(scs_inference,[],[831,40,16,13,1290])).
% 63.13/63.21 cnf(1578,plain,
% 63.13/63.21 (~P1(f3(f2(a1,a1),a1),f3(f7(x15781),a1))),
% 63.13/63.21 inference(scs_inference,[],[671,1570,19])).
% 63.13/63.21 cnf(1579,plain,
% 63.13/63.21 (P2(f3(f2(a1,a1),a1),f3(f7(x15791),a1))),
% 63.13/63.21 inference(scs_inference,[],[1578,1550])).
% 63.13/63.21 cnf(1585,plain,
% 63.13/63.21 (P1(f3(a1,a1),f2(f3(f2(x15851,a1),a1),f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[831,1576,968,1578,1550,11,13,16])).
% 63.13/63.21 cnf(1592,plain,
% 63.13/63.21 (P1(f3(f2(a1,f7(a1)),a1),f3(f7(x15921),f7(x15922)))+~P1(f3(f7(x15921),f7(x15922)),f3(f2(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1527,11])).
% 63.13/63.21 cnf(1596,plain,
% 63.13/63.21 (P2(f2(a1,f7(f7(a1))),f3(f7(x15961),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[832,825,26,17,12])).
% 63.13/63.21 cnf(1599,plain,
% 63.13/63.21 (~P2(f3(f7(x15991),f3(a1,a1)),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1596,49,17])).
% 63.13/63.21 cnf(1610,plain,
% 63.13/63.21 (P1(f3(f7(x16101),f7(x16102)),f3(f2(a1,f7(a1)),a1))+~P1(f3(f7(x16101),f7(x16102)),f3(f2(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1592,11])).
% 63.13/63.21 cnf(1612,plain,
% 63.13/63.21 (P1(f3(a1,a1),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[840,1257,16])).
% 63.13/63.21 cnf(1615,plain,
% 63.13/63.21 (~P2(f3(a1,a1),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[840,1257,16,13])).
% 63.13/63.21 cnf(1617,plain,
% 63.13/63.21 (~P1(f3(f7(x16171),f7(x16172)),f3(f2(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[674,1610,19])).
% 63.13/63.21 cnf(1618,plain,
% 63.13/63.21 (~P1(f3(f2(a1,a1),a1),f3(f7(x16181),f7(x16182)))),
% 63.13/63.21 inference(scs_inference,[],[1617,11])).
% 63.13/63.21 cnf(1620,plain,
% 63.13/63.21 (P2(f3(f2(a1,a1),a1),f3(f7(x16201),f7(x16202)))),
% 63.13/63.21 inference(scs_inference,[],[1617,1539,11,12])).
% 63.13/63.21 cnf(1653,plain,
% 63.13/63.21 (P2(f3(a1,a1),f3(f7(x16531),a1))),
% 63.13/63.21 inference(scs_inference,[],[863,838,1579,1578,17,12,13,16])).
% 63.13/63.21 cnf(1657,plain,
% 63.13/63.21 (P1(f3(a1,a1),f3(f7(x16571),f7(x16572)))+P2(f3(a1,a1),f3(f7(x16571),f7(x16572)))),
% 63.13/63.21 inference(scs_inference,[],[863,1620,17,12])).
% 63.13/63.21 cnf(1674,plain,
% 63.13/63.21 (~P2(f3(f7(x16741),f2(x16742,a1)),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[868,1491,17])).
% 63.13/63.21 cnf(1686,plain,
% 63.13/63.21 (P2(f3(a1,a1),f3(f7(x16861),f7(x16862)))),
% 63.13/63.21 inference(scs_inference,[],[838,1618,1657,16])).
% 63.13/63.21 cnf(1746,plain,
% 63.13/63.21 (P1(f2(a1,f7(x17461)),f3(f2(f2(x17462,a1),x17461),f2(x17462,a1)))),
% 63.13/63.21 inference(scs_inference,[],[968,353,16])).
% 63.13/63.21 cnf(1754,plain,
% 63.13/63.21 (P1(f2(a1,x17541),f2(f2(x17542,a1),x17541))),
% 63.13/63.21 inference(scs_inference,[],[968,120,16])).
% 63.13/63.21 cnf(1757,plain,
% 63.13/63.21 (~P2(f2(a1,x17571),f2(f2(x17572,a1),x17571))),
% 63.13/63.21 inference(scs_inference,[],[968,120,16,13])).
% 63.13/63.21 cnf(1759,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(x17591)),f2(f2(x17592,a1),x17591))),
% 63.13/63.21 inference(scs_inference,[],[278,1754,16])).
% 63.13/63.21 cnf(1766,plain,
% 63.13/63.21 (~P2(f3(f7(x17661),f2(a1,x17662)),f2(f3(f2(x17663,a1),a1),x17662))),
% 63.13/63.21 inference(scs_inference,[],[969,26,17])).
% 63.13/63.21 cnf(1789,plain,
% 63.13/63.21 (~P2(f3(a1,a1),f3(f3(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1002,10,20])).
% 63.13/63.21 cnf(1795,plain,
% 63.13/63.21 (P1(f3(a1,a1),f3(f3(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1686,1789,24,17,12])).
% 63.13/63.21 cnf(1805,plain,
% 63.13/63.21 (P1(f3(f2(x18051,a1),a1),f3(f3(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[838,1653,1795,1789,17,16])).
% 63.13/63.21 cnf(1812,plain,
% 63.13/63.21 (P1(a1,f3(f3(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[752,1805,16])).
% 63.13/63.21 cnf(1815,plain,
% 63.13/63.21 (~P2(a1,f3(f3(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[752,1805,16,13])).
% 63.13/63.21 cnf(1834,plain,
% 63.13/63.21 (P1(f3(f3(a1,a1),a1),a1)+P2(f3(f3(a1,a1),a1),a1)),
% 63.13/63.21 inference(scs_inference,[],[1815,12])).
% 63.13/63.21 cnf(1847,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f2(f3(f2(x18471,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1006,971,385,1815,17,16])).
% 63.13/63.21 cnf(1856,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f2(f2(x18561,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1006,1042,1759,1815,17,16])).
% 63.13/63.21 cnf(1864,plain,
% 63.13/63.21 (~P2(f7(x18641),f3(f3(a1,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[51,1815,17])).
% 63.13/63.21 cnf(1866,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f3(f2(f3(a1,a1),f7(a1)),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1006,6,51,1815,17,16])).
% 63.13/63.21 cnf(1875,plain,
% 63.13/63.21 (P1(f3(f3(a1,a1),a1),f7(x18751))+P2(f3(f3(a1,a1),a1),f7(x18751))),
% 63.13/63.21 inference(scs_inference,[],[93,1815,1864,17,12])).
% 63.13/63.21 cnf(1881,plain,
% 63.13/63.21 (P2(f3(f3(a1,a1),a1),f7(x18811))),
% 63.13/63.21 inference(scs_inference,[],[1812,35,1875,16])).
% 63.13/63.21 cnf(1931,plain,
% 63.13/63.21 (~P1(f2(a1,a1),f3(f7(x19311),f3(f7(x19312),f7(x19313))))+P1(f2(f3(a1,a1),f7(a1)),f3(f7(x19311),f3(f7(x19312),f7(x19313))))),
% 63.13/63.21 inference(scs_inference,[],[1424,13])).
% 63.13/63.21 cnf(1932,plain,
% 63.13/63.21 (P1(f2(f3(f2(x19321,a1),a1),f7(a1)),a1)),
% 63.13/63.21 inference(scs_inference,[],[1105,54,16])).
% 63.13/63.21 cnf(1940,plain,
% 63.13/63.21 (P1(f2(f3(f2(x19401,a1),a1),f7(x19402)),f2(a1,x19402))),
% 63.13/63.21 inference(scs_inference,[],[1105,40,16])).
% 63.13/63.21 cnf(1947,plain,
% 63.13/63.21 (P1(f2(f3(f2(x19471,a1),a1),f7(a1)),f3(a1,a1))),
% 63.13/63.21 inference(scs_inference,[],[1105,1280,16])).
% 63.13/63.21 cnf(1961,plain,
% 63.13/63.21 (P1(f2(f3(f2(x19611,a1),a1),f7(a1)),f2(x19612,a1))),
% 63.13/63.21 inference(scs_inference,[],[1105,1273,16])).
% 63.13/63.21 cnf(2015,plain,
% 63.13/63.21 (~P2(f2(a1,f7(a1)),f3(f2(x20151,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[54,752,16,13])).
% 63.13/63.21 cnf(2044,plain,
% 63.13/63.21 (P1(f2(a4,x20441),f2(a5,x20441))),
% 63.13/63.21 inference(scs_inference,[],[1111,120,16])).
% 63.13/63.21 cnf(2047,plain,
% 63.13/63.21 (~P2(f2(a4,x20471),f2(a5,x20471))),
% 63.13/63.21 inference(scs_inference,[],[1111,120,16,13])).
% 63.13/63.21 cnf(2053,plain,
% 63.13/63.21 (P1(f3(f2(f3(a4,a1),x20531),a1),f2(a5,x20531))),
% 63.13/63.21 inference(scs_inference,[],[1112,140,1086,2044,17,16])).
% 63.13/63.21 cnf(2062,plain,
% 63.13/63.21 (~P2(f3(f7(x20621),f2(a4,x20622)),f2(f3(a5,a1),x20622))),
% 63.13/63.21 inference(scs_inference,[],[1112,26,17])).
% 63.13/63.21 cnf(2179,plain,
% 63.13/63.21 (P1(f3(f3(a4,a1),a1),f3(a5,a1))),
% 63.13/63.21 inference(scs_inference,[],[1187,1119,16])).
% 63.13/63.21 cnf(2201,plain,
% 63.13/63.21 (P1(a1,f2(f3(f2(x22011,a1),a1),f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[1248,1585,16])).
% 63.13/63.21 cnf(2203,plain,
% 63.13/63.21 (~P2(a1,f2(f3(f2(x22031,a1),a1),f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[1248,1585,16,13])).
% 63.13/63.21 cnf(2221,plain,
% 63.13/63.21 (P2(f3(a1,a1),f3(f7(x22211),f3(f7(x22212),f7(x22213))))+P1(f2(f3(a1,a1),f7(a1)),f3(f7(x22211),f3(f7(x22212),f7(x22213))))),
% 63.13/63.21 inference(scs_inference,[],[1250,846,93,17,12,13,16])).
% 63.13/63.21 cnf(2224,plain,
% 63.13/63.21 (P1(a1,f2(f3(a1,a1),f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[1253,1006,16])).
% 63.13/63.21 cnf(2229,plain,
% 63.13/63.21 (P1(a1,f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1253,1003,16])).
% 63.13/63.21 cnf(2231,plain,
% 63.13/63.21 (~P2(a1,f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1253,1003,16,13])).
% 63.13/63.21 cnf(2233,plain,
% 63.13/63.21 (P1(f7(a1),f7(f2(f3(f3(a1,a1),a1),f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[2231,374])).
% 63.13/63.21 cnf(2236,plain,
% 63.13/63.21 (P1(a1,f3(f2(f3(a1,a1),f7(a1)),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1253,1866,2233,13,16])).
% 63.13/63.21 cnf(2243,plain,
% 63.13/63.21 (P1(a1,f2(f2(x22431,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1253,1856,2236,13,16])).
% 63.13/63.21 cnf(2250,plain,
% 63.13/63.21 (P1(a1,f2(f3(f2(x22501,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1253,1847,2243,13,16])).
% 63.13/63.21 cnf(2255,plain,
% 63.13/63.21 (~P2(a1,f2(f3(f2(x22551,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[2250,13])).
% 63.13/63.21 cnf(2257,plain,
% 63.13/63.21 (P1(f2(a1,f7(a1)),f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[54,2229,2250,13,16])).
% 63.13/63.21 cnf(2261,plain,
% 63.13/63.21 (P1(f2(a1,f7(a1)),f2(f3(a1,a1),f7(f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[54,2257,2224,13,16])).
% 63.13/63.21 cnf(2267,plain,
% 63.13/63.21 (P1(f2(a1,f7(a1)),f3(f2(f3(a1,a1),f7(a1)),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[54,2261,2236,13,16])).
% 63.13/63.21 cnf(2272,plain,
% 63.13/63.21 (P1(a1,f3(f2(f3(a1,a1),a1),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1253,2267,6,13,16])).
% 63.13/63.21 cnf(2280,plain,
% 63.13/63.21 (P1(f2(a1,f7(a1)),f3(f2(f3(a1,a1),a1),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[54,2272,13,16])).
% 63.13/63.21 cnf(2285,plain,
% 63.13/63.21 (~P2(f2(a1,f7(a1)),f3(f2(f3(a1,a1),a1),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[2280,13])).
% 63.13/63.21 cnf(2291,plain,
% 63.13/63.21 (~P2(f3(f7(x22911),f2(a1,f7(a1))),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1255,385,17])).
% 63.13/63.21 cnf(2306,plain,
% 63.13/63.21 (~P2(f3(f7(x23061),f7(x23062)),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1255,86,17])).
% 63.13/63.21 cnf(2308,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),f7(a1)),f3(f7(x23081),f7(x23082)))+P2(f2(f3(a1,a1),f7(a1)),f3(f7(x23081),f7(x23082)))),
% 63.13/63.21 inference(scs_inference,[],[1255,86,17,12])).
% 63.13/63.21 cnf(2313,plain,
% 63.13/63.21 (~P2(f3(f7(x23131),a1),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1255,26,17])).
% 63.13/63.21 cnf(2321,plain,
% 63.13/63.21 (~P2(f3(f7(x23211),f3(f7(x23212),f7(x23213))),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1255,93,17])).
% 63.13/63.21 cnf(2333,plain,
% 63.13/63.21 (P1(f3(f2(x23331,a1),a1),f2(f3(f3(a1,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1257,1003,16])).
% 63.13/63.21 cnf(2337,plain,
% 63.13/63.21 (P1(f3(f2(x23371,a1),a1),f3(f2(f3(a1,a1),f7(a1)),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1257,1866,16])).
% 63.13/63.21 cnf(2339,plain,
% 63.13/63.21 (~P2(f3(f2(x23391,a1),a1),f3(f2(f3(a1,a1),f7(a1)),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1257,1866,16,13])).
% 63.13/63.21 cnf(2343,plain,
% 63.13/63.21 (P2(f2(f3(a1,a1),f7(a1)),f3(f7(x23431),f7(x23432)))),
% 63.13/63.21 inference(scs_inference,[],[1257,1618,2308,16])).
% 63.13/63.21 cnf(2344,plain,
% 63.13/63.21 (P1(f3(f2(x23441,a1),a1),f2(f2(x23442,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1257,1856,16])).
% 63.13/63.21 cnf(2346,plain,
% 63.13/63.21 (~P2(f3(f2(x23461,a1),a1),f2(f2(x23462,a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1257,1856,16,13])).
% 63.13/63.21 cnf(2353,plain,
% 63.13/63.21 (~P2(f3(f2(x23531,a1),a1),f2(f3(f2(x23532,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1257,1847,16,13])).
% 63.13/63.21 cnf(2358,plain,
% 63.13/63.21 (~P2(f3(f2(x23581,a1),a1),f3(f2(f3(a1,a1),a1),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1257,6,16,13])).
% 63.13/63.21 cnf(2365,plain,
% 63.13/63.21 (P1(a1,f3(f2(f2(x23651,a1),a1),f2(x23651,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1262,1746,16])).
% 63.13/63.21 cnf(2373,plain,
% 63.13/63.21 (~P2(f3(f7(x23731),f3(f2(x23732,a1),a1)),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1265,1042,17])).
% 63.13/63.21 cnf(2381,plain,
% 63.13/63.21 (~P2(f3(f7(x23811),a1),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1265,26,17])).
% 63.13/63.21 cnf(2392,plain,
% 63.13/63.21 (~P2(f3(f7(x23921),f3(f7(x23922),f7(x23923))),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1265,93,17])).
% 63.13/63.21 cnf(2400,plain,
% 63.13/63.21 (P1(f3(f2(x24001,a1),a1),f3(f2(f2(x24002,a1),a1),f2(x24002,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1268,1746,16])).
% 63.13/63.21 cnf(2403,plain,
% 63.13/63.21 (~P2(f3(f2(x24031,a1),a1),f3(f2(f2(x24032,a1),a1),f2(x24032,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1268,1746,16,13])).
% 63.13/63.21 cnf(2425,plain,
% 63.13/63.21 (~P1(f3(a1,a1),f3(f7(x24251),f3(f7(x24252),f7(x24253))))+P1(f2(f3(a1,a1),f7(a1)),f3(f7(x24251),f3(f7(x24252),f7(x24253))))),
% 63.13/63.21 inference(scs_inference,[],[2221,13])).
% 63.13/63.21 cnf(2428,plain,
% 63.13/63.21 (P2(a1,f3(f7(x24281),f3(f7(x24282),f3(a1,a1))))),
% 63.13/63.21 inference(scs_inference,[],[2365,1599,18,553])).
% 63.13/63.21 cnf(2430,plain,
% 63.13/63.21 (P1(f3(f7(f8(f7(x24301),f2(a1,a1))),f2(a1,a1)),f7(x24301))),
% 63.13/63.21 inference(scs_inference,[],[2365,1599,730,18,553,21])).
% 63.13/63.21 cnf(2432,plain,
% 63.13/63.21 (P1(f7(a1),f7(f3(f2(f2(x24321,a1),a1),f2(x24321,a1))))),
% 63.13/63.21 inference(scs_inference,[],[2365,1599,730,18,553,21,14])).
% 63.13/63.21 cnf(2438,plain,
% 63.13/63.21 (P1(f3(f2(f2(x24381,a1),a1),f2(x24381,a1)),f3(f2(x24382,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[1323,2400,2365,1023,1599,730,18,553,21,14,19,15,11])).
% 63.13/63.21 cnf(2442,plain,
% 63.13/63.21 (~P2(f3(f3(a1,a1),a1),a1)),
% 63.13/63.21 inference(scs_inference,[],[1323,2400,511,2365,1023,1507,1599,730,10,18,553,21,14,19,15,11,13,20])).
% 63.13/63.21 cnf(2451,plain,
% 63.13/63.21 (P1(f3(f3(a1,a1),a1),a1)),
% 63.13/63.21 inference(scs_inference,[],[1323,2400,511,2365,1123,1023,1507,1599,1087,730,4,5,10,18,553,21,14,19,15,11,13,20,17,16,1834])).
% 63.13/63.21 cnf(2452,plain,
% 63.13/63.21 (P1(f3(f7(x24521),f3(f7(x24522),f7(x24523))),f2(a1,f7(a1)))+P2(f2(a1,f7(a1)),f3(f7(x24521),f3(f7(x24522),f7(x24523))))),
% 63.13/63.21 inference(scs_inference,[],[1323,2400,511,2365,2392,1123,1023,1507,1599,1087,730,4,5,10,18,553,21,14,19,15,11,13,20,17,16,1834,12])).
% 63.13/63.21 cnf(2455,plain,
% 63.13/63.21 (P2(f2(a1,f7(a1)),f3(f7(x24551),f3(f7(x24552),f7(x24553))))),
% 63.13/63.21 inference(scs_inference,[],[1311,2452,19])).
% 63.13/63.21 cnf(2456,plain,
% 63.13/63.21 (P1(f2(f3(f3(a1,a1),a1),x24561),f2(a1,x24561))),
% 63.13/63.21 inference(scs_inference,[],[2451,18])).
% 63.13/63.21 cnf(2458,plain,
% 63.13/63.21 (P1(f7(f3(f3(a1,a1),a1)),f7(a1))),
% 63.13/63.21 inference(scs_inference,[],[2451,18,14])).
% 63.13/63.21 cnf(2460,plain,
% 63.13/63.21 (P1(f3(f7(f8(f2(a4,a6),f2(a5,a6))),f2(a5,a6)),f2(a4,a6))),
% 63.13/63.21 inference(scs_inference,[],[2451,4,18,14,21])).
% 63.13/63.21 cnf(2462,plain,
% 63.13/63.21 (~P1(f3(f7(x24621),f3(a1,a1)),f2(x24622,a1))),
% 63.13/63.21 inference(scs_inference,[],[1534,2451,4,18,14,21,19])).
% 63.13/63.21 cnf(2478,plain,
% 63.13/63.21 (P1(f2(f3(f3(a4,a1),a1),x24781),f2(f3(a5,a1),x24781))),
% 63.13/63.21 inference(scs_inference,[],[2179,18])).
% 63.13/63.21 cnf(2480,plain,
% 63.13/63.21 (P1(f7(f3(f3(a4,a1),a1)),f7(f3(a5,a1)))),
% 63.13/63.21 inference(scs_inference,[],[2179,18,14])).
% 63.13/63.21 cnf(2482,plain,
% 63.13/63.21 (~P1(f3(f7(x24821),f2(a4,x24822)),f2(a5,x24822))),
% 63.13/63.21 inference(scs_inference,[],[2047,2179,18,14,19])).
% 63.13/63.21 cnf(2486,plain,
% 63.13/63.21 (P1(f2(a1,x24861),f2(f3(f3(a1,a1),a1),x24861))),
% 63.13/63.21 inference(scs_inference,[],[2047,2462,2456,2179,18,14,19,15,11])).
% 63.13/63.21 cnf(2490,plain,
% 63.13/63.21 (~P1(f2(f2(x24901,a1),f7(a1)),a6)),
% 63.13/63.21 inference(scs_inference,[],[2047,2462,2456,2428,2344,2179,1078,18,14,19,15,11,13,16])).
% 63.13/63.21 cnf(2502,plain,
% 63.13/63.21 (~P1(f3(f7(x25021),f7(x25022)),a1)),
% 63.13/63.21 inference(scs_inference,[],[429,2482,1947,18,14,15,19])).
% 63.13/63.21 cnf(2504,plain,
% 63.13/63.21 (P1(f7(a1),f7(f3(f3(a1,a1),a1)))),
% 63.13/63.21 inference(scs_inference,[],[429,2482,2458,1947,18,14,15,19,11])).
% 63.13/63.21 cnf(2506,plain,
% 63.13/63.21 (~P1(f2(a1,f7(a1)),f3(f7(x25061),f3(f7(x25062),f7(x25063))))),
% 63.13/63.21 inference(scs_inference,[],[429,2482,2458,2455,1947,18,14,15,19,11,13])).
% 63.13/63.21 cnf(2508,plain,
% 63.13/63.21 (~P1(f3(f2(x25081,a1),a1),f3(f7(x25082),f2(f3(f2(x25083,a1),a1),f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[429,2482,2458,2438,2455,1947,1020,18,14,15,19,11,13,16])).
% 63.13/63.21 cnf(2519,plain,
% 63.13/63.21 (~P1(f3(f7(x25191),f3(a1,a1)),f2(a1,f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[1574,1940,18,14,19])).
% 63.13/63.21 cnf(2523,plain,
% 63.13/63.21 (P1(f2(a4,a6),f3(f7(f8(f2(a4,a6),f2(a5,a6))),f2(a5,a6)))),
% 63.13/63.21 inference(scs_inference,[],[1574,2502,2460,1940,18,14,19,15,11])).
% 63.13/63.21 cnf(2525,plain,
% 63.13/63.21 (~P1(f2(f3(a1,a1),f7(a1)),f3(f7(x25251),f7(x25252)))),
% 63.13/63.21 inference(scs_inference,[],[1574,2502,2460,2343,1940,18,14,19,15,11,13])).
% 63.13/63.21 cnf(2530,plain,
% 63.13/63.21 (P2(f2(a5,a1),f3(f7(x25301),f2(a4,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1574,2502,2486,2460,2506,2343,1940,2482,1512,18,14,19,15,11,13,16,12])).
% 63.13/63.21 cnf(2534,plain,
% 63.13/63.21 (P2(a1,f3(f7(x25341),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1574,2502,2486,2460,2506,2343,1940,2482,1512,18,14,19,15,11,13,16,12,258])).
% 63.13/63.21 cnf(2538,plain,
% 63.13/63.21 (~P1(f2(a1,a1),f3(f7(x25381),f7(x25382)))),
% 63.13/63.21 inference(scs_inference,[],[1574,2502,2486,2460,2506,2343,1940,2482,1512,18,14,19,15,11,13,16,12,258,1397,1438])).
% 63.13/63.21 cnf(2554,plain,
% 63.13/63.21 (~P1(f2(a5,a1),f3(f7(x25541),f2(a4,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1615,2530,2538,2478,1961,18,14,15,19,11,13])).
% 63.13/63.21 cnf(2558,plain,
% 63.13/63.21 (P2(f2(a1,f7(a1)),f3(f7(x25581),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1615,2530,2538,2519,2504,2478,1961,1010,1599,18,14,15,19,11,13,16,12])).
% 63.13/63.21 cnf(2561,plain,
% 63.13/63.21 (P1(f2(f2(f3(f2(x25611,a1),a1),f7(a1)),x25612),f2(a1,x25612))),
% 63.13/63.21 inference(scs_inference,[],[1932,18])).
% 63.13/63.21 cnf(2563,plain,
% 63.13/63.21 (P1(f7(f2(f3(f2(x25631,a1),a1),f7(a1))),f7(a1))),
% 63.13/63.21 inference(scs_inference,[],[1932,18,14])).
% 63.13/63.21 cnf(2571,plain,
% 63.13/63.21 (~P1(a1,f3(f7(x25711),f3(a1,a1)))),
% 63.13/63.21 inference(scs_inference,[],[2554,2442,2534,2480,1932,18,14,19,15,11,13])).
% 63.13/63.21 cnf(2573,plain,
% 63.13/63.21 (~P1(f2(x25731,a1),f3(f7(x25732),f2(a4,a1)))),
% 63.13/63.21 inference(scs_inference,[],[2554,2442,2534,2480,1932,1452,18,14,19,15,11,13,16])).
% 63.13/63.21 cnf(2580,plain,
% 63.13/63.21 (P1(f2(f3(a1,a1),x25801),f2(f2(f3(a1,a1),f7(a1)),x25801))),
% 63.13/63.21 inference(scs_inference,[],[1612,18])).
% 63.13/63.21 cnf(2582,plain,
% 63.13/63.21 (P1(f7(f3(a1,a1)),f7(f2(f3(a1,a1),f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[1612,18,14])).
% 63.13/63.21 cnf(2584,plain,
% 63.13/63.21 (~P1(f3(f7(x25841),f2(a1,f7(a1))),f3(f2(x25842,a1),a1))),
% 63.13/63.21 inference(scs_inference,[],[2015,1612,18,14,19])).
% 63.13/63.21 cnf(2599,plain,
% 63.13/63.21 (~P2(f3(f7(x25991),f3(a1,a1)),f2(f3(f2(x25992,a1),a1),f7(a1)))),
% 63.13/63.21 inference(scs_inference,[],[2573,2558,2015,2255,2561,2523,1612,2534,2062,1013,18,14,19,15,11,13,16,12,17])).
% 63.13/63.21 cnf(2603,plain,
% 63.13/63.21 (P1(f7(f3(a1,a1)),f7(f2(a1,f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[1571,18,14])).
% 63.13/63.21 cnf(2611,plain,
% 63.13/63.21 (~P1(f3(f3(a1,a1),a1),f7(x26111))),
% 63.13/63.21 inference(scs_inference,[],[2571,2599,2563,1881,1571,18,14,19,15,11,13])).
% 63.13/63.21 cnf(2615,plain,
% 63.13/63.21 (P2(f3(f2(x26151,a1),a1),f3(f7(x26152),f2(a1,f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[2571,2599,2563,2584,2201,1881,1571,844,18,14,19,15,11,13,16,12])).
% 63.13/63.21 cnf(2618,plain,
% 63.13/63.21 (P1(f2(f2(x26181,a1),x26182),f2(f3(f2(a1,a1),a1),x26182))),
% 63.13/63.21 inference(scs_inference,[],[1439,18])).
% 63.13/63.21 cnf(2620,plain,
% 63.13/63.21 (P1(f7(f2(x26201,a1)),f7(f3(f2(a1,a1),a1)))),
% 63.13/63.21 inference(scs_inference,[],[1439,18,14])).
% 63.13/63.21 cnf(2628,plain,
% 63.13/63.21 (~P1(f3(f2(x26281,a1),a1),f3(f7(x26282),f2(a1,f7(a1))))),
% 63.13/63.21 inference(scs_inference,[],[2611,1348,2580,2615,1439,18,14,19,15,11,13])).
% 63.13/63.21 cnf(2637,plain,
% 63.13/63.21 (P1(f2(a5,x26371),f2(a4,x26371))),
% 63.13/63.21 inference(scs_inference,[],[1048,18])).
% 63.13/63.21 cnf(2639,plain,
% 63.13/63.21 (P1(f7(a5),f7(a4))),
% 63.13/63.21 inference(scs_inference,[],[1048,18,14])).
% 63.13/63.21 cnf(2647,plain,
% 63.13/63.21 (~P1(a5,f3(f7(x26471),f3(a4,a1)))),
% 63.13/63.21 inference(scs_inference,[],[1390,2582,1186,1048,2490,18,14,19,15,11,13])).
% 63.13/63.21 cnf(2662,plain,
% 63.13/63.21 (P1(f7(a4),f7(a5))),
% 63.13/63.21 inference(scs_inference,[],[2637,2639,2647,1407,18,14,15,19,11])).
% 63.13/63.21 cnf(2673,plain,
% 63.13/63.21 (P1(f2(f7(a4),x26731),f2(f7(a5),x26731))),
% 63.13/63.21 inference(scs_inference,[],[2662,18])).
% 63.13/63.21 cnf(2694,plain,
% 63.13/63.21 (~P1(f7(a1),f7(f7(x26941)))),
% 63.13/63.21 inference(scs_inference,[],[2243,35,18,14,15])).
% 63.13/63.21 cnf(2707,plain,
% 63.13/63.21 (P1(f2(a1,x27071),f2(f2(f3(f3(a1,a1),a1),f7(a1)),x27071))),
% 63.13/63.21 inference(scs_inference,[],[2229,18])).
% 63.13/63.21 cnf(2717,plain,
% 63.13/63.21 (~P1(f3(a1,a1),f3(f7(x27171),f7(x27172)))),
% 63.13/63.21 inference(scs_inference,[],[2694,2673,2203,2229,1686,1452,18,14,19,15,11,13])).
% 63.13/63.21 cnf(2730,plain,
% 63.13/63.21 (~P1(f3(f7(x27301),f2(a1,x27302)),f2(f2(x27303,a1),x27302))),
% 63.13/63.21 inference(scs_inference,[],[2717,1757,1169,18,14,15,19])).
% 63.13/63.21 cnf(2744,plain,
% 63.13/63.21 (P1(f2(f2(f3(f3(a1,a1),a1),f7(a1)),x27441),f2(f3(a1,a1),x27441))),
% 63.13/63.21 inference(scs_inference,[],[983,18])).
% 63.13/63.21 cnf(2761,plain,
% 63.13/63.21 (P1(f2(f3(a4,a1),x27611),f2(a5,x27611))),
% 63.13/63.21 inference(scs_inference,[],[612,18])).
% 63.13/63.21 cnf(2763,plain,
% 63.13/63.21 (P1(f7(f3(a4,a1)),f7(a5))),
% 63.13/63.22 inference(scs_inference,[],[612,18,14])).
% 63.13/63.22 cnf(2779,plain,
% 63.13/63.22 (P1(f2(f2(f3(a4,a1),x27791),x27792),f2(f2(a5,x27791),x27792))),
% 63.13/63.22 inference(scs_inference,[],[2761,18])).
% 63.13/63.22 cnf(2783,plain,
% 63.13/63.22 (~P1(f3(f7(x27831),f2(x27832,a1)),f2(a1,f7(a1)))),
% 63.13/63.22 inference(scs_inference,[],[2761,1431,18,14,19])).
% 63.13/63.22 cnf(2787,plain,
% 63.13/63.22 (P1(f2(a5,x27871),f2(f3(a4,a1),x27871))),
% 63.13/63.22 inference(scs_inference,[],[2761,1431,1010,18,14,19,15,11])).
% 63.13/63.22 cnf(2789,plain,
% 63.13/63.22 (~P1(f2(a5,a6),f3(f7(x27891),f3(f7(x27892),f2(a4,a6))))),
% 63.13/63.22 inference(scs_inference,[],[2761,1431,58,1010,18,14,19,15,11,13])).
% 63.13/63.22 cnf(2791,plain,
% 63.13/63.22 (P2(f2(a1,f7(a1)),f3(f7(x27911),f2(x27912,a1)))),
% 63.13/63.22 inference(scs_inference,[],[2761,1431,1493,58,1010,18,14,19,15,11,13,12])).
% 63.13/63.22 cnf(2794,plain,
% 63.13/63.22 (~P1(f7(x27941),f2(f2(x27942,a1),a1))),
% 63.13/63.22 inference(scs_inference,[],[2761,2730,1431,1493,2430,58,1010,18,14,19,15,11,13,12,16])).
% 63.13/63.22 cnf(2797,plain,
% 63.13/63.22 (P2(a1,f3(f7(x27971),f2(x27972,a1)))),
% 63.13/63.22 inference(scs_inference,[],[2761,2730,1431,1493,2430,58,1010,18,14,19,15,11,13,12,16,334])).
% 63.13/63.22 cnf(2803,plain,
% 63.13/63.22 (~P1(f3(f7(x28031),f3(f2(x28032,a1),a1)),f2(a1,f7(a1)))),
% 63.13/63.22 inference(scs_inference,[],[2763,1270,18,14,19])).
% 63.13/63.22 cnf(2807,plain,
% 63.13/63.22 (P1(f7(a5),f7(f3(a4,a1)))),
% 63.13/63.22 inference(scs_inference,[],[2763,2794,1270,18,14,19,15,11])).
% 63.13/63.22 cnf(2809,plain,
% 63.13/63.22 (~P1(a1,f3(f7(x28091),f2(x28092,a1)))),
% 63.13/63.22 inference(scs_inference,[],[2763,2794,2797,1270,18,14,19,15,11,13])).
% 63.13/63.22 cnf(2814,plain,
% 63.13/63.22 (P2(f2(f2(x28141,a1),a1),f7(x28142))),
% 63.13/63.22 inference(scs_inference,[],[2763,2787,2794,2797,2789,1270,804,18,14,19,15,11,13,16,12])).
% 63.13/63.22 cnf(2831,plain,
% 63.13/63.22 (~P1(f2(f2(x28311,a1),a1),f7(x28312))),
% 63.13/63.22 inference(scs_inference,[],[2814,2807,2809,2779,2353,18,14,19,15,11,13])).
% 63.13/63.22 cnf(2838,plain,
% 63.13/63.22 (P1(f2(f3(a1,a1),x28381),f2(f2(x28382,a1),x28381))),
% 63.13/63.22 inference(scs_inference,[],[1533,18])).
% 63.13/63.22 cnf(2846,plain,
% 63.13/63.22 (P1(f7(f2(a1,f7(a1))),f7(f3(a1,a1)))),
% 63.13/63.22 inference(scs_inference,[],[2831,2603,1460,2787,1533,18,14,19,15,11])).
% 63.13/63.22 cnf(2848,plain,
% 63.13/63.22 (~P1(f2(a1,f7(a1)),f3(f7(x28481),f2(x28482,a1)))),
% 63.13/63.22 inference(scs_inference,[],[2831,2791,2603,1460,2787,1533,18,14,19,15,11,13])).
% 63.13/63.22 cnf(2850,plain,
% 63.13/63.22 (~P1(f2(f3(f2(a1,a1),a1),a1),f7(x28501))),
% 63.13/63.22 inference(scs_inference,[],[2831,2791,2603,2618,1460,2787,1533,18,14,19,15,11,13,16])).
% 63.13/63.22 cnf(2853,plain,
% 63.13/63.22 (P2(f2(a1,f7(a1)),f3(f7(x28531),f3(f2(x28532,a1),a1)))),
% 63.13/63.22 inference(scs_inference,[],[2831,2791,2803,2603,2618,1460,2373,2787,1533,18,14,19,15,11,13,16,12])).
% 63.13/63.22 cnf(2863,plain,
% 63.13/63.22 (P1(f7(f2(x28631,a1)),f7(f3(a1,a1)))),
% 63.13/63.22 inference(scs_inference,[],[1445,18,14])).
% 63.13/63.22 cnf(2865,plain,
% 63.13/63.22 (~P1(f3(f7(x28651),f2(x28652,a1)),f2(x28653,a1))),
% 63.13/63.22 inference(scs_inference,[],[1454,1445,18,14,19])).
% 63.13/63.22 cnf(2867,plain,
% 63.13/63.22 (~P1(f7(f7(x28671)),f7(a1))),
% 63.13/63.22 inference(scs_inference,[],[1454,1445,10,18,14,19,15])).
% 63.13/63.22 cnf(2873,plain,
% 63.13/63.22 (P2(f2(f3(f2(x28731,a1),a1),a1),f3(f7(x28732),f2(a1,a1)))),
% 63.13/63.22 inference(scs_inference,[],[2853,2620,1454,1766,1445,10,18,14,19,15,11,13,12])).
% 63.13/63.22 cnf(2876,plain,
% 63.13/63.22 (~P1(f7(x28761),f2(a1,f7(a1)))),
% 63.13/63.22 inference(scs_inference,[],[2783,2853,2620,1454,1766,1445,2430,10,18,14,19,15,11,13,12,16])).
% 63.13/63.22 cnf(2881,plain,
% 63.13/63.22 (P1(f2(f2(x28811,a1),x28812),f2(f2(a1,f7(a1)),x28812))),
% 63.13/63.22 inference(scs_inference,[],[1428,18])).
% 63.13/63.22 cnf(2885,plain,
% 63.13/63.22 (~P1(f3(f7(x28851),f2(a1,f7(a1))),f2(f3(a1,a1),f7(a1)))),
% 63.13/63.22 inference(scs_inference,[],[1288,1428,18,14,19])).
% 63.13/63.22 cnf(2896,plain,
% 63.13/63.22 (P2(f2(x28961,a1),f3(f7(x28962),f2(f3(x28961,a1),a1)))),
% 63.13/63.22 inference(scs_inference,[],[2865,2838,2863,2873,1288,375,1428,2525,18,14,19,15,11,13,16,12])).
% 63.13/63.22 cnf(2902,plain,
% 63.13/63.22 (P1(f2(a5,x29021),f2(f3(a5,a1),x29021))),
% 63.13/63.22 inference(scs_inference,[],[1321,18])).
% 63.13/63.22 cnf(2904,plain,
% 63.13/63.22 (P1(f7(a5),f7(f3(a5,a1)))),
% 63.13/63.22 inference(scs_inference,[],[1321,18,14])).
% 63.13/63.22 cnf(2920,plain,
% 63.13/63.22 (P2(a1,f3(f7(x29201),f3(f7(x29202),a1)))),
% 63.13/63.22 inference(scs_inference,[],[2867,2848,2896,2885,2881,2707,2381,2291,1321,18,14,19,15,11,13,12,16,384])).
% 63.13/63.22 cnf(2922,plain,
% 63.13/63.22 (P1(f2(f2(a5,x29221),x29222),f2(f2(f3(a5,a1),x29221),x29222))),
% 63.13/63.22 inference(scs_inference,[],[2902,18])).
% 63.13/63.22 cnf(2930,plain,
% 63.13/63.22 (P1(f7(f3(a5,a1)),f7(a5))),
% 63.13/63.22 inference(scs_inference,[],[2876,2902,2904,1547,18,14,19,15,11])).
% 63.13/63.22 cnf(2937,plain,
% 63.13/63.22 (P2(f2(a1,f7(a1)),f7(x29371))),
% 63.13/63.22 inference(scs_inference,[],[2876,2902,2904,2920,2628,2333,1547,710,18,14,19,15,11,13,16,12])).
% 63.13/63.22 cnf(2944,plain,
% 63.13/63.22 (~P1(f3(f7(x29441),f2(x29442,a1)),f3(f2(a1,a1),a1))),
% 63.13/63.22 inference(scs_inference,[],[2930,1442,18,14,19])).
% 63.13/63.22 cnf(2950,plain,
% 63.13/63.22 (~P1(f2(a1,f7(a1)),f7(x29501))),
% 63.13/63.22 inference(scs_inference,[],[2937,2930,2922,1442,1013,18,14,19,15,11,13])).
% 63.13/63.22 cnf(2964,plain,
% 63.13/63.22 (~P1(f7(f2(a1,f7(a1))),f7(f7(x29641)))),
% 63.13/63.22 inference(scs_inference,[],[2950,2403,2904,18,14,19,15])).
% 63.13/63.22 cnf(2984,plain,
% 63.13/63.22 (P1(f2(a1,x29841),f2(f3(a1,a1),x29841))),
% 63.13/63.22 inference(scs_inference,[],[1248,18])).
% 63.13/63.22 cnf(2986,plain,
% 63.13/63.22 (P1(f7(a1),f7(f3(a1,a1)))),
% 63.13/63.22 inference(scs_inference,[],[1248,18,14])).
% 63.13/63.22 cnf(3001,plain,
% 63.13/63.22 (P1(f2(f2(a1,x30011),x30012),f2(f2(f3(a1,a1),x30011),x30012))),
% 63.13/63.22 inference(scs_inference,[],[2984,18])).
% 63.13/63.22 cnf(3007,plain,
% 63.13/63.22 (P1(f7(f3(a1,a1)),f7(a1))),
% 63.13/63.22 inference(scs_inference,[],[2984,2986,2358,18,19,14,11])).
% 63.13/63.22 cnf(3009,plain,
% 63.13/63.22 (~P1(f3(f2(a1,a1),a1),f7(x30091))),
% 63.13/63.22 inference(scs_inference,[],[2984,2986,2358,747,18,19,14,11,13])).
% 63.13/63.22 cnf(3023,plain,
% 63.13/63.22 (~P1(f3(f7(x30231),f2(x30232,a1)),f3(a1,a1))),
% 63.13/63.22 inference(scs_inference,[],[3007,1447,18,14,19])).
% 63.13/63.22 cnf(3029,plain,
% 63.13/63.22 (~P1(f2(a1,a1),f7(x30291))),
% 63.13/63.22 inference(scs_inference,[],[3007,3001,1447,730,18,14,19,15,11,13])).
% 63.13/63.22 cnf(3035,plain,
% 63.13/63.22 (~P1(f3(f2(f3(a1,a1),f7(a1)),f3(a1,a1)),f7(x30351))),
% 63.13/63.22 inference(scs_inference,[],[3009,3007,2850,3001,2337,1447,730,804,18,14,19,15,11,13,12,16])).
% 63.13/63.22 cnf(3048,plain,
% 63.13/63.22 (~P1(f2(a5,a6),f3(f7(x30481),f2(a4,a6)))),
% 63.13/63.22 inference(scs_inference,[],[3029,2432,2346,2986,29,18,19,14,15,11,13])).
% 63.13/63.22 cnf(3050,plain,
% 63.13/63.22 (P2(f3(a1,a1),f3(f7(x30501),f2(x30502,a1)))),
% 63.13/63.22 inference(scs_inference,[],[3029,3023,2432,2346,1674,2986,29,18,19,14,15,11,13,12])).
% 63.13/63.22 cnf(3055,plain,
% 63.13/63.22 (~P2(f3(f7(x30551),f2(a1,f7(a1))),f2(f2(x30552,a1),f7(a1)))),
% 63.13/63.22 inference(scs_inference,[],[3029,3023,2846,2964,2432,2346,1674,2986,2615,29,18,19,14,15,11,13,12,16,17])).
% 63.13/63.22 cnf(3062,plain,
% 63.13/63.22 (P1(f7(f7(a4)),f7(f7(f3(a5,a1))))),
% 63.13/63.22 inference(scs_inference,[],[2339,1280,1120,18,19,14])).
% 63.13/63.22 cnf(3068,plain,
% 63.13/63.22 (~P1(f3(a1,a1),f3(f7(x30681),f2(x30682,a1)))),
% 63.13/63.22 inference(scs_inference,[],[3048,3050,2744,2339,1280,1120,18,19,14,15,11,13])).
% 63.13/63.22 cnf(3077,plain,
% 63.13/63.22 (P1(f2(a1,x30771),f2(f3(f2(f3(a1,a1),f7(a1)),f3(a1,a1)),x30771))),
% 63.13/63.22 inference(scs_inference,[],[2236,18])).
% 63.13/63.22 cnf(3089,plain,
% 63.13/63.22 (P2(f2(f2(x30891,a1),f7(a1)),f3(f7(x30892),f2(a1,f7(a1))))),
% 63.13/63.22 inference(scs_inference,[],[3068,3055,3062,2313,2730,2236,1086,18,19,14,15,11,13,12])).
% 63.13/63.22 cnf(3095,plain,
% 63.13/63.22 (P1(f2(a1,x30951),f2(f3(f2(f3(a1,a1),a1),f3(a1,a1)),x30951))),
% 63.13/63.22 inference(scs_inference,[],[2272,18])).
% 63.13/63.22 cnf(3107,plain,
% 63.13/63.22 (P2(f2(f3(a1,a1),f7(a1)),f3(f7(x31071),f3(f7(x31072),f7(x31073))))),
% 63.13/63.22 inference(scs_inference,[],[3035,3089,3077,2321,2306,2272,18,19,14,15,11,13,12])).
% 63.13/63.22 cnf(3109,plain,
% 63.13/63.22 (~P1(f7(x31091),f3(f2(a1,a1),a1))),
% 63.13/63.22 inference(scs_inference,[],[3035,2944,3089,3077,2321,2306,2272,2430,18,19,14,15,11,13,12,16])).
% 63.13/63.22 cnf(3118,plain,
% 63.13/63.22 (P1(f7(f3(a1,a1)),f7(f3(f3(a1,a1),a1)))),
% 63.13/63.22 inference(scs_inference,[],[3109,2285,1452,1795,18,19,15,14])).
% 63.13/63.22 cnf(3136,plain,
% 63.13/63.22 (~P2(f3(f7(x31361),f2(x31362,a1)),f3(f2(f3(a1,a1),a1),f3(a1,a1)))),
% 63.13/63.22 inference(scs_inference,[],[3109,3107,3095,2508,2053,2285,2791,1452,1795,18,19,15,14,11,13,16,1424,1931,2221,2425,17])).
% 63.13/63.22 cnf(3152,plain,
% 63.13/63.22 ($false),
% 63.13/63.22 inference(scs_inference,[],[3136,3118,2637,1187,4,18,14,19,11,13]),
% 63.13/63.22 ['proof']).
% 63.13/63.22 % SZS output end Proof
% 63.13/63.22 % Total time :62.550000s
%------------------------------------------------------------------------------