%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET663+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:12:25 PM UTC 2026
% Result : Theorem 0.09s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET663+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 05:33:58 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.39 % Refutation found
% 0.09/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.39 fof(f1,axiom,(
% 0.09/0.39 (! [B] :( ilf_type(B,set_type)=> ( subset(B,empty_set)=> B = empty_set ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f2,axiom,(
% 0.09/0.39 (! [B] :( ilf_type(B,binary_relation_type)=> ( ( domain_of(B) = empty_set| range_of(B) = empty_set )=> B = empty_set ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f3,axiom,(
% 0.09/0.39 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,relation_type(B,C))=> ( subset(domain_of(D),B)& subset(range_of(D),C) ) ) )) )) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f7,axiom,(
% 0.09/0.39 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> ( (! [D] :( ilf_type(D,subset_type(cross_product(B,C)))=> ilf_type(D,relation_type(B,C)) ))& (! [E] :( ilf_type(E,relation_type(B,C))=> ilf_type(E,subset_type(cross_product(B,C))) ) )) ) )) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f14,axiom,(
% 0.09/0.39 (! [B] :( ilf_type(B,set_type)=> ( ilf_type(B,binary_relation_type)<=> ( relation_like(B)& ilf_type(B,set_type) ) ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f29,axiom,(
% 0.09/0.39 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,subset_type(cross_product(B,C)))=> relation_like(D) ) )) )) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f34,axiom,(
% 0.09/0.39 (! [B] : ilf_type(B,set_type) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f35,conjecture,(
% 0.09/0.39 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,relation_type(B,C))=> ( ilf_type(D,relation_type(empty_set,C))=> D = empty_set ) ) )) )) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f36,negated_conjecture,(
% 0.09/0.39 ~((! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,relation_type(B,C))=> ( ilf_type(D,relation_type(empty_set,C))=> D = empty_set ) ) )) )) ))),
% 0.09/0.39 inference(negated_conjecture,[status(cth)],[f35])).
% 0.09/0.39 fof(f37,plain,(
% 0.09/0.39 ![B]: (~ilf_type(B,set_type)|(~subset(B,empty_set)|B=empty_set))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.09/0.39 fof(f38,plain,(
% 0.09/0.39 ![X0]: (~ilf_type(X0,set_type)|~subset(X0,empty_set)|X0=empty_set)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f37])).
% 0.09/0.39 fof(f39,plain,(
% 0.09/0.39 ![B]: (~ilf_type(B,binary_relation_type)|((~domain_of(B)=empty_set&~range_of(B)=empty_set)|B=empty_set))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.09/0.39 fof(f40,plain,(
% 0.09/0.39 ![X0]: (~ilf_type(X0,binary_relation_type)|~domain_of(X0)=empty_set|X0=empty_set)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f39])).
% 0.09/0.39 fof(f42,plain,(
% 0.09/0.39 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,relation_type(B,C))|(subset(domain_of(D),B)&subset(range_of(D),C)))))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.09/0.39 fof(f43,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X0,X1))|subset(domain_of(X2),X0))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.39 fof(f49,plain,(
% 0.09/0.39 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|((![D]: (~ilf_type(D,subset_type(cross_product(B,C)))|ilf_type(D,relation_type(B,C))))&(![E]: (~ilf_type(E,relation_type(B,C))|ilf_type(E,subset_type(cross_product(B,C)))))))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.09/0.39 fof(f51,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X0,X1))|ilf_type(X2,subset_type(cross_product(X0,X1))))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f49])).
% 0.09/0.39 fof(f72,plain,(
% 0.09/0.39 ![B]: (~ilf_type(B,set_type)|(ilf_type(B,binary_relation_type)<=>(relation_like(B)&ilf_type(B,set_type))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.09/0.39 fof(f73,plain,(
% 0.09/0.39 ![B]: (~ilf_type(B,set_type)|((~ilf_type(B,binary_relation_type)|(relation_like(B)&ilf_type(B,set_type)))&(ilf_type(B,binary_relation_type)|(~relation_like(B)|~ilf_type(B,set_type)))))),
% 0.09/0.39 inference(NNF_transformation,[status(thm)],[f72])).
% 0.09/0.39 fof(f76,plain,(
% 0.09/0.39 ![X0]: (~ilf_type(X0,set_type)|ilf_type(X0,binary_relation_type)|~relation_like(X0)|~ilf_type(X0,set_type))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f73])).
% 0.09/0.39 fof(f133,plain,(
% 0.09/0.39 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,subset_type(cross_product(B,C)))|relation_like(D))))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.09/0.39 fof(f134,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,subset_type(cross_product(X0,X1)))|relation_like(X2))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f133])).
% 0.09/0.39 fof(f143,plain,(
% 0.09/0.39 ![X0]: (ilf_type(X0,set_type))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f34])).
% 0.09/0.39 fof(f144,plain,(
% 0.09/0.39 (?[B]: (ilf_type(B,set_type)&(?[C]: (ilf_type(C,set_type)&(?[D]: (ilf_type(D,relation_type(B,C))&(ilf_type(D,relation_type(empty_set,C))&~D=empty_set)))))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.09/0.39 fof(f145,plain,(
% 0.09/0.39 (ilf_type(sK12_skl,set_type)&(ilf_type(sK13_skl,set_type)&(ilf_type(sK14_skl,relation_type(sK12_skl,sK13_skl))&(ilf_type(sK14_skl,relation_type(empty_set,sK13_skl))&~sK14_skl=empty_set))))),
% 0.09/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(B,sK12_skl),skolemize(C,sK13_skl),skolemize(D,sK14_skl)],[f144])).
% 0.09/0.39 fof(f149,plain,(
% 0.09/0.39 ilf_type(sK14_skl,relation_type(empty_set,sK13_skl))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f145])).
% 0.09/0.39 fof(f150,plain,(
% 0.09/0.39 ~sK14_skl=empty_set),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f145])).
% 0.09/0.39 fof(f151,plain,(
% 0.09/0.39 ![X0]: (~ilf_type(X0,set_type)|ilf_type(X0,binary_relation_type)|~relation_like(X0))),
% 0.09/0.39 inference(duplicate_literals_removal,[status(thm)],[f76])).
% 0.09/0.39 fof(f157,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,subset_type(cross_product(X0,X2)))|relation_like(X1))),
% 0.09/0.39 inference(backward_subsumption_resolution,[status(thm)],[f134,f143])).
% 0.09/0.39 fof(f178,plain,(
% 0.09/0.39 ![X0]: (ilf_type(X0,binary_relation_type)|~relation_like(X0))),
% 0.09/0.39 inference(backward_subsumption_resolution,[status(thm)],[f151,f143])).
% 0.09/0.39 fof(f181,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X0,X2))|ilf_type(X1,subset_type(cross_product(X0,X2))))),
% 0.09/0.39 inference(backward_subsumption_resolution,[status(thm)],[f51,f143])).
% 0.09/0.39 fof(f185,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X0,X2))|subset(domain_of(X1),X0))),
% 0.09/0.39 inference(backward_subsumption_resolution,[status(thm)],[f43,f143])).
% 0.09/0.39 fof(f186,plain,(
% 0.09/0.39 ![X0]: (~subset(X0,empty_set)|X0=empty_set)),
% 0.09/0.39 inference(backward_subsumption_resolution,[status(thm)],[f38,f143])).
% 0.09/0.39 fof(f191,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ilf_type(X0,subset_type(cross_product(X1,X2)))|relation_like(X0))),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f157,f143])).
% 0.09/0.39 fof(f206,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|ilf_type(X0,subset_type(cross_product(X1,X2))))),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f181,f143])).
% 0.09/0.39 fof(f209,plain,(
% 0.09/0.39 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|subset(domain_of(X0),X1))),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f185,f143])).
% 0.09/0.39 fof(f366,plain,(
% 0.09/0.39 ilf_type(sK14_skl,subset_type(cross_product(empty_set,sK13_skl)))),
% 0.09/0.39 inference(resolution,[status(thm)],[f206,f149])).
% 0.09/0.39 fof(f373,plain,(
% 0.09/0.39 subset(domain_of(sK14_skl),empty_set)),
% 0.09/0.39 inference(resolution,[status(thm)],[f209,f149])).
% 0.09/0.39 fof(f403,plain,(
% 0.09/0.39 relation_like(sK14_skl)),
% 0.09/0.39 inference(resolution,[status(thm)],[f366,f191])).
% 0.09/0.39 fof(f405,plain,(
% 0.09/0.39 ilf_type(sK14_skl,binary_relation_type)),
% 0.09/0.39 inference(resolution,[status(thm)],[f403,f178])).
% 0.09/0.39 fof(f441,plain,(
% 0.09/0.39 ~domain_of(sK14_skl)=empty_set|sK14_skl=empty_set),
% 0.09/0.39 inference(resolution,[status(thm)],[f405,f40])).
% 0.09/0.39 fof(f445,definition,(
% 0.09/0.39 sQ12_spl <=> (domain_of(sK14_skl)=empty_set)),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.09/0.39 fof(f447,plain,(
% 0.09/0.39 ~domain_of(sK14_skl)=empty_set|sQ12_spl),
% 0.09/0.39 inference(component_clause,[status(thm)],[f445])).
% 0.09/0.39 fof(f448,definition,(
% 0.09/0.39 sQ13_spl <=> (sK14_skl=empty_set)),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f449,plain,(
% 0.09/0.40 sK14_skl=empty_set|~sQ13_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f448])).
% 0.09/0.40 fof(f451,plain,(
% 0.09/0.40 ~sQ12_spl|sQ13_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f441,f445,f448])).
% 0.09/0.40 fof(f456,plain,(
% 0.09/0.40 $false|~sQ13_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f449,f150])).
% 0.09/0.40 fof(f457,plain,(
% 0.09/0.40 ~sQ13_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f456])).
% 0.09/0.40 fof(f513,plain,(
% 0.09/0.40 domain_of(sK14_skl)=empty_set),
% 0.09/0.40 inference(resolution,[status(thm)],[f373,f186])).
% 0.09/0.40 fof(f515,plain,(
% 0.09/0.40 $false|sQ12_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f513,f447])).
% 0.09/0.40 fof(f516,plain,(
% 0.09/0.40 sQ12_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f515])).
% 0.09/0.40 fof(f517,plain,(
% 0.09/0.40 $false),
% 0.09/0.40 inference(sat_refutation,[status(thm)],[f451,f457,f516])).
% 0.09/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.42 % Elapsed time: 0.055739 seconds
% 0.09/0.42 % CPU time: 0.216164 seconds
% 0.09/0.42 % Total memory used: 84.420 MB
% 0.09/0.42 % Net memory used: 84.248 MB
%------------------------------------------------------------------------------