%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CAT010-4 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:59 EDT 2024
% Result : Unsatisfiable 15.33s 15.52s
% Output : Refutation 15.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 14
% Syntax : Number of clauses : 36 ( 20 unt; 0 nHn; 29 RR)
% Number of literals : 58 ( 26 equ; 23 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 45 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_codomain_of_ab_equals_codomain_of_a,negated_conjecture,
codomain(compose(a,b)) != codomain(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_codomain_of_ab_equals_codomain_of_a) ).
cnf(equivalence_implies_existence2,axiom,
( ~ equivalent(X5,X6)
| X5 = X6 ),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',equivalence_implies_existence2) ).
cnf(domain_codomain_composition1,axiom,
( ~ there_exists(compose(X18,X19))
| domain(X18) = codomain(X19) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',domain_codomain_composition1) ).
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(ab_exists,plain,
there_exists(compose(a,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ab_exists) ).
cnf(composition_implies_domain,axiom,
( ~ there_exists(compose(X16,X17))
| there_exists(domain(X16)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',composition_implies_domain) ).
cnf(c10,plain,
there_exists(domain(a)),
inference(resolution,[status(thm)],[composition_implies_domain,ab_exists]) ).
cnf(c12,plain,
there_exists(a),
inference(resolution,[status(thm)],[c10,domain_has_elements]) ).
cnf(symmetry,axiom,
( X12 != X13
| X13 = X12 ),
theory(equality) ).
cnf(compose_codomain,axiom,
compose(codomain(X20),X20) = X20,
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',compose_codomain) ).
cnf(c17,plain,
X22 = compose(codomain(X22),X22),
inference(resolution,[status(thm)],[compose_codomain,symmetry]) ).
cnf(c4,axiom,
( X28 != X27
| ~ there_exists(X28)
| there_exists(X27) ),
theory(equality) ).
cnf(c24,plain,
( ~ there_exists(X34)
| there_exists(compose(codomain(X34),X34)) ),
inference(resolution,[status(thm)],[c4,c17]) ).
cnf(c41,plain,
there_exists(compose(codomain(a),a)),
inference(resolution,[status(thm)],[c24,c12]) ).
cnf(c46,plain,
domain(codomain(a)) = codomain(a),
inference(resolution,[status(thm)],[c41,domain_codomain_composition1]) ).
cnf(c3,axiom,
( X57 != X55
| X56 != X58
| ~ equivalent(X57,X56)
| equivalent(X55,X58) ),
theory(equality) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(existence_and_equality_implies_equivalence1,axiom,
( ~ there_exists(X9)
| X9 != X10
| equivalent(X9,X10) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',existence_and_equality_implies_equivalence1) ).
cnf(c5,plain,
( ~ there_exists(X11)
| equivalent(X11,X11) ),
inference(resolution,[status(thm)],[existence_and_equality_implies_equivalence1,reflexivity]) ).
cnf(c43,plain,
there_exists(domain(codomain(a))),
inference(resolution,[status(thm)],[c41,composition_implies_domain]) ).
cnf(c49,plain,
equivalent(domain(codomain(a)),domain(codomain(a))),
inference(resolution,[status(thm)],[c43,c5]) ).
cnf(c360,plain,
( domain(codomain(a)) != X396
| domain(codomain(a)) != X395
| equivalent(X396,X395) ),
inference(resolution,[status(thm)],[c49,c3]) ).
cnf(c7187,plain,
( domain(codomain(a)) != X581
| equivalent(X581,codomain(a)) ),
inference(resolution,[status(thm)],[c360,c46]) ).
cnf(associativity_of_compose,axiom,
compose(X30,compose(X31,X32)) = compose(compose(X30,X31),X32),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',associativity_of_compose) ).
cnf(c35,plain,
compose(compose(X65,X64),X66) = compose(X65,compose(X64,X66)),
inference(resolution,[status(thm)],[associativity_of_compose,symmetry]) ).
cnf(c234,plain,
( ~ there_exists(compose(compose(X302,X304),X303))
| there_exists(compose(X302,compose(X304,X303))) ),
inference(resolution,[status(thm)],[c35,c4]) ).
cnf(c2,axiom,
( X53 != X51
| X52 != X54
| compose(X53,X52) = compose(X51,X54) ),
theory(equality) ).
cnf(c113,plain,
( X114 != X112
| compose(X114,X113) = compose(X112,X113) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(c744,plain,
compose(X190,X189) = compose(compose(codomain(X190),X190),X189),
inference(resolution,[status(thm)],[c113,c17]) ).
cnf(c1669,plain,
( ~ there_exists(compose(X718,X719))
| there_exists(compose(compose(codomain(X718),X718),X719)) ),
inference(resolution,[status(thm)],[c744,c4]) ).
cnf(c25883,plain,
there_exists(compose(compose(codomain(a),a),b)),
inference(resolution,[status(thm)],[c1669,ab_exists]) ).
cnf(c25996,plain,
there_exists(compose(codomain(a),compose(a,b))),
inference(resolution,[status(thm)],[c25883,c234]) ).
cnf(c26006,plain,
domain(codomain(a)) = codomain(compose(a,b)),
inference(resolution,[status(thm)],[c25996,domain_codomain_composition1]) ).
cnf(c26139,plain,
equivalent(codomain(compose(a,b)),codomain(a)),
inference(resolution,[status(thm)],[c26006,c7187]) ).
cnf(c26178,plain,
codomain(compose(a,b)) = codomain(a),
inference(resolution,[status(thm)],[c26139,equivalence_implies_existence2]) ).
cnf(c26270,plain,
$false,
inference(resolution,[status(thm)],[c26178,prove_codomain_of_ab_equals_codomain_of_a]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CAT010-4 : TPTP v8.1.2. Released v1.0.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n019.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 21:00:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 15.33/15.52 % Version: 1.5
% 15.33/15.52 % SZS status Unsatisfiable
% 15.33/15.52 % SZS output start CNFRefutation
% See solution above
% 15.33/15.52
% 15.33/15.52 % Initial clauses : 21
% 15.33/15.52 % Processed clauses : 1074
% 15.33/15.52 % Factors computed : 11
% 15.33/15.52 % Resolvents computed: 26258
% 15.33/15.52 % Tautologies deleted: 3
% 15.33/15.52 % Forward subsumed : 1540
% 15.33/15.52 % Backward subsumed : 7
% 15.33/15.52 % -------- CPU Time ---------
% 15.33/15.52 % User time : 15.120 s
% 15.33/15.52 % System time : 0.063 s
% 15.33/15.52 % Total time : 15.183 s
%------------------------------------------------------------------------------