%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB024+2 : 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 : n006.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:36 PM UTC 2026
% Result : Theorem 0.17s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB024+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n006.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 07:40:30 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 0.17/0.49 % Refutation found
% 0.17/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.49 fof(f1,axiom,(
% 0.17/0.49 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f2,axiom,(
% 0.17/0.49 (! [Z,P] :( ( iext(uri_owl_minCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))& iext(uri_owl_onProperty,Z,P) )=> (! [X] :( icext(Z,X)<=> (? [Y] : iext(P,X,Y) )) )) )),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f3,axiom,(
% 0.17/0.49 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f4,axiom,(
% 0.17/0.49 (! [P] :( icext(uri_owl_TransitiveProperty,P)<=> ( ip(P)& (! [X,Y,Z] :( ( iext(P,X,Y)& iext(P,Y,Z) )=> iext(P,X,Z) ) )) ) )),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f5,conjecture,(
% 0.17/0.49 (? [BNODE_x] :( iext(uri_ex_hasAncestor,uri_ex_bob,BNODE_x)& iext(uri_ex_hasAncestor,uri_ex_alice,BNODE_x) ) )),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f6,negated_conjecture,(
% 0.17/0.49 ~((? [BNODE_x] :( iext(uri_ex_hasAncestor,uri_ex_bob,BNODE_x)& iext(uri_ex_hasAncestor,uri_ex_alice,BNODE_x) ) ))),
% 0.17/0.49 inference(negated_conjecture,[status(cth)],[f5])).
% 0.17/0.49 fof(f7,axiom,(
% 0.17/0.49 (? [BNODE_z] :( iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)& iext(uri_rdfs_subClassOf,uri_ex_Person,BNODE_z)& iext(uri_rdf_type,BNODE_z,uri_owl_Restriction)& iext(uri_owl_onProperty,BNODE_z,uri_ex_hasAncestor)& iext(uri_owl_minCardinality,BNODE_z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))& iext(uri_rdf_type,uri_ex_alice,uri_ex_Person)& iext(uri_rdf_type,uri_ex_bob,uri_ex_Person)& iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob) ) )),
% 0.17/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.49 fof(f8,plain,(
% 0.17/0.49 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 0.17/0.49 inference(NNF_transformation,[status(thm)],[f1])).
% 0.17/0.49 fof(f9,plain,(
% 0.17/0.49 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f8])).
% 0.17/0.49 fof(f10,plain,(
% 0.17/0.49 ![X0,X1]: (~iext(uri_rdf_type,X0,X1)|icext(X1,X0))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f9])).
% 0.17/0.49 fof(f12,plain,(
% 0.17/0.49 ![Z,P]: ((~iext(uri_owl_minCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|(![X]: (icext(Z,X)<=>(?[Y]: iext(P,X,Y)))))),
% 0.17/0.49 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.17/0.49 fof(f13,plain,(
% 0.17/0.49 ![Z,P]: ((~iext(uri_owl_minCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|(![X]: ((~icext(Z,X)|(?[Y]: iext(P,X,Y)))&(icext(Z,X)|(![Y]: ~iext(P,X,Y))))))),
% 0.17/0.49 inference(NNF_transformation,[status(thm)],[f12])).
% 0.17/0.49 fof(f14,plain,(
% 0.17/0.49 ![Z,P]: ((~iext(uri_owl_minCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|((![X]: (~icext(Z,X)|(?[Y]: iext(P,X,Y))))&(![X]: (icext(Z,X)|(![Y]: ~iext(P,X,Y))))))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f13])).
% 0.17/0.49 fof(f15,plain,(
% 0.17/0.49 ![Z,P]: ((~iext(uri_owl_minCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|((![X]: (~icext(Z,X)|iext(P,X,sK0_skl(X,P,Z))))&(![X]: (icext(Z,X)|(![Y]: ~iext(P,X,Y))))))),
% 0.17/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y,sK0_skl(X,P,Z))],[f14])).
% 0.17/0.49 fof(f16,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~iext(uri_owl_minCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X0,X1)|~icext(X0,X2)|iext(X1,X2,sK0_skl(X2,X1,X0)))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f15])).
% 0.17/0.49 fof(f18,plain,(
% 0.17/0.49 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 0.17/0.49 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.17/0.49 fof(f19,plain,(
% 0.17/0.49 ![C1,C2]: ((~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))&(iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: (icext(C1,X)&~icext(C2,X))))))),
% 0.17/0.49 inference(NNF_transformation,[status(thm)],[f18])).
% 0.17/0.49 fof(f20,plain,(
% 0.17/0.49 (![C1,C2]: (~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X))))))&(![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: (icext(C1,X)&~icext(C2,X))))))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f19])).
% 0.17/0.49 fof(f21,plain,(
% 0.17/0.49 (![C1,C2]: (~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X))))))&(![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(icext(C1,sK1_skl(C2,C1))&~icext(C2,sK1_skl(C2,C1))))))),
% 0.17/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl(C2,C1))],[f20])).
% 0.17/0.49 fof(f24,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~iext(uri_rdfs_subClassOf,X0,X1)|~icext(X0,X2)|icext(X1,X2))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f21])).
% 0.17/0.49 fof(f27,plain,(
% 0.17/0.49 ![P]: (icext(uri_owl_TransitiveProperty,P)<=>(ip(P)&(![X,Y,Z]: ((~iext(P,X,Y)|~iext(P,Y,Z))|iext(P,X,Z)))))),
% 0.17/0.49 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.17/0.49 fof(f28,plain,(
% 0.17/0.49 ![P]: ((~icext(uri_owl_TransitiveProperty,P)|(ip(P)&(![X,Y,Z]: ((~iext(P,X,Y)|~iext(P,Y,Z))|iext(P,X,Z)))))&(icext(uri_owl_TransitiveProperty,P)|(~ip(P)|(?[X,Y,Z]: ((iext(P,X,Y)&iext(P,Y,Z))&~iext(P,X,Z))))))),
% 0.17/0.49 inference(NNF_transformation,[status(thm)],[f27])).
% 0.17/0.49 fof(f29,plain,(
% 0.17/0.49 (![P]: (~icext(uri_owl_TransitiveProperty,P)|(ip(P)&(![X,Z]: ((![Y]: (~iext(P,X,Y)|~iext(P,Y,Z)))|iext(P,X,Z))))))&(![P]: (icext(uri_owl_TransitiveProperty,P)|(~ip(P)|(?[X,Z]: ((?[Y]: (iext(P,X,Y)&iext(P,Y,Z)))&~iext(P,X,Z))))))),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f28])).
% 0.17/0.49 fof(f30,plain,(
% 0.17/0.49 (![P]: (~icext(uri_owl_TransitiveProperty,P)|(ip(P)&(![X,Z]: ((![Y]: (~iext(P,X,Y)|~iext(P,Y,Z)))|iext(P,X,Z))))))&(![P]: (icext(uri_owl_TransitiveProperty,P)|(~ip(P)|((iext(P,sK2_skl(P),sK4_skl(P))&iext(P,sK4_skl(P),sK3_skl(P)))&~iext(P,sK2_skl(P),sK3_skl(P))))))),
% 0.17/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl]),skolemize(X,sK2_skl(P)),skolemize(Z,sK3_skl(P)),skolemize(Y,sK4_skl(P))],[f29])).
% 0.17/0.49 fof(f32,plain,(
% 0.17/0.49 ![X0,X1,X2,X3]: (~icext(uri_owl_TransitiveProperty,X0)|~iext(X0,X1,X2)|~iext(X0,X2,X3)|iext(X0,X1,X3))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f30])).
% 0.17/0.49 fof(f36,plain,(
% 0.17/0.49 (![BNODE_x]: (~iext(uri_ex_hasAncestor,uri_ex_bob,BNODE_x)|~iext(uri_ex_hasAncestor,uri_ex_alice,BNODE_x)))),
% 0.17/0.49 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.17/0.49 fof(f37,plain,(
% 0.17/0.49 ![X0]: (~iext(uri_ex_hasAncestor,uri_ex_bob,X0)|~iext(uri_ex_hasAncestor,uri_ex_alice,X0))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f36])).
% 0.17/0.49 fof(f38,plain,(
% 0.17/0.49 (((?[BNODE_z]: ((((iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)&iext(uri_rdfs_subClassOf,uri_ex_Person,BNODE_z))&iext(uri_rdf_type,BNODE_z,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_z,uri_ex_hasAncestor))&iext(uri_owl_minCardinality,BNODE_z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))))&iext(uri_rdf_type,uri_ex_alice,uri_ex_Person))&iext(uri_rdf_type,uri_ex_bob,uri_ex_Person))&iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob)),
% 0.17/0.49 inference(miniscoping,[status(thm)],[f7])).
% 0.17/0.49 fof(f39,plain,(
% 0.17/0.49 ((((((iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)&iext(uri_rdfs_subClassOf,uri_ex_Person,sK5_skl))&iext(uri_rdf_type,sK5_skl,uri_owl_Restriction))&iext(uri_owl_onProperty,sK5_skl,uri_ex_hasAncestor))&iext(uri_owl_minCardinality,sK5_skl,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger)))&iext(uri_rdf_type,uri_ex_alice,uri_ex_Person))&iext(uri_rdf_type,uri_ex_bob,uri_ex_Person))&iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob)),
% 0.17/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(BNODE_z,sK5_skl)],[f38])).
% 0.17/0.49 fof(f40,plain,(
% 0.17/0.49 iext(uri_rdf_type,uri_ex_hasAncestor,uri_owl_TransitiveProperty)),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/0.49 fof(f41,plain,(
% 0.17/0.49 iext(uri_rdfs_subClassOf,uri_ex_Person,sK5_skl)),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/0.49 fof(f43,plain,(
% 0.17/0.49 iext(uri_owl_onProperty,sK5_skl,uri_ex_hasAncestor)),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/0.49 fof(f44,plain,(
% 0.17/0.49 iext(uri_owl_minCardinality,sK5_skl,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/0.49 fof(f46,plain,(
% 0.17/0.49 iext(uri_rdf_type,uri_ex_bob,uri_ex_Person)),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/0.49 fof(f47,plain,(
% 0.17/0.49 iext(uri_ex_hasAncestor,uri_ex_alice,uri_ex_bob)),
% 0.17/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/0.49 fof(f49,plain,(
% 0.17/0.49 icext(uri_ex_Person,uri_ex_bob)),
% 0.17/0.49 inference(resolution,[status(thm)],[f10,f46])).
% 0.17/0.49 fof(f51,plain,(
% 0.17/0.49 icext(uri_owl_TransitiveProperty,uri_ex_hasAncestor)),
% 0.17/0.49 inference(resolution,[status(thm)],[f10,f40])).
% 0.17/0.49 fof(f83,plain,(
% 0.17/0.49 ![X0,X1,X2]: (~iext(uri_ex_hasAncestor,X0,X1)|~iext(uri_ex_hasAncestor,X1,X2)|iext(uri_ex_hasAncestor,X0,X2))),
% 0.17/0.49 inference(resolution,[status(thm)],[f32,f51])).
% 0.17/0.49 fof(f117,plain,(
% 0.17/0.49 ![X0,X1]: (~iext(uri_owl_onProperty,sK5_skl,X0)|~icext(sK5_skl,X1)|iext(X0,X1,sK0_skl(X1,X0,sK5_skl)))),
% 0.17/0.49 inference(resolution,[status(thm)],[f44,f16])).
% 0.17/0.49 fof(f127,plain,(
% 0.17/0.49 ![X0]: (~icext(sK5_skl,X0)|iext(uri_ex_hasAncestor,X0,sK0_skl(X0,uri_ex_hasAncestor,sK5_skl)))),
% 0.17/0.49 inference(resolution,[status(thm)],[f117,f43])).
% 0.17/0.49 fof(f129,plain,(
% 0.17/0.49 ![X0,X1]: (iext(uri_ex_hasAncestor,X0,sK0_skl(X0,uri_ex_hasAncestor,sK5_skl))|~iext(uri_rdfs_subClassOf,X1,sK5_skl)|~icext(X1,X0))),
% 0.17/0.49 inference(resolution,[status(thm)],[f127,f24])).
% 0.17/0.49 fof(f136,plain,(
% 0.17/0.49 ![X0]: (iext(uri_ex_hasAncestor,X0,sK0_skl(X0,uri_ex_hasAncestor,sK5_skl))|~icext(uri_ex_Person,X0))),
% 0.17/0.49 inference(resolution,[status(thm)],[f129,f41])).
% 0.17/0.49 fof(f139,plain,(
% 0.17/0.49 iext(uri_ex_hasAncestor,uri_ex_bob,sK0_skl(uri_ex_bob,uri_ex_hasAncestor,sK5_skl))),
% 0.17/0.49 inference(resolution,[status(thm)],[f136,f49])).
% 0.17/0.49 fof(f142,plain,(
% 0.17/0.49 ![X0]: (~iext(uri_ex_hasAncestor,X0,uri_ex_bob)|iext(uri_ex_hasAncestor,X0,sK0_skl(uri_ex_bob,uri_ex_hasAncestor,sK5_skl)))),
% 0.17/0.49 inference(resolution,[status(thm)],[f139,f83])).
% 0.17/0.49 fof(f144,plain,(
% 0.17/0.49 iext(uri_ex_hasAncestor,uri_ex_alice,sK0_skl(uri_ex_bob,uri_ex_hasAncestor,sK5_skl))),
% 0.17/0.49 inference(resolution,[status(thm)],[f142,f47])).
% 0.17/0.49 fof(f145,plain,(
% 0.17/0.49 ~iext(uri_ex_hasAncestor,uri_ex_bob,sK0_skl(uri_ex_bob,uri_ex_hasAncestor,sK5_skl))),
% 0.17/0.49 inference(resolution,[status(thm)],[f144,f37])).
% 0.17/0.49 fof(f148,plain,(
% 0.17/0.49 $false),
% 0.17/0.49 inference(forward_subsumption_resolution,[status(thm)],[f145,f139])).
% 0.17/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.53 % Elapsed time: 0.082150 seconds
% 0.17/0.53 % CPU time: 0.083517 seconds
% 0.17/0.53 % Total memory used: 2.648 MB
% 0.17/0.53 % Net memory used: 2.626 MB
%------------------------------------------------------------------------------