%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU381+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 : n026.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:28 PM UTC 2026
% Result : Theorem 121.73s 16.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU381+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n026.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:20:21 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 121.73/16.01 % Refutation found
% 121.73/16.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 121.73/16.01 % SZS output start CNFRefutation for theBenchmark
% 121.73/16.01 fof(f36,axiom,(
% 121.73/16.01 (! [A] :( rel_str(A)=> (! [B] :( element(B,powerset(the_carrier(A)))=> ( upper_relstr_subset(B,A)<=> (! [C] :( element(C,the_carrier(A))=> (! [D] :( element(D,the_carrier(A))=> ( ( in(C,B)& related(A,C,D) )=> in(D,B) ) ) )) )) ) )) )),
% 121.73/16.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 121.73/16.01 fof(f41,axiom,(
% 121.73/16.01 (! [A] :( strict_rel_str(boole_POSet(A))& rel_str(boole_POSet(A)) ) )),
% 121.73/16.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 121.73/16.01 fof(f58,axiom,(
% 121.73/16.01 (! [A] :( ~ empty_carrier(boole_POSet(A))& strict_rel_str(boole_POSet(A))& reflexive_relstr(boole_POSet(A))& transitive_relstr(boole_POSet(A))& antisymmetric_relstr(boole_POSet(A))& with_suprema_relstr(boole_POSet(A))& with_infima_relstr(boole_POSet(A))& complete_relstr(boole_POSet(A))& lower_bounded_relstr(boole_POSet(A))& upper_bounded_relstr(boole_POSet(A))& bounded_relstr(boole_POSet(A))& up_complete_relstr(boole_POSet(A))& join_complete_relstr(boole_POSet(A))& distributive_relstr(boole_POSet(A)) ) )),
% 121.73/16.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 121.73/16.01 fof(f95,axiom,(
% 121.73/16.01 (! [A,B,C] :( ( ~ empty_carrier(A)& reflexive_relstr(A)& rel_str(A)& element(B,the_carrier(A))& element(C,the_carrier(A)) )=> ( related_reflexive(A,B,C)<=> related(A,B,C) ) ) )),
% 121.73/16.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 121.73/16.01 fof(f98,conjecture,(
% 121.73/16.01 (! [A,B] :( element(B,powerset(the_carrier(boole_POSet(A))))=> ( upper_relstr_subset(B,boole_POSet(A))<=> (! [C,D] :( ( subset(C,D)& subset(D,A)& in(C,B) )=> in(D,B) ) )) ) )),
% 121.73/16.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 121.73/16.01 fof(f99,negated_conjecture,(
% 121.73/16.01 ~((! [A,B] :( element(B,powerset(the_carrier(boole_POSet(A))))=> ( upper_relstr_subset(B,boole_POSet(A))<=> (! [C,D] :( ( subset(C,D)& subset(D,A)& in(C,B) )=> in(D,B) ) )) ) ))),
% 121.73/16.01 inference(negated_conjecture,[status(cth)],[f98])).
% 121.73/16.01 fof(f102,axiom,(
% 121.73/16.01 (! [A,B] :( element(B,the_carrier(boole_POSet(A)))=> (! [C] :( element(C,the_carrier(boole_POSet(A)))=> ( related_reflexive(boole_POSet(A),B,C)<=> subset(B,C) ) ) )) )),
% 121.73/16.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 121.73/16.01 fof(f103,axiom,(
% 121.73/16.01 (! [A,B] :( element(A,powerset(B))<=> subset(A,B) ) )),
% 121.73/16.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 121.73/16.01 fof(f104,axiom,(
% 121.73/16.01 (! [A,B,C] :( ( in(A,B)& element(B,powerset(C)) )=> element(A,C) ) )),
% 121.73/16.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 121.73/16.01 fof(f105,axiom,(
% 121.73/16.01 (! [A] : the_carrier(boole_POSet(A)) = powerset(A) )),
% 121.73/16.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 121.73/16.01 fof(f305,plain,(
% 121.73/16.01 ![A]: (~rel_str(A)|(![B]: (~element(B,powerset(the_carrier(A)))|(upper_relstr_subset(B,A)<=>(![C]: (~element(C,the_carrier(A))|(![D]: (~element(D,the_carrier(A))|((~in(C,B)|~related(A,C,D))|in(D,B))))))))))),
% 121.73/16.01 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 121.73/16.01 fof(f306,plain,(
% 121.73/16.01 ![A]: (~rel_str(A)|(![B]: (~element(B,powerset(the_carrier(A)))|((~upper_relstr_subset(B,A)|(![C]: (~element(C,the_carrier(A))|(![D]: (~element(D,the_carrier(A))|((~in(C,B)|~related(A,C,D))|in(D,B)))))))&(upper_relstr_subset(B,A)|(?[C]: (element(C,the_carrier(A))&(?[D]: (element(D,the_carrier(A))&((in(C,B)&related(A,C,D))&~in(D,B)))))))))))),
% 121.73/16.01 inference(NNF_transformation,[status(thm)],[f305])).
% 121.73/16.01 fof(f307,plain,(
% 121.73/16.01 ![A]: (~rel_str(A)|(![B]: (~element(B,powerset(the_carrier(A)))|((~upper_relstr_subset(B,A)|(![C]: (~element(C,the_carrier(A))|(![D]: (~element(D,the_carrier(A))|((~in(C,B)|~related(A,C,D))|in(D,B)))))))&(upper_relstr_subset(B,A)|(element(sK0_skl(B,A),the_carrier(A))&(element(sK1_skl(B,A),the_carrier(A))&((in(sK0_skl(B,A),B)&related(A,sK0_skl(B,A),sK1_skl(B,A)))&~in(sK1_skl(B,A),B)))))))))),
% 121.73/16.01 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(B,A)),skolemize(D,sK1_skl(B,A))],[f306])).
% 121.73/16.01 fof(f308,plain,(
% 121.73/16.01 ![X0,X1,X2,X3]: (~rel_str(X0)|~element(X1,powerset(the_carrier(X0)))|~upper_relstr_subset(X1,X0)|~element(X2,the_carrier(X0))|~element(X3,the_carrier(X0))|~in(X2,X1)|~related(X0,X2,X3)|in(X3,X1))),
% 121.73/16.01 inference(cnf_transformation,[status(thm)],[f307])).
% 121.73/16.01 fof(f309,plain,(
% 121.73/16.01 ![X0,X1]: (~rel_str(X0)|~element(X1,powerset(the_carrier(X0)))|upper_relstr_subset(X1,X0)|element(sK0_skl(X1,X0),the_carrier(X0)))),
% 121.73/16.01 inference(cnf_transformation,[status(thm)],[f307])).
% 121.73/16.01 fof(f310,plain,(
% 121.73/16.01 ![X0,X1]: (~rel_str(X0)|~element(X1,powerset(the_carrier(X0)))|upper_relstr_subset(X1,X0)|element(sK1_skl(X1,X0),the_carrier(X0)))),
% 121.73/16.01 inference(cnf_transformation,[status(thm)],[f307])).
% 121.73/16.01 fof(f311,plain,(
% 121.73/16.01 ![X0,X1]: (~rel_str(X0)|~element(X1,powerset(the_carrier(X0)))|upper_relstr_subset(X1,X0)|in(sK0_skl(X1,X0),X1))),
% 121.73/16.01 inference(cnf_transformation,[status(thm)],[f307])).
% 121.73/16.01 fof(f312,plain,(
% 121.73/16.01 ![X0,X1]: (~rel_str(X0)|~element(X1,powerset(the_carrier(X0)))|upper_relstr_subset(X1,X0)|related(X0,sK0_skl(X1,X0),sK1_skl(X1,X0)))),
% 121.73/16.01 inference(cnf_transformation,[status(thm)],[f307])).
% 121.73/16.01 fof(f313,plain,(
% 121.73/16.01 ![X0,X1]: (~rel_str(X0)|~element(X1,powerset(the_carrier(X0)))|upper_relstr_subset(X1,X0)|~in(sK1_skl(X1,X0),X1))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f307])).
% 122.68/16.01 fof(f317,plain,(
% 122.68/16.01 (![A]: strict_rel_str(boole_POSet(A)))&(![A]: rel_str(boole_POSet(A)))),
% 122.68/16.01 inference(miniscoping,[status(thm)],[f41])).
% 122.68/16.01 fof(f319,plain,(
% 122.68/16.01 ![X0]: (rel_str(boole_POSet(X0)))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f317])).
% 122.68/16.01 fof(f344,plain,(
% 122.68/16.01 (((((((((((((![A]: ~empty_carrier(boole_POSet(A)))&(![A]: strict_rel_str(boole_POSet(A))))&(![A]: reflexive_relstr(boole_POSet(A))))&(![A]: transitive_relstr(boole_POSet(A))))&(![A]: antisymmetric_relstr(boole_POSet(A))))&(![A]: with_suprema_relstr(boole_POSet(A))))&(![A]: with_infima_relstr(boole_POSet(A))))&(![A]: complete_relstr(boole_POSet(A))))&(![A]: lower_bounded_relstr(boole_POSet(A))))&(![A]: upper_bounded_relstr(boole_POSet(A))))&(![A]: bounded_relstr(boole_POSet(A))))&(![A]: up_complete_relstr(boole_POSet(A))))&(![A]: join_complete_relstr(boole_POSet(A))))&(![A]: distributive_relstr(boole_POSet(A)))),
% 122.68/16.01 inference(miniscoping,[status(thm)],[f58])).
% 122.68/16.01 fof(f345,plain,(
% 122.68/16.01 ![X0]: (~empty_carrier(boole_POSet(X0)))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f344])).
% 122.68/16.01 fof(f347,plain,(
% 122.68/16.01 ![X0]: (reflexive_relstr(boole_POSet(X0)))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f344])).
% 122.68/16.01 fof(f667,plain,(
% 122.68/16.01 ![A,B,C]: (((((empty_carrier(A)|~reflexive_relstr(A))|~rel_str(A))|~element(B,the_carrier(A)))|~element(C,the_carrier(A)))|(related_reflexive(A,B,C)<=>related(A,B,C)))),
% 122.68/16.01 inference(pre_NNF_transformation,[status(thm)],[f95])).
% 122.68/16.01 fof(f668,plain,(
% 122.68/16.01 ![A,B,C]: (((((empty_carrier(A)|~reflexive_relstr(A))|~rel_str(A))|~element(B,the_carrier(A)))|~element(C,the_carrier(A)))|((~related_reflexive(A,B,C)|related(A,B,C))&(related_reflexive(A,B,C)|~related(A,B,C))))),
% 122.68/16.01 inference(NNF_transformation,[status(thm)],[f667])).
% 122.68/16.01 fof(f669,plain,(
% 122.68/16.01 ![X0,X1,X2]: (empty_carrier(X0)|~reflexive_relstr(X0)|~rel_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|~related_reflexive(X0,X1,X2)|related(X0,X1,X2))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f668])).
% 122.68/16.01 fof(f670,plain,(
% 122.68/16.01 ![X0,X1,X2]: (empty_carrier(X0)|~reflexive_relstr(X0)|~rel_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|related_reflexive(X0,X1,X2)|~related(X0,X1,X2))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f668])).
% 122.68/16.01 fof(f676,plain,(
% 122.68/16.01 (?[A,B]: (element(B,powerset(the_carrier(boole_POSet(A))))&(upper_relstr_subset(B,boole_POSet(A))<~>(![C,D]: (((~subset(C,D)|~subset(D,A))|~in(C,B))|in(D,B))))))),
% 122.68/16.01 inference(pre_NNF_transformation,[status(thm)],[f99])).
% 122.68/16.01 fof(f677,plain,(
% 122.68/16.01 ?[A,B]: (element(B,powerset(the_carrier(boole_POSet(A))))&((upper_relstr_subset(B,boole_POSet(A))|(![C,D]: (((~subset(C,D)|~subset(D,A))|~in(C,B))|in(D,B))))&(~upper_relstr_subset(B,boole_POSet(A))|(?[C,D]: (((subset(C,D)&subset(D,A))&in(C,B))&~in(D,B))))))),
% 122.68/16.01 inference(NNF_transformation,[status(thm)],[f676])).
% 122.68/16.01 fof(f678,plain,(
% 122.68/16.01 ?[A,B]: (element(B,powerset(the_carrier(boole_POSet(A))))&((upper_relstr_subset(B,boole_POSet(A))|(![D]: ((![C]: ((~subset(C,D)|~subset(D,A))|~in(C,B)))|in(D,B))))&(~upper_relstr_subset(B,boole_POSet(A))|(?[D]: ((?[C]: ((subset(C,D)&subset(D,A))&in(C,B)))&~in(D,B))))))),
% 122.68/16.01 inference(miniscoping,[status(thm)],[f677])).
% 122.68/16.01 fof(f679,plain,(
% 122.68/16.01 (element(sK35_skl,powerset(the_carrier(boole_POSet(sK34_skl))))&((upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|(![D]: ((![C]: ((~subset(C,D)|~subset(D,sK34_skl))|~in(C,sK35_skl)))|in(D,sK35_skl))))&(~upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|(((subset(sK37_skl,sK36_skl)&subset(sK36_skl,sK34_skl))&in(sK37_skl,sK35_skl))&~in(sK36_skl,sK35_skl)))))),
% 122.68/16.01 inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl,sK35_skl,sK36_skl,sK37_skl]),skolemize(A,sK34_skl),skolemize(B,sK35_skl),skolemize(D,sK36_skl),skolemize(C,sK37_skl)],[f678])).
% 122.68/16.01 fof(f680,plain,(
% 122.68/16.01 element(sK35_skl,powerset(the_carrier(boole_POSet(sK34_skl))))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f679])).
% 122.68/16.01 fof(f681,plain,(
% 122.68/16.01 ![X0,X1]: (upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~subset(X0,X1)|~subset(X1,sK34_skl)|~in(X0,sK35_skl)|in(X1,sK35_skl))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f679])).
% 122.68/16.01 fof(f682,plain,(
% 122.68/16.01 ~upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|subset(sK37_skl,sK36_skl)),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f679])).
% 122.68/16.01 fof(f683,plain,(
% 122.68/16.01 ~upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|subset(sK36_skl,sK34_skl)),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f679])).
% 122.68/16.01 fof(f684,plain,(
% 122.68/16.01 ~upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|in(sK37_skl,sK35_skl)),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f679])).
% 122.68/16.01 fof(f685,plain,(
% 122.68/16.01 ~upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~in(sK36_skl,sK35_skl)),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f679])).
% 122.68/16.01 fof(f690,plain,(
% 122.68/16.01 ![A,B]: (~element(B,the_carrier(boole_POSet(A)))|(![C]: (~element(C,the_carrier(boole_POSet(A)))|(related_reflexive(boole_POSet(A),B,C)<=>subset(B,C)))))),
% 122.68/16.01 inference(pre_NNF_transformation,[status(thm)],[f102])).
% 122.68/16.01 fof(f691,plain,(
% 122.68/16.01 ![A,B]: (~element(B,the_carrier(boole_POSet(A)))|(![C]: (~element(C,the_carrier(boole_POSet(A)))|((~related_reflexive(boole_POSet(A),B,C)|subset(B,C))&(related_reflexive(boole_POSet(A),B,C)|~subset(B,C))))))),
% 122.68/16.01 inference(NNF_transformation,[status(thm)],[f690])).
% 122.68/16.01 fof(f692,plain,(
% 122.68/16.01 ![X0,X1,X2]: (~element(X0,the_carrier(boole_POSet(X1)))|~element(X2,the_carrier(boole_POSet(X1)))|~related_reflexive(boole_POSet(X1),X0,X2)|subset(X0,X2))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f691])).
% 122.68/16.01 fof(f693,plain,(
% 122.68/16.01 ![X0,X1,X2]: (~element(X0,the_carrier(boole_POSet(X1)))|~element(X2,the_carrier(boole_POSet(X1)))|related_reflexive(boole_POSet(X1),X0,X2)|~subset(X0,X2))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f691])).
% 122.68/16.01 fof(f694,plain,(
% 122.68/16.01 ![A,B]: ((~element(A,powerset(B))|subset(A,B))&(element(A,powerset(B))|~subset(A,B)))),
% 122.68/16.01 inference(NNF_transformation,[status(thm)],[f103])).
% 122.68/16.01 fof(f695,plain,(
% 122.68/16.01 (![A,B]: (~element(A,powerset(B))|subset(A,B)))&(![A,B]: (element(A,powerset(B))|~subset(A,B)))),
% 122.68/16.01 inference(miniscoping,[status(thm)],[f694])).
% 122.68/16.01 fof(f696,plain,(
% 122.68/16.01 ![X0,X1]: (~element(X0,powerset(X1))|subset(X0,X1))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f695])).
% 122.68/16.01 fof(f697,plain,(
% 122.68/16.01 ![X0,X1]: (element(X0,powerset(X1))|~subset(X0,X1))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f695])).
% 122.68/16.01 fof(f698,plain,(
% 122.68/16.01 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|element(A,C))),
% 122.68/16.01 inference(pre_NNF_transformation,[status(thm)],[f104])).
% 122.68/16.01 fof(f699,plain,(
% 122.68/16.01 ![A,C]: ((![B]: (~in(A,B)|~element(B,powerset(C))))|element(A,C))),
% 122.68/16.01 inference(miniscoping,[status(thm)],[f698])).
% 122.68/16.01 fof(f700,plain,(
% 122.68/16.01 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|element(X0,X2))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f699])).
% 122.68/16.01 fof(f701,plain,(
% 122.68/16.01 ![X0]: (the_carrier(boole_POSet(X0))=powerset(X0))),
% 122.68/16.01 inference(cnf_transformation,[status(thm)],[f105])).
% 122.68/16.01 fof(f715,plain,(
% 122.68/16.01 ![X0,X1]: (in(sK37_skl,sK35_skl)|~subset(X0,X1)|~subset(X1,sK34_skl)|~in(X0,sK35_skl)|in(X1,sK35_skl))),
% 122.68/16.01 inference(resolution,[status(thm)],[f684,f681])).
% 122.68/16.01 fof(f748,plain,(
% 122.68/16.01 element(sK35_skl,powerset(powerset(sK34_skl)))),
% 122.68/16.01 inference(backward_demodulation,[status(thm)],[f701,f680])).
% 122.68/16.01 fof(f842,plain,(
% 122.68/16.01 ![X0,X1,X2,X3]: (~rel_str(X0)|~element(X1,powerset(the_carrier(X0)))|~upper_relstr_subset(X1,X0)|~element(X2,the_carrier(X0))|~in(X3,X1)|~related(X0,X3,X2)|in(X2,X1))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f308,f700])).
% 122.68/16.02 fof(f844,plain,(
% 122.68/16.02 ![X0,X1]: (~rel_str(boole_POSet(X0))|~element(X1,powerset(the_carrier(boole_POSet(X0))))|upper_relstr_subset(X1,boole_POSet(X0))|element(sK0_skl(X1,boole_POSet(X0)),powerset(X0)))),
% 122.68/16.02 inference(paramodulation,[status(thm)],[f701,f309])).
% 122.68/16.02 fof(f845,plain,(
% 122.68/16.02 ![X0,X1]: (~rel_str(boole_POSet(X0))|~element(X1,powerset(powerset(X0)))|upper_relstr_subset(X1,boole_POSet(X0))|element(sK0_skl(X1,boole_POSet(X0)),powerset(X0)))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f844])).
% 122.68/16.02 fof(f846,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|upper_relstr_subset(X0,boole_POSet(X1))|element(sK0_skl(X0,boole_POSet(X1)),powerset(X1)))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f845,f319])).
% 122.68/16.02 fof(f877,plain,(
% 122.68/16.02 ![X0,X1]: (~rel_str(boole_POSet(X0))|~element(X1,powerset(the_carrier(boole_POSet(X0))))|upper_relstr_subset(X1,boole_POSet(X0))|element(sK1_skl(X1,boole_POSet(X0)),powerset(X0)))),
% 122.68/16.02 inference(paramodulation,[status(thm)],[f701,f310])).
% 122.68/16.02 fof(f878,plain,(
% 122.68/16.02 ![X0,X1]: (~rel_str(boole_POSet(X0))|~element(X1,powerset(powerset(X0)))|upper_relstr_subset(X1,boole_POSet(X0))|element(sK1_skl(X1,boole_POSet(X0)),powerset(X0)))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f877])).
% 122.68/16.02 fof(f879,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|upper_relstr_subset(X0,boole_POSet(X1))|element(sK1_skl(X0,boole_POSet(X1)),powerset(X1)))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f878,f319])).
% 122.68/16.02 fof(f884,plain,(
% 122.68/16.02 ![X0,X1]: (~rel_str(boole_POSet(X0))|~element(X1,powerset(powerset(X0)))|upper_relstr_subset(X1,boole_POSet(X0))|in(sK0_skl(X1,boole_POSet(X0)),X1))),
% 122.68/16.02 inference(paramodulation,[status(thm)],[f701,f311])).
% 122.68/16.02 fof(f885,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|upper_relstr_subset(X0,boole_POSet(X1))|in(sK0_skl(X0,boole_POSet(X1)),X0))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f884,f319])).
% 122.68/16.02 fof(f904,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|upper_relstr_subset(X0,boole_POSet(X1))|subset(sK1_skl(X0,boole_POSet(X1)),X1))),
% 122.68/16.02 inference(resolution,[status(thm)],[f879,f696])).
% 122.68/16.02 fof(f926,plain,(
% 122.68/16.02 upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|in(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)),
% 122.68/16.02 inference(resolution,[status(thm)],[f885,f748])).
% 122.68/16.02 fof(f954,plain,(
% 122.68/16.02 ![X0]: (upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|in(sK37_skl,sK35_skl)|~subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),X0)|~subset(X0,sK34_skl)|in(X0,sK35_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f926,f715])).
% 122.68/16.02 fof(f958,plain,(
% 122.68/16.02 ![X0]: (in(sK37_skl,sK35_skl)|~subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),X0)|~subset(X0,sK34_skl)|in(X0,sK35_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f954,f684])).
% 122.68/16.02 fof(f1840,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,the_carrier(boole_POSet(X1)))|~related_reflexive(boole_POSet(X1),X0,X2)|subset(X0,X2))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f692])).
% 122.68/16.02 fof(f1841,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~related_reflexive(boole_POSet(X1),X0,X2)|subset(X0,X2))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f1840])).
% 122.68/16.02 fof(f1843,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|subset(X0,X2)|empty_carrier(boole_POSet(X1))|~reflexive_relstr(boole_POSet(X1))|~rel_str(boole_POSet(X1))|~element(X0,the_carrier(boole_POSet(X1)))|~element(X2,the_carrier(boole_POSet(X1)))|~related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(resolution,[status(thm)],[f1841,f670])).
% 122.68/16.02 fof(f1847,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|subset(X0,X2)|empty_carrier(boole_POSet(X1))|~reflexive_relstr(boole_POSet(X1))|~rel_str(boole_POSet(X1))|~element(X0,powerset(X1))|~element(X2,the_carrier(boole_POSet(X1)))|~related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f1843])).
% 122.68/16.02 fof(f1848,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|subset(X0,X2)|empty_carrier(boole_POSet(X1))|~reflexive_relstr(boole_POSet(X1))|~rel_str(boole_POSet(X1))|~element(X0,powerset(X1))|~element(X2,powerset(X1))|~related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f1847])).
% 122.68/16.02 fof(f1849,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|subset(X0,X2)|empty_carrier(boole_POSet(X1))|~reflexive_relstr(boole_POSet(X1))|~rel_str(boole_POSet(X1))|~related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(duplicate_literals_removal,[status(thm)],[f1848])).
% 122.68/16.02 fof(f1850,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|subset(X0,X2)|~reflexive_relstr(boole_POSet(X1))|~rel_str(boole_POSet(X1))|~related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f1849,f345])).
% 122.68/16.02 fof(f1851,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,the_carrier(boole_POSet(X1)))|related_reflexive(boole_POSet(X1),X0,X2)|~subset(X0,X2))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f693])).
% 122.68/16.02 fof(f1852,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|related_reflexive(boole_POSet(X1),X0,X2)|~subset(X0,X2))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f1851])).
% 122.68/16.02 fof(f1854,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|empty_carrier(boole_POSet(X1))|~reflexive_relstr(boole_POSet(X1))|~rel_str(boole_POSet(X1))|~element(X0,the_carrier(boole_POSet(X1)))|~element(X2,the_carrier(boole_POSet(X1)))|related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(resolution,[status(thm)],[f1852,f669])).
% 122.68/16.02 fof(f1855,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|empty_carrier(boole_POSet(X1))|~reflexive_relstr(boole_POSet(X1))|~rel_str(boole_POSet(X1))|~element(X0,powerset(X1))|~element(X2,the_carrier(boole_POSet(X1)))|related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f1854])).
% 122.68/16.02 fof(f1856,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|empty_carrier(boole_POSet(X1))|~reflexive_relstr(boole_POSet(X1))|~rel_str(boole_POSet(X1))|~element(X0,powerset(X1))|~element(X2,powerset(X1))|related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f1855])).
% 122.68/16.02 fof(f1857,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|empty_carrier(boole_POSet(X1))|~reflexive_relstr(boole_POSet(X1))|~rel_str(boole_POSet(X1))|related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(duplicate_literals_removal,[status(thm)],[f1856])).
% 122.68/16.02 fof(f1858,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|~reflexive_relstr(boole_POSet(X1))|~rel_str(boole_POSet(X1))|related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f1857,f345])).
% 122.68/16.02 fof(f1881,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|subset(X0,X2)|~rel_str(boole_POSet(X1))|~related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f1850,f347])).
% 122.68/16.02 fof(f1882,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|subset(X0,X2)|~related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(resolution,[status(thm)],[f1881,f319])).
% 122.68/16.02 fof(f1883,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|~rel_str(boole_POSet(X1))|related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f1858,f347])).
% 122.68/16.02 fof(f1884,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|related(boole_POSet(X1),X0,X2))),
% 122.68/16.02 inference(resolution,[status(thm)],[f1883,f319])).
% 122.68/16.02 fof(f2102,plain,(
% 122.68/16.02 ![X0,X1]: (~element(sK0_skl(X0,boole_POSet(X1)),powerset(X1))|~element(sK1_skl(X0,boole_POSet(X1)),powerset(X1))|subset(sK0_skl(X0,boole_POSet(X1)),sK1_skl(X0,boole_POSet(X1)))|~rel_str(boole_POSet(X1))|~element(X0,powerset(the_carrier(boole_POSet(X1))))|upper_relstr_subset(X0,boole_POSet(X1)))),
% 122.68/16.02 inference(resolution,[status(thm)],[f1882,f312])).
% 122.68/16.02 fof(f2103,plain,(
% 122.68/16.02 ![X0,X1]: (~element(sK0_skl(X0,boole_POSet(X1)),powerset(X1))|~element(sK1_skl(X0,boole_POSet(X1)),powerset(X1))|subset(sK0_skl(X0,boole_POSet(X1)),sK1_skl(X0,boole_POSet(X1)))|~rel_str(boole_POSet(X1))|~element(X0,powerset(powerset(X1)))|upper_relstr_subset(X0,boole_POSet(X1)))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f2102])).
% 122.68/16.02 fof(f2104,plain,(
% 122.68/16.02 ![X0,X1]: (~element(sK1_skl(X0,boole_POSet(X1)),powerset(X1))|subset(sK0_skl(X0,boole_POSet(X1)),sK1_skl(X0,boole_POSet(X1)))|~rel_str(boole_POSet(X1))|~element(X0,powerset(powerset(X1)))|upper_relstr_subset(X0,boole_POSet(X1)))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f2103,f846])).
% 122.68/16.02 fof(f2106,plain,(
% 122.68/16.02 ![X0,X1,X2,X3]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|~rel_str(boole_POSet(X1))|~element(X3,powerset(the_carrier(boole_POSet(X1))))|~upper_relstr_subset(X3,boole_POSet(X1))|~element(X2,the_carrier(boole_POSet(X1)))|~in(X0,X3)|in(X2,X3))),
% 122.68/16.02 inference(resolution,[status(thm)],[f1884,f842])).
% 122.68/16.02 fof(f2107,plain,(
% 122.68/16.02 ![X0,X1,X2,X3]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|~rel_str(boole_POSet(X1))|~element(X3,powerset(powerset(X1)))|~upper_relstr_subset(X3,boole_POSet(X1))|~element(X2,the_carrier(boole_POSet(X1)))|~in(X0,X3)|in(X2,X3))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f2106])).
% 122.68/16.02 fof(f2108,plain,(
% 122.68/16.02 ![X0,X1,X2,X3]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|~rel_str(boole_POSet(X1))|~element(X3,powerset(powerset(X1)))|~upper_relstr_subset(X3,boole_POSet(X1))|~element(X2,powerset(X1))|~in(X0,X3)|in(X2,X3))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f2107])).
% 122.68/16.02 fof(f2109,plain,(
% 122.68/16.02 ![X0,X1,X2,X3]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|~subset(X0,X2)|~rel_str(boole_POSet(X1))|~element(X3,powerset(powerset(X1)))|~upper_relstr_subset(X3,boole_POSet(X1))|~in(X0,X3)|in(X2,X3))),
% 122.68/16.02 inference(duplicate_literals_removal,[status(thm)],[f2108])).
% 122.68/16.02 fof(f2110,plain,(
% 122.68/16.02 ![X0,X1,X2,X3]: (~element(X0,powerset(X1))|~subset(X2,X0)|~rel_str(boole_POSet(X1))|~element(X3,powerset(powerset(X1)))|~upper_relstr_subset(X3,boole_POSet(X1))|~in(X2,X3)|in(X0,X3))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f2109,f700])).
% 122.68/16.02 fof(f3945,plain,(
% 122.68/16.02 ![X0,X1]: (subset(sK0_skl(X0,boole_POSet(X1)),sK1_skl(X0,boole_POSet(X1)))|~rel_str(boole_POSet(X1))|~element(X0,powerset(powerset(X1)))|upper_relstr_subset(X0,boole_POSet(X1)))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f2104,f879])).
% 122.68/16.02 fof(f3946,plain,(
% 122.68/16.02 ![X0,X1]: (subset(sK0_skl(X0,boole_POSet(X1)),sK1_skl(X0,boole_POSet(X1)))|~element(X0,powerset(powerset(X1)))|upper_relstr_subset(X0,boole_POSet(X1)))),
% 122.68/16.02 inference(resolution,[status(thm)],[f3945,f319])).
% 122.68/16.02 fof(f3947,plain,(
% 122.68/16.02 ![X0,X1,X2,X3]: (~element(X0,powerset(X1))|~subset(X2,X0)|~element(X3,powerset(powerset(X1)))|~upper_relstr_subset(X3,boole_POSet(X1))|~in(X2,X3)|in(X0,X3))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f2110,f319])).
% 122.68/16.02 fof(f3963,plain,(
% 122.68/16.02 ![X0,X1,X2,X3]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~element(sK35_skl,powerset(powerset(sK34_skl)))|~in(X1,sK35_skl)|in(X0,sK35_skl)|~subset(X2,X3)|~subset(X3,sK34_skl)|~in(X2,sK35_skl)|in(X3,sK35_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f3947,f681])).
% 122.68/16.02 fof(f3975,plain,(
% 122.68/16.02 ![X0,X1,X2,X3]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|~subset(X2,X3)|~subset(X3,sK34_skl)|~in(X2,sK35_skl)|in(X3,sK35_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f3963,f748])).
% 122.68/16.02 fof(f3983,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|~subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),X2)|~subset(X2,sK34_skl)|in(X2,sK35_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)))),
% 122.68/16.02 inference(resolution,[status(thm)],[f3975,f926])).
% 122.68/16.02 fof(f8958,plain,(
% 122.68/16.02 ![X0,X1]: (~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|~subset(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK34_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)))),
% 122.68/16.02 inference(resolution,[status(thm)],[f3946,f3983])).
% 122.68/16.02 fof(f8959,plain,(
% 122.68/16.02 ~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|in(sK37_skl,sK35_skl)|~subset(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK34_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)),
% 122.68/16.02 inference(resolution,[status(thm)],[f3946,f958])).
% 122.68/16.02 fof(f8963,plain,(
% 122.68/16.02 ![X0,X1]: (~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|~subset(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK34_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl))),
% 122.68/16.02 inference(duplicate_literals_removal,[status(thm)],[f8958])).
% 122.68/16.02 fof(f8964,plain,(
% 122.68/16.02 ![X0,X1]: (upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|~subset(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK34_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f8963,f748])).
% 122.68/16.02 fof(f8965,plain,(
% 122.68/16.02 upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|in(sK37_skl,sK35_skl)|~subset(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK34_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f8959,f748])).
% 122.68/16.02 fof(f9001,plain,(
% 122.68/16.02 in(sK37_skl,sK35_skl)|~subset(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK34_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f8965,f684])).
% 122.68/16.02 fof(f9002,plain,(
% 122.68/16.02 in(sK37_skl,sK35_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f9001,f904])).
% 122.68/16.02 fof(f9003,plain,(
% 122.68/16.02 in(sK37_skl,sK35_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f9002,f748])).
% 122.68/16.02 fof(f9004,plain,(
% 122.68/16.02 ![X0,X1]: (upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)))),
% 122.68/16.02 inference(resolution,[status(thm)],[f8964,f904])).
% 122.68/16.02 fof(f9005,plain,(
% 122.68/16.02 ![X0,X1]: (upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|~element(sK35_skl,powerset(powerset(sK34_skl))))),
% 122.68/16.02 inference(duplicate_literals_removal,[status(thm)],[f9004])).
% 122.68/16.02 fof(f9006,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|~element(sK35_skl,powerset(powerset(sK34_skl))))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f9005,f3947])).
% 122.68/16.02 fof(f9007,plain,(
% 122.68/16.02 in(sK37_skl,sK35_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f9003,f684])).
% 122.68/16.02 fof(f9008,plain,(
% 122.68/16.02 in(sK37_skl,sK35_skl)|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(the_carrier(boole_POSet(sK34_skl))))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f9007,f313])).
% 122.68/16.02 fof(f9014,plain,(
% 122.68/16.02 in(sK37_skl,sK35_skl)|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f9008])).
% 122.68/16.02 fof(f9015,plain,(
% 122.68/16.02 in(sK37_skl,sK35_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f9014,f319])).
% 122.68/16.02 fof(f9048,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f9006,f748])).
% 122.68/16.02 fof(f9049,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(the_carrier(boole_POSet(sK34_skl))))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)))),
% 122.68/16.02 inference(resolution,[status(thm)],[f9048,f313])).
% 122.68/16.02 fof(f9055,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f9049])).
% 122.68/16.02 fof(f9056,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f9055,f319])).
% 122.68/16.02 fof(f9057,plain,(
% 122.68/16.02 in(sK37_skl,sK35_skl)),
% 122.68/16.02 inference(backward_subsumption_resolution,[status(thm)],[f684,f9058])).
% 122.68/16.02 fof(f9058,plain,(
% 122.68/16.02 in(sK37_skl,sK35_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f9015,f748])).
% 122.68/16.02 fof(f9067,plain,(
% 122.68/16.02 ![X0,X1,X2]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|~subset(sK37_skl,X2)|~subset(X2,sK34_skl)|in(X2,sK35_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f9057,f3975])).
% 122.68/16.02 fof(f9331,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f9056,f748])).
% 122.68/16.02 fof(f9332,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|subset(sK36_skl,sK34_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f9331,f683])).
% 122.68/16.02 fof(f9333,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|subset(sK37_skl,sK36_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f9331,f682])).
% 122.68/16.02 fof(f9453,plain,(
% 122.68/16.02 ![X0]: (~element(X0,powerset(sK34_skl))|~subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),X0)|in(X0,sK35_skl)|subset(sK36_skl,sK34_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)))),
% 122.68/16.02 inference(resolution,[status(thm)],[f9332,f926])).
% 122.68/16.02 fof(f9454,plain,(
% 122.68/16.02 ![X0]: (~element(X0,powerset(sK34_skl))|~subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),X0)|in(X0,sK35_skl)|subset(sK36_skl,sK34_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f9453,f683])).
% 122.68/16.02 fof(f9644,plain,(
% 122.68/16.02 ![X0]: (~element(X0,powerset(sK34_skl))|~subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),X0)|in(X0,sK35_skl)|subset(sK37_skl,sK36_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)))),
% 122.68/16.02 inference(resolution,[status(thm)],[f9333,f926])).
% 122.68/16.02 fof(f9645,plain,(
% 122.68/16.02 ![X0]: (~element(X0,powerset(sK34_skl))|~subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),X0)|in(X0,sK35_skl)|subset(sK37_skl,sK36_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f9644,f682])).
% 122.68/16.02 fof(f10348,plain,(
% 122.68/16.02 ~element(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl))|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|subset(sK36_skl,sK34_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f9454,f3946])).
% 122.68/16.02 fof(f10351,plain,(
% 122.68/16.02 in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|subset(sK36_skl,sK34_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f10348,f879])).
% 122.68/16.02 fof(f10663,plain,(
% 122.68/16.02 ~element(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl))|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|subset(sK37_skl,sK36_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f9645,f3946])).
% 122.68/16.02 fof(f10666,plain,(
% 122.68/16.02 in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|subset(sK37_skl,sK36_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f10663,f879])).
% 122.68/16.02 fof(f11801,plain,(
% 122.68/16.02 in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|subset(sK36_skl,sK34_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f10351,f748])).
% 122.68/16.02 fof(f11802,plain,(
% 122.68/16.02 subset(sK36_skl,sK34_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(the_carrier(boole_POSet(sK34_skl))))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f11801,f313])).
% 122.68/16.02 fof(f11810,plain,(
% 122.68/16.02 subset(sK36_skl,sK34_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f11802])).
% 122.68/16.02 fof(f11811,plain,(
% 122.68/16.02 subset(sK36_skl,sK34_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))),
% 122.68/16.02 inference(duplicate_literals_removal,[status(thm)],[f11810])).
% 122.68/16.02 fof(f11812,plain,(
% 122.68/16.02 subset(sK36_skl,sK34_skl)|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f11811,f683])).
% 122.68/16.02 fof(f11818,plain,(
% 122.68/16.02 in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|subset(sK37_skl,sK36_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f10666,f748])).
% 122.68/16.02 fof(f11819,plain,(
% 122.68/16.02 subset(sK37_skl,sK36_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(the_carrier(boole_POSet(sK34_skl))))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f11818,f313])).
% 122.68/16.02 fof(f11827,plain,(
% 122.68/16.02 subset(sK37_skl,sK36_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.68/16.02 inference(forward_demodulation,[status(thm)],[f701,f11819])).
% 122.68/16.02 fof(f11828,plain,(
% 122.68/16.02 subset(sK37_skl,sK36_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))),
% 122.68/16.02 inference(duplicate_literals_removal,[status(thm)],[f11827])).
% 122.68/16.02 fof(f11829,plain,(
% 122.68/16.02 subset(sK37_skl,sK36_skl)|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f11828,f682])).
% 122.68/16.02 fof(f12092,plain,(
% 122.68/16.02 subset(sK36_skl,sK34_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f11812,f319])).
% 122.68/16.02 fof(f12093,plain,(
% 122.68/16.02 subset(sK36_skl,sK34_skl)),
% 122.68/16.02 inference(resolution,[status(thm)],[f12092,f748])).
% 122.68/16.02 fof(f12484,plain,(
% 122.68/16.02 subset(sK37_skl,sK36_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f11829,f319])).
% 122.68/16.02 fof(f12485,plain,(
% 122.68/16.02 subset(sK37_skl,sK36_skl)),
% 122.68/16.02 inference(resolution,[status(thm)],[f12484,f748])).
% 122.68/16.02 fof(f12491,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|~subset(sK36_skl,sK34_skl)|in(sK36_skl,sK35_skl))),
% 122.68/16.02 inference(resolution,[status(thm)],[f12485,f9067])).
% 122.68/16.02 fof(f12493,plain,(
% 122.68/16.02 ![X0,X1]: (~element(X0,powerset(sK34_skl))|~subset(X1,X0)|~in(X1,sK35_skl)|in(X0,sK35_skl)|in(sK36_skl,sK35_skl))),
% 122.68/16.02 inference(forward_subsumption_resolution,[status(thm)],[f12491,f12093])).
% 122.68/16.02 fof(f13008,plain,(
% 122.68/16.02 ![X0]: (~element(X0,powerset(sK34_skl))|~subset(sK37_skl,X0)|in(X0,sK35_skl)|in(sK36_skl,sK35_skl))),
% 122.90/16.11 inference(resolution,[status(thm)],[f12493,f9057])).
% 122.90/16.11 fof(f13102,plain,(
% 122.90/16.11 ~element(sK36_skl,powerset(sK34_skl))|in(sK36_skl,sK35_skl)|in(sK36_skl,sK35_skl)),
% 122.90/16.11 inference(resolution,[status(thm)],[f13008,f12485])).
% 122.90/16.11 fof(f13104,plain,(
% 122.90/16.11 ~element(sK36_skl,powerset(sK34_skl))|in(sK36_skl,sK35_skl)),
% 122.90/16.11 inference(duplicate_literals_removal,[status(thm)],[f13102])).
% 122.90/16.11 fof(f13224,plain,(
% 122.90/16.11 in(sK36_skl,sK35_skl)|~subset(sK36_skl,sK34_skl)),
% 122.90/16.11 inference(resolution,[status(thm)],[f13104,f697])).
% 122.90/16.11 fof(f13226,plain,(
% 122.90/16.11 in(sK36_skl,sK35_skl)),
% 122.90/16.11 inference(forward_subsumption_resolution,[status(thm)],[f13224,f12093])).
% 122.90/16.11 fof(f13230,plain,(
% 122.90/16.11 ~upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.90/16.11 inference(backward_subsumption_resolution,[status(thm)],[f685,f13226])).
% 122.90/16.11 fof(f13275,plain,(
% 122.90/16.11 in(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)),
% 122.90/16.11 inference(backward_subsumption_resolution,[status(thm)],[f926,f13230])).
% 122.90/16.11 fof(f13277,plain,(
% 122.90/16.11 ![X0,X1]: (~subset(X0,X1)|~subset(X1,sK34_skl)|~in(X0,sK35_skl)|in(X1,sK35_skl))),
% 122.90/16.11 inference(backward_subsumption_resolution,[status(thm)],[f681,f13230])).
% 122.90/16.11 fof(f13292,plain,(
% 122.90/16.11 ![X0]: (~subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),X0)|~subset(X0,sK34_skl)|in(X0,sK35_skl))),
% 122.90/16.11 inference(resolution,[status(thm)],[f13275,f13277])).
% 122.90/16.11 fof(f13317,plain,(
% 122.90/16.11 ~subset(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK34_skl)|in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.90/16.11 inference(resolution,[status(thm)],[f13292,f3946])).
% 122.90/16.11 fof(f13320,plain,(
% 122.90/16.11 in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.90/16.11 inference(forward_subsumption_resolution,[status(thm)],[f13317,f904])).
% 122.90/16.11 fof(f13924,plain,(
% 122.90/16.11 in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.90/16.11 inference(forward_subsumption_resolution,[status(thm)],[f13320,f748])).
% 122.90/16.11 fof(f13925,plain,(
% 122.90/16.11 upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(the_carrier(boole_POSet(sK34_skl))))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.90/16.11 inference(resolution,[status(thm)],[f13924,f313])).
% 122.90/16.11 fof(f13931,plain,(
% 122.90/16.11 upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))|upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))),
% 122.90/16.11 inference(forward_demodulation,[status(thm)],[f701,f13925])).
% 122.90/16.11 fof(f13932,plain,(
% 122.90/16.11 upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))|~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))),
% 122.90/16.11 inference(duplicate_literals_removal,[status(thm)],[f13931])).
% 122.90/16.11 fof(f13933,plain,(
% 122.90/16.11 ~rel_str(boole_POSet(sK34_skl))|~element(sK35_skl,powerset(powerset(sK34_skl)))),
% 122.90/16.11 inference(forward_subsumption_resolution,[status(thm)],[f13932,f13230])).
% 122.90/16.11 fof(f14280,plain,(
% 122.90/16.11 ~element(sK35_skl,powerset(powerset(sK34_skl)))),
% 122.90/16.11 inference(forward_subsumption_resolution,[status(thm)],[f13933,f319])).
% 122.90/16.11 fof(f14281,plain,(
% 122.90/16.11 $false),
% 122.90/16.11 inference(backward_subsumption_resolution,[status(thm)],[f748,f14280])).
% 122.90/16.11 % SZS output end CNFRefutation for theBenchmark.p
% 38.61/16.18 % Elapsed time: 15.717885 seconds
% 38.61/16.18 % CPU time: 123.781615 seconds
% 38.61/16.18 % Total memory used: 716.983 MB
% 38.61/16.18 % Net memory used: 693.637 MB
%------------------------------------------------------------------------------