%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD027-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 : n017.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:17 EDT 2024
% Result : Unsatisfiable 107.76s 107.84s
% Output : CNFRefutation 107.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : FLD027-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.06/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n017.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Wed Jun 19 11:04:24 EDT 2024
% 0.11/0.32 % CPUTime :
% 0.53/0.55 start to proof:theBenchmark
% 107.76/107.83 %-------------------------------------------
% 107.76/107.83 % File :CSE---1.7
% 107.76/107.83 % Problem :theBenchmark
% 107.76/107.83 % Transform :cnf
% 107.76/107.83 % Format :tptp:raw
% 107.76/107.83 % Command :java -jar mcs_scs.jar %d %s
% 107.76/107.83
% 107.76/107.83 % Result :Theorem 107.210000s
% 107.76/107.83 % Output :CNFRefutation 107.210000s
% 107.76/107.83 %-------------------------------------------
% 107.76/107.83 %--------------------------------------------------------------------------
% 107.76/107.83 % File : FLD027-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 107.76/107.83 % Domain : Field Theory (Ordered fields)
% 107.76/107.83 % Problem : Elimination of multiplicative inverses in an equation
% 107.76/107.83 % Version : [Dra93] axioms : Especial.
% 107.76/107.83 % Theorem formulation : Functional with re axiom set.
% 107.76/107.83 % English :
% 107.76/107.83
% 107.76/107.83 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 107.76/107.83 % Source : [Dra93]
% 107.76/107.83 % Names :
% 107.76/107.83
% 107.76/107.83 % Status : Unsatisfiable
% 107.76/107.83 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 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
% 107.76/107.83 % Syntax : Number of clauses : 32 ( 9 unt; 3 nHn; 32 RR)
% 107.76/107.83 % Number of literals : 83 ( 0 equ; 52 neg)
% 107.76/107.83 % Maximal clause size : 5 ( 2 avg)
% 107.76/107.83 % Maximal term depth : 2 ( 1 avg)
% 107.76/107.83 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 107.76/107.83 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 107.76/107.83 % Number of variables : 73 ( 0 sgn)
% 107.76/107.83 % SPC : CNF_UNS_RFO_NEQ_NHN
% 107.76/107.83
% 107.76/107.83 % Comments :
% 107.76/107.83 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 107.76/107.83 %--------------------------------------------------------------------------
% 107.76/107.83 include('Axioms/FLD002-0.ax').
% 107.76/107.83 %--------------------------------------------------------------------------
% 107.76/107.83 cnf(a_is_defined,hypothesis,
% 107.76/107.83 defined(a) ).
% 107.76/107.83
% 107.76/107.83 cnf(b_is_defined,hypothesis,
% 107.76/107.83 defined(b) ).
% 107.76/107.83
% 107.76/107.83 cnf(not_sum_3,negated_conjecture,
% 107.76/107.83 ~ sum(additive_identity,a,additive_identity) ).
% 107.76/107.83
% 107.76/107.83 cnf(not_sum_4,negated_conjecture,
% 107.76/107.84 ~ sum(additive_identity,b,additive_identity) ).
% 107.76/107.84
% 107.76/107.84 cnf(product_5,negated_conjecture,
% 107.76/107.84 product(multiplicative_identity,multiplicative_inverse(a),multiplicative_inverse(b)) ).
% 107.76/107.84
% 107.76/107.84 cnf(not_product_6,negated_conjecture,
% 107.76/107.84 ~ product(multiplicative_identity,a,b) ).
% 107.76/107.84
% 107.76/107.84 %--------------------------------------------------------------------------
% 107.76/107.84 %-------------------------------------------
% 107.76/107.84 % Proof found
% 107.76/107.84 % SZS status Theorem for theBenchmark
% 107.76/107.84 % SZS output start Proof
% 107.84/107.84 %ClaNum:32(EqnAxiom:0)
% 107.84/107.84 %VarNum:162(SingletonVarNum:73)
% 107.84/107.84 %MaxLitNum:5
% 107.84/107.84 %MaxfuncDepth:1
% 107.84/107.84 %SharedTerms:15
% 107.84/107.84 %goalClause: 5 7 8 9
% 107.84/107.84 %singleGoalClaCount:4
% 107.84/107.84 [1]P1(a1)
% 107.84/107.84 [2]P1(a4)
% 107.84/107.84 [3]P1(a2)
% 107.84/107.84 [4]P1(a5)
% 107.84/107.84 [6]~P4(a1,a1,a4)
% 107.84/107.84 [7]~P4(a1,a2,a1)
% 107.84/107.84 [8]~P4(a1,a5,a1)
% 107.84/107.84 [9]~P2(a4,a2,a5)
% 107.84/107.84 [5]P2(a4,f7(a2),f7(a5))
% 107.84/107.84 [15]~P1(x151)+P4(a1,x151,x151)
% 107.84/107.84 [16]~P1(x161)+P2(a4,x161,x161)
% 107.84/107.84 [10]~P1(x101)+P1(f6(x101))
% 107.84/107.84 [17]~P1(x171)+P4(f6(x171),x171,a1)
% 107.84/107.84 [24]~P4(x242,x241,x243)+P4(x241,x242,x243)
% 107.84/107.84 [25]~P2(x252,x251,x253)+P2(x251,x252,x253)
% 107.84/107.84 [18]~P1(x181)+P4(a1,x181,a1)+P1(f7(x181))
% 107.84/107.84 [22]~P1(x221)+P2(f7(x221),x221,a4)+P4(a1,x221,a1)
% 107.84/107.84 [21]~P3(x212,x211)+~P3(x211,x212)+P4(a1,x211,x212)
% 107.84/107.84 [12]~P1(x122)+~P1(x121)+P1(f3(x121,x122))
% 107.84/107.84 [13]~P1(x132)+~P1(x131)+P1(f8(x131,x132))
% 107.84/107.84 [19]~P1(x192)+~P1(x191)+P4(x191,x192,f3(x191,x192))
% 107.84/107.84 [20]~P1(x202)+~P1(x201)+P2(x201,x202,f8(x201,x202))
% 107.84/107.84 [14]~P3(x141,x143)+P3(x141,x142)+~P3(x143,x142)
% 107.84/107.84 [11]P3(x112,x111)+~P1(x111)+~P1(x112)+P3(x111,x112)
% 107.84/107.84 [23]~P2(x233,x232,x231)+P3(a1,x231)+~P3(a1,x232)+~P3(a1,x233)
% 107.84/107.84 [26]~P4(x263,x265,x261)+P3(x261,x262)+~P4(x264,x265,x262)+~P3(x263,x264)
% 107.84/107.84 [27]~P4(x271,x276,x274)+P4(x271,x272,x273)+~P4(x274,x275,x273)+~P4(x276,x275,x272)
% 107.84/107.84 [28]~P4(x286,x284,x281)+P4(x281,x282,x283)+~P4(x284,x282,x285)+~P4(x286,x285,x283)
% 107.84/107.84 [29]~P2(x291,x296,x294)+P2(x291,x292,x293)+~P2(x294,x295,x293)+~P2(x296,x295,x292)
% 107.84/107.84 [30]~P2(x306,x304,x301)+P2(x301,x302,x303)+~P2(x304,x302,x305)+~P2(x306,x305,x303)
% 107.84/107.84 [31]~P2(x315,x317,x312)+~P2(x314,x317,x311)+P4(x311,x312,x313)+~P4(x314,x315,x316)+~P2(x316,x317,x313)
% 107.84/107.84 [32]~P2(x327,x322,x325)+~P2(x326,x322,x324)+P2(x321,x322,x323)+~P4(x324,x325,x323)+~P4(x326,x327,x321)
% 107.84/107.84 %EqnAxiom
% 107.84/107.84
% 107.84/107.84 %-------------------------------------------
% 107.84/107.85 cnf(37,plain,
% 107.84/107.85 (P3(a1,a1)),
% 107.84/107.85 inference(scs_inference,[],[7,9,1,25,24,11])).
% 107.84/107.85 cnf(41,plain,
% 107.84/107.85 (~P2(x411,a4,a4)+P2(x411,f7(a5),f7(a5))),
% 107.84/107.85 inference(scs_inference,[],[5,7,9,1,25,24,11,21,29])).
% 107.84/107.85 cnf(43,plain,
% 107.84/107.85 (P2(f7(a5),x431,f7(a5))+~P2(f7(a2),x431,f7(a2))),
% 107.84/107.85 inference(scs_inference,[],[5,7,9,1,25,24,11,21,29,30])).
% 107.84/107.85 cnf(46,plain,
% 107.84/107.85 (~P4(a5,a1,a1)),
% 107.84/107.85 inference(scs_inference,[],[8,24])).
% 107.84/107.85 cnf(48,plain,
% 107.84/107.85 (P3(a4,a4)),
% 107.84/107.85 inference(scs_inference,[],[8,2,24,11])).
% 107.84/107.85 cnf(53,plain,
% 107.84/107.85 (P3(a2,a2)),
% 107.84/107.85 inference(scs_inference,[],[3,11])).
% 107.84/107.85 cnf(67,plain,
% 107.84/107.85 (~P4(a2,x671,x672)+~P4(a2,x671,x673)+P3(x672,x673)),
% 107.84/107.85 inference(scs_inference,[],[53,26])).
% 107.84/107.85 cnf(72,plain,
% 107.84/107.85 (~P4(a1,x721,x722)+~P4(a1,x721,x723)+P3(x722,x723)),
% 107.84/107.85 inference(scs_inference,[],[37,26])).
% 107.84/107.85 cnf(93,plain,
% 107.84/107.85 (P4(a1,f6(a4),f6(a4))),
% 107.84/107.85 inference(scs_inference,[],[2,15,10])).
% 107.84/107.85 cnf(115,plain,
% 107.84/107.85 (P2(a4,f6(a4),f6(a4))),
% 107.84/107.85 inference(scs_inference,[],[2,16,10])).
% 107.84/107.85 cnf(185,plain,
% 107.84/107.85 (P4(f6(f6(a5)),f6(a5),a1)),
% 107.84/107.85 inference(scs_inference,[],[4,17,10])).
% 107.84/107.85 cnf(186,plain,
% 107.84/107.85 (~P4(f6(a5),a5,f6(a5))),
% 107.84/107.85 inference(scs_inference,[],[8,185,28])).
% 107.84/107.85 cnf(188,plain,
% 107.84/107.85 (~P4(a5,f6(a5),f6(a5))),
% 107.84/107.85 inference(scs_inference,[],[8,185,28,24])).
% 107.84/107.85 cnf(191,plain,
% 107.84/107.85 (~P4(f6(a5),a2,f6(a5))),
% 107.84/107.85 inference(scs_inference,[],[7,185,28])).
% 107.84/107.85 cnf(193,plain,
% 107.84/107.85 (~P4(a2,f6(a5),f6(a5))),
% 107.84/107.85 inference(scs_inference,[],[7,185,28,24])).
% 107.84/107.85 cnf(225,plain,
% 107.84/107.85 (P2(f7(a5),x2251,f7(a5))+~P2(x2251,a4,a4)),
% 107.84/107.85 inference(scs_inference,[],[41,25])).
% 107.84/107.85 cnf(273,plain,
% 107.84/107.85 (P2(f7(a5),f7(a5),x2731)+~P2(f7(a5),f7(a2),x2731)+~P2(a4,a4,a4)),
% 107.84/107.85 inference(scs_inference,[],[5,225,29])).
% 107.84/107.85 cnf(352,plain,
% 107.84/107.85 (~P2(x3521,f7(a2),f7(a2))+P2(f7(a5),x3521,f7(a5))),
% 107.84/107.85 inference(scs_inference,[],[43,25])).
% 107.84/107.85 cnf(398,plain,
% 107.84/107.85 (P2(x3981,f7(a5),f7(a5))+~P2(x3981,f7(a2),f7(a2))),
% 107.84/107.85 inference(scs_inference,[],[352,25])).
% 107.84/107.85 cnf(414,plain,
% 107.84/107.85 (~P1(f7(a2))+P2(a4,f7(a5),f7(a5))),
% 107.84/107.85 inference(scs_inference,[],[398,16])).
% 107.84/107.85 cnf(430,plain,
% 107.84/107.85 (P2(a4,f7(a5),f7(a5))),
% 107.84/107.85 inference(scs_inference,[],[7,3,414,18])).
% 107.84/107.85 cnf(698,plain,
% 107.84/107.85 (~P2(f7(a5),f7(a2),x6981)+P2(f7(a5),f7(a5),x6981)),
% 107.84/107.85 inference(scs_inference,[],[2,273,16])).
% 107.84/107.85 cnf(803,plain,
% 107.84/107.85 (~P4(x8031,a4,x8032)+~P2(x8031,f6(a4),a1)+P4(f6(a4),f6(a4),f6(a4))+~P4(a4,a4,x8032)),
% 107.84/107.85 inference(scs_inference,[],[93,115,48,32,31])).
% 107.84/107.85 cnf(845,plain,
% 107.84/107.85 (~P2(a4,a4,x8451)+P2(x8451,f7(a5),f7(a5))),
% 107.84/107.85 inference(scs_inference,[],[430,30])).
% 107.84/107.85 cnf(1257,plain,
% 107.84/107.85 (P4(a1,f6(a1),f6(a1))),
% 107.84/107.85 inference(scs_inference,[],[1,10,15])).
% 107.84/107.85 cnf(1263,plain,
% 107.84/107.85 (~P4(x12631,a1,a1)+P4(x12631,f6(a1),f6(a1))),
% 107.84/107.85 inference(scs_inference,[],[1257,27])).
% 107.84/107.85 cnf(1285,plain,
% 107.84/107.85 (P4(f6(a1),x12851,f6(a1))+~P4(x12851,a1,a1)),
% 107.84/107.85 inference(scs_inference,[],[1263,24])).
% 107.84/107.85 cnf(1515,plain,
% 107.84/107.85 (~P4(x15151,f6(f6(a5)),a5)+~P4(x15151,a1,f6(a5))),
% 107.84/107.85 inference(scs_inference,[],[46,185,28,24])).
% 107.84/107.85 cnf(1634,plain,
% 107.84/107.85 (P4(a1,f6(a2),f6(a2))),
% 107.84/107.85 inference(scs_inference,[],[3,10,15])).
% 107.84/107.85 cnf(1750,plain,
% 107.84/107.85 (P2(a4,f6(a2),f6(a2))),
% 107.84/107.85 inference(scs_inference,[],[3,10,16])).
% 107.84/107.85 cnf(1751,plain,
% 107.84/107.85 (~P2(a4,a4,x17511)+P2(x17511,f6(a2),f6(a2))),
% 107.84/107.85 inference(scs_inference,[],[1750,30])).
% 107.84/107.85 cnf(1753,plain,
% 107.84/107.85 (~P2(x17531,a4,a4)+P2(x17531,f6(a2),f6(a2))),
% 107.84/107.85 inference(scs_inference,[],[1750,30,29])).
% 107.84/107.85 cnf(1771,plain,
% 107.84/107.85 (P2(f6(a2),x17711,f6(a2))+~P2(a4,a4,x17711)),
% 107.84/107.85 inference(scs_inference,[],[1751,25])).
% 107.84/107.85 cnf(1787,plain,
% 107.84/107.85 (P2(f6(a2),x17871,f6(a2))+~P2(x17871,a4,a4)),
% 107.84/107.85 inference(scs_inference,[],[1753,25])).
% 107.84/107.85 cnf(1803,plain,
% 107.84/107.85 (~P2(f6(a2),a4,x18031)+P2(x18031,f7(a2),f6(a2))+~P2(a4,a4,f7(a5))),
% 107.84/107.85 inference(scs_inference,[],[5,1771,30])).
% 107.84/107.85 cnf(1819,plain,
% 107.84/107.85 (~P2(f6(a2),a4,x18191)+P2(x18191,f7(a2),f6(a2))+~P2(f7(a5),a4,a4)),
% 107.84/107.85 inference(scs_inference,[],[5,1787,30])).
% 107.84/107.85 cnf(1915,plain,
% 107.84/107.85 (~P2(a4,f7(a5),a4)+P2(x19151,f7(a2),f6(a2))+~P2(f6(a2),a4,x19151)),
% 107.84/107.85 inference(scs_inference,[],[1819,25])).
% 107.84/107.85 cnf(2136,plain,
% 107.84/107.85 (P4(f6(f6(a4)),f6(a4),a1)),
% 107.84/107.85 inference(scs_inference,[],[2,10,17])).
% 107.84/107.85 cnf(2139,plain,
% 107.84/107.85 (~P4(a2,f6(a4),f6(a4))),
% 107.84/107.85 inference(scs_inference,[],[7,2136,28,24])).
% 107.84/107.85 cnf(2147,plain,
% 107.84/107.85 (~P4(a5,f6(a4),f6(a4))),
% 107.84/107.85 inference(scs_inference,[],[8,2136,28,24])).
% 107.84/107.85 cnf(2180,plain,
% 107.84/107.85 (P4(a1,f6(a5),f6(a5))),
% 107.84/107.85 inference(scs_inference,[],[4,10,15])).
% 107.84/107.85 cnf(2198,plain,
% 107.84/107.85 (P2(a4,f6(a1),f6(a1))),
% 107.84/107.85 inference(scs_inference,[],[1,10,16])).
% 107.84/107.85 cnf(2199,plain,
% 107.84/107.85 (~P2(a4,a4,x21991)+P2(x21991,f6(a1),f6(a1))),
% 107.84/107.85 inference(scs_inference,[],[2198,30])).
% 107.84/107.85 cnf(2201,plain,
% 107.84/107.85 (~P2(x22011,a4,a4)+P2(x22011,f6(a1),f6(a1))),
% 107.84/107.85 inference(scs_inference,[],[2198,30,29])).
% 107.84/107.85 cnf(2219,plain,
% 107.84/107.85 (P2(f6(a1),x22191,f6(a1))+~P2(a4,a4,x22191)),
% 107.84/107.85 inference(scs_inference,[],[2199,25])).
% 107.84/107.85 cnf(2235,plain,
% 107.84/107.85 (P2(f6(a1),x22351,f6(a1))+~P2(x22351,a4,a4)),
% 107.84/107.85 inference(scs_inference,[],[2201,25])).
% 107.84/107.85 cnf(2251,plain,
% 107.84/107.86 (~P2(f6(a1),a4,x22511)+P2(x22511,f7(a2),f6(a1))+~P2(a4,a4,f7(a5))),
% 107.84/107.86 inference(scs_inference,[],[5,2219,30])).
% 107.84/107.86 cnf(2267,plain,
% 107.84/107.86 (~P2(f6(a1),a4,x22671)+P2(x22671,f7(a2),f6(a1))+~P2(f7(a5),a4,a4)),
% 107.84/107.86 inference(scs_inference,[],[5,2235,30])).
% 107.84/107.86 cnf(2422,plain,
% 107.84/107.86 (~P4(f6(a4),x24221,a2)+~P4(f6(a4),x24221,a1)),
% 107.84/107.86 inference(scs_inference,[],[7,93,27])).
% 107.84/107.86 cnf(2430,plain,
% 107.84/107.86 (~P4(f6(a4),x24301,a1)+~P4(f6(a4),x24301,a4)),
% 107.84/107.86 inference(scs_inference,[],[93,6,27])).
% 107.84/107.86 cnf(2435,plain,
% 107.84/107.86 (~P4(f6(a4),a4,a2)),
% 107.84/107.86 inference(scs_inference,[],[2,2422,17])).
% 107.84/107.86 cnf(2438,plain,
% 107.84/107.86 (~P4(x24381,f6(a5),a5)+~P4(f6(a5),x24381,a1)),
% 107.84/107.86 inference(scs_inference,[],[186,2180,2435,24,27])).
% 107.84/107.86 cnf(2446,plain,
% 107.84/107.86 (~P4(x24461,f6(a5),a2)+~P4(f6(a5),x24461,a1)),
% 107.84/107.86 inference(scs_inference,[],[191,2180,27])).
% 107.84/107.86 cnf(2492,plain,
% 107.84/107.86 (~P2(x24921,f6(a4),a2)+~P4(x24921,a4,a4)),
% 107.84/107.86 inference(scs_inference,[],[115,2139,31])).
% 107.84/107.86 cnf(2497,plain,
% 107.84/107.86 (~P2(x24971,f6(a4),a5)+~P4(x24971,a4,a4)),
% 107.84/107.86 inference(scs_inference,[],[115,2147,31])).
% 107.84/107.86 cnf(2515,plain,
% 107.84/107.86 (~P2(x25151,a4,x25152)+~P2(x25152,f6(a4),a2)+~P4(x25151,a4,a4)),
% 107.84/107.86 inference(scs_inference,[],[115,2492,29])).
% 107.84/107.86 cnf(2524,plain,
% 107.84/107.86 (~P4(f6(a2),x25241,a2)+~P4(f6(a2),x25241,a1)),
% 107.84/107.86 inference(scs_inference,[],[7,1634,27])).
% 107.84/107.86 cnf(2530,plain,
% 107.84/107.86 (~P4(f6(a2),x25301,a5)+~P4(f6(a2),x25301,a1)),
% 107.84/107.86 inference(scs_inference,[],[8,1634,27])).
% 107.84/107.86 cnf(2559,plain,
% 107.84/107.86 (~P2(x25591,a4,x25592)+~P2(x25592,f6(a4),a5)+~P4(x25591,a4,a4)),
% 107.84/107.86 inference(scs_inference,[],[115,2497,29])).
% 107.84/107.86 cnf(2702,plain,
% 107.84/107.86 (~P4(x27021,f6(a4),a4)+~P4(f6(a4),x27021,a1)),
% 107.84/107.86 inference(scs_inference,[],[2430,24])).
% 107.84/107.86 cnf(2734,plain,
% 107.84/107.86 (~P4(a5,f6(a5),a5)),
% 107.84/107.86 inference(scs_inference,[],[4,2438,17])).
% 107.84/107.86 cnf(2735,plain,
% 107.84/107.86 (~P4(f6(a5),a5,a5)),
% 107.84/107.86 inference(scs_inference,[],[2734,24])).
% 107.84/107.86 cnf(2786,plain,
% 107.84/107.86 (~P4(a5,f6(a5),a2)),
% 107.84/107.86 inference(scs_inference,[],[4,2446,17])).
% 107.84/107.86 cnf(2787,plain,
% 107.84/107.86 (~P4(f6(a5),a5,a2)),
% 107.84/107.86 inference(scs_inference,[],[2786,24])).
% 107.84/107.86 cnf(2838,plain,
% 107.84/107.86 (~P4(f6(a2),a2,a2)),
% 107.84/107.86 inference(scs_inference,[],[3,2524,17])).
% 107.84/107.86 cnf(2841,plain,
% 107.84/107.86 (~P4(a2,a1,x28411)+~P4(x28411,f6(a2),a2)),
% 107.84/107.86 inference(scs_inference,[],[1634,2838,24,27])).
% 107.84/107.86 cnf(2858,plain,
% 107.84/107.86 (~P4(f6(a2),x28581,a2)+~P4(a2,a1,x28581)),
% 107.84/107.86 inference(scs_inference,[],[2841,24])).
% 107.84/107.86 cnf(2906,plain,
% 107.84/107.86 (~P4(f6(a2),a2,a5)),
% 107.84/107.86 inference(scs_inference,[],[3,2530,17])).
% 107.84/107.86 cnf(2937,plain,
% 107.84/107.86 (~P4(f6(a1),x29371,a5)+~P4(f6(a1),x29371,a1)),
% 107.84/107.86 inference(scs_inference,[],[8,1257,27])).
% 107.84/107.86 cnf(2942,plain,
% 107.84/107.86 (~P4(f6(a1),x29421,a2)+~P4(f6(a1),x29421,a1)),
% 107.84/107.86 inference(scs_inference,[],[7,1257,27])).
% 107.84/107.86 cnf(2947,plain,
% 107.84/107.86 (~P4(f6(a1),x29471,a1)+~P4(f6(a1),x29471,a4)),
% 107.84/107.86 inference(scs_inference,[],[1257,6,27])).
% 107.84/107.86 cnf(3034,plain,
% 107.84/107.86 (~P4(a4,f6(a4),a4)),
% 107.84/107.86 inference(scs_inference,[],[2,2702,17])).
% 107.84/107.86 cnf(3035,plain,
% 107.84/107.86 (~P4(f6(a4),a4,a4)),
% 107.84/107.86 inference(scs_inference,[],[3034,24])).
% 107.84/107.86 cnf(3037,plain,
% 107.84/107.86 (~P4(a4,a1,x30371)+~P4(x30371,f6(a4),a4)),
% 107.84/107.86 inference(scs_inference,[],[3034,93,24,27])).
% 107.84/107.86 cnf(3058,plain,
% 107.84/107.86 (~P4(f6(a4),x30581,a4)+~P4(a4,a1,x30581)),
% 107.84/107.86 inference(scs_inference,[],[3037,24])).
% 107.84/107.86 cnf(3106,plain,
% 107.84/107.86 (~P4(f6(a1),a1,a5)),
% 107.84/107.86 inference(scs_inference,[],[1,2937,17])).
% 107.84/107.86 cnf(3107,plain,
% 107.84/107.86 (~P4(a1,f6(a1),a5)),
% 107.84/107.86 inference(scs_inference,[],[3106,24])).
% 107.84/107.86 cnf(3170,plain,
% 107.84/107.86 (~P4(f6(a1),a1,a2)),
% 107.84/107.86 inference(scs_inference,[],[1,2942,17])).
% 107.84/107.86 cnf(3171,plain,
% 107.84/107.86 (~P4(a1,f6(a1),a2)),
% 107.84/107.86 inference(scs_inference,[],[3170,24])).
% 107.84/107.86 cnf(3234,plain,
% 107.84/107.86 (~P4(x32341,f6(a1),a4)+~P4(f6(a1),x32341,a1)),
% 107.84/107.86 inference(scs_inference,[],[2947,24])).
% 107.84/107.86 cnf(3240,plain,
% 107.84/107.86 (~P4(f7(a5),f7(a5),x32401)+~P4(a4,a4,x32402)+P2(x32402,f7(a5),x32401)),
% 107.84/107.86 inference(scs_inference,[],[430,2787,53,32])).
% 107.84/107.86 cnf(3350,plain,
% 107.84/107.86 (~P4(a1,f6(a1),a4)),
% 107.84/107.86 inference(scs_inference,[],[1,3234,17])).
% 107.84/107.86 cnf(3351,plain,
% 107.84/107.86 (~P4(f6(a1),a1,a4)),
% 107.84/107.86 inference(scs_inference,[],[3350,24])).
% 107.84/107.86 cnf(3692,plain,
% 107.84/107.86 (P4(f6(a2),a1,f6(a2))),
% 107.84/107.86 inference(scs_inference,[],[1634,24])).
% 107.84/107.86 cnf(3694,plain,
% 107.84/107.86 (P4(f6(a2),x36941,f6(a2))+~P4(a1,x36941,a1)),
% 107.84/107.86 inference(scs_inference,[],[1634,24,28])).
% 107.84/107.86 cnf(3698,plain,
% 107.84/107.86 (P4(f6(a1),a1,f6(a1))),
% 107.84/107.86 inference(scs_inference,[],[1257,24])).
% 107.84/107.86 cnf(3700,plain,
% 107.84/107.86 (P4(f6(a1),x37001,f6(a1))+~P4(a1,x37001,a1)),
% 107.84/107.86 inference(scs_inference,[],[1257,24,28])).
% 107.84/107.86 cnf(3717,plain,
% 107.84/107.86 (P4(f6(a4),a1,f6(a4))),
% 107.84/107.86 inference(scs_inference,[],[93,24])).
% 107.84/107.86 cnf(3725,plain,
% 107.84/107.86 (P4(f6(a5),a1,f6(a5))),
% 107.84/107.86 inference(scs_inference,[],[2180,24])).
% 107.84/107.86 cnf(3731,plain,
% 107.84/107.86 (~P4(a1,x37311,a4)+~P4(f6(a4),x37311,a4)),
% 107.84/107.86 inference(scs_inference,[],[3035,193,3717,185,2180,24,28,1515,27])).
% 107.84/107.86 cnf(3827,plain,
% 107.84/107.86 (~P4(a1,x38271,a2)+~P4(f6(a2),x38271,a2)),
% 107.84/107.86 inference(scs_inference,[],[3692,2838,27])).
% 107.84/107.86 cnf(3949,plain,
% 107.84/107.86 (P2(f7(a2),a4,f7(a5))),
% 107.84/107.86 inference(scs_inference,[],[5,25])).
% 107.84/107.86 cnf(3956,plain,
% 107.84/107.86 (P2(f7(a5),a4,f7(a5))),
% 107.84/107.86 inference(scs_inference,[],[430,25])).
% 107.84/107.86 cnf(3963,plain,
% 107.84/107.86 (P2(f6(a4),a4,f6(a4))),
% 107.84/107.86 inference(scs_inference,[],[115,25])).
% 107.84/107.86 cnf(3974,plain,
% 107.84/107.86 (P2(f6(a1),a4,f6(a1))),
% 107.84/107.86 inference(scs_inference,[],[2198,25])).
% 107.84/107.86 cnf(3976,plain,
% 107.84/107.86 (~P2(a1,a4,a5)),
% 107.84/107.86 inference(scs_inference,[],[2147,3963,2198,93,25,31])).
% 107.84/107.86 cnf(3988,plain,
% 107.84/107.86 (P2(f6(a2),a4,f6(a2))),
% 107.84/107.86 inference(scs_inference,[],[1750,25])).
% 107.84/107.86 cnf(3990,plain,
% 107.84/107.86 (~P2(a1,a4,a2)),
% 107.84/107.86 inference(scs_inference,[],[2139,3963,1750,93,25,31])).
% 107.84/107.86 cnf(3998,plain,
% 107.84/107.86 (P2(f7(a2),f6(a1),x39981)+~P2(f7(a5),f6(a1),x39981)),
% 107.84/107.86 inference(scs_inference,[],[2139,3949,3963,2198,1750,93,25,31,1915,1803,1819,29])).
% 107.84/107.86 cnf(4026,plain,
% 107.84/107.86 (P2(f6(a1),f7(a5),x40261)+~P2(f6(a1),f7(a2),x40261)),
% 107.84/107.86 inference(scs_inference,[],[5,3974,29])).
% 107.84/107.86 cnf(4048,plain,
% 107.84/107.86 (~P2(f6(a1),a4,a4)+~P2(a1,a4,a1)),
% 107.84/107.86 inference(scs_inference,[],[3351,3698,3974,31])).
% 107.84/107.86 cnf(4054,plain,
% 107.84/107.86 (~P2(f6(a1),a4,a2)+~P2(a1,a4,a1)),
% 107.84/107.86 inference(scs_inference,[],[1257,3171,3974,31])).
% 107.84/107.86 cnf(4073,plain,
% 107.84/107.86 (~P2(f6(a1),a4,a5)+~P2(a1,a4,a1)),
% 107.84/107.86 inference(scs_inference,[],[1257,3107,3974,31])).
% 107.84/107.86 cnf(4422,plain,
% 107.84/107.86 (~P2(a1,a4,a1)+~P2(a4,f6(a1),a4)),
% 107.84/107.86 inference(scs_inference,[],[4048,25])).
% 107.84/107.86 cnf(4438,plain,
% 107.84/107.86 (~P2(a1,a4,a1)+~P2(a4,f6(a1),a2)),
% 107.84/107.86 inference(scs_inference,[],[4054,25])).
% 107.84/107.86 cnf(4518,plain,
% 107.84/107.86 (~P2(a1,a4,a1)+~P2(a4,f6(a1),a5)),
% 107.84/107.86 inference(scs_inference,[],[4073,25])).
% 107.84/107.86 cnf(4759,plain,
% 107.84/107.86 (~P2(a4,a1,a1)+~P2(a4,f6(a1),a4)),
% 107.84/107.86 inference(scs_inference,[],[4422,25])).
% 107.84/107.86 cnf(4775,plain,
% 107.84/107.86 (~P2(a4,a1,a1)+~P2(a4,f6(a1),a2)),
% 107.84/107.86 inference(scs_inference,[],[4438,25])).
% 107.84/107.86 cnf(4921,plain,
% 107.84/107.86 (~P2(a4,f6(a1),a4)),
% 107.84/107.86 inference(scs_inference,[],[1,4759,16])).
% 107.84/107.86 cnf(4922,plain,
% 107.84/107.86 (~P2(f6(a1),a4,a4)),
% 107.84/107.86 inference(scs_inference,[],[4921,3974,2198,29])).
% 107.84/107.86 cnf(4951,plain,
% 107.84/107.86 (~P2(f6(a1),a4,a2)+~P2(a4,a1,a1)),
% 107.84/107.86 inference(scs_inference,[],[4775,25])).
% 107.84/107.86 cnf(5103,plain,
% 107.84/107.86 (P4(x51031,f6(a2),f6(a2))+~P4(a1,x51031,a1)),
% 107.84/107.86 inference(scs_inference,[],[3694,24])).
% 107.84/107.86 cnf(5603,plain,
% 107.84/107.86 (~P2(f6(a2),x56031,f6(a4))+~P2(x56032,x56031,a2)+~P4(a1,x56032,a1)),
% 107.84/107.86 inference(scs_inference,[],[2139,5103,31])).
% 107.84/107.86 cnf(6402,plain,
% 107.84/107.86 (P1(f6(a5))),
% 107.84/107.86 inference(scs_inference,[],[4,10])).
% 107.84/107.86 cnf(6404,plain,
% 107.84/107.86 (P2(a4,a5,a5)),
% 107.84/107.86 inference(scs_inference,[],[4,10,16])).
% 107.84/107.86 cnf(6406,plain,
% 107.84/107.86 (P4(a1,a5,a5)),
% 107.84/107.86 inference(scs_inference,[],[4,10,16,15])).
% 107.84/107.86 cnf(6408,plain,
% 107.84/107.86 (P4(f6(a5),a5,a1)),
% 107.84/107.86 inference(scs_inference,[],[4,10,16,15,17])).
% 107.84/107.86 cnf(6410,plain,
% 107.84/107.86 (~P2(a4,a1,a5)),
% 107.84/107.86 inference(scs_inference,[],[3976,4,10,16,15,17,25])).
% 107.84/107.86 cnf(6412,plain,
% 107.84/107.86 (P1(f3(a5,a5))),
% 107.84/107.86 inference(scs_inference,[],[3976,4,10,16,15,17,25,12])).
% 107.84/107.86 cnf(6414,plain,
% 107.84/107.86 (P1(f8(a5,a5))),
% 107.84/107.86 inference(scs_inference,[],[3976,4,10,16,15,17,25,12,13])).
% 107.84/107.86 cnf(6416,plain,
% 107.84/107.86 (P2(a5,a5,f8(a5,a5))),
% 107.84/107.86 inference(scs_inference,[],[3976,4,10,16,15,17,25,12,13,20])).
% 107.84/107.86 cnf(6418,plain,
% 107.84/107.86 (P1(f7(a5))),
% 107.84/107.86 inference(scs_inference,[],[3976,4,8,10,16,15,17,25,12,13,20,18])).
% 107.84/107.86 cnf(6420,plain,
% 107.84/107.86 (P4(a5,a5,f3(a5,a5))),
% 107.84/107.86 inference(scs_inference,[],[3976,4,8,10,16,15,17,25,12,13,20,18,19])).
% 107.84/107.86 cnf(6422,plain,
% 107.84/107.86 (P2(f7(a5),a5,a4)),
% 107.84/107.86 inference(scs_inference,[],[3976,4,8,10,16,15,17,25,12,13,20,18,19,22])).
% 107.84/107.86 cnf(6424,plain,
% 107.84/107.86 (P4(a1,a1,a1)),
% 107.84/107.86 inference(scs_inference,[],[3976,4,37,8,10,16,15,17,25,12,13,20,18,19,22,21])).
% 107.84/107.86 cnf(6426,plain,
% 107.84/107.86 (P2(f7(a5),f8(a5,a5),a5)),
% 107.84/107.86 inference(scs_inference,[],[3976,4,37,8,10,16,15,17,25,12,13,20,18,19,22,21,29])).
% 107.84/107.86 cnf(6428,plain,
% 107.84/107.86 (~P2(a5,f6(a1),a5)),
% 107.84/107.86 inference(scs_inference,[],[3976,4921,4,37,8,10,16,15,17,25,12,13,20,18,19,22,21,29,30])).
% 107.84/107.86 cnf(6430,plain,
% 107.84/107.86 (~P4(a1,a1,f6(a5))),
% 107.84/107.86 inference(scs_inference,[],[3976,4921,186,4,37,8,2180,10,16,15,17,25,12,13,20,18,19,22,21,29,30,28])).
% 107.84/107.86 cnf(6432,plain,
% 107.84/107.86 (P4(a1,f3(a5,a5),f3(a5,a5))),
% 107.84/107.86 inference(scs_inference,[],[3976,4921,186,4,37,8,2180,10,16,15,17,25,12,13,20,18,19,22,21,29,30,28,27])).
% 107.84/107.86 cnf(6446,plain,
% 107.84/107.86 (P4(a1,f8(a5,a5),f8(a5,a5))),
% 107.84/107.86 inference(scs_inference,[],[6412,6414,1,16,10,15])).
% 107.84/107.86 cnf(6448,plain,
% 107.84/107.86 (P4(f6(a1),a1,a1)),
% 107.84/107.86 inference(scs_inference,[],[6412,6414,1,16,10,15,17])).
% 107.84/107.86 cnf(6450,plain,
% 107.84/107.86 (~P2(a4,a1,a2)),
% 107.84/107.86 inference(scs_inference,[],[3990,6412,6414,1,16,10,15,17,25])).
% 107.84/107.86 cnf(6452,plain,
% 107.84/107.86 (P1(f7(a2))),
% 107.84/107.86 inference(scs_inference,[],[3990,6412,6414,1,3,7,16,10,15,17,25,18])).
% 107.84/107.86 cnf(6454,plain,
% 107.84/107.86 (P2(a1,a1,f8(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[3990,6412,6414,1,3,7,16,10,15,17,25,18,20])).
% 107.84/107.86 cnf(6456,plain,
% 107.84/107.86 (P1(f8(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[3990,6412,6414,1,3,7,16,10,15,17,25,18,20,13])).
% 107.84/107.86 cnf(6458,plain,
% 107.84/107.86 (P1(f3(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[3990,6412,6414,1,3,7,16,10,15,17,25,18,20,13,12])).
% 107.84/107.86 cnf(6460,plain,
% 107.84/107.86 (P4(a1,a1,f3(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[3990,6412,6414,1,3,7,16,10,15,17,25,18,20,13,12,19])).
% 107.84/107.86 cnf(6462,plain,
% 107.84/107.86 (P2(f7(a2),a2,a4)),
% 107.84/107.86 inference(scs_inference,[],[3990,6412,6414,1,3,7,16,10,15,17,25,18,20,13,12,19,22])).
% 107.84/107.86 cnf(6464,plain,
% 107.84/107.86 (P4(a1,a4,a4)),
% 107.84/107.86 inference(scs_inference,[],[3990,6412,6414,1,3,7,48,16,10,15,17,25,18,20,13,12,19,22,21])).
% 107.84/107.86 cnf(6466,plain,
% 107.84/107.86 (P3(a1,f8(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[3990,6412,6414,1,3,37,7,48,16,10,15,17,25,18,20,13,12,19,22,21,23])).
% 107.84/107.86 cnf(6468,plain,
% 107.84/107.86 (~P2(f8(a5,a5),f6(a1),f8(a5,a5))),
% 107.84/107.86 inference(scs_inference,[],[3990,6412,6414,6426,6428,1,3,37,7,48,16,10,15,17,25,18,20,13,12,19,22,21,23,30])).
% 107.84/107.86 cnf(6470,plain,
% 107.84/107.86 (~P2(f7(a2),f8(a5,a5),a1)),
% 107.84/107.86 inference(scs_inference,[],[5,3990,6410,6412,6414,6426,6428,1,3,37,7,48,16,10,15,17,25,18,20,13,12,19,22,21,23,30,29])).
% 107.84/107.86 cnf(6474,plain,
% 107.84/107.86 (P4(a1,f3(a1,a1),f3(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[5,3990,6424,6410,6412,6414,6426,6420,6408,6428,1,3,37,8,7,48,16,10,15,17,25,18,20,13,12,19,22,21,23,30,29,28,27])).
% 107.84/107.86 cnf(6478,plain,
% 107.84/107.86 (P4(f8(a1,a1),f8(a1,a1),f8(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[5,3990,6424,6410,6412,6414,6426,6420,6408,6428,1,3,37,8,7,48,16,10,15,17,25,18,20,13,12,19,22,21,23,30,29,28,27,26,31])).
% 107.84/107.86 cnf(6490,plain,
% 107.84/107.86 (P2(a4,f8(a1,a1),f8(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[6456,2,10,16])).
% 107.84/107.86 cnf(6492,plain,
% 107.84/107.86 (P4(f6(a4),a4,a1)),
% 107.84/107.86 inference(scs_inference,[],[6456,2,10,16,17])).
% 107.84/107.86 cnf(6494,plain,
% 107.84/107.86 (P4(a1,f8(a1,a1),f8(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[6456,2,10,16,17,15])).
% 107.84/107.86 cnf(6498,plain,
% 107.84/107.86 (P1(f8(a4,a4))),
% 107.84/107.86 inference(scs_inference,[],[6456,6468,2,10,16,17,15,25,13])).
% 107.84/107.86 cnf(6500,plain,
% 107.84/107.86 (P2(a4,a4,f8(a4,a4))),
% 107.84/107.86 inference(scs_inference,[],[6456,6468,2,10,16,17,15,25,13,20])).
% 107.84/107.86 cnf(6502,plain,
% 107.84/107.86 (P1(f3(a4,a4))),
% 107.84/107.86 inference(scs_inference,[],[6456,6468,2,10,16,17,15,25,13,20,12])).
% 107.84/107.86 cnf(6504,plain,
% 107.84/107.86 (P4(a4,a4,f3(a4,a4))),
% 107.84/107.86 inference(scs_inference,[],[6456,6468,2,10,16,17,15,25,13,20,12,19])).
% 107.84/107.86 cnf(6506,plain,
% 107.84/107.86 (P4(a1,a2,a2)),
% 107.84/107.86 inference(scs_inference,[],[6456,6468,2,53,10,16,17,15,25,13,20,12,19,21])).
% 107.84/107.86 cnf(6508,plain,
% 107.84/107.86 (~P2(a5,f7(a5),f6(a1))),
% 107.84/107.86 inference(scs_inference,[],[6456,6468,6416,6426,2,53,10,16,17,15,25,13,20,12,19,21,30])).
% 107.84/107.86 cnf(6510,plain,
% 107.84/107.86 (~P2(f6(a1),f7(a5),f7(a5))),
% 107.84/107.86 inference(scs_inference,[],[4922,6456,6468,6416,6422,6426,2,53,10,16,17,15,25,13,20,12,19,21,30,29])).
% 107.84/107.86 cnf(6512,plain,
% 107.84/107.86 (P4(f3(a1,a1),a4,a4)),
% 107.84/107.86 inference(scs_inference,[],[6464,4922,6456,6468,6460,6416,6422,6426,2,53,10,16,17,15,25,13,20,12,19,21,30,29,28])).
% 107.84/107.86 cnf(6514,plain,
% 107.84/107.86 (P4(a1,f3(a4,a4),f3(a4,a4))),
% 107.84/107.86 inference(scs_inference,[],[6464,4922,6456,6468,6460,6416,6422,6426,2,53,10,16,17,15,25,13,20,12,19,21,30,29,28,27])).
% 107.84/107.86 cnf(6516,plain,
% 107.84/107.86 (~P2(a1,a5,f6(a5))),
% 107.84/107.86 inference(scs_inference,[],[6404,6464,4922,6456,6468,6460,6416,6422,6426,2,53,2735,10,16,17,15,25,13,20,12,19,21,30,29,28,27,31])).
% 107.84/107.86 cnf(6518,plain,
% 107.84/107.86 (~P2(a4,a4,f6(a1))),
% 107.84/107.86 inference(scs_inference,[],[6404,6464,4922,6456,6468,6460,6416,6422,6426,2,53,2735,10,16,17,15,25,13,20,12,19,21,30,29,28,27,31,845])).
% 107.84/107.86 cnf(6522,plain,
% 107.84/107.86 (~P2(f6(a1),f7(a2),f7(a5))),
% 107.84/107.86 inference(scs_inference,[],[6404,6464,4922,6456,6468,6460,6416,6422,6426,2,53,2735,10,16,17,15,25,13,20,12,19,21,30,29,28,27,31,845,398,4026])).
% 107.84/107.86 cnf(6535,plain,
% 107.84/107.86 (P2(a4,f3(a4,a4),f3(a4,a4))),
% 107.84/107.86 inference(scs_inference,[],[6502,16])).
% 107.84/107.86 cnf(6539,plain,
% 107.84/107.86 (P4(a1,f7(a5),f7(a5))),
% 107.84/107.86 inference(scs_inference,[],[6502,6418,3,16,10,15])).
% 107.84/107.86 cnf(6541,plain,
% 107.84/107.86 (P4(f6(a2),a2,a1)),
% 107.84/107.86 inference(scs_inference,[],[6502,6418,3,16,10,15,17])).
% 107.84/107.86 cnf(6543,plain,
% 107.84/107.86 (~P2(f7(a5),f6(a1),f7(a5))),
% 107.84/107.86 inference(scs_inference,[],[6502,6418,6510,3,16,10,15,17,25])).
% 107.84/107.86 cnf(6547,plain,
% 107.84/107.86 (P1(f3(a2,a2))),
% 107.84/107.86 inference(scs_inference,[],[6502,6418,6510,3,16,10,15,17,25,20,12])).
% 107.84/107.86 cnf(6549,plain,
% 107.84/107.86 (P1(f8(a2,a2))),
% 107.84/107.86 inference(scs_inference,[],[6502,6418,6510,3,16,10,15,17,25,20,12,13])).
% 107.84/107.86 cnf(6551,plain,
% 107.84/107.86 (P4(a2,a2,f3(a2,a2))),
% 107.84/107.86 inference(scs_inference,[],[6502,6418,6510,3,16,10,15,17,25,20,12,13,19])).
% 107.84/107.86 cnf(6553,plain,
% 107.84/107.86 (~P2(f7(a2),f6(a1),f7(a2))),
% 107.84/107.86 inference(scs_inference,[],[5,6502,6418,6510,3,16,10,15,17,25,20,12,13,19,30])).
% 107.84/107.86 cnf(6555,plain,
% 107.84/107.86 (P2(a4,f8(a5,a5),f8(a5,a5))),
% 107.84/107.86 inference(scs_inference,[],[5,6502,6418,6510,6416,6404,3,16,10,15,17,25,20,12,13,19,30,29])).
% 107.84/107.86 cnf(6559,plain,
% 107.84/107.86 (P4(f6(a1),a2,a2)),
% 107.84/107.86 inference(scs_inference,[],[5,6506,6502,6430,6418,6510,6448,6460,6416,6404,3,16,10,15,17,25,20,12,13,19,30,29,28,27])).
% 107.84/107.86 cnf(6563,plain,
% 107.84/107.86 (~P2(a1,a5,f6(a4))),
% 107.84/107.86 inference(scs_inference,[],[5,6506,6502,6478,6430,6490,6418,6510,6504,6448,6460,6416,6422,6404,3035,3,16,10,15,17,25,20,12,13,19,30,29,28,27,32,31])).
% 107.84/107.86 cnf(6565,plain,
% 107.84/107.86 (~P4(f6(a1),a2,a1)),
% 107.84/107.86 inference(scs_inference,[],[5,6506,6502,6478,6430,6490,6418,6510,6504,6448,6460,6416,6422,6404,3035,3,16,10,15,17,25,20,12,13,19,30,29,28,27,32,31,2942])).
% 107.84/107.86 cnf(6567,plain,
% 107.84/107.86 (~P2(f7(a5),f6(a1),f7(a2))),
% 107.84/107.86 inference(scs_inference,[],[5,6506,6502,6478,6430,6490,6418,6510,6504,6448,6460,6416,6422,6404,3035,3,16,10,15,17,25,20,12,13,19,30,29,28,27,32,31,2942,3998])).
% 107.84/107.86 cnf(6569,plain,
% 107.84/107.86 (~P4(f3(a1,a1),f6(a1),f6(a5))),
% 107.84/107.86 inference(scs_inference,[],[5,6506,6502,6478,6430,6490,6418,6510,6504,6448,6460,6416,6422,6404,3035,3,16,10,15,17,25,20,12,13,19,30,29,28,27,32,31,2942,3998,24])).
% 107.84/107.86 cnf(6575,plain,
% 107.84/107.86 (P4(a1,f3(a2,a2),f3(a2,a2))),
% 107.84/107.86 inference(scs_inference,[],[5,6506,6502,6478,6430,6490,6418,6510,6504,6448,6460,6416,6422,6404,3035,3,16,10,15,17,25,20,12,13,19,30,29,28,27,32,31,2942,3998,24,67,3240,21])).
% 107.84/107.86 cnf(6582,plain,
% 107.84/107.86 (P2(a4,f3(a1,a1),f3(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[6458,16])).
% 107.84/107.86 cnf(6586,plain,
% 107.84/107.86 (P4(a1,f8(a2,a2),f8(a2,a2))),
% 107.84/107.86 inference(scs_inference,[],[6458,6549,6565,16,24,15])).
% 107.84/107.86 cnf(6592,plain,
% 107.84/107.86 (~P4(a1,f6(a1),f6(a5))),
% 107.84/107.86 inference(scs_inference,[],[5,6458,6549,6569,6543,6567,6565,6460,6422,1257,16,24,15,25,29,28])).
% 107.84/107.86 cnf(6594,plain,
% 107.84/107.86 (P4(f6(a1),f3(a2,a2),f3(a2,a2))),
% 107.84/107.86 inference(scs_inference,[],[5,6458,6549,6569,6543,6567,6551,6559,6565,6460,6422,1257,16,24,15,25,29,28,27])).
% 107.84/107.86 cnf(6601,plain,
% 107.84/107.86 (P2(a4,f3(a2,a2),f3(a2,a2))),
% 107.84/107.86 inference(scs_inference,[],[6547,16])).
% 107.84/107.86 cnf(6605,plain,
% 107.84/107.86 (P4(a1,f7(a2),f7(a2))),
% 107.84/107.86 inference(scs_inference,[],[6547,6452,6592,16,24,15])).
% 107.84/107.86 cnf(6607,plain,
% 107.84/107.86 (~P2(f7(a5),a5,f6(a1))),
% 107.84/107.86 inference(scs_inference,[],[6508,6547,6452,6592,16,24,15,25])).
% 107.84/107.86 cnf(6609,plain,
% 107.84/107.86 (~P2(f7(a2),f8(a5,a5),a2)),
% 107.84/107.86 inference(scs_inference,[],[5,6508,6547,6452,6592,9,6426,16,24,15,25,29])).
% 107.84/107.86 cnf(6611,plain,
% 107.84/107.86 (P4(f3(a1,a1),a1,f3(a1,a1))),
% 107.84/107.86 inference(scs_inference,[],[5,6474,6508,6547,6452,6592,9,6460,6426,16,24,15,25,29,28])).
% 107.84/107.86 cnf(6613,plain,
% 107.84/107.86 (P4(f3(a1,a1),f3(a4,a4),f3(a4,a4))),
% 107.84/107.86 inference(scs_inference,[],[5,6474,6508,6512,6547,6452,6592,6504,9,6460,6426,16,24,15,25,29,28,27])).
% 107.84/107.86 cnf(6619,plain,
% 107.84/107.86 (P2(a4,f6(a5),f6(a5))),
% 107.84/107.86 inference(scs_inference,[],[6402,16])).
% 107.84/107.86 cnf(6621,plain,
% 107.84/107.86 (P4(a1,f8(a4,a4),f8(a4,a4))),
% 107.84/107.86 inference(scs_inference,[],[6402,6498,16,15])).
% 107.84/107.86 cnf(6625,plain,
% 107.84/107.86 (~P2(f7(a2),a5,f6(a1))),
% 107.84/107.86 inference(scs_inference,[],[5,6470,6402,6498,6607,2198,16,15,25,30])).
% 107.84/107.86 cnf(6627,plain,
% 107.84/107.86 (P2(f6(a2),f8(a4,a4),f6(a2))),
% 107.84/107.86 inference(scs_inference,[],[5,6500,6470,6402,6498,6607,3988,2198,16,15,25,30,29])).
% 107.84/107.86 cnf(6629,plain,
% 107.84/107.86 (P4(f6(a1),f3(a4,a4),f3(a4,a4))),
% 107.84/107.86 inference(scs_inference,[],[5,6514,6500,6470,6402,6498,6607,6448,3988,2198,16,15,25,30,29,27])).
% 107.84/107.86 cnf(6644,plain,
% 107.84/107.86 (~P2(a2,f6(a1),a2)),
% 107.84/107.86 inference(scs_inference,[],[6586,6609,6462,6549,4921,16,25,72,30])).
% 107.84/107.86 cnf(6646,plain,
% 107.84/107.86 (~P2(a2,f6(a1),a5)),
% 107.84/107.86 inference(scs_inference,[],[6625,6586,6609,6462,6549,4921,2198,16,25,72,30,29])).
% 107.84/107.86 cnf(6648,plain,
% 107.84/107.86 (~P4(a2,a5,a2)),
% 107.84/107.86 inference(scs_inference,[],[6625,6586,6609,6406,6462,6549,6541,2906,4921,2198,16,25,72,30,29,27])).
% 107.84/107.86 cnf(6652,plain,
% 107.84/107.86 (~P4(a5,a2,a2)),
% 107.84/107.86 inference(scs_inference,[],[6625,6586,6539,6609,6406,6462,6549,6541,2906,4921,2198,37,16,25,72,30,29,27,26,24])).
% 107.84/107.86 cnf(6654,plain,
% 107.84/107.86 (P4(a1,a4,a1)+P2(f7(a4),a4,a4)),
% 107.84/107.86 inference(scs_inference,[],[6625,6586,6539,6609,6406,6462,6549,6541,2906,4921,2,2198,37,16,25,72,30,29,27,26,24,22])).
% 107.84/107.86 cnf(6656,plain,
% 107.84/107.87 (~P4(f6(a2),f3(a2,a2),a1)),
% 107.84/107.87 inference(scs_inference,[],[6625,6586,6539,6609,6406,6462,6551,6549,6541,2906,4921,2,2198,37,7,16,25,72,30,29,27,26,24,22,28])).
% 107.84/107.87 cnf(6663,plain,
% 107.84/107.87 (P2(a4,f7(a2),f7(a2))),
% 107.84/107.87 inference(scs_inference,[],[6656,6452,24,16])).
% 107.84/107.87 cnf(6669,plain,
% 107.84/107.87 (P4(f6(a4),f3(a4,a4),a4)),
% 107.84/107.87 inference(scs_inference,[],[6656,6516,6553,6452,6492,6464,6462,6504,24,16,25,29,27])).
% 107.84/107.87 cnf(6673,plain,
% 107.84/107.87 (~P4(a4,a1,f3(a4,a4))),
% 107.84/107.87 inference(scs_inference,[],[6621,6656,6516,6553,6452,6492,6464,6462,6504,37,24,16,25,29,27,26,3058])).
% 107.84/107.87 cnf(6675,plain,
% 107.84/107.87 (~P4(a1,f3(a4,a4),a4)),
% 107.84/107.87 inference(scs_inference,[],[6621,6656,6516,6553,6452,6492,6464,6462,6504,37,24,16,25,29,27,26,3058,3731])).
% 107.84/107.87 cnf(6679,plain,
% 107.84/107.87 (P2(f6(a1),f8(a4,a4),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6621,6656,6516,6553,6500,6466,6452,6492,6464,6462,6504,37,24,16,25,29,27,26,3058,3731,21,2219])).
% 107.84/107.87 cnf(6683,plain,
% 107.84/107.87 (~P4(a1,a4,f3(a4,a4))),
% 107.84/107.87 inference(scs_inference,[],[6673,24])).
% 107.84/107.87 cnf(6685,plain,
% 107.84/107.87 (P2(a4,f8(a4,a4),f8(a4,a4))),
% 107.84/107.87 inference(scs_inference,[],[6673,6498,24,16])).
% 107.84/107.87 cnf(6691,plain,
% 107.84/107.87 (~P4(f6(a4),f3(a4,a4),f3(a4,a4))),
% 107.84/107.87 inference(scs_inference,[],[6644,6663,6673,6498,6492,6504,6462,4921,24,16,25,29,28])).
% 107.84/107.87 cnf(6693,plain,
% 107.84/107.87 (~P2(a1,a2,f6(a4))),
% 107.84/107.87 inference(scs_inference,[],[6605,6644,6663,6673,6498,6492,6504,6462,4921,3035,24,16,25,29,28,31])).
% 107.84/107.87 cnf(6702,plain,
% 107.84/107.87 (P2(a4,a1,a1)),
% 107.84/107.87 inference(scs_inference,[],[6675,1,24,16])).
% 107.84/107.87 cnf(6706,plain,
% 107.84/107.87 (~P2(f8(a4,a4),a1,a2)),
% 107.84/107.87 inference(scs_inference,[],[6450,6675,6563,6500,1,24,16,25,29])).
% 107.84/107.87 cnf(6708,plain,
% 107.84/107.87 (~P4(f6(a4),f3(a1,a1),a1)),
% 107.84/107.87 inference(scs_inference,[],[6450,6675,6563,6613,6669,6500,1,24,16,25,29,28])).
% 107.84/107.87 cnf(6715,plain,
% 107.84/107.87 (~P2(a4,f6(a1),a2)),
% 107.84/107.87 inference(scs_inference,[],[6702,4775])).
% 107.84/107.87 cnf(6716,plain,
% 107.84/107.87 (~P2(f6(a1),a4,a2)),
% 107.84/107.87 inference(scs_inference,[],[6702,4951])).
% 107.84/107.87 cnf(6717,plain,
% 107.84/107.87 (P2(a4,a4,a4)),
% 107.84/107.87 inference(scs_inference,[],[2,16])).
% 107.84/107.87 cnf(6723,plain,
% 107.84/107.87 (P2(f8(a4,a4),a4,f8(a4,a4))),
% 107.84/107.87 inference(scs_inference,[],[6691,6706,6500,2,16,24,25,30])).
% 107.84/107.87 cnf(6725,plain,
% 107.84/107.87 (~P2(f6(a1),f8(a4,a4),a4)),
% 107.84/107.87 inference(scs_inference,[],[6518,6679,6691,6706,6500,2,2198,16,24,25,30,29])).
% 107.84/107.87 cnf(6727,plain,
% 107.84/107.87 (~P4(a5,f6(a1),a1)),
% 107.84/107.87 inference(scs_inference,[],[6518,6679,6691,6706,6592,6408,6500,2,2198,3725,16,24,25,30,29,28])).
% 107.84/107.87 cnf(6733,plain,
% 107.84/107.87 (P2(f3(a4,a4),a4,f3(a4,a4))),
% 107.84/107.87 inference(scs_inference,[],[6518,6679,6691,6706,6592,6494,6408,6500,6466,6504,2,2198,37,3725,16,24,25,30,29,28,26,23,32])).
% 107.84/107.87 cnf(6740,plain,
% 107.84/107.87 (P2(a4,a2,a2)),
% 107.84/107.87 inference(scs_inference,[],[6708,3,24,16])).
% 107.84/107.87 cnf(6742,plain,
% 107.84/107.87 (~P2(f8(a4,a4),f6(a1),a4)),
% 107.84/107.87 inference(scs_inference,[],[6708,6725,3,24,16,25])).
% 107.84/107.87 cnf(6744,plain,
% 107.84/107.87 (~P2(f6(a1),f8(a4,a4),a2)),
% 107.84/107.87 inference(scs_inference,[],[6716,6723,6708,6725,6679,3,24,16,25,30])).
% 107.84/107.87 cnf(6746,plain,
% 107.84/107.87 (~P2(a4,a5,a1)),
% 107.84/107.87 inference(scs_inference,[],[6717,6716,6723,6708,6725,6410,6679,6404,3,24,16,25,30,29])).
% 107.84/107.87 cnf(6750,plain,
% 107.84/107.87 (~P4(f3(a4,a4),a4,f3(a4,a4))),
% 107.84/107.87 inference(scs_inference,[],[6717,6716,6723,6708,6725,6410,6679,6691,6669,6404,6504,3,24,16,25,30,29,5603,27])).
% 107.84/107.87 cnf(6752,plain,
% 107.84/107.87 (P2(f3(a4,a4),a2,f3(a2,a2))),
% 107.84/107.87 inference(scs_inference,[],[6717,6716,6723,6708,6725,6410,6679,6691,6669,6551,6404,6504,3,24,16,25,30,29,5603,27,32])).
% 107.84/107.87 cnf(6756,plain,
% 107.84/107.87 (~P4(a4,f3(a4,a4),f3(a4,a4))),
% 107.84/107.87 inference(scs_inference,[],[6750,24])).
% 107.84/107.87 cnf(6758,plain,
% 107.84/107.87 (~P2(a5,a4,a1)),
% 107.84/107.87 inference(scs_inference,[],[6746,6750,24,25])).
% 107.84/107.87 cnf(6760,plain,
% 107.84/107.87 (~P2(f8(a4,a4),a5,a1)),
% 107.84/107.87 inference(scs_inference,[],[6746,6750,6404,6500,24,25,29])).
% 107.84/107.87 cnf(6770,plain,
% 107.84/107.87 (~P2(a4,a2,f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6740,6715,6744,6727,6717,24,25,29])).
% 107.84/107.87 cnf(6777,plain,
% 107.84/107.87 (~P2(f6(a1),f7(a2),a4)),
% 107.84/107.87 inference(scs_inference,[],[6760,6770,6462,3974,25,30])).
% 107.84/107.87 cnf(6779,plain,
% 107.84/107.87 (~P2(a4,a2,a1)),
% 107.84/107.87 inference(scs_inference,[],[6760,6770,6740,6450,6717,6462,3974,25,30,29])).
% 107.84/107.87 cnf(6783,plain,
% 107.84/107.87 (~P4(f8(a1,a1),a1,a2)),
% 107.84/107.87 inference(scs_inference,[],[6760,6770,6454,6702,6740,6450,6717,6464,6462,6504,3974,25,30,29,803,32])).
% 107.84/107.87 cnf(6792,plain,
% 107.84/107.87 (~P2(a2,a4,a1)),
% 107.84/107.87 inference(scs_inference,[],[6779,6783,24,25])).
% 107.84/107.87 cnf(6794,plain,
% 107.84/107.87 (~P2(f8(a4,a4),a2,a1)),
% 107.84/107.87 inference(scs_inference,[],[6779,6783,6740,6500,24,25,29])).
% 107.84/107.87 cnf(6804,plain,
% 107.84/107.87 (~P2(a1,f7(a5),a4)),
% 107.84/107.87 inference(scs_inference,[],[6646,3976,6422,6404,25,29])).
% 107.84/107.87 cnf(6816,plain,
% 107.84/107.87 (~P4(f6(a1),f6(a1),a5)),
% 107.84/107.87 inference(scs_inference,[],[6693,6652,6559,25,28])).
% 107.84/107.87 cnf(6823,plain,
% 107.84/107.87 (~P2(f7(a2),f6(a1),a4)),
% 107.84/107.87 inference(scs_inference,[],[6777,25])).
% 107.84/107.87 cnf(6825,plain,
% 107.84/107.87 (~P2(f7(a5),a2,f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[5,6777,6518,6462,25,29])).
% 107.84/107.87 cnf(6827,plain,
% 107.84/107.87 (P2(a1,a4,a1)),
% 107.84/107.87 inference(scs_inference,[],[5,6777,6518,6492,6717,6462,3963,25,29,32])).
% 107.84/107.87 cnf(6829,plain,
% 107.84/107.87 (~P2(f6(a1),a4,a5)),
% 107.84/107.87 inference(scs_inference,[],[5,6777,6518,6492,6717,6462,3963,25,29,32,4073])).
% 107.84/107.87 cnf(6830,plain,
% 107.84/107.87 (~P2(a4,f6(a1),a5)),
% 107.84/107.87 inference(scs_inference,[],[5,6777,6518,6492,6717,6462,3963,25,29,32,4073,4518])).
% 107.84/107.87 cnf(6831,plain,
% 107.84/107.87 (~P2(f7(a5),f6(a1),a4)),
% 107.84/107.87 inference(scs_inference,[],[5,6777,6518,6492,6717,6462,3963,25,29,32,4073,4518,3998])).
% 107.84/107.87 cnf(6839,plain,
% 107.84/107.87 (~P2(a4,f6(a1),a2)),
% 107.84/107.87 inference(scs_inference,[],[6827,4438])).
% 107.84/107.87 cnf(6842,plain,
% 107.84/107.87 (~P2(a1,f6(a4),a5)),
% 107.84/107.87 inference(scs_inference,[],[6827,6831,6464,25,2559])).
% 107.84/107.87 cnf(6844,plain,
% 107.84/107.87 (~P2(a1,f6(a4),a2)),
% 107.84/107.87 inference(scs_inference,[],[6827,6831,6464,25,2559,2515])).
% 107.84/107.87 cnf(6846,plain,
% 107.84/107.87 (P2(f8(a1,a1),a4,f8(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[6827,6831,6454,6464,25,2559,2515,30])).
% 107.84/107.87 cnf(6848,plain,
% 107.84/107.87 (~P2(a4,a5,f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6827,6831,6454,6422,6464,3956,25,2559,2515,30,29])).
% 107.84/107.87 cnf(6850,plain,
% 107.84/107.87 (~P4(f6(a4),f3(a4,a4),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6827,6831,4922,6454,6733,6669,6422,6464,3956,3963,25,2559,2515,30,29,32])).
% 107.84/107.87 cnf(6852,plain,
% 107.84/107.87 (~P4(f3(a4,a4),f6(a4),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6827,6831,4922,6454,6733,6669,6422,6464,3956,3963,25,2559,2515,30,29,32,24])).
% 107.84/107.87 cnf(6859,plain,
% 107.84/107.87 (~P2(f7(a2),f8(a5,a5),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[5,6830,6844,6426,25,29])).
% 107.84/107.87 cnf(6863,plain,
% 107.84/107.87 (P2(f3(a1,a1),a4,f3(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[5,6830,6844,6852,6629,6827,6460,6426,3698,25,29,28,32])).
% 107.84/107.87 cnf(6873,plain,
% 107.84/107.87 (~P2(a5,f6(a1),a2)),
% 107.84/107.87 inference(scs_inference,[],[6842,6825,6422,2198,25,29])).
% 107.84/107.87 cnf(6875,plain,
% 107.84/107.87 (~P4(a4,f3(a1,a1),a1)),
% 107.84/107.87 inference(scs_inference,[],[6842,6825,6683,6512,6422,6504,2198,25,29,28])).
% 107.84/107.87 cnf(6877,plain,
% 107.84/107.87 (~P2(f3(a1,a1),a5,f6(a5))),
% 107.84/107.87 inference(scs_inference,[],[6842,6825,6683,6512,6746,6408,6422,6404,6504,2198,25,29,28,32])).
% 107.84/107.87 cnf(6879,plain,
% 107.84/107.87 (~P4(f3(a1,a1),a4,a1)),
% 107.84/107.87 inference(scs_inference,[],[6842,6825,6683,6512,6746,6408,6422,6404,6504,2198,25,29,28,32,24])).
% 107.84/107.87 cnf(6891,plain,
% 107.84/107.87 (~P2(f8(a5,a5),f7(a2),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6859,25])).
% 107.84/107.87 cnf(6893,plain,
% 107.84/107.87 (~P2(f6(a1),f8(a4,a4),a5)),
% 107.84/107.87 inference(scs_inference,[],[6859,6848,6679,2198,25,29])).
% 107.84/107.87 cnf(6895,plain,
% 107.84/107.87 (~P4(a1,a4,a1)),
% 107.84/107.87 inference(scs_inference,[],[6859,6879,6848,6474,6512,6679,2198,25,29,28])).
% 107.84/107.87 cnf(6897,plain,
% 107.84/107.87 (P2(f3(a1,a1),a1,f8(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[6859,6879,6848,6474,6478,6454,6512,6679,6460,2198,25,29,28,32])).
% 107.84/107.87 cnf(6899,plain,
% 107.84/107.87 (P2(f7(a4),a4,a4)),
% 107.84/107.87 inference(scs_inference,[],[6859,6879,6848,6474,6478,6454,6512,6679,6460,2198,25,29,28,32,6654])).
% 107.84/107.87 cnf(6900,plain,
% 107.84/107.87 (~P4(a4,a1,a1)),
% 107.84/107.87 inference(scs_inference,[],[6859,6879,6848,6474,6478,6454,6512,6679,6460,2198,25,29,28,32,6654,24])).
% 107.84/107.87 cnf(6906,plain,
% 107.84/107.87 (~P2(f7(a4),f6(a1),a2)),
% 107.84/107.87 inference(scs_inference,[],[6839,6859,6879,6848,6474,6478,6454,6512,6679,6460,2,2198,25,29,28,32,6654,24,2267,18,30])).
% 107.84/107.87 cnf(6908,plain,
% 107.84/107.87 (P4(a1,f7(a4),f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[6839,6859,6879,6848,6474,6478,6454,6512,6679,6460,2,2198,25,29,28,32,6654,24,2267,18,30,15])).
% 107.84/107.87 cnf(6910,plain,
% 107.84/107.87 (P2(a4,f7(a4),f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[6839,6859,6879,6848,6474,6478,6454,6512,6679,6460,2,2198,25,29,28,32,6654,24,2267,18,30,15,16])).
% 107.84/107.87 cnf(6914,plain,
% 107.84/107.87 (P2(f7(a4),f6(a1),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6899,2201])).
% 107.84/107.87 cnf(6920,plain,
% 107.84/107.87 (~P2(a5,f6(a1),f8(a5,a5))),
% 107.84/107.87 inference(scs_inference,[],[6899,6877,6908,6830,6422,6426,2201,25,72,30])).
% 107.84/107.87 cnf(6922,plain,
% 107.84/107.87 (P2(f7(a4),f7(a5),f7(a5))),
% 107.84/107.87 inference(scs_inference,[],[5,6899,6877,6908,6830,6422,6426,2201,25,72,30,29])).
% 107.84/107.87 cnf(6926,plain,
% 107.84/107.87 (~P2(f3(a4,a4),a1,f6(a5))),
% 107.84/107.87 inference(scs_inference,[],[5,6895,6899,6877,6908,6430,6830,6702,6408,6422,6426,6504,2201,25,72,30,29,28,31])).
% 107.84/107.87 cnf(6928,plain,
% 107.84/107.87 (~P4(a4,a5,a5)),
% 107.84/107.87 inference(scs_inference,[],[5,6895,6899,6877,6908,6430,6830,6702,6408,6422,6426,6504,2201,25,72,30,29,28,31,24])).
% 107.84/107.87 cnf(6932,plain,
% 107.84/107.87 (P2(f3(a4,a4),a1,a1)),
% 107.84/107.87 inference(scs_inference,[],[5,6895,6899,6877,6908,6430,6830,6702,6424,6408,6422,6426,6504,2201,25,72,30,29,28,31,24,27,32])).
% 107.84/107.87 cnf(6938,plain,
% 107.84/107.87 (~P2(a1,a4,f6(a5))),
% 107.84/107.87 inference(scs_inference,[],[6893,6926,6932,6827,25,29])).
% 107.84/107.87 cnf(6942,plain,
% 107.84/107.87 (P4(f8(a4,a4),f8(a4,a4),f3(a4,a4))),
% 107.84/107.87 inference(scs_inference,[],[6893,6926,6932,6750,6733,6512,6827,6500,6504,25,29,28,31])).
% 107.84/107.87 cnf(6944,plain,
% 107.84/107.87 (~P4(f6(a4),f7(a4),a2)),
% 107.84/107.87 inference(scs_inference,[],[6792,6893,6926,6932,6750,6899,6733,6512,6492,6827,6500,6504,3963,25,29,28,31,32])).
% 107.84/107.87 cnf(6948,plain,
% 107.84/107.87 (~P2(f3(a1,a1),f6(a4),a5)),
% 107.84/107.87 inference(scs_inference,[],[6792,6893,6926,6932,6863,6750,6899,6733,6512,6492,6827,6500,6504,3963,25,29,28,31,32,24,2559])).
% 107.84/107.87 cnf(6957,plain,
% 107.84/107.87 (~P2(f3(a1,a1),f6(a4),a2)),
% 107.84/107.87 inference(scs_inference,[],[6906,6944,6863,6512,24,25,2515])).
% 107.84/107.87 cnf(6959,plain,
% 107.84/107.87 (~P2(f7(a4),f6(a1),a5)),
% 107.84/107.87 inference(scs_inference,[],[6829,6906,6914,6944,6863,6512,3974,24,25,2515,30])).
% 107.84/107.87 cnf(6961,plain,
% 107.84/107.87 (~P2(f8(a4,a4),f6(a1),f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[6829,6742,6906,6914,6944,6863,6899,6512,3974,24,25,2515,30,29])).
% 107.84/107.87 cnf(6963,plain,
% 107.84/107.87 (~P4(a1,a4,f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6829,6742,6850,6906,6914,6944,6863,6669,6899,6512,3974,93,24,25,2515,30,29,28])).
% 107.84/107.87 cnf(6965,plain,
% 107.84/107.87 (P2(f8(a4,a4),f6(a1),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6829,6742,6850,6906,6914,6944,6863,6669,6899,6512,6500,3974,93,24,25,2515,30,29,28,2199])).
% 107.84/107.87 cnf(6967,plain,
% 107.84/107.87 (~P2(a1,f6(a1),x69671)+P4(x69671,f6(a1),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6829,6742,6850,6906,6914,6944,6863,6908,6669,6899,6512,6500,3974,93,24,25,2515,30,29,28,2199,31])).
% 107.84/107.87 cnf(6984,plain,
% 107.84/107.87 (~P2(f7(a5),a1,a4)),
% 107.84/107.87 inference(scs_inference,[],[6804,6963,24,25])).
% 107.84/107.87 cnf(6986,plain,
% 107.84/107.87 (~P2(f3(a4,a4),a1,a2)),
% 107.84/107.87 inference(scs_inference,[],[6804,6963,6792,6932,6827,24,25,30])).
% 107.84/107.87 cnf(6988,plain,
% 107.84/107.87 (P2(f7(a4),f3(a2,a2),f3(a2,a2))),
% 107.84/107.87 inference(scs_inference,[],[6601,6804,6963,6792,6932,6899,6827,24,25,30,29])).
% 107.84/107.87 cnf(6990,plain,
% 107.84/107.87 (~P4(f6(a1),a4,f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6601,6804,6963,6792,6932,6448,6899,6827,6464,24,25,30,29,28])).
% 107.84/107.87 cnf(6992,plain,
% 107.84/107.87 (~P2(f3(a4,a4),f6(a1),a5)),
% 107.84/107.87 inference(scs_inference,[],[6816,6942,6601,6965,6804,6963,6792,6932,6448,6899,6827,6464,24,25,30,29,28,31])).
% 107.84/107.87 cnf(6998,plain,
% 107.84/107.87 (~P4(a4,f6(a1),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6990,24])).
% 107.84/107.87 cnf(7000,plain,
% 107.84/107.87 (~P2(f6(a1),f8(a4,a4),f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[6961,6990,24,25])).
% 107.84/107.87 cnf(7002,plain,
% 107.84/107.87 (~P2(f7(a5),f8(a5,a5),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6922,6961,6959,6990,6426,24,25,29])).
% 107.84/107.87 cnf(7004,plain,
% 107.84/107.87 (~P4(f6(a1),f6(a4),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6922,6961,6959,6990,6492,6426,3698,24,25,29,28])).
% 107.84/107.87 cnf(7008,plain,
% 107.84/107.87 (~P4(a1,f6(a4),a1)),
% 107.84/107.87 inference(scs_inference,[],[6922,6961,6959,6990,6492,6426,3698,24,25,29,28,1285,3700])).
% 107.84/107.87 cnf(7015,plain,
% 107.84/107.87 (~P4(f6(a4),f6(a1),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[7004,24])).
% 107.84/107.87 cnf(7019,plain,
% 107.84/107.87 (~P2(f7(a4),f6(a1),f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[7000,7002,7004,6914,6679,24,25,30])).
% 107.84/107.87 cnf(7021,plain,
% 107.84/107.87 (~P2(f7(a5),a1,f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[7000,7002,7004,6984,6914,6679,6899,6827,24,25,30,29])).
% 107.84/107.87 cnf(7023,plain,
% 107.84/107.87 (P2(f3(a4,a4),f8(a4,a4),f3(a4,a4))),
% 107.84/107.87 inference(scs_inference,[],[7000,7002,7004,6984,6685,6942,6914,6679,6899,6827,6504,24,25,30,29,32])).
% 107.84/107.87 cnf(7030,plain,
% 107.84/107.87 (~P2(f7(a2),a1,f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[5,6910,6992,7021,25,30])).
% 107.84/107.87 cnf(7032,plain,
% 107.84/107.87 (~P2(f7(a4),a4,f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[5,6910,6992,7021,4921,6899,25,30,29])).
% 107.84/107.87 cnf(7036,plain,
% 107.84/107.87 (P4(f8(a1,a1),a1,a1)),
% 107.84/107.87 inference(scs_inference,[],[5,6910,7008,6992,6897,7021,6613,6932,6408,4921,6899,25,30,29,28,31])).
% 107.84/107.87 cnf(7042,plain,
% 107.84/107.87 (~P4(f6(a4),a4,f6(a5))),
% 107.84/107.87 inference(scs_inference,[],[5,6910,7008,6992,6897,7021,6938,6891,6613,6932,6408,6717,6492,4921,6899,3963,25,30,29,28,31,24,2251,32])).
% 107.84/107.87 cnf(7050,plain,
% 107.84/107.87 (~P2(a4,f7(a4),f6(a1))),
% 107.84/107.87 inference(scs_inference,[],[6948,7019,7042,6910,6899,24,25,29])).
% 107.84/107.87 cnf(7052,plain,
% 107.84/107.87 (~P4(f8(a1,a1),f8(a1,a1),a4)),
% 107.84/107.87 inference(scs_inference,[],[6900,6948,7019,7036,7042,6910,6899,24,25,29,28])).
% 107.84/107.87 cnf(7056,plain,
% 107.84/107.87 (~P2(a1,f8(a4,a4),f6(a4))),
% 107.84/107.87 inference(scs_inference,[],[6900,6948,7019,7036,7042,6432,7004,6910,6679,6899,3698,24,25,29,28,27,31])).
% 107.84/107.87 cnf(7058,plain,
% 107.84/107.87 (~P4(f6(a1),a1,f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[6900,6948,7019,7032,7036,7042,6432,7004,6910,6679,6899,6827,3698,3974,24,25,29,28,27,31,32])).
% 107.84/107.87 cnf(7070,plain,
% 107.84/107.87 (~P4(a1,a1,f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[6957,7030,7058,6910,6448,6462,1257,24,25,29,28])).
% 107.84/107.87 cnf(7072,plain,
% 107.84/107.87 (~P2(a1,f6(a1),f6(a4))),
% 107.84/107.87 inference(scs_inference,[],[6957,7030,7058,7015,6910,6448,6462,1257,24,25,29,28,6967])).
% 107.84/107.87 cnf(7080,plain,
% 107.84/107.87 (~P2(a4,f6(a1),f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[6986,7050,6717,2198,25,29])).
% 107.84/107.87 cnf(7096,plain,
% 107.84/107.87 (P4(f8(a1,a1),f8(a5,a5),f8(a5,a5))),
% 107.84/107.87 inference(scs_inference,[],[7056,6823,7008,6446,7036,6717,6462,93,25,29,28,27])).
% 107.84/107.87 cnf(7105,plain,
% 107.84/107.87 (~P2(f6(a1),a5,f8(a5,a5))),
% 107.84/107.87 inference(scs_inference,[],[6920,25])).
% 107.84/107.87 cnf(7116,plain,
% 107.84/107.87 (~P2(a5,f7(a4),a1)),
% 107.84/107.87 inference(scs_inference,[],[5,7080,7021,6984,6910,6422,6717,25,30,29])).
% 107.84/107.87 cnf(7120,plain,
% 107.84/107.87 (~P2(a1,f6(a1),a4)),
% 107.84/107.87 inference(scs_inference,[],[5,7080,6998,6846,7021,6938,6984,6910,7036,6422,6827,6717,25,30,29,32,6967])).
% 107.84/107.87 cnf(7127,plain,
% 107.84/107.87 (~P2(a2,f8(a4,a4),a1)),
% 107.84/107.87 inference(scs_inference,[],[6794,25])).
% 107.84/107.87 cnf(7131,plain,
% 107.84/107.87 (~P4(f8(a1,a1),a1,a4)),
% 107.84/107.87 inference(scs_inference,[],[7052,6794,6478,6494,25,28,24])).
% 107.84/107.87 cnf(7142,plain,
% 107.84/107.87 (~P2(f6(a1),a1,a4)),
% 107.84/107.87 inference(scs_inference,[],[7120,25])).
% 107.84/107.87 cnf(7148,plain,
% 107.84/107.87 (~P4(f3(a1,a1),f3(a1,a1),f6(a4))),
% 107.84/107.87 inference(scs_inference,[],[7120,7105,6609,6416,6740,6512,6404,3035,6462,25,30,29,28])).
% 107.84/107.87 cnf(7166,plain,
% 107.84/107.87 (~P4(a1,f3(a1,a1),f6(a4))),
% 107.84/107.87 inference(scs_inference,[],[5,7148,7116,6715,6474,6460,25,29,28])).
% 107.84/107.87 cnf(7181,plain,
% 107.84/107.87 (~P2(f7(a4),f6(a1),a4)),
% 107.84/107.87 inference(scs_inference,[],[7072,7166,6518,6914,6910,24,25,29])).
% 107.84/107.87 cnf(7185,plain,
% 107.84/107.87 (~P2(a1,f8(a5,a5),a4)),
% 107.84/107.87 inference(scs_inference,[],[7072,7166,6928,6879,6539,6518,6914,6424,6910,6492,6426,24,25,29,28,31])).
% 107.84/107.87 cnf(7206,plain,
% 107.84/107.87 (~P2(a4,a5,a2)),
% 107.84/107.87 inference(scs_inference,[],[7181,9,6404,6717,25,29])).
% 107.84/107.87 cnf(7222,plain,
% 107.84/107.87 (~P4(f3(a1,a1),f3(a4,a4),a4)),
% 107.84/107.87 inference(scs_inference,[],[7206,6875,6723,6669,6492,6500,25,29,28,24])).
% 107.84/107.87 cnf(7226,plain,
% 107.84/107.87 (P4(f6(a2),f3(a2,a2),a2)),
% 107.84/107.87 inference(scs_inference,[],[7206,6875,6986,6723,7023,6506,6551,6669,6541,6492,6500,25,29,28,24,30,27])).
% 107.84/107.87 cnf(7228,plain,
% 107.84/107.87 (~P4(a2,a1,f3(a2,a2))),
% 107.84/107.87 inference(scs_inference,[],[7206,6875,6986,6723,7023,6506,6551,6669,6541,6492,6500,25,29,28,24,30,27,2858])).
% 107.84/107.87 cnf(7230,plain,
% 107.84/107.87 (~P4(a1,f3(a2,a2),a2)),
% 107.84/107.87 inference(scs_inference,[],[7206,6875,6986,6723,7023,6506,6551,6669,6541,6492,6500,25,29,28,24,30,27,2858,3827])).
% 107.84/107.87 cnf(7235,plain,
% 107.84/107.87 (~P4(a1,a2,f3(a2,a2))),
% 107.84/107.87 inference(scs_inference,[],[7228,24])).
% 107.84/107.87 cnf(7237,plain,
% 107.84/107.87 (~P2(f8(a5,a5),a1,a4)),
% 107.84/107.87 inference(scs_inference,[],[7228,7185,24,25])).
% 107.84/107.87 cnf(7239,plain,
% 107.84/107.87 (~P2(f7(a5),f7(a5),a1)),
% 107.84/107.87 inference(scs_inference,[],[7228,7185,6422,6426,24,25,30])).
% 107.84/107.87 cnf(7241,plain,
% 107.84/107.87 (~P2(f8(a4,a4),a5,a2)),
% 107.84/107.87 inference(scs_inference,[],[7228,7185,7206,6404,6422,6426,6500,24,25,30,29])).
% 107.84/107.87 cnf(7245,plain,
% 107.84/107.87 (~P2(f7(a5),f7(a2),a1)),
% 107.84/107.87 inference(scs_inference,[],[7228,7226,7185,7230,7206,6559,6404,6422,6426,6500,24,25,30,29,28,698])).
% 107.84/107.87 cnf(7269,plain,
% 107.84/107.87 (P2(f7(a4),f8(a5,a5),f8(a5,a5))),
% 107.84/107.87 inference(scs_inference,[],[7241,6555,7230,6899,24,25,29])).
% 107.84/107.87 cnf(7271,plain,
% 107.84/107.87 (~P4(f3(a2,a2),a5,f3(a2,a2))),
% 107.84/107.87 inference(scs_inference,[],[7241,6648,6555,7230,7226,6899,24,25,29,28])).
% 107.84/107.87 cnf(7280,plain,
% 107.84/107.87 (~P4(a5,f3(a2,a2),f3(a2,a2))),
% 107.84/107.87 inference(scs_inference,[],[7271,24])).
% 107.84/107.87 cnf(7284,plain,
% 107.84/107.87 (~P2(a5,a1,f7(a5))),
% 107.84/107.87 inference(scs_inference,[],[7271,6873,7239,6702,6422,24,25,29])).
% 107.84/107.87 cnf(7314,plain,
% 107.84/107.87 (~P2(a1,a5,f7(a5))),
% 107.84/107.87 inference(scs_inference,[],[7284,25])).
% 107.84/107.87 cnf(7316,plain,
% 107.84/107.87 (~P2(f7(a2),f7(a2),a1)),
% 107.84/107.87 inference(scs_inference,[],[5,7284,7245,6702,25,30])).
% 107.84/107.87 cnf(7318,plain,
% 107.84/107.87 (~P2(f3(a1,a1),f3(a4,a4),a4)),
% 107.84/107.87 inference(scs_inference,[],[5,7284,6756,7245,6535,6702,6512,25,30,31])).
% 107.84/107.87 cnf(7323,plain,
% 107.84/107.87 (~P2(f3(a4,a4),f3(a1,a1),a4)),
% 107.84/107.87 inference(scs_inference,[],[7318,25])).
% 107.84/107.87 cnf(7325,plain,
% 107.84/107.87 (~P2(a1,f3(a2,a2),a5)),
% 107.84/107.87 inference(scs_inference,[],[7318,7280,6988,6908,25,31])).
% 107.84/107.87 cnf(7335,plain,
% 107.84/107.87 (~P2(f6(a1),a1,f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[7142,7325,6827,6899,25,29])).
% 107.84/107.87 cnf(7337,plain,
% 107.84/107.87 (~P2(a4,f3(a1,a1),a4)),
% 107.84/107.87 inference(scs_inference,[],[7142,7323,7325,6582,6512,6827,6899,6504,25,29,32])).
% 107.84/107.87 cnf(7341,plain,
% 107.84/107.87 (~P4(f8(a1,a1),f3(a2,a2),a2)),
% 107.84/107.87 inference(scs_inference,[],[7142,7323,7325,7131,7096,6575,7230,6582,7036,6512,6827,6899,6504,25,29,32,27,28])).
% 107.84/107.87 cnf(7352,plain,
% 107.84/107.87 (~P4(f6(a2),f6(a1),f8(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[7341,7335,6594,7226,25,24,28])).
% 107.84/107.87 cnf(7354,plain,
% 107.84/107.87 (~P2(a2,a1,f7(a2))),
% 107.84/107.87 inference(scs_inference,[],[7316,7341,7335,6594,7226,6702,6462,25,24,28,29])).
% 107.84/107.87 cnf(7356,plain,
% 107.84/107.87 (~P4(f8(a1,a1),a1,a5)),
% 107.84/107.87 inference(scs_inference,[],[7316,7341,7335,6594,6758,6846,7226,6702,7036,6827,6462,25,24,28,29,32])).
% 107.84/107.87 cnf(7362,plain,
% 107.84/107.87 (~P2(f3(a1,a1),a4,a4)),
% 107.84/107.87 inference(scs_inference,[],[7337,25])).
% 107.84/107.87 cnf(7366,plain,
% 107.84/107.87 (~P4(a5,a2,a5)),
% 107.84/107.87 inference(scs_inference,[],[7,7352,7337,6408,25,24,28])).
% 107.84/107.87 cnf(7368,plain,
% 107.84/107.87 (~P2(a5,f3(a1,a1),a5)),
% 107.84/107.87 inference(scs_inference,[],[7,7352,7337,6408,6422,25,24,28,30])).
% 107.84/107.87 cnf(7370,plain,
% 107.84/107.87 (~P2(f7(a2),a2,f3(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[7,7352,7337,6663,6408,6422,6462,25,24,28,30,29])).
% 107.84/107.87 cnf(7377,plain,
% 107.84/107.87 (~P4(a2,a5,a5)),
% 107.84/107.87 inference(scs_inference,[],[7366,7370,25,24])).
% 107.84/107.87 cnf(7379,plain,
% 107.84/107.87 (~P2(f3(a1,a1),f7(a2),f7(a2))),
% 107.84/107.87 inference(scs_inference,[],[7366,7370,6863,6462,25,24,30])).
% 107.84/107.87 cnf(7391,plain,
% 107.84/107.87 (~P4(f6(a4),f6(a1),f3(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[7356,7379,7222,6629,6669,25,24,28])).
% 107.84/107.87 cnf(7398,plain,
% 107.84/107.87 (~P2(f3(a1,a1),a5,a5)),
% 107.84/107.87 inference(scs_inference,[],[7368,25])).
% 107.84/107.87 cnf(7402,plain,
% 107.84/107.87 (~P2(f8(a5,a5),f3(a1,a1),f8(a5,a5))),
% 107.84/107.87 inference(scs_inference,[],[7391,7368,6426,25,24,30])).
% 107.84/107.87 cnf(7404,plain,
% 107.84/107.87 (~P2(a4,a4,f3(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[7391,7368,7337,6717,6426,25,24,30,29])).
% 107.84/107.87 cnf(7410,plain,
% 107.84/107.87 (~P2(f3(a1,a1),f8(a5,a5),f8(a5,a5))),
% 107.84/107.87 inference(scs_inference,[],[7402,25])).
% 107.84/107.87 cnf(7416,plain,
% 107.84/107.87 (~P2(f8(a5,a5),a1,f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[7,7402,7237,7314,6506,6702,7036,6827,6899,5,25,28,30,29])).
% 107.84/107.87 cnf(7429,plain,
% 107.84/107.87 (~P2(a2,f6(a1),f8(a5,a5))),
% 107.84/107.87 inference(scs_inference,[],[7070,7416,6859,6460,6424,6462,2198,25,28,29])).
% 107.84/107.87 cnf(7431,plain,
% 107.84/107.87 (~P4(f6(a4),f3(a4,a4),f3(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[7070,7404,7416,6859,6733,6669,6460,6424,6462,2198,3963,25,28,29,32])).
% 107.84/107.87 cnf(7433,plain,
% 107.84/107.87 (~P4(f3(a1,a1),a1,f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[7070,7404,7416,6859,6733,6669,6460,6424,6462,2198,3963,25,28,29,32,24])).
% 107.84/107.87 cnf(7445,plain,
% 107.84/107.87 (~P4(f6(a1),f3(a4,a4),a4)),
% 107.84/107.87 inference(scs_inference,[],[7431,7429,6675,6586,6514,6448,25,24,27,28])).
% 107.84/107.87 cnf(7447,plain,
% 107.84/107.87 (~P2(f7(a5),a5,f3(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[7431,7429,6675,6586,6514,7337,6448,6422,430,25,24,27,28,29])).
% 107.84/107.87 cnf(7449,plain,
% 107.84/107.87 (~P2(f3(a2,a2),f8(a4,a4),a2)),
% 107.84/107.87 inference(scs_inference,[],[7431,7429,7127,6627,6675,6586,6514,7337,7226,6448,6541,6422,430,25,24,27,28,29,32])).
% 107.84/107.87 cnf(7451,plain,
% 107.84/107.87 (~P2(a1,a2,a5)),
% 107.84/107.87 inference(scs_inference,[],[7431,7429,7127,7280,6752,6627,6675,6586,6514,7337,7226,6448,6541,6422,430,25,24,27,28,29,32,31])).
% 107.84/107.87 cnf(7459,plain,
% 107.84/107.87 (~P4(f3(a1,a1),f3(a1,a1),f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[7451,7433,7445,6611,6460,25,24,28])).
% 107.84/107.87 cnf(7461,plain,
% 107.84/107.87 (~P2(f3(a1,a1),f7(a4),f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[7451,7410,7433,7445,7269,6611,6460,25,24,28,29])).
% 107.84/107.87 cnf(7472,plain,
% 107.84/107.87 (~P4(f6(a2),f3(a2,a2),f3(a2,a2))),
% 107.84/107.87 inference(scs_inference,[],[7449,7235,6432,6551,6541,6448,25,27,28])).
% 107.84/107.87 cnf(7485,plain,
% 107.84/107.87 (P2(f7(a2),f8(a5,a5),a5)),
% 107.84/107.87 inference(scs_inference,[],[7354,6555,6426,3949,25,29])).
% 107.84/107.87 cnf(7495,plain,
% 107.84/107.87 (~P4(a2,f3(a2,a2),f3(a2,a2))),
% 107.84/107.87 inference(scs_inference,[],[7461,7472,6551,7226,25,27,28])).
% 107.84/107.87 cnf(7497,plain,
% 107.84/107.87 (~P2(f3(a1,a1),f7(a5),f7(a5))),
% 107.84/107.87 inference(scs_inference,[],[7362,7461,7472,6551,7226,6422,25,27,28,29])).
% 107.84/107.87 cnf(7506,plain,
% 107.84/107.87 (~P2(f7(a4),a4,f3(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[7497,7447,6922,6422,25,30])).
% 107.84/107.87 cnf(7517,plain,
% 107.84/107.87 (~P2(a4,f7(a4),f3(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[7506,25])).
% 107.84/107.87 cnf(7519,plain,
% 107.84/107.87 (~P2(f7(a2),a5,f3(a1,a1))),
% 107.84/107.87 inference(scs_inference,[],[7398,7485,7506,6416,25,30])).
% 107.84/107.87 cnf(7525,plain,
% 107.84/107.87 (~P2(f3(a4,a4),f3(a1,a1),f7(a4))),
% 107.84/107.87 inference(scs_inference,[],[7495,7459,7398,7485,7506,6594,6846,6582,6416,6500,6504,25,30,28,29,31])).
% 107.84/107.87 cnf(7535,plain,
% 107.84/107.87 (~P2(a1,f8(a5,a5),a2)),
% 107.84/107.87 inference(scs_inference,[],[7525,7517,7377,7485,6863,6605,6582,25,29,31])).
% 107.84/107.87 cnf(7577,plain,
% 107.84/107.87 (~P2(f3(a1,a1),f7(a5),f7(a2))),
% 107.84/107.87 inference(scs_inference,[],[7535,7519,6863,6422,25,30])).
% 107.84/107.87 cnf(7588,plain,
% 107.84/107.87 (~P2(f7(a5),f8(a5,a5),a2)),
% 107.84/107.87 inference(scs_inference,[],[9,7577,6426,430,25,29])).
% 107.84/107.87 cnf(7628,plain,
% 107.84/107.87 (~P2(a1,f8(a5,a5),f6(a5))),
% 107.84/107.87 inference(scs_inference,[],[6522,7449,6470,6988,6605,7485,6408,25,30,32])).
% 107.84/107.87 cnf(7635,plain,
% 107.84/107.87 (~P2(a5,a2,f8(a5,a5))),
% 107.84/107.87 inference(scs_inference,[],[7628,7588,7497,6922,6740,6422,25,30,29])).
% 107.84/107.87 cnf(7644,plain,
% 107.84/107.87 (~P2(a2,a5,f8(a5,a5))),
% 107.84/107.87 inference(scs_inference,[],[7635,25])).
% 107.84/107.87 cnf(7646,plain,
% 107.84/107.87 (~P2(a1,f6(a5),a5)),
% 107.84/107.87 inference(scs_inference,[],[7635,188,6619,6464,25,31])).
% 107.84/107.87 cnf(7657,plain,
% 107.84/107.87 (~P2(f3(a1,a1),f6(a5),a5)),
% 107.84/107.87 inference(scs_inference,[],[9,7646,188,6619,6740,6512,6500,25,29,31])).
% 107.84/107.87 cnf(7668,plain,
% 107.84/107.87 (~P2(a2,f7(a2),a4)),
% 107.84/107.87 inference(scs_inference,[],[7657,7644,6555,7485,25,29])).
% 107.84/107.87 cnf(9897,plain,
% 107.84/107.87 ($false),
% 107.84/107.87 inference(scs_inference,[],[7668,6462,25]),
% 107.84/107.87 ['proof']).
% 107.84/107.87 % SZS output end Proof
% 107.84/107.87 % Total time :107.210000s
%------------------------------------------------------------------------------