%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD031-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 05:55:19 EDT 2024
% Result : Unsatisfiable 71.65s 71.73s
% Output : CNFRefutation 71.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : FLD031-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n025.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:01:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.45/0.57 start to proof:theBenchmark
% 71.62/71.72 %-------------------------------------------
% 71.62/71.72 % File :CSE---1.7
% 71.62/71.72 % Problem :theBenchmark
% 71.62/71.72 % Transform :cnf
% 71.62/71.72 % Format :tptp:raw
% 71.62/71.72 % Command :java -jar mcs_scs.jar %d %s
% 71.62/71.72
% 71.62/71.72 % Result :Theorem 71.060000s
% 71.62/71.72 % Output :CNFRefutation 71.060000s
% 71.62/71.72 %-------------------------------------------
% 71.65/71.73 %--------------------------------------------------------------------------
% 71.65/71.73 % File : FLD031-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 71.65/71.73 % Domain : Field Theory (Ordered fields)
% 71.65/71.73 % Problem : If a is one, then the multiplicative inverse of a is also one
% 71.65/71.73 % Version : [Dra93] axioms : Especial.
% 71.65/71.73 % Theorem formulation : Functional with re axiom set.
% 71.65/71.73 % English :
% 71.65/71.73
% 71.65/71.73 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 71.65/71.73 % Source : [Dra93]
% 71.65/71.73 % Names :
% 71.65/71.73
% 71.65/71.73 % Status : Unsatisfiable
% 71.65/71.73 % Rating : 0.00 v7.0.0, 0.12 v6.3.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.10 v5.2.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.00 v2.4.0, 0.00 v2.2.1, 0.33 v2.1.0
% 71.65/71.73 % Syntax : Number of clauses : 30 ( 7 unt; 3 nHn; 30 RR)
% 71.65/71.73 % Number of literals : 81 ( 0 equ; 51 neg)
% 71.65/71.73 % Maximal clause size : 5 ( 2 avg)
% 71.65/71.73 % Maximal term depth : 2 ( 1 avg)
% 71.65/71.73 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 71.65/71.73 % Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% 71.65/71.73 % Number of variables : 73 ( 0 sgn)
% 71.65/71.73 % SPC : CNF_UNS_RFO_NEQ_NHN
% 71.65/71.73
% 71.65/71.73 % Comments :
% 71.65/71.73 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 71.65/71.73 %--------------------------------------------------------------------------
% 71.65/71.73 include('Axioms/FLD002-0.ax').
% 71.65/71.73 %--------------------------------------------------------------------------
% 71.65/71.73 cnf(a_is_defined,hypothesis,
% 71.65/71.73 defined(a) ).
% 71.65/71.73
% 71.65/71.73 cnf(product_2,negated_conjecture,
% 71.65/71.73 product(multiplicative_identity,a,multiplicative_identity) ).
% 71.65/71.73
% 71.65/71.73 cnf(not_sum_3,negated_conjecture,
% 71.65/71.73 ~ sum(additive_identity,a,additive_identity) ).
% 71.65/71.73
% 71.65/71.73 cnf(not_product_4,negated_conjecture,
% 71.65/71.73 ~ product(multiplicative_identity,multiplicative_inverse(a),multiplicative_identity) ).
% 71.65/71.73
% 71.65/71.73 %--------------------------------------------------------------------------
% 71.65/71.73 %-------------------------------------------
% 71.65/71.73 % Proof found
% 71.65/71.73 % SZS status Theorem for theBenchmark
% 71.65/71.73 % SZS output start Proof
% 71.66/71.74 %ClaNum:30(EqnAxiom:0)
% 71.66/71.74 %VarNum:162(SingletonVarNum:73)
% 71.66/71.74 %MaxLitNum:5
% 71.66/71.74 %MaxfuncDepth:1
% 71.66/71.74 %SharedTerms:11
% 71.66/71.74 %goalClause: 4 6 7
% 71.66/71.74 %singleGoalClaCount:3
% 71.66/71.74 [1]P1(a1)
% 71.66/71.74 [2]P1(a4)
% 71.66/71.74 [3]P1(a2)
% 71.66/71.74 [4]P2(a4,a2,a4)
% 71.66/71.74 [5]~P4(a1,a1,a4)
% 71.66/71.74 [6]~P4(a1,a2,a1)
% 71.66/71.74 [7]~P2(a4,f6(a2),a4)
% 71.66/71.74 [13]~P1(x131)+P4(a1,x131,x131)
% 71.66/71.74 [14]~P1(x141)+P2(a4,x141,x141)
% 71.66/71.74 [8]~P1(x81)+P1(f5(x81))
% 71.66/71.74 [15]~P1(x151)+P4(f5(x151),x151,a1)
% 71.66/71.74 [22]~P4(x222,x221,x223)+P4(x221,x222,x223)
% 71.66/71.74 [23]~P2(x232,x231,x233)+P2(x231,x232,x233)
% 71.66/71.74 [16]~P1(x161)+P4(a1,x161,a1)+P1(f6(x161))
% 71.66/71.74 [20]~P1(x201)+P2(f6(x201),x201,a4)+P4(a1,x201,a1)
% 71.66/71.74 [19]~P3(x192,x191)+~P3(x191,x192)+P4(a1,x191,x192)
% 71.66/71.74 [10]~P1(x102)+~P1(x101)+P1(f3(x101,x102))
% 71.66/71.74 [11]~P1(x112)+~P1(x111)+P1(f7(x111,x112))
% 71.66/71.74 [17]~P1(x172)+~P1(x171)+P4(x171,x172,f3(x171,x172))
% 71.66/71.74 [18]~P1(x182)+~P1(x181)+P2(x181,x182,f7(x181,x182))
% 71.66/71.74 [12]~P3(x121,x123)+P3(x121,x122)+~P3(x123,x122)
% 71.66/71.74 [9]P3(x92,x91)+~P1(x91)+~P1(x92)+P3(x91,x92)
% 71.66/71.74 [21]~P2(x213,x212,x211)+P3(a1,x211)+~P3(a1,x212)+~P3(a1,x213)
% 71.66/71.74 [24]~P4(x243,x245,x241)+P3(x241,x242)+~P4(x244,x245,x242)+~P3(x243,x244)
% 71.66/71.74 [25]~P4(x251,x256,x254)+P4(x251,x252,x253)+~P4(x254,x255,x253)+~P4(x256,x255,x252)
% 71.66/71.74 [26]~P4(x266,x264,x261)+P4(x261,x262,x263)+~P4(x264,x262,x265)+~P4(x266,x265,x263)
% 71.66/71.74 [27]~P2(x271,x276,x274)+P2(x271,x272,x273)+~P2(x274,x275,x273)+~P2(x276,x275,x272)
% 71.66/71.74 [28]~P2(x286,x284,x281)+P2(x281,x282,x283)+~P2(x284,x282,x285)+~P2(x286,x285,x283)
% 71.66/71.74 [29]~P2(x295,x297,x292)+~P2(x294,x297,x291)+P4(x291,x292,x293)+~P4(x294,x295,x296)+~P2(x296,x297,x293)
% 71.66/71.74 [30]~P2(x307,x302,x305)+~P2(x306,x302,x304)+P2(x301,x302,x303)+~P4(x304,x305,x303)+~P4(x306,x307,x301)
% 71.66/71.74 %EqnAxiom
% 71.66/71.74
% 71.66/71.74 %-------------------------------------------
% 71.66/71.76 cnf(31,plain,
% 71.66/71.76 (~P2(f6(a2),a4,a4)),
% 71.66/71.76 inference(scs_inference,[],[7,23])).
% 71.66/71.76 cnf(33,plain,
% 71.66/71.76 (~P4(a2,a1,a1)),
% 71.66/71.76 inference(scs_inference,[],[6,7,23,22])).
% 71.66/71.76 cnf(35,plain,
% 71.66/71.76 (~P2(a2,f6(a2),a2)),
% 71.66/71.76 inference(scs_inference,[],[4,6,7,23,22,28])).
% 71.66/71.76 cnf(37,plain,
% 71.66/71.76 (P3(a1,a1)),
% 71.66/71.76 inference(scs_inference,[],[4,6,7,1,23,22,28,9])).
% 71.66/71.76 cnf(39,plain,
% 71.66/71.76 (~P3(a2,a1)+~P3(a1,a2)),
% 71.66/71.76 inference(scs_inference,[],[4,6,7,1,23,22,28,9,19])).
% 71.66/71.76 cnf(42,plain,
% 71.66/71.76 (~P2(f6(a2),a2,a2)),
% 71.66/71.76 inference(scs_inference,[],[35,23])).
% 71.66/71.76 cnf(44,plain,
% 71.66/71.76 (P3(a4,a4)),
% 71.66/71.76 inference(scs_inference,[],[35,2,23,9])).
% 71.66/71.76 cnf(51,plain,
% 71.66/71.76 (P3(a2,a2)),
% 71.66/71.76 inference(scs_inference,[],[3,9])).
% 71.66/71.76 cnf(53,plain,
% 71.66/71.76 (~P4(a4,x531,x532)+~P4(a4,x531,x533)+P3(x532,x533)),
% 71.66/71.76 inference(scs_inference,[],[3,44,9,24])).
% 71.66/71.76 cnf(54,plain,
% 71.66/71.76 (~P4(a2,x541,x542)+~P4(a2,x541,x543)+P3(x542,x543)),
% 71.66/71.76 inference(scs_inference,[],[51,24])).
% 71.66/71.76 cnf(59,plain,
% 71.66/71.76 (~P4(a1,x591,x592)+~P4(a1,x591,x593)+P3(x592,x593)),
% 71.66/71.76 inference(scs_inference,[],[37,24])).
% 71.66/71.76 cnf(115,plain,
% 71.66/71.76 (~P3(a2,a1)+~P4(a4,x1151,a1)+~P4(a4,x1151,a2)),
% 71.66/71.76 inference(scs_inference,[],[39,53])).
% 71.66/71.76 cnf(147,plain,
% 71.66/71.76 (P4(f5(f5(a4)),f5(a4),a1)),
% 71.66/71.76 inference(scs_inference,[],[2,15,8])).
% 71.66/71.76 cnf(148,plain,
% 71.66/71.76 (~P4(f5(a4),a2,f5(a4))),
% 71.66/71.76 inference(scs_inference,[],[6,147,26])).
% 71.66/71.76 cnf(150,plain,
% 71.66/71.76 (~P4(a2,f5(a4),f5(a4))),
% 71.66/71.76 inference(scs_inference,[],[6,147,26,22])).
% 71.66/71.76 cnf(608,plain,
% 71.66/71.76 (P4(a1,f5(a4),f5(a4))),
% 71.66/71.76 inference(scs_inference,[],[2,8,13])).
% 71.66/71.76 cnf(659,plain,
% 71.66/71.76 (P4(a1,f5(a2),f5(a2))),
% 71.66/71.76 inference(scs_inference,[],[3,8,13])).
% 71.66/71.76 cnf(1375,plain,
% 71.66/71.76 (P4(a1,f5(a1),f5(a1))),
% 71.66/71.76 inference(scs_inference,[],[1,8,13])).
% 71.66/71.76 cnf(1571,plain,
% 71.66/71.76 (P2(a4,f5(a1),f5(a1))),
% 71.66/71.76 inference(scs_inference,[],[1,8,14])).
% 71.66/71.76 cnf(1575,plain,
% 71.66/71.76 (~P2(x15751,a4,a4)+P2(x15751,f5(a1),f5(a1))),
% 71.66/71.76 inference(scs_inference,[],[1571,27])).
% 71.66/71.76 cnf(1593,plain,
% 71.66/71.76 (P2(f5(a1),x15931,f5(a1))+~P2(x15931,a4,a4)),
% 71.66/71.76 inference(scs_inference,[],[1575,23])).
% 71.66/71.76 cnf(1883,plain,
% 71.66/71.76 (P4(f5(f5(a1)),f5(a1),a1)),
% 71.66/71.76 inference(scs_inference,[],[1,8,15])).
% 71.66/71.76 cnf(1952,plain,
% 71.66/71.76 (~P4(a2,f5(a1),f5(a1))),
% 71.66/71.76 inference(scs_inference,[],[6,1883,26,22])).
% 71.66/71.76 cnf(2032,plain,
% 71.66/71.77 (P2(a4,f5(a4),f5(a4))),
% 71.66/71.77 inference(scs_inference,[],[2,8,14])).
% 71.66/71.77 cnf(2033,plain,
% 71.66/71.77 (~P2(x20331,a4,a4)+P2(x20331,f5(a4),f5(a4))),
% 71.66/71.77 inference(scs_inference,[],[2032,27])).
% 71.66/71.77 cnf(2058,plain,
% 71.66/71.77 (P2(f5(a4),x20581,f5(a4))+~P2(x20581,a4,a4)),
% 71.66/71.77 inference(scs_inference,[],[2033,23])).
% 71.66/71.77 cnf(2106,plain,
% 71.66/71.77 (P2(f5(a4),a2,f5(a4))+~P2(a4,a4,a4)),
% 71.66/71.77 inference(scs_inference,[],[4,2058,28])).
% 71.66/71.77 cnf(2138,plain,
% 71.66/71.77 (P2(f5(a4),a2,f5(a4))),
% 71.66/71.77 inference(scs_inference,[],[2,2106,14])).
% 71.66/71.77 cnf(2534,plain,
% 71.66/71.77 (P2(a4,f5(a2),f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[3,8,14])).
% 71.66/71.77 cnf(2535,plain,
% 71.66/71.77 (~P2(x25351,a4,a4)+P2(x25351,f5(a2),f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[2534,27])).
% 71.66/71.77 cnf(2537,plain,
% 71.66/71.77 (~P2(a4,a4,x25371)+P2(x25371,f5(a2),f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[2534,27,28])).
% 71.66/71.77 cnf(2573,plain,
% 71.66/71.77 (P2(f5(a2),x25731,f5(a2))+~P2(a4,a4,x25731)),
% 71.66/71.77 inference(scs_inference,[],[2537,23])).
% 71.66/71.77 cnf(2607,plain,
% 71.66/71.77 (~P2(f5(a2),a4,x26071)+P2(x26071,a2,f5(a2))+~P2(a4,a4,a4)),
% 71.66/71.77 inference(scs_inference,[],[4,2573,28])).
% 71.66/71.77 cnf(2686,plain,
% 71.66/71.77 (P2(x26861,a2,f5(a2))+~P2(f5(a2),a4,x26861)),
% 71.66/71.77 inference(scs_inference,[],[2,2607,14])).
% 71.66/71.77 cnf(2702,plain,
% 71.66/71.77 (P2(f5(a2),a2,f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[2534,2686,23])).
% 71.66/71.77 cnf(2705,plain,
% 71.66/71.77 (~P2(x27051,a2,a2)+P2(f5(a2),x27051,f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[2702,28,23])).
% 71.66/71.77 cnf(2738,plain,
% 71.66/71.77 (P2(x27381,f5(a2),f5(a2))+~P2(x27381,a2,a2)),
% 71.66/71.77 inference(scs_inference,[],[2705,23])).
% 71.66/71.77 cnf(2770,plain,
% 71.66/71.77 (P2(a4,x27701,f5(a2))+~P2(a2,x27701,f5(a2))+~P2(a4,a2,a2)),
% 71.66/71.77 inference(scs_inference,[],[4,2738,28])).
% 71.66/71.77 cnf(2951,plain,
% 71.66/71.77 (~P2(a2,x29511,f5(a2))+P2(a4,x29511,f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[3,2770,14])).
% 71.66/71.77 cnf(2967,plain,
% 71.66/71.77 (P2(x29671,a4,f5(a2))+~P2(a2,x29671,f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[2951,23])).
% 71.66/71.77 cnf(2983,plain,
% 71.66/71.77 (P2(f5(a2),a4,f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[2702,2967,23])).
% 71.66/71.77 cnf(3635,plain,
% 71.66/71.77 (P4(f5(a2),a1,f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[659,22])).
% 71.66/71.77 cnf(3644,plain,
% 71.66/71.77 (P2(a2,a4,a4)),
% 71.66/71.77 inference(scs_inference,[],[4,1883,22,23])).
% 71.66/71.77 cnf(3646,plain,
% 71.66/71.77 (P4(f5(a1),a1,f5(a1))),
% 71.66/71.77 inference(scs_inference,[],[4,1883,1375,22,23,25])).
% 71.66/71.77 cnf(3650,plain,
% 71.66/71.77 (P2(a2,f5(a1),f5(a1))),
% 71.66/71.77 inference(scs_inference,[],[4,1952,1883,1375,22,23,25,26,1575])).
% 71.66/71.77 cnf(3652,plain,
% 71.66/71.77 (P2(f5(a1),a2,f5(a1))),
% 71.66/71.77 inference(scs_inference,[],[4,1952,1883,1375,22,23,25,26,1575,1593])).
% 71.66/71.77 cnf(3654,plain,
% 71.66/71.77 (P2(a2,f5(a4),f5(a4))),
% 71.66/71.77 inference(scs_inference,[],[4,1952,1883,1375,22,23,25,26,1575,1593,2033])).
% 71.66/71.77 cnf(3656,plain,
% 71.66/71.77 (P2(a2,f5(a2),f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[4,1952,1883,1375,22,23,25,26,1575,1593,2033,2535])).
% 71.66/71.77 cnf(3663,plain,
% 71.66/71.77 (P4(f5(a4),a1,f5(a4))),
% 71.66/71.77 inference(scs_inference,[],[608,22])).
% 71.66/71.77 cnf(3665,plain,
% 71.66/71.77 (P2(f5(a1),a4,f5(a1))),
% 71.66/71.77 inference(scs_inference,[],[1571,608,22,23])).
% 71.66/71.77 cnf(3671,plain,
% 71.66/71.77 (~P4(f5(a2),f5(a1),x36711)+P2(x36711,a4,x36711)),
% 71.66/71.77 inference(scs_inference,[],[2983,150,3635,1571,608,147,1375,22,23,26,25,30])).
% 71.66/71.77 cnf(3678,plain,
% 71.66/71.77 (P2(f5(a4),a4,f5(a4))),
% 71.66/71.77 inference(scs_inference,[],[2032,147,22,23])).
% 71.66/71.77 cnf(3741,plain,
% 71.66/71.77 (~P4(f5(a1),f5(a2),x37411)+P2(x37411,a4,x37411)),
% 71.66/71.77 inference(scs_inference,[],[3671,22])).
% 71.66/71.77 cnf(3758,plain,
% 71.66/71.77 (~P2(a1,a2,a2)),
% 71.66/71.77 inference(scs_inference,[],[2138,150,608,29])).
% 71.66/71.77 cnf(3761,plain,
% 71.66/71.77 (~P2(a1,a4,a2)),
% 71.66/71.77 inference(scs_inference,[],[3665,1952,1375,29])).
% 71.66/71.77 cnf(4066,plain,
% 71.66/71.77 (~P2(f6(a2),a2,a4)+~P4(f5(a1),f5(a2),f6(a2))),
% 71.66/71.77 inference(scs_inference,[],[4,31,3741,27])).
% 71.66/71.77 cnf(4609,plain,
% 71.66/71.77 (~P4(f5(a2),f5(a1),f6(a2))+~P2(f6(a2),a2,a4)),
% 71.66/71.77 inference(scs_inference,[],[4066,22])).
% 71.66/71.77 cnf(5060,plain,
% 71.66/71.77 (~P4(a4,x50601,x50602)+~P2(x50601,f5(a2),a1)+P2(x50602,f5(a2),f5(a2))),
% 71.66/71.77 inference(scs_inference,[],[2534,4,3635,5,44,30])).
% 71.66/71.77 cnf(5730,plain,
% 71.66/71.77 (~P2(x57301,a4,a1)+~P2(x57302,a4,a1)+~P4(x57302,x57301,a2)),
% 71.66/71.77 inference(scs_inference,[],[3644,3663,3654,5,44,29])).
% 71.66/71.77 cnf(6230,plain,
% 71.66/71.77 (~P2(a2,a4,a1)+~P2(a1,a4,a1)),
% 71.66/71.77 inference(scs_inference,[],[3,5730,13])).
% 71.66/71.77 cnf(6246,plain,
% 71.66/71.77 (~P2(a4,a1,a1)+~P2(a2,a4,a1)),
% 71.66/71.77 inference(scs_inference,[],[6230,23])).
% 71.66/71.77 cnf(6262,plain,
% 71.66/71.77 (~P2(a2,a4,a1)),
% 71.66/71.77 inference(scs_inference,[],[1,6246,14])).
% 71.66/71.77 cnf(6845,plain,
% 71.66/71.77 (P2(f5(a2),x68451,f5(a2))+~P4(a4,x68452,x68451)+~P2(x68452,f5(a2),a1)),
% 71.66/71.77 inference(scs_inference,[],[5060,23])).
% 71.66/71.77 cnf(7128,plain,
% 71.66/71.77 (~P2(x71281,a4,a2)+~P2(x71281,a4,f6(a2))),
% 71.66/71.77 inference(scs_inference,[],[4,42,28])).
% 71.66/71.77 cnf(7197,plain,
% 71.66/71.77 (~P2(x71971,a4,a1)+~P2(x71971,a2,a2)),
% 71.66/71.77 inference(scs_inference,[],[3644,6262,28])).
% 71.66/71.77 cnf(7225,plain,
% 71.66/71.77 (~P2(a4,a4,a1)),
% 71.66/71.77 inference(scs_inference,[],[3,7197,14])).
% 71.66/71.77 cnf(7471,plain,
% 71.66/71.77 (~P2(a1,a4,x74711)+~P2(x74711,a2,a2)),
% 71.66/71.77 inference(scs_inference,[],[3761,4,27])).
% 71.66/71.77 cnf(7505,plain,
% 71.66/71.77 (~P2(a1,a4,a4)),
% 71.66/71.77 inference(scs_inference,[],[3,7471,14])).
% 71.66/71.77 cnf(7506,plain,
% 71.66/71.77 (~P2(a4,a1,a4)),
% 71.66/71.77 inference(scs_inference,[],[7505,23])).
% 71.66/71.77 cnf(7508,plain,
% 71.66/71.77 (~P2(a2,a2,a1)),
% 71.66/71.77 inference(scs_inference,[],[3644,7505,23,28])).
% 71.66/71.77 cnf(7758,plain,
% 71.66/71.77 (~P2(a2,a2,x77581)+~P2(x77581,a4,a1)),
% 71.66/71.77 inference(scs_inference,[],[6262,3644,27])).
% 71.66/71.77 cnf(8012,plain,
% 71.66/71.77 (~P2(a4,a4,x80121)+~P2(x80121,a2,a1)),
% 71.66/71.77 inference(scs_inference,[],[7225,4,27])).
% 71.66/71.77 cnf(8019,plain,
% 71.66/71.77 (~P2(a2,x80191,a1)+~P2(a4,a4,x80191)),
% 71.66/71.77 inference(scs_inference,[],[8012,23])).
% 71.66/71.77 cnf(8043,plain,
% 71.66/71.77 (~P2(a2,f7(a4,a4),a1)),
% 71.66/71.77 inference(scs_inference,[],[2,8019,18])).
% 71.66/71.77 cnf(8046,plain,
% 71.66/71.77 (~P2(x80461,a4,a1)+~P2(x80461,a4,f7(a4,a4))),
% 71.66/71.77 inference(scs_inference,[],[4,8043,23,28])).
% 71.66/71.77 cnf(8987,plain,
% 71.66/71.77 (P4(f5(a2),x89871,f5(a2))+~P4(a1,x89871,a1)),
% 71.66/71.77 inference(scs_inference,[],[3635,26])).
% 71.66/71.77 cnf(8990,plain,
% 71.66/71.77 (~P4(f5(a4),x89901,a2)+~P4(x89901,f5(a4),a1)),
% 71.66/71.77 inference(scs_inference,[],[3663,150,26])).
% 71.66/71.77 cnf(9001,plain,
% 71.66/71.77 (~P4(f5(a1),x90011,a1)+~P4(f5(a1),x90011,a2)),
% 71.66/71.77 inference(scs_inference,[],[1952,3646,26,22])).
% 71.66/71.77 cnf(9024,plain,
% 71.66/71.77 (P4(a1,a1,a1)),
% 71.66/71.77 inference(scs_inference,[],[1,8,13])).
% 71.66/71.77 cnf(9026,plain,
% 71.66/71.77 (P4(f5(a1),a1,a1)),
% 71.66/71.77 inference(scs_inference,[],[1,8,13,15])).
% 71.66/71.77 cnf(9028,plain,
% 71.66/71.77 (~P4(f5(a1),a1,a2)),
% 71.66/71.77 inference(scs_inference,[],[1,8,13,15,9001])).
% 71.66/71.77 cnf(9030,plain,
% 71.66/71.77 (P2(a4,a1,a1)),
% 71.66/71.77 inference(scs_inference,[],[1,8,13,15,9001,14])).
% 71.66/71.77 cnf(9032,plain,
% 71.66/71.77 (P4(a1,f5(a1),a1)),
% 71.66/71.77 inference(scs_inference,[],[1,8,13,15,9001,14,22])).
% 71.66/71.77 cnf(9034,plain,
% 71.66/71.77 (P2(a1,a4,a1)),
% 71.66/71.77 inference(scs_inference,[],[1,8,13,15,9001,14,22,23])).
% 71.66/71.77 cnf(9036,plain,
% 71.66/71.77 (P1(f3(a1,a1))),
% 71.66/71.77 inference(scs_inference,[],[1,8,13,15,9001,14,22,23,10])).
% 71.66/71.77 cnf(9038,plain,
% 71.66/71.77 (P1(f7(a1,a1))),
% 71.66/71.77 inference(scs_inference,[],[1,8,13,15,9001,14,22,23,10,11])).
% 71.66/71.77 cnf(9040,plain,
% 71.66/71.77 (P1(f6(a2))),
% 71.66/71.77 inference(scs_inference,[],[1,3,6,8,13,15,9001,14,22,23,10,11,16])).
% 71.66/71.77 cnf(9042,plain,
% 71.66/71.77 (P2(f6(a2),a2,a4)),
% 71.66/71.77 inference(scs_inference,[],[1,3,6,8,13,15,9001,14,22,23,10,11,16,20])).
% 71.66/71.77 cnf(9044,plain,
% 71.66/71.77 (P2(a1,a1,f7(a1,a1))),
% 71.66/71.77 inference(scs_inference,[],[1,3,6,8,13,15,9001,14,22,23,10,11,16,20,18])).
% 71.66/71.77 cnf(9046,plain,
% 71.66/71.77 (P4(a1,a1,f3(a1,a1))),
% 71.66/71.77 inference(scs_inference,[],[1,3,6,8,13,15,9001,14,22,23,10,11,16,20,18,17])).
% 71.66/71.77 cnf(9050,plain,
% 71.66/71.77 (P4(a1,a2,a2)),
% 71.66/71.77 inference(scs_inference,[],[1,3,6,51,8,13,15,9001,14,22,23,10,11,16,20,18,17,59,19])).
% 71.66/71.77 cnf(9052,plain,
% 71.66/71.77 (~P2(a2,a1,a4)),
% 71.66/71.77 inference(scs_inference,[],[4,7225,1,3,6,51,8,13,15,9001,14,22,23,10,11,16,20,18,17,59,19,27])).
% 71.66/71.77 cnf(9054,plain,
% 71.66/71.77 (~P4(f5(a1),f5(a1),a2)),
% 71.66/71.77 inference(scs_inference,[],[4,7225,1,3,6,51,8,13,15,9001,14,22,23,10,11,16,20,18,17,59,19,27,25])).
% 71.66/71.77 cnf(9058,plain,
% 71.66/71.77 (~P4(a1,f5(a1),a2)),
% 71.66/71.77 inference(scs_inference,[],[4,7225,1,3,6,3646,37,51,1375,8,13,15,9001,14,22,23,10,11,16,20,18,17,59,19,27,25,21,26])).
% 71.66/71.77 cnf(9060,plain,
% 71.66/71.77 (P2(a1,a2,a1)),
% 71.66/71.77 inference(scs_inference,[],[4,7225,1,3,6,3646,37,51,1375,8,13,15,9001,14,22,23,10,11,16,20,18,17,59,19,27,25,21,26,28])).
% 71.66/71.77 cnf(9062,plain,
% 71.66/71.77 (~P2(f5(a1),a4,a2)),
% 71.66/71.77 inference(scs_inference,[],[4,7225,1,3,3665,6,3646,37,51,1375,8,13,15,9001,14,22,23,10,11,16,20,18,17,59,19,27,25,21,26,28,29])).
% 71.66/71.77 cnf(9064,plain,
% 71.66/71.77 (~P4(f5(a1),a1,a4)),
% 71.66/71.77 inference(scs_inference,[],[4,7505,7225,1,3,3665,6,3646,37,51,1375,8,13,15,9001,14,22,23,10,11,16,20,18,17,59,19,27,25,21,26,28,29,30])).
% 71.66/71.77 cnf(9071,plain,
% 71.66/71.77 (~P4(f5(a1),f5(a2),f6(a2))),
% 71.66/71.77 inference(scs_inference,[],[9042,4066])).
% 71.66/71.77 cnf(9072,plain,
% 71.66/71.77 (~P4(f5(a2),f5(a1),f6(a2))),
% 71.66/71.77 inference(scs_inference,[],[9042,4609])).
% 71.66/71.77 cnf(9078,plain,
% 71.66/71.77 (P4(f5(a4),a4,a1)),
% 71.66/71.77 inference(scs_inference,[],[2,8,15])).
% 71.66/71.77 cnf(9080,plain,
% 71.66/71.77 (P4(a1,f3(a1,a1),f3(a1,a1))),
% 71.66/71.77 inference(scs_inference,[],[9036,2,8,15,13])).
% 71.66/71.77 cnf(9082,plain,
% 71.66/71.77 (P2(a4,f3(a1,a1),f3(a1,a1))),
% 71.66/71.77 inference(scs_inference,[],[9036,2,8,15,13,14])).
% 71.66/71.77 cnf(9084,plain,
% 71.66/71.77 (P4(a2,a1,a2)),
% 71.66/71.77 inference(scs_inference,[],[9050,9036,2,8,15,13,14,22])).
% 71.66/71.77 cnf(9086,plain,
% 71.66/71.77 (P2(a2,a1,a1)),
% 71.66/71.77 inference(scs_inference,[],[9060,9050,9036,2,8,15,13,14,22,23])).
% 71.66/71.77 cnf(9088,plain,
% 71.66/71.77 (P1(f7(a4,a4))),
% 71.66/71.77 inference(scs_inference,[],[9060,9050,9036,2,8,15,13,14,22,23,11])).
% 71.66/71.77 cnf(9090,plain,
% 71.66/71.77 (P1(f3(a4,a4))),
% 71.66/71.77 inference(scs_inference,[],[9060,9050,9036,2,8,15,13,14,22,23,11,10])).
% 71.66/71.77 cnf(9092,plain,
% 71.66/71.77 (P2(a4,a4,f7(a4,a4))),
% 71.66/71.77 inference(scs_inference,[],[9060,9050,9036,2,8,15,13,14,22,23,11,10,18])).
% 71.66/71.77 cnf(9094,plain,
% 71.66/71.77 (P4(a4,a4,f3(a4,a4))),
% 71.66/71.77 inference(scs_inference,[],[9060,9050,9036,2,8,15,13,14,22,23,11,10,18,17])).
% 71.66/71.77 cnf(9096,plain,
% 71.66/71.77 (P4(a1,a4,a4)),
% 71.66/71.77 inference(scs_inference,[],[9060,9050,9036,2,44,8,15,13,14,22,23,11,10,18,17,19])).
% 71.66/71.77 cnf(9098,plain,
% 71.66/71.77 (P2(a1,f7(a4,a4),a1)),
% 71.66/71.77 inference(scs_inference,[],[9034,9060,9050,9036,2,44,8,15,13,14,22,23,11,10,18,17,19,27])).
% 71.66/71.77 cnf(9100,plain,
% 71.66/71.77 (~P4(a2,a1,f5(a1))),
% 71.66/71.77 inference(scs_inference,[],[9034,9060,9050,9058,9036,2,44,8,15,13,14,22,23,11,10,18,17,19,27,25])).
% 71.66/71.77 cnf(9102,plain,
% 71.66/71.77 (P4(f3(a1,a1),a1,f3(a1,a1))),
% 71.66/71.77 inference(scs_inference,[],[9034,9060,9050,9058,9036,9046,2,44,8,15,13,14,22,23,11,10,18,17,19,27,25,26])).
% 71.66/71.77 cnf(9104,plain,
% 71.66/71.77 (P2(f7(a4,a4),a1,a1)),
% 71.66/71.77 inference(scs_inference,[],[9034,9060,9030,9050,9058,9036,9046,2,44,8,15,13,14,22,23,11,10,18,17,19,27,25,26,28])).
% 71.66/71.77 cnf(9110,plain,
% 71.66/71.77 (P2(f3(a4,a4),a2,f3(a4,a4))),
% 71.66/71.77 inference(scs_inference,[],[4,9034,9060,9030,9050,9058,9036,9046,148,2,3654,44,8,15,13,14,22,23,11,10,18,17,19,27,25,26,28,24,29,30])).
% 71.66/71.77 cnf(9118,plain,
% 71.66/71.77 (P4(a1,f3(a4,a4),f3(a4,a4))),
% 71.66/71.77 inference(scs_inference,[],[9090,3,8,13])).
% 71.66/71.77 cnf(9120,plain,
% 71.66/71.77 (P4(f5(a2),a2,a1)),
% 71.66/71.77 inference(scs_inference,[],[9090,3,8,13,15])).
% 71.66/71.77 cnf(9122,plain,
% 71.66/71.77 (P2(a4,f3(a4,a4),f3(a4,a4))),
% 71.66/71.77 inference(scs_inference,[],[9090,3,8,13,15,14])).
% 71.66/71.77 cnf(9124,plain,
% 71.66/71.77 (P4(a4,a1,a4)),
% 71.66/71.77 inference(scs_inference,[],[9096,9090,3,8,13,15,14,22])).
% 71.66/71.77 cnf(9126,plain,
% 71.66/71.77 (P2(a2,f6(a2),a4)),
% 71.66/71.77 inference(scs_inference,[],[9096,9090,9042,3,8,13,15,14,22,23])).
% 71.66/71.77 cnf(9128,plain,
% 71.66/71.77 (P1(f7(a2,a2))),
% 71.66/71.77 inference(scs_inference,[],[9096,9090,9042,3,8,13,15,14,22,23,11])).
% 71.66/71.77 cnf(9130,plain,
% 71.66/71.77 (P2(a2,a2,f7(a2,a2))),
% 71.66/71.77 inference(scs_inference,[],[9096,9090,9042,3,8,13,15,14,22,23,11,18])).
% 71.66/71.77 cnf(9132,plain,
% 71.66/71.77 (P1(f3(a2,a2))),
% 71.66/71.77 inference(scs_inference,[],[9096,9090,9042,3,8,13,15,14,22,23,11,18,10])).
% 71.66/71.77 cnf(9134,plain,
% 71.66/71.77 (P4(a2,a2,f3(a2,a2))),
% 71.66/71.77 inference(scs_inference,[],[9096,9090,9042,3,8,13,15,14,22,23,11,18,10,17])).
% 71.66/71.77 cnf(9136,plain,
% 71.66/71.77 (~P2(a2,a1,f6(a2))),
% 71.66/71.77 inference(scs_inference,[],[9052,9096,9090,9042,9060,3,8,13,15,14,22,23,11,18,10,17,27])).
% 71.66/71.77 cnf(9138,plain,
% 71.66/71.77 (~P4(a1,a4,a1)),
% 71.66/71.78 inference(scs_inference,[],[9052,9096,9090,9064,9042,9026,9060,3,8,13,15,14,22,23,11,18,10,17,27,25])).
% 71.66/71.78 cnf(9140,plain,
% 71.66/71.78 (~P4(f5(a4),f3(a4,a4),a1)),
% 71.66/71.78 inference(scs_inference,[],[9052,9096,9090,9064,9042,9094,9078,9026,9060,3,8,13,15,14,22,23,11,18,10,17,27,25,26])).
% 71.66/71.78 cnf(9142,plain,
% 71.66/71.78 (P2(f7(a4,a4),a2,f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[4,9052,9096,9090,9064,9042,9094,9092,9078,9026,9060,3,8,13,15,14,22,23,11,18,10,17,27,25,26,28])).
% 71.66/71.78 cnf(9144,plain,
% 71.66/71.78 (P4(f7(a1,a1),f7(a1,a1),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[4,9024,9052,9096,9090,9064,9042,9094,9092,9044,9078,9026,9060,3,8,13,15,14,22,23,11,18,10,17,27,25,26,28,29])).
% 71.66/71.78 cnf(9146,plain,
% 71.66/71.78 (~P4(a1,f7(a1,a1),a4)),
% 71.66/71.78 inference(scs_inference,[],[4,9086,9024,9052,9084,9096,9090,9064,9042,9094,9092,9044,9078,9026,9060,3,8,13,15,14,22,23,11,18,10,17,27,25,26,28,29,30])).
% 71.66/71.78 cnf(9148,plain,
% 71.66/71.78 (~P2(f7(a2,a2),a4,a1)),
% 71.66/71.78 inference(scs_inference,[],[4,9086,9024,9052,9084,9096,9090,9064,9042,9094,9092,9044,9078,9026,9060,3,8,13,15,14,22,23,11,18,10,17,27,25,26,28,29,30,7758])).
% 71.66/71.78 cnf(9154,plain,
% 71.66/71.78 (P1(f6(a4))),
% 71.66/71.78 inference(scs_inference,[],[4,9086,9024,9052,9084,9096,9090,9064,9042,9094,9092,9044,9078,9026,9060,3,2,8,13,15,14,22,23,11,18,10,17,27,25,26,28,29,30,7758,6845,54,16])).
% 71.66/71.78 cnf(9156,plain,
% 71.66/71.78 (P2(f6(a4),a4,a4)),
% 71.66/71.78 inference(scs_inference,[],[4,9086,9024,9052,9084,9096,9090,9064,9042,9094,9092,9044,9078,9026,9060,3,2,8,13,15,14,22,23,11,18,10,17,27,25,26,28,29,30,7758,6845,54,16,20])).
% 71.66/71.78 cnf(9158,plain,
% 71.66/71.78 (P4(a1,f3(a2,a2),f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[4,9086,9024,9052,9084,9096,9090,9064,9042,9094,9092,9044,9078,9026,9060,3,2,8,13,15,14,22,23,11,18,10,17,27,25,26,28,29,30,7758,6845,54,16,20,19])).
% 71.66/71.78 cnf(9163,plain,
% 71.66/71.78 (P4(a1,f7(a4,a4),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9088,13])).
% 71.66/71.78 cnf(9165,plain,
% 71.66/71.78 (P2(a4,f3(a2,a2),f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9132,9088,13,14])).
% 71.66/71.78 cnf(9167,plain,
% 71.66/71.78 (P4(f3(a4,a4),a1,f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9132,9088,9118,13,14,22])).
% 71.66/71.78 cnf(9169,plain,
% 71.66/71.78 (P2(a2,f3(a4,a4),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9132,9088,9118,9110,13,14,22,23])).
% 71.66/71.78 cnf(9171,plain,
% 71.66/71.78 (P2(f3(a4,a4),f7(a2,a2),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9132,9088,9118,9110,9130,13,14,22,23,27])).
% 71.66/71.78 cnf(9173,plain,
% 71.66/71.78 (~P4(a1,a2,f5(a1))),
% 71.66/71.78 inference(scs_inference,[],[9132,9054,9088,9118,9110,9130,9026,9050,13,14,22,23,27,25])).
% 71.66/71.78 cnf(9175,plain,
% 71.66/71.78 (~P4(f5(a4),f5(a2),f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[9132,9054,9088,9118,9110,9130,9120,9026,9050,148,3663,13,14,22,23,27,25,26])).
% 71.66/71.78 cnf(9177,plain,
% 71.66/71.78 (~P2(f6(a2),a1,f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9132,9054,9088,9118,9110,9130,9120,9126,7506,9026,9050,148,3663,13,14,22,23,27,25,26,28])).
% 71.66/71.78 cnf(9181,plain,
% 71.66/71.78 (~P2(f5(a4),a2,a1)),
% 71.66/71.78 inference(scs_inference,[],[4,9138,9132,9054,9088,9118,9110,9130,9120,9126,7506,9078,9026,9050,9060,148,3663,37,13,14,22,23,27,25,26,28,24,29])).
% 71.66/71.78 cnf(9183,plain,
% 71.66/71.78 (~P4(a1,f5(a1),a4)),
% 71.66/71.78 inference(scs_inference,[],[4,9138,9132,9054,9088,9118,9110,9032,9130,9120,9126,7506,9078,9026,9034,9050,9060,148,7505,3665,3663,37,13,14,22,23,27,25,26,28,24,29,30])).
% 71.66/71.78 cnf(9189,plain,
% 71.66/71.78 (P4(a1,f7(a1,a1),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9038,13])).
% 71.66/71.78 cnf(9191,plain,
% 71.66/71.78 (P2(a4,f7(a1,a1),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9038,13,14])).
% 71.66/71.78 cnf(9193,plain,
% 71.66/71.78 (P4(f7(a4,a4),a1,f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9163,9038,13,14,22])).
% 71.66/71.78 cnf(9195,plain,
% 71.66/71.78 (P2(f7(a2,a2),f3(a4,a4),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9171,9163,9038,13,14,22,23])).
% 71.66/71.78 cnf(9197,plain,
% 71.66/71.78 (~P2(a4,a1,f6(a4))),
% 71.66/71.78 inference(scs_inference,[],[9171,9156,9163,9038,7506,9034,13,14,22,23,27])).
% 71.66/71.78 cnf(9199,plain,
% 71.66/71.78 (~P4(f5(a1),f5(a1),a4)),
% 71.66/71.78 inference(scs_inference,[],[9171,9156,9163,9038,9138,9032,7506,9034,13,14,22,23,27,25])).
% 71.66/71.78 cnf(9201,plain,
% 71.66/71.78 (~P4(f5(a2),f3(a2,a2),f5(a1))),
% 71.66/71.78 inference(scs_inference,[],[9171,9134,9156,9163,9038,9173,9120,9138,9032,7506,9034,13,14,22,23,27,25,26])).
% 71.66/71.78 cnf(9203,plain,
% 71.66/71.78 (~P2(f6(a4),f6(a4),a1)),
% 71.66/71.78 inference(scs_inference,[],[9171,9134,9156,9163,9038,9173,9120,9138,9032,7506,9034,7505,13,14,22,23,27,25,26,28])).
% 71.66/71.78 cnf(9205,plain,
% 71.66/71.78 (P4(f7(a1,a1),a1,a1)),
% 71.66/71.78 inference(scs_inference,[],[9171,9134,9156,9163,9038,9104,9173,9120,9138,9032,7506,9044,9034,7505,13,14,22,23,27,25,26,28,29])).
% 71.66/71.78 cnf(9207,plain,
% 71.66/71.78 (~P4(a1,a1,f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[9171,9134,9156,9163,9038,9181,9104,9173,9120,9024,9138,9032,7506,9044,9034,9060,7505,13,14,22,23,27,25,26,28,29,30])).
% 71.66/71.78 cnf(9215,plain,
% 71.66/71.78 (P4(a1,f7(a2,a2),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9128,13])).
% 71.66/71.78 cnf(9217,plain,
% 71.66/71.78 (P2(a4,f7(a2,a2),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9128,13,14])).
% 71.66/71.78 cnf(9219,plain,
% 71.66/71.78 (P4(f7(a1,a1),a1,f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9189,9128,13,14,22])).
% 71.66/71.78 cnf(9221,plain,
% 71.66/71.78 (P2(f3(a2,a2),a4,f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9189,9128,9165,13,14,22,23])).
% 71.66/71.78 cnf(9223,plain,
% 71.66/71.78 (P2(f7(a4,a4),f7(a2,a2),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9189,9128,9165,9142,9130,13,14,22,23,27])).
% 71.66/71.78 cnf(9225,plain,
% 71.66/71.78 (P4(f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9102,9189,9128,9165,9142,9046,9130,13,14,22,23,27,25])).
% 71.66/71.78 cnf(9229,plain,
% 71.66/71.78 (P2(a4,f6(a2),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[4,9102,9189,9128,9165,9142,9205,9146,9126,9046,9130,9092,13,14,22,23,27,25,26,28])).
% 71.66/71.78 cnf(9231,plain,
% 71.66/71.78 (~P2(f3(a1,a1),f7(a4,a4),f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[4,9207,9102,9189,9098,9128,9165,9142,9205,9146,9126,9046,9130,9092,13,14,22,23,27,25,26,28,29])).
% 71.66/71.78 cnf(9233,plain,
% 71.66/71.78 (~P4(f7(a2,a2),a1,a1)),
% 71.66/71.78 inference(scs_inference,[],[4,9207,9102,9189,9098,9128,9165,9142,9205,9146,7508,9126,9084,9046,9130,9092,9060,13,14,22,23,27,25,26,28,29,30])).
% 71.66/71.78 cnf(9238,plain,
% 71.66/71.78 (P4(a1,f6(a2),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9040,13])).
% 71.66/71.78 cnf(9240,plain,
% 71.66/71.78 (P4(f7(a2,a2),a1,f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9215,9040,13,22])).
% 71.66/71.78 cnf(9242,plain,
% 71.66/71.78 (P2(a4,f6(a2),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9215,9040,13,22,14])).
% 71.66/71.78 cnf(9244,plain,
% 71.66/71.78 (P2(f7(a2,a2),f7(a4,a4),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9223,9215,9040,13,22,14,23])).
% 71.66/71.78 cnf(9246,plain,
% 71.66/71.78 (~P2(f6(a2),a2,a1)),
% 71.66/71.78 inference(scs_inference,[],[4,9223,9215,9040,9052,9126,13,22,14,23,27])).
% 71.66/71.78 cnf(9248,plain,
% 71.66/71.78 (~P4(a1,a4,f5(a1))),
% 71.66/71.78 inference(scs_inference,[],[4,9223,9199,9215,9040,9052,9126,9026,9096,13,22,14,23,27,25])).
% 71.66/71.78 cnf(9250,plain,
% 71.66/71.78 (~P4(f5(a1),f5(a2),a1)),
% 71.66/71.78 inference(scs_inference,[],[4,9223,9199,9215,9040,9173,9052,9120,9126,9026,9096,3646,13,22,14,23,27,25,26])).
% 71.66/71.78 cnf(9252,plain,
% 71.66/71.78 (P2(f3(a2,a2),a2,f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[4,9223,9199,9221,9215,9040,9173,9052,9120,9126,9026,9096,3646,13,22,14,23,27,25,26,28])).
% 71.66/71.78 cnf(9256,plain,
% 71.66/71.78 (~P4(a1,f7(a1,a1),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[4,9223,9199,9221,9215,9040,9136,9173,9086,9052,9120,9126,9084,9026,9096,9044,3646,37,13,22,14,23,27,25,26,28,24,30])).
% 71.66/71.78 cnf(9263,plain,
% 71.66/71.78 (P4(a1,f6(a4),f6(a4))),
% 71.66/71.78 inference(scs_inference,[],[9154,13])).
% 71.66/71.78 cnf(9265,plain,
% 71.66/71.78 (P2(a4,f6(a4),f6(a4))),
% 71.66/71.78 inference(scs_inference,[],[9154,13,14])).
% 71.66/71.78 cnf(9267,plain,
% 71.66/71.78 (P4(f6(a2),a1,f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9154,9238,13,14,22])).
% 71.66/71.78 cnf(9269,plain,
% 71.66/71.78 (P2(f3(a4,a4),a4,f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9122,9154,9238,13,14,22,23])).
% 71.66/71.78 cnf(9273,plain,
% 71.66/71.78 (~P4(f6(a2),a1,f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[4,9062,9122,9154,9256,9238,3665,13,14,22,23,27,25])).
% 71.66/71.78 cnf(9275,plain,
% 71.66/71.78 (~P4(f7(a1,a1),f7(a1,a1),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[4,9062,9122,9154,9256,9238,9189,9205,3665,13,14,22,23,27,25,26])).
% 71.66/71.78 cnf(9277,plain,
% 71.66/71.78 (P2(f7(a4,a4),f3(a4,a4),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[4,9062,9122,9154,9256,9238,9189,9205,9092,3665,13,14,22,23,27,25,26,28])).
% 71.66/71.78 cnf(9281,plain,
% 71.66/71.78 (~P4(f5(a4),a4,a2)),
% 71.66/71.78 inference(scs_inference,[],[4,9062,9122,9154,9256,9238,9189,9205,9078,9092,3758,3665,37,2138,13,14,22,23,27,25,26,28,24,30])).
% 71.66/71.78 cnf(9283,plain,
% 71.66/71.78 (~P2(a1,a1,f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[4,9062,9122,9154,9256,9238,9233,9104,9189,9205,9163,9078,9092,3758,3665,37,2138,13,14,22,23,27,25,26,28,24,30,29])).
% 71.66/71.78 cnf(9290,plain,
% 71.66/71.78 (P4(f6(a4),a1,f6(a4))),
% 71.66/71.78 inference(scs_inference,[],[9263,22])).
% 71.66/71.78 cnf(9292,plain,
% 71.66/71.78 (P2(a4,f7(a4,a4),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9263,9088,22,14])).
% 71.66/71.78 cnf(9294,plain,
% 71.66/71.78 (P2(f3(a4,a4),f7(a4,a4),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9277,9263,9088,22,14,23])).
% 71.66/71.78 cnf(9296,plain,
% 71.66/71.78 (P2(f3(a2,a2),f7(a2,a2),f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9277,9252,9263,9088,9130,22,14,23,27])).
% 71.66/71.78 cnf(9298,plain,
% 71.66/71.78 (~P4(a4,a1,f5(a1))),
% 71.66/71.78 inference(scs_inference,[],[9277,9252,9263,9183,9124,9088,9130,9096,22,14,23,27,25])).
% 71.66/71.78 cnf(9300,plain,
% 71.66/71.78 (~P4(a1,f7(a2,a2),a1)),
% 71.66/71.78 inference(scs_inference,[],[9277,9252,9240,9263,9183,9124,9088,9233,9215,9130,9096,22,14,23,27,25,26])).
% 71.66/71.78 cnf(9302,plain,
% 71.66/71.78 (P2(f3(a4,a4),f6(a2),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9277,9252,9240,9269,9229,9263,9183,9124,9088,9233,9215,9130,9096,22,14,23,27,25,26,28])).
% 71.66/71.78 cnf(9304,plain,
% 71.66/71.78 (~P2(f6(a2),a2,f5(a1))),
% 71.66/71.78 inference(scs_inference,[],[9277,9252,9240,9269,9229,9263,9183,9248,9124,9088,9233,9042,9215,9238,9130,9096,9060,22,14,23,27,25,26,28,29])).
% 71.66/71.78 cnf(9306,plain,
% 71.66/71.78 (P2(f3(a4,a4),f3(a1,a1),f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9277,9225,9252,9240,9269,9082,9229,9263,9183,9248,9124,9088,9233,9042,9215,9238,9130,9096,9094,9060,22,14,23,27,25,26,28,29,30])).
% 71.66/71.78 cnf(9312,plain,
% 71.66/71.78 (P4(f3(a2,a2),a1,f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9158,22])).
% 71.66/71.78 cnf(9314,plain,
% 71.66/71.78 (P2(a4,a4,a4)),
% 71.66/71.78 inference(scs_inference,[],[9158,2,22,14])).
% 71.66/71.78 cnf(9316,plain,
% 71.66/71.78 (P2(f3(a1,a1),f3(a4,a4),f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9306,9158,2,22,14,23])).
% 71.66/71.78 cnf(9318,plain,
% 71.66/71.78 (~P2(a2,f6(a4),a1)),
% 71.66/71.78 inference(scs_inference,[],[4,9306,9265,9197,9158,2,22,14,23,27])).
% 71.66/71.78 cnf(9320,plain,
% 71.66/71.78 (~P4(a1,a1,f5(a2))),
% 71.66/71.78 inference(scs_inference,[],[4,9306,9250,9265,9197,9158,9024,9026,2,22,14,23,27,25])).
% 71.66/71.78 cnf(9322,plain,
% 71.66/71.78 (~P4(f5(a2),a1,f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[4,9306,9250,9072,9265,9197,9158,9024,9032,9026,2,3635,22,14,23,27,25,26])).
% 71.66/71.78 cnf(9324,plain,
% 71.66/71.78 (P2(a1,f7(a2,a2),a1)),
% 71.66/71.78 inference(scs_inference,[],[4,9306,9250,9072,9265,9197,9158,9223,9098,9024,9032,9026,2,3635,22,14,23,27,25,26,28])).
% 71.66/71.78 cnf(9326,plain,
% 71.66/71.78 (~P2(f6(a4),a4,f5(a1))),
% 71.66/71.78 inference(scs_inference,[],[4,9306,9250,9072,9290,9265,9197,9298,9158,9223,9156,9098,9024,9032,9026,9034,2,3635,22,14,23,27,25,26,28,29])).
% 71.66/71.78 cnf(9332,plain,
% 71.66/71.78 (P4(a2,f5(a2),a1)),
% 71.66/71.78 inference(scs_inference,[],[9120,22])).
% 71.66/71.78 cnf(9334,plain,
% 71.66/71.78 (P2(a4,a2,a2)),
% 71.66/71.78 inference(scs_inference,[],[9120,3,22,14])).
% 71.66/71.78 cnf(9336,plain,
% 71.66/71.78 (P2(f7(a4,a4),a4,f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9292,9120,3,22,14,23])).
% 71.66/71.78 cnf(9340,plain,
% 71.66/71.78 (~P2(f7(a4,a4),a1,a4)),
% 71.66/71.78 inference(scs_inference,[],[9148,9244,9292,9263,9120,9104,3,22,14,23,59,27])).
% 71.66/71.78 cnf(9342,plain,
% 71.66/71.78 (P4(f7(a1,a1),f3(a1,a1),f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9148,9244,9292,9080,9263,9120,9104,9205,3,22,14,23,59,27,25])).
% 71.66/71.78 cnf(9344,plain,
% 71.66/71.78 (~P4(f5(a2),a2,f5(a2))),
% 71.66/71.78 inference(scs_inference,[],[9148,9244,9320,9292,9080,9263,9120,9104,9205,9084,3,22,14,23,59,27,25,26])).
% 71.66/71.78 cnf(9346,plain,
% 71.66/71.78 (P2(f3(a1,a1),f7(a4,a4),f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9316,9294,9148,9244,9320,9292,9080,9263,9120,9104,9205,9084,3,22,14,23,59,27,25,26,28])).
% 71.66/71.78 cnf(9348,plain,
% 71.66/71.78 (~P4(a1,f3(a1,a1),f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[9316,9294,9148,9244,9231,9320,9292,9080,9263,9120,9104,9205,9098,9084,3,22,14,23,59,27,25,26,28,30])).
% 71.66/71.78 cnf(9350,plain,
% 71.66/71.78 (~P2(a4,a2,f5(a1))),
% 71.66/71.78 inference(scs_inference,[],[4,9316,9294,9148,9244,9231,9320,9292,9080,9263,9298,9124,9120,9104,9205,9098,9084,9060,3,22,14,23,59,27,25,26,28,30,29])).
% 71.66/71.78 cnf(9352,plain,
% 71.66/71.78 (~P2(f7(a4,a4),a4,a1)),
% 71.66/71.78 inference(scs_inference,[],[4,9316,9294,9148,9244,9231,9320,9292,9080,9263,9298,9124,9120,9104,9205,9098,9084,9060,3,22,14,23,59,27,25,26,28,30,29,8046])).
% 71.66/71.78 cnf(9358,plain,
% 71.66/71.78 (P4(f3(a1,a1),f7(a1,a1),f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9342,22])).
% 71.66/71.78 cnf(9360,plain,
% 71.66/71.78 (P2(a2,a4,a2)),
% 71.66/71.78 inference(scs_inference,[],[9334,9342,22,23])).
% 71.66/71.78 cnf(9362,plain,
% 71.66/71.78 (~P2(f6(a4),a4,a1)),
% 71.66/71.78 inference(scs_inference,[],[9334,9342,9265,7506,9156,22,23,27])).
% 71.66/71.78 cnf(9364,plain,
% 71.66/71.78 (~P4(a4,a1,f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9334,9342,9140,9265,7506,9156,9024,9078,22,23,27,25])).
% 71.66/71.78 cnf(9366,plain,
% 71.66/71.78 (~P4(f5(a4),a4,f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[9334,9342,9140,9207,9265,9124,7506,9156,9024,9078,22,23,27,25,26])).
% 71.66/71.78 cnf(9368,plain,
% 71.66/71.78 (P2(f3(a1,a1),a4,f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9334,9346,9342,9140,9336,9207,9265,9124,7506,9156,9024,9078,22,23,27,25,26,28])).
% 71.66/71.78 cnf(9370,plain,
% 71.66/71.78 (~P4(a4,a1,a1)),
% 71.66/71.78 inference(scs_inference,[],[9334,9346,9342,9140,9246,9336,9267,9207,9265,9124,7506,9042,9156,9024,9078,9060,22,23,27,25,26,28,30])).
% 71.66/71.78 cnf(9372,plain,
% 71.66/71.78 (~P2(f5(a4),f7(a2,a2),a1)),
% 71.66/71.78 inference(scs_inference,[],[9334,9346,9342,9140,9246,9336,9300,9324,9217,9267,9207,9265,9124,7506,9042,9156,9024,9078,9060,22,23,27,25,26,28,30,29])).
% 71.66/71.78 cnf(9379,plain,
% 71.66/71.78 (P2(f6(a2),f3(a4,a4),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9302,23])).
% 71.66/71.78 cnf(9381,plain,
% 71.66/71.78 (P4(a1,f7(a1,a1),a1)),
% 71.66/71.78 inference(scs_inference,[],[9302,9205,23,22])).
% 71.66/71.78 cnf(9385,plain,
% 71.66/71.78 (~P4(a4,f5(a1),a1)),
% 71.66/71.78 inference(scs_inference,[],[9370,9302,9071,9267,9332,9032,9205,9124,23,22,26,25])).
% 71.66/71.78 cnf(9389,plain,
% 71.66/71.78 (P2(a2,a2,a2)),
% 71.66/71.78 inference(scs_inference,[],[4,9360,9370,9302,9177,9071,9242,9267,9332,9032,9042,9205,9124,23,22,26,25,27,28])).
% 71.66/71.78 cnf(9391,plain,
% 71.66/71.78 (~P4(f7(a2,a2),f5(a2),a2)),
% 71.66/71.78 inference(scs_inference,[],[4,9360,9370,9302,9177,9071,9242,9267,9332,9032,9042,9205,9130,9124,3758,2702,23,22,26,25,27,28,30])).
% 71.66/71.78 cnf(9393,plain,
% 71.66/71.78 (~P2(a4,a4,f5(a1))),
% 71.66/71.78 inference(scs_inference,[],[4,9360,9370,9302,9177,9071,9242,9314,9248,9267,9332,9032,9042,9205,9130,9096,9124,9034,3758,2702,23,22,26,25,27,28,30,29])).
% 71.66/71.78 cnf(9399,plain,
% 71.66/71.78 (P2(f7(a2,a2),f3(a2,a2),f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9296,23])).
% 71.66/71.78 cnf(9401,plain,
% 71.66/71.78 (P4(a4,f5(a4),a1)),
% 71.66/71.78 inference(scs_inference,[],[9296,9078,23,22])).
% 71.66/71.78 cnf(9403,plain,
% 71.66/71.78 (~P4(f7(a1,a1),a2,f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[6,9381,9296,9078,23,22,26])).
% 71.66/71.78 cnf(9405,plain,
% 71.66/71.78 (~P4(f7(a1,a1),f7(a1,a1),a2)),
% 71.66/71.78 inference(scs_inference,[],[6,9381,9296,9078,23,22,26,25])).
% 71.66/71.78 cnf(9407,plain,
% 71.66/71.78 (~P2(a4,f5(a1),a4)),
% 71.66/71.78 inference(scs_inference,[],[6,9381,9326,9296,9156,9078,1571,23,22,26,25,27])).
% 71.66/71.78 cnf(9409,plain,
% 71.66/71.78 (P2(f7(a1,a1),f7(a2,a2),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[6,9381,9326,9296,9324,9156,9044,9078,1571,23,22,26,25,27,28])).
% 71.66/71.78 cnf(9411,plain,
% 71.66/71.78 (~P4(f3(a1,a1),f3(a1,a1),f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[6,9381,9326,9296,9231,9324,9225,9346,9156,9044,9078,1571,23,22,26,25,27,28,30])).
% 71.66/71.78 cnf(9413,plain,
% 71.66/71.78 (~P2(f7(a1,a1),f7(a2,a2),a2)),
% 71.66/71.78 inference(scs_inference,[],[6,9381,9326,9296,9231,9324,9225,9346,9156,9044,9078,1571,23,22,26,25,27,28,30,29])).
% 71.66/71.78 cnf(9417,plain,
% 71.66/71.78 (~P4(a4,f5(a4),a2)),
% 71.66/71.78 inference(scs_inference,[],[6,9381,9326,9296,9231,9324,9225,9346,9156,9044,9078,1571,23,22,26,25,27,28,30,29,115,53])).
% 71.66/71.78 cnf(9420,plain,
% 71.66/71.78 (P2(f7(a2,a2),f7(a1,a1),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9409,23])).
% 71.66/71.78 cnf(9422,plain,
% 71.66/71.78 (~P4(a1,f6(a2),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9409,9273,9267,9238,23,26])).
% 71.66/71.78 cnf(9424,plain,
% 71.66/71.78 (P4(f7(a4,a4),f3(a1,a1),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9409,9273,9193,9267,9046,9238,23,26,25])).
% 71.66/71.78 cnf(9426,plain,
% 71.66/71.78 (~P2(a1,f7(a2,a2),a4)),
% 71.66/71.78 inference(scs_inference,[],[9409,9273,9193,9030,9267,9046,9324,9238,7225,23,26,25,27])).
% 71.66/71.78 cnf(9428,plain,
% 71.66/71.78 (P2(f3(a1,a1),f6(a2),f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9409,9368,9273,9193,9229,9030,9267,9346,9046,9324,9238,7225,23,26,25,27,28])).
% 71.66/71.78 cnf(9430,plain,
% 71.66/71.78 (~P4(f7(a4,a4),a1,a1)),
% 71.66/71.78 inference(scs_inference,[],[9409,9352,9368,9273,9193,9229,9030,9336,9267,9346,9046,9324,9238,9034,7225,23,26,25,27,28,30])).
% 71.66/71.78 cnf(9432,plain,
% 71.66/71.78 (~P2(f7(a1,a1),f7(a2,a2),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9409,9352,9275,9368,9273,9193,9144,9229,9030,9336,9267,9346,9046,9324,9238,9034,7225,23,26,25,27,28,30,29])).
% 71.66/71.78 cnf(9434,plain,
% 71.66/71.78 (P4(f3(a1,a1),f7(a4,a4),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9409,9352,9275,9368,9273,9193,9144,9229,9030,9336,9267,9346,9046,9324,9238,9034,7225,23,26,25,27,28,30,29,22])).
% 71.66/71.78 cnf(9442,plain,
% 71.66/71.78 (~P4(f5(a2),f3(a2,a2),a1)),
% 71.66/71.78 inference(scs_inference,[],[6,9428,9134,9120,23,26])).
% 71.66/71.78 cnf(9444,plain,
% 71.66/71.78 (~P4(a2,f5(a1),f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[6,9201,9428,9134,9120,1375,23,26,25])).
% 71.66/71.78 cnf(9446,plain,
% 71.66/71.78 (P2(f7(a2,a2),f3(a1,a1),f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[6,9195,9201,9428,9306,9134,9120,1375,23,26,25,27])).
% 71.66/71.78 cnf(9448,plain,
% 71.66/71.78 (~P2(f6(a2),f5(a1),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[6,9195,9201,9428,9407,9306,9126,9134,9120,1375,23,26,25,27,28])).
% 71.66/71.78 cnf(9450,plain,
% 71.66/71.78 (~P4(f7(a1,a1),a1,f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[6,9195,9201,9428,9432,9407,9219,9306,9409,9126,9134,9324,9120,1375,23,26,25,27,28,30])).
% 71.66/71.78 cnf(9452,plain,
% 71.66/71.78 (~P2(a1,a1,f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[6,9195,9201,9428,9432,9407,9430,9219,9306,9409,9030,9126,9134,9324,9120,9096,1375,23,26,25,27,28,30,29])).
% 71.66/71.78 cnf(9458,plain,
% 71.66/71.78 (P2(f3(a1,a1),f7(a2,a2),f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9446,23])).
% 71.66/71.78 cnf(9460,plain,
% 71.66/71.78 (~P4(f5(a2),f3(a2,a2),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9446,9442,9381,659,23,26])).
% 71.66/71.78 cnf(9462,plain,
% 71.66/71.78 (P4(f7(a1,a1),f7(a4,a4),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9446,9442,9434,9342,9381,659,23,26,25])).
% 71.66/71.78 cnf(9464,plain,
% 71.66/71.78 (~P2(f3(a4,a4),x94641,a2)),
% 71.66/71.78 inference(scs_inference,[],[9446,9379,9442,9434,9342,9381,42,659,23,26,25,27])).
% 71.66/71.78 cnf(9466,plain,
% 71.66/71.78 (P2(f7(a2,a2),a2,f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9446,9379,9442,9434,9342,9389,9381,9130,42,659,23,26,25,27,28])).
% 71.66/71.78 cnf(9468,plain,
% 71.66/71.78 (~P4(f3(a4,a4),a1,a2)),
% 71.66/71.78 inference(scs_inference,[],[9446,9379,9442,9434,9167,9294,9342,9389,9098,9381,9130,42,659,23,26,25,27,28,30])).
% 71.66/71.78 cnf(9470,plain,
% 71.66/71.78 (P4(f3(a4,a4),f3(a1,a1),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9446,9379,9442,9424,9434,9167,9316,9277,9294,9342,9389,9098,9381,9130,42,659,23,26,25,27,28,30,29])).
% 71.66/71.78 cnf(9472,plain,
% 71.66/71.78 (P4(f7(a4,a4),f7(a1,a1),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9446,9379,9442,9424,9434,9167,9316,9277,9294,9342,9389,9098,9381,9130,42,659,23,26,25,27,28,30,29,22])).
% 71.66/71.78 cnf(9476,plain,
% 71.66/71.78 (P2(a2,f7(a2,a2),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9466,23])).
% 71.66/71.78 cnf(9478,plain,
% 71.66/71.78 (P4(f3(a1,a1),f3(a4,a4),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9470,9466,23,22])).
% 71.66/71.78 cnf(9480,plain,
% 71.66/71.78 (P4(f3(a4,a4),f7(a1,a1),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9470,9466,9358,23,22,26])).
% 71.66/71.78 cnf(9482,plain,
% 71.66/71.78 (~P4(a4,f3(a1,a1),a1)),
% 71.66/71.78 inference(scs_inference,[],[9470,9466,9364,9358,9094,23,22,26,25])).
% 71.66/71.78 cnf(9484,plain,
% 71.66/71.78 (~P2(a4,a4,f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9470,9466,9364,9358,9360,9094,35,23,22,26,25,27])).
% 71.66/71.78 cnf(9486,plain,
% 71.66/71.78 (P2(f3(a1,a1),a2,f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9470,9458,9466,9364,9358,9360,9094,35,23,22,26,25,27,28])).
% 71.66/71.78 cnf(9488,plain,
% 71.66/71.78 (~P4(f3(a2,a2),f3(a2,a2),a2)),
% 71.66/71.78 inference(scs_inference,[],[9470,9458,9464,9466,9364,9358,9165,9360,9094,35,23,22,26,25,27,28,30])).
% 71.66/71.78 cnf(9494,plain,
% 71.66/71.78 (P2(a2,f3(a1,a1),f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9486,23])).
% 71.66/71.78 cnf(9496,plain,
% 71.66/71.78 (P4(f7(a1,a1),f3(a4,a4),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9480,9486,23,22])).
% 71.66/71.78 cnf(9500,plain,
% 71.66/71.78 (~P4(f3(a2,a2),f5(a2),f5(a1))),
% 71.66/71.78 inference(scs_inference,[],[9028,9480,9100,9486,9046,9134,9332,3646,23,22,26,25])).
% 71.66/71.78 cnf(9502,plain,
% 71.66/71.78 (P2(a2,f3(a2,a2),f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9028,9480,9399,9100,9476,9486,9046,9134,9332,3646,23,22,26,25,27])).
% 71.66/71.78 cnf(9504,plain,
% 71.66/71.78 (P2(f7(a1,a1),a2,f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9028,9480,9399,9100,9476,9486,9466,9409,9046,9134,9332,3646,23,22,26,25,27,28])).
% 71.66/71.78 cnf(9509,plain,
% 71.66/71.78 (~P2(f3(a1,a1),a2,f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[9028,9480,9399,9411,9100,9476,9486,9082,9464,9466,9225,9409,9046,9134,9332,9094,3646,23,22,26,25,27,28,30,29])).
% 71.66/71.78 cnf(9511,plain,
% 71.66/71.78 (P4(f5(a2),f5(a1),f5(a2))),
% 71.66/71.78 inference(scs_inference,[],[9032,8987])).
% 71.66/71.78 cnf(9513,plain,
% 71.66/71.78 (P2(a2,f7(a1,a1),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9504,9032,8987,23])).
% 71.66/71.78 cnf(9515,plain,
% 71.66/71.78 (P4(f5(a1),f5(a2),f5(a2))),
% 71.66/71.78 inference(scs_inference,[],[9504,9032,8987,23,22])).
% 71.66/71.78 cnf(9517,plain,
% 71.66/71.78 (~P4(a2,a1,f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9504,9444,9032,9084,8987,23,22,26])).
% 71.66/71.78 cnf(9519,plain,
% 71.66/71.78 (P4(f5(a1),f3(a4,a4),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9504,9444,9118,9032,9026,9084,8987,23,22,26,25])).
% 71.66/71.78 cnf(9521,plain,
% 71.66/71.78 (~P2(f7(a1,a1),f7(a4,a4),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9452,9504,9444,9118,9032,9026,9044,9098,9084,8987,23,22,26,25,27])).
% 71.66/71.78 cnf(9523,plain,
% 71.66/71.78 (~P2(f7(a2,a2),f7(a2,a2),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9452,9504,9444,9244,9118,9032,9026,9044,9098,9084,8987,23,22,26,25,27,28])).
% 71.66/71.78 cnf(9525,plain,
% 71.66/71.78 (~P4(a4,a1,f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9484,9452,9504,9444,9244,9118,9314,9032,9026,9044,9098,9084,9124,9034,8987,23,22,26,25,27,28,30])).
% 71.66/71.78 cnf(9527,plain,
% 71.66/71.78 (~P2(a1,a1,a4)),
% 71.66/71.78 inference(scs_inference,[],[9484,9452,9504,9444,9370,9244,9118,9314,9086,9032,9026,9044,9098,9084,9124,9050,9034,8987,23,22,26,25,27,28,30,29])).
% 71.66/71.78 cnf(9533,plain,
% 71.66/71.78 (P2(a2,f7(a4,a4),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9142,23])).
% 71.66/71.78 cnf(9535,plain,
% 71.66/71.78 (P4(f3(a4,a4),f5(a1),f3(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9519,9142,23,22])).
% 71.66/71.78 cnf(9539,plain,
% 71.66/71.78 (~P4(a4,f7(a1,a1),a1)),
% 71.66/71.78 inference(scs_inference,[],[9511,9519,9480,9142,9058,9364,9332,9094,23,22,26,25])).
% 71.66/71.78 cnf(9541,plain,
% 71.66/71.78 (~P2(f7(a1,a1),a2,f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9523,9511,9519,9480,9142,9058,9504,9364,9420,9332,9094,23,22,26,25,27])).
% 71.66/71.78 cnf(9543,plain,
% 71.66/71.78 (P2(f3(a2,a2),f6(a2),f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9523,9511,9519,9480,9252,9142,9058,9221,9504,9364,9420,9126,9332,9094,23,22,26,25,27,28])).
% 71.66/71.78 cnf(9545,plain,
% 71.66/71.78 (~P4(f3(a1,a1),f3(a4,a4),a2)),
% 71.66/71.78 inference(scs_inference,[],[9523,9478,9511,9519,9480,9252,9142,9368,9058,9221,9504,9364,9269,9420,9464,9126,9332,9094,23,22,26,25,27,28,30])).
% 71.66/71.78 cnf(9556,plain,
% 71.66/71.78 (~P4(f7(a1,a1),f3(a4,a4),a2)),
% 71.66/71.78 inference(scs_inference,[],[9543,9545,9478,9342,23,26])).
% 71.66/71.78 cnf(9562,plain,
% 71.66/71.78 (P2(f7(a1,a1),a4,f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9521,9281,9543,9533,9545,9478,9504,9342,9360,9050,9078,23,26,25,27,28])).
% 71.66/71.78 cnf(9564,plain,
% 71.66/71.78 (~P4(f3(a4,a4),f3(a4,a4),a2)),
% 71.66/71.78 inference(scs_inference,[],[9521,9281,9543,9533,9545,9478,9122,9504,9342,9360,9464,9050,9078,9094,23,26,25,27,28,30])).
% 71.66/71.78 cnf(9573,plain,
% 71.66/71.78 (P2(f7(a2,a2),a4,f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9217,23])).
% 71.66/71.78 cnf(9575,plain,
% 71.66/71.78 (~P4(a1,a4,f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9525,9217,9096,9124,23,26])).
% 71.66/71.78 cnf(9577,plain,
% 71.66/71.78 (P4(f7(a1,a1),f3(a2,a2),f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9525,9217,9158,9205,9096,9124,23,26,25])).
% 71.66/71.78 cnf(9579,plain,
% 71.66/71.78 (~P2(a1,a2,a4)),
% 71.66/71.78 inference(scs_inference,[],[9426,9525,9217,9158,9466,9205,9324,9096,9124,23,26,25,27])).
% 71.66/71.78 cnf(9581,plain,
% 71.66/71.78 (~P2(f6(a2),a4,a1)),
% 71.66/71.78 inference(scs_inference,[],[9426,9525,9217,9158,9334,9466,9042,9205,9324,9096,9124,23,26,25,27,28])).
% 71.66/71.78 cnf(9587,plain,
% 71.66/71.78 (P4(f3(a2,a2),f7(a1,a1),f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9527,9169,9564,9426,9525,9217,9158,9334,9466,9401,9030,9042,9205,9324,9096,9124,9134,23,26,25,27,28,30,29,22])).
% 71.66/71.78 cnf(9590,plain,
% 71.66/71.78 (P2(f6(a2),a4,f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9242,23])).
% 71.66/71.78 cnf(9592,plain,
% 71.66/71.78 (~P2(f7(a1,a1),a4,f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9562,9523,9242,9420,23,27])).
% 71.66/71.78 cnf(9594,plain,
% 71.66/71.78 (~P4(a1,a2,f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9562,9517,9523,9242,9420,9084,9050,23,27,26])).
% 71.66/71.78 cnf(9596,plain,
% 71.66/71.78 (~P4(a2,f7(a1,a1),a1)),
% 71.66/71.78 inference(scs_inference,[],[9587,9562,9517,9523,9242,9420,9084,9050,9134,23,27,26,25])).
% 71.66/71.78 cnf(9598,plain,
% 71.66/71.78 (~P2(f5(a2),a2,a1)),
% 71.66/71.78 inference(scs_inference,[],[6,9587,9562,9517,9523,9242,9389,9420,9084,9120,9050,9134,9060,23,27,26,25,29])).
% 71.66/71.78 cnf(9600,plain,
% 71.66/71.78 (~P4(f3(a1,a1),f7(a1,a1),f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[6,9587,9509,9562,9517,9523,9358,9242,9486,9389,9420,9504,9084,9120,9050,9134,9060,23,27,26,25,29,30])).
% 71.66/71.78 cnf(9602,plain,
% 71.66/71.78 (~P2(f6(a2),a4,a2)),
% 71.66/71.78 inference(scs_inference,[],[6,9587,9509,9562,9517,9523,9358,9242,9486,9389,9420,9504,9084,9120,9050,9134,9060,23,27,26,25,29,30,7128])).
% 71.66/71.78 cnf(9604,plain,
% 71.66/71.78 (P4(f5(a2),f7(a1,a1),f5(a2))),
% 71.66/71.78 inference(scs_inference,[],[6,9587,9509,9562,9517,9523,9358,9242,9486,9389,9420,9504,9381,9084,9120,9050,9134,9060,23,27,26,25,29,30,7128,8987])).
% 71.66/71.78 cnf(9606,plain,
% 71.66/71.78 (P4(f7(a1,a1),f5(a2),f5(a2))),
% 71.66/71.78 inference(scs_inference,[],[6,9587,9509,9562,9517,9523,9358,9242,9486,9389,9420,9504,9381,9084,9120,9050,9134,9060,23,27,26,25,29,30,7128,8987,22])).
% 71.66/71.78 cnf(9611,plain,
% 71.66/71.78 (P2(f6(a4),a4,f6(a4))),
% 71.66/71.78 inference(scs_inference,[],[9265,23])).
% 71.66/71.78 cnf(9613,plain,
% 71.66/71.78 (~P2(f7(a1,a1),a4,a4)),
% 71.66/71.78 inference(scs_inference,[],[9521,9292,9265,23,27])).
% 71.66/71.78 cnf(9617,plain,
% 71.66/71.78 (~P4(a4,f5(a4),a4)),
% 71.66/71.78 inference(scs_inference,[],[9366,9385,9521,9292,9265,9511,9078,9332,608,23,27,26,25])).
% 71.66/71.78 cnf(9619,plain,
% 71.66/71.78 (~P2(f6(a2),a4,f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9422,9366,9385,9590,9521,9292,9265,9511,9238,9034,9078,9332,608,23,27,26,25,29])).
% 71.66/71.78 cnf(9621,plain,
% 71.66/71.78 (~P4(f3(a4,a4),f5(a1),a2)),
% 71.66/71.78 inference(scs_inference,[],[9535,9422,9366,9385,9590,9521,9292,9265,9511,9269,9464,9238,9034,9078,9332,3665,608,23,27,26,25,29,30])).
% 71.66/71.78 cnf(9625,plain,
% 71.66/71.78 (P2(f6(a2),a4,f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9229,23])).
% 71.66/71.78 cnf(9627,plain,
% 71.66/71.78 (~P2(f5(a2),a4,a1)),
% 71.66/71.78 inference(scs_inference,[],[9598,9229,9360,2702,23,27])).
% 71.66/71.78 cnf(9629,plain,
% 71.66/71.78 (~P4(f5(a2),f7(a1,a1),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9598,9604,9322,9219,9229,9360,2702,23,27,26])).
% 71.66/71.78 cnf(9631,plain,
% 71.66/71.78 (~P4(f7(a1,a1),f3(a2,a2),a2)),
% 71.66/71.78 inference(scs_inference,[],[9577,9598,9604,9322,9594,9219,9229,9189,9360,2702,23,27,26,25])).
% 71.66/71.78 cnf(9633,plain,
% 71.66/71.78 (~P2(f7(a1,a1),a4,a2)),
% 71.66/71.78 inference(scs_inference,[],[9577,9405,9598,9604,9322,9594,9562,9144,9219,9229,9189,9360,2702,23,27,26,25,29])).
% 71.66/71.78 cnf(9635,plain,
% 71.66/71.78 (~P4(f3(a2,a2),f3(a2,a2),a4)),
% 71.66/71.78 inference(scs_inference,[],[7,9577,9405,9598,9604,9322,9594,9543,9562,9144,9219,9229,9189,9360,2702,23,27,26,25,29,30])).
% 71.66/71.78 cnf(9642,plain,
% 71.66/71.78 (P2(f6(a2),a2,f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9625,9142,9334,9346,23,27])).
% 71.66/71.78 cnf(9644,plain,
% 71.66/71.78 (~P4(f7(a1,a1),f5(a2),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9629,9625,9606,9604,9142,9334,9346,23,27,26])).
% 71.66/71.78 cnf(9650,plain,
% 71.66/71.78 (~P4(f7(a4,a4),a1,a2)),
% 71.66/71.78 inference(scs_inference,[],[9602,9488,9629,9625,9606,9502,9444,9587,9604,9142,9334,9267,9346,9034,9134,23,27,26,25,29,30])).
% 71.66/71.78 cnf(9655,plain,
% 71.66/71.78 (P2(a2,f6(a2),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9642,23])).
% 71.66/71.78 cnf(9657,plain,
% 71.66/71.78 (~P2(a1,a1,f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9642,9452,9060,23,27])).
% 71.66/71.78 cnf(9659,plain,
% 71.66/71.78 (P2(a4,a2,f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9642,9452,9533,9126,9060,23,27,28])).
% 71.66/71.78 cnf(9661,plain,
% 71.66/71.78 (~P4(f7(a1,a1),f3(a1,a1),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9450,9642,9452,9533,9219,9126,9046,9060,23,27,28,26])).
% 71.66/71.78 cnf(9663,plain,
% 71.66/71.78 (~P4(f5(a4),a1,f3(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9482,9450,9642,9452,9533,9219,9024,9126,9046,9401,9060,23,27,28,26,25])).
% 71.66/71.78 cnf(9665,plain,
% 71.66/71.78 (~P2(f5(a2),a2,f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9482,9644,9450,9642,9452,9533,9606,9219,9504,9024,9126,9046,9401,9060,2702,23,27,28,26,25,29])).
% 71.66/71.78 cnf(9667,plain,
% 71.66/71.78 (~P4(f6(a2),a1,a1)),
% 71.66/71.78 inference(scs_inference,[],[9581,9482,9644,9450,9642,9452,9533,9606,9590,9219,9504,9267,9024,9126,9046,9401,9060,9034,2702,23,27,28,26,25,29,30])).
% 71.66/71.78 cnf(9672,plain,
% 71.66/71.78 (P2(a2,a4,f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9659,23])).
% 71.66/71.78 cnf(9675,plain,
% 71.66/71.78 (P2(x96751,x96752,x96753)+~P2(x96751,x96754,x96755)+~P2(x96755,x96756,x96753)+~P2(x96754,x96756,x96752)),
% 71.66/71.78 inference(rename_variables,[],[27])).
% 71.66/71.78 cnf(9676,plain,
% 71.66/71.78 (~P4(f7(a4,a4),f7(a1,a1),a2)),
% 71.66/71.78 inference(scs_inference,[],[9627,9650,9659,9472,9219,9126,2702,23,27,26])).
% 71.66/71.78 cnf(9678,plain,
% 71.66/71.78 (~P4(f3(a2,a2),a1,a2)),
% 71.66/71.78 inference(scs_inference,[],[9627,9650,9659,9472,9312,9594,9219,9158,9126,2702,23,27,26,25])).
% 71.66/71.78 cnf(9680,plain,
% 71.66/71.78 (P4(f5(a4),f7(a4,a4),a1)),
% 71.66/71.78 inference(scs_inference,[],[9627,9650,9659,9472,9312,9594,9219,9158,9126,9078,9060,2702,2138,23,27,26,25,29])).
% 71.66/71.78 cnf(9682,plain,
% 71.66/71.78 (~P4(f7(a4,a4),f7(a1,a1),a1)),
% 71.66/71.78 inference(scs_inference,[],[9627,9650,9659,9472,9312,9352,9594,9336,9562,9219,9158,9126,9078,9060,2702,2138,23,27,26,25,29,30])).
% 71.66/71.78 cnf(9684,plain,
% 71.66/71.78 (P4(f7(a4,a4),f5(a4),a1)),
% 71.66/71.78 inference(scs_inference,[],[9627,9650,9659,9472,9312,9352,9594,9336,9562,9219,9158,9126,9078,9060,2702,2138,23,27,26,25,29,30,22])).
% 71.66/71.78 cnf(9686,plain,
% 71.66/71.78 (~P2(a2,x96861,f6(a2))+~P2(f7(a4,a4),x96861,a4)),
% 71.66/71.78 inference(scs_inference,[],[7,9627,9650,9659,9472,9312,9352,9594,9336,9562,9219,9158,9126,9078,9060,2702,2138,23,27,26,25,29,30,22,9675])).
% 71.66/71.78 cnf(9688,plain,
% 71.66/71.78 (~P4(f5(a4),f7(a4,a4),a2)),
% 71.66/71.78 inference(scs_inference,[],[7,9627,9650,9659,9472,9312,9352,9594,9336,9562,9219,9158,9126,9078,9060,2702,2138,23,27,26,25,29,30,22,9675,8990])).
% 71.66/71.78 cnf(9690,plain,
% 71.66/71.78 (P2(a4,f6(a4),a4)),
% 71.66/71.78 inference(scs_inference,[],[9156,23])).
% 71.66/71.78 cnf(9692,plain,
% 71.66/71.78 (P2(f7(a4,a4),f7(a1,a1),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9104,9156,9044,23,27])).
% 71.66/71.78 cnf(9694,plain,
% 71.66/71.78 (P4(f7(a4,a4),f5(a4),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9684,9462,9104,9219,9156,9044,23,27,26])).
% 71.66/71.78 cnf(9696,plain,
% 71.66/71.78 (~P4(a4,f7(a4,a4),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9539,9684,9462,9104,9219,9156,9044,23,27,26,25])).
% 71.66/71.78 cnf(9700,plain,
% 71.66/71.78 (~P4(f3(a1,a1),f3(a1,a1),a4)),
% 71.66/71.78 inference(scs_inference,[],[7,9600,9539,9684,9462,9368,9428,9358,9562,9104,9219,9156,9044,23,27,26,25,29,30])).
% 71.66/71.78 cnf(9702,plain,
% 71.66/71.78 (P4(f5(a4),f7(a4,a4),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[7,9600,9539,9684,9462,9368,9428,9358,9562,9104,9219,9156,9044,23,27,26,25,29,30,22])).
% 71.66/71.78 cnf(9704,plain,
% 71.66/71.78 (P2(f7(a1,a1),f7(a4,a4),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9692,23])).
% 71.66/71.78 cnf(9706,plain,
% 71.66/71.78 (~P2(a4,f7(a1,a1),a4)),
% 71.66/71.78 inference(scs_inference,[],[9692,9619,9625,23,27])).
% 71.66/71.78 cnf(9708,plain,
% 71.66/71.78 (P2(f7(a2,a2),f6(a4),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9692,9573,9619,9690,9625,23,27,28])).
% 71.66/71.78 cnf(9710,plain,
% 71.66/71.78 (~P4(a1,f7(a1,a1),a2)),
% 71.66/71.78 inference(scs_inference,[],[9692,9573,9702,9688,9619,9690,9625,608,23,27,28,26])).
% 71.66/71.78 cnf(9712,plain,
% 71.66/71.78 (~P4(f7(a4,a4),a2,f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9692,9573,9680,9702,9688,9619,9690,9625,9050,608,23,27,28,26,25])).
% 71.66/71.78 cnf(9714,plain,
% 71.66/71.78 (~P4(a2,f7(a1,a1),a2)),
% 71.66/71.78 inference(scs_inference,[],[9692,9573,9680,9702,9688,9672,9676,9619,9690,9625,9360,9562,9050,608,23,27,28,26,25,29])).
% 71.66/71.78 cnf(9716,plain,
% 71.66/71.78 (~P4(f7(a4,a4),f5(a4),a4)),
% 71.66/71.78 inference(scs_inference,[],[9579,9692,9573,9680,9702,9688,9672,9676,9619,9690,9684,9625,9142,9360,9562,9050,608,2138,23,27,28,26,25,29,30])).
% 71.66/71.78 cnf(9718,plain,
% 71.66/71.78 (P2(f6(a4),f7(a2,a2),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9708,23])).
% 71.66/71.78 cnf(9720,plain,
% 71.66/71.78 (~P2(f6(a4),f6(a4),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[7,9708,9690,23,27])).
% 71.66/71.78 cnf(9722,plain,
% 71.66/71.78 (P2(f6(a4),f6(a4),f6(a4))),
% 71.66/71.78 inference(scs_inference,[],[7,9708,9611,9690,23,27,28])).
% 71.66/71.78 cnf(9724,plain,
% 71.66/71.78 (~P4(f5(a4),f7(a4,a4),f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[7,9348,9708,9611,9680,9690,9424,23,27,28,26])).
% 71.66/71.78 cnf(9726,plain,
% 71.66/71.78 (~P4(f7(a4,a4),f5(a4),a2)),
% 71.66/71.78 inference(scs_inference,[],[7,9694,9348,9708,9611,9680,9403,9690,9462,9424,23,27,28,26,25])).
% 71.66/71.78 cnf(9728,plain,
% 71.66/71.78 (~P2(f3(a2,a2),f7(a4,a4),a2)),
% 71.66/71.78 inference(scs_inference,[],[7,9704,9694,9348,9708,9714,9611,9680,9403,9690,9462,9424,9587,23,27,28,26,25,29])).
% 71.66/71.78 cnf(9730,plain,
% 71.66/71.78 (~P4(f7(a4,a4),f5(a4),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[7,9704,9694,9541,9348,9708,9714,9611,9680,9403,9690,9462,9424,9587,9142,2138,23,27,28,26,25,29,30])).
% 71.66/71.78 cnf(9732,plain,
% 71.66/71.78 (P2(f7(a2,a2),a1,a1)),
% 71.66/71.78 inference(scs_inference,[],[9324,23])).
% 71.66/71.78 cnf(9734,plain,
% 71.66/71.78 (~P2(f7(a1,a1),f7(a4,a4),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9704,9523,9420,9324,23,27])).
% 71.66/71.78 cnf(9736,plain,
% 71.66/71.78 (P2(f7(a1,a1),f6(a2),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9655,9704,9523,9420,9504,9324,23,27,28])).
% 71.66/71.78 cnf(9740,plain,
% 71.66/71.78 (~P4(f7(a4,a4),f5(a4),f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[9621,9682,9655,9704,9702,9535,9519,9523,9680,9420,9504,9324,23,27,28,26,25])).
% 71.66/71.78 cnf(9742,plain,
% 71.66/71.78 (~P2(f6(a4),f7(a2,a2),a1)),
% 71.66/71.78 inference(scs_inference,[],[9621,9718,9682,9655,9704,9702,9300,9535,9519,9523,9680,9263,9420,9504,9324,23,27,28,26,25,29])).
% 71.66/71.78 cnf(9747,plain,
% 71.66/71.78 (P2(f6(a2),f7(a1,a1),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9736,23])).
% 71.66/71.78 cnf(9753,plain,
% 71.66/71.78 (~P4(f7(a1,a1),a1,f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9730,9468,9736,9619,9102,9694,9470,3663,23,27,26,25])).
% 71.66/71.78 cnf(9757,plain,
% 71.66/71.78 (~P4(f3(a4,a4),f3(a4,a4),a4)),
% 71.66/71.78 inference(scs_inference,[],[7,9730,9468,9736,9710,9732,9619,9102,9694,9240,9302,9470,9044,3663,23,27,26,25,29,30])).
% 71.66/71.78 cnf(9759,plain,
% 71.66/71.78 (~P2(f7(a1,a1),a2,a4)),
% 71.66/71.78 inference(scs_inference,[],[9613,9736,9042,27])).
% 71.66/71.78 cnf(9761,plain,
% 71.66/71.78 (~P4(f5(a4),f7(a4,a4),f6(a2))),
% 71.66/71.78 inference(scs_inference,[],[9661,9613,9736,9702,9424,9042,27,26])).
% 71.66/71.78 cnf(9763,plain,
% 71.66/71.78 (~P4(f5(a4),f7(a2,a2),f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[9661,9613,9730,9736,9702,9424,9684,9215,9042,27,26,25])).
% 71.66/71.78 cnf(9765,plain,
% 71.66/71.78 (~P4(a2,f5(a4),a4)),
% 71.66/71.78 inference(scs_inference,[],[9661,9716,9613,9730,9672,9736,9702,9424,9684,9215,9314,9042,3678,27,26,25,29])).
% 71.66/71.78 cnf(9767,plain,
% 71.66/71.78 (~P4(f7(a1,a1),f7(a1,a1),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9734,9661,9716,9613,9730,9672,9736,9702,9424,9144,9684,9215,9314,9704,9042,3678,27,26,25,29,30])).
% 71.66/71.78 cnf(9777,plain,
% 71.66/71.78 (~P2(a1,f7(a4,a4),a4)),
% 71.66/71.78 inference(scs_inference,[],[9148,9732,9098,27])).
% 71.66/71.78 cnf(9779,plain,
% 71.66/71.78 (~P2(f6(a4),a2,f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9148,9541,9732,9718,9130,9098,27,28])).
% 71.66/71.78 cnf(9783,plain,
% 71.66/71.78 (~P4(a4,f7(a1,a1),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9696,9148,9541,9676,9732,9718,9472,9462,9130,9098,27,28,26,25])).
% 71.66/71.78 cnf(9787,plain,
% 71.66/71.78 (~P4(f5(a4),f7(a4,a4),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9592,9696,9740,9148,9541,9676,9732,9718,9472,9462,9702,9336,9130,9098,9096,2032,3678,27,28,26,25,29,30])).
% 71.66/71.78 cnf(9791,plain,
% 71.66/71.78 (P2(f3(a2,a2),f6(a4),f3(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9283,9708,9476,9296,9324,27,28])).
% 71.66/71.78 cnf(9793,plain,
% 71.66/71.78 (~P4(a1,a1,f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9787,9283,9708,9476,9296,9680,9324,608,27,28,26])).
% 71.66/71.78 cnf(9795,plain,
% 71.66/71.78 (~P4(f7(a4,a4),f7(a2,a2),f7(a4,a4))),
% 71.66/71.78 inference(scs_inference,[],[9787,9283,9708,9476,9296,9680,9215,9324,608,27,28,26,25])).
% 71.66/71.78 cnf(9797,plain,
% 71.66/71.78 (~P2(f3(a2,a2),f7(a2,a2),a2)),
% 71.66/71.78 inference(scs_inference,[],[9631,9787,9283,9708,9577,9476,9296,9680,9409,9215,9324,608,27,28,26,25,29])).
% 71.66/71.78 cnf(9799,plain,
% 71.66/71.78 (~P4(f3(a1,a1),a1,f5(a4))),
% 71.66/71.78 inference(scs_inference,[],[9631,9787,9283,9708,9577,9476,9296,9231,9102,9680,9409,9215,9346,9098,9324,608,27,28,26,25,29,30])).
% 71.66/71.78 cnf(9803,plain,
% 71.66/71.78 (~P2(f7(a2,a2),f7(a1,a1),a4)),
% 71.66/71.78 inference(scs_inference,[],[9706,9217,9420,27])).
% 71.66/71.78 cnf(9805,plain,
% 71.66/71.78 (P2(f7(a4,a4),f7(a2,a2),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9706,9476,9217,9672,9420,27,28])).
% 71.66/71.78 cnf(9809,plain,
% 71.66/71.78 (~P4(f3(a1,a1),f3(a1,a1),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9795,9726,9706,9476,9217,9434,9694,9672,9424,9420,27,28,26,25])).
% 71.66/71.78 cnf(9811,plain,
% 71.66/71.78 (~P2(f3(a1,a1),f7(a2,a2),a4)),
% 71.66/71.78 inference(scs_inference,[],[9795,9700,9726,9706,9458,9476,9217,9434,9694,9672,9225,9424,9420,27,28,26,25,29])).
% 71.66/71.78 cnf(9815,plain,
% 71.66/71.78 (P2(f7(a2,a2),f7(a4,a4),f7(a2,a2))),
% 71.66/71.78 inference(scs_inference,[],[9795,9728,9700,9726,9706,9458,9476,9533,9217,9434,9694,9672,9225,9424,9420,9134,27,28,26,25,29,30,23])).
% 71.66/71.78 cnf(9818,plain,
% 71.66/71.78 (~P2(f6(a4),f6(a4),f5(a1))),
% 71.66/71.78 inference(scs_inference,[],[9407,9690,27])).
% 71.66/71.78 cnf(9820,plain,
% 71.66/71.78 (~P2(f7(a2,a2),f6(a2),f7(a1,a1))),
% 71.66/71.78 inference(scs_inference,[],[9407,9573,9541,9690,9042,27,28])).
% 71.66/71.78 cnf(9822,plain,
% 71.66/71.78 (~P4(f3(a1,a1),f7(a4,a4),a2)),
% 71.66/71.78 inference(scs_inference,[],[9407,9650,9573,9541,9193,9434,9690,9042,27,28,26])).
% 71.66/71.78 cnf(9824,plain,
% 71.66/71.78 (~P4(f7(a4,a4),f3(a1,a1),a1)),
% 71.66/71.78 inference(scs_inference,[],[9663,9407,9650,9573,9541,9193,9434,9342,9702,9690,9042,27,28,26,25])).
% 71.66/71.78 cnf(9826,plain,
% 71.66/71.78 (~P2(f3(a2,a2),f7(a1,a1),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9767,9663,9513,9407,9650,9573,9541,9193,9434,9342,9702,9690,9042,9134,27,28,26,25,29])).
% 71.66/71.79 cnf(9830,plain,
% 71.66/71.79 (~P2(f3(a2,a2),f7(a1,a1),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9805,9826,9409,27])).
% 71.66/71.79 cnf(9832,plain,
% 71.66/71.79 (P2(f7(a2,a2),f7(a2,a2),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9805,9815,9826,9223,9409,27,28])).
% 71.66/71.79 cnf(9836,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f5(a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9417,9805,9815,9826,9724,9223,9680,9684,9409,9084,608,27,28,26,25])).
% 71.66/71.79 cnf(9838,plain,
% 71.66/71.79 (~P2(f7(a2,a2),a1,f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9417,9805,9815,9826,9724,9753,9732,9223,9680,9684,9409,9215,9084,9044,608,27,28,26,25,29])).
% 71.66/71.79 cnf(9840,plain,
% 71.66/71.79 (~P4(f7(a4,a4),a1,f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[9417,9805,9815,9826,9350,9724,9753,9732,9223,9659,9680,9684,9409,9215,9084,9124,9044,9060,608,27,28,26,25,29,30])).
% 71.66/71.79 cnf(9842,plain,
% 71.66/71.79 (~P2(f7(a2,a2),f7(a1,a1),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[9832,9820,9420,27])).
% 71.66/71.79 cnf(9844,plain,
% 71.66/71.79 (P2(f7(a2,a2),f6(a2),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9832,9820,9815,9655,9466,9420,27,28])).
% 71.66/71.79 cnf(9846,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f5(a4),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9832,9820,9836,9815,9655,9472,9466,9420,27,28,26])).
% 71.66/71.79 cnf(9848,plain,
% 71.66/71.79 (P4(f5(a1),f6(a4),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[9832,9820,9836,9815,9655,9472,9263,9466,9026,9420,27,28,26,25])).
% 71.66/71.79 cnf(9852,plain,
% 71.66/71.79 (~P4(a1,f3(a4,a4),a2)),
% 71.66/71.79 inference(scs_inference,[],[9832,9820,9836,9815,9655,9171,9300,9472,9263,9118,9466,9026,9464,9420,9215,9324,27,28,26,25,29,30])).
% 71.66/71.79 cnf(9855,plain,
% 71.66/71.79 (P2(f6(a2),f7(a2,a2),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9832,9820,9836,9815,9655,9171,9300,9472,9263,9118,9466,9026,9464,9420,9215,9324,27,28,26,25,29,30,23])).
% 71.66/71.79 cnf(9857,plain,
% 71.66/71.79 (P4(f6(a4),f5(a1),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[9832,9820,9836,9815,9655,9171,9300,9472,9263,9118,9466,9026,9464,9420,9215,9324,27,28,26,25,29,30,23,22])).
% 71.66/71.79 cnf(9859,plain,
% 71.66/71.79 (~P2(f6(a2),f6(a2),a1)),
% 71.66/71.79 inference(scs_inference,[],[9844,9838,27])).
% 71.66/71.79 cnf(9861,plain,
% 71.66/71.79 (P2(f7(a4,a4),a2,f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9844,9855,9838,9642,9130,27,28])).
% 71.66/71.79 cnf(9863,plain,
% 71.66/71.79 (~P4(a2,f7(a1,a1),f3(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9460,9844,9855,9838,9642,9189,9130,9120,27,28,25])).
% 71.66/71.79 cnf(9865,plain,
% 71.66/71.79 (~P4(a1,f7(a4,a4),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[9460,9840,9844,9855,9838,9642,9193,9163,9189,9130,9120,27,28,25,26])).
% 71.66/71.79 cnf(9867,plain,
% 71.66/71.79 (~P2(f3(a1,a1),f3(a4,a4),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9809,9460,9840,9844,9855,9838,9316,9642,9193,9163,9225,9189,9130,9120,27,28,25,26,29])).
% 71.66/71.79 cnf(9869,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f7(a1,a1),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9809,9830,9460,9840,9844,9855,9838,9513,9316,9642,9193,9163,9225,9189,9130,9120,9134,27,28,25,26,29,30])).
% 71.66/71.79 cnf(9871,plain,
% 71.66/71.79 (P2(a2,f7(a4,a4),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9809,9830,9460,9840,9844,9855,9838,9513,9316,9642,9193,9163,9225,9189,9130,9120,9134,27,28,25,26,29,30,23])).
% 71.66/71.79 cnf(9874,plain,
% 71.66/71.79 (~P2(f3(a1,a1),f3(a4,a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9867,9861,9110,27])).
% 71.66/71.79 cnf(9876,plain,
% 71.66/71.79 (P2(f7(a4,a4),f6(a2),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9867,9861,9844,9110,9223,27,28])).
% 71.66/71.79 cnf(9878,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f3(a1,a1),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9867,9869,9861,9844,9110,9223,9358,9424,27,28,26])).
% 71.66/71.79 cnf(9880,plain,
% 71.66/71.79 (~P4(f5(a4),f7(a1,a1),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9867,9869,9783,9861,9844,9110,9223,9358,9424,9189,9401,27,28,26,25])).
% 71.66/71.79 cnf(9882,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f5(a2),a2)),
% 71.66/71.79 inference(scs_inference,[],[9867,9869,9391,9783,9861,9844,9110,9223,9358,9389,9424,9189,9401,2702,27,28,26,25,29])).
% 71.66/71.79 cnf(9886,plain,
% 71.66/71.79 (P2(f6(a2),f7(a4,a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9867,9869,9391,9340,9783,9861,9844,9110,9223,9358,9389,9424,9189,9104,9401,9096,2702,27,28,26,25,29,30,23])).
% 71.66/71.79 cnf(9888,plain,
% 71.66/71.79 (~P2(a1,f6(a2),a4)),
% 71.66/71.79 inference(scs_inference,[],[9876,9777,9098,27])).
% 71.66/71.79 cnf(9890,plain,
% 71.66/71.79 (P2(f7(a4,a4),f7(a4,a4),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9871,9886,9876,9777,9655,9098,27,28])).
% 71.66/71.79 cnf(9892,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f7(a4,a4),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9878,9871,9886,9876,9777,9655,9462,9424,9098,27,28,26])).
% 71.66/71.79 cnf(9894,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f7(a1,a1),f5(a4))),
% 71.66/71.79 inference(scs_inference,[],[9878,9871,9886,9846,9876,9777,9655,9144,9462,9424,9098,27,28,26,25])).
% 71.66/71.79 cnf(9896,plain,
% 71.66/71.79 (~P2(a1,f7(a1,a1),f5(a4))),
% 71.66/71.79 inference(scs_inference,[],[9878,9871,9886,9846,9876,9880,9777,9747,9655,9144,9462,9424,9238,9098,27,28,26,25,29])).
% 71.66/71.79 cnf(9898,plain,
% 71.66/71.79 (~P2(a1,f3(a4,a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9874,9878,9871,9886,9846,9876,9880,9777,9747,9655,9144,9102,9316,9462,9434,9424,9238,9098,27,28,26,25,29,30])).
% 71.66/71.79 cnf(9900,plain,
% 71.66/71.79 (~P2(f7(a4,a4),f7(a4,a4),a1)),
% 71.66/71.79 inference(scs_inference,[],[9838,9815,27])).
% 71.66/71.79 cnf(9902,plain,
% 71.66/71.79 (~P2(f6(a2),f6(a2),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9886,9838,9815,9521,27,28])).
% 71.66/71.79 cnf(9904,plain,
% 71.66/71.79 (~P4(a2,a1,f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9863,9886,9838,9312,9815,9521,9134,27,28,25])).
% 71.66/71.79 cnf(9906,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f7(a1,a1),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9892,9863,9886,9838,9312,9815,9521,9694,9702,9134,27,28,25,26])).
% 71.66/71.79 cnf(9910,plain,
% 71.66/71.79 (~P4(f6(a4),f5(a1),a1)),
% 71.66/71.79 inference(scs_inference,[],[9892,9857,9362,9863,9805,9886,9838,9312,9815,9521,9611,9300,9694,9163,9702,9324,9134,3665,27,28,25,26,29,30])).
% 71.66/71.79 cnf(9914,plain,
% 71.66/71.79 (P2(a1,f6(a2),a1)),
% 71.66/71.79 inference(scs_inference,[],[9826,9855,9876,9409,9098,27,28])).
% 71.66/71.79 cnf(9916,plain,
% 71.66/71.79 (~P4(a1,f5(a4),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9906,9826,9855,9876,9193,9694,9409,9098,27,28,25])).
% 71.66/71.79 cnf(9918,plain,
% 71.66/71.79 (~P4(f5(a1),f6(a4),a1)),
% 71.66/71.79 inference(scs_inference,[],[9906,9848,9910,9826,9857,9855,9876,9193,9694,9409,9098,27,28,25,26])).
% 71.66/71.79 cnf(9925,plain,
% 71.66/71.79 (P2(f6(a2),a1,a1)),
% 71.66/71.79 inference(scs_inference,[],[9906,9848,9822,9910,9826,9857,9855,9876,9368,9193,9336,9694,9434,9409,9464,9098,9094,2534,27,28,25,26,30,29,23])).
% 71.66/71.79 cnf(9929,plain,
% 71.66/71.79 (~P2(f7(a4,a4),a1,f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9890,9900,9732,27])).
% 71.66/71.79 cnf(9935,plain,
% 71.66/71.79 (~P4(a1,a1,f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9890,9824,9900,9892,9706,9191,9732,9462,9219,9156,9424,27,28,26,25])).
% 71.66/71.79 cnf(9937,plain,
% 71.66/71.79 (~P2(a1,f6(a2),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9890,9824,9793,9900,9914,9892,9706,9191,9732,9462,9219,9024,9156,9424,27,28,26,25,29])).
% 71.66/71.79 cnf(9942,plain,
% 71.66/71.79 (~P2(a1,f6(a2),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[9859,9925,9914,27])).
% 71.66/71.79 cnf(9944,plain,
% 71.66/71.79 (P2(f7(a4,a4),f6(a2),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9859,9925,9890,9914,9229,9336,27,28])).
% 71.66/71.79 cnf(9946,plain,
% 71.66/71.79 (P4(f6(a4),f3(a1,a1),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[9859,9925,9890,9914,9290,9229,9336,9046,27,28,25])).
% 71.66/71.79 cnf(9948,plain,
% 71.66/71.79 (~P4(a1,f3(a2,a2),a2)),
% 71.66/71.79 inference(scs_inference,[],[9678,9859,9925,9890,9914,9290,9312,9229,9158,9336,9046,27,28,25,26])).
% 71.66/71.79 cnf(9952,plain,
% 71.66/71.79 (~P2(f7(a4,a4),f6(a2),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[9372,9678,9865,9859,9925,9890,9914,9290,9876,9312,9229,9158,9336,9163,9205,9046,9324,3663,27,28,25,26,30,29])).
% 71.66/71.79 cnf(9954,plain,
% 71.66/71.79 (P2(f6(a2),f7(a4,a4),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9372,9678,9865,9859,9925,9890,9914,9290,9876,9312,9229,9158,9336,9163,9205,9046,9324,3663,27,28,25,26,30,29,23])).
% 71.66/71.79 cnf(9956,plain,
% 71.66/71.79 (P4(f3(a1,a1),f6(a4),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[9372,9678,9865,9859,9925,9890,9914,9290,9876,9312,9229,9158,9336,9163,9205,9046,9324,3663,27,28,25,26,30,29,23,22])).
% 71.66/71.79 cnf(9958,plain,
% 71.66/71.79 (~P2(a1,a4,f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9944,9937,9242,27])).
% 71.66/71.79 cnf(9960,plain,
% 71.66/71.79 (~P4(a1,f6(a4),a1)),
% 71.66/71.79 inference(scs_inference,[],[9944,9937,9918,9848,9242,1375,27,26])).
% 71.66/71.79 cnf(9962,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f6(a2),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9944,9761,9937,9918,9848,9242,9680,9238,1375,27,26,25])).
% 71.66/71.79 cnf(9964,plain,
% 71.66/71.79 (~P4(f7(a2,a2),a1,f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9944,9761,9937,9918,9820,9848,9844,9242,9914,9240,9680,9238,1375,27,26,25,30])).
% 71.66/71.79 cnf(9966,plain,
% 71.66/71.79 (~P2(f6(a2),f7(a4,a4),a1)),
% 71.66/71.79 inference(scs_inference,[],[9944,9954,9761,9937,9918,9820,9848,9844,9242,9914,9240,9300,9680,9238,9098,1375,27,26,25,30,29])).
% 71.66/71.79 cnf(9969,plain,
% 71.66/71.79 (~P2(a1,a2,f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9958,9914,9042,27])).
% 71.66/71.79 cnf(9971,plain,
% 71.66/71.79 (P4(f7(a1,a1),f6(a4),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[9958,9956,9914,9342,9042,27,25])).
% 71.66/71.79 cnf(9973,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f6(a2),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9958,9956,9962,9914,9342,9472,9042,27,25,26])).
% 71.66/71.79 cnf(9975,plain,
% 71.66/71.79 (~P4(a1,a1,f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[9958,9956,9962,9966,9914,9342,9472,9024,9042,9098,27,25,26,30])).
% 71.66/71.79 cnf(9977,plain,
% 71.66/71.79 (~P2(a2,f7(a4,a4),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9958,9956,9962,9964,9966,9871,9914,9342,9472,9024,9042,9084,9098,27,25,26,30,29])).
% 71.66/71.79 cnf(9979,plain,
% 71.66/71.79 (P4(f6(a4),f7(a1,a1),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[9958,9956,9962,9964,9966,9871,9914,9342,9472,9024,9042,9084,9098,27,25,26,30,29,22])).
% 71.66/71.79 cnf(9983,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f7(a1,a1),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[9865,9446,9718,9684,9702,27,26])).
% 71.66/71.79 cnf(9987,plain,
% 71.66/71.79 (~P4(f7(a4,a4),a1,f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9977,9863,9865,9446,9718,9587,9533,9684,9702,9084,9098,9134,27,26,25,30])).
% 71.66/71.79 cnf(9991,plain,
% 71.66/71.79 (P2(f3(a1,a1),f6(a4),f3(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9757,9977,9863,9865,9446,9169,9718,9587,9533,9684,9702,9084,9098,9134,27,26,25,30,29,23])).
% 71.66/71.79 cnf(9993,plain,
% 71.66/71.79 (~P2(f3(a1,a1),f3(a4,a4),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[9867,9954,9294,27])).
% 71.66/71.79 cnf(9995,plain,
% 71.66/71.79 (~P4(f3(a1,a1),f7(a4,a4),a1)),
% 71.66/71.79 inference(scs_inference,[],[9935,9867,9954,9080,9294,9434,27,25])).
% 71.66/71.79 cnf(9997,plain,
% 71.66/71.79 (~P4(f5(a4),f5(a1),f3(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9799,9935,9867,9954,9080,9294,9434,9026,3663,27,25,26])).
% 71.66/71.79 cnf(9999,plain,
% 71.66/71.79 (~P4(f6(a4),f3(a1,a1),a1)),
% 71.66/71.79 inference(scs_inference,[],[9946,9203,9991,9799,9935,9867,9722,9954,9080,9294,9434,9026,3663,27,25,26,30])).
% 71.66/71.79 cnf(10008,plain,
% 71.66/71.79 (~P4(a2,f3(a1,a1),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9413,9904,9954,9736,9046,9084,27,26])).
% 71.66/71.79 cnf(10010,plain,
% 71.66/71.79 (P4(f3(a2,a2),f3(a1,a1),f3(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9413,9904,9954,9312,9736,9046,9084,27,26,25])).
% 71.66/71.79 cnf(10014,plain,
% 71.66/71.79 (~P2(f7(a4,a4),f6(a2),a1)),
% 71.66/71.79 inference(scs_inference,[],[9413,9720,9904,9946,9991,9722,9944,9954,9312,9736,9300,9914,9163,9046,9084,27,26,25,30,29])).
% 71.66/71.79 cnf(10016,plain,
% 71.66/71.79 (P4(f3(a1,a1),f3(a2,a2),f3(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9413,9720,9904,9946,9991,9722,9944,9954,9312,9736,9300,9914,9163,9046,9084,27,26,25,30,29,22])).
% 71.66/71.79 cnf(10023,plain,
% 71.66/71.79 (P2(f7(a2,a2),f6(a2),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9902,9861,9747,9704,9336,9126,27,28])).
% 71.66/71.79 cnf(10025,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f3(a1,a1),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[9902,9997,9861,9747,9080,9704,9336,9680,9126,27,28,25])).
% 71.66/71.79 cnf(10031,plain,
% 71.66/71.79 (~P2(a1,a4,f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9797,9902,9763,9987,9997,9861,9747,9476,9080,9704,9193,9336,9680,9126,9434,9134,3678,3663,27,28,25,26,30,29])).
% 71.66/71.79 cnf(10033,plain,
% 71.66/71.79 (P2(f6(a2),f7(a2,a2),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9797,9902,9763,9987,9997,9861,9747,9476,9080,9704,9193,9336,9680,9126,9434,9134,3678,3663,27,28,25,26,30,29,23])).
% 71.66/71.79 cnf(10036,plain,
% 71.66/71.79 (~P2(a1,f3(a4,a4),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9898,10023,9302,27])).
% 71.66/71.79 cnf(10038,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f7(a4,a4),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[9898,9983,10023,9302,9694,9702,27,25])).
% 71.66/71.79 cnf(10044,plain,
% 71.66/71.79 (~P4(f3(a2,a2),f3(a2,a2),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[9635,9898,9983,10023,9818,9667,9956,9991,9252,9722,9302,9267,9694,9702,9042,9238,27,25,26,30,29])).
% 71.66/71.79 cnf(10046,plain,
% 71.66/71.79 (P2(f7(a2,a2),f7(a2,a2),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9635,9898,9983,10023,10033,9818,9667,9956,9991,9252,9244,9722,9844,9302,9267,9694,9702,9042,9238,27,25,26,30,29,28])).
% 71.66/71.79 cnf(10049,plain,
% 71.66/71.79 (~P2(f7(a4,a4),f7(a1,a1),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[10046,9842,9420,27])).
% 71.66/71.79 cnf(10051,plain,
% 71.66/71.79 (P2(f7(a4,a4),f6(a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10046,9842,9708,9420,27,28])).
% 71.66/71.79 cnf(10053,plain,
% 71.66/71.79 (~P4(f3(a1,a1),f3(a2,a2),a2)),
% 71.66/71.79 inference(scs_inference,[],[10016,10046,9842,9594,9708,9080,9420,27,28,25])).
% 71.66/71.79 cnf(10057,plain,
% 71.66/71.79 (~P4(f7(a2,a2),f7(a1,a1),a1)),
% 71.66/71.79 inference(scs_inference,[],[10016,10046,9742,9842,9575,9979,9594,9708,9718,9080,9381,9409,9420,9238,27,28,25,26,30])).
% 71.66/71.79 cnf(10061,plain,
% 71.66/71.79 (P2(f6(a4),f7(a4,a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10016,10046,9742,9842,9575,9979,9344,9594,9708,9718,9389,9080,9381,9409,9420,9238,9120,2702,27,28,25,26,30,29,23])).
% 71.66/71.79 cnf(10063,plain,
% 71.66/71.79 (~P2(f7(a2,a2),f6(a2),a1)),
% 71.66/71.79 inference(scs_inference,[],[9929,10023,9805,27])).
% 71.66/71.79 cnf(10065,plain,
% 71.66/71.79 (P2(f3(a4,a4),f6(a4),f3(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10051,9929,10023,9805,9294,27,28])).
% 71.66/71.79 cnf(10069,plain,
% 71.66/71.79 (~P4(a1,f7(a2,a2),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10051,9929,9320,10023,9964,9805,9604,9240,9294,9215,659,27,28,25,26])).
% 71.66/71.79 cnf(10071,plain,
% 71.66/71.79 (~P4(f5(a2),f5(a1),a1)),
% 71.66/71.79 inference(scs_inference,[],[10051,9929,9320,9627,10023,9964,9805,9604,9511,9240,9294,9215,3665,659,2983,27,28,25,26,30])).
% 71.66/71.79 cnf(10073,plain,
% 71.66/71.79 (~P2(f6(a4),f7(a4,a4),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10061,10038,10051,9929,9971,9320,9627,10023,9964,9805,9604,9511,9240,9294,9704,9215,3665,659,2983,27,28,25,26,30,29])).
% 71.66/71.79 cnf(10075,plain,
% 71.66/71.79 (P2(f6(a4),f3(a4,a4),f3(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10061,10038,10051,9929,9971,9320,9627,10023,9964,9805,9604,9511,9240,9294,9704,9215,3665,659,2983,27,28,25,26,30,29,23])).
% 71.66/71.79 cnf(10085,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f5(a2),a1)),
% 71.66/71.79 inference(scs_inference,[],[10071,10036,9855,9606,9171,9604,9511,9120,27,25,26])).
% 71.66/71.79 cnf(10096,plain,
% 71.66/71.79 (P2(f7(a1,a1),f6(a4),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9665,10051,9360,9704,2702,27,28])).
% 71.66/71.79 cnf(10098,plain,
% 71.66/71.79 (~P4(f3(a2,a2),f3(a1,a1),a2)),
% 71.66/71.79 inference(scs_inference,[],[9665,10010,10051,9594,9158,9360,9704,2702,27,28,25])).
% 71.66/71.79 cnf(10100,plain,
% 71.66/71.79 (~P4(f5(a1),f3(a2,a2),a2)),
% 71.66/71.79 inference(scs_inference,[],[9665,9948,10010,10051,9594,9158,9360,9032,9704,9050,2702,27,28,25,26])).
% 71.66/71.79 cnf(10104,plain,
% 71.66/71.79 (P2(f6(a4),f7(a1,a1),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9665,9960,9948,10010,10051,9925,9594,9158,9360,9267,9032,9704,9050,2702,27,28,25,26,29,23])).
% 71.66/71.79 cnf(10115,plain,
% 71.66/71.79 (~P2(f3(a2,a2),f6(a4),a2)),
% 71.66/71.79 inference(scs_inference,[],[10096,10104,10053,9779,9791,9663,9840,10016,9991,9102,9193,9205,9434,27,25,26,29])).
% 71.66/71.79 cnf(10120,plain,
% 71.66/71.79 (~P2(a1,f6(a2),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10031,9861,9042,27])).
% 71.66/71.79 cnf(10122,plain,
% 71.66/71.79 (P2(f7(a4,a4),f7(a4,a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10031,10033,9871,9861,9642,9042,27,28])).
% 71.66/71.79 cnf(10126,plain,
% 71.66/71.79 (~P4(a4,f7(a4,a4),a2)),
% 71.66/71.79 inference(scs_inference,[],[9765,10098,10031,10010,10033,9871,9861,9642,9358,9684,9124,9042,27,28,25,26])).
% 71.66/71.79 cnf(10135,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f5(a4),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[10122,9973,10014,9694,9104,9462,27,25])).
% 71.66/71.79 cnf(10137,plain,
% 71.66/71.79 (~P4(f5(a1),a1,f5(a2))),
% 71.66/71.79 inference(scs_inference,[],[10122,9973,10014,9344,9515,9694,9104,9462,9120,27,25,26])).
% 71.66/71.79 cnf(10139,plain,
% 71.66/71.79 (~P4(f3(a1,a1),f3(a1,a1),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[10122,9973,9993,10014,9344,9515,9225,9316,9694,9104,9462,9120,27,25,26,30])).
% 71.66/71.79 cnf(10144,plain,
% 71.66/71.79 (~P2(f7(a1,a1),f6(a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9977,10096,9513,27])).
% 71.66/71.79 cnf(10148,plain,
% 71.66/71.79 (~P4(a1,f7(a4,a4),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10137,9906,9977,10096,9513,9606,9472,9163,9332,27,25,26])).
% 71.66/71.79 cnf(10150,plain,
% 71.66/71.79 (~P4(f6(a4),f7(a1,a1),a1)),
% 71.66/71.79 inference(scs_inference,[],[10137,9906,9203,9977,10096,9979,9513,9606,9722,9472,9163,9332,27,25,26,30])).
% 71.66/71.79 cnf(10152,plain,
% 71.66/71.79 (~P2(f3(a2,a2),f3(a2,a2),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[10044,10137,9906,9203,9977,10096,9979,9513,9502,9606,9722,9472,9163,9332,9134,27,25,26,30,29])).
% 71.66/71.79 cnf(10154,plain,
% 71.66/71.79 (~P2(f7(a1,a1),a4,f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10144,10051,9265,27])).
% 71.66/71.79 cnf(10156,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f5(a4),f5(a2))),
% 71.66/71.79 inference(scs_inference,[],[10144,9175,10051,9265,9680,608,27,25])).
% 71.66/71.79 cnf(10177,plain,
% 71.66/71.79 (~P2(f7(a1,a1),f6(a4),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[9902,10096,9747,27])).
% 71.66/71.79 cnf(10179,plain,
% 71.66/71.79 (~P4(f5(a2),f7(a1,a1),f3(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10008,9902,10096,9747,9189,9332,27,25])).
% 71.66/71.79 cnf(10183,plain,
% 71.66/71.79 (~P4(f7(a2,a2),a1,f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10008,9952,10150,9902,9979,10096,9944,9971,9747,9914,9189,9193,9332,27,25,26,30])).
% 71.66/71.79 cnf(10185,plain,
% 71.66/71.79 (~P2(f3(a1,a1),f6(a2),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[10008,10139,9952,10150,9902,9979,10096,9944,9971,9747,9428,9225,9914,9189,9193,9332,27,25,26,30,29])).
% 71.66/71.79 cnf(10187,plain,
% 71.66/71.79 (~P2(f7(a1,a1),f6(a2),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9734,9573,9625,27])).
% 71.66/71.79 cnf(10191,plain,
% 71.66/71.79 (~P4(a4,f7(a4,a4),a4)),
% 71.66/71.79 inference(scs_inference,[],[9617,9596,9734,9573,9625,9684,9124,9084,9332,27,25,26])).
% 71.66/71.79 cnf(10193,plain,
% 71.66/71.79 (~P4(f6(a4),f7(a1,a1),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[9617,9596,9734,9720,9573,9979,9625,10096,9722,9684,9124,9084,9332,27,25,26,30])).
% 71.66/71.79 cnf(10199,plain,
% 71.66/71.79 (~P4(a1,a1,f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[10177,9960,9611,10096,9024,27,25])).
% 71.66/71.79 cnf(10201,plain,
% 71.66/71.79 (~P4(f5(a1),f5(a2),f3(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10179,10177,9960,9611,9515,9604,10096,9024,27,25,26])).
% 71.66/71.79 cnf(10203,plain,
% 71.66/71.79 (~P2(f6(a2),f7(a4,a4),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10179,10148,10177,9960,9886,9611,9515,9604,10096,9024,9238,9098,27,25,26,29])).
% 71.66/71.79 cnf(10210,plain,
% 71.66/71.79 (P2(f7(a2,a2),a2,f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9318,10046,9815,9861,9914,9086,27,28])).
% 71.66/71.79 cnf(10212,plain,
% 71.66/71.79 (~P4(f6(a4),a1,a1)),
% 71.66/71.79 inference(scs_inference,[],[9318,10199,9290,10046,9815,9861,9263,9914,9086,27,28,25])).
% 71.66/71.79 cnf(10218,plain,
% 71.66/71.79 (P2(a2,f7(a2,a2),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9318,10199,10053,9910,9221,10016,9857,9290,10046,9815,9368,9861,9956,9263,9914,9086,27,28,25,26,29,23])).
% 71.66/71.79 cnf(10223,plain,
% 71.66/71.79 (~P2(f7(a1,a1),a2,f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10154,9876,9126,27])).
% 71.66/71.79 cnf(10225,plain,
% 71.66/71.79 (~P4(f7(a2,a2),f7(a1,a1),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10154,10183,9876,9240,9381,9126,27,25])).
% 71.66/71.79 cnf(10227,plain,
% 71.66/71.79 (~P4(f5(a4),f7(a4,a4),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[9999,10154,10183,9876,9240,9381,9424,9126,9680,27,25,26])).
% 71.66/71.79 cnf(10235,plain,
% 71.66/71.79 (~P2(f3(a1,a1),f7(a4,a4),a4)),
% 71.66/71.79 inference(scs_inference,[],[9811,9871,9486,27])).
% 71.66/71.79 cnf(10237,plain,
% 71.66/71.79 (~P4(a2,a1,f3(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9852,9811,9871,9486,9084,9050,27,25])).
% 71.66/71.79 cnf(10239,plain,
% 71.66/71.79 (~P4(f5(a1),a1,f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[9852,9975,9811,9871,9486,9026,9024,9084,9050,27,25,26])).
% 71.66/71.79 cnf(10241,plain,
% 71.66/71.79 (~P4(f6(a2),a1,a4)),
% 71.66/71.79 inference(scs_inference,[],[9852,9975,9811,9871,9242,9486,9026,9024,9914,9124,9084,9050,7,27,25,26,30])).
% 71.66/71.79 cnf(10243,plain,
% 71.66/71.79 (~P4(f7(a2,a2),a4,f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9852,9975,9712,9811,10210,9871,9242,9486,9334,9026,9024,9914,9124,9084,9050,7,27,25,26,30,29])).
% 71.66/71.79 cnf(10249,plain,
% 71.66/71.79 (~P4(a2,f7(a1,a1),f3(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10237,9929,10210,9167,9805,9205,27,25])).
% 71.66/71.79 cnf(10251,plain,
% 71.66/71.79 (~P4(a1,f7(a2,a2),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10237,10183,9929,10210,9167,9805,9240,9205,9215,27,25,26])).
% 71.66/71.79 cnf(10253,plain,
% 71.66/71.79 (~P4(f6(a4),f7(a1,a1),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10237,10183,9818,9929,10210,9167,9805,9979,9722,10096,9240,9205,9215,27,25,26,30])).
% 71.66/71.79 cnf(10255,plain,
% 71.66/71.79 (~P2(f5(a2),f7(a2,a2),f3(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9995,10237,10218,10183,9818,9929,10210,9167,9805,9979,9722,10096,9240,9205,9215,9120,9324,27,25,26,30,29])).
% 71.66/71.79 cnf(10259,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f6(a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9969,10227,10210,9971,9389,9702,27,25])).
% 71.66/71.79 cnf(10261,plain,
% 71.66/71.79 (~P4(f5(a4),f7(a4,a4),a4)),
% 71.66/71.79 inference(scs_inference,[],[5,9969,10227,10210,9971,9389,9702,9193,9680,27,25,26])).
% 71.66/71.79 cnf(10263,plain,
% 71.66/71.79 (~P4(f3(a1,a1),f3(a1,a1),f5(a2))),
% 71.66/71.79 inference(scs_inference,[],[5,10255,9969,10227,10210,9971,9458,9389,9225,9702,9193,9680,27,25,26,30])).
% 71.66/71.79 cnf(10265,plain,
% 71.66/71.79 (~P2(f7(a2,a2),a2,f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[5,10255,9969,10227,10148,10210,9971,9458,9389,9225,9702,9193,9215,9680,9060,27,25,26,30,29])).
% 71.66/71.79 cnf(10274,plain,
% 71.66/71.79 (~P2(f5(a2),f7(a4,a4),f3(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[9896,10255,10218,9044,2702,27,28])).
% 71.66/71.79 cnf(10276,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f7(a1,a1),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[10259,9896,10255,10218,9472,9044,2702,27,28,25])).
% 71.66/71.79 cnf(10278,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f7(a2,a2),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10259,10069,9896,10255,10218,9189,9472,9381,9044,2702,27,28,25,26])).
% 71.66/71.79 cnf(10285,plain,
% 71.66/71.79 (~P2(f5(a1),a4,a4)),
% 71.66/71.79 inference(scs_inference,[],[9393,3665,1571,27])).
% 71.66/71.79 cnf(10287,plain,
% 71.66/71.79 (~P4(f6(a4),f5(a1),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10276,9393,9857,9971,3665,1571,27,25])).
% 71.66/71.79 cnf(10289,plain,
% 71.66/71.79 (~P4(f3(a1,a1),f7(a1,a1),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[10135,10276,9393,9857,9971,9694,9434,3665,1571,27,25,26])).
% 71.66/71.79 cnf(10293,plain,
% 71.66/71.79 (~P2(f5(a1),f7(a1,a1),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[10278,9888,10135,10276,9393,10104,9857,9971,9694,9026,9914,9434,9124,3665,1571,27,25,26,30,29])).
% 71.66/71.79 cnf(10300,plain,
% 71.66/71.79 (~P4(f5(a4),a2,f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10203,10126,9191,9401,9042,9050,27,25])).
% 71.66/71.79 cnf(10302,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f7(a1,a1),f5(a2))),
% 71.66/71.79 inference(scs_inference,[],[10203,10156,10126,9191,9462,9694,9401,9042,9050,27,25,26])).
% 71.66/71.79 cnf(10306,plain,
% 71.66/71.79 (~P2(f7(a2,a2),a4,f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10203,10156,10251,10126,9509,9573,9191,9486,9504,9342,9462,9694,9215,9401,9042,9034,9050,27,25,26,30,29])).
% 71.66/71.79 cnf(10313,plain,
% 71.66/71.79 (P2(a1,f6(a4),a1)),
% 71.66/71.79 inference(scs_inference,[],[9657,9708,9044,9914,9324,27,28])).
% 71.66/71.79 cnf(10315,plain,
% 71.66/71.79 (~P4(f5(a2),f7(a1,a1),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10302,9657,9708,9606,9604,9044,9914,9324,27,28,25])).
% 71.66/71.79 cnf(10319,plain,
% 71.66/71.79 (~P2(f7(a4,a4),f7(a4,a4),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10193,10302,9657,10148,9848,10122,9708,9606,9979,9604,9163,9044,9914,9324,9098,27,28,25,26,29])).
% 71.66/71.79 cnf(10321,plain,
% 71.66/71.79 (P2(f6(a4),a1,a1)),
% 71.66/71.79 inference(scs_inference,[],[10193,10302,9657,10148,9848,10122,9708,9606,9979,9604,9163,9044,9914,9324,9098,27,28,25,26,29,23])).
% 71.66/71.79 cnf(10326,plain,
% 71.66/71.79 (~P2(a1,f6(a4),a4)),
% 71.66/71.79 inference(scs_inference,[],[10313,10321,9362,27])).
% 71.66/71.79 cnf(10328,plain,
% 71.66/71.79 (~P4(f6(a4),a1,f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10313,10321,9362,10276,9290,9971,27,25])).
% 71.66/71.79 cnf(10332,plain,
% 71.66/71.79 (~P4(f7(a2,a2),f7(a1,a1),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[5,10319,10313,10321,9362,10276,9290,9890,9971,9704,9472,9078,9124,27,25,26,30])).
% 71.66/71.79 cnf(10347,plain,
% 71.66/71.79 (~P2(f7(a4,a4),f6(a4),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10025,9942,10287,10261,10063,10313,10051,9848,9732,9991,9857,9032,9702,9424,9914,9238,25,26,27,30,29])).
% 71.66/71.79 cnf(10354,plain,
% 71.66/71.79 (~P4(f6(a4),f3(a1,a1),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10253,10276,9946,9358,9971,25,26])).
% 71.66/71.79 cnf(10356,plain,
% 71.66/71.79 (~P2(f3(a4,a4),x103561,a4)),
% 71.66/71.79 inference(scs_inference,[],[31,10253,10276,9379,9946,9358,9971,25,26,27])).
% 71.66/71.79 cnf(10365,plain,
% 71.66/71.79 (~P4(f5(a4),a1,f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10249,9846,9118,9684,9702,9332,25,26])).
% 71.66/71.79 cnf(10369,plain,
% 71.66/71.79 (P2(f6(a2),f6(a4),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[10249,9846,9742,10321,9590,10313,9690,9118,9684,9702,9332,25,26,27,28])).
% 71.66/71.79 cnf(10374,plain,
% 71.66/71.79 (~P2(f7(a2,a2),f6(a2),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10249,10356,9846,9742,10321,9865,10023,9590,9217,10313,9690,9118,9684,9702,9215,9914,9094,9332,25,26,27,28,30,29])).
% 71.66/71.79 cnf(10376,plain,
% 71.66/71.79 (P2(f6(a4),f6(a2),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[10249,10356,9846,9742,10321,9865,10023,9590,9217,10313,9690,9118,9684,9702,9215,9914,9094,9332,25,26,27,28,30,29,23])).
% 71.66/71.79 cnf(10378,plain,
% 71.66/71.79 (~P4(f5(a4),a4,f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10191,9096,9401,25])).
% 71.66/71.79 cnf(10380,plain,
% 71.66/71.79 (~P4(a1,f6(a2),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10239,10191,9267,9096,9401,9238,25,26])).
% 71.66/71.79 cnf(10382,plain,
% 71.66/71.79 (~P2(f3(a2,a2),f3(a2,a2),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[10152,10239,10376,10191,9543,9267,9096,9401,9238,25,26,27])).
% 71.66/71.79 cnf(10384,plain,
% 71.66/71.79 (P2(f6(a4),f6(a2),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10152,10239,10376,10191,9543,9229,9265,9267,9096,9401,9238,25,26,27,28])).
% 71.66/71.79 cnf(10390,plain,
% 71.66/71.79 (P2(f6(a2),f6(a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10152,10187,10239,10376,9916,10191,9543,9944,9229,9265,10313,10096,9240,9267,9189,9694,9096,9401,9238,25,26,27,28,30,29,23])).
% 71.66/71.79 cnf(10399,plain,
% 71.66/71.79 (~P4(a1,f6(a4),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10276,9263,9205,25])).
% 71.66/71.79 cnf(10401,plain,
% 71.66/71.79 (~P4(f5(a1),f5(a2),f7(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10315,10276,9515,9604,9263,9205,25,26])).
% 71.66/71.79 cnf(10405,plain,
% 71.66/71.79 (P2(f7(a4,a4),f6(a2),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[31,10315,10369,10276,9242,9515,9092,9604,9263,9205,9042,25,26,27,28])).
% 71.66/71.79 cnf(10407,plain,
% 71.66/71.79 (~P4(f7(a4,a4),a1,a4)),
% 71.66/71.79 inference(scs_inference,[],[31,10315,10369,10276,9625,9242,9515,9092,9604,9263,9205,9267,9042,9034,25,26,27,28,30])).
% 71.66/71.79 cnf(10411,plain,
% 71.66/71.79 (P2(f6(a2),f7(a4,a4),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[31,10263,10315,10369,9494,10276,9625,9242,9515,9092,9604,9263,9205,9267,9042,9034,9134,25,26,27,28,30,29,23])).
% 71.66/71.79 cnf(10413,plain,
% 71.66/71.79 (~P4(f7(a2,a2),f7(a4,a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10057,9684,9694,25])).
% 71.66/71.79 cnf(10419,plain,
% 71.66/71.79 (P2(a2,f6(a4),a2)),
% 71.66/71.79 inference(scs_inference,[],[10057,10384,10407,10405,9720,9690,9360,9462,9193,9684,9694,25,26,27,28])).
% 71.66/71.79 cnf(10421,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f3(a4,a4),a4)),
% 71.66/71.79 inference(scs_inference,[],[10057,10384,10407,10405,9496,10065,10356,9720,9690,9360,10096,9462,9193,9684,9694,25,26,27,28,30])).
% 71.66/71.79 cnf(10426,plain,
% 71.66/71.79 (P2(f6(a4),a2,a2)),
% 71.66/71.79 inference(scs_inference,[],[10057,10212,10384,10407,10405,9496,10065,10356,9720,10321,9848,9690,9360,10096,9462,9193,9684,9694,25,26,27,28,30,29,23])).
% 71.66/71.79 cnf(10438,plain,
% 71.66/71.79 (P2(f6(a4),a2,f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10390,10223,10328,10421,10419,10426,9496,9535,9659,9290,9265,9956,25,26,27,28])).
% 71.66/71.79 cnf(10442,plain,
% 71.66/71.79 (~P2(f6(a2),f7(a4,a4),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10411,10390,10223,10328,10382,10421,10380,10419,10426,9496,9535,9502,9659,9290,9265,9956,9238,9098,9134,25,26,27,28,30,29])).
% 71.66/71.79 cnf(10444,plain,
% 71.66/71.79 (P2(a2,f6(a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10411,10390,10223,10328,10382,10421,10380,10419,10426,9496,9535,9502,9659,9290,9265,9956,9238,9098,9134,25,26,27,28,30,29,23])).
% 71.66/71.79 cnf(10456,plain,
% 71.66/71.79 (P2(f6(a2),a2,f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[31,10354,10438,10411,10369,10302,9848,9606,9946,9511,9042,25,26,27,28])).
% 71.66/71.79 cnf(10458,plain,
% 71.66/71.79 (~P4(f7(a2,a2),f5(a4),a4)),
% 71.66/71.79 inference(scs_inference,[],[31,10354,9759,10438,10411,10369,10302,9861,9848,9606,9946,9511,9694,9042,2138,25,26,27,28,30])).
% 71.66/71.79 cnf(10462,plain,
% 71.66/71.79 (~P2(f5(a2),a4,f3(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[31,10354,9882,9759,10438,10411,10369,10302,10426,9861,9848,9606,9946,9511,9694,9042,2138,25,26,27,28,30,29,2686])).
% 71.66/71.79 cnf(10464,plain,
% 71.66/71.79 (P2(a2,f6(a2),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[31,10354,9882,9759,10438,10411,10369,10302,10426,9861,9848,9606,9946,9511,9694,9042,2138,25,26,27,28,30,29,2686,23])).
% 71.66/71.79 cnf(10466,plain,
% 71.66/71.79 (~P2(f7(a4,a4),f6(a2),a4)),
% 71.66/71.79 inference(scs_inference,[],[31,10354,9882,9759,10438,10411,10369,10302,10426,9861,9848,9606,9946,9511,9694,9042,2138,25,26,27,28,30,29,2686,23,9686])).
% 71.66/71.79 cnf(10475,plain,
% 71.66/71.79 (P2(f5(a2),f6(a4),f5(a2))),
% 71.66/71.79 inference(scs_inference,[],[10085,9448,10456,9348,10419,9080,9381,9026,9205,2702,25,26,27,28])).
% 71.66/71.79 cnf(10481,plain,
% 71.66/71.79 (P2(f6(a4),f5(a2),f5(a2))),
% 71.66/71.79 inference(scs_inference,[],[10085,10235,9448,10444,10456,9795,9348,10419,9708,9346,9358,9080,9381,9026,9704,9205,2702,25,26,27,28,30,29,23])).
% 71.66/71.79 cnf(10483,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f7(a4,a4),a4)),
% 71.66/71.79 inference(scs_inference,[],[10378,9462,9702,25])).
% 71.66/71.79 cnf(10489,plain,
% 71.66/71.79 (P2(f6(a2),f6(a4),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[10241,10185,10378,10464,10390,9871,9462,9267,9702,9238,25,26,27,28])).
% 71.66/71.79 cnf(10496,plain,
% 71.66/71.79 (P2(f6(a4),f6(a2),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[10332,10241,10185,10378,10464,10390,10065,10356,9478,10104,9871,9956,9991,9462,9267,9702,9238,25,26,27,28,30,29,23])).
% 71.66/71.79 cnf(10499,plain,
% 71.66/71.79 (~P4(f3(a1,a1),f3(a1,a1),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[10259,9424,25])).
% 71.66/71.79 cnf(10501,plain,
% 71.66/71.79 (~P4(a1,f7(a4,a4),a1)),
% 71.66/71.79 inference(scs_inference,[],[10259,9682,9163,9472,9424,25,26])).
% 71.66/71.79 cnf(10505,plain,
% 71.66/71.79 (P2(f6(a2),f6(a2),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[31,10489,10259,9682,10411,9855,9944,9156,9163,9472,9424,25,26,27,28])).
% 71.66/71.79 cnf(10528,plain,
% 71.66/71.79 (~P4(a1,f5(a2),a1)),
% 71.66/71.79 inference(scs_inference,[],[33,9084,9332,25])).
% 71.66/71.79 cnf(10530,plain,
% 71.66/71.79 (~P4(a4,f7(a4,a4),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[33,10458,9684,9124,9084,9332,25,26])).
% 71.66/71.79 cnf(10534,plain,
% 71.66/71.79 (P2(f7(a4,a4),f5(a2),f5(a2))),
% 71.66/71.79 inference(scs_inference,[],[33,10481,10496,10293,10458,10444,9736,9684,9124,9084,9332,3656,25,26,27,28])).
% 71.66/71.79 cnf(10536,plain,
% 71.66/71.79 (~P4(f6(a4),f6(a4),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[33,10413,10481,10496,10293,10458,10444,10384,9736,9684,9124,9084,9332,3656,25,26,27,28,29])).
% 71.66/71.79 cnf(10541,plain,
% 71.66/71.79 (P2(f5(a2),f7(a4,a4),f5(a2))),
% 71.66/71.79 inference(scs_inference,[],[33,10413,10481,10496,10293,10458,10444,10384,9519,9269,10356,9736,9684,9124,9084,9332,3665,3656,25,26,27,28,29,30,23])).
% 71.66/71.79 cnf(10543,plain,
% 71.66/71.79 (~P4(f5(a1),f5(a1),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[10536,9857,25])).
% 71.66/71.79 cnf(10545,plain,
% 71.66/71.79 (~P4(f3(a1,a1),a1,f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[10289,10536,9857,9102,9381,25,26])).
% 71.66/71.79 cnf(10556,plain,
% 71.66/71.79 (~P4(f5(a2),a1,a1)),
% 71.66/71.79 inference(scs_inference,[],[33,9024,9332,25])).
% 71.66/71.79 cnf(10562,plain,
% 71.66/71.79 (P2(f5(a1),f6(a4),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[33,10049,10545,10405,10456,10419,9024,9046,9332,3652,25,26,27,28])).
% 71.66/71.79 cnf(10568,plain,
% 71.66/71.79 (P2(f6(a4),f5(a1),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[33,10115,10401,10049,10545,10475,10405,10456,10419,9515,9024,9046,9134,9332,3652,25,26,27,28,29,30,23])).
% 71.66/71.79 cnf(10573,plain,
% 71.66/71.79 (~P4(f7(a2,a2),f5(a4),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[10556,10243,9604,9240,9078,9120,25,26])).
% 71.66/71.79 cnf(10577,plain,
% 71.66/71.79 (P2(f7(a4,a4),f5(a1),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10556,10073,10243,10562,10568,10444,9604,9240,9078,9120,3650,25,26,27,28])).
% 71.66/71.79 cnf(10579,plain,
% 71.66/71.79 (~P2(f5(a1),f6(a4),f5(a2))),
% 71.66/71.79 inference(scs_inference,[],[10556,10528,10073,10243,10562,10568,10444,9604,9240,9032,10313,9078,9120,3650,25,26,27,28,29])).
% 71.66/71.79 cnf(10583,plain,
% 71.66/71.79 (P2(f5(a1),f7(a4,a4),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10556,10528,10073,10120,10243,10562,10568,10444,9604,9240,9032,10313,9163,9078,9120,9914,3650,25,26,27,28,29,30,23])).
% 71.66/71.79 cnf(10591,plain,
% 71.66/71.79 (P2(f5(a1),f6(a2),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[10499,10583,10347,10577,10543,10562,10384,9290,9956,9032,3646,25,26,27,28])).
% 71.66/71.79 cnf(10597,plain,
% 71.66/71.79 (P2(f6(a2),f5(a1),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[9633,10499,10483,10583,10347,10577,10543,10562,10438,10384,9290,9562,9219,9956,9032,9034,9042,3646,25,26,27,28,29,30,23])).
% 71.66/71.79 cnf(10606,plain,
% 71.66/71.79 (~P4(f5(a2),a2,f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[33,10199,9684,9120,9084,25,26])).
% 71.66/71.79 cnf(10608,plain,
% 71.66/71.79 (P2(f5(a1),f7(a2,a2),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[33,10591,10199,10505,9684,9120,9084,25,26,27])).
% 71.66/71.79 cnf(10612,plain,
% 71.66/71.79 (P2(f7(a2,a2),f5(a1),f5(a1))),
% 71.66/71.79 inference(scs_inference,[],[33,10300,10591,10199,10505,10438,10426,9848,9684,9120,9084,25,26,27,29,23])).
% 71.66/71.79 cnf(10619,plain,
% 71.66/71.79 (~P4(a2,f3(a1,a1),a1)),
% 71.66/71.79 inference(scs_inference,[],[33,10530,9215,9046,9401,9084,25,26])).
% 71.66/71.79 cnf(10621,plain,
% 71.66/71.79 (~P2(f5(a1),f7(a2,a2),f6(a2))),
% 71.66/71.79 inference(scs_inference,[],[33,10530,10374,10608,10612,9215,9046,9401,9084,25,26,27])).
% 71.66/71.79 cnf(10623,plain,
% 71.66/71.79 (P2(a2,f6(a2),f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[33,10530,10374,10608,10612,10496,10464,10426,9215,9046,9401,9084,25,26,27,28])).
% 71.66/71.79 cnf(10627,plain,
% 71.66/71.79 (~P4(f7(a4,a4),f5(a2),a4)),
% 71.66/71.79 inference(scs_inference,[],[33,10326,10530,10201,10374,10608,10612,10475,10562,10496,10464,10444,10426,9515,9215,9046,9401,9084,9332,25,26,27,28,29,30])).
% 71.66/71.79 cnf(10629,plain,
% 71.66/71.79 (P2(f6(a2),a2,f7(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[33,10326,10530,10201,10374,10608,10612,10475,10562,10496,10464,10444,10426,9515,9215,9046,9401,9084,9332,25,26,27,28,29,30,23])).
% 71.66/71.79 cnf(10643,plain,
% 71.66/71.79 (~P4(f7(a1,a1),f5(a2),f3(a1,a1))),
% 71.66/71.79 inference(scs_inference,[],[10462,10399,10442,10579,10629,10606,10612,10499,10541,10390,9979,9722,9562,9606,9263,9956,10313,9120,2983,25,26,27,28,29,30])).
% 71.66/71.79 cnf(10671,plain,
% 71.66/71.79 (P4(f5(a1),f3(a2,a2),f3(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[9158,9026,25])).
% 71.66/71.79 cnf(10681,plain,
% 71.66/71.79 (P4(f3(a2,a2),f5(a1),f3(a2,a2))),
% 71.66/71.79 inference(scs_inference,[],[10285,10621,9071,10328,10591,10608,10583,10541,9158,9979,9219,9515,9026,9042,9324,1375,25,26,27,29,30,22])).
% 71.66/71.79 cnf(10689,plain,
% 71.66/71.79 (~P2(f6(a4),a2,f3(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9556,10681,10287,9304,10597,9863,10591,10426,9504,9857,9971,9134,26,25,27,29])).
% 71.66/71.79 cnf(10708,plain,
% 71.66/71.79 (P2(f5(a2),f7(a2,a2),f5(a2))),
% 71.66/71.79 inference(scs_inference,[],[10225,10100,10274,10365,10689,10671,10534,10681,10075,10629,10583,10541,9890,9611,9511,9504,9219,9026,3652,25,26,27,28,29,30,23])).
% 71.66/71.79 cnf(10714,plain,
% 71.66/71.79 (~P2(f7(a2,a2),f6(a4),a2)),
% 71.66/71.79 inference(scs_inference,[],[35,9500,10643,10671,10623,10369,9080,9205,3646,26,25,27])).
% 71.66/71.79 cnf(10727,plain,
% 71.66/71.79 (P2(a4,f7(a4,a4),a4)),
% 71.66/71.79 inference(scs_inference,[],[10306,10407,9444,10612,10608,10010,10411,9126,9193,9163,9134,26,25,27,28])).
% 71.66/71.79 cnf(10733,plain,
% 71.66/71.79 (P2(f7(a4,a4),a4,a4)),
% 71.66/71.79 inference(scs_inference,[],[35,10306,10708,9250,10407,9444,10612,10623,10608,10010,10411,9515,9126,9193,9163,9914,9050,9134,26,25,27,28,29,30,23])).
% 71.66/71.79 cnf(10744,plain,
% 71.66/71.79 (P2(f7(a2,a2),f6(a4),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[10466,10573,10619,10727,10733,10489,10623,10218,9240,9684,9084,9332,9686,26,25,27,28])).
% 71.66/71.79 cnf(10750,plain,
% 71.66/71.79 (P2(f6(a4),f7(a2,a2),f7(a4,a4))),
% 71.66/71.79 inference(scs_inference,[],[9894,10466,10573,10619,10727,10733,10405,10489,10623,10218,9144,9736,9240,9472,9684,9084,9332,9686,26,25,27,28,29,30,23])).
% 71.66/71.79 cnf(10764,plain,
% 71.66/71.79 (P2(f7(a2,a2),f6(a4),a4)),
% 71.66/71.79 inference(scs_inference,[],[10750,10627,10744,10265,10501,10727,10708,10071,9742,9692,10608,9265,9857,9604,9032,9120,26,25,27,28,29,30,23])).
% 71.66/71.79 cnf(10772,plain,
% 71.66/71.79 (P2(f6(a4),f7(a4,a4),f6(a4))),
% 71.66/71.79 inference(scs_inference,[],[10764,9803,9975,10727,9517,10681,9611,9078,9124,9134,26,25,27,28])).
% 71.66/71.79 cnf(10836,plain,
% 71.66/71.79 (P2(a2,f7(a4,a4),a2)),
% 71.66/71.79 inference(scs_inference,[],[10772,10419,28])).
% 71.66/71.79 cnf(10851,plain,
% 71.66/71.79 ($false),
% 71.66/71.79 inference(scs_inference,[],[10714,10836,10744,9476,28]),
% 71.66/71.79 ['proof']).
% 71.66/71.79 % SZS output end Proof
% 71.66/71.79 % Total time :71.060000s
%------------------------------------------------------------------------------