%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO258+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n010.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:17:45 PM UTC 2026
% Result : Theorem 17.38s 2.91s
% Output : Proof 17.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 10
% Syntax : Number of formulae : 77 ( 24 unt; 0 def)
% Number of atoms : 189 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 171 ( 59 ~; 79 |; 25 &)
% ( 3 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 124 ( 2 sgn 71 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [L,A,B,C] :
( between_on_line(L,A,B,C)
<=> ( ( before_on_line(L,B,A)
& before_on_line(L,C,B) )
| ( before_on_line(L,B,C)
& before_on_line(L,A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a9_defns) ).
fof(f9_nnf,plain,
! [L,A,B,C] :
( ( ( ( ~ before_on_line(L,B,A)
| ~ before_on_line(L,C,B) )
& ( ~ before_on_line(L,B,C)
| ~ before_on_line(L,A,B) ) )
| between_on_line(L,A,B,C) )
& ( ( before_on_line(L,B,A)
& before_on_line(L,C,B) )
| ( before_on_line(L,B,C)
& before_on_line(L,A,B) )
| ~ between_on_line(L,A,B,C) ) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [L,A,B,C] :
( ( ( ( ~ before_on_line(L,B,A)
| ~ before_on_line(L,C,B) )
& ( ~ before_on_line(L,B,C)
| ~ before_on_line(L,A,B) ) )
| between_on_line(L,A,B,C) )
& ( ( before_on_line(L,B,A)
& before_on_line(L,C,B) )
| ( before_on_line(L,B,C)
& before_on_line(L,A,B) )
| ~ between_on_line(L,A,B,C) ) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c31,plain,
( ~ before_on_line(X0,X2,X3)
| ~ before_on_line(X0,X1,X2)
| between_on_line(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(c27,plain,
( before_on_line(X0,X3,X2)
| before_on_line(X0,X1,X2)
| ~ between_on_line(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f36,conjecture,
! [L,A,B,C] :
( between_on_line(L,A,B,C)
=> between_on_line(L,C,B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',con) ).
fof(f36_neg,negated_conjecture,
~ ! [L,A,B,C] :
( between_on_line(L,A,B,C)
=> between_on_line(L,C,B,A) ),
inference(negated_conjecture,[status(cth)],[f36]) ).
fof(f36_nnf,plain,
? [L,A,B,C] :
( ~ between_on_line(L,C,B,A)
& between_on_line(L,A,B,C) ),
inference(nnf_transformation,[status(thm)],[f36_neg]) ).
fof(f36_sk,plain,
( ~ between_on_line(sk0,sk3,sk2,sk1)
& between_on_line(sk0,sk1,sk2,sk3) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3])],[f36_nnf]) ).
cnf(c66,plain,
between_on_line(sk0,sk1,sk2,sk3),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p120,plain,
( before_on_line(sk0,sk3,sk2)
| before_on_line(sk0,sk1,sk2) ),
inference(resolution,[status(thm)],[c27,c66]) ).
cnf(p150,plain,
( before_on_line(sk0,sk1,sk2)
| ~ before_on_line(sk0,sk2,X0)
| between_on_line(sk0,sk3,sk2,X0) ),
inference(resolution,[status(thm)],[c31,p120]) ).
cnf(c28,plain,
( before_on_line(X0,X2,X1)
| before_on_line(X0,X1,X2)
| ~ between_on_line(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p134,plain,
( before_on_line(sk0,sk2,sk1)
| before_on_line(sk0,sk1,sk2) ),
inference(resolution,[status(thm)],[c28,c66]) ).
cnf(p1190,plain,
( before_on_line(sk0,sk1,sk2)
| before_on_line(sk0,sk1,sk2)
| between_on_line(sk0,sk3,sk2,sk1) ),
inference(resolution,[status(thm)],[p150,p134]) ).
cnf(p6619,plain,
( before_on_line(sk0,sk1,sk2)
| between_on_line(sk0,sk3,sk2,sk1) ),
inference(factoring,[status(thm)],[p1190]) ).
cnf(c67,plain,
~ between_on_line(sk0,sk3,sk2,sk1),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p6620,plain,
before_on_line(sk0,sk1,sk2),
inference(resolution,[status(thm)],[p6619,c67]) ).
cnf(c32,plain,
( ~ before_on_line(X0,X2,X1)
| ~ before_on_line(X0,X3,X2)
| between_on_line(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p6785,plain,
( ~ before_on_line(sk0,sk2,X0)
| between_on_line(sk0,X0,sk2,sk1) ),
inference(resolution,[status(thm)],[p6620,c32]) ).
cnf(c30,plain,
( before_on_line(X0,X2,X1)
| before_on_line(X0,X2,X3)
| ~ between_on_line(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p146,plain,
( before_on_line(sk0,sk2,sk1)
| before_on_line(sk0,sk2,sk3) ),
inference(resolution,[status(thm)],[c30,c66]) ).
cnf(p7129,plain,
( before_on_line(sk0,sk2,sk1)
| between_on_line(sk0,sk3,sk2,sk1) ),
inference(resolution,[status(thm)],[p6785,p146]) ).
cnf(p7401,plain,
before_on_line(sk0,sk2,sk1),
inference(resolution,[status(thm)],[p7129,c67]) ).
fof(f8,axiom,
! [L,A,B] :
( before_on_line(L,A,B)
<=> ( equally_directed_lines(L,line_connecting(A,B))
& incident_point_and_line(B,L)
& incident_point_and_line(A,L)
& distinct_points(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4_defns) ).
fof(f8_nnf,plain,
! [L,A,B] :
( ( ~ equally_directed_lines(L,line_connecting(A,B))
| ~ incident_point_and_line(B,L)
| ~ incident_point_and_line(A,L)
| ~ distinct_points(A,B)
| before_on_line(L,A,B) )
& ( ( equally_directed_lines(L,line_connecting(A,B))
& incident_point_and_line(B,L)
& incident_point_and_line(A,L)
& distinct_points(A,B) )
| ~ before_on_line(L,A,B) ) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [L,A,B] :
( ( ~ equally_directed_lines(L,line_connecting(A,B))
| ~ incident_point_and_line(B,L)
| ~ incident_point_and_line(A,L)
| ~ distinct_points(A,B)
| before_on_line(L,A,B) )
& ( ( equally_directed_lines(L,line_connecting(A,B))
& incident_point_and_line(B,L)
& incident_point_and_line(A,L)
& distinct_points(A,B) )
| ~ before_on_line(L,A,B) ) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c25,plain,
( equally_directed_lines(X0,line_connecting(X1,X2))
| ~ before_on_line(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p7402,plain,
equally_directed_lines(sk0,line_connecting(sk2,sk1)),
inference(resolution,[status(thm)],[p7401,c25]) ).
fof(f3,axiom,
! [X,Y] :
( equally_directed_lines(X,Y)
<=> ~ unequally_directed_lines(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4_defns) ).
fof(f3_nnf,plain,
! [X,Y] :
( ( unequally_directed_lines(X,Y)
| equally_directed_lines(X,Y) )
& ( ~ unequally_directed_lines(X,Y)
| ~ equally_directed_lines(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] :
( ( unequally_directed_lines(X,Y)
| equally_directed_lines(X,Y) )
& ( ~ unequally_directed_lines(X,Y)
| ~ equally_directed_lines(X,Y) ) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c6,plain,
( ~ unequally_directed_lines(X0,X1)
| ~ equally_directed_lines(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p7407,plain,
~ unequally_directed_lines(sk0,line_connecting(sk2,sk1)),
inference(resolution,[status(thm)],[p7402,c6]) ).
cnf(c22,plain,
( distinct_points(X1,X2)
| ~ before_on_line(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p153,plain,
( distinct_points(sk2,sk1)
| before_on_line(sk0,sk1,sk2) ),
inference(resolution,[status(thm)],[p134,c22]) ).
cnf(p157,plain,
( distinct_points(sk1,sk2)
| distinct_points(sk2,sk1) ),
inference(resolution,[status(thm)],[p153,c22]) ).
fof(f11,axiom,
! [A,B,C] :
( distinct_points(A,B)
=> ( distinct_points(B,C)
| distinct_points(A,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_basics) ).
fof(f11_nnf,plain,
! [A,B,C] :
( distinct_points(B,C)
| distinct_points(A,C)
| ~ distinct_points(A,B) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A,B,C] :
( distinct_points(B,C)
| distinct_points(A,C)
| ~ distinct_points(A,B) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c34,plain,
( distinct_points(X1,X2)
| distinct_points(X0,X2)
| ~ distinct_points(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p163,plain,
( distinct_points(sk1,X0)
| distinct_points(sk2,X0)
| distinct_points(sk1,sk2) ),
inference(resolution,[status(thm)],[p157,c34]) ).
cnf(p339,plain,
( distinct_points(sk2,sk2)
| distinct_points(sk1,sk2) ),
inference(factoring,[status(thm)],[p163]) ).
fof(f10,axiom,
! [A] : ~ distinct_points(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_basics) ).
fof(f10_nnf,plain,
! [A] : ~ distinct_points(A,A),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A] : ~ distinct_points(A,A),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c33,plain,
~ distinct_points(X0,X0),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p347,plain,
distinct_points(sk1,sk2),
inference(resolution,[status(thm)],[p339,c33]) ).
fof(f29,axiom,
! [A,B] :
( distinct_points(A,B)
=> equally_directed_lines(line_connecting(A,B),reverse_line(line_connecting(B,A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9_cons_objs) ).
fof(f29_nnf,plain,
! [A,B] :
( equally_directed_lines(line_connecting(A,B),reverse_line(line_connecting(B,A)))
| ~ distinct_points(A,B) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [A,B] :
( equally_directed_lines(line_connecting(A,B),reverse_line(line_connecting(B,A)))
| ~ distinct_points(A,B) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c59,plain,
( equally_directed_lines(line_connecting(X0,X1),reverse_line(line_connecting(X1,X0)))
| ~ distinct_points(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p352,plain,
equally_directed_lines(line_connecting(sk1,sk2),reverse_line(line_connecting(sk2,sk1))),
inference(resolution,[status(thm)],[p347,c59]) ).
cnf(p360,plain,
~ unequally_directed_lines(line_connecting(sk1,sk2),reverse_line(line_connecting(sk2,sk1))),
inference(resolution,[status(thm)],[p352,c6]) ).
fof(f17,axiom,
! [L,M] :
( unequally_directed_lines(L,reverse_line(M))
| unequally_directed_lines(L,M) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8_basics) ).
fof(f17_nnf,plain,
! [L,M] :
( unequally_directed_lines(L,reverse_line(M))
| unequally_directed_lines(L,M) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [L,M] :
( unequally_directed_lines(L,reverse_line(M))
| unequally_directed_lines(L,M) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c43,plain,
( unequally_directed_lines(X0,reverse_line(X1))
| unequally_directed_lines(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p361,plain,
unequally_directed_lines(line_connecting(sk1,sk2),line_connecting(sk2,sk1)),
inference(resolution,[status(thm)],[p360,c43]) ).
fof(f15,axiom,
! [L,M,N] :
( unequally_directed_lines(L,M)
=> ( unequally_directed_lines(M,N)
| unequally_directed_lines(L,N) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6_basics) ).
fof(f15_nnf,plain,
! [L,M,N] :
( unequally_directed_lines(M,N)
| unequally_directed_lines(L,N)
| ~ unequally_directed_lines(L,M) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [L,M,N] :
( unequally_directed_lines(M,N)
| unequally_directed_lines(L,N)
| ~ unequally_directed_lines(L,M) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c38,plain,
( unequally_directed_lines(X1,X2)
| unequally_directed_lines(X0,X2)
| ~ unequally_directed_lines(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p365,plain,
( unequally_directed_lines(line_connecting(sk2,sk1),X0)
| unequally_directed_lines(line_connecting(sk1,sk2),X0) ),
inference(resolution,[status(thm)],[p361,c38]) ).
cnf(p591,plain,
( unequally_directed_lines(X0,X1)
| unequally_directed_lines(line_connecting(sk2,sk1),X1)
| unequally_directed_lines(line_connecting(sk1,sk2),X0) ),
inference(resolution,[status(thm)],[p365,c38]) ).
fof(f14,axiom,
! [L] : equally_directed_lines(L,L),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5_basics) ).
fof(f14_nnf,plain,
! [L] : equally_directed_lines(L,L),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [L] : equally_directed_lines(L,L),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c37,plain,
equally_directed_lines(X0,X0),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p68,plain,
~ unequally_directed_lines(X0,X0),
inference(resolution,[status(thm)],[c6,c37]) ).
cnf(p4414,plain,
( unequally_directed_lines(X0,line_connecting(sk2,sk1))
| unequally_directed_lines(line_connecting(sk1,sk2),X0) ),
inference(resolution,[status(thm)],[p591,p68]) ).
cnf(p7421,plain,
unequally_directed_lines(line_connecting(sk1,sk2),sk0),
inference(resolution,[status(thm)],[p7407,p4414]) ).
cnf(p7778,plain,
( unequally_directed_lines(sk0,X0)
| unequally_directed_lines(line_connecting(sk1,sk2),X0) ),
inference(resolution,[status(thm)],[p7421,c38]) ).
cnf(p8521,plain,
unequally_directed_lines(sk0,line_connecting(sk1,sk2)),
inference(resolution,[status(thm)],[p7778,p68]) ).
cnf(p6783,plain,
equally_directed_lines(sk0,line_connecting(sk1,sk2)),
inference(resolution,[status(thm)],[p6620,c25]) ).
cnf(p6786,plain,
~ unequally_directed_lines(sk0,line_connecting(sk1,sk2)),
inference(resolution,[status(thm)],[p6783,c6]) ).
cnf(p8565,plain,
$false,
inference(resolution,[status(thm)],[p8521,p6786]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO258+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.33 % Computer : n010.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Wed Sep 23 11:44:12 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.34 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 17.38/2.91 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.38/2.91 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------