%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRA008+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:39 PM UTC 2026
% Result : Theorem 0.08s 0.42s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 23
% Syntax : Number of formulae : 134 ( 14 unt; 17 def)
% Number of atoms : 467 ( 96 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 569 ( 236 ~; 235 |; 69 &)
% ( 21 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 19 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-3 aty)
% Number of variables : 202 ( 185 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [E] :
( edge(E)
=> head_of(E) != tail_of(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(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(f13,axiom,
! [E1,E2,E3] :
( triangle(E1,E2,E3)
<=> ( sequential(E3,E1)
& sequential(E2,E3)
& sequential(E1,E2)
& edge(E3)
& edge(E2)
& edge(E1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,lemma,
( complete
=> ! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ? [E3] :
( head_of(E3) = tail_of(E1)
& tail_of(E3) = head_of(E2)
& edge(E3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,conjecture,
( complete
=> ! [V1,V2,E1,E2,P] :
( ( sequential(E1,E2)
& precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ? [E3] : triangle(E1,E2,E3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
~ ( complete
=> ! [V1,V2,E1,E2,P] :
( ( sequential(E1,E2)
& precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ? [E3] : triangle(E1,E2,E3) ) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
! [E] :
( head_of(E) != tail_of(E)
| ~ edge(E) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f22,plain,
! [X0] :
( head_of(X0) != tail_of(X0)
| ~ edge(X0) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f61,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(f62,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)],[f61]) ).
fof(f63,plain,
! [X0,X1] :
( edge(X0)
| ~ sequential(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
! [X0,X1] :
( edge(X1)
| ~ sequential(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f65,plain,
! [X0,X1] :
( X0 != X1
| ~ sequential(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f66,plain,
! [X0,X1] :
( head_of(X0) = tail_of(X1)
| ~ sequential(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f67,plain,
! [X0,X1] :
( head_of(X0) != tail_of(X1)
| X0 = X1
| ~ edge(X1)
| ~ edge(X0)
| sequential(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f81,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(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) )
& ( ( ! [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)],[f81]) ).
fof(f83,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)],[f82]) ).
fof(f84,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))],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( path(X0,X1,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f94,plain,
! [E1,E2,E3] :
( ( ~ sequential(E3,E1)
| ~ sequential(E2,E3)
| ~ sequential(E1,E2)
| ~ edge(E3)
| ~ edge(E2)
| ~ edge(E1)
| triangle(E1,E2,E3) )
& ( ( sequential(E3,E1)
& sequential(E2,E3)
& sequential(E1,E2)
& edge(E3)
& edge(E2)
& edge(E1) )
| ~ triangle(E1,E2,E3) ) ),
inference(NNF_transformation,[status(thm)],[f13]) ).
fof(f95,plain,
( ! [E1,E2,E3] :
( ~ sequential(E3,E1)
| ~ sequential(E2,E3)
| ~ sequential(E1,E2)
| ~ edge(E3)
| ~ edge(E2)
| ~ edge(E1)
| triangle(E1,E2,E3) )
& ! [E1,E2,E3] :
( ( sequential(E3,E1)
& sequential(E2,E3)
& sequential(E1,E2)
& edge(E3)
& edge(E2)
& edge(E1) )
| ~ triangle(E1,E2,E3) ) ),
inference(miniscoping,[status(thm)],[f94]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ~ sequential(X2,X0)
| ~ sequential(X1,X2)
| ~ sequential(X0,X1)
| ~ edge(X2)
| ~ edge(X1)
| ~ edge(X0)
| triangle(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f117,plain,
( ! [V1,V2,E1,E2,P] :
( ? [E3] :
( head_of(E3) = tail_of(E1)
& tail_of(E3) = head_of(E2)
& edge(E3) )
| ~ precedes(E1,E2,P)
| ~ shortest_path(V1,V2,P) )
| ~ complete ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f118,plain,
( ! [E1,E2] :
( ? [E3] :
( head_of(E3) = tail_of(E1)
& tail_of(E3) = head_of(E2)
& edge(E3) )
| ! [P] :
( ~ precedes(E1,E2,P)
| ! [V1,V2] : ~ shortest_path(V1,V2,P) ) )
| ~ complete ),
inference(miniscoping,[status(thm)],[f117]) ).
fof(f119,plain,
( ! [E1,E2] :
( ( head_of(sK8_skl(E2,E1)) = tail_of(E1)
& tail_of(sK8_skl(E2,E1)) = head_of(E2)
& edge(sK8_skl(E2,E1)) )
| ! [P] :
( ~ precedes(E1,E2,P)
| ! [V1,V2] : ~ shortest_path(V1,V2,P) ) )
| ~ complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(E3,sK8_skl(E2,E1))],[f118]) ).
fof(f120,plain,
! [X0,X1,X2,X3,X4] :
( edge(sK8_skl(X4,X3))
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2)
| ~ complete ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [X0,X1,X2,X3,X4] :
( tail_of(sK8_skl(X4,X3)) = head_of(X4)
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2)
| ~ complete ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f122,plain,
! [X0,X1,X2,X3,X4] :
( head_of(sK8_skl(X4,X3)) = tail_of(X3)
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2)
| ~ complete ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f123,plain,
( ? [V1,V2,E1,E2,P] :
( ! [E3] : ~ triangle(E1,E2,E3)
& sequential(E1,E2)
& precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
& complete ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f124,plain,
( ? [E1,E2] :
( ! [E3] : ~ triangle(E1,E2,E3)
& sequential(E1,E2)
& ? [P] :
( precedes(E1,E2,P)
& ? [V1,V2] : shortest_path(V1,V2,P) ) )
& complete ),
inference(miniscoping,[status(thm)],[f123]) ).
fof(f125,plain,
( ! [E3] : ~ triangle(sK9_skl,sK10_skl,E3)
& sequential(sK9_skl,sK10_skl)
& precedes(sK9_skl,sK10_skl,sK11_skl)
& shortest_path(sK12_skl,sK13_skl,sK11_skl)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(E1,sK9_skl),skolemize(E2,sK10_skl),skolemize(P,sK11_skl),skolemize(V1,sK12_skl),skolemize(V2,sK13_skl)],[f124]) ).
fof(f126,plain,
complete,
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
shortest_path(sK12_skl,sK13_skl,sK11_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f128,plain,
precedes(sK9_skl,sK10_skl,sK11_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f129,plain,
sequential(sK9_skl,sK10_skl),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f130,plain,
! [X0] : ~ triangle(sK9_skl,sK10_skl,X0),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f141,definition,
( sQ0_spl
<=> complete ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f143,plain,
( sQ0_spl
| ~ complete ),
inference(component_clause,[status(thm)],[f141]) ).
fof(f160,definition,
! [X0,X1,X2,X3,X4] :
( sQ5_spl
<=> ( edge(sK8_skl(X4,X3))
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f161,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ5_spl
| edge(sK8_skl(X4,X3))
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(component_clause,[status(thm)],[f160]) ).
fof(f163,plain,
( sQ5_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f120,f141,f160]) ).
fof(f164,definition,
! [X0,X1,X2,X3,X4] :
( sQ6_spl
<=> ( tail_of(sK8_skl(X4,X3)) = head_of(X4)
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f165,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ6_spl
| tail_of(sK8_skl(X4,X3)) = head_of(X4)
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(component_clause,[status(thm)],[f164]) ).
fof(f167,plain,
( sQ6_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f121,f141,f164]) ).
fof(f168,definition,
! [X0,X1,X2,X3,X4] :
( sQ7_spl
<=> ( head_of(sK8_skl(X4,X3)) = tail_of(X3)
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f169,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ7_spl
| head_of(sK8_skl(X4,X3)) = tail_of(X3)
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(component_clause,[status(thm)],[f168]) ).
fof(f171,plain,
( sQ7_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f122,f141,f168]) ).
fof(f174,plain,
! [X0] : ~ sequential(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f65]) ).
fof(f178,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f143,f126]) ).
fof(f179,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f178]) ).
fof(f214,plain,
! [X0,X1,X2] :
( ~ sequential(X2,X0)
| ~ sequential(X1,X2)
| ~ sequential(X0,X1)
| ~ edge(X1)
| ~ edge(X0)
| triangle(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f102,f64]) ).
fof(f220,definition,
( sQ14_spl
<=> edge(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f222,plain,
( sQ14_spl
| ~ edge(sK9_skl) ),
inference(component_clause,[status(thm)],[f220]) ).
fof(f227,definition,
( sQ16_spl
<=> edge(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f229,plain,
( sQ16_spl
| ~ edge(sK10_skl) ),
inference(component_clause,[status(thm)],[f227]) ).
fof(f236,plain,
head_of(sK9_skl) = tail_of(sK10_skl),
inference(resolution,[status(thm)],[f66,f129]) ).
fof(f240,plain,
( head_of(sK10_skl) != head_of(sK9_skl)
| ~ edge(sK10_skl) ),
inference(paramodulation,[status(thm)],[f236,f22]) ).
fof(f253,definition,
( sQ20_spl
<=> head_of(sK10_skl) = head_of(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f255,plain,
( sQ20_spl
| head_of(sK10_skl) != head_of(sK9_skl) ),
inference(component_clause,[status(thm)],[f253]) ).
fof(f256,plain,
( ~ sQ20_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f240,f227,f253]) ).
fof(f261,plain,
! [X0] :
( sQ16_spl
| ~ sequential(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f229,f64]) ).
fof(f266,plain,
( sQ16_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f129,f261]) ).
fof(f267,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f266]) ).
fof(f398,plain,
! [X0,X1,X2] :
( ~ sequential(X1,X2)
| ~ sequential(X2,X0)
| ~ edge(X0)
| ~ edge(X2)
| triangle(X2,X0,X1)
| head_of(X0) != tail_of(X1)
| X0 = X1
| ~ edge(X1)
| ~ edge(X0) ),
inference(resolution,[status(thm)],[f67,f214]) ).
fof(f414,plain,
! [X0,X1,X2] :
( ~ sequential(X1,X2)
| ~ sequential(X2,X0)
| ~ edge(X2)
| triangle(X2,X0,X1)
| head_of(X0) != tail_of(X1)
| X0 = X1
| ~ edge(X1)
| ~ edge(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f398]) ).
fof(f415,plain,
! [X0,X1,X2] :
( ~ sequential(X0,X2)
| ~ sequential(X2,X1)
| ~ edge(X2)
| triangle(X2,X1,X0)
| head_of(X1) != tail_of(X0)
| X1 = X0
| ~ edge(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f414,f64]) ).
fof(f420,plain,
! [X0] :
( sQ14_spl
| ~ sequential(sK9_skl,X0) ),
inference(resolution,[status(thm)],[f222,f63]) ).
fof(f439,plain,
( sQ14_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f129,f420]) ).
fof(f441,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f439]) ).
fof(f473,plain,
! [X0,X1,X2] :
( ~ sequential(X0,X2)
| ~ sequential(X2,X1)
| triangle(X2,X1,X0)
| head_of(X1) != tail_of(X0)
| X1 = X0
| ~ edge(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f415,f64]) ).
fof(f474,plain,
! [X0] :
( ~ sequential(X0,sK9_skl)
| triangle(sK9_skl,sK10_skl,X0)
| head_of(sK10_skl) != tail_of(X0)
| sK10_skl = X0
| ~ edge(X0) ),
inference(resolution,[status(thm)],[f473,f129]) ).
fof(f476,plain,
! [X0] :
( ~ sequential(X0,sK9_skl)
| triangle(sK9_skl,sK10_skl,X0)
| head_of(sK10_skl) != tail_of(X0)
| sK10_skl = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f474,f63]) ).
fof(f478,plain,
! [X0,X1] :
( ~ sQ6_spl
| tail_of(sK8_skl(X1,X0)) = head_of(X1)
| ~ precedes(X0,X1,sK11_skl) ),
inference(resolution,[status(thm)],[f165,f127]) ).
fof(f479,plain,
( ~ sQ6_spl
| tail_of(sK8_skl(sK10_skl,sK9_skl)) = head_of(sK10_skl) ),
inference(resolution,[status(thm)],[f478,f128]) ).
fof(f484,plain,
( ~ sQ6_spl
| head_of(sK8_skl(sK10_skl,sK9_skl)) != head_of(sK10_skl)
| ~ edge(sK8_skl(sK10_skl,sK9_skl)) ),
inference(paramodulation,[status(thm)],[f479,f22]) ).
fof(f489,definition,
( sQ46_spl
<=> head_of(sK8_skl(sK10_skl,sK9_skl)) = head_of(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f491,plain,
( sQ46_spl
| head_of(sK8_skl(sK10_skl,sK9_skl)) != head_of(sK10_skl) ),
inference(component_clause,[status(thm)],[f489]) ).
fof(f496,definition,
( sQ48_spl
<=> edge(sK8_skl(sK10_skl,sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f497,plain,
( ~ sQ48_spl
| edge(sK8_skl(sK10_skl,sK9_skl)) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f498,plain,
( sQ48_spl
| ~ edge(sK8_skl(sK10_skl,sK9_skl)) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f507,plain,
( ~ sQ6_spl
| ~ sQ46_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f484,f496,f489,f164]) ).
fof(f509,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| sQ48_spl
| ~ precedes(sK9_skl,sK10_skl,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(resolution,[status(thm)],[f498,f161]) ).
fof(f537,plain,
! [X0,X1] :
( ~ sQ5_spl
| sQ48_spl
| ~ shortest_path(X0,X1,sK11_skl) ),
inference(resolution,[status(thm)],[f509,f128]) ).
fof(f538,plain,
( ~ sQ5_spl
| sQ48_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f127,f537]) ).
fof(f539,plain,
( ~ sQ5_spl
| sQ48_spl ),
inference(contradiction_clause,[status(thm)],[f538]) ).
fof(f565,plain,
! [X0,X1] :
( ~ sQ7_spl
| head_of(sK8_skl(X1,X0)) = tail_of(X0)
| ~ precedes(X0,X1,sK11_skl) ),
inference(resolution,[status(thm)],[f169,f127]) ).
fof(f566,plain,
( ~ sQ7_spl
| head_of(sK8_skl(sK10_skl,sK9_skl)) = tail_of(sK9_skl) ),
inference(resolution,[status(thm)],[f565,f128]) ).
fof(f568,plain,
( sQ46_spl
| ~ sQ7_spl
| tail_of(sK9_skl) != head_of(sK10_skl) ),
inference(backward_demodulation,[status(thm)],[f566,f491]) ).
fof(f599,plain,
! [X0] :
( ~ sequential(X0,sK9_skl)
| head_of(sK10_skl) != tail_of(X0)
| sK10_skl = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f476,f130]) ).
fof(f600,plain,
! [X0] :
( head_of(X0) != tail_of(sK9_skl)
| X0 = sK9_skl
| ~ edge(sK9_skl)
| ~ edge(X0)
| head_of(sK10_skl) != tail_of(X0)
| sK10_skl = X0 ),
inference(resolution,[status(thm)],[f599,f67]) ).
fof(f601,definition,
! [X0] :
( sQ61_spl
<=> ( head_of(X0) != tail_of(sK9_skl)
| X0 = sK9_skl
| ~ edge(X0)
| head_of(sK10_skl) != tail_of(X0)
| sK10_skl = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f602,plain,
! [X0] :
( ~ sQ61_spl
| head_of(X0) != tail_of(sK9_skl)
| X0 = sK9_skl
| ~ edge(X0)
| head_of(sK10_skl) != tail_of(X0)
| sK10_skl = X0 ),
inference(component_clause,[status(thm)],[f601]) ).
fof(f604,plain,
( ~ sQ14_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f600,f601,f220]) ).
fof(f608,plain,
( ~ sQ48_spl
| ~ sQ61_spl
| head_of(sK8_skl(sK10_skl,sK9_skl)) != tail_of(sK9_skl)
| sK8_skl(sK10_skl,sK9_skl) = sK9_skl
| head_of(sK10_skl) != tail_of(sK8_skl(sK10_skl,sK9_skl))
| sK10_skl = sK8_skl(sK10_skl,sK9_skl) ),
inference(resolution,[status(thm)],[f602,f497]) ).
fof(f621,definition,
( sQ62_spl
<=> sK10_skl = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f622,plain,
( ~ sQ62_spl
| sK10_skl = sK9_skl ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f625,definition,
( sQ63_spl
<=> sK10_skl = sK8_skl(sK10_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f626,plain,
( ~ sQ63_spl
| sK10_skl = sK8_skl(sK10_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f625]) ).
fof(f628,definition,
( sQ64_spl
<=> head_of(sK10_skl) = tail_of(sK8_skl(sK10_skl,sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f630,plain,
( sQ64_spl
| head_of(sK10_skl) != tail_of(sK8_skl(sK10_skl,sK9_skl)) ),
inference(component_clause,[status(thm)],[f628]) ).
fof(f631,definition,
( sQ65_spl
<=> sK8_skl(sK10_skl,sK9_skl) = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( ~ sQ65_spl
| sK8_skl(sK10_skl,sK9_skl) = sK9_skl ),
inference(component_clause,[status(thm)],[f631]) ).
fof(f634,definition,
( sQ66_spl
<=> head_of(sK8_skl(sK10_skl,sK9_skl)) = tail_of(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f636,plain,
( sQ66_spl
| head_of(sK8_skl(sK10_skl,sK9_skl)) != tail_of(sK9_skl) ),
inference(component_clause,[status(thm)],[f634]) ).
fof(f637,plain,
( ~ sQ48_spl
| ~ sQ61_spl
| ~ sQ66_spl
| sQ65_spl
| ~ sQ64_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f608,f625,f628,f631,f634,f601,f496]) ).
fof(f674,plain,
( sQ66_spl
| ~ sQ7_spl
| tail_of(sK9_skl) != tail_of(sK9_skl) ),
inference(forward_demodulation,[status(thm)],[f566,f636]) ).
fof(f675,plain,
( sQ66_spl
| ~ sQ7_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f674]) ).
fof(f676,plain,
( sQ66_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f675]) ).
fof(f697,plain,
( ~ sQ62_spl
| sequential(sK9_skl,sK9_skl) ),
inference(backward_demodulation,[status(thm)],[f622,f129]) ).
fof(f730,plain,
( ~ sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f697,f174]) ).
fof(f731,plain,
~ sQ62_spl,
inference(contradiction_clause,[status(thm)],[f730]) ).
fof(f761,definition,
! [X0,X1,X2] :
( sQ77_spl
<=> ( ~ precedes(sK9_skl,sK10_skl,X2)
| ~ shortest_path(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f762,plain,
! [X0,X1,X2] :
( ~ sQ77_spl
| ~ precedes(sK9_skl,sK10_skl,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(component_clause,[status(thm)],[f761]) ).
fof(f823,definition,
( sQ81_spl
<=> path(sK12_skl,sK13_skl,sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f825,plain,
( sQ81_spl
| ~ path(sK12_skl,sK13_skl,sK11_skl) ),
inference(component_clause,[status(thm)],[f823]) ).
fof(f845,plain,
( sQ81_spl
| ~ shortest_path(sK12_skl,sK13_skl,sK11_skl) ),
inference(resolution,[status(thm)],[f825,f85]) ).
fof(f846,plain,
( sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f845,f127]) ).
fof(f847,plain,
sQ81_spl,
inference(contradiction_clause,[status(thm)],[f846]) ).
fof(f893,plain,
! [X0,X1] :
( ~ sQ77_spl
| ~ shortest_path(X0,X1,sK11_skl) ),
inference(resolution,[status(thm)],[f762,f128]) ).
fof(f894,plain,
( ~ sQ77_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f127,f893]) ).
fof(f895,plain,
~ sQ77_spl,
inference(contradiction_clause,[status(thm)],[f894]) ).
fof(f901,plain,
( sQ64_spl
| ~ sQ6_spl
| head_of(sK10_skl) != head_of(sK10_skl) ),
inference(forward_demodulation,[status(thm)],[f479,f630]) ).
fof(f902,plain,
( sQ64_spl
| ~ sQ6_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f901]) ).
fof(f903,plain,
( sQ64_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f902]) ).
fof(f904,plain,
( ~ sQ6_spl
| ~ sQ63_spl
| tail_of(sK10_skl) = head_of(sK10_skl) ),
inference(backward_demodulation,[status(thm)],[f626,f479]) ).
fof(f908,plain,
( ~ sQ6_spl
| ~ sQ63_spl
| head_of(sK9_skl) = head_of(sK10_skl) ),
inference(forward_demodulation,[status(thm)],[f236,f904]) ).
fof(f909,plain,
( ~ sQ6_spl
| ~ sQ63_spl
| sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f908,f255]) ).
fof(f910,plain,
( ~ sQ6_spl
| ~ sQ63_spl
| sQ20_spl ),
inference(contradiction_clause,[status(thm)],[f909]) ).
fof(f927,plain,
( ~ sQ6_spl
| ~ sQ65_spl
| tail_of(sK9_skl) = head_of(sK10_skl) ),
inference(forward_demodulation,[status(thm)],[f632,f479]) ).
fof(f928,plain,
( ~ sQ6_spl
| ~ sQ65_spl
| sQ46_spl
| ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f927,f568]) ).
fof(f929,plain,
( ~ sQ6_spl
| ~ sQ65_spl
| sQ46_spl
| ~ sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f928]) ).
fof(f930,plain,
$false,
inference(sat_refutation,[status(thm)],[f163,f167,f171,f179,f256,f267,f441,f507,f539,f604,f637,f676,f731,f847,f895,f903,f910,f929]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA008+2 : 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.36 % Computer : n008.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 18:22:55 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.08/0.42 % Refutation found
% 0.08/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.08/0.45 % Elapsed time: 0.079954 seconds
% 0.08/0.45 % CPU time: 0.290434 seconds
% 0.08/0.45 % Total memory used: 86.636 MB
% 0.08/0.45 % Net memory used: 86.282 MB
%------------------------------------------------------------------------------