%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET664+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 : n009.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.14s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET664+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.10/0.35 % Computer : n009.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 05:31:57 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.14/0.39 % Refutation found
% 0.14/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.39 fof(f1,axiom,(
% 0.14/0.39 (! [B] :( ilf_type(B,set_type)=> ( subset(B,empty_set)=> B = empty_set ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f2,axiom,(
% 0.14/0.39 (! [B] :( ilf_type(B,binary_relation_type)=> ( ( domain_of(B) = empty_set| range_of(B) = empty_set )=> B = empty_set ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f3,axiom,(
% 0.14/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.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f7,axiom,(
% 0.14/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.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f14,axiom,(
% 0.14/0.39 (! [B] :( ilf_type(B,set_type)=> ( ilf_type(B,binary_relation_type)<=> ( relation_like(B)& ilf_type(B,set_type) ) ) ) )),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f29,axiom,(
% 0.14/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.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f34,axiom,(
% 0.14/0.39 (! [B] : ilf_type(B,set_type) )),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f35,conjecture,(
% 0.14/0.39 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,relation_type(C,B))=> ( ilf_type(D,relation_type(C,empty_set))=> D = empty_set ) ) )) )) )),
% 0.14/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.39 fof(f36,negated_conjecture,(
% 0.14/0.39 ~((! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,relation_type(C,B))=> ( ilf_type(D,relation_type(C,empty_set))=> D = empty_set ) ) )) )) ))),
% 0.14/0.39 inference(negated_conjecture,[status(cth)],[f35])).
% 0.14/0.39 fof(f37,plain,(
% 0.14/0.39 ![B]: (~ilf_type(B,set_type)|(~subset(B,empty_set)|B=empty_set))),
% 0.14/0.39 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.14/0.39 fof(f38,plain,(
% 0.14/0.39 ![X0]: (~ilf_type(X0,set_type)|~subset(X0,empty_set)|X0=empty_set)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f37])).
% 0.14/0.39 fof(f39,plain,(
% 0.14/0.39 ![B]: (~ilf_type(B,binary_relation_type)|((~domain_of(B)=empty_set&~range_of(B)=empty_set)|B=empty_set))),
% 0.14/0.39 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/0.39 fof(f41,plain,(
% 0.14/0.39 ![X0]: (~ilf_type(X0,binary_relation_type)|~range_of(X0)=empty_set|X0=empty_set)),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f39])).
% 0.14/0.39 fof(f42,plain,(
% 0.14/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.14/0.39 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.14/0.39 fof(f44,plain,(
% 0.14/0.39 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X0,X1))|subset(range_of(X2),X1))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.14/0.39 fof(f49,plain,(
% 0.14/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.14/0.39 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.14/0.39 fof(f51,plain,(
% 0.14/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.14/0.39 inference(cnf_transformation,[status(thm)],[f49])).
% 0.14/0.39 fof(f72,plain,(
% 0.14/0.39 ![B]: (~ilf_type(B,set_type)|(ilf_type(B,binary_relation_type)<=>(relation_like(B)&ilf_type(B,set_type))))),
% 0.14/0.39 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.14/0.39 fof(f73,plain,(
% 0.14/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.14/0.39 inference(NNF_transformation,[status(thm)],[f72])).
% 0.14/0.39 fof(f76,plain,(
% 0.14/0.39 ![X0]: (~ilf_type(X0,set_type)|ilf_type(X0,binary_relation_type)|~relation_like(X0)|~ilf_type(X0,set_type))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/0.39 fof(f133,plain,(
% 0.14/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.14/0.39 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.14/0.39 fof(f134,plain,(
% 0.14/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.14/0.39 inference(cnf_transformation,[status(thm)],[f133])).
% 0.14/0.39 fof(f143,plain,(
% 0.14/0.39 ![X0]: (ilf_type(X0,set_type))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f34])).
% 0.14/0.39 fof(f144,plain,(
% 0.14/0.39 (?[B]: (ilf_type(B,set_type)&(?[C]: (ilf_type(C,set_type)&(?[D]: (ilf_type(D,relation_type(C,B))&(ilf_type(D,relation_type(C,empty_set))&~D=empty_set)))))))),
% 0.14/0.39 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.14/0.39 fof(f145,plain,(
% 0.14/0.39 (ilf_type(sK12_skl,set_type)&(ilf_type(sK13_skl,set_type)&(ilf_type(sK14_skl,relation_type(sK13_skl,sK12_skl))&(ilf_type(sK14_skl,relation_type(sK13_skl,empty_set))&~sK14_skl=empty_set))))),
% 0.14/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.14/0.39 fof(f149,plain,(
% 0.14/0.39 ilf_type(sK14_skl,relation_type(sK13_skl,empty_set))),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f145])).
% 0.14/0.39 fof(f150,plain,(
% 0.14/0.39 ~sK14_skl=empty_set),
% 0.14/0.39 inference(cnf_transformation,[status(thm)],[f145])).
% 0.14/0.39 fof(f151,plain,(
% 0.14/0.39 ![X0]: (~ilf_type(X0,set_type)|ilf_type(X0,binary_relation_type)|~relation_like(X0))),
% 0.14/0.39 inference(duplicate_literals_removal,[status(thm)],[f76])).
% 0.14/0.39 fof(f157,plain,(
% 0.14/0.39 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,subset_type(cross_product(X0,X2)))|relation_like(X1))),
% 0.14/0.39 inference(backward_subsumption_resolution,[status(thm)],[f134,f143])).
% 0.14/0.39 fof(f178,plain,(
% 0.14/0.39 ![X0]: (ilf_type(X0,binary_relation_type)|~relation_like(X0))),
% 0.14/0.39 inference(backward_subsumption_resolution,[status(thm)],[f151,f143])).
% 0.14/0.39 fof(f181,plain,(
% 0.14/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.14/0.39 inference(backward_subsumption_resolution,[status(thm)],[f51,f143])).
% 0.14/0.39 fof(f184,plain,(
% 0.14/0.39 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X0,X2))|subset(range_of(X1),X2))),
% 0.14/0.39 inference(backward_subsumption_resolution,[status(thm)],[f44,f143])).
% 0.14/0.39 fof(f186,plain,(
% 0.14/0.39 ![X0]: (~subset(X0,empty_set)|X0=empty_set)),
% 0.14/0.39 inference(backward_subsumption_resolution,[status(thm)],[f38,f143])).
% 0.14/0.39 fof(f191,plain,(
% 0.14/0.39 ![X0,X1,X2]: (~ilf_type(X0,subset_type(cross_product(X1,X2)))|relation_like(X0))),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f157,f143])).
% 0.14/0.39 fof(f206,plain,(
% 0.14/0.39 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|ilf_type(X0,subset_type(cross_product(X1,X2))))),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f181,f143])).
% 0.14/0.39 fof(f208,plain,(
% 0.14/0.39 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|subset(range_of(X0),X2))),
% 0.14/0.39 inference(forward_subsumption_resolution,[status(thm)],[f184,f143])).
% 0.14/0.39 fof(f366,plain,(
% 0.14/0.39 ilf_type(sK14_skl,subset_type(cross_product(sK13_skl,empty_set)))),
% 0.14/0.39 inference(resolution,[status(thm)],[f206,f149])).
% 0.14/0.39 fof(f370,plain,(
% 0.14/0.39 subset(range_of(sK14_skl),empty_set)),
% 0.14/0.39 inference(resolution,[status(thm)],[f208,f149])).
% 0.14/0.39 fof(f392,plain,(
% 0.14/0.39 range_of(sK14_skl)=empty_set),
% 0.14/0.39 inference(resolution,[status(thm)],[f370,f186])).
% 0.14/0.39 fof(f407,plain,(
% 0.14/0.39 relation_like(sK14_skl)),
% 0.14/0.39 inference(resolution,[status(thm)],[f366,f191])).
% 0.14/0.39 fof(f412,plain,(
% 0.14/0.39 ilf_type(sK14_skl,binary_relation_type)),
% 0.14/0.39 inference(resolution,[status(thm)],[f407,f178])).
% 0.14/0.39 fof(f449,plain,(
% 0.14/0.39 ~range_of(sK14_skl)=empty_set|sK14_skl=empty_set),
% 0.14/0.39 inference(resolution,[status(thm)],[f412,f41])).
% 0.14/0.39 fof(f455,definition,(
% 0.14/0.39 sQ12_spl <=> (sK14_skl=empty_set)),
% 0.14/0.39 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.39 fof(f456,plain,(
% 0.14/0.39 sK14_skl=empty_set|~sQ12_spl),
% 0.14/0.39 inference(component_clause,[status(thm)],[f455])).
% 0.14/0.40 fof(f459,definition,(
% 0.14/0.40 sQ13_spl <=> (range_of(sK14_skl)=empty_set)),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f461,plain,(
% 0.14/0.40 ~range_of(sK14_skl)=empty_set|sQ13_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f459])).
% 0.14/0.40 fof(f462,plain,(
% 0.14/0.40 ~sQ13_spl|sQ12_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f449,f459,f455])).
% 0.14/0.40 fof(f463,plain,(
% 0.14/0.40 $false|~sQ12_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f456,f150])).
% 0.14/0.40 fof(f464,plain,(
% 0.14/0.40 ~sQ12_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f463])).
% 0.14/0.40 fof(f465,plain,(
% 0.14/0.40 ~empty_set=empty_set|sQ13_spl),
% 0.14/0.40 inference(forward_demodulation,[status(thm)],[f392,f461])).
% 0.14/0.40 fof(f466,plain,(
% 0.14/0.40 $false|sQ13_spl),
% 0.14/0.40 inference(trivial_equality_resolution,[status(thm)],[f465])).
% 0.14/0.40 fof(f467,plain,(
% 0.14/0.40 sQ13_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f466])).
% 0.14/0.40 fof(f468,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(sat_refutation,[status(thm)],[f462,f464,f467])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.42 % Elapsed time: 0.053176 seconds
% 0.14/0.42 % CPU time: 0.167048 seconds
% 0.14/0.42 % Total memory used: 65.154 MB
% 0.14/0.42 % Net memory used: 65.061 MB
%------------------------------------------------------------------------------