%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRA003+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n012.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:22:52 PM UTC 2026
% Result : Theorem 13.24s 12.27s
% Output : Proof 13.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 6
% Syntax : Number of formulae : 51 ( 13 unt; 0 def)
% Number of atoms : 223 ( 53 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 270 ( 98 ~; 86 |; 75 &)
% ( 1 <=>; 8 =>; 0 <=; 2 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-5 aty)
% Number of variables : 131 ( 17 sgn 79 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,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('/export/starexec/sandbox/benchmark/theBenchmark.p',shortest_path_properties) ).
fof(f11_nnf,plain,
! [V1,V2,E1,E2,P] :
( ( ~ precedes(E2,E1,P)
& ! [E3] :
( head_of(E3) != head_of(E2)
| tail_of(E3) != tail_of(E1) ) )
| ~ precedes(E1,E2,P)
| ~ shortest_path(V1,V2,P) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [V1,V2,P,E1,E2,E3] :
( ( ~ precedes(E2,E1,P)
& ( head_of(E3) != head_of(E2)
| tail_of(E3) != tail_of(E1) ) )
| ~ precedes(E1,E2,P)
| ~ shortest_path(V1,V2,P) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c55,plain,
( ~ precedes(X3,X2,X4)
| ~ precedes(X2,X3,X4)
| ~ shortest_path(X0,X1,X4) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
fof(f17,conjecture,
! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ( path(V1,V2,P)
& E1 != E2
& edge(E2)
& edge(E1)
& V1 != V2
& vertex(V2)
& vertex(V1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',vertices_and_edges) ).
fof(f17_neg,negated_conjecture,
~ ! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ( path(V1,V2,P)
& E1 != E2
& edge(E2)
& edge(E1)
& V1 != V2
& vertex(V2)
& vertex(V1) ) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f17_nnf,plain,
? [V1,V2,E1,E2,P] :
( ( ~ path(V1,V2,P)
| E1 = E2
| ~ edge(E2)
| ~ edge(E1)
| V1 = V2
| ~ vertex(V2)
| ~ vertex(V1) )
& precedes(E1,E2,P)
& shortest_path(V1,V2,P) ),
inference(nnf_transformation,[status(thm)],[f17_neg]) ).
fof(f17_sk,plain,
( ( ~ path(sk8,sk9,sk12)
| sk10 = sk11
| ~ edge(sk11)
| ~ edge(sk10)
| sk8 = sk9
| ~ vertex(sk9)
| ~ vertex(sk8) )
& precedes(sk10,sk11,sk12)
& shortest_path(sk8,sk9,sk12) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8,sk9,sk10,sk11,sk12])],[f17_nnf]) ).
cnf(c70,plain,
shortest_path(sk8,sk9,sk12),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p117,plain,
( ~ precedes(X1,X0,sk12)
| ~ precedes(X0,X1,sk12) ),
inference(resolution,[status(thm)],[c55,c70]) ).
cnf(p118,plain,
~ precedes(X0,X0,sk12),
inference(factoring,[status(thm)],[p117]) ).
fof(f9,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('/export/starexec/sandbox/benchmark/theBenchmark.p',precedes_properties) ).
fof(f9_nnf,plain,
! [P,V1,V2] :
( ! [E1,E2] :
( ( ( ( ? [E3] :
( precedes(E3,E2,P)
& sequential(E1,E3) )
& ~ sequential(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) )
| ~ path(V1,V2,P) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [V1,V2,P,E1,E2,E3] :
( ( ( ( precedes(sk4(P,V1,V2,E1,E2),E2,P)
& sequential(E1,sk4(P,V1,V2,E1,E2))
& ~ sequential(E1,E2) )
| ( ( ~ precedes(E3,E2,P)
| ~ sequential(E1,E3) )
& sequential(E1,E2) ) )
& on_path(E2,P)
& on_path(E1,P) )
| ~ precedes(E1,E2,P)
| ~ path(V1,V2,P) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4])],[f9_nnf]) ).
cnf(c42,plain,
( on_path(X4,X0)
| ~ precedes(X3,X4,X0)
| ~ path(X1,X2,X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f10,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('/export/starexec/sandbox/benchmark/theBenchmark.p',shortest_path_defn) ).
fof(f10_nnf,plain,
! [V1,V2,SP] :
( ( ? [P] :
( ~ less_or_equal(length_of(SP),length_of(P))
& path(V1,V2,P) )
| V1 = V2
| ~ path(V1,V2,SP)
| shortest_path(V1,V2,SP) )
& ( ( ! [P] :
( less_or_equal(length_of(SP),length_of(P))
| ~ path(V1,V2,P) )
& V1 != V2
& path(V1,V2,SP) )
| ~ shortest_path(V1,V2,SP) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [V1,V2,SP,P] :
( ( ( ~ less_or_equal(length_of(SP),length_of(sk5(V1,V2,SP)))
& path(V1,V2,sk5(V1,V2,SP)) )
| V1 = V2
| ~ path(V1,V2,SP)
| shortest_path(V1,V2,SP) )
& ( ( ( less_or_equal(length_of(SP),length_of(P))
| ~ path(V1,V2,P) )
& V1 != V2
& path(V1,V2,SP) )
| ~ shortest_path(V1,V2,SP) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f10_nnf]) ).
cnf(c49,plain,
( path(X0,X1,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p76,plain,
path(sk8,sk9,sk12),
inference(resolution,[status(thm)],[c49,c70]) ).
cnf(p102,plain,
( on_path(X1,sk12)
| ~ precedes(X0,X1,sk12) ),
inference(resolution,[status(thm)],[c42,p76]) ).
cnf(c71,plain,
precedes(sk10,sk11,sk12),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p103,plain,
on_path(sk11,sk12),
inference(resolution,[status(thm)],[p102,c71]) ).
fof(f5,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('/export/starexec/sandbox/benchmark/theBenchmark.p',on_path_properties) ).
fof(f5_nnf,plain,
! [V1,V2,P,E] :
( ( in_path(tail_of(E),P)
& in_path(head_of(E),P)
& edge(E) )
| ~ on_path(E,P)
| ~ path(V1,V2,P) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [V1,V2,P,E] :
( ( in_path(tail_of(E),P)
& in_path(head_of(E),P)
& edge(E) )
| ~ on_path(E,P)
| ~ path(V1,V2,P) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c28,plain,
( edge(X3)
| ~ on_path(X3,X2)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p85,plain,
( edge(X0)
| ~ on_path(X0,sk12) ),
inference(resolution,[status(thm)],[c28,p76]) ).
cnf(p104,plain,
edge(sk11),
inference(resolution,[status(thm)],[p103,p85]) ).
cnf(c41,plain,
( on_path(X3,X0)
| ~ precedes(X3,X4,X0)
| ~ path(X1,X2,X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p93,plain,
( on_path(X0,sk12)
| ~ precedes(X0,X1,sk12) ),
inference(resolution,[status(thm)],[c41,p76]) ).
cnf(p94,plain,
on_path(sk10,sk12),
inference(resolution,[status(thm)],[p93,c71]) ).
cnf(p95,plain,
edge(sk10),
inference(resolution,[status(thm)],[p94,p85]) ).
fof(f4,axiom,
! [V1,V2,P] :
( path(V1,V2,P)
=> ( ? [E] :
( ( ( P = path_cons(E,empty)
& V2 = head_of(E) )
<~> ? [TP] :
( P = path_cons(E,TP)
& path(head_of(E),V2,TP) ) )
& V1 = tail_of(E)
& edge(E) )
& vertex(V2)
& vertex(V1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',path_properties) ).
fof(f4_nnf,plain,
! [V1,V2,P] :
( ( ? [E] :
( ( ( ? [TP] :
( P = path_cons(E,TP)
& path(head_of(E),V2,TP) )
& ( P != path_cons(E,empty)
| V2 != head_of(E) ) )
| ( ! [TP] :
( P != path_cons(E,TP)
| ~ path(head_of(E),V2,TP) )
& P = path_cons(E,empty)
& V2 = head_of(E) ) )
& V1 = tail_of(E)
& edge(E) )
& vertex(V2)
& vertex(V1) )
| ~ path(V1,V2,P) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [V1,V2,P,TP] :
( ( ( ( P = path_cons(sk1(V1,V2,P),sk2(V1,V2,P))
& path(head_of(sk1(V1,V2,P)),V2,sk2(V1,V2,P))
& ( P != path_cons(sk1(V1,V2,P),empty)
| V2 != head_of(sk1(V1,V2,P)) ) )
| ( ( P != path_cons(sk1(V1,V2,P),TP)
| ~ path(head_of(sk1(V1,V2,P)),V2,TP) )
& P = path_cons(sk1(V1,V2,P),empty)
& V2 = head_of(sk1(V1,V2,P)) ) )
& V1 = tail_of(sk1(V1,V2,P))
& edge(sk1(V1,V2,P))
& vertex(V2)
& vertex(V1) )
| ~ path(V1,V2,P) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2])],[f4_nnf]) ).
cnf(c15,plain,
( vertex(X0)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p77,plain,
vertex(sk8),
inference(resolution,[status(thm)],[p76,c15]) ).
cnf(c72,plain,
( ~ path(sk8,sk9,sk12)
| sk10 = sk11
| ~ edge(sk11)
| ~ edge(sk10)
| sk8 = sk9
| ~ vertex(sk9)
| ~ vertex(sk8) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p79,plain,
( ~ path(sk8,sk9,sk12)
| sk10 = sk11
| ~ edge(sk11)
| ~ edge(sk10)
| sk8 = sk9
| ~ vertex(sk9) ),
inference(resolution,[status(thm)],[p77,c72]) ).
cnf(c16,plain,
( vertex(X1)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p78,plain,
vertex(sk9),
inference(resolution,[status(thm)],[p76,c16]) ).
cnf(p80,plain,
( ~ path(sk8,sk9,sk12)
| sk10 = sk11
| ~ edge(sk11)
| ~ edge(sk10)
| sk8 = sk9 ),
inference(resolution,[status(thm)],[p79,p78]) ).
cnf(p101,plain,
( ~ path(sk8,sk9,sk12)
| sk10 = sk11
| ~ edge(sk11)
| sk8 = sk9 ),
inference(resolution,[status(thm)],[p95,p80]) ).
cnf(p110,plain,
( ~ path(sk8,sk9,sk12)
| sk10 = sk11
| sk8 = sk9 ),
inference(resolution,[status(thm)],[p104,p101]) ).
cnf(p111,plain,
( sk10 = sk11
| sk8 = sk9 ),
inference(resolution,[status(thm)],[p110,p76]) ).
cnf(p112,plain,
( precedes(sk10,sk10,sk12)
| sk8 = sk9 ),
inference(superposition,[status(thm)],[p111,c71]) ).
cnf(p120,plain,
sk8 = sk9,
inference(resolution,[status(thm)],[p118,p112]) ).
cnf(c50,plain,
( X0 != X1
| ~ shortest_path(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p75,plain,
sk8 != sk9,
inference(resolution,[status(thm)],[c50,c70]) ).
cnf(p122,plain,
$false,
inference(resolution,[status(thm)],[p120,p75]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRA003+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.05/10.52 % Computer : n012.cluster.edu
% 0.05/10.52 % Model : x86_64 x86_64
% 0.05/10.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/10.52 % Memory : 8046.5625MB
% 0.05/10.52 % OS : Linux 6.8.0-71-generic
% 0.05/10.52 % CPULimit : 300
% 0.05/10.52 % WCLimit : 300
% 0.05/10.52 % DateTime : Wed Sep 23 12:42:45 UTC 2026
% 0.05/10.52 % CPUTime :
% 0.05/10.52 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 13.24/12.27 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.24/12.27 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------