%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU369+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 : n018.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:46:06 AM UTC 2026
% Result : Theorem 57.31s 7.61s
% Output : CNFRefutation 57.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 14
% Syntax : Number of formulae : 117 ( 29 unt; 0 def)
% Number of atoms : 393 ( 38 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 464 ( 188 ~; 204 |; 47 &)
% ( 6 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 35 ( 33 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-2 aty)
% Number of variables : 161 ( 12 sgn 31 !; 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(d2_yellow_1,axiom,
! [A] : boole_POSet(A) = poset_of_lattice(boole_lattice(A)),
file('theBenchmark.p',d2_yellow_1) ).
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(dt_k1_lattice3,axiom,
! [A] :
( latt_str(boole_lattice(A))
& strict_latt_str(boole_lattice(A)) ),
file('theBenchmark.p',dt_k1_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(fc3_lattice3,axiom,
! [A] :
( boolean_lattstr(boole_lattice(A))
& complemented_lattstr(boole_lattice(A))
& bounded_lattstr(boole_lattice(A))
& upper_bounded_semilattstr(boole_lattice(A))
& lower_bounded_semilattstr(boole_lattice(A))
& modular_lattstr(boole_lattice(A))
& distributive_lattstr(boole_lattice(A))
& lattice(boole_lattice(A))
& join_absorbing(boole_lattice(A))
& meet_absorbing(boole_lattice(A))
& meet_associative(boole_lattice(A))
& meet_commutative(boole_lattice(A))
& join_associative(boole_lattice(A))
& join_commutative(boole_lattice(A))
& strict_latt_str(boole_lattice(A))
& ~ empty_carrier(boole_lattice(A)) ),
file('theBenchmark.p',fc3_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(t2_lattice3,axiom,
! [A,B] :
( element(B,the_carrier(boole_lattice(A)))
=> ! [C] :
( element(C,the_carrier(boole_lattice(A)))
=> ( below(boole_lattice(A),B,C)
<=> subset(B,C) ) ) ),
file('theBenchmark.p',t2_lattice3) ).
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(t2_yellow_1,conjecture,
! [A,B] :
( element(B,the_carrier(boole_POSet(A)))
=> ! [C] :
( element(C,the_carrier(boole_POSet(A)))
=> ( related_reflexive(boole_POSet(A),B,C)
<=> subset(B,C) ) ) ),
file('theBenchmark.p',t2_yellow_1) ).
fof(t2_yellow_1_neg,negated_conjecture,
~ ! [A,B] :
( element(B,the_carrier(boole_POSet(A)))
=> ! [C] :
( element(C,the_carrier(boole_POSet(A)))
=> ( related_reflexive(boole_POSet(A),B,C)
<=> subset(B,C) ) ) ),
inference(assume_negation,[status(cth)],[t2_yellow_1]) ).
cnf(c_135,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_136,plain,
( rel_str(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[dt_k3_lattice3]) ).
cnf(c_157,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_158,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_160,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_161,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_169,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_136,c_135]) ).
cnf(c_233,plain,
( strict_rel_str(poset_of_lattice(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[dt_k3_lattice3]) ).
cnf(c_234,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_239,plain,
latt_str(boole_lattice(A)),
inference(clausify,[status(thm)],[dt_k1_lattice3]) ).
cnf(c_241,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_242,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_309,plain,
( relation_of2(A,B,C)
| ~ relation_of2_as_subset(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_340,plain,
( relation_of2_as_subset(k2_lattice3(boole_lattice(A)),the_carrier(boole_lattice(A)),the_carrier(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_239,c_234]) ).
fof(nnf_120,plain,
? [A,B] :
( ? [C] :
( ( ~ subset(B,C)
| ~ related_reflexive(boole_POSet(A),B,C) )
& ( subset(B,C)
| related_reflexive(boole_POSet(A),B,C) )
& element(C,the_carrier(boole_POSet(A))) )
& element(B,the_carrier(boole_POSet(A))) ),
inference(fof_nnf,[status(thm)],[t2_yellow_1_neg]) ).
fof(sk_t2_yellow_1_neg,plain,
( ( ~ subset(sK1,sK2)
| ~ related_reflexive(boole_POSet(sK0),sK1,sK2) )
& ( subset(sK1,sK2)
| related_reflexive(boole_POSet(sK0),sK1,sK2) )
& element(sK2,the_carrier(boole_POSet(sK0)))
& element(sK1,the_carrier(boole_POSet(sK0))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0,sK2]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2)],[nnf_120]) ).
cnf(c_786,negated_conjecture,
( ~ subset(sK1,sK2)
| ~ related_reflexive(boole_POSet(sK0),sK1,sK2) ),
inference(split_conjunct,[status(thm)],[sk_t2_yellow_1_neg]) ).
cnf(c_787,negated_conjecture,
( subset(sK1,sK2)
| related_reflexive(boole_POSet(sK0),sK1,sK2) ),
inference(split_conjunct,[status(thm)],[sk_t2_yellow_1_neg]) ).
cnf(c_788,negated_conjecture,
element(sK2,the_carrier(boole_POSet(sK0))),
inference(split_conjunct,[status(thm)],[sk_t2_yellow_1_neg]) ).
cnf(c_789,negated_conjecture,
element(sK1,the_carrier(boole_POSet(sK0))),
inference(split_conjunct,[status(thm)],[sk_t2_yellow_1_neg]) ).
cnf(c_798,plain,
( ~ subset(A,C)
| below(boole_lattice(B),A,C)
| ~ element(C,the_carrier(boole_lattice(B)))
| ~ element(A,the_carrier(boole_lattice(B))) ),
inference(clausify,[status(thm)],[t2_lattice3]) ).
cnf(c_799,plain,
( subset(A,C)
| ~ below(boole_lattice(B),A,C)
| ~ element(C,the_carrier(boole_lattice(B)))
| ~ element(A,the_carrier(boole_lattice(B))) ),
inference(clausify,[status(thm)],[t2_lattice3]) ).
cnf(c_918,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_940,plain,
lattice(boole_lattice(A)),
inference(clausify,[status(thm)],[fc3_lattice3]) ).
cnf(c_941,plain,
join_absorbing(boole_lattice(A)),
inference(clausify,[status(thm)],[fc3_lattice3]) ).
cnf(c_942,plain,
meet_absorbing(boole_lattice(A)),
inference(clausify,[status(thm)],[fc3_lattice3]) ).
cnf(c_944,plain,
meet_commutative(boole_lattice(A)),
inference(clausify,[status(thm)],[fc3_lattice3]) ).
cnf(c_948,plain,
~ empty_carrier(boole_lattice(A)),
inference(clausify,[status(thm)],[fc3_lattice3]) ).
cnf(c_963,plain,
boole_POSet(A) = poset_of_lattice(boole_lattice(A)),
inference(clausify,[status(thm)],[d2_yellow_1]) ).
cnf(c_1621,plain,
( strict_rel_str(poset_of_lattice(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_239,c_233]) ).
cnf(c_12301,plain,
( strict_rel_str(poset_of_lattice(boole_lattice(A)))
| ~ lattice(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_948,c_1621]) ).
cnf(c_1622,plain,
strict_rel_str(poset_of_lattice(boole_lattice(A))),
inference(resolve,[status(thm)],[c_940,c_12301]) ).
cnf(c_1649,plain,
( below(boole_lattice(A),B,C)
| ~ below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ join_absorbing(boole_lattice(A))
| ~ meet_absorbing(boole_lattice(A))
| ~ meet_commutative(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_239,c_157]) ).
cnf(c_12302,plain,
( below(boole_lattice(A),B,C)
| ~ below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ join_absorbing(boole_lattice(A))
| ~ meet_absorbing(boole_lattice(A))
| ~ meet_commutative(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_948,c_1649]) ).
cnf(c_12303,plain,
( below(boole_lattice(A),B,C)
| ~ below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ join_absorbing(boole_lattice(A))
| ~ meet_absorbing(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_944,c_12302]) ).
cnf(c_12304,plain,
( below(boole_lattice(A),B,C)
| ~ below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ join_absorbing(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_942,c_12303]) ).
cnf(c_1650,plain,
( below(boole_lattice(B),A,C)
| ~ below_refl(boole_lattice(B),A,C)
| ~ element(C,the_carrier(boole_lattice(B)))
| ~ element(A,the_carrier(boole_lattice(B))) ),
inference(resolve,[status(thm)],[c_941,c_12304]) ).
cnf(c_1651,plain,
( ~ below(boole_lattice(A),B,C)
| below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ join_absorbing(boole_lattice(A))
| ~ meet_absorbing(boole_lattice(A))
| ~ meet_commutative(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_239,c_158]) ).
cnf(c_12305,plain,
( ~ below(boole_lattice(A),B,C)
| below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ join_absorbing(boole_lattice(A))
| ~ meet_absorbing(boole_lattice(A))
| ~ meet_commutative(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_948,c_1651]) ).
cnf(c_12306,plain,
( ~ below(boole_lattice(A),B,C)
| below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ join_absorbing(boole_lattice(A))
| ~ meet_absorbing(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_944,c_12305]) ).
cnf(c_12307,plain,
( ~ below(boole_lattice(A),B,C)
| below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ join_absorbing(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_942,c_12306]) ).
cnf(c_1652,plain,
( ~ below(boole_lattice(B),A,C)
| below_refl(boole_lattice(B),A,C)
| ~ element(C,the_carrier(boole_lattice(B)))
| ~ element(A,the_carrier(boole_lattice(B))) ),
inference(resolve,[status(thm)],[c_941,c_12307]) ).
cnf(c_1655,plain,
( related_reflexive(poset_of_lattice(boole_lattice(A)),cast_to_el_of_LattPOSet(boole_lattice(A),B),cast_to_el_of_LattPOSet(boole_lattice(A),C))
| ~ below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_239,c_160]) ).
cnf(c_12308,plain,
( related_reflexive(poset_of_lattice(boole_lattice(A)),cast_to_el_of_LattPOSet(boole_lattice(A),B),cast_to_el_of_LattPOSet(boole_lattice(A),C))
| ~ below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ lattice(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_948,c_1655]) ).
cnf(c_1656,plain,
( related_reflexive(poset_of_lattice(boole_lattice(B)),cast_to_el_of_LattPOSet(boole_lattice(B),A),cast_to_el_of_LattPOSet(boole_lattice(B),C))
| ~ below_refl(boole_lattice(B),A,C)
| ~ element(C,the_carrier(boole_lattice(B)))
| ~ element(A,the_carrier(boole_lattice(B))) ),
inference(resolve,[status(thm)],[c_940,c_12308]) ).
cnf(c_1657,plain,
( ~ related_reflexive(poset_of_lattice(boole_lattice(A)),cast_to_el_of_LattPOSet(boole_lattice(A),B),cast_to_el_of_LattPOSet(boole_lattice(A),C))
| below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_239,c_161]) ).
cnf(c_12309,plain,
( ~ related_reflexive(poset_of_lattice(boole_lattice(A)),cast_to_el_of_LattPOSet(boole_lattice(A),B),cast_to_el_of_LattPOSet(boole_lattice(A),C))
| below_refl(boole_lattice(A),B,C)
| ~ element(C,the_carrier(boole_lattice(A)))
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ lattice(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_948,c_1657]) ).
cnf(c_1658,plain,
( ~ related_reflexive(poset_of_lattice(boole_lattice(B)),cast_to_el_of_LattPOSet(boole_lattice(B),A),cast_to_el_of_LattPOSet(boole_lattice(B),C))
| below_refl(boole_lattice(B),A,C)
| ~ element(C,the_carrier(boole_lattice(B)))
| ~ element(A,the_carrier(boole_lattice(B))) ),
inference(resolve,[status(thm)],[c_940,c_12309]) ).
cnf(c_1668,plain,
( rel_str_of(the_carrier(poset_of_lattice(boole_lattice(A))),the_InternalRel(poset_of_lattice(boole_lattice(A)))) = poset_of_lattice(boole_lattice(A))
| ~ strict_rel_str(poset_of_lattice(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_239,c_169]) ).
cnf(c_12310,plain,
( rel_str_of(the_carrier(poset_of_lattice(boole_lattice(A))),the_InternalRel(poset_of_lattice(boole_lattice(A)))) = poset_of_lattice(boole_lattice(A))
| ~ strict_rel_str(poset_of_lattice(boole_lattice(A)))
| ~ lattice(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_948,c_1668]) ).
cnf(c_12311,plain,
( rel_str_of(the_carrier(poset_of_lattice(boole_lattice(A))),the_InternalRel(poset_of_lattice(boole_lattice(A)))) = poset_of_lattice(boole_lattice(A))
| ~ strict_rel_str(poset_of_lattice(boole_lattice(A))) ),
inference(resolve,[status(thm)],[c_940,c_12310]) ).
cnf(c_1669,plain,
rel_str_of(the_carrier(poset_of_lattice(boole_lattice(A))),the_InternalRel(poset_of_lattice(boole_lattice(A)))) = poset_of_lattice(boole_lattice(A)),
inference(resolve,[status(thm)],[c_1622,c_12311]) ).
cnf(c_1722,plain,
( cast_to_el_of_LattPOSet(boole_lattice(A),B) = B
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_241,c_239]) ).
cnf(c_12312,plain,
( cast_to_el_of_LattPOSet(boole_lattice(A),B) = B
| ~ element(B,the_carrier(boole_lattice(A)))
| ~ lattice(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_948,c_1722]) ).
cnf(c_1723,plain,
( cast_to_el_of_LattPOSet(boole_lattice(B),A) = A
| ~ element(A,the_carrier(boole_lattice(B))) ),
inference(resolve,[status(thm)],[c_940,c_12312]) ).
cnf(c_1740,plain,
( poset_of_lattice(boole_lattice(A)) = rel_str_of(the_carrier(boole_lattice(A)),k2_lattice3(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_242,c_239]) ).
cnf(c_12313,plain,
( rel_str_of(the_carrier(boole_lattice(A)),k2_lattice3(boole_lattice(A))) = poset_of_lattice(boole_lattice(A))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(copy,[status(thm)],[c_1740]) ).
cnf(c_12314,plain,
( rel_str_of(the_carrier(boole_lattice(A)),k2_lattice3(boole_lattice(A))) = poset_of_lattice(boole_lattice(A))
| ~ lattice(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_948,c_12313]) ).
cnf(c_1741,plain,
rel_str_of(the_carrier(boole_lattice(A)),k2_lattice3(boole_lattice(A))) = poset_of_lattice(boole_lattice(A)),
inference(resolve,[status(thm)],[c_940,c_12314]) ).
cnf(c_2153,plain,
( relation_of2(k2_lattice3(boole_lattice(A)),the_carrier(boole_lattice(A)),the_carrier(boole_lattice(A)))
| ~ lattice(boole_lattice(A))
| empty_carrier(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_340,c_309]) ).
cnf(c_12315,plain,
( relation_of2(k2_lattice3(boole_lattice(A)),the_carrier(boole_lattice(A)),the_carrier(boole_lattice(A)))
| ~ lattice(boole_lattice(A)) ),
inference(resolve,[status(thm)],[c_948,c_2153]) ).
cnf(c_2154,plain,
relation_of2(k2_lattice3(boole_lattice(A)),the_carrier(boole_lattice(A)),the_carrier(boole_lattice(A))),
inference(resolve,[status(thm)],[c_940,c_12315]) ).
cnf(c_2481,negated_conjecture,
element(sK1,the_carrier(poset_of_lattice(boole_lattice(sK0)))),
inference(paramod,[status(thm)],[c_963,c_789]) ).
cnf(c_2482,negated_conjecture,
element(sK2,the_carrier(poset_of_lattice(boole_lattice(sK0)))),
inference(paramod,[status(thm)],[c_963,c_788]) ).
cnf(c_2483,negated_conjecture,
( subset(sK1,sK2)
| related_reflexive(poset_of_lattice(boole_lattice(sK0)),sK1,sK2) ),
inference(paramod,[status(thm)],[c_963,c_787]) ).
cnf(c_2484,negated_conjecture,
( ~ subset(sK1,sK2)
| ~ related_reflexive(poset_of_lattice(boole_lattice(sK0)),sK1,sK2) ),
inference(paramod,[status(thm)],[c_963,c_786]) ).
cnf(c_12316,plain,
( A = the_carrier(boole_lattice(C))
| rel_str_of(A,B) != rel_str_of(the_carrier(boole_lattice(C)),k2_lattice3(boole_lattice(C))) ),
inference(resolve,[status(thm)],[c_2154,c_918]) ).
cnf(c_12317,plain,
( A = the_carrier(boole_lattice(C))
| rel_str_of(A,B) != poset_of_lattice(boole_lattice(C)) ),
inference(paramod,[status(thm)],[c_1741,c_12316]) ).
cnf(c_12318,plain,
( A = the_carrier(boole_lattice(C))
| poset_of_lattice(boole_lattice(C)) != rel_str_of(A,B) ),
inference(copy,[status(thm)],[c_12317]) ).
cnf(c_5680,plain,
( the_carrier(boole_lattice(A)) = B
| poset_of_lattice(boole_lattice(A)) != rel_str_of(B,C) ),
inference(copy,[status(thm)],[c_12318]) ).
cnf(c_12319,plain,
poset_of_lattice(boole_lattice(A)) = rel_str_of(the_carrier(poset_of_lattice(boole_lattice(A))),the_InternalRel(poset_of_lattice(boole_lattice(A)))),
inference(copy,[status(thm)],[c_1669]) ).
cnf(c_12320,plain,
the_carrier(boole_lattice(A)) = the_carrier(poset_of_lattice(boole_lattice(A))),
inference(resolve,[status(thm)],[c_5680,c_12319]) ).
cnf(c_8875,plain,
the_carrier(poset_of_lattice(boole_lattice(A))) = the_carrier(boole_lattice(A)),
inference(copy,[status(thm)],[c_12320]) ).
cnf(c_8906,negated_conjecture,
element(sK2,the_carrier(boole_lattice(sK0))),
inference(paramod,[status(thm)],[c_8875,c_2482]) ).
cnf(c_8907,negated_conjecture,
element(sK1,the_carrier(boole_lattice(sK0))),
inference(paramod,[status(thm)],[c_8875,c_2481]) ).
cnf(c_8924,plain,
cast_to_el_of_LattPOSet(boole_lattice(sK0),sK2) = sK2,
inference(resolve,[status(thm)],[c_8906,c_1723]) ).
cnf(c_8927,plain,
cast_to_el_of_LattPOSet(boole_lattice(sK0),sK1) = sK1,
inference(resolve,[status(thm)],[c_8907,c_1723]) ).
cnf(c_12321,plain,
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK0)),cast_to_el_of_LattPOSet(boole_lattice(sK0),A),sK2)
| below_refl(boole_lattice(sK0),A,sK2)
| ~ element(sK2,the_carrier(boole_lattice(sK0)))
| ~ element(A,the_carrier(boole_lattice(sK0))) ),
inference(paramod,[status(thm)],[c_8924,c_1658]) ).
cnf(c_8929,negated_conjecture,
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK0)),cast_to_el_of_LattPOSet(boole_lattice(sK0),A),sK2)
| below_refl(boole_lattice(sK0),A,sK2)
| ~ element(A,the_carrier(boole_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_8906,c_12321]) ).
cnf(c_12322,plain,
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK0)),sK1,sK2)
| below_refl(boole_lattice(sK0),sK1,sK2)
| ~ element(sK1,the_carrier(boole_lattice(sK0))) ),
inference(paramod,[status(thm)],[c_8927,c_8929]) ).
cnf(c_12272,negated_conjecture,
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK0)),sK1,sK2)
| below_refl(boole_lattice(sK0),sK1,sK2) ),
inference(resolve,[status(thm)],[c_8907,c_12322]) ).
cnf(c_12276,plain,
( subset(sK1,sK2)
| below_refl(boole_lattice(sK0),sK1,sK2) ),
inference(resolve,[status(thm)],[c_12272,c_2483]) ).
cnf(c_12323,plain,
( below(boole_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(boole_lattice(sK0)))
| ~ element(sK1,the_carrier(boole_lattice(sK0)))
| subset(sK1,sK2) ),
inference(resolve,[status(thm)],[c_12276,c_1650]) ).
cnf(c_12324,negated_conjecture,
( below(boole_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(boole_lattice(sK0)))
| subset(sK1,sK2) ),
inference(resolve,[status(thm)],[c_8907,c_12323]) ).
cnf(c_12277,negated_conjecture,
( below(boole_lattice(sK0),sK1,sK2)
| subset(sK1,sK2) ),
inference(resolve,[status(thm)],[c_8906,c_12324]) ).
cnf(c_12325,plain,
( subset(sK1,sK2)
| ~ element(sK2,the_carrier(boole_lattice(sK0)))
| ~ element(sK1,the_carrier(boole_lattice(sK0)))
| subset(sK1,sK2) ),
inference(resolve,[status(thm)],[c_12277,c_799]) ).
cnf(c_12326,plain,
( ~ element(sK2,the_carrier(boole_lattice(sK0)))
| ~ element(sK1,the_carrier(boole_lattice(sK0)))
| subset(sK1,sK2) ),
inference(copy,[status(thm)],[c_12325]) ).
cnf(c_12327,negated_conjecture,
( ~ element(sK2,the_carrier(boole_lattice(sK0)))
| subset(sK1,sK2) ),
inference(resolve,[status(thm)],[c_8907,c_12326]) ).
cnf(c_12278,negated_conjecture,
subset(sK1,sK2),
inference(resolve,[status(thm)],[c_8906,c_12327]) ).
cnf(c_12279,negated_conjecture,
~ related_reflexive(poset_of_lattice(boole_lattice(sK0)),sK1,sK2),
inference(resolve,[status(thm)],[c_12278,c_2484]) ).
cnf(c_12280,plain,
( below(boole_lattice(A),sK1,sK2)
| ~ element(sK2,the_carrier(boole_lattice(A)))
| ~ element(sK1,the_carrier(boole_lattice(A))) ),
inference(resolve,[status(thm)],[c_12278,c_798]) ).
cnf(c_12328,negated_conjecture,
( below(boole_lattice(sK0),sK1,sK2)
| ~ element(sK1,the_carrier(boole_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_12280,c_8906]) ).
cnf(c_12298,negated_conjecture,
below(boole_lattice(sK0),sK1,sK2),
inference(resolve,[status(thm)],[c_8907,c_12328]) ).
cnf(c_12329,plain,
( below_refl(boole_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(boole_lattice(sK0)))
| ~ element(sK1,the_carrier(boole_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_12298,c_1652]) ).
cnf(c_12330,negated_conjecture,
( below_refl(boole_lattice(sK0),sK1,sK2)
| ~ element(sK2,the_carrier(boole_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_8907,c_12329]) ).
cnf(c_12299,negated_conjecture,
below_refl(boole_lattice(sK0),sK1,sK2),
inference(resolve,[status(thm)],[c_8906,c_12330]) ).
cnf(c_12331,plain,
( related_reflexive(poset_of_lattice(boole_lattice(sK0)),cast_to_el_of_LattPOSet(boole_lattice(sK0),sK1),cast_to_el_of_LattPOSet(boole_lattice(sK0),sK2))
| ~ element(sK2,the_carrier(boole_lattice(sK0)))
| ~ element(sK1,the_carrier(boole_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_12299,c_1656]) ).
cnf(c_12332,plain,
( related_reflexive(poset_of_lattice(boole_lattice(sK0)),sK1,cast_to_el_of_LattPOSet(boole_lattice(sK0),sK2))
| ~ element(sK2,the_carrier(boole_lattice(sK0)))
| ~ element(sK1,the_carrier(boole_lattice(sK0))) ),
inference(paramod,[status(thm)],[c_8927,c_12331]) ).
cnf(c_12333,plain,
( related_reflexive(poset_of_lattice(boole_lattice(sK0)),sK1,sK2)
| ~ element(sK2,the_carrier(boole_lattice(sK0)))
| ~ element(sK1,the_carrier(boole_lattice(sK0))) ),
inference(paramod,[status(thm)],[c_8924,c_12332]) ).
cnf(c_12334,negated_conjecture,
( related_reflexive(poset_of_lattice(boole_lattice(sK0)),sK1,sK2)
| ~ element(sK2,the_carrier(boole_lattice(sK0))) ),
inference(resolve,[status(thm)],[c_8907,c_12333]) ).
cnf(c_12335,negated_conjecture,
related_reflexive(poset_of_lattice(boole_lattice(sK0)),sK1,sK2),
inference(resolve,[status(thm)],[c_8906,c_12334]) ).
cnf(c_12300,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_12279,c_12335]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU369+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n018.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 26 09:23:06 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 83727 was started by sandbox on n018,
% 0.08/0.35 % Sat Sep 26 09:23:06 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.38
% 0.13/0.38 % From the command line: assign(max_seconds, 300).
% 57.31/7.61
% 57.31/7.61 % given #500 (I,wt=7): 1528 empty_carrier(c5) | -lattice(c5) | antisymmetric_relstr(poset_of_lattice(c5)). [resolve(225,a,220,c)].
% 57.31/7.61
% 57.31/7.61 % given #1000 (I,wt=3): 2421 antisymmetric(the_InternalRel(c10)). [back_unit_del(743),unit_del(a,859),unit_del(b,858),unit_del(c,857)].
% 57.31/7.61
% 57.31/7.61 % given #1500 (F,wt=8): 7892 -in(powerset(the_carrier(poset_of_lattice(c9))),f7(poset_of_lattice(c9))). [resolve(5895,a,965,b)].
% 57.31/7.61
% 57.31/7.61 % given #2000 (T,wt=7): 8431 element(f2(f7(poset_of_lattice(c21))),the_carrier(c21)). [resolve(7765,b,8415,a),unit_del(a,2265)].
% 57.31/7.61
% 57.31/7.61 % given #2500 (T,wt=12): 8458 empty(the_InternalRel(c15)) | element(f2(the_InternalRel(c15)),cartesian_product2(the_carrier(c15),the_carrier(c15))). [resolve(7765,b,2093,a)].
% 57.31/7.61
% 57.31/7.61 % given #3000 (T,wt=15): 8778 -element(the_InternalRel(poset_of_lattice(boole_lattice(c22))),powerset(A)) | element(unordered_pair(unordered_pair(c23,c23),singleton(c23)),A). [resolve(7802,a,794,a)].
% 57.31/7.61
% 57.31/7.61 % given #3500 (T,wt=16): 6317 latt_str_of(the_carrier(c6),the_L_meet(c6),the_L_meet(c6)) != latt_str_of(A,B,C) | the_carrier(c6) = A. [resolve(2454,b,503,a),flip(c),flip(d),unit_del(a,513),unit_del(b,518)].
% 57.31/7.61
% 57.31/7.61 % given #4000 (T,wt=13): 10375 empty(f2(powerset(f7(c14)))) | element(f2(f2(powerset(f7(c14)))),the_carrier(c14)). [resolve(8949,c,2201,a),unit_del(b,2171)].
% 57.31/7.61
% 57.31/7.61 % given #4500 (T,wt=17): 6582 -lattice(latt_str_of(the_carrier(c8),the_L_meet(c8),the_L_meet(c8))) | antisymmetric_relstr(poset_of_lattice(latt_str_of(the_carrier(c8),the_L_meet(c8),the_L_meet(c8)))). [resolve(2614,b,501,a),unit_del(a,511),unit_del(b,522),unit_del(c,6339)].
% 57.31/7.61
% 57.31/7.61 % given #5000 (T,wt=18): 11332 element(f2(f7(latt_str_of(the_carrier(c20),the_L_join(c20),the_L_join(c20)))),the_carrier(latt_str_of(the_carrier(c20),the_L_join(c20),the_L_join(c20)))). [resolve(6390,a,7765,b),unit_del(a,6391)].
% 57.31/7.61
% 57.31/7.61 % SZS status Theorem for theBenchmark
% 57.31/7.61
% 57.31/7.61 % Proof 1 at 6.73 (+ 0.42) seconds.
% 57.31/7.61 % Length of proof is 79.
% 57.31/7.61 % Level of proof is 17.
% 57.31/7.61 % Maximum clause weight is 27.000.
% 57.31/7.61 % Given clauses 5325.
% 57.31/7.61
% 57.31/7.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------