%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO003-1 : TPTP v8.1.2. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:20:42 EDT 2024
% Result : Unsatisfiable 1.20s 1.40s
% Output : Refutation 1.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of clauses : 19 ( 10 unt; 0 nHn; 11 RR)
% Number of literals : 35 ( 15 equ; 17 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-4 aty)
% Number of variables : 51 ( 9 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_b_between_a_and_b,negated_conjecture,
~ between(a,b,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_b_between_a_and_b) ).
cnf(segment_construction1,axiom,
between(X21,X20,extension(X21,X20,X19,X18)),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO001-0.ax',segment_construction1) ).
cnf(transitivity_for_betweeness,axiom,
( ~ between(X17,X16,X15)
| ~ between(X16,X14,X15)
| between(X17,X16,X14) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO001-0.ax',transitivity_for_betweeness) ).
cnf(symmetry,axiom,
( X8 != X7
| X7 = X8 ),
theory(equality) ).
cnf(identity_for_equidistance,axiom,
( ~ equidistant(X12,X11,X10,X10)
| X12 = X11 ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO001-0.ax',identity_for_equidistance) ).
cnf(segment_construction2,axiom,
equidistant(X34,extension(X35,X34,X33,X32),X33,X32),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO001-0.ax',segment_construction2) ).
cnf(c17,plain,
X36 = extension(X38,X36,X37,X37),
inference(resolution,[status(thm)],[segment_construction2,identity_for_equidistance]) ).
cnf(c18,plain,
extension(X41,X39,X40,X40) = X39,
inference(resolution,[status(thm)],[c17,symmetry]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c9,plain,
( ~ between(X22,X22,X23)
| between(X22,X22,X22) ),
inference(factor,[status(thm)],[transitivity_for_betweeness]) ).
cnf(c11,plain,
between(X24,X24,X24),
inference(resolution,[status(thm)],[c9,segment_construction1]) ).
cnf(c5,axiom,
( X370 != X372
| X369 != X373
| X374 != X371
| ~ between(X370,X369,X374)
| between(X372,X373,X371) ),
theory(equality) ).
cnf(c283,plain,
( X1462 != X1464
| X1462 != X1463
| X1462 != X1465
| between(X1464,X1463,X1465) ),
inference(resolution,[status(thm)],[c5,c11]) ).
cnf(c1215,plain,
( X1506 != X1505
| X1506 != X1507
| between(X1505,X1507,X1506) ),
inference(resolution,[status(thm)],[c283,reflexivity]) ).
cnf(c1378,plain,
( X1509 != X1508
| between(X1508,X1508,X1509) ),
inference(factor,[status(thm)],[c1215]) ).
cnf(c1403,plain,
between(X1519,X1519,extension(X1518,X1519,X1520,X1520)),
inference(resolution,[status(thm)],[c1378,c18]) ).
cnf(c1441,plain,
( ~ between(X1776,X1774,extension(X1777,X1774,X1775,X1775))
| between(X1776,X1774,X1774) ),
inference(resolution,[status(thm)],[c1403,transitivity_for_betweeness]) ).
cnf(c2132,plain,
between(X1778,X1779,X1779),
inference(resolution,[status(thm)],[c1441,segment_construction1]) ).
cnf(c2139,plain,
$false,
inference(resolution,[status(thm)],[c2132,prove_b_between_a_and_b]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO003-1 : TPTP v8.1.2. Bugfixed v2.5.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n025.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 07:43:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 1.20/1.40 % Version: 1.5
% 1.20/1.40 % SZS status Unsatisfiable
% 1.20/1.40 % SZS output start CNFRefutation
% See solution above
% 1.20/1.40
% 1.20/1.40 % Initial clauses : 31
% 1.20/1.40 % Processed clauses : 183
% 1.20/1.40 % Factors computed : 65
% 1.20/1.40 % Resolvents computed: 2092
% 1.20/1.40 % Tautologies deleted: 4
% 1.20/1.40 % Forward subsumed : 243
% 1.20/1.40 % Backward subsumed : 19
% 1.20/1.40 % -------- CPU Time ---------
% 1.20/1.40 % User time : 1.037 s
% 1.20/1.40 % System time : 0.014 s
% 1.20/1.40 % Total time : 1.051 s
%------------------------------------------------------------------------------