%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET658+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:24 PM UTC 2026
% Result : Theorem 0.09s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET658+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.56 % Computer : n017.cluster.edu
% 0.09/0.56 % Model : x86_64 x86_64
% 0.09/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.56 % Memory : 8046.5625MB
% 0.09/0.56 % OS : Linux 6.8.0-71-generic
% 0.09/0.56 % CPULimit : 300
% 0.09/0.56 % WCLimit : 300
% 0.09/0.56 % DateTime : Mon Sep 21 05:26:27 UTC 2026
% 0.09/0.56 % CPUTime :
% 0.09/0.57 % Drodi V4.1.1
% 0.09/0.60 % Refutation found
% 0.09/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.60 fof(f1,axiom,(
% 0.09/0.60 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,binary_relation_type)=> ( subset(domain_of(C),B)=> ilf_type(C,relation_type(B,range_of(C))) ) ) )) )),
% 0.09/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f15,axiom,(
% 0.09/0.60 (! [B] :( ilf_type(B,set_type)=> subset(B,B) ) )),
% 0.09/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f28,axiom,(
% 0.09/0.60 (! [B] : ilf_type(B,set_type) )),
% 0.09/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f29,conjecture,(
% 0.09/0.60 (! [B] :( ilf_type(B,binary_relation_type)=> ilf_type(B,relation_type(domain_of(B),range_of(B))) ) )),
% 0.09/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.60 fof(f30,negated_conjecture,(
% 0.09/0.60 ~((! [B] :( ilf_type(B,binary_relation_type)=> ilf_type(B,relation_type(domain_of(B),range_of(B))) ) ))),
% 0.09/0.60 inference(negated_conjecture,[status(cth)],[f29])).
% 0.09/0.60 fof(f31,plain,(
% 0.09/0.60 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,binary_relation_type)|(~subset(domain_of(C),B)|ilf_type(C,relation_type(B,range_of(C)))))))),
% 0.09/0.60 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.09/0.60 fof(f32,plain,(
% 0.09/0.60 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X1,binary_relation_type)|~subset(domain_of(X1),X0)|ilf_type(X1,relation_type(X0,range_of(X1))))),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f31])).
% 0.09/0.60 fof(f80,plain,(
% 0.09/0.60 ![B]: (~ilf_type(B,set_type)|subset(B,B))),
% 0.09/0.60 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.09/0.60 fof(f81,plain,(
% 0.09/0.60 ![X0]: (~ilf_type(X0,set_type)|subset(X0,X0))),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.09/0.60 fof(f126,plain,(
% 0.09/0.60 ![X0]: (ilf_type(X0,set_type))),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f28])).
% 0.09/0.60 fof(f127,plain,(
% 0.09/0.60 (?[B]: (ilf_type(B,binary_relation_type)&~ilf_type(B,relation_type(domain_of(B),range_of(B)))))),
% 0.09/0.60 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.09/0.60 fof(f128,plain,(
% 0.09/0.60 (ilf_type(sK12_skl,binary_relation_type)&~ilf_type(sK12_skl,relation_type(domain_of(sK12_skl),range_of(sK12_skl))))),
% 0.09/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(B,sK12_skl)],[f127])).
% 0.09/0.60 fof(f129,plain,(
% 0.09/0.60 ilf_type(sK12_skl,binary_relation_type)),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f128])).
% 0.09/0.60 fof(f130,plain,(
% 0.09/0.60 ~ilf_type(sK12_skl,relation_type(domain_of(sK12_skl),range_of(sK12_skl)))),
% 0.09/0.60 inference(cnf_transformation,[status(thm)],[f128])).
% 0.09/0.60 fof(f137,plain,(
% 0.09/0.60 ![X0]: (subset(X0,X0))),
% 0.09/0.60 inference(forward_subsumption_resolution,[status(thm)],[f81,f126])).
% 0.09/0.60 fof(f138,plain,(
% 0.09/0.60 ![X0,X1]: (~ilf_type(X0,binary_relation_type)|~subset(domain_of(X0),X1)|ilf_type(X0,relation_type(X1,range_of(X0))))),
% 0.09/0.60 inference(forward_subsumption_resolution,[status(thm)],[f32,f126])).
% 0.09/0.60 fof(f140,plain,(
% 0.09/0.60 ~ilf_type(sK12_skl,binary_relation_type)|~subset(domain_of(sK12_skl),domain_of(sK12_skl))),
% 0.09/0.60 inference(resolution,[status(thm)],[f138,f130])).
% 0.09/0.60 fof(f141,plain,(
% 0.09/0.60 ~subset(domain_of(sK12_skl),domain_of(sK12_skl))),
% 0.09/0.60 inference(forward_subsumption_resolution,[status(thm)],[f140,f129])).
% 0.09/0.60 fof(f145,plain,(
% 0.09/0.60 $false),
% 0.09/0.60 inference(forward_subsumption_resolution,[status(thm)],[f141,f137])).
% 0.09/0.60 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.61 % Elapsed time: 0.046880 seconds
% 0.09/0.61 % CPU time: 0.142732 seconds
% 0.09/0.61 % Total memory used: 46.887 MB
% 0.09/0.61 % Net memory used: 46.769 MB
%------------------------------------------------------------------------------