%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRA005+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 : n019.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 8.80s 7.32s
% Output : Proof 8.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 2
% Syntax : Number of formulae : 15 ( 5 unt; 0 def)
% Number of atoms : 49 ( 22 equ)
% Maximal formula atoms : 5 ( 3 avg)
% Number of connectives : 59 ( 25 ~; 12 |; 19 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 46 ( 2 sgn 27 !; 9 ?)
% 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(c54,plain,
( head_of(X5) != head_of(X3)
| tail_of(X5) != tail_of(X2)
| ~ 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) )
=> ~ ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1)
& edge(E3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_short_cut_edge) ).
fof(f17_neg,negated_conjecture,
~ ! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ~ ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1)
& edge(E3) ) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f17_nnf,plain,
? [V1,V2,E1,E2,P] :
( ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1)
& edge(E3) )
& precedes(E1,E2,P)
& shortest_path(V1,V2,P) ),
inference(nnf_transformation,[status(thm)],[f17_neg]) ).
fof(f17_sk,plain,
( head_of(sk13) = head_of(sk11)
& tail_of(sk13) = tail_of(sk10)
& edge(sk13)
& precedes(sk10,sk11,sk12)
& shortest_path(sk8,sk9,sk12) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8,sk9,sk10,sk11,sk12,sk13])],[f17_nnf]) ).
cnf(c70,plain,
shortest_path(sk8,sk9,sk12),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p330,plain,
( head_of(X2) != head_of(X1)
| tail_of(X2) != tail_of(X0)
| ~ precedes(X0,X1,sk12) ),
inference(resolution,[status(thm)],[c54,c70]) ).
cnf(c71,plain,
precedes(sk10,sk11,sk12),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p455,plain,
( head_of(X0) != head_of(sk11)
| tail_of(X0) != tail_of(sk10) ),
inference(resolution,[status(thm)],[p330,c71]) ).
cnf(c73,plain,
tail_of(sk13) = tail_of(sk10),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p456,plain,
head_of(sk11) != head_of(sk11),
inference(resolution,[status(thm)],[p455,c73]) ).
cnf(p458,plain,
$false,
inference(equality_resolution,[status(thm)],[p456]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA005+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/6.01 % Computer : n019.cluster.edu
% 0.09/6.01 % Model : x86_64 x86_64
% 0.09/6.01 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/6.01 % Memory : 8046.5625MB
% 0.09/6.01 % OS : Linux 6.8.0-71-generic
% 0.09/6.01 % CPULimit : 300
% 0.09/6.01 % WCLimit : 300
% 0.09/6.01 % DateTime : Wed Sep 23 12:43:13 UTC 2026
% 0.09/6.01 % CPUTime :
% 0.09/6.01 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.80/7.32 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.80/7.32 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------