%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU340+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 : n016.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:22:22 PM UTC 2026
% Result : Theorem 3.41s 1.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU340+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n016.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 06:18:08 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 3.41/1.09 % Refutation found
% 3.41/1.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.41/1.09 % SZS output start CNFRefutation for theBenchmark
% 3.41/1.09 fof(f1,axiom,(
% 3.41/1.09 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f2,axiom,(
% 3.41/1.09 (! [A,B,C] :( element(C,powerset(cartesian_product2(A,B)))=> relation(C) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f3,axiom,(
% 3.41/1.09 (! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f4,axiom,(
% 3.41/1.09 (! [A] :( rel_str(A)=> ( transitive_relstr(A)<=> is_transitive_in(the_InternalRel(A),the_carrier(A)) ) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f5,axiom,(
% 3.41/1.09 (! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f6,axiom,(
% 3.41/1.09 (! [A] :( relation(A)=> (! [B] :( is_transitive_in(A,B)<=> (! [C,D,E] :( ( in(C,B)& in(D,B)& in(E,B)& in(ordered_pair(C,D),A)& in(ordered_pair(D,E),A) )=> in(ordered_pair(C,E),A) ) )) )) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f7,axiom,(
% 3.41/1.09 (! [A] :( rel_str(A)=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> ( related(A,B,C)<=> in(ordered_pair(B,C),the_InternalRel(A)) ) ) )) )) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f18,axiom,(
% 3.41/1.09 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> element(C,powerset(cartesian_product2(A,B))) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f19,axiom,(
% 3.41/1.09 (! [A] :( rel_str(A)=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f21,axiom,(
% 3.41/1.09 (? [A] : rel_str(A) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f24,axiom,(
% 3.41/1.09 (! [A] :(? [B] : element(B,A) ))),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f25,axiom,(
% 3.41/1.09 (! [A,B] :(? [C] : relation_of2_as_subset(C,A,B) ))),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f26,axiom,(
% 3.41/1.09 (! [A] : ~ empty(powerset(A)) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f27,axiom,(
% 3.41/1.09 empty(empty_set) ),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f29,axiom,(
% 3.41/1.09 (! [A,B] : ~ empty(unordered_pair(A,B)) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f31,axiom,(
% 3.41/1.09 (! [A] :( ~ empty(A)=> (? [B] :( element(B,powerset(A))& ~ empty(B) ) )) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f33,axiom,(
% 3.41/1.09 (! [A] :(? [B] :( element(B,powerset(A))& empty(B) ) ))),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f36,axiom,(
% 3.41/1.09 (! [A,B] : subset(A,A) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f37,axiom,(
% 3.41/1.09 (! [A,B,C,D] :( in(ordered_pair(A,B),cartesian_product2(C,D))<=> ( in(A,C)& in(B,D) ) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f39,conjecture,(
% 3.41/1.09 (! [A] :( ( transitive_relstr(A)& rel_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> (! [D] :( element(D,the_carrier(A))=> ( ( related(A,B,C)& related(A,C,D) )=> related(A,B,D) ) ) )) )) )) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f40,negated_conjecture,(
% 3.41/1.09 ~((! [A] :( ( transitive_relstr(A)& rel_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> (! [D] :( element(D,the_carrier(A))=> ( ( related(A,B,C)& related(A,C,D) )=> related(A,B,D) ) ) )) )) )) ))),
% 3.41/1.09 inference(negated_conjecture,[status(cth)],[f39])).
% 3.41/1.09 fof(f41,axiom,(
% 3.41/1.09 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f42,axiom,(
% 3.41/1.09 (! [A,B] :( element(A,powerset(B))<=> subset(A,B) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f43,axiom,(
% 3.41/1.09 (! [A,B,C] :( ( in(A,B)& element(B,powerset(C)) )=> element(A,C) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f44,axiom,(
% 3.41/1.09 (! [A,B,C] :~ ( in(A,B)& element(B,powerset(C))& empty(C) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f45,axiom,(
% 3.41/1.09 (! [A] :( empty(A)=> A = empty_set ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f46,axiom,(
% 3.41/1.09 (! [A,B] :~ ( in(A,B)& empty(B) ) )),
% 3.41/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.41/1.09 fof(f48,plain,(
% 3.41/1.09 ![A,B]: (~in(A,B)|~in(B,A))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 3.41/1.09 fof(f49,plain,(
% 3.41/1.09 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f48])).
% 3.41/1.09 fof(f50,plain,(
% 3.41/1.09 ![A,B,C]: (~element(C,powerset(cartesian_product2(A,B)))|relation(C))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 3.41/1.09 fof(f51,plain,(
% 3.41/1.09 ![C]: ((![A,B]: ~element(C,powerset(cartesian_product2(A,B))))|relation(C))),
% 3.41/1.09 inference(miniscoping,[status(thm)],[f50])).
% 3.41/1.09 fof(f52,plain,(
% 3.41/1.09 ![X0,X1,X2]: (~element(X0,powerset(cartesian_product2(X1,X2)))|relation(X0))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f51])).
% 3.41/1.09 fof(f53,plain,(
% 3.41/1.09 ![X0,X1]: (unordered_pair(X0,X1)=unordered_pair(X1,X0))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f3])).
% 3.41/1.09 fof(f54,plain,(
% 3.41/1.09 ![A]: (~rel_str(A)|(transitive_relstr(A)<=>is_transitive_in(the_InternalRel(A),the_carrier(A))))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 3.41/1.09 fof(f55,plain,(
% 3.41/1.09 ![A]: (~rel_str(A)|((~transitive_relstr(A)|is_transitive_in(the_InternalRel(A),the_carrier(A)))&(transitive_relstr(A)|~is_transitive_in(the_InternalRel(A),the_carrier(A)))))),
% 3.41/1.09 inference(NNF_transformation,[status(thm)],[f54])).
% 3.41/1.09 fof(f56,plain,(
% 3.41/1.09 ![X0]: (~rel_str(X0)|~transitive_relstr(X0)|is_transitive_in(the_InternalRel(X0),the_carrier(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f55])).
% 3.41/1.09 fof(f57,plain,(
% 3.41/1.09 ![X0]: (~rel_str(X0)|transitive_relstr(X0)|~is_transitive_in(the_InternalRel(X0),the_carrier(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f55])).
% 3.41/1.09 fof(f58,plain,(
% 3.41/1.09 ![X0,X1]: (ordered_pair(X0,X1)=unordered_pair(unordered_pair(X0,X1),singleton(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f5])).
% 3.41/1.09 fof(f59,plain,(
% 3.41/1.09 ![A]: (~relation(A)|(![B]: (is_transitive_in(A,B)<=>(![C,D,E]: (((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A))|in(ordered_pair(C,E),A))))))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 3.41/1.09 fof(f60,plain,(
% 3.41/1.09 ![A]: (~relation(A)|(![B]: ((~is_transitive_in(A,B)|(![C,D,E]: (((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A))|in(ordered_pair(C,E),A))))&(is_transitive_in(A,B)|(?[C,D,E]: (((((in(C,B)&in(D,B))&in(E,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,E),A))&~in(ordered_pair(C,E),A)))))))),
% 3.41/1.09 inference(NNF_transformation,[status(thm)],[f59])).
% 3.41/1.09 fof(f61,plain,(
% 3.41/1.09 ![A]: (~relation(A)|((![B]: (~is_transitive_in(A,B)|(![C,E]: ((![D]: ((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A)))|in(ordered_pair(C,E),A)))))&(![B]: (is_transitive_in(A,B)|(?[C,E]: ((?[D]: ((((in(C,B)&in(D,B))&in(E,B))&in(ordered_pair(C,D),A))&in(ordered_pair(D,E),A)))&~in(ordered_pair(C,E),A)))))))),
% 3.41/1.09 inference(miniscoping,[status(thm)],[f60])).
% 3.41/1.09 fof(f62,plain,(
% 3.41/1.09 ![A]: (~relation(A)|((![B]: (~is_transitive_in(A,B)|(![C,E]: ((![D]: ((((~in(C,B)|~in(D,B))|~in(E,B))|~in(ordered_pair(C,D),A))|~in(ordered_pair(D,E),A)))|in(ordered_pair(C,E),A)))))&(![B]: (is_transitive_in(A,B)|(((((in(sK0_skl(B,A),B)&in(sK2_skl(B,A),B))&in(sK1_skl(B,A),B))&in(ordered_pair(sK0_skl(B,A),sK2_skl(B,A)),A))&in(ordered_pair(sK2_skl(B,A),sK1_skl(B,A)),A))&~in(ordered_pair(sK0_skl(B,A),sK1_skl(B,A)),A))))))),
% 3.41/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(C,sK0_skl(B,A)),skolemize(E,sK1_skl(B,A)),skolemize(D,sK2_skl(B,A))],[f61])).
% 3.41/1.09 fof(f63,plain,(
% 3.41/1.09 ![X0,X1,X2,X3,X4]: (~relation(X0)|~is_transitive_in(X0,X1)|~in(X2,X1)|~in(X3,X1)|~in(X4,X1)|~in(ordered_pair(X2,X3),X0)|~in(ordered_pair(X3,X4),X0)|in(ordered_pair(X2,X4),X0))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f62])).
% 3.41/1.09 fof(f68,plain,(
% 3.41/1.09 ![X0,X1]: (~relation(X0)|is_transitive_in(X0,X1)|in(ordered_pair(sK2_skl(X1,X0),sK1_skl(X1,X0)),X0))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f62])).
% 3.41/1.09 fof(f70,plain,(
% 3.41/1.09 ![A]: (~rel_str(A)|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|(related(A,B,C)<=>in(ordered_pair(B,C),the_InternalRel(A))))))))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 3.41/1.09 fof(f71,plain,(
% 3.41/1.09 ![A]: (~rel_str(A)|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|((~related(A,B,C)|in(ordered_pair(B,C),the_InternalRel(A)))&(related(A,B,C)|~in(ordered_pair(B,C),the_InternalRel(A)))))))))),
% 3.41/1.09 inference(NNF_transformation,[status(thm)],[f70])).
% 3.41/1.09 fof(f72,plain,(
% 3.41/1.09 ![X0,X1,X2]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|~related(X0,X1,X2)|in(ordered_pair(X1,X2),the_InternalRel(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f71])).
% 3.41/1.09 fof(f73,plain,(
% 3.41/1.09 ![X0,X1,X2]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|related(X0,X1,X2)|~in(ordered_pair(X1,X2),the_InternalRel(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f71])).
% 3.41/1.09 fof(f76,plain,(
% 3.41/1.09 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|element(C,powerset(cartesian_product2(A,B))))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 3.41/1.09 fof(f77,plain,(
% 3.41/1.09 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|element(X0,powerset(cartesian_product2(X1,X2))))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f76])).
% 3.41/1.09 fof(f78,plain,(
% 3.41/1.09 ![A]: (~rel_str(A)|relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 3.41/1.09 fof(f79,plain,(
% 3.41/1.09 ![X0]: (~rel_str(X0)|relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f78])).
% 3.41/1.09 fof(f80,plain,(
% 3.41/1.09 rel_str(sK3_skl)),
% 3.41/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f21])).
% 3.41/1.09 fof(f81,plain,(
% 3.41/1.09 rel_str(sK3_skl)),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f80])).
% 3.41/1.09 fof(f86,plain,(
% 3.41/1.09 ![A]: element(sK6_skl(A),A)),
% 3.41/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(B,sK6_skl(A))],[f24])).
% 3.41/1.09 fof(f87,plain,(
% 3.41/1.09 ![X0]: (element(sK6_skl(X0),X0))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f86])).
% 3.41/1.09 fof(f88,plain,(
% 3.41/1.09 ![A,B]: relation_of2_as_subset(sK7_skl(B,A),A,B)),
% 3.41/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(C,sK7_skl(B,A))],[f25])).
% 3.41/1.09 fof(f89,plain,(
% 3.41/1.09 ![X0,X1]: (relation_of2_as_subset(sK7_skl(X0,X1),X1,X0))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f88])).
% 3.41/1.09 fof(f90,plain,(
% 3.41/1.09 ![X0]: (~empty(powerset(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f26])).
% 3.41/1.09 fof(f91,plain,(
% 3.41/1.09 empty(empty_set)),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f27])).
% 3.41/1.09 fof(f93,plain,(
% 3.41/1.09 ![X0,X1]: (~empty(unordered_pair(X0,X1)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f29])).
% 3.41/1.09 fof(f96,plain,(
% 3.41/1.09 ![A]: (empty(A)|(?[B]: (element(B,powerset(A))&~empty(B))))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 3.41/1.09 fof(f97,plain,(
% 3.41/1.09 ![A]: (empty(A)|(element(sK8_skl(A),powerset(A))&~empty(sK8_skl(A))))),
% 3.41/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f96])).
% 3.41/1.09 fof(f98,plain,(
% 3.41/1.09 ![X0]: (empty(X0)|element(sK8_skl(X0),powerset(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f97])).
% 3.41/1.09 fof(f99,plain,(
% 3.41/1.09 ![X0]: (empty(X0)|~empty(sK8_skl(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f97])).
% 3.41/1.09 fof(f102,plain,(
% 3.41/1.09 ![A]: (element(sK10_skl(A),powerset(A))&empty(sK10_skl(A)))),
% 3.41/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(B,sK10_skl(A))],[f33])).
% 3.41/1.09 fof(f103,plain,(
% 3.41/1.09 ![X0]: (element(sK10_skl(X0),powerset(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f102])).
% 3.41/1.09 fof(f104,plain,(
% 3.41/1.09 ![X0]: (empty(sK10_skl(X0)))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f102])).
% 3.41/1.09 fof(f111,plain,(
% 3.41/1.09 ![A]: subset(A,A)),
% 3.41/1.09 inference(miniscoping,[status(thm)],[f36])).
% 3.41/1.09 fof(f112,plain,(
% 3.41/1.09 ![X0]: (subset(X0,X0))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f111])).
% 3.41/1.09 fof(f113,plain,(
% 3.41/1.09 ![A,B,C,D]: ((~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))&(in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 3.41/1.09 inference(NNF_transformation,[status(thm)],[f37])).
% 3.41/1.09 fof(f114,plain,(
% 3.41/1.09 (![A,B,C,D]: (~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D))))&(![A,B,C,D]: (in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 3.41/1.09 inference(miniscoping,[status(thm)],[f113])).
% 3.41/1.09 fof(f115,plain,(
% 3.41/1.09 ![X0,X1,X2,X3]: (~in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|in(X0,X2))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f114])).
% 3.41/1.09 fof(f116,plain,(
% 3.41/1.09 ![X0,X1,X2,X3]: (~in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|in(X1,X3))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f114])).
% 3.41/1.09 fof(f117,plain,(
% 3.41/1.09 ![X0,X1,X2,X3]: (in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|~in(X0,X2)|~in(X1,X3))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f114])).
% 3.41/1.09 fof(f120,plain,(
% 3.41/1.09 (?[A]: ((transitive_relstr(A)&rel_str(A))&(?[B]: (element(B,the_carrier(A))&(?[C]: (element(C,the_carrier(A))&(?[D]: (element(D,the_carrier(A))&((related(A,B,C)&related(A,C,D))&~related(A,B,D))))))))))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 3.41/1.09 fof(f121,plain,(
% 3.41/1.09 ((transitive_relstr(sK12_skl)&rel_str(sK12_skl))&(element(sK13_skl,the_carrier(sK12_skl))&(element(sK14_skl,the_carrier(sK12_skl))&(element(sK15_skl,the_carrier(sK12_skl))&((related(sK12_skl,sK13_skl,sK14_skl)&related(sK12_skl,sK14_skl,sK15_skl))&~related(sK12_skl,sK13_skl,sK15_skl))))))),
% 3.41/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl,sK15_skl]),skolemize(A,sK12_skl),skolemize(B,sK13_skl),skolemize(C,sK14_skl),skolemize(D,sK15_skl)],[f120])).
% 3.41/1.09 fof(f122,plain,(
% 3.41/1.09 transitive_relstr(sK12_skl)),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f121])).
% 3.41/1.09 fof(f123,plain,(
% 3.41/1.09 rel_str(sK12_skl)),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f121])).
% 3.41/1.09 fof(f124,plain,(
% 3.41/1.09 element(sK13_skl,the_carrier(sK12_skl))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f121])).
% 3.41/1.09 fof(f125,plain,(
% 3.41/1.09 element(sK14_skl,the_carrier(sK12_skl))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f121])).
% 3.41/1.09 fof(f126,plain,(
% 3.41/1.09 element(sK15_skl,the_carrier(sK12_skl))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f121])).
% 3.41/1.09 fof(f127,plain,(
% 3.41/1.09 related(sK12_skl,sK13_skl,sK14_skl)),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f121])).
% 3.41/1.09 fof(f128,plain,(
% 3.41/1.09 related(sK12_skl,sK14_skl,sK15_skl)),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f121])).
% 3.41/1.09 fof(f129,plain,(
% 3.41/1.09 ~related(sK12_skl,sK13_skl,sK15_skl)),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f121])).
% 3.41/1.09 fof(f130,plain,(
% 3.41/1.09 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 3.41/1.09 fof(f131,plain,(
% 3.41/1.09 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f130])).
% 3.41/1.09 fof(f132,plain,(
% 3.41/1.09 ![A,B]: ((~element(A,powerset(B))|subset(A,B))&(element(A,powerset(B))|~subset(A,B)))),
% 3.41/1.09 inference(NNF_transformation,[status(thm)],[f42])).
% 3.41/1.09 fof(f133,plain,(
% 3.41/1.09 (![A,B]: (~element(A,powerset(B))|subset(A,B)))&(![A,B]: (element(A,powerset(B))|~subset(A,B)))),
% 3.41/1.09 inference(miniscoping,[status(thm)],[f132])).
% 3.41/1.09 fof(f135,plain,(
% 3.41/1.09 ![X0,X1]: (element(X0,powerset(X1))|~subset(X0,X1))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f133])).
% 3.41/1.09 fof(f136,plain,(
% 3.41/1.09 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|element(A,C))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 3.41/1.09 fof(f137,plain,(
% 3.41/1.09 ![A,C]: ((![B]: (~in(A,B)|~element(B,powerset(C))))|element(A,C))),
% 3.41/1.09 inference(miniscoping,[status(thm)],[f136])).
% 3.41/1.09 fof(f138,plain,(
% 3.41/1.09 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|element(X0,X2))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f137])).
% 3.41/1.09 fof(f139,plain,(
% 3.41/1.09 ![A,B,C]: ((~in(A,B)|~element(B,powerset(C)))|~empty(C))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 3.41/1.09 fof(f140,plain,(
% 3.41/1.09 ![C]: ((![B]: ((![A]: ~in(A,B))|~element(B,powerset(C))))|~empty(C))),
% 3.41/1.09 inference(miniscoping,[status(thm)],[f139])).
% 3.41/1.09 fof(f141,plain,(
% 3.41/1.09 ![X0,X1,X2]: (~in(X0,X1)|~element(X1,powerset(X2))|~empty(X2))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f140])).
% 3.41/1.09 fof(f142,plain,(
% 3.41/1.09 ![A]: (~empty(A)|A=empty_set)),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 3.41/1.09 fof(f143,plain,(
% 3.41/1.09 ![X0]: (~empty(X0)|X0=empty_set)),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f142])).
% 3.41/1.09 fof(f144,plain,(
% 3.41/1.09 ![A,B]: (~in(A,B)|~empty(B))),
% 3.41/1.09 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 3.41/1.09 fof(f145,plain,(
% 3.41/1.09 ![B]: ((![A]: ~in(A,B))|~empty(B))),
% 3.41/1.09 inference(miniscoping,[status(thm)],[f144])).
% 3.41/1.09 fof(f146,plain,(
% 3.41/1.09 ![X0,X1]: (~in(X0,X1)|~empty(X1))),
% 3.41/1.09 inference(cnf_transformation,[status(thm)],[f145])).
% 3.41/1.09 fof(f150,plain,(
% 3.41/1.09 ~rel_str(sK12_skl)|is_transitive_in(the_InternalRel(sK12_skl),the_carrier(sK12_skl))),
% 3.41/1.09 inference(resolution,[status(thm)],[f56,f122])).
% 3.41/1.09 fof(f151,definition,(
% 3.41/1.09 sQ0_spl <=> (rel_str(sK12_skl))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f153,plain,(
% 3.41/1.09 ~rel_str(sK12_skl)|sQ0_spl),
% 3.41/1.09 inference(component_clause,[status(thm)],[f151])).
% 3.41/1.09 fof(f154,definition,(
% 3.41/1.09 sQ1_spl <=> (is_transitive_in(the_InternalRel(sK12_skl),the_carrier(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f155,plain,(
% 3.41/1.09 is_transitive_in(the_InternalRel(sK12_skl),the_carrier(sK12_skl))|~sQ1_spl),
% 3.41/1.09 inference(component_clause,[status(thm)],[f154])).
% 3.41/1.09 fof(f157,plain,(
% 3.41/1.09 ~sQ0_spl|sQ1_spl),
% 3.41/1.09 inference(split_clause,[status(thm)],[f150,f151,f154])).
% 3.41/1.09 fof(f158,plain,(
% 3.41/1.09 $false|sQ0_spl),
% 3.41/1.09 inference(forward_subsumption_resolution,[status(thm)],[f153,f123])).
% 3.41/1.09 fof(f159,plain,(
% 3.41/1.09 sQ0_spl),
% 3.41/1.09 inference(contradiction_clause,[status(thm)],[f158])).
% 3.41/1.09 fof(f164,plain,(
% 3.41/1.09 ~rel_str(sK12_skl)|~element(sK14_skl,the_carrier(sK12_skl))|~element(sK15_skl,the_carrier(sK12_skl))|in(ordered_pair(sK14_skl,sK15_skl),the_InternalRel(sK12_skl))),
% 3.41/1.09 inference(resolution,[status(thm)],[f72,f128])).
% 3.41/1.09 fof(f165,plain,(
% 3.41/1.09 ~rel_str(sK12_skl)|~element(sK13_skl,the_carrier(sK12_skl))|~element(sK14_skl,the_carrier(sK12_skl))|in(ordered_pair(sK13_skl,sK14_skl),the_InternalRel(sK12_skl))),
% 3.41/1.09 inference(resolution,[status(thm)],[f72,f127])).
% 3.41/1.09 fof(f166,definition,(
% 3.41/1.09 sQ2_spl <=> (element(sK14_skl,the_carrier(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f168,plain,(
% 3.41/1.09 ~element(sK14_skl,the_carrier(sK12_skl))|sQ2_spl),
% 3.41/1.09 inference(component_clause,[status(thm)],[f166])).
% 3.41/1.09 fof(f169,definition,(
% 3.41/1.09 sQ3_spl <=> (element(sK15_skl,the_carrier(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f171,plain,(
% 3.41/1.09 ~element(sK15_skl,the_carrier(sK12_skl))|sQ3_spl),
% 3.41/1.09 inference(component_clause,[status(thm)],[f169])).
% 3.41/1.09 fof(f172,definition,(
% 3.41/1.09 sQ4_spl <=> (in(ordered_pair(sK14_skl,sK15_skl),the_InternalRel(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f173,plain,(
% 3.41/1.09 in(ordered_pair(sK14_skl,sK15_skl),the_InternalRel(sK12_skl))|~sQ4_spl),
% 3.41/1.09 inference(component_clause,[status(thm)],[f172])).
% 3.41/1.09 fof(f175,plain,(
% 3.41/1.09 ~sQ0_spl|~sQ2_spl|~sQ3_spl|sQ4_spl),
% 3.41/1.09 inference(split_clause,[status(thm)],[f164,f151,f166,f169,f172])).
% 3.41/1.09 fof(f176,definition,(
% 3.41/1.09 sQ5_spl <=> (element(sK13_skl,the_carrier(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f178,plain,(
% 3.41/1.09 ~element(sK13_skl,the_carrier(sK12_skl))|sQ5_spl),
% 3.41/1.09 inference(component_clause,[status(thm)],[f176])).
% 3.41/1.09 fof(f179,definition,(
% 3.41/1.09 sQ6_spl <=> (in(ordered_pair(sK13_skl,sK14_skl),the_InternalRel(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f180,plain,(
% 3.41/1.09 in(ordered_pair(sK13_skl,sK14_skl),the_InternalRel(sK12_skl))|~sQ6_spl),
% 3.41/1.09 inference(component_clause,[status(thm)],[f179])).
% 3.41/1.09 fof(f182,plain,(
% 3.41/1.09 ~sQ0_spl|~sQ5_spl|~sQ2_spl|sQ6_spl),
% 3.41/1.09 inference(split_clause,[status(thm)],[f165,f151,f176,f166,f179])).
% 3.41/1.09 fof(f183,plain,(
% 3.41/1.09 $false|sQ2_spl),
% 3.41/1.09 inference(forward_subsumption_resolution,[status(thm)],[f168,f125])).
% 3.41/1.09 fof(f184,plain,(
% 3.41/1.09 sQ2_spl),
% 3.41/1.09 inference(contradiction_clause,[status(thm)],[f183])).
% 3.41/1.09 fof(f185,plain,(
% 3.41/1.09 $false|sQ3_spl),
% 3.41/1.09 inference(forward_subsumption_resolution,[status(thm)],[f171,f126])).
% 3.41/1.09 fof(f186,plain,(
% 3.41/1.09 sQ3_spl),
% 3.41/1.09 inference(contradiction_clause,[status(thm)],[f185])).
% 3.41/1.09 fof(f187,plain,(
% 3.41/1.09 $false|sQ5_spl),
% 3.41/1.09 inference(forward_subsumption_resolution,[status(thm)],[f178,f124])).
% 3.41/1.09 fof(f188,plain,(
% 3.41/1.09 sQ5_spl),
% 3.41/1.09 inference(contradiction_clause,[status(thm)],[f187])).
% 3.41/1.09 fof(f189,plain,(
% 3.41/1.09 ![X0,X1]: (ordered_pair(X0,X1)=unordered_pair(singleton(X0),unordered_pair(X0,X1)))),
% 3.41/1.09 inference(forward_demodulation,[status(thm)],[f53,f58])).
% 3.41/1.09 fof(f193,plain,(
% 3.41/1.09 ~rel_str(sK12_skl)|transitive_relstr(sK12_skl)|~sQ1_spl),
% 3.41/1.09 inference(resolution,[status(thm)],[f155,f57])).
% 3.41/1.09 fof(f194,plain,(
% 3.41/1.09 ![X0,X1,X2]: (~relation(the_InternalRel(sK12_skl))|~in(X0,the_carrier(sK12_skl))|~in(X1,the_carrier(sK12_skl))|~in(X2,the_carrier(sK12_skl))|~in(ordered_pair(X0,X1),the_InternalRel(sK12_skl))|~in(ordered_pair(X1,X2),the_InternalRel(sK12_skl))|in(ordered_pair(X0,X2),the_InternalRel(sK12_skl))|~sQ1_spl)),
% 3.41/1.09 inference(resolution,[status(thm)],[f155,f63])).
% 3.41/1.09 fof(f195,definition,(
% 3.41/1.09 sQ7_spl <=> (transitive_relstr(sK12_skl))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f198,plain,(
% 3.41/1.09 ~sQ0_spl|sQ7_spl|~sQ1_spl),
% 3.41/1.09 inference(split_clause,[status(thm)],[f193,f151,f195,f154])).
% 3.41/1.09 fof(f199,definition,(
% 3.41/1.09 sQ8_spl <=> (relation(the_InternalRel(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f201,plain,(
% 3.41/1.09 ~relation(the_InternalRel(sK12_skl))|sQ8_spl),
% 3.41/1.09 inference(component_clause,[status(thm)],[f199])).
% 3.41/1.09 fof(f202,definition,(
% 3.41/1.09 ![X0,X1,X2]: (sQ9_spl <=> (~in(X0,the_carrier(sK12_skl))|~in(X1,the_carrier(sK12_skl))|~in(X2,the_carrier(sK12_skl))|~in(ordered_pair(X0,X1),the_InternalRel(sK12_skl))|~in(ordered_pair(X1,X2),the_InternalRel(sK12_skl))|in(ordered_pair(X0,X2),the_InternalRel(sK12_skl))))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f203,plain,(
% 3.41/1.09 ![X0,X1,X2]: (~in(X0,the_carrier(sK12_skl))|~in(X1,the_carrier(sK12_skl))|~in(X2,the_carrier(sK12_skl))|~in(ordered_pair(X0,X1),the_InternalRel(sK12_skl))|~in(ordered_pair(X1,X2),the_InternalRel(sK12_skl))|in(ordered_pair(X0,X2),the_InternalRel(sK12_skl))|~sQ9_spl)),
% 3.41/1.09 inference(component_clause,[status(thm)],[f202])).
% 3.41/1.09 fof(f205,plain,(
% 3.41/1.09 ~sQ8_spl|sQ9_spl|~sQ1_spl),
% 3.41/1.09 inference(split_clause,[status(thm)],[f194,f199,f202,f154])).
% 3.41/1.09 fof(f206,plain,(
% 3.41/1.09 empty(the_carrier(sK12_skl))|in(sK15_skl,the_carrier(sK12_skl))),
% 3.41/1.09 inference(resolution,[status(thm)],[f131,f126])).
% 3.41/1.09 fof(f207,plain,(
% 3.41/1.09 empty(the_carrier(sK12_skl))|in(sK14_skl,the_carrier(sK12_skl))),
% 3.41/1.09 inference(resolution,[status(thm)],[f131,f125])).
% 3.41/1.09 fof(f208,plain,(
% 3.41/1.09 empty(the_carrier(sK12_skl))|in(sK13_skl,the_carrier(sK12_skl))),
% 3.41/1.09 inference(resolution,[status(thm)],[f131,f124])).
% 3.41/1.09 fof(f209,definition,(
% 3.41/1.09 sQ10_spl <=> (empty(the_carrier(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f210,plain,(
% 3.41/1.09 empty(the_carrier(sK12_skl))|~sQ10_spl),
% 3.41/1.09 inference(component_clause,[status(thm)],[f209])).
% 3.41/1.09 fof(f212,definition,(
% 3.41/1.09 sQ11_spl <=> (in(sK15_skl,the_carrier(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f215,plain,(
% 3.41/1.09 sQ10_spl|sQ11_spl),
% 3.41/1.09 inference(split_clause,[status(thm)],[f206,f209,f212])).
% 3.41/1.09 fof(f216,definition,(
% 3.41/1.09 sQ12_spl <=> (in(sK14_skl,the_carrier(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f219,plain,(
% 3.41/1.09 sQ10_spl|sQ12_spl),
% 3.41/1.09 inference(split_clause,[status(thm)],[f207,f209,f216])).
% 3.41/1.09 fof(f220,definition,(
% 3.41/1.09 sQ13_spl <=> (in(sK13_skl,the_carrier(sK12_skl)))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 3.41/1.09 fof(f223,plain,(
% 3.41/1.09 sQ10_spl|sQ13_spl),
% 3.41/1.09 inference(split_clause,[status(thm)],[f208,f209,f220])).
% 3.41/1.09 fof(f224,plain,(
% 3.41/1.09 ~rel_str(sK12_skl)|~element(sK14_skl,the_carrier(sK12_skl))|~element(sK15_skl,the_carrier(sK12_skl))|related(sK12_skl,sK14_skl,sK15_skl)|~sQ4_spl),
% 3.41/1.09 inference(resolution,[status(thm)],[f173,f73])).
% 3.41/1.09 fof(f227,definition,(
% 3.41/1.09 sQ14_spl <=> (related(sK12_skl,sK14_skl,sK15_skl))),
% 3.41/1.09 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f230,plain,(
% 3.09/1.10 ~sQ0_spl|~sQ2_spl|~sQ3_spl|sQ14_spl|~sQ4_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f224,f151,f166,f169,f227,f172])).
% 3.09/1.10 fof(f231,plain,(
% 3.09/1.10 ~rel_str(sK12_skl)|~element(sK13_skl,the_carrier(sK12_skl))|~element(sK14_skl,the_carrier(sK12_skl))|related(sK12_skl,sK13_skl,sK14_skl)|~sQ6_spl),
% 3.09/1.10 inference(resolution,[status(thm)],[f180,f73])).
% 3.09/1.10 fof(f234,definition,(
% 3.09/1.10 sQ15_spl <=> (related(sK12_skl,sK13_skl,sK14_skl))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f237,plain,(
% 3.09/1.10 ~sQ0_spl|~sQ5_spl|~sQ2_spl|sQ15_spl|~sQ6_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f231,f151,f176,f166,f234,f179])).
% 3.09/1.10 fof(f239,definition,(
% 3.09/1.10 sQ16_spl <=> (empty(the_InternalRel(sK12_skl)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f240,plain,(
% 3.09/1.10 empty(the_InternalRel(sK12_skl))|~sQ16_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f239])).
% 3.09/1.10 fof(f247,plain,(
% 3.09/1.10 relation_of2_as_subset(the_InternalRel(sK3_skl),the_carrier(sK3_skl),the_carrier(sK3_skl))),
% 3.09/1.10 inference(resolution,[status(thm)],[f79,f81])).
% 3.09/1.10 fof(f248,plain,(
% 3.09/1.10 relation_of2_as_subset(the_InternalRel(sK12_skl),the_carrier(sK12_skl),the_carrier(sK12_skl))),
% 3.09/1.10 inference(resolution,[status(thm)],[f79,f123])).
% 3.09/1.10 fof(f249,plain,(
% 3.09/1.10 element(the_InternalRel(sK12_skl),powerset(cartesian_product2(the_carrier(sK12_skl),the_carrier(sK12_skl))))),
% 3.09/1.10 inference(resolution,[status(thm)],[f248,f77])).
% 3.09/1.10 fof(f250,plain,(
% 3.09/1.10 relation(the_InternalRel(sK12_skl))),
% 3.09/1.10 inference(resolution,[status(thm)],[f249,f52])).
% 3.09/1.10 fof(f251,plain,(
% 3.09/1.10 empty(powerset(cartesian_product2(the_carrier(sK12_skl),the_carrier(sK12_skl))))|in(the_InternalRel(sK12_skl),powerset(cartesian_product2(the_carrier(sK12_skl),the_carrier(sK12_skl))))),
% 3.09/1.10 inference(resolution,[status(thm)],[f249,f131])).
% 3.09/1.10 fof(f252,plain,(
% 3.09/1.10 $false|sQ8_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f250,f201])).
% 3.09/1.10 fof(f253,plain,(
% 3.09/1.10 sQ8_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f252])).
% 3.09/1.10 fof(f254,definition,(
% 3.09/1.10 sQ17_spl <=> (empty(powerset(cartesian_product2(the_carrier(sK12_skl),the_carrier(sK12_skl)))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f255,plain,(
% 3.09/1.10 empty(powerset(cartesian_product2(the_carrier(sK12_skl),the_carrier(sK12_skl))))|~sQ17_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f254])).
% 3.09/1.10 fof(f257,definition,(
% 3.09/1.10 sQ18_spl <=> (in(the_InternalRel(sK12_skl),powerset(cartesian_product2(the_carrier(sK12_skl),the_carrier(sK12_skl)))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f260,plain,(
% 3.09/1.10 sQ17_spl|sQ18_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f251,f254,f257])).
% 3.09/1.10 fof(f261,plain,(
% 3.09/1.10 $false|~sQ17_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f255,f90])).
% 3.09/1.10 fof(f262,plain,(
% 3.09/1.10 ~sQ17_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f261])).
% 3.09/1.10 fof(f268,plain,(
% 3.09/1.10 ![X0]: (~in(sK13_skl,the_carrier(sK12_skl))|~in(sK14_skl,the_carrier(sK12_skl))|~in(X0,the_carrier(sK12_skl))|~in(ordered_pair(sK14_skl,X0),the_InternalRel(sK12_skl))|in(ordered_pair(sK13_skl,X0),the_InternalRel(sK12_skl))|~sQ9_spl|~sQ6_spl)),
% 3.09/1.10 inference(resolution,[status(thm)],[f203,f180])).
% 3.09/1.10 fof(f270,definition,(
% 3.09/1.10 ![X0]: (sQ19_spl <=> (~in(X0,the_carrier(sK12_skl))|~in(ordered_pair(sK14_skl,X0),the_InternalRel(sK12_skl))|in(ordered_pair(sK13_skl,X0),the_InternalRel(sK12_skl))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f271,plain,(
% 3.09/1.10 ![X0]: (~in(X0,the_carrier(sK12_skl))|~in(ordered_pair(sK14_skl,X0),the_InternalRel(sK12_skl))|in(ordered_pair(sK13_skl,X0),the_InternalRel(sK12_skl))|~sQ19_spl)),
% 3.09/1.10 inference(component_clause,[status(thm)],[f270])).
% 3.09/1.10 fof(f273,plain,(
% 3.09/1.10 ~sQ13_spl|~sQ12_spl|sQ19_spl|~sQ9_spl|~sQ6_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f268,f220,f216,f270,f202,f179])).
% 3.09/1.10 fof(f281,plain,(
% 3.09/1.10 ![X0]: (empty(X0)|in(sK6_skl(X0),X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f87,f131])).
% 3.09/1.10 fof(f282,plain,(
% 3.09/1.10 ![X0,X1]: (~empty(ordered_pair(X0,X1)))),
% 3.09/1.10 inference(paramodulation,[status(thm)],[f189,f93])).
% 3.09/1.10 fof(f285,plain,(
% 3.09/1.10 the_carrier(sK12_skl)=empty_set|~sQ10_spl),
% 3.09/1.10 inference(resolution,[status(thm)],[f143,f210])).
% 3.09/1.10 fof(f286,plain,(
% 3.09/1.10 ![X0]: (sK10_skl(X0)=empty_set)),
% 3.09/1.10 inference(resolution,[status(thm)],[f143,f104])).
% 3.09/1.10 fof(f289,plain,(
% 3.09/1.10 ![X0,X1]: (element(sK7_skl(X0,X1),powerset(cartesian_product2(X1,X0))))),
% 3.09/1.10 inference(resolution,[status(thm)],[f89,f77])).
% 3.09/1.10 fof(f292,plain,(
% 3.09/1.10 element(the_InternalRel(sK12_skl),powerset(cartesian_product2(the_carrier(sK12_skl),empty_set)))|~sQ10_spl),
% 3.09/1.10 inference(backward_demodulation,[status(thm)],[f285,f249])).
% 3.09/1.10 fof(f303,plain,(
% 3.09/1.10 element(the_InternalRel(sK12_skl),powerset(cartesian_product2(empty_set,empty_set)))|~sQ10_spl),
% 3.09/1.10 inference(forward_demodulation,[status(thm)],[f285,f292])).
% 3.09/1.10 fof(f310,definition,(
% 3.09/1.10 sQ22_spl <=> (empty(empty_set))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f312,plain,(
% 3.09/1.10 ~empty(empty_set)|sQ22_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f310])).
% 3.09/1.10 fof(f313,definition,(
% 3.09/1.10 sQ23_spl <=> (in(sK15_skl,empty_set))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f314,plain,(
% 3.09/1.10 in(sK15_skl,empty_set)|~sQ23_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f313])).
% 3.09/1.10 fof(f318,definition,(
% 3.09/1.10 sQ24_spl <=> (in(sK14_skl,empty_set))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f319,plain,(
% 3.09/1.10 in(sK14_skl,empty_set)|~sQ24_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f318])).
% 3.09/1.10 fof(f323,definition,(
% 3.09/1.10 sQ25_spl <=> (in(sK13_skl,empty_set))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f324,plain,(
% 3.09/1.10 in(sK13_skl,empty_set)|~sQ25_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f323])).
% 3.09/1.10 fof(f327,plain,(
% 3.09/1.10 ![X0]: (empty(X0)|~in(X0,sK6_skl(X0)))),
% 3.09/1.10 inference(resolution,[status(thm)],[f281,f49])).
% 3.09/1.10 fof(f333,plain,(
% 3.09/1.10 ![X0]: (empty(X0)|empty(powerset(X0))|in(sK8_skl(X0),powerset(X0)))),
% 3.09/1.10 inference(resolution,[status(thm)],[f98,f131])).
% 3.09/1.10 fof(f334,plain,(
% 3.09/1.10 ![X0]: (empty(X0)|in(sK8_skl(X0),powerset(X0)))),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f333,f90])).
% 3.09/1.10 fof(f335,plain,(
% 3.09/1.10 ![X0]: (element(empty_set,powerset(X0)))),
% 3.09/1.10 inference(forward_demodulation,[status(thm)],[f286,f103])).
% 3.09/1.10 fof(f336,plain,(
% 3.09/1.10 relation(empty_set)),
% 3.09/1.10 inference(resolution,[status(thm)],[f335,f52])).
% 3.09/1.10 fof(f337,plain,(
% 3.09/1.10 ![X0]: (empty(powerset(X0))|in(empty_set,powerset(X0)))),
% 3.09/1.10 inference(resolution,[status(thm)],[f335,f131])).
% 3.09/1.10 fof(f338,plain,(
% 3.09/1.10 ![X0]: (in(empty_set,powerset(X0)))),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f337,f90])).
% 3.09/1.10 fof(f352,plain,(
% 3.09/1.10 ![X0]: (is_transitive_in(empty_set,X0)|in(ordered_pair(sK2_skl(X0,empty_set),sK1_skl(X0,empty_set)),empty_set))),
% 3.09/1.10 inference(resolution,[status(thm)],[f336,f68])).
% 3.09/1.10 fof(f359,plain,(
% 3.09/1.10 ~empty(the_InternalRel(sK12_skl))|~sQ6_spl),
% 3.09/1.10 inference(resolution,[status(thm)],[f146,f180])).
% 3.09/1.10 fof(f382,plain,(
% 3.09/1.10 ![X0,X1,X2]: (in(ordered_pair(sK8_skl(X0),X1),cartesian_product2(powerset(X0),X2))|~in(X1,X2)|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f117,f334])).
% 3.09/1.10 fof(f384,plain,(
% 3.09/1.10 ![X0,X1,X2]: (in(ordered_pair(empty_set,X0),cartesian_product2(powerset(X1),X2))|~in(X0,X2))),
% 3.09/1.10 inference(resolution,[status(thm)],[f117,f338])).
% 3.09/1.10 fof(f385,plain,(
% 3.09/1.10 ![X0,X1,X2]: (in(ordered_pair(sK6_skl(X0),X1),cartesian_product2(X0,X2))|~in(X1,X2)|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f117,f281])).
% 3.09/1.10 fof(f386,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(ordered_pair(sK13_skl,sK14_skl),X0),cartesian_product2(the_InternalRel(sK12_skl),X1))|~in(X0,X1)|~sQ6_spl)),
% 3.09/1.10 inference(resolution,[status(thm)],[f117,f180])).
% 3.09/1.10 fof(f387,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(ordered_pair(sK14_skl,sK15_skl),X0),cartesian_product2(the_InternalRel(sK12_skl),X1))|~in(X0,X1)|~sQ4_spl)),
% 3.09/1.10 inference(resolution,[status(thm)],[f117,f173])).
% 3.09/1.10 fof(f403,plain,(
% 3.09/1.10 ![X0]: (element(X0,powerset(X0)))),
% 3.09/1.10 inference(resolution,[status(thm)],[f135,f112])).
% 3.09/1.10 fof(f409,plain,(
% 3.09/1.10 ![X0,X1]: (~element(X0,powerset(X1))|element(sK6_skl(X0),X1)|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f138,f281])).
% 3.09/1.10 fof(f411,plain,(
% 3.09/1.10 ![X0]: (~element(the_InternalRel(sK12_skl),powerset(X0))|element(ordered_pair(sK14_skl,sK15_skl),X0)|~sQ4_spl)),
% 3.09/1.10 inference(resolution,[status(thm)],[f138,f173])).
% 3.09/1.10 fof(f417,plain,(
% 3.09/1.10 ![X0,X1]: (~element(X0,powerset(X1))|~empty(X1)|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f141,f281])).
% 3.09/1.10 fof(f429,plain,(
% 3.09/1.10 ![X0]: (empty(powerset(X0))|in(X0,powerset(X0)))),
% 3.09/1.10 inference(resolution,[status(thm)],[f403,f131])).
% 3.09/1.10 fof(f430,plain,(
% 3.09/1.10 ![X0]: (in(X0,powerset(X0)))),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f429,f90])).
% 3.09/1.10 fof(f476,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(sK8_skl(X0),sK8_skl(X1)),cartesian_product2(powerset(X0),powerset(X1)))|empty(X0)|empty(X1))),
% 3.09/1.10 inference(resolution,[status(thm)],[f382,f334])).
% 3.09/1.10 fof(f478,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(sK8_skl(X0),empty_set),cartesian_product2(powerset(X0),powerset(X1)))|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f382,f338])).
% 3.09/1.10 fof(f479,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(sK8_skl(X0),sK6_skl(X1)),cartesian_product2(powerset(X0),X1))|empty(X0)|empty(X1))),
% 3.09/1.10 inference(resolution,[status(thm)],[f382,f281])).
% 3.09/1.10 fof(f482,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(sK8_skl(X0),X1),cartesian_product2(powerset(X0),powerset(X1)))|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f382,f430])).
% 3.09/1.10 fof(f491,plain,(
% 3.09/1.10 element(the_InternalRel(sK3_skl),powerset(cartesian_product2(the_carrier(sK3_skl),the_carrier(sK3_skl))))),
% 3.09/1.10 inference(resolution,[status(thm)],[f247,f77])).
% 3.09/1.10 fof(f494,plain,(
% 3.09/1.10 ![X0,X1]: (empty(powerset(cartesian_product2(X0,X1)))|in(sK7_skl(X1,X0),powerset(cartesian_product2(X0,X1))))),
% 3.09/1.10 inference(resolution,[status(thm)],[f289,f131])).
% 3.09/1.10 fof(f495,plain,(
% 3.09/1.10 ![X0,X1]: (in(sK7_skl(X0,X1),powerset(cartesian_product2(X1,X0))))),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f494,f90])).
% 3.09/1.10 fof(f513,plain,(
% 3.09/1.10 ~empty(cartesian_product2(the_carrier(sK12_skl),the_carrier(sK12_skl)))|empty(the_InternalRel(sK12_skl))),
% 3.09/1.10 inference(resolution,[status(thm)],[f417,f249])).
% 3.09/1.10 fof(f516,plain,(
% 3.09/1.10 ![X0]: (~empty(X0)|empty(sK6_skl(powerset(X0))))),
% 3.09/1.10 inference(resolution,[status(thm)],[f417,f87])).
% 3.09/1.10 fof(f518,definition,(
% 3.09/1.10 sQ27_spl <=> (empty(cartesian_product2(the_carrier(sK12_skl),the_carrier(sK12_skl))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f521,plain,(
% 3.09/1.10 ~sQ27_spl|sQ16_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f513,f518,f239])).
% 3.09/1.10 fof(f522,definition,(
% 3.09/1.10 ![X0]: (sQ28_spl <=> (~empty(X0)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f523,plain,(
% 3.09/1.10 ![X0]: (~empty(X0)|~sQ28_spl)),
% 3.09/1.10 inference(component_clause,[status(thm)],[f522])).
% 3.09/1.10 fof(f526,plain,(
% 3.09/1.10 empty(sK6_skl(powerset(empty_set)))),
% 3.09/1.10 inference(resolution,[status(thm)],[f516,f91])).
% 3.09/1.10 fof(f532,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(empty_set,sK6_skl(X0)),cartesian_product2(powerset(X1),X0))|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f384,f281])).
% 3.09/1.10 fof(f538,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(sK6_skl(X0),sK8_skl(X1)),cartesian_product2(X0,powerset(X1)))|empty(X0)|empty(X1))),
% 3.09/1.10 inference(resolution,[status(thm)],[f385,f334])).
% 3.09/1.10 fof(f540,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(sK6_skl(X0),empty_set),cartesian_product2(X0,powerset(X1)))|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f385,f338])).
% 3.09/1.10 fof(f541,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(sK6_skl(X0),sK6_skl(X1)),cartesian_product2(X0,X1))|empty(X0)|empty(X1))),
% 3.09/1.10 inference(resolution,[status(thm)],[f385,f281])).
% 3.09/1.10 fof(f542,plain,(
% 3.09/1.10 ![X0]: (in(ordered_pair(sK6_skl(X0),ordered_pair(sK13_skl,sK14_skl)),cartesian_product2(X0,the_InternalRel(sK12_skl)))|empty(X0)|~sQ6_spl)),
% 3.09/1.10 inference(resolution,[status(thm)],[f385,f180])).
% 3.09/1.10 fof(f543,plain,(
% 3.09/1.10 ![X0]: (in(ordered_pair(sK6_skl(X0),ordered_pair(sK14_skl,sK15_skl)),cartesian_product2(X0,the_InternalRel(sK12_skl)))|empty(X0)|~sQ4_spl)),
% 3.09/1.10 inference(resolution,[status(thm)],[f385,f173])).
% 3.09/1.10 fof(f544,plain,(
% 3.09/1.10 ![X0,X1]: (in(ordered_pair(sK6_skl(X0),X1),cartesian_product2(X0,powerset(X1)))|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f385,f430])).
% 3.09/1.10 fof(f552,plain,(
% 3.09/1.10 sK6_skl(powerset(empty_set))=empty_set),
% 3.09/1.10 inference(resolution,[status(thm)],[f526,f143])).
% 3.09/1.10 fof(f555,plain,(
% 3.09/1.10 empty(powerset(empty_set))|~in(powerset(empty_set),empty_set)),
% 3.09/1.10 inference(paramodulation,[status(thm)],[f552,f327])).
% 3.09/1.10 fof(f556,plain,(
% 3.09/1.10 empty(powerset(empty_set))|in(empty_set,powerset(empty_set))),
% 3.09/1.10 inference(paramodulation,[status(thm)],[f552,f281])).
% 3.09/1.10 fof(f558,definition,(
% 3.09/1.10 sQ29_spl <=> (empty(powerset(empty_set)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f559,plain,(
% 3.09/1.10 empty(powerset(empty_set))|~sQ29_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f558])).
% 3.09/1.10 fof(f561,definition,(
% 3.09/1.10 sQ30_spl <=> (in(powerset(empty_set),empty_set))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f564,plain,(
% 3.09/1.10 sQ29_spl|~sQ30_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f555,f558,f561])).
% 3.09/1.10 fof(f565,definition,(
% 3.09/1.10 sQ31_spl <=> (in(empty_set,powerset(empty_set)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f568,plain,(
% 3.09/1.10 sQ29_spl|sQ31_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f556,f558,f565])).
% 3.09/1.10 fof(f569,plain,(
% 3.09/1.10 $false|~sQ29_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f559,f90])).
% 3.09/1.10 fof(f570,plain,(
% 3.09/1.10 ~sQ29_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f569])).
% 3.09/1.10 fof(f580,plain,(
% 3.09/1.10 ![X0]: (is_transitive_in(empty_set,X0)|~empty(empty_set))),
% 3.09/1.10 inference(resolution,[status(thm)],[f352,f146])).
% 3.09/1.10 fof(f583,definition,(
% 3.09/1.10 ![X0]: (sQ32_spl <=> (is_transitive_in(empty_set,X0)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f584,plain,(
% 3.09/1.10 ![X0]: (is_transitive_in(empty_set,X0)|~sQ32_spl)),
% 3.09/1.10 inference(component_clause,[status(thm)],[f583])).
% 3.09/1.10 fof(f586,definition,(
% 3.09/1.10 ![X1]: (sQ33_spl <=> (~element(empty_set,powerset(X1))|~empty(X1)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f587,plain,(
% 3.09/1.10 ![X0]: (~element(empty_set,powerset(X0))|~empty(X0)|~sQ33_spl)),
% 3.09/1.10 inference(component_clause,[status(thm)],[f586])).
% 3.09/1.10 fof(f591,plain,(
% 3.09/1.10 sQ32_spl|~sQ22_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f580,f583,f310])).
% 3.09/1.10 fof(f592,plain,(
% 3.09/1.10 $false|sQ22_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f312,f91])).
% 3.09/1.10 fof(f593,plain,(
% 3.09/1.10 sQ22_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f592])).
% 3.09/1.10 fof(f627,plain,(
% 3.09/1.10 ![X0]: (in(ordered_pair(ordered_pair(sK13_skl,sK14_skl),sK6_skl(X0)),cartesian_product2(the_InternalRel(sK12_skl),X0))|empty(X0)|~sQ6_spl)),
% 3.09/1.10 inference(resolution,[status(thm)],[f386,f281])).
% 3.09/1.10 fof(f641,plain,(
% 3.09/1.10 ![X0]: (in(ordered_pair(ordered_pair(sK14_skl,sK15_skl),sK6_skl(X0)),cartesian_product2(the_InternalRel(sK12_skl),X0))|empty(X0)|~sQ4_spl)),
% 3.09/1.10 inference(resolution,[status(thm)],[f387,f281])).
% 3.09/1.10 fof(f648,plain,(
% 3.09/1.10 ![X0,X1,X2,X3]: (~relation(empty_set)|~in(X0,X1)|~in(X2,X1)|~in(X3,X1)|~in(ordered_pair(X0,X2),empty_set)|~in(ordered_pair(X2,X3),empty_set)|in(ordered_pair(X0,X3),empty_set)|~sQ32_spl)),
% 3.09/1.10 inference(resolution,[status(thm)],[f584,f63])).
% 3.09/1.10 fof(f649,definition,(
% 3.09/1.10 sQ34_spl <=> (relation(empty_set))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f651,plain,(
% 3.09/1.10 ~relation(empty_set)|sQ34_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f649])).
% 3.09/1.10 fof(f652,definition,(
% 3.09/1.10 ![X0,X1,X2,X3]: (sQ35_spl <=> (~in(X0,X1)|~in(X2,X1)|~in(X3,X1)|~in(ordered_pair(X0,X2),empty_set)|~in(ordered_pair(X2,X3),empty_set)|in(ordered_pair(X0,X3),empty_set)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f655,plain,(
% 3.09/1.10 ~sQ34_spl|sQ35_spl|~sQ32_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f648,f649,f652,f583])).
% 3.09/1.10 fof(f656,plain,(
% 3.09/1.10 $false|sQ34_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f651,f336])).
% 3.09/1.10 fof(f657,plain,(
% 3.09/1.10 sQ34_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f656])).
% 3.09/1.10 fof(f667,plain,(
% 3.09/1.10 ![X0,X1,X2]: (in(ordered_pair(sK6_skl(X0),sK7_skl(X1,X2)),cartesian_product2(X0,powerset(cartesian_product2(X2,X1))))|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f495,f385])).
% 3.09/1.10 fof(f690,plain,(
% 3.09/1.10 element(sK6_skl(the_InternalRel(sK12_skl)),cartesian_product2(the_carrier(sK12_skl),the_carrier(sK12_skl)))|empty(the_InternalRel(sK12_skl))),
% 3.09/1.10 inference(resolution,[status(thm)],[f409,f249])).
% 3.09/1.10 fof(f692,plain,(
% 3.09/1.10 ![X0]: (element(sK6_skl(sK8_skl(X0)),X0)|empty(sK8_skl(X0))|empty(X0))),
% 3.09/1.10 inference(resolution,[status(thm)],[f409,f98])).
% 3.09/1.10 fof(f695,definition,(
% 3.09/1.10 sQ36_spl <=> (element(sK6_skl(the_InternalRel(sK12_skl)),cartesian_product2(the_carrier(sK12_skl),the_carrier(sK12_skl))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f698,plain,(
% 3.09/1.10 sQ36_spl|sQ16_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f690,f695,f239])).
% 3.09/1.10 fof(f703,plain,(
% 3.09/1.10 ![X0]: (element(sK6_skl(sK8_skl(X0)),X0)|empty(X0))),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f692,f99])).
% 3.09/1.10 fof(f704,plain,(
% 3.09/1.10 $false|~sQ6_spl|~sQ16_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f240,f359])).
% 3.09/1.10 fof(f705,plain,(
% 3.09/1.10 ~sQ6_spl|~sQ16_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f704])).
% 3.09/1.10 fof(f713,plain,(
% 3.09/1.10 ![X0]: (empty(powerset(X0))|~empty(X0)|empty(sK6_skl(sK8_skl(powerset(X0)))))),
% 3.09/1.10 inference(resolution,[status(thm)],[f703,f417])).
% 3.09/1.10 fof(f718,plain,(
% 3.09/1.10 ![X0]: (~empty(X0)|empty(sK6_skl(sK8_skl(powerset(X0)))))),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f713,f90])).
% 3.09/1.10 fof(f819,plain,(
% 3.09/1.10 ~in(sK15_skl,the_carrier(sK12_skl))|in(ordered_pair(sK13_skl,sK15_skl),the_InternalRel(sK12_skl))|~sQ19_spl|~sQ4_spl),
% 3.09/1.10 inference(resolution,[status(thm)],[f271,f173])).
% 3.09/1.10 fof(f820,definition,(
% 3.09/1.10 sQ38_spl <=> (in(ordered_pair(sK13_skl,sK15_skl),the_InternalRel(sK12_skl)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f821,plain,(
% 3.09/1.10 in(ordered_pair(sK13_skl,sK15_skl),the_InternalRel(sK12_skl))|~sQ38_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f820])).
% 3.09/1.10 fof(f823,plain,(
% 3.09/1.10 ~sQ11_spl|sQ38_spl|~sQ19_spl|~sQ4_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f819,f212,f820,f270,f172])).
% 3.09/1.10 fof(f916,plain,(
% 3.09/1.10 ~rel_str(sK12_skl)|~element(sK13_skl,the_carrier(sK12_skl))|~element(sK15_skl,the_carrier(sK12_skl))|related(sK12_skl,sK13_skl,sK15_skl)|~sQ38_spl),
% 3.09/1.10 inference(resolution,[status(thm)],[f821,f73])).
% 3.09/1.10 fof(f936,definition,(
% 3.09/1.10 sQ40_spl <=> (related(sK12_skl,sK13_skl,sK15_skl))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f937,plain,(
% 3.09/1.10 related(sK12_skl,sK13_skl,sK15_skl)|~sQ40_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f936])).
% 3.09/1.10 fof(f939,plain,(
% 3.09/1.10 ~sQ0_spl|~sQ5_spl|~sQ3_spl|sQ40_spl|~sQ38_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f916,f151,f176,f169,f936,f820])).
% 3.09/1.10 fof(f940,plain,(
% 3.09/1.10 $false|~sQ40_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f937,f129])).
% 3.09/1.10 fof(f941,plain,(
% 3.09/1.10 ~sQ40_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f940])).
% 3.09/1.10 fof(f942,plain,(
% 3.09/1.10 ![X0]: (~empty(X0)|~sQ33_spl)),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f587,f335])).
% 3.09/1.10 fof(f960,plain,(
% 3.09/1.10 $false|~sQ28_spl),
% 3.09/1.10 inference(backward_subsumption_resolution,[status(thm)],[f91,f523])).
% 3.09/1.10 fof(f961,plain,(
% 3.09/1.10 ~sQ28_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f960])).
% 3.09/1.10 fof(f971,plain,(
% 3.09/1.10 $false|~sQ33_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f91,f942])).
% 3.09/1.10 fof(f972,plain,(
% 3.09/1.10 ~sQ33_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f971])).
% 3.09/1.10 fof(f973,plain,(
% 3.09/1.10 ![X0]: (~element(empty_set,powerset(X0))|~empty(X0)|~sQ25_spl)),
% 3.09/1.10 inference(resolution,[status(thm)],[f141,f324])).
% 3.09/1.10 fof(f983,plain,(
% 3.09/1.10 sQ33_spl|~sQ25_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f973,f586,f323])).
% 3.09/1.10 fof(f987,plain,(
% 3.09/1.10 ![X0]: (~empty(powerset(X0)))),
% 3.09/1.10 inference(resolution,[status(thm)],[f146,f338])).
% 3.09/1.10 fof(f993,plain,(
% 3.09/1.10 ~empty(empty_set)|~sQ24_spl),
% 3.09/1.10 inference(resolution,[status(thm)],[f319,f146])).
% 3.09/1.10 fof(f1003,plain,(
% 3.09/1.10 ~sQ22_spl|~sQ24_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f993,f310,f318])).
% 3.09/1.10 fof(f1006,plain,(
% 3.09/1.10 ~empty(empty_set)|~sQ23_spl),
% 3.09/1.10 inference(resolution,[status(thm)],[f314,f146])).
% 3.09/1.10 fof(f1016,plain,(
% 3.09/1.10 ~sQ22_spl|~sQ23_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1006,f310,f313])).
% 3.09/1.10 fof(f1145,plain,(
% 3.09/1.10 element(ordered_pair(sK14_skl,sK15_skl),cartesian_product2(empty_set,empty_set))|~sQ10_spl|~sQ4_spl),
% 3.09/1.10 inference(resolution,[status(thm)],[f303,f411])).
% 3.09/1.10 fof(f1150,definition,(
% 3.09/1.10 sQ43_spl <=> (empty(powerset(cartesian_product2(empty_set,empty_set))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1151,plain,(
% 3.09/1.10 empty(powerset(cartesian_product2(empty_set,empty_set)))|~sQ43_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f1150])).
% 3.09/1.10 fof(f1157,plain,(
% 3.09/1.10 $false|~sQ43_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f1151,f987])).
% 3.09/1.10 fof(f1158,plain,(
% 3.09/1.10 ~sQ43_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f1157])).
% 3.09/1.10 fof(f1214,plain,(
% 3.09/1.10 ~empty(cartesian_product2(empty_set,empty_set))|empty(the_InternalRel(sK12_skl))|~sQ10_spl),
% 3.09/1.10 inference(resolution,[status(thm)],[f417,f303])).
% 3.09/1.10 fof(f1221,definition,(
% 3.09/1.10 sQ48_spl <=> (empty(cartesian_product2(empty_set,empty_set)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1224,plain,(
% 3.09/1.10 ~sQ48_spl|sQ16_spl|~sQ10_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1214,f1221,f239,f209])).
% 3.09/1.10 fof(f1231,plain,(
% 3.09/1.10 relation(the_InternalRel(sK3_skl))),
% 3.09/1.10 inference(resolution,[status(thm)],[f491,f52])).
% 3.09/1.10 fof(f1234,plain,(
% 3.09/1.10 empty(powerset(cartesian_product2(the_carrier(sK3_skl),the_carrier(sK3_skl))))|in(the_InternalRel(sK3_skl),powerset(cartesian_product2(the_carrier(sK3_skl),the_carrier(sK3_skl))))),
% 3.09/1.10 inference(resolution,[status(thm)],[f491,f131])).
% 3.09/1.10 fof(f1242,definition,(
% 3.09/1.10 sQ51_spl <=> (empty(powerset(cartesian_product2(the_carrier(sK3_skl),the_carrier(sK3_skl)))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1243,plain,(
% 3.09/1.10 empty(powerset(cartesian_product2(the_carrier(sK3_skl),the_carrier(sK3_skl))))|~sQ51_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f1242])).
% 3.09/1.10 fof(f1245,definition,(
% 3.09/1.10 sQ52_spl <=> (in(the_InternalRel(sK3_skl),powerset(cartesian_product2(the_carrier(sK3_skl),the_carrier(sK3_skl)))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1248,plain,(
% 3.09/1.10 sQ51_spl|sQ52_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1234,f1242,f1245])).
% 3.09/1.10 fof(f1249,plain,(
% 3.09/1.10 $false|~sQ51_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f1243,f987])).
% 3.09/1.10 fof(f1250,plain,(
% 3.09/1.10 ~sQ51_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f1249])).
% 3.09/1.10 fof(f1280,definition,(
% 3.09/1.10 sQ53_spl <=> (rel_str(sK3_skl))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1282,plain,(
% 3.09/1.10 ~rel_str(sK3_skl)|sQ53_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f1280])).
% 3.09/1.10 fof(f1290,definition,(
% 3.09/1.10 sQ56_spl <=> (is_transitive_in(empty_set,the_carrier(sK3_skl)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1292,plain,(
% 3.09/1.10 ~is_transitive_in(empty_set,the_carrier(sK3_skl))|sQ56_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f1290])).
% 3.09/1.10 fof(f1294,plain,(
% 3.09/1.10 $false|sQ53_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f1282,f81])).
% 3.09/1.10 fof(f1295,plain,(
% 3.09/1.10 sQ53_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f1294])).
% 3.09/1.10 fof(f1296,plain,(
% 3.09/1.10 $false|~sQ32_spl|sQ56_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f1292,f584])).
% 3.09/1.10 fof(f1297,plain,(
% 3.09/1.10 ~sQ32_spl|sQ56_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f1296])).
% 3.09/1.10 fof(f1386,definition,(
% 3.09/1.10 sQ59_spl <=> (relation(the_InternalRel(sK3_skl)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1388,plain,(
% 3.09/1.10 ~relation(the_InternalRel(sK3_skl))|sQ59_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f1386])).
% 3.09/1.10 fof(f1393,plain,(
% 3.09/1.10 $false|sQ59_spl),
% 3.09/1.10 inference(forward_subsumption_resolution,[status(thm)],[f1388,f1231])).
% 3.09/1.10 fof(f1394,plain,(
% 3.09/1.10 sQ59_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f1393])).
% 3.09/1.10 fof(f1444,definition,(
% 3.09/1.10 ![X0]: (sQ61_spl <=> (empty(X0)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1445,plain,(
% 3.09/1.10 ![X0]: (empty(X0)|~sQ61_spl)),
% 3.09/1.10 inference(component_clause,[status(thm)],[f1444])).
% 3.09/1.10 fof(f1448,plain,(
% 3.09/1.10 empty(sK6_skl(sK8_skl(powerset(empty_set))))),
% 3.09/1.10 inference(resolution,[status(thm)],[f718,f91])).
% 3.09/1.10 fof(f1478,plain,(
% 3.09/1.10 sK6_skl(sK8_skl(powerset(empty_set)))=empty_set),
% 3.09/1.10 inference(resolution,[status(thm)],[f1448,f143])).
% 3.09/1.10 fof(f1482,plain,(
% 3.09/1.10 element(empty_set,powerset(empty_set))|empty(powerset(empty_set))),
% 3.09/1.10 inference(paramodulation,[status(thm)],[f1478,f703])).
% 3.09/1.10 fof(f1485,plain,(
% 3.09/1.10 empty(sK8_skl(powerset(empty_set)))|~in(sK8_skl(powerset(empty_set)),empty_set)),
% 3.09/1.10 inference(paramodulation,[status(thm)],[f1478,f327])).
% 3.09/1.10 fof(f1486,plain,(
% 3.09/1.10 empty(sK8_skl(powerset(empty_set)))|in(empty_set,sK8_skl(powerset(empty_set)))),
% 3.09/1.10 inference(paramodulation,[status(thm)],[f1478,f281])).
% 3.09/1.10 fof(f1488,definition,(
% 3.09/1.10 sQ62_spl <=> (element(empty_set,powerset(empty_set)))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1491,plain,(
% 3.09/1.10 sQ62_spl|sQ29_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1482,f1488,f558])).
% 3.09/1.10 fof(f1494,definition,(
% 3.09/1.10 sQ63_spl <=> (empty(sK8_skl(powerset(empty_set))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1495,plain,(
% 3.09/1.10 empty(sK8_skl(powerset(empty_set)))|~sQ63_spl),
% 3.09/1.10 inference(component_clause,[status(thm)],[f1494])).
% 3.09/1.10 fof(f1497,definition,(
% 3.09/1.10 sQ64_spl <=> (in(sK8_skl(powerset(empty_set)),empty_set))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1500,plain,(
% 3.09/1.10 sQ63_spl|~sQ64_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1485,f1494,f1497])).
% 3.09/1.10 fof(f1501,definition,(
% 3.09/1.10 sQ65_spl <=> (in(empty_set,sK8_skl(powerset(empty_set))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1504,plain,(
% 3.09/1.10 sQ63_spl|sQ65_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1486,f1494,f1501])).
% 3.09/1.10 fof(f1505,plain,(
% 3.09/1.10 empty(powerset(empty_set))|~sQ63_spl),
% 3.09/1.10 inference(resolution,[status(thm)],[f1495,f99])).
% 3.09/1.10 fof(f1510,plain,(
% 3.09/1.10 sQ29_spl|~sQ63_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1505,f558,f1494])).
% 3.09/1.10 fof(f1552,plain,(
% 3.09/1.10 ![X0,X1]: (empty(X0)|empty(X1)|in(sK8_skl(X1),powerset(X1)))),
% 3.09/1.10 inference(resolution,[status(thm)],[f476,f116])).
% 3.09/1.10 fof(f1566,definition,(
% 3.09/1.10 ![X1]: (sQ67_spl <=> (empty(X1)|in(sK8_skl(X1),powerset(X1))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1569,plain,(
% 3.09/1.10 sQ61_spl|sQ67_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1552,f1444,f1566])).
% 3.09/1.10 fof(f1571,plain,(
% 3.09/1.10 ![X0,X1]: (empty(X0)|in(empty_set,powerset(X1)))),
% 3.09/1.10 inference(resolution,[status(thm)],[f478,f116])).
% 3.09/1.10 fof(f1585,definition,(
% 3.09/1.10 ![X1]: (sQ68_spl <=> (in(empty_set,powerset(X1))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1588,plain,(
% 3.09/1.10 sQ61_spl|sQ68_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1571,f1444,f1585])).
% 3.09/1.10 fof(f1594,plain,(
% 3.09/1.10 $false|~sQ61_spl),
% 3.09/1.10 inference(backward_subsumption_resolution,[status(thm)],[f282,f1445])).
% 3.09/1.10 fof(f1604,plain,(
% 3.09/1.10 ~sQ61_spl),
% 3.09/1.10 inference(contradiction_clause,[status(thm)],[f1594])).
% 3.09/1.10 fof(f1735,plain,(
% 3.09/1.10 in(ordered_pair(empty_set,ordered_pair(sK13_skl,sK14_skl)),cartesian_product2(sK8_skl(powerset(empty_set)),the_InternalRel(sK12_skl)))|empty(sK8_skl(powerset(empty_set)))|~sQ6_spl),
% 3.09/1.10 inference(paramodulation,[status(thm)],[f1478,f542])).
% 3.09/1.10 fof(f1737,plain,(
% 3.09/1.10 in(ordered_pair(empty_set,ordered_pair(sK13_skl,sK14_skl)),cartesian_product2(powerset(empty_set),the_InternalRel(sK12_skl)))|empty(powerset(empty_set))|~sQ6_spl),
% 3.09/1.10 inference(paramodulation,[status(thm)],[f552,f542])).
% 3.09/1.10 fof(f1739,definition,(
% 3.09/1.10 sQ69_spl <=> (in(ordered_pair(empty_set,ordered_pair(sK13_skl,sK14_skl)),cartesian_product2(sK8_skl(powerset(empty_set)),the_InternalRel(sK12_skl))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1742,plain,(
% 3.09/1.10 sQ69_spl|sQ63_spl|~sQ6_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1735,f1739,f1494,f179])).
% 3.09/1.10 fof(f1747,definition,(
% 3.09/1.10 sQ71_spl <=> (in(ordered_pair(empty_set,ordered_pair(sK13_skl,sK14_skl)),cartesian_product2(powerset(empty_set),the_InternalRel(sK12_skl))))),
% 3.09/1.10 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 3.09/1.10 fof(f1750,plain,(
% 3.09/1.10 sQ71_spl|sQ29_spl|~sQ6_spl),
% 3.09/1.10 inference(split_clause,[status(thm)],[f1737,f1747,f558,f179])).
% 3.09/1.10 fof(f1793,plain,(
% 3.09/1.10 in(ordered_pair(empty_set,ordered_pair(sK14_skl,sK15_skl)),cartesian_product2(sK8_skl(powerset(empty_set)),the_InternalRel(sK12_skl)))|empty(sK8_skl(powerset(empty_set)))|~sQ4_spl),
% 3.09/1.10 inference(paramodulation,[status(thm)],[f1478,f543])).
% 3.09/1.10 fof(f1794,plain,(
% 3.09/1.10 in(ordered_pair(empty_set,ordered_pair(sK14_skl,sK15_skl)),cartesian_product2(powerset(empty_set),the_InternalRel(sK12_skl)))|empty(powerset(empty_set))|~sQ4_spl),
% 3.09/1.10 inference(paramodulation,[status(thm)],[f552,f543])).
% 3.09/1.10 fof(f1800,definition,(
% 3.09/1.10 sQ76_spl <=> (in(ordered_pair(empty_set,ordered_pair(sK14_skl,sK15_skl)),cartesian_product2(sK8_skl(powerset(empty_set)),the_InternalRel(sK12_skl))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f1803,plain,(
% 3.09/1.11 sQ76_spl|sQ63_spl|~sQ4_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f1793,f1800,f1494,f172])).
% 3.09/1.11 fof(f1804,definition,(
% 3.09/1.11 sQ77_spl <=> (in(ordered_pair(empty_set,ordered_pair(sK14_skl,sK15_skl)),cartesian_product2(powerset(empty_set),the_InternalRel(sK12_skl))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f1807,plain,(
% 3.09/1.11 sQ77_spl|sQ29_spl|~sQ4_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f1794,f1804,f558,f172])).
% 3.09/1.11 fof(f2050,plain,(
% 3.09/1.11 in(ordered_pair(ordered_pair(sK13_skl,sK14_skl),empty_set),cartesian_product2(the_InternalRel(sK12_skl),sK8_skl(powerset(empty_set))))|empty(sK8_skl(powerset(empty_set)))|~sQ6_spl),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f1478,f627])).
% 3.09/1.11 fof(f2051,plain,(
% 3.09/1.11 in(ordered_pair(ordered_pair(sK13_skl,sK14_skl),empty_set),cartesian_product2(the_InternalRel(sK12_skl),powerset(empty_set)))|empty(powerset(empty_set))|~sQ6_spl),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f552,f627])).
% 3.09/1.11 fof(f2053,definition,(
% 3.09/1.11 sQ79_spl <=> (in(ordered_pair(ordered_pair(sK13_skl,sK14_skl),empty_set),cartesian_product2(the_InternalRel(sK12_skl),sK8_skl(powerset(empty_set)))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2056,plain,(
% 3.09/1.11 sQ79_spl|sQ63_spl|~sQ6_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2050,f2053,f1494,f179])).
% 3.09/1.11 fof(f2057,definition,(
% 3.09/1.11 sQ80_spl <=> (in(ordered_pair(ordered_pair(sK13_skl,sK14_skl),empty_set),cartesian_product2(the_InternalRel(sK12_skl),powerset(empty_set))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2060,plain,(
% 3.09/1.11 sQ80_spl|sQ29_spl|~sQ6_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2051,f2057,f558,f179])).
% 3.09/1.11 fof(f2061,plain,(
% 3.09/1.11 ![X0,X1]: (empty(X0)|empty(X1)|in(sK6_skl(X1),X1))),
% 3.09/1.11 inference(resolution,[status(thm)],[f479,f116])).
% 3.09/1.11 fof(f2075,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(sK8_skl(X0),empty_set),cartesian_product2(powerset(X0),sK8_skl(powerset(empty_set))))|empty(X0)|empty(sK8_skl(powerset(empty_set))))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f1478,f479])).
% 3.09/1.11 fof(f2076,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(sK8_skl(X0),empty_set),cartesian_product2(powerset(X0),powerset(empty_set)))|empty(X0)|empty(powerset(empty_set)))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f552,f479])).
% 3.09/1.11 fof(f2077,definition,(
% 3.09/1.11 ![X1]: (sQ81_spl <=> (empty(X1)|in(sK6_skl(X1),X1)))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2080,plain,(
% 3.09/1.11 sQ61_spl|sQ81_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2061,f1444,f2077])).
% 3.09/1.11 fof(f2082,definition,(
% 3.09/1.11 ![X0]: (sQ82_spl <=> (in(ordered_pair(sK8_skl(X0),empty_set),cartesian_product2(powerset(X0),sK8_skl(powerset(empty_set))))|empty(X0)))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2085,plain,(
% 3.09/1.11 sQ82_spl|sQ63_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2075,f2082,f1494])).
% 3.09/1.11 fof(f2086,definition,(
% 3.09/1.11 ![X0]: (sQ83_spl <=> (in(ordered_pair(sK8_skl(X0),empty_set),cartesian_product2(powerset(X0),powerset(empty_set)))|empty(X0)))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2089,plain,(
% 3.09/1.11 sQ83_spl|sQ29_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2076,f2086,f558])).
% 3.09/1.11 fof(f2090,plain,(
% 3.09/1.11 ![X0,X1]: (empty(X0)|in(X1,powerset(X1)))),
% 3.09/1.11 inference(resolution,[status(thm)],[f482,f116])).
% 3.09/1.11 fof(f2104,definition,(
% 3.09/1.11 ![X1]: (sQ84_spl <=> (in(X1,powerset(X1))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2107,plain,(
% 3.09/1.11 sQ61_spl|sQ84_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2090,f1444,f2104])).
% 3.09/1.11 fof(f2188,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(empty_set,empty_set),cartesian_product2(powerset(X0),sK8_skl(powerset(empty_set))))|empty(sK8_skl(powerset(empty_set))))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f1478,f532])).
% 3.09/1.11 fof(f2189,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(empty_set,empty_set),cartesian_product2(powerset(X0),powerset(empty_set)))|empty(powerset(empty_set)))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f552,f532])).
% 3.09/1.11 fof(f2191,definition,(
% 3.09/1.11 ![X0]: (sQ85_spl <=> (in(ordered_pair(empty_set,empty_set),cartesian_product2(powerset(X0),sK8_skl(powerset(empty_set))))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2194,plain,(
% 3.09/1.11 sQ85_spl|sQ63_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2188,f2191,f1494])).
% 3.09/1.11 fof(f2195,definition,(
% 3.09/1.11 ![X0]: (sQ86_spl <=> (in(ordered_pair(empty_set,empty_set),cartesian_product2(powerset(X0),powerset(empty_set)))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2198,plain,(
% 3.09/1.11 sQ86_spl|sQ29_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2189,f2195,f558])).
% 3.09/1.11 fof(f2249,plain,(
% 3.09/1.11 empty(cartesian_product2(empty_set,empty_set))|in(ordered_pair(sK14_skl,sK15_skl),cartesian_product2(empty_set,empty_set))|~sQ10_spl|~sQ4_spl),
% 3.09/1.11 inference(resolution,[status(thm)],[f1145,f131])).
% 3.09/1.11 fof(f2250,definition,(
% 3.09/1.11 sQ87_spl <=> (in(ordered_pair(sK14_skl,sK15_skl),cartesian_product2(empty_set,empty_set)))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2251,plain,(
% 3.09/1.11 in(ordered_pair(sK14_skl,sK15_skl),cartesian_product2(empty_set,empty_set))|~sQ87_spl),
% 3.09/1.11 inference(component_clause,[status(thm)],[f2250])).
% 3.09/1.11 fof(f2253,plain,(
% 3.09/1.11 sQ48_spl|sQ87_spl|~sQ10_spl|~sQ4_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2249,f1221,f2250,f209,f172])).
% 3.09/1.11 fof(f2282,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(empty_set,sK8_skl(X0)),cartesian_product2(sK8_skl(powerset(empty_set)),powerset(X0)))|empty(sK8_skl(powerset(empty_set)))|empty(X0))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f1478,f538])).
% 3.09/1.11 fof(f2283,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(empty_set,sK8_skl(X0)),cartesian_product2(powerset(empty_set),powerset(X0)))|empty(powerset(empty_set))|empty(X0))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f552,f538])).
% 3.09/1.11 fof(f2286,definition,(
% 3.09/1.11 ![X0]: (sQ88_spl <=> (in(ordered_pair(empty_set,sK8_skl(X0)),cartesian_product2(sK8_skl(powerset(empty_set)),powerset(X0)))|empty(X0)))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2289,plain,(
% 3.09/1.11 sQ88_spl|sQ63_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2282,f2286,f1494])).
% 3.09/1.11 fof(f2290,definition,(
% 3.09/1.11 ![X0]: (sQ89_spl <=> (in(ordered_pair(empty_set,sK8_skl(X0)),cartesian_product2(powerset(empty_set),powerset(X0)))|empty(X0)))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2293,plain,(
% 3.09/1.11 sQ89_spl|sQ29_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2283,f2290,f558])).
% 3.09/1.11 fof(f2308,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(empty_set,empty_set),cartesian_product2(sK8_skl(powerset(empty_set)),powerset(X0)))|empty(sK8_skl(powerset(empty_set))))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f1478,f540])).
% 3.09/1.11 fof(f2309,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(empty_set,empty_set),cartesian_product2(powerset(empty_set),powerset(X0)))|empty(powerset(empty_set)))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f552,f540])).
% 3.09/1.11 fof(f2311,definition,(
% 3.09/1.11 ![X0]: (sQ90_spl <=> (in(ordered_pair(empty_set,empty_set),cartesian_product2(sK8_skl(powerset(empty_set)),powerset(X0)))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2314,plain,(
% 3.09/1.11 sQ90_spl|sQ63_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2308,f2311,f1494])).
% 3.09/1.11 fof(f2315,definition,(
% 3.09/1.11 ![X0]: (sQ91_spl <=> (in(ordered_pair(empty_set,empty_set),cartesian_product2(powerset(empty_set),powerset(X0)))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2318,plain,(
% 3.09/1.11 sQ91_spl|sQ29_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2309,f2315,f558])).
% 3.09/1.11 fof(f2336,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(empty_set,sK6_skl(X0)),cartesian_product2(sK8_skl(powerset(empty_set)),X0))|empty(sK8_skl(powerset(empty_set)))|empty(X0))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f1478,f541])).
% 3.09/1.11 fof(f2337,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(empty_set,sK6_skl(X0)),cartesian_product2(powerset(empty_set),X0))|empty(powerset(empty_set))|empty(X0))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f552,f541])).
% 3.09/1.11 fof(f2338,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(sK6_skl(X0),empty_set),cartesian_product2(X0,sK8_skl(powerset(empty_set))))|empty(X0)|empty(sK8_skl(powerset(empty_set))))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f1478,f541])).
% 3.09/1.11 fof(f2339,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(sK6_skl(X0),empty_set),cartesian_product2(X0,powerset(empty_set)))|empty(X0)|empty(powerset(empty_set)))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f552,f541])).
% 3.09/1.11 fof(f2342,definition,(
% 3.09/1.11 ![X0]: (sQ92_spl <=> (in(ordered_pair(empty_set,sK6_skl(X0)),cartesian_product2(sK8_skl(powerset(empty_set)),X0))|empty(X0)))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2345,plain,(
% 3.09/1.11 sQ92_spl|sQ63_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2336,f2342,f1494])).
% 3.09/1.11 fof(f2346,definition,(
% 3.09/1.11 ![X0]: (sQ93_spl <=> (in(ordered_pair(empty_set,sK6_skl(X0)),cartesian_product2(powerset(empty_set),X0))|empty(X0)))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2349,plain,(
% 3.09/1.11 sQ93_spl|sQ29_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2337,f2346,f558])).
% 3.09/1.11 fof(f2350,definition,(
% 3.09/1.11 ![X0]: (sQ94_spl <=> (in(ordered_pair(sK6_skl(X0),empty_set),cartesian_product2(X0,sK8_skl(powerset(empty_set))))|empty(X0)))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2353,plain,(
% 3.09/1.11 sQ94_spl|sQ63_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2338,f2350,f1494])).
% 3.09/1.11 fof(f2354,definition,(
% 3.09/1.11 ![X0]: (sQ95_spl <=> (in(ordered_pair(sK6_skl(X0),empty_set),cartesian_product2(X0,powerset(empty_set)))|empty(X0)))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2357,plain,(
% 3.09/1.11 sQ95_spl|sQ29_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2339,f2354,f558])).
% 3.09/1.11 fof(f2372,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(empty_set,X0),cartesian_product2(sK8_skl(powerset(empty_set)),powerset(X0)))|empty(sK8_skl(powerset(empty_set))))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f1478,f544])).
% 3.09/1.11 fof(f2373,plain,(
% 3.09/1.11 ![X0]: (in(ordered_pair(empty_set,X0),cartesian_product2(powerset(empty_set),powerset(X0)))|empty(powerset(empty_set)))),
% 3.09/1.11 inference(paramodulation,[status(thm)],[f552,f544])).
% 3.09/1.11 fof(f2375,definition,(
% 3.09/1.11 ![X0]: (sQ96_spl <=> (in(ordered_pair(empty_set,X0),cartesian_product2(sK8_skl(powerset(empty_set)),powerset(X0)))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2378,plain,(
% 3.09/1.11 sQ96_spl|sQ63_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2372,f2375,f1494])).
% 3.09/1.11 fof(f2379,definition,(
% 3.09/1.11 ![X0]: (sQ97_spl <=> (in(ordered_pair(empty_set,X0),cartesian_product2(powerset(empty_set),powerset(X0)))))),
% 3.09/1.11 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 3.09/1.11 fof(f2382,plain,(
% 3.09/1.11 sQ97_spl|sQ29_spl),
% 3.09/1.11 inference(split_clause,[status(thm)],[f2373,f2379,f558])).
% 3.09/1.11 fof(f2541,plain,(
% 3.09/1.12 in(ordered_pair(ordered_pair(sK14_skl,sK15_skl),empty_set),cartesian_product2(the_InternalRel(sK12_skl),sK8_skl(powerset(empty_set))))|empty(sK8_skl(powerset(empty_set)))|~sQ4_spl),
% 3.09/1.12 inference(paramodulation,[status(thm)],[f1478,f641])).
% 3.09/1.12 fof(f2542,plain,(
% 3.09/1.12 in(ordered_pair(ordered_pair(sK14_skl,sK15_skl),empty_set),cartesian_product2(the_InternalRel(sK12_skl),powerset(empty_set)))|empty(powerset(empty_set))|~sQ4_spl),
% 3.09/1.12 inference(paramodulation,[status(thm)],[f552,f641])).
% 3.09/1.12 fof(f2544,definition,(
% 3.09/1.12 sQ100_spl <=> (in(ordered_pair(ordered_pair(sK14_skl,sK15_skl),empty_set),cartesian_product2(the_InternalRel(sK12_skl),sK8_skl(powerset(empty_set)))))),
% 3.09/1.12 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 3.09/1.12 fof(f2547,plain,(
% 3.09/1.12 sQ100_spl|sQ63_spl|~sQ4_spl),
% 3.09/1.12 inference(split_clause,[status(thm)],[f2541,f2544,f1494,f172])).
% 3.09/1.12 fof(f2548,definition,(
% 3.09/1.12 sQ101_spl <=> (in(ordered_pair(ordered_pair(sK14_skl,sK15_skl),empty_set),cartesian_product2(the_InternalRel(sK12_skl),powerset(empty_set))))),
% 3.09/1.12 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 3.09/1.12 fof(f2551,plain,(
% 3.09/1.12 sQ101_spl|sQ29_spl|~sQ4_spl),
% 3.09/1.12 inference(split_clause,[status(thm)],[f2542,f2548,f558,f172])).
% 3.09/1.12 fof(f2632,plain,(
% 3.09/1.12 ![X0,X1,X2]: (empty(X0)|in(sK7_skl(X1,X2),powerset(cartesian_product2(X2,X1))))),
% 3.09/1.12 inference(resolution,[status(thm)],[f667,f116])).
% 3.09/1.12 fof(f2646,plain,(
% 3.09/1.12 ![X0,X1]: (in(ordered_pair(empty_set,sK7_skl(X0,X1)),cartesian_product2(sK8_skl(powerset(empty_set)),powerset(cartesian_product2(X1,X0))))|empty(sK8_skl(powerset(empty_set))))),
% 3.09/1.12 inference(paramodulation,[status(thm)],[f1478,f667])).
% 3.09/1.12 fof(f2647,plain,(
% 3.09/1.12 ![X0,X1]: (in(ordered_pair(empty_set,sK7_skl(X0,X1)),cartesian_product2(powerset(empty_set),powerset(cartesian_product2(X1,X0))))|empty(powerset(empty_set)))),
% 3.09/1.12 inference(paramodulation,[status(thm)],[f552,f667])).
% 3.09/1.12 fof(f2648,definition,(
% 3.09/1.12 ![X1,X2]: (sQ102_spl <=> (in(sK7_skl(X1,X2),powerset(cartesian_product2(X2,X1)))))),
% 3.09/1.12 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 3.09/1.12 fof(f2651,plain,(
% 3.09/1.12 sQ61_spl|sQ102_spl),
% 3.09/1.12 inference(split_clause,[status(thm)],[f2632,f1444,f2648])).
% 3.09/1.12 fof(f2652,definition,(
% 3.09/1.12 ![X0,X1]: (sQ103_spl <=> (in(ordered_pair(empty_set,sK7_skl(X0,X1)),cartesian_product2(sK8_skl(powerset(empty_set)),powerset(cartesian_product2(X1,X0))))))),
% 3.09/1.12 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 3.09/1.12 fof(f2655,plain,(
% 3.09/1.12 sQ103_spl|sQ63_spl),
% 3.09/1.12 inference(split_clause,[status(thm)],[f2646,f2652,f1494])).
% 3.09/1.12 fof(f2656,definition,(
% 3.09/1.12 ![X0,X1]: (sQ104_spl <=> (in(ordered_pair(empty_set,sK7_skl(X0,X1)),cartesian_product2(powerset(empty_set),powerset(cartesian_product2(X1,X0))))))),
% 3.09/1.12 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 3.09/1.12 fof(f2659,plain,(
% 3.09/1.12 sQ104_spl|sQ29_spl),
% 3.09/1.12 inference(split_clause,[status(thm)],[f2647,f2656,f558])).
% 3.09/1.12 fof(f2754,plain,(
% 3.09/1.12 in(sK14_skl,empty_set)|~sQ87_spl),
% 3.09/1.12 inference(resolution,[status(thm)],[f2251,f115])).
% 3.09/1.12 fof(f2769,plain,(
% 3.09/1.12 sQ24_spl|~sQ87_spl),
% 3.09/1.12 inference(split_clause,[status(thm)],[f2754,f318,f2250])).
% 3.09/1.12 fof(f2770,plain,(
% 3.09/1.12 $false),
% 3.09/1.12 inference(sat_refutation,[status(thm)],[f157,f159,f175,f182,f184,f186,f188,f198,f205,f215,f219,f223,f230,f237,f253,f260,f262,f273,f521,f564,f568,f570,f591,f593,f655,f657,f698,f705,f823,f939,f941,f961,f972,f983,f1003,f1016,f1158,f1224,f1248,f1250,f1295,f1297,f1394,f1491,f1500,f1504,f1510,f1569,f1588,f1604,f1742,f1750,f1803,f1807,f2056,f2060,f2080,f2085,f2089,f2107,f2194,f2198,f2253,f2289,f2293,f2314,f2318,f2345,f2349,f2353,f2357,f2378,f2382,f2547,f2551,f2651,f2655,f2659,f2769])).
% 3.09/1.12 % SZS output end CNFRefutation for theBenchmark.p
% 0.38/1.13 % Elapsed time: 0.666220 seconds
% 0.38/1.13 % CPU time: 4.643767 seconds
% 0.38/1.13 % Total memory used: 160.135 MB
% 0.38/1.13 % Net memory used: 156.921 MB
%------------------------------------------------------------------------------