%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT006-1 : 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 : n013.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:11 EDT 2024
% Result : Unsatisfiable 58.59s 58.64s
% Output : CNFRefutation 58.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : CAT006-1 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n013.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Tue Jun 18 12:20:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.48/0.56 start to proof:theBenchmark
% 58.59/58.62 %-------------------------------------------
% 58.59/58.62 % File :CSE---1.7
% 58.59/58.62 % Problem :theBenchmark
% 58.59/58.62 % Transform :cnf
% 58.59/58.62 % Format :tptp:raw
% 58.59/58.62 % Command :java -jar mcs_scs.jar %d %s
% 58.59/58.62
% 58.59/58.63 % Result :Theorem 58.040000s
% 58.59/58.63 % Output :CNFRefutation 58.040000s
% 58.59/58.63 %-------------------------------------------
% 58.59/58.64 %--------------------------------------------------------------------------
% 58.59/58.64 % File : CAT006-1 : TPTP v8.2.0. Released v1.0.0.
% 58.59/58.64 % Domain : Category Theory
% 58.59/58.64 % Problem : Codomain is the unique left identity
% 58.59/58.64 % Version : [Mit67] axioms.
% 58.59/58.64 % English : codomain(x) is the unique identity j such that jx is defined.
% 58.59/58.64
% 58.59/58.64 % Refs : [Mit67] Mitchell (1967), Theory of Categories
% 58.59/58.64 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 58.59/58.64 % Source : [ANL]
% 58.59/58.64 % Names : C6 [MOW76]
% 58.59/58.64 % : p6.ver1.in [ANL]
% 58.59/58.64
% 58.59/58.64 % Status : Unsatisfiable
% 58.59/58.64 % 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.14 v5.0.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.00 v2.0.0
% 58.59/58.64 % Syntax : Number of clauses : 21 ( 9 unt; 0 nHn; 15 RR)
% 58.59/58.64 % Number of literals : 48 ( 2 equ; 28 neg)
% 58.59/58.64 % Maximal clause size : 4 ( 2 avg)
% 58.59/58.64 % Maximal term depth : 2 ( 1 avg)
% 58.59/58.64 % Number of predicates : 4 ( 3 usr; 0 prp; 1-3 aty)
% 58.59/58.64 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 58.59/58.64 % Number of variables : 52 ( 5 sgn)
% 58.59/58.64 % SPC : CNF_UNS_RFO_SEQ_HRN
% 58.59/58.64
% 58.59/58.64 % Comments :
% 58.59/58.64 %--------------------------------------------------------------------------
% 58.59/58.64 %----Include Mitchell's axioms for category theory
% 58.59/58.64 include('Axioms/CAT001-0.ax').
% 58.59/58.64 %--------------------------------------------------------------------------
% 58.59/58.64 cnf(ha_defined,hypothesis,
% 58.59/58.64 defined(h,a) ).
% 58.59/58.64
% 58.59/58.64 cnf(h_is_the_identity_map,hypothesis,
% 58.59/58.64 identity_map(h) ).
% 58.59/58.64
% 58.59/58.64 cnf(prove_codomain_of_a_is_h,negated_conjecture,
% 58.59/58.64 codomain(a) != h ).
% 58.59/58.64
% 58.59/58.64 %--------------------------------------------------------------------------
% 58.59/58.64 %-------------------------------------------
% 58.59/58.64 % Proof found
% 58.59/58.64 % SZS status Theorem for theBenchmark
% 58.59/58.64 % SZS output start Proof
% 58.59/58.65 %ClaNum:34(EqnAxiom:13)
% 58.59/58.65 %VarNum:108(SingletonVarNum:52)
% 58.59/58.65 %MaxLitNum:4
% 58.59/58.65 %MaxfuncDepth:1
% 58.59/58.65 %SharedTerms:6
% 58.59/58.65 %goalClause: 22
% 58.59/58.65 %singleGoalClaCount:1
% 58.59/58.65 [14]P1(a1)
% 58.59/58.65 [17]P2(a1,a4)
% 58.59/58.65 [22]~E(f3(a4),a1)
% 58.59/58.65 [15]P1(f2(x151))
% 58.59/58.65 [16]P1(f3(x161))
% 58.59/58.65 [18]P2(x181,f2(x181))
% 58.59/58.65 [19]P2(f3(x191),x191)
% 58.59/58.65 [20]P3(x201,f2(x201),x201)
% 58.59/58.65 [21]P3(f3(x211),x211,x211)
% 58.59/58.65 [27]~P2(x271,x272)+P3(x271,x272,f5(x271,x272))
% 58.59/58.65 [26]P2(x261,x262)+~P3(x261,x262,x263)
% 58.59/58.65 [24]~P1(x241)+~P2(x241,x242)+P3(x241,x242,x242)
% 58.59/58.65 [25]~P1(x252)+~P2(x251,x252)+P3(x251,x252,x251)
% 58.59/58.65 [28]P2(x281,x282)+~P3(x282,x284,x283)+~P2(x281,x283)
% 58.59/58.65 [29]P2(x291,x292)+~P3(x294,x291,x293)+~P2(x293,x292)
% 58.59/58.65 [30]~P3(x303,x304,x301)+E(x301,x302)+~P3(x303,x304,x302)
% 58.59/58.65 [23]~P2(x233,x232)+~P2(x231,x233)+P2(x231,x232)+~P1(x233)
% 58.59/58.65 [31]~P3(x315,x312,x314)+P2(x311,x312)+~P3(x313,x315,x311)+~P2(x313,x314)
% 58.59/58.65 [32]~P3(x321,x325,x323)+P2(x321,x322)+~P3(x325,x324,x322)+~P2(x323,x324)
% 58.59/58.65 [33]~P3(x336,x332,x335)+P3(x331,x332,x333)+~P3(x334,x335,x333)+~P3(x334,x336,x331)
% 58.59/58.65 [34]~P3(x341,x346,x344)+P3(x341,x342,x343)+~P3(x344,x345,x343)+~P3(x346,x345,x342)
% 58.59/58.65 %EqnAxiom
% 58.59/58.65 [1]E(x11,x11)
% 58.59/58.65 [2]E(x22,x21)+~E(x21,x22)
% 58.59/58.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.59/58.65 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 58.59/58.65 [5]~E(x51,x52)+E(f3(x51),f3(x52))
% 58.59/58.65 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 58.59/58.65 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 58.59/58.65 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 58.59/58.65 [9]P3(x92,x93,x94)+~E(x91,x92)+~P3(x91,x93,x94)
% 58.59/58.65 [10]P3(x103,x102,x104)+~E(x101,x102)+~P3(x103,x101,x104)
% 58.59/58.65 [11]P3(x113,x114,x112)+~E(x111,x112)+~P3(x113,x114,x111)
% 58.59/58.65 [12]P2(x122,x123)+~E(x121,x122)+~P2(x121,x123)
% 58.59/58.65 [13]P2(x133,x132)+~E(x131,x132)+~P2(x133,x131)
% 58.59/58.65
% 58.59/58.65 %-------------------------------------------
% 58.59/58.67 cnf(35,plain,
% 58.59/58.67 (P2(f2(x351),f2(x351))),
% 58.59/58.67 inference(scs_inference,[],[20,18,29])).
% 58.59/58.67 cnf(51,plain,
% 58.59/58.67 (P3(x511,f2(x511),x511)),
% 58.59/58.67 inference(rename_variables,[],[20])).
% 58.59/58.67 cnf(55,plain,
% 58.59/58.67 (P3(x551,x552,x551)+~E(f2(x551),x552)),
% 58.59/58.67 inference(scs_inference,[],[20,51,21,19,29,12,9,10])).
% 58.59/58.67 cnf(57,plain,
% 58.59/58.67 (P2(f3(x571),x572)+~E(x571,x572)),
% 58.59/58.67 inference(scs_inference,[],[20,51,21,19,29,12,9,10,11,13])).
% 58.59/58.67 cnf(72,plain,
% 58.59/58.67 (P3(f3(x721),x721,x722)+~E(x721,x722)),
% 58.59/58.67 inference(scs_inference,[],[20,21,35,29,12,10,11])).
% 58.59/58.67 cnf(81,plain,
% 58.59/58.67 (P2(f2(a1),a4)),
% 58.59/58.67 inference(scs_inference,[],[20,17,29])).
% 58.59/58.67 cnf(94,plain,
% 58.59/58.67 (P2(f2(f2(a1)),a4)),
% 58.59/58.67 inference(scs_inference,[],[20,81,29])).
% 58.59/58.67 cnf(95,plain,
% 58.59/58.67 (P3(x951,f2(x951),x951)),
% 58.59/58.67 inference(rename_variables,[],[20])).
% 58.59/58.67 cnf(98,plain,
% 58.59/58.67 (P2(a1,x981)+~E(a4,x981)),
% 58.59/58.67 inference(scs_inference,[],[20,17,81,29,12,13])).
% 58.59/58.67 cnf(101,plain,
% 58.59/58.67 (~P3(a1,a4,x1011)+P2(x1011,f2(a4))),
% 58.59/58.67 inference(scs_inference,[],[20,95,17,81,29,12,13,33,31])).
% 58.59/58.67 cnf(109,plain,
% 58.59/58.67 (P2(x1091,f2(x1092))+~E(x1092,x1091)),
% 58.59/58.67 inference(scs_inference,[],[18,12])).
% 58.59/58.67 cnf(163,plain,
% 58.59/58.67 (P2(f2(a1),x1631)+~E(a4,x1631)),
% 58.59/58.67 inference(scs_inference,[],[81,13])).
% 58.59/58.67 cnf(205,plain,
% 58.59/58.67 (~P3(a1,f2(a1),f3(a4))),
% 58.59/58.67 inference(scs_inference,[],[22,20,30])).
% 58.59/58.67 cnf(220,plain,
% 58.59/58.67 (~P3(f3(a1),a1,f3(a4))),
% 58.59/58.67 inference(scs_inference,[],[22,21,30])).
% 58.59/58.67 cnf(221,plain,
% 58.59/58.67 (P3(f3(x2211),x2211,x2211)),
% 58.59/58.67 inference(rename_variables,[],[21])).
% 58.59/58.67 cnf(224,plain,
% 58.59/58.67 (P3(x2241,f2(x2241),x2241)),
% 58.59/58.67 inference(rename_variables,[],[20])).
% 58.59/58.67 cnf(232,plain,
% 58.59/58.67 (P2(f3(x2321),x2321)),
% 58.59/58.67 inference(rename_variables,[],[19])).
% 58.59/58.67 cnf(235,plain,
% 58.59/58.67 (P3(x2351,f2(x2351),x2351)),
% 58.59/58.67 inference(rename_variables,[],[20])).
% 58.59/58.67 cnf(239,plain,
% 58.59/58.67 (P2(f3(x2391),x2391)),
% 58.59/58.67 inference(rename_variables,[],[19])).
% 58.59/58.67 cnf(243,plain,
% 58.59/58.67 (~P3(a1,f3(f2(a1)),f3(a4))+~P2(f3(a4),a1)),
% 58.59/58.67 inference(scs_inference,[],[22,205,20,224,235,21,221,19,232,239,35,18,14,15,30,11,34,25,28,9,10,29,12,13,23])).
% 58.59/58.67 cnf(256,plain,
% 58.59/58.67 (~P2(f3(a4),a1)+~P3(f3(a1),f3(a1),f3(a4))),
% 58.59/58.67 inference(scs_inference,[],[220,21,14,34,25])).
% 58.59/58.67 cnf(361,plain,
% 58.59/58.67 (~P2(a1,f3(a4))+~P3(f2(a1),f2(a1),f3(a4))),
% 58.59/58.67 inference(scs_inference,[],[205,20,14,33,24])).
% 58.59/58.67 cnf(379,plain,
% 58.59/58.67 (P3(x3791,f2(x3791),f5(x3791,f2(x3791)))),
% 58.59/58.67 inference(scs_inference,[],[20,26,27])).
% 58.59/58.67 cnf(380,plain,
% 58.59/58.67 (E(x3801,f5(x3801,f2(x3801)))),
% 58.59/58.67 inference(scs_inference,[],[20,379,30])).
% 58.59/58.67 cnf(383,plain,
% 58.59/58.67 (P3(f5(x3831,f2(x3831)),f2(x3831),x3831)),
% 58.59/58.67 inference(scs_inference,[],[20,379,30,9])).
% 58.59/58.67 cnf(384,plain,
% 58.59/58.67 (P3(f3(x3841),f5(x3841,f2(x3841)),x3841)),
% 58.59/58.67 inference(scs_inference,[],[20,21,379,30,9,10])).
% 58.59/58.67 cnf(385,plain,
% 58.59/58.67 (P3(f3(x3851),x3851,x3851)),
% 58.59/58.67 inference(rename_variables,[],[21])).
% 58.59/58.67 cnf(389,plain,
% 58.59/58.67 (P3(f3(f3(a1)),a1,a1)),
% 58.59/58.67 inference(scs_inference,[],[20,21,385,379,19,17,30,9,10,12,13,34])).
% 58.59/58.67 cnf(390,plain,
% 58.59/58.67 (P3(f3(x3901),x3901,x3901)),
% 58.59/58.67 inference(rename_variables,[],[21])).
% 58.59/58.67 cnf(395,plain,
% 58.59/58.67 (~P3(f3(f3(a1)),a1,f3(a4))),
% 58.59/58.67 inference(scs_inference,[],[205,20,21,385,390,379,19,17,30,9,10,12,13,34,32,33])).
% 58.59/58.67 cnf(402,plain,
% 58.59/58.67 (P1(f5(a1,f2(a1)))),
% 58.59/58.67 inference(scs_inference,[],[14,22,205,20,21,385,390,379,19,17,30,9,10,12,13,34,32,33,2,72,109,3,8])).
% 58.59/58.67 cnf(411,plain,
% 58.59/58.67 (E(x4111,f5(x4111,f2(x4111)))),
% 58.59/58.67 inference(rename_variables,[],[380])).
% 58.59/58.67 cnf(413,plain,
% 58.59/58.67 (E(x4131,f5(x4131,f2(x4131)))),
% 58.59/58.67 inference(rename_variables,[],[380])).
% 58.59/58.67 cnf(414,plain,
% 58.59/58.67 (P2(f3(x4141),f5(x4141,f2(x4141)))),
% 58.59/58.67 inference(scs_inference,[],[380,411,413,98,163,57])).
% 58.59/58.67 cnf(419,plain,
% 58.59/58.67 (P3(f5(x4191,f2(x4191)),f2(x4191),x4191)),
% 58.59/58.67 inference(rename_variables,[],[383])).
% 58.59/58.67 cnf(425,plain,
% 58.59/58.67 (P3(x4251,f2(f2(x4251)),x4251)),
% 58.59/58.67 inference(scs_inference,[],[22,20,380,411,413,21,383,419,384,395,98,163,57,109,72,2,30,34,33])).
% 58.59/58.67 cnf(459,plain,
% 58.59/58.67 (P3(x4591,f2(a4),f5(x4591,f2(a4)))+~P3(a1,a4,x4591)),
% 58.59/58.67 inference(scs_inference,[],[101,27])).
% 58.59/58.67 cnf(466,plain,
% 58.59/58.67 (P2(f3(x4661),x4661)),
% 58.59/58.67 inference(rename_variables,[],[19])).
% 58.59/58.67 cnf(473,plain,
% 58.59/58.67 (P3(f3(x4731),x4731,x4731)),
% 58.59/58.67 inference(rename_variables,[],[21])).
% 58.59/58.67 cnf(479,plain,
% 58.59/58.67 (~P3(f3(a1),f3(a1),f3(a4))),
% 58.59/58.67 inference(scs_inference,[],[21,473,20,19,466,384,414,28,29,32,31,243,256])).
% 58.59/58.67 cnf(484,plain,
% 58.59/58.67 (P2(a1,f3(a4))),
% 58.59/58.67 inference(scs_inference,[],[21,17,28])).
% 58.59/58.67 cnf(485,plain,
% 58.59/58.67 (P3(f3(x4851),x4851,x4851)),
% 58.59/58.67 inference(rename_variables,[],[21])).
% 58.59/58.67 cnf(487,plain,
% 58.59/58.67 (P2(f5(a1,f2(a1)),f3(a4))),
% 58.59/58.67 inference(scs_inference,[],[21,380,17,28,12])).
% 58.59/58.67 cnf(490,plain,
% 58.59/58.67 (~P3(a1,a4,x4901)+P2(f3(a1),x4901)),
% 58.59/58.67 inference(scs_inference,[],[21,485,380,17,28,12,361,32])).
% 58.59/58.67 cnf(585,plain,
% 58.59/58.67 (P3(f3(a1),x5851,f5(f3(a1),x5851))+~P3(a1,a4,x5851)),
% 58.59/58.67 inference(scs_inference,[],[490,27])).
% 58.59/58.67 cnf(843,plain,
% 58.59/58.67 (~P3(f5(a1,f2(a1)),f3(a4),x8431)+P2(f3(a1),x8431)),
% 58.59/58.67 inference(scs_inference,[],[384,484,32])).
% 58.59/58.67 cnf(895,plain,
% 58.59/58.67 (~P3(a1,a4,x8951)+P2(f3(f3(a1)),x8951)),
% 58.59/58.67 inference(scs_inference,[],[389,17,32])).
% 58.59/58.67 cnf(900,plain,
% 58.59/58.67 (P3(f3(f3(a1)),x9001,x9001)+~P3(a1,a4,x9001)),
% 58.59/58.67 inference(scs_inference,[],[16,895,24])).
% 58.59/58.67 cnf(935,plain,
% 58.59/58.67 (~P3(f2(f2(a1)),a4,x9351)+P2(a1,x9351)),
% 58.59/58.67 inference(scs_inference,[],[425,17,32])).
% 58.59/58.67 cnf(945,plain,
% 58.59/58.67 (P3(a1,x9451,f5(a1,x9451))+~P3(f2(f2(a1)),a4,x9451)),
% 58.59/58.67 inference(scs_inference,[],[935,27])).
% 58.59/58.67 cnf(966,plain,
% 58.59/58.67 (~P3(a1,a4,x9661)+P2(x9661,f2(f2(a4)))),
% 58.59/58.67 inference(scs_inference,[],[425,17,31])).
% 58.59/58.67 cnf(1083,plain,
% 58.59/58.67 (P2(f3(a1),f3(a4))),
% 58.59/58.67 inference(scs_inference,[],[487,402,843,24])).
% 58.59/58.67 cnf(1116,plain,
% 58.59/58.67 (P3(a1,a4,f5(a1,a4))),
% 58.59/58.67 inference(scs_inference,[],[94,15,945,24])).
% 58.59/58.67 cnf(1121,plain,
% 58.59/58.67 (P2(f5(a1,a4),f2(a4))),
% 58.59/58.67 inference(scs_inference,[],[1116,459,585,101])).
% 58.59/58.67 cnf(1123,plain,
% 58.59/58.67 (P2(f3(a1),f5(a1,a4))),
% 58.59/58.67 inference(scs_inference,[],[1116,459,585,101,490])).
% 58.59/58.67 cnf(1132,plain,
% 58.59/58.67 (E(x11321,f5(x11321,f2(x11321)))),
% 58.59/58.67 inference(rename_variables,[],[380])).
% 58.59/58.67 cnf(1138,plain,
% 58.59/58.67 (P3(f3(a1),f5(a1,a4),f5(a1,a4))),
% 58.59/58.67 inference(scs_inference,[],[380,1132,20,21,1116,459,585,101,490,895,900,966,9,10,29,34])).
% 58.59/58.67 cnf(1744,plain,
% 58.59/58.67 (P3(f3(x17441),x17441,x17441)),
% 58.59/58.67 inference(rename_variables,[],[21])).
% 58.59/58.67 cnf(1746,plain,
% 58.59/58.67 (~P3(x17461,f3(x17462),f3(x17462))+P3(x17461,x17462,x17462)),
% 58.59/58.67 inference(scs_inference,[],[21,1744,1083,28,34])).
% 58.59/58.67 cnf(3942,plain,
% 58.59/58.67 (P3(f3(a1),a1,f3(a1))),
% 58.59/58.67 inference(scs_inference,[],[14,19,25])).
% 58.59/58.67 cnf(3945,plain,
% 58.59/58.67 (P3(a1,f3(a4),f3(a4))),
% 58.59/58.67 inference(scs_inference,[],[14,484,19,25,24])).
% 58.59/58.67 cnf(3947,plain,
% 58.59/58.67 (~P3(a1,f3(a4),f3(a1))),
% 58.59/58.67 inference(scs_inference,[],[479,14,484,19,21,25,24,34])).
% 58.59/58.67 cnf(3957,plain,
% 58.59/58.67 (~E(f3(a4),f2(a1))),
% 58.59/58.67 inference(scs_inference,[],[22,1121,479,1123,14,484,19,21,25,24,34,1746,30,23,55,2])).
% 58.59/58.67 cnf(3970,plain,
% 58.59/58.67 (P2(a1,f5(a1,a4))),
% 58.59/58.67 inference(scs_inference,[],[3957,3942,3945,1123,30,29])).
% 58.59/58.67 cnf(3972,plain,
% 58.59/58.67 (P3(f3(a1),f3(a4),f3(a1))),
% 58.59/58.67 inference(scs_inference,[],[3957,3942,3945,1123,1083,16,30,29,25])).
% 58.59/58.67 cnf(3980,plain,
% 58.59/58.67 (P2(f3(a1),f2(a1))),
% 58.59/58.67 inference(scs_inference,[],[3957,3942,3945,1123,1083,1138,14,18,205,16,19,1116,20,30,29,25,33,34,23])).
% 58.59/58.67 cnf(3992,plain,
% 58.59/58.67 ($false),
% 58.59/58.67 inference(scs_inference,[],[3970,3980,3947,3972,3945,14,15,21,25,24,33]),
% 58.59/58.67 ['proof']).
% 58.59/58.67 % SZS output end Proof
% 58.59/58.67 % Total time :58.040000s
%------------------------------------------------------------------------------