%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU326+1 : 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 : n011.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.09s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU326+1 : 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 : n011.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:11:55 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.39 % Refutation found
% 0.09/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.39 fof(f19,axiom,(
% 0.09/0.39 (! [A,B] :( element(B,powerset(powerset(A)))=> element(complements_of_subsets(A,B),powerset(powerset(A))) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f24,axiom,(
% 0.09/0.39 (! [A,B] :( element(B,powerset(powerset(A)))=> complements_of_subsets(A,complements_of_subsets(A,B)) = B ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f29,conjecture,(
% 0.09/0.39 (! [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.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f30,negated_conjecture,(
% 0.09/0.39 ~((! [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.09/0.39 inference(negated_conjecture,[status(cth)],[f29])).
% 0.09/0.39 fof(f34,axiom,(
% 0.09/0.39 (! [A,B] :( element(B,powerset(powerset(A)))=> ~ ( B != empty_set& complements_of_subsets(A,B) = empty_set ) ) )),
% 0.09/0.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.39 fof(f96,plain,(
% 0.09/0.39 ![A,B]: (~element(B,powerset(powerset(A)))|element(complements_of_subsets(A,B),powerset(powerset(A))))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.09/0.39 fof(f97,plain,(
% 0.09/0.39 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|element(complements_of_subsets(X1,X0),powerset(powerset(X1))))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f96])).
% 0.09/0.39 fof(f107,plain,(
% 0.09/0.39 ![A,B]: (~element(B,powerset(powerset(A)))|complements_of_subsets(A,complements_of_subsets(A,B))=B)),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.09/0.39 fof(f108,plain,(
% 0.09/0.39 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|complements_of_subsets(X1,complements_of_subsets(X1,X0))=X0)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f107])).
% 0.09/0.39 fof(f125,plain,(
% 0.09/0.39 (?[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.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.09/0.39 fof(f126,definition,(
% 0.09/0.39 ![A,B]: (sP0_prd(B,A)<=>(~B=empty_set&complements_of_subsets(A,B)=empty_set))),
% 0.09/0.39 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.09/0.39 fof(f127,plain,(
% 0.09/0.39 ?[A,B]: (element(B,powerset(powerset(A)))&(sP0_prd(B,A)|(~complements_of_subsets(A,B)=empty_set&B=empty_set)))),
% 0.09/0.39 inference(formula_renaming,[status(thm)],[f125,f126])).
% 0.09/0.39 fof(f128,plain,(
% 0.09/0.39 (element(sK5_skl,powerset(powerset(sK4_skl)))&(sP0_prd(sK5_skl,sK4_skl)|(~complements_of_subsets(sK4_skl,sK5_skl)=empty_set&sK5_skl=empty_set)))),
% 0.09/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(A,sK4_skl),skolemize(B,sK5_skl)],[f127])).
% 0.09/0.39 fof(f129,plain,(
% 0.09/0.39 element(sK5_skl,powerset(powerset(sK4_skl)))),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f128])).
% 0.09/0.39 fof(f130,plain,(
% 0.09/0.39 sP0_prd(sK5_skl,sK4_skl)|~complements_of_subsets(sK4_skl,sK5_skl)=empty_set),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f128])).
% 0.09/0.39 fof(f131,plain,(
% 0.09/0.39 sP0_prd(sK5_skl,sK4_skl)|sK5_skl=empty_set),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f128])).
% 0.09/0.39 fof(f140,plain,(
% 0.09/0.39 ![A,B]: (~element(B,powerset(powerset(A)))|(B=empty_set|~complements_of_subsets(A,B)=empty_set))),
% 0.09/0.39 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.09/0.39 fof(f141,plain,(
% 0.09/0.39 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|X0=empty_set|~complements_of_subsets(X1,X0)=empty_set)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f140])).
% 0.09/0.39 fof(f156,plain,(
% 0.09/0.39 ![A,B]: ((~sP0_prd(B,A)|(~B=empty_set&complements_of_subsets(A,B)=empty_set))&(sP0_prd(B,A)|(B=empty_set|~complements_of_subsets(A,B)=empty_set)))),
% 0.09/0.39 inference(NNF_transformation,[status(thm)],[f126])).
% 0.09/0.39 fof(f157,plain,(
% 0.09/0.39 (![A,B]: (~sP0_prd(B,A)|(~B=empty_set&complements_of_subsets(A,B)=empty_set)))&(![A,B]: (sP0_prd(B,A)|(B=empty_set|~complements_of_subsets(A,B)=empty_set)))),
% 0.09/0.39 inference(miniscoping,[status(thm)],[f156])).
% 0.09/0.39 fof(f158,plain,(
% 0.09/0.39 ![X0,X1]: (~sP0_prd(X0,X1)|~X0=empty_set)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f157])).
% 0.09/0.39 fof(f159,plain,(
% 0.09/0.39 ![X0,X1]: (~sP0_prd(X0,X1)|complements_of_subsets(X1,X0)=empty_set)),
% 0.09/0.39 inference(cnf_transformation,[status(thm)],[f157])).
% 0.09/0.39 fof(f161,plain,(
% 0.09/0.39 ![X0]: (~sP0_prd(empty_set,X0))),
% 0.09/0.39 inference(destructive_equality_resolution,[status(thm)],[f158])).
% 0.09/0.39 fof(f162,plain,(
% 0.09/0.39 element(complements_of_subsets(sK4_skl,sK5_skl),powerset(powerset(sK4_skl)))),
% 0.09/0.39 inference(resolution,[status(thm)],[f97,f129])).
% 0.09/0.39 fof(f163,plain,(
% 0.09/0.39 complements_of_subsets(sK4_skl,complements_of_subsets(sK4_skl,sK5_skl))=sK5_skl),
% 0.09/0.39 inference(resolution,[status(thm)],[f108,f129])).
% 0.09/0.39 fof(f169,plain,(
% 0.09/0.39 complements_of_subsets(sK4_skl,sK5_skl)=empty_set|sK5_skl=empty_set),
% 0.09/0.39 inference(resolution,[status(thm)],[f159,f131])).
% 0.09/0.39 fof(f179,plain,(
% 0.09/0.39 complements_of_subsets(sK4_skl,sK5_skl)=empty_set|~complements_of_subsets(sK4_skl,complements_of_subsets(sK4_skl,sK5_skl))=empty_set),
% 0.09/0.39 inference(resolution,[status(thm)],[f141,f162])).
% 0.09/0.39 fof(f180,plain,(
% 0.09/0.39 sK5_skl=empty_set|~complements_of_subsets(sK4_skl,sK5_skl)=empty_set),
% 0.09/0.39 inference(resolution,[status(thm)],[f141,f129])).
% 0.09/0.39 fof(f181,plain,(
% 0.09/0.39 complements_of_subsets(sK4_skl,sK5_skl)=empty_set|~sK5_skl=empty_set),
% 0.09/0.39 inference(forward_demodulation,[status(thm)],[f163,f179])).
% 0.09/0.39 fof(f207,plain,(
% 0.09/0.39 sP0_prd(sK5_skl,sK4_skl)|~empty_set=empty_set),
% 0.09/0.39 inference(backward_demodulation,[status(thm)],[f208,f130])).
% 0.09/0.39 fof(f208,plain,(
% 0.09/0.39 complements_of_subsets(sK4_skl,sK5_skl)=empty_set),
% 0.09/0.39 inference(forward_subsumption_resolution,[status(thm)],[f181,f169])).
% 0.09/0.39 fof(f211,plain,(
% 0.09/0.39 sP0_prd(sK5_skl,sK4_skl)),
% 0.09/0.39 inference(trivial_equality_resolution,[status(thm)],[f207])).
% 0.09/0.39 fof(f214,plain,(
% 0.09/0.39 sK5_skl=empty_set|~empty_set=empty_set),
% 0.09/0.39 inference(forward_demodulation,[status(thm)],[f208,f180])).
% 0.09/0.39 fof(f226,plain,(
% 0.09/0.39 ![X0]: (~sP0_prd(sK5_skl,X0))),
% 0.09/0.39 inference(backward_demodulation,[status(thm)],[f227,f161])).
% 0.09/0.39 fof(f227,plain,(
% 0.09/0.39 sK5_skl=empty_set),
% 0.09/0.39 inference(trivial_equality_resolution,[status(thm)],[f214])).
% 0.09/0.39 fof(f240,plain,(
% 0.09/0.39 $false),
% 0.09/0.39 inference(backward_subsumption_resolution,[status(thm)],[f211,f226])).
% 0.09/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.42 % Elapsed time: 0.055890 seconds
% 0.09/0.42 % CPU time: 0.160840 seconds
% 0.09/0.42 % Total memory used: 82.145 MB
% 0.09/0.42 % Net memory used: 82.093 MB
%------------------------------------------------------------------------------