%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO008-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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:30 PM UTC 2026
% Result : Unsatisfiable 160.13s 23.53s
% Output : Proof 160.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 14
% Syntax : Number of formulae : 128 ( 112 unt; 0 def)
% Number of atoms : 152 ( 86 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 66 ( 42 ~; 24 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-5 aty)
% Number of variables : 196 ( 17 sgn 46 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f7,axiom,
( between(Z,W,outer_pasch(W,X,Y,Z,V))
| ~ between(Y,V,Z)
| ~ between(X,W,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outer_pasch2) ).
fof(f7_nnf,plain,
! [X,W,V,Y,Z] :
( between(Z,W,outer_pasch(W,X,Y,Z,V))
| ~ between(Y,V,Z)
| ~ between(X,W,V) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,W,V,Y,Z] :
( between(Z,W,outer_pasch(W,X,Y,Z,V))
| ~ between(Y,V,Z)
| ~ between(X,W,V) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( between(X4,X1,outer_pasch(X1,X0,X3,X4,X2))
| ~ between(X3,X2,X4)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t211,plain,
ifeq(between(X1,X2,X3),true,ifeq(between(X4,X3,X5),true,between(X5,X2,outer_pasch(X2,X1,X4,X5,X3)),true),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t411,plain,
ifeq(between(X1,X2,X3),true,ifeq(between(X4,X3,X5),true,between(X5,X2,outer_pasch(X2,X1,X4,X5,X3)),true),true) = true,
inference(orient,[status(thm)],[t211]) ).
cnf(hi7,axiom,
ifeq(between(X0,X1,X2),true,ifeq(between(X3,X2,X4),true,between(X4,X1,outer_pasch(X1,X0,X3,X4,X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(f22,hypothesis,
between(c,b,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_between_c_and_d) ).
fof(f22_nnf,plain,
between(c,b,d),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
between(c,b,d),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(hi19,axiom,
between(c,b,d) = true,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(f21,hypothesis,
between(a,d,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_between_a_and_e) ).
fof(f21_nnf,plain,
between(a,d,e),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
between(a,d,e),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(hi18,axiom,
between(a,d,e) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t38,plain,
between(e,b,outer_pasch(b,c,a,e,d)) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi19,hi18]) ).
cnf(t306,plain,
between(e,b,outer_pasch(b,c,a,e,d)) = true,
inference(orient,[status(thm)],[t38]) ).
cnf(t438,plain,
true = ifeq(true,true,ifeq(between(X1,outer_pasch(b,c,a,e,d),X2),true,between(X2,b,outer_pasch(b,e,X1,X2,outer_pasch(b,c,a,e,d))),true),true),
inference(cp,[status(thm)],[t411,t306]) ).
cnf(t17,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t266,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t17]) ).
cnf(t96568,plain,
true = ifeq(between(X1,outer_pasch(b,c,a,e,d),X2),true,between(X2,b,outer_pasch(b,e,X1,X2,outer_pasch(b,c,a,e,d))),true),
inference(step,[status(thm)],[t438,t266]) ).
cnf(t29586,plain,
ifeq(between(X1,outer_pasch(b,c,a,e,d),X2),true,between(X2,b,outer_pasch(b,e,X1,X2,outer_pasch(b,c,a,e,d))),true) = true,
inference(orient,[status(thm)],[t96568]) ).
cnf(f0,axiom,
( X = Y
| ~ between(X,Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_for_betweeness) ).
fof(f0_nnf,plain,
! [X,Y] :
( X = Y
| ~ between(X,Y,X) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] :
( X = Y
| ~ between(X,Y,X) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( X0 = X1
| ~ between(X0,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t22,plain,
ifeq(between(X1,X2,X1),true,X1,X2) = X2,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t267,plain,
ifeq(between(X1,X2,X1),true,X1,X2) = X2,
inference(orient,[status(thm)],[t22]) ).
cnf(f6,axiom,
( between(X,outer_pasch(W,X,Y,Z,V),Y)
| ~ between(Y,V,Z)
| ~ between(X,W,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',outer_pasch1) ).
fof(f6_nnf,plain,
! [X,W,V,Y,Z] :
( between(X,outer_pasch(W,X,Y,Z,V),Y)
| ~ between(Y,V,Z)
| ~ between(X,W,V) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,W,V,Y,Z] :
( between(X,outer_pasch(W,X,Y,Z,V),Y)
| ~ between(Y,V,Z)
| ~ between(X,W,V) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( between(X0,outer_pasch(X1,X0,X3,X4,X2),X3)
| ~ between(X3,X2,X4)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t210,plain,
ifeq(between(X1,X2,X3),true,ifeq(between(X4,X3,X5),true,between(X1,outer_pasch(X2,X1,X4,X5,X3),X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t527,plain,
ifeq(between(X1,X2,X3),true,ifeq(between(X4,X3,X5),true,between(X1,outer_pasch(X2,X1,X4,X5,X3),X4),true),true) = true,
inference(orient,[status(thm)],[t210]) ).
cnf(t554,plain,
true = ifeq(true,true,ifeq(between(X1,outer_pasch(b,c,a,e,d),X2),true,between(e,outer_pasch(b,e,X1,X2,outer_pasch(b,c,a,e,d)),X1),true),true),
inference(cp,[status(thm)],[t527,t306]) ).
cnf(t98592,plain,
true = ifeq(between(X1,outer_pasch(b,c,a,e,d),X2),true,between(e,outer_pasch(b,e,X1,X2,outer_pasch(b,c,a,e,d)),X1),true),
inference(step,[status(thm)],[t554,t266]) ).
cnf(t92271,plain,
ifeq(between(X1,outer_pasch(b,c,a,e,d),X2),true,between(e,outer_pasch(b,e,X1,X2,outer_pasch(b,c,a,e,d)),X1),true) = true,
inference(orient,[status(thm)],[t98592]) ).
cnf(f20,hypothesis,
between(a,c,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_between_a_and_e) ).
fof(f20_nnf,plain,
between(a,c,e),
inference(nnf_transformation,[status(thm)],[f20]) ).
cnf(c20,plain,
between(a,c,e),
inference(cnf_transformation,[status(esa)],[f20_nnf]) ).
cnf(t7,plain,
between(a,c,e) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t315,plain,
between(a,c,e) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t484,plain,
true = ifeq(between(X1,X2,c),true,ifeq(true,true,between(e,X2,outer_pasch(X2,X1,a,e,c)),true),true),
inference(cp,[status(thm)],[t411,t315]) ).
cnf(t95475,plain,
true = ifeq(between(X1,X2,c),true,between(e,X2,outer_pasch(X2,X1,a,e,c)),true),
inference(step,[status(thm)],[t484,t266]) ).
cnf(t5684,plain,
ifeq(between(X1,X2,c),true,between(e,X2,outer_pasch(X2,X1,a,e,c)),true) = true,
inference(orient,[status(thm)],[t95475]) ).
cnf(t600,plain,
true = ifeq(between(X1,X2,c),true,ifeq(true,true,between(X1,outer_pasch(X2,X1,a,e,c),a),true),true),
inference(cp,[status(thm)],[t527,t315]) ).
cnf(t95556,plain,
true = ifeq(between(X1,X2,c),true,between(X1,outer_pasch(X2,X1,a,e,c),a),true),
inference(step,[status(thm)],[t600,t266]) ).
cnf(t7814,plain,
ifeq(between(X1,X2,c),true,between(X1,outer_pasch(X2,X1,a,e,c),a),true) = true,
inference(orient,[status(thm)],[t95556]) ).
cnf(f12,axiom,
between(X,Y,extension(X,Y,W,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',segment_construction1) ).
fof(f12_nnf,plain,
! [X,Y,W,V] : between(X,Y,extension(X,Y,W,V)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X,Y,W,V] : between(X,Y,extension(X,Y,W,V)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
between(X0,X1,extension(X0,X1,X2,X3)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t21,plain,
between(X1,X2,extension(X1,X2,X3,X4)) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t272,plain,
between(X1,X2,extension(X1,X2,X3,X4)) = true,
inference(orient,[status(thm)],[t21]) ).
cnf(f4,axiom,
( X = Y
| ~ equidistant(X,Y,Z,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_for_equidistance) ).
fof(f4_nnf,plain,
! [X,Y,Z] :
( X = Y
| ~ equidistant(X,Y,Z,Z) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y,Z] :
( X = Y
| ~ equidistant(X,Y,Z,Z) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( X0 = X1
| ~ equidistant(X0,X1,X2,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi4,axiom,
ifeq(equidistant(X0,X1,X2,X2),true,X0,X1) = X1,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(f13,axiom,
equidistant(Y,extension(X,Y,W,V),W,V),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',segment_construction2) ).
fof(f13_nnf,plain,
! [Y,X,W,V] : equidistant(Y,extension(X,Y,W,V),W,V),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [Y,X,W,V] : equidistant(Y,extension(X,Y,W,V),W,V),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
equidistant(X0,extension(X1,X0,X2,X3),X2,X3),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi13,axiom,
equidistant(X0,extension(X1,X0,X2,X3),X2,X3) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t16,plain,
extension(X1,X2,X3,X3) = X2,
inference(hyper_resolution,[status(thm)],[hi4,hi13]) ).
cnf(t256,plain,
extension(X1,X2,X3,X3) = X2,
inference(orient,[status(thm)],[t16]) ).
cnf(t273,plain,
true = between(X1,X2,X2),
inference(cp,[status(thm)],[t272,t256]) ).
cnf(t2482,plain,
between(X1,X2,X2) = true,
inference(orient,[status(thm)],[t273]) ).
cnf(t2487,plain,
true = ifeq(between(X1,X2,X3),true,ifeq(true,true,between(X1,outer_pasch(X2,X1,X4,X3,X3),X4),true),true),
inference(cp,[status(thm)],[t527,t2482]) ).
cnf(t96150,plain,
true = ifeq(between(X1,X2,X3),true,between(X1,outer_pasch(X2,X1,X4,X3,X3),X4),true),
inference(step,[status(thm)],[t2487,t266]) ).
cnf(t19671,plain,
ifeq(between(X1,X2,X3),true,between(X1,outer_pasch(X2,X1,X4,X3,X3),X4),true) = true,
inference(orient,[status(thm)],[t96150]) ).
cnf(hi6,axiom,
ifeq(between(X0,X1,X2),true,ifeq(between(X3,X2,X4),true,between(X0,outer_pasch(X1,X0,X3,X4,X2),X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t32,plain,
between(c,outer_pasch(b,c,a,e,d),a) = true,
inference(hyper_resolution,[status(thm)],[hi6,hi19,hi18]) ).
cnf(t295,plain,
between(c,outer_pasch(b,c,a,e,d),a) = true,
inference(orient,[status(thm)],[t32]) ).
cnf(t20150,plain,
true = ifeq(true,true,between(c,outer_pasch(outer_pasch(b,c,a,e,d),c,X1,a,a),X1),true),
inference(cp,[status(thm)],[t19671,t295]) ).
cnf(t96496,plain,
true = between(c,outer_pasch(outer_pasch(b,c,a,e,d),c,X1,a,a),X1),
inference(step,[status(thm)],[t20150,t266]) ).
cnf(t28072,plain,
between(c,outer_pasch(outer_pasch(b,c,a,e,d),c,X1,a,a),X1) = true,
inference(orient,[status(thm)],[t96496]) ).
cnf(t28075,plain,
outer_pasch(outer_pasch(b,c,a,e,d),c,c,a,a) = ifeq(true,true,c,outer_pasch(outer_pasch(b,c,a,e,d),c,c,a,a)),
inference(cp,[status(thm)],[t267,t28072]) ).
cnf(t96497,plain,
outer_pasch(outer_pasch(b,c,a,e,d),c,c,a,a) = c,
inference(step,[status(thm)],[t28075,t266]) ).
cnf(t28111,plain,
outer_pasch(outer_pasch(b,c,a,e,d),c,c,a,a) = c,
inference(orient,[status(thm)],[t96497]) ).
cnf(t28112,plain,
true = ifeq(between(c,outer_pasch(b,c,a,e,d),a),true,ifeq(between(c,a,a),true,between(a,outer_pasch(b,c,a,e,d),c),true),true),
inference(cp,[status(thm)],[t411,t28111]) ).
cnf(t96499,plain,
true = ifeq(true,true,ifeq(between(c,a,a),true,between(a,outer_pasch(b,c,a,e,d),c),true),true),
inference(step,[status(thm)],[t28112,t295]) ).
cnf(t96500,plain,
true = ifeq(between(c,a,a),true,between(a,outer_pasch(b,c,a,e,d),c),true),
inference(step,[status(thm)],[t96499,t266]) ).
cnf(t96501,plain,
true = ifeq(true,true,between(a,outer_pasch(b,c,a,e,d),c),true),
inference(step,[status(thm)],[t96500,t2482]) ).
cnf(t96502,plain,
true = between(a,outer_pasch(b,c,a,e,d),c),
inference(step,[status(thm)],[t96501,t266]) ).
cnf(t28219,plain,
between(a,outer_pasch(b,c,a,e,d),c) = true,
inference(orient,[status(thm)],[t96502]) ).
cnf(t28222,plain,
true = ifeq(true,true,between(a,outer_pasch(outer_pasch(b,c,a,e,d),a,a,e,c),a),true),
inference(cp,[status(thm)],[t7814,t28219]) ).
cnf(t97014,plain,
true = between(a,outer_pasch(outer_pasch(b,c,a,e,d),a,a,e,c),a),
inference(step,[status(thm)],[t28222,t266]) ).
cnf(t38423,plain,
between(a,outer_pasch(outer_pasch(b,c,a,e,d),a,a,e,c),a) = true,
inference(orient,[status(thm)],[t97014]) ).
cnf(t38425,plain,
outer_pasch(outer_pasch(b,c,a,e,d),a,a,e,c) = ifeq(true,true,a,outer_pasch(outer_pasch(b,c,a,e,d),a,a,e,c)),
inference(cp,[status(thm)],[t267,t38423]) ).
cnf(t97015,plain,
outer_pasch(outer_pasch(b,c,a,e,d),a,a,e,c) = a,
inference(step,[status(thm)],[t38425,t266]) ).
cnf(t38450,plain,
outer_pasch(outer_pasch(b,c,a,e,d),a,a,e,c) = a,
inference(orient,[status(thm)],[t97015]) ).
cnf(t38451,plain,
true = ifeq(between(a,outer_pasch(b,c,a,e,d),c),true,between(e,outer_pasch(b,c,a,e,d),a),true),
inference(cp,[status(thm)],[t5684,t38450]) ).
cnf(t97016,plain,
true = ifeq(true,true,between(e,outer_pasch(b,c,a,e,d),a),true),
inference(step,[status(thm)],[t38451,t28219]) ).
cnf(t97017,plain,
true = between(e,outer_pasch(b,c,a,e,d),a),
inference(step,[status(thm)],[t97016,t266]) ).
cnf(t38453,plain,
between(e,outer_pasch(b,c,a,e,d),a) = true,
inference(orient,[status(thm)],[t97017]) ).
cnf(t92329,plain,
true = ifeq(true,true,between(e,outer_pasch(b,e,e,a,outer_pasch(b,c,a,e,d)),e),true),
inference(cp,[status(thm)],[t92271,t38453]) ).
cnf(t98731,plain,
true = between(e,outer_pasch(b,e,e,a,outer_pasch(b,c,a,e,d)),e),
inference(step,[status(thm)],[t92329,t266]) ).
cnf(t95161,plain,
between(e,outer_pasch(b,e,e,a,outer_pasch(b,c,a,e,d)),e) = true,
inference(orient,[status(thm)],[t98731]) ).
cnf(t95163,plain,
outer_pasch(b,e,e,a,outer_pasch(b,c,a,e,d)) = ifeq(true,true,e,outer_pasch(b,e,e,a,outer_pasch(b,c,a,e,d))),
inference(cp,[status(thm)],[t267,t95161]) ).
cnf(t98732,plain,
outer_pasch(b,e,e,a,outer_pasch(b,c,a,e,d)) = e,
inference(step,[status(thm)],[t95163,t266]) ).
cnf(t95191,plain,
outer_pasch(b,e,e,a,outer_pasch(b,c,a,e,d)) = e,
inference(orient,[status(thm)],[t98732]) ).
cnf(t95192,plain,
true = ifeq(between(e,outer_pasch(b,c,a,e,d),a),true,between(a,b,e),true),
inference(cp,[status(thm)],[t29586,t95191]) ).
cnf(t98735,plain,
true = ifeq(true,true,between(a,b,e),true),
inference(step,[status(thm)],[t95192,t38453]) ).
cnf(t98736,plain,
true = between(a,b,e),
inference(step,[status(thm)],[t98735,t266]) ).
cnf(f23,negated_conjecture,
~ between(a,b,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_betweenness) ).
fof(f23_nnf,plain,
~ between(a,b,e),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
~ between(a,b,e),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
~ between(a,b,e),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t6,plain,
between(a,b,e) = false,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t2370,plain,
between(a,b,e) = false,
inference(orient,[status(thm)],[t6]) ).
cnf(t98737,plain,
true = false,
inference(step,[status(thm)],[t98736,t2370]) ).
cnf(t95195,plain,
false = true,
inference(orient,[status(thm)],[t98737]) ).
cnf(f14,axiom,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lower_dimension1) ).
fof(f14_nnf,plain,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
~ between(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f15,axiom,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lower_dimension2) ).
fof(f15_nnf,plain,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
~ between(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(f16,axiom,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lower_dimension3) ).
fof(f16_nnf,plain,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
~ between(lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c14,c15,c16,c23]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t95195]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO008-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.38 % Computer : n005.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Wed Sep 23 10:20:33 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 160.13/23.53 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 160.13/23.53 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------