%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT005-4 : 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 : n032.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 2.13s 2.26s
% Output : CNFRefutation 2.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : CAT005-4 : TPTP v8.2.0. Released v1.0.0.
% 0.10/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n032.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:14:38 EDT 2024
% 0.12/0.32 % CPUTime :
% 0.18/0.50 start to proof:theBenchmark
% 2.13/2.25 %-------------------------------------------
% 2.13/2.25 % File :CSE---1.7
% 2.13/2.25 % Problem :theBenchmark
% 2.13/2.25 % Transform :cnf
% 2.13/2.25 % Format :tptp:raw
% 2.13/2.25 % Command :java -jar mcs_scs.jar %d %s
% 2.13/2.25
% 2.13/2.26 % Result :Theorem 1.730000s
% 2.13/2.26 % Output :CNFRefutation 1.730000s
% 2.13/2.26 %-------------------------------------------
% 2.13/2.26 %--------------------------------------------------------------------------
% 2.13/2.26 % File : CAT005-4 : TPTP v8.2.0. Released v1.0.0.
% 2.13/2.26 % Domain : Category Theory
% 2.13/2.26 % Problem : Domain is the unique right identity
% 2.13/2.26 % Version : [Sco79] axioms : Reduced > Complete.
% 2.13/2.26 % English : domain(x) is the unique identity i such that xi is defined.
% 2.13/2.26
% 2.13/2.26 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 2.13/2.26 % Source : [TPTP]
% 2.13/2.26 % Names :
% 2.13/2.26
% 2.13/2.26 % Status : Unsatisfiable
% 2.13/2.26 % Rating : 0.00 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.3.0, 0.14 v3.1.0, 0.22 v2.7.0, 0.17 v2.6.0, 0.43 v2.5.0, 0.20 v2.4.0, 0.17 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 2.13/2.26 % Syntax : Number of clauses : 15 ( 5 unt; 0 nHn; 12 RR)
% 2.13/2.26 % Number of literals : 27 ( 10 equ; 13 neg)
% 2.13/2.26 % Maximal clause size : 3 ( 1 avg)
% 2.13/2.26 % Maximal term depth : 3 ( 1 avg)
% 2.13/2.26 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 2.13/2.26 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 2.13/2.26 % Number of variables : 21 ( 2 sgn)
% 2.13/2.26 % SPC : CNF_UNS_RFO_SEQ_HRN
% 2.13/2.26
% 2.13/2.26 % Comments : The dependent axioms have been removed.
% 2.13/2.26 %--------------------------------------------------------------------------
% 2.13/2.26 %----Include Scott's axioms for category theory
% 2.13/2.26 include('Axioms/CAT004-0.ax').
% 2.13/2.26 %--------------------------------------------------------------------------
% 2.13/2.26 %----Denial of the theorem: d is an identity not equal to dom(a),
% 2.13/2.26 cnf(ad_exists,hypothesis,
% 2.13/2.26 there_exists(compose(a,d)) ).
% 2.13/2.26
% 2.13/2.26 cnf(xd_equals_x,hypothesis,
% 2.13/2.26 ( ~ there_exists(compose(X,d))
% 2.13/2.26 | compose(X,d) = X ) ).
% 2.13/2.26
% 2.13/2.26 cnf(dy_equals_y,hypothesis,
% 2.13/2.26 ( ~ there_exists(compose(d,Y))
% 2.13/2.26 | compose(d,Y) = Y ) ).
% 2.13/2.26
% 2.13/2.26 cnf(prove_domain_of_a_is_d,negated_conjecture,
% 2.13/2.26 domain(a) != d ).
% 2.13/2.26
% 2.13/2.26 %--------------------------------------------------------------------------
% 2.13/2.26 %-------------------------------------------
% 2.13/2.26 % Proof found
% 2.13/2.26 % SZS status Theorem for theBenchmark
% 2.13/2.26 % SZS output start Proof
% 2.13/2.26 %ClaNum:25(EqnAxiom:10)
% 2.13/2.26 %VarNum:46(SingletonVarNum:21)
% 2.13/2.26 %MaxLitNum:3
% 2.13/2.26 %MaxfuncDepth:2
% 2.13/2.26 %SharedTerms:6
% 2.13/2.26 %goalClause: 15
% 2.13/2.26 %singleGoalClaCount:1
% 2.13/2.26 [13]P1(f2(a4,a5))
% 2.13/2.26 [15]~E(f1(a4),a5)
% 2.13/2.26 [11]E(f2(x111,f1(x111)),x111)
% 2.13/2.26 [12]E(f2(f3(x121),x121),x121)
% 2.13/2.26 [14]E(f2(f2(x141,x142),x143),f2(x141,f2(x142,x143)))
% 2.13/2.26 [16]P1(x161)+~P1(f1(x161))
% 2.13/2.26 [17]P1(x171)+~P1(f3(x171))
% 2.13/2.26 [22]E(f2(x221,a5),x221)+~P1(f2(x221,a5))
% 2.13/2.26 [23]E(f2(a5,x231),x231)+~P1(f2(a5,x231))
% 2.13/2.26 [18]~P2(x181,x182)+E(x181,x182)
% 2.13/2.26 [20]P1(x201)+~P2(x201,x202)
% 2.13/2.26 [21]E(f3(x211),f1(x212))+~P1(f2(x212,x211))
% 2.13/2.26 [24]P1(f1(x241))+~P1(f2(x241,x242))
% 2.13/2.26 [19]~E(x191,x192)+~P1(x191)+P2(x191,x192)
% 2.13/2.26 [25]~E(f3(x252),f1(x251))+~P1(f1(x251))+P1(f2(x251,x252))
% 2.13/2.26 %EqnAxiom
% 2.13/2.26 [1]E(x11,x11)
% 2.13/2.26 [2]E(x22,x21)+~E(x21,x22)
% 2.13/2.26 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 2.13/2.26 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 2.13/2.26 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53))
% 2.13/2.26 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62))
% 2.13/2.26 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 2.13/2.26 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 2.13/2.26 [9]P2(x92,x93)+~E(x91,x92)+~P2(x91,x93)
% 2.13/2.26 [10]P2(x103,x102)+~E(x101,x102)+~P2(x103,x101)
% 2.13/2.26
% 2.13/2.26 %-------------------------------------------
% 2.13/2.27 cnf(26,plain,
% 2.13/2.27 (~P1(x261)+P2(x261,x261)),
% 2.13/2.27 inference(equality_inference,[],[19])).
% 2.13/2.27 cnf(29,plain,
% 2.13/2.27 (E(x291,f2(x291,f1(x291)))),
% 2.13/2.27 inference(scs_inference,[],[15,11,18,2])).
% 2.13/2.27 cnf(30,plain,
% 2.13/2.27 (E(f3(a5),f1(a4))),
% 2.13/2.27 inference(scs_inference,[],[15,11,13,18,2,21])).
% 2.13/2.27 cnf(32,plain,
% 2.13/2.27 (E(f2(a4,a5),a4)),
% 2.13/2.27 inference(scs_inference,[],[15,11,13,18,2,21,22])).
% 2.13/2.27 cnf(34,plain,
% 2.13/2.27 (P2(f2(a4,a5),f2(f2(a4,a5),f1(f2(a4,a5))))),
% 2.13/2.27 inference(scs_inference,[],[15,11,13,18,2,21,22,19])).
% 2.13/2.27 cnf(36,plain,
% 2.13/2.27 (~E(f1(a4),f2(f3(a5),a5))),
% 2.13/2.27 inference(scs_inference,[],[15,11,12,13,18,2,21,22,19,3])).
% 2.13/2.27 cnf(38,plain,
% 2.13/2.27 (P1(f2(f2(a4,a5),f1(f2(a4,a5))))),
% 2.13/2.27 inference(scs_inference,[],[15,11,12,13,18,2,21,22,19,3,8])).
% 2.13/2.27 cnf(42,plain,
% 2.13/2.27 (~P2(f1(a4),f2(f3(a5),a5))),
% 2.13/2.27 inference(scs_inference,[],[36,18])).
% 2.13/2.27 cnf(44,plain,
% 2.13/2.27 (E(f1(a4),f3(a5))),
% 2.13/2.27 inference(scs_inference,[],[36,30,18,2])).
% 2.13/2.27 cnf(45,plain,
% 2.13/2.27 (P1(a4)),
% 2.13/2.27 inference(scs_inference,[],[36,30,32,13,18,2,8])).
% 2.13/2.27 cnf(46,plain,
% 2.13/2.27 (E(f3(a5),f2(f1(a4),f1(f1(a4))))),
% 2.13/2.27 inference(scs_inference,[],[29,36,30,32,13,18,2,8,3])).
% 2.13/2.27 cnf(47,plain,
% 2.13/2.27 (E(x471,f2(x471,f1(x471)))),
% 2.13/2.27 inference(rename_variables,[],[29])).
% 2.13/2.27 cnf(48,plain,
% 2.13/2.27 (P2(a4,f2(a4,f1(a4)))),
% 2.13/2.27 inference(scs_inference,[],[29,47,36,30,32,13,18,2,8,3,19])).
% 2.13/2.27 cnf(53,plain,
% 2.13/2.27 (E(f2(f1(a4),f1(f1(a4))),f3(a5))),
% 2.13/2.27 inference(scs_inference,[],[46,2])).
% 2.13/2.27 cnf(54,plain,
% 2.13/2.27 (E(f2(f3(f1(a4)),f1(a4)),f3(a5))),
% 2.13/2.27 inference(scs_inference,[],[46,44,12,2,3])).
% 2.13/2.27 cnf(57,plain,
% 2.13/2.27 (~P2(f3(a5),x571)+P1(f2(f1(a4),f1(f1(a4))))),
% 2.13/2.27 inference(scs_inference,[],[46,44,12,2,3,8,20])).
% 2.13/2.27 cnf(60,plain,
% 2.13/2.27 (E(f3(a5),f2(f3(f1(a4)),f1(a4)))),
% 2.13/2.27 inference(scs_inference,[],[54,2])).
% 2.13/2.27 cnf(61,plain,
% 2.13/2.27 (E(f2(f2(a4,a5),f1(f2(a4,a5))),a4)),
% 2.13/2.27 inference(scs_inference,[],[54,32,11,2,3])).
% 2.13/2.27 cnf(63,plain,
% 2.13/2.27 (~P1(f2(f1(a4),f1(f1(a4))))+P1(f3(a5))),
% 2.13/2.27 inference(scs_inference,[],[53,54,32,11,2,3,8])).
% 2.13/2.27 cnf(71,plain,
% 2.13/2.27 (E(a4,f2(f2(a4,a5),f1(f2(a4,a5))))),
% 2.13/2.27 inference(scs_inference,[],[61,2])).
% 2.13/2.27 cnf(74,plain,
% 2.13/2.27 (P2(f2(a4,a5),a4)),
% 2.13/2.27 inference(scs_inference,[],[61,34,38,2,19,10])).
% 2.13/2.27 cnf(75,plain,
% 2.13/2.27 (E(f1(a4),f2(f3(f1(a4)),f1(a4)))),
% 2.13/2.27 inference(scs_inference,[],[60,61,44,34,38,2,19,10,3])).
% 2.13/2.27 cnf(92,plain,
% 2.13/2.27 (E(f2(f3(f2(a4,a5)),f2(a4,a5)),a4)),
% 2.13/2.27 inference(scs_inference,[],[71,45,14,32,12,2,19,3])).
% 2.13/2.27 cnf(96,plain,
% 2.13/2.27 (~P2(f1(a4),x961)+P1(f2(f3(f1(a4)),f1(a4)))),
% 2.13/2.27 inference(scs_inference,[],[75,71,13,45,14,32,12,2,19,3,8,24,20])).
% 2.13/2.27 cnf(99,plain,
% 2.13/2.27 (E(a4,f2(f3(f2(a4,a5)),f2(a4,a5)))),
% 2.13/2.27 inference(scs_inference,[],[92,2])).
% 2.13/2.27 cnf(103,plain,
% 2.13/2.27 (~E(f1(a4),f2(a5,f1(a5)))),
% 2.13/2.27 inference(scs_inference,[],[15,92,29,74,45,11,2,10,8,3])).
% 2.13/2.27 cnf(109,plain,
% 2.13/2.27 (E(a4,f2(a4,a5))),
% 2.13/2.27 inference(scs_inference,[],[32,2])).
% 2.13/2.27 cnf(110,plain,
% 2.13/2.27 (P2(a4,f2(f3(f2(a4,a5)),f2(a4,a5)))),
% 2.13/2.27 inference(scs_inference,[],[99,45,32,2,19])).
% 2.13/2.27 cnf(113,plain,
% 2.13/2.27 (P2(f2(f3(f2(a4,a5)),f2(a4,a5)),f2(a4,f1(a4)))),
% 2.13/2.27 inference(scs_inference,[],[99,48,74,45,32,2,19,10,9])).
% 2.13/2.27 cnf(118,plain,
% 2.13/2.27 (E(x1181,f2(f3(x1181),x1181))),
% 2.13/2.27 inference(scs_inference,[],[12,2])).
% 2.13/2.27 cnf(123,plain,
% 2.13/2.27 (~P2(f1(a4),x1231)+P1(f3(a5))),
% 2.13/2.27 inference(scs_inference,[],[29,44,110,13,12,2,9,8,24,20])).
% 2.13/2.27 cnf(125,plain,
% 2.13/2.27 (~P1(f3(a5))+P1(f1(a4))),
% 2.13/2.27 inference(scs_inference,[],[30,8])).
% 2.13/2.27 cnf(143,plain,
% 2.13/2.27 (E(f2(x1431,f1(x1431)),x1431)),
% 2.13/2.27 inference(rename_variables,[],[11])).
% 2.13/2.27 cnf(150,plain,
% 2.13/2.27 (E(f3(f1(a4)),f1(a4))),
% 2.13/2.27 inference(scs_inference,[],[11,143,29,109,48,13,10,3,9,2,8,21])).
% 2.13/2.27 cnf(152,plain,
% 2.13/2.27 (P2(f1(a4),f1(a4))),
% 2.13/2.27 inference(scs_inference,[],[13,26,24])).
% 2.13/2.27 cnf(153,plain,
% 2.13/2.27 (P1(f2(f3(f1(a4)),f1(a4)))),
% 2.13/2.27 inference(scs_inference,[],[152,96])).
% 2.13/2.27 cnf(154,plain,
% 2.13/2.27 (P1(f3(a5))),
% 2.13/2.27 inference(scs_inference,[],[152,123])).
% 2.13/2.27 cnf(157,plain,
% 2.13/2.27 (E(f2(x1571,f1(x1571)),x1571)),
% 2.13/2.27 inference(rename_variables,[],[11])).
% 2.13/2.27 cnf(158,plain,
% 2.13/2.27 (E(f2(a4,f1(a4)),f2(f3(f2(a4,a5)),f2(a4,a5)))),
% 2.13/2.27 inference(scs_inference,[],[11,157,99,113,150,2,10,3])).
% 2.13/2.27 cnf(159,plain,
% 2.13/2.27 (E(f2(x1591,f1(x1591)),x1591)),
% 2.13/2.27 inference(rename_variables,[],[11])).
% 2.13/2.27 cnf(161,plain,
% 2.13/2.27 (P1(f2(f1(a4),f1(f1(a4))))),
% 2.13/2.27 inference(scs_inference,[],[11,157,44,99,152,113,150,2,10,3,9,57])).
% 2.13/2.27 cnf(163,plain,
% 2.13/2.27 (P2(f2(f1(a4),f1(f1(a4))),f1(a4))),
% 2.13/2.27 inference(scs_inference,[],[11,157,159,44,99,152,113,150,2,10,3,9,57,19])).
% 2.13/2.27 cnf(183,plain,
% 2.13/2.27 (P1(f3(a5))),
% 2.13/2.27 inference(scs_inference,[],[161,63])).
% 2.13/2.27 cnf(190,plain,
% 2.13/2.27 (P1(f1(a4))),
% 2.13/2.27 inference(scs_inference,[],[154,125])).
% 2.13/2.27 cnf(200,plain,
% 2.13/2.27 (P1(a5)),
% 2.13/2.27 inference(scs_inference,[],[154,17])).
% 2.13/2.27 cnf(205,plain,
% 2.13/2.27 (P2(f2(f1(a4),f1(f1(a4))),f3(a5))),
% 2.13/2.27 inference(scs_inference,[],[54,44,158,163,153,154,17,2,19,10])).
% 2.13/2.27 cnf(206,plain,
% 2.13/2.27 (E(f2(f3(a5),f1(f3(a5))),f1(a4))),
% 2.13/2.27 inference(scs_inference,[],[11,54,44,158,163,30,153,154,17,2,19,10,3])).
% 2.13/2.27 cnf(216,plain,
% 2.13/2.27 (P2(f1(a4),f3(a5))),
% 2.13/2.27 inference(scs_inference,[],[11,46,206,205,183,190,2,19,8,9])).
% 2.13/2.27 cnf(230,plain,
% 2.13/2.27 (~E(f3(a5),f2(f3(a5),a5))),
% 2.13/2.27 inference(scs_inference,[],[42,29,216,200,19,10])).
% 2.13/2.27 cnf(419,plain,
% 2.13/2.27 (E(x4191,f2(x4191,f1(x4191)))),
% 2.13/2.27 inference(rename_variables,[],[29])).
% 2.13/2.27 cnf(422,plain,
% 2.13/2.27 (E(f3(f1(a5)),f1(a5))),
% 2.13/2.27 inference(scs_inference,[],[200,29,8,23,21])).
% 2.13/2.27 cnf(424,plain,
% 2.13/2.27 (E(f1(a5),f2(a5,f1(a5)))),
% 2.13/2.27 inference(scs_inference,[],[200,29,8,23,21,2])).
% 2.13/2.27 cnf(425,plain,
% 2.13/2.27 (E(a5,f1(a5))),
% 2.13/2.27 inference(scs_inference,[],[200,29,419,8,23,21,2,3])).
% 2.13/2.27 cnf(431,plain,
% 2.13/2.27 (~E(f1(a4),f1(a5))),
% 2.13/2.27 inference(scs_inference,[],[200,103,118,424,425,2,8,3])).
% 2.13/2.27 cnf(432,plain,
% 2.13/2.27 (~E(a4,a5)),
% 2.13/2.27 inference(scs_inference,[],[200,103,118,424,425,2,8,3,4])).
% 2.13/2.27 cnf(433,plain,
% 2.13/2.27 (E(f2(f3(a5),a5),f3(a5))),
% 2.13/2.27 inference(scs_inference,[],[200,103,118,424,425,2,8,3,4,22])).
% 2.13/2.27 cnf(445,plain,
% 2.13/2.27 (~E(f1(a4),f3(f1(a5)))),
% 2.13/2.27 inference(scs_inference,[],[200,431,425,110,422,432,18,2,8,10,3])).
% 2.13/2.27 cnf(452,plain,
% 2.13/2.27 ($false),
% 2.13/2.27 inference(scs_inference,[],[445,230,433,18,2]),
% 2.13/2.27 ['proof']).
% 2.13/2.27 % SZS output end Proof
% 2.13/2.27 % Total time :1.730000s
%------------------------------------------------------------------------------