%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB029+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 : n008.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:39 PM UTC 2026
% Result : Theorem 11.90s 1.98s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB029+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n008.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % 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:43:09 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 11.90/1.98 % Refutation found
% 11.90/1.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.90/1.98 % SZS output start CNFRefutation for theBenchmark
% 11.90/1.98 fof(f1,axiom,(
% 11.90/1.98 (! [Z,C] :( iext(uri_owl_complementOf,Z,C)=> ( ic(Z)& ic(C)& (! [X] :( icext(Z,X)<=> ~ icext(C,X) ) )) ) )),
% 11.90/1.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.90/1.98 fof(f4,axiom,(
% 11.90/1.98 (! [Z,S1,C1,S2,C2] :( ( iext(uri_rdf_first,S1,C1)& iext(uri_rdf_rest,S1,S2)& iext(uri_rdf_first,S2,C2)& iext(uri_rdf_rest,S2,uri_rdf_nil) )=> ( iext(uri_owl_intersectionOf,Z,S1)<=> ( ic(Z)& ic(C1)& ic(C2)& (! [X] :( icext(Z,X)<=> ( icext(C1,X)& icext(C2,X) ) ) )) ) ) )),
% 11.90/1.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.90/1.98 fof(f80,axiom,(
% 11.90/1.98 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 11.90/1.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.90/1.98 fof(f141,axiom,(
% 11.90/1.98 (? [BNODE_x,BNODE_y,BNODE_l1,BNODE_l2] :( iext(uri_rdf_type,uri_ex_A,uri_owl_Class)& iext(uri_rdf_type,uri_ex_B,uri_owl_Class)& iext(uri_rdf_type,uri_ex_w,BNODE_x)& iext(uri_owl_intersectionOf,BNODE_x,BNODE_l1)& iext(uri_rdf_first,BNODE_l1,uri_ex_A)& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)& iext(uri_rdf_first,BNODE_l2,BNODE_y)& iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)& iext(uri_owl_complementOf,BNODE_y,uri_ex_A) ) )),
% 11.90/1.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.90/1.98 fof(f142,plain,(
% 11.90/1.98 ![Z,C]: (~iext(uri_owl_complementOf,Z,C)|((ic(Z)&ic(C))&(![X]: (icext(Z,X)<=>~icext(C,X)))))),
% 11.90/1.98 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 11.90/1.98 fof(f143,plain,(
% 11.90/1.98 ![Z,C]: (~iext(uri_owl_complementOf,Z,C)|((ic(Z)&ic(C))&(![X]: ((~icext(Z,X)|~icext(C,X))&(icext(Z,X)|icext(C,X))))))),
% 11.90/1.98 inference(NNF_transformation,[status(thm)],[f142])).
% 11.90/1.98 fof(f144,plain,(
% 11.90/1.98 ![Z,C]: (~iext(uri_owl_complementOf,Z,C)|((ic(Z)&ic(C))&((![X]: (~icext(Z,X)|~icext(C,X)))&(![X]: (icext(Z,X)|icext(C,X))))))),
% 11.90/1.98 inference(miniscoping,[status(thm)],[f143])).
% 11.90/1.98 fof(f147,plain,(
% 11.90/1.98 ![X0,X1,X2]: (~iext(uri_owl_complementOf,X0,X1)|~icext(X0,X2)|~icext(X1,X2))),
% 11.90/1.98 inference(cnf_transformation,[status(thm)],[f144])).
% 11.90/1.98 fof(f167,plain,(
% 11.90/1.98 ![Z,S1,C1,S2,C2]: ((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|(iext(uri_owl_intersectionOf,Z,S1)<=>(((ic(Z)&ic(C1))&ic(C2))&(![X]: (icext(Z,X)<=>(icext(C1,X)&icext(C2,X)))))))),
% 11.90/1.98 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 11.90/1.98 fof(f168,plain,(
% 11.90/1.98 ![Z,S1,C1,S2,C2]: ((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,Z,S1)|(((ic(Z)&ic(C1))&ic(C2))&(![X]: ((~icext(Z,X)|(icext(C1,X)&icext(C2,X)))&(icext(Z,X)|(~icext(C1,X)|~icext(C2,X)))))))&(iext(uri_owl_intersectionOf,Z,S1)|(((~ic(Z)|~ic(C1))|~ic(C2))|(?[X]: ((~icext(Z,X)|(~icext(C1,X)|~icext(C2,X)))&(icext(Z,X)|(icext(C1,X)&icext(C2,X)))))))))),
% 11.90/1.98 inference(NNF_transformation,[status(thm)],[f167])).
% 11.90/1.98 fof(f169,plain,(
% 11.90/1.98 ![S1,C1,C2]: ((![S2]: (((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_intersectionOf,Z,S1)|(((ic(Z)&ic(C1))&ic(C2))&((![X]: (~icext(Z,X)|(icext(C1,X)&icext(C2,X))))&(![X]: (icext(Z,X)|(~icext(C1,X)|~icext(C2,X))))))))&(![Z]: (iext(uri_owl_intersectionOf,Z,S1)|(((~ic(Z)|~ic(C1))|~ic(C2))|(?[X]: ((~icext(Z,X)|(~icext(C1,X)|~icext(C2,X)))&(icext(Z,X)|(icext(C1,X)&icext(C2,X))))))))))),
% 11.90/1.98 inference(miniscoping,[status(thm)],[f168])).
% 11.90/1.98 fof(f170,plain,(
% 11.90/1.98 ![S1,C1,C2]: ((![S2]: (((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_intersectionOf,Z,S1)|(((ic(Z)&ic(C1))&ic(C2))&((![X]: (~icext(Z,X)|(icext(C1,X)&icext(C2,X))))&(![X]: (icext(Z,X)|(~icext(C1,X)|~icext(C2,X))))))))&(![Z]: (iext(uri_owl_intersectionOf,Z,S1)|(((~ic(Z)|~ic(C1))|~ic(C2))|((~icext(Z,sK2_skl(Z,C2,C1,S1))|(~icext(C1,sK2_skl(Z,C2,C1,S1))|~icext(C2,sK2_skl(Z,C2,C1,S1))))&(icext(Z,sK2_skl(Z,C2,C1,S1))|(icext(C1,sK2_skl(Z,C2,C1,S1))&icext(C2,sK2_skl(Z,C2,C1,S1))))))))))),
% 11.90/1.98 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X,sK2_skl(Z,C2,C1,S1))],[f169])).
% 11.90/1.98 fof(f174,plain,(
% 11.90/1.98 ![X0,X1,X2,X3,X4,X5]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,X2)|~iext(uri_rdf_first,X2,X3)|~iext(uri_rdf_rest,X2,uri_rdf_nil)|~iext(uri_owl_intersectionOf,X4,X0)|~icext(X4,X5)|icext(X1,X5))),
% 11.90/1.98 inference(cnf_transformation,[status(thm)],[f170])).
% 11.90/1.98 fof(f175,plain,(
% 11.90/1.98 ![X0,X1,X2,X3,X4,X5]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,X2)|~iext(uri_rdf_first,X2,X3)|~iext(uri_rdf_rest,X2,uri_rdf_nil)|~iext(uri_owl_intersectionOf,X4,X0)|~icext(X4,X5)|icext(X3,X5))),
% 11.90/1.98 inference(cnf_transformation,[status(thm)],[f170])).
% 11.90/1.98 fof(f421,plain,(
% 11.90/1.98 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 11.90/1.98 inference(NNF_transformation,[status(thm)],[f80])).
% 11.90/1.98 fof(f422,plain,(
% 11.90/1.98 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 11.90/1.98 inference(miniscoping,[status(thm)],[f421])).
% 11.90/1.98 fof(f423,plain,(
% 11.90/1.98 ![X0,X1]: (~iext(uri_rdf_type,X0,X1)|icext(X1,X0))),
% 11.90/1.98 inference(cnf_transformation,[status(thm)],[f422])).
% 11.90/1.99 fof(f515,plain,(
% 11.90/1.99 ?[BNODE_y]: ((?[BNODE_l2]: (((?[BNODE_l1]: (((?[BNODE_x]: (((iext(uri_rdf_type,uri_ex_A,uri_owl_Class)&iext(uri_rdf_type,uri_ex_B,uri_owl_Class))&iext(uri_rdf_type,uri_ex_w,BNODE_x))&iext(uri_owl_intersectionOf,BNODE_x,BNODE_l1)))&iext(uri_rdf_first,BNODE_l1,uri_ex_A))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2)))&iext(uri_rdf_first,BNODE_l2,BNODE_y))&iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)))&iext(uri_owl_complementOf,BNODE_y,uri_ex_A))),
% 11.90/1.99 inference(miniscoping,[status(thm)],[f141])).
% 11.90/1.99 fof(f516,plain,(
% 11.90/1.99 ((((((((iext(uri_rdf_type,uri_ex_A,uri_owl_Class)&iext(uri_rdf_type,uri_ex_B,uri_owl_Class))&iext(uri_rdf_type,uri_ex_w,sK21_skl))&iext(uri_owl_intersectionOf,sK21_skl,sK20_skl))&iext(uri_rdf_first,sK20_skl,uri_ex_A))&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_owl_complementOf,sK18_skl,uri_ex_A))),
% 11.90/1.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl,sK21_skl]),skolemize(BNODE_y,sK18_skl),skolemize(BNODE_l2,sK19_skl),skolemize(BNODE_l1,sK20_skl),skolemize(BNODE_x,sK21_skl)],[f515])).
% 11.90/1.99 fof(f519,plain,(
% 11.90/1.99 iext(uri_rdf_type,uri_ex_w,sK21_skl)),
% 11.90/1.99 inference(cnf_transformation,[status(thm)],[f516])).
% 11.90/1.99 fof(f520,plain,(
% 11.90/1.99 iext(uri_owl_intersectionOf,sK21_skl,sK20_skl)),
% 11.90/1.99 inference(cnf_transformation,[status(thm)],[f516])).
% 11.90/1.99 fof(f521,plain,(
% 11.90/1.99 iext(uri_rdf_first,sK20_skl,uri_ex_A)),
% 11.90/1.99 inference(cnf_transformation,[status(thm)],[f516])).
% 11.90/1.99 fof(f522,plain,(
% 11.90/1.99 iext(uri_rdf_rest,sK20_skl,sK19_skl)),
% 11.90/1.99 inference(cnf_transformation,[status(thm)],[f516])).
% 11.90/1.99 fof(f523,plain,(
% 11.90/1.99 iext(uri_rdf_first,sK19_skl,sK18_skl)),
% 11.90/1.99 inference(cnf_transformation,[status(thm)],[f516])).
% 11.90/1.99 fof(f524,plain,(
% 11.90/1.99 iext(uri_rdf_rest,sK19_skl,uri_rdf_nil)),
% 11.90/1.99 inference(cnf_transformation,[status(thm)],[f516])).
% 11.90/1.99 fof(f525,plain,(
% 11.90/1.99 iext(uri_owl_complementOf,sK18_skl,uri_ex_A)),
% 11.90/1.99 inference(cnf_transformation,[status(thm)],[f516])).
% 11.90/1.99 fof(f538,plain,(
% 11.90/1.99 icext(sK21_skl,uri_ex_w)),
% 11.90/1.99 inference(resolution,[status(thm)],[f519,f423])).
% 11.90/1.99 fof(f578,plain,(
% 11.90/1.99 ![X0,X1,X2,X3,X4]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK19_skl)|~iext(uri_rdf_first,sK19_skl,X2)|~iext(uri_owl_intersectionOf,X3,X0)|~icext(X3,X4)|icext(X2,X4))),
% 11.90/1.99 inference(resolution,[status(thm)],[f524,f175])).
% 11.90/1.99 fof(f579,plain,(
% 11.90/1.99 ![X0,X1,X2,X3,X4]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK19_skl)|~iext(uri_rdf_first,sK19_skl,X2)|~iext(uri_owl_intersectionOf,X3,X0)|~icext(X3,X4)|icext(X1,X4))),
% 11.90/1.99 inference(resolution,[status(thm)],[f524,f174])).
% 11.90/1.99 fof(f591,plain,(
% 11.90/1.99 ![X0]: (~icext(sK18_skl,X0)|~icext(uri_ex_A,X0))),
% 11.90/1.99 inference(resolution,[status(thm)],[f525,f147])).
% 11.90/1.99 fof(f2252,plain,(
% 11.90/1.99 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK20_skl,X0)|~iext(uri_rdf_first,sK19_skl,X1)|~iext(uri_owl_intersectionOf,X2,sK20_skl)|~icext(X2,X3)|icext(X1,X3))),
% 11.90/1.99 inference(resolution,[status(thm)],[f578,f522])).
% 11.90/1.99 fof(f2253,plain,(
% 11.90/1.99 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK20_skl,X0)|~iext(uri_rdf_first,sK19_skl,X1)|~iext(uri_owl_intersectionOf,X2,sK20_skl)|~icext(X2,X3)|icext(X0,X3))),
% 2.92/2.02 inference(resolution,[status(thm)],[f579,f522])).
% 2.92/2.02 fof(f9144,plain,(
% 2.92/2.02 ![X0,X1,X2]: (~iext(uri_rdf_first,sK19_skl,X0)|~iext(uri_owl_intersectionOf,X1,sK20_skl)|~icext(X1,X2)|icext(X0,X2))),
% 2.92/2.02 inference(resolution,[status(thm)],[f2252,f521])).
% 2.92/2.02 fof(f9145,plain,(
% 2.92/2.02 ![X0,X1,X2]: (~iext(uri_rdf_first,sK19_skl,X0)|~iext(uri_owl_intersectionOf,X1,sK20_skl)|~icext(X1,X2)|icext(uri_ex_A,X2))),
% 2.92/2.02 inference(resolution,[status(thm)],[f2253,f521])).
% 2.92/2.02 fof(f9239,plain,(
% 2.92/2.02 ![X0,X1]: (~iext(uri_owl_intersectionOf,X0,sK20_skl)|~icext(X0,X1)|icext(sK18_skl,X1))),
% 2.92/2.02 inference(resolution,[status(thm)],[f9144,f523])).
% 2.92/2.02 fof(f9240,plain,(
% 2.92/2.02 ![X0]: (~icext(sK21_skl,X0)|icext(sK18_skl,X0))),
% 2.92/2.02 inference(resolution,[status(thm)],[f9239,f520])).
% 2.92/2.02 fof(f9242,plain,(
% 2.92/2.02 icext(sK18_skl,uri_ex_w)),
% 2.92/2.02 inference(resolution,[status(thm)],[f9240,f538])).
% 2.92/2.02 fof(f9335,plain,(
% 2.92/2.02 ![X0,X1]: (~iext(uri_owl_intersectionOf,X0,sK20_skl)|~icext(X0,X1)|icext(uri_ex_A,X1))),
% 2.92/2.02 inference(resolution,[status(thm)],[f9145,f523])).
% 2.92/2.02 fof(f9336,plain,(
% 2.92/2.02 ![X0]: (~icext(sK21_skl,X0)|icext(uri_ex_A,X0))),
% 2.92/2.02 inference(resolution,[status(thm)],[f9335,f520])).
% 2.92/2.02 fof(f9338,plain,(
% 2.92/2.02 icext(uri_ex_A,uri_ex_w)),
% 2.92/2.02 inference(resolution,[status(thm)],[f9336,f538])).
% 2.92/2.02 fof(f9411,plain,(
% 2.92/2.02 ~icext(sK18_skl,uri_ex_w)),
% 2.92/2.02 inference(resolution,[status(thm)],[f9338,f591])).
% 2.92/2.02 fof(f9427,plain,(
% 2.92/2.02 $false),
% 2.92/2.02 inference(forward_subsumption_resolution,[status(thm)],[f9411,f9242])).
% 2.92/2.02 % SZS output end CNFRefutation for theBenchmark.p
% 2.92/2.02 % Elapsed time: 1.652772 seconds
% 2.92/2.02 % CPU time: 12.781020 seconds
% 2.92/2.02 % Total memory used: 145.413 MB
% 2.92/2.02 % Net memory used: 138.274 MB
%------------------------------------------------------------------------------