%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD015-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n013.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:13 EDT 2024
% Result : Unsatisfiable 65.99s 66.24s
% Output : CNFRefutation 66.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : FLD015-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n013.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Jun 19 10:21:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.44/0.58 start to proof:theBenchmark
% 65.99/66.23 %-------------------------------------------
% 65.99/66.23 % File :CSE---1.7
% 65.99/66.23 % Problem :theBenchmark
% 65.99/66.23 % Transform :cnf
% 65.99/66.23 % Format :tptp:raw
% 65.99/66.23 % Command :java -jar mcs_scs.jar %d %s
% 65.99/66.23
% 65.99/66.23 % Result :Theorem 65.420000s
% 65.99/66.23 % Output :CNFRefutation 65.420000s
% 65.99/66.23 %-------------------------------------------
% 65.99/66.23 %--------------------------------------------------------------------------
% 65.99/66.23 % File : FLD015-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 65.99/66.23 % Domain : Field Theory (Ordered fields)
% 65.99/66.23 % Problem : Compatibility of additive inverses with the equality, part 2
% 65.99/66.23 % Version : [Dra93] axioms : Especial.
% 65.99/66.23 % Theorem formulation : Functional with re axiom set.
% 65.99/66.23 % English :
% 65.99/66.23
% 65.99/66.23 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 65.99/66.23 % Source : [Dra93]
% 65.99/66.23 % Names :
% 65.99/66.23
% 65.99/66.23 % Status : Unsatisfiable
% 65.99/66.23 % Rating : 0.00 v7.0.0, 0.12 v6.3.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.10 v5.2.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0, 0.00 v2.4.0, 0.00 v2.2.1, 0.33 v2.1.0
% 65.99/66.23 % Syntax : Number of clauses : 30 ( 7 unt; 3 nHn; 30 RR)
% 65.99/66.23 % Number of literals : 81 ( 0 equ; 50 neg)
% 65.99/66.23 % Maximal clause size : 5 ( 2 avg)
% 65.99/66.23 % Maximal term depth : 2 ( 1 avg)
% 65.99/66.23 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 65.99/66.23 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 65.99/66.24 % Number of variables : 73 ( 0 sgn)
% 65.99/66.24 % SPC : CNF_UNS_RFO_NEQ_NHN
% 65.99/66.24
% 65.99/66.24 % Comments :
% 65.99/66.24 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 65.99/66.24 %--------------------------------------------------------------------------
% 65.99/66.24 include('Axioms/FLD002-0.ax').
% 65.99/66.24 %--------------------------------------------------------------------------
% 65.99/66.24 cnf(a_is_defined,hypothesis,
% 65.99/66.24 defined(a) ).
% 65.99/66.24
% 65.99/66.24 cnf(b_is_defined,hypothesis,
% 65.99/66.24 defined(b) ).
% 65.99/66.24
% 65.99/66.24 cnf(sum_3,negated_conjecture,
% 65.99/66.24 sum(additive_identity,additive_inverse(a),additive_inverse(b)) ).
% 65.99/66.24
% 65.99/66.24 cnf(not_sum_4,negated_conjecture,
% 65.99/66.24 ~ sum(additive_identity,a,b) ).
% 65.99/66.24
% 65.99/66.24 %--------------------------------------------------------------------------
% 65.99/66.24 %-------------------------------------------
% 65.99/66.24 % Proof found
% 65.99/66.24 % SZS status Theorem for theBenchmark
% 65.99/66.24 % SZS output start Proof
% 65.99/66.24 %ClaNum:30(EqnAxiom:0)
% 65.99/66.24 %VarNum:162(SingletonVarNum:73)
% 65.99/66.24 %MaxLitNum:5
% 65.99/66.24 %MaxfuncDepth:1
% 65.99/66.24 %SharedTerms:13
% 65.99/66.24 %goalClause: 5 7
% 65.99/66.24 %singleGoalClaCount:2
% 65.99/66.24 [1]P1(a1)
% 65.99/66.24 [2]P1(a4)
% 65.99/66.24 [3]P1(a2)
% 65.99/66.24 [4]P1(a5)
% 65.99/66.24 [6]~P2(a1,a1,a4)
% 65.99/66.24 [7]~P2(a1,a2,a5)
% 65.99/66.24 [5]P2(a1,f6(a2),f6(a5))
% 65.99/66.24 [13]~P1(x131)+P2(a1,x131,x131)
% 65.99/66.24 [14]~P1(x141)+P4(a4,x141,x141)
% 65.99/66.24 [8]~P1(x81)+P1(f6(x81))
% 65.99/66.24 [15]~P1(x151)+P2(f6(x151),x151,a1)
% 65.99/66.24 [22]~P2(x222,x221,x223)+P2(x221,x222,x223)
% 65.99/66.24 [23]~P4(x232,x231,x233)+P4(x231,x232,x233)
% 65.99/66.24 [16]~P1(x161)+P2(a1,x161,a1)+P1(f8(x161))
% 65.99/66.24 [20]~P1(x201)+P4(f8(x201),x201,a4)+P2(a1,x201,a1)
% 65.99/66.24 [19]~P3(x192,x191)+~P3(x191,x192)+P2(a1,x191,x192)
% 65.99/66.24 [10]~P1(x102)+~P1(x101)+P1(f3(x101,x102))
% 65.99/66.24 [11]~P1(x112)+~P1(x111)+P1(f7(x111,x112))
% 65.99/66.24 [17]~P1(x172)+~P1(x171)+P2(x171,x172,f3(x171,x172))
% 65.99/66.24 [18]~P1(x182)+~P1(x181)+P4(x181,x182,f7(x181,x182))
% 65.99/66.24 [12]~P3(x121,x123)+P3(x121,x122)+~P3(x123,x122)
% 65.99/66.24 [9]P3(x92,x91)+~P1(x91)+~P1(x92)+P3(x91,x92)
% 65.99/66.24 [21]~P4(x213,x212,x211)+P3(a1,x211)+~P3(a1,x212)+~P3(a1,x213)
% 65.99/66.24 [24]~P2(x243,x245,x241)+P3(x241,x242)+~P2(x244,x245,x242)+~P3(x243,x244)
% 65.99/66.24 [25]~P2(x251,x256,x254)+P2(x251,x252,x253)+~P2(x254,x255,x253)+~P2(x256,x255,x252)
% 65.99/66.24 [26]~P2(x266,x264,x261)+P2(x261,x262,x263)+~P2(x264,x262,x265)+~P2(x266,x265,x263)
% 65.99/66.24 [27]~P4(x271,x276,x274)+P4(x271,x272,x273)+~P4(x274,x275,x273)+~P4(x276,x275,x272)
% 65.99/66.24 [28]~P4(x286,x284,x281)+P4(x281,x282,x283)+~P4(x284,x282,x285)+~P4(x286,x285,x283)
% 65.99/66.24 [29]~P4(x295,x297,x292)+~P4(x294,x297,x291)+P2(x291,x292,x293)+~P2(x294,x295,x296)+~P4(x296,x297,x293)
% 65.99/66.24 [30]~P4(x307,x302,x305)+~P4(x306,x302,x304)+P4(x301,x302,x303)+~P2(x304,x305,x303)+~P2(x306,x307,x301)
% 65.99/66.24 %EqnAxiom
% 65.99/66.24
% 65.99/66.24 %-------------------------------------------
% 65.99/66.25 cnf(31,plain,
% 65.99/66.25 (~P2(a2,a1,a5)),
% 65.99/66.25 inference(scs_inference,[],[7,22])).
% 65.99/66.25 cnf(33,plain,
% 65.99/66.25 (P3(a1,a1)),
% 65.99/66.25 inference(scs_inference,[],[7,1,22,9])).
% 65.99/66.25 cnf(41,plain,
% 65.99/66.25 (P2(f6(a5),x411,f6(a5))+~P2(f6(a2),x411,f6(a2))),
% 65.99/66.25 inference(scs_inference,[],[5,7,1,22,9,19,24,25,26])).
% 65.99/66.25 cnf(44,plain,
% 65.99/66.25 (P3(a4,a4)),
% 65.99/66.25 inference(scs_inference,[],[2,9])).
% 65.99/66.25 cnf(54,plain,
% 65.99/66.25 (P3(a5,a5)),
% 65.99/66.25 inference(scs_inference,[],[4,9])).
% 65.99/66.25 cnf(164,plain,
% 65.99/66.25 (P2(f6(f6(a4)),f6(a4),a1)),
% 65.99/66.25 inference(scs_inference,[],[2,15,8])).
% 65.99/66.25 cnf(170,plain,
% 65.99/66.25 (P2(a1,x1701,a1)+~P2(f6(a4),x1701,f6(a4))),
% 65.99/66.25 inference(scs_inference,[],[164,26])).
% 65.99/66.25 cnf(268,plain,
% 65.99/66.25 (~P2(x2681,f6(a4),f6(a4))+P2(a1,x2681,a1)),
% 65.99/66.25 inference(scs_inference,[],[170,22])).
% 65.99/66.25 cnf(284,plain,
% 65.99/66.25 (~P1(f6(a4))+P2(a1,a1,a1)),
% 65.99/66.25 inference(scs_inference,[],[268,13])).
% 65.99/66.25 cnf(348,plain,
% 65.99/66.25 (~P2(x3481,f6(a2),f6(a2))+P2(f6(a5),x3481,f6(a5))),
% 65.99/66.25 inference(scs_inference,[],[41,22])).
% 65.99/66.25 cnf(396,plain,
% 65.99/66.25 (P2(x3961,f6(a5),f6(a5))+~P2(x3961,f6(a2),f6(a2))),
% 65.99/66.25 inference(scs_inference,[],[348,22])).
% 65.99/66.25 cnf(444,plain,
% 65.99/66.25 (~P1(f6(a2))+P2(a1,f6(a5),f6(a5))),
% 65.99/66.25 inference(scs_inference,[],[396,13])).
% 65.99/66.25 cnf(460,plain,
% 65.99/66.25 (P2(f6(a5),a1,f6(a5))+~P1(f6(a2))),
% 65.99/66.25 inference(scs_inference,[],[444,22])).
% 65.99/66.25 cnf(476,plain,
% 65.99/66.25 (P2(f6(a5),x4761,f6(a5))+~P2(a1,x4761,a1)+~P1(f6(a2))),
% 65.99/66.25 inference(scs_inference,[],[460,26])).
% 65.99/66.25 cnf(713,plain,
% 65.99/66.25 (P2(x7131,f6(a5),f6(a5))+~P1(f6(a2))+~P2(a1,x7131,a1)),
% 65.99/66.25 inference(scs_inference,[],[476,22])).
% 65.99/66.25 cnf(729,plain,
% 65.99/66.25 (P2(x7291,f6(a5),f6(a5))+~P2(a1,x7291,a1)),
% 65.99/66.25 inference(scs_inference,[],[3,713,8])).
% 65.99/66.25 cnf(1703,plain,
% 65.99/66.25 (P2(a1,a1,a1)),
% 65.99/66.25 inference(scs_inference,[],[2,8,284])).
% 65.99/66.25 cnf(1704,plain,
% 65.99/66.25 (P2(a1,f6(a5),f6(a5))),
% 65.99/66.25 inference(scs_inference,[],[1703,729])).
% 65.99/66.25 cnf(2020,plain,
% 65.99/66.25 (P2(a1,f6(a4),f6(a4))),
% 65.99/66.25 inference(scs_inference,[],[2,8,13])).
% 65.99/66.25 cnf(2194,plain,
% 65.99/66.25 (P4(a4,f6(a4),f6(a4))),
% 65.99/66.25 inference(scs_inference,[],[2,8,14])).
% 65.99/66.25 cnf(3594,plain,
% 65.99/66.25 (P2(f6(a2),a1,f6(a5))),
% 65.99/66.25 inference(scs_inference,[],[5,22])).
% 65.99/66.25 cnf(3597,plain,
% 65.99/66.25 (P2(f6(a4),a1,f6(a4))),
% 65.99/66.25 inference(scs_inference,[],[2020,22])).
% 65.99/66.25 cnf(3628,plain,
% 65.99/66.25 (~P2(f6(a2),x36281,a1)+~P2(f6(a5),x36281,a4)),
% 65.99/66.25 inference(scs_inference,[],[5,6,25])).
% 65.99/66.25 cnf(3639,plain,
% 65.99/66.25 (~P2(x36391,a1,a5)+~P2(x36391,a1,a2)),
% 65.99/66.25 inference(scs_inference,[],[31,1703,26])).
% 65.99/66.25 cnf(3655,plain,
% 65.99/66.25 (~P2(a1,x36551,a2)+~P2(x36551,a1,a5)),
% 65.99/66.25 inference(scs_inference,[],[3639,22])).
% 65.99/66.25 cnf(3671,plain,
% 65.99/66.25 (~P2(a1,x36711,a5)+~P2(a1,x36711,a2)),
% 65.99/66.25 inference(scs_inference,[],[3655,22])).
% 65.99/66.25 cnf(3675,plain,
% 65.99/66.25 (P4(f6(a4),a4,f6(a4))),
% 65.99/66.25 inference(scs_inference,[],[2194,23])).
% 65.99/66.25 cnf(10236,plain,
% 65.99/66.25 (P1(f6(a1))),
% 65.99/66.25 inference(scs_inference,[],[1,8])).
% 65.99/66.25 cnf(10238,plain,
% 65.99/66.25 (P4(a4,a1,a1)),
% 65.99/66.25 inference(scs_inference,[],[1,8,14])).
% 65.99/66.25 cnf(10240,plain,
% 65.99/66.25 (P2(f6(a1),a1,a1)),
% 65.99/66.25 inference(scs_inference,[],[1,8,14,15])).
% 65.99/66.25 cnf(10242,plain,
% 65.99/66.25 (P2(a1,f6(a1),a1)),
% 65.99/66.25 inference(scs_inference,[],[1,8,14,15,22])).
% 65.99/66.25 cnf(10244,plain,
% 65.99/66.25 (P4(a1,a4,a1)),
% 65.99/66.25 inference(scs_inference,[],[1,8,14,15,22,23])).
% 65.99/66.25 cnf(10246,plain,
% 65.99/66.25 (P2(a1,a2,a2)),
% 65.99/66.25 inference(scs_inference,[],[1,3,8,14,15,22,23,13])).
% 65.99/66.25 cnf(10248,plain,
% 65.99/66.25 (P1(f3(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[1,3,8,14,15,22,23,13,10])).
% 65.99/66.25 cnf(10250,plain,
% 65.99/66.25 (P1(f7(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[1,3,8,14,15,22,23,13,10,11])).
% 65.99/66.25 cnf(10252,plain,
% 65.99/66.25 (P4(a1,a1,f7(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[1,3,8,14,15,22,23,13,10,11,18])).
% 65.99/66.25 cnf(10254,plain,
% 65.99/66.25 (P2(a1,a1,f3(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[1,3,8,14,15,22,23,13,10,11,18,17])).
% 65.99/66.25 cnf(10256,plain,
% 65.99/66.25 (P2(a1,a5,a5)),
% 65.99/66.25 inference(scs_inference,[],[1,3,54,8,14,15,22,23,13,10,11,18,17,19])).
% 65.99/66.25 cnf(10260,plain,
% 65.99/66.25 (P2(a1,f3(a1,a1),f3(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[33,1,3,54,1703,8,14,15,22,23,13,10,11,18,17,19,21,25])).
% 65.99/66.25 cnf(10262,plain,
% 65.99/66.25 (P2(f3(a1,a1),a1,f3(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[33,1,3,54,1703,8,14,15,22,23,13,10,11,18,17,19,21,25,26])).
% 65.99/66.25 cnf(10264,plain,
% 65.99/66.25 (P4(f7(a1,a1),a4,f7(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[33,1,3,54,1703,8,14,15,22,23,13,10,11,18,17,19,21,25,26,28])).
% 65.99/66.25 cnf(10268,plain,
% 65.99/66.25 (P2(f7(a1,a1),f7(a1,a1),f7(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[33,1,3,54,1703,8,14,15,22,23,13,10,11,18,17,19,21,25,26,28,24,29])).
% 65.99/66.25 cnf(10270,plain,
% 65.99/66.25 (~P2(a1,a5,a2)),
% 65.99/66.25 inference(scs_inference,[],[33,1,3,54,1703,8,14,15,22,23,13,10,11,18,17,19,21,25,26,28,24,29,3671])).
% 65.99/66.25 cnf(10274,plain,
% 65.99/66.25 (P4(a4,f7(a1,a1),f7(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[33,1,3,54,1703,8,14,15,22,23,13,10,11,18,17,19,21,25,26,28,24,29,3671,16,27])).
% 65.99/66.25 cnf(10286,plain,
% 65.99/66.25 (P2(f6(a5),a5,a1)),
% 65.99/66.25 inference(scs_inference,[],[4,15])).
% 65.99/66.25 cnf(10288,plain,
% 65.99/66.25 (P4(a4,f3(a1,a1),f3(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[10248,4,15,14])).
% 65.99/66.25 cnf(10290,plain,
% 65.99/66.25 (P1(f6(a5))),
% 65.99/66.25 inference(scs_inference,[],[10248,4,15,14,8])).
% 65.99/66.25 cnf(10292,plain,
% 65.99/66.25 (P2(a2,a1,a2)),
% 65.99/66.25 inference(scs_inference,[],[10246,10248,4,15,14,8,22])).
% 65.99/66.25 cnf(10294,plain,
% 65.99/66.25 (P4(f3(a1,a1),a4,f3(a1,a1))),
% 65.99/66.25 inference(scs_inference,[],[10246,10248,4,15,14,8,22,23])).
% 65.99/66.25 cnf(10296,plain,
% 65.99/66.25 (P2(a1,f6(a1),f6(a1))),
% 65.99/66.25 inference(scs_inference,[],[10246,10248,10236,4,15,14,8,22,23,13])).
% 65.99/66.25 cnf(10300,plain,
% 65.99/66.25 (P1(f3(a5,a5))),
% 65.99/66.25 inference(scs_inference,[],[10246,10248,10236,4,15,14,8,22,23,13,18,10])).
% 65.99/66.25 cnf(10302,plain,
% 65.99/66.25 (P1(f7(a5,a5))),
% 65.99/66.25 inference(scs_inference,[],[10246,10248,10236,4,15,14,8,22,23,13,18,10,11])).
% 65.99/66.25 cnf(10304,plain,
% 65.99/66.25 (P2(a5,a5,f3(a5,a5))),
% 65.99/66.25 inference(scs_inference,[],[10246,10248,10236,4,15,14,8,22,23,13,18,10,11,17])).
% 65.99/66.25 cnf(10306,plain,
% 65.99/66.25 (P2(a1,a4,a4)),
% 65.99/66.25 inference(scs_inference,[],[10246,10248,10236,4,44,15,14,8,22,23,13,18,10,11,17,19])).
% 65.99/66.25 cnf(10308,plain,
% 65.99/66.25 (P2(f6(a1),f6(a5),f6(a5))),
% 65.99/66.26 inference(scs_inference,[],[5,10246,10248,10236,10240,4,44,15,14,8,22,23,13,18,10,11,17,19,25])).
% 65.99/66.26 cnf(10310,plain,
% 65.99/66.26 (P2(f3(a1,a1),f6(a2),f6(a5))),
% 65.99/66.26 inference(scs_inference,[],[5,10246,10248,10236,10254,10240,4,44,1704,15,14,8,22,23,13,18,10,11,17,19,25,26])).
% 65.99/66.26 cnf(10316,plain,
% 65.99/66.26 (P4(f3(a1,a1),a1,f7(a1,a1))),
% 65.99/66.26 inference(scs_inference,[],[5,10246,10268,10248,10236,10254,10252,10240,33,4,44,1704,15,14,8,22,23,13,18,10,11,17,19,25,26,24,20,30])).
% 65.99/66.26 cnf(10321,plain,
% 65.99/66.26 (P1(f6(a2))),
% 65.99/66.26 inference(scs_inference,[],[3,8])).
% 65.99/66.26 cnf(10323,plain,
% 65.99/66.26 (P2(f6(a2),a2,a1)),
% 65.99/66.26 inference(scs_inference,[],[3,8,15])).
% 65.99/66.26 cnf(10325,plain,
% 65.99/66.26 (P4(a4,f7(a5,a5),f7(a5,a5))),
% 65.99/66.26 inference(scs_inference,[],[10302,3,8,15,14])).
% 65.99/66.26 cnf(10327,plain,
% 65.99/66.26 (P2(a4,a1,a4)),
% 65.99/66.26 inference(scs_inference,[],[10306,10302,3,8,15,14,22])).
% 65.99/66.26 cnf(10329,plain,
% 65.99/66.26 (P4(a1,f3(a1,a1),f7(a1,a1))),
% 65.99/66.26 inference(scs_inference,[],[10306,10302,10316,3,8,15,14,22,23])).
% 65.99/66.26 cnf(10331,plain,
% 65.99/66.26 (P2(a1,f7(a5,a5),f7(a5,a5))),
% 65.99/66.26 inference(scs_inference,[],[10306,10302,10316,3,8,15,14,22,23,13])).
% 65.99/66.26 cnf(10333,plain,
% 65.99/66.26 (P4(a2,a2,f7(a2,a2))),
% 65.99/66.26 inference(scs_inference,[],[10306,10302,10316,3,8,15,14,22,23,13,18])).
% 65.99/66.26 cnf(10335,plain,
% 65.99/66.26 (P1(f7(a2,a2))),
% 65.99/66.26 inference(scs_inference,[],[10306,10302,10316,3,8,15,14,22,23,13,18,11])).
% 65.99/66.26 cnf(10337,plain,
% 65.99/66.26 (P1(f3(a2,a2))),
% 65.99/66.26 inference(scs_inference,[],[10306,10302,10316,3,8,15,14,22,23,13,18,11,10])).
% 65.99/66.26 cnf(10339,plain,
% 65.99/66.26 (P2(a2,a2,f3(a2,a2))),
% 65.99/66.26 inference(scs_inference,[],[10306,10302,10316,3,8,15,14,22,23,13,18,11,10,17])).
% 65.99/66.26 cnf(10341,plain,
% 65.99/66.26 (P2(f6(a1),a4,a4)),
% 65.99/66.26 inference(scs_inference,[],[10306,10302,10316,10240,3,8,15,14,22,23,13,18,11,10,17,25])).
% 65.99/66.26 cnf(10343,plain,
% 65.99/66.26 (P2(a2,f6(a1),a2)),
% 65.99/66.26 inference(scs_inference,[],[10292,10306,10302,10242,10316,10240,3,8,15,14,22,23,13,18,11,10,17,25,26])).
% 65.99/66.26 cnf(10345,plain,
% 65.99/66.26 (P2(f7(a1,a1),f3(a1,a1),f3(a1,a1))),
% 65.99/66.26 inference(scs_inference,[],[10292,10306,10288,10302,10242,10316,10240,3,8,15,14,22,23,13,18,11,10,17,25,26,29])).
% 65.99/66.26 cnf(10347,plain,
% 65.99/66.26 (~P2(f6(a5),a2,a4)),
% 65.99/66.26 inference(scs_inference,[],[10292,10306,10288,10302,10242,10316,10240,3,8,15,14,22,23,13,18,11,10,17,25,26,29,3628])).
% 65.99/66.26 cnf(10356,plain,
% 65.99/66.26 (P4(a4,f7(a2,a2),f7(a2,a2))),
% 65.99/66.26 inference(scs_inference,[],[10335,14])).
% 65.99/66.26 cnf(10358,plain,
% 65.99/66.26 (P2(f6(a4),a4,a1)),
% 65.99/66.26 inference(scs_inference,[],[10335,2,14,15])).
% 65.99/66.26 cnf(10362,plain,
% 65.99/66.26 (P2(a1,f7(a2,a2),f7(a2,a2))),
% 65.99/66.26 inference(scs_inference,[],[10335,2,14,15,8,13])).
% 65.99/66.26 cnf(10364,plain,
% 65.99/66.26 (P2(f3(a1,a1),f7(a1,a1),f3(a1,a1))),
% 65.99/66.26 inference(scs_inference,[],[10345,10335,2,14,15,8,13,22])).
% 65.99/66.26 cnf(10366,plain,
% 65.99/66.26 (P4(f7(a5,a5),a4,f7(a5,a5))),
% 66.10/66.26 inference(scs_inference,[],[10345,10335,10325,2,14,15,8,13,22,23])).
% 66.10/66.26 cnf(10368,plain,
% 66.10/66.26 (P4(a4,a4,f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10345,10335,10325,2,14,15,8,13,22,23,18])).
% 66.10/66.26 cnf(10370,plain,
% 66.10/66.26 (P1(f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10345,10335,10325,2,14,15,8,13,22,23,18,10])).
% 66.10/66.26 cnf(10372,plain,
% 66.10/66.26 (P1(f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10345,10335,10325,2,14,15,8,13,22,23,18,10,11])).
% 66.10/66.26 cnf(10374,plain,
% 66.10/66.26 (P2(a4,a4,f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10345,10335,10325,2,14,15,8,13,22,23,18,10,11,17])).
% 66.10/66.26 cnf(10376,plain,
% 66.10/66.26 (P4(f3(a1,a1),f7(a4,a4),f3(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10294,10345,10335,10325,2,14,15,8,13,22,23,18,10,11,17,27])).
% 66.10/66.26 cnf(10378,plain,
% 66.10/66.26 (P2(f6(a1),f3(a1,a1),f3(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10294,10345,10260,10335,10325,10240,2,14,15,8,13,22,23,18,10,11,17,27,25])).
% 66.10/66.26 cnf(10380,plain,
% 66.10/66.26 (~P2(f6(a1),a4,a1)),
% 66.10/66.26 inference(scs_inference,[],[10327,10294,10345,10260,10335,10325,10341,10240,2,6,14,15,8,13,22,23,18,10,11,17,27,25,26])).
% 66.10/66.26 cnf(10384,plain,
% 66.10/66.26 (P4(f3(a1,a1),f3(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10327,10294,10345,10260,10329,10335,10325,10331,10341,10268,10254,10240,33,2,6,14,15,8,13,22,23,18,10,11,17,27,25,26,24,30])).
% 66.10/66.26 cnf(10391,plain,
% 66.10/66.26 (P4(a4,f3(a4,a4),f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10370,14])).
% 66.10/66.26 cnf(10393,plain,
% 66.10/66.26 (P4(f7(a4,a4),f3(a1,a1),f3(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10376,10370,14,23])).
% 66.10/66.26 cnf(10395,plain,
% 66.10/66.26 (P2(f6(a5),f6(a1),f6(a5))),
% 66.10/66.26 inference(scs_inference,[],[10308,10376,10370,14,23,22])).
% 66.10/66.26 cnf(10397,plain,
% 66.10/66.26 (P2(a1,f3(a4,a4),f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10308,10376,10370,14,23,22,13])).
% 66.10/66.26 cnf(10399,plain,
% 66.10/66.26 (~P2(f3(a1,a1),a5,a2)),
% 66.10/66.26 inference(scs_inference,[],[10270,10308,10376,10370,10256,10254,14,23,22,13,25])).
% 66.10/66.26 cnf(10401,plain,
% 66.10/66.26 (P2(f3(a1,a1),f6(a1),f6(a1))),
% 66.10/66.26 inference(scs_inference,[],[10270,10308,10376,10370,10296,10256,10254,14,23,22,13,25,26])).
% 66.10/66.26 cnf(10403,plain,
% 66.10/66.26 (P4(f7(a1,a1),f7(a4,a4),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10270,10384,10308,10376,10370,10296,10256,10254,14,23,22,13,25,26,28])).
% 66.10/66.26 cnf(10407,plain,
% 66.10/66.26 (P4(f3(a4,a4),a1,f3(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10270,10384,10308,10376,10370,10296,10362,10374,10238,10256,10254,33,14,23,22,13,25,26,28,24,30])).
% 66.10/66.26 cnf(10413,plain,
% 66.10/66.26 (P4(a4,f7(a4,a4),f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10372,14])).
% 66.10/66.26 cnf(10415,plain,
% 66.10/66.26 (P4(f7(a4,a4),f7(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10403,10372,14,23])).
% 66.10/66.26 cnf(10417,plain,
% 66.10/66.26 (P2(a4,f6(a4),a1)),
% 66.10/66.26 inference(scs_inference,[],[10403,10372,10358,14,23,22])).
% 66.10/66.26 cnf(10419,plain,
% 66.10/66.26 (P2(a1,f7(a4,a4),f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10403,10372,10358,14,23,22,13])).
% 66.10/66.26 cnf(10421,plain,
% 66.10/66.26 (~P2(f6(a1),f6(a4),f6(a1))),
% 66.10/66.26 inference(scs_inference,[],[10403,10372,10358,10380,10240,14,23,22,13,26])).
% 66.10/66.26 cnf(10423,plain,
% 66.10/66.26 (P2(a1,f3(a5,a5),f3(a5,a5))),
% 66.10/66.26 inference(scs_inference,[],[10403,10372,10358,10304,10380,10256,10240,14,23,22,13,26,25])).
% 66.10/66.26 cnf(10434,plain,
% 66.10/66.26 (P4(a4,f6(a5),f6(a5))),
% 66.10/66.26 inference(scs_inference,[],[10290,14])).
% 66.10/66.26 cnf(10436,plain,
% 66.10/66.26 (P2(f3(a1,a1),f6(a1),f3(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10378,10290,14,22])).
% 66.10/66.26 cnf(10438,plain,
% 66.10/66.26 (P4(f7(a4,a4),a4,f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10378,10413,10290,14,22,23])).
% 66.10/66.26 cnf(10440,plain,
% 66.10/66.26 (P2(a1,f7(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10378,10413,10250,10290,14,22,23,13])).
% 66.10/66.26 cnf(10442,plain,
% 66.10/66.26 (P2(a1,f3(a2,a2),f3(a2,a2))),
% 66.10/66.26 inference(scs_inference,[],[10339,10378,10413,10250,10290,10246,14,22,23,13,25])).
% 66.10/66.26 cnf(10444,plain,
% 66.10/66.26 (~P2(a4,f6(a2),f6(a5))),
% 66.10/66.26 inference(scs_inference,[],[10347,10339,10378,10413,10250,10290,10323,10327,10246,14,22,23,13,25,26])).
% 66.10/66.26 cnf(10456,plain,
% 66.10/66.26 (P4(a4,f3(a5,a5),f3(a5,a5))),
% 66.10/66.26 inference(scs_inference,[],[10300,14])).
% 66.10/66.26 cnf(10458,plain,
% 66.10/66.26 (P4(f3(a4,a4),a4,f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10391,10300,14,23])).
% 66.10/66.26 cnf(10460,plain,
% 66.10/66.26 (P2(f7(a4,a4),a1,f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10419,10391,10300,14,23,22])).
% 66.10/66.26 cnf(10462,plain,
% 66.10/66.26 (P2(a1,f6(a2),f6(a2))),
% 66.10/66.26 inference(scs_inference,[],[10419,10391,10300,10321,14,23,22,13])).
% 66.10/66.26 cnf(10464,plain,
% 66.10/66.26 (P2(f3(a1,a1),f7(a4,a4),f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10419,10391,10300,10321,10254,14,23,22,13,26])).
% 66.10/66.26 cnf(10466,plain,
% 66.10/66.26 (~P2(a1,f6(a4),f6(a1))),
% 66.10/66.26 inference(scs_inference,[],[10419,10391,10300,10321,10421,10240,10254,2020,14,23,22,13,26,25])).
% 66.10/66.26 cnf(10475,plain,
% 66.10/66.26 (P4(a4,f3(a2,a2),f3(a2,a2))),
% 66.10/66.26 inference(scs_inference,[],[10337,14])).
% 66.10/66.26 cnf(10477,plain,
% 66.10/66.26 (P2(f7(a4,a4),f3(a1,a1),f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10464,10337,14,22])).
% 66.10/66.26 cnf(10479,plain,
% 66.10/66.26 (P4(f3(a5,a5),a4,f3(a5,a5))),
% 66.10/66.26 inference(scs_inference,[],[10464,10456,10337,14,22,23])).
% 66.10/66.26 cnf(10481,plain,
% 66.10/66.26 (P2(f7(a1,a1),f7(a4,a4),f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10464,10456,10337,10345,14,22,23,25])).
% 66.10/66.26 cnf(10483,plain,
% 66.10/66.26 (~P2(f6(a1),a1,a4)),
% 66.10/66.26 inference(scs_inference,[],[5,10464,10456,10337,10444,10345,10308,14,22,23,25,26])).
% 66.10/66.26 cnf(10485,plain,
% 66.10/66.26 (P2(f7(a4,a4),f7(a4,a4),f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[5,10464,10458,10456,10337,10444,10345,10308,10374,10368,14,22,23,25,26,29])).
% 66.10/66.26 cnf(10490,plain,
% 66.10/66.26 (P4(a4,f6(a2),f6(a2))),
% 66.10/66.26 inference(scs_inference,[],[10321,14])).
% 66.10/66.26 cnf(10492,plain,
% 66.10/66.26 (P4(f3(a2,a2),a4,f3(a2,a2))),
% 66.10/66.26 inference(scs_inference,[],[10475,10321,14,23])).
% 66.10/66.26 cnf(10494,plain,
% 66.10/66.26 (P2(f7(a4,a4),f7(a1,a1),f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10481,10475,10321,14,23,22])).
% 66.10/66.26 cnf(10496,plain,
% 66.10/66.26 (~P2(a4,a1,a1)),
% 66.10/66.26 inference(scs_inference,[],[5,10481,10475,10462,10444,10321,14,23,22,25])).
% 66.10/66.26 cnf(10498,plain,
% 66.10/66.26 (~P2(a4,f6(a1),f6(a1))),
% 66.10/66.26 inference(scs_inference,[],[5,10481,10475,10483,10462,10444,10321,10327,10240,14,23,22,25,26])).
% 66.10/66.26 cnf(10500,plain,
% 66.10/66.26 (P2(f6(a4),f7(a4,a4),a1)),
% 66.10/66.26 inference(scs_inference,[],[5,10481,10475,10483,10244,10462,10444,10321,10327,10358,10368,10240,3675,14,23,22,25,26,29])).
% 66.10/66.26 cnf(10502,plain,
% 66.10/66.26 (P4(f3(a5,a5),f7(a4,a4),f3(a5,a5))),
% 66.10/66.26 inference(scs_inference,[],[5,10481,10479,10475,10483,10244,10462,10444,10321,10327,10358,10368,10240,3675,14,23,22,25,26,29,27])).
% 66.10/66.26 cnf(10508,plain,
% 66.10/66.26 (P4(a4,f6(a1),f6(a1))),
% 66.10/66.26 inference(scs_inference,[],[10236,14])).
% 66.10/66.26 cnf(10516,plain,
% 66.10/66.26 (P2(f3(a4,a4),f7(a1,a1),f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10496,10494,10502,10485,10442,10500,10236,14,22,23,25,26])).
% 66.10/66.26 cnf(10522,plain,
% 66.10/66.26 (P4(a4,a2,a2)),
% 66.10/66.26 inference(scs_inference,[],[3,14])).
% 66.10/66.26 cnf(10524,plain,
% 66.10/66.26 (P4(f6(a5),a4,f6(a5))),
% 66.10/66.26 inference(scs_inference,[],[10434,3,14,23])).
% 66.10/66.26 cnf(10526,plain,
% 66.10/66.26 (P2(f7(a1,a1),f3(a4,a4),f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10516,10434,3,14,23,22])).
% 66.10/66.26 cnf(10528,plain,
% 66.10/66.26 (P2(f6(a1),f7(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10516,10440,10434,10240,3,14,23,22,25])).
% 66.10/66.26 cnf(10530,plain,
% 66.10/66.26 (P2(f3(a1,a1),f7(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10516,10440,10434,10240,10254,3,14,23,22,25,26])).
% 66.10/66.26 cnf(10534,plain,
% 66.10/66.26 (P4(f3(a4,a4),f7(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10516,10440,10423,10434,10415,10485,10268,10240,10254,33,3,14,23,22,25,26,24,30])).
% 66.10/66.26 cnf(10539,plain,
% 66.10/66.26 (P4(a4,a5,a5)),
% 66.10/66.26 inference(scs_inference,[],[4,14])).
% 66.10/66.26 cnf(10541,plain,
% 66.10/66.26 (P2(f7(a1,a1),f3(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10530,4,14,22])).
% 66.10/66.26 cnf(10543,plain,
% 66.10/66.26 (P4(a2,a4,a2)),
% 66.10/66.26 inference(scs_inference,[],[10522,10530,4,14,22,23])).
% 66.10/66.26 cnf(10549,plain,
% 66.10/66.26 (~P2(f3(a1,a1),f3(a1,a1),a4)),
% 66.10/66.26 inference(scs_inference,[],[10522,10530,10492,10401,10498,10333,10368,4,14,22,23,27,28,26])).
% 66.10/66.26 cnf(10551,plain,
% 66.10/66.26 (P2(f3(a1,a1),f3(a4,a4),f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10522,10530,10526,10492,10401,10498,10333,10368,4,14,22,23,27,28,26,25])).
% 66.10/66.26 cnf(10558,plain,
% 66.10/66.26 (P4(a4,a4,a4)),
% 66.10/66.26 inference(scs_inference,[],[2,14])).
% 66.10/66.26 cnf(10560,plain,
% 66.10/66.26 (P4(a5,a4,a5)),
% 66.10/66.26 inference(scs_inference,[],[10539,2,14,23])).
% 66.10/66.26 cnf(10562,plain,
% 66.10/66.26 (P2(f3(a4,a4),f3(a1,a1),f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10539,10551,2,14,23,22])).
% 66.10/66.26 cnf(10564,plain,
% 66.10/66.26 (P4(a2,f7(a4,a4),a2)),
% 66.10/66.26 inference(scs_inference,[],[10543,10539,10551,10368,2,14,23,22,27])).
% 66.10/66.26 cnf(10566,plain,
% 66.10/66.26 (P2(f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10543,10539,10541,10551,10364,10368,2,14,23,22,27,26])).
% 66.10/66.26 cnf(10568,plain,
% 66.10/66.26 (~P2(f3(a1,a1),f7(a1,a1),a4)),
% 66.10/66.26 inference(scs_inference,[],[10543,10539,10541,10551,10364,10549,10368,2,14,23,22,27,26,25])).
% 66.10/66.26 cnf(10576,plain,
% 66.10/66.26 (P2(f6(a2),f3(a1,a1),f6(a5))),
% 66.10/66.26 inference(scs_inference,[],[10310,22])).
% 66.10/66.26 cnf(10578,plain,
% 66.10/66.26 (P4(f7(a4,a4),a2,a2)),
% 66.10/66.26 inference(scs_inference,[],[10310,10564,22,23])).
% 66.10/66.26 cnf(10580,plain,
% 66.10/66.26 (P4(f7(a2,a2),f7(a4,a4),f7(a2,a2))),
% 66.10/66.26 inference(scs_inference,[],[10310,10564,10333,22,23,28])).
% 66.10/66.26 cnf(10582,plain,
% 66.10/66.26 (P2(f3(a1,a1),f6(a5),f6(a5))),
% 66.10/66.26 inference(scs_inference,[],[10566,10310,10564,10333,22,23,28,25])).
% 66.10/66.26 cnf(10584,plain,
% 66.10/66.26 (~P2(f6(a1),f3(a1,a1),a4)),
% 66.10/66.26 inference(scs_inference,[],[10566,10310,10564,10308,10444,10333,22,23,28,25,26])).
% 66.10/66.26 cnf(10586,plain,
% 66.10/66.26 (P4(f3(a4,a4),a5,f3(a5,a5))),
% 66.10/66.26 inference(scs_inference,[],[10566,10310,10564,10304,10539,10374,10308,10444,10333,22,23,28,25,26,30])).
% 66.10/66.26 cnf(10588,plain,
% 66.10/66.26 (P2(f7(a1,a1),a1,a1)),
% 66.10/66.26 inference(scs_inference,[],[10566,10310,10564,10304,10539,10238,10252,10374,10308,10444,10333,10306,22,23,28,25,26,30,29])).
% 66.10/66.26 cnf(10592,plain,
% 66.10/66.26 (P2(f7(a1,a1),f6(a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10528,22])).
% 66.10/66.26 cnf(10596,plain,
% 66.10/66.26 (~P2(a4,f7(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10580,10528,10588,10496,22,23,25])).
% 66.10/66.26 cnf(10598,plain,
% 66.10/66.26 (~P2(f7(a1,a1),f7(a1,a1),a4)),
% 66.10/66.26 inference(scs_inference,[],[10580,10528,10588,10496,22,23,25,26])).
% 66.10/66.26 cnf(10600,plain,
% 66.10/66.26 (P4(f3(a4,a4),a2,f3(a2,a2))),
% 66.10/66.26 inference(scs_inference,[],[10580,10528,10578,10588,10496,10339,10485,22,23,25,26,30])).
% 66.10/66.26 cnf(10602,plain,
% 66.10/66.26 (~P4(f6(a1),a4,a4)),
% 66.10/66.26 inference(scs_inference,[],[10580,10528,10578,10588,10264,10496,10339,10485,22,23,25,26,30,29])).
% 66.10/66.26 cnf(10608,plain,
% 66.10/66.26 (P4(a2,f3(a4,a4),f3(a2,a2))),
% 66.10/66.26 inference(scs_inference,[],[10600,23])).
% 66.10/66.26 cnf(10612,plain,
% 66.10/66.26 (~P2(f7(a1,a1),f6(a1),a4)),
% 66.10/66.26 inference(scs_inference,[],[10600,10592,10568,10582,10530,23,22,25])).
% 66.10/66.26 cnf(10614,plain,
% 66.10/66.26 (P2(f3(a4,a4),a1,f3(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10562,10600,10262,10592,10568,10582,10530,23,22,25,26])).
% 66.10/66.26 cnf(10616,plain,
% 66.10/66.26 (P4(f3(a4,a4),f3(a1,a1),f3(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10562,10600,10262,10592,10568,10582,10393,10566,10530,10485,23,22,25,26,30])).
% 66.10/66.26 cnf(10625,plain,
% 66.10/66.26 (P2(f6(a1),a2,a2)),
% 66.10/66.26 inference(scs_inference,[],[10343,22])).
% 66.10/66.26 cnf(10627,plain,
% 66.10/66.26 (P4(f3(a1,a1),f3(a4,a4),f3(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10616,10343,22,23])).
% 66.10/66.26 cnf(10631,plain,
% 66.10/66.26 (P2(f7(a1,a1),f6(a5),f6(a5))),
% 66.10/66.26 inference(scs_inference,[],[5,10616,10608,10343,10578,10588,22,23,27,25])).
% 66.10/66.26 cnf(10633,plain,
% 66.10/66.26 (~P2(f3(a1,a1),a1,a4)),
% 66.10/66.26 inference(scs_inference,[],[5,10616,10608,10343,10582,10578,10444,10588,22,23,27,25,26])).
% 66.10/66.26 cnf(10640,plain,
% 66.10/66.26 (P4(a5,f3(a4,a4),f3(a5,a5))),
% 66.10/66.26 inference(scs_inference,[],[10586,23])).
% 66.10/66.26 cnf(10644,plain,
% 66.10/66.26 (~P2(f6(a1),a2,a5)),
% 66.10/66.26 inference(scs_inference,[],[10631,10399,10625,10586,10401,23,22,25])).
% 66.10/66.26 cnf(10648,plain,
% 66.10/66.26 (P2(a1,f7(a1,a1),a1)),
% 66.10/66.26 inference(scs_inference,[],[10631,10596,10399,10625,10586,10541,10364,10401,10238,10252,10327,23,22,25,26,29])).
% 66.10/66.26 cnf(10654,plain,
% 66.10/66.26 (P2(a5,f6(a5),a1)),
% 66.10/66.26 inference(scs_inference,[],[10286,22])).
% 66.10/66.26 cnf(10656,plain,
% 66.10/66.26 (P4(f7(a1,a1),f3(a4,a4),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10534,10286,22,23])).
% 66.10/66.26 cnf(10660,plain,
% 66.10/66.26 (P2(f7(a4,a4),f6(a1),f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10584,10477,10436,10534,10286,10378,22,23,25,26])).
% 66.10/66.26 cnf(10662,plain,
% 66.10/66.26 (P4(f3(a4,a4),f3(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10584,10477,10436,10534,10286,10616,10397,10378,10541,10329,22,23,25,26,30])).
% 66.10/66.26 cnf(10668,plain,
% 66.10/66.26 (P4(f3(a1,a1),f3(a4,a4),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10662,23])).
% 66.10/66.26 cnf(10670,plain,
% 66.10/66.26 (P2(f6(a1),f7(a4,a4),f7(a4,a4))),
% 66.10/66.26 inference(scs_inference,[],[10662,10660,23,22])).
% 66.10/66.26 cnf(10672,plain,
% 66.10/66.26 (~P2(a4,a5,a5)),
% 66.10/66.26 inference(scs_inference,[],[10662,10660,10654,10496,23,22,25])).
% 66.10/66.26 cnf(10674,plain,
% 66.10/66.26 (~P2(f7(a1,a1),a1,a4)),
% 66.10/66.26 inference(scs_inference,[],[5,10662,10660,10654,10631,10496,10444,23,22,25,26])).
% 66.10/66.26 cnf(10676,plain,
% 66.10/66.26 (~P4(a1,f3(a4,a4),a4)),
% 66.10/66.26 inference(scs_inference,[],[5,10656,10662,10660,10654,10631,10596,10440,10496,10444,23,22,25,26,29])).
% 66.10/66.26 cnf(10685,plain,
% 66.10/66.26 (P4(a1,f3(a4,a4),f3(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10331,10407,22,23])).
% 66.10/66.26 cnf(10687,plain,
% 66.10/66.26 (~P2(a1,f7(a1,a1),a4)),
% 66.10/66.26 inference(scs_inference,[],[10648,10380,10331,10407,10240,22,23,25])).
% 66.10/66.26 cnf(10689,plain,
% 66.10/66.26 (~P2(f7(a1,a1),f6(a4),f6(a1))),
% 66.10/66.26 inference(scs_inference,[],[10648,10466,10380,10331,10296,10407,10240,22,23,25,26])).
% 66.10/66.26 cnf(10691,plain,
% 66.10/66.26 (P4(f3(a4,a4),a1,f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10648,10466,10614,10380,10331,10296,10407,10530,10252,10240,22,23,25,26,30])).
% 66.10/66.26 cnf(10697,plain,
% 66.10/66.26 (P4(a1,f3(a4,a4),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10691,23])).
% 66.10/66.26 cnf(10701,plain,
% 66.10/66.26 (P4(a1,f7(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10685,10691,10423,10384,10662,23,22,27])).
% 66.10/66.26 cnf(10705,plain,
% 66.10/66.26 (P2(f3(a1,a1),f3(a2,a2),f3(a2,a2))),
% 66.10/66.26 inference(scs_inference,[],[10612,10685,10691,10442,10423,10384,10662,10296,10588,10254,23,22,27,25,26])).
% 66.10/66.26 cnf(10707,plain,
% 66.10/66.26 (P2(f3(a1,a1),f3(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10612,10685,10691,10668,10442,10423,10384,10662,10296,10588,10254,23,22,27,25,26,29])).
% 66.10/66.26 cnf(10711,plain,
% 66.10/66.26 (P4(f7(a1,a1),a1,f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10701,23])).
% 66.10/66.26 cnf(10715,plain,
% 66.10/66.26 (~P4(f7(a1,a1),a4,a4)),
% 66.10/66.26 inference(scs_inference,[],[10705,10697,10701,10676,10458,23,22,27])).
% 66.10/66.26 cnf(10719,plain,
% 66.10/66.26 (P2(f7(a1,a1),f3(a2,a2),f3(a2,a2))),
% 66.10/66.26 inference(scs_inference,[],[10707,10705,10697,10701,10676,10458,10596,23,22,27,25,26])).
% 66.10/66.26 cnf(10721,plain,
% 66.10/66.26 (~P4(f7(a1,a1),f3(a1,a1),a4)),
% 66.10/66.26 inference(scs_inference,[],[10707,10705,10598,10697,10701,10676,10458,10384,10596,23,22,27,25,26,29])).
% 66.10/66.26 cnf(10726,plain,
% 66.10/66.26 (P4(f6(a2),a4,f6(a2))),
% 66.10/66.26 inference(scs_inference,[],[10490,23])).
% 66.10/66.26 cnf(10732,plain,
% 66.10/66.26 (P4(f7(a1,a1),f7(a1,a1),f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10719,10711,10721,10490,10329,10252,23,22,28,27])).
% 66.10/66.26 cnf(10734,plain,
% 66.10/66.26 (P2(f6(a1),f3(a2,a2),f3(a2,a2))),
% 66.10/66.26 inference(scs_inference,[],[10719,10711,10721,10490,10528,10329,10252,23,22,28,27,25])).
% 66.10/66.26 cnf(10736,plain,
% 66.10/66.26 (~P2(f6(a1),a4,f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10719,10674,10711,10721,10490,10528,10341,10329,10252,10327,23,22,28,27,25,26])).
% 66.10/66.26 cnf(10744,plain,
% 66.10/66.26 (P4(f6(a1),a4,f6(a1))),
% 66.10/66.26 inference(scs_inference,[],[10508,23])).
% 66.10/66.26 cnf(10748,plain,
% 66.10/66.26 (~P2(a1,a4,f7(a1,a1))),
% 66.10/66.26 inference(scs_inference,[],[10734,10736,10306,10508,10240,23,22,25])).
% 66.10/66.27 cnf(10750,plain,
% 66.10/66.27 (P2(f3(a4,a4),f6(a1),f3(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10734,10736,10516,10592,10306,10508,10240,23,22,25,26])).
% 66.10/66.27 cnf(10758,plain,
% 66.10/66.27 (P2(f6(a1),f3(a4,a4),f3(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10750,22])).
% 66.10/66.27 cnf(10760,plain,
% 66.10/66.27 (~P4(f7(a1,a1),x107601,a4)),
% 66.10/66.27 inference(scs_inference,[],[10750,10732,10715,22,27])).
% 66.10/66.27 cnf(10762,plain,
% 66.10/66.27 (~P2(a4,a4,a4)),
% 66.10/66.27 inference(scs_inference,[],[10750,10732,10417,10715,10496,22,27,25])).
% 66.10/66.27 cnf(10766,plain,
% 66.10/66.27 (P4(f3(a4,a4),f7(a4,a4),f3(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10750,10687,10732,10417,10715,10413,10494,10500,10374,10496,10485,22,27,25,26,30])).
% 66.10/66.27 cnf(10770,plain,
% 66.10/66.27 (P4(f7(a4,a4),f3(a4,a4),f3(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10750,10687,10748,10732,10417,10715,10413,10494,10500,10374,10238,10496,10485,10252,22,27,25,26,30,29,23])).
% 66.10/66.27 cnf(10772,plain,
% 66.10/66.27 (P2(f7(a2,a2),a1,f7(a2,a2))),
% 66.10/66.27 inference(scs_inference,[],[10362,22])).
% 66.10/66.27 cnf(10774,plain,
% 66.10/66.27 (P4(f3(a1,a1),f7(a1,a1),f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[10732,10316,10701,10362,22,27])).
% 66.10/66.27 cnf(10776,plain,
% 66.10/66.27 (~P2(a2,f6(a1),a5)),
% 66.10/66.27 inference(scs_inference,[],[10270,10732,10343,10316,10701,10362,10246,22,27,25])).
% 66.10/66.27 cnf(10778,plain,
% 66.10/66.27 (~P2(f6(a1),f6(a1),a4)),
% 66.10/66.27 inference(scs_inference,[],[10762,10270,10732,10343,10316,10701,10362,10246,10341,22,27,25,26])).
% 66.10/66.27 cnf(10780,plain,
% 66.10/66.27 (P4(f7(a1,a1),f3(a1,a1),f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[10762,10270,10732,10343,10316,10701,10362,10246,10341,22,27,25,26,23])).
% 66.10/66.27 cnf(10786,plain,
% 66.10/66.27 (~P4(f3(a4,a4),f7(a1,a1),a4)),
% 66.10/66.27 inference(scs_inference,[],[5,10762,10758,10760,10270,10691,10732,10697,10481,10343,10316,10701,10362,10246,10596,10341,22,27,25,26,23,30,29,28])).
% 66.10/66.27 cnf(10789,plain,
% 66.10/66.27 (P2(a2,f6(a2),a1)),
% 66.10/66.27 inference(scs_inference,[],[10323,22])).
% 66.10/66.27 cnf(10791,plain,
% 66.10/66.27 (~P2(f3(a1,a1),f6(a4),f6(a1))),
% 66.10/66.27 inference(scs_inference,[],[10466,10323,10254,2020,22,25])).
% 66.10/66.27 cnf(10793,plain,
% 66.10/66.27 (P2(f3(a1,a1),f7(a5,a5),f7(a5,a5))),
% 66.10/66.27 inference(scs_inference,[],[10466,10331,10323,10254,2020,22,25,26])).
% 66.10/66.27 cnf(10804,plain,
% 66.10/66.27 (~P4(f3(a1,a1),f7(a4,a4),a4)),
% 66.10/66.27 inference(scs_inference,[],[10793,10676,10766,10685,22,27])).
% 66.10/66.27 cnf(10806,plain,
% 66.10/66.27 (~P2(a4,a2,a2)),
% 66.10/66.27 inference(scs_inference,[],[10793,10789,10676,10766,10685,10496,22,27,25])).
% 66.10/66.27 cnf(10808,plain,
% 66.10/66.27 (~P2(a1,f3(a1,a1),a4)),
% 66.10/66.27 inference(scs_inference,[],[10793,10633,10789,10676,10766,10262,10260,10685,10496,22,27,25,26])).
% 66.10/66.27 cnf(10819,plain,
% 66.10/66.27 (P2(a5,a1,a5)),
% 66.10/66.27 inference(scs_inference,[],[10256,22])).
% 66.10/66.27 cnf(10821,plain,
% 66.10/66.27 (~P2(a2,f6(a2),a4)),
% 66.10/66.27 inference(scs_inference,[],[10789,10625,10380,10256,22,25])).
% 66.10/66.27 cnf(10825,plain,
% 66.10/66.27 (~P2(a5,a1,a2)),
% 66.10/66.27 inference(scs_inference,[],[5,10347,10789,10625,10380,10256,10306,22,25,26,3639])).
% 66.10/66.27 cnf(10834,plain,
% 66.10/66.27 (P2(f6(a1),a1,f6(a1))),
% 66.10/66.27 inference(scs_inference,[],[10296,22])).
% 66.10/66.27 cnf(10836,plain,
% 66.10/66.27 (~P2(a4,a1,f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[10736,10296,10327,10341,22,25])).
% 66.10/66.27 cnf(10838,plain,
% 66.10/66.27 (~P2(a2,f6(a5),f3(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[10736,10399,10292,10286,10296,10327,10341,22,25,26])).
% 66.10/66.27 cnf(10840,plain,
% 66.10/66.27 (P2(f3(a5,a5),f7(a1,a1),f3(a5,a5))),
% 66.10/66.27 inference(scs_inference,[],[10819,10736,10399,10292,10286,10640,10296,10697,10327,10341,22,25,26,29])).
% 66.10/66.27 cnf(10849,plain,
% 66.10/66.27 (~P2(a4,f6(a5),f6(a5))),
% 66.10/66.27 inference(scs_inference,[],[10840,10286,10496,22,25])).
% 66.10/66.27 cnf(10851,plain,
% 66.10/66.27 (~P2(a2,f6(a5),a4)),
% 66.10/66.27 inference(scs_inference,[],[5,10840,10821,10292,10286,10496,22,25,26])).
% 66.10/66.27 cnf(10853,plain,
% 66.10/66.27 (~P4(f6(a4),f7(a1,a1),a4)),
% 66.10/66.27 inference(scs_inference,[],[5,10840,10821,10274,10292,10286,10358,10701,10496,10596,22,25,26,29])).
% 66.10/66.27 cnf(10855,plain,
% 66.10/66.27 (~P2(a1,a4,a1)),
% 66.10/66.27 inference(scs_inference,[],[5,10840,10821,10274,10292,10286,10358,10701,10496,10596,22,25,26,29,729])).
% 66.10/66.27 cnf(10859,plain,
% 66.10/66.27 (P4(f8(a4),a4,a4)),
% 66.10/66.27 inference(scs_inference,[],[5,10840,10821,10274,10292,10286,10358,10701,10496,10596,2,22,25,26,29,729,16,20])).
% 66.10/66.27 cnf(10863,plain,
% 66.10/66.27 (P4(a4,f8(a4),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[5,10840,10821,10274,10292,10286,10358,10701,10496,10596,2,22,25,26,29,729,16,20,9,14])).
% 66.10/66.27 cnf(10865,plain,
% 66.10/66.27 (P2(a1,f8(a4),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[5,10840,10821,10274,10292,10286,10358,10701,10496,10596,2,22,25,26,29,729,16,20,9,14,13])).
% 66.10/66.27 cnf(10867,plain,
% 66.10/66.27 (P4(a4,f8(a4),a4)),
% 66.10/66.27 inference(scs_inference,[],[5,10840,10821,10274,10292,10286,10358,10701,10496,10596,2,22,25,26,29,729,16,20,9,14,13,23])).
% 66.10/66.27 cnf(10873,plain,
% 66.10/66.27 (P4(f8(a4),a4,f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10863,23])).
% 66.10/66.27 cnf(10875,plain,
% 66.10/66.27 (P2(f8(a4),a1,f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10863,10865,23,22])).
% 66.10/66.27 cnf(10877,plain,
% 66.10/66.27 (~P4(f8(a4),f8(a4),f6(a1))),
% 66.10/66.27 inference(scs_inference,[],[10859,10863,10865,10602,23,22,28])).
% 66.10/66.27 cnf(10881,plain,
% 66.10/66.27 (P2(f7(a1,a1),f8(a4),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10859,10863,10865,10867,10602,10744,10588,23,22,28,27,25])).
% 66.10/66.27 cnf(10883,plain,
% 66.10/66.27 (~P2(f6(a2),a4,f6(a2))),
% 66.10/66.27 inference(scs_inference,[],[10855,10859,10863,10865,10867,10602,10744,10789,10588,23,22,28,27,25,26])).
% 66.10/66.27 cnf(10885,plain,
% 66.10/66.27 (~P2(f8(a4),f8(a4),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10855,10859,10863,10865,10867,10602,10744,10762,10789,10588,23,22,28,27,25,26,29])).
% 66.10/66.27 cnf(10891,plain,
% 66.10/66.27 (P2(f8(a4),f7(a1,a1),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10881,22])).
% 66.10/66.27 cnf(10893,plain,
% 66.10/66.27 (P4(f8(a4),f8(a4),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10881,10873,10867,22,28])).
% 66.10/66.27 cnf(10895,plain,
% 66.10/66.27 (~P2(a5,f7(a1,a1),a2)),
% 66.10/66.27 inference(scs_inference,[],[10825,10881,10873,10867,10819,10648,22,28,25])).
% 66.10/66.27 cnf(10897,plain,
% 66.10/66.27 (~P2(f7(a1,a1),f7(a1,a1),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10825,10881,10885,10873,10867,10819,10648,22,28,25,26])).
% 66.10/66.27 cnf(10906,plain,
% 66.10/66.27 (P2(f7(a1,a1),a1,f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[10440,22])).
% 66.10/66.27 cnf(10912,plain,
% 66.10/66.27 (~P2(a4,f6(a2),f6(a2))),
% 66.10/66.27 inference(scs_inference,[],[10786,10849,10770,10576,10534,10264,10859,10440,22,28,27,25])).
% 66.10/66.27 cnf(10914,plain,
% 66.10/66.27 (~P2(f7(a1,a1),f8(a4),f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[10786,10897,10891,10849,10770,10576,10534,10881,10264,10859,10440,22,28,27,25,26])).
% 66.10/66.27 cnf(10918,plain,
% 66.10/66.27 (~P4(f7(a1,a1),f8(a4),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10786,10893,10897,10891,10849,10770,10576,10885,10758,10534,10881,10264,10859,10440,22,28,27,25,26,30,29])).
% 66.10/66.27 cnf(10920,plain,
% 66.10/66.27 (P2(f6(a1),f3(a1,a1),f6(a1))),
% 66.10/66.27 inference(scs_inference,[],[10401,22])).
% 66.10/66.27 cnf(10922,plain,
% 66.10/66.27 (~P4(f6(a1),a4,f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10877,10744,10867,10401,22,28])).
% 66.10/66.27 cnf(10930,plain,
% 66.10/66.27 (~P4(a1,f8(a4),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10644,10877,10875,10893,10897,10744,10885,10865,10676,10819,10458,10867,10401,10323,10685,10588,22,28,27,25,26,29])).
% 66.10/66.27 cnf(10936,plain,
% 66.10/66.27 (P2(f7(a4,a4),f6(a4),a1)),
% 66.10/66.27 inference(scs_inference,[],[10500,22])).
% 66.10/66.27 cnf(10942,plain,
% 66.10/66.27 (P2(f7(a2,a2),f6(a1),f7(a2,a2))),
% 66.10/66.27 inference(scs_inference,[],[10776,10920,10772,10356,10242,10343,10500,10859,22,27,25,26])).
% 66.10/66.27 cnf(10944,plain,
% 66.10/66.27 (~P2(f6(a1),f3(a1,a1),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10776,10920,10922,10772,10356,10294,10242,10343,10744,10500,10859,22,27,25,26,30])).
% 66.10/66.27 cnf(10956,plain,
% 66.10/66.27 (~P2(a4,f7(a4,a4),f7(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10853,10942,10936,10264,10859,10496,22,27,25])).
% 66.10/66.27 cnf(10960,plain,
% 66.10/66.27 (~P4(f3(a4,a4),f8(a4),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[5,10853,10942,10912,10936,10885,10863,10264,10859,10374,10496,10327,22,27,25,26,29])).
% 66.10/66.27 cnf(10967,plain,
% 66.10/66.27 (P2(f6(a2),a1,f6(a2))),
% 66.10/66.27 inference(scs_inference,[],[10462,22])).
% 66.10/66.27 cnf(10969,plain,
% 66.10/66.27 (~P4(f7(a1,a1),x109691,f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10918,10732,10462,22,27])).
% 66.10/66.27 cnf(10971,plain,
% 66.10/66.27 (~P2(f7(a4,a4),f6(a4),a4)),
% 66.10/66.27 inference(scs_inference,[],[10918,10936,10855,10732,10419,10462,22,27,25])).
% 66.10/66.27 cnf(10973,plain,
% 66.10/66.27 (~P2(f6(a1),f7(a4,a4),f3(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[10791,10918,10834,10936,10855,10732,10419,10462,22,27,25,26])).
% 66.10/66.27 cnf(10980,plain,
% 66.10/66.27 (P2(a4,f6(a1),a4)),
% 66.10/66.27 inference(scs_inference,[],[10341,22])).
% 66.10/66.27 cnf(10982,plain,
% 66.10/66.27 (P4(f8(a4),f6(a5),f6(a5))),
% 66.10/66.27 inference(scs_inference,[],[10434,10859,10341,22,27])).
% 66.10/66.27 cnf(10984,plain,
% 66.10/66.27 (~P2(a2,f6(a2),f3(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[5,10838,10434,10292,10859,10341,22,27,25])).
% 66.10/66.27 cnf(10986,plain,
% 66.10/66.27 (P2(f3(a1,a1),f3(a5,a5),f3(a5,a5))),
% 66.10/66.27 inference(scs_inference,[],[5,10838,10434,10423,10292,10859,10341,10254,22,27,25,26])).
% 66.10/66.27 cnf(10988,plain,
% 66.10/66.27 (~P2(f6(a1),a1,f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[5,10838,10922,10834,10434,10423,10744,10292,10859,10244,10341,10254,22,27,25,26,30])).
% 66.10/66.27 cnf(10992,plain,
% 66.10/66.27 (P4(f6(a5),f8(a4),f6(a5))),
% 66.10/66.27 inference(scs_inference,[],[5,10838,10914,10922,10834,10434,10423,10592,10711,10744,10292,10859,10244,10341,10254,22,27,25,26,30,29,23])).
% 66.10/66.27 cnf(10996,plain,
% 66.10/66.27 (~P4(a4,f6(a1),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10986,10877,10508,10859,22,27])).
% 66.10/66.27 cnf(10998,plain,
% 66.10/66.27 (~P2(f8(a4),f7(a1,a1),f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[10986,10877,10881,10885,10508,10859,22,27,25])).
% 66.10/66.27 cnf(11010,plain,
% 66.10/66.27 (~P4(f7(a1,a1),x110101,f8(a4))),
% 66.10/66.27 inference(rename_variables,[],[10969])).
% 66.10/66.27 cnf(11012,plain,
% 66.10/66.27 (~P2(a4,f6(a4),a4)),
% 66.10/66.27 inference(scs_inference,[],[10774,10969,10417,10780,10380,10341,28,25])).
% 66.10/66.27 cnf(11019,plain,
% 66.10/66.27 (P2(a1,a1,f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[10778,10774,10969,11010,10980,10417,10780,10380,10707,10691,10627,10296,10238,10374,10341,28,25,26,30,29])).
% 66.10/66.27 cnf(11023,plain,
% 66.10/66.27 (~P4(f8(a4),a4,f3(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10960,10873,10867,28])).
% 66.10/66.27 cnf(11027,plain,
% 66.10/66.27 (~P2(f8(a4),a1,a1)),
% 66.10/66.27 inference(scs_inference,[],[11019,10998,10960,10873,10456,10867,10859,28,27,25])).
% 66.10/66.27 cnf(11029,plain,
% 66.10/66.27 (P2(a5,f6(a5),f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[11019,10998,10960,10873,10456,10654,10256,10867,10859,28,27,25,26])).
% 66.10/66.27 cnf(11035,plain,
% 66.10/66.27 (P2(f6(a5),a5,f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[11019,10998,10960,10906,10873,10456,10914,10403,10654,10256,10867,10859,28,27,25,26,29,23,22])).
% 66.10/66.27 cnf(11039,plain,
% 66.10/66.27 (~P4(a4,f3(a4,a4),a4)),
% 66.10/66.27 inference(scs_inference,[],[11023,10391,10859,27])).
% 66.10/66.27 cnf(11041,plain,
% 66.10/66.27 (~P2(f8(a4),a5,a5)),
% 66.10/66.27 inference(scs_inference,[],[11023,11029,10998,10391,10859,27,25])).
% 66.10/66.27 cnf(11043,plain,
% 66.10/66.27 (~P2(f7(a1,a1),f8(a4),f6(a1))),
% 66.10/66.27 inference(scs_inference,[],[10988,11023,11029,10998,10875,10391,10881,10859,27,25,26])).
% 66.10/66.27 cnf(11045,plain,
% 66.10/66.27 (~P2(f6(a5),a5,f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10988,11023,11029,11035,10560,10998,10875,10524,10969,10391,10881,10859,27,25,26,30])).
% 66.10/66.27 cnf(11050,plain,
% 66.10/66.27 (~P4(f8(a4),f3(a4,a4),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10988,11023,11029,11035,10992,10560,10998,10875,10849,10524,10969,10582,10391,10881,10867,10859,27,25,26,30,29,28])).
% 66.10/66.27 cnf(11067,plain,
% 66.10/66.27 (~P4(f8(a4),a4,a1)),
% 66.10/66.27 inference(scs_inference,[],[10930,10873,10867,28])).
% 66.10/66.27 cnf(11069,plain,
% 66.10/66.27 (~P4(a4,a4,f3(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10930,11039,10558,10873,10867,28,27])).
% 66.10/66.27 cnf(11071,plain,
% 66.10/66.27 (~P2(f7(a1,a1),a5,a2)),
% 66.10/66.27 inference(scs_inference,[],[10930,11039,10895,11035,11029,10558,10873,10867,28,27,25])).
% 66.10/66.27 cnf(11073,plain,
% 66.10/66.27 (P2(f3(a4,a4),f6(a4),f7(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10930,11039,10895,10460,11035,11029,10558,10873,10936,10485,10867,28,27,25,26])).
% 66.10/66.27 cnf(11079,plain,
% 66.10/66.27 (P2(f6(a4),f3(a4,a4),f7(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10930,11039,10895,10460,10778,11035,11029,10558,10873,10936,10391,10485,10685,10867,10508,10306,10374,28,27,25,26,30,29,22])).
% 66.10/66.27 cnf(11082,plain,
% 66.10/66.27 (~P4(f8(a4),f8(a4),f3(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[11050,10893,27])).
% 66.10/66.27 cnf(11086,plain,
% 66.10/66.27 (~P2(a1,f6(a1),f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[10956,10944,11073,11050,10920,10893,10296,27,25,26])).
% 66.10/66.27 cnf(11088,plain,
% 66.10/66.27 (~P2(a4,f6(a1),f3(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10956,10944,11073,11069,11050,10920,10980,10893,10558,10296,10744,27,25,26,30])).
% 66.10/66.27 cnf(11102,plain,
% 66.10/66.27 (~P4(a4,a1,a4)),
% 66.10/66.27 inference(scs_inference,[],[11067,10238,10859,27])).
% 66.10/66.27 cnf(11114,plain,
% 66.10/66.27 (~P4(f7(a4,a4),f3(a1,a1),a4)),
% 66.10/66.27 inference(scs_inference,[],[10804,10393,10376,28])).
% 66.10/66.27 cnf(11116,plain,
% 66.10/66.27 (~P4(a4,a4,a1)),
% 66.10/66.27 inference(scs_inference,[],[11102,10804,10393,10376,10558,28,27])).
% 66.10/66.27 cnf(11118,plain,
% 66.10/66.27 (~P2(f8(a4),f6(a5),f6(a5))),
% 66.10/66.27 inference(scs_inference,[],[11102,10804,10393,10998,10376,11035,10558,28,27,25])).
% 66.10/66.27 cnf(11120,plain,
% 66.10/66.27 (~P2(f7(a4,a4),f7(a4,a4),a4)),
% 66.10/66.27 inference(scs_inference,[],[11102,10804,11088,10660,10393,10998,10376,11035,10485,10558,28,27,25,26])).
% 66.10/66.27 cnf(11122,plain,
% 66.10/66.27 (~P2(a1,f8(a4),a1)),
% 66.10/66.27 inference(scs_inference,[],[11102,10804,11088,10660,10393,10998,10376,11035,10485,10558,28,27,25,26,729])).
% 66.10/66.27 cnf(11128,plain,
% 66.10/66.27 (~P4(a4,f6(a1),a4)),
% 66.10/66.27 inference(scs_inference,[],[10996,10873,10859,28])).
% 66.10/66.27 cnf(11132,plain,
% 66.10/66.27 (~P2(f8(a4),f6(a2),f6(a2))),
% 66.10/66.27 inference(scs_inference,[],[11118,10366,10996,10576,10873,10368,10859,28,27,25])).
% 66.10/66.27 cnf(11134,plain,
% 66.10/66.27 (~P2(f6(a1),f7(a4,a4),f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[10689,11118,10366,10996,10576,10834,10873,10936,10368,10859,28,27,25,26])).
% 66.10/66.27 cnf(11138,plain,
% 66.10/66.27 (~P2(f7(a4,a4),f6(a1),a1)),
% 66.10/66.27 inference(scs_inference,[],[11116,10689,11118,10982,10366,10996,10576,10834,10873,10936,10865,10980,10368,10744,10859,28,27,25,26,29,30])).
% 66.10/66.27 cnf(11144,plain,
% 66.10/66.27 (~P4(a4,a4,f6(a1))),
% 66.10/66.27 inference(scs_inference,[],[11128,10558,10867,28,27])).
% 66.10/66.27 cnf(11146,plain,
% 66.10/66.27 (~P2(a1,f3(a4,a4),a4)),
% 66.10/66.27 inference(scs_inference,[],[11120,11128,11079,10936,10558,10867,28,27,25])).
% 66.10/66.27 cnf(11148,plain,
% 66.10/66.27 (P2(a5,f6(a2),f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[5,11120,11128,11079,11029,10819,10936,10558,10867,28,27,25,26])).
% 66.10/66.27 cnf(11152,plain,
% 66.10/66.27 (P2(f6(a2),a5,f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[5,11120,11128,11079,11116,11029,10819,10936,10980,10558,10867,10744,28,27,25,26,30,22])).
% 66.10/66.27 cnf(11156,plain,
% 66.10/66.27 (P4(f6(a2),f8(a4),f6(a2))),
% 66.10/66.27 inference(scs_inference,[],[10726,10867,28])).
% 66.10/66.27 cnf(11158,plain,
% 66.10/66.27 (P4(f7(a4,a4),f7(a4,a4),f7(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[10438,10726,10368,10867,28,27])).
% 66.10/66.27 cnf(11166,plain,
% 66.10/66.27 (P4(f8(a4),f6(a2),f6(a2))),
% 66.10/66.27 inference(scs_inference,[],[11027,10438,10726,10967,11118,10308,10789,10885,10863,10980,10368,10867,28,27,25,26,29,23])).
% 66.10/66.27 cnf(11171,plain,
% 66.10/66.27 (~P4(f8(a4),f8(a4),a1)),
% 66.10/66.27 inference(scs_inference,[],[10930,10893,28])).
% 66.10/66.27 cnf(11173,plain,
% 66.10/66.27 (P4(a5,f7(a4,a4),a5)),
% 66.10/66.27 inference(scs_inference,[],[10930,10560,10893,10368,28,27])).
% 66.10/66.27 cnf(11177,plain,
% 66.10/66.27 (~P2(a5,f8(a4),a5)),
% 66.10/66.27 inference(scs_inference,[],[11122,10973,10930,10477,10560,10260,10286,10893,10368,28,27,25,26])).
% 66.10/66.27 cnf(11181,plain,
% 66.10/66.27 (~P2(a1,f7(a4,a4),f6(a1))),
% 66.10/66.27 inference(scs_inference,[],[11122,10973,11166,11144,10930,10883,10477,10560,10875,10260,10286,10893,10306,10244,10368,28,27,25,26,29,30])).
% 66.10/66.27 cnf(11183,plain,
% 66.10/66.27 (P4(f7(a4,a4),a5,a5)),
% 66.10/66.27 inference(scs_inference,[],[11122,10973,11166,11144,10930,10883,10477,10560,10875,10260,10286,10893,10306,10244,10368,28,27,25,26,29,30,23])).
% 66.10/66.27 cnf(11188,plain,
% 66.10/66.27 (~P4(a4,a1,f8(a4))),
% 66.10/66.27 inference(scs_inference,[],[11171,11102,10238,10867,10859,28,27])).
% 66.10/66.27 cnf(11190,plain,
% 66.10/66.27 (~P2(f7(a4,a4),f6(a1),f7(a1,a1))),
% 66.10/66.27 inference(scs_inference,[],[11138,11171,11102,10834,10238,10588,10867,10859,28,27,25])).
% 66.10/66.27 cnf(11192,plain,
% 66.10/66.27 (~P2(a5,f6(a2),a4)),
% 66.10/66.27 inference(scs_inference,[],[11138,10836,11171,11148,11102,10967,10834,10238,10588,10867,10859,28,27,25,26])).
% 66.10/66.27 cnf(11196,plain,
% 66.10/66.27 (~P2(f8(a4),a1,f3(a4,a4))),
% 66.10/66.27 inference(scs_inference,[],[5,11138,10836,11171,11148,11102,11023,11156,10967,10875,10834,10992,10873,10444,10238,10588,10244,10867,10859,28,27,25,26,29,30])).
% 66.10/66.27 cnf(11206,plain,
% 66.10/66.27 (~P4(a4,f8(a4),a1)),
% 66.10/66.27 inference(scs_inference,[],[11188,10586,10668,10760,10863,10558,28,27])).
% 66.10/66.27 cnf(11247,plain,
% 66.15/66.27 (~P2(f8(a4),f3(a1,a1),f3(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[10998,10707,25])).
% 66.15/66.27 cnf(11249,plain,
% 66.15/66.27 (~P2(a5,f6(a5),f7(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11190,10395,10998,11029,10707,25,26])).
% 66.15/66.27 cnf(11253,plain,
% 66.15/66.27 (~P2(a1,a1,f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[10672,11190,10395,11173,10998,11019,11029,10969,10707,10256,10244,25,26,29,30])).
% 66.15/66.27 cnf(11261,plain,
% 66.15/66.27 (~P4(a1,a4,f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11206,10238,10244,27])).
% 66.15/66.27 cnf(11263,plain,
% 66.15/66.27 (~P2(f6(a2),f7(a4,a4),f6(a5))),
% 66.15/66.27 inference(scs_inference,[],[11206,11249,11148,10481,10238,10244,27,25])).
% 66.15/66.27 cnf(11267,plain,
% 66.15/66.27 (~P2(f6(a2),a5,a4)),
% 66.15/66.27 inference(scs_inference,[],[11041,11206,11249,11152,11148,10726,10481,10560,10760,10819,10286,10238,10244,27,25,26,30])).
% 66.15/66.27 cnf(11272,plain,
% 66.15/66.27 (~P4(f3(a4,a4),a4,a4)),
% 66.15/66.27 inference(scs_inference,[],[11069,10458,10391,27])).
% 66.15/66.27 cnf(11280,plain,
% 66.15/66.27 (~P2(f7(a1,a1),a1,f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11043,11196,11188,11069,11177,10906,10516,10477,11183,10458,10891,10391,10881,10252,10306,10238,27,25,26,29,30])).
% 66.15/66.27 cnf(11287,plain,
% 66.15/66.27 (~P4(f3(a4,a4),f7(a4,a4),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[10438,11023,10766,28])).
% 66.15/66.27 cnf(11291,plain,
% 66.15/66.27 (~P2(a1,f7(a4,a4),f7(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[11134,11027,10670,10438,11023,10766,10417,10296,28,25,26])).
% 66.15/66.27 cnf(11315,plain,
% 66.15/66.27 (~P2(f6(a4),f3(a4,a4),f7(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[11291,11079,10475,10859,2020,27,25])).
% 66.15/66.27 cnf(11317,plain,
% 66.15/66.27 (~P2(f7(a4,a4),a5,a5)),
% 66.15/66.27 inference(scs_inference,[],[11291,11249,11079,10475,10460,10654,10859,2020,27,25,26])).
% 66.15/66.27 cnf(11325,plain,
% 66.15/66.27 (~P4(a4,f3(a4,a4),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11082,10391,10859,27])).
% 66.15/66.27 cnf(11327,plain,
% 66.15/66.27 (~P2(f8(a4),a2,a2)),
% 66.15/66.27 inference(scs_inference,[],[11082,11027,10789,10391,10859,27,25])).
% 66.15/66.27 cnf(11329,plain,
% 66.15/66.27 (~P2(f8(a4),f6(a2),f6(a5))),
% 66.15/66.27 inference(scs_inference,[],[11045,11082,11027,11152,10891,10789,10391,10859,27,25,26])).
% 66.15/66.27 cnf(11331,plain,
% 66.15/66.27 (~P4(f6(a1),f8(a4),f6(a4))),
% 66.15/66.27 inference(scs_inference,[],[11012,11045,11082,11027,11152,10891,10789,10391,10980,10867,10859,27,25,26,29])).
% 66.15/66.27 cnf(11333,plain,
% 66.15/66.27 (~P2(f8(a4),f7(a1,a1),a1)),
% 66.15/66.27 inference(scs_inference,[],[11012,11045,11082,11067,11027,11152,10891,10789,10264,10391,10873,10980,10867,10859,27,25,26,29,30])).
% 66.15/66.27 cnf(11341,plain,
% 66.15/66.27 (~P2(f3(a4,a4),f6(a1),a4)),
% 66.15/66.27 inference(scs_inference,[],[10971,11329,11272,10750,10982,10849,10310,10458,10865,10417,10462,10327,10744,25,26,29,30])).
% 66.15/66.27 cnf(11348,plain,
% 66.15/66.27 (~P4(f6(a4),a4,f6(a1))),
% 66.15/66.27 inference(scs_inference,[],[11331,10867,3675,28])).
% 66.15/66.27 cnf(11354,plain,
% 66.15/66.27 (P2(f7(a4,a4),a4,f3(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11331,11333,11073,10614,11148,11069,10766,10358,10789,10391,10867,3675,28,27,25,26])).
% 66.15/66.27 cnf(11356,plain,
% 66.15/66.27 (~P4(a1,f7(a4,a4),f7(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11331,11333,11317,11073,10614,11148,11069,11173,10766,10358,10256,10789,10391,10867,3675,28,27,25,26,29])).
% 66.15/66.27 cnf(11358,plain,
% 66.15/66.27 (P2(a4,f7(a4,a4),f3(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11331,11333,11317,11073,10614,11148,11069,11173,10766,10358,10256,10789,10391,10867,3675,28,27,25,26,29,22])).
% 66.15/66.27 cnf(11363,plain,
% 66.15/66.27 (~P4(a4,f8(a4),f3(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11325,10863,10558,27])).
% 66.15/66.27 cnf(11378,plain,
% 66.15/66.27 (~P2(a1,f7(a4,a4),f3(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[11315,11181,10614,10524,11019,10920,10240,10368,27,25,26])).
% 66.15/66.27 cnf(11384,plain,
% 66.15/66.27 (P4(f7(a4,a4),f6(a5),f6(a5))),
% 66.15/66.27 inference(scs_inference,[],[10806,11315,11261,11181,10543,10614,10522,10524,10726,11019,10920,10323,10306,10240,10368,27,25,26,29,30,23])).
% 66.15/66.27 cnf(11390,plain,
% 66.15/66.27 (~P2(f7(a4,a4),a4,f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11146,11363,11358,11196,11354,10458,10391,10327,10306,27,25,26])).
% 66.15/66.27 cnf(11392,plain,
% 66.15/66.27 (~P4(f6(a4),f3(a1,a1),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11247,11146,11363,11358,11196,11354,11079,10393,10616,10458,10391,10327,10306,27,25,26,29])).
% 66.15/66.27 cnf(11397,plain,
% 66.15/66.27 (~P2(f8(a4),f7(a4,a4),f7(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11027,10936,25])).
% 66.15/66.27 cnf(11399,plain,
% 66.15/66.27 (~P2(f6(a1),f6(a1),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11327,10625,11027,10936,25,26])).
% 66.15/66.27 cnf(11401,plain,
% 66.15/66.27 (~P4(a1,f8(a4),f7(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11327,11263,10625,11156,11027,10936,10992,3594,25,26,29])).
% 66.15/66.27 cnf(11415,plain,
% 66.15/66.27 (~P2(a4,a1,f3(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11378,11341,11401,11325,10438,10477,10260,10413,10770,10296,10980,10867,28,27,25,26])).
% 66.15/66.27 cnf(11433,plain,
% 66.15/66.27 (~P2(f6(a1),f3(a4,a4),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11390,11397,10670,11354,11073,25,26])).
% 66.15/66.27 cnf(11435,plain,
% 66.15/66.27 (~P4(f6(a1),f6(a5),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11390,11397,11384,10670,11354,11073,11118,25,26,29])).
% 66.15/66.27 cnf(11453,plain,
% 66.15/66.27 (~P2(f7(a4,a4),f7(a4,a4),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11433,10956,11287,11358,11158,11079,10413,10341,25,26,30])).
% 66.15/66.27 cnf(11475,plain,
% 66.15/66.27 (~P4(f8(a4),a4,f7(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[10969,10873,10558,28])).
% 66.15/66.27 cnf(11486,plain,
% 66.15/66.27 (P4(f6(a2),f7(a4,a4),f6(a2))),
% 66.15/66.27 inference(scs_inference,[],[10726,10368,27])).
% 66.15/66.27 cnf(11494,plain,
% 66.15/66.27 (P4(f7(a4,a4),f6(a2),f6(a2))),
% 66.15/66.27 inference(scs_inference,[],[11348,11415,11132,11166,10906,10516,10726,10865,10244,10368,3675,3597,27,26,29,30,23])).
% 66.15/66.27 cnf(11498,plain,
% 66.15/66.27 (~P4(a4,f7(a1,a1),a4)),
% 66.15/66.27 inference(scs_inference,[],[11475,10274,10859,27])).
% 66.15/66.27 cnf(11504,plain,
% 66.15/66.27 (~P2(f8(a4),a1,f7(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[11253,11494,11475,10883,10274,10460,10477,10875,10500,10873,10244,10859,27,26,29,30])).
% 66.15/66.27 cnf(11508,plain,
% 66.15/66.27 (~P4(f8(a4),f7(a1,a1),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11498,10867,28])).
% 66.15/66.27 cnf(11519,plain,
% 66.15/66.27 (~P4(a4,f3(a1,a1),a4)),
% 66.15/66.27 inference(scs_inference,[],[11114,10368,10558,28])).
% 66.15/66.27 cnf(11521,plain,
% 66.15/66.27 (~P4(f8(a4),f8(a4),f7(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[11114,11508,10893,10368,10558,28,27])).
% 66.15/66.27 cnf(11523,plain,
% 66.15/66.27 (~P2(f6(a1),f8(a4),f6(a1))),
% 66.15/66.27 inference(scs_inference,[],[11114,11086,11508,10242,10865,10893,10368,10558,28,27,25])).
% 66.15/66.27 cnf(11531,plain,
% 66.15/66.27 (~P4(a4,f7(a1,a1),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11521,10274,10859,27])).
% 66.15/66.27 cnf(11539,plain,
% 66.15/66.27 (~P2(f7(a4,a4),f6(a1),f6(a1))),
% 66.15/66.27 inference(scs_inference,[],[11392,11399,11521,11280,11144,10262,10274,10541,10893,10508,10374,10980,10744,10368,10859,27,26,29,28,30])).
% 66.15/66.27 cnf(11542,plain,
% 66.15/66.27 (~P4(f8(a4),f3(a1,a1),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11519,10867,28])).
% 66.15/66.27 cnf(11544,plain,
% 66.15/66.27 (~P4(f7(a1,a1),x115441,f7(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11519,11356,10701,10867,28,27])).
% 66.15/66.27 cnf(11546,plain,
% 66.15/66.27 (~P2(f8(a4),f6(a4),f7(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11453,11519,11356,10701,10875,10500,10867,28,27,26])).
% 66.15/66.27 cnf(11548,plain,
% 66.15/66.27 (~P4(f7(a4,a4),a1,f7(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11453,11519,11356,11378,10407,11358,10701,10875,10500,10238,10867,28,27,26,29])).
% 66.15/66.27 cnf(11555,plain,
% 66.15/66.27 (~P4(f7(a1,a1),x115551,f7(a4,a4))),
% 66.15/66.27 inference(rename_variables,[],[11544])).
% 66.15/66.27 cnf(11557,plain,
% 66.15/66.27 (~P4(f7(a4,a4),f7(a4,a4),a1)),
% 66.15/66.27 inference(scs_inference,[],[11544,11548,10774,10403,11158,28,27])).
% 66.15/66.27 cnf(11563,plain,
% 66.15/66.27 (~P2(f7(a1,a1),f7(a1,a1),f7(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11544,11555,11546,11548,10774,10403,11158,10914,11073,10592,10707,2020,28,27,26,29,30])).
% 66.15/66.27 cnf(11571,plain,
% 66.15/66.27 (~P2(f7(a1,a1),f3(a1,a1),f7(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[11563,11435,11544,10464,10494,10627,10541,10656,10992,10863,27,26,30])).
% 66.15/66.27 cnf(11582,plain,
% 66.15/66.27 (~P4(f6(a1),f7(a4,a4),f6(a4))),
% 66.15/66.27 inference(scs_inference,[],[11571,11539,11557,10660,10378,10834,11158,10477,10936,10242,25,26,30])).
% 66.15/66.27 cnf(11597,plain,
% 66.15/66.27 (~P4(f3(a1,a1),f8(a4),f8(a4))),
% 66.15/66.27 inference(scs_inference,[],[11267,11542,11504,11329,11544,11486,11152,10310,11148,11156,11173,10323,10967,10992,10893,10306,25,26,27,30,29])).
% 66.15/66.27 cnf(11621,plain,
% 66.15/66.27 (~P4(f8(a4),a4,f3(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[11597,11498,11415,11354,10873,10327,10558,10867,26,27,28])).
% 66.15/66.27 cnf(11646,plain,
% 66.15/66.27 (~P2(f7(a4,a4),f7(a1,a1),f7(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[11563,10268,10494,26])).
% 66.15/66.27 cnf(11655,plain,
% 66.15/66.27 (~P2(f7(a4,a4),a1,a1)),
% 66.15/66.27 inference(scs_inference,[],[11646,10440,25])).
% 66.15/66.27 cnf(11679,plain,
% 66.15/66.27 (~P2(f3(a1,a1),f3(a1,a1),f7(a4,a4))),
% 66.15/66.27 inference(scs_inference,[],[10808,11646,10530,10296,10341,25,26])).
% 66.15/66.27 cnf(11690,plain,
% 66.15/66.27 (~P2(f7(a4,a4),f7(a1,a1),f3(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[11679,10345,11646,10530,10477,25,26])).
% 66.15/66.27 cnf(11692,plain,
% 66.15/66.27 (~P4(a4,f8(a4),f7(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[11679,11531,10345,11646,10530,10477,10863,10558,25,26,27])).
% 66.15/66.27 cnf(11700,plain,
% 66.15/66.27 (~P2(f7(a4,a4),a1,f3(a1,a1))),
% 66.15/66.27 inference(scs_inference,[],[11690,10262,11019,25])).
% 66.15/66.27 cnf(11712,plain,
% 66.15/66.27 (P4(f6(a1),f7(a4,a4),f6(a1))),
% 66.15/66.27 inference(scs_inference,[],[10851,11700,10436,10834,10789,10306,10744,10368,25,26,27])).
% 66.15/66.27 cnf(11716,plain,
% 66.15/66.27 (P4(f7(a4,a4),f6(a1),f6(a1))),
% 66.15/66.27 inference(scs_inference,[],[10851,11700,11272,10436,10758,10834,10789,10458,10306,10744,10368,25,26,27,30,23])).
% 66.15/66.27 cnf(11722,plain,
% 66.15/66.27 (~P2(f6(a2),f3(a5,a5),a2)),
% 66.15/66.27 inference(scs_inference,[],[11071,11655,10304,11152,10358,25,26])).
% 66.15/66.27 cnf(11733,plain,
% 66.15/66.27 (~P2(a4,a2,a5)),
% 66.15/66.27 inference(scs_inference,[],[11192,11722,10986,10576,10789,10327,25,26])).
% 66.15/66.27 cnf(11735,plain,
% 66.15/66.27 (~P4(f6(a1),a4,f6(a4))),
% 66.15/66.27 inference(scs_inference,[],[11192,11582,11722,11712,10986,10576,10438,10789,10327,25,26,27])).
% 66.15/66.27 cnf(11757,plain,
% 66.15/66.27 (P2(f3(a1,a1),a2,a2)),
% 66.15/66.27 inference(scs_inference,[],[11733,11523,11692,11735,11621,11716,10343,10660,10616,10294,10920,10256,10417,10697,10238,10744,25,26,27,28,30,29,22])).
% 66.15/66.27 cnf(11828,plain,
% 66.15/66.27 ($false),
% 66.15/66.27 inference(scs_inference,[],[10984,11655,11757,10325,10262,10936,10789,10859,25,27,26]),
% 66.15/66.27 ['proof']).
% 66.15/66.27 % SZS output end Proof
% 66.15/66.27 % Total time :65.420000s
%------------------------------------------------------------------------------