%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO077-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n018.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:58 PM UTC 2026
% Result : Unsatisfiable 67.18s 8.93s
% Output : Proof 67.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 22
% Syntax : Number of formulae : 181 ( 149 unt; 0 def)
% Number of atoms : 341 ( 183 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 298 ( 138 ~; 160 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-4 aty)
% Number of variables : 125 ( 2 sgn 38 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f28,axiom,
( ~ collinear(X1,X2,X3)
| on(X3,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_G10C) ).
fof(f28_nnf,plain,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| on(X3,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| on(X3,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( ~ collinear(X0,X1,X2)
| on(X2,line_through_3_points(X0,X1,X2))
| X1 = X2
| X0 = X2
| X0 = X1
| ~ point(X2)
| ~ point(X1)
| ~ point(X0) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(t251,plain,
ifeq(point(X1),true,ifeq(point(X2),true,ifeq(point(X3),true,ifeq(collinear(X1,X2,X3),true,or(eq(X1,X2),or(eq(X1,X3),or(eq(X2,X3),on(X3,line_through_3_points(X1,X2,X3))))),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t724,plain,
ifeq(point(X1),true,ifeq(point(X2),true,ifeq(point(X3),true,ifeq(collinear(X1,X2,X3),true,or(eq(X1,X2),or(eq(X1,X3),or(eq(X2,X3),on(X3,line_through_3_points(X1,X2,X3))))),true),true),true),true) = true,
inference(orient,[status(thm)],[t251]) ).
cnf(t34,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t259,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t34]) ).
cnf(f3,axiom,
( ~ line(Y4)
| ~ line(Y3)
| ~ point(Z2)
| ~ point(Z1)
| ~ on(Z2,Y4)
| ~ on(Z1,Y4)
| Y3 = Y4
| ~ on(Z2,Y3)
| Z1 = Z2
| ~ on(Z1,Y3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_G1D) ).
fof(f3_nnf,plain,
! [Z1,Y3,Z2,Y4] :
( ~ line(Y4)
| ~ line(Y3)
| ~ point(Z2)
| ~ point(Z1)
| ~ on(Z2,Y4)
| ~ on(Z1,Y4)
| Y3 = Y4
| ~ on(Z2,Y3)
| Z1 = Z2
| ~ on(Z1,Y3) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [Z1,Y3,Z2,Y4] :
( ~ line(Y4)
| ~ line(Y3)
| ~ point(Z2)
| ~ point(Z1)
| ~ on(Z2,Y4)
| ~ on(Z1,Y4)
| Y3 = Y4
| ~ on(Z2,Y3)
| Z1 = Z2
| ~ on(Z1,Y3) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( ~ line(X3)
| ~ line(X1)
| ~ point(X2)
| ~ point(X0)
| ~ on(X2,X3)
| ~ on(X0,X3)
| X1 = X3
| ~ on(X2,X1)
| X0 = X2
| ~ on(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t253,plain,
ifeq(on(X1,X2),true,ifeq(on(X3,X2),true,ifeq(on(X1,X4),true,ifeq(on(X3,X4),true,ifeq(point(X1),true,ifeq(point(X3),true,ifeq(line(X2),true,ifeq(line(X4),true,or(eq(X1,X3),eq(X2,X4)),true),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t453,plain,
ifeq(on(X1,X2),true,ifeq(on(X3,X2),true,ifeq(on(X1,X4),true,ifeq(on(X3,X4),true,ifeq(point(X1),true,ifeq(point(X3),true,ifeq(line(X2),true,ifeq(line(X4),true,or(eq(X1,X3),eq(X2,X4)),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t253]) ).
cnf(f35,hypothesis,
on(point1,a_line),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',point1_on_line) ).
fof(f35_nnf,plain,
on(point1,a_line),
inference(nnf_transformation,[status(thm)],[f35]) ).
cnf(c35,plain,
on(point1,a_line),
inference(cnf_transformation,[status(esa)],[f35_nnf]) ).
cnf(t11,plain,
on(point1,a_line) = true,
inference(equality_encoding,[status(esa)],[c35]) ).
cnf(t412,plain,
on(point1,a_line) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t459,plain,
true = ifeq(true,true,ifeq(on(X1,a_line),true,ifeq(on(point1,X2),true,ifeq(on(X1,X2),true,ifeq(point(point1),true,ifeq(point(X1),true,ifeq(line(a_line),true,ifeq(line(X2),true,or(eq(point1,X1),eq(a_line,X2)),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t453,t412]) ).
cnf(t29,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t258,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t29]) ).
cnf(t18761,plain,
true = ifeq(on(X1,a_line),true,ifeq(on(point1,X2),true,ifeq(on(X1,X2),true,ifeq(point(point1),true,ifeq(point(X1),true,ifeq(line(a_line),true,ifeq(line(X2),true,or(eq(point1,X1),eq(a_line,X2)),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t459,t258]) ).
cnf(f31,hypothesis,
point(point1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',point1) ).
fof(f31_nnf,plain,
point(point1),
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
point(point1),
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(t4,plain,
point(point1) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t859,plain,
point(point1) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t18762,plain,
true = ifeq(on(X1,a_line),true,ifeq(on(point1,X2),true,ifeq(on(X1,X2),true,ifeq(true,true,ifeq(point(X1),true,ifeq(line(a_line),true,ifeq(line(X2),true,or(eq(point1,X1),eq(a_line,X2)),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t18761,t859]) ).
cnf(t18763,plain,
true = ifeq(on(X1,a_line),true,ifeq(on(point1,X2),true,ifeq(on(X1,X2),true,ifeq(point(X1),true,ifeq(line(a_line),true,ifeq(line(X2),true,or(eq(point1,X1),eq(a_line,X2)),true),true),true),true),true),true),
inference(step,[status(thm)],[t18762,t258]) ).
cnf(f34,hypothesis,
line(a_line),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',line) ).
fof(f34_nnf,plain,
line(a_line),
inference(nnf_transformation,[status(thm)],[f34]) ).
cnf(c34,plain,
line(a_line),
inference(cnf_transformation,[status(esa)],[f34_nnf]) ).
cnf(t0,plain,
line(a_line) = true,
inference(equality_encoding,[status(esa)],[c34]) ).
cnf(t790,plain,
line(a_line) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t18764,plain,
true = ifeq(on(X1,a_line),true,ifeq(on(point1,X2),true,ifeq(on(X1,X2),true,ifeq(point(X1),true,ifeq(true,true,ifeq(line(X2),true,or(eq(point1,X1),eq(a_line,X2)),true),true),true),true),true),true),
inference(step,[status(thm)],[t18763,t790]) ).
cnf(t18765,plain,
true = ifeq(on(X1,a_line),true,ifeq(on(point1,X2),true,ifeq(on(X1,X2),true,ifeq(point(X1),true,ifeq(line(X2),true,or(eq(point1,X1),eq(a_line,X2)),true),true),true),true),true),
inference(step,[status(thm)],[t18764,t258]) ).
cnf(t15700,plain,
ifeq(on(X1,a_line),true,ifeq(on(point1,X2),true,ifeq(on(X1,X2),true,ifeq(point(X1),true,ifeq(line(X2),true,or(eq(point1,X1),eq(a_line,X2)),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t18765]) ).
cnf(f27,axiom,
( ~ collinear(X1,X2,X3)
| on(X2,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_G10B) ).
fof(f27_nnf,plain,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| on(X2,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| on(X2,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
( ~ collinear(X0,X1,X2)
| on(X1,line_through_3_points(X0,X1,X2))
| X1 = X2
| X0 = X2
| X0 = X1
| ~ point(X2)
| ~ point(X1)
| ~ point(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(hi24,axiom,
ifeq(point(X0),true,ifeq(point(X1),true,ifeq(point(X2),true,ifeq(collinear(X0,X1,X2),true,or(eq(X0,X1),or(eq(X0,X2),or(eq(X1,X2),on(X1,line_through_3_points(X0,X1,X2))))),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(hi28,axiom,
point(point1) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(f32,hypothesis,
point(point2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',point2) ).
fof(f32_nnf,plain,
point(point2),
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c32,plain,
point(point2),
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(hi29,axiom,
point(point2) = true,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(f33,hypothesis,
point(point3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',point3) ).
fof(f33_nnf,plain,
point(point3),
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c33,plain,
point(point3),
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(hi30,axiom,
point(point3) = true,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(f41,negated_conjecture,
collinear(point1,point2,point3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_points_noncollinear) ).
fof(f41_nnf,plain,
collinear(point1,point2,point3),
inference(nnf_transformation,[status(thm)],[f41]) ).
cnf(c41,plain,
collinear(point1,point2,point3),
inference(cnf_transformation,[status(esa)],[f41_nnf]) ).
cnf(hi34,negated_conjecture,
collinear(point1,point2,point3) = true,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(t230,plain,
or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point2,line_through_3_points(point1,point2,point3))))) = true,
inference(hyper_resolution,[status(thm)],[hi24,hi28,hi29,hi30,hi34]) ).
cnf(t264,plain,
or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point2,line_through_3_points(point1,point2,point3))))) = true,
inference(orient,[status(thm)],[t230]) ).
cnf(f40,hypothesis,
point2 != point3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',point2_not_point3) ).
fof(f40_nnf,plain,
point2 != point3,
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
point2 != point3,
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
point2 != point3,
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(t10,plain,
eq(point2,point3) = false,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(t1223,plain,
eq(point2,point3) = false,
inference(orient,[status(thm)],[t10]) ).
cnf(t15985,plain,
or(eq(point1,point2),or(eq(point1,point3),or(false,on(point2,line_through_3_points(point1,point2,point3))))) = true,
inference(step,[status(thm)],[t264,t1223]) ).
cnf(t16,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t257,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t16]) ).
cnf(t15986,plain,
or(eq(point1,point2),or(eq(point1,point3),on(point2,line_through_3_points(point1,point2,point3)))) = true,
inference(step,[status(thm)],[t15985,t257]) ).
cnf(t1268,plain,
or(eq(point1,point2),or(eq(point1,point3),on(point2,line_through_3_points(point1,point2,point3)))) = true,
inference(rw,[status(thm)],[t15986]) ).
cnf(f38,hypothesis,
point1 != point2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',point1_not_point2) ).
fof(f38_nnf,plain,
point1 != point2,
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
point1 != point2,
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
point1 != point2,
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(t8,plain,
eq(point1,point2) = false,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(t1272,plain,
eq(point1,point2) = false,
inference(orient,[status(thm)],[t8]) ).
cnf(t16234,plain,
or(false,or(eq(point1,point3),on(point2,line_through_3_points(point1,point2,point3)))) = true,
inference(step,[status(thm)],[t1268,t1272]) ).
cnf(t16235,plain,
or(eq(point1,point3),on(point2,line_through_3_points(point1,point2,point3))) = true,
inference(step,[status(thm)],[t16234,t257]) ).
cnf(f39,hypothesis,
point1 != point3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',point1_not_point3) ).
fof(f39_nnf,plain,
point1 != point3,
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
point1 != point3,
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
point1 != point3,
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(t9,plain,
eq(point1,point3) = false,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(t1317,plain,
eq(point1,point3) = false,
inference(orient,[status(thm)],[t9]) ).
cnf(t16236,plain,
or(false,on(point2,line_through_3_points(point1,point2,point3))) = true,
inference(step,[status(thm)],[t16235,t1317]) ).
cnf(t16237,plain,
on(point2,line_through_3_points(point1,point2,point3)) = true,
inference(step,[status(thm)],[t16236,t257]) ).
cnf(t4573,plain,
on(point2,line_through_3_points(point1,point2,point3)) = true,
inference(orient,[status(thm)],[t16237]) ).
cnf(t15758,plain,
true = ifeq(on(point2,a_line),true,ifeq(on(point1,line_through_3_points(point1,point2,point3)),true,ifeq(true,true,ifeq(point(point2),true,ifeq(line(line_through_3_points(point1,point2,point3)),true,or(eq(point1,point2),eq(a_line,line_through_3_points(point1,point2,point3))),true),true),true),true),true),
inference(cp,[status(thm)],[t15700,t4573]) ).
cnf(f36,hypothesis,
on(point2,a_line),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',point2_on_line) ).
fof(f36_nnf,plain,
on(point2,a_line),
inference(nnf_transformation,[status(thm)],[f36]) ).
cnf(c36,plain,
on(point2,a_line),
inference(cnf_transformation,[status(esa)],[f36_nnf]) ).
cnf(t12,plain,
on(point2,a_line) = true,
inference(equality_encoding,[status(esa)],[c36]) ).
cnf(t409,plain,
on(point2,a_line) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t18778,plain,
true = ifeq(true,true,ifeq(on(point1,line_through_3_points(point1,point2,point3)),true,ifeq(true,true,ifeq(point(point2),true,ifeq(line(line_through_3_points(point1,point2,point3)),true,or(eq(point1,point2),eq(a_line,line_through_3_points(point1,point2,point3))),true),true),true),true),true),
inference(step,[status(thm)],[t15758,t409]) ).
cnf(t18779,plain,
true = ifeq(on(point1,line_through_3_points(point1,point2,point3)),true,ifeq(true,true,ifeq(point(point2),true,ifeq(line(line_through_3_points(point1,point2,point3)),true,or(eq(point1,point2),eq(a_line,line_through_3_points(point1,point2,point3))),true),true),true),true),
inference(step,[status(thm)],[t18778,t258]) ).
cnf(f26,axiom,
( ~ collinear(X1,X2,X3)
| on(X1,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_G10A) ).
fof(f26_nnf,plain,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| on(X1,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| on(X1,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( ~ collinear(X0,X1,X2)
| on(X0,line_through_3_points(X0,X1,X2))
| X1 = X2
| X0 = X2
| X0 = X1
| ~ point(X2)
| ~ point(X1)
| ~ point(X0) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(hi23,axiom,
ifeq(point(X0),true,ifeq(point(X1),true,ifeq(point(X2),true,ifeq(collinear(X0,X1,X2),true,or(eq(X0,X1),or(eq(X0,X2),or(eq(X1,X2),on(X0,line_through_3_points(X0,X1,X2))))),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t229,plain,
or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point1,line_through_3_points(point1,point2,point3))))) = true,
inference(hyper_resolution,[status(thm)],[hi23,hi28,hi29,hi30,hi34]) ).
cnf(t265,plain,
or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point1,line_through_3_points(point1,point2,point3))))) = true,
inference(orient,[status(thm)],[t229]) ).
cnf(t15991,plain,
or(eq(point1,point2),or(eq(point1,point3),or(false,on(point1,line_through_3_points(point1,point2,point3))))) = true,
inference(step,[status(thm)],[t265,t1223]) ).
cnf(t15992,plain,
or(eq(point1,point2),or(eq(point1,point3),on(point1,line_through_3_points(point1,point2,point3)))) = true,
inference(step,[status(thm)],[t15991,t257]) ).
cnf(t1271,plain,
or(eq(point1,point2),or(eq(point1,point3),on(point1,line_through_3_points(point1,point2,point3)))) = true,
inference(rw,[status(thm)],[t15992]) ).
cnf(t16242,plain,
or(false,or(eq(point1,point3),on(point1,line_through_3_points(point1,point2,point3)))) = true,
inference(step,[status(thm)],[t1271,t1272]) ).
cnf(t16243,plain,
or(eq(point1,point3),on(point1,line_through_3_points(point1,point2,point3))) = true,
inference(step,[status(thm)],[t16242,t257]) ).
cnf(t16244,plain,
or(false,on(point1,line_through_3_points(point1,point2,point3))) = true,
inference(step,[status(thm)],[t16243,t1317]) ).
cnf(t16245,plain,
on(point1,line_through_3_points(point1,point2,point3)) = true,
inference(step,[status(thm)],[t16244,t257]) ).
cnf(t4629,plain,
on(point1,line_through_3_points(point1,point2,point3)) = true,
inference(orient,[status(thm)],[t16245]) ).
cnf(t18780,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(point(point2),true,ifeq(line(line_through_3_points(point1,point2,point3)),true,or(eq(point1,point2),eq(a_line,line_through_3_points(point1,point2,point3))),true),true),true),true),
inference(step,[status(thm)],[t18779,t4629]) ).
cnf(t18781,plain,
true = ifeq(true,true,ifeq(point(point2),true,ifeq(line(line_through_3_points(point1,point2,point3)),true,or(eq(point1,point2),eq(a_line,line_through_3_points(point1,point2,point3))),true),true),true),
inference(step,[status(thm)],[t18780,t258]) ).
cnf(t18782,plain,
true = ifeq(point(point2),true,ifeq(line(line_through_3_points(point1,point2,point3)),true,or(eq(point1,point2),eq(a_line,line_through_3_points(point1,point2,point3))),true),true),
inference(step,[status(thm)],[t18781,t258]) ).
cnf(t5,plain,
point(point2) = true,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(t814,plain,
point(point2) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t18783,plain,
true = ifeq(true,true,ifeq(line(line_through_3_points(point1,point2,point3)),true,or(eq(point1,point2),eq(a_line,line_through_3_points(point1,point2,point3))),true),true),
inference(step,[status(thm)],[t18782,t814]) ).
cnf(t18784,plain,
true = ifeq(line(line_through_3_points(point1,point2,point3)),true,or(eq(point1,point2),eq(a_line,line_through_3_points(point1,point2,point3))),true),
inference(step,[status(thm)],[t18783,t258]) ).
cnf(f29,axiom,
( ~ collinear(X1,X2,X3)
| line(line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_G10D) ).
fof(f29_nnf,plain,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| line(line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| line(line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( ~ collinear(X0,X1,X2)
| line(line_through_3_points(X0,X1,X2))
| X1 = X2
| X0 = X2
| X0 = X1
| ~ point(X2)
| ~ point(X1)
| ~ point(X0) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(hi26,axiom,
ifeq(point(X0),true,ifeq(point(X1),true,ifeq(point(X2),true,ifeq(collinear(X0,X1,X2),true,or(eq(X0,X1),or(eq(X0,X2),or(eq(X1,X2),line(line_through_3_points(X0,X1,X2))))),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t227,plain,
or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),line(line_through_3_points(point1,point2,point3))))) = true,
inference(hyper_resolution,[status(thm)],[hi26,hi28,hi29,hi30,hi34]) ).
cnf(t267,plain,
or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),line(line_through_3_points(point1,point2,point3))))) = true,
inference(orient,[status(thm)],[t227]) ).
cnf(t15987,plain,
or(eq(point1,point2),or(eq(point1,point3),or(false,line(line_through_3_points(point1,point2,point3))))) = true,
inference(step,[status(thm)],[t267,t1223]) ).
cnf(t15988,plain,
or(eq(point1,point2),or(eq(point1,point3),line(line_through_3_points(point1,point2,point3)))) = true,
inference(step,[status(thm)],[t15987,t257]) ).
cnf(t1269,plain,
or(eq(point1,point2),or(eq(point1,point3),line(line_through_3_points(point1,point2,point3)))) = true,
inference(rw,[status(thm)],[t15988]) ).
cnf(t16186,plain,
or(false,or(eq(point1,point3),line(line_through_3_points(point1,point2,point3)))) = true,
inference(step,[status(thm)],[t1269,t1272]) ).
cnf(t16187,plain,
or(eq(point1,point3),line(line_through_3_points(point1,point2,point3))) = true,
inference(step,[status(thm)],[t16186,t257]) ).
cnf(t16188,plain,
or(false,line(line_through_3_points(point1,point2,point3))) = true,
inference(step,[status(thm)],[t16187,t1317]) ).
cnf(t16189,plain,
line(line_through_3_points(point1,point2,point3)) = true,
inference(step,[status(thm)],[t16188,t257]) ).
cnf(t3669,plain,
line(line_through_3_points(point1,point2,point3)) = true,
inference(orient,[status(thm)],[t16189]) ).
cnf(t18785,plain,
true = ifeq(true,true,or(eq(point1,point2),eq(a_line,line_through_3_points(point1,point2,point3))),true),
inference(step,[status(thm)],[t18784,t3669]) ).
cnf(t18786,plain,
true = or(eq(point1,point2),eq(a_line,line_through_3_points(point1,point2,point3))),
inference(step,[status(thm)],[t18785,t258]) ).
cnf(t18787,plain,
true = or(false,eq(a_line,line_through_3_points(point1,point2,point3))),
inference(step,[status(thm)],[t18786,t1272]) ).
cnf(t18788,plain,
true = eq(a_line,line_through_3_points(point1,point2,point3)),
inference(step,[status(thm)],[t18787,t257]) ).
cnf(t15850,plain,
eq(a_line,line_through_3_points(point1,point2,point3)) = true,
inference(orient,[status(thm)],[t18788]) ).
cnf(t15851,plain,
line_through_3_points(point1,point2,point3) = ifeq(true,true,a_line,line_through_3_points(point1,point2,point3)),
inference(cp,[status(thm)],[t259,t15850]) ).
cnf(t18789,plain,
line_through_3_points(point1,point2,point3) = a_line,
inference(step,[status(thm)],[t15851,t258]) ).
cnf(t15892,plain,
line_through_3_points(point1,point2,point3) = a_line,
inference(orient,[status(thm)],[t18789]) ).
cnf(t15893,plain,
true = ifeq(point(point1),true,ifeq(point(point2),true,ifeq(point(point3),true,ifeq(collinear(point1,point2,point3),true,or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line)))),true),true),true),true),
inference(cp,[status(thm)],[t724,t15892]) ).
cnf(t18792,plain,
true = ifeq(true,true,ifeq(point(point2),true,ifeq(point(point3),true,ifeq(collinear(point1,point2,point3),true,or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line)))),true),true),true),true),
inference(step,[status(thm)],[t15893,t859]) ).
cnf(t18793,plain,
true = ifeq(point(point2),true,ifeq(point(point3),true,ifeq(collinear(point1,point2,point3),true,or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line)))),true),true),true),
inference(step,[status(thm)],[t18792,t258]) ).
cnf(t18794,plain,
true = ifeq(true,true,ifeq(point(point3),true,ifeq(collinear(point1,point2,point3),true,or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line)))),true),true),true),
inference(step,[status(thm)],[t18793,t814]) ).
cnf(t18795,plain,
true = ifeq(point(point3),true,ifeq(collinear(point1,point2,point3),true,or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line)))),true),true),
inference(step,[status(thm)],[t18794,t258]) ).
cnf(t6,plain,
point(point3) = true,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(t1084,plain,
point(point3) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t18796,plain,
true = ifeq(true,true,ifeq(collinear(point1,point2,point3),true,or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line)))),true),true),
inference(step,[status(thm)],[t18795,t1084]) ).
cnf(t18797,plain,
true = ifeq(collinear(point1,point2,point3),true,or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line)))),true),
inference(step,[status(thm)],[t18796,t258]) ).
cnf(t24,plain,
collinear(point1,point2,point3) = true,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(t1219,plain,
collinear(point1,point2,point3) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t18798,plain,
true = ifeq(true,true,or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line)))),true),
inference(step,[status(thm)],[t18797,t1219]) ).
cnf(t18799,plain,
true = or(eq(point1,point2),or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line)))),
inference(step,[status(thm)],[t18798,t258]) ).
cnf(t18800,plain,
true = or(false,or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line)))),
inference(step,[status(thm)],[t18799,t1272]) ).
cnf(t18801,plain,
true = or(eq(point1,point3),or(eq(point2,point3),on(point3,a_line))),
inference(step,[status(thm)],[t18800,t257]) ).
cnf(t18802,plain,
true = or(false,or(eq(point2,point3),on(point3,a_line))),
inference(step,[status(thm)],[t18801,t1317]) ).
cnf(t18803,plain,
true = or(eq(point2,point3),on(point3,a_line)),
inference(step,[status(thm)],[t18802,t257]) ).
cnf(t18804,plain,
true = or(false,on(point3,a_line)),
inference(step,[status(thm)],[t18803,t1223]) ).
cnf(t18805,plain,
true = on(point3,a_line),
inference(step,[status(thm)],[t18804,t257]) ).
cnf(f37,hypothesis,
~ on(point3,a_line),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',point3_not_on_line) ).
fof(f37_nnf,plain,
~ on(point3,a_line),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
~ on(point3,a_line),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
~ on(point3,a_line),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(t13,plain,
on(point3,a_line) = false,
inference(equality_encoding,[status(esa)],[c37]) ).
cnf(t1362,plain,
on(point3,a_line) = false,
inference(orient,[status(thm)],[t13]) ).
cnf(t18806,plain,
true = false,
inference(step,[status(thm)],[t18805,t1362]) ).
cnf(t15895,plain,
false = true,
inference(orient,[status(thm)],[t18806]) ).
cnf(f8,axiom,
( ~ line(Y1)
| point_1_on_line(Y1) != point_2_on_line(Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_G2E) ).
fof(f8_nnf,plain,
! [Y1] :
( ~ line(Y1)
| point_1_on_line(Y1) != point_2_on_line(Y1) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [Y1] :
( ~ line(Y1)
| point_1_on_line(Y1) != point_2_on_line(Y1) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( ~ line(X0)
| point_1_on_line(X0) != point_2_on_line(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(f9,axiom,
( ~ line(Y1)
| ~ on(point_not_on_line(Y1),Y1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_G3A) ).
fof(f9_nnf,plain,
! [Y1] :
( ~ line(Y1)
| ~ on(point_not_on_line(Y1),Y1) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [Y1] :
( ~ line(Y1)
| ~ on(point_not_on_line(Y1),Y1) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( ~ line(X0)
| ~ on(point_not_on_line(X0),X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(f14,axiom,
( ~ on(point_not_on_plane(Z1),Z1)
| ~ plane(Z1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_G6A) ).
fof(f14_nnf,plain,
! [Z1] :
( ~ on(point_not_on_plane(Z1),Z1)
| ~ plane(Z1) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Z1] :
( ~ on(point_not_on_plane(Z1),Z1)
| ~ plane(Z1) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( ~ on(point_not_on_plane(X0),X0)
| ~ plane(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c8,c9,c14,c37,c38,c39,c40]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t15895]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO077-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 10:45:31 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 67.18/8.93 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 67.18/8.93 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------