%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET667+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 : n013.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.13s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET667+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n013.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.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 05:31:06 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.48 % Refutation found
% 0.13/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.48 fof(f1,axiom,(
% 0.13/0.48 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,binary_relation_type)=> ( member(ordered_pair(B,C),D)=> ( member(B,domain_of(D))& member(C,range_of(D)) ) ) ) )) )) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f2,axiom,(
% 0.13/0.48 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> ( member(C,B)<=> member(ordered_pair(C,C),identity_relation_of(B)) ) ) )) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f5,axiom,(
% 0.13/0.48 (! [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.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f7,axiom,(
% 0.13/0.48 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> ( subset(B,C)<=> (! [D] :( ilf_type(D,set_type)=> ( member(D,B)=> member(D,C) ) ) )) ) )) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f13,axiom,(
% 0.13/0.48 (! [B] :( ilf_type(B,set_type)=> ( ilf_type(B,binary_relation_type)<=> ( relation_like(B)& ilf_type(B,set_type) ) ) ) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f24,axiom,(
% 0.13/0.48 (! [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.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f27,axiom,(
% 0.13/0.48 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,relation_type(B,C))=> domain(B,C,D) = domain_of(D) ) )) )) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f29,axiom,(
% 0.13/0.48 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,relation_type(B,C))=> range(B,C,D) = range_of(D) ) )) )) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f31,axiom,(
% 0.13/0.48 (! [B] : ilf_type(B,set_type) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f32,conjecture,(
% 0.13/0.48 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,set_type)=> (! [E] :( ilf_type(E,relation_type(B,C))=> ( subset(identity_relation_of(D),E)=> ( subset(D,domain(B,C,E))& subset(D,range(B,C,E)) ) ) ) )) )) )) )),
% 0.13/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.48 fof(f33,negated_conjecture,(
% 0.13/0.48 ~((! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,set_type)=> (! [E] :( ilf_type(E,relation_type(B,C))=> ( subset(identity_relation_of(D),E)=> ( subset(D,domain(B,C,E))& subset(D,range(B,C,E)) ) ) ) )) )) )) ))),
% 0.13/0.48 inference(negated_conjecture,[status(cth)],[f32])).
% 0.13/0.48 fof(f34,plain,(
% 0.13/0.48 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,binary_relation_type)|(~member(ordered_pair(B,C),D)|(member(B,domain_of(D))&member(C,range_of(D)))))))))),
% 0.13/0.48 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.13/0.48 fof(f35,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,binary_relation_type)|~member(ordered_pair(X0,X1),X2)|member(X0,domain_of(X2)))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f34])).
% 0.13/0.48 fof(f36,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,binary_relation_type)|~member(ordered_pair(X0,X1),X2)|member(X1,range_of(X2)))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f34])).
% 0.13/0.48 fof(f37,plain,(
% 0.13/0.48 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(member(C,B)<=>member(ordered_pair(C,C),identity_relation_of(B))))))),
% 0.13/0.48 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.13/0.48 fof(f38,plain,(
% 0.13/0.48 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|((~member(C,B)|member(ordered_pair(C,C),identity_relation_of(B)))&(member(C,B)|~member(ordered_pair(C,C),identity_relation_of(B)))))))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f37])).
% 0.13/0.48 fof(f39,plain,(
% 0.13/0.48 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~member(X1,X0)|member(ordered_pair(X1,X1),identity_relation_of(X0)))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f38])).
% 0.13/0.48 fof(f48,plain,(
% 0.13/0.48 ![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.13/0.48 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.13/0.48 fof(f50,plain,(
% 0.13/0.48 ![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.13/0.48 inference(cnf_transformation,[status(thm)],[f48])).
% 0.13/0.48 fof(f54,plain,(
% 0.13/0.48 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(subset(B,C)<=>(![D]: (~ilf_type(D,set_type)|(~member(D,B)|member(D,C))))))))),
% 0.13/0.48 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.13/0.48 fof(f55,plain,(
% 0.13/0.48 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|((~subset(B,C)|(![D]: (~ilf_type(D,set_type)|(~member(D,B)|member(D,C)))))&(subset(B,C)|(?[D]: (ilf_type(D,set_type)&(member(D,B)&~member(D,C)))))))))),
% 0.13/0.48 inference(NNF_transformation,[status(thm)],[f54])).
% 0.13/0.48 fof(f56,plain,(
% 0.13/0.48 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|((~subset(B,C)|(![D]: (~ilf_type(D,set_type)|(~member(D,B)|member(D,C)))))&(subset(B,C)|(ilf_type(sK1_skl(C,B),set_type)&(member(sK1_skl(C,B),B)&~member(sK1_skl(C,B),C))))))))),
% 0.13/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(C,B))],[f55])).
% 0.13/0.48 fof(f57,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~subset(X0,X1)|~ilf_type(X2,set_type)|~member(X2,X0)|member(X2,X1))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.48 fof(f59,plain,(
% 0.13/0.48 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|subset(X0,X1)|member(sK1_skl(X1,X0),X0))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.48 fof(f60,plain,(
% 0.13/0.48 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|subset(X0,X1)|~member(sK1_skl(X1,X0),X1))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.48 fof(f77,plain,(
% 0.13/0.48 ![B]: (~ilf_type(B,set_type)|(ilf_type(B,binary_relation_type)<=>(relation_like(B)&ilf_type(B,set_type))))),
% 0.13/0.48 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.13/0.48 fof(f78,plain,(
% 0.13/0.48 ![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.13/0.48 inference(NNF_transformation,[status(thm)],[f77])).
% 0.13/0.48 fof(f81,plain,(
% 0.13/0.48 ![X0]: (~ilf_type(X0,set_type)|ilf_type(X0,binary_relation_type)|~relation_like(X0)|~ilf_type(X0,set_type))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f78])).
% 0.13/0.48 fof(f121,plain,(
% 0.13/0.48 ![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.13/0.48 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.13/0.48 fof(f122,plain,(
% 0.13/0.48 ![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.13/0.48 inference(cnf_transformation,[status(thm)],[f121])).
% 0.13/0.48 fof(f131,plain,(
% 0.13/0.48 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,relation_type(B,C))|domain(B,C,D)=domain_of(D))))))),
% 0.13/0.48 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.13/0.48 fof(f132,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X0,X1))|domain(X0,X1,X2)=domain_of(X2))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f131])).
% 0.13/0.48 fof(f135,plain,(
% 0.13/0.48 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,relation_type(B,C))|range(B,C,D)=range_of(D))))))),
% 0.13/0.48 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.13/0.48 fof(f136,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,relation_type(X0,X1))|range(X0,X1,X2)=range_of(X2))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f135])).
% 0.13/0.48 fof(f139,plain,(
% 0.13/0.48 ![X0]: (ilf_type(X0,set_type))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f31])).
% 0.13/0.48 fof(f140,plain,(
% 0.13/0.48 (?[B]: (ilf_type(B,set_type)&(?[C]: (ilf_type(C,set_type)&(?[D]: (ilf_type(D,set_type)&(?[E]: (ilf_type(E,relation_type(B,C))&(subset(identity_relation_of(D),E)&(~subset(D,domain(B,C,E))|~subset(D,range(B,C,E))))))))))))),
% 0.13/0.48 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.13/0.48 fof(f141,plain,(
% 0.13/0.48 (ilf_type(sK12_skl,set_type)&(ilf_type(sK13_skl,set_type)&(ilf_type(sK14_skl,set_type)&(ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))&(subset(identity_relation_of(sK14_skl),sK15_skl)&(~subset(sK14_skl,domain(sK12_skl,sK13_skl,sK15_skl))|~subset(sK14_skl,range(sK12_skl,sK13_skl,sK15_skl))))))))),
% 0.13/0.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl,sK15_skl]),skolemize(B,sK12_skl),skolemize(C,sK13_skl),skolemize(D,sK14_skl),skolemize(E,sK15_skl)],[f140])).
% 0.13/0.48 fof(f145,plain,(
% 0.13/0.48 ilf_type(sK15_skl,relation_type(sK12_skl,sK13_skl))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.48 fof(f146,plain,(
% 0.13/0.48 subset(identity_relation_of(sK14_skl),sK15_skl)),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.48 fof(f147,plain,(
% 0.13/0.48 ~subset(sK14_skl,domain(sK12_skl,sK13_skl,sK15_skl))|~subset(sK14_skl,range(sK12_skl,sK13_skl,sK15_skl))),
% 0.13/0.48 inference(cnf_transformation,[status(thm)],[f141])).
% 0.13/0.48 fof(f150,plain,(
% 0.13/0.48 ![X0]: (~ilf_type(X0,set_type)|ilf_type(X0,binary_relation_type)|~relation_like(X0))),
% 0.13/0.48 inference(duplicate_literals_removal,[status(thm)],[f81])).
% 0.13/0.48 fof(f153,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X0,X2))|range(X0,X2,X1)=range_of(X1))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f136,f139])).
% 0.13/0.48 fof(f155,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X0,X2))|domain(X0,X2,X1)=domain_of(X1))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f132,f139])).
% 0.13/0.48 fof(f159,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,subset_type(cross_product(X0,X2)))|relation_like(X1))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f122,f139])).
% 0.13/0.48 fof(f173,plain,(
% 0.13/0.48 ![X0]: (ilf_type(X0,binary_relation_type)|~relation_like(X0))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f150,f139])).
% 0.13/0.48 fof(f176,plain,(
% 0.13/0.48 ![X0,X1]: (~ilf_type(X0,set_type)|subset(X0,X1)|~member(sK1_skl(X1,X0),X1))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f60,f139])).
% 0.13/0.48 fof(f177,plain,(
% 0.13/0.48 ![X0,X1]: (~ilf_type(X0,set_type)|subset(X0,X1)|member(sK1_skl(X1,X0),X0))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f59,f139])).
% 0.13/0.48 fof(f178,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~subset(X0,X1)|~member(X2,X0)|member(X2,X1))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f57,f139])).
% 0.13/0.48 fof(f180,plain,(
% 0.13/0.48 ![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.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f50,f139])).
% 0.13/0.48 fof(f186,plain,(
% 0.13/0.48 ![X0,X1]: (~ilf_type(X0,set_type)|~member(X1,X0)|member(ordered_pair(X1,X1),identity_relation_of(X0)))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f39,f139])).
% 0.13/0.48 fof(f187,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,binary_relation_type)|~member(ordered_pair(X0,X2),X1)|member(X2,range_of(X1)))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f36,f139])).
% 0.13/0.48 fof(f188,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,binary_relation_type)|~member(ordered_pair(X0,X2),X1)|member(X0,domain_of(X1)))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f35,f139])).
% 0.13/0.48 fof(f191,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|range(X1,X2,X0)=range_of(X0))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f153,f139])).
% 0.13/0.48 fof(f193,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|domain(X1,X2,X0)=domain_of(X0))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f155,f139])).
% 0.13/0.48 fof(f195,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,subset_type(cross_product(X1,X2)))|relation_like(X0))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f159,f139])).
% 0.13/0.48 fof(f205,plain,(
% 0.13/0.48 ![X0,X1]: (subset(X0,X1)|~member(sK1_skl(X1,X0),X1))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f176,f139])).
% 0.13/0.48 fof(f206,plain,(
% 0.13/0.48 ![X0,X1]: (subset(X0,X1)|member(sK1_skl(X1,X0),X0))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f177,f139])).
% 0.13/0.48 fof(f207,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~subset(X1,X0)|~member(X2,X1)|member(X2,X0))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f178,f139])).
% 0.13/0.48 fof(f209,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|ilf_type(X0,subset_type(cross_product(X1,X2))))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f180,f139])).
% 0.13/0.48 fof(f214,plain,(
% 0.13/0.48 ![X0,X1]: (~member(X0,X1)|member(ordered_pair(X0,X0),identity_relation_of(X1)))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f186,f139])).
% 0.13/0.48 fof(f215,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,binary_relation_type)|~member(ordered_pair(X1,X2),X0)|member(X2,range_of(X0)))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f187,f139])).
% 0.13/0.48 fof(f216,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,binary_relation_type)|~member(ordered_pair(X1,X2),X0)|member(X1,domain_of(X0)))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f188,f139])).
% 0.13/0.48 fof(f218,plain,(
% 0.13/0.48 range(sK12_skl,sK13_skl,sK15_skl)=range_of(sK15_skl)),
% 0.13/0.48 inference(resolution,[status(thm)],[f191,f145])).
% 0.13/0.48 fof(f219,plain,(
% 0.13/0.48 ~subset(sK14_skl,domain(sK12_skl,sK13_skl,sK15_skl))|~subset(sK14_skl,range_of(sK15_skl))),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f218,f147])).
% 0.13/0.48 fof(f221,plain,(
% 0.13/0.48 domain(sK12_skl,sK13_skl,sK15_skl)=domain_of(sK15_skl)),
% 0.13/0.48 inference(resolution,[status(thm)],[f193,f145])).
% 0.13/0.48 fof(f222,plain,(
% 0.13/0.48 ~subset(sK14_skl,domain_of(sK15_skl))|~subset(sK14_skl,range_of(sK15_skl))),
% 0.13/0.48 inference(backward_demodulation,[status(thm)],[f221,f219])).
% 0.13/0.48 fof(f260,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~subset(X0,X1)|~member(X2,X0)|member(X2,X1))),
% 0.13/0.48 inference(resolution,[status(thm)],[f207,f139])).
% 0.13/0.48 fof(f271,plain,(
% 0.13/0.48 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|relation_like(X0))),
% 0.13/0.48 inference(resolution,[status(thm)],[f209,f195])).
% 0.13/0.48 fof(f298,plain,(
% 0.13/0.48 relation_like(sK15_skl)),
% 0.13/0.48 inference(resolution,[status(thm)],[f271,f145])).
% 0.13/0.48 fof(f300,plain,(
% 0.13/0.48 ilf_type(sK15_skl,binary_relation_type)),
% 0.13/0.48 inference(resolution,[status(thm)],[f298,f173])).
% 0.13/0.48 fof(f373,plain,(
% 0.13/0.48 ![X0]: (~member(X0,identity_relation_of(sK14_skl))|member(X0,sK15_skl))),
% 0.13/0.48 inference(resolution,[status(thm)],[f260,f146])).
% 0.13/0.48 fof(f406,plain,(
% 0.13/0.48 ![X0]: (member(ordered_pair(X0,X0),sK15_skl)|~member(X0,sK14_skl))),
% 0.13/0.48 inference(resolution,[status(thm)],[f373,f214])).
% 0.13/0.48 fof(f455,plain,(
% 0.13/0.48 ![X0]: (~member(X0,sK14_skl)|~ilf_type(sK15_skl,binary_relation_type)|member(X0,domain_of(sK15_skl)))),
% 0.13/0.48 inference(resolution,[status(thm)],[f406,f216])).
% 0.13/0.48 fof(f456,plain,(
% 0.13/0.48 ![X0]: (~member(X0,sK14_skl)|~ilf_type(sK15_skl,binary_relation_type)|member(X0,range_of(sK15_skl)))),
% 0.13/0.48 inference(resolution,[status(thm)],[f406,f215])).
% 0.13/0.48 fof(f458,plain,(
% 0.13/0.48 ![X0]: (~member(X0,sK14_skl)|member(X0,domain_of(sK15_skl)))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f455,f300])).
% 0.13/0.48 fof(f459,plain,(
% 0.13/0.48 ![X0]: (~member(X0,sK14_skl)|member(X0,range_of(sK15_skl)))),
% 0.13/0.48 inference(forward_subsumption_resolution,[status(thm)],[f456,f300])).
% 0.13/0.48 fof(f471,plain,(
% 0.13/0.48 ![X0]: (~member(sK1_skl(domain_of(sK15_skl),X0),sK14_skl)|subset(X0,domain_of(sK15_skl)))),
% 0.13/0.48 inference(resolution,[status(thm)],[f458,f205])).
% 0.13/0.48 fof(f475,plain,(
% 0.13/0.48 ![X0]: (~member(sK1_skl(range_of(sK15_skl),X0),sK14_skl)|subset(X0,range_of(sK15_skl)))),
% 0.13/0.48 inference(resolution,[status(thm)],[f459,f205])).
% 0.13/0.48 fof(f522,plain,(
% 0.13/0.48 subset(sK14_skl,domain_of(sK15_skl))|subset(sK14_skl,domain_of(sK15_skl))),
% 0.13/0.48 inference(resolution,[status(thm)],[f471,f206])).
% 0.13/0.48 fof(f523,plain,(
% 0.13/0.48 ~subset(sK14_skl,range_of(sK15_skl))),
% 0.13/0.48 inference(backward_subsumption_resolution,[status(thm)],[f222,f524])).
% 0.13/0.48 fof(f524,plain,(
% 0.13/0.48 subset(sK14_skl,domain_of(sK15_skl))),
% 0.13/0.48 inference(duplicate_literals_removal,[status(thm)],[f522])).
% 0.13/0.48 fof(f549,plain,(
% 0.13/0.48 subset(sK14_skl,range_of(sK15_skl))|subset(sK14_skl,range_of(sK15_skl))),
% 0.13/0.48 inference(resolution,[status(thm)],[f475,f206])).
% 0.13/0.48 fof(f550,plain,(
% 0.13/0.48 subset(sK14_skl,range_of(sK15_skl))),
% 0.13/0.49 inference(duplicate_literals_removal,[status(thm)],[f549])).
% 0.13/0.49 fof(f551,plain,(
% 0.13/0.49 $false),
% 0.13/0.49 inference(forward_subsumption_resolution,[status(thm)],[f550,f523])).
% 0.13/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.50 % Elapsed time: 0.139057 seconds
% 0.13/0.50 % CPU time: 0.811493 seconds
% 0.13/0.50 % Total memory used: 100.482 MB
% 0.13/0.50 % Net memory used: 99.238 MB
%------------------------------------------------------------------------------