%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWB041+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 01:00:17 PM UTC 2026
% Result : Theorem 11.18s 2.70s
% Output : Refutation 13.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 23
% Syntax : Number of formulae : 180 ( 31 unt; 18 def)
% Number of atoms : 812 ( 0 equ)
% Maximal formula atoms : 24 ( 4 avg)
% Number of connectives : 1114 ( 482 ~; 518 |; 86 &)
% ( 26 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 19 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-3 aty)
% Number of variables : 256 ( 0 sgn 243 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f202,axiom,
! [X0,X1] :
( iext(uri_owl_equivalentClass,X0,X1)
=> ( ic(X0)
& ic(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_prop_equivalentclass_ext) ).
fof(f289,axiom,
! [X0,X1,X2,X3,X4] :
( ( iext(uri_rdf_first,X1,X2)
& iext(uri_rdf_rest,X1,X3)
& iext(uri_rdf_first,X3,X4)
& iext(uri_rdf_rest,X3,uri_rdf_nil) )
=> ( iext(uri_owl_unionOf,X0,X1)
<=> ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( icext(X0,X5)
<=> ( icext(X2,X5)
| icext(X4,X5) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_bool_unionof_class_002) ).
fof(f351,axiom,
! [X0,X1] :
( iext(uri_owl_equivalentClass,X0,X1)
<=> ( ic(X0)
& ic(X1)
& ! [X2] :
( icext(X0,X2)
<=> icext(X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_eqdis_equivalentclass) ).
fof(f559,conjecture,
? [X0,X1] :
( iext(uri_rdf_first,X0,uri_ex_x)
& iext(uri_rdf_rest,X0,X1)
& iext(uri_rdf_first,X1,uri_ex_y)
& iext(uri_rdf_rest,X1,uri_rdf_nil)
& iext(uri_owl_unionOf,uri_ex_c,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conclusion_rdfbased_sem_bool_union_ext) ).
fof(f560,negated_conjecture,
~ ? [X0,X1] :
( iext(uri_rdf_first,X0,uri_ex_x)
& iext(uri_rdf_rest,X0,X1)
& iext(uri_rdf_first,X1,uri_ex_y)
& iext(uri_rdf_rest,X1,uri_rdf_nil)
& iext(uri_owl_unionOf,uri_ex_c,X0) ),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
? [X0,X1,X2] :
( iext(uri_owl_unionOf,X2,X1)
& iext(uri_rdf_first,X1,uri_ex_x)
& iext(uri_rdf_rest,X1,X0)
& iext(uri_rdf_first,X0,uri_ex_y)
& iext(uri_rdf_rest,X0,uri_rdf_nil)
& iext(uri_owl_equivalentClass,uri_ex_c,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_rdfbased_sem_bool_union_ext) ).
fof(f562,plain,
! [X0,X1] :
( ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_rest,X0,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_owl_unionOf,uri_ex_c,X0) ),
inference(ennf_transformation,[],[f560]) ).
fof(f571,plain,
! [X0,X1,X2,X3,X4] :
( ( iext(uri_owl_unionOf,X0,X1)
<=> ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( icext(X0,X5)
<=> ( icext(X2,X5)
| icext(X4,X5) ) ) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(ennf_transformation,[],[f289]) ).
fof(f572,plain,
! [X0,X1,X2,X3,X4] :
( ( iext(uri_owl_unionOf,X0,X1)
<=> ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( icext(X0,X5)
<=> ( icext(X2,X5)
| icext(X4,X5) ) ) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(flattening,[],[f571]) ).
fof(f576,plain,
! [X0,X1] :
( ( ic(X0)
& ic(X1) )
| ~ iext(uri_owl_equivalentClass,X0,X1) ),
inference(ennf_transformation,[],[f202]) ).
fof(f593,plain,
( iext(uri_owl_unionOf,sK2,sK1)
& iext(uri_rdf_first,sK1,uri_ex_x)
& iext(uri_rdf_rest,sK1,sK0)
& iext(uri_rdf_first,sK0,uri_ex_y)
& iext(uri_rdf_rest,sK0,uri_rdf_nil)
& iext(uri_owl_equivalentClass,uri_ex_c,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f561]) ).
fof(f598,plain,
! [X0,X1,X2,X3,X4] :
( ( ( iext(uri_owl_unionOf,X0,X1)
| ~ ic(X0)
| ~ ic(X2)
| ~ ic(X4)
| ? [X5] :
( ( ( ~ icext(X2,X5)
& ~ icext(X4,X5) )
| ~ icext(X0,X5) )
& ( icext(X2,X5)
| icext(X4,X5)
| icext(X0,X5) ) ) )
& ( ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( ( icext(X0,X5)
| ( ~ icext(X2,X5)
& ~ icext(X4,X5) ) )
& ( icext(X2,X5)
| icext(X4,X5)
| ~ icext(X0,X5) ) ) )
| ~ iext(uri_owl_unionOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(nnf_transformation,[],[f572]) ).
fof(f599,plain,
! [X0,X1,X2,X3,X4] :
( ( ( iext(uri_owl_unionOf,X0,X1)
| ~ ic(X0)
| ~ ic(X2)
| ~ ic(X4)
| ? [X5] :
( ( ( ~ icext(X2,X5)
& ~ icext(X4,X5) )
| ~ icext(X0,X5) )
& ( icext(X2,X5)
| icext(X4,X5)
| icext(X0,X5) ) ) )
& ( ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X5] :
( ( icext(X0,X5)
| ( ~ icext(X2,X5)
& ~ icext(X4,X5) ) )
& ( icext(X2,X5)
| icext(X4,X5)
| ~ icext(X0,X5) ) ) )
| ~ iext(uri_owl_unionOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(flattening,[],[f598]) ).
fof(f600,plain,
! [X0,X1,X2,X3,X4] :
( ( ( iext(uri_owl_unionOf,X0,X1)
| ~ ic(X0)
| ~ ic(X2)
| ~ ic(X4)
| ? [X5] :
( ( ( ~ icext(X2,X5)
& ~ icext(X4,X5) )
| ~ icext(X0,X5) )
& ( icext(X2,X5)
| icext(X4,X5)
| icext(X0,X5) ) ) )
& ( ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X6] :
( ( icext(X0,X6)
| ( ~ icext(X2,X6)
& ~ icext(X4,X6) ) )
& ( icext(X2,X6)
| icext(X4,X6)
| ~ icext(X0,X6) ) ) )
| ~ iext(uri_owl_unionOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(rectify,[],[f599]) ).
fof(f601,plain,
! [X0,X1,X2,X3,X4] :
( ( ( iext(uri_owl_unionOf,X0,X1)
| ~ ic(X0)
| ~ ic(X2)
| ~ ic(X4)
| ( ( ( ~ icext(X2,sK4(X0,X2,X4))
& ~ icext(X4,sK4(X0,X2,X4)) )
| ~ icext(X0,sK4(X0,X2,X4)) )
& ( icext(X2,sK4(X0,X2,X4))
| icext(X4,sK4(X0,X2,X4))
| icext(X0,sK4(X0,X2,X4)) ) ) )
& ( ( ic(X0)
& ic(X2)
& ic(X4)
& ! [X6] :
( ( icext(X0,X6)
| ( ~ icext(X2,X6)
& ~ icext(X4,X6) ) )
& ( icext(X2,X6)
| icext(X4,X6)
| ~ icext(X0,X6) ) ) )
| ~ iext(uri_owl_unionOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X5,sK4(X0,X2,X4))],[f600]) ).
fof(f610,plain,
! [X0,X1] :
( ( iext(uri_owl_equivalentClass,X0,X1)
| ~ ic(X0)
| ~ ic(X1)
| ? [X2] :
( ( ~ icext(X1,X2)
| ~ icext(X0,X2) )
& ( icext(X1,X2)
| icext(X0,X2) ) ) )
& ( ( ic(X0)
& ic(X1)
& ! [X2] :
( ( icext(X0,X2)
| ~ icext(X1,X2) )
& ( icext(X1,X2)
| ~ icext(X0,X2) ) ) )
| ~ iext(uri_owl_equivalentClass,X0,X1) ) ),
inference(nnf_transformation,[],[f351]) ).
fof(f611,plain,
! [X0,X1] :
( ( iext(uri_owl_equivalentClass,X0,X1)
| ~ ic(X0)
| ~ ic(X1)
| ? [X2] :
( ( ~ icext(X1,X2)
| ~ icext(X0,X2) )
& ( icext(X1,X2)
| icext(X0,X2) ) ) )
& ( ( ic(X0)
& ic(X1)
& ! [X2] :
( ( icext(X0,X2)
| ~ icext(X1,X2) )
& ( icext(X1,X2)
| ~ icext(X0,X2) ) ) )
| ~ iext(uri_owl_equivalentClass,X0,X1) ) ),
inference(flattening,[],[f610]) ).
fof(f612,plain,
! [X0,X1] :
( ( iext(uri_owl_equivalentClass,X0,X1)
| ~ ic(X0)
| ~ ic(X1)
| ? [X2] :
( ( ~ icext(X1,X2)
| ~ icext(X0,X2) )
& ( icext(X1,X2)
| icext(X0,X2) ) ) )
& ( ( ic(X0)
& ic(X1)
& ! [X3] :
( ( icext(X0,X3)
| ~ icext(X1,X3) )
& ( icext(X1,X3)
| ~ icext(X0,X3) ) ) )
| ~ iext(uri_owl_equivalentClass,X0,X1) ) ),
inference(rectify,[],[f611]) ).
fof(f613,plain,
! [X0,X1] :
( ( iext(uri_owl_equivalentClass,X0,X1)
| ~ ic(X0)
| ~ ic(X1)
| ( ( ~ icext(X1,sK7(X0,X1))
| ~ icext(X0,sK7(X0,X1)) )
& ( icext(X1,sK7(X0,X1))
| icext(X0,sK7(X0,X1)) ) ) )
& ( ( ic(X0)
& ic(X1)
& ! [X3] :
( ( icext(X0,X3)
| ~ icext(X1,X3) )
& ( icext(X1,X3)
| ~ icext(X0,X3) ) ) )
| ~ iext(uri_owl_equivalentClass,X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f612]) ).
fof(f627,plain,
! [X0,X1] :
( ~ iext(uri_owl_unionOf,uri_ex_c,X0)
| ~ iext(uri_rdf_rest,X0,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,uri_ex_x) ),
inference(cnf_transformation,[],[f562]) ).
fof(f628,plain,
iext(uri_owl_equivalentClass,uri_ex_c,sK2),
inference(cnf_transformation,[],[f593]) ).
fof(f629,plain,
iext(uri_rdf_rest,sK0,uri_rdf_nil),
inference(cnf_transformation,[],[f593]) ).
fof(f630,plain,
iext(uri_rdf_first,sK0,uri_ex_y),
inference(cnf_transformation,[],[f593]) ).
fof(f631,plain,
iext(uri_rdf_rest,sK1,sK0),
inference(cnf_transformation,[],[f593]) ).
fof(f632,plain,
iext(uri_rdf_first,sK1,uri_ex_x),
inference(cnf_transformation,[],[f593]) ).
fof(f633,plain,
iext(uri_owl_unionOf,sK2,sK1),
inference(cnf_transformation,[],[f593]) ).
fof(f649,plain,
! [X2,X3,X0,X1,X6,X4] :
( ~ icext(X0,X6)
| icext(X4,X6)
| icext(X2,X6)
| ~ iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(cnf_transformation,[],[f601]) ).
fof(f650,plain,
! [X2,X3,X0,X1,X6,X4] :
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ icext(X4,X6)
| ~ iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| icext(X0,X6) ),
inference(cnf_transformation,[],[f601]) ).
fof(f651,plain,
! [X2,X3,X0,X1,X6,X4] :
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ icext(X2,X6)
| ~ iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| icext(X0,X6) ),
inference(cnf_transformation,[],[f601]) ).
fof(f652,plain,
! [X2,X3,X0,X1,X4] :
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ic(X4) ),
inference(cnf_transformation,[],[f601]) ).
fof(f653,plain,
! [X2,X3,X0,X1,X4] :
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ic(X2) ),
inference(cnf_transformation,[],[f601]) ).
fof(f655,plain,
! [X2,X3,X0,X1,X4] :
( ~ ic(X2)
| ~ ic(X0)
| iext(uri_owl_unionOf,X0,X1)
| ~ ic(X4)
| icext(X2,sK4(X0,X2,X4))
| icext(X4,sK4(X0,X2,X4))
| icext(X0,sK4(X0,X2,X4))
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(cnf_transformation,[],[f601]) ).
fof(f656,plain,
! [X2,X3,X0,X1,X4] :
( ~ ic(X2)
| ~ ic(X0)
| iext(uri_owl_unionOf,X0,X1)
| ~ ic(X4)
| ~ icext(X4,sK4(X0,X2,X4))
| ~ icext(X0,sK4(X0,X2,X4))
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(cnf_transformation,[],[f601]) ).
fof(f657,plain,
! [X2,X3,X0,X1,X4] :
( ~ ic(X2)
| ~ ic(X0)
| iext(uri_owl_unionOf,X0,X1)
| ~ ic(X4)
| ~ icext(X2,sK4(X0,X2,X4))
| ~ icext(X0,sK4(X0,X2,X4))
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(cnf_transformation,[],[f601]) ).
fof(f670,plain,
! [X3,X0,X1] :
( ~ icext(X0,X3)
| icext(X1,X3)
| ~ iext(uri_owl_equivalentClass,X0,X1) ),
inference(cnf_transformation,[],[f613]) ).
fof(f671,plain,
! [X3,X0,X1] :
( ~ icext(X1,X3)
| icext(X0,X3)
| ~ iext(uri_owl_equivalentClass,X0,X1) ),
inference(cnf_transformation,[],[f613]) ).
fof(f678,plain,
! [X0,X1] :
( ~ iext(uri_owl_equivalentClass,X0,X1)
| ic(X0) ),
inference(cnf_transformation,[],[f576]) ).
fof(f722,plain,
ic(uri_ex_c),
inference(resolution,[],[f678,f628]) ).
fof(f781,definition,
( spl13_2
<=> ic(uri_ex_y) ),
introduced(definition,[new_symbols(definition,[spl13_2])],[avatar_definition]) ).
fof(f782,plain,
( ~ ic(uri_ex_y)
| spl13_2 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f785,plain,
! [X2,X3,X0,X1,X4] :
( ~ iext(uri_rdf_rest,X3,sK0)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ icext(X0,X1)
| ~ iext(uri_rdf_first,sK0,X0)
| icext(X2,X1) ),
inference(resolution,[],[f650,f629]) ).
fof(f786,plain,
! [X2,X3,X0,X1] :
( ~ iext(uri_owl_unionOf,X0,sK1)
| ~ iext(uri_rdf_first,sK1,X1)
| ~ icext(X2,X3)
| ~ iext(uri_rdf_first,sK0,X2)
| icext(X0,X3) ),
inference(resolution,[],[f785,f631]) ).
fof(f788,definition,
( spl13_3
<=> ! [X1] : ~ iext(uri_rdf_first,sK1,X1) ),
introduced(definition,[new_symbols(definition,[spl13_3])],[avatar_definition]) ).
fof(f789,plain,
( ! [X1] : ~ iext(uri_rdf_first,sK1,X1)
| ~ spl13_3 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f791,definition,
( spl13_4
<=> ! [X2,X0,X3] :
( ~ iext(uri_owl_unionOf,X0,sK1)
| icext(X0,X3)
| ~ icext(X2,X3)
| ~ iext(uri_rdf_first,sK0,X2) ) ),
introduced(definition,[new_symbols(definition,[spl13_4])],[avatar_definition]) ).
fof(f792,plain,
( ! [X2,X3,X0] :
( ~ iext(uri_owl_unionOf,X0,sK1)
| icext(X0,X3)
| ~ icext(X2,X3)
| ~ iext(uri_rdf_first,sK0,X2) )
| ~ spl13_4 ),
inference(avatar_component_clause,[],[f791]) ).
fof(f793,plain,
( spl13_3
| spl13_4 ),
inference(avatar_split_clause,[],[f786,f791,f788]) ).
fof(f794,plain,
( $false
| ~ spl13_3 ),
inference(unit_resulting_resolution,[],[f789,f632]) ).
fof(f797,plain,
~ spl13_3,
inference(avatar_contradiction_clause,[],[f794]) ).
fof(f798,plain,
( ! [X0,X1] :
( ~ iext(uri_rdf_first,sK0,X1)
| ~ icext(X1,X0)
| icext(sK2,X0) )
| ~ spl13_4 ),
inference(resolution,[],[f792,f633]) ).
fof(f799,plain,
( ! [X0] :
( ~ icext(uri_ex_y,X0)
| icext(sK2,X0) )
| ~ spl13_4 ),
inference(resolution,[],[f798,f630]) ).
fof(f800,plain,
! [X2,X3,X0,X1,X4] :
( ~ icext(X0,X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X0)
| ~ iext(uri_rdf_rest,X3,sK0)
| ~ iext(uri_rdf_first,sK0,X4)
| icext(X2,X1) ),
inference(resolution,[],[f651,f629]) ).
fof(f802,definition,
( spl13_5
<=> ! [X4] : ~ iext(uri_rdf_first,sK0,X4) ),
introduced(definition,[new_symbols(definition,[spl13_5])],[avatar_definition]) ).
fof(f803,plain,
( ! [X4] : ~ iext(uri_rdf_first,sK0,X4)
| ~ spl13_5 ),
inference(avatar_component_clause,[],[f802]) ).
fof(f805,definition,
( spl13_6
<=> ! [X0,X3,X2,X1] :
( ~ icext(X0,X1)
| icext(X2,X1)
| ~ iext(uri_rdf_rest,X3,sK0)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl13_6])],[avatar_definition]) ).
fof(f806,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(uri_rdf_rest,X3,sK0)
| icext(X2,X1)
| ~ icext(X0,X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X0) )
| ~ spl13_6 ),
inference(avatar_component_clause,[],[f805]) ).
fof(f807,plain,
( spl13_5
| spl13_6 ),
inference(avatar_split_clause,[],[f800,f805,f802]) ).
fof(f808,plain,
( $false
| ~ spl13_5 ),
inference(unit_resulting_resolution,[],[f803,f630]) ).
fof(f811,plain,
~ spl13_5,
inference(avatar_contradiction_clause,[],[f808]) ).
fof(f812,plain,
( ! [X2,X0,X1] :
( ~ iext(uri_owl_unionOf,X0,sK1)
| ~ icext(X2,X1)
| icext(X0,X1)
| ~ iext(uri_rdf_first,sK1,X2) )
| ~ spl13_6 ),
inference(resolution,[],[f806,f631]) ).
fof(f813,plain,
( ! [X0,X1] :
( ~ iext(uri_rdf_first,sK1,X0)
| icext(sK2,X1)
| ~ icext(X0,X1) )
| ~ spl13_6 ),
inference(resolution,[],[f812,f633]) ).
fof(f814,plain,
( ! [X0] :
( ~ icext(uri_ex_x,X0)
| icext(sK2,X0) )
| ~ spl13_6 ),
inference(resolution,[],[f813,f632]) ).
fof(f826,plain,
! [X2,X3,X0,X1] :
( ~ iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,sK0)
| ~ iext(uri_rdf_first,sK0,X3)
| ic(X2) ),
inference(resolution,[],[f653,f629]) ).
fof(f828,definition,
( spl13_7
<=> ! [X2,X0,X1] :
( ~ iext(uri_owl_unionOf,X0,X1)
| ic(X2)
| ~ iext(uri_rdf_rest,X1,sK0)
| ~ iext(uri_rdf_first,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl13_7])],[avatar_definition]) ).
fof(f829,plain,
( ! [X2,X0,X1] :
( ~ iext(uri_rdf_rest,X1,sK0)
| ic(X2)
| ~ iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_first,X1,X2) )
| ~ spl13_7 ),
inference(avatar_component_clause,[],[f828]) ).
fof(f830,plain,
( spl13_5
| spl13_7 ),
inference(avatar_split_clause,[],[f826,f828,f802]) ).
fof(f831,plain,
( ! [X0,X1] :
( ic(X0)
| ~ iext(uri_owl_unionOf,X1,sK1)
| ~ iext(uri_rdf_first,sK1,X0) )
| ~ spl13_7 ),
inference(resolution,[],[f829,f631]) ).
fof(f833,definition,
( spl13_8
<=> ! [X1] : ~ iext(uri_owl_unionOf,X1,sK1) ),
introduced(definition,[new_symbols(definition,[spl13_8])],[avatar_definition]) ).
fof(f834,plain,
( ! [X1] : ~ iext(uri_owl_unionOf,X1,sK1)
| ~ spl13_8 ),
inference(avatar_component_clause,[],[f833]) ).
fof(f836,definition,
( spl13_9
<=> ! [X0] :
( ic(X0)
| ~ iext(uri_rdf_first,sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl13_9])],[avatar_definition]) ).
fof(f837,plain,
( ! [X0] :
( ~ iext(uri_rdf_first,sK1,X0)
| ic(X0) )
| ~ spl13_9 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f838,plain,
( spl13_8
| spl13_9
| ~ spl13_7 ),
inference(avatar_split_clause,[],[f831,f828,f836,f833]) ).
fof(f839,plain,
( $false
| ~ spl13_8 ),
inference(unit_resulting_resolution,[],[f834,f633]) ).
fof(f842,plain,
~ spl13_8,
inference(avatar_contradiction_clause,[],[f839]) ).
fof(f843,plain,
( ic(uri_ex_x)
| ~ spl13_9 ),
inference(resolution,[],[f837,f632]) ).
fof(f844,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| iext(uri_owl_unionOf,X0,X1)
| ~ ic(X2)
| icext(uri_ex_x,sK4(X0,uri_ex_x,X2))
| icext(X2,sK4(X0,uri_ex_x,X2))
| icext(X0,sK4(X0,uri_ex_x,X2))
| ~ iext(uri_rdf_first,X1,uri_ex_x)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X2)
| ~ ic(X0) )
| ~ spl13_9 ),
inference(resolution,[],[f843,f655]) ).
fof(f845,plain,
( ! [X2,X3,X0,X1] :
( ~ icext(X2,sK4(X0,uri_ex_x,X2))
| iext(uri_owl_unionOf,X0,X1)
| ~ ic(X2)
| ~ ic(X0)
| ~ icext(X0,sK4(X0,uri_ex_x,X2))
| ~ iext(uri_rdf_first,X1,uri_ex_x)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X2)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) )
| ~ spl13_9 ),
inference(resolution,[],[f843,f656]) ).
fof(f846,plain,
( ! [X2,X3,X0,X1] :
( ~ icext(uri_ex_x,sK4(X0,uri_ex_x,X2))
| iext(uri_owl_unionOf,X0,X1)
| ~ ic(X2)
| ~ ic(X0)
| ~ icext(X0,sK4(X0,uri_ex_x,X2))
| ~ iext(uri_rdf_first,X1,uri_ex_x)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X3,X2)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) )
| ~ spl13_9 ),
inference(resolution,[],[f843,f657]) ).
fof(f850,plain,
( ! [X2,X0,X1] :
( ~ iext(uri_rdf_rest,X1,sK0)
| ~ ic(X2)
| icext(uri_ex_x,sK4(X0,uri_ex_x,X2))
| icext(X2,sK4(X0,uri_ex_x,X2))
| icext(X0,sK4(X0,uri_ex_x,X2))
| ~ iext(uri_rdf_first,X1,uri_ex_x)
| iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_first,sK0,X2)
| ~ ic(X0) )
| ~ spl13_9 ),
inference(resolution,[],[f844,f629]) ).
fof(f851,plain,
( ! [X0,X1] :
( ~ ic(X0)
| icext(uri_ex_x,sK4(X1,uri_ex_x,X0))
| icext(X0,sK4(X1,uri_ex_x,X0))
| icext(X1,sK4(X1,uri_ex_x,X0))
| ~ iext(uri_rdf_first,sK1,uri_ex_x)
| iext(uri_owl_unionOf,X1,sK1)
| ~ iext(uri_rdf_first,sK0,X0)
| ~ ic(X1) )
| ~ spl13_9 ),
inference(resolution,[],[f850,f631]) ).
fof(f852,plain,
( ! [X0,X1] :
( ~ iext(uri_rdf_first,sK0,X0)
| icext(uri_ex_x,sK4(X1,uri_ex_x,X0))
| icext(X0,sK4(X1,uri_ex_x,X0))
| icext(X1,sK4(X1,uri_ex_x,X0))
| iext(uri_owl_unionOf,X1,sK1)
| ~ ic(X0)
| ~ ic(X1) )
| ~ spl13_9 ),
inference(forward_subsumption_resolution,[],[f851,f632]) ).
fof(f853,plain,
( ! [X0] :
( icext(uri_ex_x,sK4(X0,uri_ex_x,uri_ex_y))
| icext(uri_ex_y,sK4(X0,uri_ex_x,uri_ex_y))
| icext(X0,sK4(X0,uri_ex_x,uri_ex_y))
| iext(uri_owl_unionOf,X0,sK1)
| ~ ic(uri_ex_y)
| ~ ic(X0) )
| ~ spl13_9 ),
inference(resolution,[],[f852,f630]) ).
fof(f856,plain,
( $false
| spl13_2 ),
inference(unit_resulting_resolution,[],[f652,f782,f630,f633,f632,f631,f629]) ).
fof(f857,plain,
! [X2,X3,X0,X1] :
( ~ iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,sK0)
| ~ iext(uri_rdf_first,sK0,X3)
| ic(X3) ),
inference(resolution,[],[f652,f629]) ).
fof(f858,plain,
spl13_2,
inference(avatar_contradiction_clause,[],[f856]) ).
fof(f860,definition,
( spl13_10
<=> ! [X3] :
( ~ iext(uri_rdf_first,sK0,X3)
| ic(X3) ) ),
introduced(definition,[new_symbols(definition,[spl13_10])],[avatar_definition]) ).
fof(f861,plain,
( ! [X3] :
( ~ iext(uri_rdf_first,sK0,X3)
| ic(X3) )
| ~ spl13_10 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f863,definition,
( spl13_11
<=> ! [X2,X0,X1] :
( ~ iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_rest,X1,sK0)
| ~ iext(uri_rdf_first,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl13_11])],[avatar_definition]) ).
fof(f864,plain,
( ! [X2,X0,X1] :
( ~ iext(uri_rdf_rest,X1,sK0)
| ~ iext(uri_owl_unionOf,X0,X1)
| ~ iext(uri_rdf_first,X1,X2) )
| ~ spl13_11 ),
inference(avatar_component_clause,[],[f863]) ).
fof(f865,plain,
( spl13_10
| spl13_11 ),
inference(avatar_split_clause,[],[f857,f863,f860]) ).
fof(f867,definition,
( spl13_12
<=> ! [X0] :
( icext(uri_ex_x,sK4(X0,uri_ex_x,uri_ex_y))
| ~ ic(X0)
| iext(uri_owl_unionOf,X0,sK1)
| icext(X0,sK4(X0,uri_ex_x,uri_ex_y))
| icext(uri_ex_y,sK4(X0,uri_ex_x,uri_ex_y)) ) ),
introduced(definition,[new_symbols(definition,[spl13_12])],[avatar_definition]) ).
fof(f868,plain,
( ! [X0] :
( ~ ic(X0)
| icext(uri_ex_x,sK4(X0,uri_ex_x,uri_ex_y))
| iext(uri_owl_unionOf,X0,sK1)
| icext(X0,sK4(X0,uri_ex_x,uri_ex_y))
| icext(uri_ex_y,sK4(X0,uri_ex_x,uri_ex_y)) )
| ~ spl13_12 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f869,plain,
( ~ spl13_2
| spl13_12
| ~ spl13_9 ),
inference(avatar_split_clause,[],[f853,f836,f867,f781]) ).
fof(f870,plain,
( icext(uri_ex_x,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| iext(uri_owl_unionOf,uri_ex_c,sK1)
| icext(uri_ex_c,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| icext(uri_ex_y,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ spl13_12 ),
inference(resolution,[],[f868,f722]) ).
fof(f885,definition,
( spl13_16
<=> icext(uri_ex_y,sK4(uri_ex_c,uri_ex_x,uri_ex_y)) ),
introduced(definition,[new_symbols(definition,[spl13_16])],[avatar_definition]) ).
fof(f886,plain,
( icext(uri_ex_y,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ spl13_16 ),
inference(avatar_component_clause,[],[f885]) ).
fof(f888,definition,
( spl13_17
<=> icext(uri_ex_c,sK4(uri_ex_c,uri_ex_x,uri_ex_y)) ),
introduced(definition,[new_symbols(definition,[spl13_17])],[avatar_definition]) ).
fof(f889,plain,
( icext(uri_ex_c,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ spl13_17 ),
inference(avatar_component_clause,[],[f888]) ).
fof(f891,definition,
( spl13_18
<=> iext(uri_owl_unionOf,uri_ex_c,sK1) ),
introduced(definition,[new_symbols(definition,[spl13_18])],[avatar_definition]) ).
fof(f892,plain,
( iext(uri_owl_unionOf,uri_ex_c,sK1)
| ~ spl13_18 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f894,definition,
( spl13_19
<=> icext(uri_ex_x,sK4(uri_ex_c,uri_ex_x,uri_ex_y)) ),
introduced(definition,[new_symbols(definition,[spl13_19])],[avatar_definition]) ).
fof(f895,plain,
( icext(uri_ex_x,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ spl13_19 ),
inference(avatar_component_clause,[],[f894]) ).
fof(f896,plain,
( spl13_16
| spl13_17
| spl13_18
| spl13_19
| ~ spl13_12 ),
inference(avatar_split_clause,[],[f870,f867,f894,f891,f888,f885]) ).
fof(f897,plain,
( icext(sK2,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ spl13_4
| ~ spl13_16 ),
inference(resolution,[],[f886,f799]) ).
fof(f898,plain,
( ! [X0,X1] :
( iext(uri_owl_unionOf,uri_ex_c,X0)
| ~ ic(uri_ex_y)
| ~ ic(uri_ex_c)
| ~ icext(uri_ex_c,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_rest,X0,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) )
| ~ spl13_9
| ~ spl13_16 ),
inference(resolution,[],[f886,f845]) ).
fof(f904,plain,
( ! [X0,X1] :
( iext(uri_owl_unionOf,uri_ex_c,X0)
| ~ ic(uri_ex_y)
| ~ icext(uri_ex_c,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_rest,X0,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) )
| ~ spl13_9
| ~ spl13_16 ),
inference(forward_subsumption_resolution,[],[f898,f722]) ).
fof(f905,plain,
( ! [X0,X1] :
( ~ ic(uri_ex_y)
| ~ icext(uri_ex_c,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_rest,X0,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) )
| ~ spl13_9
| ~ spl13_16 ),
inference(forward_subsumption_resolution,[],[f904,f627]) ).
fof(f907,definition,
( spl13_20
<=> ! [X0,X1] :
( ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl13_20])],[avatar_definition]) ).
fof(f908,plain,
( ! [X0,X1] :
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X0,X1) )
| ~ spl13_20 ),
inference(avatar_component_clause,[],[f907]) ).
fof(f909,plain,
( ~ icext(uri_ex_c,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| spl13_17 ),
inference(avatar_component_clause,[],[f888]) ).
fof(f910,plain,
( spl13_20
| ~ spl13_17
| ~ spl13_2
| ~ spl13_9
| ~ spl13_16 ),
inference(avatar_split_clause,[],[f905,f885,f836,f781,f888,f907]) ).
fof(f934,plain,
( $false
| ~ spl13_4
| ~ spl13_16
| spl13_17 ),
inference(unit_resulting_resolution,[],[f671,f628,f897,f909]) ).
fof(f935,plain,
( ~ spl13_4
| ~ spl13_16
| spl13_17 ),
inference(avatar_contradiction_clause,[],[f934]) ).
fof(f939,plain,
( ! [X0] :
( ~ iext(uri_owl_equivalentClass,uri_ex_c,X0)
| icext(X0,sK4(uri_ex_c,uri_ex_x,uri_ex_y)) )
| ~ spl13_17 ),
inference(resolution,[],[f889,f670]) ).
fof(f994,plain,
( $false
| ~ spl13_11 ),
inference(unit_resulting_resolution,[],[f864,f632,f633,f631]) ).
fof(f996,plain,
~ spl13_11,
inference(avatar_contradiction_clause,[],[f994]) ).
fof(f998,plain,
( ic(uri_ex_y)
| ~ spl13_10 ),
inference(resolution,[],[f861,f630]) ).
fof(f1127,plain,
( icext(sK2,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ spl13_17 ),
inference(resolution,[],[f939,f628]) ).
fof(f1130,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(uri_owl_unionOf,sK2,X2)
| icext(X1,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| icext(X0,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,X2,X1)
| ~ iext(uri_rdf_rest,X2,X3)
| ~ iext(uri_rdf_first,X3,X0)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) )
| ~ spl13_17 ),
inference(resolution,[],[f1127,f649]) ).
fof(f1243,plain,
( ! [X2,X0,X1] :
( icext(X0,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| icext(X1,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,sK1,X0)
| ~ iext(uri_rdf_rest,sK1,X2)
| ~ iext(uri_rdf_first,X2,X1)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) )
| ~ spl13_17 ),
inference(resolution,[],[f1130,f633]) ).
fof(f1245,definition,
( spl13_54
<=> ! [X2,X1] :
( icext(X1,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_rest,sK1,X2)
| ~ iext(uri_rdf_first,X2,X1) ) ),
introduced(definition,[new_symbols(definition,[spl13_54])],[avatar_definition]) ).
fof(f1246,plain,
( ! [X2,X1] :
( ~ iext(uri_rdf_rest,sK1,X2)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| icext(X1,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,X2,X1) )
| ~ spl13_54 ),
inference(avatar_component_clause,[],[f1245]) ).
fof(f1248,definition,
( spl13_55
<=> ! [X0] :
( icext(X0,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,sK1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl13_55])],[avatar_definition]) ).
fof(f1249,plain,
( ! [X0] :
( ~ iext(uri_rdf_first,sK1,X0)
| icext(X0,sK4(uri_ex_c,uri_ex_x,uri_ex_y)) )
| ~ spl13_55 ),
inference(avatar_component_clause,[],[f1248]) ).
fof(f1250,plain,
( spl13_54
| spl13_55
| ~ spl13_17 ),
inference(avatar_split_clause,[],[f1243,f888,f1248,f1245]) ).
fof(f1251,plain,
( icext(uri_ex_x,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ spl13_55 ),
inference(resolution,[],[f1249,f632]) ).
fof(f1252,plain,
( spl13_19
| ~ spl13_55 ),
inference(avatar_split_clause,[],[f1251,f1248,f894]) ).
fof(f1253,plain,
( ! [X0] :
( ~ iext(uri_rdf_rest,sK0,uri_rdf_nil)
| icext(X0,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,sK0,X0) )
| ~ spl13_54 ),
inference(resolution,[],[f1246,f631]) ).
fof(f1254,plain,
( ! [X0] :
( ~ iext(uri_rdf_first,sK0,X0)
| icext(X0,sK4(uri_ex_c,uri_ex_x,uri_ex_y)) )
| ~ spl13_54 ),
inference(forward_subsumption_resolution,[],[f1253,f629]) ).
fof(f1255,plain,
( icext(uri_ex_y,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ spl13_54 ),
inference(resolution,[],[f1254,f630]) ).
fof(f1256,plain,
( spl13_16
| ~ spl13_54 ),
inference(avatar_split_clause,[],[f1255,f1245,f885]) ).
fof(f1257,plain,
( ! [X0,X1] :
( iext(uri_owl_unionOf,uri_ex_c,X0)
| ~ ic(uri_ex_y)
| ~ ic(uri_ex_c)
| ~ icext(uri_ex_c,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_rest,X0,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) )
| ~ spl13_9
| ~ spl13_19 ),
inference(resolution,[],[f895,f846]) ).
fof(f1258,plain,
( icext(sK2,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ spl13_6
| ~ spl13_19 ),
inference(resolution,[],[f895,f814]) ).
fof(f1264,plain,
( ! [X0,X1] :
( iext(uri_owl_unionOf,uri_ex_c,X0)
| ~ ic(uri_ex_c)
| ~ icext(uri_ex_c,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_rest,X0,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) )
| ~ spl13_9
| ~ spl13_10
| ~ spl13_19 ),
inference(forward_subsumption_resolution,[],[f1257,f998]) ).
fof(f1265,plain,
( ! [X0,X1] :
( iext(uri_owl_unionOf,uri_ex_c,X0)
| ~ icext(uri_ex_c,sK4(uri_ex_c,uri_ex_x,uri_ex_y))
| ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_rest,X0,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) )
| ~ spl13_9
| ~ spl13_10
| ~ spl13_19 ),
inference(forward_subsumption_resolution,[],[f1264,f722]) ).
fof(f1266,plain,
( ! [X0,X1] :
( iext(uri_owl_unionOf,uri_ex_c,X0)
| ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_rest,X0,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) )
| ~ spl13_9
| ~ spl13_10
| ~ spl13_17
| ~ spl13_19 ),
inference(forward_subsumption_resolution,[],[f1265,f889]) ).
fof(f1267,plain,
( ! [X0,X1] :
( ~ iext(uri_rdf_first,X0,uri_ex_x)
| ~ iext(uri_rdf_rest,X0,X1)
| ~ iext(uri_rdf_first,X1,uri_ex_y)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) )
| ~ spl13_9
| ~ spl13_10
| ~ spl13_17
| ~ spl13_19 ),
inference(forward_subsumption_resolution,[],[f1266,f627]) ).
fof(f1268,plain,
( spl13_20
| ~ spl13_9
| ~ spl13_10
| ~ spl13_17
| ~ spl13_19 ),
inference(avatar_split_clause,[],[f1267,f894,f888,f860,f836,f907]) ).
fof(f1270,plain,
( $false
| ~ spl13_20 ),
inference(unit_resulting_resolution,[],[f908,f631,f632,f630,f629]) ).
fof(f1272,plain,
~ spl13_20,
inference(avatar_contradiction_clause,[],[f1270]) ).
fof(f1274,plain,
( $false
| ~ spl13_18 ),
inference(unit_resulting_resolution,[],[f627,f631,f629,f630,f632,f892]) ).
fof(f1281,plain,
~ spl13_18,
inference(avatar_contradiction_clause,[],[f1274]) ).
fof(f1283,plain,
( $false
| ~ spl13_6
| spl13_17
| ~ spl13_19 ),
inference(unit_resulting_resolution,[],[f671,f628,f909,f1258]) ).
fof(f1289,plain,
( ~ spl13_6
| spl13_17
| ~ spl13_19 ),
inference(avatar_contradiction_clause,[],[f1283]) ).
cnf(s2,plain,
( spl13_3
| spl13_4 ),
inference(sat_conversion,[],[f793]) ).
cnf(s4,plain,
~ spl13_3,
inference(sat_conversion,[],[f797]) ).
cnf(s5,plain,
( spl13_5
| spl13_6 ),
inference(sat_conversion,[],[f807]) ).
cnf(s7,plain,
~ spl13_5,
inference(sat_conversion,[],[f811]) ).
cnf(s8,plain,
( spl13_5
| spl13_7 ),
inference(sat_conversion,[],[f830]) ).
cnf(s9,plain,
( ~ spl13_7
| spl13_8
| spl13_9 ),
inference(sat_conversion,[],[f838]) ).
cnf(s11,plain,
~ spl13_8,
inference(sat_conversion,[],[f842]) ).
cnf(s12,plain,
spl13_2,
inference(sat_conversion,[],[f858]) ).
cnf(s13,plain,
( spl13_10
| spl13_11 ),
inference(sat_conversion,[],[f865]) ).
cnf(s14,plain,
( ~ spl13_2
| ~ spl13_9
| spl13_12 ),
inference(sat_conversion,[],[f869]) ).
cnf(s16,plain,
( ~ spl13_12
| spl13_16
| spl13_17
| spl13_18
| spl13_19 ),
inference(sat_conversion,[],[f896]) ).
cnf(s17,plain,
( ~ spl13_2
| ~ spl13_9
| ~ spl13_16
| ~ spl13_17
| spl13_20 ),
inference(sat_conversion,[],[f910]) ).
cnf(s19,plain,
( ~ spl13_4
| ~ spl13_16
| spl13_17 ),
inference(sat_conversion,[],[f935]) ).
cnf(s23,plain,
~ spl13_11,
inference(sat_conversion,[],[f996]) ).
cnf(s46,plain,
( ~ spl13_17
| spl13_54
| spl13_55 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s47,plain,
( spl13_19
| ~ spl13_55 ),
inference(sat_conversion,[],[f1252]) ).
cnf(s48,plain,
( spl13_16
| ~ spl13_54 ),
inference(sat_conversion,[],[f1256]) ).
cnf(s49,plain,
( ~ spl13_9
| ~ spl13_10
| ~ spl13_17
| ~ spl13_19
| spl13_20 ),
inference(sat_conversion,[],[f1268]) ).
cnf(s50,plain,
~ spl13_20,
inference(sat_conversion,[],[f1272]) ).
cnf(s51,plain,
~ spl13_18,
inference(sat_conversion,[],[f1281]) ).
cnf(s52,plain,
( ~ spl13_6
| spl13_17
| ~ spl13_19 ),
inference(sat_conversion,[],[f1289]) ).
cnf(s53,plain,
( ~ spl13_9
| ~ spl13_10
| ~ spl13_17
| ~ spl13_19 ),
inference(rat,[],[s49,s50]) ).
cnf(s54,plain,
( ~ spl13_2
| ~ spl13_9
| ~ spl13_16
| ~ spl13_17 ),
inference(rat,[],[s17,s50]) ).
cnf(s55,plain,
( ~ spl13_12
| spl13_16
| spl13_17
| spl13_19 ),
inference(rat,[],[s16,s51]) ).
cnf(s56,plain,
spl13_10,
inference(rat,[],[s13,s23]) ).
cnf(s57,plain,
( ~ spl13_7
| spl13_9 ),
inference(rat,[],[s9,s11]) ).
cnf(s60,plain,
spl13_7,
inference(rat,[],[s8,s7]) ).
cnf(s61,plain,
spl13_9,
inference(rat,[],[s57,s60]) ).
cnf(s62,plain,
spl13_12,
inference(rat,[],[s14,s12,s61]) ).
cnf(s63,plain,
spl13_6,
inference(rat,[],[s5,s7]) ).
cnf(s66,plain,
spl13_4,
inference(rat,[],[s2,s4]) ).
cnf(s68,plain,
( spl13_17
| spl13_16 ),
inference(rat,[],[s55,s52,s62,s63]) ).
cnf(s69,plain,
spl13_16,
inference(rat,[],[s47,s46,s53,s68,s48,s56,s61]) ).
cnf(s70,plain,
spl13_17,
inference(rat,[],[s19,s66,s69]) ).
cnf(s71,plain,
$false,
inference(rat,[],[s54,s61,s12,s70,s69]) ).
fof(f1290,plain,
$false,
inference(avatar_sat_refutation,[],[s71]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB041+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n016.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 07:15:18 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 11.18/2.70 % (3451048)Detected formulas, will run a generic FOF schedule.
% 11.18/2.70 % (3451094)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=753752008:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.18/2.70 % (3451101)dis-21_1_sil=8000:lcm=predicate:random_seed=1619159691: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)
% 11.18/2.70 % (3451101)Instruction limit reached!
% 11.18/2.70 % (3451101)------------------------------
% 11.18/2.70 % (3451101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451101)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451101)Termination reason: Instruction limit
% 11.18/2.70 % (3451101)Termination phase: Saturation
% 11.18/2.70 % (3451101)Time elapsed: 0.076 s
% 11.18/2.70 % (3451101)Peak memory usage: 91 MB
% 11.18/2.70 % (3451101)Instructions burned: 129 (million)
% 11.18/2.70 % (3451098)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2008989871:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.18/2.70 % (3451100)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3361780246:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.18/2.70 % (3451097)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=3845348194:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.18/2.70 % (3451096)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=1665585595:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.18/2.70 % (3451098)Refutation not found, incomplete strategy
% 11.18/2.70 % (3451098)------------------------------
% 11.18/2.70 % (3451098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451098)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451098)Termination reason: Refutation not found, incomplete strategy
% 11.18/2.70 % (3451098)Time elapsed: 0.010 s
% 11.18/2.70 % (3451098)Peak memory usage: 88 MB
% 11.18/2.70 % (3451098)Instructions burned: 9 (million)
% 11.18/2.70 % (3451099)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4002638792:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.18/2.70 % (3451099)Instruction limit reached!
% 11.18/2.70 % (3451099)------------------------------
% 11.18/2.70 % (3451099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451099)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451099)Termination reason: Instruction limit
% 11.18/2.70 % (3451099)Termination phase: Saturation
% 11.18/2.70 % (3451099)Time elapsed: 0.112 s
% 11.18/2.70 % (3451099)Peak memory usage: 89 MB
% 11.18/2.70 % (3451099)Instructions burned: 119 (million)
% 11.18/2.70 % (3451100)Instruction limit reached!
% 11.18/2.70 % (3451100)------------------------------
% 11.18/2.70 % (3451100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451100)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451100)Termination reason: Instruction limit
% 11.18/2.70 % (3451100)Termination phase: Saturation
% 11.18/2.70 % (3451100)Time elapsed: 0.147 s
% 11.18/2.70 % (3451100)Peak memory usage: 91 MB
% 11.18/2.70 % (3451100)Instructions burned: 139 (million)
% 11.18/2.70 % (3451109)lrs+10_1_sil=8000:sp=occurrence:random_seed=4162838853:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.18/2.70 % (3451098)------------------------------
% 11.18/2.70 % (3451098)------------------------------
% 11.18/2.70 % (3451116)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1916487076:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 11.18/2.70 % (3451116)Refutation not found, incomplete strategy
% 11.18/2.70 % (3451116)------------------------------
% 11.18/2.70 % (3451116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451116)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451116)Termination reason: Refutation not found, incomplete strategy
% 11.18/2.70 % (3451116)Time elapsed: 0.010 s
% 11.18/2.70 % (3451116)Peak memory usage: 89 MB
% 11.18/2.70 % (3451116)Instructions burned: 11 (million)
% 11.18/2.70 % (3451115)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2359486557:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 11.18/2.70 % (3451115)Refutation not found, incomplete strategy
% 11.18/2.70 % (3451115)------------------------------
% 11.18/2.70 % (3451115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451115)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451115)Termination reason: Refutation not found, incomplete strategy
% 11.18/2.70 % (3451115)Time elapsed: 0.014 s
% 11.18/2.70 % (3451115)Peak memory usage: 89 MB
% 11.18/2.70 % (3451115)Instructions burned: 13 (million)
% 11.18/2.70 % (3451109)Instruction limit reached!
% 11.18/2.70 % (3451109)------------------------------
% 11.18/2.70 % (3451109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451109)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451109)Termination reason: Instruction limit
% 11.18/2.70 % (3451109)Termination phase: Saturation
% 11.18/2.70 % (3451109)Time elapsed: 0.269 s
% 11.18/2.70 % (3451109)Peak memory usage: 92 MB
% 11.18/2.70 % (3451109)Instructions burned: 286 (million)
% 11.18/2.70 % (3451126)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=1034964520:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 11.18/2.70 % (3451116)------------------------------
% 11.18/2.70 % (3451116)------------------------------
% 11.18/2.70 % (3451128)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2015303951:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 11.18/2.70 % (3451128)Refutation not found, incomplete strategy
% 11.18/2.70 % (3451128)------------------------------
% 11.18/2.70 % (3451128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451128)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451128)Termination reason: Refutation not found, incomplete strategy
% 11.18/2.70 % (3451128)Time elapsed: 0.013 s
% 11.18/2.70 % (3451128)Peak memory usage: 89 MB
% 11.18/2.70 % (3451115)------------------------------
% 11.18/2.70 % (3451115)------------------------------
% 11.18/2.70 % (3451128)Instructions burned: 12 (million)
% 11.18/2.70 % (3451126)Instruction limit reached!
% 11.18/2.70 % (3451126)------------------------------
% 11.18/2.70 % (3451126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451126)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451126)Termination reason: Instruction limit
% 11.18/2.70 % (3451126)Termination phase: Saturation
% 11.18/2.70 % (3451126)Time elapsed: 0.221 s
% 11.18/2.70 % (3451126)Peak memory usage: 93 MB
% 11.18/2.70 % (3451126)Instructions burned: 248 (million)
% 11.18/2.70 % (3451132)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2264997859:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 11.18/2.70 % (3451135)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1779711073:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 11.18/2.70 % (3451096)First to succeed.
% 11.18/2.70 % (3451096)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3451048"
% 11.18/2.70 % (3451137)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2447352075:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 11.18/2.70 % (3451128)------------------------------
% 11.18/2.70 % (3451128)------------------------------
% 11.18/2.70 % (3451135)Instruction limit reached!
% 11.18/2.70 % (3451135)------------------------------
% 11.18/2.70 % (3451135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451135)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451135)Termination reason: Instruction limit
% 11.18/2.70 % (3451135)Termination phase: Saturation
% 11.18/2.70 % (3451135)Time elapsed: 0.117 s
% 11.18/2.70 % (3451135)Peak memory usage: 90 MB
% 11.18/2.70 % (3451135)Instructions burned: 114 (million)
% 11.18/2.70 % (3451137)Instruction limit reached!
% 11.18/2.70 % (3451137)------------------------------
% 11.18/2.70 % (3451137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.70 % (3451137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.70 % (3451137)CaDiCaL version: 2.1.3
% 11.18/2.70 % (3451137)Termination reason: Instruction limit
% 11.18/2.70 % (3451137)Termination phase: Saturation
% 11.18/2.70 % (3451137)Time elapsed: 0.108 s
% 11.18/2.70 % (3451137)Peak memory usage: 90 MB
% 11.18/2.70 % (3451137)Instructions burned: 127 (million)
% 11.18/2.70 % (3451145)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1972281858:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 11.18/2.70 % (3451146)lrs+10_1_sil=8000:sp=occurrence:random_seed=378117477:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 11.18/2.70 % (3451096)Refutation found. Thanks to Tanya!
% 11.18/2.70 % SZS status Theorem for theBenchmark
% 11.18/2.70 % SZS output start Proof for theBenchmark
% See solution above
% 13.50/2.91 % (3451096)------------------------------
% 13.50/2.91 % (3451096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.50/2.91 % (3451096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.50/2.91 % (3451096)CaDiCaL version: 2.1.3
% 13.50/2.91 % (3451096)Termination reason: Refutation
% 13.50/2.91 % (3451096)Time elapsed: 1.183 s
% 13.50/2.91 % (3451096)Peak memory usage: 131 MB
% 13.50/2.91 % (3451096)Instructions burned: 1107 (million)
% 13.50/2.91 % (3451096)------------------------------
% 13.50/2.91 % (3451096)------------------------------
% 13.50/2.91 % (3451048)Success in time 1.83 s
% 13.50/2.91 % Vampire exiting
%------------------------------------------------------------------------------