%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET677+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 : n014.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:26 PM UTC 2026
% Result : Theorem 0.12s 0.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET677+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n014.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 05:32:19 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.12/0.36 % Refutation found
% 0.12/0.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.36 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.36 fof(f1,axiom,(
% 0.12/0.36 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,relation_type(C,B))=> ( subset(identity_relation_of(C),D)=> ( C = domain(C,B,D)& subset(C,range(C,B,D)) ) ) ) )) )) )),
% 0.12/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.36 fof(f2,axiom,(
% 0.12/0.36 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,relation_type(B,C))=> ( subset(identity_relation_of(C),D)=> ( subset(C,domain(B,C,D))& C = range(B,C,D) ) ) ) )) )) )),
% 0.12/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.36 fof(f5,axiom,(
% 0.12/0.36 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> ( ilf_type(C,identity_relation_of_type(B))<=> ilf_type(C,relation_type(B,B)) ) ) )) )),
% 0.12/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.36 fof(f34,axiom,(
% 0.12/0.36 (! [B] : ilf_type(B,set_type) )),
% 0.12/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.36 fof(f35,conjecture,(
% 0.12/0.36 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,identity_relation_of_type(B))=> ( subset(identity_relation_of(B),C)=> ( B = domain(B,B,C)& B = range(B,B,C) ) ) ) )) )),
% 0.12/0.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.36 fof(f36,negated_conjecture,(
% 0.12/0.36 ~((! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,identity_relation_of_type(B))=> ( subset(identity_relation_of(B),C)=> ( B = domain(B,B,C)& B = range(B,B,C) ) ) ) )) ))),
% 0.12/0.36 inference(negated_conjecture,[status(cth)],[f35])).
% 0.12/0.36 fof(f37,plain,(
% 0.12/0.36 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,relation_type(C,B))|(~subset(identity_relation_of(C),D)|(C=domain(C,B,D)&subset(C,range(C,B,D)))))))))),
% 0.12/0.36 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.12/0.36 fof(f38,plain,(
% 0.12/0.36 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X1,X0))|~subset(identity_relation_of(X1),X2)|X1=domain(X1,X0,X2))),
% 0.12/0.36 inference(cnf_transformation,[status(thm)],[f37])).
% 0.12/0.36 fof(f40,plain,(
% 0.12/0.36 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,relation_type(B,C))|(~subset(identity_relation_of(C),D)|(subset(C,domain(B,C,D))&C=range(B,C,D))))))))),
% 0.12/0.36 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.12/0.36 fof(f42,plain,(
% 0.12/0.36 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X0,X1))|~subset(identity_relation_of(X1),X2)|X1=range(X0,X1,X2))),
% 0.12/0.36 inference(cnf_transformation,[status(thm)],[f40])).
% 0.12/0.36 fof(f50,plain,(
% 0.12/0.36 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(ilf_type(C,identity_relation_of_type(B))<=>ilf_type(C,relation_type(B,B))))))),
% 0.12/0.36 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.12/0.36 fof(f51,plain,(
% 0.12/0.36 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|((~ilf_type(C,identity_relation_of_type(B))|ilf_type(C,relation_type(B,B)))&(ilf_type(C,identity_relation_of_type(B))|~ilf_type(C,relation_type(B,B)))))))),
% 0.12/0.36 inference(NNF_transformation,[status(thm)],[f50])).
% 0.12/0.36 fof(f52,plain,(
% 0.12/0.36 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X1,identity_relation_of_type(X0))|ilf_type(X1,relation_type(X0,X0)))),
% 0.12/0.36 inference(cnf_transformation,[status(thm)],[f51])).
% 0.12/0.36 fof(f153,plain,(
% 0.12/0.36 ![X0]: (ilf_type(X0,set_type))),
% 0.12/0.36 inference(cnf_transformation,[status(thm)],[f34])).
% 0.12/0.36 fof(f154,plain,(
% 0.12/0.36 (?[B]: (ilf_type(B,set_type)&(?[C]: (ilf_type(C,identity_relation_of_type(B))&(subset(identity_relation_of(B),C)&(~B=domain(B,B,C)|~B=range(B,B,C)))))))),
% 0.12/0.36 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.12/0.36 fof(f155,plain,(
% 0.12/0.36 (ilf_type(sK13_skl,set_type)&(ilf_type(sK14_skl,identity_relation_of_type(sK13_skl))&(subset(identity_relation_of(sK13_skl),sK14_skl)&(~sK13_skl=domain(sK13_skl,sK13_skl,sK14_skl)|~sK13_skl=range(sK13_skl,sK13_skl,sK14_skl)))))),
% 0.12/0.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(B,sK13_skl),skolemize(C,sK14_skl)],[f154])).
% 0.12/0.36 fof(f157,plain,(
% 0.12/0.36 ilf_type(sK14_skl,identity_relation_of_type(sK13_skl))),
% 0.12/0.36 inference(cnf_transformation,[status(thm)],[f155])).
% 0.12/0.37 fof(f158,plain,(
% 0.12/0.37 subset(identity_relation_of(sK13_skl),sK14_skl)),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f155])).
% 0.12/0.37 fof(f159,plain,(
% 0.12/0.37 ~sK13_skl=domain(sK13_skl,sK13_skl,sK14_skl)|~sK13_skl=range(sK13_skl,sK13_skl,sK14_skl)),
% 0.12/0.37 inference(cnf_transformation,[status(thm)],[f155])).
% 0.12/0.37 fof(f168,plain,(
% 0.12/0.37 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X0,X2))|~subset(identity_relation_of(X0),X1)|X0=domain(X0,X2,X1))),
% 0.12/0.37 inference(forward_subsumption_resolution,[status(thm)],[f38,f153])).
% 0.12/0.37 fof(f171,plain,(
% 0.12/0.37 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X2,X0))|~subset(identity_relation_of(X0),X1)|X0=range(X2,X0,X1))),
% 0.12/0.37 inference(forward_subsumption_resolution,[status(thm)],[f42,f153])).
% 0.12/0.37 fof(f176,plain,(
% 0.12/0.37 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X0,identity_relation_of_type(X1))|ilf_type(X0,relation_type(X1,X1)))),
% 0.12/0.37 inference(forward_subsumption_resolution,[status(thm)],[f52,f153])).
% 0.12/0.37 fof(f177,plain,(
% 0.12/0.37 ~ilf_type(sK14_skl,set_type)|ilf_type(sK14_skl,relation_type(sK13_skl,sK13_skl))),
% 0.12/0.37 inference(resolution,[status(thm)],[f176,f157])).
% 0.12/0.37 fof(f178,plain,(
% 0.12/0.37 ilf_type(sK14_skl,relation_type(sK13_skl,sK13_skl))),
% 0.12/0.37 inference(forward_subsumption_resolution,[status(thm)],[f177,f153])).
% 0.12/0.37 fof(f181,plain,(
% 0.12/0.37 ~ilf_type(sK13_skl,set_type)|~subset(identity_relation_of(sK13_skl),sK14_skl)|sK13_skl=range(sK13_skl,sK13_skl,sK14_skl)),
% 0.12/0.37 inference(resolution,[status(thm)],[f178,f171])).
% 0.12/0.37 fof(f184,plain,(
% 0.12/0.37 ~ilf_type(sK13_skl,set_type)|~subset(identity_relation_of(sK13_skl),sK14_skl)|sK13_skl=domain(sK13_skl,sK13_skl,sK14_skl)),
% 0.12/0.37 inference(resolution,[status(thm)],[f178,f168])).
% 0.12/0.37 fof(f185,plain,(
% 0.12/0.37 ~subset(identity_relation_of(sK13_skl),sK14_skl)|sK13_skl=range(sK13_skl,sK13_skl,sK14_skl)),
% 0.12/0.37 inference(forward_subsumption_resolution,[status(thm)],[f181,f153])).
% 0.12/0.37 fof(f188,plain,(
% 0.12/0.37 ~subset(identity_relation_of(sK13_skl),sK14_skl)|sK13_skl=domain(sK13_skl,sK13_skl,sK14_skl)),
% 0.12/0.37 inference(forward_subsumption_resolution,[status(thm)],[f184,f153])).
% 0.12/0.37 fof(f189,plain,(
% 0.12/0.37 ~sK13_skl=domain(sK13_skl,sK13_skl,sK14_skl)|~sK13_skl=sK13_skl),
% 0.12/0.37 inference(backward_demodulation,[status(thm)],[f190,f159])).
% 0.12/0.37 fof(f190,plain,(
% 0.12/0.37 sK13_skl=range(sK13_skl,sK13_skl,sK14_skl)),
% 0.12/0.37 inference(forward_subsumption_resolution,[status(thm)],[f185,f158])).
% 0.12/0.37 fof(f191,plain,(
% 0.12/0.37 ~sK13_skl=domain(sK13_skl,sK13_skl,sK14_skl)),
% 0.12/0.37 inference(trivial_equality_resolution,[status(thm)],[f189])).
% 0.12/0.37 fof(f192,plain,(
% 0.12/0.37 ~sK13_skl=sK13_skl),
% 0.12/0.37 inference(backward_demodulation,[status(thm)],[f193,f191])).
% 0.12/0.37 fof(f193,plain,(
% 0.12/0.37 sK13_skl=domain(sK13_skl,sK13_skl,sK14_skl)),
% 0.12/0.37 inference(forward_subsumption_resolution,[status(thm)],[f188,f158])).
% 0.12/0.37 fof(f194,plain,(
% 0.12/0.37 $false),
% 0.12/0.37 inference(trivial_equality_resolution,[status(thm)],[f192])).
% 0.12/0.37 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.40 % Elapsed time: 0.043221 seconds
% 0.12/0.40 % CPU time: 0.071138 seconds
% 0.12/0.40 % Total memory used: 7.820 MB
% 0.12/0.40 % Net memory used: 7.810 MB
%------------------------------------------------------------------------------