%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB012+3 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:28 PM UTC 2026
% Result : Theorem 3.96s 0.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB012+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.33 % Computer : n019.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Mon Sep 21 07:38:50 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 3.96/0.91 % Refutation found
% 3.96/0.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.96/0.91 % SZS output start CNFRefutation for theBenchmark
% 3.96/0.91 fof(f5,axiom,(
% 3.96/0.91 (! [Z,S1,C1,S2,C2,S3,C3] :( ( iext(uri_rdf_first,S1,C1)& iext(uri_rdf_rest,S1,S2)& iext(uri_rdf_first,S2,C2)& iext(uri_rdf_rest,S2,S3)& iext(uri_rdf_first,S3,C3)& iext(uri_rdf_rest,S3,uri_rdf_nil) )=> ( iext(uri_owl_intersectionOf,Z,S1)<=> ( ic(Z)& ic(C1)& ic(C2)& ic(C3)& (! [X] :( icext(Z,X)<=> ( icext(C1,X)& icext(C2,X)& icext(C3,X) ) ) )) ) ) )),
% 3.96/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.96/0.91 fof(f52,axiom,(
% 3.96/0.91 (! [P,C] :( iext(uri_rdfs_domain,P,C)<=> ( ip(P)& ic(C)& (! [X,Y] :( iext(P,X,Y)=> icext(C,X) ) )) ) )),
% 3.96/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.96/0.91 fof(f57,axiom,(
% 3.96/0.91 (! [Z,P,A] :( ( iext(uri_owl_hasValue,Z,A)& iext(uri_owl_onProperty,Z,P) )=> (! [X] :( icext(Z,X)<=> iext(P,X,A) ) )) )),
% 3.96/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.96/0.91 fof(f80,axiom,(
% 3.96/0.91 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 3.96/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.96/0.91 fof(f139,conjecture,(
% 3.96/0.91 ( iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)& iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person) ) ),
% 3.96/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.96/0.91 fof(f140,negated_conjecture,(
% 3.96/0.91 ~(( iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)& iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person) ) )),
% 3.96/0.91 inference(negated_conjecture,[status(cth)],[f139])).
% 3.96/0.91 fof(f141,axiom,(
% 3.96/0.91 (? [BNODE_l1,BNODE_l2,BNODE_l3,BNODE_r] :( iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)& iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1)& iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty)& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)& iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty)& iext(uri_rdf_rest,BNODE_l2,BNODE_l3)& iext(uri_rdf_first,BNODE_l3,BNODE_r)& iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil)& iext(uri_rdf_type,BNODE_r,uri_owl_Restriction)& iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain)& iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person)& iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute)& iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice)) ) )),
% 3.96/0.91 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.96/0.91 fof(f180,plain,(
% 3.96/0.91 ![Z,S1,C1,S2,C2,S3,C3]: ((((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|(iext(uri_owl_intersectionOf,Z,S1)<=>((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&(![X]: (icext(Z,X)<=>((icext(C1,X)&icext(C2,X))&icext(C3,X)))))))),
% 3.96/0.91 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 3.96/0.91 fof(f181,definition,(
% 3.96/0.91 ![C1,C2,C3,X]: (sP0_prd(X,C3,C2,C1)<=>((icext(C1,X)&icext(C2,X))&icext(C3,X)))),
% 3.96/0.91 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 3.96/0.91 fof(f182,plain,(
% 3.96/0.91 ![Z,S1,C1,S2,C2,S3,C3]: ((((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|(iext(uri_owl_intersectionOf,Z,S1)<=>((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&(![X]: (icext(Z,X)<=>sP0_prd(X,C3,C2,C1))))))),
% 3.96/0.91 inference(formula_renaming,[status(thm)],[f180,f181])).
% 3.96/0.91 fof(f183,plain,(
% 3.96/0.91 ![Z,S1,C1,S2,C2,S3,C3]: ((((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,Z,S1)|((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&(![X]: ((~icext(Z,X)|sP0_prd(X,C3,C2,C1))&(icext(Z,X)|~sP0_prd(X,C3,C2,C1))))))&(iext(uri_owl_intersectionOf,Z,S1)|((((~ic(Z)|~ic(C1))|~ic(C2))|~ic(C3))|(?[X]: ((~icext(Z,X)|~sP0_prd(X,C3,C2,C1))&(icext(Z,X)|sP0_prd(X,C3,C2,C1))))))))),
% 3.96/0.91 inference(NNF_transformation,[status(thm)],[f182])).
% 3.96/0.91 fof(f184,plain,(
% 3.96/0.91 ![S1,C1,C2,C3]: ((![S3]: (((![S2]: (((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3)))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_intersectionOf,Z,S1)|((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&((![X]: (~icext(Z,X)|sP0_prd(X,C3,C2,C1)))&(![X]: (icext(Z,X)|~sP0_prd(X,C3,C2,C1)))))))&(![Z]: (iext(uri_owl_intersectionOf,Z,S1)|((((~ic(Z)|~ic(C1))|~ic(C2))|~ic(C3))|(?[X]: ((~icext(Z,X)|~sP0_prd(X,C3,C2,C1))&(icext(Z,X)|sP0_prd(X,C3,C2,C1)))))))))),
% 3.96/0.91 inference(miniscoping,[status(thm)],[f183])).
% 3.96/0.91 fof(f185,plain,(
% 3.96/0.91 ![S1,C1,C2,C3]: ((![S3]: (((![S2]: (((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3)))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_intersectionOf,Z,S1)|((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&((![X]: (~icext(Z,X)|sP0_prd(X,C3,C2,C1)))&(![X]: (icext(Z,X)|~sP0_prd(X,C3,C2,C1)))))))&(![Z]: (iext(uri_owl_intersectionOf,Z,S1)|((((~ic(Z)|~ic(C1))|~ic(C2))|~ic(C3))|((~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))|sP0_prd(sK3_skl(Z,C3,C2,C1,S1),C3,C2,C1))))))))),
% 3.96/0.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X,sK3_skl(Z,C3,C2,C1,S1))],[f184])).
% 3.96/0.91 fof(f190,plain,(
% 3.96/0.91 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,X2)|~iext(uri_rdf_first,X2,X3)|~iext(uri_rdf_rest,X2,X4)|~iext(uri_rdf_first,X4,X5)|~iext(uri_rdf_rest,X4,uri_rdf_nil)|~iext(uri_owl_intersectionOf,X6,X0)|~icext(X6,X7)|sP0_prd(X7,X5,X3,X1))),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f185])).
% 3.96/0.91 fof(f342,plain,(
% 3.96/0.91 ![P,C]: (iext(uri_rdfs_domain,P,C)<=>((ip(P)&ic(C))&(![X,Y]: (~iext(P,X,Y)|icext(C,X)))))),
% 3.96/0.91 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 3.96/0.91 fof(f343,plain,(
% 3.96/0.91 ![P,C]: ((~iext(uri_rdfs_domain,P,C)|((ip(P)&ic(C))&(![X,Y]: (~iext(P,X,Y)|icext(C,X)))))&(iext(uri_rdfs_domain,P,C)|((~ip(P)|~ic(C))|(?[X,Y]: (iext(P,X,Y)&~icext(C,X))))))),
% 3.96/0.91 inference(NNF_transformation,[status(thm)],[f342])).
% 3.96/0.91 fof(f344,plain,(
% 3.96/0.91 (![P,C]: (~iext(uri_rdfs_domain,P,C)|((ip(P)&ic(C))&(![X]: ((![Y]: ~iext(P,X,Y))|icext(C,X))))))&(![P,C]: (iext(uri_rdfs_domain,P,C)|((~ip(P)|~ic(C))|(?[X]: ((?[Y]: iext(P,X,Y))&~icext(C,X))))))),
% 3.96/0.91 inference(miniscoping,[status(thm)],[f343])).
% 3.96/0.91 fof(f345,plain,(
% 3.96/0.91 (![P,C]: (~iext(uri_rdfs_domain,P,C)|((ip(P)&ic(C))&(![X]: ((![Y]: ~iext(P,X,Y))|icext(C,X))))))&(![P,C]: (iext(uri_rdfs_domain,P,C)|((~ip(P)|~ic(C))|(iext(P,sK9_skl(C,P),sK10_skl(C,P))&~icext(C,sK9_skl(C,P))))))),
% 3.96/0.91 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl]),skolemize(X,sK9_skl(C,P)),skolemize(Y,sK10_skl(C,P))],[f344])).
% 3.96/0.91 fof(f348,plain,(
% 3.96/0.91 ![X0,X1,X2,X3]: (~iext(uri_rdfs_domain,X0,X1)|~iext(X0,X2,X3)|icext(X1,X2))),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f345])).
% 3.96/0.91 fof(f385,plain,(
% 3.96/0.91 ![Z,P,A]: ((~iext(uri_owl_hasValue,Z,A)|~iext(uri_owl_onProperty,Z,P))|(![X]: (icext(Z,X)<=>iext(P,X,A))))),
% 3.96/0.91 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 3.96/0.91 fof(f386,plain,(
% 3.96/0.91 ![Z,P,A]: ((~iext(uri_owl_hasValue,Z,A)|~iext(uri_owl_onProperty,Z,P))|(![X]: ((~icext(Z,X)|iext(P,X,A))&(icext(Z,X)|~iext(P,X,A)))))),
% 3.96/0.91 inference(NNF_transformation,[status(thm)],[f385])).
% 3.96/0.91 fof(f387,plain,(
% 3.96/0.91 ![Z,P,A]: ((~iext(uri_owl_hasValue,Z,A)|~iext(uri_owl_onProperty,Z,P))|((![X]: (~icext(Z,X)|iext(P,X,A)))&(![X]: (icext(Z,X)|~iext(P,X,A)))))),
% 3.96/0.91 inference(miniscoping,[status(thm)],[f386])).
% 3.96/0.91 fof(f388,plain,(
% 3.96/0.91 ![X0,X1,X2,X3]: (~iext(uri_owl_hasValue,X0,X1)|~iext(uri_owl_onProperty,X0,X2)|~icext(X0,X3)|iext(X2,X3,X1))),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f387])).
% 3.96/0.91 fof(f421,plain,(
% 3.96/0.91 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 3.96/0.91 inference(NNF_transformation,[status(thm)],[f80])).
% 3.96/0.91 fof(f422,plain,(
% 3.96/0.91 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 3.96/0.91 inference(miniscoping,[status(thm)],[f421])).
% 3.96/0.91 fof(f423,plain,(
% 3.96/0.91 ![X0,X1]: (~iext(uri_rdf_type,X0,X1)|icext(X1,X0))),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f422])).
% 3.96/0.91 fof(f424,plain,(
% 3.96/0.91 ![X0,X1]: (iext(uri_rdf_type,X0,X1)|~icext(X1,X0))),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f422])).
% 3.96/0.91 fof(f514,plain,(
% 3.96/0.91 (~iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)|~iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person))),
% 3.96/0.91 inference(pre_NNF_transformation,[status(thm)],[f140])).
% 3.96/0.91 fof(f515,plain,(
% 3.96/0.91 ~iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)|~iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f514])).
% 3.96/0.91 fof(f516,plain,(
% 3.96/0.91 ((?[BNODE_r]: ((((?[BNODE_l3]: (((?[BNODE_l2]: (((?[BNODE_l1]: (((iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)&iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2)))&iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty))&iext(uri_rdf_rest,BNODE_l2,BNODE_l3)))&iext(uri_rdf_first,BNODE_l3,BNODE_r))&iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil)))&iext(uri_rdf_type,BNODE_r,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain))&iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person)))&iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute))&iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))),
% 3.96/0.91 inference(miniscoping,[status(thm)],[f141])).
% 3.96/0.91 fof(f517,plain,(
% 3.96/0.91 (((((((((((iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)&iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,sK21_skl))&iext(uri_rdf_first,sK21_skl,uri_owl_DatatypeProperty))&iext(uri_rdf_rest,sK21_skl,sK20_skl))&iext(uri_rdf_first,sK20_skl,uri_owl_FunctionalProperty))&iext(uri_rdf_rest,sK20_skl,sK19_skl))&iext(uri_rdf_first,sK19_skl,sK18_skl))&iext(uri_rdf_rest,sK19_skl,uri_rdf_nil))&iext(uri_rdf_type,sK18_skl,uri_owl_Restriction))&iext(uri_owl_onProperty,sK18_skl,uri_rdfs_domain))&iext(uri_owl_hasValue,sK18_skl,uri_foaf_Person))&iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute))&iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))),
% 3.96/0.91 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])).
% 3.96/0.91 fof(f519,plain,(
% 3.96/0.91 iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,sK21_skl)),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.91 fof(f520,plain,(
% 3.96/0.91 iext(uri_rdf_first,sK21_skl,uri_owl_DatatypeProperty)),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.91 fof(f521,plain,(
% 3.96/0.91 iext(uri_rdf_rest,sK21_skl,sK20_skl)),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.91 fof(f522,plain,(
% 3.96/0.91 iext(uri_rdf_first,sK20_skl,uri_owl_FunctionalProperty)),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.91 fof(f523,plain,(
% 3.96/0.91 iext(uri_rdf_rest,sK20_skl,sK19_skl)),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.91 fof(f524,plain,(
% 3.96/0.91 iext(uri_rdf_first,sK19_skl,sK18_skl)),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.91 fof(f525,plain,(
% 3.96/0.91 iext(uri_rdf_rest,sK19_skl,uri_rdf_nil)),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.91 fof(f527,plain,(
% 3.96/0.91 iext(uri_owl_onProperty,sK18_skl,uri_rdfs_domain)),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.91 fof(f528,plain,(
% 3.96/0.91 iext(uri_owl_hasValue,sK18_skl,uri_foaf_Person)),
% 3.96/0.91 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.92 fof(f529,plain,(
% 3.96/0.92 iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute)),
% 3.96/0.92 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.92 fof(f530,plain,(
% 3.96/0.92 iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))),
% 3.96/0.92 inference(cnf_transformation,[status(thm)],[f517])).
% 3.96/0.92 fof(f531,plain,(
% 3.96/0.92 ![C1,C2,C3,X]: ((~sP0_prd(X,C3,C2,C1)|((icext(C1,X)&icext(C2,X))&icext(C3,X)))&(sP0_prd(X,C3,C2,C1)|((~icext(C1,X)|~icext(C2,X))|~icext(C3,X))))),
% 3.96/0.92 inference(NNF_transformation,[status(thm)],[f181])).
% 3.96/0.92 fof(f532,plain,(
% 3.96/0.92 (![C1,C2,C3,X]: (~sP0_prd(X,C3,C2,C1)|((icext(C1,X)&icext(C2,X))&icext(C3,X))))&(![C1,C2,C3,X]: (sP0_prd(X,C3,C2,C1)|((~icext(C1,X)|~icext(C2,X))|~icext(C3,X))))),
% 3.96/0.92 inference(miniscoping,[status(thm)],[f531])).
% 3.96/0.92 fof(f534,plain,(
% 3.96/0.92 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|icext(X2,X0))),
% 3.96/0.92 inference(cnf_transformation,[status(thm)],[f532])).
% 3.96/0.92 fof(f535,plain,(
% 3.96/0.92 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|icext(X1,X0))),
% 3.96/0.92 inference(cnf_transformation,[status(thm)],[f532])).
% 3.96/0.92 fof(f548,plain,(
% 3.96/0.92 icext(uri_ex_PersonAttribute,uri_ex_name)),
% 1.80/0.92 inference(resolution,[status(thm)],[f529,f423])).
% 1.80/0.92 fof(f723,plain,(
% 1.80/0.92 ![X0,X1]: (~iext(uri_owl_onProperty,sK18_skl,X0)|~icext(sK18_skl,X1)|iext(X0,X1,uri_foaf_Person))),
% 1.80/0.92 inference(resolution,[status(thm)],[f388,f528])).
% 1.80/0.92 fof(f724,plain,(
% 1.80/0.92 ![X0]: (~icext(sK18_skl,X0)|iext(uri_rdfs_domain,X0,uri_foaf_Person))),
% 1.80/0.92 inference(resolution,[status(thm)],[f723,f527])).
% 1.80/0.92 fof(f859,plain,(
% 1.80/0.92 ![X0,X1,X2,X3,X4,X5]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK20_skl)|~iext(uri_rdf_rest,sK20_skl,X2)|~iext(uri_rdf_first,X2,X3)|~iext(uri_rdf_rest,X2,uri_rdf_nil)|~iext(uri_owl_intersectionOf,X4,X0)|~icext(X4,X5)|sP0_prd(X5,X3,uri_owl_FunctionalProperty,X1))),
% 1.80/0.92 inference(resolution,[status(thm)],[f190,f522])).
% 1.80/0.92 fof(f877,plain,(
% 1.80/0.92 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK21_skl,X0)|~iext(uri_rdf_rest,sK21_skl,sK20_skl)|~iext(uri_rdf_rest,sK20_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|~icext(uri_ex_PersonAttribute,X3)|sP0_prd(X3,X2,uri_owl_FunctionalProperty,X0))),
% 1.80/0.92 inference(resolution,[status(thm)],[f859,f519])).
% 1.80/0.92 fof(f881,plain,(
% 1.80/0.92 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK21_skl,X0)|~iext(uri_rdf_rest,sK20_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|~icext(uri_ex_PersonAttribute,X3)|sP0_prd(X3,X2,uri_owl_FunctionalProperty,X0))),
% 1.80/0.92 inference(forward_subsumption_resolution,[status(thm)],[f877,f521])).
% 1.80/0.92 fof(f882,plain,(
% 1.80/0.92 ![X0,X1,X2]: (~iext(uri_rdf_first,sK21_skl,X0)|~iext(uri_rdf_first,sK19_skl,X1)|~iext(uri_rdf_rest,sK19_skl,uri_rdf_nil)|~icext(uri_ex_PersonAttribute,X2)|sP0_prd(X2,X1,uri_owl_FunctionalProperty,X0))),
% 1.80/0.92 inference(resolution,[status(thm)],[f881,f523])).
% 1.80/0.92 fof(f884,plain,(
% 1.80/0.92 ![X0,X1,X2]: (~iext(uri_rdf_first,sK21_skl,X0)|~iext(uri_rdf_first,sK19_skl,X1)|~icext(uri_ex_PersonAttribute,X2)|sP0_prd(X2,X1,uri_owl_FunctionalProperty,X0))),
% 1.80/0.92 inference(forward_subsumption_resolution,[status(thm)],[f882,f525])).
% 1.80/0.92 fof(f898,plain,(
% 1.80/0.92 ![X0,X1]: (~iext(uri_rdf_first,sK19_skl,X0)|~icext(uri_ex_PersonAttribute,X1)|sP0_prd(X1,X0,uri_owl_FunctionalProperty,uri_owl_DatatypeProperty))),
% 1.80/0.92 inference(resolution,[status(thm)],[f884,f520])).
% 1.80/0.92 fof(f899,plain,(
% 1.80/0.92 ![X0]: (~icext(uri_ex_PersonAttribute,X0)|sP0_prd(X0,sK18_skl,uri_owl_FunctionalProperty,uri_owl_DatatypeProperty))),
% 1.80/0.92 inference(resolution,[status(thm)],[f898,f524])).
% 1.80/0.92 fof(f900,plain,(
% 1.80/0.92 sP0_prd(uri_ex_name,sK18_skl,uri_owl_FunctionalProperty,uri_owl_DatatypeProperty)),
% 1.80/0.92 inference(resolution,[status(thm)],[f899,f548])).
% 1.80/0.92 fof(f901,plain,(
% 1.80/0.92 icext(sK18_skl,uri_ex_name)),
% 1.80/0.92 inference(resolution,[status(thm)],[f900,f535])).
% 1.80/0.92 fof(f902,plain,(
% 1.80/0.92 icext(uri_owl_FunctionalProperty,uri_ex_name)),
% 1.80/0.92 inference(resolution,[status(thm)],[f900,f534])).
% 1.80/0.92 fof(f926,plain,(
% 1.80/0.92 iext(uri_rdfs_domain,uri_ex_name,uri_foaf_Person)),
% 1.80/0.92 inference(resolution,[status(thm)],[f901,f724])).
% 1.80/0.92 fof(f942,plain,(
% 1.80/0.92 iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)),
% 1.80/0.92 inference(resolution,[status(thm)],[f902,f424])).
% 1.80/0.92 fof(f951,plain,(
% 1.80/0.92 ![X0,X1]: (~iext(uri_ex_name,X0,X1)|icext(uri_foaf_Person,X0))),
% 1.80/0.92 inference(resolution,[status(thm)],[f926,f348])).
% 1.80/0.92 fof(f999,plain,(
% 1.80/0.92 ~iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)),
% 1.80/0.92 inference(backward_subsumption_resolution,[status(thm)],[f515,f942])).
% 1.80/0.92 fof(f1024,plain,(
% 1.80/0.92 icext(uri_foaf_Person,uri_ex_alice)),
% 1.80/0.92 inference(resolution,[status(thm)],[f951,f530])).
% 1.80/0.92 fof(f1031,plain,(
% 1.80/0.92 iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)),
% 1.80/0.92 inference(resolution,[status(thm)],[f1024,f424])).
% 1.80/0.92 fof(f1032,plain,(
% 1.80/0.92 $false),
% 1.80/0.92 inference(forward_subsumption_resolution,[status(thm)],[f1031,f999])).
% 1.80/0.92 % SZS output end CNFRefutation for theBenchmark.p
% 1.80/0.94 % Elapsed time: 0.588730 seconds
% 1.80/0.94 % CPU time: 4.260767 seconds
% 1.80/0.94 % Total memory used: 75.008 MB
% 1.80/0.94 % Net memory used: 72.230 MB
%------------------------------------------------------------------------------