%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU311+1 : 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 : n015.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:18 PM UTC 2026
% Result : Theorem 0.09s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU311+1 : 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.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:13:38 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.55 % Refutation found
% 0.09/0.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.55 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.55 fof(f1,conjecture,(
% 0.09/0.55 (! [A,B] :( ( topological_space(A)& top_str(A)& element(B,powerset(powerset(the_carrier(A)))) )=> (? [C] :( element(C,powerset(powerset(the_carrier(A))))& (! [D] :( element(D,powerset(the_carrier(A)))=> ( in(D,C)<=> in(set_difference(cast_as_carrier_subset(A),D),B) ) ) )) )) )),
% 0.09/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f2,negated_conjecture,(
% 0.09/0.55 ~((! [A,B] :( ( topological_space(A)& top_str(A)& element(B,powerset(powerset(the_carrier(A)))) )=> (? [C] :( element(C,powerset(powerset(the_carrier(A))))& (! [D] :( element(D,powerset(the_carrier(A)))=> ( in(D,C)<=> in(set_difference(cast_as_carrier_subset(A),D),B) ) ) )) )) ))),
% 0.09/0.55 inference(negated_conjecture,[status(cth)],[f1])).
% 0.09/0.55 fof(f36,axiom,(
% 0.09/0.55 (! [A] : ~ empty(powerset(A)) )),
% 0.09/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f37,axiom,(
% 0.09/0.55 (! [A,B] :( ( topological_space(A)& top_str(A)& element(B,powerset(powerset(the_carrier(A)))) )=> (? [C] :(! [D] :( in(D,C)<=> ( in(D,powerset(the_carrier(A)))& in(set_difference(cast_as_carrier_subset(A),D),B) ) ) ))) )),
% 0.09/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f38,axiom,(
% 0.09/0.55 (! [A,B] :( ( ~ empty(A)=> ( element(B,A)<=> in(B,A) ) )& ( empty(A)=> ( element(B,A)<=> empty(B) ) ) ) )),
% 0.09/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f42,axiom,(
% 0.09/0.55 (! [A,B] :( (! [C] :( in(C,A)=> in(C,B) ))=> element(A,powerset(B)) ) )),
% 0.09/0.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.55 fof(f48,plain,(
% 0.09/0.55 (?[A,B]: (((topological_space(A)&top_str(A))&element(B,powerset(powerset(the_carrier(A)))))&(![C]: (~element(C,powerset(powerset(the_carrier(A))))|(?[D]: (element(D,powerset(the_carrier(A)))&(in(D,C)<~>in(set_difference(cast_as_carrier_subset(A),D),B))))))))),
% 0.09/0.55 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.09/0.55 fof(f49,plain,(
% 0.09/0.55 ?[A,B]: (((topological_space(A)&top_str(A))&element(B,powerset(powerset(the_carrier(A)))))&(![C]: (~element(C,powerset(powerset(the_carrier(A))))|(?[D]: (element(D,powerset(the_carrier(A)))&((in(D,C)|in(set_difference(cast_as_carrier_subset(A),D),B))&(~in(D,C)|~in(set_difference(cast_as_carrier_subset(A),D),B))))))))),
% 0.09/0.55 inference(NNF_transformation,[status(thm)],[f48])).
% 0.09/0.55 fof(f50,plain,(
% 0.09/0.55 (((topological_space(sK0_skl)&top_str(sK0_skl))&element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))))&(![C]: (~element(C,powerset(powerset(the_carrier(sK0_skl))))|(element(sK2_skl(C),powerset(the_carrier(sK0_skl)))&((in(sK2_skl(C),C)|in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(C)),sK1_skl))&(~in(sK2_skl(C),C)|~in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(C)),sK1_skl)))))))),
% 0.09/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(D,sK2_skl(C))],[f49])).
% 0.09/0.55 fof(f51,plain,(
% 0.09/0.55 topological_space(sK0_skl)),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f50])).
% 0.09/0.55 fof(f52,plain,(
% 0.09/0.55 top_str(sK0_skl)),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f50])).
% 0.09/0.55 fof(f53,plain,(
% 0.09/0.55 element(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f50])).
% 0.09/0.55 fof(f54,plain,(
% 0.09/0.55 ![X0]: (~element(X0,powerset(powerset(the_carrier(sK0_skl))))|element(sK2_skl(X0),powerset(the_carrier(sK0_skl))))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f50])).
% 0.09/0.55 fof(f55,plain,(
% 0.09/0.55 ![X0]: (~element(X0,powerset(powerset(the_carrier(sK0_skl))))|in(sK2_skl(X0),X0)|in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X0)),sK1_skl))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f50])).
% 0.09/0.55 fof(f56,plain,(
% 0.09/0.55 ![X0]: (~element(X0,powerset(powerset(the_carrier(sK0_skl))))|~in(sK2_skl(X0),X0)|~in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X0)),sK1_skl))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f50])).
% 0.09/0.55 fof(f162,plain,(
% 0.09/0.55 ![X0]: (~empty(powerset(X0)))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f36])).
% 0.09/0.55 fof(f163,plain,(
% 0.09/0.55 ![A,B]: (((~topological_space(A)|~top_str(A))|~element(B,powerset(powerset(the_carrier(A)))))|(?[C]: ![D]: (in(D,C)<=>(in(D,powerset(the_carrier(A)))&in(set_difference(cast_as_carrier_subset(A),D),B)))))),
% 0.09/0.55 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.09/0.55 fof(f164,plain,(
% 0.09/0.55 ![A,B]: (((~topological_space(A)|~top_str(A))|~element(B,powerset(powerset(the_carrier(A)))))|(?[C]: ![D]: ((~in(D,C)|(in(D,powerset(the_carrier(A)))&in(set_difference(cast_as_carrier_subset(A),D),B)))&(in(D,C)|(~in(D,powerset(the_carrier(A)))|~in(set_difference(cast_as_carrier_subset(A),D),B))))))),
% 0.09/0.55 inference(NNF_transformation,[status(thm)],[f163])).
% 0.09/0.55 fof(f165,plain,(
% 0.09/0.55 ![A,B]: (((~topological_space(A)|~top_str(A))|~element(B,powerset(powerset(the_carrier(A)))))|(?[C]: ((![D]: (~in(D,C)|(in(D,powerset(the_carrier(A)))&in(set_difference(cast_as_carrier_subset(A),D),B))))&(![D]: (in(D,C)|(~in(D,powerset(the_carrier(A)))|~in(set_difference(cast_as_carrier_subset(A),D),B)))))))),
% 0.09/0.55 inference(miniscoping,[status(thm)],[f164])).
% 0.09/0.55 fof(f166,plain,(
% 0.09/0.55 ![A,B]: (((~topological_space(A)|~top_str(A))|~element(B,powerset(powerset(the_carrier(A)))))|((![D]: (~in(D,sK7_skl(B,A))|(in(D,powerset(the_carrier(A)))&in(set_difference(cast_as_carrier_subset(A),D),B))))&(![D]: (in(D,sK7_skl(B,A))|(~in(D,powerset(the_carrier(A)))|~in(set_difference(cast_as_carrier_subset(A),D),B))))))),
% 0.09/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(C,sK7_skl(B,A))],[f165])).
% 0.09/0.55 fof(f167,plain,(
% 0.09/0.55 ![X0,X1,X2]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|~in(X2,sK7_skl(X1,X0))|in(X2,powerset(the_carrier(X0))))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f166])).
% 0.09/0.55 fof(f168,plain,(
% 0.09/0.55 ![X0,X1,X2]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|~in(X2,sK7_skl(X1,X0))|in(set_difference(cast_as_carrier_subset(X0),X2),X1))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f166])).
% 0.09/0.55 fof(f169,plain,(
% 0.09/0.55 ![X0,X1,X2]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|in(X2,sK7_skl(X1,X0))|~in(X2,powerset(the_carrier(X0)))|~in(set_difference(cast_as_carrier_subset(X0),X2),X1))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f166])).
% 0.09/0.55 fof(f170,plain,(
% 0.09/0.55 ![A,B]: ((empty(A)|(element(B,A)<=>in(B,A)))&(~empty(A)|(element(B,A)<=>empty(B))))),
% 0.09/0.55 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.09/0.55 fof(f171,plain,(
% 0.09/0.55 ![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)))))),
% 0.09/0.55 inference(NNF_transformation,[status(thm)],[f170])).
% 0.09/0.55 fof(f172,plain,(
% 0.09/0.55 (![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))))))),
% 0.09/0.55 inference(miniscoping,[status(thm)],[f171])).
% 0.09/0.55 fof(f173,plain,(
% 0.09/0.55 ![X0,X1]: (empty(X0)|~element(X1,X0)|in(X1,X0))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f172])).
% 0.09/0.55 fof(f180,plain,(
% 0.09/0.55 ![A,B]: ((?[C]: (in(C,A)&~in(C,B)))|element(A,powerset(B)))),
% 0.09/0.55 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.09/0.55 fof(f181,plain,(
% 0.09/0.55 ![A,B]: ((in(sK9_skl(B,A),A)&~in(sK9_skl(B,A),B))|element(A,powerset(B)))),
% 0.09/0.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(C,sK9_skl(B,A))],[f180])).
% 0.09/0.55 fof(f182,plain,(
% 0.09/0.55 ![X0,X1]: (in(sK9_skl(X0,X1),X1)|element(X1,powerset(X0)))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f181])).
% 0.09/0.55 fof(f183,plain,(
% 0.09/0.55 ![X0,X1]: (~in(sK9_skl(X0,X1),X0)|element(X1,powerset(X0)))),
% 0.09/0.55 inference(cnf_transformation,[status(thm)],[f181])).
% 0.09/0.55 fof(f1595,plain,(
% 0.09/0.55 ![X0,X1]: (~topological_space(sK0_skl)|~element(X0,powerset(powerset(the_carrier(sK0_skl))))|~in(X1,sK7_skl(X0,sK0_skl))|in(X1,powerset(the_carrier(sK0_skl))))),
% 0.09/0.55 inference(resolution,[status(thm)],[f167,f52])).
% 0.09/0.55 fof(f1596,plain,(
% 0.09/0.55 ![X0,X1]: (~element(X0,powerset(powerset(the_carrier(sK0_skl))))|~in(X1,sK7_skl(X0,sK0_skl))|in(X1,powerset(the_carrier(sK0_skl))))),
% 0.09/0.55 inference(forward_subsumption_resolution,[status(thm)],[f1595,f51])).
% 0.09/0.55 fof(f1597,plain,(
% 0.09/0.55 ![X0,X1]: (~topological_space(sK0_skl)|~element(X0,powerset(powerset(the_carrier(sK0_skl))))|~in(X1,sK7_skl(X0,sK0_skl))|in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0))),
% 0.91/0.58 inference(resolution,[status(thm)],[f168,f52])).
% 0.91/0.58 fof(f1598,plain,(
% 0.91/0.58 ![X0,X1]: (~element(X0,powerset(powerset(the_carrier(sK0_skl))))|~in(X1,sK7_skl(X0,sK0_skl))|in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0))),
% 0.91/0.58 inference(forward_subsumption_resolution,[status(thm)],[f1597,f51])).
% 0.91/0.58 fof(f1599,plain,(
% 0.91/0.58 ![X0,X1]: (~topological_space(sK0_skl)|~element(X0,powerset(powerset(the_carrier(sK0_skl))))|in(X1,sK7_skl(X0,sK0_skl))|~in(X1,powerset(the_carrier(sK0_skl)))|~in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0))),
% 0.91/0.58 inference(resolution,[status(thm)],[f169,f52])).
% 0.91/0.58 fof(f1600,plain,(
% 0.91/0.58 ![X0,X1]: (~element(X0,powerset(powerset(the_carrier(sK0_skl))))|in(X1,sK7_skl(X0,sK0_skl))|~in(X1,powerset(the_carrier(sK0_skl)))|~in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0))),
% 0.91/0.58 inference(forward_subsumption_resolution,[status(thm)],[f1599,f51])).
% 0.91/0.58 fof(f1606,plain,(
% 0.91/0.58 ![X0]: (~in(X0,sK7_skl(sK1_skl,sK0_skl))|in(X0,powerset(the_carrier(sK0_skl))))),
% 0.91/0.58 inference(resolution,[status(thm)],[f1596,f53])).
% 0.91/0.58 fof(f1639,plain,(
% 0.91/0.58 ![X0]: (~in(X0,sK7_skl(sK1_skl,sK0_skl))|in(set_difference(cast_as_carrier_subset(sK0_skl),X0),sK1_skl))),
% 0.91/0.58 inference(resolution,[status(thm)],[f1598,f53])).
% 0.91/0.58 fof(f1645,plain,(
% 0.91/0.58 ![X0]: (in(X0,sK7_skl(sK1_skl,sK0_skl))|~in(X0,powerset(the_carrier(sK0_skl)))|~in(set_difference(cast_as_carrier_subset(sK0_skl),X0),sK1_skl))),
% 0.91/0.58 inference(resolution,[status(thm)],[f1600,f53])).
% 0.91/0.58 fof(f1734,plain,(
% 0.91/0.58 ![X0]: (in(sK9_skl(X0,sK7_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))|element(sK7_skl(sK1_skl,sK0_skl),powerset(X0)))),
% 0.91/0.58 inference(resolution,[status(thm)],[f1606,f182])).
% 0.91/0.58 fof(f2722,plain,(
% 0.91/0.58 element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl))))|element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl))))),
% 0.91/0.58 inference(resolution,[status(thm)],[f1734,f183])).
% 0.91/0.58 fof(f2725,plain,(
% 0.91/0.58 element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl))))),
% 0.91/0.58 inference(duplicate_literals_removal,[status(thm)],[f2722])).
% 0.91/0.58 fof(f2918,plain,(
% 0.91/0.58 in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),sK7_skl(sK1_skl,sK0_skl))|in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK7_skl(sK1_skl,sK0_skl))),sK1_skl)),
% 0.91/0.58 inference(resolution,[status(thm)],[f2725,f55])).
% 0.91/0.58 fof(f2919,plain,(
% 0.91/0.58 element(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))),
% 0.91/0.58 inference(resolution,[status(thm)],[f2725,f54])).
% 0.91/0.58 fof(f2928,plain,(
% 0.91/0.58 in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK7_skl(sK1_skl,sK0_skl))),sK1_skl)),
% 0.91/0.58 inference(forward_subsumption_resolution,[status(thm)],[f2918,f1639])).
% 0.91/0.58 fof(f2937,plain,(
% 0.91/0.58 empty(powerset(the_carrier(sK0_skl)))|in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))),
% 0.91/0.58 inference(resolution,[status(thm)],[f2919,f173])).
% 0.91/0.58 fof(f2938,plain,(
% 0.91/0.58 in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))),
% 0.91/0.58 inference(forward_subsumption_resolution,[status(thm)],[f2937,f162])).
% 0.91/0.58 fof(f3363,plain,(
% 0.91/0.58 ~element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl))))|~in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),sK7_skl(sK1_skl,sK0_skl))),
% 0.91/0.58 inference(resolution,[status(thm)],[f2928,f56])).
% 0.91/0.58 fof(f3364,plain,(
% 0.91/0.58 in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),sK7_skl(sK1_skl,sK0_skl))|~in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))),
% 0.91/0.58 inference(resolution,[status(thm)],[f2928,f1645])).
% 0.91/0.58 fof(f3367,plain,(
% 0.91/0.58 ~in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),sK7_skl(sK1_skl,sK0_skl))),
% 0.91/0.58 inference(forward_subsumption_resolution,[status(thm)],[f3363,f2725])).
% 0.91/0.58 fof(f3368,plain,(
% 0.91/0.58 in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),sK7_skl(sK1_skl,sK0_skl))),
% 0.91/0.58 inference(forward_subsumption_resolution,[status(thm)],[f3364,f2938])).
% 0.91/0.58 fof(f3369,plain,(
% 0.91/0.58 $false),
% 0.91/0.58 inference(forward_subsumption_resolution,[status(thm)],[f3368,f3367])).
% 0.91/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.91/0.58 % Elapsed time: 0.201772 seconds
% 0.91/0.58 % CPU time: 1.325576 seconds
% 0.91/0.58 % Total memory used: 112.851 MB
% 0.91/0.58 % Net memory used: 111.747 MB
%------------------------------------------------------------------------------