%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU170+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:21:53 PM UTC 2026
% Result : Theorem 234.09s 29.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU170+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n001.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 06:00:13 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 234.09/29.95 % Refutation found
% 234.09/29.95 % SZS status Theorem for theBenchmark: Theorem is valid
% 234.09/29.95 % SZS output start CNFRefutation for theBenchmark
% 234.09/29.95 fof(f4,axiom,(
% 234.09/29.95 (! [A,B] : set_union2(A,B) = set_union2(B,A) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f8,axiom,(
% 234.09/29.95 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f9,axiom,(
% 234.09/29.95 (! [A,B] :( B = powerset(A)<=> (! [C] :( in(C,B)<=> subset(C,A) ) )) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f10,axiom,(
% 234.09/29.95 (! [A,B] :( ( ~ empty(A)=> ( element(B,A)<=> in(B,A) ) )& ( empty(A)=> ( element(B,A)<=> empty(B) ) ) ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f18,axiom,(
% 234.09/29.95 (! [A,B] :( element(B,powerset(A))=> subset_complement(A,B) = set_difference(A,B) ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f20,axiom,(
% 234.09/29.95 (! [A,B] :( disjoint(A,B)<=> set_intersection2(A,B) = empty_set ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f35,axiom,(
% 234.09/29.95 (! [A] : ~ empty(powerset(A)) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f42,axiom,(
% 234.09/29.95 (! [A,B] :( element(B,powerset(A))=> subset_complement(A,subset_complement(A,B)) = B ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f49,lemma,(
% 234.09/29.95 (! [A,B] :( set_difference(A,B) = empty_set<=> subset(A,B) ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f60,axiom,(
% 234.09/29.95 (! [A,B] :( disjoint(A,B)=> disjoint(B,A) ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f77,lemma,(
% 234.09/29.95 (! [A,B,C] :( subset(A,B)=> subset(set_difference(A,C),set_difference(B,C)) ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f83,lemma,(
% 234.09/29.95 (! [A,B] : set_union2(A,set_difference(B,A)) = set_union2(A,B) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f88,lemma,(
% 234.09/29.95 (! [A,B] : set_difference(set_union2(A,B),B) = set_difference(A,B) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f89,conjecture,(
% 234.09/29.95 (! [A,B] :( element(B,powerset(A))=> (! [C] :( element(C,powerset(A))=> ( disjoint(B,C)<=> subset(B,subset_complement(A,C)) ) ) )) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f90,negated_conjecture,(
% 234.09/29.95 ~((! [A,B] :( element(B,powerset(A))=> (! [C] :( element(C,powerset(A))=> ( disjoint(B,C)<=> subset(B,subset_complement(A,C)) ) ) )) ))),
% 234.09/29.95 inference(negated_conjecture,[status(cth)],[f89])).
% 234.09/29.95 fof(f95,lemma,(
% 234.09/29.95 (! [A,B] :( ~ ( ~ disjoint(A,B)& (! [C] : ~ in(C,set_intersection2(A,B)) ))& ~ ( (? [C] : in(C,set_intersection2(A,B)))& disjoint(A,B) ) ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f97,lemma,(
% 234.09/29.95 (! [A,B,C] :( ( subset(A,B)& disjoint(B,C) )=> disjoint(A,C) ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f102,axiom,(
% 234.09/29.95 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f103,lemma,(
% 234.09/29.95 (! [A,B] : subset(A,set_union2(A,B)) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f104,lemma,(
% 234.09/29.95 (! [A,B] :( disjoint(A,B)<=> set_difference(A,B) = A ) )),
% 234.09/29.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 234.09/29.95 fof(f117,plain,(
% 234.09/29.95 ![X0,X1]: (set_union2(X0,X1)=set_union2(X1,X0))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f4])).
% 234.09/29.95 fof(f131,plain,(
% 234.09/29.95 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 234.09/29.95 inference(NNF_transformation,[status(thm)],[f8])).
% 234.09/29.95 fof(f132,plain,(
% 234.09/29.95 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 234.09/29.95 inference(miniscoping,[status(thm)],[f131])).
% 234.09/29.95 fof(f133,plain,(
% 234.09/29.95 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK1_skl(A),A)))),
% 234.09/29.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f132])).
% 234.09/29.95 fof(f134,plain,(
% 234.09/29.95 ![X0,X1]: (~X0=empty_set|~in(X1,X0))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f133])).
% 234.09/29.95 fof(f136,plain,(
% 234.09/29.95 ![A,B]: ((~B=powerset(A)|(![C]: ((~in(C,B)|subset(C,A))&(in(C,B)|~subset(C,A)))))&(B=powerset(A)|(?[C]: ((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))))),
% 234.09/29.95 inference(NNF_transformation,[status(thm)],[f9])).
% 234.09/29.95 fof(f137,plain,(
% 234.09/29.95 (![A,B]: (~B=powerset(A)|((![C]: (~in(C,B)|subset(C,A)))&(![C]: (in(C,B)|~subset(C,A))))))&(![A,B]: (B=powerset(A)|(?[C]: ((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))))),
% 234.09/29.95 inference(miniscoping,[status(thm)],[f136])).
% 234.09/29.95 fof(f138,plain,(
% 234.09/29.95 (![A,B]: (~B=powerset(A)|((![C]: (~in(C,B)|subset(C,A)))&(![C]: (in(C,B)|~subset(C,A))))))&(![A,B]: (B=powerset(A)|((~in(sK2_skl(B,A),B)|~subset(sK2_skl(B,A),A))&(in(sK2_skl(B,A),B)|subset(sK2_skl(B,A),A)))))),
% 234.09/29.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f137])).
% 234.09/29.95 fof(f139,plain,(
% 234.09/29.95 ![X0,X1,X2]: (~X0=powerset(X1)|~in(X2,X0)|subset(X2,X1))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f138])).
% 234.09/29.95 fof(f140,plain,(
% 234.09/29.95 ![X0,X1,X2]: (~X0=powerset(X1)|in(X2,X0)|~subset(X2,X1))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f138])).
% 234.09/29.95 fof(f143,plain,(
% 234.09/29.95 ![A,B]: ((empty(A)|(element(B,A)<=>in(B,A)))&(~empty(A)|(element(B,A)<=>empty(B))))),
% 234.09/29.95 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 234.09/29.95 fof(f144,plain,(
% 234.09/29.95 ![A,B]: ((empty(A)|((~element(B,A)|in(B,A))&(element(B,A)|~in(B,A))))&(~empty(A)|((~element(B,A)|empty(B))&(element(B,A)|~empty(B)))))),
% 234.09/29.95 inference(NNF_transformation,[status(thm)],[f143])).
% 234.09/29.95 fof(f145,plain,(
% 234.09/29.95 (![A]: (empty(A)|((![B]: (~element(B,A)|in(B,A)))&(![B]: (element(B,A)|~in(B,A))))))&(![A]: (~empty(A)|((![B]: (~element(B,A)|empty(B)))&(![B]: (element(B,A)|~empty(B))))))),
% 234.09/29.95 inference(miniscoping,[status(thm)],[f144])).
% 234.09/29.95 fof(f146,plain,(
% 234.09/29.95 ![X0,X1]: (empty(X0)|~element(X1,X0)|in(X1,X0))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f145])).
% 234.09/29.95 fof(f147,plain,(
% 234.09/29.95 ![X0,X1]: (empty(X0)|element(X1,X0)|~in(X1,X0))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f145])).
% 234.09/29.95 fof(f211,plain,(
% 234.09/29.95 ![A,B]: (~element(B,powerset(A))|subset_complement(A,B)=set_difference(A,B))),
% 234.09/29.95 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 234.09/29.95 fof(f212,plain,(
% 234.09/29.95 ![X0,X1]: (~element(X0,powerset(X1))|subset_complement(X1,X0)=set_difference(X1,X0))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f211])).
% 234.09/29.95 fof(f214,plain,(
% 234.09/29.95 ![A,B]: ((~disjoint(A,B)|set_intersection2(A,B)=empty_set)&(disjoint(A,B)|~set_intersection2(A,B)=empty_set))),
% 234.09/29.95 inference(NNF_transformation,[status(thm)],[f20])).
% 234.09/29.95 fof(f215,plain,(
% 234.09/29.95 (![A,B]: (~disjoint(A,B)|set_intersection2(A,B)=empty_set))&(![A,B]: (disjoint(A,B)|~set_intersection2(A,B)=empty_set))),
% 234.09/29.95 inference(miniscoping,[status(thm)],[f214])).
% 234.09/29.95 fof(f216,plain,(
% 234.09/29.95 ![X0,X1]: (~disjoint(X0,X1)|set_intersection2(X0,X1)=empty_set)),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f215])).
% 234.09/29.95 fof(f227,plain,(
% 234.09/29.95 ![X0]: (~empty(powerset(X0)))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f35])).
% 234.09/29.95 fof(f240,plain,(
% 234.09/29.95 ![A,B]: (~element(B,powerset(A))|subset_complement(A,subset_complement(A,B))=B)),
% 234.09/29.95 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 234.09/29.95 fof(f241,plain,(
% 234.09/29.95 ![X0,X1]: (~element(X0,powerset(X1))|subset_complement(X1,subset_complement(X1,X0))=X0)),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f240])).
% 234.09/29.95 fof(f255,plain,(
% 234.09/29.95 ![A,B]: ((~set_difference(A,B)=empty_set|subset(A,B))&(set_difference(A,B)=empty_set|~subset(A,B)))),
% 234.09/29.95 inference(NNF_transformation,[status(thm)],[f49])).
% 234.09/29.95 fof(f256,plain,(
% 234.09/29.95 (![A,B]: (~set_difference(A,B)=empty_set|subset(A,B)))&(![A,B]: (set_difference(A,B)=empty_set|~subset(A,B)))),
% 234.09/29.95 inference(miniscoping,[status(thm)],[f255])).
% 234.09/29.95 fof(f257,plain,(
% 234.09/29.95 ![X0,X1]: (~set_difference(X0,X1)=empty_set|subset(X0,X1))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f256])).
% 234.09/29.95 fof(f258,plain,(
% 234.09/29.95 ![X0,X1]: (set_difference(X0,X1)=empty_set|~subset(X0,X1))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f256])).
% 234.09/29.95 fof(f289,plain,(
% 234.09/29.95 ![A,B]: (~disjoint(A,B)|disjoint(B,A))),
% 234.09/29.95 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 234.09/29.95 fof(f290,plain,(
% 234.09/29.95 ![X0,X1]: (~disjoint(X0,X1)|disjoint(X1,X0))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f289])).
% 234.09/29.95 fof(f334,plain,(
% 234.09/29.95 ![A,B,C]: (~subset(A,B)|subset(set_difference(A,C),set_difference(B,C)))),
% 234.09/29.95 inference(pre_NNF_transformation,[status(thm)],[f77])).
% 234.09/29.95 fof(f335,plain,(
% 234.09/29.95 ![A,B]: (~subset(A,B)|(![C]: subset(set_difference(A,C),set_difference(B,C))))),
% 234.09/29.95 inference(miniscoping,[status(thm)],[f334])).
% 234.09/29.95 fof(f336,plain,(
% 234.09/29.95 ![X0,X1,X2]: (~subset(X0,X1)|subset(set_difference(X0,X2),set_difference(X1,X2)))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f335])).
% 234.09/29.95 fof(f354,plain,(
% 234.09/29.95 ![X0,X1]: (set_union2(X0,set_difference(X1,X0))=set_union2(X0,X1))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f83])).
% 234.09/29.95 fof(f369,plain,(
% 234.09/29.95 ![X0,X1]: (set_difference(set_union2(X0,X1),X1)=set_difference(X0,X1))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f88])).
% 234.09/29.95 fof(f370,plain,(
% 234.09/29.95 (?[A,B]: (element(B,powerset(A))&(?[C]: (element(C,powerset(A))&(disjoint(B,C)<~>subset(B,subset_complement(A,C)))))))),
% 234.09/29.95 inference(pre_NNF_transformation,[status(thm)],[f90])).
% 234.09/29.95 fof(f371,plain,(
% 234.09/29.95 ?[A,B]: (element(B,powerset(A))&(?[C]: (element(C,powerset(A))&((disjoint(B,C)|subset(B,subset_complement(A,C)))&(~disjoint(B,C)|~subset(B,subset_complement(A,C)))))))),
% 234.09/29.95 inference(NNF_transformation,[status(thm)],[f370])).
% 234.09/29.95 fof(f372,plain,(
% 234.09/29.95 (element(sK25_skl,powerset(sK24_skl))&(element(sK26_skl,powerset(sK24_skl))&((disjoint(sK25_skl,sK26_skl)|subset(sK25_skl,subset_complement(sK24_skl,sK26_skl)))&(~disjoint(sK25_skl,sK26_skl)|~subset(sK25_skl,subset_complement(sK24_skl,sK26_skl))))))),
% 234.09/29.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl,sK25_skl,sK26_skl]),skolemize(A,sK24_skl),skolemize(B,sK25_skl),skolemize(C,sK26_skl)],[f371])).
% 234.09/29.95 fof(f373,plain,(
% 234.09/29.95 element(sK25_skl,powerset(sK24_skl))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f372])).
% 234.09/29.95 fof(f374,plain,(
% 234.09/29.95 element(sK26_skl,powerset(sK24_skl))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f372])).
% 234.09/29.95 fof(f375,plain,(
% 234.09/29.95 disjoint(sK25_skl,sK26_skl)|subset(sK25_skl,subset_complement(sK24_skl,sK26_skl))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f372])).
% 234.09/29.95 fof(f376,plain,(
% 234.09/29.95 ~disjoint(sK25_skl,sK26_skl)|~subset(sK25_skl,subset_complement(sK24_skl,sK26_skl))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f372])).
% 234.09/29.95 fof(f383,plain,(
% 234.09/29.95 ![A,B]: ((disjoint(A,B)|(?[C]: in(C,set_intersection2(A,B))))&((![C]: ~in(C,set_intersection2(A,B)))|~disjoint(A,B)))),
% 234.09/29.95 inference(pre_NNF_transformation,[status(thm)],[f95])).
% 234.09/29.95 fof(f384,plain,(
% 234.09/29.95 (![A,B]: (disjoint(A,B)|(?[C]: in(C,set_intersection2(A,B)))))&(![A,B]: ((![C]: ~in(C,set_intersection2(A,B)))|~disjoint(A,B)))),
% 234.09/29.95 inference(miniscoping,[status(thm)],[f383])).
% 234.09/29.95 fof(f385,plain,(
% 234.09/29.95 (![A,B]: (disjoint(A,B)|in(sK27_skl(B,A),set_intersection2(A,B))))&(![A,B]: ((![C]: ~in(C,set_intersection2(A,B)))|~disjoint(A,B)))),
% 234.09/29.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(C,sK27_skl(B,A))],[f384])).
% 234.09/29.95 fof(f386,plain,(
% 234.09/29.95 ![X0,X1]: (disjoint(X0,X1)|in(sK27_skl(X1,X0),set_intersection2(X0,X1)))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f385])).
% 234.09/29.95 fof(f390,plain,(
% 234.09/29.95 ![A,B,C]: ((~subset(A,B)|~disjoint(B,C))|disjoint(A,C))),
% 234.09/29.95 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 234.09/29.95 fof(f391,plain,(
% 234.09/29.95 ![A,C]: ((![B]: (~subset(A,B)|~disjoint(B,C)))|disjoint(A,C))),
% 234.09/29.95 inference(miniscoping,[status(thm)],[f390])).
% 234.09/29.95 fof(f392,plain,(
% 234.09/29.95 ![X0,X1,X2]: (~subset(X0,X1)|~disjoint(X1,X2)|disjoint(X0,X2))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f391])).
% 234.09/29.95 fof(f402,plain,(
% 234.09/29.95 ![A,B]: (~in(A,B)|~empty(B))),
% 234.09/29.95 inference(pre_NNF_transformation,[status(thm)],[f102])).
% 234.09/29.95 fof(f403,plain,(
% 234.09/29.95 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 234.09/29.95 inference(miniscoping,[status(thm)],[f402])).
% 234.09/29.95 fof(f404,plain,(
% 234.09/29.95 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f403])).
% 234.09/29.95 fof(f405,plain,(
% 234.09/29.95 ![X0,X1]: (subset(X0,set_union2(X0,X1)))),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f103])).
% 234.09/29.95 fof(f406,plain,(
% 234.09/29.95 ![A,B]: ((~disjoint(A,B)|set_difference(A,B)=A)&(disjoint(A,B)|~set_difference(A,B)=A))),
% 234.09/29.95 inference(NNF_transformation,[status(thm)],[f104])).
% 234.09/29.95 fof(f407,plain,(
% 234.09/29.95 (![A,B]: (~disjoint(A,B)|set_difference(A,B)=A))&(![A,B]: (disjoint(A,B)|~set_difference(A,B)=A))),
% 234.09/29.95 inference(miniscoping,[status(thm)],[f406])).
% 234.09/29.95 fof(f408,plain,(
% 234.09/29.95 ![X0,X1]: (~disjoint(X0,X1)|set_difference(X0,X1)=X0)),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f407])).
% 234.09/29.95 fof(f409,plain,(
% 234.09/29.95 ![X0,X1]: (disjoint(X0,X1)|~set_difference(X0,X1)=X0)),
% 234.09/29.95 inference(cnf_transformation,[status(thm)],[f407])).
% 234.09/29.95 fof(f442,plain,(
% 234.09/29.95 ![X0]: (~in(X0,empty_set))),
% 234.09/29.95 inference(destructive_equality_resolution,[status(thm)],[f134])).
% 234.09/29.95 fof(f443,plain,(
% 234.09/29.95 ![X0,X1]: (~in(X0,powerset(X1))|subset(X0,X1))),
% 234.09/29.95 inference(destructive_equality_resolution,[status(thm)],[f139])).
% 234.09/29.95 fof(f444,plain,(
% 234.09/29.95 ![X0,X1]: (in(X0,powerset(X1))|~subset(X0,X1))),
% 234.09/29.95 inference(destructive_equality_resolution,[status(thm)],[f140])).
% 234.09/29.95 fof(f468,plain,(
% 234.09/29.95 ![X0,X1]: (element(X0,X1)|~in(X0,X1))),
% 234.09/29.95 inference(backward_subsumption_resolution,[status(thm)],[f147,f404])).
% 234.09/29.95 fof(f487,plain,(
% 234.09/29.95 empty(powerset(sK24_skl))|in(sK25_skl,powerset(sK24_skl))),
% 234.09/29.95 inference(resolution,[status(thm)],[f146,f373])).
% 234.09/29.95 fof(f490,plain,(
% 234.09/29.95 in(sK25_skl,powerset(sK24_skl))),
% 234.09/29.95 inference(forward_subsumption_resolution,[status(thm)],[f487,f227])).
% 234.09/29.95 fof(f516,plain,(
% 234.09/29.95 subset(sK25_skl,sK24_skl)),
% 234.09/29.95 inference(resolution,[status(thm)],[f490,f443])).
% 234.09/29.95 fof(f566,plain,(
% 234.09/29.95 subset_complement(sK24_skl,sK26_skl)=set_difference(sK24_skl,sK26_skl)),
% 234.09/29.95 inference(resolution,[status(thm)],[f212,f374])).
% 234.09/29.95 fof(f569,plain,(
% 234.09/29.95 ![X0,X1]: (subset_complement(X0,X1)=set_difference(X0,X1)|~in(X1,powerset(X0)))),
% 234.09/29.95 inference(resolution,[status(thm)],[f212,f468])).
% 234.09/29.95 fof(f575,plain,(
% 234.09/29.95 ~disjoint(sK25_skl,sK26_skl)|~subset(sK25_skl,set_difference(sK24_skl,sK26_skl))),
% 234.09/29.95 inference(backward_demodulation,[status(thm)],[f566,f376])).
% 234.09/29.95 fof(f576,plain,(
% 234.09/29.95 disjoint(sK25_skl,sK26_skl)|subset(sK25_skl,set_difference(sK24_skl,sK26_skl))),
% 234.09/29.95 inference(backward_demodulation,[status(thm)],[f566,f375])).
% 234.09/29.95 fof(f617,plain,(
% 234.09/29.95 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~disjoint(X1,X0))),
% 234.09/29.95 inference(resolution,[status(thm)],[f216,f290])).
% 234.09/29.95 fof(f686,plain,(
% 234.09/29.95 ![X0,X1]: (subset_complement(X0,subset_complement(X0,X1))=X1|~in(X1,powerset(X0)))),
% 234.09/29.95 inference(resolution,[status(thm)],[f241,f468])).
% 234.09/29.95 fof(f715,plain,(
% 234.09/29.95 ![X0,X1]: (in(X0,powerset(set_union2(X0,X1))))),
% 234.09/29.95 inference(resolution,[status(thm)],[f405,f444])).
% 234.09/29.95 fof(f793,plain,(
% 234.09/29.95 ![X0,X1]: (in(X0,powerset(set_union2(X1,X0))))),
% 234.09/29.95 inference(paramodulation,[status(thm)],[f117,f715])).
% 234.09/29.95 fof(f991,plain,(
% 234.09/29.95 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~set_difference(X1,X0)=X1)),
% 234.09/29.95 inference(resolution,[status(thm)],[f617,f409])).
% 234.09/29.95 fof(f1648,plain,(
% 234.09/29.95 ![X0,X1]: (subset_complement(set_union2(X0,X1),X1)=set_difference(set_union2(X0,X1),X1))),
% 234.09/29.95 inference(resolution,[status(thm)],[f569,f793])).
% 234.09/29.95 fof(f1657,plain,(
% 234.09/29.95 ![X0,X1]: (subset_complement(set_union2(X0,X1),X1)=set_difference(X0,X1))),
% 234.09/29.95 inference(forward_demodulation,[status(thm)],[f369,f1648])).
% 234.09/29.95 fof(f2311,plain,(
% 234.09/29.95 ![X0,X1]: (subset_complement(set_union2(X0,X1),X0)=set_difference(X1,X0))),
% 234.09/29.95 inference(paramodulation,[status(thm)],[f117,f1657])).
% 234.09/29.95 fof(f2976,plain,(
% 234.09/29.95 ~set_difference(sK25_skl,set_difference(sK24_skl,sK26_skl))=empty_set|~disjoint(sK25_skl,sK26_skl)),
% 234.09/29.95 inference(resolution,[status(thm)],[f257,f575])).
% 234.09/29.95 fof(f3261,plain,(
% 234.09/29.95 ![X0,X1]: (subset_complement(set_union2(X0,X1),subset_complement(set_union2(X0,X1),X0))=X0)),
% 234.09/29.95 inference(resolution,[status(thm)],[f686,f715])).
% 234.09/29.95 fof(f3285,plain,(
% 234.09/29.95 ![X0,X1]: (subset_complement(set_union2(X0,X1),set_difference(X1,X0))=X0)),
% 234.09/29.95 inference(forward_demodulation,[status(thm)],[f2311,f3261])).
% 234.09/29.95 fof(f3454,plain,(
% 234.09/29.95 set_difference(sK25_skl,set_difference(sK24_skl,sK26_skl))=empty_set|disjoint(sK25_skl,sK26_skl)),
% 234.09/29.95 inference(resolution,[status(thm)],[f258,f576])).
% 234.09/29.95 fof(f3506,plain,(
% 234.09/29.95 set_difference(sK25_skl,set_difference(sK24_skl,sK26_skl))=empty_set|set_difference(sK25_skl,sK26_skl)=sK25_skl),
% 234.09/29.95 inference(resolution,[status(thm)],[f3454,f408])).
% 234.09/29.95 fof(f5779,plain,(
% 234.09/29.95 ![X0]: (subset(set_difference(sK25_skl,X0),set_difference(sK24_skl,X0)))),
% 234.09/29.95 inference(resolution,[status(thm)],[f336,f516])).
% 234.09/29.95 fof(f6347,plain,(
% 234.09/29.95 ![X0,X1]: (subset_complement(set_union2(X0,X1),set_difference(X1,X0))=set_difference(X0,set_difference(X1,X0)))),
% 234.09/29.95 inference(paramodulation,[status(thm)],[f354,f1657])).
% 234.09/29.95 fof(f6388,plain,(
% 234.09/29.95 ![X0,X1]: (X0=set_difference(X0,set_difference(X1,X0)))),
% 234.09/29.95 inference(forward_demodulation,[status(thm)],[f3285,f6347])).
% 175.48/30.08 fof(f6589,plain,(
% 175.48/30.08 ![X0,X1]: (set_intersection2(set_difference(X0,X1),X1)=empty_set)),
% 175.48/30.08 inference(resolution,[status(thm)],[f6388,f991])).
% 175.48/30.08 fof(f7847,plain,(
% 175.48/30.08 ![X0,X1]: (disjoint(set_difference(X0,X1),X1)|in(sK27_skl(X1,set_difference(X0,X1)),empty_set))),
% 175.48/30.08 inference(paramodulation,[status(thm)],[f6589,f386])).
% 175.48/30.08 fof(f7879,plain,(
% 175.48/30.08 ![X0,X1]: (disjoint(set_difference(X0,X1),X1))),
% 175.48/30.08 inference(forward_subsumption_resolution,[status(thm)],[f7847,f442])).
% 175.48/30.08 fof(f8317,plain,(
% 175.48/30.08 ![X0,X1,X2]: (~subset(X0,set_difference(X1,X2))|disjoint(X0,X2))),
% 175.48/30.08 inference(resolution,[status(thm)],[f7879,f392])).
% 175.48/30.08 fof(f8348,plain,(
% 175.48/30.08 disjoint(sK25_skl,sK26_skl)),
% 175.48/30.08 inference(backward_subsumption_resolution,[status(thm)],[f576,f8317])).
% 175.48/30.08 fof(f8349,plain,(
% 175.48/30.08 ~subset(sK25_skl,set_difference(sK24_skl,sK26_skl))),
% 175.48/30.08 inference(backward_subsumption_resolution,[status(thm)],[f575,f8317])).
% 175.48/30.08 fof(f8353,plain,(
% 175.48/30.08 ~set_difference(sK25_skl,set_difference(sK24_skl,sK26_skl))=empty_set),
% 175.48/30.08 inference(backward_subsumption_resolution,[status(thm)],[f2976,f8348])).
% 175.48/30.08 fof(f8355,plain,(
% 175.48/30.08 set_difference(sK25_skl,sK26_skl)=sK25_skl),
% 175.48/30.08 inference(backward_subsumption_resolution,[status(thm)],[f3506,f8353])).
% 175.48/30.08 fof(f24477,plain,(
% 175.48/30.08 subset(sK25_skl,set_difference(sK24_skl,sK26_skl))),
% 175.48/30.08 inference(paramodulation,[status(thm)],[f8355,f5779])).
% 175.48/30.08 fof(f24509,plain,(
% 175.48/30.08 $false),
% 175.48/30.08 inference(forward_subsumption_resolution,[status(thm)],[f24477,f8349])).
% 175.48/30.08 % SZS output end CNFRefutation for theBenchmark.p
% 14.95/30.13 % Elapsed time: 29.769050 seconds
% 14.95/30.13 % CPU time: 235.624752 seconds
% 14.95/30.13 % Total memory used: 1.165 GB
% 14.95/30.13 % Net memory used: 1.027 GB
%------------------------------------------------------------------------------