%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO147+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 : 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:17:10 PM UTC 2026
% Result : Theorem 7.57s 6.42s
% Output : Proof 7.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 10
% Syntax : Number of formulae : 60 ( 22 unt; 0 def)
% Number of atoms : 161 ( 30 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 175 ( 74 ~; 54 |; 37 &)
% ( 5 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-4 aty)
% Number of variables : 126 ( 7 sgn 79 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f27,axiom,
! [X,Y,P] :
( connect(X,Y,P)
<=> once(at_the_same_time(at(X,P),at(Y,P))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',connect_defn) ).
fof(f27_nnf,plain,
! [X,Y,P] :
( ( ~ once(at_the_same_time(at(X,P),at(Y,P)))
| connect(X,Y,P) )
& ( once(at_the_same_time(at(X,P),at(Y,P)))
| ~ connect(X,Y,P) ) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [X,Y,P] :
( ( ~ once(at_the_same_time(at(X,P),at(Y,P)))
| connect(X,Y,P) )
& ( once(at_the_same_time(at(X,P),at(Y,P)))
| ~ connect(X,Y,P) ) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c96,plain,
( once(at_the_same_time(at(X0,X2),at(X1,X2)))
| ~ connect(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(hi81,axiom,
ifeq(connect(X0,X1,X2),true,once(at_the_same_time(at(X0,X2),at(X1,X2))),true) = true,
inference(equality_encoding,[status(esa)],[c96]) ).
fof(f36,conjecture,
! [P,X,Y] :
( connect(X,Y,P)
=> ( incident_o(P,trajectory_of(Y))
& incident_o(P,trajectory_of(X)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13) ).
fof(f36_neg,negated_conjecture,
~ ! [P,X,Y] :
( connect(X,Y,P)
=> ( incident_o(P,trajectory_of(Y))
& incident_o(P,trajectory_of(X)) ) ),
inference(negated_conjecture,[status(cth)],[f36]) ).
fof(f36_nnf,plain,
? [P,X,Y] :
( ( ~ incident_o(P,trajectory_of(Y))
| ~ incident_o(P,trajectory_of(X)) )
& connect(X,Y,P) ),
inference(nnf_transformation,[status(thm)],[f36_neg]) ).
fof(f36_sk,plain,
( ( ~ incident_o(sk26,trajectory_of(sk28))
| ~ incident_o(sk26,trajectory_of(sk27)) )
& connect(sk27,sk28,sk26) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk26,sk27,sk28])],[f36_nnf]) ).
cnf(c110,plain,
connect(sk27,sk28,sk26),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(hi94,negated_conjecture,
connect(sk27,sk28,sk26) = true,
inference(equality_encoding,[status(esa)],[c110]) ).
cnf(h5,plain,
once(at_the_same_time(at(sk27,sk26),at(sk28,sk26))) = true,
inference(hyper_resolution,[status(thm)],[hi81,hi94]) ).
fof(f31,axiom,
! [A,B] :
( once(at_the_same_time(A,B))
=> ( once(B)
& once(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjunction_at_the_same_time) ).
fof(f31_nnf,plain,
! [A,B] :
( ( once(B)
& once(A) )
| ~ once(at_the_same_time(A,B)) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [A,B] :
( ( once(B)
& once(A) )
| ~ once(at_the_same_time(A,B)) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c104,plain,
( once(X1)
| ~ once(at_the_same_time(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(hi89,axiom,
ifeq(once(at_the_same_time(X0,X1)),true,once(X1),true) = true,
inference(equality_encoding,[status(esa)],[c104]) ).
cnf(h196,plain,
once(at(sk28,sk26)) = true,
inference(hyper_resolution,[status(thm)],[hi89,h5]) ).
fof(f32,axiom,
! [X,P] :
( once(at(X,P))
<=> incident_o(P,trajectory_of(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',at_on_trajectory) ).
fof(f32_nnf,plain,
! [X,P] :
( ( ~ incident_o(P,trajectory_of(X))
| once(at(X,P)) )
& ( incident_o(P,trajectory_of(X))
| ~ once(at(X,P)) ) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [X,P] :
( ( ~ incident_o(P,trajectory_of(X))
| once(at(X,P)) )
& ( incident_o(P,trajectory_of(X))
| ~ once(at(X,P)) ) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c105,plain,
( incident_o(X1,trajectory_of(X0))
| ~ once(at(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(hi90,axiom,
ifeq(once(at(X0,X1)),true,incident_o(X1,trajectory_of(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c105]) ).
fof(f33,axiom,
! [X] :
? [O] : trajectory_of(X) = O,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',trajectories_are_oriented_curves) ).
fof(f33_nnf,plain,
! [X] :
? [O] : trajectory_of(X) = O,
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [X] : trajectory_of(X) = sk24(X),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk24])],[f33_nnf]) ).
cnf(c107,plain,
trajectory_of(X0) = sk24(X0),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(hi91,axiom,
trajectory_of(X0) = sk24(X0),
inference(equality_encoding,[status(esa)],[c107]) ).
cnf(h201,plain,
incident_o(sk26,trajectory_of(sk28)) = true,
inference(hyper_resolution,[status(thm)],[hi90,h196,hi91]) ).
cnf(c103,plain,
( once(X0)
| ~ once(at_the_same_time(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(hi88,axiom,
ifeq(once(at_the_same_time(X0,X1)),true,once(X0),true) = true,
inference(equality_encoding,[status(esa)],[c103]) ).
cnf(h197,plain,
once(at(sk27,sk26)) = true,
inference(hyper_resolution,[status(thm)],[hi88,h5]) ).
cnf(h204,plain,
incident_o(sk26,trajectory_of(sk27)) = true,
inference(hyper_resolution,[status(thm)],[hi90,h197,hi91]) ).
cnf(c111,plain,
( ~ incident_o(sk26,trajectory_of(sk28))
| ~ incident_o(sk26,trajectory_of(sk27)) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(hi100,negated_conjecture,
ifeq(incident_o(sk26,trajectory_of(sk27)),true,ifeq(incident_o(sk26,trajectory_of(sk28)),true,false,true),true) = true,
inference(equality_encoding,[status(esa)],[c111]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi100,h204,h201,hi91]) ).
cnf(t323,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
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(c21,plain,
( ~ end_point(X0,X1)
| ~ inner_point(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
fof(f5,axiom,
! [C] :
( closed(C)
<=> ~ ? [P] : end_point(P,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closed_defn) ).
fof(f5_nnf,plain,
! [C] :
( ( ? [P] : end_point(P,C)
| closed(C) )
& ( ! [P] : ~ end_point(P,C)
| ~ closed(C) ) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [C,P] :
( ( end_point(sk5(C),C)
| closed(C) )
& ( ~ end_point(P,C)
| ~ closed(C) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f5_nnf]) ).
cnf(c30,plain,
( ~ end_point(X1,X0)
| ~ closed(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f12,axiom,
! [C,P] :
( end_point(P,C)
=> ? [Q] :
( P != Q
& end_point(Q,C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c6) ).
fof(f12_nnf,plain,
! [C,P] :
( ? [Q] :
( P != Q
& end_point(Q,C) )
| ~ end_point(P,C) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [P,C] :
( ( P != sk10(C,P)
& end_point(sk10(C,P),C) )
| ~ end_point(P,C) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk10])],[f12_nnf]) ).
cnf(c41,plain,
( X1 != sk10(X0,X1)
| ~ end_point(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f16,axiom,
! [C,P,Q,R] :
( between_c(C,P,Q,R)
<=> ( ? [Cpp] :
( inner_point(Q,Cpp)
& end_point(R,Cpp)
& end_point(P,Cpp)
& part_of(Cpp,C) )
& P != R ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',between_c_defn) ).
fof(f16_nnf,plain,
! [C,P,Q,R] :
( ( ! [Cpp] :
( ~ inner_point(Q,Cpp)
| ~ end_point(R,Cpp)
| ~ end_point(P,Cpp)
| ~ part_of(Cpp,C) )
| P = R
| between_c(C,P,Q,R) )
& ( ( ? [Cpp] :
( inner_point(Q,Cpp)
& end_point(R,Cpp)
& end_point(P,Cpp)
& part_of(Cpp,C) )
& P != R )
| ~ between_c(C,P,Q,R) ) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [C,P,Q,R,Cpp] :
( ( ~ inner_point(Q,Cpp)
| ~ end_point(R,Cpp)
| ~ end_point(P,Cpp)
| ~ part_of(Cpp,C)
| P = R
| between_c(C,P,Q,R) )
& ( ( inner_point(Q,sk13(C,P,Q,R))
& end_point(R,sk13(C,P,Q,R))
& end_point(P,sk13(C,P,Q,R))
& part_of(sk13(C,P,Q,R),C)
& P != R )
| ~ between_c(C,P,Q,R) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13])],[f16_nnf]) ).
cnf(c48,plain,
( X1 != X3
| ~ between_c(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
fof(f34,axiom,
! [P1,P2,Q1,Q2,X,Y] :
( ( once(at_the_same_time(at(X,Q1),at(Y,Q2)))
& once(at_the_same_time(at(X,P1),at(Y,P2))) )
=> ~ ( ordered_by(trajectory_of(Y),Q2,P2)
& ordered_by(trajectory_of(X),P1,Q1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homogeneous_behaviour) ).
fof(f34_nnf,plain,
! [P1,P2,Q1,Q2,X,Y] :
( ~ ordered_by(trajectory_of(Y),Q2,P2)
| ~ ordered_by(trajectory_of(X),P1,Q1)
| ~ once(at_the_same_time(at(X,Q1),at(Y,Q2)))
| ~ once(at_the_same_time(at(X,P1),at(Y,P2))) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [X,P1,Y,P2,Q1,Q2] :
( ~ ordered_by(trajectory_of(Y),Q2,P2)
| ~ ordered_by(trajectory_of(X),P1,Q1)
| ~ once(at_the_same_time(at(X,Q1),at(Y,Q2)))
| ~ once(at_the_same_time(at(X,P1),at(Y,P2))) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c108,plain,
( ~ ordered_by(trajectory_of(X5),X3,X1)
| ~ ordered_by(trajectory_of(X4),X0,X2)
| ~ once(at_the_same_time(at(X4,X2),at(X5,X3)))
| ~ once(at_the_same_time(at(X4,X0),at(X5,X1))) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c21,c30,c41,c48,c108,c111]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t323]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO147+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.36 % Computer : n004.cluster.edu
% 0.10/5.36 % Model : x86_64 x86_64
% 0.10/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36 % Memory : 8046.5625MB
% 0.10/5.36 % OS : Linux 6.8.0-71-generic
% 0.10/5.36 % CPULimit : 300
% 0.10/5.36 % WCLimit : 300
% 0.10/5.36 % DateTime : Wed Sep 23 11:08:42 UTC 2026
% 0.10/5.36 % CPUTime :
% 0.10/5.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.57/6.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.57/6.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------