%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT003-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 : n024.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 58.62s 59.41s
% Output : CNFRefutation 58.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CAT003-1 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n024.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 : Tue Jun 18 12:21:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.19/0.57 start to proof:theBenchmark
% 58.54/59.40 %-------------------------------------------
% 58.54/59.40 % File :CSE---1.7
% 58.54/59.40 % Problem :theBenchmark
% 58.54/59.40 % Transform :cnf
% 58.54/59.40 % Format :tptp:raw
% 58.54/59.40 % Command :java -jar mcs_scs.jar %d %s
% 58.54/59.40
% 58.54/59.40 % Result :Theorem 58.070000s
% 58.54/59.40 % Output :CNFRefutation 58.070000s
% 58.54/59.40 %-------------------------------------------
% 58.62/59.41 %--------------------------------------------------------------------------
% 58.62/59.41 % File : CAT003-1 : TPTP v8.2.0. Released v1.0.0.
% 58.62/59.41 % Domain : Category Theory
% 58.62/59.41 % Problem : XY epimorphism => X epimorphism
% 58.62/59.41 % Version : [Mit67] axioms.
% 58.62/59.41 % English : If xy is an epimorphism, then x is an epimorphism.
% 58.62/59.41
% 58.62/59.41 % Refs : [Mit67] Mitchell (1967), Theory of Categories
% 58.62/59.41 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 58.62/59.41 % Source : [ANL]
% 58.62/59.41 % Names : C3 [MOW76]
% 58.62/59.41 % : p3.ver1.in [ANL]
% 58.62/59.41
% 58.62/59.41 % Status : Unsatisfiable
% 58.62/59.41 % 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
% 58.62/59.41 % Syntax : Number of clauses : 23 ( 10 unt; 0 nHn; 17 RR)
% 58.62/59.41 % Number of literals : 52 ( 3 equ; 30 neg)
% 58.62/59.41 % Maximal clause size : 4 ( 2 avg)
% 58.62/59.41 % Maximal term depth : 2 ( 1 avg)
% 58.62/59.41 % Number of predicates : 4 ( 3 usr; 0 prp; 1-3 aty)
% 58.62/59.41 % Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% 58.62/59.41 % Number of variables : 55 ( 5 sgn)
% 58.62/59.41 % SPC : CNF_UNS_RFO_SEQ_HRN
% 58.62/59.41
% 58.62/59.41 % Comments :
% 58.62/59.41 %--------------------------------------------------------------------------
% 58.62/59.41 %----Include Mitchell's axioms for category theory
% 58.62/59.41 include('Axioms/CAT001-0.ax').
% 58.62/59.41 %--------------------------------------------------------------------------
% 58.62/59.41 cnf(ab_equals_c,hypothesis,
% 58.62/59.41 product(a,b,c) ).
% 58.62/59.41
% 58.62/59.41 cnf(cancellation_for_product,hypothesis,
% 58.62/59.41 ( ~ product(X,c,W)
% 58.62/59.41 | ~ product(Y,c,W)
% 58.62/59.41 | X = Y ) ).
% 58.62/59.41
% 58.62/59.41 cnf(ha_equals_d,hypothesis,
% 58.62/59.41 product(h,a,d) ).
% 58.62/59.41
% 58.62/59.41 cnf(ga_equals_d,hypothesis,
% 58.62/59.41 product(g,a,d) ).
% 58.62/59.41
% 58.62/59.41 cnf(prove_h_equals_g,negated_conjecture,
% 58.62/59.41 h != g ).
% 58.62/59.41
% 58.62/59.41 %----The ANL group use these extra lemmas as demodulators -
% 58.62/59.41 %input_clause(name,hypothesis,
% 58.62/59.41 % [++equal(domain(domain(X)),domain(X))]).
% 58.62/59.41 %input_clause(name,hypothesis,
% 58.62/59.41 % [++equal(codomain(domain(X)),domain(X))]).
% 58.62/59.41 %input_clause(name,hypothesis,
% 58.62/59.41 % [++equal(domain(codomain(X)),codomain(X))]).
% 58.62/59.41 %input_clause(name,hypothesis,
% 58.62/59.41 % [++equal(codomain(codomain(X)),codomain(X))]).
% 58.62/59.41 %input_clause(name,hypothesis,
% 58.62/59.41 % [++equal(compose(codomain(X),X),X)]).
% 58.62/59.41 %input_clause(name,hypothesis,
% 58.62/59.41 % [++equal(compose(X,domain(X)),X)]).
% 58.62/59.41 %input_clause(name,hypothesis,
% 58.62/59.41 % [++equal(compose(codomain(X),codomain(X)),codomain(X))]).
% 58.62/59.41 %input_clause(name,hypothesis,
% 58.62/59.41 % [++equal(compose(domain(X),domain(X)),domain(X))]).
% 58.62/59.41 %input_clause(name,hypothesis,
% 58.62/59.41 % [++equal(domain(compose(X,Y)),domain(Y))]).
% 58.62/59.41 %input_clause(name,hypothesis,
% 58.62/59.41 % [++equal(codomain(compose(X,Y)),codomain(X))]).
% 58.62/59.41 %--------------------------------------------------------------------------
% 58.62/59.41 %-------------------------------------------
% 58.62/59.41 % Proof found
% 58.62/59.41 % SZS status Theorem for theBenchmark
% 58.62/59.41 % SZS output start Proof
% 58.62/59.42 %ClaNum:36(EqnAxiom:13)
% 58.62/59.42 %VarNum:114(SingletonVarNum:55)
% 58.62/59.42 %MaxLitNum:4
% 58.62/59.42 %MaxfuncDepth:1
% 58.62/59.42 %SharedTerms:10
% 58.62/59.42 %goalClause: 23
% 58.62/59.42 %singleGoalClaCount:1
% 58.62/59.42 [18]P3(a3,a4,a5)
% 58.62/59.42 [19]P3(a8,a3,a6)
% 58.62/59.42 [20]P3(a9,a3,a6)
% 58.62/59.42 [23]~E(a9,a8)
% 58.62/59.42 [14]P1(f1(x141))
% 58.62/59.42 [15]P1(f2(x151))
% 58.62/59.42 [16]P2(x161,f1(x161))
% 58.62/59.42 [17]P2(f2(x171),x171)
% 58.62/59.42 [21]P3(x211,f1(x211),x211)
% 58.62/59.42 [22]P3(f2(x221),x221,x221)
% 58.62/59.42 [28]~P2(x281,x282)+P3(x281,x282,f7(x281,x282))
% 58.62/59.42 [27]P2(x271,x272)+~P3(x271,x272,x273)
% 58.62/59.42 [25]~P1(x251)+~P2(x251,x252)+P3(x251,x252,x252)
% 58.62/59.42 [26]~P1(x262)+~P2(x261,x262)+P3(x261,x262,x261)
% 58.62/59.42 [31]E(x311,x312)+~P3(x311,a5,x313)+~P3(x312,a5,x313)
% 58.62/59.42 [29]P2(x291,x292)+~P3(x292,x294,x293)+~P2(x291,x293)
% 58.62/59.42 [30]P2(x301,x302)+~P3(x304,x301,x303)+~P2(x303,x302)
% 58.62/59.42 [32]~P3(x323,x324,x321)+E(x321,x322)+~P3(x323,x324,x322)
% 58.62/59.42 [24]~P2(x243,x242)+~P2(x241,x243)+P2(x241,x242)+~P1(x243)
% 58.62/59.42 [33]~P3(x335,x332,x334)+P2(x331,x332)+~P3(x333,x335,x331)+~P2(x333,x334)
% 58.62/59.42 [34]~P3(x341,x345,x343)+P2(x341,x342)+~P3(x345,x344,x342)+~P2(x343,x344)
% 58.62/59.42 [35]~P3(x356,x352,x355)+P3(x351,x352,x353)+~P3(x354,x355,x353)+~P3(x354,x356,x351)
% 58.62/59.42 [36]~P3(x361,x366,x364)+P3(x361,x362,x363)+~P3(x364,x365,x363)+~P3(x366,x365,x362)
% 58.62/59.42 %EqnAxiom
% 58.62/59.42 [1]E(x11,x11)
% 58.62/59.42 [2]E(x22,x21)+~E(x21,x22)
% 58.62/59.42 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.62/59.42 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 58.62/59.42 [5]~E(x51,x52)+E(f2(x51),f2(x52))
% 58.62/59.42 [6]~E(x61,x62)+E(f7(x61,x63),f7(x62,x63))
% 58.62/59.42 [7]~E(x71,x72)+E(f7(x73,x71),f7(x73,x72))
% 58.62/59.42 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 58.62/59.42 [9]P3(x92,x93,x94)+~E(x91,x92)+~P3(x91,x93,x94)
% 58.62/59.42 [10]P3(x103,x102,x104)+~E(x101,x102)+~P3(x103,x101,x104)
% 58.62/59.42 [11]P3(x113,x114,x112)+~E(x111,x112)+~P3(x113,x114,x111)
% 58.62/59.42 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123)
% 58.62/59.42 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131)
% 58.62/59.42
% 58.62/59.42 %-------------------------------------------
% 58.62/59.43 cnf(37,plain,
% 58.62/59.43 (P2(f1(x371),f1(x371))),
% 58.62/59.43 inference(scs_inference,[],[21,16,30])).
% 58.62/59.43 cnf(40,plain,
% 58.62/59.43 (P3(a5,f1(a4),a5)),
% 58.62/59.43 inference(scs_inference,[],[21,16,18,30,35])).
% 58.62/59.43 cnf(43,plain,
% 58.62/59.43 (P3(f2(a3),a5,a5)),
% 58.62/59.43 inference(scs_inference,[],[21,22,16,18,30,35,36])).
% 58.62/59.43 cnf(55,plain,
% 58.62/59.43 (P3(f2(x551),x551,x551)),
% 58.62/59.43 inference(rename_variables,[],[22])).
% 58.62/59.43 cnf(57,plain,
% 58.62/59.43 (P2(f1(a4),f1(a5))),
% 58.62/59.43 inference(scs_inference,[],[37,40,22,16,29,30])).
% 58.62/59.43 cnf(60,plain,
% 58.62/59.43 (P3(a5,f1(f1(a4)),a5)),
% 58.62/59.43 inference(scs_inference,[],[37,40,22,16,21,29,30,35])).
% 58.62/59.43 cnf(63,plain,
% 58.62/59.43 (P2(a5,f1(a4))),
% 58.62/59.43 inference(scs_inference,[],[17,37,40,22,55,16,21,29,30,35,33])).
% 58.62/59.43 cnf(65,plain,
% 58.62/59.43 (P3(f2(x651),x651,x651)),
% 58.62/59.43 inference(rename_variables,[],[22])).
% 58.62/59.43 cnf(67,plain,
% 58.62/59.43 (P3(f2(f2(a3)),a5,a5)),
% 58.62/59.43 inference(scs_inference,[],[17,37,40,43,22,55,65,16,21,29,30,35,33,36])).
% 58.62/59.43 cnf(87,plain,
% 58.62/59.43 (P3(f2(x871),x871,x871)),
% 58.62/59.43 inference(rename_variables,[],[22])).
% 58.62/59.43 cnf(89,plain,
% 58.62/59.43 (P2(a5,f1(f1(a4)))),
% 58.62/59.43 inference(scs_inference,[],[17,57,63,60,22,87,30,29,33])).
% 58.62/59.43 cnf(91,plain,
% 58.62/59.43 (P3(f2(x911),x911,x911)),
% 58.62/59.43 inference(rename_variables,[],[22])).
% 58.62/59.43 cnf(93,plain,
% 58.62/59.43 (P3(f2(a8),a6,a6)),
% 58.62/59.43 inference(scs_inference,[],[17,57,63,60,19,22,87,91,30,29,33,36])).
% 58.62/59.43 cnf(110,plain,
% 58.62/59.43 (P2(f2(x1101),x1101)),
% 58.62/59.43 inference(rename_variables,[],[17])).
% 58.62/59.43 cnf(112,plain,
% 58.62/59.43 (P2(f1(f2(x1121)),x1121)),
% 58.62/59.43 inference(scs_inference,[],[17,110,67,21,29,30])).
% 58.62/59.43 cnf(115,plain,
% 58.62/59.43 (P2(f2(f2(a3)),a5)),
% 58.62/59.43 inference(scs_inference,[],[17,110,67,89,21,60,29,30,34])).
% 58.62/59.43 cnf(140,plain,
% 58.62/59.43 (P2(f2(a3),a5)),
% 58.62/59.43 inference(scs_inference,[],[43,17,40,63,57,21,30,29,34])).
% 58.62/59.43 cnf(142,plain,
% 58.62/59.43 (P3(f2(a9),a6,a6)),
% 58.62/59.43 inference(scs_inference,[],[43,17,40,63,57,20,21,22,30,29,34,36])).
% 58.62/59.43 cnf(158,plain,
% 58.62/59.43 (P2(a3,a4)),
% 58.62/59.43 inference(scs_inference,[],[18,17,140,21,22,29,30,33])).
% 58.62/59.43 cnf(201,plain,
% 58.62/59.43 (~E(f1(f1(a4)),x2011)+P3(a6,a4,x2012)+~P3(a9,a5,x2012)),
% 58.62/59.43 inference(scs_inference,[],[40,18,63,89,20,22,29,13,30,35])).
% 58.62/59.43 cnf(204,plain,
% 58.62/59.43 (~P3(a9,a5,x2041)+P3(a6,a4,x2041)),
% 58.62/59.43 inference(equality_inference,[],[201])).
% 58.62/59.43 cnf(252,plain,
% 58.62/59.43 (P2(x2521,f2(f1(x2521)))),
% 58.62/59.43 inference(scs_inference,[],[16,22,29])).
% 58.62/59.43 cnf(781,plain,
% 58.62/59.43 (P2(a4,f1(a5))),
% 58.62/59.43 inference(scs_inference,[],[18,16,115,29,30])).
% 58.62/59.43 cnf(948,plain,
% 58.62/59.43 (P2(a3,f1(a6))),
% 58.62/59.43 inference(scs_inference,[],[19,17,16,29,30])).
% 58.62/59.43 cnf(953,plain,
% 58.62/59.43 (P3(a8,a5,x9531)+~P3(a6,a4,x9531)),
% 58.62/59.43 inference(scs_inference,[],[19,18,17,16,29,30,12,13,36])).
% 58.62/59.43 cnf(971,plain,
% 58.62/59.43 (P3(a8,a3,x9711)+~P3(a6,f1(a3),x9711)),
% 58.62/59.43 inference(scs_inference,[],[19,21,112,252,948,29,30,12,13,36])).
% 58.62/59.43 cnf(1027,plain,
% 58.62/59.43 (P2(f1(a3),f1(a6))),
% 58.62/59.43 inference(scs_inference,[],[21,948,30])).
% 58.62/59.43 cnf(1224,plain,
% 58.62/59.43 (P2(f2(a6),a9)),
% 58.62/59.43 inference(scs_inference,[],[20,17,29])).
% 58.62/59.43 cnf(1228,plain,
% 58.62/59.43 (P3(x12281,f1(x12281),x12281)),
% 58.62/59.43 inference(rename_variables,[],[21])).
% 58.62/59.43 cnf(1232,plain,
% 58.62/59.43 (P3(a9,a3,x12321)+~P3(a6,f1(a3),x12321)),
% 58.62/59.43 inference(scs_inference,[],[20,17,21,1228,29,30,12,13,36])).
% 58.62/59.43 cnf(1392,plain,
% 58.62/59.43 (P3(x13921,f1(x13921),x13921)),
% 58.62/59.43 inference(rename_variables,[],[21])).
% 58.62/59.43 cnf(1394,plain,
% 58.62/59.43 (P3(a6,f1(a3),a6)),
% 58.62/59.43 inference(scs_inference,[],[21,1392,19,63,30,35])).
% 58.62/59.43 cnf(1753,plain,
% 58.62/59.43 (P2(f2(a3),f2(a5))),
% 58.62/59.43 inference(scs_inference,[],[22,140,29])).
% 58.62/59.43 cnf(1754,plain,
% 58.62/59.43 (P3(f2(x17541),x17541,x17541)),
% 58.62/59.43 inference(rename_variables,[],[22])).
% 58.62/59.43 cnf(1758,plain,
% 58.62/59.43 (~P3(x17581,f2(x17582),f2(x17582))+P3(x17581,x17582,x17582)),
% 58.62/59.43 inference(scs_inference,[],[22,1754,140,29,12,13,36])).
% 58.62/59.43 cnf(2080,plain,
% 58.62/59.43 (P2(f2(a8),a6)),
% 58.62/59.43 inference(scs_inference,[],[93,16,21,34])).
% 58.62/59.43 cnf(2233,plain,
% 58.62/59.43 (P2(f2(a8),f2(a9))),
% 58.62/59.43 inference(scs_inference,[],[142,2080,29])).
% 58.62/59.43 cnf(2235,plain,
% 58.62/59.43 (P2(f2(a9),a6)),
% 58.62/59.43 inference(scs_inference,[],[142,16,21,2080,29,34])).
% 58.62/59.43 cnf(2397,plain,
% 58.62/59.43 (P2(f2(a9),f2(a8))),
% 58.62/59.43 inference(scs_inference,[],[93,2235,29])).
% 58.62/59.43 cnf(2572,plain,
% 58.62/59.43 (P2(a8,a3)),
% 58.62/59.43 inference(scs_inference,[],[1394,971,27])).
% 58.62/59.43 cnf(2769,plain,
% 58.62/59.43 (P2(a9,a3)),
% 58.62/59.43 inference(scs_inference,[],[1394,1232,27])).
% 58.62/59.43 cnf(2770,plain,
% 58.62/59.43 (P2(a9,f2(a3))),
% 58.62/59.43 inference(scs_inference,[],[22,2769,29])).
% 58.62/59.43 cnf(2930,plain,
% 58.62/59.43 (P2(f1(a9),a3)),
% 58.62/59.43 inference(scs_inference,[],[21,2769,30])).
% 58.62/59.43 cnf(2942,plain,
% 58.62/59.43 (P2(f1(a9),f2(a3))),
% 58.62/59.43 inference(scs_inference,[],[22,2930,29])).
% 58.62/59.43 cnf(4523,plain,
% 58.62/59.43 (P3(a4,f1(a5),a4)),
% 58.62/59.43 inference(scs_inference,[],[14,2769,781,28,26])).
% 58.62/59.43 cnf(4524,plain,
% 58.62/59.43 (P1(f1(x45241))),
% 58.62/59.43 inference(rename_variables,[],[14])).
% 58.62/59.43 cnf(4531,plain,
% 58.62/59.43 (P2(f2(a9),f7(a9,a3))),
% 58.62/59.43 inference(scs_inference,[],[14,4524,2769,781,2942,43,22,28,26,25,36,34])).
% 58.62/59.43 cnf(4534,plain,
% 58.62/59.43 (P2(f1(a9),a5)),
% 58.62/59.43 inference(scs_inference,[],[14,4524,2769,781,2942,43,22,28,26,25,36,34,27])).
% 58.62/59.43 cnf(4536,plain,
% 58.62/59.43 (P3(f1(a9),a3,a3)),
% 58.62/59.43 inference(scs_inference,[],[14,4524,2769,781,2942,43,22,28,26,25,36,34,27,1758])).
% 58.62/59.43 cnf(4538,plain,
% 58.62/59.43 (P2(f2(a8),a9)),
% 58.62/59.43 inference(scs_inference,[],[14,4524,2769,781,2942,2080,20,43,22,28,26,25,36,34,27,1758,29])).
% 58.62/59.43 cnf(4542,plain,
% 58.62/59.43 (P3(f7(a9,a3),f1(a3),f7(a9,a3))),
% 58.62/59.43 inference(scs_inference,[],[14,4524,1224,2769,781,2942,2080,20,43,21,22,28,26,25,36,34,27,1758,29,24,35])).
% 58.62/59.43 cnf(4548,plain,
% 58.62/59.43 (P2(f7(a9,a3),f1(a3))),
% 58.62/59.43 inference(scs_inference,[],[4542,27])).
% 58.62/59.43 cnf(4553,plain,
% 58.62/59.43 (P1(f2(x45531))),
% 58.62/59.43 inference(rename_variables,[],[15])).
% 58.62/59.43 cnf(4556,plain,
% 58.62/59.43 (P1(f2(x45561))),
% 58.62/59.43 inference(rename_variables,[],[15])).
% 58.62/59.43 cnf(4558,plain,
% 58.62/59.43 (P2(a9,f2(a5))),
% 58.62/59.43 inference(scs_inference,[],[4542,4531,15,4553,4556,2397,2770,1753,2572,27,28,26,25,24])).
% 58.62/59.43 cnf(4561,plain,
% 58.62/59.43 (P2(f2(a8),f7(a9,a3))),
% 58.62/59.43 inference(scs_inference,[],[4542,4531,15,4553,4556,2397,2770,1753,2572,27,28,26,25,24,30])).
% 58.62/59.43 cnf(4569,plain,
% 58.62/59.43 (P3(a3,a4,f7(a3,a4))),
% 58.62/59.43 inference(scs_inference,[],[158,28])).
% 58.62/59.43 cnf(4572,plain,
% 58.62/59.43 (P1(f2(x45721))),
% 58.62/59.43 inference(rename_variables,[],[15])).
% 58.62/59.43 cnf(4579,plain,
% 58.62/59.43 (P2(a9,a5)),
% 58.62/59.43 inference(scs_inference,[],[14,4534,4561,4558,15,4572,23,16,158,28,26,25,32,24])).
% 58.62/59.43 cnf(4596,plain,
% 58.62/59.43 (P1(f2(x45961))),
% 58.62/59.43 inference(rename_variables,[],[15])).
% 58.62/59.43 cnf(4614,plain,
% 58.62/59.43 ($false),
% 58.62/59.43 inference(scs_inference,[],[14,4579,4548,4538,4569,4523,4536,15,4596,2233,23,1027,158,28,31,26,25,32,24,36,35,33,204,953]),
% 58.62/59.43 ['proof']).
% 58.62/59.43 % SZS output end Proof
% 58.62/59.43 % Total time :58.070000s
%------------------------------------------------------------------------------