%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU326+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 : n009.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 0.23s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU326+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.35 % Computer : n009.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 06:11:57 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.42 % Drodi V4.1.1
% 0.23/0.46 % Refutation found
% 0.23/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.23/0.46 fof(f167,axiom,(
% 0.23/0.46 (! [A,B] :( element(B,powerset(powerset(A)))=> element(complements_of_subsets(A,B),powerset(powerset(A))) ) )),
% 0.23/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.46 fof(f258,axiom,(
% 0.23/0.46 (! [A,B] :( element(B,powerset(powerset(A)))=> complements_of_subsets(A,complements_of_subsets(A,B)) = B ) )),
% 0.23/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.46 fof(f360,conjecture,(
% 0.23/0.46 (! [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 ) ) ) )),
% 0.23/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.46 fof(f361,negated_conjecture,(
% 0.23/0.46 ~((! [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 ) ) ) ))),
% 0.23/0.46 inference(negated_conjecture,[status(cth)],[f360])).
% 0.23/0.46 fof(f476,lemma,(
% 0.23/0.46 (! [A,B] :( element(B,powerset(powerset(A)))=> ~ ( B != empty_set& complements_of_subsets(A,B) = empty_set ) ) )),
% 0.23/0.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.46 fof(f1274,plain,(
% 0.23/0.46 ![A,B]: (~element(B,powerset(powerset(A)))|element(complements_of_subsets(A,B),powerset(powerset(A))))),
% 0.23/0.46 inference(pre_NNF_transformation,[status(thm)],[f167])).
% 0.23/0.46 fof(f1275,plain,(
% 0.23/0.46 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|element(complements_of_subsets(X1,X0),powerset(powerset(X1))))),
% 0.23/0.46 inference(cnf_transformation,[status(thm)],[f1274])).
% 0.23/0.46 fof(f1542,plain,(
% 0.23/0.46 ![A,B]: (~element(B,powerset(powerset(A)))|complements_of_subsets(A,complements_of_subsets(A,B))=B)),
% 0.23/0.46 inference(pre_NNF_transformation,[status(thm)],[f258])).
% 0.23/0.46 fof(f1543,plain,(
% 0.23/0.46 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|complements_of_subsets(X1,complements_of_subsets(X1,X0))=X0)),
% 0.23/0.46 inference(cnf_transformation,[status(thm)],[f1542])).
% 0.23/0.46 fof(f2155,plain,(
% 0.23/0.46 (?[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))))),
% 0.23/0.46 inference(pre_NNF_transformation,[status(thm)],[f361])).
% 0.23/0.46 fof(f2156,definition,(
% 0.23/0.46 ![A,B]: (sP24_prd(B,A)<=>(~B=empty_set&complements_of_subsets(A,B)=empty_set))),
% 0.23/0.46 introduced(definition,[new_symbols(definition,[sP24_prd])],[])).
% 0.23/0.46 fof(f2157,plain,(
% 0.23/0.46 ?[A,B]: (element(B,powerset(powerset(A)))&(sP24_prd(B,A)|(~complements_of_subsets(A,B)=empty_set&B=empty_set)))),
% 0.23/0.46 inference(formula_renaming,[status(thm)],[f2155,f2156])).
% 0.23/0.46 fof(f2158,plain,(
% 0.23/0.46 (element(sK277_skl,powerset(powerset(sK276_skl)))&(sP24_prd(sK277_skl,sK276_skl)|(~complements_of_subsets(sK276_skl,sK277_skl)=empty_set&sK277_skl=empty_set)))),
% 0.23/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK276_skl,sK277_skl]),skolemize(A,sK276_skl),skolemize(B,sK277_skl)],[f2157])).
% 0.23/0.46 fof(f2159,plain,(
% 0.23/0.46 element(sK277_skl,powerset(powerset(sK276_skl)))),
% 0.23/0.46 inference(cnf_transformation,[status(thm)],[f2158])).
% 0.23/0.46 fof(f2160,plain,(
% 0.23/0.46 sP24_prd(sK277_skl,sK276_skl)|~complements_of_subsets(sK276_skl,sK277_skl)=empty_set),
% 0.23/0.46 inference(cnf_transformation,[status(thm)],[f2158])).
% 0.23/0.46 fof(f2161,plain,(
% 0.23/0.46 sP24_prd(sK277_skl,sK276_skl)|sK277_skl=empty_set),
% 0.23/0.46 inference(cnf_transformation,[status(thm)],[f2158])).
% 0.23/0.46 fof(f2544,plain,(
% 0.23/0.46 ![A,B]: (~element(B,powerset(powerset(A)))|(B=empty_set|~complements_of_subsets(A,B)=empty_set))),
% 0.23/0.46 inference(pre_NNF_transformation,[status(thm)],[f476])).
% 0.23/0.46 fof(f2545,plain,(
% 0.23/0.46 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|X0=empty_set|~complements_of_subsets(X1,X0)=empty_set)),
% 0.23/0.46 inference(cnf_transformation,[status(thm)],[f2544])).
% 0.23/0.46 fof(f3068,plain,(
% 0.23/0.46 ![A,B]: ((~sP24_prd(B,A)|(~B=empty_set&complements_of_subsets(A,B)=empty_set))&(sP24_prd(B,A)|(B=empty_set|~complements_of_subsets(A,B)=empty_set)))),
% 0.23/0.46 inference(NNF_transformation,[status(thm)],[f2156])).
% 0.23/0.46 fof(f3069,plain,(
% 0.23/0.46 (![A,B]: (~sP24_prd(B,A)|(~B=empty_set&complements_of_subsets(A,B)=empty_set)))&(![A,B]: (sP24_prd(B,A)|(B=empty_set|~complements_of_subsets(A,B)=empty_set)))),
% 0.23/0.46 inference(miniscoping,[status(thm)],[f3068])).
% 0.23/0.48 fof(f3070,plain,(
% 0.23/0.48 ![X0,X1]: (~sP24_prd(X0,X1)|~X0=empty_set)),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f3069])).
% 0.23/0.48 fof(f3071,plain,(
% 0.23/0.48 ![X0,X1]: (~sP24_prd(X0,X1)|complements_of_subsets(X1,X0)=empty_set)),
% 0.23/0.48 inference(cnf_transformation,[status(thm)],[f3069])).
% 0.23/0.48 fof(f3320,plain,(
% 0.23/0.48 ![X0]: (~sP24_prd(empty_set,X0))),
% 0.23/0.48 inference(destructive_equality_resolution,[status(thm)],[f3070])).
% 0.23/0.48 fof(f3337,plain,(
% 0.23/0.48 element(complements_of_subsets(sK276_skl,sK277_skl),powerset(powerset(sK276_skl)))),
% 0.23/0.48 inference(resolution,[status(thm)],[f1275,f2159])).
% 0.23/0.48 fof(f3338,plain,(
% 0.23/0.48 complements_of_subsets(sK276_skl,sK277_skl)=empty_set|sK277_skl=empty_set),
% 0.23/0.48 inference(resolution,[status(thm)],[f3071,f2161])).
% 0.23/0.48 fof(f3342,plain,(
% 0.23/0.48 complements_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl))=sK277_skl),
% 0.23/0.48 inference(resolution,[status(thm)],[f1543,f2159])).
% 0.23/0.48 fof(f3343,plain,(
% 0.23/0.48 sK277_skl=empty_set|~complements_of_subsets(sK276_skl,sK277_skl)=empty_set),
% 0.23/0.48 inference(resolution,[status(thm)],[f2545,f2159])).
% 0.23/0.48 fof(f3344,plain,(
% 0.23/0.48 complements_of_subsets(sK276_skl,sK277_skl)=empty_set|~complements_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl))=empty_set),
% 0.23/0.48 inference(resolution,[status(thm)],[f3337,f2545])).
% 0.23/0.48 fof(f3357,plain,(
% 0.23/0.48 sP24_prd(sK277_skl,sK276_skl)|~complements_of_subsets(sK276_skl,sK277_skl)=sK277_skl),
% 0.23/0.48 inference(backward_demodulation,[status(thm)],[f3359,f2160])).
% 0.23/0.48 fof(f3358,plain,(
% 0.23/0.48 ![X0]: (~sP24_prd(sK277_skl,X0))),
% 0.23/0.48 inference(backward_demodulation,[status(thm)],[f3359,f3320])).
% 0.23/0.48 fof(f3359,plain,(
% 0.23/0.48 sK277_skl=empty_set),
% 0.23/0.48 inference(forward_subsumption_resolution,[status(thm)],[f3343,f3338])).
% 0.23/0.48 fof(f3370,plain,(
% 0.23/0.48 ~complements_of_subsets(sK276_skl,sK277_skl)=sK277_skl),
% 0.23/0.48 inference(forward_subsumption_resolution,[status(thm)],[f3357,f3358])).
% 0.23/0.48 fof(f3371,plain,(
% 0.23/0.48 complements_of_subsets(sK276_skl,sK277_skl)=sK277_skl|~complements_of_subsets(sK276_skl,complements_of_subsets(sK276_skl,sK277_skl))=empty_set),
% 0.23/0.48 inference(forward_demodulation,[status(thm)],[f3359,f3344])).
% 0.23/0.48 fof(f3372,plain,(
% 0.23/0.48 complements_of_subsets(sK276_skl,sK277_skl)=sK277_skl|~sK277_skl=empty_set),
% 0.23/0.48 inference(forward_demodulation,[status(thm)],[f3342,f3371])).
% 0.23/0.48 fof(f3373,plain,(
% 0.23/0.48 complements_of_subsets(sK276_skl,sK277_skl)=sK277_skl|~sK277_skl=sK277_skl),
% 0.23/0.48 inference(forward_demodulation,[status(thm)],[f3359,f3372])).
% 0.23/0.48 fof(f3374,plain,(
% 0.23/0.48 complements_of_subsets(sK276_skl,sK277_skl)=sK277_skl),
% 0.23/0.48 inference(trivial_equality_resolution,[status(thm)],[f3373])).
% 0.23/0.48 fof(f3375,plain,(
% 0.23/0.48 $false),
% 0.23/0.48 inference(forward_subsumption_resolution,[status(thm)],[f3374,f3370])).
% 0.23/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.51 % Elapsed time: 0.142386 seconds
% 0.23/0.51 % CPU time: 0.395150 seconds
% 0.23/0.51 % Total memory used: 177.275 MB
% 0.23/0.51 % Net memory used: 176.411 MB
%------------------------------------------------------------------------------