%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO044-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 : n019.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:43 PM UTC 2026
% Result : Unsatisfiable 7.50s 1.50s
% Output : Proof 7.50s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t68,axiom,
sF1 = ifeq(between(u,w,x),true,false,true),
introduced(definition) ).
cnf(f56,negated_conjecture,
~ between(u,w,x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_w_between_u_and_x) ).
fof(f56_nnf,plain,
~ between(u,w,x),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
~ between(u,w,x),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c56,plain,
~ between(u,w,x),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(t12,plain,
between(u,w,x) = false,
inference(equality_encoding,[status(esa)],[c56]) ).
cnf(t81,plain,
between(u,w,x) = false,
inference(orient,[status(thm)],[t12]) ).
cnf(t67,axiom,
sF0 = between(u,w,x),
introduced(definition) ).
cnf(t2409,plain,
sF0 = false,
inference(step,[status(thm)],[t67,t81]) ).
cnf(t83,plain,
false = sF0,
inference(orient,[status(thm)],[t2409]) ).
cnf(t2420,plain,
between(u,w,x) = sF0,
inference(step,[status(thm)],[t81,t83]) ).
cnf(t94,plain,
between(u,w,x) = sF0,
inference(orient,[status(thm)],[t2420]) ).
cnf(t2427,plain,
sF1 = ifeq(sF0,true,false,true),
inference(step,[status(thm)],[t68,t94]) ).
cnf(t2428,plain,
sF1 = ifeq(sF0,true,sF0,true),
inference(step,[status(thm)],[t2427,t83]) ).
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(t25,plain,
ifeq(between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t8,plain,
between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3) = false,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t77,plain,
between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3) = false,
inference(orient,[status(thm)],[t8]) ).
cnf(t2414,plain,
between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3) = sF0,
inference(step,[status(thm)],[t77,t83]) ).
cnf(t88,plain,
between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3) = sF0,
inference(orient,[status(thm)],[t2414]) ).
cnf(t2425,plain,
ifeq(sF0,true,false,true) = true,
inference(step,[status(thm)],[t25,t88]) ).
cnf(t2426,plain,
ifeq(sF0,true,sF0,true) = true,
inference(step,[status(thm)],[t2425,t83]) ).
cnf(t113,plain,
ifeq(sF0,true,sF0,true) = true,
inference(orient,[status(thm)],[t2426]) ).
cnf(t2429,plain,
sF1 = true,
inference(step,[status(thm)],[t2428,t113]) ).
cnf(t114,plain,
true = sF1,
inference(orient,[status(thm)],[t2429]) ).
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(t23,plain,
between(X1,X2,extension(X1,X2,X3,X4)) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t110,plain,
between(X1,X2,extension(X1,X2,X3,X4)) = true,
inference(orient,[status(thm)],[t23]) ).
cnf(t2448,plain,
between(X1,X2,extension(X1,X2,X3,X4)) = sF1,
inference(step,[status(thm)],[t110,t114]) ).
cnf(t136,plain,
between(X1,X2,extension(X1,X2,X3,X4)) = sF1,
inference(orient,[status(thm)],[t2448]) ).
cnf(t21,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t106,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t21]) ).
cnf(t2446,plain,
ifeq(eq(X1,X2),sF1,X1,X2) = X2,
inference(step,[status(thm)],[t106,t114]) ).
cnf(t134,plain,
ifeq(eq(X1,X2),sF1,X1,X2) = X2,
inference(rw,[status(thm)],[t2446]) ).
cnf(t145,plain,
ifeq(eq(X1,X2),sF1,X1,X2) = X2,
inference(orient,[status(thm)],[t134]) ).
cnf(f39,axiom,
( U = V
| extension(U,V,W,X) = extension(U,V,Y,Z)
| ~ equidistant(W,X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_2) ).
fof(f39_nnf,plain,
! [W,X,Y,Z,U,V] :
( U = V
| extension(U,V,W,X) = extension(U,V,Y,Z)
| ~ equidistant(W,X,Y,Z) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [W,X,Y,Z,U,V] :
( U = V
| extension(U,V,W,X) = extension(U,V,Y,Z)
| ~ equidistant(W,X,Y,Z) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( X4 = X5
| extension(X4,X5,X0,X1) = extension(X4,X5,X2,X3)
| ~ equidistant(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(t57,plain,
ifeq(equidistant(X1,X2,X3,X4),true,or(eq(extension(X5,X6,X1,X2),extension(X5,X6,X3,X4)),eq(X5,X6)),true) = true,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(t2650,plain,
ifeq(equidistant(X1,X2,X3,X4),sF1,or(eq(extension(X5,X6,X1,X2),extension(X5,X6,X3,X4)),eq(X5,X6)),true) = true,
inference(step,[status(thm)],[t57,t114]) ).
cnf(t2651,plain,
ifeq(equidistant(X1,X2,X3,X4),sF1,or(eq(extension(X5,X6,X1,X2),extension(X5,X6,X3,X4)),eq(X5,X6)),sF1) = true,
inference(step,[status(thm)],[t2650,t114]) ).
cnf(t2652,plain,
ifeq(equidistant(X1,X2,X3,X4),sF1,or(eq(extension(X5,X6,X1,X2),extension(X5,X6,X3,X4)),eq(X5,X6)),sF1) = sF1,
inference(step,[status(thm)],[t2651,t114]) ).
cnf(t766,plain,
ifeq(equidistant(X1,X2,X3,X4),sF1,or(eq(extension(X5,X6,X1,X2),extension(X5,X6,X3,X4)),eq(X5,X6)),sF1) = sF1,
inference(orient,[status(thm)],[t2652]) ).
cnf(f0,axiom,
equidistant(X,Y,Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_equidistance) ).
fof(f0_nnf,plain,
! [X,Y] : equidistant(X,Y,Y,X),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] : equidistant(X,Y,Y,X),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
equidistant(X0,X1,X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t16,plain,
equidistant(X1,X2,X2,X1) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t100,plain,
equidistant(X1,X2,X2,X1) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(t2444,plain,
equidistant(X1,X2,X2,X1) = sF1,
inference(step,[status(thm)],[t100,t114]) ).
cnf(t131,plain,
equidistant(X1,X2,X2,X1) = sF1,
inference(orient,[status(thm)],[t2444]) ).
cnf(t768,plain,
sF1 = ifeq(sF1,sF1,or(eq(extension(X1,X2,X3,X4),extension(X1,X2,X4,X3)),eq(X1,X2)),sF1),
inference(cp,[status(thm)],[t766,t131]) ).
cnf(t19,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t104,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t19]) ).
cnf(t2779,plain,
sF1 = or(eq(extension(X1,X2,X3,X4),extension(X1,X2,X4,X3)),eq(X1,X2)),
inference(step,[status(thm)],[t768,t104]) ).
cnf(t1854,plain,
or(eq(extension(X1,X2,X3,X4),extension(X1,X2,X4,X3)),eq(X1,X2)) = sF1,
inference(orient,[status(thm)],[t2779]) ).
cnf(f38,axiom,
( W = extension(U,V,V,W)
| U = V
| ~ between(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_1) ).
fof(f38_nnf,plain,
! [U,V,W] :
( W = extension(U,V,V,W)
| U = V
| ~ between(U,V,W) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [U,V,W] :
( W = extension(U,V,V,W)
| U = V
| ~ between(U,V,W) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( X2 = extension(X0,X1,X1,X2)
| X0 = X1
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(t50,plain,
ifeq(between(X1,X2,X3),true,or(eq(X1,X2),eq(X3,extension(X1,X2,X2,X3))),true) = true,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(t2554,plain,
ifeq(between(X1,X2,X3),sF1,or(eq(X1,X2),eq(X3,extension(X1,X2,X2,X3))),true) = true,
inference(step,[status(thm)],[t50,t114]) ).
cnf(t2555,plain,
ifeq(between(X1,X2,X3),sF1,or(eq(X1,X2),eq(X3,extension(X1,X2,X2,X3))),sF1) = true,
inference(step,[status(thm)],[t2554,t114]) ).
cnf(t2556,plain,
ifeq(between(X1,X2,X3),sF1,or(eq(X1,X2),eq(X3,extension(X1,X2,X2,X3))),sF1) = sF1,
inference(step,[status(thm)],[t2555,t114]) ).
cnf(t451,plain,
ifeq(between(X1,X2,X3),sF1,or(eq(X1,X2),eq(X3,extension(X1,X2,X2,X3))),sF1) = sF1,
inference(orient,[status(thm)],[t2556]) ).
cnf(f54,hypothesis,
between(v,w,x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',w_between_v_and_x) ).
fof(f54_nnf,plain,
between(v,w,x),
inference(nnf_transformation,[status(thm)],[f54]) ).
cnf(c54,plain,
between(v,w,x),
inference(cnf_transformation,[status(esa)],[f54_nnf]) ).
cnf(t13,plain,
between(v,w,x) = true,
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(t82,plain,
between(v,w,x) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t2438,plain,
between(v,w,x) = sF1,
inference(step,[status(thm)],[t82,t114]) ).
cnf(t125,plain,
between(v,w,x) = sF1,
inference(orient,[status(thm)],[t2438]) ).
cnf(t458,plain,
sF1 = ifeq(sF1,sF1,or(eq(v,w),eq(x,extension(v,w,w,x))),sF1),
inference(cp,[status(thm)],[t451,t125]) ).
cnf(t2557,plain,
sF1 = or(eq(v,w),eq(x,extension(v,w,w,x))),
inference(step,[status(thm)],[t458,t104]) ).
cnf(f55,hypothesis,
v != w,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v_not_w) ).
fof(f55_nnf,plain,
v != w,
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
v != w,
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c55,plain,
v != w,
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(t1,plain,
eq(v,w) = false,
inference(equality_encoding,[status(esa)],[c55]) ).
cnf(t70,plain,
eq(v,w) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t2410,plain,
eq(v,w) = sF0,
inference(step,[status(thm)],[t70,t83]) ).
cnf(t84,plain,
eq(v,w) = sF0,
inference(orient,[status(thm)],[t2410]) ).
cnf(t2558,plain,
sF1 = or(sF0,eq(x,extension(v,w,w,x))),
inference(step,[status(thm)],[t2557,t84]) ).
cnf(t4,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t73,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t2413,plain,
or(sF0,X1) = X1,
inference(step,[status(thm)],[t73,t83]) ).
cnf(t87,plain,
or(sF0,X1) = X1,
inference(rw,[status(thm)],[t2413]) ).
cnf(t97,plain,
or(sF0,X1) = X1,
inference(orient,[status(thm)],[t87]) ).
cnf(t2559,plain,
sF1 = eq(x,extension(v,w,w,x)),
inference(step,[status(thm)],[t2558,t97]) ).
cnf(t467,plain,
eq(x,extension(v,w,w,x)) = sF1,
inference(orient,[status(thm)],[t2559]) ).
cnf(t468,plain,
extension(v,w,w,x) = ifeq(sF1,sF1,x,extension(v,w,w,x)),
inference(cp,[status(thm)],[t145,t467]) ).
cnf(t2560,plain,
extension(v,w,w,x) = x,
inference(step,[status(thm)],[t468,t104]) ).
cnf(t469,plain,
extension(v,w,w,x) = x,
inference(orient,[status(thm)],[t2560]) ).
cnf(t1859,plain,
sF1 = or(eq(x,extension(v,w,x,w)),eq(v,w)),
inference(cp,[status(thm)],[t1854,t469]) ).
cnf(t2781,plain,
sF1 = or(eq(x,extension(v,w,x,w)),sF0),
inference(step,[status(thm)],[t1859,t84]) ).
cnf(t2,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t71,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t2412,plain,
or(X1,sF0) = X1,
inference(step,[status(thm)],[t71,t83]) ).
cnf(t86,plain,
or(X1,sF0) = X1,
inference(rw,[status(thm)],[t2412]) ).
cnf(t96,plain,
or(X1,sF0) = X1,
inference(orient,[status(thm)],[t86]) ).
cnf(t2782,plain,
sF1 = eq(x,extension(v,w,x,w)),
inference(step,[status(thm)],[t2781,t96]) ).
cnf(t1865,plain,
eq(x,extension(v,w,x,w)) = sF1,
inference(orient,[status(thm)],[t2782]) ).
cnf(t1866,plain,
extension(v,w,x,w) = ifeq(sF1,sF1,x,extension(v,w,x,w)),
inference(cp,[status(thm)],[t145,t1865]) ).
cnf(t2783,plain,
extension(v,w,x,w) = x,
inference(step,[status(thm)],[t1866,t104]) ).
cnf(t1867,plain,
extension(v,w,x,w) = x,
inference(orient,[status(thm)],[t2783]) ).
cnf(t1869,plain,
sF1 = ifeq(equidistant(x,w,X1,X2),sF1,or(eq(x,extension(v,w,X1,X2)),eq(v,w)),sF1),
inference(cp,[status(thm)],[t766,t1867]) ).
cnf(t2806,plain,
sF1 = ifeq(equidistant(x,w,X1,X2),sF1,or(eq(x,extension(v,w,X1,X2)),sF0),sF1),
inference(step,[status(thm)],[t1869,t84]) ).
cnf(t2807,plain,
sF1 = ifeq(equidistant(x,w,X1,X2),sF1,eq(x,extension(v,w,X1,X2)),sF1),
inference(step,[status(thm)],[t2806,t96]) ).
cnf(t2026,plain,
ifeq(equidistant(x,w,X1,X2),sF1,eq(x,extension(v,w,X1,X2)),sF1) = sF1,
inference(orient,[status(thm)],[t2807]) ).
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(t2483,plain,
ifeq(equidistant(X1,X2,X3,X4),sF1,equidistant(X3,X4,X1,X2),true) = true,
inference(step,[status(thm)],[t40,t114]) ).
cnf(t2484,plain,
ifeq(equidistant(X1,X2,X3,X4),sF1,equidistant(X3,X4,X1,X2),sF1) = true,
inference(step,[status(thm)],[t2483,t114]) ).
cnf(t2485,plain,
ifeq(equidistant(X1,X2,X3,X4),sF1,equidistant(X3,X4,X1,X2),sF1) = sF1,
inference(step,[status(thm)],[t2484,t114]) ).
cnf(t232,plain,
ifeq(equidistant(X1,X2,X3,X4),sF1,equidistant(X3,X4,X1,X2),sF1) = sF1,
inference(orient,[status(thm)],[t2485]) ).
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(t2456,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4) = sF1,
inference(step,[status(thm)],[t30,t114]) ).
cnf(t148,plain,
equidistant(X1,extension(X2,X1,X3,X4),X3,X4) = sF1,
inference(orient,[status(thm)],[t2456]) ).
cnf(t233,plain,
sF1 = ifeq(sF1,sF1,equidistant(X1,X2,X3,extension(X4,X3,X1,X2)),sF1),
inference(cp,[status(thm)],[t232,t148]) ).
cnf(t2486,plain,
sF1 = equidistant(X1,X2,X3,extension(X4,X3,X1,X2)),
inference(step,[status(thm)],[t233,t104]) ).
cnf(t237,plain,
equidistant(X1,X2,X3,extension(X4,X3,X1,X2)) = sF1,
inference(orient,[status(thm)],[t2486]) ).
cnf(t2029,plain,
sF1 = ifeq(sF1,sF1,eq(x,extension(v,w,X1,extension(X2,X1,x,w))),sF1),
inference(cp,[status(thm)],[t2026,t237]) ).
cnf(t2808,plain,
sF1 = eq(x,extension(v,w,X1,extension(X2,X1,x,w))),
inference(step,[status(thm)],[t2029,t104]) ).
cnf(t2037,plain,
eq(x,extension(v,w,X1,extension(X2,X1,x,w))) = sF1,
inference(orient,[status(thm)],[t2808]) ).
cnf(f52,axiom,
( between(V,W,X)
| ~ between(U,W,X)
| ~ between(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b5) ).
fof(f52_nnf,plain,
! [U,V,W,X] :
( between(V,W,X)
| ~ between(U,W,X)
| ~ between(U,V,W) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [U,V,W,X] :
( between(V,W,X)
| ~ between(U,W,X)
| ~ between(U,V,W) ),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c52,plain,
( between(X1,X2,X3)
| ~ between(X0,X2,X3)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(t49,plain,
ifeq(between(X1,X2,X3),true,ifeq(between(X1,X3,X4),true,between(X2,X3,X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c52]) ).
cnf(t2540,plain,
ifeq(between(X1,X2,X3),sF1,ifeq(between(X1,X3,X4),true,between(X2,X3,X4),true),true) = true,
inference(step,[status(thm)],[t49,t114]) ).
cnf(t2541,plain,
ifeq(between(X1,X2,X3),sF1,ifeq(between(X1,X3,X4),sF1,between(X2,X3,X4),true),true) = true,
inference(step,[status(thm)],[t2540,t114]) ).
cnf(t2542,plain,
ifeq(between(X1,X2,X3),sF1,ifeq(between(X1,X3,X4),sF1,between(X2,X3,X4),sF1),true) = true,
inference(step,[status(thm)],[t2541,t114]) ).
cnf(t2543,plain,
ifeq(between(X1,X2,X3),sF1,ifeq(between(X1,X3,X4),sF1,between(X2,X3,X4),sF1),sF1) = true,
inference(step,[status(thm)],[t2542,t114]) ).
cnf(t2544,plain,
ifeq(between(X1,X2,X3),sF1,ifeq(between(X1,X3,X4),sF1,between(X2,X3,X4),sF1),sF1) = sF1,
inference(step,[status(thm)],[t2543,t114]) ).
cnf(t381,plain,
ifeq(between(X1,X2,X3),sF1,ifeq(between(X1,X3,X4),sF1,between(X2,X3,X4),sF1),sF1) = sF1,
inference(orient,[status(thm)],[t2544]) ).
cnf(f53,hypothesis,
between(u,v,w),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v_between_u_and_w) ).
fof(f53_nnf,plain,
between(u,v,w),
inference(nnf_transformation,[status(thm)],[f53]) ).
cnf(c53,plain,
between(u,v,w),
inference(cnf_transformation,[status(esa)],[f53_nnf]) ).
cnf(t11,plain,
between(u,v,w) = true,
inference(equality_encoding,[status(esa)],[c53]) ).
cnf(t80,plain,
between(u,v,w) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t2436,plain,
between(u,v,w) = sF1,
inference(step,[status(thm)],[t80,t114]) ).
cnf(t123,plain,
between(u,v,w) = sF1,
inference(orient,[status(thm)],[t2436]) ).
cnf(t393,plain,
sF1 = ifeq(sF1,sF1,ifeq(between(u,w,X1),sF1,between(v,w,X1),sF1),sF1),
inference(cp,[status(thm)],[t381,t123]) ).
cnf(t2547,plain,
sF1 = ifeq(between(u,w,X1),sF1,between(v,w,X1),sF1),
inference(step,[status(thm)],[t393,t104]) ).
cnf(t412,plain,
ifeq(between(u,w,X1),sF1,between(v,w,X1),sF1) = sF1,
inference(orient,[status(thm)],[t2547]) ).
cnf(t413,plain,
sF1 = ifeq(sF1,sF1,between(v,w,extension(u,w,X1,X2)),sF1),
inference(cp,[status(thm)],[t412,t136]) ).
cnf(t2548,plain,
sF1 = between(v,w,extension(u,w,X1,X2)),
inference(step,[status(thm)],[t413,t104]) ).
cnf(t414,plain,
between(v,w,extension(u,w,X1,X2)) = sF1,
inference(orient,[status(thm)],[t2548]) ).
cnf(t463,plain,
sF1 = ifeq(sF1,sF1,or(eq(v,w),eq(extension(u,w,X1,X2),extension(v,w,w,extension(u,w,X1,X2)))),sF1),
inference(cp,[status(thm)],[t451,t414]) ).
cnf(t2762,plain,
sF1 = or(eq(v,w),eq(extension(u,w,X1,X2),extension(v,w,w,extension(u,w,X1,X2)))),
inference(step,[status(thm)],[t463,t104]) ).
cnf(t2763,plain,
sF1 = or(sF0,eq(extension(u,w,X1,X2),extension(v,w,w,extension(u,w,X1,X2)))),
inference(step,[status(thm)],[t2762,t84]) ).
cnf(t2764,plain,
sF1 = eq(extension(u,w,X1,X2),extension(v,w,w,extension(u,w,X1,X2))),
inference(step,[status(thm)],[t2763,t97]) ).
cnf(t1818,plain,
eq(extension(u,w,X1,X2),extension(v,w,w,extension(u,w,X1,X2))) = sF1,
inference(orient,[status(thm)],[t2764]) ).
cnf(t1819,plain,
extension(v,w,w,extension(u,w,X1,X2)) = ifeq(sF1,sF1,extension(u,w,X1,X2),extension(v,w,w,extension(u,w,X1,X2))),
inference(cp,[status(thm)],[t145,t1818]) ).
cnf(t2765,plain,
extension(v,w,w,extension(u,w,X1,X2)) = extension(u,w,X1,X2),
inference(step,[status(thm)],[t1819,t104]) ).
cnf(t1820,plain,
extension(v,w,w,extension(u,w,X1,X2)) = extension(u,w,X1,X2),
inference(orient,[status(thm)],[t2765]) ).
cnf(t2038,plain,
sF1 = eq(x,extension(u,w,x,w)),
inference(cp,[status(thm)],[t2037,t1820]) ).
cnf(t2041,plain,
eq(x,extension(u,w,x,w)) = sF1,
inference(orient,[status(thm)],[t2038]) ).
cnf(t2042,plain,
extension(u,w,x,w) = ifeq(sF1,sF1,x,extension(u,w,x,w)),
inference(cp,[status(thm)],[t145,t2041]) ).
cnf(t2809,plain,
extension(u,w,x,w) = x,
inference(step,[status(thm)],[t2042,t104]) ).
cnf(t2043,plain,
extension(u,w,x,w) = x,
inference(orient,[status(thm)],[t2809]) ).
cnf(t2045,plain,
sF1 = between(u,w,x),
inference(cp,[status(thm)],[t136,t2043]) ).
cnf(t2810,plain,
sF1 = sF0,
inference(step,[status(thm)],[t2045,t94]) ).
cnf(t2067,plain,
sF1 = sF0,
inference(orient,[status(thm)],[t2810]) ).
cnf(t2829,plain,
true = sF0,
inference(step,[status(thm)],[t114,t2067]) ).
cnf(t2086,plain,
true = sF0,
inference(orient,[status(thm)],[t2829]) ).
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(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c9,c10,c11,c55,c56]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t2086]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t83]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO044-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 : n019.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:33:19 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.50/1.50 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.50/1.50 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------