%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD070-2 : 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 : n028.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 182.14s 182.47s
% Output : CNFRefutation 182.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : FLD070-2 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.00/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.09/0.30 % Computer : n028.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Wed Jun 19 10:35:23 EDT 2024
% 0.09/0.30 % CPUTime :
% 0.15/0.54 start to proof:theBenchmark
% 182.14/182.46 %-------------------------------------------
% 182.14/182.46 % File :CSE---1.7
% 182.14/182.46 % Problem :theBenchmark
% 182.14/182.46 % Transform :cnf
% 182.14/182.46 % Format :tptp:raw
% 182.14/182.46 % Command :java -jar mcs_scs.jar %d %s
% 182.14/182.46
% 182.14/182.46 % Result :Theorem 181.580000s
% 182.14/182.46 % Output :CNFRefutation 181.580000s
% 182.14/182.46 %-------------------------------------------
% 182.14/182.46 %--------------------------------------------------------------------------
% 182.14/182.47 % File : FLD070-2 : TPTP v8.2.0. Bugfixed v2.1.0.
% 182.14/182.47 % Domain : Field Theory (Ordered fields)
% 182.14/182.47 % Problem : One-sided addition of two order relations
% 182.14/182.47 % Version : [Dra93] axioms : Especial.
% 182.14/182.47 % Theorem formulation : Relational with glxx axiom set.
% 182.14/182.47 % English :
% 182.14/182.47
% 182.14/182.47 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 182.14/182.47 % Source : [Dra93]
% 182.14/182.47 % Names :
% 182.14/182.47
% 182.14/182.47 % Status : Unsatisfiable
% 182.14/182.47 % Rating : 0.00 v8.1.0, 0.14 v7.5.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.38 v6.4.0, 0.25 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.30 v5.2.0, 0.10 v5.1.0, 0.09 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 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0, 0.20 v2.4.0, 0.00 v2.2.1, 0.33 v2.1.0
% 182.14/182.47 % Syntax : Number of clauses : 34 ( 10 unt; 3 nHn; 34 RR)
% 182.14/182.47 % Number of literals : 80 ( 0 equ; 45 neg)
% 182.14/182.47 % Maximal clause size : 4 ( 2 avg)
% 182.14/182.47 % Maximal term depth : 3 ( 1 avg)
% 182.14/182.47 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 182.14/182.47 % Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% 182.14/182.47 % Number of variables : 50 ( 0 sgn)
% 182.14/182.47 % SPC : CNF_UNS_RFO_NEQ_NHN
% 182.14/182.47
% 182.14/182.47 % Comments :
% 182.14/182.47 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 182.14/182.47 %--------------------------------------------------------------------------
% 182.14/182.47 include('Axioms/FLD001-0.ax').
% 182.14/182.47 %--------------------------------------------------------------------------
% 182.14/182.47 cnf(a_is_defined,hypothesis,
% 182.14/182.47 defined(a) ).
% 182.14/182.47
% 182.14/182.47 cnf(b_is_defined,hypothesis,
% 182.14/182.47 defined(b) ).
% 182.14/182.47
% 182.14/182.47 cnf(c_is_defined,hypothesis,
% 182.14/182.47 defined(c) ).
% 182.14/182.47
% 182.14/182.47 cnf(add_equals_c_4,negated_conjecture,
% 182.14/182.47 equalish(add(a,b),c) ).
% 182.14/182.47
% 182.14/182.47 cnf(less_or_equal_5,negated_conjecture,
% 182.14/182.47 less_or_equal(additive_identity,a) ).
% 182.14/182.47
% 182.14/182.47 cnf(less_or_equal_6,negated_conjecture,
% 182.14/182.47 less_or_equal(additive_identity,b) ).
% 182.14/182.47
% 182.14/182.47 cnf(not_less_or_equal_7,negated_conjecture,
% 182.14/182.47 ~ less_or_equal(additive_identity,c) ).
% 182.14/182.47
% 182.14/182.47 %--------------------------------------------------------------------------
% 182.14/182.47 %-------------------------------------------
% 182.14/182.47 % Proof found
% 182.14/182.47 % SZS status Theorem for theBenchmark
% 182.14/182.47 % SZS output start Proof
% 182.14/182.47 %ClaNum:34(EqnAxiom:0)
% 182.14/182.47 %VarNum:128(SingletonVarNum:50)
% 182.14/182.47 %MaxLitNum:4
% 182.14/182.47 %MaxfuncDepth:2
% 182.14/182.47 %SharedTerms:16
% 182.14/182.47 %goalClause: 6 7 8 10
% 182.14/182.47 %singleGoalClaCount:4
% 182.14/182.47 [1]P1(a1)
% 182.14/182.47 [2]P1(a4)
% 182.14/182.47 [3]P1(a2)
% 182.14/182.47 [4]P1(a5)
% 182.14/182.47 [5]P1(a7)
% 182.14/182.47 [6]P2(a1,a2)
% 182.14/182.47 [7]P2(a1,a5)
% 182.14/182.47 [9]~P3(a1,a4)
% 182.14/182.47 [10]~P2(a1,a7)
% 182.14/182.47 [8]P3(f3(a2,a5),a7)
% 182.14/182.47 [12]~P1(x121)+P3(x121,x121)
% 182.14/182.47 [11]~P1(x111)+P1(f6(x111))
% 182.14/182.47 [16]~P1(x161)+P3(f3(a1,x161),x161)
% 182.14/182.47 [17]~P1(x171)+P3(f9(a4,x171),x171)
% 182.14/182.47 [20]~P1(x201)+P3(f3(x201,f6(x201)),a1)
% 182.14/182.47 [14]~P3(x142,x141)+P3(x141,x142)
% 182.14/182.47 [13]~P1(x131)+P3(x131,a1)+P1(f8(x131))
% 182.14/182.47 [25]~P1(x251)+P3(x251,a1)+P3(f9(x251,f8(x251)),a4)
% 182.14/182.47 [22]~P2(x222,x221)+~P2(x221,x222)+P3(x221,x222)
% 182.14/182.47 [18]~P1(x182)+~P1(x181)+P1(f3(x181,x182))
% 182.14/182.47 [19]~P1(x192)+~P1(x191)+P1(f9(x191,x192))
% 182.14/182.47 [26]~P2(a1,x262)+~P2(a1,x261)+P2(a1,f9(x261,x262))
% 182.14/182.47 [27]~P1(x272)+~P1(x271)+P3(f3(x271,x272),f3(x272,x271))
% 182.14/182.47 [28]~P1(x282)+~P1(x281)+P3(f9(x281,x282),f9(x282,x281))
% 182.14/182.47 [21]~P3(x211,x213)+P3(x211,x212)+~P3(x213,x212)
% 182.14/182.47 [23]~P2(x233,x232)+P2(x231,x232)+~P3(x233,x231)
% 182.14/182.47 [24]~P2(x241,x243)+P2(x241,x242)+~P2(x243,x242)
% 182.14/182.47 [29]~P1(x292)+~P3(x291,x293)+P3(f3(x291,x292),f3(x293,x292))
% 182.14/182.47 [30]~P1(x302)+~P3(x301,x303)+P3(f9(x301,x302),f9(x303,x302))
% 182.14/182.47 [31]~P1(x312)+~P2(x311,x313)+P2(f3(x311,x312),f3(x313,x312))
% 182.14/182.47 [15]P2(x152,x151)+~P1(x151)+~P1(x152)+P2(x151,x152)
% 182.14/182.47 [32]~P1(x323)+~P1(x322)+~P1(x321)+P3(f3(x321,f3(x322,x323)),f3(f3(x321,x322),x323))
% 182.14/182.47 [33]~P1(x333)+~P1(x332)+~P1(x331)+P3(f9(x331,f9(x332,x333)),f9(f9(x331,x332),x333))
% 182.14/182.47 [34]~P1(x343)+~P1(x342)+~P1(x341)+P3(f3(f9(x341,x342),f9(x343,x342)),f9(f3(x341,x343),x342))
% 182.14/182.47 %EqnAxiom
% 182.14/182.47
% 182.14/182.47 %-------------------------------------------
% 182.14/182.49 cnf(35,plain,
% 182.14/182.49 (~P3(a4,a1)),
% 182.14/182.49 inference(scs_inference,[],[9,14])).
% 182.14/182.49 cnf(37,plain,
% 182.14/182.49 (P2(a1,a1)),
% 182.14/182.49 inference(scs_inference,[],[1,9,14,15])).
% 182.14/182.49 cnf(44,plain,
% 182.14/182.49 (P3(a1,a1)),
% 182.14/182.49 inference(scs_inference,[],[37,22])).
% 182.14/182.49 cnf(46,plain,
% 182.14/182.49 (P2(a4,a4)),
% 182.14/182.49 inference(scs_inference,[],[2,37,22,15])).
% 182.14/182.49 cnf(48,plain,
% 182.14/182.49 (~P2(f3(a2,a5),x481)+P2(a7,x481)),
% 182.14/182.49 inference(scs_inference,[],[8,2,37,22,15,23])).
% 182.14/182.49 cnf(55,plain,
% 182.14/182.49 (P2(a2,a2)),
% 182.14/182.49 inference(scs_inference,[],[3,46,22,15])).
% 182.14/182.49 cnf(57,plain,
% 182.14/182.49 (~P3(x571,f3(a2,a5))+P3(x571,a7)),
% 182.14/182.49 inference(scs_inference,[],[8,3,46,22,15,21])).
% 182.14/182.49 cnf(63,plain,
% 182.14/182.49 (P2(a7,a7)),
% 182.14/182.49 inference(scs_inference,[],[55,5,22,15])).
% 182.14/182.49 cnf(65,plain,
% 182.14/182.49 (P3(a7,a7)),
% 182.14/182.49 inference(scs_inference,[],[63,22])).
% 182.14/182.49 cnf(67,plain,
% 182.14/182.49 (P2(a5,a5)),
% 182.14/182.49 inference(scs_inference,[],[63,4,22,15])).
% 182.14/182.49 cnf(73,plain,
% 182.14/182.49 (~P2(a5,a1)+P2(a5,a2)),
% 182.14/182.49 inference(scs_inference,[],[6,7,22,23])).
% 182.14/182.49 cnf(76,plain,
% 182.14/182.49 (P1(f6(f8(a4)))),
% 182.14/182.49 inference(scs_inference,[],[35,2,11,13])).
% 182.14/182.49 cnf(89,plain,
% 182.14/182.49 (P3(f3(a1,f6(a4)),f6(a4))),
% 182.14/182.49 inference(scs_inference,[],[2,16,11])).
% 182.14/182.49 cnf(92,plain,
% 182.14/182.49 (~P1(f6(a4))+P2(f6(a4),f3(a2,f6(a4)))),
% 182.14/182.49 inference(scs_inference,[],[6,89,23,31])).
% 182.14/182.49 cnf(100,plain,
% 182.14/182.49 (~P3(x1001,f3(a1,f6(a4)))+P3(x1001,f6(a4))),
% 182.14/182.49 inference(scs_inference,[],[89,21])).
% 182.14/182.49 cnf(105,plain,
% 182.14/182.49 (P3(f3(f6(a2),f6(f6(a2))),a1)),
% 182.14/182.49 inference(scs_inference,[],[3,20,11])).
% 182.14/182.49 cnf(108,plain,
% 182.14/182.49 (~P3(a4,f3(f6(a2),f6(f6(a2))))),
% 182.14/182.49 inference(scs_inference,[],[10,35,105,23,21])).
% 182.14/182.49 cnf(112,plain,
% 182.14/182.49 (P2(a7,f3(a2,a5))),
% 182.14/182.49 inference(scs_inference,[],[55,4,48,31])).
% 182.14/182.49 cnf(127,plain,
% 182.14/182.49 (P3(f3(a5,a2),a7)),
% 182.14/182.49 inference(scs_inference,[],[3,4,57,27])).
% 182.14/182.49 cnf(128,plain,
% 182.14/182.49 (~P2(f3(a5,a2),x1281)+P2(a7,x1281)),
% 182.14/182.49 inference(scs_inference,[],[127,23])).
% 182.14/182.49 cnf(134,plain,
% 182.14/182.49 (~P3(x1341,f3(a5,a2))+P3(x1341,a7)),
% 182.14/182.49 inference(scs_inference,[],[127,21])).
% 182.14/182.49 cnf(139,plain,
% 182.14/182.49 (P2(a7,f3(a5,a2))),
% 182.14/182.49 inference(scs_inference,[],[67,3,128,31])).
% 182.14/182.49 cnf(140,plain,
% 182.14/182.49 (P3(a7,f3(a5,a2))+~P2(f3(a5,a2),a7)),
% 182.14/182.49 inference(scs_inference,[],[139,22])).
% 182.14/182.49 cnf(146,plain,
% 182.14/182.49 (P3(a7,x1461)+~P3(x1461,f3(a5,a2))),
% 182.14/182.49 inference(scs_inference,[],[134,14])).
% 182.14/182.49 cnf(148,plain,
% 182.14/182.49 (P3(a7,f3(a2,a5))),
% 182.14/182.49 inference(scs_inference,[],[4,3,146,27])).
% 182.14/182.49 cnf(149,plain,
% 182.14/182.49 (P2(f3(a2,a5),f3(a2,a5))),
% 182.14/182.49 inference(scs_inference,[],[112,148,23])).
% 182.14/182.49 cnf(159,plain,
% 182.14/182.49 (P2(f3(a2,a5),a7)),
% 182.14/182.49 inference(scs_inference,[],[63,148,23])).
% 182.14/182.49 cnf(163,plain,
% 182.14/182.49 (P2(f3(a2,a5),f3(a5,a2))),
% 182.14/182.49 inference(scs_inference,[],[139,159,24])).
% 182.14/182.49 cnf(168,plain,
% 182.14/182.49 (P3(f3(a2,a5),f3(a5,a2))+~P2(f3(a5,a2),f3(a2,a5))),
% 182.14/182.49 inference(scs_inference,[],[163,22])).
% 182.14/182.49 cnf(170,plain,
% 182.14/182.49 (~P1(f3(a1,f6(a4)))+P3(f3(a1,f3(a1,f6(a4))),f6(a4))),
% 182.14/182.49 inference(scs_inference,[],[100,16])).
% 182.14/182.49 cnf(172,plain,
% 182.14/182.49 (~P3(f3(a2,a5),f3(a5,a2))+P3(a7,f3(a5,a2))),
% 182.14/182.49 inference(scs_inference,[],[159,140,23])).
% 182.14/182.49 cnf(178,plain,
% 182.14/182.49 (~P3(f3(a2,a5),f3(a5,a2))+P3(f9(a7,a4),f9(f3(a5,a2),a4))),
% 182.14/182.49 inference(scs_inference,[],[2,172,30])).
% 182.14/182.49 cnf(182,plain,
% 182.14/182.49 (P2(f3(a5,a2),f3(a5,a2))+~P2(f3(a5,a2),f3(a2,a5))),
% 182.14/182.49 inference(scs_inference,[],[163,168,23])).
% 182.14/182.49 cnf(183,plain,
% 182.14/182.49 (~P1(f6(a4))+P3(f3(a1,f3(a1,f6(a4))),f6(a4))),
% 182.14/182.49 inference(scs_inference,[],[1,170,18])).
% 182.14/182.49 cnf(184,plain,
% 182.14/182.49 (P3(f3(a5,a2),f3(a2,a5))),
% 182.14/182.49 inference(scs_inference,[],[127,148,21])).
% 182.14/182.49 cnf(186,plain,
% 182.14/182.49 (~P2(f3(a5,a2),x1861)+P2(f3(a2,a5),x1861)),
% 182.14/182.49 inference(scs_inference,[],[127,148,21,23])).
% 182.14/182.49 cnf(192,plain,
% 182.14/182.49 (~P3(x1921,f3(a5,a2))+P3(x1921,f3(a2,a5))),
% 182.14/182.49 inference(scs_inference,[],[184,21])).
% 182.14/182.49 cnf(195,plain,
% 182.14/182.49 (P3(f3(a2,a5),x1951)+~P3(x1951,f3(a5,a2))),
% 182.14/182.49 inference(scs_inference,[],[192,14])).
% 182.14/182.49 cnf(196,plain,
% 182.14/182.49 (~P3(a1,f3(a5,a2))),
% 182.14/182.49 inference(scs_inference,[],[10,159,195,23])).
% 182.14/182.49 cnf(197,plain,
% 182.14/182.49 (~P3(f3(a5,a2),a1)),
% 182.14/182.49 inference(scs_inference,[],[196,14])).
% 182.14/182.49 cnf(199,plain,
% 182.14/182.49 (P3(f6(a4),f3(a1,f3(a1,f6(a4))))+~P1(f6(a4))),
% 182.14/182.49 inference(scs_inference,[],[183,14])).
% 182.14/182.49 cnf(203,plain,
% 182.14/182.49 (~P3(a7,f3(a5,a2))+P2(f3(a5,a2),f3(a5,a2))),
% 182.14/182.49 inference(scs_inference,[],[112,182,23])).
% 182.14/182.49 cnf(208,plain,
% 182.14/182.49 (~P3(f3(f6(a2),f6(f6(a2))),f3(a5,a2))),
% 182.14/182.49 inference(scs_inference,[],[197,105,21,14])).
% 182.14/182.49 cnf(212,plain,
% 182.14/182.49 (P3(f9(a7,a4),f9(f3(a5,a2),a4))),
% 182.14/182.49 inference(scs_inference,[],[184,178,14])).
% 182.14/182.49 cnf(219,plain,
% 182.14/182.49 (~P3(x2191,f9(a7,a4))+P3(x2191,f9(f3(a5,a2),a4))),
% 182.14/182.49 inference(scs_inference,[],[212,21])).
% 182.14/182.49 cnf(222,plain,
% 182.14/182.49 (P3(f9(f3(a5,a2),a4),x2221)+~P3(x2221,f9(a7,a4))),
% 182.14/182.49 inference(scs_inference,[],[219,14])).
% 182.14/182.49 cnf(255,plain,
% 182.14/182.49 (~P2(a1,f3(a2,a5))),
% 182.14/182.49 inference(scs_inference,[],[10,159,24])).
% 182.14/182.49 cnf(257,plain,
% 182.14/182.49 (P1(f9(f6(a1),f6(a1)))),
% 182.14/182.49 inference(scs_inference,[],[1,19,11])).
% 182.14/182.49 cnf(264,plain,
% 182.14/182.49 (P3(f9(f3(a5,a2),f8(f3(a5,a2))),a4)),
% 182.14/182.49 inference(scs_inference,[],[197,3,4,25,18])).
% 182.14/182.49 cnf(267,plain,
% 182.14/182.49 (~P3(f9(f3(a5,a2),f8(f3(a5,a2))),a1)),
% 182.14/182.49 inference(scs_inference,[],[9,264,21,14])).
% 182.14/182.49 cnf(276,plain,
% 182.14/182.49 (P2(a7,a1)),
% 182.14/182.49 inference(scs_inference,[],[10,5,1,15])).
% 182.14/182.49 cnf(278,plain,
% 182.14/182.49 (P2(f3(a2,a5),a1)),
% 182.14/182.49 inference(scs_inference,[],[10,159,5,1,15,24])).
% 182.14/182.49 cnf(281,plain,
% 182.14/182.49 (P2(f3(a2,a5),a2)),
% 182.14/182.49 inference(scs_inference,[],[6,278,24])).
% 182.14/182.49 cnf(286,plain,
% 182.14/182.49 (P2(f3(a2,a5),a5)),
% 182.14/182.49 inference(scs_inference,[],[7,278,24])).
% 182.14/182.49 cnf(288,plain,
% 182.14/182.49 (P3(f3(a2,a5),a5)+~P2(a5,f3(a2,a5))),
% 182.14/182.49 inference(scs_inference,[],[7,278,24,22])).
% 182.14/182.49 cnf(291,plain,
% 182.14/182.49 (P2(a7,a2)),
% 182.14/182.49 inference(scs_inference,[],[112,281,24])).
% 182.14/182.49 cnf(296,plain,
% 182.14/182.49 (P2(a7,a5)),
% 182.14/182.49 inference(scs_inference,[],[112,286,24])).
% 182.14/182.49 cnf(298,plain,
% 182.14/182.49 (P3(a7,a5)+~P2(a5,a7)),
% 182.14/182.49 inference(scs_inference,[],[112,286,24,22])).
% 182.14/182.49 cnf(300,plain,
% 182.14/182.49 (~P2(a5,f3(a2,a5))+P3(a7,a5)),
% 182.14/182.49 inference(scs_inference,[],[159,298,24])).
% 182.14/182.49 cnf(304,plain,
% 182.14/182.49 (~P2(a5,a7)+P3(f3(a2,a5),a5)),
% 182.14/182.49 inference(scs_inference,[],[112,288,24])).
% 182.14/182.49 cnf(305,plain,
% 182.14/182.49 (P2(a5,f3(a5,a2))+~P2(a5,a7)),
% 182.14/182.49 inference(scs_inference,[],[163,304,23])).
% 182.14/182.49 cnf(306,plain,
% 182.14/182.49 (~P2(a5,f3(a2,a5))+P2(a5,f3(a5,a2))),
% 182.14/182.49 inference(scs_inference,[],[159,305,24])).
% 182.14/182.49 cnf(330,plain,
% 182.14/182.49 (P2(a1,f9(a2,a1))),
% 182.14/182.49 inference(scs_inference,[],[6,1,26,15])).
% 182.14/182.49 cnf(331,plain,
% 182.14/182.49 (P2(f3(a2,a5),f9(a2,a1))),
% 182.14/182.49 inference(scs_inference,[],[278,330,24])).
% 182.14/182.49 cnf(333,plain,
% 182.14/182.49 (P3(a1,f9(a2,a1))+~P2(f9(a2,a1),a1)),
% 182.14/182.49 inference(scs_inference,[],[278,330,24,22])).
% 182.14/182.49 cnf(336,plain,
% 182.14/182.49 (P2(f9(a2,a1),a2)+~P2(f9(a2,a1),a1)),
% 182.14/182.49 inference(scs_inference,[],[6,333,23])).
% 182.14/182.49 cnf(337,plain,
% 182.14/182.49 (P2(a7,f9(a2,a1))),
% 182.14/182.49 inference(scs_inference,[],[112,331,24])).
% 182.14/182.49 cnf(343,plain,
% 182.14/182.49 (~P2(f9(a2,a1),f3(a2,a5))+P2(f9(a2,a1),a2)),
% 182.14/182.49 inference(scs_inference,[],[278,336,24])).
% 182.14/182.49 cnf(346,plain,
% 182.14/182.49 (~P3(a7,f9(a2,a1))+P2(f9(a2,a1),a2)),
% 182.14/182.49 inference(scs_inference,[],[112,343,23])).
% 182.14/182.49 cnf(347,plain,
% 182.14/182.49 (~P3(f9(a2,a1),f3(a5,a2))+P2(f9(a2,a1),a2)),
% 182.14/182.49 inference(scs_inference,[],[346,146])).
% 182.14/182.49 cnf(349,plain,
% 182.14/182.49 (~P3(f3(a5,a2),f9(a2,a1))+P2(f9(a2,a1),a2)),
% 182.14/182.49 inference(scs_inference,[],[347,14])).
% 182.14/182.49 cnf(351,plain,
% 182.14/182.49 (~P2(f3(a5,a2),f9(a2,a1))+~P2(f9(a2,a1),f3(a5,a2))+P2(f9(a2,a1),a2)),
% 182.14/182.49 inference(scs_inference,[],[349,22])).
% 182.14/182.49 cnf(383,plain,
% 182.14/182.49 (~P3(a7,f3(a5,a2))+~P2(f9(a2,a1),f3(a5,a2))+P2(f9(a2,a1),a2)),
% 182.14/182.49 inference(scs_inference,[],[337,351,23])).
% 182.14/182.49 cnf(384,plain,
% 182.14/182.49 (~P2(f9(a2,a1),a7)+~P3(a7,f3(a5,a2))+P2(f9(a2,a1),a2)),
% 182.14/182.49 inference(scs_inference,[],[139,383,24])).
% 182.14/182.49 cnf(385,plain,
% 182.14/182.49 (~P3(f3(a2,a5),f9(a2,a1))+~P3(a7,f3(a5,a2))+P2(f9(a2,a1),a2)),
% 182.14/182.49 inference(scs_inference,[],[159,384,23])).
% 182.14/182.49 cnf(418,plain,
% 182.14/182.49 (P1(f6(f3(a7,a7)))),
% 182.14/182.49 inference(scs_inference,[],[5,11,18])).
% 182.14/182.49 cnf(427,plain,
% 182.14/182.49 (P1(f6(f3(a4,a4)))),
% 182.14/182.49 inference(scs_inference,[],[2,11,18])).
% 182.14/182.49 cnf(428,plain,
% 182.14/182.49 (P2(f6(f3(a4,a4)),f6(f3(a4,a4)))),
% 182.14/182.49 inference(scs_inference,[],[427,15])).
% 182.14/182.49 cnf(430,plain,
% 182.14/182.49 (P3(f3(a1,f6(a5)),f6(a5))),
% 182.14/182.49 inference(scs_inference,[],[4,11,16])).
% 182.14/182.49 cnf(439,plain,
% 182.14/182.49 (~P3(x4391,f3(a1,f6(a5)))+P3(x4391,f6(a5))),
% 182.14/182.49 inference(scs_inference,[],[430,21])).
% 182.14/182.49 cnf(443,plain,
% 182.14/182.49 (~P1(f3(a1,f6(a5)))+P3(f9(a4,f3(a1,f6(a5))),f6(a5))),
% 182.14/182.49 inference(scs_inference,[],[439,17])).
% 182.14/182.49 cnf(450,plain,
% 182.14/182.49 (~P1(f6(a5))+P3(f9(a4,f3(a1,f6(a5))),f6(a5))),
% 182.14/182.49 inference(scs_inference,[],[1,443,18])).
% 182.14/182.49 cnf(451,plain,
% 182.14/182.49 (P3(f6(a5),f9(a4,f3(a1,f6(a5))))+~P1(f6(a5))),
% 182.14/182.49 inference(scs_inference,[],[450,14])).
% 182.14/182.49 cnf(466,plain,
% 182.14/182.49 (P3(f3(f6(a4),f6(f6(a4))),a1)),
% 182.14/182.49 inference(scs_inference,[],[2,11,20])).
% 182.14/182.49 cnf(469,plain,
% 182.14/182.49 (~P3(a4,f3(f6(a4),f6(f6(a4))))),
% 182.14/182.49 inference(scs_inference,[],[10,35,466,23,21])).
% 182.14/182.49 cnf(475,plain,
% 182.14/182.49 (P1(f6(f9(a2,a2)))),
% 182.14/182.49 inference(scs_inference,[],[3,11,19])).
% 182.14/182.49 cnf(476,plain,
% 182.14/182.49 (P2(f6(f9(a2,a2)),f6(f9(a2,a2)))),
% 182.14/182.49 inference(scs_inference,[],[475,15])).
% 182.14/182.49 cnf(478,plain,
% 182.14/182.49 (P2(f6(a4),f3(a2,f6(a4)))),
% 182.14/182.49 inference(scs_inference,[],[2,11,92])).
% 182.14/182.49 cnf(481,plain,
% 182.14/182.49 (~P2(x4811,f6(a4))+P2(x4811,f3(a2,f6(a4)))),
% 182.14/182.49 inference(scs_inference,[],[478,476,22,24])).
% 182.14/182.49 cnf(503,plain,
% 182.14/182.49 (P1(f6(f3(a2,a2)))),
% 182.14/182.49 inference(scs_inference,[],[3,11,18])).
% 182.14/182.49 cnf(504,plain,
% 182.14/182.49 (P2(f6(f3(a2,a2)),f6(f3(a2,a2)))),
% 182.14/182.49 inference(scs_inference,[],[503,15])).
% 182.14/182.49 cnf(506,plain,
% 182.14/182.49 (P3(f9(a4,f6(a5)),f6(a5))),
% 182.14/182.49 inference(scs_inference,[],[4,11,17])).
% 182.14/182.49 cnf(511,plain,
% 182.14/182.49 (~P2(f9(a4,f6(a5)),f6(a4))+P2(f6(a5),f3(a2,f6(a4)))),
% 182.14/182.49 inference(scs_inference,[],[504,506,22,23,481])).
% 182.14/182.49 cnf(515,plain,
% 182.14/182.49 (~P3(x5151,f9(a4,f6(a5)))+P3(x5151,f6(a5))),
% 182.14/182.49 inference(scs_inference,[],[506,21])).
% 182.14/182.49 cnf(518,plain,
% 182.14/182.49 (~P1(f9(a4,f6(a5)))+P3(f3(a1,f9(a4,f6(a5))),f6(a5))),
% 182.14/182.49 inference(scs_inference,[],[515,16])).
% 182.14/182.49 cnf(519,plain,
% 182.14/182.49 (~P2(x5191,f6(a4))+~P2(f9(a4,f6(a5)),x5191)+P2(f6(a5),f3(a2,f6(a4)))),
% 182.14/182.49 inference(scs_inference,[],[511,24])).
% 182.14/182.49 cnf(520,plain,
% 182.14/182.49 (~P1(f6(a5))+P3(f3(a1,f9(a4,f6(a5))),f6(a5))),
% 182.14/182.49 inference(scs_inference,[],[2,518,19])).
% 182.14/182.50 cnf(521,plain,
% 182.14/182.50 (P3(f6(a5),f3(a1,f9(a4,f6(a5))))+~P1(f6(a5))),
% 182.14/182.50 inference(scs_inference,[],[520,14])).
% 182.14/182.50 cnf(526,plain,
% 182.14/182.50 (~P2(f9(a4,f6(a5)),x5261)+~P2(x5261,f6(a4))+P2(f3(f6(a5),a2),f3(f3(a2,f6(a4)),a2))),
% 182.14/182.50 inference(scs_inference,[],[3,519,31])).
% 182.14/182.50 cnf(528,plain,
% 182.14/182.50 (P1(f6(f9(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,11,19])).
% 182.14/182.50 cnf(529,plain,
% 182.14/182.50 (P2(f6(f9(a5,a5)),f6(f9(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[528,15])).
% 182.14/182.50 cnf(563,plain,
% 182.14/182.50 (P3(f3(f6(a5),f6(f6(a5))),a1)),
% 182.14/182.50 inference(scs_inference,[],[4,11,20])).
% 182.14/182.50 cnf(566,plain,
% 182.14/182.50 (~P3(a4,f3(f6(a5),f6(f6(a5))))),
% 182.14/182.50 inference(scs_inference,[],[10,35,563,23,21])).
% 182.14/182.50 cnf(573,plain,
% 182.14/182.50 (P3(f6(a4),f3(a1,f3(a1,f6(a4))))),
% 182.14/182.50 inference(scs_inference,[],[2,11,199])).
% 182.14/182.50 cnf(596,plain,
% 182.14/182.50 (P3(f6(a5),f9(a4,f3(a1,f6(a5))))),
% 182.14/182.50 inference(scs_inference,[],[4,11,451])).
% 182.14/182.50 cnf(597,plain,
% 182.14/182.50 (~P2(f6(a5),x5971)+P2(f9(a4,f3(a1,f6(a5))),x5971)),
% 182.14/182.50 inference(scs_inference,[],[596,23])).
% 182.14/182.50 cnf(600,plain,
% 182.14/182.50 (P2(f9(a4,f3(a1,f6(a5))),a2)+~P2(f6(a5),a1)),
% 182.14/182.50 inference(scs_inference,[],[6,597,24])).
% 182.14/182.50 cnf(606,plain,
% 182.14/182.50 (P3(f3(a1,f9(a4,f6(a5))),f6(a5))),
% 182.14/182.50 inference(scs_inference,[],[4,11,520])).
% 182.14/182.50 cnf(611,plain,
% 182.14/182.50 (~P2(f3(a1,f9(a4,f6(a5))),a1)+P2(f9(a4,f3(a1,f6(a5))),a2)),
% 182.14/182.50 inference(scs_inference,[],[606,23,597,600])).
% 182.14/182.50 cnf(633,plain,
% 182.14/182.50 (~P2(f3(a1,f9(a4,f6(a5))),f3(a2,a5))+P2(f9(a4,f3(a1,f6(a5))),a2)),
% 182.14/182.50 inference(scs_inference,[],[278,611,24])).
% 182.14/182.50 cnf(640,plain,
% 182.14/182.50 (~P2(x6401,f9(a4,f3(a1,f6(a5))))+P2(x6401,a2)+~P2(f3(a1,f9(a4,f6(a5))),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[633,24])).
% 182.14/182.50 cnf(648,plain,
% 182.14/182.50 (P3(f3(a1,f6(a2)),f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[3,11,16])).
% 182.14/182.50 cnf(655,plain,
% 182.14/182.50 (~P3(x6551,f3(a1,f6(a2)))+P3(x6551,f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[648,21])).
% 182.14/182.50 cnf(658,plain,
% 182.14/182.50 (~P1(f3(a1,f6(a2)))+P3(f9(a4,f3(a1,f6(a2))),f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[655,17])).
% 182.14/182.50 cnf(660,plain,
% 182.14/182.50 (~P1(f6(a2))+P3(f9(a4,f3(a1,f6(a2))),f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[1,658,18])).
% 182.14/182.50 cnf(661,plain,
% 182.14/182.50 (P3(f6(a2),f9(a4,f3(a1,f6(a2))))+~P1(f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[660,14])).
% 182.14/182.50 cnf(665,plain,
% 182.14/182.50 (P3(f9(a4,f6(a2)),f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[3,11,17])).
% 182.14/182.50 cnf(672,plain,
% 182.14/182.50 (~P3(x6721,f9(a4,f6(a2)))+P3(x6721,f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[665,21])).
% 182.14/182.50 cnf(675,plain,
% 182.14/182.50 (~P1(f9(a4,f6(a2)))+P3(f3(a1,f9(a4,f6(a2))),f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[672,16])).
% 182.14/182.50 cnf(677,plain,
% 182.14/182.50 (~P1(f6(a2))+P3(f3(a1,f9(a4,f6(a2))),f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[2,675,19])).
% 182.14/182.50 cnf(678,plain,
% 182.14/182.50 (P3(f6(a2),f3(a1,f9(a4,f6(a2))))+~P1(f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[677,14])).
% 182.14/182.50 cnf(682,plain,
% 182.14/182.50 (P3(f6(a5),f3(a1,f9(a4,f6(a5))))),
% 182.14/182.50 inference(scs_inference,[],[4,11,521])).
% 182.14/182.50 cnf(683,plain,
% 182.14/182.50 (~P2(f6(a5),x6831)+P2(f3(a1,f9(a4,f6(a5))),x6831)),
% 182.14/182.50 inference(scs_inference,[],[682,23])).
% 182.14/182.50 cnf(723,plain,
% 182.14/182.50 (P3(f6(a2),f9(a4,f3(a1,f6(a2))))),
% 182.14/182.50 inference(scs_inference,[],[3,11,661])).
% 182.14/182.50 cnf(724,plain,
% 182.14/182.50 (~P2(f6(a2),x7241)+P2(f9(a4,f3(a1,f6(a2))),x7241)),
% 182.14/182.50 inference(scs_inference,[],[723,23])).
% 182.14/182.50 cnf(780,plain,
% 182.14/182.50 (P3(f6(a2),f3(a1,f9(a4,f6(a2))))),
% 182.14/182.50 inference(scs_inference,[],[3,11,678])).
% 182.14/182.50 cnf(781,plain,
% 182.14/182.50 (~P2(f6(a2),x7811)+P2(f3(a1,f9(a4,f6(a2))),x7811)),
% 182.14/182.50 inference(scs_inference,[],[780,23])).
% 182.14/182.50 cnf(792,plain,
% 182.14/182.50 (P1(f3(f6(a4),f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[2,11,18])).
% 182.14/182.50 cnf(795,plain,
% 182.14/182.50 (P1(f9(f6(a5),f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,11,19])).
% 182.14/182.50 cnf(806,plain,
% 182.14/182.50 (P1(f9(f6(a4),f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[2,11,19])).
% 182.14/182.50 cnf(807,plain,
% 182.14/182.50 (P2(f9(f6(a4),f6(a4)),f9(f6(a4),f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[806,15])).
% 182.14/182.50 cnf(809,plain,
% 182.14/182.50 (P1(f3(f6(a2),f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,11,18])).
% 182.14/182.50 cnf(819,plain,
% 182.14/182.50 (P1(f9(f6(a2),f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,11,19])).
% 182.14/182.50 cnf(820,plain,
% 182.14/182.50 (P2(f9(f6(a2),f6(a2)),f9(f6(a2),f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[819,15])).
% 182.14/182.50 cnf(822,plain,
% 182.14/182.50 (P3(f3(f3(a2,a5),f6(a5)),f3(a7,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,8,11,29])).
% 182.14/182.50 cnf(825,plain,
% 182.14/182.50 (~P2(f3(f3(a2,a5),f6(a5)),x8251)+P2(f3(a7,f6(a5)),x8251)),
% 182.14/182.50 inference(scs_inference,[],[820,822,22,23])).
% 182.14/182.50 cnf(830,plain,
% 182.14/182.50 (~P1(f6(a5))+P2(f3(a7,f6(a5)),f3(f3(a5,a2),f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[163,825,31])).
% 182.14/182.50 cnf(841,plain,
% 182.14/182.50 (P2(f3(a7,f6(a5)),f3(f3(a5,a2),f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,11,830])).
% 182.14/182.50 cnf(848,plain,
% 182.14/182.50 (P3(f3(a7,f6(a5)),f3(f3(a5,a2),f6(a5)))+~P2(f3(f3(a5,a2),f6(a5)),f3(a7,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[841,22])).
% 182.14/182.50 cnf(855,plain,
% 182.14/182.50 (~P1(f6(a5))+~P2(f3(a5,a2),a7)+P3(f3(a7,f6(a5)),f3(f3(a5,a2),f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[848,31])).
% 182.14/182.50 cnf(858,plain,
% 182.14/182.50 (~P3(f3(a2,a5),f3(a5,a2))+P3(f3(a7,f6(a5)),f3(f3(a5,a2),f6(a5)))+~P1(f6(a5))),
% 182.14/182.50 inference(scs_inference,[],[159,855,23])).
% 182.14/182.50 cnf(876,plain,
% 182.14/182.50 (P3(f3(f3(a2,a5),f6(a2)),f3(a7,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,8,11,29])).
% 182.14/182.50 cnf(877,plain,
% 182.14/182.50 (~P2(f3(f3(a2,a5),f6(a2)),x8771)+P2(f3(a7,f6(a2)),x8771)),
% 182.14/182.50 inference(scs_inference,[],[876,23])).
% 182.14/182.50 cnf(882,plain,
% 182.14/182.50 (~P1(f6(a2))+P2(f3(a7,f6(a2)),f3(f3(a5,a2),f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[163,877,31])).
% 182.14/182.50 cnf(891,plain,
% 182.14/182.50 (P2(f3(a7,f6(a2)),f3(f3(a5,a2),f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,11,882])).
% 182.14/182.50 cnf(898,plain,
% 182.14/182.50 (P3(f3(a7,f6(a2)),f3(f3(a5,a2),f6(a2)))+~P2(f3(f3(a5,a2),f6(a2)),f3(a7,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[891,22])).
% 182.14/182.50 cnf(905,plain,
% 182.14/182.50 (~P1(f6(a2))+~P2(f3(a5,a2),a7)+P3(f3(a7,f6(a2)),f3(f3(a5,a2),f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[898,31])).
% 182.14/182.50 cnf(924,plain,
% 182.14/182.50 (P3(f3(f3(a2,a5),f6(a4)),f3(a7,f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[2,8,11,29])).
% 182.14/182.50 cnf(944,plain,
% 182.14/182.50 (P1(f3(f6(a5),f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,11,18])).
% 182.14/182.50 cnf(948,plain,
% 182.14/182.50 (P3(f9(f9(f3(a5,a2),f8(f3(a5,a2))),f6(a2)),f9(a4,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,264,11,30])).
% 182.14/182.50 cnf(949,plain,
% 182.14/182.50 (P2(f3(a1,f6(a5)),f3(a2,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,6,11,31])).
% 182.14/182.50 cnf(950,plain,
% 182.14/182.50 (P2(f6(a5),f3(a2,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[430,949,23])).
% 182.14/182.50 cnf(1057,plain,
% 182.14/182.50 (P2(f3(a1,f6(a4)),f3(a2,f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[2,6,11,31])).
% 182.14/182.50 cnf(1058,plain,
% 182.14/182.50 (~P2(x10581,f3(a1,f6(a4)))+P2(x10581,f3(a2,f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[1057,24])).
% 182.14/182.50 cnf(1065,plain,
% 182.14/182.50 (~P1(f6(a4))+P2(f3(f3(a2,a5),f6(a4)),f3(a2,f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[278,1058,31])).
% 182.14/182.50 cnf(1092,plain,
% 182.14/182.50 (P2(f3(f3(a2,a5),f6(a4)),f3(a2,f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[2,11,1065])).
% 182.14/182.50 cnf(1093,plain,
% 182.14/182.50 (P2(f3(a7,f6(a4)),f3(a2,f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[1092,924,23])).
% 182.14/182.50 cnf(1103,plain,
% 182.14/182.50 (~P2(f3(a5,a2),f3(a7,f6(a4)))+P2(a7,f3(a2,f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[1093,127,24,23])).
% 182.14/182.50 cnf(1115,plain,
% 182.14/182.50 (~P3(x11151,f3(a5,a2))+~P2(x11151,f3(a7,f6(a4)))+P2(a7,f3(a2,f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[1103,23])).
% 182.14/182.50 cnf(1122,plain,
% 182.14/182.50 (~P3(x11221,f3(a5,a2))+~P2(x11221,f3(a7,f6(a4)))+P2(f3(a7,a4),f3(f3(a2,f6(a4)),a4))),
% 182.14/182.50 inference(scs_inference,[],[2,1115,31])).
% 182.14/182.50 cnf(1172,plain,
% 182.14/182.50 (P2(f3(a7,f6(a5)),f3(a5,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,296,11,31])).
% 182.14/182.50 cnf(1173,plain,
% 182.14/182.50 (~P2(x11731,f3(a7,f6(a5)))+P2(x11731,f3(a5,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[1172,24])).
% 182.14/182.50 cnf(1178,plain,
% 182.14/182.50 (~P1(f6(a5))+P2(f3(f3(a2,a5),f6(a5)),f3(a5,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[159,1173,31])).
% 182.14/182.50 cnf(1196,plain,
% 182.14/182.50 (P2(f3(f3(a2,a5),f6(a5)),f3(a5,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,11,1178])).
% 182.14/182.50 cnf(1197,plain,
% 182.14/182.50 (~P2(x11971,f3(f3(a2,a5),f6(a5)))+P2(x11971,f3(a5,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[1196,24])).
% 182.14/182.50 cnf(1219,plain,
% 182.14/182.50 (P2(f3(a1,f6(a2)),f3(a2,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,6,11,31])).
% 182.14/182.50 cnf(1220,plain,
% 182.14/182.50 (P2(f6(a2),f3(a2,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[648,1219,23])).
% 182.14/182.50 cnf(1222,plain,
% 182.14/182.50 (~P2(x12221,f3(a1,f6(a2)))+P2(x12221,f3(a2,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[648,1219,23,24])).
% 182.14/182.50 cnf(1227,plain,
% 182.14/182.50 (~P1(f6(a2))+P2(f3(f3(a2,a5),f6(a2)),f3(a2,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[278,1222,31])).
% 182.14/182.50 cnf(1228,plain,
% 182.14/182.50 (~P2(x12281,f6(a2))+P2(x12281,f3(a2,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[1220,24])).
% 182.14/182.50 cnf(1263,plain,
% 182.14/182.50 (P2(f3(f3(a2,a5),f6(a2)),f3(a2,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,11,1227])).
% 182.14/182.50 cnf(1264,plain,
% 182.14/182.50 (P2(f3(a7,f6(a2)),f3(a2,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[1263,876,23])).
% 182.14/182.50 cnf(1322,plain,
% 182.14/182.50 (P2(f3(a1,f6(a5)),f3(a5,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,7,11,31])).
% 182.14/182.50 cnf(1393,plain,
% 182.14/182.50 (P2(f3(a7,f6(a5)),f3(f3(a2,a5),f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,112,11,31])).
% 182.14/182.50 cnf(1443,plain,
% 182.14/182.50 (P2(f3(f6(f3(a4,a4)),f6(a2)),f3(f6(f3(a4,a4)),f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,428,11,31])).
% 182.14/182.50 cnf(1444,plain,
% 182.14/182.50 (P3(f3(f3(a1,f6(a5)),f6(a5)),f3(f6(a5),f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,430,11,29])).
% 182.14/182.50 cnf(1445,plain,
% 182.14/182.50 (~P2(f3(f3(a1,f6(a5)),f6(a5)),x14451)+P2(f3(f6(a5),f6(a5)),x14451)),
% 182.14/182.50 inference(scs_inference,[],[1444,23])).
% 182.14/182.50 cnf(1482,plain,
% 182.14/182.50 (P2(f3(f6(f9(a5,a5)),f6(a4)),f3(f6(f9(a5,a5)),f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[2,529,11,31])).
% 182.14/182.50 cnf(1489,plain,
% 182.14/182.50 (P3(f3(f3(f6(a5),f6(f6(a5))),f6(a5)),f3(a1,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,563,11,29])).
% 182.14/182.50 cnf(1498,plain,
% 182.14/182.50 (P3(f3(f6(a5),f6(a2)),f3(f9(a4,f3(a1,f6(a5))),f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,596,11,29])).
% 182.14/182.50 cnf(1525,plain,
% 182.14/182.50 (P2(f3(f9(f6(a4),f6(a4)),f6(a2)),f3(f9(f6(a4),f6(a4)),f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,807,11,31])).
% 182.14/182.50 cnf(1531,plain,
% 182.14/182.50 (P2(f3(f9(f6(a2),f6(a2)),f6(a5)),f3(f9(f6(a2),f6(a2)),f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,820,11,31])).
% 182.14/182.50 cnf(1544,plain,
% 182.14/182.50 (P2(f3(f3(a1,f6(a5)),f6(a5)),f3(f3(a2,f6(a5)),f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,949,11,31])).
% 182.14/182.50 cnf(1568,plain,
% 182.14/182.50 (P2(f3(f3(a1,f6(a5)),f6(a5)),f3(f3(a5,f6(a5)),f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[4,1322,11,31])).
% 182.14/182.50 cnf(1569,plain,
% 182.14/182.50 (P2(f6(a5),f3(a5,f6(a5)))),
% 182.14/182.50 inference(scs_inference,[],[1322,430,23])).
% 182.14/182.50 cnf(1594,plain,
% 182.14/182.50 (P2(f3(f6(a5),f6(a2)),f3(f3(a5,f6(a5)),f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,1569,11,31])).
% 182.14/182.50 cnf(1612,plain,
% 182.14/182.50 (P2(f3(a1,f6(a2)),f3(a1,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[3,37,11,31])).
% 182.14/182.50 cnf(1618,plain,
% 182.14/182.50 (P2(f6(a2),f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[3,11,15])).
% 182.14/182.50 cnf(1621,plain,
% 182.14/182.50 (P2(f9(a4,f3(a1,f6(a2))),f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[1618,781,724])).
% 182.14/182.50 cnf(1641,plain,
% 182.14/182.50 (~P2(f3(a5,a2),f9(a4,f3(a1,f6(a2))))+P2(f3(a5,a2),f3(a2,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[1621,127,24,23,1228])).
% 182.14/182.50 cnf(1686,plain,
% 182.14/182.50 (~P3(x16861,f3(a5,a2))+~P2(x16861,f9(a4,f3(a1,f6(a2))))+P2(f3(a5,a2),f3(a2,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[1641,23])).
% 182.14/182.50 cnf(1735,plain,
% 182.14/182.50 (P2(f6(a4),f6(a4))),
% 182.14/182.50 inference(scs_inference,[],[2,11,15])).
% 182.14/182.50 cnf(1773,plain,
% 182.14/182.50 (~P1(f3(a5,a2))+P2(f3(a7,a4),f3(f3(a2,f6(a4)),a4))+~P2(f3(a5,a2),f3(a7,f6(a4)))),
% 182.14/182.50 inference(scs_inference,[],[12,1122])).
% 182.14/182.50 cnf(1774,plain,
% 182.14/182.50 (~P2(f3(a5,a2),f3(a7,f6(a4)))+P2(f3(a7,a4),f3(f3(a2,f6(a4)),a4))),
% 182.14/182.50 inference(scs_inference,[],[3,4,1773,18])).
% 182.14/182.50 cnf(1775,plain,
% 182.14/182.50 (~P2(x17751,f3(a7,f6(a4)))+~P2(f3(a5,a2),x17751)+P2(f3(a7,a4),f3(f3(a2,f6(a4)),a4))),
% 182.14/182.50 inference(scs_inference,[],[1774,24])).
% 182.14/182.50 cnf(1777,plain,
% 182.14/182.50 (P3(a7,f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[184,14,172])).
% 182.14/182.50 cnf(1778,plain,
% 182.14/182.50 (P2(f3(a5,a2),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[1777,203])).
% 182.14/182.50 cnf(1784,plain,
% 182.14/182.50 (~P3(f3(a2,a5),f9(a2,a1))+P2(f9(a2,a1),a2)),
% 182.14/182.50 inference(scs_inference,[],[1777,385])).
% 182.14/182.50 cnf(1785,plain,
% 182.14/182.50 (~P3(f3(f6(a2),f6(f6(a2))),a7)),
% 182.14/182.50 inference(scs_inference,[],[1777,208,21])).
% 182.14/182.50 cnf(1787,plain,
% 182.14/182.50 (~P3(f3(f6(a2),f6(f6(a2))),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[1777,208,21,57])).
% 182.14/182.50 cnf(1797,plain,
% 182.14/182.50 (~P3(a1,a7)),
% 182.14/182.50 inference(scs_inference,[],[1777,196,1787,14,21])).
% 182.14/182.50 cnf(1799,plain,
% 182.14/182.50 (P3(f3(a5,a2),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[1777,1778,196,1787,14,21,22])).
% 182.14/182.50 cnf(1801,plain,
% 182.14/182.50 (P3(f3(a2,a5),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[1777,1778,196,1787,14,21,22,195])).
% 182.14/182.50 cnf(1803,plain,
% 182.14/182.50 (~P3(a1,f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[1777,1778,196,1787,14,21,22,195,57])).
% 182.14/182.50 cnf(1805,plain,
% 182.14/182.50 (P3(f3(a7,f6(a5)),f3(f3(a5,a2),f6(a5)))+~P1(f6(a5))),
% 182.14/182.50 inference(scs_inference,[],[1801,858])).
% 182.14/182.50 cnf(1811,plain,
% 182.14/182.50 (~P3(a7,a1)),
% 182.14/182.50 inference(scs_inference,[],[1797,14])).
% 182.14/182.50 cnf(1814,plain,
% 182.14/182.50 (~P3(f3(a2,a5),f9(a2,a1))+P2(f3(f9(a2,a1),a5),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[4,1784,31])).
% 182.14/182.50 cnf(1822,plain,
% 182.14/182.50 (~P3(f9(a2,a1),f3(a5,a2))+P2(f3(f9(a2,a1),a5),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[1814,195])).
% 182.14/182.50 cnf(1826,plain,
% 182.14/182.50 (~P3(f3(a5,a2),f9(a2,a1))+P2(f3(f9(a2,a1),a5),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[1822,14])).
% 182.14/182.50 cnf(1827,plain,
% 182.14/182.50 (~P2(f3(a5,a2),f9(a2,a1))+~P2(f9(a2,a1),f3(a5,a2))+P2(f3(f9(a2,a1),a5),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[1826,22])).
% 182.14/182.50 cnf(1848,plain,
% 182.14/182.50 (P3(a4,f3(a1,a4))),
% 182.14/182.50 inference(scs_inference,[],[2,14,16])).
% 182.14/182.50 cnf(1849,plain,
% 182.14/182.50 (P2(f3(a1,a4),a4)),
% 182.14/182.50 inference(scs_inference,[],[46,1848,23])).
% 182.14/182.50 cnf(1851,plain,
% 182.14/182.50 (~P2(x18511,f3(a1,a4))+P2(x18511,a4)),
% 182.14/182.50 inference(scs_inference,[],[46,1848,23,24])).
% 182.14/182.50 cnf(1858,plain,
% 182.14/182.50 (P2(f3(f3(a2,a5),a4),a4)),
% 182.14/182.50 inference(scs_inference,[],[278,2,1851,31])).
% 182.14/182.50 cnf(1859,plain,
% 182.14/182.50 (~P2(x18591,f3(f3(a2,a5),a4))+P2(x18591,a4)),
% 182.14/182.50 inference(scs_inference,[],[1858,24])).
% 182.14/182.50 cnf(1875,plain,
% 182.14/182.50 (P2(f3(a7,a4),a4)),
% 182.14/182.50 inference(scs_inference,[],[112,2,1859,31])).
% 182.14/182.50 cnf(1901,plain,
% 182.14/182.50 (P2(f6(a2),f3(a1,f6(a2)))),
% 182.14/182.50 inference(scs_inference,[],[1612,648,23])).
% 182.14/182.50 cnf(1927,plain,
% 182.14/182.50 (P2(f3(a1,f3(a1,f6(a4))),f6(a4))),
% 182.14/182.50 inference(scs_inference,[],[1735,573,23])).
% 182.14/182.50 cnf(1975,plain,
% 182.14/182.50 (~P3(a7,f3(f6(a4),f6(f6(a4))))),
% 182.14/182.50 inference(scs_inference,[],[1811,466,21])).
% 182.14/182.50 cnf(2008,plain,
% 182.14/182.50 (P2(f3(a5,a2),a7)),
% 182.14/182.50 inference(scs_inference,[],[63,1777,23])).
% 182.14/182.50 cnf(2010,plain,
% 182.14/182.50 (~P2(a1,f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[63,10,1777,23,24])).
% 182.14/182.50 cnf(2013,plain,
% 182.14/182.50 (P3(f3(a7,f6(a2)),f3(f3(a5,a2),f6(a2)))+~P1(f6(a2))),
% 182.14/182.50 inference(scs_inference,[],[2008,905])).
% 182.14/182.50 cnf(2030,plain,
% 182.14/182.50 (P2(f3(a5,a2),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[112,1777,23])).
% 182.14/182.50 cnf(2034,plain,
% 182.14/182.50 (P2(f3(a5,a2),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[2030,182])).
% 182.14/182.50 cnf(2051,plain,
% 182.14/182.50 (P3(f9(f3(a5,a2),f8(f3(a5,a2))),f3(a1,a4))),
% 182.14/182.50 inference(scs_inference,[],[264,1848,21])).
% 182.14/182.50 cnf(2067,plain,
% 182.14/182.50 (P2(f3(a5,a2),a1)),
% 182.14/182.50 inference(scs_inference,[],[276,1777,23])).
% 182.14/182.50 cnf(2072,plain,
% 182.14/182.50 (P2(f3(a5,a2),a2)),
% 182.14/182.50 inference(scs_inference,[],[281,1801,23])).
% 182.14/182.50 cnf(2082,plain,
% 182.14/182.50 (P3(f3(a5,a2),a5)+~P2(a5,f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[286,1801,23,22])).
% 182.14/182.50 cnf(2094,plain,
% 182.14/182.50 (P3(f3(a5,a2),f9(a2,a1))+~P2(f9(a2,a1),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[331,1801,23,1827,22])).
% 182.14/182.50 cnf(2098,plain,
% 182.14/182.50 (~P2(a5,f3(a2,a5))+P3(f3(a5,a2),a5)),
% 182.14/182.50 inference(scs_inference,[],[163,2082,24])).
% 182.14/182.50 cnf(2109,plain,
% 182.14/182.50 (~P3(f3(a2,a5),f9(a2,a1))+P3(f3(a5,a2),f9(a2,a1))),
% 182.14/182.50 inference(scs_inference,[],[163,2094,23])).
% 182.14/182.50 cnf(2137,plain,
% 182.14/182.50 (P3(a5,f3(a1,a5))),
% 182.14/182.50 inference(scs_inference,[],[4,14,16])).
% 182.14/182.50 cnf(2138,plain,
% 182.14/182.50 (P2(f3(a1,a5),a5)),
% 182.14/182.50 inference(scs_inference,[],[67,2137,23])).
% 182.14/182.50 cnf(2140,plain,
% 182.14/182.50 (~P2(x21401,f3(a1,a5))+P2(x21401,a5)),
% 182.14/182.50 inference(scs_inference,[],[67,2137,23,24])).
% 182.14/182.50 cnf(2147,plain,
% 182.14/182.50 (P2(f3(f3(a2,a5),a5),a5)),
% 182.14/182.50 inference(scs_inference,[],[278,4,2140,31])).
% 182.14/182.50 cnf(2148,plain,
% 182.14/182.50 (~P2(x21481,f3(f3(a2,a5),a5))+P2(x21481,a5)),
% 182.14/182.50 inference(scs_inference,[],[2147,24])).
% 182.14/182.50 cnf(2153,plain,
% 182.14/182.50 (P2(f3(a7,a5),a5)),
% 182.14/182.50 inference(scs_inference,[],[112,4,2148,31])).
% 182.14/182.50 cnf(2180,plain,
% 182.14/182.50 (P3(f3(a1,a7),a7)),
% 182.14/182.50 inference(scs_inference,[],[528,5,11,16])).
% 182.14/182.50 cnf(2182,plain,
% 182.14/182.50 (P3(f9(a4,a7),a7)),
% 182.14/182.50 inference(scs_inference,[],[528,5,11,16,17])).
% 182.14/182.50 cnf(2184,plain,
% 182.14/182.50 (P3(f3(a7,f6(a7)),a1)),
% 182.14/182.50 inference(scs_inference,[],[528,5,11,16,17,20])).
% 182.14/182.50 cnf(2186,plain,
% 182.14/182.50 (P3(f3(a1,a5),a5)),
% 182.14/182.50 inference(scs_inference,[],[2137,528,5,11,16,17,20,14])).
% 182.14/182.50 cnf(2188,plain,
% 182.14/182.50 (P1(f9(a7,a7))),
% 182.14/182.50 inference(scs_inference,[],[2137,528,5,11,16,17,20,14,19])).
% 182.14/182.50 cnf(2190,plain,
% 182.14/182.50 (P1(f8(a7))),
% 182.14/182.50 inference(scs_inference,[],[2137,528,1811,5,11,16,17,20,14,19,13])).
% 182.14/182.50 cnf(2192,plain,
% 182.14/182.50 (P3(f3(a7,a7),f3(a7,a7))),
% 182.14/182.50 inference(scs_inference,[],[2137,528,1811,5,11,16,17,20,14,19,13,27])).
% 182.14/182.50 cnf(2194,plain,
% 182.14/182.50 (P3(f9(a7,a7),f9(a7,a7))),
% 182.14/182.50 inference(scs_inference,[],[2137,528,1811,5,11,16,17,20,14,19,13,27,28])).
% 182.14/182.50 cnf(2196,plain,
% 182.14/182.50 (P3(f9(a7,f8(a7)),a4)),
% 182.14/182.50 inference(scs_inference,[],[2137,528,1811,5,11,16,17,20,14,19,13,27,28,25])).
% 182.14/182.50 cnf(2198,plain,
% 182.14/182.50 (P2(a1,f9(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[7,2137,528,1811,5,11,16,17,20,14,19,13,27,28,25,26])).
% 182.14/182.50 cnf(2200,plain,
% 182.14/182.50 (P1(f3(a7,a7))),
% 182.14/182.50 inference(scs_inference,[],[7,2137,528,1811,5,11,16,17,20,14,19,13,27,28,25,26,18])).
% 182.14/182.50 cnf(2202,plain,
% 182.14/182.50 (P2(f3(a1,a7),f3(a5,a7))),
% 182.14/182.50 inference(scs_inference,[],[7,2137,528,1811,5,11,16,17,20,14,19,13,27,28,25,26,18,31])).
% 182.14/182.50 cnf(2204,plain,
% 182.14/182.50 (~P2(a5,f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[7,2010,2137,528,1811,5,11,16,17,20,14,19,13,27,28,25,26,18,31,24])).
% 182.14/182.50 cnf(2206,plain,
% 182.14/182.50 (P2(a7,f3(a5,a7))),
% 182.14/182.50 inference(scs_inference,[],[7,2010,2137,528,1811,5,11,16,17,20,14,19,13,27,28,25,26,18,31,24,23])).
% 182.14/182.50 cnf(2210,plain,
% 182.14/182.50 (P3(f3(a7,f3(a7,a7)),f3(f3(a7,a7),a7))),
% 182.14/182.50 inference(scs_inference,[],[7,2010,566,2137,528,1848,1811,5,11,16,17,20,14,19,13,27,28,25,26,18,31,24,23,21,32])).
% 182.14/182.50 cnf(2212,plain,
% 182.14/182.50 (P3(f9(a7,f9(a7,a7)),f9(f9(a7,a7),a7))),
% 182.14/182.50 inference(scs_inference,[],[7,2010,566,2137,528,1848,1811,5,11,16,17,20,14,19,13,27,28,25,26,18,31,24,23,21,32,33])).
% 182.14/182.50 cnf(2214,plain,
% 182.14/182.50 (P3(f3(f9(a7,a7),f9(a7,a7)),f9(f3(a7,a7),a7))),
% 182.14/182.50 inference(scs_inference,[],[7,2010,566,2137,528,1848,1811,5,11,16,17,20,14,19,13,27,28,25,26,18,31,24,23,21,32,33,34])).
% 182.14/182.50 cnf(2216,plain,
% 182.14/182.50 (P3(f8(a7),f8(a7))),
% 182.14/182.50 inference(scs_inference,[],[7,2010,566,2137,528,1848,1811,5,11,16,17,20,14,19,13,27,28,25,26,18,31,24,23,21,32,33,34,12])).
% 182.14/182.50 cnf(2223,plain,
% 182.14/182.50 (~P2(a5,f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[2204,306])).
% 182.14/182.50 cnf(2225,plain,
% 182.14/182.50 (P3(f9(a4,f3(a7,a7)),f3(a7,a7))),
% 182.14/182.50 inference(scs_inference,[],[2200,17])).
% 182.14/182.50 cnf(2229,plain,
% 182.14/182.50 (P3(f3(a1,f3(a7,a7)),f3(a7,a7))),
% 182.14/182.50 inference(scs_inference,[],[2200,17,20,16])).
% 182.14/182.50 cnf(2231,plain,
% 182.14/182.50 (P1(f6(f9(a7,a7)))),
% 182.14/182.50 inference(scs_inference,[],[2200,2188,17,20,16,11])).
% 182.14/182.50 cnf(2233,plain,
% 182.14/182.50 (P3(a7,f3(a1,a7))),
% 182.14/182.50 inference(scs_inference,[],[2200,2188,2180,17,20,16,11,14])).
% 182.14/182.50 cnf(2237,plain,
% 182.14/182.50 (P1(f9(f3(a7,a7),f3(a7,a7)))),
% 182.14/182.50 inference(scs_inference,[],[2200,2192,2188,2180,17,20,16,11,14,30,19])).
% 182.14/182.50 cnf(2239,plain,
% 182.14/182.50 (P1(f8(a4))),
% 182.14/182.50 inference(scs_inference,[],[2200,2192,2188,2180,35,2,17,20,16,11,14,30,19,13])).
% 182.14/182.50 cnf(2243,plain,
% 182.14/182.50 (P2(a1,f9(f9(a5,a5),f9(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[2200,2192,2198,2188,2180,35,2,17,20,16,11,14,30,19,13,28,26])).
% 182.14/182.50 cnf(2245,plain,
% 182.14/182.50 (P3(f9(a4,f8(a4)),a4)),
% 182.14/182.50 inference(scs_inference,[],[2200,2192,2198,2188,2180,35,2,17,20,16,11,14,30,19,13,28,26,25])).
% 182.14/182.50 cnf(2251,plain,
% 182.14/182.50 (P1(f3(f3(a7,a7),f3(a7,a7)))),
% 182.14/182.50 inference(scs_inference,[],[2200,2192,2198,2188,2180,35,2,17,20,16,11,14,30,19,13,28,26,25,27,29,18])).
% 182.14/182.50 cnf(2253,plain,
% 182.14/182.50 (P2(f3(a1,f3(a7,a7)),f3(a5,f3(a7,a7)))),
% 182.14/182.50 inference(scs_inference,[],[7,2200,2192,2198,2188,2180,35,2,17,20,16,11,14,30,19,13,28,26,25,27,29,18,31])).
% 182.14/182.50 cnf(2255,plain,
% 182.14/182.50 (~P2(f9(a5,a5),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[7,2200,2192,2198,2188,2180,2010,35,2,17,20,16,11,14,30,19,13,28,26,25,27,29,18,31,24])).
% 182.14/182.50 cnf(2257,plain,
% 182.14/182.50 (~P3(f3(a5,a2),a5)),
% 182.14/182.50 inference(scs_inference,[],[7,2204,2200,2192,2198,2188,2180,2034,2010,35,2,17,20,16,11,14,30,19,13,28,26,25,27,29,18,31,24,23])).
% 182.14/182.50 cnf(2259,plain,
% 182.14/182.50 (P3(f9(a7,f8(a7)),f3(a1,a4))),
% 182.14/182.50 inference(scs_inference,[],[7,2204,2200,2192,2198,2188,2180,2196,2034,2010,1848,35,2,17,20,16,11,14,30,19,13,28,26,25,27,29,18,31,24,23,21])).
% 182.14/182.50 cnf(2261,plain,
% 182.14/182.50 (P3(f9(a1,f9(a1,a1)),f9(f9(a1,a1),a1))),
% 182.14/182.50 inference(scs_inference,[],[7,2204,2200,2192,2198,2188,2180,2196,2034,2010,1848,35,1,2,17,20,16,11,14,30,19,13,28,26,25,27,29,18,31,24,23,21,33])).
% 182.14/182.50 cnf(2263,plain,
% 182.14/182.50 (P3(f3(a1,f3(a1,a1)),f3(f3(a1,a1),a1))),
% 182.14/182.50 inference(scs_inference,[],[7,2204,2200,2192,2198,2188,2180,2196,2034,2010,1848,35,1,2,17,20,16,11,14,30,19,13,28,26,25,27,29,18,31,24,23,21,33,32])).
% 182.14/182.50 cnf(2265,plain,
% 182.14/182.50 (P3(f3(f9(a1,a1),f9(a1,a1)),f9(f3(a1,a1),a1))),
% 182.14/182.50 inference(scs_inference,[],[7,2204,2200,2192,2198,2188,2180,2196,2034,2010,1848,35,1,2,17,20,16,11,14,30,19,13,28,26,25,27,29,18,31,24,23,21,33,32,34])).
% 182.14/182.50 cnf(2273,plain,
% 182.14/182.50 (~P2(a5,f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[2257,2098])).
% 182.14/182.50 cnf(2275,plain,
% 182.14/182.50 (P3(f3(a1,f8(a7)),f8(a7))),
% 182.14/182.50 inference(scs_inference,[],[2190,16])).
% 182.14/182.50 cnf(2279,plain,
% 182.14/182.50 (P3(f9(a4,f8(a7)),f8(a7))),
% 182.14/182.50 inference(scs_inference,[],[2190,16,20,17])).
% 182.14/182.50 cnf(2281,plain,
% 182.14/182.50 (P1(f6(f8(a7)))),
% 182.14/182.50 inference(scs_inference,[],[2190,16,20,17,11])).
% 182.14/182.50 cnf(2285,plain,
% 182.14/182.50 (P3(a7,f9(a4,a7))),
% 182.14/182.50 inference(scs_inference,[],[2182,2190,16,20,17,11,12,14])).
% 182.14/182.50 cnf(2289,plain,
% 182.14/182.50 (P1(f9(f8(a7),f8(a7)))),
% 182.14/182.50 inference(scs_inference,[],[2194,2182,2190,16,20,17,11,12,14,30,19])).
% 182.14/182.50 cnf(2295,plain,
% 182.14/182.50 (P2(a1,f9(f9(a2,a1),f9(a2,a1)))),
% 182.14/182.50 inference(scs_inference,[],[2194,2182,2190,330,16,20,17,11,12,14,30,19,28,27,26])).
% 182.14/182.50 cnf(2299,plain,
% 182.14/182.50 (P1(f3(f8(a7),f8(a7)))),
% 182.14/182.50 inference(scs_inference,[],[2194,2182,2190,330,16,20,17,11,12,14,30,19,28,27,26,29,18])).
% 182.14/182.50 cnf(2301,plain,
% 182.14/182.50 (P2(f3(a1,f8(a7)),f3(a5,f8(a7)))),
% 182.14/182.50 inference(scs_inference,[],[7,2194,2182,2190,330,16,20,17,11,12,14,30,19,28,27,26,29,18,31])).
% 182.14/182.50 cnf(2303,plain,
% 182.14/182.50 (~P2(f9(f9(a5,a5),f9(a5,a5)),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[7,2194,2182,2190,2243,2010,330,16,20,17,11,12,14,30,19,28,27,26,29,18,31,24])).
% 182.14/182.50 cnf(2307,plain,
% 182.14/182.50 (P3(f9(a4,a7),f3(a1,a7))),
% 182.14/182.50 inference(scs_inference,[],[7,2194,2182,2190,2233,2229,2243,2253,2010,330,16,20,17,11,12,14,30,19,28,27,26,29,18,31,24,23,21])).
% 182.14/182.50 cnf(2309,plain,
% 182.14/182.50 (P3(f9(a5,f9(a5,a5)),f9(f9(a5,a5),a5))),
% 182.14/182.50 inference(scs_inference,[],[7,2194,2182,2190,2233,2229,2243,2253,2010,330,4,16,20,17,11,12,14,30,19,28,27,26,29,18,31,24,23,21,33])).
% 182.14/182.50 cnf(2311,plain,
% 182.14/182.50 (P3(f3(a5,f3(a5,a5)),f3(f3(a5,a5),a5))),
% 182.14/182.50 inference(scs_inference,[],[7,2194,2182,2190,2233,2229,2243,2253,2010,330,4,16,20,17,11,12,14,30,19,28,27,26,29,18,31,24,23,21,33,32])).
% 182.14/182.50 cnf(2313,plain,
% 182.14/182.50 (P3(f3(f9(a5,a5),f9(a5,a5)),f9(f3(a5,a5),a5))),
% 182.14/182.50 inference(scs_inference,[],[7,2194,2182,2190,2233,2229,2243,2253,2010,330,4,16,20,17,11,12,14,30,19,28,27,26,29,18,31,24,23,21,33,32,34])).
% 182.14/182.50 cnf(2320,plain,
% 182.14/182.50 (P3(f9(a4,f8(a4)),f8(a4))),
% 182.14/182.50 inference(scs_inference,[],[2239,17])).
% 182.14/182.50 cnf(2326,plain,
% 182.14/182.50 (P3(f3(a1,f8(a4)),f8(a4))),
% 182.14/182.50 inference(scs_inference,[],[2239,2231,17,11,20,16])).
% 182.14/182.50 cnf(2328,plain,
% 182.14/182.50 (P3(f3(a1,a7),f9(a4,a7))),
% 182.14/182.50 inference(scs_inference,[],[2307,2239,2231,17,11,20,16,14])).
% 182.14/182.50 cnf(2334,plain,
% 182.14/182.50 (P1(f9(f8(a4),f8(a4)))),
% 182.14/182.50 inference(scs_inference,[],[2216,2307,2239,2231,17,11,20,16,14,30,28,19])).
% 182.14/182.50 cnf(2336,plain,
% 182.14/182.50 (P2(a1,f9(a1,a1))),
% 182.14/182.50 inference(scs_inference,[],[2216,2307,2239,2231,37,17,11,20,16,14,30,28,19,26])).
% 182.14/182.50 cnf(2342,plain,
% 182.14/182.50 (P1(f3(f8(a4),f8(a4)))),
% 182.14/182.50 inference(scs_inference,[],[2216,2307,2239,2231,37,17,11,20,16,14,30,28,19,26,27,29,18])).
% 182.14/182.50 cnf(2344,plain,
% 182.14/182.50 (P2(f3(a1,f8(a4)),f3(a5,f8(a4)))),
% 182.14/182.50 inference(scs_inference,[],[7,2216,2307,2239,2231,37,17,11,20,16,14,30,28,19,26,27,29,18,31])).
% 182.14/182.50 cnf(2352,plain,
% 182.14/182.50 (P3(f9(a2,f9(a2,a2)),f9(f9(a2,a2),a2))),
% 182.14/182.50 inference(scs_inference,[],[7,2216,2307,2206,2239,2285,2231,2295,1975,255,37,3,17,11,20,16,14,30,28,19,26,27,29,18,31,24,23,21,33])).
% 182.14/182.50 cnf(2365,plain,
% 182.14/182.50 (P3(f3(a1,f9(a7,a7)),f9(a7,a7))),
% 182.14/182.50 inference(scs_inference,[],[2188,20,16])).
% 182.14/182.50 cnf(2367,plain,
% 182.14/182.50 (P3(f9(a4,f9(a7,a7)),f9(a7,a7))),
% 182.14/182.50 inference(scs_inference,[],[2188,20,16,17])).
% 182.14/182.50 cnf(2373,plain,
% 182.14/182.50 (P3(f9(a1,a1),f9(a1,a1))),
% 182.14/182.50 inference(scs_inference,[],[2225,2342,2188,1,20,16,17,11,14,28])).
% 182.14/182.50 cnf(2375,plain,
% 182.14/182.50 (P2(a1,f9(f9(a1,a1),f9(a1,a1)))),
% 182.14/182.50 inference(scs_inference,[],[2336,2225,2342,2188,1,20,16,17,11,14,28,26])).
% 182.14/182.50 cnf(2377,plain,
% 182.14/182.50 (P1(f9(f9(a7,a7),f9(a7,a7)))),
% 182.14/182.50 inference(scs_inference,[],[2336,2225,2342,2188,1,20,16,17,11,14,28,26,19])).
% 182.14/182.50 cnf(2381,plain,
% 182.14/182.50 (P1(f3(f9(a7,a7),f9(a7,a7)))),
% 182.14/182.50 inference(scs_inference,[],[2336,2225,2342,2188,1,20,16,17,11,14,28,26,19,27,18])).
% 182.14/182.50 cnf(2383,plain,
% 182.14/182.50 (P2(f3(a1,f9(a7,a7)),f3(a5,f9(a7,a7)))),
% 182.14/182.50 inference(scs_inference,[],[7,2336,2225,2342,2188,1,20,16,17,11,14,28,26,19,27,18,31])).
% 182.14/182.50 cnf(2385,plain,
% 182.14/182.50 (~P2(f9(a1,a1),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[7,2336,2225,2342,2010,2188,1,20,16,17,11,14,28,26,19,27,18,31,24])).
% 182.14/182.50 cnf(2387,plain,
% 182.14/182.50 (P2(f8(a7),f3(a5,f8(a7)))),
% 182.14/182.50 inference(scs_inference,[],[7,2336,2225,2275,2342,2301,2010,2188,1,20,16,17,11,14,28,26,19,27,18,31,24,23])).
% 182.14/182.50 cnf(2389,plain,
% 182.14/182.50 (P3(f3(a1,a7),f3(a1,a7))),
% 182.14/182.50 inference(scs_inference,[],[7,2328,2336,2225,2275,2342,2301,2307,2010,2188,1,20,16,17,11,14,28,26,19,27,18,31,24,23,21])).
% 182.14/182.50 cnf(2391,plain,
% 182.14/182.50 (P3(f9(a4,f9(a4,a4)),f9(f9(a4,a4),a4))),
% 182.14/182.50 inference(scs_inference,[],[7,2328,2336,2225,2275,2342,2301,2307,2010,2188,1,2,20,16,17,11,14,28,26,19,27,18,31,24,23,21,33])).
% 182.14/182.50 cnf(2393,plain,
% 182.14/182.50 (P3(f3(a4,f3(a4,a4)),f3(f3(a4,a4),a4))),
% 182.14/182.50 inference(scs_inference,[],[7,2328,2336,2225,2275,2342,2301,2307,2010,2188,1,2,20,16,17,11,14,28,26,19,27,18,31,24,23,21,33,32])).
% 182.14/182.50 cnf(2402,plain,
% 182.14/182.50 (P3(f9(a4,a1),a1)),
% 182.14/182.50 inference(scs_inference,[],[1,17])).
% 182.14/182.50 cnf(2406,plain,
% 182.14/182.50 (P3(f3(a1,a1),a1)),
% 182.14/182.50 inference(scs_inference,[],[2377,1,17,11,16])).
% 182.14/182.50 cnf(2408,plain,
% 182.14/182.50 (P3(f3(a1,f6(a1)),a1)),
% 182.14/182.50 inference(scs_inference,[],[2377,1,17,11,16,20])).
% 182.14/182.50 cnf(2410,plain,
% 182.14/182.50 (P3(f9(a7,a7),f3(a1,f9(a7,a7)))),
% 182.14/182.50 inference(scs_inference,[],[2365,2377,1,17,11,16,20,14])).
% 182.14/182.50 cnf(2412,plain,
% 182.14/182.50 (P3(f9(a2,a2),f9(a2,a2))),
% 182.14/182.50 inference(scs_inference,[],[2365,2377,1,3,17,11,16,20,14,28])).
% 182.14/182.50 cnf(2414,plain,
% 182.14/182.50 (P2(a1,f9(a2,a2))),
% 182.14/182.50 inference(scs_inference,[],[2365,2377,1,6,3,17,11,16,20,14,28,26])).
% 182.14/182.50 cnf(2416,plain,
% 182.14/182.50 (P1(f9(a1,a1))),
% 182.14/182.50 inference(scs_inference,[],[2365,2377,1,6,3,17,11,16,20,14,28,26,19])).
% 182.14/182.50 cnf(2418,plain,
% 182.14/182.50 (P1(f3(a1,a1))),
% 182.14/182.50 inference(scs_inference,[],[2365,2377,1,6,3,17,11,16,20,14,28,26,19,18])).
% 182.14/182.50 cnf(2420,plain,
% 182.14/182.50 (P2(f3(a1,a1),f3(a5,a1))),
% 182.14/182.50 inference(scs_inference,[],[7,2365,2377,1,6,3,17,11,16,20,14,28,26,19,18,31])).
% 182.14/182.50 cnf(2435,plain,
% 182.14/182.50 (P3(f3(a1,f9(a1,a1)),f9(a1,a1))),
% 182.14/182.50 inference(scs_inference,[],[2416,16])).
% 182.14/182.50 cnf(2439,plain,
% 182.14/182.50 (P1(f6(f9(a1,a1)))),
% 182.14/182.50 inference(scs_inference,[],[2416,16,20,11])).
% 182.14/182.50 cnf(2441,plain,
% 182.14/182.50 (P3(f9(a4,f9(a1,a1)),f9(a1,a1))),
% 182.14/182.50 inference(scs_inference,[],[2416,16,20,11,17])).
% 182.14/182.50 cnf(2443,plain,
% 182.14/182.50 (P3(a1,f3(a1,a1))),
% 182.14/182.50 inference(scs_inference,[],[2416,2406,16,20,11,17,14])).
% 182.14/182.50 cnf(2449,plain,
% 182.14/182.50 (P2(a1,f9(f9(a2,a2),f9(a2,a2)))),
% 182.14/182.50 inference(scs_inference,[],[2412,2416,2414,2406,16,20,11,17,14,30,28,26])).
% 182.14/182.50 cnf(2453,plain,
% 182.14/182.50 (P1(f9(f9(a1,a1),f9(a1,a1)))),
% 182.14/182.50 inference(scs_inference,[],[2412,2416,2418,2414,2406,16,20,11,17,14,30,28,26,27,19])).
% 182.14/182.50 cnf(2457,plain,
% 182.14/182.50 (P1(f3(f9(a1,a1),f9(a1,a1)))),
% 182.14/182.50 inference(scs_inference,[],[2412,2416,2418,2414,2406,16,20,11,17,14,30,28,26,27,19,29,18])).
% 182.14/182.50 cnf(2459,plain,
% 182.14/182.50 (P2(f3(a1,f9(a1,a1)),f3(a5,f9(a1,a1)))),
% 182.14/182.50 inference(scs_inference,[],[7,2412,2416,2418,2414,2406,16,20,11,17,14,30,28,26,27,19,29,18,31])).
% 182.14/182.50 cnf(2461,plain,
% 182.14/182.50 (~P2(f9(a2,a2),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[7,2412,2416,2418,2414,2406,2010,16,20,11,17,14,30,28,26,27,19,29,18,31,24])).
% 182.14/182.50 cnf(2463,plain,
% 182.14/182.50 (P2(a1,f3(a5,a1))),
% 182.14/182.50 inference(scs_inference,[],[7,2412,2416,2418,2420,2414,2406,2010,16,20,11,17,14,30,28,26,27,19,29,18,31,24,23])).
% 182.14/182.50 cnf(2465,plain,
% 182.14/182.50 (P3(f9(a4,f9(a7,a7)),f3(a1,f9(a7,a7)))),
% 182.14/182.50 inference(scs_inference,[],[7,2412,2416,2418,2420,2414,2406,2367,2410,2010,16,20,11,17,14,30,28,26,27,19,29,18,31,24,23,21])).
% 182.14/182.50 cnf(2476,plain,
% 182.14/182.50 (P3(f9(a4,f3(a1,a1)),f3(a1,a1))),
% 182.14/182.50 inference(scs_inference,[],[2439,2418,11,17])).
% 182.14/182.50 cnf(2480,plain,
% 182.14/182.50 (P3(f3(a1,f3(a1,a1)),f3(a1,a1))),
% 182.14/182.50 inference(scs_inference,[],[2439,2418,11,17,20,16])).
% 182.14/182.50 cnf(2482,plain,
% 182.14/182.50 (P3(a1,f9(a4,a1))),
% 182.14/182.50 inference(scs_inference,[],[2402,2439,2418,11,17,20,16,14])).
% 182.14/182.50 cnf(2488,plain,
% 182.14/182.50 (P2(a1,f9(f3(a5,a1),f3(a5,a1)))),
% 182.14/182.50 inference(scs_inference,[],[2373,2402,2463,2439,2418,11,17,20,16,14,30,28,26])).
% 182.14/182.50 cnf(2490,plain,
% 182.14/182.50 (P1(f9(f3(a1,a1),f3(a1,a1)))),
% 182.14/182.50 inference(scs_inference,[],[2373,2402,2463,2439,2418,11,17,20,16,14,30,28,26,19])).
% 182.14/182.50 cnf(2494,plain,
% 182.14/182.50 (P1(f3(f3(a1,a1),f3(a1,a1)))),
% 182.14/182.50 inference(scs_inference,[],[2373,2402,2463,2439,2418,11,17,20,16,14,30,28,26,19,29,18])).
% 182.14/182.50 cnf(2496,plain,
% 182.14/182.50 (P2(f3(a1,f3(a1,a1)),f3(a5,f3(a1,a1)))),
% 182.14/182.50 inference(scs_inference,[],[7,2373,2402,2463,2439,2418,11,17,20,16,14,30,28,26,19,29,18,31])).
% 182.14/182.50 cnf(2498,plain,
% 182.14/182.50 (~P2(f3(a5,a1),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[7,2373,2402,2463,2439,2418,255,11,17,20,16,14,30,28,26,19,29,18,31,24])).
% 182.14/182.50 cnf(2500,plain,
% 182.14/182.50 (P2(f3(a1,a1),a5)),
% 182.14/182.50 inference(scs_inference,[],[7,2373,2402,2443,2463,2439,2418,255,11,17,20,16,14,30,28,26,19,29,18,31,24,23])).
% 182.14/182.50 cnf(2509,plain,
% 182.14/182.50 (P3(f3(a5,f6(a5)),a1)),
% 182.14/182.50 inference(scs_inference,[],[4,20])).
% 182.14/182.50 cnf(2511,plain,
% 182.14/182.50 (P3(f3(a1,a2),a2)),
% 182.14/182.50 inference(scs_inference,[],[4,3,20,16])).
% 182.14/182.50 cnf(2513,plain,
% 182.14/182.50 (P3(f9(a4,a5),a5)),
% 182.14/182.50 inference(scs_inference,[],[4,3,20,16,17])).
% 182.14/182.50 cnf(2517,plain,
% 182.14/182.50 (P3(f3(a1,a1),f3(a1,f3(a1,a1)))),
% 182.14/182.50 inference(scs_inference,[],[2480,2490,4,3,20,16,17,11,14])).
% 182.14/182.50 cnf(2519,plain,
% 182.14/182.50 (P1(f9(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[2480,2490,4,3,20,16,17,11,14,19])).
% 182.14/182.50 cnf(2521,plain,
% 182.14/182.50 (P1(f3(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[2480,2490,4,3,20,16,17,11,14,19,18])).
% 182.14/182.50 cnf(2523,plain,
% 182.14/182.50 (P2(f3(a1,a5),f3(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[7,2480,2490,4,3,20,16,17,11,14,19,18,31])).
% 182.14/182.50 cnf(2525,plain,
% 182.14/182.50 (~P2(f9(f9(a2,a2),f9(a2,a2)),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[7,2480,2490,2449,2010,4,3,20,16,17,11,14,19,18,31,24])).
% 182.14/182.50 cnf(2527,plain,
% 182.14/182.50 (P2(f9(a4,a1),a5)),
% 182.14/182.50 inference(scs_inference,[],[7,2482,2480,2490,2449,2010,4,3,20,16,17,11,14,19,18,31,24,23])).
% 182.14/182.50 cnf(2540,plain,
% 182.14/182.50 (P3(f9(a4,f9(a5,a5)),f9(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[2519,17])).
% 182.14/182.50 cnf(2546,plain,
% 182.14/182.50 (P3(f3(a1,f9(a5,a5)),f9(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[2519,2494,17,20,11,16])).
% 182.14/182.50 cnf(2548,plain,
% 182.14/182.50 (P3(a2,f3(a1,a2))),
% 182.14/182.50 inference(scs_inference,[],[2519,2511,2494,17,20,11,16,14])).
% 182.14/182.50 cnf(2556,plain,
% 182.14/182.50 (P1(f9(f9(a5,a5),f9(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[2519,2521,2389,2511,2494,17,20,11,16,14,30,28,27,19])).
% 182.14/182.50 cnf(2560,plain,
% 182.14/182.50 (P1(f3(f9(a5,a5),f9(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[2519,2521,2389,2511,2494,17,20,11,16,14,30,28,27,19,29,18])).
% 182.14/182.50 cnf(2562,plain,
% 182.14/182.50 (P2(f3(a1,f9(a5,a5)),f3(a5,f9(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[7,2519,2521,2389,2511,2494,17,20,11,16,14,30,28,27,19,29,18,31])).
% 182.14/182.50 cnf(2564,plain,
% 182.14/182.50 (~P2(f9(f3(a5,a1),f3(a5,a1)),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[7,2519,2521,2389,2511,2488,2494,255,17,20,11,16,14,30,28,27,19,29,18,31,24])).
% 182.14/182.50 cnf(2566,plain,
% 182.14/182.50 (P2(a5,f3(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[7,2519,2521,2389,2523,2511,2488,2494,2186,255,17,20,11,16,14,30,28,27,19,29,18,31,24,23])).
% 182.14/182.50 cnf(2568,plain,
% 182.14/182.50 (~P3(f3(a1,a4),a1)),
% 182.14/182.50 inference(scs_inference,[],[7,2519,2521,2389,2523,2511,2488,2494,267,2051,2186,255,17,20,11,16,14,30,28,27,19,29,18,31,24,23,21])).
% 182.14/182.50 cnf(2570,plain,
% 182.14/182.50 (~P1(f3(a5,a2))+P1(f8(f3(a5,a2)))),
% 182.14/182.50 inference(scs_inference,[],[7,2519,2521,2389,2523,2511,2488,2494,267,2051,2186,197,255,17,20,11,16,14,30,28,27,19,29,18,31,24,23,21,13])).
% 182.14/182.50 cnf(2574,plain,
% 182.14/182.50 (P1(f8(f3(a5,a2)))),
% 182.14/182.50 inference(scs_inference,[],[4,3,2570,18])).
% 182.14/182.50 cnf(2579,plain,
% 182.14/182.50 (P3(f9(a4,f3(a5,a5)),f3(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[2560,2574,2521,12,11,17])).
% 182.14/182.50 cnf(2581,plain,
% 182.14/182.50 (P3(f3(a1,f3(a5,a5)),f3(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[2560,2574,2521,12,11,17,16])).
% 182.14/182.50 cnf(2585,plain,
% 182.14/182.50 (P3(a5,f9(a4,a5))),
% 182.14/182.50 inference(scs_inference,[],[2513,2560,2574,2521,12,11,17,16,20,14])).
% 182.14/182.50 cnf(2587,plain,
% 182.14/182.50 (P3(f9(a2,f3(a5,a5)),f9(f3(a1,a2),f3(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[2548,2513,2560,2574,2521,12,11,17,16,20,14,30])).
% 182.14/182.50 cnf(2589,plain,
% 182.14/182.50 (P2(f3(a1,f3(a5,a5)),f3(a5,f3(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[7,2548,2513,2560,2574,2521,12,11,17,16,20,14,30,31])).
% 182.14/182.50 cnf(2591,plain,
% 182.14/182.50 (P1(f9(f3(a5,a5),f3(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[7,2548,2513,2560,2574,2521,12,11,17,16,20,14,30,31,19])).
% 182.14/182.50 cnf(2593,plain,
% 182.14/182.50 (P3(f3(a2,f3(a5,a5)),f3(f3(a1,a2),f3(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[7,2548,2513,2560,2574,2521,12,11,17,16,20,14,30,31,19,29])).
% 182.14/182.50 cnf(2595,plain,
% 182.14/182.50 (~P3(f3(a2,a5),a5)),
% 182.14/182.50 inference(scs_inference,[],[7,2223,2548,2513,2560,2574,149,2521,12,11,17,16,20,14,30,31,19,29,23])).
% 182.14/182.50 cnf(2597,plain,
% 182.14/182.50 (P3(f9(a4,a5),f3(a1,a5))),
% 182.14/182.50 inference(scs_inference,[],[7,2223,2548,2513,2560,2574,149,2521,2137,12,11,17,16,20,14,30,31,19,29,23,21])).
% 182.14/182.50 cnf(2599,plain,
% 182.14/182.50 (P1(f3(f3(a5,a5),f3(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[7,2223,2548,2513,2560,2574,149,2521,2137,12,11,17,16,20,14,30,31,19,29,23,21,18])).
% 182.14/182.50 cnf(2601,plain,
% 182.14/182.50 (P2(f3(a1,a1),f3(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[7,2223,2500,2566,2548,2513,2560,2574,149,2521,2137,12,11,17,16,20,14,30,31,19,29,23,21,18,24])).
% 182.14/182.50 cnf(2603,plain,
% 182.14/182.50 (~P3(a5,f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[7,2223,2500,2566,2548,2513,2560,2574,149,2521,2137,12,11,17,16,20,14,30,31,19,29,23,21,18,24,195])).
% 182.14/182.50 cnf(2605,plain,
% 182.14/182.50 (~P1(f3(a1,a4))+P3(f9(f3(a1,a4),f8(f3(a1,a4))),a4)),
% 182.14/182.50 inference(scs_inference,[],[7,2223,2500,2568,2566,2548,2513,2560,2574,149,2521,2137,12,11,17,16,20,14,30,31,19,29,23,21,18,24,195,25])).
% 182.14/182.50 cnf(2609,plain,
% 182.14/182.50 (~P2(a5,f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[2595,288])).
% 182.14/182.50 cnf(2610,plain,
% 182.14/182.50 (~P2(a5,a7)),
% 182.14/182.50 inference(scs_inference,[],[2595,304])).
% 182.14/182.50 cnf(2612,plain,
% 182.14/182.50 (P3(f9(a4,a4),a4)),
% 182.14/182.50 inference(scs_inference,[],[2,17])).
% 182.14/182.50 cnf(2616,plain,
% 182.14/182.50 (P3(f3(a1,a4),a4)),
% 182.14/182.50 inference(scs_inference,[],[2599,2,17,11,16])).
% 182.14/182.50 cnf(2618,plain,
% 182.14/182.50 (P3(f3(a4,f6(a4)),a1)),
% 182.14/182.50 inference(scs_inference,[],[2599,2,17,11,16,20])).
% 182.14/182.50 cnf(2620,plain,
% 182.14/182.50 (P3(f3(a1,a5),f9(a4,a5))),
% 182.14/182.50 inference(scs_inference,[],[2597,2599,2,17,11,16,20,14])).
% 182.14/182.50 cnf(2622,plain,
% 182.14/182.50 (P1(f9(a4,a4))),
% 182.14/182.50 inference(scs_inference,[],[2597,2599,2,17,11,16,20,14,19])).
% 182.14/182.50 cnf(2624,plain,
% 182.14/182.50 (P2(f3(a1,f3(a1,a1)),f3(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[2601,2597,2599,2517,2,17,11,16,20,14,19,23])).
% 182.14/182.50 cnf(2626,plain,
% 182.14/182.50 (~P3(a7,a5)),
% 182.14/182.50 inference(scs_inference,[],[8,2601,2597,2595,2599,2517,2,17,11,16,20,14,19,23,21])).
% 182.14/182.50 cnf(2628,plain,
% 182.14/182.50 (P1(f3(a4,a4))),
% 182.14/182.50 inference(scs_inference,[],[8,2601,2597,2595,2599,2517,2,17,11,16,20,14,19,23,21,18])).
% 182.14/182.50 cnf(2630,plain,
% 182.14/182.50 (P2(f9(a4,a1),f3(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[8,2601,2597,2527,2595,2599,2517,2566,2,17,11,16,20,14,19,23,21,18,24])).
% 182.14/182.50 cnf(2641,plain,
% 182.14/182.50 (~P2(a5,f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[2626,300])).
% 182.14/182.50 cnf(2643,plain,
% 182.14/182.50 (P3(f3(a1,f9(a4,a4)),f9(a4,a4))),
% 182.14/182.50 inference(scs_inference,[],[2622,16])).
% 182.14/182.50 cnf(2645,plain,
% 182.14/182.50 (P3(f9(a4,f9(a4,a4)),f9(a4,a4))),
% 182.14/182.50 inference(scs_inference,[],[2622,16,17])).
% 182.14/182.50 cnf(2651,plain,
% 182.14/182.50 (P3(a4,f9(a4,a4))),
% 182.14/182.50 inference(scs_inference,[],[2622,2612,2556,16,17,20,11,14])).
% 182.14/182.50 cnf(2653,plain,
% 182.14/182.50 (P3(f9(f3(a2,a5),f9(a4,a4)),f9(a7,f9(a4,a4)))),
% 182.14/182.50 inference(scs_inference,[],[8,2622,2612,2556,16,17,20,11,14,30])).
% 182.14/182.50 cnf(2661,plain,
% 182.14/182.50 (P3(f3(f3(a2,a5),f9(a4,a4)),f3(a7,f9(a4,a4)))),
% 182.14/182.50 inference(scs_inference,[],[8,2622,2628,2202,2612,2556,16,17,20,11,14,30,28,27,31,29])).
% 182.14/182.50 cnf(2663,plain,
% 182.14/182.50 (P1(f9(f9(a4,a4),f9(a4,a4)))),
% 182.14/182.50 inference(scs_inference,[],[8,2622,2628,2202,2612,2556,16,17,20,11,14,30,28,27,31,29,19])).
% 182.14/182.50 cnf(2665,plain,
% 182.14/182.50 (~P3(f3(a5,a2),f9(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[8,2622,2628,2255,2202,2612,2556,2034,16,17,20,11,14,30,28,27,31,29,19,23])).
% 182.14/182.50 cnf(2667,plain,
% 182.14/182.50 (P3(f3(a1,a5),f3(a1,a5))),
% 182.14/182.50 inference(scs_inference,[],[8,2622,2628,2255,2202,2620,2612,2556,2597,2034,16,17,20,11,14,30,28,27,31,29,19,23,21])).
% 182.14/182.50 cnf(2669,plain,
% 182.14/182.50 (P1(f3(f9(a4,a4),f9(a4,a4)))),
% 182.14/182.50 inference(scs_inference,[],[8,2622,2628,2255,2202,2620,2612,2556,2597,2034,16,17,20,11,14,30,28,27,31,29,19,23,21,18])).
% 182.14/182.50 cnf(2673,plain,
% 182.14/182.50 (P3(f9(a4,a4),a1)+P1(f8(f9(a4,a4)))),
% 182.14/182.50 inference(scs_inference,[],[8,2622,2628,2255,2202,2620,2612,2556,2597,2295,2034,2010,16,17,20,11,14,30,28,27,31,29,19,23,21,18,24,13])).
% 182.14/182.50 cnf(2680,plain,
% 182.14/182.50 (P3(f3(a1,f3(a4,a4)),f3(a4,a4))),
% 182.14/182.50 inference(scs_inference,[],[2628,20,16])).
% 182.14/182.50 cnf(2682,plain,
% 182.14/182.50 (P3(f9(a4,f3(a4,a4)),f3(a4,a4))),
% 182.14/182.50 inference(scs_inference,[],[2628,20,16,17])).
% 182.14/182.50 cnf(2684,plain,
% 182.14/182.50 (P1(f6(f9(f9(a4,a4),f9(a4,a4))))),
% 182.14/182.50 inference(scs_inference,[],[2663,2628,20,16,17,11])).
% 182.14/182.50 cnf(2686,plain,
% 182.14/182.50 (P3(f9(a4,a4),f9(a4,f9(a4,a4)))),
% 182.14/182.50 inference(scs_inference,[],[2645,2663,2628,20,16,17,11,14])).
% 182.14/182.50 cnf(2690,plain,
% 182.14/182.50 (P3(f3(f3(a2,a5),f3(a4,a4)),f3(a7,f3(a4,a4)))),
% 182.14/182.50 inference(scs_inference,[],[8,2630,2645,2663,2628,20,16,17,11,14,31,29])).
% 182.14/182.50 cnf(2692,plain,
% 182.14/182.50 (P1(f9(f3(a4,a4),f3(a4,a4)))),
% 182.14/182.50 inference(scs_inference,[],[8,2630,2645,2663,2628,20,16,17,11,14,31,29,19])).
% 182.14/182.50 cnf(2694,plain,
% 182.14/182.50 (P2(a1,f3(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[8,2630,2645,2663,2402,2628,20,16,17,11,14,31,29,19,23])).
% 182.14/182.50 cnf(2696,plain,
% 182.14/182.50 (~P3(f9(a4,a5),f3(a5,a2))),
% 182.14/182.50 inference(scs_inference,[],[8,2630,2585,2645,2663,2603,2402,2628,20,16,17,11,14,31,29,19,23,21])).
% 182.14/182.50 cnf(2698,plain,
% 182.14/182.50 (P1(f3(f3(a4,a4),f3(a4,a4)))),
% 182.14/182.50 inference(scs_inference,[],[8,2630,2585,2645,2663,2603,2402,2628,20,16,17,11,14,31,29,19,23,21,18])).
% 182.14/182.50 cnf(2700,plain,
% 182.14/182.50 (~P2(f3(a5,a5),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[8,2273,2630,2585,2645,2663,2603,2402,2566,2628,20,16,17,11,14,31,29,19,23,21,18,24])).
% 182.14/182.50 cnf(2704,plain,
% 182.14/182.50 (P2(a1,f9(f3(a5,a5),f3(a5,a5)))),
% 182.14/182.50 inference(scs_inference,[],[8,2273,2630,2585,2645,2663,2603,2402,2566,2628,1801,20,16,17,11,14,31,29,19,23,21,18,24,1686,26])).
% 182.14/182.50 cnf(2709,plain,
% 182.14/182.50 (P3(f9(a4,a2),a2)),
% 182.14/182.50 inference(scs_inference,[],[3,17])).
% 182.14/182.50 cnf(2711,plain,
% 182.14/182.50 (P3(f3(a2,f6(a2)),a1)),
% 182.14/182.50 inference(scs_inference,[],[3,17,20])).
% 182.14/182.50 cnf(2715,plain,
% 182.14/182.50 (P3(f9(a1,a1),f3(a1,f9(a1,a1)))),
% 182.14/182.50 inference(scs_inference,[],[2435,2698,3,17,20,11,14])).
% 182.14/182.50 cnf(2717,plain,
% 182.14/182.50 (P1(f9(a2,a2))),
% 182.14/182.50 inference(scs_inference,[],[2435,2698,3,17,20,11,14,19])).
% 182.14/182.50 cnf(2719,plain,
% 182.14/182.50 (~P3(f3(a5,a2),f3(a5,a5))),
% 182.14/182.50 inference(scs_inference,[],[2700,2435,2698,2030,3,17,20,11,14,19,23])).
% 182.14/182.50 cnf(2723,plain,
% 182.14/182.50 (P1(f3(a2,a2))),
% 182.14/182.50 inference(scs_inference,[],[2700,2651,2435,2698,108,2030,3,17,20,11,14,19,23,21,18])).
% 182.14/182.50 cnf(2725,plain,
% 182.14/182.50 (~P2(f9(f3(a5,a5),f3(a5,a5)),f3(a2,a5))),
% 182.14/182.50 inference(scs_inference,[],[2700,2651,2435,2698,2704,108,2030,255,3,17,20,11,14,19,23,21,18,24])).
% 182.14/182.50 cnf(2727,plain,
% 182.14/182.50 (P3(f3(a1,f9(a2,a2)),f9(a2,a2))),
% 182.14/182.50 inference(scs_inference,[],[2700,2651,2435,2698,2704,108,2030,255,3,17,20,11,14,19,23,21,18,24,16])).
% 182.14/182.50 cnf(2744,plain,
% 182.14/182.50 (P3(f3(a1,f3(a2,a2)),f3(a2,a2))),
% 182.14/182.50 inference(scs_inference,[],[2723,2669,11,16])).
% 182.14/182.50 cnf(2746,plain,
% 182.25/182.50 (P3(f9(a4,f9(a2,a2)),f9(a2,a2))),
% 182.25/182.50 inference(scs_inference,[],[2717,2723,2669,11,16,17])).
% 182.25/182.50 cnf(2750,plain,
% 182.25/182.50 (P3(a2,f9(a4,a2))),
% 182.25/182.50 inference(scs_inference,[],[2717,2723,2709,2669,11,16,17,20,14])).
% 182.25/182.50 cnf(2752,plain,
% 182.25/182.50 (P3(f9(f3(a2,a5),f9(a2,a2)),f9(a7,f9(a2,a2)))),
% 182.25/182.50 inference(scs_inference,[],[8,2717,2723,2709,2669,11,16,17,20,14,30])).
% 182.25/182.50 cnf(2758,plain,
% 182.25/182.50 (P3(f3(f3(a2,a5),f9(a2,a2)),f3(a7,f9(a2,a2)))),
% 182.25/182.50 inference(scs_inference,[],[8,2717,2723,2709,2669,11,16,17,20,14,30,28,27,29])).
% 182.25/182.50 cnf(2762,plain,
% 182.25/182.50 (P1(f9(f9(a2,a2),f9(a2,a2)))),
% 182.25/182.50 inference(scs_inference,[],[8,2717,2723,2709,2624,2669,11,16,17,20,14,30,28,27,29,31,19])).
% 182.25/182.50 cnf(2764,plain,
% 182.25/182.50 (P2(f3(f3(a1,a1),a1),f3(a5,a5))),
% 182.25/182.50 inference(scs_inference,[],[8,2717,2723,2709,2624,2263,2669,11,16,17,20,14,30,28,27,29,31,19,23])).
% 182.25/182.50 cnf(2768,plain,
% 182.25/182.50 (P1(f3(f9(a2,a2),f9(a2,a2)))),
% 182.25/182.50 inference(scs_inference,[],[8,2717,2723,2696,2709,2624,2263,2669,2597,11,16,17,20,14,30,28,27,29,31,19,23,21,18])).
% 182.25/182.50 cnf(2770,plain,
% 182.25/182.50 (~P2(f3(a5,a5),a7)),
% 182.25/182.50 inference(scs_inference,[],[8,2717,2723,2696,2709,2624,2263,2610,2669,2597,2566,11,16,17,20,14,30,28,27,29,31,19,23,21,18,24])).
% 182.25/182.50 cnf(2772,plain,
% 182.25/182.50 (P2(a7,f3(a5,a5))),
% 182.25/182.50 inference(scs_inference,[],[8,2717,2723,2696,2709,2624,2263,2610,2669,2597,2566,2521,5,11,16,17,20,14,30,28,27,29,31,19,23,21,18,24,15])).
% 182.25/182.50 cnf(2781,plain,
% 182.25/182.50 (P3(f9(a4,f3(a2,a2)),f3(a2,a2))),
% 182.25/182.50 inference(scs_inference,[],[2762,2723,11,17])).
% 182.25/182.50 cnf(2785,plain,
% 182.25/182.50 (P3(f8(a4),f3(a1,f8(a4)))),
% 182.25/182.50 inference(scs_inference,[],[2326,2762,2723,11,17,20,14])).
% 182.25/182.50 cnf(2787,plain,
% 182.25/182.50 (P3(f9(f3(a2,a5),f3(a2,a2)),f9(a7,f3(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[8,2326,2762,2723,11,17,20,14,30])).
% 182.25/182.51 cnf(2793,plain,
% 182.25/182.51 (P1(f9(f3(a2,a2),f3(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[8,2772,2326,2762,2723,11,17,20,14,30,29,31,19])).
% 182.25/182.51 cnf(2795,plain,
% 182.25/182.51 (~P3(f3(a5,a2),f9(a2,a2))),
% 182.25/182.51 inference(scs_inference,[],[8,2461,2772,2326,2762,1778,2723,11,17,20,14,30,29,31,19,23])).
% 182.25/182.51 cnf(2797,plain,
% 182.25/182.51 (P3(f9(a4,f9(a1,a1)),f3(a1,f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[8,2461,2772,2326,2441,2762,2715,1778,2723,11,17,20,14,30,29,31,19,23,21])).
% 182.25/182.51 cnf(2799,plain,
% 182.25/182.51 (P1(f3(f3(a2,a2),f3(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[8,2461,2772,2326,2441,2762,2715,1778,2723,11,17,20,14,30,29,31,19,23,21,18])).
% 182.25/182.51 cnf(2801,plain,
% 182.25/182.51 (~P2(f3(a5,a5),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[8,2461,2772,2326,2441,2762,2715,2694,1778,2723,2010,11,17,20,14,30,29,31,19,23,21,18,24])).
% 182.25/182.51 cnf(2810,plain,
% 182.25/182.51 (P3(f9(a5,a5),f3(a1,f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2546,2793,11,14])).
% 182.25/182.51 cnf(2816,plain,
% 182.25/182.51 (~P2(f9(f9(a5,a5),f9(a5,a5)),f3(a2,a5))),
% 182.25/182.51 inference(scs_inference,[],[2546,2793,2383,2651,2365,2243,566,255,11,14,23,21,24])).
% 182.25/182.51 cnf(2822,plain,
% 182.25/182.51 (P3(a4,f9(f3(a1,a4),f8(f3(a1,a4))))+~P1(f3(a1,a4))),
% 182.25/182.51 inference(scs_inference,[],[2605,14])).
% 182.25/182.51 cnf(2825,plain,
% 182.25/182.51 (P3(f3(a5,a5),f3(a1,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2581,2799,11,14])).
% 182.25/182.51 cnf(2827,plain,
% 182.25/182.51 (~P3(f3(a5,a2),f9(a1,a1))),
% 182.25/182.51 inference(scs_inference,[],[2385,2581,2799,2034,11,14,23])).
% 182.25/182.51 cnf(2829,plain,
% 182.25/182.51 (P3(f3(a1,f9(a4,a4)),f9(a4,f9(a4,a4)))),
% 182.25/182.51 inference(scs_inference,[],[2385,2581,2643,2686,2799,2034,11,14,23,21])).
% 182.25/182.51 cnf(2831,plain,
% 182.25/182.51 (~P2(f9(f9(a1,a1),f9(a1,a1)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[2385,2581,2643,2686,2799,2375,2034,2010,11,14,23,21,24])).
% 182.25/182.51 cnf(2840,plain,
% 182.25/182.51 (P3(f3(a4,a4),f3(a1,f3(a4,a4)))),
% 182.25/182.51 inference(scs_inference,[],[2680,2768,11,14])).
% 182.25/182.51 cnf(2842,plain,
% 182.25/182.51 (P2(f3(a5,a5),f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2680,2589,2768,2581,11,14,23])).
% 182.25/182.51 cnf(2846,plain,
% 182.25/182.51 (~P2(f3(a5,f3(a5,a5)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[2801,2680,2589,2768,2581,469,2651,11,14,23,21,24])).
% 182.25/182.51 cnf(2848,plain,
% 182.25/182.51 (P3(f9(f3(a2,a5),f3(a4,a4)),f9(a7,f3(a4,a4)))),
% 182.25/182.51 inference(scs_inference,[],[8,2801,2680,2589,2768,2581,469,2651,2628,11,14,23,21,24,30])).
% 182.25/182.51 cnf(2854,plain,
% 182.25/182.51 (P3(a4,f9(f3(a1,a4),f8(f3(a1,a4))))),
% 182.25/182.51 inference(scs_inference,[],[2,1,2822,18])).
% 182.25/182.51 cnf(2857,plain,
% 182.25/182.51 (P3(f9(a2,a2),f3(a1,f9(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[2727,2591,11,14])).
% 182.25/182.51 cnf(2859,plain,
% 182.25/182.51 (~P3(f3(a2,a5),f3(a5,a1))),
% 182.25/182.51 inference(scs_inference,[],[2498,2727,2591,149,11,14,23])).
% 182.25/182.51 cnf(2861,plain,
% 182.25/182.51 (P3(f9(a4,f3(a1,a1)),f3(a1,f3(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[2498,2727,2476,2591,2517,149,11,14,23,21])).
% 182.25/182.51 cnf(2863,plain,
% 182.25/182.51 (~P2(f3(a5,f3(a5,a5)),a7)),
% 182.25/182.51 inference(scs_inference,[],[2498,2770,2727,2476,2842,2591,2517,149,11,14,23,21,24])).
% 182.25/182.51 cnf(2874,plain,
% 182.25/182.51 (P3(f3(a2,a2),f3(a1,f3(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[2744,2453,11,14])).
% 182.25/182.51 cnf(2876,plain,
% 182.25/182.51 (P2(f3(a1,a1),f3(a5,f3(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[2744,2496,2453,2480,11,14,23])).
% 182.25/182.51 cnf(2880,plain,
% 182.25/182.51 (~P2(f3(a5,f3(a5,a5)),f3(a2,a5))),
% 182.25/182.51 inference(scs_inference,[],[8,2859,2744,2496,2453,2700,2480,2842,11,14,23,21,24])).
% 182.25/182.51 cnf(2890,plain,
% 182.25/182.51 (P3(f8(a4),f9(a4,f8(a4)))),
% 182.25/182.51 inference(scs_inference,[],[2320,2457,11,14])).
% 182.25/182.51 cnf(2894,plain,
% 182.25/182.51 (~P3(f3(a2,a5),f9(f9(a5,a5),f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2616,2816,2320,2457,149,2200,11,14,29,23])).
% 182.25/182.51 cnf(2896,plain,
% 182.25/182.51 (P3(f9(a4,f8(a4)),f3(a1,f8(a4)))),
% 182.25/182.51 inference(scs_inference,[],[2616,2816,2320,2785,2457,149,2200,11,14,29,23,21])).
% 182.25/182.51 cnf(2898,plain,
% 182.25/182.51 (P2(f3(a1,a1),f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2616,2816,2320,2785,2457,2601,2842,149,2200,11,14,29,23,21,24])).
% 182.25/182.51 cnf(2909,plain,
% 182.25/182.51 (P3(f8(a7),f9(a4,f8(a7)))),
% 182.25/182.51 inference(scs_inference,[],[2279,2381,11,14])).
% 182.25/182.51 cnf(2911,plain,
% 182.25/182.51 (P2(a1,f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2279,2898,2381,2406,11,14,23])).
% 182.25/182.51 cnf(2913,plain,
% 182.25/182.51 (~P3(f3(a5,a2),f9(f9(a5,a5),f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2279,2894,2898,2381,2406,1801,11,14,23,21])).
% 182.25/182.51 cnf(2917,plain,
% 182.25/182.51 (P2(a7,f9(f9(a2,a2),f9(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[10,2279,2894,2898,2381,2449,2762,2406,1801,5,11,14,23,21,24,15])).
% 182.25/182.51 cnf(2925,plain,
% 182.25/182.51 (P3(f9(a5,a5),f9(a4,f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2540,2251,11,14])).
% 182.25/182.51 cnf(2929,plain,
% 182.25/182.51 (P3(f9(a4,f9(a5,a5)),f3(a1,f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2725,2540,2810,2251,2030,11,14,23,21])).
% 182.25/182.51 cnf(2931,plain,
% 182.25/182.51 (P2(a7,f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2725,2540,2810,2251,2772,2842,2030,11,14,23,21,24])).
% 182.25/182.51 cnf(2941,plain,
% 182.25/182.51 (P3(f3(a5,a5),f9(a4,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2579,2237,11,14])).
% 182.25/182.51 cnf(2943,plain,
% 182.25/182.51 (P2(f8(a4),f3(a5,f8(a4)))),
% 182.25/182.51 inference(scs_inference,[],[2579,2344,2237,2326,11,14,23])).
% 182.25/182.51 cnf(2945,plain,
% 182.25/182.51 (~P3(f3(a5,a2),f3(a5,a1))),
% 182.25/182.51 inference(scs_inference,[],[2579,2344,2237,2326,2859,1801,11,14,23,21])).
% 182.25/182.51 cnf(2953,plain,
% 182.25/182.51 (P3(f3(a4,a4),f9(a4,f3(a4,a4)))),
% 182.25/182.51 inference(scs_inference,[],[2682,2299,11,14])).
% 182.25/182.51 cnf(2955,plain,
% 182.25/182.51 (~P3(f3(a2,a5),f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2682,2880,2299,149,11,14,23])).
% 182.25/182.51 cnf(2957,plain,
% 182.25/182.51 (P3(f9(a4,f3(a4,a4)),f3(a1,f3(a4,a4)))),
% 182.25/182.51 inference(scs_inference,[],[2682,2840,2880,2299,149,11,14,23,21])).
% 182.25/182.51 cnf(2959,plain,
% 182.25/182.51 (P2(f3(a1,a5),f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2682,2840,2880,2299,2523,149,2842,11,14,23,21,24])).
% 182.25/182.51 cnf(2961,plain,
% 182.25/182.51 (~P3(f3(a5,f3(a5,a5)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[2682,2840,2880,2299,2523,149,2842,11,14,23,21,24,195])).
% 182.25/182.51 cnf(2969,plain,
% 182.25/182.51 (P3(f9(a2,a2),f9(a4,f9(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[2746,2289,11,14])).
% 182.25/182.51 cnf(2973,plain,
% 182.25/182.51 (P2(f9(a4,f8(a4)),f3(a5,f8(a4)))),
% 182.25/182.51 inference(scs_inference,[],[2746,2959,2890,2943,2289,2628,11,14,31,23])).
% 182.25/182.51 cnf(2977,plain,
% 182.25/182.51 (~P2(f9(f3(a5,a1),f3(a5,a1)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[2746,2961,2959,2890,2943,2311,2564,2289,2030,2628,11,14,31,23,21,24])).
% 182.25/182.51 cnf(2985,plain,
% 182.25/182.51 (P3(f3(a2,a2),f9(a4,f3(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[2781,2281,11,14])).
% 182.25/182.51 cnf(2987,plain,
% 182.25/182.51 (P3(f3(a2,f9(a5,a5)),f3(f9(a4,a2),f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2750,2781,2281,2519,11,14,29])).
% 182.25/182.51 cnf(2989,plain,
% 182.25/182.51 (~P3(f3(a5,a2),f9(f3(a5,a1),f3(a5,a1)))),
% 182.25/182.51 inference(scs_inference,[],[2750,2781,2977,2281,2034,2519,11,14,29,23])).
% 182.25/182.51 cnf(2991,plain,
% 182.25/182.51 (P3(f9(a4,f3(a2,a2)),f3(a1,f3(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[2750,2781,2977,2874,2281,2034,2519,11,14,29,23,21])).
% 182.25/182.51 cnf(2995,plain,
% 182.25/182.51 (P3(f9(a2,f9(a5,a5)),f9(f9(a4,a2),f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2750,2781,2977,2874,2281,2764,2034,2842,2519,11,14,29,23,21,24,30])).
% 182.25/182.51 cnf(3003,plain,
% 182.25/182.51 (P3(f3(a1,a4),f9(a7,f8(a7)))),
% 182.25/182.51 inference(scs_inference,[],[2259,2692,11,14])).
% 182.25/182.51 cnf(3005,plain,
% 182.25/182.51 (P2(a4,f3(a5,f8(a4)))),
% 182.25/182.51 inference(scs_inference,[],[2259,2245,2973,2692,11,14,23])).
% 182.25/182.51 cnf(3007,plain,
% 182.25/182.51 (~P3(f3(a5,a2),f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2259,2245,2973,2955,2692,1801,11,14,23,21])).
% 182.25/182.51 cnf(3009,plain,
% 182.25/182.51 (~P2(f9(f3(a5,a1),f3(a5,a1)),a7)),
% 182.25/182.51 inference(scs_inference,[],[10,2259,2245,2973,2955,2488,2692,1801,11,14,23,21,24])).
% 182.25/182.51 cnf(3017,plain,
% 182.25/182.51 (P3(a1,f3(a7,f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[2184,2574,11,14])).
% 182.25/182.51 cnf(3021,plain,
% 182.25/182.51 (P3(f9(a4,f3(a1,a1)),f3(f3(a1,a1),a1))),
% 182.25/182.51 inference(scs_inference,[],[2184,3009,2861,2263,2574,63,11,14,23,21])).
% 182.25/182.51 cnf(3023,plain,
% 182.25/182.51 (~P2(f9(f3(a5,a5),f3(a5,a5)),a7)),
% 182.25/182.51 inference(scs_inference,[],[10,2184,3009,2861,2704,2263,2574,63,11,14,23,21,24])).
% 182.25/182.51 cnf(3025,plain,
% 182.25/182.51 (P2(a7,f9(f3(a5,a5),f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[10,2184,3009,2861,2704,2263,2591,2574,63,5,11,14,23,21,24,15])).
% 182.25/182.51 cnf(3033,plain,
% 182.25/182.51 (P3(a1,f3(a1,f6(a1)))),
% 182.25/182.51 inference(scs_inference,[],[2408,2334,11,14])).
% 182.25/182.51 cnf(3035,plain,
% 182.25/182.51 (P2(f9(a1,a1),f3(a5,f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[2408,2459,2435,2334,11,14,23])).
% 182.25/182.51 cnf(3041,plain,
% 182.25/182.51 (~P3(f3(a7,f6(a7)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[2408,3017,3023,2459,2435,2334,1803,2008,11,14,23,21,24,192])).
% 182.25/182.51 cnf(3049,plain,
% 182.25/182.51 (P3(a1,f3(a2,f6(a2)))),
% 182.25/182.51 inference(scs_inference,[],[2711,257,11,14])).
% 182.25/182.51 cnf(3051,plain,
% 182.25/182.51 (~P2(f3(a5,f9(a1,a1)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[2711,3035,2385,257,11,14,24])).
% 182.25/182.51 cnf(3055,plain,
% 182.25/182.51 (P3(f3(a2,f6(a2)),f3(a1,f6(a1)))),
% 182.25/182.51 inference(scs_inference,[],[2711,3035,3033,2525,2385,257,1778,11,14,24,23,21])).
% 182.25/182.51 cnf(3059,plain,
% 182.25/182.51 (P3(f9(f3(a1,a4),f3(a1,a1)),f9(f9(a7,f8(a7)),f3(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[3003,2711,3035,3033,2525,2385,257,1778,2418,11,14,24,23,21,22,30])).
% 182.25/182.51 cnf(3065,plain,
% 182.25/182.51 (P1(f6(a1))),
% 182.25/182.51 inference(scs_inference,[],[1,11])).
% 182.25/182.51 cnf(3067,plain,
% 182.25/182.51 (P3(a1,f3(a5,f6(a5)))),
% 182.25/182.51 inference(scs_inference,[],[1,2509,11,14])).
% 182.25/182.51 cnf(3075,plain,
% 182.25/182.51 (P3(f3(f3(a5,f6(a5)),a1),f3(a1,a1))),
% 182.25/182.51 inference(scs_inference,[],[1,2509,3005,11,14,30,27,31,29])).
% 182.25/182.51 cnf(3077,plain,
% 182.25/182.51 (P2(f9(a5,a5),f3(a5,f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[1,2509,3005,2562,2546,11,14,30,27,31,29,23])).
% 182.25/182.51 cnf(3081,plain,
% 182.25/182.51 (P1(f3(f6(a1),f6(a1)))),
% 182.25/182.51 inference(scs_inference,[],[1,2509,3049,3005,2562,2546,1803,11,14,30,27,31,29,23,21,18])).
% 182.25/182.51 cnf(3083,plain,
% 182.25/182.51 (~P3(f3(a2,f6(a2)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[1,2509,3049,3005,2562,2546,1803,11,14,30,27,31,29,23,21,18,192])).
% 182.25/182.51 cnf(3085,plain,
% 182.25/182.51 (P3(f6(a1),f6(a1))),
% 182.25/182.51 inference(scs_inference,[],[1,2509,3049,3005,2562,2546,1803,11,14,30,27,31,29,23,21,18,192,12])).
% 182.25/182.51 cnf(3087,plain,
% 182.25/182.51 (P3(f3(a1,f6(a1)),f6(a1))),
% 182.25/182.51 inference(scs_inference,[],[1,2509,3049,3005,2562,2546,1803,11,14,30,27,31,29,23,21,18,192,12,16])).
% 182.25/182.51 cnf(3089,plain,
% 182.25/182.51 (P3(f9(a4,f6(a1)),f6(a1))),
% 182.25/182.51 inference(scs_inference,[],[1,2509,3049,3005,2562,2546,1803,11,14,30,27,31,29,23,21,18,192,12,16,17])).
% 182.25/182.51 cnf(3095,plain,
% 182.25/182.51 (~P2(f3(a5,f9(a5,a5)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[1,3041,2509,3049,3005,2562,2546,2255,1803,11,14,30,27,31,29,23,21,18,192,12,16,17,20,22,24])).
% 182.25/182.51 cnf(3099,plain,
% 182.25/182.51 (P1(f6(f6(a1)))),
% 182.25/182.51 inference(scs_inference,[],[3065,11])).
% 182.25/182.51 cnf(3101,plain,
% 182.25/182.51 (P3(f6(a1),f3(a1,f6(a1)))),
% 182.25/182.51 inference(scs_inference,[],[3065,3087,11,14])).
% 182.25/182.51 cnf(3103,plain,
% 182.25/182.51 (P2(f3(a1,a4),f3(a5,f8(a4)))),
% 182.25/182.51 inference(scs_inference,[],[3065,3087,3005,1849,11,14,24])).
% 182.25/182.51 cnf(3111,plain,
% 182.25/182.51 (~P3(f3(a5,a2),f3(a5,f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[1,3065,3085,3095,3087,2917,3005,1849,2034,11,14,24,30,31,29,23])).
% 182.25/182.51 cnf(3113,plain,
% 182.25/182.51 (P3(f3(a4,f6(a4)),f3(a5,f6(a5)))),
% 182.25/182.51 inference(scs_inference,[],[1,3065,3085,3095,3087,2618,3067,2917,3005,1849,2034,11,14,24,30,31,29,23,21])).
% 182.25/182.51 cnf(3133,plain,
% 182.25/182.51 (~P3(f3(a1,f6(a1)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[1,3083,3089,3103,3081,3055,1799,2420,3065,2517,11,14,30,31,29,23,21])).
% 182.25/182.51 cnf(3154,plain,
% 182.25/182.51 (P2(f9(a4,a1),f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2214,3099,2630,2842,11,14,24])).
% 182.25/182.51 cnf(3156,plain,
% 182.25/182.51 (P3(f9(f3(a2,a2),f6(a1)),f9(f9(a4,f3(a2,a2)),f6(a1)))),
% 182.25/182.51 inference(scs_inference,[],[2985,2214,3099,2630,3065,2842,11,14,24,30])).
% 182.25/182.51 cnf(3164,plain,
% 182.25/182.51 (P3(f3(a1,f9(a4,a4)),f9(f9(a4,a4),a4))),
% 182.25/182.51 inference(scs_inference,[],[1,2985,2214,2391,2829,3025,3099,3051,2630,3065,1778,2842,11,14,24,30,31,29,23,21])).
% 182.25/182.51 cnf(3174,plain,
% 182.25/182.51 (P3(f9(a7,a1),f9(a7,a1))),
% 182.25/182.51 inference(scs_inference,[],[1,2210,65,76,11,14,30])).
% 182.25/182.51 cnf(3178,plain,
% 182.25/182.51 (P3(f3(a7,a1),f3(a7,a1))),
% 182.25/182.51 inference(scs_inference,[],[1,3154,2210,65,76,3065,11,14,30,31,29])).
% 182.25/182.51 cnf(3182,plain,
% 182.25/182.51 (~P3(f6(a1),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[1,3133,3154,2909,2210,65,3087,2387,76,3065,11,14,30,31,29,23,21])).
% 182.25/182.51 cnf(3191,plain,
% 182.25/182.51 (P3(f9(f9(a7,a7),a7),f9(a7,f9(a7,a7)))),
% 182.25/182.51 inference(scs_inference,[],[2212,475,11,14])).
% 182.25/182.51 cnf(3201,plain,
% 182.25/182.51 (~P3(f3(a5,a2),f9(f9(a1,a1),f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[1,3178,2212,2931,2831,2624,475,2034,2842,11,14,24,30,29,31,23])).
% 182.25/182.51 cnf(3217,plain,
% 182.25/182.51 (P2(a1,f3(a5,f3(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[1,3174,2265,2876,418,2406,11,14,30,29,23])).
% 182.25/182.51 cnf(3221,plain,
% 182.25/182.51 (~P3(f9(f3(a5,a1),f3(a5,a1)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[1,3174,2989,2265,2876,418,2406,184,11,14,30,29,23,21,195])).
% 182.25/182.51 cnf(3231,plain,
% 182.25/182.51 (P3(f9(f9(a1,a1),a1),f9(a1,f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[2261,944,11,14])).
% 182.25/182.51 cnf(3233,plain,
% 182.25/182.51 (~P2(f3(a5,f3(a1,a1)),f3(a2,a5))),
% 182.25/182.51 inference(scs_inference,[],[3217,2261,944,255,11,14,24])).
% 182.25/182.51 cnf(3235,plain,
% 182.25/182.51 (P3(f9(f3(a4,a4),f6(a1)),f9(f9(a4,f3(a4,a4)),f6(a1)))),
% 182.25/182.51 inference(scs_inference,[],[2953,3217,2261,944,3065,255,11,14,24,30])).
% 182.25/182.51 cnf(3237,plain,
% 182.25/182.51 (P2(f3(a1,a1),f3(f3(a5,f3(a1,a1)),a1))),
% 182.25/182.51 inference(scs_inference,[],[1,2953,3217,2261,944,3065,255,11,14,24,30,31])).
% 182.25/182.51 cnf(3255,plain,
% 182.25/182.51 (~P2(f3(a5,a1),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[2313,2463,809,2010,11,14,24])).
% 182.25/182.51 cnf(3257,plain,
% 182.25/182.51 (P3(f9(f3(a1,a4),a1),f9(a4,a1))),
% 182.25/182.51 inference(scs_inference,[],[1,2313,2616,2463,809,2010,11,14,24,30])).
% 182.25/182.51 cnf(3261,plain,
% 182.25/182.51 (P3(f3(f3(a1,a4),a1),f3(a4,a1))),
% 182.25/182.51 inference(scs_inference,[],[1,2313,2616,2206,2463,809,2010,11,14,24,30,31,29])).
% 182.25/182.51 cnf(3263,plain,
% 182.25/182.51 (P2(f3(a1,f3(a1,a1)),a5)),
% 182.25/182.51 inference(scs_inference,[],[1,2313,2616,2206,2500,2463,2517,809,2010,11,14,24,30,31,29,23])).
% 182.25/182.51 cnf(3275,plain,
% 182.25/182.51 (P3(f3(a4,a1),f3(f3(a1,a4),a1))),
% 182.25/182.51 inference(scs_inference,[],[3261,792,11,14])).
% 182.25/182.51 cnf(3279,plain,
% 182.25/182.51 (P3(f9(f3(f3(a1,a4),a1),f6(a1)),f9(f3(a4,a1),f6(a1)))),
% 182.25/182.51 inference(scs_inference,[],[3261,3233,792,2030,3065,11,14,24,30])).
% 182.25/182.51 cnf(3299,plain,
% 182.25/182.51 (P3(f9(f9(a4,a2),a1),f9(a2,a1))),
% 182.25/182.51 inference(scs_inference,[],[1,3257,2709,2449,427,255,11,14,24,30])).
% 182.25/182.51 cnf(3305,plain,
% 182.25/182.51 (P2(a1,f3(f3(a5,f3(a1,a1)),a1))),
% 182.25/182.51 inference(scs_inference,[],[1,3257,3263,3237,2709,2449,427,2406,255,11,14,24,30,31,29,23])).
% 182.25/182.51 cnf(3313,plain,
% 182.25/182.51 (P1(f6(a4))),
% 182.25/182.51 inference(scs_inference,[],[2,11])).
% 182.25/182.51 cnf(3315,plain,
% 182.25/182.51 (P3(f9(a2,a1),f9(f9(a4,a2),a1))),
% 182.25/182.51 inference(scs_inference,[],[2,3299,11,14])).
% 182.25/182.51 cnf(3321,plain,
% 182.25/182.51 (P3(f3(f9(f9(a4,a2),a1),f3(a7,a7)),f3(f9(a2,a1),f3(a7,a7)))),
% 182.25/182.51 inference(scs_inference,[],[2,3299,3305,2010,2200,11,14,24,30,29])).
% 182.25/182.51 cnf(3424,plain,
% 182.25/182.51 (P3(f9(f9(a5,a5),a5),f9(a5,f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2309,503,11,14])).
% 182.25/182.51 cnf(3426,plain,
% 182.25/182.51 (P3(f9(f3(a1,a7),a4),f9(a7,a4))),
% 182.25/182.51 inference(scs_inference,[],[2,2309,2180,503,11,14,30])).
% 182.25/182.51 cnf(3430,plain,
% 182.25/182.51 (P3(f3(f3(a1,a7),a4),f3(a7,a4))),
% 182.25/182.51 inference(scs_inference,[],[2,2309,2180,2911,503,11,14,30,31,29])).
% 182.25/182.51 cnf(3442,plain,
% 182.25/182.51 (P3(f3(a7,a4),f3(f3(a1,a7),a4))),
% 182.25/182.51 inference(scs_inference,[],[3430,795,11,14])).
% 182.25/182.51 cnf(3448,plain,
% 182.25/182.51 (~P3(a7,f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[3430,2863,3313,63,795,11,14,30,29,23])).
% 182.25/182.51 cnf(3459,plain,
% 182.25/182.51 (P3(f9(a7,a4),f9(f3(a1,a7),a4))),
% 182.25/182.51 inference(scs_inference,[],[3426,819,11,14])).
% 182.25/182.51 cnf(3461,plain,
% 182.25/182.51 (P3(f9(f3(a1,a2),a4),f9(a2,a4))),
% 182.25/182.51 inference(scs_inference,[],[2,3426,2511,819,11,14,30])).
% 182.25/182.51 cnf(3463,plain,
% 182.25/182.51 (P3(f3(f3(a1,a2),a4),f3(a2,a4))),
% 182.25/182.51 inference(scs_inference,[],[2,3426,2511,819,11,14,30,29])).
% 182.25/182.51 cnf(3467,plain,
% 182.25/182.51 (~P3(f3(a1,a7),f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2,3426,2925,3448,2511,3077,2233,819,11,14,30,29,23,21])).
% 182.25/182.51 cnf(3475,plain,
% 182.25/182.51 (P3(f3(a2,a4),f3(f3(a1,a2),a4))),
% 182.25/182.51 inference(scs_inference,[],[3463,806,11,14])).
% 182.25/182.51 cnf(3493,plain,
% 182.25/182.51 (P1(f6(f3(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[2418,11])).
% 182.25/182.51 cnf(3495,plain,
% 182.25/182.51 (P3(f9(a2,a4),f9(f3(a1,a2),a4))),
% 182.25/182.51 inference(scs_inference,[],[3461,2418,11,14])).
% 182.25/182.51 cnf(3497,plain,
% 182.25/182.51 (P3(f9(f9(a4,a4),a4),f9(a4,a4))),
% 182.25/182.51 inference(scs_inference,[],[2,3461,2612,2418,11,14,30])).
% 182.25/182.51 cnf(3499,plain,
% 182.25/182.51 (P3(f3(f9(a4,a4),a4),f3(a4,a4))),
% 182.25/182.51 inference(scs_inference,[],[2,3461,2612,2418,11,14,30,29])).
% 182.25/182.51 cnf(3501,plain,
% 182.25/182.51 (P2(f9(a4,a7),f9(f9(a2,a2),f9(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[2,3461,2612,2917,2285,2418,11,14,30,29,23])).
% 182.25/182.51 cnf(3511,plain,
% 182.25/182.51 (P3(f9(a4,a4),f9(f9(a4,a4),a4))),
% 182.25/182.51 inference(scs_inference,[],[3497,14])).
% 182.25/182.51 cnf(3515,plain,
% 182.25/182.51 (P3(f9(f9(f9(a4,a4),a4),f6(a4)),f9(f9(a4,a4),f6(a4)))),
% 182.25/182.51 inference(scs_inference,[],[3497,3493,3313,14,11,30])).
% 182.25/182.51 cnf(3527,plain,
% 182.25/182.51 (P3(f3(a4,a4),f3(f9(a4,a4),a4))),
% 182.25/182.51 inference(scs_inference,[],[3499,14])).
% 182.25/182.51 cnf(3529,plain,
% 182.25/182.51 (P1(f6(a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3499,14,11])).
% 182.25/182.51 cnf(3537,plain,
% 182.25/182.51 (~P3(f3(a2,a5),f3(a5,a5))),
% 182.25/182.51 inference(scs_inference,[],[3,3499,2719,2667,3025,184,14,11,31,30,29,21])).
% 182.25/182.51 cnf(3539,plain,
% 182.25/182.51 (~P3(f3(a5,a5),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3499,2719,2667,3025,184,14,11,31,30,29,21,195])).
% 182.25/182.51 cnf(3562,plain,
% 182.25/182.51 (P3(f3(a7,f6(a2)),f3(f3(a5,a2),f6(a2)))),
% 182.25/182.51 inference(scs_inference,[],[3529,2013])).
% 182.25/182.51 cnf(3569,plain,
% 182.25/182.51 (P1(f6(f6(a2)))),
% 182.25/182.51 inference(scs_inference,[],[3529,2352,14,11])).
% 182.25/182.51 cnf(3575,plain,
% 182.25/182.51 (~P3(f9(a4,f3(a5,a5)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[3539,3529,3511,2941,2352,14,11,30,29,21])).
% 182.25/182.51 cnf(3588,plain,
% 182.25/182.51 (P3(f9(f3(a1,a5),a2),f9(f9(a4,a5),a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3569,2393,2620,14,11,30])).
% 182.25/182.51 cnf(3590,plain,
% 182.25/182.51 (P3(f3(f3(a1,a5),a2),f3(f9(a4,a5),a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3569,2393,2620,14,11,30,29])).
% 182.25/182.51 cnf(3594,plain,
% 182.25/182.51 (~P3(f9(a5,a5),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3569,2393,2665,2620,184,14,11,30,29,21,195])).
% 182.25/182.51 cnf(3598,plain,
% 182.25/182.51 (P2(f9(a4,a5),f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[3,3575,3569,2393,2665,2620,2959,184,14,11,30,29,21,195,22,23])).
% 182.25/182.51 cnf(3605,plain,
% 182.25/182.51 (P1(f6(a7))),
% 182.25/182.51 inference(scs_inference,[],[3164,5,14,11])).
% 182.25/182.51 cnf(3609,plain,
% 182.25/182.51 (P2(f3(a7,a5),f3(a5,a5))),
% 182.25/182.51 inference(scs_inference,[],[3164,2153,2566,5,14,11,27,24])).
% 182.25/182.51 cnf(3611,plain,
% 182.25/182.51 (P1(f9(f6(a7),f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[3164,2153,2566,5,14,11,27,24,19])).
% 182.25/182.51 cnf(3615,plain,
% 182.25/182.51 (P3(f9(f9(a2,a2),f6(a2)),f9(f9(a4,f9(a2,a2)),f6(a2)))),
% 182.25/182.51 inference(scs_inference,[],[3598,2969,3164,2153,3529,2566,5,14,11,27,24,19,31,30])).
% 182.25/182.51 cnf(3619,plain,
% 182.25/182.51 (P1(f3(f6(a7),f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[3598,2969,3164,2153,3529,2566,5,14,11,27,24,19,31,30,29,18])).
% 182.25/182.51 cnf(3621,plain,
% 182.25/182.51 (~P3(f3(a1,f3(a5,a5)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[3598,2969,2825,3164,3539,2153,3529,2566,5,14,11,27,24,19,31,30,29,18,21])).
% 182.25/182.51 cnf(3623,plain,
% 182.25/182.51 (P3(f3(a1,f6(a7)),f6(a7))),
% 182.25/182.51 inference(scs_inference,[],[3598,2969,2825,3164,3539,2153,3529,2566,5,14,11,27,24,19,31,30,29,18,21,16])).
% 182.25/182.51 cnf(3625,plain,
% 182.25/182.51 (P3(f9(a4,f6(a7)),f6(a7))),
% 182.25/182.51 inference(scs_inference,[],[3598,2969,2825,3164,3539,2153,3529,2566,5,14,11,27,24,19,31,30,29,18,21,16,17])).
% 182.25/182.51 cnf(3633,plain,
% 182.25/182.51 (P3(f6(a7),f3(a1,f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[3623,14])).
% 182.25/182.51 cnf(3635,plain,
% 182.25/182.51 (P1(f6(f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[3605,3623,14,11])).
% 182.25/182.51 cnf(3639,plain,
% 182.25/182.51 (P3(f9(a1,a2),f9(f3(a1,a1),a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3609,3605,3623,2443,14,11,31,30])).
% 182.25/182.51 cnf(3641,plain,
% 182.25/182.51 (P3(f3(a1,a2),f3(f3(a1,a1),a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3609,3605,3623,2443,14,11,31,30,29])).
% 182.25/182.51 cnf(3643,plain,
% 182.25/182.51 (~P3(f9(a4,f9(a5,a5)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3594,3609,3605,3623,2443,2925,14,11,31,30,29,21])).
% 182.25/182.51 cnf(3652,plain,
% 182.25/182.51 (P3(f6(a7),f9(a4,f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[3625,14])).
% 182.25/182.51 cnf(3656,plain,
% 182.25/182.51 (P2(f3(a7,a5),f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[3625,3611,3609,2842,14,11,24])).
% 182.25/182.51 cnf(3658,plain,
% 182.25/182.51 (P3(f9(f9(a4,f6(a7)),f6(a7)),f9(f6(a7),f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[3625,3611,3609,3605,2842,14,11,24,30])).
% 182.25/182.51 cnf(3662,plain,
% 182.25/182.51 (P3(f9(a4,f6(a7)),f3(a1,f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[3625,3611,3633,3609,3605,2842,14,11,24,30,29,21])).
% 182.25/182.51 cnf(3668,plain,
% 182.25/182.51 (P3(f3(f3(a1,a1),a2),f3(a1,a2))),
% 182.25/182.51 inference(scs_inference,[],[3641,14])).
% 182.25/182.51 cnf(3674,plain,
% 182.25/182.51 (P3(f9(a5,a2),f9(f9(a4,a5),a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3656,3641,3619,2585,3605,14,11,31,30])).
% 182.25/182.51 cnf(3676,plain,
% 182.25/182.51 (P3(f3(a5,a2),f3(f9(a4,a5),a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3656,3641,3619,2585,3605,14,11,31,30,29])).
% 182.25/182.51 cnf(3678,plain,
% 182.25/182.51 (~P3(f3(a1,f9(a5,a5)),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3643,3656,3641,2929,3619,2585,3605,14,11,31,30,29,21])).
% 182.25/182.51 cnf(3684,plain,
% 182.25/182.51 (P3(f3(f9(a4,a5),a2),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[3676,14])).
% 182.25/182.51 cnf(3692,plain,
% 182.25/182.51 (P3(f3(f3(f3(a1,a1),a2),f6(a7)),f3(f3(a1,a2),f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[3,3668,3676,3635,2931,3605,14,11,31,30,29])).
% 182.25/182.51 cnf(3696,plain,
% 182.25/182.51 (P3(a7,f3(f9(a4,a5),a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3668,3676,3635,3641,2931,3605,14,11,31,30,29,21,146])).
% 182.25/182.51 cnf(3698,plain,
% 182.25/182.51 (P3(f3(f9(a4,a5),a2),a7)),
% 182.25/182.51 inference(scs_inference,[],[3,3668,3676,3635,3641,2931,3605,14,11,31,30,29,21,146,134])).
% 182.25/182.51 cnf(3704,plain,
% 182.25/182.51 (P3(f9(f3(a1,a1),a2),f9(a1,a2))),
% 182.25/182.51 inference(scs_inference,[],[3639,14])).
% 182.25/182.51 cnf(3706,plain,
% 182.25/182.51 (P1(f6(a5))),
% 182.25/182.51 inference(scs_inference,[],[3639,4,14,11])).
% 182.25/182.51 cnf(3712,plain,
% 182.25/182.51 (P2(f3(a7,f6(a7)),f3(a5,a5))),
% 182.25/182.51 inference(scs_inference,[],[3,3639,3696,3017,2694,4,14,11,30,29,23])).
% 182.25/182.51 cnf(3714,plain,
% 182.25/182.51 (~P3(f3(f9(a4,a5),a2),f3(a5,a1))),
% 182.25/182.51 inference(scs_inference,[],[3,3639,3696,2945,3676,3017,2694,4,14,11,30,29,23,21])).
% 182.25/182.51 cnf(3735,plain,
% 182.25/182.51 (P3(f3(a7,f6(a5)),f3(f3(a5,a2),f6(a5)))),
% 182.25/182.51 inference(scs_inference,[],[3706,1805])).
% 182.25/182.51 cnf(3745,plain,
% 182.25/182.51 (P3(f9(f9(a4,a5),a2),f9(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[3674,14])).
% 182.25/182.51 cnf(3747,plain,
% 182.25/182.51 (P1(f6(f6(a5)))),
% 182.25/182.51 inference(scs_inference,[],[3706,3674,14,11])).
% 182.25/182.51 cnf(3749,plain,
% 182.25/182.51 (~P2(f9(f9(a5,a5),f9(a5,a5)),a7)),
% 182.25/182.51 inference(scs_inference,[],[3706,3674,2243,10,14,11,24])).
% 182.25/182.51 cnf(3751,plain,
% 182.25/182.51 (P2(f3(f3(a1,a5),a2),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[3,3706,3674,2138,2243,10,14,11,24,31])).
% 182.25/182.51 cnf(3753,plain,
% 182.25/182.51 (P3(f9(f9(f3(a1,a1),a2),f6(a5)),f9(f9(a1,a2),f6(a5)))),
% 182.25/182.51 inference(scs_inference,[],[3,3706,3704,3674,2138,2243,10,14,11,24,31,30])).
% 182.25/182.51 cnf(3755,plain,
% 182.25/182.51 (P3(f3(f9(f3(a1,a1),a2),f6(a5)),f3(f9(a1,a2),f6(a5)))),
% 182.25/182.51 inference(scs_inference,[],[3,3706,3704,3674,2138,2243,10,14,11,24,31,30,29])).
% 182.25/182.51 cnf(3772,plain,
% 182.25/182.51 (~P3(f3(f9(a4,a5),a2),f9(a2,a2))),
% 182.25/182.51 inference(scs_inference,[],[3747,3113,2795,3676,14,11,21])).
% 182.25/182.51 cnf(3782,plain,
% 182.25/182.51 (P2(f3(f9(a4,a5),a2),a2)),
% 182.25/182.51 inference(scs_inference,[],[3,3712,3698,3747,3113,2795,291,3676,3696,3706,2842,14,11,21,24,31,30,29,23])).
% 182.25/182.51 cnf(3784,plain,
% 182.25/182.51 (P2(a7,f9(f9(a5,a5),f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[3,3712,3698,3747,3749,3113,2795,291,3676,3696,2556,3706,2842,5,14,11,21,24,31,30,29,23,15])).
% 182.25/182.51 cnf(3790,plain,
% 182.25/182.51 (P3(f3(f3(a1,a1),a1),f9(a4,f3(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[3021,14])).
% 182.25/182.51 cnf(3808,plain,
% 182.25/182.51 (P3(f3(a1,f3(a2,a2)),f9(a4,f3(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[2991,14])).
% 182.25/182.51 cnf(3812,plain,
% 182.25/182.51 (P2(f3(f3(a1,a5),a2),a2)),
% 182.25/182.51 inference(scs_inference,[],[3772,2991,3751,3698,2072,14,21,24])).
% 182.25/182.51 cnf(3814,plain,
% 182.25/182.51 (P2(f3(f3(f9(a4,a5),a2),a5),f3(a2,a5))),
% 182.25/182.51 inference(scs_inference,[],[4,3772,3782,2991,3751,3698,2072,14,21,24,31])).
% 182.25/182.51 cnf(3816,plain,
% 182.25/182.51 (P3(f9(f3(a7,f6(a7)),a5),f9(a1,a5))),
% 182.25/182.51 inference(scs_inference,[],[4,3772,3782,2991,2184,3751,3698,2072,14,21,24,31,30])).
% 182.25/182.51 cnf(3818,plain,
% 182.25/182.51 (P3(f3(f3(a7,f6(a7)),a5),f3(a1,a5))),
% 182.25/182.51 inference(scs_inference,[],[4,3772,3782,2991,2184,3751,3698,2072,14,21,24,31,30,29])).
% 182.25/182.51 cnf(3826,plain,
% 182.25/182.51 (P3(f3(a1,f3(a4,a4)),f9(a4,f3(a4,a4)))),
% 182.25/182.51 inference(scs_inference,[],[2957,14])).
% 182.25/182.51 cnf(3828,plain,
% 182.25/182.51 (P3(f9(a7,a4),f9(a7,a4))),
% 182.25/182.51 inference(scs_inference,[],[3459,2957,3426,14,21])).
% 182.25/182.51 cnf(3832,plain,
% 182.25/182.51 (P2(f3(f3(f3(a1,a5),a2),a5),f3(a2,a5))),
% 182.25/182.51 inference(scs_inference,[],[4,3459,3812,2957,2846,3426,3751,14,21,24,31])).
% 182.25/182.51 cnf(3834,plain,
% 182.25/182.51 (P3(f9(f9(a2,a2),f6(a5)),f9(f3(a1,f9(a2,a2)),f6(a5)))),
% 182.25/182.51 inference(scs_inference,[],[4,2857,3459,3812,2957,2846,3426,3751,3706,14,21,24,31,30])).
% 182.25/182.51 cnf(3838,plain,
% 182.25/182.51 (~P3(f3(f3(f9(a4,a5),a2),a5),a5)),
% 182.25/182.51 inference(scs_inference,[],[4,2857,3459,3812,2957,3814,2609,2846,3426,3751,3706,14,21,24,31,30,29,23])).
% 182.25/182.51 cnf(3849,plain,
% 182.25/182.51 (P2(f3(f3(f3(a1,a5),a2),a5),a5)),
% 182.25/182.51 inference(scs_inference,[],[2896,3832,3838,2513,286,14,21,24])).
% 182.25/182.51 cnf(3855,plain,
% 182.25/182.51 (P2(f9(a4,f3(a1,a1)),f3(a5,a5))),
% 182.25/182.51 inference(scs_inference,[],[4,3828,2896,3832,3838,3790,2513,2764,286,14,21,24,30,29,23])).
% 182.25/182.51 cnf(3857,plain,
% 182.25/182.51 (P3(a5,a1)+P1(f8(a5))),
% 182.25/182.51 inference(scs_inference,[],[4,3828,2896,3832,3838,3790,2513,2764,286,14,21,24,30,29,23,13])).
% 182.25/182.51 cnf(3873,plain,
% 182.25/182.51 (~P3(f3(f3(f3(a1,a5),a2),a5),a5)),
% 182.25/182.51 inference(scs_inference,[],[3855,3275,3495,2465,2641,2303,3461,3832,3751,3529,14,21,24,31,30,29,23])).
% 182.25/182.51 cnf(3879,plain,
% 182.25/182.51 (P3(f9(a7,f9(a2,a2)),f9(f3(a2,a5),f9(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[2752,14])).
% 182.25/182.51 cnf(3885,plain,
% 182.25/182.51 (~P2(a5,f3(f3(f3(a1,a5),a2),a5))),
% 182.25/182.51 inference(scs_inference,[],[2752,3849,3873,2513,2566,14,21,24,22])).
% 182.25/182.51 cnf(3906,plain,
% 182.25/182.51 (P3(f9(f3(a4,a4),f6(a7)),f9(f3(f9(a4,a4),a4),f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[3527,3808,2797,3885,2991,2566,3605,14,21,24,30])).
% 182.25/182.51 cnf(3917,plain,
% 182.25/182.51 (P3(f3(a1,f6(a7)),f9(a4,f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[3662,14])).
% 182.25/182.51 cnf(3919,plain,
% 182.25/182.51 (~P3(f3(f9(a4,a5),a2),f9(a1,a1))),
% 182.25/182.51 inference(scs_inference,[],[3662,2827,3676,14,21])).
% 182.25/182.51 cnf(3923,plain,
% 182.25/182.51 (~P2(a5,f3(f3(f9(a4,a5),a2),a5))),
% 182.25/182.51 inference(scs_inference,[],[3662,2827,3814,3838,3676,286,14,21,24,22])).
% 182.25/182.51 cnf(3927,plain,
% 182.25/182.51 (P3(f3(f9(a7,f8(a7)),a5),f3(a4,a5))),
% 182.25/182.51 inference(scs_inference,[],[4,3662,2827,2196,3814,3838,3676,286,14,21,24,22,30,29])).
% 182.25/182.51 cnf(3945,plain,
% 182.25/182.51 (~P3(f3(f3(a1,a5),a2),f3(a5,a1))),
% 182.25/182.51 inference(scs_inference,[],[3475,3826,2661,3923,2957,3255,3751,2566,3706,14,21,24,30,29,23])).
% 182.25/182.51 cnf(3951,plain,
% 182.25/182.51 (P3(f3(a7,f3(a4,a4)),f3(f3(a2,a5),f3(a4,a4)))),
% 182.25/182.51 inference(scs_inference,[],[2690,14])).
% 182.25/182.51 cnf(3953,plain,
% 182.25/182.51 (~P3(a7,f9(a1,a1))),
% 182.25/182.51 inference(scs_inference,[],[3919,2690,3698,14,21])).
% 182.25/182.51 cnf(3969,plain,
% 182.25/182.51 (P3(f3(a7,f9(a2,a2)),f3(f3(a2,a5),f9(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[2758,14])).
% 182.25/182.51 cnf(3991,plain,
% 182.25/182.51 (P2(f3(a7,a4),f3(a5,f8(a4)))),
% 182.25/182.51 inference(scs_inference,[],[2653,3007,3005,1875,3676,14,21,24])).
% 182.25/182.51 cnf(3999,plain,
% 182.25/182.51 (P2(f3(a5,f6(a5)),f9(f9(a1,a1),f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[5,2653,3007,2408,3067,3784,2375,3005,1875,3676,14,21,24,31,30,29,23])).
% 182.25/182.51 cnf(4034,plain,
% 182.25/182.51 (P3(f3(f3(a4,f6(a4)),a7),f3(a1,a7))),
% 182.25/182.51 inference(scs_inference,[],[5,2787,2913,2618,3812,1858,3005,3676,14,21,24,31,30,29])).
% 182.25/182.51 cnf(4060,plain,
% 182.25/182.51 (P3(f9(a7,f3(a4,a4)),f9(f3(a2,a5),f3(a4,a4)))),
% 182.25/182.51 inference(scs_inference,[],[2848,14])).
% 182.25/182.51 cnf(4062,plain,
% 182.25/182.51 (~P3(f3(f9(a4,a5),a2),f9(f9(a1,a1),f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[2848,3201,3676,14,21])).
% 182.25/182.51 cnf(4093,plain,
% 182.25/182.51 (~P3(a7,f9(f9(a1,a1),f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[4062,2987,3698,14,21])).
% 182.25/182.51 cnf(4095,plain,
% 182.25/182.51 (~P2(f9(a2,a1),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[4062,2987,330,3698,2010,14,21,24])).
% 182.25/182.51 cnf(4107,plain,
% 182.25/182.51 (~P3(f3(a5,a2),f9(a2,a1))),
% 182.25/182.51 inference(scs_inference,[],[4095,3424,2995,2309,2034,14,21,23])).
% 182.25/182.51 cnf(4110,plain,
% 182.25/182.51 (~P3(f9(a2,a1),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[4095,3424,2995,2309,2034,14,21,23,2109,195])).
% 182.25/182.51 cnf(4119,plain,
% 182.25/182.51 (~P3(f9(f9(a4,a2),a1),f3(a5,a2))),
% 182.25/182.51 inference(scs_inference,[],[4110,2587,3315,14,21])).
% 182.25/182.51 cnf(4126,plain,
% 182.25/182.51 (P3(f3(f3(a1,a2),f3(a5,a5)),f3(a2,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[2593,14])).
% 182.25/182.51 cnf(4130,plain,
% 182.25/182.51 (~P2(f9(a5,a5),f3(a2,a5))),
% 182.25/182.51 inference(scs_inference,[],[3191,2593,2212,2198,255,14,21,24])).
% 182.25/182.51 cnf(4142,plain,
% 182.25/182.51 (P3(a1,a5)+P1(f8(a5))),
% 182.25/182.51 inference(scs_inference,[],[3857,14])).
% 182.25/182.51 cnf(4147,plain,
% 182.25/182.51 (~P3(f3(f9(a4,a5),a2),f9(a2,a1))),
% 182.25/182.51 inference(scs_inference,[],[3588,4107,2482,2488,3676,14,23,21])).
% 182.25/182.51 cnf(4190,plain,
% 182.25/182.51 (P2(f6(a5),f9(f9(a1,a1),f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[3917,3927,4130,3662,3999,1569,3832,14,23,21,24])).
% 182.25/182.51 cnf(4235,plain,
% 182.25/182.51 (P3(f3(a1,a7),f3(f3(a4,f6(a4)),a7))),
% 182.25/182.51 inference(scs_inference,[],[4034,14])).
% 182.25/182.51 cnf(4237,plain,
% 182.25/182.51 (~P3(f3(f3(f9(a4,a5),a2),a5),f3(a5,a5))),
% 182.25/182.51 inference(scs_inference,[],[4034,2700,3814,14,23])).
% 182.25/182.51 cnf(4241,plain,
% 182.25/182.51 (P2(f3(a5,a2),f3(a5,a5))),
% 182.25/182.51 inference(scs_inference,[],[3879,4034,2752,2694,2700,2067,3814,14,23,21,24])).
% 182.25/182.51 cnf(4274,plain,
% 182.25/182.51 (P3(f3(a1,a1),f3(f3(a5,f6(a5)),a1))),
% 182.25/182.51 inference(scs_inference,[],[3075,14])).
% 182.25/182.51 cnf(4288,plain,
% 182.25/182.51 (P3(f3(a1,a5),f3(f3(a7,f6(a7)),a5))),
% 182.25/182.51 inference(scs_inference,[],[3818,14])).
% 182.25/182.51 cnf(4292,plain,
% 182.25/182.51 (P2(f3(a5,a2),f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[3951,3818,2690,4241,2842,14,21,24])).
% 182.25/182.51 cnf(4305,plain,
% 182.25/182.51 (~P2(f9(a2,a2),f3(a2,a5))),
% 182.25/182.51 inference(scs_inference,[],[35,4292,3816,2854,2414,184,255,14,23,21,24])).
% 182.25/182.51 cnf(4316,plain,
% 182.25/182.51 (P2(f3(a5,a2),f9(f9(a5,a5),f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[3969,3059,2758,2243,2067,14,21,24])).
% 182.25/182.51 cnf(4342,plain,
% 182.25/182.51 (P2(a7,f9(f9(a1,a1),f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[4060,3321,4305,2848,2375,276,149,14,23,21,24])).
% 182.25/182.51 cnf(4354,plain,
% 182.25/182.51 (~P3(f9(f3(a5,a1),f3(a5,a1)),f3(a2,a5))),
% 182.25/182.51 inference(scs_inference,[],[3658,4235,3221,2202,1801,14,23,21])).
% 182.25/182.51 cnf(4360,plain,
% 182.25/182.51 (P2(f3(a5,a2),f9(f9(a1,a1),f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[4093,4342,3658,4235,3221,2202,4316,2008,1801,14,23,21,22,1775,24])).
% 182.25/182.51 cnf(4378,plain,
% 182.25/182.51 (~P3(f9(f3(a5,a1),f3(a5,a1)),a7)),
% 182.25/182.51 inference(scs_inference,[],[3156,4354,4360,148,184,14,23,21])).
% 182.25/182.51 cnf(4398,plain,
% 182.25/182.51 (~P3(f9(f3(a5,a1),f3(a5,a1)),f9(a4,a7))),
% 182.25/182.51 inference(scs_inference,[],[4378,3235,2182,3991,3442,14,23,21])).
% 182.25/182.51 cnf(4414,plain,
% 182.25/182.51 (P2(f3(f3(a5,f6(a5)),a1),a5)),
% 182.25/182.51 inference(scs_inference,[],[3515,4274,2500,14,23])).
% 182.25/182.51 cnf(4418,plain,
% 182.25/182.51 (P2(f3(a5,a2),f9(f9(a2,a2),f9(a2,a2)))),
% 182.25/182.51 inference(scs_inference,[],[4398,3515,4274,2328,2500,2449,2067,14,23,21,24])).
% 182.25/182.51 cnf(4464,plain,
% 182.25/182.51 (~P3(f3(f9(a4,a5),a2),f3(a5,f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[3615,4288,3111,2523,3676,14,23,21])).
% 182.25/182.51 cnf(4486,plain,
% 182.25/182.51 (~P3(a7,f3(a5,f9(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[4464,3834,3698,14,21])).
% 182.25/182.51 cnf(4523,plain,
% 182.25/182.51 (~P3(f3(a5,a2),a2)),
% 182.25/182.51 inference(scs_inference,[],[4126,3692,2593,2490,1778,2010,6,14,21,24,13,23])).
% 182.25/182.51 cnf(4534,plain,
% 182.25/182.51 (~P3(f3(f9(a4,a5),a2),a2)),
% 182.25/182.51 inference(scs_inference,[],[4523,3753,4288,2138,3676,14,23,21])).
% 182.25/182.51 cnf(4536,plain,
% 182.25/182.51 (~P2(a2,f3(f9(a4,a5),a2))),
% 182.25/182.51 inference(scs_inference,[],[4523,3753,4288,3782,2138,3676,14,23,21,22])).
% 182.25/182.51 cnf(4544,plain,
% 182.25/182.51 (~P2(f3(a1,a2),f3(f9(a4,a5),a2))),
% 182.25/182.51 inference(scs_inference,[],[4536,3755,2511,14,23])).
% 182.25/182.51 cnf(4558,plain,
% 182.25/182.51 (~P3(a7,a2)),
% 182.25/182.51 inference(scs_inference,[],[44,4534,3562,3906,1264,3698,3706,14,23,30,21])).
% 182.25/182.51 cnf(4618,plain,
% 182.25/182.51 (P2(a1,f9(f9(f3(a5,a5),f3(a5,a5)),f9(f3(a5,a5),f3(a5,a5))))),
% 182.25/182.51 inference(scs_inference,[],[3279,2684,1489,948,2457,2704,672,439,12,16,17,20,14,11,28,26])).
% 182.25/182.51 cnf(4658,plain,
% 182.25/182.51 (P3(f9(f3(a1,a7),a4),f9(f3(a5,a2),a4))),
% 182.25/182.51 inference(scs_inference,[],[3684,4316,3083,3426,3953,14,186,195,192,146,219])).
% 182.25/182.51 cnf(4662,plain,
% 182.25/182.51 (P2(a5,f3(a5,f3(a5,a5)))),
% 182.25/182.51 inference(scs_inference,[],[3684,2842,2566,4316,3828,3083,3426,3953,14,186,195,192,146,219,222,24])).
% 182.25/182.51 cnf(4668,plain,
% 182.25/182.51 (~P2(a5,a2)),
% 182.25/182.51 inference(scs_inference,[],[4,1777,3684,2842,2566,4316,2700,3828,3083,3426,3953,4237,14,186,195,192,146,219,222,24,21,29,31])).
% 182.25/182.51 cnf(4674,plain,
% 182.25/182.51 (~P2(a5,a1)),
% 182.25/182.51 inference(scs_inference,[],[3,4,1777,3684,2842,3676,2566,2067,4316,2700,3828,3083,3426,3953,4237,14,186,195,192,146,219,222,24,21,29,31,23,15,73])).
% 182.25/182.51 cnf(4701,plain,
% 182.25/182.51 (P3(f9(f3(a5,a2),a4),f9(f3(a1,a7),a4))),
% 182.25/182.51 inference(scs_inference,[],[1927,950,1220,4418,3426,3133,4486,1568,14,481,186,724,683,781,597,146,1445,222])).
% 182.25/182.51 cnf(4753,plain,
% 182.25/182.51 (P2(f3(a2,f6(a2)),a2)),
% 182.25/182.51 inference(scs_inference,[],[6,4,3,2010,3751,3698,3049,1569,4241,1785,1901,3643,4544,1525,1544,4558,3537,14,186,724,683,781,597,146,1445,24,22,21,29,31,23])).
% 182.25/182.51 cnf(4819,plain,
% 182.25/182.51 (~P3(f3(f9(a4,a5),a2),a1)),
% 182.25/182.51 inference(scs_inference,[],[4,278,2186,2295,3467,3838,4190,1531,14,683,597,24,22,21,29])).
% 182.25/182.51 cnf(4873,plain,
% 182.25/182.51 (~P3(f3(a5,a2),f3(a1,a2))),
% 182.25/182.51 inference(scs_inference,[],[2511,4147,4523,1482,14,22,21])).
% 182.25/182.51 cnf(4879,plain,
% 182.25/182.51 (~P3(a5,a1)),
% 182.25/182.51 inference(scs_inference,[],[7,3,159,2511,3017,2206,4147,4523,1482,14,22,21,23,24,29])).
% 182.25/182.51 cnf(4890,plain,
% 182.25/182.51 (P1(f8(a5))),
% 182.25/182.51 inference(scs_inference,[],[4879,3857])).
% 182.25/182.51 cnf(4897,plain,
% 182.25/182.51 (P3(f3(a1,a1),f3(a7,f6(a7)))),
% 182.25/182.51 inference(scs_inference,[],[7,2406,3017,3033,3873,1443,14,23,22,21])).
% 182.25/182.51 cnf(4899,plain,
% 182.25/182.51 (P2(a1,f3(a5,f9(a1,a1)))),
% 182.25/182.51 inference(scs_inference,[],[7,2406,3017,3033,3035,3873,2336,1443,14,23,22,21,24])).
% 182.25/182.51 cnf(4944,plain,
% 182.25/182.51 (P3(a1,f6(a1))),
% 182.25/182.51 inference(scs_inference,[],[3033,3087,2568,14,21])).
% 182.25/182.51 cnf(4971,plain,
% 182.25/182.51 (P2(f3(a1,f9(a4,f6(a2))),a2)),
% 182.25/182.51 inference(scs_inference,[],[1220,3261,4753,3501,2307,3275,3041,14,24,21,23,724,781])).
% 182.25/182.51 cnf(4984,plain,
% 182.25/182.51 (P2(f9(a4,a4),f3(a5,f8(a4)))),
% 182.25/182.51 inference(scs_inference,[],[278,3005,3430,2651,3442,3217,4398,14,21,24,23])).
% 182.25/182.51 cnf(5015,plain,
% 182.25/182.51 (~P3(a5,f3(a1,a1))),
% 182.25/182.51 inference(scs_inference,[],[3,278,112,3668,2285,2463,3678,4873,14,23,21,24,29])).
% 182.25/182.51 cnf(5048,plain,
% 182.25/182.51 (~P2(f3(a1,f6(a1)),f3(a2,a5))),
% 182.25/182.51 inference(scs_inference,[],[255,2408,3621,14,23])).
% 182.25/182.51 cnf(5224,plain,
% 182.25/182.51 (~P2(f3(a1,a5),a2)),
% 182.25/182.51 inference(scs_inference,[],[2186,4668,3772,14,23])).
% 182.25/182.51 cnf(5279,plain,
% 182.25/182.51 (~P3(a1,f9(a4,a4))),
% 182.25/182.51 inference(scs_inference,[],[255,9,2612,2711,3714,14,23,21])).
% 182.25/182.51 cnf(5298,plain,
% 182.25/182.51 (P2(f3(a2,a5),f9(f9(f3(a5,a5),f3(a5,a5)),f9(f3(a5,a5),f3(a5,a5))))),
% 182.25/182.51 inference(scs_inference,[],[278,3497,3511,3945,4984,4618,5279,14,23,21,24])).
% 182.25/182.51 cnf(5322,plain,
% 182.25/182.51 (P2(f6(a7),f6(a7))),
% 182.25/182.51 inference(scs_inference,[],[1735,112,3605,3035,3704,2686,3639,4984,4119,5224,5298,14,23,21,24,22,640,526,15])).
% 182.25/182.51 cnf(5326,plain,
% 182.25/182.51 (P1(f8(f9(a4,a4)))),
% 182.25/182.51 inference(scs_inference,[],[5279,14,2673])).
% 182.25/182.51 cnf(5337,plain,
% 182.25/182.51 (P2(f6(a5),f6(a5))),
% 182.25/182.51 inference(scs_inference,[],[1927,3706,4668,3077,3745,3674,3101,5279,4971,5048,14,2673,23,21,24,22,526,15])).
% 182.25/182.51 cnf(5347,plain,
% 182.25/182.51 (P2(f9(a4,f6(a7)),f6(a7))),
% 182.25/182.51 inference(scs_inference,[],[3652,3182,5322,5337,14,683,597,23])).
% 182.25/182.51 cnf(5361,plain,
% 182.25/182.51 (P2(f3(a1,f6(a7)),f6(a7))),
% 182.25/182.51 inference(scs_inference,[],[3662,4819,5347,14,23])).
% 182.25/182.51 cnf(5372,plain,
% 182.25/182.51 (P2(f3(f3(a5,a2),f6(a5)),f3(f3(a2,a5),f6(a5)))),
% 182.25/182.51 inference(scs_inference,[],[1393,3735,4062,14,23])).
% 182.25/182.51 cnf(5536,plain,
% 182.25/182.51 (~P3(a5,f3(f3(a5,f6(a5)),a1))),
% 182.25/182.51 inference(scs_inference,[],[3751,5015,3075,3590,4558,14,57,23,21])).
% 182.25/182.51 cnf(5574,plain,
% 182.25/182.51 (~P3(a1,a5)),
% 182.25/182.51 inference(scs_inference,[],[3,2261,1594,4873,3231,1498,14,23,21,29])).
% 182.25/182.51 cnf(5581,plain,
% 182.25/182.51 (P1(f8(a5))),
% 182.25/182.51 inference(scs_inference,[],[5574,4142])).
% 182.25/182.51 cnf(6088,plain,
% 182.25/182.51 (P1(f9(f8(a5),f8(a5)))),
% 182.25/182.51 inference(scs_inference,[],[5326,4890,28,12,27,16,17,20,19])).
% 182.25/182.51 cnf(6100,plain,
% 182.25/182.51 (P2(f3(a1,a5),f3(a2,a5))),
% 182.25/182.51 inference(scs_inference,[],[6,4,8,5326,4890,5372,28,12,27,16,17,20,19,18,30,11,1197,29,31])).
% 182.25/182.51 cnf(6108,plain,
% 182.25/182.51 (P3(f3(a7,f6(a7)),f3(a1,a1))),
% 182.25/182.51 inference(scs_inference,[],[6,4,8,4674,4658,4701,4897,5326,5536,4890,4414,5372,4662,28,12,27,16,17,20,19,18,30,11,1197,29,31,21,24,22,14])).
% 182.25/182.51 cnf(6144,plain,
% 182.25/182.51 ($false),
% 182.25/182.51 inference(scs_inference,[],[4,9,5361,6100,6108,4944,6088,5581,5224,4899,281,26,17,12,16,30,11,19,18,29,31,21,24]),
% 182.25/182.51 ['proof']).
% 182.25/182.51 % SZS output end Proof
% 182.25/182.51 % Total time :181.580000s
%------------------------------------------------------------------------------