%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU321+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:22:19 PM UTC 2026
% Result : Theorem 0.14s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU321+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n001.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 06:17:14 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.46 % Drodi V4.1.1
% 0.14/0.52 % Refutation found
% 0.14/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.52 fof(f145,axiom,(
% 0.14/0.52 (! [A,B] :( element(B,powerset(A))=> element(subset_complement(A,B),powerset(A)) ) )),
% 0.14/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f191,axiom,(
% 0.14/0.52 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 0.14/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f201,axiom,(
% 0.14/0.52 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> ~ empty(the_carrier(A)) ) )),
% 0.14/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f247,axiom,(
% 0.14/0.52 (! [A,B] :( element(B,powerset(A))=> subset_complement(A,subset_complement(A,B)) = B ) )),
% 0.14/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f264,conjecture,(
% 0.14/0.52 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( element(B,powerset(the_carrier(A)))=> (! [C] :( element(C,the_carrier(A))=> ( in(C,subset_complement(the_carrier(A),B))<=> ~ in(C,B) ) ) )) )) )),
% 0.14/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f265,negated_conjecture,(
% 0.14/0.52 ~((! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (! [B] :( element(B,powerset(the_carrier(A)))=> (! [C] :( element(C,the_carrier(A))=> ( in(C,subset_complement(the_carrier(A),B))<=> ~ in(C,B) ) ) )) )) ))),
% 0.14/0.52 inference(negated_conjecture,[status(cth)],[f264])).
% 0.14/0.52 fof(f454,lemma,(
% 0.14/0.52 (! [A,B] :( element(B,powerset(A))=> (! [C] :( element(C,powerset(A))=> ( disjoint(B,C)<=> subset(B,subset_complement(A,C)) ) ) )) )),
% 0.14/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f475,lemma,(
% 0.14/0.52 (! [A] :( A != empty_set=> (! [B] :( element(B,powerset(A))=> (! [C] :( element(C,A)=> ( ~ in(C,B)=> in(C,subset_complement(A,B)) ) ) )) )) )),
% 0.14/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f479,lemma,(
% 0.14/0.52 (! [A,B,C] :( element(C,powerset(A))=> ~ ( in(B,subset_complement(A,C))& in(B,C) ) ) )),
% 0.14/0.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.52 fof(f1220,plain,(
% 0.14/0.52 ![A,B]: (~element(B,powerset(A))|element(subset_complement(A,B),powerset(A)))),
% 0.14/0.52 inference(pre_NNF_transformation,[status(thm)],[f145])).
% 0.14/0.52 fof(f1221,plain,(
% 0.14/0.52 ![X0,X1]: (~element(X0,powerset(X1))|element(subset_complement(X1,X0),powerset(X1)))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f1220])).
% 0.14/0.52 fof(f1303,plain,(
% 0.14/0.52 empty(empty_set)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f191])).
% 0.14/0.52 fof(f1337,plain,(
% 0.14/0.52 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|~empty(the_carrier(A)))),
% 0.14/0.52 inference(pre_NNF_transformation,[status(thm)],[f201])).
% 0.14/0.52 fof(f1338,plain,(
% 0.14/0.52 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|~empty(the_carrier(X0)))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f1337])).
% 0.14/0.52 fof(f1500,plain,(
% 0.14/0.52 ![A,B]: (~element(B,powerset(A))|subset_complement(A,subset_complement(A,B))=B)),
% 0.14/0.52 inference(pre_NNF_transformation,[status(thm)],[f247])).
% 0.14/0.52 fof(f1501,plain,(
% 0.14/0.52 ![X0,X1]: (~element(X0,powerset(X1))|subset_complement(X1,subset_complement(X1,X0))=X0)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f1500])).
% 0.14/0.52 fof(f1557,plain,(
% 0.14/0.52 (?[A]: ((~empty_carrier(A)&one_sorted_str(A))&(?[B]: (element(B,powerset(the_carrier(A)))&(?[C]: (element(C,the_carrier(A))&(in(C,subset_complement(the_carrier(A),B))<~>~in(C,B))))))))),
% 0.14/0.52 inference(pre_NNF_transformation,[status(thm)],[f265])).
% 0.14/0.52 fof(f1558,plain,(
% 0.14/0.52 ?[A]: ((~empty_carrier(A)&one_sorted_str(A))&(?[B]: (element(B,powerset(the_carrier(A)))&(?[C]: (element(C,the_carrier(A))&((in(C,subset_complement(the_carrier(A),B))|~in(C,B))&(~in(C,subset_complement(the_carrier(A),B))|in(C,B))))))))),
% 0.14/0.52 inference(NNF_transformation,[status(thm)],[f1557])).
% 0.14/0.52 fof(f1559,plain,(
% 0.14/0.52 ((~empty_carrier(sK114_skl)&one_sorted_str(sK114_skl))&(element(sK115_skl,powerset(the_carrier(sK114_skl)))&(element(sK116_skl,the_carrier(sK114_skl))&((in(sK116_skl,subset_complement(the_carrier(sK114_skl),sK115_skl))|~in(sK116_skl,sK115_skl))&(~in(sK116_skl,subset_complement(the_carrier(sK114_skl),sK115_skl))|in(sK116_skl,sK115_skl))))))),
% 0.14/0.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK114_skl,sK115_skl,sK116_skl]),skolemize(A,sK114_skl),skolemize(B,sK115_skl),skolemize(C,sK116_skl)],[f1558])).
% 0.14/0.52 fof(f1560,plain,(
% 0.14/0.52 ~empty_carrier(sK114_skl)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f1559])).
% 0.14/0.52 fof(f1561,plain,(
% 0.14/0.52 one_sorted_str(sK114_skl)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f1559])).
% 0.14/0.52 fof(f1562,plain,(
% 0.14/0.52 element(sK115_skl,powerset(the_carrier(sK114_skl)))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f1559])).
% 0.14/0.52 fof(f1563,plain,(
% 0.14/0.52 element(sK116_skl,the_carrier(sK114_skl))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f1559])).
% 0.14/0.52 fof(f1564,plain,(
% 0.14/0.52 in(sK116_skl,subset_complement(the_carrier(sK114_skl),sK115_skl))|~in(sK116_skl,sK115_skl)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f1559])).
% 0.14/0.52 fof(f1565,plain,(
% 0.14/0.52 ~in(sK116_skl,subset_complement(the_carrier(sK114_skl),sK115_skl))|in(sK116_skl,sK115_skl)),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f1559])).
% 0.14/0.52 fof(f2454,plain,(
% 0.14/0.52 ![A,B]: (~element(B,powerset(A))|(![C]: (~element(C,powerset(A))|(disjoint(B,C)<=>subset(B,subset_complement(A,C))))))),
% 0.14/0.52 inference(pre_NNF_transformation,[status(thm)],[f454])).
% 0.14/0.52 fof(f2455,plain,(
% 0.14/0.52 ![A,B]: (~element(B,powerset(A))|(![C]: (~element(C,powerset(A))|((~disjoint(B,C)|subset(B,subset_complement(A,C)))&(disjoint(B,C)|~subset(B,subset_complement(A,C)))))))),
% 0.14/0.52 inference(NNF_transformation,[status(thm)],[f2454])).
% 0.14/0.52 fof(f2457,plain,(
% 0.14/0.52 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|disjoint(X0,X2)|~subset(X0,subset_complement(X1,X2)))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f2455])).
% 0.14/0.52 fof(f2519,plain,(
% 0.14/0.52 ![A]: (A=empty_set|(![B]: (~element(B,powerset(A))|(![C]: (~element(C,A)|(in(C,B)|in(C,subset_complement(A,B))))))))),
% 0.14/0.52 inference(pre_NNF_transformation,[status(thm)],[f475])).
% 0.14/0.52 fof(f2520,plain,(
% 0.14/0.52 ![X0,X1,X2]: (X0=empty_set|~element(X1,powerset(X0))|~element(X2,X0)|in(X2,X1)|in(X2,subset_complement(X0,X1)))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f2519])).
% 0.14/0.52 fof(f2543,plain,(
% 0.14/0.52 ![A,B,C]: (~element(C,powerset(A))|(~in(B,subset_complement(A,C))|~in(B,C)))),
% 0.14/0.52 inference(pre_NNF_transformation,[status(thm)],[f479])).
% 0.14/0.52 fof(f2544,plain,(
% 0.14/0.52 ![A,C]: (~element(C,powerset(A))|(![B]: (~in(B,subset_complement(A,C))|~in(B,C))))),
% 0.14/0.52 inference(miniscoping,[status(thm)],[f2543])).
% 0.14/0.52 fof(f2545,plain,(
% 0.14/0.52 ![X0,X1,X2]: (~element(X0,powerset(X1))|~in(X2,subset_complement(X1,X0))|~in(X2,X0))),
% 0.14/0.52 inference(cnf_transformation,[status(thm)],[f2544])).
% 0.14/0.52 fof(f3061,definition,(
% 0.14/0.52 sQ0_spl <=> (in(sK116_skl,subset_complement(the_carrier(sK114_skl),sK115_skl)))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3062,plain,(
% 0.14/0.52 in(sK116_skl,subset_complement(the_carrier(sK114_skl),sK115_skl))|~sQ0_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f3061])).
% 0.14/0.52 fof(f3064,definition,(
% 0.14/0.52 sQ1_spl <=> (in(sK116_skl,sK115_skl))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3067,plain,(
% 0.14/0.52 sQ0_spl|~sQ1_spl),
% 0.14/0.52 inference(split_clause,[status(thm)],[f1564,f3061,f3064])).
% 0.14/0.52 fof(f3068,plain,(
% 0.14/0.52 ~sQ0_spl|sQ1_spl),
% 0.14/0.52 inference(split_clause,[status(thm)],[f1565,f3061,f3064])).
% 0.14/0.52 fof(f3527,plain,(
% 0.14/0.52 subset_complement(the_carrier(sK114_skl),subset_complement(the_carrier(sK114_skl),sK115_skl))=sK115_skl),
% 0.14/0.52 inference(resolution,[status(thm)],[f1501,f1562])).
% 0.14/0.52 fof(f3530,plain,(
% 0.14/0.52 element(subset_complement(the_carrier(sK114_skl),sK115_skl),powerset(the_carrier(sK114_skl)))),
% 0.14/0.52 inference(resolution,[status(thm)],[f1221,f1562])).
% 0.14/0.52 fof(f3589,plain,(
% 0.14/0.52 ![X0]: (~element(subset_complement(the_carrier(sK114_skl),sK115_skl),powerset(the_carrier(sK114_skl)))|~in(X0,sK115_skl)|~in(X0,subset_complement(the_carrier(sK114_skl),sK115_skl)))),
% 0.14/0.52 inference(paramodulation,[status(thm)],[f3527,f2545])).
% 0.14/0.52 fof(f3590,definition,(
% 0.14/0.52 sQ68_spl <=> (element(subset_complement(the_carrier(sK114_skl),sK115_skl),powerset(the_carrier(sK114_skl))))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3592,plain,(
% 0.14/0.52 ~element(subset_complement(the_carrier(sK114_skl),sK115_skl),powerset(the_carrier(sK114_skl)))|sQ68_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f3590])).
% 0.14/0.52 fof(f3593,definition,(
% 0.14/0.52 ![X0]: (sQ69_spl <=> (~in(X0,sK115_skl)|~in(X0,subset_complement(the_carrier(sK114_skl),sK115_skl))))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3596,plain,(
% 0.14/0.52 ~sQ68_spl|sQ69_spl),
% 0.14/0.52 inference(split_clause,[status(thm)],[f3589,f3590,f3593])).
% 0.14/0.52 fof(f3597,plain,(
% 0.14/0.52 $false|sQ68_spl),
% 0.14/0.52 inference(forward_subsumption_resolution,[status(thm)],[f3592,f3530])).
% 0.14/0.52 fof(f3598,plain,(
% 0.14/0.52 sQ68_spl),
% 0.14/0.52 inference(contradiction_clause,[status(thm)],[f3597])).
% 0.14/0.52 fof(f3600,plain,(
% 0.14/0.52 ![X0]: (~element(X0,powerset(the_carrier(sK114_skl)))|~element(subset_complement(the_carrier(sK114_skl),sK115_skl),powerset(the_carrier(sK114_skl)))|disjoint(X0,subset_complement(the_carrier(sK114_skl),sK115_skl))|~subset(X0,sK115_skl))),
% 0.14/0.52 inference(paramodulation,[status(thm)],[f3527,f2457])).
% 0.14/0.52 fof(f3602,definition,(
% 0.14/0.52 ![X0]: (sQ70_spl <=> (~element(X0,powerset(the_carrier(sK114_skl)))|disjoint(X0,subset_complement(the_carrier(sK114_skl),sK115_skl))|~subset(X0,sK115_skl)))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3605,plain,(
% 0.14/0.52 sQ70_spl|~sQ68_spl),
% 0.14/0.52 inference(split_clause,[status(thm)],[f3600,f3602,f3590])).
% 0.14/0.52 fof(f3606,plain,(
% 0.14/0.52 ![X0]: (the_carrier(sK114_skl)=empty_set|~element(X0,the_carrier(sK114_skl))|in(X0,subset_complement(the_carrier(sK114_skl),sK115_skl))|in(X0,subset_complement(the_carrier(sK114_skl),subset_complement(the_carrier(sK114_skl),sK115_skl))))),
% 0.14/0.52 inference(resolution,[status(thm)],[f2520,f3530])).
% 0.14/0.52 fof(f3607,plain,(
% 0.14/0.52 ![X0]: (the_carrier(sK114_skl)=empty_set|~element(X0,the_carrier(sK114_skl))|in(X0,sK115_skl)|in(X0,subset_complement(the_carrier(sK114_skl),sK115_skl)))),
% 0.14/0.52 inference(resolution,[status(thm)],[f2520,f1562])).
% 0.14/0.52 fof(f3608,definition,(
% 0.14/0.52 sQ71_spl <=> (the_carrier(sK114_skl)=empty_set)),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3609,plain,(
% 0.14/0.52 the_carrier(sK114_skl)=empty_set|~sQ71_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f3608])).
% 0.14/0.52 fof(f3611,definition,(
% 0.14/0.52 ![X0]: (sQ72_spl <=> (~element(X0,the_carrier(sK114_skl))|in(X0,subset_complement(the_carrier(sK114_skl),sK115_skl))|in(X0,subset_complement(the_carrier(sK114_skl),subset_complement(the_carrier(sK114_skl),sK115_skl)))))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3614,plain,(
% 0.14/0.52 sQ71_spl|sQ72_spl),
% 0.14/0.52 inference(split_clause,[status(thm)],[f3606,f3608,f3611])).
% 0.14/0.52 fof(f3615,definition,(
% 0.14/0.52 ![X0]: (sQ73_spl <=> (~element(X0,the_carrier(sK114_skl))|in(X0,sK115_skl)|in(X0,subset_complement(the_carrier(sK114_skl),sK115_skl))))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3616,plain,(
% 0.14/0.52 ![X0]: (~element(X0,the_carrier(sK114_skl))|in(X0,sK115_skl)|in(X0,subset_complement(the_carrier(sK114_skl),sK115_skl))|~sQ73_spl)),
% 0.14/0.52 inference(component_clause,[status(thm)],[f3615])).
% 0.14/0.52 fof(f3618,plain,(
% 0.14/0.52 sQ71_spl|sQ73_spl),
% 0.14/0.52 inference(split_clause,[status(thm)],[f3607,f3608,f3615])).
% 0.14/0.52 fof(f3663,plain,(
% 0.14/0.52 empty_carrier(sK114_skl)|~one_sorted_str(sK114_skl)|~empty(empty_set)|~sQ71_spl),
% 0.14/0.52 inference(paramodulation,[status(thm)],[f3609,f1338])).
% 0.14/0.52 fof(f3668,definition,(
% 0.14/0.52 sQ79_spl <=> (empty_carrier(sK114_skl))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3669,plain,(
% 0.14/0.52 empty_carrier(sK114_skl)|~sQ79_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f3668])).
% 0.14/0.52 fof(f3671,definition,(
% 0.14/0.52 sQ80_spl <=> (one_sorted_str(sK114_skl))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3673,plain,(
% 0.14/0.52 ~one_sorted_str(sK114_skl)|sQ80_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f3671])).
% 0.14/0.52 fof(f3674,definition,(
% 0.14/0.52 sQ81_spl <=> (empty(empty_set))),
% 0.14/0.52 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.14/0.52 fof(f3676,plain,(
% 0.14/0.52 ~empty(empty_set)|sQ81_spl),
% 0.14/0.52 inference(component_clause,[status(thm)],[f3674])).
% 0.14/0.52 fof(f3677,plain,(
% 0.14/0.52 sQ79_spl|~sQ80_spl|~sQ81_spl|~sQ71_spl),
% 0.14/0.52 inference(split_clause,[status(thm)],[f3663,f3668,f3671,f3674,f3608])).
% 0.14/0.53 fof(f3680,plain,(
% 0.14/0.53 $false|sQ81_spl),
% 0.14/0.53 inference(forward_subsumption_resolution,[status(thm)],[f3676,f1303])).
% 0.14/0.53 fof(f3681,plain,(
% 0.14/0.53 sQ81_spl),
% 0.14/0.53 inference(contradiction_clause,[status(thm)],[f3680])).
% 0.14/0.53 fof(f3682,plain,(
% 0.14/0.53 $false|~sQ79_spl),
% 0.14/0.53 inference(forward_subsumption_resolution,[status(thm)],[f3669,f1560])).
% 0.14/0.53 fof(f3683,plain,(
% 0.14/0.53 ~sQ79_spl),
% 0.14/0.53 inference(contradiction_clause,[status(thm)],[f3682])).
% 0.14/0.53 fof(f3684,plain,(
% 0.14/0.53 $false|sQ80_spl),
% 0.14/0.53 inference(forward_subsumption_resolution,[status(thm)],[f3673,f1561])).
% 0.14/0.53 fof(f3685,plain,(
% 0.14/0.53 sQ80_spl),
% 0.14/0.53 inference(contradiction_clause,[status(thm)],[f3684])).
% 0.14/0.53 fof(f3723,plain,(
% 0.14/0.53 in(sK116_skl,sK115_skl)|in(sK116_skl,subset_complement(the_carrier(sK114_skl),sK115_skl))|~sQ73_spl),
% 0.14/0.53 inference(resolution,[status(thm)],[f3616,f1563])).
% 0.14/0.53 fof(f3724,plain,(
% 0.14/0.53 sQ1_spl|sQ0_spl|~sQ73_spl),
% 0.14/0.53 inference(split_clause,[status(thm)],[f3723,f3064,f3061,f3615])).
% 0.14/0.53 fof(f3755,plain,(
% 0.14/0.53 ~element(sK115_skl,powerset(the_carrier(sK114_skl)))|~in(sK116_skl,sK115_skl)|~sQ0_spl),
% 0.14/0.53 inference(resolution,[status(thm)],[f3062,f2545])).
% 0.14/0.53 fof(f3760,definition,(
% 0.14/0.53 sQ88_spl <=> (element(sK115_skl,powerset(the_carrier(sK114_skl))))),
% 0.14/0.53 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.14/0.53 fof(f3762,plain,(
% 0.14/0.53 ~element(sK115_skl,powerset(the_carrier(sK114_skl)))|sQ88_spl),
% 0.14/0.53 inference(component_clause,[status(thm)],[f3760])).
% 0.14/0.53 fof(f3763,plain,(
% 0.14/0.53 ~sQ88_spl|~sQ1_spl|~sQ0_spl),
% 0.14/0.53 inference(split_clause,[status(thm)],[f3755,f3760,f3064,f3061])).
% 0.14/0.53 fof(f3764,plain,(
% 0.14/0.53 $false|sQ88_spl),
% 0.14/0.53 inference(forward_subsumption_resolution,[status(thm)],[f3762,f1562])).
% 0.14/0.53 fof(f3765,plain,(
% 0.14/0.53 sQ88_spl),
% 0.14/0.53 inference(contradiction_clause,[status(thm)],[f3764])).
% 0.14/0.53 fof(f3766,plain,(
% 0.14/0.53 $false),
% 0.14/0.53 inference(sat_refutation,[status(thm)],[f3067,f3068,f3596,f3598,f3605,f3614,f3618,f3677,f3681,f3683,f3685,f3724,f3763,f3765])).
% 0.14/0.53 % SZS output end CNFRefutation for theBenchmark.p
% 0.27/0.59 % Elapsed time: 0.206508 seconds
% 0.27/0.59 % CPU time: 0.633483 seconds
% 0.27/0.59 % Total memory used: 176.416 MB
% 0.27/0.59 % Net memory used: 175.508 MB
%------------------------------------------------------------------------------