%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU350+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 : n015.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:24 PM UTC 2026
% Result : Theorem 5.21s 6.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU350+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.35 % Computer : n015.cluster.edu
% 0.09/5.35 % Model : x86_64 x86_64
% 0.09/5.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.35 % Memory : 8046.5625MB
% 0.09/5.35 % OS : Linux 6.8.0-71-generic
% 0.09/5.35 % CPULimit : 300
% 0.09/5.35 % WCLimit : 300
% 0.09/5.35 % DateTime : Mon Sep 21 06:17:56 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.13/5.44 % Drodi V4.1.1
% 5.21/6.14 % Refutation found
% 5.21/6.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.21/6.14 % SZS output start CNFRefutation for theBenchmark
% 5.21/6.14 fof(f1,axiom,(
% 5.21/6.14 (! [A] :( rel_str(A)=> ( strict_rel_str(A)=> A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f84,axiom,(
% 5.21/6.14 (! [A] :( ( ~ empty_carrier(A)& lattice(A)& latt_str(A) )=> poset_of_lattice(A) = rel_str_of(the_carrier(A),k2_lattice3(A)) ) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f91,axiom,(
% 5.21/6.14 (! [A,B,C] :( C = unordered_pair(A,B)<=> (! [D] :( in(D,C)<=> ( D = A| D = B ) ) )) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f97,axiom,(
% 5.21/6.14 (! [A] :( ( ~ empty_carrier(A)& lattice(A)& latt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> cast_to_el_of_LattPOSet(A,B) = B ) )) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f106,axiom,(
% 5.21/6.14 (! [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 ) )) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f142,axiom,(
% 5.21/6.14 (! [A] :( rel_str(A)=> (! [B,C] :( element(C,the_carrier(A))=> ( relstr_set_smaller(A,B,C)<=> (! [D] :( element(D,the_carrier(A))=> ( in(D,B)=> related(A,D,C) ) ) )) ) )) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f178,axiom,(
% 5.21/6.14 (! [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)) ) ) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f191,axiom,(
% 5.21/6.14 (! [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)) ) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f372,axiom,(
% 5.21/6.14 (? [A] :( latt_str(A)& ~ empty_carrier(A)& strict_latt_str(A)& join_commutative(A)& join_associative(A)& meet_commutative(A)& meet_associative(A)& meet_absorbing(A)& join_absorbing(A)& lattice(A) ) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f524,lemma,(
% 5.21/6.14 (! [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) ) ) )) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f532,lemma,(
% 5.21/6.14 (! [A,B] :( ( ~ empty_carrier(B)& lattice(B)& latt_str(B) )=> (! [C] :( element(C,the_carrier(B))=> ( latt_element_smaller(B,C,A)<=> relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C)) ) ) )) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f535,conjecture,(
% 5.21/6.14 (! [A,B] :( ( ~ empty_carrier(B)& lattice(B)& latt_str(B) )=> (! [C] :( element(C,the_carrier(poset_of_lattice(B)))=> ( relstr_set_smaller(poset_of_lattice(B),A,C)<=> latt_element_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) )) )),
% 5.21/6.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.14 fof(f536,negated_conjecture,(
% 5.21/6.14 ~((! [A,B] :( ( ~ empty_carrier(B)& lattice(B)& latt_str(B) )=> (! [C] :( element(C,the_carrier(poset_of_lattice(B)))=> ( relstr_set_smaller(poset_of_lattice(B),A,C)<=> latt_element_smaller(B,cast_to_el_of_lattice(B,C),A) ) ) )) ))),
% 5.21/6.14 inference(negated_conjecture,[status(cth)],[f535])).
% 5.21/6.14 fof(f642,plain,(
% 5.21/6.14 ![A]: (~rel_str(A)|(~strict_rel_str(A)|A=rel_str_of(the_carrier(A),the_InternalRel(A))))),
% 5.21/6.14 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 5.21/6.14 fof(f643,plain,(
% 5.21/6.14 ![X0]: (~rel_str(X0)|~strict_rel_str(X0)|X0=rel_str_of(the_carrier(X0),the_InternalRel(X0)))),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f642])).
% 5.21/6.14 fof(f1075,plain,(
% 5.21/6.14 ![A]: (((empty_carrier(A)|~lattice(A))|~latt_str(A))|poset_of_lattice(A)=rel_str_of(the_carrier(A),k2_lattice3(A)))),
% 5.21/6.14 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 5.21/6.14 fof(f1076,plain,(
% 5.21/6.14 ![X0]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|poset_of_lattice(X0)=rel_str_of(the_carrier(X0),k2_lattice3(X0)))),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f1075])).
% 5.21/6.14 fof(f1110,plain,(
% 5.21/6.14 ![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))))))),
% 5.21/6.14 inference(NNF_transformation,[status(thm)],[f91])).
% 5.21/6.14 fof(f1111,plain,(
% 5.21/6.14 (![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))))))),
% 5.21/6.14 inference(miniscoping,[status(thm)],[f1110])).
% 5.21/6.14 fof(f1112,plain,(
% 5.21/6.14 (![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(sK56_skl(C,B,A),C)|(~sK56_skl(C,B,A)=A&~sK56_skl(C,B,A)=B))&(in(sK56_skl(C,B,A),C)|(sK56_skl(C,B,A)=A|sK56_skl(C,B,A)=B)))))),
% 5.21/6.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK56_skl]),skolemize(D,sK56_skl(C,B,A))],[f1111])).
% 5.21/6.14 fof(f1114,plain,(
% 5.21/6.14 ![X0,X1,X2,X3]: (~X0=unordered_pair(X1,X2)|in(X3,X0)|~X3=X1)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f1112])).
% 5.21/6.14 fof(f1115,plain,(
% 5.21/6.14 ![X0,X1,X2,X3]: (~X0=unordered_pair(X1,X2)|in(X3,X0)|~X3=X2)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f1112])).
% 5.21/6.14 fof(f1163,plain,(
% 5.21/6.14 ![A]: (((empty_carrier(A)|~lattice(A))|~latt_str(A))|(![B]: (~element(B,the_carrier(A))|cast_to_el_of_LattPOSet(A,B)=B)))),
% 5.21/6.14 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 5.21/6.14 fof(f1164,plain,(
% 5.21/6.14 ![X0,X1]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|cast_to_el_of_LattPOSet(X0,X1)=X1)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f1163])).
% 5.21/6.14 fof(f1219,plain,(
% 5.21/6.14 ![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)))),
% 5.21/6.14 inference(pre_NNF_transformation,[status(thm)],[f106])).
% 5.21/6.14 fof(f1220,plain,(
% 5.21/6.14 ![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)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f1219])).
% 5.21/6.14 fof(f1446,plain,(
% 5.21/6.14 ![A]: (~rel_str(A)|(![B,C]: (~element(C,the_carrier(A))|(relstr_set_smaller(A,B,C)<=>(![D]: (~element(D,the_carrier(A))|(~in(D,B)|related(A,D,C))))))))),
% 5.21/6.14 inference(pre_NNF_transformation,[status(thm)],[f142])).
% 5.21/6.14 fof(f1447,plain,(
% 5.21/6.14 ![A]: (~rel_str(A)|(![B,C]: (~element(C,the_carrier(A))|((~relstr_set_smaller(A,B,C)|(![D]: (~element(D,the_carrier(A))|(~in(D,B)|related(A,D,C)))))&(relstr_set_smaller(A,B,C)|(?[D]: (element(D,the_carrier(A))&(in(D,B)&~related(A,D,C)))))))))),
% 5.21/6.14 inference(NNF_transformation,[status(thm)],[f1446])).
% 5.21/6.14 fof(f1448,plain,(
% 5.21/6.14 ![A]: (~rel_str(A)|(![C]: (~element(C,the_carrier(A))|((![B]: (~relstr_set_smaller(A,B,C)|(![D]: (~element(D,the_carrier(A))|(~in(D,B)|related(A,D,C))))))&(![B]: (relstr_set_smaller(A,B,C)|(?[D]: (element(D,the_carrier(A))&(in(D,B)&~related(A,D,C))))))))))),
% 5.21/6.14 inference(miniscoping,[status(thm)],[f1447])).
% 5.21/6.14 fof(f1449,plain,(
% 5.21/6.14 ![A]: (~rel_str(A)|(![C]: (~element(C,the_carrier(A))|((![B]: (~relstr_set_smaller(A,B,C)|(![D]: (~element(D,the_carrier(A))|(~in(D,B)|related(A,D,C))))))&(![B]: (relstr_set_smaller(A,B,C)|(element(sK112_skl(B,C,A),the_carrier(A))&(in(sK112_skl(B,C,A),B)&~related(A,sK112_skl(B,C,A),C)))))))))),
% 5.21/6.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK112_skl]),skolemize(D,sK112_skl(B,C,A))],[f1448])).
% 5.21/6.14 fof(f1450,plain,(
% 5.21/6.14 ![X0,X1,X2,X3]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~relstr_set_smaller(X0,X2,X1)|~element(X3,the_carrier(X0))|~in(X3,X2)|related(X0,X3,X1))),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f1449])).
% 5.21/6.14 fof(f1501,plain,(
% 5.21/6.14 ![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))))),
% 5.21/6.14 inference(pre_NNF_transformation,[status(thm)],[f178])).
% 5.21/6.14 fof(f1502,plain,(
% 5.21/6.14 ![X0]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|strict_rel_str(poset_of_lattice(X0)))),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f1501])).
% 5.21/6.14 fof(f1506,plain,(
% 5.21/6.14 ![X0]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|rel_str(poset_of_lattice(X0)))),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f1501])).
% 5.21/6.14 fof(f1521,plain,(
% 5.21/6.14 ![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)))),
% 5.21/6.14 inference(pre_NNF_transformation,[status(thm)],[f191])).
% 5.21/6.14 fof(f1522,plain,(
% 5.21/6.14 ![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)))),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f1521])).
% 5.21/6.14 fof(f2144,plain,(
% 5.21/6.14 (((((((((latt_str(sK169_skl)&~empty_carrier(sK169_skl))&strict_latt_str(sK169_skl))&join_commutative(sK169_skl))&join_associative(sK169_skl))&meet_commutative(sK169_skl))&meet_associative(sK169_skl))&meet_absorbing(sK169_skl))&join_absorbing(sK169_skl))&lattice(sK169_skl))),
% 5.21/6.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK169_skl]),skolemize(A,sK169_skl)],[f372])).
% 5.21/6.14 fof(f2145,plain,(
% 5.21/6.14 latt_str(sK169_skl)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f2144])).
% 5.21/6.14 fof(f2146,plain,(
% 5.21/6.14 ~empty_carrier(sK169_skl)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f2144])).
% 5.21/6.14 fof(f2154,plain,(
% 5.21/6.14 lattice(sK169_skl)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f2144])).
% 5.21/6.14 fof(f2963,plain,(
% 5.21/6.14 ![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)))))),
% 5.21/6.14 inference(pre_NNF_transformation,[status(thm)],[f524])).
% 5.21/6.14 fof(f2964,plain,(
% 5.21/6.14 ![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))))))),
% 5.21/6.14 inference(NNF_transformation,[status(thm)],[f2963])).
% 5.21/6.14 fof(f2965,plain,(
% 5.21/6.14 ![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)))&(![A]: (relstr_element_smaller(poset_of_lattice(B),A,C)|~latt_set_smaller(B,cast_to_el_of_lattice(B,C),A)))))))),
% 5.21/6.14 inference(miniscoping,[status(thm)],[f2964])).
% 5.21/6.14 fof(f2967,plain,(
% 5.21/6.14 ![X0,X1,X2]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(poset_of_lattice(X0)))|relstr_element_smaller(poset_of_lattice(X0),X2,X1)|~latt_set_smaller(X0,cast_to_el_of_lattice(X0,X1),X2))),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f2965])).
% 5.21/6.14 fof(f2986,plain,(
% 5.21/6.14 ![A,B]: (((empty_carrier(B)|~lattice(B))|~latt_str(B))|(![C]: (~element(C,the_carrier(B))|(latt_element_smaller(B,C,A)<=>relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))))))),
% 5.21/6.14 inference(pre_NNF_transformation,[status(thm)],[f532])).
% 5.21/6.14 fof(f2987,plain,(
% 5.21/6.14 ![A,B]: (((empty_carrier(B)|~lattice(B))|~latt_str(B))|(![C]: (~element(C,the_carrier(B))|((~latt_element_smaller(B,C,A)|relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C)))&(latt_element_smaller(B,C,A)|~relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C)))))))),
% 5.21/6.14 inference(NNF_transformation,[status(thm)],[f2986])).
% 5.21/6.14 fof(f2988,plain,(
% 5.21/6.14 ![B]: (((empty_carrier(B)|~lattice(B))|~latt_str(B))|(![C]: (~element(C,the_carrier(B))|((![A]: (~latt_element_smaller(B,C,A)|relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))))&(![A]: (latt_element_smaller(B,C,A)|~relstr_set_smaller(poset_of_lattice(B),A,cast_to_el_of_LattPOSet(B,C))))))))),
% 5.21/6.14 inference(miniscoping,[status(thm)],[f2987])).
% 5.21/6.14 fof(f2989,plain,(
% 5.21/6.14 ![X0,X1,X2]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|~latt_element_smaller(X0,X1,X2)|relstr_set_smaller(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1)))),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f2988])).
% 5.21/6.14 fof(f2990,plain,(
% 5.21/6.14 ![X0,X1,X2]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|latt_element_smaller(X0,X1,X2)|~relstr_set_smaller(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1)))),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f2988])).
% 5.21/6.14 fof(f2999,plain,(
% 5.21/6.14 (?[A,B]: (((~empty_carrier(B)&lattice(B))&latt_str(B))&(?[C]: (element(C,the_carrier(poset_of_lattice(B)))&(relstr_set_smaller(poset_of_lattice(B),A,C)<~>latt_element_smaller(B,cast_to_el_of_lattice(B,C),A))))))),
% 5.21/6.14 inference(pre_NNF_transformation,[status(thm)],[f536])).
% 5.21/6.14 fof(f3000,plain,(
% 5.21/6.14 ?[A,B]: (((~empty_carrier(B)&lattice(B))&latt_str(B))&(?[C]: (element(C,the_carrier(poset_of_lattice(B)))&((relstr_set_smaller(poset_of_lattice(B),A,C)|latt_element_smaller(B,cast_to_el_of_lattice(B,C),A))&(~relstr_set_smaller(poset_of_lattice(B),A,C)|~latt_element_smaller(B,cast_to_el_of_lattice(B,C),A))))))),
% 5.21/6.14 inference(NNF_transformation,[status(thm)],[f2999])).
% 5.21/6.14 fof(f3001,plain,(
% 5.21/6.14 ?[B]: (((~empty_carrier(B)&lattice(B))&latt_str(B))&(?[C]: (element(C,the_carrier(poset_of_lattice(B)))&(?[A]: ((relstr_set_smaller(poset_of_lattice(B),A,C)|latt_element_smaller(B,cast_to_el_of_lattice(B,C),A))&(~relstr_set_smaller(poset_of_lattice(B),A,C)|~latt_element_smaller(B,cast_to_el_of_lattice(B,C),A)))))))),
% 5.21/6.14 inference(miniscoping,[status(thm)],[f3000])).
% 5.21/6.14 fof(f3002,plain,(
% 5.21/6.14 (((~empty_carrier(sK362_skl)&lattice(sK362_skl))&latt_str(sK362_skl))&(element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl)))&((relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl)|latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl))&(~relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl)|~latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl)))))),
% 5.21/6.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK362_skl,sK363_skl,sK364_skl]),skolemize(B,sK362_skl),skolemize(C,sK363_skl),skolemize(A,sK364_skl)],[f3001])).
% 5.21/6.14 fof(f3003,plain,(
% 5.21/6.14 ~empty_carrier(sK362_skl)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f3002])).
% 5.21/6.14 fof(f3004,plain,(
% 5.21/6.14 lattice(sK362_skl)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f3002])).
% 5.21/6.14 fof(f3005,plain,(
% 5.21/6.14 latt_str(sK362_skl)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f3002])).
% 5.21/6.14 fof(f3006,plain,(
% 5.21/6.14 element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl)))),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f3002])).
% 5.21/6.14 fof(f3007,plain,(
% 5.21/6.14 relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl)|latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f3002])).
% 5.21/6.14 fof(f3008,plain,(
% 5.21/6.14 ~relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl)|~latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl)),
% 5.21/6.14 inference(cnf_transformation,[status(thm)],[f3002])).
% 5.21/6.14 fof(f4023,definition,(
% 5.21/6.14 sQ31_spl <=> (relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4024,plain,(
% 5.21/6.14 relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl)|~sQ31_spl),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4023])).
% 5.21/6.14 fof(f4026,definition,(
% 5.21/6.14 sQ32_spl <=> (latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4027,plain,(
% 5.21/6.14 latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl)|~sQ32_spl),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4026])).
% 5.21/6.14 fof(f4028,plain,(
% 5.21/6.14 ~latt_element_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,sK363_skl),sK364_skl)|sQ32_spl),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4026])).
% 5.21/6.14 fof(f4029,plain,(
% 5.21/6.14 sQ31_spl|sQ32_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f3007,f4023,f4026])).
% 5.21/6.14 fof(f4030,plain,(
% 5.21/6.14 ~sQ31_spl|~sQ32_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f3008,f4023,f4026])).
% 5.21/6.14 fof(f4228,plain,(
% 5.21/6.14 ![X0,X1]: (in(X0,unordered_pair(X0,X1)))),
% 5.21/6.14 inference(destructive_equality_resolution,[status(thm)],[f1114])).
% 5.21/6.14 fof(f4229,plain,(
% 5.21/6.14 ![X0,X1]: (in(X0,unordered_pair(X1,X0)))),
% 5.21/6.14 inference(destructive_equality_resolution,[status(thm)],[f1115])).
% 5.21/6.14 fof(f4478,plain,(
% 5.21/6.14 ![X0]: (empty_carrier(sK362_skl)|~latt_str(sK362_skl)|~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|cast_to_el_of_lattice(sK362_skl,X0)=X0)),
% 5.21/6.14 inference(resolution,[status(thm)],[f1220,f3004])).
% 5.21/6.14 fof(f4479,definition,(
% 5.21/6.14 sQ63_spl <=> (empty_carrier(sK362_skl))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4480,plain,(
% 5.21/6.14 empty_carrier(sK362_skl)|~sQ63_spl),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4479])).
% 5.21/6.14 fof(f4482,definition,(
% 5.21/6.14 sQ64_spl <=> (latt_str(sK362_skl))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4484,plain,(
% 5.21/6.14 ~latt_str(sK362_skl)|sQ64_spl),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4482])).
% 5.21/6.14 fof(f4485,definition,(
% 5.21/6.14 ![X0]: (sQ65_spl <=> (~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|cast_to_el_of_lattice(sK362_skl,X0)=X0))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4486,plain,(
% 5.21/6.14 ![X0]: (~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|cast_to_el_of_lattice(sK362_skl,X0)=X0|~sQ65_spl)),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4485])).
% 5.21/6.14 fof(f4488,plain,(
% 5.21/6.14 sQ63_spl|~sQ64_spl|sQ65_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f4478,f4479,f4482,f4485])).
% 5.21/6.14 fof(f4489,plain,(
% 5.21/6.14 cast_to_el_of_lattice(sK362_skl,sK363_skl)=sK363_skl|~sQ65_spl),
% 5.21/6.14 inference(resolution,[status(thm)],[f4486,f3006])).
% 5.21/6.14 fof(f4490,plain,(
% 5.21/6.14 ~latt_element_smaller(sK362_skl,sK363_skl,sK364_skl)|~sQ65_spl|sQ32_spl),
% 5.21/6.14 inference(backward_demodulation,[status(thm)],[f4489,f4028])).
% 5.21/6.14 fof(f4491,plain,(
% 5.21/6.14 ![X0]: (empty_carrier(sK362_skl)|~latt_str(sK362_skl)|~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|element(cast_to_el_of_lattice(sK362_skl,X0),the_carrier(sK362_skl)))),
% 5.21/6.14 inference(resolution,[status(thm)],[f1522,f3004])).
% 5.21/6.14 fof(f4492,definition,(
% 5.21/6.14 ![X0]: (sQ66_spl <=> (~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|element(cast_to_el_of_lattice(sK362_skl,X0),the_carrier(sK362_skl))))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4493,plain,(
% 5.21/6.14 ![X0]: (~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|element(cast_to_el_of_lattice(sK362_skl,X0),the_carrier(sK362_skl))|~sQ66_spl)),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4492])).
% 5.21/6.14 fof(f4495,plain,(
% 5.21/6.14 sQ63_spl|~sQ64_spl|sQ66_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f4491,f4479,f4482,f4492])).
% 5.21/6.14 fof(f4496,plain,(
% 5.21/6.14 $false|sQ64_spl),
% 5.21/6.14 inference(forward_subsumption_resolution,[status(thm)],[f4484,f3005])).
% 5.21/6.14 fof(f4497,plain,(
% 5.21/6.14 sQ64_spl),
% 5.21/6.14 inference(contradiction_clause,[status(thm)],[f4496])).
% 5.21/6.14 fof(f4498,plain,(
% 5.21/6.14 $false|~sQ63_spl),
% 5.21/6.14 inference(forward_subsumption_resolution,[status(thm)],[f4480,f3003])).
% 5.21/6.14 fof(f4499,plain,(
% 5.21/6.14 ~sQ63_spl),
% 5.21/6.14 inference(contradiction_clause,[status(thm)],[f4498])).
% 5.21/6.14 fof(f4501,plain,(
% 5.21/6.14 ![X0,X1]: (empty_carrier(sK362_skl)|~latt_str(sK362_skl)|~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|relstr_element_smaller(poset_of_lattice(sK362_skl),X1,X0)|~latt_set_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,X0),X1))),
% 5.21/6.14 inference(resolution,[status(thm)],[f2967,f3004])).
% 5.21/6.14 fof(f4502,definition,(
% 5.21/6.14 ![X0,X1]: (sQ67_spl <=> (~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|relstr_element_smaller(poset_of_lattice(sK362_skl),X1,X0)|~latt_set_smaller(sK362_skl,cast_to_el_of_lattice(sK362_skl,X0),X1)))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4505,plain,(
% 5.21/6.14 sQ63_spl|~sQ64_spl|sQ67_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f4501,f4479,f4482,f4502])).
% 5.21/6.14 fof(f4506,plain,(
% 5.21/6.14 ![X0,X1]: (empty_carrier(sK362_skl)|~latt_str(sK362_skl)|~element(X0,the_carrier(sK362_skl))|latt_element_smaller(sK362_skl,X0,X1)|~relstr_set_smaller(poset_of_lattice(sK362_skl),X1,cast_to_el_of_LattPOSet(sK362_skl,X0)))),
% 5.21/6.14 inference(resolution,[status(thm)],[f2990,f3004])).
% 5.21/6.14 fof(f4507,definition,(
% 5.21/6.14 ![X0,X1]: (sQ68_spl <=> (~element(X0,the_carrier(sK362_skl))|latt_element_smaller(sK362_skl,X0,X1)|~relstr_set_smaller(poset_of_lattice(sK362_skl),X1,cast_to_el_of_LattPOSet(sK362_skl,X0))))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4508,plain,(
% 5.21/6.14 ![X0,X1]: (~element(X0,the_carrier(sK362_skl))|latt_element_smaller(sK362_skl,X0,X1)|~relstr_set_smaller(poset_of_lattice(sK362_skl),X1,cast_to_el_of_LattPOSet(sK362_skl,X0))|~sQ68_spl)),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4507])).
% 5.21/6.14 fof(f4510,plain,(
% 5.21/6.14 sQ63_spl|~sQ64_spl|sQ68_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f4506,f4479,f4482,f4507])).
% 5.21/6.14 fof(f4512,plain,(
% 5.21/6.14 ~element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl)))|element(sK363_skl,the_carrier(sK362_skl))|~sQ66_spl|~sQ65_spl),
% 5.21/6.14 inference(paramodulation,[status(thm)],[f4489,f4493])).
% 5.21/6.14 fof(f4513,definition,(
% 5.21/6.14 sQ69_spl <=> (element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl))))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4515,plain,(
% 5.21/6.14 ~element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl)))|sQ69_spl),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4513])).
% 5.21/6.14 fof(f4516,definition,(
% 5.21/6.14 sQ70_spl <=> (element(sK363_skl,the_carrier(sK362_skl)))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4517,plain,(
% 5.21/6.14 element(sK363_skl,the_carrier(sK362_skl))|~sQ70_spl),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4516])).
% 5.21/6.14 fof(f4519,plain,(
% 5.21/6.14 ~sQ69_spl|sQ70_spl|~sQ66_spl|~sQ65_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f4512,f4513,f4516,f4492,f4485])).
% 5.21/6.14 fof(f4520,plain,(
% 5.21/6.14 $false|sQ69_spl),
% 5.21/6.14 inference(forward_subsumption_resolution,[status(thm)],[f4515,f3006])).
% 5.21/6.14 fof(f4521,plain,(
% 5.21/6.14 sQ69_spl),
% 5.21/6.14 inference(contradiction_clause,[status(thm)],[f4520])).
% 5.21/6.14 fof(f4524,plain,(
% 5.21/6.14 ![X0,X1]: (~element(X0,the_carrier(sK362_skl))|latt_element_smaller(sK362_skl,X0,X1)|empty_carrier(sK362_skl)|~lattice(sK362_skl)|~latt_str(sK362_skl)|~element(X0,the_carrier(sK362_skl))|~latt_element_smaller(sK362_skl,X0,X1)|~sQ68_spl)),
% 5.21/6.14 inference(resolution,[status(thm)],[f4508,f2989])).
% 5.21/6.14 fof(f4525,definition,(
% 5.21/6.14 ![X0,X1]: (sQ71_spl <=> (~element(X0,the_carrier(sK362_skl))|latt_element_smaller(sK362_skl,X0,X1)|~element(X0,the_carrier(sK362_skl))|~latt_element_smaller(sK362_skl,X0,X1)))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4528,definition,(
% 5.21/6.14 sQ72_spl <=> (lattice(sK362_skl))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4530,plain,(
% 5.21/6.14 ~lattice(sK362_skl)|sQ72_spl),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4528])).
% 5.21/6.14 fof(f4531,plain,(
% 5.21/6.14 sQ71_spl|sQ63_spl|~sQ72_spl|~sQ64_spl|~sQ68_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f4524,f4525,f4479,f4528,f4482,f4507])).
% 5.21/6.14 fof(f4532,plain,(
% 5.21/6.14 ![X0,X1]: (empty_carrier(sK169_skl)|~latt_str(sK169_skl)|~element(X0,the_carrier(sK169_skl))|latt_element_smaller(sK169_skl,X0,X1)|~relstr_set_smaller(poset_of_lattice(sK169_skl),X1,cast_to_el_of_LattPOSet(sK169_skl,X0)))),
% 5.21/6.14 inference(resolution,[status(thm)],[f2154,f2990])).
% 5.21/6.14 fof(f4533,plain,(
% 5.21/6.14 ![X0,X1]: (empty_carrier(sK169_skl)|~latt_str(sK169_skl)|~element(X0,the_carrier(poset_of_lattice(sK169_skl)))|relstr_element_smaller(poset_of_lattice(sK169_skl),X1,X0)|~latt_set_smaller(sK169_skl,cast_to_el_of_lattice(sK169_skl,X0),X1))),
% 5.21/6.14 inference(resolution,[status(thm)],[f2154,f2967])).
% 5.21/6.14 fof(f4534,plain,(
% 5.21/6.14 ![X0]: (empty_carrier(sK169_skl)|~latt_str(sK169_skl)|~element(X0,the_carrier(poset_of_lattice(sK169_skl)))|element(cast_to_el_of_lattice(sK169_skl,X0),the_carrier(sK169_skl)))),
% 5.21/6.14 inference(resolution,[status(thm)],[f2154,f1522])).
% 5.21/6.14 fof(f4535,plain,(
% 5.21/6.14 ![X0]: (empty_carrier(sK169_skl)|~latt_str(sK169_skl)|~element(X0,the_carrier(poset_of_lattice(sK169_skl)))|cast_to_el_of_lattice(sK169_skl,X0)=X0)),
% 5.21/6.14 inference(resolution,[status(thm)],[f2154,f1220])).
% 5.21/6.14 fof(f4536,definition,(
% 5.21/6.14 sQ73_spl <=> (empty_carrier(sK169_skl))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4537,plain,(
% 5.21/6.14 empty_carrier(sK169_skl)|~sQ73_spl),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4536])).
% 5.21/6.14 fof(f4539,definition,(
% 5.21/6.14 sQ74_spl <=> (latt_str(sK169_skl))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4541,plain,(
% 5.21/6.14 ~latt_str(sK169_skl)|sQ74_spl),
% 5.21/6.14 inference(component_clause,[status(thm)],[f4539])).
% 5.21/6.14 fof(f4542,definition,(
% 5.21/6.14 ![X0,X1]: (sQ75_spl <=> (~element(X0,the_carrier(sK169_skl))|latt_element_smaller(sK169_skl,X0,X1)|~relstr_set_smaller(poset_of_lattice(sK169_skl),X1,cast_to_el_of_LattPOSet(sK169_skl,X0))))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4545,plain,(
% 5.21/6.14 sQ73_spl|~sQ74_spl|sQ75_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f4532,f4536,f4539,f4542])).
% 5.21/6.14 fof(f4546,definition,(
% 5.21/6.14 ![X0,X1]: (sQ76_spl <=> (~element(X0,the_carrier(poset_of_lattice(sK169_skl)))|relstr_element_smaller(poset_of_lattice(sK169_skl),X1,X0)|~latt_set_smaller(sK169_skl,cast_to_el_of_lattice(sK169_skl,X0),X1)))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4549,plain,(
% 5.21/6.14 sQ73_spl|~sQ74_spl|sQ76_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f4533,f4536,f4539,f4546])).
% 5.21/6.14 fof(f4550,definition,(
% 5.21/6.14 ![X0]: (sQ77_spl <=> (~element(X0,the_carrier(poset_of_lattice(sK169_skl)))|element(cast_to_el_of_lattice(sK169_skl,X0),the_carrier(sK169_skl))))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4553,plain,(
% 5.21/6.14 sQ73_spl|~sQ74_spl|sQ77_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f4534,f4536,f4539,f4550])).
% 5.21/6.14 fof(f4554,definition,(
% 5.21/6.14 ![X0]: (sQ78_spl <=> (~element(X0,the_carrier(poset_of_lattice(sK169_skl)))|cast_to_el_of_lattice(sK169_skl,X0)=X0))),
% 5.21/6.14 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 5.21/6.14 fof(f4557,plain,(
% 5.21/6.14 sQ73_spl|~sQ74_spl|sQ78_spl),
% 5.21/6.14 inference(split_clause,[status(thm)],[f4535,f4536,f4539,f4554])).
% 5.21/6.14 fof(f4558,plain,(
% 5.21/6.14 $false|sQ74_spl),
% 5.21/6.14 inference(forward_subsumption_resolution,[status(thm)],[f4541,f2145])).
% 5.21/6.15 fof(f4559,plain,(
% 5.21/6.15 sQ74_spl),
% 5.21/6.15 inference(contradiction_clause,[status(thm)],[f4558])).
% 5.21/6.15 fof(f4560,plain,(
% 5.21/6.15 $false|~sQ73_spl),
% 5.21/6.15 inference(forward_subsumption_resolution,[status(thm)],[f4537,f2146])).
% 5.21/6.15 fof(f4561,plain,(
% 5.21/6.15 ~sQ73_spl),
% 5.21/6.15 inference(contradiction_clause,[status(thm)],[f4560])).
% 5.21/6.15 fof(f4577,plain,(
% 5.21/6.15 ![X0,X1,X2,X3]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~relstr_set_smaller(X0,unordered_pair(X2,X3),X1)|~element(X2,the_carrier(X0))|related(X0,X2,X1))),
% 5.21/6.15 inference(resolution,[status(thm)],[f4228,f1450])).
% 5.21/6.15 fof(f4581,plain,(
% 5.21/6.15 ![X0,X1,X2,X3]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~relstr_set_smaller(X0,unordered_pair(X2,X3),X1)|~element(X3,the_carrier(X0))|related(X0,X3,X1))),
% 5.21/6.15 inference(resolution,[status(thm)],[f4229,f1450])).
% 5.21/6.15 fof(f4584,plain,(
% 5.21/6.15 ![X0,X1,X2,X3]: (~rel_str(poset_of_lattice(X0))|~element(cast_to_el_of_LattPOSet(X0,X1),the_carrier(poset_of_lattice(X0)))|~element(X2,the_carrier(poset_of_lattice(X0)))|related(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1))|empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|~latt_element_smaller(X0,X1,unordered_pair(X2,X3)))),
% 5.21/6.15 inference(resolution,[status(thm)],[f4577,f2989])).
% 5.21/6.15 fof(f4585,plain,(
% 5.21/6.15 ![X0,X1,X2,X3]: (~element(cast_to_el_of_LattPOSet(X0,X1),the_carrier(poset_of_lattice(X0)))|~element(X2,the_carrier(poset_of_lattice(X0)))|related(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1))|empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|~latt_element_smaller(X0,X1,unordered_pair(X2,X3)))),
% 5.21/6.15 inference(forward_subsumption_resolution,[status(thm)],[f4584,f1506])).
% 5.21/6.15 fof(f4586,plain,(
% 5.21/6.15 ![X0,X1,X2,X3]: (~rel_str(poset_of_lattice(X0))|~element(cast_to_el_of_LattPOSet(X0,X1),the_carrier(poset_of_lattice(X0)))|~element(X2,the_carrier(poset_of_lattice(X0)))|related(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1))|empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|~latt_element_smaller(X0,X1,unordered_pair(X3,X2)))),
% 5.21/6.15 inference(resolution,[status(thm)],[f4581,f2989])).
% 5.21/6.15 fof(f4587,plain,(
% 5.21/6.15 ![X0,X1,X2,X3]: (~element(cast_to_el_of_LattPOSet(X0,X1),the_carrier(poset_of_lattice(X0)))|~element(X2,the_carrier(poset_of_lattice(X0)))|related(poset_of_lattice(X0),X2,cast_to_el_of_LattPOSet(X0,X1))|empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~element(X1,the_carrier(X0))|~latt_element_smaller(X0,X1,unordered_pair(X3,X2)))),
% 5.21/6.15 inference(forward_subsumption_resolution,[status(thm)],[f4586,f1506])).
% 5.21/6.15 fof(f4593,plain,(
% 5.21/6.15 ![X0]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|~rel_str(poset_of_lattice(X0))|poset_of_lattice(X0)=rel_str_of(the_carrier(poset_of_lattice(X0)),the_InternalRel(poset_of_lattice(X0))))),
% 5.21/6.15 inference(resolution,[status(thm)],[f1502,f643])).
% 5.21/6.15 fof(f4594,plain,(
% 5.21/6.15 ![X0]: (empty_carrier(X0)|~lattice(X0)|~latt_str(X0)|poset_of_lattice(X0)=rel_str_of(the_carrier(poset_of_lattice(X0)),the_InternalRel(poset_of_lattice(X0))))),
% 5.21/6.15 inference(forward_subsumption_resolution,[status(thm)],[f4593,f1506])).
% 5.21/6.15 fof(f4596,plain,(
% 5.21/6.15 empty_carrier(sK169_skl)|~latt_str(sK169_skl)|poset_of_lattice(sK169_skl)=rel_str_of(the_carrier(poset_of_lattice(sK169_skl)),the_InternalRel(poset_of_lattice(sK169_skl)))),
% 5.21/6.15 inference(resolution,[status(thm)],[f4594,f2154])).
% 5.21/6.15 fof(f4597,plain,(
% 5.21/6.15 empty_carrier(sK362_skl)|~latt_str(sK362_skl)|poset_of_lattice(sK362_skl)=rel_str_of(the_carrier(poset_of_lattice(sK362_skl)),the_InternalRel(poset_of_lattice(sK362_skl)))),
% 5.21/6.15 inference(resolution,[status(thm)],[f4594,f3004])).
% 5.21/6.15 fof(f4599,definition,(
% 5.21/6.15 sQ79_spl <=> (poset_of_lattice(sK169_skl)=rel_str_of(the_carrier(poset_of_lattice(sK169_skl)),the_InternalRel(poset_of_lattice(sK169_skl))))),
% 5.21/6.15 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 5.21/6.15 fof(f4602,plain,(
% 5.21/6.15 sQ73_spl|~sQ74_spl|sQ79_spl),
% 5.21/6.15 inference(split_clause,[status(thm)],[f4596,f4536,f4539,f4599])).
% 5.21/6.15 fof(f4603,definition,(
% 5.21/6.15 sQ80_spl <=> (poset_of_lattice(sK362_skl)=rel_str_of(the_carrier(poset_of_lattice(sK362_skl)),the_InternalRel(poset_of_lattice(sK362_skl))))),
% 5.21/6.15 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 5.21/6.15 fof(f4606,plain,(
% 5.21/6.15 sQ63_spl|~sQ64_spl|sQ80_spl),
% 5.21/6.15 inference(split_clause,[status(thm)],[f4597,f4479,f4482,f4603])).
% 5.21/6.15 fof(f4617,plain,(
% 5.21/6.15 empty_carrier(sK169_skl)|~latt_str(sK169_skl)|poset_of_lattice(sK169_skl)=rel_str_of(the_carrier(sK169_skl),k2_lattice3(sK169_skl))),
% 5.21/6.15 inference(resolution,[status(thm)],[f1076,f2154])).
% 5.21/6.15 fof(f4618,plain,(
% 5.21/6.15 empty_carrier(sK362_skl)|~latt_str(sK362_skl)|poset_of_lattice(sK362_skl)=rel_str_of(the_carrier(sK362_skl),k2_lattice3(sK362_skl))),
% 5.21/6.15 inference(resolution,[status(thm)],[f1076,f3004])).
% 5.21/6.15 fof(f4620,definition,(
% 5.21/6.15 sQ81_spl <=> (poset_of_lattice(sK169_skl)=rel_str_of(the_carrier(sK169_skl),k2_lattice3(sK169_skl)))),
% 5.21/6.15 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 5.21/6.15 fof(f4623,plain,(
% 5.21/6.15 sQ73_spl|~sQ74_spl|sQ81_spl),
% 5.21/6.15 inference(split_clause,[status(thm)],[f4617,f4536,f4539,f4620])).
% 5.21/6.15 fof(f4624,definition,(
% 5.21/6.15 sQ82_spl <=> (poset_of_lattice(sK362_skl)=rel_str_of(the_carrier(sK362_skl),k2_lattice3(sK362_skl)))),
% 5.21/6.15 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 5.21/6.15 fof(f4627,plain,(
% 5.21/6.15 sQ63_spl|~sQ64_spl|sQ82_spl),
% 5.21/6.15 inference(split_clause,[status(thm)],[f4618,f4479,f4482,f4624])).
% 5.21/6.15 fof(f4629,plain,(
% 5.21/6.15 ![X0]: (empty_carrier(sK169_skl)|~latt_str(sK169_skl)|~element(X0,the_carrier(sK169_skl))|cast_to_el_of_LattPOSet(sK169_skl,X0)=X0)),
% 5.21/6.15 inference(resolution,[status(thm)],[f1164,f2154])).
% 5.21/6.15 fof(f4630,plain,(
% 5.21/6.15 ![X0]: (empty_carrier(sK362_skl)|~latt_str(sK362_skl)|~element(X0,the_carrier(sK362_skl))|cast_to_el_of_LattPOSet(sK362_skl,X0)=X0)),
% 5.21/6.15 inference(resolution,[status(thm)],[f1164,f3004])).
% 5.21/6.15 fof(f4632,definition,(
% 5.21/6.15 ![X0]: (sQ83_spl <=> (~element(X0,the_carrier(sK169_skl))|cast_to_el_of_LattPOSet(sK169_skl,X0)=X0))),
% 5.21/6.15 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 5.21/6.15 fof(f4635,plain,(
% 5.21/6.15 sQ73_spl|~sQ74_spl|sQ83_spl),
% 5.21/6.15 inference(split_clause,[status(thm)],[f4629,f4536,f4539,f4632])).
% 5.21/6.15 fof(f4636,definition,(
% 5.21/6.15 ![X0]: (sQ84_spl <=> (~element(X0,the_carrier(sK362_skl))|cast_to_el_of_LattPOSet(sK362_skl,X0)=X0))),
% 5.21/6.15 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 5.21/6.15 fof(f4637,plain,(
% 5.21/6.15 ![X0]: (~element(X0,the_carrier(sK362_skl))|cast_to_el_of_LattPOSet(sK362_skl,X0)=X0|~sQ84_spl)),
% 5.21/6.15 inference(component_clause,[status(thm)],[f4636])).
% 5.21/6.15 fof(f4639,plain,(
% 5.21/6.15 sQ63_spl|~sQ64_spl|sQ84_spl),
% 5.21/6.15 inference(split_clause,[status(thm)],[f4630,f4479,f4482,f4636])).
% 5.21/6.15 fof(f4641,plain,(
% 5.21/6.15 cast_to_el_of_LattPOSet(sK362_skl,sK363_skl)=sK363_skl|~sQ84_spl|~sQ70_spl),
% 5.21/6.15 inference(resolution,[status(thm)],[f4637,f4517])).
% 5.21/6.15 fof(f4642,plain,(
% 5.21/6.15 ![X0]: (~element(sK363_skl,the_carrier(sK362_skl))|latt_element_smaller(sK362_skl,sK363_skl,X0)|~relstr_set_smaller(poset_of_lattice(sK362_skl),X0,sK363_skl)|~sQ68_spl|~sQ84_spl|~sQ70_spl)),
% 5.21/6.15 inference(paramodulation,[status(thm)],[f4641,f4508])).
% 5.21/6.15 fof(f4643,plain,(
% 5.21/6.15 ![X0,X1]: (~element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl)))|~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|related(poset_of_lattice(sK362_skl),X0,cast_to_el_of_LattPOSet(sK362_skl,sK363_skl))|empty_carrier(sK362_skl)|~lattice(sK362_skl)|~latt_str(sK362_skl)|~element(sK363_skl,the_carrier(sK362_skl))|~latt_element_smaller(sK362_skl,sK363_skl,unordered_pair(X1,X0))|~sQ84_spl|~sQ70_spl)),
% 5.21/6.15 inference(paramodulation,[status(thm)],[f4641,f4587])).
% 5.21/6.15 fof(f4644,plain,(
% 5.21/6.15 ![X0,X1]: (~element(sK363_skl,the_carrier(poset_of_lattice(sK362_skl)))|~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|related(poset_of_lattice(sK362_skl),X0,cast_to_el_of_LattPOSet(sK362_skl,sK363_skl))|empty_carrier(sK362_skl)|~lattice(sK362_skl)|~latt_str(sK362_skl)|~element(sK363_skl,the_carrier(sK362_skl))|~latt_element_smaller(sK362_skl,sK363_skl,unordered_pair(X0,X1))|~sQ84_spl|~sQ70_spl)),
% 5.21/6.15 inference(paramodulation,[status(thm)],[f4641,f4585])).
% 5.21/6.15 fof(f4645,plain,(
% 5.21/6.15 ![X0]: (empty_carrier(sK362_skl)|~lattice(sK362_skl)|~latt_str(sK362_skl)|~element(sK363_skl,the_carrier(sK362_skl))|~latt_element_smaller(sK362_skl,sK363_skl,X0)|relstr_set_smaller(poset_of_lattice(sK362_skl),X0,sK363_skl)|~sQ84_spl|~sQ70_spl)),
% 5.21/6.15 inference(paramodulation,[status(thm)],[f4641,f2989])).
% 5.21/6.15 fof(f4646,definition,(
% 5.21/6.15 ![X0]: (sQ85_spl <=> (latt_element_smaller(sK362_skl,sK363_skl,X0)|~relstr_set_smaller(poset_of_lattice(sK362_skl),X0,sK363_skl)))),
% 5.21/6.15 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 5.21/6.15 fof(f4647,plain,(
% 5.21/6.15 ![X0]: (latt_element_smaller(sK362_skl,sK363_skl,X0)|~relstr_set_smaller(poset_of_lattice(sK362_skl),X0,sK363_skl)|~sQ85_spl)),
% 5.21/6.15 inference(component_clause,[status(thm)],[f4646])).
% 5.21/6.15 fof(f4649,plain,(
% 5.21/6.15 ~sQ70_spl|sQ85_spl|~sQ68_spl|~sQ84_spl),
% 5.21/6.15 inference(split_clause,[status(thm)],[f4642,f4516,f4646,f4507,f4636])).
% 5.21/6.15 fof(f4650,definition,(
% 5.21/6.15 ![X0,X1]: (sQ86_spl <=> (~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|related(poset_of_lattice(sK362_skl),X0,cast_to_el_of_LattPOSet(sK362_skl,sK363_skl))|~latt_element_smaller(sK362_skl,sK363_skl,unordered_pair(X1,X0))))),
% 5.21/6.15 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 5.21/6.15 fof(f4653,plain,(
% 5.21/6.15 ~sQ69_spl|sQ86_spl|sQ63_spl|~sQ72_spl|~sQ64_spl|~sQ70_spl|~sQ84_spl),
% 5.21/6.15 inference(split_clause,[status(thm)],[f4643,f4513,f4650,f4479,f4528,f4482,f4516,f4636])).
% 5.21/6.15 fof(f4654,definition,(
% 5.21/6.15 ![X0,X1]: (sQ87_spl <=> (~element(X0,the_carrier(poset_of_lattice(sK362_skl)))|related(poset_of_lattice(sK362_skl),X0,cast_to_el_of_LattPOSet(sK362_skl,sK363_skl))|~latt_element_smaller(sK362_skl,sK363_skl,unordered_pair(X0,X1))))),
% 5.21/6.15 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 5.21/6.15 fof(f4657,plain,(
% 5.21/6.15 ~sQ69_spl|sQ87_spl|sQ63_spl|~sQ72_spl|~sQ64_spl|~sQ70_spl|~sQ84_spl),
% 5.21/6.15 inference(split_clause,[status(thm)],[f4644,f4513,f4654,f4479,f4528,f4482,f4516,f4636])).
% 5.21/6.15 fof(f4658,definition,(
% 5.21/6.15 ![X0]: (sQ88_spl <=> (~latt_element_smaller(sK362_skl,sK363_skl,X0)|relstr_set_smaller(poset_of_lattice(sK362_skl),X0,sK363_skl)))),
% 5.21/6.15 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 5.21/6.17 fof(f4659,plain,(
% 5.21/6.17 ![X0]: (~latt_element_smaller(sK362_skl,sK363_skl,X0)|relstr_set_smaller(poset_of_lattice(sK362_skl),X0,sK363_skl)|~sQ88_spl)),
% 5.21/6.17 inference(component_clause,[status(thm)],[f4658])).
% 5.21/6.17 fof(f4661,plain,(
% 5.21/6.17 sQ63_spl|~sQ72_spl|~sQ64_spl|~sQ70_spl|sQ88_spl|~sQ84_spl),
% 5.21/6.17 inference(split_clause,[status(thm)],[f4645,f4479,f4528,f4482,f4516,f4658,f4636])).
% 5.21/6.17 fof(f4662,plain,(
% 5.21/6.17 $false|sQ72_spl),
% 5.21/6.17 inference(forward_subsumption_resolution,[status(thm)],[f4530,f3004])).
% 5.21/6.17 fof(f4663,plain,(
% 5.21/6.17 sQ72_spl),
% 5.21/6.17 inference(contradiction_clause,[status(thm)],[f4662])).
% 5.21/6.17 fof(f4669,plain,(
% 5.21/6.17 latt_element_smaller(sK362_skl,sK363_skl,sK364_skl)|~sQ85_spl|~sQ31_spl),
% 5.21/6.17 inference(resolution,[status(thm)],[f4647,f4024])).
% 5.21/6.17 fof(f4670,plain,(
% 5.21/6.17 $false|~sQ65_spl|sQ32_spl|~sQ85_spl|~sQ31_spl),
% 5.21/6.17 inference(forward_subsumption_resolution,[status(thm)],[f4669,f4490])).
% 5.21/6.17 fof(f4671,plain,(
% 5.21/6.17 ~sQ65_spl|sQ32_spl|~sQ85_spl|~sQ31_spl),
% 5.21/6.17 inference(contradiction_clause,[status(thm)],[f4670])).
% 5.21/6.17 fof(f4672,plain,(
% 5.21/6.17 latt_element_smaller(sK362_skl,sK363_skl,sK364_skl)|~sQ65_spl|~sQ32_spl),
% 5.21/6.17 inference(forward_demodulation,[status(thm)],[f4489,f4027])).
% 5.21/6.17 fof(f4673,plain,(
% 5.21/6.17 relstr_set_smaller(poset_of_lattice(sK362_skl),sK364_skl,sK363_skl)|~sQ88_spl|~sQ65_spl|~sQ32_spl),
% 5.21/6.17 inference(resolution,[status(thm)],[f4659,f4672])).
% 5.21/6.17 fof(f4674,plain,(
% 5.21/6.17 sQ31_spl|~sQ88_spl|~sQ65_spl|~sQ32_spl),
% 5.21/6.17 inference(split_clause,[status(thm)],[f4673,f4023,f4658,f4485,f4026])).
% 5.21/6.17 fof(f4675,plain,(
% 5.21/6.17 $false),
% 5.21/6.17 inference(sat_refutation,[status(thm)],[f4029,f4030,f4488,f4495,f4497,f4499,f4505,f4510,f4519,f4521,f4531,f4545,f4549,f4553,f4557,f4559,f4561,f4602,f4606,f4623,f4627,f4635,f4639,f4649,f4653,f4657,f4661,f4663,f4671,f4674])).
% 5.21/6.17 % SZS output end CNFRefutation for theBenchmark.p
% 5.21/6.18 % Elapsed time: 0.817581 seconds
% 5.21/6.18 % CPU time: 5.676617 seconds
% 5.21/6.18 % Total memory used: 263.869 MB
% 5.21/6.18 % Net memory used: 257.484 MB
%------------------------------------------------------------------------------