%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU369+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:20:19 PM UTC 2026
% Result : Theorem 0.20s 5.86s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 14
% Syntax : Number of formulae : 136 ( 27 unt; 0 def)
% Number of atoms : 551 ( 46 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 710 ( 295 ~; 324 |; 63 &)
% ( 9 <=>; 18 =>; 0 <=; 1 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-2 aty)
% Number of variables : 191 ( 185 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A] :
( rel_str(A)
=> ( strict_rel_str(A)
=> A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( ( latt_str(A)
& lattice(A)
& ~ empty_carrier(A) )
=> poset_of_lattice(A) = rel_str_of(the_carrier(A),k2_lattice3(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] : boole_POSet(A) = poset_of_lattice(boole_lattice(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( latt_str(boole_lattice(A))
& strict_latt_str(boole_lattice(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A] :
( rel_str(boole_POSet(A))
& strict_rel_str(boole_POSet(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A] :
( rel_str(A)
=> relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [A] :
( complete_latt_str(boole_lattice(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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,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(negated_conjecture,[status(cth)],[f114]) ).
fof(f121,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,plain,
! [A] :
( A = rel_str_of(the_carrier(A),the_InternalRel(A))
| ~ strict_rel_str(A)
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f124,plain,
! [X0] :
( X0 = rel_str_of(the_carrier(X0),the_InternalRel(X0))
| ~ strict_rel_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f205,plain,
! [A] :
( poset_of_lattice(A) = rel_str_of(the_carrier(A),k2_lattice3(A))
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f206,plain,
! [X0] :
( poset_of_lattice(X0) = rel_str_of(the_carrier(X0),k2_lattice3(X0))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f207,plain,
! [X0] : boole_POSet(X0) = poset_of_lattice(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f208,plain,
! [A] :
( ! [B] :
( cast_to_el_of_LattPOSet(A,B) = B
| ~ element(B,the_carrier(A)) )
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f209,plain,
! [X0,X1] :
( cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ element(X1,the_carrier(X0))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f221,plain,
( ! [A] : latt_str(boole_lattice(A))
& ! [A] : strict_latt_str(boole_lattice(A)) ),
inference(miniscoping,[status(thm)],[f28]) ).
fof(f223,plain,
! [X0] : latt_str(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f236,plain,
( ! [A] : rel_str(boole_POSet(A))
& ! [A] : strict_rel_str(boole_POSet(A)) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f237,plain,
! [X0] : strict_rel_str(boole_POSet(X0)),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f238,plain,
! [X0] : rel_str(boole_POSet(X0)),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f258,plain,
! [A] :
( relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A))
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f259,plain,
! [X0] :
( relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f280,plain,
( ! [A] : complete_latt_str(boole_lattice(A))
& ! [A] : boolean_lattstr(boole_lattice(A))
& ! [A] : complemented_lattstr(boole_lattice(A))
& ! [A] : bounded_lattstr(boole_lattice(A))
& ! [A] : upper_bounded_semilattstr(boole_lattice(A))
& ! [A] : lower_bounded_semilattstr(boole_lattice(A))
& ! [A] : modular_lattstr(boole_lattice(A))
& ! [A] : distributive_lattstr(boole_lattice(A))
& ! [A] : lattice(boole_lattice(A))
& ! [A] : join_absorbing(boole_lattice(A))
& ! [A] : meet_absorbing(boole_lattice(A))
& ! [A] : meet_associative(boole_lattice(A))
& ! [A] : meet_commutative(boole_lattice(A))
& ! [A] : join_associative(boole_lattice(A))
& ! [A] : join_commutative(boole_lattice(A))
& ! [A] : strict_latt_str(boole_lattice(A))
& ! [A] : ~ empty_carrier(boole_lattice(A)) ),
inference(miniscoping,[status(thm)],[f60]) ).
fof(f281,plain,
! [X0] : ~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f285,plain,
! [X0] : meet_commutative(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f287,plain,
! [X0] : meet_absorbing(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f288,plain,
! [X0] : join_absorbing(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f289,plain,
! [X0] : lattice(boole_lattice(X0)),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f419,plain,
! [A,B] :
( ! [C,D] :
( ( B = D
& A = C )
| rel_str_of(A,B) != rel_str_of(C,D) )
| ~ relation_of2(B,A,A) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f420,plain,
! [X0,X1,X2,X3] :
( X1 = X2
| rel_str_of(X1,X0) != rel_str_of(X2,X3)
| ~ relation_of2(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f421,plain,
! [X0,X1,X2,X3] :
( X0 = X3
| rel_str_of(X1,X0) != rel_str_of(X2,X3)
| ~ relation_of2(X0,X1,X1) ),
inference(cnf_transformation,[status(thm)],[f419]) ).
fof(f580,plain,
! [A,B,C] :
( ( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f105]) ).
fof(f581,plain,
( ! [A,B,C] :
( ~ relation_of2(C,A,B)
| relation_of2_as_subset(C,A,B) )
& ! [A,B,C] :
( relation_of2(C,A,B)
| ~ relation_of2_as_subset(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f580]) ).
fof(f582,plain,
! [X0,X1,X2] :
( relation_of2(X0,X1,X2)
| ~ relation_of2_as_subset(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f581]) ).
fof(f584,plain,
! [A,B,C] :
( ( below_refl(A,B,C)
<=> below(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(pre_NNF_transformation,[status(thm)],[f106]) ).
fof(f585,plain,
! [A,B,C] :
( ( ( ~ below(A,B,C)
| below_refl(A,B,C) )
& ( 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(NNF_transformation,[status(thm)],[f584]) ).
fof(f586,plain,
! [X0,X1,X2] :
( below(X0,X1,X2)
| ~ below_refl(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ latt_str(X0)
| ~ join_absorbing(X0)
| ~ meet_absorbing(X0)
| ~ meet_commutative(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f585]) ).
fof(f587,plain,
! [X0,X1,X2] :
( ~ below(X0,X1,X2)
| below_refl(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ latt_str(X0)
| ~ join_absorbing(X0)
| ~ meet_absorbing(X0)
| ~ meet_commutative(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f585]) ).
fof(f602,plain,
! [A,B] :
( ! [C] :
( ( below(boole_lattice(A),B,C)
<=> subset(B,C) )
| ~ element(C,the_carrier(boole_lattice(A))) )
| ~ element(B,the_carrier(boole_lattice(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f112]) ).
fof(f603,plain,
! [A,B] :
( ! [C] :
( ( ( ~ subset(B,C)
| below(boole_lattice(A),B,C) )
& ( subset(B,C)
| ~ below(boole_lattice(A),B,C) ) )
| ~ element(C,the_carrier(boole_lattice(A))) )
| ~ element(B,the_carrier(boole_lattice(A))) ),
inference(NNF_transformation,[status(thm)],[f602]) ).
fof(f604,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ below(boole_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(boole_lattice(X1)))
| ~ element(X0,the_carrier(boole_lattice(X1))) ),
inference(cnf_transformation,[status(thm)],[f603]) ).
fof(f605,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| below(boole_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(boole_lattice(X1)))
| ~ element(X0,the_carrier(boole_lattice(X1))) ),
inference(cnf_transformation,[status(thm)],[f603]) ).
fof(f608,plain,
? [A,B] :
( ? [C] :
( ( related_reflexive(boole_POSet(A),B,C)
<~> subset(B,C) )
& element(C,the_carrier(boole_POSet(A))) )
& element(B,the_carrier(boole_POSet(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f115]) ).
fof(f609,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(NNF_transformation,[status(thm)],[f608]) ).
fof(f610,plain,
( ( ~ subset(sK29_skl,sK30_skl)
| ~ related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl) )
& ( subset(sK29_skl,sK30_skl)
| related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl) )
& element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
& element(sK29_skl,the_carrier(boole_POSet(sK28_skl))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl,sK29_skl,sK30_skl]),skolemize(A,sK28_skl),skolemize(B,sK29_skl),skolemize(C,sK30_skl)],[f609]) ).
fof(f611,plain,
element(sK29_skl,the_carrier(boole_POSet(sK28_skl))),
inference(cnf_transformation,[status(thm)],[f610]) ).
fof(f612,plain,
element(sK30_skl,the_carrier(boole_POSet(sK28_skl))),
inference(cnf_transformation,[status(thm)],[f610]) ).
fof(f613,plain,
( subset(sK29_skl,sK30_skl)
| related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl) ),
inference(cnf_transformation,[status(thm)],[f610]) ).
fof(f614,plain,
( ~ subset(sK29_skl,sK30_skl)
| ~ related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl) ),
inference(cnf_transformation,[status(thm)],[f610]) ).
fof(f630,plain,
! [A] :
( ! [B] :
( ! [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)) )
| ~ element(C,the_carrier(A)) )
| ~ element(B,the_carrier(A)) )
| ~ latt_str(A)
| ~ lattice(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f121]) ).
fof(f631,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(NNF_transformation,[status(thm)],[f630]) ).
fof(f632,plain,
! [X0,X1,X2] :
( related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2))
| ~ below_refl(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f631]) ).
fof(f633,plain,
! [X0,X1,X2] :
( ~ related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2))
| below_refl(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ latt_str(X0)
| ~ lattice(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f631]) ).
fof(f859,plain,
! [X0] :
( boole_POSet(X0) = rel_str_of(the_carrier(boole_POSet(X0)),the_InternalRel(boole_POSet(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(resolution,[status(thm)],[f237,f124]) ).
fof(f860,plain,
! [X0] : boole_POSet(X0) = rel_str_of(the_carrier(boole_POSet(X0)),the_InternalRel(boole_POSet(X0))),
inference(forward_subsumption_resolution,[status(thm)],[f859,f238]) ).
fof(f952,plain,
! [X0] : relation_of2_as_subset(the_InternalRel(boole_POSet(X0)),the_carrier(boole_POSet(X0)),the_carrier(boole_POSet(X0))),
inference(resolution,[status(thm)],[f259,f238]) ).
fof(f1058,plain,
! [X0] :
( poset_of_lattice(boole_lattice(X0)) = rel_str_of(the_carrier(boole_lattice(X0)),k2_lattice3(boole_lattice(X0)))
| ~ latt_str(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(resolution,[status(thm)],[f289,f206]) ).
fof(f1076,plain,
! [X0] :
( boole_POSet(X0) = rel_str_of(the_carrier(boole_lattice(X0)),k2_lattice3(boole_lattice(X0)))
| ~ latt_str(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(forward_demodulation,[status(thm)],[f207,f1058]) ).
fof(f1077,plain,
! [X0] :
( boole_POSet(X0) = rel_str_of(the_carrier(boole_lattice(X0)),k2_lattice3(boole_lattice(X0)))
| ~ latt_str(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1076,f281]) ).
fof(f1078,plain,
! [X0] : boole_POSet(X0) = rel_str_of(the_carrier(boole_lattice(X0)),k2_lattice3(boole_lattice(X0))),
inference(resolution,[status(thm)],[f1077,f223]) ).
fof(f1345,plain,
! [X0] : relation_of2(the_InternalRel(boole_POSet(X0)),the_carrier(boole_POSet(X0)),the_carrier(boole_POSet(X0))),
inference(resolution,[status(thm)],[f582,f952]) ).
fof(f1356,plain,
! [X0,X1,X2] :
( the_InternalRel(boole_POSet(X0)) = X2
| rel_str_of(the_carrier(boole_POSet(X0)),the_InternalRel(boole_POSet(X0))) != rel_str_of(X1,X2) ),
inference(resolution,[status(thm)],[f1345,f421]) ).
fof(f1357,plain,
! [X0,X1,X2] :
( the_carrier(boole_POSet(X0)) = X1
| rel_str_of(the_carrier(boole_POSet(X0)),the_InternalRel(boole_POSet(X0))) != rel_str_of(X1,X2) ),
inference(resolution,[status(thm)],[f1345,f420]) ).
fof(f1361,plain,
! [X0,X1,X2] :
( the_InternalRel(boole_POSet(X0)) = X2
| boole_POSet(X0) != rel_str_of(X1,X2) ),
inference(forward_demodulation,[status(thm)],[f860,f1356]) ).
fof(f1362,plain,
! [X0,X1,X2] :
( the_carrier(boole_POSet(X0)) = X1
| boole_POSet(X0) != rel_str_of(X1,X2) ),
inference(forward_demodulation,[status(thm)],[f860,f1357]) ).
fof(f1366,plain,
! [X0] : the_InternalRel(boole_POSet(X0)) = k2_lattice3(boole_lattice(X0)),
inference(resolution,[status(thm)],[f1361,f1078]) ).
fof(f1370,plain,
! [X0] : boole_POSet(X0) = rel_str_of(the_carrier(boole_lattice(X0)),the_InternalRel(boole_POSet(X0))),
inference(backward_demodulation,[status(thm)],[f1366,f1078]) ).
fof(f1384,plain,
! [X0] : the_carrier(boole_POSet(X0)) = the_carrier(boole_lattice(X0)),
inference(resolution,[status(thm)],[f1370,f1362]) ).
fof(f1397,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| below(boole_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_lattice(X1))) ),
inference(backward_demodulation,[status(thm)],[f1384,f605]) ).
fof(f1398,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ below(boole_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_lattice(X1))) ),
inference(backward_demodulation,[status(thm)],[f1384,f604]) ).
fof(f1410,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| below(boole_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_POSet(X1))) ),
inference(forward_demodulation,[status(thm)],[f1384,f1397]) ).
fof(f1411,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ below(boole_lattice(X1),X0,X2)
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_POSet(X1))) ),
inference(forward_demodulation,[status(thm)],[f1384,f1398]) ).
fof(f1414,plain,
! [X0,X1] :
( cast_to_el_of_LattPOSet(boole_lattice(X0),X1) = X1
| ~ element(X1,the_carrier(boole_POSet(X0)))
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(paramodulation,[status(thm)],[f1384,f209]) ).
fof(f1419,plain,
! [X0,X1] :
( cast_to_el_of_LattPOSet(boole_lattice(X0),X1) = X1
| ~ element(X1,the_carrier(boole_POSet(X0)))
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1414,f281]) ).
fof(f1424,plain,
! [X0] :
( ~ subset(sK29_skl,X0)
| below(boole_lattice(sK28_skl),sK29_skl,X0)
| ~ element(X0,the_carrier(boole_POSet(sK28_skl))) ),
inference(resolution,[status(thm)],[f1410,f611]) ).
fof(f1555,plain,
! [X0,X1,X2] :
( ~ related_reflexive(boole_POSet(X0),cast_to_el_of_LattPOSet(boole_lattice(X0),X1),cast_to_el_of_LattPOSet(boole_lattice(X0),X2))
| below_refl(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(paramodulation,[status(thm)],[f207,f633]) ).
fof(f1556,plain,
! [X0,X1,X2] :
( ~ related_reflexive(boole_POSet(X0),cast_to_el_of_LattPOSet(boole_lattice(X0),X1),cast_to_el_of_LattPOSet(boole_lattice(X0),X2))
| below_refl(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_POSet(X0)))
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(forward_demodulation,[status(thm)],[f1384,f1555]) ).
fof(f1557,plain,
! [X0,X1,X2] :
( ~ related_reflexive(boole_POSet(X0),cast_to_el_of_LattPOSet(boole_lattice(X0),X1),cast_to_el_of_LattPOSet(boole_lattice(X0),X2))
| below_refl(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_POSet(X0)))
| ~ element(X1,the_carrier(boole_POSet(X0)))
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0))
| empty_carrier(boole_lattice(X0)) ),
inference(forward_demodulation,[status(thm)],[f1384,f1556]) ).
fof(f1558,plain,
! [X0,X1,X2] :
( ~ related_reflexive(boole_POSet(X0),cast_to_el_of_LattPOSet(boole_lattice(X0),X1),cast_to_el_of_LattPOSet(boole_lattice(X0),X2))
| below_refl(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_POSet(X0)))
| ~ element(X1,the_carrier(boole_POSet(X0)))
| ~ latt_str(boole_lattice(X0))
| ~ lattice(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1557,f281]) ).
fof(f1965,plain,
( cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK30_skl) = sK30_skl
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f1419,f612]) ).
fof(f1966,plain,
( cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK29_skl) = sK29_skl
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f1419,f611]) ).
fof(f1968,plain,
( cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK30_skl) = sK30_skl
| ~ latt_str(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1965,f289]) ).
fof(f1969,plain,
( cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK29_skl) = sK29_skl
| ~ latt_str(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1966,f289]) ).
fof(f1970,plain,
cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK30_skl) = sK30_skl,
inference(resolution,[status(thm)],[f1968,f223]) ).
fof(f1974,plain,
! [X0] :
( ~ related_reflexive(boole_POSet(sK28_skl),cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),X0),sK30_skl)
| below_refl(boole_lattice(sK28_skl),X0,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(X0,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl)) ),
inference(paramodulation,[status(thm)],[f1970,f1558]) ).
fof(f1978,plain,
! [X0] :
( ~ related_reflexive(boole_POSet(sK28_skl),cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),X0),sK30_skl)
| below_refl(boole_lattice(sK28_skl),X0,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(X0,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1974,f289]) ).
fof(f1986,plain,
cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK29_skl) = sK29_skl,
inference(resolution,[status(thm)],[f1969,f223]) ).
fof(f2080,plain,
( ~ related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl)
| below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl)) ),
inference(paramodulation,[status(thm)],[f1986,f1978]) ).
fof(f2083,plain,
( ~ related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl)
| below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2080,f223]) ).
fof(f2110,plain,
( subset(sK29_skl,sK30_skl)
| below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl))) ),
inference(resolution,[status(thm)],[f2083,f613]) ).
fof(f2111,plain,
( subset(sK29_skl,sK30_skl)
| below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2110,f611]) ).
fof(f2112,plain,
( subset(sK29_skl,sK30_skl)
| below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl) ),
inference(resolution,[status(thm)],[f2111,f612]) ).
fof(f2120,plain,
( below(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_lattice(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_lattice(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl))
| subset(sK29_skl,sK30_skl) ),
inference(resolution,[status(thm)],[f2112,f586]) ).
fof(f2126,plain,
( below(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_lattice(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl))
| subset(sK29_skl,sK30_skl) ),
inference(forward_demodulation,[status(thm)],[f1384,f2120]) ).
fof(f2127,plain,
( below(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl))
| subset(sK29_skl,sK30_skl) ),
inference(forward_demodulation,[status(thm)],[f1384,f2126]) ).
fof(f2128,plain,
( below(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2127,f1424]) ).
fof(f2207,plain,
( below(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f2128,f612]) ).
fof(f2208,plain,
( below(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2207,f281]) ).
fof(f2209,plain,
( below(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f2208,f611]) ).
fof(f2210,plain,
( below(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2209,f285]) ).
fof(f2251,plain,
( below(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ latt_str(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f2210,f288]) ).
fof(f2252,plain,
( below(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ latt_str(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2251,f287]) ).
fof(f2253,plain,
below(boole_lattice(sK28_skl),sK29_skl,sK30_skl),
inference(resolution,[status(thm)],[f2252,f223]) ).
fof(f2254,plain,
( subset(sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl))) ),
inference(resolution,[status(thm)],[f2253,f1411]) ).
fof(f2255,plain,
( below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_lattice(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_lattice(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f2253,f587]) ).
fof(f2256,plain,
( subset(sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2254,f611]) ).
fof(f2257,plain,
( below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_lattice(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(forward_demodulation,[status(thm)],[f1384,f2255]) ).
fof(f2258,plain,
( below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(forward_demodulation,[status(thm)],[f1384,f2257]) ).
fof(f2259,plain,
( below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2258,f281]) ).
fof(f2283,plain,
subset(sK29_skl,sK30_skl),
inference(resolution,[status(thm)],[f2256,f612]) ).
fof(f2284,plain,
~ related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl),
inference(backward_subsumption_resolution,[status(thm)],[f614,f2283]) ).
fof(f2328,plain,
( below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl))
| ~ meet_commutative(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f2259,f612]) ).
fof(f2329,plain,
( below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2328,f285]) ).
fof(f2330,plain,
( below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl))
| ~ meet_absorbing(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f2329,f611]) ).
fof(f2331,plain,
( below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ latt_str(boole_lattice(sK28_skl))
| ~ join_absorbing(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2330,f287]) ).
fof(f2376,plain,
( below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl)
| ~ latt_str(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f2331,f288]) ).
fof(f2377,plain,
below_refl(boole_lattice(sK28_skl),sK29_skl,sK30_skl),
inference(forward_subsumption_resolution,[status(thm)],[f2376,f223]) ).
fof(f2378,plain,
( related_reflexive(poset_of_lattice(boole_lattice(sK28_skl)),cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK29_skl),cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK30_skl))
| ~ element(sK30_skl,the_carrier(boole_lattice(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_lattice(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f2377,f632]) ).
fof(f2380,plain,
( related_reflexive(poset_of_lattice(boole_lattice(sK28_skl)),cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK29_skl),cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK30_skl))
| ~ element(sK30_skl,the_carrier(boole_lattice(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(forward_demodulation,[status(thm)],[f1384,f2378]) ).
fof(f2381,plain,
( related_reflexive(poset_of_lattice(boole_lattice(sK28_skl)),cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK29_skl),cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK30_skl))
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(forward_demodulation,[status(thm)],[f1384,f2380]) ).
fof(f2382,plain,
( related_reflexive(boole_POSet(sK28_skl),cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK29_skl),cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK30_skl))
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(forward_demodulation,[status(thm)],[f207,f2381]) ).
fof(f2383,plain,
( related_reflexive(boole_POSet(sK28_skl),sK29_skl,cast_to_el_of_LattPOSet(boole_lattice(sK28_skl),sK30_skl))
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(forward_demodulation,[status(thm)],[f1986,f2382]) ).
fof(f2384,plain,
( related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl))
| empty_carrier(boole_lattice(sK28_skl)) ),
inference(forward_demodulation,[status(thm)],[f1970,f2383]) ).
fof(f2385,plain,
( related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK30_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2384,f281]) ).
fof(f2388,plain,
( related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl))
| ~ lattice(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f2385,f612]) ).
fof(f2389,plain,
( related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl)
| ~ element(sK29_skl,the_carrier(boole_POSet(sK28_skl)))
| ~ latt_str(boole_lattice(sK28_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2388,f289]) ).
fof(f2419,plain,
( related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl)
| ~ latt_str(boole_lattice(sK28_skl)) ),
inference(resolution,[status(thm)],[f2389,f611]) ).
fof(f2421,plain,
related_reflexive(boole_POSet(sK28_skl),sK29_skl,sK30_skl),
inference(forward_subsumption_resolution,[status(thm)],[f2419,f223]) ).
fof(f2422,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f2284,f2421]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU369+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/5.62 % Computer : n017.cluster.edu
% 0.15/5.62 % Model : x86_64 x86_64
% 0.15/5.62 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.62 % Memory : 8046.5625MB
% 0.15/5.62 % OS : Linux 6.8.0-71-generic
% 0.15/5.63 % CPULimit : 300
% 0.15/5.63 % WCLimit : 300
% 0.15/5.63 % DateTime : Mon Sep 21 06:11:32 UTC 2026
% 0.15/5.63 % CPUTime :
% 0.15/5.65 % Drodi V4.1.1
% 0.20/5.86 % Refutation found
% 0.20/5.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/5.86 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.20/5.90 % Elapsed time: 0.254347 seconds
% 0.20/5.90 % CPU time: 1.654084 seconds
% 0.20/5.90 % Total memory used: 140.644 MB
% 0.20/5.90 % Net memory used: 140.000 MB
%------------------------------------------------------------------------------