%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU119+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:42 PM UTC 2026
% Result : Theorem 1.22s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU119+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n011.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 05:51:25 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 1.22/0.57 % Refutation found
% 1.22/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.22/0.57 % SZS output start CNFRefutation for theBenchmark
% 1.22/0.57 fof(f1,axiom,(
% 1.22/0.57 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 1.22/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.22/0.57 fof(f2,axiom,(
% 1.22/0.57 (! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) )),
% 1.22/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.22/0.57 fof(f3,axiom,(
% 1.22/0.57 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 1.22/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.22/0.57 fof(f4,axiom,(
% 1.22/0.57 (! [A,B,C] :( C = set_intersection2(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)& in(D,B) ) ) )) )),
% 1.22/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.22/0.57 fof(f5,axiom,(
% 1.22/0.57 (! [A,B] :( disjoint(A,B)<=> set_intersection2(A,B) = empty_set ) )),
% 1.22/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.22/0.57 fof(f9,axiom,(
% 1.22/0.57 (! [A,B] : set_intersection2(A,A) = A )),
% 1.22/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.22/0.57 fof(f12,axiom,(
% 1.22/0.57 (! [A,B] :( disjoint(A,B)=> disjoint(B,A) ) )),
% 1.22/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.22/0.57 fof(f13,conjecture,(
% 1.22/0.57 (! [A,B] :( ~ ( ~ disjoint(A,B)& (! [C] :~ ( in(C,A)& in(C,B) ) ))& ~ ( (? [C] :( in(C,A)& in(C,B) ))& disjoint(A,B) ) ) )),
% 1.22/0.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.22/0.57 fof(f14,negated_conjecture,(
% 1.22/0.57 ~((! [A,B] :( ~ ( ~ disjoint(A,B)& (! [C] :~ ( in(C,A)& in(C,B) ) ))& ~ ( (? [C] :( in(C,A)& in(C,B) ))& disjoint(A,B) ) ) ))),
% 1.22/0.57 inference(negated_conjecture,[status(cth)],[f13])).
% 1.22/0.57 fof(f15,plain,(
% 1.22/0.57 ![A,B]: (~in(A,B)|~in(B,A))),
% 1.22/0.57 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 1.22/0.57 fof(f16,plain,(
% 1.22/0.57 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f15])).
% 1.22/0.57 fof(f17,plain,(
% 1.22/0.57 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,X0))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f2])).
% 1.22/0.57 fof(f18,plain,(
% 1.22/0.57 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 1.22/0.57 inference(NNF_transformation,[status(thm)],[f3])).
% 1.22/0.57 fof(f19,plain,(
% 1.22/0.57 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 1.22/0.57 inference(miniscoping,[status(thm)],[f18])).
% 1.22/0.57 fof(f20,plain,(
% 1.22/0.57 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK0_skl(A),A)))),
% 1.22/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f19])).
% 1.22/0.57 fof(f21,plain,(
% 1.22/0.57 ![X0,X1]: (~X0=empty_set|~in(X1,X0))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f20])).
% 1.22/0.57 fof(f22,plain,(
% 1.22/0.57 ![X0]: (X0=empty_set|in(sK0_skl(X0),X0))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f20])).
% 1.22/0.57 fof(f23,plain,(
% 1.22/0.57 ![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)))))))),
% 1.22/0.57 inference(NNF_transformation,[status(thm)],[f4])).
% 1.22/0.57 fof(f24,plain,(
% 1.22/0.57 (![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)))))))),
% 1.22/0.57 inference(miniscoping,[status(thm)],[f23])).
% 1.22/0.57 fof(f25,plain,(
% 1.22/0.57 (![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(sK1_skl(C,B,A),C)|(~in(sK1_skl(C,B,A),A)|~in(sK1_skl(C,B,A),B)))&(in(sK1_skl(C,B,A),C)|(in(sK1_skl(C,B,A),A)&in(sK1_skl(C,B,A),B))))))),
% 1.22/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(C,B,A))],[f24])).
% 1.22/0.57 fof(f26,plain,(
% 1.22/0.57 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|~in(X3,X0)|in(X3,X1))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f25])).
% 1.22/0.57 fof(f27,plain,(
% 1.22/0.57 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|~in(X3,X0)|in(X3,X2))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f25])).
% 1.22/0.57 fof(f28,plain,(
% 1.22/0.57 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|in(X3,X0)|~in(X3,X1)|~in(X3,X2))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f25])).
% 1.22/0.57 fof(f29,plain,(
% 1.22/0.57 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|~in(sK1_skl(X0,X2,X1),X0)|~in(sK1_skl(X0,X2,X1),X1)|~in(sK1_skl(X0,X2,X1),X2))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f25])).
% 1.22/0.57 fof(f30,plain,(
% 1.22/0.57 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|in(sK1_skl(X0,X2,X1),X0)|in(sK1_skl(X0,X2,X1),X1))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f25])).
% 1.22/0.57 fof(f31,plain,(
% 1.22/0.57 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|in(sK1_skl(X0,X2,X1),X0)|in(sK1_skl(X0,X2,X1),X2))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f25])).
% 1.22/0.57 fof(f32,plain,(
% 1.22/0.57 ![A,B]: ((~disjoint(A,B)|set_intersection2(A,B)=empty_set)&(disjoint(A,B)|~set_intersection2(A,B)=empty_set))),
% 1.22/0.57 inference(NNF_transformation,[status(thm)],[f5])).
% 1.22/0.57 fof(f33,plain,(
% 1.22/0.57 (![A,B]: (~disjoint(A,B)|set_intersection2(A,B)=empty_set))&(![A,B]: (disjoint(A,B)|~set_intersection2(A,B)=empty_set))),
% 1.22/0.57 inference(miniscoping,[status(thm)],[f32])).
% 1.22/0.57 fof(f34,plain,(
% 1.22/0.57 ![X0,X1]: (~disjoint(X0,X1)|set_intersection2(X0,X1)=empty_set)),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f33])).
% 1.22/0.57 fof(f35,plain,(
% 1.22/0.57 ![X0,X1]: (disjoint(X0,X1)|~set_intersection2(X0,X1)=empty_set)),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f33])).
% 1.22/0.57 fof(f37,plain,(
% 1.22/0.57 ![A]: set_intersection2(A,A)=A),
% 1.22/0.57 inference(miniscoping,[status(thm)],[f9])).
% 1.22/0.57 fof(f38,plain,(
% 1.22/0.57 ![X0]: (set_intersection2(X0,X0)=X0)),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f37])).
% 1.22/0.57 fof(f43,plain,(
% 1.22/0.57 ![A,B]: (~disjoint(A,B)|disjoint(B,A))),
% 1.22/0.57 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 1.22/0.57 fof(f44,plain,(
% 1.22/0.57 ![X0,X1]: (~disjoint(X0,X1)|disjoint(X1,X0))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f43])).
% 1.22/0.57 fof(f45,plain,(
% 1.22/0.57 (?[A,B]: ((~disjoint(A,B)&(![C]: (~in(C,A)|~in(C,B))))|((?[C]: (in(C,A)&in(C,B)))&disjoint(A,B))))),
% 1.22/0.57 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 1.22/0.57 fof(f46,definition,(
% 1.22/0.57 ![A,B]: (sP0_prd(B,A)<=>(~disjoint(A,B)&(![C]: (~in(C,A)|~in(C,B)))))),
% 1.22/0.57 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 1.22/0.57 fof(f47,plain,(
% 1.22/0.57 ?[A,B]: (sP0_prd(B,A)|((?[C]: (in(C,A)&in(C,B)))&disjoint(A,B)))),
% 1.22/0.57 inference(formula_renaming,[status(thm)],[f45,f46])).
% 1.22/0.57 fof(f48,plain,(
% 1.22/0.57 (?[A,B]: sP0_prd(B,A))|(?[A,B]: ((?[C]: (in(C,A)&in(C,B)))&disjoint(A,B)))),
% 1.22/0.57 inference(miniscoping,[status(thm)],[f47])).
% 1.22/0.57 fof(f49,plain,(
% 1.22/0.57 sP0_prd(sK5_skl,sK4_skl)|((in(sK8_skl,sK6_skl)&in(sK8_skl,sK7_skl))&disjoint(sK6_skl,sK7_skl))),
% 1.22/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl]),skolemize(A,sK4_skl),skolemize(B,sK5_skl),skolemize(A,sK6_skl),skolemize(B,sK7_skl),skolemize(C,sK8_skl)],[f48])).
% 1.22/0.57 fof(f50,plain,(
% 1.22/0.57 sP0_prd(sK5_skl,sK4_skl)|in(sK8_skl,sK6_skl)),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f49])).
% 1.22/0.57 fof(f51,plain,(
% 1.22/0.57 sP0_prd(sK5_skl,sK4_skl)|in(sK8_skl,sK7_skl)),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f49])).
% 1.22/0.57 fof(f52,plain,(
% 1.22/0.57 sP0_prd(sK5_skl,sK4_skl)|disjoint(sK6_skl,sK7_skl)),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f49])).
% 1.22/0.57 fof(f53,plain,(
% 1.22/0.57 ![A,B]: ((~sP0_prd(B,A)|(~disjoint(A,B)&(![C]: (~in(C,A)|~in(C,B)))))&(sP0_prd(B,A)|(disjoint(A,B)|(?[C]: (in(C,A)&in(C,B))))))),
% 1.22/0.57 inference(NNF_transformation,[status(thm)],[f46])).
% 1.22/0.57 fof(f54,plain,(
% 1.22/0.57 (![A,B]: (~sP0_prd(B,A)|(~disjoint(A,B)&(![C]: (~in(C,A)|~in(C,B))))))&(![A,B]: (sP0_prd(B,A)|(disjoint(A,B)|(?[C]: (in(C,A)&in(C,B))))))),
% 1.22/0.57 inference(miniscoping,[status(thm)],[f53])).
% 1.22/0.57 fof(f55,plain,(
% 1.22/0.57 (![A,B]: (~sP0_prd(B,A)|(~disjoint(A,B)&(![C]: (~in(C,A)|~in(C,B))))))&(![A,B]: (sP0_prd(B,A)|(disjoint(A,B)|(in(sK9_skl(B,A),A)&in(sK9_skl(B,A),B)))))),
% 1.22/0.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(C,sK9_skl(B,A))],[f54])).
% 1.22/0.57 fof(f56,plain,(
% 1.22/0.57 ![X0,X1]: (~sP0_prd(X0,X1)|~disjoint(X1,X0))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f55])).
% 1.22/0.57 fof(f57,plain,(
% 1.22/0.57 ![X0,X1,X2]: (~sP0_prd(X0,X1)|~in(X2,X1)|~in(X2,X0))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f55])).
% 1.22/0.57 fof(f58,plain,(
% 1.22/0.57 ![X0,X1]: (sP0_prd(X0,X1)|disjoint(X1,X0)|in(sK9_skl(X0,X1),X1))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f55])).
% 1.22/0.57 fof(f59,plain,(
% 1.22/0.57 ![X0,X1]: (sP0_prd(X0,X1)|disjoint(X1,X0)|in(sK9_skl(X0,X1),X0))),
% 1.22/0.57 inference(cnf_transformation,[status(thm)],[f55])).
% 1.22/0.57 fof(f60,definition,(
% 1.22/0.57 sQ0_spl <=> (sP0_prd(sK5_skl,sK4_skl))),
% 1.22/0.57 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.22/0.57 fof(f61,plain,(
% 1.22/0.57 sP0_prd(sK5_skl,sK4_skl)|~sQ0_spl),
% 1.22/0.57 inference(component_clause,[status(thm)],[f60])).
% 1.22/0.57 fof(f63,definition,(
% 1.22/0.57 sQ1_spl <=> (in(sK8_skl,sK6_skl))),
% 1.22/0.57 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.22/0.57 fof(f64,plain,(
% 1.22/0.57 in(sK8_skl,sK6_skl)|~sQ1_spl),
% 1.22/0.57 inference(component_clause,[status(thm)],[f63])).
% 1.22/0.57 fof(f66,plain,(
% 1.22/0.57 sQ0_spl|sQ1_spl),
% 1.22/0.57 inference(split_clause,[status(thm)],[f50,f60,f63])).
% 1.22/0.57 fof(f67,definition,(
% 1.22/0.57 sQ2_spl <=> (in(sK8_skl,sK7_skl))),
% 1.22/0.57 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 1.22/0.57 fof(f68,plain,(
% 1.22/0.57 in(sK8_skl,sK7_skl)|~sQ2_spl),
% 1.22/0.57 inference(component_clause,[status(thm)],[f67])).
% 1.22/0.57 fof(f70,plain,(
% 1.22/0.57 sQ0_spl|sQ2_spl),
% 1.22/0.57 inference(split_clause,[status(thm)],[f51,f60,f67])).
% 1.22/0.57 fof(f71,definition,(
% 1.22/0.57 sQ3_spl <=> (disjoint(sK6_skl,sK7_skl))),
% 1.22/0.57 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f72,plain,(
% 1.22/0.58 disjoint(sK6_skl,sK7_skl)|~sQ3_spl),
% 1.22/0.58 inference(component_clause,[status(thm)],[f71])).
% 1.22/0.58 fof(f74,plain,(
% 1.22/0.58 sQ0_spl|sQ3_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f52,f60,f71])).
% 1.22/0.58 fof(f75,plain,(
% 1.22/0.58 ![X0]: (~in(X0,empty_set))),
% 1.22/0.58 inference(destructive_equality_resolution,[status(thm)],[f21])).
% 1.22/0.58 fof(f76,plain,(
% 1.22/0.58 ![X0,X1,X2]: (~in(X0,set_intersection2(X1,X2))|in(X0,X1))),
% 1.22/0.58 inference(destructive_equality_resolution,[status(thm)],[f26])).
% 1.22/0.58 fof(f77,plain,(
% 1.22/0.58 ![X0,X1,X2]: (~in(X0,set_intersection2(X1,X2))|in(X0,X2))),
% 1.22/0.58 inference(destructive_equality_resolution,[status(thm)],[f27])).
% 1.22/0.58 fof(f78,plain,(
% 1.22/0.58 ![X0,X1,X2]: (in(X0,set_intersection2(X1,X2))|~in(X0,X1)|~in(X0,X2))),
% 1.22/0.58 inference(destructive_equality_resolution,[status(thm)],[f28])).
% 1.22/0.58 fof(f80,plain,(
% 1.22/0.58 ![X0,X1,X2]: (sP0_prd(X0,X1)|disjoint(X1,X0)|~sP0_prd(X1,X2)|~in(sK9_skl(X0,X1),X2))),
% 1.22/0.58 inference(resolution,[status(thm)],[f58,f57])).
% 1.22/0.58 fof(f89,plain,(
% 1.22/0.58 ![X0,X1]: (sP0_prd(X0,X1)|disjoint(X1,X0)|~sP0_prd(X1,X0)|sP0_prd(X0,X1)|disjoint(X1,X0))),
% 1.22/0.58 inference(resolution,[status(thm)],[f80,f59])).
% 1.22/0.58 fof(f91,plain,(
% 1.22/0.58 ![X0,X1]: (sP0_prd(X0,X1)|disjoint(X1,X0)|~sP0_prd(X1,X0))),
% 1.22/0.58 inference(duplicate_literals_removal,[status(thm)],[f89])).
% 1.22/0.58 fof(f93,plain,(
% 1.22/0.58 sP0_prd(sK4_skl,sK5_skl)|disjoint(sK5_skl,sK4_skl)|~sQ0_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f91,f61])).
% 1.22/0.58 fof(f94,definition,(
% 1.22/0.58 sQ4_spl <=> (sP0_prd(sK4_skl,sK5_skl))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f95,plain,(
% 1.22/0.58 sP0_prd(sK4_skl,sK5_skl)|~sQ4_spl),
% 1.22/0.58 inference(component_clause,[status(thm)],[f94])).
% 1.22/0.58 fof(f97,definition,(
% 1.22/0.58 sQ5_spl <=> (disjoint(sK5_skl,sK4_skl))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f98,plain,(
% 1.22/0.58 disjoint(sK5_skl,sK4_skl)|~sQ5_spl),
% 1.22/0.58 inference(component_clause,[status(thm)],[f97])).
% 1.22/0.58 fof(f100,plain,(
% 1.22/0.58 sQ4_spl|sQ5_spl|~sQ0_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f93,f94,f97,f60])).
% 1.22/0.58 fof(f114,plain,(
% 1.22/0.58 disjoint(sK4_skl,sK5_skl)|~sQ5_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f98,f44])).
% 1.22/0.58 fof(f117,plain,(
% 1.22/0.58 ~sP0_prd(sK5_skl,sK4_skl)|~sQ5_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f114,f56])).
% 1.22/0.58 fof(f118,plain,(
% 1.22/0.58 $false|~sQ0_spl|~sQ5_spl),
% 1.22/0.58 inference(forward_subsumption_resolution,[status(thm)],[f117,f61])).
% 1.22/0.58 fof(f119,plain,(
% 1.22/0.58 ~sQ0_spl|~sQ5_spl),
% 1.22/0.58 inference(contradiction_clause,[status(thm)],[f118])).
% 1.22/0.58 fof(f130,plain,(
% 1.22/0.58 disjoint(sK7_skl,sK6_skl)|~sQ3_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f72,f44])).
% 1.22/0.58 fof(f141,plain,(
% 1.22/0.58 ![X0,X1]: (X0=empty_set|~sP0_prd(X0,X1)|~in(sK0_skl(X0),X1))),
% 1.22/0.58 inference(resolution,[status(thm)],[f22,f57])).
% 1.22/0.58 fof(f143,plain,(
% 1.22/0.58 ![X0,X1]: (X0=empty_set|~sP0_prd(X1,X0)|~in(sK0_skl(X0),X1))),
% 1.22/0.58 inference(resolution,[status(thm)],[f22,f57])).
% 1.22/0.58 fof(f144,plain,(
% 1.22/0.58 ![X0,X1]: (in(sK0_skl(set_intersection2(X0,X1)),X0)|set_intersection2(X0,X1)=empty_set)),
% 1.22/0.58 inference(resolution,[status(thm)],[f76,f22])).
% 1.22/0.58 fof(f170,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sQ3_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f34,f130])).
% 1.22/0.58 fof(f172,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sQ3_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f34,f72])).
% 1.22/0.58 fof(f193,plain,(
% 1.22/0.58 disjoint(sK7_skl,sK6_skl)|~empty_set=empty_set|~sQ3_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f170,f35])).
% 1.22/0.58 fof(f195,plain,(
% 1.22/0.58 ![X0,X1]: (disjoint(X0,X1)|~set_intersection2(X1,X0)=empty_set)),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f17,f35])).
% 1.22/0.58 fof(f198,definition,(
% 1.22/0.58 sQ7_spl <=> (empty_set=empty_set)),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f200,plain,(
% 1.22/0.58 ~empty_set=empty_set|sQ7_spl),
% 1.22/0.58 inference(component_clause,[status(thm)],[f198])).
% 1.22/0.58 fof(f203,definition,(
% 1.22/0.58 sQ8_spl <=> (disjoint(sK7_skl,sK6_skl))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f204,plain,(
% 1.22/0.58 disjoint(sK7_skl,sK6_skl)|~sQ8_spl),
% 1.22/0.58 inference(component_clause,[status(thm)],[f203])).
% 1.22/0.58 fof(f206,plain,(
% 1.22/0.58 sQ8_spl|~sQ7_spl|~sQ3_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f193,f203,f198,f71])).
% 1.22/0.58 fof(f209,plain,(
% 1.22/0.58 $false|sQ7_spl),
% 1.22/0.58 inference(trivial_equality_resolution,[status(thm)],[f200])).
% 1.22/0.58 fof(f210,plain,(
% 1.22/0.58 sQ7_spl),
% 1.22/0.58 inference(contradiction_clause,[status(thm)],[f209])).
% 1.22/0.58 fof(f214,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sQ8_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f204,f34])).
% 1.22/0.58 fof(f222,plain,(
% 1.22/0.58 ![X0,X1]: (in(sK0_skl(set_intersection2(X0,X1)),X1)|set_intersection2(X0,X1)=empty_set)),
% 1.22/0.58 inference(resolution,[status(thm)],[f77,f22])).
% 1.22/0.58 fof(f228,plain,(
% 1.22/0.58 ![X0]: (in(sK8_skl,set_intersection2(X0,sK6_skl))|~in(sK8_skl,X0)|~sQ1_spl)),
% 1.22/0.58 inference(resolution,[status(thm)],[f78,f64])).
% 1.22/0.58 fof(f241,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sQ3_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f72,f34])).
% 1.22/0.58 fof(f283,plain,(
% 1.22/0.58 ![X0,X1,X2]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X2)|in(sK1_skl(set_intersection2(X0,X1),X2,set_intersection2(X0,X1)),X1))),
% 1.22/0.58 inference(resolution,[status(thm)],[f30,f77])).
% 1.22/0.58 fof(f287,plain,(
% 1.22/0.58 ![X0]: (empty_set=set_intersection2(empty_set,X0))),
% 1.22/0.58 inference(resolution,[status(thm)],[f30,f75])).
% 1.22/0.58 fof(f288,plain,(
% 1.22/0.58 ![X0,X1]: (empty_set=set_intersection2(X0,X1)|in(sK1_skl(empty_set,X1,X0),X0))),
% 1.22/0.58 inference(resolution,[status(thm)],[f30,f75])).
% 1.22/0.58 fof(f307,plain,(
% 1.22/0.58 ![X0,X1,X2,X3]: (X0=set_intersection2(X1,X2)|in(sK1_skl(X0,X2,X1),X0)|~sP0_prd(X1,X3)|~in(sK1_skl(X0,X2,X1),X3))),
% 1.22/0.58 inference(resolution,[status(thm)],[f30,f57])).
% 1.22/0.58 fof(f318,plain,(
% 1.22/0.58 ![X0]: (empty_set=set_intersection2(X0,empty_set))),
% 1.22/0.58 inference(resolution,[status(thm)],[f31,f75])).
% 1.22/0.58 fof(f319,plain,(
% 1.22/0.58 ![X0,X1]: (empty_set=set_intersection2(X0,X1)|in(sK1_skl(empty_set,X1,X0),X1))),
% 1.22/0.58 inference(resolution,[status(thm)],[f31,f75])).
% 1.22/0.58 fof(f341,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|set_intersection2(X0,X1)=empty_set|~sP0_prd(X0,set_intersection2(X0,X1)))),
% 1.22/0.58 inference(resolution,[status(thm)],[f144,f143])).
% 1.22/0.58 fof(f342,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|set_intersection2(X0,X1)=empty_set|~sP0_prd(set_intersection2(X0,X1),X0))),
% 1.22/0.58 inference(resolution,[status(thm)],[f144,f141])).
% 1.22/0.58 fof(f347,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~in(X0,sK0_skl(set_intersection2(X0,X1))))),
% 1.22/0.58 inference(resolution,[status(thm)],[f144,f16])).
% 1.22/0.58 fof(f354,plain,(
% 1.22/0.58 in(sK0_skl(empty_set),sK6_skl)|set_intersection2(sK6_skl,sK7_skl)=empty_set|~sQ3_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f172,f144])).
% 1.22/0.58 fof(f355,plain,(
% 1.22/0.58 in(sK0_skl(empty_set),sK7_skl)|set_intersection2(sK7_skl,sK6_skl)=empty_set|~sQ3_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f170,f144])).
% 1.22/0.58 fof(f359,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~sP0_prd(X0,set_intersection2(X0,X1)))),
% 1.22/0.58 inference(duplicate_literals_removal,[status(thm)],[f341])).
% 1.22/0.58 fof(f360,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~sP0_prd(set_intersection2(X0,X1),X0))),
% 1.22/0.58 inference(duplicate_literals_removal,[status(thm)],[f342])).
% 1.22/0.58 fof(f375,definition,(
% 1.22/0.58 sQ13_spl <=> (in(sK0_skl(empty_set),sK6_skl))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f378,definition,(
% 1.22/0.58 sQ14_spl <=> (set_intersection2(sK6_skl,sK7_skl)=empty_set)),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f381,plain,(
% 1.22/0.58 sQ13_spl|sQ14_spl|~sQ3_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f354,f375,f378,f71])).
% 1.22/0.58 fof(f382,definition,(
% 1.22/0.58 sQ15_spl <=> (in(sK0_skl(empty_set),sK7_skl))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f385,definition,(
% 1.22/0.58 sQ16_spl <=> (set_intersection2(sK7_skl,sK6_skl)=empty_set)),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f388,plain,(
% 1.22/0.58 sQ15_spl|sQ16_spl|~sQ3_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f355,f382,f385,f71])).
% 1.22/0.58 fof(f473,plain,(
% 1.22/0.58 ![X0]: (in(sK0_skl(empty_set),empty_set)|set_intersection2(empty_set,X0)=empty_set)),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f287,f144])).
% 1.22/0.58 fof(f475,plain,(
% 1.22/0.58 ![X0]: (disjoint(empty_set,X0)|~empty_set=empty_set)),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f287,f35])).
% 1.22/0.58 fof(f486,definition,(
% 1.22/0.58 sQ17_spl <=> (in(sK0_skl(empty_set),empty_set))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f487,plain,(
% 1.22/0.58 in(sK0_skl(empty_set),empty_set)|~sQ17_spl),
% 1.22/0.58 inference(component_clause,[status(thm)],[f486])).
% 1.22/0.58 fof(f489,definition,(
% 1.22/0.58 ![X0]: (sQ18_spl <=> (set_intersection2(empty_set,X0)=empty_set))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f492,plain,(
% 1.22/0.58 sQ17_spl|sQ18_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f473,f486,f489])).
% 1.22/0.58 fof(f493,definition,(
% 1.22/0.58 ![X0]: (sQ19_spl <=> (disjoint(empty_set,X0)))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f496,plain,(
% 1.22/0.58 sQ19_spl|~sQ7_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f475,f493,f198])).
% 1.22/0.58 fof(f497,plain,(
% 1.22/0.58 $false|~sQ17_spl),
% 1.22/0.58 inference(forward_subsumption_resolution,[status(thm)],[f487,f75])).
% 1.22/0.58 fof(f498,plain,(
% 1.22/0.58 ~sQ17_spl),
% 1.22/0.58 inference(contradiction_clause,[status(thm)],[f497])).
% 1.22/0.58 fof(f517,plain,(
% 1.22/0.58 ![X0]: (disjoint(X0,empty_set)|~empty_set=empty_set)),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f318,f35])).
% 1.22/0.58 fof(f528,definition,(
% 1.22/0.58 ![X0]: (sQ20_spl <=> (disjoint(X0,empty_set)))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f531,plain,(
% 1.22/0.58 sQ20_spl|~sQ7_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f517,f528,f198])).
% 1.22/0.58 fof(f545,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~sP0_prd(X0,set_intersection2(X1,X0)))),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f17,f359])).
% 1.22/0.58 fof(f585,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~sP0_prd(set_intersection2(X1,X0),X0))),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f17,f360])).
% 1.22/0.58 fof(f606,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~in(X0,sK0_skl(set_intersection2(X1,X0))))),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f17,f347])).
% 1.22/0.58 fof(f647,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|set_intersection2(X0,X1)=empty_set|~sP0_prd(X1,set_intersection2(X0,X1)))),
% 1.22/0.58 inference(resolution,[status(thm)],[f222,f143])).
% 1.22/0.58 fof(f648,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|set_intersection2(X0,X1)=empty_set|~sP0_prd(set_intersection2(X0,X1),X1))),
% 1.22/0.58 inference(resolution,[status(thm)],[f222,f141])).
% 1.22/0.58 fof(f653,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~in(X1,sK0_skl(set_intersection2(X0,X1))))),
% 1.22/0.58 inference(resolution,[status(thm)],[f222,f16])).
% 1.22/0.58 fof(f659,plain,(
% 1.22/0.58 ![X0]: (in(sK0_skl(empty_set),empty_set)|set_intersection2(X0,empty_set)=empty_set)),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f318,f222])).
% 1.22/0.58 fof(f663,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~sP0_prd(X1,set_intersection2(X0,X1)))),
% 1.22/0.58 inference(duplicate_literals_removal,[status(thm)],[f647])).
% 1.22/0.58 fof(f664,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~sP0_prd(set_intersection2(X0,X1),X1))),
% 1.22/0.58 inference(duplicate_literals_removal,[status(thm)],[f648])).
% 1.22/0.58 fof(f665,definition,(
% 1.22/0.58 ![X0]: (sQ23_spl <=> (set_intersection2(X0,empty_set)=empty_set))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f668,plain,(
% 1.22/0.58 sQ17_spl|sQ23_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f659,f486,f665])).
% 1.22/0.58 fof(f672,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~sP0_prd(X1,set_intersection2(X1,X0)))),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f17,f663])).
% 1.22/0.58 fof(f679,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~sP0_prd(set_intersection2(X1,X0),X1))),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f17,f664])).
% 1.22/0.58 fof(f735,definition,(
% 1.22/0.58 sQ24_spl <=> (empty_set=set_intersection2(empty_set,empty_set))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f815,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X0)=set_intersection2(set_intersection2(X0,X0),X1)|in(sK1_skl(X0,X1,set_intersection2(X0,X0)),X0))),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f38,f283])).
% 1.22/0.58 fof(f828,plain,(
% 1.22/0.58 ![X0,X1]: (X0=set_intersection2(set_intersection2(X0,X0),X1)|in(sK1_skl(X0,X1,set_intersection2(X0,X0)),X0))),
% 1.22/0.58 inference(forward_demodulation,[status(thm)],[f38,f815])).
% 1.22/0.58 fof(f829,plain,(
% 1.22/0.58 ![X0,X1]: (X0=set_intersection2(X0,X1)|in(sK1_skl(X0,X1,set_intersection2(X0,X0)),X0))),
% 1.22/0.58 inference(forward_demodulation,[status(thm)],[f38,f828])).
% 1.22/0.58 fof(f830,plain,(
% 1.22/0.58 ![X0,X1]: (X0=set_intersection2(X0,X1)|in(sK1_skl(X0,X1,X0),X0))),
% 1.22/0.58 inference(forward_demodulation,[status(thm)],[f38,f829])).
% 1.22/0.58 fof(f952,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~in(X1,sK0_skl(set_intersection2(X1,X0))))),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f17,f653])).
% 1.22/0.58 fof(f1142,plain,(
% 1.22/0.58 ![X0,X1]: (X0=set_intersection2(X0,X1)|X0=set_intersection2(X0,X1)|~in(sK1_skl(X0,X1,X0),X0)|~in(sK1_skl(X0,X1,X0),X1))),
% 1.22/0.58 inference(resolution,[status(thm)],[f830,f29])).
% 1.22/0.58 fof(f1158,plain,(
% 1.22/0.58 ![X0,X1]: (X0=set_intersection2(X0,X1)|~in(sK1_skl(X0,X1,X0),X0)|~in(sK1_skl(X0,X1,X0),X1))),
% 1.22/0.58 inference(duplicate_literals_removal,[status(thm)],[f1142])).
% 1.22/0.58 fof(f1159,plain,(
% 1.22/0.58 ![X0,X1]: (X0=set_intersection2(X0,X1)|~in(sK1_skl(X0,X1,X0),X1))),
% 1.22/0.58 inference(forward_subsumption_resolution,[status(thm)],[f1158,f830])).
% 1.22/0.58 fof(f1160,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1)|set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1))),
% 1.22/0.58 inference(resolution,[status(thm)],[f1159,f283])).
% 1.22/0.58 fof(f1164,plain,(
% 1.22/0.58 empty_set=set_intersection2(empty_set,empty_set)|empty_set=set_intersection2(empty_set,empty_set)),
% 1.22/0.58 inference(resolution,[status(thm)],[f1159,f288])).
% 1.22/0.58 fof(f1176,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X0,X1),X1))),
% 1.22/0.58 inference(duplicate_literals_removal,[status(thm)],[f1160])).
% 1.22/0.58 fof(f1178,plain,(
% 1.22/0.58 sQ24_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f1164,f735])).
% 1.22/0.58 fof(f1188,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(set_intersection2(X1,X0),X1))),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f17,f1176])).
% 1.22/0.58 fof(f1351,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(set_intersection2(X0,X1),X0)=empty_set|~sP0_prd(set_intersection2(X1,X0),set_intersection2(X0,X1)))),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f1188,f360])).
% 1.22/0.58 fof(f1353,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(set_intersection2(X0,X1),X0)=empty_set|~sP0_prd(set_intersection2(X0,X1),set_intersection2(X1,X0)))),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f1188,f359])).
% 1.22/0.58 fof(f1383,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~sP0_prd(set_intersection2(X0,X1),set_intersection2(X1,X0)))),
% 1.22/0.58 inference(forward_demodulation,[status(thm)],[f1188,f1351])).
% 1.22/0.58 fof(f1386,plain,(
% 1.22/0.58 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~sP0_prd(set_intersection2(X1,X0),set_intersection2(X0,X1)))),
% 1.22/0.58 inference(forward_demodulation,[status(thm)],[f1188,f1353])).
% 1.22/0.58 fof(f1906,plain,(
% 1.22/0.58 ![X0,X1]: (empty_set=set_intersection2(X0,X1)|in(sK1_skl(empty_set,X1,X0),empty_set)|~sP0_prd(X0,X1)|empty_set=set_intersection2(X0,X1))),
% 1.22/0.58 inference(resolution,[status(thm)],[f307,f319])).
% 1.22/0.58 fof(f1929,plain,(
% 1.22/0.58 ![X0,X1]: (empty_set=set_intersection2(X0,X1)|in(sK1_skl(empty_set,X1,X0),empty_set)|~sP0_prd(X0,X1))),
% 1.22/0.58 inference(duplicate_literals_removal,[status(thm)],[f1906])).
% 1.22/0.58 fof(f1930,plain,(
% 1.22/0.58 ![X0,X1]: (empty_set=set_intersection2(X0,X1)|~sP0_prd(X0,X1))),
% 1.22/0.58 inference(forward_subsumption_resolution,[status(thm)],[f1929,f75])).
% 1.22/0.58 fof(f1945,plain,(
% 1.22/0.58 empty_set=set_intersection2(sK4_skl,sK5_skl)|~sQ4_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f1930,f95])).
% 1.22/0.58 fof(f1947,plain,(
% 1.22/0.58 disjoint(sK5_skl,sK4_skl)|~sQ4_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f1945,f195])).
% 1.22/0.58 fof(f1991,plain,(
% 1.22/0.58 sQ5_spl|~sQ4_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f1947,f97,f94])).
% 1.22/0.58 fof(f2563,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sP0_prd(set_intersection2(sK6_skl,sK7_skl),empty_set)|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f1386])).
% 1.22/0.58 fof(f2564,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sP0_prd(empty_set,set_intersection2(sK6_skl,sK7_skl))|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f1386])).
% 1.22/0.58 fof(f2565,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sP0_prd(set_intersection2(sK6_skl,sK7_skl),empty_set)|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f1383])).
% 1.22/0.58 fof(f2566,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sP0_prd(empty_set,set_intersection2(sK6_skl,sK7_skl))|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f1383])).
% 1.22/0.58 fof(f2575,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~in(sK7_skl,sK0_skl(empty_set))|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f952])).
% 1.22/0.58 fof(f2576,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~in(sK6_skl,sK0_skl(empty_set))|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f653])).
% 1.22/0.58 fof(f2581,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sP0_prd(empty_set,sK7_skl)|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f679])).
% 1.22/0.58 fof(f2582,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sP0_prd(sK7_skl,empty_set)|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f672])).
% 1.22/0.58 fof(f2583,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sP0_prd(empty_set,sK6_skl)|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f664])).
% 1.22/0.58 fof(f2584,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sP0_prd(sK6_skl,empty_set)|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f663])).
% 1.22/0.58 fof(f2585,plain,(
% 1.22/0.58 in(sK0_skl(empty_set),sK6_skl)|set_intersection2(sK7_skl,sK6_skl)=empty_set|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f222])).
% 1.22/0.58 fof(f2586,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~in(sK6_skl,sK0_skl(empty_set))|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f606])).
% 1.22/0.58 fof(f2587,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~in(sK7_skl,sK0_skl(empty_set))|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f347])).
% 1.22/0.58 fof(f2588,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sP0_prd(empty_set,sK6_skl)|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f585])).
% 1.22/0.58 fof(f2589,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sP0_prd(sK6_skl,empty_set)|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f545])).
% 1.22/0.58 fof(f2590,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sP0_prd(empty_set,sK7_skl)|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f360])).
% 1.22/0.58 fof(f2592,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sP0_prd(sK7_skl,empty_set)|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f359])).
% 1.22/0.58 fof(f2593,plain,(
% 1.22/0.58 disjoint(sK6_skl,sK7_skl)|~empty_set=empty_set|~sQ8_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f214,f195])).
% 1.22/0.58 fof(f2607,definition,(
% 1.22/0.58 sQ43_spl <=> (sP0_prd(set_intersection2(sK6_skl,sK7_skl),empty_set))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f2610,plain,(
% 1.22/0.58 sQ16_spl|~sQ43_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2563,f385,f2607,f203])).
% 1.22/0.58 fof(f2611,definition,(
% 1.22/0.58 sQ44_spl <=> (sP0_prd(empty_set,set_intersection2(sK6_skl,sK7_skl)))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f2614,plain,(
% 1.22/0.58 sQ14_spl|~sQ44_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2564,f378,f2611,f203])).
% 1.22/0.58 fof(f2615,plain,(
% 1.22/0.58 sQ14_spl|~sQ43_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2565,f378,f2607,f203])).
% 1.22/0.58 fof(f2616,plain,(
% 1.22/0.58 sQ16_spl|~sQ44_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2566,f385,f2611,f203])).
% 1.22/0.58 fof(f2629,definition,(
% 1.22/0.58 sQ45_spl <=> (in(sK7_skl,sK0_skl(empty_set)))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f2632,plain,(
% 1.22/0.58 sQ14_spl|~sQ45_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2575,f378,f2629,f203])).
% 1.22/0.58 fof(f2633,definition,(
% 1.22/0.58 sQ46_spl <=> (in(sK6_skl,sK0_skl(empty_set)))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f2636,plain,(
% 1.22/0.58 sQ16_spl|~sQ46_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2576,f385,f2633,f203])).
% 1.22/0.58 fof(f2645,definition,(
% 1.22/0.58 sQ47_spl <=> (sP0_prd(empty_set,sK7_skl))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f2648,plain,(
% 1.22/0.58 sQ14_spl|~sQ47_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2581,f378,f2645,f203])).
% 1.22/0.58 fof(f2649,definition,(
% 1.22/0.58 sQ48_spl <=> (sP0_prd(sK7_skl,empty_set))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f2652,plain,(
% 1.22/0.58 sQ14_spl|~sQ48_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2582,f378,f2649,f203])).
% 1.22/0.58 fof(f2653,definition,(
% 1.22/0.58 sQ49_spl <=> (sP0_prd(empty_set,sK6_skl))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f2656,plain,(
% 1.22/0.58 sQ16_spl|~sQ49_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2583,f385,f2653,f203])).
% 1.22/0.58 fof(f2657,definition,(
% 1.22/0.58 sQ50_spl <=> (sP0_prd(sK6_skl,empty_set))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f2660,plain,(
% 1.22/0.58 sQ16_spl|~sQ50_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2584,f385,f2657,f203])).
% 1.22/0.58 fof(f2661,plain,(
% 1.22/0.58 sQ13_spl|sQ16_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2585,f375,f385,f203])).
% 1.22/0.58 fof(f2662,plain,(
% 1.22/0.58 sQ14_spl|~sQ46_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2586,f378,f2633,f203])).
% 1.22/0.58 fof(f2663,plain,(
% 1.22/0.58 sQ16_spl|~sQ45_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2587,f385,f2629,f203])).
% 1.22/0.58 fof(f2664,plain,(
% 1.22/0.58 sQ14_spl|~sQ49_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2588,f378,f2653,f203])).
% 1.22/0.58 fof(f2665,plain,(
% 1.22/0.58 sQ14_spl|~sQ50_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2589,f378,f2657,f203])).
% 1.22/0.58 fof(f2666,plain,(
% 1.22/0.58 sQ16_spl|~sQ47_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2590,f385,f2645,f203])).
% 1.22/0.58 fof(f2669,plain,(
% 1.22/0.58 sQ16_spl|~sQ48_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2592,f385,f2649,f203])).
% 1.22/0.58 fof(f2670,plain,(
% 1.22/0.58 sQ3_spl|~sQ7_spl|~sQ8_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2593,f71,f198,f203])).
% 1.22/0.58 fof(f2685,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sP0_prd(set_intersection2(sK7_skl,sK6_skl),empty_set)|~sQ3_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f241,f1386])).
% 1.22/0.58 fof(f2686,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sP0_prd(empty_set,set_intersection2(sK7_skl,sK6_skl))|~sQ3_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f241,f1386])).
% 1.22/0.58 fof(f2687,plain,(
% 1.22/0.58 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sP0_prd(set_intersection2(sK7_skl,sK6_skl),empty_set)|~sQ3_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f241,f1383])).
% 1.22/0.58 fof(f2688,plain,(
% 1.22/0.58 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sP0_prd(empty_set,set_intersection2(sK7_skl,sK6_skl))|~sQ3_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f241,f1383])).
% 1.22/0.58 fof(f2707,plain,(
% 1.22/0.58 in(sK0_skl(empty_set),sK7_skl)|set_intersection2(sK6_skl,sK7_skl)=empty_set|~sQ3_spl),
% 1.22/0.58 inference(paramodulation,[status(thm)],[f241,f222])).
% 1.22/0.58 fof(f2731,definition,(
% 1.22/0.58 sQ51_spl <=> (sP0_prd(set_intersection2(sK7_skl,sK6_skl),empty_set))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f2734,plain,(
% 1.22/0.58 sQ14_spl|~sQ51_spl|~sQ3_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2685,f378,f2731,f71])).
% 1.22/0.58 fof(f2735,definition,(
% 1.22/0.58 sQ52_spl <=> (sP0_prd(empty_set,set_intersection2(sK7_skl,sK6_skl)))),
% 1.22/0.58 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 1.22/0.58 fof(f2738,plain,(
% 1.22/0.58 sQ16_spl|~sQ52_spl|~sQ3_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2686,f385,f2735,f71])).
% 1.22/0.58 fof(f2739,plain,(
% 1.22/0.58 sQ16_spl|~sQ51_spl|~sQ3_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2687,f385,f2731,f71])).
% 1.22/0.58 fof(f2740,plain,(
% 1.22/0.58 sQ14_spl|~sQ52_spl|~sQ3_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2688,f378,f2735,f71])).
% 1.22/0.58 fof(f2767,plain,(
% 1.22/0.58 sQ15_spl|sQ14_spl|~sQ3_spl),
% 1.22/0.58 inference(split_clause,[status(thm)],[f2707,f382,f378,f71])).
% 1.22/0.58 fof(f4077,plain,(
% 1.22/0.58 in(sK8_skl,set_intersection2(sK7_skl,sK6_skl))|~sQ1_spl|~sQ2_spl),
% 1.22/0.58 inference(resolution,[status(thm)],[f228,f68])).
% 1.22/0.58 fof(f4079,plain,(
% 1.22/0.58 in(sK8_skl,empty_set)|~sQ8_spl|~sQ1_spl|~sQ2_spl),
% 1.22/0.58 inference(forward_demodulation,[status(thm)],[f214,f4077])).
% 1.22/0.58 fof(f4080,plain,(
% 1.22/0.58 $false|~sQ8_spl|~sQ1_spl|~sQ2_spl),
% 1.22/0.58 inference(forward_subsumption_resolution,[status(thm)],[f4079,f75])).
% 1.22/0.58 fof(f4081,plain,(
% 1.22/0.58 ~sQ8_spl|~sQ1_spl|~sQ2_spl),
% 1.22/0.58 inference(contradiction_clause,[status(thm)],[f4080])).
% 1.22/0.58 fof(f4082,plain,(
% 1.22/0.58 $false),
% 1.22/0.58 inference(sat_refutation,[status(thm)],[f66,f70,f74,f100,f119,f206,f210,f381,f388,f492,f496,f498,f531,f668,f1178,f1991,f2610,f2614,f2615,f2616,f2632,f2636,f2648,f2652,f2656,f2660,f2661,f2662,f2663,f2664,f2665,f2666,f2669,f2670,f2734,f2738,f2739,f2740,f2767,f4081])).
% 1.22/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 1.22/0.61 % Elapsed time: 0.244435 seconds
% 1.22/0.61 % CPU time: 1.650320 seconds
% 1.22/0.61 % Total memory used: 123.614 MB
% 1.22/0.61 % Net memory used: 120.695 MB
%------------------------------------------------------------------------------