%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO037-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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:51 EDT 2024
% Result : Unsatisfiable 38.51s 38.68s
% Output : Refutation 38.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 11
% Syntax : Number of clauses : 51 ( 29 unt; 0 nHn; 24 RR)
% Number of literals : 92 ( 41 equ; 42 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-4 aty)
% Number of variables : 199 ( 46 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(lower_dimension3,axiom,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',lower_dimension3) ).
cnf(symmetry,axiom,
( X12 != X11
| X11 = X12 ),
theory(equality) ).
cnf(identity_for_equidistance,axiom,
( ~ equidistant(X18,X17,X16,X16)
| X18 = X17 ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',identity_for_equidistance) ).
cnf(segment_construction2,axiom,
equidistant(X26,extension(X27,X26,X24,X25),X24,X25),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',segment_construction2) ).
cnf(c12,plain,
X28 = extension(X30,X28,X29,X29),
inference(resolution,[status(thm)],[segment_construction2,identity_for_equidistance]) ).
cnf(c13,plain,
extension(X31,X33,X32,X32) = X33,
inference(resolution,[status(thm)],[c12,symmetry]) ).
cnf(transitivity,axiom,
( X39 != X38
| X38 != X37
| X39 = X37 ),
theory(equality) ).
cnf(c17,plain,
( X189 != extension(X187,X188,X186,X186)
| X189 = X188 ),
inference(resolution,[status(thm)],[transitivity,c13]) ).
cnf(reflexivity_for_equidistance,axiom,
equidistant(X4,X3,X3,X4),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',reflexivity_for_equidistance) ).
cnf(transitivity_for_equidistance,axiom,
( ~ equidistant(X7,X8,X10,X6)
| ~ equidistant(X7,X8,X9,X5)
| equidistant(X10,X6,X9,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',transitivity_for_equidistance) ).
cnf(c8,plain,
( ~ equidistant(X67,X66,X65,X68)
| equidistant(X65,X68,X66,X67) ),
inference(resolution,[status(thm)],[transitivity_for_equidistance,reflexivity_for_equidistance]) ).
cnf(c32,plain,
equidistant(X76,X74,extension(X75,X73,X76,X74),X73),
inference(resolution,[status(thm)],[c8,segment_construction2]) ).
cnf(c34,plain,
equidistant(extension(X84,X82,X83,X85),X82,X85,X83),
inference(resolution,[status(thm)],[c32,c8]) ).
cnf(c39,plain,
equidistant(X90,X89,X92,extension(X91,X92,X89,X90)),
inference(resolution,[status(thm)],[c34,c8]) ).
cnf(c11,plain,
( ~ equidistant(X274,extension(X273,X274,X269,X272),X270,X271)
| equidistant(X270,X271,X269,X272) ),
inference(resolution,[status(thm)],[segment_construction2,transitivity_for_equidistance]) ).
cnf(c143,plain,
equidistant(X300,extension(X298,X300,extension(X297,X302,X299,X301),X302),X299,X301),
inference(resolution,[status(thm)],[c11,c39]) ).
cnf(c168,plain,
X307 = extension(X311,X307,extension(X308,X310,X309,X309),X310),
inference(resolution,[status(thm)],[c143,identity_for_equidistance]) ).
cnf(c171,plain,
extension(X315,X314,extension(X312,X316,X313,X313),X316) = X314,
inference(resolution,[status(thm)],[c168,symmetry]) ).
cnf(c179,plain,
extension(X1730,extension(X1725,X1728,X1724,X1724),extension(X1727,X1726,X1729,X1729),X1726) = X1728,
inference(resolution,[status(thm)],[c171,c17]) ).
cnf(c165,plain,
equidistant(X393,X392,extension(X394,X391,extension(X389,X390,X393,X392),X390),X391),
inference(resolution,[status(thm)],[c143,c8]) ).
cnf(c244,plain,
equidistant(extension(X3262,X3255,extension(X3259,X3257,X3258,extension(X3256,X3258,X3260,X3261)),X3257),X3255,X3260,X3261),
inference(resolution,[status(thm)],[c165,c11]) ).
cnf(c6262,plain,
extension(X3276,X3275,extension(X3281,X3278,X3277,extension(X3279,X3277,X3280,X3280)),X3278) = X3275,
inference(resolution,[status(thm)],[c244,identity_for_equidistance]) ).
cnf(segment_construction1,axiom,
between(X23,X22,extension(X23,X22,X20,X21)),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',segment_construction1) ).
cnf(c6,axiom,
( X476 != X474
| X475 != X477
| X478 != X479
| ~ between(X476,X475,X478)
| between(X474,X477,X479) ),
theory(equality) ).
cnf(c311,plain,
( X6908 != X6914
| X6909 != X6911
| extension(X6908,X6909,X6913,X6910) != X6912
| between(X6914,X6911,X6912) ),
inference(resolution,[status(thm)],[c6,segment_construction1]) ).
cnf(c16812,plain,
( X6956 != X6955
| X6957 != X6954
| between(X6955,X6954,X6957) ),
inference(resolution,[status(thm)],[c311,c6262]) ).
cnf(c7,plain,
( ~ equidistant(X53,X54,X51,X52)
| equidistant(X51,X52,X51,X52) ),
inference(factor,[status(thm)],[transitivity_for_equidistance]) ).
cnf(c24,plain,
equidistant(X56,X55,X56,X55),
inference(resolution,[status(thm)],[c7,segment_construction2]) ).
cnf(c26,plain,
( ~ equidistant(X99,X100,X97,X98)
| equidistant(X97,X98,X99,X100) ),
inference(resolution,[status(thm)],[c24,transitivity_for_equidistance]) ).
cnf(c47,plain,
equidistant(X110,extension(X113,X110,X112,X111),X111,X112),
inference(resolution,[status(thm)],[c26,c39]) ).
cnf(c63,plain,
( ~ equidistant(X1104,extension(X1101,X1104,X1103,X1099),X1100,X1102)
| equidistant(X1100,X1102,X1099,X1103) ),
inference(resolution,[status(thm)],[c47,transitivity_for_equidistance]) ).
cnf(c51,plain,
equidistant(extension(X132,X133,X130,X131),X133,X130,X131),
inference(resolution,[status(thm)],[c26,c32]) ).
cnf(c5,axiom,
( X441 != X438
| X439 != X442
| X443 != X444
| X437 != X440
| ~ equidistant(X441,X439,X443,X437)
| equidistant(X438,X442,X444,X440) ),
theory(equality) ).
cnf(c287,plain,
( extension(X6394,X6388,X6389,X6391) != X6390
| X6388 != X6395
| X6389 != X6392
| X6391 != X6393
| equidistant(X6390,X6395,X6392,X6393) ),
inference(resolution,[status(thm)],[c5,c51]) ).
cnf(c14214,plain,
( X6399 != X6398
| X6396 != X6397
| X6396 != X6400
| equidistant(X6399,X6398,X6397,X6400) ),
inference(resolution,[status(thm)],[c287,c13]) ).
cnf(c14223,plain,
( X6638 != X6641
| X6639 != X6640
| equidistant(X6638,X6641,X6640,X6640) ),
inference(factor,[status(thm)],[c14214]) ).
cnf(c15585,plain,
( X6645 != X6644
| equidistant(X6645,X6644,X6646,X6646) ),
inference(resolution,[status(thm)],[c14223,c179]) ).
cnf(prove_lengthen,negated_conjecture,
( v = extension(u,v,lower_dimension_point_1,lower_dimension_point_2)
| ~ equidistant(v,extension(u,v,lower_dimension_point_1,lower_dimension_point_2),x,extension(w,x,lower_dimension_point_1,lower_dimension_point_2))
| ~ between(u,v,extension(u,v,lower_dimension_point_1,lower_dimension_point_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_lengthen) ).
cnf(c36,plain,
( ~ equidistant(X670,X666,X667,X668)
| equidistant(X667,X668,extension(X665,X669,X670,X666),X669) ),
inference(resolution,[status(thm)],[c32,transitivity_for_equidistance]) ).
cnf(c457,plain,
equidistant(extension(X725,X729,X726,X727),X729,extension(X730,X728,X726,X727),X728),
inference(resolution,[status(thm)],[c36,c32]) ).
cnf(c518,plain,
equidistant(extension(X789,X793,X790,X791),X793,X794,extension(X792,X794,X790,X791)),
inference(resolution,[status(thm)],[c457,c8]) ).
cnf(c582,plain,
equidistant(X845,extension(X842,X845,X843,X841),X846,extension(X844,X846,X843,X841)),
inference(resolution,[status(thm)],[c518,c8]) ).
cnf(c630,plain,
( v = extension(u,v,lower_dimension_point_1,lower_dimension_point_2)
| ~ between(u,v,extension(u,v,lower_dimension_point_1,lower_dimension_point_2)) ),
inference(resolution,[status(thm)],[c582,prove_lengthen]) ).
cnf(c39250,plain,
v = extension(u,v,lower_dimension_point_1,lower_dimension_point_2),
inference(resolution,[status(thm)],[c630,segment_construction1]) ).
cnf(c39283,plain,
equidistant(v,extension(u,v,lower_dimension_point_1,lower_dimension_point_2),X13641,X13641),
inference(resolution,[status(thm)],[c39250,c15585]) ).
cnf(c39565,plain,
equidistant(X13642,X13642,lower_dimension_point_2,lower_dimension_point_1),
inference(resolution,[status(thm)],[c39283,c63]) ).
cnf(c39618,plain,
equidistant(lower_dimension_point_2,lower_dimension_point_1,X13652,X13652),
inference(resolution,[status(thm)],[c39565,c8]) ).
cnf(c39791,plain,
lower_dimension_point_2 = lower_dimension_point_1,
inference(resolution,[status(thm)],[c39618,identity_for_equidistance]) ).
cnf(c39911,plain,
( X13723 != X13722
| between(X13722,lower_dimension_point_1,lower_dimension_point_2) ),
inference(resolution,[status(thm)],[c39791,c16812]) ).
cnf(c40644,plain,
between(X13731,lower_dimension_point_1,lower_dimension_point_2),
inference(resolution,[status(thm)],[c39911,c179]) ).
cnf(c40731,plain,
$false,
inference(resolution,[status(thm)],[c40644,lower_dimension3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GEO037-2 : TPTP v8.1.2. Released v1.0.0.
% 0.00/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.31 % Computer : n017.cluster.edu
% 0.12/0.31 % Model : x86_64 x86_64
% 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31 % Memory : 8042.1875MB
% 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31 % CPULimit : 300
% 0.12/0.31 % WCLimit : 300
% 0.12/0.31 % DateTime : Thu May 9 07:53:53 EDT 2024
% 0.17/0.31 % CPUTime :
% 38.51/38.68 % Version: 1.5
% 38.51/38.68 % SZS status Unsatisfiable
% 38.51/38.68 % SZS output start CNFRefutation
% See solution above
% 38.51/38.68
% 38.51/38.68 % Initial clauses : 29
% 38.51/38.68 % Processed clauses : 863
% 38.51/38.68 % Factors computed : 409
% 38.51/38.68 % Resolvents computed: 40323
% 38.51/38.68 % Tautologies deleted: 5
% 38.51/38.68 % Forward subsumed : 1875
% 38.51/38.68 % Backward subsumed : 147
% 38.51/38.68 % -------- CPU Time ---------
% 38.51/38.68 % User time : 38.262 s
% 38.51/38.68 % System time : 0.105 s
% 38.51/38.68 % Total time : 38.367 s
%------------------------------------------------------------------------------