%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRA008+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 243.53s 41.31s
% Output : CNFRefutation 142.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 90
% Syntax : Number of formulae : 483 ( 20 unt; 77 def)
% Number of atoms : 2973 ( 627 equ)
% Maximal formula atoms : 18 ( 6 avg)
% Number of connectives : 4314 (1824 ~;2227 |; 157 &)
% ( 81 <=>; 16 =>; 1 <=; 8 <~>)
% Maximal formula depth : 25 ( 9 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 90 ( 88 usr; 77 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 1108 (1073 !; 35 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [E] :
( edge(E)
=> head_of(E) != tail_of(E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [E] :
( edge(E)
=> ( vertex(tail_of(E))
& vertex(head_of(E)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( complete
=> ! [V1,V2] :
( ( V1 != V2
& vertex(V2)
& vertex(V1) )
=> ? [E] :
( ( ( V2 = tail_of(E)
& V1 = head_of(E) )
<~> ( V1 = tail_of(E)
& V2 = head_of(E) ) )
& edge(E) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,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/sandbox2/benchmark/theBenchmark.p') ).
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/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [V1,V2,P,V] :
( ( in_path(V,P)
& path(V1,V2,P) )
=> ( ? [E] :
( ( V = tail_of(E)
| V = head_of(E) )
& on_path(E,P) )
& vertex(V) ) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,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)],[f18]) ).
fof(f20,plain,
! [E] :
( head_of(E) != tail_of(E)
| ~ edge(E) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f21,plain,
! [X0] :
( head_of(X0) != tail_of(X0)
| ~ edge(X0) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f22,plain,
! [E] :
( ( vertex(tail_of(E))
& vertex(head_of(E)) )
| ~ edge(E) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f23,plain,
! [X0] :
( vertex(head_of(X0))
| ~ edge(X0) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [X0] :
( vertex(tail_of(X0))
| ~ edge(X0) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f25,plain,
( ! [V1,V2] :
( ? [E] :
( ( ( V2 = tail_of(E)
& V1 = head_of(E) )
<~> ( V1 = tail_of(E)
& V2 = head_of(E) ) )
& edge(E) )
| V1 = V2
| ~ vertex(V2)
| ~ vertex(V1) )
| ~ complete ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f26,definition,
! [V1,V2,E] :
( sP0_prd(E,V2,V1)
<=> ( V2 = tail_of(E)
& V1 = head_of(E) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f27,plain,
( ! [V1,V2] :
( ? [E] :
( ( sP0_prd(E,V2,V1)
<~> ( V1 = tail_of(E)
& V2 = head_of(E) ) )
& edge(E) )
| V1 = V2
| ~ vertex(V2)
| ~ vertex(V1) )
| ~ complete ),
inference(formula_renaming,[status(thm)],[f25,f26]) ).
fof(f28,plain,
( ! [V1,V2] :
( ? [E] :
( ( V1 != tail_of(E)
| V2 != head_of(E)
| ~ sP0_prd(E,V2,V1) )
& ( ( V1 = tail_of(E)
& V2 = head_of(E) )
| sP0_prd(E,V2,V1) )
& edge(E) )
| V1 = V2
| ~ vertex(V2)
| ~ vertex(V1) )
| ~ complete ),
inference(NNF_transformation,[status(thm)],[f27]) ).
fof(f29,plain,
( ! [V1,V2] :
( ( ( V1 != tail_of(sK0_skl(V2,V1))
| V2 != head_of(sK0_skl(V2,V1))
| ~ sP0_prd(sK0_skl(V2,V1),V2,V1) )
& ( ( V1 = tail_of(sK0_skl(V2,V1))
& V2 = head_of(sK0_skl(V2,V1)) )
| sP0_prd(sK0_skl(V2,V1),V2,V1) )
& edge(sK0_skl(V2,V1)) )
| V1 = V2
| ~ vertex(V2)
| ~ vertex(V1) )
| ~ complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(E,sK0_skl(V2,V1))],[f28]) ).
fof(f30,plain,
! [X0,X1] :
( edge(sK0_skl(X1,X0))
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| ~ complete ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f31,plain,
! [X0,X1] :
( X1 = head_of(sK0_skl(X1,X0))
| sP0_prd(sK0_skl(X1,X0),X1,X0)
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| ~ complete ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f32,plain,
! [X0,X1] :
( X0 = tail_of(sK0_skl(X1,X0))
| sP0_prd(sK0_skl(X1,X0),X1,X0)
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| ~ complete ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f33,plain,
! [X0,X1] :
( X0 != tail_of(sK0_skl(X1,X0))
| X1 != head_of(sK0_skl(X1,X0))
| ~ sP0_prd(sK0_skl(X1,X0),X1,X0)
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| ~ complete ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f37,plain,
! [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) )
| ~ path(V1,V2,P) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f38,definition,
! [V2,P,E] :
( sP1_prd(E,P,V2)
<=> ( P = path_cons(E,empty)
& V2 = head_of(E) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f39,plain,
! [V1,V2,P] :
( ( ? [E] :
( ( sP1_prd(E,P,V2)
<~> ? [TP] :
( P = path_cons(E,TP)
& path(head_of(E),V2,TP) ) )
& V1 = tail_of(E)
& edge(E) )
& vertex(V2)
& vertex(V1) )
| ~ path(V1,V2,P) ),
inference(formula_renaming,[status(thm)],[f37,f38]) ).
fof(f40,plain,
! [V1,V2,P] :
( ( ? [E] :
( ( ! [TP] :
( P != path_cons(E,TP)
| ~ path(head_of(E),V2,TP) )
| ~ sP1_prd(E,P,V2) )
& ( ? [TP] :
( P = path_cons(E,TP)
& path(head_of(E),V2,TP) )
| sP1_prd(E,P,V2) )
& V1 = tail_of(E)
& edge(E) )
& vertex(V2)
& vertex(V1) )
| ~ path(V1,V2,P) ),
inference(NNF_transformation,[status(thm)],[f39]) ).
fof(f41,plain,
! [V1,V2,P] :
( ( ( ! [TP] :
( P != path_cons(sK1_skl(P,V2,V1),TP)
| ~ path(head_of(sK1_skl(P,V2,V1)),V2,TP) )
| ~ sP1_prd(sK1_skl(P,V2,V1),P,V2) )
& ( ( P = path_cons(sK1_skl(P,V2,V1),sK2_skl(P,V2,V1))
& path(head_of(sK1_skl(P,V2,V1)),V2,sK2_skl(P,V2,V1)) )
| sP1_prd(sK1_skl(P,V2,V1),P,V2) )
& V1 = tail_of(sK1_skl(P,V2,V1))
& edge(sK1_skl(P,V2,V1))
& vertex(V2)
& vertex(V1) )
| ~ path(V1,V2,P) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(E,sK1_skl(P,V2,V1)),skolemize(TP,sK2_skl(P,V2,V1))],[f40]) ).
fof(f44,plain,
! [X0,X1,X2] :
( ~ path(X2,X1,X0)
| edge(sK1_skl(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f45,plain,
! [X0,X1,X2] :
( ~ path(X2,X1,X0)
| tail_of(sK1_skl(X0,X1,X2)) = X2 ),
inference(cnf_transformation,[status(thm)],[f41]) ).
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] :
( ~ path(X2,X3,X1)
| edge(X0)
| ~ on_path(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
! [X0,X1,X2,X3] :
( ~ on_path(X3,X2)
| in_path(head_of(X3),X2)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f54,plain,
! [V1,V2,P,V] :
( ( ? [E] :
( ( V = tail_of(E)
| V = head_of(E) )
& on_path(E,P) )
& vertex(V) )
| ~ in_path(V,P)
| ~ path(V1,V2,P) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f55,plain,
! [P,V] :
( ( ? [E] :
( ( V = tail_of(E)
| V = head_of(E) )
& on_path(E,P) )
& vertex(V) )
| ~ in_path(V,P)
| ! [V1,V2] : ~ path(V1,V2,P) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f56,plain,
! [P,V] :
( ( ( V = tail_of(sK3_skl(V,P))
| V = head_of(sK3_skl(V,P)) )
& on_path(sK3_skl(V,P),P)
& vertex(V) )
| ~ in_path(V,P)
| ! [V1,V2] : ~ path(V1,V2,P) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(E,sK3_skl(V,P))],[f55]) ).
fof(f57,plain,
! [X0,X1,X2,X3] :
( vertex(X0)
| ~ path(X2,X3,X1)
| ~ in_path(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f58,plain,
! [X0,X1,X2,X3] :
( ~ path(X2,X3,X1)
| ~ in_path(X0,X1)
| on_path(sK3_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f59,plain,
! [X0,X1,X2,X3] :
( X0 = head_of(sK3_skl(X0,X1))
| ~ in_path(X0,X1)
| ~ path(X2,X3,X1)
| X0 = tail_of(sK3_skl(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
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(f62,plain,
! [X0,X1] :
( edge(X0)
| ~ sequential(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
! [X0,X1] :
( ~ sequential(X1,X0)
| edge(X0) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f66,plain,
! [X0,X1] :
( ~ edge(X0)
| X1 = X0
| sequential(X1,X0)
| ~ edge(X1)
| tail_of(X0) != head_of(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] :
( ~ on_path(X3,X2)
| ~ on_path(X4,X2)
| precedes(X3,X4,X2)
| ~ sequential(X3,X4)
| ~ 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] :
( ~ precedes(X0,X4,X1)
| ~ path(X2,X3,X1)
| on_path(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
! [X0,X1,X2,X3,X4] :
( ~ path(X3,X4,X2)
| on_path(X1,X2)
| ~ precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f77,plain,
! [X0,X1,X2,X3,X4] :
( ~ precedes(X0,X1,X2)
| ~ path(X3,X4,X2)
| sequential(X0,X1)
| sequential(X0,sK4_skl(X1,X0,X2)) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f78,plain,
! [X0,X1,X2,X3,X4] :
( sequential(X1,X0)
| ~ path(X3,X4,X2)
| ~ precedes(X1,X0,X2)
| precedes(sK4_skl(X0,X1,X2),X0,X2) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f79,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ precedes(X5,X1,X2)
| ~ sequential(X0,X5)
| ~ path(X3,X4,X2)
| ~ sequential(X0,X1)
| ~ precedes(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] :
( ~ shortest_path(X0,X1,X2)
| 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(X1) != head_of(X5)
| ~ precedes(X0,X5,X4)
| ~ shortest_path(X2,X3,X4)
| tail_of(X0) != tail_of(X1) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
! [X0,X1,X2,X3,X4] :
( ~ precedes(X1,X0,X2)
| ~ shortest_path(X3,X4,X2)
| ~ precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f93,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(f94,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)],[f93]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ~ edge(X1)
| ~ edge(X2)
| ~ sequential(X0,X1)
| triangle(X2,X0,X1)
| ~ sequential(X2,X0)
| ~ sequential(X1,X2)
| ~ edge(X0) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f116,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)],[f19]) ).
fof(f117,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)],[f116]) ).
fof(f118,plain,
( ! [E3] : ~ triangle(sK8_skl,sK9_skl,E3)
& sequential(sK8_skl,sK9_skl)
& precedes(sK8_skl,sK9_skl,sK10_skl)
& shortest_path(sK11_skl,sK12_skl,sK10_skl)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(E1,sK8_skl),skolemize(E2,sK9_skl),skolemize(P,sK10_skl),skolemize(V1,sK11_skl),skolemize(V2,sK12_skl)],[f117]) ).
fof(f119,plain,
complete,
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
shortest_path(sK11_skl,sK12_skl,sK10_skl),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f121,plain,
precedes(sK8_skl,sK9_skl,sK10_skl),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f122,plain,
sequential(sK8_skl,sK9_skl),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f123,plain,
! [X0] : ~ triangle(sK8_skl,sK9_skl,X0),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f124,plain,
! [V1,V2,E] :
( ( V2 != tail_of(E)
| V1 != head_of(E)
| sP0_prd(E,V2,V1) )
& ( ( V2 = tail_of(E)
& V1 = head_of(E) )
| ~ sP0_prd(E,V2,V1) ) ),
inference(NNF_transformation,[status(thm)],[f26]) ).
fof(f125,plain,
( ! [V1,V2,E] :
( V2 != tail_of(E)
| V1 != head_of(E)
| sP0_prd(E,V2,V1) )
& ! [V1,V2,E] :
( ( V2 = tail_of(E)
& V1 = head_of(E) )
| ~ sP0_prd(E,V2,V1) ) ),
inference(miniscoping,[status(thm)],[f124]) ).
fof(f126,plain,
! [X0,X1,X2] :
( X2 = head_of(X0)
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f127,plain,
! [X0,X1,X2] :
( ~ sP0_prd(X0,X1,X2)
| tail_of(X0) = X1 ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f134,definition,
( sQ0_spl
<=> complete ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f136,plain,
( sQ0_spl
| ~ complete ),
inference(component_clause,[status(thm)],[f134]) ).
fof(f137,definition,
! [X0,X1] :
( sQ1_spl
<=> ( edge(sK0_skl(X1,X0))
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f138,plain,
! [X0,X1] :
( ~ sQ1_spl
| X1 = X0
| ~ vertex(X1)
| edge(sK0_skl(X1,X0))
| ~ vertex(X0) ),
inference(component_clause,[status(thm)],[f137]) ).
fof(f140,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f30,f134,f137]) ).
fof(f141,definition,
! [X0,X1] :
( sQ2_spl
<=> ( X1 = head_of(sK0_skl(X1,X0))
| sP0_prd(sK0_skl(X1,X0),X1,X0)
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f142,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ vertex(X1)
| ~ vertex(X0)
| sP0_prd(sK0_skl(X1,X0),X1,X0)
| head_of(sK0_skl(X1,X0)) = X1
| X0 = X1 ),
inference(component_clause,[status(thm)],[f141]) ).
fof(f144,plain,
( sQ2_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f31,f134,f141]) ).
fof(f145,definition,
! [X0,X1] :
( sQ3_spl
<=> ( X0 = tail_of(sK0_skl(X1,X0))
| sP0_prd(sK0_skl(X1,X0),X1,X0)
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f146,plain,
! [X0,X1] :
( ~ sQ3_spl
| tail_of(sK0_skl(X1,X0)) = X0
| ~ vertex(X1)
| ~ vertex(X0)
| sP0_prd(sK0_skl(X1,X0),X1,X0)
| X0 = X1 ),
inference(component_clause,[status(thm)],[f145]) ).
fof(f148,plain,
( sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f32,f134,f145]) ).
fof(f149,definition,
! [X0,X1] :
( sQ4_spl
<=> ( X0 != tail_of(sK0_skl(X1,X0))
| X1 != head_of(sK0_skl(X1,X0))
| ~ sP0_prd(sK0_skl(X1,X0),X1,X0)
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f152,plain,
( sQ4_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f33,f134,f149]) ).
fof(f159,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f119,f136]) ).
fof(f160,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f159]) ).
fof(f162,plain,
! [X0,X1,X2] :
( ~ precedes(X2,X0,sK10_skl)
| tail_of(X2) != tail_of(X1)
| head_of(X0) != head_of(X1) ),
inference(resolution,[status(thm)],[f91,f120]) ).
fof(f163,plain,
! [X0,X1,X2] :
( head_of(X0) != head_of(sK9_skl)
| ~ shortest_path(X1,X2,sK10_skl)
| tail_of(sK8_skl) != tail_of(X0) ),
inference(resolution,[status(thm)],[f91,f121]) ).
fof(f164,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ shortest_path(X6,X7,X2)
| ~ path(X4,X5,X2)
| sequential(X1,X0)
| ~ precedes(X1,X0,X2)
| head_of(X0) != head_of(X3)
| tail_of(sK4_skl(X0,X1,X2)) != tail_of(X3) ),
inference(resolution,[status(thm)],[f91,f78]) ).
fof(f165,definition,
! [X0] :
( sQ5_spl
<=> ( head_of(X0) != head_of(sK9_skl)
| tail_of(sK8_skl) != tail_of(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f166,plain,
! [X0] :
( ~ sQ5_spl
| tail_of(X0) != tail_of(sK8_skl)
| head_of(sK9_skl) != head_of(X0) ),
inference(component_clause,[status(thm)],[f165]) ).
fof(f168,definition,
! [X1,X2] :
( sQ6_spl
<=> ~ shortest_path(X1,X2,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f169,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ shortest_path(X0,X1,sK10_skl) ),
inference(component_clause,[status(thm)],[f168]) ).
fof(f171,plain,
( sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f163,f165,f168]) ).
fof(f172,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| head_of(sK3_skl(tail_of(sK8_skl),X0)) != head_of(sK9_skl)
| ~ in_path(tail_of(sK8_skl),X0)
| ~ path(X1,X2,X0)
| head_of(sK3_skl(tail_of(sK8_skl),X0)) = tail_of(sK8_skl) ),
inference(resolution,[status(thm)],[f166,f59]) ).
fof(f174,plain,
! [X0,X1,X2,X3,X4] :
( head_of(X4) != head_of(sK3_skl(tail_of(X3),X2))
| head_of(sK3_skl(tail_of(X3),X2)) = tail_of(X3)
| ~ in_path(tail_of(X3),X2)
| ~ precedes(X3,X4,sK10_skl)
| ~ path(X0,X1,X2) ),
inference(resolution,[status(thm)],[f162,f59]) ).
fof(f177,plain,
! [X0,X1,X2,X3,X4] :
( sequential(X2,X0)
| ~ path(X3,X4,sK10_skl)
| ~ precedes(X2,X0,sK10_skl)
| tail_of(sK4_skl(X0,X2,sK10_skl)) != tail_of(X1)
| head_of(X0) != head_of(X1) ),
inference(resolution,[status(thm)],[f162,f78]) ).
fof(f178,plain,
! [X0,X1] :
( head_of(X0) != head_of(X1)
| ~ precedes(X0,X1,sK10_skl) ),
inference(equality_resolution,[status(thm)],[f162]) ).
fof(f179,definition,
! [X0,X1,X2] :
( sQ7_spl
<=> ( sequential(X2,X0)
| ~ precedes(X2,X0,sK10_skl)
| tail_of(sK4_skl(X0,X2,sK10_skl)) != tail_of(X1)
| head_of(X0) != head_of(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f180,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ precedes(X2,X1,sK10_skl)
| sequential(X2,X1)
| head_of(X0) != head_of(X1)
| tail_of(X0) != tail_of(sK4_skl(X1,X2,sK10_skl)) ),
inference(component_clause,[status(thm)],[f179]) ).
fof(f182,definition,
! [X3,X4] :
( sQ8_spl
<=> ~ path(X3,X4,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f183,plain,
! [X0,X1] :
( ~ sQ8_spl
| ~ path(X0,X1,sK10_skl) ),
inference(component_clause,[status(thm)],[f182]) ).
fof(f185,plain,
( sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f177,f179,f182]) ).
fof(f186,plain,
head_of(sK8_skl) != head_of(sK9_skl),
inference(resolution,[status(thm)],[f178,f121]) ).
fof(f187,plain,
! [X0,X1,X2,X3] :
( sequential(X1,X0)
| ~ path(X2,X3,sK10_skl)
| ~ precedes(X1,X0,sK10_skl)
| head_of(sK4_skl(X0,X1,sK10_skl)) != head_of(X0) ),
inference(resolution,[status(thm)],[f178,f78]) ).
fof(f188,definition,
! [X0,X1] :
( sQ9_spl
<=> ( sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| head_of(sK4_skl(X0,X1,sK10_skl)) != head_of(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( sQ8_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f187,f188,f182]) ).
fof(f192,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ edge(sK8_skl)
| sK3_skl(tail_of(sK8_skl),X0) = sK8_skl
| sequential(sK3_skl(tail_of(sK8_skl),X0),sK8_skl)
| ~ edge(sK3_skl(tail_of(sK8_skl),X0))
| ~ in_path(tail_of(sK8_skl),X0)
| ~ path(X1,X2,X0)
| head_of(sK9_skl) != head_of(sK3_skl(tail_of(sK8_skl),X0)) ),
inference(resolution,[status(thm)],[f172,f66]) ).
fof(f193,definition,
! [X0,X1,X2] :
( sQ10_spl
<=> ( sK3_skl(tail_of(sK8_skl),X0) = sK8_skl
| sequential(sK3_skl(tail_of(sK8_skl),X0),sK8_skl)
| ~ edge(sK3_skl(tail_of(sK8_skl),X0))
| ~ in_path(tail_of(sK8_skl),X0)
| ~ path(X1,X2,X0)
| head_of(sK9_skl) != head_of(sK3_skl(tail_of(sK8_skl),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f196,definition,
( sQ11_spl
<=> edge(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f198,plain,
( sQ11_spl
| ~ edge(sK8_skl) ),
inference(component_clause,[status(thm)],[f196]) ).
fof(f199,plain,
( ~ sQ5_spl
| ~ sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f192,f193,f196,f165]) ).
fof(f200,plain,
( ~ sQ6_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f120,f169]) ).
fof(f201,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f200]) ).
fof(f205,plain,
! [X0,X1,X2,X3,X4] :
( ~ precedes(X0,X4,sK10_skl)
| ~ in_path(tail_of(X0),X1)
| ~ edge(X0)
| sequential(sK3_skl(tail_of(X0),X1),X0)
| X0 = sK3_skl(tail_of(X0),X1)
| head_of(X4) != head_of(sK3_skl(tail_of(X0),X1))
| ~ path(X2,X3,X1)
| ~ edge(sK3_skl(tail_of(X0),X1)) ),
inference(resolution,[status(thm)],[f174,f66]) ).
fof(f207,plain,
! [X0,X1,X2,X3] :
( ~ path(X2,X3,X1)
| ~ edge(X0)
| sequential(sK3_skl(tail_of(X0),X1),X0)
| ~ edge(sK3_skl(tail_of(X0),X1))
| ~ in_path(tail_of(X0),X1)
| ~ precedes(X0,sK3_skl(tail_of(X0),X1),sK10_skl)
| X0 = sK3_skl(tail_of(X0),X1) ),
inference(equality_resolution,[status(thm)],[f205]) ).
fof(f211,plain,
! [X0,X1] :
( ~ sQ8_spl
| ~ shortest_path(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f84,f183]) ).
fof(f212,plain,
( ~ sQ8_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f211,f168,f182]) ).
fof(f213,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ7_spl
| head_of(X0) != head_of(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2))
| ~ in_path(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)
| sequential(X1,X0)
| ~ path(X3,X4,X2)
| ~ precedes(X1,X0,sK10_skl)
| head_of(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)) = tail_of(sK4_skl(X0,X1,sK10_skl)) ),
inference(resolution,[status(thm)],[f180,f59]) ).
fof(f215,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ7_spl
| sequential(X1,X0)
| head_of(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)) != head_of(X0)
| ~ path(X3,X4,X2)
| sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2) = sK4_skl(X0,X1,sK10_skl)
| ~ edge(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2))
| ~ edge(sK4_skl(X0,X1,sK10_skl))
| sequential(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),sK4_skl(X0,X1,sK10_skl))
| ~ precedes(X1,X0,sK10_skl)
| ~ in_path(tail_of(sK4_skl(X0,X1,sK10_skl)),X2) ),
inference(resolution,[status(thm)],[f213,f66]) ).
fof(f216,plain,
! [X0,X1] :
( ~ precedes(X1,X0,sK10_skl)
| ~ precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f92,f120]) ).
fof(f217,plain,
! [X0,X1] :
( ~ shortest_path(X0,X1,sK10_skl)
| ~ precedes(sK9_skl,sK8_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f92,f121]) ).
fof(f218,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ shortest_path(X5,X6,X2)
| ~ path(X3,X4,X2)
| ~ precedes(X1,X0,X2)
| sequential(X1,X0)
| ~ precedes(X0,sK4_skl(X0,X1,X2),X2) ),
inference(resolution,[status(thm)],[f92,f78]) ).
fof(f219,definition,
( sQ12_spl
<=> precedes(sK9_skl,sK8_skl,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f221,plain,
( sQ12_spl
| ~ precedes(sK9_skl,sK8_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f222,plain,
( sQ6_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f217,f219,f168]) ).
fof(f224,plain,
! [X0,X1,X2,X3] :
( sequential(X1,X0)
| ~ path(X2,X3,sK10_skl)
| ~ precedes(X1,X0,sK10_skl)
| ~ precedes(X0,sK4_skl(X0,X1,sK10_skl),sK10_skl) ),
inference(resolution,[status(thm)],[f216,f78]) ).
fof(f225,definition,
! [X0,X1] :
( sQ13_spl
<=> ( sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ precedes(X0,sK4_skl(X0,X1,sK10_skl),sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f228,plain,
( sQ8_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f224,f225,f182]) ).
fof(f231,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sequential(X3,X5)
| ~ precedes(X3,X4,X2)
| ~ precedes(X5,X4,X2)
| ~ sequential(X3,X4)
| ~ shortest_path(X0,X1,X2) ),
inference(resolution,[status(thm)],[f79,f84]) ).
fof(f232,plain,
! [X0,X1,X2] :
( ~ sequential(X0,sK8_skl)
| ~ path(X1,X2,sK10_skl)
| ~ sequential(X0,sK9_skl)
| ~ precedes(X0,sK9_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f79,f121]) ).
fof(f233,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( sequential(X2,X1)
| ~ path(X6,X7,X3)
| ~ precedes(X2,X1,X3)
| ~ precedes(X0,X1,X3)
| ~ sequential(X0,X1)
| ~ path(X4,X5,X3)
| ~ sequential(X0,sK4_skl(X1,X2,X3)) ),
inference(resolution,[status(thm)],[f79,f78]) ).
fof(f234,definition,
! [X0] :
( sQ14_spl
<=> ( ~ sequential(X0,sK8_skl)
| ~ sequential(X0,sK9_skl)
| ~ precedes(X0,sK9_skl,sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f235,plain,
! [X0] :
( ~ sQ14_spl
| ~ sequential(X0,sK9_skl)
| ~ sequential(X0,sK8_skl)
| ~ precedes(X0,sK9_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f234]) ).
fof(f237,plain,
( sQ8_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f232,f234,f182]) ).
fof(f245,plain,
( ~ sQ14_spl
| ~ sequential(sK8_skl,sK9_skl)
| ~ sequential(sK8_skl,sK8_skl) ),
inference(resolution,[status(thm)],[f235,f121]) ).
fof(f246,plain,
! [X0,X1,X2] :
( ~ sQ14_spl
| sequential(X0,sK9_skl)
| ~ path(X1,X2,sK10_skl)
| ~ precedes(X0,sK9_skl,sK10_skl)
| ~ sequential(sK4_skl(sK9_skl,X0,sK10_skl),sK9_skl)
| ~ sequential(sK4_skl(sK9_skl,X0,sK10_skl),sK8_skl) ),
inference(resolution,[status(thm)],[f235,f78]) ).
fof(f247,definition,
( sQ15_spl
<=> sequential(sK8_skl,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f250,definition,
( sQ16_spl
<=> sequential(sK8_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f252,plain,
( sQ16_spl
| ~ sequential(sK8_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f250]) ).
fof(f253,plain,
( ~ sQ14_spl
| ~ sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f245,f247,f250,f234]) ).
fof(f254,definition,
! [X0] :
( sQ17_spl
<=> ( sequential(X0,sK9_skl)
| ~ precedes(X0,sK9_skl,sK10_skl)
| ~ sequential(sK4_skl(sK9_skl,X0,sK10_skl),sK9_skl)
| ~ sequential(sK4_skl(sK9_skl,X0,sK10_skl),sK8_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f257,plain,
( ~ sQ14_spl
| sQ8_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f246,f254,f182,f234]) ).
fof(f258,plain,
! [X0] :
( ~ edge(X0)
| ~ edge(sK8_skl)
| ~ sequential(sK9_skl,X0)
| ~ sequential(sK8_skl,sK9_skl)
| ~ sequential(X0,sK8_skl)
| ~ edge(sK9_skl) ),
inference(resolution,[status(thm)],[f101,f123]) ).
fof(f265,definition,
( sQ18_spl
<=> edge(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f267,plain,
( sQ18_spl
| ~ edge(sK9_skl) ),
inference(component_clause,[status(thm)],[f265]) ).
fof(f268,definition,
! [X0] :
( sQ19_spl
<=> ( ~ edge(X0)
| ~ sequential(sK9_skl,X0)
| ~ sequential(X0,sK8_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f269,plain,
! [X0] :
( ~ sQ19_spl
| ~ sequential(X0,sK8_skl)
| ~ sequential(sK9_skl,X0)
| ~ edge(X0) ),
inference(component_clause,[status(thm)],[f268]) ).
fof(f271,plain,
( ~ sQ11_spl
| ~ sQ16_spl
| sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f258,f265,f268,f250,f196]) ).
fof(f272,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f252,f122]) ).
fof(f273,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f272]) ).
fof(f281,plain,
! [X0,X1] :
( ~ sQ2_spl
| X1 = X0
| ~ vertex(X1)
| X0 = head_of(sK0_skl(X1,X0))
| X1 = head_of(sK0_skl(X1,X0))
| ~ vertex(X0) ),
inference(resolution,[status(thm)],[f126,f142]) ).
fof(f282,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ vertex(X1)
| head_of(sK0_skl(X0,X1)) = X1
| ~ vertex(X0)
| X1 = X0
| tail_of(sK0_skl(X0,X1)) = X1 ),
inference(resolution,[status(thm)],[f126,f146]) ).
fof(f283,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ sQ3_spl
| ~ vertex(tail_of(sK4_skl(X1,X2,sK10_skl)))
| head_of(sK0_skl(X0,tail_of(sK4_skl(X1,X2,sK10_skl)))) != head_of(X1)
| ~ vertex(X0)
| ~ precedes(X2,X1,sK10_skl)
| X0 = tail_of(sK4_skl(X1,X2,sK10_skl))
| sequential(X2,X1)
| head_of(sK0_skl(X0,tail_of(sK4_skl(X1,X2,sK10_skl)))) = tail_of(sK4_skl(X1,X2,sK10_skl)) ),
inference(resolution,[status(thm)],[f282,f180]) ).
fof(f284,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ3_spl
| head_of(sK0_skl(X0,tail_of(sK8_skl))) != head_of(sK9_skl)
| ~ vertex(tail_of(sK8_skl))
| head_of(sK0_skl(X0,tail_of(sK8_skl))) = tail_of(sK8_skl)
| ~ vertex(X0)
| tail_of(sK8_skl) = X0 ),
inference(resolution,[status(thm)],[f282,f166]) ).
fof(f286,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ edge(sK0_skl(X1,head_of(X0)))
| X0 = sK0_skl(X1,head_of(X0))
| sequential(X0,sK0_skl(X1,head_of(X0)))
| ~ edge(X0)
| ~ vertex(head_of(X0))
| head_of(sK0_skl(X1,head_of(X0))) = head_of(X0)
| ~ vertex(X1)
| head_of(X0) = X1 ),
inference(resolution,[status(thm)],[f282,f66]) ).
fof(f287,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| ~ precedes(X2,X0,sK10_skl)
| X1 = tail_of(X2)
| ~ vertex(X1)
| ~ vertex(tail_of(X2))
| head_of(sK0_skl(X1,tail_of(X2))) = tail_of(X2)
| head_of(X0) != head_of(sK0_skl(X1,tail_of(X2))) ),
inference(resolution,[status(thm)],[f282,f162]) ).
fof(f288,definition,
! [X0] :
( sQ20_spl
<=> ( head_of(sK0_skl(X0,tail_of(sK8_skl))) != head_of(sK9_skl)
| head_of(sK0_skl(X0,tail_of(sK8_skl))) = tail_of(sK8_skl)
| ~ vertex(X0)
| tail_of(sK8_skl) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f289,plain,
! [X0] :
( ~ sQ20_spl
| head_of(sK0_skl(X0,tail_of(sK8_skl))) = tail_of(sK8_skl)
| ~ vertex(X0)
| tail_of(sK8_skl) = X0
| head_of(sK0_skl(X0,tail_of(sK8_skl))) != head_of(sK9_skl) ),
inference(component_clause,[status(thm)],[f288]) ).
fof(f291,definition,
( sQ21_spl
<=> vertex(tail_of(sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( sQ21_spl
| ~ vertex(tail_of(sK8_skl)) ),
inference(component_clause,[status(thm)],[f291]) ).
fof(f294,plain,
( ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f284,f288,f291,f145,f165]) ).
fof(f295,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| head_of(sK0_skl(X0,head_of(X1))) = head_of(X1)
| sequential(X1,sK0_skl(X0,head_of(X1)))
| ~ vertex(head_of(X1))
| head_of(X1) = X0
| X1 = sK0_skl(X0,head_of(X1))
| ~ edge(X1)
| ~ vertex(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f286,f138]) ).
fof(f298,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ edge(X1)
| sK0_skl(tail_of(X1),X0) = X1
| sequential(sK0_skl(tail_of(X1),X0),X1)
| ~ edge(sK0_skl(tail_of(X1),X0))
| tail_of(X1) = X0
| ~ vertex(tail_of(X1))
| X0 = head_of(sK0_skl(tail_of(X1),X0))
| ~ vertex(X0) ),
inference(resolution,[status(thm)],[f281,f66]) ).
fof(f301,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| X0 = sK0_skl(tail_of(X0),X1)
| ~ edge(X0)
| sequential(sK0_skl(tail_of(X0),X1),X0)
| X1 = head_of(sK0_skl(tail_of(X0),X1))
| ~ vertex(X1)
| ~ vertex(tail_of(X0))
| tail_of(X0) = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f298,f138]) ).
fof(f302,plain,
! [X0] :
( ~ sQ20_spl
| ~ edge(sK8_skl)
| sK0_skl(X0,tail_of(sK8_skl)) = sK8_skl
| sequential(sK0_skl(X0,tail_of(sK8_skl)),sK8_skl)
| ~ edge(sK0_skl(X0,tail_of(sK8_skl)))
| tail_of(sK8_skl) = X0
| ~ vertex(X0)
| head_of(sK9_skl) != head_of(sK0_skl(X0,tail_of(sK8_skl))) ),
inference(resolution,[status(thm)],[f289,f66]) ).
fof(f303,definition,
! [X0] :
( sQ22_spl
<=> ( sK0_skl(X0,tail_of(sK8_skl)) = sK8_skl
| sequential(sK0_skl(X0,tail_of(sK8_skl)),sK8_skl)
| ~ edge(sK0_skl(X0,tail_of(sK8_skl)))
| tail_of(sK8_skl) = X0
| ~ vertex(X0)
| head_of(sK9_skl) != head_of(sK0_skl(X0,tail_of(sK8_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f306,plain,
( ~ sQ20_spl
| ~ sQ11_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f302,f303,f196,f288]) ).
fof(f307,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| ~ edge(X2)
| sK0_skl(X1,tail_of(X2)) = X2
| sequential(sK0_skl(X1,tail_of(X2)),X2)
| ~ edge(sK0_skl(X1,tail_of(X2)))
| ~ precedes(X2,X0,sK10_skl)
| X1 = tail_of(X2)
| ~ vertex(X1)
| ~ vertex(tail_of(X2))
| head_of(X0) != head_of(sK0_skl(X1,tail_of(X2))) ),
inference(resolution,[status(thm)],[f287,f66]) ).
fof(f308,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| ~ sQ1_spl
| X1 = tail_of(X0)
| ~ vertex(X1)
| head_of(sK0_skl(X1,tail_of(X0))) != head_of(X2)
| sK0_skl(X1,tail_of(X0)) = X0
| ~ edge(X0)
| ~ precedes(X0,X2,sK10_skl)
| sequential(sK0_skl(X1,tail_of(X0)),X0)
| ~ vertex(tail_of(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f307,f138]) ).
fof(f309,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ sQ3_spl
| ~ edge(sK4_skl(X1,X0,sK10_skl))
| sK0_skl(X2,tail_of(sK4_skl(X1,X0,sK10_skl))) = sK4_skl(X1,X0,sK10_skl)
| sequential(sK0_skl(X2,tail_of(sK4_skl(X1,X0,sK10_skl))),sK4_skl(X1,X0,sK10_skl))
| ~ edge(sK0_skl(X2,tail_of(sK4_skl(X1,X0,sK10_skl))))
| ~ vertex(tail_of(sK4_skl(X1,X0,sK10_skl)))
| head_of(sK0_skl(X2,tail_of(sK4_skl(X1,X0,sK10_skl)))) != head_of(X1)
| ~ vertex(X2)
| ~ precedes(X0,X1,sK10_skl)
| X2 = tail_of(sK4_skl(X1,X0,sK10_skl))
| sequential(X0,X1) ),
inference(resolution,[status(thm)],[f283,f66]) ).
fof(f310,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ edge(sK4_skl(X1,X0,sK10_skl))
| ~ precedes(X0,X1,sK10_skl)
| sK4_skl(X1,X0,sK10_skl) = sK0_skl(X2,tail_of(sK4_skl(X1,X0,sK10_skl)))
| sequential(sK0_skl(X2,tail_of(sK4_skl(X1,X0,sK10_skl))),sK4_skl(X1,X0,sK10_skl))
| ~ vertex(tail_of(sK4_skl(X1,X0,sK10_skl)))
| tail_of(sK4_skl(X1,X0,sK10_skl)) = X2
| ~ vertex(X2)
| head_of(X1) != head_of(sK0_skl(X2,tail_of(sK4_skl(X1,X0,sK10_skl))))
| sequential(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f309,f138]) ).
fof(f313,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| head_of(X1) = tail_of(X0)
| ~ vertex(head_of(X1))
| tail_of(X0) = head_of(sK0_skl(head_of(X1),tail_of(X0)))
| ~ vertex(tail_of(X0))
| head_of(X1) = tail_of(X0)
| ~ vertex(head_of(X1))
| sK0_skl(head_of(X1),tail_of(X0)) = X0
| ~ edge(X0)
| ~ precedes(X0,X1,sK10_skl)
| sequential(sK0_skl(head_of(X1),tail_of(X0)),X0)
| ~ vertex(tail_of(X0)) ),
inference(resolution,[status(thm)],[f308,f281]) ).
fof(f314,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ edge(X0)
| X0 = sK0_skl(X1,tail_of(X0))
| ~ precedes(X0,sK0_skl(X1,tail_of(X0)),sK10_skl)
| sequential(sK0_skl(X1,tail_of(X0)),X0)
| ~ vertex(X1)
| ~ vertex(tail_of(X0))
| tail_of(X0) = X1 ),
inference(equality_resolution,[status(thm)],[f308]) ).
fof(f316,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sK0_skl(head_of(X1),tail_of(X0)) = X0
| head_of(sK0_skl(head_of(X1),tail_of(X0))) = tail_of(X0)
| ~ vertex(head_of(X1))
| sequential(sK0_skl(head_of(X1),tail_of(X0)),X0)
| ~ vertex(tail_of(X0))
| ~ edge(X0)
| ~ precedes(X0,X1,sK10_skl)
| tail_of(X0) = head_of(X1) ),
inference(duplicate_literals_removal,[status(thm)],[f313]) ).
fof(f321,plain,
! [X0,X1,X2] :
( ~ sequential(X0,X2)
| ~ precedes(X2,X1,sK10_skl)
| ~ precedes(X0,X1,sK10_skl)
| ~ sequential(X0,X1) ),
inference(resolution,[status(thm)],[f231,f120]) ).
fof(f322,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ edge(X0)
| sK0_skl(head_of(X1),tail_of(X0)) = X0
| sequential(sK0_skl(head_of(X1),tail_of(X0)),X0)
| ~ edge(sK0_skl(head_of(X1),tail_of(X0)))
| sK0_skl(head_of(X1),tail_of(X0)) = X0
| ~ vertex(head_of(X1))
| sequential(sK0_skl(head_of(X1),tail_of(X0)),X0)
| ~ vertex(tail_of(X0))
| ~ edge(X0)
| ~ precedes(X0,X1,sK10_skl)
| tail_of(X0) = head_of(X1) ),
inference(resolution,[status(thm)],[f316,f66]) ).
fof(f323,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ edge(sK0_skl(head_of(X1),tail_of(X0)))
| sK0_skl(head_of(X1),tail_of(X0)) = X0
| ~ vertex(head_of(X1))
| sequential(sK0_skl(head_of(X1),tail_of(X0)),X0)
| ~ vertex(tail_of(X0))
| ~ edge(X0)
| ~ precedes(X0,X1,sK10_skl)
| tail_of(X0) = head_of(X1) ),
inference(duplicate_literals_removal,[status(thm)],[f322]) ).
fof(f324,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ vertex(head_of(X0))
| sK0_skl(head_of(X0),tail_of(X1)) = X1
| sequential(sK0_skl(head_of(X0),tail_of(X1)),X1)
| ~ precedes(X1,X0,sK10_skl)
| ~ edge(X1)
| ~ vertex(tail_of(X1))
| head_of(X0) = tail_of(X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f323,f138]) ).
fof(f326,plain,
! [X0,X1,X2,X3,X4] :
( sequential(X2,X1)
| ~ path(X3,X4,sK10_skl)
| ~ precedes(X2,X1,sK10_skl)
| ~ sequential(X0,sK4_skl(X1,X2,sK10_skl))
| ~ precedes(X0,X1,sK10_skl)
| ~ sequential(X0,X1) ),
inference(resolution,[status(thm)],[f321,f78]) ).
fof(f327,definition,
! [X0,X1,X2] :
( sQ23_spl
<=> ( sequential(X2,X1)
| ~ precedes(X2,X1,sK10_skl)
| ~ sequential(X0,sK4_skl(X1,X2,sK10_skl))
| ~ precedes(X0,X1,sK10_skl)
| ~ sequential(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f328,plain,
! [X0,X1,X2] :
( ~ sQ23_spl
| ~ precedes(X2,X1,sK10_skl)
| ~ precedes(X0,X1,sK10_skl)
| ~ sequential(X0,sK4_skl(X1,X2,sK10_skl))
| sequential(X2,X1)
| ~ sequential(X0,X1) ),
inference(component_clause,[status(thm)],[f327]) ).
fof(f330,plain,
( sQ8_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f326,f327,f182]) ).
fof(f335,plain,
! [X0,X1,X2,X3] :
( ~ sQ23_spl
| ~ precedes(X0,X1,sK10_skl)
| ~ path(X2,X3,sK10_skl)
| sequential(X0,X1)
| ~ precedes(X0,X1,sK10_skl)
| ~ precedes(X0,X1,sK10_skl)
| sequential(X0,X1)
| ~ sequential(X0,X1) ),
inference(resolution,[status(thm)],[f328,f77]) ).
fof(f338,definition,
! [X0,X1] :
( sQ24_spl
<=> ( ~ precedes(X0,X1,sK10_skl)
| sequential(X0,X1)
| ~ precedes(X0,X1,sK10_skl)
| ~ precedes(X0,X1,sK10_skl)
| sequential(X0,X1)
| ~ sequential(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f341,plain,
( ~ sQ23_spl
| sQ8_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f335,f338,f182,f327]) ).
fof(f342,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ in_path(tail_of(sK4_skl(X7,X6,X5)),X2)
| head_of(sK3_skl(tail_of(sK4_skl(X7,X6,X5)),X2)) != head_of(X7)
| tail_of(sK4_skl(X7,X6,X5)) = head_of(sK3_skl(tail_of(sK4_skl(X7,X6,X5)),X2))
| ~ path(X8,X9,X5)
| ~ precedes(X6,X7,X5)
| sequential(X6,X7)
| ~ shortest_path(X3,X4,X5)
| ~ path(X0,X1,X2) ),
inference(resolution,[status(thm)],[f164,f59]) ).
fof(f343,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ3_spl
| sequential(X3,X4)
| ~ shortest_path(X6,X7,X2)
| head_of(sK0_skl(X5,tail_of(sK4_skl(X4,X3,X2)))) != head_of(X4)
| tail_of(sK4_skl(X4,X3,X2)) = X5
| ~ vertex(X5)
| ~ vertex(tail_of(sK4_skl(X4,X3,X2)))
| tail_of(sK4_skl(X4,X3,X2)) = head_of(sK0_skl(X5,tail_of(sK4_skl(X4,X3,X2))))
| ~ precedes(X3,X4,X2)
| ~ path(X0,X1,X2) ),
inference(resolution,[status(thm)],[f164,f282]) ).
fof(f345,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( sequential(X1,X0)
| ~ path(X8,X9,X3)
| ~ shortest_path(X6,X7,X2)
| ~ in_path(tail_of(sK4_skl(X0,X1,X2)),X3)
| head_of(X0) != head_of(sK3_skl(tail_of(sK4_skl(X0,X1,X2)),X3))
| ~ precedes(X1,X0,X2)
| sK4_skl(X0,X1,X2) = sK3_skl(tail_of(sK4_skl(X0,X1,X2)),X3)
| sequential(sK3_skl(tail_of(sK4_skl(X0,X1,X2)),X3),sK4_skl(X0,X1,X2))
| ~ path(X4,X5,X2)
| ~ edge(sK4_skl(X0,X1,X2))
| ~ edge(sK3_skl(tail_of(sK4_skl(X0,X1,X2)),X3)) ),
inference(resolution,[status(thm)],[f342,f66]) ).
fof(f346,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ3_spl
| ~ edge(sK4_skl(X4,X3,X2))
| sK0_skl(X5,tail_of(sK4_skl(X4,X3,X2))) = sK4_skl(X4,X3,X2)
| sequential(sK0_skl(X5,tail_of(sK4_skl(X4,X3,X2))),sK4_skl(X4,X3,X2))
| ~ edge(sK0_skl(X5,tail_of(sK4_skl(X4,X3,X2))))
| sequential(X3,X4)
| ~ shortest_path(X6,X7,X2)
| head_of(sK0_skl(X5,tail_of(sK4_skl(X4,X3,X2)))) != head_of(X4)
| tail_of(sK4_skl(X4,X3,X2)) = X5
| ~ vertex(X5)
| ~ vertex(tail_of(sK4_skl(X4,X3,X2)))
| ~ precedes(X3,X4,X2)
| ~ path(X0,X1,X2) ),
inference(resolution,[status(thm)],[f343,f66]) ).
fof(f347,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ3_spl
| ~ sQ1_spl
| sK4_skl(X0,X1,X2) = sK0_skl(X3,tail_of(sK4_skl(X0,X1,X2)))
| ~ precedes(X1,X0,X2)
| sequential(sK0_skl(X3,tail_of(sK4_skl(X0,X1,X2))),sK4_skl(X0,X1,X2))
| head_of(sK0_skl(X3,tail_of(sK4_skl(X0,X1,X2)))) != head_of(X0)
| ~ shortest_path(X6,X7,X2)
| ~ path(X4,X5,X2)
| sequential(X1,X0)
| ~ vertex(X3)
| ~ edge(sK4_skl(X0,X1,X2))
| tail_of(sK4_skl(X0,X1,X2)) = X3
| ~ vertex(tail_of(sK4_skl(X0,X1,X2))) ),
inference(forward_subsumption_resolution,[status(thm)],[f346,f138]) ).
fof(f349,definition,
! [X0,X1,X2,X7,X8] :
( sQ25_spl
<=> ( ~ precedes(X1,X0,sK10_skl)
| ~ precedes(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),X0,sK10_skl)
| sequential(X1,X0)
| ~ sequential(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),X0)
| sequential(X1,X0)
| ~ path(X7,X8,X2)
| ~ in_path(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)
| head_of(X0) != head_of(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2))
| ~ precedes(X1,X0,sK10_skl)
| sK4_skl(X0,X1,sK10_skl) = sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)
| ~ edge(sK4_skl(X0,X1,sK10_skl))
| ~ edge(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f355,definition,
! [X0,X1,X2] :
( sQ26_spl
<=> ( ~ precedes(X1,X0,sK10_skl)
| ~ precedes(sK0_skl(X2,tail_of(sK4_skl(X0,X1,sK10_skl))),X0,sK10_skl)
| sequential(X1,X0)
| ~ sequential(sK0_skl(X2,tail_of(sK4_skl(X0,X1,sK10_skl))),X0)
| sK4_skl(X0,X1,sK10_skl) = sK0_skl(X2,tail_of(sK4_skl(X0,X1,sK10_skl)))
| ~ precedes(X1,X0,sK10_skl)
| head_of(sK0_skl(X2,tail_of(sK4_skl(X0,X1,sK10_skl)))) != head_of(X0)
| sequential(X1,X0)
| ~ vertex(X2)
| ~ edge(sK4_skl(X0,X1,sK10_skl))
| tail_of(sK4_skl(X0,X1,sK10_skl)) = X2
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f362,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ7_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ edge(sK4_skl(X3,X4,sK10_skl))
| ~ precedes(X4,X3,sK10_skl)
| sK4_skl(X3,X4,sK10_skl) = sK0_skl(X2,tail_of(sK4_skl(X3,X4,sK10_skl)))
| ~ vertex(tail_of(sK4_skl(X3,X4,sK10_skl)))
| tail_of(sK4_skl(X3,X4,sK10_skl)) = X2
| ~ vertex(X2)
| head_of(X3) != head_of(sK0_skl(X2,tail_of(sK4_skl(X3,X4,sK10_skl))))
| sequential(X4,X3)
| sequential(X4,X3)
| ~ path(X5,X6,sK10_skl)
| ~ precedes(X4,X3,sK10_skl)
| ~ precedes(sK0_skl(X2,tail_of(sK4_skl(X3,X4,sK10_skl))),X3,sK10_skl)
| ~ sequential(sK0_skl(X2,tail_of(sK4_skl(X3,X4,sK10_skl))),X3)
| ~ path(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f233,f310]) ).
fof(f364,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ sQ7_spl
| sequential(X3,X2)
| head_of(sK3_skl(tail_of(sK4_skl(X2,X3,sK10_skl)),X4)) != head_of(X2)
| ~ path(X7,X8,X4)
| sK3_skl(tail_of(sK4_skl(X2,X3,sK10_skl)),X4) = sK4_skl(X2,X3,sK10_skl)
| ~ edge(sK3_skl(tail_of(sK4_skl(X2,X3,sK10_skl)),X4))
| ~ edge(sK4_skl(X2,X3,sK10_skl))
| ~ precedes(X3,X2,sK10_skl)
| ~ in_path(tail_of(sK4_skl(X2,X3,sK10_skl)),X4)
| sequential(X3,X2)
| ~ path(X5,X6,sK10_skl)
| ~ precedes(X3,X2,sK10_skl)
| ~ precedes(sK3_skl(tail_of(sK4_skl(X2,X3,sK10_skl)),X4),X2,sK10_skl)
| ~ sequential(sK3_skl(tail_of(sK4_skl(X2,X3,sK10_skl)),X4),X2)
| ~ path(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f233,f215]) ).
fof(f367,plain,
( ~ sQ7_spl
| sQ25_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f364,f182,f349,f179]) ).
fof(f370,plain,
( ~ sQ7_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sQ26_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f362,f182,f355,f137,f145,f179]) ).
fof(f374,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ vertex(X1)
| X0 = X1
| X0 = head_of(sK0_skl(X0,X1))
| ~ vertex(X0)
| tail_of(sK0_skl(X0,X1)) = X0 ),
inference(resolution,[status(thm)],[f127,f142]) ).
fof(f375,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ vertex(X1)
| tail_of(sK0_skl(X0,X1)) = X0
| ~ vertex(X0)
| X1 = tail_of(sK0_skl(X0,X1))
| X0 = X1 ),
inference(resolution,[status(thm)],[f127,f146]) ).
fof(f376,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ sQ2_spl
| sequential(X0,X1)
| ~ vertex(X2)
| ~ vertex(tail_of(sK4_skl(X1,X0,sK10_skl)))
| head_of(sK0_skl(tail_of(sK4_skl(X1,X0,sK10_skl)),X2)) != head_of(X1)
| tail_of(sK4_skl(X1,X0,sK10_skl)) = head_of(sK0_skl(tail_of(sK4_skl(X1,X0,sK10_skl)),X2))
| X2 = tail_of(sK4_skl(X1,X0,sK10_skl))
| ~ precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f374,f180]) ).
fof(f377,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ2_spl
| head_of(sK0_skl(tail_of(sK8_skl),X0)) != head_of(sK9_skl)
| ~ vertex(X0)
| tail_of(sK8_skl) = X0
| tail_of(sK8_skl) = head_of(sK0_skl(tail_of(sK8_skl),X0))
| ~ vertex(tail_of(sK8_skl)) ),
inference(resolution,[status(thm)],[f374,f166]) ).
fof(f378,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ precedes(sK0_skl(tail_of(X1),X0),X2,sK10_skl)
| head_of(sK0_skl(tail_of(X1),X0)) = tail_of(X1)
| ~ vertex(tail_of(X1))
| head_of(X1) != head_of(X2)
| X0 = tail_of(X1)
| ~ vertex(X0) ),
inference(resolution,[status(thm)],[f374,f162]) ).
fof(f379,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ edge(sK0_skl(head_of(X0),X1))
| X0 = sK0_skl(head_of(X0),X1)
| sequential(X0,sK0_skl(head_of(X0),X1))
| ~ edge(X0)
| ~ vertex(X1)
| head_of(X0) = X1
| head_of(X0) = head_of(sK0_skl(head_of(X0),X1))
| ~ vertex(head_of(X0)) ),
inference(resolution,[status(thm)],[f374,f66]) ).
fof(f380,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ2_spl
| ~ vertex(tail_of(sK4_skl(X1,X2,X3)))
| X0 = tail_of(sK4_skl(X1,X2,X3))
| ~ path(X6,X7,X3)
| ~ precedes(X2,X1,X3)
| head_of(sK0_skl(tail_of(sK4_skl(X1,X2,X3)),X0)) != head_of(X1)
| ~ shortest_path(X4,X5,X3)
| sequential(X2,X1)
| tail_of(sK4_skl(X1,X2,X3)) = head_of(sK0_skl(tail_of(sK4_skl(X1,X2,X3)),X0))
| ~ vertex(X0) ),
inference(resolution,[status(thm)],[f374,f164]) ).
fof(f381,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ vertex(X1)
| X1 = tail_of(X0)
| ~ vertex(tail_of(X0))
| ~ precedes(X0,X2,sK10_skl)
| head_of(X2) != head_of(sK0_skl(tail_of(X0),X1))
| tail_of(X0) = head_of(sK0_skl(tail_of(X0),X1)) ),
inference(resolution,[status(thm)],[f374,f162]) ).
fof(f382,definition,
! [X0] :
( sQ27_spl
<=> ( head_of(sK0_skl(tail_of(sK8_skl),X0)) != head_of(sK9_skl)
| ~ vertex(X0)
| tail_of(sK8_skl) = X0
| tail_of(sK8_skl) = head_of(sK0_skl(tail_of(sK8_skl),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f383,plain,
! [X0] :
( ~ sQ27_spl
| tail_of(sK8_skl) = head_of(sK0_skl(tail_of(sK8_skl),X0))
| head_of(sK9_skl) != head_of(sK0_skl(tail_of(sK8_skl),X0))
| tail_of(sK8_skl) = X0
| ~ vertex(X0) ),
inference(component_clause,[status(thm)],[f382]) ).
fof(f385,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| sQ27_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f377,f291,f382,f141,f165]) ).
fof(f386,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| head_of(sK0_skl(head_of(X0),X1)) = head_of(X0)
| ~ vertex(X1)
| X0 = sK0_skl(head_of(X0),X1)
| sequential(X0,sK0_skl(head_of(X0),X1))
| X1 = head_of(X0)
| ~ vertex(head_of(X0))
| ~ edge(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f379,f138]) ).
fof(f387,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ edge(X1)
| sK0_skl(tail_of(X1),X2) = X1
| sequential(sK0_skl(tail_of(X1),X2),X1)
| ~ edge(sK0_skl(tail_of(X1),X2))
| ~ vertex(X2)
| X2 = tail_of(X1)
| ~ vertex(tail_of(X1))
| ~ precedes(X1,X0,sK10_skl)
| head_of(X0) != head_of(sK0_skl(tail_of(X1),X2)) ),
inference(resolution,[status(thm)],[f381,f66]) ).
fof(f388,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ vertex(tail_of(X0))
| ~ precedes(X0,X2,sK10_skl)
| sequential(sK0_skl(tail_of(X0),X1),X0)
| ~ edge(X0)
| head_of(sK0_skl(tail_of(X0),X1)) != head_of(X2)
| ~ vertex(X1)
| X0 = sK0_skl(tail_of(X0),X1)
| tail_of(X0) = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f387,f138]) ).
fof(f389,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ3_spl
| ~ precedes(X0,X1,X4)
| X5 = tail_of(sK0_skl(X5,tail_of(sK4_skl(X1,X0,X4))))
| ~ shortest_path(X6,X7,X4)
| X5 = tail_of(sK4_skl(X1,X0,X4))
| head_of(X1) != head_of(sK0_skl(X5,tail_of(sK4_skl(X1,X0,X4))))
| ~ vertex(X5)
| ~ vertex(tail_of(sK4_skl(X1,X0,X4)))
| ~ path(X2,X3,X4)
| sequential(X0,X1) ),
inference(resolution,[status(thm)],[f375,f164]) ).
fof(f390,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| ~ vertex(X0)
| tail_of(sK0_skl(X0,tail_of(X1))) = X0
| ~ precedes(X1,X2,sK10_skl)
| ~ vertex(tail_of(X1))
| head_of(sK0_skl(X0,tail_of(X1))) != head_of(X2)
| X0 = tail_of(X1) ),
inference(resolution,[status(thm)],[f375,f162]) ).
fof(f391,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ sQ3_spl
| ~ vertex(X2)
| ~ precedes(X1,X0,sK10_skl)
| tail_of(sK4_skl(X0,X1,sK10_skl)) = X2
| X2 = tail_of(sK0_skl(X2,tail_of(sK4_skl(X0,X1,sK10_skl))))
| sequential(X1,X0)
| head_of(sK0_skl(X2,tail_of(sK4_skl(X0,X1,sK10_skl)))) != head_of(X0)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl))) ),
inference(resolution,[status(thm)],[f375,f180]) ).
fof(f392,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ3_spl
| head_of(sK0_skl(X0,tail_of(sK8_skl))) != head_of(sK9_skl)
| ~ vertex(tail_of(sK8_skl))
| tail_of(sK0_skl(X0,tail_of(sK8_skl))) = X0
| ~ vertex(X0)
| X0 = tail_of(sK8_skl) ),
inference(resolution,[status(thm)],[f375,f166]) ).
fof(f393,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| X0 = tail_of(sK0_skl(X0,tail_of(X1)))
| ~ vertex(tail_of(X1))
| ~ precedes(sK0_skl(X0,tail_of(X1)),X2,sK10_skl)
| head_of(X1) != head_of(X2)
| X0 = tail_of(X1)
| ~ vertex(X0) ),
inference(resolution,[status(thm)],[f375,f162]) ).
fof(f394,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ edge(sK0_skl(X0,head_of(X1)))
| X1 = sK0_skl(X0,head_of(X1))
| sequential(X1,sK0_skl(X0,head_of(X1)))
| ~ edge(X1)
| ~ vertex(head_of(X1))
| tail_of(sK0_skl(X0,head_of(X1))) = X0
| ~ vertex(X0)
| X0 = head_of(X1) ),
inference(resolution,[status(thm)],[f375,f66]) ).
fof(f396,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| head_of(X0) = X1
| ~ edge(X0)
| tail_of(sK0_skl(X1,head_of(X0))) = X1
| ~ vertex(head_of(X0))
| sequential(X0,sK0_skl(X1,head_of(X0)))
| ~ vertex(X1)
| X0 = sK0_skl(X1,head_of(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f394,f138]) ).
fof(f397,definition,
! [X0] :
( sQ28_spl
<=> ( head_of(sK0_skl(X0,tail_of(sK8_skl))) != head_of(sK9_skl)
| tail_of(sK0_skl(X0,tail_of(sK8_skl))) = X0
| ~ vertex(X0)
| X0 = tail_of(sK8_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f400,plain,
( ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ21_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f392,f397,f291,f145,f165]) ).
fof(f411,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ vertex(head_of(X0))
| tail_of(sK0_skl(head_of(X0),tail_of(X1))) = head_of(X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ vertex(tail_of(X1))
| head_of(X0) = tail_of(X1)
| ~ vertex(tail_of(X1))
| X0 = sK0_skl(head_of(X0),tail_of(X1))
| sequential(X0,sK0_skl(head_of(X0),tail_of(X1)))
| tail_of(X1) = head_of(X0)
| ~ vertex(head_of(X0))
| ~ edge(X0) ),
inference(resolution,[status(thm)],[f386,f390]) ).
fof(f416,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ vertex(tail_of(X0))
| head_of(X1) = tail_of(sK0_skl(head_of(X1),tail_of(X0)))
| head_of(X1) = tail_of(X0)
| sK0_skl(head_of(X1),tail_of(X0)) = X1
| ~ vertex(head_of(X1))
| ~ edge(X1)
| sequential(X1,sK0_skl(head_of(X1),tail_of(X0)))
| ~ precedes(X0,X1,sK10_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f411]) ).
fof(f421,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ2_spl
| sequential(X1,sK0_skl(tail_of(X0),head_of(X1)))
| ~ vertex(head_of(X1))
| head_of(X1) = tail_of(X0)
| X1 = sK0_skl(tail_of(X0),head_of(X1))
| ~ edge(X1)
| ~ vertex(tail_of(X0))
| ~ vertex(tail_of(X0))
| ~ precedes(X0,X1,sK10_skl)
| sequential(sK0_skl(tail_of(X0),head_of(X1)),X0)
| ~ edge(X0)
| ~ vertex(head_of(X1))
| X0 = sK0_skl(tail_of(X0),head_of(X1))
| tail_of(X0) = head_of(X1) ),
inference(resolution,[status(thm)],[f388,f295]) ).
fof(f428,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ2_spl
| sK0_skl(tail_of(X0),head_of(X1)) = X1
| sequential(X1,sK0_skl(tail_of(X0),head_of(X1)))
| ~ edge(X0)
| sequential(sK0_skl(tail_of(X0),head_of(X1)),X0)
| ~ edge(X1)
| ~ vertex(tail_of(X0))
| ~ precedes(X0,X1,sK10_skl)
| sK0_skl(tail_of(X0),head_of(X1)) = X0
| ~ vertex(head_of(X1))
| tail_of(X0) = head_of(X1) ),
inference(duplicate_literals_removal,[status(thm)],[f421]) ).
fof(f433,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ edge(sK0_skl(head_of(X1),tail_of(X0)))
| X1 = sK0_skl(head_of(X1),tail_of(X0))
| sequential(X1,sK0_skl(head_of(X1),tail_of(X0)))
| ~ edge(X1)
| ~ vertex(tail_of(X0))
| head_of(X1) = tail_of(X0)
| sK0_skl(head_of(X1),tail_of(X0)) = X1
| ~ vertex(head_of(X1))
| ~ edge(X1)
| sequential(X1,sK0_skl(head_of(X1),tail_of(X0)))
| ~ precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f416,f66]) ).
fof(f434,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ edge(sK0_skl(head_of(X1),tail_of(X0)))
| ~ vertex(tail_of(X0))
| head_of(X1) = tail_of(X0)
| sK0_skl(head_of(X1),tail_of(X0)) = X1
| ~ vertex(head_of(X1))
| ~ edge(X1)
| sequential(X1,sK0_skl(head_of(X1),tail_of(X0)))
| ~ precedes(X0,X1,sK10_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f433]) ).
fof(f435,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ precedes(X1,X0,sK10_skl)
| sK0_skl(head_of(X0),tail_of(X1)) = X0
| ~ vertex(head_of(X0))
| ~ vertex(tail_of(X1))
| head_of(X0) = tail_of(X1)
| ~ edge(X0)
| sequential(X0,sK0_skl(head_of(X0),tail_of(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f434,f138]) ).
fof(f442,plain,
! [X0,X1,X2,X3] :
( vertex(X3)
| ~ in_path(X3,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(resolution,[status(thm)],[f57,f84]) ).
fof(f445,plain,
! [X0,X1,X2,X3] :
( edge(X0)
| ~ shortest_path(X2,X3,X1)
| ~ on_path(X0,X1) ),
inference(resolution,[status(thm)],[f51,f84]) ).
fof(f446,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| X0 = sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl)))
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))))
| tail_of(sK4_skl(X0,X1,sK10_skl)) = head_of(X0)
| ~ vertex(head_of(X0))
| ~ edge(X0)
| ~ vertex(head_of(X0))
| ~ precedes(X1,X0,sK10_skl)
| tail_of(sK4_skl(X0,X1,sK10_skl)) = head_of(X0)
| head_of(X0) = tail_of(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))))
| sequential(X1,X0)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl))) ),
inference(resolution,[status(thm)],[f391,f386]) ).
fof(f447,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ7_spl
| ~ sQ3_spl
| head_of(X0) = tail_of(sK4_skl(X0,X1,sK10_skl))
| ~ vertex(head_of(X0))
| tail_of(sK4_skl(X0,X1,sK10_skl)) = head_of(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))))
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| ~ vertex(head_of(X0))
| ~ precedes(X1,X0,sK10_skl)
| tail_of(sK4_skl(X0,X1,sK10_skl)) = head_of(X0)
| head_of(X0) = tail_of(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))))
| sequential(X1,X0)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl))) ),
inference(resolution,[status(thm)],[f391,f281]) ).
fof(f448,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ precedes(X0,X1,sK10_skl)
| head_of(X1) = tail_of(sK4_skl(X1,X0,sK10_skl))
| head_of(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl)))) = tail_of(sK4_skl(X1,X0,sK10_skl))
| head_of(X1) = tail_of(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl))))
| ~ vertex(head_of(X1))
| ~ vertex(tail_of(sK4_skl(X1,X0,sK10_skl)))
| sequential(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f447]) ).
fof(f449,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ edge(X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| tail_of(sK4_skl(X0,X1,sK10_skl)) = head_of(X0)
| tail_of(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl)))) = head_of(X0)
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))) = X0
| ~ vertex(head_of(X0))
| sequential(X1,X0)
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl)))) ),
inference(duplicate_literals_removal,[status(thm)],[f446]) ).
fof(f450,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ2_spl
| ~ edge(sK4_skl(X2,X1,X5))
| sK0_skl(tail_of(sK4_skl(X2,X1,X5)),X0) = sK4_skl(X2,X1,X5)
| sequential(sK0_skl(tail_of(sK4_skl(X2,X1,X5)),X0),sK4_skl(X2,X1,X5))
| ~ edge(sK0_skl(tail_of(sK4_skl(X2,X1,X5)),X0))
| ~ vertex(tail_of(sK4_skl(X2,X1,X5)))
| X0 = tail_of(sK4_skl(X2,X1,X5))
| ~ path(X6,X7,X5)
| ~ precedes(X1,X2,X5)
| head_of(sK0_skl(tail_of(sK4_skl(X2,X1,X5)),X0)) != head_of(X2)
| ~ shortest_path(X3,X4,X5)
| sequential(X1,X2)
| ~ vertex(X0) ),
inference(resolution,[status(thm)],[f380,f66]) ).
fof(f451,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ2_spl
| ~ sQ1_spl
| sK4_skl(X1,X0,X4) = sK0_skl(tail_of(sK4_skl(X1,X0,X4)),X5)
| ~ path(X6,X7,X4)
| ~ edge(sK4_skl(X1,X0,X4))
| ~ precedes(X0,X1,X4)
| head_of(sK0_skl(tail_of(sK4_skl(X1,X0,X4)),X5)) != head_of(X1)
| ~ vertex(X5)
| ~ vertex(tail_of(sK4_skl(X1,X0,X4)))
| X5 = tail_of(sK4_skl(X1,X0,X4))
| sequential(sK0_skl(tail_of(sK4_skl(X1,X0,X4)),X5),sK4_skl(X1,X0,X4))
| ~ shortest_path(X2,X3,X4)
| sequential(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f450,f138]) ).
fof(f453,plain,
! [X0] :
( ~ in_path(X0,sK10_skl)
| vertex(X0) ),
inference(resolution,[status(thm)],[f442,f120]) ).
fof(f456,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ sQ2_spl
| ~ edge(sK4_skl(X1,X0,sK10_skl))
| sK0_skl(tail_of(sK4_skl(X1,X0,sK10_skl)),X2) = sK4_skl(X1,X0,sK10_skl)
| sequential(sK0_skl(tail_of(sK4_skl(X1,X0,sK10_skl)),X2),sK4_skl(X1,X0,sK10_skl))
| ~ edge(sK0_skl(tail_of(sK4_skl(X1,X0,sK10_skl)),X2))
| sequential(X0,X1)
| ~ vertex(X2)
| ~ vertex(tail_of(sK4_skl(X1,X0,sK10_skl)))
| head_of(sK0_skl(tail_of(sK4_skl(X1,X0,sK10_skl)),X2)) != head_of(X1)
| X2 = tail_of(sK4_skl(X1,X0,sK10_skl))
| ~ precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f376,f66]) ).
fof(f457,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ sQ2_spl
| ~ sQ1_spl
| head_of(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)) != head_of(X0)
| tail_of(sK4_skl(X0,X1,sK10_skl)) = X2
| sequential(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),sK4_skl(X0,X1,sK10_skl))
| sK4_skl(X0,X1,sK10_skl) = sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)
| ~ vertex(X2)
| ~ edge(sK4_skl(X0,X1,sK10_skl))
| sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f456,f138]) ).
fof(f458,plain,
! [X0] :
( ~ on_path(X0,sK10_skl)
| edge(X0) ),
inference(resolution,[status(thm)],[f445,f120]) ).
fof(f460,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| ~ vertex(tail_of(sK4_skl(X1,X0,X4)))
| X1 = sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,X4)))
| sequential(X1,sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,X4))))
| tail_of(sK4_skl(X1,X0,X4)) = head_of(X1)
| ~ vertex(head_of(X1))
| ~ edge(X1)
| ~ precedes(X0,X1,X4)
| head_of(X1) = tail_of(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,X4))))
| ~ shortest_path(X5,X6,X4)
| head_of(X1) = tail_of(sK4_skl(X1,X0,X4))
| ~ vertex(head_of(X1))
| ~ vertex(tail_of(sK4_skl(X1,X0,X4)))
| ~ path(X2,X3,X4)
| sequential(X0,X1) ),
inference(resolution,[status(thm)],[f389,f386]) ).
fof(f462,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| sequential(X1,X0)
| tail_of(sK4_skl(X0,X1,X2)) = head_of(X0)
| ~ edge(X0)
| ~ precedes(X1,X0,X2)
| tail_of(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2)))) = head_of(X0)
| ~ vertex(tail_of(sK4_skl(X0,X1,X2)))
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))) = X0
| ~ path(X5,X6,X2)
| ~ shortest_path(X3,X4,X2)
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))))
| ~ vertex(head_of(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f460]) ).
fof(f463,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ edge(sK4_skl(X1,X0,sK10_skl))
| sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl))) = sK4_skl(X1,X0,sK10_skl)
| sequential(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl))),sK4_skl(X1,X0,sK10_skl))
| ~ edge(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl))))
| ~ precedes(X0,X1,sK10_skl)
| head_of(X1) = tail_of(sK4_skl(X1,X0,sK10_skl))
| head_of(X1) = tail_of(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl))))
| ~ vertex(head_of(X1))
| ~ vertex(tail_of(sK4_skl(X1,X0,sK10_skl)))
| sequential(X0,X1) ),
inference(resolution,[status(thm)],[f448,f66]) ).
fof(f464,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))) = sK4_skl(X0,X1,sK10_skl)
| tail_of(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl)))) = head_of(X0)
| sequential(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))),sK4_skl(X0,X1,sK10_skl))
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| head_of(X0) = tail_of(sK4_skl(X0,X1,sK10_skl))
| ~ edge(sK4_skl(X0,X1,sK10_skl))
| ~ vertex(head_of(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f463,f138]) ).
fof(f467,plain,
! [X0,X1,X2] :
( ~ path(X1,X2,sK10_skl)
| ~ in_path(X0,sK10_skl)
| edge(sK3_skl(X0,sK10_skl)) ),
inference(resolution,[status(thm)],[f458,f58]) ).
fof(f468,definition,
! [X0] :
( sQ29_spl
<=> ( ~ in_path(X0,sK10_skl)
| edge(sK3_skl(X0,sK10_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( sQ8_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f467,f468,f182]) ).
fof(f472,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ edge(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))))
| X0 = sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl)))
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))))
| ~ edge(X0)
| ~ edge(X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| tail_of(sK4_skl(X0,X1,sK10_skl)) = head_of(X0)
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))) = X0
| ~ vertex(head_of(X0))
| sequential(X1,X0)
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl)))) ),
inference(resolution,[status(thm)],[f449,f66]) ).
fof(f473,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ edge(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))))
| ~ edge(X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| tail_of(sK4_skl(X0,X1,sK10_skl)) = head_of(X0)
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))) = X0
| ~ vertex(head_of(X0))
| sequential(X1,X0)
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl)))) ),
inference(duplicate_literals_removal,[status(thm)],[f472]) ).
fof(f474,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ precedes(X1,X0,sK10_skl)
| ~ vertex(head_of(X0))
| tail_of(sK4_skl(X0,X1,sK10_skl)) = head_of(X0)
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))) = X0
| sequential(X1,X0)
| ~ edge(X0)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f473,f138]) ).
fof(f477,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| ~ edge(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))))
| X0 = sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2)))
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))))
| ~ edge(X0)
| sequential(X1,X0)
| tail_of(sK4_skl(X0,X1,X2)) = head_of(X0)
| ~ edge(X0)
| ~ precedes(X1,X0,X2)
| ~ vertex(tail_of(sK4_skl(X0,X1,X2)))
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))) = X0
| ~ path(X5,X6,X2)
| ~ shortest_path(X3,X4,X2)
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))))
| ~ vertex(head_of(X0)) ),
inference(resolution,[status(thm)],[f462,f66]) ).
fof(f478,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| ~ edge(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))))
| sequential(X1,X0)
| tail_of(sK4_skl(X0,X1,X2)) = head_of(X0)
| ~ edge(X0)
| ~ precedes(X1,X0,X2)
| ~ vertex(tail_of(sK4_skl(X0,X1,X2)))
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))) = X0
| ~ path(X5,X6,X2)
| ~ shortest_path(X3,X4,X2)
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))))
| ~ vertex(head_of(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f477]) ).
fof(f479,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| sequential(X4,X3)
| ~ path(X5,X6,X2)
| ~ edge(X3)
| head_of(X3) = tail_of(sK4_skl(X3,X4,X2))
| ~ vertex(head_of(X3))
| sequential(X3,sK0_skl(head_of(X3),tail_of(sK4_skl(X3,X4,X2))))
| ~ precedes(X4,X3,X2)
| X3 = sK0_skl(head_of(X3),tail_of(sK4_skl(X3,X4,X2)))
| ~ vertex(tail_of(sK4_skl(X3,X4,X2)))
| ~ shortest_path(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f478,f138]) ).
fof(f483,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ7_spl
| ~ sQ2_spl
| ~ sQ1_spl
| sequential(X1,X0)
| ~ path(X5,X6,sK10_skl)
| ~ precedes(X1,X0,sK10_skl)
| ~ precedes(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),X0,sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),X0)
| ~ path(X3,X4,sK10_skl)
| head_of(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)) != head_of(X0)
| tail_of(sK4_skl(X0,X1,sK10_skl)) = X2
| sK4_skl(X0,X1,sK10_skl) = sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)
| ~ vertex(X2)
| ~ edge(sK4_skl(X0,X1,sK10_skl))
| sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl))) ),
inference(resolution,[status(thm)],[f457,f233]) ).
fof(f485,definition,
! [X0,X1,X2] :
( sQ30_spl
<=> ( sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ precedes(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),X0,sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),X0)
| head_of(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)) != head_of(X0)
| tail_of(sK4_skl(X0,X1,sK10_skl)) = X2
| sK4_skl(X0,X1,sK10_skl) = sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)
| ~ vertex(X2)
| ~ edge(sK4_skl(X0,X1,sK10_skl))
| sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( ~ sQ7_spl
| ~ sQ2_spl
| ~ sQ1_spl
| sQ8_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f483,f485,f182,f137,f141,f179]) ).
fof(f496,plain,
! [X0,X1,X2,X3,X4] :
( on_path(X4,X2)
| ~ precedes(X3,X4,X2)
| ~ shortest_path(X0,X1,X2) ),
inference(resolution,[status(thm)],[f76,f84]) ).
fof(f499,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ2_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sequential(X1,X0)
| ~ path(X4,X5,sK10_skl)
| ~ precedes(X1,X0,sK10_skl)
| ~ precedes(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))),X0,sK10_skl)
| ~ sequential(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))),X0)
| ~ path(X2,X3,sK10_skl)
| sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))) = sK4_skl(X0,X1,sK10_skl)
| tail_of(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl)))) = head_of(X0)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| head_of(X0) = tail_of(sK4_skl(X0,X1,sK10_skl))
| ~ edge(sK4_skl(X0,X1,sK10_skl))
| ~ vertex(head_of(X0)) ),
inference(resolution,[status(thm)],[f464,f233]) ).
fof(f500,definition,
! [X0,X1] :
( sQ31_spl
<=> ( sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ precedes(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))),X0,sK10_skl)
| ~ sequential(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))),X0)
| sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))) = sK4_skl(X0,X1,sK10_skl)
| tail_of(sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl)))) = head_of(X0)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| head_of(X0) = tail_of(sK4_skl(X0,X1,sK10_skl))
| ~ edge(sK4_skl(X0,X1,sK10_skl))
| ~ vertex(head_of(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f503,plain,
( ~ sQ2_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sQ8_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f499,f500,f182,f137,f145,f179,f141]) ).
fof(f510,plain,
! [X0,X1] :
( ~ precedes(X1,X0,sK10_skl)
| on_path(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f496,f120]) ).
fof(f511,plain,
on_path(sK9_skl,sK10_skl),
inference(resolution,[status(thm)],[f510,f121]) ).
fof(f512,plain,
! [X0,X1,X2,X3] :
( sequential(X1,X0)
| ~ path(X2,X3,sK10_skl)
| ~ precedes(X1,X0,sK10_skl)
| on_path(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f510,f78]) ).
fof(f513,definition,
! [X0,X1] :
( sQ32_spl
<=> ( sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| on_path(X0,sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f516,plain,
( sQ8_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f512,f513,f182]) ).
fof(f529,plain,
edge(sK9_skl),
inference(resolution,[status(thm)],[f511,f458]) ).
fof(f532,plain,
! [X0,X1,X2,X3,X4] :
( ~ shortest_path(X3,X4,X2)
| on_path(X0,X2)
| ~ precedes(X0,X1,X2) ),
inference(resolution,[status(thm)],[f75,f84]) ).
fof(f536,plain,
! [X0,X1] :
( on_path(X0,sK10_skl)
| ~ precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f532,f120]) ).
fof(f539,plain,
! [X0,X1,X2,X3,X4] :
( precedes(X2,X0,X1)
| ~ shortest_path(X3,X4,X1)
| ~ sequential(X2,X0)
| ~ on_path(X2,X1)
| ~ on_path(X0,X1) ),
inference(resolution,[status(thm)],[f69,f84]) ).
fof(f558,plain,
! [X0,X1] :
( precedes(X1,X0,sK10_skl)
| ~ on_path(X1,sK10_skl)
| ~ sequential(X1,X0)
| ~ on_path(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f539,f120]) ).
fof(f607,plain,
on_path(sK8_skl,sK10_skl),
inference(resolution,[status(thm)],[f536,f121]) ).
fof(f608,plain,
! [X0,X1,X2,X3] :
( sequential(X1,X0)
| ~ path(X2,X3,sK10_skl)
| ~ precedes(X1,X0,sK10_skl)
| on_path(sK4_skl(X0,X1,sK10_skl),sK10_skl) ),
inference(resolution,[status(thm)],[f536,f78]) ).
fof(f609,definition,
! [X0,X1] :
( sQ33_spl
<=> ( sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| on_path(sK4_skl(X0,X1,sK10_skl),sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f610,plain,
! [X0,X1] :
( ~ sQ33_spl
| sequential(X0,X1)
| on_path(sK4_skl(X1,X0,sK10_skl),sK10_skl)
| ~ precedes(X0,X1,sK10_skl) ),
inference(component_clause,[status(thm)],[f609]) ).
fof(f612,plain,
( sQ8_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f608,f609,f182]) ).
fof(f613,plain,
! [X0,X1] :
( ~ sQ33_spl
| ~ precedes(X1,X0,sK10_skl)
| sequential(X1,X0)
| edge(sK4_skl(X0,X1,sK10_skl)) ),
inference(resolution,[status(thm)],[f610,f458]) ).
fof(f617,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ33_spl
| ~ vertex(tail_of(sK4_skl(X1,X0,sK10_skl)))
| tail_of(sK4_skl(X1,X0,sK10_skl)) = head_of(X1)
| sK4_skl(X1,X0,sK10_skl) = sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl)))
| sequential(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl))),sK4_skl(X1,X0,sK10_skl))
| ~ precedes(X0,X1,sK10_skl)
| ~ vertex(head_of(X1))
| tail_of(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl)))) = head_of(X1)
| sequential(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f464,f613]) ).
fof(f623,plain,
edge(sK8_skl),
inference(resolution,[status(thm)],[f607,f458]) ).
fof(f624,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f623,f198]) ).
fof(f625,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f624]) ).
fof(f626,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f267,f529]) ).
fof(f627,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f626]) ).
fof(f630,definition,
( sQ34_spl
<=> vertex(head_of(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( sQ34_spl
| ~ vertex(head_of(sK9_skl)) ),
inference(component_clause,[status(thm)],[f630]) ).
fof(f633,definition,
( sQ35_spl
<=> tail_of(sK8_skl) = head_of(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( ~ sQ35_spl
| head_of(sK9_skl) = tail_of(sK8_skl) ),
inference(component_clause,[status(thm)],[f633]) ).
fof(f636,definition,
( sQ36_spl
<=> sK0_skl(head_of(sK9_skl),tail_of(sK8_skl)) = sK8_skl ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f637,plain,
( ~ sQ36_spl
| sK0_skl(head_of(sK9_skl),tail_of(sK8_skl)) = sK8_skl ),
inference(component_clause,[status(thm)],[f636]) ).
fof(f652,definition,
( sQ41_spl
<=> sK9_skl = sK0_skl(head_of(sK9_skl),tail_of(sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f653,plain,
( ~ sQ41_spl
| sK0_skl(head_of(sK9_skl),tail_of(sK8_skl)) = sK9_skl ),
inference(component_clause,[status(thm)],[f652]) ).
fof(f659,plain,
! [X0,X1,X2] :
( ~ edge(sK1_skl(X2,X1,head_of(X0)))
| X0 = sK1_skl(X2,X1,head_of(X0))
| sequential(X0,sK1_skl(X2,X1,head_of(X0)))
| ~ edge(X0)
| ~ path(head_of(X0),X1,X2) ),
inference(resolution,[status(thm)],[f45,f66]) ).
fof(f662,plain,
! [X0,X1,X2] :
( sK1_skl(X1,X2,head_of(X0)) = X0
| ~ path(head_of(X0),X2,X1)
| ~ edge(X0)
| sequential(X0,sK1_skl(X1,X2,head_of(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f659,f44]) ).
fof(f704,plain,
! [X0,X1,X2] :
( ~ edge(X2)
| ~ sequential(X0,X1)
| triangle(X2,X0,X1)
| ~ sequential(X2,X0)
| ~ sequential(X1,X2)
| ~ edge(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f101,f62]) ).
fof(f730,plain,
! [X0,X1,X2,X3,X4] :
( ~ precedes(X0,X1,X4)
| ~ path(X2,X3,X4)
| sequential(X0,X1)
| edge(X0) ),
inference(resolution,[status(thm)],[f62,f77]) ).
fof(f731,plain,
! [X0,X1,X2] :
( triangle(X0,X1,X2)
| ~ sequential(X1,X2)
| ~ sequential(X2,X0)
| ~ sequential(X0,X1)
| ~ edge(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f704,f62]) ).
fof(f732,plain,
! [X0,X1,X2,X3,X4] :
( ~ precedes(X3,X4,X2)
| edge(X3)
| ~ path(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f730,f62]) ).
fof(f760,definition,
! [X0,X1,X2] :
( sQ42_spl
<=> ( sequential(X2,X1)
| ~ precedes(X2,X1,sK10_skl)
| ~ precedes(sK0_skl(X0,tail_of(sK4_skl(X1,X2,sK10_skl))),X1,sK10_skl)
| ~ sequential(sK0_skl(X0,tail_of(sK4_skl(X1,X2,sK10_skl))),X1)
| head_of(X1) != head_of(sK0_skl(X0,tail_of(sK4_skl(X1,X2,sK10_skl))))
| ~ vertex(tail_of(sK4_skl(X1,X2,sK10_skl)))
| sequential(X2,X1)
| X0 = tail_of(sK4_skl(X1,X2,sK10_skl))
| ~ precedes(X2,X1,sK10_skl)
| sK4_skl(X1,X2,sK10_skl) = sK0_skl(X0,tail_of(sK4_skl(X1,X2,sK10_skl)))
| ~ vertex(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f769,definition,
! [X0,X1,X2] :
( sQ43_spl
<=> ( sequential(X0,X1)
| ~ precedes(X0,X1,sK10_skl)
| ~ precedes(sK0_skl(tail_of(sK4_skl(X1,X0,sK10_skl)),X2),X1,sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK4_skl(X1,X0,sK10_skl)),X2),X1)
| ~ vertex(X2)
| X2 = tail_of(sK4_skl(X1,X0,sK10_skl))
| head_of(X1) != head_of(sK0_skl(tail_of(sK4_skl(X1,X0,sK10_skl)),X2))
| ~ vertex(tail_of(sK4_skl(X1,X0,sK10_skl)))
| sequential(X0,X1)
| sK0_skl(tail_of(sK4_skl(X1,X0,sK10_skl)),X2) = sK4_skl(X1,X0,sK10_skl)
| ~ precedes(X0,X1,sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f781,definition,
! [X0,X1,X2,X3,X4] :
( sQ44_spl
<=> ( sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ precedes(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),X0,sK10_skl)
| ~ sequential(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ in_path(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)
| sequential(X1,X0)
| ~ path(X3,X4,X2)
| head_of(X0) != head_of(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2))
| sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2) = sK4_skl(X0,X1,sK10_skl)
| ~ edge(sK3_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f788,plain,
! [X0,X1,X2,X3,X4] :
( ~ shortest_path(X3,X4,X2)
| edge(X0)
| ~ precedes(X0,X1,X2) ),
inference(resolution,[status(thm)],[f732,f84]) ).
fof(f789,plain,
! [X0,X1] :
( edge(X0)
| ~ precedes(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f788,f120]) ).
fof(f794,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ2_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ33_spl
| sequential(X0,X1)
| ~ path(X4,X5,sK10_skl)
| ~ precedes(X0,X1,sK10_skl)
| ~ precedes(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl))),X1,sK10_skl)
| ~ sequential(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl))),X1)
| ~ path(X2,X3,sK10_skl)
| ~ vertex(tail_of(sK4_skl(X1,X0,sK10_skl)))
| tail_of(sK4_skl(X1,X0,sK10_skl)) = head_of(X1)
| sK4_skl(X1,X0,sK10_skl) = sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl)))
| ~ precedes(X0,X1,sK10_skl)
| ~ vertex(head_of(X1))
| tail_of(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl)))) = head_of(X1)
| sequential(X0,X1) ),
inference(resolution,[status(thm)],[f617,f233]) ).
fof(f796,definition,
! [X0,X1] :
( sQ45_spl
<=> ( sequential(X0,X1)
| ~ precedes(X0,X1,sK10_skl)
| ~ precedes(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl))),X1,sK10_skl)
| ~ sequential(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl))),X1)
| ~ vertex(tail_of(sK4_skl(X1,X0,sK10_skl)))
| tail_of(sK4_skl(X1,X0,sK10_skl)) = head_of(X1)
| sK4_skl(X1,X0,sK10_skl) = sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl)))
| ~ precedes(X0,X1,sK10_skl)
| ~ vertex(head_of(X1))
| tail_of(sK0_skl(head_of(X1),tail_of(sK4_skl(X1,X0,sK10_skl)))) = head_of(X1)
| sequential(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f799,plain,
( ~ sQ2_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ33_spl
| sQ8_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f794,f796,f182,f609,f137,f145,f179,f141]) ).
fof(f809,plain,
! [X0,X1,X2,X3] :
( ~ edge(sK3_skl(tail_of(X0),X1))
| ~ in_path(tail_of(X0),X1)
| X0 = sK3_skl(tail_of(X0),X1)
| ~ precedes(X0,sK3_skl(tail_of(X0),X1),sK10_skl)
| ~ path(X2,X3,X1)
| sequential(sK3_skl(tail_of(X0),X1),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f207,f789]) ).
fof(f817,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ2_spl
| ~ precedes(X1,X0,sK10_skl)
| sequential(sK0_skl(tail_of(X1),head_of(X0)),X1)
| X1 = sK0_skl(tail_of(X1),head_of(X0))
| X0 = sK0_skl(tail_of(X1),head_of(X0))
| ~ vertex(tail_of(X1))
| head_of(X0) = tail_of(X1)
| sequential(X0,sK0_skl(tail_of(X1),head_of(X0)))
| ~ edge(X0)
| ~ vertex(head_of(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f428,f789]) ).
fof(f822,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ vertex(head_of(X0))
| ~ precedes(X1,X0,sK10_skl)
| tail_of(X1) = head_of(X0)
| ~ vertex(tail_of(X1))
| sequential(sK0_skl(head_of(X0),tail_of(X1)),X1)
| sK0_skl(head_of(X0),tail_of(X1)) = X1 ),
inference(backward_subsumption_resolution,[status(thm)],[f324,f789]) ).
fof(f823,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| X1 = sK0_skl(X0,tail_of(X1))
| X0 = tail_of(X1)
| ~ vertex(tail_of(X1))
| ~ precedes(X1,sK0_skl(X0,tail_of(X1)),sK10_skl)
| ~ vertex(X0)
| sequential(sK0_skl(X0,tail_of(X1)),X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f314,f789]) ).
fof(f826,plain,
! [X0,X1,X2,X3] :
( sequential(X1,X0)
| ~ path(X2,X3,sK10_skl)
| ~ precedes(X1,X0,sK10_skl)
| edge(sK4_skl(X0,X1,sK10_skl)) ),
inference(resolution,[status(thm)],[f789,f78]) ).
fof(f827,definition,
! [X0,X1] :
( sQ46_spl
<=> ( sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| edge(sK4_skl(X0,X1,sK10_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f830,plain,
( sQ8_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f826,f827,f182]) ).
fof(f839,plain,
! [X0] :
( ~ sQ19_spl
| ~ sequential(X0,sK8_skl)
| ~ sequential(sK9_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f269,f62]) ).
fof(f840,plain,
! [X0,X1] :
( ~ sQ19_spl
| sK1_skl(X0,X1,head_of(sK9_skl)) = sK9_skl
| ~ path(head_of(sK9_skl),X1,X0)
| ~ edge(sK9_skl)
| ~ sequential(sK1_skl(X0,X1,head_of(sK9_skl)),sK8_skl) ),
inference(resolution,[status(thm)],[f839,f662]) ).
fof(f846,definition,
! [X0] :
( sQ47_spl
<=> ( ~ precedes(X0,sK9_skl,sK10_skl)
| tail_of(sK4_skl(sK9_skl,X0,sK10_skl)) = head_of(sK9_skl)
| sK0_skl(head_of(sK9_skl),tail_of(sK4_skl(sK9_skl,X0,sK10_skl))) = sK9_skl
| sequential(X0,sK9_skl)
| ~ vertex(tail_of(sK4_skl(sK9_skl,X0,sK10_skl)))
| ~ sequential(sK0_skl(head_of(sK9_skl),tail_of(sK4_skl(sK9_skl,X0,sK10_skl))),sK8_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f850,definition,
! [X0] :
( sQ48_spl
<=> ( ~ precedes(X0,sK9_skl,sK10_skl)
| sK0_skl(head_of(sK9_skl),tail_of(X0)) = sK9_skl
| ~ vertex(tail_of(X0))
| head_of(sK9_skl) = tail_of(X0)
| ~ sequential(sK0_skl(head_of(sK9_skl),tail_of(X0)),sK8_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f851,plain,
! [X0] :
( ~ sQ48_spl
| head_of(sK9_skl) = tail_of(X0)
| ~ precedes(X0,sK9_skl,sK10_skl)
| sK0_skl(head_of(sK9_skl),tail_of(X0)) = sK9_skl
| ~ vertex(tail_of(X0))
| ~ sequential(sK0_skl(head_of(sK9_skl),tail_of(X0)),sK8_skl) ),
inference(component_clause,[status(thm)],[f850]) ).
fof(f854,definition,
! [X0] :
( sQ49_spl
<=> ( head_of(sK9_skl) = X0
| tail_of(sK0_skl(X0,head_of(sK9_skl))) = X0
| ~ vertex(X0)
| sK9_skl = sK0_skl(X0,head_of(sK9_skl))
| ~ sequential(sK0_skl(X0,head_of(sK9_skl)),sK8_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f858,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ50_spl
<=> ( sequential(X0,sK9_skl)
| ~ path(X4,X5,X1)
| head_of(sK9_skl) = tail_of(sK4_skl(sK9_skl,X0,X1))
| ~ precedes(X0,sK9_skl,X1)
| sK9_skl = sK0_skl(head_of(sK9_skl),tail_of(sK4_skl(sK9_skl,X0,X1)))
| ~ vertex(tail_of(sK4_skl(sK9_skl,X0,X1)))
| ~ shortest_path(X2,X3,X1)
| ~ sequential(sK0_skl(head_of(sK9_skl),tail_of(sK4_skl(sK9_skl,X0,X1))),sK8_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f862,definition,
! [X0,X1] :
( sQ51_spl
<=> ( sK1_skl(X0,X1,head_of(sK9_skl)) = sK9_skl
| ~ path(head_of(sK9_skl),X1,X0)
| ~ sequential(sK1_skl(X0,X1,head_of(sK9_skl)),sK8_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f865,plain,
( ~ sQ19_spl
| ~ sQ18_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f840,f862,f265,f268]) ).
fof(f896,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| tail_of(X0) = X2
| ~ vertex(X2)
| ~ sequential(sK0_skl(tail_of(X0),X2),X1)
| ~ on_path(sK0_skl(tail_of(X0),X2),sK10_skl)
| ~ on_path(X1,sK10_skl)
| head_of(sK0_skl(tail_of(X0),X2)) = tail_of(X0)
| ~ vertex(tail_of(X0))
| head_of(X0) != head_of(X1) ),
inference(resolution,[status(thm)],[f558,f378]) ).
fof(f897,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| X0 = tail_of(X1)
| ~ vertex(X0)
| ~ sequential(sK0_skl(X0,tail_of(X1)),X2)
| ~ vertex(tail_of(X1))
| ~ on_path(X2,sK10_skl)
| ~ on_path(sK0_skl(X0,tail_of(X1)),sK10_skl)
| head_of(X2) != head_of(X1)
| X0 = tail_of(sK0_skl(X0,tail_of(X1))) ),
inference(resolution,[status(thm)],[f558,f393]) ).
fof(f899,plain,
( sQ12_spl
| ~ on_path(sK9_skl,sK10_skl)
| ~ sequential(sK9_skl,sK8_skl)
| ~ on_path(sK8_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f558,f221]) ).
fof(f905,plain,
! [X0] :
( ~ sQ14_spl
| ~ sequential(X0,sK9_skl)
| ~ sequential(X0,sK8_skl)
| ~ on_path(X0,sK10_skl)
| ~ sequential(X0,sK9_skl)
| ~ on_path(sK9_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f558,f235]) ).
fof(f907,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ shortest_path(X4,X5,sK10_skl)
| ~ path(X2,X3,sK10_skl)
| ~ precedes(X1,X0,sK10_skl)
| sequential(X1,X0)
| ~ on_path(X0,sK10_skl)
| ~ sequential(X0,sK4_skl(X0,X1,sK10_skl))
| ~ on_path(sK4_skl(X0,X1,sK10_skl),sK10_skl) ),
inference(resolution,[status(thm)],[f558,f218]) ).
fof(f912,plain,
! [X0,X1] :
( ~ precedes(X0,X1,sK10_skl)
| ~ on_path(X1,sK10_skl)
| ~ sequential(X1,X0)
| ~ on_path(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f558,f216]) ).
fof(f915,plain,
! [X0,X1,X2,X3,X4] :
( ~ sequential(X2,X1)
| ~ path(X3,X4,sK10_skl)
| ~ sequential(X2,X0)
| ~ precedes(X2,X0,sK10_skl)
| ~ on_path(X1,sK10_skl)
| ~ sequential(X1,X0)
| ~ on_path(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f558,f79]) ).
fof(f916,plain,
! [X0,X1,X2,X3] :
( ~ shortest_path(X2,X3,sK10_skl)
| ~ precedes(X0,X1,sK10_skl)
| ~ on_path(X1,sK10_skl)
| ~ sequential(X1,X0)
| ~ on_path(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f558,f92]) ).
fof(f917,plain,
! [X0,X1,X2,X3,X4] :
( head_of(X2) != head_of(X0)
| ~ shortest_path(X3,X4,sK10_skl)
| tail_of(X1) != tail_of(X2)
| ~ on_path(X1,sK10_skl)
| ~ sequential(X1,X0)
| ~ on_path(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f558,f91]) ).
fof(f918,plain,
! [X0,X1] :
( ~ on_path(X0,sK10_skl)
| ~ precedes(X1,X0,sK10_skl)
| ~ sequential(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f912,f536]) ).
fof(f920,definition,
! [X0,X1] :
( sQ52_spl
<=> ( ~ precedes(X0,X1,sK10_skl)
| ~ on_path(X1,sK10_skl)
| ~ sequential(X1,X0)
| ~ on_path(X0,sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f923,plain,
( sQ6_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f916,f920,f168]) ).
fof(f925,definition,
! [X0,X1] :
( sQ53_spl
<=> ( ~ precedes(X1,X0,sK10_skl)
| sequential(X1,X0)
| ~ on_path(X0,sK10_skl)
| ~ sequential(X0,sK4_skl(X0,X1,sK10_skl))
| ~ on_path(sK4_skl(X0,X1,sK10_skl),sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f928,plain,
( sQ6_spl
| sQ8_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f907,f925,f182,f168]) ).
fof(f929,definition,
( sQ54_spl
<=> on_path(sK8_skl,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f931,plain,
( sQ54_spl
| ~ on_path(sK8_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f929]) ).
fof(f932,definition,
( sQ55_spl
<=> sequential(sK9_skl,sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f935,definition,
( sQ56_spl
<=> on_path(sK9_skl,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f937,plain,
( sQ56_spl
| ~ on_path(sK9_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f935]) ).
fof(f938,plain,
( sQ12_spl
| ~ sQ56_spl
| ~ sQ55_spl
| ~ sQ54_spl ),
inference(split_clause,[status(thm)],[f899,f929,f932,f935,f219]) ).
fof(f939,definition,
! [X0] :
( sQ57_spl
<=> ( ~ sequential(X0,sK9_skl)
| ~ sequential(X0,sK8_skl)
| ~ on_path(X0,sK10_skl)
| ~ sequential(X0,sK9_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f940,plain,
! [X0] :
( ~ sQ57_spl
| ~ sequential(X0,sK9_skl)
| ~ sequential(X0,sK8_skl)
| ~ on_path(X0,sK10_skl)
| ~ sequential(X0,sK9_skl) ),
inference(component_clause,[status(thm)],[f939]) ).
fof(f942,plain,
( ~ sQ14_spl
| sQ57_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f905,f935,f939,f234]) ).
fof(f943,definition,
! [X0,X1,X2] :
( sQ58_spl
<=> ( ~ sequential(X2,X1)
| ~ sequential(X2,X0)
| ~ precedes(X2,X0,sK10_skl)
| ~ on_path(X1,sK10_skl)
| ~ sequential(X1,X0)
| ~ on_path(X0,sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f946,plain,
( sQ8_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f915,f943,f182]) ).
fof(f947,definition,
! [X0,X1,X2] :
( sQ59_spl
<=> ( head_of(X2) != head_of(X0)
| tail_of(X1) != tail_of(X2)
| ~ on_path(X1,sK10_skl)
| ~ sequential(X1,X0)
| ~ on_path(X0,sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f950,plain,
( sQ6_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f917,f947,f168]) ).
fof(f951,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f937,f511]) ).
fof(f952,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f951]) ).
fof(f954,plain,
( sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f931,f607]) ).
fof(f955,plain,
sQ54_spl,
inference(contradiction_clause,[status(thm)],[f954]) ).
fof(f957,plain,
! [X0] :
( ~ sQ57_spl
| ~ on_path(X0,sK10_skl)
| ~ sequential(X0,sK8_skl)
| ~ sequential(X0,sK9_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f940]) ).
fof(f959,plain,
! [X0,X1,X2] :
( triangle(X0,X1,X2)
| ~ sequential(X2,X0)
| ~ sequential(X1,X2)
| ~ sequential(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f731,f62]) ).
fof(f960,plain,
! [X0] :
( ~ sequential(X0,sK8_skl)
| ~ sequential(sK9_skl,X0)
| ~ sequential(sK8_skl,sK9_skl) ),
inference(resolution,[status(thm)],[f959,f123]) ).
fof(f967,definition,
! [X0] :
( sQ60_spl
<=> ( ~ sequential(X0,sK8_skl)
| ~ sequential(sK9_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f970,plain,
( sQ60_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f960,f250,f967]) ).
fof(f977,plain,
! [X0,X1,X2,X3] :
( ~ on_path(X0,sK10_skl)
| ~ sequential(X0,sK3_skl(tail_of(X0),X1))
| ~ on_path(sK3_skl(tail_of(X0),X1),sK10_skl)
| ~ edge(sK3_skl(tail_of(X0),X1))
| ~ in_path(tail_of(X0),X1)
| X0 = sK3_skl(tail_of(X0),X1)
| ~ path(X2,X3,X1)
| sequential(sK3_skl(tail_of(X0),X1),X0) ),
inference(resolution,[status(thm)],[f809,f558]) ).
fof(f978,plain,
! [X0,X1,X2,X3] :
( ~ on_path(X0,sK10_skl)
| ~ path(X2,X3,X1)
| sK3_skl(tail_of(X0),X1) = X0
| ~ sequential(X0,sK3_skl(tail_of(X0),X1))
| sequential(sK3_skl(tail_of(X0),X1),X0)
| ~ in_path(tail_of(X0),X1)
| ~ on_path(sK3_skl(tail_of(X0),X1),sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f977,f458]) ).
fof(f989,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| X0 = sK0_skl(tail_of(X0),tail_of(X1))
| ~ edge(X0)
| tail_of(X1) = head_of(sK0_skl(tail_of(X0),tail_of(X1)))
| ~ vertex(tail_of(X1))
| ~ vertex(tail_of(X0))
| tail_of(X0) = tail_of(X1)
| tail_of(X0) = tail_of(X1)
| ~ vertex(tail_of(X0))
| ~ vertex(tail_of(X1))
| ~ on_path(X0,sK10_skl)
| ~ on_path(sK0_skl(tail_of(X0),tail_of(X1)),sK10_skl)
| head_of(X0) != head_of(X1)
| tail_of(X0) = tail_of(sK0_skl(tail_of(X0),tail_of(X1))) ),
inference(resolution,[status(thm)],[f897,f301]) ).
fof(f1010,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| X0 = sK0_skl(tail_of(X0),tail_of(X1))
| ~ edge(X0)
| tail_of(X1) = head_of(sK0_skl(tail_of(X0),tail_of(X1)))
| tail_of(X0) = tail_of(X1)
| ~ vertex(tail_of(X0))
| ~ vertex(tail_of(X1))
| ~ on_path(X0,sK10_skl)
| ~ on_path(sK0_skl(tail_of(X0),tail_of(X1)),sK10_skl)
| head_of(X0) != head_of(X1)
| tail_of(X0) = tail_of(sK0_skl(tail_of(X0),tail_of(X1))) ),
inference(duplicate_literals_removal,[status(thm)],[f989]) ).
fof(f1011,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| tail_of(X1) = tail_of(sK0_skl(tail_of(X1),tail_of(X0)))
| head_of(X1) != head_of(X0)
| X1 = sK0_skl(tail_of(X1),tail_of(X0))
| head_of(sK0_skl(tail_of(X1),tail_of(X0))) = tail_of(X0)
| ~ vertex(tail_of(X0))
| ~ on_path(sK0_skl(tail_of(X1),tail_of(X0)),sK10_skl)
| ~ vertex(tail_of(X1))
| ~ on_path(X1,sK10_skl)
| tail_of(X0) = tail_of(X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1010,f458]) ).
fof(f1028,plain,
! [X0,X1,X2,X3,X4] :
( ~ path(X3,X4,sK10_skl)
| ~ in_path(tail_of(X0),sK10_skl)
| ~ on_path(X0,sK10_skl)
| ~ path(X1,X2,sK10_skl)
| sK3_skl(tail_of(X0),sK10_skl) = X0
| ~ sequential(X0,sK3_skl(tail_of(X0),sK10_skl))
| sequential(sK3_skl(tail_of(X0),sK10_skl),X0)
| ~ in_path(tail_of(X0),sK10_skl) ),
inference(resolution,[status(thm)],[f978,f58]) ).
fof(f1029,definition,
! [X0] :
( sQ61_spl
<=> ( ~ in_path(tail_of(X0),sK10_skl)
| ~ on_path(X0,sK10_skl)
| sK3_skl(tail_of(X0),sK10_skl) = X0
| ~ sequential(X0,sK3_skl(tail_of(X0),sK10_skl))
| sequential(sK3_skl(tail_of(X0),sK10_skl),X0)
| ~ in_path(tail_of(X0),sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1032,plain,
( sQ8_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1028,f1029,f182]) ).
fof(f1040,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ vertex(tail_of(X1))
| ~ precedes(X1,sK0_skl(X0,tail_of(X1)),sK10_skl)
| sK0_skl(X0,tail_of(X1)) = X1
| X0 = tail_of(X1)
| ~ vertex(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f823,f1042]) ).
fof(f1042,plain,
! [X0,X1] :
( ~ precedes(X1,X0,sK10_skl)
| ~ sequential(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f918,f510]) ).
fof(f1044,plain,
! [X0,X1,X2,X3] :
( sequential(X1,X0)
| ~ path(X2,X3,sK10_skl)
| ~ precedes(X1,X0,sK10_skl)
| ~ sequential(X0,sK4_skl(X0,X1,sK10_skl)) ),
inference(resolution,[status(thm)],[f1042,f78]) ).
fof(f1046,definition,
! [X0,X1] :
( sQ62_spl
<=> ( sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ sequential(X0,sK4_skl(X0,X1,sK10_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f1049,plain,
( sQ8_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f1044,f1046,f182]) ).
fof(f1074,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ edge(X0)
| sK0_skl(tail_of(X0),X2) = X0
| sequential(sK0_skl(tail_of(X0),X2),X0)
| ~ edge(sK0_skl(tail_of(X0),X2))
| tail_of(X0) = X2
| ~ vertex(X2)
| ~ sequential(sK0_skl(tail_of(X0),X2),X1)
| ~ on_path(sK0_skl(tail_of(X0),X2),sK10_skl)
| ~ on_path(X1,sK10_skl)
| ~ vertex(tail_of(X0))
| head_of(X0) != head_of(X1) ),
inference(resolution,[status(thm)],[f896,f66]) ).
fof(f1075,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ on_path(X2,sK10_skl)
| ~ vertex(X1)
| X1 = tail_of(X0)
| sequential(sK0_skl(tail_of(X0),X1),X0)
| ~ vertex(tail_of(X0))
| ~ edge(X0)
| X0 = sK0_skl(tail_of(X0),X1)
| ~ sequential(sK0_skl(tail_of(X0),X1),X2)
| head_of(X2) != head_of(X0)
| ~ on_path(sK0_skl(tail_of(X0),X1),sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1074,f62]) ).
fof(f1177,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| head_of(sK0_skl(tail_of(sK8_skl),tail_of(X0))) != head_of(sK9_skl)
| head_of(sK8_skl) != head_of(X0)
| sK8_skl = sK0_skl(tail_of(sK8_skl),tail_of(X0))
| head_of(sK0_skl(tail_of(sK8_skl),tail_of(X0))) = tail_of(X0)
| ~ vertex(tail_of(X0))
| ~ on_path(sK0_skl(tail_of(sK8_skl),tail_of(X0)),sK10_skl)
| ~ vertex(tail_of(sK8_skl))
| ~ on_path(sK8_skl,sK10_skl)
| tail_of(X0) = tail_of(sK8_skl) ),
inference(resolution,[status(thm)],[f1011,f166]) ).
fof(f1182,definition,
! [X0] :
( sQ63_spl
<=> ( head_of(sK0_skl(tail_of(sK8_skl),tail_of(X0))) != head_of(sK9_skl)
| head_of(sK8_skl) != head_of(X0)
| sK8_skl = sK0_skl(tail_of(sK8_skl),tail_of(X0))
| head_of(sK0_skl(tail_of(sK8_skl),tail_of(X0))) = tail_of(X0)
| ~ vertex(tail_of(X0))
| ~ on_path(sK0_skl(tail_of(sK8_skl),tail_of(X0)),sK10_skl)
| tail_of(X0) = tail_of(sK8_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1185,plain,
( ~ sQ5_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| ~ sQ21_spl
| ~ sQ54_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1177,f1182,f929,f291,f145,f137,f141,f165]) ).
fof(f1219,plain,
! [X0,X1,X2,X3,X4] :
( edge(sK4_skl(X1,X0,X2))
| ~ path(X3,X4,X2)
| sequential(X0,X1)
| ~ precedes(X0,X1,X2) ),
inference(resolution,[status(thm)],[f63,f77]) ).
fof(f1225,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ2_spl
| ~ sQ1_spl
| sequential(X1,X0)
| ~ vertex(tail_of(sK4_skl(X0,X1,X2)))
| sK0_skl(tail_of(sK4_skl(X0,X1,X2)),X3) = sK4_skl(X0,X1,X2)
| head_of(sK0_skl(tail_of(sK4_skl(X0,X1,X2)),X3)) != head_of(X0)
| ~ precedes(X1,X0,X2)
| ~ path(X6,X7,X2)
| sequential(sK0_skl(tail_of(sK4_skl(X0,X1,X2)),X3),sK4_skl(X0,X1,X2))
| ~ shortest_path(X4,X5,X2)
| ~ vertex(X3)
| tail_of(sK4_skl(X0,X1,X2)) = X3 ),
inference(backward_subsumption_resolution,[status(thm)],[f451,f1219]) ).
fof(f1228,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ sQ3_spl
| ~ sQ1_spl
| head_of(X0) != head_of(sK0_skl(X3,tail_of(sK4_skl(X0,X1,X2))))
| sequential(X1,X0)
| ~ precedes(X1,X0,X2)
| ~ shortest_path(X6,X7,X2)
| ~ vertex(tail_of(sK4_skl(X0,X1,X2)))
| sK4_skl(X0,X1,X2) = sK0_skl(X3,tail_of(sK4_skl(X0,X1,X2)))
| ~ vertex(X3)
| ~ path(X4,X5,X2)
| sequential(sK0_skl(X3,tail_of(sK4_skl(X0,X1,X2))),sK4_skl(X0,X1,X2))
| tail_of(sK4_skl(X0,X1,X2)) = X3 ),
inference(backward_subsumption_resolution,[status(thm)],[f347,f1219]) ).
fof(f1229,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( head_of(X5) != head_of(sK3_skl(tail_of(sK4_skl(X5,X6,X2)),X7))
| ~ path(X8,X9,X7)
| ~ in_path(tail_of(sK4_skl(X5,X6,X2)),X7)
| sK3_skl(tail_of(sK4_skl(X5,X6,X2)),X7) = sK4_skl(X5,X6,X2)
| sequential(sK3_skl(tail_of(sK4_skl(X5,X6,X2)),X7),sK4_skl(X5,X6,X2))
| sequential(X6,X5)
| ~ precedes(X6,X5,X2)
| ~ edge(sK3_skl(tail_of(sK4_skl(X5,X6,X2)),X7))
| ~ shortest_path(X3,X4,X2)
| ~ path(X0,X1,X2) ),
inference(backward_subsumption_resolution,[status(thm)],[f345,f1219]) ).
fof(f1261,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ57_spl
| ~ vertex(head_of(X0))
| ~ precedes(sK8_skl,X0,sK10_skl)
| tail_of(sK8_skl) = head_of(X0)
| ~ vertex(tail_of(sK8_skl))
| sK0_skl(head_of(X0),tail_of(sK8_skl)) = sK8_skl
| ~ on_path(sK0_skl(head_of(X0),tail_of(sK8_skl)),sK10_skl)
| ~ sequential(sK0_skl(head_of(X0),tail_of(sK8_skl)),sK9_skl) ),
inference(resolution,[status(thm)],[f957,f822]) ).
fof(f1262,plain,
! [X0] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ2_spl
| ~ sQ57_spl
| ~ precedes(sK8_skl,X0,sK10_skl)
| sK8_skl = sK0_skl(tail_of(sK8_skl),head_of(X0))
| X0 = sK0_skl(tail_of(sK8_skl),head_of(X0))
| ~ vertex(tail_of(sK8_skl))
| head_of(X0) = tail_of(sK8_skl)
| sequential(X0,sK0_skl(tail_of(sK8_skl),head_of(X0)))
| ~ edge(X0)
| ~ vertex(head_of(X0))
| ~ on_path(sK0_skl(tail_of(sK8_skl),head_of(X0)),sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),head_of(X0)),sK9_skl) ),
inference(resolution,[status(thm)],[f957,f817]) ).
fof(f1268,plain,
! [X0,X1,X2] :
( ~ sQ57_spl
| ~ path(X1,X2,sK10_skl)
| ~ in_path(X0,sK10_skl)
| ~ sequential(sK3_skl(X0,sK10_skl),sK8_skl)
| ~ sequential(sK3_skl(X0,sK10_skl),sK9_skl) ),
inference(resolution,[status(thm)],[f957,f58]) ).
fof(f1285,definition,
! [X0] :
( sQ69_spl
<=> ( ~ precedes(sK8_skl,X0,sK10_skl)
| sK8_skl = sK0_skl(tail_of(sK8_skl),head_of(X0))
| X0 = sK0_skl(tail_of(sK8_skl),head_of(X0))
| head_of(X0) = tail_of(sK8_skl)
| sequential(X0,sK0_skl(tail_of(sK8_skl),head_of(X0)))
| ~ edge(X0)
| ~ vertex(head_of(X0))
| ~ on_path(sK0_skl(tail_of(sK8_skl),head_of(X0)),sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),head_of(X0)),sK9_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1288,plain,
( ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ2_spl
| ~ sQ57_spl
| ~ sQ21_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f1262,f1285,f291,f939,f141,f137,f145]) ).
fof(f1289,definition,
! [X0] :
( sQ70_spl
<=> ( sK8_skl = sK0_skl(tail_of(sK8_skl),X0)
| X0 = head_of(sK0_skl(tail_of(sK8_skl),X0))
| ~ vertex(X0)
| tail_of(sK8_skl) = X0
| ~ on_path(sK0_skl(tail_of(sK8_skl),X0),sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),X0),sK9_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1293,definition,
! [X0] :
( sQ71_spl
<=> ( ~ in_path(X0,sK10_skl)
| ~ sequential(sK3_skl(X0,sK10_skl),sK8_skl)
| ~ sequential(sK3_skl(X0,sK10_skl),sK9_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1296,plain,
( ~ sQ57_spl
| sQ8_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f1268,f1293,f182,f939]) ).
fof(f1298,definition,
! [X0] :
( sQ72_spl
<=> ( ~ vertex(head_of(X0))
| ~ precedes(sK8_skl,X0,sK10_skl)
| tail_of(sK8_skl) = head_of(X0)
| sK0_skl(head_of(X0),tail_of(sK8_skl)) = sK8_skl
| ~ on_path(sK0_skl(head_of(X0),tail_of(sK8_skl)),sK10_skl)
| ~ sequential(sK0_skl(head_of(X0),tail_of(sK8_skl)),sK9_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1301,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ57_spl
| ~ sQ21_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f1261,f1298,f291,f939,f137,f145,f141]) ).
fof(f1312,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ23_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ precedes(X1,X0,sK10_skl)
| ~ precedes(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),X0,sK10_skl)
| sequential(X1,X0)
| ~ sequential(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2),X0)
| sequential(X1,X0)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2) = sK4_skl(X0,X1,sK10_skl)
| head_of(sK0_skl(tail_of(sK4_skl(X0,X1,sK10_skl)),X2)) != head_of(X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ path(X5,X6,sK10_skl)
| ~ shortest_path(X3,X4,sK10_skl)
| ~ vertex(X2)
| tail_of(sK4_skl(X0,X1,sK10_skl)) = X2 ),
inference(resolution,[status(thm)],[f1225,f328]) ).
fof(f1320,plain,
( ~ sQ23_spl
| ~ sQ2_spl
| ~ sQ1_spl
| sQ8_spl
| sQ6_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f1312,f769,f168,f182,f137,f141,f327]) ).
fof(f1389,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ sQ23_spl
| ~ precedes(X5,X4,sK10_skl)
| ~ precedes(sK3_skl(tail_of(sK4_skl(X4,X5,sK10_skl)),X6),X4,sK10_skl)
| sequential(X5,X4)
| ~ sequential(sK3_skl(tail_of(sK4_skl(X4,X5,sK10_skl)),X6),X4)
| head_of(X4) != head_of(sK3_skl(tail_of(sK4_skl(X4,X5,sK10_skl)),X6))
| ~ path(X7,X8,X6)
| ~ in_path(tail_of(sK4_skl(X4,X5,sK10_skl)),X6)
| sK3_skl(tail_of(sK4_skl(X4,X5,sK10_skl)),X6) = sK4_skl(X4,X5,sK10_skl)
| sequential(X5,X4)
| ~ precedes(X5,X4,sK10_skl)
| ~ edge(sK3_skl(tail_of(sK4_skl(X4,X5,sK10_skl)),X6))
| ~ shortest_path(X2,X3,sK10_skl)
| ~ path(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f1229,f328]) ).
fof(f1401,plain,
( ~ sQ23_spl
| sQ44_spl
| sQ6_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1389,f182,f168,f781,f327]) ).
fof(f1408,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ2_spl
| ~ edge(X1)
| ~ precedes(X0,X1,sK10_skl)
| tail_of(X0) = head_of(X1)
| sequential(sK0_skl(tail_of(X0),head_of(X1)),X0)
| X0 = sK0_skl(tail_of(X0),head_of(X1))
| ~ vertex(tail_of(X0))
| sequential(X1,sK0_skl(tail_of(X0),head_of(X1)))
| sK0_skl(tail_of(X0),head_of(X1)) = X1 ),
inference(backward_subsumption_resolution,[status(thm)],[f817,f23]) ).
fof(f1410,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))))
| ~ edge(X0)
| tail_of(sK4_skl(X0,X1,X2)) = head_of(X0)
| ~ precedes(X1,X0,X2)
| ~ vertex(tail_of(sK4_skl(X0,X1,X2)))
| sequential(X1,X0)
| ~ shortest_path(X5,X6,X2)
| ~ path(X3,X4,X2)
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,X2))) = X0 ),
inference(backward_subsumption_resolution,[status(thm)],[f479,f23]) ).
fof(f1411,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ3_spl
| head_of(X0) = tail_of(sK4_skl(X0,X1,sK10_skl))
| sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| ~ edge(X0)
| sequential(X0,sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))))
| sK0_skl(head_of(X0),tail_of(sK4_skl(X0,X1,sK10_skl))) = X0 ),
inference(backward_subsumption_resolution,[status(thm)],[f474,f23]) ).
fof(f1412,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ vertex(tail_of(X1))
| head_of(X0) = tail_of(X1)
| ~ edge(X0)
| ~ precedes(X1,X0,sK10_skl)
| sequential(X0,sK0_skl(head_of(X0),tail_of(X1)))
| sK0_skl(head_of(X0),tail_of(X1)) = X0 ),
inference(backward_subsumption_resolution,[status(thm)],[f435,f23]) ).
fof(f1414,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| sequential(X1,sK0_skl(X0,head_of(X1)))
| X0 = tail_of(sK0_skl(X0,head_of(X1)))
| ~ vertex(X0)
| sK0_skl(X0,head_of(X1)) = X1
| ~ edge(X1)
| X0 = head_of(X1) ),
inference(backward_subsumption_resolution,[status(thm)],[f396,f23]) ).
fof(f1416,plain,
( sQ34_spl
| ~ edge(sK9_skl) ),
inference(resolution,[status(thm)],[f23,f632]) ).
fof(f1417,plain,
( sQ34_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1416,f265,f630]) ).
fof(f1420,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sequential(sK0_skl(X0,head_of(sK9_skl)),sK8_skl)
| X0 = tail_of(sK0_skl(X0,head_of(sK9_skl)))
| ~ vertex(X0)
| sK0_skl(X0,head_of(sK9_skl)) = sK9_skl
| ~ edge(sK9_skl)
| X0 = head_of(sK9_skl) ),
inference(resolution,[status(thm)],[f1414,f839]) ).
fof(f1427,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ1_spl
| sK0_skl(X0,head_of(X1)) = X1
| edge(sK0_skl(X0,head_of(X1)))
| head_of(X1) = X0
| X0 = tail_of(sK0_skl(X0,head_of(X1)))
| ~ edge(X1)
| ~ vertex(X0) ),
inference(resolution,[status(thm)],[f1414,f63]) ).
fof(f1435,plain,
( ~ sQ19_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ18_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1420,f854,f265,f137,f145,f268]) ).
fof(f1440,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ1_spl
| head_of(sK0_skl(tail_of(sK8_skl),head_of(X0))) != head_of(sK9_skl)
| sK0_skl(tail_of(sK8_skl),head_of(X0)) = X0
| edge(sK0_skl(tail_of(sK8_skl),head_of(X0)))
| head_of(X0) = tail_of(sK8_skl)
| ~ edge(X0)
| ~ vertex(tail_of(sK8_skl)) ),
inference(resolution,[status(thm)],[f1427,f166]) ).
fof(f1443,definition,
! [X0] :
( sQ74_spl
<=> ( head_of(sK0_skl(tail_of(sK8_skl),head_of(X0))) != head_of(sK9_skl)
| sK0_skl(tail_of(sK8_skl),head_of(X0)) = X0
| edge(sK0_skl(tail_of(sK8_skl),head_of(X0)))
| head_of(X0) = tail_of(sK8_skl)
| ~ edge(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1446,plain,
( ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sQ74_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f1440,f291,f1443,f137,f145,f165]) ).
fof(f1494,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sequential(sK0_skl(head_of(sK9_skl),tail_of(X0)),sK8_skl)
| ~ vertex(tail_of(X0))
| head_of(sK9_skl) = tail_of(X0)
| ~ edge(sK9_skl)
| ~ precedes(X0,sK9_skl,sK10_skl)
| sK0_skl(head_of(sK9_skl),tail_of(X0)) = sK9_skl ),
inference(resolution,[status(thm)],[f1412,f839]) ).
fof(f1504,plain,
( ~ sQ19_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ18_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1494,f850,f265,f137,f141,f145,f268]) ).
fof(f1513,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ48_spl
| ~ vertex(head_of(sK9_skl))
| ~ precedes(sK8_skl,sK9_skl,sK10_skl)
| tail_of(sK8_skl) = head_of(sK9_skl)
| ~ vertex(tail_of(sK8_skl))
| sK0_skl(head_of(sK9_skl),tail_of(sK8_skl)) = sK8_skl
| head_of(sK9_skl) = tail_of(sK8_skl)
| ~ precedes(sK8_skl,sK9_skl,sK10_skl)
| sK0_skl(head_of(sK9_skl),tail_of(sK8_skl)) = sK9_skl
| ~ vertex(tail_of(sK8_skl)) ),
inference(resolution,[status(thm)],[f851,f822]) ).
fof(f1514,definition,
( sQ79_spl
<=> precedes(sK8_skl,sK9_skl,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1516,plain,
( sQ79_spl
| ~ precedes(sK8_skl,sK9_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f1514]) ).
fof(f1517,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ48_spl
| ~ sQ34_spl
| sQ36_spl
| sQ35_spl
| ~ sQ79_spl
| sQ41_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f1513,f291,f652,f1514,f633,f636,f630,f850,f137,f145,f141]) ).
fof(f1518,plain,
( sQ79_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1516,f121]) ).
fof(f1519,plain,
sQ79_spl,
inference(contradiction_clause,[status(thm)],[f1518]) ).
fof(f1544,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ23_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ precedes(X1,X0,sK10_skl)
| ~ precedes(sK0_skl(X2,tail_of(sK4_skl(X0,X1,sK10_skl))),X0,sK10_skl)
| sequential(X1,X0)
| ~ sequential(sK0_skl(X2,tail_of(sK4_skl(X0,X1,sK10_skl))),X0)
| head_of(X0) != head_of(sK0_skl(X2,tail_of(sK4_skl(X0,X1,sK10_skl))))
| sequential(X1,X0)
| ~ precedes(X1,X0,sK10_skl)
| ~ shortest_path(X5,X6,sK10_skl)
| ~ vertex(tail_of(sK4_skl(X0,X1,sK10_skl)))
| sK4_skl(X0,X1,sK10_skl) = sK0_skl(X2,tail_of(sK4_skl(X0,X1,sK10_skl)))
| ~ vertex(X2)
| ~ path(X3,X4,sK10_skl)
| tail_of(sK4_skl(X0,X1,sK10_skl)) = X2 ),
inference(resolution,[status(thm)],[f1228,f328]) ).
fof(f1555,plain,
( ~ sQ23_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sQ6_spl
| sQ8_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f1544,f760,f182,f168,f137,f145,f327]) ).
fof(f1557,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ on_path(sK0_skl(tail_of(X2),X0),sK10_skl)
| tail_of(X2) = X0
| ~ edge(X2)
| X2 = sK0_skl(tail_of(X2),X0)
| sequential(sK0_skl(tail_of(X2),X0),X2)
| ~ on_path(X1,sK10_skl)
| ~ sequential(sK0_skl(tail_of(X2),X0),X1)
| head_of(X1) != head_of(X2)
| ~ vertex(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1075,f24]) ).
fof(f1558,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ1_spl
| ~ vertex(X1)
| sequential(sK0_skl(tail_of(X0),X1),X0)
| tail_of(X0) = X1
| sK0_skl(tail_of(X0),X1) = X0
| head_of(sK0_skl(tail_of(X0),X1)) = X1
| ~ edge(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f301,f24]) ).
fof(f1559,plain,
( sQ21_spl
| ~ edge(sK8_skl) ),
inference(resolution,[status(thm)],[f24,f293]) ).
fof(f1560,plain,
( sQ21_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f1559,f196,f291]) ).
fof(f1568,plain,
! [X0] :
( ~ sQ27_spl
| ~ edge(sK8_skl)
| sK0_skl(tail_of(sK8_skl),X0) = sK8_skl
| sequential(sK0_skl(tail_of(sK8_skl),X0),sK8_skl)
| ~ edge(sK0_skl(tail_of(sK8_skl),X0))
| X0 = tail_of(sK8_skl)
| ~ vertex(X0)
| head_of(sK0_skl(tail_of(sK8_skl),X0)) != head_of(sK9_skl) ),
inference(resolution,[status(thm)],[f383,f66]) ).
fof(f1569,definition,
! [X0] :
( sQ83_spl
<=> ( sK0_skl(tail_of(sK8_skl),X0) = sK8_skl
| sequential(sK0_skl(tail_of(sK8_skl),X0),sK8_skl)
| ~ edge(sK0_skl(tail_of(sK8_skl),X0))
| X0 = tail_of(sK8_skl)
| ~ vertex(X0)
| head_of(sK0_skl(tail_of(sK8_skl),X0)) != head_of(sK9_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1572,plain,
( ~ sQ27_spl
| ~ sQ11_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f1568,f1569,f196,f382]) ).
fof(f1577,plain,
! [X0] :
( ~ sQ57_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ on_path(sK0_skl(tail_of(sK8_skl),X0),sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),X0),sK9_skl)
| ~ vertex(X0)
| tail_of(sK8_skl) = X0
| sK0_skl(tail_of(sK8_skl),X0) = sK8_skl
| head_of(sK0_skl(tail_of(sK8_skl),X0)) = X0
| ~ edge(sK8_skl) ),
inference(resolution,[status(thm)],[f1558,f957]) ).
fof(f1590,plain,
( ~ sQ57_spl
| ~ sQ2_spl
| ~ sQ1_spl
| sQ70_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f1577,f196,f1289,f137,f141,f939]) ).
fof(f1605,plain,
( ~ sQ35_spl
| ~ edge(sK8_skl)
| sK9_skl = sK8_skl
| sequential(sK9_skl,sK8_skl)
| ~ edge(sK9_skl) ),
inference(resolution,[status(thm)],[f634,f66]) ).
fof(f1847,definition,
( sQ122_spl
<=> sK9_skl = sK8_skl ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1848,plain,
( ~ sQ122_spl
| sK9_skl = sK8_skl ),
inference(component_clause,[status(thm)],[f1847]) ).
fof(f1850,plain,
( ~ sQ35_spl
| ~ sQ11_spl
| sQ122_spl
| sQ55_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1605,f265,f932,f1847,f196,f633]) ).
fof(f1892,definition,
! [X0] :
( sQ130_spl
<=> ( X0 = sK8_skl
| sequential(X0,sK8_skl)
| ~ edge(X0)
| head_of(sK9_skl) != head_of(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition]) ).
fof(f1893,plain,
! [X0] :
( ~ sQ130_spl
| head_of(X0) != head_of(sK9_skl)
| sequential(X0,sK8_skl)
| sK8_skl = X0
| ~ edge(X0) ),
inference(component_clause,[status(thm)],[f1892]) ).
fof(f2011,plain,
( ~ sQ36_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ vertex(tail_of(sK8_skl))
| head_of(sK9_skl) = tail_of(sK8_skl)
| ~ edge(sK9_skl)
| ~ precedes(sK8_skl,sK9_skl,sK10_skl)
| sequential(sK9_skl,sK8_skl)
| sK0_skl(head_of(sK9_skl),tail_of(sK8_skl)) = sK9_skl ),
inference(paramodulation,[status(thm)],[f637,f1412]) ).
fof(f2043,plain,
( ~ sQ36_spl
| ~ sQ2_spl
| ~ vertex(tail_of(sK8_skl))
| head_of(sK9_skl) = tail_of(sK8_skl)
| head_of(sK9_skl) = head_of(sK0_skl(head_of(sK9_skl),tail_of(sK8_skl)))
| ~ vertex(head_of(sK9_skl))
| tail_of(sK8_skl) = head_of(sK9_skl) ),
inference(paramodulation,[status(thm)],[f637,f374]) ).
fof(f2105,definition,
( sQ157_spl
<=> head_of(sK0_skl(head_of(sK9_skl),tail_of(sK8_skl))) = head_of(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f2134,plain,
( ~ sQ36_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ21_spl
| sQ35_spl
| ~ sQ18_spl
| ~ sQ79_spl
| sQ55_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f2011,f652,f932,f1514,f265,f633,f291,f137,f141,f145,f636]) ).
fof(f2135,definition,
( sQ162_spl
<=> tail_of(sK8_skl) = head_of(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f2136,plain,
( ~ sQ162_spl
| head_of(sK8_skl) = tail_of(sK8_skl) ),
inference(component_clause,[status(thm)],[f2135]) ).
fof(f2142,plain,
( ~ sQ36_spl
| ~ sQ2_spl
| ~ sQ21_spl
| sQ157_spl
| ~ sQ34_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f2043,f633,f630,f2105,f291,f141,f636]) ).
fof(f2159,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| ~ sQ2_spl
| tail_of(X2) = tail_of(X0)
| ~ vertex(tail_of(X2))
| ~ vertex(tail_of(X0))
| ~ on_path(X2,sK10_skl)
| ~ on_path(sK0_skl(tail_of(X2),tail_of(X0)),sK10_skl)
| head_of(X2) != head_of(X0)
| tail_of(X2) = tail_of(sK0_skl(tail_of(X2),tail_of(X0)))
| ~ on_path(sK0_skl(tail_of(X2),tail_of(X0)),sK10_skl)
| tail_of(X2) = tail_of(X0)
| ~ edge(X2)
| X2 = sK0_skl(tail_of(X2),tail_of(X0))
| ~ on_path(X1,sK10_skl)
| ~ sequential(sK0_skl(tail_of(X2),tail_of(X0)),X1)
| head_of(X1) != head_of(X2)
| ~ vertex(tail_of(X0)) ),
inference(resolution,[status(thm)],[f1557,f897]) ).
fof(f2160,plain,
! [X0,X1] :
( ~ sQ57_spl
| ~ sQ2_spl
| ~ on_path(sK0_skl(tail_of(sK8_skl),X0),sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),X0),sK9_skl)
| ~ on_path(sK0_skl(tail_of(sK8_skl),X0),sK10_skl)
| tail_of(sK8_skl) = X0
| ~ edge(sK8_skl)
| sK8_skl = sK0_skl(tail_of(sK8_skl),X0)
| ~ on_path(X1,sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),X0),X1)
| head_of(X1) != head_of(sK8_skl)
| ~ vertex(X0) ),
inference(resolution,[status(thm)],[f1557,f957]) ).
fof(f2171,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| ~ sQ2_spl
| ~ vertex(tail_of(X2))
| ~ on_path(X2,sK10_skl)
| head_of(X2) != head_of(X0)
| tail_of(X2) = tail_of(sK0_skl(tail_of(X2),tail_of(X0)))
| ~ on_path(sK0_skl(tail_of(X2),tail_of(X0)),sK10_skl)
| tail_of(X2) = tail_of(X0)
| ~ edge(X2)
| X2 = sK0_skl(tail_of(X2),tail_of(X0))
| ~ on_path(X1,sK10_skl)
| ~ sequential(sK0_skl(tail_of(X2),tail_of(X0)),X1)
| head_of(X1) != head_of(X2)
| ~ vertex(tail_of(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f2159]) ).
fof(f2172,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| ~ sQ2_spl
| ~ on_path(X0,sK10_skl)
| ~ on_path(X1,sK10_skl)
| tail_of(X1) = tail_of(sK0_skl(tail_of(X1),tail_of(X2)))
| ~ edge(X1)
| head_of(X1) != head_of(X2)
| ~ vertex(tail_of(X2))
| tail_of(X2) = tail_of(X1)
| ~ on_path(sK0_skl(tail_of(X1),tail_of(X2)),sK10_skl)
| X1 = sK0_skl(tail_of(X1),tail_of(X2))
| ~ sequential(sK0_skl(tail_of(X1),tail_of(X2)),X0)
| head_of(X0) != head_of(X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2171,f24]) ).
fof(f2175,definition,
! [X0,X1] :
( sQ164_spl
<=> ( ~ on_path(sK0_skl(tail_of(sK8_skl),X0),sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),X0),sK9_skl)
| ~ on_path(sK0_skl(tail_of(sK8_skl),X0),sK10_skl)
| tail_of(sK8_skl) = X0
| sK8_skl = sK0_skl(tail_of(sK8_skl),X0)
| ~ on_path(X1,sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),X0),X1)
| head_of(X1) != head_of(sK8_skl)
| ~ vertex(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f2178,plain,
( ~ sQ57_spl
| ~ sQ2_spl
| ~ sQ11_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f2160,f2175,f196,f141,f939]) ).
fof(f2206,plain,
! [X0] :
( ~ sQ57_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ2_spl
| ~ on_path(sK0_skl(tail_of(sK8_skl),head_of(X0)),sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),head_of(X0)),sK9_skl)
| ~ edge(X0)
| ~ precedes(sK8_skl,X0,sK10_skl)
| tail_of(sK8_skl) = head_of(X0)
| sK8_skl = sK0_skl(tail_of(sK8_skl),head_of(X0))
| ~ vertex(tail_of(sK8_skl))
| sequential(X0,sK0_skl(tail_of(sK8_skl),head_of(X0)))
| sK0_skl(tail_of(sK8_skl),head_of(X0)) = X0 ),
inference(resolution,[status(thm)],[f1408,f957]) ).
fof(f2216,definition,
! [X0] :
( sQ167_spl
<=> ( ~ on_path(sK0_skl(tail_of(sK8_skl),head_of(X0)),sK10_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),head_of(X0)),sK9_skl)
| ~ edge(X0)
| ~ precedes(sK8_skl,X0,sK10_skl)
| tail_of(sK8_skl) = head_of(X0)
| sK8_skl = sK0_skl(tail_of(sK8_skl),head_of(X0))
| sequential(X0,sK0_skl(tail_of(sK8_skl),head_of(X0)))
| sK0_skl(tail_of(sK8_skl),head_of(X0)) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f2219,plain,
( ~ sQ57_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ2_spl
| ~ sQ21_spl
| sQ167_spl ),
inference(split_clause,[status(thm)],[f2206,f2216,f291,f141,f137,f145,f939]) ).
fof(f2226,plain,
! [X0] :
( ~ sQ19_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ sequential(sK0_skl(head_of(sK9_skl),tail_of(sK4_skl(sK9_skl,X0,sK10_skl))),sK8_skl)
| head_of(sK9_skl) = tail_of(sK4_skl(sK9_skl,X0,sK10_skl))
| sequential(X0,sK9_skl)
| ~ precedes(X0,sK9_skl,sK10_skl)
| ~ vertex(tail_of(sK4_skl(sK9_skl,X0,sK10_skl)))
| ~ edge(sK9_skl)
| sK0_skl(head_of(sK9_skl),tail_of(sK4_skl(sK9_skl,X0,sK10_skl))) = sK9_skl ),
inference(resolution,[status(thm)],[f1411,f839]) ).
fof(f2239,plain,
( ~ sQ19_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ3_spl
| ~ sQ18_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f2226,f846,f265,f145,f179,f137,f141,f268]) ).
fof(f2244,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ19_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| ~ sequential(sK0_skl(head_of(sK9_skl),tail_of(sK4_skl(sK9_skl,X0,X1))),sK8_skl)
| ~ edge(sK9_skl)
| tail_of(sK4_skl(sK9_skl,X0,X1)) = head_of(sK9_skl)
| ~ precedes(X0,sK9_skl,X1)
| ~ vertex(tail_of(sK4_skl(sK9_skl,X0,X1)))
| sequential(X0,sK9_skl)
| ~ shortest_path(X4,X5,X1)
| ~ path(X2,X3,X1)
| sK0_skl(head_of(sK9_skl),tail_of(sK4_skl(sK9_skl,X0,X1))) = sK9_skl ),
inference(resolution,[status(thm)],[f1410,f839]) ).
fof(f2259,plain,
( ~ sQ19_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ3_spl
| ~ sQ18_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f2244,f858,f265,f145,f137,f141,f268]) ).
fof(f2275,plain,
( ~ sQ162_spl
| ~ edge(sK8_skl) ),
inference(resolution,[status(thm)],[f2136,f21]) ).
fof(f2467,plain,
( ~ sQ162_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2275,f196,f2135]) ).
fof(f2710,plain,
! [X0,X1,X2] :
( vertex(head_of(X2))
| ~ on_path(X2,sK10_skl)
| ~ path(X0,X1,sK10_skl) ),
inference(resolution,[status(thm)],[f52,f453]) ).
fof(f2712,definition,
! [X2] :
( sQ230_spl
<=> ( vertex(head_of(X2))
| ~ on_path(X2,sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f2715,plain,
( sQ230_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f2710,f182,f2712]) ).
fof(f2756,plain,
! [X0,X1,X2] :
( ~ sQ3_spl
| ~ sQ2_spl
| tail_of(sK0_skl(tail_of(X0),tail_of(X1))) = tail_of(X0)
| tail_of(X1) = tail_of(X0)
| ~ sequential(sK0_skl(tail_of(X0),tail_of(X1)),X2)
| ~ on_path(X0,sK10_skl)
| head_of(X2) != head_of(X0)
| sK0_skl(tail_of(X0),tail_of(X1)) = X0
| head_of(X1) != head_of(X0)
| ~ on_path(X2,sK10_skl)
| ~ vertex(tail_of(X1))
| ~ on_path(sK0_skl(tail_of(X0),tail_of(X1)),sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2172,f458]) ).
fof(f2757,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ2_spl
| head_of(sK9_skl) != head_of(sK0_skl(tail_of(sK8_skl),tail_of(X0)))
| tail_of(X0) = tail_of(sK8_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),tail_of(X0)),X1)
| ~ on_path(sK8_skl,sK10_skl)
| head_of(X1) != head_of(sK8_skl)
| sK0_skl(tail_of(sK8_skl),tail_of(X0)) = sK8_skl
| head_of(X0) != head_of(sK8_skl)
| ~ on_path(X1,sK10_skl)
| ~ vertex(tail_of(X0))
| ~ on_path(sK0_skl(tail_of(sK8_skl),tail_of(X0)),sK10_skl) ),
inference(resolution,[status(thm)],[f2756,f166]) ).
fof(f2765,definition,
! [X0,X1] :
( sQ231_spl
<=> ( head_of(sK9_skl) != head_of(sK0_skl(tail_of(sK8_skl),tail_of(X0)))
| tail_of(X0) = tail_of(sK8_skl)
| ~ sequential(sK0_skl(tail_of(sK8_skl),tail_of(X0)),X1)
| head_of(X1) != head_of(sK8_skl)
| sK0_skl(tail_of(sK8_skl),tail_of(X0)) = sK8_skl
| head_of(X0) != head_of(sK8_skl)
| ~ on_path(X1,sK10_skl)
| ~ vertex(tail_of(X0))
| ~ on_path(sK0_skl(tail_of(sK8_skl),tail_of(X0)),sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f2768,plain,
( ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ54_spl
| sQ231_spl ),
inference(split_clause,[status(thm)],[f2757,f2765,f929,f141,f145,f165]) ).
fof(f3063,plain,
( ~ sQ41_spl
| ~ sQ20_spl
| head_of(sK9_skl) = tail_of(sK8_skl)
| ~ vertex(head_of(sK9_skl))
| tail_of(sK8_skl) = head_of(sK9_skl)
| head_of(sK0_skl(head_of(sK9_skl),tail_of(sK8_skl))) != head_of(sK9_skl) ),
inference(paramodulation,[status(thm)],[f653,f289]) ).
fof(f3079,plain,
( ~ sQ41_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ vertex(tail_of(sK8_skl))
| ~ precedes(sK8_skl,sK9_skl,sK10_skl)
| sK0_skl(head_of(sK9_skl),tail_of(sK8_skl)) = sK8_skl
| head_of(sK9_skl) = tail_of(sK8_skl)
| ~ vertex(head_of(sK9_skl)) ),
inference(paramodulation,[status(thm)],[f653,f1040]) ).
fof(f3159,plain,
( ~ sQ41_spl
| ~ sQ3_spl
| ~ sQ1_spl
| ~ sQ21_spl
| ~ sQ79_spl
| sQ36_spl
| sQ35_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f3079,f630,f633,f636,f1514,f291,f137,f145,f652]) ).
fof(f3161,plain,
( ~ sQ41_spl
| ~ sQ20_spl
| ~ sQ34_spl
| sQ35_spl
| ~ sQ157_spl ),
inference(split_clause,[status(thm)],[f3063,f2105,f633,f630,f288,f652]) ).
fof(f3196,plain,
( ~ sQ130_spl
| sequential(sK9_skl,sK8_skl)
| sK8_skl = sK9_skl
| ~ edge(sK9_skl) ),
inference(equality_resolution,[status(thm)],[f1893]) ).
fof(f3209,plain,
( ~ sQ130_spl
| sQ55_spl
| sQ122_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f3196,f265,f1847,f932,f1892]) ).
fof(f3297,plain,
( ~ sQ122_spl
| head_of(sK9_skl) != head_of(sK9_skl) ),
inference(backward_demodulation,[status(thm)],[f1848,f186]) ).
fof(f3317,plain,
( ~ sQ122_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3297]) ).
fof(f3318,plain,
~ sQ122_spl,
inference(contradiction_clause,[status(thm)],[f3317]) ).
fof(f3319,plain,
$false,
inference(sat_refutation,[status(thm)],[f140,f144,f148,f152,f160,f171,f185,f191,f199,f201,f212,f222,f228,f237,f253,f257,f271,f273,f294,f306,f330,f341,f367,f370,f385,f400,f471,f488,f503,f516,f612,f625,f627,f799,f830,f865,f923,f928,f938,f942,f946,f950,f952,f955,f970,f1032,f1049,f1185,f1288,f1296,f1301,f1320,f1401,f1417,f1435,f1446,f1504,f1517,f1519,f1555,f1560,f1572,f1590,f1850,f2134,f2142,f2178,f2219,f2239,f2259,f2467,f2715,f2768,f3159,f3161,f3209,f3318]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRA008+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/10.46 % Computer : n026.cluster.edu
% 0.16/10.46 % Model : x86_64 x86_64
% 0.16/10.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/10.46 % Memory : 8046.5625MB
% 0.16/10.46 % OS : Linux 6.8.0-71-generic
% 0.16/10.46 % CPULimit : 300
% 0.16/10.46 % WCLimit : 300
% 0.16/10.46 % DateTime : Sun Sep 20 18:24:02 UTC 2026
% 0.16/10.46 % CPUTime :
% 0.16/10.47 % Drodi V4.1.1
% 243.53/41.31 % Refutation found
% 243.53/41.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 243.53/41.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 142.57/42.54 % Elapsed time: 31.864171 seconds
% 142.57/42.54 % CPU time: 237.117337 seconds
% 142.57/42.54 % Total memory used: 745.039 MB
% 142.57/42.54 % Net memory used: 693.741 MB
%------------------------------------------------------------------------------