%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT019-3 : 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:18 EDT 2024
% Result : Unsatisfiable 0.52s 0.66s
% Output : CNFRefutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CAT019-3 : 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.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jun 18 12:25:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.51/0.56 start to proof:theBenchmark
% 0.52/0.65 %-------------------------------------------
% 0.52/0.65 % File :CSE---1.7
% 0.52/0.65 % Problem :theBenchmark
% 0.52/0.65 % Transform :cnf
% 0.52/0.65 % Format :tptp:raw
% 0.52/0.65 % Command :java -jar mcs_scs.jar %d %s
% 0.52/0.65
% 0.52/0.65 % Result :Theorem 0.050000s
% 0.52/0.65 % Output :CNFRefutation 0.050000s
% 0.52/0.65 %-------------------------------------------
% 0.52/0.66 %--------------------------------------------------------------------------
% 0.52/0.66 % File : CAT019-3 : TPTP v8.2.0. Released v1.0.0.
% 0.52/0.66 % Domain : Category Theory
% 0.52/0.66 % Problem : Axiom of Indiscernibles
% 0.52/0.66 % Version : [Sco79] axioms : Reduced > Complete.
% 0.52/0.66 % English : [all z (x=z <-> y=z)] -> x=y.
% 0.52/0.66
% 0.52/0.66 % Refs : [Sco79] Scott (1979), Identity and Existence in Intuitionist L
% 0.52/0.66 % Source : [ANL]
% 0.52/0.66 % Names : p15.ver3.no2.in [ANL]
% 0.52/0.66 % : p15.ver3.no4.in [ANL]
% 0.52/0.66
% 0.52/0.66 % Status : Unsatisfiable
% 0.52/0.66 % Rating : 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.20 v6.4.0, 0.13 v6.3.0, 0.18 v6.2.0, 0.20 v6.1.0, 0.21 v6.0.0, 0.20 v5.3.0, 0.22 v5.2.0, 0.25 v5.1.0, 0.12 v5.0.0, 0.00 v4.0.1, 0.09 v4.0.0, 0.00 v2.5.0, 0.08 v2.4.0, 0.00 v2.1.0, 0.00 v2.0.0
% 0.52/0.66 % Syntax : Number of clauses : 20 ( 4 unt; 2 nHn; 15 RR)
% 0.52/0.66 % Number of literals : 44 ( 20 equ; 22 neg)
% 0.52/0.66 % Maximal clause size : 4 ( 2 avg)
% 0.52/0.66 % Maximal term depth : 3 ( 1 avg)
% 0.52/0.66 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty)
% 0.52/0.66 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% 0.52/0.66 % Number of variables : 33 ( 4 sgn)
% 0.52/0.66 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.52/0.66
% 0.52/0.66 % Comments : The ANL set uses very few axioms for this. I'm not sure
% 0.52/0.66 % if using them all is OK.
% 0.52/0.66 % : Axioms simplified by Art Quaife.
% 0.52/0.66 %--------------------------------------------------------------------------
% 0.52/0.66 %----Include Scott's axioms for category theory
% 0.52/0.66 include('Axioms/CAT003-0.ax').
% 0.52/0.66 %--------------------------------------------------------------------------
% 0.52/0.66 %----Denial of the axiom of indiscernibles
% 0.52/0.66 cnf(equality_of_a_and_b1,hypothesis,
% 0.52/0.66 ( ~ there_exists(Z)
% 0.52/0.66 | a != Z
% 0.52/0.66 | b = Z ) ).
% 0.52/0.66
% 0.52/0.66 cnf(equality_of_a_and_b2,hypothesis,
% 0.52/0.66 ( ~ there_exists(Z)
% 0.52/0.66 | a = Z
% 0.52/0.66 | b != Z ) ).
% 0.52/0.66
% 0.52/0.66 cnf(prove_a_equals_b,negated_conjecture,
% 0.52/0.66 a != b ).
% 0.52/0.66
% 0.52/0.66 %--------------------------------------------------------------------------
% 0.52/0.66 %-------------------------------------------
% 0.52/0.66 % Proof found
% 0.52/0.66 % SZS status Theorem for theBenchmark
% 0.52/0.66 % SZS output start Proof
% 0.52/0.66 %ClaNum:31(EqnAxiom:12)
% 0.52/0.66 %VarNum:64(SingletonVarNum:29)
% 0.52/0.66 %MaxLitNum:3
% 0.52/0.66 %MaxfuncDepth:2
% 0.52/0.66 %SharedTerms:3
% 0.52/0.66 %goalClause: 16
% 0.52/0.66 %singleGoalClaCount:1
% 0.52/0.66 [16]~E(a4,a5)
% 0.52/0.66 [13]E(f2(x131,f1(x131)),x131)
% 0.52/0.66 [14]E(f2(f3(x141),x141),x141)
% 0.52/0.66 [15]E(f2(f2(x151,x152),x153),f2(x151,f2(x152,x153)))
% 0.52/0.66 [19]P1(x191)+~P1(f1(x191))
% 0.52/0.66 [20]P1(x201)+~P1(f3(x201))
% 0.52/0.66 [21]~P2(x211,x212)+E(x211,x212)
% 0.52/0.66 [23]P1(x231)+~P2(x232,x231)
% 0.52/0.66 [24]P1(x241)+~P2(x241,x242)
% 0.52/0.66 [26]E(x261,x262)+P1(f6(x261,x262))
% 0.52/0.66 [28]E(f3(x281),f1(x282))+~P1(f2(x282,x281))
% 0.52/0.66 [29]P1(f1(x291))+~P1(f2(x291,x292))
% 0.52/0.66 [30]P1(f3(x301))+~P1(f2(x301,x302))
% 0.52/0.66 [17]~P1(x171)+~E(a4,x171)+E(a5,x171)
% 0.52/0.66 [18]~P1(x181)+~E(a5,x181)+E(a4,x181)
% 0.52/0.66 [22]~E(x221,x222)+~P1(x221)+P2(x221,x222)
% 0.52/0.66 [27]E(x271,x272)+E(f6(x271,x272),x272)+E(f6(x271,x272),x271)
% 0.52/0.66 [31]~E(f3(x312),f1(x311))+~P1(f1(x311))+P1(f2(x311,x312))
% 0.52/0.66 %EqnAxiom
% 0.52/0.66 [1]E(x11,x11)
% 0.52/0.66 [2]E(x22,x21)+~E(x21,x22)
% 0.52/0.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.52/0.66 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 0.52/0.66 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53))
% 0.52/0.66 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62))
% 0.52/0.66 [7]~E(x71,x72)+E(f3(x71),f3(x72))
% 0.52/0.66 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 0.52/0.66 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 0.52/0.66 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 0.52/0.66 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 0.52/0.66 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 0.52/0.66
% 0.52/0.66 %-------------------------------------------
% 0.52/0.66 cnf(33,plain,
% 0.52/0.66 (~P1(a5)+E(a4,a5)),
% 0.52/0.66 inference(equality_inference,[],[18])).
% 0.52/0.66 cnf(34,plain,
% 0.52/0.66 (~P1(x341)+P2(x341,x341)),
% 0.52/0.66 inference(equality_inference,[],[22])).
% 0.52/0.66 cnf(35,plain,
% 0.52/0.66 (~P1(a5)),
% 0.52/0.66 inference(scs_inference,[],[16,33])).
% 0.52/0.66 cnf(38,plain,
% 0.52/0.66 (E(x381,f2(x381,f1(x381)))),
% 0.52/0.66 inference(scs_inference,[],[16,13,21,2])).
% 0.52/0.66 cnf(45,plain,
% 0.52/0.66 (~P2(x451,f2(a5,f1(a5)))),
% 0.52/0.66 inference(scs_inference,[],[16,13,21,2,3,18,31,23])).
% 0.52/0.66 cnf(47,plain,
% 0.52/0.66 (~P2(f2(a5,f1(a5)),x471)),
% 0.52/0.66 inference(scs_inference,[],[16,13,21,2,3,18,31,23,24])).
% 0.52/0.66 cnf(53,plain,
% 0.52/0.66 (~P2(x531,a5)),
% 0.52/0.66 inference(scs_inference,[],[35,23])).
% 0.52/0.66 cnf(62,plain,
% 0.52/0.66 (~P1(f2(a4,f1(a4)))+E(a5,f2(a4,f1(a4)))),
% 0.52/0.66 inference(scs_inference,[],[16,38,35,14,23,24,2,3,21,17])).
% 0.52/0.66 cnf(93,plain,
% 0.52/0.67 (P2(f6(a4,a5),f6(a4,a5))),
% 0.52/0.67 inference(scs_inference,[],[16,34,26])).
% 0.52/0.67 cnf(94,plain,
% 0.52/0.67 (~E(f6(a4,a5),f2(a5,f1(a5)))),
% 0.52/0.67 inference(scs_inference,[],[47,93,11])).
% 0.52/0.67 cnf(99,plain,
% 0.52/0.67 (E(f6(a4,a5),a4)),
% 0.52/0.67 inference(scs_inference,[],[16,38,94,3,27])).
% 0.52/0.67 cnf(101,plain,
% 0.52/0.67 (~P1(f6(a4,a5))+P1(a4)),
% 0.52/0.67 inference(scs_inference,[],[16,38,94,3,27,10])).
% 0.52/0.67 cnf(108,plain,
% 0.52/0.67 (P1(a4)),
% 0.52/0.67 inference(scs_inference,[],[93,101,24])).
% 0.52/0.67 cnf(110,plain,
% 0.52/0.67 (E(a4,f6(a4,a5))),
% 0.52/0.67 inference(scs_inference,[],[99,2])).
% 0.52/0.67 cnf(111,plain,
% 0.52/0.67 (P1(f2(a4,f1(a4)))),
% 0.52/0.67 inference(scs_inference,[],[38,99,108,2,10])).
% 0.52/0.67 cnf(113,plain,
% 0.52/0.67 (E(f2(f3(f6(a4,a5)),f6(a4,a5)),a4)),
% 0.52/0.67 inference(scs_inference,[],[38,99,14,108,2,10,3])).
% 0.52/0.67 cnf(117,plain,
% 0.52/0.67 (E(a5,f2(a4,f1(a4)))),
% 0.52/0.67 inference(scs_inference,[],[38,99,14,108,2,10,3,28,62])).
% 0.52/0.67 cnf(118,plain,
% 0.52/0.67 (~E(f2(a4,f1(a4)),f2(a5,f1(a5)))),
% 0.52/0.67 inference(scs_inference,[],[38,99,45,14,108,2,10,3,28,62,22])).
% 0.52/0.67 cnf(128,plain,
% 0.52/0.67 (E(f2(a5,f1(a5)),f2(a4,f1(a4)))),
% 0.52/0.67 inference(scs_inference,[],[110,113,53,13,111,117,108,2,22,10,3])).
% 0.52/0.67 cnf(132,plain,
% 0.52/0.67 ($false),
% 0.52/0.67 inference(scs_inference,[],[128,118,2]),
% 0.52/0.67 ['proof']).
% 0.52/0.67 % SZS output end Proof
% 0.52/0.67 % Total time :0.050000s
%------------------------------------------------------------------------------