%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO067-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 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:55 PM UTC 2026
% Result : Unsatisfiable 9.35s 1.69s
% Output : Proof 9.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 22
% Syntax : Number of formulae : 158 ( 138 unt; 0 def)
% Number of atoms : 194 ( 117 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 111 ( 75 ~; 36 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 12 con; 0-4 aty)
% Number of variables : 141 ( 25 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f18,axiom,
( colinear(X,Y,Z)
| ~ between(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',colinearity1) ).
fof(f18_nnf,plain,
! [X,Y,Z] :
( colinear(X,Y,Z)
| ~ between(X,Y,Z) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X,Y,Z] :
( colinear(X,Y,Z)
| ~ between(X,Y,Z) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( colinear(X0,X1,X2)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t42,plain,
ifeq(between(X1,X2,X3),true,colinear(X1,X2,X3),true) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t210,plain,
ifeq(between(X1,X2,X3),true,colinear(X1,X2,X3),true) = true,
inference(orient,[status(thm)],[t42]) ).
cnf(t114,axiom,
sF0 = colinear(x,x,y),
introduced(definition) ).
cnf(t148,plain,
colinear(x,x,y) = sF0,
inference(orient,[status(thm)],[t114]) ).
cnf(t215,plain,
true = ifeq(between(x,x,y),true,sF0,true),
inference(cp,[status(thm)],[t210,t148]) ).
cnf(f51,axiom,
between(U,U,V),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2) ).
fof(f51_nnf,plain,
! [U,V] : between(U,U,V),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
! [U,V] : between(U,U,V),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
between(X0,X0,X1),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(t10,plain,
between(X1,X1,X2) = true,
inference(equality_encoding,[status(esa)],[c51]) ).
cnf(t142,plain,
between(X1,X1,X2) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t1676,plain,
true = ifeq(true,true,sF0,true),
inference(step,[status(thm)],[t215,t142]) ).
cnf(t21,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t158,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t21]) ).
cnf(t1677,plain,
true = sF0,
inference(step,[status(thm)],[t1676,t158]) ).
cnf(t220,plain,
true = sF0,
inference(orient,[status(thm)],[t1677]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t133,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t223,plain,
not(sF0) = false,
inference(rw,[status(thm)],[t133]) ).
cnf(t120,axiom,
sF6 = not(colinear(x,x,y)),
introduced(definition) ).
cnf(t1667,plain,
sF6 = not(sF0),
inference(step,[status(thm)],[t120,t148]) ).
cnf(t162,plain,
not(sF0) = sF6,
inference(orient,[status(thm)],[t1667]) ).
cnf(t1713,plain,
sF6 = false,
inference(step,[status(thm)],[t223,t162]) ).
cnf(t264,plain,
false = sF6,
inference(orient,[status(thm)],[t1713]) ).
cnf(f97,negated_conjecture,
( ~ colinear(x,z,y)
| ~ colinear(y,x,x)
| ~ colinear(x,y,x)
| ~ colinear(x,x,y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',part_2) ).
fof(f97_nnf,plain,
( ~ colinear(x,z,y)
| ~ colinear(y,x,x)
| ~ colinear(x,y,x)
| ~ colinear(x,x,y) ),
inference(nnf_transformation,[status(thm)],[f97]) ).
fof(f97_sk,plain,
( ~ colinear(x,z,y)
| ~ colinear(y,x,x)
| ~ colinear(x,y,x)
| ~ colinear(x,x,y) ),
inference(skolemisation,[status(esa)],[f97_nnf]) ).
cnf(c97,plain,
( ~ colinear(x,z,y)
| ~ colinear(y,x,x)
| ~ colinear(x,y,x)
| ~ colinear(x,x,y) ),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
cnf(t88,plain,
or(not(colinear(x,x,y)),or(not(colinear(x,y,x)),or(not(colinear(y,x,x)),not(colinear(x,z,y))))) = true,
inference(equality_encoding,[status(esa)],[c97]) ).
cnf(f89,axiom,
( colinear(U,V,W)
| ~ between(V,U,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c2_3) ).
fof(f89_nnf,plain,
! [V,U,W] :
( colinear(U,V,W)
| ~ between(V,U,W) ),
inference(nnf_transformation,[status(thm)],[f89]) ).
fof(f89_sk,plain,
! [V,U,W] :
( colinear(U,V,W)
| ~ between(V,U,W) ),
inference(skolemisation,[status(esa)],[f89_nnf]) ).
cnf(c89,plain,
( colinear(X1,X0,X2)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f89_sk]) ).
cnf(t44,plain,
ifeq(between(X1,X2,X3),true,colinear(X2,X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c89]) ).
cnf(t1761,plain,
ifeq(between(X1,X2,X3),sF0,colinear(X2,X1,X3),true) = true,
inference(step,[status(thm)],[t44,t220]) ).
cnf(t1762,plain,
ifeq(between(X1,X2,X3),sF0,colinear(X2,X1,X3),sF0) = true,
inference(step,[status(thm)],[t1761,t220]) ).
cnf(t1763,plain,
ifeq(between(X1,X2,X3),sF0,colinear(X2,X1,X3),sF0) = sF0,
inference(step,[status(thm)],[t1762,t220]) ).
cnf(t319,plain,
ifeq(between(X1,X2,X3),sF0,colinear(X2,X1,X3),sF0) = sF0,
inference(orient,[status(thm)],[t1763]) ).
cnf(t1682,plain,
between(X1,X1,X2) = sF0,
inference(step,[status(thm)],[t142,t220]) ).
cnf(t228,plain,
between(X1,X1,X2) = sF0,
inference(orient,[status(thm)],[t1682]) ).
cnf(t320,plain,
sF0 = ifeq(sF0,sF0,colinear(X1,X1,X2),sF0),
inference(cp,[status(thm)],[t319,t228]) ).
cnf(t1764,plain,
sF0 = colinear(X1,X1,X2),
inference(step,[status(thm)],[t320,t158]) ).
cnf(t325,plain,
colinear(X1,X1,X2) = sF0,
inference(orient,[status(thm)],[t1764]) ).
cnf(t2122,plain,
or(not(sF0),or(not(colinear(x,y,x)),or(not(colinear(y,x,x)),not(colinear(x,z,y))))) = true,
inference(step,[status(thm)],[t88,t325]) ).
cnf(t2123,plain,
or(sF6,or(not(colinear(x,y,x)),or(not(colinear(y,x,x)),not(colinear(x,z,y))))) = true,
inference(step,[status(thm)],[t2122,t162]) ).
cnf(t8,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t140,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t1722,plain,
or(sF6,X1) = X1,
inference(step,[status(thm)],[t140,t264]) ).
cnf(t273,plain,
or(sF6,X1) = X1,
inference(rw,[status(thm)],[t1722]) ).
cnf(t288,plain,
or(sF6,X1) = X1,
inference(orient,[status(thm)],[t273]) ).
cnf(t2124,plain,
or(not(colinear(x,y,x)),or(not(colinear(y,x,x)),not(colinear(x,z,y)))) = true,
inference(step,[status(thm)],[t2123,t288]) ).
cnf(f88,axiom,
( colinear(U,V,W)
| ~ between(U,W,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c2_2) ).
fof(f88_nnf,plain,
! [U,W,V] :
( colinear(U,V,W)
| ~ between(U,W,V) ),
inference(nnf_transformation,[status(thm)],[f88]) ).
fof(f88_sk,plain,
! [U,W,V] :
( colinear(U,V,W)
| ~ between(U,W,V) ),
inference(skolemisation,[status(esa)],[f88_nnf]) ).
cnf(c88,plain,
( colinear(X0,X2,X1)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f88_sk]) ).
cnf(t43,plain,
ifeq(between(X1,X2,X3),true,colinear(X1,X3,X2),true) = true,
inference(equality_encoding,[status(esa)],[c88]) ).
cnf(t1741,plain,
ifeq(between(X1,X2,X3),sF0,colinear(X1,X3,X2),true) = true,
inference(step,[status(thm)],[t43,t220]) ).
cnf(t1742,plain,
ifeq(between(X1,X2,X3),sF0,colinear(X1,X3,X2),sF0) = true,
inference(step,[status(thm)],[t1741,t220]) ).
cnf(t1743,plain,
ifeq(between(X1,X2,X3),sF0,colinear(X1,X3,X2),sF0) = sF0,
inference(step,[status(thm)],[t1742,t220]) ).
cnf(t292,plain,
ifeq(between(X1,X2,X3),sF0,colinear(X1,X3,X2),sF0) = sF0,
inference(orient,[status(thm)],[t1743]) ).
cnf(t293,plain,
sF0 = ifeq(sF0,sF0,colinear(X1,X2,X1),sF0),
inference(cp,[status(thm)],[t292,t228]) ).
cnf(t1754,plain,
sF0 = colinear(X1,X2,X1),
inference(step,[status(thm)],[t293,t158]) ).
cnf(t314,plain,
colinear(X1,X2,X1) = sF0,
inference(orient,[status(thm)],[t1754]) ).
cnf(t2125,plain,
or(not(sF0),or(not(colinear(y,x,x)),not(colinear(x,z,y)))) = true,
inference(step,[status(thm)],[t2124,t314]) ).
cnf(t2126,plain,
or(sF6,or(not(colinear(y,x,x)),not(colinear(x,z,y)))) = true,
inference(step,[status(thm)],[t2125,t162]) ).
cnf(t2127,plain,
or(not(colinear(y,x,x)),not(colinear(x,z,y))) = true,
inference(step,[status(thm)],[t2126,t288]) ).
cnf(f48,axiom,
between(U,V,V),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3) ).
fof(f48_nnf,plain,
! [U,V] : between(U,V,V),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [U,V] : between(U,V,V),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c48,plain,
between(X0,X1,X1),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(t11,plain,
between(X1,X2,X2) = true,
inference(equality_encoding,[status(esa)],[c48]) ).
cnf(t143,plain,
between(X1,X2,X2) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t1684,plain,
between(X1,X2,X2) = sF0,
inference(step,[status(thm)],[t143,t220]) ).
cnf(t230,plain,
between(X1,X2,X2) = sF0,
inference(orient,[status(thm)],[t1684]) ).
cnf(t294,plain,
sF0 = ifeq(sF0,sF0,colinear(X1,X2,X2),sF0),
inference(cp,[status(thm)],[t292,t230]) ).
cnf(t1756,plain,
sF0 = colinear(X1,X2,X2),
inference(step,[status(thm)],[t294,t158]) ).
cnf(t316,plain,
colinear(X1,X2,X2) = sF0,
inference(orient,[status(thm)],[t1756]) ).
cnf(t2128,plain,
or(not(sF0),not(colinear(x,z,y))) = true,
inference(step,[status(thm)],[t2127,t316]) ).
cnf(t2129,plain,
or(sF6,not(colinear(x,z,y))) = true,
inference(step,[status(thm)],[t2128,t162]) ).
cnf(t2130,plain,
not(colinear(x,z,y)) = true,
inference(step,[status(thm)],[t2129,t288]) ).
cnf(t117,axiom,
sF3 = ifeq(colinear(y,x,x),true,x,y),
introduced(definition) ).
cnf(t116,axiom,
sF2 = colinear(y,x,x),
introduced(definition) ).
cnf(t150,plain,
colinear(y,x,x) = sF2,
inference(orient,[status(thm)],[t116]) ).
cnf(t1673,plain,
sF3 = ifeq(sF2,true,x,y),
inference(step,[status(thm)],[t117,t150]) ).
cnf(t192,plain,
ifeq(sF2,true,x,y) = sF3,
inference(orient,[status(thm)],[t1673]) ).
cnf(t1706,plain,
ifeq(sF2,sF0,x,y) = sF3,
inference(step,[status(thm)],[t192,t220]) ).
cnf(t255,plain,
ifeq(sF2,sF0,x,y) = sF3,
inference(rw,[status(thm)],[t1706]) ).
cnf(t301,plain,
sF0 = ifeq(between(y,x,x),sF0,sF2,sF0),
inference(cp,[status(thm)],[t292,t150]) ).
cnf(t1748,plain,
sF0 = ifeq(sF0,sF0,sF2,sF0),
inference(step,[status(thm)],[t301,t230]) ).
cnf(t1749,plain,
sF0 = sF2,
inference(step,[status(thm)],[t1748,t158]) ).
cnf(t308,plain,
sF2 = sF0,
inference(orient,[status(thm)],[t1749]) ).
cnf(t1774,plain,
ifeq(sF0,sF0,x,y) = sF3,
inference(step,[status(thm)],[t255,t308]) ).
cnf(t1775,plain,
x = sF3,
inference(step,[status(thm)],[t1774,t158]) ).
cnf(t332,plain,
x = sF3,
inference(orient,[status(thm)],[t1775]) ).
cnf(t2131,plain,
not(colinear(sF3,z,y)) = true,
inference(step,[status(thm)],[t2130,t332]) ).
cnf(f96,negated_conjecture,
( x = y
| ~ colinear(y,x,x)
| ~ colinear(x,y,x)
| ~ colinear(x,x,y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',part_1) ).
fof(f96_nnf,plain,
( x = y
| ~ colinear(y,x,x)
| ~ colinear(x,y,x)
| ~ colinear(x,x,y) ),
inference(nnf_transformation,[status(thm)],[f96]) ).
fof(f96_sk,plain,
( x = y
| ~ colinear(y,x,x)
| ~ colinear(x,y,x)
| ~ colinear(x,x,y) ),
inference(skolemisation,[status(esa)],[f96_nnf]) ).
cnf(c96,plain,
( x = y
| ~ colinear(y,x,x)
| ~ colinear(x,y,x)
| ~ colinear(x,x,y) ),
inference(cnf_transformation,[status(esa)],[f96_sk]) ).
cnf(t82,plain,
ifeq(colinear(x,x,y),true,ifeq(colinear(x,y,x),true,ifeq(colinear(y,x,x),true,x,y),y),y) = y,
inference(equality_encoding,[status(esa)],[c96]) ).
cnf(t2047,plain,
ifeq(sF0,true,ifeq(colinear(x,y,x),true,ifeq(colinear(y,x,x),true,x,y),y),y) = y,
inference(step,[status(thm)],[t82,t325]) ).
cnf(t2048,plain,
ifeq(sF0,sF0,ifeq(colinear(x,y,x),true,ifeq(colinear(y,x,x),true,x,y),y),y) = y,
inference(step,[status(thm)],[t2047,t220]) ).
cnf(t2049,plain,
ifeq(colinear(x,y,x),true,ifeq(colinear(y,x,x),true,x,y),y) = y,
inference(step,[status(thm)],[t2048,t158]) ).
cnf(t2050,plain,
ifeq(sF0,true,ifeq(colinear(y,x,x),true,x,y),y) = y,
inference(step,[status(thm)],[t2049,t314]) ).
cnf(t2051,plain,
ifeq(sF0,sF0,ifeq(colinear(y,x,x),true,x,y),y) = y,
inference(step,[status(thm)],[t2050,t220]) ).
cnf(t2052,plain,
ifeq(colinear(y,x,x),true,x,y) = y,
inference(step,[status(thm)],[t2051,t158]) ).
cnf(t2053,plain,
ifeq(sF0,true,x,y) = y,
inference(step,[status(thm)],[t2052,t316]) ).
cnf(t2054,plain,
ifeq(sF0,sF0,x,y) = y,
inference(step,[status(thm)],[t2053,t220]) ).
cnf(t2055,plain,
x = y,
inference(step,[status(thm)],[t2054,t158]) ).
cnf(t2056,plain,
sF3 = y,
inference(step,[status(thm)],[t2055,t332]) ).
cnf(t1228,plain,
y = sF3,
inference(orient,[status(thm)],[t2056]) ).
cnf(t2132,plain,
not(colinear(sF3,z,sF3)) = true,
inference(step,[status(thm)],[t2131,t1228]) ).
cnf(t2133,plain,
not(sF0) = true,
inference(step,[status(thm)],[t2132,t314]) ).
cnf(t2134,plain,
sF6 = true,
inference(step,[status(thm)],[t2133,t162]) ).
cnf(t2135,plain,
sF6 = sF0,
inference(step,[status(thm)],[t2134,t220]) ).
cnf(t1491,plain,
sF6 = sF0,
inference(orient,[status(thm)],[t2135]) ).
cnf(t2154,plain,
false = sF0,
inference(step,[status(thm)],[t264,t1491]) ).
cnf(t1510,plain,
false = sF0,
inference(orient,[status(thm)],[t2154]) ).
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(f62,axiom,
lower_dimension_point_1 != lower_dimension_point_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e2_1) ).
fof(f62_nnf,plain,
lower_dimension_point_1 != lower_dimension_point_2,
inference(nnf_transformation,[status(thm)],[f62]) ).
fof(f62_sk,plain,
lower_dimension_point_1 != lower_dimension_point_2,
inference(skolemisation,[status(esa)],[f62_nnf]) ).
cnf(c62,plain,
lower_dimension_point_1 != lower_dimension_point_2,
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(f63,axiom,
lower_dimension_point_2 != lower_dimension_point_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e2_2) ).
fof(f63_nnf,plain,
lower_dimension_point_2 != lower_dimension_point_3,
inference(nnf_transformation,[status(thm)],[f63]) ).
fof(f63_sk,plain,
lower_dimension_point_2 != lower_dimension_point_3,
inference(skolemisation,[status(esa)],[f63_nnf]) ).
cnf(c63,plain,
lower_dimension_point_2 != lower_dimension_point_3,
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
cnf(f64,axiom,
lower_dimension_point_1 != lower_dimension_point_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e2_3) ).
fof(f64_nnf,plain,
lower_dimension_point_1 != lower_dimension_point_3,
inference(nnf_transformation,[status(thm)],[f64]) ).
fof(f64_sk,plain,
lower_dimension_point_1 != lower_dimension_point_3,
inference(skolemisation,[status(esa)],[f64_nnf]) ).
cnf(c64,plain,
lower_dimension_point_1 != lower_dimension_point_3,
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
cnf(f65,axiom,
V != extension(U,V,lower_dimension_point_1,lower_dimension_point_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e3_1) ).
fof(f65_nnf,plain,
! [V,U] : V != extension(U,V,lower_dimension_point_1,lower_dimension_point_2),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [V,U] : V != extension(U,V,lower_dimension_point_1,lower_dimension_point_2),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c65,plain,
X0 != extension(X1,X0,lower_dimension_point_1,lower_dimension_point_2),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(f95,axiom,
~ colinear(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11) ).
fof(f95_nnf,plain,
~ colinear(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
inference(nnf_transformation,[status(thm)],[f95]) ).
fof(f95_sk,plain,
~ colinear(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
inference(skolemisation,[status(esa)],[f95_nnf]) ).
cnf(c95,plain,
~ colinear(lower_dimension_point_1,lower_dimension_point_2,lower_dimension_point_3),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c9,c10,c11,c62,c63,c64,c65,c95,c97]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t220]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t1510]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO067-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.33 % Computer : n019.cluster.edu
% 0.09/0.33 % Model : x86_64 x86_64
% 0.09/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.33 % Memory : 8046.5625MB
% 0.09/0.33 % OS : Linux 6.8.0-71-generic
% 0.09/0.33 % CPULimit : 300
% 0.09/0.33 % WCLimit : 300
% 0.09/0.33 % DateTime : Wed Sep 23 10:41:19 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.09/0.34 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.35/1.69 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.35/1.69 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------