%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU348+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:23 PM UTC 2026
% Result : Theorem 0.41s 0.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU348+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n017.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 06:09:42 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.23/0.64 % Drodi V4.1.1
% 0.41/0.93 % Refutation found
% 0.41/0.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.41/0.93 % SZS output start CNFRefutation for theBenchmark
% 0.41/0.93 fof(f19,axiom,(
% 0.41/0.93 (! [A] :( latt_str(A)=> ( ( ~ empty_carrier(A)& lattice(A) )=> ( ~ empty_carrier(A)& join_commutative(A)& join_associative(A)& meet_commutative(A)& meet_associative(A)& meet_absorbing(A)& join_absorbing(A) ) ) ) )),
% 0.41/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/0.93 fof(f56,axiom,(
% 0.41/0.93 (! [A] :( ( ~ empty_carrier(A)& latt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( latt_set_smaller(A,B,C)<=> (! [D] :( element(D,the_carrier(A))=> ( in(D,C)=> below(A,B,D) ) ) )) )) )) )),
% 0.41/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/0.93 fof(f83,axiom,(
% 0.41/0.93 (! [A] :( ( ~ empty_carrier(A)& lattice(A)& latt_str(A) )=> poset_of_lattice(A) = rel_str_of(the_carrier(A),k2_lattice3(A)) ) )),
% 0.41/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/0.93 fof(f90,axiom,(
% 0.41/0.93 (! [A,B,C] :( C = unordered_pair(A,B)<=> (! [D] :( in(D,C)<=> ( D = A| D = B ) ) )) )),
% 0.41/0.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/0.94 fof(f96,axiom,(
% 0.41/0.94 (! [A] :( ( ~ empty_carrier(A)& lattice(A)& latt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> cast_to_el_of_LattPOSet(A,B) = B ) )) )),
% 0.41/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/0.94 fof(f105,axiom,(
% 0.41/0.94 (! [A] :( ( ~ empty_carrier(A)& lattice(A)& latt_str(A) )=> (! [B] :( element(B,the_carrier(poset_of_lattice(A)))=> cast_to_el_of_lattice(A,B) = B ) )) )),
% 0.41/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/0.94 fof(f176,axiom,(
% 0.41/0.94 (! [A] :( ( ~ empty_carrier(A)& lattice(A)& latt_str(A) )=> ( strict_rel_str(poset_of_lattice(A))& reflexive_relstr(poset_of_lattice(A))& transitive_relstr(poset_of_lattice(A))& antisymmetric_relstr(poset_of_lattice(A))& rel_str(poset_of_lattice(A)) ) ) )),
% 0.41/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/0.94 fof(f189,axiom,(
% 0.41/0.94 (! [A,B] :( ( ~ empty_carrier(A)& lattice(A)& latt_str(A)& element(B,the_carrier(poset_of_lattice(A))) )=> element(cast_to_el_of_lattice(A,B),the_carrier(A)) ) )),
% 0.41/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/0.94 fof(f519,lemma,(
% 0.41/0.94 (! [A,B] :( ( ~ empty_carrier(B)& lattice(B)& latt_str(B) )=> (! [C] :( element(C,the_carrier(B))=> ( latt_set_smaller(B,C,A)<=> relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C)) ) ) )) )),
% 0.41/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/0.94 fof(f522,conjecture,(
% 0.41/0.94 (! [A,B] :( ( ~ empty_carrier(B)& lattice(B)& latt_str(B) )=> (! [C] :( element(C,the_carrier(poset_of_lattice(B)))=> ( relstr_element_smaller(poset_of_lattice(B),A,C)<=> latt_set_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) )) )),
% 0.41/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.41/0.94 fof(f523,negated_conjecture,(
% 0.41/0.94 ~((! [A,B] :( ( ~ empty_carrier(B)& lattice(B)& latt_str(B) )=> (! [C] :( element(C,the_carrier(poset_of_lattice(B)))=> ( relstr_element_smaller(poset_of_lattice(B),A,C)<=> latt_set_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) )) ))),
% 0.41/0.94 inference(negated_conjecture,[status(cth)],[f522])).
% 0.41/0.94 fof(f697,plain,(
% 0.41/0.94 ![A]: (~latt_str(A)|((empty_carrier(A)|~lattice(A))|((((((~empty_carrier(A)&join_commutative(A))&join_associative(A))&meet_commutative(A))&meet_associative(A))&meet_absorbing(A))&join_absorbing(A))))),
% 0.41/0.94 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.41/0.94 fof(f699,plain,(
% 0.41/0.94 ![X0]: (~latt_str(X0)|empty_carrier(X0)|~lattice(X0)|join_commutative(X0))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f697])).
% 0.41/0.94 fof(f700,plain,(
% 0.41/0.94 ![X0]: (~latt_str(X0)|empty_carrier(X0)|~lattice(X0)|join_associative(X0))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f697])).
% 0.41/0.94 fof(f701,plain,(
% 0.41/0.94 ![X0]: (~latt_str(X0)|empty_carrier(X0)|~lattice(X0)|meet_commutative(X0))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f697])).
% 0.41/0.94 fof(f702,plain,(
% 0.41/0.94 ![X0]: (~latt_str(X0)|empty_carrier(X0)|~lattice(X0)|meet_associative(X0))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f697])).
% 0.41/0.94 fof(f703,plain,(
% 0.41/0.94 ![X0]: (~latt_str(X0)|empty_carrier(X0)|~lattice(X0)|meet_absorbing(X0))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f697])).
% 0.41/0.94 fof(f704,plain,(
% 0.41/0.94 ![X0]: (~latt_str(X0)|empty_carrier(X0)|~lattice(X0)|join_absorbing(X0))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f697])).
% 0.41/0.94 fof(f870,plain,(
% 0.41/0.94 ![A]: ((empty_carrier(A)|~latt_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: (latt_set_smaller(A,B,C)<=>(![D]: (~element(D,the_carrier(A))|(~in(D,C)|below(A,B,D)))))))))),
% 0.41/0.94 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.41/0.94 fof(f871,plain,(
% 0.41/0.94 ![A]: ((empty_carrier(A)|~latt_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: ((~latt_set_smaller(A,B,C)|(![D]: (~element(D,the_carrier(A))|(~in(D,C)|below(A,B,D)))))&(latt_set_smaller(A,B,C)|(?[D]: (element(D,the_carrier(A))&(in(D,C)&~below(A,B,D))))))))))),
% 0.41/0.94 inference(NNF_transformation,[status(thm)],[f870])).
% 0.41/0.94 fof(f872,plain,(
% 0.41/0.94 ![A]: ((empty_carrier(A)|~latt_str(A))|(![B]: (~element(B,the_carrier(A))|((![C]: (~latt_set_smaller(A,B,C)|(![D]: (~element(D,the_carrier(A))|(~in(D,C)|below(A,B,D))))))&(![C]: (latt_set_smaller(A,B,C)|(?[D]: (element(D,the_carrier(A))&(in(D,C)&~below(A,B,D))))))))))),
% 0.41/0.94 inference(miniscoping,[status(thm)],[f871])).
% 0.41/0.94 fof(f873,plain,(
% 0.41/0.94 ![A]: ((empty_carrier(A)|~latt_str(A))|(![B]: (~element(B,the_carrier(A))|((![C]: (~latt_set_smaller(A,B,C)|(![D]: (~element(D,the_carrier(A))|(~in(D,C)|below(A,B,D))))))&(![C]: (latt_set_smaller(A,B,C)|(element(sK21_skl(C,B,A),the_carrier(A))&(in(sK21_skl(C,B,A),C)&~below(A,B,sK21_skl(C,B,A))))))))))),
% 0.41/0.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(D,sK21_skl(C,B,A))],[f872])).
% 0.41/0.94 fof(f874,plain,(
% 0.41/0.94 ![X0,X1,X2,X3]: (empty_carrier(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|~latt_set_smaller(X0,X1,X2)|~element(X3,the_carrier(X0))|~in(X3,X2)|below(X0,X1,X3))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f873])).
% 0.41/0.94 fof(f875,plain,(
% 0.41/0.94 ![X0,X1,X2]: (empty_carrier(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|latt_set_smaller(X0,X1,X2)|element(sK21_skl(X2,X1,X0),the_carrier(X0)))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f873])).
% 0.41/0.94 fof(f1063,plain,(
% 0.41/0.94 ![A]: (((empty_carrier(A)|~lattice(A))|~latt_str(A))|poset_of_lattice(A)=rel_str_of(the_carrier(A),k2_lattice3(A)))),
% 0.41/0.94 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 0.41/0.94 fof(f1064,plain,(
% 0.41/0.94 ![X0]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|poset_of_lattice(X0)=rel_str_of(the_carrier(X0),k2_lattice3(X0)))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f1063])).
% 0.41/0.94 fof(f1098,plain,(
% 0.41/0.94 ![A,B,C]: ((~C=unordered_pair(A,B)|(![D]: ((~in(D,C)|(D=A|D=B))&(in(D,C)|(~D=A&~D=B)))))&(C=unordered_pair(A,B)|(?[D]: ((~in(D,C)|(~D=A&~D=B))&(in(D,C)|(D=A|D=B))))))),
% 0.41/0.94 inference(NNF_transformation,[status(thm)],[f90])).
% 0.41/0.94 fof(f1099,plain,(
% 0.41/0.94 (![A,B,C]: (~C=unordered_pair(A,B)|((![D]: (~in(D,C)|(D=A|D=B)))&(![D]: (in(D,C)|(~D=A&~D=B))))))&(![A,B,C]: (C=unordered_pair(A,B)|(?[D]: ((~in(D,C)|(~D=A&~D=B))&(in(D,C)|(D=A|D=B))))))),
% 0.41/0.94 inference(miniscoping,[status(thm)],[f1098])).
% 0.41/0.94 fof(f1100,plain,(
% 0.41/0.94 (![A,B,C]: (~C=unordered_pair(A,B)|((![D]: (~in(D,C)|(D=A|D=B)))&(![D]: (in(D,C)|(~D=A&~D=B))))))&(![A,B,C]: (C=unordered_pair(A,B)|((~in(sK55_skl(C,B,A),C)|(~sK55_skl(C,B,A)=A&~sK55_skl(C,B,A)=B))&(in(sK55_skl(C,B,A),C)|(sK55_skl(C,B,A)=A|sK55_skl(C,B,A)=B)))))),
% 0.41/0.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK55_skl]),skolemize(D,sK55_skl(C,B,A))],[f1099])).
% 0.41/0.94 fof(f1102,plain,(
% 0.41/0.94 ![X0,X1,X2,X3]: (~X0=unordered_pair(X1,X2)|in(X3,X0)|~X3=X1)),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f1100])).
% 0.41/0.94 fof(f1103,plain,(
% 0.41/0.94 ![X0,X1,X2,X3]: (~X0=unordered_pair(X1,X2)|in(X3,X0)|~X3=X2)),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f1100])).
% 0.41/0.94 fof(f1151,plain,(
% 0.41/0.94 ![A]: (((empty_carrier(A)|~lattice(A))|~latt_str(A))|(![B]: (~element(B,the_carrier(A))|cast_to_el_of_LattPOSet(A,B)=B)))),
% 0.41/0.94 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 0.41/0.94 fof(f1152,plain,(
% 0.41/0.94 ![X0,X1]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|cast_to_el_of_LattPOSet(X0,X1)=X1)),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f1151])).
% 0.41/0.94 fof(f1207,plain,(
% 0.41/0.94 ![A]: (((empty_carrier(A)|~lattice(A))|~latt_str(A))|(![B]: (~element(B,the_carrier(poset_of_lattice(A)))|cast_to_el_of_lattice(A,B)=B)))),
% 0.41/0.94 inference(pre_NNF_transformation,[status(thm)],[f105])).
% 0.41/0.94 fof(f1208,plain,(
% 0.41/0.94 ![X0,X1]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(poset_of_lattice(X0)))|cast_to_el_of_lattice(X0,X1)=X1)),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f1207])).
% 0.41/0.94 fof(f1481,plain,(
% 0.41/0.94 ![A]: (((empty_carrier(A)|~lattice(A))|~latt_str(A))|((((strict_rel_str(poset_of_lattice(A))&reflexive_relstr(poset_of_lattice(A)))&transitive_relstr(poset_of_lattice(A)))&antisymmetric_relstr(poset_of_lattice(A)))&rel_str(poset_of_lattice(A))))),
% 0.41/0.94 inference(pre_NNF_transformation,[status(thm)],[f176])).
% 0.41/0.94 fof(f1486,plain,(
% 0.41/0.94 ![X0]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|rel_str(poset_of_lattice(X0)))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f1481])).
% 0.41/0.94 fof(f1501,plain,(
% 0.41/0.94 ![A,B]: ((((empty_carrier(A)|~lattice(A))|~latt_str(A))|~element(B,the_carrier(poset_of_lattice(A))))|element(cast_to_el_of_lattice(A,B),the_carrier(A)))),
% 0.41/0.94 inference(pre_NNF_transformation,[status(thm)],[f189])).
% 0.41/0.94 fof(f1502,plain,(
% 0.41/0.94 ![X0,X1]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(poset_of_lattice(X0)))|element(cast_to_el_of_lattice(X0,X1),the_carrier(X0)))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f1501])).
% 0.41/0.94 fof(f2928,plain,(
% 0.41/0.94 ![A,B]: (((empty_carrier(B)|~lattice(B))|~latt_str(B))|(![C]: (~element(C,the_carrier(B))|(latt_set_smaller(B,C,A)<=>relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))))))),
% 0.41/0.94 inference(pre_NNF_transformation,[status(thm)],[f519])).
% 0.41/0.94 fof(f2929,plain,(
% 0.41/0.94 ![A,B]: (((empty_carrier(B)|~lattice(B))|~latt_str(B))|(![C]: (~element(C,the_carrier(B))|((~latt_set_smaller(B,C,A)|relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C)))&(latt_set_smaller(B,C,A)|~relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C)))))))),
% 0.41/0.94 inference(NNF_transformation,[status(thm)],[f2928])).
% 0.41/0.94 fof(f2930,plain,(
% 0.41/0.94 ![B]: (((empty_carrier(B)|~lattice(B))|~latt_str(B))|(![C]: (~element(C,the_carrier(B))|((![A]: (~latt_set_smaller(B,C,A)|relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))))&(![A]: (latt_set_smaller(B,C,A)|~relstr_element_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))))))))),
% 0.41/0.94 inference(miniscoping,[status(thm)],[f2929])).
% 0.41/0.94 fof(f2931,plain,(
% 0.41/0.94 ![X0,X1,X2]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|~latt_set_smaller(X0,X1,X2)|relstr_element_smaller(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1)))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f2930])).
% 0.41/0.94 fof(f2932,plain,(
% 0.41/0.94 ![X0,X1,X2]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|latt_set_smaller(X0,X1,X2)|~relstr_element_smaller(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1)))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f2930])).
% 0.41/0.94 fof(f2943,plain,(
% 0.41/0.94 (?[A,B]: (((~empty_carrier(B)&lattice(B))&latt_str(B))&(?[C]: (element(C,the_carrier(poset_of_lattice(B)))&(relstr_element_smaller(poset_of_lattice(B),A,C)<~>latt_set_smaller(B,cast_to_el_of_lattice(B,C),A))))))),
% 0.41/0.94 inference(pre_NNF_transformation,[status(thm)],[f523])).
% 0.41/0.94 fof(f2944,plain,(
% 0.41/0.94 ?[A,B]: (((~empty_carrier(B)&lattice(B))&latt_str(B))&(?[C]: (element(C,the_carrier(poset_of_lattice(B)))&((relstr_element_smaller(poset_of_lattice(B),A,C)|latt_set_smaller(B,cast_to_el_of_lattice(B,C),A))&(~relstr_element_smaller(poset_of_lattice(B),A,C)|~latt_set_smaller(B,cast_to_el_of_lattice(B,C),A))))))),
% 0.41/0.94 inference(NNF_transformation,[status(thm)],[f2943])).
% 0.41/0.94 fof(f2945,plain,(
% 0.41/0.94 ?[B]: (((~empty_carrier(B)&lattice(B))&latt_str(B))&(?[C]: (element(C,the_carrier(poset_of_lattice(B)))&(?[A]: ((relstr_element_smaller(poset_of_lattice(B),A,C)|latt_set_smaller(B,cast_to_el_of_lattice(B,C),A))&(~relstr_element_smaller(poset_of_lattice(B),A,C)|~latt_set_smaller(B,cast_to_el_of_lattice(B,C),A)))))))),
% 0.41/0.94 inference(miniscoping,[status(thm)],[f2944])).
% 0.41/0.94 fof(f2946,plain,(
% 0.41/0.94 (((~empty_carrier(sK359_skl)&lattice(sK359_skl))&latt_str(sK359_skl))&(element(sK360_skl,the_carrier(poset_of_lattice(sK359_skl)))&((relstr_element_smaller(poset_of_lattice(sK359_skl),sK361_skl,sK360_skl)|latt_set_smaller(sK359_skl,cast_to_el_of_lattice(sK359_skl,sK360_skl),sK361_skl))&(~relstr_element_smaller(poset_of_lattice(sK359_skl),sK361_skl,sK360_skl)|~latt_set_smaller(sK359_skl,cast_to_el_of_lattice(sK359_skl,sK360_skl),sK361_skl)))))),
% 0.41/0.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK359_skl,sK360_skl,sK361_skl]),skolemize(B,sK359_skl),skolemize(C,sK360_skl),skolemize(A,sK361_skl)],[f2945])).
% 0.41/0.94 fof(f2947,plain,(
% 0.41/0.94 ~empty_carrier(sK359_skl)),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f2946])).
% 0.41/0.94 fof(f2948,plain,(
% 0.41/0.94 lattice(sK359_skl)),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f2946])).
% 0.41/0.94 fof(f2949,plain,(
% 0.41/0.94 latt_str(sK359_skl)),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f2946])).
% 0.41/0.94 fof(f2950,plain,(
% 0.41/0.94 element(sK360_skl,the_carrier(poset_of_lattice(sK359_skl)))),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f2946])).
% 0.41/0.94 fof(f2951,plain,(
% 0.41/0.94 relstr_element_smaller(poset_of_lattice(sK359_skl),sK361_skl,sK360_skl)|latt_set_smaller(sK359_skl,cast_to_el_of_lattice(sK359_skl,sK360_skl),sK361_skl)),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f2946])).
% 0.41/0.94 fof(f2952,plain,(
% 0.41/0.94 ~relstr_element_smaller(poset_of_lattice(sK359_skl),sK361_skl,sK360_skl)|~latt_set_smaller(sK359_skl,cast_to_el_of_lattice(sK359_skl,sK360_skl),sK361_skl)),
% 0.41/0.94 inference(cnf_transformation,[status(thm)],[f2946])).
% 0.41/0.94 fof(f3993,definition,(
% 0.41/0.94 sQ31_spl <=> (relstr_element_smaller(poset_of_lattice(sK359_skl),sK361_skl,sK360_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f3994,plain,(
% 0.41/0.94 relstr_element_smaller(poset_of_lattice(sK359_skl),sK361_skl,sK360_skl)|~sQ31_spl),
% 0.41/0.94 inference(component_clause,[status(thm)],[f3993])).
% 0.41/0.94 fof(f3996,definition,(
% 0.41/0.94 sQ32_spl <=> (latt_set_smaller(sK359_skl,cast_to_el_of_lattice(sK359_skl,sK360_skl),sK361_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f3997,plain,(
% 0.41/0.94 latt_set_smaller(sK359_skl,cast_to_el_of_lattice(sK359_skl,sK360_skl),sK361_skl)|~sQ32_spl),
% 0.41/0.94 inference(component_clause,[status(thm)],[f3996])).
% 0.41/0.94 fof(f3998,plain,(
% 0.41/0.94 ~latt_set_smaller(sK359_skl,cast_to_el_of_lattice(sK359_skl,sK360_skl),sK361_skl)|sQ32_spl),
% 0.41/0.94 inference(component_clause,[status(thm)],[f3996])).
% 0.41/0.94 fof(f3999,plain,(
% 0.41/0.94 sQ31_spl|sQ32_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f2951,f3993,f3996])).
% 0.41/0.94 fof(f4000,plain,(
% 0.41/0.94 ~sQ31_spl|~sQ32_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f2952,f3993,f3996])).
% 0.41/0.94 fof(f4198,plain,(
% 0.41/0.94 ![X0,X1]: (in(X0,unordered_pair(X0,X1)))),
% 0.41/0.94 inference(destructive_equality_resolution,[status(thm)],[f1102])).
% 0.41/0.94 fof(f4199,plain,(
% 0.41/0.94 ![X0,X1]: (in(X0,unordered_pair(X1,X0)))),
% 0.41/0.94 inference(destructive_equality_resolution,[status(thm)],[f1103])).
% 0.41/0.94 fof(f4449,plain,(
% 0.41/0.94 empty_carrier(sK359_skl)|~lattice(sK359_skl)|join_associative(sK359_skl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f2949,f700])).
% 0.41/0.94 fof(f4450,plain,(
% 0.41/0.94 empty_carrier(sK359_skl)|~lattice(sK359_skl)|join_commutative(sK359_skl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f2949,f699])).
% 0.41/0.94 fof(f4451,plain,(
% 0.41/0.94 empty_carrier(sK359_skl)|~lattice(sK359_skl)|rel_str(poset_of_lattice(sK359_skl))),
% 0.41/0.94 inference(resolution,[status(thm)],[f2949,f1486])).
% 0.41/0.94 fof(f4452,plain,(
% 0.41/0.94 ![X0]: (empty_carrier(sK359_skl)|~lattice(sK359_skl)|~element(X0,the_carrier(poset_of_lattice(sK359_skl)))|cast_to_el_of_lattice(sK359_skl,X0)=X0)),
% 0.41/0.94 inference(resolution,[status(thm)],[f2949,f1208])).
% 0.41/0.94 fof(f4453,plain,(
% 0.41/0.94 ![X0,X1,X2]: (empty_carrier(sK359_skl)|~element(X0,the_carrier(sK359_skl))|~latt_set_smaller(sK359_skl,X0,X1)|~element(X2,the_carrier(sK359_skl))|~in(X2,X1)|below(sK359_skl,X0,X2))),
% 0.41/0.94 inference(resolution,[status(thm)],[f2949,f874])).
% 0.41/0.94 fof(f4461,definition,(
% 0.41/0.94 sQ65_spl <=> (empty_carrier(sK359_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4462,plain,(
% 0.41/0.94 empty_carrier(sK359_skl)|~sQ65_spl),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4461])).
% 0.41/0.94 fof(f4464,definition,(
% 0.41/0.94 sQ66_spl <=> (lattice(sK359_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4466,plain,(
% 0.41/0.94 ~lattice(sK359_skl)|sQ66_spl),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4464])).
% 0.41/0.94 fof(f4467,definition,(
% 0.41/0.94 sQ67_spl <=> (join_associative(sK359_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4470,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ67_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4449,f4461,f4464,f4467])).
% 0.41/0.94 fof(f4471,definition,(
% 0.41/0.94 sQ68_spl <=> (join_commutative(sK359_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4474,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ68_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4450,f4461,f4464,f4471])).
% 0.41/0.94 fof(f4475,definition,(
% 0.41/0.94 sQ69_spl <=> (rel_str(poset_of_lattice(sK359_skl)))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4478,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ69_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4451,f4461,f4464,f4475])).
% 0.41/0.94 fof(f4479,definition,(
% 0.41/0.94 ![X0]: (sQ70_spl <=> (~element(X0,the_carrier(poset_of_lattice(sK359_skl)))|cast_to_el_of_lattice(sK359_skl,X0)=X0))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4480,plain,(
% 0.41/0.94 ![X0]: (~element(X0,the_carrier(poset_of_lattice(sK359_skl)))|cast_to_el_of_lattice(sK359_skl,X0)=X0|~sQ70_spl)),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4479])).
% 0.41/0.94 fof(f4482,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ70_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4452,f4461,f4464,f4479])).
% 0.41/0.94 fof(f4483,definition,(
% 0.41/0.94 ![X0,X1,X2]: (sQ71_spl <=> (~element(X0,the_carrier(sK359_skl))|~latt_set_smaller(sK359_skl,X0,X1)|~element(X2,the_carrier(sK359_skl))|~in(X2,X1)|below(sK359_skl,X0,X2)))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4484,plain,(
% 0.41/0.94 ![X0,X1,X2]: (~element(X0,the_carrier(sK359_skl))|~latt_set_smaller(sK359_skl,X0,X1)|~element(X2,the_carrier(sK359_skl))|~in(X2,X1)|below(sK359_skl,X0,X2)|~sQ71_spl)),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4483])).
% 0.41/0.94 fof(f4486,plain,(
% 0.41/0.94 sQ65_spl|sQ71_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4453,f4461,f4483])).
% 0.41/0.94 fof(f4487,plain,(
% 0.41/0.94 $false|~sQ65_spl),
% 0.41/0.94 inference(forward_subsumption_resolution,[status(thm)],[f4462,f2947])).
% 0.41/0.94 fof(f4488,plain,(
% 0.41/0.94 ~sQ65_spl),
% 0.41/0.94 inference(contradiction_clause,[status(thm)],[f4487])).
% 0.41/0.94 fof(f4489,plain,(
% 0.41/0.94 $false|sQ66_spl),
% 0.41/0.94 inference(forward_subsumption_resolution,[status(thm)],[f4466,f2948])).
% 0.41/0.94 fof(f4490,plain,(
% 0.41/0.94 sQ66_spl),
% 0.41/0.94 inference(contradiction_clause,[status(thm)],[f4489])).
% 0.41/0.94 fof(f4491,plain,(
% 0.41/0.94 empty_carrier(sK359_skl)|~lattice(sK359_skl)|meet_commutative(sK359_skl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f701,f2949])).
% 0.41/0.94 fof(f4492,definition,(
% 0.41/0.94 sQ72_spl <=> (meet_commutative(sK359_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4495,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ72_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4491,f4461,f4464,f4492])).
% 0.41/0.94 fof(f4496,plain,(
% 0.41/0.94 empty_carrier(sK359_skl)|~lattice(sK359_skl)|meet_associative(sK359_skl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f702,f2949])).
% 0.41/0.94 fof(f4497,definition,(
% 0.41/0.94 sQ73_spl <=> (meet_associative(sK359_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4500,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ73_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4496,f4461,f4464,f4497])).
% 0.41/0.94 fof(f4501,plain,(
% 0.41/0.94 empty_carrier(sK359_skl)|~lattice(sK359_skl)|meet_absorbing(sK359_skl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f703,f2949])).
% 0.41/0.94 fof(f4502,definition,(
% 0.41/0.94 sQ74_spl <=> (meet_absorbing(sK359_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4505,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ74_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4501,f4461,f4464,f4502])).
% 0.41/0.94 fof(f4506,plain,(
% 0.41/0.94 ![X0,X1]: (empty_carrier(sK359_skl)|~lattice(sK359_skl)|~element(X0,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,X0,X1)|~relstr_element_smaller(poset_of_lattice(sK359_skl),X1,cast_to_el_of_LattPOSet(sK359_skl,X0)))),
% 0.41/0.94 inference(resolution,[status(thm)],[f2932,f2949])).
% 0.41/0.94 fof(f4507,definition,(
% 0.41/0.94 ![X0,X1]: (sQ75_spl <=> (~element(X0,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,X0,X1)|~relstr_element_smaller(poset_of_lattice(sK359_skl),X1,cast_to_el_of_LattPOSet(sK359_skl,X0))))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4508,plain,(
% 0.41/0.94 ![X0,X1]: (~element(X0,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,X0,X1)|~relstr_element_smaller(poset_of_lattice(sK359_skl),X1,cast_to_el_of_LattPOSet(sK359_skl,X0))|~sQ75_spl)),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4507])).
% 0.41/0.94 fof(f4510,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ75_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4506,f4461,f4464,f4507])).
% 0.41/0.94 fof(f4511,plain,(
% 0.41/0.94 empty_carrier(sK359_skl)|~lattice(sK359_skl)|join_absorbing(sK359_skl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f704,f2949])).
% 0.41/0.94 fof(f4512,definition,(
% 0.41/0.94 sQ76_spl <=> (join_absorbing(sK359_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4515,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ76_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4511,f4461,f4464,f4512])).
% 0.41/0.94 fof(f4526,plain,(
% 0.41/0.94 cast_to_el_of_lattice(sK359_skl,sK360_skl)=sK360_skl|~sQ70_spl),
% 0.41/0.94 inference(resolution,[status(thm)],[f4480,f2950])).
% 0.41/0.94 fof(f4545,plain,(
% 0.41/0.94 ~latt_set_smaller(sK359_skl,sK360_skl,sK361_skl)|~sQ70_spl|sQ32_spl),
% 0.41/0.94 inference(backward_demodulation,[status(thm)],[f4526,f3998])).
% 0.41/0.94 fof(f4546,plain,(
% 0.41/0.94 empty_carrier(sK359_skl)|~lattice(sK359_skl)|~latt_str(sK359_skl)|~element(sK360_skl,the_carrier(poset_of_lattice(sK359_skl)))|element(sK360_skl,the_carrier(sK359_skl))|~sQ70_spl),
% 0.41/0.94 inference(paramodulation,[status(thm)],[f4526,f1502])).
% 0.41/0.94 fof(f4547,definition,(
% 0.41/0.94 sQ84_spl <=> (latt_str(sK359_skl))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4549,plain,(
% 0.41/0.94 ~latt_str(sK359_skl)|sQ84_spl),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4547])).
% 0.41/0.94 fof(f4550,definition,(
% 0.41/0.94 sQ85_spl <=> (element(sK360_skl,the_carrier(poset_of_lattice(sK359_skl))))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4552,plain,(
% 0.41/0.94 ~element(sK360_skl,the_carrier(poset_of_lattice(sK359_skl)))|sQ85_spl),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4550])).
% 0.41/0.94 fof(f4553,definition,(
% 0.41/0.94 sQ86_spl <=> (element(sK360_skl,the_carrier(sK359_skl)))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4554,plain,(
% 0.41/0.94 element(sK360_skl,the_carrier(sK359_skl))|~sQ86_spl),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4553])).
% 0.41/0.94 fof(f4556,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|~sQ84_spl|~sQ85_spl|sQ86_spl|~sQ70_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4546,f4461,f4464,f4547,f4550,f4553,f4479])).
% 0.41/0.94 fof(f4557,plain,(
% 0.41/0.94 ![X0,X1]: (~element(X0,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,X0,X1)|empty_carrier(sK359_skl)|~lattice(sK359_skl)|~latt_str(sK359_skl)|~element(X0,the_carrier(sK359_skl))|~latt_set_smaller(sK359_skl,X0,X1)|~sQ75_spl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f4508,f2931])).
% 0.41/0.94 fof(f4558,definition,(
% 0.41/0.94 ![X0,X1]: (sQ87_spl <=> (~element(X0,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,X0,X1)|~element(X0,the_carrier(sK359_skl))|~latt_set_smaller(sK359_skl,X0,X1)))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4561,plain,(
% 0.41/0.94 sQ87_spl|sQ65_spl|~sQ66_spl|~sQ84_spl|~sQ75_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4557,f4558,f4461,f4464,f4547,f4507])).
% 0.41/0.94 fof(f4562,plain,(
% 0.41/0.94 $false|sQ84_spl),
% 0.41/0.94 inference(forward_subsumption_resolution,[status(thm)],[f4549,f2949])).
% 0.41/0.94 fof(f4563,plain,(
% 0.41/0.94 sQ84_spl),
% 0.41/0.94 inference(contradiction_clause,[status(thm)],[f4562])).
% 0.41/0.94 fof(f4564,plain,(
% 0.41/0.94 $false|sQ85_spl),
% 0.41/0.94 inference(forward_subsumption_resolution,[status(thm)],[f4552,f2950])).
% 0.41/0.94 fof(f4565,plain,(
% 0.41/0.94 sQ85_spl),
% 0.41/0.94 inference(contradiction_clause,[status(thm)],[f4564])).
% 0.41/0.94 fof(f4566,plain,(
% 0.41/0.94 empty_carrier(sK359_skl)|~lattice(sK359_skl)|poset_of_lattice(sK359_skl)=rel_str_of(the_carrier(sK359_skl),k2_lattice3(sK359_skl))),
% 0.41/0.94 inference(resolution,[status(thm)],[f1064,f2949])).
% 0.41/0.94 fof(f4567,definition,(
% 0.41/0.94 sQ88_spl <=> (poset_of_lattice(sK359_skl)=rel_str_of(the_carrier(sK359_skl),k2_lattice3(sK359_skl)))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4570,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ88_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4566,f4461,f4464,f4567])).
% 0.41/0.94 fof(f4571,plain,(
% 0.41/0.94 ![X0,X1,X2]: (~element(X0,the_carrier(sK359_skl))|~latt_set_smaller(sK359_skl,X0,unordered_pair(X1,X2))|~element(X1,the_carrier(sK359_skl))|below(sK359_skl,X0,X1)|~sQ71_spl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f4198,f4484])).
% 0.41/0.94 fof(f4574,plain,(
% 0.41/0.94 ![X0,X1,X2]: (~element(X0,the_carrier(sK359_skl))|~latt_set_smaller(sK359_skl,X0,unordered_pair(X1,X2))|~element(X2,the_carrier(sK359_skl))|below(sK359_skl,X0,X2)|~sQ71_spl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f4199,f4484])).
% 0.41/0.94 fof(f4581,plain,(
% 0.41/0.94 ![X0]: (empty_carrier(sK359_skl)|~lattice(sK359_skl)|~element(X0,the_carrier(sK359_skl))|cast_to_el_of_LattPOSet(sK359_skl,X0)=X0)),
% 0.41/0.94 inference(resolution,[status(thm)],[f1152,f2949])).
% 0.41/0.94 fof(f4582,definition,(
% 0.41/0.94 ![X0]: (sQ89_spl <=> (~element(X0,the_carrier(sK359_skl))|cast_to_el_of_LattPOSet(sK359_skl,X0)=X0))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4583,plain,(
% 0.41/0.94 ![X0]: (~element(X0,the_carrier(sK359_skl))|cast_to_el_of_LattPOSet(sK359_skl,X0)=X0|~sQ89_spl)),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4582])).
% 0.41/0.94 fof(f4585,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|sQ89_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4581,f4461,f4464,f4582])).
% 0.41/0.94 fof(f4586,plain,(
% 0.41/0.94 ![X0,X1]: (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(X0,X1,sK359_skl))=sK21_skl(X0,X1,sK359_skl)|empty_carrier(sK359_skl)|~latt_str(sK359_skl)|~element(X1,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,X1,X0)|~sQ89_spl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f4583,f875])).
% 0.41/0.94 fof(f4587,plain,(
% 0.41/0.94 ![X0]: (cast_to_el_of_LattPOSet(sK359_skl,cast_to_el_of_lattice(sK359_skl,X0))=cast_to_el_of_lattice(sK359_skl,X0)|empty_carrier(sK359_skl)|~lattice(sK359_skl)|~latt_str(sK359_skl)|~element(X0,the_carrier(poset_of_lattice(sK359_skl)))|~sQ89_spl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f4583,f1502])).
% 0.41/0.94 fof(f4588,plain,(
% 0.41/0.94 cast_to_el_of_LattPOSet(sK359_skl,sK360_skl)=sK360_skl|~sQ89_spl|~sQ86_spl),
% 0.41/0.94 inference(resolution,[status(thm)],[f4583,f4554])).
% 0.41/0.94 fof(f4589,definition,(
% 0.41/0.94 ![X0,X1]: (sQ90_spl <=> (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(X0,X1,sK359_skl))=sK21_skl(X0,X1,sK359_skl)|~element(X1,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,X1,X0)))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4590,plain,(
% 0.41/0.94 ![X0,X1]: (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(X0,X1,sK359_skl))=sK21_skl(X0,X1,sK359_skl)|~element(X1,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,X1,X0)|~sQ90_spl)),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4589])).
% 0.41/0.94 fof(f4592,plain,(
% 0.41/0.94 sQ90_spl|sQ65_spl|~sQ84_spl|~sQ89_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4586,f4589,f4461,f4547,f4582])).
% 0.41/0.94 fof(f4593,definition,(
% 0.41/0.94 ![X0]: (sQ91_spl <=> (cast_to_el_of_LattPOSet(sK359_skl,cast_to_el_of_lattice(sK359_skl,X0))=cast_to_el_of_lattice(sK359_skl,X0)|~element(X0,the_carrier(poset_of_lattice(sK359_skl)))))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4596,plain,(
% 0.41/0.94 sQ91_spl|sQ65_spl|~sQ66_spl|~sQ84_spl|~sQ89_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4587,f4593,f4461,f4464,f4547,f4582])).
% 0.41/0.94 fof(f4597,plain,(
% 0.41/0.94 ![X0]: (~element(sK360_skl,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,sK360_skl,X0)|~relstr_element_smaller(poset_of_lattice(sK359_skl),X0,sK360_skl)|~sQ75_spl|~sQ89_spl|~sQ86_spl)),
% 0.41/0.94 inference(paramodulation,[status(thm)],[f4588,f4508])).
% 0.41/0.94 fof(f4598,plain,(
% 0.41/0.94 ![X0]: (empty_carrier(sK359_skl)|~lattice(sK359_skl)|~latt_str(sK359_skl)|~element(sK360_skl,the_carrier(sK359_skl))|~latt_set_smaller(sK359_skl,sK360_skl,X0)|relstr_element_smaller(poset_of_lattice(sK359_skl),X0,sK360_skl)|~sQ89_spl|~sQ86_spl)),
% 0.41/0.94 inference(paramodulation,[status(thm)],[f4588,f2931])).
% 0.41/0.94 fof(f4599,definition,(
% 0.41/0.94 ![X0]: (sQ92_spl <=> (latt_set_smaller(sK359_skl,sK360_skl,X0)|~relstr_element_smaller(poset_of_lattice(sK359_skl),X0,sK360_skl)))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4600,plain,(
% 0.41/0.94 ![X0]: (latt_set_smaller(sK359_skl,sK360_skl,X0)|~relstr_element_smaller(poset_of_lattice(sK359_skl),X0,sK360_skl)|~sQ92_spl)),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4599])).
% 0.41/0.94 fof(f4602,plain,(
% 0.41/0.94 ~sQ86_spl|sQ92_spl|~sQ75_spl|~sQ89_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4597,f4553,f4599,f4507,f4582])).
% 0.41/0.94 fof(f4603,definition,(
% 0.41/0.94 ![X0]: (sQ93_spl <=> (~latt_set_smaller(sK359_skl,sK360_skl,X0)|relstr_element_smaller(poset_of_lattice(sK359_skl),X0,sK360_skl)))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4604,plain,(
% 0.41/0.94 ![X0]: (~latt_set_smaller(sK359_skl,sK360_skl,X0)|relstr_element_smaller(poset_of_lattice(sK359_skl),X0,sK360_skl)|~sQ93_spl)),
% 0.41/0.94 inference(component_clause,[status(thm)],[f4603])).
% 0.41/0.94 fof(f4606,plain,(
% 0.41/0.94 sQ65_spl|~sQ66_spl|~sQ84_spl|~sQ86_spl|sQ93_spl|~sQ89_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4598,f4461,f4464,f4547,f4553,f4603,f4582])).
% 0.41/0.94 fof(f4608,plain,(
% 0.41/0.94 ![X0,X1,X2]: (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(X0,sK21_skl(X1,X2,sK359_skl),sK359_skl))=sK21_skl(X0,sK21_skl(X1,X2,sK359_skl),sK359_skl)|latt_set_smaller(sK359_skl,sK21_skl(X1,X2,sK359_skl),X0)|empty_carrier(sK359_skl)|~latt_str(sK359_skl)|~element(X2,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,X2,X1)|~sQ90_spl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f4590,f875])).
% 0.41/0.94 fof(f4609,plain,(
% 0.41/0.94 ![X0,X1]: (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(X0,cast_to_el_of_lattice(sK359_skl,X1),sK359_skl))=sK21_skl(X0,cast_to_el_of_lattice(sK359_skl,X1),sK359_skl)|latt_set_smaller(sK359_skl,cast_to_el_of_lattice(sK359_skl,X1),X0)|empty_carrier(sK359_skl)|~lattice(sK359_skl)|~latt_str(sK359_skl)|~element(X1,the_carrier(poset_of_lattice(sK359_skl)))|~sQ90_spl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f4590,f1502])).
% 0.41/0.94 fof(f4610,plain,(
% 0.41/0.94 ![X0]: (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(X0,sK360_skl,sK359_skl))=sK21_skl(X0,sK360_skl,sK359_skl)|latt_set_smaller(sK359_skl,sK360_skl,X0)|~sQ90_spl|~sQ86_spl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f4590,f4554])).
% 0.41/0.94 fof(f4611,definition,(
% 0.41/0.94 ![X0,X1,X2]: (sQ94_spl <=> (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(X0,sK21_skl(X1,X2,sK359_skl),sK359_skl))=sK21_skl(X0,sK21_skl(X1,X2,sK359_skl),sK359_skl)|latt_set_smaller(sK359_skl,sK21_skl(X1,X2,sK359_skl),X0)|~element(X2,the_carrier(sK359_skl))|latt_set_smaller(sK359_skl,X2,X1)))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4614,plain,(
% 0.41/0.94 sQ94_spl|sQ65_spl|~sQ84_spl|~sQ90_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4608,f4611,f4461,f4547,f4589])).
% 0.41/0.94 fof(f4615,definition,(
% 0.41/0.94 ![X0,X1]: (sQ95_spl <=> (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(X0,cast_to_el_of_lattice(sK359_skl,X1),sK359_skl))=sK21_skl(X0,cast_to_el_of_lattice(sK359_skl,X1),sK359_skl)|latt_set_smaller(sK359_skl,cast_to_el_of_lattice(sK359_skl,X1),X0)|~element(X1,the_carrier(poset_of_lattice(sK359_skl)))))),
% 0.41/0.94 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.41/0.94 fof(f4618,plain,(
% 0.41/0.94 sQ95_spl|sQ65_spl|~sQ66_spl|~sQ84_spl|~sQ90_spl),
% 0.41/0.94 inference(split_clause,[status(thm)],[f4609,f4615,f4461,f4464,f4547,f4589])).
% 0.41/0.94 fof(f4633,plain,(
% 0.41/0.94 ![X0,X1]: (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(unordered_pair(X0,X1),sK360_skl,sK359_skl))=sK21_skl(unordered_pair(X0,X1),sK360_skl,sK359_skl)|~element(sK360_skl,the_carrier(sK359_skl))|~element(X1,the_carrier(sK359_skl))|below(sK359_skl,sK360_skl,X1)|~sQ90_spl|~sQ86_spl|~sQ71_spl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f4610,f4574])).
% 0.41/0.94 fof(f4634,plain,(
% 0.41/0.94 ![X0,X1]: (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(unordered_pair(X0,X1),sK360_skl,sK359_skl))=sK21_skl(unordered_pair(X0,X1),sK360_skl,sK359_skl)|~element(sK360_skl,the_carrier(sK359_skl))|~element(X0,the_carrier(sK359_skl))|below(sK359_skl,sK360_skl,X0)|~sQ90_spl|~sQ86_spl|~sQ71_spl)),
% 0.41/0.94 inference(resolution,[status(thm)],[f4610,f4571])).
% 0.41/0.94 fof(f4635,definition,(
% 0.41/0.94 ![X0,X1]: (sQ98_spl <=> (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(unordered_pair(X0,X1),sK360_skl,sK359_skl))=sK21_skl(unordered_pair(X0,X1),sK360_skl,sK359_skl)|~element(X1,the_carrier(sK359_skl))|below(sK359_skl,sK360_skl,X1)))),
% 0.41/0.95 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.41/0.95 fof(f4638,plain,(
% 0.41/0.95 sQ98_spl|~sQ86_spl|~sQ90_spl|~sQ71_spl),
% 0.41/0.95 inference(split_clause,[status(thm)],[f4633,f4635,f4553,f4589,f4483])).
% 0.41/0.95 fof(f4639,definition,(
% 0.41/0.95 ![X0,X1]: (sQ99_spl <=> (cast_to_el_of_LattPOSet(sK359_skl,sK21_skl(unordered_pair(X0,X1),sK360_skl,sK359_skl))=sK21_skl(unordered_pair(X0,X1),sK360_skl,sK359_skl)|~element(X0,the_carrier(sK359_skl))|below(sK359_skl,sK360_skl,X0)))),
% 0.41/0.95 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.41/0.95 fof(f4642,plain,(
% 0.41/0.95 sQ99_spl|~sQ86_spl|~sQ90_spl|~sQ71_spl),
% 0.41/0.95 inference(split_clause,[status(thm)],[f4634,f4639,f4553,f4589,f4483])).
% 0.41/0.95 fof(f4656,plain,(
% 0.41/0.95 latt_set_smaller(sK359_skl,sK360_skl,sK361_skl)|~sQ70_spl|~sQ32_spl),
% 0.41/0.95 inference(forward_demodulation,[status(thm)],[f4526,f3997])).
% 0.41/0.95 fof(f4660,plain,(
% 0.41/0.95 relstr_element_smaller(poset_of_lattice(sK359_skl),sK361_skl,sK360_skl)|~sQ93_spl|~sQ70_spl|~sQ32_spl),
% 0.41/0.95 inference(resolution,[status(thm)],[f4604,f4656])).
% 0.41/0.95 fof(f4662,plain,(
% 0.41/0.95 sQ31_spl|~sQ93_spl|~sQ70_spl|~sQ32_spl),
% 0.41/0.95 inference(split_clause,[status(thm)],[f4660,f3993,f4603,f4479,f3996])).
% 0.41/0.95 fof(f4664,plain,(
% 0.41/0.95 latt_set_smaller(sK359_skl,sK360_skl,sK361_skl)|~sQ31_spl|~sQ92_spl),
% 0.41/0.95 inference(resolution,[status(thm)],[f3994,f4600])).
% 0.41/0.95 fof(f4672,plain,(
% 0.41/0.95 $false|~sQ70_spl|sQ32_spl|~sQ31_spl|~sQ92_spl),
% 0.41/0.95 inference(forward_subsumption_resolution,[status(thm)],[f4664,f4545])).
% 0.41/0.95 fof(f4673,plain,(
% 0.41/0.95 ~sQ70_spl|sQ32_spl|~sQ31_spl|~sQ92_spl),
% 0.41/0.95 inference(contradiction_clause,[status(thm)],[f4672])).
% 0.41/0.95 fof(f4674,plain,(
% 0.41/0.95 $false),
% 0.41/0.95 inference(sat_refutation,[status(thm)],[f3999,f4000,f4470,f4474,f4478,f4482,f4486,f4488,f4490,f4495,f4500,f4505,f4510,f4515,f4556,f4561,f4563,f4565,f4570,f4585,f4592,f4596,f4602,f4606,f4614,f4618,f4638,f4642,f4662,f4673])).
% 0.41/0.95 % SZS output end CNFRefutation for theBenchmark.p
% 0.43/1.03 % Elapsed time: 0.551918 seconds
% 0.43/1.03 % CPU time: 2.358456 seconds
% 0.43/1.03 % Total memory used: 211.273 MB
% 0.43/1.03 % Net memory used: 209.903 MB
%------------------------------------------------------------------------------