%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO148+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 : n009.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:11 PM UTC 2026
% Result : Theorem 8.45s 1.69s
% Output : Proof 8.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 8
% Syntax : Number of formulae : 49 ( 21 unt; 0 def)
% Number of atoms : 137 ( 26 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 149 ( 61 ~; 42 |; 36 &)
% ( 4 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-4 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-4 aty)
% Number of variables : 114 ( 3 sgn 71 !; 13 ?)
% 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)
=> ! [Q1,Q2] :
( ( ordered_by(trajectory_of(X),P,Q1)
& ordered_by(trajectory_of(Y),Q2,P) )
=> ~ once(at_the_same_time(at(X,Q1),at(Y,Q2))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t14) ).
fof(f36_neg,negated_conjecture,
~ ! [P,X,Y] :
( connect(X,Y,P)
=> ! [Q1,Q2] :
( ( ordered_by(trajectory_of(X),P,Q1)
& ordered_by(trajectory_of(Y),Q2,P) )
=> ~ once(at_the_same_time(at(X,Q1),at(Y,Q2))) ) ),
inference(negated_conjecture,[status(cth)],[f36]) ).
fof(f36_nnf,plain,
? [P,X,Y] :
( ? [Q1,Q2] :
( once(at_the_same_time(at(X,Q1),at(Y,Q2)))
& ordered_by(trajectory_of(X),P,Q1)
& ordered_by(trajectory_of(Y),Q2,P) )
& connect(X,Y,P) ),
inference(nnf_transformation,[status(thm)],[f36_neg]) ).
fof(f36_sk,plain,
( once(at_the_same_time(at(sk27,sk29),at(sk28,sk30)))
& ordered_by(trajectory_of(sk27),sk26,sk29)
& ordered_by(trajectory_of(sk28),sk30,sk26)
& connect(sk27,sk28,sk26) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk26,sk27,sk28,sk29,sk30])],[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(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(hi102,axiom,
ifeq(once(at_the_same_time(at(X0,X1),at(X2,X3))),true,ifeq(once(at_the_same_time(at(X0,X4),at(X2,X5))),true,ifeq(ordered_by(trajectory_of(X0),X1,X4),true,ifeq(ordered_by(trajectory_of(X2),X5,X3),true,false,true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c108]) ).
cnf(c113,plain,
once(at_the_same_time(at(sk27,sk29),at(sk28,sk30))),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(hi97,negated_conjecture,
once(at_the_same_time(at(sk27,sk29),at(sk28,sk30))) = true,
inference(equality_encoding,[status(esa)],[c113]) ).
cnf(c112,plain,
ordered_by(trajectory_of(sk27),sk26,sk29),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(hi96,negated_conjecture,
ordered_by(trajectory_of(sk27),sk26,sk29) = true,
inference(equality_encoding,[status(esa)],[c112]) ).
cnf(c111,plain,
ordered_by(trajectory_of(sk28),sk30,sk26),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(hi95,negated_conjecture,
ordered_by(trajectory_of(sk28),sk30,sk26) = true,
inference(equality_encoding,[status(esa)],[c111]) ).
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(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi102,h5,hi97,hi96,hi95,hi91]) ).
cnf(t1454,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]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c21,c30,c41,c48,c108]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1454]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO148+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 11:09:00 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.45/1.69 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.45/1.69 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------