%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT005-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 : n011.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:10 EDT 2024
% Result : Unsatisfiable 58.83s 59.04s
% Output : CNFRefutation 58.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : CAT005-1 : TPTP v8.2.0. Released v1.0.0.
% 0.09/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.36 % Computer : n011.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Tue Jun 18 12:03:24 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.50/0.59 start to proof:theBenchmark
% 58.83/59.02 %-------------------------------------------
% 58.83/59.02 % File :CSE---1.7
% 58.83/59.02 % Problem :theBenchmark
% 58.83/59.02 % Transform :cnf
% 58.83/59.02 % Format :tptp:raw
% 58.83/59.02 % Command :java -jar mcs_scs.jar %d %s
% 58.83/59.02
% 58.83/59.02 % Result :Theorem 58.250000s
% 58.83/59.02 % Output :CNFRefutation 58.250000s
% 58.83/59.02 %-------------------------------------------
% 58.83/59.03 %--------------------------------------------------------------------------
% 58.83/59.03 % File : CAT005-1 : TPTP v8.2.0. Released v1.0.0.
% 58.83/59.03 % Domain : Category Theory
% 58.83/59.03 % Problem : Domain is the unique right identity
% 58.83/59.03 % Version : [Mit67] axioms.
% 58.83/59.03 % English : domain(x) is the unique identity i such that xi is defined.
% 58.83/59.03
% 58.83/59.04 % Refs : [Mit67] Mitchell (1967), Theory of Categories
% 58.83/59.04 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 58.83/59.04 % Source : [ANL]
% 58.83/59.04 % Names : C5 [MOW76]
% 58.83/59.04 % : p5.ver1.in [ANL]
% 58.83/59.04
% 58.83/59.04 % Status : Unsatisfiable
% 58.83/59.04 % Rating : 0.00 v6.0.0, 0.22 v5.5.0, 0.25 v5.4.0, 0.20 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.00 v2.0.0
% 58.83/59.04 % Syntax : Number of clauses : 21 ( 9 unt; 0 nHn; 15 RR)
% 58.83/59.04 % Number of literals : 48 ( 2 equ; 28 neg)
% 58.83/59.04 % Maximal clause size : 4 ( 2 avg)
% 58.83/59.04 % Maximal term depth : 2 ( 1 avg)
% 58.83/59.04 % Number of predicates : 4 ( 3 usr; 0 prp; 1-3 aty)
% 58.83/59.04 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 58.83/59.04 % Number of variables : 52 ( 5 sgn)
% 58.83/59.04 % SPC : CNF_UNS_RFO_SEQ_HRN
% 58.83/59.04
% 58.83/59.04 % Comments :
% 58.83/59.04 %--------------------------------------------------------------------------
% 58.83/59.04 %----Include Mitchell's axioms for category theory
% 58.83/59.04 include('Axioms/CAT001-0.ax').
% 58.83/59.04 %--------------------------------------------------------------------------
% 58.83/59.04 cnf(ad_defined,hypothesis,
% 58.83/59.04 defined(a,d) ).
% 58.83/59.04
% 58.83/59.04 cnf(d_is_identity_map,hypothesis,
% 58.83/59.04 identity_map(d) ).
% 58.83/59.04
% 58.83/59.04 cnf(prove_domain_of_a_is_d,negated_conjecture,
% 58.83/59.04 domain(a) != d ).
% 58.83/59.04
% 58.83/59.04 %--------------------------------------------------------------------------
% 58.83/59.04 %-------------------------------------------
% 58.83/59.04 % Proof found
% 58.83/59.04 % SZS status Theorem for theBenchmark
% 58.83/59.04 % SZS output start Proof
% 58.83/59.05 %ClaNum:34(EqnAxiom:13)
% 58.83/59.05 %VarNum:108(SingletonVarNum:52)
% 58.83/59.05 %MaxLitNum:4
% 58.83/59.05 %MaxfuncDepth:1
% 58.83/59.05 %SharedTerms:6
% 58.83/59.05 %goalClause: 22
% 58.83/59.05 %singleGoalClaCount:1
% 58.83/59.05 [14]P1(a1)
% 58.83/59.05 [17]P2(a3,a1)
% 58.83/59.05 [22]~E(f5(a3),a1)
% 58.83/59.05 [15]P1(f5(x151))
% 58.83/59.05 [16]P1(f2(x161))
% 58.83/59.05 [18]P2(x181,f5(x181))
% 58.83/59.05 [19]P2(f2(x191),x191)
% 58.83/59.05 [20]P3(x201,f5(x201),x201)
% 58.83/59.05 [21]P3(f2(x211),x211,x211)
% 58.83/59.05 [27]~P2(x271,x272)+P3(x271,x272,f4(x271,x272))
% 58.83/59.05 [26]P2(x261,x262)+~P3(x261,x262,x263)
% 58.83/59.05 [24]~P1(x241)+~P2(x241,x242)+P3(x241,x242,x242)
% 58.83/59.05 [25]~P1(x252)+~P2(x251,x252)+P3(x251,x252,x251)
% 58.83/59.05 [28]P2(x281,x282)+~P3(x282,x284,x283)+~P2(x281,x283)
% 58.83/59.05 [29]P2(x291,x292)+~P3(x294,x291,x293)+~P2(x293,x292)
% 58.83/59.05 [30]~P3(x303,x304,x301)+E(x301,x302)+~P3(x303,x304,x302)
% 58.83/59.05 [23]~P2(x233,x232)+~P2(x231,x233)+P2(x231,x232)+~P1(x233)
% 58.83/59.05 [31]~P3(x315,x312,x314)+P2(x311,x312)+~P3(x313,x315,x311)+~P2(x313,x314)
% 58.83/59.05 [32]~P3(x321,x325,x323)+P2(x321,x322)+~P3(x325,x324,x322)+~P2(x323,x324)
% 58.83/59.05 [33]~P3(x336,x332,x335)+P3(x331,x332,x333)+~P3(x334,x335,x333)+~P3(x334,x336,x331)
% 58.83/59.05 [34]~P3(x341,x346,x344)+P3(x341,x342,x343)+~P3(x344,x345,x343)+~P3(x346,x345,x342)
% 58.83/59.05 %EqnAxiom
% 58.83/59.05 [1]E(x11,x11)
% 58.83/59.05 [2]E(x22,x21)+~E(x21,x22)
% 58.83/59.05 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.83/59.05 [4]~E(x41,x42)+E(f5(x41),f5(x42))
% 58.83/59.05 [5]~E(x51,x52)+E(f2(x51),f2(x52))
% 58.83/59.05 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 58.83/59.05 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 58.83/59.05 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 58.83/59.05 [9]P3(x92,x93,x94)+~E(x91,x92)+~P3(x91,x93,x94)
% 58.83/59.05 [10]P3(x103,x102,x104)+~E(x101,x102)+~P3(x103,x101,x104)
% 58.83/59.05 [11]P3(x113,x114,x112)+~E(x111,x112)+~P3(x113,x114,x111)
% 58.83/59.05 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123)
% 58.83/59.05 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131)
% 58.83/59.05
% 58.83/59.05 %-------------------------------------------
% 58.83/59.07 cnf(35,plain,
% 58.83/59.07 (P2(f5(x351),f5(x351))),
% 58.83/59.07 inference(scs_inference,[],[20,18,29])).
% 58.83/59.07 cnf(51,plain,
% 58.83/59.07 (P3(x511,f5(x511),x511)),
% 58.83/59.07 inference(rename_variables,[],[20])).
% 58.83/59.07 cnf(53,plain,
% 58.83/59.07 (P3(x531,f5(x531),x532)+~E(x531,x532)),
% 58.83/59.07 inference(scs_inference,[],[20,51,19,29,11])).
% 58.83/59.07 cnf(66,plain,
% 58.83/59.07 (P2(f5(a3),a1)),
% 58.83/59.07 inference(scs_inference,[],[20,17,29])).
% 58.83/59.07 cnf(80,plain,
% 58.83/59.07 (P3(x801,f5(x801),x801)),
% 58.83/59.07 inference(rename_variables,[],[20])).
% 58.83/59.07 cnf(84,plain,
% 58.83/59.07 (P3(f2(x841),x841,x842)+~E(x841,x842)),
% 58.83/59.07 inference(scs_inference,[],[20,80,21,19,35,29,13,10,11])).
% 58.83/59.07 cnf(86,plain,
% 58.83/59.07 (~P3(f5(x861),x862,f5(x861))+P3(x861,x862,x861)),
% 58.83/59.07 inference(scs_inference,[],[20,80,21,19,35,29,13,10,11,12,33])).
% 58.83/59.07 cnf(88,plain,
% 58.83/59.07 (~P3(a3,a1,x881)+P2(x881,f5(a1))),
% 58.83/59.07 inference(scs_inference,[],[20,80,21,19,17,35,29,13,10,11,12,33,31])).
% 58.83/59.07 cnf(95,plain,
% 58.83/59.07 (P2(f5(f5(a3)),a1)),
% 58.83/59.07 inference(scs_inference,[],[20,66,29])).
% 58.83/59.07 cnf(96,plain,
% 58.83/59.07 (P3(x961,f5(x961),x961)),
% 58.83/59.07 inference(rename_variables,[],[20])).
% 58.83/59.07 cnf(99,plain,
% 58.83/59.07 (P2(x991,f5(x992))+~E(x992,x991)),
% 58.83/59.07 inference(scs_inference,[],[20,18,66,29,13,12])).
% 58.83/59.07 cnf(104,plain,
% 58.83/59.07 (P3(x1041,f5(x1041),x1041)),
% 58.83/59.07 inference(rename_variables,[],[20])).
% 58.83/59.07 cnf(106,plain,
% 58.83/59.07 (~P3(f5(x1061),f5(x1061),x1062)+P2(x1061,x1062)),
% 58.83/59.07 inference(scs_inference,[],[20,96,104,21,18,66,29,13,12,34,31,32])).
% 58.83/59.07 cnf(111,plain,
% 58.83/59.07 (P2(a3,x1111)+~E(a1,x1111)),
% 58.83/59.07 inference(scs_inference,[],[17,13])).
% 58.83/59.07 cnf(112,plain,
% 58.83/59.07 (P2(f5(a3),x1121)+~E(a1,x1121)),
% 58.83/59.07 inference(scs_inference,[],[20,17,13,29])).
% 58.83/59.07 cnf(236,plain,
% 58.83/59.07 (~P3(a1,f5(a1),f5(a3))),
% 58.83/59.07 inference(scs_inference,[],[22,20,30])).
% 58.83/59.07 cnf(258,plain,
% 58.83/59.07 (P3(x2581,f5(x2581),x2581)),
% 58.83/59.07 inference(rename_variables,[],[20])).
% 58.83/59.07 cnf(262,plain,
% 58.83/59.07 (~P2(a1,f5(a3))+~P3(f5(a1),f5(a1),f5(a3))),
% 58.83/59.07 inference(scs_inference,[],[22,236,20,258,21,14,30,11,33,24])).
% 58.83/59.07 cnf(359,plain,
% 58.83/59.07 (P3(x3591,f5(x3591),f4(x3591,f5(x3591)))),
% 58.83/59.07 inference(scs_inference,[],[20,26,27])).
% 58.83/59.07 cnf(360,plain,
% 58.83/59.07 (E(x3601,f4(x3601,f5(x3601)))),
% 58.83/59.07 inference(scs_inference,[],[20,359,30])).
% 58.83/59.07 cnf(361,plain,
% 58.83/59.07 (P3(x3611,f5(x3611),f4(x3611,f5(x3611)))),
% 58.83/59.07 inference(rename_variables,[],[359])).
% 58.83/59.07 cnf(363,plain,
% 58.83/59.07 (P3(f4(x3631,f5(x3631)),f5(x3631),x3631)),
% 58.83/59.07 inference(scs_inference,[],[20,359,30,9])).
% 58.83/59.07 cnf(364,plain,
% 58.83/59.07 (P3(f2(x3641),f4(x3641,f5(x3641)),x3641)),
% 58.83/59.07 inference(scs_inference,[],[20,21,359,30,9,10])).
% 58.83/59.07 cnf(365,plain,
% 58.83/59.07 (P3(f2(x3651),x3651,x3651)),
% 58.83/59.07 inference(rename_variables,[],[21])).
% 58.83/59.07 cnf(372,plain,
% 58.83/59.07 (P3(f2(x3721),x3721,x3721)),
% 58.83/59.07 inference(rename_variables,[],[21])).
% 58.83/59.07 cnf(375,plain,
% 58.83/59.07 (P3(f2(x3751),x3751,x3751)),
% 58.83/59.07 inference(rename_variables,[],[21])).
% 58.83/59.07 cnf(381,plain,
% 58.83/59.07 (P2(a3,f2(a1))),
% 58.83/59.07 inference(scs_inference,[],[236,20,21,365,372,375,359,361,19,17,30,9,10,11,13,12,34,32,2,84,99,8,28])).
% 58.83/59.07 cnf(384,plain,
% 58.83/59.07 (P2(f5(a3),f2(a1))),
% 58.83/59.07 inference(scs_inference,[],[236,20,21,365,372,375,359,361,19,17,30,9,10,11,13,12,34,32,2,84,99,8,28,29])).
% 58.83/59.07 cnf(394,plain,
% 58.83/59.07 (P2(a3,f4(a1,f5(a1)))),
% 58.83/59.07 inference(scs_inference,[],[360,111])).
% 58.83/59.07 cnf(395,plain,
% 58.83/59.07 (E(x3951,f4(x3951,f5(x3951)))),
% 58.83/59.07 inference(rename_variables,[],[360])).
% 58.83/59.07 cnf(396,plain,
% 58.83/59.07 (P2(f5(a3),f4(a1,f5(a1)))),
% 58.83/59.07 inference(scs_inference,[],[360,395,111,112])).
% 58.83/59.07 cnf(397,plain,
% 58.83/59.07 (E(x3971,f4(x3971,f5(x3971)))),
% 58.83/59.07 inference(rename_variables,[],[360])).
% 58.83/59.07 cnf(399,plain,
% 58.83/59.07 (P3(f2(x3991),x3991,f4(x3991,f5(x3991)))),
% 58.83/59.07 inference(scs_inference,[],[360,395,397,111,112,84])).
% 58.83/59.07 cnf(400,plain,
% 58.83/59.07 (E(f4(x4001,f5(x4001)),x4001)),
% 58.83/59.07 inference(scs_inference,[],[360,395,397,111,112,84,2])).
% 58.83/59.07 cnf(403,plain,
% 58.83/59.07 (P1(f4(a1,f5(a1)))),
% 58.83/59.07 inference(scs_inference,[],[14,22,360,395,397,111,112,84,2,99,3,8])).
% 58.83/59.07 cnf(404,plain,
% 58.83/59.07 (E(x4041,f4(x4041,f5(x4041)))),
% 58.83/59.07 inference(rename_variables,[],[360])).
% 58.83/59.07 cnf(406,plain,
% 58.83/59.07 (P3(f4(x4061,f5(x4061)),f5(x4061),x4061)),
% 58.83/59.07 inference(rename_variables,[],[363])).
% 58.83/59.07 cnf(409,plain,
% 58.83/59.07 (P3(x4091,f5(x4091),x4091)),
% 58.83/59.07 inference(rename_variables,[],[20])).
% 58.83/59.07 cnf(413,plain,
% 58.83/59.07 (P3(x4131,f5(f5(x4131)),x4131)),
% 58.83/59.07 inference(scs_inference,[],[14,22,20,409,360,395,397,404,363,406,384,381,111,112,84,2,99,3,8,30,29,12,33])).
% 58.83/59.07 cnf(416,plain,
% 58.83/59.07 (P3(f2(f2(x4161)),x4161,x4161)),
% 58.83/59.07 inference(scs_inference,[],[14,22,20,409,360,395,397,404,21,363,406,364,384,381,111,112,84,2,99,3,8,30,29,12,33,34])).
% 58.83/59.07 cnf(507,plain,
% 58.83/59.07 (P3(x5071,f5(a1),f4(x5071,f5(a1)))+~P3(a3,a1,x5071)),
% 58.83/59.07 inference(scs_inference,[],[88,27])).
% 58.83/59.07 cnf(510,plain,
% 58.83/59.07 (~P3(f5(a1),f5(a1),f5(a3))),
% 58.83/59.07 inference(scs_inference,[],[106,262])).
% 58.83/59.07 cnf(513,plain,
% 58.83/59.07 (P2(f2(x5131),f2(x5131))),
% 58.83/59.07 inference(scs_inference,[],[21,19,28])).
% 58.83/59.07 cnf(531,plain,
% 58.83/59.07 (P3(f2(x5311),x5311,x5311)),
% 58.83/59.07 inference(rename_variables,[],[21])).
% 58.83/59.07 cnf(533,plain,
% 58.83/59.07 (~P3(a3,a1,x5331)+P2(f2(a3),x5331)),
% 58.83/59.07 inference(scs_inference,[],[21,531,17,18,28,32])).
% 58.83/59.07 cnf(540,plain,
% 58.83/59.07 (P3(f2(a3),x5401,f4(f2(a3),x5401))+~P3(a3,a1,x5401)),
% 58.83/59.07 inference(scs_inference,[],[533,27])).
% 58.83/59.07 cnf(584,plain,
% 58.83/59.07 (P3(f2(x5841),x5841,x5841)),
% 58.83/59.07 inference(rename_variables,[],[21])).
% 58.83/59.07 cnf(586,plain,
% 58.83/59.07 (P2(f2(a3),f2(x5861))+~P3(a3,f4(a1,f5(a1)),x5861)),
% 58.83/59.07 inference(scs_inference,[],[21,584,394,32,28])).
% 58.83/59.07 cnf(822,plain,
% 58.83/59.07 (P3(f4(x8221,f5(x8221)),f5(x8221),x8221)),
% 58.83/59.07 inference(rename_variables,[],[363])).
% 58.83/59.07 cnf(824,plain,
% 58.83/59.07 (~P3(a3,f4(a1,f5(a1)),x8241)+P2(x8241,f5(a1))),
% 58.83/59.07 inference(scs_inference,[],[363,822,17,32,31])).
% 58.83/59.07 cnf(828,plain,
% 58.83/59.07 (~P3(f5(x8281),f5(x8281),x8282)+P2(f4(x8281,f5(x8281)),x8282)),
% 58.83/59.07 inference(scs_inference,[],[363,18,32])).
% 58.83/59.07 cnf(837,plain,
% 58.83/59.07 (P3(f4(x8371,f5(x8371)),f5(x8371),x8371)),
% 58.83/59.07 inference(rename_variables,[],[363])).
% 58.83/59.07 cnf(839,plain,
% 58.83/59.07 (~P3(f5(a3),f4(a1,f5(a1)),x8391)+P2(x8391,f5(a1))),
% 58.83/59.07 inference(scs_inference,[],[363,837,66,381,32,31])).
% 58.83/59.07 cnf(919,plain,
% 58.83/59.07 (~P3(f5(f5(a3)),a1,x9191)+P2(a3,x9191)),
% 58.83/59.07 inference(scs_inference,[],[413,17,32])).
% 58.83/59.07 cnf(930,plain,
% 58.83/59.07 (P3(a3,x9301,f4(a3,x9301))+~P3(f5(f5(a3)),a1,x9301)),
% 58.83/59.07 inference(scs_inference,[],[919,27])).
% 58.83/59.07 cnf(931,plain,
% 58.83/59.07 (~P3(a3,a1,x9311)+P2(x9311,f5(f5(a1)))),
% 58.83/59.07 inference(scs_inference,[],[413,17,31])).
% 58.83/59.07 cnf(974,plain,
% 58.83/59.07 (~P3(a3,a1,x9741)+P2(f2(f2(a3)),x9741)),
% 58.83/59.07 inference(scs_inference,[],[416,17,32])).
% 58.83/59.07 cnf(980,plain,
% 58.83/59.07 (P3(f2(f2(a3)),x9801,x9801)+~P3(a3,a1,x9801)),
% 58.83/59.07 inference(scs_inference,[],[16,974,24])).
% 58.83/59.07 cnf(1157,plain,
% 58.83/59.07 (P3(x11571,f5(a1),f4(x11571,f5(a1)))+~P3(a3,f4(a1,f5(a1)),x11571)),
% 58.83/59.07 inference(scs_inference,[],[824,27])).
% 58.83/59.07 cnf(1305,plain,
% 58.83/59.07 (~P3(a3,f4(a1,f5(a1)),x13051)+P3(f2(a3),f2(x13051),f4(f2(a3),f2(x13051)))),
% 58.83/59.07 inference(scs_inference,[],[586,27])).
% 58.83/59.07 cnf(1328,plain,
% 58.83/59.07 (P3(f4(a1,f5(a1)),x13281,x13281)+~P3(f5(a1),f5(a1),x13281)),
% 58.83/59.07 inference(scs_inference,[],[403,828,24])).
% 58.83/59.07 cnf(1330,plain,
% 58.83/59.07 (P2(f5(a3),f5(a1))),
% 58.83/59.07 inference(scs_inference,[],[396,403,839,25])).
% 58.83/59.07 cnf(1419,plain,
% 58.83/59.07 (P3(a3,a1,f4(a3,a1))),
% 58.83/59.07 inference(scs_inference,[],[95,15,930,24])).
% 58.83/59.07 cnf(1422,plain,
% 58.83/59.07 (P2(f2(a3),f4(a3,a1))),
% 58.83/59.07 inference(scs_inference,[],[1419,88,533])).
% 58.83/59.07 cnf(1434,plain,
% 58.83/59.07 (P3(a3,f4(a1,f5(a1)),f4(a3,a1))),
% 58.83/59.07 inference(scs_inference,[],[360,1419,88,533,974,507,980,540,931,10])).
% 58.83/59.07 cnf(1435,plain,
% 58.83/59.07 (E(x14351,f4(x14351,f5(x14351)))),
% 58.83/59.07 inference(rename_variables,[],[360])).
% 58.83/59.07 cnf(1437,plain,
% 58.83/59.07 (P3(x14371,f5(x14371),x14371)),
% 58.83/59.07 inference(rename_variables,[],[20])).
% 58.83/59.07 cnf(1441,plain,
% 58.83/59.07 (P3(f2(a3),f4(a3,a1),f4(a3,a1))),
% 58.83/59.07 inference(scs_inference,[],[360,1435,20,21,1419,88,533,974,507,980,540,931,10,29,9,34])).
% 58.83/59.07 cnf(1444,plain,
% 58.83/59.07 (P3(f4(a3,a1),f5(a1),f4(a3,a1))),
% 58.83/59.07 inference(scs_inference,[],[360,1435,20,1437,21,1419,88,533,974,507,980,540,931,10,29,9,34,33])).
% 58.83/59.07 cnf(1457,plain,
% 58.83/59.07 (P3(x14571,f5(x14571),x14571)),
% 58.83/59.07 inference(rename_variables,[],[20])).
% 58.83/59.07 cnf(1460,plain,
% 58.83/59.07 (P3(x14601,f5(x14601),x14601)),
% 58.83/59.07 inference(rename_variables,[],[20])).
% 58.83/59.07 cnf(1462,plain,
% 58.83/59.07 (~P3(f5(a1),f5(a1),x14621)+~P3(x14621,f5(f5(a1)),f5(a3))),
% 58.83/59.07 inference(scs_inference,[],[510,20,1457,1460,1422,1444,29,33,34])).
% 58.83/59.07 cnf(1579,plain,
% 58.83/59.07 (P2(a1,f5(f4(a3,a1)))),
% 58.83/59.07 inference(scs_inference,[],[1419,19,18,28,29])).
% 58.83/59.07 cnf(1580,plain,
% 58.83/59.07 (P2(x15801,f5(x15801))),
% 58.83/59.07 inference(rename_variables,[],[18])).
% 58.83/59.07 cnf(1586,plain,
% 58.83/59.07 (E(x15861,f4(x15861,f5(x15861)))),
% 58.83/59.07 inference(rename_variables,[],[360])).
% 58.83/59.07 cnf(1587,plain,
% 58.83/59.07 (P2(a3,f4(x15871,f5(x15871)))+~P3(a1,f5(f4(a3,a1)),x15871)),
% 58.83/59.07 inference(scs_inference,[],[1419,360,1586,19,18,1580,28,29,32,12,13])).
% 58.83/59.07 cnf(1725,plain,
% 58.83/59.07 (~P3(f2(a3),f2(a3),x17251)+P2(x17251,f4(a3,a1))),
% 58.83/59.07 inference(scs_inference,[],[1441,1422,31])).
% 58.83/59.07 cnf(1727,plain,
% 58.83/59.07 (P2(x17271,f2(a3))+~P3(f2(a3),f2(a3),x17271)),
% 58.83/59.07 inference(scs_inference,[],[1441,1422,31,28])).
% 58.83/59.07 cnf(2086,plain,
% 58.83/59.07 (~E(f5(a1),f5(a3))+~P3(f5(a1),f5(a1),f5(a1))),
% 58.83/59.07 inference(scs_inference,[],[1462,53])).
% 58.83/59.07 cnf(2094,plain,
% 58.83/59.07 (~E(f5(a3),f5(a1))+~P3(f5(a1),f5(a1),f5(a1))),
% 58.83/59.07 inference(scs_inference,[],[2086,2])).
% 58.83/59.07 cnf(2107,plain,
% 58.83/59.07 (~E(a3,a1)+~P3(f5(a1),f5(a1),f5(a1))),
% 58.83/59.07 inference(scs_inference,[],[2094,4])).
% 58.83/59.07 cnf(2108,plain,
% 58.83/59.07 (~E(a1,a3)+~P3(f5(a1),f5(a1),f5(a1))),
% 58.83/59.07 inference(scs_inference,[],[2107,2])).
% 58.83/59.07 cnf(2117,plain,
% 58.83/59.07 (~E(a1,a3)),
% 58.83/59.07 inference(scs_inference,[],[35,15,2108,24])).
% 58.83/59.07 cnf(2123,plain,
% 58.83/59.07 (P3(a3,f4(a1,f5(a1)),a3)+~P3(a1,f5(f4(a3,a1)),a1)),
% 58.83/59.07 inference(scs_inference,[],[403,1587,25])).
% 58.83/59.07 cnf(2197,plain,
% 58.83/59.07 (~P3(a3,f5(a3),a1)),
% 58.83/59.07 inference(scs_inference,[],[2117,20,400,3,30])).
% 58.83/59.07 cnf(2204,plain,
% 58.83/59.07 (~E(a3,a1)),
% 58.83/59.07 inference(scs_inference,[],[2117,2197,20,21,30,11])).
% 58.83/59.07 cnf(2382,plain,
% 58.83/59.07 (~P3(a1,f5(a1),a3)),
% 58.83/59.07 inference(scs_inference,[],[2204,20,400,3,30])).
% 58.83/59.07 cnf(2401,plain,
% 58.83/59.07 (~P3(f2(a1),f4(a1,f5(a1)),a3)),
% 58.83/59.07 inference(scs_inference,[],[2204,364,30])).
% 58.83/59.07 cnf(2431,plain,
% 58.83/59.07 (~P3(f2(a1),f2(a1),x24311)+~P3(x24311,a1,a3)),
% 58.83/59.07 inference(scs_inference,[],[2401,399,34])).
% 58.83/59.07 cnf(2447,plain,
% 58.83/59.07 (~P3(f4(f2(a1),f2(a1)),a1,a3)),
% 58.83/59.07 inference(scs_inference,[],[513,2431,27])).
% 58.83/59.07 cnf(2607,plain,
% 58.83/59.07 (~P3(f5(a1),f5(a1),x26071)+~P3(f4(a1,f5(a1)),x26071,a3)),
% 58.83/59.07 inference(scs_inference,[],[2382,363,33])).
% 58.83/59.07 cnf(2802,plain,
% 58.83/59.07 (~P3(f4(f2(a1),f2(a1)),f2(a1),x28021)+~P3(x28021,f4(a1,f5(a1)),a3)),
% 58.83/59.07 inference(scs_inference,[],[2447,364,34])).
% 58.83/59.07 cnf(3011,plain,
% 58.83/59.07 (~P3(f5(a1),f5(a1),a3)),
% 58.83/59.07 inference(scs_inference,[],[2607,1328])).
% 58.83/59.07 cnf(4209,plain,
% 58.83/59.07 (P3(a3,f4(a1,f5(a1)),a3)),
% 58.83/59.07 inference(scs_inference,[],[1579,15,2123,25])).
% 58.83/59.07 cnf(4220,plain,
% 58.83/59.07 (P2(a3,f5(a1))),
% 58.83/59.07 inference(scs_inference,[],[4209,1305,1725,1727,2802,1157,824])).
% 58.83/59.07 cnf(4222,plain,
% 58.83/59.08 (~P3(a3,f4(a1,f5(a1)),a1)),
% 58.83/59.08 inference(scs_inference,[],[2117,4209,1305,1725,1727,2802,1157,824,30])).
% 58.83/59.08 cnf(4238,plain,
% 58.83/59.08 (P3(f2(x42381),x42381,x42381)),
% 58.83/59.08 inference(rename_variables,[],[21])).
% 58.83/59.08 cnf(4240,plain,
% 58.83/59.08 (~P3(a3,a1,a1)),
% 58.83/59.08 inference(scs_inference,[],[4222,2401,1419,21,4238,1434,4209,9,33,34])).
% 58.83/59.08 cnf(4243,plain,
% 58.83/59.08 (~P1(a3)),
% 58.83/59.08 inference(scs_inference,[],[4222,2401,1419,21,4238,17,1434,4209,9,33,34,24])).
% 58.83/59.08 cnf(4259,plain,
% 58.83/59.08 (P3(f2(f2(x42591)),x42591,x42591)),
% 58.83/59.08 inference(rename_variables,[],[416])).
% 58.83/59.08 cnf(4263,plain,
% 58.83/59.08 (~P3(f4(a3,a1),f5(a1),a1)),
% 58.83/59.08 inference(scs_inference,[],[4222,1419,359,1434,416,4259,4240,9,33,34])).
% 58.83/59.08 cnf(4480,plain,
% 58.83/59.08 (P3(f2(a1),a1,f2(a1))),
% 58.83/59.08 inference(scs_inference,[],[4243,14,16,19,8,25])).
% 58.83/59.08 cnf(4481,plain,
% 58.83/59.08 (P2(f2(x44811),x44811)),
% 58.83/59.08 inference(rename_variables,[],[19])).
% 58.83/59.08 cnf(4483,plain,
% 58.83/59.08 (P3(a1,f5(a1),f5(a1))),
% 58.83/59.08 inference(scs_inference,[],[4243,14,16,18,19,8,25,24])).
% 58.83/59.08 cnf(4484,plain,
% 58.83/59.08 (P2(x44841,f5(x44841))),
% 58.83/59.08 inference(rename_variables,[],[18])).
% 58.83/59.08 cnf(4486,plain,
% 58.83/59.08 (P2(f2(a1),f5(a1))),
% 58.83/59.08 inference(scs_inference,[],[4243,14,16,18,4484,19,4481,8,25,24,23])).
% 58.83/59.08 cnf(4490,plain,
% 58.83/59.08 (P3(f2(a1),f5(a1),f5(a1))),
% 58.83/59.08 inference(scs_inference,[],[4243,14,16,18,4484,19,4481,21,8,25,24,23,34])).
% 58.83/59.08 cnf(4493,plain,
% 58.83/59.08 (~E(a3,f2(x44931))),
% 58.83/59.08 inference(scs_inference,[],[4243,14,16,18,4484,19,4481,21,8,25,24,23,34,2])).
% 58.83/59.08 cnf(4503,plain,
% 58.83/59.08 (P3(f5(a3),f2(a1),f5(a3))),
% 58.83/59.08 inference(scs_inference,[],[384,16,25])).
% 58.83/59.08 cnf(4509,plain,
% 58.83/59.08 (P3(f5(a3),f5(a1),f5(a1))),
% 58.83/59.08 inference(scs_inference,[],[4493,1330,384,16,15,21,25,30,24])).
% 58.83/59.08 cnf(4512,plain,
% 58.83/59.08 (P2(f2(a1),f5(a3))),
% 58.83/59.08 inference(scs_inference,[],[4486,4493,1330,384,16,15,21,25,30,24,28])).
% 58.83/59.08 cnf(4517,plain,
% 58.83/59.08 (P3(a3,f2(a1),a3)),
% 58.83/59.08 inference(scs_inference,[],[4486,4483,4493,4263,1330,384,16,15,21,20,25,30,24,28,33,86])).
% 58.83/59.08 cnf(4539,plain,
% 58.83/59.08 (~P3(f5(a3),f2(a1),a1)),
% 58.83/59.08 inference(scs_inference,[],[22,4503,4512,15,25,30])).
% 58.83/59.08 cnf(4541,plain,
% 58.83/59.08 (P3(f2(a1),f5(a3),f5(a3))),
% 58.83/59.08 inference(scs_inference,[],[22,4503,4512,16,15,25,30,24])).
% 58.83/59.08 cnf(4547,plain,
% 58.83/59.08 (~P3(a3,f2(a1),f2(a1))),
% 58.83/59.08 inference(scs_inference,[],[22,4509,4503,4512,4240,4263,16,15,21,20,25,30,24,33,34])).
% 58.83/59.08 cnf(4551,plain,
% 58.83/59.08 (P3(f2(a1),f5(a1),f2(a1))),
% 58.83/59.08 inference(scs_inference,[],[4486,15,25])).
% 58.83/59.08 cnf(4552,plain,
% 58.83/59.08 (P1(f5(x45521))),
% 58.83/59.08 inference(rename_variables,[],[15])).
% 58.83/59.08 cnf(4556,plain,
% 58.83/59.08 (P3(f5(a3),f2(a1),f2(a1))),
% 58.83/59.08 inference(scs_inference,[],[22,4541,4486,384,15,4552,25,30,24])).
% 58.83/59.08 cnf(4565,plain,
% 58.83/59.08 (P1(f5(x45651))),
% 58.83/59.08 inference(rename_variables,[],[15])).
% 58.83/59.08 cnf(4573,plain,
% 58.83/59.08 (~E(f5(x45731),a3)),
% 58.83/59.08 inference(scs_inference,[],[4517,4551,4547,4243,4493,4220,3011,15,4565,25,30,34,33,8])).
% 58.83/59.08 cnf(4579,plain,
% 58.83/59.08 ($false),
% 58.83/59.08 inference(scs_inference,[],[4539,4573,4490,4556,4480,21,30,34]),
% 58.83/59.08 ['proof']).
% 58.83/59.08 % SZS output end Proof
% 58.83/59.08 % Total time :58.250000s
%------------------------------------------------------------------------------