%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRA009+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.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 09:55:21 AM UTC 2026
% Result : Theorem 5.58s 1.91s
% Output : Refutation 8.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 32
% Syntax : Number of formulae : 250 ( 40 unt; 22 def)
% Number of atoms : 885 ( 210 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 1066 ( 431 ~; 475 |; 116 &)
% ( 26 <=>; 15 =>; 0 <=; 3 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 24 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-3 aty)
% Number of variables : 287 ( 0 sgn 262 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( edge(X0)
=> head_of(X0) != tail_of(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_loops) ).
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/theBenchmark.p',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/theBenchmark.p',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/theBenchmark.p',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/theBenchmark.p',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/theBenchmark.p',precedes_defn) ).
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/theBenchmark.p',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/theBenchmark.p',shortest_path_properties) ).
fof(f13,axiom,
! [X0,X1,X2] :
( triangle(X0,X1,X2)
<=> ( edge(X0)
& edge(X1)
& edge(X2)
& sequential(X0,X1)
& sequential(X1,X2)
& sequential(X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',triangle_defn) ).
fof(f18,conjecture,
( complete
=> ! [X0,X1,X2] :
( shortest_path(X1,X2,X0)
=> ! [X3,X4] :
( ( on_path(X3,X0)
& on_path(X4,X0)
& sequential(X3,X4) )
=> ? [X5] : triangle(X3,X4,X5) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complete_means_path_means_stuff_means_triangles) ).
fof(f19,negated_conjecture,
~ ( complete
=> ! [X0,X1,X2] :
( shortest_path(X1,X2,X0)
=> ! [X3,X4] :
( ( on_path(X3,X0)
& on_path(X4,X0)
& sequential(X3,X4) )
=> ? [X5] : triangle(X3,X4,X5) ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f24,plain,
( ? [X0,X1,X2] :
( ? [X3,X4] :
( ! [X5] : ~ triangle(X3,X4,X5)
& on_path(X3,X0)
& on_path(X4,X0)
& sequential(X3,X4) )
& shortest_path(X1,X2,X0) )
& complete ),
inference(ennf_transformation,[],[f19]) ).
fof(f25,plain,
( ? [X0,X1,X2] :
( ? [X3,X4] :
( ! [X5] : ~ triangle(X3,X4,X5)
& on_path(X3,X0)
& on_path(X4,X0)
& sequential(X3,X4) )
& shortest_path(X1,X2,X0) )
& complete ),
inference(flattening,[],[f24]) ).
fof(f26,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(f27,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,[],[f26]) ).
fof(f31,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(f32,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,[],[f31]) ).
fof(f34,plain,
! [X0] :
( head_of(X0) != tail_of(X0)
| ~ edge(X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f36,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(f37,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,[],[f36]) ).
fof(f38,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(f39,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(f40,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,[],[f39]) ).
fof(f41,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(f42,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,[],[f41]) ).
fof(f43,plain,
! [X0,X1,X2] :
( ( triangle(X0,X1,X2)
| ~ edge(X0)
| ~ edge(X1)
| ~ edge(X2)
| ~ sequential(X0,X1)
| ~ sequential(X1,X2)
| ~ sequential(X2,X0) )
& ( ( edge(X0)
& edge(X1)
& edge(X2)
& sequential(X0,X1)
& sequential(X1,X2)
& sequential(X2,X0) )
| ~ triangle(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f44,plain,
! [X0,X1,X2] :
( ( triangle(X0,X1,X2)
| ~ edge(X0)
| ~ edge(X1)
| ~ edge(X2)
| ~ sequential(X0,X1)
| ~ sequential(X1,X2)
| ~ sequential(X2,X0) )
& ( ( edge(X0)
& edge(X1)
& edge(X2)
& sequential(X0,X1)
& sequential(X1,X2)
& sequential(X2,X0) )
| ~ triangle(X0,X1,X2) ) ),
inference(flattening,[],[f43]) ).
fof(f46,plain,
( ! [X5] : ~ triangle(sK5,sK6,X5)
& on_path(sK5,sK2)
& on_path(sK6,sK2)
& sequential(sK5,sK6)
& shortest_path(sK3,sK4,sK2)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6)],[f25]) ).
fof(f47,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(f48,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,[],[f47]) ).
fof(f53,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,[],[f32]) ).
fof(f54,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,[],[f53]) ).
fof(f55,plain,
( ! [X0,X1] :
( ( edge(sK9(X0,X1))
& ( head_of(sK9(X0,X1)) != X1
| tail_of(sK9(X0,X1)) != X0
| head_of(sK9(X0,X1)) != X0
| tail_of(sK9(X0,X1)) != X1 )
& ( ( head_of(sK9(X0,X1)) = X1
& tail_of(sK9(X0,X1)) = X0 )
| ( head_of(sK9(X0,X1)) = X0
& tail_of(sK9(X0,X1)) = X1 ) ) )
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1 )
| ~ complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X2,sK9(X0,X1))],[f54]) ).
fof(f60,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,[],[f38]) ).
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(flattening,[],[f60]) ).
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
& ! [X4] :
( less_or_equal(length_of(X2),length_of(X4))
| ~ path(X0,X1,X4) ) )
| ~ shortest_path(X0,X1,X2) ) ),
inference(rectify,[],[f61]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ( shortest_path(X0,X1,X2)
| ~ path(X0,X1,X2)
| X0 = X1
| ( ~ less_or_equal(length_of(X2),length_of(sK11(X0,X1,X2)))
& path(X0,X1,sK11(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,[sK11]),skolemize(X3,sK11(X0,X1,X2))],[f62]) ).
fof(f64,plain,
! [X0,X1,X2,X3] :
( ( vertex(X3)
& on_path(sK12(X2,X3),X2)
& ( head_of(sK12(X2,X3)) = X3
| tail_of(sK12(X2,X3)) = X3 ) )
| ~ path(X0,X1,X2)
| ~ in_path(X3,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X4,sK12(X2,X3))],[f40]) ).
fof(f71,plain,
! [X2,X0,X1] :
( triangle(X0,X1,X2)
| ~ edge(X0)
| ~ edge(X1)
| ~ edge(X2)
| ~ sequential(X0,X1)
| ~ sequential(X1,X2)
| ~ sequential(X2,X0) ),
inference(cnf_transformation,[],[f44]) ).
fof(f79,plain,
complete,
inference(cnf_transformation,[],[f46]) ).
fof(f80,plain,
shortest_path(sK3,sK4,sK2),
inference(cnf_transformation,[],[f46]) ).
fof(f81,plain,
sequential(sK5,sK6),
inference(cnf_transformation,[],[f46]) ).
fof(f82,plain,
on_path(sK6,sK2),
inference(cnf_transformation,[],[f46]) ).
fof(f83,plain,
on_path(sK5,sK2),
inference(cnf_transformation,[],[f46]) ).
fof(f84,plain,
! [X5] : ~ triangle(sK5,sK6,X5),
inference(cnf_transformation,[],[f46]) ).
fof(f85,plain,
! [X0,X1] :
( ~ sequential(X0,X1)
| head_of(X0) = tail_of(X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f86,plain,
! [X0,X1] :
( X0 != X1
| ~ sequential(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f87,plain,
! [X0,X1] :
( ~ sequential(X0,X1)
| edge(X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f88,plain,
! [X0,X1] :
( ~ sequential(X0,X1)
| edge(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f89,plain,
! [X0,X1] :
( head_of(X0) != tail_of(X1)
| ~ edge(X0)
| ~ edge(X1)
| X0 = X1
| sequential(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f90,plain,
! [X2,X3,X0,X1] :
( ~ path(X0,X1,X2)
| in_path(tail_of(X3),X2)
| ~ on_path(X3,X2) ),
inference(cnf_transformation,[],[f27]) ).
fof(f91,plain,
! [X2,X3,X0,X1] :
( ~ path(X0,X1,X2)
| in_path(head_of(X3),X2)
| ~ on_path(X3,X2) ),
inference(cnf_transformation,[],[f27]) ).
fof(f92,plain,
! [X2,X3,X0,X1] :
( ~ path(X0,X1,X2)
| edge(X3)
| ~ on_path(X3,X2) ),
inference(cnf_transformation,[],[f27]) ).
fof(f104,plain,
! [X0,X1] :
( tail_of(sK9(X0,X1)) = X0
| tail_of(sK9(X0,X1)) = X1
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1
| ~ complete ),
inference(cnf_transformation,[],[f55]) ).
fof(f105,plain,
! [X0,X1] :
( tail_of(sK9(X0,X1)) = X0
| head_of(sK9(X0,X1)) = X0
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1
| ~ complete ),
inference(cnf_transformation,[],[f55]) ).
fof(f106,plain,
! [X0,X1] :
( head_of(sK9(X0,X1)) = X1
| tail_of(sK9(X0,X1)) = X1
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1
| ~ complete ),
inference(cnf_transformation,[],[f55]) ).
fof(f107,plain,
! [X0,X1] :
( head_of(sK9(X0,X1)) = X1
| head_of(sK9(X0,X1)) = X0
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1
| ~ complete ),
inference(cnf_transformation,[],[f55]) ).
fof(f109,plain,
! [X0,X1] :
( edge(sK9(X0,X1))
| ~ vertex(X0)
| ~ vertex(X1)
| X0 = X1
| ~ complete ),
inference(cnf_transformation,[],[f55]) ).
fof(f112,plain,
! [X0] :
( head_of(X0) != tail_of(X0)
| ~ edge(X0) ),
inference(cnf_transformation,[],[f34]) ).
fof(f119,plain,
! [X2,X3,X0,X1,X4] :
( ~ sequential(X3,X4)
| ~ on_path(X3,X0)
| ~ on_path(X4,X0)
| precedes(X3,X4,X0)
| ~ path(X1,X2,X0) ),
inference(cnf_transformation,[],[f37]) ).
fof(f122,plain,
! [X2,X0,X1] :
( ~ shortest_path(X0,X1,X2)
| path(X0,X1,X2) ),
inference(cnf_transformation,[],[f63]) ).
fof(f127,plain,
! [X2,X3,X0,X1] :
( ~ path(X0,X1,X2)
| vertex(X3)
| ~ in_path(X3,X2) ),
inference(cnf_transformation,[],[f64]) ).
fof(f128,plain,
! [X2,X3,X0,X1,X4] :
( ~ shortest_path(X0,X1,X4)
| ~ precedes(X3,X2,X4)
| ~ precedes(X2,X3,X4) ),
inference(cnf_transformation,[],[f42]) ).
fof(f129,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,[],[f42]) ).
fof(f130,plain,
! [X1] : ~ sequential(X1,X1),
inference(equality_resolution,[],[f86]) ).
fof(f138,definition,
( spl13_1
<=> complete ),
introduced(definition,[new_symbols(definition,[spl13_1])],[avatar_definition]) ).
fof(f139,plain,
( ~ complete
| spl13_1 ),
inference(avatar_component_clause,[],[f138]) ).
fof(f141,definition,
( spl13_2
<=> ! [X0,X1] :
( tail_of(sK9(X0,X1)) = X0
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| tail_of(sK9(X0,X1)) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl13_2])],[avatar_definition]) ).
fof(f142,plain,
( ! [X0,X1] :
( ~ vertex(X0)
| X0 = X1
| ~ vertex(X1)
| tail_of(sK9(X0,X1)) = X0
| tail_of(sK9(X0,X1)) = X1 )
| ~ spl13_2 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f143,plain,
( ~ spl13_1
| spl13_2 ),
inference(avatar_split_clause,[],[f104,f141,f138]) ).
fof(f145,definition,
( spl13_3
<=> ! [X0,X1] :
( tail_of(sK9(X0,X1)) = X0
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| head_of(sK9(X0,X1)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl13_3])],[avatar_definition]) ).
fof(f146,plain,
( ! [X0,X1] :
( ~ vertex(X0)
| X0 = X1
| ~ vertex(X1)
| tail_of(sK9(X0,X1)) = X0
| head_of(sK9(X0,X1)) = X0 )
| ~ spl13_3 ),
inference(avatar_component_clause,[],[f145]) ).
fof(f147,plain,
( ~ spl13_1
| spl13_3 ),
inference(avatar_split_clause,[],[f105,f145,f138]) ).
fof(f149,definition,
( spl13_4
<=> ! [X0,X1] :
( head_of(sK9(X0,X1)) = X1
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| tail_of(sK9(X0,X1)) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl13_4])],[avatar_definition]) ).
fof(f150,plain,
( ! [X0,X1] :
( ~ vertex(X0)
| X0 = X1
| ~ vertex(X1)
| head_of(sK9(X0,X1)) = X1
| tail_of(sK9(X0,X1)) = X1 )
| ~ spl13_4 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f151,plain,
( ~ spl13_1
| spl13_4 ),
inference(avatar_split_clause,[],[f106,f149,f138]) ).
fof(f153,definition,
( spl13_5
<=> ! [X0,X1] :
( head_of(sK9(X0,X1)) = X1
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0)
| head_of(sK9(X0,X1)) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl13_5])],[avatar_definition]) ).
fof(f154,plain,
( ! [X0,X1] :
( ~ vertex(X0)
| X0 = X1
| ~ vertex(X1)
| head_of(sK9(X0,X1)) = X1
| head_of(sK9(X0,X1)) = X0 )
| ~ spl13_5 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f155,plain,
( ~ spl13_1
| spl13_5 ),
inference(avatar_split_clause,[],[f107,f153,f138]) ).
fof(f161,definition,
( spl13_7
<=> ! [X0,X1] :
( edge(sK9(X0,X1))
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0) ) ),
introduced(definition,[new_symbols(definition,[spl13_7])],[avatar_definition]) ).
fof(f162,plain,
( ! [X0,X1] :
( edge(sK9(X0,X1))
| X0 = X1
| ~ vertex(X1)
| ~ vertex(X0) )
| ~ spl13_7 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f163,plain,
( ~ spl13_1
| spl13_7 ),
inference(avatar_split_clause,[],[f109,f161,f138]) ).
fof(f166,plain,
! [X2,X0,X1] :
( triangle(X0,X1,X2)
| ~ edge(X0)
| ~ edge(X2)
| ~ sequential(X0,X1)
| ~ sequential(X1,X2)
| ~ sequential(X2,X0) ),
inference(forward_subsumption_resolution,[],[f71,f87]) ).
fof(f169,plain,
! [X2,X0,X1] :
( triangle(X0,X1,X2)
| ~ edge(X0)
| ~ sequential(X0,X1)
| ~ sequential(X1,X2)
| ~ sequential(X2,X0) ),
inference(forward_subsumption_resolution,[],[f166,f87]) ).
fof(f170,plain,
! [X2,X0,X1] :
( triangle(X0,X1,X2)
| ~ sequential(X0,X1)
| ~ sequential(X1,X2)
| ~ sequential(X2,X0) ),
inference(forward_subsumption_resolution,[],[f169,f87]) ).
fof(f171,plain,
( $false
| spl13_1 ),
inference(forward_subsumption_resolution,[],[f139,f79]) ).
fof(f172,plain,
spl13_1,
inference(avatar_contradiction_clause,[],[f171]) ).
fof(f173,plain,
! [X0] :
( ~ sequential(sK5,sK6)
| ~ sequential(sK6,X0)
| ~ sequential(X0,sK5) ),
inference(resolution,[],[f84,f170]) ).
fof(f174,plain,
! [X0] :
( ~ sequential(sK6,X0)
| ~ sequential(X0,sK5) ),
inference(forward_subsumption_resolution,[],[f173,f81]) ).
fof(f175,plain,
path(sK3,sK4,sK2),
inference(resolution,[],[f122,f80]) ).
fof(f176,plain,
! [X0] :
( ~ on_path(X0,sK2)
| edge(X0) ),
inference(resolution,[],[f92,f175]) ).
fof(f177,plain,
edge(sK6),
inference(resolution,[],[f176,f82]) ).
fof(f178,plain,
edge(sK5),
inference(resolution,[],[f176,f83]) ).
fof(f181,plain,
head_of(sK5) = tail_of(sK6),
inference(resolution,[],[f85,f81]) ).
fof(f184,plain,
! [X2,X0,X1] :
( ~ on_path(sK6,X0)
| ~ on_path(sK5,X0)
| precedes(sK5,sK6,X0)
| ~ path(X1,X2,X0) ),
inference(resolution,[],[f119,f81]) ).
fof(f185,plain,
! [X0,X1] :
( ~ on_path(sK5,sK2)
| precedes(sK5,sK6,sK2)
| ~ path(X0,X1,sK2) ),
inference(resolution,[],[f184,f82]) ).
fof(f186,plain,
! [X0,X1] :
( precedes(sK5,sK6,sK2)
| ~ path(X0,X1,sK2) ),
inference(forward_subsumption_resolution,[],[f185,f83]) ).
fof(f188,definition,
( spl13_8
<=> ! [X0,X1] : ~ path(X0,X1,sK2) ),
introduced(definition,[new_symbols(definition,[spl13_8])],[avatar_definition]) ).
fof(f189,plain,
( ! [X0,X1] : ~ path(X0,X1,sK2)
| ~ spl13_8 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f191,definition,
( spl13_9
<=> precedes(sK5,sK6,sK2) ),
introduced(definition,[new_symbols(definition,[spl13_9])],[avatar_definition]) ).
fof(f192,plain,
( precedes(sK5,sK6,sK2)
| ~ spl13_9 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f193,plain,
( spl13_8
| spl13_9 ),
inference(avatar_split_clause,[],[f186,f191,f188]) ).
fof(f194,plain,
! [X0] :
( in_path(tail_of(X0),sK2)
| ~ on_path(X0,sK2) ),
inference(resolution,[],[f90,f175]) ).
fof(f197,plain,
! [X0] :
( in_path(head_of(X0),sK2)
| ~ on_path(X0,sK2) ),
inference(resolution,[],[f91,f175]) ).
fof(f198,plain,
! [X2,X3,X0,X1,X4] :
( ~ shortest_path(X2,X3,X4)
| tail_of(X0) != tail_of(X1)
| ~ precedes(X0,X1,X4) ),
inference(equality_resolution,[],[f129]) ).
fof(f199,plain,
! [X0,X1] :
( ~ precedes(X0,X1,sK2)
| tail_of(X0) != tail_of(X1) ),
inference(resolution,[],[f198,f80]) ).
fof(f200,plain,
( tail_of(sK6) != tail_of(sK5)
| ~ spl13_9 ),
inference(resolution,[],[f199,f192]) ).
fof(f201,plain,
( head_of(sK5) != tail_of(sK5)
| ~ spl13_9 ),
inference(forward_demodulation,[],[f200,f181]) ).
fof(f203,plain,
( head_of(sK5) != head_of(sK6)
| ~ edge(sK6) ),
inference(superposition,[],[f112,f181]) ).
fof(f204,plain,
head_of(sK5) != head_of(sK6),
inference(forward_subsumption_resolution,[],[f203,f177]) ).
fof(f205,plain,
! [X0] :
( ~ in_path(X0,sK2)
| vertex(X0) ),
inference(resolution,[],[f127,f175]) ).
fof(f206,plain,
! [X0] :
( ~ on_path(X0,sK2)
| vertex(tail_of(X0)) ),
inference(resolution,[],[f205,f194]) ).
fof(f207,plain,
! [X0] :
( ~ on_path(X0,sK2)
| vertex(head_of(X0)) ),
inference(resolution,[],[f205,f197]) ).
fof(f209,plain,
vertex(head_of(sK6)),
inference(resolution,[],[f207,f82]) ).
fof(f216,plain,
vertex(tail_of(sK5)),
inference(resolution,[],[f206,f83]) ).
fof(f218,plain,
( ! [X0] :
( ~ vertex(X0)
| tail_of(sK5) = X0
| head_of(sK9(tail_of(sK5),X0)) = X0
| tail_of(sK5) = head_of(sK9(tail_of(sK5),X0)) )
| ~ spl13_5 ),
inference(resolution,[],[f216,f154]) ).
fof(f219,plain,
( ! [X0] :
( ~ vertex(X0)
| tail_of(sK5) = X0
| head_of(sK9(tail_of(sK5),X0)) = X0
| tail_of(sK9(tail_of(sK5),X0)) = X0 )
| ~ spl13_4 ),
inference(resolution,[],[f216,f150]) ).
fof(f220,plain,
( ! [X0] :
( ~ vertex(X0)
| tail_of(sK5) = X0
| tail_of(sK5) = tail_of(sK9(tail_of(sK5),X0))
| tail_of(sK5) = head_of(sK9(tail_of(sK5),X0)) )
| ~ spl13_3 ),
inference(resolution,[],[f216,f146]) ).
fof(f221,plain,
( ! [X0] :
( ~ vertex(X0)
| tail_of(sK5) = X0
| tail_of(sK5) = tail_of(sK9(tail_of(sK5),X0))
| tail_of(sK9(tail_of(sK5),X0)) = X0 )
| ~ spl13_2 ),
inference(resolution,[],[f216,f142]) ).
fof(f222,plain,
( tail_of(sK5) = head_of(sK6)
| head_of(sK6) = head_of(sK9(tail_of(sK5),head_of(sK6)))
| tail_of(sK5) = head_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_5 ),
inference(resolution,[],[f218,f209]) ).
fof(f226,definition,
( spl13_10
<=> tail_of(sK5) = head_of(sK9(tail_of(sK5),head_of(sK6))) ),
introduced(definition,[new_symbols(definition,[spl13_10])],[avatar_definition]) ).
fof(f227,plain,
( tail_of(sK5) = head_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_10 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,definition,
( spl13_11
<=> head_of(sK6) = head_of(sK9(tail_of(sK5),head_of(sK6))) ),
introduced(definition,[new_symbols(definition,[spl13_11])],[avatar_definition]) ).
fof(f230,plain,
( head_of(sK6) = head_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_11 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f232,definition,
( spl13_12
<=> tail_of(sK5) = head_of(sK6) ),
introduced(definition,[new_symbols(definition,[spl13_12])],[avatar_definition]) ).
fof(f233,plain,
( tail_of(sK5) = head_of(sK6)
| ~ spl13_12 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f234,plain,
( spl13_10
| spl13_11
| spl13_12
| ~ spl13_5 ),
inference(avatar_split_clause,[],[f222,f153,f232,f229,f226]) ).
fof(f238,plain,
( ! [X0] :
( tail_of(X0) != tail_of(sK5)
| ~ edge(sK9(tail_of(sK5),head_of(sK6)))
| ~ edge(X0)
| sK9(tail_of(sK5),head_of(sK6)) = X0
| sequential(sK9(tail_of(sK5),head_of(sK6)),X0) )
| ~ spl13_10 ),
inference(superposition,[],[f89,f227]) ).
fof(f240,definition,
( spl13_13
<=> edge(sK9(tail_of(sK5),head_of(sK6))) ),
introduced(definition,[new_symbols(definition,[spl13_13])],[avatar_definition]) ).
fof(f241,plain,
( ~ edge(sK9(tail_of(sK5),head_of(sK6)))
| spl13_13 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f243,definition,
( spl13_14
<=> ! [X0] :
( tail_of(X0) != tail_of(sK5)
| sequential(sK9(tail_of(sK5),head_of(sK6)),X0)
| sK9(tail_of(sK5),head_of(sK6)) = X0
| ~ edge(X0) ) ),
introduced(definition,[new_symbols(definition,[spl13_14])],[avatar_definition]) ).
fof(f244,plain,
( ! [X0] :
( tail_of(X0) != tail_of(sK5)
| sequential(sK9(tail_of(sK5),head_of(sK6)),X0)
| sK9(tail_of(sK5),head_of(sK6)) = X0
| ~ edge(X0) )
| ~ spl13_14 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f245,plain,
( ~ spl13_13
| spl13_14
| ~ spl13_10 ),
inference(avatar_split_clause,[],[f238,f226,f243,f240]) ).
fof(f253,plain,
( tail_of(sK5) = head_of(sK6)
| ~ vertex(head_of(sK6))
| ~ vertex(tail_of(sK5))
| ~ spl13_7
| spl13_13 ),
inference(resolution,[],[f241,f162]) ).
fof(f254,plain,
( tail_of(sK5) = head_of(sK6)
| ~ vertex(tail_of(sK5))
| ~ spl13_7
| spl13_13 ),
inference(forward_subsumption_resolution,[],[f253,f209]) ).
fof(f255,plain,
( tail_of(sK5) = head_of(sK6)
| ~ spl13_7
| spl13_13 ),
inference(forward_subsumption_resolution,[],[f254,f216]) ).
fof(f256,plain,
( spl13_12
| ~ spl13_7
| spl13_13 ),
inference(avatar_split_clause,[],[f255,f240,f161,f232]) ).
fof(f263,plain,
( ! [X0] :
( head_of(X0) != head_of(sK6)
| ~ edge(X0)
| ~ edge(sK5)
| sK5 = X0
| sequential(X0,sK5) )
| ~ spl13_12 ),
inference(superposition,[],[f89,f233]) ).
fof(f264,plain,
( ! [X0] :
( head_of(X0) != head_of(sK6)
| ~ edge(X0)
| sK5 = X0
| sequential(X0,sK5) )
| ~ spl13_12 ),
inference(forward_subsumption_resolution,[],[f263,f178]) ).
fof(f267,plain,
( ~ edge(sK6)
| sK5 = sK6
| sequential(sK6,sK5)
| ~ spl13_12 ),
inference(equality_resolution,[],[f264]) ).
fof(f268,plain,
( sK5 = sK6
| sequential(sK6,sK5)
| ~ spl13_12 ),
inference(forward_subsumption_resolution,[],[f267,f177]) ).
fof(f270,definition,
( spl13_17
<=> sequential(sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl13_17])],[avatar_definition]) ).
fof(f271,plain,
( sequential(sK6,sK5)
| ~ spl13_17 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f273,definition,
( spl13_18
<=> sK5 = sK6 ),
introduced(definition,[new_symbols(definition,[spl13_18])],[avatar_definition]) ).
fof(f274,plain,
( sK5 = sK6
| ~ spl13_18 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f275,plain,
( spl13_17
| spl13_18
| ~ spl13_12 ),
inference(avatar_split_clause,[],[f268,f232,f273,f270]) ).
fof(f277,plain,
( sequential(sK9(tail_of(sK5),head_of(sK6)),sK5)
| sK5 = sK9(tail_of(sK5),head_of(sK6))
| ~ edge(sK5)
| ~ spl13_14 ),
inference(equality_resolution,[],[f244]) ).
fof(f278,plain,
( sequential(sK9(tail_of(sK5),head_of(sK6)),sK5)
| sK5 = sK9(tail_of(sK5),head_of(sK6))
| ~ spl13_14 ),
inference(forward_subsumption_resolution,[],[f277,f178]) ).
fof(f280,definition,
( spl13_19
<=> sK5 = sK9(tail_of(sK5),head_of(sK6)) ),
introduced(definition,[new_symbols(definition,[spl13_19])],[avatar_definition]) ).
fof(f281,plain,
( sK5 = sK9(tail_of(sK5),head_of(sK6))
| ~ spl13_19 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f283,definition,
( spl13_20
<=> sequential(sK9(tail_of(sK5),head_of(sK6)),sK5) ),
introduced(definition,[new_symbols(definition,[spl13_20])],[avatar_definition]) ).
fof(f284,plain,
( sequential(sK9(tail_of(sK5),head_of(sK6)),sK5)
| ~ spl13_20 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f287,plain,
( sequential(sK5,sK5)
| ~ spl13_18 ),
inference(superposition,[],[f81,f274]) ).
fof(f304,plain,
( $false
| ~ spl13_18 ),
inference(forward_subsumption_resolution,[],[f287,f130]) ).
fof(f305,plain,
~ spl13_18,
inference(avatar_contradiction_clause,[],[f304]) ).
fof(f308,plain,
( ! [X2,X0,X1] :
( ~ on_path(sK6,X0)
| ~ on_path(sK5,X0)
| precedes(sK6,sK5,X0)
| ~ path(X1,X2,X0) )
| ~ spl13_17 ),
inference(resolution,[],[f271,f119]) ).
fof(f319,plain,
( ! [X0,X1] :
( ~ on_path(sK5,sK2)
| precedes(sK6,sK5,sK2)
| ~ path(X0,X1,sK2) )
| ~ spl13_17 ),
inference(resolution,[],[f308,f82]) ).
fof(f320,plain,
( ! [X0,X1] :
( precedes(sK6,sK5,sK2)
| ~ path(X0,X1,sK2) )
| ~ spl13_17 ),
inference(forward_subsumption_resolution,[],[f319,f83]) ).
fof(f322,definition,
( spl13_21
<=> precedes(sK6,sK5,sK2) ),
introduced(definition,[new_symbols(definition,[spl13_21])],[avatar_definition]) ).
fof(f323,plain,
( precedes(sK6,sK5,sK2)
| ~ spl13_21 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f324,plain,
( spl13_8
| spl13_21
| ~ spl13_17 ),
inference(avatar_split_clause,[],[f320,f270,f322,f188]) ).
fof(f340,plain,
( tail_of(sK5) = head_of(sK6)
| tail_of(sK5) = tail_of(sK9(tail_of(sK5),head_of(sK6)))
| head_of(sK6) = tail_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_2 ),
inference(resolution,[],[f221,f209]) ).
fof(f343,plain,
( tail_of(sK5) = head_of(sK6)
| head_of(sK6) = head_of(sK9(tail_of(sK5),head_of(sK6)))
| head_of(sK6) = tail_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_4 ),
inference(resolution,[],[f219,f209]) ).
fof(f360,plain,
( tail_of(sK5) = head_of(sK6)
| tail_of(sK5) = tail_of(sK9(tail_of(sK5),head_of(sK6)))
| tail_of(sK5) = head_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_3 ),
inference(resolution,[],[f220,f209]) ).
fof(f367,plain,
( $false
| ~ spl13_9
| ~ spl13_21 ),
inference(unit_resulting_resolution,[],[f128,f192,f323,f80]) ).
fof(f370,plain,
( ~ spl13_9
| ~ spl13_21 ),
inference(avatar_contradiction_clause,[],[f367]) ).
fof(f372,plain,
( $false
| ~ spl13_8 ),
inference(unit_resulting_resolution,[],[f122,f80,f189]) ).
fof(f376,plain,
~ spl13_8,
inference(avatar_contradiction_clause,[],[f372]) ).
fof(f377,plain,
( spl13_19
| spl13_20
| ~ spl13_14 ),
inference(avatar_split_clause,[],[f278,f243,f283,f280]) ).
fof(f379,definition,
( spl13_22
<=> head_of(sK6) = tail_of(sK9(tail_of(sK5),head_of(sK6))) ),
introduced(definition,[new_symbols(definition,[spl13_22])],[avatar_definition]) ).
fof(f380,plain,
( head_of(sK6) = tail_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_22 ),
inference(avatar_component_clause,[],[f379]) ).
fof(f382,definition,
( spl13_23
<=> tail_of(sK5) = tail_of(sK9(tail_of(sK5),head_of(sK6))) ),
introduced(definition,[new_symbols(definition,[spl13_23])],[avatar_definition]) ).
fof(f383,plain,
( tail_of(sK5) = tail_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_23 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f384,plain,
( spl13_22
| spl13_23
| spl13_12
| ~ spl13_2 ),
inference(avatar_split_clause,[],[f340,f141,f232,f382,f379]) ).
fof(f385,plain,
( tail_of(sK5) = head_of(sK6)
| tail_of(sK5) = head_of(sK6)
| head_of(sK6) = tail_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_4
| ~ spl13_10 ),
inference(forward_demodulation,[],[f343,f227]) ).
fof(f386,plain,
( tail_of(sK5) = head_of(sK6)
| head_of(sK6) = tail_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_4
| ~ spl13_10 ),
inference(duplicate_literal_removal,[],[f385]) ).
fof(f403,plain,
( spl13_22
| spl13_12
| ~ spl13_4
| ~ spl13_10 ),
inference(avatar_split_clause,[],[f386,f226,f149,f232,f379]) ).
fof(f406,plain,
( edge(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_20 ),
inference(resolution,[],[f284,f88]) ).
fof(f446,plain,
( ! [X0] :
( head_of(X0) != head_of(sK6)
| ~ edge(X0)
| ~ edge(sK9(tail_of(sK5),head_of(sK6)))
| sK9(tail_of(sK5),head_of(sK6)) = X0
| sequential(X0,sK9(tail_of(sK5),head_of(sK6))) )
| ~ spl13_22 ),
inference(superposition,[],[f89,f380]) ).
fof(f447,plain,
( ! [X0] :
( head_of(X0) != head_of(sK6)
| ~ edge(X0)
| sK9(tail_of(sK5),head_of(sK6)) = X0
| sequential(X0,sK9(tail_of(sK5),head_of(sK6))) )
| ~ spl13_20
| ~ spl13_22 ),
inference(forward_subsumption_resolution,[],[f446,f406]) ).
fof(f454,plain,
( ~ edge(sK6)
| sK6 = sK9(tail_of(sK5),head_of(sK6))
| sequential(sK6,sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_20
| ~ spl13_22 ),
inference(equality_resolution,[],[f447]) ).
fof(f455,plain,
( sK6 = sK9(tail_of(sK5),head_of(sK6))
| sequential(sK6,sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_20
| ~ spl13_22 ),
inference(forward_subsumption_resolution,[],[f454,f177]) ).
fof(f457,definition,
( spl13_32
<=> sequential(sK6,sK9(tail_of(sK5),head_of(sK6))) ),
introduced(definition,[new_symbols(definition,[spl13_32])],[avatar_definition]) ).
fof(f458,plain,
( sequential(sK6,sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_32 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f460,definition,
( spl13_33
<=> sK6 = sK9(tail_of(sK5),head_of(sK6)) ),
introduced(definition,[new_symbols(definition,[spl13_33])],[avatar_definition]) ).
fof(f461,plain,
( sK6 = sK9(tail_of(sK5),head_of(sK6))
| ~ spl13_33 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f462,plain,
( spl13_32
| spl13_33
| ~ spl13_20
| ~ spl13_22 ),
inference(avatar_split_clause,[],[f455,f379,f283,f460,f457]) ).
fof(f463,plain,
( tail_of(sK6) = head_of(sK6)
| ~ spl13_22
| ~ spl13_33 ),
inference(superposition,[],[f380,f461]) ).
fof(f471,plain,
( head_of(sK5) = head_of(sK6)
| ~ spl13_22
| ~ spl13_33 ),
inference(forward_demodulation,[],[f463,f181]) ).
fof(f472,plain,
( $false
| ~ spl13_22
| ~ spl13_33 ),
inference(forward_subsumption_resolution,[],[f471,f204]) ).
fof(f473,plain,
( ~ spl13_22
| ~ spl13_33 ),
inference(avatar_contradiction_clause,[],[f472]) ).
fof(f476,plain,
( ~ sequential(sK9(tail_of(sK5),head_of(sK6)),sK5)
| ~ spl13_32 ),
inference(resolution,[],[f458,f174]) ).
fof(f483,plain,
( $false
| ~ spl13_20
| ~ spl13_32 ),
inference(forward_subsumption_resolution,[],[f476,f284]) ).
fof(f484,plain,
( ~ spl13_20
| ~ spl13_32 ),
inference(avatar_contradiction_clause,[],[f483]) ).
fof(f497,plain,
( head_of(sK5) = tail_of(sK5)
| ~ spl13_10
| ~ spl13_19 ),
inference(superposition,[],[f227,f281]) ).
fof(f499,plain,
( $false
| ~ spl13_9
| ~ spl13_10
| ~ spl13_19 ),
inference(forward_subsumption_resolution,[],[f497,f201]) ).
fof(f500,plain,
( ~ spl13_9
| ~ spl13_10
| ~ spl13_19 ),
inference(avatar_contradiction_clause,[],[f499]) ).
fof(f508,plain,
( tail_of(sK5) = head_of(sK6)
| tail_of(sK5) = head_of(sK6)
| tail_of(sK5) = head_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_3
| ~ spl13_22 ),
inference(forward_demodulation,[],[f360,f380]) ).
fof(f509,plain,
( tail_of(sK5) = head_of(sK6)
| tail_of(sK5) = head_of(sK9(tail_of(sK5),head_of(sK6)))
| ~ spl13_3
| ~ spl13_22 ),
inference(duplicate_literal_removal,[],[f508]) ).
fof(f511,plain,
( tail_of(sK5) = head_of(sK6)
| tail_of(sK5) = head_of(sK6)
| ~ spl13_3
| ~ spl13_11
| ~ spl13_22 ),
inference(forward_demodulation,[],[f509,f230]) ).
fof(f512,plain,
( tail_of(sK5) = head_of(sK6)
| ~ spl13_3
| ~ spl13_11
| ~ spl13_22 ),
inference(duplicate_literal_removal,[],[f511]) ).
fof(f515,plain,
( spl13_12
| ~ spl13_3
| ~ spl13_11
| ~ spl13_22 ),
inference(avatar_split_clause,[],[f512,f379,f229,f145,f232]) ).
fof(f535,plain,
( $false
| ~ spl13_9
| ~ spl13_11
| ~ spl13_23 ),
inference(unit_resulting_resolution,[],[f129,f80,f192,f230,f383]) ).
fof(f539,plain,
( ~ spl13_9
| ~ spl13_11
| ~ spl13_23 ),
inference(avatar_contradiction_clause,[],[f535]) ).
cnf(s1,plain,
( ~ spl13_1
| spl13_2 ),
inference(sat_conversion,[],[f143]) ).
cnf(s2,plain,
( ~ spl13_1
| spl13_3 ),
inference(sat_conversion,[],[f147]) ).
cnf(s3,plain,
( ~ spl13_1
| spl13_4 ),
inference(sat_conversion,[],[f151]) ).
cnf(s4,plain,
( ~ spl13_1
| spl13_5 ),
inference(sat_conversion,[],[f155]) ).
cnf(s6,plain,
( ~ spl13_1
| spl13_7 ),
inference(sat_conversion,[],[f163]) ).
cnf(s7,plain,
spl13_1,
inference(sat_conversion,[],[f172]) ).
cnf(s8,plain,
( spl13_8
| spl13_9 ),
inference(sat_conversion,[],[f193]) ).
cnf(s9,plain,
( ~ spl13_5
| spl13_10
| spl13_11
| spl13_12 ),
inference(sat_conversion,[],[f234]) ).
cnf(s10,plain,
( ~ spl13_10
| ~ spl13_13
| spl13_14 ),
inference(sat_conversion,[],[f245]) ).
cnf(s12,plain,
( ~ spl13_7
| spl13_12
| spl13_13 ),
inference(sat_conversion,[],[f256]) ).
cnf(s13,plain,
( ~ spl13_12
| spl13_17
| spl13_18 ),
inference(sat_conversion,[],[f275]) ).
cnf(s17,plain,
~ spl13_18,
inference(sat_conversion,[],[f305]) ).
cnf(s18,plain,
( spl13_8
| ~ spl13_17
| spl13_21 ),
inference(sat_conversion,[],[f324]) ).
cnf(s20,plain,
( ~ spl13_9
| ~ spl13_21 ),
inference(sat_conversion,[],[f370]) ).
cnf(s23,plain,
~ spl13_8,
inference(sat_conversion,[],[f376]) ).
cnf(s24,plain,
( ~ spl13_14
| spl13_19
| spl13_20 ),
inference(sat_conversion,[],[f377]) ).
cnf(s25,plain,
( ~ spl13_2
| spl13_12
| spl13_22
| spl13_23 ),
inference(sat_conversion,[],[f384]) ).
cnf(s30,plain,
( ~ spl13_4
| ~ spl13_10
| spl13_12
| spl13_22 ),
inference(sat_conversion,[],[f403]) ).
cnf(s36,plain,
( ~ spl13_20
| ~ spl13_22
| spl13_32
| spl13_33 ),
inference(sat_conversion,[],[f462]) ).
cnf(s39,plain,
( ~ spl13_22
| ~ spl13_33 ),
inference(sat_conversion,[],[f473]) ).
cnf(s42,plain,
( ~ spl13_20
| ~ spl13_32 ),
inference(sat_conversion,[],[f484]) ).
cnf(s43,plain,
( ~ spl13_9
| ~ spl13_10
| ~ spl13_19 ),
inference(sat_conversion,[],[f500]) ).
cnf(s48,plain,
( ~ spl13_3
| ~ spl13_11
| spl13_12
| ~ spl13_22 ),
inference(sat_conversion,[],[f515]) ).
cnf(s51,plain,
( ~ spl13_9
| ~ spl13_11
| ~ spl13_23 ),
inference(sat_conversion,[],[f539]) ).
cnf(s54,plain,
( ~ spl13_17
| spl13_21 ),
inference(rat,[],[s18,s23]) ).
cnf(s55,plain,
( ~ spl13_12
| spl13_17 ),
inference(rat,[],[s13,s17]) ).
cnf(s56,plain,
spl13_9,
inference(rat,[],[s8,s23]) ).
cnf(s57,plain,
~ spl13_21,
inference(rat,[],[s20,s56]) ).
cnf(s58,plain,
~ spl13_17,
inference(rat,[],[s54,s57]) ).
cnf(s59,plain,
~ spl13_12,
inference(rat,[],[s55,s58]) ).
cnf(s60,plain,
spl13_7,
inference(rat,[],[s6,s7]) ).
cnf(s61,plain,
spl13_13,
inference(rat,[],[s12,s59,s60]) ).
cnf(s63,plain,
spl13_5,
inference(rat,[],[s4,s7]) ).
cnf(s64,plain,
spl13_4,
inference(rat,[],[s3,s7]) ).
cnf(s65,plain,
spl13_3,
inference(rat,[],[s2,s7]) ).
cnf(s66,plain,
spl13_2,
inference(rat,[],[s1,s7]) ).
cnf(s67,plain,
~ spl13_11,
inference(rat,[],[s25,s48,s51,s59,s66,s65,s56]) ).
cnf(s68,plain,
spl13_10,
inference(rat,[],[s9,s59,s63,s67]) ).
cnf(s69,plain,
~ spl13_19,
inference(rat,[],[s43,s56,s68]) ).
cnf(s70,plain,
spl13_22,
inference(rat,[],[s30,s64,s59,s68]) ).
cnf(s71,plain,
spl13_14,
inference(rat,[],[s10,s61,s68]) ).
cnf(s73,plain,
~ spl13_33,
inference(rat,[],[s39,s70]) ).
cnf(s74,plain,
spl13_20,
inference(rat,[],[s24,s69,s71]) ).
cnf(s75,plain,
~ spl13_32,
inference(rat,[],[s42,s74]) ).
cnf(s76,plain,
$false,
inference(rat,[],[s36,s73,s70,s75,s74]) ).
fof(f547,plain,
$false,
inference(avatar_sat_refutation,[],[s76]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA009+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.36 % Computer : n013.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Sun Sep 27 08:47:07 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/0.39 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.58/1.91 % (4117639)Detected formulas, will run a generic FOF schedule.
% 5.58/1.91 % (4117648)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2900281841:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.58/1.91 % (4117644)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=828041951:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.58/1.91 % (4117649)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3891546355:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.58/1.91 % (4117646)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3244666725:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.58/1.91 % (4117647)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2727674184:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.58/1.91 % (4117645)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4154899433:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.58/1.91 % (4117647)Refutation not found, incomplete strategy
% 5.58/1.91 % (4117647)------------------------------
% 5.58/1.91 % (4117647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117647)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117647)Termination reason: Refutation not found, incomplete strategy
% 5.58/1.91 % (4117647)Time elapsed: 0.001 s
% 5.58/1.91 % (4117647)Peak memory usage: 88 MB
% 5.58/1.91 % (4117648)Instruction limit reached!
% 5.58/1.91 % (4117648)------------------------------
% 5.58/1.91 % (4117648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117648)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117648)Termination reason: Instruction limit
% 5.58/1.91 % (4117648)Termination phase: Saturation
% 5.58/1.91 % (4117648)Time elapsed: 0.036 s
% 5.58/1.91 % (4117648)Peak memory usage: 88 MB
% 5.58/1.91 % (4117648)Instructions burned: 123 (million)
% 5.58/1.91 % (4117650)dis-21_1_sil=8000:lcm=predicate:random_seed=2003204671:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.58/1.91 % (4117650)Instruction limit reached!
% 5.58/1.91 % (4117650)------------------------------
% 5.58/1.91 % (4117650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117650)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117650)Termination reason: Instruction limit
% 5.58/1.91 % (4117650)Termination phase: Saturation
% 5.58/1.91 % (4117650)Time elapsed: 0.067 s
% 5.58/1.91 % (4117650)Peak memory usage: 89 MB
% 5.58/1.91 % (4117650)Instructions burned: 129 (million)
% 5.58/1.91 % (4117658)lrs+10_1_sil=8000:sp=occurrence:random_seed=1956688587:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 5.58/1.91 % (4117649)Instruction limit reached!
% 5.58/1.91 % (4117649)------------------------------
% 5.58/1.91 % (4117649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117649)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117649)Termination reason: Instruction limit
% 5.58/1.91 % (4117649)Termination phase: Saturation
% 5.58/1.91 % (4117649)Time elapsed: 0.100 s
% 5.58/1.91 % (4117649)Peak memory usage: 89 MB
% 5.58/1.91 % (4117649)Instructions burned: 140 (million)
% 5.58/1.91 % (4117658)Instruction limit reached!
% 5.58/1.91 % (4117658)------------------------------
% 5.58/1.91 % (4117658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117658)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117658)Termination reason: Instruction limit
% 5.58/1.91 % (4117658)Termination phase: Saturation
% 5.58/1.91 % (4117658)Time elapsed: 0.090 s
% 5.58/1.91 % (4117658)Peak memory usage: 91 MB
% 5.58/1.91 % (4117658)Instructions burned: 285 (million)
% 5.58/1.91 % (4117659)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3746407927:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.58/1.91 % (4117661)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1664572840:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.58/1.91 % (4117647)------------------------------
% 5.58/1.91 % (4117647)------------------------------
% 5.58/1.91 % (4117662)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4243945175:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 5.58/1.91 % (4117659)Instruction limit reached!
% 5.58/1.91 % (4117659)------------------------------
% 5.58/1.91 % (4117659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117659)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117659)Termination reason: Instruction limit
% 5.58/1.91 % (4117659)Termination phase: Saturation
% 5.58/1.91 % (4117659)Time elapsed: 0.081 s
% 5.58/1.91 % (4117659)Peak memory usage: 89 MB
% 5.58/1.91 % (4117659)Instructions burned: 158 (million)
% 5.58/1.91 % (4117662)Instruction limit reached!
% 5.58/1.91 % (4117662)------------------------------
% 5.58/1.91 % (4117662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117662)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117662)Termination reason: Instruction limit
% 5.58/1.91 % (4117662)Termination phase: Saturation
% 5.58/1.91 % (4117662)Time elapsed: 0.078 s
% 5.58/1.91 % (4117662)Peak memory usage: 90 MB
% 5.58/1.91 % (4117662)Instructions burned: 250 (million)
% 5.58/1.91 % (4117665)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=623171874:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 5.58/1.91 % (4117667)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3267142427:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 5.58/1.91 % (4117668)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4086527789:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 5.58/1.91 % (4117661)Instruction limit reached!
% 5.58/1.91 % (4117661)------------------------------
% 5.58/1.91 % (4117661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117661)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117661)Termination reason: Instruction limit
% 5.58/1.91 % (4117661)Termination phase: Saturation
% 5.58/1.91 % (4117661)Time elapsed: 0.210 s
% 5.58/1.91 % (4117661)Peak memory usage: 91 MB
% 5.58/1.91 % (4117661)Instructions burned: 326 (million)
% 5.58/1.91 % (4117668)Instruction limit reached!
% 5.58/1.91 % (4117668)------------------------------
% 5.58/1.91 % (4117668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117668)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117668)Termination reason: Instruction limit
% 5.58/1.91 % (4117668)Termination phase: Saturation
% 5.58/1.91 % (4117668)Time elapsed: 0.042 s
% 5.58/1.91 % (4117668)Peak memory usage: 90 MB
% 5.58/1.91 % (4117668)Instructions burned: 116 (million)
% 5.58/1.91 % (4117665)Instruction limit reached!
% 5.58/1.91 % (4117665)------------------------------
% 5.58/1.91 % (4117665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117665)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117665)Termination reason: Instruction limit
% 5.58/1.91 % (4117665)Termination phase: Saturation
% 5.58/1.91 % (4117665)Time elapsed: 0.155 s
% 5.58/1.91 % (4117665)Peak memory usage: 88 MB
% 5.58/1.91 % (4117665)Instructions burned: 294 (million)
% 5.58/1.91 % (4117672)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2579101680:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 5.58/1.91 % (4117673)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=654059636:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 5.58/1.91 % (4117673)Instruction limit reached!
% 5.58/1.91 % (4117673)------------------------------
% 5.58/1.91 % (4117673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117673)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117673)Termination reason: Instruction limit
% 5.58/1.91 % (4117673)Termination phase: Saturation
% 5.58/1.91 % (4117673)Time elapsed: 0.036 s
% 5.58/1.91 % (4117673)Peak memory usage: 89 MB
% 5.58/1.91 % (4117673)Instructions burned: 115 (million)
% 5.58/1.91 % (4117672)Instruction limit reached!
% 5.58/1.91 % (4117672)------------------------------
% 5.58/1.91 % (4117672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117672)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117672)Termination reason: Instruction limit
% 5.58/1.91 % (4117672)Termination phase: Saturation
% 5.58/1.91 % (4117672)Time elapsed: 0.066 s
% 5.58/1.91 % (4117672)Peak memory usage: 89 MB
% 5.58/1.91 % (4117672)Instructions burned: 127 (million)
% 5.58/1.91 % (4117645)First to succeed.
% 5.58/1.91 % (4117674)lrs+10_1_sil=8000:sp=occurrence:random_seed=722889250:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 5.58/1.91 % (4117645)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4117639"
% 5.58/1.91 % (4117677)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=443018385:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 5.58/1.91 % (4117677)Refutation not found, incomplete strategy
% 5.58/1.91 % (4117677)------------------------------
% 5.58/1.91 % (4117677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.58/1.91 % (4117677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.58/1.91 % (4117677)CaDiCaL version: 2.1.3
% 5.58/1.91 % (4117677)Termination reason: Refutation not found, incomplete strategy
% 5.58/1.91 % (4117677)Time elapsed: 0.001 s
% 5.58/1.91 % (4117677)Peak memory usage: 88 MB
% 5.58/1.91 % (4117677)Instructions burned: 1 (million)
% 5.58/1.91 % (4117678)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1638994420:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 5.58/1.91 % (4117677)------------------------------
% 5.58/1.91 % (4117677)------------------------------
% 5.58/1.91 % (4117645)Refutation found. Thanks to Tanya!
% 5.58/1.91 % SZS status Theorem for theBenchmark
% 5.58/1.91 % SZS output start Proof for theBenchmark
% See solution above
% 8.18/2.05 % (4117645)------------------------------
% 8.18/2.05 % (4117645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/2.05 % (4117645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/2.05 % (4117645)CaDiCaL version: 2.1.3
% 8.18/2.05 % (4117645)Termination reason: Refutation
% 8.18/2.05 % (4117645)Time elapsed: 0.674 s
% 8.18/2.05 % (4117645)Peak memory usage: 130 MB
% 8.18/2.05 % (4117645)Instructions burned: 987 (million)
% 8.18/2.05 % (4117645)------------------------------
% 8.18/2.05 % (4117645)------------------------------
% 8.18/2.05 % (4117639)Success in time 1.08 s
% 8.18/2.05 % Vampire exiting
%------------------------------------------------------------------------------