%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWB102+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:26 PM UTC 2026
% Result : Theorem 5.09s 1.70s
% Output : Refutation 6.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 14
% Syntax : Number of formulae : 213 ( 20 unt; 4 def)
% Number of atoms : 1123 ( 47 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 1572 ( 662 ~; 750 |; 137 &)
% ( 12 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 5 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 15 con; 0-3 aty)
% Number of variables : 422 ( 0 sgn 395 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f84,axiom,
! [X0] :
( idc(X0)
=> ! [X1] :
( icext(X0,X1)
=> lv(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_parts_idc_cond_inst) ).
fof(f90,axiom,
! [X0] :
( iodp(X0)
=> ! [X1,X2] :
( iext(X0,X1,X2)
=> ( ir(X1)
& lv(X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_parts_iodp_cond_inst) ).
fof(f159,axiom,
! [X0] :
( icext(uri_owl_Restriction,X0)
=> ic(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_class_restriction_ext) ).
fof(f237,axiom,
! [X0,X1] :
( iext(uri_owl_onDataRange,X0,X1)
=> ( icext(uri_owl_Restriction,X0)
& idc(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_prop_ondatarange_ext) ).
fof(f243,axiom,
! [X0,X1] :
( iext(uri_owl_onProperty,X0,X1)
=> ( icext(uri_owl_Restriction,X0)
& ip(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_prop_onproperty_ext) ).
fof(f307,axiom,
! [X0,X1,X2] :
( ( iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
& iext(uri_owl_onProperty,X0,X1)
& iext(uri_owl_onDataRange,X0,X2) )
=> ( iodp(X1)
& ! [X3] :
( icext(X0,X3)
<=> ( ? [X4] :
( lv(X4)
& iext(X1,X3,X4)
& icext(X2,X4) )
& ! [X5,X6] :
( ( lv(X5)
& iext(X1,X3,X5)
& icext(X2,X5)
& lv(X6)
& iext(X1,X3,X6)
& icext(X2,X6) )
=> X6 = X5 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_restrict_exactqcr_data_001) ).
fof(f311,axiom,
! [X0,X1,X2] :
( ( iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
& iext(uri_owl_onProperty,X0,X1)
& iext(uri_owl_onClass,X0,X2) )
=> ! [X3] :
( icext(X0,X3)
<=> ( ? [X4] :
( iext(X1,X3,X4)
& icext(X2,X4) )
& ! [X5,X6] :
( ( iext(X1,X3,X5)
& icext(X2,X5)
& iext(X1,X3,X6)
& icext(X2,X6) )
=> X6 = X5 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_restrict_exactqcr_object_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/theBenchmark.p',owl_eqdis_equivalentclass) ).
fof(f559,conjecture,
iext(uri_owl_equivalentClass,uri_ex_z1,uri_ex_z2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conclusion_rdfbased_sem_restrict_term_dataqcr) ).
fof(f560,negated_conjecture,
~ iext(uri_owl_equivalentClass,uri_ex_z1,uri_ex_z2),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
( iext(uri_rdf_type,uri_ex_p,uri_owl_DatatypeProperty)
& iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
& iext(uri_owl_onProperty,uri_ex_z2,uri_ex_p)
& iext(uri_owl_onDataRange,uri_ex_z2,uri_ex_d)
& iext(uri_rdf_type,uri_ex_d,uri_rdfs_Datatype)
& iext(uri_owl_qualifiedCardinality,uri_ex_z1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
& iext(uri_owl_onProperty,uri_ex_z1,uri_ex_p)
& iext(uri_owl_onClass,uri_ex_z1,uri_ex_d) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',premise_rdfbased_sem_restrict_term_dataqcr) ).
fof(f562,plain,
~ iext(uri_owl_equivalentClass,uri_ex_z1,uri_ex_z2),
inference(flattening,[],[f560]) ).
fof(f572,plain,
! [X0,X1] :
( ( icext(uri_owl_Restriction,X0)
& idc(X1) )
| ~ iext(uri_owl_onDataRange,X0,X1) ),
inference(ennf_transformation,[],[f237]) ).
fof(f586,plain,
! [X0,X1,X2] :
( ! [X3] :
( icext(X0,X3)
<=> ( ? [X4] :
( iext(X1,X3,X4)
& icext(X2,X4) )
& ! [X5,X6] :
( X6 = X5
| ~ iext(X1,X3,X5)
| ~ icext(X2,X5)
| ~ iext(X1,X3,X6)
| ~ icext(X2,X6) ) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(ennf_transformation,[],[f311]) ).
fof(f587,plain,
! [X0,X1,X2] :
( ! [X3] :
( icext(X0,X3)
<=> ( ? [X4] :
( iext(X1,X3,X4)
& icext(X2,X4) )
& ! [X5,X6] :
( X6 = X5
| ~ iext(X1,X3,X5)
| ~ icext(X2,X5)
| ~ iext(X1,X3,X6)
| ~ icext(X2,X6) ) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(flattening,[],[f586]) ).
fof(f588,plain,
! [X0,X1,X2] :
( ( iodp(X1)
& ! [X3] :
( icext(X0,X3)
<=> ( ? [X4] :
( lv(X4)
& iext(X1,X3,X4)
& icext(X2,X4) )
& ! [X5,X6] :
( X6 = X5
| ~ lv(X5)
| ~ iext(X1,X3,X5)
| ~ icext(X2,X5)
| ~ lv(X6)
| ~ iext(X1,X3,X6)
| ~ icext(X2,X6) ) ) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(ennf_transformation,[],[f307]) ).
fof(f589,plain,
! [X0,X1,X2] :
( ( iodp(X1)
& ! [X3] :
( icext(X0,X3)
<=> ( ? [X4] :
( lv(X4)
& iext(X1,X3,X4)
& icext(X2,X4) )
& ! [X5,X6] :
( X6 = X5
| ~ lv(X5)
| ~ iext(X1,X3,X5)
| ~ icext(X2,X5)
| ~ lv(X6)
| ~ iext(X1,X3,X6)
| ~ icext(X2,X6) ) ) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(flattening,[],[f588]) ).
fof(f594,plain,
! [X0] :
( ! [X1] :
( lv(X1)
| ~ icext(X0,X1) )
| ~ idc(X0) ),
inference(ennf_transformation,[],[f84]) ).
fof(f603,plain,
! [X0] :
( ! [X1,X2] :
( ( ir(X1)
& lv(X2) )
| ~ iext(X0,X1,X2) )
| ~ iodp(X0) ),
inference(ennf_transformation,[],[f90]) ).
fof(f604,plain,
! [X0,X1] :
( ( icext(uri_owl_Restriction,X0)
& ip(X1) )
| ~ iext(uri_owl_onProperty,X0,X1) ),
inference(ennf_transformation,[],[f243]) ).
fof(f605,plain,
! [X0] :
( ic(X0)
| ~ icext(uri_owl_Restriction,X0) ),
inference(ennf_transformation,[],[f159]) ).
fof(f693,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(f694,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,[],[f693]) ).
fof(f695,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,[],[f694]) ).
fof(f696,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))],[f695]) ).
fof(f720,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( icext(X0,X3)
| ! [X4] :
( ~ iext(X1,X3,X4)
| ~ icext(X2,X4) )
| ? [X5,X6] :
( X5 != X6
& iext(X1,X3,X5)
& icext(X2,X5)
& iext(X1,X3,X6)
& icext(X2,X6) ) )
& ( ( ? [X4] :
( iext(X1,X3,X4)
& icext(X2,X4) )
& ! [X5,X6] :
( X6 = X5
| ~ iext(X1,X3,X5)
| ~ icext(X2,X5)
| ~ iext(X1,X3,X6)
| ~ icext(X2,X6) ) )
| ~ icext(X0,X3) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(nnf_transformation,[],[f587]) ).
fof(f721,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( icext(X0,X3)
| ! [X4] :
( ~ iext(X1,X3,X4)
| ~ icext(X2,X4) )
| ? [X5,X6] :
( X5 != X6
& iext(X1,X3,X5)
& icext(X2,X5)
& iext(X1,X3,X6)
& icext(X2,X6) ) )
& ( ( ? [X4] :
( iext(X1,X3,X4)
& icext(X2,X4) )
& ! [X5,X6] :
( X6 = X5
| ~ iext(X1,X3,X5)
| ~ icext(X2,X5)
| ~ iext(X1,X3,X6)
| ~ icext(X2,X6) ) )
| ~ icext(X0,X3) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(flattening,[],[f720]) ).
fof(f722,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( icext(X0,X3)
| ! [X4] :
( ~ iext(X1,X3,X4)
| ~ icext(X2,X4) )
| ? [X5,X6] :
( X5 != X6
& iext(X1,X3,X5)
& icext(X2,X5)
& iext(X1,X3,X6)
& icext(X2,X6) ) )
& ( ( ? [X7] :
( iext(X1,X3,X7)
& icext(X2,X7) )
& ! [X8,X9] :
( X8 = X9
| ~ iext(X1,X3,X8)
| ~ icext(X2,X8)
| ~ iext(X1,X3,X9)
| ~ icext(X2,X9) ) )
| ~ icext(X0,X3) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(rectify,[],[f721]) ).
fof(f723,plain,
! [X0,X1,X2] :
( ! [X3] :
( ( icext(X0,X3)
| ! [X4] :
( ~ iext(X1,X3,X4)
| ~ icext(X2,X4) )
| ( sK17(X1,X2,X3) != sK18(X1,X2,X3)
& iext(X1,X3,sK17(X1,X2,X3))
& icext(X2,sK17(X1,X2,X3))
& iext(X1,X3,sK18(X1,X2,X3))
& icext(X2,sK18(X1,X2,X3)) ) )
& ( ( iext(X1,X3,sK19(X1,X2,X3))
& icext(X2,sK19(X1,X2,X3))
& ! [X8,X9] :
( X8 = X9
| ~ iext(X1,X3,X8)
| ~ icext(X2,X8)
| ~ iext(X1,X3,X9)
| ~ icext(X2,X9) ) )
| ~ icext(X0,X3) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19]),skolemize(X5,sK17(X1,X2,X3)),skolemize(X6,sK18(X1,X2,X3)),skolemize(X7,sK19(X1,X2,X3))],[f722]) ).
fof(f724,plain,
! [X0,X1,X2] :
( ( iodp(X1)
& ! [X3] :
( ( icext(X0,X3)
| ! [X4] :
( ~ lv(X4)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4) )
| ? [X5,X6] :
( X5 != X6
& lv(X5)
& iext(X1,X3,X5)
& icext(X2,X5)
& lv(X6)
& iext(X1,X3,X6)
& icext(X2,X6) ) )
& ( ( ? [X4] :
( lv(X4)
& iext(X1,X3,X4)
& icext(X2,X4) )
& ! [X5,X6] :
( X6 = X5
| ~ lv(X5)
| ~ iext(X1,X3,X5)
| ~ icext(X2,X5)
| ~ lv(X6)
| ~ iext(X1,X3,X6)
| ~ icext(X2,X6) ) )
| ~ icext(X0,X3) ) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(nnf_transformation,[],[f589]) ).
fof(f725,plain,
! [X0,X1,X2] :
( ( iodp(X1)
& ! [X3] :
( ( icext(X0,X3)
| ! [X4] :
( ~ lv(X4)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4) )
| ? [X5,X6] :
( X5 != X6
& lv(X5)
& iext(X1,X3,X5)
& icext(X2,X5)
& lv(X6)
& iext(X1,X3,X6)
& icext(X2,X6) ) )
& ( ( ? [X4] :
( lv(X4)
& iext(X1,X3,X4)
& icext(X2,X4) )
& ! [X5,X6] :
( X6 = X5
| ~ lv(X5)
| ~ iext(X1,X3,X5)
| ~ icext(X2,X5)
| ~ lv(X6)
| ~ iext(X1,X3,X6)
| ~ icext(X2,X6) ) )
| ~ icext(X0,X3) ) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(flattening,[],[f724]) ).
fof(f726,plain,
! [X0,X1,X2] :
( ( iodp(X1)
& ! [X3] :
( ( icext(X0,X3)
| ! [X4] :
( ~ lv(X4)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4) )
| ? [X5,X6] :
( X5 != X6
& lv(X5)
& iext(X1,X3,X5)
& icext(X2,X5)
& lv(X6)
& iext(X1,X3,X6)
& icext(X2,X6) ) )
& ( ( ? [X7] :
( lv(X7)
& iext(X1,X3,X7)
& icext(X2,X7) )
& ! [X8,X9] :
( X8 = X9
| ~ lv(X8)
| ~ iext(X1,X3,X8)
| ~ icext(X2,X8)
| ~ lv(X9)
| ~ iext(X1,X3,X9)
| ~ icext(X2,X9) ) )
| ~ icext(X0,X3) ) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(rectify,[],[f725]) ).
fof(f727,plain,
! [X0,X1,X2] :
( ( iodp(X1)
& ! [X3] :
( ( icext(X0,X3)
| ! [X4] :
( ~ lv(X4)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4) )
| ( sK20(X1,X2,X3) != sK21(X1,X2,X3)
& lv(sK20(X1,X2,X3))
& iext(X1,X3,sK20(X1,X2,X3))
& icext(X2,sK20(X1,X2,X3))
& lv(sK21(X1,X2,X3))
& iext(X1,X3,sK21(X1,X2,X3))
& icext(X2,sK21(X1,X2,X3)) ) )
& ( ( lv(sK22(X1,X2,X3))
& iext(X1,X3,sK22(X1,X2,X3))
& icext(X2,sK22(X1,X2,X3))
& ! [X8,X9] :
( X8 = X9
| ~ lv(X8)
| ~ iext(X1,X3,X8)
| ~ icext(X2,X8)
| ~ lv(X9)
| ~ iext(X1,X3,X9)
| ~ icext(X2,X9) ) )
| ~ icext(X0,X3) ) ) )
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22]),skolemize(X5,sK20(X1,X2,X3)),skolemize(X6,sK21(X1,X2,X3)),skolemize(X7,sK22(X1,X2,X3))],[f726]) ).
fof(f841,plain,
~ iext(uri_owl_equivalentClass,uri_ex_z1,uri_ex_z2),
inference(cnf_transformation,[],[f562]) ).
fof(f842,plain,
iext(uri_owl_onClass,uri_ex_z1,uri_ex_d),
inference(cnf_transformation,[],[f561]) ).
fof(f843,plain,
iext(uri_owl_onProperty,uri_ex_z1,uri_ex_p),
inference(cnf_transformation,[],[f561]) ).
fof(f844,plain,
iext(uri_owl_qualifiedCardinality,uri_ex_z1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)),
inference(cnf_transformation,[],[f561]) ).
fof(f846,plain,
iext(uri_owl_onDataRange,uri_ex_z2,uri_ex_d),
inference(cnf_transformation,[],[f561]) ).
fof(f847,plain,
iext(uri_owl_onProperty,uri_ex_z2,uri_ex_p),
inference(cnf_transformation,[],[f561]) ).
fof(f848,plain,
iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)),
inference(cnf_transformation,[],[f561]) ).
fof(f854,plain,
! [X0,X1] :
( ~ ic(X1)
| ~ ic(X0)
| iext(uri_owl_equivalentClass,X0,X1)
| icext(X1,sK7(X0,X1))
| icext(X0,sK7(X0,X1)) ),
inference(cnf_transformation,[],[f696]) ).
fof(f855,plain,
! [X0,X1] :
( ~ ic(X1)
| ~ ic(X0)
| iext(uri_owl_equivalentClass,X0,X1)
| ~ icext(X1,sK7(X0,X1))
| ~ icext(X0,sK7(X0,X1)) ),
inference(cnf_transformation,[],[f696]) ).
fof(f878,plain,
! [X0,X1] :
( ~ iext(uri_owl_onDataRange,X0,X1)
| idc(X1) ),
inference(cnf_transformation,[],[f572]) ).
fof(f913,plain,
! [X2,X3,X0,X1,X8,X9] :
( ~ icext(X0,X3)
| ~ iext(X1,X3,X8)
| ~ icext(X2,X8)
| ~ iext(X1,X3,X9)
| ~ icext(X2,X9)
| X8 = X9
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(cnf_transformation,[],[f723]) ).
fof(f914,plain,
! [X2,X3,X0,X1] :
( ~ icext(X0,X3)
| icext(X2,sK19(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(cnf_transformation,[],[f723]) ).
fof(f915,plain,
! [X2,X3,X0,X1] :
( ~ icext(X0,X3)
| iext(X1,X3,sK19(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(cnf_transformation,[],[f723]) ).
fof(f916,plain,
! [X2,X3,X0,X1,X4] :
( ~ icext(X2,X4)
| ~ iext(X1,X3,X4)
| icext(X0,X3)
| icext(X2,sK18(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(cnf_transformation,[],[f723]) ).
fof(f917,plain,
! [X2,X3,X0,X1,X4] :
( ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4)
| iext(X1,X3,sK18(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| icext(X0,X3) ),
inference(cnf_transformation,[],[f723]) ).
fof(f918,plain,
! [X2,X3,X0,X1,X4] :
( ~ icext(X2,X4)
| ~ iext(X1,X3,X4)
| icext(X0,X3)
| icext(X2,sK17(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(cnf_transformation,[],[f723]) ).
fof(f919,plain,
! [X2,X3,X0,X1,X4] :
( ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4)
| iext(X1,X3,sK17(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| icext(X0,X3) ),
inference(cnf_transformation,[],[f723]) ).
fof(f920,plain,
! [X2,X3,X0,X1,X4] :
( sK17(X1,X2,X3) != sK18(X1,X2,X3)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4)
| icext(X0,X3)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onClass,X0,X2) ),
inference(cnf_transformation,[],[f723]) ).
fof(f921,plain,
! [X2,X3,X0,X1,X8,X9] :
( ~ lv(X8)
| X8 = X9
| ~ iext(X1,X3,X8)
| ~ icext(X2,X8)
| ~ lv(X9)
| ~ iext(X1,X3,X9)
| ~ icext(X2,X9)
| ~ icext(X0,X3)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(cnf_transformation,[],[f727]) ).
fof(f922,plain,
! [X2,X3,X0,X1] :
( ~ icext(X0,X3)
| icext(X2,sK22(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(cnf_transformation,[],[f727]) ).
fof(f923,plain,
! [X2,X3,X0,X1] :
( ~ icext(X0,X3)
| iext(X1,X3,sK22(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(cnf_transformation,[],[f727]) ).
fof(f925,plain,
! [X2,X3,X0,X1,X4] :
( ~ lv(X4)
| icext(X0,X3)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4)
| icext(X2,sK21(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(cnf_transformation,[],[f727]) ).
fof(f926,plain,
! [X2,X3,X0,X1,X4] :
( ~ lv(X4)
| icext(X0,X3)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4)
| iext(X1,X3,sK21(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(cnf_transformation,[],[f727]) ).
fof(f927,plain,
! [X2,X3,X0,X1,X4] :
( ~ lv(X4)
| icext(X0,X3)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4)
| lv(sK21(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(cnf_transformation,[],[f727]) ).
fof(f928,plain,
! [X2,X3,X0,X1,X4] :
( ~ lv(X4)
| icext(X0,X3)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4)
| icext(X2,sK20(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(cnf_transformation,[],[f727]) ).
fof(f929,plain,
! [X2,X3,X0,X1,X4] :
( ~ lv(X4)
| icext(X0,X3)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4)
| iext(X1,X3,sK20(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(cnf_transformation,[],[f727]) ).
fof(f930,plain,
! [X2,X3,X0,X1,X4] :
( ~ lv(X4)
| icext(X0,X3)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4)
| lv(sK20(X1,X2,X3))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(cnf_transformation,[],[f727]) ).
fof(f931,plain,
! [X2,X3,X0,X1,X4] :
( sK20(X1,X2,X3) != sK21(X1,X2,X3)
| ~ lv(X4)
| ~ iext(X1,X3,X4)
| ~ icext(X2,X4)
| icext(X0,X3)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_onDataRange,X0,X2) ),
inference(cnf_transformation,[],[f727]) ).
fof(f932,plain,
! [X2,X0,X1] :
( ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X1)
| iodp(X1) ),
inference(cnf_transformation,[],[f727]) ).
fof(f940,plain,
! [X0,X1] :
( ~ idc(X0)
| ~ icext(X0,X1)
| lv(X1) ),
inference(cnf_transformation,[],[f594]) ).
fof(f978,plain,
! [X2,X0,X1] :
( ~ iodp(X0)
| ~ iext(X0,X1,X2)
| lv(X2) ),
inference(cnf_transformation,[],[f603]) ).
fof(f981,plain,
! [X0,X1] :
( ~ iext(uri_owl_onProperty,X0,X1)
| icext(uri_owl_Restriction,X0) ),
inference(cnf_transformation,[],[f604]) ).
fof(f983,plain,
! [X0] :
( ~ icext(uri_owl_Restriction,X0)
| ic(X0) ),
inference(cnf_transformation,[],[f605]) ).
fof(f1322,plain,
icext(uri_owl_Restriction,uri_ex_z1),
inference(resolution,[],[f981,f843]) ).
fof(f1323,plain,
icext(uri_owl_Restriction,uri_ex_z2),
inference(resolution,[],[f981,f847]) ).
fof(f1367,plain,
! [X2,X0,X1] :
( ~ iext(X0,X1,X2)
| ~ icext(uri_ex_d,X2)
| iext(X0,X1,sK18(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z1,X0)
| icext(uri_ex_z1,X1) ),
inference(resolution,[],[f917,f842]) ).
fof(f1368,plain,
! [X2,X0,X1] :
( ~ icext(uri_ex_d,X2)
| ~ iext(X0,X1,X2)
| iext(X0,X1,sK18(X0,uri_ex_d,X1))
| ~ iext(uri_owl_onProperty,uri_ex_z1,X0)
| icext(uri_ex_z1,X1) ),
inference(forward_subsumption_resolution,[],[f1367,f844]) ).
fof(f1369,plain,
! [X2,X0,X1] :
( ~ iext(X0,X1,X2)
| ~ icext(uri_ex_d,X2)
| iext(X0,X1,sK17(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z1,X0)
| icext(uri_ex_z1,X1) ),
inference(resolution,[],[f919,f842]) ).
fof(f1370,plain,
! [X2,X0,X1] :
( ~ icext(uri_ex_d,X2)
| ~ iext(X0,X1,X2)
| iext(X0,X1,sK17(X0,uri_ex_d,X1))
| ~ iext(uri_owl_onProperty,uri_ex_z1,X0)
| icext(uri_ex_z1,X1) ),
inference(forward_subsumption_resolution,[],[f1369,f844]) ).
fof(f1371,plain,
! [X0] :
( ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| iodp(X0) ),
inference(resolution,[],[f932,f846]) ).
fof(f1372,plain,
! [X0] :
( ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| iodp(X0) ),
inference(forward_subsumption_resolution,[],[f1371,f848]) ).
fof(f1373,plain,
iodp(uri_ex_p),
inference(resolution,[],[f1372,f847]) ).
fof(f1491,plain,
idc(uri_ex_d),
inference(resolution,[],[f878,f846]) ).
fof(f1493,plain,
! [X0,X1] :
( ~ iext(uri_ex_p,X0,X1)
| lv(X1) ),
inference(resolution,[],[f978,f1373]) ).
fof(f1496,plain,
ic(uri_ex_z1),
inference(resolution,[],[f983,f1322]) ).
fof(f1497,plain,
ic(uri_ex_z2),
inference(resolution,[],[f983,f1323]) ).
fof(f1498,plain,
! [X0] :
( ~ ic(X0)
| iext(uri_owl_equivalentClass,X0,uri_ex_z2)
| icext(uri_ex_z2,sK7(X0,uri_ex_z2))
| icext(X0,sK7(X0,uri_ex_z2)) ),
inference(resolution,[],[f1497,f854]) ).
fof(f1499,plain,
! [X0] :
( ~ icext(uri_ex_z2,sK7(X0,uri_ex_z2))
| iext(uri_owl_equivalentClass,X0,uri_ex_z2)
| ~ ic(X0)
| ~ icext(X0,sK7(X0,uri_ex_z2)) ),
inference(resolution,[],[f1497,f855]) ).
fof(f1504,plain,
( iext(uri_owl_equivalentClass,uri_ex_z1,uri_ex_z2)
| icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2)) ),
inference(resolution,[],[f1498,f1496]) ).
fof(f1506,plain,
( icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2)) ),
inference(forward_subsumption_resolution,[],[f1504,f841]) ).
fof(f1525,definition,
( spl110_34
<=> icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2)) ),
introduced(definition,[new_symbols(definition,[spl110_34])],[avatar_definition]) ).
fof(f1526,plain,
( icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_34 ),
inference(avatar_component_clause,[],[f1525]) ).
fof(f1528,definition,
( spl110_35
<=> icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2)) ),
introduced(definition,[new_symbols(definition,[spl110_35])],[avatar_definition]) ).
fof(f1529,plain,
( icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1530,plain,
( spl110_34
| spl110_35 ),
inference(avatar_split_clause,[],[f1506,f1528,f1525]) ).
fof(f1531,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(X0,sK7(uri_ex_z1,uri_ex_z2),X1)
| ~ icext(X2,X1)
| ~ iext(X0,sK7(uri_ex_z1,uri_ex_z2),X3)
| ~ icext(X2,X3)
| X1 = X3
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z1,X0)
| ~ iext(uri_owl_onClass,uri_ex_z1,X2) )
| ~ spl110_34 ),
inference(resolution,[],[f1526,f913]) ).
fof(f1532,plain,
( ! [X0,X1] :
( icext(X0,sK19(X1,X0,sK7(uri_ex_z1,uri_ex_z2)))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z1,X1)
| ~ iext(uri_owl_onClass,uri_ex_z1,X0) )
| ~ spl110_34 ),
inference(resolution,[],[f1526,f914]) ).
fof(f1533,plain,
( ! [X0,X1] :
( iext(X0,sK7(uri_ex_z1,uri_ex_z2),sK19(X0,X1,sK7(uri_ex_z1,uri_ex_z2)))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z1,X0)
| ~ iext(uri_owl_onClass,uri_ex_z1,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1526,f915]) ).
fof(f1542,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z1,X0)
| iext(X0,sK7(uri_ex_z1,uri_ex_z2),sK19(X0,X1,sK7(uri_ex_z1,uri_ex_z2)))
| ~ iext(uri_owl_onClass,uri_ex_z1,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f1533,f844]) ).
fof(f1543,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z1,X1)
| icext(X0,sK19(X1,X0,sK7(uri_ex_z1,uri_ex_z2)))
| ~ iext(uri_owl_onClass,uri_ex_z1,X0) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f1532,f844]) ).
fof(f1544,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z1,X0)
| ~ icext(X2,X1)
| ~ iext(X0,sK7(uri_ex_z1,uri_ex_z2),X3)
| ~ icext(X2,X3)
| X1 = X3
| ~ iext(X0,sK7(uri_ex_z1,uri_ex_z2),X1)
| ~ iext(uri_owl_onClass,uri_ex_z1,X2) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f1531,f844]) ).
fof(f1545,plain,
( ! [X0] :
( ~ iext(uri_owl_onClass,uri_ex_z1,X0)
| icext(X0,sK19(uri_ex_p,X0,sK7(uri_ex_z1,uri_ex_z2))) )
| ~ spl110_34 ),
inference(resolution,[],[f1543,f843]) ).
fof(f1546,plain,
( ! [X0] :
( ~ iext(uri_owl_onClass,uri_ex_z1,X0)
| iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK19(uri_ex_p,X0,sK7(uri_ex_z1,uri_ex_z2))) )
| ~ spl110_34 ),
inference(resolution,[],[f1542,f843]) ).
fof(f1547,plain,
( icext(uri_ex_d,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_34 ),
inference(resolution,[],[f1545,f842]) ).
fof(f1548,plain,
( iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_34 ),
inference(resolution,[],[f1546,f842]) ).
fof(f1549,plain,
( lv(sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_34 ),
inference(resolution,[],[f1548,f1493]) ).
fof(f1678,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(uri_owl_onDataRange,X0,X3)
| ~ iext(X2,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(X3,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(X3,sK21(X2,X3,X1))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X2)
| icext(X0,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1549,f925]) ).
fof(f1680,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(uri_owl_onDataRange,X0,X3)
| ~ iext(X2,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(X3,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| lv(sK21(X2,X3,X1))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X2)
| icext(X0,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1549,f927]) ).
fof(f1681,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(uri_owl_onDataRange,X0,X3)
| ~ iext(X2,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(X3,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(X3,sK20(X2,X3,X1))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X2)
| icext(X0,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1549,f928]) ).
fof(f1682,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(uri_owl_onDataRange,X0,X3)
| ~ iext(X2,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(X3,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| iext(X2,X1,sK20(X2,X3,X1))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X2)
| icext(X0,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1549,f929]) ).
fof(f1683,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(uri_owl_onDataRange,X0,X3)
| ~ iext(X2,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(X3,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| lv(sK20(X2,X3,X1))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X2)
| icext(X0,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1549,f930]) ).
fof(f1709,plain,
( ! [X2,X0,X1] :
( ~ iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),X1)
| ~ iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),X2)
| ~ icext(X0,X2)
| X1 = X2
| ~ icext(X0,X1)
| ~ iext(uri_owl_onClass,uri_ex_z1,X0) )
| ~ spl110_34 ),
inference(resolution,[],[f1544,f843]) ).
fof(f1794,plain,
( ~ icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| spl110_35 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1878,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(uri_ex_d,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_d,sK20(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1681,f846]) ).
fof(f1879,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_d,sK20(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f1878,f1547]) ).
fof(f1880,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_d,sK20(X0,uri_ex_d,X1))
| ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f1879,f848]) ).
fof(f1881,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_d,sK20(uri_ex_p,uri_ex_d,X0))
| icext(uri_ex_z2,X0) )
| ~ spl110_34 ),
inference(resolution,[],[f1880,f847]) ).
fof(f1882,plain,
( icext(uri_ex_d,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_34 ),
inference(resolution,[],[f1881,f1548]) ).
fof(f1894,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(uri_ex_d,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_d,sK21(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1678,f846]) ).
fof(f1895,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_d,sK21(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f1894,f1547]) ).
fof(f1896,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_d,sK21(X0,uri_ex_d,X1))
| ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f1895,f848]) ).
fof(f1897,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_d,sK21(uri_ex_p,uri_ex_d,X0))
| icext(uri_ex_z2,X0) )
| ~ spl110_34 ),
inference(resolution,[],[f1896,f847]) ).
fof(f1898,plain,
( icext(uri_ex_d,sK21(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_34 ),
inference(resolution,[],[f1897,f1548]) ).
fof(f1976,plain,
! [X0] :
( ~ icext(uri_ex_d,X0)
| lv(X0) ),
inference(resolution,[],[f940,f1491]) ).
fof(f1998,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(uri_ex_d,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| lv(sK20(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1683,f846]) ).
fof(f1999,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| lv(sK20(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f1998,f1547]) ).
fof(f2000,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| lv(sK20(X0,uri_ex_d,X1))
| ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f1999,f848]) ).
fof(f2001,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| lv(sK20(uri_ex_p,uri_ex_d,X0))
| icext(uri_ex_z2,X0) )
| ~ spl110_34 ),
inference(resolution,[],[f2000,f847]) ).
fof(f2002,plain,
( lv(sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_34 ),
inference(resolution,[],[f2001,f1548]) ).
fof(f2003,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(uri_ex_d,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| lv(sK21(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1680,f846]) ).
fof(f2004,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| lv(sK21(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f2003,f1547]) ).
fof(f2005,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| lv(sK21(X0,uri_ex_d,X1))
| ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f2004,f848]) ).
fof(f2006,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| lv(sK21(uri_ex_p,uri_ex_d,X0))
| icext(uri_ex_z2,X0) )
| ~ spl110_34 ),
inference(resolution,[],[f2005,f847]) ).
fof(f2007,plain,
( lv(sK21(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_34 ),
inference(resolution,[],[f2006,f1548]) ).
fof(f2028,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(uri_ex_d,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| iext(X0,X1,sK20(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(resolution,[],[f1682,f846]) ).
fof(f2029,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| iext(X0,X1,sK20(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f2028,f1547]) ).
fof(f2030,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| iext(X0,X1,sK20(X0,uri_ex_d,X1))
| ~ iext(X0,X1,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,X1) )
| ~ spl110_34 ),
inference(forward_subsumption_resolution,[],[f2029,f848]) ).
fof(f2031,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,sK19(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| iext(uri_ex_p,X0,sK20(uri_ex_p,uri_ex_d,X0))
| icext(uri_ex_z2,X0) )
| ~ spl110_34 ),
inference(resolution,[],[f2030,f847]) ).
fof(f2032,plain,
( iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_34 ),
inference(resolution,[],[f2031,f1548]) ).
fof(f2043,definition,
( spl110_61
<=> icext(uri_ex_d,sK17(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))) ),
introduced(definition,[new_symbols(definition,[spl110_61])],[avatar_definition]) ).
fof(f2044,plain,
( icext(uri_ex_d,sK17(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_61 ),
inference(avatar_component_clause,[],[f2043]) ).
fof(f2050,definition,
( spl110_63
<=> icext(uri_ex_d,sK18(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))) ),
introduced(definition,[new_symbols(definition,[spl110_63])],[avatar_definition]) ).
fof(f2051,plain,
( icext(uri_ex_d,sK18(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_63 ),
inference(avatar_component_clause,[],[f2050]) ).
fof(f2062,plain,
( iext(uri_owl_equivalentClass,uri_ex_z1,uri_ex_z2)
| ~ ic(uri_ex_z1)
| ~ icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35 ),
inference(resolution,[],[f1529,f1499]) ).
fof(f2079,plain,
( ~ ic(uri_ex_z1)
| ~ icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2062,f841]) ).
fof(f2080,plain,
( ~ icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2079,f1496]) ).
fof(f2083,plain,
( icext(uri_ex_d,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_34
| spl110_35 ),
inference(forward_subsumption_resolution,[],[f1882,f1794]) ).
fof(f2084,plain,
( icext(uri_ex_d,sK21(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_34
| spl110_35 ),
inference(forward_subsumption_resolution,[],[f1898,f1794]) ).
fof(f2085,plain,
( lv(sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_34
| spl110_35 ),
inference(forward_subsumption_resolution,[],[f2002,f1794]) ).
fof(f2086,plain,
( lv(sK21(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_34
| spl110_35 ),
inference(forward_subsumption_resolution,[],[f2007,f1794]) ).
fof(f2087,plain,
( iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_34
| spl110_35 ),
inference(forward_subsumption_resolution,[],[f2032,f1794]) ).
fof(f2089,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onClass,uri_ex_z1,X1)
| ~ icext(X1,X0)
| sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X0
| ~ icext(X1,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),X0) )
| ~ spl110_34
| spl110_35 ),
inference(resolution,[],[f2087,f1709]) ).
fof(f2121,plain,
( ! [X2,X3,X0,X1] :
( ~ iext(uri_owl_onDataRange,X0,X3)
| ~ iext(X2,X1,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(X3,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| iext(X2,X1,sK21(X2,X3,X1))
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X0,X2)
| icext(X0,X1) )
| ~ spl110_34
| spl110_35 ),
inference(resolution,[],[f2085,f926]) ).
fof(f2174,plain,
( ! [X0] :
( ~ icext(uri_ex_d,X0)
| sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X0
| ~ icext(uri_ex_d,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),X0) )
| ~ spl110_34
| spl110_35 ),
inference(resolution,[],[f2089,f842]) ).
fof(f2175,plain,
( ! [X0] :
( ~ iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),X0)
| sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X0
| ~ icext(uri_ex_d,X0) )
| ~ spl110_34
| spl110_35 ),
inference(forward_subsumption_resolution,[],[f2174,f2083]) ).
fof(f2192,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(uri_ex_d,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| iext(X0,X1,sK21(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34
| spl110_35 ),
inference(resolution,[],[f2121,f846]) ).
fof(f2193,plain,
( ! [X0,X1] :
( ~ iext(X0,X1,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| iext(X0,X1,sK21(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| icext(uri_ex_z2,X1) )
| ~ spl110_34
| spl110_35 ),
inference(forward_subsumption_resolution,[],[f2192,f2083]) ).
fof(f2194,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| iext(X0,X1,sK21(X0,uri_ex_d,X1))
| ~ iext(X0,X1,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,X1) )
| ~ spl110_34
| spl110_35 ),
inference(forward_subsumption_resolution,[],[f2193,f848]) ).
fof(f2195,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| iext(uri_ex_p,X0,sK21(uri_ex_p,uri_ex_d,X0))
| icext(uri_ex_z2,X0) )
| ~ spl110_34
| spl110_35 ),
inference(resolution,[],[f2194,f847]) ).
fof(f2196,plain,
( iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK21(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_34
| spl110_35 ),
inference(resolution,[],[f2195,f2087]) ).
fof(f2197,plain,
( iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK21(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_34
| spl110_35 ),
inference(forward_subsumption_resolution,[],[f2196,f1794]) ).
fof(f2198,plain,
( sK21(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))
| ~ icext(uri_ex_d,sK21(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_34
| spl110_35 ),
inference(resolution,[],[f2197,f2175]) ).
fof(f2214,plain,
( sK21(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = sK20(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_34
| spl110_35 ),
inference(forward_subsumption_resolution,[],[f2198,f2084]) ).
fof(f2219,plain,
( $false
| ~ spl110_34
| spl110_35 ),
inference(unit_resulting_resolution,[],[f931,f846,f847,f1794,f848,f2086,f2084,f2197,f2214]) ).
fof(f2234,plain,
( ~ spl110_34
| spl110_35 ),
inference(avatar_contradiction_clause,[],[f2219]) ).
fof(f2253,plain,
( ! [X0,X1] :
( icext(X0,sK22(X1,X0,sK7(uri_ex_z1,uri_ex_z2)))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X1)
| ~ iext(uri_owl_onDataRange,uri_ex_z2,X0) )
| ~ spl110_35 ),
inference(resolution,[],[f1529,f922]) ).
fof(f2254,plain,
( ! [X0,X1] :
( iext(X0,sK7(uri_ex_z1,uri_ex_z2),sK22(X0,X1,sK7(uri_ex_z1,uri_ex_z2)))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| ~ iext(uri_owl_onDataRange,uri_ex_z2,X1) )
| ~ spl110_35 ),
inference(resolution,[],[f1529,f923]) ).
fof(f2257,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| iext(X0,sK7(uri_ex_z1,uri_ex_z2),sK22(X0,X1,sK7(uri_ex_z1,uri_ex_z2)))
| ~ iext(uri_owl_onDataRange,uri_ex_z2,X1) )
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2254,f848]) ).
fof(f2258,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z2,X1)
| icext(X0,sK22(X1,X0,sK7(uri_ex_z1,uri_ex_z2)))
| ~ iext(uri_owl_onDataRange,uri_ex_z2,X0) )
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2253,f848]) ).
fof(f2262,plain,
( ! [X0] :
( ~ iext(uri_owl_onDataRange,uri_ex_z2,X0)
| icext(X0,sK22(uri_ex_p,X0,sK7(uri_ex_z1,uri_ex_z2))) )
| ~ spl110_35 ),
inference(resolution,[],[f2258,f847]) ).
fof(f2263,plain,
( ! [X0] :
( ~ iext(uri_owl_onDataRange,uri_ex_z2,X0)
| iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK22(uri_ex_p,X0,sK7(uri_ex_z1,uri_ex_z2))) )
| ~ spl110_35 ),
inference(resolution,[],[f2257,f847]) ).
fof(f2264,plain,
( icext(uri_ex_d,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_35 ),
inference(resolution,[],[f2262,f846]) ).
fof(f2265,plain,
( lv(sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_35 ),
inference(resolution,[],[f2264,f1976]) ).
fof(f2266,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z1,X0)
| iext(X0,X1,sK17(X0,uri_ex_d,X1))
| ~ iext(X0,X1,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z1,X1) )
| ~ spl110_35 ),
inference(resolution,[],[f2264,f1370]) ).
fof(f2267,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z1,X0)
| iext(X0,X1,sK18(X0,uri_ex_d,X1))
| ~ iext(X0,X1,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z1,X1) )
| ~ spl110_35 ),
inference(resolution,[],[f2264,f1368]) ).
fof(f2271,plain,
( ! [X2,X0,X1] :
( ~ iext(uri_owl_onClass,X2,uri_ex_d)
| icext(X2,X1)
| icext(uri_ex_d,sK18(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,X2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X2,X0)
| ~ iext(X0,X1,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))) )
| ~ spl110_35 ),
inference(resolution,[],[f2264,f916]) ).
fof(f2272,plain,
( ! [X2,X0,X1] :
( ~ iext(uri_owl_onClass,X2,uri_ex_d)
| icext(X2,X1)
| icext(uri_ex_d,sK17(X0,uri_ex_d,X1))
| ~ iext(uri_owl_qualifiedCardinality,X2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X2,X0)
| ~ iext(X0,X1,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))) )
| ~ spl110_35 ),
inference(resolution,[],[f2264,f918]) ).
fof(f2277,plain,
( iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_35 ),
inference(resolution,[],[f2263,f846]) ).
fof(f2300,plain,
( ! [X0,X1] :
( icext(uri_ex_z1,X0)
| icext(uri_ex_d,sK17(X1,uri_ex_d,X0))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z1,X1)
| ~ iext(X1,X0,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))) )
| ~ spl110_35 ),
inference(resolution,[],[f2272,f842]) ).
fof(f2301,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z1,X1)
| icext(uri_ex_d,sK17(X1,uri_ex_d,X0))
| icext(uri_ex_z1,X0)
| ~ iext(X1,X0,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))) )
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2300,f844]) ).
fof(f2307,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z1,X0)
| icext(uri_ex_d,sK17(uri_ex_p,uri_ex_d,X0)) )
| ~ spl110_35 ),
inference(resolution,[],[f2301,f843]) ).
fof(f2308,plain,
( icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2))
| icext(uri_ex_d,sK17(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_35 ),
inference(resolution,[],[f2307,f2277]) ).
fof(f2309,plain,
( icext(uri_ex_d,sK17(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2308,f2080]) ).
fof(f2310,plain,
( spl110_61
| ~ spl110_35 ),
inference(avatar_split_clause,[],[f2309,f1528,f2043]) ).
fof(f2322,plain,
( ! [X0,X1] :
( icext(uri_ex_z1,X0)
| icext(uri_ex_d,sK18(X1,uri_ex_d,X0))
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z1,X1)
| ~ iext(X1,X0,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))) )
| ~ spl110_35 ),
inference(resolution,[],[f2271,f842]) ).
fof(f2323,plain,
( ! [X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z1,X1)
| icext(uri_ex_d,sK18(X1,uri_ex_d,X0))
| icext(uri_ex_z1,X0)
| ~ iext(X1,X0,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))) )
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2322,f844]) ).
fof(f2324,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z1,X0)
| icext(uri_ex_d,sK18(uri_ex_p,uri_ex_d,X0)) )
| ~ spl110_35 ),
inference(resolution,[],[f2323,f843]) ).
fof(f2325,plain,
( icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2))
| icext(uri_ex_d,sK18(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_35 ),
inference(resolution,[],[f2324,f2277]) ).
fof(f2326,plain,
( icext(uri_ex_d,sK18(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2325,f2080]) ).
fof(f2327,plain,
( spl110_63
| ~ spl110_35 ),
inference(avatar_split_clause,[],[f2326,f1528,f2050]) ).
fof(f2339,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ iext(uri_owl_onDataRange,X4,X3)
| ~ iext(X1,X2,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(X3,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ lv(X0)
| ~ iext(X1,X2,X0)
| ~ icext(X3,X0)
| ~ icext(X4,X2)
| ~ iext(uri_owl_qualifiedCardinality,X4,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,X4,X1)
| sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X0 )
| ~ spl110_35 ),
inference(resolution,[],[f2265,f921]) ).
fof(f2346,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| iext(uri_ex_p,X0,sK17(uri_ex_p,uri_ex_d,X0))
| icext(uri_ex_z1,X0) )
| ~ spl110_35 ),
inference(resolution,[],[f2266,f843]) ).
fof(f2347,plain,
( iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK17(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35 ),
inference(resolution,[],[f2346,f2277]) ).
fof(f2348,plain,
( iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK17(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2347,f2080]) ).
fof(f2351,plain,
( ! [X0] :
( ~ iext(uri_ex_p,X0,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| iext(uri_ex_p,X0,sK18(uri_ex_p,uri_ex_d,X0))
| icext(uri_ex_z1,X0) )
| ~ spl110_35 ),
inference(resolution,[],[f2267,f843]) ).
fof(f2352,plain,
( iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK18(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| icext(uri_ex_z1,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35 ),
inference(resolution,[],[f2351,f2277]) ).
fof(f2353,plain,
( iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),sK18(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2352,f2080]) ).
fof(f2356,plain,
( ! [X2,X0,X1] :
( ~ iext(X0,X1,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(uri_ex_d,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ lv(X2)
| ~ iext(X0,X1,X2)
| ~ icext(uri_ex_d,X2)
| ~ icext(uri_ex_z2,X1)
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X2 )
| ~ spl110_35 ),
inference(resolution,[],[f2339,f846]) ).
fof(f2357,plain,
( ! [X2,X0,X1] :
( ~ iext(X0,X1,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ lv(X2)
| ~ iext(X0,X1,X2)
| ~ icext(uri_ex_d,X2)
| ~ icext(uri_ex_z2,X1)
| ~ iext(uri_owl_qualifiedCardinality,uri_ex_z2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X2 )
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2356,f2264]) ).
fof(f2358,plain,
( ! [X2,X0,X1] :
( ~ iext(X0,X1,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ lv(X2)
| ~ iext(X0,X1,X2)
| ~ icext(uri_ex_d,X2)
| ~ icext(uri_ex_z2,X1)
| ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X2 )
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2357,f848]) ).
fof(f2359,plain,
( ! [X2,X0,X1] :
( ~ iext(uri_owl_onProperty,uri_ex_z2,X0)
| ~ iext(X0,X1,X2)
| ~ icext(uri_ex_d,X2)
| ~ icext(uri_ex_z2,X1)
| ~ iext(X0,X1,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X2 )
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2358,f1976]) ).
fof(f2360,plain,
( ! [X0,X1] :
( ~ iext(uri_ex_p,X0,sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| ~ icext(uri_ex_d,X1)
| ~ icext(uri_ex_z2,X0)
| ~ iext(uri_ex_p,X0,X1)
| sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X1 )
| ~ spl110_35 ),
inference(resolution,[],[f2359,f847]) ).
fof(f2361,plain,
( ! [X0] :
( ~ icext(uri_ex_d,X0)
| ~ icext(uri_ex_z2,sK7(uri_ex_z1,uri_ex_z2))
| ~ iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),X0)
| sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X0 )
| ~ spl110_35 ),
inference(resolution,[],[f2360,f2277]) ).
fof(f2362,plain,
( ! [X0] :
( ~ iext(uri_ex_p,sK7(uri_ex_z1,uri_ex_z2),X0)
| ~ icext(uri_ex_d,X0)
| sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = X0 )
| ~ spl110_35 ),
inference(forward_subsumption_resolution,[],[f2361,f1529]) ).
fof(f2363,plain,
( ~ icext(uri_ex_d,sK17(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| sK17(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35 ),
inference(resolution,[],[f2362,f2348]) ).
fof(f2364,plain,
( ~ icext(uri_ex_d,sK18(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)))
| sK18(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35 ),
inference(resolution,[],[f2362,f2353]) ).
fof(f2366,plain,
( sK18(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35
| ~ spl110_63 ),
inference(forward_subsumption_resolution,[],[f2364,f2051]) ).
fof(f2367,plain,
( sK17(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = sK22(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35
| ~ spl110_61 ),
inference(forward_subsumption_resolution,[],[f2363,f2044]) ).
fof(f2385,plain,
( sK18(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2)) = sK17(uri_ex_p,uri_ex_d,sK7(uri_ex_z1,uri_ex_z2))
| ~ spl110_35
| ~ spl110_61
| ~ spl110_63 ),
inference(superposition,[],[f2367,f2366]) ).
fof(f2394,plain,
( $false
| ~ spl110_35
| ~ spl110_61
| ~ spl110_63 ),
inference(unit_resulting_resolution,[],[f920,f842,f843,f2080,f844,f2264,f2277,f2385]) ).
fof(f2401,plain,
( ~ spl110_35
| ~ spl110_61
| ~ spl110_63 ),
inference(avatar_contradiction_clause,[],[f2394]) ).
cnf(s27,plain,
( spl110_34
| spl110_35 ),
inference(sat_conversion,[],[f1530]) ).
cnf(s58,plain,
( ~ spl110_34
| spl110_35 ),
inference(sat_conversion,[],[f2234]) ).
cnf(s62,plain,
( ~ spl110_35
| spl110_61 ),
inference(sat_conversion,[],[f2310]) ).
cnf(s63,plain,
( ~ spl110_35
| spl110_63 ),
inference(sat_conversion,[],[f2327]) ).
cnf(s66,plain,
( ~ spl110_35
| ~ spl110_61
| ~ spl110_63 ),
inference(sat_conversion,[],[f2401]) ).
cnf(s68,plain,
~ spl110_35,
inference(rat,[],[s66,s62,s63]) ).
cnf(s69,plain,
~ spl110_34,
inference(rat,[],[s58,s68]) ).
cnf(s70,plain,
$false,
inference(rat,[],[s27,s68,s69]) ).
fof(f2403,plain,
$false,
inference(avatar_sat_refutation,[],[s70]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB102+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n001.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 07:27:02 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.09/1.70 % (183929)Detected formulas, will run a generic FOF schedule.
% 5.09/1.70 % (183935)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=3903565299:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.09/1.70 % (183938)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3910785924:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.09/1.70 % (183934)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=628356375:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.09/1.70 % (183937)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2604304445:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.09/1.70 % (183936)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=2365964281:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.09/1.70 % (183939)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2722690881:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.09/1.70 % (183940)dis-21_1_sil=8000:lcm=predicate:random_seed=3575998636:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.09/1.70 % (183937)Refutation not found, incomplete strategy
% 5.09/1.70 % (183937)------------------------------
% 5.09/1.70 % (183937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.09/1.70 % (183937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.09/1.70 % (183937)CaDiCaL version: 2.1.3
% 5.09/1.70 % (183937)Termination reason: Refutation not found, incomplete strategy
% 5.09/1.70 % (183937)Time elapsed: 0.002 s
% 5.09/1.70 % (183937)Peak memory usage: 88 MB
% 5.09/1.70 % (183937)Instructions burned: 2 (million)
% 5.09/1.70 % (183938)Refutation not found, incomplete strategy
% 5.09/1.70 % (183938)------------------------------
% 5.09/1.70 % (183938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.09/1.70 % (183938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.09/1.70 % (183938)CaDiCaL version: 2.1.3
% 5.09/1.70 % (183938)Termination reason: Refutation not found, incomplete strategy
% 5.09/1.70 % (183938)Time elapsed: 0.003 s
% 5.09/1.70 % (183938)Peak memory usage: 88 MB
% 5.09/1.70 % (183938)Instructions burned: 2 (million)
% 5.09/1.70 % (183940)Instruction limit reached!
% 5.09/1.70 % (183940)------------------------------
% 5.09/1.70 % (183940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.09/1.70 % (183940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.09/1.70 % (183940)CaDiCaL version: 2.1.3
% 5.09/1.70 % (183940)Termination reason: Instruction limit
% 5.09/1.70 % (183940)Termination phase: Saturation
% 5.09/1.70 % (183940)Time elapsed: 0.068 s
% 5.09/1.70 % (183940)Peak memory usage: 91 MB
% 5.09/1.70 % (183940)Instructions burned: 130 (million)
% 5.09/1.70 % (183939)Instruction limit reached!
% 5.09/1.70 % (183939)------------------------------
% 5.09/1.70 % (183939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.09/1.70 % (183939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.09/1.70 % (183939)CaDiCaL version: 2.1.3
% 5.09/1.70 % (183939)Termination reason: Instruction limit
% 5.09/1.70 % (183939)Termination phase: Saturation
% 5.09/1.70 % (183939)Time elapsed: 0.081 s
% 5.09/1.70 % (183939)Peak memory usage: 90 MB
% 5.09/1.70 % (183939)Instructions burned: 140 (million)
% 5.09/1.70 % (183948)lrs+10_1_sil=8000:sp=occurrence:random_seed=2773734732:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.09/1.70 % (183937)------------------------------
% 5.09/1.70 % (183937)------------------------------
% 5.09/1.70 % (183938)------------------------------
% 5.09/1.70 % (183938)------------------------------
% 5.09/1.70 % (183949)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3926506189:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.09/1.70 % (183949)Refutation not found, incomplete strategy
% 5.09/1.70 % (183949)------------------------------
% 5.09/1.70 % (183949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.09/1.70 % (183949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.09/1.70 % (183949)CaDiCaL version: 2.1.3
% 5.09/1.70 % (183949)Termination reason: Refutation not found, incomplete strategy
% 5.09/1.70 % (183949)Time elapsed: 0.004 s
% 5.09/1.70 % (183949)Peak memory usage: 89 MB
% 5.09/1.70 % (183949)Instructions burned: 6 (million)
% 5.09/1.70 % (183948)Instruction limit reached!
% 5.09/1.70 % (183948)------------------------------
% 5.09/1.70 % (183948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.09/1.70 % (183948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.09/1.70 % (183948)CaDiCaL version: 2.1.3
% 5.09/1.70 % (183948)Termination reason: Instruction limit
% 5.09/1.70 % (183948)Termination phase: Saturation
% 5.09/1.70 % (183948)Time elapsed: 0.166 s
% 5.09/1.70 % (183948)Peak memory usage: 93 MB
% 5.09/1.70 % (183948)Instructions burned: 285 (million)
% 5.09/1.70 % (183952)lrs+1011_1_sil=32000:sp=occurrence:random_seed=666428838:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 5.09/1.70 % (183953)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=511083530:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.09/1.70 % (183952)Refutation not found, incomplete strategy
% 5.09/1.70 % (183952)------------------------------
% 5.09/1.70 % (183952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.09/1.70 % (183952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.09/1.70 % (183952)CaDiCaL version: 2.1.3
% 5.09/1.70 % (183952)Termination reason: Refutation not found, incomplete strategy
% 5.09/1.70 % (183952)Time elapsed: 0.003 s
% 5.09/1.70 % (183952)Peak memory usage: 89 MB
% 5.09/1.70 % (183952)Instructions burned: 2 (million)
% 5.09/1.70 % (183935)First to succeed.
% 5.09/1.70 % (183935)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-183929"
% 5.09/1.70 % (183949)------------------------------
% 5.09/1.70 % (183949)------------------------------
% 5.09/1.70 % (183953)Instruction limit reached!
% 5.09/1.70 % (183953)------------------------------
% 5.09/1.70 % (183953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.09/1.70 % (183953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.09/1.70 % (183953)CaDiCaL version: 2.1.3
% 5.09/1.70 % (183953)Termination reason: Instruction limit
% 5.09/1.70 % (183953)Termination phase: Saturation
% 5.09/1.70 % (183953)Time elapsed: 0.123 s
% 5.09/1.70 % (183953)Peak memory usage: 90 MB
% 5.09/1.70 % (183953)Instructions burned: 248 (million)
% 5.09/1.70 % (183954)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2404404491:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 5.09/1.70 % (183954)Refutation not found, incomplete strategy
% 5.09/1.70 % (183954)------------------------------
% 5.09/1.70 % (183954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.09/1.70 % (183954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.09/1.70 % (183954)CaDiCaL version: 2.1.3
% 5.09/1.70 % (183954)Termination reason: Refutation not found, incomplete strategy
% 5.09/1.70 % (183954)Time elapsed: 0.010 s
% 5.09/1.70 % (183954)Peak memory usage: 89 MB
% 5.09/1.70 % (183954)Instructions burned: 15 (million)
% 5.09/1.70 % (183935)Refutation found. Thanks to Tanya!
% 5.09/1.70 % SZS status Theorem for theBenchmark
% 5.09/1.70 % SZS output start Proof for theBenchmark
% See solution above
% 6.31/1.89 % (183935)------------------------------
% 6.31/1.89 % (183935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.89 % (183935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.89 % (183935)CaDiCaL version: 2.1.3
% 6.31/1.89 % (183935)Termination reason: Refutation
% 6.31/1.89 % (183935)Time elapsed: 0.515 s
% 6.31/1.89 % (183935)Peak memory usage: 137 MB
% 6.31/1.89 % (183935)Instructions burned: 1391 (million)
% 6.31/1.89 % (183935)------------------------------
% 6.31/1.89 % (183935)------------------------------
% 6.31/1.89 % (183929)Success in time 0.825 s
% 6.31/1.89 % Vampire exiting
%------------------------------------------------------------------------------