%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD005-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 : n004.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:08 EDT 2024
% Result : Unsatisfiable 116.73s 116.77s
% Output : CNFRefutation 116.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : FLD005-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n004.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Jun 19 09:59:09 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.20/0.58 start to proof:theBenchmark
% 116.73/116.76 %-------------------------------------------
% 116.73/116.76 % File :CSE---1.7
% 116.73/116.76 % Problem :theBenchmark
% 116.73/116.76 % Transform :cnf
% 116.73/116.76 % Format :tptp:raw
% 116.73/116.76 % Command :java -jar mcs_scs.jar %d %s
% 116.73/116.76
% 116.73/116.76 % Result :Theorem 116.130000s
% 116.73/116.76 % Output :CNFRefutation 116.130000s
% 116.73/116.76 %-------------------------------------------
% 116.73/116.77 %--------------------------------------------------------------------------
% 116.73/116.77 % File : FLD005-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 116.73/116.77 % Domain : Field Theory (Ordered fields)
% 116.73/116.77 % Problem : Every linear equation in the additive group has a solution
% 116.73/116.77 % Version : [Dra93] axioms : Especial.
% 116.73/116.77 % Theorem formulation : Functional with re axiom set.
% 116.73/116.77 % English :
% 116.73/116.77
% 116.73/116.77 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 116.73/116.77 % Source : [Dra93]
% 116.73/116.77 % Names :
% 116.73/116.77
% 116.73/116.77 % Status : Unsatisfiable
% 116.73/116.77 % Rating : 0.08 v8.2.0, 0.14 v7.5.0, 0.33 v7.4.0, 0.17 v7.1.0, 0.50 v7.0.0, 0.38 v6.3.0, 0.29 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.30 v5.2.0, 0.10 v5.1.0, 0.18 v5.0.0, 0.36 v4.1.0, 0.12 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.20 v2.3.0, 0.00 v2.2.1, 0.33 v2.1.0
% 116.73/116.77 % Syntax : Number of clauses : 29 ( 6 unt; 3 nHn; 29 RR)
% 116.73/116.77 % Number of literals : 80 ( 0 equ; 50 neg)
% 116.73/116.77 % Maximal clause size : 5 ( 2 avg)
% 116.73/116.77 % Maximal term depth : 2 ( 1 avg)
% 116.73/116.77 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 116.73/116.77 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 116.73/116.77 % Number of variables : 74 ( 1 sgn)
% 116.73/116.77 % SPC : CNF_UNS_RFO_NEQ_NHN
% 116.73/116.77
% 116.73/116.77 % Comments :
% 116.73/116.77 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 116.73/116.77 %--------------------------------------------------------------------------
% 116.73/116.77 include('Axioms/FLD002-0.ax').
% 116.73/116.77 %--------------------------------------------------------------------------
% 116.73/116.77 cnf(a_is_defined,hypothesis,
% 116.73/116.77 defined(a) ).
% 116.73/116.77
% 116.73/116.77 cnf(b_is_defined,hypothesis,
% 116.73/116.77 defined(b) ).
% 116.73/116.77
% 116.73/116.77 cnf(not_sum_3,negated_conjecture,
% 116.73/116.77 ~ sum(a,X,b) ).
% 116.73/116.77
% 116.73/116.77 %--------------------------------------------------------------------------
% 116.73/116.77 %-------------------------------------------
% 116.73/116.77 % Proof found
% 116.73/116.77 % SZS status Theorem for theBenchmark
% 116.73/116.77 % SZS output start Proof
% 116.73/116.78 %ClaNum:29(EqnAxiom:0)
% 116.73/116.78 %VarNum:163(SingletonVarNum:74)
% 116.73/116.78 %MaxLitNum:5
% 116.73/116.78 %MaxfuncDepth:1
% 116.73/116.78 %SharedTerms:9
% 116.73/116.78 %goalClause: 6
% 116.73/116.78 %singleGoalClaCount:1
% 116.73/116.78 [1]P1(a1)
% 116.73/116.78 [2]P1(a4)
% 116.73/116.78 [3]P1(a2)
% 116.73/116.78 [4]P1(a5)
% 116.73/116.78 [5]~P2(a1,a1,a4)
% 116.73/116.78 [6]~P2(a2,x61,a5)
% 116.73/116.78 [12]~P1(x121)+P2(a1,x121,x121)
% 116.73/116.78 [13]~P1(x131)+P4(a4,x131,x131)
% 116.73/116.78 [7]~P1(x71)+P1(f6(x71))
% 116.73/116.78 [14]~P1(x141)+P2(f6(x141),x141,a1)
% 116.73/116.78 [21]~P2(x212,x211,x213)+P2(x211,x212,x213)
% 116.73/116.78 [22]~P4(x222,x221,x223)+P4(x221,x222,x223)
% 116.73/116.78 [15]~P1(x151)+P2(a1,x151,a1)+P1(f8(x151))
% 116.73/116.78 [19]~P1(x191)+P4(f8(x191),x191,a4)+P2(a1,x191,a1)
% 116.73/116.78 [18]~P3(x182,x181)+~P3(x181,x182)+P2(a1,x181,x182)
% 116.73/116.78 [9]~P1(x92)+~P1(x91)+P1(f3(x91,x92))
% 116.73/116.78 [10]~P1(x102)+~P1(x101)+P1(f7(x101,x102))
% 116.73/116.78 [16]~P1(x162)+~P1(x161)+P2(x161,x162,f3(x161,x162))
% 116.73/116.78 [17]~P1(x172)+~P1(x171)+P4(x171,x172,f7(x171,x172))
% 116.73/116.78 [11]~P3(x111,x113)+P3(x111,x112)+~P3(x113,x112)
% 116.73/116.78 [8]P3(x82,x81)+~P1(x81)+~P1(x82)+P3(x81,x82)
% 116.73/116.78 [20]~P4(x203,x202,x201)+P3(a1,x201)+~P3(a1,x202)+~P3(a1,x203)
% 116.73/116.78 [23]~P2(x233,x235,x231)+P3(x231,x232)+~P2(x234,x235,x232)+~P3(x233,x234)
% 116.73/116.78 [24]~P2(x241,x246,x244)+P2(x241,x242,x243)+~P2(x244,x245,x243)+~P2(x246,x245,x242)
% 116.73/116.78 [25]~P2(x256,x254,x251)+P2(x251,x252,x253)+~P2(x254,x252,x255)+~P2(x256,x255,x253)
% 116.73/116.78 [26]~P4(x261,x266,x264)+P4(x261,x262,x263)+~P4(x264,x265,x263)+~P4(x266,x265,x262)
% 116.73/116.78 [27]~P4(x276,x274,x271)+P4(x271,x272,x273)+~P4(x274,x272,x275)+~P4(x276,x275,x273)
% 116.73/116.78 [28]~P4(x285,x287,x282)+~P4(x284,x287,x281)+P2(x281,x282,x283)+~P2(x284,x285,x286)+~P4(x286,x287,x283)
% 116.73/116.78 [29]~P4(x297,x292,x295)+~P4(x296,x292,x294)+P4(x291,x292,x293)+~P2(x294,x295,x293)+~P2(x296,x297,x291)
% 116.73/116.78 %EqnAxiom
% 116.73/116.78
% 116.73/116.78 %-------------------------------------------
% 116.73/116.79 cnf(30,plain,
% 116.73/116.79 (~P2(x301,a2,a5)),
% 116.73/116.79 inference(scs_inference,[],[6,21])).
% 116.73/116.79 cnf(32,plain,
% 116.73/116.79 (P3(a1,a1)),
% 116.73/116.79 inference(scs_inference,[],[6,1,21,8])).
% 116.73/116.79 cnf(36,plain,
% 116.73/116.79 (~P4(a1,a1,a4)+~P3(a4,a1)),
% 116.73/116.79 inference(scs_inference,[],[6,1,5,21,8,18,20])).
% 116.73/116.79 cnf(38,plain,
% 116.73/116.79 (~P3(a4,a1)+~P2(a1,x381,a1)+~P2(a1,x381,a4)),
% 116.73/116.79 inference(scs_inference,[],[6,1,5,21,8,18,20,23])).
% 116.73/116.79 cnf(39,plain,
% 116.73/116.79 (P3(a4,a4)),
% 116.73/116.79 inference(scs_inference,[],[2,8])).
% 116.73/116.79 cnf(45,plain,
% 116.73/116.79 (P3(a2,a2)),
% 116.73/116.79 inference(scs_inference,[],[3,8])).
% 116.73/116.79 cnf(47,plain,
% 116.73/116.79 (~P2(a4,x471,x472)+~P2(a4,x471,x473)+P3(x472,x473)),
% 116.73/116.79 inference(scs_inference,[],[3,39,8,23])).
% 116.73/116.79 cnf(48,plain,
% 116.73/116.79 (P3(a5,a5)),
% 116.73/116.79 inference(scs_inference,[],[4,8])).
% 116.73/116.79 cnf(50,plain,
% 116.73/116.79 (~P2(a2,x501,x502)+~P2(a2,x501,x503)+P3(x502,x503)),
% 116.73/116.79 inference(scs_inference,[],[4,45,8,23])).
% 116.73/116.79 cnf(51,plain,
% 116.73/116.79 (~P2(a5,x511,x512)+~P2(a5,x511,x513)+P3(x512,x513)),
% 116.73/116.79 inference(scs_inference,[],[48,23])).
% 116.73/116.79 cnf(52,plain,
% 116.73/116.79 (~P2(a1,x521,x522)+~P2(a1,x521,x523)+P3(x522,x523)),
% 116.73/116.79 inference(scs_inference,[],[32,23])).
% 116.73/116.79 cnf(79,plain,
% 116.73/116.79 (P2(a1,f6(a4),f6(a4))),
% 116.73/116.79 inference(scs_inference,[],[2,12,7])).
% 116.73/116.79 cnf(106,plain,
% 116.73/116.79 (P4(a4,f6(a4),f6(a4))),
% 116.73/116.79 inference(scs_inference,[],[2,13,7])).
% 116.73/116.79 cnf(178,plain,
% 116.73/116.79 (P2(f6(f6(a1)),f6(a1),a1)),
% 116.73/116.79 inference(scs_inference,[],[1,14,7])).
% 116.73/116.79 cnf(186,plain,
% 116.73/116.79 (P2(a1,x1861,a1)+~P2(f6(a1),x1861,f6(a1))),
% 116.73/116.79 inference(scs_inference,[],[178,25])).
% 116.73/116.79 cnf(206,plain,
% 116.73/116.79 (~P2(a4,x2061,a4)+~P2(a4,x2061,a1)+~P4(a1,a1,a4)),
% 116.73/116.79 inference(scs_inference,[],[36,47])).
% 116.73/116.79 cnf(222,plain,
% 116.73/116.79 (P4(f6(a4),x2221,f6(a4))+~P4(a4,x2221,a4)),
% 116.73/116.79 inference(scs_inference,[],[106,22,27])).
% 116.73/116.79 cnf(286,plain,
% 116.73/116.79 (~P2(x2861,f6(a1),f6(a1))+P2(a1,x2861,a1)),
% 116.73/116.79 inference(scs_inference,[],[186,21])).
% 116.73/116.79 cnf(302,plain,
% 116.73/116.79 (P4(x3021,f6(a4),f6(a4))+~P4(a4,x3021,a4)),
% 116.73/116.79 inference(scs_inference,[],[222,22])).
% 116.73/116.79 cnf(334,plain,
% 116.73/116.79 (~P1(f6(a1))+P2(a1,a1,a1)),
% 116.73/116.79 inference(scs_inference,[],[286,12])).
% 116.73/116.79 cnf(350,plain,
% 116.73/116.79 (P2(a1,a1,a1)),
% 116.73/116.79 inference(scs_inference,[],[1,334,7])).
% 116.73/116.79 cnf(351,plain,
% 116.73/116.79 (~P2(a2,a1,x3511)+~P2(x3511,a1,a5)),
% 116.73/116.79 inference(scs_inference,[],[6,350,24])).
% 116.73/116.79 cnf(354,plain,
% 116.73/116.79 (~P2(a1,a2,x3541)+~P2(x3541,a1,a5)),
% 116.73/116.79 inference(scs_inference,[],[6,350,24,21])).
% 116.73/116.79 cnf(376,plain,
% 116.73/116.79 (~P2(a1,x3761,a5)+~P2(a2,a1,x3761)),
% 116.73/116.79 inference(scs_inference,[],[351,21])).
% 116.73/116.79 cnf(392,plain,
% 116.73/116.79 (~P2(a1,x3921,a5)+~P2(a1,a2,x3921)),
% 116.73/116.79 inference(scs_inference,[],[354,21])).
% 116.73/116.79 cnf(423,plain,
% 116.73/116.79 (~P2(a1,f3(a2,a1),a5)),
% 116.73/116.79 inference(scs_inference,[],[1,3,376,16])).
% 116.73/116.79 cnf(424,plain,
% 116.73/116.79 (~P2(f3(a2,a1),a1,a5)),
% 116.73/116.79 inference(scs_inference,[],[423,21])).
% 116.73/116.79 cnf(444,plain,
% 116.73/116.79 (~P2(a1,f3(a1,a2),a5)),
% 116.73/116.79 inference(scs_inference,[],[3,1,392,16])).
% 116.73/116.79 cnf(445,plain,
% 116.73/116.79 (~P2(f3(a1,a2),a1,a5)),
% 116.73/116.80 inference(scs_inference,[],[444,21])).
% 116.73/116.80 cnf(465,plain,
% 116.73/116.80 (~P4(x4651,a4,x4652)+P4(x4651,f6(a4),f6(a4))+~P4(a4,x4652,a4)),
% 116.73/116.80 inference(scs_inference,[],[106,302,26])).
% 116.73/116.80 cnf(933,plain,
% 116.73/116.80 (~P3(a4,a1)+~P2(a1,a4,a1)),
% 116.73/116.80 inference(scs_inference,[],[2,38,12])).
% 116.73/116.80 cnf(950,plain,
% 116.73/116.80 (~P2(a4,x9501,a4)+~P2(a4,x9501,a1)+~P2(a1,a4,a1)),
% 116.73/116.80 inference(scs_inference,[],[933,47])).
% 116.73/116.80 cnf(1171,plain,
% 116.73/116.80 (~P2(x11711,a4,a1)+~P2(a4,x11711,a4)+~P2(a1,a4,a1)),
% 116.73/116.80 inference(scs_inference,[],[950,21])).
% 116.73/116.80 cnf(1424,plain,
% 116.73/116.80 (P4(f6(a4),x14241,f6(a4))+~P4(x14241,a4,x14242)+~P4(a4,x14242,a4)),
% 116.73/116.80 inference(scs_inference,[],[465,22])).
% 116.73/116.80 cnf(1865,plain,
% 116.73/116.80 (~P2(a1,x18651,a5)+~P2(x18651,a1,a2)),
% 116.73/116.80 inference(scs_inference,[],[6,350,25,21])).
% 116.73/116.80 cnf(1877,plain,
% 116.73/116.80 (~P2(a1,x18771,a5)+~P2(x18771,a1,f3(a1,a2))),
% 116.73/116.80 inference(scs_inference,[],[445,350,25,21])).
% 116.73/116.80 cnf(1901,plain,
% 116.73/116.80 (~P2(a1,x19011,a2)+~P2(a1,x19011,a5)),
% 116.73/116.80 inference(scs_inference,[],[1865,21])).
% 116.73/116.80 cnf(1932,plain,
% 116.73/116.80 (~P2(a1,a5,a2)),
% 116.73/116.80 inference(scs_inference,[],[4,1901,12])).
% 116.73/116.80 cnf(1933,plain,
% 116.73/116.80 (~P2(a5,a1,a2)),
% 116.73/116.80 inference(scs_inference,[],[1932,21])).
% 116.73/116.80 cnf(1935,plain,
% 116.73/116.80 (~P2(a1,x19351,a2)+~P2(a1,a5,x19351)),
% 116.73/116.80 inference(scs_inference,[],[1932,350,21,25])).
% 116.73/116.80 cnf(1953,plain,
% 116.73/116.80 (~P2(a1,f3(a1,a5),a2)),
% 116.73/116.80 inference(scs_inference,[],[4,1,1935,16])).
% 116.73/116.80 cnf(1954,plain,
% 116.73/116.80 (~P2(f3(a1,a5),a1,a2)),
% 116.73/116.80 inference(scs_inference,[],[1953,21])).
% 116.73/116.80 cnf(1962,plain,
% 116.73/116.80 (~P2(a1,x19621,a2)+~P2(x19621,a1,f3(a1,a5))),
% 116.73/116.80 inference(scs_inference,[],[1954,350,25,21])).
% 116.73/116.80 cnf(2013,plain,
% 116.73/116.80 (~P2(a1,x20131,a5)+~P2(x20131,f6(f6(a1)),a2)),
% 116.73/116.80 inference(scs_inference,[],[178,6,25,21])).
% 116.73/116.80 cnf(2036,plain,
% 116.73/116.80 (~P2(f6(f6(a1)),x20361,a4)+~P2(f6(a1),a1,x20361)),
% 116.73/116.80 inference(scs_inference,[],[178,5,25])).
% 116.73/116.80 cnf(2038,plain,
% 116.73/116.80 (~P2(x20381,f6(f6(a1)),a4)+~P2(f6(a1),a1,x20381)),
% 116.73/116.80 inference(scs_inference,[],[178,5,25,21])).
% 116.73/116.80 cnf(2099,plain,
% 116.73/116.80 (~P2(a1,x20991,f3(a1,a2))+~P2(a1,x20991,a5)),
% 116.73/116.80 inference(scs_inference,[],[1877,21])).
% 116.73/116.80 cnf(2147,plain,
% 116.73/116.80 (~P2(a1,x21471,f3(a1,a5))+~P2(a1,x21471,a2)),
% 116.73/116.80 inference(scs_inference,[],[1962,21])).
% 116.73/116.80 cnf(2283,plain,
% 116.73/116.80 (~P2(f3(a1,a5),f6(f6(a1)),x22831)+~P2(x22831,f6(a1),a2)),
% 116.73/116.80 inference(scs_inference,[],[1954,178,24])).
% 116.73/116.80 cnf(2285,plain,
% 116.73/116.80 (~P2(f6(f6(a1)),f3(a1,a5),x22851)+~P2(x22851,f6(a1),a2)),
% 116.73/116.80 inference(scs_inference,[],[1954,178,24,21])).
% 116.73/116.80 cnf(2288,plain,
% 116.73/116.80 (~P2(a1,a5,f3(a1,a2))),
% 116.73/116.80 inference(scs_inference,[],[4,2099,12])).
% 116.73/116.80 cnf(2289,plain,
% 116.73/116.80 (~P2(a5,a1,f3(a1,a2))),
% 116.73/116.80 inference(scs_inference,[],[2288,21])).
% 116.73/116.80 cnf(2323,plain,
% 116.73/116.80 (~P2(a1,a2,f3(a1,a5))),
% 116.73/116.80 inference(scs_inference,[],[3,2147,12])).
% 116.73/116.80 cnf(2324,plain,
% 116.73/116.80 (~P2(a2,a1,f3(a1,a5))),
% 116.73/116.80 inference(scs_inference,[],[2323,21])).
% 116.73/116.80 cnf(2419,plain,
% 116.73/116.80 (~P2(f3(a2,a1),f6(f6(a1)),x24191)+~P2(x24191,f6(a1),a5)),
% 116.73/116.80 inference(scs_inference,[],[424,178,24])).
% 116.73/116.80 cnf(2421,plain,
% 116.73/116.80 (~P2(f6(a1),x24211,a5)+~P2(f3(a2,a1),f6(f6(a1)),x24211)),
% 116.73/116.80 inference(scs_inference,[],[424,178,24,21])).
% 116.73/116.80 cnf(2632,plain,
% 116.73/116.80 (~P2(f6(f6(a1)),a1,x26321)+~P2(x26321,a1,a4)+~P2(f6(a1),a1,a1)),
% 116.73/116.80 inference(scs_inference,[],[350,2036,24])).
% 116.73/116.80 cnf(2692,plain,
% 116.73/116.80 (~P2(f3(a1,a2),f6(f6(a1)),x26921)+~P2(x26921,f6(a1),a5)),
% 116.73/116.80 inference(scs_inference,[],[445,178,24])).
% 116.73/116.80 cnf(2694,plain,
% 116.73/116.80 (~P2(f6(a1),x26941,a5)+~P2(f3(a1,a2),f6(f6(a1)),x26941)),
% 116.73/116.80 inference(scs_inference,[],[445,178,24,21])).
% 116.73/116.80 cnf(3197,plain,
% 116.73/116.80 (~P2(a5,a1,x31971)+~P2(x31971,a1,a2)),
% 116.73/116.80 inference(scs_inference,[],[1933,350,24])).
% 116.73/116.80 cnf(3208,plain,
% 116.73/116.80 (~P2(f6(f6(a1)),a5,x32081)+~P2(x32081,f6(a1),a2)),
% 116.73/116.80 inference(scs_inference,[],[1933,178,24,21])).
% 116.73/116.80 cnf(3222,plain,
% 116.73/116.80 (~P2(a1,x32221,a2)+~P2(a5,a1,x32221)),
% 116.73/116.80 inference(scs_inference,[],[3197,21])).
% 116.73/116.80 cnf(3253,plain,
% 116.73/116.80 (~P2(a1,f3(a5,a1),a2)),
% 116.73/116.80 inference(scs_inference,[],[1,4,3222,16])).
% 116.73/116.80 cnf(3254,plain,
% 116.73/116.80 (~P2(f3(a5,a1),a1,a2)),
% 116.73/116.80 inference(scs_inference,[],[3253,21])).
% 116.73/116.80 cnf(3261,plain,
% 116.73/116.80 (~P2(a1,x32611,a2)+~P2(x32611,a1,f3(a5,a1))),
% 116.73/116.80 inference(scs_inference,[],[3254,350,25,21])).
% 116.73/116.80 cnf(3344,plain,
% 116.73/116.80 (~P2(a2,a1,f3(a5,a1))),
% 116.73/116.80 inference(scs_inference,[],[3,3261,12])).
% 116.73/116.80 cnf(4067,plain,
% 116.73/116.80 (P4(f6(a4),a4,f6(a4))),
% 116.73/116.80 inference(scs_inference,[],[106,22])).
% 116.73/116.80 cnf(5020,plain,
% 116.73/116.80 (~P2(f6(f6(a1)),f3(a2,a1),x50201)+~P2(x50201,f6(a1),a5)),
% 116.73/116.80 inference(scs_inference,[],[2419,21])).
% 116.73/116.80 cnf(5084,plain,
% 116.73/116.80 (~P2(f6(f6(a1)),f3(a1,a2),x50841)+~P2(x50841,f6(a1),a5)),
% 116.73/116.80 inference(scs_inference,[],[2692,21])).
% 116.73/116.80 cnf(6227,plain,
% 116.73/116.80 (P4(a4,a4,a4)),
% 116.73/116.80 inference(scs_inference,[],[2,7,13])).
% 116.73/116.80 cnf(6229,plain,
% 116.73/116.80 (P2(f6(a4),a4,a1)),
% 116.73/116.80 inference(scs_inference,[],[2,7,13,14])).
% 116.73/116.80 cnf(6231,plain,
% 116.73/116.80 (P2(a1,a4,a4)),
% 116.73/116.80 inference(scs_inference,[],[2,7,13,14,12])).
% 116.73/116.80 cnf(6233,plain,
% 116.73/116.80 (P2(f6(a4),a1,f6(a4))),
% 116.73/116.80 inference(scs_inference,[],[2,79,7,13,14,12,21])).
% 116.73/116.80 cnf(6235,plain,
% 116.73/116.80 (P1(f3(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[2,79,7,13,14,12,21,9])).
% 116.73/116.80 cnf(6237,plain,
% 116.73/116.80 (P1(f7(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[2,79,7,13,14,12,21,9,10])).
% 116.73/116.80 cnf(6239,plain,
% 116.73/116.80 (P4(a4,a4,f7(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[2,79,7,13,14,12,21,9,10,17])).
% 116.73/116.80 cnf(6241,plain,
% 116.73/116.80 (P2(a4,a4,f3(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[2,79,7,13,14,12,21,9,10,17,16])).
% 116.73/116.80 cnf(6243,plain,
% 116.73/116.80 (P2(a1,a2,a2)),
% 116.73/116.80 inference(scs_inference,[],[2,45,79,7,13,14,12,21,9,10,17,16,18])).
% 116.73/116.80 cnf(6245,plain,
% 116.73/116.80 (P2(a1,f3(a4,a4),f3(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[2,45,79,7,13,14,12,21,9,10,17,16,18,24])).
% 116.73/116.80 cnf(6249,plain,
% 116.73/116.80 (P4(f7(a4,a4),a4,f7(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[2,45,79,7,13,14,12,21,9,10,17,16,18,24,8,27])).
% 116.73/116.80 cnf(6264,plain,
% 116.73/116.80 (P1(f6(a1))),
% 116.73/116.80 inference(scs_inference,[],[1,7])).
% 116.73/116.80 cnf(6266,plain,
% 116.73/116.80 (P2(f6(a1),a1,a1)),
% 116.73/116.80 inference(scs_inference,[],[1,7,14])).
% 116.73/116.80 cnf(6268,plain,
% 116.73/116.80 (P4(a4,f3(a4,a4),f3(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[6235,1,7,14,13])).
% 116.73/116.80 cnf(6270,plain,
% 116.73/116.80 (P2(a1,f7(a4,a4),f7(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[6235,6237,1,7,14,13,12])).
% 116.73/116.80 cnf(6272,plain,
% 116.73/116.80 (P2(a4,a1,a4)),
% 116.73/116.80 inference(scs_inference,[],[6231,6235,6237,1,7,14,13,12,21])).
% 116.73/116.80 cnf(6274,plain,
% 116.73/116.80 (P4(a1,a1,f7(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6231,6235,6237,1,7,14,13,12,21,17])).
% 116.73/116.80 cnf(6276,plain,
% 116.73/116.80 (P1(f7(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6231,6235,6237,1,7,14,13,12,21,17,10])).
% 116.73/116.80 cnf(6278,plain,
% 116.73/116.80 (P1(f3(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6231,6235,6237,1,7,14,13,12,21,17,10,9])).
% 116.73/116.80 cnf(6280,plain,
% 116.73/116.80 (~P2(a1,a4,a1)),
% 116.73/116.80 inference(scs_inference,[],[6231,6235,6237,1,7,14,13,12,21,17,10,9,1171])).
% 116.73/116.80 cnf(6282,plain,
% 116.73/116.80 (P2(a1,a1,f3(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6231,6235,6237,1,7,14,13,12,21,17,10,9,1171,16])).
% 116.73/116.80 cnf(6284,plain,
% 116.73/116.80 (P2(a1,a5,a5)),
% 116.73/116.80 inference(scs_inference,[],[6231,6235,6237,1,48,7,14,13,12,21,17,10,9,1171,16,18])).
% 116.73/116.80 cnf(6286,plain,
% 116.73/116.80 (~P2(f6(a4),a4,a4)),
% 116.73/116.80 inference(scs_inference,[],[6231,6229,6235,6237,1,48,79,7,14,13,12,21,17,10,9,1171,16,18,24])).
% 116.73/116.80 cnf(6288,plain,
% 116.73/116.80 (P3(a1,f7(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6231,6229,6235,6237,32,1,48,79,7,14,13,12,21,17,10,9,1171,16,18,24,20])).
% 116.73/116.80 cnf(6290,plain,
% 116.73/116.80 (~P4(a1,a4,a4)),
% 116.73/116.80 inference(scs_inference,[],[6227,6231,6229,6235,6237,32,1,48,79,4067,7,14,13,12,21,17,10,9,1171,16,18,24,20,28])).
% 116.73/116.80 cnf(6292,plain,
% 116.73/116.80 (~P4(a4,a1,a4)),
% 116.73/116.80 inference(scs_inference,[],[6227,6231,6229,6235,6237,32,1,48,79,4067,7,14,13,12,21,17,10,9,1171,16,18,24,20,28,22])).
% 116.73/116.80 cnf(6294,plain,
% 116.73/116.80 (P4(f8(a4),a4,a4)),
% 116.73/116.80 inference(scs_inference,[],[6227,6231,6229,6235,6237,32,1,2,48,79,4067,7,14,13,12,21,17,10,9,1171,16,18,24,20,28,22,19])).
% 116.73/116.80 cnf(6298,plain,
% 116.73/116.80 (P4(f8(a4),f6(a4),f6(a4))),
% 116.73/116.80 inference(scs_inference,[],[6227,6231,6229,6235,6237,32,1,2,48,79,4067,7,14,13,12,21,17,10,9,1171,16,18,24,20,28,22,19,206,465])).
% 116.73/116.80 cnf(6300,plain,
% 116.73/116.80 (P1(f8(a4))),
% 116.73/116.80 inference(scs_inference,[],[6227,6231,6229,6235,6237,32,1,2,48,79,4067,7,14,13,12,21,17,10,9,1171,16,18,24,20,28,22,19,206,465,15])).
% 116.73/116.80 cnf(6304,plain,
% 116.73/116.80 (P3(f3(a1,a1),f3(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6227,6231,6229,6235,6237,32,1,2,48,79,4067,7,14,13,12,21,17,10,9,1171,16,18,24,20,28,22,19,206,465,15,52,23])).
% 116.73/116.80 cnf(6306,plain,
% 116.73/116.80 (P4(a4,f7(a4,a4),f7(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[6227,6231,6229,6235,6237,6239,32,1,2,48,79,4067,7,14,13,12,21,17,10,9,1171,16,18,24,20,28,22,19,206,465,15,52,23,26])).
% 116.73/116.80 cnf(6308,plain,
% 116.73/116.80 (~P4(a4,a4,a1)),
% 116.73/116.80 inference(scs_inference,[],[6227,6231,6229,6235,6237,6239,32,1,2,48,79,4067,7,14,13,12,21,17,10,9,1171,16,18,24,20,28,22,19,206,465,15,52,23,26,27])).
% 116.73/116.80 cnf(6310,plain,
% 116.73/116.80 (~P2(a4,f6(a4),f6(a4))),
% 116.73/116.80 inference(scs_inference,[],[6227,6231,6229,6235,6237,6239,32,1,2,48,79,4067,7,14,13,12,21,17,10,9,1171,16,18,24,20,28,22,19,206,465,15,52,23,26,27,25])).
% 116.73/116.80 cnf(6312,plain,
% 116.73/116.80 (P4(f3(a4,a4),a4,f3(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[6227,6231,6241,6229,6235,6237,6239,32,1,2,48,79,4067,7,14,13,12,21,17,10,9,1171,16,18,24,20,28,22,19,206,465,15,52,23,26,27,25,29])).
% 116.73/116.80 cnf(6317,plain,
% 116.73/116.80 (~P2(f6(f6(a1)),a1,x63171)+~P2(x63171,a1,a4)),
% 116.73/116.80 inference(scs_inference,[],[6266,2632])).
% 116.73/116.80 cnf(6319,plain,
% 116.73/116.80 (P1(f6(a5))),
% 116.73/116.80 inference(scs_inference,[],[4,7])).
% 116.73/116.80 cnf(6321,plain,
% 116.73/116.80 (P2(f6(a5),a5,a1)),
% 116.73/116.80 inference(scs_inference,[],[4,7,14])).
% 116.73/116.80 cnf(6323,plain,
% 116.73/116.80 (P4(a4,f7(a1,a1),f7(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6276,4,7,14,13])).
% 116.73/116.80 cnf(6325,plain,
% 116.73/116.80 (P2(a1,f7(a1,a1),f7(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6276,4,7,14,13,12])).
% 116.73/116.80 cnf(6327,plain,
% 116.73/116.80 (P2(a5,a1,a5)),
% 116.73/116.80 inference(scs_inference,[],[6284,6276,4,7,14,13,12,21])).
% 116.73/116.80 cnf(6329,plain,
% 116.73/116.80 (P1(f7(a5,a5))),
% 116.73/116.80 inference(scs_inference,[],[6284,6276,4,7,14,13,12,21,10])).
% 116.73/116.80 cnf(6331,plain,
% 116.73/116.80 (P1(f3(a5,a5))),
% 116.73/116.80 inference(scs_inference,[],[6284,6276,4,7,14,13,12,21,10,9])).
% 116.73/116.80 cnf(6333,plain,
% 116.73/116.80 (P4(a5,a5,f7(a5,a5))),
% 116.73/116.80 inference(scs_inference,[],[6284,6276,4,7,14,13,12,21,10,9,17])).
% 116.73/116.80 cnf(6335,plain,
% 116.73/116.80 (P2(a5,a5,f3(a5,a5))),
% 116.73/116.80 inference(scs_inference,[],[6284,6276,4,7,14,13,12,21,10,9,17,16])).
% 116.73/116.80 cnf(6337,plain,
% 116.73/116.80 (P2(a1,f3(a1,a1),f3(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6284,6304,6276,4,7,14,13,12,21,10,9,17,16,18])).
% 116.73/116.80 cnf(6339,plain,
% 116.73/116.80 (~P2(a2,a1,a1)),
% 116.73/116.80 inference(scs_inference,[],[6,6284,6304,6276,4,7,14,13,12,21,10,9,17,16,18,24])).
% 116.73/116.80 cnf(6344,plain,
% 116.73/116.80 (~P4(f8(a4),f8(a4),a1)),
% 116.73/116.80 inference(scs_inference,[],[6,6290,6284,6304,6276,6294,32,4,7,14,13,12,21,10,9,17,16,18,24,23,27])).
% 116.73/116.80 cnf(6346,plain,
% 116.73/116.80 (P2(f3(a1,a1),a1,f3(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6,6290,6284,6304,6276,6282,6294,32,4,7,14,13,12,21,10,9,17,16,18,24,23,27,25])).
% 116.73/116.80 cnf(6348,plain,
% 116.73/116.80 (P2(f7(a4,a4),f7(a4,a4),f3(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[6,6290,6284,6304,6276,6312,6282,6294,6239,6241,32,4,7,14,13,12,21,10,9,17,16,18,24,23,27,25,28])).
% 116.73/116.80 cnf(6350,plain,
% 116.73/116.80 (P4(f3(a4,a4),f7(a4,a4),f3(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[6,6290,6284,6304,6306,6276,6312,6282,6294,6239,6241,32,4,7,14,13,12,21,10,9,17,16,18,24,23,27,25,28,29])).
% 116.73/116.80 cnf(6352,plain,
% 116.73/116.80 (P3(f3(a5,a5),f3(a5,a5))),
% 116.73/116.80 inference(scs_inference,[],[6,6290,6284,6304,6306,6276,6312,6282,6294,6239,6241,32,4,7,14,13,12,21,10,9,17,16,18,24,23,27,25,28,29,51])).
% 116.73/116.80 cnf(6354,plain,
% 116.73/116.80 (P4(f6(a4),f8(a4),f6(a4))),
% 116.73/116.80 inference(scs_inference,[],[6,6290,6284,6304,6306,6276,6312,6282,6294,6239,6241,6227,32,4,7,14,13,12,21,10,9,17,16,18,24,23,27,25,28,29,51,1424])).
% 116.73/116.80 cnf(6362,plain,
% 116.73/116.80 (P1(f6(a2))),
% 116.73/116.80 inference(scs_inference,[],[3,7])).
% 116.73/116.80 cnf(6364,plain,
% 116.73/116.80 (P4(a4,f3(a1,a1),f3(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6278,3,7,13])).
% 116.73/116.80 cnf(6366,plain,
% 116.73/116.80 (P2(a1,f6(a1),f6(a1))),
% 116.73/116.80 inference(scs_inference,[],[6278,6264,3,7,13,12])).
% 116.73/116.80 cnf(6368,plain,
% 116.73/116.80 (P2(f6(a2),a2,a1)),
% 116.73/116.80 inference(scs_inference,[],[6278,6264,3,7,13,12,14])).
% 116.73/116.80 cnf(6370,plain,
% 116.73/116.80 (P2(f7(a4,a4),a1,f7(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[6270,6278,6264,3,7,13,12,14,21])).
% 116.73/116.80 cnf(6372,plain,
% 116.73/116.80 (P4(a2,a2,f7(a2,a2))),
% 116.73/116.80 inference(scs_inference,[],[6270,6278,6264,3,7,13,12,14,21,17])).
% 116.73/116.80 cnf(6374,plain,
% 116.73/116.80 (P1(f3(a2,a2))),
% 116.73/116.80 inference(scs_inference,[],[6270,6278,6264,3,7,13,12,14,21,17,9])).
% 116.73/116.80 cnf(6376,plain,
% 116.73/116.80 (P1(f7(a2,a2))),
% 116.73/116.80 inference(scs_inference,[],[6270,6278,6264,3,7,13,12,14,21,17,9,10])).
% 116.73/116.80 cnf(6378,plain,
% 116.73/116.80 (P2(a1,f3(a5,a5),f3(a5,a5))),
% 116.73/116.80 inference(scs_inference,[],[6352,6270,6278,6264,3,7,13,12,14,21,17,9,10,18])).
% 116.73/116.80 cnf(6380,plain,
% 116.73/116.80 (P2(a2,a2,f3(a2,a2))),
% 116.73/116.80 inference(scs_inference,[],[6352,6270,6278,6264,3,7,13,12,14,21,17,9,10,18,16])).
% 116.73/116.80 cnf(6382,plain,
% 116.73/116.80 (P2(a4,f3(a1,a1),a4)),
% 116.73/116.80 inference(scs_inference,[],[6272,6352,6270,6278,6264,6282,3,7,13,12,14,21,17,9,10,18,16,24])).
% 116.73/116.80 cnf(6384,plain,
% 116.73/116.80 (P4(f7(a4,a4),f3(a4,a4),f3(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[6272,6352,6270,6278,6268,6264,6282,6239,3,7,13,12,14,21,17,9,10,18,16,24,27])).
% 116.73/116.80 cnf(6386,plain,
% 116.73/116.80 (P2(f3(a4,a4),a1,f3(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[6272,6348,6352,6270,6278,6268,6264,6282,6239,3,7,13,12,14,21,17,9,10,18,16,24,27,25])).
% 116.73/116.80 cnf(6388,plain,
% 116.73/116.80 (P3(f3(a2,a2),f3(a2,a2))),
% 116.73/116.80 inference(scs_inference,[],[6272,6348,6352,6270,6278,6268,6264,6282,6239,3,7,13,12,14,21,17,9,10,18,16,24,27,25,50])).
% 116.73/116.80 cnf(6394,plain,
% 116.73/116.80 (P2(a1,f7(a2,a2),f7(a2,a2))),
% 116.73/116.80 inference(scs_inference,[],[6376,12])).
% 116.73/116.80 cnf(6396,plain,
% 116.73/116.80 (P4(a4,f7(a2,a2),f7(a2,a2))),
% 116.73/116.80 inference(scs_inference,[],[6376,12,13])).
% 116.73/116.80 cnf(6398,plain,
% 116.73/116.80 (P2(a1,f6(a1),a1)),
% 116.73/116.80 inference(scs_inference,[],[6266,6376,12,13,21])).
% 116.73/116.80 cnf(6400,plain,
% 116.73/116.80 (P2(a1,f3(a2,a2),f3(a2,a2))),
% 116.73/116.80 inference(scs_inference,[],[6266,6388,6376,12,13,21,18])).
% 116.73/116.80 cnf(6402,plain,
% 116.73/116.80 (~P2(a2,f6(a1),f6(a1))),
% 116.73/116.80 inference(scs_inference,[],[6339,6266,6388,6376,12,13,21,18,24])).
% 116.73/116.80 cnf(6404,plain,
% 116.73/116.80 (P4(f7(a4,a4),f3(a1,a1),f3(a1,a1))),
% 116.73/116.80 inference(scs_inference,[],[6339,6266,6388,6376,6364,6239,12,13,21,18,24,27])).
% 116.73/116.80 cnf(6406,plain,
% 116.73/116.80 (~P2(f6(a1),f6(a1),a2)),
% 116.73/116.80 inference(scs_inference,[],[6339,6266,6388,6376,6364,6239,12,13,21,18,24,27,25])).
% 116.73/116.80 cnf(6413,plain,
% 116.73/116.80 (P2(a1,f8(a4),f8(a4))),
% 116.73/116.80 inference(scs_inference,[],[6300,12])).
% 116.73/116.80 cnf(6415,plain,
% 116.73/116.80 (P4(a4,f8(a4),f8(a4))),
% 116.73/116.80 inference(scs_inference,[],[6300,12,13])).
% 116.73/116.80 cnf(6417,plain,
% 116.73/116.80 (P2(a5,f6(a5),a1)),
% 116.73/116.80 inference(scs_inference,[],[6321,6300,12,13,21])).
% 116.73/116.80 cnf(6419,plain,
% 116.73/116.80 (~P2(a1,a2,f6(a1))),
% 116.73/116.80 inference(scs_inference,[],[6321,6300,6406,6243,6266,12,13,21,24])).
% 116.73/116.80 cnf(6421,plain,
% 116.73/116.80 (P2(f3(a4,a4),f6(a1),f3(a4,a4))),
% 116.73/116.80 inference(scs_inference,[],[6321,6398,6386,6300,6406,6243,6266,12,13,21,24,25])).
% 116.73/116.80 cnf(6428,plain,
% 116.73/116.80 (P2(a1,f6(a5),f6(a5))),
% 116.73/116.80 inference(scs_inference,[],[6319,12])).
% 116.73/116.80 cnf(6430,plain,
% 116.73/116.80 (P4(a4,f6(a5),f6(a5))),
% 116.73/116.80 inference(scs_inference,[],[6319,12,13])).
% 116.73/116.80 cnf(6432,plain,
% 116.73/116.80 (P2(a2,f6(a2),a1)),
% 116.73/116.81 inference(scs_inference,[],[6368,6319,12,13,21])).
% 116.73/116.81 cnf(6442,plain,
% 116.73/116.81 (~P4(f8(a4),a4,a1)),
% 116.73/116.81 inference(scs_inference,[],[6280,6308,6368,6335,6319,6394,6415,6417,2289,6288,6294,32,12,13,21,24,23,25,18,26])).
% 116.73/116.81 cnf(6444,plain,
% 116.73/116.81 (~P4(a4,f8(a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[6280,6308,6368,6335,6319,6394,6415,6417,2289,6288,6294,32,12,13,21,24,23,25,18,26,22])).
% 116.73/116.81 cnf(6447,plain,
% 116.73/116.81 (P2(a1,f7(a5,a5),f7(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6329,12])).
% 116.73/116.81 cnf(6449,plain,
% 116.73/116.81 (P4(a4,f7(a5,a5),f7(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6329,12,13])).
% 116.73/116.81 cnf(6451,plain,
% 116.73/116.81 (P2(f3(a2,a2),a1,f3(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6400,6329,12,13,21])).
% 116.73/116.81 cnf(6455,plain,
% 116.73/116.81 (P2(f7(a4,a4),f3(a1,a1),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6400,6370,6329,6413,6282,12,13,21,52,24])).
% 116.73/116.81 cnf(6459,plain,
% 116.73/116.81 (~P4(a1,f8(a4),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6400,6370,6329,6413,6428,6290,6282,6294,32,12,13,21,52,24,23,26])).
% 116.73/116.81 cnf(6461,plain,
% 116.73/116.81 (P2(f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6337,6400,6370,6329,6413,6428,6290,6282,6294,32,12,13,21,52,24,23,26,25])).
% 116.73/116.81 cnf(6467,plain,
% 116.73/116.81 (~P4(a1,a4,f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6337,6400,6370,6329,6413,6428,6442,6290,6282,6288,6294,6229,32,12,13,21,52,24,23,26,25,22,20,29])).
% 116.73/116.81 cnf(6472,plain,
% 116.73/116.81 (P2(a1,f6(a2),f6(a2))),
% 116.73/116.81 inference(scs_inference,[],[6362,12])).
% 116.73/116.81 cnf(6474,plain,
% 116.73/116.81 (~P4(a4,a1,f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6362,6467,12,22])).
% 116.73/116.81 cnf(6476,plain,
% 116.73/116.81 (P4(a4,f3(a5,a5),f3(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6331,6362,6467,12,22,13])).
% 116.73/116.81 cnf(6478,plain,
% 116.73/116.81 (P2(f3(a1,a1),f7(a4,a4),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6455,6331,6362,6467,12,22,13,21])).
% 116.73/116.81 cnf(6482,plain,
% 116.73/116.81 (~P4(f8(a4),f6(a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[6455,6380,6298,6331,6362,6432,6467,6415,2324,12,22,13,21,24,26])).
% 116.73/116.81 cnf(6484,plain,
% 116.73/116.81 (~P4(a4,f6(a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[6455,6380,6298,6331,6362,6432,6467,6415,2324,12,22,13,21,24,26,27])).
% 116.73/116.81 cnf(6486,plain,
% 116.73/116.81 (P2(f6(a5),a5,f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6455,6380,6298,6331,6362,6432,6467,6321,6428,6415,2324,6282,12,22,13,21,24,26,27,25])).
% 116.73/116.81 cnf(6488,plain,
% 116.73/116.81 (P2(f7(a1,a1),f7(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6455,6274,6380,6298,6331,6362,6432,6467,6321,6428,6415,2324,6282,350,12,22,13,21,24,26,27,25,28])).
% 116.73/116.81 cnf(6490,plain,
% 116.73/116.81 (~P4(f3(a1,a1),f6(a4),a4)),
% 116.73/116.81 inference(scs_inference,[],[6455,6274,6380,6298,6331,6362,6432,6467,6382,6321,6428,6415,2324,6282,6229,106,350,12,22,13,21,24,26,27,25,28,29])).
% 116.73/116.81 cnf(6496,plain,
% 116.73/116.81 (~P4(f6(a4),f8(a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[6482,22])).
% 116.73/116.81 cnf(6498,plain,
% 116.73/116.81 (P4(a4,f3(a2,a2),f3(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6482,6374,22,13])).
% 116.73/116.81 cnf(6500,plain,
% 116.73/116.81 (P2(f3(a5,a5),a1,f3(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6378,6482,6374,22,13,21])).
% 116.73/116.81 cnf(6502,plain,
% 116.73/116.81 (P2(f3(a2,a2),f3(a1,a1),f3(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6378,6482,6451,6374,6282,22,13,21,24])).
% 116.73/116.81 cnf(6504,plain,
% 116.73/116.81 (P4(f7(a4,a4),f7(a4,a4),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6378,6482,6451,6374,6249,6239,6282,22,13,21,24,26])).
% 116.73/116.81 cnf(6508,plain,
% 116.73/116.81 (P2(f3(a1,a1),f6(a1),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6378,6346,6482,6476,6451,6374,6249,6398,6239,6282,22,13,21,24,26,27,25])).
% 116.73/116.81 cnf(6510,plain,
% 116.73/116.81 (~P4(a1,f8(a4),a4)),
% 116.73/116.81 inference(scs_inference,[],[6378,6354,6346,6482,6476,6451,6374,6249,6233,6398,6239,6282,6229,22,13,21,24,26,27,25,29])).
% 116.73/116.81 cnf(6514,plain,
% 116.73/116.81 (P2(a1,a2,a1)+P1(f8(a2))),
% 116.73/116.81 inference(scs_inference,[],[6333,6378,6354,6346,6482,6476,6451,6374,6249,6233,6335,6398,6239,6282,6229,3,22,13,21,24,26,27,25,29,28,15])).
% 116.73/116.81 cnf(6518,plain,
% 116.73/116.81 (P4(a4,f6(a1),f6(a1))),
% 116.73/116.81 inference(scs_inference,[],[6490,6264,22,13])).
% 116.73/116.81 cnf(6520,plain,
% 116.73/116.81 (P2(f3(a1,a1),f3(a2,a2),f3(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6502,6490,6264,22,13,21])).
% 116.73/116.81 cnf(6522,plain,
% 116.73/116.81 (P2(f3(a5,a5),f3(a1,a1),f3(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6502,6500,6490,6264,6282,22,13,21,24])).
% 116.73/116.81 cnf(6524,plain,
% 116.73/116.81 (~P4(f3(a1,a1),f6(a4),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6502,6500,6490,6264,6282,6294,4067,22,13,21,24,26])).
% 116.73/116.81 cnf(6528,plain,
% 116.73/116.81 (P2(f3(a1,a1),f6(a2),f6(a2))),
% 116.73/116.81 inference(scs_inference,[],[6502,6472,6500,6498,6490,6264,6282,6239,6294,4067,22,13,21,24,26,27,25])).
% 116.73/116.81 cnf(6530,plain,
% 116.73/116.81 (P4(f3(a4,a4),f7(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6488,6502,6472,6500,6498,6323,6490,6264,6241,6282,6239,6294,4067,22,13,21,24,26,27,25,29])).
% 116.73/116.81 cnf(6538,plain,
% 116.73/116.81 (~P4(f6(a4),f3(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6524,22])).
% 116.73/116.81 cnf(6540,plain,
% 116.73/116.81 (P2(f3(a1,a1),f3(a5,a5),f3(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6522,6524,22,21])).
% 116.73/116.81 cnf(6542,plain,
% 116.73/116.81 (P4(a4,f6(a2),f6(a2))),
% 116.73/116.81 inference(scs_inference,[],[6522,6524,6362,22,21,13])).
% 116.73/116.81 cnf(6546,plain,
% 116.73/116.81 (P2(f3(a5,a5),f6(a1),f3(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6522,6508,6524,6380,6432,6339,6362,22,21,13,24,25])).
% 116.73/116.81 cnf(6551,plain,
% 116.73/116.81 (~P4(f6(a4),a4,a1)),
% 116.73/116.81 inference(scs_inference,[],[6484,22])).
% 116.73/116.81 cnf(6553,plain,
% 116.73/116.81 (P4(a4,a1,a1)),
% 116.73/116.81 inference(scs_inference,[],[6484,1,22,13])).
% 116.73/116.81 cnf(6557,plain,
% 116.73/116.81 (P2(f3(a1,a1),a1,a1)),
% 116.73/116.81 inference(scs_inference,[],[6484,6421,6528,6368,1,22,13,21,24])).
% 116.73/116.81 cnf(6559,plain,
% 116.73/116.81 (P4(f7(a4,a4),f7(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6484,6421,6528,6384,6530,6368,1,22,13,21,24,26])).
% 116.73/116.81 cnf(6561,plain,
% 116.73/116.81 (P2(f3(a4,a4),f3(a1,a1),f3(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6484,6421,6528,6384,6530,6455,6348,6368,1,22,13,21,24,26,25])).
% 116.73/116.81 cnf(6563,plain,
% 116.73/116.81 (P2(f7(a1,a1),a1,a1)),
% 116.73/116.81 inference(scs_inference,[],[6484,6421,6528,6384,6530,6455,6348,6231,6368,6274,1,22,13,21,24,26,25,28])).
% 116.73/116.81 cnf(6565,plain,
% 116.73/116.81 (~P2(a1,f7(a1,a1),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6484,6421,6474,6528,6384,6530,6455,6348,6231,6272,6368,6274,1,22,13,21,24,26,25,28,29])).
% 116.73/116.81 cnf(6573,plain,
% 116.73/116.81 (P2(f3(a1,a1),f3(a4,a4),f3(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6561,6510,22,21])).
% 116.73/116.81 cnf(6575,plain,
% 116.73/116.81 (P4(a4,a5,a5)),
% 116.73/116.81 inference(scs_inference,[],[6561,6510,4,22,21,13])).
% 116.73/116.81 cnf(6577,plain,
% 116.73/116.81 (P2(f3(a1,a1),f7(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6561,6510,6557,6325,4,22,21,13,24])).
% 116.73/116.81 cnf(6579,plain,
% 116.73/116.81 (~P4(a4,a1,f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6553,6561,6344,6510,6557,6325,6294,4,22,21,13,24,26])).
% 116.73/116.81 cnf(6581,plain,
% 116.73/116.81 (P2(f3(a1,a1),f7(a2,a2),f7(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6553,6561,6344,6510,6557,6325,6394,6282,6294,4,22,21,13,24,26,25])).
% 116.73/116.81 cnf(6583,plain,
% 116.73/116.81 (~P4(f3(a4,a4),a1,a4)),
% 116.73/116.81 inference(scs_inference,[],[6553,6561,6344,6510,6557,6325,6394,6241,6282,6294,5,4,22,21,13,24,26,25,28])).
% 116.73/116.81 cnf(6593,plain,
% 116.73/116.81 (P4(a4,a2,a2)),
% 116.73/116.81 inference(scs_inference,[],[6579,3,22,13])).
% 116.73/116.81 cnf(6595,plain,
% 116.73/116.81 (P2(f7(a1,a1),f3(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6577,6579,3,22,13,21])).
% 116.73/116.81 cnf(6599,plain,
% 116.73/116.81 (P2(f7(a1,a1),a1,f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6577,6563,6579,6346,6380,6432,3344,3,22,13,21,24,25])).
% 116.73/116.81 cnf(6601,plain,
% 116.73/116.81 (~P4(f3(a4,a4),f6(a1),a2)),
% 116.73/116.81 inference(scs_inference,[],[6577,6518,6563,6579,6346,6406,6380,6432,3344,6241,3,22,13,21,24,25,28])).
% 116.73/116.81 cnf(6603,plain,
% 116.73/116.81 (~P4(f3(a1,a1),a1,f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6577,6518,6563,6579,6346,6406,6413,6380,6432,6382,3344,6553,6241,3,22,13,21,24,25,28,29])).
% 116.73/116.81 cnf(6611,plain,
% 116.73/116.81 (P2(f7(a2,a2),f3(a1,a1),f7(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6581,6601,22,21])).
% 116.73/116.81 cnf(6613,plain,
% 116.73/116.81 (P2(f7(a1,a1),f3(a4,a4),f3(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6573,6581,6601,6599,6245,22,21,24])).
% 116.73/116.81 cnf(6615,plain,
% 116.73/116.81 (~P4(f7(a4,a4),f8(a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[6573,6581,6601,6599,6444,6245,6415,6239,22,21,24,26])).
% 116.73/116.81 cnf(6617,plain,
% 116.73/116.81 (P2(f3(a2,a2),f6(a1),f3(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6573,6581,6601,6599,6444,6245,6451,6415,6398,6239,22,21,24,26,25])).
% 116.73/116.81 cnf(6619,plain,
% 116.73/116.81 (~P4(a1,a5,a2)),
% 116.73/116.81 inference(scs_inference,[],[6,6575,6573,6581,6601,6599,6444,6245,6451,6231,6415,6398,6239,22,21,24,26,25,28])).
% 116.73/116.81 cnf(6622,plain,
% 116.73/116.81 (~P2(f7(a1,a1),a1,a4)),
% 116.73/116.81 inference(scs_inference,[],[6,6575,6573,6581,6601,6599,6444,6245,6292,6451,6231,6415,6398,6553,6274,6239,22,21,24,26,25,28,29])).
% 116.73/116.81 cnf(6628,plain,
% 116.73/116.81 (P2(f3(a4,a4),f7(a1,a1),f3(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6619,6613,22,21])).
% 116.73/116.81 cnf(6630,plain,
% 116.73/116.81 (P2(f7(a1,a1),f7(a4,a4),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6619,6613,6563,6270,22,21,24])).
% 116.73/116.81 cnf(6632,plain,
% 116.73/116.81 (P2(a1,f6(a1),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6619,6613,6508,6563,6557,6270,6366,22,21,24,25])).
% 116.73/116.81 cnf(6634,plain,
% 116.73/116.81 (~P4(f3(a4,a4),a2,a5)),
% 116.73/116.81 inference(scs_inference,[],[6,6593,6619,6613,6508,6563,6557,6270,6366,6241,22,21,24,25,28])).
% 116.73/116.81 cnf(6637,plain,
% 116.73/116.81 (~P2(f7(a1,a1),f7(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6,6593,6619,6613,6603,6508,6563,6557,6270,6366,6274,6241,6282,22,21,24,25,28,29])).
% 116.73/116.81 cnf(6643,plain,
% 116.73/116.81 (~P4(f8(a4),f7(a4,a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[6615,22])).
% 116.73/116.81 cnf(6645,plain,
% 116.73/116.81 (P2(f7(a4,a4),f7(a1,a1),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6630,6615,22,21])).
% 116.73/116.81 cnf(6647,plain,
% 116.73/116.81 (~P2(f6(a1),a1,a4)),
% 116.73/116.81 inference(scs_inference,[],[6630,6615,6632,6280,6557,22,21,24])).
% 116.73/116.81 cnf(6649,plain,
% 116.73/116.81 (P2(f7(a4,a4),f6(a1),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6630,6615,6632,6370,6280,6455,6557,22,21,24,25])).
% 116.73/116.81 cnf(6651,plain,
% 116.73/116.81 (~P4(f3(a4,a4),f7(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6630,6615,6637,6632,6559,6370,6280,6455,6348,6557,22,21,24,25,28])).
% 116.73/116.81 cnf(6655,plain,
% 116.73/116.81 (~P4(a4,f7(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6630,6615,6637,6632,6559,6268,6370,6280,6455,6354,6348,6557,6530,22,21,24,25,28,26,27])).
% 116.73/116.81 cnf(6662,plain,
% 116.73/116.81 (P2(f7(a1,a1),f3(a5,a5),f3(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6651,6617,6540,6599,6378,22,21,24])).
% 116.73/116.81 cnf(6664,plain,
% 116.73/116.81 (~P4(f7(a4,a4),f7(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6651,6617,6655,6540,6306,6599,6378,6559,22,21,24,26])).
% 116.73/116.81 cnf(6666,plain,
% 116.73/116.81 (~P2(f6(a5),a4,f6(a5))),
% 116.73/116.81 inference(scs_inference,[],[6651,6617,6655,6540,6306,6599,6378,6417,6559,6280,22,21,24,26,25])).
% 116.73/116.81 cnf(6668,plain,
% 116.73/116.81 (~P4(a1,f6(a4),a4)),
% 116.73/116.81 inference(scs_inference,[],[6310,6651,6617,6655,6540,6306,6599,6378,6417,6559,6298,6280,6413,22,21,24,26,25,28])).
% 116.73/116.81 cnf(6677,plain,
% 116.73/116.81 (~P2(f6(a4),a1,f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6668,6662,6565,6233,79,22,21,24])).
% 116.73/116.81 cnf(6679,plain,
% 116.73/116.81 (~P4(a4,a1,f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6668,6662,6565,6643,6233,6553,6294,79,22,21,24,26])).
% 116.73/116.81 cnf(6681,plain,
% 116.73/116.81 (P2(f3(a1,a1),f7(a5,a5),f7(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6668,6662,6565,6643,6447,6233,6553,6294,6282,79,22,21,24,26,25])).
% 116.73/116.81 cnf(6690,plain,
% 116.73/116.81 (P2(f7(a5,a5),f3(a1,a1),f7(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6681,6664,22,21])).
% 116.73/116.81 cnf(6692,plain,
% 116.73/116.81 (~P2(f6(a4),f6(a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6681,6664,6677,6233,6398,22,21,24])).
% 116.73/116.81 cnf(6694,plain,
% 116.73/116.81 (~P4(a4,f7(a4,a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[6681,6664,6677,6679,6306,6233,6398,6227,22,21,24,26])).
% 116.73/116.81 cnf(6696,plain,
% 116.73/116.81 (P2(f7(a2,a2),a1,f7(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6681,6611,6664,6677,6679,6306,6346,6233,6398,6227,22,21,24,26,25])).
% 116.73/116.81 cnf(6698,plain,
% 116.73/116.81 (P4(f3(a4,a4),f3(a1,a1),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6681,6611,6664,6677,6679,6461,6404,6306,6346,6348,6233,6398,6227,22,21,24,26,25,29])).
% 116.73/116.81 cnf(6707,plain,
% 116.73/116.81 (P2(f6(a1),f7(a4,a4),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6649,6694,22,21])).
% 116.73/116.81 cnf(6711,plain,
% 116.73/116.81 (~P4(f7(a4,a4),f7(a4,a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[6649,6694,6504,6472,6306,6280,6368,22,21,24,26])).
% 116.73/116.81 cnf(6713,plain,
% 116.73/116.81 (P2(f7(a2,a2),f6(a1),f7(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6649,6696,6694,6504,6472,6306,6280,6368,6398,22,21,24,26,25])).
% 116.73/116.81 cnf(6715,plain,
% 116.73/116.81 (~P2(a1,f7(a1,a1),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6649,6696,6694,6679,6504,6472,6272,6306,6280,6368,6398,6274,6553,22,21,24,26,25,29])).
% 116.73/116.81 cnf(6719,plain,
% 116.73/116.81 (~P4(a1,f6(a5),a4)),
% 116.73/116.81 inference(scs_inference,[],[6698,6649,6696,6666,6694,6538,6430,6679,6504,6472,6272,6306,6280,6368,6398,6274,6553,22,21,24,26,25,29,27,28])).
% 116.73/116.81 cnf(6725,plain,
% 116.73/116.81 (~P2(f6(a1),f7(a4,a4),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6707,6713,6719,6715,6366,22,21,24])).
% 116.73/116.81 cnf(6727,plain,
% 116.73/116.81 (~P4(a4,f8(a4),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6707,6713,6719,6715,6655,6366,6415,6227,22,21,24,26])).
% 116.73/116.81 cnf(6729,plain,
% 116.73/116.81 (P2(f3(a1,a1),f6(a5),f6(a5))),
% 116.73/116.81 inference(scs_inference,[],[6707,6713,6719,6715,6655,6428,6366,6415,6227,6282,22,21,24,26,25])).
% 116.73/116.81 cnf(6736,plain,
% 116.73/116.81 (~P4(f8(a4),a4,f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6727,22])).
% 116.73/116.81 cnf(6738,plain,
% 116.73/116.81 (P2(f6(a5),f3(a1,a1),f6(a5))),
% 116.73/116.81 inference(scs_inference,[],[6727,6729,22,21])).
% 116.73/116.81 cnf(6740,plain,
% 116.73/116.81 (~P2(f3(a1,a1),f7(a1,a1),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6727,6729,6565,6337,6577,22,21,24])).
% 116.73/116.81 cnf(6742,plain,
% 116.73/116.81 (~P4(a1,a1,f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6727,6729,6565,6337,6577,6274,6553,22,21,24,26])).
% 116.73/116.81 cnf(6746,plain,
% 116.73/116.81 (P2(f7(a5,a5),f6(a1),f7(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[6727,6729,6690,6449,6565,6337,6577,6508,6239,6274,6553,22,21,24,26,27,25])).
% 116.73/116.81 cnf(6748,plain,
% 116.73/116.81 (~P4(f3(a1,a1),a1,a4)),
% 116.73/116.81 inference(scs_inference,[],[6727,6729,6690,6449,6565,6337,6292,6577,6508,6382,6231,6239,6274,6553,22,21,24,26,27,25,29])).
% 116.73/116.81 cnf(6750,plain,
% 116.73/116.81 (~P4(a1,f6(a1),a2)),
% 116.73/116.81 inference(scs_inference,[],[6402,6727,6729,6690,6449,6565,6518,6337,6292,6577,6508,6382,6231,6239,6274,6553,22,21,24,26,27,25,29,28])).
% 116.73/116.81 cnf(6757,plain,
% 116.73/116.81 (~P2(f3(a1,a1),f3(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[6746,6738,6748,6666,22,21,24])).
% 116.73/116.81 cnf(6759,plain,
% 116.73/116.81 (~P4(f7(a4,a4),f6(a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[6746,6738,6748,6666,6484,6239,106,22,21,24,26])).
% 116.73/116.81 cnf(6761,plain,
% 116.73/116.81 (P2(a1,f3(a1,a1),a1)),
% 116.73/116.81 inference(scs_inference,[],[6746,6738,6748,6666,6484,6417,6239,106,22,21,24,26,25])).
% 116.73/116.81 cnf(6763,plain,
% 116.73/116.81 (~P2(f7(a1,a1),f7(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[6746,6738,6748,6666,6484,6417,6239,6274,6282,106,22,21,24,26,25,29])).
% 116.73/116.81 cnf(6765,plain,
% 116.73/116.81 (~P4(f3(a4,a4),f3(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[6746,6738,6748,6666,6364,6484,6417,6241,6239,6274,6282,106,22,21,24,26,25,29,28])).
% 116.73/116.81 cnf(6775,plain,
% 116.73/116.81 (~P2(f7(a4,a4),f7(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6765,6645,6546,6715,6270,22,21,24])).
% 116.73/116.81 cnf(6777,plain,
% 116.73/116.81 (~P4(a4,f7(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[6765,6736,6645,6546,6715,6323,6270,6294,22,21,24,26])).
% 116.73/116.81 cnf(6779,plain,
% 116.73/116.81 (P2(a5,f3(a1,a1),a5)),
% 116.73/116.81 inference(scs_inference,[],[6761,6765,6736,6645,6546,6715,6323,6270,6327,6294,22,21,24,26,25])).
% 116.73/116.81 cnf(6781,plain,
% 116.73/116.81 (~P4(f3(a1,a1),f6(a5),a4)),
% 116.73/116.81 inference(scs_inference,[],[6761,6765,6736,6645,6546,6715,6430,6323,6666,6270,6327,6382,6294,22,21,24,26,25,28])).
% 116.73/116.81 cnf(6787,plain,
% 116.73/116.81 (~P4(f6(a4),f7(a4,a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[6759,22])).
% 116.73/116.81 cnf(6789,plain,
% 116.73/116.81 (P2(f3(a1,a1),a5,a5)),
% 116.73/116.81 inference(scs_inference,[],[6759,6779,22,21])).
% 116.73/116.81 cnf(6791,plain,
% 116.73/116.81 (~P2(f7(a4,a4),f3(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6775,6759,6779,6595,6645,22,21,24])).
% 116.73/116.81 cnf(6793,plain,
% 116.73/116.81 (~P4(a4,a4,f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6775,6759,6777,6779,6595,6645,6227,22,21,24,26])).
% 116.73/116.81 cnf(6795,plain,
% 116.73/116.81 (P2(a5,f6(a1),a5)),
% 116.73/116.81 inference(scs_inference,[],[6775,6759,6777,6779,6595,6645,6508,6227,22,21,24,26,25])).
% 116.73/116.81 cnf(6797,plain,
% 116.73/116.81 (~P2(f6(a4),f8(a4),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6775,6759,6777,6779,6595,6459,6645,6508,6354,6415,6227,6229,22,21,24,26,25,29])).
% 116.73/116.81 cnf(6802,plain,
% 116.73/116.81 (~P4(f6(a1),a1,a2)),
% 116.73/116.81 inference(scs_inference,[],[6750,22])).
% 116.73/116.81 cnf(6804,plain,
% 116.73/116.81 (P2(f6(a1),a5,a5)),
% 116.73/116.81 inference(scs_inference,[],[6750,6795,22,21])).
% 116.73/116.81 cnf(6806,plain,
% 116.73/116.81 (~P2(a5,f6(a1),a2)),
% 116.73/116.81 inference(scs_inference,[],[6750,6789,6795,30,22,21,24])).
% 116.73/116.81 cnf(6807,plain,
% 116.73/116.81 (~P2(x68071,a2,a5)),
% 116.73/116.81 inference(rename_variables,[],[30])).
% 116.73/116.81 cnf(6809,plain,
% 116.73/116.81 (~P4(f3(a4,a4),f7(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[6750,6789,6793,6795,6268,6530,30,22,21,24,26])).
% 116.73/116.81 cnf(6811,plain,
% 116.73/116.81 (~P2(f6(a1),a2,f6(a1))),
% 116.73/116.81 inference(scs_inference,[],[6750,6789,6793,6795,6268,6530,30,6807,22,21,24,26,25])).
% 116.73/116.81 cnf(6814,plain,
% 116.73/116.81 (~P2(a1,f7(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6750,6789,6793,6795,6268,6579,6530,6272,30,6807,6274,6553,22,21,24,26,25,29])).
% 116.73/116.81 cnf(6823,plain,
% 116.73/116.81 (P2(a5,f6(a5),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6809,6486,22,21])).
% 116.73/116.81 cnf(6827,plain,
% 116.73/116.81 (P2(f3(a1,a1),a2,a2)),
% 116.73/116.81 inference(scs_inference,[],[6809,6486,6729,6243,6666,6282,22,21,24,25])).
% 116.73/116.81 cnf(6835,plain,
% 116.73/116.81 (~P4(f6(a5),f3(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[6781,22])).
% 116.73/116.81 cnf(6837,plain,
% 116.73/116.81 (P2(a2,f3(a1,a1),a2)),
% 116.73/116.81 inference(scs_inference,[],[6827,6781,22,21])).
% 116.73/116.81 cnf(6843,plain,
% 116.73/116.81 (P2(a2,f6(a2),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6823,6827,6806,6781,6793,6346,6432,6274,6553,22,21,24,26,25])).
% 116.73/116.81 cnf(6845,plain,
% 116.73/116.81 (~P4(a1,f7(a1,a1),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6823,6827,6806,6781,6775,6793,6323,6346,6432,6231,6274,6553,22,21,24,26,25,28])).
% 116.73/116.81 cnf(6849,plain,
% 116.73/116.81 (~P4(f3(a1,a1),a1,f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6823,6827,6806,6781,6775,6793,6474,6323,6559,6346,6432,6382,6231,6274,6553,79,22,21,24,26,25,28,27,29])).
% 116.73/116.81 cnf(6856,plain,
% 116.73/116.81 (P2(f6(a2),a2,f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6845,6843,22,21])).
% 116.73/116.81 cnf(6858,plain,
% 116.73/116.81 (P2(f6(a1),f3(a1,a1),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6845,6843,6823,6804,22,21,24])).
% 116.73/116.81 cnf(6860,plain,
% 116.73/116.81 (~P4(f7(a4,a4),f7(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[6845,6843,6823,6804,6777,6559,6306,22,21,24,26])).
% 116.73/116.81 cnf(6862,plain,
% 116.73/116.81 (~P2(f6(a2),a4,f6(a2))),
% 116.73/116.81 inference(scs_inference,[],[6845,6843,6823,6804,6777,6559,6306,6280,6432,22,21,24,26,25])).
% 116.73/116.81 cnf(6864,plain,
% 116.73/116.81 (~P2(a1,f7(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[6845,6843,6823,6804,6777,6292,6559,6306,6280,6432,6272,6274,6553,22,21,24,26,25,29])).
% 116.73/116.81 cnf(6872,plain,
% 116.73/116.81 (P2(f6(a2),f3(a1,a1),f6(a2))),
% 116.73/116.81 inference(scs_inference,[],[6860,6528,22,21])).
% 116.73/116.81 cnf(6874,plain,
% 116.73/116.81 (~P2(f6(a2),a5,x68741)),
% 116.73/116.81 inference(scs_inference,[],[6,6860,6789,6843,6528,22,21,24])).
% 116.73/116.81 cnf(6878,plain,
% 116.73/116.81 (~P4(f3(a1,a1),f6(a2),a4)),
% 116.73/116.81 inference(scs_inference,[],[6,6860,6862,6542,6789,6843,6696,6528,6321,6382,22,21,24,25,28])).
% 116.73/116.81 cnf(6886,plain,
% 116.73/116.81 (P2(a1,f7(a1,a1),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6849,6599,22,21])).
% 116.73/116.81 cnf(6888,plain,
% 116.73/116.81 (~P2(f3(a1,a1),f7(a1,a1),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6725,6849,6858,6599,6577,22,21,24])).
% 116.73/116.81 cnf(6892,plain,
% 116.73/116.81 (P4(f7(a4,a4),f7(a2,a2),f7(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6725,6849,6858,6476,6396,6599,6577,6239,6294,22,21,24,26,27])).
% 116.73/116.81 cnf(6894,plain,
% 116.73/116.81 (P2(f6(a2),a1,f6(a2))),
% 116.73/116.81 inference(scs_inference,[],[6725,6872,6849,6858,6476,6396,6599,6577,6346,6239,6294,22,21,24,26,27,25])).
% 116.73/116.81 cnf(6903,plain,
% 116.73/116.81 (P2(a1,f7(a1,a1),a1)),
% 116.73/116.81 inference(scs_inference,[],[6878,6563,22,21])).
% 116.73/116.81 cnf(6905,plain,
% 116.73/116.81 (~P2(a1,a1,a5)),
% 116.73/116.81 inference(scs_inference,[],[6874,6878,6894,6563,22,21,24])).
% 116.73/116.81 cnf(6908,plain,
% 116.73/116.81 (P2(f6(a4),f3(a1,a1),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6874,6878,6894,6563,6761,6233,22,21,24,25])).
% 116.73/116.81 cnf(6916,plain,
% 116.73/116.81 (P2(f3(a1,a1),f6(a4),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6908,6634,22,21])).
% 116.73/116.81 cnf(6918,plain,
% 116.73/116.81 (~P2(f6(a4),f3(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6740,6908,6634,22,21,24])).
% 116.73/116.81 cnf(6920,plain,
% 116.73/116.81 (P2(f6(a4),f7(a1,a1),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6740,6908,6886,6634,6233,22,21,24,25])).
% 116.73/116.81 cnf(6927,plain,
% 116.73/116.81 (~P4(a1,f3(a4,a4),a4)),
% 116.73/116.81 inference(scs_inference,[],[6583,22])).
% 116.73/116.81 cnf(6929,plain,
% 116.73/116.81 (P2(f7(a1,a1),f6(a4),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6920,6583,22,21])).
% 116.73/116.81 cnf(6933,plain,
% 116.73/116.81 (P2(f6(a2),f7(a1,a1),f6(a2))),
% 116.73/116.81 inference(scs_inference,[],[6905,6920,6903,6583,6894,6284,22,21,24,25])).
% 116.73/116.81 cnf(6935,plain,
% 116.73/116.81 (~P4(f7(a1,a1),f8(a4),a4)),
% 116.73/116.81 inference(scs_inference,[],[6905,6920,6903,6583,6496,6894,6284,6354,6229,22,21,24,25,29])).
% 116.73/116.81 cnf(6939,plain,
% 116.73/116.81 (~P4(f3(a1,a1),f8(a4),a4)),
% 116.73/116.81 inference(scs_inference,[],[6905,6835,6916,6920,6903,6583,6496,6310,6894,6284,6354,6229,6227,22,21,24,25,29,26,28])).
% 116.73/116.81 cnf(6945,plain,
% 116.73/116.81 (P2(f7(a1,a1),f6(a2),f6(a2))),
% 116.73/116.81 inference(scs_inference,[],[6933,6935,22,21])).
% 116.73/116.81 cnf(6947,plain,
% 116.73/116.81 (~P2(f7(a1,a1),f7(a1,a1),a5)),
% 116.73/116.81 inference(scs_inference,[],[6933,6935,6874,22,21,24])).
% 116.73/116.81 cnf(6954,plain,
% 116.73/116.81 (P2(f3(a1,a1),f7(a1,a1),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6933,6935,6874,6498,6542,6843,6239,6294,22,21,24,26,27,25])).
% 116.73/116.81 cnf(6956,plain,
% 116.73/116.81 (~P4(f7(a1,a1),a1,f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6929,6933,6935,6849,6874,6886,6498,6542,6843,6239,6294,6274,22,21,24,26,27,25,29])).
% 116.73/116.81 cnf(6960,plain,
% 116.73/116.81 (~P4(f8(a4),f3(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[6939,22])).
% 116.73/116.81 cnf(6962,plain,
% 116.73/116.81 (P2(f7(a1,a1),f3(a1,a1),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6954,6939,22,21])).
% 116.73/116.81 cnf(6964,plain,
% 116.73/116.81 (~P2(f7(a1,a1),f7(a4,a4),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6954,6888,6939,6478,22,21,24])).
% 116.73/116.81 cnf(6968,plain,
% 116.73/116.81 (P2(a2,f7(a1,a1),a2)),
% 116.73/116.81 inference(scs_inference,[],[6954,6888,6939,6956,6837,6478,6274,22,21,24,27,25])).
% 116.73/116.81 cnf(6970,plain,
% 116.73/116.81 (~P2(f8(a4),f6(a4),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6954,6888,6939,6956,6837,6478,6310,6294,6274,4067,22,21,24,27,25,28])).
% 116.73/116.81 cnf(6978,plain,
% 116.73/116.81 (P2(f7(a1,a1),a2,a2)),
% 116.73/116.81 inference(scs_inference,[],[6968,6603,22,21])).
% 116.73/116.81 cnf(6982,plain,
% 116.73/116.81 (P2(a2,a1,a2)),
% 116.73/116.81 inference(scs_inference,[],[6962,6763,6968,6603,6837,6599,6577,22,21,24,25])).
% 116.73/116.81 cnf(6989,plain,
% 116.73/116.81 (~P4(f7(a1,a1),a4,a4)),
% 116.73/116.81 inference(scs_inference,[],[6777,22])).
% 116.73/116.81 cnf(6991,plain,
% 116.73/116.81 (P2(f6(a1),a1,f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6777,6632,22,21])).
% 116.73/116.81 cnf(6993,plain,
% 116.73/116.81 (~P4(a1,f7(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[6845,6777,6632,6239,6553,22,21,27])).
% 116.73/116.81 cnf(6995,plain,
% 116.73/116.81 (P2(f7(a1,a1),f3(a2,a2),f3(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6520,6962,6845,6777,6632,6239,6553,22,21,27,24])).
% 116.73/116.81 cnf(6999,plain,
% 116.73/116.81 (P2(f7(a2,a2),f7(a1,a1),f7(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6520,6962,6845,6449,6777,6696,6903,6632,6239,6294,6553,22,21,27,24,26,25])).
% 116.73/116.81 cnf(7008,plain,
% 116.73/116.81 (P2(f3(a2,a2),f7(a1,a1),f3(a2,a2))),
% 116.73/116.81 inference(scs_inference,[],[6995,6993,22,21])).
% 116.73/116.81 cnf(7010,plain,
% 116.73/116.81 (~P4(a1,f3(a4,a4),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6995,6927,6993,6312,6294,22,21,26])).
% 116.73/116.81 cnf(7012,plain,
% 116.73/116.81 (~P2(f8(a4),f7(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6995,6927,6970,6993,6929,6312,6294,22,21,26,24])).
% 116.73/116.81 cnf(7014,plain,
% 116.73/116.81 (~P2(f6(a1),f6(a5),f6(a2))),
% 116.73/116.81 inference(scs_inference,[],[6995,6927,6970,6991,6993,6929,6312,6874,6321,6294,22,21,26,24,25])).
% 116.73/116.81 cnf(7017,plain,
% 116.73/116.81 (~P4(f3(a4,a4),f7(a1,a1),a5)),
% 116.73/116.81 inference(scs_inference,[],[6995,6927,6947,6970,6991,6993,6929,6312,6874,6321,6323,6241,6294,22,21,26,24,25,28])).
% 116.73/116.81 cnf(7019,plain,
% 116.73/116.81 (~P2(f7(a1,a1),f7(a1,a1),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6995,6927,6947,6970,6991,6993,6929,6312,6849,6874,6321,6323,6241,6282,6294,6274,22,21,26,24,25,28,29])).
% 116.73/116.81 cnf(7032,plain,
% 116.73/116.81 (~P2(f7(a4,a4),a1,f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6999,6791,7017,6989,6991,6649,6294,22,21,27,24])).
% 116.73/116.81 cnf(7034,plain,
% 116.73/116.81 (P2(f6(a2),a2,f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[6999,6791,7017,6989,6856,6945,6991,6649,6595,6294,22,21,27,24,25])).
% 116.73/116.81 cnf(7036,plain,
% 116.73/116.81 (~P4(f3(a4,a4),f7(a1,a1),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6999,6791,7019,7017,6989,6856,6945,6991,6649,6595,6559,6348,6294,22,21,27,24,25,28])).
% 116.73/116.81 cnf(7043,plain,
% 116.73/116.81 (P2(a2,f6(a2),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7036,7034,22,21])).
% 116.73/116.81 cnf(7045,plain,
% 116.73/116.81 (~P2(f6(a4),f7(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7036,7034,6740,6916,6920,22,21,24])).
% 116.73/116.81 cnf(7047,plain,
% 116.73/116.81 (P2(f7(a1,a1),a1,f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7036,7034,6740,6916,6982,6920,22,21,24,25])).
% 116.73/116.81 cnf(7049,plain,
% 116.73/116.81 (~P4(f3(a1,a1),f6(a1),a2)),
% 116.73/116.81 inference(scs_inference,[],[6811,7036,7034,6740,6916,6982,6920,6518,6382,22,21,24,25,28])).
% 116.73/116.81 cnf(7058,plain,
% 116.73/116.81 (P1(f8(a2))),
% 116.73/116.81 inference(scs_inference,[],[6339,6514,21])).
% 116.73/116.81 cnf(7059,plain,
% 116.73/116.81 (P2(a1,f8(a2),f8(a2))),
% 116.73/116.81 inference(scs_inference,[],[7058,12])).
% 116.73/116.81 cnf(7061,plain,
% 116.73/116.81 (P4(a4,f8(a2),f8(a2))),
% 116.73/116.81 inference(scs_inference,[],[7058,12,13])).
% 116.73/116.81 cnf(7065,plain,
% 116.73/116.81 (P2(f7(a5,a5),a1,f7(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[7010,7058,6447,12,13,22,21])).
% 116.73/116.81 cnf(7067,plain,
% 116.73/116.81 (~P2(a1,a1,f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6964,7010,7047,7058,6447,12,13,22,21,24])).
% 116.73/116.81 cnf(7069,plain,
% 116.73/116.81 (~P2(a5,f6(a2),a2)),
% 116.73/116.81 inference(scs_inference,[],[6,6964,7010,7047,7058,6856,6447,6779,12,13,22,21,24,25])).
% 116.73/116.81 cnf(7072,plain,
% 116.73/116.81 (~P2(a1,a1,f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6,6964,7010,7047,7058,6856,6447,6779,6241,6553,12,13,22,21,24,25,29])).
% 116.73/116.81 cnf(7081,plain,
% 116.73/116.81 (P2(f8(a2),a1,f8(a2))),
% 116.73/116.81 inference(scs_inference,[],[7059,7049,22,21])).
% 116.73/116.81 cnf(7083,plain,
% 116.73/116.81 (~P2(f8(a4),a2,a2)),
% 116.73/116.81 inference(scs_inference,[],[7012,7043,7059,7049,22,21,24])).
% 116.73/116.81 cnf(7085,plain,
% 116.73/116.81 (P2(f7(a5,a5),f7(a1,a1),f7(a5,a5))),
% 116.73/116.81 inference(scs_inference,[],[7012,7043,7059,7065,7049,6690,6886,22,21,24,25])).
% 116.73/116.81 cnf(7095,plain,
% 116.73/116.81 (P2(f8(a2),f3(a1,a1),f8(a2))),
% 116.73/116.81 inference(scs_inference,[],[7085,7081,6655,6282,22,21,24])).
% 116.73/116.81 cnf(7097,plain,
% 116.73/116.81 (P2(f8(a2),f7(a1,a1),f8(a2))),
% 116.73/116.81 inference(scs_inference,[],[7085,7081,6655,6903,6282,22,21,24,25])).
% 116.73/116.81 cnf(7103,plain,
% 116.73/116.81 (~P4(a1,a4,f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[6679,22])).
% 116.73/116.81 cnf(7111,plain,
% 116.73/116.81 (~P2(f7(a1,a1),f6(a1),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[6918,7095,7067,7061,6858,6478,6595,6337,6679,6294,22,21,26,24,25])).
% 116.73/116.81 cnf(7122,plain,
% 116.73/116.81 (P2(f8(a2),f6(a1),f8(a2))),
% 116.73/116.81 inference(scs_inference,[],[7097,7069,7095,6827,6823,6508,21,24,25])).
% 116.73/116.81 cnf(7126,plain,
% 116.73/116.81 (~P2(f7(a1,a1),a1,f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[7097,7103,7069,7095,6474,6827,6823,6504,6508,6231,6553,6274,21,24,25,26,29])).
% 116.73/116.81 cnf(7133,plain,
% 116.73/116.81 (~P2(a2,f6(a2),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[7122,6978,6964,7043,21,24])).
% 116.73/116.81 cnf(7135,plain,
% 116.73/116.81 (~P2(f6(a1),a4,f6(a1))),
% 116.73/116.81 inference(scs_inference,[],[7122,6978,6964,7043,6280,6398,21,24,25])).
% 116.73/116.81 cnf(7144,plain,
% 116.73/116.81 (P2(f6(a5),a1,f6(a5))),
% 116.73/116.81 inference(scs_inference,[],[6428,21])).
% 116.73/116.81 cnf(7146,plain,
% 116.73/116.81 (~P2(f3(a1,a1),f6(a4),f6(a1))),
% 116.73/116.81 inference(scs_inference,[],[7111,6962,6916,6428,21,24])).
% 116.73/116.81 cnf(7148,plain,
% 116.73/116.81 (P2(f3(a1,a1),f8(a4),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[7111,6962,6916,6428,6413,6282,21,24,25])).
% 116.73/116.81 cnf(7155,plain,
% 116.73/116.81 (P2(f8(a4),f3(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[7148,21])).
% 116.73/116.81 cnf(7159,plain,
% 116.73/116.81 (P2(f6(a5),f7(a1,a1),f6(a5))),
% 116.73/116.81 inference(scs_inference,[],[7148,7144,6862,7034,6945,6738,6886,21,24,25])).
% 116.73/116.81 cnf(7166,plain,
% 116.73/116.81 (P2(f7(a1,a1),f6(a5),f6(a5))),
% 116.73/116.81 inference(scs_inference,[],[7159,21])).
% 116.73/116.81 cnf(7168,plain,
% 116.73/116.81 (~P4(a4,a4,f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7159,6960,6227,6294,21,26])).
% 116.73/116.81 cnf(7170,plain,
% 116.73/116.81 (~P2(f7(a1,a1),f7(a1,a1),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[7159,6960,6488,6964,6227,6294,21,26,24])).
% 116.73/116.81 cnf(7177,plain,
% 116.73/116.81 (P2(f8(a4),a1,f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[6413,21])).
% 116.73/116.81 cnf(7179,plain,
% 116.73/116.81 (~P4(a4,f3(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[7168,6364,6413,6227,21,26])).
% 116.73/116.81 cnf(7183,plain,
% 116.73/116.81 (~P2(f8(a4),f3(a1,a1),a1)),
% 116.73/116.81 inference(scs_inference,[],[7072,7155,7168,7061,6364,6413,6239,6227,21,26,27,24])).
% 116.73/116.81 cnf(7185,plain,
% 116.73/116.81 (~P4(f3(a1,a1),a1,f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[7170,7072,7155,7168,7061,6364,6413,6239,6227,6282,6274,21,26,27,24,28])).
% 116.73/116.81 cnf(7187,plain,
% 116.73/116.81 (~P4(f3(a1,a1),a4,a4)),
% 116.73/116.81 inference(scs_inference,[],[7170,7072,7155,7168,7061,6364,6413,6239,6227,6282,6274,21,26,27,24,28,22])).
% 116.73/116.81 cnf(7192,plain,
% 116.73/116.81 (~P4(a1,f3(a1,a1),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[7185,22])).
% 116.73/116.81 cnf(7194,plain,
% 116.73/116.81 (P2(f3(a1,a1),a4,a4)),
% 116.73/116.81 inference(scs_inference,[],[7185,6382,22,21])).
% 116.73/116.81 cnf(7196,plain,
% 116.73/116.81 (~P4(f7(a4,a4),f3(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[7185,7179,6404,6306,6382,22,21,26])).
% 116.73/116.81 cnf(7198,plain,
% 116.73/116.81 (~P4(f8(a4),f8(a4),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7185,7179,7187,6404,6306,6382,6294,22,21,26,27])).
% 116.73/116.81 cnf(7202,plain,
% 116.73/116.81 (~P4(f3(a4,a4),f7(a1,a1),f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[7166,6622,7185,7179,7187,7170,6404,6321,6306,6559,6348,6382,6294,22,21,26,27,24,28])).
% 116.73/116.81 cnf(7210,plain,
% 116.73/116.81 (P2(f6(a1),a1,f6(a1))),
% 116.73/116.81 inference(scs_inference,[],[7202,6366,22,21])).
% 116.73/116.81 cnf(7212,plain,
% 116.73/116.81 (~P4(a4,f3(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[7198,7202,6364,6366,6294,22,21,26])).
% 116.73/116.81 cnf(7216,plain,
% 116.73/116.81 (~P2(f8(a4),f7(a1,a1),a1)),
% 116.73/116.81 inference(scs_inference,[],[7198,7202,6757,7177,7194,7072,6563,6364,6272,6366,6294,22,21,26,24,25])).
% 116.73/116.81 cnf(7218,plain,
% 116.73/116.81 (~P4(a1,f6(a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[7198,7202,6757,7135,7177,7194,7072,6563,6364,6518,6272,6366,6294,22,21,26,24,25,28])).
% 116.73/116.81 cnf(7222,plain,
% 116.73/116.81 (~P4(f7(a1,a1),f3(a1,a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[7198,7202,6757,7135,7177,7192,7194,7072,6628,6765,6563,6364,6249,6698,6518,6272,6366,6294,22,21,26,24,25,28,27,29])).
% 116.73/116.81 cnf(7226,plain,
% 116.73/116.81 (P2(a4,f6(a4),a1)),
% 116.73/116.81 inference(scs_inference,[],[7222,6229,22,21])).
% 116.73/116.81 cnf(7228,plain,
% 116.73/116.81 (P4(f7(a4,a4),f6(a5),f6(a5))),
% 116.73/116.81 inference(scs_inference,[],[7222,6430,6229,6239,22,21,27])).
% 116.73/116.81 cnf(7230,plain,
% 116.73/116.81 (~P4(a4,f8(a4),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7222,7212,6430,6415,6229,6239,6227,22,21,27,26])).
% 116.73/116.81 cnf(7232,plain,
% 116.73/116.81 (~P2(f6(a4),f3(a1,a1),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7222,6797,7212,7148,6430,6415,6229,6239,6227,22,21,27,26,24])).
% 116.73/116.81 cnf(7234,plain,
% 116.73/116.81 (P2(f8(a4),f7(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[7222,6797,7212,7155,7148,6954,6430,6415,6229,6239,6227,22,21,27,26,24,25])).
% 116.73/116.81 cnf(7236,plain,
% 116.73/116.81 (~P4(f6(a1),a1,f7(a4,a4))),
% 116.73/116.81 inference(scs_inference,[],[7222,6797,7212,7155,7148,7185,6991,6645,6954,6430,6415,6229,6239,6227,6274,22,21,27,26,24,25,29])).
% 116.73/116.81 cnf(7242,plain,
% 116.73/116.81 (P2(f7(a1,a1),f8(a4),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[7196,7234,22,21])).
% 116.73/116.81 cnf(7244,plain,
% 116.73/116.81 (~P4(f3(a4,a4),f3(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[7196,7234,7230,6268,6698,22,21,26])).
% 116.73/116.81 cnf(7248,plain,
% 116.73/116.81 (P2(f6(a1),f3(a1,a1),f6(a1))),
% 116.73/116.81 inference(scs_inference,[],[7196,7234,7216,7230,7210,7047,6268,6761,6698,22,21,26,24,25])).
% 116.73/116.81 cnf(7250,plain,
% 116.73/116.81 (~P4(a1,f8(a4),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[7196,7234,7216,7230,7226,6970,7210,7047,6268,6761,6698,6354,6415,22,21,26,24,25,28])).
% 116.73/116.81 cnf(7258,plain,
% 116.73/116.81 (P2(f3(a1,a1),f6(a1),f6(a1))),
% 116.73/116.81 inference(scs_inference,[],[7244,7248,22,21])).
% 116.73/116.81 cnf(7260,plain,
% 116.73/116.81 (~P4(f7(a4,a4),f3(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[7244,7248,7230,6404,6306,22,21,26])).
% 116.73/116.81 cnf(7262,plain,
% 116.73/116.81 (~P2(f8(a4),a1,f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7244,7242,7248,6637,7177,7230,6404,6306,22,21,26,24])).
% 116.73/116.81 cnf(7264,plain,
% 116.73/116.81 (~P2(f6(a1),f6(a1),f6(a4))),
% 116.73/116.81 inference(scs_inference,[],[7232,7244,7242,7248,6637,7177,7230,6858,6404,6306,22,21,26,24,25])).
% 116.73/116.81 cnf(7266,plain,
% 116.73/116.81 (~P4(f3(a4,a4),a1,a5)),
% 116.73/116.81 inference(scs_inference,[],[7232,7244,7242,7248,6905,6637,7177,7230,6858,6404,6306,6241,6553,22,21,26,24,25,28])).
% 116.73/116.81 cnf(7268,plain,
% 116.73/116.81 (~P2(f3(a1,a1),f3(a1,a1),f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[7232,7244,7242,7248,6905,6637,7177,7230,6858,6404,6306,6348,6241,6553,22,21,26,24,25,28,29])).
% 116.73/116.81 cnf(7274,plain,
% 116.73/116.81 (P4(f7(a4,a4),a5,a5)),
% 116.73/116.81 inference(scs_inference,[],[7260,6575,6239,22,27])).
% 116.73/116.81 cnf(7278,plain,
% 116.73/116.81 (~P2(f7(a1,a1),f8(a4),f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7268,7260,7242,7179,6575,6577,6415,6239,6294,22,27,26,24])).
% 116.73/116.81 cnf(7280,plain,
% 116.73/116.81 (P2(f6(a5),f6(a1),f6(a5))),
% 116.73/116.81 inference(scs_inference,[],[7268,7260,7242,7144,7179,6738,6632,6575,6577,6415,6239,6294,22,27,26,24,25])).
% 116.73/116.81 cnf(7284,plain,
% 116.73/116.81 (P2(f6(a1),f6(a5),f6(a5))),
% 116.73/116.81 inference(scs_inference,[],[7268,7260,7242,7144,7179,6561,7244,7148,6738,6632,6575,6577,6698,6415,6239,6294,22,27,26,24,25,29,21])).
% 116.73/116.81 cnf(7291,plain,
% 116.73/116.81 (~P2(f6(a5),f6(a1),f6(a2))),
% 116.73/116.81 inference(scs_inference,[],[7014,7218,7280,7284,22,24])).
% 116.73/116.81 cnf(7293,plain,
% 116.73/116.81 (P2(f6(a1),f7(a1,a1),f6(a1))),
% 116.73/116.81 inference(scs_inference,[],[7014,7218,7280,7284,7210,6903,22,24,25])).
% 116.73/116.81 cnf(7295,plain,
% 116.73/116.81 (~P4(f6(a1),a1,f8(a4))),
% 116.73/116.81 inference(scs_inference,[],[7014,7218,7280,7284,6742,7234,7210,6266,6903,6274,22,24,25,29])).
% 116.73/116.81 cnf(7297,plain,
% 116.73/116.81 (P2(f7(a1,a1),f6(a1),f6(a1))),
% 116.73/116.81 inference(scs_inference,[],[7014,7218,7280,7284,6742,7234,7210,6266,6903,6274,22,24,25,29,21])).
% 116.73/116.81 cnf(7303,plain,
% 116.73/116.81 (~P4(a1,f3(a4,a4),a5)),
% 116.73/116.81 inference(scs_inference,[],[7266,22])).
% 116.73/116.81 cnf(7305,plain,
% 116.73/116.81 (~P2(f7(a1,a1),f7(a1,a1),a2)),
% 116.73/116.81 inference(scs_inference,[],[7266,7293,6811,22,24])).
% 116.73/116.81 cnf(7307,plain,
% 116.73/116.81 (~P2(f6(a1),a4,f3(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7266,7146,7293,6811,7226,7210,22,24,25])).
% 116.73/116.81 cnf(7317,plain,
% 116.73/116.81 (P2(f6(a1),f6(a1),f6(a1))),
% 116.73/116.81 inference(scs_inference,[],[6864,7295,7248,7194,6337,6508,22,24,25])).
% 116.73/116.81 cnf(7326,plain,
% 116.73/116.81 (~P2(f8(a4),f3(a1,a1),f7(a1,a1))),
% 116.73/116.81 inference(scs_inference,[],[7262,7250,7177,6761,22,24])).
% 116.73/116.81 cnf(7337,plain,
% 116.73/116.81 (~P2(f6(a1),f6(a1),a4)),
% 116.73/116.81 inference(scs_inference,[],[7317,7135,7212,22,24])).
% 116.73/116.81 cnf(7339,plain,
% 116.73/116.81 (P2(a5,f7(a1,a1),a5)),
% 116.73/116.81 inference(scs_inference,[],[7317,7135,7212,6903,6327,22,24,25])).
% 116.73/116.81 cnf(7341,plain,
% 116.73/116.82 (P2(f7(a1,a1),a5,a5)),
% 116.73/116.82 inference(scs_inference,[],[7317,7135,7212,6903,6327,22,24,25,21])).
% 116.73/116.82 cnf(7350,plain,
% 116.73/116.82 (~P2(f7(a1,a1),f8(a4),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[6814,7236,7242,6325,22,24])).
% 116.73/116.82 cnf(7352,plain,
% 116.73/116.82 (P2(f7(a1,a1),f6(a1),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[6814,7297,7236,7242,6325,6632,22,24,25])).
% 116.73/116.82 cnf(7354,plain,
% 116.73/116.82 (~P4(f6(a1),a5,a2)),
% 116.73/116.82 inference(scs_inference,[],[6,6814,7297,7236,7242,6707,6325,7274,6632,22,24,25,28])).
% 116.73/116.82 cnf(7357,plain,
% 116.73/116.82 (P2(f6(a1),f7(a1,a1),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[6,6814,7297,7236,7242,6707,6325,7274,6632,22,24,25,28,21])).
% 116.73/116.82 cnf(7361,plain,
% 116.73/116.82 (~P4(f6(a1),f7(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[6,6814,7297,7236,7202,6421,7242,6707,6630,6892,6325,7274,6372,6632,6530,22,24,25,28,21,27,29])).
% 116.73/116.82 cnf(7367,plain,
% 116.73/116.82 (~P4(f6(a1),f7(a1,a1),a4)),
% 116.73/116.82 inference(scs_inference,[],[7354,7361,6518,6239,22,27])).
% 116.73/116.82 cnf(7369,plain,
% 116.73/116.82 (~P2(f7(a1,a1),f6(a4),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7264,7354,7357,7361,6916,6518,6239,22,27,24])).
% 116.73/116.82 cnf(7371,plain,
% 116.73/116.82 (~P2(f6(a1),f6(a4),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7264,7354,7357,7361,7146,6929,6916,6518,6239,22,27,24,25])).
% 116.73/116.82 cnf(7373,plain,
% 116.73/116.82 (~P4(f6(a1),f3(a1,a1),a4)),
% 116.73/116.82 inference(scs_inference,[],[7264,7354,7357,7361,7196,7146,7194,6929,6916,6649,6518,6404,6239,22,27,24,25,29])).
% 116.73/116.82 cnf(7381,plain,
% 116.73/116.82 (~P2(a5,f7(a1,a1),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7367,7341,7339,6947,22,24])).
% 116.73/116.82 cnf(7389,plain,
% 116.73/116.82 (~P2(f7(a1,a1),f6(a1),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7278,7373,7352,6488,22,24])).
% 116.73/116.82 cnf(7398,plain,
% 116.73/116.82 (~P2(a5,a1,f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7381,7361,7339,7047,22,24])).
% 116.73/116.82 cnf(7411,plain,
% 116.73/116.82 (~P2(f7(a1,a1),f3(a1,a1),a4)),
% 116.73/116.82 inference(scs_inference,[],[7307,6461,7357,24])).
% 116.73/116.82 cnf(7425,plain,
% 116.73/116.82 (~P2(a2,a1,f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7305,6978,6982,24])).
% 116.73/116.82 cnf(7446,plain,
% 116.73/116.82 (~P2(f7(a1,a1),f6(a2),a1)),
% 116.73/116.82 inference(scs_inference,[],[7425,6968,7043,24])).
% 116.73/116.82 cnf(7448,plain,
% 116.73/116.82 (P2(a4,f6(a4),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7425,6968,7226,7043,6231,6282,24,25])).
% 116.73/116.82 cnf(7452,plain,
% 116.73/116.82 (P2(f6(a4),a4,f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7425,6765,6561,6968,7226,7194,7043,6698,6231,6282,24,25,29,21])).
% 116.73/116.82 cnf(7468,plain,
% 116.73/116.82 (~P4(f3(a1,a1),a4,f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[6,7452,7168,6502,7339,6789,6486,6478,6874,7274,7194,30,6227,24,25,28,29])).
% 116.73/116.82 cnf(7476,plain,
% 116.73/116.82 (~P4(a4,f3(a1,a1),f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7468,22])).
% 116.73/116.82 cnf(7478,plain,
% 116.73/116.82 (P4(f7(a4,a4),f6(a1),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7468,6518,6239,22,27])).
% 116.73/116.82 cnf(7480,plain,
% 116.73/116.82 (~P4(f6(a4),f8(a4),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7468,6518,6354,6239,106,22,27,26])).
% 116.73/116.82 cnf(7482,plain,
% 116.73/116.82 (~P2(f3(a1,a1),a4,f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7468,7232,7452,6908,6518,6354,6239,106,22,27,26,24])).
% 116.73/116.82 cnf(7484,plain,
% 116.73/116.82 (~P4(f3(a1,a1),f8(a4),f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7468,7448,7232,7452,6970,6908,6518,6354,6415,6239,106,22,27,26,24,28])).
% 116.73/116.82 cnf(7495,plain,
% 116.73/116.82 (~P4(f8(a4),f6(a4),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7480,22])).
% 116.73/116.82 cnf(7497,plain,
% 116.73/116.82 (~P4(a4,f6(a4),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7480,6298,6415,22,27])).
% 116.73/116.82 cnf(7499,plain,
% 116.73/116.82 (~P2(a4,a4,a4)),
% 116.73/116.82 inference(scs_inference,[],[6286,7480,7452,7194,6298,6415,22,27,24])).
% 116.73/116.82 cnf(7501,plain,
% 116.73/116.82 (~P4(f3(a1,a1),f8(a4),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[6286,7480,6797,7452,7194,6298,6354,6415,22,27,24,28])).
% 116.73/116.82 cnf(7510,plain,
% 116.73/116.82 (~P4(f3(a4,a4),f6(a1),a4)),
% 116.73/116.82 inference(scs_inference,[],[7337,7478,7497,7341,6947,6795,6348,22,24,28])).
% 116.73/116.82 cnf(7512,plain,
% 116.73/116.82 (~P4(f3(a1,a1),f3(a1,a1),f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7337,7478,7497,7476,7341,6947,6795,6908,6364,7194,6348,22,24,28,29])).
% 116.73/116.82 cnf(7516,plain,
% 116.73/116.82 (~P2(f7(a1,a1),f6(a1),a4)),
% 116.73/116.82 inference(scs_inference,[],[7482,7484,7352,6577,22,24])).
% 116.73/116.82 cnf(7520,plain,
% 116.73/116.82 (~P4(f6(a4),f3(a1,a1),f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7499,7512,7482,7484,7008,7352,7452,6908,6364,6577,22,24,28,29])).
% 116.73/116.82 cnf(7526,plain,
% 116.73/116.82 (~P2(f6(a5),f7(a1,a1),f6(a2))),
% 116.73/116.82 inference(scs_inference,[],[7520,7291,7280,7293,6335,2288,6321,22,25,24])).
% 116.73/116.82 cnf(7528,plain,
% 116.73/116.82 (~P4(f3(a1,a1),f6(a1),f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7371,7520,7291,7478,7280,7293,6455,6335,2288,6321,22,25,24,28])).
% 116.73/116.82 cnf(7530,plain,
% 116.73/116.82 (~P4(f7(a1,a1),f6(a4),a4)),
% 116.73/116.82 inference(scs_inference,[],[7371,7495,7520,7291,7478,7280,7293,7448,6455,7242,6335,2288,6321,6298,22,25,24,28,29])).
% 116.73/116.82 cnf(7534,plain,
% 116.73/116.82 (~P4(f8(a4),f3(a1,a1),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7501,22])).
% 116.73/116.82 cnf(7536,plain,
% 116.73/116.82 (~P2(a5,f6(a5),f6(a2))),
% 116.73/116.82 inference(scs_inference,[],[7501,7446,7341,6417,22,24])).
% 116.73/116.82 cnf(7541,plain,
% 116.73/116.82 (~P4(f3(a4,a4),f6(a1),f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7501,7446,7264,7065,7341,6417,6874,7478,6321,6348,22,24,25,28])).
% 116.73/116.82 cnf(7550,plain,
% 116.73/116.82 (~P2(f7(a1,a1),f6(a1),a2)),
% 116.73/116.82 inference(scs_inference,[],[6419,7530,7258,6886,22,24])).
% 116.73/116.82 cnf(7570,plain,
% 116.73/116.82 (~P2(a2,f3(a1,a1),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7528,7550,6978,6837,22,24])).
% 116.73/116.82 cnf(7580,plain,
% 116.73/116.82 (~P2(f6(a1),f3(a1,a1),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7541,7278,6461,7352,22,24])).
% 116.73/116.82 cnf(7587,plain,
% 116.73/116.82 (~P4(f3(a4,a4),a4,a4)),
% 116.73/116.82 inference(scs_inference,[],[7541,7499,7278,7303,6461,6856,7352,6380,7274,30,6241,6227,22,24,27,25,28])).
% 116.73/116.82 cnf(7591,plain,
% 116.73/116.82 (~P4(a4,f3(a4,a4),a4)),
% 116.73/116.82 inference(scs_inference,[],[7587,22])).
% 116.73/116.82 cnf(7593,plain,
% 116.73/116.82 (~P4(f7(a4,a4),f3(a4,a4),a4)),
% 116.73/116.82 inference(scs_inference,[],[7587,6384,6312,22,27])).
% 116.73/116.82 cnf(7595,plain,
% 116.73/116.82 (P4(f8(a4),f6(a2),f6(a2))),
% 116.73/116.82 inference(scs_inference,[],[7587,6542,6384,6312,6294,22,27,26])).
% 116.73/116.82 cnf(7597,plain,
% 116.73/116.82 (~P2(f6(a2),f6(a1),f6(a5))),
% 116.73/116.82 inference(scs_inference,[],[7526,7587,6542,6872,7357,6384,6312,6294,22,27,26,25])).
% 116.73/116.82 cnf(7599,plain,
% 116.73/116.82 (~P2(f6(a2),f7(a4,a4),f6(a2))),
% 116.73/116.82 inference(scs_inference,[],[7133,7526,7587,6542,6872,7357,6478,6843,6384,6312,6294,22,27,26,25,24])).
% 116.73/116.82 cnf(7601,plain,
% 116.73/116.82 (~P2(f8(a4),f8(a4),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7133,7526,7587,7499,6542,6872,7357,6478,6843,6384,6312,6294,22,27,26,25,24,28])).
% 116.73/116.82 cnf(7603,plain,
% 116.73/116.82 (~P2(f7(a4,a4),f7(a4,a4),a4)),
% 116.73/116.82 inference(scs_inference,[],[7133,7526,7587,7499,6542,6872,7357,6478,6843,6384,6312,6249,6348,6294,22,27,26,25,24,28,29])).
% 116.73/116.82 cnf(7608,plain,
% 116.73/116.82 (P4(f7(a4,a4),a2,a2)),
% 116.73/116.82 inference(scs_inference,[],[7593,6593,6239,22,27])).
% 116.73/116.82 cnf(7610,plain,
% 116.73/116.82 (~P4(f8(a4),a4,f3(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7591,7593,6593,6415,6239,6294,22,27,26])).
% 116.73/116.82 cnf(7623,plain,
% 116.73/116.82 (~P4(f3(a4,a4),f7(a4,a4),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7610,6350,6249,22,27])).
% 116.73/116.82 cnf(7625,plain,
% 116.73/116.82 (~P4(a4,a4,f3(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7610,7591,6350,6249,6227,22,27,26])).
% 116.73/116.82 cnf(7627,plain,
% 116.73/116.82 (~P2(a2,f6(a5),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7597,7610,7591,7166,6350,7034,6249,6227,22,27,26,24])).
% 116.73/116.82 cnf(7636,plain,
% 116.73/116.82 (~P4(a4,f3(a4,a4),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7623,6350,6268,22,27])).
% 116.73/116.82 cnf(7638,plain,
% 116.73/116.82 (~P2(f3(a1,a1),f3(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7623,7599,6872,6350,6268,22,27,24])).
% 116.73/116.82 cnf(7640,plain,
% 116.73/116.82 (~P4(f3(a4,a4),f8(a4),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7601,7623,7599,6872,6350,6268,6415,6241,22,27,24,28])).
% 116.73/116.82 cnf(7642,plain,
% 116.73/116.82 (~P2(f7(a4,a4),f6(a4),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7601,7623,7599,7103,6872,6350,7226,6268,6415,6241,6239,4067,22,27,24,28,29])).
% 116.73/116.82 cnf(7645,plain,
% 116.73/116.82 (~P4(f3(a4,a4),a4,f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7636,22])).
% 116.73/116.82 cnf(7647,plain,
% 116.73/116.82 (P4(f7(a4,a4),a1,a1)),
% 116.73/116.82 inference(scs_inference,[],[7636,6239,6553,22,27])).
% 116.73/116.82 cnf(7649,plain,
% 116.73/116.82 (~P4(f7(a4,a4),a1,f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7636,6615,6504,6239,6553,22,27,26])).
% 116.73/116.82 cnf(7651,plain,
% 116.73/116.82 (~P2(a1,a1,f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7636,7642,6615,6370,6504,6239,6553,22,27,26,24])).
% 116.73/116.82 cnf(7662,plain,
% 116.73/116.82 (~P4(f3(a1,a1),a4,f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7625,7369,7640,7258,6962,7194,6348,6239,22,24,29])).
% 116.73/116.82 cnf(7666,plain,
% 116.73/116.82 (~P2(f6(a5),f6(a5),f6(a2))),
% 116.73/116.82 inference(scs_inference,[],[7625,7369,7640,7647,6787,7258,7144,6962,6874,6321,7194,6348,6239,22,24,29,27,25])).
% 116.73/116.82 cnf(7671,plain,
% 116.73/116.82 (~P4(a4,f3(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7662,22])).
% 116.73/116.82 cnf(7675,plain,
% 116.73/116.82 (~P2(f3(a5,a5),f6(a5),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7398,7662,6308,7647,6335,6417,6306,22,26,24])).
% 116.73/116.82 cnf(7683,plain,
% 116.73/116.82 (~P4(f7(a4,a4),a1,f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7649,6711,7647,6504,22,26])).
% 116.73/116.82 cnf(7691,plain,
% 116.73/116.82 (~P4(f3(a4,a4),a1,f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7645,7649,7651,7278,7595,6711,7647,7341,6823,6504,6249,6348,22,26,24,29,27,28])).
% 116.73/116.82 cnf(7695,plain,
% 116.73/116.82 (~P2(f6(a2),f6(a1),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7691,7570,7297,7043,22,24])).
% 116.73/116.82 cnf(7699,plain,
% 116.73/116.82 (~P4(f6(a4),f3(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7691,7570,6551,7192,7297,6478,7647,7043,7226,6364,22,24,27,29])).
% 116.73/116.82 cnf(7705,plain,
% 116.73/116.82 (~P4(f7(a4,a4),f7(a4,a4),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7699,7671,6504,6306,22,26])).
% 116.73/116.82 cnf(7707,plain,
% 116.73/116.82 (~P2(f7(a1,a1),a2,f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7699,7695,7671,6933,6856,6504,6306,22,26,24])).
% 116.73/116.82 cnf(7715,plain,
% 116.73/116.82 (~P4(a1,f7(a4,a4),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7683,22])).
% 116.73/116.82 cnf(7717,plain,
% 116.73/116.82 (P4(f8(a4),f7(a2,a2),f7(a2,a2))),
% 116.73/116.82 inference(scs_inference,[],[7683,6396,6294,22,26])).
% 116.73/116.82 cnf(7726,plain,
% 116.73/116.82 (~P4(f6(a1),f3(a4,a4),a4)),
% 116.73/116.82 inference(scs_inference,[],[7510,22])).
% 116.73/116.82 cnf(7728,plain,
% 116.73/116.82 (~P4(f3(a4,a4),f3(a1,a1),f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7510,7497,6268,6698,22,26])).
% 116.73/116.82 cnf(7730,plain,
% 116.73/116.82 (P2(a4,f7(a1,a1),a4)),
% 116.73/116.82 inference(scs_inference,[],[7510,7497,6268,6903,6698,6272,22,26,25])).
% 116.73/116.82 cnf(7734,plain,
% 116.73/116.82 (P2(f7(a1,a1),a4,a4)),
% 116.73/116.82 inference(scs_inference,[],[7707,7510,7497,7293,7297,6268,6903,6698,6272,22,26,25,24,21])).
% 116.73/116.82 cnf(7743,plain,
% 116.73/116.82 (~P4(f7(a4,a4),f3(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7705,7728,6404,6504,22,26])).
% 116.73/116.82 cnf(7745,plain,
% 116.73/116.82 (P2(f3(a1,a1),a1,f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7705,7728,6858,6557,7210,6404,6504,22,26,25])).
% 116.73/116.82 cnf(7747,plain,
% 116.73/116.82 (~P2(a4,f7(a1,a1),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7705,7728,7411,7730,7734,6858,6557,7210,6404,6504,22,26,25,24])).
% 116.73/116.82 cnf(7749,plain,
% 116.73/116.82 (P2(a1,f3(a1,a1),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7705,7728,7411,7730,7734,6858,6557,7210,6404,6504,22,26,25,24,21])).
% 116.73/116.82 cnf(7759,plain,
% 116.73/116.82 (~P4(a4,f7(a4,a4),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7743,7671,6306,6227,22,26])).
% 116.73/116.82 cnf(7761,plain,
% 116.73/116.82 (P2(f6(a1),f6(a2),f6(a2))),
% 116.73/116.82 inference(scs_inference,[],[7743,7749,7671,6528,6472,6306,6227,22,26,25])).
% 116.73/116.82 cnf(7763,plain,
% 116.73/116.82 (~P2(a4,f7(a1,a1),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7743,7516,7749,7734,7671,7730,6528,6472,6306,6227,22,26,25,24])).
% 116.73/116.82 cnf(7767,plain,
% 116.73/116.82 (P2(f6(a2),f6(a1),f6(a2))),
% 116.73/116.82 inference(scs_inference,[],[7743,7516,7749,7734,7671,7730,7645,6528,6472,6306,6241,6227,22,26,25,24,29,21])).
% 116.73/116.82 cnf(7775,plain,
% 116.73/116.82 (~P4(f3(a4,a4),f3(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7759,7705,6384,6698,22,26])).
% 116.73/116.82 cnf(7777,plain,
% 116.73/116.82 (P2(f7(a1,a1),f6(a1),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7759,7767,7705,7043,6384,6698,22,26,25])).
% 116.73/116.82 cnf(7781,plain,
% 116.73/116.82 (~P4(f7(a1,a1),a1,f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7627,7745,7759,7767,7705,7649,6645,6843,7647,7043,6413,6384,6698,22,26,25,24,29])).
% 116.73/116.82 cnf(7783,plain,
% 116.73/116.82 (P2(f6(a1),f7(a1,a1),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7627,7745,7759,7767,7705,7649,6645,6843,7647,7043,6413,6384,6698,22,26,25,24,29,21])).
% 116.73/116.82 cnf(7787,plain,
% 116.73/116.82 (~P4(f7(a1,a1),a5,a2)),
% 116.73/116.82 inference(scs_inference,[],[6,7627,7745,7759,7767,7717,7705,7649,7734,6645,6843,6372,7647,6575,7043,6413,6384,6698,22,26,25,24,29,21,27,28])).
% 116.73/116.82 cnf(7795,plain,
% 116.73/116.82 (~P4(f6(a1),f3(a4,a4),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7775,7726,6312,6294,22,26])).
% 116.73/116.82 cnf(7797,plain,
% 116.73/116.82 (~P2(f6(a1),f8(a4),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7775,7777,7389,7726,7242,6312,6294,22,26,24])).
% 116.73/116.82 cnf(7799,plain,
% 116.73/116.82 (P2(a4,f6(a1),a4)),
% 116.73/116.82 inference(scs_inference,[],[7775,7777,7389,7726,7730,7242,6312,6294,22,26,24,25])).
% 116.73/116.82 cnf(7803,plain,
% 116.73/116.82 (~P4(f7(a1,a1),f3(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7775,7777,7389,7726,7625,6613,7730,6455,7242,6312,6698,6294,22,26,24,25,27,29])).
% 116.73/116.82 cnf(7805,plain,
% 116.73/116.82 (P2(f6(a1),a4,a4)),
% 116.73/116.82 inference(scs_inference,[],[7775,7777,7389,7726,7625,6613,7730,6455,7242,6312,6698,6294,22,26,24,25,27,29,21])).
% 116.73/116.82 cnf(7812,plain,
% 116.73/116.82 (~P4(f3(a1,a1),f7(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7803,22])).
% 116.73/116.82 cnf(7816,plain,
% 116.73/116.82 (P2(f6(a1),f6(a1),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7803,6647,7799,7805,7749,7258,6632,22,24,25])).
% 116.73/116.82 cnf(7818,plain,
% 116.73/116.82 (~P4(a4,f7(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7803,6647,7799,7805,7749,7202,7258,6632,6268,6530,22,24,25,27])).
% 116.73/116.82 cnf(7820,plain,
% 116.73/116.82 (~P4(f3(a4,a4),f6(a5),f6(a2))),
% 116.73/116.82 inference(scs_inference,[],[7803,6647,7666,7799,7805,7749,7202,7258,7228,6632,6268,6530,6348,22,24,25,27,28])).
% 116.73/116.82 cnf(7830,plain,
% 116.73/116.82 (~P4(a4,f7(a4,a4),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7787,7818,6306,6227,22,26])).
% 116.73/116.82 cnf(7832,plain,
% 116.73/116.82 (~P2(f6(a4),f6(a1),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[6692,7787,7818,7783,7293,6306,6227,22,26,24])).
% 116.73/116.82 cnf(7834,plain,
% 116.73/116.82 (P2(f8(a4),f6(a1),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[6692,7787,7818,7783,7777,7234,7293,6306,6227,22,26,24,25])).
% 116.73/116.82 cnf(7836,plain,
% 116.73/116.82 (~P4(f3(a4,a4),a1,f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[6692,7787,7818,7783,7067,7777,7234,7293,7647,6306,6348,6227,22,26,24,25,28])).
% 116.73/116.82 cnf(7838,plain,
% 116.73/116.82 (~P4(f6(a4),f7(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7812,6692,7787,7818,7783,7067,7777,7234,7293,6630,7448,7647,6323,6306,6348,6227,22,26,24,25,28,29])).
% 116.73/116.82 cnf(7840,plain,
% 116.73/116.82 (P2(f6(a1),f8(a4),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7812,6692,7787,7818,7783,7067,7777,7234,7293,6630,7448,7647,6323,6306,6348,6227,22,26,24,25,28,29,21])).
% 116.73/116.82 cnf(7848,plain,
% 116.73/116.82 (~P4(f7(a4,a4),f7(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7820,7830,6559,6306,22,26])).
% 116.73/116.82 cnf(7852,plain,
% 116.73/116.82 (P2(f3(a1,a1),f7(a1,a1),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7183,7820,7830,7834,7816,7783,7293,6559,6306,22,26,24,25])).
% 116.73/116.82 cnf(7854,plain,
% 116.73/116.82 (~P4(f7(a4,a4),f8(a4),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7183,7820,7830,7834,7816,7783,7662,7293,6559,6249,6306,6294,22,26,24,25,27])).
% 116.73/116.82 cnf(7858,plain,
% 116.73/116.82 (~P4(f6(a1),f3(a1,a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7832,7183,7820,7830,7834,7816,7743,7783,7662,6707,7293,7478,6455,6559,6249,6306,6404,6294,22,26,24,25,27,28,29])).
% 116.73/116.82 cnf(7860,plain,
% 116.73/116.82 (P2(f7(a1,a1),f3(a1,a1),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7832,7183,7820,7830,7834,7816,7743,7783,7662,6707,7293,7478,6455,6559,6249,6306,6404,6294,22,26,24,25,27,28,29,21])).
% 116.73/116.82 cnf(7864,plain,
% 116.73/116.82 (~P4(f7(a4,a4),f7(a4,a4),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7848,6504,22,26])).
% 116.73/116.82 cnf(7868,plain,
% 116.73/116.82 (P2(f6(a1),a1,f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7848,7840,7860,7580,7834,7745,7777,6504,22,26,24,25])).
% 116.73/116.82 cnf(7870,plain,
% 116.73/116.82 (~P4(f3(a1,a1),a1,a2)),
% 116.73/116.82 inference(scs_inference,[],[7848,7840,7860,7580,6802,7834,7745,7777,6968,6504,6274,22,26,24,25,29])).
% 116.73/116.82 cnf(7872,plain,
% 116.73/116.82 (P2(a1,f6(a1),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7848,7840,7860,7580,6802,7834,7745,7777,6968,6504,6274,22,26,24,25,29,21])).
% 116.73/116.82 cnf(7876,plain,
% 116.73/116.82 (~P4(f6(a1),a4,f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7848,7840,7860,7580,6802,6286,7834,7745,7777,7595,6878,6968,6504,6294,6274,22,26,24,25,29,21,27,28])).
% 116.73/116.82 cnf(7880,plain,
% 116.73/116.82 (~P4(a1,a1,f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7864,7836,7647,6274,22,26])).
% 116.73/116.82 cnf(7884,plain,
% 116.73/116.82 (~P4(f8(a4),f6(a4),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7864,7045,7836,7876,7872,7647,6298,6229,6274,4067,22,26,24,27])).
% 116.73/116.82 cnf(7886,plain,
% 116.73/116.82 (~P4(f7(a4,a4),a1,f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7864,7045,7836,7876,7126,7872,6270,7647,6298,6229,6274,4067,22,26,24,27,28])).
% 116.73/116.82 cnf(7893,plain,
% 116.73/116.82 (~P4(f8(a4),f7(a4,a4),f3(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7854,22])).
% 116.73/116.82 cnf(7897,plain,
% 116.73/116.82 (~P4(f6(a4),a4,f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7638,7854,7852,7876,6707,6227,4067,22,24,27])).
% 116.73/116.82 cnf(7899,plain,
% 116.73/116.82 (~P4(f6(a1),f6(a4),a4)),
% 116.73/116.82 inference(scs_inference,[],[7638,7854,7852,7876,7495,7840,6707,7448,6298,6227,4067,22,24,27,29])).
% 116.73/116.82 cnf(7905,plain,
% 116.73/116.82 (~P4(a4,f6(a4),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7897,22])).
% 116.73/116.82 cnf(7907,plain,
% 116.73/116.82 (~P2(f6(a1),f6(a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7897,7599,7767,22,24])).
% 116.73/116.82 cnf(7913,plain,
% 116.73/116.82 (P2(f3(a1,a1),f6(a1),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7897,7893,7599,7872,7717,7767,7783,6991,6239,4067,22,24,27,26,25])).
% 116.73/116.82 cnf(7915,plain,
% 116.73/116.82 (P2(f6(a1),f3(a1,a1),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[7897,7893,7599,7872,7717,7767,7783,6991,6239,4067,22,24,27,26,25,21])).
% 116.73/116.82 cnf(7921,plain,
% 116.73/116.82 (~P4(f6(a1),f6(a4),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7858,7899,6294,4067,22,26])).
% 116.73/116.82 cnf(7925,plain,
% 116.73/116.82 (P2(f7(a1,a1),a1,f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7032,7858,7899,7913,7868,7852,6398,6294,4067,22,26,24,25])).
% 116.73/116.82 cnf(7929,plain,
% 116.73/116.82 (P2(a1,f7(a1,a1),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7032,7858,7899,7715,7913,7868,7852,6398,7647,6249,6294,4067,22,26,24,25,27,21])).
% 116.73/116.82 cnf(7948,plain,
% 116.73/116.82 (~P4(f3(a4,a4),f6(a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7838,7534,7907,7915,7350,7925,7717,7478,6348,22,24,26,28])).
% 116.73/116.82 cnf(7950,plain,
% 116.73/116.82 (~P4(f7(a1,a1),a1,a2)),
% 116.73/116.82 inference(scs_inference,[],[7838,7870,7534,7907,7915,7350,7925,7717,6599,6968,7478,6348,6274,22,24,26,28,29])).
% 116.73/116.82 cnf(7956,plain,
% 116.73/116.82 (~P4(a4,f6(a1),f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7781,7884,6518,6294,22,26])).
% 116.73/116.82 cnf(7960,plain,
% 116.73/116.82 (~P4(f6(a1),a4,f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7603,7326,7781,7884,7915,7799,6461,6518,6239,6227,6294,22,26,24,28])).
% 116.73/116.82 cnf(7968,plain,
% 116.73/116.82 (~P4(f7(a4,a4),f7(a1,a1),f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7950,7036,6384,6530,22,27])).
% 116.73/116.82 cnf(7970,plain,
% 116.73/116.82 (~P2(a4,f3(a1,a1),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7950,7763,7915,7036,7799,6384,6530,22,27,24])).
% 116.73/116.82 cnf(7985,plain,
% 116.73/116.82 (P2(f7(a1,a1),f7(a1,a1),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7886,7797,7956,7929,7317,7868,6354,106,22,26,24,25])).
% 116.73/116.82 cnf(7995,plain,
% 116.73/116.82 (~P4(a4,f7(a1,a1),f6(a4))),
% 116.73/116.82 inference(scs_inference,[],[7948,7968,6559,6306,22,27])).
% 116.73/116.82 cnf(8003,plain,
% 116.73/116.82 (~P4(f7(a1,a1),a2,f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7083,7675,7948,7968,7905,7860,7913,7280,7166,6486,7608,6630,7478,6559,6306,22,27,26,24,25,28])).
% 116.73/116.82 cnf(8005,plain,
% 116.73/116.82 (P2(a5,f6(a5),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7083,7675,7948,7968,7905,7860,7913,7280,7166,6486,7608,6630,7478,6559,6306,22,27,26,24,25,28,21])).
% 116.73/116.82 cnf(8011,plain,
% 116.73/116.82 (~P4(f7(a4,a4),f7(a4,a4),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7795,7960,6504,6249,22,27])).
% 116.73/116.82 cnf(8021,plain,
% 116.73/116.82 (~P4(f7(a4,a4),a4,f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[7921,7960,6249,6227,22,27])).
% 116.73/116.82 cnf(8023,plain,
% 116.73/116.82 (~P4(f7(a4,a4),f6(a1),f7(a4,a4))),
% 116.73/116.82 inference(scs_inference,[],[7921,8011,7960,7478,6504,6249,6227,22,27,26])).
% 116.73/116.82 cnf(8025,plain,
% 116.73/116.82 (~P2(f6(a5),f6(a2),f6(a5))),
% 116.73/116.82 inference(scs_inference,[],[7921,8011,7536,8005,7761,7960,7478,6504,6249,6227,22,27,26,24])).
% 116.73/116.82 cnf(8035,plain,
% 116.73/116.82 (~P4(a4,f7(a4,a4),f6(a1))),
% 116.73/116.82 inference(scs_inference,[],[8023,8021,6306,6249,22,27])).
% 116.73/116.82 cnf(8037,plain,
% 116.73/116.82 (~P4(f8(a4),f6(a4),f7(a1,a1))),
% 116.73/116.82 inference(scs_inference,[],[8023,7995,8021,6298,6306,6249,6415,22,27,26])).
% 116.73/116.82 cnf(8054,plain,
% 116.73/116.82 (~P4(f6(a1),f8(a4),f8(a4))),
% 116.73/116.82 inference(scs_inference,[],[7880,8037,7747,8035,7601,7805,7799,6270,7226,7478,7448,6415,6239,6553,22,26,24,29,28])).
% 116.73/116.82 cnf(8069,plain,
% 116.73/116.82 (~P4(f6(a1),a4,a4)),
% 116.73/116.82 inference(scs_inference,[],[8003,8054,6415,22,27,26])).
% 116.73/116.82 cnf(8071,plain,
% 116.73/116.82 (~P2(f7(a1,a1),f7(a1,a1),f6(a2))),
% 116.73/116.82 inference(scs_inference,[],[8003,8025,8054,7159,6415,22,27,26,24])).
% 116.73/116.82 cnf(8088,plain,
% 116.73/116.82 (P2(a2,f6(a1),a2)),
% 116.73/116.82 inference(scs_inference,[],[8069,8071,7970,7985,6954,6978,6323,6241,6294,22,27,24,25,28,21])).
% 116.73/116.82 cnf(9754,plain,
% 116.73/116.82 ($false),
% 116.73/116.82 inference(scs_inference,[],[4,6294,6272,6874,6266,6284,6804,6795,7210,8088,6362,21,22,6317,5020,5084,2013,2038,2285,2421,2694,3208,2036,2283,16]),
% 116.73/116.82 ['proof']).
% 116.73/116.82 % SZS output end Proof
% 116.73/116.82 % Total time :116.130000s
%------------------------------------------------------------------------------