%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU320+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 : n005.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:19 PM UTC 2026
% Result : Theorem 0.26s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU320+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n005.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 06:11:02 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.26/0.53 % Drodi V4.1.1
% 0.26/0.57 % Refutation found
% 0.26/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.26/0.57 % SZS output start CNFRefutation for theBenchmark
% 0.26/0.57 fof(f145,axiom,(
% 0.26/0.57 (! [A,B] :( element(B,powerset(A))=> element(subset_complement(A,B),powerset(A)) ) )),
% 0.26/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.57 fof(f247,axiom,(
% 0.26/0.57 (! [A,B] :( element(B,powerset(A))=> subset_complement(A,subset_complement(A,B)) = B ) )),
% 0.26/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.57 fof(f418,lemma,(
% 0.26/0.57 (! [A] :( top_str(A)=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( closed_subset(B,A)<=> open_subset(subset_complement(the_carrier(A),B),A) ) ) )) )),
% 0.26/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.57 fof(f425,conjecture,(
% 0.26/0.57 (! [A] :( top_str(A)=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( open_subset(B,A)<=> closed_subset(subset_complement(the_carrier(A),B),A) ) ) )) )),
% 0.26/0.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.57 fof(f426,negated_conjecture,(
% 0.26/0.57 ~((! [A] :( top_str(A)=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( open_subset(B,A)<=> closed_subset(subset_complement(the_carrier(A),B),A) ) ) )) ))),
% 0.26/0.57 inference(negated_conjecture,[status(cth)],[f425])).
% 0.26/0.57 fof(f1219,plain,(
% 0.26/0.57 ![A,B]: (~element(B,powerset(A))|element(subset_complement(A,B),powerset(A)))),
% 0.26/0.57 inference(pre_NNF_transformation,[status(thm)],[f145])).
% 0.26/0.57 fof(f1220,plain,(
% 0.26/0.57 ![X0,X1]: (~element(X0,powerset(X1))|element(subset_complement(X1,X0),powerset(X1)))),
% 0.26/0.57 inference(cnf_transformation,[status(thm)],[f1219])).
% 0.26/0.57 fof(f1499,plain,(
% 0.26/0.57 ![A,B]: (~element(B,powerset(A))|subset_complement(A,subset_complement(A,B))=B)),
% 0.26/0.57 inference(pre_NNF_transformation,[status(thm)],[f247])).
% 0.26/0.57 fof(f1500,plain,(
% 0.26/0.57 ![X0,X1]: (~element(X0,powerset(X1))|subset_complement(X1,subset_complement(X1,X0))=X0)),
% 0.26/0.57 inference(cnf_transformation,[status(thm)],[f1499])).
% 0.26/0.57 fof(f2330,plain,(
% 0.26/0.57 ![A]: (~top_str(A)|(![B]: (~element(B,powerset(the_carrier(A)))|(closed_subset(B,A)<=>open_subset(subset_complement(the_carrier(A),B),A)))))),
% 0.26/0.57 inference(pre_NNF_transformation,[status(thm)],[f418])).
% 0.26/0.57 fof(f2331,plain,(
% 0.26/0.57 ![A]: (~top_str(A)|(![B]: (~element(B,powerset(the_carrier(A)))|((~closed_subset(B,A)|open_subset(subset_complement(the_carrier(A),B),A))&(closed_subset(B,A)|~open_subset(subset_complement(the_carrier(A),B),A))))))),
% 0.26/0.57 inference(NNF_transformation,[status(thm)],[f2330])).
% 0.26/0.57 fof(f2332,plain,(
% 0.26/0.57 ![X0,X1]: (~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~closed_subset(X1,X0)|open_subset(subset_complement(the_carrier(X0),X1),X0))),
% 0.26/0.57 inference(cnf_transformation,[status(thm)],[f2331])).
% 0.26/0.57 fof(f2333,plain,(
% 0.26/0.57 ![X0,X1]: (~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|closed_subset(X1,X0)|~open_subset(subset_complement(the_carrier(X0),X1),X0))),
% 0.26/0.57 inference(cnf_transformation,[status(thm)],[f2331])).
% 0.26/0.57 fof(f2348,plain,(
% 0.26/0.57 (?[A]: (top_str(A)&(?[B]: (element(B,powerset(the_carrier(A)))&(open_subset(B,A)<~>closed_subset(subset_complement(the_carrier(A),B),A))))))),
% 0.26/0.57 inference(pre_NNF_transformation,[status(thm)],[f426])).
% 0.26/0.57 fof(f2349,plain,(
% 0.26/0.57 ?[A]: (top_str(A)&(?[B]: (element(B,powerset(the_carrier(A)))&((open_subset(B,A)|closed_subset(subset_complement(the_carrier(A),B),A))&(~open_subset(B,A)|~closed_subset(subset_complement(the_carrier(A),B),A))))))),
% 0.26/0.57 inference(NNF_transformation,[status(thm)],[f2348])).
% 0.26/0.57 fof(f2350,plain,(
% 0.26/0.57 (top_str(sK286_skl)&(element(sK287_skl,powerset(the_carrier(sK286_skl)))&((open_subset(sK287_skl,sK286_skl)|closed_subset(subset_complement(the_carrier(sK286_skl),sK287_skl),sK286_skl))&(~open_subset(sK287_skl,sK286_skl)|~closed_subset(subset_complement(the_carrier(sK286_skl),sK287_skl),sK286_skl)))))),
% 0.26/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK286_skl,sK287_skl]),skolemize(A,sK286_skl),skolemize(B,sK287_skl)],[f2349])).
% 0.26/0.57 fof(f2351,plain,(
% 0.26/0.57 top_str(sK286_skl)),
% 0.26/0.57 inference(cnf_transformation,[status(thm)],[f2350])).
% 0.26/0.57 fof(f2352,plain,(
% 0.26/0.57 element(sK287_skl,powerset(the_carrier(sK286_skl)))),
% 0.26/0.57 inference(cnf_transformation,[status(thm)],[f2350])).
% 0.26/0.57 fof(f2353,plain,(
% 0.26/0.57 open_subset(sK287_skl,sK286_skl)|closed_subset(subset_complement(the_carrier(sK286_skl),sK287_skl),sK286_skl)),
% 0.26/0.57 inference(cnf_transformation,[status(thm)],[f2350])).
% 0.26/0.57 fof(f2354,plain,(
% 0.26/0.57 ~open_subset(sK287_skl,sK286_skl)|~closed_subset(subset_complement(the_carrier(sK286_skl),sK287_skl),sK286_skl)),
% 0.26/0.57 inference(cnf_transformation,[status(thm)],[f2350])).
% 0.26/0.57 fof(f3183,definition,(
% 0.26/0.57 sQ31_spl <=> (open_subset(sK287_skl,sK286_skl))),
% 0.26/0.57 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.26/0.57 fof(f3185,plain,(
% 0.26/0.57 ~open_subset(sK287_skl,sK286_skl)|sQ31_spl),
% 0.26/0.57 inference(component_clause,[status(thm)],[f3183])).
% 0.26/0.57 fof(f3186,definition,(
% 0.26/0.57 sQ32_spl <=> (closed_subset(subset_complement(the_carrier(sK286_skl),sK287_skl),sK286_skl))),
% 0.26/0.57 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.26/0.57 fof(f3187,plain,(
% 0.26/0.57 closed_subset(subset_complement(the_carrier(sK286_skl),sK287_skl),sK286_skl)|~sQ32_spl),
% 0.26/0.57 inference(component_clause,[status(thm)],[f3186])).
% 0.26/0.57 fof(f3189,plain,(
% 0.26/0.57 sQ31_spl|sQ32_spl),
% 0.26/0.57 inference(split_clause,[status(thm)],[f2353,f3183,f3186])).
% 0.26/0.57 fof(f3190,plain,(
% 0.26/0.57 ~sQ31_spl|~sQ32_spl),
% 0.26/0.57 inference(split_clause,[status(thm)],[f2354,f3183,f3186])).
% 0.26/0.57 fof(f3520,plain,(
% 0.26/0.57 subset_complement(the_carrier(sK286_skl),subset_complement(the_carrier(sK286_skl),sK287_skl))=sK287_skl),
% 0.26/0.57 inference(resolution,[status(thm)],[f1500,f2352])).
% 0.26/0.57 fof(f3521,plain,(
% 0.26/0.57 element(subset_complement(the_carrier(sK286_skl),sK287_skl),powerset(the_carrier(sK286_skl)))),
% 0.26/0.57 inference(resolution,[status(thm)],[f1220,f2352])).
% 0.26/0.57 fof(f3530,plain,(
% 0.26/0.57 ~top_str(sK286_skl)|~element(subset_complement(the_carrier(sK286_skl),sK287_skl),powerset(the_carrier(sK286_skl)))|open_subset(subset_complement(the_carrier(sK286_skl),subset_complement(the_carrier(sK286_skl),sK287_skl)),sK286_skl)|~sQ32_spl),
% 0.26/0.57 inference(resolution,[status(thm)],[f2332,f3187])).
% 0.26/0.57 fof(f3531,definition,(
% 0.26/0.57 sQ59_spl <=> (top_str(sK286_skl))),
% 0.26/0.57 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.26/0.57 fof(f3533,plain,(
% 0.26/0.57 ~top_str(sK286_skl)|sQ59_spl),
% 0.26/0.57 inference(component_clause,[status(thm)],[f3531])).
% 0.26/0.57 fof(f3534,definition,(
% 0.26/0.57 sQ60_spl <=> (element(subset_complement(the_carrier(sK286_skl),sK287_skl),powerset(the_carrier(sK286_skl))))),
% 0.26/0.57 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.26/0.57 fof(f3536,plain,(
% 0.26/0.57 ~element(subset_complement(the_carrier(sK286_skl),sK287_skl),powerset(the_carrier(sK286_skl)))|sQ60_spl),
% 0.26/0.57 inference(component_clause,[status(thm)],[f3534])).
% 0.26/0.57 fof(f3537,definition,(
% 0.26/0.57 sQ61_spl <=> (open_subset(subset_complement(the_carrier(sK286_skl),subset_complement(the_carrier(sK286_skl),sK287_skl)),sK286_skl))),
% 0.26/0.57 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.26/0.57 fof(f3538,plain,(
% 0.26/0.57 open_subset(subset_complement(the_carrier(sK286_skl),subset_complement(the_carrier(sK286_skl),sK287_skl)),sK286_skl)|~sQ61_spl),
% 0.26/0.57 inference(component_clause,[status(thm)],[f3537])).
% 0.26/0.57 fof(f3540,plain,(
% 0.26/0.57 ~sQ59_spl|~sQ60_spl|sQ61_spl|~sQ32_spl),
% 0.26/0.57 inference(split_clause,[status(thm)],[f3530,f3531,f3534,f3537,f3186])).
% 0.26/0.57 fof(f3541,plain,(
% 0.26/0.57 open_subset(sK287_skl,sK286_skl)|~sQ61_spl),
% 0.26/0.57 inference(forward_demodulation,[status(thm)],[f3520,f3538])).
% 0.26/0.57 fof(f3542,plain,(
% 0.26/0.57 $false|sQ31_spl|~sQ61_spl),
% 0.26/0.57 inference(forward_subsumption_resolution,[status(thm)],[f3541,f3185])).
% 0.26/0.57 fof(f3543,plain,(
% 0.26/0.57 sQ31_spl|~sQ61_spl),
% 0.26/0.57 inference(contradiction_clause,[status(thm)],[f3542])).
% 0.26/0.57 fof(f3545,definition,(
% 0.26/0.57 sQ62_spl <=> (element(sK287_skl,powerset(the_carrier(sK286_skl))))),
% 0.26/0.57 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.26/0.57 fof(f3547,plain,(
% 0.26/0.57 ~element(sK287_skl,powerset(the_carrier(sK286_skl)))|sQ62_spl),
% 0.26/0.57 inference(component_clause,[status(thm)],[f3545])).
% 0.26/0.57 fof(f3552,plain,(
% 0.26/0.57 $false|sQ59_spl),
% 0.26/0.57 inference(forward_subsumption_resolution,[status(thm)],[f3533,f2351])).
% 0.26/0.57 fof(f3553,plain,(
% 0.26/0.57 sQ59_spl),
% 0.26/0.57 inference(contradiction_clause,[status(thm)],[f3552])).
% 0.26/0.57 fof(f3555,plain,(
% 0.26/0.57 $false|sQ60_spl),
% 0.26/0.57 inference(forward_subsumption_resolution,[status(thm)],[f3536,f3521])).
% 0.26/0.57 fof(f3556,plain,(
% 0.26/0.57 sQ60_spl),
% 0.26/0.57 inference(contradiction_clause,[status(thm)],[f3555])).
% 0.26/0.58 fof(f3557,plain,(
% 0.26/0.58 $false|sQ62_spl),
% 0.26/0.58 inference(forward_subsumption_resolution,[status(thm)],[f3547,f2352])).
% 0.26/0.58 fof(f3558,plain,(
% 0.26/0.58 sQ62_spl),
% 0.26/0.58 inference(contradiction_clause,[status(thm)],[f3557])).
% 0.26/0.58 fof(f3561,plain,(
% 0.26/0.58 ~top_str(sK286_skl)|~element(subset_complement(the_carrier(sK286_skl),sK287_skl),powerset(the_carrier(sK286_skl)))|closed_subset(subset_complement(the_carrier(sK286_skl),sK287_skl),sK286_skl)|~open_subset(sK287_skl,sK286_skl)),
% 0.26/0.58 inference(paramodulation,[status(thm)],[f3520,f2333])).
% 0.26/0.58 fof(f3562,plain,(
% 0.26/0.58 ~sQ59_spl|~sQ60_spl|sQ32_spl|~sQ31_spl),
% 0.26/0.58 inference(split_clause,[status(thm)],[f3561,f3531,f3534,f3186,f3183])).
% 0.26/0.58 fof(f3563,plain,(
% 0.26/0.58 $false),
% 0.26/0.58 inference(sat_refutation,[status(thm)],[f3189,f3190,f3540,f3543,f3553,f3556,f3558,f3562])).
% 0.26/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.26/0.62 % Elapsed time: 0.176323 seconds
% 0.26/0.62 % CPU time: 0.479136 seconds
% 0.26/0.62 % Total memory used: 126.668 MB
% 0.26/0.62 % Net memory used: 126.061 MB
%------------------------------------------------------------------------------