%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU383+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 : n002.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:29 PM UTC 2026
% Result : Theorem 6.47s 1.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU383+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.34 % Computer : n002.cluster.edu
% 0.10/0.34 % Model : x86_64 x86_64
% 0.10/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.34 % Memory : 8046.5625MB
% 0.10/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/0.34 % CPULimit : 300
% 0.10/0.34 % WCLimit : 300
% 0.10/0.34 % DateTime : Mon Sep 21 06:20:46 UTC 2026
% 0.10/0.34 % CPUTime :
% 0.10/0.36 % Drodi V4.1.1
% 6.47/1.54 % Refutation found
% 6.47/1.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.47/1.54 % SZS output start CNFRefutation for theBenchmark
% 6.47/1.54 fof(f8,axiom,(
% 6.47/1.54 (! [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) ) ) )) )) ) )) )),
% 6.47/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.54 fof(f12,axiom,(
% 6.47/1.54 (! [A] :( rel_str(A)=> element(bottom_of_relstr(A),the_carrier(A)) ) )),
% 6.47/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.54 fof(f13,axiom,(
% 6.47/1.54 (! [A] :( rel_str(A)=> one_sorted_str(A) ) )),
% 6.47/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.54 fof(f20,axiom,(
% 6.47/1.54 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> ~ empty(the_carrier(A)) ) )),
% 6.47/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.54 fof(f33,axiom,(
% 6.47/1.54 (! [A,B] : subset(A,A) )),
% 6.47/1.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.54 fof(f34,axiom,(
% 6.47/1.54 (! [A,B] :( in(A,B)=> element(A,B) ) )),
% 6.47/1.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.55 fof(f35,axiom,(
% 6.47/1.55 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 6.47/1.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.55 fof(f36,axiom,(
% 6.47/1.55 (! [A,B] :( (! [C] :( in(C,A)<=> in(C,B) ))=> A = B ) )),
% 6.47/1.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.55 fof(f37,axiom,(
% 6.47/1.55 (! [A,B] :( element(A,powerset(B))<=> subset(A,B) ) )),
% 6.47/1.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.55 fof(f38,axiom,(
% 6.47/1.55 (! [A] :( ( ~ empty_carrier(A)& antisymmetric_relstr(A)& lower_bounded_relstr(A)& rel_str(A) )=> (! [B] :( element(B,the_carrier(A))=> related(A,bottom_of_relstr(A),B) ) )) )),
% 6.47/1.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.55 fof(f39,axiom,(
% 6.47/1.55 (! [A,B,C] :( ( in(A,B)& element(B,powerset(C)) )=> element(A,C) ) )),
% 6.47/1.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.55 fof(f41,axiom,(
% 6.47/1.55 (! [A,B] :( element(B,powerset(A))=> ( proper_element(B,powerset(A))<=> B != A ) ) )),
% 6.47/1.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.55 fof(f45,conjecture,(
% 6.47/1.55 (! [A] :( ( ~ empty_carrier(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& lower_bounded_relstr(A)& rel_str(A) )=> (! [B] :( ( ~ empty(B)& filtered_subset(B,A)& upper_relstr_subset(B,A)& element(B,powerset(the_carrier(A))) )=> ( proper_element(B,powerset(the_carrier(A)))<=> ~ in(bottom_of_relstr(A),B) ) ) )) )),
% 6.47/1.55 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.47/1.55 fof(f46,negated_conjecture,(
% 6.47/1.55 ~((! [A] :( ( ~ empty_carrier(A)& reflexive_relstr(A)& transitive_relstr(A)& antisymmetric_relstr(A)& lower_bounded_relstr(A)& rel_str(A) )=> (! [B] :( ( ~ empty(B)& filtered_subset(B,A)& upper_relstr_subset(B,A)& element(B,powerset(the_carrier(A))) )=> ( proper_element(B,powerset(the_carrier(A)))<=> ~ in(bottom_of_relstr(A),B) ) ) )) ))),
% 6.47/1.55 inference(negated_conjecture,[status(cth)],[f45])).
% 6.47/1.55 fof(f62,plain,(
% 6.47/1.55 ![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))))))))))),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 6.47/1.55 fof(f63,plain,(
% 6.47/1.55 ![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)))))))))))),
% 6.47/1.55 inference(NNF_transformation,[status(thm)],[f62])).
% 6.47/1.55 fof(f64,plain,(
% 6.47/1.55 ![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)))))))))),
% 6.47/1.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(B,A)),skolemize(D,sK1_skl(B,A))],[f63])).
% 6.47/1.55 fof(f65,plain,(
% 6.47/1.55 ![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))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f64])).
% 6.47/1.55 fof(f74,plain,(
% 6.47/1.55 ![A]: (~rel_str(A)|element(bottom_of_relstr(A),the_carrier(A)))),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 6.47/1.55 fof(f75,plain,(
% 6.47/1.55 ![X0]: (~rel_str(X0)|element(bottom_of_relstr(X0),the_carrier(X0)))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f74])).
% 6.47/1.55 fof(f76,plain,(
% 6.47/1.55 ![A]: (~rel_str(A)|one_sorted_str(A))),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 6.47/1.55 fof(f77,plain,(
% 6.47/1.55 ![X0]: (~rel_str(X0)|one_sorted_str(X0))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f76])).
% 6.47/1.55 fof(f84,plain,(
% 6.47/1.55 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|~empty(the_carrier(A)))),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 6.47/1.55 fof(f85,plain,(
% 6.47/1.55 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|~empty(the_carrier(X0)))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f84])).
% 6.47/1.55 fof(f125,plain,(
% 6.47/1.55 ![A]: subset(A,A)),
% 6.47/1.55 inference(miniscoping,[status(thm)],[f33])).
% 6.47/1.55 fof(f126,plain,(
% 6.47/1.55 ![X0]: (subset(X0,X0))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f125])).
% 6.47/1.55 fof(f127,plain,(
% 6.47/1.55 ![A,B]: (~in(A,B)|element(A,B))),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 6.47/1.55 fof(f128,plain,(
% 6.47/1.55 ![X0,X1]: (~in(X0,X1)|element(X0,X1))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f127])).
% 6.47/1.55 fof(f129,plain,(
% 6.47/1.55 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 6.47/1.55 fof(f130,plain,(
% 6.47/1.55 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f129])).
% 6.47/1.55 fof(f131,plain,(
% 6.47/1.55 ![A,B]: ((?[C]: (in(C,A)<~>in(C,B)))|A=B)),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 6.47/1.55 fof(f132,plain,(
% 6.47/1.55 ![A,B]: ((?[C]: ((in(C,A)|in(C,B))&(~in(C,A)|~in(C,B))))|A=B)),
% 6.47/1.55 inference(NNF_transformation,[status(thm)],[f131])).
% 6.47/1.55 fof(f133,plain,(
% 6.47/1.55 ![A,B]: (((in(sK15_skl(B,A),A)|in(sK15_skl(B,A),B))&(~in(sK15_skl(B,A),A)|~in(sK15_skl(B,A),B)))|A=B)),
% 6.47/1.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(C,sK15_skl(B,A))],[f132])).
% 6.47/1.55 fof(f134,plain,(
% 6.47/1.55 ![X0,X1]: (in(sK15_skl(X0,X1),X1)|in(sK15_skl(X0,X1),X0)|X1=X0)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f133])).
% 6.47/1.55 fof(f135,plain,(
% 6.47/1.55 ![X0,X1]: (~in(sK15_skl(X0,X1),X1)|~in(sK15_skl(X0,X1),X0)|X1=X0)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f133])).
% 6.47/1.55 fof(f136,plain,(
% 6.47/1.55 ![A,B]: ((~element(A,powerset(B))|subset(A,B))&(element(A,powerset(B))|~subset(A,B)))),
% 6.47/1.55 inference(NNF_transformation,[status(thm)],[f37])).
% 6.47/1.55 fof(f137,plain,(
% 6.47/1.55 (![A,B]: (~element(A,powerset(B))|subset(A,B)))&(![A,B]: (element(A,powerset(B))|~subset(A,B)))),
% 6.47/1.55 inference(miniscoping,[status(thm)],[f136])).
% 6.47/1.55 fof(f139,plain,(
% 6.47/1.55 ![X0,X1]: (element(X0,powerset(X1))|~subset(X0,X1))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f137])).
% 6.47/1.55 fof(f140,plain,(
% 6.47/1.55 ![A]: ((((empty_carrier(A)|~antisymmetric_relstr(A))|~lower_bounded_relstr(A))|~rel_str(A))|(![B]: (~element(B,the_carrier(A))|related(A,bottom_of_relstr(A),B))))),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 6.47/1.55 fof(f141,plain,(
% 6.47/1.55 ![X0,X1]: (empty_carrier(X0)|~antisymmetric_relstr(X0)|~lower_bounded_relstr(X0)|~rel_str(X0)|~element(X1,the_carrier(X0))|related(X0,bottom_of_relstr(X0),X1))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f140])).
% 6.47/1.55 fof(f142,plain,(
% 6.47/1.55 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|element(A,C))),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 6.47/1.55 fof(f143,plain,(
% 6.47/1.55 ![A,C]: ((![B]: (~in(A,B)|~element(B,powerset(C))))|element(A,C))),
% 6.47/1.55 inference(miniscoping,[status(thm)],[f142])).
% 6.47/1.55 fof(f144,plain,(
% 6.47/1.55 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|element(X0,X2))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f143])).
% 6.47/1.55 fof(f148,plain,(
% 6.47/1.55 ![A,B]: (~element(B,powerset(A))|(proper_element(B,powerset(A))<=>~B=A))),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 6.47/1.55 fof(f149,plain,(
% 6.47/1.55 ![A,B]: (~element(B,powerset(A))|((~proper_element(B,powerset(A))|~B=A)&(proper_element(B,powerset(A))|B=A)))),
% 6.47/1.55 inference(NNF_transformation,[status(thm)],[f148])).
% 6.47/1.55 fof(f150,plain,(
% 6.47/1.55 ![X0,X1]: (~element(X0,powerset(X1))|~proper_element(X0,powerset(X1))|~X0=X1)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f149])).
% 6.47/1.55 fof(f151,plain,(
% 6.47/1.55 ![X0,X1]: (~element(X0,powerset(X1))|proper_element(X0,powerset(X1))|X0=X1)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f149])).
% 6.47/1.55 fof(f160,plain,(
% 6.47/1.55 (?[A]: ((((((~empty_carrier(A)&reflexive_relstr(A))&transitive_relstr(A))&antisymmetric_relstr(A))&lower_bounded_relstr(A))&rel_str(A))&(?[B]: ((((~empty(B)&filtered_subset(B,A))&upper_relstr_subset(B,A))&element(B,powerset(the_carrier(A))))&(proper_element(B,powerset(the_carrier(A)))<~>~in(bottom_of_relstr(A),B))))))),
% 6.47/1.55 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 6.47/1.55 fof(f161,plain,(
% 6.47/1.55 ?[A]: ((((((~empty_carrier(A)&reflexive_relstr(A))&transitive_relstr(A))&antisymmetric_relstr(A))&lower_bounded_relstr(A))&rel_str(A))&(?[B]: ((((~empty(B)&filtered_subset(B,A))&upper_relstr_subset(B,A))&element(B,powerset(the_carrier(A))))&((proper_element(B,powerset(the_carrier(A)))|~in(bottom_of_relstr(A),B))&(~proper_element(B,powerset(the_carrier(A)))|in(bottom_of_relstr(A),B))))))),
% 6.47/1.55 inference(NNF_transformation,[status(thm)],[f160])).
% 6.47/1.55 fof(f162,plain,(
% 6.47/1.55 ((((((~empty_carrier(sK16_skl)&reflexive_relstr(sK16_skl))&transitive_relstr(sK16_skl))&antisymmetric_relstr(sK16_skl))&lower_bounded_relstr(sK16_skl))&rel_str(sK16_skl))&((((~empty(sK17_skl)&filtered_subset(sK17_skl,sK16_skl))&upper_relstr_subset(sK17_skl,sK16_skl))&element(sK17_skl,powerset(the_carrier(sK16_skl))))&((proper_element(sK17_skl,powerset(the_carrier(sK16_skl)))|~in(bottom_of_relstr(sK16_skl),sK17_skl))&(~proper_element(sK17_skl,powerset(the_carrier(sK16_skl)))|in(bottom_of_relstr(sK16_skl),sK17_skl)))))),
% 6.47/1.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl]),skolemize(A,sK16_skl),skolemize(B,sK17_skl)],[f161])).
% 6.47/1.55 fof(f163,plain,(
% 6.47/1.55 ~empty_carrier(sK16_skl)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f162])).
% 6.47/1.55 fof(f166,plain,(
% 6.47/1.55 antisymmetric_relstr(sK16_skl)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f162])).
% 6.47/1.55 fof(f167,plain,(
% 6.47/1.55 lower_bounded_relstr(sK16_skl)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f162])).
% 6.47/1.55 fof(f168,plain,(
% 6.47/1.55 rel_str(sK16_skl)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f162])).
% 6.47/1.55 fof(f169,plain,(
% 6.47/1.55 ~empty(sK17_skl)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f162])).
% 6.47/1.55 fof(f171,plain,(
% 6.47/1.55 upper_relstr_subset(sK17_skl,sK16_skl)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f162])).
% 6.47/1.55 fof(f172,plain,(
% 6.47/1.55 element(sK17_skl,powerset(the_carrier(sK16_skl)))),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f162])).
% 6.47/1.55 fof(f173,plain,(
% 6.47/1.55 proper_element(sK17_skl,powerset(the_carrier(sK16_skl)))|~in(bottom_of_relstr(sK16_skl),sK17_skl)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f162])).
% 6.47/1.55 fof(f174,plain,(
% 6.47/1.55 ~proper_element(sK17_skl,powerset(the_carrier(sK16_skl)))|in(bottom_of_relstr(sK16_skl),sK17_skl)),
% 6.47/1.55 inference(cnf_transformation,[status(thm)],[f162])).
% 6.47/1.55 fof(f175,plain,(
% 6.47/1.55 ![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))),
% 6.47/1.55 inference(backward_subsumption_resolution,[status(thm)],[f65,f144])).
% 6.47/1.55 fof(f176,plain,(
% 6.47/1.55 ![X0]: (~element(X0,powerset(X0))|~proper_element(X0,powerset(X0)))),
% 6.47/1.55 inference(destructive_equality_resolution,[status(thm)],[f150])).
% 6.47/1.55 fof(f185,plain,(
% 6.47/1.55 ![X0]: (empty(the_carrier(X0))|in(bottom_of_relstr(X0),the_carrier(X0))|~rel_str(X0))),
% 6.47/1.55 inference(resolution,[status(thm)],[f130,f75])).
% 6.47/1.55 fof(f210,plain,(
% 6.47/1.55 one_sorted_str(sK16_skl)),
% 6.47/1.55 inference(resolution,[status(thm)],[f77,f168])).
% 6.47/1.55 fof(f244,plain,(
% 6.47/1.55 proper_element(sK17_skl,powerset(the_carrier(sK16_skl)))|sK17_skl=the_carrier(sK16_skl)),
% 6.47/1.55 inference(resolution,[status(thm)],[f151,f172])).
% 6.47/1.55 fof(f245,plain,(
% 6.47/1.55 ![X0,X1]: (~rel_str(sK16_skl)|~element(sK17_skl,powerset(the_carrier(sK16_skl)))|~element(X0,the_carrier(sK16_skl))|~in(X1,sK17_skl)|~related(sK16_skl,X1,X0)|in(X0,sK17_skl))),
% 6.47/1.55 inference(resolution,[status(thm)],[f175,f171])).
% 6.47/1.55 fof(f246,plain,(
% 6.47/1.55 ![X0,X1]: (~element(sK17_skl,powerset(the_carrier(sK16_skl)))|~element(X0,the_carrier(sK16_skl))|~in(X1,sK17_skl)|~related(sK16_skl,X1,X0)|in(X0,sK17_skl))),
% 6.47/1.55 inference(forward_subsumption_resolution,[status(thm)],[f245,f168])).
% 6.47/1.55 fof(f254,plain,(
% 6.47/1.55 ![X0]: (element(X0,powerset(X0)))),
% 6.47/1.55 inference(resolution,[status(thm)],[f139,f126])).
% 6.47/1.55 fof(f255,plain,(
% 6.47/1.55 ![X0]: (~proper_element(X0,powerset(X0)))),
% 6.47/1.55 inference(backward_subsumption_resolution,[status(thm)],[f176,f254])).
% 6.47/1.55 fof(f271,plain,(
% 6.47/1.55 sK17_skl=the_carrier(sK16_skl)|in(bottom_of_relstr(sK16_skl),sK17_skl)),
% 6.47/1.55 inference(resolution,[status(thm)],[f244,f174])).
% 6.47/1.55 fof(f277,plain,(
% 6.47/1.55 ![X0,X1]: (~element(X0,the_carrier(sK16_skl))|~in(X1,sK17_skl)|~related(sK16_skl,X1,X0)|in(X0,sK17_skl))),
% 6.47/1.55 inference(resolution,[status(thm)],[f246,f172])).
% 6.47/1.55 fof(f286,plain,(
% 6.47/1.55 empty(the_carrier(sK16_skl))|in(bottom_of_relstr(sK16_skl),the_carrier(sK16_skl))),
% 6.47/1.55 inference(resolution,[status(thm)],[f185,f168])).
% 6.47/1.55 fof(f462,plain,(
% 6.47/1.55 ![X0,X1,X2]: (in(sK15_skl(X0,X1),X1)|X1=X0|~element(X0,powerset(X2))|element(sK15_skl(X0,X1),X2))),
% 6.47/1.55 inference(resolution,[status(thm)],[f134,f144])).
% 6.47/1.55 fof(f586,plain,(
% 6.47/1.55 ![X0]: (~element(X0,the_carrier(sK16_skl))|~in(bottom_of_relstr(sK16_skl),sK17_skl)|in(X0,sK17_skl)|empty_carrier(sK16_skl)|~antisymmetric_relstr(sK16_skl)|~lower_bounded_relstr(sK16_skl)|~rel_str(sK16_skl)|~element(X0,the_carrier(sK16_skl)))),
% 6.47/1.55 inference(resolution,[status(thm)],[f277,f141])).
% 6.47/1.55 fof(f588,plain,(
% 6.47/1.55 ![X0]: (~element(X0,the_carrier(sK16_skl))|~in(bottom_of_relstr(sK16_skl),sK17_skl)|in(X0,sK17_skl)|empty_carrier(sK16_skl)|~antisymmetric_relstr(sK16_skl)|~lower_bounded_relstr(sK16_skl)|~rel_str(sK16_skl))),
% 6.47/1.55 inference(duplicate_literals_removal,[status(thm)],[f586])).
% 6.47/1.55 fof(f589,plain,(
% 6.47/1.55 ![X0]: (~element(X0,the_carrier(sK16_skl))|~in(bottom_of_relstr(sK16_skl),sK17_skl)|in(X0,sK17_skl)|~antisymmetric_relstr(sK16_skl)|~lower_bounded_relstr(sK16_skl)|~rel_str(sK16_skl))),
% 6.47/1.55 inference(forward_subsumption_resolution,[status(thm)],[f588,f163])).
% 6.47/1.55 fof(f713,plain,(
% 6.47/1.55 ![X0]: (in(sK15_skl(sK17_skl,X0),X0)|X0=sK17_skl|element(sK15_skl(sK17_skl,X0),the_carrier(sK16_skl)))),
% 6.47/1.55 inference(resolution,[status(thm)],[f462,f172])).
% 6.47/1.55 fof(f1048,plain,(
% 6.47/1.55 ![X0]: (X0=sK17_skl|element(sK15_skl(sK17_skl,X0),the_carrier(sK16_skl))|element(sK15_skl(sK17_skl,X0),X0))),
% 6.47/1.55 inference(resolution,[status(thm)],[f713,f128])).
% 6.47/1.55 fof(f1653,plain,(
% 6.47/1.55 the_carrier(sK16_skl)=sK17_skl|empty(the_carrier(sK16_skl))|in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),the_carrier(sK16_skl))),
% 6.47/1.55 inference(resolution,[status(thm)],[f1048,f130])).
% 6.47/1.55 fof(f1669,plain,(
% 6.47/1.55 ![X0]: (~element(X0,the_carrier(sK16_skl))|in(X0,sK17_skl)|~antisymmetric_relstr(sK16_skl)|~lower_bounded_relstr(sK16_skl)|~rel_str(sK16_skl)|sK17_skl=the_carrier(sK16_skl))),
% 6.47/1.55 inference(resolution,[status(thm)],[f589,f271])).
% 6.47/1.55 fof(f1670,plain,(
% 6.47/1.55 ![X0]: (~element(X0,the_carrier(sK16_skl))|in(X0,sK17_skl)|~lower_bounded_relstr(sK16_skl)|~rel_str(sK16_skl)|sK17_skl=the_carrier(sK16_skl))),
% 6.47/1.55 inference(forward_subsumption_resolution,[status(thm)],[f1669,f166])).
% 6.47/1.55 fof(f3013,plain,(
% 6.47/1.55 the_carrier(sK16_skl)=sK17_skl|empty(the_carrier(sK16_skl))|~in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl)|the_carrier(sK16_skl)=sK17_skl),
% 6.47/1.55 inference(resolution,[status(thm)],[f1653,f135])).
% 6.47/1.55 fof(f3017,plain,(
% 6.47/1.55 the_carrier(sK16_skl)=sK17_skl|empty(the_carrier(sK16_skl))|~in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl)),
% 6.47/1.55 inference(duplicate_literals_removal,[status(thm)],[f3013])).
% 6.47/1.55 fof(f3485,plain,(
% 6.47/1.55 ![X0]: (~element(X0,the_carrier(sK16_skl))|in(X0,sK17_skl)|~lower_bounded_relstr(sK16_skl)|sK17_skl=the_carrier(sK16_skl))),
% 6.47/1.55 inference(resolution,[status(thm)],[f1670,f168])).
% 6.47/1.55 fof(f3486,plain,(
% 6.47/1.55 ![X0]: (~element(X0,the_carrier(sK16_skl))|in(X0,sK17_skl)|sK17_skl=the_carrier(sK16_skl))),
% 6.47/1.55 inference(forward_subsumption_resolution,[status(thm)],[f3485,f167])).
% 6.47/1.55 fof(f3501,plain,(
% 6.47/1.55 in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl)|sK17_skl=the_carrier(sK16_skl)|the_carrier(sK16_skl)=sK17_skl),
% 8.79/1.58 inference(resolution,[status(thm)],[f3486,f1048])).
% 8.79/1.58 fof(f3557,plain,(
% 8.79/1.58 the_carrier(sK16_skl)=sK17_skl|empty(the_carrier(sK16_skl))),
% 8.79/1.58 inference(backward_subsumption_resolution,[status(thm)],[f3017,f3558])).
% 8.79/1.58 fof(f3558,plain,(
% 8.79/1.58 in(sK15_skl(sK17_skl,the_carrier(sK16_skl)),sK17_skl)|sK17_skl=the_carrier(sK16_skl)),
% 8.79/1.58 inference(duplicate_literals_removal,[status(thm)],[f3501])).
% 8.79/1.58 fof(f3567,plain,(
% 8.79/1.58 the_carrier(sK16_skl)=sK17_skl|empty_carrier(sK16_skl)|~one_sorted_str(sK16_skl)),
% 8.79/1.58 inference(resolution,[status(thm)],[f3557,f85])).
% 8.79/1.58 fof(f3575,plain,(
% 8.79/1.58 the_carrier(sK16_skl)=sK17_skl|~one_sorted_str(sK16_skl)),
% 8.79/1.58 inference(forward_subsumption_resolution,[status(thm)],[f3567,f163])).
% 8.79/1.58 fof(f3587,plain,(
% 8.79/1.58 the_carrier(sK16_skl)=sK17_skl),
% 8.79/1.58 inference(resolution,[status(thm)],[f3575,f210])).
% 8.79/1.58 fof(f3650,plain,(
% 8.79/1.58 empty(the_carrier(sK16_skl))|in(bottom_of_relstr(sK16_skl),sK17_skl)),
% 8.79/1.58 inference(backward_demodulation,[status(thm)],[f3587,f286])).
% 8.79/1.58 fof(f3662,plain,(
% 8.79/1.58 proper_element(sK17_skl,powerset(sK17_skl))|~in(bottom_of_relstr(sK16_skl),sK17_skl)),
% 8.79/1.58 inference(backward_demodulation,[status(thm)],[f3587,f173])).
% 8.79/1.58 fof(f3874,plain,(
% 8.79/1.58 empty(sK17_skl)|in(bottom_of_relstr(sK16_skl),sK17_skl)),
% 8.79/1.58 inference(forward_demodulation,[status(thm)],[f3587,f3650])).
% 8.79/1.58 fof(f3876,plain,(
% 8.79/1.58 in(bottom_of_relstr(sK16_skl),sK17_skl)),
% 8.79/1.58 inference(forward_subsumption_resolution,[status(thm)],[f3874,f169])).
% 8.79/1.58 fof(f3879,plain,(
% 8.79/1.58 ~in(bottom_of_relstr(sK16_skl),sK17_skl)),
% 8.79/1.58 inference(forward_subsumption_resolution,[status(thm)],[f3662,f255])).
% 8.79/1.58 fof(f3880,plain,(
% 8.79/1.58 $false),
% 8.79/1.58 inference(backward_subsumption_resolution,[status(thm)],[f3876,f3879])).
% 8.79/1.58 % SZS output end CNFRefutation for theBenchmark.p
% 8.79/1.59 % Elapsed time: 1.231084 seconds
% 8.79/1.59 % CPU time: 9.300303 seconds
% 8.79/1.59 % Total memory used: 165.949 MB
% 8.79/1.59 % Net memory used: 159.937 MB
%------------------------------------------------------------------------------