%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : CAT007-3 : 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 : n021.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 0.54s 0.63s % Output : CNFRefutation 0.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : CAT007-3 : TPTP v8.2.0. Released v1.0.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.35 % Computer : n021.cluster.edu % 0.12/0.35 % Model : x86_64 x86_64 % 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.35 % Memory : 8042.1875MB % 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 300 % 0.12/0.35 % DateTime : Tue Jun 18 12:03:09 EDT 2024 % 0.12/0.35 % CPUTime : % 0.43/0.59 start to proof:theBenchmark % 0.43/0.62 %------------------------------------------- % 0.43/0.62 % File :CSE---1.7 % 0.43/0.62 % Problem :theBenchmark % 0.43/0.62 % Transform :cnf % 0.43/0.62 % Format :tptp:raw % 0.43/0.62 % Command :java -jar mcs_scs.jar %d %s % 0.43/0.62 % 0.43/0.62 % Result :Theorem 0.000000s % 0.43/0.62 % Output :CNFRefutation 0.000000s % 0.43/0.62 %------------------------------------------- % 0.54/0.63 %-------------------------------------------------------------------------- % 0.54/0.63 % File : CAT007-3 : TPTP v8.2.0. Released v1.0.0. % 0.54/0.63 % Domain : Category Theory % 0.54/0.63 % Problem : If domain(x) = codomain(y) then xy is defined % 0.54/0.63 % Version : [Sco79] axioms : Reduced > Complete. % 0.54/0.63 % English : % 0.54/0.63 % 0.54/0.63 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a % 0.54/0.63 % : [Sco79] Scott (1979), Identity and Existence in Intuitionist L % 0.54/0.63 % Source : [ANL] % 0.54/0.63 % Names : p7.ver3.in [ANL] % 0.54/0.63 % 0.54/0.63 % Status : Unsatisfiable % 0.54/0.63 % Rating : 0.00 v2.0.0 % 0.54/0.63 % Syntax : Number of clauses : 12 ( 5 unt; 2 nHn; 9 RR) % 0.54/0.63 % Number of literals : 23 ( 0 equ; 9 neg) % 0.54/0.63 % Maximal clause size : 3 ( 1 avg) % 0.54/0.63 % Maximal term depth : 2 ( 1 avg) % 0.54/0.63 % Number of predicates : 2 ( 2 usr; 0 prp; 1-2 aty) % 0.54/0.63 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty) % 0.54/0.63 % Number of variables : 15 ( 0 sgn) % 0.54/0.63 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.54/0.63 % 0.54/0.63 % Comments : In Scott's axiom system, this is an axiom; but % 0.54/0.63 % it is dependant, vis. proof included. % 0.54/0.63 % : Axioms simplified by Art Quaife. % 0.54/0.63 %-------------------------------------------------------------------------- % 0.54/0.63 cnf(reflexivity,axiom, % 0.54/0.63 equalish(X,X) ). % 0.54/0.63 % 0.54/0.63 cnf(symmetry,axiom, % 0.54/0.63 ( ~ equalish(X,Y) % 0.54/0.63 | equalish(Y,X) ) ). % 0.54/0.63 % 0.54/0.63 cnf(transitivity,axiom, % 0.54/0.63 ( ~ equalish(X,Y) % 0.54/0.63 | ~ equalish(Y,Z) % 0.54/0.63 | equalish(X,Z) ) ). % 0.54/0.63 % 0.54/0.63 %----Supply the axioms upon which it is dependant. % 0.54/0.63 % 0.54/0.63 %----Category theory axioms % 0.54/0.63 cnf(domain_has_elements,axiom, % 0.54/0.63 ( ~ there_exists(domain(X)) % 0.54/0.63 | there_exists(X) ) ). % 0.54/0.63 % 0.54/0.63 cnf(domain_codomain_composition2,axiom, % 0.54/0.63 ( ~ there_exists(domain(X)) % 0.54/0.63 | ~ equalish(domain(X),codomain(Y)) % 0.54/0.63 | there_exists(compose(X,Y)) ) ). % 0.54/0.63 % 0.54/0.63 %----Axiom of indiscernibles % 0.54/0.63 cnf(indiscernibles1,axiom, % 0.54/0.63 ( there_exists(f1(X,Y)) % 0.54/0.63 | equalish(X,Y) ) ). % 0.54/0.63 % 0.54/0.63 cnf(indiscernibles2,axiom, % 0.54/0.63 ( equalish(X,f1(X,Y)) % 0.54/0.63 | equalish(Y,f1(X,Y)) % 0.54/0.63 | equalish(X,Y) ) ). % 0.54/0.63 % 0.54/0.63 cnf(indiscernibles3,axiom, % 0.54/0.63 ( ~ equalish(X,f1(X,Y)) % 0.54/0.63 | ~ equalish(Y,f1(X,Y)) % 0.54/0.63 | equalish(X,Y) ) ). % 0.54/0.63 % 0.54/0.63 cnf(domain_of_c2_exists,hypothesis, % 0.54/0.63 there_exists(domain(c2)) ). % 0.54/0.63 % 0.54/0.63 cnf(domain_of_c1_exists,hypothesis, % 0.54/0.63 there_exists(domain(c1)) ). % 0.54/0.63 % 0.54/0.63 cnf(domain_of_c2_equals_codomain_of_c1,hypothesis, % 0.54/0.63 equalish(domain(c2),codomain(c1)) ). % 0.54/0.63 % 0.54/0.63 cnf(prove_c1_c2_is_defined,negated_conjecture, % 0.54/0.63 ~ there_exists(compose(c2,c1)) ). % 0.54/0.63 % 0.54/0.63 %-------------------------------------------------------------------------- % 0.54/0.63 %------------------------------------------- % 0.54/0.63 % Proof found % 0.54/0.63 % SZS status Theorem for theBenchmark % 0.54/0.63 % SZS output start Proof % 0.54/0.63 %ClaNum:12(EqnAxiom:0) % 0.54/0.63 %VarNum:39(SingletonVarNum:15) % 0.54/0.63 %MaxLitNum:3 % 0.54/0.63 %MaxfuncDepth:1 % 0.54/0.63 %SharedTerms:10 % 0.54/0.63 %goalClause: 5 % 0.54/0.63 %singleGoalClaCount:1 % 0.54/0.63 [1]P1(f3(a1)) % 0.54/0.63 [2]P1(f3(a2)) % 0.54/0.63 [4]P2(f3(a1),f4(a2)) % 0.54/0.63 [5]~P1(f5(a1,a2)) % 0.54/0.63 [3]P2(x31,x31) % 0.54/0.63 [6]P1(x61)+~P1(f3(x61)) % 0.54/0.63 [7]~P2(x72,x71)+P2(x71,x72) % 0.54/0.63 [8]P2(x81,x82)+P1(f6(x81,x82)) % 0.54/0.63 [10]~P2(f3(x101),f4(x102))+~P1(f3(x101))+P1(f5(x101,x102)) % 0.54/0.63 [11]P2(x111,x112)+P2(x112,f6(x111,x112))+P2(x111,f6(x111,x112)) % 0.54/0.63 [12]P2(x121,x122)+~P2(x122,f6(x121,x122))+~P2(x121,f6(x121,x122)) % 0.54/0.63 [9]~P2(x91,x93)+P2(x91,x92)+~P2(x93,x92) % 0.54/0.63 %EqnAxiom % 0.54/0.63 % 0.54/0.63 %------------------------------------------- % 0.54/0.63 cnf(13,plain, % 0.54/0.63 ($false), % 0.54/0.63 inference(scs_inference,[],[4,1,5,10]), % 0.54/0.63 ['proof']). % 0.54/0.63 % SZS output end Proof % 0.54/0.63 % Total time :0.000000s %------------------------------------------------------------------------------