%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU360+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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.56s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU360+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n020.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 06:16:02 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 0.56/0.60 % Refutation found
% 0.56/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.56/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.56/0.60 fof(f3,axiom,(
% 0.56/0.60 (! [A] :( rel_str(A)=> ( lower_bounded_relstr(A)<=> (? [B] :( element(B,the_carrier(A))& relstr_element_smaller(A,the_carrier(A),B) ) )) ) )),
% 0.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f4,axiom,(
% 0.56/0.60 (! [A] :( rel_str(A)=> (! [B,C] :( element(C,the_carrier(A))=> ( relstr_element_smaller(A,B,C)<=> (! [D] :( element(D,the_carrier(A))=> ( in(D,B)=> related(A,C,D) ) ) )) ) )) )),
% 0.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f6,axiom,(
% 0.56/0.60 (! [A] :( rel_str(A)=> one_sorted_str(A) ) )),
% 0.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f13,axiom,(
% 0.56/0.60 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> ~ empty(the_carrier(A)) ) )),
% 0.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f16,axiom,(
% 0.56/0.60 (? [A] : empty(A) )),
% 0.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f19,axiom,(
% 0.56/0.60 (! [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.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f20,axiom,(
% 0.56/0.60 (! [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.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f21,axiom,(
% 0.56/0.60 (! [A,B] :( in(A,B)=> element(A,B) ) )),
% 0.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f22,axiom,(
% 0.56/0.60 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 0.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f23,conjecture,(
% 0.56/0.60 (! [A] :( ( ~ empty_carrier(A)& antisymmetric_relstr(A)& lower_bounded_relstr(A)& rel_str(A) )=> ( ex_sup_of_relstr_set(A,empty_set)& ex_inf_of_relstr_set(A,the_carrier(A)) ) ) )),
% 0.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f24,negated_conjecture,(
% 0.56/0.60 ~((! [A] :( ( ~ empty_carrier(A)& antisymmetric_relstr(A)& lower_bounded_relstr(A)& rel_str(A) )=> ( ex_sup_of_relstr_set(A,empty_set)& ex_inf_of_relstr_set(A,the_carrier(A)) ) ) ))),
% 0.56/0.60 inference(negated_conjecture,[status(cth)],[f23])).
% 0.56/0.60 fof(f25,axiom,(
% 0.56/0.60 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f26,axiom,(
% 0.56/0.60 (! [A] :( rel_str(A)=> (! [B] :( element(B,the_carrier(A))=> ( relstr_set_smaller(A,empty_set,B)& relstr_element_smaller(A,empty_set,B) ) ) )) )),
% 0.56/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.56/0.60 fof(f33,plain,(
% 0.56/0.60 ![A]: (~rel_str(A)|(lower_bounded_relstr(A)<=>(?[B]: (element(B,the_carrier(A))&relstr_element_smaller(A,the_carrier(A),B)))))),
% 0.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.56/0.60 fof(f34,plain,(
% 0.56/0.60 ![A]: (~rel_str(A)|((~lower_bounded_relstr(A)|(?[B]: (element(B,the_carrier(A))&relstr_element_smaller(A,the_carrier(A),B))))&(lower_bounded_relstr(A)|(![B]: (~element(B,the_carrier(A))|~relstr_element_smaller(A,the_carrier(A),B))))))),
% 0.56/0.60 inference(NNF_transformation,[status(thm)],[f33])).
% 0.56/0.60 fof(f35,plain,(
% 0.56/0.60 ![A]: (~rel_str(A)|((~lower_bounded_relstr(A)|(element(sK0_skl(A),the_carrier(A))&relstr_element_smaller(A,the_carrier(A),sK0_skl(A))))&(lower_bounded_relstr(A)|(![B]: (~element(B,the_carrier(A))|~relstr_element_smaller(A,the_carrier(A),B))))))),
% 0.56/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f34])).
% 0.56/0.60 fof(f36,plain,(
% 0.56/0.60 ![X0]: (~rel_str(X0)|~lower_bounded_relstr(X0)|element(sK0_skl(X0),the_carrier(X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f35])).
% 0.56/0.60 fof(f37,plain,(
% 0.56/0.60 ![X0]: (~rel_str(X0)|~lower_bounded_relstr(X0)|relstr_element_smaller(X0,the_carrier(X0),sK0_skl(X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f35])).
% 0.56/0.60 fof(f39,plain,(
% 0.56/0.60 ![A]: (~rel_str(A)|(![B,C]: (~element(C,the_carrier(A))|(relstr_element_smaller(A,B,C)<=>(![D]: (~element(D,the_carrier(A))|(~in(D,B)|related(A,C,D))))))))),
% 0.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.56/0.60 fof(f40,plain,(
% 0.56/0.60 ![A]: (~rel_str(A)|(![B,C]: (~element(C,the_carrier(A))|((~relstr_element_smaller(A,B,C)|(![D]: (~element(D,the_carrier(A))|(~in(D,B)|related(A,C,D)))))&(relstr_element_smaller(A,B,C)|(?[D]: (element(D,the_carrier(A))&(in(D,B)&~related(A,C,D)))))))))),
% 0.56/0.60 inference(NNF_transformation,[status(thm)],[f39])).
% 0.56/0.60 fof(f41,plain,(
% 0.56/0.60 ![A]: (~rel_str(A)|(![C]: (~element(C,the_carrier(A))|((![B]: (~relstr_element_smaller(A,B,C)|(![D]: (~element(D,the_carrier(A))|(~in(D,B)|related(A,C,D))))))&(![B]: (relstr_element_smaller(A,B,C)|(?[D]: (element(D,the_carrier(A))&(in(D,B)&~related(A,C,D))))))))))),
% 0.56/0.60 inference(miniscoping,[status(thm)],[f40])).
% 0.56/0.60 fof(f42,plain,(
% 0.56/0.60 ![A]: (~rel_str(A)|(![C]: (~element(C,the_carrier(A))|((![B]: (~relstr_element_smaller(A,B,C)|(![D]: (~element(D,the_carrier(A))|(~in(D,B)|related(A,C,D))))))&(![B]: (relstr_element_smaller(A,B,C)|(element(sK1_skl(B,C,A),the_carrier(A))&(in(sK1_skl(B,C,A),B)&~related(A,C,sK1_skl(B,C,A))))))))))),
% 0.56/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(D,sK1_skl(B,C,A))],[f41])).
% 0.56/0.60 fof(f43,plain,(
% 0.56/0.60 ![X0,X1,X2,X3]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~relstr_element_smaller(X0,X2,X1)|~element(X3,the_carrier(X0))|~in(X3,X2)|related(X0,X1,X3))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f42])).
% 0.56/0.60 fof(f44,plain,(
% 0.56/0.60 ![X0,X1,X2]: (~rel_str(X0)|~element(X1,the_carrier(X0))|relstr_element_smaller(X0,X2,X1)|element(sK1_skl(X2,X1,X0),the_carrier(X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f42])).
% 0.56/0.60 fof(f46,plain,(
% 0.56/0.60 ![X0,X1,X2]: (~rel_str(X0)|~element(X1,the_carrier(X0))|relstr_element_smaller(X0,X2,X1)|~related(X0,X1,sK1_skl(X2,X1,X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f42])).
% 0.56/0.60 fof(f47,plain,(
% 0.56/0.60 ![A]: (~rel_str(A)|one_sorted_str(A))),
% 0.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.56/0.60 fof(f48,plain,(
% 0.56/0.60 ![X0]: (~rel_str(X0)|one_sorted_str(X0))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f47])).
% 0.56/0.60 fof(f55,plain,(
% 0.56/0.60 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|~empty(the_carrier(A)))),
% 0.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.56/0.60 fof(f56,plain,(
% 0.56/0.60 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|~empty(the_carrier(X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f55])).
% 0.56/0.60 fof(f61,plain,(
% 0.56/0.60 empty(sK6_skl)),
% 0.56/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f16])).
% 0.56/0.60 fof(f62,plain,(
% 0.56/0.60 empty(sK6_skl)),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f61])).
% 0.56/0.60 fof(f68,plain,(
% 0.56/0.60 ![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.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.56/0.60 fof(f69,plain,(
% 0.56/0.60 ![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.56/0.60 inference(NNF_transformation,[status(thm)],[f68])).
% 0.56/0.60 fof(f70,plain,(
% 0.56/0.60 ![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))))))))&(![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.56/0.60 inference(miniscoping,[status(thm)],[f69])).
% 0.56/0.60 fof(f71,plain,(
% 0.56/0.60 ![A]: ((~antisymmetric_relstr(A)|~rel_str(A))|((![B]: (~ex_sup_of_relstr_set(A,B)|((element(sK9_skl(B,A),the_carrier(A))&relstr_set_smaller(A,B,sK9_skl(B,A)))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,sK9_skl(B,A),D)))))))&(![B]: (ex_sup_of_relstr_set(A,B)|(![C]: ((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(element(sK10_skl(C,B,A),the_carrier(A))&(relstr_set_smaller(A,B,sK10_skl(C,B,A))&~related(A,C,sK10_skl(C,B,A))))))))))),
% 0.56/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl]),skolemize(C,sK9_skl(B,A)),skolemize(D,sK10_skl(C,B,A))],[f70])).
% 0.56/0.60 fof(f75,plain,(
% 0.56/0.60 ![X0,X1,X2]: (~antisymmetric_relstr(X0)|~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|element(sK10_skl(X2,X1,X0),the_carrier(X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f71])).
% 0.56/0.60 fof(f77,plain,(
% 0.56/0.60 ![X0,X1,X2]: (~antisymmetric_relstr(X0)|~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|~related(X0,X2,sK10_skl(X2,X1,X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f71])).
% 0.56/0.60 fof(f78,plain,(
% 0.56/0.60 ![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.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.56/0.60 fof(f79,plain,(
% 0.56/0.60 ![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.56/0.60 inference(NNF_transformation,[status(thm)],[f78])).
% 0.56/0.60 fof(f80,plain,(
% 0.56/0.60 ![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))))))))&(![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.56/0.60 inference(miniscoping,[status(thm)],[f79])).
% 0.56/0.60 fof(f81,plain,(
% 0.56/0.60 ![A]: ((~antisymmetric_relstr(A)|~rel_str(A))|((![B]: (~ex_inf_of_relstr_set(A,B)|((element(sK11_skl(B,A),the_carrier(A))&relstr_element_smaller(A,B,sK11_skl(B,A)))&(![D]: (~element(D,the_carrier(A))|(~relstr_element_smaller(A,B,D)|related(A,D,sK11_skl(B,A))))))))&(![B]: (ex_inf_of_relstr_set(A,B)|(![C]: ((~element(C,the_carrier(A))|~relstr_element_smaller(A,B,C))|(element(sK12_skl(C,B,A),the_carrier(A))&(relstr_element_smaller(A,B,sK12_skl(C,B,A))&~related(A,sK12_skl(C,B,A),C)))))))))),
% 0.56/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl]),skolemize(C,sK11_skl(B,A)),skolemize(D,sK12_skl(C,B,A))],[f80])).
% 0.56/0.60 fof(f82,plain,(
% 0.56/0.60 ![X0,X1]: (~antisymmetric_relstr(X0)|~rel_str(X0)|~ex_inf_of_relstr_set(X0,X1)|element(sK11_skl(X1,X0),the_carrier(X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f81])).
% 0.56/0.60 fof(f83,plain,(
% 0.56/0.60 ![X0,X1]: (~antisymmetric_relstr(X0)|~rel_str(X0)|~ex_inf_of_relstr_set(X0,X1)|relstr_element_smaller(X0,X1,sK11_skl(X1,X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f81])).
% 0.56/0.60 fof(f85,plain,(
% 0.56/0.60 ![X0,X1,X2]: (~antisymmetric_relstr(X0)|~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|element(sK12_skl(X2,X1,X0),the_carrier(X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f81])).
% 0.56/0.60 fof(f86,plain,(
% 0.56/0.60 ![X0,X1,X2]: (~antisymmetric_relstr(X0)|~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,sK12_skl(X2,X1,X0)))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f81])).
% 0.56/0.60 fof(f87,plain,(
% 0.56/0.60 ![X0,X1,X2]: (~antisymmetric_relstr(X0)|~rel_str(X0)|ex_inf_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_element_smaller(X0,X1,X2)|~related(X0,sK12_skl(X2,X1,X0),X2))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f81])).
% 0.56/0.60 fof(f88,plain,(
% 0.56/0.60 ![A,B]: (~in(A,B)|element(A,B))),
% 0.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.56/0.60 fof(f89,plain,(
% 0.56/0.60 ![X0,X1]: (~in(X0,X1)|element(X0,X1))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f88])).
% 0.56/0.60 fof(f90,plain,(
% 0.56/0.60 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 0.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.56/0.60 fof(f91,plain,(
% 0.56/0.60 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f90])).
% 0.56/0.60 fof(f92,plain,(
% 0.56/0.60 (?[A]: ((((~empty_carrier(A)&antisymmetric_relstr(A))&lower_bounded_relstr(A))&rel_str(A))&(~ex_sup_of_relstr_set(A,empty_set)|~ex_inf_of_relstr_set(A,the_carrier(A)))))),
% 0.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.56/0.60 fof(f93,plain,(
% 0.56/0.60 ((((~empty_carrier(sK13_skl)&antisymmetric_relstr(sK13_skl))&lower_bounded_relstr(sK13_skl))&rel_str(sK13_skl))&(~ex_sup_of_relstr_set(sK13_skl,empty_set)|~ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))))),
% 0.56/0.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f92])).
% 0.56/0.60 fof(f94,plain,(
% 0.56/0.60 ~empty_carrier(sK13_skl)),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f93])).
% 0.56/0.60 fof(f95,plain,(
% 0.56/0.60 antisymmetric_relstr(sK13_skl)),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f93])).
% 0.56/0.60 fof(f96,plain,(
% 0.56/0.60 lower_bounded_relstr(sK13_skl)),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f93])).
% 0.56/0.60 fof(f97,plain,(
% 0.56/0.60 rel_str(sK13_skl)),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f93])).
% 0.56/0.60 fof(f98,plain,(
% 0.56/0.60 ~ex_sup_of_relstr_set(sK13_skl,empty_set)|~ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f93])).
% 0.56/0.60 fof(f99,plain,(
% 0.56/0.60 ![A]: (~empty(A)|A=empty_set)),
% 0.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.56/0.60 fof(f100,plain,(
% 0.56/0.60 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f99])).
% 0.56/0.60 fof(f101,plain,(
% 0.56/0.60 ![A]: (~rel_str(A)|(![B]: (~element(B,the_carrier(A))|(relstr_set_smaller(A,empty_set,B)&relstr_element_smaller(A,empty_set,B)))))),
% 0.56/0.60 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.56/0.60 fof(f102,plain,(
% 0.56/0.60 ![X0,X1]: (~rel_str(X0)|~element(X1,the_carrier(X0))|relstr_set_smaller(X0,empty_set,X1))),
% 0.56/0.60 inference(cnf_transformation,[status(thm)],[f101])).
% 0.56/0.60 fof(f114,plain,(
% 0.56/0.60 sK6_skl=empty_set),
% 0.56/0.60 inference(resolution,[status(thm)],[f62,f100])).
% 0.56/0.60 fof(f116,plain,(
% 0.56/0.60 ![X0,X1]: (~rel_str(X0)|~element(X1,the_carrier(X0))|relstr_set_smaller(X0,sK6_skl,X1))),
% 0.56/0.60 inference(backward_demodulation,[status(thm)],[f114,f102])).
% 0.56/0.60 fof(f118,plain,(
% 0.56/0.60 ~ex_sup_of_relstr_set(sK13_skl,sK6_skl)|~ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))),
% 0.56/0.60 inference(backward_demodulation,[status(thm)],[f114,f98])).
% 0.56/0.60 fof(f141,plain,(
% 0.56/0.60 ![X0,X1]: (~rel_str(sK13_skl)|ex_inf_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,X0,X1)|relstr_element_smaller(sK13_skl,X0,sK12_skl(X1,X0,sK13_skl)))),
% 0.56/0.60 inference(resolution,[status(thm)],[f86,f95])).
% 0.56/0.60 fof(f142,plain,(
% 0.56/0.60 ![X0,X1]: (ex_inf_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,X0,X1)|relstr_element_smaller(sK13_skl,X0,sK12_skl(X1,X0,sK13_skl)))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f141,f97])).
% 0.56/0.60 fof(f145,plain,(
% 0.56/0.60 ![X0,X1]: (~rel_str(sK13_skl)|ex_inf_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,X0,X1)|~related(sK13_skl,sK12_skl(X1,X0,sK13_skl),X1))),
% 0.56/0.60 inference(resolution,[status(thm)],[f87,f95])).
% 0.56/0.60 fof(f146,plain,(
% 0.56/0.60 ![X0,X1]: (ex_inf_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,X0,X1)|~related(sK13_skl,sK12_skl(X1,X0,sK13_skl),X1))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f145,f97])).
% 0.56/0.60 fof(f151,plain,(
% 0.56/0.60 ![X0,X1,X2]: (empty(the_carrier(X0))|in(sK12_skl(X1,X2,X0),the_carrier(X0))|~antisymmetric_relstr(X0)|~rel_str(X0)|ex_inf_of_relstr_set(X0,X2)|~element(X1,the_carrier(X0))|~relstr_element_smaller(X0,X2,X1))),
% 0.56/0.60 inference(resolution,[status(thm)],[f91,f85])).
% 0.56/0.60 fof(f152,plain,(
% 0.56/0.60 ![X0,X1,X2]: (empty(the_carrier(X0))|in(sK10_skl(X1,X2,X0),the_carrier(X0))|~antisymmetric_relstr(X0)|~rel_str(X0)|ex_sup_of_relstr_set(X0,X2)|~element(X1,the_carrier(X0))|~relstr_set_smaller(X0,X2,X1))),
% 0.56/0.60 inference(resolution,[status(thm)],[f91,f75])).
% 0.56/0.60 fof(f155,plain,(
% 0.56/0.60 ![X0,X1,X2]: (empty(the_carrier(X0))|in(sK1_skl(X1,X2,X0),the_carrier(X0))|~rel_str(X0)|~element(X2,the_carrier(X0))|relstr_element_smaller(X0,X1,X2))),
% 0.56/0.60 inference(resolution,[status(thm)],[f91,f44])).
% 0.56/0.60 fof(f156,plain,(
% 0.56/0.60 ![X0]: (empty(the_carrier(X0))|in(sK0_skl(X0),the_carrier(X0))|~rel_str(X0)|~lower_bounded_relstr(X0))),
% 0.56/0.60 inference(resolution,[status(thm)],[f91,f36])).
% 0.56/0.60 fof(f165,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|in(sK12_skl(X0,X1,sK13_skl),the_carrier(sK13_skl))|~rel_str(sK13_skl)|ex_inf_of_relstr_set(sK13_skl,X1)|~element(X0,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,X1,X0))),
% 0.56/0.60 inference(resolution,[status(thm)],[f151,f95])).
% 0.56/0.60 fof(f166,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|in(sK12_skl(X0,X1,sK13_skl),the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,X1)|~element(X0,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,X1,X0))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f165,f97])).
% 0.56/0.60 fof(f167,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|in(sK10_skl(X0,X1,sK13_skl),the_carrier(sK13_skl))|~rel_str(sK13_skl)|ex_sup_of_relstr_set(sK13_skl,X1)|~element(X0,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X1,X0))),
% 0.56/0.60 inference(resolution,[status(thm)],[f152,f95])).
% 0.56/0.60 fof(f168,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|in(sK10_skl(X0,X1,sK13_skl),the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X1)|~element(X0,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X1,X0))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f167,f97])).
% 0.56/0.60 fof(f170,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|in(sK1_skl(X0,X1,sK13_skl),the_carrier(sK13_skl))|~element(X1,the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X0,X1))),
% 0.56/0.60 inference(resolution,[status(thm)],[f155,f97])).
% 0.56/0.60 fof(f171,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|in(sK0_skl(sK13_skl),the_carrier(sK13_skl))|~rel_str(sK13_skl)),
% 0.56/0.60 inference(resolution,[status(thm)],[f156,f96])).
% 0.56/0.60 fof(f172,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|in(sK0_skl(sK13_skl),the_carrier(sK13_skl))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f171,f97])).
% 0.56/0.60 fof(f174,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|element(sK0_skl(sK13_skl),the_carrier(sK13_skl))),
% 0.56/0.60 inference(resolution,[status(thm)],[f172,f89])).
% 0.56/0.60 fof(f175,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|~rel_str(X0)|~element(X1,the_carrier(X0))|~relstr_element_smaller(X0,the_carrier(sK13_skl),X1)|~element(sK0_skl(sK13_skl),the_carrier(X0))|related(X0,X1,sK0_skl(sK13_skl)))),
% 0.56/0.60 inference(resolution,[status(thm)],[f172,f43])).
% 0.56/0.60 fof(f177,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,X0,X1)|element(sK12_skl(X1,X0,sK13_skl),the_carrier(sK13_skl)))),
% 0.56/0.60 inference(resolution,[status(thm)],[f166,f89])).
% 0.56/0.60 fof(f180,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1)|element(sK10_skl(X1,X0,sK13_skl),the_carrier(sK13_skl)))),
% 0.56/0.60 inference(resolution,[status(thm)],[f168,f89])).
% 0.56/0.60 fof(f181,plain,(
% 0.56/0.60 ![X0,X1,X2,X3]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1)|~rel_str(X2)|~element(X3,the_carrier(X2))|~relstr_element_smaller(X2,the_carrier(sK13_skl),X3)|~element(sK10_skl(X1,X0,sK13_skl),the_carrier(X2))|related(X2,X3,sK10_skl(X1,X0,sK13_skl)))),
% 0.56/0.60 inference(resolution,[status(thm)],[f168,f43])).
% 0.56/0.60 fof(f186,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|~element(X0,the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X1,X0)|element(sK1_skl(X1,X0,sK13_skl),the_carrier(sK13_skl)))),
% 0.56/0.60 inference(resolution,[status(thm)],[f170,f89])).
% 0.56/0.60 fof(f187,plain,(
% 0.56/0.60 ![X0,X1,X2,X3]: (empty(the_carrier(sK13_skl))|~element(X0,the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X1,X0)|~rel_str(X2)|~element(X3,the_carrier(X2))|~relstr_element_smaller(X2,the_carrier(sK13_skl),X3)|~element(sK1_skl(X1,X0,sK13_skl),the_carrier(X2))|related(X2,X3,sK1_skl(X1,X0,sK13_skl)))),
% 0.56/0.60 inference(resolution,[status(thm)],[f170,f43])).
% 0.56/0.60 fof(f189,plain,(
% 0.56/0.60 ![X0]: (empty(the_carrier(sK13_skl))|~rel_str(sK13_skl)|~element(sK12_skl(sK0_skl(sK13_skl),X0,sK13_skl),the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),sK12_skl(sK0_skl(sK13_skl),X0,sK13_skl))|~element(sK0_skl(sK13_skl),the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,X0)|~element(sK0_skl(sK13_skl),the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,X0,sK0_skl(sK13_skl)))),
% 0.56/0.60 inference(resolution,[status(thm)],[f175,f146])).
% 0.56/0.60 fof(f190,plain,(
% 0.56/0.60 ![X0]: (empty(the_carrier(sK13_skl))|~rel_str(sK13_skl)|~element(sK12_skl(sK0_skl(sK13_skl),X0,sK13_skl),the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),sK12_skl(sK0_skl(sK13_skl),X0,sK13_skl))|~element(sK0_skl(sK13_skl),the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,X0)|~relstr_element_smaller(sK13_skl,X0,sK0_skl(sK13_skl)))),
% 0.56/0.60 inference(duplicate_literals_removal,[status(thm)],[f189])).
% 0.56/0.60 fof(f191,plain,(
% 0.56/0.60 ![X0]: (empty(the_carrier(sK13_skl))|~element(sK12_skl(sK0_skl(sK13_skl),X0,sK13_skl),the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),sK12_skl(sK0_skl(sK13_skl),X0,sK13_skl))|~element(sK0_skl(sK13_skl),the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,X0)|~relstr_element_smaller(sK13_skl,X0,sK0_skl(sK13_skl)))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f190,f97])).
% 0.56/0.60 fof(f218,plain,(
% 0.56/0.60 ![X0,X1,X2]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1)|~rel_str(sK13_skl)|~element(X2,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X2)|related(sK13_skl,X2,sK10_skl(X1,X0,sK13_skl))|empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1))),
% 0.56/0.60 inference(resolution,[status(thm)],[f181,f180])).
% 0.56/0.60 fof(f220,plain,(
% 0.56/0.60 ![X0,X1,X2]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1)|~rel_str(sK13_skl)|~element(X2,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X2)|related(sK13_skl,X2,sK10_skl(X1,X0,sK13_skl)))),
% 0.56/0.60 inference(duplicate_literals_removal,[status(thm)],[f218])).
% 0.56/0.60 fof(f221,plain,(
% 0.56/0.60 ![X0,X1,X2]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1)|~element(X2,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X2)|related(sK13_skl,X2,sK10_skl(X1,X0,sK13_skl)))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f220,f97])).
% 0.56/0.60 fof(f225,plain,(
% 0.56/0.60 ![X0,X1,X2]: (empty(the_carrier(sK13_skl))|~element(X0,the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X1,X0)|~element(X2,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X2)|~element(sK1_skl(X1,X0,sK13_skl),the_carrier(sK13_skl))|related(sK13_skl,X2,sK1_skl(X1,X0,sK13_skl)))),
% 0.56/0.60 inference(resolution,[status(thm)],[f187,f97])).
% 0.56/0.60 fof(f226,plain,(
% 0.56/0.60 ![X0,X1,X2]: (empty(the_carrier(sK13_skl))|~element(X0,the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X1,X0)|~element(X2,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X2)|related(sK13_skl,X2,sK1_skl(X1,X0,sK13_skl)))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f225,f186])).
% 0.56/0.60 fof(f237,plain,(
% 0.56/0.60 ![X0]: (empty(the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),sK12_skl(sK0_skl(sK13_skl),X0,sK13_skl))|~element(sK0_skl(sK13_skl),the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,X0)|~relstr_element_smaller(sK13_skl,X0,sK0_skl(sK13_skl)))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f191,f177])).
% 0.56/0.60 fof(f238,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|~element(sK0_skl(sK13_skl),the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),sK0_skl(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))|~element(sK0_skl(sK13_skl),the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),sK0_skl(sK13_skl))),
% 0.56/0.60 inference(resolution,[status(thm)],[f237,f142])).
% 0.56/0.60 fof(f239,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|~element(sK0_skl(sK13_skl),the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),sK0_skl(sK13_skl))),
% 0.56/0.60 inference(duplicate_literals_removal,[status(thm)],[f238])).
% 0.56/0.60 fof(f240,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),sK0_skl(sK13_skl))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f239,f174])).
% 0.56/0.60 fof(f241,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))|~rel_str(sK13_skl)|~lower_bounded_relstr(sK13_skl)),
% 0.56/0.60 inference(resolution,[status(thm)],[f240,f37])).
% 0.56/0.60 fof(f242,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))|~lower_bounded_relstr(sK13_skl)),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f241,f97])).
% 0.56/0.60 fof(f243,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f242,f96])).
% 0.56/0.60 fof(f244,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|~ex_sup_of_relstr_set(sK13_skl,sK6_skl)),
% 0.56/0.60 inference(resolution,[status(thm)],[f243,f118])).
% 0.56/0.60 fof(f246,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|~antisymmetric_relstr(sK13_skl)|~rel_str(sK13_skl)|element(sK11_skl(the_carrier(sK13_skl),sK13_skl),the_carrier(sK13_skl))),
% 0.56/0.60 inference(resolution,[status(thm)],[f243,f82])).
% 0.56/0.60 fof(f248,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|~rel_str(sK13_skl)|element(sK11_skl(the_carrier(sK13_skl),sK13_skl),the_carrier(sK13_skl))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f246,f95])).
% 0.56/0.60 fof(f263,plain,(
% 0.56/0.60 empty(the_carrier(sK13_skl))|element(sK11_skl(the_carrier(sK13_skl),sK13_skl),the_carrier(sK13_skl))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f248,f97])).
% 0.56/0.60 fof(f270,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1)|~element(X1,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X1)|~antisymmetric_relstr(sK13_skl)|~rel_str(sK13_skl)|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1))),
% 0.56/0.60 inference(resolution,[status(thm)],[f221,f77])).
% 0.56/0.60 fof(f272,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1)|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X1)|~antisymmetric_relstr(sK13_skl)|~rel_str(sK13_skl))),
% 0.56/0.60 inference(duplicate_literals_removal,[status(thm)],[f270])).
% 0.56/0.60 fof(f273,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1)|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X1)|~rel_str(sK13_skl))),
% 0.56/0.60 inference(forward_subsumption_resolution,[status(thm)],[f272,f95])).
% 0.56/0.60 fof(f278,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|~element(X0,the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X1,X0)|~element(X0,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)|~rel_str(sK13_skl)|~element(X0,the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X1,X0))),
% 0.56/0.60 inference(resolution,[status(thm)],[f226,f46])).
% 0.56/0.60 fof(f280,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|~element(X0,the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X1,X0)|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)|~rel_str(sK13_skl))),
% 0.56/0.60 inference(duplicate_literals_removal,[status(thm)],[f278])).
% 0.56/0.60 fof(f281,plain,(
% 0.56/0.60 ![X0,X1]: (empty(the_carrier(sK13_skl))|~element(X0,the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X1,X0)|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0))),
% 0.56/0.62 inference(forward_subsumption_resolution,[status(thm)],[f280,f97])).
% 0.56/0.62 fof(f286,plain,(
% 0.56/0.62 ![X0]: (empty(the_carrier(sK13_skl))|~element(sK11_skl(the_carrier(sK13_skl),sK13_skl),the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X0,sK11_skl(the_carrier(sK13_skl),sK13_skl))|~antisymmetric_relstr(sK13_skl)|~rel_str(sK13_skl)|~ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl)))),
% 0.56/0.62 inference(resolution,[status(thm)],[f281,f83])).
% 0.56/0.62 fof(f288,plain,(
% 0.56/0.62 ![X0]: (empty(the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X0,sK11_skl(the_carrier(sK13_skl),sK13_skl))|~antisymmetric_relstr(sK13_skl)|~rel_str(sK13_skl)|~ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl)))),
% 0.56/0.62 inference(forward_subsumption_resolution,[status(thm)],[f286,f82])).
% 0.56/0.62 fof(f308,plain,(
% 0.56/0.62 ![X0]: (empty(the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X0,sK11_skl(the_carrier(sK13_skl),sK13_skl))|~rel_str(sK13_skl)|~ex_inf_of_relstr_set(sK13_skl,the_carrier(sK13_skl)))),
% 0.56/0.62 inference(forward_subsumption_resolution,[status(thm)],[f288,f95])).
% 0.56/0.62 fof(f309,plain,(
% 0.56/0.62 ![X0]: (empty(the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X0,sK11_skl(the_carrier(sK13_skl),sK13_skl))|~rel_str(sK13_skl)|empty(the_carrier(sK13_skl)))),
% 0.56/0.62 inference(resolution,[status(thm)],[f308,f243])).
% 0.56/0.62 fof(f310,plain,(
% 0.56/0.62 ![X0]: (empty(the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X0,sK11_skl(the_carrier(sK13_skl),sK13_skl))|~rel_str(sK13_skl))),
% 0.56/0.62 inference(duplicate_literals_removal,[status(thm)],[f309])).
% 0.56/0.62 fof(f311,plain,(
% 0.56/0.62 ![X0]: (empty(the_carrier(sK13_skl))|relstr_element_smaller(sK13_skl,X0,sK11_skl(the_carrier(sK13_skl),sK13_skl)))),
% 0.56/0.62 inference(forward_subsumption_resolution,[status(thm)],[f310,f97])).
% 0.56/0.62 fof(f316,plain,(
% 0.56/0.62 ![X0,X1]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,X0)|~element(X1,the_carrier(sK13_skl))|~relstr_set_smaller(sK13_skl,X0,X1)|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X1))),
% 0.56/0.62 inference(forward_subsumption_resolution,[status(thm)],[f273,f97])).
% 0.56/0.62 fof(f317,plain,(
% 0.56/0.62 ![X0]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,sK6_skl)|~element(X0,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)|~rel_str(sK13_skl)|~element(X0,the_carrier(sK13_skl)))),
% 0.56/0.62 inference(resolution,[status(thm)],[f316,f116])).
% 0.56/0.62 fof(f320,plain,(
% 0.56/0.62 ![X0]: (empty(the_carrier(sK13_skl))|ex_sup_of_relstr_set(sK13_skl,sK6_skl)|~element(X0,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)|~rel_str(sK13_skl))),
% 0.56/0.62 inference(duplicate_literals_removal,[status(thm)],[f317])).
% 0.56/0.62 fof(f321,plain,(
% 0.56/0.62 ![X0]: (empty(the_carrier(sK13_skl))|~element(X0,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0)|~rel_str(sK13_skl))),
% 0.56/0.62 inference(forward_subsumption_resolution,[status(thm)],[f320,f244])).
% 0.56/0.62 fof(f335,plain,(
% 0.56/0.62 ![X0]: (empty(the_carrier(sK13_skl))|~element(X0,the_carrier(sK13_skl))|~relstr_element_smaller(sK13_skl,the_carrier(sK13_skl),X0))),
% 0.56/0.62 inference(forward_subsumption_resolution,[status(thm)],[f321,f97])).
% 0.56/0.62 fof(f336,plain,(
% 0.56/0.62 empty(the_carrier(sK13_skl))|~element(sK11_skl(the_carrier(sK13_skl),sK13_skl),the_carrier(sK13_skl))|empty(the_carrier(sK13_skl))),
% 0.56/0.62 inference(resolution,[status(thm)],[f335,f311])).
% 0.56/0.62 fof(f341,plain,(
% 0.56/0.62 empty(the_carrier(sK13_skl))|~element(sK11_skl(the_carrier(sK13_skl),sK13_skl),the_carrier(sK13_skl))),
% 0.56/0.62 inference(duplicate_literals_removal,[status(thm)],[f336])).
% 0.56/0.62 fof(f342,plain,(
% 0.56/0.62 empty(the_carrier(sK13_skl))),
% 0.56/0.62 inference(forward_subsumption_resolution,[status(thm)],[f341,f263])).
% 0.56/0.62 fof(f347,plain,(
% 0.56/0.62 empty_carrier(sK13_skl)|~one_sorted_str(sK13_skl)),
% 0.56/0.62 inference(resolution,[status(thm)],[f342,f56])).
% 0.56/0.62 fof(f351,plain,(
% 0.56/0.62 ~one_sorted_str(sK13_skl)),
% 0.56/0.62 inference(forward_subsumption_resolution,[status(thm)],[f347,f94])).
% 0.56/0.62 fof(f352,plain,(
% 0.56/0.62 ~rel_str(sK13_skl)),
% 0.56/0.62 inference(resolution,[status(thm)],[f351,f48])).
% 0.56/0.62 fof(f353,plain,(
% 0.56/0.62 $false),
% 0.56/0.62 inference(forward_subsumption_resolution,[status(thm)],[f352,f97])).
% 0.56/0.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.56/0.62 % Elapsed time: 0.194531 seconds
% 0.56/0.62 % CPU time: 1.152458 seconds
% 0.56/0.62 % Total memory used: 101.308 MB
% 0.56/0.62 % Net memory used: 100.507 MB
%------------------------------------------------------------------------------