%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEU369+1 : TPTP v9.2.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:12:05 PM UTC 2026
% Result : Theorem 4.25s 3.33s
% Output : CNFRefutation 4.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of formulae : 80 ( 16 unt; 0 def)
% Number of atoms : 382 ( 29 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 462 ( 160 ~; 168 |; 99 &)
% ( 8 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 32 ( 30 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-2 aty)
% Number of variables : 134 ( 9 sgn 67 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(redefinition_m2_relset_1,axiom,
! [X1,X2,X3] :
( relation_of2_as_subset(X3,X1,X2)
<=> relation_of2(X3,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(dt_u1_orders_2,axiom,
! [X1] :
( rel_str(X1)
=> relation_of2_as_subset(the_InternalRel(X1),the_carrier(X1),the_carrier(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_orders_2) ).
fof(t7_lattice3,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ! [X3] :
( element(X3,the_carrier(X1))
=> ( below_refl(X1,X2,X3)
<=> related_reflexive(poset_of_lattice(X1),cast_to_el_of_LattPOSet(X1,X2),cast_to_el_of_LattPOSet(X1,X3)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_lattice3) ).
fof(d3_lattice3,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> cast_to_el_of_LattPOSet(X1,X2) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_lattice3) ).
fof(free_g1_orders_2,axiom,
! [X1,X2] :
( relation_of2(X2,X1,X1)
=> ! [X3,X4] :
( rel_str_of(X1,X2) = rel_str_of(X3,X4)
=> ( X1 = X3
& X2 = X4 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',free_g1_orders_2) ).
fof(t2_yellow_1,conjecture,
! [X1,X2] :
( element(X2,the_carrier(boole_POSet(X1)))
=> ! [X3] :
( element(X3,the_carrier(boole_POSet(X1)))
=> ( related_reflexive(boole_POSet(X1),X2,X3)
<=> subset(X2,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_yellow_1) ).
fof(redefinition_r3_lattices,axiom,
! [X1,X2,X3] :
( ( ~ empty_carrier(X1)
& meet_commutative(X1)
& meet_absorbing(X1)
& join_absorbing(X1)
& latt_str(X1)
& element(X2,the_carrier(X1))
& element(X3,the_carrier(X1)) )
=> ( below_refl(X1,X2,X3)
<=> below(X1,X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r3_lattices) ).
fof(fc1_knaster,axiom,
! [X1] :
( ~ empty_carrier(boole_lattice(X1))
& strict_latt_str(boole_lattice(X1))
& join_commutative(boole_lattice(X1))
& join_associative(boole_lattice(X1))
& meet_commutative(boole_lattice(X1))
& meet_associative(boole_lattice(X1))
& meet_absorbing(boole_lattice(X1))
& join_absorbing(boole_lattice(X1))
& lattice(boole_lattice(X1))
& distributive_lattstr(boole_lattice(X1))
& modular_lattstr(boole_lattice(X1))
& lower_bounded_semilattstr(boole_lattice(X1))
& upper_bounded_semilattstr(boole_lattice(X1))
& bounded_lattstr(boole_lattice(X1))
& complemented_lattstr(boole_lattice(X1))
& boolean_lattstr(boole_lattice(X1))
& complete_latt_str(boole_lattice(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_knaster) ).
fof(abstractness_v1_orders_2,axiom,
! [X1] :
( rel_str(X1)
=> ( strict_rel_str(X1)
=> X1 = rel_str_of(the_carrier(X1),the_InternalRel(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v1_orders_2) ).
fof(d2_yellow_1,axiom,
! [X1] : boole_POSet(X1) = poset_of_lattice(boole_lattice(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_yellow_1) ).
fof(t2_lattice3,axiom,
! [X1,X2] :
( element(X2,the_carrier(boole_lattice(X1)))
=> ! [X3] :
( element(X3,the_carrier(boole_lattice(X1)))
=> ( below(boole_lattice(X1),X2,X3)
<=> subset(X2,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_lattice3) ).
fof(dt_k1_lattice3,axiom,
! [X1] :
( strict_latt_str(boole_lattice(X1))
& latt_str(boole_lattice(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice3) ).
fof(d2_lattice3,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> poset_of_lattice(X1) = rel_str_of(the_carrier(X1),k2_lattice3(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_lattice3) ).
fof(dt_k3_lattice3,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ( strict_rel_str(poset_of_lattice(X1))
& reflexive_relstr(poset_of_lattice(X1))
& transitive_relstr(poset_of_lattice(X1))
& antisymmetric_relstr(poset_of_lattice(X1))
& rel_str(poset_of_lattice(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_lattice3) ).
fof(c_0_14,plain,
! [X314,X315,X316] :
( ( ~ relation_of2_as_subset(X316,X314,X315)
| relation_of2(X316,X314,X315) )
& ( ~ relation_of2(X316,X314,X315)
| relation_of2_as_subset(X316,X314,X315) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[redefinition_m2_relset_1])]) ).
fof(c_0_15,plain,
! [X235] :
( ~ rel_str(X235)
| relation_of2_as_subset(the_InternalRel(X235),the_carrier(X235),the_carrier(X235)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_u1_orders_2])]) ).
fof(c_0_16,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ! [X3] :
( element(X3,the_carrier(X1))
=> ( below_refl(X1,X2,X3)
<=> related_reflexive(poset_of_lattice(X1),cast_to_el_of_LattPOSet(X1,X2),cast_to_el_of_LattPOSet(X1,X3)) ) ) ) ),
inference(fof_simplification,[status(thm)],[t7_lattice3]) ).
fof(c_0_17,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> cast_to_el_of_LattPOSet(X1,X2) = X2 ) ),
inference(fof_simplification,[status(thm)],[d3_lattice3]) ).
fof(c_0_18,plain,
! [X278,X279,X280,X281] :
( ( X278 = X280
| rel_str_of(X278,X279) != rel_str_of(X280,X281)
| ~ relation_of2(X279,X278,X278) )
& ( X279 = X281
| rel_str_of(X278,X279) != rel_str_of(X280,X281)
| ~ relation_of2(X279,X278,X278) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[free_g1_orders_2])])])]) ).
cnf(c_0_19,plain,
( relation_of2(X1,X2,X3)
| ~ relation_of2_as_subset(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_20,plain,
( relation_of2_as_subset(the_InternalRel(X1),the_carrier(X1),the_carrier(X1))
| ~ rel_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
fof(c_0_21,plain,
! [X351,X352,X353] :
( ( ~ below_refl(X351,X352,X353)
| related_reflexive(poset_of_lattice(X351),cast_to_el_of_LattPOSet(X351,X352),cast_to_el_of_LattPOSet(X351,X353))
| ~ element(X353,the_carrier(X351))
| ~ element(X352,the_carrier(X351))
| empty_carrier(X351)
| ~ lattice(X351)
| ~ latt_str(X351) )
& ( ~ related_reflexive(poset_of_lattice(X351),cast_to_el_of_LattPOSet(X351,X352),cast_to_el_of_LattPOSet(X351,X353))
| below_refl(X351,X352,X353)
| ~ element(X353,the_carrier(X351))
| ~ element(X352,the_carrier(X351))
| empty_carrier(X351)
| ~ lattice(X351)
| ~ latt_str(X351) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])]) ).
fof(c_0_22,plain,
! [X208,X209] :
( empty_carrier(X208)
| ~ lattice(X208)
| ~ latt_str(X208)
| ~ element(X209,the_carrier(X208))
| cast_to_el_of_LattPOSet(X208,X209) = X209 ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_17])])]) ).
fof(c_0_23,negated_conjecture,
~ ! [X1,X2] :
( element(X2,the_carrier(boole_POSet(X1)))
=> ! [X3] :
( element(X3,the_carrier(boole_POSet(X1)))
=> ( related_reflexive(boole_POSet(X1),X2,X3)
<=> subset(X2,X3) ) ) ),
inference(assume_negation,[status(cth)],[t2_yellow_1]) ).
fof(c_0_24,plain,
! [X1,X2,X3] :
( ( ~ empty_carrier(X1)
& meet_commutative(X1)
& meet_absorbing(X1)
& join_absorbing(X1)
& latt_str(X1)
& element(X2,the_carrier(X1))
& element(X3,the_carrier(X1)) )
=> ( below_refl(X1,X2,X3)
<=> below(X1,X2,X3) ) ),
inference(fof_simplification,[status(thm)],[redefinition_r3_lattices]) ).
fof(c_0_25,plain,
! [X1] :
( ~ empty_carrier(boole_lattice(X1))
& strict_latt_str(boole_lattice(X1))
& join_commutative(boole_lattice(X1))
& join_associative(boole_lattice(X1))
& meet_commutative(boole_lattice(X1))
& meet_associative(boole_lattice(X1))
& meet_absorbing(boole_lattice(X1))
& join_absorbing(boole_lattice(X1))
& lattice(boole_lattice(X1))
& distributive_lattstr(boole_lattice(X1))
& modular_lattstr(boole_lattice(X1))
& lower_bounded_semilattstr(boole_lattice(X1))
& upper_bounded_semilattstr(boole_lattice(X1))
& bounded_lattstr(boole_lattice(X1))
& complemented_lattstr(boole_lattice(X1))
& boolean_lattstr(boole_lattice(X1))
& complete_latt_str(boole_lattice(X1)) ),
inference(fof_simplification,[status(thm)],[fc1_knaster]) ).
cnf(c_0_26,plain,
( X1 = X2
| rel_str_of(X1,X3) != rel_str_of(X2,X4)
| ~ relation_of2(X3,X1,X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_27,plain,
( relation_of2(the_InternalRel(X1),the_carrier(X1),the_carrier(X1))
| ~ rel_str(X1) ),
inference(spm,[status(thm)],[c_0_19,c_0_20]) ).
fof(c_0_28,plain,
! [X182] :
( ~ rel_str(X182)
| ~ strict_rel_str(X182)
| X182 = rel_str_of(the_carrier(X182),the_InternalRel(X182)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[abstractness_v1_orders_2])]) ).
cnf(c_0_29,plain,
( below_refl(X1,X2,X3)
| empty_carrier(X1)
| ~ related_reflexive(poset_of_lattice(X1),cast_to_el_of_LattPOSet(X1,X2),cast_to_el_of_LattPOSet(X1,X3))
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_30,plain,
( empty_carrier(X1)
| cast_to_el_of_LattPOSet(X1,X2) = X2
| ~ lattice(X1)
| ~ latt_str(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
fof(c_0_31,negated_conjecture,
( element(esk30_0,the_carrier(boole_POSet(esk29_0)))
& element(esk31_0,the_carrier(boole_POSet(esk29_0)))
& ( ~ related_reflexive(boole_POSet(esk29_0),esk30_0,esk31_0)
| ~ subset(esk30_0,esk31_0) )
& ( related_reflexive(boole_POSet(esk29_0),esk30_0,esk31_0)
| subset(esk30_0,esk31_0) ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_23])])]) ).
fof(c_0_32,plain,
! [X207] : boole_POSet(X207) = poset_of_lattice(boole_lattice(X207)),
inference(variable_rename,[status(thm)],[d2_yellow_1]) ).
fof(c_0_33,plain,
! [X332,X333,X334] :
( ( ~ below(boole_lattice(X332),X333,X334)
| subset(X333,X334)
| ~ element(X334,the_carrier(boole_lattice(X332)))
| ~ element(X333,the_carrier(boole_lattice(X332))) )
& ( ~ subset(X333,X334)
| below(boole_lattice(X332),X333,X334)
| ~ element(X334,the_carrier(boole_lattice(X332)))
| ~ element(X333,the_carrier(boole_lattice(X332))) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_lattice3])])])]) ).
fof(c_0_34,plain,
! [X317,X318,X319] :
( ( ~ below_refl(X317,X318,X319)
| below(X317,X318,X319)
| empty_carrier(X317)
| ~ meet_commutative(X317)
| ~ meet_absorbing(X317)
| ~ join_absorbing(X317)
| ~ latt_str(X317)
| ~ element(X318,the_carrier(X317))
| ~ element(X319,the_carrier(X317)) )
& ( ~ below(X317,X318,X319)
| below_refl(X317,X318,X319)
| empty_carrier(X317)
| ~ meet_commutative(X317)
| ~ meet_absorbing(X317)
| ~ join_absorbing(X317)
| ~ latt_str(X317)
| ~ element(X318,the_carrier(X317))
| ~ element(X319,the_carrier(X317)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_24])])]) ).
fof(c_0_35,plain,
! [X250] :
( ~ empty_carrier(boole_lattice(X250))
& strict_latt_str(boole_lattice(X250))
& join_commutative(boole_lattice(X250))
& join_associative(boole_lattice(X250))
& meet_commutative(boole_lattice(X250))
& meet_associative(boole_lattice(X250))
& meet_absorbing(boole_lattice(X250))
& join_absorbing(boole_lattice(X250))
& lattice(boole_lattice(X250))
& distributive_lattstr(boole_lattice(X250))
& modular_lattstr(boole_lattice(X250))
& lower_bounded_semilattstr(boole_lattice(X250))
& upper_bounded_semilattstr(boole_lattice(X250))
& bounded_lattstr(boole_lattice(X250))
& complemented_lattstr(boole_lattice(X250))
& boolean_lattstr(boole_lattice(X250))
& complete_latt_str(boole_lattice(X250)) ),
inference(variable_rename,[status(thm)],[c_0_25]) ).
fof(c_0_36,plain,
! [X220] :
( strict_latt_str(boole_lattice(X220))
& latt_str(boole_lattice(X220)) ),
inference(variable_rename,[status(thm)],[dt_k1_lattice3]) ).
cnf(c_0_37,plain,
( the_carrier(X1) = X2
| rel_str_of(the_carrier(X1),the_InternalRel(X1)) != rel_str_of(X2,X3)
| ~ rel_str(X1) ),
inference(spm,[status(thm)],[c_0_26,c_0_27]) ).
cnf(c_0_38,plain,
( X1 = rel_str_of(the_carrier(X1),the_InternalRel(X1))
| ~ rel_str(X1)
| ~ strict_rel_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
fof(c_0_39,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> poset_of_lattice(X1) = rel_str_of(the_carrier(X1),k2_lattice3(X1)) ),
inference(fof_simplification,[status(thm)],[d2_lattice3]) ).
fof(c_0_40,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ( strict_rel_str(poset_of_lattice(X1))
& reflexive_relstr(poset_of_lattice(X1))
& transitive_relstr(poset_of_lattice(X1))
& antisymmetric_relstr(poset_of_lattice(X1))
& rel_str(poset_of_lattice(X1)) ) ),
inference(fof_simplification,[status(thm)],[dt_k3_lattice3]) ).
cnf(c_0_41,plain,
( related_reflexive(poset_of_lattice(X1),cast_to_el_of_LattPOSet(X1,X2),cast_to_el_of_LattPOSet(X1,X3))
| empty_carrier(X1)
| ~ below_refl(X1,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_42,plain,
( below_refl(X1,X2,X3)
| empty_carrier(X1)
| ~ related_reflexive(poset_of_lattice(X1),X2,cast_to_el_of_LattPOSet(X1,X3))
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
cnf(c_0_43,negated_conjecture,
( related_reflexive(boole_POSet(esk29_0),esk30_0,esk31_0)
| subset(esk30_0,esk31_0) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_44,plain,
boole_POSet(X1) = poset_of_lattice(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_45,plain,
( subset(X2,X3)
| ~ below(boole_lattice(X1),X2,X3)
| ~ element(X3,the_carrier(boole_lattice(X1)))
| ~ element(X2,the_carrier(boole_lattice(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
cnf(c_0_46,plain,
( below(X1,X2,X3)
| empty_carrier(X1)
| ~ below_refl(X1,X2,X3)
| ~ meet_commutative(X1)
| ~ meet_absorbing(X1)
| ~ join_absorbing(X1)
| ~ latt_str(X1)
| ~ element(X2,the_carrier(X1))
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_47,plain,
join_absorbing(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_48,plain,
meet_absorbing(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_49,plain,
meet_commutative(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_50,plain,
latt_str(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_51,plain,
~ empty_carrier(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_52,plain,
( the_carrier(X1) = X2
| X1 != rel_str_of(X2,X3)
| ~ strict_rel_str(X1)
| ~ rel_str(X1) ),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
fof(c_0_53,plain,
! [X206] :
( empty_carrier(X206)
| ~ lattice(X206)
| ~ latt_str(X206)
| poset_of_lattice(X206) = rel_str_of(the_carrier(X206),k2_lattice3(X206)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_39])]) ).
fof(c_0_54,plain,
! [X222] :
( ( strict_rel_str(poset_of_lattice(X222))
| empty_carrier(X222)
| ~ lattice(X222)
| ~ latt_str(X222) )
& ( reflexive_relstr(poset_of_lattice(X222))
| empty_carrier(X222)
| ~ lattice(X222)
| ~ latt_str(X222) )
& ( transitive_relstr(poset_of_lattice(X222))
| empty_carrier(X222)
| ~ lattice(X222)
| ~ latt_str(X222) )
& ( antisymmetric_relstr(poset_of_lattice(X222))
| empty_carrier(X222)
| ~ lattice(X222)
| ~ latt_str(X222) )
& ( rel_str(poset_of_lattice(X222))
| empty_carrier(X222)
| ~ lattice(X222)
| ~ latt_str(X222) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_40])])]) ).
cnf(c_0_55,negated_conjecture,
( ~ related_reflexive(boole_POSet(esk29_0),esk30_0,esk31_0)
| ~ subset(esk30_0,esk31_0) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_56,plain,
( related_reflexive(poset_of_lattice(X1),cast_to_el_of_LattPOSet(X1,X2),X3)
| empty_carrier(X1)
| ~ below_refl(X1,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(spm,[status(thm)],[c_0_41,c_0_30]) ).
cnf(c_0_57,plain,
( below_refl(X1,X2,X3)
| empty_carrier(X1)
| ~ below(X1,X2,X3)
| ~ meet_commutative(X1)
| ~ meet_absorbing(X1)
| ~ join_absorbing(X1)
| ~ latt_str(X1)
| ~ element(X2,the_carrier(X1))
| ~ element(X3,the_carrier(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_58,plain,
( below(boole_lattice(X3),X1,X2)
| ~ subset(X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X3)))
| ~ element(X1,the_carrier(boole_lattice(X3))) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
cnf(c_0_59,plain,
( below_refl(X1,X2,X3)
| empty_carrier(X1)
| ~ related_reflexive(poset_of_lattice(X1),X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(spm,[status(thm)],[c_0_42,c_0_30]) ).
cnf(c_0_60,negated_conjecture,
( subset(esk30_0,esk31_0)
| related_reflexive(poset_of_lattice(boole_lattice(esk29_0)),esk30_0,esk31_0) ),
inference(rw,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_61,plain,
lattice(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_62,plain,
( subset(X1,X2)
| ~ below_refl(boole_lattice(X3),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X3)))
| ~ element(X1,the_carrier(boole_lattice(X3))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_46]),c_0_47]),c_0_48]),c_0_49]),c_0_50])]),c_0_51]) ).
cnf(c_0_63,negated_conjecture,
element(esk30_0,the_carrier(boole_POSet(esk29_0))),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_64,plain,
( the_carrier(rel_str_of(X1,X2)) = X1
| ~ strict_rel_str(rel_str_of(X1,X2))
| ~ rel_str(rel_str_of(X1,X2)) ),
inference(er,[status(thm)],[c_0_52]) ).
cnf(c_0_65,plain,
( empty_carrier(X1)
| poset_of_lattice(X1) = rel_str_of(the_carrier(X1),k2_lattice3(X1))
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
cnf(c_0_66,plain,
( rel_str(poset_of_lattice(X1))
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_54]) ).
cnf(c_0_67,plain,
( strict_rel_str(poset_of_lattice(X1))
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_54]) ).
cnf(c_0_68,negated_conjecture,
element(esk31_0,the_carrier(boole_POSet(esk29_0))),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_69,negated_conjecture,
( ~ subset(esk30_0,esk31_0)
| ~ related_reflexive(poset_of_lattice(boole_lattice(esk29_0)),esk30_0,esk31_0) ),
inference(rw,[status(thm)],[c_0_55,c_0_44]) ).
cnf(c_0_70,plain,
( related_reflexive(poset_of_lattice(X1),X2,X3)
| empty_carrier(X1)
| ~ below_refl(X1,X2,X3)
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(spm,[status(thm)],[c_0_56,c_0_30]) ).
cnf(c_0_71,plain,
( below_refl(boole_lattice(X1),X2,X3)
| ~ subset(X2,X3)
| ~ element(X3,the_carrier(boole_lattice(X1)))
| ~ element(X2,the_carrier(boole_lattice(X1))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_58]),c_0_47]),c_0_48]),c_0_49]),c_0_50])]),c_0_51]) ).
cnf(c_0_72,negated_conjecture,
( subset(esk30_0,esk31_0)
| ~ element(esk31_0,the_carrier(boole_lattice(esk29_0)))
| ~ element(esk30_0,the_carrier(boole_lattice(esk29_0))) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_60]),c_0_61]),c_0_50])]),c_0_51]),c_0_62]) ).
cnf(c_0_73,negated_conjecture,
element(esk30_0,the_carrier(poset_of_lattice(boole_lattice(esk29_0)))),
inference(rw,[status(thm)],[c_0_63,c_0_44]) ).
cnf(c_0_74,plain,
( the_carrier(poset_of_lattice(X1)) = the_carrier(X1)
| empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_64,c_0_65]),c_0_66]),c_0_67]) ).
cnf(c_0_75,negated_conjecture,
element(esk31_0,the_carrier(poset_of_lattice(boole_lattice(esk29_0)))),
inference(rw,[status(thm)],[c_0_68,c_0_44]) ).
cnf(c_0_76,negated_conjecture,
( ~ element(esk31_0,the_carrier(boole_lattice(esk29_0)))
| ~ element(esk30_0,the_carrier(boole_lattice(esk29_0))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_70]),c_0_61]),c_0_50])]),c_0_51]),c_0_71]),c_0_72]) ).
cnf(c_0_77,negated_conjecture,
element(esk30_0,the_carrier(boole_lattice(esk29_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_74]),c_0_61]),c_0_50])]),c_0_51]) ).
cnf(c_0_78,negated_conjecture,
element(esk31_0,the_carrier(boole_lattice(esk29_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_74]),c_0_61]),c_0_50])]),c_0_51]) ).
cnf(c_0_79,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_76,c_0_77])]),c_0_78])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU369+1 : TPTP v9.2.1. Released v3.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n005.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 03:00:45 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 4.25/3.33 % Version : CSE_E---1.7
% 4.25/3.33 % Problem : theBenchmark.p
% 4.25/3.33 % SZS status Theorem for theBenchmark.p
% 4.25/3.33 % SZS output start CNFRefutation
% See solution above
% 4.25/3.34 % Total time : 2.421s
%------------------------------------------------------------------------------