%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB012+3 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:37:04 PM UTC 2026
% Result : Theorem 25.37s 3.93s
% Output : CNFRefutation 27.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 9
% Syntax : Number of formulae : 90 ( 13 unt; 1 def)
% Number of atoms : 472 ( 0 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 635 ( 253 ~; 238 |; 125 &)
% ( 14 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-4 aty)
% Number of functors : 27 ( 27 usr; 22 con; 0-5 aty)
% Number of variables : 290 ( 274 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [Z,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_intersectionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C3,X)
& icext(C2,X)
& icext(C1,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [P,C] :
( iext(uri_rdfs_domain,P,C)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> icext(C,X) )
& ic(C)
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [C1,C2] :
( iext(uri_rdfs_subClassOf,C1,C2)
<=> ( ! [X] :
( icext(C1,X)
=> icext(C2,X) )
& ic(C2)
& ic(C1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [Z,P,A] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_hasValue,Z,A) )
=> ! [X] :
( icext(Z,X)
<=> iext(P,X,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,axiom,
! [C] :
( ic(C)
=> iext(uri_rdfs_subClassOf,C,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f139,conjecture,
( iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)
& iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,negated_conjecture,
~ ( iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)
& iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty) ),
inference(negated_conjecture,[status(cth)],[f139]) ).
fof(f141,axiom,
? [BNODE_l1,BNODE_l2,BNODE_l3,BNODE_r] :
( iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))
& iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute)
& iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person)
& iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain)
& iext(uri_rdf_type,BNODE_r,uri_owl_Restriction)
& iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l3,BNODE_r)
& iext(uri_rdf_rest,BNODE_l2,BNODE_l3)
& iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty)
& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty)
& iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1)
& iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,plain,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( iext(uri_owl_intersectionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C3,X)
& icext(C2,X)
& icext(C1,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(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(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f181,definition,
! [C1,C2,C3,X] :
( sP0_prd(X,C3,C2,C1)
<=> ( icext(C3,X)
& icext(C2,X)
& icext(C1,X) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f182,plain,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( iext(uri_owl_intersectionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> sP0_prd(X,C3,C2,C1) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(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(formula_renaming,[status(thm)],[f180,f181]) ).
fof(f183,plain,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( ( ? [X] :
( ( sP0_prd(X,C3,C2,C1)
| icext(Z,X) )
& ( ~ sP0_prd(X,C3,C2,C1)
| ~ icext(Z,X) ) )
| ~ ic(C3)
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_intersectionOf,Z,S1) )
& ( ( ! [X] :
( ( ~ sP0_prd(X,C3,C2,C1)
| icext(Z,X) )
& ( sP0_prd(X,C3,C2,C1)
| ~ icext(Z,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,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)],[f182]) ).
fof(f184,plain,
! [S1,C1,C2,C3] :
( ( ! [Z] :
( ? [X] :
( ( sP0_prd(X,C3,C2,C1)
| icext(Z,X) )
& ( ~ sP0_prd(X,C3,C2,C1)
| ~ icext(Z,X) ) )
| ~ ic(C3)
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_intersectionOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( ~ sP0_prd(X,C3,C2,C1)
| icext(Z,X) )
& ! [X] :
( sP0_prd(X,C3,C2,C1)
| ~ icext(Z,X) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,S1) ) )
| ! [S3] :
( ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,C3)
| ! [S2] :
( ~ 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(miniscoping,[status(thm)],[f183]) ).
fof(f185,plain,
! [S1,C1,C2,C3] :
( ( ! [Z] :
( ( ( sP0_prd(sK3_skl(Z,C3,C2,C1,S1),C3,C2,C1)
| icext(Z,sK3_skl(Z,C3,C2,C1,S1)) )
& ( ~ sP0_prd(sK3_skl(Z,C3,C2,C1,S1),C3,C2,C1)
| ~ icext(Z,sK3_skl(Z,C3,C2,C1,S1)) ) )
| ~ ic(C3)
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_intersectionOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( ~ sP0_prd(X,C3,C2,C1)
| icext(Z,X) )
& ! [X] :
( sP0_prd(X,C3,C2,C1)
| ~ icext(Z,X) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,S1) ) )
| ! [S3] :
( ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,C3)
| ! [S2] :
( ~ 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(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X,sK3_skl(Z,C3,C2,C1,S1))],[f184]) ).
fof(f190,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( sP0_prd(X7,X5,X3,X1)
| ~ icext(X6,X7)
| ~ iext(uri_owl_intersectionOf,X6,X0)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f342,plain,
! [P,C] :
( iext(uri_rdfs_domain,P,C)
<=> ( ! [X,Y] :
( icext(C,X)
| ~ iext(P,X,Y) )
& ic(C)
& ip(P) ) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f343,plain,
! [P,C] :
( ( ? [X,Y] :
( ~ icext(C,X)
& iext(P,X,Y) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ( ( ! [X,Y] :
( icext(C,X)
| ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(NNF_transformation,[status(thm)],[f342]) ).
fof(f344,plain,
( ! [P,C] :
( ? [X] :
( ~ icext(C,X)
& ? [Y] : iext(P,X,Y) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ! [P,C] :
( ( ! [X] :
( icext(C,X)
| ! [Y] : ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(miniscoping,[status(thm)],[f343]) ).
fof(f345,plain,
( ! [P,C] :
( ( ~ icext(C,sK9_skl(C,P))
& iext(P,sK9_skl(C,P),sK10_skl(C,P)) )
| ~ ic(C)
| ~ ip(P)
| iext(uri_rdfs_domain,P,C) )
& ! [P,C] :
( ( ! [X] :
( icext(C,X)
| ! [Y] : ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl]),skolemize(X,sK9_skl(C,P)),skolemize(Y,sK10_skl(C,P))],[f344]) ).
fof(f347,plain,
! [X0,X1] :
( ic(X1)
| ~ iext(uri_rdfs_domain,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f345]) ).
fof(f348,plain,
! [X0,X1,X2,X3] :
( icext(X1,X2)
| ~ iext(X0,X2,X3)
| ~ iext(uri_rdfs_domain,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f345]) ).
fof(f360,plain,
! [C1,C2] :
( iext(uri_rdfs_subClassOf,C1,C2)
<=> ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) ) ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f361,plain,
! [C1,C2] :
( ( ? [X] :
( ~ icext(C2,X)
& icext(C1,X) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ( ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(NNF_transformation,[status(thm)],[f360]) ).
fof(f362,plain,
( ! [C1,C2] :
( ? [X] :
( ~ icext(C2,X)
& icext(C1,X) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ! [C1,C2] :
( ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(miniscoping,[status(thm)],[f361]) ).
fof(f363,plain,
( ! [C1,C2] :
( ( ~ icext(C2,sK13_skl(C2,C1))
& icext(C1,sK13_skl(C2,C1)) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_rdfs_subClassOf,C1,C2) )
& ! [C1,C2] :
( ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X,sK13_skl(C2,C1))],[f362]) ).
fof(f366,plain,
! [X0,X1,X2] :
( icext(X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_rdfs_subClassOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f385,plain,
! [Z,P,A] :
( ! [X] :
( icext(Z,X)
<=> iext(P,X,A) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_hasValue,Z,A) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f386,plain,
! [Z,P,A] :
( ! [X] :
( ( ~ iext(P,X,A)
| icext(Z,X) )
& ( iext(P,X,A)
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_hasValue,Z,A) ),
inference(NNF_transformation,[status(thm)],[f385]) ).
fof(f387,plain,
! [Z,P,A] :
( ( ! [X] :
( ~ iext(P,X,A)
| icext(Z,X) )
& ! [X] :
( iext(P,X,A)
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_hasValue,Z,A) ),
inference(miniscoping,[status(thm)],[f386]) ).
fof(f388,plain,
! [X0,X1,X2,X3] :
( iext(X2,X3,X1)
| ~ icext(X0,X3)
| ~ iext(uri_owl_onProperty,X0,X2)
| ~ iext(uri_owl_hasValue,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f387]) ).
fof(f421,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)],[f80]) ).
fof(f422,plain,
( ! [X,C] :
( ~ icext(C,X)
| iext(uri_rdf_type,X,C) )
& ! [X,C] :
( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(miniscoping,[status(thm)],[f421]) ).
fof(f423,plain,
! [X0,X1] :
( icext(X1,X0)
| ~ iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f424,plain,
! [X0,X1] :
( ~ icext(X1,X0)
| iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f488,plain,
! [C] :
( iext(uri_rdfs_subClassOf,C,C)
| ~ ic(C) ),
inference(pre_NNF_transformation,[status(thm)],[f125]) ).
fof(f489,plain,
! [X0] :
( iext(uri_rdfs_subClassOf,X0,X0)
| ~ ic(X0) ),
inference(cnf_transformation,[status(thm)],[f488]) ).
fof(f514,plain,
( ~ iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)
| ~ iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty) ),
inference(pre_NNF_transformation,[status(thm)],[f140]) ).
fof(f515,plain,
( ~ iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)
| ~ iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty) ),
inference(cnf_transformation,[status(thm)],[f514]) ).
fof(f516,plain,
( iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))
& iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute)
& ? [BNODE_r] :
( iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person)
& iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain)
& iext(uri_rdf_type,BNODE_r,uri_owl_Restriction)
& ? [BNODE_l3] :
( iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l3,BNODE_r)
& ? [BNODE_l2] :
( iext(uri_rdf_rest,BNODE_l2,BNODE_l3)
& iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty)
& ? [BNODE_l1] :
( iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty)
& iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1)
& iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f141]) ).
fof(f517,plain,
( iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))
& iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute)
& iext(uri_owl_hasValue,sK18_skl,uri_foaf_Person)
& iext(uri_owl_onProperty,sK18_skl,uri_rdfs_domain)
& iext(uri_rdf_type,sK18_skl,uri_owl_Restriction)
& iext(uri_rdf_rest,sK19_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK19_skl,sK18_skl)
& iext(uri_rdf_rest,sK20_skl,sK19_skl)
& iext(uri_rdf_first,sK20_skl,uri_owl_FunctionalProperty)
& iext(uri_rdf_rest,sK21_skl,sK20_skl)
& iext(uri_rdf_first,sK21_skl,uri_owl_DatatypeProperty)
& iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,sK21_skl)
& iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl,sK21_skl]),skolemize(BNODE_r,sK18_skl),skolemize(BNODE_l3,sK19_skl),skolemize(BNODE_l2,sK20_skl),skolemize(BNODE_l1,sK21_skl)],[f516]) ).
fof(f519,plain,
iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,sK21_skl),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f520,plain,
iext(uri_rdf_first,sK21_skl,uri_owl_DatatypeProperty),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f521,plain,
iext(uri_rdf_rest,sK21_skl,sK20_skl),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f522,plain,
iext(uri_rdf_first,sK20_skl,uri_owl_FunctionalProperty),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f523,plain,
iext(uri_rdf_rest,sK20_skl,sK19_skl),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f524,plain,
iext(uri_rdf_first,sK19_skl,sK18_skl),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f525,plain,
iext(uri_rdf_rest,sK19_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f527,plain,
iext(uri_owl_onProperty,sK18_skl,uri_rdfs_domain),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f528,plain,
iext(uri_owl_hasValue,sK18_skl,uri_foaf_Person),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f529,plain,
iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f530,plain,
iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice)),
inference(cnf_transformation,[status(thm)],[f517]) ).
fof(f531,plain,
! [C1,C2,C3,X] :
( ( ~ icext(C3,X)
| ~ icext(C2,X)
| ~ icext(C1,X)
| sP0_prd(X,C3,C2,C1) )
& ( ( icext(C3,X)
& icext(C2,X)
& icext(C1,X) )
| ~ sP0_prd(X,C3,C2,C1) ) ),
inference(NNF_transformation,[status(thm)],[f181]) ).
fof(f532,plain,
( ! [C1,C2,C3,X] :
( ~ icext(C3,X)
| ~ icext(C2,X)
| ~ icext(C1,X)
| sP0_prd(X,C3,C2,C1) )
& ! [C1,C2,C3,X] :
( ( icext(C3,X)
& icext(C2,X)
& icext(C1,X) )
| ~ sP0_prd(X,C3,C2,C1) ) ),
inference(miniscoping,[status(thm)],[f531]) ).
fof(f534,plain,
! [X0,X1,X2,X3] :
( icext(X2,X0)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f532]) ).
fof(f535,plain,
! [X0,X1,X2,X3] :
( icext(X1,X0)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f532]) ).
fof(f601,plain,
! [X0,X1,X2,X3] :
( iext(uri_rdf_type,X0,X2)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f534,f424]) ).
fof(f606,plain,
! [X0,X1,X2,X3] :
( iext(uri_rdf_type,X0,X1)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f535,f424]) ).
fof(f618,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ icext(X7,X0)
| ~ iext(uri_owl_intersectionOf,X7,X2)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X4,X5)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f601,f190]) ).
fof(f622,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ icext(X7,X0)
| ~ iext(uri_owl_intersectionOf,X7,X2)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f606,f190]) ).
fof(f635,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ icext(X6,X0)
| ~ iext(uri_owl_intersectionOf,X6,X2)
| ~ iext(uri_rdf_first,sK19_skl,X5)
| ~ iext(uri_rdf_rest,X4,sK19_skl)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f618,f525]) ).
fof(f636,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ icext(X6,X0)
| ~ iext(uri_owl_intersectionOf,X6,X2)
| ~ iext(uri_rdf_first,sK19_skl,X1)
| ~ iext(uri_rdf_rest,X4,sK19_skl)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X2,X3)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f622,f525]) ).
fof(f637,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ icext(X5,X0)
| ~ iext(uri_owl_intersectionOf,X5,X2)
| ~ iext(uri_rdf_first,sK19_skl,X4)
| ~ iext(uri_rdf_first,sK20_skl,X1)
| ~ iext(uri_rdf_rest,X2,sK20_skl)
| ~ iext(uri_rdf_first,X2,X3)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f635,f523]) ).
fof(f638,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ icext(X5,X0)
| ~ iext(uri_owl_intersectionOf,X5,X2)
| ~ iext(uri_rdf_first,sK19_skl,X1)
| ~ iext(uri_rdf_first,sK20_skl,X4)
| ~ iext(uri_rdf_rest,X2,sK20_skl)
| ~ iext(uri_rdf_first,X2,X3)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f636,f523]) ).
fof(f639,plain,
! [X0,X1,X2,X3,X4] :
( ~ icext(X4,X0)
| ~ iext(uri_owl_intersectionOf,X4,sK21_skl)
| ~ iext(uri_rdf_first,sK19_skl,X3)
| ~ iext(uri_rdf_first,sK20_skl,X1)
| ~ iext(uri_rdf_first,sK21_skl,X2)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f637,f521]) ).
fof(f640,plain,
! [X0,X1,X2,X3] :
( ~ icext(X3,X0)
| ~ iext(uri_owl_intersectionOf,X3,sK21_skl)
| ~ iext(uri_rdf_first,sK19_skl,X2)
| ~ iext(uri_rdf_first,sK20_skl,X1)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f639,f520]) ).
fof(f641,plain,
! [X0,X1,X2] :
( ~ icext(X2,X0)
| ~ iext(uri_owl_intersectionOf,X2,sK21_skl)
| ~ iext(uri_rdf_first,sK19_skl,X1)
| iext(uri_rdf_type,X0,uri_owl_FunctionalProperty) ),
inference(resolution,[status(thm)],[f640,f522]) ).
fof(f642,plain,
! [X0,X1,X2,X3,X4] :
( ~ icext(X4,X0)
| ~ iext(uri_owl_intersectionOf,X4,sK21_skl)
| ~ iext(uri_rdf_first,sK19_skl,X1)
| ~ iext(uri_rdf_first,sK20_skl,X3)
| ~ iext(uri_rdf_first,sK21_skl,X2)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f638,f521]) ).
fof(f643,plain,
! [X0,X1,X2,X3] :
( ~ icext(X3,X0)
| ~ iext(uri_owl_intersectionOf,X3,sK21_skl)
| ~ iext(uri_rdf_first,sK19_skl,X1)
| ~ iext(uri_rdf_first,sK20_skl,X2)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f642,f520]) ).
fof(f644,plain,
! [X0,X1,X2] :
( ~ icext(X2,X0)
| ~ iext(uri_owl_intersectionOf,X2,sK21_skl)
| ~ iext(uri_rdf_first,sK19_skl,X1)
| iext(uri_rdf_type,X0,X1) ),
inference(resolution,[status(thm)],[f643,f522]) ).
fof(f645,plain,
! [X0,X1] :
( ~ icext(X1,X0)
| ~ iext(uri_owl_intersectionOf,X1,sK21_skl)
| iext(uri_rdf_type,X0,sK18_skl) ),
inference(resolution,[status(thm)],[f644,f524]) ).
fof(f772,plain,
! [X0,X1,X2] :
( iext(uri_rdf_type,X2,X1)
| ~ icext(X0,X2)
| ~ iext(uri_rdfs_subClassOf,X0,X1) ),
inference(resolution,[status(thm)],[f366,f424]) ).
fof(f799,plain,
! [X0] :
( ~ iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)
| ~ icext(X0,uri_ex_alice)
| ~ iext(uri_rdfs_subClassOf,X0,uri_foaf_Person) ),
inference(resolution,[status(thm)],[f772,f515]) ).
fof(f806,plain,
( ~ ic(uri_foaf_Person)
| ~ iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)
| ~ icext(uri_foaf_Person,uri_ex_alice) ),
inference(resolution,[status(thm)],[f799,f489]) ).
fof(f808,plain,
! [X0,X1] :
( ~ icext(X1,uri_ex_name)
| ~ iext(uri_owl_intersectionOf,X1,sK21_skl)
| ~ iext(uri_rdf_first,sK19_skl,X0)
| ~ ic(uri_foaf_Person)
| ~ icext(uri_foaf_Person,uri_ex_alice) ),
inference(resolution,[status(thm)],[f806,f641]) ).
fof(f1018,plain,
! [X0] :
( ~ icext(X0,uri_ex_name)
| ~ iext(uri_owl_intersectionOf,X0,sK21_skl)
| ~ ic(uri_foaf_Person)
| ~ icext(uri_foaf_Person,uri_ex_alice) ),
inference(resolution,[status(thm)],[f808,f524]) ).
fof(f1019,plain,
( ~ icext(uri_ex_PersonAttribute,uri_ex_name)
| ~ ic(uri_foaf_Person)
| ~ icext(uri_foaf_Person,uri_ex_alice) ),
inference(resolution,[status(thm)],[f1018,f519]) ).
fof(f1054,plain,
( ~ iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute)
| ~ ic(uri_foaf_Person)
| ~ icext(uri_foaf_Person,uri_ex_alice) ),
inference(resolution,[status(thm)],[f1019,f423]) ).
fof(f1055,plain,
( ~ ic(uri_foaf_Person)
| ~ icext(uri_foaf_Person,uri_ex_alice) ),
inference(forward_subsumption_resolution,[status(thm)],[f1054,f529]) ).
fof(f1057,plain,
! [X0,X1] :
( ~ iext(X0,uri_ex_alice,X1)
| ~ iext(uri_rdfs_domain,X0,uri_foaf_Person)
| ~ ic(uri_foaf_Person) ),
inference(resolution,[status(thm)],[f1055,f348]) ).
fof(f1064,plain,
! [X0,X1] :
( ~ iext(X0,uri_ex_alice,X1)
| ~ iext(uri_rdfs_domain,X0,uri_foaf_Person) ),
inference(forward_subsumption_resolution,[status(thm)],[f1057,f347]) ).
fof(f1847,plain,
! [X0,X1] :
( iext(uri_rdfs_domain,X1,X0)
| ~ icext(sK18_skl,X1)
| ~ iext(uri_owl_hasValue,sK18_skl,X0) ),
inference(resolution,[status(thm)],[f388,f527]) ).
fof(f1855,plain,
! [X0] :
( iext(uri_rdfs_domain,X0,uri_foaf_Person)
| ~ icext(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f1847,f528]) ).
fof(f1863,plain,
! [X0,X1] :
( ~ iext(X0,uri_ex_alice,X1)
| ~ icext(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f1855,f1064]) ).
fof(f1883,plain,
! [X0,X1] :
( ~ iext(uri_rdf_type,X0,sK18_skl)
| ~ iext(X0,uri_ex_alice,X1) ),
inference(resolution,[status(thm)],[f1863,f423]) ).
fof(f1919,plain,
! [X0,X1,X2] :
( ~ icext(X2,X0)
| ~ iext(uri_owl_intersectionOf,X2,sK21_skl)
| ~ iext(X0,uri_ex_alice,X1) ),
inference(resolution,[status(thm)],[f1883,f645]) ).
fof(f1949,plain,
! [X0,X1] :
( ~ icext(uri_ex_PersonAttribute,X0)
| ~ iext(X0,uri_ex_alice,X1) ),
inference(resolution,[status(thm)],[f1919,f519]) ).
fof(f1971,plain,
! [X0,X1] :
( ~ iext(uri_rdf_type,X0,uri_ex_PersonAttribute)
| ~ iext(X0,uri_ex_alice,X1) ),
inference(resolution,[status(thm)],[f1949,f423]) ).
fof(f2038,plain,
! [X0] : ~ iext(uri_ex_name,uri_ex_alice,X0),
inference(resolution,[status(thm)],[f1971,f529]) ).
fof(f2044,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f530,f2038]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB012+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n020.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 07:39:32 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 25.37/3.93 % Refutation found
% 25.37/3.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 25.37/3.93 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.71/4.58 % Elapsed time: 4.215120 seconds
% 2.71/4.58 % CPU time: 28.788543 seconds
% 2.71/4.58 % Total memory used: 133.008 MB
% 2.71/4.58 % Net memory used: 119.856 MB
%------------------------------------------------------------------------------