%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU328+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:22:20 PM UTC 2026
% Result : Theorem 1.15s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU328+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 06:07:27 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.15/0.40 % Drodi V4.1.1
% 1.15/0.66 % Refutation found
% 1.15/0.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.15/0.66 % SZS output start CNFRefutation for theBenchmark
% 1.15/0.66 fof(f160,axiom,(
% 1.15/0.66 (! [A,B] :( element(B,powerset(powerset(A)))=> element(union_of_subsets(A,B),powerset(A)) ) )),
% 1.15/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.15/0.66 fof(f167,axiom,(
% 1.15/0.66 (! [A,B] :( element(B,powerset(powerset(A)))=> element(complements_of_subsets(A,B),powerset(powerset(A))) ) )),
% 1.15/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.15/0.66 fof(f256,axiom,(
% 1.15/0.66 (! [A,B] :( element(B,powerset(A))=> subset_complement(A,subset_complement(A,B)) = B ) )),
% 1.15/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.15/0.66 fof(f258,axiom,(
% 1.15/0.66 (! [A,B] :( element(B,powerset(powerset(A)))=> complements_of_subsets(A,complements_of_subsets(A,B)) = B ) )),
% 1.15/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.15/0.66 fof(f313,axiom,(
% 1.15/0.66 (! [A,B] :( element(B,powerset(powerset(A)))=> union_of_subsets(A,B) = union(B) ) )),
% 1.15/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.15/0.66 fof(f360,lemma,(
% 1.15/0.66 (! [A,B] :( element(B,powerset(powerset(A)))=> ( ~ ( B != empty_set& complements_of_subsets(A,B) = empty_set )& ~ ( complements_of_subsets(A,B) != empty_set& B = empty_set ) ) ) )),
% 1.15/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.15/0.66 fof(f369,lemma,(
% 1.15/0.66 (! [A,B] :( element(B,powerset(powerset(A)))=> ( B != empty_set=> meet_of_subsets(A,complements_of_subsets(A,B)) = subset_complement(A,union_of_subsets(A,B)) ) ) )),
% 1.15/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.15/0.66 fof(f372,conjecture,(
% 1.15/0.66 (! [A,B] :( element(B,powerset(powerset(A)))=> ( B != empty_set=> union_of_subsets(A,complements_of_subsets(A,B)) = subset_complement(A,meet_of_subsets(A,B)) ) ) )),
% 1.15/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.15/0.66 fof(f373,negated_conjecture,(
% 1.15/0.66 ~((! [A,B] :( element(B,powerset(powerset(A)))=> ( B != empty_set=> union_of_subsets(A,complements_of_subsets(A,B)) = subset_complement(A,meet_of_subsets(A,B)) ) ) ))),
% 1.15/0.66 inference(negated_conjecture,[status(cth)],[f372])).
% 1.15/0.66 fof(f1262,plain,(
% 1.15/0.66 ![A,B]: (~element(B,powerset(powerset(A)))|element(union_of_subsets(A,B),powerset(A)))),
% 1.15/0.66 inference(pre_NNF_transformation,[status(thm)],[f160])).
% 1.15/0.66 fof(f1263,plain,(
% 1.15/0.66 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|element(union_of_subsets(X1,X0),powerset(X1)))),
% 1.15/0.66 inference(cnf_transformation,[status(thm)],[f1262])).
% 1.15/0.66 fof(f1276,plain,(
% 1.15/0.66 ![A,B]: (~element(B,powerset(powerset(A)))|element(complements_of_subsets(A,B),powerset(powerset(A))))),
% 1.15/0.66 inference(pre_NNF_transformation,[status(thm)],[f167])).
% 1.15/0.66 fof(f1277,plain,(
% 1.15/0.66 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|element(complements_of_subsets(X1,X0),powerset(powerset(X1))))),
% 1.15/0.66 inference(cnf_transformation,[status(thm)],[f1276])).
% 1.15/0.66 fof(f1540,plain,(
% 1.15/0.66 ![A,B]: (~element(B,powerset(A))|subset_complement(A,subset_complement(A,B))=B)),
% 1.15/0.66 inference(pre_NNF_transformation,[status(thm)],[f256])).
% 1.15/0.66 fof(f1541,plain,(
% 1.15/0.66 ![X0,X1]: (~element(X0,powerset(X1))|subset_complement(X1,subset_complement(X1,X0))=X0)),
% 1.15/0.66 inference(cnf_transformation,[status(thm)],[f1540])).
% 1.15/0.66 fof(f1544,plain,(
% 1.15/0.66 ![A,B]: (~element(B,powerset(powerset(A)))|complements_of_subsets(A,complements_of_subsets(A,B))=B)),
% 1.15/0.66 inference(pre_NNF_transformation,[status(thm)],[f258])).
% 1.15/0.66 fof(f1545,plain,(
% 1.15/0.66 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|complements_of_subsets(X1,complements_of_subsets(X1,X0))=X0)),
% 1.15/0.66 inference(cnf_transformation,[status(thm)],[f1544])).
% 1.15/0.66 fof(f1765,plain,(
% 1.15/0.66 ![A,B]: (~element(B,powerset(powerset(A)))|union_of_subsets(A,B)=union(B))),
% 1.15/0.66 inference(pre_NNF_transformation,[status(thm)],[f313])).
% 1.15/0.66 fof(f1766,plain,(
% 1.15/0.66 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|union_of_subsets(X1,X0)=union(X0))),
% 1.15/0.66 inference(cnf_transformation,[status(thm)],[f1765])).
% 1.15/0.66 fof(f2157,plain,(
% 1.15/0.66 ![A,B]: (~element(B,powerset(powerset(A)))|((B=empty_set|~complements_of_subsets(A,B)=empty_set)&(complements_of_subsets(A,B)=empty_set|~B=empty_set)))),
% 1.15/0.66 inference(pre_NNF_transformation,[status(thm)],[f360])).
% 1.15/0.66 fof(f2158,plain,(
% 1.15/0.66 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|X0=empty_set|~complements_of_subsets(X1,X0)=empty_set)),
% 1.15/0.67 inference(cnf_transformation,[status(thm)],[f2157])).
% 1.15/0.67 fof(f2187,plain,(
% 1.15/0.67 ![A,B]: (~element(B,powerset(powerset(A)))|(B=empty_set|meet_of_subsets(A,complements_of_subsets(A,B))=subset_complement(A,union_of_subsets(A,B))))),
% 1.15/0.67 inference(pre_NNF_transformation,[status(thm)],[f369])).
% 1.15/0.67 fof(f2188,plain,(
% 1.15/0.67 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|X0=empty_set|meet_of_subsets(X1,complements_of_subsets(X1,X0))=subset_complement(X1,union_of_subsets(X1,X0)))),
% 1.15/0.67 inference(cnf_transformation,[status(thm)],[f2187])).
% 1.15/0.67 fof(f2194,plain,(
% 1.15/0.67 (?[A,B]: (element(B,powerset(powerset(A)))&(~B=empty_set&~union_of_subsets(A,complements_of_subsets(A,B))=subset_complement(A,meet_of_subsets(A,B)))))),
% 1.15/0.67 inference(pre_NNF_transformation,[status(thm)],[f373])).
% 1.15/0.67 fof(f2195,plain,(
% 1.15/0.67 (element(sK277_skl,powerset(powerset(sK276_skl)))&(~sK277_skl=empty_set&~union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl))=subset_complement(sK276_skl,meet_of_subsets(sK276_skl,sK277_skl))))),
% 1.15/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK276_skl,sK277_skl]),skolemize(A,sK276_skl),skolemize(B,sK277_skl)],[f2194])).
% 1.15/0.67 fof(f2196,plain,(
% 1.15/0.67 element(sK277_skl,powerset(powerset(sK276_skl)))),
% 1.15/0.67 inference(cnf_transformation,[status(thm)],[f2195])).
% 1.15/0.67 fof(f2197,plain,(
% 1.15/0.67 ~sK277_skl=empty_set),
% 1.15/0.67 inference(cnf_transformation,[status(thm)],[f2195])).
% 1.15/0.67 fof(f2198,plain,(
% 1.15/0.67 ~union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl))=subset_complement(sK276_skl,meet_of_subsets(sK276_skl,sK277_skl))),
% 1.15/0.67 inference(cnf_transformation,[status(thm)],[f2195])).
% 1.15/0.67 fof(f3353,plain,(
% 1.15/0.67 complements_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl))=sK277_skl),
% 1.15/0.67 inference(resolution,[status(thm)],[f1545,f2196])).
% 1.15/0.67 fof(f3357,plain,(
% 1.15/0.67 ![X0,X1]: (union_of_subsets(X0,complements_of_subsets(X0,X1))=union(complements_of_subsets(X0,X1))|~element(X1,powerset(powerset(X0))))),
% 1.15/0.67 inference(resolution,[status(thm)],[f1766,f1277])).
% 1.15/0.67 fof(f3366,plain,(
% 1.15/0.67 sK277_skl=empty_set|~complements_of_subsets(sK276_skl,sK277_skl)=empty_set),
% 1.15/0.67 inference(resolution,[status(thm)],[f2158,f2196])).
% 1.15/0.67 fof(f3367,plain,(
% 1.15/0.67 ~complements_of_subsets(sK276_skl,sK277_skl)=empty_set),
% 1.15/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3366,f2197])).
% 1.15/0.67 fof(f3376,plain,(
% 1.15/0.67 ![X0,X1]: (complements_of_subsets(X0,X1)=empty_set|meet_of_subsets(X0,complements_of_subsets(X0,complements_of_subsets(X0,X1)))=subset_complement(X0,union_of_subsets(X0,complements_of_subsets(X0,X1)))|~element(X1,powerset(powerset(X0))))),
% 1.15/0.67 inference(resolution,[status(thm)],[f2188,f1277])).
% 1.15/0.67 fof(f3486,plain,(
% 1.15/0.67 union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl))=union(complements_of_subsets(sK276_skl,sK277_skl))),
% 1.15/0.67 inference(resolution,[status(thm)],[f3357,f2196])).
% 1.15/0.67 fof(f3503,plain,(
% 1.15/0.67 ~union(complements_of_subsets(sK276_skl,sK277_skl))=subset_complement(sK276_skl,meet_of_subsets(sK276_skl,sK277_skl))),
% 1.15/0.67 inference(backward_demodulation,[status(thm)],[f3486,f2198])).
% 1.15/0.67 fof(f3504,plain,(
% 1.15/0.67 ~element(complements_of_subsets(sK276_skl,sK277_skl),powerset(powerset(sK276_skl)))|element(union(complements_of_subsets(sK276_skl,sK277_skl)),powerset(sK276_skl))),
% 1.15/0.67 inference(paramodulation,[status(thm)],[f3486,f1263])).
% 1.15/0.67 fof(f3595,plain,(
% 1.15/0.67 complements_of_subsets(sK276_skl,sK277_skl)=empty_set|meet_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl)))=subset_complement(sK276_skl,union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl)))),
% 1.15/0.67 inference(resolution,[status(thm)],[f3376,f2196])).
% 1.15/0.67 fof(f3596,plain,(
% 1.15/0.67 complements_of_subsets(sK276_skl,sK277_skl)=empty_set|meet_of_subsets(sK276_skl,sK277_skl)=subset_complement(sK276_skl,union_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl)))),
% 1.15/0.67 inference(forward_demodulation,[status(thm)],[f3353,f3595])).
% 1.15/0.67 fof(f3597,plain,(
% 1.15/0.67 complements_of_subsets(sK276_skl,sK277_skl)=empty_set|meet_of_subsets(sK276_skl,sK277_skl)=subset_complement(sK276_skl,union(complements_of_subsets(sK276_skl,sK277_skl)))),
% 1.15/0.67 inference(forward_demodulation,[status(thm)],[f3486,f3596])).
% 1.15/0.68 fof(f3598,plain,(
% 1.15/0.68 meet_of_subsets(sK276_skl,sK277_skl)=subset_complement(sK276_skl,union(complements_of_subsets(sK276_skl,sK277_skl)))),
% 1.15/0.68 inference(forward_subsumption_resolution,[status(thm)],[f3597,f3367])).
% 1.15/0.68 fof(f4297,plain,(
% 1.15/0.68 element(union(complements_of_subsets(sK276_skl,sK277_skl)),powerset(sK276_skl))|~element(sK277_skl,powerset(powerset(sK276_skl)))),
% 1.15/0.68 inference(resolution,[status(thm)],[f3504,f1277])).
% 1.15/0.68 fof(f4298,plain,(
% 1.15/0.68 element(union(complements_of_subsets(sK276_skl,sK277_skl)),powerset(sK276_skl))),
% 1.15/0.68 inference(forward_subsumption_resolution,[status(thm)],[f4297,f2196])).
% 1.15/0.68 fof(f4311,plain,(
% 1.15/0.68 subset_complement(sK276_skl,subset_complement(sK276_skl,union(complements_of_subsets(sK276_skl,sK277_skl))))=union(complements_of_subsets(sK276_skl,sK277_skl))),
% 1.15/0.68 inference(resolution,[status(thm)],[f4298,f1541])).
% 1.15/0.68 fof(f4324,plain,(
% 1.15/0.68 subset_complement(sK276_skl,meet_of_subsets(sK276_skl,sK277_skl))=union(complements_of_subsets(sK276_skl,sK277_skl))),
% 1.15/0.68 inference(forward_demodulation,[status(thm)],[f3598,f4311])).
% 1.15/0.68 fof(f4325,plain,(
% 1.15/0.68 $false),
% 1.15/0.68 inference(forward_subsumption_resolution,[status(thm)],[f4324,f3503])).
% 1.15/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 1.15/0.69 % Elapsed time: 0.314561 seconds
% 1.15/0.69 % CPU time: 2.034828 seconds
% 1.15/0.69 % Total memory used: 196.501 MB
% 1.15/0.69 % Net memory used: 193.454 MB
%------------------------------------------------------------------------------