%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU105+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 : n015.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 11.24s 2.16s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU105+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n015.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 05:54:05 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.49 % Drodi V4.1.1
% 11.24/2.16 % Refutation found
% 11.24/2.16 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.24/2.16 % SZS output start CNFRefutation for theBenchmark
% 11.24/2.16 fof(f3,axiom,(
% 11.24/2.16 (! [A] :( preboolean(A)=> ( cup_closed(A)& diff_closed(A) ) ) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f7,axiom,(
% 11.24/2.16 (! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f10,axiom,(
% 11.24/2.16 (! [A] :(? [B] : element(B,A) ))),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f15,axiom,(
% 11.24/2.16 (! [A] : ~ empty(powerset(A)) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f16,axiom,(
% 11.24/2.16 empty(empty_set) ),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f21,axiom,(
% 11.24/2.16 (! [A,B] : set_intersection2(A,A) = A )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f32,axiom,(
% 11.24/2.16 (! [A,B] : set_difference(A,B) = symmetric_difference(A,set_intersection2(A,B)) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f33,axiom,(
% 11.24/2.16 (! [A] :( preboolean(A)<=> (! [B,C] :( ( in(B,A)& in(C,A) )=> ( in(set_union2(B,C),A)& in(set_difference(B,C),A) ) ) )) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f34,conjecture,(
% 11.24/2.16 (! [A] :( ~ empty(A)=> ( (! [B] :( element(B,A)=> (! [C] :( element(C,A)=> ( in(symmetric_difference(B,C),A)& in(set_intersection2(B,C),A) ) ) )))=> preboolean(A) ) ) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f35,negated_conjecture,(
% 11.24/2.16 ~((! [A] :( ~ empty(A)=> ( (! [B] :( element(B,A)=> (! [C] :( element(C,A)=> ( in(symmetric_difference(B,C),A)& in(set_intersection2(B,C),A) ) ) )))=> preboolean(A) ) ) ))),
% 11.24/2.16 inference(negated_conjecture,[status(cth)],[f34])).
% 11.24/2.16 fof(f37,axiom,(
% 11.24/2.16 (! [A,B] :( in(A,B)=> element(A,B) ) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f39,axiom,(
% 11.24/2.16 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f45,axiom,(
% 11.24/2.16 (! [A,B,C] :~ ( in(A,B)& element(B,powerset(C))& empty(C) ) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f46,axiom,(
% 11.24/2.16 (! [A] :( empty(A)=> A = empty_set ) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f47,axiom,(
% 11.24/2.16 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f49,axiom,(
% 11.24/2.16 (! [A,B] : set_union2(A,B) = symmetric_difference(symmetric_difference(A,B),set_intersection2(A,B)) )),
% 11.24/2.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.24/2.16 fof(f54,plain,(
% 11.24/2.16 ![A]: (~preboolean(A)|(cup_closed(A)&diff_closed(A)))),
% 11.24/2.16 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 11.24/2.16 fof(f55,plain,(
% 11.24/2.16 ![X0]: (~preboolean(X0)|cup_closed(X0))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f54])).
% 11.24/2.16 fof(f62,plain,(
% 11.24/2.16 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,X0))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f7])).
% 11.24/2.16 fof(f65,plain,(
% 11.24/2.16 ![A]: element(sK0_skl(A),A)),
% 11.24/2.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f10])).
% 11.24/2.16 fof(f66,plain,(
% 11.24/2.16 ![X0]: (element(sK0_skl(X0),X0))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f65])).
% 11.24/2.16 fof(f78,plain,(
% 11.24/2.16 ![X0]: (~empty(powerset(X0)))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f15])).
% 11.24/2.16 fof(f79,plain,(
% 11.24/2.16 empty(empty_set)),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f16])).
% 11.24/2.16 fof(f90,plain,(
% 11.24/2.16 ![A]: set_intersection2(A,A)=A),
% 11.24/2.16 inference(miniscoping,[status(thm)],[f21])).
% 11.24/2.16 fof(f91,plain,(
% 11.24/2.16 ![X0]: (set_intersection2(X0,X0)=X0)),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f90])).
% 11.24/2.16 fof(f135,plain,(
% 11.24/2.16 ![X0,X1]: (set_difference(X0,X1)=symmetric_difference(X0,set_intersection2(X0,X1)))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f32])).
% 11.24/2.16 fof(f136,plain,(
% 11.24/2.16 ![A]: (preboolean(A)<=>(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A)))))),
% 11.24/2.16 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 11.24/2.16 fof(f137,plain,(
% 11.24/2.16 ![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))))))),
% 11.24/2.16 inference(NNF_transformation,[status(thm)],[f136])).
% 11.24/2.16 fof(f138,plain,(
% 11.24/2.16 (![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))))))),
% 11.24/2.16 inference(miniscoping,[status(thm)],[f137])).
% 11.24/2.16 fof(f139,plain,(
% 11.24/2.16 (![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)))))),
% 11.24/2.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl]),skolemize(B,sK10_skl(A)),skolemize(C,sK11_skl(A))],[f138])).
% 11.24/2.16 fof(f142,plain,(
% 11.24/2.16 ![X0]: (preboolean(X0)|in(sK10_skl(X0),X0))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f139])).
% 11.24/2.16 fof(f143,plain,(
% 11.24/2.16 ![X0]: (preboolean(X0)|in(sK11_skl(X0),X0))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f139])).
% 11.24/2.16 fof(f144,plain,(
% 11.24/2.16 ![X0]: (preboolean(X0)|~in(set_union2(sK10_skl(X0),sK11_skl(X0)),X0)|~in(set_difference(sK10_skl(X0),sK11_skl(X0)),X0))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f139])).
% 11.24/2.16 fof(f145,plain,(
% 11.24/2.16 (?[A]: (~empty(A)&((![B]: (~element(B,A)|(![C]: (~element(C,A)|(in(symmetric_difference(B,C),A)&in(set_intersection2(B,C),A))))))&~preboolean(A))))),
% 11.24/2.16 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 11.24/2.16 fof(f146,plain,(
% 11.24/2.16 (~empty(sK12_skl)&((![B]: (~element(B,sK12_skl)|(![C]: (~element(C,sK12_skl)|(in(symmetric_difference(B,C),sK12_skl)&in(set_intersection2(B,C),sK12_skl))))))&~preboolean(sK12_skl)))),
% 11.24/2.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f145])).
% 11.24/2.16 fof(f148,plain,(
% 11.24/2.16 ![X0,X1]: (~element(X0,sK12_skl)|~element(X1,sK12_skl)|in(symmetric_difference(X0,X1),sK12_skl))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f146])).
% 11.24/2.16 fof(f149,plain,(
% 11.24/2.16 ![X0,X1]: (~element(X0,sK12_skl)|~element(X1,sK12_skl)|in(set_intersection2(X0,X1),sK12_skl))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f146])).
% 11.24/2.16 fof(f150,plain,(
% 11.24/2.16 ~preboolean(sK12_skl)),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f146])).
% 11.24/2.16 fof(f152,plain,(
% 11.24/2.16 ![A,B]: (~in(A,B)|element(A,B))),
% 11.24/2.16 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 11.24/2.16 fof(f153,plain,(
% 11.24/2.16 ![X0,X1]: (~in(X0,X1)|element(X0,X1))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f152])).
% 11.24/2.16 fof(f155,plain,(
% 11.24/2.16 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 11.24/2.16 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 11.24/2.16 fof(f156,plain,(
% 11.24/2.16 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f155])).
% 11.24/2.16 fof(f167,plain,(
% 11.24/2.16 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|~empty(C))),
% 11.24/2.16 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 11.24/2.16 fof(f168,plain,(
% 11.24/2.16 ![C]: ((![B]: ((![A]: ~in(A,B))|~element(B,powerset(C))))|~empty(C))),
% 11.24/2.16 inference(miniscoping,[status(thm)],[f167])).
% 11.24/2.16 fof(f169,plain,(
% 11.24/2.16 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|~empty(X2))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f168])).
% 11.24/2.16 fof(f170,plain,(
% 11.24/2.16 ![A]: (~empty(A)|A=empty_set)),
% 11.24/2.16 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 11.24/2.16 fof(f171,plain,(
% 11.24/2.16 ![X0]: (~empty(X0)|X0=empty_set)),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f170])).
% 11.24/2.16 fof(f172,plain,(
% 11.24/2.16 ![A,B]: (~in(A,B)|~empty(B))),
% 11.24/2.16 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 11.24/2.16 fof(f173,plain,(
% 11.24/2.16 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 11.24/2.16 inference(miniscoping,[status(thm)],[f172])).
% 11.24/2.16 fof(f174,plain,(
% 11.24/2.16 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f173])).
% 11.24/2.16 fof(f178,plain,(
% 11.24/2.16 ![X0,X1]: (set_union2(X0,X1)=symmetric_difference(symmetric_difference(X0,X1),set_intersection2(X0,X1)))),
% 11.24/2.16 inference(cnf_transformation,[status(thm)],[f49])).
% 11.24/2.16 fof(f179,plain,(
% 11.24/2.16 ![X0]: (~element(X0,sK12_skl)|~element(X0,sK12_skl)|in(X0,sK12_skl))),
% 11.24/2.16 inference(paramodulation,[status(thm)],[f91,f149])).
% 11.24/2.16 fof(f180,plain,(
% 11.24/2.16 ![X0]: (~element(X0,sK12_skl)|in(X0,sK12_skl))),
% 11.24/2.16 inference(duplicate_literals_removal,[status(thm)],[f179])).
% 11.24/2.16 fof(f221,plain,(
% 11.24/2.16 ![X0]: (~in(X0,empty_set))),
% 11.24/2.16 inference(resolution,[status(thm)],[f79,f174])).
% 11.24/2.16 fof(f300,plain,(
% 11.24/2.16 ![X0,X1]: (element(set_intersection2(X0,X1),sK12_skl)|~element(X0,sK12_skl)|~element(X1,sK12_skl))),
% 11.24/2.16 inference(resolution,[status(thm)],[f153,f149])).
% 11.24/2.16 fof(f301,plain,(
% 11.24/2.16 ![X0,X1]: (element(symmetric_difference(X0,X1),sK12_skl)|~element(X0,sK12_skl)|~element(X1,sK12_skl))),
% 11.24/2.16 inference(resolution,[status(thm)],[f153,f148])).
% 11.24/2.16 fof(f320,plain,(
% 11.24/2.16 ![X0]: (empty(X0)|in(sK0_skl(X0),X0))),
% 11.24/2.16 inference(resolution,[status(thm)],[f66,f156])).
% 11.24/2.16 fof(f347,plain,(
% 11.24/2.16 ![X0,X1]: (~element(symmetric_difference(X0,X1),sK12_skl)|~element(set_intersection2(X0,X1),sK12_skl)|in(set_union2(X0,X1),sK12_skl))),
% 11.24/2.16 inference(paramodulation,[status(thm)],[f178,f148])).
% 11.24/2.16 fof(f485,plain,(
% 11.24/2.16 ![X0,X1]: (~element(symmetric_difference(X0,X1),sK12_skl)|~element(set_intersection2(X1,X0),sK12_skl)|in(set_union2(X0,X1),sK12_skl))),
% 11.24/2.16 inference(paramodulation,[status(thm)],[f62,f347])).
% 11.24/2.16 fof(f671,plain,(
% 11.24/2.16 ![X0,X1]: (set_difference(X0,X1)=symmetric_difference(X0,set_intersection2(X1,X0)))),
% 11.24/2.16 inference(paramodulation,[status(thm)],[f62,f135])).
% 11.24/2.16 fof(f736,plain,(
% 11.24/2.16 preboolean(empty_set)),
% 11.24/2.16 inference(resolution,[status(thm)],[f142,f221])).
% 11.24/2.16 fof(f737,plain,(
% 11.24/2.16 ![X0]: (preboolean(X0)|element(sK10_skl(X0),X0))),
% 11.24/2.16 inference(resolution,[status(thm)],[f142,f153])).
% 11.24/2.16 fof(f746,plain,(
% 11.24/2.16 cup_closed(empty_set)),
% 11.24/2.16 inference(resolution,[status(thm)],[f736,f55])).
% 11.24/2.16 fof(f759,plain,(
% 11.24/2.16 ![X0]: (preboolean(X0)|element(sK11_skl(X0),X0))),
% 11.24/2.16 inference(resolution,[status(thm)],[f143,f153])).
% 11.24/2.16 fof(f785,plain,(
% 11.24/2.16 ![X0]: (preboolean(sK12_skl)|element(set_intersection2(X0,sK10_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl))),
% 11.24/2.16 inference(resolution,[status(thm)],[f737,f300])).
% 11.24/2.16 fof(f789,plain,(
% 11.24/2.16 preboolean(sK12_skl)|in(sK10_skl(sK12_skl),sK12_skl)),
% 11.24/2.16 inference(resolution,[status(thm)],[f737,f180])).
% 11.24/2.16 fof(f791,definition,(
% 11.24/2.16 sQ27_spl <=> (preboolean(sK12_skl))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 11.24/2.16 fof(f792,plain,(
% 11.24/2.16 preboolean(sK12_skl)|~sQ27_spl),
% 11.24/2.16 inference(component_clause,[status(thm)],[f791])).
% 11.24/2.16 fof(f818,definition,(
% 11.24/2.16 ![X0]: (sQ34_spl <=> (element(set_intersection2(X0,sK10_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 11.24/2.16 fof(f819,plain,(
% 11.24/2.16 ![X0]: (element(set_intersection2(X0,sK10_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)|~sQ34_spl)),
% 11.24/2.16 inference(component_clause,[status(thm)],[f818])).
% 11.24/2.16 fof(f821,plain,(
% 11.24/2.16 sQ27_spl|sQ34_spl),
% 11.24/2.16 inference(split_clause,[status(thm)],[f785,f791,f818])).
% 11.24/2.16 fof(f834,definition,(
% 11.24/2.16 sQ38_spl <=> (in(sK10_skl(sK12_skl),sK12_skl))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 11.24/2.16 fof(f835,plain,(
% 11.24/2.16 in(sK10_skl(sK12_skl),sK12_skl)|~sQ38_spl),
% 11.24/2.16 inference(component_clause,[status(thm)],[f834])).
% 11.24/2.16 fof(f837,plain,(
% 11.24/2.16 sQ27_spl|sQ38_spl),
% 11.24/2.16 inference(split_clause,[status(thm)],[f789,f791,f834])).
% 11.24/2.16 fof(f838,plain,(
% 11.24/2.16 $false|~sQ27_spl),
% 11.24/2.16 inference(forward_subsumption_resolution,[status(thm)],[f792,f150])).
% 11.24/2.16 fof(f839,plain,(
% 11.24/2.16 ~sQ27_spl),
% 11.24/2.16 inference(contradiction_clause,[status(thm)],[f838])).
% 11.24/2.16 fof(f840,plain,(
% 11.24/2.16 element(sK10_skl(sK12_skl),sK12_skl)|~sQ38_spl),
% 11.24/2.16 inference(resolution,[status(thm)],[f835,f153])).
% 11.24/2.16 fof(f906,plain,(
% 11.24/2.16 ![X0]: (preboolean(sK12_skl)|element(symmetric_difference(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl))),
% 11.24/2.16 inference(resolution,[status(thm)],[f759,f301])).
% 11.24/2.16 fof(f913,plain,(
% 11.24/2.16 preboolean(sK12_skl)|in(sK11_skl(sK12_skl),sK12_skl)),
% 11.24/2.16 inference(resolution,[status(thm)],[f759,f180])).
% 11.24/2.16 fof(f927,definition,(
% 11.24/2.16 ![X0]: (sQ42_spl <=> (element(symmetric_difference(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 11.24/2.16 fof(f928,plain,(
% 11.24/2.16 ![X0]: (element(symmetric_difference(X0,sK11_skl(sK12_skl)),sK12_skl)|~element(X0,sK12_skl)|~sQ42_spl)),
% 11.24/2.16 inference(component_clause,[status(thm)],[f927])).
% 11.24/2.16 fof(f930,plain,(
% 11.24/2.16 sQ27_spl|sQ42_spl),
% 11.24/2.16 inference(split_clause,[status(thm)],[f906,f791,f927])).
% 11.24/2.16 fof(f955,definition,(
% 11.24/2.16 sQ49_spl <=> (in(sK11_skl(sK12_skl),sK12_skl))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 11.24/2.16 fof(f956,plain,(
% 11.24/2.16 in(sK11_skl(sK12_skl),sK12_skl)|~sQ49_spl),
% 11.24/2.16 inference(component_clause,[status(thm)],[f955])).
% 11.24/2.16 fof(f958,plain,(
% 11.24/2.16 sQ27_spl|sQ49_spl),
% 11.24/2.16 inference(split_clause,[status(thm)],[f913,f791,f955])).
% 11.24/2.16 fof(f959,plain,(
% 11.24/2.16 element(sK11_skl(sK12_skl),sK12_skl)|~sQ49_spl),
% 11.24/2.16 inference(resolution,[status(thm)],[f956,f153])).
% 11.24/2.16 fof(f982,plain,(
% 11.24/2.16 ![X0,X1]: (~in(X0,X1)|~element(X1,powerset(empty_set)))),
% 11.24/2.16 inference(resolution,[status(thm)],[f169,f79])).
% 11.24/2.16 fof(f1289,definition,(
% 11.24/2.16 sQ60_spl <=> (in(set_union2(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 11.24/2.16 fof(f1556,plain,(
% 11.24/2.16 element(set_intersection2(sK11_skl(sK12_skl),sK10_skl(sK12_skl)),sK12_skl)|~sQ34_spl|~sQ49_spl),
% 11.24/2.16 inference(resolution,[status(thm)],[f819,f959])).
% 11.24/2.16 fof(f1557,plain,(
% 11.24/2.16 element(set_intersection2(sK11_skl(sK12_skl),sK10_skl(sK12_skl)),sK12_skl)|preboolean(sK12_skl)|~sQ34_spl),
% 11.24/2.16 inference(resolution,[status(thm)],[f819,f759])).
% 11.24/2.16 fof(f1562,definition,(
% 11.24/2.16 sQ65_spl <=> (element(set_intersection2(sK11_skl(sK12_skl),sK10_skl(sK12_skl)),sK12_skl))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 11.24/2.16 fof(f1565,plain,(
% 11.24/2.16 sQ65_spl|sQ27_spl|~sQ34_spl),
% 11.24/2.16 inference(split_clause,[status(thm)],[f1557,f1562,f791,f818])).
% 11.24/2.16 fof(f1591,plain,(
% 11.24/2.16 ![X0,X1]: (~element(X0,sK12_skl)|~element(set_intersection2(X1,X0),sK12_skl)|in(set_difference(X0,X1),sK12_skl))),
% 11.24/2.16 inference(paramodulation,[status(thm)],[f671,f148])).
% 11.24/2.16 fof(f1633,plain,(
% 11.24/2.16 ![X0]: (~in(X0,sK0_skl(powerset(empty_set))))),
% 11.24/2.16 inference(resolution,[status(thm)],[f982,f66])).
% 11.24/2.16 fof(f1669,plain,(
% 11.24/2.16 empty(sK0_skl(powerset(empty_set)))),
% 11.24/2.16 inference(resolution,[status(thm)],[f1633,f320])).
% 11.24/2.16 fof(f1676,plain,(
% 11.24/2.16 sK0_skl(powerset(empty_set))=empty_set),
% 11.24/2.16 inference(resolution,[status(thm)],[f1669,f171])).
% 11.24/2.16 fof(f1680,definition,(
% 11.24/2.16 sQ76_spl <=> (cup_closed(sK0_skl(powerset(empty_set))))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 11.24/2.16 fof(f1682,plain,(
% 11.24/2.16 ~cup_closed(sK0_skl(powerset(empty_set)))|sQ76_spl),
% 11.24/2.16 inference(component_clause,[status(thm)],[f1680])).
% 11.24/2.16 fof(f1833,definition,(
% 11.24/2.16 sQ91_spl <=> (element(sK10_skl(sK12_skl),sK12_skl))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 11.24/2.16 fof(f1835,plain,(
% 11.24/2.16 ~element(sK10_skl(sK12_skl),sK12_skl)|sQ91_spl),
% 11.24/2.16 inference(component_clause,[status(thm)],[f1833])).
% 11.24/2.16 fof(f1854,definition,(
% 11.24/2.16 sQ92_spl <=> (empty(powerset(empty_set)))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 11.24/2.16 fof(f1855,plain,(
% 11.24/2.16 empty(powerset(empty_set))|~sQ92_spl),
% 11.24/2.16 inference(component_clause,[status(thm)],[f1854])).
% 11.24/2.16 fof(f1865,plain,(
% 11.24/2.16 $false|~sQ92_spl),
% 11.24/2.16 inference(forward_subsumption_resolution,[status(thm)],[f1855,f78])).
% 11.24/2.16 fof(f1866,plain,(
% 11.24/2.16 ~sQ92_spl),
% 11.24/2.16 inference(contradiction_clause,[status(thm)],[f1865])).
% 11.24/2.16 fof(f1926,plain,(
% 11.24/2.16 ~cup_closed(empty_set)|sQ76_spl),
% 11.24/2.16 inference(forward_demodulation,[status(thm)],[f1676,f1682])).
% 11.24/2.16 fof(f1927,plain,(
% 11.24/2.16 $false|sQ76_spl),
% 11.24/2.16 inference(forward_subsumption_resolution,[status(thm)],[f1926,f746])).
% 11.24/2.16 fof(f1928,plain,(
% 11.24/2.16 sQ76_spl),
% 11.24/2.16 inference(contradiction_clause,[status(thm)],[f1927])).
% 11.24/2.16 fof(f1976,plain,(
% 11.24/2.16 $false|~sQ38_spl|sQ91_spl),
% 11.24/2.16 inference(forward_subsumption_resolution,[status(thm)],[f1835,f840])).
% 11.24/2.16 fof(f1977,plain,(
% 11.24/2.16 ~sQ38_spl|sQ91_spl),
% 11.24/2.16 inference(contradiction_clause,[status(thm)],[f1976])).
% 11.24/2.16 fof(f2537,plain,(
% 11.24/2.16 element(symmetric_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|preboolean(sK12_skl)|~sQ42_spl),
% 11.24/2.16 inference(resolution,[status(thm)],[f928,f737])).
% 11.24/2.16 fof(f2552,definition,(
% 11.24/2.16 sQ155_spl <=> (element(symmetric_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl))),
% 11.24/2.16 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 11.24/2.18 fof(f2555,plain,(
% 11.24/2.18 sQ155_spl|sQ27_spl|~sQ42_spl),
% 11.24/2.18 inference(split_clause,[status(thm)],[f2537,f2552,f791,f927])).
% 11.24/2.18 fof(f4049,plain,(
% 11.24/2.18 ~element(sK10_skl(sK12_skl),sK12_skl)|~element(set_intersection2(sK11_skl(sK12_skl),sK10_skl(sK12_skl)),sK12_skl)|preboolean(sK12_skl)|~in(set_union2(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)),
% 11.24/2.18 inference(resolution,[status(thm)],[f1591,f144])).
% 11.24/2.18 fof(f4054,plain,(
% 11.24/2.18 ~sQ91_spl|~sQ65_spl|sQ27_spl|~sQ60_spl),
% 11.24/2.18 inference(split_clause,[status(thm)],[f4049,f1833,f1562,f791,f1289])).
% 11.24/2.18 fof(f4570,definition,(
% 11.24/2.18 sQ233_spl <=> (element(set_intersection2(sK0_skl(sK12_skl),set_intersection2(sK0_skl(sK12_skl),sK0_skl(sK12_skl))),sK12_skl))),
% 11.24/2.18 introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition])).
% 11.24/2.18 fof(f4572,plain,(
% 11.24/2.18 ~element(set_intersection2(sK0_skl(sK12_skl),set_intersection2(sK0_skl(sK12_skl),sK0_skl(sK12_skl))),sK12_skl)|sQ233_spl),
% 11.24/2.18 inference(component_clause,[status(thm)],[f4570])).
% 11.24/2.18 fof(f4589,plain,(
% 11.24/2.18 ~element(set_intersection2(sK0_skl(sK12_skl),sK0_skl(sK12_skl)),sK12_skl)|sQ233_spl),
% 11.24/2.18 inference(forward_demodulation,[status(thm)],[f91,f4572])).
% 11.24/2.18 fof(f4590,plain,(
% 11.24/2.18 ~element(sK0_skl(sK12_skl),sK12_skl)|sQ233_spl),
% 11.24/2.18 inference(forward_demodulation,[status(thm)],[f91,f4589])).
% 11.24/2.18 fof(f4591,plain,(
% 11.24/2.18 $false|sQ233_spl),
% 11.24/2.18 inference(forward_subsumption_resolution,[status(thm)],[f4590,f66])).
% 11.24/2.18 fof(f4592,plain,(
% 11.24/2.18 sQ233_spl),
% 11.24/2.18 inference(contradiction_clause,[status(thm)],[f4591])).
% 11.24/2.18 fof(f5237,definition,(
% 11.24/2.18 sQ271_spl <=> (element(sK0_skl(sK12_skl),sK12_skl))),
% 11.24/2.18 introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition])).
% 11.24/2.18 fof(f5239,plain,(
% 11.24/2.18 ~element(sK0_skl(sK12_skl),sK12_skl)|sQ271_spl),
% 11.24/2.18 inference(component_clause,[status(thm)],[f5237])).
% 11.24/2.18 fof(f5244,plain,(
% 11.24/2.18 $false|sQ271_spl),
% 11.24/2.18 inference(forward_subsumption_resolution,[status(thm)],[f5239,f66])).
% 11.24/2.18 fof(f5245,plain,(
% 11.24/2.18 sQ271_spl),
% 11.24/2.18 inference(contradiction_clause,[status(thm)],[f5244])).
% 11.24/2.18 fof(f6765,plain,(
% 11.24/2.18 ~element(symmetric_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|in(set_union2(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|~sQ34_spl|~sQ49_spl),
% 11.24/2.18 inference(resolution,[status(thm)],[f1556,f485])).
% 11.24/2.18 fof(f6789,plain,(
% 11.24/2.18 ~sQ155_spl|sQ60_spl|~sQ34_spl|~sQ49_spl),
% 11.24/2.18 inference(split_clause,[status(thm)],[f6765,f2552,f1289,f818,f955])).
% 11.24/2.18 fof(f6795,plain,(
% 11.24/2.18 $false),
% 11.24/2.18 inference(sat_refutation,[status(thm)],[f821,f837,f839,f930,f958,f1565,f1866,f1928,f1977,f2555,f4054,f4592,f5245,f6789])).
% 11.24/2.18 % SZS output end CNFRefutation for theBenchmark.p
% 11.24/2.20 % Elapsed time: 1.716179 seconds
% 11.24/2.20 % CPU time: 11.476636 seconds
% 11.24/2.20 % Total memory used: 197.705 MB
% 11.24/2.20 % Net memory used: 192.476 MB
%------------------------------------------------------------------------------