%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CAT007-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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 : Thu May 9 17:16:58 EDT 2024
% Result : Unsatisfiable 1.15s 1.34s
% Output : Refutation 1.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 8
% Syntax : Number of clauses : 15 ( 9 unt; 0 nHn; 11 RR)
% Number of literals : 27 ( 7 equ; 13 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 17 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_ab_is_defined,negated_conjecture,
~ defined(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_ab_is_defined) ).
cnf(codomain_is_an_identity_map,axiom,
identity_map(codomain(X4)),
file('/export/starexec/sandbox/benchmark/Axioms/CAT001-0.ax',codomain_is_an_identity_map) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(domain_of_a_equals_codomain_of_b,plain,
domain(a) = codomain(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain_of_a_equals_codomain_of_b) ).
cnf(mapping_from_x_to_its_domain,axiom,
defined(X5,domain(X5)),
file('/export/starexec/sandbox/benchmark/Axioms/CAT001-0.ax',mapping_from_x_to_its_domain) ).
cnf(c3,axiom,
( X119 != X122
| X121 != X120
| ~ defined(X119,X121)
| defined(X122,X120) ),
theory(equality) ).
cnf(c180,plain,
( X404 != X406
| domain(X404) != X405
| defined(X406,X405) ),
inference(resolution,[status(thm)],[c3,mapping_from_x_to_its_domain]) ).
cnf(c1432,plain,
( a != X425
| defined(X425,codomain(b)) ),
inference(resolution,[status(thm)],[c180,domain_of_a_equals_codomain_of_b]) ).
cnf(c1531,plain,
defined(a,codomain(b)),
inference(resolution,[status(thm)],[c1432,reflexivity]) ).
cnf(mapping_from_codomain_of_x_to_x,axiom,
defined(codomain(X6),X6),
file('/export/starexec/sandbox/benchmark/Axioms/CAT001-0.ax',mapping_from_codomain_of_x_to_x) ).
cnf(category_theory_axiom6,axiom,
( ~ defined(X92,X91)
| ~ defined(X91,X93)
| ~ identity_map(X91)
| defined(X92,X93) ),
file('/export/starexec/sandbox/benchmark/Axioms/CAT001-0.ax',category_theory_axiom6) ).
cnf(c117,plain,
( ~ defined(X543,codomain(X544))
| ~ identity_map(codomain(X544))
| defined(X543,X544) ),
inference(resolution,[status(thm)],[category_theory_axiom6,mapping_from_codomain_of_x_to_x]) ).
cnf(c2442,plain,
( ~ identity_map(codomain(b))
| defined(a,b) ),
inference(resolution,[status(thm)],[c117,c1531]) ).
cnf(c2464,plain,
defined(a,b),
inference(resolution,[status(thm)],[c2442,codomain_is_an_identity_map]) ).
cnf(c2474,plain,
$false,
inference(resolution,[status(thm)],[c2464,prove_ab_is_defined]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CAT007-1 : TPTP v8.1.2. Released v1.0.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n023.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 : Wed May 8 21:05:23 EDT 2024
% 0.12/0.33 % CPUTime :
% 1.15/1.34 % Version: 1.5
% 1.15/1.34 % SZS status Unsatisfiable
% 1.15/1.34 % SZS output start CNFRefutation
% See solution above
% 1.15/1.34
% 1.15/1.34 % Initial clauses : 29
% 1.15/1.34 % Processed clauses : 269
% 1.15/1.34 % Factors computed : 14
% 1.15/1.34 % Resolvents computed: 2457
% 1.15/1.34 % Tautologies deleted: 34
% 1.15/1.34 % Forward subsumed : 120
% 1.15/1.34 % Backward subsumed : 13
% 1.15/1.34 % -------- CPU Time ---------
% 1.15/1.34 % User time : 0.988 s
% 1.15/1.34 % System time : 0.015 s
% 1.15/1.34 % Total time : 1.003 s
%------------------------------------------------------------------------------