%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CAT014-4 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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:17:02 EDT 2024
% Result : Unsatisfiable 1.35s 1.51s
% Output : Refutation 1.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 13
% Syntax : Number of clauses : 34 ( 20 unt; 0 nHn; 25 RR)
% Number of literals : 51 ( 31 equ; 18 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-2 aty)
% Number of variables : 40 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_codomain_is_idempotent,negated_conjecture,
codomain(codomain(a)) != codomain(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_codomain_is_idempotent) ).
cnf(transitivity,axiom,
( X36 != X38
| X38 != X37
| X36 = X37 ),
theory(equality) ).
cnf(domain_codomain_composition1,axiom,
( ~ there_exists(compose(X19,X20))
| domain(X19) = codomain(X20) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',domain_codomain_composition1) ).
cnf(assume_codomain_exists,plain,
there_exists(codomain(a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assume_codomain_exists) ).
cnf(codomain_has_elements,axiom,
( ~ there_exists(codomain(X11))
| there_exists(X11) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',codomain_has_elements) ).
cnf(c7,plain,
there_exists(a),
inference(resolution,[status(thm)],[codomain_has_elements,assume_codomain_exists]) ).
cnf(symmetry,axiom,
( X14 != X15
| X15 = X14 ),
theory(equality) ).
cnf(compose_codomain,axiom,
compose(codomain(X18),X18) = X18,
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',compose_codomain) ).
cnf(c14,plain,
X22 = compose(codomain(X22),X22),
inference(resolution,[status(thm)],[compose_codomain,symmetry]) ).
cnf(c4,axiom,
( X26 != X25
| ~ there_exists(X26)
| there_exists(X25) ),
theory(equality) ).
cnf(c23,plain,
( ~ there_exists(X35)
| there_exists(compose(codomain(X35),X35)) ),
inference(resolution,[status(thm)],[c4,c14]) ).
cnf(c43,plain,
there_exists(compose(codomain(a),a)),
inference(resolution,[status(thm)],[c23,c7]) ).
cnf(c47,plain,
domain(codomain(a)) = codomain(a),
inference(resolution,[status(thm)],[c43,domain_codomain_composition1]) ).
cnf(c105,plain,
( X218 != domain(codomain(a))
| X218 = codomain(a) ),
inference(resolution,[status(thm)],[c47,transitivity]) ).
cnf(domain_has_elements,axiom,
( ~ there_exists(domain(X7))
| there_exists(X7) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',domain_has_elements) ).
cnf(composition_implies_domain,axiom,
( ~ there_exists(compose(X12,X13))
| there_exists(domain(X12)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',composition_implies_domain) ).
cnf(associativity_of_compose,axiom,
compose(X31,compose(X33,X32)) = compose(compose(X31,X33),X32),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',associativity_of_compose) ).
cnf(c55,plain,
( X114 != compose(X113,compose(X112,X115))
| X114 = compose(compose(X113,X112),X115) ),
inference(resolution,[status(thm)],[transitivity,associativity_of_compose]) ).
cnf(c53,plain,
( X61 != compose(codomain(X62),X62)
| X61 = X62 ),
inference(resolution,[status(thm)],[transitivity,compose_codomain]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c2,axiom,
( X52 != X50
| X53 != X51
| compose(X52,X53) = compose(X50,X51) ),
theory(equality) ).
cnf(c83,plain,
( X134 != X136
| compose(X134,compose(codomain(X135),X135)) = compose(X136,X135) ),
inference(resolution,[status(thm)],[c2,compose_codomain]) ).
cnf(c595,plain,
compose(X166,compose(codomain(X167),X167)) = compose(X166,X167),
inference(resolution,[status(thm)],[c83,reflexivity]) ).
cnf(c843,plain,
compose(codomain(X168),compose(codomain(X168),X168)) = X168,
inference(resolution,[status(thm)],[c595,c53]) ).
cnf(c860,plain,
X172 = compose(codomain(X172),compose(codomain(X172),X172)),
inference(resolution,[status(thm)],[c843,symmetry]) ).
cnf(c910,plain,
X173 = compose(compose(codomain(X173),codomain(X173)),X173),
inference(resolution,[status(thm)],[c860,c55]) ).
cnf(c939,plain,
( ~ there_exists(X280)
| there_exists(compose(compose(codomain(X280),codomain(X280)),X280)) ),
inference(resolution,[status(thm)],[c910,c4]) ).
cnf(c2484,plain,
there_exists(compose(compose(codomain(a),codomain(a)),a)),
inference(resolution,[status(thm)],[c939,c7]) ).
cnf(c3688,plain,
there_exists(domain(compose(codomain(a),codomain(a)))),
inference(resolution,[status(thm)],[c2484,composition_implies_domain]) ).
cnf(c3725,plain,
there_exists(compose(codomain(a),codomain(a))),
inference(resolution,[status(thm)],[c3688,domain_has_elements]) ).
cnf(c3746,plain,
domain(codomain(a)) = codomain(codomain(a)),
inference(resolution,[status(thm)],[c3725,domain_codomain_composition1]) ).
cnf(c3752,plain,
codomain(codomain(a)) = domain(codomain(a)),
inference(resolution,[status(thm)],[c3746,symmetry]) ).
cnf(c3797,plain,
codomain(codomain(a)) = codomain(a),
inference(resolution,[status(thm)],[c3752,c105]) ).
cnf(c3822,plain,
$false,
inference(resolution,[status(thm)],[c3797,prove_codomain_is_idempotent]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : CAT014-4 : TPTP v8.1.2. Released v1.0.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n020.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 21:00:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 1.35/1.51 % Version: 1.5
% 1.35/1.51 % SZS status Unsatisfiable
% 1.35/1.51 % SZS output start CNFRefutation
% See solution above
% 1.35/1.51
% 1.35/1.51 % Initial clauses : 21
% 1.35/1.51 % Processed clauses : 287
% 1.35/1.51 % Factors computed : 5
% 1.35/1.51 % Resolvents computed: 3826
% 1.35/1.51 % Tautologies deleted: 3
% 1.35/1.51 % Forward subsumed : 259
% 1.35/1.51 % Backward subsumed : 3
% 1.35/1.51 % -------- CPU Time ---------
% 1.35/1.51 % User time : 1.146 s
% 1.35/1.51 % System time : 0.026 s
% 1.35/1.51 % Total time : 1.172 s
%------------------------------------------------------------------------------