%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU310+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 : n012.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:17 PM UTC 2026
% Result : Theorem 0.04s 15.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU310+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/15.33 % Computer : n012.cluster.edu
% 0.04/15.33 % Model : x86_64 x86_64
% 0.04/15.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/15.33 % Memory : 8046.5625MB
% 0.04/15.33 % OS : Linux 6.8.0-71-generic
% 0.04/15.33 % CPULimit : 300
% 0.04/15.33 % WCLimit : 300
% 0.04/15.33 % DateTime : Mon Sep 21 06:10:23 UTC 2026
% 0.04/15.33 % CPUTime :
% 0.04/15.34 % Drodi V4.1.1
% 0.04/15.36 % Refutation found
% 0.04/15.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.04/15.36 % SZS output start CNFRefutation for theBenchmark
% 0.04/15.36 fof(f1,conjecture,(
% 0.04/15.36 (! [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.04/15.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/15.36 fof(f2,negated_conjecture,(
% 0.04/15.36 ~((! [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.04/15.36 inference(negated_conjecture,[status(cth)],[f1])).
% 0.04/15.36 fof(f24,axiom,(
% 0.04/15.36 (! [A] :( ( topological_space(A)& top_str(A) )=> (? [B] :( element(B,powerset(the_carrier(A)))& closed_subset(B,A) ) )) )),
% 0.04/15.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/15.36 fof(f35,axiom,(
% 0.04/15.36 (! [A] :( ( topological_space(A)& top_str(A) )=> closed_subset(cast_as_carrier_subset(A),A) ) )),
% 0.04/15.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/15.36 fof(f37,axiom,(
% 0.04/15.36 (! [A,B] :( ( topological_space(A)& top_str(A)& element(B,powerset(powerset(the_carrier(A)))) )=> ( (! [C,D,E] :( ( C = D& in(set_difference(cast_as_carrier_subset(A),D),B)& C = E& in(set_difference(cast_as_carrier_subset(A),E),B) )=> D = E ))=> (? [C] :(! [D] :( in(D,C)<=> (? [E] :( in(E,powerset(the_carrier(A)))& E = D& in(set_difference(cast_as_carrier_subset(A),D),B) ) )) ))) ) )),
% 0.04/15.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.04/15.36 fof(f38,plain,(
% 0.04/15.36 (?[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.04/15.36 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.04/15.36 fof(f39,plain,(
% 0.04/15.36 ?[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.04/15.36 inference(NNF_transformation,[status(thm)],[f38])).
% 0.04/15.36 fof(f40,plain,(
% 0.04/15.36 (((topological_space(sK0_skl)&top_str(sK0_skl))&element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))))&(![C]: ((in(sK2_skl(C),C)|(in(sK2_skl(C),powerset(the_carrier(sK0_skl)))&in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(C)),sK1_skl)))&(~in(sK2_skl(C),C)|(~in(sK2_skl(C),powerset(the_carrier(sK0_skl)))|~in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(C)),sK1_skl))))))),
% 0.04/15.36 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))],[f39])).
% 0.04/15.36 fof(f41,plain,(
% 0.04/15.36 topological_space(sK0_skl)),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f40])).
% 0.04/15.36 fof(f42,plain,(
% 0.04/15.36 top_str(sK0_skl)),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f40])).
% 0.04/15.36 fof(f43,plain,(
% 0.04/15.36 element(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f40])).
% 0.04/15.36 fof(f44,plain,(
% 0.04/15.36 ![X0]: (in(sK2_skl(X0),X0)|in(sK2_skl(X0),powerset(the_carrier(sK0_skl))))),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f40])).
% 0.04/15.36 fof(f45,plain,(
% 0.04/15.36 ![X0]: (in(sK2_skl(X0),X0)|in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X0)),sK1_skl))),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f40])).
% 0.04/15.36 fof(f46,plain,(
% 0.04/15.36 ![X0]: (~in(sK2_skl(X0),X0)|~in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))|~in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X0)),sK1_skl))),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f40])).
% 0.04/15.36 fof(f127,plain,(
% 0.04/15.36 ![A]: ((~topological_space(A)|~top_str(A))|(?[B]: (element(B,powerset(the_carrier(A)))&closed_subset(B,A))))),
% 0.04/15.36 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.04/15.36 fof(f128,plain,(
% 0.04/15.36 ![A]: ((~topological_space(A)|~top_str(A))|(element(sK4_skl(A),powerset(the_carrier(A)))&closed_subset(sK4_skl(A),A)))),
% 0.04/15.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f127])).
% 0.04/15.36 fof(f129,plain,(
% 0.04/15.36 ![X0]: (~topological_space(X0)|~top_str(X0)|element(sK4_skl(X0),powerset(the_carrier(X0))))),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f128])).
% 0.04/15.36 fof(f130,plain,(
% 0.04/15.36 ![X0]: (~topological_space(X0)|~top_str(X0)|closed_subset(sK4_skl(X0),X0))),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f128])).
% 0.04/15.36 fof(f150,plain,(
% 0.04/15.36 ![A]: ((~topological_space(A)|~top_str(A))|closed_subset(cast_as_carrier_subset(A),A))),
% 0.04/15.36 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.04/15.36 fof(f151,plain,(
% 0.04/15.36 ![X0]: (~topological_space(X0)|~top_str(X0)|closed_subset(cast_as_carrier_subset(X0),X0))),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f150])).
% 0.04/15.36 fof(f153,plain,(
% 0.04/15.36 ![A,B]: (((~topological_space(A)|~top_str(A))|~element(B,powerset(powerset(the_carrier(A)))))|((?[C,D,E]: ((((C=D&in(set_difference(cast_as_carrier_subset(A),D),B))&C=E)&in(set_difference(cast_as_carrier_subset(A),E),B))&~D=E))|(?[C]: ![D]: (in(D,C)<=>(?[E]: ((in(E,powerset(the_carrier(A)))&E=D)&in(set_difference(cast_as_carrier_subset(A),D),B)))))))),
% 0.04/15.36 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.04/15.36 fof(f154,definition,(
% 0.04/15.36 ![A,B,C,D,E]: (sP0_prd(E,D,C,B,A)<=>((((C=D&in(set_difference(cast_as_carrier_subset(A),D),B))&C=E)&in(set_difference(cast_as_carrier_subset(A),E),B))&~D=E))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.04/15.36 fof(f155,plain,(
% 0.04/15.36 ![A,B]: (((~topological_space(A)|~top_str(A))|~element(B,powerset(powerset(the_carrier(A)))))|((?[C,D,E]: sP0_prd(E,D,C,B,A))|(?[C]: ![D]: (in(D,C)<=>(?[E]: ((in(E,powerset(the_carrier(A)))&E=D)&in(set_difference(cast_as_carrier_subset(A),D),B)))))))),
% 0.04/15.36 inference(formula_renaming,[status(thm)],[f153,f154])).
% 0.04/15.36 fof(f156,plain,(
% 0.04/15.36 ![A,B]: (((~topological_space(A)|~top_str(A))|~element(B,powerset(powerset(the_carrier(A)))))|((?[C,D,E]: sP0_prd(E,D,C,B,A))|(?[C]: ![D]: ((~in(D,C)|(?[E]: ((in(E,powerset(the_carrier(A)))&E=D)&in(set_difference(cast_as_carrier_subset(A),D),B))))&(in(D,C)|(![E]: ((~in(E,powerset(the_carrier(A)))|~E=D)|~in(set_difference(cast_as_carrier_subset(A),D),B))))))))),
% 0.04/15.36 inference(NNF_transformation,[status(thm)],[f155])).
% 0.04/15.36 fof(f157,plain,(
% 0.04/15.36 ![A,B]: (((~topological_space(A)|~top_str(A))|~element(B,powerset(powerset(the_carrier(A)))))|((?[C,D,E]: sP0_prd(E,D,C,B,A))|(?[C]: ((![D]: (~in(D,C)|((?[E]: (in(E,powerset(the_carrier(A)))&E=D))&in(set_difference(cast_as_carrier_subset(A),D),B))))&(![D]: (in(D,C)|((![E]: (~in(E,powerset(the_carrier(A)))|~E=D))|~in(set_difference(cast_as_carrier_subset(A),D),B))))))))),
% 0.04/15.36 inference(miniscoping,[status(thm)],[f156])).
% 0.04/15.36 fof(f158,plain,(
% 0.04/15.36 ![A,B]: (((~topological_space(A)|~top_str(A))|~element(B,powerset(powerset(the_carrier(A)))))|(sP0_prd(sK9_skl(B,A),sK8_skl(B,A),sK7_skl(B,A),B,A)|((![D]: (~in(D,sK10_skl(B,A))|((in(sK11_skl(D,B,A),powerset(the_carrier(A)))&sK11_skl(D,B,A)=D)&in(set_difference(cast_as_carrier_subset(A),D),B))))&(![D]: (in(D,sK10_skl(B,A))|((![E]: (~in(E,powerset(the_carrier(A)))|~E=D))|~in(set_difference(cast_as_carrier_subset(A),D),B)))))))),
% 0.04/15.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl]),skolemize(C,sK7_skl(B,A)),skolemize(D,sK8_skl(B,A)),skolemize(E,sK9_skl(B,A)),skolemize(C,sK10_skl(B,A)),skolemize(E,sK11_skl(D,B,A))],[f157])).
% 0.04/15.36 fof(f159,plain,(
% 0.04/15.36 ![X0,X1,X2]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|sP0_prd(sK9_skl(X1,X0),sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)|~in(X2,sK10_skl(X1,X0))|in(sK11_skl(X2,X1,X0),powerset(the_carrier(X0))))),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f158])).
% 0.04/15.36 fof(f160,plain,(
% 0.04/15.36 ![X0,X1,X2]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|sP0_prd(sK9_skl(X1,X0),sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)|~in(X2,sK10_skl(X1,X0))|sK11_skl(X2,X1,X0)=X2)),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f158])).
% 0.04/15.36 fof(f161,plain,(
% 0.04/15.36 ![X0,X1,X2]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|sP0_prd(sK9_skl(X1,X0),sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)|~in(X2,sK10_skl(X1,X0))|in(set_difference(cast_as_carrier_subset(X0),X2),X1))),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f158])).
% 0.04/15.36 fof(f162,plain,(
% 0.04/15.36 ![X0,X1,X2,X3]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|sP0_prd(sK9_skl(X1,X0),sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)|in(X2,sK10_skl(X1,X0))|~in(X3,powerset(the_carrier(X0)))|~X3=X2|~in(set_difference(cast_as_carrier_subset(X0),X2),X1))),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f158])).
% 0.04/15.36 fof(f163,plain,(
% 0.04/15.36 ![A,B,C,D,E]: ((~sP0_prd(E,D,C,B,A)|((((C=D&in(set_difference(cast_as_carrier_subset(A),D),B))&C=E)&in(set_difference(cast_as_carrier_subset(A),E),B))&~D=E))&(sP0_prd(E,D,C,B,A)|((((~C=D|~in(set_difference(cast_as_carrier_subset(A),D),B))|~C=E)|~in(set_difference(cast_as_carrier_subset(A),E),B))|D=E)))),
% 0.04/15.36 inference(NNF_transformation,[status(thm)],[f154])).
% 0.04/15.36 fof(f164,plain,(
% 0.04/15.36 (![A,B,C,D,E]: (~sP0_prd(E,D,C,B,A)|((((C=D&in(set_difference(cast_as_carrier_subset(A),D),B))&C=E)&in(set_difference(cast_as_carrier_subset(A),E),B))&~D=E)))&(![A,B,C,D,E]: (sP0_prd(E,D,C,B,A)|((((~C=D|~in(set_difference(cast_as_carrier_subset(A),D),B))|~C=E)|~in(set_difference(cast_as_carrier_subset(A),E),B))|D=E)))),
% 0.04/15.36 inference(miniscoping,[status(thm)],[f163])).
% 0.04/15.36 fof(f165,plain,(
% 0.04/15.36 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|X2=X1)),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f164])).
% 0.04/15.36 fof(f167,plain,(
% 0.04/15.36 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|X2=X0)),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f164])).
% 0.04/15.36 fof(f169,plain,(
% 0.04/15.36 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|~X1=X0)),
% 0.04/15.36 inference(cnf_transformation,[status(thm)],[f164])).
% 0.04/15.36 fof(f171,plain,(
% 0.04/15.36 ![X0,X1,X2]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|sP0_prd(sK9_skl(X1,X0),sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)|in(X2,sK10_skl(X1,X0))|~in(X2,powerset(the_carrier(X0)))|~in(set_difference(cast_as_carrier_subset(X0),X2),X1))),
% 0.04/15.36 inference(destructive_equality_resolution,[status(thm)],[f162])).
% 0.04/15.36 fof(f172,plain,(
% 0.04/15.36 ![X0,X1,X2,X3]: (~sP0_prd(X0,X0,X1,X2,X3))),
% 0.04/15.36 inference(destructive_equality_resolution,[status(thm)],[f169])).
% 0.04/15.36 fof(f432,plain,(
% 0.04/15.36 ~topological_space(sK0_skl)|element(sK4_skl(sK0_skl),powerset(the_carrier(sK0_skl)))),
% 0.04/15.36 inference(resolution,[status(thm)],[f129,f42])).
% 0.04/15.36 fof(f433,definition,(
% 0.04/15.36 sQ20_spl <=> (topological_space(sK0_skl))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f435,plain,(
% 0.04/15.36 ~topological_space(sK0_skl)|sQ20_spl),
% 0.04/15.36 inference(component_clause,[status(thm)],[f433])).
% 0.04/15.36 fof(f436,definition,(
% 0.04/15.36 sQ21_spl <=> (element(sK4_skl(sK0_skl),powerset(the_carrier(sK0_skl))))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f439,plain,(
% 0.04/15.36 ~sQ20_spl|sQ21_spl),
% 0.04/15.36 inference(split_clause,[status(thm)],[f432,f433,f436])).
% 0.04/15.36 fof(f440,plain,(
% 0.04/15.36 $false|sQ20_spl),
% 0.04/15.36 inference(forward_subsumption_resolution,[status(thm)],[f435,f41])).
% 0.04/15.36 fof(f441,plain,(
% 0.04/15.36 sQ20_spl),
% 0.04/15.36 inference(contradiction_clause,[status(thm)],[f440])).
% 0.04/15.36 fof(f567,plain,(
% 0.04/15.36 ~topological_space(sK0_skl)|closed_subset(sK4_skl(sK0_skl),sK0_skl)),
% 0.04/15.36 inference(resolution,[status(thm)],[f130,f42])).
% 0.04/15.36 fof(f568,definition,(
% 0.04/15.36 sQ37_spl <=> (closed_subset(sK4_skl(sK0_skl),sK0_skl))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f571,plain,(
% 0.04/15.36 ~sQ20_spl|sQ37_spl),
% 0.04/15.36 inference(split_clause,[status(thm)],[f567,f433,f568])).
% 0.04/15.36 fof(f603,plain,(
% 0.04/15.36 ~topological_space(sK0_skl)|closed_subset(cast_as_carrier_subset(sK0_skl),sK0_skl)),
% 0.04/15.36 inference(resolution,[status(thm)],[f151,f42])).
% 0.04/15.36 fof(f604,definition,(
% 0.04/15.36 sQ38_spl <=> (closed_subset(cast_as_carrier_subset(sK0_skl),sK0_skl))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f607,plain,(
% 0.04/15.36 ~sQ20_spl|sQ38_spl),
% 0.04/15.36 inference(split_clause,[status(thm)],[f603,f433,f604])).
% 0.04/15.36 fof(f610,plain,(
% 0.04/15.36 ![X0]: (~topological_space(sK0_skl)|~top_str(sK0_skl)|sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~in(X0,sK10_skl(sK1_skl,sK0_skl))|in(sK11_skl(X0,sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl))))),
% 0.04/15.36 inference(resolution,[status(thm)],[f159,f43])).
% 0.04/15.36 fof(f612,definition,(
% 0.04/15.36 sQ39_spl <=> (top_str(sK0_skl))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f614,plain,(
% 0.04/15.36 ~top_str(sK0_skl)|sQ39_spl),
% 0.04/15.36 inference(component_clause,[status(thm)],[f612])).
% 0.04/15.36 fof(f615,definition,(
% 0.04/15.36 sQ40_spl <=> (sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f616,plain,(
% 0.04/15.36 sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~sQ40_spl),
% 0.04/15.36 inference(component_clause,[status(thm)],[f615])).
% 0.04/15.36 fof(f618,definition,(
% 0.04/15.36 ![X0]: (sQ41_spl <=> (~in(X0,sK10_skl(sK1_skl,sK0_skl))|in(sK11_skl(X0,sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl)))))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f619,plain,(
% 0.04/15.36 ![X0]: (~in(X0,sK10_skl(sK1_skl,sK0_skl))|in(sK11_skl(X0,sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl)))|~sQ41_spl)),
% 0.04/15.36 inference(component_clause,[status(thm)],[f618])).
% 0.04/15.36 fof(f621,plain,(
% 0.04/15.36 ~sQ20_spl|~sQ39_spl|sQ40_spl|sQ41_spl),
% 0.04/15.36 inference(split_clause,[status(thm)],[f610,f433,f612,f615,f618])).
% 0.04/15.36 fof(f624,plain,(
% 0.04/15.36 ![X0]: (~topological_space(sK0_skl)|~top_str(sK0_skl)|sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~in(X0,sK10_skl(sK1_skl,sK0_skl))|sK11_skl(X0,sK1_skl,sK0_skl)=X0)),
% 0.04/15.36 inference(resolution,[status(thm)],[f160,f43])).
% 0.04/15.36 fof(f626,definition,(
% 0.04/15.36 ![X0]: (sQ42_spl <=> (~in(X0,sK10_skl(sK1_skl,sK0_skl))|sK11_skl(X0,sK1_skl,sK0_skl)=X0))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f627,plain,(
% 0.04/15.36 ![X0]: (~in(X0,sK10_skl(sK1_skl,sK0_skl))|sK11_skl(X0,sK1_skl,sK0_skl)=X0|~sQ42_spl)),
% 0.04/15.36 inference(component_clause,[status(thm)],[f626])).
% 0.04/15.36 fof(f629,plain,(
% 0.04/15.36 ~sQ20_spl|~sQ39_spl|sQ40_spl|sQ42_spl),
% 0.04/15.36 inference(split_clause,[status(thm)],[f624,f433,f612,f615,f626])).
% 0.04/15.36 fof(f735,plain,(
% 0.04/15.36 ![X0]: (~topological_space(sK0_skl)|~top_str(sK0_skl)|sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~in(X0,sK10_skl(sK1_skl,sK0_skl))|in(set_difference(cast_as_carrier_subset(sK0_skl),X0),sK1_skl))),
% 0.04/15.36 inference(resolution,[status(thm)],[f161,f43])).
% 0.04/15.36 fof(f737,definition,(
% 0.04/15.36 ![X0]: (sQ53_spl <=> (~in(X0,sK10_skl(sK1_skl,sK0_skl))|in(set_difference(cast_as_carrier_subset(sK0_skl),X0),sK1_skl)))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f738,plain,(
% 0.04/15.36 ![X0]: (~in(X0,sK10_skl(sK1_skl,sK0_skl))|in(set_difference(cast_as_carrier_subset(sK0_skl),X0),sK1_skl)|~sQ53_spl)),
% 0.04/15.36 inference(component_clause,[status(thm)],[f737])).
% 0.04/15.36 fof(f740,plain,(
% 0.04/15.36 ~sQ20_spl|~sQ39_spl|sQ40_spl|sQ53_spl),
% 0.04/15.36 inference(split_clause,[status(thm)],[f735,f433,f612,f615,f737])).
% 0.04/15.36 fof(f741,plain,(
% 0.04/15.36 ![X0]: (~topological_space(sK0_skl)|~top_str(sK0_skl)|~element(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))|sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK2_skl(X0),sK10_skl(sK1_skl,sK0_skl))|~in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))|in(sK2_skl(X0),X0))),
% 0.04/15.36 inference(resolution,[status(thm)],[f171,f45])).
% 0.04/15.36 fof(f742,definition,(
% 0.04/15.36 sQ54_spl <=> (element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f744,plain,(
% 0.04/15.36 ~element(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))|sQ54_spl),
% 0.04/15.36 inference(component_clause,[status(thm)],[f742])).
% 0.04/15.36 fof(f745,definition,(
% 0.04/15.36 ![X0]: (sQ55_spl <=> (in(sK2_skl(X0),sK10_skl(sK1_skl,sK0_skl))|~in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))|in(sK2_skl(X0),X0)))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f746,plain,(
% 0.04/15.36 ![X0]: (in(sK2_skl(X0),sK10_skl(sK1_skl,sK0_skl))|~in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))|in(sK2_skl(X0),X0)|~sQ55_spl)),
% 0.04/15.36 inference(component_clause,[status(thm)],[f745])).
% 0.04/15.36 fof(f748,plain,(
% 0.04/15.36 ~sQ20_spl|~sQ39_spl|~sQ54_spl|sQ40_spl|sQ55_spl),
% 0.04/15.36 inference(split_clause,[status(thm)],[f741,f433,f612,f742,f615,f745])).
% 0.04/15.36 fof(f749,plain,(
% 0.04/15.36 sK7_skl(sK1_skl,sK0_skl)=sK8_skl(sK1_skl,sK0_skl)|~sQ40_spl),
% 0.04/15.36 inference(resolution,[status(thm)],[f165,f616])).
% 0.04/15.36 fof(f750,plain,(
% 0.04/15.36 sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~sQ40_spl),
% 0.04/15.36 inference(backward_demodulation,[status(thm)],[f749,f616])).
% 0.04/15.36 fof(f753,plain,(
% 0.04/15.36 sK7_skl(sK1_skl,sK0_skl)=sK9_skl(sK1_skl,sK0_skl)|~sQ40_spl),
% 0.04/15.36 inference(resolution,[status(thm)],[f750,f167])).
% 0.04/15.36 fof(f757,plain,(
% 0.04/15.36 sP0_prd(sK7_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~sQ40_spl),
% 0.04/15.36 inference(backward_demodulation,[status(thm)],[f753,f750])).
% 0.04/15.36 fof(f760,plain,(
% 0.04/15.36 $false|~sQ40_spl),
% 0.04/15.36 inference(forward_subsumption_resolution,[status(thm)],[f757,f172])).
% 0.04/15.36 fof(f761,plain,(
% 0.04/15.36 ~sQ40_spl),
% 0.04/15.36 inference(contradiction_clause,[status(thm)],[f760])).
% 0.04/15.36 fof(f762,plain,(
% 0.04/15.36 $false|sQ39_spl),
% 0.04/15.36 inference(forward_subsumption_resolution,[status(thm)],[f614,f42])).
% 0.04/15.36 fof(f763,plain,(
% 0.04/15.36 sQ39_spl),
% 0.04/15.36 inference(contradiction_clause,[status(thm)],[f762])).
% 0.04/15.36 fof(f764,plain,(
% 0.04/15.36 $false|sQ54_spl),
% 0.04/15.36 inference(forward_subsumption_resolution,[status(thm)],[f744,f43])).
% 0.04/15.36 fof(f765,plain,(
% 0.04/15.36 sQ54_spl),
% 0.04/15.36 inference(contradiction_clause,[status(thm)],[f764])).
% 0.04/15.36 fof(f766,plain,(
% 0.04/15.36 ![X0]: (in(sK2_skl(X0),sK10_skl(sK1_skl,sK0_skl))|in(sK2_skl(X0),X0)|~sQ55_spl)),
% 0.04/15.36 inference(forward_subsumption_resolution,[status(thm)],[f746,f44])).
% 0.04/15.36 fof(f769,plain,(
% 0.04/15.36 in(sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl)))|in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))|~sQ41_spl),
% 0.04/15.36 inference(resolution,[status(thm)],[f619,f44])).
% 0.04/15.36 fof(f770,definition,(
% 0.04/15.36 sQ56_spl <=> (in(sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl))))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f771,plain,(
% 0.04/15.36 in(sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl)))|~sQ56_spl),
% 0.04/15.36 inference(component_clause,[status(thm)],[f770])).
% 0.04/15.36 fof(f773,definition,(
% 0.04/15.36 sQ57_spl <=> (in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK10_skl(sK1_skl,sK0_skl))),sK1_skl))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f774,plain,(
% 0.04/15.36 in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK10_skl(sK1_skl,sK0_skl))),sK1_skl)|~sQ57_spl),
% 0.04/15.36 inference(component_clause,[status(thm)],[f773])).
% 0.04/15.36 fof(f777,definition,(
% 0.04/15.36 sQ58_spl <=> (in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl))))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f779,plain,(
% 0.04/15.36 ~in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))|sQ58_spl),
% 0.04/15.36 inference(component_clause,[status(thm)],[f777])).
% 0.04/15.36 fof(f780,plain,(
% 0.04/15.36 sQ56_spl|sQ58_spl|~sQ41_spl),
% 0.04/15.36 inference(split_clause,[status(thm)],[f769,f770,f777,f618])).
% 0.04/15.36 fof(f782,plain,(
% 0.04/15.36 sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK10_skl(sK1_skl,sK0_skl))|in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))|~sQ42_spl),
% 0.04/15.36 inference(resolution,[status(thm)],[f627,f44])).
% 0.04/15.36 fof(f783,definition,(
% 0.04/15.36 sQ59_spl <=> (sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK10_skl(sK1_skl,sK0_skl)))),
% 0.04/15.36 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.04/15.36 fof(f784,plain,(
% 0.04/15.36 sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK10_skl(sK1_skl,sK0_skl))|~sQ59_spl),
% 0.04/15.36 inference(component_clause,[status(thm)],[f783])).
% 0.04/15.36 fof(f787,plain,(
% 0.04/15.36 sQ59_spl|sQ58_spl|~sQ42_spl),
% 0.04/15.36 inference(split_clause,[status(thm)],[f782,f783,f777,f626])).
% 0.04/15.36 fof(f788,plain,(
% 0.04/15.36 in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))|~sQ59_spl|~sQ56_spl),
% 0.04/15.36 inference(backward_demodulation,[status(thm)],[f784,f771])).
% 0.04/15.36 fof(f789,plain,(
% 0.04/15.36 in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK10_skl(sK1_skl,sK0_skl))),sK1_skl)|in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK10_skl(sK1_skl,sK0_skl))),sK1_skl)|~sQ53_spl),
% 0.04/15.37 inference(resolution,[status(thm)],[f738,f45])).
% 0.04/15.37 fof(f791,plain,(
% 0.04/15.37 sQ57_spl|~sQ53_spl),
% 0.04/15.37 inference(split_clause,[status(thm)],[f789,f773,f737])).
% 0.04/15.37 fof(f802,plain,(
% 0.04/15.37 in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK10_skl(sK1_skl,sK0_skl))|sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK2_skl(sK10_skl(sK1_skl,sK0_skl))|~sQ55_spl|~sQ42_spl),
% 0.04/15.37 inference(resolution,[status(thm)],[f766,f627])).
% 0.04/15.37 fof(f803,plain,(
% 0.04/15.37 in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK10_skl(sK1_skl,sK0_skl))|in(sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl)))|~sQ55_spl|~sQ41_spl),
% 0.04/15.37 inference(resolution,[status(thm)],[f766,f619])).
% 0.04/15.37 fof(f807,definition,(
% 0.04/15.37 sQ60_spl <=> (in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK10_skl(sK1_skl,sK0_skl)))),
% 0.04/15.37 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.04/15.37 fof(f811,plain,(
% 0.04/15.37 sQ60_spl|sQ59_spl|~sQ55_spl|~sQ42_spl),
% 0.04/15.37 inference(split_clause,[status(thm)],[f802,f807,f783,f745,f626])).
% 0.04/15.37 fof(f812,plain,(
% 0.04/15.37 sQ60_spl|sQ56_spl|~sQ55_spl|~sQ41_spl),
% 0.04/15.37 inference(split_clause,[status(thm)],[f803,f807,f770,f745,f618])).
% 0.04/15.37 fof(f823,plain,(
% 0.04/15.37 ~in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK10_skl(sK1_skl,sK0_skl))|~in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))|~sQ57_spl),
% 0.04/15.37 inference(resolution,[status(thm)],[f774,f46])).
% 0.04/15.37 fof(f824,plain,(
% 0.04/15.37 ~topological_space(sK0_skl)|~top_str(sK0_skl)|~element(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))|sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK10_skl(sK1_skl,sK0_skl))|~in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))|~sQ57_spl),
% 0.04/15.37 inference(resolution,[status(thm)],[f774,f171])).
% 0.04/15.37 fof(f826,plain,(
% 0.04/15.37 ~sQ60_spl|~sQ58_spl|~sQ57_spl),
% 0.04/15.37 inference(split_clause,[status(thm)],[f823,f807,f777,f773])).
% 0.04/15.37 fof(f827,plain,(
% 0.04/15.37 ~sQ20_spl|~sQ39_spl|~sQ54_spl|sQ40_spl|sQ60_spl|~sQ58_spl|~sQ57_spl),
% 0.04/15.37 inference(split_clause,[status(thm)],[f824,f433,f612,f742,f615,f807,f777,f773])).
% 0.04/15.37 fof(f828,plain,(
% 0.04/15.37 $false|~sQ59_spl|~sQ56_spl|sQ58_spl),
% 0.04/15.37 inference(forward_subsumption_resolution,[status(thm)],[f779,f788])).
% 0.04/15.37 fof(f829,plain,(
% 0.04/15.37 ~sQ59_spl|~sQ56_spl|sQ58_spl),
% 0.04/15.37 inference(contradiction_clause,[status(thm)],[f828])).
% 0.04/15.37 fof(f830,plain,(
% 0.04/15.37 $false),
% 0.04/15.37 inference(sat_refutation,[status(thm)],[f439,f441,f571,f607,f621,f629,f740,f748,f761,f763,f765,f780,f787,f791,f811,f812,f826,f827,f829])).
% 0.04/15.37 % SZS output end CNFRefutation for theBenchmark.p
% 0.04/15.38 % Elapsed time: 0.044869 seconds
% 0.04/15.38 % CPU time: 0.166786 seconds
% 0.04/15.38 % Total memory used: 86.707 MB
% 0.04/15.38 % Net memory used: 86.504 MB
%------------------------------------------------------------------------------