%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD011-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n025.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:10 EDT 2024
% Result : Unsatisfiable 63.65s 63.68s
% Output : CNFRefutation 63.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : FLD011-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jun 19 10:35:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.54/0.58 start to proof:theBenchmark
% 63.57/63.67 %-------------------------------------------
% 63.57/63.67 % File :CSE---1.7
% 63.57/63.67 % Problem :theBenchmark
% 63.57/63.67 % Transform :cnf
% 63.57/63.67 % Format :tptp:raw
% 63.57/63.67 % Command :java -jar mcs_scs.jar %d %s
% 63.57/63.67
% 63.57/63.67 % Result :Theorem 63.050000s
% 63.57/63.67 % Output :CNFRefutation 63.050000s
% 63.57/63.67 %-------------------------------------------
% 63.65/63.68 %--------------------------------------------------------------------------
% 63.65/63.68 % File : FLD011-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 63.65/63.68 % Domain : Field Theory (Ordered fields)
% 63.65/63.68 % Problem : The multiplicative inverse fulfills the involution property
% 63.65/63.68 % Version : [Dra93] axioms : Especial.
% 63.65/63.68 % Theorem formulation : Functional with re axiom set.
% 63.65/63.68 % English :
% 63.65/63.68
% 63.65/63.68 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 63.65/63.68 % Source : [Dra93]
% 63.65/63.68 % Names :
% 63.65/63.68
% 63.65/63.68 % Status : Unsatisfiable
% 63.65/63.68 % Rating : 0.08 v8.2.0, 0.14 v7.5.0, 0.00 v7.4.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.25 v6.3.0, 0.00 v6.2.0, 0.11 v6.1.0, 0.14 v6.0.0, 0.43 v5.5.0, 0.38 v5.4.0, 0.60 v5.2.0, 0.30 v5.1.0, 0.36 v5.0.0, 0.50 v4.1.0, 0.38 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.50 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.50 v2.6.0, 0.67 v2.5.0, 0.40 v2.4.0, 0.80 v2.3.0, 0.67 v2.2.1, 0.67 v2.1.0
% 63.65/63.68 % Syntax : Number of clauses : 29 ( 6 unt; 3 nHn; 29 RR)
% 63.65/63.68 % Number of literals : 80 ( 0 equ; 51 neg)
% 63.65/63.68 % Maximal clause size : 5 ( 2 avg)
% 63.65/63.68 % Maximal term depth : 3 ( 1 avg)
% 63.65/63.68 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 63.65/63.68 % Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% 63.65/63.68 % Number of variables : 73 ( 0 sgn)
% 63.65/63.68 % SPC : CNF_UNS_RFO_NEQ_NHN
% 63.65/63.68
% 63.65/63.68 % Comments :
% 63.65/63.68 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 63.65/63.68 %--------------------------------------------------------------------------
% 63.65/63.68 include('Axioms/FLD002-0.ax').
% 63.65/63.68 %--------------------------------------------------------------------------
% 63.65/63.68 cnf(a_is_defined,hypothesis,
% 63.65/63.68 defined(a) ).
% 63.65/63.68
% 63.65/63.68 cnf(not_sum_2,negated_conjecture,
% 63.65/63.68 ~ sum(additive_identity,a,additive_identity) ).
% 63.65/63.68
% 63.65/63.68 cnf(not_product_3,negated_conjecture,
% 63.65/63.68 ~ product(multiplicative_identity,multiplicative_inverse(multiplicative_inverse(a)),a) ).
% 63.65/63.68
% 63.65/63.68 %--------------------------------------------------------------------------
% 63.65/63.68 %-------------------------------------------
% 63.65/63.68 % Proof found
% 63.65/63.68 % SZS status Theorem for theBenchmark
% 63.65/63.68 % SZS output start Proof
% 63.65/63.68 %ClaNum:29(EqnAxiom:0)
% 63.65/63.68 %VarNum:162(SingletonVarNum:73)
% 63.65/63.68 %MaxLitNum:5
% 63.65/63.68 %MaxfuncDepth:2
% 63.65/63.68 %SharedTerms:11
% 63.65/63.68 %goalClause: 5 6
% 63.65/63.68 %singleGoalClaCount:2
% 63.65/63.68 [1]P1(a1)
% 63.65/63.68 [2]P1(a4)
% 63.65/63.68 [3]P1(a2)
% 63.65/63.68 [4]~P2(a1,a1,a4)
% 63.65/63.68 [5]~P2(a1,a2,a1)
% 63.65/63.68 [6]~P3(a4,f6(f6(a2)),a2)
% 63.65/63.68 [12]~P1(x121)+P2(a1,x121,x121)
% 63.65/63.68 [13]~P1(x131)+P3(a4,x131,x131)
% 63.65/63.68 [7]~P1(x71)+P1(f5(x71))
% 63.65/63.68 [14]~P1(x141)+P2(f5(x141),x141,a1)
% 63.65/63.68 [21]~P2(x212,x211,x213)+P2(x211,x212,x213)
% 63.65/63.68 [22]~P3(x222,x221,x223)+P3(x221,x222,x223)
% 63.65/63.68 [15]~P1(x151)+P2(a1,x151,a1)+P1(f6(x151))
% 63.65/63.68 [19]~P1(x191)+P3(f6(x191),x191,a4)+P2(a1,x191,a1)
% 63.65/63.68 [18]~P4(x182,x181)+~P4(x181,x182)+P2(a1,x181,x182)
% 63.65/63.68 [9]~P1(x92)+~P1(x91)+P1(f3(x91,x92))
% 63.65/63.68 [10]~P1(x102)+~P1(x101)+P1(f7(x101,x102))
% 63.65/63.68 [16]~P1(x162)+~P1(x161)+P2(x161,x162,f3(x161,x162))
% 63.65/63.68 [17]~P1(x172)+~P1(x171)+P3(x171,x172,f7(x171,x172))
% 63.65/63.68 [11]~P4(x111,x113)+P4(x111,x112)+~P4(x113,x112)
% 63.65/63.68 [8]P4(x82,x81)+~P1(x81)+~P1(x82)+P4(x81,x82)
% 63.65/63.68 [20]~P3(x203,x202,x201)+P4(a1,x201)+~P4(a1,x202)+~P4(a1,x203)
% 63.65/63.68 [23]~P2(x233,x235,x231)+P4(x231,x232)+~P2(x234,x235,x232)+~P4(x233,x234)
% 63.65/63.69 [24]~P2(x241,x246,x244)+P2(x241,x242,x243)+~P2(x244,x245,x243)+~P2(x246,x245,x242)
% 63.65/63.69 [25]~P2(x256,x254,x251)+P2(x251,x252,x253)+~P2(x254,x252,x255)+~P2(x256,x255,x253)
% 63.65/63.69 [26]~P3(x261,x266,x264)+P3(x261,x262,x263)+~P3(x264,x265,x263)+~P3(x266,x265,x262)
% 63.65/63.69 [27]~P3(x276,x274,x271)+P3(x271,x272,x273)+~P3(x274,x272,x275)+~P3(x276,x275,x273)
% 63.65/63.69 [28]~P3(x285,x287,x282)+~P3(x284,x287,x281)+P2(x281,x282,x283)+~P2(x284,x285,x286)+~P3(x286,x287,x283)
% 63.65/63.69 [29]~P3(x297,x292,x295)+~P3(x296,x292,x294)+P3(x291,x292,x293)+~P2(x294,x295,x293)+~P2(x296,x297,x291)
% 63.65/63.69 %EqnAxiom
% 63.65/63.69
% 63.65/63.69 %-------------------------------------------
% 63.65/63.69 cnf(30,plain,
% 63.65/63.69 (~P2(a2,a1,a1)),
% 63.65/63.69 inference(scs_inference,[],[5,21])).
% 63.65/63.69 cnf(32,plain,
% 63.65/63.69 (~P3(f6(f6(a2)),a4,a2)),
% 63.65/63.69 inference(scs_inference,[],[5,6,21,22])).
% 63.65/63.69 cnf(34,plain,
% 63.65/63.69 (P4(a1,a1)),
% 63.65/63.69 inference(scs_inference,[],[5,6,1,21,22,8])).
% 63.65/63.69 cnf(39,plain,
% 63.65/63.69 (P4(a4,a4)),
% 63.65/63.69 inference(scs_inference,[],[2,8])).
% 63.65/63.69 cnf(45,plain,
% 63.65/63.69 (~P4(a4,a1)+~P2(a1,x451,a1)+~P2(a1,x451,a4)),
% 63.65/63.69 inference(scs_inference,[],[5,2,4,34,8,18,20,23])).
% 63.65/63.69 cnf(46,plain,
% 63.65/63.69 (P4(a2,a2)),
% 63.65/63.69 inference(scs_inference,[],[3,8])).
% 63.65/63.69 cnf(48,plain,
% 63.65/63.69 (~P2(a4,x481,x482)+~P2(a4,x481,x483)+P4(x482,x483)),
% 63.65/63.69 inference(scs_inference,[],[3,39,8,23])).
% 63.65/63.69 cnf(54,plain,
% 63.65/63.69 (~P2(a1,x541,x542)+~P2(a1,x541,x543)+P4(x542,x543)),
% 63.65/63.69 inference(scs_inference,[],[34,23])).
% 63.65/63.69 cnf(62,plain,
% 63.65/63.69 (P1(f5(f3(a1,a1)))),
% 63.65/63.69 inference(scs_inference,[],[1,7,9])).
% 63.65/63.69 cnf(63,plain,
% 63.65/63.69 (P4(f5(f3(a1,a1)),f5(f3(a1,a1)))),
% 63.65/63.69 inference(scs_inference,[],[62,8])).
% 63.65/63.69 cnf(66,plain,
% 63.65/63.69 (~P2(f5(f3(a1,a1)),x661,x662)+~P2(f5(f3(a1,a1)),x661,x663)+P4(x662,x663)),
% 63.65/63.69 inference(scs_inference,[],[63,23])).
% 63.65/63.69 cnf(80,plain,
% 63.65/63.69 (P2(a1,f5(a4),f5(a4))),
% 63.65/63.70 inference(scs_inference,[],[2,12,7])).
% 63.65/63.70 cnf(102,plain,
% 63.65/63.70 (P3(a4,f5(a2),f5(a2))),
% 63.65/63.70 inference(scs_inference,[],[3,13,7])).
% 63.65/63.70 cnf(156,plain,
% 63.65/63.70 (P2(f5(f5(a1)),f5(a1),a1)),
% 63.65/63.70 inference(scs_inference,[],[1,14,7])).
% 63.65/63.70 cnf(159,plain,
% 63.65/63.70 (~P2(a2,f5(f5(a1)),f5(f5(a1)))),
% 63.65/63.70 inference(scs_inference,[],[5,30,156,25,24])).
% 63.69/63.70 cnf(164,plain,
% 63.69/63.70 (~P2(f5(f5(a1)),a2,f5(f5(a1)))),
% 63.69/63.70 inference(scs_inference,[],[159,21])).
% 63.69/63.70 cnf(305,plain,
% 63.69/63.70 (P1(f7(f5(a1),f5(a1)))),
% 63.69/63.70 inference(scs_inference,[],[1,10,7])).
% 63.69/63.70 cnf(306,plain,
% 63.69/63.70 (P4(f7(f5(a1),f5(a1)),f7(f5(a1),f5(a1)))),
% 63.69/63.70 inference(scs_inference,[],[305,8])).
% 63.69/63.70 cnf(402,plain,
% 63.69/63.70 (P2(f5(a1),f5(a1),f3(f5(a1),f5(a1)))),
% 63.69/63.70 inference(scs_inference,[],[1,16,7])).
% 63.69/63.70 cnf(795,plain,
% 63.69/63.70 (~P3(f5(a1),x7951,f5(a1))+~P3(f5(f5(a1)),x7951,f5(f5(a1)))+P3(a1,x7951,a1)),
% 63.69/63.70 inference(scs_inference,[],[156,63,29])).
% 63.69/63.70 cnf(993,plain,
% 63.69/63.70 (~P4(a4,a1)+~P2(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[2,45,12])).
% 63.69/63.70 cnf(1009,plain,
% 63.69/63.70 (~P2(a4,x10091,a4)+~P2(a4,x10091,a1)+~P2(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[993,48])).
% 63.69/63.70 cnf(1088,plain,
% 63.69/63.70 (~P2(x10881,a4,a1)+~P2(a4,x10881,a4)+~P2(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[1009,21])).
% 63.69/63.70 cnf(1119,plain,
% 63.69/63.70 (~P2(x11191,a4,a4)+~P2(x11191,a4,a1)+~P2(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[1088,21])).
% 63.69/63.70 cnf(1135,plain,
% 63.69/63.70 (~P2(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[39,1119,18])).
% 63.69/63.70 cnf(1136,plain,
% 63.69/63.70 (~P2(a4,a1,a1)),
% 63.69/63.70 inference(scs_inference,[],[1135,21])).
% 63.69/63.70 cnf(1457,plain,
% 63.69/63.70 (~P4(a2,a1)+~P2(f5(f3(a1,a1)),x14571,a1)+~P2(f5(f3(a1,a1)),x14571,a2)),
% 63.69/63.70 inference(scs_inference,[],[5,66,18])).
% 63.69/63.70 cnf(1776,plain,
% 63.69/63.70 (~P3(x17761,f5(f5(a1)),f5(f5(a1)))+~P3(f5(a1),x17761,f5(a1))+P3(a1,x17761,a1)),
% 63.69/63.70 inference(scs_inference,[],[795,22])).
% 63.69/63.70 cnf(1808,plain,
% 63.69/63.70 (~P1(f5(f5(a1)))+~P3(f5(a1),a4,f5(a1))+P3(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[1776,13])).
% 63.69/63.70 cnf(1824,plain,
% 63.69/63.70 (~P1(f5(a1))+~P3(f5(a1),a4,f5(a1))+P3(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[1808,7])).
% 63.69/63.70 cnf(1840,plain,
% 63.69/63.70 (~P3(a4,f5(a1),f5(a1))+~P1(f5(a1))+P3(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[1824,22])).
% 63.69/63.70 cnf(1856,plain,
% 63.69/63.70 (~P3(a4,f5(a1),f5(a1))+P3(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[1,1840,7])).
% 63.69/63.70 cnf(1872,plain,
% 63.69/63.70 (~P1(f5(a1))+P3(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[1856,13])).
% 63.69/63.70 cnf(1888,plain,
% 63.69/63.70 (P3(a1,a4,a1)),
% 63.69/63.70 inference(scs_inference,[],[1,1872,7])).
% 63.69/63.70 cnf(1892,plain,
% 63.69/63.70 (P3(a1,x18921,a1)+~P3(a4,x18921,a4)),
% 63.69/63.70 inference(scs_inference,[],[1888,27])).
% 63.69/63.70 cnf(1922,plain,
% 63.69/63.70 (~P3(x19221,a4,a4)+P3(a1,x19221,a1)),
% 63.69/63.70 inference(scs_inference,[],[1892,22])).
% 63.69/63.70 cnf(1953,plain,
% 63.69/63.70 (P3(x19531,a1,a1)+~P3(x19531,a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[1922,22])).
% 63.69/63.70 cnf(1969,plain,
% 63.69/63.70 (P3(a4,a1,a1)),
% 63.69/63.70 inference(scs_inference,[],[2,1953,13])).
% 63.69/63.70 cnf(2895,plain,
% 63.69/63.70 (P3(a4,f5(a4),f5(a4))),
% 63.69/63.70 inference(scs_inference,[],[2,7,13])).
% 63.69/63.70 cnf(2962,plain,
% 63.69/63.70 (P1(f5(f3(a4,a4)))),
% 63.69/63.70 inference(scs_inference,[],[2,7,9])).
% 63.69/63.70 cnf(2965,plain,
% 63.69/63.70 (P4(f5(f3(a4,a4)),f5(f3(a4,a4)))),
% 63.69/63.70 inference(scs_inference,[],[1135,156,2962,25,8])).
% 63.69/63.70 cnf(3586,plain,
% 63.69/63.70 (~P3(x35861,x35862,a2)+~P3(x35861,x35863,a4)+~P3(x35863,f6(f6(a2)),x35862)),
% 63.69/63.70 inference(scs_inference,[],[6,164,306,27])).
% 63.69/63.70 cnf(3631,plain,
% 63.69/63.70 (P2(f5(a4),a1,f5(a4))),
% 63.69/63.70 inference(scs_inference,[],[80,21])).
% 63.69/63.70 cnf(3633,plain,
% 63.69/63.70 (~P2(x36331,f5(a4),a1)+~P2(x36331,f5(a4),a2)),
% 63.69/63.70 inference(scs_inference,[],[30,80,21,25])).
% 63.69/63.70 cnf(3639,plain,
% 63.69/63.70 (~P2(x36391,f5(a4),a1)+~P2(x36391,f5(a4),a4)),
% 63.69/63.70 inference(scs_inference,[],[1136,3631,156,21,25])).
% 63.69/63.70 cnf(3660,plain,
% 63.69/63.70 (P3(f5(a4),a4,f5(a4))),
% 63.69/63.70 inference(scs_inference,[],[2895,22])).
% 63.69/63.70 cnf(3671,plain,
% 63.69/63.70 (P3(f5(a2),a4,f5(a2))),
% 63.69/63.70 inference(scs_inference,[],[102,22])).
% 63.69/63.70 cnf(3693,plain,
% 63.69/63.70 (~P3(x36931,a1,a2)+~P2(a4,x36931,a4)),
% 63.69/63.70 inference(scs_inference,[],[5,1969,28])).
% 63.69/63.70 cnf(3696,plain,
% 63.69/63.70 (~P3(x36961,a4,a2)+~P2(a1,x36961,a1)),
% 63.69/63.70 inference(scs_inference,[],[5,1888,28])).
% 63.69/63.70 cnf(3700,plain,
% 63.69/63.70 (~P2(f5(f3(a4,a4)),x37001,x37002)+~P2(f5(f3(a4,a4)),x37001,x37003)+P4(x37002,x37003)),
% 63.69/63.70 inference(scs_inference,[],[6,164,2965,23])).
% 63.69/63.70 cnf(3712,plain,
% 63.69/63.70 (~P2(x37121,a4,a4)+~P3(x37121,a1,a2)),
% 63.69/63.70 inference(scs_inference,[],[3693,21])).
% 63.69/63.70 cnf(3728,plain,
% 63.69/63.70 (~P3(a1,a4,a2)),
% 63.69/63.70 inference(scs_inference,[],[1,3696,12])).
% 63.69/63.70 cnf(3729,plain,
% 63.69/63.70 (~P3(a4,a1,a2)),
% 63.69/63.70 inference(scs_inference,[],[1969,1888,3728,27])).
% 63.69/63.70 cnf(3734,plain,
% 63.69/63.70 (~P3(x37341,a1,a2)+~P3(x37341,a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[1969,3729,27])).
% 63.69/63.70 cnf(3750,plain,
% 63.69/63.70 (~P3(a1,x37501,a2)+~P2(x37501,a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[3712,22])).
% 63.69/63.70 cnf(3751,plain,
% 63.69/63.70 (~P3(a1,x37511,a2)+~P3(a4,a4,x37511)),
% 63.69/63.70 inference(scs_inference,[],[1888,3728,27])).
% 63.69/63.70 cnf(3788,plain,
% 63.69/63.70 (~P3(f6(a4),a1,a2)),
% 63.69/63.70 inference(scs_inference,[],[1135,2,3734,19])).
% 63.69/63.70 cnf(3806,plain,
% 63.69/63.70 (~P3(a1,a1,a2)),
% 63.69/63.70 inference(scs_inference,[],[2,3750,12])).
% 63.69/63.70 cnf(3822,plain,
% 63.69/63.70 (~P3(a1,f7(a4,a4),a2)),
% 63.69/63.70 inference(scs_inference,[],[2,3751,17])).
% 63.69/63.70 cnf(3898,plain,
% 63.69/63.70 (~P3(a4,x38981,a2)+~P3(a1,f7(a4,a4),x38981)),
% 63.69/63.70 inference(scs_inference,[],[1969,3822,27])).
% 63.69/63.70 cnf(3901,plain,
% 63.69/63.70 (~P3(a4,x39011,a2)+~P3(a1,a1,x39011)),
% 63.69/63.70 inference(scs_inference,[],[1969,3806,27])).
% 63.69/63.70 cnf(3904,plain,
% 63.69/63.70 (~P3(x39041,a4,a2)+~P2(x39041,a1,a1)),
% 63.69/63.70 inference(scs_inference,[],[30,1888,28])).
% 63.69/63.70 cnf(3908,plain,
% 63.69/63.70 (~P3(a4,f7(a1,a1),a2)),
% 63.69/63.70 inference(scs_inference,[],[1,3901,17])).
% 63.69/63.70 cnf(3924,plain,
% 63.69/63.70 (~P3(f5(a1),a4,a2)),
% 63.69/63.70 inference(scs_inference,[],[1,3904,14])).
% 63.69/63.70 cnf(4056,plain,
% 63.69/63.70 (~P3(f7(a4,a4),a1,x40561)+~P3(a4,x40561,a2)),
% 63.69/63.70 inference(scs_inference,[],[3898,22])).
% 63.69/63.70 cnf(4120,plain,
% 63.69/63.70 (~P1(f7(a4,a4))+~P3(a4,f7(f7(a4,a4),a1),a2)),
% 63.69/63.70 inference(scs_inference,[],[1,4056,17])).
% 63.69/63.70 cnf(4279,plain,
% 63.69/63.70 (~P3(x42791,a1,a4)+~P2(x42791,a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[1136,1969,28])).
% 63.69/63.70 cnf(4284,plain,
% 63.69/63.70 (~P3(x42841,a4,a4)+~P2(x42841,a1,a1)),
% 63.69/63.70 inference(scs_inference,[],[1136,1888,28])).
% 63.69/63.70 cnf(4289,plain,
% 63.69/63.70 (~P3(a1,a1,a4)),
% 63.69/63.70 inference(scs_inference,[],[2,4279,12])).
% 63.69/63.70 cnf(4290,plain,
% 63.69/63.70 (~P3(a4,x42901,a4)+~P3(a1,a1,x42901)),
% 63.69/63.70 inference(scs_inference,[],[1969,4289,27])).
% 63.69/63.70 cnf(4292,plain,
% 63.69/63.70 (~P3(a4,a1,a4)+~P3(a1,a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[1969,4289,27,1922])).
% 63.69/63.70 cnf(4309,plain,
% 63.69/63.70 (~P3(f5(a1),a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[1,4284,14])).
% 63.69/63.70 cnf(4342,plain,
% 63.69/63.70 (~P3(a4,f7(a1,a1),a4)),
% 63.69/63.70 inference(scs_inference,[],[1,4290,17])).
% 63.69/63.70 cnf(4374,plain,
% 63.69/63.70 (~P3(a1,a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[4292,22])).
% 63.69/63.70 cnf(4375,plain,
% 63.69/63.70 (~P3(a4,a1,a4)),
% 63.69/63.70 inference(scs_inference,[],[1969,1888,4374,27])).
% 63.69/63.70 cnf(4395,plain,
% 63.69/63.70 (~P3(x43951,a1,a4)+~P3(x43951,a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[1969,4375,27])).
% 63.69/63.70 cnf(4410,plain,
% 63.69/63.70 (~P3(f6(a4),a1,a4)),
% 63.69/63.70 inference(scs_inference,[],[1135,2,4395,19])).
% 63.69/63.70 cnf(4699,plain,
% 63.69/63.70 (~P3(a1,x46991,a4)+~P3(a4,a4,x46991)),
% 63.69/63.70 inference(scs_inference,[],[1888,4374,27])).
% 63.69/63.70 cnf(4711,plain,
% 63.69/63.70 (~P3(a1,f7(a4,a4),a4)),
% 63.69/63.70 inference(scs_inference,[],[2,4699,17])).
% 63.69/63.70 cnf(4794,plain,
% 63.69/63.70 (~P3(a4,x47941,a4)+~P3(a1,f7(a4,a4),x47941)),
% 63.69/63.70 inference(scs_inference,[],[1969,4711,27])).
% 63.69/63.70 cnf(4811,plain,
% 63.69/63.70 (~P3(f7(a4,a4),a1,x48111)+~P3(a4,x48111,a4)),
% 63.69/63.70 inference(scs_inference,[],[4794,22])).
% 63.69/63.70 cnf(4827,plain,
% 63.69/63.70 (~P1(f7(a4,a4))+~P3(a4,f7(f7(a4,a4),a1),a4)),
% 63.69/63.70 inference(scs_inference,[],[1,4811,17])).
% 63.69/63.70 cnf(5356,plain,
% 63.69/63.70 (~P3(a4,f7(f7(a4,a4),a1),a2)),
% 63.69/63.70 inference(scs_inference,[],[2,4120,10])).
% 63.69/63.70 cnf(5390,plain,
% 63.69/63.70 (~P3(a4,f7(f7(a4,a4),a1),a4)),
% 63.69/63.70 inference(scs_inference,[],[2,4827,10])).
% 63.69/63.70 cnf(5522,plain,
% 63.69/63.70 (~P3(f6(a4),a1,x55221)+~P3(x55221,a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[4410,1888,26])).
% 63.69/63.70 cnf(5524,plain,
% 63.69/63.70 (~P1(f6(a4))+~P3(f7(f6(a4),a1),a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[4410,1888,1,26,17])).
% 63.69/63.70 cnf(5527,plain,
% 63.69/63.70 (~P3(f6(a4),a1,x55271)+~P3(x55271,a4,a2)),
% 63.69/63.70 inference(scs_inference,[],[3788,1888,26])).
% 63.69/63.70 cnf(5529,plain,
% 63.69/63.70 (~P1(f6(a4))+~P3(f7(f6(a4),a1),a4,a2)),
% 63.69/63.70 inference(scs_inference,[],[3788,1888,1,26,17])).
% 63.69/63.70 cnf(5532,plain,
% 63.69/63.70 (~P3(a4,x55321,a4)+~P3(a1,x55321,a4)),
% 63.69/63.70 inference(scs_inference,[],[1888,4374,26])).
% 63.69/63.70 cnf(5535,plain,
% 63.69/63.70 (~P3(a1,a1,x55351)+~P3(x55351,a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[1888,4289,26])).
% 63.69/63.70 cnf(5544,plain,
% 63.69/63.70 (~P3(a1,a1,x55441)+~P3(x55441,a4,a2)),
% 63.69/63.70 inference(scs_inference,[],[1888,3806,26])).
% 63.69/63.70 cnf(5577,plain,
% 63.69/63.70 (~P3(a1,a1,f6(a4))),
% 63.69/63.70 inference(scs_inference,[],[1135,2,5535,19])).
% 63.69/63.70 cnf(5578,plain,
% 63.69/63.70 (~P3(a1,a1,x55781)+~P3(x55781,a4,f6(a4))),
% 63.69/63.70 inference(scs_inference,[],[1888,5577,26])).
% 63.69/63.70 cnf(5595,plain,
% 63.69/63.70 (~P3(f7(a1,a1),a4,a2)),
% 63.69/63.70 inference(scs_inference,[],[1,5544,17])).
% 63.69/63.70 cnf(5598,plain,
% 63.69/63.70 (~P3(x55981,x55982,a4)+~P3(f5(a1),x55981,x55983)+~P3(x55983,x55982,a2)),
% 63.69/63.70 inference(scs_inference,[],[164,1888,3924,5595,26])).
% 63.69/63.70 cnf(5629,plain,
% 63.69/63.70 (~P3(a1,f6(a4),x56291)+~P3(x56291,a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[5522,22])).
% 63.69/63.70 cnf(5645,plain,
% 63.69/63.70 (~P3(a1,f6(a4),x56451)+~P3(x56451,a4,a2)),
% 63.69/63.70 inference(scs_inference,[],[5527,22])).
% 63.69/63.70 cnf(5661,plain,
% 63.69/63.70 (~P3(a4,x56611,f6(a4))+~P3(a1,a1,x56611)),
% 63.69/63.70 inference(scs_inference,[],[5578,22])).
% 63.69/63.70 cnf(5693,plain,
% 63.69/63.70 (~P1(f6(a4))+~P3(f7(a1,f6(a4)),a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[1,5629,17])).
% 63.69/63.70 cnf(5709,plain,
% 63.69/63.70 (~P1(f6(a4))+~P3(f7(a1,f6(a4)),a4,a2)),
% 63.69/63.70 inference(scs_inference,[],[1,5645,17])).
% 63.69/63.70 cnf(5774,plain,
% 63.69/63.70 (~P3(a4,f7(a1,a1),f6(a4))),
% 63.69/63.70 inference(scs_inference,[],[1,5661,17])).
% 63.69/63.70 cnf(5908,plain,
% 63.69/63.70 (~P3(a4,f7(f6(a4),a1),a4)+~P1(f6(a4))),
% 63.69/63.70 inference(scs_inference,[],[5524,22])).
% 63.69/63.70 cnf(5924,plain,
% 63.69/63.70 (~P3(a4,f7(f6(a4),a1),a2)+~P1(f6(a4))),
% 63.69/63.70 inference(scs_inference,[],[5529,22])).
% 63.69/63.70 cnf(5956,plain,
% 63.69/63.70 (~P3(f7(a1,f6(a4)),a4,a4)),
% 63.69/63.70 inference(scs_inference,[],[1135,2,5693,15])).
% 63.69/63.70 cnf(5978,plain,
% 63.69/63.70 (~P3(f7(a1,f6(a4)),a4,a2)),
% 63.69/63.70 inference(scs_inference,[],[1135,2,5709,15])).
% 63.69/63.70 cnf(5998,plain,
% 63.69/63.70 (~P3(x59981,x59982,a2)+~P3(x59981,x59983,a4)+~P3(x59983,f7(a1,a1),x59982)),
% 63.69/63.70 inference(scs_inference,[],[3908,164,306,27])).
% 63.69/63.70 cnf(6003,plain,
% 63.69/63.70 (~P3(x60031,x60032,a4)+~P3(f5(a1),x60031,x60033)+~P3(x60033,x60032,a4)),
% 63.69/63.70 inference(scs_inference,[],[164,4309,63,26])).
% 63.69/63.70 cnf(6146,plain,
% 63.69/63.70 (~P3(a4,f7(f6(a4),a1),a4)),
% 63.69/63.70 inference(scs_inference,[],[1135,2,5908,15])).
% 63.69/63.70 cnf(6164,plain,
% 63.69/63.70 (~P3(a4,f7(f6(a4),a1),a2)),
% 63.69/63.70 inference(scs_inference,[],[1135,2,5924,15])).
% 63.69/63.70 cnf(6279,plain,
% 63.69/63.70 (~P3(x62791,x62792,a4)+~P3(f6(f6(a2)),x62791,x62793)+~P3(x62793,x62792,a2)),
% 63.69/63.70 inference(scs_inference,[],[164,6,32,26])).
% 63.69/63.70 cnf(6516,plain,
% 63.69/63.70 (~P3(x65161,x65162,a4)+~P3(x65161,x65163,a4)+~P3(x65163,f7(a1,a1),x65162)),
% 63.69/63.70 inference(scs_inference,[],[4342,164,306,27])).
% 63.69/63.70 cnf(6629,plain,
% 63.69/63.70 (~P3(x66291,x66292,a4)+~P3(f7(a1,a1),x66291,x66293)+~P3(x66293,x66292,a2)),
% 63.69/63.71 inference(scs_inference,[],[6,164,5595,26])).
% 63.69/63.71 cnf(7130,plain,
% 63.69/63.71 (~P3(x71301,x71302,a4)+~P3(f7(a1,f6(a4)),x71301,x71303)+~P3(x71303,x71302,a2)),
% 63.69/63.71 inference(scs_inference,[],[6,164,5978,26])).
% 63.69/63.71 cnf(7252,plain,
% 63.69/63.71 (~P3(x72521,x72522,a2)+~P3(x72521,x72523,a4)+~P3(x72523,f7(f7(a4,a4),a1),x72522)),
% 63.69/63.71 inference(scs_inference,[],[5356,5595,2965,27])).
% 63.69/63.71 cnf(7496,plain,
% 63.69/63.71 (~P3(x74961,x74962,a4)+~P3(x74961,x74963,a4)+~P3(x74963,f7(f7(a4,a4),a1),x74962)),
% 63.69/63.71 inference(scs_inference,[],[5390,164,32,27])).
% 63.69/63.71 cnf(7512,plain,
% 63.69/63.71 (~P3(f7(f7(a4,a4),a1),a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[5390,22])).
% 63.69/63.71 cnf(7515,plain,
% 63.69/63.71 (~P3(f7(a1,a1),a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[4342,22])).
% 63.69/63.71 cnf(7520,plain,
% 63.69/63.71 (~P3(a4,f7(a1,f6(a4)),a4)),
% 63.69/63.71 inference(scs_inference,[],[5956,22])).
% 63.69/63.71 cnf(7538,plain,
% 63.69/63.71 (~P3(f7(f7(a4,a4),a1),a4,a2)),
% 63.69/63.71 inference(scs_inference,[],[5356,22])).
% 63.69/63.71 cnf(7555,plain,
% 63.69/63.71 (~P3(f7(f6(a4),a1),a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[6146,22])).
% 63.69/63.71 cnf(7560,plain,
% 63.69/63.71 (~P3(f7(f6(a4),a1),a4,a2)),
% 63.69/63.71 inference(scs_inference,[],[6164,22])).
% 63.69/63.71 cnf(7577,plain,
% 63.69/63.71 (~P3(f7(a1,a1),a4,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[5774,22])).
% 63.69/63.71 cnf(7582,plain,
% 63.69/63.71 (~P3(f7(a4,a4),a1,a4)),
% 63.69/63.71 inference(scs_inference,[],[4711,22])).
% 63.69/63.71 cnf(7584,plain,
% 63.69/63.71 (~P3(f7(a4,a4),a4,x75841)+~P3(x75841,a1,a4)),
% 63.69/63.71 inference(scs_inference,[],[1969,4711,22,26])).
% 63.69/63.71 cnf(7632,plain,
% 63.69/63.71 (~P3(a4,f7(a4,a4),x76321)+~P3(x76321,a1,a4)),
% 63.69/63.71 inference(scs_inference,[],[7584,22])).
% 63.69/63.71 cnf(7692,plain,
% 63.69/63.71 (~P1(f7(a4,a4))+~P3(f7(a4,f7(a4,a4)),a1,a4)),
% 63.69/63.71 inference(scs_inference,[],[2,7632,17])).
% 63.69/63.71 cnf(7886,plain,
% 63.69/63.71 (~P3(f7(a4,a4),a1,x78861)+~P3(x78861,a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[7582,1888,26])).
% 63.69/63.71 cnf(7888,plain,
% 63.69/63.71 (~P3(a1,f7(a4,a4),x78881)+~P3(x78881,a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[7582,1888,26,22])).
% 63.69/63.71 cnf(7913,plain,
% 63.69/63.71 (~P3(f7(a4,a4),a1,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[1135,2,7886,19])).
% 63.69/63.71 cnf(7914,plain,
% 63.69/63.71 (~P3(a1,f7(a4,a4),f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[7913,22])).
% 63.69/63.71 cnf(7940,plain,
% 63.69/63.71 (~P3(a4,x79401,f7(a4,a4))+~P3(a1,x79401,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[1888,7914,26])).
% 63.69/63.71 cnf(7947,plain,
% 63.69/63.71 (~P3(f7(a4,a4),a1,x79471)+~P3(x79471,a4,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[164,1888,7560,7913,306,27,25,23,26])).
% 63.69/63.71 cnf(7949,plain,
% 63.69/63.71 (~P3(a1,x79491,f6(a4))+~P3(a4,f7(a4,a4),x79491)),
% 63.69/63.71 inference(scs_inference,[],[1888,7914,27])).
% 63.69/63.71 cnf(7951,plain,
% 63.69/63.71 (~P3(x79511,a1,f6(a4))+~P3(a4,f7(a4,a4),x79511)),
% 63.69/63.71 inference(scs_inference,[],[1888,7914,27,22])).
% 63.69/63.71 cnf(7965,plain,
% 63.69/63.71 (~P1(f7(a4,a4))+~P3(f7(a1,f7(a4,a4)),a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[1,7888,17])).
% 63.69/63.71 cnf(8166,plain,
% 63.69/63.71 (~P3(a1,a4,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[2,7940,17])).
% 63.69/63.71 cnf(8167,plain,
% 63.69/63.71 (~P3(a4,a1,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[8166,22])).
% 63.69/63.71 cnf(8172,plain,
% 63.69/63.71 (~P3(x81721,a1,f6(a4))+~P3(x81721,a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[1969,8167,27])).
% 63.69/63.71 cnf(8185,plain,
% 63.69/63.71 (~P3(f7(a4,a4),a4,x81851)+~P3(x81851,a1,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[7913,1969,26])).
% 63.69/63.71 cnf(8187,plain,
% 63.69/63.71 (~P3(a1,x81871,f6(a4))+~P3(f7(a4,a4),a4,x81871)),
% 63.69/63.71 inference(scs_inference,[],[7913,1969,26,22])).
% 63.69/63.71 cnf(8190,plain,
% 63.69/63.71 (~P3(a4,x81901,f6(a4))+~P3(a1,f7(a4,a4),x81901)),
% 63.69/63.71 inference(scs_inference,[],[7914,1969,27])).
% 63.69/63.71 cnf(8192,plain,
% 63.69/63.71 (~P3(x81921,a4,f6(a4))+~P3(a1,f7(a4,a4),x81921)),
% 63.69/63.71 inference(scs_inference,[],[7914,1969,27,22])).
% 63.69/63.71 cnf(8195,plain,
% 63.69/63.71 (~P3(x81951,x81952,a4)+~P3(f7(a1,a1),x81951,x81953)+~P3(x81953,x81952,a4)),
% 63.69/63.71 inference(scs_inference,[],[164,7515,2965,26])).
% 63.69/63.71 cnf(8196,plain,
% 63.69/63.71 (~P3(x81961,x81962,f6(a4))+~P3(x81961,x81963,a4)+~P3(x81963,f7(a1,a1),x81962)),
% 63.69/63.71 inference(scs_inference,[],[5774,164,39,27])).
% 63.69/63.71 cnf(8199,plain,
% 63.69/63.71 (~P3(x81991,x81992,a4)+~P3(f7(f7(a4,a4),a1),x81991,x81993)+~P3(x81993,x81992,a2)),
% 63.69/63.71 inference(scs_inference,[],[5774,164,7538,26])).
% 63.69/63.71 cnf(8218,plain,
% 63.69/63.71 (~P3(f6(a4),a1,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[1135,2,8172,19])).
% 63.69/63.71 cnf(8219,plain,
% 63.69/63.71 (~P3(a1,f6(a4),f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[8218,22])).
% 63.69/63.71 cnf(8239,plain,
% 63.69/63.71 (~P3(x82391,x82392,a4)+~P3(f7(f6(a4),a1),x82391,x82393)+~P3(x82393,x82392,a4)),
% 63.69/63.71 inference(scs_inference,[],[164,7555,63,26])).
% 63.69/63.71 cnf(8425,plain,
% 63.69/63.71 (~P3(x84251,x84252,a4)+~P3(f7(a1,f6(a4)),x84251,x84253)+~P3(x84253,x84252,a4)),
% 63.69/63.71 inference(scs_inference,[],[5956,6,164,26])).
% 63.69/63.71 cnf(8526,plain,
% 63.69/63.71 (~P1(f7(a4,a4))+~P3(f7(f7(a4,a4),a1),a4,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[1,7947,17])).
% 63.69/63.71 cnf(8542,plain,
% 63.69/63.71 (~P1(f7(a4,a4))+~P3(a1,f7(a4,f7(a4,a4)),f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[2,7949,17])).
% 63.69/63.71 cnf(8558,plain,
% 63.69/63.71 (~P1(f7(a4,a4))+~P3(f7(a4,f7(a4,a4)),a1,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[2,7951,17])).
% 63.69/63.71 cnf(8689,plain,
% 63.69/63.71 (~P1(f7(a4,a4))+~P3(f7(f7(a4,a4),a4),a1,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[2,8185,17])).
% 63.69/63.71 cnf(8705,plain,
% 63.69/63.71 (~P1(f7(a4,a4))+~P3(a1,f7(f7(a4,a4),a4),f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[2,8187,17])).
% 63.69/63.71 cnf(8710,plain,
% 63.69/63.71 (~P3(x87101,x87102,a4)+~P3(f7(f6(a4),a1),x87101,x87103)+~P3(x87103,x87102,a2)),
% 63.69/63.71 inference(scs_inference,[],[6,164,7560,26])).
% 63.69/63.71 cnf(8714,plain,
% 63.69/63.71 (~P3(x87141,x87142,a4)+~P3(f7(a1,a1),x87141,x87143)+~P3(x87143,x87142,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[6,164,7577,26])).
% 63.69/63.71 cnf(8721,plain,
% 63.69/63.71 (~P3(f7(a4,a4),a1,x87211)+~P3(a4,x87211,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[8190,22])).
% 63.69/63.71 cnf(8737,plain,
% 63.69/63.71 (~P1(f7(a4,a4))+~P3(f7(a1,f7(a4,a4)),a4,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[1,8192,17])).
% 63.69/63.71 cnf(8766,plain,
% 63.69/63.71 (~P3(x87661,x87662,a4)+~P3(f7(f7(a4,a4),a1),x87661,x87663)+~P3(x87663,x87662,a4)),
% 63.69/63.71 inference(scs_inference,[],[6,164,7512,26])).
% 63.69/63.71 cnf(8797,plain,
% 63.69/63.71 (~P1(f7(a4,a4))+~P3(a4,f7(f7(a4,a4),a1),f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[1,8721,17])).
% 63.69/63.71 cnf(8861,plain,
% 63.69/63.71 (~P3(x88611,x88612,a4)+~P3(x88611,x88613,a4)+~P3(x88613,f7(f6(a4),a1),x88612)),
% 63.69/63.71 inference(scs_inference,[],[6146,7560,63,27])).
% 63.69/63.71 cnf(8940,plain,
% 63.69/63.71 (P1(f5(a2))),
% 63.69/63.71 inference(scs_inference,[],[3,7])).
% 63.69/63.71 cnf(8942,plain,
% 63.69/63.71 (P2(f5(a2),a2,a1)),
% 63.69/63.71 inference(scs_inference,[],[3,7,14])).
% 63.69/63.71 cnf(8948,plain,
% 63.69/63.71 (P2(a2,f5(a2),a1)),
% 63.69/63.71 inference(scs_inference,[],[2962,3,7,14,12,13,21])).
% 63.69/63.71 cnf(8952,plain,
% 63.69/63.71 (P1(f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[2962,3,7,14,12,13,21,22,9])).
% 63.69/63.71 cnf(8954,plain,
% 63.69/63.71 (P1(f7(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[2962,3,7,14,12,13,21,22,9,10])).
% 63.69/63.71 cnf(8956,plain,
% 63.69/63.71 (P1(f6(a2))),
% 63.69/63.71 inference(scs_inference,[],[5,2962,3,7,14,12,13,21,22,9,10,15])).
% 63.69/63.71 cnf(8958,plain,
% 63.69/63.71 (P2(a2,a2,f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[5,2962,3,7,14,12,13,21,22,9,10,15,16])).
% 63.69/63.71 cnf(8960,plain,
% 63.69/63.71 (P3(f6(a2),a2,a4)),
% 63.69/63.71 inference(scs_inference,[],[5,2962,3,7,14,12,13,21,22,9,10,15,16,19])).
% 63.69/63.71 cnf(8962,plain,
% 63.69/63.71 (P2(a1,a1,a1)),
% 63.69/63.71 inference(scs_inference,[],[5,2962,3,34,7,14,12,13,21,22,9,10,15,16,19,18])).
% 63.69/63.71 cnf(8964,plain,
% 63.69/63.71 (P3(a2,a2,f7(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[5,2962,3,34,7,14,12,13,21,22,9,10,15,16,19,18,17])).
% 63.69/63.71 cnf(8968,plain,
% 63.69/63.71 (~P2(a2,a2,a2)),
% 63.69/63.71 inference(scs_inference,[],[5,2962,3,34,7,14,12,13,21,22,9,10,15,16,19,18,17,24,25])).
% 63.69/63.71 cnf(8974,plain,
% 63.69/63.71 (P4(f3(a2,a2),f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[5,2962,7520,4374,3,34,46,7,14,12,13,21,22,9,10,15,16,19,18,17,24,25,27,26,23])).
% 63.69/63.71 cnf(8976,plain,
% 63.69/63.71 (~P3(a2,a4,x89761)+P2(f5(a2),x89761,a1)),
% 63.69/63.71 inference(scs_inference,[],[5,2962,7520,4374,3,3671,1888,34,46,7,14,12,13,21,22,9,10,15,16,19,18,17,24,25,27,26,23,28])).
% 63.69/63.71 cnf(8985,plain,
% 63.69/63.71 (P2(a1,f5(a2),f5(a2))),
% 63.69/63.71 inference(scs_inference,[],[8940,14,7,12])).
% 63.69/63.71 cnf(8987,plain,
% 63.69/63.71 (P3(a4,f3(a2,a2),f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[8940,8952,14,7,12,13])).
% 63.69/63.71 cnf(8989,plain,
% 63.69/63.71 (P3(a2,f6(a2),a4)),
% 63.69/63.71 inference(scs_inference,[],[8960,8940,8952,14,7,12,13,22])).
% 63.69/63.71 cnf(8991,plain,
% 63.69/63.71 (P2(f5(a2),f5(f5(a2)),a1)),
% 63.69/63.71 inference(scs_inference,[],[8960,8940,8952,14,7,12,13,22,21])).
% 63.69/63.71 cnf(9013,plain,
% 63.69/63.71 (P1(f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[8960,8940,8952,1135,2,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15])).
% 63.69/63.71 cnf(9015,plain,
% 63.69/63.71 (P2(f5(a2),f5(a2),f3(f5(a2),f5(a2)))),
% 63.69/63.71 inference(scs_inference,[],[8960,8940,8952,1135,2,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15,16])).
% 63.69/63.71 cnf(9017,plain,
% 63.69/63.71 (P3(f6(a4),a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[8960,8940,8952,1135,2,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15,16,19])).
% 63.69/63.71 cnf(9019,plain,
% 63.69/63.71 (P2(a1,f3(a2,a2),f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[8974,8960,8940,8952,1135,2,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15,16,19,18])).
% 63.69/63.71 cnf(9023,plain,
% 63.69/63.71 (~P2(f5(a2),a1,a1)),
% 63.69/63.71 inference(scs_inference,[],[8962,8974,8960,8940,8952,8948,1135,2,30,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15,16,19,18,17,24])).
% 63.69/63.71 cnf(9025,plain,
% 63.69/63.71 (~P3(f6(a4),f6(a4),a1)),
% 63.69/63.71 inference(scs_inference,[],[8962,8974,8960,8940,8952,8948,4374,1135,2,30,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15,16,19,18,17,24,27])).
% 63.69/63.71 cnf(9029,plain,
% 63.69/63.71 (P3(f6(a4),f5(a4),f5(a4))),
% 63.69/63.71 inference(scs_inference,[],[8962,8974,8960,8940,8952,8948,4374,1135,2,30,2895,34,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15,16,19,18,17,24,27,23,26])).
% 63.69/63.71 cnf(9037,plain,
% 63.69/63.71 (P3(a1,f6(a4),a1)),
% 63.69/63.71 inference(scs_inference,[],[8962,8974,8960,8940,8952,8948,8166,4374,1135,2,30,2895,1888,34,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15,16,19,18,17,24,27,23,26,29,4284,8976,1922])).
% 63.69/63.71 cnf(9039,plain,
% 63.69/63.71 (~P3(a1,a1,x90391)+P4(a1,x90391)),
% 63.69/63.71 inference(scs_inference,[],[8962,8974,8960,8940,8952,8948,8166,4374,1135,2,30,2895,1888,34,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15,16,19,18,17,24,27,23,26,29,4284,8976,1922,20])).
% 63.69/63.71 cnf(9041,plain,
% 63.69/63.71 (~P2(a1,f6(a4),a1)),
% 63.69/63.71 inference(scs_inference,[],[8962,8974,8960,8940,8952,8948,8166,4374,1135,2,30,2895,1888,34,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15,16,19,18,17,24,27,23,26,29,4284,8976,1922,20,28])).
% 63.69/63.71 cnf(9043,plain,
% 63.69/63.71 (~P3(f5(a1),f6(a2),x90431)+~P3(x90431,a2,a2)),
% 63.69/63.71 inference(scs_inference,[],[8962,8974,8960,8940,8952,8948,8166,4374,1135,2,30,2895,1888,34,14,7,12,13,22,21,6003,6516,8195,8239,8425,8861,7496,8766,10,9,15,16,19,18,17,24,27,23,26,29,4284,8976,1922,20,28,5598])).
% 63.69/63.71 cnf(9045,plain,
% 63.69/63.71 (P4(a1,f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[1,9039,17])).
% 63.69/63.71 cnf(9048,plain,
% 63.69/63.71 (P2(f5(f7(a2,a2)),f7(a2,a2),a1)),
% 63.69/63.71 inference(scs_inference,[],[8954,7,14])).
% 63.69/63.71 cnf(9050,plain,
% 63.69/63.71 (P2(a1,f7(a2,a2),f7(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[8954,7,14,12])).
% 63.69/63.71 cnf(9052,plain,
% 63.69/63.71 (P3(a4,f7(a2,a2),f7(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[8954,7,14,12,13])).
% 63.69/63.71 cnf(9054,plain,
% 63.69/63.71 (P2(f5(a2),a1,f5(a2))),
% 63.69/63.71 inference(scs_inference,[],[8985,8954,7,14,12,13,21])).
% 63.69/63.71 cnf(9056,plain,
% 63.69/63.71 (P3(f3(a2,a2),a4,f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[8985,8987,8954,7,14,12,13,21,22])).
% 63.69/63.71 cnf(9064,plain,
% 63.69/63.71 (P2(f7(a2,a2),f7(a2,a2),f3(f7(a2,a2),f7(a2,a2)))),
% 63.69/63.71 inference(scs_inference,[],[8985,8987,8954,9013,9041,7,14,12,13,21,22,10,9,15,16])).
% 63.69/63.71 cnf(9066,plain,
% 63.69/63.71 (P3(f6(f6(a4)),f6(a4),a4)),
% 63.69/63.71 inference(scs_inference,[],[8985,8987,8954,9013,9041,7,14,12,13,21,22,10,9,15,16,19])).
% 63.69/63.71 cnf(9068,plain,
% 63.69/63.71 (P2(a1,a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[8985,8987,8954,9013,9041,39,7,14,12,13,21,22,10,9,15,16,19,18])).
% 63.69/63.71 cnf(9074,plain,
% 63.69/63.71 (~P2(f5(a2),f3(a2,a2),a1)),
% 63.69/63.71 inference(scs_inference,[],[5,8985,8987,8954,9013,8958,9041,8991,8942,39,7,14,12,13,21,22,10,9,15,16,19,18,17,24,25])).
% 63.69/63.71 cnf(9076,plain,
% 63.69/63.71 (P3(f6(a4),f3(a2,a2),f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[5,8985,8987,8954,9013,8958,9017,9041,8991,8942,39,7,14,12,13,21,22,10,9,15,16,19,18,17,24,25,26])).
% 63.69/63.71 cnf(9080,plain,
% 63.69/63.71 (P3(f3(a2,a2),a2,f3(f7(a2,a2),f7(a2,a2)))),
% 63.69/63.71 inference(scs_inference,[],[5,8985,8987,8954,9013,8958,8964,8989,9017,9041,8991,8942,7520,39,7,14,12,13,21,22,10,9,15,16,19,18,17,24,25,26,27,29])).
% 63.69/63.71 cnf(9091,plain,
% 63.69/63.71 (P2(f5(f6(a2)),f6(a2),a1)),
% 63.69/63.71 inference(scs_inference,[],[8956,14])).
% 63.69/63.71 cnf(9095,plain,
% 63.69/63.71 (P2(a1,f6(a2),f6(a2))),
% 63.69/63.71 inference(scs_inference,[],[8956,14,7,12])).
% 63.69/63.71 cnf(9097,plain,
% 63.69/63.71 (P3(a4,f6(a2),f6(a2))),
% 63.69/63.71 inference(scs_inference,[],[8956,14,7,12,13])).
% 63.69/63.71 cnf(9099,plain,
% 63.69/63.71 (P3(f3(a2,a2),f6(a4),f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[9076,8956,14,7,12,13,22])).
% 63.69/63.71 cnf(9101,plain,
% 63.69/63.71 (P2(a4,a1,a4)),
% 63.69/63.71 inference(scs_inference,[],[9068,9076,8956,14,7,12,13,22,21])).
% 63.69/63.71 cnf(9107,plain,
% 63.69/63.71 (P2(f6(a2),f6(a2),f3(f6(a2),f6(a2)))),
% 63.69/63.71 inference(scs_inference,[],[9068,9076,8956,14,7,12,13,22,21,10,9,16])).
% 63.69/63.71 cnf(9109,plain,
% 63.69/63.71 (P2(a1,a2,a2)),
% 63.69/63.71 inference(scs_inference,[],[9068,9076,8956,46,14,7,12,13,22,21,10,9,16,18])).
% 63.69/63.71 cnf(9111,plain,
% 63.69/63.71 (P3(f6(a2),f6(a2),f7(f6(a2),f6(a2)))),
% 63.69/63.71 inference(scs_inference,[],[9068,9076,8956,46,14,7,12,13,22,21,10,9,16,18,17])).
% 63.69/63.71 cnf(9115,plain,
% 63.69/63.71 (P2(f3(f5(a2),f5(a2)),a2,f5(a2))),
% 63.69/63.71 inference(scs_inference,[],[8968,9068,9076,8956,9054,9015,8948,8942,46,14,7,12,13,22,21,10,9,16,18,17,24,25])).
% 63.69/63.71 cnf(9117,plain,
% 63.69/63.71 (P3(f6(f6(a4)),f3(a2,a2),f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[8968,9068,9076,8956,9054,9066,9015,8948,8942,8987,46,14,7,12,13,22,21,10,9,16,18,17,24,25,26])).
% 63.69/63.71 cnf(9128,plain,
% 63.69/63.71 (P2(a1,f6(a4),f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[8952,9013,7,12])).
% 63.69/63.71 cnf(9130,plain,
% 63.69/63.71 (P2(f5(f3(a2,a2)),f3(a2,a2),a1)),
% 63.69/63.71 inference(scs_inference,[],[8952,9013,7,12,14])).
% 63.69/63.71 cnf(9132,plain,
% 63.69/63.71 (P3(a4,f6(a4),f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[8952,9013,7,12,14,13])).
% 63.69/63.71 cnf(9134,plain,
% 63.69/63.71 (P2(a2,a1,a2)),
% 63.69/63.71 inference(scs_inference,[],[9109,8952,9013,7,12,14,13,21])).
% 63.69/63.71 cnf(9144,plain,
% 63.69/63.71 (P2(f3(a2,a2),f3(a2,a2),f3(f3(a2,a2),f3(a2,a2)))),
% 63.69/63.71 inference(scs_inference,[],[9109,9029,8952,9066,9013,7,12,14,13,21,22,8714,10,9,16])).
% 63.69/63.71 cnf(9148,plain,
% 63.69/63.71 (~P2(a2,f5(a2),a2)),
% 63.69/63.71 inference(scs_inference,[],[5,9109,9029,8952,8948,9066,9013,7,12,14,13,21,22,8714,10,9,16,17,24])).
% 63.69/63.71 cnf(9150,plain,
% 63.69/63.71 (~P2(f7(a2,a2),a2,f7(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[5,9109,9029,9048,8952,8948,9066,9013,7,12,14,13,21,22,8714,10,9,16,17,24,25])).
% 63.69/63.71 cnf(9152,plain,
% 63.69/63.71 (P3(f6(a4),f7(a2,a2),f7(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[5,9109,9029,9052,9048,8952,8948,9066,9013,9017,7,12,14,13,21,22,8714,10,9,16,17,24,25,26])).
% 63.69/63.71 cnf(9154,plain,
% 63.69/63.71 (P3(f3(f7(a2,a2),f7(a2,a2)),f6(a2),f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[5,9109,9056,9029,9052,9048,9080,8952,8948,8989,9066,9013,9017,7,12,14,13,21,22,8714,10,9,16,17,24,25,26,27])).
% 63.69/63.71 cnf(9162,plain,
% 63.69/63.71 (P2(f5(f6(a4)),f6(a4),a1)),
% 63.69/63.71 inference(scs_inference,[],[9013,14])).
% 63.69/63.71 cnf(9166,plain,
% 63.69/63.71 (P3(a4,a2,a2)),
% 63.69/63.71 inference(scs_inference,[],[9013,3,14,7,13])).
% 63.69/63.71 cnf(9168,plain,
% 63.69/63.71 (P3(f7(a2,a2),f6(a4),f7(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[9152,9013,3,14,7,13,22])).
% 63.69/63.71 cnf(9170,plain,
% 63.69/63.71 (P2(f7(a2,a2),a1,f7(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[9050,9152,9013,3,14,7,13,22,21])).
% 63.69/63.71 cnf(9182,plain,
% 63.69/63.71 (P2(f6(a4),f6(a4),f3(f6(a4),f6(a4)))),
% 63.69/63.71 inference(scs_inference,[],[9050,9152,9013,8960,3,14,7,13,22,21,7130,8710,8199,10,9,16])).
% 63.69/63.71 cnf(9184,plain,
% 63.69/63.71 (P3(f6(a4),f6(a4),f7(f6(a4),f6(a4)))),
% 63.69/63.71 inference(scs_inference,[],[9050,9152,9013,8960,3,14,7,13,22,21,7130,8710,8199,10,9,16,17])).
% 63.69/63.71 cnf(9186,plain,
% 63.69/63.71 (P3(f6(a4),f6(a2),f6(a2))),
% 63.69/63.71 inference(scs_inference,[],[9050,9152,9097,9017,9013,8960,3,14,7,13,22,21,7130,8710,8199,10,9,16,17,26])).
% 63.69/63.71 cnf(9188,plain,
% 63.69/63.71 (~P2(a4,a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[9050,9152,9097,8968,9017,9013,8960,3,14,7,13,22,21,7130,8710,8199,10,9,16,17,26,28])).
% 63.69/63.71 cnf(9192,plain,
% 63.69/63.71 (~P3(a2,a4,f3(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[9050,9152,9074,9097,8968,9017,9013,8960,3,14,7,13,22,21,7130,8710,8199,10,9,16,17,26,28,9043,8976])).
% 63.69/63.71 cnf(9196,plain,
% 63.69/63.71 (~P2(f5(a2),a1,f5(f3(a2,a2)))),
% 63.69/63.71 inference(scs_inference,[],[9050,9152,9074,9097,9130,9019,8968,9045,9017,9013,8960,3,14,7,13,22,21,7130,8710,8199,10,9,16,17,26,28,9043,8976,18,24])).
% 63.69/63.71 cnf(9202,plain,
% 63.69/63.71 (P1(f5(a1))),
% 63.69/63.71 inference(scs_inference,[],[1,7])).
% 63.69/63.71 cnf(9204,plain,
% 63.69/63.71 (P2(f5(a1),a1,a1)),
% 63.69/63.71 inference(scs_inference,[],[1,7,14])).
% 63.69/63.71 cnf(9206,plain,
% 63.69/63.71 (P3(a4,a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[1,2,7,14,13])).
% 63.69/63.71 cnf(9208,plain,
% 63.69/63.71 (P3(a2,a4,a2)),
% 63.69/63.71 inference(scs_inference,[],[9166,1,2,7,14,13,22])).
% 63.69/63.71 cnf(9210,plain,
% 63.69/63.71 (P2(f6(a2),a1,f6(a2))),
% 63.69/63.71 inference(scs_inference,[],[9166,9095,1,2,7,14,13,22,21])).
% 63.69/63.71 cnf(9214,plain,
% 63.69/63.71 (P1(f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9166,9095,8989,1,2,7,14,13,22,21,7252,10])).
% 63.69/63.71 cnf(9216,plain,
% 63.69/63.71 (P1(f3(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9166,9095,8989,1,2,7,14,13,22,21,7252,10,9])).
% 63.69/63.71 cnf(9220,plain,
% 63.69/63.71 (P2(a1,a1,f3(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9166,9095,8989,1,2,7,14,13,22,21,7252,10,9,3586,16])).
% 63.69/63.71 cnf(9222,plain,
% 63.69/63.71 (P3(a1,a1,f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9166,9095,8989,1,2,7,14,13,22,21,7252,10,9,3586,16,17])).
% 63.69/63.71 cnf(9224,plain,
% 63.69/63.71 (~P2(a1,a1,f5(a2))),
% 63.69/63.71 inference(scs_inference,[],[9166,9095,9148,9134,8989,1,2,7,14,13,22,21,7252,10,9,3586,16,17,24])).
% 63.69/63.71 cnf(9226,plain,
% 63.69/63.71 (~P2(f6(a4),a2,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[5,9166,9095,9148,9162,9134,8989,1,2,7,14,13,22,21,7252,10,9,3586,16,17,24,25])).
% 63.69/63.71 cnf(9228,plain,
% 63.69/63.71 (P3(f7(a2,a2),a4,f7(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[5,9166,9095,9148,9162,9134,8964,8989,1,2,7,14,13,22,21,7252,10,9,3586,16,17,24,25,27])).
% 63.69/63.71 cnf(9232,plain,
% 63.69/63.71 (~P2(f7(a1,a1),f7(a1,a1),f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[5,9188,9166,9095,9148,9162,9134,5577,8962,8964,8989,8960,1,2,7,14,13,22,21,7252,10,9,3586,16,17,24,25,27,28,29])).
% 63.69/63.71 cnf(9234,plain,
% 63.69/63.71 (P2(a1,f5(a1),f5(a1))),
% 63.69/63.71 inference(scs_inference,[],[5,9188,9166,9095,9148,9162,9134,5577,8962,8964,8989,8960,1,2,7,14,13,22,21,7252,10,9,3586,16,17,24,25,27,28,29,12])).
% 63.69/63.71 cnf(9250,plain,
% 63.69/63.71 (P2(a1,f7(a1,a1),f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9214,12])).
% 63.69/63.71 cnf(9252,plain,
% 63.69/63.71 (P2(f5(f7(a1,a1)),f7(a1,a1),a1)),
% 63.69/63.71 inference(scs_inference,[],[9214,12,14])).
% 63.69/63.71 cnf(9256,plain,
% 63.69/63.71 (P3(a4,f7(a1,a1),f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9214,12,14,7,13])).
% 63.69/63.71 cnf(9258,plain,
% 63.69/63.71 (P3(f6(a2),f6(a4),f6(a2))),
% 63.69/63.71 inference(scs_inference,[],[9214,9186,12,14,7,13,22])).
% 63.69/63.71 cnf(9260,plain,
% 63.69/63.71 (P2(f6(a4),a1,f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[9214,9128,9186,12,14,7,13,22,21])).
% 63.69/63.71 cnf(9284,plain,
% 63.69/63.71 (P2(f7(a1,a1),f7(a1,a1),f3(f7(a1,a1),f7(a1,a1)))),
% 63.69/63.71 inference(scs_inference,[],[9208,9214,9128,9186,9066,9017,12,14,7,13,22,21,6516,6003,8766,8425,8239,7496,8195,5598,10,8861,9,16])).
% 63.69/63.71 cnf(9286,plain,
% 63.69/63.71 (P3(f7(a1,a1),f7(a1,a1),f7(f7(a1,a1),f7(a1,a1)))),
% 63.69/63.71 inference(scs_inference,[],[9208,9214,9128,9186,9066,9017,12,14,7,13,22,21,6516,6003,8766,8425,8239,7496,8195,5598,10,8861,9,16,17])).
% 63.69/63.71 cnf(9290,plain,
% 63.69/63.71 (P2(f6(a2),f3(a1,a1),f6(a2))),
% 63.69/63.71 inference(scs_inference,[],[9208,9214,9128,9210,9186,9220,9045,9066,9017,12,14,7,13,22,21,6516,6003,8766,8425,8239,7496,8195,5598,10,8861,9,16,17,20,24])).
% 63.69/63.71 cnf(9294,plain,
% 63.69/63.71 (P2(f3(a1,a1),f6(a4),f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[9208,9214,9128,9210,9186,9220,9045,9066,9017,34,12,14,7,13,22,21,6516,6003,8766,8425,8239,7496,8195,5598,10,8861,9,16,17,20,24,23,25])).
% 63.69/63.71 cnf(9296,plain,
% 63.69/63.71 (P3(f7(f6(a4),f6(a4)),f6(a2),f6(a2))),
% 63.69/63.71 inference(scs_inference,[],[9208,9214,9128,9210,9186,9220,9184,9045,9066,9017,34,12,14,7,13,22,21,6516,6003,8766,8425,8239,7496,8195,5598,10,8861,9,16,17,20,24,23,25,27])).
% 63.69/63.71 cnf(9298,plain,
% 63.69/63.71 (~P3(f5(a2),a4,a1)),
% 63.69/63.71 inference(scs_inference,[],[5,9208,9214,9128,9210,9186,9220,9184,9045,8942,9066,9017,1888,34,12,14,7,13,22,21,6516,6003,8766,8425,8239,7496,8195,5598,10,8861,9,16,17,20,24,23,25,27,28])).
% 63.69/63.71 cnf(9300,plain,
% 63.69/63.71 (~P2(a1,f7(f6(a4),f6(a4)),a1)),
% 63.69/63.71 inference(scs_inference,[],[5,9208,9214,9128,9210,9186,9025,9220,9184,9037,9045,8942,9066,9017,1888,34,12,14,7,13,22,21,6516,6003,8766,8425,8239,7496,8195,5598,10,8861,9,16,17,20,24,23,25,27,28,29])).
% 63.69/63.71 cnf(9306,plain,
% 63.69/63.71 (P2(f5(f3(a1,a1)),f3(a1,a1),a1)),
% 63.69/63.71 inference(scs_inference,[],[9216,14])).
% 63.69/63.71 cnf(9308,plain,
% 63.69/63.71 (P2(a1,f3(a1,a1),f3(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9216,14,12])).
% 63.69/63.71 cnf(9312,plain,
% 63.69/63.71 (P3(a4,f3(a1,a1),f3(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9216,9202,14,12,7,13])).
% 63.69/63.71 cnf(9314,plain,
% 63.69/63.71 (P3(f7(a1,a1),a4,f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9256,9216,9202,14,12,7,13,22])).
% 63.69/63.71 cnf(9316,plain,
% 63.69/63.71 (P2(f7(a1,a1),a1,f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9256,9216,9250,9202,14,12,7,13,22,21])).
% 63.69/63.71 cnf(9326,plain,
% 63.69/63.71 (P2(f3(a1,a1),f3(a1,a1),f3(f3(a1,a1),f3(a1,a1)))),
% 63.69/63.71 inference(scs_inference,[],[9256,9216,9250,9202,9208,8989,14,12,7,13,22,21,5998,10,54,9,16])).
% 63.69/63.71 cnf(9330,plain,
% 63.69/63.71 (~P2(f5(a1),a1,a2)),
% 63.69/63.71 inference(scs_inference,[],[5,9256,9216,9250,9202,9204,9234,9208,8989,14,12,7,13,22,21,5998,10,54,9,16,17,24])).
% 63.69/63.71 cnf(9334,plain,
% 63.69/63.71 (P3(f7(a1,a1),f6(a4),f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[5,9256,9216,9250,9202,9204,9222,9234,9208,9037,8989,34,14,12,7,13,22,21,5998,10,54,9,16,17,24,23,27])).
% 63.69/63.71 cnf(9336,plain,
% 63.69/63.71 (P2(a1,f3(a1,a1),a1)),
% 63.69/63.71 inference(scs_inference,[],[5,9256,9216,9250,9290,9202,9204,9091,9222,9234,9208,9037,8989,34,14,12,7,13,22,21,5998,10,54,9,16,17,24,23,27,25])).
% 63.69/63.71 cnf(9338,plain,
% 63.69/63.71 (P3(f7(f6(a4),f6(a4)),a4,a4)),
% 63.69/63.71 inference(scs_inference,[],[5,9256,9216,9250,9290,9202,9204,9091,9296,9222,9234,9208,9037,8989,8960,34,14,12,7,13,22,21,5998,10,54,9,16,17,24,23,27,25,26])).
% 63.69/63.71 cnf(9342,plain,
% 63.69/63.71 (~P3(f3(f5(a2),f5(a2)),a4,f5(a2))),
% 63.69/63.71 inference(scs_inference,[],[5,9256,9216,9224,9250,9290,9202,9204,9298,9091,9296,9115,9222,9234,9220,9208,9037,8942,8989,8960,34,14,12,7,13,22,21,5998,10,54,9,16,17,24,23,27,25,26,28,29])).
% 63.69/63.71 cnf(9346,plain,
% 63.69/63.71 (P3(a1,f7(f6(a4),f6(a4)),a1)),
% 63.69/63.71 inference(scs_inference,[],[5,9256,9216,9224,9250,9290,9202,9204,9298,9091,9296,9115,9222,9234,9220,9208,9037,8942,8989,8960,34,14,12,7,13,22,21,5998,10,54,9,16,17,24,23,27,25,26,28,29,4284,1922])).
% 63.69/63.71 cnf(9354,plain,
% 63.69/63.71 (~P2(f5(f3(a1,a1)),f3(a1,a1),a2)),
% 63.69/63.71 inference(scs_inference,[],[5,9256,9216,9224,9250,9290,9202,9204,9298,9091,9296,9115,9222,9234,9220,9208,9037,8942,8964,8989,8960,3,1,34,14,12,7,13,22,21,5998,10,54,9,16,17,24,23,27,25,26,28,29,4284,1922,1457,8,20,66])).
% 63.69/63.71 cnf(9365,plain,
% 63.69/63.71 (P1(f5(a4))),
% 63.69/63.71 inference(scs_inference,[],[2,7])).
% 63.69/63.71 cnf(9367,plain,
% 63.69/63.71 (P2(f5(a4),a4,a1)),
% 63.69/63.71 inference(scs_inference,[],[2,7,14])).
% 63.69/63.71 cnf(9369,plain,
% 63.69/63.71 (P3(a4,f5(a1),f5(a1))),
% 63.69/63.71 inference(scs_inference,[],[9202,2,7,14,13])).
% 63.69/63.71 cnf(9371,plain,
% 63.69/63.71 (P2(f6(a4),f3(a1,a1),f6(a4))),
% 63.69/63.71 inference(scs_inference,[],[9294,9202,2,7,14,13,21])).
% 63.69/63.71 cnf(9373,plain,
% 63.69/63.71 (P3(f6(a4),f7(a1,a1),f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9334,9294,9202,2,7,14,13,21,22])).
% 63.69/63.71 cnf(9383,plain,
% 63.69/63.71 (P1(f7(a4,a4))),
% 63.69/63.71 inference(scs_inference,[],[9334,9294,9338,9202,9256,9208,9017,2,7,14,13,21,22,6516,8196,6279,5998,10])).
% 63.69/63.71 cnf(9387,plain,
% 63.69/63.71 (P2(a4,a4,f3(a4,a4))),
% 63.69/63.71 inference(scs_inference,[],[9334,9294,9338,9202,9256,9208,9017,2,7,14,13,21,22,6516,8196,6279,5998,10,9,16])).
% 63.69/63.71 cnf(9391,plain,
% 63.69/63.71 (P2(f7(a1,a1),f3(a1,a1),f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9334,9316,9294,9338,9202,9256,9220,9208,9017,2,7,14,13,21,22,6516,8196,6279,5998,10,9,16,17,24])).
% 63.69/63.71 cnf(9393,plain,
% 63.69/63.71 (P3(f7(a1,a1),f7(f6(a4),f6(a4)),f7(a1,a1))),
% 63.69/63.71 inference(scs_inference,[],[9334,9316,9294,9338,9346,9202,9256,9222,9220,9208,9017,2,7,14,13,21,22,6516,8196,6279,5998,10,9,16,17,24,27])).
% 63.69/63.71 cnf(9395,plain,
% 63.69/63.71 (P2(f7(a2,a2),f3(a1,a1),f7(a2,a2))),
% 63.69/63.71 inference(scs_inference,[],[9334,9316,9294,9170,9336,9338,9346,9202,9256,9222,9220,9208,9017,2,7,14,13,21,22,6516,8196,6279,5998,10,9,16,17,24,27,25])).
% 63.69/63.71 cnf(9399,plain,
% 63.69/63.71 (P3(f3(a4,a4),f3(a1,a1),f3(f3(a1,a1),f3(a1,a1)))),
% 63.69/63.71 inference(scs_inference,[],[9334,9232,9316,9294,9312,9170,9336,9284,9326,9338,9346,9202,9256,9222,9220,9208,9017,2,7,14,13,21,22,6516,8196,6279,5998,10,9,16,17,24,27,25,28,29])).
% 63.69/63.71 cnf(9410,plain,
% 63.69/63.71 (P2(a1,f7(a4,a4),f7(a4,a4))),
% 63.69/63.71 inference(scs_inference,[],[9334,9232,9316,9294,9312,9170,9336,9284,9326,9338,9346,9202,9256,9222,9220,9208,9017,2,7,14,13,21,22,6516,8196,6279,5998,10,9,16,17,24,27,25,28,29,7692,7965,8526,8542,8558,8689,8705,8737,8797,12])).
% 63.69/63.71 cnf(9416,plain,
% 63.69/63.71 (P2(a1,f3(a4,a4),f3(a4,a4))),
% 63.69/63.71 inference(scs_inference,[],[9334,9232,9316,9294,9312,9170,9336,9284,9326,9338,9346,9286,9202,9256,9222,9220,9208,9017,2,7,14,13,21,22,6516,8196,6279,5998,10,9,16,17,24,27,25,28,29,7692,7965,8526,8542,8558,8689,8705,8737,8797,12,48,8714,18])).
% 63.69/63.71 cnf(9421,plain,
% 63.69/63.71 (P2(f5(f7(a4,a4)),f7(a4,a4),a1)),
% 63.69/63.71 inference(scs_inference,[],[9383,14])).
% 63.69/63.72 cnf(9425,plain,
% 63.69/63.72 (P3(a4,f7(a4,a4),f7(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9383,14,7,13])).
% 63.69/63.72 cnf(9427,plain,
% 63.69/63.72 (P2(f3(a1,a1),f7(a1,a1),f7(a1,a1))),
% 63.69/63.72 inference(scs_inference,[],[9391,9383,14,7,13,21])).
% 63.69/63.72 cnf(9429,plain,
% 63.69/63.72 (P3(f5(a1),a4,f5(a1))),
% 63.69/63.72 inference(scs_inference,[],[9391,9383,9369,14,7,13,21,22])).
% 63.69/63.72 cnf(9441,plain,
% 63.69/63.72 (P2(f7(a4,a4),f7(a4,a4),f3(f7(a4,a4),f7(a4,a4)))),
% 63.69/63.72 inference(scs_inference,[],[9391,9383,9373,9369,9166,9066,8960,14,7,13,21,22,6516,6629,5998,10,9,16])).
% 63.69/63.72 cnf(9443,plain,
% 63.69/63.72 (P3(f7(a4,a4),f7(a4,a4),f7(f7(a4,a4),f7(a4,a4)))),
% 63.69/63.72 inference(scs_inference,[],[9391,9383,9373,9369,9166,9066,8960,14,7,13,21,22,6516,6629,5998,10,9,16,17])).
% 63.69/63.72 cnf(9445,plain,
% 63.69/63.72 (~P2(f3(a1,a1),f3(a1,a1),a2)),
% 63.69/63.72 inference(scs_inference,[],[9391,9383,9395,9373,9150,9369,9166,9066,8960,14,7,13,21,22,6516,6629,5998,10,9,16,17,24])).
% 63.69/63.72 cnf(9449,plain,
% 63.69/63.72 (P2(f3(f5(a1),f5(a1)),a1,a1)),
% 63.69/63.72 inference(scs_inference,[],[9391,9383,9395,9373,9150,9369,9204,9166,9184,9066,8960,402,14,7,13,21,22,6516,6629,5998,10,9,16,17,24,27,25])).
% 63.69/63.72 cnf(9451,plain,
% 63.69/63.72 (P3(f6(a2),f7(f6(a4),f6(a4)),f6(a2))),
% 63.69/63.72 inference(scs_inference,[],[9391,9258,9383,9395,9373,9150,9369,9204,9166,9184,9066,8960,402,14,7,13,21,22,6516,6629,5998,10,9,16,17,24,27,25,26])).
% 63.69/63.72 cnf(9455,plain,
% 63.69/63.72 (P3(f3(a4,a4),f5(a1),f3(f5(a1),f5(a1)))),
% 63.69/63.72 inference(scs_inference,[],[9391,9258,9383,9395,9373,9150,9369,9387,9182,9232,9204,9166,9184,9066,8960,402,14,7,13,21,22,6516,6629,5998,10,9,16,17,24,27,25,26,28,29])).
% 63.69/63.72 cnf(9463,plain,
% 63.69/63.72 (P2(f5(f5(a4)),f5(a4),a1)),
% 63.69/63.72 inference(scs_inference,[],[9365,7,14])).
% 63.69/63.72 cnf(9465,plain,
% 63.69/63.72 (P2(f3(a1,a1),a1,f3(a1,a1))),
% 63.69/63.72 inference(scs_inference,[],[9308,9365,7,14,21])).
% 63.69/63.72 cnf(9467,plain,
% 63.69/63.72 (P3(f7(a4,a4),a4,f7(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9308,9425,9365,7,14,21,22])).
% 63.69/63.72 cnf(9479,plain,
% 63.69/63.72 (P2(f5(a4),f5(a4),f3(f5(a4),f5(a4)))),
% 63.69/63.72 inference(scs_inference,[],[9308,9425,9365,9208,8989,9017,7,14,21,22,8710,7130,6003,10,9,16])).
% 63.69/63.72 cnf(9481,plain,
% 63.69/63.72 (P3(a4,a4,f7(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9308,9425,9365,9208,8989,9017,2,7,14,21,22,8710,7130,6003,10,9,16,17])).
% 63.69/63.72 cnf(9483,plain,
% 63.69/63.72 (~P2(f5(a4),a4,a2)),
% 63.69/63.72 inference(scs_inference,[],[5,9308,9425,9367,9365,9208,8989,9017,2,80,7,14,21,22,8710,7130,6003,10,9,16,17,24])).
% 63.69/63.72 cnf(9485,plain,
% 63.69/63.72 (P3(f3(a2,a2),f7(f6(a4),f6(a4)),f3(a2,a2))),
% 63.69/63.72 inference(scs_inference,[],[5,9308,9425,9367,9154,9451,9365,9208,8989,9017,2,80,7,14,21,22,8710,7130,6003,10,9,16,17,24,27])).
% 63.69/63.72 cnf(9491,plain,
% 63.69/63.72 (P3(f3(a4,a4),f7(a4,a4),f3(f7(a4,a4),f7(a4,a4)))),
% 63.69/63.72 inference(scs_inference,[],[5,9308,9260,9425,9367,9154,9252,9451,9441,9365,9336,9387,9346,9232,9208,8989,9017,2,80,7,14,21,22,8710,7130,6003,10,9,16,17,24,27,25,28,29])).
% 63.69/63.72 cnf(9501,plain,
% 63.69/63.72 (P2(f7(a4,a4),a1,f7(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9410,21])).
% 63.69/63.72 cnf(9507,plain,
% 63.69/63.72 (P1(f3(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9410,9485,8989,2,21,22,6516,9])).
% 63.69/63.72 cnf(9513,plain,
% 63.69/63.72 (P2(f7(a1,a1),f3(f3(a1,a1),f3(a1,a1)),f7(a1,a1))),
% 63.69/63.72 inference(scs_inference,[],[9410,9485,9391,9326,8989,2,21,22,6516,9,16,17,24])).
% 63.69/63.72 cnf(9515,plain,
% 63.69/63.72 (P3(a4,f6(a4),a4)),
% 63.69/63.72 inference(scs_inference,[],[9410,9485,9391,9326,9258,8989,2,21,22,6516,9,16,17,24,27])).
% 63.69/63.72 cnf(9517,plain,
% 63.69/63.72 (P2(f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 63.69/63.72 inference(scs_inference,[],[9410,9465,9485,9391,9326,9258,9336,8989,2,21,22,6516,9,16,17,24,27,25])).
% 63.69/63.72 cnf(9523,plain,
% 63.69/63.72 (P2(f5(f3(a4,a4)),f3(a4,a4),a1)),
% 63.69/63.72 inference(scs_inference,[],[9410,9445,9465,9485,9391,9312,9326,9258,9336,9387,4289,8962,9222,8989,2,21,22,6516,9,16,17,24,27,25,28,29,14])).
% 63.69/63.72 cnf(9525,plain,
% 63.69/63.72 (P3(a4,f3(a4,a4),f3(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9410,9445,9465,9485,9391,9312,9326,9258,9336,9387,4289,8962,9222,8989,2,21,22,6516,9,16,17,24,27,25,28,29,14,13])).
% 63.69/63.72 cnf(9533,plain,
% 63.69/63.72 (P2(f3(a4,a4),a1,f3(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9416,21])).
% 63.69/63.72 cnf(9535,plain,
% 63.69/63.72 (P3(f3(a4,a4),a4,f3(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9416,9525,21,22])).
% 63.69/63.72 cnf(9539,plain,
% 63.69/63.72 (~P3(f7(a1,a1),f6(a4),a2)),
% 63.69/63.72 inference(scs_inference,[],[9416,9525,9515,9429,9314,21,22,6003,6629])).
% 63.69/63.72 cnf(9549,plain,
% 63.69/63.72 (~P3(f7(a1,a1),f6(a4),a4)),
% 63.69/63.72 inference(scs_inference,[],[9416,9525,9515,9429,9314,9338,9208,8989,21,22,6003,6629,8766,8239,8425,5598,8195])).
% 63.69/63.72 cnf(9559,plain,
% 63.69/63.72 (P2(f7(a4,a4),f3(a1,a1),f7(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9416,9507,9501,9525,9515,9429,9314,9166,9220,9338,9208,8989,21,22,6003,6629,8766,8239,8425,5598,8195,8861,7496,3586,9,24])).
% 63.69/63.72 cnf(9561,plain,
% 63.69/63.72 (P3(f7(a4,a4),f3(a4,a4),f3(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9416,9507,9501,9525,9515,9429,9314,9481,9166,9220,9338,9208,8989,21,22,6003,6629,8766,8239,8425,5598,8195,8861,7496,3586,9,24,27])).
% 63.69/63.72 cnf(9563,plain,
% 63.69/63.72 (P2(f3(a1,a1),f3(a4,a4),f3(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9416,9507,9501,9525,9515,9429,9314,9481,9166,9220,9338,9208,8989,21,22,6003,6629,8766,8239,8425,5598,8195,8861,7496,3586,9,24,27,25])).
% 63.69/63.72 cnf(9573,plain,
% 63.69/63.72 (P2(f3(a4,a4),f3(a1,a1),f3(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9563,21])).
% 63.69/63.72 cnf(9583,plain,
% 63.69/63.72 (P3(f7(f7(a4,a4),f7(a4,a4)),f3(a4,a4),f3(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9561,9563,9330,9443,9449,9308,9410,9134,34,21,22,54,24,23,27])).
% 63.69/63.72 cnf(9585,plain,
% 63.69/63.72 (P2(f3(f5(a4),f5(a4)),a4,f5(a4))),
% 63.69/63.72 inference(scs_inference,[],[9561,9563,9330,9443,9479,9449,9308,9410,9367,9134,3631,34,21,22,54,24,23,27,25])).
% 63.69/63.72 cnf(9587,plain,
% 63.69/63.72 (P2(f5(a4),f7(a4,a4),a1)),
% 63.69/63.72 inference(scs_inference,[],[9561,9563,9330,9443,9479,9449,9308,9410,9367,9134,9481,3631,3660,1888,34,21,22,54,24,23,27,25,28])).
% 63.69/63.72 cnf(9595,plain,
% 63.69/63.72 (P3(f3(a4,a4),f7(f7(a4,a4),f7(a4,a4)),f3(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9583,22])).
% 63.69/63.72 cnf(9597,plain,
% 63.69/63.72 (P2(f3(a1,a1),f7(a4,a4),f7(a4,a4))),
% 63.69/63.72 inference(scs_inference,[],[9559,9583,22,21])).
% 63.77/63.72 cnf(9603,plain,
% 63.77/63.72 (~P2(a1,f5(f5(a2)),a1)),
% 63.77/63.72 inference(scs_inference,[],[9559,9583,9023,8991,9054,9256,9208,9017,22,21,8199,6516,24])).
% 63.77/63.72 cnf(9607,plain,
% 63.77/63.72 (P3(a4,f7(f6(a4),f6(a4)),a4)),
% 63.77/63.72 inference(scs_inference,[],[9559,9583,9023,8991,9054,9451,9095,9256,9208,9017,8989,34,22,21,8199,6516,24,23,27])).
% 63.77/63.72 cnf(9609,plain,
% 63.77/63.72 (~P2(f3(a2,a2),a2,f3(a2,a2))),
% 63.77/63.72 inference(scs_inference,[],[5,9559,9583,9023,9130,8991,9054,9451,9095,9256,9208,9017,8989,34,22,21,8199,6516,24,23,27,25])).
% 63.77/63.72 cnf(9611,plain,
% 63.77/63.72 (~P3(a1,f7(f6(a4),f6(a4)),a2)),
% 63.77/63.72 inference(scs_inference,[],[5,9559,9583,9023,9130,8991,9054,9451,9095,9346,8962,9256,9208,9017,8989,34,22,21,8199,6516,24,23,27,25,28])).
% 63.77/63.72 cnf(9613,plain,
% 63.77/63.72 (~P2(f5(a2),f5(a2),f5(a2))),
% 63.77/63.72 inference(scs_inference,[],[5,9559,9583,9342,9023,9130,9015,8991,9054,9451,9095,9346,8962,9256,9208,9017,8989,3671,34,22,21,8199,6516,24,23,27,25,28,29])).
% 63.77/63.72 cnf(9615,plain,
% 63.77/63.72 (~P3(a1,a1,f7(f6(a4),f6(a4)))),
% 63.77/63.72 inference(scs_inference,[],[5,9559,9583,9342,9023,9130,9015,8991,9054,9451,9095,9346,8962,9256,9208,9017,8989,3671,34,22,21,8199,6516,24,23,27,25,28,29,4290])).
% 63.77/63.72 cnf(9617,plain,
% 63.77/63.72 (~P3(a1,f7(f6(a4),f6(a4)),a4)),
% 63.77/63.72 inference(scs_inference,[],[5,9559,9583,9342,9023,9130,9015,8991,9054,9451,9095,9346,8962,9256,9208,9017,8989,3671,34,22,21,8199,6516,24,23,27,25,28,29,4290,5532])).
% 63.77/63.72 cnf(9625,plain,
% 63.77/63.72 (P2(f7(a4,a4),f5(a4),a1)),
% 63.77/63.72 inference(scs_inference,[],[9587,21])).
% 63.77/63.72 cnf(9627,plain,
% 63.77/63.72 (P3(f7(a4,a4),f3(a4,a4),f3(f7(a4,a4),f7(a4,a4)))),
% 63.77/63.72 inference(scs_inference,[],[9587,9491,21,22])).
% 63.77/63.72 cnf(9631,plain,
% 63.77/63.72 (~P3(f7(a1,a1),f7(f6(a4),f6(a4)),f6(a4))),
% 63.77/63.72 inference(scs_inference,[],[9587,9491,9607,9314,9166,9515,21,22,7252,8714])).
% 63.77/63.72 cnf(9637,plain,
% 63.77/63.72 (~P3(f7(a1,a1),f7(f6(a4),f6(a4)),a4)),
% 63.77/63.72 inference(scs_inference,[],[9587,9491,9607,9314,9166,9256,9515,9017,21,22,7252,8714,6629,5998,8195])).
% 63.77/63.72 cnf(9639,plain,
% 63.77/63.72 (~P2(f7(a4,a4),a2,a4)),
% 63.77/63.72 inference(scs_inference,[],[9483,9587,9491,9607,9109,9314,9166,9256,9515,9017,21,22,7252,8714,6629,5998,8195,24])).
% 63.77/63.72 cnf(9641,plain,
% 63.77/63.72 (P3(f3(f7(a4,a4),f7(a4,a4)),f7(a4,a4),f3(a4,a4))),
% 63.77/63.72 inference(scs_inference,[],[9483,9587,9595,9491,9607,9443,9109,9314,9166,9256,9515,9017,21,22,7252,8714,6629,5998,8195,24,27])).
% 63.77/63.72 cnf(9649,plain,
% 63.77/63.72 (~P2(f7(a4,a4),f5(a4),a4)),
% 63.77/63.72 inference(scs_inference,[],[9483,9587,9595,9491,9196,9607,9615,9443,9019,9130,9109,9054,9074,9314,9166,8962,9256,9515,9222,9017,3671,1888,21,22,7252,8714,6629,5998,8195,24,27,25,28,29,3639])).
% 63.77/63.72 cnf(9651,plain,
% 63.77/63.72 (~P2(f7(a4,a4),f5(a4),a2)),
% 63.77/63.72 inference(scs_inference,[],[9483,9587,9595,9491,9196,9607,9615,9443,9019,9130,9109,9054,9074,9314,9166,8962,9256,9515,9222,9017,3671,1888,21,22,7252,8714,6629,5998,8195,24,27,25,28,29,3639,3633])).
% 63.77/63.72 cnf(9658,plain,
% 63.77/63.72 (P3(f7(a4,a4),f3(f7(a4,a4),f7(a4,a4)),f3(a4,a4))),
% 63.77/63.72 inference(scs_inference,[],[9641,22])).
% 63.77/63.72 cnf(9660,plain,
% 63.77/63.72 (P2(f7(a4,a4),f5(f7(a4,a4)),a1)),
% 63.77/63.72 inference(scs_inference,[],[9641,9421,22,21])).
% 63.77/63.72 cnf(9664,plain,
% 63.77/63.72 (~P2(f5(a2),a2,f5(a2))),
% 63.77/63.72 inference(scs_inference,[],[9613,9641,9421,9115,9015,8989,22,21,8195,24])).
% 63.77/63.72 cnf(9666,plain,
% 63.77/63.72 (P3(f3(a4,a4),f7(f6(a4),f6(a4)),f3(a4,a4))),
% 63.77/63.72 inference(scs_inference,[],[9613,9641,9421,9535,9115,9015,9607,8989,22,21,8195,24,27])).
% 63.77/63.72 cnf(9668,plain,
% 63.77/63.72 (P2(f7(a4,a4),f5(a4),f3(a1,a1))),
% 63.77/63.72 inference(scs_inference,[],[9613,9597,9625,9641,9421,9535,9465,9115,9015,9607,8989,22,21,8195,24,27,25])).
% 63.77/63.72 cnf(9670,plain,
% 63.77/63.72 (~P3(f3(a4,a4),a4,a4)),
% 63.77/63.72 inference(scs_inference,[],[9613,9597,9625,9641,9421,9535,9206,9188,9465,9115,9015,9607,9387,8989,22,21,8195,24,27,25,28])).
% 63.77/63.72 cnf(9672,plain,
% 63.77/63.72 (P3(f3(a4,a4),f6(a2),f3(f6(a2),f6(a2)))),
% 63.77/63.72 inference(scs_inference,[],[9613,9597,9625,9641,9421,9107,9535,9206,9188,9465,9097,9115,9015,9607,9387,8989,22,21,8195,24,27,25,28,29])).
% 63.77/63.72 cnf(9680,plain,
% 63.77/63.72 (P2(f5(a4),f7(a4,a4),f3(a1,a1))),
% 63.77/63.72 inference(scs_inference,[],[9668,9666,22,21])).
% 63.77/63.72 cnf(9682,plain,
% 63.77/63.72 (~P2(f5(f7(a4,a4)),a4,f5(a4))),
% 63.77/63.72 inference(scs_inference,[],[9649,9668,9666,9660,9068,22,21,24])).
% 63.77/63.72 cnf(9684,plain,
% 63.77/63.72 (P2(a1,f3(f3(a1,a1),f3(a1,a1)),a1)),
% 63.77/63.72 inference(scs_inference,[],[9649,9668,9666,9513,9660,9252,9068,22,21,24,25])).
% 63.77/63.72 cnf(9688,plain,
% 63.77/63.72 (P3(f3(a1,a1),a4,f3(a1,a1))),
% 63.77/63.72 inference(scs_inference,[],[9649,9668,9666,9513,9660,9467,9483,9252,9068,9338,9208,3660,22,21,24,25,28,29])).
% 63.77/63.72 cnf(9698,plain,
% 63.77/63.72 (~P2(f3(a1,a1),a2,f3(a1,a1))),
% 63.77/63.72 inference(scs_inference,[],[9354,9585,9399,9306,9109,22,21,24])).
% 63.77/63.72 cnf(9700,plain,
% 63.77/63.72 (P2(f3(a4,a4),f3(f3(a1,a1),f3(a1,a1)),f3(a4,a4))),
% 63.77/63.72 inference(scs_inference,[],[9533,9354,9585,9399,9684,9306,9109,22,21,24,25])).
% 63.77/63.72 cnf(9706,plain,
% 63.77/63.72 (~P3(f6(f6(a2)),f6(a2),a4)),
% 63.77/63.72 inference(scs_inference,[],[9539,9533,9354,9585,9399,9684,9306,9316,9109,9334,9166,9607,9037,8960,22,21,24,25,29,8199,6279])).
% 63.77/63.72 cnf(9716,plain,
% 63.77/63.72 (P2(a1,f6(a2),a1)),
% 63.77/63.72 inference(scs_inference,[],[9700,9706,9455,8956,22,21,19])).
% 63.77/63.72 cnf(9730,plain,
% 63.77/63.72 (P2(f6(a2),a1,a1)),
% 63.77/63.72 inference(scs_inference,[],[9716,21])).
% 63.77/63.72 cnf(9736,plain,
% 63.77/63.72 (P2(f3(a4,a4),f6(a2),f3(a4,a4))),
% 63.77/63.72 inference(scs_inference,[],[5,9716,9672,9533,21,22,24,25])).
% 63.77/63.72 cnf(9738,plain,
% 63.77/63.72 (~P3(a1,a4,f5(a2))),
% 63.77/63.72 inference(scs_inference,[],[5,9716,9664,9672,9533,8942,9208,3671,21,22,24,25,28])).
% 63.77/63.72 cnf(9740,plain,
% 63.77/63.72 (P3(f3(a4,a4),f6(a4),f3(f6(a4),f6(a4)))),
% 63.77/63.72 inference(scs_inference,[],[5,9716,9664,9672,9533,9182,9132,8942,9387,9208,3671,21,22,24,25,28,29])).
% 63.77/63.72 cnf(9752,plain,
% 63.77/63.72 (P2(f3(a4,a4),f3(f6(a2),f6(a2)),f3(a4,a4))),
% 63.77/63.72 inference(scs_inference,[],[9736,9740,9107,22,21,24])).
% 63.77/63.72 cnf(9754,plain,
% 63.77/63.72 (P2(f3(f6(a2),f6(a2)),a1,a1)),
% 63.77/63.72 inference(scs_inference,[],[9736,9730,9740,9107,22,21,24,25])).
% 63.77/63.72 cnf(9758,plain,
% 63.77/63.72 (~P2(f6(a2),a1,a2)),
% 63.77/63.72 inference(scs_inference,[],[9736,9730,9611,9740,9517,9445,9107,9688,9451,9346,22,21,24,25,28,29])).
% 63.77/63.72 cnf(9766,plain,
% 63.77/63.72 (P3(f3(a2,a2),f6(f6(a4)),f3(a2,a2))),
% 63.77/63.72 inference(scs_inference,[],[9752,9117,21,22])).
% 63.77/63.72 cnf(9770,plain,
% 63.77/63.72 (P2(f3(a1,a1),f5(f7(a4,a4)),f5(a4))),
% 63.77/63.72 inference(scs_inference,[],[5,9752,9754,9680,9117,9660,9134,3631,21,22,24,25])).
% 63.77/63.72 cnf(9772,plain,
% 63.77/63.72 (~P2(f3(a4,a4),f3(a1,a1),a4)),
% 63.77/63.72 inference(scs_inference,[],[5,9670,9752,9754,9573,9680,9117,9660,9688,9535,9134,3631,21,22,24,25,29])).
% 63.77/63.72 cnf(9778,plain,
% 63.77/63.72 (P3(a2,f3(a2,a2),f3(f7(a2,a2),f7(a2,a2)))),
% 63.77/63.72 inference(scs_inference,[],[9080,22])).
% 63.77/63.72 cnf(9780,plain,
% 63.77/63.72 (P2(f5(f7(a4,a4)),f3(a1,a1),f5(a4))),
% 63.77/63.72 inference(scs_inference,[],[9770,9080,22,21])).
% 63.77/63.72 cnf(9782,plain,
% 63.77/63.72 (P2(f3(a1,a1),f5(a4),f5(a4))),
% 63.77/63.72 inference(scs_inference,[],[9770,9080,9517,22,21,24])).
% 63.77/63.72 cnf(9784,plain,
% 63.77/63.72 (P2(a1,f3(f6(a2),f6(a2)),a1)),
% 63.77/63.72 inference(scs_inference,[],[9770,9523,9752,9080,9517,22,21,24,25])).
% 63.77/63.72 cnf(9790,plain,
% 63.77/63.72 (P2(f5(a4),f3(a1,a1),f5(a4))),
% 63.77/63.72 inference(scs_inference,[],[9782,21])).
% 63.77/63.72 cnf(9792,plain,
% 63.77/63.72 (P3(f6(a2),f3(f7(a2,a2),f7(a2,a2)),f3(a2,a2))),
% 63.77/63.72 inference(scs_inference,[],[9782,9154,21,22])).
% 63.77/63.72 cnf(9796,plain,
% 63.77/63.72 (P2(f3(f3(a1,a1),f3(a1,a1)),f5(a4),f5(a4))),
% 63.77/63.72 inference(scs_inference,[],[9698,9782,9680,9326,9154,21,22,24,25])).
% 63.77/63.72 cnf(9802,plain,
% 63.77/63.72 (P3(f6(a2),a4,f6(a2))),
% 63.77/63.72 inference(scs_inference,[],[9097,22])).
% 63.77/63.72 cnf(9804,plain,
% 63.77/63.72 (P2(f5(a4),f3(f3(a1,a1),f3(a1,a1)),f5(a4))),
% 63.77/63.72 inference(scs_inference,[],[9796,9097,22,21])).
% 63.77/63.72 cnf(9815,plain,
% 63.77/63.72 (P2(f5(a4),f5(f5(a4)),a1)),
% 63.77/63.72 inference(scs_inference,[],[9463,21])).
% 63.77/63.72 cnf(9817,plain,
% 63.77/63.72 (P3(f6(a4),a4,f6(a4))),
% 63.77/63.72 inference(scs_inference,[],[9463,9132,21,22])).
% 63.77/63.72 cnf(9819,plain,
% 63.77/63.72 (P2(f6(a2),f6(a2),a1)),
% 63.77/63.72 inference(scs_inference,[],[9463,9210,9754,9132,9107,21,22,24])).
% 63.77/63.72 cnf(9821,plain,
% 63.77/63.72 (P2(f7(a4,a4),f3(f6(a2),f6(a2)),f7(a4,a4))),
% 63.77/63.72 inference(scs_inference,[],[9784,9463,9501,9210,9754,9132,9107,21,22,24,25])).
% 63.77/63.72 cnf(9823,plain,
% 63.77/63.72 (~P2(f6(a2),f6(a2),f5(a2))),
% 63.77/63.72 inference(scs_inference,[],[9802,9738,9784,9463,9501,9210,9754,9132,9107,21,22,24,25,29])).
% 63.77/63.72 cnf(9836,plain,
% 63.77/63.72 (P2(f3(f6(a2),f6(a2)),f7(a4,a4),f7(a4,a4))),
% 63.77/63.72 inference(scs_inference,[],[9821,9346,22,21])).
% 63.77/63.72 cnf(9838,plain,
% 63.77/63.72 (~P2(f6(a2),f5(a2),f6(a2))),
% 63.77/63.72 inference(scs_inference,[],[9823,9819,9821,8985,9346,22,21,24])).
% 63.77/63.72 cnf(9842,plain,
% 63.77/63.72 (~P3(f6(a4),a4,a1)),
% 63.77/63.72 inference(scs_inference,[],[9817,9823,9819,9821,9162,9294,8985,9041,9128,9346,1888,22,21,24,25,28])).
% 63.77/63.72 cnf(9844,plain,
% 63.77/63.72 (P3(f3(a4,a4),f7(a2,a2),f3(f7(a2,a2),f7(a2,a2)))),
% 63.80/63.72 inference(scs_inference,[],[9817,9823,9819,9821,9064,9162,9294,9052,8985,9041,9128,9346,9387,1888,22,21,24,25,28,29])).
% 63.80/63.72 cnf(9853,plain,
% 63.80/63.72 (P2(f7(a2,a2),f5(f7(a2,a2)),a1)),
% 63.80/63.72 inference(scs_inference,[],[9048,21])).
% 63.80/63.72 cnf(9855,plain,
% 63.80/63.72 (P3(f7(a2,a2),f3(a4,a4),f3(f7(a2,a2),f7(a2,a2)))),
% 63.80/63.72 inference(scs_inference,[],[9844,9048,21,22])).
% 63.80/63.72 cnf(9859,plain,
% 63.80/63.72 (~P2(f3(f3(a1,a1),f3(a1,a1)),a1,a2)),
% 63.80/63.72 inference(scs_inference,[],[5,9844,9815,9048,9796,80,21,22,24,25])).
% 63.80/63.72 cnf(9863,plain,
% 63.80/63.72 (~P2(f6(a4),f3(a1,a1),a1)),
% 63.80/63.72 inference(scs_inference,[],[5,9842,9844,9815,9048,9796,9371,9023,9817,8991,9688,3671,80,1888,21,22,24,25,28,29])).
% 63.80/63.72 cnf(9871,plain,
% 63.80/63.72 (P2(a1,f3(f5(a1),f5(a1)),a1)),
% 63.80/63.72 inference(scs_inference,[],[9449,9037,22,21])).
% 63.80/63.72 cnf(9873,plain,
% 63.80/63.72 (~P2(f3(a1,a1),f3(a1,a1),f5(a2))),
% 63.80/63.72 inference(scs_inference,[],[9838,9449,9290,9037,22,21,24])).
% 63.80/63.72 cnf(9875,plain,
% 63.80/63.72 (P3(f7(a2,a2),f3(f6(a2),f6(a2)),f3(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9838,9855,9672,9449,9290,9154,9037,22,21,24,26])).
% 63.80/63.72 cnf(9877,plain,
% 63.80/63.72 (P2(f6(a4),f3(f6(a2),f6(a2)),f6(a4))),
% 63.80/63.72 inference(scs_inference,[],[9838,9855,9672,9449,9784,9290,9260,9154,9037,22,21,24,26,25])).
% 63.80/63.72 cnf(9887,plain,
% 63.80/63.72 (P2(f3(f6(a2),f6(a2)),f6(a4),f6(a4))),
% 63.80/63.72 inference(scs_inference,[],[9877,21])).
% 63.80/63.72 cnf(9889,plain,
% 63.80/63.72 (P3(f3(f6(a2),f6(a2)),f7(a2,a2),f3(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9875,9877,21,22])).
% 63.80/63.72 cnf(9893,plain,
% 63.80/63.72 (P2(f5(a1),f5(a1),a1)),
% 63.80/63.72 inference(scs_inference,[],[9875,9780,9877,9682,9871,9790,9234,402,21,22,24,25])).
% 63.80/63.72 cnf(9902,plain,
% 63.80/63.72 (P3(f6(a4),f6(f6(a4)),a4)),
% 63.80/63.72 inference(scs_inference,[],[9066,22])).
% 63.80/63.72 cnf(9904,plain,
% 63.80/63.72 (P2(f3(a1,a1),f7(a2,a2),f7(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9395,9066,22,21])).
% 63.80/63.72 cnf(9908,plain,
% 63.80/63.72 (~P2(f5(a1),f5(a1),a2)),
% 63.80/63.72 inference(scs_inference,[],[5,9893,9395,9334,9234,9066,22,21,6629,24])).
% 63.80/63.72 cnf(9910,plain,
% 63.80/63.72 (P3(f7(f6(a4),f6(a4)),f7(a2,a2),f7(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[5,9893,9395,9152,9334,9184,9234,9066,22,21,6629,24,27])).
% 63.80/63.72 cnf(9912,plain,
% 63.80/63.72 (P2(a1,f5(a1),a1)),
% 63.80/63.72 inference(scs_inference,[],[5,9893,9395,9152,9204,9334,9184,9234,9066,22,21,6629,24,27,25])).
% 63.80/63.72 cnf(9914,plain,
% 63.80/63.72 (P3(f3(a4,a4),f3(a2,a2),f3(f3(a2,a2),f3(a2,a2)))),
% 63.80/63.72 inference(scs_inference,[],[5,9893,9144,9395,9152,9204,8987,9334,9184,9234,9387,9066,22,21,6629,24,27,25,29])).
% 63.80/63.72 cnf(9924,plain,
% 63.80/63.72 (P2(f3(f3(a1,a1),f3(a1,a1)),f7(a1,a1),f7(a1,a1))),
% 63.80/63.72 inference(scs_inference,[],[9513,21])).
% 63.80/63.72 cnf(9930,plain,
% 63.80/63.72 (P2(f3(a1,a1),a1,a1)),
% 63.80/63.72 inference(scs_inference,[],[9904,9910,9853,9902,9513,9334,21,22,8714,24])).
% 63.80/63.72 cnf(9932,plain,
% 63.80/63.72 (P2(f7(a2,a2),f5(a1),f7(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9904,9912,9910,9853,9902,9170,9513,9334,21,22,8714,24,25])).
% 63.80/63.72 cnf(9934,plain,
% 63.80/63.72 (~P3(f3(a4,a4),f5(a1),a2)),
% 63.80/63.72 inference(scs_inference,[],[9904,9908,9912,9910,9853,9902,9170,9513,9369,9334,9387,21,22,8714,24,25,28])).
% 63.80/63.72 cnf(9936,plain,
% 63.80/63.72 (~P2(a1,f7(a1,a1),f6(a4))),
% 63.80/63.72 inference(scs_inference,[],[9904,9908,9912,9910,9631,9853,9902,9393,9170,9513,9250,9369,9334,9346,9387,21,22,8714,24,25,28,29])).
% 63.80/63.72 cnf(9948,plain,
% 63.80/63.72 (P2(f3(a1,a1),f5(a1),a1)),
% 63.80/63.72 inference(scs_inference,[],[9873,9932,9930,9914,9912,8985,9220,9234,22,21,24,25])).
% 63.80/63.72 cnf(9958,plain,
% 63.80/63.72 (P2(f5(a1),f3(a1,a1),a1)),
% 63.80/63.72 inference(scs_inference,[],[9948,21])).
% 63.80/63.72 cnf(9962,plain,
% 63.80/63.72 (P2(f3(f5(a4),f5(a4)),f7(a4,a4),f5(a4))),
% 63.80/63.72 inference(scs_inference,[],[9651,9948,9479,9790,9680,9660,9109,21,24,25])).
% 63.80/63.72 cnf(9964,plain,
% 63.80/63.72 (P2(f3(a2,a2),f7(a2,a2),f7(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9651,9948,9889,9887,9479,9790,9680,9660,9152,9109,21,24,25,28])).
% 63.80/63.72 cnf(9972,plain,
% 63.80/63.72 (P2(f7(a2,a2),f3(a2,a2),f7(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9964,21])).
% 63.80/63.72 cnf(9978,plain,
% 63.80/63.72 (P2(f5(a4),f3(f6(a2),f6(a2)),f5(a4))),
% 63.80/63.72 inference(scs_inference,[],[9964,9934,9958,9962,9300,9821,9455,9429,9234,21,24,26,25])).
% 63.80/63.72 cnf(9992,plain,
% 63.80/63.72 (~P2(f3(a2,a2),f3(a2,a2),a2)),
% 63.80/63.72 inference(scs_inference,[],[9972,9978,9150,21,24])).
% 63.80/63.72 cnf(9994,plain,
% 63.80/63.72 (~P3(f3(a2,a2),f6(a2),a4)),
% 63.80/63.72 inference(scs_inference,[],[9972,9978,9778,9192,9150,9154,21,24,26])).
% 63.80/63.72 cnf(9996,plain,
% 63.80/63.72 (P2(f3(f3(a2,a2),f3(a2,a2)),f7(a2,a2),f7(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9972,9978,9778,9964,9192,9144,9150,9154,21,24,26,25])).
% 63.80/63.72 cnf(10006,plain,
% 63.80/63.72 (P2(f7(a2,a2),f3(f3(a2,a2),f3(a2,a2)),f7(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9996,21])).
% 63.80/63.72 cnf(10012,plain,
% 63.80/63.72 (~P2(f3(f5(a1),f5(a1)),a4,a1)),
% 63.80/63.72 inference(scs_inference,[],[9863,9996,9228,9168,9421,9449,9068,9680,9902,1135,21,27,24,25])).
% 63.80/63.72 cnf(10016,plain,
% 63.80/63.72 (~P2(f7(a1,a1),a1,a4)),
% 63.80/63.72 inference(scs_inference,[],[9992,9863,9996,9637,9792,9228,9168,9421,9393,9449,9819,9316,9068,9680,9902,9346,1135,21,27,24,25,28,29])).
% 63.80/63.72 cnf(10022,plain,
% 63.80/63.72 (P2(f7(a4,a4),f3(f5(a4),f5(a4)),f5(a4))),
% 63.80/63.72 inference(scs_inference,[],[9962,21])).
% 63.80/63.72 cnf(10026,plain,
% 63.80/63.72 (P2(a1,f3(f3(a2,a2),f3(a2,a2)),a1)),
% 63.80/63.72 inference(scs_inference,[],[10006,9603,9962,9958,9048,9234,21,24,25])).
% 63.80/63.72 cnf(10030,plain,
% 63.80/63.72 (P3(f5(a2),f3(a4,a4),f3(f5(a2),f5(a2)))),
% 63.80/63.72 inference(scs_inference,[],[10006,9603,9962,9958,9048,9015,9234,9387,102,21,24,25,29,22])).
% 63.80/63.72 cnf(10039,plain,
% 63.80/63.72 (P2(f3(f3(a2,a2),f3(a2,a2)),a1,a1)),
% 63.80/63.72 inference(scs_inference,[],[10026,21])).
% 63.80/63.72 cnf(10043,plain,
% 63.80/63.72 (P2(f3(a2,a2),f3(a2,a2),a1)),
% 63.80/63.72 inference(scs_inference,[],[9936,10026,9144,9019,9128,21,24,25])).
% 63.80/63.72 cnf(10053,plain,
% 63.80/63.72 (P2(f3(a4,a4),f5(f3(a4,a4)),a1)),
% 63.80/63.72 inference(scs_inference,[],[9523,21])).
% 63.80/63.72 cnf(10061,plain,
% 63.80/63.72 (~P2(f3(a2,a2),f3(a2,a2),a4)),
% 63.80/63.72 inference(scs_inference,[],[10016,10043,9226,9836,10039,9651,9617,9523,9485,9877,9668,9101,9817,21,24,25,28,29])).
% 63.80/63.72 cnf(10067,plain,
% 63.80/63.72 (P2(f7(a1,a1),f5(f7(a1,a1)),a1)),
% 63.80/63.72 inference(scs_inference,[],[9252,21])).
% 63.80/63.72 cnf(10071,plain,
% 63.80/63.72 (~P2(f3(a2,a2),f7(f6(a4),f6(a4)),f3(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9300,10043,9252,9019,21,24,25])).
% 63.80/63.72 cnf(10075,plain,
% 63.80/63.72 (~P3(f3(f3(a2,a2),f3(a2,a2)),f6(a4),f6(a4))),
% 63.80/63.72 inference(scs_inference,[],[10061,9766,10039,9300,10043,9252,9260,9019,8219,9037,21,24,25,28,29])).
% 63.80/63.72 cnf(10084,plain,
% 63.80/63.72 (P2(f3(a1,a1),f6(a2),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[9290,21])).
% 63.80/63.72 cnf(10088,plain,
% 63.80/63.72 (~P2(f7(a1,a1),f5(f7(a1,a1)),a2)),
% 63.80/63.72 inference(scs_inference,[],[9924,10067,9859,9627,9290,9481,9525,21,26,24])).
% 63.80/63.72 cnf(10090,plain,
% 63.80/63.72 (P2(f7(a1,a1),f5(f7(a1,a1)),f3(a1,a1))),
% 63.80/63.72 inference(scs_inference,[],[9924,10067,9859,9627,9427,9465,9290,9481,9525,21,26,24,25])).
% 63.80/63.72 cnf(10092,plain,
% 63.80/63.72 (P3(f3(a4,a4),a4,f3(f7(a4,a4),f7(a4,a4)))),
% 63.80/63.72 inference(scs_inference,[],[9924,10067,9859,9627,9427,9465,9290,9481,9525,21,26,24,25,22])).
% 63.80/63.72 cnf(10098,plain,
% 63.80/63.72 (P2(f5(f7(a1,a1)),f7(a1,a1),f3(a1,a1))),
% 63.80/63.72 inference(scs_inference,[],[10090,21])).
% 63.80/63.72 cnf(10102,plain,
% 63.80/63.72 (~P2(f3(a2,a2),a1,a2)),
% 63.80/63.72 inference(scs_inference,[],[9609,10090,10092,10030,9342,8958,9109,21,27,24])).
% 63.80/63.72 cnf(10104,plain,
% 63.80/63.72 (~P2(f3(f3(a1,a1),f3(a1,a1)),f3(a1,a1),a2)),
% 63.80/63.72 inference(scs_inference,[],[9609,10090,10092,10088,10030,9924,9342,8958,9109,21,27,24,25])).
% 63.80/63.72 cnf(10114,plain,
% 63.80/63.72 (P2(f3(f3(a1,a1),f3(a1,a1)),a1,a1)),
% 63.80/63.72 inference(scs_inference,[],[9684,21])).
% 63.80/63.72 cnf(10116,plain,
% 63.80/63.72 (P3(f3(f7(a4,a4),f7(a4,a4)),a4,f3(a4,a4))),
% 63.80/63.72 inference(scs_inference,[],[9658,10092,9627,9684,21,27])).
% 63.80/63.72 cnf(10131,plain,
% 63.80/63.72 (P2(f3(a1,a1),f5(f3(a1,a1)),a1)),
% 63.80/63.72 inference(scs_inference,[],[9306,21])).
% 63.80/63.72 cnf(10135,plain,
% 63.80/63.72 (~P2(f6(a4),f5(f7(a1,a1)),a1)),
% 63.80/63.72 inference(scs_inference,[],[10098,10104,10114,9936,9371,9306,9109,21,24,25])).
% 63.80/63.72 cnf(10137,plain,
% 63.80/63.72 (P2(f7(a4,a4),f7(a4,a4),f3(a4,a4))),
% 63.80/63.72 inference(scs_inference,[],[10098,10104,10116,10114,9936,9441,9467,9371,9306,9109,21,24,25,28])).
% 63.80/63.72 cnf(10143,plain,
% 63.80/63.72 (P2(f3(a2,a2),f5(f3(a2,a2)),a1)),
% 63.80/63.72 inference(scs_inference,[],[9130,21])).
% 63.80/63.72 cnf(10147,plain,
% 63.80/63.72 (P2(f3(a4,a4),f3(f5(a4),f5(a4)),a1)),
% 63.80/63.72 inference(scs_inference,[],[10137,10102,10022,10114,9625,9130,9134,21,24,25])).
% 63.80/63.72 cnf(10162,plain,
% 63.80/63.72 (P2(f3(a4,a4),f5(a4),f7(a4,a4))),
% 63.80/63.72 inference(scs_inference,[],[10147,9962,9410,21,24])).
% 63.80/63.72 cnf(10164,plain,
% 63.80/63.72 (P2(f3(a4,a4),f3(f5(a1),f5(a1)),f3(a4,a4))),
% 63.80/63.72 inference(scs_inference,[],[10147,9962,9533,9871,9410,21,24,25])).
% 63.80/63.72 cnf(10174,plain,
% 63.80/63.72 (P2(f5(a4),f3(a4,a4),f7(a4,a4))),
% 63.80/63.72 inference(scs_inference,[],[10162,21])).
% 63.80/63.72 cnf(10176,plain,
% 63.80/63.72 (P3(f3(a2,a2),f7(a4,a4),f3(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[10162,9056,9481,21,26])).
% 63.80/63.72 cnf(10180,plain,
% 63.80/63.72 (P2(f3(a1,a1),f6(a2),a1)),
% 63.80/63.72 inference(scs_inference,[],[9772,10162,10084,9056,9308,9716,9481,9680,21,26,24,25])).
% 63.80/63.72 cnf(10182,plain,
% 63.80/63.72 (~P2(f3(a2,a2),f6(a4),f3(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9772,10162,10071,10084,9056,9099,9308,9716,9481,9680,9184,21,26,24,25,28])).
% 63.80/63.72 cnf(10184,plain,
% 63.80/63.72 (P3(f7(a4,a4),f3(a2,a2),f3(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[9772,10162,10071,10084,9056,9099,9308,9716,9481,9680,9184,21,26,24,25,28,22])).
% 63.80/63.72 cnf(10190,plain,
% 63.80/63.72 (P2(f6(a2),f3(a1,a1),a1)),
% 63.80/63.72 inference(scs_inference,[],[10180,21])).
% 63.80/63.72 cnf(10194,plain,
% 63.80/63.72 (P2(f7(a4,a4),f3(f5(a1),f5(a1)),f7(a4,a4))),
% 63.80/63.72 inference(scs_inference,[],[10174,10182,10180,10164,10143,9019,21,24,25])).
% 63.80/63.72 cnf(10196,plain,
% 63.80/63.72 (~P2(a1,f7(a1,a1),a4)),
% 63.80/63.72 inference(scs_inference,[],[9549,10174,10182,10180,10164,10143,9250,9019,9334,9037,21,24,25,29])).
% 63.80/63.72 cnf(10204,plain,
% 63.80/63.72 (P2(f3(f5(a1),f5(a1)),f7(a4,a4),f7(a4,a4))),
% 63.80/63.72 inference(scs_inference,[],[10194,21])).
% 63.80/63.72 cnf(10210,plain,
% 63.80/63.72 (P2(f7(a4,a4),f3(f3(a1,a1),f3(a1,a1)),f7(a4,a4))),
% 63.80/63.72 inference(scs_inference,[],[10194,10184,9804,10143,9443,10162,8958,30,21,27,24,25])).
% 63.80/63.72 cnf(10214,plain,
% 63.80/63.72 (P3(f3(a2,a2),f7(f7(a4,a4),f7(a4,a4)),f3(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[10194,10075,10184,9804,10143,9443,10162,9099,9144,8958,30,21,27,24,25,29,22])).
% 63.80/63.72 cnf(10224,plain,
% 63.80/63.72 (P2(a1,f3(a1,a1),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10190,9758,10210,9210,9819,9109,21,24,25])).
% 63.80/63.72 cnf(10232,plain,
% 63.80/63.72 (P2(f3(a1,a1),a1,f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10224,21])).
% 63.80/63.72 cnf(10236,plain,
% 63.80/63.72 (P2(f6(a2),f5(f3(a1,a1)),a1)),
% 63.80/63.72 inference(scs_inference,[],[9639,10224,10131,9660,9068,8962,21,24,25])).
% 63.80/63.72 cnf(10244,plain,
% 63.80/63.72 (P2(f5(f3(a1,a1)),f6(a2),a1)),
% 63.80/63.72 inference(scs_inference,[],[10236,21])).
% 63.80/63.72 cnf(10248,plain,
% 63.80/63.72 (P2(f5(f7(a1,a1)),f7(a1,a1),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10232,10236,9934,10098,10092,9316,9369,21,26,24])).
% 63.80/63.72 cnf(10250,plain,
% 63.80/63.72 (P2(f6(a2),f5(a1),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10232,10236,9934,10098,10092,9316,9912,9369,21,26,24,25])).
% 63.80/63.72 cnf(10260,plain,
% 63.80/63.72 (~P2(f5(f3(a1,a1)),f6(a2),a2)),
% 63.80/63.72 inference(scs_inference,[],[1,10232,10236,9934,10098,10092,9316,9523,9912,9369,3,21,26,24,25,1457,54,8,3700,66])).
% 63.80/63.72 cnf(10263,plain,
% 63.80/63.72 (P2(f5(a1),f6(a2),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10250,21])).
% 63.80/63.72 cnf(10267,plain,
% 63.80/63.72 (~P2(f6(a2),a2,f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10250,10260,10244,9228,9481,9109,21,26,24])).
% 63.80/63.72 cnf(10269,plain,
% 63.80/63.72 (P2(a1,f5(a1),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10250,10260,10244,9228,9730,9481,9109,9234,21,26,24,25])).
% 63.80/63.72 cnf(10273,plain,
% 63.80/63.72 (P3(f7(a4,a4),f7(a2,a2),f7(a2,a2))),
% 63.80/63.72 inference(scs_inference,[],[10250,10260,10244,9609,9792,9228,9730,9481,9109,9234,21,26,24,25,28,22])).
% 63.80/63.72 cnf(10278,plain,
% 63.80/63.72 (P2(f5(a1),a1,f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10269,21])).
% 63.80/63.72 cnf(10282,plain,
% 63.80/63.72 (P2(f6(a2),f6(a2),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10196,10263,10269,9095,9101,9068,21,24,25])).
% 63.80/63.72 cnf(10289,plain,
% 63.80/63.72 (P2(f7(a1,a1),f5(f7(a1,a1)),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10248,21])).
% 63.80/63.72 cnf(10293,plain,
% 63.80/63.72 (P2(f3(f5(a1),f5(a1)),f3(a4,a4),f3(a4,a4))),
% 63.80/63.72 inference(scs_inference,[],[10204,10248,10137,10273,9443,21,27,24])).
% 63.80/63.72 cnf(10295,plain,
% 63.80/63.72 (P2(f6(a2),f3(f5(a1),f5(a1)),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10278,10204,10248,10137,10273,9443,9871,21,27,24,25])).
% 63.80/63.72 cnf(10305,plain,
% 63.80/63.72 (P3(a2,f7(f6(a2),f6(a2)),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10278,10204,10248,9111,10176,10061,9631,10137,10273,9443,9871,9097,9393,9316,9144,8952,9346,8989,21,27,24,25,28,29,22,15,26])).
% 63.80/63.72 cnf(10309,plain,
% 63.80/63.72 (P3(f7(f6(a2),f6(a2)),a2,f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10305,10295,21,22])).
% 63.80/63.72 cnf(10317,plain,
% 63.80/63.72 (P3(f3(a2,a2),f7(f6(a2),f6(a2)),f6(a2))),
% 63.80/63.72 inference(scs_inference,[],[10267,10293,10305,10289,10295,10135,10282,10053,10244,10012,9258,8958,21,22,24,25,28,29])).
% 63.80/63.72 cnf(10338,plain,
% 63.80/63.72 ($false),
% 63.80/63.72 inference(scs_inference,[],[10317,10309,9994,10214,9162,8960,21,22,27,26]),
% 63.80/63.72 ['proof']).
% 63.80/63.72 % SZS output end Proof
% 63.80/63.72 % Total time :63.050000s
%------------------------------------------------------------------------------