%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD060-2 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n003.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:32 EDT 2024
% Result : Unsatisfiable 116.95s 117.06s
% Output : CNFRefutation 116.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : FLD060-2 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n003.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Jun 19 11:24:39 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.57/0.59 start to proof:theBenchmark
% 116.95/117.05 %-------------------------------------------
% 116.95/117.05 % File :CSE---1.7
% 116.95/117.05 % Problem :theBenchmark
% 116.95/117.05 % Transform :cnf
% 116.95/117.05 % Format :tptp:raw
% 116.95/117.05 % Command :java -jar mcs_scs.jar %d %s
% 116.95/117.05
% 116.95/117.05 % Result :Theorem 116.340000s
% 116.95/117.05 % Output :CNFRefutation 116.340000s
% 116.95/117.05 %-------------------------------------------
% 116.95/117.05 %--------------------------------------------------------------------------
% 116.95/117.05 % File : FLD060-2 : TPTP v8.2.0. Bugfixed v2.1.0.
% 116.95/117.05 % Domain : Field Theory (Ordered fields)
% 116.95/117.05 % Problem : If b greater or equal b, then 2b greater or equal 2a
% 116.95/117.05 % Version : [Dra93] axioms : Especial.
% 116.95/117.05 % Theorem formulation : Relational with glxx axiom set.
% 116.95/117.05 % English :
% 116.95/117.05
% 116.95/117.05 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 116.95/117.05 % Source : [Dra93]
% 116.95/117.05 % Names :
% 116.95/117.05
% 116.95/117.05 % Status : Unsatisfiable
% 116.95/117.05 % Rating : 0.25 v8.2.0, 0.29 v7.5.0, 0.33 v7.1.0, 0.67 v7.0.0, 0.50 v6.3.0, 0.43 v6.2.0, 0.33 v6.1.0, 0.43 v6.0.0, 0.29 v5.5.0, 0.38 v5.4.0, 0.30 v5.2.0, 0.20 v5.1.0, 0.36 v5.0.0, 0.43 v4.1.0, 0.25 v4.0.1, 0.40 v4.0.0, 0.43 v3.7.0, 0.29 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.60 v2.3.0, 0.67 v2.2.1, 1.00 v2.1.0
% 116.95/117.05 % Syntax : Number of clauses : 35 ( 11 unt; 3 nHn; 35 RR)
% 116.95/117.05 % Number of literals : 81 ( 0 equ; 45 neg)
% 116.95/117.05 % Maximal clause size : 4 ( 2 avg)
% 116.95/117.05 % Maximal term depth : 3 ( 1 avg)
% 116.95/117.05 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 116.95/117.05 % Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% 116.95/117.05 % Number of variables : 50 ( 0 sgn)
% 116.95/117.05 % SPC : CNF_UNS_RFO_NEQ_NHN
% 116.95/117.05
% 116.95/117.05 % Comments :
% 116.95/117.05 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 116.95/117.05 %--------------------------------------------------------------------------
% 116.95/117.05 include('Axioms/FLD001-0.ax').
% 116.95/117.05 %--------------------------------------------------------------------------
% 116.95/117.05 cnf(a_is_defined,hypothesis,
% 116.95/117.05 defined(a) ).
% 116.95/117.05
% 116.95/117.05 cnf(b_is_defined,hypothesis,
% 116.95/117.05 defined(b) ).
% 116.95/117.05
% 116.95/117.05 cnf(u_is_defined,hypothesis,
% 116.95/117.05 defined(u) ).
% 116.95/117.05
% 116.95/117.05 cnf(v_is_defined,hypothesis,
% 116.95/117.05 defined(v) ).
% 116.95/117.05
% 116.95/117.05 cnf(add_equals_u_5,negated_conjecture,
% 116.95/117.06 equalish(add(a,a),u) ).
% 116.95/117.06
% 116.95/117.06 cnf(add_equals_v_6,negated_conjecture,
% 116.95/117.06 equalish(add(b,b),v) ).
% 116.95/117.06
% 116.95/117.06 cnf(less_or_equal_7,negated_conjecture,
% 116.95/117.06 less_or_equal(a,b) ).
% 116.95/117.06
% 116.95/117.06 cnf(not_less_or_equal_8,negated_conjecture,
% 116.95/117.06 ~ less_or_equal(u,v) ).
% 116.95/117.06
% 116.95/117.06 %--------------------------------------------------------------------------
% 116.95/117.06 %-------------------------------------------
% 116.95/117.06 % Proof found
% 116.95/117.06 % SZS status Theorem for theBenchmark
% 116.95/117.06 % SZS output start Proof
% 116.95/117.06 %ClaNum:35(EqnAxiom:0)
% 116.95/117.06 %VarNum:128(SingletonVarNum:50)
% 116.95/117.06 %MaxLitNum:4
% 116.95/117.06 %MaxfuncDepth:2
% 116.95/117.06 %SharedTerms:19
% 116.95/117.06 %goalClause: 7 8 9 11
% 116.95/117.06 %singleGoalClaCount:4
% 116.95/117.06 [1]P1(a1)
% 116.95/117.06 [2]P1(a4)
% 116.95/117.06 [3]P1(a2)
% 116.95/117.06 [4]P1(a5)
% 116.95/117.06 [5]P1(a7)
% 116.95/117.06 [6]P1(a10)
% 116.95/117.06 [7]P2(a2,a5)
% 116.95/117.06 [10]~P3(a1,a4)
% 116.95/117.06 [11]~P2(a7,a10)
% 116.95/117.06 [8]P3(f3(a2,a2),a7)
% 116.95/117.06 [9]P3(f3(a5,a5),a10)
% 116.95/117.06 [13]~P1(x131)+P3(x131,x131)
% 116.95/117.06 [12]~P1(x121)+P1(f6(x121))
% 116.95/117.06 [17]~P1(x171)+P3(f3(a1,x171),x171)
% 116.95/117.06 [18]~P1(x181)+P3(f9(a4,x181),x181)
% 116.95/117.06 [21]~P1(x211)+P3(f3(x211,f6(x211)),a1)
% 116.95/117.06 [15]~P3(x152,x151)+P3(x151,x152)
% 116.95/117.06 [14]~P1(x141)+P3(x141,a1)+P1(f8(x141))
% 116.95/117.06 [26]~P1(x261)+P3(x261,a1)+P3(f9(x261,f8(x261)),a4)
% 116.95/117.06 [23]~P2(x232,x231)+~P2(x231,x232)+P3(x231,x232)
% 116.95/117.06 [19]~P1(x192)+~P1(x191)+P1(f3(x191,x192))
% 116.95/117.06 [20]~P1(x202)+~P1(x201)+P1(f9(x201,x202))
% 116.95/117.06 [27]~P2(a1,x272)+~P2(a1,x271)+P2(a1,f9(x271,x272))
% 116.95/117.06 [28]~P1(x282)+~P1(x281)+P3(f3(x281,x282),f3(x282,x281))
% 116.95/117.06 [29]~P1(x292)+~P1(x291)+P3(f9(x291,x292),f9(x292,x291))
% 116.95/117.06 [22]~P3(x221,x223)+P3(x221,x222)+~P3(x223,x222)
% 116.95/117.06 [24]~P2(x243,x242)+P2(x241,x242)+~P3(x243,x241)
% 116.95/117.06 [25]~P2(x251,x253)+P2(x251,x252)+~P2(x253,x252)
% 116.95/117.06 [30]~P1(x302)+~P3(x301,x303)+P3(f3(x301,x302),f3(x303,x302))
% 116.95/117.06 [31]~P1(x312)+~P3(x311,x313)+P3(f9(x311,x312),f9(x313,x312))
% 116.95/117.06 [32]~P1(x322)+~P2(x321,x323)+P2(f3(x321,x322),f3(x323,x322))
% 116.95/117.06 [16]P2(x162,x161)+~P1(x161)+~P1(x162)+P2(x161,x162)
% 116.95/117.06 [33]~P1(x333)+~P1(x332)+~P1(x331)+P3(f3(x331,f3(x332,x333)),f3(f3(x331,x332),x333))
% 116.95/117.06 [34]~P1(x343)+~P1(x342)+~P1(x341)+P3(f9(x341,f9(x342,x343)),f9(f9(x341,x342),x343))
% 116.95/117.06 [35]~P1(x353)+~P1(x352)+~P1(x351)+P3(f3(f9(x351,x352),f9(x353,x352)),f9(f3(x351,x353),x352))
% 116.95/117.06 %EqnAxiom
% 116.95/117.06
% 116.95/117.06 %-------------------------------------------
% 116.95/117.07 cnf(36,plain,
% 116.95/117.07 (~P3(a4,a1)),
% 116.95/117.07 inference(scs_inference,[],[10,15])).
% 116.95/117.07 cnf(38,plain,
% 116.95/117.07 (~P2(f3(a2,a2),a10)),
% 116.95/117.07 inference(scs_inference,[],[11,8,10,15,24])).
% 116.95/117.07 cnf(40,plain,
% 116.95/117.07 (P2(a1,a1)),
% 116.95/117.07 inference(scs_inference,[],[11,8,1,10,15,24,16])).
% 116.95/117.07 cnf(44,plain,
% 116.95/117.07 (~P2(x441,a2)+P2(x441,a5)),
% 116.95/117.07 inference(scs_inference,[],[7,11,8,1,10,15,24,16,23,25])).
% 116.95/117.07 cnf(46,plain,
% 116.95/117.07 (~P3(x461,f3(a2,a2))+P3(x461,a7)),
% 116.95/117.07 inference(scs_inference,[],[7,11,8,1,10,15,24,16,23,25,22])).
% 116.95/117.07 cnf(50,plain,
% 116.95/117.07 (P2(a4,a4)),
% 116.95/117.07 inference(scs_inference,[],[2,40,23,16])).
% 116.95/117.07 cnf(52,plain,
% 116.95/117.07 (~P2(f3(a5,a5),x521)+P2(a10,x521)),
% 116.95/117.07 inference(scs_inference,[],[9,2,40,23,16,24])).
% 116.95/117.07 cnf(59,plain,
% 116.95/117.07 (P2(a2,a2)),
% 116.95/117.07 inference(scs_inference,[],[3,50,23,16])).
% 116.95/117.07 cnf(61,plain,
% 116.95/117.07 (~P3(x611,f3(a5,a5))+P3(x611,a10)),
% 116.95/117.07 inference(scs_inference,[],[9,3,50,23,16,22])).
% 116.95/117.07 cnf(67,plain,
% 116.95/117.07 (P2(a5,a5)),
% 116.95/117.07 inference(scs_inference,[],[4,59,23,16])).
% 116.95/117.07 cnf(71,plain,
% 116.95/117.07 (P2(a7,a7)),
% 116.95/117.07 inference(scs_inference,[],[67,5,23,16])).
% 116.95/117.07 cnf(75,plain,
% 116.95/117.07 (P2(a10,a10)),
% 116.95/117.07 inference(scs_inference,[],[71,6,23,16])).
% 116.95/117.07 cnf(86,plain,
% 116.95/117.07 (P2(f3(a2,a2),f3(a5,a2))),
% 116.95/117.07 inference(scs_inference,[],[59,3,44,32])).
% 116.95/117.07 cnf(87,plain,
% 116.95/117.07 (P2(a7,f3(a5,a2))),
% 116.95/117.07 inference(scs_inference,[],[8,86,24])).
% 116.95/117.07 cnf(89,plain,
% 116.95/117.07 (~P2(x891,f3(a2,a2))+P2(x891,f3(a5,a2))),
% 116.95/117.07 inference(scs_inference,[],[8,86,24,25])).
% 116.95/117.07 cnf(113,plain,
% 116.95/117.07 (P3(f9(a4,f6(a1)),f6(a1))),
% 116.95/117.07 inference(scs_inference,[],[1,18,12])).
% 116.95/117.07 cnf(114,plain,
% 116.95/117.07 (~P2(f9(a4,f6(a1)),x1141)+P2(f6(a1),x1141)),
% 116.95/117.07 inference(scs_inference,[],[113,24])).
% 116.95/117.07 cnf(119,plain,
% 116.95/117.07 (P3(f3(f6(a1),f6(f6(a1))),a1)),
% 116.95/117.07 inference(scs_inference,[],[1,21,12])).
% 116.95/117.07 cnf(129,plain,
% 116.95/117.07 (~P3(x1291,f9(a4,f6(a1)))+P3(x1291,f6(a1))),
% 116.95/117.07 inference(scs_inference,[],[113,22])).
% 116.95/117.07 cnf(134,plain,
% 116.95/117.07 (P3(a7,x1341)+~P3(x1341,f3(a2,a2))),
% 116.95/117.07 inference(scs_inference,[],[46,15])).
% 116.95/117.07 cnf(135,plain,
% 116.95/117.07 (P2(a10,f3(a5,a5))),
% 116.95/117.07 inference(scs_inference,[],[67,4,52,32])).
% 116.95/117.07 cnf(142,plain,
% 116.95/117.07 (P3(a10,x1421)+~P3(x1421,f3(a5,a5))),
% 116.95/117.07 inference(scs_inference,[],[61,15])).
% 116.95/117.07 cnf(147,plain,
% 116.95/117.07 (P3(a10,f3(a5,a5))),
% 116.95/117.07 inference(scs_inference,[],[4,142,28])).
% 116.95/117.07 cnf(148,plain,
% 116.95/117.07 (P2(f3(a5,a5),f3(a5,a5))),
% 116.95/117.07 inference(scs_inference,[],[135,147,24])).
% 116.95/117.07 cnf(153,plain,
% 116.95/117.07 (~P1(f3(a2,a2))+P2(a10,f3(a5,a2))),
% 116.95/117.07 inference(scs_inference,[],[6,38,89,16])).
% 116.95/117.07 cnf(154,plain,
% 116.95/117.07 (P2(a10,a7)),
% 116.95/117.07 inference(scs_inference,[],[11,6,5,16])).
% 116.95/117.07 cnf(156,plain,
% 116.95/117.07 (P2(a10,f3(a5,a2))),
% 116.95/117.07 inference(scs_inference,[],[3,153,19])).
% 116.95/117.07 cnf(159,plain,
% 116.95/117.07 (~P2(f3(a5,a2),a10)+P2(f3(a5,a2),f3(a5,a5))),
% 116.95/117.07 inference(scs_inference,[],[135,156,23,24])).
% 116.95/117.07 cnf(185,plain,
% 116.95/117.07 (P2(f3(a5,a5),a10)),
% 116.95/117.07 inference(scs_inference,[],[75,147,24])).
% 116.95/117.07 cnf(198,plain,
% 116.95/117.07 (P3(f3(a5,a5),a7)+~P2(a7,f3(a5,a5))),
% 116.95/117.07 inference(scs_inference,[],[185,154,25,23])).
% 116.95/117.07 cnf(201,plain,
% 116.95/117.07 (~P2(f3(a2,a2),f3(a5,a5))+P3(f3(a5,a5),a7)),
% 116.95/117.07 inference(scs_inference,[],[8,198,24])).
% 116.95/117.07 cnf(206,plain,
% 116.95/117.07 (~P2(a7,f3(a5,a5))),
% 116.95/117.07 inference(scs_inference,[],[11,185,25])).
% 116.95/117.07 cnf(212,plain,
% 116.95/117.07 (P3(a10,a7)+~P2(f3(a2,a2),f3(a5,a5))),
% 116.95/117.07 inference(scs_inference,[],[147,201,22])).
% 116.95/117.07 cnf(213,plain,
% 116.95/117.07 (~P2(f3(a2,a2),f3(a5,a5))),
% 116.95/117.07 inference(scs_inference,[],[11,75,212,24])).
% 116.95/117.07 cnf(339,plain,
% 116.95/117.07 (P3(f3(a1,f6(a1)),f6(a1))),
% 116.95/117.07 inference(scs_inference,[],[1,12,17])).
% 116.95/117.07 cnf(340,plain,
% 116.95/117.07 (~P3(x3401,f3(a1,f6(a1)))+P3(x3401,f6(a1))),
% 116.95/117.07 inference(scs_inference,[],[339,22])).
% 116.95/117.07 cnf(345,plain,
% 116.95/117.07 (~P1(f3(a1,f6(a1)))+P3(f9(a4,f3(a1,f6(a1))),f6(a1))),
% 116.95/117.07 inference(scs_inference,[],[340,18])).
% 116.95/117.07 cnf(346,plain,
% 116.95/117.07 (~P2(f3(a1,f6(a1)),x3461)+P2(f6(a1),x3461)),
% 116.95/117.07 inference(scs_inference,[],[339,24])).
% 116.95/117.07 cnf(352,plain,
% 116.95/117.07 (~P1(f6(a1))+P2(f6(a1),f3(a1,f6(a1)))),
% 116.95/117.07 inference(scs_inference,[],[40,346,32])).
% 116.95/117.07 cnf(355,plain,
% 116.95/117.07 (~P1(f6(a1))+P3(f9(a4,f3(a1,f6(a1))),f6(a1))),
% 116.95/117.07 inference(scs_inference,[],[1,345,19])).
% 116.95/117.07 cnf(356,plain,
% 116.95/117.07 (P3(f6(a1),f9(a4,f3(a1,f6(a1))))+~P1(f6(a1))),
% 116.95/117.07 inference(scs_inference,[],[355,15])).
% 116.95/117.07 cnf(363,plain,
% 116.95/117.07 (P1(f6(f3(a1,a1)))),
% 116.95/117.07 inference(scs_inference,[],[1,12,19])).
% 116.95/117.07 cnf(369,plain,
% 116.95/117.07 (P1(f6(f9(a4,a4)))),
% 116.95/117.07 inference(scs_inference,[],[2,12,20])).
% 116.95/117.07 cnf(387,plain,
% 116.95/117.07 (P2(f6(a1),f3(a1,f6(a1)))),
% 116.95/117.07 inference(scs_inference,[],[1,12,352])).
% 116.95/117.07 cnf(388,plain,
% 116.95/117.07 (~P2(x3881,f6(a1))+P2(x3881,f3(a1,f6(a1)))),
% 116.95/117.07 inference(scs_inference,[],[387,25])).
% 116.95/117.07 cnf(394,plain,
% 116.95/117.07 (P3(f6(a1),f3(a1,f6(a1)))+~P2(f3(a1,f6(a1)),f6(a1))),
% 116.95/117.07 inference(scs_inference,[],[387,23])).
% 116.95/117.07 cnf(398,plain,
% 116.95/117.07 (~P3(x3981,f3(a1,f6(a1)))+~P2(x3981,f6(a1))+P3(f6(a1),f3(a1,f6(a1)))),
% 116.95/117.07 inference(scs_inference,[],[394,24])).
% 116.95/117.07 cnf(402,plain,
% 116.95/117.07 (P3(f9(a4,f6(a1)),f3(a1,f6(a1)))+~P3(x4021,f3(a1,f6(a1)))+~P2(x4021,f6(a1))),
% 116.95/117.07 inference(scs_inference,[],[113,398,22])).
% 116.95/117.07 cnf(404,plain,
% 116.95/117.07 (~P2(f6(a1),f6(a1))+P3(f9(a4,f6(a1)),f3(a1,f6(a1)))),
% 116.95/117.07 inference(scs_inference,[],[339,402,15])).
% 116.95/117.07 cnf(412,plain,
% 116.95/117.07 (P3(f9(a4,f3(a1,f6(a1))),f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1,12,355])).
% 116.95/117.08 cnf(419,plain,
% 116.95/117.08 (~P3(x4191,f9(a4,f3(a1,f6(a1))))+P3(x4191,f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[412,22])).
% 116.95/117.08 cnf(436,plain,
% 116.95/117.08 (P3(f6(a1),f9(a4,f3(a1,f6(a1))))),
% 116.95/117.08 inference(scs_inference,[],[1,12,356])).
% 116.95/117.08 cnf(444,plain,
% 116.95/117.08 (P1(f9(f6(a1),f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1,12,20])).
% 116.95/117.08 cnf(450,plain,
% 116.95/117.08 (P3(f3(a1,f6(a4)),f6(a4))),
% 116.95/117.08 inference(scs_inference,[],[2,12,17])).
% 116.95/117.08 cnf(453,plain,
% 116.95/117.08 (~P2(f3(a1,f6(a4)),f6(a1))+P2(f6(a4),f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[450,24,388])).
% 116.95/117.08 cnf(466,plain,
% 116.95/117.08 (~P2(x4661,f6(a1))+~P2(f3(a1,f6(a4)),x4661)+P2(f6(a4),f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[453,25])).
% 116.95/117.08 cnf(519,plain,
% 116.95/117.08 (P3(f3(f3(a5,a5),f6(a1)),f3(a10,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1,9,12,30])).
% 116.95/117.08 cnf(529,plain,
% 116.95/117.08 (~P2(f3(f3(a5,a5),f6(a1)),x5291)+P2(f3(a10,f6(a1)),x5291)),
% 116.95/117.08 inference(scs_inference,[],[519,24])).
% 116.95/117.08 cnf(531,plain,
% 116.95/117.08 (~P2(f3(f3(a5,a5),f6(a1)),f6(a1))+P2(f3(a10,f6(a1)),f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[519,24,388])).
% 116.95/117.08 cnf(534,plain,
% 116.95/117.08 (P2(f3(a10,f6(a1)),a5)+~P2(f3(f3(a5,a5),f6(a1)),a2)),
% 116.95/117.08 inference(scs_inference,[],[529,44])).
% 116.95/117.08 cnf(535,plain,
% 116.95/117.08 (~P3(a2,f3(f3(a5,a5),f6(a1)))+P2(f3(a10,f6(a1)),a5)),
% 116.95/117.08 inference(scs_inference,[],[59,534,24])).
% 116.95/117.08 cnf(536,plain,
% 116.95/117.08 (~P3(f3(f3(a5,a5),f6(a1)),a2)+P2(f3(a10,f6(a1)),a5)),
% 116.95/117.08 inference(scs_inference,[],[535,15])).
% 116.95/117.08 cnf(537,plain,
% 116.95/117.08 (~P2(x5371,f3(a10,f6(a1)))+P2(x5371,a5)+~P3(f3(f3(a5,a5),f6(a1)),a2)),
% 116.95/117.08 inference(scs_inference,[],[536,25])).
% 116.95/117.08 cnf(538,plain,
% 116.95/117.08 (~P2(x5381,f6(a1))+~P2(f3(f3(a5,a5),f6(a1)),x5381)+P2(f3(a10,f6(a1)),f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[531,25])).
% 116.95/117.08 cnf(572,plain,
% 116.95/117.08 (P1(f6(f3(a7,a7)))),
% 116.95/117.08 inference(scs_inference,[],[5,12,19])).
% 116.95/117.08 cnf(575,plain,
% 116.95/117.08 (P1(f6(f9(a7,a7)))),
% 116.95/117.08 inference(scs_inference,[],[5,12,20])).
% 116.95/117.08 cnf(586,plain,
% 116.95/117.08 (P1(f6(f3(a10,a10)))),
% 116.95/117.08 inference(scs_inference,[],[6,12,19])).
% 116.95/117.08 cnf(587,plain,
% 116.95/117.08 (P2(f6(f3(a10,a10)),f6(f3(a10,a10)))),
% 116.95/117.08 inference(scs_inference,[],[586,16])).
% 116.95/117.08 cnf(589,plain,
% 116.95/117.08 (P1(f6(f9(a10,a10)))),
% 116.95/117.08 inference(scs_inference,[],[6,12,20])).
% 116.95/117.08 cnf(592,plain,
% 116.95/117.08 (P2(f6(f9(a10,a10)),f6(f9(a10,a10)))),
% 116.95/117.08 inference(scs_inference,[],[587,589,23,16])).
% 116.95/117.08 cnf(619,plain,
% 116.95/117.08 (P2(f3(a10,f6(a1)),f3(a10,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1,75,12,32])).
% 116.95/117.08 cnf(650,plain,
% 116.95/117.08 (P2(f3(f3(a5,a5),f6(a1)),f3(a10,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1,185,12,32])).
% 116.95/117.08 cnf(719,plain,
% 116.95/117.08 (P2(f3(f3(a10,f6(a1)),f6(a1)),f3(f3(a10,f6(a1)),f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1,619,12,32])).
% 116.95/117.08 cnf(767,plain,
% 116.95/117.08 (P2(f6(a1),f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1,12,16])).
% 116.95/117.08 cnf(768,plain,
% 116.95/117.08 (P3(f9(a4,f6(a1)),f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[767,404])).
% 116.95/117.08 cnf(772,plain,
% 116.95/117.08 (~P3(x7721,f9(a4,f6(a1)))+P3(x7721,f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[768,22])).
% 116.95/117.08 cnf(836,plain,
% 116.95/117.08 (P3(f6(a1),f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[113,15,772])).
% 116.95/117.08 cnf(841,plain,
% 116.95/117.08 (P3(a1,f3(a1,a1))),
% 116.95/117.08 inference(scs_inference,[],[1,15,17])).
% 116.95/117.08 cnf(842,plain,
% 116.95/117.08 (P2(f3(a1,a1),a1)),
% 116.95/117.08 inference(scs_inference,[],[40,841,24])).
% 116.95/117.08 cnf(888,plain,
% 116.95/117.08 (P3(a1,f9(a4,a1))),
% 116.95/117.08 inference(scs_inference,[],[1,15,18])).
% 116.95/117.08 cnf(889,plain,
% 116.95/117.08 (P2(f3(a1,f6(a1)),f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[767,836,24])).
% 116.95/117.08 cnf(892,plain,
% 116.95/117.08 (P2(f9(a4,f3(a1,f6(a1))),f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[767,436,24])).
% 116.95/117.08 cnf(902,plain,
% 116.95/117.08 (P2(f9(a4,a1),a1)),
% 116.95/117.08 inference(scs_inference,[],[40,888,24])).
% 116.95/117.08 cnf(970,plain,
% 116.95/117.08 (P3(f3(f6(a1),f6(f6(a1))),f3(a1,a1))),
% 116.95/117.08 inference(scs_inference,[],[119,841,22])).
% 116.95/117.08 cnf(985,plain,
% 116.95/117.08 (~P3(x9851,f3(f6(a1),f6(f6(a1))))+P3(x9851,f3(a1,a1))),
% 116.95/117.08 inference(scs_inference,[],[970,22])).
% 116.95/117.08 cnf(997,plain,
% 116.95/117.08 (P3(f3(a1,a1),x9971)+~P3(x9971,f3(f6(a1),f6(f6(a1))))),
% 116.95/117.08 inference(scs_inference,[],[985,15])).
% 116.95/117.08 cnf(1042,plain,
% 116.95/117.08 (P3(f6(f9(a10,a10)),f3(a1,f6(f9(a10,a10))))),
% 116.95/117.08 inference(scs_inference,[],[589,15,17])).
% 116.95/117.08 cnf(1043,plain,
% 116.95/117.08 (P3(f3(a1,a1),a1)),
% 116.95/117.08 inference(scs_inference,[],[119,15,997])).
% 116.95/117.08 cnf(1044,plain,
% 116.95/117.08 (~P3(a4,f3(a1,a1))),
% 116.95/117.08 inference(scs_inference,[],[36,1043,22])).
% 116.95/117.08 cnf(1046,plain,
% 116.95/117.08 (~P3(f3(a1,a1),a4)),
% 116.95/117.08 inference(scs_inference,[],[36,1043,22,15])).
% 116.95/117.08 cnf(1048,plain,
% 116.95/117.08 (P3(a1,f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1,15,21])).
% 116.95/117.08 cnf(1049,plain,
% 116.95/117.08 (P2(f3(a1,f6(a1)),a1)),
% 116.95/117.08 inference(scs_inference,[],[40,1048,24])).
% 116.95/117.08 cnf(1051,plain,
% 116.95/117.08 (P2(f6(a1),a1)),
% 116.95/117.08 inference(scs_inference,[],[387,40,1048,24,25])).
% 116.95/117.08 cnf(1110,plain,
% 116.95/117.08 (P3(f3(a1,a1),f9(a4,a1))),
% 116.95/117.08 inference(scs_inference,[],[1043,888,22])).
% 116.95/117.08 cnf(1113,plain,
% 116.95/117.08 (P3(f3(a1,a1),f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1043,1048,22])).
% 116.95/117.08 cnf(1118,plain,
% 116.95/117.08 (P3(a1,f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1048,339,22])).
% 116.95/117.08 cnf(1122,plain,
% 116.95/117.08 (P3(f6(a1),f3(a1,a1))),
% 116.95/117.08 inference(scs_inference,[],[1113,15,340])).
% 116.95/117.08 cnf(1125,plain,
% 116.95/117.08 (P2(f3(a1,a1),f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1113,387,339,1122,22,24])).
% 116.95/117.08 cnf(1142,plain,
% 116.95/117.08 (~P3(a4,f9(a4,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1044,1122,22,129])).
% 116.95/117.08 cnf(1148,plain,
% 116.95/117.08 (~P3(f6(a1),a4)),
% 116.95/117.08 inference(scs_inference,[],[1044,1122,22,129,340,419,15])).
% 116.95/117.08 cnf(1164,plain,
% 116.95/117.08 (~P3(f9(a4,f6(a1)),a4)),
% 116.95/117.08 inference(scs_inference,[],[1142,15])).
% 116.95/117.08 cnf(1171,plain,
% 116.95/117.08 (P3(f6(a1),f9(a4,a1))),
% 116.95/117.08 inference(scs_inference,[],[1122,1110,22])).
% 116.95/117.08 cnf(1173,plain,
% 116.95/117.08 (P2(f9(a4,a1),f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1122,387,1110,22,24])).
% 116.95/117.08 cnf(1181,plain,
% 116.95/117.08 (P3(f9(a4,f6(a1)),f9(a4,a1))),
% 116.95/117.08 inference(scs_inference,[],[113,1171,22])).
% 116.95/117.08 cnf(1188,plain,
% 116.95/117.08 (~P3(x11881,f9(a4,f6(a1)))+P3(x11881,f9(a4,a1))),
% 116.95/117.08 inference(scs_inference,[],[1181,22])).
% 116.95/117.08 cnf(1200,plain,
% 116.95/117.08 (P2(f3(a1,a1),f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1125,889,25])).
% 116.95/117.08 cnf(1202,plain,
% 116.95/117.08 (P2(a1,f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1125,889,1043,25,24])).
% 116.95/117.08 cnf(1204,plain,
% 116.95/117.08 (P3(f3(a1,f6(a1)),a1)),
% 116.95/117.08 inference(scs_inference,[],[1125,889,1049,1043,25,24,23])).
% 116.95/117.08 cnf(1213,plain,
% 116.95/117.08 (P2(a1,f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[889,1204,24])).
% 116.95/117.08 cnf(1215,plain,
% 116.95/117.08 (P3(f6(a1),a1)),
% 116.95/117.08 inference(scs_inference,[],[889,1051,1204,24,23])).
% 116.95/117.08 cnf(1235,plain,
% 116.95/117.08 (~P2(x12351,f3(a1,a1))+P2(x12351,f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1200,1213,888,24,25])).
% 116.95/117.08 cnf(1259,plain,
% 116.95/117.08 (P2(f3(f3(a1,a1),a1),f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[842,1,1235,32])).
% 116.95/117.08 cnf(1272,plain,
% 116.95/117.08 (~P1(f6(a1))+P3(f9(f6(a1),a4),f9(a4,a1))),
% 116.95/117.08 inference(scs_inference,[],[2,1188,29])).
% 116.95/117.08 cnf(1281,plain,
% 116.95/117.08 (P3(f9(a4,a1),f9(f6(a1),a4))+~P1(f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1272,15])).
% 116.95/117.08 cnf(1290,plain,
% 116.95/117.08 (P2(f9(f6(a1),a4),a1)+~P1(f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[902,1281,24])).
% 116.95/117.08 cnf(1291,plain,
% 116.95/117.08 (P2(f9(f6(a1),a4),a1)),
% 116.95/117.08 inference(scs_inference,[],[1,1290,12])).
% 116.95/117.08 cnf(1315,plain,
% 116.95/117.08 (P3(f9(f6(a1),a4),f6(a1))+~P2(f6(a1),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[1291,1213,25,388,538,466,23])).
% 116.95/117.08 cnf(1443,plain,
% 116.95/117.08 (P3(f9(f6(a1),a4),f6(a1))+~P2(f3(a1,f6(a1)),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[1315,346])).
% 116.95/117.08 cnf(1503,plain,
% 116.95/117.08 (~P2(f3(a1,f6(a1)),f9(f6(a1),a4))+P3(f6(a1),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[1443,15])).
% 116.95/117.08 cnf(1517,plain,
% 116.95/117.08 (~P2(f6(a1),f9(f6(a1),a4))+P3(f6(a1),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[889,1503,25])).
% 116.95/117.08 cnf(1518,plain,
% 116.95/117.08 (~P2(f9(a4,f6(a1)),f9(f6(a1),a4))+P3(f6(a1),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[1517,114])).
% 116.95/117.08 cnf(1519,plain,
% 116.95/117.08 (~P3(x15191,f9(a4,f6(a1)))+~P2(x15191,f9(f6(a1),a4))+P3(f6(a1),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[1518,24])).
% 116.95/117.08 cnf(1668,plain,
% 116.95/117.08 (~P1(f6(a1))+~P2(f9(f6(a1),a4),f9(f6(a1),a4))+P3(f6(a1),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[2,1519,29])).
% 116.95/117.08 cnf(1670,plain,
% 116.95/117.08 (~P1(f9(f6(a1),a4))+P3(f6(a1),f9(f6(a1),a4))+~P1(f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1668,16])).
% 116.95/117.08 cnf(1671,plain,
% 116.95/117.08 (~P1(f6(a1))+P3(f6(a1),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[2,1670,20])).
% 116.95/117.08 cnf(1672,plain,
% 116.95/117.08 (P3(f9(f6(a1),a4),f6(a1))+~P1(f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1671,15])).
% 116.95/117.08 cnf(1673,plain,
% 116.95/117.08 (P3(f9(f6(a1),a4),a1)+~P1(f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1215,1672,22])).
% 116.95/117.08 cnf(1674,plain,
% 116.95/117.08 (P3(a1,f9(f6(a1),a4))+~P1(f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1673,15])).
% 116.95/117.08 cnf(1675,plain,
% 116.95/117.08 (P3(a1,f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[1,1674,12])).
% 116.95/117.08 cnf(1676,plain,
% 116.95/117.08 (P3(f3(a1,a1),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[1043,1675,22])).
% 116.95/117.08 cnf(1688,plain,
% 116.95/117.08 (P3(f6(a1),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[1122,1676,22])).
% 116.95/117.08 cnf(1691,plain,
% 116.95/117.08 (P3(f9(a4,f6(a1)),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[113,1688,22])).
% 116.95/117.08 cnf(1719,plain,
% 116.95/117.08 (P3(f3(a1,f6(a1)),f9(f6(a1),a4))),
% 116.95/117.08 inference(scs_inference,[],[1204,1675,22])).
% 116.95/117.08 cnf(1807,plain,
% 116.95/117.08 (P1(f8(a4))),
% 116.95/117.08 inference(scs_inference,[],[10,2,15,14])).
% 116.95/117.08 cnf(1814,plain,
% 116.95/117.08 (P3(f9(a4,f8(a4)),a4)),
% 116.95/117.08 inference(scs_inference,[],[10,2,15,26])).
% 116.95/117.08 cnf(1817,plain,
% 116.95/117.08 (~P3(f9(a4,f8(a4)),a1)),
% 116.95/117.08 inference(scs_inference,[],[10,1814,22,15])).
% 116.95/117.08 cnf(1854,plain,
% 116.95/117.08 (~P3(f9(a4,f8(a4)),f3(a1,a1))),
% 116.95/117.08 inference(scs_inference,[],[1046,1814,22,15])).
% 116.95/117.08 cnf(1873,plain,
% 116.95/117.08 (~P3(f9(a4,f8(a4)),f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1148,1814,22,15])).
% 116.95/117.08 cnf(1877,plain,
% 116.95/117.08 (~P3(f9(a4,f8(a4)),f3(a1,f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[1148,1814,22,15,129,340])).
% 116.95/117.08 cnf(1879,plain,
% 116.95/117.08 (~P3(f3(a1,f6(a1)),f9(a4,f8(a4)))),
% 116.95/117.08 inference(scs_inference,[],[1877,15])).
% 116.95/117.08 cnf(2021,plain,
% 116.95/117.08 (P3(a4,f9(a4,f8(a4)))),
% 116.95/117.08 inference(scs_inference,[],[36,2,15,26])).
% 116.95/117.08 cnf(2022,plain,
% 116.95/117.08 (P2(f9(a4,f8(a4)),a4)),
% 116.95/117.08 inference(scs_inference,[],[50,2021,24])).
% 116.95/117.08 cnf(2123,plain,
% 116.95/117.08 (P3(f3(f3(a1,f6(a1)),a1),f3(f6(a1),a1))),
% 116.95/117.08 inference(scs_inference,[],[836,1,15,30])).
% 116.95/117.08 cnf(2169,plain,
% 116.95/117.08 (P3(f3(f3(a1,a1),a1),f3(a1,f3(a1,a1)))),
% 116.95/117.08 inference(scs_inference,[],[1,15,33])).
% 116.95/117.08 cnf(2170,plain,
% 116.95/117.08 (P2(f3(a1,f3(a1,a1)),f6(a1))),
% 116.95/117.08 inference(scs_inference,[],[1259,2169,24])).
% 116.95/117.08 cnf(2227,plain,
% 116.95/117.08 (~P2(f3(a5,a2),f3(a5,a5))),
% 116.95/117.08 inference(scs_inference,[],[7,206,2123,1854,1202,575,87,1807,12,17,18,21,985,15,20,28,32,27,29,19,25])).
% 116.95/117.08 cnf(2229,plain,
% 116.95/117.08 (~P3(f9(f6(a1),a4),f9(a4,f8(a4)))),
% 116.95/117.08 inference(scs_inference,[],[7,206,2123,1854,1879,1719,1202,575,87,1807,12,17,18,21,985,15,20,28,32,27,29,19,25,22])).
% 116.95/117.08 cnf(2235,plain,
% 116.95/117.08 (P3(f3(a7,f3(a7,a7)),f3(f3(a7,a7),a7))),
% 116.95/117.08 inference(scs_inference,[],[7,206,2123,719,1042,1854,1879,1719,1202,592,575,87,1807,5,12,17,18,21,985,15,20,28,32,27,29,19,25,22,24,23,33])).
% 116.95/117.08 cnf(2237,plain,
% 116.95/117.08 (P3(f9(a7,f9(a7,a7)),f9(f9(a7,a7),a7))),
% 116.95/117.08 inference(scs_inference,[],[7,206,2123,719,1042,1854,1879,1719,1202,592,575,87,1807,5,12,17,18,21,985,15,20,28,32,27,29,19,25,22,24,23,33,34])).
% 116.95/117.08 cnf(2239,plain,
% 116.95/117.08 (P3(f3(f9(a7,a7),f9(a7,a7)),f9(f3(a7,a7),a7))),
% 116.95/117.08 inference(scs_inference,[],[7,206,2123,719,1042,1854,1879,1719,1202,592,575,87,1807,5,12,17,18,21,985,15,20,28,32,27,29,19,25,22,24,23,33,34,35])).
% 116.95/117.08 cnf(2243,plain,
% 116.95/117.08 (P3(f8(a4),a1)+P3(f9(f8(a4),f8(f8(a4))),a4)),
% 116.95/117.08 inference(scs_inference,[],[7,206,2123,719,1042,1854,1879,1719,1202,592,575,87,1807,5,12,17,18,21,985,15,20,28,32,27,29,19,25,22,24,23,33,34,35,14,26])).
% 116.95/117.08 cnf(2245,plain,
% 116.95/117.08 (~P2(f3(a5,a2),a10)),
% 116.95/117.08 inference(scs_inference,[],[2227,159])).
% 116.95/117.08 cnf(2249,plain,
% 116.95/117.08 (P3(f9(a4,f8(a4)),f8(a4))),
% 116.95/117.08 inference(scs_inference,[],[1807,5,21,18])).
% 116.95/117.08 cnf(2253,plain,
% 116.95/117.08 (P3(f3(a1,f8(a4)),f8(a4))),
% 116.95/117.08 inference(scs_inference,[],[572,1807,5,21,18,12,17])).
% 116.95/117.08 cnf(2259,plain,
% 116.95/117.08 (P1(f9(f8(a4),f8(a4)))),
% 116.95/117.08 inference(scs_inference,[],[7,2239,572,1807,5,21,18,12,17,15,32,20])).
% 116.95/117.08 cnf(2261,plain,
% 116.95/117.08 (P3(f3(a7,a7),f3(a7,a7))),
% 116.95/117.08 inference(scs_inference,[],[7,2239,572,1807,5,21,18,12,17,15,32,20,28])).
% 116.95/117.08 cnf(2263,plain,
% 116.95/117.08 (P1(f3(f8(a4),f8(a4)))),
% 116.95/117.08 inference(scs_inference,[],[7,2239,572,1807,5,21,18,12,17,15,32,20,28,19])).
% 116.95/117.08 cnf(2265,plain,
% 116.95/117.08 (P3(f9(a7,a7),f9(a7,a7))),
% 116.95/117.08 inference(scs_inference,[],[7,2239,572,1807,5,21,18,12,17,15,32,20,28,19,29])).
% 116.95/117.08 cnf(2267,plain,
% 116.95/117.08 (P2(a1,f9(a1,a1))),
% 116.95/117.08 inference(scs_inference,[],[7,2239,572,40,1807,5,21,18,12,17,15,32,20,28,19,29,27])).
% 116.95/117.08 cnf(2269,plain,
% 116.95/117.08 (P2(f3(a1,f3(a1,a1)),a1)),
% 116.95/117.08 inference(scs_inference,[],[7,2239,572,1051,2170,40,1807,5,21,18,12,17,15,32,20,28,19,29,27,25])).
% 116.95/117.08 cnf(2277,plain,
% 116.95/117.08 (P3(f3(a10,f3(a10,a10)),f3(f3(a10,a10),a10))),
% 116.95/117.08 inference(scs_inference,[],[7,213,2239,148,572,1051,2170,40,1807,5,6,21,18,12,17,15,32,20,28,19,29,27,25,22,24,34,33])).
% 116.95/117.08 cnf(2288,plain,
% 116.95/117.08 (P3(f3(a1,a7),a7)),
% 116.95/117.08 inference(scs_inference,[],[5,6,21,17])).
% 116.95/117.08 cnf(2292,plain,
% 116.95/117.08 (P3(f9(a4,a7),a7)),
% 116.95/117.08 inference(scs_inference,[],[2263,5,6,21,17,12,18])).
% 116.95/117.08 cnf(2294,plain,
% 116.95/117.08 (P3(f8(a4),f9(a4,f8(a4)))),
% 116.95/117.08 inference(scs_inference,[],[2249,2263,5,6,21,17,12,18,15])).
% 116.95/117.08 cnf(2302,plain,
% 116.95/117.08 (P1(f9(a7,a7))),
% 116.95/117.08 inference(scs_inference,[],[7,2265,2249,2263,1807,5,6,21,17,12,18,15,30,31,32,20])).
% 116.95/117.08 cnf(2304,plain,
% 116.95/117.08 (P1(f3(a7,a7))),
% 116.95/117.08 inference(scs_inference,[],[7,2265,2249,2263,1807,5,6,21,17,12,18,15,30,31,32,20,19])).
% 116.95/117.08 cnf(2306,plain,
% 116.95/117.08 (P3(f3(a10,a10),f3(a10,a10))),
% 116.95/117.08 inference(scs_inference,[],[7,2265,2249,2263,1807,5,6,21,17,12,18,15,30,31,32,20,19,28])).
% 116.95/117.08 cnf(2308,plain,
% 116.95/117.08 (P2(a1,f9(f9(a1,a1),f9(a1,a1)))),
% 116.95/117.08 inference(scs_inference,[],[7,2265,2267,2249,2263,1807,5,6,21,17,12,18,15,30,31,32,20,19,28,27])).
% 116.95/117.08 cnf(2310,plain,
% 116.95/117.08 (P3(f9(a10,a10),f9(a10,a10))),
% 116.95/117.08 inference(scs_inference,[],[7,2265,2267,2249,2263,1807,5,6,21,17,12,18,15,30,31,32,20,19,28,27,29])).
% 116.95/117.08 cnf(2316,plain,
% 116.95/117.08 (P2(f6(a1),f9(a1,a1))),
% 116.95/117.08 inference(scs_inference,[],[7,2265,2267,2249,2263,2269,1817,1118,1807,5,6,21,17,12,18,15,30,31,32,20,19,28,27,29,25,22,24])).
% 116.95/117.08 cnf(2327,plain,
% 116.95/117.08 (P1(f8(f8(a4)))),
% 116.95/117.08 inference(scs_inference,[],[7,2265,2267,2249,2263,2269,1817,1118,650,1807,5,6,4,21,17,12,18,15,30,31,32,20,19,28,27,29,25,22,24,34,35,33,2243,537,14])).
% 116.95/117.08 cnf(2333,plain,
% 116.95/117.08 (P3(f9(a4,f9(a7,a7)),f9(a7,a7))),
% 116.95/117.08 inference(scs_inference,[],[2302,18])).
% 116.95/117.08 cnf(2337,plain,
% 116.95/117.08 (P3(f3(a1,f9(a7,a7)),f9(a7,a7))),
% 116.95/117.08 inference(scs_inference,[],[2302,18,21,17])).
% 116.95/117.08 cnf(2341,plain,
% 116.95/117.08 (P3(a7,f3(a1,a7))),
% 116.95/117.08 inference(scs_inference,[],[2302,2288,2327,18,21,17,12,15])).
% 116.95/117.08 cnf(2347,plain,
% 116.95/117.08 (P1(f9(f9(a7,a7),f9(a7,a7)))),
% 116.95/117.08 inference(scs_inference,[],[2302,2261,2288,2327,18,21,17,12,15,30,31,20])).
% 116.95/117.08 cnf(2351,plain,
% 116.95/117.08 (P2(a1,f9(f6(a1),f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[7,2302,2261,2288,2327,1213,18,21,17,12,15,30,31,20,32,27])).
% 116.95/117.08 cnf(2359,plain,
% 116.95/117.08 (P2(f3(a1,f3(a1,a1)),f9(f9(a1,a1),f9(a1,a1)))),
% 116.95/117.08 inference(scs_inference,[],[7,2302,2304,2261,2288,2327,2308,2269,1213,18,21,17,12,15,30,31,20,32,27,19,28,29,25])).
% 116.95/117.08 cnf(2361,plain,
% 116.95/117.08 (~P3(f9(f6(a1),a4),f8(a4))),
% 116.95/117.08 inference(scs_inference,[],[7,2302,2304,2261,2288,2327,2294,2308,2229,2269,1213,18,21,17,12,15,30,31,20,32,27,19,28,29,25,22])).
% 116.95/117.08 cnf(2377,plain,
% 116.95/117.08 (P3(f9(a4,f3(a7,a7)),f3(a7,a7))),
% 116.95/117.08 inference(scs_inference,[],[2347,2304,12,18])).
% 116.95/117.08 cnf(2379,plain,
% 116.95/117.08 (P3(f3(a1,f3(a7,a7)),f3(a7,a7))),
% 116.95/117.08 inference(scs_inference,[],[2347,2304,12,18,17])).
% 116.95/117.08 cnf(2383,plain,
% 116.95/117.08 (P3(a7,f9(a4,a7))),
% 116.95/117.08 inference(scs_inference,[],[2292,2347,2304,12,18,17,21,15])).
% 116.95/117.08 cnf(2391,plain,
% 116.95/117.08 (P1(f9(f3(a7,a7),f3(a7,a7)))),
% 116.95/117.08 inference(scs_inference,[],[7,2310,2292,2347,2304,12,18,17,21,15,30,31,32,20])).
% 116.95/117.08 cnf(2393,plain,
% 116.95/117.08 (P3(f3(a4,a4),f3(a4,a4))),
% 116.95/117.08 inference(scs_inference,[],[7,2310,2292,2347,2304,2,12,18,17,21,15,30,31,32,20,28])).
% 116.95/117.08 cnf(2395,plain,
% 116.95/117.08 (P1(f3(f3(a7,a7),f3(a7,a7)))),
% 116.95/117.08 inference(scs_inference,[],[7,2310,2292,2347,2304,2,12,18,17,21,15,30,31,32,20,28,19])).
% 116.95/117.08 cnf(2401,plain,
% 116.95/117.08 (P3(f9(a4,a7),f3(a1,a7))),
% 116.95/117.08 inference(scs_inference,[],[7,2310,2292,2341,2347,2351,2304,2269,2,12,18,17,21,15,30,31,32,20,28,19,29,25,22])).
% 116.95/117.08 cnf(2403,plain,
% 116.95/117.08 (P2(f6(a1),f9(f6(a1),f6(a1)))),
% 116.95/117.08 inference(scs_inference,[],[7,2310,2292,2341,2347,2351,2304,1118,2269,2,12,18,17,21,15,30,31,32,20,28,19,29,25,22,24])).
% 116.95/117.08 cnf(2415,plain,
% 116.95/117.08 (P3(f3(a5,f6(a5)),a1)),
% 116.95/117.08 inference(scs_inference,[],[4,21])).
% 116.95/117.08 cnf(2419,plain,
% 116.95/117.08 (P3(f3(a1,a10),a10)),
% 116.95/117.08 inference(scs_inference,[],[2395,6,4,21,12,17])).
% 116.95/117.08 cnf(2421,plain,
% 116.95/117.08 (P3(f9(a4,a10),a10)),
% 116.95/117.08 inference(scs_inference,[],[2395,6,4,21,12,17,18])).
% 116.95/117.08 cnf(2423,plain,
% 116.95/117.08 (P3(f3(a1,a7),f9(a4,a7))),
% 116.95/117.08 inference(scs_inference,[],[2401,2395,6,4,21,12,17,18,15])).
% 116.95/117.08 cnf(2427,plain,
% 116.95/117.08 (P1(f9(a10,a10))),
% 116.95/117.08 inference(scs_inference,[],[2306,2401,2395,2302,6,4,21,12,17,18,15,30,20])).
% 116.95/117.08 cnf(2429,plain,
% 116.95/117.08 (P2(f3(a2,a5),f3(a5,a5))),
% 116.95/117.08 inference(scs_inference,[],[7,2306,2401,2395,2302,6,4,21,12,17,18,15,30,20,32])).
% 116.95/117.08 cnf(2431,plain,
% 116.95/117.08 (P3(f9(a5,a5),f9(a5,a5))),
% 116.95/117.08 inference(scs_inference,[],[7,2306,2401,2395,2302,6,4,21,12,17,18,15,30,20,32,29])).
% 116.95/117.08 cnf(2435,plain,
% 116.95/117.08 (P1(f3(a10,a10))),
% 116.95/117.08 inference(scs_inference,[],[7,2306,2401,2395,2302,6,4,21,12,17,18,15,30,20,32,29,28,19])).
% 116.95/117.08 cnf(2447,plain,
% 116.95/117.08 (P3(f3(a1,f3(a1,a1)),f3(f3(a1,a1),a1))),
% 116.95/117.08 inference(scs_inference,[],[7,2306,2401,2253,2361,2395,2403,2308,1688,902,2302,6,4,1,21,12,17,18,15,30,20,32,29,28,19,25,22,24,34,35,33])).
% 116.95/117.08 cnf(2457,plain,
% 116.95/117.08 (P3(f3(a1,f9(a10,a10)),f9(a10,a10))),
% 116.95/117.08 inference(scs_inference,[],[2427,18,21,17])).
% 116.95/117.08 cnf(2467,plain,
% 116.95/117.08 (P1(f9(f9(a10,a10),f9(a10,a10)))),
% 116.95/117.08 inference(scs_inference,[],[2427,2431,2419,2391,18,21,17,12,15,30,31,20])).
% 116.95/117.08 cnf(2475,plain,
% 116.95/117.08 (P1(f3(f9(a10,a10),f9(a10,a10)))),
% 116.95/117.08 inference(scs_inference,[],[7,2427,2435,2431,2419,2391,18,21,17,12,15,30,31,20,32,29,28,19])).
% 116.95/117.08 cnf(2479,plain,
% 116.95/117.08 (P3(f3(a1,a7),f3(a1,a7))),
% 116.95/117.08 inference(scs_inference,[],[7,2427,2435,2431,2423,2419,2391,2316,2401,1200,18,21,17,12,15,30,31,20,32,29,28,19,25,22])).
% 116.95/117.08 cnf(2481,plain,
% 116.95/117.08 (~P3(f3(a2,a5),f3(a5,a2))),
% 116.95/117.08 inference(scs_inference,[],[7,2227,2427,2435,2429,2431,2423,2419,2391,2316,2401,1200,18,21,17,12,15,30,31,20,32,29,28,19,25,22,24])).
% 116.95/117.08 cnf(2489,plain,
% 116.95/117.08 (P3(f9(a4,f3(a10,a10)),f3(a10,a10))),
% 116.95/117.08 inference(scs_inference,[],[2467,2435,12,18])).
% 116.95/117.08 cnf(2493,plain,
% 116.95/117.08 (P3(f3(a1,f3(a10,a10)),f3(a10,a10))),
% 116.95/117.08 inference(scs_inference,[],[2467,2435,12,18,21,17])).
% 116.95/117.08 cnf(2501,plain,
% 116.95/117.08 (P1(f9(f3(a10,a10),f3(a10,a10)))),
% 116.95/117.08 inference(scs_inference,[],[2393,2421,2467,2435,12,18,21,17,15,30,31,20])).
% 116.95/117.08 cnf(2519,plain,
% 116.95/117.09 (P3(f3(a1,a5),a5)),
% 116.95/117.09 inference(scs_inference,[],[4,17])).
% 116.95/117.09 cnf(2523,plain,
% 116.95/117.09 (P3(f3(a2,f6(a2)),a1)),
% 116.95/117.09 inference(scs_inference,[],[2501,4,3,17,12,21])).
% 116.95/117.09 cnf(2525,plain,
% 116.95/117.09 (P3(f9(a4,a5),a5)),
% 116.95/117.09 inference(scs_inference,[],[2501,4,3,17,12,21,18])).
% 116.95/117.09 cnf(2531,plain,
% 116.95/117.09 (P1(f9(a5,a5))),
% 116.95/117.09 inference(scs_inference,[],[7,2333,2501,4,3,2,17,12,21,18,15,32,20])).
% 116.95/117.09 cnf(2535,plain,
% 116.95/117.09 (P3(f9(a2,a2),f9(a2,a2))),
% 116.95/117.09 inference(scs_inference,[],[7,2333,2501,4,3,2,17,12,21,18,15,32,20,28,29])).
% 116.95/117.09 cnf(2537,plain,
% 116.95/117.09 (P1(f3(a5,a5))),
% 116.95/117.09 inference(scs_inference,[],[7,2333,2501,4,3,2,17,12,21,18,15,32,20,28,29,19])).
% 116.95/117.09 cnf(2551,plain,
% 116.95/117.09 (P3(f3(a1,f3(a5,a5)),f3(a5,a5))),
% 116.95/117.09 inference(scs_inference,[],[2537,18,17])).
% 116.95/117.09 cnf(2557,plain,
% 116.95/117.09 (P3(a5,f3(a1,a5))),
% 116.95/117.09 inference(scs_inference,[],[2537,2519,18,17,12,21,15])).
% 116.95/117.09 cnf(2565,plain,
% 116.95/117.09 (P1(f9(f3(a5,a5),f3(a5,a5)))),
% 116.95/117.09 inference(scs_inference,[],[7,2537,2535,2519,18,17,12,21,15,30,31,32,20])).
% 116.95/117.09 cnf(2571,plain,
% 116.95/117.09 (P1(f3(f3(a5,a5),f3(a5,a5)))),
% 116.95/117.09 inference(scs_inference,[],[7,2537,2535,2519,18,17,12,21,15,30,31,32,20,29,28,19])).
% 116.95/117.09 cnf(2573,plain,
% 116.95/117.09 (~P3(f9(f6(a1),a4),a4)),
% 116.95/117.09 inference(scs_inference,[],[7,2537,2535,2519,1164,1691,18,17,12,21,15,30,31,32,20,29,28,19,22])).
% 116.95/117.09 cnf(2579,plain,
% 116.95/117.09 (P3(a10,f9(a4,f3(a5,a5)))),
% 116.95/117.09 inference(scs_inference,[],[7,2537,2535,2519,2359,1164,1691,2447,18,17,12,21,15,30,31,32,20,29,28,19,22,24,61,142])).
% 116.95/117.09 cnf(2588,plain,
% 116.95/117.09 (P3(a10,f3(a1,f3(a5,a5)))),
% 116.95/117.09 inference(scs_inference,[],[2551,142])).
% 116.95/117.09 cnf(2598,plain,
% 116.95/117.09 (P1(f6(f9(a5,a5)))),
% 116.95/117.09 inference(scs_inference,[],[2531,2551,142,61,18,17,21,12])).
% 116.95/117.09 cnf(2600,plain,
% 116.95/117.09 (P3(a5,f9(a4,a5))),
% 116.95/117.09 inference(scs_inference,[],[2531,2525,2551,142,61,18,17,21,12,15])).
% 116.95/117.09 cnf(2614,plain,
% 116.95/117.09 (P3(f9(a4,a5),f3(a1,a5))),
% 116.95/117.09 inference(scs_inference,[],[7,2531,2479,2557,2525,2551,142,61,18,17,21,12,15,30,31,32,20,29,19,22])).
% 116.95/117.09 cnf(2626,plain,
% 116.95/117.09 (P3(f9(a4,a2),a2)),
% 116.95/117.09 inference(scs_inference,[],[3,18])).
% 116.95/117.09 cnf(2628,plain,
% 116.95/117.09 (P3(f3(a1,a2),a2)),
% 116.95/117.09 inference(scs_inference,[],[3,18,17])).
% 116.95/117.09 cnf(2632,plain,
% 116.95/117.09 (P3(f3(a4,f6(a4)),a1)),
% 116.95/117.09 inference(scs_inference,[],[2598,3,2,18,17,12,21])).
% 116.95/117.09 cnf(2634,plain,
% 116.95/117.09 (P3(f3(a1,a5),f9(a4,a5))),
% 116.95/117.09 inference(scs_inference,[],[2614,2598,3,2,18,17,12,21,15])).
% 116.95/117.09 cnf(2636,plain,
% 116.95/117.09 (P1(f9(a2,a2))),
% 116.95/117.09 inference(scs_inference,[],[2614,2598,3,2,18,17,12,21,15,20])).
% 116.95/117.09 cnf(2640,plain,
% 116.95/117.09 (P3(f9(a4,a4),f9(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[2614,2598,3,2,18,17,12,21,15,20,28,29])).
% 116.95/117.09 cnf(2642,plain,
% 116.95/117.09 (P1(f3(a2,a2))),
% 116.95/117.09 inference(scs_inference,[],[2614,2598,3,2,18,17,12,21,15,20,28,29,19])).
% 116.95/117.09 cnf(2646,plain,
% 116.95/117.09 (~P3(f8(a4),f6(a1))),
% 116.95/117.09 inference(scs_inference,[],[2614,2598,1873,2316,2249,3,2,892,18,17,12,21,15,20,28,29,19,25,22])).
% 116.95/117.09 cnf(2650,plain,
% 116.95/117.09 (P2(f3(a5,a5),f3(a2,a2))),
% 116.95/117.09 inference(scs_inference,[],[2614,2383,2598,1873,213,71,2316,2249,2537,3,2,892,18,17,12,21,15,20,28,29,19,25,22,24,16])).
% 116.95/117.09 cnf(2662,plain,
% 116.95/117.09 (P3(f3(a1,f3(a2,a2)),f3(a2,a2))),
% 116.95/117.09 inference(scs_inference,[],[2642,18,17])).
% 116.95/117.09 cnf(2664,plain,
% 116.95/117.09 (P1(f6(f3(a2,a2)))),
% 116.95/117.09 inference(scs_inference,[],[2642,18,17,12])).
% 116.95/117.09 cnf(2676,plain,
% 116.95/117.09 (P1(f9(f3(a2,a2),f3(a2,a2)))),
% 116.95/117.09 inference(scs_inference,[],[7,2628,2642,2626,18,17,12,21,15,30,31,32,20])).
% 116.95/117.09 cnf(2682,plain,
% 116.95/117.09 (P1(f3(f3(a2,a2),f3(a2,a2)))),
% 116.95/117.09 inference(scs_inference,[],[7,2628,2642,2626,18,17,12,21,15,30,31,32,20,28,29,19])).
% 116.95/117.09 cnf(2684,plain,
% 116.95/117.09 (P3(f3(a1,a5),f3(a1,a5))),
% 116.95/117.09 inference(scs_inference,[],[7,2628,2642,2634,2626,2614,18,17,12,21,15,30,31,32,20,28,29,19,22])).
% 116.95/117.09 cnf(2707,plain,
% 116.95/117.09 (P3(f3(a1,f9(a2,a2)),f9(a2,a2))),
% 116.95/117.09 inference(scs_inference,[],[2636,2662,46,134,18,17])).
% 116.95/117.09 cnf(2709,plain,
% 116.95/117.09 (P1(f6(f9(a2,a2)))),
% 116.95/117.09 inference(scs_inference,[],[2636,2662,46,134,18,17,12])).
% 116.95/117.09 cnf(2721,plain,
% 116.95/117.09 (P1(f9(f9(a2,a2),f9(a2,a2)))),
% 116.95/117.09 inference(scs_inference,[],[7,2636,2640,2337,2662,46,134,18,17,12,21,15,30,31,32,20])).
% 116.95/117.09 cnf(2733,plain,
% 116.95/117.09 (~P3(f8(a4),f3(f6(a1),f6(f6(a1))))),
% 116.95/117.09 inference(scs_inference,[],[7,2636,2640,2337,2662,2245,2650,1854,2249,2429,75,46,134,18,17,12,21,15,30,31,32,20,29,19,25,22,24,985])).
% 116.95/117.09 cnf(2744,plain,
% 116.95/117.09 (P3(f9(a4,a4),a4)),
% 116.95/117.09 inference(scs_inference,[],[2,18])).
% 116.95/117.09 cnf(2746,plain,
% 116.95/117.09 (P3(f3(a1,a4),a4)),
% 116.95/117.09 inference(scs_inference,[],[2,18,17])).
% 116.95/117.09 cnf(2752,plain,
% 116.95/117.09 (P1(f9(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[2377,2709,2,18,17,12,15,20])).
% 116.95/117.09 cnf(2754,plain,
% 116.95/117.09 (P1(f3(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[2377,2709,2,18,17,12,15,20,19])).
% 116.95/117.09 cnf(2773,plain,
% 116.95/117.09 (P3(f9(a4,f9(a4,a4)),f9(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[2752,18])).
% 116.95/117.09 cnf(2775,plain,
% 116.95/117.09 (P3(f3(a1,f9(a4,a4)),f9(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[2752,18,17])).
% 116.95/117.09 cnf(2781,plain,
% 116.95/117.09 (P3(a4,f9(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[2752,2754,2744,2664,18,17,21,12,15])).
% 116.95/117.09 cnf(2791,plain,
% 116.95/117.09 (P1(f9(f9(a4,a4),f9(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[7,2752,2754,2684,2744,2664,18,17,21,12,15,30,31,32,28,20])).
% 116.95/117.09 cnf(2793,plain,
% 116.95/117.09 (P1(f3(f9(a4,a4),f9(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[7,2752,2754,2684,2744,2664,18,17,21,12,15,30,31,32,28,20,19])).
% 116.95/117.09 cnf(2797,plain,
% 116.95/117.09 (P2(f3(a1,f6(a1)),f9(f6(a1),f6(a1)))),
% 116.95/117.09 inference(scs_inference,[],[7,2752,2754,2684,2744,2664,2403,889,18,17,21,12,15,30,31,32,28,20,19,29,25])).
% 116.95/117.09 cnf(2799,plain,
% 116.95/117.09 (~P3(f9(f6(a1),a4),f9(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[7,2752,2754,2684,2744,2573,2664,2403,889,18,17,21,12,15,30,31,32,28,20,19,29,25,22])).
% 116.95/117.09 cnf(2807,plain,
% 116.95/117.09 (P3(f9(a4,f3(a4,a4)),f3(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[2754,18])).
% 116.95/117.09 cnf(2809,plain,
% 116.95/117.09 (P3(f3(a1,f3(a4,a4)),f3(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[2754,18,17])).
% 116.95/117.09 cnf(2815,plain,
% 116.95/117.09 (P3(f9(a4,f3(a4,a4)),f9(f9(a4,a4),f3(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[2781,2746,2791,2754,18,17,12,15,31])).
% 116.95/117.09 cnf(2821,plain,
% 116.95/117.09 (P1(f9(f3(a4,a4),f3(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[7,2781,2746,2791,2754,18,17,12,15,31,30,32,20])).
% 116.95/117.09 cnf(2823,plain,
% 116.95/117.09 (P1(f3(f3(a4,a4),f3(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[7,2781,2746,2791,2754,18,17,12,15,31,30,32,20,19])).
% 116.95/117.09 cnf(2833,plain,
% 116.95/117.09 (P3(f9(a4,a1),a1)),
% 116.95/117.09 inference(scs_inference,[],[1,18])).
% 116.95/117.09 cnf(2837,plain,
% 116.95/117.09 (P3(f9(a4,a4),f9(a4,f9(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[2773,2823,1,18,12,15])).
% 116.95/117.09 cnf(2839,plain,
% 116.95/117.09 (P1(f9(a1,a1))),
% 116.95/117.09 inference(scs_inference,[],[2773,2823,1,18,12,15,20])).
% 116.95/117.09 cnf(2843,plain,
% 116.95/117.09 (P1(f3(a1,a1))),
% 116.95/117.09 inference(scs_inference,[],[2773,2823,1,18,12,15,20,29,19])).
% 116.95/117.09 cnf(2845,plain,
% 116.95/117.09 (~P3(f9(f6(a1),a4),f9(a4,f9(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[2773,2799,2823,1,18,12,15,20,29,19,22])).
% 116.95/117.09 cnf(2847,plain,
% 116.95/117.09 (~P3(a10,f3(a2,a2))),
% 116.95/117.09 inference(scs_inference,[],[2773,2799,2823,38,75,1,18,12,15,20,29,19,22,24])).
% 116.95/117.09 cnf(2849,plain,
% 116.95/117.09 (P3(f3(a1,f9(a1,a1)),f9(a1,a1))),
% 116.95/117.09 inference(scs_inference,[],[2773,2799,2823,38,75,1,18,12,15,20,29,19,22,24,17])).
% 116.95/117.09 cnf(2859,plain,
% 116.95/117.09 (P3(f9(a4,f9(a1,a1)),f9(a1,a1))),
% 116.95/117.09 inference(scs_inference,[],[2839,18])).
% 116.95/117.09 cnf(2861,plain,
% 116.95/117.09 (P3(f3(a1,f3(a1,a1)),f3(a1,a1))),
% 116.95/117.09 inference(scs_inference,[],[2839,2843,18,17])).
% 116.95/117.09 cnf(2875,plain,
% 116.95/117.09 (P1(f9(f9(a1,a1),f9(a1,a1)))),
% 116.95/117.09 inference(scs_inference,[],[7,2833,2839,2843,2379,2821,18,17,21,12,15,30,31,32,20])).
% 116.95/117.09 cnf(2897,plain,
% 116.95/117.09 (P3(f9(a5,f3(a1,a1)),f9(f9(a4,a5),f3(a1,a1)))),
% 116.95/117.09 inference(scs_inference,[],[2600,2861,2875,2843,18,12,15,30,31])).
% 116.95/117.09 cnf(2901,plain,
% 116.95/117.09 (P1(f9(f3(a1,a1),f3(a1,a1)))),
% 116.95/117.09 inference(scs_inference,[],[7,2600,2861,2875,2843,18,12,15,30,31,32,20])).
% 116.95/117.09 cnf(2903,plain,
% 116.95/117.09 (P1(f3(f3(a1,a1),f3(a1,a1)))),
% 116.95/117.09 inference(scs_inference,[],[7,2600,2861,2875,2843,18,12,15,30,31,32,20,19])).
% 116.95/117.09 cnf(2907,plain,
% 116.95/117.09 (~P3(a10,a7)),
% 116.95/117.09 inference(scs_inference,[],[7,2847,2600,2861,2875,2579,2843,75,11,18,12,15,30,31,32,20,19,22,24])).
% 116.95/117.09 cnf(2919,plain,
% 116.95/117.09 (P3(f3(a1,f9(a4,a4)),f9(a4,f9(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[2457,2775,2901,2797,2837,1173,12,15,25,22])).
% 116.95/117.09 cnf(2929,plain,
% 116.95/117.09 (P3(f3(a10,a10),f3(a1,f3(a10,a10)))),
% 116.95/117.09 inference(scs_inference,[],[2493,2903,12,15])).
% 116.95/117.09 cnf(2933,plain,
% 116.95/117.09 (~P3(f3(a1,f3(a5,a5)),a7)),
% 116.95/117.09 inference(scs_inference,[],[2907,2493,2588,2903,2839,12,15,30,22])).
% 116.95/117.09 cnf(2955,plain,
% 116.95/117.09 (~P3(f9(f6(a1),a4),f3(a1,f9(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[2707,2845,2919,2793,2839,12,15,31,22])).
% 116.95/117.09 cnf(2968,plain,
% 116.95/117.09 (P3(f9(a4,f3(a10,a10)),f3(a1,f3(a10,a10)))),
% 116.95/117.09 inference(scs_inference,[],[2489,2929,2682,12,15,22])).
% 116.95/117.09 cnf(2976,plain,
% 116.95/117.09 (P3(f3(a4,a4),f3(a1,f3(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[2809,2721,12,15])).
% 116.95/117.09 cnf(2987,plain,
% 116.95/117.09 (P3(f9(a1,a1),f3(a1,f9(a1,a1)))),
% 116.95/117.09 inference(scs_inference,[],[2849,2676,12,15])).
% 116.95/117.09 cnf(3024,plain,
% 116.95/117.09 (P3(f3(a4,a4),f9(a4,f3(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[2807,2571,12,15])).
% 116.95/117.09 cnf(3038,plain,
% 116.95/117.09 (P3(f9(a4,f9(a1,a1)),f3(a1,f9(a1,a1)))),
% 116.95/117.09 inference(scs_inference,[],[2859,2987,2565,12,15,22])).
% 116.95/117.09 cnf(3080,plain,
% 116.95/117.09 (P3(a1,f3(a5,f6(a5)))),
% 116.95/117.09 inference(scs_inference,[],[2415,2475,12,15])).
% 116.95/117.09 cnf(3105,plain,
% 116.95/117.09 (P3(a1,f3(a4,f6(a4)))),
% 116.95/117.09 inference(scs_inference,[],[2632,2259,12,15])).
% 116.95/117.09 cnf(3107,plain,
% 116.95/117.09 (P3(f3(a4,f6(a4)),f3(a5,f6(a5)))),
% 116.95/117.09 inference(scs_inference,[],[2632,3080,2259,12,15,22])).
% 116.95/117.09 cnf(3130,plain,
% 116.95/117.09 (P3(f3(a4,a4),f9(f9(a4,a4),f3(a4,a4)))),
% 116.95/117.09 inference(scs_inference,[],[3024,2235,2815,363,12,15,22])).
% 116.95/117.09 cnf(3141,plain,
% 116.95/117.09 (P3(f9(f9(a4,a4),f3(a4,a4)),f3(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[3130,586,12,15])).
% 116.95/117.09 cnf(3158,plain,
% 116.95/117.09 (P2(f3(a4,f6(a4)),f3(a1,f6(a1)))),
% 116.95/117.09 inference(scs_inference,[],[3141,2976,3105,2237,1202,444,12,15,22,24])).
% 116.95/117.09 cnf(3183,plain,
% 116.95/117.09 (P2(f3(a5,f6(a5)),f3(a1,f6(a1)))),
% 116.95/117.09 inference(scs_inference,[],[2277,3158,3107,369,12,15,22,24])).
% 116.95/117.09 cnf(3386,plain,
% 116.95/117.09 (P1(f6(a5))),
% 116.95/117.09 inference(scs_inference,[],[4,12])).
% 116.95/117.09 cnf(3392,plain,
% 116.95/117.09 (P2(f3(a2,f6(a5)),f3(a5,f6(a5)))),
% 116.95/117.09 inference(scs_inference,[],[7,3038,4,12,15,28,32])).
% 116.95/117.09 cnf(3459,plain,
% 116.95/117.09 (P1(f6(a2))),
% 116.95/117.09 inference(scs_inference,[],[2968,3,15,12])).
% 116.95/117.09 cnf(3471,plain,
% 116.95/117.09 (P3(f6(a2),f6(a2))),
% 116.95/117.09 inference(scs_inference,[],[7,2968,3,15,12,28,32,20,29,19,13])).
% 116.95/117.09 cnf(3473,plain,
% 116.95/117.09 (P3(f3(a1,f6(a2)),f6(a2))),
% 116.95/117.09 inference(scs_inference,[],[7,2968,3,15,12,28,32,20,29,19,13,17])).
% 116.95/117.09 cnf(3481,plain,
% 116.95/117.09 (P2(a1,f3(a5,f6(a2)))),
% 116.95/117.09 inference(scs_inference,[],[7,2968,2733,2523,3,15,12,28,32,20,29,19,13,17,18,21,23,24])).
% 116.95/117.09 cnf(3499,plain,
% 116.95/117.09 (~P3(x34991,f3(a1,f9(a4,a4)))+~P3(f9(f6(a1),a4),x34991)),
% 116.95/117.09 inference(scs_inference,[],[3459,3471,3473,3481,3392,2955,3183,3386,15,12,31,30,32,25,13,22])).
% 116.95/117.09 cnf(3615,plain,
% 116.95/117.09 (P1(f6(a1))),
% 116.95/117.09 inference(scs_inference,[],[1,12])).
% 116.95/117.09 cnf(3635,plain,
% 116.95/117.09 (P3(f9(f6(a1),a4),f6(a1))),
% 116.95/117.09 inference(scs_inference,[],[3615,1672])).
% 116.95/117.09 cnf(3636,plain,
% 116.95/117.09 (P3(f9(f6(a1),a4),a1)),
% 116.95/117.09 inference(scs_inference,[],[3615,1673])).
% 116.95/117.09 cnf(3640,plain,
% 116.95/117.09 (P1(f6(f6(a1)))),
% 116.95/117.09 inference(scs_inference,[],[3615,12])).
% 116.95/117.09 cnf(3664,plain,
% 116.95/117.09 (P3(f9(f9(f6(a1),a4),f6(a1)),f9(f6(a1),f6(a1)))),
% 116.95/117.09 inference(scs_inference,[],[3635,3640,2897,3615,3499,12,15,31])).
% 116.95/117.09 cnf(3764,plain,
% 116.95/117.09 (~P3(a1,f9(a4,a4))),
% 116.95/117.09 inference(scs_inference,[],[3664,2799,3636,15,22])).
% 116.95/117.09 cnf(4321,plain,
% 116.95/117.09 ($false),
% 116.95/117.09 inference(scs_inference,[],[3,4,2294,3764,2249,2022,2646,2907,2933,2481,15,340,46,142,419,22,24,28]),
% 116.95/117.09 ['proof']).
% 116.95/117.09 % SZS output end Proof
% 116.95/117.09 % Total time :116.340000s
%------------------------------------------------------------------------------