%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD040-5 : 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 : n007.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:23 EDT 2024
% Result : Unsatisfiable 65.52s 65.56s
% Output : CNFRefutation 65.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : FLD040-5 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n007.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 10:56:39 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.44/0.63 start to proof:theBenchmark
% 65.52/65.55 %-------------------------------------------
% 65.52/65.55 % File :CSE---1.7
% 65.52/65.55 % Problem :theBenchmark
% 65.52/65.55 % Transform :cnf
% 65.52/65.55 % Format :tptp:raw
% 65.52/65.55 % Command :java -jar mcs_scs.jar %d %s
% 65.52/65.55
% 65.52/65.55 % Result :Theorem 64.870000s
% 65.52/65.55 % Output :CNFRefutation 64.870000s
% 65.52/65.55 %-------------------------------------------
% 65.52/65.56 %--------------------------------------------------------------------------
% 65.52/65.56 % File : FLD040-5 : TPTP v8.2.0. Bugfixed v2.1.0.
% 65.52/65.56 % Domain : Field Theory (Ordered fields)
% 65.52/65.56 % Problem : If a is not 0, then the multiplicative inverse of a is not 0
% 65.52/65.56 % Version : [Dra93] axioms : Especial.
% 65.52/65.56 % Theorem formulation : Relational variant with re axiom set.
% 65.52/65.56 % English :
% 65.52/65.56
% 65.52/65.56 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 65.52/65.56 % Source : [Dra93]
% 65.52/65.56 % Names :
% 65.52/65.56
% 65.52/65.56 % Status : Unsatisfiable
% 65.52/65.56 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.25 v6.3.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.10 v5.2.0, 0.00 v5.1.0, 0.09 v5.0.0, 0.14 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0, 0.20 v2.3.0, 0.00 v2.2.1, 0.33 v2.1.0
% 65.52/65.56 % Syntax : Number of clauses : 29 ( 6 unt; 3 nHn; 29 RR)
% 65.52/65.56 % Number of literals : 80 ( 0 equ; 50 neg)
% 65.52/65.56 % Maximal clause size : 5 ( 2 avg)
% 65.52/65.56 % Maximal term depth : 2 ( 1 avg)
% 65.52/65.56 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 65.52/65.56 % Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% 65.52/65.56 % Number of variables : 73 ( 0 sgn)
% 65.52/65.56 % SPC : CNF_UNS_RFO_NEQ_NHN
% 65.52/65.56
% 65.52/65.56 % Comments :
% 65.52/65.56 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 65.52/65.56 %--------------------------------------------------------------------------
% 65.52/65.56 include('Axioms/FLD002-0.ax').
% 65.52/65.56 %--------------------------------------------------------------------------
% 65.52/65.56 cnf(a_is_defined,hypothesis,
% 65.52/65.56 defined(a) ).
% 65.52/65.56
% 65.52/65.56 cnf(not_sum_2,negated_conjecture,
% 65.52/65.56 ~ sum(additive_identity,a,additive_identity) ).
% 65.52/65.56
% 65.52/65.56 cnf(sum_3,negated_conjecture,
% 65.52/65.56 sum(additive_identity,multiplicative_inverse(a),additive_identity) ).
% 65.52/65.56
% 65.52/65.56 %--------------------------------------------------------------------------
% 65.52/65.56 %-------------------------------------------
% 65.52/65.56 % Proof found
% 65.52/65.56 % SZS status Theorem for theBenchmark
% 65.52/65.56 % SZS output start Proof
% 65.52/65.57 %ClaNum:29(EqnAxiom:0)
% 65.52/65.57 %VarNum:162(SingletonVarNum:73)
% 65.52/65.57 %MaxLitNum:5
% 65.52/65.57 %MaxfuncDepth:1
% 65.52/65.57 %SharedTerms:10
% 65.52/65.57 %goalClause: 4 6
% 65.52/65.57 %singleGoalClaCount:2
% 65.52/65.57 [1]P1(a1)
% 65.52/65.57 [2]P1(a4)
% 65.52/65.57 [3]P1(a2)
% 65.52/65.57 [5]~P2(a1,a1,a4)
% 65.52/65.57 [6]~P2(a1,a2,a1)
% 65.52/65.57 [4]P2(a1,f6(a2),a1)
% 65.52/65.57 [12]~P1(x121)+P2(a1,x121,x121)
% 65.52/65.57 [13]~P1(x131)+P4(a4,x131,x131)
% 65.52/65.57 [7]~P1(x71)+P1(f5(x71))
% 65.52/65.57 [14]~P1(x141)+P2(f5(x141),x141,a1)
% 65.52/65.57 [21]~P2(x212,x211,x213)+P2(x211,x212,x213)
% 65.52/65.57 [22]~P4(x222,x221,x223)+P4(x221,x222,x223)
% 65.52/65.57 [15]~P1(x151)+P2(a1,x151,a1)+P1(f6(x151))
% 65.52/65.57 [19]~P1(x191)+P4(f6(x191),x191,a4)+P2(a1,x191,a1)
% 65.52/65.57 [18]~P3(x182,x181)+~P3(x181,x182)+P2(a1,x181,x182)
% 65.52/65.57 [9]~P1(x92)+~P1(x91)+P1(f3(x91,x92))
% 65.52/65.57 [10]~P1(x102)+~P1(x101)+P1(f7(x101,x102))
% 65.52/65.57 [16]~P1(x162)+~P1(x161)+P2(x161,x162,f3(x161,x162))
% 65.52/65.57 [17]~P1(x172)+~P1(x171)+P4(x171,x172,f7(x171,x172))
% 65.52/65.57 [11]~P3(x111,x113)+P3(x111,x112)+~P3(x113,x112)
% 65.52/65.57 [8]P3(x82,x81)+~P1(x81)+~P1(x82)+P3(x81,x82)
% 65.52/65.57 [20]~P4(x203,x202,x201)+P3(a1,x201)+~P3(a1,x202)+~P3(a1,x203)
% 65.52/65.57 [23]~P2(x233,x235,x231)+P3(x231,x232)+~P2(x234,x235,x232)+~P3(x233,x234)
% 65.52/65.57 [24]~P2(x241,x246,x244)+P2(x241,x242,x243)+~P2(x244,x245,x243)+~P2(x246,x245,x242)
% 65.52/65.57 [25]~P2(x256,x254,x251)+P2(x251,x252,x253)+~P2(x254,x252,x255)+~P2(x256,x255,x253)
% 65.52/65.57 [26]~P4(x261,x266,x264)+P4(x261,x262,x263)+~P4(x264,x265,x263)+~P4(x266,x265,x262)
% 65.52/65.57 [27]~P4(x276,x274,x271)+P4(x271,x272,x273)+~P4(x274,x272,x275)+~P4(x276,x275,x273)
% 65.52/65.57 [28]~P4(x285,x287,x282)+~P4(x284,x287,x281)+P2(x281,x282,x283)+~P2(x284,x285,x286)+~P4(x286,x287,x283)
% 65.52/65.57 [29]~P4(x297,x292,x295)+~P4(x296,x292,x294)+P4(x291,x292,x293)+~P2(x294,x295,x293)+~P2(x296,x297,x291)
% 65.52/65.57 %EqnAxiom
% 65.52/65.57
% 65.52/65.57 %-------------------------------------------
% 65.52/65.58 cnf(30,plain,
% 65.52/65.58 (~P2(a2,a1,a1)),
% 65.52/65.58 inference(scs_inference,[],[6,21])).
% 65.52/65.58 cnf(32,plain,
% 65.52/65.58 (~P2(f6(a2),a2,f6(a2))),
% 65.52/65.58 inference(scs_inference,[],[4,6,21,25])).
% 65.52/65.58 cnf(34,plain,
% 65.52/65.58 (P3(a1,a1)),
% 65.52/65.58 inference(scs_inference,[],[4,6,1,21,25,8])).
% 65.52/65.58 cnf(38,plain,
% 65.52/65.58 (~P2(a1,a1,x381)+~P2(x381,f6(a2),a4)),
% 65.52/65.58 inference(scs_inference,[],[4,6,1,5,21,25,8,18,24])).
% 65.52/65.58 cnf(41,plain,
% 65.52/65.58 (~P2(a2,f6(a2),f6(a2))),
% 65.52/65.58 inference(scs_inference,[],[32,21])).
% 65.52/65.58 cnf(43,plain,
% 65.52/65.58 (P3(a4,a4)),
% 65.52/65.58 inference(scs_inference,[],[32,2,21,8])).
% 65.52/65.58 cnf(50,plain,
% 65.52/65.58 (P3(a2,a2)),
% 65.52/65.58 inference(scs_inference,[],[3,8])).
% 65.52/65.58 cnf(82,plain,
% 65.52/65.58 (P2(a1,f5(a4),f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[2,12,7])).
% 65.52/65.58 cnf(83,plain,
% 65.52/65.58 (~P2(x831,a1,a1)+P2(x831,f5(a4),f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[82,24])).
% 65.52/65.58 cnf(102,plain,
% 65.52/65.58 (P4(a4,f5(a4),f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[2,13,7])).
% 65.52/65.58 cnf(103,plain,
% 65.52/65.58 (~P4(x1031,a4,a4)+P4(x1031,f5(a4),f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[102,26])).
% 65.52/65.58 cnf(171,plain,
% 65.52/65.58 (P2(f5(f5(a4)),f5(a4),a1)),
% 65.52/65.58 inference(scs_inference,[],[2,14,7])).
% 65.52/65.58 cnf(172,plain,
% 65.52/65.58 (~P2(f5(a4),a2,f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[6,171,25])).
% 65.52/65.58 cnf(174,plain,
% 65.52/65.58 (~P2(a2,f5(a4),f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[6,171,25,21])).
% 65.52/65.58 cnf(223,plain,
% 65.52/65.58 (P4(f5(a4),x2231,f5(a4))+~P4(a4,x2231,a4)),
% 65.52/65.58 inference(scs_inference,[],[102,22,27])).
% 65.52/65.58 cnf(239,plain,
% 65.52/65.58 (~P2(f6(a2),x2391,a4)+~P2(a1,a1,x2391)),
% 65.52/65.58 inference(scs_inference,[],[38,21])).
% 65.52/65.58 cnf(271,plain,
% 65.52/65.58 (~P2(f6(a2),a1,x2711)+~P2(x2711,f6(a2),a4)+~P2(a1,a1,a1)),
% 65.52/65.58 inference(scs_inference,[],[4,239,24])).
% 65.52/65.58 cnf(303,plain,
% 65.52/65.58 (P3(f5(a4),f5(a4))+~P2(a1,a1,a1)),
% 65.52/65.58 inference(scs_inference,[],[34,83,23])).
% 65.52/65.58 cnf(319,plain,
% 65.52/65.58 (P3(f5(a4),f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[1,303,12])).
% 65.52/65.58 cnf(335,plain,
% 65.52/65.58 (P4(f5(a4),x3351,f5(a4))+~P4(x3351,a4,a4)),
% 65.52/65.58 inference(scs_inference,[],[103,22])).
% 65.52/65.58 cnf(351,plain,
% 65.52/65.58 (P4(x3511,f5(a4),f5(a4))+~P4(a4,x3511,a4)),
% 65.52/65.58 inference(scs_inference,[],[223,22])).
% 65.52/65.58 cnf(367,plain,
% 65.52/65.58 (~P4(f5(a4),a4,x3671)+P4(x3671,f5(a4),f5(a4))+~P4(f5(a4),a4,a4)),
% 65.52/65.58 inference(scs_inference,[],[102,335,27])).
% 65.52/65.58 cnf(383,plain,
% 65.52/65.58 (~P4(x3831,a4,x3832)+P4(x3831,f5(a4),f5(a4))+~P4(a4,x3832,a4)),
% 65.52/65.58 inference(scs_inference,[],[102,351,26])).
% 65.52/65.58 cnf(635,plain,
% 65.52/65.58 (~P2(x6351,f6(a2),a4)+~P2(f6(a2),a1,x6351)),
% 65.52/65.58 inference(scs_inference,[],[1,271,12])).
% 65.52/65.58 cnf(651,plain,
% 65.52/65.58 (~P2(a1,f6(a2),a4)),
% 65.52/65.58 inference(scs_inference,[],[4,635,21])).
% 65.52/65.58 cnf(652,plain,
% 65.52/65.58 (~P2(f6(a2),a1,a4)),
% 65.52/65.58 inference(scs_inference,[],[651,21])).
% 65.52/65.58 cnf(992,plain,
% 65.52/65.58 (P4(f5(a4),x9921,f5(a4))+~P4(x9921,a4,x9922)+~P4(a4,x9922,a4)),
% 65.52/65.58 inference(scs_inference,[],[383,22])).
% 65.52/65.58 cnf(1134,plain,
% 65.52/65.58 (P4(f5(a4),a4,f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[2,992,13])).
% 65.52/65.58 cnf(1479,plain,
% 65.52/65.58 (P2(a1,f5(a1),f5(a1))),
% 65.52/65.58 inference(scs_inference,[],[1,7,12])).
% 65.52/65.58 cnf(1483,plain,
% 65.52/65.58 (~P2(x14831,a1,a1)+P2(x14831,f5(a1),f5(a1))),
% 65.52/65.58 inference(scs_inference,[],[1479,24])).
% 65.52/65.58 cnf(1499,plain,
% 65.52/65.58 (P3(f5(a1),f5(a1))+~P2(a1,a1,a1)),
% 65.52/65.58 inference(scs_inference,[],[1479,34,1483,23])).
% 65.52/65.58 cnf(1515,plain,
% 65.52/65.58 (P3(f5(a1),f5(a1))),
% 65.52/65.58 inference(scs_inference,[],[1,1499,12])).
% 65.52/65.58 cnf(1626,plain,
% 65.52/65.58 (P2(f5(f5(a1)),f5(a1),a1)),
% 65.52/65.58 inference(scs_inference,[],[1,7,14])).
% 65.52/65.58 cnf(1629,plain,
% 65.52/65.58 (~P2(a2,f5(a1),f5(a1))),
% 65.52/65.58 inference(scs_inference,[],[6,1626,25,21])).
% 65.52/65.58 cnf(1662,plain,
% 65.52/65.58 (P4(a4,f5(a1),f5(a1))),
% 65.52/65.58 inference(scs_inference,[],[1,7,13])).
% 65.52/65.58 cnf(1940,plain,
% 65.52/65.58 (P2(a1,f3(a1,a1),f3(a1,a1))),
% 65.52/65.58 inference(scs_inference,[],[1,12,9])).
% 65.52/65.58 cnf(1944,plain,
% 65.52/65.58 (~P2(x19441,a1,a1)+P2(x19441,f3(a1,a1),f3(a1,a1))),
% 65.52/65.58 inference(scs_inference,[],[1940,24])).
% 65.52/65.58 cnf(1960,plain,
% 65.52/65.58 (P2(f3(a1,a1),x19601,f3(a1,a1))+~P2(x19601,a1,a1)),
% 65.52/65.58 inference(scs_inference,[],[1944,21])).
% 65.52/65.58 cnf(2150,plain,
% 65.52/65.58 (P2(f3(a1,a1),a1,f3(a1,a1))),
% 65.52/65.58 inference(scs_inference,[],[1,12,1960])).
% 65.52/65.58 cnf(2151,plain,
% 65.52/65.58 (P2(f3(a1,a1),f6(a2),f3(a1,a1))),
% 65.52/65.58 inference(scs_inference,[],[4,2150,25])).
% 65.52/65.58 cnf(2249,plain,
% 65.52/65.58 (P2(a1,f7(a1,a1),f7(a1,a1))),
% 65.52/65.58 inference(scs_inference,[],[1,12,10])).
% 65.52/65.58 cnf(2330,plain,
% 65.52/65.58 (P2(a1,f6(a2),f6(a2))),
% 65.52/65.58 inference(scs_inference,[],[6,3,12,15])).
% 65.52/65.58 cnf(2521,plain,
% 65.52/65.58 (P4(a1,a4,a1)),
% 65.52/65.58 inference(scs_inference,[],[1,13,22])).
% 65.52/65.58 cnf(2522,plain,
% 65.52/65.58 (P4(a1,x25221,a1)+~P4(a4,x25221,a4)),
% 65.52/65.58 inference(scs_inference,[],[2521,27])).
% 65.52/65.58 cnf(2547,plain,
% 65.52/65.58 (~P4(x25471,a4,a4)+P4(a1,x25471,a1)),
% 65.52/65.58 inference(scs_inference,[],[2522,22])).
% 65.52/65.58 cnf(2784,plain,
% 65.52/65.58 (~P4(a4,a4,x27841)+P4(x27841,f5(a4),f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[102,27])).
% 65.52/65.58 cnf(2818,plain,
% 65.52/65.58 (P2(f5(a4),f5(a4),f5(a4))+~P2(x28181,a4,a4)+~P4(a4,a4,x28181)),
% 65.52/65.58 inference(scs_inference,[],[102,2784,28])).
% 65.52/65.58 cnf(2889,plain,
% 65.52/65.58 (~P4(x28891,a4,a2)+~P2(f5(a4),x28891,f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[172,1134,28])).
% 65.52/65.58 cnf(2891,plain,
% 65.52/65.58 (~P4(a4,x28911,a2)+~P2(f5(a4),x28911,f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[172,1134,28,22])).
% 65.52/65.58 cnf(2894,plain,
% 65.52/65.58 (~P4(x28941,f5(a4),a2)+~P2(a4,x28941,a4)),
% 65.52/65.58 inference(scs_inference,[],[172,102,28])).
% 65.52/65.58 cnf(2942,plain,
% 65.52/65.58 (~P2(f5(a4),f5(a4),a2)+~P2(a4,a4,x29421)+~P2(a4,x29421,a4)),
% 65.52/65.58 inference(scs_inference,[],[102,2894,29])).
% 65.52/65.58 cnf(2974,plain,
% 65.52/65.58 (~P4(a1,a4,a2)),
% 65.52/65.58 inference(scs_inference,[],[82,2889,21])).
% 65.52/65.58 cnf(2975,plain,
% 65.52/65.58 (~P4(a4,a1,a2)),
% 65.52/65.58 inference(scs_inference,[],[2974,22])).
% 65.52/65.58 cnf(2992,plain,
% 65.52/65.58 (~P4(a4,a4,x29921)+~P4(a4,f5(a4),a2)+~P2(x29921,a4,a4)),
% 65.52/65.58 inference(scs_inference,[],[2891,2818])).
% 65.52/65.58 cnf(3634,plain,
% 65.52/65.58 (~P2(f3(a1,a1),a1,a4)+~P2(f6(a2),a1,f3(a1,a1))),
% 65.52/65.58 inference(scs_inference,[],[652,2150,1940,2330,25,24])).
% 65.52/65.58 cnf(3662,plain,
% 65.52/65.58 (~P4(a4,a4,x36621)+P4(f5(a4),x36621,f5(a4))),
% 65.52/65.58 inference(scs_inference,[],[1134,26])).
% 65.52/65.58 cnf(3665,plain,
% 65.52/65.58 (~P4(a4,a4,x36651)+P4(a1,x36651,a1)),
% 65.52/65.58 inference(scs_inference,[],[2521,26])).
% 65.52/65.58 cnf(3676,plain,
% 65.52/65.58 (P4(x36761,a1,a1)+~P4(a4,a4,x36761)),
% 65.52/65.58 inference(scs_inference,[],[3665,22])).
% 65.52/65.58 cnf(3698,plain,
% 65.52/65.58 (P2(f6(a2),a1,a1)),
% 65.52/65.58 inference(scs_inference,[],[4,21])).
% 65.52/65.58 cnf(3700,plain,
% 65.52/65.59 (P2(f6(a2),f5(a4),f5(a4))),
% 65.52/65.59 inference(scs_inference,[],[4,21,83])).
% 65.52/65.59 cnf(3702,plain,
% 65.52/65.59 (P2(f6(a2),f5(a1),f5(a1))),
% 65.52/65.59 inference(scs_inference,[],[4,21,83,1483])).
% 65.52/65.59 cnf(3704,plain,
% 65.52/65.59 (P2(f6(a2),f3(a1,a1),f3(a1,a1))),
% 65.52/65.59 inference(scs_inference,[],[4,21,83,1483,1944])).
% 65.52/65.59 cnf(3707,plain,
% 65.52/65.59 (P2(f5(a4),f6(a2),f5(a4))),
% 65.52/65.59 inference(scs_inference,[],[3700,21])).
% 65.52/65.59 cnf(3709,plain,
% 65.52/65.59 (~P2(f6(a2),f6(a2),a2)),
% 65.52/65.59 inference(scs_inference,[],[174,3700,21,25])).
% 65.52/65.59 cnf(3712,plain,
% 65.52/65.59 (P2(f5(a1),f6(a2),f5(a1))),
% 65.52/65.59 inference(scs_inference,[],[3702,21])).
% 65.52/65.59 cnf(3716,plain,
% 65.52/65.59 (P2(f7(a1,a1),a1,f7(a1,a1))),
% 65.52/65.59 inference(scs_inference,[],[2249,21])).
% 65.52/65.59 cnf(3718,plain,
% 65.52/65.59 (~P2(f5(a1),x37181,a2)+~P2(x37181,f5(a1),f6(a2))),
% 65.52/65.59 inference(scs_inference,[],[1629,3712,2249,21,25])).
% 65.52/65.59 cnf(3722,plain,
% 65.52/65.59 (P2(f5(a4),a1,f5(a4))),
% 65.52/65.59 inference(scs_inference,[],[82,21])).
% 65.52/65.59 cnf(3734,plain,
% 65.52/65.59 (P2(f6(a2),a1,f6(a2))),
% 65.52/65.59 inference(scs_inference,[],[2330,21])).
% 65.52/65.59 cnf(3736,plain,
% 65.60/65.59 (~P2(f6(a2),f6(a2),a4)),
% 65.60/65.59 inference(scs_inference,[],[2330,21,635])).
% 65.60/65.59 cnf(3757,plain,
% 65.60/65.59 (P2(f5(a1),a1,f5(a1))),
% 65.60/65.59 inference(scs_inference,[],[1479,21])).
% 65.60/65.59 cnf(3793,plain,
% 65.60/65.59 (P4(a4,a1,a1)),
% 65.60/65.59 inference(scs_inference,[],[2,3676,13])).
% 65.60/65.59 cnf(3794,plain,
% 65.60/65.59 (~P4(x37941,a1,a2)+~P2(a4,x37941,a4)),
% 65.60/65.59 inference(scs_inference,[],[6,3793,28])).
% 65.60/65.59 cnf(3817,plain,
% 65.60/65.59 (~P2(x38171,a4,a4)+~P4(x38171,a1,a2)),
% 65.60/65.59 inference(scs_inference,[],[3794,21])).
% 65.60/65.59 cnf(3821,plain,
% 65.60/65.59 (P4(f5(a1),a4,f5(a1))),
% 65.60/65.59 inference(scs_inference,[],[1662,22])).
% 65.60/65.59 cnf(3979,plain,
% 65.60/65.59 (P4(f5(a4),f7(a4,a4),f5(a4))),
% 65.60/65.59 inference(scs_inference,[],[2,3662,17])).
% 65.60/65.59 cnf(3980,plain,
% 65.60/65.59 (P4(f7(a4,a4),f5(a4),f5(a4))),
% 65.60/65.59 inference(scs_inference,[],[3979,22])).
% 65.60/65.59 cnf(3982,plain,
% 65.60/65.59 (~P4(f6(a2),f7(a4,a4),a2)),
% 65.60/65.59 inference(scs_inference,[],[3707,172,3979,22,28])).
% 65.60/65.59 cnf(4378,plain,
% 65.60/65.59 (~P2(f5(a1),x43781,f6(a2))+~P2(f5(a1),x43781,a2)),
% 65.60/65.59 inference(scs_inference,[],[3718,21])).
% 65.60/65.59 cnf(4433,plain,
% 65.60/65.59 (P2(f6(a2),f7(a1,a1),f7(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[3698,2249,24])).
% 65.60/65.59 cnf(4435,plain,
% 65.60/65.59 (P2(f7(a1,a1),f6(a2),f7(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[3698,2249,24,21])).
% 65.60/65.59 cnf(4546,plain,
% 65.60/65.59 (~P2(f5(a1),f6(a2),f6(a2))+~P2(f5(a1),a1,a2)),
% 65.60/65.59 inference(scs_inference,[],[4,3757,4378,24])).
% 65.60/65.59 cnf(4570,plain,
% 65.60/65.59 (~P4(a1,f7(a4,a4),a2)),
% 65.60/65.59 inference(scs_inference,[],[3722,172,3979,28])).
% 65.60/65.59 cnf(4786,plain,
% 65.60/65.59 (P3(f6(a2),f6(a2))),
% 65.60/65.59 inference(scs_inference,[],[2330,34,23])).
% 65.60/65.59 cnf(5286,plain,
% 65.60/65.59 (~P2(a1,f5(a1),a2)+~P2(f5(a1),f6(a2),f6(a2))),
% 65.60/65.59 inference(scs_inference,[],[4546,21])).
% 65.60/65.59 cnf(5806,plain,
% 65.60/65.59 (~P4(f5(a1),a4,a2)+~P2(f5(a1),f6(a2),f6(a2))),
% 65.60/65.59 inference(scs_inference,[],[2521,3821,1479,5286,28])).
% 65.60/65.59 cnf(5902,plain,
% 65.60/65.59 (~P2(f6(a2),f5(a1),f6(a2))+~P4(f5(a1),a4,a2)),
% 65.60/65.59 inference(scs_inference,[],[5806,21])).
% 65.60/65.59 cnf(5918,plain,
% 65.60/65.59 (~P2(a1,f5(a1),a1)+~P4(f5(a1),a4,a2)),
% 65.60/65.59 inference(scs_inference,[],[3734,5902,25])).
% 65.60/65.59 cnf(5934,plain,
% 65.60/65.59 (~P2(f5(a1),a1,a1)+~P4(f5(a1),a4,a2)),
% 65.60/65.59 inference(scs_inference,[],[5918,21])).
% 65.60/65.59 cnf(5950,plain,
% 65.60/65.59 (~P4(f5(a1),a4,a2)),
% 65.60/65.59 inference(scs_inference,[],[1,5934,14])).
% 65.60/65.59 cnf(6384,plain,
% 65.60/65.59 (~P2(a1,f6(a2),f3(a1,a1))+~P2(f3(a1,a1),a1,a4)),
% 65.60/65.59 inference(scs_inference,[],[3634,21])).
% 65.60/65.59 cnf(7394,plain,
% 65.60/65.59 (~P2(a1,a1,f3(a1,a1))+~P2(f3(a1,a1),a1,a4)),
% 65.60/65.59 inference(scs_inference,[],[3734,4,6384,24])).
% 65.60/65.59 cnf(7410,plain,
% 65.60/65.59 (~P2(a1,f3(a1,a1),a4)+~P2(a1,a1,f3(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[7394,21])).
% 65.60/65.59 cnf(7426,plain,
% 65.60/65.59 (~P2(a1,f3(a1,a1),a4)),
% 65.60/65.59 inference(scs_inference,[],[1,7410,16])).
% 65.60/65.59 cnf(7429,plain,
% 65.60/65.59 (~P2(f6(a2),f3(a1,a1),a4)),
% 65.60/65.59 inference(scs_inference,[],[7426,2150,3704,1940,24,25])).
% 65.60/65.59 cnf(7439,plain,
% 65.60/65.59 (~P2(a1,a1,x74391)+~P2(x74391,f3(a1,a1),a4)),
% 65.60/65.59 inference(scs_inference,[],[7426,1940,24])).
% 65.60/65.59 cnf(7456,plain,
% 65.60/65.59 (P2(f5(a4),a4,a1)),
% 65.60/65.59 inference(scs_inference,[],[2,7,14])).
% 65.60/65.59 cnf(7460,plain,
% 65.60/65.59 (P4(a4,a4,a4)),
% 65.60/65.59 inference(scs_inference,[],[4570,2,7,14,22,13])).
% 65.60/65.59 cnf(7462,plain,
% 65.60/65.59 (P2(a1,a4,a4)),
% 65.60/65.59 inference(scs_inference,[],[4570,2,7,14,22,13,12])).
% 65.60/65.59 cnf(7464,plain,
% 65.60/65.59 (P1(f3(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[4570,2,7,14,22,13,12,9])).
% 65.60/65.59 cnf(7466,plain,
% 65.60/65.59 (P1(f7(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[4570,2,7,14,22,13,12,9,10])).
% 65.60/65.59 cnf(7468,plain,
% 65.60/65.59 (P1(f6(a2))),
% 65.60/65.59 inference(scs_inference,[],[4570,2,3,6,7,14,22,13,12,9,10,15])).
% 65.60/65.59 cnf(7470,plain,
% 65.60/65.59 (P2(a4,a4,f3(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[4570,2,3,6,7,14,22,13,12,9,10,15,16])).
% 65.60/65.59 cnf(7472,plain,
% 65.60/65.59 (P4(f6(a2),a2,a4)),
% 65.60/65.59 inference(scs_inference,[],[4570,2,3,6,7,14,22,13,12,9,10,15,16,19])).
% 65.60/65.59 cnf(7474,plain,
% 65.60/65.59 (P4(a4,a4,f7(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[4570,2,3,6,7,14,22,13,12,9,10,15,16,19,17])).
% 65.60/65.59 cnf(7476,plain,
% 65.60/65.59 (P2(a1,a1,a1)),
% 65.60/65.59 inference(scs_inference,[],[4570,2,3,34,6,7,14,22,13,12,9,10,15,16,19,17,18])).
% 65.60/65.59 cnf(7480,plain,
% 65.60/65.59 (P2(a1,f3(a4,a4),f3(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[4570,2,3,34,43,6,7,14,22,13,12,9,10,15,16,19,17,18,23,24])).
% 65.60/65.59 cnf(7484,plain,
% 65.60/65.59 (P4(f7(a4,a4),a4,f7(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[4570,2,3,34,43,6,7,14,22,13,12,9,10,15,16,19,17,18,23,24,8,27])).
% 65.60/65.59 cnf(7486,plain,
% 65.60/65.59 (~P2(a1,f5(a1),a2)),
% 65.60/65.59 inference(scs_inference,[],[5950,1479,4570,3821,2,3,34,2521,43,6,7,14,22,13,12,9,10,15,16,19,17,18,23,24,8,27,29])).
% 65.60/65.59 cnf(7488,plain,
% 65.60/65.59 (P2(f5(a4),f7(a4,a4),a1)),
% 65.60/65.59 inference(scs_inference,[],[5950,1479,4570,3821,2,3,34,2521,1134,43,6,7,14,22,13,12,9,10,15,16,19,17,18,23,24,8,27,29,28])).
% 65.60/65.59 cnf(7490,plain,
% 65.60/65.59 (~P4(a1,a1,a2)),
% 65.60/65.59 inference(scs_inference,[],[5950,1479,4570,3821,2,3,34,2521,1134,43,6,7,14,22,13,12,9,10,15,16,19,17,18,23,24,8,27,29,28,3817])).
% 65.60/65.59 cnf(7492,plain,
% 65.60/65.59 (~P2(f5(a1),a1,a2)),
% 65.60/65.59 inference(scs_inference,[],[5950,1479,4570,3821,2,3,34,2521,1134,43,6,7,14,22,13,12,9,10,15,16,19,17,18,23,24,8,27,29,28,3817,21])).
% 65.60/65.59 cnf(7494,plain,
% 65.60/65.59 (P4(a1,f7(a4,a4),a1)),
% 65.60/65.59 inference(scs_inference,[],[5950,1479,4570,3821,2,3,34,2521,1134,43,6,7,14,22,13,12,9,10,15,16,19,17,18,23,24,8,27,29,28,3817,21,3665])).
% 65.60/65.59 cnf(7498,plain,
% 65.60/65.59 (P4(a4,f7(a4,a4),f7(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[5950,1479,4570,3821,2,3,34,2521,1134,43,6,7,14,22,13,12,9,10,15,16,19,17,18,23,24,8,27,29,28,3817,21,3665,2992,26])).
% 65.60/65.59 cnf(7511,plain,
% 65.60/65.59 (P2(f5(a2),a2,a1)),
% 65.60/65.59 inference(scs_inference,[],[3,3982,22,14])).
% 65.60/65.59 cnf(7513,plain,
% 65.60/65.59 (P1(f5(a2))),
% 65.60/65.59 inference(scs_inference,[],[3,3982,22,14,7])).
% 65.60/65.59 cnf(7515,plain,
% 65.60/65.59 (P4(a4,f3(a4,a4),f3(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[7464,3,3982,22,14,7,13])).
% 65.60/65.59 cnf(7517,plain,
% 65.60/65.59 (P2(a1,f7(a4,a4),f7(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[7464,7466,3,3982,22,14,7,13,12])).
% 65.60/65.59 cnf(7519,plain,
% 65.60/65.59 (P1(f7(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7464,7466,3,3982,22,14,7,13,12,10])).
% 65.60/65.59 cnf(7521,plain,
% 65.60/65.59 (P1(f3(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7464,7466,3,3982,22,14,7,13,12,10,9])).
% 65.60/65.59 cnf(7523,plain,
% 65.60/65.59 (P2(a2,a2,f3(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7464,7466,3,3982,22,14,7,13,12,10,9,16])).
% 65.60/65.59 cnf(7525,plain,
% 65.60/65.59 (P4(a2,a2,f7(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7464,7466,3,3982,22,14,7,13,12,10,9,16,17])).
% 65.60/65.59 cnf(7527,plain,
% 65.60/65.59 (P2(a1,a2,a2)),
% 65.60/65.59 inference(scs_inference,[],[7464,7466,3,50,3982,22,14,7,13,12,10,9,16,17,18])).
% 65.60/65.59 cnf(7529,plain,
% 65.60/65.59 (~P2(f6(a2),a4,f3(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[4,7462,7464,7466,7426,3,50,3982,22,14,7,13,12,10,9,16,17,18,24])).
% 65.60/65.59 cnf(7531,plain,
% 65.60/65.59 (~P2(f5(a2),a1,a1)),
% 65.60/65.59 inference(scs_inference,[],[4,7462,7464,7466,7426,3,50,6,3982,22,14,7,13,12,10,9,16,17,18,24,25])).
% 65.60/65.59 cnf(7533,plain,
% 65.60/65.59 (~P2(f5(a4),f7(a4,a4),a2)),
% 65.60/65.59 inference(scs_inference,[],[4,7462,7464,7456,7466,7498,7426,4570,3979,3,50,6,3982,22,14,7,13,12,10,9,16,17,18,24,25,29])).
% 65.60/65.59 cnf(7535,plain,
% 65.60/65.59 (~P4(a1,f7(a4,a4),a4)),
% 65.60/65.59 inference(scs_inference,[],[4,7476,7462,7494,7464,7456,7466,7498,7426,5,4570,3979,3,50,6,3982,22,14,7,13,12,10,9,16,17,18,24,25,29,28])).
% 65.60/65.59 cnf(7537,plain,
% 65.60/65.59 (~P2(a4,f6(a2),f3(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[4,7476,7462,7494,7464,7456,7466,7498,7426,5,4570,3979,3,50,6,3982,22,14,7,13,12,10,9,16,17,18,24,25,29,28,21])).
% 65.60/65.59 cnf(7541,plain,
% 65.60/65.59 (P3(f3(a2,a2),f3(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[4,7476,7462,7494,7464,7456,7466,7470,7498,7426,5,4570,3979,3,50,6,3982,22,14,7,13,12,10,9,16,17,18,24,25,29,28,21,2942,23])).
% 65.60/65.59 cnf(7547,plain,
% 65.60/65.59 (P2(f5(a1),a1,a1)),
% 65.60/65.59 inference(scs_inference,[],[1,7,14])).
% 65.60/65.59 cnf(7553,plain,
% 65.60/65.59 (P4(a4,f6(a2),f6(a2))),
% 65.60/65.59 inference(scs_inference,[],[7468,7533,7535,1,7,14,22,21,13])).
% 65.60/65.59 cnf(7555,plain,
% 65.60/65.59 (P2(a1,f5(a2),f5(a2))),
% 65.60/65.59 inference(scs_inference,[],[7468,7513,7533,7535,1,7,14,22,21,13,12])).
% 65.60/65.59 cnf(7557,plain,
% 65.60/65.59 (P1(f3(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[7468,7513,7533,7535,1,7,14,22,21,13,12,9])).
% 65.60/65.59 cnf(7561,plain,
% 65.60/65.59 (P2(a1,a1,f3(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[7468,7513,7533,7535,1,7,14,22,21,13,12,9,10,16])).
% 65.60/65.59 cnf(7563,plain,
% 65.60/65.59 (P4(a1,a1,f7(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[7468,7513,7533,7535,1,7,14,22,21,13,12,9,10,16,17])).
% 65.60/65.59 cnf(7565,plain,
% 65.60/65.59 (P2(a1,f3(a2,a2),f3(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7541,7468,7513,7533,7535,1,7,14,22,21,13,12,9,10,16,17,18])).
% 65.60/65.59 cnf(7567,plain,
% 65.60/65.59 (~P2(a2,f6(a2),a1)),
% 65.60/65.59 inference(scs_inference,[],[4,7541,7468,7513,7533,7535,7511,7531,1,7,14,22,21,13,12,9,10,16,17,18,24])).
% 65.60/65.59 cnf(7569,plain,
% 65.60/65.59 (~P2(f6(a2),f5(a2),f6(a2))),
% 65.60/65.59 inference(scs_inference,[],[4,7541,7468,7513,7533,7535,7511,7531,32,1,3734,7,14,22,21,13,12,9,10,16,17,18,24,25])).
% 65.60/65.59 cnf(7571,plain,
% 65.60/65.59 (P4(a4,f7(a1,a1),f7(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[4,7541,7468,7513,7533,7535,7511,7531,32,1,3734,3793,7,14,22,21,13,12,9,10,16,17,18,24,25,26])).
% 65.60/65.59 cnf(7573,plain,
% 65.60/65.59 (P4(f6(a2),a2,f7(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[4,7472,7541,7468,7513,7533,7535,7511,7531,7474,32,1,3734,3793,7,14,22,21,13,12,9,10,16,17,18,24,25,26,27])).
% 65.60/65.59 cnf(7575,plain,
% 65.60/65.59 (P4(f3(a4,a4),a4,f3(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[4,7472,7541,7468,7513,7533,7535,7511,7531,7474,7460,7470,32,1,3734,3793,7,14,22,21,13,12,9,10,16,17,18,24,25,26,27,29])).
% 65.60/65.59 cnf(7577,plain,
% 65.60/65.59 (P2(f7(a4,a4),f7(a4,a4),f3(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[4,7472,7541,7468,7513,7533,7535,7511,7531,7474,7460,7470,32,1,3734,3793,7,14,22,21,13,12,9,10,16,17,18,24,25,26,27,29,28])).
% 65.60/65.59 cnf(7579,plain,
% 65.60/65.59 (P2(f5(a4),f5(a4),f5(a4))+~P4(a4,a4,a1)),
% 65.60/65.59 inference(scs_inference,[],[4,7472,7541,7468,7513,7533,7535,7511,7531,7474,7460,7470,32,7462,1,3734,3793,7,14,22,21,13,12,9,10,16,17,18,24,25,26,27,29,28,2818])).
% 65.60/65.59 cnf(7581,plain,
% 65.60/65.59 (P3(a1,f7(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[4,7472,7541,7468,7513,7533,7535,7511,7531,7474,7460,7470,32,7462,1,34,3734,3793,7,14,22,21,13,12,9,10,16,17,18,24,25,26,27,29,28,2818,20])).
% 65.60/65.59 cnf(7588,plain,
% 65.60/65.59 (~P2(f5(a2),f6(a2),f6(a2))),
% 65.60/65.59 inference(scs_inference,[],[7569,21])).
% 65.60/65.59 cnf(7590,plain,
% 65.60/65.59 (P4(a4,f3(a1,a1),f3(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[7557,7569,21,13])).
% 65.60/65.59 cnf(7592,plain,
% 65.60/65.59 (P2(a1,f7(a2,a2),f7(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7557,7519,7569,21,13,12])).
% 65.60/65.59 cnf(7594,plain,
% 65.60/65.59 (~P2(f6(a2),a2,f5(a1))),
% 65.60/65.59 inference(scs_inference,[],[4,7527,7486,7557,7519,7569,21,13,12,24])).
% 65.60/65.59 cnf(7596,plain,
% 65.60/65.59 (~P2(f6(a2),f5(a1),a2)),
% 65.60/65.59 inference(scs_inference,[],[4,7527,7486,7557,7519,7569,21,13,12,24,25])).
% 65.60/65.59 cnf(7598,plain,
% 65.60/65.59 (P4(f7(a1,a1),f7(a4,a4),f7(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[4,7527,7486,7557,7519,7569,7563,7494,21,13,12,24,25,27])).
% 65.60/65.59 cnf(7600,plain,
% 65.60/65.59 (~P2(f5(a4),f7(a4,a4),a4)),
% 65.60/65.59 inference(scs_inference,[],[4,7527,7486,7557,7519,7569,7563,7535,7456,7498,7494,3979,21,13,12,24,25,27,29])).
% 65.60/65.59 cnf(7606,plain,
% 65.60/65.59 (P2(a1,a4,a1)+P1(f6(a4))),
% 65.60/65.59 inference(scs_inference,[],[4,7527,7486,7557,7519,7569,7561,7563,7535,7456,7498,7494,5,3979,2,21,13,12,24,25,27,29,28,22,15])).
% 65.60/65.59 cnf(7610,plain,
% 65.60/65.59 (~P2(f7(a4,a4),f5(a4),a4)),
% 65.60/65.59 inference(scs_inference,[],[7600,21])).
% 65.60/65.59 cnf(7612,plain,
% 65.60/65.59 (P4(a4,f3(a2,a2),f3(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7521,7600,21,13])).
% 65.60/65.59 cnf(7614,plain,
% 65.60/65.59 (~P2(f5(a2),a2,a2)),
% 65.60/65.59 inference(scs_inference,[],[7521,7600,7555,7511,6,21,13,24])).
% 65.60/65.59 cnf(7616,plain,
% 65.60/65.59 (~P2(a1,f6(a2),f5(a2))),
% 65.60/65.59 inference(scs_inference,[],[4,7521,7600,7555,7531,7511,3734,6,21,13,24,25])).
% 65.60/65.59 cnf(7618,plain,
% 65.60/65.59 (~P2(f7(a1,a1),f7(a1,a1),a2)),
% 65.60/65.59 inference(scs_inference,[],[4,7490,7521,7600,7555,7563,7531,7476,7511,3734,6,21,13,24,25,29])).
% 65.60/65.59 cnf(7628,plain,
% 65.60/65.59 (~P2(a2,f6(a2),f5(a1))),
% 65.60/65.59 inference(scs_inference,[],[7594,21])).
% 65.60/65.59 cnf(7630,plain,
% 65.60/65.59 (P4(a4,f5(a2),f5(a2))),
% 65.60/65.59 inference(scs_inference,[],[7594,7513,21,13])).
% 65.60/65.59 cnf(7632,plain,
% 65.60/65.59 (~P2(a1,a4,f3(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[7429,7594,7513,7462,3698,21,13,24])).
% 65.60/65.59 cnf(7634,plain,
% 65.60/65.59 (~P2(f6(a2),a1,f5(a2))),
% 65.60/65.59 inference(scs_inference,[],[4,7429,7588,7594,7513,7462,3698,3734,21,13,24,25])).
% 65.60/65.59 cnf(7640,plain,
% 65.60/65.59 (~P3(f7(a1,a1),a1)+P2(a1,f7(a1,a1),a1)),
% 65.60/65.59 inference(scs_inference,[],[4,7429,7581,7571,7618,7588,7594,7513,7462,7470,3698,3734,21,13,24,25,28,22,18])).
% 65.60/65.59 cnf(7642,plain,
% 65.60/65.59 (~P2(f7(a1,a1),f7(a1,a1),a1)+P2(a1,f7(a1,a1),a1)),
% 65.60/65.59 inference(scs_inference,[],[4,7429,7581,7571,7618,7588,7594,7513,7462,7470,3698,2249,3734,21,13,24,25,28,22,18,23])).
% 65.60/65.59 cnf(7647,plain,
% 65.60/65.59 (~P2(f6(a2),a2,a1)),
% 65.60/65.59 inference(scs_inference,[],[7567,21])).
% 65.60/65.59 cnf(7649,plain,
% 65.60/65.59 (P4(a4,f7(a2,a2),f7(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7567,7519,21,13])).
% 65.60/65.59 cnf(7651,plain,
% 65.60/65.59 (~P2(a2,a2,a2)),
% 65.60/65.59 inference(scs_inference,[],[7567,7614,7519,7527,7511,21,13,24])).
% 65.60/65.59 cnf(7653,plain,
% 65.60/65.59 (~P2(a1,f5(a4),f6(a2))),
% 65.60/65.59 inference(scs_inference,[],[7529,7567,7614,7519,7527,7561,7456,7511,21,13,24,25])).
% 65.60/65.59 cnf(7655,plain,
% 65.60/65.59 (P4(f7(a1,a1),a4,f7(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[7529,7567,7614,7519,7527,7598,7561,7456,7484,7511,21,13,24,25,27])).
% 65.60/65.59 cnf(7663,plain,
% 65.60/65.59 (~P2(f5(a1),a1,f7(a1,a1))+P2(a1,a1,f7(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[7547,7529,7567,7614,7519,7527,7598,7581,7561,7531,7456,7484,7511,1515,7494,21,13,24,25,27,28,22,18,23])).
% 65.60/65.59 cnf(7666,plain,
% 65.60/65.59 (~P2(f5(a4),a1,f6(a2))),
% 65.60/65.59 inference(scs_inference,[],[7653,21])).
% 65.60/65.59 cnf(7668,plain,
% 65.60/65.59 (P4(a4,a2,a2)),
% 65.60/65.59 inference(scs_inference,[],[7653,3,21,13])).
% 65.60/65.59 cnf(7670,plain,
% 65.60/65.59 (~P2(a1,a1,f5(a2))),
% 65.60/65.59 inference(scs_inference,[],[7653,7569,3,3734,21,13,24])).
% 65.60/65.59 cnf(7672,plain,
% 65.60/65.59 (P3(f7(a2,a2),f7(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7653,7592,7569,3,34,3734,21,13,24,23])).
% 65.60/65.59 cnf(7674,plain,
% 65.60/65.59 (~P2(f5(a1),f5(a1),f5(a2))),
% 65.60/65.59 inference(scs_inference,[],[7653,7592,7569,7547,7531,3,34,3734,21,13,24,23,25])).
% 65.60/65.59 cnf(7676,plain,
% 65.60/65.59 (P4(f3(a4,a4),a2,f3(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7653,7592,7523,7569,7547,7531,7470,3,34,3734,21,13,24,23,25,29])).
% 65.60/65.59 cnf(7684,plain,
% 65.60/65.59 (P4(f6(a2),f7(a2,a2),a2)),
% 65.60/65.59 inference(scs_inference,[],[7653,7592,7523,7525,7569,7472,7547,7531,7581,7470,7494,82,3979,3,34,3734,21,13,24,23,25,29,28,22,20,26])).
% 65.60/65.59 cnf(7686,plain,
% 65.60/65.59 (P4(f7(a4,a4),a2,a2)),
% 65.60/65.59 inference(scs_inference,[],[7653,7592,7523,7525,7573,7569,7472,7547,7531,7581,7470,7494,82,3979,3,34,3734,21,13,24,23,25,29,28,22,20,26,27])).
% 65.60/65.59 cnf(7694,plain,
% 65.60/65.59 (~P2(a1,f3(a2,a2),a2)),
% 65.60/65.59 inference(scs_inference,[],[7651,7537,7596,7523,7527,7561,3734,21,24,25])).
% 65.60/65.59 cnf(7696,plain,
% 65.60/65.59 (P4(f7(a4,a4),f7(a2,a2),f7(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[7651,7537,7596,7686,7523,7525,7527,7561,3734,21,24,25,26])).
% 65.60/65.59 cnf(7700,plain,
% 65.60/65.59 (~P4(a2,f3(a4,a4),a2)),
% 65.60/65.59 inference(scs_inference,[],[7651,7577,7537,7596,7686,7523,7525,7527,7561,3734,21,24,25,26,28,22])).
% 65.60/65.59 cnf(7702,plain,
% 65.60/65.59 (P3(f5(a2),f5(a2))),
% 65.60/65.59 inference(scs_inference,[],[7651,7577,7537,7596,7686,7523,7525,7513,7527,7561,3734,21,24,25,26,28,22,8])).
% 65.60/65.59 cnf(7704,plain,
% 65.60/65.59 (~P4(f7(a4,a4),f7(a4,a4),f3(a4,a4))),
% 65.60/65.59 inference(scs_inference,[],[7651,7577,7537,7596,7686,7523,7525,7513,7527,7561,3734,21,24,25,26,28,22,8,27])).
% 65.60/65.59 cnf(7708,plain,
% 65.60/65.59 (~P2(a4,a1,f3(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[7632,21])).
% 65.60/65.59 cnf(7710,plain,
% 65.60/65.59 (~P2(a1,f5(a2),f5(a1))),
% 65.60/65.59 inference(scs_inference,[],[7674,7632,7555,7547,21,24])).
% 65.60/65.59 cnf(7712,plain,
% 65.60/65.59 (~P2(f6(a2),f6(a2),f5(a2))),
% 65.60/65.59 inference(scs_inference,[],[4,7616,7674,7632,7555,7547,21,24,25])).
% 65.60/65.59 cnf(7714,plain,
% 65.60/65.59 (~P2(f5(a4),a4,a2)),
% 65.60/65.59 inference(scs_inference,[],[4,7616,7674,7632,7555,7460,7547,7456,2974,1134,21,24,25,29])).
% 65.60/65.59 cnf(7723,plain,
% 65.60/65.59 (P2(a4,a1,a1)+P1(f6(a4))),
% 65.60/65.59 inference(scs_inference,[],[7606,21])).
% 65.60/65.59 cnf(7724,plain,
% 65.60/65.59 (~P2(f3(a1,a1),f3(a1,a1),a4)),
% 65.60/65.59 inference(scs_inference,[],[7561,7439])).
% 65.60/65.59 cnf(7726,plain,
% 65.60/65.59 (~P2(f3(a2,a2),a1,a2)),
% 65.60/65.59 inference(scs_inference,[],[7694,7561,7439,21])).
% 65.60/65.59 cnf(7728,plain,
% 65.60/65.59 (~P2(f5(a2),a1,f6(a2))),
% 65.60/65.59 inference(scs_inference,[],[7694,7647,7527,7511,7561,7439,21,25])).
% 65.60/65.59 cnf(7730,plain,
% 65.60/65.59 (P4(f7(a4,a4),f3(a1,a1),f3(a1,a1))),
% 65.60/65.59 inference(scs_inference,[],[7590,7694,7647,7474,7527,7511,7561,7439,21,25,27])).
% 65.60/65.59 cnf(7732,plain,
% 65.60/65.59 (~P2(f7(a1,a1),a1,a2)),
% 65.60/65.59 inference(scs_inference,[],[7590,7694,7647,7474,7527,7511,7561,7462,7563,2975,3793,7439,21,25,27,29])).
% 65.60/65.59 cnf(7734,plain,
% 65.60/65.59 (~P4(a1,f7(a4,a4),f5(a2))),
% 65.60/65.59 inference(scs_inference,[],[7590,7694,7647,7670,7476,7474,7527,7511,7561,7462,7563,2975,7494,3793,7439,21,25,27,29,28])).
% 65.60/65.59 cnf(7738,plain,
% 65.60/65.59 (~P2(f6(a2),f3(a2,a2),x77381)+P2(a1,x77381,f3(a2,a2))),
% 65.60/65.59 inference(scs_inference,[],[4,7565,7590,7694,7647,7670,7476,7474,7527,7511,7561,7462,7563,2975,7494,3793,7439,21,25,27,29,28,22,24])).
% 65.60/65.59 cnf(7742,plain,
% 65.60/65.59 (~P2(a1,f7(a1,a1),a2)),
% 65.60/65.59 inference(scs_inference,[],[7732,21])).
% 65.60/65.59 cnf(7744,plain,
% 65.60/65.59 (~P2(f6(a2),f5(a1),f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7732,7710,1479,21,24])).
% 65.60/65.60 cnf(7746,plain,
% 65.60/65.60 (~P2(f5(a1),f5(a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7732,7710,7594,7511,1479,3757,21,24,25])).
% 65.60/65.60 cnf(7750,plain,
% 65.60/65.60 (~P2(a4,a4,f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7704,7700,7732,7710,7684,7577,7594,7498,7511,1479,3757,21,24,25,27,29])).
% 65.60/65.60 cnf(7752,plain,
% 65.60/65.60 (~P4(a1,a4,f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7704,7700,7732,7710,7684,7577,7594,7670,7476,7498,7511,1479,3757,2521,21,24,25,27,29,28])).
% 65.60/65.60 cnf(7754,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f7(a2,a2),f7(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7704,7700,7732,7710,7684,7577,7594,7670,7476,7498,7511,1479,3757,2521,21,24,25,27,29,28,22])).
% 65.60/65.60 cnf(7756,plain,
% 65.60/65.60 (~P2(f7(a2,a2),x77561,x77562)+~P2(f7(a2,a2),x77561,x77563)+P3(x77562,x77563)),
% 65.60/65.60 inference(scs_inference,[],[4,7704,7700,7732,7710,7684,7672,7577,7594,7670,7476,7498,7511,1479,3757,2521,21,24,25,27,29,28,22,23])).
% 65.60/65.60 cnf(7757,plain,
% 65.60/65.60 (~P4(a4,a1,f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[7752,22])).
% 65.60/65.60 cnf(7761,plain,
% 65.60/65.60 (~P2(a1,f5(a2),a1)),
% 65.60/65.60 inference(scs_inference,[],[7634,7744,7752,7555,3698,22,21,24])).
% 65.60/65.60 cnf(7763,plain,
% 65.60/65.60 (~P2(f5(a1),f5(a2),a1)),
% 65.60/65.60 inference(scs_inference,[],[7634,7744,7746,7752,7555,3702,3698,3734,22,21,24,25])).
% 65.60/65.60 cnf(7765,plain,
% 65.60/65.60 (~P2(f7(a2,a2),f7(a2,a2),f7(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[7649,7754,7634,7744,7746,7752,7555,7470,3702,3698,3734,22,21,24,25,29])).
% 65.60/65.60 cnf(7767,plain,
% 65.60/65.60 (~P4(f3(a2,a2),a2,f7(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[7649,7754,7634,7744,7746,7752,7523,7555,7525,7470,3702,3698,3734,22,21,24,25,29,28])).
% 65.60/65.60 cnf(7781,plain,
% 65.60/65.60 (~P2(a1,f5(a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[7767,7728,22,21])).
% 65.60/65.60 cnf(7783,plain,
% 65.60/65.60 (~P2(f6(a2),a2,f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[4,7767,7728,7742,7527,22,21,24])).
% 65.60/65.60 cnf(7785,plain,
% 65.60/65.60 (~P2(a1,a1,f7(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7765,7767,7728,7742,7592,7527,22,21,24,25])).
% 65.60/65.60 cnf(7787,plain,
% 65.60/65.60 (~P2(f5(a4),a4,f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7765,7767,7728,7742,7592,7752,7460,7456,7527,1134,22,21,24,25,29])).
% 65.60/65.60 cnf(7789,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f3(a1,a1),a4)),
% 65.60/65.60 inference(scs_inference,[],[4,7730,7765,7724,7767,7728,7742,7592,7752,7577,7460,7456,7527,1134,22,21,24,25,29,28])).
% 65.60/65.60 cnf(7794,plain,
% 65.60/65.60 (~P4(f3(a1,a1),f3(a4,a4),a4)),
% 65.60/65.60 inference(scs_inference,[],[7789,22])).
% 65.60/65.60 cnf(7796,plain,
% 65.60/65.60 (~P2(a2,f6(a2),f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[7789,7783,22,21])).
% 65.60/65.60 cnf(7798,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f5(a2),a4)),
% 65.60/65.60 inference(scs_inference,[],[7789,7783,7787,7488,7555,22,21,24])).
% 65.60/65.60 cnf(7800,plain,
% 65.60/65.60 (~P2(f5(a1),f3(a2,a2),a2)),
% 65.60/65.60 inference(scs_inference,[],[7789,7783,7787,7565,7694,7488,7555,7547,22,21,24,25])).
% 65.60/65.60 cnf(7802,plain,
% 65.60/65.60 (P4(f7(a4,a4),f3(a2,a2),f3(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[7612,7789,7783,7787,7565,7694,7488,7555,7547,7474,22,21,24,25,27])).
% 65.60/65.60 cnf(7804,plain,
% 65.60/65.60 (~P2(f5(a1),a1,f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[7612,7789,7783,7787,7565,7694,7488,7752,7555,7547,7474,3821,2521,22,21,24,25,27,29])).
% 65.60/65.60 cnf(7806,plain,
% 65.60/65.60 (~P4(a1,f7(a2,a2),f7(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[7612,7789,7783,7787,7517,7565,7765,7694,7696,7488,7752,7555,7547,7474,3821,2521,22,21,24,25,27,29,28])).
% 65.60/65.60 cnf(7812,plain,
% 65.60/65.60 (~P4(f7(a2,a2),a1,f7(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[7806,22])).
% 65.60/65.60 cnf(7814,plain,
% 65.60/65.60 (~P2(f5(a2),f7(a4,a4),a4)),
% 65.60/65.60 inference(scs_inference,[],[7806,7798,22,21])).
% 65.60/65.60 cnf(7818,plain,
% 65.60/65.60 (~P2(f6(a2),a1,f7(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7628,7806,7798,7785,7592,3712,2330,22,21,24,25])).
% 65.60/65.60 cnf(7820,plain,
% 65.60/65.60 (~P4(a1,a2,f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7628,7806,7798,7785,7614,7517,7592,7686,3712,2330,22,21,24,25,28])).
% 65.60/65.60 cnf(7829,plain,
% 65.60/65.60 (~P2(f6(a2),f7(a2,a2),a1)),
% 65.60/65.60 inference(scs_inference,[],[4,7800,7820,7785,7592,22,21,24])).
% 65.60/65.60 cnf(7831,plain,
% 65.60/65.60 (~P2(f6(a2),f7(a1,a1),a2)),
% 65.60/65.60 inference(scs_inference,[],[4,7800,7796,7820,4435,7785,7592,4433,22,21,24,25])).
% 65.60/65.60 cnf(7838,plain,
% 65.60/65.60 (~P2(f7(a4,a4),a2,a4)),
% 65.60/65.60 inference(scs_inference,[],[7831,7714,7488,7527,21,24])).
% 65.60/65.60 cnf(7840,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f5(a2),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[7831,7761,7714,7488,7527,21,24,25])).
% 65.60/65.60 cnf(7844,plain,
% 65.60/65.60 (~P4(f3(a4,a4),a4,f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[7831,7750,7761,7714,7767,7668,7488,7460,7527,7525,7470,21,24,25,27,28])).
% 65.60/65.60 cnf(7846,plain,
% 65.60/65.60 (~P4(a4,a2,f3(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[7831,7750,7761,7714,7767,7668,7488,7460,7527,7525,7470,21,24,25,27,28,22])).
% 65.60/65.60 cnf(7852,plain,
% 65.60/65.60 (~P2(f5(a2),f7(a4,a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[7840,21])).
% 65.60/65.60 cnf(7854,plain,
% 65.60/65.60 (~P4(a4,f3(a4,a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[7840,7844,21,22])).
% 65.60/65.60 cnf(7856,plain,
% 65.60/65.60 (~P2(f3(a2,a2),f5(a2),a1)),
% 65.60/65.60 inference(scs_inference,[],[7840,7726,7844,7511,7527,21,22,24])).
% 65.60/65.60 cnf(7858,plain,
% 65.60/65.60 (~P2(a1,f5(a4),a1)),
% 65.60/65.60 inference(scs_inference,[],[7840,7726,7844,7632,7456,7561,7511,7527,21,22,24,25])).
% 65.60/65.60 cnf(7860,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f7(a4,a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[7840,7726,7844,7632,7577,7484,7456,7561,7511,7527,21,22,24,25,29])).
% 65.60/65.60 cnf(7862,plain,
% 65.60/65.60 (~P4(f6(a2),f7(a4,a4),f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7840,7726,7844,7632,7761,7577,7484,7456,7561,7511,7527,7494,21,22,24,25,29,28])).
% 65.60/65.60 cnf(7869,plain,
% 65.60/65.60 (~P2(a1,f5(a1),f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[7804,21])).
% 65.60/65.60 cnf(7873,plain,
% 65.60/65.60 (~P2(f6(a2),f6(a2),f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7804,7862,7858,21,22,24])).
% 65.60/65.60 cnf(7875,plain,
% 65.60/65.60 (~P2(a1,a1,f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7860,7804,7862,7858,7517,21,22,24,25])).
% 65.60/65.60 cnf(7877,plain,
% 65.60/65.60 (~P4(a2,a1,a2)),
% 65.60/65.60 inference(scs_inference,[],[4,7860,7812,7804,7862,7858,7517,7525,21,22,24,25,27])).
% 65.60/65.60 cnf(7879,plain,
% 65.60/65.60 (P4(f3(a4,a4),f7(a4,a4),f3(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7860,7812,7804,7862,7858,7517,7577,7498,7525,7470,21,22,24,25,27,29])).
% 65.60/65.60 cnf(7881,plain,
% 65.60/65.60 (~P4(f5(a4),f7(a4,a4),a1)),
% 65.60/65.60 inference(scs_inference,[],[4,7860,7812,7804,7862,7858,7517,7577,7498,7525,7470,7494,82,3979,21,22,24,25,27,29,28])).
% 65.60/65.60 cnf(7897,plain,
% 65.60/65.60 (~P2(a1,f6(a2),f7(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[7877,7818,22,21])).
% 65.60/65.60 cnf(7899,plain,
% 65.60/65.60 (~P2(f7(a4,a4),a2,f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[7877,7818,7533,7488,7527,22,21,24])).
% 65.60/65.60 cnf(7901,plain,
% 65.60/65.60 (~P2(f6(a2),f7(a2,a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7877,7818,7829,7533,7488,7527,2330,22,21,24,25])).
% 65.60/65.60 cnf(7903,plain,
% 65.60/65.60 (P4(f7(a4,a4),f5(a2),f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7877,7818,7829,7630,7533,7488,7474,7527,2330,22,21,24,25,27])).
% 65.60/65.60 cnf(7905,plain,
% 65.60/65.60 (~P2(f7(a1,a1),a1,f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7877,7757,7818,7829,7630,7533,7488,7474,7462,7563,7527,2330,3793,22,21,24,25,27,29])).
% 65.60/65.60 cnf(7907,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f6(a2),f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7877,7712,7757,7818,7829,7630,7533,7553,7488,7474,7462,7563,7527,7470,2330,3793,22,21,24,25,27,29,28])).
% 65.60/65.60 cnf(7915,plain,
% 65.60/65.60 (~P4(f6(a2),f3(a4,a4),f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[7763,7907,21,22])).
% 65.60/65.60 cnf(7917,plain,
% 65.60/65.60 (~P2(a2,f7(a4,a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[7852,7763,7907,7517,7511,21,22,24])).
% 65.60/65.60 cnf(7919,plain,
% 65.60/65.60 (~P2(f6(a2),a1,f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[7852,7763,7907,7666,7517,7476,7511,3734,21,22,24,25])).
% 65.60/65.60 cnf(7921,plain,
% 65.60/65.60 (~P4(a1,a4,a4)),
% 65.60/65.60 inference(scs_inference,[],[7852,7763,7907,7600,7666,7517,7476,7484,7488,7511,3734,1134,21,22,24,25,28])).
% 65.60/65.60 cnf(7928,plain,
% 65.60/65.60 (~P4(a4,a1,a4)),
% 65.60/65.60 inference(scs_inference,[],[7921,22])).
% 65.60/65.60 cnf(7930,plain,
% 65.60/65.60 (~P2(a1,f6(a2),f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[7921,7919,22,21])).
% 65.60/65.60 cnf(7932,plain,
% 65.60/65.60 (~P2(f6(a2),f7(a4,a4),a1)),
% 65.60/65.60 inference(scs_inference,[],[4,7921,7875,7919,7517,22,21,24])).
% 65.60/65.60 cnf(7934,plain,
% 65.60/65.60 (~P4(f7(a4,a4),f3(a4,a4),a4)),
% 65.60/65.60 inference(scs_inference,[],[4,7921,7875,7919,7846,7676,7802,7517,22,21,24,27])).
% 65.60/65.60 cnf(7936,plain,
% 65.60/65.60 (~P2(f5(a1),a1,a4)),
% 65.60/65.60 inference(scs_inference,[],[4,7921,7875,7919,7846,7676,7802,7517,7547,3821,2521,22,21,24,27,29])).
% 65.60/65.60 cnf(7938,plain,
% 65.60/65.60 (~P4(a1,f7(a2,a2),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7921,7875,7919,7899,7846,7676,7802,7684,7517,7547,3821,2521,22,21,24,27,29,28])).
% 65.60/65.60 cnf(7942,plain,
% 65.60/65.60 (~P2(a1,f5(a1),a4)),
% 65.60/65.60 inference(scs_inference,[],[7936,21])).
% 65.60/65.60 cnf(7944,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f7(a4,a4),a4)),
% 65.60/65.60 inference(scs_inference,[],[7936,7934,21,22])).
% 65.60/65.60 cnf(7948,plain,
% 65.60/65.60 (~P2(f5(a1),f3(a1,a1),a2)),
% 65.60/65.60 inference(scs_inference,[],[7492,7936,7934,7787,7555,7456,7561,3757,21,22,24,25])).
% 65.60/65.60 cnf(7950,plain,
% 65.60/65.60 (~P2(f7(a1,a1),a1,a4)),
% 65.60/65.60 inference(scs_inference,[],[7928,7492,7936,7934,7787,7555,7456,7561,7563,7462,3757,3793,21,22,24,25,29])).
% 65.60/65.60 cnf(7952,plain,
% 65.60/65.60 (~P4(f5(a1),a4,f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[7928,7492,7936,7869,7934,7787,7555,7456,7561,7563,7462,1479,3757,3821,2521,3793,21,22,24,25,29,28])).
% 65.60/65.60 cnf(7961,plain,
% 65.60/65.60 (~P2(a1,a2,f3(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[7948,7938,7547,7527,22,21,24])).
% 65.60/65.60 cnf(7963,plain,
% 65.60/65.60 (~P2(f6(a2),f5(a1),a4)),
% 65.60/65.60 inference(scs_inference,[],[4,7948,7942,7938,7547,7462,7527,22,21,24,25])).
% 65.60/65.60 cnf(7965,plain,
% 65.60/65.60 (~P4(a2,f5(a2),f3(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7948,7942,7915,7938,7573,7903,7547,7462,7527,22,21,24,25,26])).
% 65.60/65.60 cnf(7967,plain,
% 65.60/65.60 (~P2(f6(a2),f6(a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7948,7942,7915,7938,7860,7573,7903,7547,7462,7527,22,21,24,25,26,28])).
% 65.60/65.60 cnf(7973,plain,
% 65.60/65.60 (~P2(f7(a2,a2),f6(a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[7901,21])).
% 65.60/65.60 cnf(7979,plain,
% 65.60/65.60 (~P2(f5(a4),a1,a1)),
% 65.60/65.60 inference(scs_inference,[],[4,7901,7930,7881,7761,7555,7511,3722,21,22,24,25])).
% 65.60/65.60 cnf(7981,plain,
% 65.60/65.60 (~P4(f3(a1,a1),f7(a2,a2),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7901,7930,7917,7881,7761,7684,7555,3704,7511,3722,21,22,24,25,28])).
% 65.60/65.60 cnf(7988,plain,
% 65.60/65.60 (~P2(a1,f7(a1,a1),f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[7981,7905,22,21])).
% 65.60/65.60 cnf(7990,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f6(a2),a1)),
% 65.60/65.60 inference(scs_inference,[],[4,7981,7979,7905,7488,22,21,24])).
% 65.60/65.60 cnf(7992,plain,
% 65.60/65.60 (~P2(a1,a1,f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7981,7979,7905,7476,7488,22,21,24,25])).
% 65.60/65.60 cnf(7994,plain,
% 65.60/65.60 (~P2(a4,a4,a4)),
% 65.60/65.60 inference(scs_inference,[],[4,7981,7979,7905,7846,7668,7523,7476,7488,22,21,24,25,29])).
% 65.60/65.60 cnf(8001,plain,
% 65.60/65.60 (~P2(f5(a2),f3(a2,a2),a1)),
% 65.60/65.60 inference(scs_inference,[],[7856,21])).
% 65.60/65.60 cnf(8005,plain,
% 65.60/65.60 (~P2(a4,a1,a1)),
% 65.60/65.60 inference(scs_inference,[],[7994,7856,7965,7462,21,22,24])).
% 65.60/65.60 cnf(8007,plain,
% 65.60/65.60 (~P2(f6(a2),f7(a4,a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,7994,7932,7856,7965,7462,2330,21,22,24,25])).
% 65.60/65.60 cnf(8009,plain,
% 65.60/65.60 (P4(f7(a4,a4),f7(a1,a1),f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[4,7994,7932,7856,7965,7571,7474,7462,2330,21,22,24,25,27])).
% 65.60/65.60 cnf(8011,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f7(a4,a4),a4)),
% 65.60/65.60 inference(scs_inference,[],[4,7994,7932,7944,7856,7965,7571,7474,7498,7462,7470,2330,21,22,24,25,27,29])).
% 65.60/65.60 cnf(8013,plain,
% 65.60/65.60 (~P4(f5(a1),a4,a4)),
% 65.60/65.60 inference(scs_inference,[],[4,7994,7932,7944,7856,7965,7942,7571,7474,7498,7462,1479,7470,3821,2330,2521,21,22,24,25,27,29,28])).
% 65.60/65.60 cnf(8016,plain,
% 65.60/65.60 (P4(a4,f6(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7994,7932,7944,7856,7965,7942,7571,7474,7498,7462,1479,7470,3821,2330,2521,21,22,24,25,27,29,28,7723,13])).
% 65.60/65.60 cnf(8018,plain,
% 65.60/65.60 (P2(a1,f6(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7994,7932,7944,7856,7965,7942,7571,7474,7498,7462,1479,7470,3821,2330,2521,21,22,24,25,27,29,28,7723,13,12])).
% 65.60/65.60 cnf(8023,plain,
% 65.60/65.60 (~P4(a4,f5(a1),a4)),
% 65.60/65.60 inference(scs_inference,[],[8013,22])).
% 65.60/65.60 cnf(8025,plain,
% 65.60/65.60 (~P2(a1,a4,a1)),
% 65.60/65.60 inference(scs_inference,[],[8005,8013,22,21])).
% 65.60/65.60 cnf(8027,plain,
% 65.60/65.60 (P4(f6(a4),a4,a4)),
% 65.60/65.60 inference(scs_inference,[],[8005,8013,2,22,21,19])).
% 65.60/65.60 cnf(8029,plain,
% 65.60/65.60 (~P2(f6(a2),f5(a2),f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[4,8005,8013,7988,7555,2,22,21,19,24])).
% 65.60/65.60 cnf(8031,plain,
% 65.60/65.60 (~P2(f5(a1),f5(a1),a4)),
% 65.60/65.60 inference(scs_inference,[],[4,8005,8013,7988,7555,7547,2,22,21,19,24,25])).
% 65.60/65.60 cnf(8033,plain,
% 65.60/65.60 (~P2(f5(a4),f7(a4,a4),f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,8005,8013,7734,7988,7555,7456,7547,7498,3979,2,22,21,19,24,25,29])).
% 65.60/65.60 cnf(8035,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f6(a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,8005,8013,7734,7967,7988,7553,7555,7456,7547,7498,7470,3979,2,22,21,19,24,25,29,28])).
% 65.60/65.60 cnf(8037,plain,
% 65.60/65.60 (P4(a1,f6(a4),a1)),
% 65.60/65.60 inference(scs_inference,[],[4,8005,8013,7734,7967,7988,7553,7555,7456,7547,7498,7470,3979,2,22,21,19,24,25,29,28,2547])).
% 65.60/65.60 cnf(8039,plain,
% 65.60/65.60 (P4(f6(a4),f5(a4),f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[4,8005,8013,7734,7967,7988,7553,7460,7555,7456,7547,7498,7470,3979,2,22,21,19,24,25,29,28,2547,383])).
% 65.60/65.60 cnf(8052,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f6(a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8007,21])).
% 65.60/65.60 cnf(8054,plain,
% 65.60/65.60 (~P4(f6(a2),f3(a4,a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8007,8035,21,22])).
% 65.60/65.60 cnf(8056,plain,
% 65.60/65.60 (P4(f5(a4),f6(a4),f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[8027,8007,8035,7460,21,22,992])).
% 65.60/65.60 cnf(8058,plain,
% 65.60/65.60 (~P2(f3(a1,a1),a4,a1)),
% 65.60/65.60 inference(scs_inference,[],[8025,8027,8007,8035,7561,7460,7462,21,22,992,24])).
% 65.60/65.60 cnf(8060,plain,
% 65.60/65.60 (~P2(a1,f3(a4,a4),a4)),
% 65.60/65.60 inference(scs_inference,[],[8025,8027,8011,8007,8035,7517,7577,7561,7460,7462,21,22,992,24,25])).
% 65.60/65.60 cnf(8062,plain,
% 65.60/65.60 (P4(f6(a4),f6(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8025,8027,8016,8011,8007,8035,7517,7577,7561,7460,7462,21,22,992,24,25,26])).
% 65.60/65.60 cnf(8064,plain,
% 65.60/65.60 (~P4(a2,f5(a1),a2)),
% 65.60/65.60 inference(scs_inference,[],[8025,8023,8027,8016,8011,8007,8035,7472,7517,7577,7561,7460,7462,21,22,992,24,25,26,27])).
% 65.60/65.60 cnf(8072,plain,
% 65.60/65.60 (~P2(f5(a2),f6(a2),f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8029,7952,22,21])).
% 65.60/65.60 cnf(8074,plain,
% 65.60/65.60 (~P2(f7(a4,a4),a1,a1)),
% 65.60/65.60 inference(scs_inference,[],[4,7990,8029,7952,2330,22,21,24])).
% 65.60/65.60 cnf(8076,plain,
% 65.60/65.60 (~P2(f6(a2),a1,f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7990,8029,8052,7952,3734,2330,22,21,24,25])).
% 65.60/65.60 cnf(8078,plain,
% 65.60/65.60 (~P4(f7(a1,a1),f6(a4),a2)),
% 65.60/65.60 inference(scs_inference,[],[4,7990,8029,8052,7952,8037,7490,7563,3734,2330,22,21,24,25,26])).
% 65.60/65.60 cnf(8080,plain,
% 65.60/65.60 (P4(f7(a4,a4),f6(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[4,7990,8029,8052,7952,8016,8037,7490,7474,7563,3734,2330,22,21,24,25,26,27])).
% 65.60/65.60 cnf(8082,plain,
% 65.60/65.60 (~P4(a1,a2,a4)),
% 65.60/65.60 inference(scs_inference,[],[4,7990,8029,8052,7952,7994,8016,8037,7490,7472,7474,7563,3734,2330,22,21,24,25,26,27,28])).
% 65.60/65.60 cnf(8091,plain,
% 65.60/65.60 (~P2(a1,f7(a4,a4),a1)),
% 65.60/65.60 inference(scs_inference,[],[8082,8033,7979,7488,3722,21,22,24])).
% 65.60/65.60 cnf(8093,plain,
% 65.60/65.60 (~P2(a1,f6(a2),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,8082,8033,8074,7979,7488,3722,3734,21,22,24,25])).
% 65.60/65.60 cnf(8095,plain,
% 65.60/65.60 (P4(f7(a4,a4),f7(a4,a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,8082,8033,8074,7979,7484,7488,7474,3722,3734,21,22,24,25,26])).
% 65.60/65.60 cnf(8097,plain,
% 65.60/65.60 (P4(f7(a1,a1),f6(a4),f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[4,8082,8033,8074,7979,8037,7484,7488,7474,7563,3722,3734,21,22,24,25,26,27])).
% 65.60/65.60 cnf(8099,plain,
% 65.60/65.60 (~P4(a1,f6(a4),f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[4,8082,7992,8033,8074,7979,8037,7484,7476,7488,7474,7563,3722,3734,21,22,24,25,26,27,28])).
% 65.60/65.60 cnf(8106,plain,
% 65.60/65.60 (~P2(a2,f7(a4,a4),a4)),
% 65.60/65.60 inference(scs_inference,[],[8078,7838,22,21])).
% 65.60/65.60 cnf(8108,plain,
% 65.60/65.60 (~P2(a4,f5(a2),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8078,7838,8033,7555,7456,22,21,24])).
% 65.60/65.60 cnf(8110,plain,
% 65.60/65.60 (~P2(a1,f5(a4),f3(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8078,7838,8058,8033,7476,7555,7456,22,21,24,25])).
% 65.60/65.60 cnf(8112,plain,
% 65.60/65.60 (P4(f6(a4),f3(a1,a1),f3(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8078,7838,8058,8033,7590,8027,7476,7555,7456,22,21,24,25,26])).
% 65.60/65.60 cnf(8114,plain,
% 65.60/65.60 (~P4(f7(a2,a2),f5(a1),f7(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[8078,7838,8058,8064,8033,7590,8027,7684,7476,7555,7456,22,21,24,25,26,27])).
% 65.60/65.60 cnf(8116,plain,
% 65.60/65.60 (~P2(f5(a4),f6(a4),f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[8056,8078,7838,8058,8099,8064,8033,8016,7590,8027,7684,7476,7555,7456,22,21,24,25,26,27,29])).
% 65.60/65.60 cnf(8118,plain,
% 65.60/65.60 (~P2(f6(a4),f6(a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8056,8078,7838,8058,8099,8064,7750,8033,8016,7590,8027,7684,7484,7476,7555,7456,22,21,24,25,26,27,29,28])).
% 65.60/65.60 cnf(8125,plain,
% 65.60/65.60 (~P2(f6(a2),a4,f3(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,8114,8060,7462,21,22,24])).
% 65.60/65.60 cnf(8127,plain,
% 65.60/65.60 (~P2(f6(a2),f6(a2),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,8093,8114,8060,7517,7462,21,22,24,25])).
% 65.60/65.60 cnf(8129,plain,
% 65.60/65.60 (~P4(f6(a2),a4,a1)),
% 65.60/65.60 inference(scs_inference,[],[4,8093,8114,8060,8082,7668,7472,7517,7462,21,22,24,25,27])).
% 65.60/65.60 cnf(8131,plain,
% 65.60/65.60 (~P2(a1,f7(a4,a4),f3(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,8095,8093,8114,8060,7704,8082,7668,7472,7517,7494,7462,21,22,24,25,27,29])).
% 65.60/65.60 cnf(8133,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f6(a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,8095,8093,8114,8060,8080,8118,7704,8082,7668,7472,7517,7577,7494,7462,21,22,24,25,27,29,28])).
% 65.60/65.60 cnf(8138,plain,
% 65.60/65.60 (~P4(a4,f6(a2),a1)),
% 65.60/65.60 inference(scs_inference,[],[8129,22])).
% 65.60/65.60 cnf(8142,plain,
% 65.60/65.60 (~P2(f6(a2),f3(a4,a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[4,8129,8131,7480,22,21,24])).
% 65.60/65.60 cnf(8144,plain,
% 65.60/65.60 (P2(f3(a1,a1),f6(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[4,8129,8018,8131,7480,7561,22,21,24,25])).
% 65.60/65.60 cnf(8148,plain,
% 65.60/65.60 (~P2(a1,a1,f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[4,8129,8018,8131,7480,7630,8027,7561,7476,2521,22,21,24,25,26,29])).
% 65.60/65.60 cnf(8150,plain,
% 65.60/65.60 (~P4(a1,a2,a1)),
% 65.60/65.60 inference(scs_inference,[],[4,8129,8018,8091,8131,7480,7630,8027,7573,7561,7476,2521,22,21,24,25,26,29,28])).
% 65.60/65.60 cnf(8157,plain,
% 65.60/65.60 (~P4(a2,a1,a1)),
% 65.60/65.60 inference(scs_inference,[],[8150,8142,21,22])).
% 65.60/65.60 cnf(8159,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f5(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8150,8142,8116,7488,82,21,22,24])).
% 65.60/65.60 cnf(8161,plain,
% 65.60/65.60 (~P2(f6(a2),f3(a1,a1),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8150,8076,8142,8116,7488,7561,82,3734,21,22,24,25])).
% 65.60/65.60 cnf(8163,plain,
% 65.60/65.60 (P4(f6(a4),f7(a2,a2),f7(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[8150,8076,8142,8116,7649,8027,7488,7561,82,3734,21,22,24,25,26])).
% 65.60/65.60 cnf(8165,plain,
% 65.60/65.60 (~P4(f7(a1,a1),f6(a4),a4)),
% 65.60/65.60 inference(scs_inference,[],[8150,8076,8142,8116,7950,8097,7649,8037,8027,3716,7488,7561,82,3734,21,22,24,25,26,28])).
% 65.60/65.60 cnf(8167,plain,
% 65.60/65.60 (~P4(a4,a4,a2)),
% 65.60/65.60 inference(scs_inference,[],[8150,8076,8142,8116,7950,8097,7649,8037,8027,3716,7488,7561,82,3734,21,22,24,25,26,28,3676])).
% 65.60/65.60 cnf(8169,plain,
% 65.60/65.60 (~P4(f7(a4,a4),f6(a2),x81691)+P4(x81691,a2,f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8150,8076,8142,8116,7950,8097,8095,7649,8037,8027,7573,3716,7488,7561,82,3734,21,22,24,25,26,28,3676,27])).
% 65.60/65.60 cnf(8173,plain,
% 65.60/65.60 (~P2(f3(a1,a1),f6(a2),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8161,21])).
% 65.60/65.60 cnf(8177,plain,
% 65.60/65.60 (~P2(a1,f7(a4,a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8127,8133,8161,7517,3698,21,22,24])).
% 65.60/65.60 cnf(8179,plain,
% 65.60/65.60 (~P2(a1,a4,f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8127,8133,8161,8125,7480,7517,7470,3698,21,22,24,25])).
% 65.60/65.60 cnf(8181,plain,
% 65.60/65.60 (P4(f6(a4),f3(a4,a4),f3(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8127,8133,8161,8125,7480,7515,8027,7517,7470,3698,21,22,24,25,26])).
% 65.60/65.60 cnf(8183,plain,
% 65.60/65.60 (P4(f3(a4,a4),a1,a1)),
% 65.60/65.60 inference(scs_inference,[],[8127,8133,8161,8125,7480,7515,8027,7517,7476,7470,3698,3793,21,22,24,25,26,29])).
% 65.60/65.60 cnf(8185,plain,
% 65.60/65.60 (~P2(f6(a4),f6(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8127,8133,8161,8163,8125,7480,7765,7515,8027,7517,7476,7470,3698,3793,21,22,24,25,26,29,28])).
% 65.60/65.60 cnf(8194,plain,
% 65.60/65.60 (P2(f6(a2),f6(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8108,8165,8144,3704,21,22,24])).
% 65.60/65.60 cnf(8196,plain,
% 65.60/65.60 (~P2(f3(a1,a1),f3(a1,a1),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8108,8165,8185,8144,3704,21,22,24,25])).
% 65.60/65.60 cnf(8198,plain,
% 65.60/65.60 (P4(f7(a4,a4),f3(a4,a4),f3(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8108,8181,8165,8185,8144,8080,3704,21,22,24,25,26])).
% 65.60/65.60 cnf(8200,plain,
% 65.60/65.60 (P4(f3(a4,a4),a1,f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8108,8181,8165,8185,8183,8144,8080,7480,3716,3704,7563,21,22,24,25,26,29])).
% 65.60/65.60 cnf(8202,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f6(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8108,8181,8165,8185,8183,8144,8080,7480,3716,7577,3704,7563,21,22,24,25,26,29,28])).
% 65.60/65.60 cnf(8207,plain,
% 65.60/65.60 (~P2(f5(a4),a1,f3(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8110,21])).
% 65.60/65.60 cnf(8213,plain,
% 65.60/65.60 (~P2(a1,f3(a1,a1),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[7814,8110,8196,8202,7511,7561,7462,1940,21,22,24,25])).
% 65.60/65.60 cnf(8215,plain,
% 65.60/65.60 (P4(f7(a4,a4),a1,a1)),
% 65.60/65.60 inference(scs_inference,[],[8198,7814,8110,8196,8202,8183,7511,7561,7462,1940,21,22,24,25,26])).
% 65.60/65.60 cnf(8217,plain,
% 65.60/65.60 (~P4(f6(a4),f7(a2,a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8198,7814,8110,8196,8202,8194,41,8183,7684,7511,7561,7462,1940,21,22,24,25,26,28])).
% 65.60/65.60 cnf(8219,plain,
% 65.60/65.60 (~P4(f6(a4),f7(a1,a1),x82191)+P4(f3(a4,a4),a1,x82191)),
% 65.60/65.60 inference(scs_inference,[],[8198,7814,8110,8196,8200,8202,8194,41,8181,8183,7684,7511,7561,7462,1940,21,22,24,25,26,28,27])).
% 65.60/65.60 cnf(8225,plain,
% 65.60/65.60 (~P2(f5(a4),f7(a4,a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8159,8217,22,21])).
% 65.60/65.60 cnf(8227,plain,
% 65.60/65.60 (~P2(a1,f7(a2,a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[7897,8159,8217,7592,7476,22,21,24])).
% 65.60/65.60 cnf(8229,plain,
% 65.60/65.60 (~P2(f6(a2),f5(a4),a1)),
% 65.60/65.60 inference(scs_inference,[],[7897,8159,8217,8177,7592,7488,7476,3734,22,21,24,25])).
% 65.60/65.60 cnf(8237,plain,
% 65.60/65.60 (~P4(f3(a4,a4),a1,a2)),
% 65.60/65.60 inference(scs_inference,[],[7897,8159,8217,8177,8157,8198,7618,8200,8181,8183,7480,7592,7577,7488,7476,7563,3734,22,21,24,25,27,26,29,28])).
% 65.60/65.60 cnf(8240,plain,
% 65.60/65.60 (~P2(f3(a1,a1),a1,f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8213,21])).
% 65.60/65.60 cnf(8244,plain,
% 65.60/65.60 (P2(f5(a1),f6(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8213,8237,8018,7547,21,22,24])).
% 65.60/65.60 cnf(8246,plain,
% 65.60/65.60 (~P2(f6(a2),f6(a2),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8213,8237,8194,8018,8185,7547,21,22,24,25])).
% 65.60/65.60 cnf(8250,plain,
% 65.60/65.60 (~P2(a2,f7(a2,a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8213,8237,8217,8194,8018,8163,8185,7612,7684,8027,7547,21,22,24,25,26,29])).
% 65.60/65.60 cnf(8252,plain,
% 65.60/65.60 (~P4(f3(a4,a4),a1,f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8213,8215,8237,8148,8217,8194,8018,8163,8185,7612,7684,8027,7547,7577,21,22,24,25,26,29,28])).
% 65.60/65.60 cnf(8254,plain,
% 65.60/65.60 (~P4(f6(a4),f7(a1,a1),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8213,8215,8237,8148,8217,8194,8018,8163,8185,7612,7684,8027,7547,7577,21,22,24,25,26,29,28,8219])).
% 65.60/65.60 cnf(8256,plain,
% 65.60/65.60 (P4(f7(a4,a4),x82561,f7(a4,a4))+~P4(a2,x82561,a2)),
% 65.60/65.60 inference(scs_inference,[],[8213,8215,8237,8148,8217,8194,8018,8163,8185,7612,7573,7684,8027,7547,7577,21,22,24,25,26,29,28,8219,27])).
% 65.60/65.60 cnf(8258,plain,
% 65.60/65.60 (~P4(f7(a1,a1),f6(a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8254,22])).
% 65.60/65.60 cnf(8262,plain,
% 65.60/65.60 (~P2(a2,a1,f3(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[8001,8254,8227,7511,7476,22,21,24])).
% 65.60/65.60 cnf(8264,plain,
% 65.60/65.60 (~P2(f5(a1),f7(a2,a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8001,8254,8227,7592,7511,7547,7476,22,21,24,25])).
% 65.60/65.60 cnf(8266,plain,
% 65.60/65.60 (~P4(f6(a4),a1,f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8001,8254,8227,8252,8181,8183,7592,7511,7547,7476,22,21,24,25,27])).
% 65.60/65.60 cnf(8268,plain,
% 65.60/65.60 (~P4(a2,f5(a2),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8001,8254,8227,8252,7862,8181,8183,7630,7592,7472,7511,7547,7476,22,21,24,25,27,26])).
% 65.60/65.60 cnf(8270,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f6(a2),f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[7873,8001,8254,8227,8252,7862,8181,8183,7630,7553,7592,7472,7511,7547,7476,7470,22,21,24,25,27,26,28])).
% 65.60/65.60 cnf(8272,plain,
% 65.60/65.60 (P3(f6(a2),f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[7873,8001,8254,8227,8252,7862,4435,8181,8183,7630,7553,7592,7472,7581,7511,7547,7476,7470,2330,22,21,24,25,27,26,28,23])).
% 65.60/65.60 cnf(8282,plain,
% 65.60/65.60 (~P2(f5(a2),a1,f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8072,8264,8270,4435,2330,21,22,24])).
% 65.60/65.60 cnf(8284,plain,
% 65.60/65.60 (~P2(f5(a1),f7(a2,a2),a1)),
% 65.60/65.60 inference(scs_inference,[],[8072,8264,8270,4435,3702,3734,2330,21,22,24,25])).
% 65.60/65.60 cnf(8286,plain,
% 65.60/65.60 (~P4(f6(a4),a2,f3(a2,a2))),
% 65.60/65.60 inference(scs_inference,[],[8072,8264,8270,7767,8163,4435,7525,3702,3734,2330,21,22,24,25,27])).
% 65.60/65.60 cnf(8288,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f7(a4,a4),a2)),
% 65.60/65.60 inference(scs_inference,[],[8072,8264,8270,8215,8157,7767,8163,4435,7525,7476,3702,3734,2330,21,22,24,25,27,29])).
% 65.60/65.60 cnf(8290,plain,
% 65.60/65.60 (~P4(f6(a4),a4,f5(a1))),
% 65.60/65.60 inference(scs_inference,[],[8072,8264,8270,8031,8215,8244,8157,7767,8163,4435,8027,7525,7476,3821,3702,3734,2330,21,22,24,25,27,29,28])).
% 65.60/65.60 cnf(8297,plain,
% 65.60/65.60 (~P4(f5(a2),a2,f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8268,22])).
% 65.60/65.60 cnf(8299,plain,
% 65.60/65.60 (~P2(f7(a2,a2),a2,f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8250,8268,22,21])).
% 65.60/65.60 cnf(8301,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f6(a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8225,8250,8268,8018,7488,22,21,24])).
% 65.60/65.60 cnf(8303,plain,
% 65.60/65.60 (~P2(f5(a1),f5(a1),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8225,8250,8268,8244,8018,8185,7488,22,21,24,25])).
% 65.60/65.60 cnf(8305,plain,
% 65.60/65.60 (P4(f3(a1,a1),f6(a4),f3(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8225,8250,8268,8244,8018,8185,8037,7488,7561,22,21,24,25,29])).
% 65.60/65.60 cnf(8307,plain,
% 65.60/65.60 (~P4(f3(a1,a1),f6(a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8225,8250,8268,7875,8244,8018,8185,8037,7488,7561,22,21,24,25,29,28])).
% 65.60/65.60 cnf(8312,plain,
% 65.60/65.60 (~P2(f6(a4),f7(a4,a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8301,21])).
% 65.60/65.60 cnf(8314,plain,
% 65.60/65.60 (~P4(f6(a4),f3(a1,a1),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8301,8307,21,22])).
% 65.60/65.60 cnf(8316,plain,
% 65.60/65.60 (~P2(f3(a1,a1),f6(a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8301,8307,8246,8144,3704,21,22,24])).
% 65.60/65.60 cnf(8318,plain,
% 65.60/65.60 (~P2(a1,f3(a4,a4),a2)),
% 65.60/65.60 inference(scs_inference,[],[8301,8307,8288,8246,8144,3704,7517,7577,21,22,24,25])).
% 65.60/65.60 cnf(8320,plain,
% 65.60/65.60 (~P2(f5(a1),a4,f5(a1))),
% 65.60/65.60 inference(scs_inference,[],[8301,8307,8288,8246,8290,8144,8244,3704,8027,7517,7577,3821,21,22,24,25,29])).
% 65.60/65.60 cnf(8322,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f7(a4,a4),a2)),
% 65.60/65.60 inference(scs_inference,[],[8301,8307,8288,8246,8290,8144,8095,8244,3704,8027,7517,7577,3821,21,22,24,25,29,28])).
% 65.60/65.60 cnf(8331,plain,
% 65.60/65.60 (~P2(f7(a2,a2),f5(a1),a1)),
% 65.60/65.60 inference(scs_inference,[],[8284,8286,22,21])).
% 65.60/65.60 cnf(8333,plain,
% 65.60/65.60 (~P2(f6(a4),a1,a1)),
% 65.60/65.60 inference(scs_inference,[],[8284,8286,8312,7517,22,21,24])).
% 65.60/65.60 cnf(8335,plain,
% 65.60/65.60 (~P2(a1,a1,f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8284,8286,8312,7517,22,21,24,25])).
% 65.60/65.60 cnf(8342,plain,
% 65.60/65.60 (~P2(f6(a4),f3(a1,a1),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8316,8322,22,21])).
% 65.60/65.60 cnf(8344,plain,
% 65.60/65.60 (~P2(a1,f6(a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8316,8322,8246,8194,3734,22,21,24])).
% 65.60/65.60 cnf(8346,plain,
% 65.60/65.60 (~P2(f7(a1,a1),f6(a2),f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[8316,8322,8282,8246,8194,4435,3734,22,21,24,25])).
% 65.60/65.60 cnf(8348,plain,
% 65.60/65.60 (~P4(f5(a4),f6(a4),f3(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8316,8322,8207,8282,8246,8194,8056,4435,8037,3722,3734,22,21,24,25,28])).
% 65.60/65.60 cnf(8354,plain,
% 65.60/65.60 (~P2(f6(a2),f7(a1,a1),f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[8346,21])).
% 65.60/65.60 cnf(8358,plain,
% 65.60/65.60 (~P2(a4,f5(a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8346,8348,8116,7456,82,21,22,24])).
% 65.60/65.60 cnf(8360,plain,
% 65.60/65.60 (~P2(f5(a1),f6(a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8346,8348,8344,8116,8018,7456,7547,82,21,22,24,25])).
% 65.60/65.60 cnf(8362,plain,
% 65.60/65.60 (~P2(a4,f6(a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8346,8348,8106,8344,8116,8018,7668,7573,7472,7456,7547,82,21,22,24,25,28])).
% 65.60/65.60 cnf(8367,plain,
% 65.60/65.60 (~P4(a1,f6(a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8266,22])).
% 65.60/65.60 cnf(8369,plain,
% 65.60/65.60 (~P2(f6(a4),f5(a1),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8360,8266,22,21])).
% 65.60/65.60 cnf(8371,plain,
% 65.60/65.60 (~P2(f6(a4),f3(a1,a1),a1)),
% 65.60/65.60 inference(scs_inference,[],[8342,8360,8266,8194,3734,22,21,25])).
% 65.60/65.60 cnf(8373,plain,
% 65.60/65.60 (~P2(a1,f6(a4),a1)),
% 65.60/65.60 inference(scs_inference,[],[8335,8342,8360,8266,8144,8194,7561,3734,22,21,25,24])).
% 65.60/65.60 cnf(8375,plain,
% 65.60/65.60 (~P4(f7(a1,a1),a2,f5(a1))),
% 65.60/65.60 inference(scs_inference,[],[8335,8342,8360,8266,8320,8144,8194,4435,7472,7561,3734,22,21,25,24,28])).
% 65.60/65.60 cnf(8377,plain,
% 65.60/65.60 (~P4(f6(a2),f6(a4),x83771)+P4(x83771,f7(a2,a2),a2)),
% 65.60/65.60 inference(scs_inference,[],[8335,8342,8360,8266,8320,8163,8144,8194,4435,7684,7472,7561,3734,22,21,25,24,28,27])).
% 65.60/65.60 cnf(8381,plain,
% 65.60/65.60 (~P2(f3(a1,a1),f6(a4),a1)),
% 65.60/65.60 inference(scs_inference,[],[8371,21])).
% 65.60/65.60 cnf(8385,plain,
% 65.60/65.60 (~P2(f6(a2),f6(a4),f5(a1))),
% 65.60/65.60 inference(scs_inference,[],[8303,8371,8375,8244,3712,21,22,24])).
% 65.60/65.60 cnf(8387,plain,
% 65.60/65.60 (~P2(f7(a1,a1),f5(a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8303,8371,8375,7783,8244,3712,3716,7511,21,22,24,25])).
% 65.60/65.60 cnf(8389,plain,
% 65.60/65.60 (~P4(a1,f7(a4,a4),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8303,8371,8375,7783,8225,8095,8244,3712,3716,7511,7488,3979,21,22,24,25,28])).
% 65.60/65.60 cnf(8398,plain,
% 65.60/65.60 (~P2(f6(a2),f6(a4),a1)),
% 65.60/65.60 inference(scs_inference,[],[8387,8381,8389,8144,3704,22,21,25])).
% 65.60/65.60 cnf(8400,plain,
% 65.60/65.60 (~P2(f3(a1,a1),f5(a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[7781,8387,8381,8389,8144,7555,3704,7561,22,21,25,24])).
% 65.60/65.60 cnf(8409,plain,
% 65.60/65.60 (~P4(f6(a4),a1,f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[8400,8099,21,22])).
% 65.60/65.60 cnf(8413,plain,
% 65.60/65.60 (~P2(f5(a2),a2,f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8373,8400,8099,7555,7511,21,22,25,24])).
% 65.60/65.60 cnf(8415,plain,
% 65.60/65.60 (~P2(f5(a4),f6(a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8373,8400,8367,8099,8016,8056,7555,7511,7456,21,22,25,24,29])).
% 65.60/65.60 cnf(8423,plain,
% 65.60/65.60 (~P2(f6(a4),f6(a2),f5(a1))),
% 65.60/65.60 inference(scs_inference,[],[8385,8064,22,21])).
% 65.60/65.60 cnf(8425,plain,
% 65.60/65.60 (P2(f5(a4),f7(a4,a4),f3(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8385,8064,7488,7561,82,22,21,25])).
% 65.60/65.60 cnf(8427,plain,
% 65.60/65.60 (P2(f5(a4),f3(a4,a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8385,8064,7488,7577,7517,7561,82,22,21,25,24])).
% 65.60/65.60 cnf(8429,plain,
% 65.60/65.60 (~P2(f7(a1,a1),a1,f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8258,8385,8064,8097,3716,8037,7488,7577,7517,7561,82,22,21,25,24,29])).
% 65.60/65.60 cnf(8433,plain,
% 65.60/65.60 (~P4(f7(a4,a4),a2,a1)),
% 65.60/65.60 inference(scs_inference,[],[8258,8385,8262,8064,8097,7649,7676,7686,7684,3716,8037,7488,7577,7517,7561,82,22,21,25,24,29,27,28])).
% 65.60/65.60 cnf(8437,plain,
% 65.60/65.60 (~P2(f6(a2),a4,f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8362,21])).
% 65.60/65.60 cnf(8441,plain,
% 65.60/65.60 (~P2(f5(a1),f3(a4,a4),a2)),
% 65.60/65.60 inference(scs_inference,[],[8362,8318,8433,7480,7547,21,22,25])).
% 65.60/65.60 cnf(8443,plain,
% 65.60/65.60 (~P2(a4,f6(a2),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8362,8415,8318,8433,7480,7456,7547,2330,21,22,25,24])).
% 65.60/65.60 cnf(8445,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f6(a2),a4)),
% 65.60/65.60 inference(scs_inference,[],[8362,8415,8318,8433,3736,7480,7553,7456,7547,7470,2330,21,22,25,24,28])).
% 65.60/65.60 cnf(8450,plain,
% 65.60/65.60 (~P2(a1,f7(a1,a1),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8429,21])).
% 65.60/65.60 cnf(8454,plain,
% 65.60/65.60 (~P3(f7(a1,a1),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8429,8445,8272,21,22,18])).
% 65.60/65.60 cnf(8456,plain,
% 65.60/65.60 (~P2(f6(a2),a1,f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8429,8445,8272,4786,3734,21,22,18,23])).
% 65.60/65.60 cnf(8458,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f6(a2),f3(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8173,8429,8445,8425,8427,8272,4786,3734,21,22,18,23,25])).
% 65.60/65.60 cnf(8460,plain,
% 65.60/65.60 (~P2(a1,f5(a2),f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8173,8354,8429,8445,8425,8427,8272,4786,7555,3698,3734,21,22,18,23,25,24])).
% 65.60/65.60 cnf(8462,plain,
% 65.60/65.60 (~P4(f5(a4),f6(a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8173,8354,8429,8445,8398,8425,8427,8272,4786,8016,7555,8037,7456,3698,3734,21,22,18,23,25,24,28])).
% 65.60/65.60 cnf(8470,plain,
% 65.60/65.60 (~P2(a1,f6(a2),f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8456,8462,22,21])).
% 65.60/65.60 cnf(8472,plain,
% 65.60/65.60 (~P2(f7(a1,a1),f6(a2),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8456,8462,4435,3734,22,21,25])).
% 65.60/65.60 cnf(8474,plain,
% 65.60/65.60 (~P2(a1,f6(a4),f3(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8456,8462,8213,8018,4435,7476,3734,22,21,25,24])).
% 65.60/65.60 cnf(8478,plain,
% 65.60/65.60 (~P4(f7(a4,a4),f6(a4),a1)),
% 65.60/65.60 inference(scs_inference,[],[8454,8456,8462,8213,8207,8425,8305,8018,8056,4435,7476,3734,22,21,25,24,7756,28])).
% 65.60/65.60 cnf(8482,plain,
% 65.60/65.60 (~P2(f6(a2),f7(a4,a4),f3(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8458,21])).
% 65.60/65.60 cnf(8486,plain,
% 65.60/65.60 (~P2(f5(a1),f6(a4),f3(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8458,8474,8478,8018,7547,21,22,25])).
% 65.60/65.60 cnf(8488,plain,
% 65.60/65.60 (~P2(f7(a4,a4),f6(a2),f6(a4))),
% 65.60/65.60 inference(scs_inference,[],[8458,8474,8478,8415,8018,7547,7488,2330,21,22,25,24])).
% 65.60/65.60 cnf(8490,plain,
% 65.60/65.60 (~P4(f3(a1,a1),f6(a4),f6(a2))),
% 65.60/65.60 inference(scs_inference,[],[8458,8474,8478,8415,8425,8080,8018,8056,7547,7488,2330,21,22,25,24,28])).
% 65.60/65.60 cnf(8492,plain,
% 65.60/65.60 (~P4(f6(a2),a4,f5(a2))),
% 65.60/65.60 inference(scs_inference,[],[8458,8474,8478,8297,8415,8425,8080,8018,7668,8056,7573,7547,7488,2330,21,22,25,24,28,27])).
% 65.60/65.60 cnf(8502,plain,
% 65.60/65.60 (~P2(f7(a1,a1),a1,a1)),
% 65.60/65.60 inference(scs_inference,[],[8470,8472,8490,4435,2330,22,21,25])).
% 65.60/65.60 cnf(8504,plain,
% 65.60/65.60 (~P2(a1,f3(a4,a4),f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8470,8482,8472,8490,7480,4435,3698,2330,22,21,25,24])).
% 65.60/65.60 cnf(8506,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f6(a4),a4)),
% 65.60/65.60 inference(scs_inference,[],[8470,8482,8472,8490,8478,8427,7480,8056,4435,7456,3698,2330,22,21,25,24,29])).
% 65.60/65.60 cnf(8508,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f6(a2),a2)),
% 65.60/65.60 inference(scs_inference,[],[8470,8482,8472,8490,3709,8478,8427,7480,7553,8056,4435,7456,7470,3698,2330,22,21,25,24,29,28])).
% 65.60/65.60 cnf(8511,plain,
% 65.60/65.60 (~P2(a1,f7(a1,a1),a1)),
% 65.60/65.60 inference(scs_inference,[],[8502,21])).
% 65.60/65.60 cnf(8515,plain,
% 65.60/65.60 (~P2(a1,a1,f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8502,8506,7476,21,22,25])).
% 65.60/65.60 cnf(8517,plain,
% 65.60/65.60 (~P2(a1,a2,f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8502,8506,7742,7527,7476,21,22,25,24])).
% 65.60/65.60 cnf(8519,plain,
% 65.60/65.60 (~P4(f5(a4),f6(a4),f5(a1))),
% 65.60/65.60 inference(scs_inference,[],[8502,8486,8506,7742,8425,8080,8305,7527,7476,21,22,25,24,28])).
% 65.60/65.60 cnf(8521,plain,
% 65.60/65.60 (~P3(f7(a1,a1),a1)),
% 65.60/65.60 inference(scs_inference,[],[8502,8486,8506,7742,8425,8080,8305,7527,7476,21,22,25,24,28,7640])).
% 65.60/65.60 cnf(8522,plain,
% 65.60/65.60 (~P2(f7(a1,a1),f7(a1,a1),a1)),
% 65.60/65.60 inference(scs_inference,[],[8502,8486,8506,7742,8425,8080,8305,7527,7476,21,22,25,24,28,7640,7642])).
% 65.60/65.60 cnf(8523,plain,
% 65.60/65.60 (~P2(f5(a2),a2,f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8502,8486,8506,7702,7742,8425,8080,8305,7527,7476,7511,21,22,25,24,28,7640,7642,23])).
% 65.60/65.60 cnf(8531,plain,
% 65.60/65.60 (~P2(f5(a1),a1,f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8515,7663])).
% 65.60/65.60 cnf(8534,plain,
% 65.60/65.60 (~P2(f3(a4,a4),a1,f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8508,8504,22,21])).
% 65.60/65.60 cnf(8538,plain,
% 65.60/65.60 (~P2(a4,a2,a4)),
% 65.60/65.60 inference(scs_inference,[],[8508,8515,8504,7714,3716,7527,7456,4433,22,21,25,24])).
% 65.60/65.60 cnf(8540,plain,
% 65.60/65.60 (~P4(f5(a4),a1,f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8508,8515,8504,8522,7714,8215,8427,8200,3716,7527,7456,4433,22,21,25,24,28])).
% 65.60/65.60 cnf(8546,plain,
% 65.60/65.60 (~P2(a2,a4,a4)),
% 65.60/65.60 inference(scs_inference,[],[8538,21])).
% 65.60/65.60 cnf(8550,plain,
% 65.60/65.60 (~P2(f7(a1,a1),f6(a2),f5(a1))),
% 65.60/65.60 inference(scs_inference,[],[8538,8531,8519,4435,3734,21,22,25])).
% 65.60/65.60 cnf(8554,plain,
% 65.60/65.60 (~P4(f3(a1,a1),f6(a4),f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[8538,8531,8331,8519,8116,8425,8080,8056,4435,7547,3757,3734,21,22,25,24,28])).
% 65.60/65.60 cnf(8556,plain,
% 65.60/65.60 (~P2(f7(a2,a2),a1,a1)),
% 65.60/65.60 inference(scs_inference,[],[8538,8531,8331,8519,8116,8425,8080,8056,4435,7547,3757,3734,21,22,25,24,28,1483])).
% 65.60/65.60 cnf(8562,plain,
% 65.60/65.60 (~P4(f6(a4),f3(a1,a1),f5(a4))),
% 65.60/65.60 inference(scs_inference,[],[8554,22])).
% 65.60/65.60 cnf(8568,plain,
% 65.60/65.60 (~P2(f7(a4,a4),a4,f7(a4,a4))),
% 65.60/65.60 inference(scs_inference,[],[8523,8554,8515,7600,4435,7488,7462,3734,22,21,25,24])).
% 65.60/65.60 cnf(8570,plain,
% 65.60/65.60 (~P2(f5(a4),f7(a4,a4),f7(a1,a1))),
% 65.60/65.60 inference(scs_inference,[],[8523,8554,8515,8521,7600,4435,7488,7462,3734,319,22,21,25,24,23])).
% 65.60/65.60 cnf(8572,plain,
% 65.60/65.60 (~P4(f3(a4,a4),f7(a1,a1),a1)),
% 65.60/65.61 inference(scs_inference,[],[8523,8554,8515,8522,8521,7600,8009,4435,7577,7488,7462,3734,319,22,21,25,24,23,28])).
% 65.60/65.61 cnf(8578,plain,
% 65.60/65.61 (~P2(a1,f7(a2,a2),a1)),
% 65.60/65.61 inference(scs_inference,[],[8556,21])).
% 65.60/65.61 cnf(8582,plain,
% 65.60/65.61 (~P2(a1,f3(a1,a1),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8556,8570,8572,8425,82,21,22,25])).
% 65.60/65.61 cnf(8584,plain,
% 65.60/65.61 (~P2(a4,f7(a1,a1),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8556,8570,8572,8425,7456,82,2249,21,22,25,24])).
% 65.60/65.61 cnf(8586,plain,
% 65.60/65.61 (~P2(f5(a4),a4,f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8556,8570,8572,8521,8425,7456,82,2249,319,21,22,25,24,23])).
% 65.60/65.61 cnf(8588,plain,
% 65.60/65.61 (~P4(f5(a4),a1,f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8556,8570,8572,8521,8427,8215,8183,8425,7456,82,2249,319,21,22,25,24,23,28])).
% 65.60/65.61 cnf(8593,plain,
% 65.60/65.61 (~P4(a1,f5(a4),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8540,22])).
% 65.60/65.61 cnf(8595,plain,
% 65.60/65.61 (~P2(f6(a2),f7(a4,a4),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8488,8540,22,21])).
% 65.60/65.61 cnf(8597,plain,
% 65.60/65.61 (~P2(f5(a4),a4,f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8488,8568,8540,8427,7470,22,21,25])).
% 65.60/65.61 cnf(8599,plain,
% 65.60/65.61 (~P2(f7(a1,a1),a1,f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[8488,8550,8568,8540,8427,3712,7470,2330,22,21,25,24])).
% 65.60/65.61 cnf(8601,plain,
% 65.60/65.61 (~P2(f7(a1,a1),f7(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8488,8550,8568,8540,8454,8272,8427,3712,7470,4433,2330,22,21,25,24,23])).
% 65.60/65.61 cnf(8603,plain,
% 65.60/65.61 (~P4(a1,f3(a4,a4),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[7854,8488,8550,8568,8540,8454,8272,7515,8427,3712,7462,7470,4433,2330,22,21,25,24,23,29])).
% 65.60/65.61 cnf(8605,plain,
% 65.60/65.61 (~P4(f3(a2,a2),a1,f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[7854,8488,8550,8568,8540,8472,8454,7565,8272,7515,8427,3712,7563,7462,7470,4433,2330,22,21,25,24,23,29,28])).
% 65.60/65.61 cnf(8608,plain,
% 65.60/65.61 (~P2(f3(a1,a1),a1,f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8582,21])).
% 65.60/65.61 cnf(8610,plain,
% 65.60/65.61 (~P4(a1,f5(a4),f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8582,8588,21,22])).
% 65.60/65.61 cnf(8612,plain,
% 65.60/65.61 (~P2(f5(a1),f6(a2),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8582,8588,8599,3712,3734,21,22,25])).
% 65.60/65.61 cnf(8614,plain,
% 65.60/65.61 (~P2(a1,f6(a4),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8582,8595,8588,8599,8194,3712,3734,21,22,25,24])).
% 65.60/65.61 cnf(8616,plain,
% 65.60/65.61 (~P2(f5(a4),f6(a4),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8582,8595,8588,8599,8307,8425,8194,8080,8056,3712,3734,21,22,25,24,29])).
% 65.60/65.61 cnf(8620,plain,
% 65.60/65.61 (~P4(f3(a4,a4),a1,f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8603,22])).
% 65.60/65.61 cnf(8624,plain,
% 65.60/65.61 (~P2(f5(a1),f5(a2),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8584,8460,8603,7555,7547,22,21,25])).
% 65.60/65.61 cnf(8626,plain,
% 65.60/65.61 (~P2(a1,f3(a4,a4),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8584,8616,8460,8603,8427,7555,7547,3722,22,21,25,24])).
% 65.60/65.61 cnf(8628,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f7(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8601,8584,8616,8460,8603,7571,8427,7555,7547,3722,7470,22,21,25,24,28])).
% 65.60/65.61 cnf(8641,plain,
% 65.60/65.61 (P4(f7(a4,a4),f6(a2),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8441,8628,8511,7553,7474,7511,21,22,25,27])).
% 65.60/65.61 cnf(8643,plain,
% 65.60/65.61 (~P2(a1,a2,f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8441,8628,8511,7553,7474,7527,7511,7547,21,22,25,27,24])).
% 65.60/65.61 cnf(8645,plain,
% 65.60/65.61 (~P4(a4,f6(a4),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8441,8628,8511,8614,8016,7553,7474,8037,7527,7511,7547,7462,21,22,25,27,24,28])).
% 65.60/65.61 cnf(8650,plain,
% 65.60/65.61 (~P4(a1,f3(a2,a2),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8605,22])).
% 65.60/65.61 cnf(8652,plain,
% 65.60/65.61 (~P2(a4,f5(a4),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8586,8605,22,21])).
% 65.60/65.61 cnf(8654,plain,
% 65.60/65.61 (~P2(f7(a1,a1),f6(a2),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8586,8608,8605,4435,3734,22,21,25])).
% 65.60/65.61 cnf(8656,plain,
% 65.60/65.61 (P4(f7(a4,a4),a4,a4)),
% 65.60/65.61 inference(scs_inference,[],[8586,8608,8641,8605,7472,4435,3734,22,21,25,26])).
% 65.60/65.61 cnf(8658,plain,
% 65.60/65.61 (~P2(a1,f6(a4),f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8586,8608,8641,8605,8626,8018,7472,4435,7476,3734,22,21,25,26,24])).
% 65.60/65.61 cnf(8660,plain,
% 65.60/65.61 (~P4(f3(a2,a2),a1,a1)),
% 65.60/65.61 inference(scs_inference,[],[8586,8608,8641,8605,8626,8502,7565,8018,7472,4435,7476,7563,3734,22,21,25,26,24,28])).
% 65.60/65.61 cnf(8662,plain,
% 65.60/65.61 (~P2(f7(a1,a1),a1,f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8586,8608,8641,8605,8620,8626,8502,7565,8183,8018,7480,7472,4435,7476,7563,3734,22,21,25,26,24,28,29])).
% 65.60/65.61 cnf(8664,plain,
% 65.60/65.61 (~P4(a4,a4,f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8586,8608,8641,8605,8620,8626,8502,7565,8183,8018,7480,7472,4435,7476,7563,3734,22,21,25,26,24,28,29,3676])).
% 65.60/65.61 cnf(8666,plain,
% 65.60/65.61 (~P2(f6(a2),f7(a1,a1),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8654,21])).
% 65.60/65.61 cnf(8668,plain,
% 65.60/65.61 (~P4(f6(a4),a4,f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8654,8645,21,22])).
% 65.60/65.61 cnf(8670,plain,
% 65.60/65.61 (~P2(f6(a2),f5(a2),f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8654,8299,8645,7511,3734,21,22,25])).
% 65.60/65.61 cnf(8672,plain,
% 65.60/65.61 (P4(f7(a4,a4),f5(a1),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[8654,8299,8645,8656,7511,3734,1662,21,22,25,26])).
% 65.60/65.61 cnf(8674,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f7(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8654,8299,8450,8645,8656,7561,7511,2249,3734,1662,21,22,25,26,24])).
% 65.60/65.61 cnf(8678,plain,
% 65.60/65.61 (P4(f3(a1,a1),a4,a1)),
% 65.60/65.61 inference(scs_inference,[],[8654,8299,8450,8645,8656,8381,8062,8144,8425,8305,7561,7511,7456,2249,3734,1134,1662,21,22,25,26,24,28,29])).
% 65.60/65.61 cnf(8684,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f7(a1,a1),a1)),
% 65.60/65.61 inference(scs_inference,[],[8658,8674,8492,3704,3734,22,21,25])).
% 65.60/65.61 cnf(8686,plain,
% 65.60/65.61 (P4(f6(a4),a1,a1)),
% 65.60/65.61 inference(scs_inference,[],[8658,8674,8678,8492,8112,3704,3734,22,21,25,26])).
% 65.60/65.61 cnf(8688,plain,
% 65.60/65.61 (~P2(f5(a4),f7(a4,a4),f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8658,8674,8578,8678,8492,8112,3704,7488,82,3734,22,21,25,26,24])).
% 65.60/65.61 cnf(8690,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f5(a1),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8658,8674,8578,8678,8672,8492,8303,8112,3704,7577,7488,82,3734,22,21,25,26,24,28])).
% 65.60/65.61 cnf(8692,plain,
% 65.60/65.61 (~P4(f6(a4),f7(a1,a1),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8658,8674,8578,8678,8672,8492,8303,8620,8112,3704,7577,7488,82,3734,22,21,25,26,24,28,8219])).
% 65.60/65.61 cnf(8699,plain,
% 65.60/65.61 (~P4(f7(a1,a1),f6(a4),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8624,8692,21,22])).
% 65.60/65.61 cnf(8701,plain,
% 65.60/65.61 (~P2(f5(a4),a1,f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8624,8692,8662,7476,3722,21,22,25])).
% 65.60/65.61 cnf(8703,plain,
% 65.60/65.61 (~P2(f5(a2),a2,f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8624,8692,8662,8091,7555,7476,3722,7511,21,22,25,24])).
% 65.60/65.61 cnf(8705,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f7(a4,a4),f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8624,8692,8688,8662,8091,8095,8425,7555,7476,3722,7511,3979,21,22,25,24,28])).
% 65.60/65.61 cnf(8707,plain,
% 65.60/65.61 (~P2(a1,a4,f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8664,8624,8692,8688,8662,8091,8095,8425,7460,7555,7476,3722,7511,7462,3979,2521,21,22,25,24,28,29])).
% 65.60/65.61 cnf(8709,plain,
% 65.60/65.61 (~P2(f6(a2),f3(a2,a2),a4)),
% 65.60/65.61 inference(scs_inference,[],[8664,8624,8692,8688,8662,8091,8095,8425,7460,7555,7476,3722,7511,7462,3979,2521,21,22,25,24,28,29,7738])).
% 65.60/65.61 cnf(8717,plain,
% 65.60/65.61 (~P2(f5(a2),f3(a2,a2),f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8705,8643,7523,7511,22,21,25])).
% 65.60/65.61 cnf(8719,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f3(a4,a4),f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8705,8643,8660,7523,8183,7511,22,21,25,27])).
% 65.60/65.61 cnf(8721,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f6(a2),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8705,8666,8643,8660,7523,8183,3704,7511,2151,22,21,25,27,24])).
% 65.60/65.61 cnf(8723,plain,
% 65.60/65.61 (~P4(f5(a1),a1,f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8705,8666,8643,8686,8333,8660,8244,7523,8183,3704,7511,2151,22,21,25,27,24,28])).
% 65.60/65.61 cnf(8725,plain,
% 65.60/65.61 (~P2(f5(a1),a4,f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8705,8666,8643,8668,8686,8333,8660,8244,7523,8183,8027,3704,7511,3821,2151,22,21,25,27,24,28,29])).
% 65.60/65.61 cnf(8734,plain,
% 65.60/65.61 (~P2(f7(a1,a1),a1,f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8709,8721,8690,4435,2330,21,22,25])).
% 65.60/65.61 cnf(8736,plain,
% 65.60/65.61 (P4(f3(a1,a1),f6(a4),a1)),
% 65.60/65.61 inference(scs_inference,[],[8709,8721,8690,8678,8016,4435,8037,2330,21,22,25,26])).
% 65.60/65.61 cnf(8738,plain,
% 65.60/65.61 (~P2(a2,f3(a4,a4),f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8709,8717,8721,8690,8678,8016,7480,4435,8037,7511,2330,21,22,25,26,24])).
% 65.60/65.61 cnf(8742,plain,
% 65.60/65.61 (~P4(f5(a1),a1,f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8709,8717,8721,8690,8409,8658,8686,8678,8062,8016,8244,8018,7480,4435,8037,3722,7511,2330,21,22,25,26,24,28,29])).
% 65.60/65.61 cnf(8746,plain,
% 65.60/65.61 (~P4(a1,f5(a1),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8723,22])).
% 65.60/65.61 cnf(8748,plain,
% 65.60/65.61 (~P2(a4,a1,f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8707,8723,22,21])).
% 65.60/65.61 cnf(8750,plain,
% 65.60/65.61 (~P2(f7(a1,a1),f5(a1),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8707,8701,8723,3716,7547,22,21,25])).
% 65.60/65.61 cnf(8752,plain,
% 65.60/65.61 (P2(f5(a1),f3(a2,a2),f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8707,8701,8723,7565,3716,7547,22,21,25,24])).
% 65.60/65.61 cnf(8754,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f5(a1),f5(a2))),
% 65.60/65.61 inference(scs_inference,[],[8707,8701,8723,7674,8672,7565,3716,7577,7547,22,21,25,24,28])).
% 65.60/65.61 cnf(8756,plain,
% 65.60/65.61 (~P2(f3(a4,a4),f3(a4,a4),f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8719,8707,8701,8723,7674,8672,8198,7565,3716,7577,7547,22,21,25,24,28,29])).
% 65.60/65.61 cnf(8760,plain,
% 65.60/65.61 (~P2(f6(a2),f5(a1),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8612,21])).
% 65.60/65.61 cnf(8764,plain,
% 65.60/65.61 (~P2(a4,f7(a4,a4),a4)),
% 65.60/65.61 inference(scs_inference,[],[8754,8612,8597,7517,7456,21,22,24])).
% 65.60/65.61 cnf(8766,plain,
% 65.60/65.61 (~P4(f5(a4),a2,f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[8754,8612,8597,7800,7676,7686,8427,7517,7456,21,22,24,28])).
% 65.60/65.61 cnf(8770,plain,
% 65.60/65.61 (~P4(a1,f6(a2),a1)),
% 65.60/65.61 inference(scs_inference,[],[8754,8612,8597,8703,8138,7800,7676,7523,7686,8427,7553,7517,7456,7462,4,21,22,24,28,25,29])).
% 65.60/65.61 cnf(8772,plain,
% 65.60/65.61 (~P4(f6(a2),a1,a1)),
% 65.60/65.61 inference(scs_inference,[],[8770,22])).
% 65.60/65.61 cnf(8774,plain,
% 65.60/65.61 (~P2(f5(a2),f6(a2),f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8770,8670,22,21])).
% 65.60/65.61 cnf(8776,plain,
% 65.60/65.61 (~P2(f7(a4,a4),f7(a1,a1),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8770,8670,8684,8425,7488,22,21,25])).
% 65.60/65.61 cnf(8778,plain,
% 65.60/65.61 (~P2(a1,f7(a2,a2),f5(a2))),
% 65.60/65.61 inference(scs_inference,[],[8770,8670,8684,7592,8425,7488,3698,22,21,25,24])).
% 65.60/65.61 cnf(8780,plain,
% 65.60/65.61 (~P4(f6(a2),f6(a4),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8770,8670,8684,8736,8554,7592,8425,7488,82,2151,3698,22,21,25,24,29])).
% 65.60/65.61 cnf(8784,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f5(a4),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8770,8670,8593,8684,8736,8554,8039,7592,8425,7488,82,2151,3698,22,21,25,24,29,3676,27])).
% 65.60/65.61 cnf(8788,plain,
% 65.60/65.61 (~P2(f7(a1,a1),f7(a4,a4),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8776,21])).
% 65.60/65.61 cnf(8792,plain,
% 65.60/65.61 (~P2(f5(a1),f5(a1),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8776,8784,8074,7547,21,22,25])).
% 65.60/65.61 cnf(8794,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f3(a4,a4),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8776,8784,8772,8074,8183,7547,21,22,25,27])).
% 65.60/65.61 cnf(8796,plain,
% 65.60/65.61 (~P2(a1,f3(a2,a2),a4)),
% 65.60/65.61 inference(scs_inference,[],[8776,8784,8772,8074,8707,7565,8183,7476,7547,21,22,25,27,24])).
% 65.60/65.61 cnf(8800,plain,
% 65.60/65.61 (P4(f3(a1,a1),a1,f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8776,8784,8652,8772,8074,8707,8736,8686,8656,7565,7655,8183,7476,7547,7563,1134,21,22,25,27,24,28,26])).
% 65.60/65.61 cnf(8809,plain,
% 65.60/65.61 (~P2(f5(a2),f3(a2,a2),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8734,8780,7961,7523,7511,22,21,25])).
% 65.60/65.61 cnf(8811,plain,
% 65.60/65.61 (~P4(a2,f6(a2),f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8734,8780,7961,8054,8641,7523,7573,7511,22,21,25,26])).
% 65.60/65.61 cnf(8813,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f7(a2,a2),f5(a2))),
% 65.60/65.61 inference(scs_inference,[],[8734,8778,8780,7961,8054,8641,7592,7523,7573,7561,7511,22,21,25,26,24])).
% 65.60/65.61 cnf(8815,plain,
% 65.60/65.61 (~P4(f6(a2),f6(a4),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8734,8778,8780,7961,8054,8641,8736,7592,7523,8305,7573,3704,7561,7511,22,21,25,26,24,28])).
% 65.60/65.61 cnf(8821,plain,
% 65.60/65.61 (~P2(f3(a2,a2),f5(a2),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8809,21])).
% 65.60/65.61 cnf(8829,plain,
% 65.60/65.61 (~P4(f3(a1,a1),a4,f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8788,8815,8809,8369,8586,8656,8194,8427,8425,3734,1134,21,22,25,24,28])).
% 65.60/65.61 cnf(8831,plain,
% 65.60/65.61 (~P2(a1,f7(a4,a4),a2)),
% 65.60/65.61 inference(scs_inference,[],[8788,8815,8809,8369,8167,8586,8656,8194,8427,8425,7474,7462,3734,2521,1134,21,22,25,24,28,29])).
% 65.60/65.61 cnf(8838,plain,
% 65.60/65.61 (~P2(a4,a1,f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8796,8829,8125,7462,7470,22,21,25])).
% 65.60/65.61 cnf(8840,plain,
% 65.60/65.61 (~P2(f7(a4,a4),f7(a2,a2),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8796,8829,8688,8125,7592,7488,7462,7470,22,21,25,24])).
% 65.60/65.61 cnf(8842,plain,
% 65.60/65.61 (~P4(f6(a4),f7(a2,a2),a4)),
% 65.60/65.61 inference(scs_inference,[],[8546,8796,8829,8688,8125,8194,7592,7684,7488,7462,7470,22,21,25,24,28])).
% 65.60/65.61 cnf(8844,plain,
% 65.60/65.61 (~P2(f5(a4),f3(a4,a4),f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8546,8796,8829,8688,8125,7704,7879,8194,7592,7684,8427,7488,7462,7470,3979,22,21,25,24,28,29])).
% 65.60/65.61 cnf(8848,plain,
% 65.60/65.61 (~P4(f6(a2),a2,f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8840,8811,21,22])).
% 65.60/65.61 cnf(8850,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f7(a4,a4),f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8840,8844,8811,8425,7577,21,22,24])).
% 65.60/65.61 cnf(8852,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f3(a1,a1),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[5,8840,8844,8811,8678,8656,8425,7577,21,22,24,28])).
% 65.60/65.61 cnf(8859,plain,
% 65.60/65.61 (~P2(f7(a4,a4),f3(a1,a1),f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8850,8842,22,21])).
% 65.60/65.61 cnf(8861,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f5(a4),f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8850,8610,8842,8039,8736,22,21,27])).
% 65.60/65.61 cnf(8863,plain,
% 65.60/65.61 (~P2(a1,f5(a1),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8850,8423,8610,8842,8039,8736,3712,1479,22,21,27,25])).
% 65.60/65.61 cnf(8877,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8813,8861,8829,8800,8678,21,22,27])).
% 65.60/65.61 cnf(8881,plain,
% 65.60/65.61 (~P2(f6(a2),a1,f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[7794,8240,8813,8861,8829,8800,7515,8678,8144,2151,21,22,27,26,25])).
% 65.60/65.61 cnf(8883,plain,
% 65.60/65.61 (~P2(a1,f6(a4),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[7794,8240,8813,8861,8863,8829,8800,7515,8678,8018,8144,7476,2151,21,22,27,26,25,24])).
% 65.60/65.61 cnf(8885,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f7(a4,a4),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[7794,8240,8813,8861,8863,8504,8829,8800,7515,7879,8678,8018,8144,7480,7494,7476,2151,21,22,27,26,25,24,28])).
% 65.60/65.61 cnf(8892,plain,
% 65.60/65.61 (~P2(f3(a4,a4),a2,f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[8885,8738,22,21])).
% 65.60/65.61 cnf(8894,plain,
% 65.60/65.61 (~P2(f6(a2),f5(a4),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8885,8738,8437,7456,3734,22,21,25])).
% 65.60/65.61 cnf(8896,plain,
% 65.60/65.61 (~P2(f5(a2),a2,a4)),
% 65.60/65.61 inference(scs_inference,[],[5,8885,8738,8437,7555,7456,7511,3734,22,21,25,24])).
% 65.60/65.61 cnf(8898,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f6(a4),a4)),
% 65.60/65.61 inference(scs_inference,[],[5,8885,8738,8437,7555,8037,7561,7456,7511,3734,22,21,25,24,28])).
% 65.60/65.61 cnf(8900,plain,
% 65.60/65.61 (~P4(f5(a4),f3(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[5,8877,8885,8738,8437,7730,8425,7555,3704,8037,7561,7456,7511,3734,22,21,25,24,28,29])).
% 65.60/65.61 cnf(8907,plain,
% 65.60/65.61 (P4(f3(a1,a1),f7(a4,a4),a1)),
% 65.60/65.61 inference(scs_inference,[],[8894,8898,8678,7498,7494,21,22,26])).
% 65.60/65.61 cnf(8909,plain,
% 65.60/65.61 (~P2(f5(a1),a2,f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8894,8898,8892,8752,8678,7523,7498,7494,21,22,26,25])).
% 65.60/65.61 cnf(8911,plain,
% 65.60/65.61 (~P2(f5(a4),f7(a4,a4),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8894,8229,8898,8892,8752,8678,7523,7498,7494,7488,3700,21,22,26,25,24])).
% 65.60/65.61 cnf(8913,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f3(a1,a1),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8852,8894,8229,8898,8892,8752,7590,8678,7523,7498,7494,7488,7470,3700,21,22,26,25,24,28])).
% 65.60/65.61 cnf(8915,plain,
% 65.60/65.61 (~P2(a1,f7(a1,a1),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8852,8894,8229,8898,8699,8892,8752,7590,8097,8678,7523,7498,7494,8037,7488,7470,2249,3700,21,22,26,25,24,28,29])).
% 65.60/65.61 cnf(8918,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f3(a4,a4),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8913,22])).
% 65.60/65.61 cnf(8922,plain,
% 65.60/65.61 (~P2(a1,f5(a1),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8913,8750,8760,4433,3734,22,21,25])).
% 65.60/65.61 cnf(8924,plain,
% 65.60/65.61 (~P2(a2,a2,a4)),
% 65.60/65.61 inference(scs_inference,[],[8913,8750,8760,8707,7523,7527,4433,3734,22,21,25,24])).
% 65.60/65.61 cnf(8926,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f7(a4,a4),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8913,8750,8760,8911,8707,8095,7523,8425,7527,4433,3979,3734,22,21,25,24,28])).
% 65.60/65.61 cnf(8935,plain,
% 65.60/65.61 (~P2(f5(a2),f3(a2,a2),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8926,7963,8517,7523,7511,21,22,25])).
% 65.60/65.61 cnf(8937,plain,
% 65.60/65.61 (~P2(f6(a2),a4,a1)),
% 65.60/65.61 inference(scs_inference,[],[5,8926,7963,8517,7523,7462,7511,4,21,22,25,24])).
% 65.60/65.61 cnf(8939,plain,
% 65.60/65.61 (~P4(f3(a4,a4),a4,a2)),
% 65.60/65.61 inference(scs_inference,[],[5,8926,7963,8517,8318,7575,7480,7523,7462,7511,2521,4,21,22,25,24,28])).
% 65.60/65.61 cnf(8944,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f5(a4),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8900,22])).
% 65.60/65.61 cnf(8948,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f5(a1),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8935,8900,8746,8907,8672,22,21,27])).
% 65.60/65.61 cnf(8950,plain,
% 65.60/65.61 (~P2(f6(a2),f7(a1,a1),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[8935,8900,8746,8907,8531,8672,3716,4433,22,21,27,25])).
% 65.60/65.61 cnf(8952,plain,
% 65.60/65.61 (~P2(f5(a1),f6(a2),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8935,8883,8900,8746,8907,8531,8672,3712,1479,3716,4433,22,21,27,25,24])).
% 65.60/65.61 cnf(8960,plain,
% 65.60/65.61 (~P4(a4,a4,f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8918,8935,8883,8900,8746,8907,8531,8672,8198,3712,1479,3716,8425,8427,4433,22,21,27,25,24,29,223,335,3662])).
% 65.60/65.61 cnf(8970,plain,
% 65.60/65.61 (~P2(a1,f7(a1,a1),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[8909,8948,8950,8815,8800,8736,3702,3734,22,21,27,25])).
% 65.60/65.61 cnf(8972,plain,
% 65.60/65.61 (~P2(f6(a2),f6(a4),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8909,8948,8950,8952,8815,8800,8736,8244,3712,3702,3734,22,21,27,25,24])).
% 65.60/65.61 cnf(8976,plain,
% 65.60/65.61 (P4(f3(a1,a1),f6(a2),x89761)+~P4(a1,f6(a2),x89761)),
% 65.60/65.61 inference(scs_inference,[],[5,8909,8948,8950,8952,8815,8907,8800,8641,8736,7565,8244,3712,7494,3702,3734,22,21,27,25,24,28,26])).
% 65.60/65.61 cnf(8980,plain,
% 65.60/65.61 (~P2(f5(a4),a4,f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8358,8742,22,21])).
% 65.60/65.61 cnf(8982,plain,
% 65.60/65.61 (~P4(a2,f7(a1,a1),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8358,8742,8815,7571,7472,22,21,26])).
% 65.60/65.61 cnf(8984,plain,
% 65.60/65.61 (~P2(a1,f3(a1,a1),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8358,8742,8161,8815,7571,7472,3704,2330,22,21,26,25])).
% 65.60/65.61 cnf(8986,plain,
% 65.60/65.61 (~P4(f5(a1),f6(a4),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8358,8742,8161,8367,8815,7571,7472,3704,8037,7547,3734,2330,22,21,26,25,29])).
% 65.60/65.61 cnf(8988,plain,
% 65.60/65.61 (~P4(f3(a4,a4),a2,a4)),
% 65.60/65.61 inference(scs_inference,[],[8924,8358,8742,8161,8367,8815,7571,7668,7472,3704,8037,7547,7470,3734,2330,22,21,26,25,29,28])).
% 65.60/65.61 cnf(8997,plain,
% 65.60/65.61 (~P2(f6(a2),f7(a1,a1),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8896,8982,8701,3716,4433,22,21,25])).
% 65.60/65.61 cnf(8999,plain,
% 65.60/65.61 (~P2(a2,a4,a2)),
% 65.60/65.61 inference(scs_inference,[],[8896,8982,8701,3716,7462,7511,4433,22,21,25,24])).
% 65.60/65.61 cnf(9001,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f5(a1),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8792,8896,8982,8701,8672,3716,7577,7462,7511,4433,22,21,25,24,28])).
% 65.60/65.61 cnf(9008,plain,
% 65.60/65.61 (~P2(a4,a2,a2)),
% 65.60/65.61 inference(scs_inference,[],[8999,9001,22,21])).
% 65.60/65.61 cnf(9010,plain,
% 65.60/65.61 (~P2(f5(a1),f5(a1),a2)),
% 65.60/65.61 inference(scs_inference,[],[30,8999,9001,7547,22,21,25])).
% 65.60/65.61 cnf(9012,plain,
% 65.60/65.61 (~P2(f7(a4,a4),f6(a4),a4)),
% 65.60/65.61 inference(scs_inference,[],[30,8999,9001,8980,8144,8425,7547,22,21,25,24])).
% 65.60/65.61 cnf(9014,plain,
% 65.60/65.61 (~P4(f7(a4,a4),f7(a4,a4),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[30,8999,8859,9001,8980,7879,8095,8144,8425,7547,7577,22,21,25,24,28])).
% 65.60/65.61 cnf(9023,plain,
% 65.60/65.61 (~P2(x90231,f7(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8972,8986,7967,4435,22,21,25])).
% 65.60/65.61 cnf(9025,plain,
% 65.60/65.61 (~P2(f3(a1,a1),a4,f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8179,8972,8986,7967,4435,7561,7462,22,21,25,24])).
% 65.60/65.61 cnf(9027,plain,
% 65.60/65.61 (~P2(f5(a4),f3(a4,a4),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9014,8179,8972,8986,7967,7879,4435,8427,7561,7462,3979,22,21,25,24,29])).
% 65.60/65.61 cnf(9029,plain,
% 65.60/65.61 (~P4(f5(a1),a1,a2)),
% 65.60/65.61 inference(scs_inference,[],[30,9014,8179,8972,8986,7967,8686,7879,8244,4435,8427,7561,7462,3979,22,21,25,24,29,28])).
% 65.60/65.61 cnf(9038,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f6(a2),a1)),
% 65.60/65.61 inference(scs_inference,[],[9029,8984,8150,8907,7573,22,21,27])).
% 65.60/65.61 cnf(9040,plain,
% 65.60/65.61 (~P2(f5(a4),f5(a4),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[9029,8984,9027,8150,8907,7573,8425,8427,22,21,27,25])).
% 65.60/65.61 cnf(9042,plain,
% 65.60/65.61 (~P2(a1,a2,f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[9029,9010,8984,9027,8150,8907,7573,8425,8427,7527,7547,22,21,27,25,24])).
% 65.60/65.61 cnf(9046,plain,
% 65.60/65.61 (~P2(f6(a2),f7(a4,a4),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[9008,9029,9010,8984,9027,8848,8150,8907,7686,7573,7472,8425,8427,7527,7547,7577,2330,22,21,27,25,24,29,28])).
% 65.60/65.61 cnf(9049,plain,
% 65.60/65.61 (~P4(f7(a4,a4),f6(a2),a1)),
% 65.60/65.61 inference(scs_inference,[],[9008,9029,9010,8984,9027,8848,8150,8907,7686,7573,7472,8425,8427,7527,7547,7577,2330,22,21,27,25,24,29,28,7579,8169])).
% 65.60/65.61 cnf(9058,plain,
% 65.60/65.61 (~P2(f7(a1,a1),x90581,f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9023,9038,22,21])).
% 65.60/65.61 cnf(9060,plain,
% 65.60/65.61 (~P4(f6(a4),f7(a4,a4),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9023,9038,8736,7494,22,21,26])).
% 65.60/65.61 cnf(9062,plain,
% 65.60/65.61 (~P2(a1,a2,f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[9023,9038,8831,8736,7527,7494,7476,22,21,26,24])).
% 65.60/65.61 cnf(9064,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f5(a1),a2)),
% 65.60/65.61 inference(scs_inference,[],[9023,9038,8831,9010,8672,8736,7527,7494,7476,7577,22,21,26,24,28])).
% 65.60/65.61 cnf(9076,plain,
% 65.60/65.61 (~P2(f6(a2),f5(a4),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8413,9060,9025,7456,3734,22,21,25])).
% 65.60/65.61 cnf(9078,plain,
% 65.60/65.61 (~P2(f6(a4),x90781,f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8413,9046,9060,9025,8194,7456,3734,22,21,25,24])).
% 65.60/65.61 cnf(9080,plain,
% 65.60/65.61 (~P4(f6(a4),f7(a2,a2),a1)),
% 65.60/65.61 inference(scs_inference,[],[30,8413,9046,9060,9025,8194,7684,7456,3734,22,21,25,24,28])).
% 65.60/65.61 cnf(9085,plain,
% 65.60/65.61 (~P4(f6(a2),f7(a4,a4),a1)),
% 65.60/65.61 inference(scs_inference,[],[9049,22])).
% 65.60/65.61 cnf(9089,plain,
% 65.60/65.61 (~P2(a1,f5(a4),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[9012,9078,9049,7517,8427,22,21,25])).
% 65.60/65.61 cnf(9092,plain,
% 65.60/65.61 (~P2(f3(a4,a4),f5(a4),a1)),
% 65.60/65.61 inference(scs_inference,[],[9012,9078,8534,9049,7517,8427,7488,22,21,25,24])).
% 65.60/65.61 cnf(9096,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f7(a2,a2),a1)),
% 65.60/65.61 inference(scs_inference,[],[30,9012,9078,8534,9049,8939,8656,7684,7517,3704,8427,7488,7577,22,21,25,24,29,28])).
% 65.60/65.61 cnf(9102,plain,
% 65.60/65.61 (~P2(a1,f6(a4),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[9096,8997,9089,8018,7476,22,21,24])).
% 65.60/65.61 cnf(9104,plain,
% 65.60/65.61 (~P4(f5(a4),f6(a2),a1)),
% 65.60/65.61 inference(scs_inference,[],[9096,8997,9089,9038,8641,8018,8425,7476,4,22,21,24,29])).
% 65.60/65.61 cnf(9106,plain,
% 65.60/65.61 (~P2(f5(a1),f7(a4,a4),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[9096,8997,8725,9089,9038,8641,7484,8656,8018,8425,7476,3821,4,22,21,24,29,28])).
% 65.60/65.61 cnf(9114,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f6(a2),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[9080,9106,8433,8907,7573,22,21,27])).
% 65.60/65.61 cnf(9116,plain,
% 65.60/65.61 (~P2(f5(a2),f3(a2,a2),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[9080,9106,9062,8433,8907,7523,7573,7511,22,21,27,25])).
% 65.60/65.61 cnf(9118,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f5(a1),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8922,9080,9106,9062,8433,8907,7523,7573,1479,7561,7511,22,21,27,25,24])).
% 65.60/65.61 cnf(9120,plain,
% 65.60/65.61 (~P2(f5(a4),f6(a4),a4)),
% 65.60/65.61 inference(scs_inference,[],[8922,9080,9106,9062,8898,8433,8907,8080,8056,7523,7573,1479,8425,7561,7511,22,21,27,25,24,29])).
% 65.60/65.61 cnf(9124,plain,
% 65.60/65.61 (~P4(a1,f6(a2),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[8922,9080,9106,9062,8335,8898,8433,8907,8215,8080,8056,7523,7573,1479,8425,7561,7511,7577,22,21,27,25,24,29,28,8976])).
% 65.60/65.61 cnf(9132,plain,
% 65.60/65.61 (~P2(f5(a4),f6(a2),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9076,9114,22,21])).
% 65.60/65.61 cnf(9134,plain,
% 65.60/65.61 (~P2(f7(a1,a1),f5(a2),f5(a2))),
% 65.60/65.61 inference(scs_inference,[],[9076,9114,8523,3716,7511,22,21,25])).
% 65.60/65.61 cnf(9148,plain,
% 65.60/65.61 (~P2(f7(a4,a4),f3(a4,a4),f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[9116,9064,8844,7480,7488,22,21,24])).
% 65.60/65.61 cnf(9150,plain,
% 65.60/65.61 (~P4(f5(a4),f7(a2,a2),a1)),
% 65.60/65.61 inference(scs_inference,[],[9116,9064,7806,8844,7696,7592,7480,7488,22,21,24,29])).
% 65.60/65.61 cnf(9152,plain,
% 65.60/65.61 (~P4(a1,f6(a4),a2)),
% 65.60/65.61 inference(scs_inference,[],[30,9116,9064,7806,8844,7696,7592,7480,8037,7488,7476,22,21,24,29,28])).
% 65.60/65.61 cnf(9160,plain,
% 65.60/65.61 (P2(f3(a1,a1),f3(a2,a2),f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[9148,9104,7565,7561,22,21,25])).
% 65.60/65.61 cnf(9162,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f7(a1,a1),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[9148,8970,9104,7565,7561,2249,22,21,25,24])).
% 65.60/65.61 cnf(9164,plain,
% 65.60/65.61 (~P4(f5(a1),a1,f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9148,8970,9104,8266,8686,7565,8244,7561,2249,3734,22,21,25,24,29])).
% 65.60/65.61 cnf(9171,plain,
% 65.60/65.61 (~P2(f6(a2),a4,f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[9164,8443,22,21])).
% 65.60/65.61 cnf(9173,plain,
% 65.60/65.61 (~P2(f3(a2,a2),f5(a2),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9160,9164,8821,8443,2151,22,21,25])).
% 65.60/65.61 cnf(9177,plain,
% 65.60/65.61 (~P2(a1,f7(a4,a4),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9160,9164,8821,8443,7708,9014,8095,8425,7517,7494,7488,2151,22,21,25,24,29])).
% 65.60/65.61 cnf(9179,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f3(a1,a1),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[9160,9164,8821,8443,7708,9014,7992,8907,8095,8425,7517,7494,7488,3979,2151,22,21,25,24,29,28])).
% 65.60/65.61 cnf(9183,plain,
% 65.60/65.61 (~P2(f5(a4),f3(a4,a4),a1)),
% 65.60/65.61 inference(scs_inference,[],[9092,9124,22,21])).
% 65.60/65.61 cnf(9185,plain,
% 65.60/65.61 (~P2(f5(a2),f3(a2,a2),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[9092,9124,9042,7523,7511,22,21,25])).
% 65.60/65.61 cnf(9187,plain,
% 65.60/65.61 (P2(f6(a2),f3(a2,a2),f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[9092,9124,9042,9160,7523,3704,7511,22,21,25,24])).
% 65.60/65.61 cnf(9189,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f3(a1,a1),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[9179,9092,9124,9042,9160,7730,7523,3704,7577,7511,22,21,25,24,28])).
% 65.60/65.61 cnf(9198,plain,
% 65.60/65.61 (~P2(f7(a1,a1),f3(a1,a1),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[9162,9189,22,21])).
% 65.60/65.61 cnf(9200,plain,
% 65.60/65.61 (~P2(f6(a2),a2,f3(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[9162,9187,9189,8892,7523,22,21,25])).
% 65.60/65.61 cnf(9202,plain,
% 65.60/65.61 (~P2(a1,f5(a4),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[8915,9162,9187,9189,8892,7523,7476,82,22,21,25,24])).
% 65.60/65.61 cnf(9204,plain,
% 65.60/65.61 (~P4(f7(a1,a1),f7(a2,a2),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[32,8915,9162,9187,9189,8892,7684,4435,7523,7476,82,22,21,25,24,28])).
% 65.60/65.61 cnf(9214,plain,
% 65.60/65.61 (~P2(f6(a2),f3(a1,a1),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[9118,9204,9132,3704,2151,22,21,25])).
% 65.60/65.61 cnf(9218,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f3(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8838,9085,9118,9204,9132,8907,3704,7547,7476,2151,3734,22,21,25,24,29])).
% 65.60/65.61 cnf(9222,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f3(a2,a2),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8838,9085,9118,9204,9102,9132,8650,7802,8062,8907,8736,8144,3704,7547,7476,2151,3734,22,21,25,24,29,28,27])).
% 65.60/65.61 cnf(9228,plain,
% 65.60/65.61 (~P2(f5(a1),f5(a4),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9222,9120,8937,7456,7547,22,21,25])).
% 65.60/65.61 cnf(9234,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f3(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8960,9218,9222,9120,8937,8980,7590,8018,7460,7456,7547,7462,7470,2521,22,21,25,24,29,28])).
% 65.60/65.61 cnf(9236,plain,
% 65.60/65.61 (~P4(f3(a4,a4),f6(a4),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[8960,9218,9222,9120,8937,8980,8540,7590,8686,8200,8018,7460,7456,7547,7462,7470,2521,22,21,25,24,29,28,27])).
% 65.60/65.61 cnf(9242,plain,
% 65.60/65.61 (~P2(f7(a1,a1),f5(a2),a1)),
% 65.60/65.61 inference(scs_inference,[],[9236,8881,8517,3716,7511,22,21,25])).
% 65.60/65.61 cnf(9246,plain,
% 65.60/65.61 (~P2(f3(a1,a1),a1,f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9236,8881,9183,8490,8517,8305,3716,8425,8037,7577,7511,2150,22,21,25,24,29])).
% 65.60/65.61 cnf(9248,plain,
% 65.60/65.61 (~P2(f6(a4),f7(a4,a4),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[8764,9236,8881,9183,8490,8517,7484,8305,8027,3716,8425,8037,7577,7511,2150,22,21,25,24,29,28])).
% 65.60/65.61 cnf(9257,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f5(a4),a1)),
% 65.60/65.61 inference(scs_inference,[],[9234,9200,9177,7488,2150,22,21,25])).
% 65.60/65.61 cnf(9259,plain,
% 65.60/65.61 (~P2(f5(a4),f7(a4,a4),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[9234,9200,9177,8425,7488,82,2150,22,21,25,24])).
% 65.60/65.61 cnf(9261,plain,
% 65.60/65.61 (~P4(f5(a1),f7(a2,a2),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[32,9234,9200,9177,3712,7684,8425,7488,82,2150,22,21,25,24,28])).
% 65.60/65.61 cnf(9269,plain,
% 65.60/65.61 (~P2(f7(a4,a4),f6(a4),f6(a4))),
% 65.60/65.61 inference(scs_inference,[],[9248,9261,22,21])).
% 65.60/65.61 cnf(9271,plain,
% 65.60/65.61 (P4(a4,f7(a4,a4),a4)),
% 65.60/65.61 inference(scs_inference,[],[9248,9261,8656,7474,22,21,26])).
% 65.60/65.61 cnf(9273,plain,
% 65.60/65.61 (~P2(a1,f3(a1,a1),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[9248,9214,9261,8656,7474,3704,2330,22,21,26,25])).
% 65.60/65.61 cnf(9279,plain,
% 65.60/65.61 (~P4(a1,f6(a2),f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[7973,8794,9248,9214,9261,8707,8752,8198,8641,8656,7474,1479,7517,3704,7577,2330,22,21,26,25,24,29,28])).
% 65.60/65.61 cnf(9281,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f7(a1,a1),x92811)+P4(f7(a1,a1),a1,x92811)),
% 65.60/65.61 inference(scs_inference,[],[7973,8794,9248,9214,9261,8707,8800,8752,8198,8641,8656,7474,1479,7517,3704,7563,7577,2330,22,21,26,25,24,29,28,27])).
% 65.60/65.61 cnf(9287,plain,
% 65.60/65.61 (~P4(f6(a4),f7(a4,a4),f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[9259,9150,9096,8736,7494,22,21,26])).
% 65.60/65.61 cnf(9289,plain,
% 65.60/65.61 (~P2(f5(a1),f5(a4),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[9259,9150,9096,8320,8736,3757,7494,7456,22,21,26,25])).
% 65.60/65.61 cnf(9291,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f5(a4),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9202,9259,9150,9096,8320,8736,3757,7494,7561,7456,82,22,21,26,25,24])).
% 65.60/65.61 cnf(9297,plain,
% 65.60/65.61 (P4(a1,f6(a4),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9202,9259,9150,9040,9096,8320,8016,8678,8305,8736,3980,3757,7494,7561,7456,82,7577,22,21,26,25,24,28,367,27])).
% 65.60/65.61 cnf(9299,plain,
% 65.60/65.61 (~P2(f5(a4),f6(a4),a2)),
% 65.60/65.61 inference(scs_inference,[],[9202,9259,9150,9152,9040,9096,8320,8016,8678,8305,8736,3980,8056,3757,7494,7561,7456,82,7577,22,21,26,25,24,28,367,27,29])).
% 65.60/65.61 cnf(9307,plain,
% 65.60/65.61 (~P4(a1,f5(a4),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[8988,9291,8944,9297,8039,22,21,27])).
% 65.60/65.61 cnf(9313,plain,
% 65.60/65.61 (~P4(f3(a1,a1),f6(a4),a2)),
% 65.60/65.61 inference(scs_inference,[],[8988,9291,8944,9269,9297,9299,8756,9187,8039,8080,8244,8056,8425,22,21,27,24,25,28])).
% 65.60/65.61 cnf(9322,plain,
% 65.60/65.61 (P4(f5(a1),f7(a4,a4),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[9287,9134,9271,3821,22,21,27])).
% 65.60/65.61 cnf(9324,plain,
% 65.60/65.61 (~P2(f7(a4,a4),a1,f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9287,9134,9271,8850,7517,3821,7577,22,21,27,25])).
% 65.60/65.61 cnf(9326,plain,
% 65.60/65.61 (~P2(f3(a1,a1),f6(a4),a4)),
% 65.60/65.61 inference(scs_inference,[],[9287,9134,9171,9271,8850,8144,7517,3704,3821,7577,22,21,27,25,24])).
% 65.60/65.61 cnf(9328,plain,
% 65.60/65.61 (~P2(a4,f5(a4),a4)),
% 65.60/65.61 inference(scs_inference,[],[7610,9287,9134,9171,9271,8850,7498,8144,7517,3704,3821,7577,3979,22,21,27,25,24,28])).
% 65.60/65.61 cnf(9337,plain,
% 65.60/65.61 (~P4(a2,f7(a4,a4),f3(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[9328,9307,7767,7686,7525,22,21,27])).
% 65.60/65.61 cnf(9345,plain,
% 65.60/65.61 (~P4(f7(a1,a1),f6(a4),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[9198,9328,9273,9307,9313,9297,9160,8892,7767,8097,7686,7525,7523,3716,7561,22,21,27,25,24,29,28])).
% 65.60/65.61 cnf(9357,plain,
% 65.60/65.61 (~P4(f5(a1),f7(a4,a4),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9322,9345,9228,9324,8348,8922,9297,8800,8056,1479,3722,7494,8425,7488,22,21,27,24,29,28])).
% 65.60/65.61 cnf(9361,plain,
% 65.60/65.61 (P4(f3(a1,a1),f3(a1,a1),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9322,9345,9228,9324,8348,8922,8748,9187,9297,8800,8097,8056,1479,3722,7494,8425,7488,22,21,27,24,29,28,25,26])).
% 65.60/65.61 cnf(9368,plain,
% 65.60/65.61 (P4(a1,f3(a1,a1),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9361,9289,9357,8112,9297,22,21,26])).
% 65.60/65.61 cnf(9374,plain,
% 65.60/65.61 (~P2(f7(a1,a1),f3(a1,a1),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[9361,9289,9357,8562,9326,8511,8112,9297,8018,8144,7561,4,22,21,26,25,24,29])).
% 65.60/65.61 cnf(9385,plain,
% 65.60/65.61 (~P4(f5(a1),f6(a2),f5(a4))),
% 65.60/65.61 inference(scs_inference,[],[9242,9337,8766,9322,7573,22,21,27])).
% 65.60/65.61 cnf(9414,plain,
% 65.60/65.61 (P2(f5(a1),f7(a2,a2),f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[9185,9279,8110,7592,7547,82,22,21,25,24])).
% 65.60/65.61 cnf(9418,plain,
% 65.60/65.61 (~P4(f7(a4,a4),f3(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9185,9058,9279,9368,8842,8110,8163,7730,7592,8194,7684,7517,7547,82,22,21,25,24,29,28])).
% 65.60/65.61 cnf(9425,plain,
% 65.60/65.61 (~P2(f5(a1),f5(a1),f7(a2,a2))),
% 65.60/65.61 inference(scs_inference,[],[9374,9418,9414,7765,22,21,25])).
% 65.60/65.61 cnf(9438,plain,
% 65.60/65.61 (~P2(a1,f3(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9246,9385,22,21])).
% 65.60/65.61 cnf(9440,plain,
% 65.60/65.61 (P4(f3(a4,a4),f7(a1,a1),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9246,9385,9368,8183,22,21,26])).
% 65.60/65.61 cnf(9442,plain,
% 65.60/65.61 (~P2(f6(a2),f7(a2,a2),f5(a1))),
% 65.60/65.61 inference(scs_inference,[],[9246,9425,9385,9414,9368,8183,3712,22,21,26,24])).
% 65.60/65.61 cnf(9444,plain,
% 65.60/65.61 (~P4(f7(a2,a2),f7(a4,a4),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[9246,9425,9385,9106,9414,9368,9322,8183,3712,22,21,26,24,28])).
% 65.60/65.61 cnf(9448,plain,
% 65.60/65.61 (~P4(a1,f7(a1,a1),x94481)+P4(f7(a1,a1),f3(a1,a1),x94481)),
% 65.60/65.61 inference(scs_inference,[],[8774,9246,9425,9385,9106,9414,9361,9368,9322,8183,3712,22,21,26,24,28,25,27])).
% 65.60/65.61 cnf(9454,plain,
% 65.60/65.61 (P4(f7(a1,a1),f3(a1,a1),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9440,9444,9257,9368,8200,22,21,27])).
% 65.60/65.61 cnf(9460,plain,
% 65.60/65.61 (~P4(f7(a1,a1),f3(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9440,9444,9257,9442,8482,9023,9368,8200,3716,7517,7577,3702,3734,22,21,27,25,24,28])).
% 65.60/65.61 cnf(9463,plain,
% 65.60/65.61 (~P4(a1,f7(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9440,9444,9257,9442,8482,9023,9368,8200,3716,7517,7577,3702,3734,22,21,27,25,24,28,9448])).
% 65.60/65.61 cnf(9465,plain,
% 65.60/65.61 (~P4(a2,f7(a2,a2),a2)),
% 65.60/65.61 inference(scs_inference,[],[9440,9444,9257,9442,8482,9023,9368,8200,3716,7517,7577,3702,3734,22,21,27,25,24,28,9448,8256])).
% 65.60/65.61 cnf(9469,plain,
% 65.60/65.61 (~P4(f6(a2),f6(a4),a2)),
% 65.60/65.61 inference(scs_inference,[],[9440,9444,9257,9442,8482,9023,9222,9368,7612,8200,3716,7517,7577,3702,3734,22,21,27,25,24,28,9448,8256,29,8377])).
% 65.60/65.61 cnf(9477,plain,
% 65.60/65.61 (~P2(a1,f6(a2),f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9173,9438,9460,9465,7684,7476,2330,22,21,27,24])).
% 65.60/65.61 cnf(9487,plain,
% 65.60/65.61 (~P2(f6(a2),a1,f3(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9477,9463,22,21])).
% 65.60/65.61 cnf(9491,plain,
% 65.60/65.61 (~P2(f6(a2),f3(a1,a1),a1)),
% 65.60/65.61 inference(scs_inference,[],[9477,9463,9454,9460,9361,3704,2151,22,21,27,25])).
% 65.60/65.61 cnf(9493,plain,
% 65.60/65.61 (~P2(f6(a2),f3(a1,a1),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[9477,9463,9454,9460,9361,3704,2151,2330,22,21,27,25,24])).
% 65.60/65.61 cnf(9497,plain,
% 65.60/65.61 (~P4(f3(a2,a2),f7(a2,a2),f6(a2))),
% 65.60/65.61 inference(scs_inference,[],[41,9477,9463,9454,9080,9460,9361,9187,8163,8194,7684,3704,2151,2330,22,21,27,25,24,29,28])).
% 65.60/65.61 cnf(9510,plain,
% 65.60/65.61 (~P2(f7(a1,a1),f3(a1,a1),f7(a4,a4))),
% 65.60/65.61 inference(scs_inference,[],[9493,9497,9491,8314,9299,9440,8540,9368,8200,8112,8018,7527,3704,7488,2330,22,21,27,25,24,29])).
% 65.60/65.61 cnf(9512,plain,
% 65.60/65.61 (P4(f3(a1,a1),f7(a1,a1),f7(a1,a1))),
% 65.60/65.61 inference(scs_inference,[],[9493,9497,9491,8314,9299,9454,9440,8540,9361,9368,8200,8112,8018,7527,3704,7488,2330,22,21,27,25,24,29,26])).
% 65.60/65.61 cnf(9527,plain,
% 65.60/65.61 ($false),
% 65.60/65.61 inference(scs_inference,[],[9510,9512,9487,9469,9454,9361,3704,7561,3734,9281,22,21,26,25]),
% 65.60/65.61 ['proof']).
% 65.60/65.61 % SZS output end Proof
% 65.60/65.61 % Total time :64.870000s
%------------------------------------------------------------------------------