%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRA004+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:19:22 AM UTC 2026
% Result : Theorem 0.22s 5.56s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 8
% Syntax : Number of formulae : 75 ( 16 unt; 0 def)
% Number of atoms : 218 ( 98 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 240 ( 97 ~; 96 |; 34 &)
% ( 3 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-1 aty)
% Number of variables : 108 ( 16 sgn 36 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(no_loops,axiom,
! [E] :
( edge(E)
=> head_of(E) != tail_of(E) ),
file('theBenchmark.p',no_loops) ).
fof(on_path_properties,axiom,
! [V1,V2,P,E] :
( ( on_path(E,P)
& path(V1,V2,P) )
=> ( in_path(tail_of(E),P)
& in_path(head_of(E),P)
& edge(E) ) ),
file('theBenchmark.p',on_path_properties) ).
fof(sequential_defn,axiom,
! [E1,E2] :
( sequential(E1,E2)
<=> ( head_of(E1) = tail_of(E2)
& E1 != E2
& edge(E2)
& edge(E1) ) ),
file('theBenchmark.p',sequential_defn) ).
fof(precedes_defn,axiom,
! [P,V1,V2] :
( path(V1,V2,P)
=> ! [E1,E2] :
( ( ( ? [E3] :
( precedes(E3,E2,P)
& sequential(E1,E3) )
| sequential(E1,E2) )
& on_path(E2,P)
& on_path(E1,P) )
=> precedes(E1,E2,P) ) ),
file('theBenchmark.p',precedes_defn) ).
fof(precedes_properties,axiom,
! [P,V1,V2] :
( path(V1,V2,P)
=> ! [E1,E2] :
( precedes(E1,E2,P)
=> ( ~ ( sequential(E1,E2)
<=> ? [E3] :
( precedes(E3,E2,P)
& sequential(E1,E3) ) )
& on_path(E2,P)
& on_path(E1,P) ) ) ),
file('theBenchmark.p',precedes_properties) ).
fof(shortest_path_defn,axiom,
! [V1,V2,SP] :
( shortest_path(V1,V2,SP)
<=> ( ! [P] :
( path(V1,V2,P)
=> less_or_equal(length_of(SP),length_of(P)) )
& V1 != V2
& path(V1,V2,SP) ) ),
file('theBenchmark.p',shortest_path_defn) ).
fof(shortest_path_properties,axiom,
! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ( ~ precedes(E2,E1,P)
& ~ ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1) ) ) ),
file('theBenchmark.p',shortest_path_properties) ).
fof(shortest_path_properties_lemma,conjecture,
! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ( head_of(E2) != head_of(E1)
& head_of(E2) != tail_of(E1)
& ~ ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1) ) ) ),
file('theBenchmark.p',shortest_path_properties_lemma) ).
fof(shortest_path_properties_lemma_neg,negated_conjecture,
~ ! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ( head_of(E2) != head_of(E1)
& head_of(E2) != tail_of(E1)
& ~ ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1) ) ) ),
inference(assume_negation,[status(cth)],[shortest_path_properties_lemma]) ).
cnf(c_24,plain,
( ~ precedes(E,D,C)
| ~ precedes(D,E,C)
| ~ shortest_path(A,B,C) ),
inference(clausify,[status(thm)],[shortest_path_properties]) ).
fof(nnf_18,plain,
? [V1,V2,E1,E2,P] :
( ( head_of(E2) = head_of(E1)
| tail_of(E1) = head_of(E2)
| ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1) ) )
& precedes(E1,E2,P)
& shortest_path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[shortest_path_properties_lemma_neg]) ).
fof(sk_shortest_path_properties_lemma_neg_sk,plain,
( ( head_of(sK4) = head_of(sK3)
| tail_of(sK3) = head_of(sK4)
| ( head_of(sK5) = head_of(sK4)
& tail_of(sK5) = tail_of(sK3) ) )
& precedes(sK3,sK4,sK2)
& shortest_path(sK0,sK1,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5]),skolemize(V1,sK0),skolemize(V2,sK1),skolemize(E1,sK3),skolemize(E2,sK4),skolemize(P,sK2),skolemize(E3,sK5)],[nnf_18]) ).
fof(sk_shortest_path_properties_lemma_neg,plain,
( ( head_of(sK4) = head_of(sK3)
| tail_of(sK3) = head_of(sK4)
| head_of(sK5) = head_of(sK4) )
& ( head_of(sK4) = head_of(sK3)
| tail_of(sK3) = head_of(sK4)
| tail_of(sK5) = tail_of(sK3) )
& precedes(sK3,sK4,sK2)
& shortest_path(sK0,sK1,sK2) ),
inference(cnf_transformation,[status(thm)],[sk_shortest_path_properties_lemma_neg_sk]) ).
cnf(c_25,negated_conjecture,
shortest_path(sK0,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_shortest_path_properties_lemma_neg]) ).
cnf(c_26,plain,
( head_of(F) != head_of(E)
| tail_of(F) != tail_of(D)
| ~ precedes(D,E,C)
| ~ shortest_path(A,B,C) ),
inference(clausify,[status(thm)],[shortest_path_properties]) ).
cnf(c_31,plain,
( path(A,B,C)
| ~ shortest_path(A,B,C) ),
inference(clausify,[status(thm)],[shortest_path_defn]) ).
cnf(c_32,negated_conjecture,
path(sK0,sK1,sK2),
inference(resolve,[status(thm)],[c_31,c_25]) ).
cnf(c_41,negated_conjecture,
( head_of(C) != head_of(B)
| tail_of(C) != tail_of(A)
| ~ precedes(A,B,sK2) ),
inference(resolve,[status(thm)],[c_26,c_25]) ).
cnf(c_42,negated_conjecture,
( ~ precedes(B,A,sK2)
| ~ precedes(A,B,sK2) ),
inference(resolve,[status(thm)],[c_24,c_25]) ).
cnf(c_43,plain,
( tail_of(A) != head_of(A)
| ~ edge(A) ),
inference(clausify,[status(thm)],[no_loops]) ).
cnf(c_63,plain,
( edge(D)
| ~ on_path(D,C)
| ~ path(A,B,C) ),
inference(clausify,[status(thm)],[on_path_properties]) ).
cnf(c_68,plain,
( tail_of(B) != head_of(A)
| B = A
| ~ edge(B)
| ~ edge(A)
| sequential(A,B) ),
inference(clausify,[status(thm)],[sequential_defn]) ).
cnf(c_70,plain,
( ~ precedes(F,E,C)
| ~ sequential(D,F)
| ~ on_path(E,C)
| ~ on_path(D,C)
| precedes(D,E,C)
| ~ path(A,B,C) ),
inference(clausify,[status(thm)],[precedes_defn]) ).
cnf(c_71,plain,
( on_path(D,C)
| ~ precedes(D,E,C)
| ~ path(A,B,C) ),
inference(clausify,[status(thm)],[precedes_properties]) ).
cnf(c_72,plain,
( on_path(E,C)
| ~ precedes(D,E,C)
| ~ path(A,B,C) ),
inference(clausify,[status(thm)],[precedes_properties]) ).
cnf(c_90,negated_conjecture,
precedes(sK3,sK4,sK2),
inference(split_conjunct,[status(thm)],[sk_shortest_path_properties_lemma_neg]) ).
cnf(c_91,negated_conjecture,
( head_of(sK4) = head_of(sK3)
| tail_of(sK3) = head_of(sK4)
| tail_of(sK5) = tail_of(sK3) ),
inference(split_conjunct,[status(thm)],[sk_shortest_path_properties_lemma_neg]) ).
cnf(c_92,negated_conjecture,
( head_of(sK4) = head_of(sK3)
| tail_of(sK3) = head_of(sK4)
| head_of(sK5) = head_of(sK4) ),
inference(split_conjunct,[status(thm)],[sk_shortest_path_properties_lemma_neg]) ).
cnf(c_103,plain,
~ precedes(A,A,sK2),
inference(factor,[status(thm)],[c_42]) ).
cnf(c_149,plain,
( edge(A)
| ~ on_path(A,sK2) ),
inference(resolve,[status(thm)],[c_63,c_32]) ).
cnf(c_152,plain,
( ~ precedes(C,B,sK2)
| ~ sequential(A,C)
| ~ on_path(B,sK2)
| ~ on_path(A,sK2)
| precedes(A,B,sK2) ),
inference(resolve,[status(thm)],[c_70,c_32]) ).
cnf(c_480,plain,
( ~ precedes(B,A,sK2)
| ~ sequential(A,B)
| ~ on_path(A,sK2)
| precedes(A,A,sK2) ),
inference(factor,[status(thm)],[c_152]) ).
cnf(c_153,plain,
( ~ precedes(B,A,sK2)
| ~ sequential(A,B)
| ~ on_path(A,sK2) ),
inference(resolve,[status(thm)],[c_103,c_480]) ).
cnf(c_154,plain,
( on_path(A,sK2)
| ~ precedes(A,B,sK2) ),
inference(resolve,[status(thm)],[c_71,c_32]) ).
cnf(c_155,plain,
( on_path(B,sK2)
| ~ precedes(A,B,sK2) ),
inference(resolve,[status(thm)],[c_72,c_32]) ).
cnf(c_481,negated_conjecture,
( head_of(A) != head_of(sK4)
| tail_of(A) != tail_of(sK3) ),
inference(resolve,[status(thm)],[c_90,c_41]) ).
cnf(c_482,negated_conjecture,
( head_of(A) != head_of(sK4)
| tail_of(sK3) != tail_of(A) ),
inference(copy,[status(thm)],[c_481]) ).
cnf(c_173,negated_conjecture,
( head_of(sK4) != head_of(A)
| tail_of(sK3) != tail_of(A) ),
inference(copy,[status(thm)],[c_482]) ).
cnf(c_483,negated_conjecture,
( head_of(A) != head_of(sK4)
| tail_of(A) != tail_of(sK3) ),
inference(resolve,[status(thm)],[c_41,c_90]) ).
cnf(c_484,plain,
head_of(sK3) != head_of(sK4),
inference(xxres,[status(thm)],[c_483]) ).
cnf(c_175,plain,
head_of(sK4) != head_of(sK3),
inference(copy,[status(thm)],[c_484]) ).
cnf(c_177,negated_conjecture,
( tail_of(sK3) = head_of(sK4)
| head_of(sK5) = head_of(sK4) ),
inference(resolve,[status(thm)],[c_175,c_92]) ).
cnf(c_178,negated_conjecture,
( tail_of(sK3) = head_of(sK4)
| tail_of(sK5) = tail_of(sK3) ),
inference(resolve,[status(thm)],[c_175,c_91]) ).
cnf(c_224,plain,
on_path(sK3,sK2),
inference(resolve,[status(thm)],[c_154,c_90]) ).
cnf(c_225,plain,
edge(sK3),
inference(resolve,[status(thm)],[c_224,c_149]) ).
cnf(c_248,plain,
tail_of(sK3) != head_of(sK3),
inference(resolve,[status(thm)],[c_225,c_43]) ).
cnf(c_250,plain,
( ~ sequential(sK4,sK3)
| ~ on_path(sK4,sK2) ),
inference(resolve,[status(thm)],[c_153,c_90]) ).
cnf(c_251,plain,
on_path(sK4,sK2),
inference(resolve,[status(thm)],[c_155,c_90]) ).
cnf(c_252,plain,
~ sequential(sK4,sK3),
inference(resolve,[status(thm)],[c_251,c_250]) ).
cnf(c_255,plain,
edge(sK4),
inference(resolve,[status(thm)],[c_251,c_149]) ).
cnf(c_485,negated_conjecture,
( sK3 = sK4
| ~ edge(sK3)
| ~ edge(sK4)
| sequential(sK4,sK3)
| head_of(sK5) = head_of(sK4) ),
inference(resolve,[status(thm)],[c_177,c_68]) ).
cnf(c_486,negated_conjecture,
( sK4 = sK3
| ~ edge(sK3)
| ~ edge(sK4)
| sequential(sK4,sK3)
| head_of(sK5) = head_of(sK4) ),
inference(copy,[status(thm)],[c_485]) ).
cnf(c_487,negated_conjecture,
( sK4 = sK3
| ~ edge(sK3)
| ~ edge(sK4)
| head_of(sK5) = head_of(sK4) ),
inference(resolve,[status(thm)],[c_252,c_486]) ).
cnf(c_488,negated_conjecture,
( sK4 = sK3
| ~ edge(sK3)
| head_of(sK5) = head_of(sK4) ),
inference(resolve,[status(thm)],[c_255,c_487]) ).
cnf(c_373,negated_conjecture,
( sK4 = sK3
| head_of(sK5) = head_of(sK4) ),
inference(resolve,[status(thm)],[c_225,c_488]) ).
cnf(c_489,plain,
( head_of(A) != head_of(sK4)
| tail_of(sK3) != tail_of(A) ),
inference(copy,[status(thm)],[c_173]) ).
cnf(c_490,plain,
( tail_of(sK3) != tail_of(sK5)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_373,c_489]) ).
cnf(c_388,plain,
( tail_of(sK5) != tail_of(sK3)
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_490]) ).
cnf(c_406,plain,
( sK4 = sK3
| tail_of(sK3) = head_of(sK4) ),
inference(resolve,[status(thm)],[c_178,c_388]) ).
cnf(c_491,plain,
( head_of(sK4) != head_of(A)
| tail_of(A) != tail_of(sK3) ),
inference(copy,[status(thm)],[c_173]) ).
cnf(c_492,negated_conjecture,
( head_of(sK4) != head_of(sK5)
| tail_of(sK3) = head_of(sK4) ),
inference(resolve,[status(thm)],[c_178,c_491]) ).
cnf(c_418,negated_conjecture,
( head_of(sK5) != head_of(sK4)
| tail_of(sK3) = head_of(sK4) ),
inference(copy,[status(thm)],[c_492]) ).
cnf(c_493,plain,
( sK3 = sK4
| ~ edge(sK3)
| ~ edge(sK4)
| sequential(sK4,sK3)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_406,c_68]) ).
cnf(c_494,plain,
( sK4 = sK3
| ~ edge(sK3)
| ~ edge(sK4)
| sequential(sK4,sK3)
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_493]) ).
cnf(c_495,plain,
( ~ edge(sK3)
| ~ edge(sK4)
| sequential(sK4,sK3)
| sK4 = sK3 ),
inference(copy,[status(thm)],[c_494]) ).
cnf(c_496,plain,
( ~ edge(sK3)
| ~ edge(sK4)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_252,c_495]) ).
cnf(c_497,plain,
( ~ edge(sK3)
| sK4 = sK3 ),
inference(resolve,[status(thm)],[c_255,c_496]) ).
cnf(c_439,plain,
sK4 = sK3,
inference(resolve,[status(thm)],[c_225,c_497]) ).
cnf(c_498,negated_conjecture,
( head_of(sK5) != head_of(sK4)
| tail_of(sK3) = head_of(sK3) ),
inference(paramod,[status(thm)],[c_439,c_418]) ).
cnf(c_499,negated_conjecture,
( head_of(sK5) != head_of(sK3)
| tail_of(sK3) = head_of(sK3) ),
inference(paramod,[status(thm)],[c_439,c_498]) ).
cnf(c_459,negated_conjecture,
head_of(sK5) != head_of(sK3),
inference(resolve,[status(thm)],[c_248,c_499]) ).
cnf(c_500,negated_conjecture,
( tail_of(sK3) = head_of(sK4)
| head_of(sK5) = head_of(sK3) ),
inference(paramod,[status(thm)],[c_439,c_177]) ).
cnf(c_501,negated_conjecture,
( tail_of(sK3) = head_of(sK3)
| head_of(sK5) = head_of(sK3) ),
inference(paramod,[status(thm)],[c_439,c_500]) ).
cnf(c_502,negated_conjecture,
tail_of(sK3) = head_of(sK3),
inference(resolve,[status(thm)],[c_459,c_501]) ).
cnf(c_479,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_248,c_502]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRA004+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.46 % Computer : n017.cluster.edu
% 0.17/5.46 % Model : x86_64 x86_64
% 0.17/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.46 % Memory : 8046.5625MB
% 0.17/5.46 % OS : Linux 6.8.0-71-generic
% 0.17/5.46 % CPULimit : 300
% 0.17/5.46 % WCLimit : 300
% 0.17/5.46 % DateTime : Fri Sep 25 13:43:39 UTC 2026
% 0.17/5.46 % CPUTime :
% 0.17/5.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/5.46 % Process 2416124 was started by sandbox2 on n017,
% 0.17/5.46 % Fri Sep 25 13:43:39 2026
% 0.17/5.46 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/5.48
% 0.17/5.48 % From the command line: assign(max_seconds, 300).
% 0.22/5.56
% 0.22/5.56 % SZS status Theorem for theBenchmark
% 0.22/5.56
% 0.22/5.56 % Proof 1 at 0.05 (+ 0.01) seconds.
% 0.22/5.56 % Length of proof is 48.
% 0.22/5.56 % Level of proof is 12.
% 0.22/5.56 % Maximum clause weight is 26.000.
% 0.22/5.56 % Given clauses 142.
% 0.22/5.56
% 0.22/5.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------