%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO069-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 : n004.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:56 PM UTC 2026
% Result : Unsatisfiable 15.49s 2.53s
% Output : Proof 15.49s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t128,axiom,
sF4 = or(not(colinear(x,w,u)),not(colinear(x,w,v))),
introduced(definition) ).
cnf(t124,axiom,
sF0 = colinear(x,w,u),
introduced(definition) ).
cnf(t153,plain,
colinear(x,w,u) = sF0,
inference(orient,[status(thm)],[t124]) ).
cnf(t2648,plain,
sF4 = or(not(sF0),not(colinear(x,w,v))),
inference(step,[status(thm)],[t128,t153]) ).
cnf(t125,axiom,
sF1 = not(colinear(x,w,u)),
introduced(definition) ).
cnf(t2621,plain,
sF1 = not(sF0),
inference(step,[status(thm)],[t125,t153]) ).
cnf(t166,plain,
not(sF0) = sF1,
inference(orient,[status(thm)],[t2621]) ).
cnf(t2649,plain,
sF4 = or(sF1,not(colinear(x,w,v))),
inference(step,[status(thm)],[t2648,t166]) ).
cnf(t126,axiom,
sF2 = colinear(x,w,v),
introduced(definition) ).
cnf(t154,plain,
colinear(x,w,v) = sF2,
inference(orient,[status(thm)],[t126]) ).
cnf(t2650,plain,
sF4 = or(sF1,not(sF2)),
inference(step,[status(thm)],[t2649,t154]) ).
cnf(t127,axiom,
sF3 = not(colinear(x,w,v)),
introduced(definition) ).
cnf(t2622,plain,
sF3 = not(sF2),
inference(step,[status(thm)],[t127,t154]) ).
cnf(t167,plain,
not(sF2) = sF3,
inference(orient,[status(thm)],[t2622]) ).
cnf(t2651,plain,
sF4 = or(sF1,sF3),
inference(step,[status(thm)],[t2650,t167]) ).
cnf(f106,negated_conjecture,
( ~ colinear(x,w,v)
| ~ colinear(x,w,u) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_xwu_and_xwv_colinear) ).
fof(f106_nnf,plain,
( ~ colinear(x,w,v)
| ~ colinear(x,w,u) ),
inference(nnf_transformation,[status(thm)],[f106]) ).
fof(f106_sk,plain,
( ~ colinear(x,w,v)
| ~ colinear(x,w,u) ),
inference(skolemisation,[status(esa)],[f106_nnf]) ).
cnf(c106,plain,
( ~ colinear(x,w,v)
| ~ colinear(x,w,u) ),
inference(cnf_transformation,[status(esa)],[f106_sk]) ).
cnf(t61,plain,
or(not(colinear(x,w,u)),not(colinear(x,w,v))) = true,
inference(equality_encoding,[status(esa)],[c106]) ).
cnf(t2644,plain,
or(not(sF0),not(colinear(x,w,v))) = true,
inference(step,[status(thm)],[t61,t153]) ).
cnf(t2645,plain,
or(sF1,not(colinear(x,w,v))) = true,
inference(step,[status(thm)],[t2644,t166]) ).
cnf(t2646,plain,
or(sF1,not(sF2)) = true,
inference(step,[status(thm)],[t2645,t154]) ).
cnf(t2647,plain,
or(sF1,sF3) = true,
inference(step,[status(thm)],[t2646,t167]) ).
cnf(t345,plain,
or(sF1,sF3) = true,
inference(orient,[status(thm)],[t2647]) ).
cnf(t2652,plain,
sF4 = true,
inference(step,[status(thm)],[t2651,t345]) ).
cnf(t350,plain,
true = sF4,
inference(orient,[status(thm)],[t2652]) ).
cnf(f90,axiom,
( colinear(W,V,U)
| ~ colinear(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_1) ).
fof(f90_nnf,plain,
! [U,V,W] :
( colinear(W,V,U)
| ~ colinear(U,V,W) ),
inference(nnf_transformation,[status(thm)],[f90]) ).
fof(f90_sk,plain,
! [U,V,W] :
( colinear(W,V,U)
| ~ colinear(U,V,W) ),
inference(skolemisation,[status(esa)],[f90_nnf]) ).
cnf(c90,plain,
( colinear(X2,X1,X0)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f90_sk]) ).
cnf(t60,plain,
ifeq(colinear(X1,X2,X3),true,colinear(X3,X2,X1),true) = true,
inference(equality_encoding,[status(esa)],[c90]) ).
cnf(t338,plain,
ifeq(colinear(X1,X2,X3),true,colinear(X3,X2,X1),true) = true,
inference(orient,[status(thm)],[t60]) ).
cnf(t493,plain,
ifeq(colinear(X1,X2,X3),sF4,colinear(X3,X2,X1),sF4) = true,
inference(rw,[status(thm)],[t338]) ).
cnf(t2844,plain,
ifeq(colinear(X1,X2,X3),sF4,colinear(X3,X2,X1),sF4) = sF4,
inference(step,[status(thm)],[t493,t350]) ).
cnf(t651,plain,
ifeq(colinear(X1,X2,X3),sF4,colinear(X3,X2,X1),sF4) = sF4,
inference(orient,[status(thm)],[t2844]) ).
cnf(f101,axiom,
( U = V
| colinear(U,W,X)
| ~ colinear(U,V,X)
| ~ colinear(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_1) ).
fof(f101_nnf,plain,
! [U,V,W,X] :
( U = V
| colinear(U,W,X)
| ~ colinear(U,V,X)
| ~ colinear(U,V,W) ),
inference(nnf_transformation,[status(thm)],[f101]) ).
fof(f101_sk,plain,
! [U,V,W,X] :
( U = V
| colinear(U,W,X)
| ~ colinear(U,V,X)
| ~ colinear(U,V,W) ),
inference(skolemisation,[status(esa)],[f101_nnf]) ).
cnf(c101,plain,
( X0 = X1
| colinear(X0,X2,X3)
| ~ colinear(X0,X1,X3)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f101_sk]) ).
cnf(t92,plain,
ifeq(colinear(X1,X2,X3),true,ifeq(colinear(X1,X2,X4),true,or(colinear(X1,X3,X4),eq(X1,X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c101]) ).
cnf(t3026,plain,
ifeq(colinear(X1,X2,X3),sF4,ifeq(colinear(X1,X2,X4),true,or(colinear(X1,X3,X4),eq(X1,X2)),true),true) = true,
inference(step,[status(thm)],[t92,t350]) ).
cnf(t3027,plain,
ifeq(colinear(X1,X2,X3),sF4,ifeq(colinear(X1,X2,X4),sF4,or(colinear(X1,X3,X4),eq(X1,X2)),true),true) = true,
inference(step,[status(thm)],[t3026,t350]) ).
cnf(t3028,plain,
ifeq(colinear(X1,X2,X3),sF4,ifeq(colinear(X1,X2,X4),sF4,or(colinear(X1,X3,X4),eq(X1,X2)),sF4),true) = true,
inference(step,[status(thm)],[t3027,t350]) ).
cnf(t3029,plain,
ifeq(colinear(X1,X2,X3),sF4,ifeq(colinear(X1,X2,X4),sF4,or(colinear(X1,X3,X4),eq(X1,X2)),sF4),sF4) = true,
inference(step,[status(thm)],[t3028,t350]) ).
cnf(t3030,plain,
ifeq(colinear(X1,X2,X3),sF4,ifeq(colinear(X1,X2,X4),sF4,or(colinear(X1,X3,X4),eq(X1,X2)),sF4),sF4) = sF4,
inference(step,[status(thm)],[t3029,t350]) ).
cnf(t1297,plain,
ifeq(colinear(X1,X2,X3),sF4,ifeq(colinear(X1,X2,X4),sF4,or(colinear(X1,X3,X4),eq(X1,X2)),sF4),sF4) = sF4,
inference(orient,[status(thm)],[t3030]) ).
cnf(f92,axiom,
( colinear(U,W,V)
| ~ colinear(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_3) ).
fof(f92_nnf,plain,
! [U,V,W] :
( colinear(U,W,V)
| ~ colinear(U,V,W) ),
inference(nnf_transformation,[status(thm)],[f92]) ).
fof(f92_sk,plain,
! [U,V,W] :
( colinear(U,W,V)
| ~ colinear(U,V,W) ),
inference(skolemisation,[status(esa)],[f92_nnf]) ).
cnf(c92,plain,
( colinear(X0,X2,X1)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(t56,plain,
ifeq(colinear(X1,X2,X3),true,colinear(X1,X3,X2),true) = true,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t274,plain,
ifeq(colinear(X1,X2,X3),true,colinear(X1,X3,X2),true) = true,
inference(orient,[status(thm)],[t56]) ).
cnf(f94,axiom,
( colinear(V,U,W)
| ~ colinear(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_5) ).
fof(f94_nnf,plain,
! [U,V,W] :
( colinear(V,U,W)
| ~ colinear(U,V,W) ),
inference(nnf_transformation,[status(thm)],[f94]) ).
fof(f94_sk,plain,
! [U,V,W] :
( colinear(V,U,W)
| ~ colinear(U,V,W) ),
inference(skolemisation,[status(esa)],[f94_nnf]) ).
cnf(c94,plain,
( colinear(X1,X0,X2)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(t57,plain,
ifeq(colinear(X1,X2,X3),true,colinear(X2,X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c94]) ).
cnf(t284,plain,
ifeq(colinear(X1,X2,X3),true,colinear(X2,X1,X3),true) = true,
inference(orient,[status(thm)],[t57]) ).
cnf(f104,hypothesis,
colinear(w,v,u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wvu_colinear) ).
fof(f104_nnf,plain,
colinear(w,v,u),
inference(nnf_transformation,[status(thm)],[f104]) ).
cnf(c104,plain,
colinear(w,v,u),
inference(cnf_transformation,[status(esa)],[f104_nnf]) ).
cnf(t20,plain,
colinear(w,v,u) = true,
inference(equality_encoding,[status(esa)],[c104]) ).
cnf(t151,plain,
colinear(w,v,u) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t276,plain,
true = ifeq(true,true,colinear(w,u,v),true),
inference(cp,[status(thm)],[t274,t151]) ).
cnf(t27,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t161,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t27]) ).
cnf(t2634,plain,
true = colinear(w,u,v),
inference(step,[status(thm)],[t276,t161]) ).
cnf(t282,plain,
colinear(w,u,v) = true,
inference(orient,[status(thm)],[t2634]) ).
cnf(t292,plain,
true = ifeq(true,true,colinear(u,w,v),true),
inference(cp,[status(thm)],[t284,t282]) ).
cnf(t2638,plain,
true = colinear(u,w,v),
inference(step,[status(thm)],[t292,t161]) ).
cnf(t298,plain,
colinear(u,w,v) = true,
inference(orient,[status(thm)],[t2638]) ).
cnf(t299,plain,
true = ifeq(true,true,colinear(u,v,w),true),
inference(cp,[status(thm)],[t274,t298]) ).
cnf(t2642,plain,
true = colinear(u,v,w),
inference(step,[status(thm)],[t299,t161]) ).
cnf(t304,plain,
colinear(u,v,w) = true,
inference(orient,[status(thm)],[t2642]) ).
cnf(t2727,plain,
colinear(u,v,w) = sF4,
inference(step,[status(thm)],[t304,t350]) ).
cnf(t467,plain,
colinear(u,v,w) = sF4,
inference(orient,[status(thm)],[t2727]) ).
cnf(t1346,plain,
sF4 = ifeq(sF4,sF4,ifeq(colinear(u,v,X1),sF4,or(colinear(u,w,X1),eq(u,v)),sF4),sF4),
inference(cp,[status(thm)],[t1297,t467]) ).
cnf(t3031,plain,
sF4 = ifeq(colinear(u,v,X1),sF4,or(colinear(u,w,X1),eq(u,v)),sF4),
inference(step,[status(thm)],[t1346,t161]) ).
cnf(f103,hypothesis,
u != v,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u_not_v) ).
fof(f103_nnf,plain,
u != v,
inference(nnf_transformation,[status(thm)],[f103]) ).
fof(f103_sk,plain,
u != v,
inference(skolemisation,[status(esa)],[f103_nnf]) ).
cnf(c103,plain,
u != v,
inference(cnf_transformation,[status(esa)],[f103_sk]) ).
cnf(t6,plain,
eq(u,v) = false,
inference(equality_encoding,[status(esa)],[c103]) ).
cnf(t137,plain,
eq(u,v) = false,
inference(orient,[status(thm)],[t6]) ).
cnf(t3032,plain,
sF4 = ifeq(colinear(u,v,X1),sF4,or(colinear(u,w,X1),false),sF4),
inference(step,[status(thm)],[t3031,t137]) ).
cnf(t7,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t138,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t3033,plain,
sF4 = ifeq(colinear(u,v,X1),sF4,colinear(u,w,X1),sF4),
inference(step,[status(thm)],[t3032,t138]) ).
cnf(t1363,plain,
ifeq(colinear(u,v,X1),sF4,colinear(u,w,X1),sF4) = sF4,
inference(orient,[status(thm)],[t3033]) ).
cnf(f105,hypothesis,
colinear(x,v,u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xvu_colinear) ).
fof(f105_nnf,plain,
colinear(x,v,u),
inference(nnf_transformation,[status(thm)],[f105]) ).
cnf(c105,plain,
colinear(x,v,u),
inference(cnf_transformation,[status(esa)],[f105_nnf]) ).
cnf(t21,plain,
colinear(x,v,u) = true,
inference(equality_encoding,[status(esa)],[c105]) ).
cnf(t152,plain,
colinear(x,v,u) = true,
inference(orient,[status(thm)],[t21]) ).
cnf(t277,plain,
true = ifeq(true,true,colinear(x,u,v),true),
inference(cp,[status(thm)],[t274,t152]) ).
cnf(t2635,plain,
true = colinear(x,u,v),
inference(step,[status(thm)],[t277,t161]) ).
cnf(t283,plain,
colinear(x,u,v) = true,
inference(orient,[status(thm)],[t2635]) ).
cnf(t293,plain,
true = ifeq(true,true,colinear(u,x,v),true),
inference(cp,[status(thm)],[t284,t283]) ).
cnf(t2639,plain,
true = colinear(u,x,v),
inference(step,[status(thm)],[t293,t161]) ).
cnf(t300,plain,
colinear(u,x,v) = true,
inference(orient,[status(thm)],[t2639]) ).
cnf(t301,plain,
true = ifeq(true,true,colinear(u,v,x),true),
inference(cp,[status(thm)],[t274,t300]) ).
cnf(t2643,plain,
true = colinear(u,v,x),
inference(step,[status(thm)],[t301,t161]) ).
cnf(t305,plain,
colinear(u,v,x) = true,
inference(orient,[status(thm)],[t2643]) ).
cnf(t2729,plain,
colinear(u,v,x) = sF4,
inference(step,[status(thm)],[t305,t350]) ).
cnf(t469,plain,
colinear(u,v,x) = sF4,
inference(orient,[status(thm)],[t2729]) ).
cnf(t1366,plain,
sF4 = ifeq(sF4,sF4,colinear(u,w,x),sF4),
inference(cp,[status(thm)],[t1363,t469]) ).
cnf(t3034,plain,
sF4 = colinear(u,w,x),
inference(step,[status(thm)],[t1366,t161]) ).
cnf(t1369,plain,
colinear(u,w,x) = sF4,
inference(orient,[status(thm)],[t3034]) ).
cnf(t1376,plain,
sF4 = ifeq(sF4,sF4,colinear(x,w,u),sF4),
inference(cp,[status(thm)],[t651,t1369]) ).
cnf(t3035,plain,
sF4 = colinear(x,w,u),
inference(step,[status(thm)],[t1376,t161]) ).
cnf(t3036,plain,
sF4 = sF0,
inference(step,[status(thm)],[t3035,t153]) ).
cnf(t1380,plain,
sF4 = sF0,
inference(orient,[status(thm)],[t3036]) ).
cnf(t3101,plain,
true = sF0,
inference(step,[status(thm)],[t350,t1380]) ).
cnf(t1445,plain,
true = sF0,
inference(orient,[status(thm)],[t3101]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t132,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t2655,plain,
not(sF4) = false,
inference(step,[status(thm)],[t132,t350]) ).
cnf(t353,plain,
not(sF4) = false,
inference(rw,[status(thm)],[t2655]) ).
cnf(t501,plain,
not(sF4) = false,
inference(orient,[status(thm)],[t353]) ).
cnf(t1447,plain,
not(sF0) = false,
inference(rw,[status(thm)],[t501]) ).
cnf(t3243,plain,
sF1 = false,
inference(step,[status(thm)],[t1447,t166]) ).
cnf(t1752,plain,
false = sF1,
inference(orient,[status(thm)],[t3243]) ).
cnf(t1560,plain,
ifeq(colinear(X1,X2,X3),sF0,colinear(X3,X2,X1),sF0) = sF4,
inference(rw,[status(thm)],[t651]) ).
cnf(t3499,plain,
ifeq(colinear(X1,X2,X3),sF0,colinear(X3,X2,X1),sF0) = sF0,
inference(step,[status(thm)],[t1560,t1380]) ).
cnf(t2354,plain,
ifeq(colinear(X1,X2,X3),sF0,colinear(X3,X2,X1),sF0) = sF0,
inference(orient,[status(thm)],[t3499]) ).
cnf(f102,axiom,
( U = V
| colinear(V,W,X)
| ~ colinear(U,V,X)
| ~ colinear(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_2) ).
fof(f102_nnf,plain,
! [U,V,W,X] :
( U = V
| colinear(V,W,X)
| ~ colinear(U,V,X)
| ~ colinear(U,V,W) ),
inference(nnf_transformation,[status(thm)],[f102]) ).
fof(f102_sk,plain,
! [U,V,W,X] :
( U = V
| colinear(V,W,X)
| ~ colinear(U,V,X)
| ~ colinear(U,V,W) ),
inference(skolemisation,[status(esa)],[f102_nnf]) ).
cnf(c102,plain,
( X0 = X1
| colinear(X1,X2,X3)
| ~ colinear(X0,X1,X3)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f102_sk]) ).
cnf(t93,plain,
ifeq(colinear(X1,X2,X3),true,ifeq(colinear(X1,X2,X4),true,or(colinear(X2,X3,X4),eq(X1,X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c102]) ).
cnf(t3272,plain,
ifeq(colinear(X1,X2,X3),sF0,ifeq(colinear(X1,X2,X4),true,or(colinear(X2,X3,X4),eq(X1,X2)),true),true) = true,
inference(step,[status(thm)],[t93,t1445]) ).
cnf(t3273,plain,
ifeq(colinear(X1,X2,X3),sF0,ifeq(colinear(X1,X2,X4),sF0,or(colinear(X2,X3,X4),eq(X1,X2)),true),true) = true,
inference(step,[status(thm)],[t3272,t1445]) ).
cnf(t3274,plain,
ifeq(colinear(X1,X2,X3),sF0,ifeq(colinear(X1,X2,X4),sF0,or(colinear(X2,X3,X4),eq(X1,X2)),sF0),true) = true,
inference(step,[status(thm)],[t3273,t1445]) ).
cnf(t3275,plain,
ifeq(colinear(X1,X2,X3),sF0,ifeq(colinear(X1,X2,X4),sF0,or(colinear(X2,X3,X4),eq(X1,X2)),sF0),sF0) = true,
inference(step,[status(thm)],[t3274,t1445]) ).
cnf(t3276,plain,
ifeq(colinear(X1,X2,X3),sF0,ifeq(colinear(X1,X2,X4),sF0,or(colinear(X2,X3,X4),eq(X1,X2)),sF0),sF0) = sF0,
inference(step,[status(thm)],[t3275,t1445]) ).
cnf(t1785,plain,
ifeq(colinear(X1,X2,X3),sF0,ifeq(colinear(X1,X2,X4),sF0,or(colinear(X2,X3,X4),eq(X1,X2)),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t3276]) ).
cnf(t3095,plain,
colinear(u,v,w) = sF0,
inference(step,[status(thm)],[t467,t1380]) ).
cnf(t1439,plain,
colinear(u,v,w) = sF0,
inference(orient,[status(thm)],[t3095]) ).
cnf(t1852,plain,
sF0 = ifeq(sF0,sF0,ifeq(colinear(u,v,X1),sF0,or(colinear(v,w,X1),eq(u,v)),sF0),sF0),
inference(cp,[status(thm)],[t1785,t1439]) ).
cnf(t3531,plain,
sF0 = ifeq(colinear(u,v,X1),sF0,or(colinear(v,w,X1),eq(u,v)),sF0),
inference(step,[status(thm)],[t1852,t161]) ).
cnf(t3251,plain,
eq(u,v) = sF1,
inference(step,[status(thm)],[t137,t1752]) ).
cnf(t1760,plain,
eq(u,v) = sF1,
inference(orient,[status(thm)],[t3251]) ).
cnf(t3532,plain,
sF0 = ifeq(colinear(u,v,X1),sF0,or(colinear(v,w,X1),sF1),sF0),
inference(step,[status(thm)],[t3531,t1760]) ).
cnf(t3253,plain,
or(X1,sF1) = X1,
inference(step,[status(thm)],[t138,t1752]) ).
cnf(t1762,plain,
or(X1,sF1) = X1,
inference(rw,[status(thm)],[t3253]) ).
cnf(t1779,plain,
or(X1,sF1) = X1,
inference(orient,[status(thm)],[t1762]) ).
cnf(t3533,plain,
sF0 = ifeq(colinear(u,v,X1),sF0,colinear(v,w,X1),sF0),
inference(step,[status(thm)],[t3532,t1779]) ).
cnf(t2470,plain,
ifeq(colinear(u,v,X1),sF0,colinear(v,w,X1),sF0) = sF0,
inference(orient,[status(thm)],[t3533]) ).
cnf(t3097,plain,
colinear(u,v,x) = sF0,
inference(step,[status(thm)],[t469,t1380]) ).
cnf(t1441,plain,
colinear(u,v,x) = sF0,
inference(orient,[status(thm)],[t3097]) ).
cnf(t2473,plain,
sF0 = ifeq(sF0,sF0,colinear(v,w,x),sF0),
inference(cp,[status(thm)],[t2470,t1441]) ).
cnf(t3539,plain,
sF0 = colinear(v,w,x),
inference(step,[status(thm)],[t2473,t161]) ).
cnf(t2512,plain,
colinear(v,w,x) = sF0,
inference(orient,[status(thm)],[t3539]) ).
cnf(t2521,plain,
sF0 = ifeq(sF0,sF0,colinear(x,w,v),sF0),
inference(cp,[status(thm)],[t2354,t2512]) ).
cnf(t3540,plain,
sF0 = colinear(x,w,v),
inference(step,[status(thm)],[t2521,t161]) ).
cnf(t32,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t168,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t32]) ).
cnf(t171,plain,
false = ifeq(sF3,true,sF2,false),
inference(cp,[status(thm)],[t168,t167]) ).
cnf(t174,plain,
ifeq(sF3,true,sF2,false) = false,
inference(orient,[status(thm)],[t171]) ).
cnf(t2682,plain,
ifeq(sF3,sF4,sF2,false) = false,
inference(step,[status(thm)],[t174,t350]) ).
cnf(t385,plain,
ifeq(sF3,sF4,sF2,false) = false,
inference(rw,[status(thm)],[t2682]) ).
cnf(t519,plain,
ifeq(sF3,sF4,sF2,false) = false,
inference(orient,[status(thm)],[t385]) ).
cnf(t3106,plain,
ifeq(sF3,sF0,sF2,false) = false,
inference(step,[status(thm)],[t519,t1380]) ).
cnf(t1457,plain,
ifeq(sF3,sF0,sF2,false) = false,
inference(rw,[status(thm)],[t3106]) ).
cnf(t2731,plain,
or(sF1,sF3) = sF4,
inference(step,[status(thm)],[t345,t350]) ).
cnf(t495,plain,
or(sF1,sF3) = sF4,
inference(orient,[status(thm)],[t2731]) ).
cnf(t3099,plain,
or(sF1,sF3) = sF0,
inference(step,[status(thm)],[t495,t1380]) ).
cnf(t1443,plain,
or(sF1,sF3) = sF0,
inference(orient,[status(thm)],[t3099]) ).
cnf(t9,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t140,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t3254,plain,
or(sF1,X1) = X1,
inference(step,[status(thm)],[t140,t1752]) ).
cnf(t1763,plain,
or(sF1,X1) = X1,
inference(rw,[status(thm)],[t3254]) ).
cnf(t1780,plain,
or(sF1,X1) = X1,
inference(orient,[status(thm)],[t1763]) ).
cnf(t3269,plain,
sF3 = sF0,
inference(step,[status(thm)],[t1443,t1780]) ).
cnf(t1781,plain,
sF3 = sF0,
inference(rw,[status(thm)],[t3269]) ).
cnf(t1782,plain,
sF3 = sF0,
inference(orient,[status(thm)],[t1781]) ).
cnf(t3288,plain,
ifeq(sF0,sF0,sF2,false) = false,
inference(step,[status(thm)],[t1457,t1782]) ).
cnf(t3289,plain,
sF2 = false,
inference(step,[status(thm)],[t3288,t161]) ).
cnf(t3290,plain,
sF2 = sF1,
inference(step,[status(thm)],[t3289,t1752]) ).
cnf(t1885,plain,
sF2 = sF1,
inference(orient,[status(thm)],[t3290]) ).
cnf(t3291,plain,
colinear(x,w,v) = sF1,
inference(step,[status(thm)],[t154,t1885]) ).
cnf(t1886,plain,
colinear(x,w,v) = sF1,
inference(orient,[status(thm)],[t3291]) ).
cnf(t3541,plain,
sF0 = sF1,
inference(step,[status(thm)],[t3540,t1886]) ).
cnf(t2522,plain,
sF1 = sF0,
inference(orient,[status(thm)],[t3541]) ).
cnf(t3566,plain,
false = sF0,
inference(step,[status(thm)],[t1752,t2522]) ).
cnf(t2547,plain,
false = sF0,
inference(orient,[status(thm)],[t3566]) ).
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,c103,c106]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t1445]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t2547]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO069-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.38 % Computer : n004.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 10:41:37 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 15.49/2.53 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.49/2.53 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------