%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRA004+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 : Thu Sep 24 12:30:38 PM UTC 2026
% Result : Theorem 0.13s 0.41s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 7
% Syntax : Number of formulae : 69 ( 14 unt; 0 def)
% Number of atoms : 285 ( 81 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 346 ( 130 ~; 123 |; 79 &)
% ( 3 <=>; 8 =>; 1 <=; 2 <~>)
% Maximal formula depth : 15 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 191 ( 169 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,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') ).
fof(f8,axiom,
! [E1,E2] :
( sequential(E1,E2)
<=> ( head_of(E1) = tail_of(E2)
& E1 != E2
& edge(E2)
& edge(E1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [P,V1,V2] :
( path(V1,V2,P)
=> ! [E1,E2] :
( precedes(E1,E2,P)
<= ( ( ? [E3] :
( precedes(E3,E2,P)
& sequential(E1,E3) )
| sequential(E1,E2) )
& on_path(E2,P)
& on_path(E1,P) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,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') ).
fof(f11,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') ).
fof(f12,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') ).
fof(f18,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,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(negated_conjecture,[status(cth)],[f18]) ).
fof(f49,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(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f50,plain,
! [P,E] :
( ( in_path(tail_of(E),P)
& in_path(head_of(E),P)
& edge(E) )
| ~ on_path(E,P)
| ! [V1,V2] : ~ path(V1,V2,P) ),
inference(miniscoping,[status(thm)],[f49]) ).
fof(f51,plain,
! [X0,X1,X2,X3] :
( edge(X3)
| ~ on_path(X3,X2)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f60,plain,
! [E1,E2] :
( ( head_of(E1) != tail_of(E2)
| E1 = E2
| ~ edge(E2)
| ~ edge(E1)
| sequential(E1,E2) )
& ( ( head_of(E1) = tail_of(E2)
& E1 != E2
& edge(E2)
& edge(E1) )
| ~ sequential(E1,E2) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f61,plain,
( ! [E1,E2] :
( head_of(E1) != tail_of(E2)
| E1 = E2
| ~ edge(E2)
| ~ edge(E1)
| sequential(E1,E2) )
& ! [E1,E2] :
( ( head_of(E1) = tail_of(E2)
& E1 != E2
& edge(E2)
& edge(E1) )
| ~ sequential(E1,E2) ) ),
inference(miniscoping,[status(thm)],[f60]) ).
fof(f66,plain,
! [X0,X1] :
( head_of(X0) != tail_of(X1)
| X0 = X1
| ~ edge(X1)
| ~ edge(X0)
| sequential(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f67,plain,
! [P,V1,V2] :
( ! [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(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f68,plain,
! [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) )
| ! [V1,V2] : ~ path(V1,V2,P) ),
inference(miniscoping,[status(thm)],[f67]) ).
fof(f69,plain,
! [X0,X1,X2,X3,X4] :
( ~ sequential(X3,X4)
| ~ on_path(X4,X2)
| ~ on_path(X3,X2)
| precedes(X3,X4,X2)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f71,plain,
! [P,V1,V2] :
( ! [E1,E2] :
( ( ( sequential(E1,E2)
<~> ? [E3] :
( precedes(E3,E2,P)
& sequential(E1,E3) ) )
& on_path(E2,P)
& on_path(E1,P) )
| ~ precedes(E1,E2,P) )
| ~ path(V1,V2,P) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f72,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)],[f71]) ).
fof(f73,plain,
! [P] :
( ! [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) )
| ! [V1,V2] : ~ path(V1,V2,P) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f74,plain,
! [P] :
( ! [E1,E2] :
( ( ( ! [E3] :
( ~ precedes(E3,E2,P)
| ~ sequential(E1,E3) )
| ~ sequential(E1,E2) )
& ( ( precedes(sK4_skl(E2,E1,P),E2,P)
& sequential(E1,sK4_skl(E2,E1,P)) )
| sequential(E1,E2) )
& on_path(E2,P)
& on_path(E1,P) )
| ~ precedes(E1,E2,P) )
| ! [V1,V2] : ~ path(V1,V2,P) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(E3,sK4_skl(E2,E1,P))],[f73]) ).
fof(f75,plain,
! [X0,X1,X2,X3,X4] :
( on_path(X3,X2)
| ~ precedes(X3,X4,X2)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
! [X0,X1,X2,X3,X4] :
( on_path(X4,X2)
| ~ precedes(X3,X4,X2)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f80,plain,
! [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) ) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f81,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)],[f80]) ).
fof(f82,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) )
& ! [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(miniscoping,[status(thm)],[f81]) ).
fof(f83,plain,
( ! [V1,V2,SP] :
( ( ~ less_or_equal(length_of(SP),length_of(sK5_skl(SP,V2,V1)))
& path(V1,V2,sK5_skl(SP,V2,V1)) )
| V1 = V2
| ~ path(V1,V2,SP)
| shortest_path(V1,V2,SP) )
& ! [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(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(P,sK5_skl(SP,V2,V1))],[f82]) ).
fof(f84,plain,
! [X0,X1,X2] :
( path(X0,X1,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f89,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(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f90,plain,
! [E1,E2,P] :
( ( ~ precedes(E2,E1,P)
& ! [E3] :
( head_of(E3) != head_of(E2)
| tail_of(E3) != tail_of(E1) ) )
| ~ precedes(E1,E2,P)
| ! [V1,V2] : ~ shortest_path(V1,V2,P) ),
inference(miniscoping,[status(thm)],[f89]) ).
fof(f91,plain,
! [X0,X1,X2,X3,X4,X5] :
( head_of(X5) != head_of(X4)
| tail_of(X5) != tail_of(X3)
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
! [X0,X1,X2,X3,X4] :
( ~ precedes(X4,X3,X2)
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f116,plain,
? [V1,V2,E1,E2,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) ) )
& precedes(E1,E2,P)
& shortest_path(V1,V2,P) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f117,plain,
? [E1,E2] :
( ( 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) ) )
& ? [P] :
( precedes(E1,E2,P)
& ? [V1,V2] : shortest_path(V1,V2,P) ) ),
inference(miniscoping,[status(thm)],[f116]) ).
fof(f118,plain,
( ( head_of(sK9_skl) = head_of(sK8_skl)
| head_of(sK9_skl) = tail_of(sK8_skl)
| ( head_of(sK13_skl) = head_of(sK9_skl)
& tail_of(sK13_skl) = tail_of(sK8_skl) ) )
& precedes(sK8_skl,sK9_skl,sK10_skl)
& shortest_path(sK11_skl,sK12_skl,sK10_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(E1,sK8_skl),skolemize(E2,sK9_skl),skolemize(P,sK10_skl),skolemize(V1,sK11_skl),skolemize(V2,sK12_skl),skolemize(E3,sK13_skl)],[f117]) ).
fof(f119,plain,
shortest_path(sK11_skl,sK12_skl,sK10_skl),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
precedes(sK8_skl,sK9_skl,sK10_skl),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f121,plain,
( head_of(sK9_skl) = head_of(sK8_skl)
| head_of(sK9_skl) = tail_of(sK8_skl)
| tail_of(sK13_skl) = tail_of(sK8_skl) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f122,plain,
( head_of(sK9_skl) = head_of(sK8_skl)
| head_of(sK9_skl) = tail_of(sK8_skl)
| head_of(sK13_skl) = head_of(sK9_skl) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f137,plain,
path(sK11_skl,sK12_skl,sK10_skl),
inference(resolution,[status(thm)],[f84,f119]) ).
fof(f139,plain,
! [X0,X1] :
( ~ precedes(X1,X0,sK10_skl)
| ~ precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f92,f119]) ).
fof(f140,plain,
~ precedes(sK9_skl,sK8_skl,sK10_skl),
inference(resolution,[status(thm)],[f139,f120]) ).
fof(f143,plain,
! [X0,X1,X2] :
( head_of(X2) != head_of(X1)
| tail_of(X2) != tail_of(X0)
| ~ precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f91,f119]) ).
fof(f144,plain,
! [X0] :
( head_of(X0) != head_of(sK9_skl)
| tail_of(X0) != tail_of(sK8_skl) ),
inference(resolution,[status(thm)],[f143,f120]) ).
fof(f145,plain,
( head_of(sK9_skl) = tail_of(sK8_skl)
| head_of(sK13_skl) = head_of(sK9_skl)
| tail_of(sK8_skl) != tail_of(sK8_skl) ),
inference(resolution,[status(thm)],[f144,f122]) ).
fof(f146,plain,
( head_of(sK9_skl) = tail_of(sK8_skl)
| tail_of(sK13_skl) = tail_of(sK8_skl)
| tail_of(sK8_skl) != tail_of(sK8_skl) ),
inference(resolution,[status(thm)],[f144,f121]) ).
fof(f149,plain,
tail_of(sK9_skl) != tail_of(sK8_skl),
inference(equality_resolution,[status(thm)],[f144]) ).
fof(f150,plain,
( head_of(sK9_skl) = tail_of(sK8_skl)
| head_of(sK13_skl) = head_of(sK9_skl) ),
inference(trivial_equality_resolution,[status(thm)],[f145]) ).
fof(f151,plain,
( head_of(sK9_skl) = tail_of(sK8_skl)
| tail_of(sK13_skl) = tail_of(sK8_skl) ),
inference(trivial_equality_resolution,[status(thm)],[f146]) ).
fof(f154,plain,
( tail_of(sK13_skl) != tail_of(sK8_skl)
| head_of(sK9_skl) = tail_of(sK8_skl) ),
inference(resolution,[status(thm)],[f150,f144]) ).
fof(f177,plain,
head_of(sK9_skl) = tail_of(sK8_skl),
inference(forward_subsumption_resolution,[status(thm)],[f154,f151]) ).
fof(f193,plain,
! [X0] :
( edge(X0)
| ~ on_path(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f51,f137]) ).
fof(f291,plain,
! [X0,X1] :
( on_path(X0,sK10_skl)
| ~ precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f75,f137]) ).
fof(f292,plain,
on_path(sK8_skl,sK10_skl),
inference(resolution,[status(thm)],[f291,f120]) ).
fof(f293,plain,
edge(sK8_skl),
inference(resolution,[status(thm)],[f292,f193]) ).
fof(f328,plain,
! [X0,X1] :
( on_path(X1,sK10_skl)
| ~ precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f76,f137]) ).
fof(f329,plain,
on_path(sK9_skl,sK10_skl),
inference(resolution,[status(thm)],[f328,f120]) ).
fof(f330,plain,
edge(sK9_skl),
inference(resolution,[status(thm)],[f329,f193]) ).
fof(f547,plain,
! [X0] :
( head_of(sK9_skl) != tail_of(X0)
| sK9_skl = X0
| ~ edge(X0)
| sequential(sK9_skl,X0) ),
inference(resolution,[status(thm)],[f66,f330]) ).
fof(f550,plain,
! [X0] :
( tail_of(sK8_skl) != tail_of(X0)
| sK9_skl = X0
| ~ edge(X0)
| sequential(sK9_skl,X0) ),
inference(forward_demodulation,[status(thm)],[f177,f547]) ).
fof(f555,plain,
! [X0,X1] :
( ~ sequential(X0,X1)
| ~ on_path(X1,sK10_skl)
| ~ on_path(X0,sK10_skl)
| precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f69,f137]) ).
fof(f590,plain,
! [X0] :
( ~ sequential(sK9_skl,X0)
| ~ on_path(X0,sK10_skl)
| precedes(sK9_skl,X0,sK10_skl) ),
inference(resolution,[status(thm)],[f555,f329]) ).
fof(f598,plain,
( ~ sequential(sK9_skl,sK8_skl)
| precedes(sK9_skl,sK8_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f590,f292]) ).
fof(f599,plain,
~ sequential(sK9_skl,sK8_skl),
inference(forward_subsumption_resolution,[status(thm)],[f598,f140]) ).
fof(f688,plain,
( tail_of(sK8_skl) != tail_of(sK8_skl)
| sK9_skl = sK8_skl
| sequential(sK9_skl,sK8_skl) ),
inference(resolution,[status(thm)],[f550,f293]) ).
fof(f690,plain,
( sK9_skl = sK8_skl
| sequential(sK9_skl,sK8_skl) ),
inference(trivial_equality_resolution,[status(thm)],[f688]) ).
fof(f691,plain,
sK9_skl = sK8_skl,
inference(forward_subsumption_resolution,[status(thm)],[f690,f599]) ).
fof(f735,plain,
tail_of(sK9_skl) != tail_of(sK9_skl),
inference(backward_demodulation,[status(thm)],[f691,f149]) ).
fof(f746,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f735]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA004+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 18:23:12 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.41 % Refutation found
% 0.13/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.43 % Elapsed time: 0.075641 seconds
% 0.13/0.43 % CPU time: 0.352743 seconds
% 0.13/0.43 % Total memory used: 88.979 MB
% 0.13/0.43 % Net memory used: 88.323 MB
%------------------------------------------------------------------------------