%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO147+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 : Sun Sep 27 07:17:11 AM UTC 2026
% Result : Theorem 0.13s 0.47s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 5
% Syntax : Number of formulae : 27 ( 12 unt; 0 def)
% Number of atoms : 47 ( 4 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 37 ( 17 ~; 10 |; 5 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 33 ( 2 sgn 16 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(connect_defn,axiom,
! [X,Y,P] :
( connect(X,Y,P)
<=> once(at_the_same_time(at(X,P),at(Y,P))) ),
file('theBenchmark.p',connect_defn) ).
fof(conjunction_at_the_same_time,axiom,
! [A,B] :
( once(at_the_same_time(A,B))
=> ( once(B)
& once(A) ) ),
file('theBenchmark.p',conjunction_at_the_same_time) ).
fof(at_on_trajectory,axiom,
! [X,P] :
( once(at(X,P))
<=> incident_o(P,trajectory_of(X)) ),
file('theBenchmark.p',at_on_trajectory) ).
fof(trajectories_are_oriented_curves,axiom,
! [X] :
? [O] : trajectory_of(X) = O,
file('theBenchmark.p',trajectories_are_oriented_curves) ).
fof(t13,conjecture,
! [P,X,Y] :
( connect(X,Y,P)
=> ( incident_o(P,trajectory_of(Y))
& incident_o(P,trajectory_of(X)) ) ),
file('theBenchmark.p',t13) ).
fof(t13_neg,negated_conjecture,
~ ! [P,X,Y] :
( connect(X,Y,P)
=> ( incident_o(P,trajectory_of(Y))
& incident_o(P,trajectory_of(X)) ) ),
inference(assume_negation,[status(cth)],[t13]) ).
cnf(c_79,plain,
( once(at_the_same_time(at(A,C),at(B,C)))
| ~ connect(A,B,C) ),
inference(clausify,[status(thm)],[connect_defn]) ).
fof(nnf_37,plain,
? [P,X,Y] :
( ( ~ incident_o(P,trajectory_of(Y))
| ~ incident_o(P,trajectory_of(X)) )
& connect(X,Y,P) ),
inference(fof_nnf,[status(thm)],[t13_neg]) ).
fof(sk_t13_neg,plain,
( ( ~ incident_o(sK2,trajectory_of(sK1))
| ~ incident_o(sK2,trajectory_of(sK0)) )
& connect(sK0,sK1,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(P,sK2),skolemize(X,sK0),skolemize(Y,sK1)],[nnf_37]) ).
cnf(c_80,negated_conjecture,
connect(sK0,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t13_neg]) ).
cnf(c_81,negated_conjecture,
once(at_the_same_time(at(sK0,sK2),at(sK1,sK2))),
inference(resolve,[status(thm)],[c_80,c_79]) ).
cnf(c_113,negated_conjecture,
( ~ incident_o(sK2,trajectory_of(sK1))
| ~ incident_o(sK2,trajectory_of(sK0)) ),
inference(split_conjunct,[status(thm)],[sk_t13_neg]) ).
fof(nnf_34,plain,
! [X] :
? [O] : trajectory_of(X) = O,
inference(fof_nnf,[status(thm)],[trajectories_are_oriented_curves]) ).
fof(sk_trajectories_are_oriented_curves,plain,
! [X] : trajectory_of(X) = sK3(X),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(O,sK3(X))],[nnf_34]) ).
cnf(c_116,plain,
trajectory_of(A) = sK3(A),
inference(split_conjunct,[status(thm)],[sk_trajectories_are_oriented_curves]) ).
cnf(c_119,plain,
( incident_o(B,trajectory_of(A))
| ~ once(at(A,B)) ),
inference(clausify,[status(thm)],[at_on_trajectory]) ).
cnf(c_120,plain,
( incident_o(B,sK3(A))
| ~ once(at(A,B)) ),
inference(paramod,[status(thm)],[c_116,c_119]) ).
cnf(c_121,plain,
( once(B)
| ~ once(at_the_same_time(A,B)) ),
inference(clausify,[status(thm)],[conjunction_at_the_same_time]) ).
cnf(c_122,plain,
( once(A)
| ~ once(at_the_same_time(A,B)) ),
inference(clausify,[status(thm)],[conjunction_at_the_same_time]) ).
cnf(c_675,negated_conjecture,
( ~ incident_o(sK2,trajectory_of(sK1))
| ~ incident_o(sK2,sK3(sK0)) ),
inference(paramod,[status(thm)],[c_116,c_113]) ).
cnf(c_210,negated_conjecture,
( ~ incident_o(sK2,sK3(sK1))
| ~ incident_o(sK2,sK3(sK0)) ),
inference(paramod,[status(thm)],[c_116,c_675]) ).
cnf(c_252,plain,
once(at(sK1,sK2)),
inference(resolve,[status(thm)],[c_121,c_81]) ).
cnf(c_253,plain,
once(at(sK0,sK2)),
inference(resolve,[status(thm)],[c_122,c_81]) ).
cnf(c_670,plain,
incident_o(sK2,sK3(sK1)),
inference(resolve,[status(thm)],[c_252,c_120]) ).
cnf(c_672,negated_conjecture,
~ incident_o(sK2,sK3(sK0)),
inference(resolve,[status(thm)],[c_670,c_210]) ).
cnf(c_676,plain,
incident_o(sK2,sK3(sK0)),
inference(resolve,[status(thm)],[c_253,c_120]) ).
cnf(c_674,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_672,c_676]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO147+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n020.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 : Fri Sep 25 12:57:06 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 2968998 was started by sandbox2 on n020,
% 0.09/0.35 % Fri Sep 25 12:57:06 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.36
% 0.13/0.36 % From the command line: assign(max_seconds, 300).
% 0.13/0.47
% 0.13/0.47 % SZS status Theorem for theBenchmark
% 0.13/0.47
% 0.13/0.47 % Proof 1 at 0.08 (+ 0.02) seconds.
% 0.13/0.47 % Length of proof is 20.
% 0.13/0.47 % Level of proof is 6.
% 0.13/0.47 % Maximum clause weight is 8.000.
% 0.13/0.47 % Given clauses 155.
% 0.13/0.47
% 0.13/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------