%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWB029+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.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 : Fri Sep 25 03:03:52 PM UTC 2026
% Result : Theorem 39.48s 5.52s
% Output : Proof 39.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 92
% Syntax : Number of formulae : 417 ( 43 unt; 0 def)
% Number of atoms : 2547 ( 275 equ)
% Maximal formula atoms : 60 ( 6 avg)
% Number of connectives : 3713 (1583 ~;1237 |; 818 &)
% ( 35 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 42 ( 7 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 131 ( 131 usr; 60 con; 0-7 aty)
% Number of variables : 1300 ( 29 sgn 810 !; 113 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rdfs_cext_def) ).
fof(f24_nnf,plain,
! [X,C] :
( ( ~ icext(C,X)
| iext(uri_rdf_type,X,C) )
& ( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X,C] :
( ( ~ icext(C,X)
| iext(uri_rdf_type,X,C) )
& ( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c25,plain,
( icext(X1,X0)
| ~ iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi25,axiom,
ifeq(iext(uri_rdf_type,X0,X1),true,icext(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
fof(f559,axiom,
? [BNODE_x,BNODE_y,BNODE_l1,BNODE_l2] :
( iext(uri_owl_complementOf,BNODE_y,uri_ex_A)
& iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,BNODE_y)
& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_ex_A)
& iext(uri_owl_intersectionOf,BNODE_x,BNODE_l1)
& iext(uri_rdf_type,uri_ex_w,BNODE_x)
& iext(uri_rdf_type,uri_ex_B,uri_owl_Class)
& iext(uri_rdf_type,uri_ex_A,uri_owl_Class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',testcase_premise_fullish_029_Ex_Falso_Quodlibet) ).
fof(f559_nnf,plain,
? [BNODE_x,BNODE_y,BNODE_l1,BNODE_l2] :
( iext(uri_owl_complementOf,BNODE_y,uri_ex_A)
& iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,BNODE_y)
& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_ex_A)
& iext(uri_owl_intersectionOf,BNODE_x,BNODE_l1)
& iext(uri_rdf_type,uri_ex_w,BNODE_x)
& iext(uri_rdf_type,uri_ex_B,uri_owl_Class)
& iext(uri_rdf_type,uri_ex_A,uri_owl_Class) ),
inference(nnf_transformation,[status(thm)],[f559]) ).
fof(f559_sk,plain,
( iext(uri_owl_complementOf,sk200,uri_ex_A)
& iext(uri_rdf_rest,sk202,uri_rdf_nil)
& iext(uri_rdf_first,sk202,sk200)
& iext(uri_rdf_rest,sk201,sk202)
& iext(uri_rdf_first,sk201,uri_ex_A)
& iext(uri_owl_intersectionOf,sk199,sk201)
& iext(uri_rdf_type,uri_ex_w,sk199)
& iext(uri_rdf_type,uri_ex_B,uri_owl_Class)
& iext(uri_rdf_type,uri_ex_A,uri_owl_Class) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk199,sk200,sk201,sk202])],[f559_nnf]) ).
cnf(c1409,plain,
iext(uri_rdf_type,uri_ex_w,sk199),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(hi1106,axiom,
iext(uri_rdf_type,uri_ex_w,sk199) = true,
inference(equality_encoding,[status(esa)],[c1409]) ).
cnf(h72434,plain,
icext(sk199,uri_ex_w) = true,
inference(hyper_resolution,[status(thm)],[hi25,hi1106]) ).
fof(f281,axiom,
! [Z,S1,C1,S2,C2] :
( ( iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_intersectionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C2,X)
& icext(C1,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_bool_intersectionof_class_002) ).
fof(f281_nnf,plain,
! [Z,S1,C1,S2,C2] :
( ( ( ? [X] :
( ( icext(C2,X)
& icext(C1,X)
& ~ icext(Z,X) )
| ( ( ~ icext(C2,X)
| ~ icext(C1,X) )
& icext(Z,X) ) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_intersectionOf,Z,S1) )
& ( ( ! [X] :
( ( ~ icext(C2,X)
| ~ icext(C1,X)
| icext(Z,X) )
& ( ( icext(C2,X)
& icext(C1,X) )
| ~ icext(Z,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(nnf_transformation,[status(thm)],[f281]) ).
fof(f281_sk,plain,
! [S1,C1,S2,C2,Z,X] :
( ( ( ( icext(C2,sk3(Z,S1,C1,S2,C2))
& icext(C1,sk3(Z,S1,C1,S2,C2))
& ~ icext(Z,sk3(Z,S1,C1,S2,C2)) )
| ( ( ~ icext(C2,sk3(Z,S1,C1,S2,C2))
| ~ icext(C1,sk3(Z,S1,C1,S2,C2)) )
& icext(Z,sk3(Z,S1,C1,S2,C2)) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_intersectionOf,Z,S1) )
& ( ( ( ~ icext(C2,X)
| ~ icext(C1,X)
| icext(Z,X) )
& ( ( icext(C2,X)
& icext(C1,X) )
| ~ icext(Z,X) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3])],[f281_nnf]) ).
cnf(c391,plain,
( icext(X2,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_intersectionOf,X0,X1)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f281_sk]) ).
cnf(hi381,axiom,
ifeq(iext(uri_rdf_first,X0,X1),true,ifeq(iext(uri_rdf_rest,X0,X2),true,ifeq(iext(uri_rdf_first,X2,X3),true,ifeq(iext(uri_rdf_rest,X2,uri_rdf_nil),true,ifeq(iext(uri_owl_intersectionOf,X4,X0),true,ifeq(icext(X4,X5),true,icext(X1,X5),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c391]) ).
cnf(c1411,plain,
iext(uri_rdf_first,sk201,uri_ex_A),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(hi1108,axiom,
iext(uri_rdf_first,sk201,uri_ex_A) = true,
inference(equality_encoding,[status(esa)],[c1411]) ).
cnf(c1412,plain,
iext(uri_rdf_rest,sk201,sk202),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(hi1109,axiom,
iext(uri_rdf_rest,sk201,sk202) = true,
inference(equality_encoding,[status(esa)],[c1412]) ).
cnf(c1413,plain,
iext(uri_rdf_first,sk202,sk200),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(hi1110,axiom,
iext(uri_rdf_first,sk202,sk200) = true,
inference(equality_encoding,[status(esa)],[c1413]) ).
cnf(c1414,plain,
iext(uri_rdf_rest,sk202,uri_rdf_nil),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(hi1111,axiom,
iext(uri_rdf_rest,sk202,uri_rdf_nil) = true,
inference(equality_encoding,[status(esa)],[c1414]) ).
cnf(c1410,plain,
iext(uri_owl_intersectionOf,sk199,sk201),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(hi1107,axiom,
iext(uri_owl_intersectionOf,sk199,sk201) = true,
inference(equality_encoding,[status(esa)],[c1410]) ).
cnf(h73319,plain,
icext(uri_ex_A,uri_ex_w) = true,
inference(hyper_resolution,[status(thm)],[hi381,hi1108,hi1109,hi1110,hi1111,hi1107,h72434]) ).
cnf(c392,plain,
( icext(X4,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_intersectionOf,X0,X1)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f281_sk]) ).
cnf(hi382,axiom,
ifeq(iext(uri_rdf_first,X0,X1),true,ifeq(iext(uri_rdf_rest,X0,X2),true,ifeq(iext(uri_rdf_first,X2,X3),true,ifeq(iext(uri_rdf_rest,X2,uri_rdf_nil),true,ifeq(iext(uri_owl_intersectionOf,X4,X0),true,ifeq(icext(X4,X5),true,icext(X3,X5),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c392]) ).
cnf(h73318,plain,
icext(sk200,uri_ex_w) = true,
inference(hyper_resolution,[status(thm)],[hi382,hi1108,hi1109,hi1110,hi1111,hi1107,h72434]) ).
fof(f277,axiom,
! [Z,C] :
( iext(uri_owl_complementOf,Z,C)
=> ( ! [X] :
( icext(Z,X)
<=> ~ icext(C,X) )
& ic(C)
& ic(Z) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_bool_complementof_class) ).
fof(f277_nnf,plain,
! [Z,C] :
( ( ! [X] :
( ( icext(C,X)
| icext(Z,X) )
& ( ~ icext(C,X)
| ~ icext(Z,X) ) )
& ic(C)
& ic(Z) )
| ~ iext(uri_owl_complementOf,Z,C) ),
inference(nnf_transformation,[status(thm)],[f277]) ).
fof(f277_sk,plain,
! [Z,C,X] :
( ( ( icext(C,X)
| icext(Z,X) )
& ( ~ icext(C,X)
| ~ icext(Z,X) )
& ic(C)
& ic(Z) )
| ~ iext(uri_owl_complementOf,Z,C) ),
inference(skolemisation,[status(esa)],[f277_nnf]) ).
cnf(c368,plain,
( ~ icext(X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_complementOf,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f277_sk]) ).
cnf(hi1116,axiom,
ifeq(iext(uri_owl_complementOf,X0,X1),true,ifeq(icext(X0,X2),true,ifeq(icext(X1,X2),true,false,true),true),true) = true,
inference(equality_encoding,[status(esa)],[c368]) ).
cnf(c1415,plain,
iext(uri_owl_complementOf,sk200,uri_ex_A),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(hi1112,axiom,
iext(uri_owl_complementOf,sk200,uri_ex_A) = true,
inference(equality_encoding,[status(esa)],[c1415]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi1116,hi1112,h73318,h73319]) ).
cnf(t2264,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f144,axiom,
! [X] : ~ icext(uri_owl_Nothing,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_class_nothing_ext) ).
fof(f144_nnf,plain,
! [X] : ~ icext(uri_owl_Nothing,X),
inference(nnf_transformation,[status(thm)],[f144]) ).
fof(f144_sk,plain,
! [X] : ~ icext(uri_owl_Nothing,X),
inference(skolemisation,[status(esa)],[f144_nnf]) ).
cnf(c173,plain,
~ icext(uri_owl_Nothing,X0),
inference(cnf_transformation,[status(esa)],[f144_sk]) ).
fof(f179,axiom,
! [X,Y] : ~ iext(uri_owl_bottomDataProperty,X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_prop_bottomdataproperty_ext) ).
fof(f179_nnf,plain,
! [X,Y] : ~ iext(uri_owl_bottomDataProperty,X,Y),
inference(nnf_transformation,[status(thm)],[f179]) ).
fof(f179_sk,plain,
! [X,Y] : ~ iext(uri_owl_bottomDataProperty,X,Y),
inference(skolemisation,[status(esa)],[f179_nnf]) ).
cnf(c220,plain,
~ iext(uri_owl_bottomDataProperty,X0,X1),
inference(cnf_transformation,[status(esa)],[f179_sk]) ).
fof(f181,axiom,
! [X,Y] : ~ iext(uri_owl_bottomObjectProperty,X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_prop_bottomobjectproperty_ext) ).
fof(f181_nnf,plain,
! [X,Y] : ~ iext(uri_owl_bottomObjectProperty,X,Y),
inference(nnf_transformation,[status(thm)],[f181]) ).
fof(f181_sk,plain,
! [X,Y] : ~ iext(uri_owl_bottomObjectProperty,X,Y),
inference(skolemisation,[status(esa)],[f181_nnf]) ).
cnf(c222,plain,
~ iext(uri_owl_bottomObjectProperty,X0,X1),
inference(cnf_transformation,[status(esa)],[f181_sk]) ).
fof(f278,axiom,
! [Z,D] :
( iext(uri_owl_datatypeComplementOf,Z,D)
=> ! [X] :
( icext(Z,X)
<=> ( ~ icext(D,X)
& lv(X) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_bool_datatypecomplementof) ).
fof(f278_nnf,plain,
! [Z,D] :
( ! [X] :
( ( icext(D,X)
| ~ lv(X)
| icext(Z,X) )
& ( ( ~ icext(D,X)
& lv(X) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_datatypeComplementOf,Z,D) ),
inference(nnf_transformation,[status(thm)],[f278]) ).
fof(f278_sk,plain,
! [Z,D,X] :
( ( ( icext(D,X)
| ~ lv(X)
| icext(Z,X) )
& ( ( ~ icext(D,X)
& lv(X) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_datatypeComplementOf,Z,D) ),
inference(skolemisation,[status(esa)],[f278_nnf]) ).
cnf(c371,plain,
( ~ icext(X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_datatypeComplementOf,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f278_sk]) ).
fof(f286,axiom,
! [Z] :
( iext(uri_owl_unionOf,Z,uri_rdf_nil)
<=> ( ! [X] : ~ icext(Z,X)
& ic(Z) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_bool_unionof_class_000) ).
fof(f286_nnf,plain,
! [Z] :
( ( ? [X] : icext(Z,X)
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,uri_rdf_nil) )
& ( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,uri_rdf_nil) ) ),
inference(nnf_transformation,[status(thm)],[f286]) ).
fof(f286_sk,plain,
! [Z,X] :
( ( icext(Z,sk5(Z))
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,uri_rdf_nil) )
& ( ( ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,uri_rdf_nil) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f286_nnf]) ).
cnf(c420,plain,
( ~ icext(X0,X1)
| ~ iext(uri_owl_unionOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
fof(f293,axiom,
! [Z] :
( iext(uri_owl_oneOf,Z,uri_rdf_nil)
<=> ( ! [X] : ~ icext(Z,X)
& ic(Z) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_enum_class_000) ).
fof(f293_nnf,plain,
! [Z] :
( ( ? [X] : icext(Z,X)
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,uri_rdf_nil) )
& ( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,uri_rdf_nil) ) ),
inference(nnf_transformation,[status(thm)],[f293]) ).
fof(f293_sk,plain,
! [Z,X] :
( ( icext(Z,sk9(Z))
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,uri_rdf_nil) )
& ( ( ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,uri_rdf_nil) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9])],[f293_nnf]) ).
cnf(c462,plain,
( ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(esa)],[f293_sk]) ).
fof(f301,axiom,
! [Z,P] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_cardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ~ ? [Y] : iext(P,X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_exactcard_000) ).
fof(f301_nnf,plain,
! [Z,P] :
( ! [X] :
( ( ? [Y] : iext(P,X,Y)
| icext(Z,X) )
& ( ! [Y] : ~ iext(P,X,Y)
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_cardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f301]) ).
fof(f301_sk,plain,
! [Z,P,X,Y] :
( ( ( iext(P,X,sk14(Z,P,X))
| icext(Z,X) )
& ( ~ iext(P,X,Y)
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_cardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14])],[f301_nnf]) ).
cnf(c500,plain,
( ~ iext(X1,X2,X3)
| ~ icext(X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_cardinality,X0,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f301_sk]) ).
fof(f303,axiom,
! [Z,P] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_cardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ( ! [Y1,Y2,Y3] :
( ( iext(P,X,Y3)
& iext(P,X,Y2)
& iext(P,X,Y1) )
=> ( Y3 = Y2
| Y3 = Y1 ) )
& ? [Y1,Y2] :
( Y1 != Y2
& iext(P,X,Y2)
& iext(P,X,Y1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_exactcard_002) ).
fof(f303_nnf,plain,
! [Z,P] :
( ! [X] :
( ( ? [Y1,Y2,Y3] :
( Y3 != Y2
& Y3 != Y1
& iext(P,X,Y3)
& iext(P,X,Y2)
& iext(P,X,Y1) )
| ! [Y1,Y2] :
( Y1 = Y2
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) )
| icext(Z,X) )
& ( ( ! [Y1,Y2,Y3] :
( Y3 = Y2
| Y3 = Y1
| ~ iext(P,X,Y3)
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) )
& ? [Y1,Y2] :
( Y1 != Y2
& iext(P,X,Y2)
& iext(P,X,Y1) ) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_cardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f303]) ).
fof(f303_sk,plain,
! [Z,P,X,Y1,Y2,Y3] :
( ( ( ( sk22(Z,P,X) != sk21(Z,P,X)
& sk22(Z,P,X) != sk20(Z,P,X)
& iext(P,X,sk22(Z,P,X))
& iext(P,X,sk21(Z,P,X))
& iext(P,X,sk20(Z,P,X)) )
| Y1 = Y2
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1)
| icext(Z,X) )
& ( ( ( Y3 = Y2
| Y3 = Y1
| ~ iext(P,X,Y3)
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) )
& sk18(Z,P,X) != sk19(Z,P,X)
& iext(P,X,sk19(Z,P,X))
& iext(P,X,sk18(Z,P,X)) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_cardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk18,sk19,sk20,sk21,sk22])],[f303_nnf]) ).
cnf(c509,plain,
( sk18(X0,X1,X2) != sk19(X0,X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_cardinality,X0,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f303_sk]) ).
fof(f304,axiom,
! [Z,P] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_cardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ( ! [Y1,Y2,Y3,Y4] :
( ( iext(P,X,Y4)
& iext(P,X,Y3)
& iext(P,X,Y2)
& iext(P,X,Y1) )
=> ( Y4 = Y3
| Y4 = Y2
| Y4 = Y1 ) )
& ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& iext(P,X,Y3)
& iext(P,X,Y2)
& iext(P,X,Y1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_exactcard_003) ).
fof(f304_nnf,plain,
! [Z,P] :
( ! [X] :
( ( ? [Y1,Y2,Y3,Y4] :
( Y4 != Y3
& Y4 != Y2
& Y4 != Y1
& iext(P,X,Y4)
& iext(P,X,Y3)
& iext(P,X,Y2)
& iext(P,X,Y1) )
| ! [Y1,Y2,Y3] :
( Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ iext(P,X,Y3)
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) )
| icext(Z,X) )
& ( ( ! [Y1,Y2,Y3,Y4] :
( Y4 = Y3
| Y4 = Y2
| Y4 = Y1
| ~ iext(P,X,Y4)
| ~ iext(P,X,Y3)
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) )
& ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& iext(P,X,Y3)
& iext(P,X,Y2)
& iext(P,X,Y1) ) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_cardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f304]) ).
fof(f304_sk,plain,
! [Z,P,X,Y1,Y2,Y3,Y4] :
( ( ( ( sk29(Z,P,X) != sk28(Z,P,X)
& sk29(Z,P,X) != sk27(Z,P,X)
& sk29(Z,P,X) != sk26(Z,P,X)
& iext(P,X,sk29(Z,P,X))
& iext(P,X,sk28(Z,P,X))
& iext(P,X,sk27(Z,P,X))
& iext(P,X,sk26(Z,P,X)) )
| Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ iext(P,X,Y3)
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1)
| icext(Z,X) )
& ( ( ( Y4 = Y3
| Y4 = Y2
| Y4 = Y1
| ~ iext(P,X,Y4)
| ~ iext(P,X,Y3)
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) )
& sk24(Z,P,X) != sk25(Z,P,X)
& sk23(Z,P,X) != sk25(Z,P,X)
& sk23(Z,P,X) != sk24(Z,P,X)
& iext(P,X,sk25(Z,P,X))
& iext(P,X,sk24(Z,P,X))
& iext(P,X,sk23(Z,P,X)) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_cardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk23,sk24,sk25,sk26,sk27,sk28,sk29])],[f304_nnf]) ).
cnf(c519,plain,
( sk23(X0,X1,X2) != sk24(X0,X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_cardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f304_sk]) ).
cnf(c520,plain,
( sk23(X0,X1,X2) != sk25(X0,X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_cardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f304_sk]) ).
cnf(c521,plain,
( sk24(X0,X1,X2) != sk25(X0,X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_cardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f304_sk]) ).
fof(f305,axiom,
! [Z,P,D] :
( ( iext(uri_owl_onDataRange,Z,D)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) )
=> ( ! [X] :
( icext(Z,X)
<=> ~ ? [Y] :
( icext(D,Y)
& iext(P,X,Y)
& lv(Y) ) )
& iodp(P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_exactqcr_data_000) ).
fof(f305_nnf,plain,
! [Z,P,D] :
( ( ! [X] :
( ( ? [Y] :
( icext(D,Y)
& iext(P,X,Y)
& lv(Y) )
| icext(Z,X) )
& ( ! [Y] :
( ~ icext(D,Y)
| ~ iext(P,X,Y)
| ~ lv(Y) )
| ~ icext(Z,X) ) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f305]) ).
fof(f305_sk,plain,
! [Z,P,D,X,Y] :
( ( ( ( icext(D,sk30(Z,P,D,X))
& iext(P,X,sk30(Z,P,D,X))
& lv(sk30(Z,P,D,X)) )
| icext(Z,X) )
& ( ~ icext(D,Y)
| ~ iext(P,X,Y)
| ~ lv(Y)
| ~ icext(Z,X) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk30])],[f305_nnf]) ).
cnf(c531,plain,
( ~ icext(X2,X4)
| ~ iext(X1,X3,X4)
| ~ lv(X4)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f305_sk]) ).
fof(f307,axiom,
! [Z,P,D] :
( ( iext(uri_owl_onDataRange,Z,D)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) )
=> ( ! [X] :
( icext(Z,X)
<=> ( ! [Y1,Y2,Y3] :
( ( icext(D,Y3)
& iext(P,X,Y3)
& lv(Y3)
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) )
=> ( Y3 = Y2
| Y3 = Y1 ) )
& ? [Y1,Y2] :
( Y1 != Y2
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) ) ) )
& iodp(P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_exactqcr_data_002) ).
fof(f307_nnf,plain,
! [Z,P,D] :
( ( ! [X] :
( ( ? [Y1,Y2,Y3] :
( Y3 != Y2
& Y3 != Y1
& icext(D,Y3)
& iext(P,X,Y3)
& lv(Y3)
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) )
| ! [Y1,Y2] :
( Y1 = Y2
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1) )
| icext(Z,X) )
& ( ( ! [Y1,Y2,Y3] :
( Y3 = Y2
| Y3 = Y1
| ~ icext(D,Y3)
| ~ iext(P,X,Y3)
| ~ lv(Y3)
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1) )
& ? [Y1,Y2] :
( Y1 != Y2
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) ) )
| ~ icext(Z,X) ) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f307]) ).
fof(f307_sk,plain,
! [Z,P,D,X,Y1,Y2,Y3] :
( ( ( ( sk38(Z,P,D,X) != sk37(Z,P,D,X)
& sk38(Z,P,D,X) != sk36(Z,P,D,X)
& icext(D,sk38(Z,P,D,X))
& iext(P,X,sk38(Z,P,D,X))
& lv(sk38(Z,P,D,X))
& icext(D,sk37(Z,P,D,X))
& iext(P,X,sk37(Z,P,D,X))
& lv(sk37(Z,P,D,X))
& icext(D,sk36(Z,P,D,X))
& iext(P,X,sk36(Z,P,D,X))
& lv(sk36(Z,P,D,X)) )
| Y1 = Y2
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1)
| icext(Z,X) )
& ( ( ( Y3 = Y2
| Y3 = Y1
| ~ icext(D,Y3)
| ~ iext(P,X,Y3)
| ~ lv(Y3)
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1) )
& sk34(Z,P,D,X) != sk35(Z,P,D,X)
& icext(D,sk35(Z,P,D,X))
& iext(P,X,sk35(Z,P,D,X))
& lv(sk35(Z,P,D,X))
& icext(D,sk34(Z,P,D,X))
& iext(P,X,sk34(Z,P,D,X))
& lv(sk34(Z,P,D,X)) )
| ~ icext(Z,X) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk34,sk35,sk36,sk37,sk38])],[f307_nnf]) ).
cnf(c554,plain,
( sk34(X0,X1,X2,X3) != sk35(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f307_sk]) ).
fof(f308,axiom,
! [Z,P,D] :
( ( iext(uri_owl_onDataRange,Z,D)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) )
=> ( ! [X] :
( icext(Z,X)
<=> ( ! [Y1,Y2,Y3,Y4] :
( ( icext(D,Y4)
& iext(P,X,Y4)
& lv(Y4)
& icext(D,Y3)
& iext(P,X,Y3)
& lv(Y3)
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) )
=> ( Y4 = Y3
| Y4 = Y2
| Y4 = Y1 ) )
& ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& icext(D,Y3)
& iext(P,X,Y3)
& lv(Y3)
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) ) ) )
& iodp(P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_exactqcr_data_003) ).
fof(f308_nnf,plain,
! [Z,P,D] :
( ( ! [X] :
( ( ? [Y1,Y2,Y3,Y4] :
( Y4 != Y3
& Y4 != Y2
& Y4 != Y1
& icext(D,Y4)
& iext(P,X,Y4)
& lv(Y4)
& icext(D,Y3)
& iext(P,X,Y3)
& lv(Y3)
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) )
| ! [Y1,Y2,Y3] :
( Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ icext(D,Y3)
| ~ iext(P,X,Y3)
| ~ lv(Y3)
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1) )
| icext(Z,X) )
& ( ( ! [Y1,Y2,Y3,Y4] :
( Y4 = Y3
| Y4 = Y2
| Y4 = Y1
| ~ icext(D,Y4)
| ~ iext(P,X,Y4)
| ~ lv(Y4)
| ~ icext(D,Y3)
| ~ iext(P,X,Y3)
| ~ lv(Y3)
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1) )
& ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& icext(D,Y3)
& iext(P,X,Y3)
& lv(Y3)
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) ) )
| ~ icext(Z,X) ) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f308]) ).
fof(f308_sk,plain,
! [Z,P,D,X,Y1,Y2,Y3,Y4] :
( ( ( ( sk45(Z,P,D,X) != sk44(Z,P,D,X)
& sk45(Z,P,D,X) != sk43(Z,P,D,X)
& sk45(Z,P,D,X) != sk42(Z,P,D,X)
& icext(D,sk45(Z,P,D,X))
& iext(P,X,sk45(Z,P,D,X))
& lv(sk45(Z,P,D,X))
& icext(D,sk44(Z,P,D,X))
& iext(P,X,sk44(Z,P,D,X))
& lv(sk44(Z,P,D,X))
& icext(D,sk43(Z,P,D,X))
& iext(P,X,sk43(Z,P,D,X))
& lv(sk43(Z,P,D,X))
& icext(D,sk42(Z,P,D,X))
& iext(P,X,sk42(Z,P,D,X))
& lv(sk42(Z,P,D,X)) )
| Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ icext(D,Y3)
| ~ iext(P,X,Y3)
| ~ lv(Y3)
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1)
| icext(Z,X) )
& ( ( ( Y4 = Y3
| Y4 = Y2
| Y4 = Y1
| ~ icext(D,Y4)
| ~ iext(P,X,Y4)
| ~ lv(Y4)
| ~ icext(D,Y3)
| ~ iext(P,X,Y3)
| ~ lv(Y3)
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1) )
& sk40(Z,P,D,X) != sk41(Z,P,D,X)
& sk39(Z,P,D,X) != sk41(Z,P,D,X)
& sk39(Z,P,D,X) != sk40(Z,P,D,X)
& icext(D,sk41(Z,P,D,X))
& iext(P,X,sk41(Z,P,D,X))
& lv(sk41(Z,P,D,X))
& icext(D,sk40(Z,P,D,X))
& iext(P,X,sk40(Z,P,D,X))
& lv(sk40(Z,P,D,X))
& icext(D,sk39(Z,P,D,X))
& iext(P,X,sk39(Z,P,D,X))
& lv(sk39(Z,P,D,X)) )
| ~ icext(Z,X) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk39,sk40,sk41,sk42,sk43,sk44,sk45])],[f308_nnf]) ).
cnf(c577,plain,
( sk39(X0,X1,X2,X3) != sk40(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f308_sk]) ).
cnf(c578,plain,
( sk39(X0,X1,X2,X3) != sk41(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f308_sk]) ).
cnf(c579,plain,
( sk40(X0,X1,X2,X3) != sk41(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f308_sk]) ).
fof(f309,axiom,
! [Z,P,C] :
( ( iext(uri_owl_onClass,Z,C)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ~ ? [Y] :
( icext(C,Y)
& iext(P,X,Y) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_exactqcr_object_000) ).
fof(f309_nnf,plain,
! [Z,P,C] :
( ! [X] :
( ( ? [Y] :
( icext(C,Y)
& iext(P,X,Y) )
| icext(Z,X) )
& ( ! [Y] :
( ~ icext(C,Y)
| ~ iext(P,X,Y) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f309]) ).
fof(f309_sk,plain,
! [Z,P,C,X,Y] :
( ( ( ( icext(C,sk46(Z,P,C,X))
& iext(P,X,sk46(Z,P,C,X)) )
| icext(Z,X) )
& ( ~ icext(C,Y)
| ~ iext(P,X,Y)
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk46])],[f309_nnf]) ).
cnf(c596,plain,
( ~ icext(X2,X4)
| ~ iext(X1,X3,X4)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f309_sk]) ).
fof(f311,axiom,
! [Z,P,C] :
( ( iext(uri_owl_onClass,Z,C)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ( ! [Y1,Y2,Y3] :
( ( icext(C,Y3)
& iext(P,X,Y3)
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) )
=> ( Y3 = Y2
| Y3 = Y1 ) )
& ? [Y1,Y2] :
( Y1 != Y2
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_exactqcr_object_002) ).
fof(f311_nnf,plain,
! [Z,P,C] :
( ! [X] :
( ( ? [Y1,Y2,Y3] :
( Y3 != Y2
& Y3 != Y1
& icext(C,Y3)
& iext(P,X,Y3)
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) )
| ! [Y1,Y2] :
( Y1 = Y2
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1) )
| icext(Z,X) )
& ( ( ! [Y1,Y2,Y3] :
( Y3 = Y2
| Y3 = Y1
| ~ icext(C,Y3)
| ~ iext(P,X,Y3)
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1) )
& ? [Y1,Y2] :
( Y1 != Y2
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) ) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f311]) ).
fof(f311_sk,plain,
! [Z,P,C,X,Y1,Y2,Y3] :
( ( ( ( sk54(Z,P,C,X) != sk53(Z,P,C,X)
& sk54(Z,P,C,X) != sk52(Z,P,C,X)
& icext(C,sk54(Z,P,C,X))
& iext(P,X,sk54(Z,P,C,X))
& icext(C,sk53(Z,P,C,X))
& iext(P,X,sk53(Z,P,C,X))
& icext(C,sk52(Z,P,C,X))
& iext(P,X,sk52(Z,P,C,X)) )
| Y1 = Y2
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1)
| icext(Z,X) )
& ( ( ( Y3 = Y2
| Y3 = Y1
| ~ icext(C,Y3)
| ~ iext(P,X,Y3)
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1) )
& sk50(Z,P,C,X) != sk51(Z,P,C,X)
& icext(C,sk51(Z,P,C,X))
& iext(P,X,sk51(Z,P,C,X))
& icext(C,sk50(Z,P,C,X))
& iext(P,X,sk50(Z,P,C,X)) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk50,sk51,sk52,sk53,sk54])],[f311_nnf]) ).
cnf(c611,plain,
( sk50(X0,X1,X2,X3) != sk51(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f311_sk]) ).
fof(f312,axiom,
! [Z,P,C] :
( ( iext(uri_owl_onClass,Z,C)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ( ! [Y1,Y2,Y3,Y4] :
( ( icext(C,Y4)
& iext(P,X,Y4)
& icext(C,Y3)
& iext(P,X,Y3)
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) )
=> ( Y4 = Y3
| Y4 = Y2
| Y4 = Y1 ) )
& ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& icext(C,Y3)
& iext(P,X,Y3)
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_exactqcr_object_003) ).
fof(f312_nnf,plain,
! [Z,P,C] :
( ! [X] :
( ( ? [Y1,Y2,Y3,Y4] :
( Y4 != Y3
& Y4 != Y2
& Y4 != Y1
& icext(C,Y4)
& iext(P,X,Y4)
& icext(C,Y3)
& iext(P,X,Y3)
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) )
| ! [Y1,Y2,Y3] :
( Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ icext(C,Y3)
| ~ iext(P,X,Y3)
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1) )
| icext(Z,X) )
& ( ( ! [Y1,Y2,Y3,Y4] :
( Y4 = Y3
| Y4 = Y2
| Y4 = Y1
| ~ icext(C,Y4)
| ~ iext(P,X,Y4)
| ~ icext(C,Y3)
| ~ iext(P,X,Y3)
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1) )
& ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& icext(C,Y3)
& iext(P,X,Y3)
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) ) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f312]) ).
fof(f312_sk,plain,
! [Z,P,C,X,Y1,Y2,Y3,Y4] :
( ( ( ( sk61(Z,P,C,X) != sk60(Z,P,C,X)
& sk61(Z,P,C,X) != sk59(Z,P,C,X)
& sk61(Z,P,C,X) != sk58(Z,P,C,X)
& icext(C,sk61(Z,P,C,X))
& iext(P,X,sk61(Z,P,C,X))
& icext(C,sk60(Z,P,C,X))
& iext(P,X,sk60(Z,P,C,X))
& icext(C,sk59(Z,P,C,X))
& iext(P,X,sk59(Z,P,C,X))
& icext(C,sk58(Z,P,C,X))
& iext(P,X,sk58(Z,P,C,X)) )
| Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ icext(C,Y3)
| ~ iext(P,X,Y3)
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1)
| icext(Z,X) )
& ( ( ( Y4 = Y3
| Y4 = Y2
| Y4 = Y1
| ~ icext(C,Y4)
| ~ iext(P,X,Y4)
| ~ icext(C,Y3)
| ~ iext(P,X,Y3)
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1) )
& sk56(Z,P,C,X) != sk57(Z,P,C,X)
& sk55(Z,P,C,X) != sk57(Z,P,C,X)
& sk55(Z,P,C,X) != sk56(Z,P,C,X)
& icext(C,sk57(Z,P,C,X))
& iext(P,X,sk57(Z,P,C,X))
& icext(C,sk56(Z,P,C,X))
& iext(P,X,sk56(Z,P,C,X))
& icext(C,sk55(Z,P,C,X))
& iext(P,X,sk55(Z,P,C,X)) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_qualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk55,sk56,sk57,sk58,sk59,sk60,sk61])],[f312_nnf]) ).
cnf(c627,plain,
( sk55(X0,X1,X2,X3) != sk56(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f312_sk]) ).
cnf(c628,plain,
( sk55(X0,X1,X2,X3) != sk57(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f312_sk]) ).
cnf(c629,plain,
( sk56(X0,X1,X2,X3) != sk57(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_qualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f312_sk]) ).
fof(f315,axiom,
! [Z,P] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_maxCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ~ ? [Y] : iext(P,X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_maxcard_000) ).
fof(f315_nnf,plain,
! [Z,P] :
( ! [X] :
( ( ? [Y] : iext(P,X,Y)
| icext(Z,X) )
& ( ! [Y] : ~ iext(P,X,Y)
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_maxCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f315]) ).
fof(f315_sk,plain,
! [Z,P,X,Y] :
( ( ( iext(P,X,sk62(Z,P,X))
| icext(Z,X) )
& ( ~ iext(P,X,Y)
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_maxCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk62])],[f315_nnf]) ).
cnf(c646,plain,
( ~ iext(X1,X2,X3)
| ~ icext(X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_maxCardinality,X0,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f315_sk]) ).
fof(f319,axiom,
! [Z,P,D] :
( ( iext(uri_owl_onDataRange,Z,D)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_maxQualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) )
=> ( ! [X] :
( icext(Z,X)
<=> ~ ? [Y] :
( icext(D,Y)
& iext(P,X,Y)
& lv(Y) ) )
& iodp(P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_maxqcr_data_000) ).
fof(f319_nnf,plain,
! [Z,P,D] :
( ( ! [X] :
( ( ? [Y] :
( icext(D,Y)
& iext(P,X,Y)
& lv(Y) )
| icext(Z,X) )
& ( ! [Y] :
( ~ icext(D,Y)
| ~ iext(P,X,Y)
| ~ lv(Y) )
| ~ icext(Z,X) ) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_maxQualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f319]) ).
fof(f319_sk,plain,
! [Z,P,D,X,Y] :
( ( ( ( icext(D,sk72(Z,P,D,X))
& iext(P,X,sk72(Z,P,D,X))
& lv(sk72(Z,P,D,X)) )
| icext(Z,X) )
& ( ~ icext(D,Y)
| ~ iext(P,X,Y)
| ~ lv(Y)
| ~ icext(Z,X) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_maxQualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk72])],[f319_nnf]) ).
cnf(c667,plain,
( ~ icext(X2,X4)
| ~ iext(X1,X3,X4)
| ~ lv(X4)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_maxQualifiedCardinality,X0,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f319_sk]) ).
fof(f323,axiom,
! [Z,P,C] :
( ( iext(uri_owl_onClass,Z,C)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_maxQualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ~ ? [Y] :
( icext(C,Y)
& iext(P,X,Y) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_maxqcr_object_000) ).
fof(f323_nnf,plain,
! [Z,P,C] :
( ! [X] :
( ( ? [Y] :
( icext(C,Y)
& iext(P,X,Y) )
| icext(Z,X) )
& ( ! [Y] :
( ~ icext(C,Y)
| ~ iext(P,X,Y) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_maxQualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f323]) ).
fof(f323_sk,plain,
! [Z,P,C,X,Y] :
( ( ( ( icext(C,sk82(Z,P,C,X))
& iext(P,X,sk82(Z,P,C,X)) )
| icext(Z,X) )
& ( ~ icext(C,Y)
| ~ iext(P,X,Y)
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_maxQualifiedCardinality,Z,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk82])],[f323_nnf]) ).
cnf(c710,plain,
( ~ icext(X2,X4)
| ~ iext(X1,X3,X4)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_maxQualifiedCardinality,X0,literal_typed(dat_str_0,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f323_sk]) ).
fof(f329,axiom,
! [Z,P] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_minCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ? [Y1,Y2] :
( Y1 != Y2
& iext(P,X,Y2)
& iext(P,X,Y1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_mincard_002) ).
fof(f329_nnf,plain,
! [Z,P] :
( ! [X] :
( ( ! [Y1,Y2] :
( Y1 = Y2
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) )
| icext(Z,X) )
& ( ? [Y1,Y2] :
( Y1 != Y2
& iext(P,X,Y2)
& iext(P,X,Y1) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f329]) ).
fof(f329_sk,plain,
! [Z,P,X,Y1,Y2] :
( ( ( Y1 = Y2
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1)
| icext(Z,X) )
& ( ( sk93(Z,P,X) != sk94(Z,P,X)
& iext(P,X,sk94(Z,P,X))
& iext(P,X,sk93(Z,P,X)) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk93,sk94])],[f329_nnf]) ).
cnf(c745,plain,
( sk93(X0,X1,X2) != sk94(X0,X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minCardinality,X0,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f329_sk]) ).
fof(f330,axiom,
! [Z,P] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_minCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& iext(P,X,Y3)
& iext(P,X,Y2)
& iext(P,X,Y1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_mincard_003) ).
fof(f330_nnf,plain,
! [Z,P] :
( ! [X] :
( ( ! [Y1,Y2,Y3] :
( Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ iext(P,X,Y3)
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1) )
| icext(Z,X) )
& ( ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& iext(P,X,Y3)
& iext(P,X,Y2)
& iext(P,X,Y1) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f330]) ).
fof(f330_sk,plain,
! [Z,P,X,Y1,Y2,Y3] :
( ( ( Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ iext(P,X,Y3)
| ~ iext(P,X,Y2)
| ~ iext(P,X,Y1)
| icext(Z,X) )
& ( ( sk96(Z,P,X) != sk97(Z,P,X)
& sk95(Z,P,X) != sk97(Z,P,X)
& sk95(Z,P,X) != sk96(Z,P,X)
& iext(P,X,sk97(Z,P,X))
& iext(P,X,sk96(Z,P,X))
& iext(P,X,sk95(Z,P,X)) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk95,sk96,sk97])],[f330_nnf]) ).
cnf(c750,plain,
( sk95(X0,X1,X2) != sk96(X0,X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f330_sk]) ).
cnf(c751,plain,
( sk95(X0,X1,X2) != sk97(X0,X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f330_sk]) ).
cnf(c752,plain,
( sk96(X0,X1,X2) != sk97(X0,X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f330_sk]) ).
fof(f333,axiom,
! [Z,P,D] :
( ( iext(uri_owl_onDataRange,Z,D)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) )
=> ( ! [X] :
( icext(Z,X)
<=> ? [Y1,Y2] :
( Y1 != Y2
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) ) )
& iodp(P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_minqcr_data_002) ).
fof(f333_nnf,plain,
! [Z,P,D] :
( ( ! [X] :
( ( ! [Y1,Y2] :
( Y1 = Y2
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1) )
| icext(Z,X) )
& ( ? [Y1,Y2] :
( Y1 != Y2
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) )
| ~ icext(Z,X) ) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f333]) ).
fof(f333_sk,plain,
! [Z,P,D,X,Y1,Y2] :
( ( ( Y1 = Y2
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1)
| icext(Z,X) )
& ( ( sk99(Z,P,D,X) != sk100(Z,P,D,X)
& icext(D,sk100(Z,P,D,X))
& iext(P,X,sk100(Z,P,D,X))
& lv(sk100(Z,P,D,X))
& icext(D,sk99(Z,P,D,X))
& iext(P,X,sk99(Z,P,D,X))
& lv(sk99(Z,P,D,X)) )
| ~ icext(Z,X) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk99,sk100])],[f333_nnf]) ).
cnf(c768,plain,
( sk99(X0,X1,X2,X3) != sk100(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f333_sk]) ).
fof(f334,axiom,
! [Z,P,D] :
( ( iext(uri_owl_onDataRange,Z,D)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) )
=> ( ! [X] :
( icext(Z,X)
<=> ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& icext(D,Y3)
& iext(P,X,Y3)
& lv(Y3)
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) ) )
& iodp(P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_minqcr_data_003) ).
fof(f334_nnf,plain,
! [Z,P,D] :
( ( ! [X] :
( ( ! [Y1,Y2,Y3] :
( Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ icext(D,Y3)
| ~ iext(P,X,Y3)
| ~ lv(Y3)
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1) )
| icext(Z,X) )
& ( ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& icext(D,Y3)
& iext(P,X,Y3)
& lv(Y3)
& icext(D,Y2)
& iext(P,X,Y2)
& lv(Y2)
& icext(D,Y1)
& iext(P,X,Y1)
& lv(Y1) )
| ~ icext(Z,X) ) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f334]) ).
fof(f334_sk,plain,
! [Z,P,D,X,Y1,Y2,Y3] :
( ( ( Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ icext(D,Y3)
| ~ iext(P,X,Y3)
| ~ lv(Y3)
| ~ icext(D,Y2)
| ~ iext(P,X,Y2)
| ~ lv(Y2)
| ~ icext(D,Y1)
| ~ iext(P,X,Y1)
| ~ lv(Y1)
| icext(Z,X) )
& ( ( sk102(Z,P,D,X) != sk103(Z,P,D,X)
& sk101(Z,P,D,X) != sk103(Z,P,D,X)
& sk101(Z,P,D,X) != sk102(Z,P,D,X)
& icext(D,sk103(Z,P,D,X))
& iext(P,X,sk103(Z,P,D,X))
& lv(sk103(Z,P,D,X))
& icext(D,sk102(Z,P,D,X))
& iext(P,X,sk102(Z,P,D,X))
& lv(sk102(Z,P,D,X))
& icext(D,sk101(Z,P,D,X))
& iext(P,X,sk101(Z,P,D,X))
& lv(sk101(Z,P,D,X)) )
| ~ icext(Z,X) )
& iodp(P) )
| ~ iext(uri_owl_onDataRange,Z,D)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk101,sk102,sk103])],[f334_nnf]) ).
cnf(c780,plain,
( sk101(X0,X1,X2,X3) != sk102(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f334_sk]) ).
cnf(c781,plain,
( sk101(X0,X1,X2,X3) != sk103(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f334_sk]) ).
cnf(c782,plain,
( sk102(X0,X1,X2,X3) != sk103(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onDataRange,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f334_sk]) ).
fof(f337,axiom,
! [Z,P,C] :
( ( iext(uri_owl_onClass,Z,C)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ? [Y1,Y2] :
( Y1 != Y2
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_minqcr_object_002) ).
fof(f337_nnf,plain,
! [Z,P,C] :
( ! [X] :
( ( ! [Y1,Y2] :
( Y1 = Y2
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1) )
| icext(Z,X) )
& ( ? [Y1,Y2] :
( Y1 != Y2
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f337]) ).
fof(f337_sk,plain,
! [Z,P,C,X,Y1,Y2] :
( ( ( Y1 = Y2
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1)
| icext(Z,X) )
& ( ( sk105(Z,P,C,X) != sk106(Z,P,C,X)
& icext(C,sk106(Z,P,C,X))
& iext(P,X,sk106(Z,P,C,X))
& icext(C,sk105(Z,P,C,X))
& iext(P,X,sk105(Z,P,C,X)) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk105,sk106])],[f337_nnf]) ).
cnf(c792,plain,
( sk105(X0,X1,X2,X3) != sk106(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f337_sk]) ).
fof(f338,axiom,
! [Z,P,C] :
( ( iext(uri_owl_onClass,Z,C)
& iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) )
=> ! [X] :
( icext(Z,X)
<=> ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& icext(C,Y3)
& iext(P,X,Y3)
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_restrict_minqcr_object_003) ).
fof(f338_nnf,plain,
! [Z,P,C] :
( ! [X] :
( ( ! [Y1,Y2,Y3] :
( Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ icext(C,Y3)
| ~ iext(P,X,Y3)
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1) )
| icext(Z,X) )
& ( ? [Y1,Y2,Y3] :
( Y2 != Y3
& Y1 != Y3
& Y1 != Y2
& icext(C,Y3)
& iext(P,X,Y3)
& icext(C,Y2)
& iext(P,X,Y2)
& icext(C,Y1)
& iext(P,X,Y1) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(nnf_transformation,[status(thm)],[f338]) ).
fof(f338_sk,plain,
! [Z,P,C,X,Y1,Y2,Y3] :
( ( ( Y2 = Y3
| Y1 = Y3
| Y1 = Y2
| ~ icext(C,Y3)
| ~ iext(P,X,Y3)
| ~ icext(C,Y2)
| ~ iext(P,X,Y2)
| ~ icext(C,Y1)
| ~ iext(P,X,Y1)
| icext(Z,X) )
& ( ( sk108(Z,P,C,X) != sk109(Z,P,C,X)
& sk107(Z,P,C,X) != sk109(Z,P,C,X)
& sk107(Z,P,C,X) != sk108(Z,P,C,X)
& icext(C,sk109(Z,P,C,X))
& iext(P,X,sk109(Z,P,C,X))
& icext(C,sk108(Z,P,C,X))
& iext(P,X,sk108(Z,P,C,X))
& icext(C,sk107(Z,P,C,X))
& iext(P,X,sk107(Z,P,C,X)) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onClass,Z,C)
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk107,sk108,sk109])],[f338_nnf]) ).
cnf(c800,plain,
( sk107(X0,X1,X2,X3) != sk108(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f338_sk]) ).
cnf(c801,plain,
( sk107(X0,X1,X2,X3) != sk109(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f338_sk]) ).
cnf(c802,plain,
( sk108(X0,X1,X2,X3) != sk109(X0,X1,X2,X3)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onClass,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_3,uri_xsd_nonNegativeInteger)) ),
inference(cnf_transformation,[status(esa)],[f338_sk]) ).
fof(f344,axiom,
! [X,Y] :
( iext(uri_owl_differentFrom,X,Y)
<=> X != Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_eqdis_differentfrom) ).
fof(f344_nnf,plain,
! [X,Y] :
( ( X = Y
| iext(uri_owl_differentFrom,X,Y) )
& ( X != Y
| ~ iext(uri_owl_differentFrom,X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f344]) ).
fof(f344_sk,plain,
! [X,Y] :
( ( X = Y
| iext(uri_owl_differentFrom,X,Y) )
& ( X != Y
| ~ iext(uri_owl_differentFrom,X,Y) ) ),
inference(skolemisation,[status(esa)],[f344_nnf]) ).
cnf(c827,plain,
( X0 != X1
| ~ iext(uri_owl_differentFrom,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f344_sk]) ).
fof(f345,axiom,
! [C] :
( iext(uri_owl_disjointUnionOf,C,uri_rdf_nil)
<=> ( ! [X] : ~ icext(C,X)
& ic(C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_eqdis_disjointunionof_000) ).
fof(f345_nnf,plain,
! [C] :
( ( ? [X] : icext(C,X)
| ~ ic(C)
| iext(uri_owl_disjointUnionOf,C,uri_rdf_nil) )
& ( ( ! [X] : ~ icext(C,X)
& ic(C) )
| ~ iext(uri_owl_disjointUnionOf,C,uri_rdf_nil) ) ),
inference(nnf_transformation,[status(thm)],[f345]) ).
fof(f345_sk,plain,
! [C,X] :
( ( icext(C,sk118(C))
| ~ ic(C)
| iext(uri_owl_disjointUnionOf,C,uri_rdf_nil) )
& ( ( ~ icext(C,X)
& ic(C) )
| ~ iext(uri_owl_disjointUnionOf,C,uri_rdf_nil) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk118])],[f345_nnf]) ).
cnf(c830,plain,
( ~ icext(X0,X1)
| ~ iext(uri_owl_disjointUnionOf,X0,uri_rdf_nil) ),
inference(cnf_transformation,[status(esa)],[f345_sk]) ).
fof(f347,axiom,
! [C,S1,C1,S2,C2] :
( ( iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_disjointUnionOf,C,S1)
<=> ( ! [X] :
( icext(C,X)
<=> ( ~ ( icext(C2,X)
& icext(C1,X) )
& ( icext(C2,X)
| icext(C1,X) ) ) )
& ic(C2)
& ic(C1)
& ic(C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_eqdis_disjointunionof_002) ).
fof(f347_nnf,plain,
! [C,S1,C1,S2,C2] :
( ( ( ? [X] :
( ( ( ~ icext(C2,X)
| ~ icext(C1,X) )
& ( icext(C2,X)
| icext(C1,X) )
& ~ icext(C,X) )
| ( ( ( icext(C2,X)
& icext(C1,X) )
| ( ~ icext(C2,X)
& ~ icext(C1,X) ) )
& icext(C,X) ) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(C)
| iext(uri_owl_disjointUnionOf,C,S1) )
& ( ( ! [X] :
( ( ( icext(C2,X)
& icext(C1,X) )
| ( ~ icext(C2,X)
& ~ icext(C1,X) )
| icext(C,X) )
& ( ( ( ~ icext(C2,X)
| ~ icext(C1,X) )
& ( icext(C2,X)
| icext(C1,X) ) )
| ~ icext(C,X) ) )
& ic(C2)
& ic(C1)
& ic(C) )
| ~ iext(uri_owl_disjointUnionOf,C,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(nnf_transformation,[status(thm)],[f347]) ).
fof(f347_sk,plain,
! [S1,C1,S2,C2,C,X] :
( ( ( ( ( ~ icext(C2,sk120(C,S1,C1,S2,C2))
| ~ icext(C1,sk120(C,S1,C1,S2,C2)) )
& ( icext(C2,sk120(C,S1,C1,S2,C2))
| icext(C1,sk120(C,S1,C1,S2,C2)) )
& ~ icext(C,sk120(C,S1,C1,S2,C2)) )
| ( ( ( icext(C2,sk120(C,S1,C1,S2,C2))
& icext(C1,sk120(C,S1,C1,S2,C2)) )
| ( ~ icext(C2,sk120(C,S1,C1,S2,C2))
& ~ icext(C1,sk120(C,S1,C1,S2,C2)) ) )
& icext(C,sk120(C,S1,C1,S2,C2)) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(C)
| iext(uri_owl_disjointUnionOf,C,S1) )
& ( ( ( ( icext(C2,X)
& icext(C1,X) )
| ( ~ icext(C2,X)
& ~ icext(C1,X) )
| icext(C,X) )
& ( ( ( ~ icext(C2,X)
| ~ icext(C1,X) )
& ( icext(C2,X)
| icext(C1,X) ) )
| ~ icext(C,X) )
& ic(C2)
& ic(C1)
& ic(C) )
| ~ iext(uri_owl_disjointUnionOf,C,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk120])],[f347_nnf]) ).
cnf(c844,plain,
( ~ icext(X4,X5)
| ~ icext(X2,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_disjointUnionOf,X0,X1)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f347_sk]) ).
fof(f348,axiom,
! [C,S1,C1,S2,C2,S3,C3] :
( ( iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,C3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_disjointUnionOf,C,S1)
<=> ( ! [X] :
( icext(C,X)
<=> ( ~ ( icext(C3,X)
& icext(C2,X) )
& ~ ( icext(C3,X)
& icext(C1,X) )
& ~ ( icext(C2,X)
& icext(C1,X) )
& ( icext(C3,X)
| icext(C2,X)
| icext(C1,X) ) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_eqdis_disjointunionof_003) ).
fof(f348_nnf,plain,
! [C,S1,C1,S2,C2,S3,C3] :
( ( ( ? [X] :
( ( ( ~ icext(C3,X)
| ~ icext(C2,X) )
& ( ~ icext(C3,X)
| ~ icext(C1,X) )
& ( ~ icext(C2,X)
| ~ icext(C1,X) )
& ( icext(C3,X)
| icext(C2,X)
| icext(C1,X) )
& ~ icext(C,X) )
| ( ( ( icext(C3,X)
& icext(C2,X) )
| ( icext(C3,X)
& icext(C1,X) )
| ( icext(C2,X)
& icext(C1,X) )
| ( ~ icext(C3,X)
& ~ icext(C2,X)
& ~ icext(C1,X) ) )
& icext(C,X) ) )
| ~ ic(C3)
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(C)
| iext(uri_owl_disjointUnionOf,C,S1) )
& ( ( ! [X] :
( ( ( icext(C3,X)
& icext(C2,X) )
| ( icext(C3,X)
& icext(C1,X) )
| ( icext(C2,X)
& icext(C1,X) )
| ( ~ icext(C3,X)
& ~ icext(C2,X)
& ~ icext(C1,X) )
| icext(C,X) )
& ( ( ( ~ icext(C3,X)
| ~ icext(C2,X) )
& ( ~ icext(C3,X)
| ~ icext(C1,X) )
& ( ~ icext(C2,X)
| ~ icext(C1,X) )
& ( icext(C3,X)
| icext(C2,X)
| icext(C1,X) ) )
| ~ icext(C,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(C) )
| ~ iext(uri_owl_disjointUnionOf,C,S1) ) )
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,C3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(nnf_transformation,[status(thm)],[f348]) ).
fof(f348_sk,plain,
! [S1,C1,S2,C2,S3,C3,C,X] :
( ( ( ( ( ~ icext(C3,sk121(C,S1,C1,S2,C2,S3,C3))
| ~ icext(C2,sk121(C,S1,C1,S2,C2,S3,C3)) )
& ( ~ icext(C3,sk121(C,S1,C1,S2,C2,S3,C3))
| ~ icext(C1,sk121(C,S1,C1,S2,C2,S3,C3)) )
& ( ~ icext(C2,sk121(C,S1,C1,S2,C2,S3,C3))
| ~ icext(C1,sk121(C,S1,C1,S2,C2,S3,C3)) )
& ( icext(C3,sk121(C,S1,C1,S2,C2,S3,C3))
| icext(C2,sk121(C,S1,C1,S2,C2,S3,C3))
| icext(C1,sk121(C,S1,C1,S2,C2,S3,C3)) )
& ~ icext(C,sk121(C,S1,C1,S2,C2,S3,C3)) )
| ( ( ( icext(C3,sk121(C,S1,C1,S2,C2,S3,C3))
& icext(C2,sk121(C,S1,C1,S2,C2,S3,C3)) )
| ( icext(C3,sk121(C,S1,C1,S2,C2,S3,C3))
& icext(C1,sk121(C,S1,C1,S2,C2,S3,C3)) )
| ( icext(C2,sk121(C,S1,C1,S2,C2,S3,C3))
& icext(C1,sk121(C,S1,C1,S2,C2,S3,C3)) )
| ( ~ icext(C3,sk121(C,S1,C1,S2,C2,S3,C3))
& ~ icext(C2,sk121(C,S1,C1,S2,C2,S3,C3))
& ~ icext(C1,sk121(C,S1,C1,S2,C2,S3,C3)) ) )
& icext(C,sk121(C,S1,C1,S2,C2,S3,C3)) )
| ~ ic(C3)
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(C)
| iext(uri_owl_disjointUnionOf,C,S1) )
& ( ( ( ( icext(C3,X)
& icext(C2,X) )
| ( icext(C3,X)
& icext(C1,X) )
| ( icext(C2,X)
& icext(C1,X) )
| ( ~ icext(C3,X)
& ~ icext(C2,X)
& ~ icext(C1,X) )
| icext(C,X) )
& ( ( ( ~ icext(C3,X)
| ~ icext(C2,X) )
& ( ~ icext(C3,X)
| ~ icext(C1,X) )
& ( ~ icext(C2,X)
| ~ icext(C1,X) )
& ( icext(C3,X)
| icext(C2,X)
| icext(C1,X) ) )
| ~ icext(C,X) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(C) )
| ~ iext(uri_owl_disjointUnionOf,C,S1) ) )
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,C3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk121])],[f348_nnf]) ).
cnf(c869,plain,
( ~ icext(X4,X7)
| ~ icext(X2,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_disjointUnionOf,X0,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f348_sk]) ).
cnf(c870,plain,
( ~ icext(X6,X7)
| ~ icext(X2,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_disjointUnionOf,X0,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f348_sk]) ).
cnf(c871,plain,
( ~ icext(X6,X7)
| ~ icext(X4,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_disjointUnionOf,X0,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f348_sk]) ).
fof(f349,axiom,
! [C1,C2] :
( iext(uri_owl_disjointWith,C1,C2)
<=> ( ! [X] :
~ ( icext(C2,X)
& icext(C1,X) )
& ic(C2)
& ic(C1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_eqdis_disjointwith) ).
fof(f349_nnf,plain,
! [C1,C2] :
( ( ? [X] :
( icext(C2,X)
& icext(C1,X) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_owl_disjointWith,C1,C2) )
& ( ( ! [X] :
( ~ icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_owl_disjointWith,C1,C2) ) ),
inference(nnf_transformation,[status(thm)],[f349]) ).
fof(f349_sk,plain,
! [C1,C2,X] :
( ( ( icext(C2,sk122(C1,C2))
& icext(C1,sk122(C1,C2)) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_owl_disjointWith,C1,C2) )
& ( ( ( ~ icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_owl_disjointWith,C1,C2) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk122])],[f349_nnf]) ).
cnf(c1023,plain,
( ~ icext(X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_disjointWith,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f349_sk]) ).
fof(f352,axiom,
! [P1,P2] :
( iext(uri_owl_propertyDisjointWith,P1,P2)
<=> ( ! [X,Y] :
~ ( iext(P2,X,Y)
& iext(P1,X,Y) )
& ip(P2)
& ip(P1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_eqdis_propertydisjointwith) ).
fof(f352_nnf,plain,
! [P1,P2] :
( ( ? [X,Y] :
( iext(P2,X,Y)
& iext(P1,X,Y) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_propertyDisjointWith,P1,P2) )
& ( ( ! [X,Y] :
( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_propertyDisjointWith,P1,P2) ) ),
inference(nnf_transformation,[status(thm)],[f352]) ).
fof(f352_sk,plain,
! [P1,P2,X,Y] :
( ( ( iext(P2,sk126(P1,P2),sk127(P1,P2))
& iext(P1,sk126(P1,P2),sk127(P1,P2)) )
| ~ ip(P2)
| ~ ip(P1)
| iext(uri_owl_propertyDisjointWith,P1,P2) )
& ( ( ( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_owl_propertyDisjointWith,P1,P2) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk126,sk127])],[f352_nnf]) ).
cnf(c1044,plain,
( ~ iext(X1,X2,X3)
| ~ iext(X0,X2,X3)
| ~ iext(uri_owl_propertyDisjointWith,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f352_sk]) ).
fof(f360,axiom,
! [Z,S1,A1,S2,A2] :
( ( iext(uri_owl_distinctMembers,Z,S1)
& icext(uri_owl_AllDifferent,Z)
& iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,A2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,A1) )
=> A1 != A2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_ndis_alldifferent_distinctmembers_if_002) ).
fof(f360_nnf,plain,
! [Z,S1,A1,S2,A2] :
( A1 != A2
| ~ iext(uri_owl_distinctMembers,Z,S1)
| ~ icext(uri_owl_AllDifferent,Z)
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(nnf_transformation,[status(thm)],[f360]) ).
fof(f360_sk,plain,
! [S1,A1,S2,A2,Z] :
( A1 != A2
| ~ iext(uri_owl_distinctMembers,Z,S1)
| ~ icext(uri_owl_AllDifferent,Z)
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(skolemisation,[status(esa)],[f360_nnf]) ).
cnf(c1059,plain,
( X2 != X4
| ~ iext(uri_owl_distinctMembers,X0,X1)
| ~ icext(uri_owl_AllDifferent,X0)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f360_sk]) ).
fof(f361,axiom,
! [Z,S1,A1,S2,A2,S3,A3] :
( ( iext(uri_owl_distinctMembers,Z,S1)
& icext(uri_owl_AllDifferent,Z)
& iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,A3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,A2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,A1) )
=> ( A2 != A3
& A1 != A3
& A1 != A2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_ndis_alldifferent_distinctmembers_if_003) ).
fof(f361_nnf,plain,
! [Z,S1,A1,S2,A2,S3,A3] :
( ( A2 != A3
& A1 != A3
& A1 != A2 )
| ~ iext(uri_owl_distinctMembers,Z,S1)
| ~ icext(uri_owl_AllDifferent,Z)
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,A3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(nnf_transformation,[status(thm)],[f361]) ).
fof(f361_sk,plain,
! [S1,A1,S2,A2,S3,A3,Z] :
( ( A2 != A3
& A1 != A3
& A1 != A2 )
| ~ iext(uri_owl_distinctMembers,Z,S1)
| ~ icext(uri_owl_AllDifferent,Z)
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,A3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(skolemisation,[status(esa)],[f361_nnf]) ).
cnf(c1060,plain,
( X2 != X4
| ~ iext(uri_owl_distinctMembers,X0,X1)
| ~ icext(uri_owl_AllDifferent,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f361_sk]) ).
cnf(c1061,plain,
( X2 != X6
| ~ iext(uri_owl_distinctMembers,X0,X1)
| ~ icext(uri_owl_AllDifferent,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f361_sk]) ).
cnf(c1062,plain,
( X4 != X6
| ~ iext(uri_owl_distinctMembers,X0,X1)
| ~ icext(uri_owl_AllDifferent,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f361_sk]) ).
fof(f368,axiom,
! [Z,S1,A1,S2,A2] :
( ( iext(uri_owl_members,Z,S1)
& icext(uri_owl_AllDifferent,Z)
& iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,A2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,A1) )
=> A1 != A2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_ndis_alldifferent_members_if_002) ).
fof(f368_nnf,plain,
! [Z,S1,A1,S2,A2] :
( A1 != A2
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDifferent,Z)
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(nnf_transformation,[status(thm)],[f368]) ).
fof(f368_sk,plain,
! [S1,A1,S2,A2,Z] :
( A1 != A2
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDifferent,Z)
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(skolemisation,[status(esa)],[f368_nnf]) ).
cnf(c1073,plain,
( X2 != X4
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDifferent,X0)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f368_sk]) ).
fof(f369,axiom,
! [Z,S1,A1,S2,A2,S3,A3] :
( ( iext(uri_owl_members,Z,S1)
& icext(uri_owl_AllDifferent,Z)
& iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,A3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,A2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,A1) )
=> ( A2 != A3
& A1 != A3
& A1 != A2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_ndis_alldifferent_members_if_003) ).
fof(f369_nnf,plain,
! [Z,S1,A1,S2,A2,S3,A3] :
( ( A2 != A3
& A1 != A3
& A1 != A2 )
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDifferent,Z)
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,A3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(nnf_transformation,[status(thm)],[f369]) ).
fof(f369_sk,plain,
! [S1,A1,S2,A2,S3,A3,Z] :
( ( A2 != A3
& A1 != A3
& A1 != A2 )
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDifferent,Z)
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,A3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(skolemisation,[status(esa)],[f369_nnf]) ).
cnf(c1074,plain,
( X2 != X4
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDifferent,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f369_sk]) ).
cnf(c1075,plain,
( X2 != X6
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDifferent,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f369_sk]) ).
cnf(c1076,plain,
( X4 != X6
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDifferent,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f369_sk]) ).
fof(f376,axiom,
! [Z,S1,C1,S2,C2] :
( ( iext(uri_owl_members,Z,S1)
& icext(uri_owl_AllDisjointClasses,Z)
& iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ! [X] :
~ ( icext(C2,X)
& icext(C1,X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_ndis_alldisjointclasses_if_002) ).
fof(f376_nnf,plain,
! [Z,S1,C1,S2,C2] :
( ! [X] :
( ~ icext(C2,X)
| ~ icext(C1,X) )
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDisjointClasses,Z)
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(nnf_transformation,[status(thm)],[f376]) ).
fof(f376_sk,plain,
! [S1,C1,S2,C2,Z,X] :
( ~ icext(C2,X)
| ~ icext(C1,X)
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDisjointClasses,Z)
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(skolemisation,[status(esa)],[f376_nnf]) ).
cnf(c1103,plain,
( ~ icext(X4,X5)
| ~ icext(X2,X5)
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDisjointClasses,X0)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f376_sk]) ).
fof(f377,axiom,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( iext(uri_owl_members,Z,S1)
& icext(uri_owl_AllDisjointClasses,Z)
& iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,C3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( ! [X] :
~ ( icext(C3,X)
& icext(C2,X) )
& ! [X] :
~ ( icext(C3,X)
& icext(C1,X) )
& ! [X] :
~ ( icext(C2,X)
& icext(C1,X) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_ndis_alldisjointclasses_if_003) ).
fof(f377_nnf,plain,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( ! [X] :
( ~ icext(C3,X)
| ~ icext(C2,X) )
& ! [X] :
( ~ icext(C3,X)
| ~ icext(C1,X) )
& ! [X] :
( ~ icext(C2,X)
| ~ icext(C1,X) ) )
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDisjointClasses,Z)
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,C3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(nnf_transformation,[status(thm)],[f377]) ).
fof(f377_sk,plain,
! [S1,C1,S2,C2,S3,C3,Z,X] :
( ( ( ~ icext(C3,X)
| ~ icext(C2,X) )
& ( ~ icext(C3,X)
| ~ icext(C1,X) )
& ( ~ icext(C2,X)
| ~ icext(C1,X) ) )
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDisjointClasses,Z)
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,C3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(skolemisation,[status(esa)],[f377_nnf]) ).
cnf(c1104,plain,
( ~ icext(X4,X7)
| ~ icext(X2,X7)
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDisjointClasses,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f377_sk]) ).
cnf(c1105,plain,
( ~ icext(X6,X7)
| ~ icext(X2,X7)
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDisjointClasses,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f377_sk]) ).
cnf(c1106,plain,
( ~ icext(X6,X7)
| ~ icext(X4,X7)
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDisjointClasses,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f377_sk]) ).
fof(f384,axiom,
! [Z,S1,P1,S2,P2] :
( ( iext(uri_owl_members,Z,S1)
& icext(uri_owl_AllDisjointProperties,Z)
& iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,P2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,P1) )
=> ! [X,Y] :
~ ( iext(P2,X,Y)
& iext(P1,X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_ndis_alldisjointproperties_if_002) ).
fof(f384_nnf,plain,
! [Z,S1,P1,S2,P2] :
( ! [X,Y] :
( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) )
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDisjointProperties,Z)
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,P2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,P1) ),
inference(nnf_transformation,[status(thm)],[f384]) ).
fof(f384_sk,plain,
! [S1,P1,S2,P2,Z,X,Y] :
( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y)
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDisjointProperties,Z)
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,P2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,P1) ),
inference(skolemisation,[status(esa)],[f384_nnf]) ).
cnf(c1133,plain,
( ~ iext(X4,X5,X6)
| ~ iext(X2,X5,X6)
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDisjointProperties,X0)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f384_sk]) ).
fof(f385,axiom,
! [Z,S1,P1,S2,P2,S3,P3] :
( ( iext(uri_owl_members,Z,S1)
& icext(uri_owl_AllDisjointProperties,Z)
& iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,P3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,P2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,P1) )
=> ( ! [X,Y] :
~ ( iext(P3,X,Y)
& iext(P2,X,Y) )
& ! [X,Y] :
~ ( iext(P3,X,Y)
& iext(P1,X,Y) )
& ! [X,Y] :
~ ( iext(P2,X,Y)
& iext(P1,X,Y) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_ndis_alldisjointproperties_if_003) ).
fof(f385_nnf,plain,
! [Z,S1,P1,S2,P2,S3,P3] :
( ( ! [X,Y] :
( ~ iext(P3,X,Y)
| ~ iext(P2,X,Y) )
& ! [X,Y] :
( ~ iext(P3,X,Y)
| ~ iext(P1,X,Y) )
& ! [X,Y] :
( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) ) )
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDisjointProperties,Z)
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,P3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,P2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,P1) ),
inference(nnf_transformation,[status(thm)],[f385]) ).
fof(f385_sk,plain,
! [S1,P1,S2,P2,S3,P3,Z,X,Y] :
( ( ( ~ iext(P3,X,Y)
| ~ iext(P2,X,Y) )
& ( ~ iext(P3,X,Y)
| ~ iext(P1,X,Y) )
& ( ~ iext(P2,X,Y)
| ~ iext(P1,X,Y) ) )
| ~ iext(uri_owl_members,Z,S1)
| ~ icext(uri_owl_AllDisjointProperties,Z)
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,P3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,P2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,P1) ),
inference(skolemisation,[status(esa)],[f385_nnf]) ).
cnf(c1134,plain,
( ~ iext(X4,X7,X8)
| ~ iext(X2,X7,X8)
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDisjointProperties,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f385_sk]) ).
cnf(c1135,plain,
( ~ iext(X6,X7,X8)
| ~ iext(X2,X7,X8)
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDisjointProperties,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f385_sk]) ).
cnf(c1136,plain,
( ~ iext(X6,X7,X8)
| ~ iext(X4,X7,X8)
| ~ iext(uri_owl_members,X0,X1)
| ~ icext(uri_owl_AllDisjointProperties,X0)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f385_sk]) ).
fof(f391,axiom,
! [P] :
( icext(uri_owl_AsymmetricProperty,P)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> ~ iext(P,Y,X) )
& ip(P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_char_asymmetric) ).
fof(f391_nnf,plain,
! [P] :
( ( ? [X,Y] :
( iext(P,Y,X)
& iext(P,X,Y) )
| ~ ip(P)
| icext(uri_owl_AsymmetricProperty,P) )
& ( ( ! [X,Y] :
( ~ iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_AsymmetricProperty,P) ) ),
inference(nnf_transformation,[status(thm)],[f391]) ).
fof(f391_sk,plain,
! [P,X,Y] :
( ( ( iext(P,sk169(P),sk168(P))
& iext(P,sk168(P),sk169(P)) )
| ~ ip(P)
| icext(uri_owl_AsymmetricProperty,P) )
& ( ( ( ~ iext(P,Y,X)
| ~ iext(P,X,Y) )
& ip(P) )
| ~ icext(uri_owl_AsymmetricProperty,P) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk168,sk169])],[f391_nnf]) ).
cnf(c1170,plain,
( ~ iext(X0,X2,X1)
| ~ iext(X0,X1,X2)
| ~ icext(uri_owl_AsymmetricProperty,X0) ),
inference(cnf_transformation,[status(esa)],[f391_sk]) ).
fof(f394,axiom,
! [P] :
( icext(uri_owl_IrreflexiveReflexiveProperty,P)
<=> ( ! [X] : ~ iext(P,X,X)
& ip(P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_char_irreflexive) ).
fof(f394_nnf,plain,
! [P] :
( ( ? [X] : iext(P,X,X)
| ~ ip(P)
| icext(uri_owl_IrreflexiveReflexiveProperty,P) )
& ( ( ! [X] : ~ iext(P,X,X)
& ip(P) )
| ~ icext(uri_owl_IrreflexiveReflexiveProperty,P) ) ),
inference(nnf_transformation,[status(thm)],[f394]) ).
fof(f394_sk,plain,
! [P,X] :
( ( iext(P,sk176(P),sk176(P))
| ~ ip(P)
| icext(uri_owl_IrreflexiveReflexiveProperty,P) )
& ( ( ~ iext(P,X,X)
& ip(P) )
| ~ icext(uri_owl_IrreflexiveReflexiveProperty,P) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk176])],[f394_nnf]) ).
cnf(c1184,plain,
( ~ iext(X0,X1,X1)
| ~ icext(uri_owl_IrreflexiveReflexiveProperty,X0) ),
inference(cnf_transformation,[status(esa)],[f394_sk]) ).
fof(f403,axiom,
! [Z,P,A,V] :
( ( iext(uri_owl_targetValue,Z,V)
& iext(uri_owl_assertionProperty,Z,P)
& iext(uri_owl_sourceIndividual,Z,A) )
=> ( ~ iext(P,A,V)
& iodp(P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_npa_data_if) ).
fof(f403_nnf,plain,
! [Z,P,A,V] :
( ( ~ iext(P,A,V)
& iodp(P) )
| ~ iext(uri_owl_targetValue,Z,V)
| ~ iext(uri_owl_assertionProperty,Z,P)
| ~ iext(uri_owl_sourceIndividual,Z,A) ),
inference(nnf_transformation,[status(thm)],[f403]) ).
fof(f403_sk,plain,
! [Z,A,P,V] :
( ( ~ iext(P,A,V)
& iodp(P) )
| ~ iext(uri_owl_targetValue,Z,V)
| ~ iext(uri_owl_assertionProperty,Z,P)
| ~ iext(uri_owl_sourceIndividual,Z,A) ),
inference(skolemisation,[status(esa)],[f403_nnf]) ).
cnf(c1240,plain,
( ~ iext(X1,X2,X3)
| ~ iext(uri_owl_targetValue,X0,X3)
| ~ iext(uri_owl_assertionProperty,X0,X1)
| ~ iext(uri_owl_sourceIndividual,X0,X2) ),
inference(cnf_transformation,[status(esa)],[f403_sk]) ).
fof(f405,axiom,
! [Z,P,A1,A2] :
( ( iext(uri_owl_targetIndividual,Z,A2)
& iext(uri_owl_assertionProperty,Z,P)
& iext(uri_owl_sourceIndividual,Z,A1) )
=> ~ iext(P,A1,A2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_npa_object_if) ).
fof(f405_nnf,plain,
! [Z,P,A1,A2] :
( ~ iext(P,A1,A2)
| ~ iext(uri_owl_targetIndividual,Z,A2)
| ~ iext(uri_owl_assertionProperty,Z,P)
| ~ iext(uri_owl_sourceIndividual,Z,A1) ),
inference(nnf_transformation,[status(thm)],[f405]) ).
fof(f405_sk,plain,
! [Z,A1,P,A2] :
( ~ iext(P,A1,A2)
| ~ iext(uri_owl_targetIndividual,Z,A2)
| ~ iext(uri_owl_assertionProperty,Z,P)
| ~ iext(uri_owl_sourceIndividual,Z,A1) ),
inference(skolemisation,[status(esa)],[f405_nnf]) ).
cnf(c1244,plain,
( ~ iext(X1,X2,X3)
| ~ iext(uri_owl_targetIndividual,X0,X3)
| ~ iext(uri_owl_assertionProperty,X0,X1)
| ~ iext(uri_owl_sourceIndividual,X0,X2) ),
inference(cnf_transformation,[status(esa)],[f405_sk]) ).
fof(f472,axiom,
! [X] :
~ ( icext(uri_xsd_base64Binary,X)
& icext(uri_xsd_anyURI,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_anyuri_base64binary) ).
fof(f472_nnf,plain,
! [X] :
( ~ icext(uri_xsd_base64Binary,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(nnf_transformation,[status(thm)],[f472]) ).
fof(f472_sk,plain,
! [X] :
( ~ icext(uri_xsd_base64Binary,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(skolemisation,[status(esa)],[f472_nnf]) ).
cnf(c1311,plain,
( ~ icext(uri_xsd_base64Binary,X0)
| ~ icext(uri_xsd_anyURI,X0) ),
inference(cnf_transformation,[status(esa)],[f472_sk]) ).
fof(f473,axiom,
! [X] :
~ ( icext(uri_xsd_boolean,X)
& icext(uri_xsd_anyURI,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_anyuri_boolean) ).
fof(f473_nnf,plain,
! [X] :
( ~ icext(uri_xsd_boolean,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(nnf_transformation,[status(thm)],[f473]) ).
fof(f473_sk,plain,
! [X] :
( ~ icext(uri_xsd_boolean,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(skolemisation,[status(esa)],[f473_nnf]) ).
cnf(c1312,plain,
( ~ icext(uri_xsd_boolean,X0)
| ~ icext(uri_xsd_anyURI,X0) ),
inference(cnf_transformation,[status(esa)],[f473_sk]) ).
fof(f474,axiom,
! [X] :
~ ( icext(uri_xsd_dateTime,X)
& icext(uri_xsd_anyURI,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_anyuri_datetime) ).
fof(f474_nnf,plain,
! [X] :
( ~ icext(uri_xsd_dateTime,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(nnf_transformation,[status(thm)],[f474]) ).
fof(f474_sk,plain,
! [X] :
( ~ icext(uri_xsd_dateTime,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(skolemisation,[status(esa)],[f474_nnf]) ).
cnf(c1313,plain,
( ~ icext(uri_xsd_dateTime,X0)
| ~ icext(uri_xsd_anyURI,X0) ),
inference(cnf_transformation,[status(esa)],[f474_sk]) ).
fof(f475,axiom,
! [X] :
~ ( icext(uri_xsd_double,X)
& icext(uri_xsd_anyURI,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_anyuri_double) ).
fof(f475_nnf,plain,
! [X] :
( ~ icext(uri_xsd_double,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(nnf_transformation,[status(thm)],[f475]) ).
fof(f475_sk,plain,
! [X] :
( ~ icext(uri_xsd_double,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(skolemisation,[status(esa)],[f475_nnf]) ).
cnf(c1314,plain,
( ~ icext(uri_xsd_double,X0)
| ~ icext(uri_xsd_anyURI,X0) ),
inference(cnf_transformation,[status(esa)],[f475_sk]) ).
fof(f476,axiom,
! [X] :
~ ( icext(uri_xsd_float,X)
& icext(uri_xsd_anyURI,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_anyuri_float) ).
fof(f476_nnf,plain,
! [X] :
( ~ icext(uri_xsd_float,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(nnf_transformation,[status(thm)],[f476]) ).
fof(f476_sk,plain,
! [X] :
( ~ icext(uri_xsd_float,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(skolemisation,[status(esa)],[f476_nnf]) ).
cnf(c1315,plain,
( ~ icext(uri_xsd_float,X0)
| ~ icext(uri_xsd_anyURI,X0) ),
inference(cnf_transformation,[status(esa)],[f476_sk]) ).
fof(f477,axiom,
! [X] :
~ ( icext(uri_xsd_hexBinary,X)
& icext(uri_xsd_anyURI,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_anyuri_hexbinary) ).
fof(f477_nnf,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(nnf_transformation,[status(thm)],[f477]) ).
fof(f477_sk,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(skolemisation,[status(esa)],[f477_nnf]) ).
cnf(c1316,plain,
( ~ icext(uri_xsd_hexBinary,X0)
| ~ icext(uri_xsd_anyURI,X0) ),
inference(cnf_transformation,[status(esa)],[f477_sk]) ).
fof(f478,axiom,
! [X] :
~ ( icext(uri_rdf_PlainLiteral,X)
& icext(uri_xsd_anyURI,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_anyuri_plainliteral) ).
fof(f478_nnf,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(nnf_transformation,[status(thm)],[f478]) ).
fof(f478_sk,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(skolemisation,[status(esa)],[f478_nnf]) ).
cnf(c1317,plain,
( ~ icext(uri_rdf_PlainLiteral,X0)
| ~ icext(uri_xsd_anyURI,X0) ),
inference(cnf_transformation,[status(esa)],[f478_sk]) ).
fof(f479,axiom,
! [X] :
~ ( icext(uri_owl_real,X)
& icext(uri_xsd_anyURI,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_anyuri_real) ).
fof(f479_nnf,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(nnf_transformation,[status(thm)],[f479]) ).
fof(f479_sk,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(skolemisation,[status(esa)],[f479_nnf]) ).
cnf(c1318,plain,
( ~ icext(uri_owl_real,X0)
| ~ icext(uri_xsd_anyURI,X0) ),
inference(cnf_transformation,[status(esa)],[f479_sk]) ).
fof(f480,axiom,
! [X] :
~ ( icext(uri_rdf_XMLLiteral,X)
& icext(uri_xsd_anyURI,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_anyuri_xmlliteral) ).
fof(f480_nnf,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(nnf_transformation,[status(thm)],[f480]) ).
fof(f480_sk,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_anyURI,X) ),
inference(skolemisation,[status(esa)],[f480_nnf]) ).
cnf(c1319,plain,
( ~ icext(uri_rdf_XMLLiteral,X0)
| ~ icext(uri_xsd_anyURI,X0) ),
inference(cnf_transformation,[status(esa)],[f480_sk]) ).
fof(f481,axiom,
! [X] :
~ ( icext(uri_xsd_boolean,X)
& icext(uri_xsd_base64Binary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_base64binary_boolean) ).
fof(f481_nnf,plain,
! [X] :
( ~ icext(uri_xsd_boolean,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(nnf_transformation,[status(thm)],[f481]) ).
fof(f481_sk,plain,
! [X] :
( ~ icext(uri_xsd_boolean,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(skolemisation,[status(esa)],[f481_nnf]) ).
cnf(c1320,plain,
( ~ icext(uri_xsd_boolean,X0)
| ~ icext(uri_xsd_base64Binary,X0) ),
inference(cnf_transformation,[status(esa)],[f481_sk]) ).
fof(f482,axiom,
! [X] :
~ ( icext(uri_xsd_dateTime,X)
& icext(uri_xsd_base64Binary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_base64binary_datetime) ).
fof(f482_nnf,plain,
! [X] :
( ~ icext(uri_xsd_dateTime,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(nnf_transformation,[status(thm)],[f482]) ).
fof(f482_sk,plain,
! [X] :
( ~ icext(uri_xsd_dateTime,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(skolemisation,[status(esa)],[f482_nnf]) ).
cnf(c1321,plain,
( ~ icext(uri_xsd_dateTime,X0)
| ~ icext(uri_xsd_base64Binary,X0) ),
inference(cnf_transformation,[status(esa)],[f482_sk]) ).
fof(f483,axiom,
! [X] :
~ ( icext(uri_xsd_double,X)
& icext(uri_xsd_base64Binary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_base64binary_double) ).
fof(f483_nnf,plain,
! [X] :
( ~ icext(uri_xsd_double,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(nnf_transformation,[status(thm)],[f483]) ).
fof(f483_sk,plain,
! [X] :
( ~ icext(uri_xsd_double,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(skolemisation,[status(esa)],[f483_nnf]) ).
cnf(c1322,plain,
( ~ icext(uri_xsd_double,X0)
| ~ icext(uri_xsd_base64Binary,X0) ),
inference(cnf_transformation,[status(esa)],[f483_sk]) ).
fof(f484,axiom,
! [X] :
~ ( icext(uri_xsd_float,X)
& icext(uri_xsd_base64Binary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_base64binary_float) ).
fof(f484_nnf,plain,
! [X] :
( ~ icext(uri_xsd_float,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(nnf_transformation,[status(thm)],[f484]) ).
fof(f484_sk,plain,
! [X] :
( ~ icext(uri_xsd_float,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(skolemisation,[status(esa)],[f484_nnf]) ).
cnf(c1323,plain,
( ~ icext(uri_xsd_float,X0)
| ~ icext(uri_xsd_base64Binary,X0) ),
inference(cnf_transformation,[status(esa)],[f484_sk]) ).
fof(f485,axiom,
! [X] :
~ ( icext(uri_xsd_hexBinary,X)
& icext(uri_xsd_base64Binary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_base64binary_hexbinary) ).
fof(f485_nnf,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(nnf_transformation,[status(thm)],[f485]) ).
fof(f485_sk,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(skolemisation,[status(esa)],[f485_nnf]) ).
cnf(c1324,plain,
( ~ icext(uri_xsd_hexBinary,X0)
| ~ icext(uri_xsd_base64Binary,X0) ),
inference(cnf_transformation,[status(esa)],[f485_sk]) ).
fof(f486,axiom,
! [X] :
~ ( icext(uri_rdf_PlainLiteral,X)
& icext(uri_xsd_base64Binary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_base64binary_plainliteral) ).
fof(f486_nnf,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(nnf_transformation,[status(thm)],[f486]) ).
fof(f486_sk,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(skolemisation,[status(esa)],[f486_nnf]) ).
cnf(c1325,plain,
( ~ icext(uri_rdf_PlainLiteral,X0)
| ~ icext(uri_xsd_base64Binary,X0) ),
inference(cnf_transformation,[status(esa)],[f486_sk]) ).
fof(f487,axiom,
! [X] :
~ ( icext(uri_owl_real,X)
& icext(uri_xsd_base64Binary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_base64binary_real) ).
fof(f487_nnf,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(nnf_transformation,[status(thm)],[f487]) ).
fof(f487_sk,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(skolemisation,[status(esa)],[f487_nnf]) ).
cnf(c1326,plain,
( ~ icext(uri_owl_real,X0)
| ~ icext(uri_xsd_base64Binary,X0) ),
inference(cnf_transformation,[status(esa)],[f487_sk]) ).
fof(f488,axiom,
! [X] :
~ ( icext(uri_rdf_XMLLiteral,X)
& icext(uri_xsd_base64Binary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_base64binary_xmlliteral) ).
fof(f488_nnf,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(nnf_transformation,[status(thm)],[f488]) ).
fof(f488_sk,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_base64Binary,X) ),
inference(skolemisation,[status(esa)],[f488_nnf]) ).
cnf(c1327,plain,
( ~ icext(uri_rdf_XMLLiteral,X0)
| ~ icext(uri_xsd_base64Binary,X0) ),
inference(cnf_transformation,[status(esa)],[f488_sk]) ).
fof(f489,axiom,
! [X] :
~ ( icext(uri_xsd_dateTime,X)
& icext(uri_xsd_boolean,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_boolean_datetime) ).
fof(f489_nnf,plain,
! [X] :
( ~ icext(uri_xsd_dateTime,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(nnf_transformation,[status(thm)],[f489]) ).
fof(f489_sk,plain,
! [X] :
( ~ icext(uri_xsd_dateTime,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(skolemisation,[status(esa)],[f489_nnf]) ).
cnf(c1328,plain,
( ~ icext(uri_xsd_dateTime,X0)
| ~ icext(uri_xsd_boolean,X0) ),
inference(cnf_transformation,[status(esa)],[f489_sk]) ).
fof(f490,axiom,
! [X] :
~ ( icext(uri_xsd_double,X)
& icext(uri_xsd_boolean,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_boolean_double) ).
fof(f490_nnf,plain,
! [X] :
( ~ icext(uri_xsd_double,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(nnf_transformation,[status(thm)],[f490]) ).
fof(f490_sk,plain,
! [X] :
( ~ icext(uri_xsd_double,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(skolemisation,[status(esa)],[f490_nnf]) ).
cnf(c1329,plain,
( ~ icext(uri_xsd_double,X0)
| ~ icext(uri_xsd_boolean,X0) ),
inference(cnf_transformation,[status(esa)],[f490_sk]) ).
fof(f491,axiom,
! [X] :
~ ( icext(uri_xsd_float,X)
& icext(uri_xsd_boolean,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_boolean_float) ).
fof(f491_nnf,plain,
! [X] :
( ~ icext(uri_xsd_float,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(nnf_transformation,[status(thm)],[f491]) ).
fof(f491_sk,plain,
! [X] :
( ~ icext(uri_xsd_float,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(skolemisation,[status(esa)],[f491_nnf]) ).
cnf(c1330,plain,
( ~ icext(uri_xsd_float,X0)
| ~ icext(uri_xsd_boolean,X0) ),
inference(cnf_transformation,[status(esa)],[f491_sk]) ).
fof(f492,axiom,
! [X] :
~ ( icext(uri_xsd_hexBinary,X)
& icext(uri_xsd_boolean,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_boolean_hexbinary) ).
fof(f492_nnf,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(nnf_transformation,[status(thm)],[f492]) ).
fof(f492_sk,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(skolemisation,[status(esa)],[f492_nnf]) ).
cnf(c1331,plain,
( ~ icext(uri_xsd_hexBinary,X0)
| ~ icext(uri_xsd_boolean,X0) ),
inference(cnf_transformation,[status(esa)],[f492_sk]) ).
fof(f493,axiom,
! [X] :
~ ( icext(uri_rdf_PlainLiteral,X)
& icext(uri_xsd_boolean,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_boolean_plainliteral) ).
fof(f493_nnf,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(nnf_transformation,[status(thm)],[f493]) ).
fof(f493_sk,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(skolemisation,[status(esa)],[f493_nnf]) ).
cnf(c1332,plain,
( ~ icext(uri_rdf_PlainLiteral,X0)
| ~ icext(uri_xsd_boolean,X0) ),
inference(cnf_transformation,[status(esa)],[f493_sk]) ).
fof(f494,axiom,
! [X] :
~ ( icext(uri_owl_real,X)
& icext(uri_xsd_boolean,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_boolean_real) ).
fof(f494_nnf,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(nnf_transformation,[status(thm)],[f494]) ).
fof(f494_sk,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(skolemisation,[status(esa)],[f494_nnf]) ).
cnf(c1333,plain,
( ~ icext(uri_owl_real,X0)
| ~ icext(uri_xsd_boolean,X0) ),
inference(cnf_transformation,[status(esa)],[f494_sk]) ).
fof(f495,axiom,
! [X] :
~ ( icext(uri_rdf_XMLLiteral,X)
& icext(uri_xsd_boolean,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_boolean_xmlliteral) ).
fof(f495_nnf,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(nnf_transformation,[status(thm)],[f495]) ).
fof(f495_sk,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_boolean,X) ),
inference(skolemisation,[status(esa)],[f495_nnf]) ).
cnf(c1334,plain,
( ~ icext(uri_rdf_XMLLiteral,X0)
| ~ icext(uri_xsd_boolean,X0) ),
inference(cnf_transformation,[status(esa)],[f495_sk]) ).
fof(f496,axiom,
! [X] :
~ ( icext(uri_xsd_double,X)
& icext(uri_xsd_dateTime,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_datetime_double) ).
fof(f496_nnf,plain,
! [X] :
( ~ icext(uri_xsd_double,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(nnf_transformation,[status(thm)],[f496]) ).
fof(f496_sk,plain,
! [X] :
( ~ icext(uri_xsd_double,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(skolemisation,[status(esa)],[f496_nnf]) ).
cnf(c1335,plain,
( ~ icext(uri_xsd_double,X0)
| ~ icext(uri_xsd_dateTime,X0) ),
inference(cnf_transformation,[status(esa)],[f496_sk]) ).
fof(f497,axiom,
! [X] :
~ ( icext(uri_xsd_float,X)
& icext(uri_xsd_dateTime,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_datetime_float) ).
fof(f497_nnf,plain,
! [X] :
( ~ icext(uri_xsd_float,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(nnf_transformation,[status(thm)],[f497]) ).
fof(f497_sk,plain,
! [X] :
( ~ icext(uri_xsd_float,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(skolemisation,[status(esa)],[f497_nnf]) ).
cnf(c1336,plain,
( ~ icext(uri_xsd_float,X0)
| ~ icext(uri_xsd_dateTime,X0) ),
inference(cnf_transformation,[status(esa)],[f497_sk]) ).
fof(f498,axiom,
! [X] :
~ ( icext(uri_xsd_hexBinary,X)
& icext(uri_xsd_dateTime,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_datetime_hexbinary) ).
fof(f498_nnf,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(nnf_transformation,[status(thm)],[f498]) ).
fof(f498_sk,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(skolemisation,[status(esa)],[f498_nnf]) ).
cnf(c1337,plain,
( ~ icext(uri_xsd_hexBinary,X0)
| ~ icext(uri_xsd_dateTime,X0) ),
inference(cnf_transformation,[status(esa)],[f498_sk]) ).
fof(f499,axiom,
! [X] :
~ ( icext(uri_rdf_PlainLiteral,X)
& icext(uri_xsd_dateTime,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_datetime_plainliteral) ).
fof(f499_nnf,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(nnf_transformation,[status(thm)],[f499]) ).
fof(f499_sk,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(skolemisation,[status(esa)],[f499_nnf]) ).
cnf(c1338,plain,
( ~ icext(uri_rdf_PlainLiteral,X0)
| ~ icext(uri_xsd_dateTime,X0) ),
inference(cnf_transformation,[status(esa)],[f499_sk]) ).
fof(f500,axiom,
! [X] :
~ ( icext(uri_owl_real,X)
& icext(uri_xsd_dateTime,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_datetime_real) ).
fof(f500_nnf,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(nnf_transformation,[status(thm)],[f500]) ).
fof(f500_sk,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(skolemisation,[status(esa)],[f500_nnf]) ).
cnf(c1339,plain,
( ~ icext(uri_owl_real,X0)
| ~ icext(uri_xsd_dateTime,X0) ),
inference(cnf_transformation,[status(esa)],[f500_sk]) ).
fof(f501,axiom,
! [X] :
~ ( icext(uri_rdf_XMLLiteral,X)
& icext(uri_xsd_dateTime,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_datetime_xmlliteral) ).
fof(f501_nnf,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(nnf_transformation,[status(thm)],[f501]) ).
fof(f501_sk,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_dateTime,X) ),
inference(skolemisation,[status(esa)],[f501_nnf]) ).
cnf(c1340,plain,
( ~ icext(uri_rdf_XMLLiteral,X0)
| ~ icext(uri_xsd_dateTime,X0) ),
inference(cnf_transformation,[status(esa)],[f501_sk]) ).
fof(f502,axiom,
! [X] :
~ ( icext(uri_xsd_float,X)
& icext(uri_xsd_double,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_double_float) ).
fof(f502_nnf,plain,
! [X] :
( ~ icext(uri_xsd_float,X)
| ~ icext(uri_xsd_double,X) ),
inference(nnf_transformation,[status(thm)],[f502]) ).
fof(f502_sk,plain,
! [X] :
( ~ icext(uri_xsd_float,X)
| ~ icext(uri_xsd_double,X) ),
inference(skolemisation,[status(esa)],[f502_nnf]) ).
cnf(c1341,plain,
( ~ icext(uri_xsd_float,X0)
| ~ icext(uri_xsd_double,X0) ),
inference(cnf_transformation,[status(esa)],[f502_sk]) ).
fof(f503,axiom,
! [X] :
~ ( icext(uri_xsd_hexBinary,X)
& icext(uri_xsd_double,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_double_hexbinary) ).
fof(f503_nnf,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_double,X) ),
inference(nnf_transformation,[status(thm)],[f503]) ).
fof(f503_sk,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_double,X) ),
inference(skolemisation,[status(esa)],[f503_nnf]) ).
cnf(c1342,plain,
( ~ icext(uri_xsd_hexBinary,X0)
| ~ icext(uri_xsd_double,X0) ),
inference(cnf_transformation,[status(esa)],[f503_sk]) ).
fof(f504,axiom,
! [X] :
~ ( icext(uri_rdf_PlainLiteral,X)
& icext(uri_xsd_double,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_double_plainliteral) ).
fof(f504_nnf,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_double,X) ),
inference(nnf_transformation,[status(thm)],[f504]) ).
fof(f504_sk,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_double,X) ),
inference(skolemisation,[status(esa)],[f504_nnf]) ).
cnf(c1343,plain,
( ~ icext(uri_rdf_PlainLiteral,X0)
| ~ icext(uri_xsd_double,X0) ),
inference(cnf_transformation,[status(esa)],[f504_sk]) ).
fof(f505,axiom,
! [X] :
~ ( icext(uri_owl_real,X)
& icext(uri_xsd_double,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_double_real) ).
fof(f505_nnf,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_double,X) ),
inference(nnf_transformation,[status(thm)],[f505]) ).
fof(f505_sk,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_double,X) ),
inference(skolemisation,[status(esa)],[f505_nnf]) ).
cnf(c1344,plain,
( ~ icext(uri_owl_real,X0)
| ~ icext(uri_xsd_double,X0) ),
inference(cnf_transformation,[status(esa)],[f505_sk]) ).
fof(f506,axiom,
! [X] :
~ ( icext(uri_rdf_XMLLiteral,X)
& icext(uri_xsd_double,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_double_xmlliteral) ).
fof(f506_nnf,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_double,X) ),
inference(nnf_transformation,[status(thm)],[f506]) ).
fof(f506_sk,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_double,X) ),
inference(skolemisation,[status(esa)],[f506_nnf]) ).
cnf(c1345,plain,
( ~ icext(uri_rdf_XMLLiteral,X0)
| ~ icext(uri_xsd_double,X0) ),
inference(cnf_transformation,[status(esa)],[f506_sk]) ).
fof(f507,axiom,
! [X] :
~ ( icext(uri_xsd_hexBinary,X)
& icext(uri_xsd_float,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_float_hexbinary) ).
fof(f507_nnf,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_float,X) ),
inference(nnf_transformation,[status(thm)],[f507]) ).
fof(f507_sk,plain,
! [X] :
( ~ icext(uri_xsd_hexBinary,X)
| ~ icext(uri_xsd_float,X) ),
inference(skolemisation,[status(esa)],[f507_nnf]) ).
cnf(c1346,plain,
( ~ icext(uri_xsd_hexBinary,X0)
| ~ icext(uri_xsd_float,X0) ),
inference(cnf_transformation,[status(esa)],[f507_sk]) ).
fof(f508,axiom,
! [X] :
~ ( icext(uri_rdf_PlainLiteral,X)
& icext(uri_xsd_float,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_float_plainliteral) ).
fof(f508_nnf,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_float,X) ),
inference(nnf_transformation,[status(thm)],[f508]) ).
fof(f508_sk,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_float,X) ),
inference(skolemisation,[status(esa)],[f508_nnf]) ).
cnf(c1347,plain,
( ~ icext(uri_rdf_PlainLiteral,X0)
| ~ icext(uri_xsd_float,X0) ),
inference(cnf_transformation,[status(esa)],[f508_sk]) ).
fof(f509,axiom,
! [X] :
~ ( icext(uri_owl_real,X)
& icext(uri_xsd_float,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_float_real) ).
fof(f509_nnf,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_float,X) ),
inference(nnf_transformation,[status(thm)],[f509]) ).
fof(f509_sk,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_float,X) ),
inference(skolemisation,[status(esa)],[f509_nnf]) ).
cnf(c1348,plain,
( ~ icext(uri_owl_real,X0)
| ~ icext(uri_xsd_float,X0) ),
inference(cnf_transformation,[status(esa)],[f509_sk]) ).
fof(f510,axiom,
! [X] :
~ ( icext(uri_rdf_XMLLiteral,X)
& icext(uri_xsd_float,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_float_xmlliteral) ).
fof(f510_nnf,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_float,X) ),
inference(nnf_transformation,[status(thm)],[f510]) ).
fof(f510_sk,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_float,X) ),
inference(skolemisation,[status(esa)],[f510_nnf]) ).
cnf(c1349,plain,
( ~ icext(uri_rdf_XMLLiteral,X0)
| ~ icext(uri_xsd_float,X0) ),
inference(cnf_transformation,[status(esa)],[f510_sk]) ).
fof(f511,axiom,
! [X] :
~ ( icext(uri_rdf_PlainLiteral,X)
& icext(uri_xsd_hexBinary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_hexbinary_plainliteral) ).
fof(f511_nnf,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_hexBinary,X) ),
inference(nnf_transformation,[status(thm)],[f511]) ).
fof(f511_sk,plain,
! [X] :
( ~ icext(uri_rdf_PlainLiteral,X)
| ~ icext(uri_xsd_hexBinary,X) ),
inference(skolemisation,[status(esa)],[f511_nnf]) ).
cnf(c1350,plain,
( ~ icext(uri_rdf_PlainLiteral,X0)
| ~ icext(uri_xsd_hexBinary,X0) ),
inference(cnf_transformation,[status(esa)],[f511_sk]) ).
fof(f512,axiom,
! [X] :
~ ( icext(uri_owl_real,X)
& icext(uri_xsd_hexBinary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_hexbinary_real) ).
fof(f512_nnf,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_hexBinary,X) ),
inference(nnf_transformation,[status(thm)],[f512]) ).
fof(f512_sk,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_xsd_hexBinary,X) ),
inference(skolemisation,[status(esa)],[f512_nnf]) ).
cnf(c1351,plain,
( ~ icext(uri_owl_real,X0)
| ~ icext(uri_xsd_hexBinary,X0) ),
inference(cnf_transformation,[status(esa)],[f512_sk]) ).
fof(f513,axiom,
! [X] :
~ ( icext(uri_rdf_XMLLiteral,X)
& icext(uri_xsd_hexBinary,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_hexbinary_xmlliteral) ).
fof(f513_nnf,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_hexBinary,X) ),
inference(nnf_transformation,[status(thm)],[f513]) ).
fof(f513_sk,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_xsd_hexBinary,X) ),
inference(skolemisation,[status(esa)],[f513_nnf]) ).
cnf(c1352,plain,
( ~ icext(uri_rdf_XMLLiteral,X0)
| ~ icext(uri_xsd_hexBinary,X0) ),
inference(cnf_transformation,[status(esa)],[f513_sk]) ).
fof(f514,axiom,
! [X] :
~ ( icext(uri_owl_real,X)
& icext(uri_rdf_PlainLiteral,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_plainliteral_real) ).
fof(f514_nnf,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_rdf_PlainLiteral,X) ),
inference(nnf_transformation,[status(thm)],[f514]) ).
fof(f514_sk,plain,
! [X] :
( ~ icext(uri_owl_real,X)
| ~ icext(uri_rdf_PlainLiteral,X) ),
inference(skolemisation,[status(esa)],[f514_nnf]) ).
cnf(c1353,plain,
( ~ icext(uri_owl_real,X0)
| ~ icext(uri_rdf_PlainLiteral,X0) ),
inference(cnf_transformation,[status(esa)],[f514_sk]) ).
fof(f515,axiom,
! [X] :
~ ( icext(uri_rdf_XMLLiteral,X)
& icext(uri_rdf_PlainLiteral,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_plainliteral_xmlliteral) ).
fof(f515_nnf,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_rdf_PlainLiteral,X) ),
inference(nnf_transformation,[status(thm)],[f515]) ).
fof(f515_sk,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_rdf_PlainLiteral,X) ),
inference(skolemisation,[status(esa)],[f515_nnf]) ).
cnf(c1354,plain,
( ~ icext(uri_rdf_XMLLiteral,X0)
| ~ icext(uri_rdf_PlainLiteral,X0) ),
inference(cnf_transformation,[status(esa)],[f515_sk]) ).
fof(f516,axiom,
! [X] :
~ ( icext(uri_rdf_XMLLiteral,X)
& icext(uri_owl_real,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_dat_dtype_relation_disjoint_real_xmlliteral) ).
fof(f516_nnf,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_owl_real,X) ),
inference(nnf_transformation,[status(thm)],[f516]) ).
fof(f516_sk,plain,
! [X] :
( ~ icext(uri_rdf_XMLLiteral,X)
| ~ icext(uri_owl_real,X) ),
inference(skolemisation,[status(esa)],[f516_nnf]) ).
cnf(c1355,plain,
( ~ icext(uri_rdf_XMLLiteral,X0)
| ~ icext(uri_owl_real,X0) ),
inference(cnf_transformation,[status(esa)],[f516_sk]) ).
fof(f558,conjecture,
iext(uri_rdf_type,uri_ex_w,uri_ex_B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',testcase_conclusion_fullish_029_Ex_Falso_Quodlibet) ).
fof(f558_neg,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_w,uri_ex_B),
inference(negated_conjecture,[status(cth)],[f558]) ).
fof(f558_nnf,plain,
~ iext(uri_rdf_type,uri_ex_w,uri_ex_B),
inference(nnf_transformation,[status(thm)],[f558_neg]) ).
fof(f558_sk,plain,
~ iext(uri_rdf_type,uri_ex_w,uri_ex_B),
inference(skolemisation,[status(esa)],[f558_nnf]) ).
cnf(c1406,plain,
~ iext(uri_rdf_type,uri_ex_w,uri_ex_B),
inference(cnf_transformation,[status(esa)],[f558_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c173,c220,c222,c368,c371,c420,c462,c500,c509,c519,c520,c521,c531,c554,c577,c578,c579,c596,c611,c627,c628,c629,c646,c667,c710,c745,c750,c751,c752,c768,c780,c781,c782,c792,c800,c801,c802,c827,c830,c844,c869,c870,c871,c1023,c1044,c1059,c1060,c1061,c1062,c1073,c1074,c1075,c1076,c1103,c1104,c1105,c1106,c1133,c1134,c1135,c1136,c1170,c1184,c1240,c1244,c1311,c1312,c1313,c1314,c1315,c1316,c1317,c1318,c1319,c1320,c1321,c1322,c1323,c1324,c1325,c1326,c1327,c1328,c1329,c1330,c1331,c1332,c1333,c1334,c1335,c1336,c1337,c1338,c1339,c1340,c1341,c1342,c1343,c1344,c1345,c1346,c1347,c1348,c1349,c1350,c1351,c1352,c1353,c1354,c1355,c1406]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2264]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB029+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n020.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Thu Sep 24 15:37:03 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 39.48/5.52 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 39.48/5.52 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------