%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU106+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:21:41 PM UTC 2026
% Result : Theorem 32.06s 4.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU106+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n007.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 05:48:50 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 32.06/4.53 % Refutation found
% 32.06/4.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 32.06/4.53 % SZS output start CNFRefutation for theBenchmark
% 32.06/4.53 fof(f1,axiom,(
% 32.06/4.53 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f6,axiom,(
% 32.06/4.53 (! [A,B] : set_union2(A,B) = set_union2(B,A) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f7,axiom,(
% 32.06/4.53 (! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f8,axiom,(
% 32.06/4.53 (! [A,B] : symmetric_difference(A,B) = symmetric_difference(B,A) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f10,axiom,(
% 32.06/4.53 (! [A] :(? [B] : element(B,A) ))),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f15,axiom,(
% 32.06/4.53 (! [A] : ~ empty(powerset(A)) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f16,axiom,(
% 32.06/4.53 empty(empty_set) ),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f20,axiom,(
% 32.06/4.53 (! [A,B] : set_union2(A,A) = A )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f23,axiom,(
% 32.06/4.53 (? [A] :( ~ empty(A)& cup_closed(A)& cap_closed(A)& diff_closed(A)& preboolean(A) ) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f32,axiom,(
% 32.06/4.53 (! [A,B] : set_difference(A,B) = symmetric_difference(A,set_intersection2(A,B)) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f33,axiom,(
% 32.06/4.53 (! [A] :( preboolean(A)<=> (! [B,C] :( ( in(B,A)& in(C,A) )=> ( in(set_union2(B,C),A)& in(set_difference(B,C),A) ) ) )) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f34,conjecture,(
% 32.06/4.53 (! [A] :( ~ empty(A)=> ( (! [B] :( element(B,A)=> (! [C] :( element(C,A)=> ( in(symmetric_difference(B,C),A)& in(set_union2(B,C),A) ) ) )))=> preboolean(A) ) ) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f35,negated_conjecture,(
% 32.06/4.53 ~((! [A] :( ~ empty(A)=> ( (! [B] :( element(B,A)=> (! [C] :( element(C,A)=> ( in(symmetric_difference(B,C),A)& in(set_union2(B,C),A) ) ) )))=> preboolean(A) ) ) ))),
% 32.06/4.53 inference(negated_conjecture,[status(cth)],[f34])).
% 32.06/4.53 fof(f36,axiom,(
% 32.06/4.53 (! [A] : set_union2(A,empty_set) = A )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f37,axiom,(
% 32.06/4.53 (! [A,B] :( in(A,B)=> element(A,B) ) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f38,axiom,(
% 32.06/4.53 (! [A] : set_intersection2(A,empty_set) = empty_set )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f39,axiom,(
% 32.06/4.53 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f44,axiom,(
% 32.06/4.53 (! [A] : symmetric_difference(A,empty_set) = A )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f49,axiom,(
% 32.06/4.53 (! [A,B] : set_intersection2(A,B) = symmetric_difference(symmetric_difference(A,B),set_union2(A,B)) )),
% 32.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.06/4.53 fof(f50,plain,(
% 32.06/4.53 ![A,B]: (~in(A,B)|~in(B,A))),
% 32.06/4.53 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 32.06/4.53 fof(f51,plain,(
% 32.06/4.53 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f50])).
% 32.06/4.53 fof(f61,plain,(
% 32.06/4.53 ![X0,X1]: (set_union2(X0,X1)=set_union2(X1,X0))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f6])).
% 32.06/4.53 fof(f62,plain,(
% 32.06/4.53 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,X0))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f7])).
% 32.06/4.53 fof(f63,plain,(
% 32.06/4.53 ![X0,X1]: (symmetric_difference(X0,X1)=symmetric_difference(X1,X0))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f8])).
% 32.06/4.53 fof(f65,plain,(
% 32.06/4.53 ![A]: element(sK0_skl(A),A)),
% 32.06/4.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f10])).
% 32.06/4.53 fof(f66,plain,(
% 32.06/4.53 ![X0]: (element(sK0_skl(X0),X0))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f65])).
% 32.06/4.53 fof(f78,plain,(
% 32.06/4.53 ![X0]: (~empty(powerset(X0)))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f15])).
% 32.06/4.53 fof(f79,plain,(
% 32.06/4.53 empty(empty_set)),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f16])).
% 32.06/4.53 fof(f88,plain,(
% 32.06/4.53 ![A]: set_union2(A,A)=A),
% 32.06/4.53 inference(miniscoping,[status(thm)],[f20])).
% 32.06/4.53 fof(f89,plain,(
% 32.06/4.53 ![X0]: (set_union2(X0,X0)=X0)),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f88])).
% 32.06/4.53 fof(f95,plain,(
% 32.06/4.53 ((((~empty(sK2_skl)&cup_closed(sK2_skl))&cap_closed(sK2_skl))&diff_closed(sK2_skl))&preboolean(sK2_skl))),
% 32.06/4.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f23])).
% 32.06/4.53 fof(f96,plain,(
% 32.06/4.53 ~empty(sK2_skl)),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f95])).
% 32.06/4.53 fof(f135,plain,(
% 32.06/4.53 ![X0,X1]: (set_difference(X0,X1)=symmetric_difference(X0,set_intersection2(X0,X1)))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f32])).
% 32.06/4.53 fof(f136,plain,(
% 32.06/4.53 ![A]: (preboolean(A)<=>(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A)))))),
% 32.06/4.53 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 32.06/4.53 fof(f137,plain,(
% 32.06/4.53 ![A]: ((~preboolean(A)|(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A)))))&(preboolean(A)|(?[B,C]: ((in(B,A)&in(C,A))&(~in(set_union2(B,C),A)|~in(set_difference(B,C),A))))))),
% 32.06/4.53 inference(NNF_transformation,[status(thm)],[f136])).
% 32.06/4.53 fof(f138,plain,(
% 32.06/4.53 (![A]: (~preboolean(A)|(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A))))))&(![A]: (preboolean(A)|(?[B,C]: ((in(B,A)&in(C,A))&(~in(set_union2(B,C),A)|~in(set_difference(B,C),A))))))),
% 32.06/4.53 inference(miniscoping,[status(thm)],[f137])).
% 32.06/4.53 fof(f139,plain,(
% 32.06/4.53 (![A]: (~preboolean(A)|(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A))))))&(![A]: (preboolean(A)|((in(sK10_skl(A),A)&in(sK11_skl(A),A))&(~in(set_union2(sK10_skl(A),sK11_skl(A)),A)|~in(set_difference(sK10_skl(A),sK11_skl(A)),A)))))),
% 32.06/4.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl]),skolemize(B,sK10_skl(A)),skolemize(C,sK11_skl(A))],[f138])).
% 32.06/4.53 fof(f142,plain,(
% 32.06/4.53 ![X0]: (preboolean(X0)|in(sK10_skl(X0),X0))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f139])).
% 32.06/4.53 fof(f143,plain,(
% 32.06/4.53 ![X0]: (preboolean(X0)|in(sK11_skl(X0),X0))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f139])).
% 32.06/4.53 fof(f144,plain,(
% 32.06/4.53 ![X0]: (preboolean(X0)|~in(set_union2(sK10_skl(X0),sK11_skl(X0)),X0)|~in(set_difference(sK10_skl(X0),sK11_skl(X0)),X0))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f139])).
% 32.06/4.53 fof(f145,plain,(
% 32.06/4.53 (?[A]: (~empty(A)&((![B]: (~element(B,A)|(![C]: (~element(C,A)|(in(symmetric_difference(B,C),A)&in(set_union2(B,C),A))))))&~preboolean(A))))),
% 32.06/4.53 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 32.06/4.53 fof(f146,plain,(
% 32.06/4.53 (~empty(sK12_skl)&((![B]: (~element(B,sK12_skl)|(![C]: (~element(C,sK12_skl)|(in(symmetric_difference(B,C),sK12_skl)&in(set_union2(B,C),sK12_skl))))))&~preboolean(sK12_skl)))),
% 32.06/4.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f145])).
% 32.06/4.53 fof(f147,plain,(
% 32.06/4.53 ~empty(sK12_skl)),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f146])).
% 32.06/4.53 fof(f148,plain,(
% 32.06/4.53 ![X0,X1]: (~element(X0,sK12_skl)|~element(X1,sK12_skl)|in(symmetric_difference(X0,X1),sK12_skl))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f146])).
% 32.06/4.53 fof(f149,plain,(
% 32.06/4.53 ![X0,X1]: (~element(X0,sK12_skl)|~element(X1,sK12_skl)|in(set_union2(X0,X1),sK12_skl))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f146])).
% 32.06/4.53 fof(f150,plain,(
% 32.06/4.53 ~preboolean(sK12_skl)),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f146])).
% 32.06/4.53 fof(f151,plain,(
% 32.06/4.53 ![X0]: (set_union2(X0,empty_set)=X0)),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f36])).
% 32.06/4.53 fof(f152,plain,(
% 32.06/4.53 ![A,B]: (~in(A,B)|element(A,B))),
% 32.06/4.53 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 32.06/4.53 fof(f153,plain,(
% 32.06/4.53 ![X0,X1]: (~in(X0,X1)|element(X0,X1))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f152])).
% 32.06/4.53 fof(f154,plain,(
% 32.06/4.53 ![X0]: (set_intersection2(X0,empty_set)=empty_set)),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f38])).
% 32.06/4.53 fof(f155,plain,(
% 32.06/4.53 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 32.06/4.53 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 32.06/4.53 fof(f156,plain,(
% 32.06/4.53 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f155])).
% 32.06/4.53 fof(f166,plain,(
% 32.06/4.53 ![X0]: (symmetric_difference(X0,empty_set)=X0)),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f44])).
% 32.06/4.53 fof(f178,plain,(
% 32.06/4.53 ![X0,X1]: (set_intersection2(X0,X1)=symmetric_difference(symmetric_difference(X0,X1),set_union2(X0,X1)))),
% 32.06/4.53 inference(cnf_transformation,[status(thm)],[f49])).
% 32.06/4.53 fof(f179,plain,(
% 32.06/4.53 ![X0]: (~element(X0,sK12_skl)|~element(X0,sK12_skl)|in(X0,sK12_skl))),
% 32.06/4.53 inference(paramodulation,[status(thm)],[f89,f149])).
% 32.06/4.53 fof(f180,plain,(
% 32.06/4.53 ![X0]: (~element(X0,sK12_skl)|in(X0,sK12_skl))),
% 32.06/4.53 inference(duplicate_literals_removal,[status(thm)],[f179])).
% 32.06/4.53 fof(f185,definition,(
% 32.06/4.53 sQ1_spl <=> (element(empty_set,sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f187,plain,(
% 32.06/4.53 ~element(empty_set,sK12_skl)|sQ1_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f185])).
% 32.06/4.53 fof(f197,plain,(
% 32.06/4.53 ![X0]: (X0=symmetric_difference(empty_set,X0))),
% 32.06/4.53 inference(paramodulation,[status(thm)],[f166,f63])).
% 32.06/4.53 fof(f249,plain,(
% 32.06/4.53 ![X0,X1]: (element(set_union2(X0,X1),sK12_skl)|~element(X0,sK12_skl)|~element(X1,sK12_skl))),
% 32.06/4.53 inference(resolution,[status(thm)],[f153,f149])).
% 32.06/4.53 fof(f250,plain,(
% 32.06/4.53 ![X0,X1]: (element(symmetric_difference(X0,X1),sK12_skl)|~element(X0,sK12_skl)|~element(X1,sK12_skl))),
% 32.06/4.53 inference(resolution,[status(thm)],[f153,f148])).
% 32.06/4.53 fof(f290,plain,(
% 32.06/4.53 ![X0]: (element(set_union2(X0,sK0_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl))),
% 32.06/4.53 inference(resolution,[status(thm)],[f66,f249])).
% 32.06/4.53 fof(f308,plain,(
% 32.06/4.53 ![X0]: (set_union2(empty_set,X0)=X0)),
% 32.06/4.53 inference(paramodulation,[status(thm)],[f61,f151])).
% 32.06/4.53 fof(f320,definition,(
% 32.06/4.53 ![X0]: (sQ5_spl <=> (~empty(X0)))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f321,plain,(
% 32.06/4.53 ![X0]: (~empty(X0)|~sQ5_spl)),
% 32.06/4.53 inference(component_clause,[status(thm)],[f320])).
% 32.06/4.53 fof(f344,plain,(
% 32.06/4.53 ![X0]: (set_intersection2(empty_set,X0)=empty_set)),
% 32.06/4.53 inference(paramodulation,[status(thm)],[f62,f154])).
% 32.06/4.53 fof(f378,definition,(
% 32.06/4.53 sQ7_spl <=> (empty(sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f379,plain,(
% 32.06/4.53 empty(sK12_skl)|~sQ7_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f378])).
% 32.06/4.53 fof(f385,plain,(
% 32.06/4.53 $false|~sQ7_spl),
% 32.06/4.53 inference(forward_subsumption_resolution,[status(thm)],[f379,f147])).
% 32.06/4.53 fof(f386,plain,(
% 32.06/4.53 ~sQ7_spl),
% 32.06/4.53 inference(contradiction_clause,[status(thm)],[f385])).
% 32.06/4.53 fof(f565,definition,(
% 32.06/4.53 sQ16_spl <=> (empty(sK2_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f566,plain,(
% 32.06/4.53 empty(sK2_skl)|~sQ16_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f565])).
% 32.06/4.53 fof(f598,plain,(
% 32.06/4.53 ![X0]: (preboolean(X0)|element(sK10_skl(X0),X0))),
% 32.06/4.53 inference(resolution,[status(thm)],[f142,f153])).
% 32.06/4.53 fof(f626,plain,(
% 32.06/4.53 ![X0,X1]: (~element(X0,sK12_skl)|~element(set_intersection2(X0,X1),sK12_skl)|in(set_difference(X0,X1),sK12_skl))),
% 32.06/4.53 inference(paramodulation,[status(thm)],[f135,f148])).
% 32.06/4.53 fof(f654,plain,(
% 32.06/4.53 ![X0]: (preboolean(sK12_skl)|~element(set_intersection2(sK10_skl(sK12_skl),X0),sK12_skl)|in(set_difference(sK10_skl(sK12_skl),X0),sK12_skl))),
% 32.06/4.53 inference(resolution,[status(thm)],[f598,f626])).
% 32.06/4.53 fof(f658,plain,(
% 32.06/4.53 preboolean(sK12_skl)|element(set_union2(sK10_skl(sK12_skl),sK0_skl(sK12_skl)),sK12_skl)),
% 32.06/4.53 inference(resolution,[status(thm)],[f598,f290])).
% 32.06/4.53 fof(f660,plain,(
% 32.06/4.53 ![X0]: (preboolean(sK12_skl)|element(symmetric_difference(X0,sK10_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl))),
% 32.06/4.53 inference(resolution,[status(thm)],[f598,f250])).
% 32.06/4.53 fof(f666,definition,(
% 32.06/4.53 sQ21_spl <=> (preboolean(sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f667,plain,(
% 32.06/4.53 preboolean(sK12_skl)|~sQ21_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f666])).
% 32.06/4.53 fof(f669,definition,(
% 32.06/4.53 ![X0]: (sQ22_spl <=> (~element(set_intersection2(sK10_skl(sK12_skl),X0),sK12_skl)|in(set_difference(sK10_skl(sK12_skl),X0),sK12_skl)))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f670,plain,(
% 32.06/4.53 ![X0]: (~element(set_intersection2(sK10_skl(sK12_skl),X0),sK12_skl)|in(set_difference(sK10_skl(sK12_skl),X0),sK12_skl)|~sQ22_spl)),
% 32.06/4.53 inference(component_clause,[status(thm)],[f669])).
% 32.06/4.53 fof(f672,plain,(
% 32.06/4.53 sQ21_spl|sQ22_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f654,f666,f669])).
% 32.06/4.53 fof(f685,definition,(
% 32.06/4.53 sQ26_spl <=> (element(set_union2(sK10_skl(sK12_skl),sK0_skl(sK12_skl)),sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f686,plain,(
% 32.06/4.53 element(set_union2(sK10_skl(sK12_skl),sK0_skl(sK12_skl)),sK12_skl)|~sQ26_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f685])).
% 32.06/4.53 fof(f688,plain,(
% 32.06/4.53 sQ21_spl|sQ26_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f658,f666,f685])).
% 32.06/4.53 fof(f693,definition,(
% 32.06/4.53 ![X0]: (sQ28_spl <=> (element(symmetric_difference(X0,sK10_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f694,plain,(
% 32.06/4.53 ![X0]: (element(symmetric_difference(X0,sK10_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)|~sQ28_spl)),
% 32.06/4.53 inference(component_clause,[status(thm)],[f693])).
% 32.06/4.53 fof(f696,plain,(
% 32.06/4.53 sQ21_spl|sQ28_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f660,f666,f693])).
% 32.06/4.53 fof(f709,definition,(
% 32.06/4.53 sQ32_spl <=> (in(sK10_skl(sK12_skl),sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f710,plain,(
% 32.06/4.53 in(sK10_skl(sK12_skl),sK12_skl)|~sQ32_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f709])).
% 32.06/4.53 fof(f713,plain,(
% 32.06/4.53 $false|~sQ21_spl),
% 32.06/4.53 inference(forward_subsumption_resolution,[status(thm)],[f667,f150])).
% 32.06/4.53 fof(f714,plain,(
% 32.06/4.53 ~sQ21_spl),
% 32.06/4.53 inference(contradiction_clause,[status(thm)],[f713])).
% 32.06/4.53 fof(f715,plain,(
% 32.06/4.53 element(sK10_skl(sK12_skl),sK12_skl)|~sQ32_spl),
% 32.06/4.53 inference(resolution,[status(thm)],[f710,f153])).
% 32.06/4.53 fof(f739,plain,(
% 32.06/4.53 ![X0]: (preboolean(X0)|element(sK11_skl(X0),X0))),
% 32.06/4.53 inference(resolution,[status(thm)],[f143,f153])).
% 32.06/4.53 fof(f774,plain,(
% 32.06/4.53 ![X0]: (preboolean(sK12_skl)|element(symmetric_difference(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl))),
% 32.06/4.53 inference(resolution,[status(thm)],[f739,f250])).
% 32.06/4.53 fof(f775,plain,(
% 32.06/4.53 ![X0]: (preboolean(sK12_skl)|element(set_union2(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl))),
% 32.06/4.53 inference(resolution,[status(thm)],[f739,f249])).
% 32.06/4.53 fof(f804,definition,(
% 32.06/4.53 ![X0]: (sQ40_spl <=> (element(symmetric_difference(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f805,plain,(
% 32.06/4.53 ![X0]: (element(symmetric_difference(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)|~sQ40_spl)),
% 32.06/4.53 inference(component_clause,[status(thm)],[f804])).
% 32.06/4.53 fof(f807,plain,(
% 32.06/4.53 sQ21_spl|sQ40_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f774,f666,f804])).
% 32.06/4.53 fof(f808,definition,(
% 32.06/4.53 ![X0]: (sQ41_spl <=> (element(set_union2(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f809,plain,(
% 32.06/4.53 ![X0]: (element(set_union2(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)|~sQ41_spl)),
% 32.06/4.53 inference(component_clause,[status(thm)],[f808])).
% 32.06/4.53 fof(f811,plain,(
% 32.06/4.53 sQ21_spl|sQ41_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f775,f666,f808])).
% 32.06/4.53 fof(f919,plain,(
% 32.06/4.53 ![X0,X1]: (~element(symmetric_difference(X0,X1),sK12_skl)|~element(set_union2(X0,X1),sK12_skl)|in(set_intersection2(X0,X1),sK12_skl))),
% 32.06/4.53 inference(paramodulation,[status(thm)],[f178,f148])).
% 32.06/4.53 fof(f968,plain,(
% 32.06/4.53 ![X0,X1]: (~element(symmetric_difference(X0,X1),sK12_skl)|~element(set_union2(X0,X1),sK12_skl)|element(set_intersection2(X0,X1),sK12_skl))),
% 32.06/4.53 inference(resolution,[status(thm)],[f919,f153])).
% 32.06/4.53 fof(f970,plain,(
% 32.06/4.53 ![X0]: (~element(symmetric_difference(empty_set,X0),sK12_skl)|~element(set_union2(empty_set,X0),sK12_skl)|in(empty_set,sK12_skl))),
% 32.06/4.53 inference(paramodulation,[status(thm)],[f344,f919])).
% 32.06/4.53 fof(f975,definition,(
% 32.06/4.53 ![X0]: (sQ49_spl <=> (~element(symmetric_difference(empty_set,X0),sK12_skl)|~element(set_union2(empty_set,X0),sK12_skl)))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f976,plain,(
% 32.06/4.53 ![X0]: (~element(symmetric_difference(empty_set,X0),sK12_skl)|~element(set_union2(empty_set,X0),sK12_skl)|~sQ49_spl)),
% 32.06/4.53 inference(component_clause,[status(thm)],[f975])).
% 32.06/4.53 fof(f978,definition,(
% 32.06/4.53 sQ50_spl <=> (in(empty_set,sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f979,plain,(
% 32.06/4.53 in(empty_set,sK12_skl)|~sQ50_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f978])).
% 32.06/4.53 fof(f981,plain,(
% 32.06/4.53 sQ49_spl|sQ50_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f970,f975,f978])).
% 32.06/4.53 fof(f1024,plain,(
% 32.06/4.53 $false|~sQ5_spl),
% 32.06/4.53 inference(backward_subsumption_resolution,[status(thm)],[f79,f321])).
% 32.06/4.53 fof(f1025,plain,(
% 32.06/4.53 ~sQ5_spl),
% 32.06/4.53 inference(contradiction_clause,[status(thm)],[f1024])).
% 32.06/4.53 fof(f1035,plain,(
% 32.06/4.53 element(empty_set,sK12_skl)|~sQ50_spl),
% 32.06/4.53 inference(resolution,[status(thm)],[f979,f153])).
% 32.06/4.53 fof(f1037,plain,(
% 32.06/4.53 $false|sQ1_spl|~sQ50_spl),
% 32.06/4.53 inference(forward_subsumption_resolution,[status(thm)],[f1035,f187])).
% 32.06/4.53 fof(f1038,plain,(
% 32.06/4.53 sQ1_spl|~sQ50_spl),
% 32.06/4.53 inference(contradiction_clause,[status(thm)],[f1037])).
% 32.06/4.53 fof(f1039,plain,(
% 32.06/4.53 ![X0]: (~element(X0,sK12_skl)|~element(set_union2(empty_set,X0),sK12_skl)|~sQ49_spl)),
% 32.06/4.53 inference(forward_demodulation,[status(thm)],[f197,f976])).
% 32.06/4.53 fof(f1040,plain,(
% 32.06/4.53 ![X0]: (~element(X0,sK12_skl)|~element(X0,sK12_skl)|~sQ49_spl)),
% 32.06/4.53 inference(forward_demodulation,[status(thm)],[f308,f1039])).
% 32.06/4.53 fof(f1041,plain,(
% 32.06/4.53 ![X0]: (~element(X0,sK12_skl)|~sQ49_spl)),
% 32.06/4.53 inference(duplicate_literals_removal,[status(thm)],[f1040])).
% 32.06/4.53 fof(f1048,plain,(
% 32.06/4.53 $false|~sQ49_spl|~sQ26_spl),
% 32.06/4.53 inference(backward_subsumption_resolution,[status(thm)],[f686,f1041])).
% 32.06/4.53 fof(f1057,plain,(
% 32.06/4.53 ~sQ49_spl|~sQ26_spl),
% 32.06/4.53 inference(contradiction_clause,[status(thm)],[f1048])).
% 32.06/4.53 fof(f1096,definition,(
% 32.06/4.53 ![X0]: (sQ54_spl <=> (~element(X0,sK12_skl)|in(set_union2(X0,sK11_skl(sK12_skl)),sK12_skl)))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f1097,plain,(
% 32.06/4.53 ![X0]: (~element(X0,sK12_skl)|in(set_union2(X0,sK11_skl(sK12_skl)),sK12_skl)|~sQ54_spl)),
% 32.06/4.53 inference(component_clause,[status(thm)],[f1096])).
% 32.06/4.53 fof(f1132,plain,(
% 32.06/4.53 ~element(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|preboolean(sK12_skl)|~in(set_union2(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)),
% 32.06/4.53 inference(resolution,[status(thm)],[f180,f144])).
% 32.06/4.53 fof(f1134,plain,(
% 32.06/4.53 ![X0]: (~element(X0,sK12_skl)|~in(sK12_skl,X0))),
% 32.06/4.53 inference(resolution,[status(thm)],[f180,f51])).
% 32.06/4.53 fof(f1135,definition,(
% 32.06/4.53 sQ56_spl <=> (element(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f1137,plain,(
% 32.06/4.53 ~element(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|sQ56_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f1135])).
% 32.06/4.53 fof(f1138,definition,(
% 32.06/4.53 sQ57_spl <=> (in(set_union2(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f1140,plain,(
% 32.06/4.53 ~in(set_union2(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|sQ57_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f1138])).
% 32.06/4.53 fof(f1141,plain,(
% 32.06/4.53 ~sQ56_spl|sQ21_spl|~sQ57_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f1132,f1135,f666,f1138])).
% 32.06/4.53 fof(f1152,definition,(
% 32.06/4.53 ![X0]: (sQ59_spl <=> (~element(X0,sK12_skl)|in(symmetric_difference(X0,sK10_skl(sK12_skl)),sK12_skl)))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f1153,plain,(
% 32.06/4.53 ![X0]: (~element(X0,sK12_skl)|in(symmetric_difference(X0,sK10_skl(sK12_skl)),sK12_skl)|~sQ59_spl)),
% 32.06/4.53 inference(component_clause,[status(thm)],[f1152])).
% 32.06/4.53 fof(f1162,plain,(
% 32.06/4.53 ~element(sK12_skl,sK12_skl)|~element(sK12_skl,sK12_skl)),
% 32.06/4.53 inference(resolution,[status(thm)],[f1134,f180])).
% 32.06/4.53 fof(f1164,definition,(
% 32.06/4.53 sQ60_spl <=> (element(sK12_skl,sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f1167,plain,(
% 32.06/4.53 ~sQ60_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f1162,f1164])).
% 32.06/4.53 fof(f1522,plain,(
% 32.06/4.53 $false|~sQ16_spl),
% 32.06/4.53 inference(forward_subsumption_resolution,[status(thm)],[f566,f96])).
% 32.06/4.53 fof(f1523,plain,(
% 32.06/4.53 ~sQ16_spl),
% 32.06/4.53 inference(contradiction_clause,[status(thm)],[f1522])).
% 32.06/4.53 fof(f1728,definition,(
% 32.06/4.53 sQ90_spl <=> (empty(powerset(empty_set)))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f1729,plain,(
% 32.06/4.53 empty(powerset(empty_set))|~sQ90_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f1728])).
% 32.06/4.53 fof(f1739,plain,(
% 32.06/4.53 $false|~sQ90_spl),
% 32.06/4.53 inference(forward_subsumption_resolution,[status(thm)],[f1729,f78])).
% 32.06/4.53 fof(f1740,plain,(
% 32.06/4.53 ~sQ90_spl),
% 32.06/4.53 inference(contradiction_clause,[status(thm)],[f1739])).
% 32.06/4.53 fof(f2823,definition,(
% 32.06/4.53 sQ147_spl <=> (element(sK10_skl(sK12_skl),sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f3019,plain,(
% 32.06/4.53 ![X0]: (~element(X0,sK12_skl)|empty(sK12_skl)|in(symmetric_difference(X0,sK10_skl(sK12_skl)),sK12_skl)|~sQ28_spl)),
% 32.06/4.53 inference(resolution,[status(thm)],[f694,f156])).
% 32.06/4.53 fof(f3020,plain,(
% 32.06/4.53 element(sK10_skl(sK12_skl),sK12_skl)|~element(empty_set,sK12_skl)|~sQ28_spl),
% 32.06/4.53 inference(paramodulation,[status(thm)],[f197,f694])).
% 32.06/4.53 fof(f3024,plain,(
% 32.06/4.53 sQ59_spl|sQ7_spl|~sQ28_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f3019,f1152,f378,f693])).
% 32.06/4.53 fof(f3025,plain,(
% 32.06/4.53 sQ147_spl|~sQ1_spl|~sQ28_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f3020,f2823,f185,f693])).
% 32.06/4.53 fof(f3275,plain,(
% 32.06/4.53 ![X0]: (~element(X0,sK12_skl)|empty(sK12_skl)|in(set_union2(X0,sK11_skl(sK12_skl)),sK12_skl)|~sQ41_spl)),
% 32.06/4.53 inference(resolution,[status(thm)],[f809,f156])).
% 32.06/4.53 fof(f3280,plain,(
% 32.06/4.53 sQ54_spl|sQ7_spl|~sQ41_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f3275,f1096,f378,f808])).
% 32.06/4.53 fof(f3410,plain,(
% 32.06/4.53 ![X0]: (~element(symmetric_difference(X0,sK11_skl(sK12_skl)),sK12_skl)|element(set_intersection2(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)|~sQ41_spl)),
% 32.06/4.53 inference(resolution,[status(thm)],[f968,f809])).
% 32.06/4.53 fof(f3431,plain,(
% 32.06/4.53 ![X0]: (element(set_intersection2(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)|~sQ40_spl|~sQ41_spl)),
% 32.06/4.53 inference(forward_subsumption_resolution,[status(thm)],[f3410,f805])).
% 32.06/4.53 fof(f3915,plain,(
% 32.06/4.53 ~element(empty_set,sK12_skl)|in(sK10_skl(sK12_skl),sK12_skl)|~sQ59_spl),
% 32.06/4.53 inference(paramodulation,[status(thm)],[f197,f1153])).
% 32.06/4.53 fof(f3919,plain,(
% 32.06/4.53 ~sQ1_spl|sQ32_spl|~sQ59_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f3915,f185,f709,f1152])).
% 32.06/4.53 fof(f7071,definition,(
% 32.06/4.53 sQ370_spl <=> (empty(powerset(sK12_skl)))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ370_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f7072,plain,(
% 32.06/4.53 empty(powerset(sK12_skl))|~sQ370_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f7071])).
% 32.06/4.53 fof(f7082,plain,(
% 32.06/4.53 $false|~sQ370_spl),
% 32.06/4.53 inference(forward_subsumption_resolution,[status(thm)],[f7072,f78])).
% 32.06/4.53 fof(f7083,plain,(
% 32.06/4.53 ~sQ370_spl),
% 32.06/4.53 inference(contradiction_clause,[status(thm)],[f7082])).
% 32.06/4.53 fof(f7258,definition,(
% 32.06/4.53 sQ399_spl <=> (empty(powerset(powerset(empty_set))))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f7259,plain,(
% 32.06/4.53 empty(powerset(powerset(empty_set)))|~sQ399_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f7258])).
% 32.06/4.53 fof(f7269,plain,(
% 32.06/4.53 $false|~sQ399_spl),
% 32.06/4.53 inference(forward_subsumption_resolution,[status(thm)],[f7259,f78])).
% 32.06/4.53 fof(f7270,plain,(
% 32.06/4.53 ~sQ399_spl),
% 32.06/4.53 inference(contradiction_clause,[status(thm)],[f7269])).
% 32.06/4.53 fof(f22374,plain,(
% 32.06/4.53 ~element(sK10_skl(sK12_skl),sK12_skl)|in(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|~sQ40_spl|~sQ41_spl|~sQ22_spl),
% 32.06/4.53 inference(resolution,[status(thm)],[f3431,f670])).
% 32.06/4.53 fof(f22387,definition,(
% 32.06/4.53 sQ612_spl <=> (in(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl))),
% 32.06/4.53 introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition])).
% 32.06/4.53 fof(f22388,plain,(
% 32.06/4.53 in(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|~sQ612_spl),
% 32.06/4.53 inference(component_clause,[status(thm)],[f22387])).
% 32.06/4.53 fof(f22390,plain,(
% 32.06/4.53 ~sQ147_spl|sQ612_spl|~sQ40_spl|~sQ41_spl|~sQ22_spl),
% 32.06/4.53 inference(split_clause,[status(thm)],[f22374,f2823,f22387,f804,f808,f669])).
% 32.06/4.53 fof(f22403,plain,(
% 32.06/4.53 element(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|~sQ612_spl),
% 32.06/4.53 inference(resolution,[status(thm)],[f22388,f153])).
% 23.78/4.56 fof(f22406,plain,(
% 23.78/4.56 $false|sQ56_spl|~sQ612_spl),
% 23.78/4.56 inference(forward_subsumption_resolution,[status(thm)],[f22403,f1137])).
% 23.78/4.56 fof(f22407,plain,(
% 23.78/4.56 sQ56_spl|~sQ612_spl),
% 23.78/4.56 inference(contradiction_clause,[status(thm)],[f22406])).
% 23.78/4.56 fof(f22408,plain,(
% 23.78/4.56 ~element(sK10_skl(sK12_skl),sK12_skl)|sQ57_spl|~sQ54_spl),
% 23.78/4.56 inference(resolution,[status(thm)],[f1140,f1097])).
% 23.78/4.56 fof(f22411,plain,(
% 23.78/4.56 $false|~sQ32_spl|sQ57_spl|~sQ54_spl),
% 23.78/4.56 inference(forward_subsumption_resolution,[status(thm)],[f22408,f715])).
% 23.78/4.56 fof(f22412,plain,(
% 23.78/4.56 ~sQ32_spl|sQ57_spl|~sQ54_spl),
% 23.78/4.56 inference(contradiction_clause,[status(thm)],[f22411])).
% 23.78/4.56 fof(f22413,plain,(
% 23.78/4.56 $false),
% 23.78/4.56 inference(sat_refutation,[status(thm)],[f386,f672,f688,f696,f714,f807,f811,f981,f1025,f1038,f1057,f1141,f1167,f1523,f1740,f3024,f3025,f3280,f3919,f7083,f7270,f22390,f22407,f22412])).
% 23.78/4.56 % SZS output end CNFRefutation for theBenchmark.p
% 23.78/4.58 % Elapsed time: 4.224945 seconds
% 23.78/4.58 % CPU time: 33.166407 seconds
% 23.78/4.58 % Total memory used: 402.729 MB
% 23.78/4.58 % Net memory used: 387.902 MB
%------------------------------------------------------------------------------