%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRA006+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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 : Tue Sep 29 10:08:26 AM UTC 2026
% Result : Theorem 43.44s 6.68s
% Output : Refutation 43.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 35
% Syntax : Number of formulae : 255 ( 32 unt; 25 def)
% Number of atoms : 1042 ( 284 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1301 ( 514 ~; 567 |; 165 &)
% ( 30 <=>; 17 =>; 0 <=; 8 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 27 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-3 aty)
% Number of variables : 361 ( 0 sgn 302 !; 59 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] :
( edge(X0)
=> ( vertex(head_of(X0))
& vertex(tail_of(X0)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax',edge_ends_are_vertices) ).
fof(f3,axiom,
( complete
=> ! [X0,X1] :
( ( vertex(X0)
& vertex(X1)
& X0 != X1 )
=> ? [X2] :
( edge(X2)
& ( ( X0 = head_of(X2)
& X1 = tail_of(X2) )
<~> ( X1 = head_of(X2)
& X0 = tail_of(X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax',complete_properties) ).
fof(f6,axiom,
! [X0,X1,X2,X3] :
( ( path(X0,X1,X2)
& on_path(X3,X2) )
=> ( edge(X3)
& in_path(head_of(X3),X2)
& in_path(tail_of(X3),X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax',on_path_properties) ).
fof(f7,axiom,
! [X0,X1,X2,X3] :
( ( path(X0,X1,X2)
& in_path(X3,X2) )
=> ( vertex(X3)
& ? [X4] :
( on_path(X4,X2)
& ( X3 = head_of(X4)
| X3 = tail_of(X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax',in_path_properties) ).
fof(f8,axiom,
! [X0,X1] :
( sequential(X0,X1)
<=> ( edge(X0)
& edge(X1)
& X0 != X1
& head_of(X0) = tail_of(X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax',sequential_defn) ).
fof(f9,axiom,
! [X0,X1,X2] :
( path(X1,X2,X0)
=> ! [X3,X4] :
( ( on_path(X3,X0)
& on_path(X4,X0)
& ( sequential(X3,X4)
| ? [X5] :
( sequential(X3,X5)
& precedes(X5,X4,X0) ) ) )
=> precedes(X3,X4,X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax',precedes_defn) ).
fof(f10,axiom,
! [X0,X1,X2] :
( path(X1,X2,X0)
=> ! [X3,X4] :
( precedes(X3,X4,X0)
=> ( on_path(X3,X0)
& on_path(X4,X0)
& ( sequential(X3,X4)
<~> ? [X5] :
( sequential(X3,X5)
& precedes(X5,X4,X0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax',precedes_properties) ).
fof(f11,axiom,
! [X0,X1,X2] :
( shortest_path(X0,X1,X2)
<=> ( path(X0,X1,X2)
& X0 != X1
& ! [X3] :
( path(X0,X1,X3)
=> less_or_equal(length_of(X2),length_of(X3)) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax',shortest_path_defn) ).
fof(f12,axiom,
! [X0,X1,X2,X3,X4] :
( ( shortest_path(X0,X1,X4)
& precedes(X2,X3,X4) )
=> ( ~ ? [X5] :
( tail_of(X5) = tail_of(X2)
& head_of(X5) = head_of(X3) )
& ~ precedes(X3,X2,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRA001+0.ax',shortest_path_properties) ).
fof(f18,conjecture,
( complete
=> ! [X0,X1,X2,X3,X4] :
( ( shortest_path(X0,X1,X4)
& precedes(X2,X3,X4) )
=> ( ? [X5] :
( edge(X5)
& tail_of(X5) = tail_of(X2)
& head_of(X5) = head_of(X3) )
<~> ? [X5] :
( edge(X5)
& tail_of(X5) = head_of(X3)
& head_of(X5) = tail_of(X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',edge_some_way) ).
fof(f19,negated_conjecture,
~ ( complete
=> ! [X0,X1,X2,X3,X4] :
( ( shortest_path(X0,X1,X4)
& precedes(X2,X3,X4) )
=> ( ? [X5] :
( edge(X5)
& tail_of(X5) = tail_of(X2)
& head_of(X5) = head_of(X3) )
<~> ? [X5] :
( edge(X5)
& tail_of(X5) = head_of(X3)
& head_of(X5) = tail_of(X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
~ ( complete
=> ! [X0,X1,X2,X3,X4] :
( ( shortest_path(X0,X1,X4)
& precedes(X2,X3,X4) )
=> ( ? [X5] :
( edge(X5)
& tail_of(X5) = tail_of(X2)
& head_of(X5) = head_of(X3) )
<~> ? [X6] :
( edge(X6)
& head_of(X3) = tail_of(X6)
& tail_of(X2) = head_of(X6) ) ) ) ),
inference(rectify,[],[f19]) ).
fof(f23,plain,
! [X0] :
( ( vertex(head_of(X0))
& vertex(tail_of(X0)) )
| ~ edge(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f24,plain,
( ! [X0,X1] :
( ? [X2] :
( edge(X2)
& ( ( X0 = head_of(X2)
& X1 = tail_of(X2) )
<~> ( X1 = head_of(X2)
& X0 = tail_of(X2) ) ) )
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1 )
| ~ complete ),
inference(ennf_transformation,[],[f3]) ).
fof(f25,plain,
( ! [X0,X1] :
( ? [X2] :
( edge(X2)
& ( ( X0 = head_of(X2)
& X1 = tail_of(X2) )
<~> ( X1 = head_of(X2)
& X0 = tail_of(X2) ) ) )
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1 )
| ~ complete ),
inference(flattening,[],[f24]) ).
fof(f29,plain,
! [X0,X1,X2,X3] :
( ( edge(X3)
& in_path(head_of(X3),X2)
& in_path(tail_of(X3),X2) )
| ~ path(X0,X1,X2)
| ~ on_path(X3,X2) ),
inference(ennf_transformation,[],[f6]) ).
fof(f30,plain,
! [X0,X1,X2,X3] :
( ( edge(X3)
& in_path(head_of(X3),X2)
& in_path(tail_of(X3),X2) )
| ~ path(X0,X1,X2)
| ~ on_path(X3,X2) ),
inference(flattening,[],[f29]) ).
fof(f31,plain,
! [X0,X1,X2,X3] :
( ( vertex(X3)
& ? [X4] :
( on_path(X4,X2)
& ( X3 = head_of(X4)
| X3 = tail_of(X4) ) ) )
| ~ path(X0,X1,X2)
| ~ in_path(X3,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f32,plain,
! [X0,X1,X2,X3] :
( ( vertex(X3)
& ? [X4] :
( on_path(X4,X2)
& ( X3 = head_of(X4)
| X3 = tail_of(X4) ) ) )
| ~ path(X0,X1,X2)
| ~ in_path(X3,X2) ),
inference(flattening,[],[f31]) ).
fof(f33,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( precedes(X3,X4,X0)
| ~ on_path(X3,X0)
| ~ on_path(X4,X0)
| ( ~ sequential(X3,X4)
& ! [X5] :
( ~ sequential(X3,X5)
| ~ precedes(X5,X4,X0) ) ) )
| ~ path(X1,X2,X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f34,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( precedes(X3,X4,X0)
| ~ on_path(X3,X0)
| ~ on_path(X4,X0)
| ( ~ sequential(X3,X4)
& ! [X5] :
( ~ sequential(X3,X5)
| ~ precedes(X5,X4,X0) ) ) )
| ~ path(X1,X2,X0) ),
inference(flattening,[],[f33]) ).
fof(f35,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( ( on_path(X3,X0)
& on_path(X4,X0)
& ( sequential(X3,X4)
<~> ? [X5] :
( sequential(X3,X5)
& precedes(X5,X4,X0) ) ) )
| ~ precedes(X3,X4,X0) )
| ~ path(X1,X2,X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f36,plain,
! [X0,X1,X2] :
( shortest_path(X0,X1,X2)
<=> ( path(X0,X1,X2)
& X0 != X1
& ! [X3] :
( less_or_equal(length_of(X2),length_of(X3))
| ~ path(X0,X1,X3) ) ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f37,plain,
! [X0,X1,X2,X3,X4] :
( ( ! [X5] :
( tail_of(X2) != tail_of(X5)
| head_of(X3) != head_of(X5) )
& ~ precedes(X3,X2,X4) )
| ~ shortest_path(X0,X1,X4)
| ~ precedes(X2,X3,X4) ),
inference(ennf_transformation,[],[f12]) ).
fof(f38,plain,
! [X0,X1,X2,X3,X4] :
( ( ! [X5] :
( tail_of(X2) != tail_of(X5)
| head_of(X3) != head_of(X5) )
& ~ precedes(X3,X2,X4) )
| ~ shortest_path(X0,X1,X4)
| ~ precedes(X2,X3,X4) ),
inference(flattening,[],[f37]) ).
fof(f45,plain,
( ? [X0,X1,X2,X3,X4] :
( ( ? [X5] :
( edge(X5)
& tail_of(X5) = tail_of(X2)
& head_of(X5) = head_of(X3) )
<=> ? [X6] :
( edge(X6)
& head_of(X3) = tail_of(X6)
& tail_of(X2) = head_of(X6) ) )
& shortest_path(X0,X1,X4)
& precedes(X2,X3,X4) )
& complete ),
inference(ennf_transformation,[],[f20]) ).
fof(f46,plain,
( ? [X0,X1,X2,X3,X4] :
( ( ? [X5] :
( edge(X5)
& tail_of(X5) = tail_of(X2)
& head_of(X5) = head_of(X3) )
<=> ? [X6] :
( edge(X6)
& head_of(X3) = tail_of(X6)
& tail_of(X2) = head_of(X6) ) )
& shortest_path(X0,X1,X4)
& precedes(X2,X3,X4) )
& complete ),
inference(flattening,[],[f45]) ).
fof(f47,plain,
( ! [X0,X1] :
( ? [X2] :
( edge(X2)
& ( head_of(X2) != X1
| tail_of(X2) != X0
| head_of(X2) != X0
| tail_of(X2) != X1 )
& ( ( X1 = head_of(X2)
& X0 = tail_of(X2) )
| ( X0 = head_of(X2)
& X1 = tail_of(X2) ) ) )
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1 )
| ~ complete ),
inference(nnf_transformation,[],[f25]) ).
fof(f48,plain,
( ! [X0,X1] :
( ? [X2] :
( edge(X2)
& ( head_of(X2) != X1
| tail_of(X2) != X0
| head_of(X2) != X0
| tail_of(X2) != X1 )
& ( ( X1 = head_of(X2)
& X0 = tail_of(X2) )
| ( X0 = head_of(X2)
& X1 = tail_of(X2) ) ) )
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1 )
| ~ complete ),
inference(flattening,[],[f47]) ).
fof(f49,plain,
( ! [X0,X1] :
( ( edge(sK0(X0,X1))
& ( head_of(sK0(X0,X1)) != X1
| tail_of(sK0(X0,X1)) != X0
| head_of(sK0(X0,X1)) != X0
| tail_of(sK0(X0,X1)) != X1 )
& ( ( head_of(sK0(X0,X1)) = X1
& tail_of(sK0(X0,X1)) = X0 )
| ( head_of(sK0(X0,X1)) = X0
& tail_of(sK0(X0,X1)) = X1 ) ) )
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1 )
| ~ complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f48]) ).
fof(f54,plain,
! [X0,X1,X2,X3] :
( ( vertex(X3)
& on_path(sK3(X2,X3),X2)
& ( head_of(sK3(X2,X3)) = X3
| tail_of(sK3(X2,X3)) = X3 ) )
| ~ path(X0,X1,X2)
| ~ in_path(X3,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X4,sK3(X2,X3))],[f32]) ).
fof(f55,plain,
! [X0,X1] :
( ( sequential(X0,X1)
| ~ edge(X0)
| ~ edge(X1)
| X0 = X1
| head_of(X0) != tail_of(X1) )
& ( ( edge(X0)
& edge(X1)
& X0 != X1
& head_of(X0) = tail_of(X1) )
| ~ sequential(X0,X1) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f56,plain,
! [X0,X1] :
( ( sequential(X0,X1)
| ~ edge(X0)
| ~ edge(X1)
| X0 = X1
| head_of(X0) != tail_of(X1) )
& ( ( edge(X0)
& edge(X1)
& X0 != X1
& head_of(X0) = tail_of(X1) )
| ~ sequential(X0,X1) ) ),
inference(flattening,[],[f55]) ).
fof(f57,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( ( on_path(X3,X0)
& on_path(X4,X0)
& ( ! [X5] :
( ~ sequential(X3,X5)
| ~ precedes(X5,X4,X0) )
| ~ sequential(X3,X4) )
& ( ? [X5] :
( sequential(X3,X5)
& precedes(X5,X4,X0) )
| sequential(X3,X4) ) )
| ~ precedes(X3,X4,X0) )
| ~ path(X1,X2,X0) ),
inference(nnf_transformation,[],[f35]) ).
fof(f58,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( ( on_path(X3,X0)
& on_path(X4,X0)
& ( ! [X5] :
( ~ sequential(X3,X5)
| ~ precedes(X5,X4,X0) )
| ~ sequential(X3,X4) )
& ( ? [X5] :
( sequential(X3,X5)
& precedes(X5,X4,X0) )
| sequential(X3,X4) ) )
| ~ precedes(X3,X4,X0) )
| ~ path(X1,X2,X0) ),
inference(flattening,[],[f57]) ).
fof(f59,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( ( on_path(X3,X0)
& on_path(X4,X0)
& ( ! [X5] :
( ~ sequential(X3,X5)
| ~ precedes(X5,X4,X0) )
| ~ sequential(X3,X4) )
& ( ? [X6] :
( sequential(X3,X6)
& precedes(X6,X4,X0) )
| sequential(X3,X4) ) )
| ~ precedes(X3,X4,X0) )
| ~ path(X1,X2,X0) ),
inference(rectify,[],[f58]) ).
fof(f60,plain,
! [X0,X1,X2] :
( ! [X3,X4] :
( ( on_path(X3,X0)
& on_path(X4,X0)
& ( ! [X5] :
( ~ sequential(X3,X5)
| ~ precedes(X5,X4,X0) )
| ~ sequential(X3,X4) )
& ( ( sequential(X3,sK4(X0,X3,X4))
& precedes(sK4(X0,X3,X4),X4,X0) )
| sequential(X3,X4) ) )
| ~ precedes(X3,X4,X0) )
| ~ path(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X6,sK4(X0,X3,X4))],[f59]) ).
fof(f61,plain,
! [X0,X1,X2] :
( ( shortest_path(X0,X1,X2)
| ~ path(X0,X1,X2)
| X0 = X1
| ? [X3] :
( ~ less_or_equal(length_of(X2),length_of(X3))
& path(X0,X1,X3) ) )
& ( ( path(X0,X1,X2)
& X0 != X1
& ! [X3] :
( less_or_equal(length_of(X2),length_of(X3))
| ~ path(X0,X1,X3) ) )
| ~ shortest_path(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f36]) ).
fof(f62,plain,
! [X0,X1,X2] :
( ( shortest_path(X0,X1,X2)
| ~ path(X0,X1,X2)
| X0 = X1
| ? [X3] :
( ~ less_or_equal(length_of(X2),length_of(X3))
& path(X0,X1,X3) ) )
& ( ( path(X0,X1,X2)
& X0 != X1
& ! [X3] :
( less_or_equal(length_of(X2),length_of(X3))
| ~ path(X0,X1,X3) ) )
| ~ shortest_path(X0,X1,X2) ) ),
inference(flattening,[],[f61]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ( shortest_path(X0,X1,X2)
| ~ path(X0,X1,X2)
| X0 = X1
| ? [X3] :
( ~ less_or_equal(length_of(X2),length_of(X3))
& path(X0,X1,X3) ) )
& ( ( path(X0,X1,X2)
& X0 != X1
& ! [X4] :
( less_or_equal(length_of(X2),length_of(X4))
| ~ path(X0,X1,X4) ) )
| ~ shortest_path(X0,X1,X2) ) ),
inference(rectify,[],[f62]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ( shortest_path(X0,X1,X2)
| ~ path(X0,X1,X2)
| X0 = X1
| ( ~ less_or_equal(length_of(X2),length_of(sK5(X0,X1,X2)))
& path(X0,X1,sK5(X0,X1,X2)) ) )
& ( ( path(X0,X1,X2)
& X0 != X1
& ! [X4] :
( less_or_equal(length_of(X2),length_of(X4))
| ~ path(X0,X1,X4) ) )
| ~ shortest_path(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X3,sK5(X0,X1,X2))],[f63]) ).
fof(f66,plain,
( ? [X0,X1,X2,X3,X4] :
( ( ? [X5] :
( edge(X5)
& tail_of(X5) = tail_of(X2)
& head_of(X5) = head_of(X3) )
| ! [X6] :
( ~ edge(X6)
| head_of(X3) != tail_of(X6)
| tail_of(X2) != head_of(X6) ) )
& ( ? [X6] :
( edge(X6)
& head_of(X3) = tail_of(X6)
& tail_of(X2) = head_of(X6) )
| ! [X5] :
( ~ edge(X5)
| tail_of(X2) != tail_of(X5)
| head_of(X3) != head_of(X5) ) )
& shortest_path(X0,X1,X4)
& precedes(X2,X3,X4) )
& complete ),
inference(nnf_transformation,[],[f46]) ).
fof(f67,plain,
( ? [X0,X1,X2,X3,X4] :
( ( ? [X5] :
( edge(X5)
& tail_of(X5) = tail_of(X2)
& head_of(X5) = head_of(X3) )
| ! [X6] :
( ~ edge(X6)
| head_of(X3) != tail_of(X6)
| tail_of(X2) != head_of(X6) ) )
& ( ? [X6] :
( edge(X6)
& head_of(X3) = tail_of(X6)
& tail_of(X2) = head_of(X6) )
| ! [X5] :
( ~ edge(X5)
| tail_of(X2) != tail_of(X5)
| head_of(X3) != head_of(X5) ) )
& shortest_path(X0,X1,X4)
& precedes(X2,X3,X4) )
& complete ),
inference(flattening,[],[f66]) ).
fof(f68,plain,
( ? [X0,X1,X2,X3,X4] :
( ( ? [X5] :
( edge(X5)
& tail_of(X5) = tail_of(X2)
& head_of(X5) = head_of(X3) )
| ! [X6] :
( ~ edge(X6)
| head_of(X3) != tail_of(X6)
| tail_of(X2) != head_of(X6) ) )
& ( ? [X7] :
( edge(X7)
& head_of(X3) = tail_of(X7)
& tail_of(X2) = head_of(X7) )
| ! [X8] :
( ~ edge(X8)
| tail_of(X2) != tail_of(X8)
| head_of(X3) != head_of(X8) ) )
& shortest_path(X0,X1,X4)
& precedes(X2,X3,X4) )
& complete ),
inference(rectify,[],[f67]) ).
fof(f69,plain,
( ( ( edge(sK13)
& tail_of(sK10) = tail_of(sK13)
& head_of(sK11) = head_of(sK13) )
| ! [X6] :
( ~ edge(X6)
| tail_of(X6) != head_of(sK11)
| head_of(X6) != tail_of(sK10) ) )
& ( ( edge(sK14)
& head_of(sK11) = tail_of(sK14)
& tail_of(sK10) = head_of(sK14) )
| ! [X8] :
( ~ edge(X8)
| tail_of(X8) != tail_of(sK10)
| head_of(X8) != head_of(sK11) ) )
& shortest_path(sK8,sK9,sK12)
& precedes(sK10,sK11,sK12)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11,sK12,sK13,sK14]),skolemize(X0,sK8),skolemize(X1,sK9),skolemize(X2,sK10),skolemize(X3,sK11),skolemize(X4,sK12),skolemize(X5,sK13),skolemize(X7,sK14)],[f68]) ).
fof(f71,plain,
! [X0] :
( vertex(tail_of(X0))
| ~ edge(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f73,plain,
! [X0,X1] :
( tail_of(sK0(X0,X1)) = X0
| tail_of(sK0(X0,X1)) = X1
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1
| ~ complete ),
inference(cnf_transformation,[],[f49]) ).
fof(f74,plain,
! [X0,X1] :
( tail_of(sK0(X0,X1)) = X0
| head_of(sK0(X0,X1)) = X0
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1
| ~ complete ),
inference(cnf_transformation,[],[f49]) ).
fof(f75,plain,
! [X0,X1] :
( head_of(sK0(X0,X1)) = X1
| tail_of(sK0(X0,X1)) = X1
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1
| ~ complete ),
inference(cnf_transformation,[],[f49]) ).
fof(f76,plain,
! [X0,X1] :
( head_of(sK0(X0,X1)) = X1
| head_of(sK0(X0,X1)) = X0
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1
| ~ complete ),
inference(cnf_transformation,[],[f49]) ).
fof(f78,plain,
! [X0,X1] :
( edge(sK0(X0,X1))
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1
| ~ complete ),
inference(cnf_transformation,[],[f49]) ).
fof(f90,plain,
! [X2,X3,X0,X1] :
( ~ path(X0,X1,X2)
| in_path(tail_of(X3),X2)
| ~ on_path(X3,X2) ),
inference(cnf_transformation,[],[f30]) ).
fof(f91,plain,
! [X2,X3,X0,X1] :
( ~ path(X0,X1,X2)
| in_path(head_of(X3),X2)
| ~ on_path(X3,X2) ),
inference(cnf_transformation,[],[f30]) ).
fof(f92,plain,
! [X2,X3,X0,X1] :
( ~ path(X0,X1,X2)
| edge(X3)
| ~ on_path(X3,X2) ),
inference(cnf_transformation,[],[f30]) ).
fof(f95,plain,
! [X2,X3,X0,X1] :
( ~ path(X0,X1,X2)
| vertex(X3)
| ~ in_path(X3,X2) ),
inference(cnf_transformation,[],[f54]) ).
fof(f100,plain,
! [X0,X1] :
( sequential(X0,X1)
| ~ edge(X0)
| ~ edge(X1)
| X0 = X1
| head_of(X0) != tail_of(X1) ),
inference(cnf_transformation,[],[f56]) ).
fof(f102,plain,
! [X2,X3,X0,X1,X4] :
( ~ path(X1,X2,X0)
| ~ on_path(X3,X0)
| ~ on_path(X4,X0)
| ~ sequential(X3,X4)
| precedes(X3,X4,X0) ),
inference(cnf_transformation,[],[f34]) ).
fof(f106,plain,
! [X2,X3,X0,X1,X4] :
( ~ path(X1,X2,X0)
| ~ precedes(X3,X4,X0)
| on_path(X4,X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f107,plain,
! [X2,X3,X0,X1,X4] :
( ~ path(X1,X2,X0)
| ~ precedes(X3,X4,X0)
| on_path(X3,X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f110,plain,
! [X2,X0,X1] :
( ~ shortest_path(X0,X1,X2)
| path(X0,X1,X2) ),
inference(cnf_transformation,[],[f64]) ).
fof(f113,plain,
! [X2,X3,X0,X1,X4] :
( ~ precedes(X2,X3,X4)
| ~ shortest_path(X0,X1,X4)
| ~ precedes(X3,X2,X4) ),
inference(cnf_transformation,[],[f38]) ).
fof(f114,plain,
! [X2,X3,X0,X1,X4,X5] :
( head_of(X3) != head_of(X5)
| tail_of(X2) != tail_of(X5)
| ~ shortest_path(X0,X1,X4)
| ~ precedes(X2,X3,X4) ),
inference(cnf_transformation,[],[f38]) ).
fof(f123,plain,
complete,
inference(cnf_transformation,[],[f69]) ).
fof(f124,plain,
precedes(sK10,sK11,sK12),
inference(cnf_transformation,[],[f69]) ).
fof(f125,plain,
shortest_path(sK8,sK9,sK12),
inference(cnf_transformation,[],[f69]) ).
fof(f126,plain,
! [X8] :
( tail_of(sK10) = head_of(sK14)
| ~ edge(X8)
| tail_of(X8) != tail_of(sK10)
| head_of(X8) != head_of(sK11) ),
inference(cnf_transformation,[],[f69]) ).
fof(f127,plain,
! [X8] :
( head_of(sK11) = tail_of(sK14)
| ~ edge(X8)
| tail_of(X8) != tail_of(sK10)
| head_of(X8) != head_of(sK11) ),
inference(cnf_transformation,[],[f69]) ).
fof(f128,plain,
! [X8] :
( edge(sK14)
| ~ edge(X8)
| tail_of(X8) != tail_of(sK10)
| head_of(X8) != head_of(sK11) ),
inference(cnf_transformation,[],[f69]) ).
fof(f129,plain,
! [X6] :
( head_of(sK11) = head_of(sK13)
| ~ edge(X6)
| tail_of(X6) != head_of(sK11)
| head_of(X6) != tail_of(sK10) ),
inference(cnf_transformation,[],[f69]) ).
fof(f130,plain,
! [X6] :
( tail_of(sK10) = tail_of(sK13)
| ~ edge(X6)
| tail_of(X6) != head_of(sK11)
| head_of(X6) != tail_of(sK10) ),
inference(cnf_transformation,[],[f69]) ).
fof(f131,plain,
! [X6] :
( edge(sK13)
| ~ edge(X6)
| tail_of(X6) != head_of(sK11)
| head_of(X6) != tail_of(sK10) ),
inference(cnf_transformation,[],[f69]) ).
fof(f140,definition,
( spl15_1
<=> ! [X8] :
( ~ edge(X8)
| head_of(X8) != head_of(sK11)
| tail_of(X8) != tail_of(sK10) ) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
fof(f141,plain,
( ! [X8] :
( ~ edge(X8)
| head_of(X8) != head_of(sK11)
| tail_of(X8) != tail_of(sK10) )
| ~ spl15_1 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f143,definition,
( spl15_2
<=> tail_of(sK10) = head_of(sK14) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
fof(f145,plain,
( tail_of(sK10) = head_of(sK14)
| ~ spl15_2 ),
inference(avatar_component_clause,[],[f143]) ).
fof(f146,plain,
( spl15_1
| spl15_2 ),
inference(avatar_split_clause,[],[f126,f143,f140]) ).
fof(f148,definition,
( spl15_3
<=> head_of(sK11) = tail_of(sK14) ),
introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition]) ).
fof(f150,plain,
( head_of(sK11) = tail_of(sK14)
| ~ spl15_3 ),
inference(avatar_component_clause,[],[f148]) ).
fof(f151,plain,
( spl15_1
| spl15_3 ),
inference(avatar_split_clause,[],[f127,f148,f140]) ).
fof(f153,definition,
( spl15_4
<=> edge(sK14) ),
introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition]) ).
fof(f155,plain,
( edge(sK14)
| ~ spl15_4 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f156,plain,
( spl15_1
| spl15_4 ),
inference(avatar_split_clause,[],[f128,f153,f140]) ).
fof(f158,definition,
( spl15_5
<=> ! [X6] :
( ~ edge(X6)
| head_of(X6) != tail_of(sK10)
| tail_of(X6) != head_of(sK11) ) ),
introduced(definition,[new_symbols(definition,[spl15_5])],[avatar_definition]) ).
fof(f159,plain,
( ! [X6] :
( ~ edge(X6)
| head_of(X6) != tail_of(sK10)
| tail_of(X6) != head_of(sK11) )
| ~ spl15_5 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f161,definition,
( spl15_6
<=> head_of(sK11) = head_of(sK13) ),
introduced(definition,[new_symbols(definition,[spl15_6])],[avatar_definition]) ).
fof(f163,plain,
( head_of(sK11) = head_of(sK13)
| ~ spl15_6 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f164,plain,
( spl15_5
| spl15_6 ),
inference(avatar_split_clause,[],[f129,f161,f158]) ).
fof(f166,definition,
( spl15_7
<=> tail_of(sK10) = tail_of(sK13) ),
introduced(definition,[new_symbols(definition,[spl15_7])],[avatar_definition]) ).
fof(f168,plain,
( tail_of(sK10) = tail_of(sK13)
| ~ spl15_7 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f169,plain,
( spl15_5
| spl15_7 ),
inference(avatar_split_clause,[],[f130,f166,f158]) ).
fof(f171,definition,
( spl15_8
<=> edge(sK13) ),
introduced(definition,[new_symbols(definition,[spl15_8])],[avatar_definition]) ).
fof(f173,plain,
( edge(sK13)
| ~ spl15_8 ),
inference(avatar_component_clause,[],[f171]) ).
fof(f174,plain,
( spl15_5
| spl15_8 ),
inference(avatar_split_clause,[],[f131,f171,f158]) ).
fof(f176,definition,
( spl15_9
<=> complete ),
introduced(definition,[new_symbols(definition,[spl15_9])],[avatar_definition]) ).
fof(f180,definition,
( spl15_10
<=> ! [X0,X1] :
( tail_of(sK0(X0,X1)) = X0
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| tail_of(sK0(X0,X1)) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition]) ).
fof(f181,plain,
( ! [X0,X1] :
( ~ vertex(X0)
| X0 = X1
| ~ vertex(X1)
| tail_of(sK0(X0,X1)) = X0
| tail_of(sK0(X0,X1)) = X1 )
| ~ spl15_10 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f182,plain,
( ~ spl15_9
| spl15_10 ),
inference(avatar_split_clause,[],[f73,f180,f176]) ).
fof(f184,definition,
( spl15_11
<=> ! [X0,X1] :
( tail_of(sK0(X0,X1)) = X0
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| head_of(sK0(X0,X1)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition]) ).
fof(f185,plain,
( ! [X0,X1] :
( ~ vertex(X0)
| X0 = X1
| ~ vertex(X1)
| tail_of(sK0(X0,X1)) = X0
| head_of(sK0(X0,X1)) = X0 )
| ~ spl15_11 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f186,plain,
( ~ spl15_9
| spl15_11 ),
inference(avatar_split_clause,[],[f74,f184,f176]) ).
fof(f188,definition,
( spl15_12
<=> ! [X0,X1] :
( head_of(sK0(X0,X1)) = X1
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| tail_of(sK0(X0,X1)) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition]) ).
fof(f189,plain,
( ! [X0,X1] :
( ~ vertex(X0)
| X0 = X1
| ~ vertex(X1)
| head_of(sK0(X0,X1)) = X1
| tail_of(sK0(X0,X1)) = X1 )
| ~ spl15_12 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f190,plain,
( ~ spl15_9
| spl15_12 ),
inference(avatar_split_clause,[],[f75,f188,f176]) ).
fof(f192,definition,
( spl15_13
<=> ! [X0,X1] :
( head_of(sK0(X0,X1)) = X1
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| head_of(sK0(X0,X1)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition]) ).
fof(f193,plain,
( ! [X0,X1] :
( ~ vertex(X0)
| X0 = X1
| ~ vertex(X1)
| head_of(sK0(X0,X1)) = X1
| head_of(sK0(X0,X1)) = X0 )
| ~ spl15_13 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f194,plain,
( ~ spl15_9
| spl15_13 ),
inference(avatar_split_clause,[],[f76,f192,f176]) ).
fof(f200,definition,
( spl15_15
<=> ! [X0,X1] :
( edge(sK0(X0,X1))
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0) ) ),
introduced(definition,[new_symbols(definition,[spl15_15])],[avatar_definition]) ).
fof(f201,plain,
( ! [X0,X1] :
( edge(sK0(X0,X1))
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0) )
| ~ spl15_15 ),
inference(avatar_component_clause,[],[f200]) ).
fof(f202,plain,
( ~ spl15_9
| spl15_15 ),
inference(avatar_split_clause,[],[f78,f200,f176]) ).
fof(f203,plain,
spl15_9,
inference(avatar_split_clause,[],[f123,f176]) ).
fof(f204,plain,
( tail_of(sK13) = head_of(sK14)
| ~ spl15_2
| ~ spl15_7 ),
inference(forward_demodulation,[],[f168,f145]) ).
fof(f206,plain,
( ! [X6] :
( ~ edge(X6)
| head_of(X6) != head_of(sK14)
| tail_of(X6) != head_of(sK11) )
| ~ spl15_2
| ~ spl15_5 ),
inference(forward_demodulation,[],[f159,f145]) ).
fof(f214,plain,
( head_of(sK14) != head_of(sK14)
| head_of(sK11) != tail_of(sK14)
| ~ spl15_2
| ~ spl15_4
| ~ spl15_5 ),
inference(resolution,[],[f206,f155]) ).
fof(f215,plain,
( head_of(sK11) != tail_of(sK14)
| ~ spl15_2
| ~ spl15_4
| ~ spl15_5 ),
inference(trivial_inequality_removal,[],[f214]) ).
fof(f216,plain,
( $false
| ~ spl15_2
| ~ spl15_3
| ~ spl15_4
| ~ spl15_5 ),
inference(forward_subsumption_resolution,[],[f215,f150]) ).
fof(f217,plain,
( ~ spl15_2
| ~ spl15_3
| ~ spl15_4
| ~ spl15_5 ),
inference(avatar_contradiction_clause,[],[f216]) ).
fof(f224,definition,
( spl15_16
<=> edge(sK10) ),
introduced(definition,[new_symbols(definition,[spl15_16])],[avatar_definition]) ).
fof(f225,plain,
( edge(sK10)
| ~ spl15_16 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f240,plain,
path(sK8,sK9,sK12),
inference(resolution,[],[f110,f125]) ).
fof(f244,plain,
! [X0] :
( ~ on_path(X0,sK12)
| edge(X0) ),
inference(resolution,[],[f92,f240]) ).
fof(f245,plain,
! [X0] :
( ~ in_path(X0,sK12)
| vertex(X0) ),
inference(resolution,[],[f95,f240]) ).
fof(f248,plain,
! [X0] :
( in_path(tail_of(X0),sK12)
| ~ on_path(X0,sK12) ),
inference(resolution,[],[f90,f240]) ).
fof(f250,plain,
! [X0] :
( in_path(head_of(X0),sK12)
| ~ on_path(X0,sK12) ),
inference(resolution,[],[f91,f240]) ).
fof(f251,plain,
! [X0,X1] :
( ~ precedes(X0,X1,sK12)
| on_path(X1,sK12) ),
inference(resolution,[],[f106,f240]) ).
fof(f253,plain,
! [X0,X1] :
( ~ precedes(X0,X1,sK12)
| on_path(X0,sK12) ),
inference(resolution,[],[f107,f240]) ).
fof(f254,plain,
! [X0] :
( ~ on_path(X0,sK12)
| vertex(tail_of(X0)) ),
inference(resolution,[],[f248,f245]) ).
fof(f278,definition,
( spl15_22
<=> on_path(sK10,sK12) ),
introduced(definition,[new_symbols(definition,[spl15_22])],[avatar_definition]) ).
fof(f279,plain,
( on_path(sK10,sK12)
| ~ spl15_22 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f293,plain,
! [X0,X1] :
( ~ shortest_path(X0,X1,sK12)
| ~ precedes(sK11,sK10,sK12) ),
inference(resolution,[],[f113,f124]) ).
fof(f295,definition,
( spl15_25
<=> precedes(sK11,sK10,sK12) ),
introduced(definition,[new_symbols(definition,[spl15_25])],[avatar_definition]) ).
fof(f297,plain,
( ~ precedes(sK11,sK10,sK12)
| spl15_25 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f299,definition,
( spl15_26
<=> ! [X0,X1] : ~ shortest_path(X0,X1,sK12) ),
introduced(definition,[new_symbols(definition,[spl15_26])],[avatar_definition]) ).
fof(f300,plain,
( ! [X0,X1] : ~ shortest_path(X0,X1,sK12)
| ~ spl15_26 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f301,plain,
( ~ spl15_25
| spl15_26 ),
inference(avatar_split_clause,[],[f293,f299,f295]) ).
fof(f385,plain,
! [X0,X1] :
( precedes(X0,X1,sK12)
| ~ on_path(X1,sK12)
| ~ sequential(X0,X1)
| ~ on_path(X0,sK12) ),
inference(resolution,[],[f102,f240]) ).
fof(f418,plain,
( ! [X2,X3,X0,X1,X4] :
( head_of(X0) != head_of(sK11)
| tail_of(X1) != tail_of(sK13)
| ~ shortest_path(X2,X3,X4)
| ~ precedes(X1,X0,X4) )
| ~ spl15_6 ),
inference(superposition,[],[f114,f163]) ).
fof(f420,plain,
( ! [X2,X3,X0,X1,X4] :
( head_of(X0) != head_of(sK11)
| tail_of(X1) != head_of(sK14)
| ~ shortest_path(X2,X3,X4)
| ~ precedes(X1,X0,X4) )
| ~ spl15_2
| ~ spl15_6
| ~ spl15_7 ),
inference(forward_demodulation,[],[f418,f204]) ).
fof(f423,plain,
! [X0] :
( ~ on_path(X0,sK12)
| vertex(head_of(X0)) ),
inference(resolution,[],[f250,f245]) ).
fof(f431,plain,
on_path(sK11,sK12),
inference(resolution,[],[f251,f124]) ).
fof(f436,plain,
vertex(head_of(sK11)),
inference(resolution,[],[f431,f423]) ).
fof(f438,plain,
edge(sK11),
inference(resolution,[],[f431,f244]) ).
fof(f473,plain,
( ! [X0,X1] :
( ~ edge(X0)
| ~ vertex(X1)
| tail_of(X0) = tail_of(sK0(tail_of(X0),X1))
| tail_of(sK0(tail_of(X0),X1)) = X1
| tail_of(X0) = X1 )
| ~ spl15_10 ),
inference(resolution,[],[f181,f71]) ).
fof(f481,plain,
( ! [X0,X1] :
( ~ edge(X0)
| ~ vertex(X1)
| tail_of(X0) = tail_of(sK0(tail_of(X0),X1))
| tail_of(X0) = head_of(sK0(tail_of(X0),X1))
| tail_of(X0) = X1 )
| ~ spl15_11 ),
inference(resolution,[],[f185,f71]) ).
fof(f488,plain,
( ! [X0,X1] :
( ~ edge(X0)
| ~ vertex(X1)
| head_of(sK0(tail_of(X0),X1)) = X1
| tail_of(sK0(tail_of(X0),X1)) = X1
| tail_of(X0) = X1 )
| ~ spl15_12 ),
inference(resolution,[],[f189,f71]) ).
fof(f492,plain,
on_path(sK10,sK12),
inference(resolution,[],[f253,f124]) ).
fof(f495,plain,
spl15_22,
inference(avatar_split_clause,[],[f492,f278]) ).
fof(f499,plain,
( ! [X0,X1] :
( ~ edge(X0)
| ~ vertex(X1)
| head_of(sK0(tail_of(X0),X1)) = X1
| tail_of(X0) = head_of(sK0(tail_of(X0),X1))
| tail_of(X0) = X1 )
| ~ spl15_13 ),
inference(resolution,[],[f193,f71]) ).
fof(f504,plain,
( vertex(tail_of(sK10))
| ~ spl15_22 ),
inference(resolution,[],[f279,f254]) ).
fof(f505,plain,
( edge(sK10)
| ~ spl15_22 ),
inference(resolution,[],[f279,f244]) ).
fof(f518,plain,
( spl15_16
| ~ spl15_22 ),
inference(avatar_split_clause,[],[f505,f278,f224]) ).
fof(f921,plain,
( ! [X2,X3,X0,X1] :
( tail_of(X0) != head_of(sK14)
| ~ shortest_path(X1,X2,X3)
| ~ precedes(X0,sK11,X3) )
| ~ spl15_2
| ~ spl15_6
| ~ spl15_7 ),
inference(equality_resolution,[],[f420]) ).
fof(f1460,plain,
( ! [X0] :
( ~ vertex(X0)
| head_of(sK0(tail_of(sK10),X0)) = X0
| tail_of(sK0(tail_of(sK10),X0)) = X0
| tail_of(sK10) = X0 )
| ~ spl15_12
| ~ spl15_16 ),
inference(resolution,[],[f488,f225]) ).
fof(f1513,plain,
( ! [X0] :
( ~ vertex(X0)
| tail_of(sK10) = tail_of(sK0(tail_of(sK10),X0))
| tail_of(sK0(tail_of(sK10),X0)) = X0
| tail_of(sK10) = X0 )
| ~ spl15_10
| ~ spl15_16 ),
inference(resolution,[],[f473,f225]) ).
fof(f1548,plain,
( ! [X0] :
( ~ vertex(X0)
| head_of(sK0(tail_of(sK10),X0)) = X0
| tail_of(sK10) = head_of(sK0(tail_of(sK10),X0))
| tail_of(sK10) = X0 )
| ~ spl15_13
| ~ spl15_16 ),
inference(resolution,[],[f499,f225]) ).
fof(f1650,plain,
( ! [X0] :
( ~ vertex(X0)
| tail_of(sK10) = tail_of(sK0(tail_of(sK10),X0))
| tail_of(sK10) = head_of(sK0(tail_of(sK10),X0))
| tail_of(sK10) = X0 )
| ~ spl15_11
| ~ spl15_16 ),
inference(resolution,[],[f481,f225]) ).
fof(f3265,plain,
( ~ on_path(sK10,sK12)
| ~ sequential(sK11,sK10)
| ~ on_path(sK11,sK12)
| spl15_25 ),
inference(resolution,[],[f385,f297]) ).
fof(f3268,plain,
( ~ sequential(sK11,sK10)
| ~ on_path(sK11,sK12)
| ~ spl15_22
| spl15_25 ),
inference(forward_subsumption_resolution,[],[f3265,f279]) ).
fof(f3270,plain,
( ~ sequential(sK11,sK10)
| ~ spl15_22
| spl15_25 ),
inference(forward_subsumption_resolution,[],[f3268,f431]) ).
fof(f3276,plain,
( ~ edge(sK11)
| ~ edge(sK10)
| sK10 = sK11
| tail_of(sK10) != head_of(sK11)
| ~ spl15_22
| spl15_25 ),
inference(resolution,[],[f3270,f100]) ).
fof(f3277,plain,
( ~ edge(sK10)
| sK10 = sK11
| tail_of(sK10) != head_of(sK11)
| ~ spl15_22
| spl15_25 ),
inference(forward_subsumption_resolution,[],[f3276,f438]) ).
fof(f3278,plain,
( sK10 = sK11
| tail_of(sK10) != head_of(sK11)
| ~ spl15_16
| ~ spl15_22
| spl15_25 ),
inference(forward_subsumption_resolution,[],[f3277,f225]) ).
fof(f3332,plain,
( ! [X2,X0,X1] :
( head_of(sK14) != head_of(sK14)
| ~ shortest_path(X0,X1,X2)
| ~ precedes(sK10,sK11,X2) )
| ~ spl15_2
| ~ spl15_6
| ~ spl15_7 ),
inference(superposition,[],[f921,f145]) ).
fof(f3336,plain,
( ! [X2,X0,X1] :
( ~ shortest_path(X0,X1,X2)
| ~ precedes(sK10,sK11,X2) )
| ~ spl15_2
| ~ spl15_6
| ~ spl15_7 ),
inference(trivial_inequality_removal,[],[f3332]) ).
fof(f3386,plain,
( ~ precedes(sK10,sK11,sK12)
| ~ spl15_2
| ~ spl15_6
| ~ spl15_7 ),
inference(resolution,[],[f3336,f125]) ).
fof(f3392,plain,
( $false
| ~ spl15_2
| ~ spl15_6
| ~ spl15_7 ),
inference(forward_subsumption_resolution,[],[f3386,f124]) ).
fof(f3393,plain,
( ~ spl15_2
| ~ spl15_6
| ~ spl15_7 ),
inference(avatar_contradiction_clause,[],[f3392]) ).
fof(f3464,definition,
( spl15_245
<=> tail_of(sK10) = head_of(sK11) ),
introduced(definition,[new_symbols(definition,[spl15_245])],[avatar_definition]) ).
fof(f3466,plain,
( tail_of(sK10) != head_of(sK11)
| spl15_245 ),
inference(avatar_component_clause,[],[f3464]) ).
fof(f3468,definition,
( spl15_246
<=> sK10 = sK11 ),
introduced(definition,[new_symbols(definition,[spl15_246])],[avatar_definition]) ).
fof(f3470,plain,
( sK10 = sK11
| ~ spl15_246 ),
inference(avatar_component_clause,[],[f3468]) ).
fof(f3471,plain,
( ~ spl15_245
| spl15_246
| ~ spl15_16
| ~ spl15_22
| spl15_25 ),
inference(avatar_split_clause,[],[f3278,f295,f278,f224,f3468,f3464]) ).
fof(f3498,plain,
( head_of(sK11) != head_of(sK11)
| tail_of(sK10) != tail_of(sK11)
| ~ spl15_1 ),
inference(resolution,[],[f141,f438]) ).
fof(f3499,plain,
( tail_of(sK10) != tail_of(sK11)
| ~ spl15_1 ),
inference(trivial_inequality_removal,[],[f3498]) ).
fof(f3527,plain,
( $false
| ~ spl15_26 ),
inference(resolution,[],[f300,f125]) ).
fof(f3533,plain,
~ spl15_26,
inference(avatar_contradiction_clause,[],[f3527]) ).
fof(f3969,plain,
( head_of(sK11) != head_of(sK13)
| tail_of(sK10) != tail_of(sK13)
| ~ spl15_1
| ~ spl15_8 ),
inference(resolution,[],[f173,f141]) ).
fof(f3997,plain,
( ~ spl15_7
| ~ spl15_6
| ~ spl15_1
| ~ spl15_8 ),
inference(avatar_split_clause,[],[f3969,f171,f140,f161,f166]) ).
fof(f4259,plain,
( tail_of(sK10) != tail_of(sK10)
| ~ spl15_1
| ~ spl15_246 ),
inference(superposition,[],[f3499,f3470]) ).
fof(f4261,plain,
( $false
| ~ spl15_1
| ~ spl15_246 ),
inference(trivial_inequality_removal,[],[f4259]) ).
fof(f4262,plain,
( ~ spl15_1
| ~ spl15_246 ),
inference(avatar_contradiction_clause,[],[f4261]) ).
fof(f13053,plain,
( head_of(sK11) = head_of(sK0(tail_of(sK10),head_of(sK11)))
| head_of(sK11) = tail_of(sK0(tail_of(sK10),head_of(sK11)))
| tail_of(sK10) = head_of(sK11)
| ~ spl15_12
| ~ spl15_16 ),
inference(resolution,[],[f1460,f436]) ).
fof(f13063,plain,
( head_of(sK11) = head_of(sK0(tail_of(sK10),head_of(sK11)))
| head_of(sK11) = tail_of(sK0(tail_of(sK10),head_of(sK11)))
| ~ spl15_12
| ~ spl15_16
| spl15_245 ),
inference(forward_subsumption_resolution,[],[f13053,f3466]) ).
fof(f13085,definition,
( spl15_1073
<=> head_of(sK11) = tail_of(sK0(tail_of(sK10),head_of(sK11))) ),
introduced(definition,[new_symbols(definition,[spl15_1073])],[avatar_definition]) ).
fof(f13089,definition,
( spl15_1074
<=> head_of(sK11) = head_of(sK0(tail_of(sK10),head_of(sK11))) ),
introduced(definition,[new_symbols(definition,[spl15_1074])],[avatar_definition]) ).
fof(f13092,plain,
( spl15_1073
| spl15_1074
| ~ spl15_12
| ~ spl15_16
| spl15_245 ),
inference(avatar_split_clause,[],[f13063,f3464,f224,f188,f13089,f13085]) ).
fof(f13315,plain,
( tail_of(sK10) = tail_of(sK0(tail_of(sK10),head_of(sK11)))
| head_of(sK11) = tail_of(sK0(tail_of(sK10),head_of(sK11)))
| tail_of(sK10) = head_of(sK11)
| ~ spl15_10
| ~ spl15_16 ),
inference(resolution,[],[f1513,f436]) ).
fof(f13326,plain,
( tail_of(sK10) = tail_of(sK0(tail_of(sK10),head_of(sK11)))
| head_of(sK11) = tail_of(sK0(tail_of(sK10),head_of(sK11)))
| ~ spl15_10
| ~ spl15_16
| spl15_245 ),
inference(forward_subsumption_resolution,[],[f13315,f3466]) ).
fof(f13344,definition,
( spl15_1091
<=> tail_of(sK10) = tail_of(sK0(tail_of(sK10),head_of(sK11))) ),
introduced(definition,[new_symbols(definition,[spl15_1091])],[avatar_definition]) ).
fof(f13347,plain,
( spl15_1073
| spl15_1091
| ~ spl15_10
| ~ spl15_16
| spl15_245 ),
inference(avatar_split_clause,[],[f13326,f3464,f224,f180,f13344,f13085]) ).
fof(f13401,plain,
( head_of(sK11) = head_of(sK0(tail_of(sK10),head_of(sK11)))
| tail_of(sK10) = head_of(sK0(tail_of(sK10),head_of(sK11)))
| tail_of(sK10) = head_of(sK11)
| ~ spl15_13
| ~ spl15_16 ),
inference(resolution,[],[f1548,f436]) ).
fof(f13412,plain,
( head_of(sK11) = head_of(sK0(tail_of(sK10),head_of(sK11)))
| tail_of(sK10) = head_of(sK0(tail_of(sK10),head_of(sK11)))
| ~ spl15_13
| ~ spl15_16
| spl15_245 ),
inference(forward_subsumption_resolution,[],[f13401,f3466]) ).
fof(f13430,definition,
( spl15_1101
<=> tail_of(sK10) = head_of(sK0(tail_of(sK10),head_of(sK11))) ),
introduced(definition,[new_symbols(definition,[spl15_1101])],[avatar_definition]) ).
fof(f13433,plain,
( spl15_1101
| spl15_1074
| ~ spl15_13
| ~ spl15_16
| spl15_245 ),
inference(avatar_split_clause,[],[f13412,f3464,f224,f192,f13089,f13430]) ).
fof(f13550,plain,
( tail_of(sK10) = tail_of(sK0(tail_of(sK10),head_of(sK11)))
| tail_of(sK10) = head_of(sK0(tail_of(sK10),head_of(sK11)))
| tail_of(sK10) = head_of(sK11)
| ~ spl15_11
| ~ spl15_16 ),
inference(resolution,[],[f1650,f436]) ).
fof(f13560,plain,
( tail_of(sK10) = tail_of(sK0(tail_of(sK10),head_of(sK11)))
| tail_of(sK10) = head_of(sK0(tail_of(sK10),head_of(sK11)))
| ~ spl15_11
| ~ spl15_16
| spl15_245 ),
inference(forward_subsumption_resolution,[],[f13550,f3466]) ).
fof(f13565,plain,
( spl15_1101
| spl15_1091
| ~ spl15_11
| ~ spl15_16
| spl15_245 ),
inference(avatar_split_clause,[],[f13560,f3464,f224,f184,f13344,f13430]) ).
fof(f20418,definition,
( spl15_1662
<=> edge(sK0(tail_of(sK10),head_of(sK11))) ),
introduced(definition,[new_symbols(definition,[spl15_1662])],[avatar_definition]) ).
fof(f20419,plain,
( edge(sK0(tail_of(sK10),head_of(sK11)))
| ~ spl15_1662 ),
inference(avatar_component_clause,[],[f20418]) ).
fof(f20420,plain,
( ~ edge(sK0(tail_of(sK10),head_of(sK11)))
| spl15_1662 ),
inference(avatar_component_clause,[],[f20418]) ).
fof(f20566,plain,
( tail_of(sK10) = head_of(sK11)
| ~ vertex(head_of(sK11))
| ~ vertex(tail_of(sK10))
| ~ spl15_15
| spl15_1662 ),
inference(resolution,[],[f20420,f201]) ).
fof(f20567,plain,
( ~ vertex(head_of(sK11))
| ~ vertex(tail_of(sK10))
| ~ spl15_15
| spl15_245
| spl15_1662 ),
inference(forward_subsumption_resolution,[],[f20566,f3466]) ).
fof(f20568,plain,
( ~ vertex(tail_of(sK10))
| ~ spl15_15
| spl15_245
| spl15_1662 ),
inference(forward_subsumption_resolution,[],[f20567,f436]) ).
fof(f20569,plain,
( $false
| ~ spl15_15
| ~ spl15_22
| spl15_245
| spl15_1662 ),
inference(forward_subsumption_resolution,[],[f20568,f504]) ).
fof(f20570,plain,
( ~ spl15_15
| ~ spl15_22
| spl15_245
| spl15_1662 ),
inference(avatar_contradiction_clause,[],[f20569]) ).
fof(f20572,plain,
( head_of(sK11) != head_of(sK0(tail_of(sK10),head_of(sK11)))
| tail_of(sK10) != tail_of(sK0(tail_of(sK10),head_of(sK11)))
| ~ spl15_1
| ~ spl15_1662 ),
inference(resolution,[],[f20419,f141]) ).
fof(f20573,plain,
( tail_of(sK10) != head_of(sK0(tail_of(sK10),head_of(sK11)))
| head_of(sK11) != tail_of(sK0(tail_of(sK10),head_of(sK11)))
| ~ spl15_5
| ~ spl15_1662 ),
inference(resolution,[],[f20419,f159]) ).
fof(f20826,plain,
( ~ spl15_1091
| ~ spl15_1074
| ~ spl15_1
| ~ spl15_1662 ),
inference(avatar_split_clause,[],[f20572,f20418,f140,f13089,f13344]) ).
fof(f20827,plain,
( ~ spl15_1073
| ~ spl15_1101
| ~ spl15_5
| ~ spl15_1662 ),
inference(avatar_split_clause,[],[f20573,f20418,f158,f13430,f13085]) ).
cnf(s1,plain,
( spl15_1
| spl15_2 ),
inference(sat_conversion,[],[f146]) ).
cnf(s2,plain,
( spl15_1
| spl15_3 ),
inference(sat_conversion,[],[f151]) ).
cnf(s3,plain,
( spl15_1
| spl15_4 ),
inference(sat_conversion,[],[f156]) ).
cnf(s4,plain,
( spl15_5
| spl15_6 ),
inference(sat_conversion,[],[f164]) ).
cnf(s5,plain,
( spl15_5
| spl15_7 ),
inference(sat_conversion,[],[f169]) ).
cnf(s6,plain,
( spl15_5
| spl15_8 ),
inference(sat_conversion,[],[f174]) ).
cnf(s7,plain,
( ~ spl15_9
| spl15_10 ),
inference(sat_conversion,[],[f182]) ).
cnf(s8,plain,
( ~ spl15_9
| spl15_11 ),
inference(sat_conversion,[],[f186]) ).
cnf(s9,plain,
( ~ spl15_9
| spl15_12 ),
inference(sat_conversion,[],[f190]) ).
cnf(s10,plain,
( ~ spl15_9
| spl15_13 ),
inference(sat_conversion,[],[f194]) ).
cnf(s12,plain,
( ~ spl15_9
| spl15_15 ),
inference(sat_conversion,[],[f202]) ).
cnf(s13,plain,
spl15_9,
inference(sat_conversion,[],[f203]) ).
cnf(s15,plain,
( ~ spl15_2
| ~ spl15_3
| ~ spl15_4
| ~ spl15_5 ),
inference(sat_conversion,[],[f217]) ).
cnf(s22,plain,
( ~ spl15_25
| spl15_26 ),
inference(sat_conversion,[],[f301]) ).
cnf(s31,plain,
spl15_22,
inference(sat_conversion,[],[f495]) ).
cnf(s35,plain,
( spl15_16
| ~ spl15_22 ),
inference(sat_conversion,[],[f518]) ).
cnf(s229,plain,
( ~ spl15_2
| ~ spl15_6
| ~ spl15_7 ),
inference(sat_conversion,[],[f3393]) ).
cnf(s251,plain,
( ~ spl15_16
| ~ spl15_22
| spl15_25
| ~ spl15_245
| spl15_246 ),
inference(sat_conversion,[],[f3471]) ).
cnf(s256,plain,
~ spl15_26,
inference(sat_conversion,[],[f3533]) ).
cnf(s324,plain,
( ~ spl15_1
| ~ spl15_6
| ~ spl15_7
| ~ spl15_8 ),
inference(sat_conversion,[],[f3997]) ).
cnf(s354,plain,
( ~ spl15_1
| ~ spl15_246 ),
inference(sat_conversion,[],[f4262]) ).
cnf(s1271,plain,
( ~ spl15_12
| ~ spl15_16
| spl15_245
| spl15_1073
| spl15_1074 ),
inference(sat_conversion,[],[f13092]) ).
cnf(s1302,plain,
( ~ spl15_10
| ~ spl15_16
| spl15_245
| spl15_1073
| spl15_1091 ),
inference(sat_conversion,[],[f13347]) ).
cnf(s1312,plain,
( ~ spl15_13
| ~ spl15_16
| spl15_245
| spl15_1074
| spl15_1101 ),
inference(sat_conversion,[],[f13433]) ).
cnf(s1335,plain,
( ~ spl15_11
| ~ spl15_16
| spl15_245
| spl15_1091
| spl15_1101 ),
inference(sat_conversion,[],[f13565]) ).
cnf(s1918,plain,
( ~ spl15_15
| ~ spl15_22
| spl15_245
| spl15_1662 ),
inference(sat_conversion,[],[f20570]) ).
cnf(s1974,plain,
( ~ spl15_1
| ~ spl15_1074
| ~ spl15_1091
| ~ spl15_1662 ),
inference(sat_conversion,[],[f20826]) ).
cnf(s1975,plain,
( ~ spl15_5
| ~ spl15_1073
| ~ spl15_1101
| ~ spl15_1662 ),
inference(sat_conversion,[],[f20827]) ).
cnf(s2132,plain,
spl15_16,
inference(rat,[],[s35,s31]) ).
cnf(s2144,plain,
~ spl15_25,
inference(rat,[],[s22,s256]) ).
cnf(s2147,plain,
spl15_15,
inference(rat,[],[s12,s13]) ).
cnf(s2152,plain,
spl15_13,
inference(rat,[],[s10,s13]) ).
cnf(s2153,plain,
spl15_12,
inference(rat,[],[s9,s13]) ).
cnf(s2154,plain,
spl15_11,
inference(rat,[],[s8,s13]) ).
cnf(s2155,plain,
spl15_10,
inference(rat,[],[s7,s13]) ).
cnf(s2156,plain,
( ~ spl15_4
| ~ spl15_3
| ~ spl15_2 ),
inference(rat,[],[s229,s4,s5,s15]) ).
cnf(s2157,plain,
spl15_1,
inference(rat,[],[s2156,s1,s2,s3]) ).
cnf(s2158,plain,
~ spl15_246,
inference(rat,[],[s354,s2157]) ).
cnf(s2160,plain,
~ spl15_245,
inference(rat,[],[s251,s2144,s2132,s31,s2158]) ).
cnf(s2162,plain,
spl15_1662,
inference(rat,[],[s1918,s2147,s31,s2160]) ).
cnf(s2163,plain,
spl15_5,
inference(rat,[],[s324,s4,s5,s6,s2157]) ).
cnf(s2164,plain,
spl15_1073,
inference(rat,[],[s1974,s1302,s1271,s2157,s2162,s2132,s2155,s2160,s2153]) ).
cnf(s2165,plain,
~ spl15_1101,
inference(rat,[],[s1975,s2162,s2163,s2164]) ).
cnf(s2166,plain,
spl15_1091,
inference(rat,[],[s1335,s2160,s2154,s2132,s2165]) ).
cnf(s2167,plain,
spl15_1074,
inference(rat,[],[s1312,s2160,s2152,s2132,s2165]) ).
cnf(s2168,plain,
$false,
inference(rat,[],[s1974,s2162,s2157,s2166,s2167]) ).
fof(f21399,plain,
$false,
inference(avatar_sat_refutation,[],[s2168]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA006+1 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n015.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 08:50:45 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.62/2.52 % (1355759)Will run a generic schedule for satisfiability detection.
% 14.62/2.52 % (1355769)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3231001030:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.62/2.52 % (1355765)% WARNING: option uhcvi not known.
% 14.62/2.52 % (1355764)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=75781964_2999 on theBenchmark for (2999ds/0Mi)
% 14.62/2.52 % (1355765)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=937643037:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.62/2.52 % (1355766)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1920519213:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.62/2.52 % (1355767)dis+10_1_sil=32000:sp=arity:random_seed=1662296963:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.62/2.52 % (1355768)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=439258066:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.62/2.52 % (1355770)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1547118655:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.62/2.52 % TRYING [1]
% 14.62/2.52 % TRYING [2]
% 14.62/2.52 % TRYING [3]
% 14.62/2.52 % TRYING [4]
% 14.62/2.52 % (1355769)Instruction limit reached!
% 14.62/2.52 % (1355769)------------------------------
% 14.62/2.52 % (1355769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.62/2.52 % (1355769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.62/2.52 % (1355769)CaDiCaL version: 2.1.3
% 14.62/2.52 % (1355769)Termination reason: Instruction limit
% 14.62/2.52 % (1355769)Termination phase: Saturation
% 14.62/2.52 % (1355769)Time elapsed: 0.042 s
% 14.62/2.52 % (1355769)Peak memory usage: 13 MB
% 14.62/2.52 % (1355769)Instructions burned: 134 (million)
% 14.62/2.52 % (1355778)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3223802735:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.62/2.52 % TRYING [1]
% 14.62/2.52 % TRYING [2]
% 14.62/2.52 % TRYING [3]
% 14.62/2.52 % (1355767)Instruction limit reached!
% 14.62/2.52 % (1355767)------------------------------
% 14.62/2.52 % (1355767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.62/2.52 % (1355767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.62/2.53 % (1355767)CaDiCaL version: 2.1.3
% 14.62/2.53 % (1355767)Termination reason: Instruction limit
% 14.62/2.53 % (1355767)Termination phase: Saturation
% 14.62/2.53 % (1355767)Time elapsed: 0.064 s
% 14.62/2.53 % (1355767)Peak memory usage: 13 MB
% 14.62/2.53 % (1355767)Instructions burned: 104 (million)
% 14.62/2.53 % (1355768)Instruction limit reached!
% 14.62/2.53 % (1355768)------------------------------
% 14.62/2.53 % (1355768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.62/2.53 % (1355768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.62/2.53 % (1355768)CaDiCaL version: 2.1.3
% 14.62/2.53 % (1355768)Termination reason: Instruction limit
% 14.62/2.53 % (1355768)Termination phase: Saturation
% 14.62/2.53 % (1355768)Time elapsed: 0.070 s
% 14.62/2.53 % (1355768)Peak memory usage: 13 MB
% 14.62/2.53 % (1355768)Instructions burned: 117 (million)
% 14.62/2.53 % TRYING [5]
% 14.62/2.53 % (1355780)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4137005112:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.62/2.53 % (1355781)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=203931605:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.62/2.53 % (1355770)Instruction limit reached!
% 14.62/2.53 % (1355770)------------------------------
% 14.62/2.53 % (1355770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.62/2.53 % (1355770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.62/2.53 % (1355770)CaDiCaL version: 2.1.3
% 14.62/2.53 % (1355770)Termination reason: Instruction limit
% 14.62/2.53 % (1355770)Termination phase: Saturation
% 14.62/2.53 % (1355770)Time elapsed: 0.099 s
% 14.62/2.53 % (1355770)Peak memory usage: 15 MB
% 14.62/2.53 % (1355770)Instructions burned: 160 (million)
% 14.62/2.53 % TRYING [4]
% 14.62/2.53 % (1355784)ott-21_1_sil=16000:fs=off:random_seed=3881318028:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.62/2.53 % (1355780)Instruction limit reached!
% 14.62/2.53 % (1355780)------------------------------
% 14.62/2.53 % (1355780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.87/6.27 % (1355780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.87/6.27 % (1355780)CaDiCaL version: 2.1.3
% 40.87/6.27 % (1355780)Termination reason: Instruction limit
% 40.87/6.27 % (1355780)Termination phase: Saturation
% 40.87/6.27 % (1355780)Time elapsed: 0.083 s
% 40.87/6.27 % (1355780)Peak memory usage: 13 MB
% 40.87/6.27 % (1355780)Instructions burned: 132 (million)
% 40.87/6.27 % TRYING [6]
% 40.87/6.27 % (1355786)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3177383555:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 40.87/6.27 % (1355784)Instruction limit reached!
% 40.87/6.27 % (1355784)------------------------------
% 40.87/6.27 % (1355784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.87/6.27 % (1355784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.87/6.27 % (1355784)CaDiCaL version: 2.1.3
% 40.87/6.27 % (1355784)Termination reason: Instruction limit
% 40.87/6.27 % (1355784)Termination phase: Saturation
% 40.87/6.27 % (1355784)Time elapsed: 0.096 s
% 40.87/6.27 % (1355784)Peak memory usage: 12 MB
% 40.87/6.27 % (1355784)Instructions burned: 180 (million)
% 40.87/6.27 % (1355788)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=94370976:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 40.87/6.27 % TRYING [1]
% 40.87/6.27 % TRYING [2]
% 40.87/6.27 % TRYING [3]
% 40.87/6.27 % (1355778)Instruction limit reached!
% 40.87/6.27 % (1355778)------------------------------
% 40.87/6.27 % (1355778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.87/6.27 % (1355778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.87/6.27 % (1355778)CaDiCaL version: 2.1.3
% 40.87/6.27 % (1355778)Termination reason: Instruction limit
% 40.87/6.27 % (1355778)Termination phase: Finite model building SAT solving
% 40.87/6.27 % (1355778)Time elapsed: 0.218 s
% 40.87/6.27 % (1355778)Peak memory usage: 17 MB
% 40.87/6.27 % (1355778)Instructions burned: 719 (million)
% 40.87/6.27 % (1355790)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1563178852:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 40.87/6.27 % TRYING [4]
% 40.87/6.27 % TRYING [5]
% 40.87/6.27 % TRYING [7]
% 40.87/6.27 % (1355781)Instruction limit reached!
% 40.87/6.27 % (1355781)------------------------------
% 40.87/6.27 % (1355781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.87/6.27 % (1355781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.87/6.27 % (1355781)CaDiCaL version: 2.1.3
% 40.87/6.27 % (1355781)Termination reason: Instruction limit
% 40.87/6.27 % (1355781)Termination phase: Saturation
% 40.87/6.27 % (1355781)Time elapsed: 0.375 s
% 40.87/6.27 % (1355781)Peak memory usage: 20 MB
% 40.87/6.27 % (1355781)Instructions burned: 684 (million)
% 40.87/6.27 % (1355792)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2550904488:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 40.87/6.27 % (1355786)Instruction limit reached!
% 40.87/6.27 % (1355786)------------------------------
% 40.87/6.27 % (1355786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.87/6.27 % (1355786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.87/6.27 % (1355786)CaDiCaL version: 2.1.3
% 40.87/6.27 % (1355786)Termination reason: Instruction limit
% 40.87/6.27 % (1355786)Termination phase: Saturation
% 40.87/6.27 % (1355786)Time elapsed: 0.316 s
% 40.87/6.27 % (1355786)Peak memory usage: 14 MB
% 40.87/6.27 % (1355786)Instructions burned: 479 (million)
% 40.87/6.27 % (1355794)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1311719998:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 40.87/6.27 % (1355788)Instruction limit reached!
% 40.87/6.27 % (1355788)------------------------------
% 40.87/6.27 % (1355788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.87/6.27 % (1355788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.87/6.27 % (1355788)CaDiCaL version: 2.1.3
% 40.87/6.27 % (1355788)Termination reason: Instruction limit
% 40.87/6.27 % (1355788)Termination phase: Finite model building SAT solving
% 40.87/6.27 % (1355788)Time elapsed: 0.354 s
% 40.87/6.27 % (1355788)Peak memory usage: 20 MB
% 40.87/6.27 % (1355788)Instructions burned: 866 (million)
% 40.87/6.27 % (1355796)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1104402650:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 40.87/6.27 % (1355790)Instruction limit reached!
% 40.87/6.27 % (1355790)------------------------------
% 43.44/6.68 % (1355790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355790)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355790)Termination reason: Instruction limit
% 43.44/6.68 % (1355790)Termination phase: Saturation
% 43.44/6.68 % (1355790)Time elapsed: 0.341 s
% 43.44/6.68 % (1355790)Peak memory usage: 21 MB
% 43.44/6.68 % (1355790)Instructions burned: 1180 (million)
% 43.44/6.68 % TRYING [14]
% 43.44/6.68 % (1355798)fmb+10_1_sil=64000:random_seed=4020185539:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 43.44/6.68 % TRYING [1]
% 43.44/6.68 % TRYING [2]
% 43.44/6.68 % TRYING [3]
% 43.44/6.68 % TRYING [4]
% 43.44/6.68 % TRYING [5]
% 43.44/6.68 % TRYING [6]
% 43.44/6.68 % (1355792)Instruction limit reached!
% 43.44/6.68 % (1355792)------------------------------
% 43.44/6.68 % (1355792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355792)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355792)Termination reason: Instruction limit
% 43.44/6.68 % (1355792)Termination phase: Finite model building constraint generation
% 43.44/6.68 % (1355792)Time elapsed: 0.326 s
% 43.44/6.68 % (1355792)Peak memory usage: 71 MB
% 43.44/6.68 % (1355792)Instructions burned: 889 (million)
% 43.44/6.68 % (1355800)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=304102538:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 43.44/6.68 % TRYING [7]
% 43.44/6.68 % TRYING [20]
% 43.44/6.68 % (1355794)Instruction limit reached!
% 43.44/6.68 % (1355794)------------------------------
% 43.44/6.68 % (1355794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355794)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355794)Termination reason: Instruction limit
% 43.44/6.68 % (1355794)Termination phase: Saturation
% 43.44/6.68 % (1355794)Time elapsed: 0.338 s
% 43.44/6.68 % (1355794)Peak memory usage: 16 MB
% 43.44/6.68 % (1355794)Instructions burned: 692 (million)
% 43.44/6.68 % (1355802)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=461638915:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 43.44/6.68 % TRYING [8]
% 43.44/6.68 % TRYING [8]
% 43.44/6.68 % TRYING [8]
% 43.44/6.68 % (1355796)Instruction limit reached!
% 43.44/6.68 % (1355796)------------------------------
% 43.44/6.68 % (1355796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355796)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355796)Termination reason: Instruction limit
% 43.44/6.68 % (1355796)Termination phase: Saturation
% 43.44/6.68 % (1355796)Time elapsed: 0.515 s
% 43.44/6.68 % (1355796)Peak memory usage: 19 MB
% 43.44/6.68 % (1355796)Instructions burned: 879 (million)
% 43.44/6.68 % (1355804)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2283161647:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 43.44/6.68 % (1355802)Instruction limit reached!
% 43.44/6.68 % (1355802)------------------------------
% 43.44/6.68 % (1355802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355802)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355802)Termination reason: Instruction limit
% 43.44/6.68 % (1355802)Termination phase: Finite model building constraint generation
% 43.44/6.68 % (1355802)Time elapsed: 0.353 s
% 43.44/6.68 % (1355802)Peak memory usage: 64 MB
% 43.44/6.68 % (1355802)Instructions burned: 921 (million)
% 43.44/6.68 % (1355806)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2879956126:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 43.44/6.68 % TRYING [9]
% 43.44/6.68 % TRYING [9]
% 43.44/6.68 % (1355806)Instruction limit reached!
% 43.44/6.68 % (1355806)------------------------------
% 43.44/6.68 % (1355806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355806)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355806)Termination reason: Instruction limit
% 43.44/6.68 % (1355806)Termination phase: Saturation
% 43.44/6.68 % (1355806)Time elapsed: 0.772 s
% 43.44/6.68 % (1355806)Peak memory usage: 25 MB
% 43.44/6.68 % (1355806)Instructions burned: 1473 (million)
% 43.44/6.68 % (1355808)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=239944452:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 43.44/6.68 % TRYING [77]
% 43.44/6.68 % TRYING [10]
% 43.44/6.68 % TRYING [10]
% 43.44/6.68 % TRYING [11]
% 43.44/6.68 % (1355804)Instruction limit reached!
% 43.44/6.68 % (1355804)------------------------------
% 43.44/6.68 % (1355804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355804)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355804)Termination reason: Instruction limit
% 43.44/6.68 % (1355804)Termination phase: Saturation
% 43.44/6.68 % (1355804)Time elapsed: 2.626 s
% 43.44/6.68 % (1355804)Peak memory usage: 24 MB
% 43.44/6.68 % (1355804)Instructions burned: 5131 (million)
% 43.44/6.68 % (1355812)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3687298678:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 43.44/6.68 % TRYING [16]
% 43.44/6.68 % (1355808)Instruction limit reached!
% 43.44/6.68 % (1355808)------------------------------
% 43.44/6.68 % (1355808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355808)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355808)Termination reason: Instruction limit
% 43.44/6.68 % (1355808)Termination phase: Finite model building constraint generation
% 43.44/6.68 % (1355808)Time elapsed: 2.307 s
% 43.44/6.68 % (1355808)Peak memory usage: 447 MB
% 43.44/6.68 % (1355808)Instructions burned: 6326 (million)
% 43.44/6.68 % (1355814)ott-2_1_sil=16000:newcnf=on:random_seed=1950821054:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 43.44/6.68 % (1355812)Instruction limit reached!
% 43.44/6.68 % (1355812)------------------------------
% 43.44/6.68 % (1355812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355812)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355812)Termination reason: Instruction limit
% 43.44/6.68 % (1355812)Termination phase: Finite model building constraint generation
% 43.44/6.68 % (1355812)Time elapsed: 0.720 s
% 43.44/6.68 % (1355812)Peak memory usage: 126 MB
% 43.44/6.68 % (1355812)Instructions burned: 2175 (million)
% 43.44/6.68 % (1355816)ott+10_1_sil=32000:tgt=ground:random_seed=2988309778:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 43.44/6.68 % (1355814)Instruction limit reached!
% 43.44/6.68 % (1355814)------------------------------
% 43.44/6.68 % (1355814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355814)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355814)Termination reason: Instruction limit
% 43.44/6.68 % (1355814)Termination phase: Saturation
% 43.44/6.68 % (1355814)Time elapsed: 0.485 s
% 43.44/6.68 % (1355814)Peak memory usage: 18 MB
% 43.44/6.68 % (1355814)Instructions burned: 871 (million)
% 43.44/6.68 % (1355818)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=43193875:i=54282_2950 on theBenchmark for (2950ds/54282Mi)
% 43.44/6.68 % TRYING [1]
% 43.44/6.68 % TRYING [2]
% 43.44/6.68 % TRYING [3]
% 43.44/6.68 % TRYING [4]
% 43.44/6.68 % TRYING [5]
% 43.44/6.68 % TRYING [6]
% 43.44/6.68 % (1355800)Instruction limit reached!
% 43.44/6.68 % (1355800)------------------------------
% 43.44/6.68 % (1355800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355800)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355800)Termination reason: Instruction limit
% 43.44/6.68 % (1355800)Termination phase: Finite model building constraint generation
% 43.44/6.68 % (1355800)Time elapsed: 4.440 s
% 43.44/6.68 % (1355800)Peak memory usage: 848 MB
% 43.44/6.68 % (1355800)Instructions burned: 9515 (million)
% 43.44/6.68 % (1355820)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3267192369:i=3512:aac=none_2945 on theBenchmark for (2945ds/3512Mi)
% 43.44/6.68 % TRYING [7]
% 43.44/6.68 % TRYING [11]
% 43.44/6.68 % (1355798)Instruction limit reached!
% 43.44/6.68 % (1355798)------------------------------
% 43.44/6.68 % (1355798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355798)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355798)Termination reason: Instruction limit
% 43.44/6.68 % (1355798)Termination phase: Finite model building SAT solving
% 43.44/6.68 % (1355798)Time elapsed: 5.177 s
% 43.44/6.68 % (1355798)Peak memory usage: 160 MB
% 43.44/6.68 % (1355798)Instructions burned: 22061 (million)
% 43.44/6.68 % (1355822)dis+21_1_sil=32000:sas=cadical:random_seed=2869144219:i=3773:amm=off_2941 on theBenchmark for (2941ds/3773Mi)
% 43.44/6.68 % TRYING [8]
% 43.44/6.68 % (1355822) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1355759-1355822"...
% 43.44/6.68 % (1355822)...printing done.
% 43.44/6.68 % (1355822)Refutation found. Thanks to Tanya!
% 43.44/6.68 % SZS status Theorem for theBenchmark
% 43.44/6.68 % SZS output start Proof for theBenchmark
% See solution above
% 43.44/6.68 % (1355822)------------------------------
% 43.44/6.68 % (1355822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.44/6.68 % (1355822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/6.68 % (1355822)CaDiCaL version: 2.1.3
% 43.44/6.68 % (1355822)Termination reason: Refutation
% 43.44/6.68 % (1355822)Time elapsed: 0.348 s
% 43.44/6.68 % (1355822)Peak memory usage: 22 MB
% 43.44/6.68 % (1355822)Instructions burned: 1187 (million)
% 43.44/6.68 % (1355759)Success in time 6.246 s
% 43.44/6.68 % Vampire exiting
%------------------------------------------------------------------------------