%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO037-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:16:39 PM UTC 2026
% Result : Unsatisfiable 10.58s 1.82s
% Output : Proof 10.58s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t75,axiom,
sF3 = between(u,v,extension(u,v,lower_dimension_point_1,lower_dimension_point_2)),
introduced(definition) ).
cnf(f3,axiom,
between(X,Y,extension(X,Y,W,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment_construction1) ).
fof(f3_nnf,plain,
! [X,Y,W,V] : between(X,Y,extension(X,Y,W,V)),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y,W,V] : between(X,Y,extension(X,Y,W,V)),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
between(X0,X1,extension(X0,X1,X2,X3)),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t24,plain,
between(X1,X2,extension(X1,X2,X3,X4)) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t111,plain,
between(X1,X2,extension(X1,X2,X3,X4)) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t2967,plain,
sF3 = true,
inference(step,[status(thm)],[t75,t111]) ).
cnf(t119,plain,
true = sF3,
inference(orient,[status(thm)],[t2967]) ).
cnf(f1,axiom,
( equidistant(Z,V,V2,W)
| ~ equidistant(X,Y,V2,W)
| ~ equidistant(X,Y,Z,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_for_equidistance) ).
fof(f1_nnf,plain,
! [X,Y,Z,V,V2,W] :
( equidistant(Z,V,V2,W)
| ~ equidistant(X,Y,V2,W)
| ~ equidistant(X,Y,Z,V) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y,Z,V,V2,W] :
( equidistant(Z,V,V2,W)
| ~ equidistant(X,Y,V2,W)
| ~ equidistant(X,Y,Z,V) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( equidistant(X2,X3,X4,X5)
| ~ equidistant(X0,X1,X4,X5)
| ~ equidistant(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t55,plain,
ifeq(equidistant(X1,X2,X3,X4),true,ifeq(equidistant(X1,X2,X5,X6),true,equidistant(X3,X4,X5,X6),true),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t3179,plain,
ifeq(equidistant(X1,X2,X3,X4),sF3,ifeq(equidistant(X1,X2,X5,X6),true,equidistant(X3,X4,X5,X6),true),true) = true,
inference(step,[status(thm)],[t55,t119]) ).
cnf(t3180,plain,
ifeq(equidistant(X1,X2,X3,X4),sF3,ifeq(equidistant(X1,X2,X5,X6),sF3,equidistant(X3,X4,X5,X6),true),true) = true,
inference(step,[status(thm)],[t3179,t119]) ).
cnf(t3181,plain,
ifeq(equidistant(X1,X2,X3,X4),sF3,ifeq(equidistant(X1,X2,X5,X6),sF3,equidistant(X3,X4,X5,X6),sF3),true) = true,
inference(step,[status(thm)],[t3180,t119]) ).
cnf(t3182,plain,
ifeq(equidistant(X1,X2,X3,X4),sF3,ifeq(equidistant(X1,X2,X5,X6),sF3,equidistant(X3,X4,X5,X6),sF3),sF3) = true,
inference(step,[status(thm)],[t3181,t119]) ).
cnf(t3183,plain,
ifeq(equidistant(X1,X2,X3,X4),sF3,ifeq(equidistant(X1,X2,X5,X6),sF3,equidistant(X3,X4,X5,X6),sF3),sF3) = sF3,
inference(step,[status(thm)],[t3182,t119]) ).
cnf(t901,plain,
ifeq(equidistant(X1,X2,X3,X4),sF3,ifeq(equidistant(X1,X2,X5,X6),sF3,equidistant(X3,X4,X5,X6),sF3),sF3) = sF3,
inference(orient,[status(thm)],[t3183]) ).
cnf(f20,axiom,
( equidistant(W,X,U,V)
| ~ equidistant(U,V,W,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2) ).
fof(f20_nnf,plain,
! [U,V,W,X] :
( equidistant(W,X,U,V)
| ~ equidistant(U,V,W,X) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [U,V,W,X] :
( equidistant(W,X,U,V)
| ~ equidistant(U,V,W,X) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( equidistant(X2,X3,X0,X1)
| ~ equidistant(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t40,plain,
ifeq(equidistant(X1,X2,X3,X4),true,equidistant(X3,X4,X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t3031,plain,
ifeq(equidistant(X1,X2,X3,X4),sF3,equidistant(X3,X4,X1,X2),true) = true,
inference(step,[status(thm)],[t40,t119]) ).
cnf(t3032,plain,
ifeq(equidistant(X1,X2,X3,X4),sF3,equidistant(X3,X4,X1,X2),sF3) = true,
inference(step,[status(thm)],[t3031,t119]) ).
cnf(t3033,plain,
ifeq(equidistant(X1,X2,X3,X4),sF3,equidistant(X3,X4,X1,X2),sF3) = sF3,
inference(step,[status(thm)],[t3032,t119]) ).
cnf(t255,plain,
ifeq(equidistant(X1,X2,X3,X4),sF3,equidistant(X3,X4,X1,X2),sF3) = sF3,
inference(orient,[status(thm)],[t3033]) ).
cnf(f4,axiom,
equidistant(Y,extension(X,Y,W,V),W,V),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment_construction2) ).
fof(f4_nnf,plain,
! [Y,X,W,V] : equidistant(Y,extension(X,Y,W,V),W,V),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [Y,X,W,V] : equidistant(Y,extension(X,Y,W,V),W,V),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
equidistant(X0,extension(X1,X0,X2,X3),X2,X3),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t30,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t2998,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4) = sF3,
inference(step,[status(thm)],[t30,t119]) ).
cnf(t161,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4) = sF3,
inference(orient,[status(thm)],[t2998]) ).
cnf(t72,axiom,
sF0 = extension(u,v,lower_dimension_point_1,lower_dimension_point_2),
introduced(definition) ).
cnf(t101,plain,
extension(u,v,lower_dimension_point_1,lower_dimension_point_2) = sF0,
inference(orient,[status(thm)],[t72]) ).
cnf(t163,plain,
sF3 = equidistant(v,sF0,lower_dimension_point_1,lower_dimension_point_2),
inference(cp,[status(thm)],[t161,t101]) ).
cnf(t165,plain,
equidistant(v,sF0,lower_dimension_point_1,lower_dimension_point_2) = sF3,
inference(orient,[status(thm)],[t163]) ).
cnf(t257,plain,
sF3 = ifeq(sF3,sF3,equidistant(lower_dimension_point_1,lower_dimension_point_2,v,sF0),sF3),
inference(cp,[status(thm)],[t255,t165]) ).
cnf(t18,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t97,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t18]) ).
cnf(t3034,plain,
sF3 = equidistant(lower_dimension_point_1,lower_dimension_point_2,v,sF0),
inference(step,[status(thm)],[t257,t97]) ).
cnf(t268,plain,
equidistant(lower_dimension_point_1,lower_dimension_point_2,v,sF0) = sF3,
inference(orient,[status(thm)],[t3034]) ).
cnf(t929,plain,
sF3 = ifeq(sF3,sF3,ifeq(equidistant(lower_dimension_point_1,lower_dimension_point_2,X1,X2),sF3,equidistant(v,sF0,X1,X2),sF3),sF3),
inference(cp,[status(thm)],[t901,t268]) ).
cnf(t3358,plain,
sF3 = ifeq(equidistant(lower_dimension_point_1,lower_dimension_point_2,X1,X2),sF3,equidistant(v,sF0,X1,X2),sF3),
inference(step,[status(thm)],[t929,t97]) ).
cnf(t2076,plain,
ifeq(equidistant(lower_dimension_point_1,lower_dimension_point_2,X1,X2),sF3,equidistant(v,sF0,X1,X2),sF3) = sF3,
inference(orient,[status(thm)],[t3358]) ).
cnf(t73,axiom,
sF1 = extension(w,x,lower_dimension_point_1,lower_dimension_point_2),
introduced(definition) ).
cnf(t102,plain,
extension(w,x,lower_dimension_point_1,lower_dimension_point_2) = sF1,
inference(orient,[status(thm)],[t73]) ).
cnf(t164,plain,
sF3 = equidistant(x,sF1,lower_dimension_point_1,lower_dimension_point_2),
inference(cp,[status(thm)],[t161,t102]) ).
cnf(t167,plain,
equidistant(x,sF1,lower_dimension_point_1,lower_dimension_point_2) = sF3,
inference(orient,[status(thm)],[t164]) ).
cnf(t258,plain,
sF3 = ifeq(sF3,sF3,equidistant(lower_dimension_point_1,lower_dimension_point_2,x,sF1),sF3),
inference(cp,[status(thm)],[t255,t167]) ).
cnf(t3038,plain,
sF3 = equidistant(lower_dimension_point_1,lower_dimension_point_2,x,sF1),
inference(step,[status(thm)],[t258,t97]) ).
cnf(t270,plain,
equidistant(lower_dimension_point_1,lower_dimension_point_2,x,sF1) = sF3,
inference(orient,[status(thm)],[t3038]) ).
cnf(t2077,plain,
sF3 = ifeq(sF3,sF3,equidistant(v,sF0,x,sF1),sF3),
inference(cp,[status(thm)],[t2076,t270]) ).
cnf(t3359,plain,
sF3 = equidistant(v,sF0,x,sF1),
inference(step,[status(thm)],[t2077,t97]) ).
cnf(t74,axiom,
sF2 = 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)),
introduced(definition) ).
cnf(t3059,plain,
sF2 = equidistant(v,sF0,x,extension(w,x,lower_dimension_point_1,lower_dimension_point_2)),
inference(step,[status(thm)],[t74,t101]) ).
cnf(t3060,plain,
sF2 = equidistant(v,sF0,x,sF1),
inference(step,[status(thm)],[t3059,t102]) ).
cnf(t287,plain,
equidistant(v,sF0,x,sF1) = sF2,
inference(orient,[status(thm)],[t3060]) ).
cnf(t3360,plain,
sF3 = sF2,
inference(step,[status(thm)],[t3359,t287]) ).
cnf(t2087,plain,
sF3 = sF2,
inference(orient,[status(thm)],[t3360]) ).
cnf(t3379,plain,
true = sF2,
inference(step,[status(thm)],[t119,t2087]) ).
cnf(t2106,plain,
true = sF2,
inference(orient,[status(thm)],[t3379]) ).
cnf(f57,axiom,
lower_dimension_point_1 != lower_dimension_point_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e2_1) ).
fof(f57_nnf,plain,
lower_dimension_point_1 != lower_dimension_point_2,
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
lower_dimension_point_1 != lower_dimension_point_2,
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c57,plain,
lower_dimension_point_1 != lower_dimension_point_2,
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(t1,plain,
eq(lower_dimension_point_1,lower_dimension_point_2) = false,
inference(equality_encoding,[status(esa)],[c57]) ).
cnf(t79,plain,
eq(lower_dimension_point_1,lower_dimension_point_2) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t2887,plain,
eq(lower_dimension_point_2,lower_dimension_point_2) = false,
inference(rw,[status(thm)],[t79]) ).
cnf(t0,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t78,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t2968,plain,
eq(X1,X1) = sF3,
inference(step,[status(thm)],[t78,t119]) ).
cnf(t120,plain,
eq(X1,X1) = sF3,
inference(orient,[status(thm)],[t2968]) ).
cnf(t3361,plain,
eq(X1,X1) = sF2,
inference(step,[status(thm)],[t120,t2087]) ).
cnf(t2088,plain,
eq(X1,X1) = sF2,
inference(orient,[status(thm)],[t3361]) ).
cnf(t3747,plain,
sF2 = false,
inference(step,[status(thm)],[t2887,t2088]) ).
cnf(t2953,plain,
false = sF2,
inference(orient,[status(thm)],[t3747]) ).
cnf(f9,axiom,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lower_dimension1) ).
fof(f9_nnf,plain,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(f10,axiom,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lower_dimension2) ).
fof(f10_nnf,plain,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(f11,axiom,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lower_dimension3) ).
fof(f11_nnf,plain,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(f58,axiom,
lower_dimension_point_2 != lower_dimension_point_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e2_2) ).
fof(f58_nnf,plain,
lower_dimension_point_2 != lower_dimension_point_3,
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
lower_dimension_point_2 != lower_dimension_point_3,
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c58,plain,
lower_dimension_point_2 != lower_dimension_point_3,
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(f59,axiom,
lower_dimension_point_1 != lower_dimension_point_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e2_3) ).
fof(f59_nnf,plain,
lower_dimension_point_1 != lower_dimension_point_3,
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
lower_dimension_point_1 != lower_dimension_point_3,
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c59,plain,
lower_dimension_point_1 != lower_dimension_point_3,
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c9,c10,c11,c57,c58,c59]) ).
cnf(g0_0,plain,
sF2 != false,
inference(rw,[status(thm)],[goal_0,t2106]) ).
cnf(g0_1,plain,
sF2 != sF2,
inference(rw,[status(thm)],[g0_0,t2953]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO037-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 10:30:57 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 10.58/1.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.58/1.82 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------