%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD070-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n002.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:36 EDT 2024
% Result : Unsatisfiable 246.16s 246.24s
% Output : CNFRefutation 246.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : FLD070-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n002.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jun 19 11:26:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.55 start to proof:theBenchmark
% 246.16/246.23 %-------------------------------------------
% 246.16/246.23 % File :CSE---1.7
% 246.16/246.23 % Problem :theBenchmark
% 246.16/246.23 % Transform :cnf
% 246.16/246.23 % Format :tptp:raw
% 246.16/246.23 % Command :java -jar mcs_scs.jar %d %s
% 246.16/246.23
% 246.16/246.23 % Result :Theorem 245.530000s
% 246.16/246.23 % Output :CNFRefutation 245.530000s
% 246.16/246.23 %-------------------------------------------
% 246.16/246.24 %--------------------------------------------------------------------------
% 246.16/246.24 % File : FLD070-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 246.16/246.24 % Domain : Field Theory (Ordered fields)
% 246.16/246.24 % Problem : One-sided addition of two order relations
% 246.16/246.24 % Version : [Dra93] axioms : Especial.
% 246.16/246.24 % Theorem formulation : Functional with glxx axiom set.
% 246.16/246.24 % English :
% 246.16/246.24
% 246.16/246.24 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 246.16/246.24 % Source : [Dra93]
% 246.16/246.24 % Names :
% 246.16/246.24
% 246.16/246.24 % Status : Unsatisfiable
% 246.16/246.24 % Rating : 0.00 v7.4.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.25 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.20 v5.2.0, 0.00 v5.0.0, 0.29 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0, 0.20 v2.3.0, 0.33 v2.2.1, 0.67 v2.1.0
% 246.16/246.24 % Syntax : Number of clauses : 32 ( 8 unt; 3 nHn; 32 RR)
% 246.16/246.24 % Number of literals : 78 ( 0 equ; 45 neg)
% 246.16/246.24 % Maximal clause size : 4 ( 2 avg)
% 246.16/246.24 % Maximal term depth : 3 ( 1 avg)
% 246.16/246.24 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 246.16/246.24 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 246.16/246.24 % Number of variables : 50 ( 0 sgn)
% 246.16/246.24 % SPC : CNF_UNS_RFO_NEQ_NHN
% 246.16/246.24
% 246.16/246.24 % Comments :
% 246.16/246.24 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 246.16/246.24 %--------------------------------------------------------------------------
% 246.16/246.24 include('Axioms/FLD001-0.ax').
% 246.16/246.24 %--------------------------------------------------------------------------
% 246.16/246.24 cnf(a_is_defined,hypothesis,
% 246.16/246.24 defined(a) ).
% 246.16/246.24
% 246.16/246.24 cnf(b_is_defined,hypothesis,
% 246.16/246.24 defined(b) ).
% 246.16/246.24
% 246.16/246.24 cnf(less_or_equal_3,negated_conjecture,
% 246.16/246.24 less_or_equal(additive_identity,a) ).
% 246.16/246.24
% 246.16/246.24 cnf(less_or_equal_4,negated_conjecture,
% 246.16/246.24 less_or_equal(additive_identity,b) ).
% 246.16/246.24
% 246.16/246.24 cnf(not_less_or_equal_5,negated_conjecture,
% 246.16/246.24 ~ less_or_equal(additive_identity,add(a,b)) ).
% 246.16/246.24
% 246.16/246.24 %--------------------------------------------------------------------------
% 246.16/246.24 %-------------------------------------------
% 246.16/246.24 % Proof found
% 246.16/246.24 % SZS status Theorem for theBenchmark
% 246.16/246.24 % SZS output start Proof
% 246.16/246.25 %ClaNum:32(EqnAxiom:0)
% 246.16/246.25 %VarNum:128(SingletonVarNum:50)
% 246.16/246.25 %MaxLitNum:4
% 246.16/246.25 %MaxfuncDepth:2
% 246.16/246.25 %SharedTerms:13
% 246.16/246.25 %goalClause: 5 6 8
% 246.16/246.25 %singleGoalClaCount:3
% 246.16/246.25 [1]P1(a1)
% 246.16/246.25 [2]P1(a4)
% 246.16/246.25 [3]P1(a2)
% 246.16/246.25 [4]P1(a5)
% 246.16/246.25 [5]P2(a1,a2)
% 246.16/246.25 [6]P2(a1,a5)
% 246.16/246.25 [7]~P3(a1,a4)
% 246.16/246.25 [8]~P2(a1,f3(a2,a5))
% 246.16/246.25 [10]~P1(x101)+P3(x101,x101)
% 246.16/246.25 [9]~P1(x91)+P1(f6(x91))
% 246.16/246.25 [14]~P1(x141)+P3(f3(a1,x141),x141)
% 246.16/246.25 [15]~P1(x151)+P3(f8(a4,x151),x151)
% 246.16/246.25 [18]~P1(x181)+P3(f3(x181,f6(x181)),a1)
% 246.16/246.25 [12]~P3(x122,x121)+P3(x121,x122)
% 246.16/246.25 [11]~P1(x111)+P3(x111,a1)+P1(f7(x111))
% 246.16/246.25 [23]~P1(x231)+P3(x231,a1)+P3(f8(x231,f7(x231)),a4)
% 246.16/246.25 [20]~P2(x202,x201)+~P2(x201,x202)+P3(x201,x202)
% 246.16/246.25 [16]~P1(x162)+~P1(x161)+P1(f3(x161,x162))
% 246.16/246.25 [17]~P1(x172)+~P1(x171)+P1(f8(x171,x172))
% 246.16/246.25 [24]~P2(a1,x242)+~P2(a1,x241)+P2(a1,f8(x241,x242))
% 246.16/246.25 [25]~P1(x252)+~P1(x251)+P3(f3(x251,x252),f3(x252,x251))
% 246.16/246.25 [26]~P1(x262)+~P1(x261)+P3(f8(x261,x262),f8(x262,x261))
% 246.16/246.25 [19]~P3(x191,x193)+P3(x191,x192)+~P3(x193,x192)
% 246.16/246.25 [21]~P2(x213,x212)+P2(x211,x212)+~P3(x213,x211)
% 246.16/246.25 [22]~P2(x221,x223)+P2(x221,x222)+~P2(x223,x222)
% 246.16/246.25 [27]~P1(x272)+~P3(x271,x273)+P3(f3(x271,x272),f3(x273,x272))
% 246.16/246.25 [28]~P1(x282)+~P3(x281,x283)+P3(f8(x281,x282),f8(x283,x282))
% 246.16/246.25 [29]~P1(x292)+~P2(x291,x293)+P2(f3(x291,x292),f3(x293,x292))
% 246.16/246.25 [13]P2(x132,x131)+~P1(x131)+~P1(x132)+P2(x131,x132)
% 246.16/246.25 [30]~P1(x303)+~P1(x302)+~P1(x301)+P3(f3(x301,f3(x302,x303)),f3(f3(x301,x302),x303))
% 246.16/246.25 [31]~P1(x313)+~P1(x312)+~P1(x311)+P3(f8(x311,f8(x312,x313)),f8(f8(x311,x312),x313))
% 246.16/246.25 [32]~P1(x323)+~P1(x322)+~P1(x321)+P3(f3(f8(x321,x322),f8(x323,x322)),f8(f3(x321,x323),x322))
% 246.16/246.25 %EqnAxiom
% 246.16/246.25
% 246.16/246.25 %-------------------------------------------
% 246.16/246.27 cnf(33,plain,
% 246.16/246.27 (~P3(a4,a1)),
% 246.16/246.27 inference(scs_inference,[],[7,12])).
% 246.16/246.27 cnf(35,plain,
% 246.16/246.27 (P2(a1,a1)),
% 246.16/246.27 inference(scs_inference,[],[1,7,12,13])).
% 246.16/246.27 cnf(41,plain,
% 246.16/246.27 (~P2(a2,a1)+~P3(x411,a1)+P3(x411,a2)),
% 246.16/246.27 inference(scs_inference,[],[5,1,7,12,13,20,21,19])).
% 246.16/246.27 cnf(44,plain,
% 246.16/246.27 (P2(a4,a4)),
% 246.16/246.27 inference(scs_inference,[],[2,35,20,13])).
% 246.16/246.27 cnf(46,plain,
% 246.16/246.27 (P3(a4,a4)),
% 246.16/246.27 inference(scs_inference,[],[44,20])).
% 246.16/246.27 cnf(48,plain,
% 246.16/246.27 (P2(a2,a2)),
% 246.16/246.27 inference(scs_inference,[],[44,3,20,13])).
% 246.16/246.27 cnf(50,plain,
% 246.16/246.27 (P3(a2,a2)),
% 246.16/246.27 inference(scs_inference,[],[48,20])).
% 246.16/246.27 cnf(52,plain,
% 246.16/246.27 (P2(a5,a5)),
% 246.16/246.27 inference(scs_inference,[],[48,4,20,13])).
% 246.16/246.27 cnf(56,plain,
% 246.16/246.27 (P3(a1,a5)+~P2(a5,a1)),
% 246.16/246.27 inference(scs_inference,[],[6,20])).
% 246.16/246.27 cnf(58,plain,
% 246.16/246.27 (~P2(a5,a1)+P2(a5,a2)),
% 246.16/246.27 inference(scs_inference,[],[5,6,20,21])).
% 246.16/246.27 cnf(61,plain,
% 246.16/246.27 (P1(f6(f7(a4)))),
% 246.16/246.27 inference(scs_inference,[],[33,2,9,11])).
% 246.16/246.27 cnf(74,plain,
% 246.16/246.27 (P3(f3(a1,f6(a2)),f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[3,14,9])).
% 246.16/246.27 cnf(80,plain,
% 246.16/246.27 (P3(f8(a4,f6(a2)),f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[3,15,9])).
% 246.16/246.27 cnf(81,plain,
% 246.16/246.27 (~P3(x811,f8(a4,f6(a2)))+P3(x811,f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[80,19])).
% 246.16/246.27 cnf(86,plain,
% 246.16/246.27 (~P2(f3(a1,f6(a2)),x861)+P2(f6(a2),x861)),
% 246.16/246.27 inference(scs_inference,[],[74,21])).
% 246.16/246.27 cnf(88,plain,
% 246.16/246.27 (~P1(f6(a2))+P2(f6(a2),f3(a2,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[5,74,21,29])).
% 246.16/246.27 cnf(91,plain,
% 246.16/246.27 (~P2(f8(a4,f6(a2)),x911)+P2(f6(a2),x911)),
% 246.16/246.27 inference(scs_inference,[],[80,21])).
% 246.16/246.27 cnf(93,plain,
% 246.16/246.27 (P3(f3(f6(a5),f6(f6(a5))),a1)),
% 246.16/246.27 inference(scs_inference,[],[4,18,9])).
% 246.16/246.27 cnf(94,plain,
% 246.16/246.27 (~P3(a4,f3(f6(a5),f6(f6(a5))))),
% 246.16/246.27 inference(scs_inference,[],[33,93,19])).
% 246.16/246.27 cnf(98,plain,
% 246.16/246.27 (~P3(f3(f6(a5),f6(f6(a5))),a4)),
% 246.16/246.27 inference(scs_inference,[],[8,33,93,19,21,12])).
% 246.16/246.27 cnf(108,plain,
% 246.16/246.27 (~P1(f6(a2))+P3(f8(f6(a2),a4),f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[2,81,26])).
% 246.16/246.27 cnf(115,plain,
% 246.16/246.27 (P3(f6(a2),f8(f6(a2),a4))+~P1(f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[108,12])).
% 246.16/246.27 cnf(119,plain,
% 246.16/246.27 (P3(f8(a4,f6(a2)),f8(f6(a2),a4))+~P1(f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[80,115,19])).
% 246.16/246.27 cnf(120,plain,
% 246.16/246.27 (P3(f8(f6(a2),a4),f8(a4,f6(a2)))+~P1(f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[119,12])).
% 246.16/246.27 cnf(124,plain,
% 246.16/246.27 (P1(f3(f6(a1),f6(a1)))),
% 246.16/246.27 inference(scs_inference,[],[1,16,9])).
% 246.16/246.27 cnf(129,plain,
% 246.16/246.27 (P1(f8(f6(a1),f6(a1)))),
% 246.16/246.27 inference(scs_inference,[],[1,17,9])).
% 246.16/246.27 cnf(130,plain,
% 246.16/246.27 (P2(f8(f6(a1),f6(a1)),f8(f6(a1),f6(a1)))),
% 246.16/246.27 inference(scs_inference,[],[129,13])).
% 246.16/246.27 cnf(145,plain,
% 246.16/246.27 (P2(a1,f8(a2,a2))),
% 246.16/246.27 inference(scs_inference,[],[5,35,24,22])).
% 246.16/246.27 cnf(165,plain,
% 246.16/246.27 (P3(f3(f6(a2),f6(f6(a2))),a1)),
% 246.16/246.27 inference(scs_inference,[],[3,9,18])).
% 246.16/246.27 cnf(166,plain,
% 246.16/246.27 (~P3(a4,f3(f6(a2),f6(f6(a2))))),
% 246.16/246.27 inference(scs_inference,[],[33,165,19])).
% 246.16/246.27 cnf(172,plain,
% 246.16/246.27 (P1(f6(f3(a5,a5)))),
% 246.16/246.27 inference(scs_inference,[],[4,9,16])).
% 246.16/246.27 cnf(187,plain,
% 246.16/246.27 (P3(f3(a1,f6(a1)),f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[1,9,14])).
% 246.16/246.27 cnf(188,plain,
% 246.16/246.27 (~P3(x1881,f3(a1,f6(a1)))+P3(x1881,f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[187,19])).
% 246.16/246.27 cnf(193,plain,
% 246.16/246.27 (~P1(f3(a1,f6(a1)))+P3(f8(a4,f3(a1,f6(a1))),f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[188,15])).
% 246.16/246.27 cnf(194,plain,
% 246.16/246.27 (~P2(f3(a1,f6(a1)),x1941)+P2(f6(a1),x1941)),
% 246.16/246.27 inference(scs_inference,[],[187,21])).
% 246.16/246.27 cnf(199,plain,
% 246.16/246.27 (~P1(f6(a1))+P3(f8(a4,f3(a1,f6(a1))),f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[1,193,16])).
% 246.16/246.27 cnf(200,plain,
% 246.16/246.27 (P3(f6(a1),f8(a4,f3(a1,f6(a1))))+~P1(f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[199,12])).
% 246.16/246.27 cnf(209,plain,
% 246.16/246.27 (P1(f6(f8(a5,a5)))),
% 246.16/246.27 inference(scs_inference,[],[4,9,17])).
% 246.16/246.27 cnf(214,plain,
% 246.16/246.27 (P3(f8(a4,f6(a1)),f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[1,9,15])).
% 246.16/246.27 cnf(215,plain,
% 246.16/246.27 (~P3(x2151,f8(a4,f6(a1)))+P3(x2151,f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[214,19])).
% 246.16/246.27 cnf(220,plain,
% 246.16/246.27 (~P1(f8(a4,f6(a1)))+P3(f3(a1,f8(a4,f6(a1))),f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[215,14])).
% 246.16/246.27 cnf(221,plain,
% 246.16/246.27 (~P2(f8(a4,f6(a1)),x2211)+P2(f6(a1),x2211)),
% 246.16/246.27 inference(scs_inference,[],[214,21])).
% 246.16/246.27 cnf(228,plain,
% 246.16/246.27 (~P1(f6(a1))+P3(f3(a1,f8(a4,f6(a1))),f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[2,220,17])).
% 246.16/246.27 cnf(229,plain,
% 246.16/246.27 (P3(f6(a1),f3(a1,f8(a4,f6(a1))))+~P1(f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[228,12])).
% 246.16/246.27 cnf(237,plain,
% 246.16/246.27 (P2(f6(a2),f3(a2,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[3,9,88])).
% 246.16/246.27 cnf(263,plain,
% 246.16/246.27 (P3(f3(f6(a1),f6(f6(a1))),a1)),
% 246.16/246.27 inference(scs_inference,[],[1,9,18])).
% 246.16/246.27 cnf(264,plain,
% 246.16/246.27 (~P3(a4,f3(f6(a1),f6(f6(a1))))),
% 246.16/246.27 inference(scs_inference,[],[33,263,19])).
% 246.16/246.27 cnf(270,plain,
% 246.16/246.27 (P1(f6(f8(a4,a4)))),
% 246.16/246.27 inference(scs_inference,[],[2,9,17])).
% 246.16/246.27 cnf(275,plain,
% 246.16/246.27 (P3(f8(f6(a2),a4),f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[3,9,108])).
% 246.16/246.27 cnf(276,plain,
% 246.16/246.27 (~P3(x2761,f8(f6(a2),a4))+P3(x2761,f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[275,19])).
% 246.16/246.27 cnf(281,plain,
% 246.16/246.27 (P3(f8(f3(a1,f6(a2)),a4),f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[74,2,276,28])).
% 246.16/246.27 cnf(282,plain,
% 246.16/246.27 (~P3(x2821,f8(f3(a1,f6(a2)),a4))+P3(x2821,f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[281,19])).
% 246.16/246.27 cnf(293,plain,
% 246.16/246.27 (~P3(x2931,f3(a1,f6(a2)))+P3(f8(x2931,a4),f6(a2))),
% 246.16/246.27 inference(scs_inference,[],[2,282,28])).
% 246.16/246.27 cnf(309,plain,
% 246.16/246.27 (~P1(f3(a2,a5))+P2(f3(a2,a5),a1)),
% 246.16/246.27 inference(scs_inference,[],[8,1,13])).
% 246.16/246.27 cnf(312,plain,
% 246.16/246.27 (~P1(f3(a2,a5))+P2(f3(f3(a2,a5),a2),f3(a1,a2))),
% 246.16/246.27 inference(scs_inference,[],[3,309,29])).
% 246.16/246.27 cnf(313,plain,
% 246.16/246.27 (P2(f3(f3(a2,a5),a2),f3(a1,a2))),
% 246.16/246.27 inference(scs_inference,[],[4,3,312,16])).
% 246.16/246.27 cnf(314,plain,
% 246.16/246.27 (~P2(x3141,f3(f3(a2,a5),a2))+P2(x3141,f3(a1,a2))),
% 246.16/246.27 inference(scs_inference,[],[313,22])).
% 246.16/246.27 cnf(319,plain,
% 246.16/246.27 (~P2(x3191,f3(a2,a5))+P2(f3(x3191,a2),f3(a1,a2))),
% 246.16/246.27 inference(scs_inference,[],[3,314,29])).
% 246.16/246.27 cnf(334,plain,
% 246.16/246.27 (P1(f6(f3(a2,a2)))),
% 246.16/246.27 inference(scs_inference,[],[3,9,16])).
% 246.16/246.27 cnf(335,plain,
% 246.16/246.27 (P2(f6(f3(a2,a2)),f6(f3(a2,a2)))),
% 246.16/246.27 inference(scs_inference,[],[334,13])).
% 246.16/246.27 cnf(337,plain,
% 246.16/246.27 (P3(f6(a2),f8(f6(a2),a4))),
% 246.16/246.27 inference(scs_inference,[],[3,9,115])).
% 246.16/246.27 cnf(338,plain,
% 246.16/246.27 (P3(f3(a1,f6(a2)),f8(f6(a2),a4))),
% 246.16/246.27 inference(scs_inference,[],[74,337,19])).
% 246.16/246.27 cnf(342,plain,
% 246.16/246.27 (P2(f8(f6(a2),a4),f3(a2,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[237,74,335,337,19,20,21])).
% 246.16/246.27 cnf(344,plain,
% 246.16/246.27 (~P2(x3441,f8(f6(a2),a4))+P2(x3441,f3(a2,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[237,74,335,337,19,20,21,22])).
% 246.16/246.27 cnf(355,plain,
% 246.16/246.27 (~P2(f3(a1,f6(a2)),x3551)+P2(f8(f6(a2),a4),x3551)),
% 246.16/246.27 inference(scs_inference,[],[342,338,20,21])).
% 246.16/246.27 cnf(371,plain,
% 246.16/246.27 (P1(f6(f8(a2,a2)))),
% 246.16/246.27 inference(scs_inference,[],[3,9,17])).
% 246.16/246.27 cnf(374,plain,
% 246.16/246.27 (P3(f8(a4,f6(a2)),f8(f6(a2),a4))),
% 246.16/246.27 inference(scs_inference,[],[3,9,119])).
% 246.16/246.27 cnf(383,plain,
% 246.16/246.27 (~P2(f8(a4,f6(a2)),x3831)+P2(f8(f6(a2),a4),x3831)),
% 246.16/246.27 inference(scs_inference,[],[374,21])).
% 246.16/246.27 cnf(403,plain,
% 246.16/246.27 (P3(f8(f6(a2),a4),f8(a4,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[3,9,120])).
% 246.16/246.27 cnf(404,plain,
% 246.16/246.27 (P3(f3(a1,f6(a2)),f8(a4,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[338,403,19])).
% 246.16/246.27 cnf(406,plain,
% 246.16/246.27 (P2(f8(a4,f6(a2)),f3(a2,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[342,338,403,19,21])).
% 246.16/246.27 cnf(414,plain,
% 246.16/246.27 (~P3(x4141,f3(a1,f6(a2)))+P3(x4141,f8(a4,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[404,19])).
% 246.16/246.27 cnf(419,plain,
% 246.16/246.27 (~P2(f3(a1,f6(a2)),x4191)+P2(f8(a4,f6(a2)),x4191)),
% 246.16/246.27 inference(scs_inference,[],[404,21])).
% 246.16/246.27 cnf(426,plain,
% 246.16/246.27 (P3(f8(a4,f6(a2)),x4261)+~P3(x4261,f3(a1,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[414,12])).
% 246.16/246.27 cnf(430,plain,
% 246.16/246.27 (~P3(f8(f6(a2),a4),f3(a1,f6(a2)))+P3(f8(a4,f6(a2)),f3(a1,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[338,426,19])).
% 246.16/246.27 cnf(467,plain,
% 246.16/246.27 (P3(f8(a4,f3(a1,f6(a1))),f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[1,9,199])).
% 246.16/246.27 cnf(474,plain,
% 246.16/246.27 (~P2(f8(a4,f3(a1,f6(a1))),x4741)+P2(f6(a1),x4741)),
% 246.16/246.27 inference(scs_inference,[],[467,21])).
% 246.16/246.27 cnf(496,plain,
% 246.16/246.27 (P3(f6(a1),f8(a4,f3(a1,f6(a1))))),
% 246.16/246.27 inference(scs_inference,[],[1,9,200])).
% 246.16/246.27 cnf(497,plain,
% 246.16/246.27 (~P2(f6(a1),x4971)+P2(f8(a4,f3(a1,f6(a1))),x4971)),
% 246.16/246.27 inference(scs_inference,[],[496,21])).
% 246.16/246.27 cnf(510,plain,
% 246.16/246.27 (P3(f3(a1,f8(a4,f6(a1))),f6(a1))),
% 246.16/246.27 inference(scs_inference,[],[1,9,228])).
% 246.16/246.27 cnf(519,plain,
% 246.16/246.27 (~P2(f3(a1,f8(a4,f6(a1))),x5191)+P2(f6(a1),x5191)),
% 246.16/246.27 inference(scs_inference,[],[510,21])).
% 246.16/246.27 cnf(539,plain,
% 246.16/246.27 (P3(f6(a1),f3(a1,f8(a4,f6(a1))))),
% 246.16/246.27 inference(scs_inference,[],[1,9,229])).
% 246.16/246.27 cnf(540,plain,
% 246.16/246.27 (~P2(f6(a1),x5401)+P2(f3(a1,f8(a4,f6(a1))),x5401)),
% 246.16/246.27 inference(scs_inference,[],[539,21])).
% 246.16/246.27 cnf(548,plain,
% 246.16/246.27 (P1(f3(f6(a2),f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[3,9,16])).
% 246.16/246.27 cnf(549,plain,
% 246.16/246.27 (P2(f3(f6(a2),f6(a2)),f3(f6(a2),f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[548,13])).
% 246.16/246.27 cnf(551,plain,
% 246.16/246.27 (P1(f8(f6(a2),f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[3,9,17])).
% 246.16/246.27 cnf(557,plain,
% 246.16/246.27 (P2(f3(a1,f6(a2)),f3(a2,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[3,5,9,29])).
% 246.16/246.27 cnf(576,plain,
% 246.16/246.27 (P1(f6(f3(a4,a4)))),
% 246.16/246.27 inference(scs_inference,[],[2,9,16])).
% 246.16/246.27 cnf(589,plain,
% 246.16/246.27 (P3(f3(a1,f6(a5)),f6(a5))),
% 246.16/246.27 inference(scs_inference,[],[4,9,14])).
% 246.16/246.27 cnf(592,plain,
% 246.16/246.27 (~P2(f3(a1,f6(a5)),f8(f6(a2),a4))+P2(f6(a5),f3(a2,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[589,21,344])).
% 246.16/246.27 cnf(596,plain,
% 246.16/246.27 (~P3(x5961,f3(a1,f6(a5)))+P3(x5961,f6(a5))),
% 246.16/246.27 inference(scs_inference,[],[589,19])).
% 246.16/246.27 cnf(601,plain,
% 246.16/246.27 (~P1(f3(a1,f6(a5)))+P3(f8(a4,f3(a1,f6(a5))),f6(a5))),
% 246.16/246.27 inference(scs_inference,[],[596,15])).
% 246.16/246.27 cnf(605,plain,
% 246.16/246.27 (~P1(f6(a5))+P3(f8(a4,f3(a1,f6(a5))),f6(a5))),
% 246.16/246.27 inference(scs_inference,[],[1,601,16])).
% 246.16/246.27 cnf(606,plain,
% 246.16/246.27 (P3(f6(a5),f8(a4,f3(a1,f6(a5))))+~P1(f6(a5))),
% 246.16/246.27 inference(scs_inference,[],[605,12])).
% 246.16/246.27 cnf(608,plain,
% 246.16/246.27 (~P2(x6081,f8(f6(a2),a4))+~P2(f3(a1,f6(a5)),x6081)+P2(f6(a5),f3(a2,f6(a2)))),
% 246.16/246.27 inference(scs_inference,[],[592,22])).
% 246.16/246.27 cnf(611,plain,
% 246.16/246.27 (P3(f8(a4,f6(a5)),f6(a5))),
% 246.16/246.27 inference(scs_inference,[],[4,9,15])).
% 246.16/246.27 cnf(618,plain,
% 246.16/246.27 (~P3(x6181,f8(a4,f6(a5)))+P3(x6181,f6(a5))),
% 246.16/246.27 inference(scs_inference,[],[611,19])).
% 246.16/246.27 cnf(623,plain,
% 246.16/246.27 (~P1(f8(a4,f6(a5)))+P3(f3(a1,f8(a4,f6(a5))),f6(a5))),
% 246.16/246.28 inference(scs_inference,[],[618,14])).
% 246.16/246.28 cnf(627,plain,
% 246.16/246.28 (~P1(f6(a5))+P3(f3(a1,f8(a4,f6(a5))),f6(a5))),
% 246.16/246.28 inference(scs_inference,[],[2,623,17])).
% 246.16/246.28 cnf(628,plain,
% 246.16/246.28 (P3(f6(a5),f3(a1,f8(a4,f6(a5))))+~P1(f6(a5))),
% 246.16/246.28 inference(scs_inference,[],[627,12])).
% 246.16/246.28 cnf(654,plain,
% 246.16/246.28 (P3(f6(a5),f8(a4,f3(a1,f6(a5))))),
% 246.16/246.28 inference(scs_inference,[],[4,9,606])).
% 246.16/246.28 cnf(655,plain,
% 246.16/246.28 (~P2(f6(a5),x6551)+P2(f8(a4,f3(a1,f6(a5))),x6551)),
% 246.16/246.28 inference(scs_inference,[],[654,21])).
% 246.16/246.28 cnf(691,plain,
% 246.16/246.28 (P3(f6(a5),f3(a1,f8(a4,f6(a5))))),
% 246.16/246.28 inference(scs_inference,[],[4,9,628])).
% 246.16/246.28 cnf(692,plain,
% 246.16/246.28 (~P2(f6(a5),x6921)+P2(f3(a1,f8(a4,f6(a5))),x6921)),
% 246.16/246.28 inference(scs_inference,[],[691,21])).
% 246.16/246.28 cnf(714,plain,
% 246.16/246.28 (P1(f3(f6(a5),f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,9,16])).
% 246.16/246.28 cnf(715,plain,
% 246.16/246.28 (P2(f3(f6(a5),f6(a5)),f3(f6(a5),f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[714,13])).
% 246.16/246.28 cnf(717,plain,
% 246.16/246.28 (P1(f8(f6(a5),f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,9,17])).
% 246.16/246.28 cnf(725,plain,
% 246.16/246.28 (P2(f3(a1,f6(a5)),f3(a2,f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,5,9,29])).
% 246.16/246.28 cnf(726,plain,
% 246.16/246.28 (P2(f6(a5),f3(a2,f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[589,725,21])).
% 246.16/246.28 cnf(735,plain,
% 246.16/246.28 (~P2(x7351,f6(a5))+P2(x7351,f3(a2,f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[726,22])).
% 246.16/246.28 cnf(768,plain,
% 246.16/246.28 (P3(f3(f3(f6(a5),f6(f6(a5))),f6(a5)),f3(a1,f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,93,9,27])).
% 246.16/246.28 cnf(769,plain,
% 246.16/246.28 (P3(f8(a4,f6(a5)),f8(a4,f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,46,9,28])).
% 246.16/246.28 cnf(786,plain,
% 246.16/246.28 (P2(f3(f8(f6(a1),f6(a1)),f6(a5)),f3(f8(f6(a1),f6(a1)),f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,130,9,29])).
% 246.16/246.28 cnf(788,plain,
% 246.16/246.28 (P2(f3(a1,f6(a5)),f3(f8(a2,a2),f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,145,9,29])).
% 246.16/246.28 cnf(863,plain,
% 246.16/246.28 (P3(f3(f3(a1,f6(a5)),f6(a5)),f3(f6(a5),f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,589,9,27])).
% 246.16/246.28 cnf(864,plain,
% 246.16/246.28 (~P2(f3(f3(a1,f6(a5)),f6(a5)),x8641)+P2(f3(f6(a5),f6(a5)),x8641)),
% 246.16/246.28 inference(scs_inference,[],[863,21])).
% 246.16/246.28 cnf(887,plain,
% 246.16/246.28 (P2(f3(f3(a1,f6(a5)),f6(a5)),f3(f3(f8(a2,a2),f6(a5)),f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,788,9,29])).
% 246.16/246.28 cnf(888,plain,
% 246.16/246.28 (P2(f6(a5),f3(f8(a2,a2),f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[788,589,21])).
% 246.16/246.28 cnf(890,plain,
% 246.16/246.28 (~P2(x8901,f6(a5))+P2(x8901,f3(f8(a2,a2),f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[788,589,21,22])).
% 246.16/246.28 cnf(978,plain,
% 246.16/246.28 (P3(f8(f8(f6(a2),a4),f6(a5)),f8(f6(a2),f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,275,9,28])).
% 246.16/246.28 cnf(1020,plain,
% 246.16/246.28 (P2(f6(a5),f6(a5))),
% 246.16/246.28 inference(scs_inference,[],[4,9,13])).
% 246.16/246.28 cnf(1021,plain,
% 246.16/246.28 (P2(f3(a1,f8(a4,f6(a5))),f6(a5))),
% 246.16/246.28 inference(scs_inference,[],[1020,692])).
% 246.16/246.28 cnf(1023,plain,
% 246.16/246.28 (P2(f8(a4,f3(a1,f6(a5))),f6(a5))),
% 246.16/246.28 inference(scs_inference,[],[1020,692,655])).
% 246.16/246.28 cnf(1083,plain,
% 246.16/246.28 (P3(f3(a5,a5),f3(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,10,27])).
% 246.16/246.28 cnf(1087,plain,
% 246.16/246.28 (P3(f8(a5,a5),f8(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,10,17])).
% 246.16/246.28 cnf(1105,plain,
% 246.16/246.28 (P3(f8(a4,f6(a2)),f3(a1,f6(a2)))),
% 246.16/246.28 inference(scs_inference,[],[338,12,430])).
% 246.16/246.28 cnf(1108,plain,
% 246.16/246.28 (P3(a5,f3(a1,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,12,14])).
% 246.16/246.28 cnf(1141,plain,
% 246.16/246.28 (P3(a5,f8(a4,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,12,15])).
% 246.16/246.28 cnf(1142,plain,
% 246.16/246.28 (P2(f8(a4,a5),a5)),
% 246.16/246.28 inference(scs_inference,[],[52,1141,21])).
% 246.16/246.28 cnf(1161,plain,
% 246.16/246.28 (P3(a1,f3(a5,f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,12,18])).
% 246.16/246.28 cnf(1162,plain,
% 246.16/246.28 (P2(f3(a5,f6(a5)),a2)),
% 246.16/246.28 inference(scs_inference,[],[5,1161,21])).
% 246.16/246.28 cnf(1164,plain,
% 246.16/246.28 (~P2(x11641,f3(a5,f6(a5)))+P2(x11641,a2)),
% 246.16/246.28 inference(scs_inference,[],[5,1161,21,22])).
% 246.16/246.28 cnf(1169,plain,
% 246.16/246.28 (~P1(f6(a5))+P2(f3(a1,f6(a5)),a2)),
% 246.16/246.28 inference(scs_inference,[],[6,1164,29])).
% 246.16/246.28 cnf(1175,plain,
% 246.16/246.28 (P2(f3(a1,f6(a5)),a2)),
% 246.16/246.28 inference(scs_inference,[],[4,1169,9])).
% 246.16/246.28 cnf(1176,plain,
% 246.16/246.28 (P2(f6(a5),a2)),
% 246.16/246.28 inference(scs_inference,[],[1175,589,21])).
% 246.16/246.28 cnf(1178,plain,
% 246.16/246.28 (P2(f3(a1,f8(a4,f6(a5))),a2)),
% 246.16/246.28 inference(scs_inference,[],[1175,589,21,692])).
% 246.16/246.28 cnf(1180,plain,
% 246.16/246.28 (P2(f8(a4,f3(a1,f6(a5))),a2)),
% 246.16/246.28 inference(scs_inference,[],[1175,589,21,692,655])).
% 246.16/246.28 cnf(1184,plain,
% 246.16/246.28 (~P2(x11841,f3(a1,f6(a5)))+P2(x11841,a2)),
% 246.16/246.28 inference(scs_inference,[],[1175,589,21,692,655,608,22])).
% 246.16/246.28 cnf(1190,plain,
% 246.16/246.28 (~P2(x11901,f8(a4,f3(a1,f6(a5))))+P2(x11901,a2)),
% 246.16/246.28 inference(scs_inference,[],[1180,22])).
% 246.16/246.28 cnf(1197,plain,
% 246.16/246.28 (~P2(x11971,f3(a1,f8(a4,f6(a5))))+P2(x11971,a2)),
% 246.16/246.28 inference(scs_inference,[],[1178,22])).
% 246.16/246.28 cnf(1247,plain,
% 246.16/246.28 (P3(f8(f6(a2),a4),f3(a1,f6(a2)))),
% 246.16/246.28 inference(scs_inference,[],[403,1105,19])).
% 246.16/246.28 cnf(1283,plain,
% 246.16/246.28 (P3(f6(a5),f8(a4,f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[769,12,618])).
% 246.16/246.28 cnf(1294,plain,
% 246.16/246.28 (P2(f8(a4,f6(a5)),f6(a5))),
% 246.16/246.28 inference(scs_inference,[],[1020,1283,21])).
% 246.16/246.28 cnf(1358,plain,
% 246.16/246.28 (P3(f3(a1,f6(a5)),f8(a4,f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[589,1283,19])).
% 246.16/246.28 cnf(1360,plain,
% 246.16/246.28 (P2(f8(a4,f6(a5)),a2)),
% 246.16/246.28 inference(scs_inference,[],[1175,589,1283,19,21])).
% 246.16/246.28 cnf(1369,plain,
% 246.16/246.28 (~P3(x13691,f3(a1,f6(a5)))+P3(x13691,f8(a4,f6(a5)))),
% 246.16/246.28 inference(scs_inference,[],[1358,19])).
% 246.16/246.28 cnf(1386,plain,
% 246.16/246.28 (~P2(x13861,f3(a5,f6(a5)))+P2(x13861,a5)),
% 246.16/246.28 inference(scs_inference,[],[6,1161,21,22])).
% 246.16/246.28 cnf(1391,plain,
% 246.16/246.28 (~P1(f6(a5))+P2(f3(a1,f6(a5)),a5)),
% 246.16/246.28 inference(scs_inference,[],[6,1386,29])).
% 246.16/246.28 cnf(1397,plain,
% 246.16/246.28 (P2(f3(a1,f6(a5)),a5)),
% 246.16/246.28 inference(scs_inference,[],[4,1391,9])).
% 246.16/246.28 cnf(1416,plain,
% 246.16/246.28 (P2(f3(a5,f6(a5)),a1)),
% 246.16/246.28 inference(scs_inference,[],[35,1161,21])).
% 246.16/246.28 cnf(1430,plain,
% 246.16/246.28 (P2(f3(a5,f6(a5)),f8(a2,a2))),
% 246.16/246.28 inference(scs_inference,[],[145,1416,22])).
% 246.16/246.28 cnf(1538,plain,
% 246.16/246.28 (P3(f8(a4,a5),f8(a4,a5))),
% 246.16/246.28 inference(scs_inference,[],[46,4,12,28])).
% 246.16/246.28 cnf(1539,plain,
% 246.16/246.28 (P1(f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[7,2,12,11])).
% 246.16/246.28 cnf(1540,plain,
% 246.16/246.28 (P2(f7(a4),f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[1539,13])).
% 246.16/246.28 cnf(1543,plain,
% 246.16/246.28 (P3(f8(a4,f7(a4)),a4)),
% 246.16/246.28 inference(scs_inference,[],[7,2,12,23])).
% 246.16/246.28 cnf(1544,plain,
% 246.16/246.28 (~P3(a1,f8(a4,f7(a4)))),
% 246.16/246.28 inference(scs_inference,[],[7,1543,19])).
% 246.16/246.28 cnf(1546,plain,
% 246.16/246.28 (~P3(f8(a4,f7(a4)),a1)),
% 246.16/246.28 inference(scs_inference,[],[7,1543,19,12])).
% 246.16/246.28 cnf(1548,plain,
% 246.16/246.28 (~P2(f8(a4,f7(a4)),x15481)+P2(a4,x15481)),
% 246.16/246.28 inference(scs_inference,[],[7,1543,19,12,21])).
% 246.16/246.28 cnf(1563,plain,
% 246.16/246.28 (P3(a4,f8(a4,f7(a4)))),
% 246.16/246.28 inference(scs_inference,[],[33,2,12,23])).
% 246.16/246.28 cnf(1564,plain,
% 246.16/246.28 (P2(f8(a4,f7(a4)),a4)),
% 246.16/246.28 inference(scs_inference,[],[44,1563,21])).
% 246.16/246.28 cnf(1581,plain,
% 246.16/246.28 (P2(f6(a5),a5)),
% 246.16/246.28 inference(scs_inference,[],[1397,589,21])).
% 246.16/246.28 cnf(1587,plain,
% 246.16/246.28 (P2(f8(a4,f6(a5)),a5)),
% 246.16/246.28 inference(scs_inference,[],[1397,1294,589,21,692,655,22])).
% 246.16/246.28 cnf(1706,plain,
% 246.16/246.28 (P3(f3(f6(a2),f6(a2)),f3(a1,f3(f6(a2),f6(a2))))),
% 246.16/246.28 inference(scs_inference,[],[548,12,14])).
% 246.16/246.28 cnf(1767,plain,
% 246.16/246.28 (P3(f3(f3(a5,a5),a5),f3(a5,f3(a5,a5)))),
% 246.16/246.28 inference(scs_inference,[],[4,12,30])).
% 246.16/246.28 cnf(1768,plain,
% 246.16/246.28 (~P2(f3(f3(a5,a5),a5),x17681)+P2(f3(a5,f3(a5,a5)),x17681)),
% 246.16/246.28 inference(scs_inference,[],[1767,21])).
% 246.16/246.28 cnf(1773,plain,
% 246.16/246.28 (~P2(f3(a5,a5),x17731)+P2(f3(a5,f3(a5,a5)),f3(x17731,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,1768,29])).
% 246.16/246.28 cnf(1796,plain,
% 246.16/246.28 (P3(f3(f8(a4,a5),a5),f3(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[1141,4,12,27])).
% 246.16/246.28 cnf(1797,plain,
% 246.16/246.28 (~P2(f3(f8(a4,a5),a5),x17971)+P2(f3(a5,a5),x17971)),
% 246.16/246.28 inference(scs_inference,[],[1796,21])).
% 246.16/246.28 cnf(1803,plain,
% 246.16/246.28 (~P3(x18031,f3(f8(a4,a5),a5))+P3(x18031,f3(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[1796,19])).
% 246.16/246.28 cnf(1808,plain,
% 246.16/246.28 (P3(f3(a5,a5),x18081)+~P3(x18081,f3(f8(a4,a5),a5))),
% 246.16/246.28 inference(scs_inference,[],[1803,12])).
% 246.16/246.28 cnf(1824,plain,
% 246.16/246.28 (P3(f7(a4),f3(a1,f7(a4)))),
% 246.16/246.28 inference(scs_inference,[],[1539,12,14])).
% 246.16/246.28 cnf(1825,plain,
% 246.16/246.28 (P2(f3(a1,f7(a4)),f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[1540,1824,21])).
% 246.16/246.28 cnf(1827,plain,
% 246.16/246.28 (~P2(x18271,f3(a1,f7(a4)))+P2(x18271,f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[1540,1824,21,22])).
% 246.16/246.28 cnf(1832,plain,
% 246.16/246.28 (P2(f3(f3(a5,f6(a5)),f7(a4)),f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[1416,1539,1827,29])).
% 246.16/246.28 cnf(1839,plain,
% 246.16/246.28 (~P2(f3(a1,f6(a1)),f3(f3(a5,f6(a5)),f7(a4)))+P2(f3(a1,f8(a4,f6(a1))),f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[1832,187,22,21,497,540])).
% 246.16/246.28 cnf(1856,plain,
% 246.16/246.28 (~P3(x18561,f3(a1,f6(a1)))+~P2(x18561,f3(f3(a5,f6(a5)),f7(a4)))+P2(f3(a1,f8(a4,f6(a1))),f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[1839,21])).
% 246.16/246.28 cnf(1876,plain,
% 246.16/246.28 (P3(f3(a2,a5),f3(a2,a5))),
% 246.16/246.28 inference(scs_inference,[],[50,4,12,27])).
% 246.16/246.28 cnf(1914,plain,
% 246.16/246.28 (~P2(a5,a1)+P2(f3(a5,a5),f3(a2,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,58,29])).
% 246.16/246.28 cnf(1915,plain,
% 246.16/246.28 (~P2(a5,f3(a5,f6(a5)))+P2(f3(a5,a5),f3(a2,a5))),
% 246.16/246.28 inference(scs_inference,[],[1416,1914,22])).
% 246.16/246.28 cnf(1949,plain,
% 246.16/246.28 (P3(f3(f3(a1,a5),a5),f3(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,14,27])).
% 246.16/246.28 cnf(1950,plain,
% 246.16/246.28 (~P2(f3(f3(a1,a5),a5),x19501)+P2(f3(a5,a5),x19501)),
% 246.16/246.28 inference(scs_inference,[],[1949,21])).
% 246.16/246.28 cnf(1956,plain,
% 246.16/246.28 (~P3(x19561,f3(f3(a1,a5),a5))+P3(x19561,f3(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[1949,19])).
% 246.16/246.28 cnf(1961,plain,
% 246.16/246.28 (P3(f3(a5,a5),x19611)+~P3(x19611,f3(f3(a1,a5),a5))),
% 246.16/246.28 inference(scs_inference,[],[1956,12])).
% 246.16/246.28 cnf(1975,plain,
% 246.16/246.28 (P3(f8(f3(a1,a5),a5),f8(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,14,28])).
% 246.16/246.28 cnf(1976,plain,
% 246.16/246.28 (~P2(f8(f3(a1,a5),a5),x19761)+P2(f8(a5,a5),x19761)),
% 246.16/246.28 inference(scs_inference,[],[1975,21])).
% 246.16/246.28 cnf(2001,plain,
% 246.16/246.28 (P3(f3(a1,f3(a5,a5)),f3(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,14,16])).
% 246.16/246.28 cnf(2002,plain,
% 246.16/246.28 (~P2(f3(a1,f3(a5,a5)),x20021)+P2(f3(a5,a5),x20021)),
% 246.16/246.28 inference(scs_inference,[],[2001,21])).
% 246.16/246.28 cnf(2008,plain,
% 246.16/246.28 (~P3(x20081,f3(a1,f3(a5,a5)))+P3(x20081,f3(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[2001,19])).
% 246.16/246.28 cnf(2013,plain,
% 246.16/246.28 (P3(f3(a5,a5),x20131)+~P3(x20131,f3(a1,f3(a5,a5)))),
% 246.16/246.28 inference(scs_inference,[],[2008,12])).
% 246.16/246.28 cnf(2030,plain,
% 246.16/246.28 (P3(f3(a1,f8(a5,a5)),f8(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,14,17])).
% 246.16/246.28 cnf(2031,plain,
% 246.16/246.28 (~P2(f3(a1,f8(a5,a5)),x20311)+P2(f8(a5,a5),x20311)),
% 246.16/246.28 inference(scs_inference,[],[2030,21])).
% 246.16/246.28 cnf(2062,plain,
% 246.16/246.28 (P3(f3(a1,f3(a4,a4)),f3(a4,a4))),
% 246.16/246.28 inference(scs_inference,[],[2,14,16])).
% 246.16/246.28 cnf(2100,plain,
% 246.16/246.28 (P3(f8(f8(a4,a5),a5),f8(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,15,28])).
% 246.16/246.28 cnf(2101,plain,
% 246.16/246.28 (~P2(f8(f8(a4,a5),a5),x21011)+P2(f8(a5,a5),x21011)),
% 246.16/246.28 inference(scs_inference,[],[2100,21])).
% 246.16/246.28 cnf(2133,plain,
% 246.16/246.28 (P3(f8(a4,f7(a4)),f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[33,2,15,11])).
% 246.16/246.28 cnf(2134,plain,
% 246.16/246.28 (P2(f7(a4),a4)),
% 246.16/246.28 inference(scs_inference,[],[1564,2133,21])).
% 246.16/246.28 cnf(2136,plain,
% 246.16/246.28 (P3(a4,f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[1564,1563,2133,21,19])).
% 246.16/246.28 cnf(2138,plain,
% 246.16/246.28 (P2(f3(a1,f7(a4)),a4)),
% 246.16/246.28 inference(scs_inference,[],[1564,1825,1563,2133,21,19,22])).
% 246.16/246.28 cnf(2140,plain,
% 246.16/246.28 (P3(f7(a4),a4)+~P2(a4,f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[1564,1825,1563,2133,21,19,22,20])).
% 246.16/246.28 cnf(2142,plain,
% 246.16/246.28 (~P3(a1,f7(a4))+~P2(a4,f7(a4))),
% 246.16/246.28 inference(scs_inference,[],[7,2140,19])).
% 246.16/246.28 cnf(2143,plain,
% 246.16/246.28 (~P2(x21431,f3(a1,f7(a4)))+P2(x21431,a4)),
% 246.16/246.28 inference(scs_inference,[],[2138,22])).
% 246.16/246.28 cnf(2158,plain,
% 246.16/246.28 (P2(f3(f3(a5,f6(a5)),f7(a4)),a4)),
% 246.16/246.28 inference(scs_inference,[],[1416,1539,2143,29])).
% 246.16/246.28 cnf(2163,plain,
% 246.16/246.28 (~P2(f3(a1,f6(a1)),f3(f3(a5,f6(a5)),f7(a4)))+P2(f8(a4,f3(a1,f6(a1))),a4)),
% 246.16/246.28 inference(scs_inference,[],[2158,187,22,21,497])).
% 246.16/246.28 cnf(2192,plain,
% 246.16/246.28 (~P3(x21921,f3(a1,f6(a1)))+~P2(x21921,f3(f3(a5,f6(a5)),f7(a4)))+P2(f8(a4,f3(a1,f6(a1))),a4)),
% 246.16/246.28 inference(scs_inference,[],[2163,21])).
% 246.16/246.28 cnf(2255,plain,
% 246.16/246.28 (P3(f8(a4,a5),a5)),
% 246.16/246.28 inference(scs_inference,[],[4,1538,15,19])).
% 246.16/246.28 cnf(2257,plain,
% 246.16/246.28 (P3(f8(a4,f3(a5,a5)),f3(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,15,16])).
% 246.16/246.28 cnf(2258,plain,
% 246.16/246.28 (~P2(f8(a4,f3(a5,a5)),x22581)+P2(f3(a5,a5),x22581)),
% 246.16/246.28 inference(scs_inference,[],[2257,21])).
% 246.16/246.28 cnf(2263,plain,
% 246.16/246.28 (~P2(f8(a4,f3(a5,a5)),x22631)+P2(f3(f3(a5,a5),a5),f3(x22631,a5))),
% 246.16/246.28 inference(scs_inference,[],[4,2258,29])).
% 246.16/246.28 cnf(2264,plain,
% 246.16/246.28 (~P3(x22641,f8(a4,f3(a5,a5)))+P3(x22641,f3(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[2257,19])).
% 246.16/246.28 cnf(2306,plain,
% 246.16/246.28 (P3(f8(a4,f7(a4)),f3(a1,f7(a4)))),
% 246.16/246.28 inference(scs_inference,[],[2133,1824,19])).
% 246.16/246.28 cnf(2309,plain,
% 246.16/246.28 (P3(a4,f3(a1,f7(a4)))),
% 246.16/246.28 inference(scs_inference,[],[1563,2306,19])).
% 246.16/246.28 cnf(2317,plain,
% 246.16/246.28 (P3(f8(a4,a5),f3(a1,a5))),
% 246.16/246.28 inference(scs_inference,[],[2255,1108,19])).
% 246.16/246.28 cnf(2350,plain,
% 246.16/246.28 (P3(f3(a1,a4),a4)),
% 246.16/246.28 inference(scs_inference,[],[717,2,9,14])).
% 246.16/246.28 cnf(2352,plain,
% 246.16/246.28 (P3(f8(a4,a4),a4)),
% 246.16/246.28 inference(scs_inference,[],[717,2,9,14,15])).
% 246.16/246.28 cnf(2354,plain,
% 246.16/246.28 (P3(f3(f7(a4),f6(f7(a4))),a1)),
% 246.16/246.28 inference(scs_inference,[],[717,1539,2,9,14,15,18])).
% 246.16/246.28 cnf(2356,plain,
% 246.16/246.28 (P3(f8(f8(f6(a2),a4),a4),f6(a2))),
% 246.16/246.28 inference(scs_inference,[],[717,1247,1539,2,9,14,15,18,293])).
% 246.16/246.28 cnf(2358,plain,
% 246.16/246.28 (P3(f3(a1,a5),f8(a4,a5))),
% 246.16/246.28 inference(scs_inference,[],[2317,717,1247,1539,2,9,14,15,18,293,12])).
% 246.16/246.28 cnf(2360,plain,
% 246.16/246.28 (P1(f8(f7(a4),f7(a4)))),
% 246.16/246.28 inference(scs_inference,[],[2317,717,1247,1539,2,9,14,15,18,293,12,17])).
% 246.16/246.28 cnf(2370,plain,
% 246.16/246.28 (P2(a1,f8(a5,a5))),
% 246.16/246.28 inference(scs_inference,[],[6,2317,717,1247,1539,2,9,14,15,18,293,12,17,25,26,27,28,24])).
% 246.16/246.28 cnf(2372,plain,
% 246.16/246.28 (P1(f3(f7(a4),f7(a4)))),
% 246.16/246.28 inference(scs_inference,[],[6,2317,717,1247,1539,2,9,14,15,18,293,12,17,25,26,27,28,24,16])).
% 246.16/246.28 cnf(2374,plain,
% 246.16/246.28 (P2(f3(a1,f7(a4)),f3(a5,f7(a4)))),
% 246.16/246.28 inference(scs_inference,[],[6,2317,717,1247,1539,2,9,14,15,18,293,12,17,25,26,27,28,24,16,29])).
% 246.16/246.28 cnf(2376,plain,
% 246.16/246.28 (~P2(a5,f3(a2,a5))),
% 246.16/246.28 inference(scs_inference,[],[6,2317,717,1247,1539,8,2,9,14,15,18,293,12,17,25,26,27,28,24,16,29,22])).
% 246.16/246.28 cnf(2380,plain,
% 246.16/246.28 (P3(f3(a4,f3(a4,a4)),f3(f3(a4,a4),a4))),
% 246.16/246.28 inference(scs_inference,[],[6,2317,2136,264,717,1247,1539,8,2,9,14,15,18,293,12,17,25,26,27,28,24,16,29,22,19,30])).
% 246.16/246.28 cnf(2382,plain,
% 246.16/246.28 (P3(f8(a4,f8(a4,a4)),f8(f8(a4,a4),a4))),
% 246.16/246.28 inference(scs_inference,[],[6,2317,2136,264,717,1247,1539,8,2,9,14,15,18,293,12,17,25,26,27,28,24,16,29,22,19,30,31])).
% 246.16/246.28 cnf(2384,plain,
% 246.16/246.28 (P3(f3(f8(a4,a4),f8(a4,a4)),f8(f3(a4,a4),a4))),
% 246.16/246.28 inference(scs_inference,[],[6,2317,2136,264,717,1247,1539,8,2,9,14,15,18,293,12,17,25,26,27,28,24,16,29,22,19,30,31,32])).
% 246.16/246.28 cnf(2391,plain,
% 246.16/246.28 (P3(f3(a4,f6(a4)),a1)),
% 246.16/246.28 inference(scs_inference,[],[2,18])).
% 246.16/246.28 cnf(2395,plain,
% 246.16/246.28 (P3(f8(a4,a2),a2)),
% 246.16/246.28 inference(scs_inference,[],[2372,2,3,18,9,15])).
% 246.16/246.28 cnf(2397,plain,
% 246.16/246.28 (P3(f3(a1,a2),a2)),
% 246.16/246.28 inference(scs_inference,[],[2372,2,3,18,9,15,14])).
% 246.16/246.28 cnf(2399,plain,
% 246.16/246.28 (P3(a4,f8(a4,a4))),
% 246.16/246.28 inference(scs_inference,[],[2352,2372,2,3,18,9,15,14,12])).
% 246.16/246.28 cnf(2403,plain,
% 246.16/246.28 (P1(f8(a4,a4))),
% 246.16/246.28 inference(scs_inference,[],[2358,2352,2372,1539,2,3,18,9,15,14,12,27,17])).
% 246.16/246.28 cnf(2405,plain,
% 246.16/246.28 (P2(a1,f8(f8(a5,a5),f8(a5,a5)))),
% 246.16/246.28 inference(scs_inference,[],[2358,2370,2352,2372,1539,2,3,18,9,15,14,12,27,17,24])).
% 246.16/246.28 cnf(2409,plain,
% 246.16/246.28 (P3(f8(a4,a4),f8(a4,a4))),
% 246.16/246.28 inference(scs_inference,[],[2358,2370,2352,2372,1539,2,3,18,9,15,14,12,27,17,24,25,26])).
% 246.16/246.28 cnf(2411,plain,
% 246.16/246.28 (P1(f3(a4,a4))),
% 246.16/246.28 inference(scs_inference,[],[2358,2370,2352,2372,1539,2,3,18,9,15,14,12,27,17,24,25,26,16])).
% 246.16/246.28 cnf(2417,plain,
% 246.16/246.28 (P2(a4,f3(a5,a4))),
% 246.16/246.28 inference(scs_inference,[],[6,2358,2370,2352,2350,2372,1539,8,2,3,18,9,15,14,12,27,17,24,25,26,16,29,22,21])).
% 246.16/246.29 cnf(2421,plain,
% 246.16/246.29 (P3(f3(a2,f3(a2,a2)),f3(f3(a2,a2),a2))),
% 246.16/246.29 inference(scs_inference,[],[6,2358,2370,2352,2350,2372,1546,2306,1539,8,2,3,18,9,15,14,12,27,17,24,25,26,16,29,22,21,19,30])).
% 246.16/246.29 cnf(2423,plain,
% 246.16/246.29 (P3(f3(f8(a2,a2),f8(a2,a2)),f8(f3(a2,a2),a2))),
% 246.16/246.29 inference(scs_inference,[],[6,2358,2370,2352,2350,2372,1546,2306,1539,8,2,3,18,9,15,14,12,27,17,24,25,26,16,29,22,21,19,30,32])).
% 246.16/246.29 cnf(2425,plain,
% 246.16/246.29 (P3(f8(a2,f8(a2,a2)),f8(f8(a2,a2),a2))),
% 246.16/246.29 inference(scs_inference,[],[6,2358,2370,2352,2350,2372,1546,2306,1539,8,2,3,18,9,15,14,12,27,17,24,25,26,16,29,22,21,19,30,32,31])).
% 246.16/246.29 cnf(2431,plain,
% 246.16/246.29 (~P2(f8(f8(a4,a5),a5),f3(a2,a5))),
% 246.16/246.29 inference(scs_inference,[],[6,2358,2370,2352,2350,2372,1546,2306,1539,8,2,3,18,9,15,14,12,27,17,24,25,26,16,29,22,21,19,30,32,31,1976,2031,2101])).
% 246.16/246.29 cnf(2442,plain,
% 246.16/246.29 (P3(f3(f3(a4,a4),f6(f3(a4,a4))),a1)),
% 246.16/246.29 inference(scs_inference,[],[2411,18])).
% 246.16/246.29 cnf(2444,plain,
% 246.16/246.29 (P3(f8(a4,f3(a4,a4)),f3(a4,a4))),
% 246.16/246.29 inference(scs_inference,[],[2411,18,15])).
% 246.16/246.29 cnf(2446,plain,
% 246.16/246.29 (P3(f3(a1,f8(a4,a4)),f8(a4,a4))),
% 246.16/246.29 inference(scs_inference,[],[2411,2403,18,15,14])).
% 246.16/246.29 cnf(2450,plain,
% 246.16/246.29 (P3(a2,f8(a4,a2))),
% 246.16/246.29 inference(scs_inference,[],[2411,2403,2395,2360,18,15,14,9,12])).
% 246.16/246.29 cnf(2452,plain,
% 246.16/246.29 (P1(f8(f3(a4,a4),f3(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[2411,2403,2395,2360,18,15,14,9,12,17])).
% 246.16/246.29 cnf(2458,plain,
% 246.16/246.29 (P2(a1,f8(f8(a2,a2),f8(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2409,2411,2403,2395,2360,145,18,15,14,9,12,17,27,26,24])).
% 246.16/246.29 cnf(2464,plain,
% 246.16/246.29 (P1(f3(f3(a4,a4),f3(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[2409,2411,2403,2395,2360,145,18,15,14,9,12,17,27,26,24,28,25,16])).
% 246.16/246.29 cnf(2466,plain,
% 246.16/246.29 (P2(f3(a1,f3(a4,a4)),f3(a5,f3(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[6,2409,2411,2403,2395,2360,145,18,15,14,9,12,17,27,26,24,28,25,16,29])).
% 246.16/246.29 cnf(2470,plain,
% 246.16/246.29 (P2(f8(a4,a4),f3(a5,a4))),
% 246.16/246.29 inference(scs_inference,[],[6,2409,2411,2403,2399,2417,2395,2405,2360,145,8,18,15,14,9,12,17,27,26,24,28,25,16,29,22,21])).
% 246.16/246.29 cnf(2474,plain,
% 246.16/246.29 (P3(f3(f8(a1,a1),f8(a1,a1)),f8(f3(a1,a1),a1))),
% 246.16/246.29 inference(scs_inference,[],[6,2409,2411,2403,2399,2417,2395,2405,2360,166,145,8,1,18,15,14,9,12,17,27,26,24,28,25,16,29,22,21,19,32])).
% 246.16/246.29 cnf(2476,plain,
% 246.16/246.29 (P3(f3(a1,f3(a1,a1)),f3(f3(a1,a1),a1))),
% 246.16/246.29 inference(scs_inference,[],[6,2409,2411,2403,2399,2417,2395,2405,2360,166,145,8,1,18,15,14,9,12,17,27,26,24,28,25,16,29,22,21,19,32,30])).
% 246.16/246.29 cnf(2478,plain,
% 246.16/246.29 (P3(f8(a1,f8(a1,a1)),f8(f8(a1,a1),a1))),
% 246.16/246.29 inference(scs_inference,[],[6,2409,2411,2403,2399,2417,2395,2405,2360,166,145,8,1,18,15,14,9,12,17,27,26,24,28,25,16,29,22,21,19,32,30,31])).
% 246.16/246.29 cnf(2485,plain,
% 246.16/246.29 (P3(f3(f8(a4,a4),f6(f8(a4,a4))),a1)),
% 246.16/246.29 inference(scs_inference,[],[2403,18])).
% 246.16/246.29 cnf(2489,plain,
% 246.16/246.29 (P3(f3(a1,a1),a1)),
% 246.16/246.29 inference(scs_inference,[],[2464,2403,1,18,9,14])).
% 246.16/246.29 cnf(2491,plain,
% 246.16/246.29 (P3(f8(a4,f8(a4,a4)),f8(a4,a4))),
% 246.16/246.29 inference(scs_inference,[],[2464,2403,1,18,9,14,15])).
% 246.16/246.29 cnf(2497,plain,
% 246.16/246.29 (P1(f8(f8(a4,a4),f8(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[2450,2446,2464,2403,1,18,9,14,15,12,27,17])).
% 246.16/246.29 cnf(2499,plain,
% 246.16/246.29 (P3(f8(a2,f8(a4,a4)),f8(f8(a4,a2),f8(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[2450,2446,2464,2403,1,18,9,14,15,12,27,17,28])).
% 246.16/246.29 cnf(2503,plain,
% 246.16/246.29 (P2(a1,f8(a1,a1))),
% 246.16/246.29 inference(scs_inference,[],[2450,2446,2464,2403,35,1,18,9,14,15,12,27,17,28,26,24])).
% 246.16/246.29 cnf(2505,plain,
% 246.16/246.29 (P1(f3(f8(a4,a4),f8(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[2450,2446,2464,2403,35,1,18,9,14,15,12,27,17,28,26,24,16])).
% 246.16/246.29 cnf(2507,plain,
% 246.16/246.29 (P2(f3(a1,f8(a4,a4)),f3(a5,f8(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[6,2450,2446,2464,2403,35,1,18,9,14,15,12,27,17,28,26,24,16,29])).
% 246.16/246.29 cnf(2511,plain,
% 246.16/246.29 (P2(f3(a4,a4),f3(a5,f3(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[6,2450,2446,2464,2458,2466,2403,2062,35,8,1,18,9,14,15,12,27,17,28,26,24,16,29,22,21])).
% 246.16/246.29 cnf(2515,plain,
% 246.16/246.29 (P3(f3(a5,f3(a5,a5)),f3(f3(a5,a5),a5))),
% 246.16/246.29 inference(scs_inference,[],[6,2450,2446,2464,2458,2466,2403,2062,35,8,1,4,18,9,14,15,12,27,17,28,26,24,16,29,22,21,32,30])).
% 246.16/246.29 cnf(2524,plain,
% 246.16/246.29 (P3(f3(a2,f6(a2)),a1)),
% 246.16/246.29 inference(scs_inference,[],[3,18])).
% 246.16/246.29 cnf(2526,plain,
% 246.16/246.29 (P3(f8(a4,a1),a1)),
% 246.16/246.29 inference(scs_inference,[],[3,1,18,15])).
% 246.16/246.29 cnf(2528,plain,
% 246.16/246.29 (P3(f3(a1,a5),a5)),
% 246.16/246.29 inference(scs_inference,[],[3,1,4,18,15,14])).
% 246.16/246.29 cnf(2532,plain,
% 246.16/246.29 (P3(a1,f3(a1,a1))),
% 246.16/246.29 inference(scs_inference,[],[2489,2497,3,1,4,18,15,14,9,12])).
% 246.16/246.29 cnf(2534,plain,
% 246.16/246.29 (P1(f8(a2,a2))),
% 246.16/246.29 inference(scs_inference,[],[2489,2497,3,1,4,18,15,14,9,12,17])).
% 246.16/246.29 cnf(2536,plain,
% 246.16/246.29 (P3(f3(f3(a1,a1),f3(a4,a4)),f3(a1,f3(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[2489,2497,2411,3,1,4,18,15,14,9,12,17,27])).
% 246.16/246.29 cnf(2538,plain,
% 246.16/246.29 (P2(a1,f8(f8(a1,a1),f8(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2489,2503,2497,2411,3,1,4,18,15,14,9,12,17,27,24])).
% 246.16/246.29 cnf(2542,plain,
% 246.16/246.29 (P3(f8(a2,a2),f8(a2,a2))),
% 246.16/246.29 inference(scs_inference,[],[2489,2503,2497,2411,3,1,4,18,15,14,9,12,17,27,24,25,26])).
% 246.16/246.29 cnf(2544,plain,
% 246.16/246.29 (P1(f3(a2,a2))),
% 246.16/246.29 inference(scs_inference,[],[2489,2503,2497,2411,3,1,4,18,15,14,9,12,17,27,24,25,26,16])).
% 246.16/246.29 cnf(2546,plain,
% 246.16/246.29 (P2(f3(a1,a2),f3(a5,a2))),
% 246.16/246.29 inference(scs_inference,[],[6,2489,2503,2497,2411,3,1,4,18,15,14,9,12,17,27,24,25,26,16,29])).
% 246.16/246.29 cnf(2548,plain,
% 246.16/246.29 (~P2(f8(a1,a1),f3(a2,a5))),
% 246.16/246.29 inference(scs_inference,[],[6,2489,2503,2497,2411,8,3,1,4,18,15,14,9,12,17,27,24,25,26,16,29,22])).
% 246.16/246.29 cnf(2563,plain,
% 246.16/246.29 (P3(f3(f3(a2,a2),f6(f3(a2,a2))),a1)),
% 246.16/246.29 inference(scs_inference,[],[2544,18])).
% 246.16/246.29 cnf(2565,plain,
% 246.16/246.29 (P3(f3(a1,f3(a2,a2)),f3(a2,a2))),
% 246.16/246.29 inference(scs_inference,[],[2544,18,14])).
% 246.16/246.29 cnf(2569,plain,
% 246.16/246.29 (P3(f8(a4,f3(a2,a2)),f3(a2,a2))),
% 246.16/246.29 inference(scs_inference,[],[2544,2505,18,14,9,15])).
% 246.16/246.29 cnf(2571,plain,
% 246.16/246.29 (P3(a1,f8(a4,a1))),
% 246.16/246.29 inference(scs_inference,[],[2544,2526,2505,18,14,9,15,12])).
% 246.16/246.29 cnf(2573,plain,
% 246.16/246.29 (P3(f8(f3(a1,a5),f3(a2,a2)),f8(a5,f3(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2528,2544,2526,2505,18,14,9,15,12,28])).
% 246.16/246.29 cnf(2575,plain,
% 246.16/246.29 (P3(f3(f3(a1,a5),f3(a2,a2)),f3(a5,f3(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2528,2544,2526,2505,18,14,9,15,12,28,27])).
% 246.16/246.29 cnf(2577,plain,
% 246.16/246.29 (P1(f8(f3(a2,a2),f3(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2528,2544,2526,2505,18,14,9,15,12,28,27,17])).
% 246.16/246.29 cnf(2583,plain,
% 246.16/246.29 (P1(f3(f3(a2,a2),f3(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2528,2544,2526,2505,18,14,9,15,12,28,27,17,26,25,16])).
% 246.16/246.29 cnf(2585,plain,
% 246.16/246.29 (P2(f3(a1,f3(a2,a2)),f3(a5,f3(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[6,2528,2544,2526,2505,18,14,9,15,12,28,27,17,26,25,16,29])).
% 246.16/246.29 cnf(2589,plain,
% 246.16/246.29 (P2(f3(a1,a1),a5)),
% 246.16/246.29 inference(scs_inference,[],[6,2528,2544,2532,2526,2538,2505,8,18,14,9,15,12,28,27,17,26,25,16,29,22,21])).
% 246.16/246.29 cnf(2591,plain,
% 246.16/246.29 (~P3(f3(a1,a1),f8(a4,f7(a4)))),
% 246.16/246.29 inference(scs_inference,[],[6,2528,2544,2532,2526,2538,2505,1544,8,18,14,9,15,12,28,27,17,26,25,16,29,22,21,19])).
% 246.16/246.29 cnf(2598,plain,
% 246.16/246.29 (P3(f3(f8(a2,a2),f6(f8(a2,a2))),a1)),
% 246.16/246.29 inference(scs_inference,[],[2534,18])).
% 246.16/246.29 cnf(2602,plain,
% 246.16/246.29 (P3(f8(a4,f8(a2,a2)),f8(a2,a2))),
% 246.16/246.29 inference(scs_inference,[],[2583,2534,18,9,15])).
% 246.16/246.29 cnf(2604,plain,
% 246.16/246.29 (P3(f3(a1,f8(a2,a2)),f8(a2,a2))),
% 246.16/246.29 inference(scs_inference,[],[2583,2534,18,9,15,14])).
% 246.16/246.29 cnf(2606,plain,
% 246.16/246.29 (P3(f8(a4,a4),f8(a4,f8(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[2491,2583,2534,18,9,15,14,12])).
% 246.16/246.29 cnf(2608,plain,
% 246.16/246.29 (P3(f3(a1,f8(a2,a2)),f3(f8(a4,a1),f8(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2571,2491,2583,2534,18,9,15,14,12,27])).
% 246.16/246.29 cnf(2610,plain,
% 246.16/246.29 (P3(f8(a1,f8(a2,a2)),f8(f8(a4,a1),f8(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2571,2491,2583,2534,18,9,15,14,12,27,28])).
% 246.16/246.29 cnf(2612,plain,
% 246.16/246.29 (P1(f8(f8(a2,a2),f8(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2571,2491,2583,2534,18,9,15,14,12,27,28,17])).
% 246.16/246.29 cnf(2616,plain,
% 246.16/246.29 (P1(f3(f8(a2,a2),f8(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2571,2491,2583,2534,18,9,15,14,12,27,28,17,26,16])).
% 246.16/246.29 cnf(2618,plain,
% 246.16/246.29 (P2(f3(a1,f8(a2,a2)),f3(a5,f8(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[6,2571,2491,2583,2534,18,9,15,14,12,27,28,17,26,16,29])).
% 246.16/246.29 cnf(2620,plain,
% 246.16/246.29 (P2(f7(a4),f3(a5,a4))),
% 246.16/246.29 inference(scs_inference,[],[6,2571,2491,2583,2534,2134,2417,18,9,15,14,12,27,28,17,26,16,29,22])).
% 246.16/246.29 cnf(2622,plain,
% 246.16/246.29 (P2(f8(a4,a1),a5)),
% 246.16/246.29 inference(scs_inference,[],[6,2571,2491,2583,2534,2134,2417,18,9,15,14,12,27,28,17,26,16,29,22,21])).
% 246.16/246.29 cnf(2624,plain,
% 246.16/246.29 (~P3(f8(a4,a1),f8(a4,f7(a4)))),
% 246.16/246.29 inference(scs_inference,[],[6,2571,2491,2583,2534,2134,2417,1544,18,9,15,14,12,27,28,17,26,16,29,22,21,19])).
% 246.16/246.29 cnf(2631,plain,
% 246.16/246.29 (P3(f3(a1,f6(a1)),a1)),
% 246.16/246.29 inference(scs_inference,[],[1,18])).
% 246.16/246.29 cnf(2635,plain,
% 246.16/246.29 (P3(f3(a4,a4),f8(a4,f3(a4,a4)))),
% 246.16/246.29 inference(scs_inference,[],[2444,2612,1,18,9,12])).
% 246.16/246.29 cnf(2637,plain,
% 246.16/246.29 (P1(f8(a1,a1))),
% 246.16/246.29 inference(scs_inference,[],[2444,2612,1,18,9,12,17])).
% 246.16/246.29 cnf(2639,plain,
% 246.16/246.29 (P3(f8(a1,a1),f8(a1,a1))),
% 246.16/246.29 inference(scs_inference,[],[2444,2612,1,18,9,12,17,26])).
% 246.16/246.29 cnf(2641,plain,
% 246.16/246.29 (P1(f3(a1,a1))),
% 246.16/246.29 inference(scs_inference,[],[2444,2612,1,18,9,12,17,26,16])).
% 246.16/246.29 cnf(2643,plain,
% 246.16/246.29 (P2(f3(a1,a1),f3(a5,a1))),
% 246.16/246.29 inference(scs_inference,[],[6,2444,2612,1,18,9,12,17,26,16,29])).
% 246.16/246.29 cnf(2647,plain,
% 246.16/246.29 (P2(a2,f3(a5,a2))),
% 246.16/246.29 inference(scs_inference,[],[6,2546,2444,2612,2397,2417,2158,1,18,9,12,17,26,16,29,22,21])).
% 246.16/246.29 cnf(2649,plain,
% 246.16/246.29 (P3(f3(a4,f6(a4)),f3(a1,a1))),
% 246.16/246.29 inference(scs_inference,[],[6,2546,2444,2612,2391,2397,2417,2532,2158,1,18,9,12,17,26,16,29,22,21,19])).
% 246.16/246.29 cnf(2651,plain,
% 246.16/246.29 (P3(f8(a4,f8(a1,a1)),f8(a1,a1))),
% 246.16/246.29 inference(scs_inference,[],[6,2546,2444,2612,2391,2397,2417,2532,2158,1,18,9,12,17,26,16,29,22,21,19,15])).
% 246.16/246.29 cnf(2653,plain,
% 246.16/246.29 (P3(f3(a1,f8(a1,a1)),f8(a1,a1))),
% 246.16/246.29 inference(scs_inference,[],[6,2546,2444,2612,2391,2397,2417,2532,2158,1,18,9,12,17,26,16,29,22,21,19,15,14])).
% 246.16/246.29 cnf(2664,plain,
% 246.16/246.29 (P3(f3(a1,f3(a1,a1)),f3(a1,a1))),
% 246.16/246.29 inference(scs_inference,[],[2641,18,14])).
% 246.16/246.29 cnf(2666,plain,
% 246.16/246.29 (P1(f6(f3(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2641,18,14,9])).
% 246.16/246.29 cnf(2668,plain,
% 246.16/246.29 (P3(f8(a4,f3(a1,a1)),f3(a1,a1))),
% 246.16/246.29 inference(scs_inference,[],[2641,18,14,9,15])).
% 246.16/246.29 cnf(2670,plain,
% 246.16/246.29 (P3(f3(a2,a2),f3(a1,f3(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2641,2565,18,14,9,15,12])).
% 246.16/246.29 cnf(2678,plain,
% 246.16/246.29 (P1(f8(f3(a1,a1),f3(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2641,2639,2565,18,14,9,15,12,28,27,25,17])).
% 246.16/246.29 cnf(2682,plain,
% 246.16/246.29 (P1(f3(f3(a1,a1),f3(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2641,2639,2565,18,14,9,15,12,28,27,25,17,26,16])).
% 246.16/246.29 cnf(2684,plain,
% 246.16/246.29 (P2(f3(a1,f3(a1,a1)),f3(a5,f3(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[6,2641,2639,2565,18,14,9,15,12,28,27,25,17,26,16,29])).
% 246.16/246.29 cnf(2686,plain,
% 246.16/246.29 (P2(f3(a1,f7(a4)),f3(a5,a4))),
% 246.16/246.29 inference(scs_inference,[],[6,2641,2639,2565,2138,2417,18,14,9,15,12,28,27,25,17,26,16,29,22])).
% 246.16/246.29 cnf(2690,plain,
% 246.16/246.29 (~P3(f3(a1,a1),a4)),
% 246.16/246.29 inference(scs_inference,[],[6,2641,2639,2647,2565,2450,2138,2417,2532,7,18,14,9,15,12,28,27,25,17,26,16,29,22,21,19])).
% 246.16/246.29 cnf(2703,plain,
% 246.16/246.29 (P3(f3(a1,a1),f3(a1,f3(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2664,2666,2637,18,9,12])).
% 246.16/246.29 cnf(2705,plain,
% 246.16/246.29 (P3(f8(f3(a1,f3(a1,a1)),f8(a1,a1)),f8(f3(a1,a1),f8(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2664,2666,2637,18,9,12,28])).
% 246.16/246.29 cnf(2709,plain,
% 246.16/246.29 (P1(f8(f8(a1,a1),f8(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2664,2666,2637,18,9,12,28,26,17])).
% 246.16/246.29 cnf(2711,plain,
% 246.16/246.29 (P1(f3(f8(a1,a1),f8(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2664,2666,2637,18,9,12,28,26,17,16])).
% 246.16/246.29 cnf(2713,plain,
% 246.16/246.29 (P2(f3(a1,f8(a1,a1)),f3(a5,f8(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[6,2664,2666,2637,18,9,12,28,26,17,16,29])).
% 246.16/246.29 cnf(2715,plain,
% 246.16/246.29 (P2(f6(a5),f3(a5,a2))),
% 246.16/246.29 inference(scs_inference,[],[6,2664,2666,2637,2647,1176,18,9,12,28,26,17,16,29,22])).
% 246.16/246.29 cnf(2719,plain,
% 246.16/246.29 (P3(f8(a4,f3(a2,a2)),f3(a1,f3(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[6,2664,2569,2666,2670,2635,2511,2637,2647,1176,18,9,12,28,26,17,16,29,22,21,19])).
% 246.16/246.29 cnf(2726,plain,
% 246.16/246.29 (P3(f3(a5,f6(a5)),a1)),
% 246.16/246.29 inference(scs_inference,[],[4,18])).
% 246.16/246.29 cnf(2730,plain,
% 246.16/246.29 (P3(f8(a2,a2),f8(a4,f8(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2602,2709,4,18,9,12])).
% 246.16/246.29 cnf(2732,plain,
% 246.16/246.29 (P1(f8(a5,a5))),
% 246.16/246.29 inference(scs_inference,[],[2602,2709,4,18,9,12,17])).
% 246.16/246.29 cnf(2734,plain,
% 246.16/246.29 (P1(f3(a5,a5))),
% 246.16/246.29 inference(scs_inference,[],[2602,2709,4,18,9,12,17,16])).
% 246.16/246.29 cnf(2736,plain,
% 246.16/246.29 (P2(f3(a1,f3(a1,a1)),a5)),
% 246.16/246.29 inference(scs_inference,[],[2589,2602,2709,2703,4,18,9,12,17,16,21])).
% 246.16/246.29 cnf(2740,plain,
% 246.16/246.29 (~P3(f3(a1,f3(a1,a1)),a4)),
% 246.16/246.29 inference(scs_inference,[],[2589,2690,2602,2709,2703,2647,1180,4,18,9,12,17,16,21,22,19])).
% 246.16/246.29 cnf(2742,plain,
% 246.16/246.29 (P2(f3(a1,a5),f3(a5,a5))),
% 246.16/246.29 inference(scs_inference,[],[6,2589,2690,2602,2709,2703,2647,1180,4,18,9,12,17,16,21,22,19,29])).
% 246.16/246.29 cnf(2753,plain,
% 246.16/246.29 (P3(f3(f8(a5,a5),f6(f8(a5,a5))),a1)),
% 246.16/246.29 inference(scs_inference,[],[2732,18])).
% 246.16/246.29 cnf(2757,plain,
% 246.16/246.29 (P3(f8(a2,a2),f3(a1,f8(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2732,2604,2711,18,9,12])).
% 246.16/246.29 cnf(2759,plain,
% 246.16/246.29 (P3(f3(f3(a1,f8(a2,a2)),f8(a5,a5)),f3(f8(a2,a2),f8(a5,a5)))),
% 246.16/246.29 inference(scs_inference,[],[2732,2604,2711,18,9,12,27])).
% 246.16/246.29 cnf(2761,plain,
% 246.16/246.29 (P3(f8(f3(a1,f8(a2,a2)),f8(a5,a5)),f8(f8(a2,a2),f8(a5,a5)))),
% 246.16/246.29 inference(scs_inference,[],[2732,2604,2711,18,9,12,27,28])).
% 246.16/246.29 cnf(2765,plain,
% 246.16/246.29 (P1(f8(f8(a5,a5),f8(a5,a5)))),
% 246.16/246.29 inference(scs_inference,[],[2732,2734,2604,2711,18,9,12,27,28,26,17])).
% 246.16/246.29 cnf(2767,plain,
% 246.16/246.29 (P1(f3(f8(a5,a5),f8(a5,a5)))),
% 246.16/246.29 inference(scs_inference,[],[2732,2734,2604,2711,18,9,12,27,28,26,17,16])).
% 246.16/246.29 cnf(2769,plain,
% 246.16/246.29 (P2(a5,f3(a5,a5))),
% 246.16/246.29 inference(scs_inference,[],[2732,2734,2742,2604,2711,2528,18,9,12,27,28,26,17,16,21])).
% 246.16/246.29 cnf(2773,plain,
% 246.16/246.29 (P3(f3(a1,f8(a2,a2)),f8(a4,f8(a2,a2)))),
% 246.16/246.29 inference(scs_inference,[],[2732,2734,2742,2604,2730,2711,2528,1178,2647,18,9,12,27,28,26,17,16,21,22,19])).
% 246.16/246.29 cnf(2782,plain,
% 246.16/246.29 (P3(f3(f3(a5,a5),f6(f3(a5,a5))),a1)),
% 246.16/246.29 inference(scs_inference,[],[2734,18])).
% 246.16/246.29 cnf(2786,plain,
% 246.16/246.29 (P3(f8(a1,a1),f8(a4,f8(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2651,2765,2734,18,9,12])).
% 246.16/246.29 cnf(2788,plain,
% 246.16/246.29 (P3(f3(f8(a4,f8(a1,a1)),f3(a5,a5)),f3(f8(a1,a1),f3(a5,a5)))),
% 246.16/246.29 inference(scs_inference,[],[2651,2765,2734,18,9,12,27])).
% 246.16/246.29 cnf(2790,plain,
% 246.16/246.29 (P3(f8(f8(a4,f8(a1,a1)),f3(a5,a5)),f8(f8(a1,a1),f3(a5,a5)))),
% 246.16/246.29 inference(scs_inference,[],[2651,2765,2734,18,9,12,27,28])).
% 246.16/246.29 cnf(2792,plain,
% 246.16/246.29 (P1(f8(f3(a5,a5),f3(a5,a5)))),
% 246.16/246.29 inference(scs_inference,[],[2651,2765,2734,18,9,12,27,28,17])).
% 246.16/246.29 cnf(2794,plain,
% 246.16/246.29 (P1(f3(f3(a5,a5),f3(a5,a5)))),
% 246.16/246.29 inference(scs_inference,[],[2651,2765,2734,18,9,12,27,28,17,16])).
% 246.16/246.29 cnf(2796,plain,
% 246.16/246.29 (~P2(f3(a5,f6(a5)),f3(a2,a5))),
% 246.16/246.29 inference(scs_inference,[],[8,2651,2726,2765,2734,18,9,12,27,28,17,16,21])).
% 246.16/246.29 cnf(2798,plain,
% 246.16/246.29 (P2(f8(a4,a1),f3(a5,a5))),
% 246.16/246.29 inference(scs_inference,[],[8,2622,2769,2651,2726,2765,2734,18,9,12,27,28,17,16,21,22])).
% 246.16/246.29 cnf(2800,plain,
% 246.16/246.29 (~P3(f3(f3(a1,a1),a1),a4)),
% 246.16/246.29 inference(scs_inference,[],[8,2622,2769,2651,2726,2765,2740,2476,2734,18,9,12,27,28,17,16,21,22,19])).
% 246.16/246.29 cnf(2811,plain,
% 246.16/246.29 (P3(f8(a1,a1),f3(a1,f8(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2653,2792,9,12])).
% 246.16/246.29 cnf(2813,plain,
% 246.16/246.29 (P2(a1,f3(a5,a5))),
% 246.16/246.29 inference(scs_inference,[],[2798,2653,2792,2526,9,12,21])).
% 246.16/246.29 cnf(2815,plain,
% 246.16/246.29 (P2(f3(a1,f3(a1,a1)),f3(a5,a5))),
% 246.16/246.29 inference(scs_inference,[],[2798,2653,2792,2736,2526,2769,9,12,21,22])).
% 246.16/246.29 cnf(2817,plain,
% 246.16/246.29 (P3(f3(a1,f8(a1,a1)),f8(a4,f8(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2798,2653,2792,2786,2736,2526,2769,9,12,21,22,19])).
% 246.16/246.29 cnf(2819,plain,
% 246.16/246.29 (P2(a1,f8(f3(a5,a5),f3(a5,a5)))),
% 246.16/246.29 inference(scs_inference,[],[2798,2653,2792,2786,2736,2526,2769,9,12,21,22,19,24])).
% 246.16/246.29 cnf(2828,plain,
% 246.16/246.29 (P3(f3(a1,a1),f8(a4,f3(a1,a1)))),
% 246.16/246.29 inference(scs_inference,[],[2668,2794,9,12])).
% 246.16/246.29 cnf(2832,plain,
% 246.16/246.29 (~P2(f3(a5,a5),f3(a2,a5))),
% 246.16/246.29 inference(scs_inference,[],[8,2813,2668,2354,2794,9,12,21,22])).
% 246.16/246.29 cnf(2834,plain,
% 246.16/246.29 (~P3(f3(f3(a1,a1),a1),f8(a4,a4))),
% 246.16/246.29 inference(scs_inference,[],[8,2813,2668,2800,2354,2794,2352,9,12,21,22,19])).
% 246.16/246.29 cnf(2836,plain,
% 246.16/246.29 (~P2(f3(f8(a4,a5),a5),f3(a2,a5))),
% 246.16/246.29 inference(scs_inference,[],[8,2813,2668,2800,2354,2794,2352,9,12,21,22,19,1797])).
% 246.16/246.29 cnf(2838,plain,
% 246.16/246.29 (~P2(f3(f3(a1,a5),a5),f3(a2,a5))),
% 246.16/246.29 inference(scs_inference,[],[8,2813,2668,2800,2354,2794,2352,9,12,21,22,19,1797,1950])).
% 246.16/246.29 cnf(2848,plain,
% 246.16/246.29 (~P2(a5,a1)),
% 246.16/246.29 inference(scs_inference,[],[2832,1914])).
% 246.16/246.29 cnf(2849,plain,
% 246.16/246.29 (~P2(a5,f3(a5,f6(a5)))),
% 246.16/246.29 inference(scs_inference,[],[2832,1915])).
% 246.16/246.29 cnf(2853,plain,
% 246.16/246.29 (P3(f3(a1,a1),f3(a4,f6(a4)))),
% 246.16/246.29 inference(scs_inference,[],[2649,2767,9,12])).
% 246.16/246.29 cnf(2855,plain,
% 246.16/246.29 (P3(f8(f3(a4,f6(a4)),f8(a5,a5)),f8(f3(a1,a1),f8(a5,a5)))),
% 246.16/246.29 inference(scs_inference,[],[2649,2767,2732,9,12,28])).
% 246.16/246.30 cnf(2861,plain,
% 246.16/246.30 (~P3(f3(f3(a1,a1),a1),f8(a4,f8(a4,a4)))),
% 246.16/246.30 inference(scs_inference,[],[8,2643,2834,2649,2828,2819,2767,2491,2732,9,12,28,21,22,19])).
% 246.16/246.30 cnf(2870,plain,
% 246.16/246.30 (P3(f3(a1,f7(a4)),a4)),
% 246.16/246.30 inference(scs_inference,[],[2309,2682,9,12])).
% 246.16/246.30 cnf(2872,plain,
% 246.16/246.30 (P3(f3(a4,f8(a5,a5)),f3(f3(a1,f7(a4)),f8(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[2309,2682,2732,9,12,27])).
% 246.16/246.30 cnf(2876,plain,
% 246.16/246.30 (~P2(f8(a2,a2),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[8,2796,2309,2485,2682,1430,2732,9,12,27,21,22])).
% 246.16/246.30 cnf(2891,plain,
% 246.16/246.30 (P2(f6(a5),f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[2815,2384,2678,1581,2476,2769,9,12,21,22])).
% 246.16/246.30 cnf(2893,plain,
% 246.16/246.30 (P3(f3(f3(a1,a1),f3(a4,a4)),f3(a4,a4))),
% 246.16/246.30 inference(scs_inference,[],[2815,2384,2536,2678,1581,2476,2769,2062,9,12,21,22,19])).
% 246.16/246.30 cnf(2897,plain,
% 246.16/246.30 (P2(f3(f7(a4),f3(a5,a5)),f3(f3(a5,a4),f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[2620,2815,2384,2536,2678,1581,2476,2769,2062,2734,9,12,21,22,19,20,29])).
% 246.16/246.30 cnf(2918,plain,
% 246.16/246.30 (~P2(f3(f8(a4,a5),a5),f3(a5,f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[8,2893,2849,2442,2577,94,2399,2769,9,12,21,22,19,2002,2258,1950,1797])).
% 246.16/246.30 cnf(2929,plain,
% 246.16/246.30 (P2(a4,f3(a5,f7(a4)))),
% 246.16/246.30 inference(scs_inference,[],[2870,2423,2374,2452,9,12,21])).
% 246.16/246.30 cnf(2931,plain,
% 246.16/246.30 (P2(f3(a1,a1),f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[2870,2423,2374,2452,2589,2769,9,12,21,22])).
% 246.16/246.30 cnf(2946,plain,
% 246.16/246.30 (~P2(f3(a5,a5),a1)),
% 246.16/246.30 inference(scs_inference,[],[8,2380,2563,2848,2616,2769,9,12,21,22])).
% 246.16/246.30 cnf(2950,plain,
% 246.16/246.30 (~P2(f3(a1,f3(a5,a5)),a1)),
% 246.16/246.30 inference(scs_inference,[],[8,2380,2563,2848,2446,2834,2616,2769,9,12,21,22,19,2002])).
% 246.16/246.30 cnf(2952,plain,
% 246.16/246.30 (~P2(f8(a4,f3(a5,a5)),a1)),
% 246.16/246.30 inference(scs_inference,[],[8,2380,2563,2848,2446,2834,2616,2769,9,12,21,22,19,2002,2258])).
% 246.16/246.30 cnf(2956,plain,
% 246.16/246.30 (~P2(f3(f3(a1,a5),a5),a1)),
% 246.16/246.30 inference(scs_inference,[],[8,2380,2563,2848,2446,2834,2616,2769,9,12,21,22,19,2002,2258,1797,1950])).
% 246.16/246.30 cnf(2965,plain,
% 246.16/246.30 (P3(f8(f8(a4,a4),a4),f8(a4,f8(a4,a4)))),
% 246.16/246.30 inference(scs_inference,[],[2382,12])).
% 246.16/246.30 cnf(2969,plain,
% 246.16/246.30 (P2(f8(a4,a4),f3(a5,f8(a4,a4)))),
% 246.16/246.30 inference(scs_inference,[],[2382,2507,2446,714,12,9,21])).
% 246.16/246.30 cnf(2971,plain,
% 246.16/246.30 (P2(f7(a4),f3(a5,f7(a4)))),
% 246.16/246.30 inference(scs_inference,[],[2929,2382,2507,2134,2446,714,12,9,21,22])).
% 246.16/246.30 cnf(2975,plain,
% 246.16/246.30 (P3(f3(f8(a1,a1),f8(a5,a5)),f3(f3(a1,f8(a1,a1)),f8(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[2811,2929,2382,2507,2134,2446,714,2732,12,9,21,22,19,27])).
% 246.16/246.30 cnf(2984,plain,
% 246.16/246.30 (P1(f6(a1))),
% 246.16/246.30 inference(scs_inference,[],[1,2421,12,9])).
% 246.16/246.30 cnf(2990,plain,
% 246.16/246.30 (~P3(a1,f3(a1,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[1,2950,2421,2542,35,12,9,27,28,21])).
% 246.16/246.30 cnf(3008,plain,
% 246.16/246.30 (P1(f6(f6(a1)))),
% 246.16/246.30 inference(scs_inference,[],[2984,2425,12,9])).
% 246.16/246.30 cnf(3010,plain,
% 246.16/246.30 (P3(f3(f8(a2,a2),f6(a1)),f3(f3(a1,f8(a2,a2)),f6(a1)))),
% 246.16/246.30 inference(scs_inference,[],[2984,2757,2425,12,9,27])).
% 246.16/246.30 cnf(3016,plain,
% 246.16/246.30 (P2(f8(a4,a5),f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[2984,2757,2606,2969,2425,1142,2769,12,9,27,28,21,22])).
% 246.16/246.30 cnf(3032,plain,
% 246.16/246.30 (P3(f3(f3(a1,a4),a1),f3(a4,a1))),
% 246.16/246.30 inference(scs_inference,[],[1,3008,2474,2350,12,9,27])).
% 246.16/246.30 cnf(3034,plain,
% 246.16/246.30 (P3(f8(f3(a1,a4),a1),f8(a4,a1))),
% 246.16/246.30 inference(scs_inference,[],[1,3008,2474,2350,12,9,27,28])).
% 246.16/246.30 cnf(3036,plain,
% 246.16/246.30 (~P2(f8(a4,f8(a2,a2)),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[1,2876,3008,2474,2350,2602,12,9,27,28,21])).
% 246.16/246.30 cnf(3038,plain,
% 246.16/246.30 (~P3(f8(a4,a1),f3(a1,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[1,2876,3008,2474,2990,2350,2602,2571,12,9,27,28,21,19])).
% 246.16/246.30 cnf(3046,plain,
% 246.16/246.30 (P3(f8(a4,a1),f8(f3(a1,a4),a1))),
% 246.16/246.30 inference(scs_inference,[],[3034,12])).
% 246.16/246.30 cnf(3050,plain,
% 246.16/246.30 (P3(f3(f8(f3(a1,a4),a1),f6(a1)),f3(f8(a4,a1),f6(a1)))),
% 246.16/246.30 inference(scs_inference,[],[3034,334,2984,12,9,27])).
% 246.16/246.30 cnf(3052,plain,
% 246.16/246.30 (P3(f8(f8(f3(a1,a4),a1),f6(a1)),f8(f8(a4,a1),f6(a1)))),
% 246.16/246.30 inference(scs_inference,[],[3034,334,2984,12,9,27,28])).
% 246.16/246.30 cnf(3056,plain,
% 246.16/246.30 (P3(f8(f3(a1,a4),a1),a1)),
% 246.16/246.30 inference(scs_inference,[],[3034,2585,2565,2526,334,2984,12,9,27,28,21,19])).
% 246.16/246.30 cnf(3064,plain,
% 246.16/246.30 (P3(f3(a4,a1),f3(f3(a1,a4),a1))),
% 246.16/246.30 inference(scs_inference,[],[3032,12])).
% 246.16/246.30 cnf(3068,plain,
% 246.16/246.30 (P3(f3(f8(f3(a1,a4),a1),a1),f3(a1,a1))),
% 246.16/246.30 inference(scs_inference,[],[1,3032,3056,61,12,9,27])).
% 246.16/246.30 cnf(3070,plain,
% 246.16/246.30 (P3(f8(f8(f3(a1,a4),a1),a1),f8(a1,a1))),
% 246.16/246.30 inference(scs_inference,[],[1,3032,3056,61,12,9,27,28])).
% 246.16/246.30 cnf(3072,plain,
% 246.16/246.30 (~P2(f3(a1,f8(a2,a2)),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[1,3036,3032,3056,2773,61,12,9,27,28,21])).
% 246.16/246.30 cnf(3076,plain,
% 246.16/246.30 (P2(f3(f6(a5),a1),f3(f3(a5,a5),a1))),
% 246.16/246.30 inference(scs_inference,[],[1,3036,3032,3046,3056,2773,2891,3038,61,12,9,27,28,21,19,29])).
% 246.16/246.30 cnf(3080,plain,
% 246.16/246.30 (~P2(f3(a5,f8(a2,a2)),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[1,3036,2686,3032,3046,3056,2773,2618,2891,3038,61,12,9,27,28,21,19,29,20,22])).
% 246.16/246.30 cnf(3084,plain,
% 246.16/246.30 (P3(f8(f8(a1,a1),a1),f8(a1,f8(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[2478,12])).
% 246.16/246.30 cnf(3094,plain,
% 246.16/246.30 (P2(f3(a1,a1),f3(a5,f3(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[3064,2478,2684,2929,2664,2158,576,2637,12,9,27,28,22,21])).
% 246.16/246.30 cnf(3096,plain,
% 246.16/246.30 (P3(f3(a4,a1),f3(a4,a1))),
% 246.16/246.30 inference(scs_inference,[],[3064,2478,2684,3032,2929,2664,2158,576,2637,12,9,27,28,22,21,19])).
% 246.16/246.30 cnf(3104,plain,
% 246.16/246.30 (P3(f8(a4,f8(a1,a1)),f3(a1,f8(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[2817,12])).
% 246.16/246.30 cnf(3120,plain,
% 246.16/246.30 (~P2(a2,f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[1,2548,3096,2971,2817,3070,2715,2624,3046,2796,1162,371,12,9,27,28,21,19,29,20,22])).
% 246.16/246.30 cnf(3124,plain,
% 246.16/246.30 (P3(f3(a1,f3(a2,a2)),f8(a4,f3(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[2719,12])).
% 246.16/246.30 cnf(3126,plain,
% 246.16/246.30 (P1(f6(f6(f8(a4,a4))))),
% 246.16/246.30 inference(scs_inference,[],[2719,270,12,9])).
% 246.16/246.30 cnf(3128,plain,
% 246.16/246.30 (P2(f3(a4,f6(a4)),f3(a5,f3(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[3094,2719,2853,270,12,9,21])).
% 246.16/246.30 cnf(3134,plain,
% 246.16/246.30 (P3(f3(f8(a4,a2),a1),f3(a2,a1))),
% 246.16/246.30 inference(scs_inference,[],[1,3094,3104,2719,2395,2853,2817,270,2984,12,9,21,19,29,27])).
% 246.16/246.30 cnf(3141,plain,
% 246.16/246.30 (P3(f3(a2,a1),f3(f8(a4,a2),a1))),
% 246.16/246.30 inference(scs_inference,[],[3134,12])).
% 246.16/246.30 cnf(3143,plain,
% 246.16/246.30 (P1(f6(f6(f8(a5,a5))))),
% 246.16/246.30 inference(scs_inference,[],[3134,209,12,9])).
% 246.16/246.30 cnf(3147,plain,
% 246.16/246.30 (P3(f8(f3(f8(a4,a2),a1),f3(a5,a5)),f8(f3(a2,a1),f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[3134,209,2734,12,9,27,28])).
% 246.16/246.30 cnf(3149,plain,
% 246.16/246.30 (~P2(f3(a5,a2),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[3120,3134,2647,209,2734,12,9,27,28,22])).
% 246.16/246.30 cnf(3151,plain,
% 246.16/246.30 (~P2(f3(a1,a2),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[3120,3134,2397,2647,209,2734,12,9,27,28,22,21])).
% 246.16/246.30 cnf(3155,plain,
% 246.16/246.30 (P2(f3(f3(a1,a1),a1),f3(f3(a5,a5),a1))),
% 246.16/246.30 inference(scs_inference,[],[1,3120,3134,2931,2870,2800,2397,2647,209,2734,12,9,27,28,22,21,19,29])).
% 246.16/246.30 cnf(3164,plain,
% 246.16/246.30 (P3(f3(f8(a4,a1),f8(a2,a2)),f3(a1,f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[2608,12])).
% 246.16/246.30 cnf(3168,plain,
% 246.16/246.30 (P3(f3(f3(a5,f6(a5)),a1),f3(a1,a1))),
% 246.16/246.30 inference(scs_inference,[],[1,2608,2726,551,12,9,27])).
% 246.16/246.30 cnf(3170,plain,
% 246.16/246.30 (P3(f8(f3(a5,f6(a5)),a1),f8(a1,a1))),
% 246.16/246.30 inference(scs_inference,[],[1,2608,2726,551,12,9,27,28])).
% 246.16/246.30 cnf(3172,plain,
% 246.16/246.30 (P2(a1,f3(a5,f3(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[1,3128,2608,2726,2391,551,12,9,27,28,21])).
% 246.16/246.30 cnf(3174,plain,
% 246.16/246.30 (P3(f3(a2,a1),f3(a2,a1))),
% 246.16/246.30 inference(scs_inference,[],[1,3141,3128,2608,2726,2391,3134,551,12,9,27,28,21,19])).
% 246.16/246.30 cnf(3181,plain,
% 246.16/246.30 (P3(f8(a5,f3(a2,a2)),f8(f3(a1,a5),f3(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[2573,12])).
% 246.16/246.30 cnf(3189,plain,
% 246.16/246.30 (~P2(f3(a5,f3(a1,a1)),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[1,3174,3172,2573,548,8,12,9,27,28,22])).
% 246.16/246.30 cnf(3193,plain,
% 246.16/246.30 (~P3(f3(a1,a1),f3(a1,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[1,3174,3172,3164,2573,3072,2990,2532,548,8,12,9,27,28,22,21,19])).
% 246.16/246.30 cnf(3195,plain,
% 246.16/246.30 (P2(f3(a1,a1),f3(f3(a5,f3(a1,a1)),a1))),
% 246.16/246.30 inference(scs_inference,[],[1,3174,3172,3164,2573,3072,2990,2532,548,8,12,9,27,28,22,21,19,29])).
% 246.16/246.30 cnf(3203,plain,
% 246.16/246.30 (P1(f6(a4))),
% 246.16/246.30 inference(scs_inference,[],[2,2575,12,9])).
% 246.16/246.30 cnf(3211,plain,
% 246.16/246.30 (P3(f3(f3(a1,f6(a1)),a4),f3(a1,a4))),
% 246.16/246.30 inference(scs_inference,[],[2,2575,2631,12,9,25,26,17,27])).
% 246.16/246.30 cnf(3215,plain,
% 246.16/246.30 (P3(f8(f3(a1,f6(a1)),a4),f8(a1,a4))),
% 246.16/246.30 inference(scs_inference,[],[2,2575,2631,12,9,25,26,17,27,16,28])).
% 246.16/246.30 cnf(3223,plain,
% 246.16/246.30 (P3(f8(a4,f6(a4)),f6(a4))),
% 246.16/246.30 inference(scs_inference,[],[2,3084,2713,2575,2470,2631,2478,2653,12,9,25,26,17,27,16,28,21,19,29,15])).
% 246.16/246.30 cnf(3225,plain,
% 246.16/246.30 (P3(f3(f6(a4),f6(f6(a4))),a1)),
% 246.16/246.30 inference(scs_inference,[],[2,3084,2713,2575,2470,2631,2478,2653,12,9,25,26,17,27,16,28,21,19,29,15,18])).
% 246.16/246.30 cnf(3229,plain,
% 246.16/246.30 (~P2(f3(a5,f8(a1,a1)),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[2,3193,3084,2713,2575,2548,2470,2631,2478,2653,12,9,25,26,17,27,16,28,21,19,29,15,18,20,22])).
% 246.16/246.30 cnf(3244,plain,
% 246.16/246.30 (~P3(a1,f8(a4,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[3203,3223,2952,2546,313,35,12,9,27,28,22,21])).
% 246.16/246.30 cnf(3255,plain,
% 246.16/246.30 (P3(f8(f8(a4,a1),f8(a2,a2)),f8(a1,f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[2610,12])).
% 246.16/246.30 cnf(3287,plain,
% 246.16/246.30 (P3(f8(f8(a4,a2),f8(a4,a4)),f8(a2,f8(a4,a4)))),
% 246.16/246.30 inference(scs_inference,[],[2499,12])).
% 246.16/246.30 cnf(3307,plain,
% 246.16/246.30 (~P3(a1,f3(f3(a1,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[2356,2956,129,35,12,9,21])).
% 246.16/246.30 cnf(3321,plain,
% 246.16/246.30 (P3(f3(a1,a1),f3(f3(a5,f6(a5)),a1))),
% 246.16/246.30 inference(scs_inference,[],[3168,12])).
% 246.16/246.30 cnf(3327,plain,
% 246.16/246.30 (~P3(f3(f3(a1,a1),a1),f8(f8(a4,a4),a4))),
% 246.16/246.30 inference(scs_inference,[],[2965,3168,3124,2585,2861,124,12,9,21,19])).
% 246.16/246.30 cnf(3339,plain,
% 246.16/246.30 (~P3(a1,f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[3170,2946,172,35,12,9,21])).
% 246.16/246.30 cnf(3348,plain,
% 246.16/246.30 (P3(f3(a1,a1),f3(f8(f3(a1,a4),a1),a1))),
% 246.16/246.30 inference(scs_inference,[],[3068,12])).
% 246.16/246.30 cnf(3350,plain,
% 246.16/246.30 (P1(f6(f8(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[3068,2637,12,9])).
% 246.16/246.30 cnf(3362,plain,
% 246.16/246.30 (P3(f3(a1,a4),f3(f3(a1,f6(a1)),a4))),
% 246.16/246.30 inference(scs_inference,[],[3211,12])).
% 246.16/246.30 cnf(3366,plain,
% 246.16/246.30 (~P3(a1,a5)),
% 246.16/246.30 inference(scs_inference,[],[3350,3211,2848,35,12,9,21])).
% 246.16/246.30 cnf(3374,plain,
% 246.16/246.30 (~P2(a5,a1)),
% 246.16/246.30 inference(scs_inference,[],[3366,56])).
% 246.16/246.30 cnf(3376,plain,
% 246.16/246.30 (P3(f8(a1,a4),f8(f3(a1,f6(a1)),a4))),
% 246.16/246.30 inference(scs_inference,[],[3215,12])).
% 246.16/246.30 cnf(3378,plain,
% 246.16/246.30 (P1(f6(a2))),
% 246.16/246.30 inference(scs_inference,[],[3215,3,12,9])).
% 246.16/246.30 cnf(3382,plain,
% 246.16/246.30 (P2(f3(f3(a1,a1),a1),f3(a5,f3(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[2,3215,2684,1087,2476,3,12,9,27,21])).
% 246.16/246.30 cnf(3401,plain,
% 246.16/246.30 (P3(f3(f3(a1,f8(a1,a1)),f8(a5,a5)),f3(f8(a1,a1),f8(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[2975,12])).
% 246.16/246.30 cnf(3403,plain,
% 246.16/246.30 (P1(f6(f6(a2)))),
% 246.16/246.30 inference(scs_inference,[],[3378,2975,12,9])).
% 246.16/246.30 cnf(3427,plain,
% 246.16/246.30 (P3(f8(f3(a1,a1),f8(a1,a1)),f8(f3(a1,f3(a1,a1)),f8(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[2705,12])).
% 246.16/246.30 cnf(3429,plain,
% 246.16/246.30 (P1(f6(a5))),
% 246.16/246.30 inference(scs_inference,[],[2705,4,12,9])).
% 246.16/246.30 cnf(3440,plain,
% 246.16/246.30 (P3(f3(f8(a2,a2),f8(a5,a5)),f3(f3(a1,f8(a2,a2)),f8(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[2759,12])).
% 246.16/246.30 cnf(3442,plain,
% 246.16/246.30 (P1(f6(f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3429,2759,12,9])).
% 246.16/246.30 cnf(3444,plain,
% 246.16/246.30 (P2(f8(a4,f8(a2,a2)),f3(a5,f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[3429,2759,2773,2618,12,9,21])).
% 246.16/246.30 cnf(3448,plain,
% 246.16/246.30 (P2(f3(a1,a2),f3(f8(f3(a5,a5),f3(a5,a5)),a2))),
% 246.16/246.30 inference(scs_inference,[],[3,3429,2759,2773,2819,2618,12,9,21,10,29])).
% 246.16/246.30 cnf(3455,plain,
% 246.16/246.30 (P3(f8(f8(a2,a2),f8(a5,a5)),f8(f3(a1,f8(a2,a2)),f8(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[2761,12])).
% 246.16/246.30 cnf(3463,plain,
% 246.16/246.30 (~P2(f3(f8(f3(a5,a5),f3(a5,a5)),a2),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[3,3442,2761,3448,3151,1083,12,9,27,28,22])).
% 246.16/246.30 cnf(3473,plain,
% 246.16/246.30 (P2(f8(a2,a2),f3(a5,f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[3444,2788,2602,12,21])).
% 246.16/246.30 cnf(3479,plain,
% 246.16/246.30 (P3(f8(f8(a1,a1),f3(a5,a5)),f8(f8(a4,f8(a1,a1)),f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[2790,12])).
% 246.16/246.30 cnf(3481,plain,
% 246.16/246.30 (P2(f3(f8(a2,a2),f6(a5)),f3(f3(a5,f8(a2,a2)),f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3473,2790,3429,12,29])).
% 246.16/246.30 cnf(3487,plain,
% 246.16/246.30 (P2(a2,f3(f8(f3(a5,a5),f3(a5,a5)),a2))),
% 246.16/246.30 inference(scs_inference,[],[3473,3181,2790,98,2573,3448,3429,2397,12,29,19,20,21])).
% 246.16/246.30 cnf(3491,plain,
% 246.16/246.30 (P3(f8(f3(a1,a1),f8(a5,a5)),f8(f3(a4,f6(a4)),f8(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[2855,12])).
% 246.16/246.30 cnf(3497,plain,
% 246.16/246.30 (P2(f6(a5),f3(f3(a5,f8(a2,a2)),f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3,3382,2855,3481,2736,888,12,29,20,22])).
% 246.16/246.30 cnf(3515,plain,
% 246.16/246.30 (P2(f3(a1,a2),f3(f3(a5,a5),a2))),
% 246.16/246.30 inference(scs_inference,[],[3,2897,3147,3487,2813,2450,12,21,20,29])).
% 246.16/246.30 cnf(3564,plain,
% 246.16/246.30 (P3(a5,a1)+P1(f7(a5))),
% 246.16/246.30 inference(scs_inference,[],[4,3255,2872,2610,2598,8,12,21,19,11])).
% 246.16/246.30 cnf(3570,plain,
% 246.16/246.30 (P2(f8(f3(a1,a4),a1),f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[3010,2798,3046,12,21])).
% 246.16/246.30 cnf(3595,plain,
% 246.16/246.30 (P2(f6(a5),f3(f8(f3(a5,a5),f3(a5,a5)),a2))),
% 246.16/246.30 inference(scs_inference,[],[4,3050,2715,3487,1176,12,29,22])).
% 246.16/246.30 cnf(3603,plain,
% 246.16/246.30 (P3(f8(f8(a4,a1),f6(a1)),f8(f8(f3(a1,a4),a1),f6(a1)))),
% 246.16/246.30 inference(scs_inference,[],[3052,12])).
% 246.16/246.30 cnf(3625,plain,
% 246.16/246.30 (P3(f3(a2,a2),f8(a4,f3(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[2569,12])).
% 246.16/246.30 cnf(3638,plain,
% 246.16/246.30 (P3(f3(f3(a2,a2),f6(a5)),f3(f8(a4,f3(a2,a2)),f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3625,2536,3429,12,27])).
% 246.16/246.30 cnf(3640,plain,
% 246.16/246.30 (P3(f8(f3(a2,a2),f6(a5)),f8(f8(a4,f3(a2,a2)),f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3625,2536,3429,12,27,28])).
% 246.16/246.30 cnf(3646,plain,
% 246.16/246.30 (~P2(f3(f3(a5,f3(a1,a1)),a1),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[3625,3195,2536,2489,2391,3429,8,12,27,28,21,41,22])).
% 246.16/246.30 cnf(3648,plain,
% 246.16/246.30 (P2(f3(f6(a5),a5),f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[4,3625,3195,2536,1581,2489,2391,3429,8,12,27,28,21,41,22,29])).
% 246.16/246.30 cnf(3652,plain,
% 246.16/246.30 (P3(f3(f8(a4,f3(a2,a2)),f6(a5)),f3(f3(a2,a2),f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3638,12])).
% 246.16/246.30 cnf(3666,plain,
% 246.16/246.30 (~P2(x36661,f3(a2,a5))+~P2(f3(a5,a2),x36661)),
% 246.16/246.30 inference(scs_inference,[],[4,3149,3648,3638,2782,3193,1876,2828,3378,8,12,29,27,28,21,19,20,22])).
% 246.16/246.30 cnf(3672,plain,
% 246.16/246.30 (P2(f3(f8(a4,a5),a5),f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[4,3287,3640,2499,3016,12,19,29])).
% 246.16/246.30 cnf(3674,plain,
% 246.16/246.30 (~P2(f3(f3(a5,a5),a5),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[4,2836,3287,3640,2499,3016,12,19,29,22])).
% 246.16/246.30 cnf(3676,plain,
% 246.16/246.30 (P2(f8(a4,f8(a4,a4)),f3(a5,a4))),
% 246.16/246.30 inference(scs_inference,[],[4,2836,3287,3640,2606,2499,3016,2470,12,19,29,22,21])).
% 246.16/246.30 cnf(3686,plain,
% 246.16/246.30 (P3(f8(a1,a1),f8(f8(f3(a1,a4),a1),a1))),
% 246.16/246.30 inference(scs_inference,[],[3070,12])).
% 246.16/246.30 cnf(3694,plain,
% 246.16/246.30 (~P2(f3(a5,f3(a5,a5)),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[3674,3676,2918,3672,2515,3070,2703,2591,3378,12,19,29,22,21])).
% 246.16/246.30 cnf(3700,plain,
% 246.16/246.30 (P3(f8(a4,f6(a5)),f3(a1,f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[1358,12])).
% 246.16/246.30 cnf(3704,plain,
% 246.16/246.30 (P2(f3(a5,a5),f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[3427,3672,2705,1358,1796,12,19,21])).
% 246.16/246.30 cnf(3712,plain,
% 246.16/246.30 (P1(f7(a5))),
% 246.16/246.30 inference(scs_inference,[],[3366,3564,12])).
% 246.16/246.30 cnf(3713,plain,
% 246.16/246.30 (P3(f3(a1,f7(a5)),f7(a5))),
% 246.16/246.30 inference(scs_inference,[],[3712,14])).
% 246.16/246.30 cnf(3715,plain,
% 246.16/246.30 (P3(f7(a5),f7(a5))),
% 246.16/246.30 inference(scs_inference,[],[3712,14,10])).
% 246.16/246.30 cnf(3717,plain,
% 246.16/246.30 (P3(f8(a4,f7(a5)),f7(a5))),
% 246.16/246.30 inference(scs_inference,[],[3712,14,10,15])).
% 246.16/246.30 cnf(3719,plain,
% 246.16/246.30 (P3(f3(f7(a5),f6(f7(a5))),a1)),
% 246.16/246.30 inference(scs_inference,[],[3712,14,10,15,18])).
% 246.16/246.30 cnf(3721,plain,
% 246.16/246.30 (P1(f6(f7(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3712,14,10,15,18,9])).
% 246.16/246.30 cnf(3723,plain,
% 246.16/246.30 (P3(a1,f8(f3(a1,a4),a1))),
% 246.16/246.30 inference(scs_inference,[],[3712,3056,14,10,15,18,9,12])).
% 246.16/246.30 cnf(3725,plain,
% 246.16/246.30 (~P3(f3(a4,f6(a4)),f3(a1,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[3712,2853,3056,3193,14,10,15,18,9,12,19])).
% 246.16/246.30 cnf(3733,plain,
% 246.16/246.30 (P1(f8(f7(a5),f7(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3712,3704,2853,3056,3193,14,10,15,18,9,12,19,25,29,26,17])).
% 246.16/246.30 cnf(3735,plain,
% 246.16/246.30 (P1(f3(f7(a5),f7(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3712,3704,2853,3056,3193,14,10,15,18,9,12,19,25,29,26,17,16])).
% 246.16/246.30 cnf(3753,plain,
% 246.16/246.30 (~P3(f8(f3(a1,a4),a1),a4)),
% 246.16/246.30 inference(scs_inference,[],[7,3713,3733,3721,3723,10,9,12,19])).
% 246.16/246.30 cnf(3759,plain,
% 246.16/246.30 (P2(f8(f3(a1,a4),a1),f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[7,3715,3713,3733,3721,3723,3570,3704,3429,10,9,12,19,27,28,22])).
% 246.16/246.30 cnf(3769,plain,
% 246.16/246.30 (P3(f7(a5),f8(a4,f7(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3717,3735,9,12])).
% 246.16/246.30 cnf(3771,plain,
% 246.16/246.30 (~P3(f8(f3(a1,a4),a1),f3(f3(a1,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[3717,3735,3307,3723,9,12,19])).
% 246.16/246.30 cnf(3783,plain,
% 246.16/246.30 (P3(a1,f3(f7(a5),f6(f7(a5))))),
% 246.16/246.30 inference(scs_inference,[],[3719,3721,9,12])).
% 246.16/246.30 cnf(3789,plain,
% 246.16/246.30 (P2(a1,f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[3759,3440,2759,3719,2815,3721,3704,3056,9,12,19,22,21])).
% 246.16/246.30 cnf(3795,plain,
% 246.16/246.30 (P3(f8(a4,f8(a2,a2)),f3(a1,f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[2773,12])).
% 246.16/246.30 cnf(3814,plain,
% 246.16/246.30 (P3(f3(a1,f7(a4)),f8(a4,f7(a4)))),
% 246.16/246.30 inference(scs_inference,[],[2306,12])).
% 246.16/246.30 cnf(3816,plain,
% 246.16/246.30 (P3(f8(a4,f8(a2,a2)),f3(f8(a4,a1),f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[3795,2608,2306,12,19])).
% 246.16/246.30 cnf(3818,plain,
% 246.16/246.30 (P3(f3(f7(a5),f6(a5)),f3(f8(a4,f7(a5)),f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3769,3795,2608,2306,3429,12,19,27])).
% 246.16/246.30 cnf(3820,plain,
% 246.16/246.30 (P3(f8(f7(a5),f6(a5)),f8(f8(a4,f7(a5)),f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[3769,3795,2608,2306,3429,12,19,27,28])).
% 246.16/246.30 cnf(3826,plain,
% 246.16/246.30 (P3(f3(f8(a4,a1),f8(a2,a2)),f8(a4,f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[3816,12])).
% 246.16/246.30 cnf(3832,plain,
% 246.16/246.30 (P2(f3(a1,a5),f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[3816,3771,2742,165,3704,3034,12,19,41,22])).
% 246.16/246.30 cnf(3843,plain,
% 246.16/246.30 (P2(f8(a4,a5),f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[3832,3455,3818,2761,2358,12,19,21])).
% 246.16/246.30 cnf(3851,plain,
% 246.16/246.30 (~P3(f3(f7(a5),f6(f7(a5))),f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[3820,3339,3783,12,19])).
% 246.16/246.30 cnf(3853,plain,
% 246.16/246.30 (P2(f6(a5),f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[3820,3339,3783,2891,3704,12,19,22])).
% 246.16/246.30 cnf(3855,plain,
% 246.16/246.30 (P2(a5,f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[3843,3820,3339,3783,2255,2891,3704,12,19,22,21])).
% 246.16/246.30 cnf(3867,plain,
% 246.16/246.30 (~P3(x38671,f8(f8(a4,a5),a5))+~P2(x38671,f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[2431,3853,3491,2855,2354,3378,12,19,29,21])).
% 246.16/246.30 cnf(3872,plain,
% 246.16/246.30 (P3(a1,f3(f3(a4,a4),f6(f3(a4,a4))))),
% 246.16/246.30 inference(scs_inference,[],[2442,12])).
% 246.16/246.30 cnf(3908,plain,
% 246.16/246.30 (P3(a1,f3(f8(a4,a4),f6(f8(a4,a4))))),
% 246.16/246.30 inference(scs_inference,[],[2485,12])).
% 246.16/246.30 cnf(3912,plain,
% 246.16/246.30 (~P3(x39121,f3(f3(a1,a5),a5))+~P2(x39121,f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[2838,3479,2790,2485,12,19,21])).
% 246.16/246.30 cnf(3925,plain,
% 246.16/246.30 (P2(f8(a4,f6(a5)),f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[3725,3814,3872,3855,2686,2563,3366,1587,12,21,19,20,22])).
% 246.16/246.30 cnf(3930,plain,
% 246.16/246.30 (P3(a1,f3(f8(a2,a2),f6(f8(a2,a2))))),
% 246.16/246.30 inference(scs_inference,[],[2598,12])).
% 246.16/246.30 cnf(3945,plain,
% 246.16/246.30 (~P3(f3(f8(a4,a4),f6(f8(a4,a4))),f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[3908,3925,3700,3225,3339,12,21,19])).
% 246.16/246.30 cnf(3973,plain,
% 246.16/246.30 (P3(a1,f3(f8(a5,a5),f6(f8(a5,a5))))),
% 246.16/246.30 inference(scs_inference,[],[2753,12])).
% 246.16/246.30 cnf(3982,plain,
% 246.16/246.30 (P3(a1,f3(f3(a5,a5),f6(f3(a5,a5))))),
% 246.16/246.30 inference(scs_inference,[],[2782,12])).
% 246.16/246.30 cnf(3986,plain,
% 246.16/246.30 (~P3(f3(f8(a2,a2),f6(f8(a2,a2))),f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[3930,2608,2782,2618,3339,12,21,19])).
% 246.16/246.30 cnf(3990,plain,
% 246.16/246.30 (P2(f3(a1,f8(a5,a5)),f3(a1,f8(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[35,3076,3930,2608,2782,2618,3339,2732,12,21,19,22,29])).
% 246.16/246.30 cnf(3995,plain,
% 246.16/246.30 (P3(f7(a4),a4)),
% 246.16/246.30 inference(scs_inference,[],[2136,12])).
% 246.16/246.30 cnf(3997,plain,
% 246.16/246.30 (~P2(f3(a1,a1),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[2136,2489,8,12,21])).
% 246.16/246.30 cnf(4001,plain,
% 246.16/246.30 (~P2(x40011,f3(a2,a5))+~P2(f3(a5,f8(a2,a2)),x40011)),
% 246.16/246.30 inference(scs_inference,[],[3080,3603,3052,2136,2489,8,12,21,19,22])).
% 246.16/246.30 cnf(4012,plain,
% 246.16/246.30 (~P2(f3(a5,a1),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[3997,214,2643,12,22])).
% 246.16/246.30 cnf(4014,plain,
% 246.16/246.30 (P2(f8(a5,a5),f3(a1,f8(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[3997,3990,214,2643,2030,12,22,21])).
% 246.16/246.30 cnf(4016,plain,
% 246.16/246.30 (~P3(f3(f3(a1,a1),a1),f7(a4))),
% 246.16/246.30 inference(scs_inference,[],[3995,3997,3990,2800,214,2643,2030,12,22,21,19])).
% 246.16/246.30 cnf(4020,plain,
% 246.16/246.30 (P3(f3(f7(a4),f8(a2,a2)),f3(a4,f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[3995,3997,3990,2800,214,2643,3056,2030,2534,12,22,21,19,41,27])).
% 246.16/246.30 cnf(4022,plain,
% 246.16/246.30 (P3(f8(f7(a4),f8(a2,a2)),f8(a4,f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[3995,3997,3990,2800,214,2643,3056,2030,2534,12,22,21,19,41,27,28])).
% 246.16/246.30 cnf(4026,plain,
% 246.16/246.30 (P3(f8(a4,f8(a2,a2)),f8(f7(a4),f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[4022,12])).
% 246.16/246.30 cnf(4030,plain,
% 246.16/246.30 (P3(f8(f7(a4),f8(a2,a2)),f3(a1,f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[4022,3997,2668,3795,12,21,19])).
% 246.16/246.30 cnf(4043,plain,
% 246.16/246.30 (P3(f3(a1,f8(a2,a2)),f8(f7(a4),f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[4030,12])).
% 246.16/246.30 cnf(4047,plain,
% 246.16/246.30 (~P3(f8(a4,a1),a4)),
% 246.16/246.30 inference(scs_inference,[],[4026,4030,3753,3444,3034,12,21,19])).
% 246.16/246.30 cnf(4060,plain,
% 246.16/246.30 (~P2(x40601,f3(a2,a5))+~P2(f3(a5,f8(a1,a1)),x40601)),
% 246.16/246.30 inference(scs_inference,[],[3229,3826,4020,3816,3068,3997,12,21,19,22])).
% 246.16/246.30 cnf(4071,plain,
% 246.16/246.30 (~P2(f8(a4,f3(a5,a5)),a2)),
% 246.16/246.30 inference(scs_inference,[],[3674,2263])).
% 246.16/246.30 cnf(4094,plain,
% 246.16/246.30 (~P3(a2,f8(a4,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[4071,2001,48,12,21])).
% 246.16/246.30 cnf(4098,plain,
% 246.16/246.30 (~P2(x40981,f3(a2,a5))+~P2(f3(a5,f3(a1,a1)),x40981)),
% 246.16/246.30 inference(scs_inference,[],[3189,4071,4043,4030,2001,48,12,21,19,22])).
% 246.16/246.30 cnf(4159,plain,
% 246.16/246.30 (P3(f8(a1,a4),f8(a1,a4))),
% 246.16/246.30 inference(scs_inference,[],[3376,3215,1975,12,19])).
% 246.16/246.30 cnf(4166,plain,
% 246.16/246.30 (P3(f3(a5,a5),f8(a4,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[2257,12])).
% 246.16/246.30 cnf(4204,plain,
% 246.16/246.30 (P3(a1,f3(a4,f6(a4)))),
% 246.16/246.30 inference(scs_inference,[],[2391,12])).
% 246.16/246.30 cnf(4217,plain,
% 246.16/246.30 (P3(f7(a4),f8(a4,f7(a4)))),
% 246.16/246.30 inference(scs_inference,[],[2133,12])).
% 246.16/246.30 cnf(4221,plain,
% 246.16/246.30 (~P3(f3(a4,f6(a4)),f8(a4,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[4204,3244,3348,2931,2133,12,21,19])).
% 246.16/246.30 cnf(4232,plain,
% 246.16/246.30 (~P3(f3(a1,a1),f8(a4,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[4221,3374,2649,1796,1416,12,21,19])).
% 246.16/246.30 cnf(4264,plain,
% 246.16/246.30 (P3(a1,f3(f6(a2),f6(f6(a2))))),
% 246.16/246.30 inference(scs_inference,[],[165,12])).
% 246.16/246.30 cnf(4289,plain,
% 246.16/246.30 (~P3(f3(a1,f3(a1,a1)),f8(a4,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[4232,2703,3046,2622,978,12,21,19])).
% 246.16/246.30 cnf(4294,plain,
% 246.16/246.30 (P3(a4,f3(a1,a4))),
% 246.16/246.30 inference(scs_inference,[],[2350,12])).
% 246.16/246.30 cnf(4300,plain,
% 246.16/246.30 (P3(f8(a2,a2),f8(f7(a4),f8(a2,a2)))),
% 246.16/246.30 inference(scs_inference,[],[44,2730,4026,2526,2350,3378,8,12,29,21,19])).
% 246.16/246.30 cnf(4311,plain,
% 246.16/246.30 (P2(f3(a1,a4),a4)),
% 246.16/246.30 inference(scs_inference,[],[44,4294,4300,12,21])).
% 246.16/246.30 cnf(4319,plain,
% 246.16/246.30 (P3(a2,f3(a1,a2))),
% 246.16/246.30 inference(scs_inference,[],[2397,12])).
% 246.16/246.30 cnf(4330,plain,
% 246.16/246.30 (P3(f3(f3(a1,a1),a1),f3(a1,f3(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[2476,12])).
% 246.16/246.30 cnf(4332,plain,
% 246.16/246.30 (P2(f3(f3(a1,f6(a1)),a4),a4)),
% 246.16/246.30 inference(scs_inference,[],[4311,3362,2476,12,21])).
% 246.16/246.30 cnf(4336,plain,
% 246.16/246.30 (~P2(x43361,f3(a2,a5))+~P2(f3(f8(f3(a5,a5),f3(a5,a5)),a2),x43361)),
% 246.16/246.30 inference(scs_inference,[],[4311,4319,4094,3463,3362,2476,12,21,19,22])).
% 246.16/246.30 cnf(4341,plain,
% 246.16/246.30 (P3(a1,f3(a1,f6(a1)))),
% 246.16/246.30 inference(scs_inference,[],[2631,12])).
% 246.16/246.30 cnf(4347,plain,
% 246.16/246.30 (~P3(f3(a1,f3(a1,a1)),f7(a4))),
% 246.16/246.30 inference(scs_inference,[],[4159,4330,4016,2631,2734,12,27,28,19])).
% 246.16/246.30 cnf(4349,plain,
% 246.16/246.30 (P3(a1,f6(a1))),
% 246.16/246.30 inference(scs_inference,[],[4159,4330,4016,2631,2734,12,27,28,19,188])).
% 246.16/246.30 cnf(4353,plain,
% 246.16/246.30 (P2(f3(a1,f3(a1,a1)),f3(f3(a5,a5),a1))),
% 246.16/246.30 inference(scs_inference,[],[4159,4330,4016,3155,2631,2734,12,27,28,19,188,2192,21])).
% 246.16/246.30 cnf(4360,plain,
% 246.16/246.30 (P3(f6(a1),a1)),
% 246.16/246.30 inference(scs_inference,[],[4349,12])).
% 246.16/246.30 cnf(4362,plain,
% 246.16/246.30 (~P3(f3(a1,a1),f7(a4))),
% 246.16/246.30 inference(scs_inference,[],[4349,4347,2664,12,19])).
% 246.16/246.30 cnf(4368,plain,
% 246.16/246.30 (P3(f3(a4,a4),f3(a1,f3(a4,a4)))),
% 246.16/246.30 inference(scs_inference,[],[2062,12])).
% 246.16/246.30 cnf(4372,plain,
% 246.16/246.30 (~P2(f6(a1),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[44,4360,2062,2732,8,12,29,21])).
% 246.16/246.30 cnf(4374,plain,
% 246.16/246.30 (P3(f6(a1),f3(f8(a5,a5),f6(f8(a5,a5))))),
% 246.16/246.30 inference(scs_inference,[],[44,4360,3973,2062,2732,8,12,29,21,19])).
% 246.16/246.30 cnf(4390,plain,
% 246.16/246.30 (~P2(f3(f3(a5,a5),a1),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[4362,4353,4374,3321,4341,3997,2664,12,21,19,1856,22])).
% 246.16/246.30 cnf(4394,plain,
% 246.16/246.30 (P3(a1,f3(f6(a5),f6(f6(a5))))),
% 246.16/246.30 inference(scs_inference,[],[93,12])).
% 246.16/246.30 cnf(4403,plain,
% 246.16/246.30 (P3(f3(f6(a5),f6(a5)),f3(f3(a1,f6(a5)),f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[863,12])).
% 246.16/246.30 cnf(4407,plain,
% 246.16/246.30 (~P3(f3(f3(a1,a1),a1),f8(a4,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[4289,2736,863,2476,12,21,19])).
% 246.16/246.30 cnf(4413,plain,
% 246.16/246.30 (P3(a1,f3(a2,f6(a2)))),
% 246.16/246.30 inference(scs_inference,[],[2524,12])).
% 246.16/246.30 cnf(4415,plain,
% 246.16/246.30 (P3(f3(f3(a4,a4),f3(a1,a1)),f3(f3(a1,f3(a4,a4)),f3(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[4368,2524,2641,12,27])).
% 246.16/246.30 cnf(4429,plain,
% 246.16/246.30 (P3(f3(f3(a1,f3(a4,a4)),f3(a1,a1)),f3(f3(a4,a4),f3(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[4415,12])).
% 246.16/246.30 cnf(4431,plain,
% 246.16/246.30 (P2(f3(a2,f6(a2)),f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[4413,4415,3789,12,21])).
% 246.16/246.30 cnf(4464,plain,
% 246.16/246.30 (P2(f6(a2),f3(f3(a5,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[3982,4431,4362,2503,406,3348,2030,12,22,21,19,383,91])).
% 246.16/246.30 cnf(4480,plain,
% 246.16/246.30 (~P3(f3(a1,f3(a1,a1)),f8(f8(a4,a4),a4))),
% 246.16/246.30 inference(scs_inference,[],[3327,4330,187,12,19])).
% 246.16/246.30 cnf(4500,plain,
% 246.16/246.30 (P2(a2,f3(f3(a5,a5),a2))),
% 246.16/246.30 inference(scs_inference,[],[3515,2397,21])).
% 246.16/246.30 cnf(4502,plain,
% 246.16/246.30 (~P3(f3(a1,a1),f8(f8(a4,a4),a4))),
% 246.16/246.30 inference(scs_inference,[],[4480,3515,2397,2664,21,19])).
% 246.16/246.30 cnf(4504,plain,
% 246.16/246.30 (~P2(x45041,f3(a2,a5))+~P2(f3(f3(a5,a5),a1),x45041)),
% 246.16/246.30 inference(scs_inference,[],[4390,4480,3515,2397,2664,21,19,22])).
% 246.16/246.30 cnf(4515,plain,
% 246.16/246.30 (P2(f6(a5),f3(f3(a5,a5),a2))),
% 246.16/246.30 inference(scs_inference,[],[4464,4500,1176,2403,29,22])).
% 246.16/246.30 cnf(4519,plain,
% 246.16/246.30 (~P3(x45191,f3(f3(a5,f3(a1,a1)),a1))+~P2(x45191,f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[4464,4500,3646,4429,4415,1176,2403,29,22,19,21])).
% 246.16/246.30 cnf(4535,plain,
% 246.16/246.30 (~P3(x45351,f3(a5,a2))+~P2(x45351,f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[3401,3149,4500,2975,1360,22,19,21])).
% 246.16/246.30 cnf(4645,plain,
% 246.16/246.30 (~P3(f3(f6(a2),f6(f6(a2))),f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[4264,2503,3339,21,19])).
% 246.16/246.30 cnf(4674,plain,
% 246.16/246.30 (P2(a4,f7(a4))),
% 246.16/246.30 inference(scs_inference,[],[4217,4394,1540,3366,21,19,1548])).
% 246.16/246.30 cnf(4685,plain,
% 246.16/246.30 (~P3(a1,f7(a4))),
% 246.16/246.30 inference(scs_inference,[],[4674,2142])).
% 246.16/246.30 cnf(4690,plain,
% 246.16/246.30 (~P3(x46901,f3(a5,a1))+~P2(x46901,f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[4674,4332,3652,4012,3638,22,19,21])).
% 246.16/246.30 cnf(4737,plain,
% 246.16/246.30 (~P3(f3(f6(a2),f6(f6(a2))),f3(f8(a4,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[4645,768,3704,596,1773,2008,1803])).
% 246.16/246.30 cnf(4807,plain,
% 246.16/246.30 (~P2(f3(a5,a5),a2)),
% 246.16/246.30 inference(scs_inference,[],[4071,3366,2891,3694,692,12,655,1184,1773])).
% 246.16/246.30 cnf(4809,plain,
% 246.16/246.30 (~P2(f3(a5,a5),f8(a4,f3(a1,f6(a5))))),
% 246.16/246.30 inference(scs_inference,[],[4071,3366,2891,3694,692,12,655,1184,1773,1190])).
% 246.16/246.30 cnf(4819,plain,
% 246.16/246.30 (P3(f3(f3(a1,a1),a1),f3(a1,a1))),
% 246.16/246.30 inference(scs_inference,[],[4071,2664,4330,3366,2891,4372,3694,692,12,655,1184,1773,1190,519,474,221,194,19])).
% 246.16/246.30 cnf(4821,plain,
% 246.16/246.30 (P2(f3(a2,f6(a2)),a2)),
% 246.16/246.30 inference(scs_inference,[],[5,4413,4071,2664,4330,3366,2891,4372,3694,692,12,655,1184,1773,1190,519,474,221,194,19,21])).
% 246.16/246.30 cnf(4825,plain,
% 246.16/246.30 (~P2(f3(a1,a5),a2)),
% 246.16/246.30 inference(scs_inference,[],[5,4,1416,4413,2370,4071,2664,4330,3366,2891,4372,2838,3694,692,12,655,1184,1773,1190,519,474,221,194,19,21,22,29])).
% 246.16/246.30 cnf(4846,plain,
% 246.16/246.30 (~P3(f3(a5,a5),a1)),
% 246.16/246.30 inference(scs_inference,[],[1023,3339,726,735,890,692,12])).
% 246.16/246.30 cnf(4854,plain,
% 246.16/246.30 (~P2(f3(a5,a5),f3(a1,f6(a5)))),
% 246.16/246.30 inference(scs_inference,[],[1023,3339,726,4515,887,4807,4809,735,890,692,12,655,864,2258,1184])).
% 246.16/246.30 cnf(4868,plain,
% 246.16/246.30 (~P2(f3(a1,f3(a1,a1)),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[4071,1023,2664,4330,2476,3339,3997,726,4645,4515,768,887,786,4807,4825,4809,735,890,692,12,655,864,2258,1184,1190,1197,2264,1369,20,19,21])).
% 246.16/246.30 cnf(4870,plain,
% 246.16/246.30 (P2(a1,f3(a5,a2))),
% 246.16/246.30 inference(scs_inference,[],[5,4071,1023,2664,4330,2476,3339,2647,3997,726,4645,4515,768,887,786,4807,4825,4809,735,890,692,12,655,864,2258,1184,1190,1197,2264,1369,20,19,21,22])).
% 246.16/246.30 cnf(4872,plain,
% 246.16/246.30 (~P2(a5,a2)),
% 246.16/246.30 inference(scs_inference,[],[5,4,4071,1023,2664,4330,2476,3339,2647,3997,726,4645,4515,768,2832,887,786,4807,4825,4809,735,890,692,12,655,864,2258,1184,1190,1197,2264,1369,20,19,21,22,29])).
% 246.16/246.30 cnf(4908,plain,
% 246.16/246.30 (~P2(f8(a4,a5),a2)),
% 246.16/246.30 inference(scs_inference,[],[4,4330,1021,2476,145,3473,4645,4515,4825,3853,2836,4872,4868,3945,890,692,12,655,1184,1190,2264,19,21,22,29])).
% 246.16/246.30 cnf(4961,plain,
% 246.16/246.30 (P3(f8(a4,a1),f8(a4,a1))),
% 246.16/246.30 inference(scs_inference,[],[3034,2690,3046,3497,4908,3851,3595,692,655,12,1184,2264,19])).
% 246.16/246.30 cnf(5030,plain,
% 246.16/246.30 (P2(a1,f3(a1,f8(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[2370,2800,4014,12,22])).
% 246.16/246.30 cnf(5034,plain,
% 246.16/246.30 (P3(f3(a1,f3(a1,a1)),f8(a4,f3(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[2370,2664,44,2828,2399,2800,4014,12,22,21,19])).
% 246.16/246.30 cnf(5057,plain,
% 246.16/246.30 (~P3(f7(a4),a1)),
% 246.16/246.30 inference(scs_inference,[],[4685,12])).
% 246.16/246.30 cnf(5153,plain,
% 246.16/246.30 (P3(f8(a4,a4),f8(f8(a4,a4),a4))),
% 246.16/246.30 inference(scs_inference,[],[1416,549,2382,3789,2606,2740,1706,12,22,21,19])).
% 246.16/246.30 cnf(5274,plain,
% 246.16/246.30 (P2(f3(a1,f6(a2)),a2)),
% 246.16/246.30 inference(scs_inference,[],[557,715,4289,4821,4403,12,21,22])).
% 246.16/246.30 cnf(5593,plain,
% 246.16/246.30 (~P3(f3(a5,a5),f3(f8(a4,a4),f6(f8(a4,a4))))),
% 246.16/246.30 inference(scs_inference,[],[3945,12])).
% 246.16/246.30 cnf(5743,plain,
% 246.16/246.30 (~P3(f8(f8(a4,a4),a4),f3(a1,a1))),
% 246.16/246.30 inference(scs_inference,[],[4502,12])).
% 246.16/246.30 cnf(5903,plain,
% 246.16/246.30 (P3(f3(f8(a4,a5),a5),f8(a4,f3(a5,a5)))),
% 246.16/246.30 inference(scs_inference,[],[1796,4166,4737,12,19])).
% 246.16/246.30 cnf(6001,plain,
% 246.16/246.30 (P3(f3(f3(a1,a1),a1),f8(a4,f3(a1,a1)))),
% 246.16/246.30 inference(scs_inference,[],[4330,5034,4047,12,19])).
% 246.16/246.30 cnf(6251,plain,
% 246.16/246.30 (P2(f6(a2),a2)),
% 246.16/246.30 inference(scs_inference,[],[5274,419,86])).
% 246.16/246.30 cnf(6259,plain,
% 246.16/246.30 (P2(a1,f8(f3(a5,a2),f3(a5,a2)))),
% 246.16/246.30 inference(scs_inference,[],[4870,5274,4854,419,86,355,2002,1950,24])).
% 246.16/246.30 cnf(6261,plain,
% 246.16/246.30 (P1(f7(f7(a4)))),
% 246.16/246.30 inference(scs_inference,[],[4870,5274,5057,4854,1539,419,86,355,2002,1950,24,11])).
% 246.16/246.30 cnf(6269,plain,
% 246.16/246.30 (P2(f3(a1,a5),f3(a2,a5))),
% 246.16/246.30 inference(scs_inference,[],[5,4,4819,4870,5274,5057,3712,4854,1539,419,86,355,2002,1950,24,11,27,9,28,29])).
% 246.16/246.30 cnf(6363,plain,
% 246.16/246.30 (P3(f8(f8(a4,a4),a4),f8(a4,a4))),
% 246.16/246.30 inference(scs_inference,[],[5,4,3,4961,5153,6001,6261,6259,5593,4407,4846,4809,3986,2734,1961,1808,2013,2008,1803,1956,14,15,17,16,1950,24,2002,27,28,11,29,19,12])).
% 246.16/246.30 cnf(6439,plain,
% 246.16/246.30 (P2(a2,f3(a5,a5))),
% 246.16/246.30 inference(scs_inference,[],[3,551,2734,4807,17,15,2002,13])).
% 246.16/246.30 cnf(6455,plain,
% 246.16/246.30 (~P3(f8(a4,a4),f3(a1,a1))),
% 246.16/246.30 inference(scs_inference,[],[5,3,2,6363,5030,5743,551,2734,4807,17,15,2002,13,1950,27,24,16,14,28,29,19])).
% 246.16/246.30 cnf(6627,plain,
% 246.16/246.30 (P3(f8(a4,f6(f6(a2))),f6(f6(a2)))),
% 246.16/246.30 inference(scs_inference,[],[3403,17,15])).
% 246.16/246.30 cnf(6663,plain,
% 246.16/246.30 (P2(a1,f8(f8(f3(a5,a5),f3(a5,a5)),f8(f3(a5,a5),f3(a5,a5))))),
% 246.16/246.30 inference(scs_inference,[],[2819,3350,17,14,15,24])).
% 246.16/246.30 cnf(6836,plain,
% 246.16/246.30 (~P3(f3(f8(a5,a5),f6(f8(a5,a5))),a4)),
% 246.16/246.30 inference(scs_inference,[],[7,3,6627,6439,3973,2765,17,14,15,16,29,12,19])).
% 246.16/246.30 cnf(7224,plain,
% 246.16/246.30 (~P3(f8(a4,a5),f3(a5,a1))),
% 246.16/246.30 inference(scs_inference,[],[4,1,187,1563,4071,3378,6269,2358,124,2651,6251,6455,3686,14,15,12,27,28,17,16,19,22,21,13,3867,3912,4535,4001,4060,4336,319,4098,4519,3666,4504,4690])).
% 246.16/246.30 cnf(7504,plain,
% 246.16/246.30 (P3(f3(f3(a1,a5),a5),f3(f8(a4,a5),a5))),
% 246.16/246.30 inference(scs_inference,[],[4,551,2358,714,2616,6836,3126,18,9,14,15,12,26,25,27])).
% 246.16/246.30 cnf(7566,plain,
% 246.16/246.30 ($false),
% 246.16/246.30 inference(scs_inference,[],[5,4,187,1416,3378,6269,338,371,2528,2616,717,5903,6663,7224,7504,3143,2376,18,9,14,15,12,26,25,27,24,28,17,29,16,19,22,21]),
% 246.16/246.30 ['proof']).
% 246.16/246.30 % SZS output end Proof
% 246.16/246.30 % Total time :245.530000s
%------------------------------------------------------------------------------