%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET665+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 : n010.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 3.85s 0.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET665+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.11/0.36 % Computer : n010.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 05:32:12 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 3.85/0.97 % Refutation found
% 3.85/0.97 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.85/0.97 % SZS output start CNFRefutation for theBenchmark
% 3.85/0.97 fof(f1,axiom,(
% 3.85/0.97 (! [B] :( ilf_type(B,binary_relation_type)=> (! [C] :( ilf_type(C,binary_relation_type)=> ( subset(B,C)<=> (! [D] :( ilf_type(D,set_type)=> (! [E] :( ilf_type(E,set_type)=> ( member(ordered_pair(D,E),B)=> member(ordered_pair(D,E),C) ) ) )) )) ) )) )),
% 3.85/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/0.97 fof(f2,axiom,(
% 3.85/0.97 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,set_type)=> ( member(ordered_pair(C,D),identity_relation_of(B))<=> ( member(C,B)& C = D ) ) ) )) )) )),
% 3.85/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/0.97 fof(f3,axiom,(
% 3.85/0.97 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,set_type)=> (! [E] :( ilf_type(E,set_type)=> ( member(ordered_pair(B,C),cross_product(D,E))<=> ( member(B,D)& member(C,E) ) ) ) )) )) )) )),
% 3.85/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/0.97 fof(f4,axiom,(
% 3.85/0.97 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> ilf_type(cross_product(B,C),relation_type(B,C)) ) )) )),
% 3.85/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/0.97 fof(f8,axiom,(
% 3.85/0.97 (! [B] :( ilf_type(B,set_type)=> ilf_type(identity_relation_of(B),binary_relation_type) ) )),
% 3.85/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/0.97 fof(f11,axiom,(
% 3.85/0.97 (! [B] :( ilf_type(B,set_type)=> ( ilf_type(B,binary_relation_type)<=> ( relation_like(B)& ilf_type(B,set_type) ) ) ) )),
% 3.85/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/0.97 fof(f13,axiom,(
% 3.85/0.97 (! [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))) ) )) ) )) )),
% 3.85/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/0.97 fof(f20,axiom,(
% 3.85/0.97 (! [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) ) )) )) )),
% 3.85/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/0.97 fof(f27,axiom,(
% 3.85/0.97 (! [B] : ilf_type(B,set_type) )),
% 3.85/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/0.97 fof(f28,conjecture,(
% 3.85/0.97 (! [B] :( ilf_type(B,set_type)=> subset(identity_relation_of(B),cross_product(B,B)) ) )),
% 3.85/0.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.85/0.97 fof(f29,negated_conjecture,(
% 3.85/0.97 ~((! [B] :( ilf_type(B,set_type)=> subset(identity_relation_of(B),cross_product(B,B)) ) ))),
% 3.85/0.97 inference(negated_conjecture,[status(cth)],[f28])).
% 3.85/0.97 fof(f30,plain,(
% 3.85/0.97 ![B]: (~ilf_type(B,binary_relation_type)|(![C]: (~ilf_type(C,binary_relation_type)|(subset(B,C)<=>(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,set_type)|(~member(ordered_pair(D,E),B)|member(ordered_pair(D,E),C))))))))))),
% 3.85/0.97 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 3.85/0.97 fof(f31,plain,(
% 3.85/0.97 ![B]: (~ilf_type(B,binary_relation_type)|(![C]: (~ilf_type(C,binary_relation_type)|((~subset(B,C)|(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,set_type)|(~member(ordered_pair(D,E),B)|member(ordered_pair(D,E),C)))))))&(subset(B,C)|(?[D]: (ilf_type(D,set_type)&(?[E]: (ilf_type(E,set_type)&(member(ordered_pair(D,E),B)&~member(ordered_pair(D,E),C)))))))))))),
% 3.85/0.97 inference(NNF_transformation,[status(thm)],[f30])).
% 3.85/0.97 fof(f32,plain,(
% 3.85/0.97 ![B]: (~ilf_type(B,binary_relation_type)|(![C]: (~ilf_type(C,binary_relation_type)|((~subset(B,C)|(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,set_type)|(~member(ordered_pair(D,E),B)|member(ordered_pair(D,E),C)))))))&(subset(B,C)|(ilf_type(sK0_skl(C,B),set_type)&(ilf_type(sK1_skl(C,B),set_type)&(member(ordered_pair(sK0_skl(C,B),sK1_skl(C,B)),B)&~member(ordered_pair(sK0_skl(C,B),sK1_skl(C,B)),C)))))))))),
% 3.85/0.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(D,sK0_skl(C,B)),skolemize(E,sK1_skl(C,B))],[f31])).
% 3.85/0.97 fof(f36,plain,(
% 3.85/0.97 ![X0,X1]: (~ilf_type(X0,binary_relation_type)|~ilf_type(X1,binary_relation_type)|subset(X0,X1)|member(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X0))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f32])).
% 3.85/0.97 fof(f37,plain,(
% 3.85/0.97 ![X0,X1]: (~ilf_type(X0,binary_relation_type)|~ilf_type(X1,binary_relation_type)|subset(X0,X1)|~member(ordered_pair(sK0_skl(X1,X0),sK1_skl(X1,X0)),X1))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f32])).
% 3.85/0.97 fof(f38,plain,(
% 3.85/0.97 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|(member(ordered_pair(C,D),identity_relation_of(B))<=>(member(C,B)&C=D)))))))),
% 3.85/0.97 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 3.85/0.97 fof(f39,plain,(
% 3.85/0.97 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|((~member(ordered_pair(C,D),identity_relation_of(B))|(member(C,B)&C=D))&(member(ordered_pair(C,D),identity_relation_of(B))|(~member(C,B)|~C=D))))))))),
% 3.85/0.97 inference(NNF_transformation,[status(thm)],[f38])).
% 3.85/0.97 fof(f40,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~member(ordered_pair(X1,X2),identity_relation_of(X0))|member(X1,X0))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f39])).
% 3.85/0.97 fof(f41,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~member(ordered_pair(X1,X2),identity_relation_of(X0))|X1=X2)),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f39])).
% 3.85/0.97 fof(f43,plain,(
% 3.85/0.97 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,set_type)|(member(ordered_pair(B,C),cross_product(D,E))<=>(member(B,D)&member(C,E))))))))))),
% 3.85/0.97 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 3.85/0.97 fof(f44,plain,(
% 3.85/0.97 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|(![E]: (~ilf_type(E,set_type)|((~member(ordered_pair(B,C),cross_product(D,E))|(member(B,D)&member(C,E)))&(member(ordered_pair(B,C),cross_product(D,E))|(~member(B,D)|~member(C,E)))))))))))),
% 3.85/0.97 inference(NNF_transformation,[status(thm)],[f43])).
% 3.85/0.97 fof(f47,plain,(
% 3.85/0.97 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,set_type)|member(ordered_pair(X0,X1),cross_product(X2,X3))|~member(X0,X2)|~member(X1,X3))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f44])).
% 3.85/0.97 fof(f48,plain,(
% 3.85/0.97 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|ilf_type(cross_product(B,C),relation_type(B,C)))))),
% 3.85/0.97 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 3.85/0.97 fof(f49,plain,(
% 3.85/0.97 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|ilf_type(cross_product(X0,X1),relation_type(X0,X1)))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f48])).
% 3.85/0.97 fof(f66,plain,(
% 3.85/0.97 ![B]: (~ilf_type(B,set_type)|ilf_type(identity_relation_of(B),binary_relation_type))),
% 3.85/0.97 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 3.85/0.97 fof(f67,plain,(
% 3.85/0.97 ![X0]: (~ilf_type(X0,set_type)|ilf_type(identity_relation_of(X0),binary_relation_type))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f66])).
% 3.85/0.97 fof(f77,plain,(
% 3.85/0.97 ![B]: (~ilf_type(B,set_type)|(ilf_type(B,binary_relation_type)<=>(relation_like(B)&ilf_type(B,set_type))))),
% 3.85/0.97 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 3.85/0.97 fof(f78,plain,(
% 3.85/0.97 ![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)))))),
% 3.85/0.97 inference(NNF_transformation,[status(thm)],[f77])).
% 3.85/0.97 fof(f81,plain,(
% 3.85/0.97 ![X0]: (~ilf_type(X0,set_type)|ilf_type(X0,binary_relation_type)|~relation_like(X0)|~ilf_type(X0,set_type))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f78])).
% 3.85/0.97 fof(f84,plain,(
% 3.85/0.97 ![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)))))))))),
% 3.85/0.97 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 3.85/0.97 fof(f86,plain,(
% 3.85/0.97 ![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))))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f84])).
% 3.85/0.97 fof(f110,plain,(
% 3.85/0.97 ![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))))))),
% 3.85/0.97 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 3.85/0.97 fof(f111,plain,(
% 3.85/0.97 ![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))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f110])).
% 3.85/0.97 fof(f137,plain,(
% 3.85/0.97 ![X0]: (ilf_type(X0,set_type))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f27])).
% 3.85/0.97 fof(f138,plain,(
% 3.85/0.97 (?[B]: (ilf_type(B,set_type)&~subset(identity_relation_of(B),cross_product(B,B))))),
% 3.85/0.97 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 3.85/0.97 fof(f139,plain,(
% 3.85/0.97 (ilf_type(sK14_skl,set_type)&~subset(identity_relation_of(sK14_skl),cross_product(sK14_skl,sK14_skl)))),
% 3.85/0.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(B,sK14_skl)],[f138])).
% 3.85/0.97 fof(f141,plain,(
% 3.85/0.97 ~subset(identity_relation_of(sK14_skl),cross_product(sK14_skl,sK14_skl))),
% 3.85/0.97 inference(cnf_transformation,[status(thm)],[f139])).
% 3.85/0.97 fof(f146,plain,(
% 3.85/0.97 ![X0]: (~ilf_type(X0,set_type)|ilf_type(X0,binary_relation_type)|~relation_like(X0))),
% 3.85/0.97 inference(duplicate_literals_removal,[status(thm)],[f81])).
% 3.85/0.97 fof(f157,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,subset_type(cross_product(X0,X2)))|relation_like(X1))),
% 3.85/0.97 inference(backward_subsumption_resolution,[status(thm)],[f111,f137])).
% 3.85/0.97 fof(f166,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,relation_type(X0,X2))|ilf_type(X1,subset_type(cross_product(X0,X2))))),
% 3.85/0.97 inference(backward_subsumption_resolution,[status(thm)],[f86,f137])).
% 3.85/0.97 fof(f168,plain,(
% 3.85/0.97 ![X0]: (ilf_type(X0,binary_relation_type)|~relation_like(X0))),
% 3.85/0.97 inference(backward_subsumption_resolution,[status(thm)],[f146,f137])).
% 3.85/0.97 fof(f173,plain,(
% 3.85/0.97 ![X0]: (ilf_type(identity_relation_of(X0),binary_relation_type))),
% 3.85/0.97 inference(backward_subsumption_resolution,[status(thm)],[f67,f137])).
% 3.85/0.97 fof(f178,plain,(
% 3.85/0.97 ![X0,X1]: (~ilf_type(X0,set_type)|ilf_type(cross_product(X0,X1),relation_type(X0,X1)))),
% 3.85/0.97 inference(backward_subsumption_resolution,[status(thm)],[f49,f137])).
% 3.85/0.97 fof(f179,plain,(
% 3.85/0.97 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|member(ordered_pair(X0,X1),cross_product(X2,X3))|~member(X0,X2)|~member(X1,X3))),
% 3.85/0.97 inference(backward_subsumption_resolution,[status(thm)],[f47,f137])).
% 3.85/0.97 fof(f183,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~member(ordered_pair(X1,X2),identity_relation_of(X0))|X1=X2)),
% 3.85/0.97 inference(backward_subsumption_resolution,[status(thm)],[f41,f137])).
% 3.85/0.97 fof(f184,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~member(ordered_pair(X1,X2),identity_relation_of(X0))|member(X1,X0))),
% 3.85/0.97 inference(backward_subsumption_resolution,[status(thm)],[f40,f137])).
% 3.85/0.97 fof(f192,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,subset_type(cross_product(X1,X2)))|relation_like(X0))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f157,f137])).
% 3.85/0.97 fof(f198,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|ilf_type(X0,subset_type(cross_product(X1,X2))))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f166,f137])).
% 3.85/0.97 fof(f207,plain,(
% 3.85/0.97 ![X0,X1]: (ilf_type(cross_product(X0,X1),relation_type(X0,X1)))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f178,f137])).
% 3.85/0.97 fof(f208,plain,(
% 3.85/0.97 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|member(ordered_pair(X2,X0),cross_product(X1,X3))|~member(X2,X1)|~member(X0,X3))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f179,f137])).
% 3.85/0.97 fof(f212,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~member(ordered_pair(X0,X1),identity_relation_of(X2))|X0=X1)),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f183,f137])).
% 3.85/0.97 fof(f213,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~member(ordered_pair(X0,X1),identity_relation_of(X2))|member(X0,X2))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f184,f137])).
% 3.85/0.97 fof(f242,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,relation_type(X1,X2))|relation_like(X0))),
% 3.85/0.97 inference(resolution,[status(thm)],[f198,f192])).
% 3.85/0.97 fof(f255,plain,(
% 3.85/0.97 ![X0,X1]: (relation_like(cross_product(X0,X1)))),
% 3.85/0.97 inference(resolution,[status(thm)],[f242,f207])).
% 3.85/0.97 fof(f258,plain,(
% 3.85/0.97 ![X0,X1]: (ilf_type(cross_product(X0,X1),binary_relation_type))),
% 3.85/0.97 inference(resolution,[status(thm)],[f255,f168])).
% 3.85/0.97 fof(f273,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(sK1_skl(cross_product(X0,X1),X2),set_type)|~ilf_type(X0,set_type)|~member(sK0_skl(cross_product(X0,X1),X2),X0)|~member(sK1_skl(cross_product(X0,X1),X2),X1)|~ilf_type(X2,binary_relation_type)|~ilf_type(cross_product(X0,X1),binary_relation_type)|subset(X2,cross_product(X0,X1)))),
% 3.85/0.97 inference(resolution,[status(thm)],[f208,f37])).
% 3.85/0.97 fof(f274,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~member(sK0_skl(cross_product(X0,X1),X2),X0)|~member(sK1_skl(cross_product(X0,X1),X2),X1)|~ilf_type(X2,binary_relation_type)|~ilf_type(cross_product(X0,X1),binary_relation_type)|subset(X2,cross_product(X0,X1)))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f273,f137])).
% 3.85/0.97 fof(f295,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~member(ordered_pair(X0,X1),identity_relation_of(X2))|X0=X1)),
% 3.85/0.97 inference(resolution,[status(thm)],[f212,f137])).
% 3.85/0.97 fof(f299,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~member(ordered_pair(X0,X1),identity_relation_of(X2))|member(X0,X2))),
% 3.85/0.97 inference(resolution,[status(thm)],[f213,f137])).
% 3.85/0.97 fof(f311,plain,(
% 3.85/0.97 ![X0,X1]: (sK0_skl(X0,identity_relation_of(X1))=sK1_skl(X0,identity_relation_of(X1))|~ilf_type(identity_relation_of(X1),binary_relation_type)|~ilf_type(X0,binary_relation_type)|subset(identity_relation_of(X1),X0))),
% 3.85/0.97 inference(resolution,[status(thm)],[f295,f36])).
% 3.85/0.97 fof(f314,plain,(
% 3.85/0.97 ![X0,X1]: (sK0_skl(X0,identity_relation_of(X1))=sK1_skl(X0,identity_relation_of(X1))|~ilf_type(X0,binary_relation_type)|subset(identity_relation_of(X1),X0))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f311,f173])).
% 3.85/0.97 fof(f344,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~member(sK0_skl(cross_product(X0,X1),X2),X0)|~member(sK1_skl(cross_product(X0,X1),X2),X1)|~ilf_type(X2,binary_relation_type)|~ilf_type(cross_product(X0,X1),binary_relation_type)|subset(X2,cross_product(X0,X1)))),
% 3.85/0.97 inference(resolution,[status(thm)],[f274,f137])).
% 3.85/0.97 fof(f345,plain,(
% 3.85/0.97 ![X0,X1,X2]: (~member(sK0_skl(cross_product(X0,X1),X2),X0)|~member(sK1_skl(cross_product(X0,X1),X2),X1)|~ilf_type(X2,binary_relation_type)|subset(X2,cross_product(X0,X1)))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f344,f258])).
% 3.85/0.97 fof(f489,plain,(
% 3.85/0.97 sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl))=sK1_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl))|~ilf_type(cross_product(sK14_skl,sK14_skl),binary_relation_type)),
% 3.85/0.97 inference(resolution,[status(thm)],[f314,f141])).
% 3.85/0.97 fof(f491,plain,(
% 3.85/0.97 sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl))=sK1_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f489,f258])).
% 3.85/0.97 fof(f505,plain,(
% 3.85/0.97 ~ilf_type(identity_relation_of(sK14_skl),binary_relation_type)|~ilf_type(cross_product(sK14_skl,sK14_skl),binary_relation_type)|subset(identity_relation_of(sK14_skl),cross_product(sK14_skl,sK14_skl))|member(ordered_pair(sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl)),sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl))),identity_relation_of(sK14_skl))),
% 3.85/0.97 inference(paramodulation,[status(thm)],[f491,f36])).
% 3.85/0.97 fof(f508,plain,(
% 3.85/0.97 ~ilf_type(cross_product(sK14_skl,sK14_skl),binary_relation_type)|subset(identity_relation_of(sK14_skl),cross_product(sK14_skl,sK14_skl))|member(ordered_pair(sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl)),sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl))),identity_relation_of(sK14_skl))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f505,f173])).
% 3.85/0.97 fof(f637,plain,(
% 3.85/0.97 subset(identity_relation_of(sK14_skl),cross_product(sK14_skl,sK14_skl))|member(ordered_pair(sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl)),sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl))),identity_relation_of(sK14_skl))),
% 3.85/0.97 inference(resolution,[status(thm)],[f508,f258])).
% 3.85/0.97 fof(f639,plain,(
% 3.85/0.97 member(ordered_pair(sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl)),sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl))),identity_relation_of(sK14_skl))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f637,f141])).
% 3.85/0.97 fof(f803,plain,(
% 3.85/0.97 member(sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl)),sK14_skl)),
% 3.85/0.97 inference(resolution,[status(thm)],[f639,f299])).
% 3.85/0.97 fof(f995,plain,(
% 3.85/0.97 ~member(sK1_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl)),sK14_skl)|~ilf_type(identity_relation_of(sK14_skl),binary_relation_type)|subset(identity_relation_of(sK14_skl),cross_product(sK14_skl,sK14_skl))),
% 3.85/0.97 inference(resolution,[status(thm)],[f803,f345])).
% 3.85/0.97 fof(f996,plain,(
% 3.85/0.97 ~member(sK0_skl(cross_product(sK14_skl,sK14_skl),identity_relation_of(sK14_skl)),sK14_skl)|~ilf_type(identity_relation_of(sK14_skl),binary_relation_type)|subset(identity_relation_of(sK14_skl),cross_product(sK14_skl,sK14_skl))),
% 3.85/0.97 inference(forward_demodulation,[status(thm)],[f491,f995])).
% 3.85/0.97 fof(f997,plain,(
% 3.85/0.97 ~ilf_type(identity_relation_of(sK14_skl),binary_relation_type)|subset(identity_relation_of(sK14_skl),cross_product(sK14_skl,sK14_skl))),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f996,f803])).
% 3.85/0.97 fof(f1266,plain,(
% 3.85/0.97 ~ilf_type(identity_relation_of(sK14_skl),binary_relation_type)),
% 3.85/0.97 inference(resolution,[status(thm)],[f997,f141])).
% 3.85/0.97 fof(f1268,plain,(
% 3.85/0.97 $false),
% 3.85/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1266,f173])).
% 3.85/0.97 % SZS output end CNFRefutation for theBenchmark.p
% 3.85/0.99 % Elapsed time: 0.605077 seconds
% 3.85/0.99 % CPU time: 4.479756 seconds
% 3.85/0.99 % Total memory used: 155.972 MB
% 3.85/0.99 % Net memory used: 150.522 MB
%------------------------------------------------------------------------------