%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU356+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 : n010.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:25 PM UTC 2026
% Result : Theorem 0.10s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU356+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n010.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 06:15:09 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.41 % Refutation found
% 0.10/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.41 fof(f1,axiom,(
% 0.10/0.41 (! [A] :( rel_str(A)=> (! [B] :( ex_sup_of_relstr_set(A,B)<=> (? [C] :( element(C,the_carrier(A))& relstr_set_smaller(A,B,C)& (! [D] :( element(D,the_carrier(A))=> ( relstr_set_smaller(A,B,D)=> related(A,C,D) ) ))& (! [D] :( element(D,the_carrier(A))=> ( ( relstr_set_smaller(A,B,D)& (! [E] :( element(E,the_carrier(A))=> ( relstr_set_smaller(A,B,E)=> related(A,D,E) ) ) ))=> D = C ) ) )) )) )) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f9,conjecture,(
% 0.10/0.41 (! [A] :( ( antisymmetric_relstr(A)& rel_str(A) )=> (! [B] :( ex_sup_of_relstr_set(A,B)<=> (? [C] :( element(C,the_carrier(A))& relstr_set_smaller(A,B,C)& (! [D] :( element(D,the_carrier(A))=> ( relstr_set_smaller(A,B,D)=> related(A,C,D) ) ) )) )) )) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f10,negated_conjecture,(
% 0.10/0.41 ~((! [A] :( ( antisymmetric_relstr(A)& rel_str(A) )=> (! [B] :( ex_sup_of_relstr_set(A,B)<=> (? [C] :( element(C,the_carrier(A))& relstr_set_smaller(A,B,C)& (! [D] :( element(D,the_carrier(A))=> ( relstr_set_smaller(A,B,D)=> related(A,C,D) ) ) )) )) )) ))),
% 0.10/0.41 inference(negated_conjecture,[status(cth)],[f9])).
% 0.10/0.41 fof(f11,axiom,(
% 0.10/0.41 (! [A] :( ( antisymmetric_relstr(A)& rel_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> ( ( related(A,B,C)& related(A,C,B) )=> B = C ) ) )) )) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f12,plain,(
% 0.10/0.41 ![A]: (~rel_str(A)|(![B]: (ex_sup_of_relstr_set(A,B)<=>(?[C]: (((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D)))))&(![D]: (~element(D,the_carrier(A))|((~relstr_set_smaller(A,B,D)|(?[E]: (element(E,the_carrier(A))&(relstr_set_smaller(A,B,E)&~related(A,D,E)))))|D=C))))))))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.10/0.41 fof(f13,plain,(
% 0.10/0.41 ![A]: (~rel_str(A)|(![B]: ((~ex_sup_of_relstr_set(A,B)|(?[C]: (((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D)))))&(![D]: (~element(D,the_carrier(A))|((~relstr_set_smaller(A,B,D)|(?[E]: (element(E,the_carrier(A))&(relstr_set_smaller(A,B,E)&~related(A,D,E)))))|D=C))))))&(ex_sup_of_relstr_set(A,B)|(![C]: (((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,B,D)&~related(A,C,D)))))|(?[D]: (element(D,the_carrier(A))&((relstr_set_smaller(A,B,D)&(![E]: (~element(E,the_carrier(A))|(~relstr_set_smaller(A,B,E)|related(A,D,E)))))&~D=C)))))))))),
% 0.10/0.41 inference(NNF_transformation,[status(thm)],[f12])).
% 0.10/0.41 fof(f14,plain,(
% 0.10/0.41 ![A]: (~rel_str(A)|((![B]: (~ex_sup_of_relstr_set(A,B)|(?[C]: (((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D)))))&(![D]: (~element(D,the_carrier(A))|((~relstr_set_smaller(A,B,D)|(?[E]: (element(E,the_carrier(A))&(relstr_set_smaller(A,B,E)&~related(A,D,E)))))|D=C)))))))&(![B]: (ex_sup_of_relstr_set(A,B)|(![C]: (((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,B,D)&~related(A,C,D)))))|(?[D]: (element(D,the_carrier(A))&((relstr_set_smaller(A,B,D)&(![E]: (~element(E,the_carrier(A))|(~relstr_set_smaller(A,B,E)|related(A,D,E)))))&~D=C)))))))))),
% 0.10/0.41 inference(miniscoping,[status(thm)],[f13])).
% 0.10/0.41 fof(f15,plain,(
% 0.10/0.41 ![A]: (~rel_str(A)|((![B]: (~ex_sup_of_relstr_set(A,B)|(((element(sK0_skl(B,A),the_carrier(A))&relstr_set_smaller(A,B,sK0_skl(B,A)))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,sK0_skl(B,A),D)))))&(![D]: (~element(D,the_carrier(A))|((~relstr_set_smaller(A,B,D)|(element(sK1_skl(D,B,A),the_carrier(A))&(relstr_set_smaller(A,B,sK1_skl(D,B,A))&~related(A,D,sK1_skl(D,B,A)))))|D=sK0_skl(B,A)))))))&(![B]: (ex_sup_of_relstr_set(A,B)|(![C]: (((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(element(sK2_skl(C,B,A),the_carrier(A))&(relstr_set_smaller(A,B,sK2_skl(C,B,A))&~related(A,C,sK2_skl(C,B,A)))))|(element(sK3_skl(C,B,A),the_carrier(A))&((relstr_set_smaller(A,B,sK3_skl(C,B,A))&(![E]: (~element(E,the_carrier(A))|(~relstr_set_smaller(A,B,E)|related(A,sK3_skl(C,B,A),E)))))&~sK3_skl(C,B,A)=C))))))))),
% 0.10/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(C,sK0_skl(B,A)),skolemize(E,sK1_skl(D,B,A)),skolemize(D,sK2_skl(C,B,A)),skolemize(D,sK3_skl(C,B,A))],[f14])).
% 0.10/0.41 fof(f16,plain,(
% 0.10/0.41 ![X0,X1]: (~rel_str(X0)|~ex_sup_of_relstr_set(X0,X1)|element(sK0_skl(X1,X0),the_carrier(X0)))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f17,plain,(
% 0.10/0.41 ![X0,X1]: (~rel_str(X0)|~ex_sup_of_relstr_set(X0,X1)|relstr_set_smaller(X0,X1,sK0_skl(X1,X0)))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f18,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|~ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|related(X0,sK0_skl(X1,X0),X2))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f19,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|~ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|element(sK1_skl(X2,X1,X0),the_carrier(X0))|X2=sK0_skl(X1,X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f20,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|~ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|relstr_set_smaller(X0,X1,sK1_skl(X2,X1,X0))|X2=sK0_skl(X1,X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f21,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|~ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|~related(X0,X2,sK1_skl(X2,X1,X0))|X2=sK0_skl(X1,X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f22,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|element(sK2_skl(X2,X1,X0),the_carrier(X0))|element(sK3_skl(X2,X1,X0),the_carrier(X0)))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f23,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|element(sK2_skl(X2,X1,X0),the_carrier(X0))|relstr_set_smaller(X0,X1,sK3_skl(X2,X1,X0)))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f24,plain,(
% 0.10/0.41 ![X0,X1,X2,X3]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|element(sK2_skl(X2,X1,X0),the_carrier(X0))|~element(X3,the_carrier(X0))|~relstr_set_smaller(X0,X1,X3)|related(X0,sK3_skl(X2,X1,X0),X3))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f25,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|element(sK2_skl(X2,X1,X0),the_carrier(X0))|~sK3_skl(X2,X1,X0)=X2)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f26,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|relstr_set_smaller(X0,X1,sK2_skl(X2,X1,X0))|element(sK3_skl(X2,X1,X0),the_carrier(X0)))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f27,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|relstr_set_smaller(X0,X1,sK2_skl(X2,X1,X0))|relstr_set_smaller(X0,X1,sK3_skl(X2,X1,X0)))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f28,plain,(
% 0.10/0.41 ![X0,X1,X2,X3]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|relstr_set_smaller(X0,X1,sK2_skl(X2,X1,X0))|~element(X3,the_carrier(X0))|~relstr_set_smaller(X0,X1,X3)|related(X0,sK3_skl(X2,X1,X0),X3))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f29,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|relstr_set_smaller(X0,X1,sK2_skl(X2,X1,X0))|~sK3_skl(X2,X1,X0)=X2)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.41 fof(f30,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|~related(X0,X2,sK2_skl(X2,X1,X0))|element(sK3_skl(X2,X1,X0),the_carrier(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.42 fof(f31,plain,(
% 0.10/0.42 ![X0,X1,X2]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|~related(X0,X2,sK2_skl(X2,X1,X0))|relstr_set_smaller(X0,X1,sK3_skl(X2,X1,X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.42 fof(f32,plain,(
% 0.10/0.42 ![X0,X1,X2,X3]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|~related(X0,X2,sK2_skl(X2,X1,X0))|~element(X3,the_carrier(X0))|~relstr_set_smaller(X0,X1,X3)|related(X0,sK3_skl(X2,X1,X0),X3))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.42 fof(f33,plain,(
% 0.10/0.42 ![X0,X1,X2]: (~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|~related(X0,X2,sK2_skl(X2,X1,X0))|~sK3_skl(X2,X1,X0)=X2)),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.42 fof(f42,plain,(
% 0.10/0.42 (?[A]: ((antisymmetric_relstr(A)&rel_str(A))&(?[B]: (ex_sup_of_relstr_set(A,B)<~>(?[C]: ((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D))))))))))),
% 0.10/0.42 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.10/0.42 fof(f43,plain,(
% 0.10/0.42 ?[A]: ((antisymmetric_relstr(A)&rel_str(A))&(?[B]: ((ex_sup_of_relstr_set(A,B)|(?[C]: ((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D)))))))&(~ex_sup_of_relstr_set(A,B)|(![C]: ((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,B,D)&~related(A,C,D))))))))))),
% 0.10/0.42 inference(NNF_transformation,[status(thm)],[f42])).
% 0.10/0.42 fof(f44,plain,(
% 0.10/0.42 ((antisymmetric_relstr(sK7_skl)&rel_str(sK7_skl))&((ex_sup_of_relstr_set(sK7_skl,sK8_skl)|((element(sK9_skl,the_carrier(sK7_skl))&relstr_set_smaller(sK7_skl,sK8_skl,sK9_skl))&(![D]: (~element(D,the_carrier(sK7_skl))|(~relstr_set_smaller(sK7_skl,sK8_skl,D)|related(sK7_skl,sK9_skl,D))))))&(~ex_sup_of_relstr_set(sK7_skl,sK8_skl)|(![C]: ((~element(C,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,C))|(element(sK10_skl(C),the_carrier(sK7_skl))&(relstr_set_smaller(sK7_skl,sK8_skl,sK10_skl(C))&~related(sK7_skl,C,sK10_skl(C)))))))))),
% 0.10/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl,sK10_skl]),skolemize(A,sK7_skl),skolemize(B,sK8_skl),skolemize(C,sK9_skl),skolemize(D,sK10_skl(C))],[f43])).
% 0.10/0.42 fof(f45,plain,(
% 0.10/0.42 antisymmetric_relstr(sK7_skl)),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.42 fof(f46,plain,(
% 0.10/0.42 rel_str(sK7_skl)),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.42 fof(f47,plain,(
% 0.10/0.42 ex_sup_of_relstr_set(sK7_skl,sK8_skl)|element(sK9_skl,the_carrier(sK7_skl))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.42 fof(f48,plain,(
% 0.10/0.42 ex_sup_of_relstr_set(sK7_skl,sK8_skl)|relstr_set_smaller(sK7_skl,sK8_skl,sK9_skl)),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.42 fof(f49,plain,(
% 0.10/0.42 ![X0]: (ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,sK9_skl,X0))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.42 fof(f50,plain,(
% 0.10/0.42 ![X0]: (~ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|element(sK10_skl(X0),the_carrier(sK7_skl)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.42 fof(f51,plain,(
% 0.10/0.42 ![X0]: (~ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|relstr_set_smaller(sK7_skl,sK8_skl,sK10_skl(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.42 fof(f52,plain,(
% 0.10/0.42 ![X0]: (~ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|~related(sK7_skl,X0,sK10_skl(X0)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.42 fof(f53,plain,(
% 0.10/0.42 ![A]: ((~antisymmetric_relstr(A)|~rel_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|((~related(A,B,C)|~related(A,C,B))|B=C))))))),
% 0.10/0.42 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.10/0.42 fof(f54,plain,(
% 0.10/0.42 ![X0,X1,X2]: (~antisymmetric_relstr(X0)|~rel_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|~related(X0,X1,X2)|~related(X0,X2,X1)|X1=X2)),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f53])).
% 0.10/0.42 fof(f55,definition,(
% 0.10/0.42 sQ0_spl <=> (ex_sup_of_relstr_set(sK7_skl,sK8_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f56,plain,(
% 0.10/0.42 ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~sQ0_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f55])).
% 0.10/0.42 fof(f58,definition,(
% 0.10/0.42 sQ1_spl <=> (element(sK9_skl,the_carrier(sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f59,plain,(
% 0.10/0.42 element(sK9_skl,the_carrier(sK7_skl))|~sQ1_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f58])).
% 0.10/0.42 fof(f61,plain,(
% 0.10/0.42 sQ0_spl|sQ1_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f47,f55,f58])).
% 0.10/0.42 fof(f62,definition,(
% 0.10/0.42 sQ2_spl <=> (relstr_set_smaller(sK7_skl,sK8_skl,sK9_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f63,plain,(
% 0.10/0.42 relstr_set_smaller(sK7_skl,sK8_skl,sK9_skl)|~sQ2_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f62])).
% 0.10/0.42 fof(f65,plain,(
% 0.10/0.42 sQ0_spl|sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f48,f55,f62])).
% 0.10/0.42 fof(f66,definition,(
% 0.10/0.42 ![X0]: (sQ3_spl <=> (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,sK9_skl,X0)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f67,plain,(
% 0.10/0.42 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,sK9_skl,X0)|~sQ3_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f66])).
% 0.10/0.42 fof(f69,plain,(
% 0.10/0.42 sQ0_spl|sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f49,f55,f66])).
% 0.10/0.42 fof(f70,definition,(
% 0.10/0.42 ![X0]: (sQ4_spl <=> (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|element(sK10_skl(X0),the_carrier(sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f71,plain,(
% 0.10/0.42 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|element(sK10_skl(X0),the_carrier(sK7_skl))|~sQ4_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f70])).
% 0.10/0.42 fof(f73,plain,(
% 0.10/0.42 ~sQ0_spl|sQ4_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f50,f55,f70])).
% 0.10/0.42 fof(f74,definition,(
% 0.10/0.42 ![X0]: (sQ5_spl <=> (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|relstr_set_smaller(sK7_skl,sK8_skl,sK10_skl(X0))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f75,plain,(
% 0.10/0.42 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|relstr_set_smaller(sK7_skl,sK8_skl,sK10_skl(X0))|~sQ5_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f74])).
% 0.10/0.42 fof(f77,plain,(
% 0.10/0.42 ~sQ0_spl|sQ5_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f51,f55,f74])).
% 0.10/0.42 fof(f78,definition,(
% 0.10/0.42 ![X0]: (sQ6_spl <=> (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|~related(sK7_skl,X0,sK10_skl(X0))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f79,plain,(
% 0.10/0.42 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|~related(sK7_skl,X0,sK10_skl(X0))|~sQ6_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f78])).
% 0.10/0.42 fof(f81,plain,(
% 0.10/0.42 ~sQ0_spl|sQ6_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f52,f55,f78])).
% 0.10/0.42 fof(f82,plain,(
% 0.10/0.42 ![X0]: (~antisymmetric_relstr(sK7_skl)|~rel_str(sK7_skl)|~element(X0,the_carrier(sK7_skl))|~related(sK7_skl,X0,sK9_skl)|~related(sK7_skl,sK9_skl,X0)|X0=sK9_skl|~sQ1_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f54,f59])).
% 0.10/0.42 fof(f84,definition,(
% 0.10/0.42 sQ7_spl <=> (antisymmetric_relstr(sK7_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f86,plain,(
% 0.10/0.42 ~antisymmetric_relstr(sK7_skl)|sQ7_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f84])).
% 0.10/0.42 fof(f87,definition,(
% 0.10/0.42 sQ8_spl <=> (rel_str(sK7_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f89,plain,(
% 0.10/0.42 ~rel_str(sK7_skl)|sQ8_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f87])).
% 0.10/0.42 fof(f90,definition,(
% 0.10/0.42 ![X0]: (sQ9_spl <=> (~element(X0,the_carrier(sK7_skl))|~related(sK7_skl,X0,sK9_skl)|~related(sK7_skl,sK9_skl,X0)|X0=sK9_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f91,plain,(
% 0.10/0.42 ![X0]: (~element(X0,the_carrier(sK7_skl))|~related(sK7_skl,X0,sK9_skl)|~related(sK7_skl,sK9_skl,X0)|X0=sK9_skl|~sQ9_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f90])).
% 0.10/0.42 fof(f93,plain,(
% 0.10/0.42 ~sQ7_spl|~sQ8_spl|sQ9_spl|~sQ1_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f82,f84,f87,f90,f58])).
% 0.10/0.42 fof(f94,plain,(
% 0.10/0.42 ~element(sK9_skl,the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,sK8_skl,sK10_skl(sK9_skl))|~sQ5_spl|~sQ2_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f75,f63])).
% 0.10/0.42 fof(f95,definition,(
% 0.10/0.42 sQ10_spl <=> (relstr_set_smaller(sK7_skl,sK8_skl,sK10_skl(sK9_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f98,plain,(
% 0.10/0.42 ~sQ1_spl|sQ10_spl|~sQ5_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f94,f58,f95,f74,f62])).
% 0.10/0.42 fof(f99,plain,(
% 0.10/0.42 ~element(sK9_skl,the_carrier(sK7_skl))|element(sK10_skl(sK9_skl),the_carrier(sK7_skl))|~sQ4_spl|~sQ2_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f71,f63])).
% 0.10/0.42 fof(f100,definition,(
% 0.10/0.42 sQ11_spl <=> (element(sK10_skl(sK9_skl),the_carrier(sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f103,plain,(
% 0.10/0.42 ~sQ1_spl|sQ11_spl|~sQ4_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f99,f58,f100,f70,f62])).
% 0.10/0.42 fof(f104,plain,(
% 0.10/0.42 ~element(sK9_skl,the_carrier(sK7_skl))|related(sK7_skl,sK9_skl,sK9_skl)|~sQ3_spl|~sQ2_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f67,f63])).
% 0.10/0.42 fof(f105,plain,(
% 0.10/0.42 ~element(sK10_skl(sK9_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK10_skl(sK9_skl))|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK9_skl)|~sQ3_spl|~sQ6_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f67,f79])).
% 0.10/0.42 fof(f107,plain,(
% 0.10/0.42 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|~antisymmetric_relstr(sK7_skl)|~rel_str(sK7_skl)|~element(X0,the_carrier(sK7_skl))|~element(sK9_skl,the_carrier(sK7_skl))|~related(sK7_skl,X0,sK9_skl)|X0=sK9_skl|~sQ3_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f67,f54])).
% 0.10/0.42 fof(f110,definition,(
% 0.10/0.42 sQ12_spl <=> (related(sK7_skl,sK9_skl,sK9_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f111,plain,(
% 0.10/0.42 related(sK7_skl,sK9_skl,sK9_skl)|~sQ12_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f110])).
% 0.10/0.42 fof(f113,plain,(
% 0.10/0.42 ~sQ1_spl|sQ12_spl|~sQ3_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f104,f58,f110,f66,f62])).
% 0.10/0.42 fof(f114,plain,(
% 0.10/0.42 ~sQ11_spl|~sQ10_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ6_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f105,f100,f95,f58,f62,f66,f78])).
% 0.10/0.42 fof(f115,definition,(
% 0.10/0.42 sQ13_spl <=> (sK9_skl=sK9_skl)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f119,definition,(
% 0.10/0.42 ![X0]: (sQ14_spl <=> (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|~element(X0,the_carrier(sK7_skl))|~related(sK7_skl,X0,sK9_skl)|X0=sK9_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f120,plain,(
% 0.10/0.42 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|~element(X0,the_carrier(sK7_skl))|~related(sK7_skl,X0,sK9_skl)|X0=sK9_skl|~sQ14_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f119])).
% 0.10/0.42 fof(f122,plain,(
% 0.10/0.42 sQ14_spl|~sQ7_spl|~sQ8_spl|~sQ1_spl|~sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f107,f119,f84,f87,f58,f66])).
% 0.10/0.42 fof(f125,plain,(
% 0.10/0.42 $false|sQ8_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f89,f46])).
% 0.10/0.42 fof(f126,plain,(
% 0.10/0.42 sQ8_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f125])).
% 0.10/0.42 fof(f127,plain,(
% 0.10/0.42 $false|sQ7_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f86,f45])).
% 0.10/0.42 fof(f128,plain,(
% 0.10/0.42 sQ7_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f127])).
% 0.10/0.42 fof(f131,plain,(
% 0.10/0.42 ~rel_str(sK7_skl)|relstr_set_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))|~sQ0_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f56,f17])).
% 0.10/0.42 fof(f132,plain,(
% 0.10/0.42 ~rel_str(sK7_skl)|element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))|~sQ0_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f56,f16])).
% 0.10/0.42 fof(f133,definition,(
% 0.10/0.42 sQ15_spl <=> (relstr_set_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f134,plain,(
% 0.10/0.42 relstr_set_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))|~sQ15_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f133])).
% 0.10/0.42 fof(f136,plain,(
% 0.10/0.42 ~sQ8_spl|sQ15_spl|~sQ0_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f131,f87,f133,f55])).
% 0.10/0.42 fof(f137,definition,(
% 0.10/0.42 sQ16_spl <=> (element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f140,plain,(
% 0.10/0.42 ~sQ8_spl|sQ16_spl|~sQ0_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f132,f87,f137,f55])).
% 0.10/0.42 fof(f141,plain,(
% 0.10/0.42 ~element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))|element(sK10_skl(sK0_skl(sK8_skl,sK7_skl)),the_carrier(sK7_skl))|~sQ15_spl|~sQ4_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f134,f71])).
% 0.10/0.42 fof(f145,definition,(
% 0.10/0.42 sQ17_spl <=> (element(sK10_skl(sK0_skl(sK8_skl,sK7_skl)),the_carrier(sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f148,plain,(
% 0.10/0.42 ~sQ16_spl|sQ17_spl|~sQ15_spl|~sQ4_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f141,f137,f145,f133,f70])).
% 0.10/0.42 fof(f164,plain,(
% 0.10/0.42 ~element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,sK8_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))|~sQ5_spl|~sQ15_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f75,f134])).
% 0.10/0.42 fof(f165,definition,(
% 0.10/0.42 sQ22_spl <=> (relstr_set_smaller(sK7_skl,sK8_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f166,plain,(
% 0.10/0.42 relstr_set_smaller(sK7_skl,sK8_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))|~sQ22_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f165])).
% 0.10/0.42 fof(f168,plain,(
% 0.10/0.42 ~sQ16_spl|sQ22_spl|~sQ5_spl|~sQ15_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f164,f137,f165,f74,f133])).
% 0.10/0.42 fof(f184,plain,(
% 0.10/0.42 ~rel_str(sK7_skl)|~ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(sK10_skl(sK0_skl(sK8_skl,sK7_skl)),the_carrier(sK7_skl))|related(sK7_skl,sK0_skl(sK8_skl,sK7_skl),sK10_skl(sK0_skl(sK8_skl,sK7_skl)))|~sQ22_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f166,f18])).
% 0.10/0.42 fof(f204,definition,(
% 0.10/0.42 sQ30_spl <=> (related(sK7_skl,sK0_skl(sK8_skl,sK7_skl),sK10_skl(sK0_skl(sK8_skl,sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f205,plain,(
% 0.10/0.42 related(sK7_skl,sK0_skl(sK8_skl,sK7_skl),sK10_skl(sK0_skl(sK8_skl,sK7_skl)))|~sQ30_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f204])).
% 0.10/0.42 fof(f207,plain,(
% 0.10/0.42 ~sQ8_spl|~sQ0_spl|~sQ17_spl|sQ30_spl|~sQ22_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f184,f87,f55,f145,f204,f165])).
% 0.10/0.42 fof(f366,plain,(
% 0.10/0.42 ~element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))|~sQ30_spl|~sQ6_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f205,f79])).
% 0.10/0.42 fof(f373,plain,(
% 0.10/0.42 ~sQ16_spl|~sQ15_spl|~sQ30_spl|~sQ6_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f366,f137,f133,f204,f78])).
% 0.10/0.42 fof(f380,plain,(
% 0.10/0.42 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|~related(sK7_skl,X0,sK9_skl)|X0=sK9_skl|~sQ14_spl)),
% 0.10/0.42 inference(duplicate_literals_removal,[status(thm)],[f120])).
% 0.10/0.42 fof(f410,plain,(
% 0.10/0.42 ~antisymmetric_relstr(sK7_skl)|~rel_str(sK7_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~element(sK9_skl,the_carrier(sK7_skl))|sK9_skl=sK9_skl|~sQ12_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f111,f54])).
% 0.10/0.42 fof(f414,plain,(
% 0.10/0.42 ~sQ7_spl|~sQ8_spl|~sQ1_spl|sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f410,f84,f87,f58,f115,f110])).
% 0.10/0.42 fof(f420,plain,(
% 0.10/0.42 ~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|~sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~sQ2_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f63,f29])).
% 0.10/0.42 fof(f421,plain,(
% 0.10/0.42 ![X0]: (~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),X0)|~sQ2_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f63,f28])).
% 0.10/0.42 fof(f422,plain,(
% 0.10/0.42 ~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|relstr_set_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~sQ2_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f63,f27])).
% 0.10/0.42 fof(f423,plain,(
% 0.10/0.42 ~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~sQ2_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f63,f26])).
% 0.10/0.42 fof(f424,plain,(
% 0.10/0.42 ~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~sQ2_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f63,f25])).
% 0.10/0.42 fof(f425,plain,(
% 0.10/0.42 ![X0]: (~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),X0)|~sQ2_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f63,f24])).
% 0.10/0.42 fof(f426,plain,(
% 0.10/0.42 ~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~sQ2_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f63,f23])).
% 0.10/0.42 fof(f427,plain,(
% 0.10/0.42 ~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~sQ2_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f63,f22])).
% 0.10/0.42 fof(f431,definition,(
% 0.10/0.42 sQ56_spl <=> (relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f432,plain,(
% 0.10/0.42 relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|~sQ56_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f431])).
% 0.10/0.42 fof(f434,definition,(
% 0.10/0.42 sQ57_spl <=> (sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f437,plain,(
% 0.10/0.42 ~sQ8_spl|sQ0_spl|~sQ1_spl|sQ56_spl|~sQ57_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f420,f87,f55,f58,f431,f434,f62])).
% 0.10/0.42 fof(f438,definition,(
% 0.10/0.42 ![X0]: (sQ58_spl <=> (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),X0)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f439,plain,(
% 0.10/0.42 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),X0)|~sQ58_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f438])).
% 0.10/0.42 fof(f441,plain,(
% 0.10/0.42 ~sQ8_spl|sQ0_spl|~sQ1_spl|sQ56_spl|sQ58_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f421,f87,f55,f58,f431,f438,f62])).
% 0.10/0.42 fof(f442,definition,(
% 0.10/0.42 sQ59_spl <=> (relstr_set_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f443,plain,(
% 0.10/0.42 relstr_set_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~sQ59_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f442])).
% 0.10/0.42 fof(f445,plain,(
% 0.10/0.42 ~sQ8_spl|sQ0_spl|~sQ1_spl|sQ56_spl|sQ59_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f422,f87,f55,f58,f431,f442,f62])).
% 0.10/0.42 fof(f446,definition,(
% 0.10/0.42 sQ60_spl <=> (element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f449,plain,(
% 0.10/0.42 ~sQ8_spl|sQ0_spl|~sQ1_spl|sQ56_spl|sQ60_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f423,f87,f55,f58,f431,f446,f62])).
% 0.10/0.42 fof(f450,definition,(
% 0.10/0.42 sQ61_spl <=> (element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f453,plain,(
% 0.10/0.42 ~sQ8_spl|sQ0_spl|~sQ1_spl|sQ61_spl|~sQ57_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f424,f87,f55,f58,f450,f434,f62])).
% 0.10/0.42 fof(f454,plain,(
% 0.10/0.42 ~sQ8_spl|sQ0_spl|~sQ1_spl|sQ61_spl|sQ58_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f425,f87,f55,f58,f450,f438,f62])).
% 0.10/0.42 fof(f455,plain,(
% 0.10/0.42 ~sQ8_spl|sQ0_spl|~sQ1_spl|sQ61_spl|sQ59_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f426,f87,f55,f58,f450,f442,f62])).
% 0.10/0.42 fof(f456,plain,(
% 0.10/0.42 ~sQ8_spl|sQ0_spl|~sQ1_spl|sQ61_spl|sQ60_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f427,f87,f55,f58,f450,f446,f62])).
% 0.10/0.42 fof(f514,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~sK3_skl(sK9_skl,X0,sK7_skl)=sK9_skl|~sQ3_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f67,f33])).
% 0.10/0.42 fof(f515,plain,(
% 0.10/0.42 ![X0,X1]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(X1,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,X1)|related(sK7_skl,sK3_skl(sK9_skl,X0,sK7_skl),X1)|~sQ3_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f67,f32])).
% 0.10/0.42 fof(f516,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|relstr_set_smaller(sK7_skl,X0,sK3_skl(sK9_skl,X0,sK7_skl))|~sQ3_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f67,f31])).
% 0.10/0.42 fof(f517,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~sQ3_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f67,f30])).
% 0.10/0.42 fof(f518,plain,(
% 0.10/0.42 ![X0]: (~element(sK1_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK1_skl(sK9_skl,X0,sK7_skl))|~rel_str(sK7_skl)|~ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|sK9_skl=sK0_skl(X0,sK7_skl)|~sQ3_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f67,f21])).
% 0.10/0.42 fof(f524,definition,(
% 0.10/0.42 ![X0]: (sQ66_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~sK3_skl(sK9_skl,X0,sK7_skl)=sK9_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f525,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~sK3_skl(sK9_skl,X0,sK7_skl)=sK9_skl|~sQ66_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f524])).
% 0.10/0.42 fof(f527,plain,(
% 0.10/0.42 sQ66_spl|~sQ8_spl|~sQ1_spl|~sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f514,f524,f87,f58,f66])).
% 0.10/0.42 fof(f528,definition,(
% 0.10/0.42 ![X0,X1]: (sQ67_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(X1,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,X1)|related(sK7_skl,sK3_skl(sK9_skl,X0,sK7_skl),X1)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f529,plain,(
% 0.10/0.42 ![X0,X1]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(X1,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,X1)|related(sK7_skl,sK3_skl(sK9_skl,X0,sK7_skl),X1)|~sQ67_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f528])).
% 0.10/0.42 fof(f531,plain,(
% 0.10/0.42 sQ67_spl|~sQ8_spl|~sQ1_spl|~sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f515,f528,f87,f58,f66])).
% 0.10/0.42 fof(f532,definition,(
% 0.10/0.42 ![X0]: (sQ68_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|relstr_set_smaller(sK7_skl,X0,sK3_skl(sK9_skl,X0,sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f533,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|relstr_set_smaller(sK7_skl,X0,sK3_skl(sK9_skl,X0,sK7_skl))|~sQ68_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f532])).
% 0.10/0.42 fof(f535,plain,(
% 0.10/0.42 sQ68_spl|~sQ8_spl|~sQ1_spl|~sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f516,f532,f87,f58,f66])).
% 0.10/0.42 fof(f536,definition,(
% 0.10/0.42 ![X0]: (sQ69_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f537,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~sQ69_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f536])).
% 0.10/0.42 fof(f539,plain,(
% 0.10/0.42 sQ69_spl|~sQ8_spl|~sQ1_spl|~sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f517,f536,f87,f58,f66])).
% 0.10/0.42 fof(f540,definition,(
% 0.10/0.42 ![X0]: (sQ70_spl <=> (~element(sK1_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK1_skl(sK9_skl,X0,sK7_skl))|~ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|sK9_skl=sK0_skl(X0,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f543,plain,(
% 0.10/0.42 sQ70_spl|~sQ8_spl|~sQ1_spl|~sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f518,f540,f87,f58,f66])).
% 0.10/0.42 fof(f610,definition,(
% 0.10/0.42 sQ72_spl <=> (related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f612,plain,(
% 0.10/0.42 ~related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|sQ72_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f610])).
% 0.10/0.42 fof(f613,definition,(
% 0.10/0.42 sQ73_spl <=> (sK2_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f614,plain,(
% 0.10/0.42 sK2_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~sQ73_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f613])).
% 0.10/0.42 fof(f675,plain,(
% 0.10/0.42 ~related(sK7_skl,sK9_skl,sK9_skl)|~sQ73_spl|sQ72_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f614,f612])).
% 0.10/0.42 fof(f676,plain,(
% 0.10/0.42 $false|~sQ12_spl|~sQ73_spl|sQ72_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f675,f111])).
% 0.10/0.42 fof(f677,plain,(
% 0.10/0.42 ~sQ12_spl|~sQ73_spl|sQ72_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f676])).
% 0.10/0.42 fof(f685,plain,(
% 0.10/0.42 ~element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~sQ59_spl|~sQ14_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f443,f380])).
% 0.10/0.42 fof(f698,definition,(
% 0.10/0.42 sQ86_spl <=> (related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f701,plain,(
% 0.10/0.42 ~sQ60_spl|~sQ86_spl|sQ57_spl|~sQ59_spl|~sQ14_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f685,f446,f698,f434,f442,f119])).
% 0.10/0.42 fof(f787,definition,(
% 0.10/0.42 sQ99_spl <=> (related(sK7_skl,sK1_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f789,plain,(
% 0.10/0.42 ~related(sK7_skl,sK1_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|sQ99_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f787])).
% 0.10/0.42 fof(f790,definition,(
% 0.10/0.42 sQ100_spl <=> (sK1_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f791,plain,(
% 0.10/0.42 sK1_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~sQ100_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f790])).
% 0.10/0.42 fof(f852,plain,(
% 0.10/0.42 ~related(sK7_skl,sK9_skl,sK9_skl)|~sQ100_spl|sQ99_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f791,f789])).
% 0.10/0.42 fof(f853,plain,(
% 0.10/0.42 $false|~sQ12_spl|~sQ100_spl|sQ99_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f852,f111])).
% 0.10/0.42 fof(f854,plain,(
% 0.10/0.42 ~sQ12_spl|~sQ100_spl|sQ99_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f853])).
% 0.10/0.42 fof(f861,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,X0,sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK9_skl|~sQ67_spl|~sQ14_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f529,f380])).
% 0.10/0.42 fof(f862,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,X0,sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK9_skl|~sQ67_spl|~sQ9_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f529,f91])).
% 0.10/0.42 fof(f863,plain,(
% 0.10/0.42 ![X0,X1]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X1)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|~sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl)=sK3_skl(sK9_skl,X0,sK7_skl)|~sQ67_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f529,f33])).
% 0.10/0.42 fof(f864,plain,(
% 0.10/0.42 ![X0,X1,X2]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X1)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|~element(X2,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,X2)|related(sK7_skl,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),X2)|~sQ67_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f529,f32])).
% 0.10/0.42 fof(f865,plain,(
% 0.10/0.42 ![X0,X1]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X1)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|relstr_set_smaller(sK7_skl,X1,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|~sQ67_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f529,f31])).
% 0.10/0.42 fof(f866,plain,(
% 0.10/0.42 ![X0,X1]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X1)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|element(sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~sQ67_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f529,f30])).
% 0.10/0.42 fof(f867,plain,(
% 0.10/0.42 ![X0,X1]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK1_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK1_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|~rel_str(sK7_skl)|~ex_sup_of_relstr_set(sK7_skl,X1)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK0_skl(X1,sK7_skl)|~sQ67_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f529,f21])).
% 0.10/0.42 fof(f868,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK3_skl(sK9_skl,X0,sK7_skl))|~antisymmetric_relstr(sK7_skl)|~rel_str(sK7_skl)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK3_skl(sK9_skl,X0,sK7_skl)|~sQ67_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f529,f54])).
% 0.10/0.42 fof(f869,plain,(
% 0.10/0.42 ![X0,X1]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(X1,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,X1)|~antisymmetric_relstr(sK7_skl)|~rel_str(sK7_skl)|~element(X1,the_carrier(sK7_skl))|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~related(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|X1=sK3_skl(sK9_skl,X0,sK7_skl)|~sQ67_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f529,f54])).
% 0.10/0.42 fof(f872,definition,(
% 0.10/0.42 ![X0]: (sQ112_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,X0,sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK9_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f875,plain,(
% 0.10/0.42 sQ112_spl|~sQ1_spl|~sQ67_spl|~sQ14_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f861,f872,f58,f528,f119])).
% 0.10/0.42 fof(f876,definition,(
% 0.10/0.42 ![X0]: (sQ113_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,X0,sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK9_skl))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f879,plain,(
% 0.10/0.42 sQ113_spl|~sQ1_spl|~sQ67_spl|~sQ9_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f862,f876,f58,f528,f90])).
% 0.10/0.42 fof(f880,definition,(
% 0.10/0.42 ![X0,X1]: (sQ114_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X1)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|~sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl)=sK3_skl(sK9_skl,X0,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f883,plain,(
% 0.10/0.42 sQ114_spl|~sQ8_spl|~sQ67_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f863,f880,f87,f528])).
% 0.10/0.42 fof(f884,definition,(
% 0.10/0.42 ![X0,X1,X2]: (sQ115_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X1)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|~element(X2,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,X2)|related(sK7_skl,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),X2)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f887,plain,(
% 0.10/0.42 sQ115_spl|~sQ8_spl|~sQ67_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f864,f884,f87,f528])).
% 0.10/0.42 fof(f888,definition,(
% 0.10/0.42 ![X0,X1]: (sQ116_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X1)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|relstr_set_smaller(sK7_skl,X1,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f891,plain,(
% 0.10/0.42 sQ116_spl|~sQ8_spl|~sQ67_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f865,f888,f87,f528])).
% 0.10/0.42 fof(f892,definition,(
% 0.10/0.42 ![X0,X1]: (sQ117_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X1)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|element(sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f895,plain,(
% 0.10/0.42 sQ117_spl|~sQ8_spl|~sQ67_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f866,f892,f87,f528])).
% 0.10/0.42 fof(f896,definition,(
% 0.10/0.42 ![X0,X1]: (sQ118_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK1_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK1_skl(sK3_skl(sK9_skl,X0,sK7_skl),X1,sK7_skl))|~ex_sup_of_relstr_set(sK7_skl,X1)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK0_skl(X1,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f899,plain,(
% 0.10/0.42 sQ118_spl|~sQ8_spl|~sQ67_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f867,f896,f87,f528])).
% 0.10/0.42 fof(f900,definition,(
% 0.10/0.42 ![X0]: (sQ119_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,sK3_skl(sK9_skl,X0,sK7_skl))|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK3_skl(sK9_skl,X0,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f903,plain,(
% 0.10/0.42 sQ119_spl|~sQ7_spl|~sQ8_spl|~sQ67_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f868,f900,f84,f87,f528])).
% 0.10/0.42 fof(f904,definition,(
% 0.10/0.42 ![X0,X1]: (sQ120_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(X1,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,X1)|~element(X1,the_carrier(sK7_skl))|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~related(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|X1=sK3_skl(sK9_skl,X0,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f907,plain,(
% 0.10/0.42 sQ120_spl|~sQ7_spl|~sQ8_spl|~sQ67_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f869,f904,f84,f87,f528])).
% 0.10/0.42 fof(f923,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|~sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl)=sK3_skl(sK9_skl,X0,sK7_skl)|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f29])).
% 0.10/0.42 fof(f924,plain,(
% 0.10/0.42 ![X0,X1]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|~element(X1,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,X1)|related(sK7_skl,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),X1)|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f28])).
% 0.10/0.42 fof(f925,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f27])).
% 0.10/0.42 fof(f926,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|element(sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f26])).
% 0.10/0.42 fof(f927,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|~sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl)=sK3_skl(sK9_skl,X0,sK7_skl)|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f25])).
% 0.10/0.42 fof(f928,plain,(
% 0.10/0.42 ![X0,X1]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|~element(X1,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,X1)|related(sK7_skl,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),X1)|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f24])).
% 0.10/0.42 fof(f929,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f23])).
% 0.10/0.42 fof(f930,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|element(sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f22])).
% 0.10/0.42 fof(f931,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|~ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK1_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK0_skl(X0,sK7_skl)|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f20])).
% 0.10/0.42 fof(f932,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|~ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK1_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK0_skl(X0,sK7_skl)|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f19])).
% 0.10/0.42 fof(f933,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~rel_str(sK7_skl)|~ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|related(sK7_skl,sK0_skl(X0,sK7_skl),sK3_skl(sK9_skl,X0,sK7_skl))|~sQ68_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f533,f18])).
% 0.10/0.42 fof(f936,definition,(
% 0.10/0.42 ![X0]: (sQ121_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|~sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl)=sK3_skl(sK9_skl,X0,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f939,plain,(
% 0.10/0.42 sQ121_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f923,f936,f87,f532])).
% 0.10/0.42 fof(f940,definition,(
% 0.10/0.42 ![X0,X1]: (sQ122_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|~element(X1,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,X1)|related(sK7_skl,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),X1)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f943,plain,(
% 0.10/0.42 sQ122_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f924,f940,f87,f532])).
% 0.10/0.42 fof(f944,definition,(
% 0.10/0.42 ![X0]: (sQ123_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f947,plain,(
% 0.10/0.42 sQ123_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f925,f944,f87,f532])).
% 0.10/0.42 fof(f948,definition,(
% 0.10/0.42 ![X0]: (sQ124_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|element(sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f951,plain,(
% 0.10/0.42 sQ124_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f926,f948,f87,f532])).
% 0.10/0.42 fof(f952,definition,(
% 0.10/0.42 ![X0]: (sQ125_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|~sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl)=sK3_skl(sK9_skl,X0,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f955,plain,(
% 0.10/0.42 sQ125_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f927,f952,f87,f532])).
% 0.10/0.42 fof(f956,definition,(
% 0.10/0.42 ![X0,X1]: (sQ126_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|~element(X1,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,X0,X1)|related(sK7_skl,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),X1)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f959,plain,(
% 0.10/0.42 sQ126_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f928,f956,f87,f532])).
% 0.10/0.42 fof(f960,definition,(
% 0.10/0.42 ![X0]: (sQ127_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f963,plain,(
% 0.10/0.42 sQ127_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f929,f960,f87,f532])).
% 0.10/0.42 fof(f964,definition,(
% 0.10/0.42 ![X0]: (sQ128_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK2_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|element(sK3_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f967,plain,(
% 0.10/0.42 sQ128_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f930,f964,f87,f532])).
% 0.10/0.42 fof(f968,definition,(
% 0.10/0.42 ![X0]: (sQ129_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_set_smaller(sK7_skl,X0,sK1_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK0_skl(X0,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f971,plain,(
% 0.10/0.42 sQ129_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f931,f968,f87,f532])).
% 0.10/0.42 fof(f972,definition,(
% 0.10/0.42 ![X0]: (sQ130_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK1_skl(sK3_skl(sK9_skl,X0,sK7_skl),X0,sK7_skl),the_carrier(sK7_skl))|sK3_skl(sK9_skl,X0,sK7_skl)=sK0_skl(X0,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f975,plain,(
% 0.10/0.42 sQ130_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f932,f972,f87,f532])).
% 0.10/0.42 fof(f976,definition,(
% 0.10/0.42 ![X0]: (sQ131_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~ex_sup_of_relstr_set(sK7_skl,X0)|~element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|related(sK7_skl,sK0_skl(X0,sK7_skl),sK3_skl(sK9_skl,X0,sK7_skl))))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f979,plain,(
% 0.10/0.42 sQ131_spl|~sQ8_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f933,f976,f87,f532])).
% 0.10/0.42 fof(f996,plain,(
% 0.10/0.42 ![X0,X1]: (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~antisymmetric_relstr(sK7_skl)|~rel_str(sK7_skl)|~element(X1,the_carrier(sK7_skl))|~related(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|~related(sK7_skl,sK3_skl(sK9_skl,X0,sK7_skl),X1)|X1=sK3_skl(sK9_skl,X0,sK7_skl)|~sQ69_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f537,f54])).
% 0.10/0.42 fof(f997,definition,(
% 0.10/0.42 ![X0,X1]: (sQ132_spl <=> (~element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,X0,sK7_skl))|ex_sup_of_relstr_set(sK7_skl,X0)|~relstr_set_smaller(sK7_skl,X0,sK9_skl)|~element(X1,the_carrier(sK7_skl))|~related(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|~related(sK7_skl,sK3_skl(sK9_skl,X0,sK7_skl),X1)|X1=sK3_skl(sK9_skl,X0,sK7_skl)))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f1000,plain,(
% 0.10/0.42 sQ132_spl|~sQ7_spl|~sQ8_spl|~sQ69_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f996,f997,f84,f87,f536])).
% 0.10/0.42 fof(f1038,plain,(
% 0.10/0.42 ~element(sK9_skl,the_carrier(sK7_skl))|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~sQ58_spl|~sQ2_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f439,f63])).
% 0.10/0.42 fof(f1044,plain,(
% 0.10/0.42 ~sQ1_spl|sQ86_spl|~sQ58_spl|~sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1038,f58,f698,f438,f62])).
% 0.10/0.42 fof(f1097,plain,(
% 0.10/0.42 ~element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~relstr_set_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~sQ56_spl|~sQ69_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f432,f537])).
% 0.10/0.42 fof(f1098,plain,(
% 0.10/0.42 ~element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~relstr_set_smaller(sK7_skl,sK8_skl,sK9_skl)|relstr_set_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~sQ56_spl|~sQ68_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f432,f533])).
% 0.10/0.42 fof(f1099,plain,(
% 0.10/0.42 ![X0]: (~element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~relstr_set_smaller(sK7_skl,sK8_skl,sK9_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_set_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),X0)|~sQ56_spl|~sQ67_spl)),
% 0.10/0.42 inference(resolution,[status(thm)],[f432,f529])).
% 0.10/0.42 fof(f1100,plain,(
% 0.10/0.42 ~element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|ex_sup_of_relstr_set(sK7_skl,sK8_skl)|~relstr_set_smaller(sK7_skl,sK8_skl,sK9_skl)|~sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~sQ56_spl|~sQ66_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f432,f525])).
% 0.10/0.42 fof(f1114,plain,(
% 0.10/0.42 ~sQ61_spl|sQ0_spl|~sQ2_spl|sQ60_spl|~sQ56_spl|~sQ69_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1097,f450,f55,f62,f446,f431,f536])).
% 0.10/0.42 fof(f1115,plain,(
% 0.10/0.42 ~sQ61_spl|sQ0_spl|~sQ2_spl|sQ59_spl|~sQ56_spl|~sQ68_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1098,f450,f55,f62,f442,f431,f532])).
% 0.10/0.42 fof(f1116,plain,(
% 0.10/0.42 ~sQ61_spl|sQ0_spl|~sQ2_spl|sQ58_spl|~sQ56_spl|~sQ67_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1099,f450,f55,f62,f438,f431,f528])).
% 0.10/0.42 fof(f1117,plain,(
% 0.10/0.42 ~sQ61_spl|sQ0_spl|~sQ2_spl|~sQ57_spl|~sQ56_spl|~sQ66_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1100,f450,f55,f62,f434,f431,f524])).
% 0.10/0.42 fof(f1131,plain,(
% 0.10/0.42 $false),
% 0.10/0.42 inference(sat_refutation,[status(thm)],[f61,f65,f69,f73,f77,f81,f93,f98,f103,f113,f114,f122,f126,f128,f136,f140,f148,f168,f207,f373,f414,f437,f441,f445,f449,f453,f454,f455,f456,f527,f531,f535,f539,f543,f677,f701,f854,f875,f879,f883,f887,f891,f895,f899,f903,f907,f939,f943,f947,f951,f955,f959,f963,f967,f971,f975,f979,f1000,f1044,f1114,f1115,f1116,f1117])).
% 0.10/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.45 % Elapsed time: 0.077031 seconds
% 0.10/0.45 % CPU time: 0.351180 seconds
% 0.10/0.45 % Total memory used: 87.036 MB
% 0.10/0.45 % Net memory used: 86.515 MB
%------------------------------------------------------------------------------