%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO127+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n006.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:07 PM UTC 2026
% Result : Theorem 235.92s 30.29s
% Output : Proof 235.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 9
% Syntax : Number of formulae : 67 ( 23 unt; 0 def)
% Number of atoms : 203 ( 17 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 208 ( 72 ~; 77 |; 49 &)
% ( 7 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 107 ( 5 sgn 59 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [P,O] :
( start_point(P,O)
<=> ( ! [Q] :
( ( incident_o(Q,O)
& P != Q )
=> ordered_by(O,P,Q) )
& incident_o(P,O) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',start_point_defn) ).
fof(f18_nnf,plain,
! [P,O] :
( ( ? [Q] :
( ~ ordered_by(O,P,Q)
& incident_o(Q,O)
& P != Q )
| ~ incident_o(P,O)
| start_point(P,O) )
& ( ( ! [Q] :
( ordered_by(O,P,Q)
| ~ incident_o(Q,O)
| P = Q )
& incident_o(P,O) )
| ~ start_point(P,O) ) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [P,O,Q] :
( ( ( ~ ordered_by(O,P,sk14(P,O))
& incident_o(sk14(P,O),O)
& P != sk14(P,O) )
| ~ incident_o(P,O)
| start_point(P,O) )
& ( ( ( ordered_by(O,P,Q)
| ~ incident_o(Q,O)
| P = Q )
& incident_o(P,O) )
| ~ start_point(P,O) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14])],[f18_nnf]) ).
cnf(c61,plain,
( ordered_by(X1,X0,X2)
| ~ incident_o(X2,X1)
| X0 = X2
| ~ start_point(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
fof(f23,axiom,
! [O] :
? [P] : start_point(P,O),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o4) ).
fof(f23_nnf,plain,
! [O] :
? [P] : start_point(P,O),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [O] : start_point(sk19(O),O),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk19])],[f23_nnf]) ).
cnf(c82,plain,
start_point(sk19(X0),X0),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p1719,plain,
( ordered_by(X0,sk19(X0),X1)
| ~ incident_o(X1,X0)
| sk19(X0) = X1 ),
inference(resolution,[status(thm)],[c61,c82]) ).
fof(f27,conjecture,
! [O,P] :
( incident_o(P,O)
<=> ? [Q] :
( ordered_by(O,Q,P)
| ordered_by(O,P,Q) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_12) ).
fof(f27_neg,negated_conjecture,
~ ! [O,P] :
( incident_o(P,O)
<=> ? [Q] :
( ordered_by(O,Q,P)
| ordered_by(O,P,Q) ) ),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f27_nnf,plain,
? [O,P] :
( ( ? [Q] :
( ordered_by(O,Q,P)
| ordered_by(O,P,Q) )
& ~ incident_o(P,O) )
| ( ! [Q] :
( ~ ordered_by(O,Q,P)
& ~ ordered_by(O,P,Q) )
& incident_o(P,O) ) ),
inference(nnf_transformation,[status(thm)],[f27_neg]) ).
fof(f27_sk,plain,
! [Q] :
( ( ( ordered_by(sk24,sk26,sk25)
| ordered_by(sk24,sk25,sk26) )
& ~ incident_o(sk25,sk24) )
| ( ~ ordered_by(sk24,Q,sk25)
& ~ ordered_by(sk24,sk25,Q)
& incident_o(sk25,sk24) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk24,sk25,sk26])],[f27_nnf]) ).
cnf(c97,plain,
( ordered_by(sk24,sk26,sk25)
| ordered_by(sk24,sk25,sk26)
| incident_o(sk25,sk24) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
fof(f20,axiom,
! [O,P,Q] :
( ordered_by(O,P,Q)
=> ( incident_o(Q,O)
& incident_o(P,O) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o1) ).
fof(f20_nnf,plain,
! [O,P,Q] :
( ( incident_o(Q,O)
& incident_o(P,O) )
| ~ ordered_by(O,P,Q) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [O,P,Q] :
( ( incident_o(Q,O)
& incident_o(P,O) )
| ~ ordered_by(O,P,Q) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c71,plain,
( incident_o(X2,X0)
| ~ ordered_by(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p2956,plain,
( incident_o(sk25,sk24)
| ordered_by(sk24,sk25,sk26)
| incident_o(sk25,sk24) ),
inference(resolution,[status(thm)],[c97,c71]) ).
cnf(p6020,plain,
( ordered_by(sk24,sk25,sk26)
| incident_o(sk25,sk24) ),
inference(factoring,[status(thm)],[p2956]) ).
cnf(c70,plain,
( incident_o(X1,X0)
| ~ ordered_by(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p6033,plain,
( incident_o(sk25,sk24)
| incident_o(sk25,sk24) ),
inference(resolution,[status(thm)],[p6020,c70]) ).
cnf(p6036,plain,
incident_o(sk25,sk24),
inference(factoring,[status(thm)],[p6033]) ).
cnf(p22620,plain,
( ordered_by(sk24,sk19(sk24),sk25)
| sk19(sk24) = sk25 ),
inference(resolution,[status(thm)],[p1719,p6036]) ).
cnf(c100,plain,
( ~ incident_o(sk25,sk24)
| ~ ordered_by(sk24,X2,sk25) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p22678,plain,
( ~ incident_o(sk25,sk24)
| sk19(sk24) = sk25 ),
inference(resolution,[status(thm)],[p22620,c100]) ).
cnf(p22699,plain,
sk19(sk24) = sk25,
inference(resolution,[status(thm)],[p22678,p6036]) ).
cnf(p22702,plain,
start_point(sk25,sk24),
inference(superposition,[status(thm)],[p22699,c82]) ).
cnf(p22748,plain,
( ordered_by(sk24,sk25,X0)
| ~ incident_o(X0,sk24)
| sk25 = X0 ),
inference(resolution,[status(thm)],[p22702,c61]) ).
fof(f21,axiom,
! [O] :
? [C] :
( ! [P] :
( incident_o(P,O)
<=> incident_c(P,C) )
& open(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',o2) ).
fof(f21_nnf,plain,
! [O] :
? [C] :
( ! [P] :
( ( ~ incident_c(P,C)
| incident_o(P,O) )
& ( incident_c(P,C)
| ~ incident_o(P,O) ) )
& open(C) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [O,P] :
( ( ~ incident_c(P,sk16(O))
| incident_o(P,O) )
& ( incident_c(P,sk16(O))
| ~ incident_o(P,O) )
& open(sk16(O)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk16])],[f21_nnf]) ).
cnf(c74,plain,
( ~ incident_c(X2,sk16(X0))
| incident_o(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
fof(f6,axiom,
! [C] :
( open(C)
<=> ? [P] : end_point(P,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',open_defn) ).
fof(f6_nnf,plain,
! [C] :
( ( ! [P] : ~ end_point(P,C)
| open(C) )
& ( ? [P] : end_point(P,C)
| ~ open(C) ) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [C,P] :
( ( ~ end_point(P,C)
| open(C) )
& ( end_point(sk6(C),C)
| ~ open(C) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk6])],[f6_nnf]) ).
cnf(c32,plain,
( end_point(sk6(X0),X0)
| ~ open(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(c72,plain,
open(sk16(X0)),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p107,plain,
end_point(sk6(sk16(X0)),sk16(X0)),
inference(resolution,[status(thm)],[c32,c72]) ).
fof(f2,axiom,
! [P,C] :
( end_point(P,C)
<=> ( ! [C1,C2] :
( ( incident_c(P,C2)
& incident_c(P,C1)
& part_of(C2,C)
& part_of(C1,C) )
=> ( part_of(C2,C1)
| part_of(C1,C2) ) )
& incident_c(P,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',end_point_defn) ).
fof(f2_nnf,plain,
! [P,C] :
( ( ? [C1,C2] :
( ~ part_of(C2,C1)
& ~ part_of(C1,C2)
& incident_c(P,C2)
& incident_c(P,C1)
& part_of(C2,C)
& part_of(C1,C) )
| ~ incident_c(P,C)
| end_point(P,C) )
& ( ( ! [C1,C2] :
( part_of(C2,C1)
| part_of(C1,C2)
| ~ incident_c(P,C2)
| ~ incident_c(P,C1)
| ~ part_of(C2,C)
| ~ part_of(C1,C) )
& incident_c(P,C) )
| ~ end_point(P,C) ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [P,C,C1,C2] :
( ( ( ~ part_of(sk3(P,C),sk2(P,C))
& ~ part_of(sk2(P,C),sk3(P,C))
& incident_c(P,sk3(P,C))
& incident_c(P,sk2(P,C))
& part_of(sk3(P,C),C)
& part_of(sk2(P,C),C) )
| ~ incident_c(P,C)
| end_point(P,C) )
& ( ( ( part_of(C2,C1)
| part_of(C1,C2)
| ~ incident_c(P,C2)
| ~ incident_c(P,C1)
| ~ part_of(C2,C)
| ~ part_of(C1,C) )
& incident_c(P,C) )
| ~ end_point(P,C) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2,sk3])],[f2_nnf]) ).
cnf(c12,plain,
( incident_c(X0,X1)
| ~ end_point(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p109,plain,
incident_c(sk6(sk16(X0)),sk16(X0)),
inference(resolution,[status(thm)],[p107,c12]) ).
cnf(p120,plain,
incident_o(sk6(sk16(X0)),X0),
inference(resolution,[status(thm)],[c74,p109]) ).
cnf(p23557,plain,
( ordered_by(sk24,sk25,sk6(sk16(sk24)))
| sk25 = sk6(sk16(sk24)) ),
inference(resolution,[status(thm)],[p22748,p120]) ).
cnf(c98,plain,
( ~ incident_o(sk25,sk24)
| ~ ordered_by(sk24,sk25,X2) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p34998,plain,
( ~ incident_o(sk25,sk24)
| sk25 = sk6(sk16(sk24)) ),
inference(resolution,[status(thm)],[p23557,c98]) ).
cnf(p35207,plain,
sk25 = sk6(sk16(sk24)),
inference(resolution,[status(thm)],[p34998,p6036]) ).
cnf(p35208,plain,
end_point(sk25,sk16(sk24)),
inference(superposition,[status(thm)],[p35207,p107]) ).
fof(f3,axiom,
! [P,C] :
( inner_point(P,C)
<=> ( ~ end_point(P,C)
& incident_c(P,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inner_point_defn) ).
fof(f3_nnf,plain,
! [P,C] :
( ( end_point(P,C)
| ~ incident_c(P,C)
| inner_point(P,C) )
& ( ( ~ end_point(P,C)
& incident_c(P,C) )
| ~ inner_point(P,C) ) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [P,C] :
( ( end_point(P,C)
| ~ incident_c(P,C)
| inner_point(P,C) )
& ( ( ~ end_point(P,C)
& incident_c(P,C) )
| ~ inner_point(P,C) ) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c20,plain,
( incident_c(X0,X1)
| ~ inner_point(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
fof(f9,axiom,
! [C] :
? [P] : inner_point(P,C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c3) ).
fof(f9_nnf,plain,
! [C] :
? [P] : inner_point(P,C),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [C] : inner_point(sk7(C),C),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7])],[f9_nnf]) ).
cnf(c36,plain,
inner_point(sk7(X0),X0),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p102,plain,
incident_c(sk7(X0),X0),
inference(resolution,[status(thm)],[c20,c36]) ).
cnf(p118,plain,
incident_o(sk7(sk16(X0)),X0),
inference(resolution,[status(thm)],[c74,p102]) ).
cnf(p23556,plain,
( ordered_by(sk24,sk25,sk7(sk16(sk24)))
| sk25 = sk7(sk16(sk24)) ),
inference(resolution,[status(thm)],[p22748,p118]) ).
cnf(p23640,plain,
( ~ incident_o(sk25,sk24)
| sk25 = sk7(sk16(sk24)) ),
inference(resolution,[status(thm)],[p23556,c98]) ).
cnf(p23644,plain,
sk25 = sk7(sk16(sk24)),
inference(resolution,[status(thm)],[p23640,p6036]) ).
cnf(c21,plain,
( ~ end_point(X0,X1)
| ~ inner_point(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p103,plain,
~ end_point(sk7(X0),X0),
inference(resolution,[status(thm)],[c21,c36]) ).
cnf(p23646,plain,
~ end_point(sk25,sk16(sk24)),
inference(superposition,[status(thm)],[p23644,p103]) ).
cnf(p35335,plain,
$false,
inference(resolution,[status(thm)],[p35208,p23646]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO127+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 11:01:14 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 235.92/30.29 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 235.92/30.29 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------