%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU346+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:52 AM UTC 2026
% Result : Theorem 90.35s 12.99s
% Output : CNFRefutation 90.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 19
% Syntax : Number of formulae : 184 ( 36 unt; 0 def)
% Number of atoms : 666 ( 67 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 813 ( 331 ~; 392 |; 55 &)
% ( 6 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-4 aty)
% Number of variables : 140 ( 10 sgn 41 !; 3 ?)
% 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(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(d5_tarski,axiom,
! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
file('theBenchmark.p',d5_tarski) ).
fof(d9_orders_2,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( related(A,B,C)
<=> in(ordered_pair(B,C),the_InternalRel(A)) ) ) ) ),
file('theBenchmark.p',d9_orders_2) ).
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(dt_l2_lattices,axiom,
! [A] :
( join_semilatt_str(A)
=> one_sorted_str(A) ),
file('theBenchmark.p',dt_l2_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( latt_str(A)
=> ( join_semilatt_str(A)
& meet_semilatt_str(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(fc1_struct_0,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ~ empty(the_carrier(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
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_k1_domain_1,axiom,
! [A,B,C,D] :
( ( element(D,B)
& element(C,A)
& ~ empty(B)
& ~ empty(A) )
=> ordered_pair_as_product_element(A,B,C,D) = ordered_pair(C,D) ),
file('theBenchmark.p',redefinition_k1_domain_1) ).
fof(redefinition_k2_lattice3,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> k2_lattice3(A) = relation_of_lattice(A) ),
file('theBenchmark.p',redefinition_k2_lattice3) ).
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_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(t32_filter_1,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ( in(ordered_pair_as_product_element(the_carrier(A),the_carrier(A),B,C),relation_of_lattice(A))
<=> below_refl(A,B,C) ) ) ) ),
file('theBenchmark.p',t32_filter_1) ).
fof(t7_lattice3,conjecture,
! [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(t7_lattice3_neg,negated_conjecture,
~ ! [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)) ) ) ) ),
inference(assume_negation,[status(cth)],[t7_lattice3]) ).
cnf(c_94,plain,
( ~ in(ordered_pair(B,C),the_InternalRel(A))
| related(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(clausify,[status(thm)],[d9_orders_2]) ).
cnf(c_95,plain,
( in(ordered_pair(B,C),the_InternalRel(A))
| ~ related(A,B,C)
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ rel_str(A) ),
inference(clausify,[status(thm)],[d9_orders_2]) ).
cnf(c_96,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_97,plain,
( rel_str(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[dt_k3_lattice3]) ).
cnf(c_108,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_109,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_161,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_165,plain,
( relation_of2(A,B,C)
| ~ relation_of2_as_subset(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_180,plain,
( ~ empty(the_carrier(A))
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
cnf(c_182,plain,
( one_sorted_str(A)
| ~ join_semilatt_str(A) ),
inference(clausify,[status(thm)],[dt_l2_lattices]) ).
cnf(c_199,plain,
( ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A)
| relation_of2(k2_lattice3(A),the_carrier(A),the_carrier(A)) ),
inference(resolve,[status(thm)],[c_165,c_161]) ).
cnf(c_240,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_109,c_97]) ).
cnf(c_245,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_108,c_97]) ).
cnf(c_273,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_97,c_96]) ).
cnf(c_274,plain,
( in(ordered_pair(B,C),the_InternalRel(poset_of_lattice(A)))
| ~ related(poset_of_lattice(A),B,C)
| ~ element(C,the_carrier(poset_of_lattice(A)))
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(resolve,[status(thm)],[c_97,c_95]) ).
cnf(c_275,plain,
( ~ in(ordered_pair(B,C),the_InternalRel(poset_of_lattice(A)))
| related(poset_of_lattice(A),B,C)
| ~ element(C,the_carrier(poset_of_lattice(A)))
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(resolve,[status(thm)],[c_97,c_94]) ).
fof(nnf_92,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ 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) )
& ( 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(fof_nnf,[status(thm)],[t7_lattice3_neg]) ).
fof(sk_t7_lattice3_neg,plain,
( ( ~ related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| ~ below_refl(sK0,sK1,sK2) )
& ( related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| below_refl(sK0,sK1,sK2) )
& element(sK2,the_carrier(sK0))
& element(sK1,the_carrier(sK0))
& latt_str(sK0)
& lattice(sK0)
& ~ empty_carrier(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2)],[nnf_92]) ).
cnf(c_279,negated_conjecture,
( ~ related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| ~ below_refl(sK0,sK1,sK2) ),
inference(split_conjunct,[status(thm)],[sk_t7_lattice3_neg]) ).
cnf(c_280,negated_conjecture,
( related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| below_refl(sK0,sK1,sK2) ),
inference(split_conjunct,[status(thm)],[sk_t7_lattice3_neg]) ).
cnf(c_281,negated_conjecture,
element(sK2,the_carrier(sK0)),
inference(split_conjunct,[status(thm)],[sk_t7_lattice3_neg]) ).
cnf(c_282,negated_conjecture,
element(sK1,the_carrier(sK0)),
inference(split_conjunct,[status(thm)],[sk_t7_lattice3_neg]) ).
cnf(c_283,negated_conjecture,
latt_str(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_lattice3_neg]) ).
cnf(c_284,negated_conjecture,
lattice(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_lattice3_neg]) ).
cnf(c_285,negated_conjecture,
~ empty_carrier(sK0),
inference(split_conjunct,[status(thm)],[sk_t7_lattice3_neg]) ).
cnf(c_291,plain,
( ~ below_refl(A,B,C)
| in(ordered_pair_as_product_element(the_carrier(A),the_carrier(A),B,C),relation_of_lattice(A))
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[t32_filter_1]) ).
cnf(c_292,plain,
( below_refl(A,B,C)
| ~ in(ordered_pair_as_product_element(the_carrier(A),the_carrier(A),B,C),relation_of_lattice(A))
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[t32_filter_1]) ).
cnf(c_295,plain,
( relation_of_lattice(A) = k2_lattice3(A)
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[redefinition_k2_lattice3]) ).
cnf(c_296,plain,
( ordered_pair_as_product_element(A,B,C,D) = ordered_pair(C,D)
| ~ element(D,B)
| ~ element(C,A)
| empty(B)
| empty(A) ),
inference(clausify,[status(thm)],[redefinition_k1_domain_1]) ).
cnf(c_322,plain,
( D = A
| 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_323,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_327,plain,
( reflexive_relstr(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[fc4_lattice3]) ).
cnf(c_328,plain,
( strict_rel_str(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[fc4_lattice3]) ).
cnf(c_329,plain,
( ~ empty_carrier(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[fc4_lattice3]) ).
cnf(c_346,plain,
( join_semilatt_str(A)
| ~ latt_str(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_349,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_357,plain,
ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)),
inference(clausify,[status(thm)],[d5_tarski]) ).
cnf(c_358,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_359,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]) ).
cnf(c_360,plain,
( rel_str_of(the_carrier(A),k2_lattice3(A)) = poset_of_lattice(A)
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(copy,[status(thm)],[c_359]) ).
cnf(c_431,plain,
( ~ empty(the_carrier(A))
| empty_carrier(A)
| ~ join_semilatt_str(A) ),
inference(resolve,[status(thm)],[c_182,c_180]) ).
cnf(c_488,plain,
( ordered_pair_as_product_element(A,B,C,D) = unordered_pair(unordered_pair(C,D),singleton(C))
| ~ element(D,B)
| ~ element(C,A)
| empty(B)
| empty(A) ),
inference(paramod,[status(thm)],[c_357,c_296]) ).
cnf(c_491,plain,
( ~ in(unordered_pair(unordered_pair(B,C),singleton(B)),the_InternalRel(poset_of_lattice(A)))
| related(poset_of_lattice(A),B,C)
| ~ element(C,the_carrier(poset_of_lattice(A)))
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(paramod,[status(thm)],[c_357,c_275]) ).
cnf(c_492,plain,
( in(unordered_pair(unordered_pair(B,C),singleton(B)),the_InternalRel(poset_of_lattice(A)))
| ~ related(poset_of_lattice(A),B,C)
| ~ element(C,the_carrier(poset_of_lattice(A)))
| ~ element(B,the_carrier(poset_of_lattice(A)))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(paramod,[status(thm)],[c_357,c_274]) ).
cnf(c_24778,negated_conjecture,
( ~ latt_str(sK0)
| empty_carrier(sK0)
| relation_of2(k2_lattice3(sK0),the_carrier(sK0),the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_284,c_199]) ).
cnf(c_24779,negated_conjecture,
( ~ latt_str(sK0)
| relation_of2(k2_lattice3(sK0),the_carrier(sK0),the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_285,c_24778]) ).
cnf(c_519,negated_conjecture,
relation_of2(k2_lattice3(sK0),the_carrier(sK0),the_carrier(sK0)),
inference(resolve,[status(thm)],[c_283,c_24779]) ).
cnf(c_24780,negated_conjecture,
( related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),relation_of_lattice(sK0))
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_291,c_280]) ).
cnf(c_24781,negated_conjecture,
( related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),relation_of_lattice(sK0))
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24780]) ).
cnf(c_24782,negated_conjecture,
( related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),relation_of_lattice(sK0))
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_284,c_24781]) ).
cnf(c_24783,negated_conjecture,
( related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),relation_of_lattice(sK0))
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_283,c_24782]) ).
cnf(c_24784,negated_conjecture,
( related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),relation_of_lattice(sK0))
| ~ element(sK2,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_282,c_24783]) ).
cnf(c_522,negated_conjecture,
( related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),relation_of_lattice(sK0)) ),
inference(resolve,[status(thm)],[c_281,c_24784]) ).
cnf(c_24785,negated_conjecture,
( relation_of_lattice(sK0) = k2_lattice3(sK0)
| ~ latt_str(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_295,c_284]) ).
cnf(c_24786,negated_conjecture,
( relation_of_lattice(sK0) = k2_lattice3(sK0)
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24785]) ).
cnf(c_530,negated_conjecture,
relation_of_lattice(sK0) = k2_lattice3(sK0),
inference(resolve,[status(thm)],[c_283,c_24786]) ).
cnf(c_531,negated_conjecture,
( related_reflexive(poset_of_lattice(sK0),cast_to_el_of_LattPOSet(sK0,sK1),cast_to_el_of_LattPOSet(sK0,sK2))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(paramod,[status(thm)],[c_530,c_522]) ).
cnf(c_24787,negated_conjecture,
( reflexive_relstr(poset_of_lattice(sK0))
| ~ latt_str(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_327,c_284]) ).
cnf(c_24788,negated_conjecture,
( reflexive_relstr(poset_of_lattice(sK0))
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24787]) ).
cnf(c_554,negated_conjecture,
reflexive_relstr(poset_of_lattice(sK0)),
inference(resolve,[status(thm)],[c_283,c_24788]) ).
cnf(c_24789,negated_conjecture,
( strict_rel_str(poset_of_lattice(sK0))
| ~ latt_str(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_328,c_284]) ).
cnf(c_24790,negated_conjecture,
( strict_rel_str(poset_of_lattice(sK0))
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24789]) ).
cnf(c_556,negated_conjecture,
strict_rel_str(poset_of_lattice(sK0)),
inference(resolve,[status(thm)],[c_283,c_24790]) ).
cnf(c_24791,negated_conjecture,
( ~ empty_carrier(poset_of_lattice(sK0))
| ~ latt_str(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_329,c_284]) ).
cnf(c_24792,negated_conjecture,
( ~ empty_carrier(poset_of_lattice(sK0))
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24791]) ).
cnf(c_558,negated_conjecture,
~ empty_carrier(poset_of_lattice(sK0)),
inference(resolve,[status(thm)],[c_283,c_24792]) ).
cnf(c_587,plain,
join_semilatt_str(sK0),
inference(resolve,[status(thm)],[c_346,c_283]) ).
cnf(c_24793,negated_conjecture,
( element(cast_to_el_of_LattPOSet(sK0,sK1),the_carrier(poset_of_lattice(sK0)))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_349,c_282]) ).
cnf(c_24794,negated_conjecture,
( element(cast_to_el_of_LattPOSet(sK0,sK1),the_carrier(poset_of_lattice(sK0)))
| ~ latt_str(sK0)
| ~ lattice(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24793]) ).
cnf(c_24795,negated_conjecture,
( element(cast_to_el_of_LattPOSet(sK0,sK1),the_carrier(poset_of_lattice(sK0)))
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_284,c_24794]) ).
cnf(c_608,negated_conjecture,
element(cast_to_el_of_LattPOSet(sK0,sK1),the_carrier(poset_of_lattice(sK0))),
inference(resolve,[status(thm)],[c_283,c_24795]) ).
cnf(c_24796,negated_conjecture,
( element(cast_to_el_of_LattPOSet(sK0,sK2),the_carrier(poset_of_lattice(sK0)))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_349,c_281]) ).
cnf(c_24797,negated_conjecture,
( element(cast_to_el_of_LattPOSet(sK0,sK2),the_carrier(poset_of_lattice(sK0)))
| ~ latt_str(sK0)
| ~ lattice(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24796]) ).
cnf(c_24798,negated_conjecture,
( element(cast_to_el_of_LattPOSet(sK0,sK2),the_carrier(poset_of_lattice(sK0)))
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_284,c_24797]) ).
cnf(c_609,negated_conjecture,
element(cast_to_el_of_LattPOSet(sK0,sK2),the_carrier(poset_of_lattice(sK0))),
inference(resolve,[status(thm)],[c_283,c_24798]) ).
cnf(c_24799,negated_conjecture,
( cast_to_el_of_LattPOSet(sK0,sK1) = sK1
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_358,c_282]) ).
cnf(c_24800,negated_conjecture,
( cast_to_el_of_LattPOSet(sK0,sK1) = sK1
| ~ latt_str(sK0)
| ~ lattice(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24799]) ).
cnf(c_24801,negated_conjecture,
( cast_to_el_of_LattPOSet(sK0,sK1) = sK1
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_284,c_24800]) ).
cnf(c_657,negated_conjecture,
cast_to_el_of_LattPOSet(sK0,sK1) = sK1,
inference(resolve,[status(thm)],[c_283,c_24801]) ).
cnf(c_24802,negated_conjecture,
( cast_to_el_of_LattPOSet(sK0,sK2) = sK2
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_358,c_281]) ).
cnf(c_24803,negated_conjecture,
( cast_to_el_of_LattPOSet(sK0,sK2) = sK2
| ~ latt_str(sK0)
| ~ lattice(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24802]) ).
cnf(c_24804,negated_conjecture,
( cast_to_el_of_LattPOSet(sK0,sK2) = sK2
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_284,c_24803]) ).
cnf(c_658,negated_conjecture,
cast_to_el_of_LattPOSet(sK0,sK2) = sK2,
inference(resolve,[status(thm)],[c_283,c_24804]) ).
cnf(c_659,negated_conjecture,
element(sK1,the_carrier(poset_of_lattice(sK0))),
inference(paramod,[status(thm)],[c_657,c_608]) ).
cnf(c_24805,negated_conjecture,
( related_reflexive(poset_of_lattice(sK0),sK1,cast_to_el_of_LattPOSet(sK0,sK2))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(paramod,[status(thm)],[c_657,c_531]) ).
cnf(c_660,negated_conjecture,
( related_reflexive(poset_of_lattice(sK0),sK1,sK2)
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(paramod,[status(thm)],[c_658,c_24805]) ).
cnf(c_24806,negated_conjecture,
( ~ related_reflexive(poset_of_lattice(sK0),sK1,cast_to_el_of_LattPOSet(sK0,sK2))
| ~ below_refl(sK0,sK1,sK2) ),
inference(paramod,[status(thm)],[c_657,c_279]) ).
cnf(c_663,negated_conjecture,
( ~ related_reflexive(poset_of_lattice(sK0),sK1,sK2)
| ~ below_refl(sK0,sK1,sK2) ),
inference(paramod,[status(thm)],[c_658,c_24806]) ).
cnf(c_664,negated_conjecture,
element(sK2,the_carrier(poset_of_lattice(sK0))),
inference(paramod,[status(thm)],[c_658,c_609]) ).
cnf(c_24807,negated_conjecture,
( rel_str_of(the_carrier(sK0),k2_lattice3(sK0)) = poset_of_lattice(sK0)
| ~ latt_str(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_360,c_284]) ).
cnf(c_24808,negated_conjecture,
( rel_str_of(the_carrier(sK0),k2_lattice3(sK0)) = poset_of_lattice(sK0)
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24807]) ).
cnf(c_666,negated_conjecture,
rel_str_of(the_carrier(sK0),k2_lattice3(sK0)) = poset_of_lattice(sK0),
inference(resolve,[status(thm)],[c_283,c_24808]) ).
cnf(c_842,plain,
( ordered_pair_as_product_element(A,the_carrier(sK0),B,sK2) = unordered_pair(unordered_pair(B,sK2),singleton(B))
| ~ element(B,A)
| empty(the_carrier(sK0))
| empty(A) ),
inference(resolve,[status(thm)],[c_488,c_281]) ).
cnf(c_24809,plain,
( ~ empty(the_carrier(sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_587,c_431]) ).
cnf(c_909,negated_conjecture,
~ empty(the_carrier(sK0)),
inference(resolve,[status(thm)],[c_285,c_24809]) ).
cnf(c_915,plain,
( ordered_pair_as_product_element(A,the_carrier(sK0),B,sK2) = unordered_pair(unordered_pair(B,sK2),singleton(B))
| ~ element(B,A)
| empty(A) ),
inference(resolve,[status(thm)],[c_909,c_842]) ).
cnf(c_24810,plain,
( rel_str_of(the_carrier(poset_of_lattice(sK0)),the_InternalRel(poset_of_lattice(sK0))) = poset_of_lattice(sK0)
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_556,c_273]) ).
cnf(c_24811,negated_conjecture,
( rel_str_of(the_carrier(poset_of_lattice(sK0)),the_InternalRel(poset_of_lattice(sK0))) = poset_of_lattice(sK0)
| ~ latt_str(sK0)
| ~ lattice(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24810]) ).
cnf(c_24812,negated_conjecture,
( rel_str_of(the_carrier(poset_of_lattice(sK0)),the_InternalRel(poset_of_lattice(sK0))) = poset_of_lattice(sK0)
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_284,c_24811]) ).
cnf(c_985,negated_conjecture,
rel_str_of(the_carrier(poset_of_lattice(sK0)),the_InternalRel(poset_of_lattice(sK0))) = poset_of_lattice(sK0),
inference(resolve,[status(thm)],[c_283,c_24812]) ).
cnf(c_24813,plain,
( A = the_carrier(sK0)
| rel_str_of(A,B) != rel_str_of(the_carrier(sK0),k2_lattice3(sK0)) ),
inference(resolve,[status(thm)],[c_519,c_323]) ).
cnf(c_24814,plain,
( A = the_carrier(sK0)
| rel_str_of(A,B) != poset_of_lattice(sK0) ),
inference(paramod,[status(thm)],[c_666,c_24813]) ).
cnf(c_24815,plain,
( A = the_carrier(sK0)
| poset_of_lattice(sK0) != rel_str_of(A,B) ),
inference(copy,[status(thm)],[c_24814]) ).
cnf(c_1034,plain,
( the_carrier(sK0) = A
| poset_of_lattice(sK0) != rel_str_of(A,B) ),
inference(copy,[status(thm)],[c_24815]) ).
cnf(c_24816,plain,
( B = k2_lattice3(sK0)
| rel_str_of(A,B) != rel_str_of(the_carrier(sK0),k2_lattice3(sK0)) ),
inference(resolve,[status(thm)],[c_519,c_322]) ).
cnf(c_24817,plain,
( B = k2_lattice3(sK0)
| rel_str_of(A,B) != poset_of_lattice(sK0) ),
inference(paramod,[status(thm)],[c_666,c_24816]) ).
cnf(c_24818,plain,
( B = k2_lattice3(sK0)
| poset_of_lattice(sK0) != rel_str_of(A,B) ),
inference(copy,[status(thm)],[c_24817]) ).
cnf(c_1035,plain,
( k2_lattice3(sK0) = B
| poset_of_lattice(sK0) != rel_str_of(A,B) ),
inference(copy,[status(thm)],[c_24818]) ).
cnf(c_24819,plain,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(poset_of_lattice(sK0)))
| ~ element(sK1,the_carrier(poset_of_lattice(sK0)))
| ~ reflexive_relstr(poset_of_lattice(sK0))
| empty_carrier(poset_of_lattice(sK0))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(resolve,[status(thm)],[c_660,c_245]) ).
cnf(c_24820,plain,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(poset_of_lattice(sK0)))
| ~ element(sK1,the_carrier(poset_of_lattice(sK0)))
| ~ reflexive_relstr(poset_of_lattice(sK0))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(resolve,[status(thm)],[c_558,c_24819]) ).
cnf(c_24821,plain,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(poset_of_lattice(sK0)))
| ~ element(sK1,the_carrier(poset_of_lattice(sK0)))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(resolve,[status(thm)],[c_554,c_24820]) ).
cnf(c_24822,plain,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(poset_of_lattice(sK0)))
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(resolve,[status(thm)],[c_659,c_24821]) ).
cnf(c_24823,plain,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related(poset_of_lattice(sK0),sK1,sK2)
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(resolve,[status(thm)],[c_664,c_24822]) ).
cnf(c_24824,negated_conjecture,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| related(poset_of_lattice(sK0),sK1,sK2)
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(resolve,[status(thm)],[c_285,c_24823]) ).
cnf(c_24825,negated_conjecture,
( ~ latt_str(sK0)
| related(poset_of_lattice(sK0),sK1,sK2)
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(resolve,[status(thm)],[c_284,c_24824]) ).
cnf(c_3331,negated_conjecture,
( related(poset_of_lattice(sK0),sK1,sK2)
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),k2_lattice3(sK0)) ),
inference(resolve,[status(thm)],[c_283,c_24825]) ).
cnf(c_24826,plain,
poset_of_lattice(sK0) = rel_str_of(the_carrier(poset_of_lattice(sK0)),the_InternalRel(poset_of_lattice(sK0))),
inference(copy,[status(thm)],[c_985]) ).
cnf(c_24827,plain,
the_carrier(sK0) = the_carrier(poset_of_lattice(sK0)),
inference(resolve,[status(thm)],[c_1034,c_24826]) ).
cnf(c_4059,plain,
the_carrier(poset_of_lattice(sK0)) = the_carrier(sK0),
inference(copy,[status(thm)],[c_24827]) ).
cnf(c_4206,negated_conjecture,
rel_str_of(the_carrier(sK0),the_InternalRel(poset_of_lattice(sK0))) = poset_of_lattice(sK0),
inference(paramod,[status(thm)],[c_4059,c_985]) ).
cnf(c_24828,plain,
poset_of_lattice(sK0) = rel_str_of(the_carrier(sK0),the_InternalRel(poset_of_lattice(sK0))),
inference(copy,[status(thm)],[c_4206]) ).
cnf(c_4248,plain,
k2_lattice3(sK0) = the_InternalRel(poset_of_lattice(sK0)),
inference(resolve,[status(thm)],[c_1035,c_24828]) ).
cnf(c_4271,negated_conjecture,
( related(poset_of_lattice(sK0),sK1,sK2)
| in(ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2),the_InternalRel(poset_of_lattice(sK0))) ),
inference(paramod,[status(thm)],[c_4248,c_3331]) ).
cnf(c_4341,negated_conjecture,
relation_of_lattice(sK0) = the_InternalRel(poset_of_lattice(sK0)),
inference(paramod,[status(thm)],[c_4248,c_530]) ).
cnf(c_24829,negated_conjecture,
( ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2) = unordered_pair(unordered_pair(sK1,sK2),singleton(sK1))
| empty(the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_915,c_282]) ).
cnf(c_12677,negated_conjecture,
ordered_pair_as_product_element(the_carrier(sK0),the_carrier(sK0),sK1,sK2) = unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),
inference(resolve,[status(thm)],[c_909,c_24829]) ).
cnf(c_12679,negated_conjecture,
( related(poset_of_lattice(sK0),sK1,sK2)
| in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))) ),
inference(paramod,[status(thm)],[c_12677,c_4271]) ).
cnf(c_24830,plain,
( below_refl(sK0,sK1,sK2)
| ~ in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),relation_of_lattice(sK0))
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(paramod,[status(thm)],[c_12677,c_292]) ).
cnf(c_24831,plain,
( below_refl(sK0,sK1,sK2)
| ~ in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0)))
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(paramod,[status(thm)],[c_4341,c_24830]) ).
cnf(c_24832,negated_conjecture,
( below_refl(sK0,sK1,sK2)
| ~ in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0)))
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24831]) ).
cnf(c_24833,negated_conjecture,
( below_refl(sK0,sK1,sK2)
| ~ in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0)))
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_284,c_24832]) ).
cnf(c_24834,negated_conjecture,
( below_refl(sK0,sK1,sK2)
| ~ in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0)))
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_283,c_24833]) ).
cnf(c_24835,negated_conjecture,
( below_refl(sK0,sK1,sK2)
| ~ in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0)))
| ~ element(sK2,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_282,c_24834]) ).
cnf(c_24007,negated_conjecture,
( below_refl(sK0,sK1,sK2)
| ~ in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_281,c_24835]) ).
cnf(c_24836,plain,
( in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0)))
| ~ element(sK2,the_carrier(poset_of_lattice(sK0)))
| ~ element(sK1,the_carrier(poset_of_lattice(sK0)))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_12679,c_492]) ).
cnf(c_24837,plain,
( in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0)))
| ~ element(sK2,the_carrier(poset_of_lattice(sK0)))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))) ),
inference(paramod,[status(thm)],[c_4059,c_24836]) ).
cnf(c_24838,plain,
( in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0)))
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))) ),
inference(paramod,[status(thm)],[c_4059,c_24837]) ).
cnf(c_24839,plain,
( ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))) ),
inference(copy,[status(thm)],[c_24838]) ).
cnf(c_24840,negated_conjecture,
( ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_285,c_24839]) ).
cnf(c_24841,negated_conjecture,
( ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_284,c_24840]) ).
cnf(c_24842,negated_conjecture,
( ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_283,c_24841]) ).
cnf(c_24843,negated_conjecture,
( ~ element(sK2,the_carrier(sK0))
| in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_282,c_24842]) ).
cnf(c_24769,negated_conjecture,
in(unordered_pair(unordered_pair(sK1,sK2),singleton(sK1)),the_InternalRel(poset_of_lattice(sK0))),
inference(resolve,[status(thm)],[c_281,c_24843]) ).
cnf(c_24770,negated_conjecture,
below_refl(sK0,sK1,sK2),
inference(resolve,[status(thm)],[c_24769,c_24007]) ).
cnf(c_24771,negated_conjecture,
~ related_reflexive(poset_of_lattice(sK0),sK1,sK2),
inference(resolve,[status(thm)],[c_24770,c_663]) ).
cnf(c_24844,plain,
( related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(poset_of_lattice(sK0)))
| ~ element(sK1,the_carrier(poset_of_lattice(sK0)))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_24769,c_491]) ).
cnf(c_24845,plain,
( related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(poset_of_lattice(sK0)))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(paramod,[status(thm)],[c_4059,c_24844]) ).
cnf(c_24846,plain,
( related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(paramod,[status(thm)],[c_4059,c_24845]) ).
cnf(c_24847,negated_conjecture,
( related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0)
| ~ lattice(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24846]) ).
cnf(c_24848,negated_conjecture,
( related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ latt_str(sK0) ),
inference(resolve,[status(thm)],[c_284,c_24847]) ).
cnf(c_24849,negated_conjecture,
( related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_283,c_24848]) ).
cnf(c_24850,negated_conjecture,
( related(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_282,c_24849]) ).
cnf(c_24773,negated_conjecture,
related(poset_of_lattice(sK0),sK1,sK2),
inference(resolve,[status(thm)],[c_281,c_24850]) ).
cnf(c_24851,plain,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related_reflexive(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(poset_of_lattice(sK0)))
| ~ element(sK1,the_carrier(poset_of_lattice(sK0)))
| ~ reflexive_relstr(poset_of_lattice(sK0))
| empty_carrier(poset_of_lattice(sK0)) ),
inference(resolve,[status(thm)],[c_24773,c_240]) ).
cnf(c_24852,plain,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related_reflexive(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(poset_of_lattice(sK0)))
| ~ element(sK1,the_carrier(sK0))
| ~ reflexive_relstr(poset_of_lattice(sK0))
| empty_carrier(poset_of_lattice(sK0)) ),
inference(paramod,[status(thm)],[c_4059,c_24851]) ).
cnf(c_24853,plain,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related_reflexive(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ reflexive_relstr(poset_of_lattice(sK0))
| empty_carrier(poset_of_lattice(sK0)) ),
inference(paramod,[status(thm)],[c_4059,c_24852]) ).
cnf(c_24854,plain,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related_reflexive(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0))
| ~ reflexive_relstr(poset_of_lattice(sK0)) ),
inference(resolve,[status(thm)],[c_558,c_24853]) ).
cnf(c_24855,plain,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related_reflexive(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(sK0))
| ~ element(sK1,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_554,c_24854]) ).
cnf(c_24856,negated_conjecture,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related_reflexive(poset_of_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(sK0)) ),
inference(resolve,[status(thm)],[c_282,c_24855]) ).
cnf(c_24857,negated_conjecture,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0)
| related_reflexive(poset_of_lattice(sK0),sK1,sK2) ),
inference(resolve,[status(thm)],[c_281,c_24856]) ).
cnf(c_24858,negated_conjecture,
( ~ latt_str(sK0)
| ~ lattice(sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_24771,c_24857]) ).
cnf(c_24859,negated_conjecture,
( ~ latt_str(sK0)
| ~ lattice(sK0) ),
inference(resolve,[status(thm)],[c_285,c_24858]) ).
cnf(c_24860,negated_conjecture,
~ latt_str(sK0),
inference(resolve,[status(thm)],[c_284,c_24859]) ).
cnf(c_24777,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_283,c_24860]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU346+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n011.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sat Sep 26 09:16:29 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.43 % Process 163749 was started by sandbox on n011,
% 0.17/0.43 % Sat Sep 26 09:16:29 2026
% 0.17/0.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.17/0.47
% 0.17/0.47 % From the command line: assign(max_seconds, 300).
% 90.35/12.99
% 90.35/12.99 % given #500 (A,wt=10): 579 quasi_total(the_L_join(c4),cartesian_product2(the_carrier(c4),the_carrier(c4)),the_carrier(c4)). [resolve(342,a,340,a)].
% 90.35/12.99
% 90.35/12.99 % given #1000 (A,wt=19): 750 empty(A) | ordered_pair_as_product_element(A,A,f2(A),f2(A)) = unordered_pair(unordered_pair(f2(A),f2(A)),singleton(f2(A))). [resolve(464,b,337,a)].
% 90.35/12.99
% 90.35/12.99 % given #1500 (T,wt=11): 8146 empty_carrier(k8_filter_1(c12,c13)) | function(the_L_meet(k8_filter_1(k8_filter_1(c12,c13),c13))). [resolve(5967,b,345,a)].
% 90.35/12.99
% 90.35/12.99 % given #2000 (T,wt=12): 14303 empty_carrier(k8_filter_1(c10,c10)) | empty_carrier(c10) | meet_semilatt_str(k8_filter_1(c13,k8_filter_1(c10,c10))). [resolve(1418,b,347,a)].
% 90.35/12.99
% 90.35/12.99 % given #2500 (T,wt=13): 19407 empty_carrier(c10) | empty_carrier(k8_filter_1(c12,c10)) | function(the_L_join(k8_filter_1(c10,k8_filter_1(c12,c10)))). [resolve(14230,c,343,a)].
% 90.35/12.99
% 90.35/12.99 % given #3000 (T,wt=14): 3413 empty_carrier(A) | -latt_str(A) | latt_str(k8_filter_1(A,latt_str_of(the_carrier(c12),the_L_join(c12),the_L_join(c12)))). [resolve(3384,a,348,d),unit_del(c,3385)].
% 90.35/12.99
% 90.35/12.99 % given #3500 (T,wt=15): 2121 empty(A) | element(ordered_pair_as_product_element(powerset(A),A,f4(A),f2(A)),cartesian_product2(powerset(A),A)). [factor(2112,a,c)].
% 90.35/12.99
% 90.35/12.99 % SZS status Theorem for theBenchmark
% 90.35/12.99
% 90.35/12.99 % Proof 1 at 10.23 (+ 2.12) seconds.
% 90.35/12.99 % Length of proof is 98.
% 90.35/12.99 % Level of proof is 13.
% 90.35/12.99 % Maximum clause weight is 32.000.
% 90.35/12.99 % Given clauses 3587.
% 90.35/12.99
% 90.35/12.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------