%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT001-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n015.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:06 EDT 2024
% Result : Unsatisfiable 59.51s 59.58s
% Output : CNFRefutation 59.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CAT001-1 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n015.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Tue Jun 18 12:42:39 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.52/0.56 start to proof:theBenchmark
% 59.51/59.57 %-------------------------------------------
% 59.51/59.57 % File :CSE---1.7
% 59.51/59.57 % Problem :theBenchmark
% 59.51/59.57 % Transform :cnf
% 59.51/59.57 % Format :tptp:raw
% 59.51/59.57 % Command :java -jar mcs_scs.jar %d %s
% 59.51/59.58
% 59.51/59.58 % Result :Theorem 58.960000s
% 59.51/59.58 % Output :CNFRefutation 58.960000s
% 59.51/59.58 %-------------------------------------------
% 59.51/59.58 %--------------------------------------------------------------------------
% 59.51/59.58 % File : CAT001-1 : TPTP v8.2.0. Released v1.0.0.
% 59.51/59.58 % Domain : Category Theory
% 59.51/59.58 % Problem : XY monomorphism => Y monomorphism
% 59.51/59.58 % Version : [Mit67] axioms.
% 59.51/59.58 % English : If xy is a monomorphism, then y is a monomorphism.
% 59.51/59.58
% 59.51/59.58 % Refs : [Mit67] Mitchell (1967), Theory of Categories
% 59.51/59.58 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 59.51/59.58 % Source : [ANL]
% 59.51/59.58 % Names : C1 [MOW76]
% 59.51/59.58 % : p1.ver1.in [ANL]
% 59.51/59.58
% 59.51/59.58 % Status : Unsatisfiable
% 59.51/59.58 % Rating : 0.06 v8.2.0, 0.08 v8.1.0, 0.11 v7.5.0, 0.10 v7.4.0, 0.11 v7.3.0, 0.00 v6.0.0, 0.33 v5.5.0, 0.31 v5.4.0, 0.27 v5.3.0, 0.33 v5.2.0, 0.38 v5.1.0, 0.43 v5.0.0, 0.29 v4.1.0, 0.11 v4.0.1, 0.17 v4.0.0, 0.33 v3.7.0, 0.17 v3.5.0, 0.00 v3.1.0, 0.22 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.17 v2.3.0, 0.00 v2.2.1, 0.44 v2.2.0, 0.43 v2.1.0, 0.60 v2.0.0
% 59.51/59.58 % Syntax : Number of clauses : 23 ( 10 unt; 0 nHn; 17 RR)
% 59.51/59.58 % Number of literals : 52 ( 3 equ; 30 neg)
% 59.51/59.58 % Maximal clause size : 4 ( 2 avg)
% 59.51/59.58 % Maximal term depth : 2 ( 1 avg)
% 59.51/59.58 % Number of predicates : 4 ( 3 usr; 0 prp; 1-3 aty)
% 59.51/59.58 % Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% 59.51/59.58 % Number of variables : 55 ( 5 sgn)
% 59.51/59.58 % SPC : CNF_UNS_RFO_SEQ_HRN
% 59.51/59.58
% 59.51/59.58 % Comments :
% 59.51/59.58 %--------------------------------------------------------------------------
% 59.51/59.58 %----Include Mitchell's axioms for category theory
% 59.51/59.58 include('Axioms/CAT001-0.ax').
% 59.51/59.58 %--------------------------------------------------------------------------
% 59.51/59.58 cnf(ab_equals_c,hypothesis,
% 59.51/59.58 product(a,b,c) ).
% 59.51/59.58
% 59.51/59.58 cnf(cancellation_for_product,hypothesis,
% 59.51/59.58 ( ~ product(c,X1,X2)
% 59.51/59.58 | ~ product(c,X3,X2)
% 59.51/59.58 | X1 = X3 ) ).
% 59.51/59.58
% 59.51/59.58 cnf(bh_equals_d,hypothesis,
% 59.51/59.58 product(b,h,d) ).
% 59.51/59.58
% 59.51/59.58 cnf(bg_equals_d,hypothesis,
% 59.51/59.58 product(b,g,d) ).
% 59.51/59.58
% 59.51/59.58 cnf(prove_h_equals_g,negated_conjecture,
% 59.51/59.58 h != g ).
% 59.51/59.58
% 59.51/59.58 %--------------------------------------------------------------------------
% 59.51/59.58 %-------------------------------------------
% 59.51/59.58 % Proof found
% 59.51/59.58 % SZS status Theorem for theBenchmark
% 59.51/59.58 % SZS output start Proof
% 59.51/59.59 %ClaNum:36(EqnAxiom:13)
% 59.51/59.59 %VarNum:114(SingletonVarNum:55)
% 59.51/59.59 %MaxLitNum:4
% 59.51/59.59 %MaxfuncDepth:1
% 59.51/59.59 %SharedTerms:10
% 59.51/59.59 %goalClause: 23
% 59.51/59.59 %singleGoalClaCount:1
% 59.51/59.59 [18]P3(a3,a4,a5)
% 59.51/59.59 [19]P3(a4,a8,a6)
% 59.51/59.59 [20]P3(a4,a9,a6)
% 59.51/59.59 [23]~E(a9,a8)
% 59.51/59.59 [14]P1(f1(x141))
% 59.51/59.59 [15]P1(f2(x151))
% 59.51/59.59 [16]P2(x161,f1(x161))
% 59.51/59.59 [17]P2(f2(x171),x171)
% 59.51/59.59 [21]P3(x211,f1(x211),x211)
% 59.51/59.59 [22]P3(f2(x221),x221,x221)
% 59.51/59.59 [28]~P2(x281,x282)+P3(x281,x282,f7(x281,x282))
% 59.51/59.59 [27]P2(x271,x272)+~P3(x271,x272,x273)
% 59.51/59.59 [25]~P1(x251)+~P2(x251,x252)+P3(x251,x252,x252)
% 59.51/59.59 [26]~P1(x262)+~P2(x261,x262)+P3(x261,x262,x261)
% 59.51/59.59 [31]E(x311,x312)+~P3(a5,x311,x313)+~P3(a5,x312,x313)
% 59.51/59.59 [29]P2(x291,x292)+~P3(x292,x294,x293)+~P2(x291,x293)
% 59.51/59.59 [30]P2(x301,x302)+~P3(x304,x301,x303)+~P2(x303,x302)
% 59.51/59.59 [32]~P3(x323,x324,x321)+E(x321,x322)+~P3(x323,x324,x322)
% 59.51/59.59 [24]~P2(x243,x242)+~P2(x241,x243)+P2(x241,x242)+~P1(x243)
% 59.51/59.59 [33]~P3(x335,x332,x334)+P2(x331,x332)+~P3(x333,x335,x331)+~P2(x333,x334)
% 59.51/59.59 [34]~P3(x341,x345,x343)+P2(x341,x342)+~P3(x345,x344,x342)+~P2(x343,x344)
% 59.51/59.59 [35]~P3(x356,x352,x355)+P3(x351,x352,x353)+~P3(x354,x355,x353)+~P3(x354,x356,x351)
% 59.51/59.59 [36]~P3(x361,x366,x364)+P3(x361,x362,x363)+~P3(x364,x365,x363)+~P3(x366,x365,x362)
% 59.51/59.59 %EqnAxiom
% 59.51/59.59 [1]E(x11,x11)
% 59.51/59.59 [2]E(x22,x21)+~E(x21,x22)
% 59.51/59.59 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.51/59.59 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 59.51/59.59 [5]~E(x51,x52)+E(f2(x51),f2(x52))
% 59.51/59.59 [6]~E(x61,x62)+E(f7(x61,x63),f7(x62,x63))
% 59.51/59.59 [7]~E(x71,x72)+E(f7(x73,x71),f7(x73,x72))
% 59.51/59.59 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 59.51/59.59 [9]P3(x92,x93,x94)+~E(x91,x92)+~P3(x91,x93,x94)
% 59.51/59.59 [10]P3(x103,x102,x104)+~E(x101,x102)+~P3(x103,x101,x104)
% 59.51/59.59 [11]P3(x113,x114,x112)+~E(x111,x112)+~P3(x113,x114,x111)
% 59.51/59.59 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123)
% 59.51/59.59 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131)
% 59.51/59.59
% 59.51/59.59 %-------------------------------------------
% 59.51/59.60 cnf(37,plain,
% 59.51/59.60 (P2(f1(x371),f1(x371))),
% 59.51/59.60 inference(scs_inference,[],[21,16,30])).
% 59.51/59.60 cnf(40,plain,
% 59.51/59.60 (P3(a5,f1(a4),a5)),
% 59.51/59.60 inference(scs_inference,[],[21,16,18,30,35])).
% 59.51/59.60 cnf(43,plain,
% 59.51/59.60 (P3(f2(a3),a5,a5)),
% 59.51/59.60 inference(scs_inference,[],[21,22,16,18,30,35,36])).
% 59.51/59.60 cnf(55,plain,
% 59.51/59.60 (P3(f2(x551),x551,x551)),
% 59.51/59.60 inference(rename_variables,[],[22])).
% 59.51/59.60 cnf(57,plain,
% 59.51/59.60 (P2(f1(a4),f1(a5))),
% 59.51/59.60 inference(scs_inference,[],[37,40,22,16,29,30])).
% 59.51/59.60 cnf(60,plain,
% 59.51/59.60 (P2(a5,f1(a4))),
% 59.51/59.60 inference(scs_inference,[],[17,37,40,22,55,16,29,30,33])).
% 59.51/59.60 cnf(62,plain,
% 59.51/59.60 (P3(f2(x621),x621,x621)),
% 59.51/59.60 inference(rename_variables,[],[22])).
% 59.51/59.60 cnf(64,plain,
% 59.51/59.60 (P3(f2(f2(a3)),a5,a5)),
% 59.51/59.60 inference(scs_inference,[],[17,37,40,43,22,55,62,16,29,30,33,36])).
% 59.51/59.60 cnf(67,plain,
% 59.51/59.60 (P3(a5,f1(f1(a4)),a5)),
% 59.51/59.60 inference(scs_inference,[],[17,37,40,43,22,55,62,16,21,29,30,33,36,35])).
% 59.51/59.60 cnf(80,plain,
% 59.51/59.60 (P2(f2(f2(a3)),a5)),
% 59.51/59.60 inference(scs_inference,[],[17,60,64,40,29,34])).
% 59.51/59.60 cnf(82,plain,
% 59.51/59.60 (P3(f2(a4),a6,a6)),
% 59.51/59.60 inference(scs_inference,[],[17,60,64,19,22,40,29,34,36])).
% 59.51/59.60 cnf(85,plain,
% 59.51/59.60 (P3(a6,f1(a8),a6)),
% 59.51/59.60 inference(scs_inference,[],[17,60,64,19,22,21,40,29,34,36,35])).
% 59.51/59.60 cnf(104,plain,
% 59.51/59.60 (P3(f2(x1041),x1041,x1041)),
% 59.51/59.60 inference(rename_variables,[],[22])).
% 59.51/59.60 cnf(106,plain,
% 59.51/59.60 (P2(a5,f1(f1(a4)))),
% 59.51/59.60 inference(scs_inference,[],[17,57,60,67,22,104,30,29,33])).
% 59.51/59.60 cnf(108,plain,
% 59.51/59.60 (P3(f2(x1081),x1081,x1081)),
% 59.51/59.60 inference(rename_variables,[],[22])).
% 59.51/59.60 cnf(110,plain,
% 59.51/59.60 (P3(f2(f2(a4)),a6,a6)),
% 59.51/59.60 inference(scs_inference,[],[17,57,60,67,82,22,104,108,30,29,33,36])).
% 59.51/59.60 cnf(113,plain,
% 59.51/59.60 (P3(a6,f1(f1(a8)),a6)),
% 59.51/59.60 inference(scs_inference,[],[17,57,60,67,82,85,22,104,108,21,30,29,33,36,35])).
% 59.51/59.60 cnf(132,plain,
% 59.51/59.60 (P2(f2(a3),a5)),
% 59.51/59.60 inference(scs_inference,[],[17,80,110,43,22,29,33])).
% 59.51/59.60 cnf(135,plain,
% 59.51/59.60 (P2(f2(f2(a4)),a6)),
% 59.51/59.60 inference(scs_inference,[],[17,16,80,110,43,22,21,29,33,34])).
% 59.51/59.60 cnf(154,plain,
% 59.51/59.60 (P3(f2(x1541),x1541,x1541)),
% 59.51/59.60 inference(rename_variables,[],[22])).
% 59.51/59.60 cnf(156,plain,
% 59.51/59.60 (P2(a6,f1(f1(a8)))),
% 59.51/59.60 inference(scs_inference,[],[17,113,60,16,22,154,30,29,33])).
% 59.51/59.60 cnf(176,plain,
% 59.51/59.60 (P2(f2(a3),f2(a3))),
% 59.51/59.60 inference(scs_inference,[],[43,132,29])).
% 59.51/59.60 cnf(184,plain,
% 59.51/59.60 (P2(f2(a6),f2(a4))),
% 59.51/59.60 inference(scs_inference,[],[17,82,29])).
% 59.51/59.60 cnf(187,plain,
% 59.51/59.60 (P2(f2(a4),a6)),
% 59.51/59.60 inference(scs_inference,[],[17,82,16,21,29,34])).
% 59.51/59.60 cnf(204,plain,
% 59.51/59.60 (P2(f1(a8),f1(a6))),
% 59.51/59.60 inference(scs_inference,[],[85,16,30])).
% 59.51/59.60 cnf(205,plain,
% 59.51/59.60 (P2(x2051,f1(x2051))),
% 59.51/59.60 inference(rename_variables,[],[16])).
% 59.51/59.60 cnf(207,plain,
% 59.51/59.60 (P2(x2071,f2(f1(x2071)))),
% 59.51/59.60 inference(scs_inference,[],[85,16,205,22,30,29])).
% 59.51/59.60 cnf(208,plain,
% 59.51/59.60 (P3(f2(x2081),x2081,x2081)),
% 59.51/59.60 inference(rename_variables,[],[22])).
% 59.51/59.60 cnf(210,plain,
% 59.51/59.60 (P2(a6,f1(a8))),
% 59.51/59.60 inference(scs_inference,[],[85,17,16,205,22,208,30,29,33])).
% 59.51/59.60 cnf(226,plain,
% 59.51/59.60 (P2(f2(a5),f2(a3))),
% 59.51/59.60 inference(scs_inference,[],[43,17,29])).
% 59.51/59.60 cnf(234,plain,
% 59.51/59.60 (P3(a3,a6,x2341)+~P3(a5,a9,x2341)),
% 59.51/59.60 inference(scs_inference,[],[43,106,18,132,17,20,29,13,11,9,12,10,36])).
% 59.51/59.60 cnf(241,plain,
% 59.51/59.60 (P2(f2(a4),f2(a4))),
% 59.51/59.60 inference(scs_inference,[],[82,187,29])).
% 59.51/59.60 cnf(316,plain,
% 59.51/59.60 (P2(f1(f2(x3161)),x3161)),
% 59.51/59.60 inference(scs_inference,[],[17,21,30])).
% 59.51/59.60 cnf(333,plain,
% 59.51/59.60 (~P3(f2(a9),a9,a8)),
% 59.51/59.60 inference(scs_inference,[],[23,22,2,32])).
% 59.51/59.60 cnf(334,plain,
% 59.51/59.60 (~P3(f2(a8),a8,a9)),
% 59.51/59.60 inference(scs_inference,[],[23,22,32])).
% 59.51/59.60 cnf(350,plain,
% 59.51/59.60 (P3(x3501,f1(x3501),x3501)),
% 59.51/59.60 inference(rename_variables,[],[21])).
% 59.51/59.60 cnf(353,plain,
% 59.51/59.60 (P3(x3531,f1(x3531),x3531)),
% 59.51/59.60 inference(rename_variables,[],[21])).
% 59.51/59.60 cnf(358,plain,
% 59.51/59.60 (~E(a8,a9)),
% 59.51/59.60 inference(scs_inference,[],[23,82,37,21,350,353,316,32,30,29,11])).
% 59.51/59.60 cnf(392,plain,
% 59.51/59.60 (P2(x3921,x3922)+~E(f1(x3921),x3922)),
% 59.51/59.60 inference(scs_inference,[],[16,13])).
% 59.51/59.60 cnf(412,plain,
% 59.51/59.60 (~P3(f2(x4121),x4121,x4122)+P2(f2(f2(x4121)),x4122)),
% 59.51/59.60 inference(scs_inference,[],[20,17,37,22,184,13,12,10,34])).
% 59.51/59.60 cnf(445,plain,
% 59.51/59.60 (P3(a5,a8,x4451)+~P3(a3,a6,x4451)),
% 59.51/59.60 inference(scs_inference,[],[18,210,19,110,22,176,241,13,12,10,33,35])).
% 59.51/59.60 cnf(952,plain,
% 59.51/59.60 (P2(a3,a4)),
% 59.51/59.60 inference(scs_inference,[],[18,60,16,80,21,30,29,34])).
% 59.51/59.60 cnf(957,plain,
% 59.51/59.60 (~P3(f2(f2(a3)),a3,x9571)+P2(x9571,a4)),
% 59.51/59.60 inference(scs_inference,[],[18,60,16,80,21,30,29,34,13,12,33])).
% 59.51/59.60 cnf(964,plain,
% 59.51/59.60 (P2(f2(a5),a3)),
% 59.51/59.60 inference(scs_inference,[],[18,17,106,30,29])).
% 59.51/59.60 cnf(993,plain,
% 59.51/59.60 (P2(a3,f2(a4))),
% 59.51/59.60 inference(scs_inference,[],[22,952,29])).
% 59.51/59.60 cnf(1333,plain,
% 59.51/59.60 (P2(a8,f1(a6))),
% 59.51/59.60 inference(scs_inference,[],[19,16,30])).
% 59.51/59.60 cnf(1338,plain,
% 59.51/59.60 (P2(a4,a8)),
% 59.51/59.60 inference(scs_inference,[],[19,210,16,135,21,30,29,34])).
% 59.51/59.60 cnf(1350,plain,
% 59.51/59.60 (P2(f2(a6),a4)),
% 59.51/59.60 inference(scs_inference,[],[19,17,156,30,29])).
% 59.51/59.60 cnf(1406,plain,
% 59.51/59.60 (P2(f1(a4),a8)),
% 59.51/59.60 inference(scs_inference,[],[21,1338,30])).
% 59.51/59.60 cnf(1420,plain,
% 59.51/59.60 (P2(f1(a4),f2(a8))),
% 59.51/59.60 inference(scs_inference,[],[22,1406,29])).
% 59.51/59.60 cnf(1913,plain,
% 59.51/59.60 (P2(a9,f1(a8))),
% 59.51/59.60 inference(scs_inference,[],[20,210,30])).
% 59.51/59.60 cnf(1916,plain,
% 59.51/59.60 (P3(f2(x19161),x19161,x19161)),
% 59.51/59.60 inference(rename_variables,[],[22])).
% 59.51/59.60 cnf(1918,plain,
% 59.51/59.60 (P2(a4,a9)),
% 59.51/59.60 inference(scs_inference,[],[20,187,210,22,1916,30,29,33])).
% 59.51/59.60 cnf(1930,plain,
% 59.51/59.60 (P2(a9,f1(a6))),
% 59.51/59.60 inference(scs_inference,[],[20,16,30])).
% 59.51/59.60 cnf(1933,plain,
% 59.51/59.60 (P2(a6,f1(a9))),
% 59.51/59.60 inference(scs_inference,[],[20,16,21,1918,30,33])).
% 59.51/59.60 cnf(1967,plain,
% 59.51/59.60 (~P3(f2(a8),a8,x19671)+~P3(f2(f2(a8)),x19671,a9)),
% 59.51/59.60 inference(scs_inference,[],[20,334,22,207,1933,30,12,13,35])).
% 59.51/59.60 cnf(1980,plain,
% 59.51/59.60 (P2(f1(a9),f1(a8))),
% 59.51/59.60 inference(scs_inference,[],[21,22,1913,1967,30])).
% 59.51/59.60 cnf(1992,plain,
% 59.51/59.60 (P2(f1(a4),a9)),
% 59.51/59.60 inference(scs_inference,[],[21,1918,30])).
% 59.51/59.60 cnf(2054,plain,
% 59.51/59.60 (P2(f1(a9),f1(a6))),
% 59.51/59.60 inference(scs_inference,[],[21,1930,30])).
% 59.51/59.60 cnf(2362,plain,
% 59.51/59.60 (P2(f1(a5),f1(a4))),
% 59.51/59.60 inference(scs_inference,[],[21,60,30])).
% 59.51/59.60 cnf(2376,plain,
% 59.51/59.60 (P2(f1(a6),f1(a8))),
% 59.51/59.60 inference(scs_inference,[],[21,210,30])).
% 59.51/59.60 cnf(2377,plain,
% 59.51/59.60 (P3(x23771,f1(x23771),x23771)),
% 59.51/59.60 inference(rename_variables,[],[21])).
% 59.51/59.60 cnf(2381,plain,
% 59.51/59.60 (~P3(f1(a6),f1(a8),x23811)+P2(a6,x23811)),
% 59.51/59.60 inference(scs_inference,[],[21,2377,210,30,12,13,34])).
% 59.51/59.60 cnf(2446,plain,
% 59.51/59.60 (P2(f1(a6),f1(a9))),
% 59.51/59.60 inference(scs_inference,[],[21,1933,30])).
% 59.51/59.60 cnf(2844,plain,
% 59.51/59.60 (P2(f2(a4),f2(a6))),
% 59.51/59.60 inference(scs_inference,[],[22,187,29])).
% 59.51/59.60 cnf(2845,plain,
% 59.51/59.60 (P3(f2(x28451),x28451,x28451)),
% 59.51/59.60 inference(rename_variables,[],[22])).
% 59.51/59.60 cnf(2847,plain,
% 59.51/59.60 (~P3(a9,f1(a9),a8)),
% 59.51/59.60 inference(scs_inference,[],[22,2845,333,187,21,29,36])).
% 59.51/59.60 cnf(2862,plain,
% 59.51/59.60 (P2(f2(a3),f2(a5))),
% 59.51/59.60 inference(scs_inference,[],[22,132,29])).
% 59.51/59.60 cnf(2876,plain,
% 59.51/59.60 (P2(f2(x28761),f2(x28761))),
% 59.51/59.60 inference(scs_inference,[],[22,17,29])).
% 59.51/59.60 cnf(3557,plain,
% 59.51/59.60 (P3(x35571,a4,f7(x35571,a4))+~P3(f2(f2(a3)),a3,x35571)),
% 59.51/59.60 inference(scs_inference,[],[957,28])).
% 59.51/59.60 cnf(4039,plain,
% 59.51/59.60 (P2(a6,f7(f1(a6),f1(a8)))),
% 59.51/59.60 inference(scs_inference,[],[2376,2381,28])).
% 59.51/59.60 cnf(4727,plain,
% 59.51/59.60 (P2(a8,f1(a9))),
% 59.51/59.60 inference(scs_inference,[],[19,1933,30])).
% 59.51/59.60 cnf(4872,plain,
% 59.51/59.60 (P3(f2(f2(x48721)),x48721,x48721)),
% 59.51/59.60 inference(scs_inference,[],[22,15,412,25])).
% 59.51/59.60 cnf(4873,plain,
% 59.51/59.60 (P3(a3,a4,f7(a3,a4))),
% 59.51/59.60 inference(scs_inference,[],[4872,3557])).
% 59.51/59.60 cnf(4878,plain,
% 59.51/59.60 (P3(f2(a3),f7(a3,a4),f7(a3,a4))),
% 59.51/59.60 inference(scs_inference,[],[20,22,4039,4872,3557,30,36])).
% 59.51/59.60 cnf(4973,plain,
% 59.51/59.60 (P3(f2(a3),f7(a3,a4),a5)),
% 59.51/59.60 inference(scs_inference,[],[18,22,4873,10,36])).
% 59.51/59.60 cnf(4976,plain,
% 59.51/59.60 (P3(a5,f1(f7(a3,a4)),a5)),
% 59.51/59.60 inference(scs_inference,[],[18,22,21,4873,10,36,35])).
% 59.51/59.60 cnf(4992,plain,
% 59.51/59.60 (E(f1(a4),f1(f7(a3,a4)))),
% 59.51/59.60 inference(scs_inference,[],[40,4976,11,31])).
% 59.51/59.60 cnf(4999,plain,
% 59.51/59.60 (E(f1(f7(a3,a4)),f1(a4))),
% 59.51/59.60 inference(scs_inference,[],[4992,2])).
% 59.51/59.60 cnf(5017,plain,
% 59.51/59.60 (P2(f7(a3,a4),f1(a4))),
% 59.51/59.60 inference(scs_inference,[],[4999,392])).
% 59.51/59.60 cnf(5371,plain,
% 59.51/59.60 (P2(f2(a3),f7(a3,a4))),
% 59.51/59.60 inference(scs_inference,[],[4973,27])).
% 59.51/59.60 cnf(5373,plain,
% 59.51/59.60 (P3(a4,a9,f7(a4,a9))),
% 59.51/59.60 inference(scs_inference,[],[4973,1918,27,28])).
% 59.51/59.60 cnf(5375,plain,
% 59.51/59.60 (P3(a8,f1(a9),a8)),
% 59.51/59.60 inference(scs_inference,[],[14,4973,4727,1918,27,28,26])).
% 59.51/59.60 cnf(5376,plain,
% 59.51/59.60 (P1(f1(x53761))),
% 59.51/59.60 inference(rename_variables,[],[14])).
% 59.51/59.60 cnf(5378,plain,
% 59.51/59.60 (P3(f1(a6),f1(a9),f1(a9))),
% 59.51/59.60 inference(scs_inference,[],[14,5376,4973,4727,2446,1918,27,28,26,25])).
% 59.51/59.60 cnf(5383,plain,
% 59.51/59.60 (P2(f7(a4,a9),f1(a9))),
% 59.51/59.61 inference(scs_inference,[],[14,5376,358,4973,4727,2446,1918,21,27,28,26,25,32,33])).
% 59.51/59.61 cnf(5396,plain,
% 59.51/59.61 (P3(a4,a8,f7(a4,a8))),
% 59.51/59.61 inference(scs_inference,[],[1338,28])).
% 59.51/59.61 cnf(5398,plain,
% 59.51/59.61 (P3(f2(a4),f2(a6),f2(a4))),
% 59.51/59.61 inference(scs_inference,[],[2844,15,1338,28,26])).
% 59.51/59.61 cnf(5399,plain,
% 59.51/59.61 (P1(f2(x53991))),
% 59.51/59.61 inference(rename_variables,[],[15])).
% 59.51/59.61 cnf(5401,plain,
% 59.51/59.61 (P3(f2(a4),f2(a6),f2(a6))),
% 59.51/59.61 inference(scs_inference,[],[2844,15,5399,1338,28,26,25])).
% 59.51/59.61 cnf(5404,plain,
% 59.51/59.61 (P2(f7(a3,a4),f1(a5))),
% 59.51/59.61 inference(scs_inference,[],[4973,2844,15,5399,1338,16,28,26,25,30])).
% 59.51/59.61 cnf(5407,plain,
% 59.51/59.61 (P2(f7(a4,a9),f1(a6))),
% 59.51/59.61 inference(scs_inference,[],[14,5383,4973,2844,15,5399,1338,2054,16,28,26,25,30,24])).
% 59.51/59.61 cnf(5422,plain,
% 59.51/59.61 (~P3(a8,f1(a6),a9)),
% 59.51/59.61 inference(scs_inference,[],[14,5407,5375,5378,2847,26,35])).
% 59.51/59.61 cnf(5426,plain,
% 59.51/59.61 (P2(f7(a4,a8),f1(a9))),
% 59.51/59.61 inference(scs_inference,[],[14,5407,5398,5396,5375,5378,2847,1338,26,35,36,33])).
% 59.51/59.61 cnf(5431,plain,
% 59.51/59.61 (P3(f7(a3,a4),f1(a5),f7(a3,a4))),
% 59.51/59.61 inference(scs_inference,[],[14,5404,26])).
% 59.51/59.61 cnf(5434,plain,
% 59.51/59.61 (P3(f7(a4,a8),f1(a9),f7(a4,a8))),
% 59.51/59.61 inference(scs_inference,[],[14,5404,5396,5375,26,35])).
% 59.51/59.61 cnf(5436,plain,
% 59.51/59.61 (P2(f7(a4,a8),f1(a6))),
% 59.51/59.61 inference(scs_inference,[],[14,5404,5426,5396,5375,5378,26,35,29])).
% 59.51/59.61 cnf(5451,plain,
% 59.51/59.61 (P3(a8,f1(a6),a8)),
% 59.51/59.61 inference(scs_inference,[],[14,1333,26])).
% 59.51/59.61 cnf(5452,plain,
% 59.51/59.61 (P1(f1(x54521))),
% 59.51/59.61 inference(rename_variables,[],[14])).
% 59.51/59.61 cnf(5457,plain,
% 59.51/59.61 (P2(f7(a4,a9),f1(a8))),
% 59.51/59.61 inference(scs_inference,[],[14,5452,5383,1333,2876,15,1980,26,25,24])).
% 59.51/59.61 cnf(5474,plain,
% 59.51/59.61 (P2(f2(a5),f7(a3,a4))),
% 59.51/59.61 inference(scs_inference,[],[14,5457,5371,15,226,26,24])).
% 59.51/59.61 cnf(5483,plain,
% 59.51/59.61 (P3(f2(a3),f2(a5),f2(a3))),
% 59.51/59.61 inference(scs_inference,[],[2862,15,26])).
% 59.51/59.61 cnf(5484,plain,
% 59.51/59.61 (P1(f2(x54841))),
% 59.51/59.61 inference(rename_variables,[],[15])).
% 59.51/59.61 cnf(5486,plain,
% 59.51/59.61 (P3(f2(a5),f7(a3,a4),f7(a3,a4))),
% 59.51/59.61 inference(scs_inference,[],[5474,2862,15,5484,26,25])).
% 59.51/59.61 cnf(5489,plain,
% 59.51/59.61 (P2(f7(a3,a4),f2(a8))),
% 59.51/59.61 inference(scs_inference,[],[14,5474,2862,1420,15,5484,5017,26,25,24])).
% 59.51/59.61 cnf(5498,plain,
% 59.51/59.61 (P3(f7(a3,a4),f2(a8),f7(a3,a4))),
% 59.51/59.61 inference(scs_inference,[],[5489,15,26])).
% 59.51/59.61 cnf(5499,plain,
% 59.51/59.61 (P1(f2(x54991))),
% 59.51/59.61 inference(rename_variables,[],[15])).
% 59.51/59.61 cnf(5501,plain,
% 59.51/59.61 (P3(f2(a3),f2(a5),f2(a5))),
% 59.51/59.61 inference(scs_inference,[],[5489,2862,15,5499,26,25])).
% 59.51/59.61 cnf(5504,plain,
% 59.51/59.61 (P2(f1(a5),f2(a8))),
% 59.51/59.61 inference(scs_inference,[],[5489,5431,2862,15,5499,26,25,30])).
% 59.51/59.61 cnf(5519,plain,
% 59.51/59.61 (P2(a5,f2(a8))),
% 59.51/59.61 inference(scs_inference,[],[14,5498,5504,5434,5371,4973,15,26,25,36,33])).
% 59.51/59.61 cnf(5525,plain,
% 59.51/59.61 (P1(f2(x55251))),
% 59.51/59.61 inference(rename_variables,[],[15])).
% 59.51/59.61 cnf(5527,plain,
% 59.51/59.61 (P3(f2(a6),a4,a4)),
% 59.51/59.61 inference(scs_inference,[],[5519,1350,15,5525,26,25])).
% 59.51/59.61 cnf(5530,plain,
% 59.51/59.61 (P2(f7(a3,a4),a8)),
% 59.51/59.61 inference(scs_inference,[],[14,5519,1350,1406,15,5525,5017,26,25,24])).
% 59.51/59.61 cnf(5533,plain,
% 59.51/59.61 (P3(f2(a5),f7(a3,a4),a5)),
% 59.51/59.61 inference(scs_inference,[],[14,5519,5501,5486,4973,1350,1406,15,5525,5017,26,25,24,35])).
% 59.51/59.61 cnf(5537,plain,
% 59.51/59.61 (P2(f2(a6),f7(a4,a9))),
% 59.51/59.61 inference(scs_inference,[],[14,5519,5501,5486,5373,5451,2847,4973,1350,1406,1918,15,5525,5017,26,25,24,35,36,34])).
% 59.51/59.61 cnf(5547,plain,
% 59.51/59.61 (P3(a9,f1(a8),a9)),
% 59.51/59.61 inference(scs_inference,[],[1913,14,26])).
% 59.51/59.61 cnf(5550,plain,
% 59.51/59.61 (P3(f2(a6),f7(a4,a9),f7(a4,a9))),
% 59.51/59.61 inference(scs_inference,[],[15,5537,1913,14,26,25])).
% 59.51/59.61 cnf(5557,plain,
% 59.51/59.61 (~P3(a9,f1(a8),a8)),
% 59.51/59.61 inference(scs_inference,[],[15,5537,5527,5396,1913,1338,23,14,26,25,36,34,32])).
% 59.51/59.61 cnf(5569,plain,
% 59.51/59.61 (P2(f2(a4),f7(a4,a9))),
% 59.51/59.61 inference(scs_inference,[],[15,5550,5401,964,25,36,27])).
% 59.51/59.61 cnf(5576,plain,
% 59.51/59.61 (P2(f1(a5),a8)),
% 59.51/59.61 inference(scs_inference,[],[5530,5431,30])).
% 59.51/59.61 cnf(5587,plain,
% 59.51/59.61 (P3(f1(a5),a8,a8)),
% 59.51/59.61 inference(scs_inference,[],[5576,14,25])).
% 59.51/59.61 cnf(5605,plain,
% 59.51/59.61 (P2(f7(a4,a8),f1(a8))),
% 59.51/59.61 inference(scs_inference,[],[5587,5436,204,358,14,32,25,29])).
% 59.51/59.61 cnf(5621,plain,
% 59.51/59.61 (P1(f1(x56211))),
% 59.51/59.61 inference(rename_variables,[],[14])).
% 59.51/59.61 cnf(5628,plain,
% 59.51/59.61 (P2(a3,f7(a4,a9))),
% 59.51/59.61 inference(scs_inference,[],[15,5569,5605,5547,5422,993,1420,14,5621,26,25,36,24])).
% 59.51/59.61 cnf(5635,plain,
% 59.51/59.61 (P3(a9,f1(a6),a9)),
% 59.51/59.61 inference(scs_inference,[],[1930,14,26])).
% 59.51/59.61 cnf(5638,plain,
% 59.51/59.61 (P3(f2(a3),a5,f7(a3,a4))),
% 59.51/59.61 inference(scs_inference,[],[5533,5483,4878,1930,14,26,36])).
% 59.51/59.61 cnf(5640,plain,
% 59.51/59.61 (P2(f7(a3,a4),a9)),
% 59.51/59.61 inference(scs_inference,[],[5628,5533,5483,5373,4878,4873,1930,14,26,36,33])).
% 59.51/59.61 cnf(5649,plain,
% 59.51/59.61 (P2(f1(a5),a9)),
% 59.51/59.61 inference(scs_inference,[],[5635,5557,1992,14,2362,36,24])).
% 59.51/59.61 cnf(5695,plain,
% 59.51/59.61 (P3(a5,a9,f7(a5,a9))),
% 59.51/59.61 inference(scs_inference,[],[16,5649,14,24,28])).
% 59.51/59.61 cnf(5697,plain,
% 59.51/59.61 (~P3(a5,a8,f7(a5,a9))),
% 59.51/59.61 inference(scs_inference,[],[16,5649,23,14,24,28,31])).
% 59.51/59.61 cnf(5721,plain,
% 59.51/59.61 ($false),
% 59.51/59.61 inference(scs_inference,[],[16,5697,5695,5640,5576,5638,5547,14,445,34,24,35,234]),
% 59.51/59.61 ['proof']).
% 59.51/59.61 % SZS output end Proof
% 59.51/59.61 % Total time :58.960000s
%------------------------------------------------------------------------------