%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT002-4 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n020.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 04:40:08 EDT 2024
% Result : Unsatisfiable 59.29s 59.50s
% Output : CNFRefutation 59.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : CAT002-4 : TPTP v8.2.0. Released v1.0.0.
% 0.06/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.31 % Computer : n020.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Tue Jun 18 12:11:09 EDT 2024
% 0.16/0.31 % CPUTime :
% 0.50/0.57 start to proof:theBenchmark
% 59.29/59.49 %-------------------------------------------
% 59.29/59.49 % File :CSE---1.7
% 59.29/59.49 % Problem :theBenchmark
% 59.29/59.49 % Transform :cnf
% 59.29/59.49 % Format :tptp:raw
% 59.29/59.49 % Command :java -jar mcs_scs.jar %d %s
% 59.29/59.49
% 59.29/59.49 % Result :Theorem 58.740000s
% 59.29/59.49 % Output :CNFRefutation 58.740000s
% 59.29/59.49 %-------------------------------------------
% 59.29/59.49 %--------------------------------------------------------------------------
% 59.29/59.49 % File : CAT002-4 : TPTP v8.2.0. Released v1.0.0.
% 59.29/59.49 % Domain : Category Theory
% 59.29/59.49 % Problem : X and Y monomorphisms, XY well-defined => XY monomorphism
% 59.29/59.49 % Version : [Sco79] axioms : Reduced > Complete.
% 59.29/59.49 % English : If x and y are monomorphisms and xy is well-defined then
% 59.29/59.49 % xy is a monomorphism.
% 59.29/59.49
% 59.29/59.49 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 59.29/59.49 % Source : [TPTP]
% 59.29/59.49 % Names :
% 59.29/59.49
% 59.29/59.49 % Status : Unsatisfiable
% 59.29/59.49 % Rating : 0.06 v8.2.0, 0.00 v7.4.0, 0.11 v7.2.0, 0.12 v7.1.0, 0.14 v7.0.0, 0.00 v5.5.0, 0.19 v5.4.0, 0.20 v5.3.0, 0.25 v5.2.0, 0.12 v5.1.0, 0.29 v4.1.0, 0.22 v4.0.1, 0.33 v3.7.0, 0.17 v3.3.0, 0.14 v3.1.0, 0.11 v2.7.0, 0.17 v2.6.0, 0.00 v2.4.0, 0.33 v2.3.0, 0.17 v2.2.1, 0.33 v2.2.0, 0.29 v2.1.0, 0.40 v2.0.0
% 59.29/59.49 % Syntax : Number of clauses : 17 ( 7 unt; 0 nHn; 14 RR)
% 59.29/59.49 % Number of literals : 31 ( 15 equ; 15 neg)
% 59.29/59.49 % Maximal clause size : 3 ( 1 avg)
% 59.29/59.49 % Maximal term depth : 3 ( 1 avg)
% 59.29/59.49 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 59.29/59.49 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% 59.29/59.49 % Number of variables : 25 ( 2 sgn)
% 59.29/59.49 % SPC : CNF_UNS_RFO_SEQ_HRN
% 59.29/59.49
% 59.29/59.49 % Comments : The dependent axioms have been removed.
% 59.29/59.49 %--------------------------------------------------------------------------
% 59.29/59.49 %----Include Scott's axioms for category theory
% 59.29/59.49 include('Axioms/CAT004-0.ax').
% 59.29/59.49 %--------------------------------------------------------------------------
% 59.29/59.49 cnf(assume_ab_exists,hypothesis,
% 59.29/59.49 there_exists(compose(a,b)) ).
% 59.29/59.49
% 59.29/59.49 cnf(cancellation_for_compose1,hypothesis,
% 59.29/59.49 ( compose(a,X) != Y
% 59.29/59.49 | compose(a,Z) != Y
% 59.29/59.49 | X = Z ) ).
% 59.29/59.49
% 59.29/59.49 cnf(cancellation_for_compose2,hypothesis,
% 59.29/59.49 ( compose(b,X) != Y
% 59.29/59.49 | compose(b,Z) != Y
% 59.29/59.49 | X = Z ) ).
% 59.29/59.49
% 59.29/59.49 cnf(assume_h_exists,hypothesis,
% 59.29/59.49 there_exists(h) ).
% 59.29/59.49
% 59.29/59.49 cnf(ab_h_equals_ab_g,hypothesis,
% 59.29/59.49 compose(compose(a,b),h) = compose(compose(a,b),g) ).
% 59.29/59.49
% 59.29/59.49 cnf(prove_g_equals_h,negated_conjecture,
% 59.29/59.49 g != h ).
% 59.29/59.49
% 59.29/59.49 %--------------------------------------------------------------------------
% 59.29/59.49 %-------------------------------------------
% 59.29/59.49 % Proof found
% 59.29/59.50 % SZS status Theorem for theBenchmark
% 59.29/59.50 % SZS output start Proof
% 59.29/59.50 %ClaNum:27(EqnAxiom:10)
% 59.29/59.50 %VarNum:52(SingletonVarNum:25)
% 59.29/59.50 %MaxLitNum:3
% 59.29/59.50 %MaxfuncDepth:2
% 59.29/59.50 %SharedTerms:11
% 59.29/59.50 %goalClause: 17
% 59.29/59.50 %singleGoalClaCount:1
% 59.29/59.50 [11]P1(a1)
% 59.29/59.50 [17]~E(a1,a7)
% 59.29/59.50 [14]P1(f3(a5,a6))
% 59.29/59.50 [15]E(f3(f3(a5,a6),a1),f3(f3(a5,a6),a7))
% 59.29/59.50 [12]E(f3(x121,f2(x121)),x121)
% 59.29/59.50 [13]E(f3(f4(x131),x131),x131)
% 59.29/59.50 [16]E(f3(f3(x161,x162),x163),f3(x161,f3(x162,x163)))
% 59.29/59.50 [18]P1(x181)+~P1(f2(x181))
% 59.29/59.50 [19]P1(x191)+~P1(f4(x191))
% 59.29/59.50 [20]~P2(x201,x202)+E(x201,x202)
% 59.29/59.50 [22]P1(x221)+~P2(x221,x222)
% 59.29/59.50 [25]E(f4(x251),f2(x252))+~P1(f3(x252,x251))
% 59.29/59.50 [26]P1(f2(x261))+~P1(f3(x261,x262))
% 59.29/59.50 [21]~E(x211,x212)+~P1(x211)+P2(x211,x212)
% 59.29/59.50 [27]~E(f4(x272),f2(x271))+~P1(f2(x271))+P1(f3(x271,x272))
% 59.29/59.50 [23]E(x231,x232)+~E(f3(a5,x231),x233)+~E(f3(a5,x232),x233)
% 59.29/59.50 [24]E(x241,x242)+~E(f3(a6,x241),x243)+~E(f3(a6,x242),x243)
% 59.29/59.50 %EqnAxiom
% 59.29/59.50 [1]E(x11,x11)
% 59.29/59.50 [2]E(x22,x21)+~E(x21,x22)
% 59.29/59.50 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.29/59.50 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 59.29/59.50 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53))
% 59.29/59.50 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62))
% 59.29/59.50 [7]~E(x71,x72)+E(f4(x71),f4(x72))
% 59.29/59.50 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 59.29/59.50 [9]P2(x92,x93)+~E(x91,x92)+~P2(x91,x93)
% 59.29/59.50 [10]P2(x103,x102)+~E(x101,x102)+~P2(x103,x101)
% 59.29/59.50
% 59.29/59.50 %-------------------------------------------
% 59.29/59.51 cnf(28,plain,
% 59.29/59.51 (~P1(x281)+P2(x281,x281)),
% 59.29/59.51 inference(equality_inference,[],[21])).
% 59.29/59.51 cnf(29,plain,
% 59.29/59.51 (~P2(a1,a7)),
% 59.29/59.51 inference(scs_inference,[],[17,20])).
% 59.29/59.51 cnf(31,plain,
% 59.29/59.51 (E(x311,f3(x311,f2(x311)))),
% 59.29/59.51 inference(scs_inference,[],[17,12,20,2])).
% 59.29/59.51 cnf(32,plain,
% 59.29/59.51 (E(f4(a6),f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[17,12,14,20,2,25])).
% 59.29/59.51 cnf(36,plain,
% 59.29/59.51 (~E(a1,f3(f4(a7),a7))),
% 59.29/59.51 inference(scs_inference,[],[17,12,13,14,20,2,25,21,3])).
% 59.29/59.51 cnf(39,plain,
% 59.29/59.51 (P2(f3(a5,a6),f3(a5,a6))),
% 59.29/59.51 inference(scs_inference,[],[17,12,13,14,20,2,25,21,3,8,10])).
% 59.29/59.51 cnf(44,plain,
% 59.29/59.51 (E(f2(a5),f4(a6))),
% 59.29/59.51 inference(scs_inference,[],[36,32,20,2])).
% 59.29/59.51 cnf(45,plain,
% 59.29/59.51 (E(f4(a6),f3(f2(a5),f2(f2(a5))))),
% 59.29/59.51 inference(scs_inference,[],[31,36,32,20,2,3])).
% 59.29/59.51 cnf(47,plain,
% 59.29/59.51 (~P1(f4(a6))+P1(f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[31,36,32,20,2,3,8])).
% 59.29/59.51 cnf(48,plain,
% 59.29/59.51 (~P2(f4(a6),x481)+P1(f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[31,36,32,20,2,3,8,22])).
% 59.29/59.51 cnf(51,plain,
% 59.29/59.51 (E(f3(f2(a5),f2(f2(a5))),f4(a6))),
% 59.29/59.51 inference(scs_inference,[],[45,2])).
% 59.29/59.51 cnf(52,plain,
% 59.29/59.51 (E(f3(f4(f2(a5)),f2(a5)),f4(a6))),
% 59.29/59.51 inference(scs_inference,[],[45,44,13,2,3])).
% 59.29/59.51 cnf(54,plain,
% 59.29/59.51 (~P1(f4(a6))+P1(f3(f2(a5),f2(f2(a5))))),
% 59.29/59.51 inference(scs_inference,[],[45,44,13,2,3,8])).
% 59.29/59.51 cnf(55,plain,
% 59.29/59.51 (~P2(f4(a6),x551)+P1(f3(f2(a5),f2(f2(a5))))),
% 59.29/59.51 inference(scs_inference,[],[45,44,13,2,3,8,22])).
% 59.29/59.51 cnf(58,plain,
% 59.29/59.51 (E(f4(a6),f3(f4(f2(a5)),f2(a5)))),
% 59.29/59.51 inference(scs_inference,[],[52,2])).
% 59.29/59.51 cnf(61,plain,
% 59.29/59.51 (~P2(a1,f3(a7,f2(a7)))),
% 59.29/59.51 inference(scs_inference,[],[17,52,12,2,3,20])).
% 59.29/59.51 cnf(63,plain,
% 59.29/59.51 (~P1(f3(f2(a5),f2(f2(a5))))+P1(f4(a6))),
% 59.29/59.51 inference(scs_inference,[],[17,51,52,12,2,3,20,8])).
% 59.29/59.51 cnf(68,plain,
% 59.29/59.51 (E(f3(x681,f3(x682,x683)),f3(f3(x681,x682),x683))),
% 59.29/59.51 inference(scs_inference,[],[16,2])).
% 59.29/59.51 cnf(70,plain,
% 59.29/59.51 (P1(f3(f4(f2(a5)),f2(a5)))+~P1(f3(f2(a5),f2(f2(a5))))),
% 59.29/59.51 inference(scs_inference,[],[58,16,2,8,63])).
% 59.29/59.51 cnf(80,plain,
% 59.29/59.51 (E(x801,f3(f4(x801),x801))),
% 59.29/59.51 inference(scs_inference,[],[13,2])).
% 59.29/59.51 cnf(82,plain,
% 59.29/59.51 (E(f3(a5,f3(a6,a1)),f3(f3(a5,a6),a7))),
% 59.29/59.51 inference(scs_inference,[],[68,14,13,15,2,8,3])).
% 59.29/59.51 cnf(84,plain,
% 59.29/59.51 (E(f3(f3(a5,a6),a7),f3(a5,f3(a6,a1)))),
% 59.29/59.51 inference(scs_inference,[],[82,2])).
% 59.29/59.51 cnf(85,plain,
% 59.29/59.51 (~P1(f2(a5))+P1(f4(a6))),
% 59.29/59.51 inference(scs_inference,[],[44,82,2,8])).
% 59.29/59.51 cnf(91,plain,
% 59.29/59.51 (E(f3(a5,f3(a6,a7)),f3(a5,f3(a6,a1)))),
% 59.29/59.51 inference(scs_inference,[],[84,68,15,2,3])).
% 59.29/59.51 cnf(134,plain,
% 59.29/59.51 (P1(f3(a1,f2(a1)))),
% 59.29/59.51 inference(scs_inference,[],[11,31,8])).
% 59.29/59.51 cnf(138,plain,
% 59.29/59.51 (E(f2(a1),f4(f2(a1)))),
% 59.29/59.51 inference(scs_inference,[],[11,31,8,25,2])).
% 59.29/59.51 cnf(139,plain,
% 59.29/59.51 (P2(f3(a1,f2(a1)),a1)),
% 59.29/59.51 inference(scs_inference,[],[11,31,28,9])).
% 59.29/59.51 cnf(140,plain,
% 59.29/59.51 (P2(f3(a1,f2(a1)),f3(a1,f2(a1)))),
% 59.29/59.51 inference(scs_inference,[],[31,139,10])).
% 59.29/59.51 cnf(142,plain,
% 59.29/59.51 (P1(f3(f4(a1),a1))),
% 59.29/59.51 inference(scs_inference,[],[11,31,80,139,10,8])).
% 59.29/59.51 cnf(144,plain,
% 59.29/59.51 (E(f4(a1),f2(f4(a1)))),
% 59.29/59.51 inference(scs_inference,[],[11,31,80,139,10,8,25])).
% 59.29/59.51 cnf(146,plain,
% 59.29/59.51 (E(f2(f4(a1)),f4(a1))),
% 59.29/59.51 inference(scs_inference,[],[11,31,80,139,10,8,25,2])).
% 59.29/59.51 cnf(147,plain,
% 59.29/59.51 (~P1(f3(f2(a5),f2(f2(a5))))+P1(f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[47,63])).
% 59.29/59.51 cnf(148,plain,
% 59.29/59.51 (~P1(f2(a1))+P1(f4(f2(a1)))),
% 59.29/59.51 inference(scs_inference,[],[138,8])).
% 59.29/59.51 cnf(153,plain,
% 59.29/59.51 (P1(f4(a6))),
% 59.29/59.51 inference(scs_inference,[],[14,85,26])).
% 59.29/59.51 cnf(154,plain,
% 59.29/59.51 (P1(f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[153,47])).
% 59.29/59.51 cnf(155,plain,
% 59.29/59.51 (P1(f3(f2(a5),f2(f2(a5))))),
% 59.29/59.51 inference(scs_inference,[],[153,54])).
% 59.29/59.51 cnf(157,plain,
% 59.29/59.51 (P1(a6)),
% 59.29/59.51 inference(scs_inference,[],[153,19])).
% 59.29/59.51 cnf(159,plain,
% 59.29/59.51 (P2(f4(a6),f3(f4(a6),f2(f4(a6))))),
% 59.29/59.51 inference(scs_inference,[],[31,153,19,21])).
% 59.29/59.51 cnf(166,plain,
% 59.29/59.51 (P1(f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[159,48])).
% 59.29/59.51 cnf(167,plain,
% 59.29/59.51 (P1(f3(f2(a5),f2(f2(a5))))),
% 59.29/59.51 inference(scs_inference,[],[159,55])).
% 59.29/59.51 cnf(168,plain,
% 59.29/59.51 (P1(f3(f4(f2(a5)),f2(a5)))),
% 59.29/59.51 inference(scs_inference,[],[155,70])).
% 59.29/59.51 cnf(170,plain,
% 59.29/59.51 (P1(f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[155,147])).
% 59.29/59.51 cnf(172,plain,
% 59.29/59.51 (P1(a5)),
% 59.29/59.51 inference(scs_inference,[],[154,18])).
% 59.29/59.51 cnf(175,plain,
% 59.29/59.51 (E(x1751,f3(f4(x1751),x1751))),
% 59.29/59.51 inference(rename_variables,[],[80])).
% 59.29/59.51 cnf(177,plain,
% 59.29/59.51 (P2(f3(a1,f2(a1)),f3(f4(a1),a1))),
% 59.29/59.51 inference(scs_inference,[],[80,175,14,139,154,18,21,10])).
% 59.29/59.51 cnf(178,plain,
% 59.29/59.51 (E(x1781,f3(f4(x1781),x1781))),
% 59.29/59.51 inference(rename_variables,[],[80])).
% 59.29/59.51 cnf(183,plain,
% 59.29/59.51 (E(f4(f2(a1)),f3(f4(f2(a1)),f2(a1)))),
% 59.29/59.51 inference(scs_inference,[],[80,175,178,138,14,39,13,139,154,18,21,10,3,9,2])).
% 59.29/59.51 cnf(189,plain,
% 59.29/59.51 (P2(f4(a6),f3(f4(f4(a6)),f4(a6)))),
% 59.29/59.51 inference(scs_inference,[],[80,153,21])).
% 59.29/59.51 cnf(192,plain,
% 59.29/59.51 (~P1(f4(f2(a1)))+P1(f3(f4(f2(a1)),f2(a1)))),
% 59.29/59.51 inference(scs_inference,[],[80,183,153,21,8])).
% 59.29/59.51 cnf(193,plain,
% 59.29/59.51 (P2(f2(a5),f4(a6))),
% 59.29/59.51 inference(scs_inference,[],[44,166,21])).
% 59.29/59.51 cnf(197,plain,
% 59.29/59.51 (P2(f4(a6),f4(a6))),
% 59.29/59.51 inference(scs_inference,[],[44,31,166,21,10,9])).
% 59.29/59.51 cnf(205,plain,
% 59.29/59.51 (P2(a6,f3(a6,f2(a6)))),
% 59.29/59.51 inference(scs_inference,[],[31,157,21])).
% 59.29/59.51 cnf(206,plain,
% 59.29/59.51 (E(x2061,f3(x2061,f2(x2061)))),
% 59.29/59.51 inference(rename_variables,[],[31])).
% 59.29/59.51 cnf(208,plain,
% 59.29/59.51 (P2(f3(a6,f2(a6)),f3(a6,f2(a6)))),
% 59.29/59.51 inference(scs_inference,[],[31,206,157,21,9])).
% 59.29/59.51 cnf(210,plain,
% 59.29/59.51 (P2(a5,f3(a5,f2(a5)))),
% 59.29/59.51 inference(scs_inference,[],[31,172,21])).
% 59.29/59.51 cnf(211,plain,
% 59.29/59.51 (E(x2111,f3(x2111,f2(x2111)))),
% 59.29/59.51 inference(rename_variables,[],[31])).
% 59.29/59.51 cnf(213,plain,
% 59.29/59.51 (P2(f3(a5,f2(a5)),f3(a5,f2(a5)))),
% 59.29/59.51 inference(scs_inference,[],[31,211,172,21,9])).
% 59.29/59.51 cnf(215,plain,
% 59.29/59.51 (P2(f3(f2(a5),f2(f2(a5))),f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[12,167,21])).
% 59.29/59.51 cnf(216,plain,
% 59.29/59.51 (E(f3(x2161,f2(x2161)),x2161)),
% 59.29/59.51 inference(rename_variables,[],[12])).
% 59.29/59.51 cnf(218,plain,
% 59.29/59.51 (P2(a6,a6)),
% 59.29/59.51 inference(scs_inference,[],[12,216,205,167,21,10])).
% 59.29/59.51 cnf(219,plain,
% 59.29/59.51 (E(f3(x2191,f2(x2191)),x2191)),
% 59.29/59.51 inference(rename_variables,[],[12])).
% 59.29/59.51 cnf(220,plain,
% 59.29/59.51 (E(f3(f4(a6),f2(f4(a6))),f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[12,216,219,205,32,167,21,10,3])).
% 59.29/59.51 cnf(221,plain,
% 59.29/59.51 (E(f3(x2211,f2(x2211)),x2211)),
% 59.29/59.51 inference(rename_variables,[],[12])).
% 59.29/59.51 cnf(222,plain,
% 59.29/59.51 (P2(a1,a1)),
% 59.29/59.51 inference(scs_inference,[],[12,216,219,221,205,32,139,167,21,10,3,9])).
% 59.29/59.51 cnf(227,plain,
% 59.29/59.51 (P2(a5,a5)),
% 59.29/59.51 inference(scs_inference,[],[12,210,10])).
% 59.29/59.51 cnf(228,plain,
% 59.29/59.51 (E(f3(x2281,f2(x2281)),x2281)),
% 59.29/59.51 inference(rename_variables,[],[12])).
% 59.29/59.51 cnf(229,plain,
% 59.29/59.51 (P2(f2(a5),f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[12,228,210,215,10,9])).
% 59.29/59.51 cnf(231,plain,
% 59.29/59.51 (P2(f3(a6,f2(a6)),a6)),
% 59.29/59.51 inference(scs_inference,[],[12,208,10])).
% 59.29/59.51 cnf(232,plain,
% 59.29/59.51 (E(f3(x2321,f2(x2321)),x2321)),
% 59.29/59.51 inference(rename_variables,[],[12])).
% 59.29/59.51 cnf(233,plain,
% 59.29/59.51 (P2(a1,f3(a1,f2(a1)))),
% 59.29/59.51 inference(scs_inference,[],[12,232,140,208,10,9])).
% 59.29/59.51 cnf(235,plain,
% 59.29/59.51 (E(f2(x2351),f2(f3(x2351,f2(x2351))))),
% 59.29/59.51 inference(scs_inference,[],[12,4,2])).
% 59.29/59.51 cnf(236,plain,
% 59.29/59.51 (E(f2(f3(x2361,f2(x2361))),f2(x2361))),
% 59.29/59.51 inference(scs_inference,[],[235,2])).
% 59.29/59.51 cnf(237,plain,
% 59.29/59.51 (P2(f3(a5,f2(a5)),a5)),
% 59.29/59.51 inference(scs_inference,[],[12,235,213,2,10])).
% 59.29/59.51 cnf(238,plain,
% 59.29/59.51 (E(f3(x2381,f2(x2381)),x2381)),
% 59.29/59.51 inference(rename_variables,[],[12])).
% 59.29/59.51 cnf(243,plain,
% 59.29/59.51 (P1(f3(a5,f2(a5)))),
% 59.29/59.51 inference(scs_inference,[],[12,238,154,235,177,213,2,10,8,9,18])).
% 59.29/59.51 cnf(245,plain,
% 59.29/59.51 (E(f4(f2(a5)),f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[12,238,154,235,177,213,2,10,8,9,18,25])).
% 59.29/59.51 cnf(248,plain,
% 59.29/59.51 (E(f2(a5),f4(f2(a5)))),
% 59.29/59.51 inference(scs_inference,[],[245,2])).
% 59.29/59.51 cnf(250,plain,
% 59.29/59.51 (P1(f4(f2(a5)))),
% 59.29/59.51 inference(scs_inference,[],[29,166,245,233,2,10,8])).
% 59.29/59.51 cnf(252,plain,
% 59.29/59.51 (~P2(f3(a1,f2(a1)),a7)),
% 59.29/59.51 inference(scs_inference,[],[29,44,166,229,245,233,2,10,8,9,20])).
% 59.29/59.51 cnf(262,plain,
% 59.29/59.51 (~P2(f3(f4(a1),a1),a7)),
% 59.29/59.51 inference(scs_inference,[],[252,177,10,20])).
% 59.29/59.51 cnf(273,plain,
% 59.29/59.51 (P2(f3(f4(f2(a5)),f2(a5)),f2(a5))),
% 59.29/59.51 inference(scs_inference,[],[13,168,21])).
% 59.29/59.51 cnf(282,plain,
% 59.29/59.51 (E(f2(f4(a1)),f3(f4(f4(a1)),f4(a1)))),
% 59.29/59.51 inference(scs_inference,[],[13,144,3,2])).
% 59.29/59.51 cnf(284,plain,
% 59.29/59.51 (P1(f4(a1))+~P1(f3(f4(f4(a1)),f4(a1)))),
% 59.29/59.51 inference(scs_inference,[],[13,144,3,2,8,18])).
% 59.29/59.51 cnf(288,plain,
% 59.29/59.51 (P2(f4(a1),f4(a1))+~P1(f3(f4(f4(a1)),f4(a1)))),
% 59.29/59.51 inference(scs_inference,[],[13,146,144,3,2,8,18,21,9])).
% 59.29/59.51 cnf(293,plain,
% 59.29/59.51 (E(f2(a5),f3(f4(f4(a6)),f4(a6)))),
% 59.29/59.51 inference(scs_inference,[],[13,32,3,2])).
% 59.29/59.51 cnf(294,plain,
% 59.29/59.52 (~P1(f2(f4(a1)))+P1(f3(f4(f4(a1)),f4(a1)))),
% 59.29/59.52 inference(scs_inference,[],[13,282,32,3,2,8])).
% 59.29/59.52 cnf(301,plain,
% 59.29/59.52 (P1(f3(f4(f4(a6)),f4(a6)))),
% 59.29/59.52 inference(scs_inference,[],[293,170,8])).
% 59.29/59.52 cnf(302,plain,
% 59.29/59.52 (P2(f3(f4(f4(a6)),f4(a6)),f4(a6))),
% 59.29/59.52 inference(scs_inference,[],[13,293,170,8,21])).
% 59.29/59.52 cnf(308,plain,
% 59.29/59.52 (E(f4(a6),f2(f3(a5,f2(a5))))),
% 59.29/59.52 inference(scs_inference,[],[44,236,3,2])).
% 59.29/59.52 cnf(346,plain,
% 59.29/59.52 (P2(f3(f4(f4(a6)),f4(a6)),f2(a5))),
% 59.29/59.52 inference(scs_inference,[],[32,248,302,3,10])).
% 59.29/59.52 cnf(348,plain,
% 59.29/59.52 (E(f4(f2(a5)),f4(a6))),
% 59.29/59.52 inference(scs_inference,[],[32,248,189,302,3,10,9,2])).
% 59.29/59.52 cnf(363,plain,
% 59.29/59.52 (P2(f2(a5),f3(f4(f2(a5)),f2(a5)))),
% 59.29/59.52 inference(scs_inference,[],[58,193,153,21,10])).
% 59.29/59.52 cnf(368,plain,
% 59.29/59.52 (E(f3(x3681,f2(f3(a5,x3681))),x3681)),
% 59.29/59.52 inference(scs_inference,[],[68,31,23])).
% 59.29/59.52 cnf(369,plain,
% 59.29/59.52 (E(x3691,f3(x3691,f2(x3691)))),
% 59.29/59.52 inference(rename_variables,[],[31])).
% 59.29/59.52 cnf(370,plain,
% 59.29/59.52 (E(f3(x3701,f3(x3702,x3703)),f3(f3(x3701,x3702),x3703))),
% 59.29/59.52 inference(rename_variables,[],[68])).
% 59.29/59.52 cnf(372,plain,
% 59.29/59.52 (E(f3(x3721,f2(f3(a6,x3721))),x3721)),
% 59.29/59.52 inference(scs_inference,[],[68,370,31,369,23,24])).
% 59.29/59.52 cnf(386,plain,
% 59.29/59.52 (E(x3861,f3(x3861,f2(f3(a5,x3861))))),
% 59.29/59.52 inference(scs_inference,[],[368,2])).
% 59.29/59.52 cnf(393,plain,
% 59.29/59.52 (E(x3931,f3(x3931,f2(f3(a6,x3931))))),
% 59.29/59.52 inference(scs_inference,[],[372,2])).
% 59.29/59.52 cnf(397,plain,
% 59.29/59.52 (E(x3971,f3(f4(x3971),x3971))),
% 59.29/59.52 inference(rename_variables,[],[80])).
% 59.29/59.52 cnf(400,plain,
% 59.29/59.52 (E(x4001,f3(f4(x4001),x4001))),
% 59.29/59.52 inference(rename_variables,[],[80])).
% 59.29/59.52 cnf(401,plain,
% 59.29/59.52 (P2(f3(f4(a6),a6),f3(a6,f2(a6)))),
% 59.29/59.52 inference(scs_inference,[],[80,397,400,205,227,157,21,10,9])).
% 59.29/59.52 cnf(403,plain,
% 59.29/59.52 (P2(f3(a5,f2(a5)),f3(f4(a5),a5))),
% 59.29/59.52 inference(scs_inference,[],[80,237,10])).
% 59.29/59.52 cnf(404,plain,
% 59.29/59.52 (E(x4041,f3(f4(x4041),x4041))),
% 59.29/59.52 inference(rename_variables,[],[80])).
% 59.29/59.52 cnf(405,plain,
% 59.29/59.52 (P2(f3(f4(a5),a5),f3(a5,f2(a5)))),
% 59.29/59.52 inference(scs_inference,[],[80,404,210,237,10,9])).
% 59.29/59.52 cnf(407,plain,
% 59.29/59.52 (P2(f3(a6,f2(a6)),f3(f4(a6),a6))),
% 59.29/59.52 inference(scs_inference,[],[80,231,10])).
% 59.29/59.52 cnf(446,plain,
% 59.29/59.52 (E(f4(f2(a6)),f2(a6))),
% 59.29/59.52 inference(scs_inference,[],[157,31,8,25])).
% 59.29/59.52 cnf(448,plain,
% 59.29/59.52 (E(f2(a6),f4(f2(a6)))),
% 59.29/59.52 inference(scs_inference,[],[157,31,8,25,2])).
% 59.29/59.52 cnf(450,plain,
% 59.29/59.52 (P1(f3(f4(a6),a6))),
% 59.29/59.52 inference(scs_inference,[],[157,80,8])).
% 59.29/59.52 cnf(452,plain,
% 59.29/59.52 (E(f4(a6),f2(f4(a6)))),
% 59.29/59.52 inference(scs_inference,[],[157,80,8,25])).
% 59.29/59.52 cnf(454,plain,
% 59.29/59.52 (E(f2(f4(a6)),f4(a6))),
% 59.29/59.52 inference(scs_inference,[],[157,80,8,25,2])).
% 59.29/59.52 cnf(460,plain,
% 59.29/59.52 (E(f2(a6),f4(f2(f3(a5,a6))))),
% 59.29/59.52 inference(scs_inference,[],[157,386,8,25,2])).
% 59.29/59.52 cnf(469,plain,
% 59.29/59.52 (E(f2(a6),f4(f2(f3(a6,a6))))),
% 59.29/59.52 inference(scs_inference,[],[157,393,8,25,2])).
% 59.29/59.52 cnf(474,plain,
% 59.29/59.52 (P1(f2(f4(a6)))),
% 59.29/59.52 inference(scs_inference,[],[153,452,8])).
% 59.29/59.52 cnf(476,plain,
% 59.29/59.52 (~P1(f2(a6))+P1(f4(f2(a6)))),
% 59.29/59.52 inference(scs_inference,[],[448,8])).
% 59.29/59.52 cnf(481,plain,
% 59.29/59.52 (P2(f4(f2(a6)),f4(f2(a6)))+~P1(f2(a6))),
% 59.29/59.52 inference(scs_inference,[],[476,28])).
% 59.29/59.52 cnf(482,plain,
% 59.29/59.52 (~P1(f2(a6))+P1(f4(f2(f3(a5,a6))))),
% 59.29/59.52 inference(scs_inference,[],[460,8])).
% 59.29/59.52 cnf(488,plain,
% 59.29/59.52 (~P1(f2(a6))+P1(f4(f2(f3(a6,a6))))),
% 59.29/59.52 inference(scs_inference,[],[469,8])).
% 59.29/59.52 cnf(493,plain,
% 59.29/59.52 (P1(f2(f3(a5,a6)))+~P1(f2(a6))),
% 59.29/59.52 inference(scs_inference,[],[482,19])).
% 59.29/59.52 cnf(498,plain,
% 59.29/59.52 (P2(f2(f3(a5,a6)),f2(f3(a5,a6)))+~P1(f2(a6))),
% 59.29/59.52 inference(scs_inference,[],[493,28])).
% 59.29/59.52 cnf(520,plain,
% 59.29/59.52 (E(f4(a5),f2(f4(a5)))),
% 59.29/59.52 inference(scs_inference,[],[172,80,8,25])).
% 59.29/59.52 cnf(522,plain,
% 59.29/59.52 (E(f2(f4(a5)),f4(a5))),
% 59.29/59.52 inference(scs_inference,[],[172,80,8,25,2])).
% 59.29/59.52 cnf(528,plain,
% 59.29/59.52 (E(f2(a5),f4(f2(f3(a5,a5))))),
% 59.29/59.52 inference(scs_inference,[],[172,386,8,25,2])).
% 59.29/59.52 cnf(536,plain,
% 59.29/59.52 (E(f2(a5),f4(f2(f3(a6,a5))))),
% 59.29/59.52 inference(scs_inference,[],[172,393,8,25,2])).
% 59.29/59.52 cnf(542,plain,
% 59.29/59.52 (P1(f2(f3(a5,a5)))),
% 59.29/59.52 inference(scs_inference,[],[528,166,8,19])).
% 59.29/59.52 cnf(544,plain,
% 59.29/59.52 (P1(f3(a5,a5))),
% 59.29/59.52 inference(scs_inference,[],[528,166,8,19,18])).
% 59.29/59.52 cnf(546,plain,
% 59.29/59.52 (E(f4(a5),f2(a5))),
% 59.29/59.52 inference(scs_inference,[],[528,166,8,19,18,25])).
% 59.29/59.52 cnf(548,plain,
% 59.29/59.52 (E(f2(a5),f4(a5))),
% 59.29/59.52 inference(scs_inference,[],[528,166,8,19,18,25,2])).
% 59.29/59.52 cnf(554,plain,
% 59.29/59.52 (P1(f2(f3(a6,a5)))),
% 59.29/59.52 inference(scs_inference,[],[536,170,8,19])).
% 59.29/59.52 cnf(556,plain,
% 59.29/59.52 (P1(f3(a6,a5))),
% 59.29/59.52 inference(scs_inference,[],[536,170,8,19,18])).
% 59.29/59.52 cnf(558,plain,
% 59.29/59.52 (E(f4(a5),f2(a6))),
% 59.29/59.52 inference(scs_inference,[],[536,170,8,19,18,25])).
% 59.29/59.52 cnf(560,plain,
% 59.29/59.52 (E(f2(a6),f4(a5))),
% 59.29/59.52 inference(scs_inference,[],[536,170,8,19,18,25,2])).
% 59.29/59.52 cnf(565,plain,
% 59.29/59.52 (P1(f4(a5))),
% 59.29/59.52 inference(scs_inference,[],[548,154,8])).
% 59.29/59.52 cnf(570,plain,
% 59.29/59.52 (P1(f2(f4(a5)))),
% 59.29/59.52 inference(scs_inference,[],[520,565,8])).
% 59.29/59.52 cnf(572,plain,
% 59.29/59.52 (P1(f2(a6))),
% 59.29/59.52 inference(scs_inference,[],[558,565,8])).
% 59.29/59.52 cnf(573,plain,
% 59.29/59.52 (P2(f4(f2(a6)),f4(f2(a6)))),
% 59.29/59.52 inference(scs_inference,[],[558,565,8,481])).
% 59.29/59.52 cnf(575,plain,
% 59.29/59.52 (P1(f4(f2(a6)))),
% 59.29/59.52 inference(scs_inference,[],[558,565,8,481,498,476])).
% 59.29/59.52 cnf(584,plain,
% 59.29/59.52 (P1(f3(a6,a6))),
% 59.29/59.52 inference(scs_inference,[],[31,558,565,8,481,498,476,482,488,493,19,21,18])).
% 59.29/59.52 cnf(586,plain,
% 59.29/59.52 (E(f4(a6),f2(a6))),
% 59.29/59.52 inference(scs_inference,[],[31,558,565,8,481,498,476,482,488,493,19,21,18,25])).
% 59.29/59.52 cnf(588,plain,
% 59.29/59.52 (E(f2(a6),f4(a6))),
% 59.29/59.52 inference(scs_inference,[],[31,558,565,8,481,498,476,482,488,493,19,21,18,25,2])).
% 59.29/59.52 cnf(607,plain,
% 59.29/59.52 (E(f4(a5),f3(f4(a6),f2(f4(a6))))),
% 59.29/59.52 inference(scs_inference,[],[220,548,3,2])).
% 59.29/59.52 cnf(624,plain,
% 59.29/59.52 (P2(f2(a6),f2(f3(a6,f2(a6))))),
% 59.29/59.52 inference(scs_inference,[],[235,572,21])).
% 59.29/59.52 cnf(632,plain,
% 59.29/59.52 (E(f2(f3(x6321,f2(x6321))),f2(x6321))),
% 59.29/59.52 inference(rename_variables,[],[236])).
% 59.29/59.52 cnf(638,plain,
% 59.29/59.52 (P1(f2(f3(a6,f2(a6))))),
% 59.29/59.52 inference(scs_inference,[],[236,632,31,560,624,565,3,10,9,2,8])).
% 59.29/59.52 cnf(645,plain,
% 59.29/59.52 (E(f4(a6),f2(f3(a6,f2(a6))))),
% 59.29/59.52 inference(scs_inference,[],[236,588,3,2])).
% 59.29/59.52 cnf(647,plain,
% 59.29/59.52 (E(f2(f3(a5,f2(a5))),f4(a5))),
% 59.29/59.52 inference(scs_inference,[],[236,548,3])).
% 59.29/59.52 cnf(652,plain,
% 59.29/59.52 (P2(f4(f2(a5)),f2(a5))),
% 59.29/59.52 inference(scs_inference,[],[245,250,21])).
% 59.29/59.52 cnf(658,plain,
% 59.29/59.52 (E(f4(a5),f4(f2(a5)))),
% 59.29/59.52 inference(scs_inference,[],[245,548,3,2])).
% 59.29/59.52 cnf(660,plain,
% 59.29/59.52 (P2(f2(a5),f4(f2(a5)))),
% 59.29/59.52 inference(scs_inference,[],[248,170,21])).
% 59.29/59.52 cnf(663,plain,
% 59.29/59.52 (P2(f4(f2(a5)),f4(a6))),
% 59.29/59.52 inference(scs_inference,[],[248,193,273,170,21,10,9])).
% 59.29/59.52 cnf(701,plain,
% 59.29/59.52 (E(f4(a6),f4(a5))),
% 59.29/59.52 inference(scs_inference,[],[308,647,3])).
% 59.29/59.52 cnf(702,plain,
% 59.29/59.52 (E(f4(a5),f4(a6))),
% 59.29/59.52 inference(scs_inference,[],[308,647,3,2])).
% 59.29/59.52 cnf(707,plain,
% 59.29/59.52 (E(f4(f2(a5)),f2(f4(a6)))),
% 59.29/59.52 inference(scs_inference,[],[348,452,3])).
% 59.29/59.52 cnf(711,plain,
% 59.29/59.52 (E(f2(a6),f4(f2(a5)))),
% 59.29/59.52 inference(scs_inference,[],[348,586,3,2])).
% 59.29/59.52 cnf(717,plain,
% 59.29/59.52 (E(x7171,f3(x7171,f2(f3(a5,x7171))))),
% 59.29/59.52 inference(rename_variables,[],[386])).
% 59.29/59.52 cnf(720,plain,
% 59.29/59.52 (E(x7201,f3(x7201,f2(f3(a5,x7201))))),
% 59.29/59.52 inference(rename_variables,[],[386])).
% 59.29/59.52 cnf(721,plain,
% 59.29/59.52 (P2(f3(a1,f2(f3(a5,a1))),a1)),
% 59.29/59.52 inference(scs_inference,[],[386,717,720,218,222,172,21,10,9])).
% 59.29/59.52 cnf(728,plain,
% 59.29/59.52 (E(x7281,f3(x7281,f2(f3(a6,x7281))))),
% 59.29/59.52 inference(rename_variables,[],[393])).
% 59.29/59.52 cnf(731,plain,
% 59.29/59.52 (E(x7311,f3(x7311,f2(f3(a6,x7311))))),
% 59.29/59.52 inference(rename_variables,[],[393])).
% 59.29/59.52 cnf(732,plain,
% 59.29/59.52 (P2(f3(a1,f2(f3(a6,a1))),a1)),
% 59.29/59.52 inference(scs_inference,[],[393,728,731,218,222,172,21,10,9])).
% 59.29/59.52 cnf(748,plain,
% 59.29/59.52 (E(f4(f2(a5)),f4(f2(a6)))),
% 59.29/59.52 inference(scs_inference,[],[446,711,573,575,21,3,9,2])).
% 59.29/59.52 cnf(750,plain,
% 59.29/59.52 (E(f4(a5),f4(f2(a6)))),
% 59.29/59.52 inference(scs_inference,[],[446,560,3,2])).
% 59.29/59.52 cnf(752,plain,
% 59.29/59.52 (E(f4(a6),f4(f2(a6)))),
% 59.29/59.52 inference(scs_inference,[],[446,588,3,2])).
% 59.29/59.52 cnf(764,plain,
% 59.29/59.52 (P2(f2(f4(a6)),f4(a6))),
% 59.29/59.52 inference(scs_inference,[],[452,197,663,10,9])).
% 59.29/59.52 cnf(777,plain,
% 59.29/59.52 (E(f4(f2(a6)),f2(f4(a6)))),
% 59.29/59.52 inference(scs_inference,[],[454,752,3,2])).
% 59.29/59.52 cnf(810,plain,
% 59.29/59.52 (P1(f2(f2(a5)))),
% 59.29/59.52 inference(scs_inference,[],[215,22,26])).
% 59.29/59.52 cnf(812,plain,
% 59.29/59.52 (P2(f4(a5),f2(f4(a5)))),
% 59.29/59.52 inference(scs_inference,[],[520,565,21])).
% 59.29/59.52 cnf(815,plain,
% 59.29/59.52 (P2(f4(a5),f4(a5))),
% 59.29/59.52 inference(scs_inference,[],[522,570,28,8])).
% 59.29/59.52 cnf(816,plain,
% 59.29/59.52 (P2(f2(f4(a5)),f4(a5))),
% 59.29/59.52 inference(scs_inference,[],[522,570,21])).
% 59.29/59.52 cnf(819,plain,
% 59.29/59.52 (P2(f3(f4(a5),f2(f4(a5))),f4(a5))),
% 59.29/59.52 inference(scs_inference,[],[522,31,702,815,570,21,3,9])).
% 59.29/59.52 cnf(821,plain,
% 59.29/59.52 (E(f4(a6),f2(f4(a5)))),
% 59.29/59.52 inference(scs_inference,[],[522,31,702,815,570,21,3,9,2])).
% 59.29/59.52 cnf(880,plain,
% 59.41/59.52 (P2(f2(a5),f4(f2(f3(a6,a5))))),
% 59.41/59.52 inference(scs_inference,[],[536,170,21])).
% 59.41/59.52 cnf(900,plain,
% 59.41/59.52 (P1(f3(f4(f3(a5,a5)),f3(a5,a5)))),
% 59.41/59.52 inference(scs_inference,[],[544,80,8])).
% 59.41/59.52 cnf(902,plain,
% 59.41/59.52 (E(f2(f2(a5)),f2(f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[193,20,4])).
% 59.41/59.52 cnf(904,plain,
% 59.41/59.52 (P2(f4(a5),f2(a5))),
% 59.41/59.52 inference(scs_inference,[],[546,902,565,2,21])).
% 59.41/59.52 cnf(906,plain,
% 59.41/59.52 (P2(f2(f4(a5)),f2(a5))),
% 59.41/59.52 inference(scs_inference,[],[546,816,902,565,2,21,10])).
% 59.41/59.52 cnf(907,plain,
% 59.41/59.52 (P2(f2(a5),f2(f4(a5)))),
% 59.41/59.52 inference(scs_inference,[],[546,816,812,902,565,2,21,10,9])).
% 59.41/59.52 cnf(908,plain,
% 59.41/59.52 (E(f3(f2(a5),x9081),f3(f4(a6),x9081))),
% 59.41/59.52 inference(scs_inference,[],[193,20,5])).
% 59.41/59.52 cnf(909,plain,
% 59.41/59.52 (E(f3(f4(a6),x9091),f3(f2(a5),x9091))),
% 59.41/59.52 inference(scs_inference,[],[908,2])).
% 59.41/59.52 cnf(910,plain,
% 59.41/59.52 (P2(f4(a5),f3(f2(a5),f2(f2(a5))))),
% 59.41/59.52 inference(scs_inference,[],[31,904,908,2,10])).
% 59.41/59.52 cnf(915,plain,
% 59.41/59.52 (E(f3(x9151,f2(a5)),f3(x9151,f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[193,20,6])).
% 59.41/59.52 cnf(916,plain,
% 59.41/59.52 (E(f3(x9161,f4(a6)),f3(x9161,f2(a5)))),
% 59.41/59.52 inference(scs_inference,[],[915,2])).
% 59.41/59.52 cnf(920,plain,
% 59.41/59.52 (P2(f2(a5),f4(a5))),
% 59.41/59.52 inference(scs_inference,[],[546,909,815,450,819,915,2,10,8,9])).
% 59.41/59.52 cnf(921,plain,
% 59.41/59.52 (E(f4(a6),f2(f2(a5)))),
% 59.41/59.52 inference(scs_inference,[],[546,909,815,450,819,915,2,10,8,9,25])).
% 59.41/59.52 cnf(923,plain,
% 59.41/59.52 (E(f4(f2(a5)),f4(f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[193,20,7])).
% 59.41/59.52 cnf(924,plain,
% 59.41/59.52 (E(f2(f2(a5)),f4(a6))),
% 59.41/59.52 inference(scs_inference,[],[921,2])).
% 59.41/59.52 cnf(925,plain,
% 59.41/59.52 (P2(f4(a5),f4(a6))),
% 59.41/59.52 inference(scs_inference,[],[51,910,921,2,10])).
% 59.41/59.52 cnf(926,plain,
% 59.41/59.52 (P1(f3(f4(f4(a6)),f2(a5)))),
% 59.41/59.52 inference(scs_inference,[],[51,916,301,910,921,2,10,8])).
% 59.41/59.52 cnf(928,plain,
% 59.41/59.52 (P2(f3(f2(a5),f2(f2(a5))),f4(a5))),
% 59.41/59.52 inference(scs_inference,[],[51,31,916,301,910,921,920,2,10,8,9])).
% 59.41/59.52 cnf(933,plain,
% 59.41/59.52 (P1(f4(f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[31,250,923,925,2,10,8])).
% 59.41/59.52 cnf(934,plain,
% 59.41/59.52 (P2(f4(a6),f4(a5))),
% 59.41/59.52 inference(scs_inference,[],[51,31,250,928,923,925,2,10,8,9])).
% 59.41/59.52 cnf(935,plain,
% 59.41/59.52 (P1(f3(a5,f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[243,915,8])).
% 59.41/59.52 cnf(939,plain,
% 59.41/59.52 (E(f4(f4(a6)),f2(a5))),
% 59.41/59.52 inference(scs_inference,[],[31,243,934,915,8,9,25])).
% 59.41/59.52 cnf(941,plain,
% 59.41/59.52 (E(f2(a5),f4(f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[31,243,934,915,8,9,25,2])).
% 59.41/59.52 cnf(942,plain,
% 59.41/59.52 (E(f4(a5),f4(f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[546,31,243,934,915,8,9,25,2,3])).
% 59.41/59.52 cnf(943,plain,
% 59.41/59.52 (P1(f4(f2(a1)))),
% 59.41/59.52 inference(scs_inference,[],[134,26,148])).
% 59.41/59.52 cnf(944,plain,
% 59.41/59.52 (P1(f3(f4(f2(a1)),f2(a1)))),
% 59.41/59.52 inference(scs_inference,[],[943,192])).
% 59.41/59.52 cnf(948,plain,
% 59.41/59.52 (E(f4(f4(a6)),f4(a5))),
% 59.41/59.52 inference(scs_inference,[],[942,943,19,2])).
% 59.41/59.52 cnf(955,plain,
% 59.41/59.52 (P1(f3(f4(f4(a1)),f4(a1)))),
% 59.41/59.52 inference(scs_inference,[],[142,26,294])).
% 59.41/59.52 cnf(957,plain,
% 59.41/59.52 (P1(f4(a1))),
% 59.41/59.52 inference(scs_inference,[],[955,284])).
% 59.41/59.52 cnf(959,plain,
% 59.41/59.52 (P2(f4(a1),f4(a1))),
% 59.41/59.52 inference(scs_inference,[],[955,288])).
% 59.41/59.52 cnf(982,plain,
% 59.41/59.52 (P2(f3(f4(a1),f2(f4(a1))),f4(a1))),
% 59.41/59.52 inference(scs_inference,[],[31,959,9])).
% 59.41/59.52 cnf(1001,plain,
% 59.41/59.52 (E(f4(f2(a6)),f2(a5))),
% 59.41/59.52 inference(scs_inference,[],[548,750,880,652,10,3,9,2])).
% 59.41/59.52 cnf(1003,plain,
% 59.41/59.52 (E(f2(a5),f2(a6))),
% 59.41/59.52 inference(scs_inference,[],[548,346,558,10,3])).
% 59.41/59.52 cnf(1005,plain,
% 59.41/59.52 (E(f2(a6),f2(a5))),
% 59.41/59.52 inference(scs_inference,[],[548,363,346,558,10,3,9,2])).
% 59.41/59.52 cnf(1027,plain,
% 59.41/59.52 (P1(f3(f4(f3(a6,a5)),f3(a6,a5)))),
% 59.41/59.52 inference(scs_inference,[],[556,80,8])).
% 59.41/59.52 cnf(1056,plain,
% 59.41/59.52 (P2(f2(f2(a6)),f4(a5))),
% 59.41/59.52 inference(scs_inference,[],[558,816,4,9])).
% 59.41/59.52 cnf(1063,plain,
% 59.41/59.52 (P2(f4(a5),f2(f2(a6)))),
% 59.41/59.52 inference(scs_inference,[],[558,812,4,10])).
% 59.41/59.52 cnf(1086,plain,
% 59.41/59.52 (E(f4(f2(a6)),f4(f4(a5)))),
% 59.41/59.52 inference(scs_inference,[],[558,7,2])).
% 59.41/59.52 cnf(1120,plain,
% 59.41/59.52 (E(f2(a6),f4(f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[560,942,3])).
% 59.41/59.52 cnf(1121,plain,
% 59.41/59.52 (E(f4(f4(a6)),f2(a6))),
% 59.41/59.52 inference(scs_inference,[],[560,942,3,2])).
% 59.41/59.52 cnf(1128,plain,
% 59.41/59.52 (P1(f3(f4(f4(a5)),f4(a5)))),
% 59.41/59.52 inference(scs_inference,[],[565,80,8])).
% 59.41/59.52 cnf(1134,plain,
% 59.41/59.52 (P1(f3(f2(a6),f2(f2(a6))))),
% 59.41/59.52 inference(scs_inference,[],[572,31,8])).
% 59.41/59.52 cnf(1137,plain,
% 59.41/59.52 (P1(f3(f4(f2(a6)),f2(a6)))),
% 59.41/59.52 inference(scs_inference,[],[572,80,8])).
% 59.41/59.52 cnf(1146,plain,
% 59.41/59.52 (P1(f3(f4(f3(a6,a6)),f3(a6,a6)))),
% 59.41/59.52 inference(scs_inference,[],[584,80,8])).
% 59.41/59.52 cnf(1149,plain,
% 59.41/59.52 (E(f3(f2(a6),x11491),f3(f4(a6),x11491))),
% 59.41/59.52 inference(scs_inference,[],[586,5,2])).
% 59.41/59.52 cnf(1150,plain,
% 59.41/59.52 (E(f3(f4(a6),x11501),f3(f2(a6),x11501))),
% 59.41/59.52 inference(scs_inference,[],[1149,2])).
% 59.41/59.52 cnf(1153,plain,
% 59.41/59.52 (E(f4(a6),f4(f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[586,1120,1149,1134,2,8,3])).
% 59.41/59.52 cnf(1155,plain,
% 59.41/59.52 (E(f4(f4(a6)),f4(a6))),
% 59.41/59.52 inference(scs_inference,[],[1153,2])).
% 59.41/59.52 cnf(1191,plain,
% 59.41/59.52 (E(f4(a5),f3(f2(a5),f2(f4(a6))))),
% 59.41/59.52 inference(scs_inference,[],[607,909,3])).
% 59.41/59.52 cnf(1196,plain,
% 59.41/59.52 (E(f4(a5),f3(f2(a6),f2(f4(a6))))),
% 59.41/59.52 inference(scs_inference,[],[607,1191,1150,565,2,8,3])).
% 59.41/59.52 cnf(1205,plain,
% 59.41/59.52 (E(f3(f2(a5),x12051),x12051)),
% 59.41/59.52 inference(scs_inference,[],[31,68,5,23])).
% 59.41/59.52 cnf(1206,plain,
% 59.41/59.52 (E(x12061,f3(f2(a5),x12061))),
% 59.41/59.52 inference(scs_inference,[],[1205,2])).
% 59.41/59.52 cnf(1207,plain,
% 59.41/59.52 (P1(f3(f2(a5),f3(a5,a6)))),
% 59.41/59.52 inference(scs_inference,[],[1205,14,2,8])).
% 59.41/59.52 cnf(1208,plain,
% 59.41/59.52 (E(f4(f3(a5,a6)),f2(f2(a5)))),
% 59.41/59.52 inference(scs_inference,[],[1205,14,2,8,25])).
% 59.41/59.52 cnf(1211,plain,
% 59.41/59.52 (E(f2(f2(a5)),f4(f3(a5,a6)))),
% 59.41/59.52 inference(scs_inference,[],[1208,2])).
% 59.41/59.52 cnf(1212,plain,
% 59.41/59.52 (P1(f4(f3(a5,a6)))),
% 59.41/59.52 inference(scs_inference,[],[1208,810,2,8])).
% 59.41/59.52 cnf(1213,plain,
% 59.41/59.52 (~E(a1,f3(f2(a5),a7))),
% 59.41/59.52 inference(scs_inference,[],[17,1205,1208,810,2,8,3])).
% 59.41/59.52 cnf(1217,plain,
% 59.41/59.52 (E(f3(f2(a6),x12171),x12171)),
% 59.41/59.52 inference(scs_inference,[],[31,68,5,24])).
% 59.41/59.52 cnf(1218,plain,
% 59.41/59.52 (E(x12181,f3(f2(a6),x12181))),
% 59.41/59.52 inference(scs_inference,[],[1217,2])).
% 59.41/59.52 cnf(1219,plain,
% 59.41/59.52 (P1(f3(f2(a6),f3(a5,a6)))),
% 59.41/59.52 inference(scs_inference,[],[1217,14,2,8])).
% 59.41/59.52 cnf(1220,plain,
% 59.41/59.52 (~E(a1,f3(f4(a6),a7))),
% 59.41/59.52 inference(scs_inference,[],[1217,1213,909,14,2,8,3])).
% 59.41/59.52 cnf(1224,plain,
% 59.41/59.52 (E(f4(f3(a5,a6)),f2(f2(a6)))),
% 59.41/59.52 inference(scs_inference,[],[1217,1213,909,14,2,8,3,20,25])).
% 59.41/59.52 cnf(1228,plain,
% 59.41/59.52 (~E(a1,f3(f2(a6),a7))),
% 59.41/59.52 inference(scs_inference,[],[17,1217,1224,2,3])).
% 59.41/59.52 cnf(1230,plain,
% 59.41/59.52 (~P2(a1,f3(f2(a6),a7))),
% 59.41/59.52 inference(scs_inference,[],[17,1217,1224,2,3,20])).
% 59.41/59.52 cnf(1274,plain,
% 59.41/59.52 (P2(f2(f2(a6)),f4(f2(a5)))),
% 59.41/59.52 inference(scs_inference,[],[658,1056,10])).
% 59.41/59.52 cnf(1275,plain,
% 59.41/59.52 (P2(f4(f2(a5)),f2(f2(a6)))),
% 59.41/59.52 inference(scs_inference,[],[658,1063,1056,10,9])).
% 59.41/59.52 cnf(1326,plain,
% 59.41/59.52 (E(f3(x13261,f4(a5)),f3(x13261,f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[701,6,2])).
% 59.41/59.52 cnf(1327,plain,
% 59.41/59.52 (E(f3(x13271,f4(a6)),f3(x13271,f4(a5)))),
% 59.41/59.52 inference(scs_inference,[],[1326,2])).
% 59.41/59.52 cnf(1328,plain,
% 59.41/59.52 (P1(f3(f4(f4(a5)),f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[1326,1128,2,8])).
% 59.41/59.52 cnf(1330,plain,
% 59.41/59.52 (E(f4(a6),f3(f2(a5),f2(f4(a6))))),
% 59.41/59.52 inference(scs_inference,[],[701,1191,1326,1128,2,8,3])).
% 59.41/59.52 cnf(1336,plain,
% 59.41/59.52 (P1(f3(a5,f4(a5)))),
% 59.41/59.52 inference(scs_inference,[],[1327,1330,935,2,8])).
% 59.41/59.52 cnf(1340,plain,
% 59.41/59.52 (~P2(f3(a1,f2(a1)),f3(f2(a6),a7))),
% 59.41/59.52 inference(scs_inference,[],[701,1230,1327,1330,1196,233,935,2,8,3,10,20])).
% 59.41/59.52 cnf(1342,plain,
% 59.41/59.52 (E(f4(f4(a5)),f2(a5))),
% 59.41/59.52 inference(scs_inference,[],[701,1230,1327,1330,1196,233,935,2,8,3,10,20,25])).
% 59.41/59.52 cnf(1349,plain,
% 59.41/59.52 (E(f2(a5),f4(f4(a5)))),
% 59.41/59.52 inference(scs_inference,[],[1342,2])).
% 59.41/59.52 cnf(1350,plain,
% 59.41/59.52 (P1(f3(f4(f4(a5)),f2(a5)))),
% 59.41/59.52 inference(scs_inference,[],[916,1342,1328,2,8])).
% 59.41/59.52 cnf(1357,plain,
% 59.41/59.52 (E(f4(a5),f2(f2(a5)))),
% 59.41/59.52 inference(scs_inference,[],[702,921,3])).
% 59.41/59.52 cnf(1372,plain,
% 59.41/59.52 (P2(f2(f2(a6)),f2(f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[707,1274,10])).
% 59.41/59.52 cnf(1373,plain,
% 59.41/59.52 (P2(f2(f4(a6)),f2(f2(a6)))),
% 59.41/59.52 inference(scs_inference,[],[707,1275,1274,10,9])).
% 59.41/59.52 cnf(1412,plain,
% 59.41/59.52 (P2(f2(a5),f4(f2(a6)))),
% 59.41/59.52 inference(scs_inference,[],[748,660,10])).
% 59.41/59.52 cnf(1433,plain,
% 59.41/59.52 (E(f4(a6),f4(f4(a5)))),
% 59.41/59.52 inference(scs_inference,[],[752,1086,3])).
% 59.41/59.52 cnf(1456,plain,
% 59.41/59.52 (E(f3(f2(a5),x14561),f3(f2(a6),x14561))),
% 59.41/59.52 inference(scs_inference,[],[1003,1336,1206,28,7,5])).
% 59.41/59.52 cnf(1465,plain,
% 59.41/59.52 (~E(a7,a1)),
% 59.41/59.52 inference(scs_inference,[],[17,1003,1336,1206,401,1146,982,28,7,5,6,4,26,22,20,2])).
% 59.41/59.52 cnf(1466,plain,
% 59.41/59.52 (~E(f3(a5,a7),f3(f2(a5),f3(a5,a1)))),
% 59.41/59.52 inference(scs_inference,[],[17,1003,1336,1206,401,1146,982,28,7,5,6,4,26,22,20,2,23])).
% 59.41/59.52 cnf(1467,plain,
% 59.41/59.52 (E(x14671,f3(f2(a5),x14671))),
% 59.41/59.52 inference(rename_variables,[],[1206])).
% 59.41/59.52 cnf(1469,plain,
% 59.41/59.52 (~E(f3(a6,a7),f3(f2(a5),f3(a6,a1)))),
% 59.41/59.52 inference(scs_inference,[],[17,1003,1336,1206,1467,401,1146,982,28,7,5,6,4,26,22,20,2,23,24])).
% 59.41/59.52 cnf(1470,plain,
% 59.41/59.52 (E(x14701,f3(f2(a5),x14701))),
% 59.41/59.52 inference(rename_variables,[],[1206])).
% 59.41/59.52 cnf(1472,plain,
% 59.41/59.52 (P1(f3(a5,f2(a6)))),
% 59.41/59.52 inference(scs_inference,[],[17,1003,1001,1336,1206,1467,401,1146,982,154,28,7,5,6,4,26,22,20,2,23,24,27])).
% 59.41/59.52 cnf(1480,plain,
% 59.41/59.52 (P2(f2(f2(a5)),f4(a6))),
% 59.41/59.52 inference(scs_inference,[],[17,1003,957,924,948,1001,941,1336,1357,1412,1206,1467,1470,401,1146,982,61,810,1205,154,28,7,5,6,4,26,22,20,2,23,24,27,8,10,3,9,21])).
% 59.41/59.52 cnf(1495,plain,
% 59.41/59.52 (~E(f3(f4(a6),a7),a1)),
% 59.41/59.52 inference(scs_inference,[],[1005,1220,1472,1218,403,1027,732,28,7,5,6,4,26,22,20,2])).
% 59.41/59.52 cnf(1496,plain,
% 59.41/59.52 (~E(f3(a5,a7),f3(f2(a6),f3(a5,a1)))),
% 59.41/59.52 inference(scs_inference,[],[17,1005,1220,1472,1218,403,1027,732,28,7,5,6,4,26,22,20,2,23])).
% 59.41/59.52 cnf(1497,plain,
% 59.41/59.52 (E(x14971,f3(f2(a6),x14971))),
% 59.41/59.52 inference(rename_variables,[],[1218])).
% 59.41/59.52 cnf(1499,plain,
% 59.41/59.52 (~E(f3(a6,a7),f3(f2(a6),f3(a6,a1)))),
% 59.41/59.52 inference(scs_inference,[],[17,1005,1220,1472,1218,1497,403,1027,732,28,7,5,6,4,26,22,20,2,23,24])).
% 59.41/59.52 cnf(1514,plain,
% 59.41/59.52 (E(f3(x15141,x15142),f3(f3(f2(a5),x15141),x15142))),
% 59.41/59.52 inference(scs_inference,[],[1212,1206,1217,28,7,5])).
% 59.41/59.52 cnf(1516,plain,
% 59.41/59.52 (E(f3(x15161,x15162),f3(x15161,f3(f2(a5),x15162)))),
% 59.41/59.52 inference(scs_inference,[],[1212,1206,1217,28,7,5,4,6])).
% 59.41/59.52 cnf(1527,plain,
% 59.41/59.52 (~E(f3(a6,a1),f3(f2(a5),f3(a6,a7)))),
% 59.41/59.52 inference(scs_inference,[],[17,1465,1228,1212,405,900,1206,1217,721,80,28,7,5,4,6,26,22,20,2,23,24])).
% 59.41/59.52 cnf(1530,plain,
% 59.41/59.52 (P1(f3(a6,f4(a6)))),
% 59.41/59.52 inference(scs_inference,[],[17,1465,1121,1228,1212,405,900,1206,1217,721,572,80,28,7,5,4,6,26,22,20,2,23,24,27])).
% 59.41/59.52 cnf(1534,plain,
% 59.41/59.52 (~P2(f3(f4(a1),a1),f3(f2(a6),a7))),
% 59.41/59.52 inference(scs_inference,[],[17,1465,939,1121,262,1228,1212,933,405,900,1206,1217,721,572,80,28,7,5,4,6,26,22,20,2,23,24,27,21,10])).
% 59.41/59.52 cnf(1542,plain,
% 59.41/59.52 (E(f3(x15421,x15422),f3(f3(f2(a6),x15421),x15422))),
% 59.41/59.52 inference(scs_inference,[],[1530,1218,1205,28,7,5])).
% 59.41/59.52 cnf(1551,plain,
% 59.41/59.52 (E(f3(x15511,x15512),f3(f3(f2(a5),x15511),x15512))),
% 59.41/59.52 inference(rename_variables,[],[1514])).
% 59.41/59.52 cnf(1554,plain,
% 59.41/59.52 (E(f3(x15541,x15542),f3(f3(f2(a5),x15541),x15542))),
% 59.41/59.52 inference(rename_variables,[],[1514])).
% 59.41/59.52 cnf(1563,plain,
% 59.41/59.52 (P2(f4(f4(a5)),f2(f4(a5)))),
% 59.41/59.52 inference(scs_inference,[],[17,906,1530,1349,907,1496,1495,407,1534,944,1514,1551,1554,638,645,142,1218,1205,28,7,5,6,4,26,20,2,24,23,27,21,10,3,9])).
% 59.41/59.52 cnf(1574,plain,
% 59.41/59.52 (E(f3(x15741,f3(f2(a5),x15742)),f3(x15741,x15742))),
% 59.41/59.52 inference(scs_inference,[],[1207,926,1205,702,28,7,5,4,26,6])).
% 59.41/59.52 cnf(1577,plain,
% 59.41/59.52 (~E(f3(f2(a5),f3(a6,a1)),f3(a6,a7))),
% 59.41/59.53 inference(scs_inference,[],[1469,1207,1373,926,1205,702,28,7,5,4,26,6,20,2])).
% 59.41/59.53 cnf(1579,plain,
% 59.41/59.53 (E(f3(x15791,x15792),f3(x15791,f3(f2(a5),x15792)))),
% 59.41/59.53 inference(rename_variables,[],[1516])).
% 59.41/59.53 cnf(1588,plain,
% 59.41/59.53 (~P2(f3(a1,f2(a1)),f3(f2(a5),a7))),
% 59.41/59.53 inference(scs_inference,[],[17,1155,821,1469,1207,1340,1373,1456,926,1516,1579,933,1205,570,702,28,7,5,4,26,6,20,2,23,24,27,21,10])).
% 59.41/59.53 cnf(1600,plain,
% 59.41/59.53 (E(f3(x16001,f3(f2(a6),x16002)),f3(x16001,x16002))),
% 59.41/59.53 inference(scs_inference,[],[1219,1137,1217,12,28,7,26,5,6])).
% 59.41/59.53 cnf(1609,plain,
% 59.41/59.53 (E(f3(x16091,x16092),f3(f3(f2(a6),x16091),x16092))),
% 59.41/59.53 inference(rename_variables,[],[1542])).
% 59.41/59.53 cnf(1618,plain,
% 59.41/59.53 (P2(f4(f3(a5,a6)),f4(a6))),
% 59.41/59.53 inference(scs_inference,[],[17,764,1577,1480,1433,1466,1219,777,1211,1588,1372,1137,1574,1542,1609,474,134,1217,12,28,7,26,5,6,4,20,2,24,23,27,21,10,3,9])).
% 59.41/59.53 cnf(1630,plain,
% 59.41/59.53 (~E(f3(f2(a6),f3(a6,a1)),f3(a6,a7))),
% 59.41/59.53 inference(scs_inference,[],[1618,1499,542,1350,546,13,28,7,26,6,4,5,20,2])).
% 59.41/59.53 cnf(1658,plain,
% 59.41/59.53 ($false),
% 59.41/59.53 inference(scs_inference,[],[1630,1527,554,1563,955,1600,91,586,702,701,80,28,7,26,6,4,5,20,2,23]),
% 59.41/59.53 ['proof']).
% 59.41/59.53 % SZS output end Proof
% 59.41/59.53 % Total time :58.740000s
%------------------------------------------------------------------------------