%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEU345+1 : TPTP v9.2.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n029.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:11:33 PM UTC 2026
% Result : Theorem 4.04s 3.20s
% Output : CNFRefutation 4.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of formulae : 66 ( 19 unt; 0 def)
% Number of atoms : 267 ( 81 equ)
% Maximal formula atoms : 32 ( 4 avg)
% Number of connectives : 327 ( 126 ~; 139 |; 38 &)
% ( 5 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 2 con; 0-3 aty)
% Number of variables : 104 ( 10 sgn 49 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d1_lattice3,axiom,
! [X1,X2] :
( ( strict_latt_str(X2)
& latt_str(X2) )
=> ( X2 = boole_lattice(X1)
<=> ( the_carrier(X2) = powerset(X1)
& ! [X3] :
( element(X3,powerset(X1))
=> ! [X4] :
( element(X4,powerset(X1))
=> ( apply_binary(the_L_join(X2),X3,X4) = subset_union2(X1,X3,X4)
& apply_binary(the_L_meet(X2),X3,X4) = subset_intersection2(X1,X3,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_lattice3) ).
fof(dt_k1_lattice3,axiom,
! [X1] :
( strict_latt_str(boole_lattice(X1))
& latt_str(boole_lattice(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice3) ).
fof(d13_lattices,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& meet_semilatt_str(X1) )
=> ( lower_bounded_semilattstr(X1)
<=> ? [X2] :
( element(X2,the_carrier(X1))
& ! [X3] :
( element(X3,the_carrier(X1))
=> ( meet(X1,X2,X3) = X2
& meet(X1,X3,X2) = X2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d13_lattices) ).
fof(dt_l3_lattices,axiom,
! [X1] :
( latt_str(X1)
=> ( meet_semilatt_str(X1)
& join_semilatt_str(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(fc1_lattice3,axiom,
! [X1] :
( ~ empty_carrier(boole_lattice(X1))
& strict_latt_str(boole_lattice(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice3) ).
fof(t1_lattice3,axiom,
! [X1,X2] :
( element(X2,the_carrier(boole_lattice(X1)))
=> ! [X3] :
( element(X3,the_carrier(boole_lattice(X1)))
=> ( join(boole_lattice(X1),X2,X3) = set_union2(X2,X3)
& meet(boole_lattice(X1),X2,X3) = set_intersection2(X2,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_lattice3) ).
fof(t6_boole,axiom,
! [X1] :
( empty(X1)
=> X1 = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(rc2_subset_1,axiom,
! [X1] :
? [X2] :
( element(X2,powerset(X1))
& empty(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_subset_1) ).
fof(d16_lattices,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& meet_semilatt_str(X1) )
=> ( lower_bounded_semilattstr(X1)
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ( X2 = bottom_of_semilattstr(X1)
<=> ! [X3] :
( element(X3,the_carrier(X1))
=> ( meet(X1,X2,X3) = X2
& meet(X1,X3,X2) = X2 ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_lattices) ).
fof(t2_boole,axiom,
! [X1] : set_intersection2(X1,empty_set) = empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_boole) ).
fof(commutativity_k3_xboole_0,axiom,
! [X1,X2] : set_intersection2(X1,X2) = set_intersection2(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(t3_lattice3,conjecture,
! [X1] :
( lower_bounded_semilattstr(boole_lattice(X1))
& bottom_of_semilattstr(boole_lattice(X1)) = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_lattice3) ).
fof(c_0_12,plain,
! [X224,X225,X226,X227] :
( ( the_carrier(X225) = powerset(X224)
| X225 != boole_lattice(X224)
| ~ strict_latt_str(X225)
| ~ latt_str(X225) )
& ( apply_binary(the_L_join(X225),X226,X227) = subset_union2(X224,X226,X227)
| ~ element(X227,powerset(X224))
| ~ element(X226,powerset(X224))
| X225 != boole_lattice(X224)
| ~ strict_latt_str(X225)
| ~ latt_str(X225) )
& ( apply_binary(the_L_meet(X225),X226,X227) = subset_intersection2(X224,X226,X227)
| ~ element(X227,powerset(X224))
| ~ element(X226,powerset(X224))
| X225 != boole_lattice(X224)
| ~ strict_latt_str(X225)
| ~ latt_str(X225) )
& ( element(esk4_2(X224,X225),powerset(X224))
| the_carrier(X225) != powerset(X224)
| X225 = boole_lattice(X224)
| ~ strict_latt_str(X225)
| ~ latt_str(X225) )
& ( element(esk5_2(X224,X225),powerset(X224))
| the_carrier(X225) != powerset(X224)
| X225 = boole_lattice(X224)
| ~ strict_latt_str(X225)
| ~ latt_str(X225) )
& ( apply_binary(the_L_join(X225),esk4_2(X224,X225),esk5_2(X224,X225)) != subset_union2(X224,esk4_2(X224,X225),esk5_2(X224,X225))
| apply_binary(the_L_meet(X225),esk4_2(X224,X225),esk5_2(X224,X225)) != subset_intersection2(X224,esk4_2(X224,X225),esk5_2(X224,X225))
| the_carrier(X225) != powerset(X224)
| X225 = boole_lattice(X224)
| ~ strict_latt_str(X225)
| ~ latt_str(X225) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[d1_lattice3])])])])]) ).
fof(c_0_13,plain,
! [X241] :
( strict_latt_str(boole_lattice(X241))
& latt_str(boole_lattice(X241)) ),
inference(variable_rename,[status(thm)],[dt_k1_lattice3]) ).
fof(c_0_14,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& meet_semilatt_str(X1) )
=> ( lower_bounded_semilattstr(X1)
<=> ? [X2] :
( element(X2,the_carrier(X1))
& ! [X3] :
( element(X3,the_carrier(X1))
=> ( meet(X1,X2,X3) = X2
& meet(X1,X3,X2) = X2 ) ) ) ) ),
inference(fof_simplification,[status(thm)],[d13_lattices]) ).
fof(c_0_15,plain,
! [X266] :
( ( meet_semilatt_str(X266)
| ~ latt_str(X266) )
& ( join_semilatt_str(X266)
| ~ latt_str(X266) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_l3_lattices])])]) ).
fof(c_0_16,plain,
! [X1] :
( ~ empty_carrier(boole_lattice(X1))
& strict_latt_str(boole_lattice(X1)) ),
inference(fof_simplification,[status(thm)],[fc1_lattice3]) ).
fof(c_0_17,plain,
! [X350,X351,X352] :
( ( join(boole_lattice(X350),X351,X352) = set_union2(X351,X352)
| ~ element(X352,the_carrier(boole_lattice(X350)))
| ~ element(X351,the_carrier(boole_lattice(X350))) )
& ( meet(boole_lattice(X350),X351,X352) = set_intersection2(X351,X352)
| ~ element(X352,the_carrier(boole_lattice(X350)))
| ~ element(X351,the_carrier(boole_lattice(X350))) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t1_lattice3])])])]) ).
cnf(c_0_18,plain,
( the_carrier(X1) = powerset(X2)
| X1 != boole_lattice(X2)
| ~ strict_latt_str(X1)
| ~ latt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_19,plain,
strict_latt_str(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_20,plain,
latt_str(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
fof(c_0_21,plain,
! [X212,X214,X215] :
( ( element(esk1_1(X212),the_carrier(X212))
| ~ lower_bounded_semilattstr(X212)
| empty_carrier(X212)
| ~ meet_semilatt_str(X212) )
& ( meet(X212,esk1_1(X212),X214) = esk1_1(X212)
| ~ element(X214,the_carrier(X212))
| ~ lower_bounded_semilattstr(X212)
| empty_carrier(X212)
| ~ meet_semilatt_str(X212) )
& ( meet(X212,X214,esk1_1(X212)) = esk1_1(X212)
| ~ element(X214,the_carrier(X212))
| ~ lower_bounded_semilattstr(X212)
| empty_carrier(X212)
| ~ meet_semilatt_str(X212) )
& ( element(esk2_2(X212,X215),the_carrier(X212))
| ~ element(X215,the_carrier(X212))
| lower_bounded_semilattstr(X212)
| empty_carrier(X212)
| ~ meet_semilatt_str(X212) )
& ( meet(X212,X215,esk2_2(X212,X215)) != X215
| meet(X212,esk2_2(X212,X215),X215) != X215
| ~ element(X215,the_carrier(X212))
| lower_bounded_semilattstr(X212)
| empty_carrier(X212)
| ~ meet_semilatt_str(X212) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_14])])])])]) ).
cnf(c_0_22,plain,
( meet_semilatt_str(X1)
| ~ latt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
fof(c_0_23,plain,
! [X284] :
( ~ empty_carrier(boole_lattice(X284))
& strict_latt_str(boole_lattice(X284)) ),
inference(variable_rename,[status(thm)],[c_0_16]) ).
fof(c_0_24,plain,
! [X368] :
( ~ empty(X368)
| X368 = empty_set ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6_boole])]) ).
fof(c_0_25,plain,
! [X321] :
( element(esk15_1(X321),powerset(X321))
& empty(esk15_1(X321)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_subset_1])]) ).
fof(c_0_26,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& meet_semilatt_str(X1) )
=> ( lower_bounded_semilattstr(X1)
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ( X2 = bottom_of_semilattstr(X1)
<=> ! [X3] :
( element(X3,the_carrier(X1))
=> ( meet(X1,X2,X3) = X2
& meet(X1,X3,X2) = X2 ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[d16_lattices]) ).
cnf(c_0_27,plain,
( meet(boole_lattice(X1),X2,X3) = set_intersection2(X2,X3)
| ~ element(X3,the_carrier(boole_lattice(X1)))
| ~ element(X2,the_carrier(boole_lattice(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_28,plain,
the_carrier(boole_lattice(X1)) = powerset(X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_18]),c_0_19]),c_0_20])]) ).
cnf(c_0_29,plain,
( element(esk1_1(X1),the_carrier(X1))
| empty_carrier(X1)
| ~ lower_bounded_semilattstr(X1)
| ~ meet_semilatt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_30,plain,
meet_semilatt_str(boole_lattice(X1)),
inference(spm,[status(thm)],[c_0_22,c_0_20]) ).
cnf(c_0_31,plain,
~ empty_carrier(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_32,plain,
( X1 = empty_set
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_33,plain,
empty(esk15_1(X1)),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
fof(c_0_34,plain,
! [X217,X218,X219] :
( ( meet(X217,X218,X219) = X218
| ~ element(X219,the_carrier(X217))
| X218 != bottom_of_semilattstr(X217)
| ~ element(X218,the_carrier(X217))
| ~ lower_bounded_semilattstr(X217)
| empty_carrier(X217)
| ~ meet_semilatt_str(X217) )
& ( meet(X217,X219,X218) = X218
| ~ element(X219,the_carrier(X217))
| X218 != bottom_of_semilattstr(X217)
| ~ element(X218,the_carrier(X217))
| ~ lower_bounded_semilattstr(X217)
| empty_carrier(X217)
| ~ meet_semilatt_str(X217) )
& ( element(esk3_2(X217,X218),the_carrier(X217))
| X218 = bottom_of_semilattstr(X217)
| ~ element(X218,the_carrier(X217))
| ~ lower_bounded_semilattstr(X217)
| empty_carrier(X217)
| ~ meet_semilatt_str(X217) )
& ( meet(X217,X218,esk3_2(X217,X218)) != X218
| meet(X217,esk3_2(X217,X218),X218) != X218
| X218 = bottom_of_semilattstr(X217)
| ~ element(X218,the_carrier(X217))
| ~ lower_bounded_semilattstr(X217)
| empty_carrier(X217)
| ~ meet_semilatt_str(X217) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_26])])])])]) ).
fof(c_0_35,plain,
! [X355] : set_intersection2(X355,empty_set) = empty_set,
inference(variable_rename,[status(thm)],[t2_boole]) ).
cnf(c_0_36,plain,
( meet(X1,esk1_1(X1),X2) = esk1_1(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ lower_bounded_semilattstr(X1)
| ~ meet_semilatt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_37,plain,
( meet(boole_lattice(X1),X2,X3) = set_intersection2(X2,X3)
| ~ element(X3,powerset(X1))
| ~ element(X2,powerset(X1)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_27,c_0_28]),c_0_28]) ).
cnf(c_0_38,plain,
( element(esk1_1(boole_lattice(X1)),powerset(X1))
| ~ lower_bounded_semilattstr(boole_lattice(X1)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_28]),c_0_30])]),c_0_31]) ).
cnf(c_0_39,plain,
element(esk15_1(X1),powerset(X1)),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_40,plain,
esk15_1(X1) = empty_set,
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_41,plain,
( X2 = bottom_of_semilattstr(X1)
| empty_carrier(X1)
| meet(X1,X2,esk3_2(X1,X2)) != X2
| meet(X1,esk3_2(X1,X2),X2) != X2
| ~ element(X2,the_carrier(X1))
| ~ lower_bounded_semilattstr(X1)
| ~ meet_semilatt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_42,plain,
( meet(X1,X2,esk1_1(X1)) = esk1_1(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ lower_bounded_semilattstr(X1)
| ~ meet_semilatt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_43,plain,
set_intersection2(X1,empty_set) = empty_set,
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_44,plain,
( set_intersection2(esk1_1(boole_lattice(X1)),X2) = esk1_1(boole_lattice(X1))
| ~ lower_bounded_semilattstr(boole_lattice(X1))
| ~ element(X2,powerset(X1)) ),
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_36,c_0_37]),c_0_30]),c_0_28])]),c_0_31]),c_0_38]) ).
cnf(c_0_45,plain,
element(empty_set,powerset(X1)),
inference(rw,[status(thm)],[c_0_39,c_0_40]) ).
fof(c_0_46,plain,
! [X201,X202] : set_intersection2(X201,X202) = set_intersection2(X202,X201),
inference(variable_rename,[status(thm)],[commutativity_k3_xboole_0]) ).
cnf(c_0_47,plain,
( element(esk2_2(X1,X2),the_carrier(X1))
| lower_bounded_semilattstr(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ meet_semilatt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
fof(c_0_48,negated_conjecture,
~ ! [X1] :
( lower_bounded_semilattstr(boole_lattice(X1))
& bottom_of_semilattstr(boole_lattice(X1)) = empty_set ),
inference(assume_negation,[status(cth)],[t3_lattice3]) ).
cnf(c_0_49,plain,
( esk1_1(X1) = bottom_of_semilattstr(X1)
| empty_carrier(X1)
| ~ lower_bounded_semilattstr(X1)
| ~ meet_semilatt_str(X1)
| ~ element(esk3_2(X1,esk1_1(X1)),the_carrier(X1)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_41,c_0_42]),c_0_29]),c_0_36]) ).
cnf(c_0_50,plain,
( esk1_1(boole_lattice(X1)) = empty_set
| ~ lower_bounded_semilattstr(boole_lattice(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_44]),c_0_45])]) ).
cnf(c_0_51,plain,
( element(esk3_2(X1,X2),the_carrier(X1))
| X2 = bottom_of_semilattstr(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ lower_bounded_semilattstr(X1)
| ~ meet_semilatt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_52,plain,
( lower_bounded_semilattstr(X1)
| empty_carrier(X1)
| meet(X1,X2,esk2_2(X1,X2)) != X2
| meet(X1,esk2_2(X1,X2),X2) != X2
| ~ element(X2,the_carrier(X1))
| ~ meet_semilatt_str(X1) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_53,plain,
set_intersection2(X1,X2) = set_intersection2(X2,X1),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
cnf(c_0_54,plain,
( lower_bounded_semilattstr(boole_lattice(X1))
| element(esk2_2(boole_lattice(X1),X2),powerset(X1))
| ~ element(X2,powerset(X1)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47,c_0_28]),c_0_30])]),c_0_31]) ).
fof(c_0_55,negated_conjecture,
( ~ lower_bounded_semilattstr(boole_lattice(esk22_0))
| bottom_of_semilattstr(boole_lattice(esk22_0)) != empty_set ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_48])])]) ).
cnf(c_0_56,plain,
( bottom_of_semilattstr(boole_lattice(X1)) = empty_set
| ~ lower_bounded_semilattstr(boole_lattice(X1))
| ~ element(esk3_2(boole_lattice(X1),empty_set),powerset(X1)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_50]),c_0_30]),c_0_28])]),c_0_31]) ).
cnf(c_0_57,plain,
( X1 = bottom_of_semilattstr(boole_lattice(X2))
| element(esk3_2(boole_lattice(X2),X1),powerset(X2))
| ~ lower_bounded_semilattstr(boole_lattice(X2))
| ~ element(X1,powerset(X2)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_28]),c_0_30])]),c_0_31]) ).
cnf(c_0_58,plain,
( lower_bounded_semilattstr(boole_lattice(X1))
| meet(boole_lattice(X1),X2,esk2_2(boole_lattice(X1),X2)) != X2
| set_intersection2(X2,esk2_2(boole_lattice(X1),X2)) != X2
| ~ element(X2,powerset(X1)) ),
inference(csr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_37]),c_0_30]),c_0_28])]),c_0_31]),c_0_53]),c_0_54]) ).
cnf(c_0_59,negated_conjecture,
( ~ lower_bounded_semilattstr(boole_lattice(esk22_0))
| bottom_of_semilattstr(boole_lattice(esk22_0)) != empty_set ),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
cnf(c_0_60,plain,
( bottom_of_semilattstr(boole_lattice(X1)) = empty_set
| ~ lower_bounded_semilattstr(boole_lattice(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_57]),c_0_45])]) ).
cnf(c_0_61,plain,
( lower_bounded_semilattstr(boole_lattice(X1))
| set_intersection2(X2,esk2_2(boole_lattice(X1),X2)) != X2
| ~ element(X2,powerset(X1)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58,c_0_37]),c_0_54]) ).
cnf(c_0_62,plain,
set_intersection2(empty_set,X1) = empty_set,
inference(spm,[status(thm)],[c_0_43,c_0_53]) ).
cnf(c_0_63,negated_conjecture,
~ lower_bounded_semilattstr(boole_lattice(esk22_0)),
inference(spm,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_64,plain,
lower_bounded_semilattstr(boole_lattice(X1)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_62]),c_0_45])]) ).
cnf(c_0_65,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63,c_0_64])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU345+1 : TPTP v9.2.1. Released v3.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n029.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 02:58:29 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 4.04/3.20 % Version : CSE_E---1.7
% 4.04/3.20 % Problem : theBenchmark.p
% 4.04/3.20 % SZS status Theorem for theBenchmark.p
% 4.04/3.20 % SZS output start CNFRefutation
% See solution above
% 4.04/3.21 % Total time : 2.374s
%------------------------------------------------------------------------------