%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO002-1 : TPTP v8.1.2. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:41 EDT 2024
% Result : Unsatisfiable 3.64s 3.89s
% Output : Refutation 3.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 10
% Syntax : Number of clauses : 29 ( 14 unt; 0 nHn; 15 RR)
% Number of literals : 53 ( 15 equ; 25 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 : 4 ( 4 usr; 2 con; 0-5 aty)
% Number of variables : 84 ( 14 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_a_between_a_and_b,negated_conjecture,
~ between(a,a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_a_between_a_and_b) ).
cnf(segment_construction1,axiom,
between(X20,X19,extension(X20,X19,X21,X18)),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/GEO001-0.ax',identity_for_equidistance) ).
cnf(segment_construction2,axiom,
equidistant(X34,extension(X33,X34,X35,X32),X35,X32),
file('/export/starexec/sandbox/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(X39,X41,X40,X40) = X41,
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 != X371
| X374 != X369
| X373 != X372
| ~ between(X370,X374,X373)
| between(X371,X369,X372) ),
theory(equality) ).
cnf(c282,plain,
( X1462 != X1464
| X1462 != X1463
| X1462 != X1465
| between(X1464,X1463,X1465) ),
inference(resolution,[status(thm)],[c5,c11]) ).
cnf(c1213,plain,
( X1509 != X1508
| X1509 != X1507
| between(X1508,X1507,X1509) ),
inference(resolution,[status(thm)],[c282,reflexivity]) ).
cnf(c1381,plain,
( X1510 != X1511
| between(X1511,X1511,X1510) ),
inference(factor,[status(thm)],[c1213]) ).
cnf(c1412,plain,
between(X1522,X1522,extension(X1521,X1522,X1520,X1520)),
inference(resolution,[status(thm)],[c1381,c18]) ).
cnf(c1447,plain,
( ~ between(X1777,X1776,extension(X1778,X1776,X1779,X1779))
| between(X1777,X1776,X1776) ),
inference(resolution,[status(thm)],[c1412,transitivity_for_betweeness]) ).
cnf(c2135,plain,
between(X1781,X1782,X1782),
inference(resolution,[status(thm)],[c1447,segment_construction1]) ).
cnf(outer_pasch2,axiom,
( ~ between(X87,X85,X86)
| ~ between(X84,X86,X83)
| between(X83,X85,outer_pasch(X85,X87,X84,X83,X86)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax',outer_pasch2) ).
cnf(c2152,plain,
( ~ between(X2282,X2281,X2279)
| between(X2279,X2281,outer_pasch(X2281,X2282,X2280,X2279,X2279)) ),
inference(resolution,[status(thm)],[c2135,outer_pasch2]) ).
cnf(c3882,plain,
between(X2284,X2284,outer_pasch(X2284,X2283,X2285,X2284,X2284)),
inference(resolution,[status(thm)],[c2152,c2135]) ).
cnf(outer_pasch1,axiom,
( ~ between(X68,X66,X67)
| ~ between(X65,X67,X64)
| between(X68,outer_pasch(X66,X68,X65,X64,X67),X65) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO001-0.ax',outer_pasch1) ).
cnf(c31,plain,
( ~ between(X267,X266,X266)
| between(X267,outer_pasch(X266,X267,X267,X266,X266),X267) ),
inference(factor,[status(thm)],[outer_pasch1]) ).
cnf(c2151,plain,
between(X1814,outer_pasch(X1815,X1814,X1814,X1815,X1815),X1814),
inference(resolution,[status(thm)],[c2135,c31]) ).
cnf(c2281,plain,
( ~ between(X2360,X2361,X2361)
| between(X2360,X2361,outer_pasch(X2362,X2361,X2361,X2362,X2362)) ),
inference(resolution,[status(thm)],[c2151,transitivity_for_betweeness]) ).
cnf(c4245,plain,
between(X2363,X2364,outer_pasch(X2365,X2364,X2364,X2365,X2365)),
inference(resolution,[status(thm)],[c2281,c2135]) ).
cnf(c4275,plain,
( ~ between(X2844,X2846,outer_pasch(X2843,X2845,X2845,X2843,X2843))
| between(X2844,X2846,X2845) ),
inference(resolution,[status(thm)],[c4245,transitivity_for_betweeness]) ).
cnf(c7215,plain,
between(X2849,X2849,X2850),
inference(resolution,[status(thm)],[c4275,c3882]) ).
cnf(c7246,plain,
$false,
inference(resolution,[status(thm)],[c7215,prove_a_between_a_and_b]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GEO002-1 : TPTP v8.1.2. Bugfixed v2.5.0.
% 0.10/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n016.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 : Thu May 9 08:27:23 EDT 2024
% 0.12/0.34 % CPUTime :
% 3.64/3.89 % Version: 1.5
% 3.64/3.89 % SZS status Unsatisfiable
% 3.64/3.89 % SZS output start CNFRefutation
% See solution above
% 3.64/3.89
% 3.64/3.89 % Initial clauses : 31
% 3.64/3.89 % Processed clauses : 327
% 3.64/3.89 % Factors computed : 140
% 3.64/3.89 % Resolvents computed: 7157
% 3.64/3.89 % Tautologies deleted: 5
% 3.64/3.89 % Forward subsumed : 394
% 3.64/3.89 % Backward subsumed : 92
% 3.64/3.89 % -------- CPU Time ---------
% 3.64/3.89 % User time : 3.520 s
% 3.64/3.89 % System time : 0.029 s
% 3.64/3.89 % Total time : 3.549 s
%------------------------------------------------------------------------------