%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU349+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 : Sun Sep 27 08:45:53 AM UTC 2026
% Result : Theorem 156.69s 21.40s
% Output : CNFRefutation 164.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 110
% Number of leaves : 16
% Syntax : Number of formulae : 296 ( 33 unt; 0 def)
% Number of atoms : 1113 ( 38 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 1347 ( 530 ~; 701 |; 78 &)
% ( 8 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 326 ( 5 sgn 82 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(abstractness_v1_orders_2,axiom,
! [A] :
( rel_str(A)
=> ( strict_rel_str(A)
=> A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ),
file('theBenchmark.p',abstractness_v1_orders_2) ).
fof(cc1_lattices,axiom,
! [A] :
( latt_str(A)
=> ( ( lattice(A)
& ~ empty_carrier(A) )
=> ( join_absorbing(A)
& meet_absorbing(A)
& meet_associative(A)
& meet_commutative(A)
& join_associative(A)
& join_commutative(A)
& ~ empty_carrier(A) ) ) ),
file('theBenchmark.p',cc1_lattices) ).
fof(d17_lattice3,axiom,
! [A] :
( ( latt_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( latt_element_smaller(A,B,C)
<=> ! [D] :
( element(D,the_carrier(A))
=> ( in(D,C)
=> below(A,D,B) ) ) ) ) ),
file('theBenchmark.p',d17_lattice3) ).
fof(d2_lattice3,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> poset_of_lattice(A) = rel_str_of(the_carrier(A),k2_lattice3(A)) ),
file('theBenchmark.p',d2_lattice3) ).
fof(d3_lattice3,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> cast_to_el_of_LattPOSet(A,B) = B ) ),
file('theBenchmark.p',d3_lattice3) ).
fof(d9_lattice3,axiom,
! [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) ) ) ) ) ),
file('theBenchmark.p',d9_lattice3) ).
fof(dt_k2_lattice3,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ( relation_of2_as_subset(k2_lattice3(A),the_carrier(A),the_carrier(A))
& v1_partfun1(k2_lattice3(A),the_carrier(A),the_carrier(A))
& transitive(k2_lattice3(A))
& antisymmetric(k2_lattice3(A))
& reflexive(k2_lattice3(A)) ) ),
file('theBenchmark.p',dt_k2_lattice3) ).
fof(dt_k3_lattice3,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ( rel_str(poset_of_lattice(A))
& antisymmetric_relstr(poset_of_lattice(A))
& transitive_relstr(poset_of_lattice(A))
& reflexive_relstr(poset_of_lattice(A))
& strict_rel_str(poset_of_lattice(A)) ) ),
file('theBenchmark.p',dt_k3_lattice3) ).
fof(dt_k4_lattice3,axiom,
! [A,B] :
( ( element(B,the_carrier(A))
& latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> element(cast_to_el_of_LattPOSet(A,B),the_carrier(poset_of_lattice(A))) ),
file('theBenchmark.p',dt_k4_lattice3) ).
fof(fc4_lattice3,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ( antisymmetric_relstr(poset_of_lattice(A))
& transitive_relstr(poset_of_lattice(A))
& reflexive_relstr(poset_of_lattice(A))
& strict_rel_str(poset_of_lattice(A))
& ~ empty_carrier(poset_of_lattice(A)) ) ),
file('theBenchmark.p',fc4_lattice3) ).
fof(free_g1_orders_2,axiom,
! [A,B] :
( relation_of2(B,A,A)
=> ! [C,D] :
( rel_str_of(A,B) = rel_str_of(C,D)
=> ( B = D
& A = C ) ) ),
file('theBenchmark.p',free_g1_orders_2) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(redefinition_r3_lattices,axiom,
! [A,B,C] :
( ( element(C,the_carrier(A))
& element(B,the_carrier(A))
& latt_str(A)
& join_absorbing(A)
& meet_absorbing(A)
& meet_commutative(A)
& ~ empty_carrier(A) )
=> ( below_refl(A,B,C)
<=> below(A,B,C) ) ),
file('theBenchmark.p',redefinition_r3_lattices) ).
fof(redefinition_r3_orders_2,axiom,
! [A,B,C] :
( ( element(C,the_carrier(A))
& element(B,the_carrier(A))
& rel_str(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( related_reflexive(A,B,C)
<=> related(A,B,C) ) ),
file('theBenchmark.p',redefinition_r3_orders_2) ).
fof(t7_lattice3,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( below_refl(A,B,C)
<=> related_reflexive(poset_of_lattice(A),cast_to_el_of_LattPOSet(A,B),cast_to_el_of_LattPOSet(A,C)) ) ) ) ),
file('theBenchmark.p',t7_lattice3) ).
fof(t30_lattice3,conjecture,
! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(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)) ) ) ),
file('theBenchmark.p',t30_lattice3) ).
fof(t30_lattice3_neg,negated_conjecture,
~ ! [A,B] :
( ( latt_str(B)
& lattice(B)
& ~ empty_carrier(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)) ) ) ),
inference(assume_negation,[status(cth)],[t30_lattice3]) ).
fof(nnf_10,plain,
! [A] :
( ! [B,C] :
( ( ( ? [D] :
( ~ related(A,D,C)
& in(D,B)
& element(D,the_carrier(A)) )
| relstr_set_smaller(A,B,C) )
& ( ! [X0] :
( related(A,X0,C)
| ~ in(X0,B)
| ~ element(X0,the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(fof_nnf,[status(thm)],[d9_lattice3]) ).
fof(sk_d9_lattice3_sk,plain,
! [A] :
( ! [B,C] :
( ( ( ( ~ related(A,sK0(A,B,C),C)
& in(sK0(A,B,C),B)
& element(sK0(A,B,C),the_carrier(A)) )
| relstr_set_smaller(A,B,C) )
& ( ! [X0] :
( related(A,X0,C)
| ~ in(X0,B)
| ~ element(X0,the_carrier(A)) )
| ~ relstr_set_smaller(A,B,C) ) )
| ~ element(C,the_carrier(A)) )
| ~ rel_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(D,sK0(A,B,C))],[nnf_10]) ).
fof(sk_d9_lattice3,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ related(VAR_0,sK0(VAR_0,VAR_2,VAR_1),VAR_1)
| relstr_set_smaller(VAR_0,VAR_2,VAR_1)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK0(VAR_0,VAR_2,VAR_1),VAR_2)
| relstr_set_smaller(VAR_0,VAR_2,VAR_1)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( element(sK0(VAR_0,VAR_2,VAR_1),the_carrier(VAR_0))
| relstr_set_smaller(VAR_0,VAR_2,VAR_1)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ rel_str(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( related(VAR_0,VAR_3,VAR_1)
| ~ in(VAR_3,VAR_2)
| ~ element(VAR_3,the_carrier(VAR_0))
| ~ relstr_set_smaller(VAR_0,VAR_2,VAR_1)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ rel_str(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d9_lattice3_sk]) ).
cnf(c_72,plain,
( ~ related(A,sK0(A,C,B),B)
| relstr_set_smaller(A,C,B)
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d9_lattice3]) ).
cnf(c_73,plain,
( in(sK0(A,C,B),C)
| relstr_set_smaller(A,C,B)
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d9_lattice3]) ).
cnf(c_74,plain,
( element(sK0(A,C,B),the_carrier(A))
| relstr_set_smaller(A,C,B)
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d9_lattice3]) ).
cnf(c_75,plain,
( related(A,D,B)
| ~ in(D,C)
| ~ element(D,the_carrier(A))
| ~ relstr_set_smaller(A,C,B)
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(split_conjunct,[status(thm)],[sk_d9_lattice3]) ).
cnf(c_76,plain,
( rel_str_of(the_carrier(A),the_InternalRel(A)) = A
| ~ strict_rel_str(A)
| ~ rel_str(A) ),
inference(clausify,[status(thm)],[abstractness_v1_orders_2]) ).
cnf(c_77,plain,
( rel_str(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[dt_k3_lattice3]) ).
cnf(c_88,plain,
( related(A,B,C)
| ~ related_reflexive(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ rel_str(A)
| ~ reflexive_relstr(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[redefinition_r3_orders_2]) ).
cnf(c_89,plain,
( ~ related(A,B,C)
| related_reflexive(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ rel_str(A)
| ~ reflexive_relstr(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[redefinition_r3_orders_2]) ).
fof(nnf_70,plain,
? [A,B] :
( ? [C] :
( ( ~ 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))
| latt_element_smaller(B,C,A) )
& element(C,the_carrier(B)) )
& latt_str(B)
& lattice(B)
& ~ empty_carrier(B) ),
inference(fof_nnf,[status(thm)],[t30_lattice3_neg]) ).
fof(sk_t30_lattice3_neg,plain,
( ( ~ relstr_set_smaller(poset_of_lattice(sK1),sK4,cast_to_el_of_LattPOSet(sK1,sK3))
| ~ latt_element_smaller(sK1,sK3,sK4) )
& ( relstr_set_smaller(poset_of_lattice(sK1),sK4,cast_to_el_of_LattPOSet(sK1,sK3))
| latt_element_smaller(sK1,sK3,sK4) )
& element(sK3,the_carrier(sK1))
& latt_str(sK1)
& lattice(sK1)
& ~ empty_carrier(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK3,sK4]),skolemize(A,sK4),skolemize(B,sK1),skolemize(C,sK3)],[nnf_70]) ).
cnf(c_91,negated_conjecture,
latt_str(sK1),
inference(split_conjunct,[status(thm)],[sk_t30_lattice3_neg]) ).
cnf(c_92,plain,
( ~ related(poset_of_lattice(A),sK0(poset_of_lattice(A),C,B),B)
| relstr_set_smaller(poset_of_lattice(A),C,B)
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(resolve,[status(thm)],[c_77,c_72]) ).
cnf(c_93,plain,
( in(sK0(poset_of_lattice(A),C,B),C)
| relstr_set_smaller(poset_of_lattice(A),C,B)
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(resolve,[status(thm)],[c_77,c_73]) ).
cnf(c_94,plain,
( element(sK0(poset_of_lattice(A),C,B),the_carrier(poset_of_lattice(A)))
| relstr_set_smaller(poset_of_lattice(A),C,B)
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(resolve,[status(thm)],[c_77,c_74]) ).
cnf(c_95,plain,
( related(poset_of_lattice(A),D,B)
| ~ in(D,C)
| ~ element(D,the_carrier(poset_of_lattice(A)))
| ~ relstr_set_smaller(poset_of_lattice(A),C,B)
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(resolve,[status(thm)],[c_77,c_75]) ).
cnf(c_96,plain,
( rel_str_of(the_carrier(poset_of_lattice(A)),the_InternalRel(poset_of_lattice(A))) = poset_of_lattice(A)
| ~ strict_rel_str(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(resolve,[status(thm)],[c_77,c_76]) ).
cnf(c_104,plain,
( ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A)
| related(poset_of_lattice(A),B,C)
| ~ related_reflexive(poset_of_lattice(A),B,C)
| ~ element(C,the_carrier(poset_of_lattice(A)))
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ reflexive_relstr(poset_of_lattice(A))
| empty_carrier(poset_of_lattice(A)) ),
inference(resolve,[status(thm)],[c_88,c_77]) ).
cnf(c_105,plain,
( ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A)
| ~ related(poset_of_lattice(A),B,C)
| related_reflexive(poset_of_lattice(A),B,C)
| ~ element(C,the_carrier(poset_of_lattice(A)))
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ reflexive_relstr(poset_of_lattice(A))
| empty_carrier(poset_of_lattice(A)) ),
inference(resolve,[status(thm)],[c_89,c_77]) ).
cnf(c_107,plain,
( ~ related_reflexive(poset_of_lattice(A),cast_to_el_of_LattPOSet(A,B),cast_to_el_of_LattPOSet(A,C))
| below_refl(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[t7_lattice3]) ).
cnf(c_108,plain,
( related_reflexive(poset_of_lattice(A),cast_to_el_of_LattPOSet(A,B),cast_to_el_of_LattPOSet(A,C))
| ~ below_refl(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[t7_lattice3]) ).
cnf(c_110,plain,
( ~ below(A,B,C)
| below_refl(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| ~ join_absorbing(A)
| ~ meet_absorbing(A)
| ~ meet_commutative(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[redefinition_r3_lattices]) ).
cnf(c_111,plain,
( below(A,B,C)
| ~ below_refl(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| ~ join_absorbing(A)
| ~ meet_absorbing(A)
| ~ meet_commutative(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[redefinition_r3_lattices]) ).
cnf(c_115,plain,
( reflexive_relstr(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[fc4_lattice3]) ).
cnf(c_116,plain,
( strict_rel_str(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[fc4_lattice3]) ).
cnf(c_117,plain,
( ~ empty_carrier(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[fc4_lattice3]) ).
cnf(c_123,plain,
( element(cast_to_el_of_LattPOSet(A,B),the_carrier(poset_of_lattice(A)))
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[dt_k4_lattice3]) ).
cnf(c_128,plain,
( relation_of2_as_subset(k2_lattice3(A),the_carrier(A),the_carrier(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[dt_k2_lattice3]) ).
cnf(c_134,plain,
( cast_to_el_of_LattPOSet(A,B) = B
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[d3_lattice3]) ).
cnf(c_135,plain,
( poset_of_lattice(A) = rel_str_of(the_carrier(A),k2_lattice3(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[d2_lattice3]) ).
fof(nnf_6,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ? [D] :
( ~ below(A,D,B)
& in(D,C)
& element(D,the_carrier(A)) )
| latt_element_smaller(A,B,C) )
& ( ! [X0] :
( below(A,X0,B)
| ~ in(X0,C)
| ~ element(X0,the_carrier(A)) )
| ~ latt_element_smaller(A,B,C) ) )
| ~ element(B,the_carrier(A)) )
| ~ latt_str(A)
| empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[d17_lattice3]) ).
fof(sk_d17_lattice3_sk,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ~ below(A,sK2(A,B,C),B)
& in(sK2(A,B,C),C)
& element(sK2(A,B,C),the_carrier(A)) )
| latt_element_smaller(A,B,C) )
& ( ! [X0] :
( below(A,X0,B)
| ~ in(X0,C)
| ~ element(X0,the_carrier(A)) )
| ~ latt_element_smaller(A,B,C) ) )
| ~ element(B,the_carrier(A)) )
| ~ latt_str(A)
| empty_carrier(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(D,sK2(A,B,C))],[nnf_6]) ).
fof(sk_d17_lattice3,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ below(VAR_0,sK2(VAR_0,VAR_1,VAR_2),VAR_1)
| latt_element_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ latt_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( in(sK2(VAR_0,VAR_1,VAR_2),VAR_2)
| latt_element_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ latt_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( element(sK2(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
| latt_element_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ latt_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( below(VAR_0,VAR_3,VAR_1)
| ~ in(VAR_3,VAR_2)
| ~ element(VAR_3,the_carrier(VAR_0))
| ~ latt_element_smaller(VAR_0,VAR_1,VAR_2)
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ latt_str(VAR_0)
| empty_carrier(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d17_lattice3_sk]) ).
cnf(c_136,plain,
( ~ below(A,sK2(A,B,C),B)
| latt_element_smaller(A,B,C)
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d17_lattice3]) ).
cnf(c_137,plain,
( in(sK2(A,B,C),C)
| latt_element_smaller(A,B,C)
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d17_lattice3]) ).
cnf(c_138,plain,
( element(sK2(A,B,C),the_carrier(A))
| latt_element_smaller(A,B,C)
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d17_lattice3]) ).
cnf(c_139,plain,
( below(A,D,B)
| ~ in(D,C)
| ~ element(D,the_carrier(A))
| ~ latt_element_smaller(A,B,C)
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d17_lattice3]) ).
cnf(c_141,plain,
( join_absorbing(A)
| ~ lattice(A)
| empty_carrier(A)
| ~ latt_str(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_142,plain,
( meet_absorbing(A)
| ~ lattice(A)
| empty_carrier(A)
| ~ latt_str(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_144,plain,
( meet_commutative(A)
| ~ lattice(A)
| empty_carrier(A)
| ~ latt_str(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_163,negated_conjecture,
( relation_of2_as_subset(k2_lattice3(sK1),the_carrier(sK1),the_carrier(sK1))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_128,c_91]) ).
cnf(c_165,plain,
( relation_of2(A,B,C)
| ~ relation_of2_as_subset(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_242,negated_conjecture,
( ~ lattice(sK1)
| empty_carrier(sK1)
| relation_of2(k2_lattice3(sK1),the_carrier(sK1),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_165,c_163]) ).
cnf(c_296,negated_conjecture,
( ~ relstr_set_smaller(poset_of_lattice(sK1),sK4,cast_to_el_of_LattPOSet(sK1,sK3))
| ~ latt_element_smaller(sK1,sK3,sK4) ),
inference(split_conjunct,[status(thm)],[sk_t30_lattice3_neg]) ).
cnf(c_297,negated_conjecture,
( relstr_set_smaller(poset_of_lattice(sK1),sK4,cast_to_el_of_LattPOSet(sK1,sK3))
| latt_element_smaller(sK1,sK3,sK4) ),
inference(split_conjunct,[status(thm)],[sk_t30_lattice3_neg]) ).
cnf(c_298,negated_conjecture,
element(sK3,the_carrier(sK1)),
inference(split_conjunct,[status(thm)],[sk_t30_lattice3_neg]) ).
cnf(c_299,negated_conjecture,
lattice(sK1),
inference(split_conjunct,[status(thm)],[sk_t30_lattice3_neg]) ).
cnf(c_300,negated_conjecture,
~ empty_carrier(sK1),
inference(split_conjunct,[status(thm)],[sk_t30_lattice3_neg]) ).
cnf(c_322,plain,
( C = B
| rel_str_of(C,D) != rel_str_of(B,A)
| ~ relation_of2(A,B,B) ),
inference(clausify,[status(thm)],[free_g1_orders_2]) ).
cnf(c_332,negated_conjecture,
( ~ related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),B,A),A)
| relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_91,c_92]) ).
cnf(c_10423,negated_conjecture,
( ~ related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),B,A),A)
| relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_332]) ).
cnf(c_333,negated_conjecture,
( ~ related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),B,A),A)
| relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1))) ),
inference(resolve,[status(thm)],[c_299,c_10423]) ).
cnf(c_334,negated_conjecture,
( in(sK0(poset_of_lattice(sK1),B,A),B)
| relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_91,c_93]) ).
cnf(c_10424,negated_conjecture,
( in(sK0(poset_of_lattice(sK1),B,A),B)
| relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_334]) ).
cnf(c_335,negated_conjecture,
( in(sK0(poset_of_lattice(sK1),B,A),B)
| relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1))) ),
inference(resolve,[status(thm)],[c_299,c_10424]) ).
cnf(c_336,negated_conjecture,
( element(sK0(poset_of_lattice(sK1),B,A),the_carrier(poset_of_lattice(sK1)))
| relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_91,c_94]) ).
cnf(c_10425,negated_conjecture,
( element(sK0(poset_of_lattice(sK1),B,A),the_carrier(poset_of_lattice(sK1)))
| relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_336]) ).
cnf(c_337,negated_conjecture,
( element(sK0(poset_of_lattice(sK1),B,A),the_carrier(poset_of_lattice(sK1)))
| relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1))) ),
inference(resolve,[status(thm)],[c_299,c_10425]) ).
cnf(c_338,negated_conjecture,
( related(poset_of_lattice(sK1),C,A)
| ~ in(C,B)
| ~ element(C,the_carrier(poset_of_lattice(sK1)))
| ~ relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_91,c_95]) ).
cnf(c_10426,negated_conjecture,
( related(poset_of_lattice(sK1),C,A)
| ~ in(C,B)
| ~ element(C,the_carrier(poset_of_lattice(sK1)))
| ~ relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_338]) ).
cnf(c_339,negated_conjecture,
( related(poset_of_lattice(sK1),C,A)
| ~ in(C,B)
| ~ element(C,the_carrier(poset_of_lattice(sK1)))
| ~ relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(poset_of_lattice(sK1))) ),
inference(resolve,[status(thm)],[c_299,c_10426]) ).
cnf(c_340,negated_conjecture,
( rel_str_of(the_carrier(poset_of_lattice(sK1)),the_InternalRel(poset_of_lattice(sK1))) = poset_of_lattice(sK1)
| ~ strict_rel_str(poset_of_lattice(sK1))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_91,c_96]) ).
cnf(c_10427,negated_conjecture,
( rel_str_of(the_carrier(poset_of_lattice(sK1)),the_InternalRel(poset_of_lattice(sK1))) = poset_of_lattice(sK1)
| ~ strict_rel_str(poset_of_lattice(sK1))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_340]) ).
cnf(c_341,negated_conjecture,
( rel_str_of(the_carrier(poset_of_lattice(sK1)),the_InternalRel(poset_of_lattice(sK1))) = poset_of_lattice(sK1)
| ~ strict_rel_str(poset_of_lattice(sK1)) ),
inference(resolve,[status(thm)],[c_299,c_10427]) ).
cnf(c_348,negated_conjecture,
( ~ lattice(sK1)
| empty_carrier(sK1)
| related(poset_of_lattice(sK1),A,B)
| ~ related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ reflexive_relstr(poset_of_lattice(sK1))
| empty_carrier(poset_of_lattice(sK1)) ),
inference(resolve,[status(thm)],[c_91,c_104]) ).
cnf(c_10428,negated_conjecture,
( ~ lattice(sK1)
| related(poset_of_lattice(sK1),A,B)
| ~ related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ reflexive_relstr(poset_of_lattice(sK1))
| empty_carrier(poset_of_lattice(sK1)) ),
inference(resolve,[status(thm)],[c_300,c_348]) ).
cnf(c_349,negated_conjecture,
( related(poset_of_lattice(sK1),A,B)
| ~ related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ reflexive_relstr(poset_of_lattice(sK1))
| empty_carrier(poset_of_lattice(sK1)) ),
inference(resolve,[status(thm)],[c_299,c_10428]) ).
cnf(c_350,negated_conjecture,
( ~ lattice(sK1)
| empty_carrier(sK1)
| ~ related(poset_of_lattice(sK1),A,B)
| related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ reflexive_relstr(poset_of_lattice(sK1))
| empty_carrier(poset_of_lattice(sK1)) ),
inference(resolve,[status(thm)],[c_91,c_105]) ).
cnf(c_10429,negated_conjecture,
( ~ lattice(sK1)
| ~ related(poset_of_lattice(sK1),A,B)
| related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ reflexive_relstr(poset_of_lattice(sK1))
| empty_carrier(poset_of_lattice(sK1)) ),
inference(resolve,[status(thm)],[c_300,c_350]) ).
cnf(c_351,negated_conjecture,
( ~ related(poset_of_lattice(sK1),A,B)
| related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ reflexive_relstr(poset_of_lattice(sK1))
| empty_carrier(poset_of_lattice(sK1)) ),
inference(resolve,[status(thm)],[c_299,c_10429]) ).
cnf(c_354,negated_conjecture,
( ~ related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,A),cast_to_el_of_LattPOSet(sK1,B))
| below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_107,c_91]) ).
cnf(c_10430,negated_conjecture,
( ~ related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,A),cast_to_el_of_LattPOSet(sK1,B))
| below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_354]) ).
cnf(c_355,negated_conjecture,
( ~ related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,A),cast_to_el_of_LattPOSet(sK1,B))
| below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_299,c_10430]) ).
cnf(c_356,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,A),cast_to_el_of_LattPOSet(sK1,B))
| ~ below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_108,c_91]) ).
cnf(c_10431,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,A),cast_to_el_of_LattPOSet(sK1,B))
| ~ below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_356]) ).
cnf(c_357,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,A),cast_to_el_of_LattPOSet(sK1,B))
| ~ below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_299,c_10431]) ).
cnf(c_360,negated_conjecture,
( ~ below(sK1,A,B)
| below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ join_absorbing(sK1)
| ~ meet_absorbing(sK1)
| ~ meet_commutative(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_110,c_91]) ).
cnf(c_361,negated_conjecture,
( ~ below(sK1,A,B)
| below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ join_absorbing(sK1)
| ~ meet_absorbing(sK1)
| ~ meet_commutative(sK1) ),
inference(resolve,[status(thm)],[c_300,c_360]) ).
cnf(c_362,negated_conjecture,
( below(sK1,A,B)
| ~ below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ join_absorbing(sK1)
| ~ meet_absorbing(sK1)
| ~ meet_commutative(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_111,c_91]) ).
cnf(c_363,negated_conjecture,
( below(sK1,A,B)
| ~ below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ join_absorbing(sK1)
| ~ meet_absorbing(sK1)
| ~ meet_commutative(sK1) ),
inference(resolve,[status(thm)],[c_300,c_362]) ).
cnf(c_370,negated_conjecture,
( reflexive_relstr(poset_of_lattice(sK1))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_115,c_91]) ).
cnf(c_10432,negated_conjecture,
( reflexive_relstr(poset_of_lattice(sK1))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_370]) ).
cnf(c_371,negated_conjecture,
reflexive_relstr(poset_of_lattice(sK1)),
inference(resolve,[status(thm)],[c_299,c_10432]) ).
cnf(c_372,negated_conjecture,
( strict_rel_str(poset_of_lattice(sK1))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_116,c_91]) ).
cnf(c_10433,negated_conjecture,
( strict_rel_str(poset_of_lattice(sK1))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_372]) ).
cnf(c_373,negated_conjecture,
strict_rel_str(poset_of_lattice(sK1)),
inference(resolve,[status(thm)],[c_299,c_10433]) ).
cnf(c_374,negated_conjecture,
( ~ empty_carrier(poset_of_lattice(sK1))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_117,c_91]) ).
cnf(c_10434,negated_conjecture,
( ~ empty_carrier(poset_of_lattice(sK1))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_374]) ).
cnf(c_375,negated_conjecture,
~ empty_carrier(poset_of_lattice(sK1)),
inference(resolve,[status(thm)],[c_299,c_10434]) ).
cnf(c_402,negated_conjecture,
( element(cast_to_el_of_LattPOSet(sK1,A),the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(sK1))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_123,c_91]) ).
cnf(c_10435,negated_conjecture,
( element(cast_to_el_of_LattPOSet(sK1,A),the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(sK1))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_402]) ).
cnf(c_403,negated_conjecture,
( element(cast_to_el_of_LattPOSet(sK1,A),the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_299,c_10435]) ).
cnf(c_417,negated_conjecture,
( cast_to_el_of_LattPOSet(sK1,A) = A
| ~ element(A,the_carrier(sK1))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_134,c_91]) ).
cnf(c_10436,negated_conjecture,
( cast_to_el_of_LattPOSet(sK1,A) = A
| ~ element(A,the_carrier(sK1))
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_417]) ).
cnf(c_418,negated_conjecture,
( cast_to_el_of_LattPOSet(sK1,A) = A
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_299,c_10436]) ).
cnf(c_421,negated_conjecture,
( poset_of_lattice(sK1) = rel_str_of(the_carrier(sK1),k2_lattice3(sK1))
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_135,c_91]) ).
cnf(c_10437,negated_conjecture,
( rel_str_of(the_carrier(sK1),k2_lattice3(sK1)) = poset_of_lattice(sK1)
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(copy,[status(thm)],[c_421]) ).
cnf(c_10438,negated_conjecture,
( rel_str_of(the_carrier(sK1),k2_lattice3(sK1)) = poset_of_lattice(sK1)
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_10437]) ).
cnf(c_422,negated_conjecture,
rel_str_of(the_carrier(sK1),k2_lattice3(sK1)) = poset_of_lattice(sK1),
inference(resolve,[status(thm)],[c_299,c_10438]) ).
cnf(c_424,negated_conjecture,
( ~ below(sK1,sK2(sK1,A,B),A)
| latt_element_smaller(sK1,A,B)
| ~ element(A,the_carrier(sK1))
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_136,c_91]) ).
cnf(c_425,negated_conjecture,
( ~ below(sK1,sK2(sK1,A,B),A)
| latt_element_smaller(sK1,A,B)
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_300,c_424]) ).
cnf(c_427,negated_conjecture,
( in(sK2(sK1,A,B),B)
| latt_element_smaller(sK1,A,B)
| ~ element(A,the_carrier(sK1))
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_137,c_91]) ).
cnf(c_428,negated_conjecture,
( in(sK2(sK1,A,B),B)
| latt_element_smaller(sK1,A,B)
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_300,c_427]) ).
cnf(c_430,negated_conjecture,
( element(sK2(sK1,A,B),the_carrier(sK1))
| latt_element_smaller(sK1,A,B)
| ~ element(A,the_carrier(sK1))
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_138,c_91]) ).
cnf(c_431,negated_conjecture,
( element(sK2(sK1,A,B),the_carrier(sK1))
| latt_element_smaller(sK1,A,B)
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_300,c_430]) ).
cnf(c_433,negated_conjecture,
( below(sK1,C,A)
| ~ in(C,B)
| ~ element(C,the_carrier(sK1))
| ~ latt_element_smaller(sK1,A,B)
| ~ element(A,the_carrier(sK1))
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_139,c_91]) ).
cnf(c_434,negated_conjecture,
( below(sK1,C,A)
| ~ in(C,B)
| ~ element(C,the_carrier(sK1))
| ~ latt_element_smaller(sK1,A,B)
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_300,c_433]) ).
cnf(c_438,negated_conjecture,
( join_absorbing(sK1)
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_141,c_91]) ).
cnf(c_10439,negated_conjecture,
( join_absorbing(sK1)
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_438]) ).
cnf(c_439,negated_conjecture,
join_absorbing(sK1),
inference(resolve,[status(thm)],[c_299,c_10439]) ).
cnf(c_441,negated_conjecture,
( meet_absorbing(sK1)
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_142,c_91]) ).
cnf(c_10440,negated_conjecture,
( meet_absorbing(sK1)
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_441]) ).
cnf(c_442,negated_conjecture,
meet_absorbing(sK1),
inference(resolve,[status(thm)],[c_299,c_10440]) ).
cnf(c_447,negated_conjecture,
( meet_commutative(sK1)
| ~ lattice(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_144,c_91]) ).
cnf(c_10441,negated_conjecture,
( meet_commutative(sK1)
| ~ lattice(sK1) ),
inference(resolve,[status(thm)],[c_300,c_447]) ).
cnf(c_448,negated_conjecture,
meet_commutative(sK1),
inference(resolve,[status(thm)],[c_299,c_10441]) ).
cnf(c_10442,negated_conjecture,
( ~ lattice(sK1)
| relation_of2(k2_lattice3(sK1),the_carrier(sK1),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_300,c_242]) ).
cnf(c_514,negated_conjecture,
relation_of2(k2_lattice3(sK1),the_carrier(sK1),the_carrier(sK1)),
inference(resolve,[status(thm)],[c_299,c_10442]) ).
cnf(c_10443,negated_conjecture,
( ~ related(poset_of_lattice(sK1),A,B)
| related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ reflexive_relstr(poset_of_lattice(sK1)) ),
inference(resolve,[status(thm)],[c_375,c_351]) ).
cnf(c_544,negated_conjecture,
( ~ related(poset_of_lattice(sK1),A,B)
| related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(poset_of_lattice(sK1))) ),
inference(resolve,[status(thm)],[c_371,c_10443]) ).
cnf(c_10444,negated_conjecture,
( related(poset_of_lattice(sK1),A,B)
| ~ related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(poset_of_lattice(sK1)))
| ~ reflexive_relstr(poset_of_lattice(sK1)) ),
inference(resolve,[status(thm)],[c_375,c_349]) ).
cnf(c_545,negated_conjecture,
( related(poset_of_lattice(sK1),A,B)
| ~ related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(poset_of_lattice(sK1))) ),
inference(resolve,[status(thm)],[c_371,c_10444]) ).
cnf(c_546,negated_conjecture,
rel_str_of(the_carrier(poset_of_lattice(sK1)),the_InternalRel(poset_of_lattice(sK1))) = poset_of_lattice(sK1),
inference(resolve,[status(thm)],[c_373,c_341]) ).
cnf(c_10445,negated_conjecture,
( below(sK1,A,B)
| ~ below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ join_absorbing(sK1)
| ~ meet_absorbing(sK1) ),
inference(resolve,[status(thm)],[c_448,c_363]) ).
cnf(c_10446,negated_conjecture,
( below(sK1,A,B)
| ~ below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ join_absorbing(sK1) ),
inference(resolve,[status(thm)],[c_442,c_10445]) ).
cnf(c_558,negated_conjecture,
( below(sK1,A,B)
| ~ below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_439,c_10446]) ).
cnf(c_10447,negated_conjecture,
( ~ below(sK1,A,B)
| below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ join_absorbing(sK1)
| ~ meet_absorbing(sK1) ),
inference(resolve,[status(thm)],[c_448,c_361]) ).
cnf(c_10448,negated_conjecture,
( ~ below(sK1,A,B)
| below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ join_absorbing(sK1) ),
inference(resolve,[status(thm)],[c_442,c_10447]) ).
cnf(c_559,negated_conjecture,
( ~ below(sK1,A,B)
| below_refl(sK1,A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_439,c_10448]) ).
cnf(c_650,plain,
element(cast_to_el_of_LattPOSet(sK1,sK3),the_carrier(poset_of_lattice(sK1))),
inference(resolve,[status(thm)],[c_403,c_298]) ).
cnf(c_656,plain,
cast_to_el_of_LattPOSet(sK1,sK3) = sK3,
inference(resolve,[status(thm)],[c_418,c_298]) ).
cnf(c_658,plain,
element(sK3,the_carrier(poset_of_lattice(sK1))),
inference(paramod,[status(thm)],[c_656,c_650]) ).
cnf(c_659,negated_conjecture,
( relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| latt_element_smaller(sK1,sK3,sK4) ),
inference(paramod,[status(thm)],[c_656,c_297]) ).
cnf(c_660,negated_conjecture,
( ~ relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| ~ latt_element_smaller(sK1,sK3,sK4) ),
inference(paramod,[status(thm)],[c_656,c_296]) ).
cnf(c_663,plain,
( in(sK2(sK1,sK3,A),A)
| latt_element_smaller(sK1,sK3,A) ),
inference(resolve,[status(thm)],[c_428,c_298]) ).
cnf(c_666,plain,
( element(sK2(sK1,sK3,A),the_carrier(sK1))
| latt_element_smaller(sK1,sK3,A) ),
inference(resolve,[status(thm)],[c_431,c_298]) ).
cnf(c_10449,negated_conjecture,
( A = the_carrier(sK1)
| rel_str_of(A,B) != rel_str_of(the_carrier(sK1),k2_lattice3(sK1)) ),
inference(resolve,[status(thm)],[c_514,c_322]) ).
cnf(c_10450,negated_conjecture,
( A = the_carrier(sK1)
| rel_str_of(A,B) != poset_of_lattice(sK1) ),
inference(paramod,[status(thm)],[c_422,c_10449]) ).
cnf(c_10451,negated_conjecture,
( A = the_carrier(sK1)
| poset_of_lattice(sK1) != rel_str_of(A,B) ),
inference(copy,[status(thm)],[c_10450]) ).
cnf(c_679,negated_conjecture,
( the_carrier(sK1) = A
| poset_of_lattice(sK1) != rel_str_of(A,B) ),
inference(copy,[status(thm)],[c_10451]) ).
cnf(c_10452,plain,
( ~ related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,A),sK3)
| below_refl(sK1,A,sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_656,c_355]) ).
cnf(c_709,negated_conjecture,
( ~ related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,A),sK3)
| below_refl(sK1,A,sK3)
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10452]) ).
cnf(c_10453,negated_conjecture,
( below(sK1,A,sK3)
| ~ in(A,sK4)
| ~ element(A,the_carrier(sK1))
| ~ element(sK3,the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_659,c_434]) ).
cnf(c_737,negated_conjecture,
( below(sK1,A,sK3)
| ~ in(A,sK4)
| ~ element(A,the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_298,c_10453]) ).
cnf(c_739,plain,
( element(sK0(poset_of_lattice(sK1),A,sK3),the_carrier(poset_of_lattice(sK1)))
| relstr_set_smaller(poset_of_lattice(sK1),A,sK3) ),
inference(resolve,[status(thm)],[c_658,c_337]) ).
cnf(c_740,plain,
( in(sK0(poset_of_lattice(sK1),A,sK3),A)
| relstr_set_smaller(poset_of_lattice(sK1),A,sK3) ),
inference(resolve,[status(thm)],[c_658,c_335]) ).
cnf(c_742,plain,
( ~ relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_663,c_660]) ).
cnf(c_10454,negated_conjecture,
( below(sK1,B,sK3)
| ~ in(B,A)
| ~ element(B,the_carrier(sK1))
| ~ element(sK3,the_carrier(sK1))
| in(sK2(sK1,sK3,A),A) ),
inference(resolve,[status(thm)],[c_663,c_434]) ).
cnf(c_743,negated_conjecture,
( below(sK1,B,sK3)
| ~ in(B,A)
| ~ element(B,the_carrier(sK1))
| in(sK2(sK1,sK3,A),A) ),
inference(resolve,[status(thm)],[c_298,c_10454]) ).
cnf(c_10455,negated_conjecture,
poset_of_lattice(sK1) = rel_str_of(the_carrier(poset_of_lattice(sK1)),the_InternalRel(poset_of_lattice(sK1))),
inference(copy,[status(thm)],[c_546]) ).
cnf(c_10456,negated_conjecture,
the_carrier(sK1) = the_carrier(poset_of_lattice(sK1)),
inference(resolve,[status(thm)],[c_679,c_10455]) ).
cnf(c_744,negated_conjecture,
the_carrier(poset_of_lattice(sK1)) = the_carrier(sK1),
inference(copy,[status(thm)],[c_10456]) ).
cnf(c_745,plain,
( element(sK0(poset_of_lattice(sK1),A,sK3),the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),A,sK3) ),
inference(paramod,[status(thm)],[c_744,c_739]) ).
cnf(c_10457,negated_conjecture,
( related(poset_of_lattice(sK1),A,B)
| ~ related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_744,c_545]) ).
cnf(c_754,negated_conjecture,
( related(poset_of_lattice(sK1),A,B)
| ~ related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_744,c_10457]) ).
cnf(c_10458,negated_conjecture,
( ~ related(poset_of_lattice(sK1),A,B)
| related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(poset_of_lattice(sK1)))
| ~ element(A,the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_744,c_544]) ).
cnf(c_755,negated_conjecture,
( ~ related(poset_of_lattice(sK1),A,B)
| related_reflexive(poset_of_lattice(sK1),A,B)
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_744,c_10458]) ).
cnf(c_10459,negated_conjecture,
( related(poset_of_lattice(sK1),C,A)
| ~ in(C,B)
| ~ element(C,the_carrier(poset_of_lattice(sK1)))
| ~ relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_744,c_339]) ).
cnf(c_766,negated_conjecture,
( related(poset_of_lattice(sK1),C,A)
| ~ in(C,B)
| ~ element(C,the_carrier(sK1))
| ~ relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_744,c_10459]) ).
cnf(c_769,negated_conjecture,
( ~ related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),B,A),A)
| relstr_set_smaller(poset_of_lattice(sK1),B,A)
| ~ element(A,the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_744,c_333]) ).
cnf(c_794,plain,
( ~ relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_666,c_660]) ).
cnf(c_10460,negated_conjecture,
( below(sK1,B,sK3)
| ~ in(B,A)
| ~ element(B,the_carrier(sK1))
| ~ element(sK3,the_carrier(sK1))
| element(sK2(sK1,sK3,A),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_666,c_434]) ).
cnf(c_795,negated_conjecture,
( below(sK1,B,sK3)
| ~ in(B,A)
| ~ element(B,the_carrier(sK1))
| element(sK2(sK1,sK3,A),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10460]) ).
cnf(c_980,plain,
( element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_740,c_794]) ).
cnf(c_981,plain,
( in(sK2(sK1,sK3,sK4),sK4)
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_740,c_742]) ).
cnf(c_1082,plain,
( element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_745,c_794]) ).
cnf(c_1083,plain,
( in(sK2(sK1,sK3,sK4),sK4)
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_745,c_742]) ).
cnf(c_10461,plain,
( below(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4)
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_981,c_743]) ).
cnf(c_1113,plain,
( below(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(copy,[status(thm)],[c_10461]) ).
cnf(c_10462,negated_conjecture,
( element(sK0(poset_of_lattice(sK1),B,sK3),the_carrier(sK1))
| related(poset_of_lattice(sK1),A,sK3)
| ~ in(A,B)
| ~ element(A,the_carrier(sK1))
| ~ element(sK3,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_766,c_745]) ).
cnf(c_1159,negated_conjecture,
( element(sK0(poset_of_lattice(sK1),B,sK3),the_carrier(sK1))
| related(poset_of_lattice(sK1),A,sK3)
| ~ in(A,B)
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10462]) ).
cnf(c_10463,negated_conjecture,
( in(sK0(poset_of_lattice(sK1),B,sK3),B)
| related(poset_of_lattice(sK1),A,sK3)
| ~ in(A,B)
| ~ element(A,the_carrier(sK1))
| ~ element(sK3,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_766,c_740]) ).
cnf(c_1160,negated_conjecture,
( in(sK0(poset_of_lattice(sK1),B,sK3),B)
| related(poset_of_lattice(sK1),A,sK3)
| ~ in(A,B)
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10463]) ).
cnf(c_10464,plain,
( below(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_980,c_795]) ).
cnf(c_1191,plain,
( below(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(copy,[status(thm)],[c_10464]) ).
cnf(c_1401,plain,
( cast_to_el_of_LattPOSet(sK1,sK0(poset_of_lattice(sK1),sK4,sK3)) = sK0(poset_of_lattice(sK1),sK4,sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_1082,c_418]) ).
cnf(c_10465,plain,
( element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| related(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_1159,c_1083]) ).
cnf(c_1947,plain,
( element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| related(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(copy,[status(thm)],[c_10465]) ).
cnf(c_10466,plain,
( element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| below(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_1191,c_1082]) ).
cnf(c_2607,plain,
( below(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(copy,[status(thm)],[c_10466]) ).
cnf(c_10467,negated_conjecture,
( below_refl(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_2607,c_559]) ).
cnf(c_2608,negated_conjecture,
( below_refl(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10467]) ).
cnf(c_10468,plain,
( element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| below_refl(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_2608,c_1082]) ).
cnf(c_2940,plain,
( below_refl(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(copy,[status(thm)],[c_10468]) ).
cnf(c_10469,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,sK0(poset_of_lattice(sK1),sK4,sK3)),cast_to_el_of_LattPOSet(sK1,sK3))
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_2940,c_357]) ).
cnf(c_10470,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,sK0(poset_of_lattice(sK1),sK4,sK3)),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_656,c_10469]) ).
cnf(c_2941,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,sK0(poset_of_lattice(sK1),sK4,sK3)),sK3)
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10470]) ).
cnf(c_10471,plain,
( element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,sK0(poset_of_lattice(sK1),sK4,sK3)),sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_2941,c_1082]) ).
cnf(c_9466,plain,
( related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,sK0(poset_of_lattice(sK1),sK4,sK3)),sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(copy,[status(thm)],[c_10471]) ).
cnf(c_10472,plain,
( related_reflexive(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_1401,c_9466]) ).
cnf(c_9469,plain,
( related_reflexive(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(copy,[status(thm)],[c_10472]) ).
cnf(c_10473,negated_conjecture,
( related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9469,c_754]) ).
cnf(c_9470,negated_conjecture,
( related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10473]) ).
cnf(c_10474,plain,
( element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9470,c_1082]) ).
cnf(c_9473,plain,
( related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(copy,[status(thm)],[c_10474]) ).
cnf(c_10475,negated_conjecture,
( relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| ~ element(sK3,the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9473,c_769]) ).
cnf(c_9474,negated_conjecture,
( relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10475]) ).
cnf(c_10476,plain,
( element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9474,c_794]) ).
cnf(c_9475,plain,
element(sK2(sK1,sK3,sK4),the_carrier(sK1)),
inference(copy,[status(thm)],[c_10476]) ).
cnf(c_9560,plain,
( element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| related(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3) ),
inference(resolve,[status(thm)],[c_9475,c_1947]) ).
cnf(c_9594,plain,
cast_to_el_of_LattPOSet(sK1,sK2(sK1,sK3,sK4)) = sK2(sK1,sK3,sK4),
inference(resolve,[status(thm)],[c_9475,c_418]) ).
cnf(c_10477,plain,
( ~ related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| below_refl(sK1,sK2(sK1,sK3,sK4),sK3)
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(paramod,[status(thm)],[c_9594,c_709]) ).
cnf(c_9633,plain,
( ~ related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| below_refl(sK1,sK2(sK1,sK3,sK4),sK3) ),
inference(resolve,[status(thm)],[c_9475,c_10477]) ).
cnf(c_10478,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9560,c_755]) ).
cnf(c_10479,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1))
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9475,c_10478]) ).
cnf(c_9854,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10479]) ).
cnf(c_9932,plain,
( below_refl(sK1,sK2(sK1,sK3,sK4),sK3)
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9854,c_9633]) ).
cnf(c_10480,negated_conjecture,
( below(sK1,sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9932,c_558]) ).
cnf(c_10481,negated_conjecture,
( below(sK1,sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1))
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9475,c_10480]) ).
cnf(c_9933,negated_conjecture,
( below(sK1,sK2(sK1,sK3,sK4),sK3)
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10481]) ).
cnf(c_10482,negated_conjecture,
( latt_element_smaller(sK1,sK3,sK4)
| ~ element(sK3,the_carrier(sK1))
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9933,c_425]) ).
cnf(c_9934,negated_conjecture,
( latt_element_smaller(sK1,sK3,sK4)
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10482]) ).
cnf(c_9935,plain,
( ~ relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9934,c_660]) ).
cnf(c_10483,plain,
( element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9935,c_745]) ).
cnf(c_9938,plain,
element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1)),
inference(copy,[status(thm)],[c_10483]) ).
cnf(c_10034,plain,
( below(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_9938,c_1113]) ).
cnf(c_10066,plain,
cast_to_el_of_LattPOSet(sK1,sK0(poset_of_lattice(sK1),sK4,sK3)) = sK0(poset_of_lattice(sK1),sK4,sK3),
inference(resolve,[status(thm)],[c_9938,c_418]) ).
cnf(c_10484,negated_conjecture,
( below_refl(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_10034,c_559]) ).
cnf(c_10485,negated_conjecture,
( below_refl(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_9938,c_10484]) ).
cnf(c_10103,negated_conjecture,
( below_refl(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_298,c_10485]) ).
cnf(c_10486,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,sK0(poset_of_lattice(sK1),sK4,sK3)),cast_to_el_of_LattPOSet(sK1,sK3))
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_10103,c_357]) ).
cnf(c_10487,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),cast_to_el_of_LattPOSet(sK1,sK3))
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(paramod,[status(thm)],[c_10066,c_10486]) ).
cnf(c_10488,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(paramod,[status(thm)],[c_656,c_10487]) ).
cnf(c_10489,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_9938,c_10488]) ).
cnf(c_10107,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_298,c_10489]) ).
cnf(c_10490,negated_conjecture,
( related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_10107,c_754]) ).
cnf(c_10491,negated_conjecture,
( related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_9938,c_10490]) ).
cnf(c_10108,negated_conjecture,
( related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_298,c_10491]) ).
cnf(c_10492,negated_conjecture,
( relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| ~ element(sK3,the_carrier(sK1))
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_10108,c_769]) ).
cnf(c_10109,negated_conjecture,
( relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_298,c_10492]) ).
cnf(c_10493,plain,
( in(sK2(sK1,sK3,sK4),sK4)
| in(sK2(sK1,sK3,sK4),sK4) ),
inference(resolve,[status(thm)],[c_10109,c_742]) ).
cnf(c_10113,plain,
in(sK2(sK1,sK3,sK4),sK4),
inference(copy,[status(thm)],[c_10493]) ).
cnf(c_10494,plain,
( in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4)
| related(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_10113,c_1160]) ).
cnf(c_10125,plain,
( in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4)
| related(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3) ),
inference(resolve,[status(thm)],[c_9475,c_10494]) ).
cnf(c_10495,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_10125,c_755]) ).
cnf(c_10496,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1))
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_9475,c_10495]) ).
cnf(c_10356,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_298,c_10496]) ).
cnf(c_10357,plain,
( below_refl(sK1,sK2(sK1,sK3,sK4),sK3)
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_10356,c_9633]) ).
cnf(c_10497,negated_conjecture,
( below(sK1,sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1))
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_10357,c_558]) ).
cnf(c_10498,negated_conjecture,
( below(sK1,sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1))
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_9475,c_10497]) ).
cnf(c_10358,negated_conjecture,
( below(sK1,sK2(sK1,sK3,sK4),sK3)
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_298,c_10498]) ).
cnf(c_10499,negated_conjecture,
( latt_element_smaller(sK1,sK3,sK4)
| ~ element(sK3,the_carrier(sK1))
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_10358,c_425]) ).
cnf(c_10359,negated_conjecture,
( latt_element_smaller(sK1,sK3,sK4)
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_298,c_10499]) ).
cnf(c_10360,plain,
( ~ relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_10359,c_660]) ).
cnf(c_10500,plain,
( in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4)
| in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4) ),
inference(resolve,[status(thm)],[c_10360,c_740]) ).
cnf(c_10362,plain,
in(sK0(poset_of_lattice(sK1),sK4,sK3),sK4),
inference(copy,[status(thm)],[c_10500]) ).
cnf(c_10501,plain,
( below(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_10362,c_737]) ).
cnf(c_10388,plain,
( below(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_9938,c_10501]) ).
cnf(c_10502,negated_conjecture,
( below_refl(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_10388,c_559]) ).
cnf(c_10503,negated_conjecture,
( below_refl(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_9938,c_10502]) ).
cnf(c_10402,negated_conjecture,
( below_refl(sK1,sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_298,c_10503]) ).
cnf(c_10504,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),cast_to_el_of_LattPOSet(sK1,sK0(poset_of_lattice(sK1),sK4,sK3)),cast_to_el_of_LattPOSet(sK1,sK3))
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_10402,c_357]) ).
cnf(c_10505,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),cast_to_el_of_LattPOSet(sK1,sK3))
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(paramod,[status(thm)],[c_10066,c_10504]) ).
cnf(c_10506,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(paramod,[status(thm)],[c_656,c_10505]) ).
cnf(c_10507,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_9938,c_10506]) ).
cnf(c_10403,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_298,c_10507]) ).
cnf(c_10508,negated_conjecture,
( related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK0(poset_of_lattice(sK1),sK4,sK3),the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_10403,c_754]) ).
cnf(c_10509,negated_conjecture,
( related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| ~ element(sK3,the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_9938,c_10508]) ).
cnf(c_10404,negated_conjecture,
( related(poset_of_lattice(sK1),sK0(poset_of_lattice(sK1),sK4,sK3),sK3)
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_298,c_10509]) ).
cnf(c_10510,negated_conjecture,
( relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3)
| ~ element(sK3,the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(resolve,[status(thm)],[c_10404,c_769]) ).
cnf(c_10511,negated_conjecture,
( ~ element(sK3,the_carrier(sK1))
| relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3) ),
inference(copy,[status(thm)],[c_10510]) ).
cnf(c_10405,negated_conjecture,
relstr_set_smaller(poset_of_lattice(sK1),sK4,sK3),
inference(resolve,[status(thm)],[c_298,c_10511]) ).
cnf(c_10408,negated_conjecture,
~ latt_element_smaller(sK1,sK3,sK4),
inference(resolve,[status(thm)],[c_10405,c_660]) ).
cnf(c_10512,negated_conjecture,
( related(poset_of_lattice(sK1),A,sK3)
| ~ in(A,sK4)
| ~ element(A,the_carrier(sK1))
| ~ element(sK3,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_10405,c_766]) ).
cnf(c_10409,negated_conjecture,
( related(poset_of_lattice(sK1),A,sK3)
| ~ in(A,sK4)
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_298,c_10512]) ).
cnf(c_10513,plain,
( related(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_10409,c_10113]) ).
cnf(c_10411,plain,
related(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3),
inference(resolve,[status(thm)],[c_9475,c_10513]) ).
cnf(c_10514,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_10411,c_755]) ).
cnf(c_10515,negated_conjecture,
( related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9475,c_10514]) ).
cnf(c_10419,negated_conjecture,
related_reflexive(poset_of_lattice(sK1),sK2(sK1,sK3,sK4),sK3),
inference(resolve,[status(thm)],[c_298,c_10515]) ).
cnf(c_10420,plain,
below_refl(sK1,sK2(sK1,sK3,sK4),sK3),
inference(resolve,[status(thm)],[c_10419,c_9633]) ).
cnf(c_10516,negated_conjecture,
( below(sK1,sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1))
| ~ element(sK2(sK1,sK3,sK4),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_10420,c_558]) ).
cnf(c_10517,negated_conjecture,
( below(sK1,sK2(sK1,sK3,sK4),sK3)
| ~ element(sK3,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_9475,c_10516]) ).
cnf(c_10421,negated_conjecture,
below(sK1,sK2(sK1,sK3,sK4),sK3),
inference(resolve,[status(thm)],[c_298,c_10517]) ).
cnf(c_10518,negated_conjecture,
( latt_element_smaller(sK1,sK3,sK4)
| ~ element(sK3,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_10421,c_425]) ).
cnf(c_10519,negated_conjecture,
latt_element_smaller(sK1,sK3,sK4),
inference(resolve,[status(thm)],[c_298,c_10518]) ).
cnf(c_10422,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_10408,c_10519]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU349+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 09:17:16 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 2755302 was started by sandbox2 on n014,
% 0.08/0.35 % Sat Sep 26 09:17:16 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.37
% 0.12/0.37 % From the command line: assign(max_seconds, 300).
% 156.69/21.40
% 156.69/21.40 % given #500 (T,wt=28): 853 rel_str_of(A,f5(A,A)) != c6 | f5(A,A) = the_InternalRel(c6). [para(530(a,1),603(a,2))].
% 156.69/21.40
% 156.69/21.40 % given #1000 (W,wt=38): 3320 in(f1(c12,f4(the_carrier(c12)),the_carrier(c12)),the_carrier(c12)) | below(c12,f4(f8(c12)),f4(the_carrier(c12))). [resolve(1084,c,826,a),unit_del(b,779)].
% 156.69/21.40
% 156.69/21.40 % given #1500 (T,wt=43): 2249 element(f1(c12,c13,c11),c11) | related_reflexive(poset_of_lattice(c12),cast_to_el_of_lattice(c12,f2(poset_of_lattice(c12),c11,c13)),cast_to_el_of_lattice(c12,f2(poset_of_lattice(c12),c11,c13))). [resolve(1251,b,757,a)].
% 156.69/21.40
% 156.69/21.40 % given #2000 (T,wt=45): 4711 element(f1(c12,f4(f8(c12)),powerset(f4(the_carrier(c12)))),the_carrier(c12)) | below(c12,f4(the_carrier(c12)),f4(f8(c12))). [resolve(4665,b,328,a)].
% 156.69/21.40
% 156.69/21.40 % SZS status Theorem for theBenchmark
% 156.69/21.40
% 156.69/21.40 % Proof 1 at 4.16 (+ 0.52) seconds.
% 156.69/21.40 % Length of proof is 190.
% 156.69/21.40 % Level of proof is 49.
% 156.69/21.40 % Maximum clause weight is 46.000.
% 156.69/21.40 % Given clauses 2264.
% 156.69/21.40
% 156.69/21.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------