%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU109+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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 252.00s 32.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU109+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n013.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 05:50:20 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 252.00/32.30 % Refutation found
% 252.00/32.30 % SZS status Theorem for theBenchmark: Theorem is valid
% 252.00/32.30 % SZS output start CNFRefutation for theBenchmark
% 252.00/32.30 fof(f1,axiom,(
% 252.00/32.30 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f7,axiom,(
% 252.00/32.30 (! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f8,axiom,(
% 252.00/32.30 (! [A,B,C] :( C = set_intersection2(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)& in(D,B) ) ) )) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f13,axiom,(
% 252.00/32.30 (! [A] :( ~ empty(powerset(A))& cup_closed(powerset(A))& diff_closed(powerset(A))& preboolean(powerset(A)) ) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f20,axiom,(
% 252.00/32.30 (! [A,B] : set_intersection2(A,A) = A )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f21,axiom,(
% 252.00/32.30 (? [A] :( ~ empty(A)& finite(A) ) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f24,axiom,(
% 252.00/32.30 (? [A] : empty(A) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f25,axiom,(
% 252.00/32.30 (! [A] :(? [B] :( element(B,powerset(A))& empty(B)& relation(B)& function(B)& one_to_one(B)& epsilon_transitive(B)& epsilon_connected(B)& ordinal(B)& natural(B)& finite(B) ) ))),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f26,axiom,(
% 252.00/32.30 (! [A] :(? [B] :( element(B,powerset(A))& empty(B) ) ))),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f31,axiom,(
% 252.00/32.30 (! [A] :( preboolean(A)<=> (! [B,C] :( ( in(B,A)& in(C,A) )=> ( in(set_union2(B,C),A)& in(set_difference(B,C),A) ) ) )) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f32,axiom,(
% 252.00/32.30 (! [A] :( ( ~ empty(A)& preboolean(A) )=> in(empty_set,A) ) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f35,conjecture,(
% 252.00/32.30 (! [A] :( ( ~ empty(A)& preboolean(A) )=> (! [B] :( ( ~ empty(B)& preboolean(B) )=> ( ~ empty(set_intersection2(A,B))& preboolean(set_intersection2(A,B)) ) ) )) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f36,negated_conjecture,(
% 252.00/32.30 ~((! [A] :( ( ~ empty(A)& preboolean(A) )=> (! [B] :( ( ~ empty(B)& preboolean(B) )=> ( ~ empty(set_intersection2(A,B))& preboolean(set_intersection2(A,B)) ) ) )) ))),
% 252.00/32.30 inference(negated_conjecture,[status(cth)],[f35])).
% 252.00/32.30 fof(f43,axiom,(
% 252.00/32.30 (! [A,B,C] :~ ( in(A,B)& element(B,powerset(C))& empty(C) ) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f44,axiom,(
% 252.00/32.30 (! [A] :( empty(A)=> A = empty_set ) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f45,axiom,(
% 252.00/32.30 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f46,axiom,(
% 252.00/32.30 (! [A,B] :~ ( empty(A)& A != B& empty(B) ) )),
% 252.00/32.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 252.00/32.30 fof(f47,plain,(
% 252.00/32.30 ![A,B]: (~in(A,B)|~in(B,A))),
% 252.00/32.30 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 252.00/32.30 fof(f48,plain,(
% 252.00/32.30 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 252.00/32.30 inference(cnf_transformation,[status(thm)],[f47])).
% 252.00/32.30 fof(f59,plain,(
% 252.00/32.30 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,X0))),
% 252.00/32.30 inference(cnf_transformation,[status(thm)],[f7])).
% 252.00/32.30 fof(f60,plain,(
% 252.00/32.30 ![A,B,C]: ((~C=set_intersection2(A,B)|(![D]: ((~in(D,C)|(in(D,A)&in(D,B)))&(in(D,C)|(~in(D,A)|~in(D,B))))))&(C=set_intersection2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)|~in(D,B)))&(in(D,C)|(in(D,A)&in(D,B)))))))),
% 252.00/32.30 inference(NNF_transformation,[status(thm)],[f8])).
% 252.00/32.30 fof(f61,plain,(
% 252.00/32.30 (![A,B,C]: (~C=set_intersection2(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_intersection2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)|~in(D,B)))&(in(D,C)|(in(D,A)&in(D,B)))))))),
% 252.00/32.30 inference(miniscoping,[status(thm)],[f60])).
% 252.00/32.30 fof(f62,plain,(
% 252.00/32.30 (![A,B,C]: (~C=set_intersection2(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_intersection2(A,B)|((~in(sK0_skl(C,B,A),C)|(~in(sK0_skl(C,B,A),A)|~in(sK0_skl(C,B,A),B)))&(in(sK0_skl(C,B,A),C)|(in(sK0_skl(C,B,A),A)&in(sK0_skl(C,B,A),B))))))),
% 252.00/32.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(D,sK0_skl(C,B,A))],[f61])).
% 252.00/32.31 fof(f63,plain,(
% 252.00/32.31 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|~in(X3,X0)|in(X3,X1))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f62])).
% 252.00/32.31 fof(f64,plain,(
% 252.00/32.31 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|~in(X3,X0)|in(X3,X2))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f62])).
% 252.00/32.31 fof(f65,plain,(
% 252.00/32.31 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|in(X3,X0)|~in(X3,X1)|~in(X3,X2))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f62])).
% 252.00/32.31 fof(f66,plain,(
% 252.00/32.31 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|~in(sK0_skl(X0,X2,X1),X0)|~in(sK0_skl(X0,X2,X1),X1)|~in(sK0_skl(X0,X2,X1),X2))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f62])).
% 252.00/32.31 fof(f67,plain,(
% 252.00/32.31 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|in(sK0_skl(X0,X2,X1),X0)|in(sK0_skl(X0,X2,X1),X1))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f62])).
% 252.00/32.31 fof(f80,plain,(
% 252.00/32.31 (((![A]: ~empty(powerset(A)))&(![A]: cup_closed(powerset(A))))&(![A]: diff_closed(powerset(A))))&(![A]: preboolean(powerset(A)))),
% 252.00/32.31 inference(miniscoping,[status(thm)],[f13])).
% 252.00/32.31 fof(f81,plain,(
% 252.00/32.31 ![X0]: (~empty(powerset(X0)))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f80])).
% 252.00/32.31 fof(f97,plain,(
% 252.00/32.31 ![A]: set_intersection2(A,A)=A),
% 252.00/32.31 inference(miniscoping,[status(thm)],[f20])).
% 252.00/32.31 fof(f98,plain,(
% 252.00/32.31 ![X0]: (set_intersection2(X0,X0)=X0)),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f97])).
% 252.00/32.31 fof(f99,plain,(
% 252.00/32.31 (~empty(sK2_skl)&finite(sK2_skl))),
% 252.00/32.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(A,sK2_skl)],[f21])).
% 252.00/32.31 fof(f100,plain,(
% 252.00/32.31 ~empty(sK2_skl)),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f99])).
% 252.00/32.31 fof(f112,plain,(
% 252.00/32.31 empty(sK5_skl)),
% 252.00/32.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f24])).
% 252.00/32.31 fof(f113,plain,(
% 252.00/32.31 empty(sK5_skl)),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f112])).
% 252.00/32.31 fof(f114,plain,(
% 252.00/32.31 ![A]: (((((((((element(sK6_skl(A),powerset(A))&empty(sK6_skl(A)))&relation(sK6_skl(A)))&function(sK6_skl(A)))&one_to_one(sK6_skl(A)))&epsilon_transitive(sK6_skl(A)))&epsilon_connected(sK6_skl(A)))&ordinal(sK6_skl(A)))&natural(sK6_skl(A)))&finite(sK6_skl(A)))),
% 252.00/32.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(B,sK6_skl(A))],[f25])).
% 252.00/32.31 fof(f116,plain,(
% 252.00/32.31 ![X0]: (empty(sK6_skl(X0)))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f114])).
% 252.00/32.31 fof(f125,plain,(
% 252.00/32.31 ![A]: (element(sK7_skl(A),powerset(A))&empty(sK7_skl(A)))),
% 252.00/32.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f26])).
% 252.00/32.31 fof(f126,plain,(
% 252.00/32.31 ![X0]: (element(sK7_skl(X0),powerset(X0)))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f125])).
% 252.00/32.31 fof(f127,plain,(
% 252.00/32.31 ![X0]: (empty(sK7_skl(X0)))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f125])).
% 252.00/32.31 fof(f142,plain,(
% 252.00/32.31 ![A]: (preboolean(A)<=>(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A)))))),
% 252.00/32.31 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 252.00/32.31 fof(f143,plain,(
% 252.00/32.31 ![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))))))),
% 252.00/32.31 inference(NNF_transformation,[status(thm)],[f142])).
% 252.00/32.31 fof(f144,plain,(
% 252.00/32.31 (![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))))))),
% 252.00/32.31 inference(miniscoping,[status(thm)],[f143])).
% 252.00/32.31 fof(f145,plain,(
% 252.00/32.31 (![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(sK11_skl(A),A)&in(sK12_skl(A),A))&(~in(set_union2(sK11_skl(A),sK12_skl(A)),A)|~in(set_difference(sK11_skl(A),sK12_skl(A)),A)))))),
% 252.00/32.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl]),skolemize(B,sK11_skl(A)),skolemize(C,sK12_skl(A))],[f144])).
% 252.00/32.31 fof(f146,plain,(
% 252.00/32.31 ![X0,X1,X2]: (~preboolean(X0)|~in(X1,X0)|~in(X2,X0)|in(set_union2(X1,X2),X0))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f145])).
% 252.00/32.31 fof(f147,plain,(
% 252.00/32.31 ![X0,X1,X2]: (~preboolean(X0)|~in(X1,X0)|~in(X2,X0)|in(set_difference(X1,X2),X0))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f145])).
% 252.00/32.31 fof(f148,plain,(
% 252.00/32.31 ![X0]: (preboolean(X0)|in(sK11_skl(X0),X0))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f145])).
% 252.00/32.31 fof(f149,plain,(
% 252.00/32.31 ![X0]: (preboolean(X0)|in(sK12_skl(X0),X0))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f145])).
% 252.00/32.31 fof(f150,plain,(
% 252.00/32.31 ![X0]: (preboolean(X0)|~in(set_union2(sK11_skl(X0),sK12_skl(X0)),X0)|~in(set_difference(sK11_skl(X0),sK12_skl(X0)),X0))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f145])).
% 252.00/32.31 fof(f151,plain,(
% 252.00/32.31 ![A]: ((empty(A)|~preboolean(A))|in(empty_set,A))),
% 252.00/32.31 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 252.00/32.31 fof(f152,plain,(
% 252.00/32.31 ![X0]: (empty(X0)|~preboolean(X0)|in(empty_set,X0))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f151])).
% 252.00/32.31 fof(f156,plain,(
% 252.00/32.31 (?[A]: ((~empty(A)&preboolean(A))&(?[B]: ((~empty(B)&preboolean(B))&(empty(set_intersection2(A,B))|~preboolean(set_intersection2(A,B)))))))),
% 252.00/32.31 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 252.00/32.31 fof(f157,plain,(
% 252.00/32.31 ((~empty(sK13_skl)&preboolean(sK13_skl))&((~empty(sK14_skl)&preboolean(sK14_skl))&(empty(set_intersection2(sK13_skl,sK14_skl))|~preboolean(set_intersection2(sK13_skl,sK14_skl)))))),
% 252.00/32.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(A,sK13_skl),skolemize(B,sK14_skl)],[f156])).
% 252.00/32.31 fof(f158,plain,(
% 252.00/32.31 ~empty(sK13_skl)),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f157])).
% 252.00/32.31 fof(f159,plain,(
% 252.00/32.31 preboolean(sK13_skl)),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f157])).
% 252.00/32.31 fof(f160,plain,(
% 252.00/32.31 ~empty(sK14_skl)),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f157])).
% 252.00/32.31 fof(f161,plain,(
% 252.00/32.31 preboolean(sK14_skl)),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f157])).
% 252.00/32.31 fof(f162,plain,(
% 252.00/32.31 empty(set_intersection2(sK13_skl,sK14_skl))|~preboolean(set_intersection2(sK13_skl,sK14_skl))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f157])).
% 252.00/32.31 fof(f175,plain,(
% 252.00/32.31 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|~empty(C))),
% 252.00/32.31 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 252.00/32.31 fof(f176,plain,(
% 252.00/32.31 ![C]: ((![B]: ((![A]: ~in(A,B))|~element(B,powerset(C))))|~empty(C))),
% 252.00/32.31 inference(miniscoping,[status(thm)],[f175])).
% 252.00/32.31 fof(f177,plain,(
% 252.00/32.31 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|~empty(X2))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f176])).
% 252.00/32.31 fof(f178,plain,(
% 252.00/32.31 ![A]: (~empty(A)|A=empty_set)),
% 252.00/32.31 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 252.00/32.31 fof(f179,plain,(
% 252.00/32.31 ![X0]: (~empty(X0)|X0=empty_set)),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f178])).
% 252.00/32.31 fof(f180,plain,(
% 252.00/32.31 ![A,B]: (~in(A,B)|~empty(B))),
% 252.00/32.31 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 252.00/32.31 fof(f181,plain,(
% 252.00/32.31 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 252.00/32.31 inference(miniscoping,[status(thm)],[f180])).
% 252.00/32.31 fof(f182,plain,(
% 252.00/32.31 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f181])).
% 252.00/32.31 fof(f183,plain,(
% 252.00/32.31 ![A,B]: ((~empty(A)|A=B)|~empty(B))),
% 252.00/32.31 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 252.00/32.31 fof(f184,plain,(
% 252.00/32.31 ![B]: ((![A]: (~empty(A)|A=B))|~empty(B))),
% 252.00/32.31 inference(miniscoping,[status(thm)],[f183])).
% 252.00/32.31 fof(f185,plain,(
% 252.00/32.31 ![X0,X1]: (~empty(X0)|X0=X1|~empty(X1))),
% 252.00/32.31 inference(cnf_transformation,[status(thm)],[f184])).
% 252.00/32.31 fof(f186,definition,(
% 252.00/32.31 sQ0_spl <=> (empty(set_intersection2(sK13_skl,sK14_skl)))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f187,plain,(
% 252.00/32.31 empty(set_intersection2(sK13_skl,sK14_skl))|~sQ0_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f186])).
% 252.00/32.31 fof(f189,definition,(
% 252.00/32.31 sQ1_spl <=> (preboolean(set_intersection2(sK13_skl,sK14_skl)))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f192,plain,(
% 252.00/32.31 sQ0_spl|~sQ1_spl),
% 252.00/32.31 inference(split_clause,[status(thm)],[f162,f186,f189])).
% 252.00/32.31 fof(f193,plain,(
% 252.00/32.31 ![X0,X1,X2]: (~in(X0,set_intersection2(X1,X2))|in(X0,X1))),
% 252.00/32.31 inference(destructive_equality_resolution,[status(thm)],[f63])).
% 252.00/32.31 fof(f194,plain,(
% 252.00/32.31 ![X0,X1,X2]: (~in(X0,set_intersection2(X1,X2))|in(X0,X2))),
% 252.00/32.31 inference(destructive_equality_resolution,[status(thm)],[f64])).
% 252.00/32.31 fof(f195,plain,(
% 252.00/32.31 ![X0,X1,X2]: (in(X0,set_intersection2(X1,X2))|~in(X0,X1)|~in(X0,X2))),
% 252.00/32.31 inference(destructive_equality_resolution,[status(thm)],[f65])).
% 252.00/32.31 fof(f224,plain,(
% 252.00/32.31 sK5_skl=empty_set),
% 252.00/32.31 inference(resolution,[status(thm)],[f179,f113])).
% 252.00/32.31 fof(f225,plain,(
% 252.00/32.31 set_intersection2(sK13_skl,sK14_skl)=empty_set|~sQ0_spl),
% 252.00/32.31 inference(resolution,[status(thm)],[f179,f187])).
% 252.00/32.31 fof(f321,plain,(
% 252.00/32.31 ![X0,X1]: (~empty(X0)|X0=sK6_skl(X1))),
% 252.00/32.31 inference(resolution,[status(thm)],[f116,f185])).
% 252.00/32.31 fof(f326,plain,(
% 252.00/32.31 ![X0,X1]: (X0=set_intersection2(X1,X1)|~in(sK0_skl(X0,X1,X1),X0)|~in(sK0_skl(X0,X1,X1),X1))),
% 252.00/32.31 inference(factoring,[status(thm)],[f66])).
% 252.00/32.31 fof(f327,plain,(
% 252.00/32.31 ![X0,X1]: (X0=X1|~in(sK0_skl(X0,X1,X1),X0)|~in(sK0_skl(X0,X1,X1),X1))),
% 252.00/32.31 inference(forward_demodulation,[status(thm)],[f98,f326])).
% 252.00/32.31 fof(f338,plain,(
% 252.00/32.31 ![X0,X1,X2]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X2)|in(sK0_skl(set_intersection2(X0,X1),X2,set_intersection2(X0,X1)),X1))),
% 252.00/32.31 inference(resolution,[status(thm)],[f67,f194])).
% 252.00/32.31 fof(f341,plain,(
% 252.00/32.31 ![X0,X1,X2,X3]: (set_intersection2(X0,X1)=set_intersection2(X2,X3)|in(sK0_skl(set_intersection2(X0,X1),X3,X2),X2)|in(sK0_skl(set_intersection2(X0,X1),X3,X2),X0))),
% 252.00/32.31 inference(resolution,[status(thm)],[f67,f193])).
% 252.00/32.31 fof(f342,plain,(
% 252.00/32.31 ![X0,X1,X2]: (X0=set_intersection2(X0,X1)|~element(X0,powerset(X2))|~empty(X2))),
% 252.00/32.31 inference(resolution,[status(thm)],[f67,f177])).
% 252.00/32.31 fof(f361,plain,(
% 252.00/32.31 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|in(sK0_skl(X0,X2,X1),X0)|~empty(X1))),
% 252.00/32.31 inference(resolution,[status(thm)],[f67,f182])).
% 252.00/32.31 fof(f363,plain,(
% 252.00/32.31 ![X0,X1]: (X0=set_intersection2(X0,X1)|in(sK0_skl(X0,X1,X0),X0))),
% 252.00/32.31 inference(factoring,[status(thm)],[f67])).
% 252.00/32.31 fof(f409,plain,(
% 252.00/32.31 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1)|set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1)|~in(sK0_skl(set_intersection2(X0,X1),X1,set_intersection2(X0,X1)),set_intersection2(X0,X1))|~in(sK0_skl(set_intersection2(X0,X1),X1,set_intersection2(X0,X1)),set_intersection2(X0,X1)))),
% 252.00/32.31 inference(resolution,[status(thm)],[f338,f66])).
% 252.00/32.31 fof(f427,plain,(
% 252.00/32.31 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1)|~in(sK0_skl(set_intersection2(X0,X1),X1,set_intersection2(X0,X1)),set_intersection2(X0,X1)))),
% 252.00/32.31 inference(duplicate_literals_removal,[status(thm)],[f409])).
% 252.00/32.31 fof(f481,plain,(
% 252.00/32.31 ![X0,X1,X2]: (X0=set_intersection2(sK7_skl(X1),X2)|in(sK0_skl(X0,X2,sK7_skl(X1)),X0))),
% 252.00/32.31 inference(resolution,[status(thm)],[f127,f361])).
% 252.00/32.31 fof(f488,plain,(
% 252.00/32.31 ![X0]: (sK7_skl(X0)=empty_set)),
% 252.00/32.31 inference(resolution,[status(thm)],[f127,f179])).
% 252.00/32.31 fof(f557,definition,(
% 252.00/32.31 ![X0]: (sQ5_spl <=> (~empty(X0)))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f558,plain,(
% 252.00/32.31 ![X0]: (~empty(X0)|~sQ5_spl)),
% 252.00/32.31 inference(component_clause,[status(thm)],[f557])).
% 252.00/32.31 fof(f1216,plain,(
% 252.00/32.31 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X0,X0)|set_intersection2(X0,X1)=X0|~in(sK0_skl(set_intersection2(X0,X1),X0,X0),set_intersection2(X0,X1)))),
% 252.00/32.31 inference(resolution,[status(thm)],[f341,f327])).
% 252.00/32.31 fof(f1256,plain,(
% 252.00/32.31 ![X0,X1]: (set_intersection2(X0,X1)=X0|set_intersection2(X0,X1)=X0|~in(sK0_skl(set_intersection2(X0,X1),X0,X0),set_intersection2(X0,X1)))),
% 252.00/32.31 inference(forward_demodulation,[status(thm)],[f98,f1216])).
% 252.00/32.31 fof(f1257,plain,(
% 252.00/32.31 ![X0,X1]: (set_intersection2(X0,X1)=X0|~in(sK0_skl(set_intersection2(X0,X1),X0,X0),set_intersection2(X0,X1)))),
% 252.00/32.31 inference(duplicate_literals_removal,[status(thm)],[f1256])).
% 252.00/32.31 fof(f1315,plain,(
% 252.00/32.31 ![X0]: (sK5_skl=sK6_skl(X0))),
% 252.00/32.31 inference(resolution,[status(thm)],[f113,f321])).
% 252.00/32.31 fof(f1329,plain,(
% 252.00/32.31 ![X0,X1]: (X0=set_intersection2(X0,X1)|~element(X0,powerset(sK5_skl)))),
% 252.00/32.31 inference(resolution,[status(thm)],[f113,f342])).
% 252.00/32.31 fof(f1506,plain,(
% 252.00/32.31 ![X0]: (element(empty_set,powerset(X0)))),
% 252.00/32.31 inference(forward_demodulation,[status(thm)],[f488,f126])).
% 252.00/32.31 fof(f1851,plain,(
% 252.00/32.31 ![X0]: (empty_set=set_intersection2(empty_set,X0))),
% 252.00/32.31 inference(resolution,[status(thm)],[f1329,f1506])).
% 252.00/32.31 fof(f2058,plain,(
% 252.00/32.31 ![X0,X1]: (set_intersection2(X0,X1)=X0|~in(sK0_skl(set_intersection2(X0,X1),X0,X0),set_intersection2(X1,X0)))),
% 252.00/32.31 inference(paramodulation,[status(thm)],[f59,f1257])).
% 252.00/32.31 fof(f2568,plain,(
% 252.00/32.31 ![X0]: (empty_set=sK6_skl(X0))),
% 252.00/32.31 inference(backward_demodulation,[status(thm)],[f224,f1315])).
% 252.00/32.31 fof(f2965,plain,(
% 252.00/32.31 empty(empty_set)),
% 252.00/32.31 inference(forward_demodulation,[status(thm)],[f2568,f116])).
% 252.00/32.31 fof(f2983,plain,(
% 252.00/32.31 ![X0,X1]: (~in(X0,sK14_skl)|~in(X1,sK14_skl)|in(set_union2(X0,X1),sK14_skl))),
% 252.00/32.31 inference(resolution,[status(thm)],[f146,f161])).
% 252.00/32.31 fof(f2984,plain,(
% 252.00/32.31 ![X0,X1]: (~in(X0,sK13_skl)|~in(X1,sK13_skl)|in(set_union2(X0,X1),sK13_skl))),
% 252.00/32.31 inference(resolution,[status(thm)],[f146,f159])).
% 252.00/32.31 fof(f2987,plain,(
% 252.00/32.31 ![X0,X1]: (~in(X0,sK14_skl)|~in(X1,sK14_skl)|in(set_difference(X0,X1),sK14_skl))),
% 252.00/32.31 inference(resolution,[status(thm)],[f147,f161])).
% 252.00/32.31 fof(f2988,plain,(
% 252.00/32.31 ![X0,X1]: (~in(X0,sK13_skl)|~in(X1,sK13_skl)|in(set_difference(X0,X1),sK13_skl))),
% 252.00/32.31 inference(resolution,[status(thm)],[f147,f159])).
% 252.00/32.31 fof(f2998,plain,(
% 252.00/32.31 ![X0,X1]: (preboolean(set_intersection2(X0,X1))|in(sK11_skl(set_intersection2(X0,X1)),X1))),
% 252.00/32.31 inference(resolution,[status(thm)],[f148,f194])).
% 252.00/32.31 fof(f2999,plain,(
% 252.00/32.31 ![X0,X1]: (preboolean(set_intersection2(X0,X1))|in(sK11_skl(set_intersection2(X0,X1)),X0))),
% 252.00/32.31 inference(resolution,[status(thm)],[f148,f193])).
% 252.00/32.31 fof(f3042,plain,(
% 252.00/32.31 ![X0,X1,X2]: (~in(X0,sK14_skl)|~in(X1,sK14_skl)|in(set_union2(X0,X1),set_intersection2(X2,sK14_skl))|~in(set_union2(X0,X1),X2))),
% 252.00/32.31 inference(resolution,[status(thm)],[f2983,f195])).
% 252.00/32.31 fof(f3055,definition,(
% 252.00/32.31 sQ63_spl <=> (empty(sK14_skl))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f3056,plain,(
% 252.00/32.31 empty(sK14_skl)|~sQ63_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f3055])).
% 252.00/32.31 fof(f3059,definition,(
% 252.00/32.31 sQ64_spl <=> (in(empty_set,sK14_skl))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f3060,plain,(
% 252.00/32.31 in(empty_set,sK14_skl)|~sQ64_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f3059])).
% 252.00/32.31 fof(f4098,plain,(
% 252.00/32.31 ![X0,X1]: (preboolean(set_intersection2(X0,X1))|in(sK12_skl(set_intersection2(X0,X1)),X1))),
% 252.00/32.31 inference(resolution,[status(thm)],[f149,f194])).
% 252.00/32.31 fof(f4099,plain,(
% 252.00/32.31 ![X0,X1]: (preboolean(set_intersection2(X0,X1))|in(sK12_skl(set_intersection2(X0,X1)),X0))),
% 252.00/32.31 inference(resolution,[status(thm)],[f149,f193])).
% 252.00/32.31 fof(f4136,plain,(
% 252.00/32.31 empty(sK14_skl)|in(empty_set,sK14_skl)),
% 252.00/32.31 inference(resolution,[status(thm)],[f152,f161])).
% 252.00/32.31 fof(f4139,plain,(
% 252.00/32.31 empty(sK13_skl)|in(empty_set,sK13_skl)),
% 252.00/32.31 inference(resolution,[status(thm)],[f152,f159])).
% 252.00/32.31 fof(f4140,plain,(
% 252.00/32.31 sQ63_spl|sQ64_spl),
% 252.00/32.31 inference(split_clause,[status(thm)],[f4136,f3055,f3059])).
% 252.00/32.31 fof(f4143,definition,(
% 252.00/32.31 sQ102_spl <=> (empty(sK13_skl))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f4144,plain,(
% 252.00/32.31 empty(sK13_skl)|~sQ102_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f4143])).
% 252.00/32.31 fof(f4146,definition,(
% 252.00/32.31 sQ103_spl <=> (in(empty_set,sK13_skl))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f4147,plain,(
% 252.00/32.31 in(empty_set,sK13_skl)|~sQ103_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f4146])).
% 252.00/32.31 fof(f4149,plain,(
% 252.00/32.31 sQ102_spl|sQ103_spl),
% 252.00/32.31 inference(split_clause,[status(thm)],[f4139,f4143,f4146])).
% 252.00/32.31 fof(f4150,plain,(
% 252.00/32.31 $false|~sQ102_spl),
% 252.00/32.31 inference(forward_subsumption_resolution,[status(thm)],[f4144,f158])).
% 252.00/32.31 fof(f4151,plain,(
% 252.00/32.31 ~sQ102_spl),
% 252.00/32.31 inference(contradiction_clause,[status(thm)],[f4150])).
% 252.00/32.31 fof(f4154,plain,(
% 252.00/32.31 $false|~sQ63_spl),
% 252.00/32.31 inference(forward_subsumption_resolution,[status(thm)],[f3056,f160])).
% 252.00/32.31 fof(f4155,plain,(
% 252.00/32.31 ~sQ63_spl),
% 252.00/32.31 inference(contradiction_clause,[status(thm)],[f4154])).
% 252.00/32.31 fof(f4206,plain,(
% 252.00/32.31 ![X0,X1,X2]: (~in(X0,sK14_skl)|~in(X1,sK14_skl)|in(set_difference(X0,X1),set_intersection2(X2,sK14_skl))|~in(set_difference(X0,X1),X2))),
% 252.00/32.31 inference(resolution,[status(thm)],[f2987,f195])).
% 252.00/32.31 fof(f4869,definition,(
% 252.00/32.31 sQ119_spl <=> (in(empty_set,empty_set))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f4870,plain,(
% 252.00/32.31 in(empty_set,empty_set)|~sQ119_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f4869])).
% 252.00/32.31 fof(f5924,plain,(
% 252.00/32.31 ~in(empty_set,empty_set)|~sQ119_spl),
% 252.00/32.31 inference(resolution,[status(thm)],[f4870,f48])).
% 252.00/32.31 fof(f5928,plain,(
% 252.00/32.31 $false|~sQ119_spl),
% 252.00/32.31 inference(forward_subsumption_resolution,[status(thm)],[f5924,f4870])).
% 252.00/32.31 fof(f5929,plain,(
% 252.00/32.31 ~sQ119_spl),
% 252.00/32.31 inference(contradiction_clause,[status(thm)],[f5928])).
% 252.00/32.31 fof(f6342,plain,(
% 252.00/32.31 ![X0]: (in(empty_set,set_intersection2(X0,sK14_skl))|~in(empty_set,X0)|~sQ64_spl)),
% 252.00/32.31 inference(resolution,[status(thm)],[f3060,f195])).
% 252.00/32.31 fof(f7129,plain,(
% 252.00/32.31 ![X0,X1]: (~in(X0,sK14_skl)|~in(X1,sK14_skl)|in(set_union2(X0,X1),set_intersection2(sK13_skl,sK14_skl))|~in(X0,sK13_skl)|~in(X1,sK13_skl))),
% 252.00/32.31 inference(resolution,[status(thm)],[f3042,f2984])).
% 252.00/32.31 fof(f8109,definition,(
% 252.00/32.31 sQ160_spl <=> (set_intersection2(set_intersection2(sK14_skl,sK13_skl),sK14_skl)=set_intersection2(sK14_skl,sK13_skl))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f8111,plain,(
% 252.00/32.31 ~set_intersection2(set_intersection2(sK14_skl,sK13_skl),sK14_skl)=set_intersection2(sK14_skl,sK13_skl)|sQ160_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f8109])).
% 252.00/32.31 fof(f8139,definition,(
% 252.00/32.31 sQ165_spl <=> (set_intersection2(sK14_skl,set_intersection2(sK14_skl,sK13_skl))=set_intersection2(sK14_skl,sK13_skl))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f8141,plain,(
% 252.00/32.31 ~set_intersection2(sK14_skl,set_intersection2(sK14_skl,sK13_skl))=set_intersection2(sK14_skl,sK13_skl)|sQ165_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f8139])).
% 252.00/32.31 fof(f8685,plain,(
% 252.00/32.31 ~set_intersection2(sK14_skl,set_intersection2(sK13_skl,sK14_skl))=set_intersection2(sK14_skl,sK13_skl)|sQ165_spl),
% 252.00/32.31 inference(paramodulation,[status(thm)],[f59,f8141])).
% 252.00/32.31 fof(f8689,plain,(
% 252.00/32.31 ~set_intersection2(set_intersection2(sK13_skl,sK14_skl),sK14_skl)=set_intersection2(sK14_skl,sK13_skl)|sQ160_spl),
% 252.00/32.31 inference(paramodulation,[status(thm)],[f59,f8111])).
% 252.00/32.31 fof(f8950,definition,(
% 252.00/32.31 ![X0]: (sQ184_spl <=> (empty(X0)))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ184_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f8951,plain,(
% 252.00/32.31 ![X0]: (empty(X0)|~sQ184_spl)),
% 252.00/32.31 inference(component_clause,[status(thm)],[f8950])).
% 252.00/32.31 fof(f8960,plain,(
% 252.00/32.31 $false|~sQ184_spl),
% 252.00/32.31 inference(backward_subsumption_resolution,[status(thm)],[f160,f8951])).
% 252.00/32.31 fof(f9135,plain,(
% 252.00/32.31 ![X0]: (~in(X0,empty_set))),
% 252.00/32.31 inference(resolution,[status(thm)],[f2965,f182])).
% 252.00/32.31 fof(f9258,plain,(
% 252.00/32.31 ![X0,X1]: (~in(X0,sK14_skl)|~in(X1,sK14_skl)|in(set_difference(X0,X1),set_intersection2(sK13_skl,sK14_skl))|~in(X0,sK13_skl)|~in(X1,sK13_skl))),
% 252.00/32.31 inference(resolution,[status(thm)],[f4206,f2988])).
% 252.00/32.31 fof(f12861,definition,(
% 252.00/32.31 sQ194_spl <=> (in(sK11_skl(empty_set),empty_set))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f12862,plain,(
% 252.00/32.31 in(sK11_skl(empty_set),empty_set)|~sQ194_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f12861])).
% 252.00/32.31 fof(f12867,plain,(
% 252.00/32.31 $false|~sQ194_spl),
% 252.00/32.31 inference(forward_subsumption_resolution,[status(thm)],[f12862,f9135])).
% 252.00/32.31 fof(f12868,plain,(
% 252.00/32.31 ~sQ194_spl),
% 252.00/32.31 inference(contradiction_clause,[status(thm)],[f12867])).
% 252.00/32.31 fof(f13006,definition,(
% 252.00/32.31 sQ198_spl <=> (empty(sK2_skl))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f13007,plain,(
% 252.00/32.31 empty(sK2_skl)|~sQ198_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f13006])).
% 252.00/32.31 fof(f13013,plain,(
% 252.00/32.31 $false|~sQ198_spl),
% 252.00/32.31 inference(forward_subsumption_resolution,[status(thm)],[f13007,f100])).
% 252.00/32.31 fof(f13014,plain,(
% 252.00/32.31 ~sQ198_spl),
% 252.00/32.31 inference(contradiction_clause,[status(thm)],[f13013])).
% 252.00/32.31 fof(f13105,definition,(
% 252.00/32.31 sQ200_spl <=> (in(sK12_skl(empty_set),empty_set))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f13106,plain,(
% 252.00/32.31 in(sK12_skl(empty_set),empty_set)|~sQ200_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f13105])).
% 252.00/32.31 fof(f13222,plain,(
% 252.00/32.31 $false|~sQ200_spl),
% 252.00/32.31 inference(forward_subsumption_resolution,[status(thm)],[f13106,f9135])).
% 252.00/32.31 fof(f13223,plain,(
% 252.00/32.31 ~sQ200_spl),
% 252.00/32.31 inference(contradiction_clause,[status(thm)],[f13222])).
% 252.00/32.31 fof(f14272,definition,(
% 252.00/32.31 sQ239_spl <=> (empty(powerset(empty_set)))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ239_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f14273,plain,(
% 252.00/32.31 empty(powerset(empty_set))|~sQ239_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f14272])).
% 252.00/32.31 fof(f14307,plain,(
% 252.00/32.31 $false|~sQ239_spl),
% 252.00/32.31 inference(forward_subsumption_resolution,[status(thm)],[f14273,f81])).
% 252.00/32.31 fof(f14308,plain,(
% 252.00/32.31 ~sQ239_spl),
% 252.00/32.31 inference(contradiction_clause,[status(thm)],[f14307])).
% 252.00/32.31 fof(f14785,plain,(
% 252.00/32.31 ~set_intersection2(sK13_skl,sK14_skl)=set_intersection2(sK14_skl,sK13_skl)|sQ160_spl),
% 252.00/32.31 inference(backward_demodulation,[status(thm)],[f14791,f8689])).
% 252.00/32.31 fof(f14791,plain,(
% 252.00/32.31 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1))),
% 252.00/32.31 inference(forward_subsumption_resolution,[status(thm)],[f427,f363])).
% 252.00/32.31 fof(f14793,plain,(
% 252.00/32.31 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,set_intersection2(X0,X1)))),
% 252.00/32.31 inference(paramodulation,[status(thm)],[f59,f14791])).
% 252.00/32.31 fof(f15058,plain,(
% 252.00/32.31 $false|sQ160_spl),
% 252.00/32.31 inference(forward_subsumption_resolution,[status(thm)],[f14785,f59])).
% 252.00/32.31 fof(f15059,plain,(
% 252.00/32.31 sQ160_spl),
% 252.00/32.31 inference(contradiction_clause,[status(thm)],[f15058])).
% 252.00/32.31 fof(f15178,plain,(
% 252.00/32.31 ~set_intersection2(sK13_skl,sK14_skl)=set_intersection2(sK14_skl,sK13_skl)|sQ165_spl),
% 252.00/32.31 inference(backward_demodulation,[status(thm)],[f14793,f8685])).
% 252.00/32.31 fof(f15437,plain,(
% 252.00/32.31 $false|sQ165_spl),
% 252.00/32.31 inference(forward_subsumption_resolution,[status(thm)],[f15178,f59])).
% 252.00/32.31 fof(f15438,plain,(
% 252.00/32.31 sQ165_spl),
% 252.00/32.31 inference(contradiction_clause,[status(thm)],[f15437])).
% 252.00/32.31 fof(f15703,plain,(
% 252.00/32.31 $false|~sQ5_spl),
% 252.00/32.31 inference(backward_subsumption_resolution,[status(thm)],[f2965,f558])).
% 252.00/32.31 fof(f15704,plain,(
% 252.00/32.31 ~sQ5_spl),
% 252.00/32.31 inference(contradiction_clause,[status(thm)],[f15703])).
% 252.00/32.31 fof(f45929,plain,(
% 252.00/32.31 in(empty_set,set_intersection2(sK13_skl,sK14_skl))|~sQ64_spl|~sQ103_spl),
% 252.00/32.31 inference(resolution,[status(thm)],[f6342,f4147])).
% 252.00/32.31 fof(f53938,plain,(
% 252.00/32.31 ![X0,X1,X2]: (X0=set_intersection2(empty_set,X1)|in(sK0_skl(X0,X1,sK7_skl(X2)),X0))),
% 252.00/32.31 inference(forward_demodulation,[status(thm)],[f488,f481])).
% 252.00/32.31 fof(f53939,plain,(
% 252.00/32.31 ![X0,X1,X2]: (X0=empty_set|in(sK0_skl(X0,X1,sK7_skl(X2)),X0))),
% 252.00/32.31 inference(forward_demodulation,[status(thm)],[f1851,f53938])).
% 252.00/32.31 fof(f53940,plain,(
% 252.00/32.31 ![X0,X1]: (X0=empty_set|in(sK0_skl(X0,X1,empty_set),X0))),
% 252.00/32.31 inference(forward_demodulation,[status(thm)],[f488,f53939])).
% 252.00/32.31 fof(f53942,plain,(
% 252.00/32.31 set_intersection2(empty_set,empty_set)=empty_set|set_intersection2(empty_set,empty_set)=empty_set),
% 252.00/32.31 inference(resolution,[status(thm)],[f53940,f2058])).
% 252.00/32.31 fof(f54049,definition,(
% 252.00/32.31 sQ280_spl <=> (set_intersection2(empty_set,empty_set)=empty_set)),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f54052,plain,(
% 252.00/32.31 sQ280_spl),
% 252.00/32.31 inference(split_clause,[status(thm)],[f53942,f54049])).
% 252.00/32.31 fof(f67423,plain,(
% 252.00/32.31 ~in(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK14_skl)|~in(sK12_skl(set_intersection2(sK13_skl,sK14_skl)),sK14_skl)|~in(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK13_skl)|~in(sK12_skl(set_intersection2(sK13_skl,sK14_skl)),sK13_skl)|preboolean(set_intersection2(sK13_skl,sK14_skl))|~in(set_union2(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK12_skl(set_intersection2(sK13_skl,sK14_skl))),set_intersection2(sK13_skl,sK14_skl))),
% 252.00/32.31 inference(resolution,[status(thm)],[f9258,f150])).
% 252.00/32.31 fof(f67432,definition,(
% 252.00/32.31 sQ306_spl <=> (in(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK14_skl))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f67434,plain,(
% 252.00/32.31 ~in(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK14_skl)|sQ306_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f67432])).
% 252.00/32.31 fof(f67435,definition,(
% 252.00/32.31 sQ307_spl <=> (in(sK12_skl(set_intersection2(sK13_skl,sK14_skl)),sK14_skl))),
% 252.00/32.31 introduced(definition,[new_symbols(definition,[sQ307_spl])],[split_symbol_definition])).
% 252.00/32.31 fof(f67437,plain,(
% 252.00/32.31 ~in(sK12_skl(set_intersection2(sK13_skl,sK14_skl)),sK14_skl)|sQ307_spl),
% 252.00/32.31 inference(component_clause,[status(thm)],[f67435])).
% 224.85/32.39 fof(f67438,definition,(
% 224.85/32.39 sQ308_spl <=> (in(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK13_skl))),
% 224.85/32.39 introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition])).
% 224.85/32.39 fof(f67440,plain,(
% 224.85/32.39 ~in(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK13_skl)|sQ308_spl),
% 224.85/32.39 inference(component_clause,[status(thm)],[f67438])).
% 224.85/32.39 fof(f67441,definition,(
% 224.85/32.39 sQ309_spl <=> (in(sK12_skl(set_intersection2(sK13_skl,sK14_skl)),sK13_skl))),
% 224.85/32.39 introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition])).
% 224.85/32.39 fof(f67443,plain,(
% 224.85/32.39 ~in(sK12_skl(set_intersection2(sK13_skl,sK14_skl)),sK13_skl)|sQ309_spl),
% 224.85/32.39 inference(component_clause,[status(thm)],[f67441])).
% 224.85/32.39 fof(f67444,definition,(
% 224.85/32.39 sQ310_spl <=> (in(set_union2(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK12_skl(set_intersection2(sK13_skl,sK14_skl))),set_intersection2(sK13_skl,sK14_skl)))),
% 224.85/32.39 introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition])).
% 224.85/32.39 fof(f67446,plain,(
% 224.85/32.39 ~in(set_union2(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK12_skl(set_intersection2(sK13_skl,sK14_skl))),set_intersection2(sK13_skl,sK14_skl))|sQ310_spl),
% 224.85/32.39 inference(component_clause,[status(thm)],[f67444])).
% 224.85/32.39 fof(f67447,plain,(
% 224.85/32.39 ~sQ306_spl|~sQ307_spl|~sQ308_spl|~sQ309_spl|sQ1_spl|~sQ310_spl),
% 224.85/32.39 inference(split_clause,[status(thm)],[f67423,f67432,f67435,f67438,f67441,f189,f67444])).
% 224.85/32.39 fof(f67676,plain,(
% 224.85/32.39 preboolean(set_intersection2(sK13_skl,sK14_skl))|sQ309_spl),
% 224.85/32.39 inference(resolution,[status(thm)],[f67443,f4099])).
% 224.85/32.39 fof(f67677,plain,(
% 224.85/32.39 sQ1_spl|sQ309_spl),
% 224.85/32.39 inference(split_clause,[status(thm)],[f67676,f189,f67441])).
% 224.85/32.39 fof(f67678,plain,(
% 224.85/32.39 preboolean(set_intersection2(sK13_skl,sK14_skl))|sQ308_spl),
% 224.85/32.39 inference(resolution,[status(thm)],[f67440,f2999])).
% 224.85/32.39 fof(f67679,plain,(
% 224.85/32.39 sQ1_spl|sQ308_spl),
% 224.85/32.39 inference(split_clause,[status(thm)],[f67678,f189,f67438])).
% 224.85/32.39 fof(f67680,plain,(
% 224.85/32.39 preboolean(set_intersection2(sK13_skl,sK14_skl))|sQ307_spl),
% 224.85/32.39 inference(resolution,[status(thm)],[f67437,f4098])).
% 224.85/32.39 fof(f67681,plain,(
% 224.85/32.39 sQ1_spl|sQ307_spl),
% 224.85/32.39 inference(split_clause,[status(thm)],[f67680,f189,f67435])).
% 224.85/32.39 fof(f67682,plain,(
% 224.85/32.39 preboolean(set_intersection2(sK13_skl,sK14_skl))|sQ306_spl),
% 224.85/32.39 inference(resolution,[status(thm)],[f67434,f2998])).
% 224.85/32.39 fof(f67683,plain,(
% 224.85/32.39 sQ1_spl|sQ306_spl),
% 224.85/32.39 inference(split_clause,[status(thm)],[f67682,f189,f67432])).
% 224.85/32.39 fof(f71522,plain,(
% 224.85/32.39 ~in(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK14_skl)|~in(sK12_skl(set_intersection2(sK13_skl,sK14_skl)),sK14_skl)|~in(sK11_skl(set_intersection2(sK13_skl,sK14_skl)),sK13_skl)|~in(sK12_skl(set_intersection2(sK13_skl,sK14_skl)),sK13_skl)|sQ310_spl),
% 224.85/32.39 inference(resolution,[status(thm)],[f67446,f7129])).
% 224.85/32.39 fof(f71523,plain,(
% 224.85/32.39 ~sQ306_spl|~sQ307_spl|~sQ308_spl|~sQ309_spl|sQ310_spl),
% 224.85/32.39 inference(split_clause,[status(thm)],[f71522,f67432,f67435,f67438,f67441,f67444])).
% 224.85/32.39 fof(f71572,plain,(
% 224.85/32.39 ~sQ184_spl),
% 224.85/32.39 inference(contradiction_clause,[status(thm)],[f8960])).
% 224.85/32.39 fof(f71599,plain,(
% 224.85/32.39 in(empty_set,empty_set)|~sQ0_spl|~sQ64_spl|~sQ103_spl),
% 224.85/32.39 inference(backward_demodulation,[status(thm)],[f225,f45929])).
% 224.85/32.39 fof(f71844,plain,(
% 224.85/32.39 sQ119_spl|~sQ0_spl|~sQ64_spl|~sQ103_spl),
% 224.85/32.39 inference(split_clause,[status(thm)],[f71599,f4869,f186,f3059,f4146])).
% 224.85/32.39 fof(f72332,plain,(
% 224.85/32.39 $false),
% 224.85/32.39 inference(sat_refutation,[status(thm)],[f192,f4140,f4149,f4151,f4155,f5929,f12868,f13014,f13223,f14308,f15059,f15438,f15704,f54052,f67447,f67677,f67679,f67681,f67683,f71523,f71572,f71844])).
% 224.85/32.39 % SZS output end CNFRefutation for theBenchmark.p
% 148.23/32.48 % Elapsed time: 32.102420 seconds
% 148.23/32.48 % CPU time: 253.666426 seconds
% 148.23/32.48 % Total memory used: 1.035 GB
% 148.23/32.48 % Net memory used: 954.807 MB
%------------------------------------------------------------------------------