%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU325+2 : 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 : n003.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:20 PM UTC 2026
% Result : Theorem 46.19s 6.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU325+2 : 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 : n003.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:13:30 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.27/0.55 % Drodi V4.1.1
% 46.19/6.52 % Refutation found
% 46.19/6.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 46.19/6.52 % SZS output start CNFRefutation for theBenchmark
% 46.19/6.52 fof(f40,axiom,(
% 46.19/6.52 (! [A,B] :( A = B<=> ( subset(A,B)& subset(B,A) ) ) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f63,axiom,(
% 46.19/6.52 (! [A] :( one_sorted_str(A)=> ( empty_carrier(A)<=> empty(the_carrier(A)) ) ) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f68,axiom,(
% 46.19/6.52 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f69,axiom,(
% 46.19/6.52 (! [A,B] :( B = powerset(A)<=> (! [C] :( in(C,B)<=> subset(C,A) ) )) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f82,axiom,(
% 46.19/6.52 (! [A] :( one_sorted_str(A)=> cast_as_carrier_subset(A) = the_carrier(A) ) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f91,axiom,(
% 46.19/6.52 (! [A] : cast_to_subset(A) = A )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f92,axiom,(
% 46.19/6.52 (! [A,B] :( B = union(A)<=> (! [C] :( in(C,B)<=> (? [D] :( in(C,D)& in(D,A) ) )) )) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f95,axiom,(
% 46.19/6.52 (! [A,B,C] :( C = set_difference(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)& ~ in(D,B) ) ) )) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f100,axiom,(
% 46.19/6.52 (! [A,B] :( element(B,powerset(A))=> subset_complement(A,B) = set_difference(A,B) ) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f113,axiom,(
% 46.19/6.52 (! [A] :( one_sorted_str(A)=> (! [B] :( element(B,powerset(powerset(the_carrier(A))))=> ( is_a_cover_of_carrier(A,B)<=> cast_as_carrier_subset(A) = union_of_subsets(the_carrier(A),B) ) ) )) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f142,axiom,(
% 46.19/6.52 (! [A] : element(cast_to_subset(A),powerset(A)) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f149,axiom,(
% 46.19/6.52 (! [A,B] :( element(B,powerset(A))=> element(subset_complement(A,B),powerset(A)) ) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f195,axiom,(
% 46.19/6.52 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f313,axiom,(
% 46.19/6.52 (! [A,B] :( element(B,powerset(powerset(A)))=> union_of_subsets(A,B) = union(B) ) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f400,axiom,(
% 46.19/6.52 (! [A,B] :( in(A,B)=> element(A,B) ) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f498,conjecture,(
% 46.19/6.52 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( element(B,powerset(powerset(the_carrier(A))))=> ~ ( is_a_cover_of_carrier(A,B)& B = empty_set ) ) )) )),
% 46.19/6.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.19/6.52 fof(f499,negated_conjecture,(
% 46.19/6.52 ~((! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( element(B,powerset(powerset(the_carrier(A))))=> ~ ( is_a_cover_of_carrier(A,B)& B = empty_set ) ) )) ))),
% 46.19/6.52 inference(negated_conjecture,[status(cth)],[f498])).
% 46.19/6.52 fof(f662,plain,(
% 46.19/6.52 ![A,B]: ((~A=B|(subset(A,B)&subset(B,A)))&(A=B|(~subset(A,B)|~subset(B,A))))),
% 46.19/6.52 inference(NNF_transformation,[status(thm)],[f40])).
% 46.19/6.52 fof(f663,plain,(
% 46.19/6.52 (![A,B]: (~A=B|(subset(A,B)&subset(B,A))))&(![A,B]: (A=B|(~subset(A,B)|~subset(B,A))))),
% 46.19/6.52 inference(miniscoping,[status(thm)],[f662])).
% 46.19/6.52 fof(f664,plain,(
% 46.19/6.52 ![X0,X1]: (~X0=X1|subset(X0,X1))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f663])).
% 46.19/6.52 fof(f846,plain,(
% 46.19/6.52 ![A]: (~one_sorted_str(A)|(empty_carrier(A)<=>empty(the_carrier(A))))),
% 46.19/6.52 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 46.19/6.52 fof(f847,plain,(
% 46.19/6.52 ![A]: (~one_sorted_str(A)|((~empty_carrier(A)|empty(the_carrier(A)))&(empty_carrier(A)|~empty(the_carrier(A)))))),
% 46.19/6.52 inference(NNF_transformation,[status(thm)],[f846])).
% 46.19/6.52 fof(f849,plain,(
% 46.19/6.52 ![X0]: (~one_sorted_str(X0)|empty_carrier(X0)|~empty(the_carrier(X0)))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f847])).
% 46.19/6.52 fof(f880,plain,(
% 46.19/6.52 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 46.19/6.52 inference(NNF_transformation,[status(thm)],[f68])).
% 46.19/6.52 fof(f881,plain,(
% 46.19/6.52 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 46.19/6.52 inference(miniscoping,[status(thm)],[f880])).
% 46.19/6.52 fof(f882,plain,(
% 46.19/6.52 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK40_skl(A),A)))),
% 46.19/6.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl]),skolemize(B,sK40_skl(A))],[f881])).
% 46.19/6.52 fof(f883,plain,(
% 46.19/6.52 ![X0,X1]: (~X0=empty_set|~in(X1,X0))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f882])).
% 46.19/6.52 fof(f885,plain,(
% 46.19/6.52 ![A,B]: ((~B=powerset(A)|(![C]: ((~in(C,B)|subset(C,A))&(in(C,B)|~subset(C,A)))))&(B=powerset(A)|(?[C]: ((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))))),
% 46.19/6.52 inference(NNF_transformation,[status(thm)],[f69])).
% 46.19/6.52 fof(f886,plain,(
% 46.19/6.52 (![A,B]: (~B=powerset(A)|((![C]: (~in(C,B)|subset(C,A)))&(![C]: (in(C,B)|~subset(C,A))))))&(![A,B]: (B=powerset(A)|(?[C]: ((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))))),
% 46.19/6.52 inference(miniscoping,[status(thm)],[f885])).
% 46.19/6.52 fof(f887,plain,(
% 46.19/6.52 (![A,B]: (~B=powerset(A)|((![C]: (~in(C,B)|subset(C,A)))&(![C]: (in(C,B)|~subset(C,A))))))&(![A,B]: (B=powerset(A)|((~in(sK41_skl(B,A),B)|~subset(sK41_skl(B,A),A))&(in(sK41_skl(B,A),B)|subset(sK41_skl(B,A),A)))))),
% 46.19/6.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl]),skolemize(C,sK41_skl(B,A))],[f886])).
% 46.19/6.52 fof(f889,plain,(
% 46.19/6.52 ![X0,X1,X2]: (~X0=powerset(X1)|in(X2,X0)|~subset(X2,X1))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f887])).
% 46.19/6.52 fof(f974,plain,(
% 46.19/6.52 ![A]: (~one_sorted_str(A)|cast_as_carrier_subset(A)=the_carrier(A))),
% 46.19/6.52 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 46.19/6.52 fof(f975,plain,(
% 46.19/6.52 ![X0]: (~one_sorted_str(X0)|cast_as_carrier_subset(X0)=the_carrier(X0))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f974])).
% 46.19/6.52 fof(f1037,plain,(
% 46.19/6.52 ![X0]: (cast_to_subset(X0)=X0)),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f91])).
% 46.19/6.52 fof(f1038,plain,(
% 46.19/6.52 ![A,B]: ((~B=union(A)|(![C]: ((~in(C,B)|(?[D]: (in(C,D)&in(D,A))))&(in(C,B)|(![D]: (~in(C,D)|~in(D,A)))))))&(B=union(A)|(?[C]: ((~in(C,B)|(![D]: (~in(C,D)|~in(D,A))))&(in(C,B)|(?[D]: (in(C,D)&in(D,A))))))))),
% 46.19/6.52 inference(NNF_transformation,[status(thm)],[f92])).
% 46.19/6.52 fof(f1039,plain,(
% 46.19/6.52 (![A,B]: (~B=union(A)|((![C]: (~in(C,B)|(?[D]: (in(C,D)&in(D,A)))))&(![C]: (in(C,B)|(![D]: (~in(C,D)|~in(D,A))))))))&(![A,B]: (B=union(A)|(?[C]: ((~in(C,B)|(![D]: (~in(C,D)|~in(D,A))))&(in(C,B)|(?[D]: (in(C,D)&in(D,A))))))))),
% 46.19/6.52 inference(miniscoping,[status(thm)],[f1038])).
% 46.19/6.52 fof(f1040,plain,(
% 46.19/6.52 (![A,B]: (~B=union(A)|((![C]: (~in(C,B)|(in(C,sK69_skl(C,B,A))&in(sK69_skl(C,B,A),A))))&(![C]: (in(C,B)|(![D]: (~in(C,D)|~in(D,A))))))))&(![A,B]: (B=union(A)|((~in(sK70_skl(B,A),B)|(![D]: (~in(sK70_skl(B,A),D)|~in(D,A))))&(in(sK70_skl(B,A),B)|(in(sK70_skl(B,A),sK71_skl(B,A))&in(sK71_skl(B,A),A))))))),
% 46.19/6.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK69_skl,sK70_skl,sK71_skl]),skolemize(D,sK69_skl(C,B,A)),skolemize(C,sK70_skl(B,A)),skolemize(D,sK71_skl(B,A))],[f1039])).
% 46.19/6.52 fof(f1046,plain,(
% 46.19/6.52 ![X0,X1]: (X0=union(X1)|in(sK70_skl(X0,X1),X0)|in(sK71_skl(X0,X1),X1))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f1040])).
% 46.19/6.52 fof(f1064,plain,(
% 46.19/6.52 ![A,B,C]: ((~C=set_difference(A,B)|(![D]: ((~in(D,C)|(in(D,A)&~in(D,B)))&(in(D,C)|(~in(D,A)|in(D,B))))))&(C=set_difference(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)|in(D,B)))&(in(D,C)|(in(D,A)&~in(D,B)))))))),
% 46.19/6.52 inference(NNF_transformation,[status(thm)],[f95])).
% 46.19/6.52 fof(f1065,plain,(
% 46.19/6.52 (![A,B,C]: (~C=set_difference(A,B)|((![D]: (~in(D,C)|(in(D,A)&~in(D,B))))&(![D]: (in(D,C)|(~in(D,A)|in(D,B)))))))&(![A,B,C]: (C=set_difference(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)|in(D,B)))&(in(D,C)|(in(D,A)&~in(D,B)))))))),
% 46.19/6.52 inference(miniscoping,[status(thm)],[f1064])).
% 46.19/6.52 fof(f1066,plain,(
% 46.19/6.52 (![A,B,C]: (~C=set_difference(A,B)|((![D]: (~in(D,C)|(in(D,A)&~in(D,B))))&(![D]: (in(D,C)|(~in(D,A)|in(D,B)))))))&(![A,B,C]: (C=set_difference(A,B)|((~in(sK73_skl(C,B,A),C)|(~in(sK73_skl(C,B,A),A)|in(sK73_skl(C,B,A),B)))&(in(sK73_skl(C,B,A),C)|(in(sK73_skl(C,B,A),A)&~in(sK73_skl(C,B,A),B))))))),
% 46.19/6.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK73_skl]),skolemize(D,sK73_skl(C,B,A))],[f1065])).
% 46.19/6.52 fof(f1071,plain,(
% 46.19/6.52 ![X0,X1,X2]: (X0=set_difference(X1,X2)|in(sK73_skl(X0,X2,X1),X0)|in(sK73_skl(X0,X2,X1),X1))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f1066])).
% 46.19/6.52 fof(f1072,plain,(
% 46.19/6.52 ![X0,X1,X2]: (X0=set_difference(X1,X2)|in(sK73_skl(X0,X2,X1),X0)|~in(sK73_skl(X0,X2,X1),X2))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f1066])).
% 46.19/6.52 fof(f1107,plain,(
% 46.19/6.52 ![A,B]: (~element(B,powerset(A))|subset_complement(A,B)=set_difference(A,B))),
% 46.19/6.52 inference(pre_NNF_transformation,[status(thm)],[f100])).
% 46.19/6.52 fof(f1108,plain,(
% 46.19/6.52 ![X0,X1]: (~element(X0,powerset(X1))|subset_complement(X1,X0)=set_difference(X1,X0))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f1107])).
% 46.19/6.52 fof(f1181,plain,(
% 46.19/6.52 ![A]: (~one_sorted_str(A)|(![B]: (~element(B,powerset(powerset(the_carrier(A))))|(is_a_cover_of_carrier(A,B)<=>cast_as_carrier_subset(A)=union_of_subsets(the_carrier(A),B)))))),
% 46.19/6.52 inference(pre_NNF_transformation,[status(thm)],[f113])).
% 46.19/6.52 fof(f1182,plain,(
% 46.19/6.52 ![A]: (~one_sorted_str(A)|(![B]: (~element(B,powerset(powerset(the_carrier(A))))|((~is_a_cover_of_carrier(A,B)|cast_as_carrier_subset(A)=union_of_subsets(the_carrier(A),B))&(is_a_cover_of_carrier(A,B)|~cast_as_carrier_subset(A)=union_of_subsets(the_carrier(A),B))))))),
% 46.19/6.52 inference(NNF_transformation,[status(thm)],[f1181])).
% 46.19/6.52 fof(f1183,plain,(
% 46.19/6.52 ![X0,X1]: (~one_sorted_str(X0)|~element(X1,powerset(powerset(the_carrier(X0))))|~is_a_cover_of_carrier(X0,X1)|cast_as_carrier_subset(X0)=union_of_subsets(the_carrier(X0),X1))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f1182])).
% 46.19/6.52 fof(f1241,plain,(
% 46.19/6.52 ![X0]: (element(cast_to_subset(X0),powerset(X0)))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f142])).
% 46.19/6.52 fof(f1247,plain,(
% 46.19/6.52 ![A,B]: (~element(B,powerset(A))|element(subset_complement(A,B),powerset(A)))),
% 46.19/6.52 inference(pre_NNF_transformation,[status(thm)],[f149])).
% 46.19/6.52 fof(f1248,plain,(
% 46.19/6.52 ![X0,X1]: (~element(X0,powerset(X1))|element(subset_complement(X1,X0),powerset(X1)))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f1247])).
% 46.19/6.52 fof(f1330,plain,(
% 46.19/6.52 empty(empty_set)),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f195])).
% 46.19/6.52 fof(f1762,plain,(
% 46.19/6.52 ![A,B]: (~element(B,powerset(powerset(A)))|union_of_subsets(A,B)=union(B))),
% 46.19/6.52 inference(pre_NNF_transformation,[status(thm)],[f313])).
% 46.19/6.52 fof(f1763,plain,(
% 46.19/6.52 ![X0,X1]: (~element(X0,powerset(powerset(X1)))|union_of_subsets(X1,X0)=union(X0))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f1762])).
% 46.19/6.52 fof(f2285,plain,(
% 46.19/6.52 ![A,B]: (~in(A,B)|element(A,B))),
% 46.19/6.52 inference(pre_NNF_transformation,[status(thm)],[f400])).
% 46.19/6.52 fof(f2286,plain,(
% 46.19/6.52 ![X0,X1]: (~in(X0,X1)|element(X0,X1))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f2285])).
% 46.19/6.52 fof(f2609,plain,(
% 46.19/6.52 (?[A]: ((~empty_carrier(A)&one_sorted_str(A))&(?[B]: (element(B,powerset(powerset(the_carrier(A))))&(is_a_cover_of_carrier(A,B)&B=empty_set)))))),
% 46.19/6.52 inference(pre_NNF_transformation,[status(thm)],[f499])).
% 46.19/6.52 fof(f2610,plain,(
% 46.19/6.52 ((~empty_carrier(sK304_skl)&one_sorted_str(sK304_skl))&(element(sK305_skl,powerset(powerset(the_carrier(sK304_skl))))&(is_a_cover_of_carrier(sK304_skl,sK305_skl)&sK305_skl=empty_set)))),
% 46.19/6.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK304_skl,sK305_skl]),skolemize(A,sK304_skl),skolemize(B,sK305_skl)],[f2609])).
% 46.19/6.52 fof(f2611,plain,(
% 46.19/6.52 ~empty_carrier(sK304_skl)),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f2610])).
% 46.19/6.52 fof(f2612,plain,(
% 46.19/6.52 one_sorted_str(sK304_skl)),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f2610])).
% 46.19/6.52 fof(f2613,plain,(
% 46.19/6.52 element(sK305_skl,powerset(powerset(the_carrier(sK304_skl))))),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f2610])).
% 46.19/6.52 fof(f2614,plain,(
% 46.19/6.52 is_a_cover_of_carrier(sK304_skl,sK305_skl)),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f2610])).
% 46.19/6.52 fof(f2615,plain,(
% 46.19/6.52 sK305_skl=empty_set),
% 46.19/6.52 inference(cnf_transformation,[status(thm)],[f2610])).
% 46.19/6.52 fof(f3119,plain,(
% 46.19/6.52 ![X0]: (subset(X0,X0))),
% 46.19/6.52 inference(destructive_equality_resolution,[status(thm)],[f664])).
% 46.19/6.52 fof(f3166,plain,(
% 46.19/6.52 ![X0]: (~in(X0,empty_set))),
% 46.19/6.52 inference(destructive_equality_resolution,[status(thm)],[f883])).
% 46.19/6.52 fof(f3168,plain,(
% 46.19/6.52 ![X0,X1]: (in(X0,powerset(X1))|~subset(X0,X1))),
% 46.19/6.52 inference(destructive_equality_resolution,[status(thm)],[f889])).
% 46.19/6.52 fof(f3326,plain,(
% 46.19/6.52 element(empty_set,powerset(powerset(the_carrier(sK304_skl))))),
% 41.09/6.57 inference(backward_demodulation,[status(thm)],[f2615,f2613])).
% 41.09/6.57 fof(f3327,plain,(
% 41.09/6.57 is_a_cover_of_carrier(sK304_skl,empty_set)),
% 41.09/6.57 inference(forward_demodulation,[status(thm)],[f2615,f2614])).
% 41.09/6.57 fof(f3328,plain,(
% 41.09/6.57 ~one_sorted_str(sK304_skl)|~element(empty_set,powerset(powerset(the_carrier(sK304_skl))))|cast_as_carrier_subset(sK304_skl)=union_of_subsets(the_carrier(sK304_skl),empty_set)),
% 41.09/6.57 inference(resolution,[status(thm)],[f3327,f1183])).
% 41.09/6.57 fof(f3329,plain,(
% 41.09/6.57 ~element(empty_set,powerset(powerset(the_carrier(sK304_skl))))|cast_as_carrier_subset(sK304_skl)=union_of_subsets(the_carrier(sK304_skl),empty_set)),
% 41.09/6.57 inference(forward_subsumption_resolution,[status(thm)],[f3328,f2612])).
% 41.09/6.57 fof(f3330,plain,(
% 41.09/6.57 cast_as_carrier_subset(sK304_skl)=union_of_subsets(the_carrier(sK304_skl),empty_set)),
% 41.09/6.57 inference(forward_subsumption_resolution,[status(thm)],[f3329,f3326])).
% 41.09/6.57 fof(f5754,plain,(
% 41.09/6.57 ![X0]: (in(X0,powerset(X0)))),
% 41.09/6.57 inference(resolution,[status(thm)],[f3168,f3119])).
% 41.09/6.57 fof(f7571,plain,(
% 41.09/6.57 cast_as_carrier_subset(sK304_skl)=the_carrier(sK304_skl)),
% 41.09/6.57 inference(resolution,[status(thm)],[f975,f2612])).
% 41.09/6.57 fof(f7592,plain,(
% 41.09/6.57 the_carrier(sK304_skl)=union_of_subsets(the_carrier(sK304_skl),empty_set)),
% 41.09/6.57 inference(backward_demodulation,[status(thm)],[f7571,f3330])).
% 41.09/6.57 fof(f9387,plain,(
% 41.09/6.57 ![X0]: (empty_set=union(X0)|in(sK71_skl(empty_set,X0),X0))),
% 41.09/6.57 inference(resolution,[status(thm)],[f1046,f3166])).
% 41.09/6.57 fof(f9553,plain,(
% 41.09/6.57 empty_set=union(empty_set)),
% 41.09/6.57 inference(resolution,[status(thm)],[f9387,f3166])).
% 41.09/6.57 fof(f9974,plain,(
% 41.09/6.57 ![X0,X1]: (empty_set=set_difference(X0,X1)|in(sK73_skl(empty_set,X1,X0),X0))),
% 41.09/6.57 inference(resolution,[status(thm)],[f1071,f3166])).
% 41.09/6.57 fof(f10179,plain,(
% 41.09/6.57 ![X0]: (empty_set=set_difference(X0,X0)|empty_set=set_difference(X0,X0)|in(sK73_skl(empty_set,X0,X0),empty_set))),
% 41.09/6.57 inference(resolution,[status(thm)],[f9974,f1072])).
% 41.09/6.57 fof(f10231,plain,(
% 41.09/6.57 ![X0]: (empty_set=set_difference(X0,X0)|in(sK73_skl(empty_set,X0,X0),empty_set))),
% 41.09/6.57 inference(duplicate_literals_removal,[status(thm)],[f10179])).
% 41.09/6.57 fof(f10232,plain,(
% 41.09/6.57 ![X0]: (empty_set=set_difference(X0,X0))),
% 41.09/6.57 inference(forward_subsumption_resolution,[status(thm)],[f10231,f3166])).
% 41.09/6.57 fof(f12885,plain,(
% 41.09/6.57 ![X0]: (element(X0,powerset(X0)))),
% 41.09/6.57 inference(forward_demodulation,[status(thm)],[f1037,f1241])).
% 41.09/6.57 fof(f12938,plain,(
% 41.09/6.57 ![X0]: (subset_complement(X0,X0)=set_difference(X0,X0))),
% 41.09/6.57 inference(resolution,[status(thm)],[f12885,f1108])).
% 41.09/6.57 fof(f12973,plain,(
% 41.09/6.57 ![X0]: (subset_complement(X0,X0)=empty_set)),
% 41.09/6.57 inference(forward_demodulation,[status(thm)],[f10232,f12938])).
% 41.09/6.57 fof(f13104,plain,(
% 41.09/6.57 ![X0,X1]: (element(subset_complement(X0,X1),powerset(X0))|~in(X1,powerset(X0)))),
% 41.09/6.57 inference(resolution,[status(thm)],[f1248,f2286])).
% 41.09/6.57 fof(f16592,plain,(
% 41.09/6.57 ![X0]: (element(subset_complement(X0,X0),powerset(X0)))),
% 41.09/6.57 inference(resolution,[status(thm)],[f5754,f13104])).
% 41.09/6.57 fof(f16613,plain,(
% 41.09/6.57 ![X0]: (element(empty_set,powerset(X0)))),
% 41.09/6.57 inference(forward_demodulation,[status(thm)],[f12973,f16592])).
% 41.09/6.57 fof(f20543,plain,(
% 41.09/6.57 ![X0]: (union_of_subsets(X0,empty_set)=union(empty_set))),
% 41.09/6.57 inference(resolution,[status(thm)],[f1763,f16613])).
% 41.09/6.57 fof(f20549,plain,(
% 41.09/6.57 ![X0]: (union_of_subsets(X0,empty_set)=empty_set)),
% 41.09/6.57 inference(forward_demodulation,[status(thm)],[f9553,f20543])).
% 41.09/6.57 fof(f21125,plain,(
% 41.09/6.57 the_carrier(sK304_skl)=empty_set),
% 41.09/6.57 inference(backward_demodulation,[status(thm)],[f20549,f7592])).
% 41.09/6.57 fof(f21472,plain,(
% 41.09/6.57 ~one_sorted_str(sK304_skl)|empty_carrier(sK304_skl)|~empty(empty_set)),
% 41.09/6.57 inference(paramodulation,[status(thm)],[f21125,f849])).
% 41.09/6.57 fof(f21819,plain,(
% 41.09/6.57 empty_carrier(sK304_skl)|~empty(empty_set)),
% 41.09/6.57 inference(forward_subsumption_resolution,[status(thm)],[f21472,f2612])).
% 41.09/6.57 fof(f23165,plain,(
% 41.09/6.57 ~empty(empty_set)),
% 41.09/6.57 inference(forward_subsumption_resolution,[status(thm)],[f21819,f2611])).
% 41.09/6.57 fof(f23166,plain,(
% 41.09/6.57 $false),
% 41.09/6.57 inference(backward_subsumption_resolution,[status(thm)],[f1330,f23165])).
% 41.09/6.57 % SZS output end CNFRefutation for theBenchmark.p
% 41.09/6.60 % Elapsed time: 6.136273 seconds
% 41.09/6.60 % CPU time: 47.353197 seconds
% 41.09/6.60 % Total memory used: 410.782 MB
% 41.09/6.60 % Net memory used: 380.792 MB
%------------------------------------------------------------------------------