%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET646+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 : n026.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:23 PM UTC 2026
% Result : Theorem 5.41s 1.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET646+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.12/0.38 % Computer : n026.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 21 05:33:37 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.40 % Drodi V4.1.1
% 5.41/1.30 % Refutation found
% 5.41/1.30 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.41/1.30 % SZS output start CNFRefutation for theBenchmark
% 5.41/1.30 fof(f2,axiom,(
% 5.41/1.30 (! [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) ) ) ) )) )) )) )),
% 5.41/1.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.41/1.30 fof(f3,axiom,(
% 5.41/1.30 (! [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))) ) )) ) )) )),
% 5.41/1.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.41/1.30 fof(f5,axiom,(
% 5.41/1.30 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> (! [D] :( ilf_type(D,set_type)=> ( D = singleton(C)<=> (! [E] :( ilf_type(E,set_type)=> ( member(E,D)<=> E = C ) ) )) ) )) )) )),
% 5.41/1.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.41/1.30 fof(f12,axiom,(
% 5.41/1.30 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> ( ilf_type(C,subset_type(B))<=> ilf_type(C,member_type(power_set(B))) ) ) )) )),
% 5.41/1.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.41/1.30 fof(f17,axiom,(
% 5.41/1.30 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ilf_type(C,set_type)=> ( member(B,power_set(C))<=> (! [D] :( ilf_type(D,set_type)=> ( member(D,B)=> member(D,C) ) ) )) ) )) )),
% 5.41/1.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.41/1.30 fof(f18,axiom,(
% 5.41/1.30 (! [B] :( ilf_type(B,set_type)=> ( ~ empty(power_set(B))& ilf_type(power_set(B),set_type) ) ) )),
% 5.41/1.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.41/1.30 fof(f19,axiom,(
% 5.41/1.30 (! [B] :( ilf_type(B,set_type)=> (! [C] :( ( ~ empty(C)& ilf_type(C,set_type) )=> ( ilf_type(B,member_type(C))<=> member(B,C) ) ) )) )),
% 5.41/1.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.41/1.30 fof(f25,axiom,(
% 5.41/1.30 (! [B] : ilf_type(B,set_type) )),
% 5.41/1.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.41/1.30 fof(f26,conjecture,(
% 5.41/1.30 (! [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(D,B)& member(E,C) )=> ilf_type(singleton(ordered_pair(D,E)),relation_type(B,C)) ) ) )) )) )) )),
% 5.41/1.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.41/1.30 fof(f27,negated_conjecture,(
% 5.41/1.30 ~((! [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(D,B)& member(E,C) )=> ilf_type(singleton(ordered_pair(D,E)),relation_type(B,C)) ) ) )) )) )) ))),
% 5.41/1.30 inference(negated_conjecture,[status(cth)],[f26])).
% 5.41/1.30 fof(f32,plain,(
% 5.41/1.30 ![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))))))))))),
% 5.41/1.30 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 5.41/1.30 fof(f33,plain,(
% 5.41/1.30 ![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)))))))))))),
% 5.41/1.30 inference(NNF_transformation,[status(thm)],[f32])).
% 5.41/1.30 fof(f36,plain,(
% 5.41/1.30 ![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))),
% 5.41/1.30 inference(cnf_transformation,[status(thm)],[f33])).
% 5.41/1.30 fof(f37,plain,(
% 5.41/1.30 ![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)))))))))),
% 5.41/1.30 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 5.41/1.30 fof(f38,plain,(
% 5.41/1.30 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,subset_type(cross_product(X0,X1)))|ilf_type(X2,relation_type(X0,X1)))),
% 5.41/1.30 inference(cnf_transformation,[status(thm)],[f37])).
% 5.41/1.30 fof(f43,plain,(
% 5.41/1.30 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|(D=singleton(C)<=>(![E]: (~ilf_type(E,set_type)|(member(E,D)<=>E=C)))))))))),
% 5.41/1.30 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 5.41/1.30 fof(f44,plain,(
% 5.41/1.30 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|((~D=singleton(C)|(![E]: (~ilf_type(E,set_type)|((~member(E,D)|E=C)&(member(E,D)|~E=C)))))&(D=singleton(C)|(?[E]: (ilf_type(E,set_type)&((~member(E,D)|~E=C)&(member(E,D)|E=C)))))))))))),
% 5.41/1.30 inference(NNF_transformation,[status(thm)],[f43])).
% 5.41/1.30 fof(f45,plain,(
% 5.41/1.30 (![B]: ~ilf_type(B,set_type))|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|((~D=singleton(C)|(![E]: (~ilf_type(E,set_type)|((~member(E,D)|E=C)&(member(E,D)|~E=C)))))&(D=singleton(C)|(?[E]: (ilf_type(E,set_type)&((~member(E,D)|~E=C)&(member(E,D)|E=C))))))))))),
% 5.41/1.30 inference(miniscoping,[status(thm)],[f44])).
% 5.41/1.30 fof(f46,plain,(
% 5.41/1.30 (![B]: ~ilf_type(B,set_type))|(![C]: (~ilf_type(C,set_type)|(![D]: (~ilf_type(D,set_type)|((~D=singleton(C)|(![E]: (~ilf_type(E,set_type)|((~member(E,D)|E=C)&(member(E,D)|~E=C)))))&(D=singleton(C)|(ilf_type(sK1_skl(D,C),set_type)&((~member(sK1_skl(D,C),D)|~sK1_skl(D,C)=C)&(member(sK1_skl(D,C),D)|sK1_skl(D,C)=C)))))))))),
% 5.41/1.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(E,sK1_skl(D,C))],[f45])).
% 5.41/1.30 fof(f47,plain,(
% 5.41/1.30 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~X2=singleton(X1)|~ilf_type(X3,set_type)|~member(X3,X2)|X3=X1)),
% 5.41/1.30 inference(cnf_transformation,[status(thm)],[f46])).
% 5.41/1.30 fof(f67,plain,(
% 5.41/1.30 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(ilf_type(C,subset_type(B))<=>ilf_type(C,member_type(power_set(B)))))))),
% 5.41/1.30 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 5.41/1.30 fof(f68,plain,(
% 5.41/1.30 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|((~ilf_type(C,subset_type(B))|ilf_type(C,member_type(power_set(B))))&(ilf_type(C,subset_type(B))|~ilf_type(C,member_type(power_set(B))))))))),
% 5.41/1.30 inference(NNF_transformation,[status(thm)],[f67])).
% 5.41/1.31 fof(f70,plain,(
% 5.41/1.31 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|ilf_type(X1,subset_type(X0))|~ilf_type(X1,member_type(power_set(X0))))),
% 5.41/1.31 inference(cnf_transformation,[status(thm)],[f68])).
% 5.41/1.31 fof(f91,plain,(
% 5.41/1.31 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|(member(B,power_set(C))<=>(![D]: (~ilf_type(D,set_type)|(~member(D,B)|member(D,C))))))))),
% 5.41/1.31 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 5.41/1.31 fof(f92,plain,(
% 5.41/1.31 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|((~member(B,power_set(C))|(![D]: (~ilf_type(D,set_type)|(~member(D,B)|member(D,C)))))&(member(B,power_set(C))|(?[D]: (ilf_type(D,set_type)&(member(D,B)&~member(D,C)))))))))),
% 5.41/1.31 inference(NNF_transformation,[status(thm)],[f91])).
% 5.41/1.31 fof(f93,plain,(
% 5.41/1.31 ![B]: (~ilf_type(B,set_type)|(![C]: (~ilf_type(C,set_type)|((~member(B,power_set(C))|(![D]: (~ilf_type(D,set_type)|(~member(D,B)|member(D,C)))))&(member(B,power_set(C))|(ilf_type(sK5_skl(C,B),set_type)&(member(sK5_skl(C,B),B)&~member(sK5_skl(C,B),C))))))))),
% 5.41/1.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(D,sK5_skl(C,B))],[f92])).
% 5.41/1.31 fof(f96,plain,(
% 5.41/1.31 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|member(X0,power_set(X1))|member(sK5_skl(X1,X0),X0))),
% 5.41/1.31 inference(cnf_transformation,[status(thm)],[f93])).
% 5.41/1.31 fof(f97,plain,(
% 5.41/1.31 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|member(X0,power_set(X1))|~member(sK5_skl(X1,X0),X1))),
% 5.41/1.31 inference(cnf_transformation,[status(thm)],[f93])).
% 5.41/1.31 fof(f98,plain,(
% 5.41/1.31 ![B]: (~ilf_type(B,set_type)|(~empty(power_set(B))&ilf_type(power_set(B),set_type)))),
% 5.41/1.31 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 5.41/1.31 fof(f99,plain,(
% 5.41/1.31 ![X0]: (~ilf_type(X0,set_type)|~empty(power_set(X0)))),
% 5.41/1.31 inference(cnf_transformation,[status(thm)],[f98])).
% 5.41/1.31 fof(f101,plain,(
% 5.41/1.31 ![B]: (~ilf_type(B,set_type)|(![C]: ((empty(C)|~ilf_type(C,set_type))|(ilf_type(B,member_type(C))<=>member(B,C)))))),
% 5.41/1.31 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 5.41/1.31 fof(f102,plain,(
% 5.41/1.31 ![B]: (~ilf_type(B,set_type)|(![C]: ((empty(C)|~ilf_type(C,set_type))|((~ilf_type(B,member_type(C))|member(B,C))&(ilf_type(B,member_type(C))|~member(B,C))))))),
% 5.41/1.31 inference(NNF_transformation,[status(thm)],[f101])).
% 5.41/1.31 fof(f104,plain,(
% 5.41/1.31 ![X0,X1]: (~ilf_type(X0,set_type)|empty(X1)|~ilf_type(X1,set_type)|ilf_type(X0,member_type(X1))|~member(X0,X1))),
% 5.41/1.31 inference(cnf_transformation,[status(thm)],[f102])).
% 5.41/1.31 fof(f127,plain,(
% 5.41/1.31 ![X0]: (ilf_type(X0,set_type))),
% 5.41/1.31 inference(cnf_transformation,[status(thm)],[f25])).
% 5.41/1.31 fof(f128,plain,(
% 5.41/1.31 (?[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(D,B)&member(E,C))&~ilf_type(singleton(ordered_pair(D,E)),relation_type(B,C)))))))))))),
% 5.41/1.31 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 5.41/1.31 fof(f129,plain,(
% 5.41/1.31 (ilf_type(sK11_skl,set_type)&(ilf_type(sK12_skl,set_type)&(ilf_type(sK13_skl,set_type)&(ilf_type(sK14_skl,set_type)&((member(sK13_skl,sK11_skl)&member(sK14_skl,sK12_skl))&~ilf_type(singleton(ordered_pair(sK13_skl,sK14_skl)),relation_type(sK11_skl,sK12_skl)))))))),
% 5.41/1.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl]),skolemize(B,sK11_skl),skolemize(C,sK12_skl),skolemize(D,sK13_skl),skolemize(E,sK14_skl)],[f128])).
% 5.41/1.31 fof(f134,plain,(
% 5.41/1.31 member(sK13_skl,sK11_skl)),
% 5.41/1.31 inference(cnf_transformation,[status(thm)],[f129])).
% 5.41/1.31 fof(f135,plain,(
% 5.41/1.31 member(sK14_skl,sK12_skl)),
% 5.41/1.31 inference(cnf_transformation,[status(thm)],[f129])).
% 5.41/1.31 fof(f136,plain,(
% 5.41/1.31 ~ilf_type(singleton(ordered_pair(sK13_skl,sK14_skl)),relation_type(sK11_skl,sK12_skl))),
% 5.41/1.31 inference(cnf_transformation,[status(thm)],[f129])).
% 5.41/1.31 fof(f137,plain,(
% 5.41/1.31 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(singleton(X1),set_type)|~ilf_type(X2,set_type)|~member(X2,singleton(X1))|X2=X1)),
% 5.41/1.31 inference(destructive_equality_resolution,[status(thm)],[f47])).
% 5.41/1.31 fof(f142,plain,(
% 5.41/1.31 ![X0,X1,X2]: (~ilf_type(X0,set_type)|~ilf_type(X1,subset_type(cross_product(X2,X0)))|ilf_type(X1,relation_type(X2,X0)))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f38,f127])).
% 5.41/1.31 fof(f144,plain,(
% 5.41/1.31 ![X0,X1]: (~ilf_type(X0,set_type)|~ilf_type(singleton(X0),set_type)|~ilf_type(X1,set_type)|~member(X1,singleton(X0))|X1=X0)),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f137,f127])).
% 5.41/1.31 fof(f150,plain,(
% 5.41/1.31 ![X0]: (~empty(power_set(X0)))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f99,f127])).
% 5.41/1.31 fof(f178,plain,(
% 5.41/1.31 ![X0,X1]: (empty(X0)|~ilf_type(X0,set_type)|ilf_type(X1,member_type(X0))|~member(X1,X0))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f104,f127])).
% 5.41/1.31 fof(f179,plain,(
% 5.41/1.31 ![X0,X1]: (empty(X0)|ilf_type(X1,member_type(X0))|~member(X1,X0))),
% 5.41/1.31 inference(resolution,[status(thm)],[f178,f127])).
% 5.41/1.31 fof(f182,plain,(
% 5.41/1.31 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|member(ordered_pair(X3,X0),cross_product(X1,X2))|~member(X3,X1)|~member(X0,X2))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f36,f127])).
% 5.41/1.31 fof(f184,plain,(
% 5.41/1.31 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|~ilf_type(X1,set_type)|member(ordered_pair(X2,X0),cross_product(X3,X1))|~member(X2,X3)|~member(X0,X1))),
% 5.41/1.31 inference(resolution,[status(thm)],[f182,f127])).
% 5.41/1.31 fof(f188,plain,(
% 5.41/1.31 ![X0,X1,X2,X3]: (~ilf_type(X0,set_type)|member(ordered_pair(X1,X2),cross_product(X3,X0))|~member(X1,X3)|~member(X2,X0))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f184,f127])).
% 5.41/1.31 fof(f191,plain,(
% 5.41/1.31 ![X0,X1,X2,X3]: (member(ordered_pair(X0,X1),cross_product(X2,X3))|~member(X0,X2)|~member(X1,X3))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f188,f127])).
% 5.41/1.31 fof(f533,plain,(
% 5.41/1.31 ![X0,X1]: (~ilf_type(X0,set_type)|ilf_type(X0,subset_type(X1))|~ilf_type(X0,member_type(power_set(X1))))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f70,f127])).
% 5.41/1.31 fof(f534,plain,(
% 5.41/1.31 ![X0,X1]: (ilf_type(X0,subset_type(X1))|~ilf_type(X0,member_type(power_set(X1))))),
% 5.41/1.31 inference(resolution,[status(thm)],[f533,f127])).
% 5.41/1.31 fof(f542,plain,(
% 5.41/1.31 ![X0,X1]: (ilf_type(X0,subset_type(X1))|empty(power_set(X1))|~member(X0,power_set(X1)))),
% 5.41/1.31 inference(resolution,[status(thm)],[f534,f179])).
% 5.41/1.31 fof(f544,plain,(
% 5.41/1.31 ![X0,X1]: (ilf_type(X0,subset_type(X1))|~member(X0,power_set(X1)))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f542,f150])).
% 5.41/1.31 fof(f549,plain,(
% 5.41/1.31 ![X0,X1,X2]: (~member(X0,power_set(cross_product(X1,X2)))|~ilf_type(X2,set_type)|ilf_type(X0,relation_type(X1,X2)))),
% 5.41/1.31 inference(resolution,[status(thm)],[f544,f142])).
% 5.41/1.31 fof(f550,plain,(
% 5.41/1.31 ![X0,X1,X2]: (~member(X0,power_set(cross_product(X1,X2)))|ilf_type(X0,relation_type(X1,X2)))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f549,f127])).
% 5.41/1.31 fof(f741,plain,(
% 5.41/1.31 ![X0,X1]: (~ilf_type(X0,set_type)|member(X1,power_set(X0))|member(sK5_skl(X0,X1),X1))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f96,f127])).
% 5.41/1.31 fof(f742,plain,(
% 5.41/1.31 ![X0,X1]: (member(X0,power_set(X1))|member(sK5_skl(X1,X0),X0))),
% 5.41/1.31 inference(resolution,[status(thm)],[f741,f127])).
% 5.41/1.31 fof(f743,plain,(
% 5.41/1.31 ![X0,X1]: (~ilf_type(X0,set_type)|member(X1,power_set(X0))|~member(sK5_skl(X0,X1),X0))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f97,f127])).
% 5.41/1.31 fof(f744,plain,(
% 5.41/1.31 ![X0,X1]: (member(X0,power_set(X1))|~member(sK5_skl(X1,X0),X1))),
% 5.41/1.31 inference(resolution,[status(thm)],[f743,f127])).
% 5.41/1.31 fof(f790,plain,(
% 5.41/1.31 ![X0,X1]: (member(singleton(X0),power_set(X1))|~ilf_type(X0,set_type)|~ilf_type(singleton(X0),set_type)|~ilf_type(sK5_skl(X1,singleton(X0)),set_type)|sK5_skl(X1,singleton(X0))=X0)),
% 5.41/1.31 inference(resolution,[status(thm)],[f742,f144])).
% 5.41/1.31 fof(f791,plain,(
% 5.41/1.31 ![X0,X1]: (member(singleton(X0),power_set(X1))|~ilf_type(singleton(X0),set_type)|~ilf_type(sK5_skl(X1,singleton(X0)),set_type)|sK5_skl(X1,singleton(X0))=X0)),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f790,f127])).
% 5.41/1.31 fof(f1788,plain,(
% 5.41/1.31 ![X0,X1]: (member(singleton(X0),power_set(X1))|~ilf_type(sK5_skl(X1,singleton(X0)),set_type)|sK5_skl(X1,singleton(X0))=X0)),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f791,f127])).
% 5.41/1.31 fof(f1789,plain,(
% 5.41/1.31 ![X0,X1]: (member(singleton(X0),power_set(X1))|sK5_skl(X1,singleton(X0))=X0)),
% 5.41/1.31 inference(resolution,[status(thm)],[f1788,f127])).
% 5.41/1.31 fof(f1828,plain,(
% 5.41/1.31 ![X0,X1,X2]: (sK5_skl(cross_product(X0,X1),singleton(X2))=X2|ilf_type(singleton(X2),relation_type(X0,X1)))),
% 5.41/1.31 inference(resolution,[status(thm)],[f1789,f550])).
% 5.41/1.31 fof(f1877,plain,(
% 5.41/1.31 sK5_skl(cross_product(sK11_skl,sK12_skl),singleton(ordered_pair(sK13_skl,sK14_skl)))=ordered_pair(sK13_skl,sK14_skl)),
% 5.41/1.31 inference(resolution,[status(thm)],[f1828,f136])).
% 5.41/1.31 fof(f2236,plain,(
% 5.41/1.31 member(singleton(ordered_pair(sK13_skl,sK14_skl)),power_set(cross_product(sK11_skl,sK12_skl)))|~member(ordered_pair(sK13_skl,sK14_skl),cross_product(sK11_skl,sK12_skl))),
% 5.41/1.31 inference(paramodulation,[status(thm)],[f1877,f744])).
% 5.41/1.31 fof(f2239,plain,(
% 5.41/1.31 ~member(ordered_pair(sK13_skl,sK14_skl),cross_product(sK11_skl,sK12_skl))|ilf_type(singleton(ordered_pair(sK13_skl,sK14_skl)),relation_type(sK11_skl,sK12_skl))),
% 5.41/1.31 inference(resolution,[status(thm)],[f2236,f550])).
% 5.41/1.31 fof(f2241,plain,(
% 5.41/1.31 ~member(ordered_pair(sK13_skl,sK14_skl),cross_product(sK11_skl,sK12_skl))),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f2239,f136])).
% 5.41/1.31 fof(f2242,plain,(
% 5.41/1.31 ~member(sK13_skl,sK11_skl)|~member(sK14_skl,sK12_skl)),
% 5.41/1.31 inference(resolution,[status(thm)],[f2241,f191])).
% 5.41/1.31 fof(f2279,plain,(
% 5.41/1.31 ~member(sK14_skl,sK12_skl)),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f2242,f134])).
% 5.41/1.31 fof(f2280,plain,(
% 5.41/1.31 $false),
% 5.41/1.31 inference(forward_subsumption_resolution,[status(thm)],[f2279,f135])).
% 5.41/1.31 % SZS output end CNFRefutation for theBenchmark.p
% 0.64/1.33 % Elapsed time: 0.927772 seconds
% 0.64/1.33 % CPU time: 7.135775 seconds
% 0.64/1.33 % Total memory used: 174.563 MB
% 0.64/1.33 % Net memory used: 160.429 MB
%------------------------------------------------------------------------------