%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CAT009-4 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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 18.61s 18.82s
% Output : Refutation 18.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of clauses : 32 ( 19 unt; 0 nHn; 26 RR)
% Number of literals : 48 ( 25 equ; 17 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 : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 34 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_domain_of_ab_equals_domain_of_b,negated_conjecture,
domain(compose(a,b)) != domain(b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_domain_of_ab_equals_domain_of_b) ).
cnf(transitivity,axiom,
( X38 != X39
| X39 != X37
| X38 = X37 ),
theory(equality) ).
cnf(symmetry,axiom,
( X12 != X13
| X13 = X12 ),
theory(equality) ).
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(compose_domain,axiom,
compose(X15,domain(X15)) = X15,
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',compose_domain) ).
cnf(c9,plain,
X21 = compose(X21,domain(X21)),
inference(resolution,[status(thm)],[compose_domain,symmetry]) ).
cnf(c4,axiom,
( X28 != X27
| ~ there_exists(X28)
| there_exists(X27) ),
theory(equality) ).
cnf(c25,plain,
( ~ there_exists(X34)
| there_exists(compose(X34,domain(X34))) ),
inference(resolution,[status(thm)],[c4,c9]) ).
cnf(codomain_has_elements,axiom,
( ~ there_exists(codomain(X8))
| there_exists(X8) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',codomain_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(c16,plain,
domain(a) = codomain(b),
inference(resolution,[status(thm)],[domain_codomain_composition1,ab_exists]) ).
cnf(c30,plain,
( ~ there_exists(domain(a))
| there_exists(codomain(b)) ),
inference(resolution,[status(thm)],[c16,c4]) ).
cnf(c107,plain,
there_exists(codomain(b)),
inference(resolution,[status(thm)],[c30,c10]) ).
cnf(c119,plain,
there_exists(b),
inference(resolution,[status(thm)],[c107,codomain_has_elements]) ).
cnf(c124,plain,
there_exists(compose(b,domain(b))),
inference(resolution,[status(thm)],[c119,c25]) ).
cnf(c137,plain,
domain(b) = codomain(domain(b)),
inference(resolution,[status(thm)],[c124,domain_codomain_composition1]) ).
cnf(c213,plain,
codomain(domain(b)) = domain(b),
inference(resolution,[status(thm)],[c137,symmetry]) ).
cnf(c263,plain,
( X350 != codomain(domain(b))
| X350 = domain(b) ),
inference(resolution,[status(thm)],[c213,transitivity]) ).
cnf(associativity_of_compose,axiom,
compose(X31,compose(X32,X30)) = compose(compose(X31,X32),X30),
file('/export/starexec/sandbox2/benchmark/Axioms/CAT004-0.ax',associativity_of_compose) ).
cnf(c34,plain,
( ~ there_exists(compose(X63,compose(X61,X62)))
| there_exists(compose(compose(X63,X61),X62)) ),
inference(resolution,[status(thm)],[associativity_of_compose,c4]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c2,axiom,
( X53 != X51
| X52 != X54
| compose(X53,X52) = compose(X51,X54) ),
theory(equality) ).
cnf(c113,plain,
( X144 != X145
| compose(X144,X146) = compose(X145,compose(X146,domain(X146))) ),
inference(resolution,[status(thm)],[c2,c9]) ).
cnf(c1056,plain,
compose(X212,X211) = compose(X212,compose(X211,domain(X211))),
inference(resolution,[status(thm)],[c113,reflexivity]) ).
cnf(c2106,plain,
( ~ there_exists(compose(X756,X757))
| there_exists(compose(X756,compose(X757,domain(X757)))) ),
inference(resolution,[status(thm)],[c1056,c4]) ).
cnf(c27570,plain,
there_exists(compose(a,compose(b,domain(b)))),
inference(resolution,[status(thm)],[c2106,ab_exists]) ).
cnf(c27682,plain,
there_exists(compose(compose(a,b),domain(b))),
inference(resolution,[status(thm)],[c27570,c34]) ).
cnf(c27717,plain,
domain(compose(a,b)) = codomain(domain(b)),
inference(resolution,[status(thm)],[c27682,domain_codomain_composition1]) ).
cnf(c27872,plain,
domain(compose(a,b)) = domain(b),
inference(resolution,[status(thm)],[c27717,c263]) ).
cnf(c27899,plain,
$false,
inference(resolution,[status(thm)],[c27872,prove_domain_of_ab_equals_domain_of_b]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.14 % Problem : CAT009-4 : TPTP v8.1.2. Released v1.0.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n011.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 21:00:38 EDT 2024
% 0.15/0.36 % CPUTime :
% 18.61/18.82 % Version: 1.5
% 18.61/18.82 % SZS status Unsatisfiable
% 18.61/18.82 % SZS output start CNFRefutation
% See solution above
% 18.61/18.82
% 18.61/18.82 % Initial clauses : 21
% 18.61/18.82 % Processed clauses : 1112
% 18.61/18.82 % Factors computed : 12
% 18.61/18.82 % Resolvents computed: 27914
% 18.61/18.82 % Tautologies deleted: 3
% 18.61/18.82 % Forward subsumed : 1588
% 18.61/18.82 % Backward subsumed : 7
% 18.61/18.82 % -------- CPU Time ---------
% 18.61/18.82 % User time : 18.387 s
% 18.61/18.82 % System time : 0.067 s
% 18.61/18.82 % Total time : 18.454 s
%------------------------------------------------------------------------------