%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU119+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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 0.18s 0.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU119+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.52 % Computer : n008.cluster.edu
% 0.11/0.52 % Model : x86_64 x86_64
% 0.11/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.52 % Memory : 8046.5625MB
% 0.11/0.52 % OS : Linux 6.8.0-71-generic
% 0.11/0.52 % CPULimit : 300
% 0.11/0.52 % WCLimit : 300
% 0.11/0.52 % DateTime : Mon Sep 21 05:52:09 UTC 2026
% 0.11/0.52 % CPUTime :
% 0.11/0.53 % Drodi V4.1.1
% 0.18/0.76 % Refutation found
% 0.18/0.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.76 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.76 fof(f2,axiom,(
% 0.18/0.76 (! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) )),
% 0.18/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.76 fof(f3,axiom,(
% 0.18/0.76 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 0.18/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.76 fof(f4,axiom,(
% 0.18/0.76 (! [A,B,C] :( C = set_intersection2(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)& in(D,B) ) ) )) )),
% 0.18/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.76 fof(f5,axiom,(
% 0.18/0.76 (! [A,B] :( disjoint(A,B)<=> set_intersection2(A,B) = empty_set ) )),
% 0.18/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.76 fof(f9,axiom,(
% 0.18/0.76 (! [A,B] : set_intersection2(A,A) = A )),
% 0.18/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.76 fof(f12,axiom,(
% 0.18/0.76 (! [A,B] :( disjoint(A,B)=> disjoint(B,A) ) )),
% 0.18/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.76 fof(f13,conjecture,(
% 0.18/0.76 (! [A,B] :( ~ ( ~ disjoint(A,B)& (! [C] :~ ( in(C,A)& in(C,B) ) ))& ~ ( (? [C] :( in(C,A)& in(C,B) ))& disjoint(A,B) ) ) )),
% 0.18/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.76 fof(f14,negated_conjecture,(
% 0.18/0.76 ~((! [A,B] :( ~ ( ~ disjoint(A,B)& (! [C] :~ ( in(C,A)& in(C,B) ) ))& ~ ( (? [C] :( in(C,A)& in(C,B) ))& disjoint(A,B) ) ) ))),
% 0.18/0.76 inference(negated_conjecture,[status(cth)],[f13])).
% 0.18/0.76 fof(f17,plain,(
% 0.18/0.76 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,X0))),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f2])).
% 0.18/0.76 fof(f18,plain,(
% 0.18/0.76 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 0.18/0.76 inference(NNF_transformation,[status(thm)],[f3])).
% 0.18/0.76 fof(f19,plain,(
% 0.18/0.76 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 0.18/0.76 inference(miniscoping,[status(thm)],[f18])).
% 0.18/0.76 fof(f20,plain,(
% 0.18/0.76 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK0_skl(A),A)))),
% 0.18/0.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f19])).
% 0.18/0.76 fof(f21,plain,(
% 0.18/0.76 ![X0,X1]: (~X0=empty_set|~in(X1,X0))),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f20])).
% 0.18/0.76 fof(f22,plain,(
% 0.18/0.76 ![X0]: (X0=empty_set|in(sK0_skl(X0),X0))),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f20])).
% 0.18/0.76 fof(f23,plain,(
% 0.18/0.76 ![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)))))))),
% 0.18/0.76 inference(NNF_transformation,[status(thm)],[f4])).
% 0.18/0.76 fof(f24,plain,(
% 0.18/0.76 (![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)))))))),
% 0.18/0.76 inference(miniscoping,[status(thm)],[f23])).
% 0.18/0.76 fof(f25,plain,(
% 0.18/0.76 (![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))))))),
% 0.18/0.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(C,B,A))],[f24])).
% 0.18/0.76 fof(f26,plain,(
% 0.18/0.76 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|~in(X3,X0)|in(X3,X1))),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f25])).
% 0.18/0.76 fof(f28,plain,(
% 0.18/0.76 ![X0,X1,X2,X3]: (~X0=set_intersection2(X1,X2)|in(X3,X0)|~in(X3,X1)|~in(X3,X2))),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f25])).
% 0.18/0.76 fof(f30,plain,(
% 0.18/0.76 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|in(sK1_skl(X0,X2,X1),X0)|in(sK1_skl(X0,X2,X1),X1))),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f25])).
% 0.18/0.76 fof(f31,plain,(
% 0.18/0.76 ![X0,X1,X2]: (X0=set_intersection2(X1,X2)|in(sK1_skl(X0,X2,X1),X0)|in(sK1_skl(X0,X2,X1),X2))),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f25])).
% 0.18/0.76 fof(f32,plain,(
% 0.18/0.76 ![A,B]: ((~disjoint(A,B)|set_intersection2(A,B)=empty_set)&(disjoint(A,B)|~set_intersection2(A,B)=empty_set))),
% 0.18/0.76 inference(NNF_transformation,[status(thm)],[f5])).
% 0.18/0.76 fof(f33,plain,(
% 0.18/0.76 (![A,B]: (~disjoint(A,B)|set_intersection2(A,B)=empty_set))&(![A,B]: (disjoint(A,B)|~set_intersection2(A,B)=empty_set))),
% 0.18/0.76 inference(miniscoping,[status(thm)],[f32])).
% 0.18/0.76 fof(f34,plain,(
% 0.18/0.76 ![X0,X1]: (~disjoint(X0,X1)|set_intersection2(X0,X1)=empty_set)),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f33])).
% 0.18/0.76 fof(f35,plain,(
% 0.18/0.76 ![X0,X1]: (disjoint(X0,X1)|~set_intersection2(X0,X1)=empty_set)),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f33])).
% 0.18/0.76 fof(f37,plain,(
% 0.18/0.76 ![A]: set_intersection2(A,A)=A),
% 0.18/0.76 inference(miniscoping,[status(thm)],[f9])).
% 0.18/0.76 fof(f38,plain,(
% 0.18/0.76 ![X0]: (set_intersection2(X0,X0)=X0)),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f37])).
% 0.18/0.76 fof(f43,plain,(
% 0.18/0.76 ![A,B]: (~disjoint(A,B)|disjoint(B,A))),
% 0.18/0.76 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.18/0.76 fof(f44,plain,(
% 0.18/0.76 ![X0,X1]: (~disjoint(X0,X1)|disjoint(X1,X0))),
% 0.18/0.76 inference(cnf_transformation,[status(thm)],[f43])).
% 0.18/0.76 fof(f45,plain,(
% 0.18/0.76 (?[A,B]: ((~disjoint(A,B)&(![C]: (~in(C,A)|~in(C,B))))|((?[C]: (in(C,A)&in(C,B)))&disjoint(A,B))))),
% 0.18/0.76 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.18/0.77 fof(f46,definition,(
% 0.18/0.77 ![A,B]: (sP0_prd(B,A)<=>(~disjoint(A,B)&(![C]: (~in(C,A)|~in(C,B)))))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.18/0.77 fof(f47,plain,(
% 0.18/0.77 ?[A,B]: (sP0_prd(B,A)|((?[C]: (in(C,A)&in(C,B)))&disjoint(A,B)))),
% 0.18/0.77 inference(formula_renaming,[status(thm)],[f45,f46])).
% 0.18/0.77 fof(f48,plain,(
% 0.18/0.77 (?[A,B]: sP0_prd(B,A))|(?[A,B]: ((?[C]: (in(C,A)&in(C,B)))&disjoint(A,B)))),
% 0.18/0.77 inference(miniscoping,[status(thm)],[f47])).
% 0.18/0.77 fof(f49,plain,(
% 0.18/0.77 sP0_prd(sK5_skl,sK4_skl)|((in(sK8_skl,sK6_skl)&in(sK8_skl,sK7_skl))&disjoint(sK6_skl,sK7_skl))),
% 0.18/0.77 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])).
% 0.18/0.77 fof(f50,plain,(
% 0.18/0.77 sP0_prd(sK5_skl,sK4_skl)|in(sK8_skl,sK6_skl)),
% 0.18/0.77 inference(cnf_transformation,[status(thm)],[f49])).
% 0.18/0.77 fof(f51,plain,(
% 0.18/0.77 sP0_prd(sK5_skl,sK4_skl)|in(sK8_skl,sK7_skl)),
% 0.18/0.77 inference(cnf_transformation,[status(thm)],[f49])).
% 0.18/0.77 fof(f52,plain,(
% 0.18/0.77 sP0_prd(sK5_skl,sK4_skl)|disjoint(sK6_skl,sK7_skl)),
% 0.18/0.77 inference(cnf_transformation,[status(thm)],[f49])).
% 0.18/0.77 fof(f53,plain,(
% 0.18/0.77 ![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))))))),
% 0.18/0.77 inference(NNF_transformation,[status(thm)],[f46])).
% 0.18/0.77 fof(f54,plain,(
% 0.18/0.77 (![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))))))),
% 0.18/0.77 inference(miniscoping,[status(thm)],[f53])).
% 0.18/0.77 fof(f55,plain,(
% 0.18/0.77 (![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)))))),
% 0.18/0.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(C,sK9_skl(B,A))],[f54])).
% 0.18/0.77 fof(f56,plain,(
% 0.18/0.77 ![X0,X1]: (~sP0_prd(X0,X1)|~disjoint(X1,X0))),
% 0.18/0.77 inference(cnf_transformation,[status(thm)],[f55])).
% 0.18/0.77 fof(f57,plain,(
% 0.18/0.77 ![X0,X1,X2]: (~sP0_prd(X0,X1)|~in(X2,X1)|~in(X2,X0))),
% 0.18/0.77 inference(cnf_transformation,[status(thm)],[f55])).
% 0.18/0.77 fof(f58,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(X0,X1)|disjoint(X1,X0)|in(sK9_skl(X0,X1),X1))),
% 0.18/0.77 inference(cnf_transformation,[status(thm)],[f55])).
% 0.18/0.77 fof(f59,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(X0,X1)|disjoint(X1,X0)|in(sK9_skl(X0,X1),X0))),
% 0.18/0.77 inference(cnf_transformation,[status(thm)],[f55])).
% 0.18/0.77 fof(f60,definition,(
% 0.18/0.77 sQ0_spl <=> (sP0_prd(sK5_skl,sK4_skl))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f61,plain,(
% 0.18/0.77 sP0_prd(sK5_skl,sK4_skl)|~sQ0_spl),
% 0.18/0.77 inference(component_clause,[status(thm)],[f60])).
% 0.18/0.77 fof(f63,definition,(
% 0.18/0.77 sQ1_spl <=> (in(sK8_skl,sK6_skl))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f64,plain,(
% 0.18/0.77 in(sK8_skl,sK6_skl)|~sQ1_spl),
% 0.18/0.77 inference(component_clause,[status(thm)],[f63])).
% 0.18/0.77 fof(f66,plain,(
% 0.18/0.77 sQ0_spl|sQ1_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f50,f60,f63])).
% 0.18/0.77 fof(f67,definition,(
% 0.18/0.77 sQ2_spl <=> (in(sK8_skl,sK7_skl))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f68,plain,(
% 0.18/0.77 in(sK8_skl,sK7_skl)|~sQ2_spl),
% 0.18/0.77 inference(component_clause,[status(thm)],[f67])).
% 0.18/0.77 fof(f70,plain,(
% 0.18/0.77 sQ0_spl|sQ2_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f51,f60,f67])).
% 0.18/0.77 fof(f71,definition,(
% 0.18/0.77 sQ3_spl <=> (disjoint(sK6_skl,sK7_skl))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f72,plain,(
% 0.18/0.77 disjoint(sK6_skl,sK7_skl)|~sQ3_spl),
% 0.18/0.77 inference(component_clause,[status(thm)],[f71])).
% 0.18/0.77 fof(f74,plain,(
% 0.18/0.77 sQ0_spl|sQ3_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f52,f60,f71])).
% 0.18/0.77 fof(f76,plain,(
% 0.18/0.77 ![X0,X1,X2]: (sP0_prd(X0,X1)|disjoint(X1,X0)|~sP0_prd(X1,X2)|~in(sK9_skl(X0,X1),X2))),
% 0.18/0.77 inference(resolution,[status(thm)],[f58,f57])).
% 0.18/0.77 fof(f85,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(X0,X1)|disjoint(X1,X0)|~sP0_prd(X1,X0)|sP0_prd(X0,X1)|disjoint(X1,X0))),
% 0.18/0.77 inference(resolution,[status(thm)],[f76,f59])).
% 0.18/0.77 fof(f87,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(X0,X1)|disjoint(X1,X0)|~sP0_prd(X1,X0))),
% 0.18/0.77 inference(duplicate_literals_removal,[status(thm)],[f85])).
% 0.18/0.77 fof(f89,plain,(
% 0.18/0.77 sP0_prd(sK4_skl,sK5_skl)|disjoint(sK5_skl,sK4_skl)|~sQ0_spl),
% 0.18/0.77 inference(resolution,[status(thm)],[f87,f61])).
% 0.18/0.77 fof(f90,definition,(
% 0.18/0.77 sQ4_spl <=> (sP0_prd(sK4_skl,sK5_skl))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f91,plain,(
% 0.18/0.77 sP0_prd(sK4_skl,sK5_skl)|~sQ4_spl),
% 0.18/0.77 inference(component_clause,[status(thm)],[f90])).
% 0.18/0.77 fof(f93,definition,(
% 0.18/0.77 sQ5_spl <=> (disjoint(sK5_skl,sK4_skl))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f94,plain,(
% 0.18/0.77 disjoint(sK5_skl,sK4_skl)|~sQ5_spl),
% 0.18/0.77 inference(component_clause,[status(thm)],[f93])).
% 0.18/0.77 fof(f96,plain,(
% 0.18/0.77 sQ4_spl|sQ5_spl|~sQ0_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f89,f90,f93,f60])).
% 0.18/0.77 fof(f102,plain,(
% 0.18/0.77 disjoint(sK4_skl,sK5_skl)|~sQ5_spl),
% 0.18/0.77 inference(resolution,[status(thm)],[f94,f44])).
% 0.18/0.77 fof(f105,plain,(
% 0.18/0.77 ~sP0_prd(sK5_skl,sK4_skl)|~sQ5_spl),
% 0.18/0.77 inference(resolution,[status(thm)],[f102,f56])).
% 0.18/0.77 fof(f106,plain,(
% 0.18/0.77 $false|~sQ0_spl|~sQ5_spl),
% 0.18/0.77 inference(forward_subsumption_resolution,[status(thm)],[f105,f61])).
% 0.18/0.77 fof(f107,plain,(
% 0.18/0.77 ~sQ0_spl|~sQ5_spl),
% 0.18/0.77 inference(contradiction_clause,[status(thm)],[f106])).
% 0.18/0.77 fof(f118,plain,(
% 0.18/0.77 disjoint(sK7_skl,sK6_skl)|~sQ3_spl),
% 0.18/0.77 inference(resolution,[status(thm)],[f72,f44])).
% 0.18/0.77 fof(f132,plain,(
% 0.18/0.77 ![X0,X1]: (~X0=empty_set|sP0_prd(X0,X1)|disjoint(X1,X0))),
% 0.18/0.77 inference(resolution,[status(thm)],[f21,f59])).
% 0.18/0.77 fof(f133,plain,(
% 0.18/0.77 ![X0,X1]: (~X0=empty_set|sP0_prd(X1,X0)|disjoint(X0,X1))),
% 0.18/0.77 inference(resolution,[status(thm)],[f21,f58])).
% 0.18/0.77 fof(f151,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(set_intersection2(empty_set,empty_set),X0)|disjoint(X0,set_intersection2(empty_set,empty_set)))),
% 0.18/0.77 inference(resolution,[status(thm)],[f132,f38])).
% 0.18/0.77 fof(f153,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(empty_set,X0)|disjoint(X0,set_intersection2(empty_set,empty_set)))),
% 0.18/0.77 inference(forward_demodulation,[status(thm)],[f38,f151])).
% 0.18/0.77 fof(f154,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(empty_set,X0)|disjoint(X0,empty_set))),
% 0.18/0.77 inference(forward_demodulation,[status(thm)],[f38,f153])).
% 0.18/0.77 fof(f155,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(empty_set,X0)|disjoint(empty_set,X0))),
% 0.18/0.77 inference(resolution,[status(thm)],[f154,f44])).
% 0.18/0.77 fof(f159,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(X0,set_intersection2(empty_set,empty_set))|disjoint(set_intersection2(empty_set,empty_set),X0))),
% 0.18/0.77 inference(resolution,[status(thm)],[f133,f38])).
% 0.18/0.77 fof(f161,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(X0,empty_set)|disjoint(set_intersection2(empty_set,empty_set),X0))),
% 0.18/0.77 inference(forward_demodulation,[status(thm)],[f38,f159])).
% 0.18/0.77 fof(f162,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(X0,empty_set)|disjoint(empty_set,X0))),
% 0.18/0.77 inference(forward_demodulation,[status(thm)],[f38,f161])).
% 0.18/0.77 fof(f163,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(X0,empty_set)|disjoint(X0,empty_set))),
% 0.18/0.77 inference(resolution,[status(thm)],[f162,f44])).
% 0.18/0.77 fof(f166,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(X0,empty_set)|~sP0_prd(empty_set,X0))),
% 0.18/0.77 inference(resolution,[status(thm)],[f163,f56])).
% 0.18/0.77 fof(f174,plain,(
% 0.18/0.77 ![X0]: (set_intersection2(empty_set,X0)=empty_set|sP0_prd(X0,empty_set))),
% 0.18/0.77 inference(resolution,[status(thm)],[f34,f162])).
% 0.18/0.77 fof(f175,plain,(
% 0.18/0.77 ![X0]: (set_intersection2(empty_set,X0)=empty_set|sP0_prd(empty_set,X0))),
% 0.18/0.77 inference(resolution,[status(thm)],[f34,f155])).
% 0.18/0.77 fof(f177,plain,(
% 0.18/0.77 set_intersection2(sK7_skl,sK6_skl)=empty_set|~sQ3_spl),
% 0.18/0.77 inference(resolution,[status(thm)],[f34,f118])).
% 0.18/0.77 fof(f181,plain,(
% 0.18/0.77 ![X0]: (set_intersection2(X0,empty_set)=empty_set|sP0_prd(empty_set,X0))),
% 0.18/0.77 inference(resolution,[status(thm)],[f34,f154])).
% 0.18/0.77 fof(f183,plain,(
% 0.18/0.77 set_intersection2(sK6_skl,sK7_skl)=empty_set|~sQ3_spl),
% 0.18/0.77 inference(forward_demodulation,[status(thm)],[f17,f177])).
% 0.18/0.77 fof(f201,plain,(
% 0.18/0.77 ![X0,X1]: (disjoint(X0,X1)|~set_intersection2(X1,X0)=empty_set)),
% 0.18/0.77 inference(paramodulation,[status(thm)],[f17,f35])).
% 0.18/0.77 fof(f204,definition,(
% 0.18/0.77 sQ7_spl <=> (empty_set=empty_set)),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f225,plain,(
% 0.18/0.77 set_intersection2(empty_set,empty_set)=empty_set|sP0_prd(empty_set,empty_set)),
% 0.18/0.77 inference(resolution,[status(thm)],[f174,f166])).
% 0.18/0.77 fof(f231,definition,(
% 0.18/0.77 sQ8_spl <=> (set_intersection2(empty_set,empty_set)=empty_set)),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f234,definition,(
% 0.18/0.77 sQ9_spl <=> (sP0_prd(empty_set,empty_set))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f235,plain,(
% 0.18/0.77 sP0_prd(empty_set,empty_set)|~sQ9_spl),
% 0.18/0.77 inference(component_clause,[status(thm)],[f234])).
% 0.18/0.77 fof(f237,plain,(
% 0.18/0.77 sQ8_spl|sQ9_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f225,f231,f234])).
% 0.18/0.77 fof(f239,definition,(
% 0.18/0.77 ![X0]: (sQ10_spl <=> (sP0_prd(empty_set,X0)|disjoint(X0,empty_set)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f243,definition,(
% 0.18/0.77 ![X0]: (sQ11_spl <=> (sP0_prd(X0,empty_set)|disjoint(empty_set,X0)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f269,plain,(
% 0.18/0.77 ![X0,X1,X2]: (~in(X0,set_intersection2(X1,X2))|in(X0,X2))),
% 0.18/0.77 inference(resolution,[status(thm)],[f26,f17])).
% 0.18/0.77 fof(f311,plain,(
% 0.18/0.77 ![X0,X1]: (in(sK0_skl(set_intersection2(X0,X1)),X1)|set_intersection2(X0,X1)=empty_set)),
% 0.18/0.77 inference(resolution,[status(thm)],[f269,f22])).
% 0.18/0.77 fof(f312,plain,(
% 0.18/0.77 ![X0,X1,X2]: (in(sK9_skl(set_intersection2(X0,X1),X2),X1)|sP0_prd(set_intersection2(X0,X1),X2)|disjoint(X2,set_intersection2(X0,X1)))),
% 0.18/0.77 inference(resolution,[status(thm)],[f269,f59])).
% 0.18/0.77 fof(f313,plain,(
% 0.18/0.77 ![X0,X1,X2]: (in(sK9_skl(X0,set_intersection2(X1,X2)),X2)|sP0_prd(X0,set_intersection2(X1,X2))|disjoint(set_intersection2(X1,X2),X0))),
% 0.18/0.77 inference(resolution,[status(thm)],[f269,f58])).
% 0.18/0.77 fof(f322,plain,(
% 0.18/0.77 ![X0,X1,X2]: (sP0_prd(set_intersection2(X0,X1),X2)|disjoint(X2,set_intersection2(X0,X1))|~X1=empty_set)),
% 0.18/0.77 inference(resolution,[status(thm)],[f312,f21])).
% 0.18/0.77 fof(f337,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(set_intersection2(X0,set_intersection2(empty_set,empty_set)),X1)|disjoint(X1,set_intersection2(X0,set_intersection2(empty_set,empty_set))))),
% 0.18/0.77 inference(resolution,[status(thm)],[f322,f38])).
% 0.18/0.77 fof(f339,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(set_intersection2(X0,empty_set),X1)|disjoint(X1,set_intersection2(X0,set_intersection2(empty_set,empty_set))))),
% 0.18/0.77 inference(forward_demodulation,[status(thm)],[f38,f337])).
% 0.18/0.77 fof(f340,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(set_intersection2(X0,empty_set),X1)|disjoint(X1,set_intersection2(X0,empty_set)))),
% 0.18/0.77 inference(forward_demodulation,[status(thm)],[f38,f339])).
% 0.18/0.77 fof(f342,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(set_intersection2(X0,empty_set),X1)|disjoint(set_intersection2(X0,empty_set),X1))),
% 0.18/0.77 inference(resolution,[status(thm)],[f340,f44])).
% 0.18/0.77 fof(f350,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(set_intersection2(X0,empty_set),X1)|~sP0_prd(X1,set_intersection2(X0,empty_set)))),
% 0.18/0.77 inference(resolution,[status(thm)],[f342,f56])).
% 0.18/0.77 fof(f364,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(set_intersection2(X0,empty_set),X1)|~sP0_prd(X1,set_intersection2(empty_set,X0)))),
% 0.18/0.77 inference(paramodulation,[status(thm)],[f17,f350])).
% 0.18/0.77 fof(f435,plain,(
% 0.18/0.77 ![X0,X1]: (set_intersection2(X0,X1)=empty_set|~X1=empty_set)),
% 0.18/0.77 inference(resolution,[status(thm)],[f311,f21])).
% 0.18/0.77 fof(f447,plain,(
% 0.18/0.77 ![X0]: (set_intersection2(X0,set_intersection2(empty_set,empty_set))=empty_set)),
% 0.18/0.77 inference(resolution,[status(thm)],[f435,f38])).
% 0.18/0.77 fof(f449,plain,(
% 0.18/0.77 ![X0]: (set_intersection2(X0,empty_set)=empty_set)),
% 0.18/0.77 inference(forward_demodulation,[status(thm)],[f38,f447])).
% 0.18/0.77 fof(f450,plain,(
% 0.18/0.77 ![X0,X1]: (sP0_prd(empty_set,X0)|~sP0_prd(X0,set_intersection2(empty_set,X1)))),
% 0.18/0.77 inference(backward_demodulation,[status(thm)],[f449,f364])).
% 0.18/0.77 fof(f457,plain,(
% 0.18/0.77 ![X0]: (empty_set=empty_set|sP0_prd(empty_set,X0))),
% 0.18/0.77 inference(backward_demodulation,[status(thm)],[f449,f181])).
% 0.18/0.77 fof(f460,plain,(
% 0.18/0.77 ![X0]: (disjoint(X0,empty_set))),
% 0.18/0.77 inference(resolution,[status(thm)],[f449,f35])).
% 0.18/0.77 fof(f469,plain,(
% 0.18/0.77 ![X0]: (set_intersection2(empty_set,X0)=empty_set)),
% 0.18/0.77 inference(paramodulation,[status(thm)],[f17,f449])).
% 0.18/0.77 fof(f481,plain,(
% 0.18/0.77 ![X0]: (disjoint(empty_set,X0)|~empty_set=empty_set)),
% 0.18/0.77 inference(paramodulation,[status(thm)],[f449,f201])).
% 0.18/0.77 fof(f482,plain,(
% 0.18/0.77 ![X0]: (disjoint(X0,empty_set)|~empty_set=empty_set)),
% 0.18/0.77 inference(paramodulation,[status(thm)],[f449,f35])).
% 0.18/0.77 fof(f489,definition,(
% 0.18/0.77 ![X0]: (sQ12_spl <=> (sP0_prd(empty_set,X0)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f490,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(empty_set,X0)|~sQ12_spl)),
% 0.18/0.77 inference(component_clause,[status(thm)],[f489])).
% 0.18/0.77 fof(f492,plain,(
% 0.18/0.77 sQ7_spl|sQ12_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f457,f204,f489])).
% 0.18/0.77 fof(f511,definition,(
% 0.18/0.77 ![X0]: (sQ15_spl <=> (set_intersection2(X0,empty_set)=empty_set))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f515,definition,(
% 0.18/0.77 ![X0,X1]: (sQ16_spl <=> (sP0_prd(set_intersection2(X0,empty_set),X1)|disjoint(X1,set_intersection2(X0,empty_set))))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f524,definition,(
% 0.18/0.77 ![X0]: (sQ17_spl <=> (disjoint(empty_set,X0)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f527,plain,(
% 0.18/0.77 sQ17_spl|~sQ7_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f481,f524,f204])).
% 0.18/0.77 fof(f528,definition,(
% 0.18/0.77 ![X0]: (sQ18_spl <=> (disjoint(X0,empty_set)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f531,plain,(
% 0.18/0.77 sQ18_spl|~sQ7_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f482,f528,f204])).
% 0.18/0.77 fof(f564,plain,(
% 0.18/0.77 ![X0,X1,X2,X3]: (X0=set_intersection2(X1,X2)|in(sK1_skl(X0,X2,X1),X0)|~sP0_prd(X3,X1)|~in(sK1_skl(X0,X2,X1),X3))),
% 0.18/0.77 inference(resolution,[status(thm)],[f30,f57])).
% 0.18/0.77 fof(f598,definition,(
% 0.18/0.77 ![X0]: (sQ19_spl <=> (empty_set=set_intersection2(empty_set,X0)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f641,plain,(
% 0.18/0.77 ![X0]: (sP0_prd(empty_set,empty_set)|set_intersection2(empty_set,set_intersection2(empty_set,X0))=empty_set)),
% 0.18/0.77 inference(resolution,[status(thm)],[f450,f175])).
% 0.18/0.77 fof(f646,definition,(
% 0.18/0.77 ![X0]: (sQ20_spl <=> (set_intersection2(empty_set,set_intersection2(empty_set,X0))=empty_set))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f647,plain,(
% 0.18/0.77 ![X0]: (set_intersection2(empty_set,set_intersection2(empty_set,X0))=empty_set|~sQ20_spl)),
% 0.18/0.77 inference(component_clause,[status(thm)],[f646])).
% 0.18/0.77 fof(f649,plain,(
% 0.18/0.77 sQ9_spl|sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f641,f234,f646])).
% 0.18/0.77 fof(f676,plain,(
% 0.18/0.77 ![X0,X1,X2]: (~X0=empty_set|in(X1,X0)|~in(X1,empty_set)|~in(X1,set_intersection2(empty_set,X2))|~sQ20_spl)),
% 0.18/0.77 inference(paramodulation,[status(thm)],[f647,f28])).
% 0.18/0.77 fof(f679,plain,(
% 0.18/0.77 ![X0]: (disjoint(set_intersection2(empty_set,X0),empty_set)|~empty_set=empty_set|~sQ20_spl)),
% 0.18/0.77 inference(paramodulation,[status(thm)],[f647,f201])).
% 0.18/0.77 fof(f680,plain,(
% 0.18/0.77 ![X0]: (disjoint(empty_set,set_intersection2(empty_set,X0))|~empty_set=empty_set|~sQ20_spl)),
% 0.18/0.77 inference(paramodulation,[status(thm)],[f647,f35])).
% 0.18/0.77 fof(f700,plain,(
% 0.18/0.77 ![X0,X1,X2]: (~X0=empty_set|~in(X1,empty_set)|~in(X1,set_intersection2(empty_set,X2))|~sQ20_spl)),
% 0.18/0.77 inference(forward_subsumption_resolution,[status(thm)],[f676,f21])).
% 0.18/0.77 fof(f701,definition,(
% 0.18/0.77 ![X0]: (sQ21_spl <=> (disjoint(set_intersection2(empty_set,X0),empty_set)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f704,plain,(
% 0.18/0.77 sQ21_spl|~sQ7_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f679,f701,f204,f646])).
% 0.18/0.77 fof(f705,definition,(
% 0.18/0.77 ![X0]: (sQ22_spl <=> (disjoint(empty_set,set_intersection2(empty_set,X0))))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f708,plain,(
% 0.18/0.77 sQ22_spl|~sQ7_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f680,f705,f204,f646])).
% 0.18/0.77 fof(f757,plain,(
% 0.18/0.77 ![X0]: (~sP0_prd(empty_set,X0))),
% 0.18/0.77 inference(resolution,[status(thm)],[f460,f56])).
% 0.18/0.77 fof(f915,plain,(
% 0.18/0.77 ![X0,X1]: (~X0=empty_set|~in(X1,empty_set)|~in(X1,empty_set)|~sQ20_spl)),
% 0.18/0.77 inference(forward_demodulation,[status(thm)],[f469,f700])).
% 0.18/0.77 fof(f916,plain,(
% 0.18/0.77 ![X0,X1]: (~X0=empty_set|~in(X1,empty_set)|~sQ20_spl)),
% 0.18/0.77 inference(duplicate_literals_removal,[status(thm)],[f915])).
% 0.18/0.77 fof(f917,plain,(
% 0.18/0.77 ![X0,X1]: (~X0=empty_set|empty_set=set_intersection2(X1,empty_set)|~sQ20_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f916,f31])).
% 0.18/0.77 fof(f918,plain,(
% 0.18/0.77 ![X0,X1,X2]: (~X0=empty_set|X1=set_intersection2(X2,empty_set)|in(sK1_skl(X1,empty_set,X2),X1)|~sQ20_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f916,f31])).
% 0.18/0.77 fof(f920,plain,(
% 0.18/0.77 ![X0,X1,X2]: (~X0=empty_set|empty_set=set_intersection2(X1,X2)|in(sK1_skl(empty_set,X2,X1),X2)|~sQ20_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f916,f31])).
% 0.18/0.77 fof(f921,plain,(
% 0.18/0.77 ![X0,X1]: (~X0=empty_set|empty_set=set_intersection2(empty_set,X1)|~sQ20_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f916,f30])).
% 0.18/0.77 fof(f922,plain,(
% 0.18/0.77 ![X0,X1,X2]: (~X0=empty_set|X1=set_intersection2(empty_set,X2)|in(sK1_skl(X1,X2,empty_set),X1)|~sQ20_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f916,f30])).
% 0.18/0.77 fof(f924,plain,(
% 0.18/0.77 ![X0,X1,X2]: (~X0=empty_set|empty_set=set_intersection2(X1,X2)|in(sK1_skl(empty_set,X2,X1),X1)|~sQ20_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f916,f30])).
% 0.18/0.77 fof(f927,plain,(
% 0.18/0.77 ![X0,X1,X2]: (~X0=empty_set|sP0_prd(set_intersection2(X1,empty_set),X2)|disjoint(X2,set_intersection2(X1,empty_set))|~sQ20_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f916,f312])).
% 0.18/0.77 fof(f928,plain,(
% 0.18/0.77 ![X0,X1,X2]: (~X0=empty_set|sP0_prd(X1,set_intersection2(X2,empty_set))|disjoint(set_intersection2(X2,empty_set),X1)|~sQ20_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f916,f313])).
% 0.18/0.77 fof(f929,plain,(
% 0.18/0.77 ![X0,X1]: (~X0=empty_set|sP0_prd(empty_set,X1)|disjoint(X1,empty_set)|~sQ20_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f916,f59])).
% 0.18/0.77 fof(f930,plain,(
% 0.18/0.77 ![X0,X1]: (~X0=empty_set|sP0_prd(X1,empty_set)|disjoint(empty_set,X1)|~sQ20_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f916,f58])).
% 0.18/0.77 fof(f931,definition,(
% 0.18/0.77 ![X0]: (sQ24_spl <=> (~X0=empty_set))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f932,plain,(
% 0.18/0.77 ![X0]: (~X0=empty_set|~sQ24_spl)),
% 0.18/0.77 inference(component_clause,[status(thm)],[f931])).
% 0.18/0.77 fof(f934,plain,(
% 0.18/0.77 sQ24_spl|sQ15_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f917,f931,f511,f646])).
% 0.18/0.77 fof(f935,definition,(
% 0.18/0.77 ![X1,X2]: (sQ25_spl <=> (X1=set_intersection2(X2,empty_set)|in(sK1_skl(X1,empty_set,X2),X1)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f938,plain,(
% 0.18/0.77 sQ24_spl|sQ25_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f918,f931,f935,f646])).
% 0.18/0.77 fof(f940,definition,(
% 0.18/0.77 ![X1,X2]: (sQ26_spl <=> (empty_set=set_intersection2(X1,X2)|in(sK1_skl(empty_set,X2,X1),X2)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f941,plain,(
% 0.18/0.77 ![X0,X1]: (empty_set=set_intersection2(X0,X1)|in(sK1_skl(empty_set,X1,X0),X1)|~sQ26_spl)),
% 0.18/0.77 inference(component_clause,[status(thm)],[f940])).
% 0.18/0.77 fof(f943,plain,(
% 0.18/0.77 sQ24_spl|sQ26_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f920,f931,f940,f646])).
% 0.18/0.77 fof(f944,plain,(
% 0.18/0.77 sQ24_spl|sQ19_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f921,f931,f598,f646])).
% 0.18/0.77 fof(f945,definition,(
% 0.18/0.77 ![X1,X2]: (sQ27_spl <=> (X1=set_intersection2(empty_set,X2)|in(sK1_skl(X1,X2,empty_set),X1)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f948,plain,(
% 0.18/0.77 sQ24_spl|sQ27_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f922,f931,f945,f646])).
% 0.18/0.77 fof(f950,definition,(
% 0.18/0.77 ![X1,X2]: (sQ28_spl <=> (empty_set=set_intersection2(X1,X2)|in(sK1_skl(empty_set,X2,X1),X1)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f953,plain,(
% 0.18/0.77 sQ24_spl|sQ28_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f924,f931,f950,f646])).
% 0.18/0.77 fof(f956,plain,(
% 0.18/0.77 sQ24_spl|sQ16_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f927,f931,f515,f646])).
% 0.18/0.77 fof(f957,definition,(
% 0.18/0.77 ![X1,X2]: (sQ29_spl <=> (sP0_prd(X1,set_intersection2(X2,empty_set))|disjoint(set_intersection2(X2,empty_set),X1)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f960,plain,(
% 0.18/0.77 sQ24_spl|sQ29_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f928,f931,f957,f646])).
% 0.18/0.77 fof(f961,plain,(
% 0.18/0.77 sQ24_spl|sQ10_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f929,f931,f239,f646])).
% 0.18/0.77 fof(f962,plain,(
% 0.18/0.77 sQ24_spl|sQ11_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f930,f931,f243,f646])).
% 0.18/0.77 fof(f963,plain,(
% 0.18/0.77 $false|~sQ12_spl),
% 0.18/0.77 inference(forward_subsumption_resolution,[status(thm)],[f490,f757])).
% 0.18/0.77 fof(f964,plain,(
% 0.18/0.77 ~sQ12_spl),
% 0.18/0.77 inference(contradiction_clause,[status(thm)],[f963])).
% 0.18/0.77 fof(f965,plain,(
% 0.18/0.77 $false|~sQ9_spl),
% 0.18/0.77 inference(forward_subsumption_resolution,[status(thm)],[f235,f757])).
% 0.18/0.77 fof(f966,plain,(
% 0.18/0.77 ~sQ9_spl),
% 0.18/0.77 inference(contradiction_clause,[status(thm)],[f965])).
% 0.18/0.77 fof(f969,definition,(
% 0.18/0.77 ![X1]: (sQ30_spl <=> (~in(X1,empty_set)))),
% 0.18/0.77 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.18/0.77 fof(f970,plain,(
% 0.18/0.77 ![X0]: (~in(X0,empty_set)|~sQ30_spl)),
% 0.18/0.77 inference(component_clause,[status(thm)],[f969])).
% 0.18/0.77 fof(f972,plain,(
% 0.18/0.77 sQ24_spl|sQ30_spl|~sQ20_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f916,f931,f969,f646])).
% 0.18/0.77 fof(f987,plain,(
% 0.18/0.77 $false|~sQ24_spl),
% 0.18/0.77 inference(backward_subsumption_resolution,[status(thm)],[f469,f932])).
% 0.18/0.77 fof(f991,plain,(
% 0.18/0.77 ~sQ24_spl),
% 0.18/0.77 inference(contradiction_clause,[status(thm)],[f987])).
% 0.18/0.77 fof(f1345,plain,(
% 0.18/0.77 ![X0,X1]: (empty_set=set_intersection2(X0,X1)|empty_set=set_intersection2(X0,X1)|in(sK1_skl(empty_set,X1,X0),empty_set)|~sP0_prd(X1,X0)|~sQ26_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f941,f564])).
% 0.18/0.77 fof(f1365,plain,(
% 0.18/0.77 ![X0,X1]: (empty_set=set_intersection2(X0,X1)|in(sK1_skl(empty_set,X1,X0),empty_set)|~sP0_prd(X1,X0)|~sQ26_spl)),
% 0.18/0.77 inference(duplicate_literals_removal,[status(thm)],[f1345])).
% 0.18/0.77 fof(f1366,plain,(
% 0.18/0.77 ![X0,X1]: (empty_set=set_intersection2(X0,X1)|~sP0_prd(X1,X0)|~sQ30_spl|~sQ26_spl)),
% 0.18/0.77 inference(forward_subsumption_resolution,[status(thm)],[f1365,f970])).
% 0.18/0.77 fof(f1381,plain,(
% 0.18/0.77 empty_set=set_intersection2(sK5_skl,sK4_skl)|~sQ30_spl|~sQ26_spl|~sQ4_spl),
% 0.18/0.77 inference(resolution,[status(thm)],[f1366,f91])).
% 0.18/0.77 fof(f1383,plain,(
% 0.18/0.77 empty_set=set_intersection2(sK4_skl,sK5_skl)|~sQ30_spl|~sQ26_spl|~sQ4_spl),
% 0.18/0.77 inference(forward_demodulation,[status(thm)],[f17,f1381])).
% 0.18/0.77 fof(f1387,plain,(
% 0.18/0.77 disjoint(sK5_skl,sK4_skl)|~sQ30_spl|~sQ26_spl|~sQ4_spl),
% 0.18/0.77 inference(resolution,[status(thm)],[f1383,f201])).
% 0.18/0.77 fof(f1411,plain,(
% 0.18/0.77 sQ5_spl|~sQ30_spl|~sQ26_spl|~sQ4_spl),
% 0.18/0.77 inference(split_clause,[status(thm)],[f1387,f93,f969,f940,f90])).
% 0.18/0.77 fof(f1488,plain,(
% 0.18/0.77 ![X0]: (in(X0,empty_set)|~in(X0,sK6_skl)|~in(X0,sK7_skl)|~sQ3_spl)),
% 0.18/0.77 inference(resolution,[status(thm)],[f183,f28])).
% 0.18/0.77 fof(f1518,plain,(
% 0.18/0.77 ![X0]: (~in(X0,sK6_skl)|~in(X0,sK7_skl)|~sQ30_spl|~sQ3_spl)),
% 0.18/0.77 inference(forward_subsumption_resolution,[status(thm)],[f1488,f970])).
% 0.18/0.77 fof(f1606,plain,(
% 0.18/0.77 ~in(sK8_skl,sK6_skl)|~sQ30_spl|~sQ3_spl|~sQ2_spl),
% 0.18/0.77 inference(resolution,[status(thm)],[f1518,f68])).
% 0.18/0.77 fof(f1623,plain,(
% 0.18/0.77 $false|~sQ1_spl|~sQ30_spl|~sQ3_spl|~sQ2_spl),
% 0.18/0.77 inference(forward_subsumption_resolution,[status(thm)],[f1606,f64])).
% 0.18/0.77 fof(f1624,plain,(
% 0.18/0.77 ~sQ1_spl|~sQ30_spl|~sQ3_spl|~sQ2_spl),
% 0.18/0.77 inference(contradiction_clause,[status(thm)],[f1623])).
% 0.18/0.77 fof(f1625,plain,(
% 0.18/0.77 $false),
% 0.18/0.77 inference(sat_refutation,[status(thm)],[f66,f70,f74,f96,f107,f237,f492,f527,f531,f649,f704,f708,f934,f938,f943,f944,f948,f953,f956,f960,f961,f962,f964,f966,f972,f991,f1411,f1624])).
% 0.18/0.77 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/0.78 % Elapsed time: 0.247661 seconds
% 0.18/0.78 % CPU time: 1.701672 seconds
% 0.18/0.78 % Total memory used: 123.672 MB
% 0.18/0.78 % Net memory used: 120.720 MB
%------------------------------------------------------------------------------