%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU318+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 : n007.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 71.61s 9.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU318+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n007.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 06:09:05 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 71.61/9.59 % Refutation found
% 71.61/9.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 71.61/9.59 % SZS output start CNFRefutation for theBenchmark
% 71.61/9.59 fof(f17,axiom,(
% 71.61/9.59 (! [A,B] :( A = B<=> ( subset(A,B)& subset(B,A) ) ) )),
% 71.61/9.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 71.61/9.59 fof(f18,axiom,(
% 71.61/9.59 (! [A,B] :( subset(A,B)<=> (! [C] :( in(C,A)=> in(C,B) ) )) )),
% 71.61/9.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 71.61/9.59 fof(f22,axiom,(
% 71.61/9.59 (! [A,B] :( ( top_str(A)& element(B,powerset(the_carrier(A))) )=> element(topstr_closure(A,B),powerset(the_carrier(A))) ) )),
% 71.61/9.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 71.61/9.59 fof(f41,axiom,(
% 71.61/9.59 (! [A,B] :( element(A,powerset(B))<=> subset(A,B) ) )),
% 71.61/9.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 71.61/9.59 fof(f42,axiom,(
% 71.61/9.59 (! [A] :( ( topological_space(A)& top_str(A) )=> (! [B] :( element(B,powerset(powerset(the_carrier(A))))=> ( (! [C] :( element(C,powerset(the_carrier(A)))=> ( in(C,B)=> closed_subset(C,A) ) ))=> closed_subset(meet_of_subsets(the_carrier(A),B),A) ) ) )) )),
% 71.61/9.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 71.61/9.59 fof(f43,axiom,(
% 71.61/9.59 (! [A] :( top_str(A)=> (! [B] :( element(B,powerset(the_carrier(A)))=> (! [C] :( in(C,the_carrier(A))=> ( in(C,topstr_closure(A,B))<=> (! [D] :( element(D,powerset(the_carrier(A)))=> ( ( closed_subset(D,A)& subset(B,D) )=> in(C,D) ) ) )) ) )) )) )),
% 71.61/9.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 71.61/9.59 fof(f44,axiom,(
% 71.61/9.59 (! [A] :( ( topological_space(A)& top_str(A) )=> (! [B] :( element(B,powerset(the_carrier(A)))=> (? [C] :( element(C,powerset(powerset(the_carrier(A))))& (! [D] :( element(D,powerset(the_carrier(A)))=> ( in(D,C)<=> ( closed_subset(D,A)& subset(B,D) ) ) ))& topstr_closure(A,B) = meet_of_subsets(the_carrier(A),C) ) )) )) )),
% 71.61/9.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 71.61/9.59 fof(f45,axiom,(
% 71.61/9.59 (! [A] :( top_str(A)=> (! [B] :( element(B,powerset(the_carrier(A)))=> subset(B,topstr_closure(A,B)) ) )) )),
% 71.61/9.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 71.61/9.59 fof(f47,conjecture,(
% 71.61/9.59 (! [A] :( top_str(A)=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( ( closed_subset(B,A)=> topstr_closure(A,B) = B )& ( ( topological_space(A)& topstr_closure(A,B) = B )=> closed_subset(B,A) ) ) ) )) )),
% 71.61/9.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 71.61/9.59 fof(f48,negated_conjecture,(
% 71.61/9.59 ~((! [A] :( top_str(A)=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( ( closed_subset(B,A)=> topstr_closure(A,B) = B )& ( ( topological_space(A)& topstr_closure(A,B) = B )=> closed_subset(B,A) ) ) ) )) ))),
% 71.61/9.59 inference(negated_conjecture,[status(cth)],[f47])).
% 71.61/9.59 fof(f109,plain,(
% 71.61/9.59 ![A,B]: ((~A=B|(subset(A,B)&subset(B,A)))&(A=B|(~subset(A,B)|~subset(B,A))))),
% 71.61/9.59 inference(NNF_transformation,[status(thm)],[f17])).
% 71.61/9.59 fof(f110,plain,(
% 71.61/9.59 (![A,B]: (~A=B|(subset(A,B)&subset(B,A))))&(![A,B]: (A=B|(~subset(A,B)|~subset(B,A))))),
% 71.61/9.59 inference(miniscoping,[status(thm)],[f109])).
% 71.61/9.59 fof(f111,plain,(
% 71.61/9.59 ![X0,X1]: (~X0=X1|subset(X0,X1))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f110])).
% 71.61/9.59 fof(f113,plain,(
% 71.61/9.59 ![X0,X1]: (X0=X1|~subset(X0,X1)|~subset(X1,X0))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f110])).
% 71.61/9.59 fof(f114,plain,(
% 71.61/9.59 ![A,B]: (subset(A,B)<=>(![C]: (~in(C,A)|in(C,B))))),
% 71.61/9.59 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 71.61/9.59 fof(f115,plain,(
% 71.61/9.59 ![A,B]: ((~subset(A,B)|(![C]: (~in(C,A)|in(C,B))))&(subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 71.61/9.59 inference(NNF_transformation,[status(thm)],[f114])).
% 71.61/9.59 fof(f116,plain,(
% 71.61/9.59 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 71.61/9.59 inference(miniscoping,[status(thm)],[f115])).
% 71.61/9.59 fof(f117,plain,(
% 71.61/9.59 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(in(sK0_skl(B,A),A)&~in(sK0_skl(B,A),B))))),
% 71.61/9.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f116])).
% 71.61/9.59 fof(f118,plain,(
% 71.61/9.59 ![X0,X1,X2]: (~subset(X0,X1)|~in(X2,X0)|in(X2,X1))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f117])).
% 71.61/9.59 fof(f119,plain,(
% 71.61/9.59 ![X0,X1]: (subset(X0,X1)|in(sK0_skl(X1,X0),X0))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f117])).
% 71.61/9.59 fof(f120,plain,(
% 71.61/9.59 ![X0,X1]: (subset(X0,X1)|~in(sK0_skl(X1,X0),X1))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f117])).
% 71.61/9.59 fof(f121,plain,(
% 71.61/9.59 ![A,B]: ((~top_str(A)|~element(B,powerset(the_carrier(A))))|element(topstr_closure(A,B),powerset(the_carrier(A))))),
% 71.61/9.59 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 71.61/9.59 fof(f122,plain,(
% 71.61/9.59 ![X0,X1]: (~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|element(topstr_closure(X0,X1),powerset(the_carrier(X0))))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f121])).
% 71.61/9.59 fof(f166,plain,(
% 71.61/9.59 ![A,B]: ((~element(A,powerset(B))|subset(A,B))&(element(A,powerset(B))|~subset(A,B)))),
% 71.61/9.59 inference(NNF_transformation,[status(thm)],[f41])).
% 71.61/9.59 fof(f167,plain,(
% 71.61/9.59 (![A,B]: (~element(A,powerset(B))|subset(A,B)))&(![A,B]: (element(A,powerset(B))|~subset(A,B)))),
% 71.61/9.59 inference(miniscoping,[status(thm)],[f166])).
% 71.61/9.59 fof(f168,plain,(
% 71.61/9.59 ![X0,X1]: (~element(X0,powerset(X1))|subset(X0,X1))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f167])).
% 71.61/9.59 fof(f170,plain,(
% 71.61/9.59 ![A]: ((~topological_space(A)|~top_str(A))|(![B]: (~element(B,powerset(powerset(the_carrier(A))))|((?[C]: (element(C,powerset(the_carrier(A)))&(in(C,B)&~closed_subset(C,A))))|closed_subset(meet_of_subsets(the_carrier(A),B),A)))))),
% 71.61/9.59 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 71.61/9.59 fof(f171,plain,(
% 71.61/9.59 ![A]: ((~topological_space(A)|~top_str(A))|(![B]: (~element(B,powerset(powerset(the_carrier(A))))|((element(sK8_skl(B,A),powerset(the_carrier(A)))&(in(sK8_skl(B,A),B)&~closed_subset(sK8_skl(B,A),A)))|closed_subset(meet_of_subsets(the_carrier(A),B),A)))))),
% 71.61/9.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(C,sK8_skl(B,A))],[f170])).
% 71.61/9.59 fof(f172,plain,(
% 71.61/9.59 ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|element(sK8_skl(X1,X0),powerset(the_carrier(X0)))|closed_subset(meet_of_subsets(the_carrier(X0),X1),X0))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f171])).
% 71.61/9.59 fof(f173,plain,(
% 71.61/9.59 ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|in(sK8_skl(X1,X0),X1)|closed_subset(meet_of_subsets(the_carrier(X0),X1),X0))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f171])).
% 71.61/9.59 fof(f174,plain,(
% 71.61/9.59 ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|~closed_subset(sK8_skl(X1,X0),X0)|closed_subset(meet_of_subsets(the_carrier(X0),X1),X0))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f171])).
% 71.61/9.59 fof(f175,plain,(
% 71.61/9.59 ![A]: (~top_str(A)|(![B]: (~element(B,powerset(the_carrier(A)))|(![C]: (~in(C,the_carrier(A))|(in(C,topstr_closure(A,B))<=>(![D]: (~element(D,powerset(the_carrier(A)))|((~closed_subset(D,A)|~subset(B,D))|in(C,D))))))))))),
% 71.61/9.59 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 71.61/9.59 fof(f176,plain,(
% 71.61/9.59 ![A]: (~top_str(A)|(![B]: (~element(B,powerset(the_carrier(A)))|(![C]: (~in(C,the_carrier(A))|((~in(C,topstr_closure(A,B))|(![D]: (~element(D,powerset(the_carrier(A)))|((~closed_subset(D,A)|~subset(B,D))|in(C,D)))))&(in(C,topstr_closure(A,B))|(?[D]: (element(D,powerset(the_carrier(A)))&((closed_subset(D,A)&subset(B,D))&~in(C,D)))))))))))),
% 71.61/9.59 inference(NNF_transformation,[status(thm)],[f175])).
% 71.61/9.59 fof(f177,plain,(
% 71.61/9.59 ![A]: (~top_str(A)|(![B]: (~element(B,powerset(the_carrier(A)))|(![C]: (~in(C,the_carrier(A))|((~in(C,topstr_closure(A,B))|(![D]: (~element(D,powerset(the_carrier(A)))|((~closed_subset(D,A)|~subset(B,D))|in(C,D)))))&(in(C,topstr_closure(A,B))|(element(sK9_skl(C,B,A),powerset(the_carrier(A)))&((closed_subset(sK9_skl(C,B,A),A)&subset(B,sK9_skl(C,B,A)))&~in(C,sK9_skl(C,B,A)))))))))))),
% 71.61/9.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(D,sK9_skl(C,B,A))],[f176])).
% 71.61/9.59 fof(f178,plain,(
% 71.61/9.59 ![X0,X1,X2,X3]: (~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~in(X2,the_carrier(X0))|~in(X2,topstr_closure(X0,X1))|~element(X3,powerset(the_carrier(X0)))|~closed_subset(X3,X0)|~subset(X1,X3)|in(X2,X3))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f177])).
% 71.61/9.59 fof(f183,plain,(
% 71.61/9.59 ![A]: ((~topological_space(A)|~top_str(A))|(![B]: (~element(B,powerset(the_carrier(A)))|(?[C]: ((element(C,powerset(powerset(the_carrier(A))))&(![D]: (~element(D,powerset(the_carrier(A)))|(in(D,C)<=>(closed_subset(D,A)&subset(B,D))))))&topstr_closure(A,B)=meet_of_subsets(the_carrier(A),C))))))),
% 71.61/9.59 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 71.61/9.59 fof(f184,plain,(
% 71.61/9.59 ![A]: ((~topological_space(A)|~top_str(A))|(![B]: (~element(B,powerset(the_carrier(A)))|(?[C]: ((element(C,powerset(powerset(the_carrier(A))))&(![D]: (~element(D,powerset(the_carrier(A)))|((~in(D,C)|(closed_subset(D,A)&subset(B,D)))&(in(D,C)|(~closed_subset(D,A)|~subset(B,D)))))))&topstr_closure(A,B)=meet_of_subsets(the_carrier(A),C))))))),
% 71.61/9.59 inference(NNF_transformation,[status(thm)],[f183])).
% 71.61/9.59 fof(f185,plain,(
% 71.61/9.59 ![A]: ((~topological_space(A)|~top_str(A))|(![B]: (~element(B,powerset(the_carrier(A)))|((element(sK10_skl(B,A),powerset(powerset(the_carrier(A))))&(![D]: (~element(D,powerset(the_carrier(A)))|((~in(D,sK10_skl(B,A))|(closed_subset(D,A)&subset(B,D)))&(in(D,sK10_skl(B,A))|(~closed_subset(D,A)|~subset(B,D)))))))&topstr_closure(A,B)=meet_of_subsets(the_carrier(A),sK10_skl(B,A))))))),
% 71.61/9.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(C,sK10_skl(B,A))],[f184])).
% 71.61/9.59 fof(f186,plain,(
% 71.61/9.59 ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|element(sK10_skl(X1,X0),powerset(powerset(the_carrier(X0)))))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f185])).
% 71.61/9.59 fof(f187,plain,(
% 71.61/9.59 ![X0,X1,X2]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|~element(X2,powerset(the_carrier(X0)))|~in(X2,sK10_skl(X1,X0))|closed_subset(X2,X0))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f185])).
% 71.61/9.59 fof(f190,plain,(
% 71.61/9.59 ![X0,X1]: (~topological_space(X0)|~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|topstr_closure(X0,X1)=meet_of_subsets(the_carrier(X0),sK10_skl(X1,X0)))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f185])).
% 71.61/9.59 fof(f191,plain,(
% 71.61/9.59 ![A]: (~top_str(A)|(![B]: (~element(B,powerset(the_carrier(A)))|subset(B,topstr_closure(A,B)))))),
% 71.61/9.59 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 71.61/9.59 fof(f192,plain,(
% 71.61/9.59 ![X0,X1]: (~top_str(X0)|~element(X1,powerset(the_carrier(X0)))|subset(X1,topstr_closure(X0,X1)))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f191])).
% 71.61/9.59 fof(f196,plain,(
% 71.61/9.59 (?[A]: (top_str(A)&(?[B]: (element(B,powerset(the_carrier(A)))&((closed_subset(B,A)&~topstr_closure(A,B)=B)|((topological_space(A)&topstr_closure(A,B)=B)&~closed_subset(B,A)))))))),
% 71.61/9.59 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 71.61/9.59 fof(f197,definition,(
% 71.61/9.59 ![A,B]: (sP0_prd(B,A)<=>(closed_subset(B,A)&~topstr_closure(A,B)=B))),
% 71.61/9.59 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 71.61/9.59 fof(f198,plain,(
% 71.61/9.59 ?[A]: (top_str(A)&(?[B]: (element(B,powerset(the_carrier(A)))&(sP0_prd(B,A)|((topological_space(A)&topstr_closure(A,B)=B)&~closed_subset(B,A))))))),
% 71.61/9.59 inference(formula_renaming,[status(thm)],[f196,f197])).
% 71.61/9.59 fof(f199,plain,(
% 71.61/9.59 (top_str(sK11_skl)&(element(sK12_skl,powerset(the_carrier(sK11_skl)))&(sP0_prd(sK12_skl,sK11_skl)|((topological_space(sK11_skl)&topstr_closure(sK11_skl,sK12_skl)=sK12_skl)&~closed_subset(sK12_skl,sK11_skl)))))),
% 71.61/9.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl]),skolemize(A,sK11_skl),skolemize(B,sK12_skl)],[f198])).
% 71.61/9.59 fof(f200,plain,(
% 71.61/9.59 top_str(sK11_skl)),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f199])).
% 71.61/9.59 fof(f201,plain,(
% 71.61/9.59 element(sK12_skl,powerset(the_carrier(sK11_skl)))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f199])).
% 71.61/9.59 fof(f202,plain,(
% 71.61/9.59 sP0_prd(sK12_skl,sK11_skl)|topological_space(sK11_skl)),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f199])).
% 71.61/9.59 fof(f203,plain,(
% 71.61/9.59 sP0_prd(sK12_skl,sK11_skl)|topstr_closure(sK11_skl,sK12_skl)=sK12_skl),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f199])).
% 71.61/9.59 fof(f204,plain,(
% 71.61/9.59 sP0_prd(sK12_skl,sK11_skl)|~closed_subset(sK12_skl,sK11_skl)),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f199])).
% 71.61/9.59 fof(f216,plain,(
% 71.61/9.59 ![A,B]: ((~sP0_prd(B,A)|(closed_subset(B,A)&~topstr_closure(A,B)=B))&(sP0_prd(B,A)|(~closed_subset(B,A)|topstr_closure(A,B)=B)))),
% 71.61/9.59 inference(NNF_transformation,[status(thm)],[f197])).
% 71.61/9.59 fof(f217,plain,(
% 71.61/9.59 (![A,B]: (~sP0_prd(B,A)|(closed_subset(B,A)&~topstr_closure(A,B)=B)))&(![A,B]: (sP0_prd(B,A)|(~closed_subset(B,A)|topstr_closure(A,B)=B)))),
% 71.61/9.59 inference(miniscoping,[status(thm)],[f216])).
% 71.61/9.59 fof(f218,plain,(
% 71.61/9.59 ![X0,X1]: (~sP0_prd(X0,X1)|closed_subset(X0,X1))),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f217])).
% 71.61/9.59 fof(f219,plain,(
% 71.61/9.59 ![X0,X1]: (~sP0_prd(X0,X1)|~topstr_closure(X1,X0)=X0)),
% 71.61/9.59 inference(cnf_transformation,[status(thm)],[f217])).
% 71.61/9.59 fof(f221,plain,(
% 71.61/9.59 ![X0]: (subset(X0,X0))),
% 71.61/9.59 inference(destructive_equality_resolution,[status(thm)],[f111])).
% 71.61/9.59 fof(f224,plain,(
% 71.61/9.59 ~top_str(sK11_skl)|element(topstr_closure(sK11_skl,sK12_skl),powerset(the_carrier(sK11_skl)))),
% 71.61/9.59 inference(resolution,[status(thm)],[f122,f201])).
% 71.61/9.59 fof(f225,plain,(
% 71.61/9.59 element(topstr_closure(sK11_skl,sK12_skl),powerset(the_carrier(sK11_skl)))),
% 71.61/9.59 inference(forward_subsumption_resolution,[status(thm)],[f224,f200])).
% 71.61/9.59 fof(f226,plain,(
% 71.61/9.59 ![X0,X1,X2]: (~element(X0,powerset(the_carrier(sK11_skl)))|~in(X1,the_carrier(sK11_skl))|~in(X1,topstr_closure(sK11_skl,X0))|~element(X2,powerset(the_carrier(sK11_skl)))|~closed_subset(X2,sK11_skl)|~subset(X0,X2)|in(X1,X2))),
% 71.61/9.59 inference(resolution,[status(thm)],[f178,f200])).
% 71.61/9.59 fof(f227,plain,(
% 71.61/9.59 ![X0]: (~element(X0,powerset(the_carrier(sK11_skl)))|subset(X0,topstr_closure(sK11_skl,X0)))),
% 71.61/9.59 inference(resolution,[status(thm)],[f192,f200])).
% 71.61/9.59 fof(f228,plain,(
% 71.61/9.59 topstr_closure(sK11_skl,sK12_skl)=sK12_skl|closed_subset(sK12_skl,sK11_skl)),
% 71.61/9.59 inference(resolution,[status(thm)],[f203,f218])).
% 71.61/9.59 fof(f250,plain,(
% 71.61/9.59 subset(sK12_skl,topstr_closure(sK11_skl,sK12_skl))),
% 71.61/9.59 inference(resolution,[status(thm)],[f227,f201])).
% 71.61/9.59 fof(f252,plain,(
% 71.61/9.59 ![X0,X1]: (topstr_closure(sK11_skl,sK12_skl)=sK12_skl|~element(X0,powerset(the_carrier(sK11_skl)))|~in(X1,the_carrier(sK11_skl))|~in(X1,topstr_closure(sK11_skl,X0))|~element(sK12_skl,powerset(the_carrier(sK11_skl)))|~subset(X0,sK12_skl)|in(X1,sK12_skl))),
% 71.61/9.59 inference(resolution,[status(thm)],[f228,f226])).
% 71.61/9.59 fof(f254,plain,(
% 71.61/9.59 ![X0,X1]: (topstr_closure(sK11_skl,sK12_skl)=sK12_skl|~element(X0,powerset(the_carrier(sK11_skl)))|~in(X1,the_carrier(sK11_skl))|~in(X1,topstr_closure(sK11_skl,X0))|~subset(X0,sK12_skl)|in(X1,sK12_skl))),
% 71.61/9.59 inference(forward_subsumption_resolution,[status(thm)],[f252,f201])).
% 71.61/9.59 fof(f345,plain,(
% 71.61/9.59 ![X0]: (topstr_closure(sK11_skl,sK12_skl)=sK12_skl|~element(sK12_skl,powerset(the_carrier(sK11_skl)))|~in(X0,the_carrier(sK11_skl))|~in(X0,topstr_closure(sK11_skl,sK12_skl))|in(X0,sK12_skl))),
% 71.61/9.59 inference(resolution,[status(thm)],[f254,f221])).
% 71.61/9.59 fof(f347,plain,(
% 71.61/9.59 ![X0]: (topstr_closure(sK11_skl,sK12_skl)=sK12_skl|~in(X0,the_carrier(sK11_skl))|~in(X0,topstr_closure(sK11_skl,sK12_skl))|in(X0,sK12_skl))),
% 71.61/9.59 inference(forward_subsumption_resolution,[status(thm)],[f345,f201])).
% 71.61/9.59 fof(f366,plain,(
% 71.61/9.59 topstr_closure(sK11_skl,sK12_skl)=sK12_skl|~subset(topstr_closure(sK11_skl,sK12_skl),sK12_skl)),
% 71.61/9.59 inference(resolution,[status(thm)],[f113,f250])).
% 71.61/9.59 fof(f518,plain,(
% 71.61/9.59 subset(topstr_closure(sK11_skl,sK12_skl),the_carrier(sK11_skl))),
% 71.61/9.59 inference(resolution,[status(thm)],[f168,f225])).
% 71.61/9.59 fof(f537,plain,(
% 71.61/9.59 ![X0]: (~in(X0,topstr_closure(sK11_skl,sK12_skl))|in(X0,the_carrier(sK11_skl)))),
% 71.61/9.59 inference(resolution,[status(thm)],[f518,f118])).
% 71.61/9.59 fof(f617,plain,(
% 71.61/9.59 ~topological_space(sK11_skl)|~top_str(sK11_skl)|element(sK10_skl(sK12_skl,sK11_skl),powerset(powerset(the_carrier(sK11_skl))))),
% 71.61/9.59 inference(resolution,[status(thm)],[f186,f201])).
% 71.61/9.59 fof(f621,plain,(
% 71.61/9.59 ~topological_space(sK11_skl)|element(sK10_skl(sK12_skl,sK11_skl),powerset(powerset(the_carrier(sK11_skl))))),
% 71.61/9.59 inference(forward_subsumption_resolution,[status(thm)],[f617,f200])).
% 71.61/9.59 fof(f1883,plain,(
% 71.61/9.59 ![X0]: (topstr_closure(sK11_skl,sK12_skl)=sK12_skl|~in(sK0_skl(sK12_skl,X0),the_carrier(sK11_skl))|~in(sK0_skl(sK12_skl,X0),topstr_closure(sK11_skl,sK12_skl))|subset(X0,sK12_skl))),
% 71.61/9.59 inference(resolution,[status(thm)],[f347,f120])).
% 71.61/9.59 fof(f9059,plain,(
% 71.61/9.59 ![X0]: (topstr_closure(sK11_skl,sK12_skl)=sK12_skl|~in(sK0_skl(sK12_skl,X0),topstr_closure(sK11_skl,sK12_skl))|subset(X0,sK12_skl))),
% 71.61/9.59 inference(forward_subsumption_resolution,[status(thm)],[f1883,f537])).
% 71.61/9.59 fof(f9061,plain,(
% 71.61/9.59 topstr_closure(sK11_skl,sK12_skl)=sK12_skl|subset(topstr_closure(sK11_skl,sK12_skl),sK12_skl)|subset(topstr_closure(sK11_skl,sK12_skl),sK12_skl)),
% 71.61/9.61 inference(resolution,[status(thm)],[f9059,f119])).
% 71.61/9.61 fof(f9063,plain,(
% 71.61/9.61 topstr_closure(sK11_skl,sK12_skl)=sK12_skl|subset(topstr_closure(sK11_skl,sK12_skl),sK12_skl)),
% 71.61/9.61 inference(duplicate_literals_removal,[status(thm)],[f9061])).
% 71.61/9.61 fof(f9064,plain,(
% 71.61/9.61 topstr_closure(sK11_skl,sK12_skl)=sK12_skl),
% 71.61/9.61 inference(forward_subsumption_resolution,[status(thm)],[f9063,f366])).
% 71.61/9.61 fof(f9368,plain,(
% 71.61/9.61 ~sP0_prd(sK12_skl,sK11_skl)),
% 71.61/9.61 inference(resolution,[status(thm)],[f9064,f219])).
% 71.61/9.61 fof(f9590,plain,(
% 71.61/9.61 ~closed_subset(sK12_skl,sK11_skl)),
% 71.61/9.61 inference(backward_subsumption_resolution,[status(thm)],[f204,f9368])).
% 71.61/9.61 fof(f9591,plain,(
% 71.61/9.61 topological_space(sK11_skl)),
% 71.61/9.61 inference(backward_subsumption_resolution,[status(thm)],[f202,f9368])).
% 71.61/9.61 fof(f9595,plain,(
% 71.61/9.61 element(sK10_skl(sK12_skl,sK11_skl),powerset(powerset(the_carrier(sK11_skl))))),
% 71.61/9.61 inference(backward_subsumption_resolution,[status(thm)],[f621,f9591])).
% 71.61/9.61 fof(f9612,plain,(
% 71.61/9.61 ![X0]: (~top_str(sK11_skl)|~element(X0,powerset(the_carrier(sK11_skl)))|topstr_closure(sK11_skl,X0)=meet_of_subsets(the_carrier(sK11_skl),sK10_skl(X0,sK11_skl)))),
% 71.61/9.61 inference(resolution,[status(thm)],[f9591,f190])).
% 71.61/9.61 fof(f9615,plain,(
% 71.61/9.61 ![X0,X1]: (~top_str(sK11_skl)|~element(X0,powerset(the_carrier(sK11_skl)))|~element(X1,powerset(the_carrier(sK11_skl)))|~in(X1,sK10_skl(X0,sK11_skl))|closed_subset(X1,sK11_skl))),
% 71.61/9.61 inference(resolution,[status(thm)],[f9591,f187])).
% 71.61/9.61 fof(f9616,plain,(
% 71.61/9.61 ![X0]: (~top_str(sK11_skl)|~element(X0,powerset(powerset(the_carrier(sK11_skl))))|~closed_subset(sK8_skl(X0,sK11_skl),sK11_skl)|closed_subset(meet_of_subsets(the_carrier(sK11_skl),X0),sK11_skl))),
% 71.61/9.61 inference(resolution,[status(thm)],[f9591,f174])).
% 71.61/9.61 fof(f9617,plain,(
% 71.61/9.61 ![X0]: (~top_str(sK11_skl)|~element(X0,powerset(powerset(the_carrier(sK11_skl))))|in(sK8_skl(X0,sK11_skl),X0)|closed_subset(meet_of_subsets(the_carrier(sK11_skl),X0),sK11_skl))),
% 71.61/9.61 inference(resolution,[status(thm)],[f9591,f173])).
% 71.61/9.61 fof(f9636,plain,(
% 71.61/9.61 ![X0]: (~element(X0,powerset(the_carrier(sK11_skl)))|topstr_closure(sK11_skl,X0)=meet_of_subsets(the_carrier(sK11_skl),sK10_skl(X0,sK11_skl)))),
% 71.61/9.61 inference(forward_subsumption_resolution,[status(thm)],[f9612,f200])).
% 71.61/9.61 fof(f9639,plain,(
% 71.61/9.61 ![X0,X1]: (~element(X0,powerset(the_carrier(sK11_skl)))|~element(X1,powerset(the_carrier(sK11_skl)))|~in(X1,sK10_skl(X0,sK11_skl))|closed_subset(X1,sK11_skl))),
% 71.61/9.61 inference(forward_subsumption_resolution,[status(thm)],[f9615,f200])).
% 71.61/9.61 fof(f9640,plain,(
% 71.61/9.61 ![X0]: (~element(X0,powerset(powerset(the_carrier(sK11_skl))))|~closed_subset(sK8_skl(X0,sK11_skl),sK11_skl)|closed_subset(meet_of_subsets(the_carrier(sK11_skl),X0),sK11_skl))),
% 71.61/9.61 inference(forward_subsumption_resolution,[status(thm)],[f9616,f200])).
% 71.61/9.61 fof(f9641,plain,(
% 71.61/9.61 ![X0]: (~element(X0,powerset(powerset(the_carrier(sK11_skl))))|in(sK8_skl(X0,sK11_skl),X0)|closed_subset(meet_of_subsets(the_carrier(sK11_skl),X0),sK11_skl))),
% 71.61/9.61 inference(forward_subsumption_resolution,[status(thm)],[f9617,f200])).
% 71.61/9.61 fof(f9648,plain,(
% 71.61/9.61 ~topological_space(sK11_skl)|~top_str(sK11_skl)|element(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),powerset(the_carrier(sK11_skl)))|closed_subset(meet_of_subsets(the_carrier(sK11_skl),sK10_skl(sK12_skl,sK11_skl)),sK11_skl)),
% 71.61/9.61 inference(resolution,[status(thm)],[f9595,f172])).
% 71.61/9.61 fof(f9683,plain,(
% 71.61/9.61 ~top_str(sK11_skl)|element(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),powerset(the_carrier(sK11_skl)))|closed_subset(meet_of_subsets(the_carrier(sK11_skl),sK10_skl(sK12_skl,sK11_skl)),sK11_skl)),
% 71.61/9.61 inference(forward_subsumption_resolution,[status(thm)],[f9648,f9591])).
% 71.61/9.61 fof(f9716,plain,(
% 71.61/9.61 topstr_closure(sK11_skl,sK12_skl)=meet_of_subsets(the_carrier(sK11_skl),sK10_skl(sK12_skl,sK11_skl))),
% 71.61/9.61 inference(resolution,[status(thm)],[f9636,f201])).
% 71.61/9.61 fof(f9720,plain,(
% 71.61/9.61 sK12_skl=meet_of_subsets(the_carrier(sK11_skl),sK10_skl(sK12_skl,sK11_skl))),
% 71.61/9.61 inference(forward_demodulation,[status(thm)],[f9064,f9716])).
% 71.61/9.61 fof(f9944,plain,(
% 71.61/9.61 in(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK10_skl(sK12_skl,sK11_skl))|closed_subset(meet_of_subsets(the_carrier(sK11_skl),sK10_skl(sK12_skl,sK11_skl)),sK11_skl)),
% 60.06/9.68 inference(resolution,[status(thm)],[f9641,f9595])).
% 60.06/9.68 fof(f10296,plain,(
% 60.06/9.68 element(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),powerset(the_carrier(sK11_skl)))|closed_subset(meet_of_subsets(the_carrier(sK11_skl),sK10_skl(sK12_skl,sK11_skl)),sK11_skl)),
% 60.06/9.68 inference(forward_subsumption_resolution,[status(thm)],[f9683,f200])).
% 60.06/9.68 fof(f10297,plain,(
% 60.06/9.68 ![X0]: (closed_subset(meet_of_subsets(the_carrier(sK11_skl),sK10_skl(sK12_skl,sK11_skl)),sK11_skl)|~element(X0,powerset(the_carrier(sK11_skl)))|~in(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK10_skl(X0,sK11_skl))|closed_subset(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK11_skl))),
% 60.06/9.68 inference(resolution,[status(thm)],[f10296,f9639])).
% 60.06/9.68 fof(f11300,plain,(
% 60.06/9.68 in(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK10_skl(sK12_skl,sK11_skl))|closed_subset(sK12_skl,sK11_skl)),
% 60.06/9.68 inference(forward_demodulation,[status(thm)],[f9720,f9944])).
% 60.06/9.68 fof(f11301,plain,(
% 60.06/9.68 in(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK10_skl(sK12_skl,sK11_skl))),
% 60.06/9.68 inference(forward_subsumption_resolution,[status(thm)],[f11300,f9590])).
% 60.06/9.68 fof(f21852,plain,(
% 60.06/9.68 ![X0]: (closed_subset(sK12_skl,sK11_skl)|~element(X0,powerset(the_carrier(sK11_skl)))|~in(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK10_skl(X0,sK11_skl))|closed_subset(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK11_skl))),
% 60.06/9.68 inference(forward_demodulation,[status(thm)],[f9720,f10297])).
% 60.06/9.68 fof(f21853,plain,(
% 60.06/9.68 ![X0]: (~element(X0,powerset(the_carrier(sK11_skl)))|~in(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK10_skl(X0,sK11_skl))|closed_subset(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK11_skl))),
% 60.06/9.68 inference(forward_subsumption_resolution,[status(thm)],[f21852,f9590])).
% 60.06/9.68 fof(f21854,plain,(
% 60.06/9.68 ~element(sK12_skl,powerset(the_carrier(sK11_skl)))|closed_subset(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK11_skl)),
% 60.06/9.68 inference(resolution,[status(thm)],[f21853,f11301])).
% 60.06/9.68 fof(f21855,plain,(
% 60.06/9.68 closed_subset(sK8_skl(sK10_skl(sK12_skl,sK11_skl),sK11_skl),sK11_skl)),
% 60.06/9.68 inference(forward_subsumption_resolution,[status(thm)],[f21854,f201])).
% 60.06/9.68 fof(f22208,plain,(
% 60.06/9.68 ~element(sK10_skl(sK12_skl,sK11_skl),powerset(powerset(the_carrier(sK11_skl))))|closed_subset(meet_of_subsets(the_carrier(sK11_skl),sK10_skl(sK12_skl,sK11_skl)),sK11_skl)),
% 60.06/9.68 inference(resolution,[status(thm)],[f21855,f9640])).
% 60.06/9.68 fof(f22212,plain,(
% 60.06/9.68 ~element(sK10_skl(sK12_skl,sK11_skl),powerset(powerset(the_carrier(sK11_skl))))|closed_subset(sK12_skl,sK11_skl)),
% 60.06/9.68 inference(forward_demodulation,[status(thm)],[f9720,f22208])).
% 60.06/9.68 fof(f22213,plain,(
% 60.06/9.68 closed_subset(sK12_skl,sK11_skl)),
% 60.06/9.68 inference(forward_subsumption_resolution,[status(thm)],[f22212,f9595])).
% 60.06/9.68 fof(f22223,plain,(
% 60.06/9.68 $false),
% 60.06/9.68 inference(forward_subsumption_resolution,[status(thm)],[f22213,f9590])).
% 60.06/9.68 % SZS output end CNFRefutation for theBenchmark.p
% 12.83/9.76 % Elapsed time: 9.294562 seconds
% 12.83/9.76 % CPU time: 72.793237 seconds
% 12.83/9.76 % Total memory used: 476.797 MB
% 12.83/9.76 % Net memory used: 451.272 MB
%------------------------------------------------------------------------------