%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB031+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:00:49 PM UTC 2026
% Result : Unsatisfiable 80.03s 23.04s
% Output : Refutation 80.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 17
% Syntax : Number of formulae : 98 ( 41 unt; 0 def)
% Number of atoms : 347 ( 25 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 398 ( 149 ~; 157 |; 75 &)
% ( 15 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 17 con; 0-2 aty)
% Number of variables : 154 ( 137 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] : ir(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',simple_ir) ).
fof(f54,axiom,
! [X0] :
( ic(X0)
<=> icext(uri_rdfs_Class,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',rdfs_ic_def) ).
fof(f122,axiom,
ic(uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_class_classrdfs_type) ).
fof(f145,axiom,
! [X0] : ~ icext(uri_owl_Nothing,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_class_nothing_ext) ).
fof(f153,axiom,
! [X0] :
( icext(uri_rdf_Property,X0)
<=> ip(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_class_property_ext) ).
fof(f154,axiom,
ic(uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_class_property_type) ).
fof(f163,axiom,
! [X0] :
( icext(uri_owl_Thing,X0)
<=> ir(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_class_thing_ext) ).
fof(f168,axiom,
ip(uri_owl_allValuesFrom),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_prop_allvaluesfrom_type) ).
fof(f182,axiom,
! [X0,X1] : ~ iext(uri_owl_bottomObjectProperty,X0,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_prop_bottomobjectproperty_ext) ).
fof(f183,axiom,
ip(uri_owl_bottomObjectProperty),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_prop_bottomobjectproperty_type) ).
fof(f255,axiom,
ip(uri_owl_sameAs),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_prop_sameas_type) ).
fof(f287,axiom,
! [X0] :
( iext(uri_owl_unionOf,X0,uri_rdf_nil)
<=> ( ic(X0)
& ! [X1] : ~ icext(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_bool_unionof_class_000) ).
fof(f295,axiom,
! [X0,X1,X2] :
( ( iext(uri_rdf_first,X1,X2)
& iext(uri_rdf_rest,X1,uri_rdf_nil) )
=> ( iext(uri_owl_oneOf,X0,X1)
<=> ( ic(X0)
& ! [X3] :
( icext(X0,X3)
<=> X3 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_enum_class_001) ).
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/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_eqdis_equivalentclass) ).
fof(f354,axiom,
! [X0,X1] :
( iext(uri_owl_sameAs,X0,X1)
<=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_eqdis_sameas) ).
fof(f392,axiom,
! [X0] :
( icext(uri_owl_AsymmetricProperty,X0)
<=> ( ip(X0)
& ! [X1,X2] :
( iext(X0,X1,X2)
=> ~ iext(X0,X2,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_char_asymmetric) ).
fof(f559,axiom,
? [X0,X1] :
( iext(uri_owl_equivalentClass,uri_owl_Thing,X0)
& iext(uri_owl_oneOf,X0,X1)
& iext(uri_rdf_first,X1,uri_ex_w)
& iext(uri_rdf_rest,X1,uri_rdf_nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_031_Large_Universe) ).
fof(f694,plain,
! [X0,X1,X2] :
( ( iext(uri_owl_oneOf,X0,X1)
<=> ( ic(X0)
& ! [X3] :
( icext(X0,X3)
<=> X3 = X2 ) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(ennf_transformation,[],[f295]) ).
fof(f695,plain,
! [X0,X1,X2] :
( ( iext(uri_owl_oneOf,X0,X1)
<=> ( ic(X0)
& ! [X3] :
( icext(X0,X3)
<=> X3 = X2 ) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(flattening,[],[f694]) ).
fof(f844,plain,
! [X0] :
( icext(uri_owl_AsymmetricProperty,X0)
<=> ( ip(X0)
& ! [X1,X2] :
( ~ iext(X0,X2,X1)
| ~ iext(X0,X1,X2) ) ) ),
inference(ennf_transformation,[],[f392]) ).
fof(f1059,plain,
! [X0] :
( ( ic(X0)
| ~ icext(uri_rdfs_Class,X0) )
& ( icext(uri_rdfs_Class,X0)
| ~ ic(X0) ) ),
inference(nnf_transformation,[],[f54]) ).
fof(f1082,plain,
! [X0] :
( ( icext(uri_rdf_Property,X0)
| ~ ip(X0) )
& ( ip(X0)
| ~ icext(uri_rdf_Property,X0) ) ),
inference(nnf_transformation,[],[f153]) ).
fof(f1084,plain,
! [X0] :
( ( icext(uri_owl_Thing,X0)
| ~ ir(X0) )
& ( ir(X0)
| ~ icext(uri_owl_Thing,X0) ) ),
inference(nnf_transformation,[],[f163]) ).
fof(f1112,plain,
! [X0] :
( ( iext(uri_owl_unionOf,X0,uri_rdf_nil)
| ~ ic(X0)
| ? [X1] : icext(X0,X1) )
& ( ( ic(X0)
& ! [X1] : ~ icext(X0,X1) )
| ~ iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ),
inference(nnf_transformation,[],[f287]) ).
fof(f1113,plain,
! [X0] :
( ( iext(uri_owl_unionOf,X0,uri_rdf_nil)
| ~ ic(X0)
| ? [X1] : icext(X0,X1) )
& ( ( ic(X0)
& ! [X1] : ~ icext(X0,X1) )
| ~ iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ),
inference(flattening,[],[f1112]) ).
fof(f1114,plain,
! [X0] :
( ( iext(uri_owl_unionOf,X0,uri_rdf_nil)
| ~ ic(X0)
| ? [X1] : icext(X0,X1) )
& ( ( ic(X0)
& ! [X2] : ~ icext(X0,X2) )
| ~ iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ),
inference(rectify,[],[f1113]) ).
fof(f1115,plain,
! [X0] :
( ( iext(uri_owl_unionOf,X0,uri_rdf_nil)
| ~ ic(X0)
| icext(X0,sK57(X0)) )
& ( ( ic(X0)
& ! [X2] : ~ icext(X0,X2) )
| ~ iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57]),skolemize(X1,sK57(X0))],[f1114]) ).
fof(f1136,plain,
! [X0,X1,X2] :
( ( ( iext(uri_owl_oneOf,X0,X1)
| ~ ic(X0)
| ? [X3] :
( ( X2 != X3
| ~ icext(X0,X3) )
& ( X3 = X2
| icext(X0,X3) ) ) )
& ( ( ic(X0)
& ! [X3] :
( ( icext(X0,X3)
| X2 != X3 )
& ( X3 = X2
| ~ icext(X0,X3) ) ) )
| ~ iext(uri_owl_oneOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(nnf_transformation,[],[f695]) ).
fof(f1137,plain,
! [X0,X1,X2] :
( ( ( iext(uri_owl_oneOf,X0,X1)
| ~ ic(X0)
| ? [X3] :
( ( X2 != X3
| ~ icext(X0,X3) )
& ( X3 = X2
| icext(X0,X3) ) ) )
& ( ( ic(X0)
& ! [X3] :
( ( icext(X0,X3)
| X2 != X3 )
& ( X3 = X2
| ~ icext(X0,X3) ) ) )
| ~ iext(uri_owl_oneOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(flattening,[],[f1136]) ).
fof(f1138,plain,
! [X0,X1,X2] :
( ( ( iext(uri_owl_oneOf,X0,X1)
| ~ ic(X0)
| ? [X3] :
( ( X2 != X3
| ~ icext(X0,X3) )
& ( X3 = X2
| icext(X0,X3) ) ) )
& ( ( ic(X0)
& ! [X4] :
( ( icext(X0,X4)
| X2 != X4 )
& ( X2 = X4
| ~ icext(X0,X4) ) ) )
| ~ iext(uri_owl_oneOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(rectify,[],[f1137]) ).
fof(f1139,plain,
! [X0,X1,X2] :
( ( ( iext(uri_owl_oneOf,X0,X1)
| ~ ic(X0)
| ( ( sK62(X0,X2) != X2
| ~ icext(X0,sK62(X0,X2)) )
& ( sK62(X0,X2) = X2
| icext(X0,sK62(X0,X2)) ) ) )
& ( ( ic(X0)
& ! [X4] :
( ( icext(X0,X4)
| X2 != X4 )
& ( X2 = X4
| ~ icext(X0,X4) ) ) )
| ~ iext(uri_owl_oneOf,X0,X1) ) )
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62]),skolemize(X3,sK62(X0,X2))],[f1138]) ).
fof(f1347,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(f1348,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,[],[f1347]) ).
fof(f1349,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,[],[f1348]) ).
fof(f1350,plain,
! [X0,X1] :
( ( iext(uri_owl_equivalentClass,X0,X1)
| ~ ic(X0)
| ~ ic(X1)
| ( ( ~ icext(X1,sK175(X0,X1))
| ~ icext(X0,sK175(X0,X1)) )
& ( icext(X1,sK175(X0,X1))
| icext(X0,sK175(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,[sK175]),skolemize(X2,sK175(X0,X1))],[f1349]) ).
fof(f1359,plain,
! [X0,X1] :
( ( iext(uri_owl_sameAs,X0,X1)
| X0 != X1 )
& ( X0 = X1
| ~ iext(uri_owl_sameAs,X0,X1) ) ),
inference(nnf_transformation,[],[f354]) ).
fof(f1408,plain,
! [X0] :
( ( icext(uri_owl_AsymmetricProperty,X0)
| ~ ip(X0)
| ? [X1,X2] :
( iext(X0,X2,X1)
& iext(X0,X1,X2) ) )
& ( ( ip(X0)
& ! [X1,X2] :
( ~ iext(X0,X2,X1)
| ~ iext(X0,X1,X2) ) )
| ~ icext(uri_owl_AsymmetricProperty,X0) ) ),
inference(nnf_transformation,[],[f844]) ).
fof(f1409,plain,
! [X0] :
( ( icext(uri_owl_AsymmetricProperty,X0)
| ~ ip(X0)
| ? [X1,X2] :
( iext(X0,X2,X1)
& iext(X0,X1,X2) ) )
& ( ( ip(X0)
& ! [X1,X2] :
( ~ iext(X0,X2,X1)
| ~ iext(X0,X1,X2) ) )
| ~ icext(uri_owl_AsymmetricProperty,X0) ) ),
inference(flattening,[],[f1408]) ).
fof(f1410,plain,
! [X0] :
( ( icext(uri_owl_AsymmetricProperty,X0)
| ~ ip(X0)
| ? [X1,X2] :
( iext(X0,X2,X1)
& iext(X0,X1,X2) ) )
& ( ( ip(X0)
& ! [X3,X4] :
( ~ iext(X0,X4,X3)
| ~ iext(X0,X3,X4) ) )
| ~ icext(uri_owl_AsymmetricProperty,X0) ) ),
inference(rectify,[],[f1409]) ).
fof(f1411,plain,
! [X0] :
( ( icext(uri_owl_AsymmetricProperty,X0)
| ~ ip(X0)
| ( iext(X0,sK221(X0),sK220(X0))
& iext(X0,sK220(X0),sK221(X0)) ) )
& ( ( ip(X0)
& ! [X3,X4] :
( ~ iext(X0,X4,X3)
| ~ iext(X0,X3,X4) ) )
| ~ icext(uri_owl_AsymmetricProperty,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK220,sK221]),skolemize(X1,sK220(X0)),skolemize(X2,sK221(X0))],[f1410]) ).
fof(f1457,plain,
( iext(uri_owl_equivalentClass,uri_owl_Thing,sK251)
& iext(uri_owl_oneOf,sK251,sK252)
& iext(uri_rdf_first,sK252,uri_ex_w)
& iext(uri_rdf_rest,sK252,uri_rdf_nil) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK251,sK252]),skolemize(X0,sK251),skolemize(X1,sK252)],[f559]) ).
fof(f1459,plain,
! [X0] : ir(X0),
inference(cnf_transformation,[],[f2]) ).
fof(f1513,plain,
! [X0] :
( ~ ic(X0)
| icext(uri_rdfs_Class,X0) ),
inference(cnf_transformation,[],[f1059]) ).
fof(f1514,plain,
! [X0] :
( ~ icext(uri_rdfs_Class,X0)
| ic(X0) ),
inference(cnf_transformation,[],[f1059]) ).
fof(f1604,plain,
ic(uri_rdfs_Class),
inference(cnf_transformation,[],[f122]) ).
fof(f1631,plain,
! [X0] : ~ icext(uri_owl_Nothing,X0),
inference(cnf_transformation,[],[f145]) ).
fof(f1643,plain,
! [X0] :
( ~ ip(X0)
| icext(uri_rdf_Property,X0) ),
inference(cnf_transformation,[],[f1082]) ).
fof(f1644,plain,
ic(uri_rdf_Property),
inference(cnf_transformation,[],[f154]) ).
fof(f1655,plain,
! [X0] :
( icext(uri_owl_Thing,X0)
| ~ ir(X0) ),
inference(cnf_transformation,[],[f1084]) ).
fof(f1661,plain,
ip(uri_owl_allValuesFrom),
inference(cnf_transformation,[],[f168]) ).
fof(f1680,plain,
! [X0,X1] : ~ iext(uri_owl_bottomObjectProperty,X0,X1),
inference(cnf_transformation,[],[f182]) ).
fof(f1681,plain,
ip(uri_owl_bottomObjectProperty),
inference(cnf_transformation,[],[f183]) ).
fof(f1788,plain,
ip(uri_owl_sameAs),
inference(cnf_transformation,[],[f255]) ).
fof(f1872,plain,
! [X2,X0] :
( ~ iext(uri_owl_unionOf,X0,uri_rdf_nil)
| ~ icext(X0,X2) ),
inference(cnf_transformation,[],[f1115]) ).
fof(f1874,plain,
! [X0] :
( ~ ic(X0)
| iext(uri_owl_unionOf,X0,uri_rdf_nil)
| icext(X0,sK57(X0)) ),
inference(cnf_transformation,[],[f1115]) ).
fof(f1914,plain,
! [X2,X0,X1,X4] :
( ~ iext(uri_owl_oneOf,X0,X1)
| ~ icext(X0,X4)
| X2 = X4
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil) ),
inference(cnf_transformation,[],[f1139]) ).
fof(f2377,plain,
! [X3,X0,X1] :
( ~ iext(uri_owl_equivalentClass,X0,X1)
| ~ icext(X0,X3)
| icext(X1,X3) ),
inference(cnf_transformation,[],[f1350]) ).
fof(f2378,plain,
! [X3,X0,X1] :
( ~ iext(uri_owl_equivalentClass,X0,X1)
| ~ icext(X1,X3)
| icext(X0,X3) ),
inference(cnf_transformation,[],[f1350]) ).
fof(f2381,plain,
! [X0,X1] :
( iext(uri_owl_equivalentClass,X0,X1)
| ~ ic(X0)
| ~ ic(X1)
| icext(X1,sK175(X0,X1))
| icext(X0,sK175(X0,X1)) ),
inference(cnf_transformation,[],[f1350]) ).
fof(f2382,plain,
! [X0,X1] :
( iext(uri_owl_equivalentClass,X0,X1)
| ~ ic(X0)
| ~ ic(X1)
| ~ icext(X1,sK175(X0,X1))
| ~ icext(X0,sK175(X0,X1)) ),
inference(cnf_transformation,[],[f1350]) ).
fof(f2395,plain,
! [X0,X1] :
( iext(uri_owl_sameAs,X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f1359]) ).
fof(f2505,plain,
! [X3,X0,X4] :
( ~ iext(X0,X4,X3)
| ~ iext(X0,X3,X4)
| ~ icext(uri_owl_AsymmetricProperty,X0) ),
inference(cnf_transformation,[],[f1411]) ).
fof(f2507,plain,
! [X0] :
( ~ ip(X0)
| icext(uri_owl_AsymmetricProperty,X0)
| iext(X0,sK220(X0),sK221(X0)) ),
inference(cnf_transformation,[],[f1411]) ).
fof(f2747,plain,
iext(uri_rdf_rest,sK252,uri_rdf_nil),
inference(cnf_transformation,[],[f1457]) ).
fof(f2748,plain,
iext(uri_rdf_first,sK252,uri_ex_w),
inference(cnf_transformation,[],[f1457]) ).
fof(f2749,plain,
iext(uri_owl_oneOf,sK251,sK252),
inference(cnf_transformation,[],[f1457]) ).
fof(f2750,plain,
iext(uri_owl_equivalentClass,uri_owl_Thing,sK251),
inference(cnf_transformation,[],[f1457]) ).
fof(f2758,plain,
! [X1] : iext(uri_owl_sameAs,X1,X1),
inference(equality_resolution,[],[f2395]) ).
fof(f2891,plain,
icext(uri_rdfs_Class,uri_rdf_Property),
inference(unit_resulting_resolution,[],[f1513,f1644]) ).
fof(f4032,plain,
icext(uri_rdf_Property,uri_owl_allValuesFrom),
inference(unit_resulting_resolution,[],[f1643,f1661]) ).
fof(f4071,plain,
icext(uri_rdf_Property,uri_owl_sameAs),
inference(unit_resulting_resolution,[],[f1643,f1788]) ).
fof(f4280,plain,
! [X0] : icext(uri_owl_Thing,X0),
inference(forward_subsumption_resolution,[],[f1655,f1459]) ).
fof(f11063,plain,
~ iext(uri_owl_unionOf,uri_rdf_Property,uri_rdf_nil),
inference(unit_resulting_resolution,[],[f1872,f4032]) ).
fof(f11162,plain,
~ iext(uri_owl_unionOf,uri_rdfs_Class,uri_rdf_nil),
inference(unit_resulting_resolution,[],[f1872,f2891]) ).
fof(f28580,plain,
( iext(uri_owl_unionOf,uri_rdf_Property,uri_rdf_nil)
| icext(uri_rdf_Property,sK57(uri_rdf_Property)) ),
inference(resolution,[],[f1874,f1644]) ).
fof(f28591,plain,
( iext(uri_owl_unionOf,uri_rdfs_Class,uri_rdf_nil)
| icext(uri_rdfs_Class,sK57(uri_rdfs_Class)) ),
inference(resolution,[],[f1874,f1604]) ).
fof(f28662,plain,
icext(uri_rdfs_Class,sK57(uri_rdfs_Class)),
inference(forward_subsumption_resolution,[],[f28591,f11162]) ).
fof(f28666,plain,
icext(uri_rdf_Property,sK57(uri_rdf_Property)),
inference(forward_subsumption_resolution,[],[f28580,f11063]) ).
fof(f29802,plain,
ic(sK57(uri_rdfs_Class)),
inference(unit_resulting_resolution,[],[f1514,f28662]) ).
fof(f36453,plain,
! [X0] : icext(sK251,X0),
inference(unit_resulting_resolution,[],[f2377,f4280,f2750]) ).
fof(f76389,plain,
~ icext(uri_owl_AsymmetricProperty,uri_owl_sameAs),
inference(unit_resulting_resolution,[],[f2505,f2758,f2758]) ).
fof(f77396,plain,
~ iext(uri_owl_equivalentClass,uri_owl_AsymmetricProperty,uri_rdf_Property),
inference(unit_resulting_resolution,[],[f2378,f4071,f76389]) ).
fof(f77835,plain,
icext(uri_owl_AsymmetricProperty,uri_owl_bottomObjectProperty),
inference(unit_resulting_resolution,[],[f2507,f1681,f1680]) ).
fof(f78071,plain,
~ iext(uri_owl_equivalentClass,uri_owl_Nothing,uri_owl_AsymmetricProperty),
inference(unit_resulting_resolution,[],[f2378,f1631,f77835]) ).
fof(f552731,plain,
! [X0] : uri_ex_w = X0,
inference(unit_resulting_resolution,[],[f1914,f36453,f2749,f2748,f2747]) ).
fof(f552775,plain,
icext(uri_rdf_Property,uri_ex_w),
inference(superposition,[],[f28666,f552731]) ).
fof(f552782,plain,
ic(uri_ex_w),
inference(superposition,[],[f29802,f552731]) ).
fof(f557713,plain,
! [X0] : ic(X0),
inference(superposition,[],[f552782,f552731]) ).
fof(f612866,plain,
! [X0,X1] :
( iext(uri_owl_equivalentClass,X0,X1)
| ~ ic(X0)
| icext(X1,sK175(X0,X1))
| icext(X0,sK175(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f2381,f557713]) ).
fof(f612867,plain,
! [X0,X1] :
( iext(uri_owl_equivalentClass,X0,X1)
| icext(X1,sK175(X0,X1))
| icext(X0,sK175(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f612866,f557713]) ).
fof(f612868,plain,
! [X0,X1] :
( icext(X1,uri_ex_w)
| iext(uri_owl_equivalentClass,X0,X1)
| icext(X0,sK175(X0,X1)) ),
inference(forward_demodulation,[],[f612867,f552731]) ).
fof(f612869,plain,
! [X0,X1] :
( icext(X1,uri_ex_w)
| icext(X0,uri_ex_w)
| iext(uri_owl_equivalentClass,X0,X1) ),
inference(forward_demodulation,[],[f612868,f552731]) ).
fof(f612882,plain,
icext(uri_owl_AsymmetricProperty,uri_ex_w),
inference(unit_resulting_resolution,[],[f612869,f78071,f1631]) ).
fof(f613180,plain,
! [X0,X1] :
( iext(uri_owl_equivalentClass,X0,X1)
| ~ ic(X0)
| ~ icext(X1,sK175(X0,X1))
| ~ icext(X0,sK175(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f2382,f557713]) ).
fof(f613181,plain,
! [X0,X1] :
( iext(uri_owl_equivalentClass,X0,X1)
| ~ icext(X1,sK175(X0,X1))
| ~ icext(X0,sK175(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f613180,f557713]) ).
fof(f613182,plain,
! [X0,X1] :
( ~ icext(X1,uri_ex_w)
| iext(uri_owl_equivalentClass,X0,X1)
| ~ icext(X0,sK175(X0,X1)) ),
inference(forward_demodulation,[],[f613181,f552731]) ).
fof(f613183,plain,
! [X0,X1] :
( ~ icext(X1,uri_ex_w)
| ~ icext(X0,uri_ex_w)
| iext(uri_owl_equivalentClass,X0,X1) ),
inference(forward_demodulation,[],[f613182,f552731]) ).
fof(f901211,plain,
$false,
inference(unit_resulting_resolution,[],[f613183,f552775,f77396,f612882]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB031+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.37 % Computer : n008.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:09:10 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.79/2.85 % (2070645)Will run a generic schedule for satisfiability detection.
% 16.79/2.85 % (2070651)% WARNING: option uhcvi not known.
% 16.79/2.85 % (2070652)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=463934088:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.79/2.85 % (2070650)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1550176482_2999 on theBenchmark for (2999ds/0Mi)
% 16.79/2.85 % (2070654)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3746168765:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.79/2.85 % (2070651)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3913920707:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.79/2.85 % (2070653)dis+10_1_sil=32000:sp=arity:random_seed=1384423650:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.79/2.85 % (2070655)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2454724225:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.79/2.85 % (2070656)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3562223498:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.79/2.85 % (2070653)Instruction limit reached!
% 16.79/2.85 % (2070653)------------------------------
% 16.79/2.85 % (2070653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.85 % (2070653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.85 % (2070653)CaDiCaL version: 2.1.3
% 16.79/2.85 % (2070653)Termination reason: Instruction limit
% 16.79/2.85 % (2070653)Termination phase: Saturation
% 16.79/2.85 % (2070653)Time elapsed: 0.055 s
% 16.79/2.85 % (2070653)Peak memory usage: 14 MB
% 16.79/2.85 % (2070653)Instructions burned: 103 (million)
% 16.79/2.85 % (2070654)Instruction limit reached!
% 16.79/2.85 % (2070654)------------------------------
% 16.79/2.85 % (2070654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.85 % (2070654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.85 % (2070654)CaDiCaL version: 2.1.3
% 16.79/2.85 % (2070654)Termination reason: Instruction limit
% 16.79/2.85 % (2070654)Termination phase: Saturation
% 16.79/2.85 % (2070654)Time elapsed: 0.056 s
% 16.79/2.85 % (2070654)Peak memory usage: 13 MB
% 16.79/2.85 % (2070654)Instructions burned: 117 (million)
% 16.79/2.85 % (2070655)Instruction limit reached!
% 16.79/2.85 % (2070655)------------------------------
% 16.79/2.85 % (2070655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.85 % (2070655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.85 % (2070655)CaDiCaL version: 2.1.3
% 16.79/2.85 % (2070655)Termination reason: Instruction limit
% 16.79/2.85 % (2070655)Termination phase: Saturation
% 16.79/2.85 % (2070655)Time elapsed: 0.068 s
% 16.79/2.85 % (2070655)Peak memory usage: 14 MB
% 16.79/2.85 % (2070655)Instructions burned: 132 (million)
% 16.79/2.85 % (2070664)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3960854305:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.79/2.85 % (2070665)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2503962474:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 16.79/2.85 % (2070656)Instruction limit reached!
% 16.79/2.85 % (2070656)------------------------------
% 16.79/2.85 % (2070656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.85 % (2070656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.85 % (2070656)CaDiCaL version: 2.1.3
% 16.79/2.85 % (2070656)Termination reason: Instruction limit
% 16.79/2.85 % (2070656)Termination phase: Saturation
% 16.79/2.85 % (2070656)Time elapsed: 0.083 s
% 16.79/2.85 % (2070656)Peak memory usage: 15 MB
% 16.79/2.85 % (2070656)Instructions burned: 159 (million)
% 16.79/2.85 % (2070666)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3563762927:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.79/2.85 % (2070669)ott-21_1_sil=16000:fs=off:random_seed=618748246:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.79/2.85 % TRYING [1]
% 16.79/2.85 % TRYING [2]
% 16.79/2.85 % (2070665)Instruction limit reached!
% 16.79/2.85 % (2070665)------------------------------
% 16.79/2.85 % (2070665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.85 % (2070665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.44/6.45 % (2070665)CaDiCaL version: 2.1.3
% 42.44/6.45 % (2070665)Termination reason: Instruction limit
% 42.44/6.45 % (2070665)Termination phase: Saturation
% 42.44/6.45 % (2070665)Time elapsed: 0.070 s
% 42.44/6.45 % (2070665)Peak memory usage: 14 MB
% 42.44/6.45 % (2070665)Instructions burned: 133 (million)
% 42.44/6.45 % TRYING [1]
% 42.44/6.45 % TRYING [2]
% 42.44/6.45 % (2070672)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2200598125:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 42.44/6.45 % TRYING [3]
% 42.44/6.45 % (2070669)Instruction limit reached!
% 42.44/6.45 % (2070669)------------------------------
% 42.44/6.45 % (2070669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.44/6.45 % (2070669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.44/6.45 % (2070669)CaDiCaL version: 2.1.3
% 42.44/6.45 % (2070669)Termination reason: Instruction limit
% 42.44/6.45 % (2070669)Termination phase: Saturation
% 42.44/6.45 % (2070669)Time elapsed: 0.086 s
% 42.44/6.45 % (2070669)Peak memory usage: 15 MB
% 42.44/6.45 % (2070669)Instructions burned: 180 (million)
% 42.44/6.45 % TRYING [3]
% 42.44/6.45 % (2070674)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=382675553:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.44/6.45 % TRYING [1]
% 42.44/6.45 % TRYING [2]
% 42.44/6.45 % (2070664)Instruction limit reached!
% 42.44/6.45 % (2070664)------------------------------
% 42.44/6.45 % (2070664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.44/6.45 % (2070664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.44/6.45 % (2070664)CaDiCaL version: 2.1.3
% 42.44/6.45 % (2070664)Termination reason: Instruction limit
% 42.44/6.45 % (2070664)Termination phase: Finite model building SAT solving
% 42.44/6.45 % (2070664)Time elapsed: 0.301 s
% 42.44/6.45 % (2070664)Peak memory usage: 42 MB
% 42.44/6.45 % (2070664)Instructions burned: 715 (million)
% 42.44/6.45 % TRYING [4]
% 42.44/6.45 % (2070676)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3712801628:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 42.44/6.45 % (2070672)Instruction limit reached!
% 42.44/6.45 % (2070672)------------------------------
% 42.44/6.45 % (2070672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.44/6.45 % (2070672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.44/6.45 % (2070672)CaDiCaL version: 2.1.3
% 42.44/6.45 % (2070672)Termination reason: Instruction limit
% 42.44/6.45 % (2070672)Termination phase: Saturation
% 42.44/6.45 % (2070672)Time elapsed: 0.283 s
% 42.44/6.45 % (2070672)Peak memory usage: 17 MB
% 42.44/6.45 % (2070672)Instructions burned: 478 (million)
% 42.44/6.45 % (2070666)Instruction limit reached!
% 42.44/6.45 % (2070666)------------------------------
% 42.44/6.45 % (2070666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.44/6.45 % (2070666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.44/6.45 % (2070666)CaDiCaL version: 2.1.3
% 42.44/6.45 % (2070666)Termination reason: Instruction limit
% 42.44/6.45 % (2070666)Termination phase: Saturation
% 42.44/6.45 % (2070666)Time elapsed: 0.369 s
% 42.44/6.45 % (2070666)Peak memory usage: 24 MB
% 42.44/6.45 % (2070666)Instructions burned: 685 (million)
% 42.44/6.45 % (2070678)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1789832434:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 42.44/6.45 % (2070679)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=60563901:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 42.44/6.45 % TRYING [3]
% 42.44/6.45 % (2070674)Instruction limit reached!
% 42.44/6.45 % (2070674)------------------------------
% 42.44/6.45 % (2070674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.44/6.45 % (2070674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.44/6.45 % (2070674)CaDiCaL version: 2.1.3
% 42.44/6.45 % (2070674)Termination reason: Instruction limit
% 42.44/6.45 % (2070674)Termination phase: Finite model building constraint generation
% 42.44/6.45 % (2070674)Time elapsed: 0.372 s
% 42.44/6.45 % (2070674)Peak memory usage: 30 MB
% 42.44/6.45 % (2070674)Instructions burned: 866 (million)
% 42.44/6.45 % (2070682)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3094797067:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 42.44/6.45 % (2070679)Instruction limit reached!
% 42.44/6.45 % (2070679)------------------------------
% 42.44/6.45 % (2070679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.71/13.90 % (2070679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.71/13.90 % (2070679)CaDiCaL version: 2.1.3
% 95.71/13.90 % (2070679)Termination reason: Instruction limit
% 95.71/13.90 % (2070679)Termination phase: Saturation
% 95.71/13.90 % (2070679)Time elapsed: 0.385 s
% 95.71/13.90 % (2070679)Peak memory usage: 18 MB
% 95.71/13.90 % (2070679)Instructions burned: 693 (million)
% 95.71/13.90 % (2070684)fmb+10_1_sil=64000:random_seed=3198473648:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 95.71/13.90 % (2070678)Instruction limit reached!
% 95.71/13.90 % (2070678)------------------------------
% 95.71/13.90 % (2070678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.71/13.90 % (2070678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.71/13.90 % (2070678)CaDiCaL version: 2.1.3
% 95.71/13.90 % (2070678)Termination reason: Instruction limit
% 95.71/13.90 % (2070678)Termination phase: Finite model building constraint generation
% 95.71/13.90 % (2070678)Time elapsed: 0.440 s
% 95.71/13.90 % (2070678)Peak memory usage: 96 MB
% 95.71/13.90 % (2070678)Instructions burned: 890 (million)
% 95.71/13.90 % (2070686)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1545929145:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 95.71/13.90 % TRYING [1]
% 95.71/13.90 % TRYING [2]
% 95.71/13.90 % (2070676)Instruction limit reached!
% 95.71/13.90 % (2070676)------------------------------
% 95.71/13.90 % (2070676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.71/13.90 % (2070676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.71/13.90 % (2070676)CaDiCaL version: 2.1.3
% 95.71/13.90 % (2070676)Termination reason: Instruction limit
% 95.71/13.90 % (2070676)Termination phase: Saturation
% 95.71/13.90 % (2070676)Time elapsed: 0.614 s
% 95.71/13.90 % (2070676)Peak memory usage: 32 MB
% 95.71/13.90 % (2070676)Instructions burned: 1180 (million)
% 95.71/13.90 % TRYING [20]
% 95.71/13.90 % (2070682)Instruction limit reached!
% 95.71/13.90 % (2070682)------------------------------
% 95.71/13.90 % (2070682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.71/13.90 % (2070682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.71/13.90 % (2070682)CaDiCaL version: 2.1.3
% 95.71/13.90 % (2070682)Termination reason: Instruction limit
% 95.71/13.90 % (2070682)Termination phase: Saturation
% 95.71/13.90 % (2070682)Time elapsed: 0.427 s
% 95.71/13.90 % (2070682)Peak memory usage: 29 MB
% 95.71/13.90 % (2070682)Instructions burned: 879 (million)
% 95.71/13.90 % (2070688)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=794194693:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 95.71/13.90 % (2070689)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2329660637:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 95.71/13.90 % TRYING [3]
% 95.71/13.90 % TRYING [5]
% 95.71/13.90 % TRYING [8]
% 95.71/13.90 % (2070688)Instruction limit reached!
% 95.71/13.90 % (2070688)------------------------------
% 95.71/13.90 % (2070688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.71/13.90 % (2070688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.71/13.90 % (2070688)CaDiCaL version: 2.1.3
% 95.71/13.90 % (2070688)Termination reason: Instruction limit
% 95.71/13.90 % (2070688)Termination phase: Finite model building constraint generation
% 95.71/13.90 % (2070688)Time elapsed: 0.327 s
% 95.71/13.90 % (2070688)Peak memory usage: 52 MB
% 95.71/13.90 % (2070688)Instructions burned: 921 (million)
% 95.71/13.90 % (2070692)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3692524524:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 95.71/13.90 % TRYING [4]
% 95.71/13.90 % (2070692)Instruction limit reached!
% 95.71/13.90 % (2070692)------------------------------
% 95.71/13.90 % (2070692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.71/13.90 % (2070692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.71/13.90 % (2070692)CaDiCaL version: 2.1.3
% 95.71/13.90 % (2070692)Termination reason: Instruction limit
% 95.71/13.90 % (2070692)Termination phase: Saturation
% 95.71/13.90 % (2070692)Time elapsed: 0.858 s
% 95.71/13.90 % (2070692)Peak memory usage: 39 MB
% 95.71/13.90 % (2070692)Instructions burned: 1473 (million)
% 95.71/13.90 % (2070694)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2527431660:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 95.71/13.90 % (2070694)Cannot represent all propositional literals internally
% 95.71/13.90 % (2070694)Refutation not found, incomplete strategy
% 80.03/23.04 % (2070694)------------------------------
% 80.03/23.04 % (2070694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070694)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070694)Termination reason: Refutation not found, incomplete strategy
% 80.03/23.04 % (2070694)Time elapsed: 0.118 s
% 80.03/23.04 % (2070694)Peak memory usage: 16 MB
% 80.03/23.04 % (2070694)Instructions burned: 251 (million)
% 80.03/23.04 % (2070694)------------------------------
% 80.03/23.04 % (2070694)------------------------------
% 80.03/23.04 % (2070696)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1920090774:fmbsr=2.30978:i=2174_2975 on theBenchmark for (2975ds/2174Mi)
% 80.03/23.04 % (2070696)Cannot represent all propositional literals internally
% 80.03/23.04 % (2070696)Refutation not found, incomplete strategy
% 80.03/23.04 % (2070696)------------------------------
% 80.03/23.04 % (2070696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070696)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070696)Termination reason: Refutation not found, incomplete strategy
% 80.03/23.04 % (2070696)Time elapsed: 0.478 s
% 80.03/23.04 % (2070696)Peak memory usage: 25 MB
% 80.03/23.04 % (2070696)Instructions burned: 990 (million)
% 80.03/23.04 % (2070696)------------------------------
% 80.03/23.04 % (2070696)------------------------------
% 80.03/23.04 % (2070698)ott-2_1_sil=16000:newcnf=on:random_seed=586548307:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 80.03/23.04 % TRYING [5]
% 80.03/23.04 % (2070698)Instruction limit reached!
% 80.03/23.04 % (2070698)------------------------------
% 80.03/23.04 % (2070698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070698)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070698)Termination reason: Instruction limit
% 80.03/23.04 % (2070698)Termination phase: Saturation
% 80.03/23.04 % (2070698)Time elapsed: 0.450 s
% 80.03/23.04 % (2070698)Peak memory usage: 26 MB
% 80.03/23.04 % (2070698)Instructions burned: 869 (million)
% 80.03/23.04 % (2070700)ott+10_1_sil=32000:tgt=ground:random_seed=2920706367:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 80.03/23.04 % (2070689)Instruction limit reached!
% 80.03/23.04 % (2070689)------------------------------
% 80.03/23.04 % (2070689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070689)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070689)Termination reason: Instruction limit
% 80.03/23.04 % (2070689)Termination phase: Saturation
% 80.03/23.04 % (2070689)Time elapsed: 2.418 s
% 80.03/23.04 % (2070689)Peak memory usage: 30 MB
% 80.03/23.04 % (2070689)Instructions burned: 5132 (million)
% 80.03/23.04 % (2070702)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3182611494:i=54282_2964 on theBenchmark for (2964ds/54282Mi)
% 80.03/23.04 % TRYING [1]
% 80.03/23.04 % TRYING [2]
% 80.03/23.04 % TRYING [3]
% 80.03/23.04 % TRYING [6]
% 80.03/23.04 % TRYING [4]
% 80.03/23.04 % (2070686)Instruction limit reached!
% 80.03/23.04 % (2070686)------------------------------
% 80.03/23.04 % (2070686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070686)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070686)Termination reason: Instruction limit
% 80.03/23.04 % (2070686)Termination phase: Finite model building constraint generation
% 80.03/23.04 % (2070686)Time elapsed: 3.201 s
% 80.03/23.04 % (2070686)Peak memory usage: 527 MB
% 80.03/23.04 % (2070686)Instructions burned: 9518 (million)
% 80.03/23.04 % (2070704)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2261349552:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 80.03/23.04 % TRYING [5]
% 80.03/23.04 % (2070704)Instruction limit reached!
% 80.03/23.04 % (2070704)------------------------------
% 80.03/23.04 % (2070704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070704)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070704)Termination reason: Instruction limit
% 80.03/23.04 % (2070704)Termination phase: Saturation
% 80.03/23.04 % (2070704)Time elapsed: 1.763 s
% 80.03/23.04 % (2070704)Peak memory usage: 37 MB
% 80.03/23.04 % (2070704)Instructions burned: 3512 (million)
% 80.03/23.04 % (2070706)dis+21_1_sil=32000:sas=cadical:random_seed=4266210940:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 80.03/23.04 % (2070700)Instruction limit reached!
% 80.03/23.04 % (2070700)------------------------------
% 80.03/23.04 % (2070700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070700)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070700)Termination reason: Instruction limit
% 80.03/23.04 % (2070700)Termination phase: Saturation
% 80.03/23.04 % (2070700)Time elapsed: 2.756 s
% 80.03/23.04 % (2070700)Peak memory usage: 64 MB
% 80.03/23.04 % (2070700)Instructions burned: 5115 (million)
% 80.03/23.04 % (2070708)ott+11_1_sil=16000:gs=on:random_seed=3136141620:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2937 on theBenchmark for (2937ds/2251Mi)
% 80.03/23.04 % TRYING [6]
% 80.03/23.04 % (2070708)Instruction limit reached!
% 80.03/23.04 % (2070708)------------------------------
% 80.03/23.04 % (2070708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070708)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070708)Termination reason: Instruction limit
% 80.03/23.04 % (2070708)Termination phase: Saturation
% 80.03/23.04 % (2070708)Time elapsed: 1.390 s
% 80.03/23.04 % (2070708)Peak memory usage: 78 MB
% 80.03/23.04 % (2070708)Instructions burned: 2251 (million)
% 80.03/23.04 % (2070712)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3282530544:fmbsr=1.6:i=67534_2923 on theBenchmark for (2923ds/67534Mi)
% 80.03/23.04 % (2070706)Instruction limit reached!
% 80.03/23.04 % (2070706)------------------------------
% 80.03/23.04 % (2070706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070706)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070706)Termination reason: Instruction limit
% 80.03/23.04 % (2070706)Termination phase: Saturation
% 80.03/23.04 % (2070706)Time elapsed: 1.947 s
% 80.03/23.04 % (2070706)Peak memory usage: 45 MB
% 80.03/23.04 % (2070706)Instructions burned: 3775 (million)
% 80.03/23.04 % (2070714)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1794738022:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2919 on theBenchmark for (2919ds/4591Mi)
% 80.03/23.04 % TRYING [7]
% 80.03/23.04 % TRYING [6]
% 80.03/23.04 % (2070684)Instruction limit reached!
% 80.03/23.04 % (2070684)------------------------------
% 80.03/23.04 % (2070684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070684)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070684)Termination reason: Instruction limit
% 80.03/23.04 % (2070684)Termination phase: Finite model building constraint generation
% 80.03/23.04 % (2070684)Time elapsed: 9.596 s
% 80.03/23.04 % (2070684)Peak memory usage: 238 MB
% 80.03/23.04 % (2070684)Instructions burned: 22062 (million)
% 80.03/23.04 % (2070716)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3036649475:i=29340_2894 on theBenchmark for (2894ds/29340Mi)
% 80.03/23.04 % (2070714)Instruction limit reached!
% 80.03/23.04 % (2070714)------------------------------
% 80.03/23.04 % (2070714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070714)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070714)Termination reason: Instruction limit
% 80.03/23.04 % (2070714)Termination phase: Saturation
% 80.03/23.04 % (2070714)Time elapsed: 2.683 s
% 80.03/23.04 % (2070714)Peak memory usage: 60 MB
% 80.03/23.04 % (2070714)Instructions burned: 4591 (million)
% 80.03/23.04 % (2070718)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2567048823:i=5211_2892 on theBenchmark for (2892ds/5211Mi)
% 80.03/23.04 % (2070718)Instruction limit reached!
% 80.03/23.04 % (2070718)------------------------------
% 80.03/23.04 % (2070718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070718)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070718)Termination reason: Instruction limit
% 80.03/23.04 % (2070718)Termination phase: Saturation
% 80.03/23.04 % (2070718)Time elapsed: 2.735 s
% 80.03/23.04 % (2070718)Peak memory usage: 70 MB
% 80.03/23.04 % (2070718)Instructions burned: 5214 (million)
% 80.03/23.04 % (2070720)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2055573923:i=5497:nm=2_2865 on theBenchmark for (2865ds/5497Mi)
% 80.03/23.04 % TRYING [17]
% 80.03/23.04 % (2070720)Instruction limit reached!
% 80.03/23.04 % (2070720)------------------------------
% 80.03/23.04 % (2070720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.04 % (2070720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.04 % (2070720)CaDiCaL version: 2.1.3
% 80.03/23.04 % (2070720)Termination reason: Instruction limit
% 80.03/23.04 % (2070720)Termination phase: Finite model building constraint generation
% 80.03/23.04 % (2070720)Time elapsed: 1.833 s
% 80.03/23.04 % (2070720)Peak memory usage: 292 MB
% 80.03/23.04 % (2070720)Instructions burned: 5499 (million)
% 80.03/23.04 % (2070722)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1215801206:fmbsr=2:i=46332_2846 on theBenchmark for (2846ds/46332Mi)
% 80.03/23.04 % TRYING [15]
% 80.03/23.04 % TRYING [7]
% 80.03/23.04 % TRYING [7]
% 80.03/23.04 % (2070716) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2070645-2070716"...
% 80.03/23.04 % (2070716)...printing done.
% 80.03/23.04 % (2070716)Refutation found. Thanks to Tanya!
% 80.03/23.04 % SZS status Unsatisfiable for theBenchmark
% 80.03/23.04 % SZS output start Proof for theBenchmark
% See solution above
% 80.03/23.05 % (2070716)------------------------------
% 80.03/23.05 % (2070716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.03/23.05 % (2070716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.03/23.05 % (2070716)CaDiCaL version: 2.1.3
% 80.03/23.05 % (2070716)Termination reason: Refutation
% 80.03/23.05 % (2070716)Time elapsed: 11.786 s
% 80.03/23.05 % (2070716)Peak memory usage: 275 MB
% 80.03/23.05 % (2070716)Instructions burned: 25471 (million)
% 80.03/23.05 % (2070645)Success in time 22.628 s
% 80.03/23.05 % Vampire exiting
%------------------------------------------------------------------------------