%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU357+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 : n019.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.13s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU357+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.09/0.35 % Computer : n019.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 06:15:34 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.43 % Refutation found
% 0.13/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.43 fof(f1,axiom,(
% 0.13/0.43 (! [A] :( rel_str(A)=> (! [B] :( ex_inf_of_relstr_set(A,B)<=> (? [C] :( element(C,the_carrier(A))& relstr_element_smaller(A,B,C)& (! [D] :( element(D,the_carrier(A))=> ( relstr_element_smaller(A,B,D)=> related(A,D,C) ) ))& (! [D] :( element(D,the_carrier(A))=> ( ( relstr_element_smaller(A,B,D)& (! [E] :( element(E,the_carrier(A))=> ( relstr_element_smaller(A,B,E)=> related(A,E,D) ) ) ))=> D = C ) ) )) )) )) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f9,conjecture,(
% 0.13/0.43 (! [A] :( ( antisymmetric_relstr(A)& rel_str(A) )=> (! [B] :( ex_inf_of_relstr_set(A,B)<=> (? [C] :( element(C,the_carrier(A))& relstr_element_smaller(A,B,C)& (! [D] :( element(D,the_carrier(A))=> ( relstr_element_smaller(A,B,D)=> related(A,D,C) ) ) )) )) )) )),
% 0.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f10,negated_conjecture,(
% 0.13/0.43 ~((! [A] :( ( antisymmetric_relstr(A)& rel_str(A) )=> (! [B] :( ex_inf_of_relstr_set(A,B)<=> (? [C] :( element(C,the_carrier(A))& relstr_element_smaller(A,B,C)& (! [D] :( element(D,the_carrier(A))=> ( relstr_element_smaller(A,B,D)=> related(A,D,C) ) ) )) )) )) ))),
% 0.13/0.43 inference(negated_conjecture,[status(cth)],[f9])).
% 0.13/0.43 fof(f11,axiom,(
% 0.13/0.43 (! [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.13/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.43 fof(f12,plain,(
% 0.13/0.43 ![A]: (~rel_str(A)|(![B]: (ex_inf_of_relstr_set(A,B)<=>(?[C]: (((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_element_smaller(A,B,D)|related(A,D,C)))))&(![D]: (~element(D,the_carrier(A))|((~relstr_element_smaller(A,B,D)|(?[E]: (element(E,the_carrier(A))&(relstr_element_smaller(A,B,E)&~related(A,E,D)))))|D=C))))))))),
% 0.13/0.43 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.13/0.43 fof(f13,plain,(
% 0.13/0.43 ![A]: (~rel_str(A)|(![B]: ((~ex_inf_of_relstr_set(A,B)|(?[C]: (((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_element_smaller(A,B,D)|related(A,D,C)))))&(![D]: (~element(D,the_carrier(A))|((~relstr_element_smaller(A,B,D)|(?[E]: (element(E,the_carrier(A))&(relstr_element_smaller(A,B,E)&~related(A,E,D)))))|D=C))))))&(ex_inf_of_relstr_set(A,B)|(![C]: (((~element(C,the_carrier(A))|~relstr_element_smaller(A,B,C))|(?[D]: (element(D,the_carrier(A))&(relstr_element_smaller(A,B,D)&~related(A,D,C)))))|(?[D]: (element(D,the_carrier(A))&((relstr_element_smaller(A,B,D)&(![E]: (~element(E,the_carrier(A))|(~relstr_element_smaller(A,B,E)|related(A,E,D)))))&~D=C)))))))))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f12])).
% 0.13/0.43 fof(f14,plain,(
% 0.13/0.43 ![A]: (~rel_str(A)|((![B]: (~ex_inf_of_relstr_set(A,B)|(?[C]: (((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_element_smaller(A,B,D)|related(A,D,C)))))&(![D]: (~element(D,the_carrier(A))|((~relstr_element_smaller(A,B,D)|(?[E]: (element(E,the_carrier(A))&(relstr_element_smaller(A,B,E)&~related(A,E,D)))))|D=C)))))))&(![B]: (ex_inf_of_relstr_set(A,B)|(![C]: (((~element(C,the_carrier(A))|~relstr_element_smaller(A,B,C))|(?[D]: (element(D,the_carrier(A))&(relstr_element_smaller(A,B,D)&~related(A,D,C)))))|(?[D]: (element(D,the_carrier(A))&((relstr_element_smaller(A,B,D)&(![E]: (~element(E,the_carrier(A))|(~relstr_element_smaller(A,B,E)|related(A,E,D)))))&~D=C)))))))))),
% 0.13/0.43 inference(miniscoping,[status(thm)],[f13])).
% 0.13/0.43 fof(f15,plain,(
% 0.13/0.43 ![A]: (~rel_str(A)|((![B]: (~ex_inf_of_relstr_set(A,B)|(((element(sK0_skl(B,A),the_carrier(A))&relstr_element_smaller(A,B,sK0_skl(B,A)))&(![D]: (~element(D,the_carrier(A))|(~relstr_element_smaller(A,B,D)|related(A,D,sK0_skl(B,A))))))&(![D]: (~element(D,the_carrier(A))|((~relstr_element_smaller(A,B,D)|(element(sK1_skl(D,B,A),the_carrier(A))&(relstr_element_smaller(A,B,sK1_skl(D,B,A))&~related(A,sK1_skl(D,B,A),D))))|D=sK0_skl(B,A)))))))&(![B]: (ex_inf_of_relstr_set(A,B)|(![C]: (((~element(C,the_carrier(A))|~relstr_element_smaller(A,B,C))|(element(sK2_skl(C,B,A),the_carrier(A))&(relstr_element_smaller(A,B,sK2_skl(C,B,A))&~related(A,sK2_skl(C,B,A),C))))|(element(sK3_skl(C,B,A),the_carrier(A))&((relstr_element_smaller(A,B,sK3_skl(C,B,A))&(![E]: (~element(E,the_carrier(A))|(~relstr_element_smaller(A,B,E)|related(A,E,sK3_skl(C,B,A))))))&~sK3_skl(C,B,A)=C))))))))),
% 0.13/0.43 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.13/0.43 fof(f16,plain,(
% 0.13/0.43 ![X0,X1]: (~rel_str(X0)|~ex_inf_of_relstr_set(X0,X1)|element(sK0_skl(X1,X0),the_carrier(X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f17,plain,(
% 0.13/0.43 ![X0,X1]: (~rel_str(X0)|~ex_inf_of_relstr_set(X0,X1)|relstr_element_smaller(X0,X1,sK0_skl(X1,X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f18,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~rel_str(X0)|~ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|related(X0,X2,sK0_skl(X1,X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f22,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|element(sK2_skl(X2,X1,X0),the_carrier(X0))|element(sK3_skl(X2,X1,X0),the_carrier(X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f23,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|element(sK2_skl(X2,X1,X0),the_carrier(X0))|relstr_element_smaller(X0,X1,sK3_skl(X2,X1,X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f24,plain,(
% 0.13/0.43 ![X0,X1,X2,X3]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|element(sK2_skl(X2,X1,X0),the_carrier(X0))|~element(X3,the_carrier(X0))|~relstr_element_smaller(X0,X1,X3)|related(X0,X3,sK3_skl(X2,X1,X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f25,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|element(sK2_skl(X2,X1,X0),the_carrier(X0))|~sK3_skl(X2,X1,X0)=X2)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f26,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|relstr_element_smaller(X0,X1,sK2_skl(X2,X1,X0))|element(sK3_skl(X2,X1,X0),the_carrier(X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f27,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|relstr_element_smaller(X0,X1,sK2_skl(X2,X1,X0))|relstr_element_smaller(X0,X1,sK3_skl(X2,X1,X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f28,plain,(
% 0.13/0.43 ![X0,X1,X2,X3]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|relstr_element_smaller(X0,X1,sK2_skl(X2,X1,X0))|~element(X3,the_carrier(X0))|~relstr_element_smaller(X0,X1,X3)|related(X0,X3,sK3_skl(X2,X1,X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f29,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|relstr_element_smaller(X0,X1,sK2_skl(X2,X1,X0))|~sK3_skl(X2,X1,X0)=X2)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f30,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|~related(X0,sK2_skl(X2,X1,X0),X2)|element(sK3_skl(X2,X1,X0),the_carrier(X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f31,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|~related(X0,sK2_skl(X2,X1,X0),X2)|relstr_element_smaller(X0,X1,sK3_skl(X2,X1,X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f32,plain,(
% 0.13/0.43 ![X0,X1,X2,X3]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|~related(X0,sK2_skl(X2,X1,X0),X2)|~element(X3,the_carrier(X0))|~relstr_element_smaller(X0,X1,X3)|related(X0,X3,sK3_skl(X2,X1,X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f33,plain,(
% 0.13/0.43 ![X0,X1,X2]: (~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|~related(X0,sK2_skl(X2,X1,X0),X2)|~sK3_skl(X2,X1,X0)=X2)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.43 fof(f42,plain,(
% 0.13/0.43 (?[A]: ((antisymmetric_relstr(A)&rel_str(A))&(?[B]: (ex_inf_of_relstr_set(A,B)<~>(?[C]: ((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_element_smaller(A,B,D)|related(A,D,C))))))))))),
% 0.13/0.43 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.13/0.43 fof(f43,plain,(
% 0.13/0.43 ?[A]: ((antisymmetric_relstr(A)&rel_str(A))&(?[B]: ((ex_inf_of_relstr_set(A,B)|(?[C]: ((element(C,the_carrier(A))&relstr_element_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_element_smaller(A,B,D)|related(A,D,C)))))))&(~ex_inf_of_relstr_set(A,B)|(![C]: ((~element(C,the_carrier(A))|~relstr_element_smaller(A,B,C))|(?[D]: (element(D,the_carrier(A))&(relstr_element_smaller(A,B,D)&~related(A,D,C))))))))))),
% 0.13/0.43 inference(NNF_transformation,[status(thm)],[f42])).
% 0.13/0.43 fof(f44,plain,(
% 0.13/0.43 ((antisymmetric_relstr(sK7_skl)&rel_str(sK7_skl))&((ex_inf_of_relstr_set(sK7_skl,sK8_skl)|((element(sK9_skl,the_carrier(sK7_skl))&relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl))&(![D]: (~element(D,the_carrier(sK7_skl))|(~relstr_element_smaller(sK7_skl,sK8_skl,D)|related(sK7_skl,D,sK9_skl))))))&(~ex_inf_of_relstr_set(sK7_skl,sK8_skl)|(![C]: ((~element(C,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,C))|(element(sK10_skl(C),the_carrier(sK7_skl))&(relstr_element_smaller(sK7_skl,sK8_skl,sK10_skl(C))&~related(sK7_skl,sK10_skl(C),C))))))))),
% 0.13/0.43 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.13/0.43 fof(f45,plain,(
% 0.13/0.43 antisymmetric_relstr(sK7_skl)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.43 fof(f46,plain,(
% 0.13/0.43 rel_str(sK7_skl)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.43 fof(f47,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK9_skl,the_carrier(sK7_skl))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.43 fof(f48,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.43 fof(f49,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,X0,sK9_skl))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.43 fof(f50,plain,(
% 0.13/0.43 ![X0]: (~ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|element(sK10_skl(X0),the_carrier(sK7_skl)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.43 fof(f51,plain,(
% 0.13/0.43 ![X0]: (~ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|relstr_element_smaller(sK7_skl,sK8_skl,sK10_skl(X0)))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.43 fof(f52,plain,(
% 0.13/0.43 ![X0]: (~ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|~related(sK7_skl,sK10_skl(X0),X0))),
% 0.13/0.43 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.43 fof(f53,plain,(
% 0.13/0.43 ![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.13/0.43 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.13/0.43 fof(f54,plain,(
% 0.13/0.43 ![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.13/0.43 inference(cnf_transformation,[status(thm)],[f53])).
% 0.13/0.43 fof(f60,plain,(
% 0.13/0.43 ![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|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f54,f47])).
% 0.13/0.43 fof(f61,plain,(
% 0.13/0.43 ![X0]: (~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|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f60,f45])).
% 0.13/0.43 fof(f62,plain,(
% 0.13/0.43 ![X0]: (~element(X0,the_carrier(sK7_skl))|~related(sK7_skl,X0,sK9_skl)|~related(sK7_skl,sK9_skl,X0)|X0=sK9_skl|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f61,f46])).
% 0.13/0.43 fof(f82,plain,(
% 0.13/0.43 ![X0]: (~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|relstr_element_smaller(sK7_skl,X0,sK2_skl(sK9_skl,X0,sK7_skl))|relstr_element_smaller(sK7_skl,X0,sK3_skl(sK9_skl,X0,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f27,f47])).
% 0.13/0.43 fof(f83,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|relstr_element_smaller(sK7_skl,X0,sK2_skl(sK9_skl,X0,sK7_skl))|relstr_element_smaller(sK7_skl,X0,sK3_skl(sK9_skl,X0,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f82,f46])).
% 0.13/0.43 fof(f85,plain,(
% 0.13/0.43 ![X0]: (~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f22,f47])).
% 0.13/0.43 fof(f86,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f85,f46])).
% 0.13/0.43 fof(f88,plain,(
% 0.13/0.43 ![X0]: (~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_element_smaller(sK7_skl,X0,sK3_skl(sK9_skl,X0,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f23,f47])).
% 0.13/0.43 fof(f89,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|relstr_element_smaller(sK7_skl,X0,sK3_skl(sK9_skl,X0,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f88,f46])).
% 0.13/0.43 fof(f91,plain,(
% 0.13/0.43 ![X0,X1]: (~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~element(X1,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,X0,X1)|related(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f24,f47])).
% 0.13/0.43 fof(f92,plain,(
% 0.13/0.43 ![X0,X1]: (ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|element(sK2_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|~element(X1,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,X0,X1)|related(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f91,f46])).
% 0.13/0.43 fof(f95,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f83,f48])).
% 0.13/0.43 fof(f96,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f95])).
% 0.13/0.43 fof(f97,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_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))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f86,f48])).
% 0.13/0.43 fof(f98,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_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))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f97])).
% 0.13/0.43 fof(f102,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f98,f49])).
% 0.13/0.43 fof(f112,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f102])).
% 0.13/0.43 fof(f121,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f89,f48])).
% 0.13/0.43 fof(f122,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f121])).
% 0.13/0.43 fof(f126,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f122,f49])).
% 0.13/0.43 fof(f136,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f126])).
% 0.13/0.43 fof(f137,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f136,f96])).
% 0.13/0.43 fof(f150,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,X0,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f92,f48])).
% 0.13/0.43 fof(f151,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,X0,sK3_skl(sK9_skl,sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f150])).
% 0.13/0.43 fof(f155,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f151,f47])).
% 0.13/0.43 fof(f158,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f155])).
% 0.13/0.43 fof(f159,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f158,f48])).
% 0.13/0.43 fof(f166,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f159,f49])).
% 0.13/0.43 fof(f177,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f166])).
% 0.13/0.43 fof(f190,plain,(
% 0.13/0.43 ![X0]: (~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|relstr_element_smaller(sK7_skl,X0,sK2_skl(sK9_skl,X0,sK7_skl))|element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f26,f47])).
% 0.13/0.43 fof(f194,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|relstr_element_smaller(sK7_skl,X0,sK2_skl(sK9_skl,X0,sK7_skl))|element(sK3_skl(sK9_skl,X0,sK7_skl),the_carrier(sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f190,f46])).
% 0.13/0.43 fof(f195,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_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))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f194,f48])).
% 0.13/0.43 fof(f196,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_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))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f195])).
% 0.13/0.43 fof(f197,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(backward_subsumption_resolution,[status(thm)],[f112,f196])).
% 0.13/0.43 fof(f228,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f197,f62])).
% 0.13/0.43 fof(f231,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f197,f49])).
% 0.13/0.43 fof(f243,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f228])).
% 0.13/0.43 fof(f244,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f231])).
% 0.13/0.43 fof(f245,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f244,f137])).
% 0.13/0.43 fof(f259,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f245,f30])).
% 0.13/0.43 fof(f260,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f245,f31])).
% 0.13/0.43 fof(f261,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~rel_str(sK7_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f259])).
% 0.13/0.43 fof(f262,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f261,f46])).
% 0.13/0.43 fof(f263,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~rel_str(sK7_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f260])).
% 0.13/0.43 fof(f264,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f263,f46])).
% 0.13/0.43 fof(f271,plain,(
% 0.13/0.43 ![X0,X1]: (~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|relstr_element_smaller(sK7_skl,X0,sK2_skl(sK9_skl,X0,sK7_skl))|~element(X1,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,X0,X1)|related(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f28,f47])).
% 0.13/0.43 fof(f277,plain,(
% 0.13/0.43 ![X0,X1]: (ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK9_skl)|relstr_element_smaller(sK7_skl,X0,sK2_skl(sK9_skl,X0,sK7_skl))|~element(X1,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,X0,X1)|related(sK7_skl,X1,sK3_skl(sK9_skl,X0,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f271,f46])).
% 0.13/0.43 fof(f285,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f262,f47])).
% 0.13/0.43 fof(f286,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f285,f48])).
% 0.13/0.43 fof(f287,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f286])).
% 0.13/0.43 fof(f292,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f287,f49])).
% 0.13/0.43 fof(f305,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f292])).
% 0.13/0.43 fof(f318,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,X0,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f277,f48])).
% 0.13/0.43 fof(f319,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,X0,sK3_skl(sK9_skl,sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f318])).
% 0.13/0.43 fof(f327,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f319,f47])).
% 0.13/0.43 fof(f333,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f327])).
% 0.13/0.43 fof(f334,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f333,f48])).
% 0.13/0.43 fof(f335,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(backward_subsumption_resolution,[status(thm)],[f177,f334])).
% 0.13/0.43 fof(f340,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,X0,sK3_skl(sK9_skl,sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f335,f32])).
% 0.13/0.43 fof(f343,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~rel_str(sK7_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,X0,sK3_skl(sK9_skl,sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f340])).
% 0.13/0.43 fof(f344,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,X0,sK3_skl(sK9_skl,sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f343,f46])).
% 0.13/0.43 fof(f349,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f264,f47])).
% 0.13/0.43 fof(f350,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f349,f48])).
% 0.13/0.43 fof(f351,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f350])).
% 0.13/0.43 fof(f352,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f351,f305])).
% 0.13/0.43 fof(f407,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f243,f352])).
% 0.13/0.43 fof(f416,plain,(
% 0.13/0.43 ![X0]: (ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|related(sK7_skl,X0,sK3_skl(sK9_skl,sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f344,f47])).
% 0.13/0.43 fof(f424,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f416,f47])).
% 0.13/0.43 fof(f434,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f424])).
% 0.13/0.43 fof(f435,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f434,f48])).
% 0.13/0.43 fof(f436,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl),
% 0.13/0.43 inference(backward_subsumption_resolution,[status(thm)],[f407,f435])).
% 0.13/0.43 fof(f439,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f436,f30])).
% 0.13/0.43 fof(f443,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~rel_str(sK7_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f439])).
% 0.13/0.43 fof(f444,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f443,f46])).
% 0.13/0.43 fof(f462,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f444,f47])).
% 0.13/0.43 fof(f463,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f462,f48])).
% 0.13/0.43 fof(f464,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|element(sK3_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f463])).
% 0.13/0.43 fof(f467,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f464,f62])).
% 0.13/0.43 fof(f484,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~related(sK7_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)|~related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f467])).
% 0.13/0.43 fof(f485,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~related(sK7_skl,sK9_skl,sK3_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f484,f352])).
% 0.13/0.43 fof(f497,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f485,f435])).
% 0.13/0.43 fof(f498,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~rel_str(sK7_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f497,f17])).
% 0.13/0.43 fof(f499,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~rel_str(sK7_skl)|element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f497,f16])).
% 0.13/0.43 fof(f500,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f498,f46])).
% 0.13/0.43 fof(f501,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f499,f46])).
% 0.13/0.43 fof(f505,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))|relstr_element_smaller(sK7_skl,sK8_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f501,f51])).
% 0.13/0.43 fof(f506,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))|element(sK10_skl(sK0_skl(sK8_skl,sK7_skl)),the_carrier(sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f501,f50])).
% 0.13/0.43 fof(f518,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))|relstr_element_smaller(sK7_skl,sK8_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f505,f497])).
% 0.13/0.43 fof(f519,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))|element(sK10_skl(sK0_skl(sK8_skl,sK7_skl)),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f506,f497])).
% 0.13/0.43 fof(f530,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|relstr_element_smaller(sK7_skl,sK8_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f518,f500])).
% 0.13/0.43 fof(f531,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|element(sK10_skl(sK0_skl(sK8_skl,sK7_skl)),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f519,f500])).
% 0.13/0.43 fof(f546,plain,(
% 0.13/0.43 ![X0]: (sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~rel_str(sK7_skl)|~ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))|related(sK7_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)),sK0_skl(X0,sK7_skl)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f531,f18])).
% 0.13/0.43 fof(f558,plain,(
% 0.13/0.43 ![X0]: (sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))|related(sK7_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)),sK0_skl(X0,sK7_skl)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f546,f46])).
% 0.13/0.43 fof(f627,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)),sK0_skl(sK8_skl,sK7_skl))|sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl),
% 0.13/0.43 inference(resolution,[status(thm)],[f558,f530])).
% 0.13/0.43 fof(f628,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)),sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f627])).
% 0.13/0.43 fof(f629,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|related(sK7_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)),sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f628,f497])).
% 0.13/0.43 fof(f630,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f629,f52])).
% 0.13/0.43 fof(f631,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f630,f497])).
% 0.13/0.43 fof(f632,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl),
% 0.13/0.43 inference(backward_subsumption_resolution,[status(thm)],[f500,f633])).
% 0.13/0.43 fof(f633,plain,(
% 0.13/0.43 sK3_skl(sK9_skl,sK8_skl,sK7_skl)=sK9_skl|~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f631,f501])).
% 0.13/0.43 fof(f676,plain,(
% 0.13/0.43 ~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f632,f25])).
% 0.13/0.43 fof(f677,plain,(
% 0.13/0.43 ~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|~related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f632,f33])).
% 0.13/0.43 fof(f678,plain,(
% 0.13/0.43 ~rel_str(sK7_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f632,f29])).
% 0.13/0.43 fof(f686,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f676,f46])).
% 0.13/0.43 fof(f687,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|~related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f677,f46])).
% 0.13/0.43 fof(f688,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~element(sK9_skl,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f678,f46])).
% 0.13/0.43 fof(f695,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f686,f47])).
% 0.13/0.43 fof(f696,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f695,f48])).
% 0.13/0.43 fof(f697,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|element(sK2_skl(sK9_skl,sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f696])).
% 0.13/0.43 fof(f701,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f697,f49])).
% 0.13/0.43 fof(f713,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f701])).
% 0.13/0.43 fof(f724,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|~related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f687,f47])).
% 0.13/0.43 fof(f725,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f688,f47])).
% 0.13/0.43 fof(f726,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))|ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(resolution,[status(thm)],[f725,f48])).
% 0.13/0.43 fof(f727,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl))),
% 0.13/0.43 inference(duplicate_literals_removal,[status(thm)],[f726])).
% 0.13/0.43 fof(f728,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK2_skl(sK9_skl,sK8_skl,sK7_skl),sK9_skl)),
% 0.13/0.43 inference(backward_subsumption_resolution,[status(thm)],[f713,f727])).
% 0.13/0.43 fof(f729,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)|~relstr_element_smaller(sK7_skl,sK8_skl,sK9_skl)),
% 0.13/0.43 inference(backward_subsumption_resolution,[status(thm)],[f724,f728])).
% 0.13/0.43 fof(f733,plain,(
% 0.13/0.43 ex_inf_of_relstr_set(sK7_skl,sK8_skl)),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f729,f48])).
% 0.13/0.43 fof(f738,plain,(
% 0.13/0.43 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|relstr_element_smaller(sK7_skl,sK8_skl,sK10_skl(X0)))),
% 0.13/0.43 inference(backward_subsumption_resolution,[status(thm)],[f51,f733])).
% 0.13/0.43 fof(f739,plain,(
% 0.13/0.43 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|~related(sK7_skl,sK10_skl(X0),X0))),
% 0.13/0.43 inference(backward_subsumption_resolution,[status(thm)],[f52,f733])).
% 0.13/0.43 fof(f740,plain,(
% 0.13/0.43 ![X0]: (~element(X0,the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,X0)|element(sK10_skl(X0),the_carrier(sK7_skl)))),
% 0.13/0.43 inference(backward_subsumption_resolution,[status(thm)],[f50,f733])).
% 0.13/0.43 fof(f741,plain,(
% 0.13/0.43 ~rel_str(sK7_skl)|relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f733,f17])).
% 0.13/0.43 fof(f742,plain,(
% 0.13/0.43 ~rel_str(sK7_skl)|element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f733,f16])).
% 0.13/0.43 fof(f743,plain,(
% 0.13/0.43 relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f741,f46])).
% 0.13/0.43 fof(f744,plain,(
% 0.13/0.43 element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f742,f46])).
% 0.13/0.43 fof(f747,plain,(
% 0.13/0.43 ~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))|element(sK10_skl(sK0_skl(sK8_skl,sK7_skl)),the_carrier(sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f744,f740])).
% 0.13/0.43 fof(f748,plain,(
% 0.13/0.43 ~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))|relstr_element_smaller(sK7_skl,sK8_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f744,f738])).
% 0.13/0.43 fof(f759,plain,(
% 0.13/0.43 element(sK10_skl(sK0_skl(sK8_skl,sK7_skl)),the_carrier(sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f747,f743])).
% 0.13/0.43 fof(f760,plain,(
% 0.13/0.43 relstr_element_smaller(sK7_skl,sK8_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f748,f743])).
% 0.13/0.43 fof(f781,plain,(
% 0.13/0.43 ![X0]: (~rel_str(sK7_skl)|~ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))|related(sK7_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)),sK0_skl(X0,sK7_skl)))),
% 0.13/0.43 inference(resolution,[status(thm)],[f759,f18])).
% 0.13/0.43 fof(f791,plain,(
% 0.13/0.43 ![X0]: (~ex_inf_of_relstr_set(sK7_skl,X0)|~relstr_element_smaller(sK7_skl,X0,sK10_skl(sK0_skl(sK8_skl,sK7_skl)))|related(sK7_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)),sK0_skl(X0,sK7_skl)))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f781,f46])).
% 0.13/0.43 fof(f843,plain,(
% 0.13/0.43 ~ex_inf_of_relstr_set(sK7_skl,sK8_skl)|related(sK7_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)),sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f791,f760])).
% 0.13/0.43 fof(f844,plain,(
% 0.13/0.43 related(sK7_skl,sK10_skl(sK0_skl(sK8_skl,sK7_skl)),sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f843,f733])).
% 0.13/0.43 fof(f845,plain,(
% 0.13/0.43 ~element(sK0_skl(sK8_skl,sK7_skl),the_carrier(sK7_skl))|~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(resolution,[status(thm)],[f844,f739])).
% 0.13/0.43 fof(f846,plain,(
% 0.13/0.43 ~relstr_element_smaller(sK7_skl,sK8_skl,sK0_skl(sK8_skl,sK7_skl))),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f845,f744])).
% 0.13/0.43 fof(f849,plain,(
% 0.13/0.43 $false),
% 0.13/0.43 inference(forward_subsumption_resolution,[status(thm)],[f846,f743])).
% 0.13/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.45 % Elapsed time: 0.089200 seconds
% 0.13/0.45 % CPU time: 0.424165 seconds
% 0.13/0.45 % Total memory used: 88.633 MB
% 0.13/0.45 % Net memory used: 87.978 MB
%------------------------------------------------------------------------------