%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEU345+1 : TPTP v9.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.tkRSbE22Op true
% Computer : n027.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 : Thu Oct 2 04:54:19 PM UTC 2025
% Result : Theorem 125.66s 21.42s
% Output : Refutation 125.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 16
% Syntax : Number of formulae : 247 ( 76 unt; 0 typ; 0 def)
% Number of atoms : 1004 ( 301 equ; 0 cnn)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 4517 ( 631 ~; 707 |; 31 &;3129 @)
% ( 4 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 35 ( 33 usr; 3 con; 0-3 aty)
% Number of variables : 440 ( 0 ^; 439 !; 1 ?; 440 :)
% Comments :
%------------------------------------------------------------------------------
thf(empty_set_type,type,
empty_set: $i ).
thf(latt_str_type,type,
latt_str: $i > $o ).
thf(join_absorbing_type,type,
join_absorbing: $i > $o ).
thf(join_semilatt_str_type,type,
join_semilatt_str: $i > $o ).
thf(subset_intersection2_type,type,
subset_intersection2: $i > $i > $i > $i ).
thf(subset_union2_type,type,
subset_union2: $i > $i > $i > $i ).
thf(join_type,type,
join: $i > $i > $i > $i ).
thf(meet_commut_type,type,
meet_commut: $i > $i > $i > $i ).
thf(lower_bounded_semilattstr_type,type,
lower_bounded_semilattstr: $i > $o ).
thf(the_carrier_type,type,
the_carrier: $i > $i ).
thf(the_L_join_type,type,
the_L_join: $i > $i ).
thf(meet_commutative_type,type,
meet_commutative: $i > $o ).
thf(bottom_of_semilattstr_type,type,
bottom_of_semilattstr: $i > $i ).
thf(set_union2_type,type,
set_union2: $i > $i > $i ).
thf(sk__16_type,type,
sk__16: $i ).
thf(the_L_meet_type,type,
the_L_meet: $i > $i ).
thf(sk__1_type,type,
sk__1: $i > $i ).
thf(strict_latt_str_type,type,
strict_latt_str: $i > $o ).
thf(apply_binary_type,type,
apply_binary: $i > $i > $i > $i ).
thf(powerset_type,type,
powerset: $i > $i ).
thf(meet_semilatt_str_type,type,
meet_semilatt_str: $i > $o ).
thf(element_type,type,
element: $i > $i > $o ).
thf(set_intersection2_type,type,
set_intersection2: $i > $i > $i ).
thf(join_commutative_type,type,
join_commutative: $i > $o ).
thf(meet_associative_type,type,
meet_associative: $i > $o ).
thf(join_associative_type,type,
join_associative: $i > $o ).
thf(meet_type,type,
meet: $i > $i > $i > $i ).
thf(subset_type,type,
subset: $i > $i > $o ).
thf(lattice_type,type,
lattice: $i > $o ).
thf(empty_carrier_type,type,
empty_carrier: $i > $o ).
thf(boole_lattice_type,type,
boole_lattice: $i > $i ).
thf(sk__type,type,
sk_: $i > $i > $i ).
thf(meet_absorbing_type,type,
meet_absorbing: $i > $o ).
thf(dt_l3_lattices,axiom,
! [A: $i] :
( ( latt_str @ A )
=> ( ( meet_semilatt_str @ A )
& ( join_semilatt_str @ A ) ) ) ).
thf(zip_derived_cl45,plain,
! [X0: $i] :
( ( meet_semilatt_str @ X0 )
| ~ ( latt_str @ X0 ) ),
inference(cnf,[status(esa)],[dt_l3_lattices]) ).
thf(d1_lattice3,axiom,
! [A: $i,B: $i] :
( ( ( strict_latt_str @ B )
& ( latt_str @ B ) )
=> ( ( B
= ( boole_lattice @ A ) )
<=> ( ( ( the_carrier @ B )
= ( powerset @ A ) )
& ! [C: $i] :
( ( element @ C @ ( powerset @ A ) )
=> ! [D: $i] :
( ( element @ D @ ( powerset @ A ) )
=> ( ( ( apply_binary @ ( the_L_join @ B ) @ C @ D )
= ( subset_union2 @ A @ C @ D ) )
& ( ( apply_binary @ ( the_L_meet @ B ) @ C @ D )
= ( subset_intersection2 @ A @ C @ D ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl31,plain,
! [X0: $i,X1: $i] :
( ( X1
!= ( boole_lattice @ X0 ) )
| ( ( the_carrier @ X1 )
= ( powerset @ X0 ) )
| ~ ( latt_str @ X1 )
| ~ ( strict_latt_str @ X1 ) ),
inference(cnf,[status(esa)],[d1_lattice3]) ).
thf(zip_derived_cl2187,plain,
! [X0: $i] :
( ~ ( strict_latt_str @ ( boole_lattice @ X0 ) )
| ~ ( latt_str @ ( boole_lattice @ X0 ) )
| ( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ) ),
inference(eq_res,[status(thm)],[zip_derived_cl31]) ).
thf(dt_k1_lattice3,axiom,
! [A: $i] :
( ( latt_str @ ( boole_lattice @ A ) )
& ( strict_latt_str @ ( boole_lattice @ A ) ) ) ).
thf(zip_derived_cl36,plain,
! [X0: $i] : ( strict_latt_str @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[dt_k1_lattice3]) ).
thf(zip_derived_cl37,plain,
! [X0: $i] : ( latt_str @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[dt_k1_lattice3]) ).
thf(zip_derived_cl2188,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(dt_k5_lattices,axiom,
! [A: $i] :
( ( ~ ( empty_carrier @ A )
& ( meet_semilatt_str @ A ) )
=> ( element @ ( bottom_of_semilattstr @ A ) @ ( the_carrier @ A ) ) ) ).
thf(zip_derived_cl42,plain,
! [X0: $i] :
( ( element @ ( bottom_of_semilattstr @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(cnf,[status(esa)],[dt_k5_lattices]) ).
thf(zip_derived_cl2208,plain,
! [X0: $i] :
( ( element @ ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( empty_carrier @ ( boole_lattice @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl2188,zip_derived_cl42]) ).
thf(fc1_lattice3,axiom,
! [A: $i] :
( ( strict_latt_str @ ( boole_lattice @ A ) )
& ~ ( empty_carrier @ ( boole_lattice @ A ) ) ) ).
thf(zip_derived_cl56,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl2209,plain,
! [X0: $i] :
( ( element @ ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2208,zip_derived_cl56]) ).
thf(t2_xboole_1,axiom,
! [A: $i] : ( subset @ empty_set @ A ) ).
thf(zip_derived_cl130,plain,
! [X0: $i] : ( subset @ empty_set @ X0 ),
inference(cnf,[status(esa)],[t2_xboole_1]) ).
thf(t3_subset,axiom,
! [A: $i,B: $i] :
( ( element @ A @ ( powerset @ B ) )
<=> ( subset @ A @ B ) ) ).
thf(zip_derived_cl132,plain,
! [X0: $i,X1: $i] :
( ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( subset @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[t3_subset]) ).
thf(zip_derived_cl714,plain,
! [X0: $i] : ( element @ empty_set @ ( powerset @ X0 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl130,zip_derived_cl132]) ).
thf(zip_derived_cl714_001,plain,
! [X0: $i] : ( element @ empty_set @ ( powerset @ X0 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl130,zip_derived_cl132]) ).
thf(zip_derived_cl2188_002,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl42_003,plain,
! [X0: $i] :
( ( element @ ( bottom_of_semilattstr @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(cnf,[status(esa)],[dt_k5_lattices]) ).
thf(d13_lattices,axiom,
! [A: $i] :
( ( ~ ( empty_carrier @ A )
& ( meet_semilatt_str @ A ) )
=> ( ( lower_bounded_semilattstr @ A )
<=> ? [B: $i] :
( ! [C: $i] :
( ( element @ C @ ( the_carrier @ A ) )
=> ( ( ( meet @ A @ B @ C )
= B )
& ( ( meet @ A @ C @ B )
= B ) ) )
& ( element @ B @ ( the_carrier @ A ) ) ) ) ) ).
thf(zip_derived_cl17,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk_ @ X0 @ X1 ) @ ( the_carrier @ X1 ) )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( lower_bounded_semilattstr @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(d16_lattices,axiom,
! [A: $i] :
( ( ~ ( empty_carrier @ A )
& ( meet_semilatt_str @ A ) )
=> ( ( lower_bounded_semilattstr @ A )
=> ! [B: $i] :
( ( element @ B @ ( the_carrier @ A ) )
=> ( ( B
= ( bottom_of_semilattstr @ A ) )
<=> ! [C: $i] :
( ( element @ C @ ( the_carrier @ A ) )
=> ( ( ( meet @ A @ B @ C )
= B )
& ( ( meet @ A @ C @ B )
= B ) ) ) ) ) ) ) ).
thf(zip_derived_cl23,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( lower_bounded_semilattstr @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( X1
!= ( bottom_of_semilattstr @ X0 ) )
| ( ( meet @ X0 @ X1 @ X2 )
= X1 )
| ~ ( element @ X2 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(cnf,[status(esa)],[d16_lattices]) ).
thf(zip_derived_cl795,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( empty_carrier @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( empty_carrier @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X3 @ ( the_carrier @ X0 ) )
| ( ( meet @ X0 @ X2 @ X3 )
= X2 )
| ( X2
!= ( bottom_of_semilattstr @ X0 ) )
| ~ ( element @ X2 @ ( the_carrier @ X0 ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl17,zip_derived_cl23]) ).
thf(zip_derived_cl2565,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( element @ X2 @ ( the_carrier @ X0 ) )
| ( X2
!= ( bottom_of_semilattstr @ X0 ) )
| ( ( meet @ X0 @ X2 @ X3 )
= X2 )
| ~ ( element @ X3 @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl795]) ).
thf(zip_derived_cl2568,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( empty_carrier @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X2 @ ( the_carrier @ X0 ) )
| ( ( meet @ X0 @ ( bottom_of_semilattstr @ X0 ) @ X2 )
= ( bottom_of_semilattstr @ X0 ) )
| ( ( bottom_of_semilattstr @ X0 )
!= ( bottom_of_semilattstr @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl42,zip_derived_cl2565]) ).
thf(zip_derived_cl2577,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( meet @ X0 @ ( bottom_of_semilattstr @ X0 ) @ X2 )
= ( bottom_of_semilattstr @ X0 ) )
| ~ ( element @ X2 @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl2568]) ).
thf(zip_derived_cl3004,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( empty_carrier @ ( boole_lattice @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X2 @ ( the_carrier @ ( boole_lattice @ X0 ) ) )
| ( element @ ( sk_ @ X2 @ ( boole_lattice @ X0 ) ) @ ( the_carrier @ ( boole_lattice @ X0 ) ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) @ X1 )
= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2188,zip_derived_cl2577]) ).
thf(zip_derived_cl56_004,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl2188_005,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_006,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl3010,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X0 ) )
| ( element @ ( sk_ @ X2 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) @ X1 )
= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3004,zip_derived_cl56,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl3741,plain,
! [X0: $i,X1: $i] :
( ( ( meet @ ( boole_lattice @ X0 ) @ ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) @ empty_set )
= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) )
| ( element @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl714,zip_derived_cl3010]) ).
thf(zip_derived_cl3866,plain,
! [X0: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) @ empty_set )
= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl714,zip_derived_cl3741]) ).
thf(t1_lattice3,axiom,
! [A: $i,B: $i] :
( ( element @ B @ ( the_carrier @ ( boole_lattice @ A ) ) )
=> ! [C: $i] :
( ( element @ C @ ( the_carrier @ ( boole_lattice @ A ) ) )
=> ( ( ( join @ ( boole_lattice @ A ) @ B @ C )
= ( set_union2 @ B @ C ) )
& ( ( meet @ ( boole_lattice @ A ) @ B @ C )
= ( set_intersection2 @ B @ C ) ) ) ) ) ).
thf(zip_derived_cl127,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( the_carrier @ ( boole_lattice @ X1 ) ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ X0 )
= ( set_intersection2 @ X2 @ X0 ) )
| ~ ( element @ X2 @ ( the_carrier @ ( boole_lattice @ X1 ) ) ) ),
inference(cnf,[status(esa)],[t1_lattice3]) ).
thf(zip_derived_cl2188_007,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_008,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2316,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ X0 )
= ( set_intersection2 @ X2 @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl127,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl3925,plain,
! [X0: $i] :
( ( ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) )
= ( set_intersection2 @ ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) @ empty_set ) )
| ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( element @ empty_set @ ( powerset @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl3866,zip_derived_cl2316]) ).
thf(t2_boole,axiom,
! [A: $i] :
( ( set_intersection2 @ A @ empty_set )
= empty_set ) ).
thf(zip_derived_cl129,plain,
! [X0: $i] :
( ( set_intersection2 @ X0 @ empty_set )
= empty_set ),
inference(cnf,[status(esa)],[t2_boole]) ).
thf(zip_derived_cl714_009,plain,
! [X0: $i] : ( element @ empty_set @ ( powerset @ X0 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl130,zip_derived_cl132]) ).
thf(zip_derived_cl3931,plain,
! [X0: $i] :
( ( ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) )
= empty_set )
| ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3925,zip_derived_cl129,zip_derived_cl714]) ).
thf(zip_derived_cl2209_010,plain,
! [X0: $i] :
( ( element @ ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2208,zip_derived_cl56]) ).
thf(zip_derived_cl3956,plain,
! [X0: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) )
= empty_set ) ),
inference(clc,[status(thm)],[zip_derived_cl3931,zip_derived_cl2209]) ).
thf(zip_derived_cl129_011,plain,
! [X0: $i] :
( ( set_intersection2 @ X0 @ empty_set )
= empty_set ),
inference(cnf,[status(esa)],[t2_boole]) ).
thf(commutativity_k3_xboole_0,axiom,
! [A: $i,B: $i] :
( ( set_intersection2 @ A @ B )
= ( set_intersection2 @ B @ A ) ) ).
thf(zip_derived_cl12,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2 @ X1 @ X0 )
= ( set_intersection2 @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[commutativity_k3_xboole_0]) ).
thf(zip_derived_cl2180,plain,
! [X0: $i] :
( empty_set
= ( set_intersection2 @ empty_set @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl129,zip_derived_cl12]) ).
thf(zip_derived_cl2316_012,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ X0 )
= ( set_intersection2 @ X2 @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl127,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl2316_013,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ X0 )
= ( set_intersection2 @ X2 @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl127,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl16,plain,
! [X0: $i,X1: $i] :
( ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( lower_bounded_semilattstr @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl19,plain,
! [X0: $i,X1: $i] :
( ~ ( lower_bounded_semilattstr @ X0 )
| ( ( meet @ X0 @ ( sk__1 @ X0 ) @ X1 )
= ( sk__1 @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl783,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( empty_carrier @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( empty_carrier @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( element @ X2 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ ( sk__1 @ X1 ) @ X2 )
= ( sk__1 @ X1 ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl16,zip_derived_cl19]) ).
thf(zip_derived_cl2458,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( meet @ X1 @ ( sk__1 @ X1 ) @ X2 )
= ( sk__1 @ X1 ) )
| ~ ( element @ X2 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl783]) ).
thf(zip_derived_cl2460,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( set_intersection2 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ X0 )
!= X0 )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( empty_carrier @ ( boole_lattice @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( the_carrier @ ( boole_lattice @ X1 ) ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ X2 @ ( the_carrier @ ( boole_lattice @ X1 ) ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ ( sk__1 @ ( boole_lattice @ X1 ) ) @ X2 )
= ( sk__1 @ ( boole_lattice @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2316,zip_derived_cl2458]) ).
thf(zip_derived_cl12_014,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2 @ X1 @ X0 )
= ( set_intersection2 @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[commutativity_k3_xboole_0]) ).
thf(zip_derived_cl56_015,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl2188_016,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_017,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2462,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ X2 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ ( sk__1 @ ( boole_lattice @ X1 ) ) @ X2 )
= ( sk__1 @ ( boole_lattice @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2460,zip_derived_cl12,zip_derived_cl56,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl2463,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( meet @ ( boole_lattice @ X1 ) @ ( sk__1 @ ( boole_lattice @ X1 ) ) @ X2 )
= ( sk__1 @ ( boole_lattice @ X1 ) ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl2462]) ).
thf(zip_derived_cl2188_018,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl17_019,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk_ @ X0 @ X1 ) @ ( the_carrier @ X1 ) )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( lower_bounded_semilattstr @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl19_020,plain,
! [X0: $i,X1: $i] :
( ~ ( lower_bounded_semilattstr @ X0 )
| ( ( meet @ X0 @ ( sk__1 @ X0 ) @ X1 )
= ( sk__1 @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl791,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( empty_carrier @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( empty_carrier @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X2 @ ( the_carrier @ X0 ) )
| ( ( meet @ X0 @ ( sk__1 @ X0 ) @ X2 )
= ( sk__1 @ X0 ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl17,zip_derived_cl19]) ).
thf(zip_derived_cl2517,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( meet @ X0 @ ( sk__1 @ X0 ) @ X2 )
= ( sk__1 @ X0 ) )
| ~ ( element @ X2 @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl791]) ).
thf(zip_derived_cl2524,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( empty_carrier @ ( boole_lattice @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X2 @ ( the_carrier @ ( boole_lattice @ X0 ) ) )
| ( element @ ( sk_ @ X2 @ ( boole_lattice @ X0 ) ) @ ( the_carrier @ ( boole_lattice @ X0 ) ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X1 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2188,zip_derived_cl2517]) ).
thf(zip_derived_cl56_021,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl2188_022,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_023,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2530,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X0 ) )
| ( element @ ( sk_ @ X2 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X1 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2524,zip_derived_cl56,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl4508,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ X2 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ ( sk__1 @ ( boole_lattice @ X1 ) ) @ X2 )
= ( sk__1 @ ( boole_lattice @ X1 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl2463,zip_derived_cl2530]) ).
thf(zip_derived_cl4510,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( set_intersection2 @ X1 @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) )
!= X1 )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( element @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X2 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X2 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( set_intersection2 @ X1 @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) )
!= X1 ) ),
inference('sup-',[status(thm)],[zip_derived_cl2316,zip_derived_cl4508]) ).
thf(zip_derived_cl4513,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X2 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( set_intersection2 @ X1 @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) )
!= X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl4510]) ).
thf(zip_derived_cl2530_024,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X0 ) )
| ( element @ ( sk_ @ X2 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X1 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2524,zip_derived_cl56,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl5538,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( set_intersection2 @ X1 @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) )
!= X1 )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X2 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X2 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl4513,zip_derived_cl2530]) ).
thf(zip_derived_cl5539,plain,
! [X0: $i,X1: $i] :
( ( empty_set != empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X1 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ empty_set @ ( powerset @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2180,zip_derived_cl5538]) ).
thf(zip_derived_cl714_025,plain,
! [X0: $i] : ( element @ empty_set @ ( powerset @ X0 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl130,zip_derived_cl132]) ).
thf(zip_derived_cl5540,plain,
! [X0: $i,X1: $i] :
( ( empty_set != empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X1 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl5539,zip_derived_cl714]) ).
thf(zip_derived_cl5541,plain,
! [X0: $i,X1: $i] :
( ( ( meet @ ( boole_lattice @ X0 ) @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X1 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl5540]) ).
thf(zip_derived_cl2316_026,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ X0 )
= ( set_intersection2 @ X2 @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl127,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl5547,plain,
! [X0: $i,X1: $i] :
( ( ( sk__1 @ ( boole_lattice @ X0 ) )
= ( set_intersection2 @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl5541,zip_derived_cl2316]) ).
thf(zip_derived_cl5563,plain,
! [X0: $i,X1: $i] :
( ~ ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( ( sk__1 @ ( boole_lattice @ X0 ) )
= ( set_intersection2 @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X1 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl5547]) ).
thf(zip_derived_cl2180_027,plain,
! [X0: $i] :
( empty_set
= ( set_intersection2 @ empty_set @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl129,zip_derived_cl12]) ).
thf(zip_derived_cl2316_028,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ X0 )
= ( set_intersection2 @ X2 @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl127,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(redefinition_k4_lattices,axiom,
! [A: $i,B: $i,C: $i] :
( ( ~ ( empty_carrier @ A )
& ( meet_commutative @ A )
& ( meet_semilatt_str @ A )
& ( element @ B @ ( the_carrier @ A ) )
& ( element @ C @ ( the_carrier @ A ) ) )
=> ( ( meet_commut @ A @ B @ C )
= ( meet @ A @ B @ C ) ) ) ).
thf(zip_derived_cl122,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( meet_commutative @ X1 )
| ( empty_carrier @ X1 )
| ~ ( element @ X2 @ ( the_carrier @ X1 ) )
| ( ( meet_commut @ X1 @ X0 @ X2 )
= ( meet @ X1 @ X0 @ X2 ) ) ),
inference(cnf,[status(esa)],[redefinition_k4_lattices]) ).
thf(zip_derived_cl2344,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( meet_commut @ ( boole_lattice @ X2 ) @ X1 @ X0 )
= ( set_intersection2 @ X1 @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X2 ) )
| ~ ( element @ X0 @ ( powerset @ X2 ) )
| ~ ( element @ X0 @ ( the_carrier @ ( boole_lattice @ X2 ) ) )
| ( empty_carrier @ ( boole_lattice @ X2 ) )
| ~ ( meet_commutative @ ( boole_lattice @ X2 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X2 ) )
| ~ ( element @ X1 @ ( the_carrier @ ( boole_lattice @ X2 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl2316,zip_derived_cl122]) ).
thf(zip_derived_cl2188_029,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl56_030,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(fc2_lattice3,axiom,
! [A: $i] :
( ( 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 ) ) ) ).
thf(zip_derived_cl69,plain,
! [X0: $i] : ( meet_commutative @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc2_lattice3]) ).
thf(zip_derived_cl2188_031,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2345,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( meet_commut @ ( boole_lattice @ X2 ) @ X1 @ X0 )
= ( set_intersection2 @ X1 @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X2 ) )
| ~ ( element @ X0 @ ( powerset @ X2 ) )
| ~ ( element @ X0 @ ( powerset @ X2 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X2 ) )
| ~ ( element @ X1 @ ( powerset @ X2 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2344,zip_derived_cl2188,zip_derived_cl56,zip_derived_cl69,zip_derived_cl2188]) ).
thf(zip_derived_cl2346,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ X2 ) )
| ~ ( element @ X0 @ ( powerset @ X2 ) )
| ~ ( element @ X1 @ ( powerset @ X2 ) )
| ( ( meet_commut @ ( boole_lattice @ X2 ) @ X1 @ X0 )
= ( set_intersection2 @ X1 @ X0 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl2345]) ).
thf(commutativity_k4_lattices,axiom,
! [A: $i,B: $i,C: $i] :
( ( ~ ( empty_carrier @ A )
& ( meet_commutative @ A )
& ( meet_semilatt_str @ A )
& ( element @ B @ ( the_carrier @ A ) )
& ( element @ C @ ( the_carrier @ A ) ) )
=> ( ( meet_commut @ A @ B @ C )
= ( meet_commut @ A @ C @ B ) ) ) ).
thf(zip_derived_cl13,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( meet_commutative @ X1 )
| ( empty_carrier @ X1 )
| ~ ( element @ X2 @ ( the_carrier @ X1 ) )
| ( ( meet_commut @ X1 @ X0 @ X2 )
= ( meet_commut @ X1 @ X2 @ X0 ) ) ),
inference(cnf,[status(esa)],[commutativity_k4_lattices]) ).
thf(zip_derived_cl122_032,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( meet_commutative @ X1 )
| ( empty_carrier @ X1 )
| ~ ( element @ X2 @ ( the_carrier @ X1 ) )
| ( ( meet_commut @ X1 @ X0 @ X2 )
= ( meet @ X1 @ X0 @ X2 ) ) ),
inference(cnf,[status(esa)],[redefinition_k4_lattices]) ).
thf(zip_derived_cl122_033,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( meet_commutative @ X1 )
| ( empty_carrier @ X1 )
| ~ ( element @ X2 @ ( the_carrier @ X1 ) )
| ( ( meet_commut @ X1 @ X0 @ X2 )
= ( meet @ X1 @ X0 @ X2 ) ) ),
inference(cnf,[status(esa)],[redefinition_k4_lattices]) ).
thf(zip_derived_cl16_034,plain,
! [X0: $i,X1: $i] :
( ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( lower_bounded_semilattstr @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl18,plain,
! [X0: $i] :
( ~ ( lower_bounded_semilattstr @ X0 )
| ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl782,plain,
! [X0: $i,X1: $i] :
( ( empty_carrier @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( empty_carrier @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( element @ ( sk__1 @ X1 ) @ ( the_carrier @ X1 ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl16,zip_derived_cl18]) ).
thf(zip_derived_cl2437,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk__1 @ X1 ) @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl782]) ).
thf(zip_derived_cl2438,plain,
! [X0: $i,X1: $i] :
( ( ( meet_commut @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( empty_carrier @ X1 )
| ~ ( meet_commutative @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( element @ ( sk_ @ X0 @ X1 ) @ ( the_carrier @ X1 ) )
| ( empty_carrier @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ( element @ ( sk__1 @ X1 ) @ ( the_carrier @ X1 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl122,zip_derived_cl2437]) ).
thf(zip_derived_cl2440,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk__1 @ X1 ) @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ~ ( element @ ( sk_ @ X0 @ X1 ) @ ( the_carrier @ X1 ) )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( meet_commutative @ X1 )
| ( empty_carrier @ X1 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( ( meet_commut @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl2438]) ).
thf(zip_derived_cl17_035,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk_ @ X0 @ X1 ) @ ( the_carrier @ X1 ) )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( lower_bounded_semilattstr @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl18_036,plain,
! [X0: $i] :
( ~ ( lower_bounded_semilattstr @ X0 )
| ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl790,plain,
! [X0: $i,X1: $i] :
( ( empty_carrier @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( empty_carrier @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl17,zip_derived_cl18]) ).
thf(zip_derived_cl2481,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl790]) ).
thf(zip_derived_cl3228,plain,
! [X0: $i,X1: $i] :
( ( ( meet_commut @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( empty_carrier @ X1 )
| ~ ( meet_commutative @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ( element @ ( sk__1 @ X1 ) @ ( the_carrier @ X1 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl2440,zip_derived_cl2481]) ).
thf(zip_derived_cl3229,plain,
! [X0: $i,X1: $i] :
( ( ( meet_commut @ X0 @ X1 @ ( sk_ @ X1 @ X0 ) )
!= X1 )
| ~ ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( empty_carrier @ X0 )
| ~ ( meet_commutative @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( meet_commutative @ X0 )
| ( empty_carrier @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( ( meet_commut @ X0 @ ( sk_ @ X1 @ X0 ) @ X1 )
!= X1 ) ),
inference('sup-',[status(thm)],[zip_derived_cl122,zip_derived_cl3228]) ).
thf(zip_derived_cl3231,plain,
! [X0: $i,X1: $i] :
( ( ( meet_commut @ X0 @ ( sk_ @ X1 @ X0 ) @ X1 )
!= X1 )
| ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( meet_commutative @ X0 )
| ( empty_carrier @ X0 )
| ~ ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( ( meet_commut @ X0 @ X1 @ ( sk_ @ X1 @ X0 ) )
!= X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl3229]) ).
thf(zip_derived_cl2481_037,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl790]) ).
thf(zip_derived_cl3234,plain,
! [X0: $i,X1: $i] :
( ( ( meet_commut @ X0 @ X1 @ ( sk_ @ X1 @ X0 ) )
!= X1 )
| ( empty_carrier @ X0 )
| ~ ( meet_commutative @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( ( meet_commut @ X0 @ ( sk_ @ X1 @ X0 ) @ X1 )
!= X1 ) ),
inference(clc,[status(thm)],[zip_derived_cl3231,zip_derived_cl2481]) ).
thf(zip_derived_cl3235,plain,
! [X0: $i,X1: $i] :
( ( ( meet_commut @ X0 @ X1 @ ( sk_ @ X1 @ X0 ) )
!= X1 )
| ~ ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( empty_carrier @ X0 )
| ~ ( meet_commutative @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( meet_commutative @ X0 )
| ( empty_carrier @ X0 )
| ( ( meet_commut @ X0 @ X1 @ ( sk_ @ X1 @ X0 ) )
!= X1 ) ),
inference('sup-',[status(thm)],[zip_derived_cl13,zip_derived_cl3234]) ).
thf(zip_derived_cl3239,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( meet_commutative @ X0 )
| ( empty_carrier @ X0 )
| ~ ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( ( meet_commut @ X0 @ X1 @ ( sk_ @ X1 @ X0 ) )
!= X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl3235]) ).
thf(zip_derived_cl2481_038,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl790]) ).
thf(zip_derived_cl3245,plain,
! [X0: $i,X1: $i] :
( ( ( meet_commut @ X0 @ X1 @ ( sk_ @ X1 @ X0 ) )
!= X1 )
| ( empty_carrier @ X0 )
| ~ ( meet_commutative @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl3239,zip_derived_cl2481]) ).
thf(zip_derived_cl3246,plain,
! [X0: $i,X1: $i] :
( ( ( set_intersection2 @ X1 @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) )
!= X1 )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( element @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( the_carrier @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X1 @ ( the_carrier @ ( boole_lattice @ X0 ) ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( meet_commutative @ ( boole_lattice @ X0 ) )
| ( empty_carrier @ ( boole_lattice @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2346,zip_derived_cl3245]) ).
thf(zip_derived_cl2188_039,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_040,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl69_041,plain,
! [X0: $i] : ( meet_commutative @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc2_lattice3]) ).
thf(zip_derived_cl56_042,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl3248,plain,
! [X0: $i,X1: $i] :
( ( ( set_intersection2 @ X1 @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) )
!= X1 )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( element @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3246,zip_derived_cl2188,zip_derived_cl2188,zip_derived_cl69,zip_derived_cl56]) ).
thf(zip_derived_cl3249,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( set_intersection2 @ X1 @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) )
!= X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl3248]) ).
thf(zip_derived_cl2188_043,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2481_044,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk__1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl790]) ).
thf(zip_derived_cl2482,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( empty_carrier @ ( boole_lattice @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ ( boole_lattice @ X0 ) ) )
| ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( the_carrier @ ( boole_lattice @ X0 ) ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl2188,zip_derived_cl2481]) ).
thf(zip_derived_cl56_045,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl2188_046,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_047,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2483,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2482,zip_derived_cl56,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl3252,plain,
! [X0: $i,X1: $i] :
( ( ( set_intersection2 @ X1 @ ( sk_ @ X1 @ ( boole_lattice @ X0 ) ) )
!= X1 )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl3249,zip_derived_cl2483]) ).
thf(zip_derived_cl3253,plain,
! [X0: $i] :
( ( empty_set != empty_set )
| ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ empty_set @ ( powerset @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2180,zip_derived_cl3252]) ).
thf(zip_derived_cl714_048,plain,
! [X0: $i] : ( element @ empty_set @ ( powerset @ X0 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl130,zip_derived_cl132]) ).
thf(zip_derived_cl3254,plain,
! [X0: $i] :
( ( empty_set != empty_set )
| ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3253,zip_derived_cl714]) ).
thf(zip_derived_cl3255,plain,
! [X0: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( element @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl3254]) ).
thf(zip_derived_cl5569,plain,
! [X0: $i,X1: $i] :
( ( ( sk__1 @ ( boole_lattice @ X0 ) )
= ( set_intersection2 @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl5563,zip_derived_cl3255]) ).
thf(zip_derived_cl129_049,plain,
! [X0: $i] :
( ( set_intersection2 @ X0 @ empty_set )
= empty_set ),
inference(cnf,[status(esa)],[t2_boole]) ).
thf(zip_derived_cl5573,plain,
! [X0: $i] :
( ( ( sk__1 @ ( boole_lattice @ X0 ) )
= empty_set )
| ~ ( element @ empty_set @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl5569,zip_derived_cl129]) ).
thf(zip_derived_cl714_050,plain,
! [X0: $i] : ( element @ empty_set @ ( powerset @ X0 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl130,zip_derived_cl132]) ).
thf(zip_derived_cl5574,plain,
! [X0: $i] :
( ( ( sk__1 @ ( boole_lattice @ X0 ) )
= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl5573,zip_derived_cl714]) ).
thf(zip_derived_cl5541_051,plain,
! [X0: $i,X1: $i] :
( ( ( meet @ ( boole_lattice @ X0 ) @ ( sk__1 @ ( boole_lattice @ X0 ) ) @ X1 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl5540]) ).
thf(zip_derived_cl5615,plain,
! [X0: $i,X1: $i] :
( ( ( meet @ ( boole_lattice @ X0 ) @ empty_set @ X1 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl5574,zip_derived_cl5541]) ).
thf(zip_derived_cl5663,plain,
! [X0: $i,X1: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ empty_set @ X1 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl5615]) ).
thf(zip_derived_cl2316_052,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ X0 )
= ( set_intersection2 @ X2 @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl127,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl16_053,plain,
! [X0: $i,X1: $i] :
( ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( lower_bounded_semilattstr @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl23_054,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( lower_bounded_semilattstr @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( X1
!= ( bottom_of_semilattstr @ X0 ) )
| ( ( meet @ X0 @ X1 @ X2 )
= X1 )
| ~ ( element @ X2 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(cnf,[status(esa)],[d16_lattices]) ).
thf(zip_derived_cl787,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( empty_carrier @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( empty_carrier @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( element @ X3 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ X2 @ X3 )
= X2 )
| ( X2
!= ( bottom_of_semilattstr @ X1 ) )
| ~ ( element @ X2 @ ( the_carrier @ X1 ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl16,zip_derived_cl23]) ).
thf(zip_derived_cl2603,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( element @ X2 @ ( the_carrier @ X1 ) )
| ( X2
!= ( bottom_of_semilattstr @ X1 ) )
| ( ( meet @ X1 @ X2 @ X3 )
= X2 )
| ~ ( element @ X3 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl787]) ).
thf(zip_derived_cl2605,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ( set_intersection2 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ X0 )
!= X0 )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( empty_carrier @ ( boole_lattice @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( the_carrier @ ( boole_lattice @ X1 ) ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ X2 @ ( the_carrier @ ( boole_lattice @ X1 ) ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X3 @ X2 )
= X3 )
| ( X3
!= ( bottom_of_semilattstr @ ( boole_lattice @ X1 ) ) )
| ~ ( element @ X3 @ ( the_carrier @ ( boole_lattice @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2316,zip_derived_cl2603]) ).
thf(zip_derived_cl12_055,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2 @ X1 @ X0 )
= ( set_intersection2 @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[commutativity_k3_xboole_0]) ).
thf(zip_derived_cl56_056,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl2188_057,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_058,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_059,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2607,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ X2 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X3 @ X2 )
= X3 )
| ( X3
!= ( bottom_of_semilattstr @ ( boole_lattice @ X1 ) ) )
| ~ ( element @ X3 @ ( powerset @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2605,zip_derived_cl12,zip_derived_cl56,zip_derived_cl2188,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl2608,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( element @ X3 @ ( powerset @ X1 ) )
| ( X3
!= ( bottom_of_semilattstr @ ( boole_lattice @ X1 ) ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X3 @ X2 )
= X3 )
| ~ ( element @ X2 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl2607]) ).
thf(zip_derived_cl7587,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( sk__1 @ ( boole_lattice @ X0 ) )
!= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( set_intersection2 @ empty_set @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) )
!= empty_set )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( element @ empty_set @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X2 @ X1 )
= X2 )
| ( X2
!= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X2 @ ( powerset @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl5663,zip_derived_cl2608]) ).
thf(zip_derived_cl2180_060,plain,
! [X0: $i] :
( empty_set
= ( set_intersection2 @ empty_set @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl129,zip_derived_cl12]) ).
thf(zip_derived_cl714_061,plain,
! [X0: $i] : ( element @ empty_set @ ( powerset @ X0 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl130,zip_derived_cl132]) ).
thf(zip_derived_cl7592,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( sk__1 @ ( boole_lattice @ X0 ) )
!= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( empty_set != empty_set )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X2 @ X1 )
= X2 )
| ( X2
!= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X2 @ ( powerset @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7587,zip_derived_cl2180,zip_derived_cl714]) ).
thf(zip_derived_cl7593,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X2 @ ( powerset @ X0 ) )
| ( X2
!= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X2 @ X1 )
= X2 )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( ( sk__1 @ ( boole_lattice @ X0 ) )
!= empty_set ) ),
inference(simplify,[status(thm)],[zip_derived_cl7592]) ).
thf(zip_derived_cl5574_062,plain,
! [X0: $i] :
( ( ( sk__1 @ ( boole_lattice @ X0 ) )
= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl5573,zip_derived_cl714]) ).
thf(zip_derived_cl44952,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X2 @ X1 )
= X2 )
| ( X2
!= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X2 @ ( powerset @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl7593,zip_derived_cl5574]) ).
thf(zip_derived_cl5663_063,plain,
! [X0: $i,X1: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ empty_set @ X1 )
= ( sk__1 @ ( boole_lattice @ X0 ) ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl5615]) ).
thf(zip_derived_cl2316_064,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ X0 )
= ( set_intersection2 @ X2 @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl127,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl16_065,plain,
! [X0: $i,X1: $i] :
( ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( lower_bounded_semilattstr @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl20,plain,
! [X0: $i,X1: $i] :
( ~ ( lower_bounded_semilattstr @ X0 )
| ( ( meet @ X0 @ X1 @ ( sk__1 @ X0 ) )
= ( sk__1 @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl784,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( empty_carrier @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( empty_carrier @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ~ ( element @ X2 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ X2 @ ( sk__1 @ X1 ) )
= ( sk__1 @ X1 ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl16,zip_derived_cl20]) ).
thf(zip_derived_cl2504,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( meet @ X1 @ X2 @ ( sk__1 @ X1 ) )
= ( sk__1 @ X1 ) )
| ~ ( element @ X2 @ ( the_carrier @ X1 ) )
| ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl784]) ).
thf(zip_derived_cl2506,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( set_intersection2 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ X0 )
!= X0 )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( empty_carrier @ ( boole_lattice @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( the_carrier @ ( boole_lattice @ X1 ) ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ X2 @ ( the_carrier @ ( boole_lattice @ X1 ) ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ ( sk__1 @ ( boole_lattice @ X1 ) ) )
= ( sk__1 @ ( boole_lattice @ X1 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2316,zip_derived_cl2504]) ).
thf(zip_derived_cl12_066,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2 @ X1 @ X0 )
= ( set_intersection2 @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[commutativity_k3_xboole_0]) ).
thf(zip_derived_cl56_067,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl2188_068,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_069,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2508,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ X2 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ ( sk__1 @ ( boole_lattice @ X1 ) ) )
= ( sk__1 @ ( boole_lattice @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2506,zip_derived_cl12,zip_derived_cl56,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl2509,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ ( sk__1 @ ( boole_lattice @ X1 ) ) )
= ( sk__1 @ ( boole_lattice @ X1 ) ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl2508]) ).
thf(zip_derived_cl2188_070,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl17_071,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk_ @ X0 @ X1 ) @ ( the_carrier @ X1 ) )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( lower_bounded_semilattstr @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl20_072,plain,
! [X0: $i,X1: $i] :
( ~ ( lower_bounded_semilattstr @ X0 )
| ( ( meet @ X0 @ X1 @ ( sk__1 @ X0 ) )
= ( sk__1 @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl792,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( empty_carrier @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ( empty_carrier @ X0 )
| ~ ( meet_semilatt_str @ X0 )
| ~ ( element @ X2 @ ( the_carrier @ X0 ) )
| ( ( meet @ X0 @ X2 @ ( sk__1 @ X0 ) )
= ( sk__1 @ X0 ) ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl17,zip_derived_cl20]) ).
thf(zip_derived_cl2531,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( meet @ X0 @ X2 @ ( sk__1 @ X0 ) )
= ( sk__1 @ X0 ) )
| ~ ( element @ X2 @ ( the_carrier @ X0 ) )
| ( element @ ( sk_ @ X1 @ X0 ) @ ( the_carrier @ X0 ) )
| ~ ( element @ X1 @ ( the_carrier @ X0 ) )
| ~ ( meet_semilatt_str @ X0 )
| ( empty_carrier @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl792]) ).
thf(zip_derived_cl2538,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( empty_carrier @ ( boole_lattice @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X2 @ ( the_carrier @ ( boole_lattice @ X0 ) ) )
| ( element @ ( sk_ @ X2 @ ( boole_lattice @ X0 ) ) @ ( the_carrier @ ( boole_lattice @ X0 ) ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X1 @ ( sk__1 @ ( boole_lattice @ X0 ) ) )
= ( sk__1 @ ( boole_lattice @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2188,zip_derived_cl2531]) ).
thf(zip_derived_cl56_073,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl2188_074,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_075,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2544,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X0 ) )
| ( element @ ( sk_ @ X2 @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X1 @ ( sk__1 @ ( boole_lattice @ X0 ) ) )
= ( sk__1 @ ( boole_lattice @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2538,zip_derived_cl56,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl4684,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ X1 ) ) )
!= X0 )
| ~ ( element @ X2 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ ( sk__1 @ ( boole_lattice @ X1 ) ) )
= ( sk__1 @ ( boole_lattice @ X1 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl2509,zip_derived_cl2544]) ).
thf(zip_derived_cl5680,plain,
! [X0: $i,X1: $i] :
( ( ( sk__1 @ ( boole_lattice @ X0 ) )
!= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X1 @ ( sk__1 @ ( boole_lattice @ X0 ) ) )
= ( sk__1 @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ empty_set @ ( powerset @ X0 ) )
| ( ( set_intersection2 @ empty_set @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) )
!= empty_set ) ),
inference('sup-',[status(thm)],[zip_derived_cl5663,zip_derived_cl4684]) ).
thf(zip_derived_cl714_076,plain,
! [X0: $i] : ( element @ empty_set @ ( powerset @ X0 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl130,zip_derived_cl132]) ).
thf(zip_derived_cl2180_077,plain,
! [X0: $i] :
( empty_set
= ( set_intersection2 @ empty_set @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl129,zip_derived_cl12]) ).
thf(zip_derived_cl5709,plain,
! [X0: $i,X1: $i] :
( ( ( sk__1 @ ( boole_lattice @ X0 ) )
!= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X1 @ ( sk__1 @ ( boole_lattice @ X0 ) ) )
= ( sk__1 @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( empty_set != empty_set ) ),
inference(demod,[status(thm)],[zip_derived_cl5680,zip_derived_cl714,zip_derived_cl2180]) ).
thf(zip_derived_cl5710,plain,
! [X0: $i,X1: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X1 @ ( sk__1 @ ( boole_lattice @ X0 ) ) )
= ( sk__1 @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( ( sk__1 @ ( boole_lattice @ X0 ) )
!= empty_set ) ),
inference(simplify,[status(thm)],[zip_derived_cl5709]) ).
thf(zip_derived_cl5711,plain,
! [X0: $i,X1: $i] :
( ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X1 @ empty_set )
= empty_set )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( ( sk__1 @ ( boole_lattice @ X0 ) )
!= empty_set ) ),
inference(local_rewriting,[status(thm)],[zip_derived_cl5710]) ).
thf(zip_derived_cl5574_078,plain,
! [X0: $i] :
( ( ( sk__1 @ ( boole_lattice @ X0 ) )
= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl5573,zip_derived_cl714]) ).
thf(zip_derived_cl10398,plain,
! [X0: $i,X1: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X0 ) ) @ ( powerset @ X0 ) )
| ( ( meet @ ( boole_lattice @ X0 ) @ X1 @ empty_set )
= empty_set )
| ~ ( element @ X1 @ ( powerset @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl5711,zip_derived_cl5574]) ).
thf(zip_derived_cl44994,plain,
! [X0: $i,X1: $i] :
( ( X0 = empty_set )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( X0
!= ( bottom_of_semilattstr @ ( boole_lattice @ X1 ) ) )
| ~ ( element @ empty_set @ ( powerset @ X1 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) ) ),
inference('sup+',[status(thm)],[zip_derived_cl44952,zip_derived_cl10398]) ).
thf(zip_derived_cl714_079,plain,
! [X0: $i] : ( element @ empty_set @ ( powerset @ X0 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl130,zip_derived_cl132]) ).
thf(zip_derived_cl45176,plain,
! [X0: $i,X1: $i] :
( ( X0 = empty_set )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( X0
!= ( bottom_of_semilattstr @ ( boole_lattice @ X1 ) ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl44994,zip_derived_cl714]) ).
thf(zip_derived_cl45177,plain,
! [X0: $i,X1: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ X1 ) )
| ~ ( element @ ( sk_ @ empty_set @ ( boole_lattice @ X1 ) ) @ ( powerset @ X1 ) )
| ( X0
!= ( bottom_of_semilattstr @ ( boole_lattice @ X1 ) ) )
| ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( X0 = empty_set ) ),
inference(simplify,[status(thm)],[zip_derived_cl45176]) ).
thf(zip_derived_cl45357,plain,
! [X0: $i,X1: $i] :
( ( ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) )
= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( X1 = empty_set )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( X1
!= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl3956,zip_derived_cl45177]) ).
thf(zip_derived_cl45377,plain,
! [X0: $i,X1: $i] :
( ( X1
!= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) )
| ~ ( element @ X1 @ ( powerset @ X0 ) )
| ( X1 = empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) )
= empty_set ) ),
inference(simplify,[status(thm)],[zip_derived_cl45357]) ).
thf(zip_derived_cl48096,plain,
! [X0: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) )
= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) )
= empty_set )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) )
!= ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2209,zip_derived_cl45377]) ).
thf(zip_derived_cl48180,plain,
! [X0: $i] :
( ( ( bottom_of_semilattstr @ ( boole_lattice @ X0 ) )
= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ X0 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl48096]) ).
thf(zip_derived_cl2180_080,plain,
! [X0: $i] :
( empty_set
= ( set_intersection2 @ empty_set @ X0 ) ),
inference('sup+',[status(thm)],[zip_derived_cl129,zip_derived_cl12]) ).
thf(zip_derived_cl2316_081,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ X0 )
= ( set_intersection2 @ X2 @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl127,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl2316_082,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( element @ X0 @ ( powerset @ X1 ) )
| ( ( meet @ ( boole_lattice @ X1 ) @ X2 @ X0 )
= ( set_intersection2 @ X2 @ X0 ) )
| ~ ( element @ X2 @ ( powerset @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl127,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl16_083,plain,
! [X0: $i,X1: $i] :
( ( ( meet @ X1 @ ( sk_ @ X0 @ X1 ) @ X0 )
!= X0 )
| ( ( meet @ X1 @ X0 @ ( sk_ @ X0 @ X1 ) )
!= X0 )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( lower_bounded_semilattstr @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(t3_lattice3,conjecture,
! [A: $i] :
( ( ( bottom_of_semilattstr @ ( boole_lattice @ A ) )
= empty_set )
& ( lower_bounded_semilattstr @ ( boole_lattice @ A ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ! [A: $i] :
( ( ( bottom_of_semilattstr @ ( boole_lattice @ A ) )
= empty_set )
& ( lower_bounded_semilattstr @ ( boole_lattice @ A ) ) ),
inference('cnf.neg',[status(esa)],[t3_lattice3]) ).
thf(zip_derived_cl137,plain,
( ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set )
| ~ ( lower_bounded_semilattstr @ ( boole_lattice @ sk__16 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl789,plain,
! [X0: $i] :
( ( empty_carrier @ ( boole_lattice @ sk__16 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ~ ( element @ X0 @ ( the_carrier @ ( boole_lattice @ sk__16 ) ) )
| ( ( meet @ ( boole_lattice @ sk__16 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 )
| ( ( meet @ ( boole_lattice @ sk__16 ) @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ X0 )
!= X0 )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl16,zip_derived_cl137]) ).
thf(zip_derived_cl56_084,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl2188_085,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2464,plain,
! [X0: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ( ( meet @ ( boole_lattice @ sk__16 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 )
| ( ( meet @ ( boole_lattice @ sk__16 ) @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ X0 )
!= X0 )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set ) ),
inference(demod,[status(thm)],[zip_derived_cl789,zip_derived_cl56,zip_derived_cl2188]) ).
thf(zip_derived_cl2466,plain,
! [X0: $i] :
( ( ( set_intersection2 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ X0 )
!= X0 )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ ( powerset @ sk__16 ) )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set )
| ( ( meet @ ( boole_lattice @ sk__16 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2316,zip_derived_cl2464]) ).
thf(zip_derived_cl12_086,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2 @ X1 @ X0 )
= ( set_intersection2 @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[commutativity_k3_xboole_0]) ).
thf(zip_derived_cl2469,plain,
! [X0: $i] :
( ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ ( powerset @ sk__16 ) )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set )
| ( ( meet @ ( boole_lattice @ sk__16 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2466,zip_derived_cl12]) ).
thf(zip_derived_cl2470,plain,
! [X0: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ( ( meet @ ( boole_lattice @ sk__16 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ ( powerset @ sk__16 ) )
| ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl2469]) ).
thf(zip_derived_cl17_087,plain,
! [X0: $i,X1: $i] :
( ( element @ ( sk_ @ X0 @ X1 ) @ ( the_carrier @ X1 ) )
| ~ ( element @ X0 @ ( the_carrier @ X1 ) )
| ( lower_bounded_semilattstr @ X1 )
| ~ ( meet_semilatt_str @ X1 )
| ( empty_carrier @ X1 ) ),
inference(cnf,[status(esa)],[d13_lattices]) ).
thf(zip_derived_cl137_088,plain,
( ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set )
| ~ ( lower_bounded_semilattstr @ ( boole_lattice @ sk__16 ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl797,plain,
! [X0: $i] :
( ( empty_carrier @ ( boole_lattice @ sk__16 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ~ ( element @ X0 @ ( the_carrier @ ( boole_lattice @ sk__16 ) ) )
| ( element @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ ( the_carrier @ ( boole_lattice @ sk__16 ) ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl17,zip_derived_cl137]) ).
thf(zip_derived_cl56_089,plain,
! [X0: $i] :
~ ( empty_carrier @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[fc1_lattice3]) ).
thf(zip_derived_cl2188_090,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2188_091,plain,
! [X0: $i] :
( ( the_carrier @ ( boole_lattice @ X0 ) )
= ( powerset @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2187,zip_derived_cl36,zip_derived_cl37]) ).
thf(zip_derived_cl2448,plain,
! [X0: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ( element @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ ( powerset @ sk__16 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set ) ),
inference(demod,[status(thm)],[zip_derived_cl797,zip_derived_cl56,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl2471,plain,
! [X0: $i] :
( ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set )
| ( ( meet @ ( boole_lattice @ sk__16 ) @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl2470,zip_derived_cl2448]) ).
thf(zip_derived_cl2473,plain,
! [X0: $i] :
( ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ ( powerset @ sk__16 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 ) ),
inference('sup-',[status(thm)],[zip_derived_cl2316,zip_derived_cl2471]) ).
thf(zip_derived_cl2476,plain,
! [X0: $i] :
( ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ~ ( element @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ ( powerset @ sk__16 ) )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl2473]) ).
thf(zip_derived_cl2448_092,plain,
! [X0: $i] :
( ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ( element @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) @ ( powerset @ sk__16 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set ) ),
inference(demod,[status(thm)],[zip_derived_cl797,zip_derived_cl56,zip_derived_cl2188,zip_derived_cl2188]) ).
thf(zip_derived_cl2477,plain,
! [X0: $i] :
( ( ( set_intersection2 @ X0 @ ( sk_ @ X0 @ ( boole_lattice @ sk__16 ) ) )
!= X0 )
| ~ ( element @ X0 @ ( powerset @ sk__16 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set ) ),
inference(clc,[status(thm)],[zip_derived_cl2476,zip_derived_cl2448]) ).
thf(zip_derived_cl2478,plain,
( ( empty_set != empty_set )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ~ ( element @ empty_set @ ( powerset @ sk__16 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl2180,zip_derived_cl2477]) ).
thf(zip_derived_cl714_093,plain,
! [X0: $i] : ( element @ empty_set @ ( powerset @ X0 ) ),
inference('dp-resolution',[status(thm)],[zip_derived_cl130,zip_derived_cl132]) ).
thf(zip_derived_cl2479,plain,
( ( empty_set != empty_set )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2478,zip_derived_cl714]) ).
thf(zip_derived_cl2480,plain,
( ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ( ( bottom_of_semilattstr @ ( boole_lattice @ sk__16 ) )
!= empty_set ) ),
inference(simplify,[status(thm)],[zip_derived_cl2479]) ).
thf(zip_derived_cl48767,plain,
( ( empty_set != empty_set )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) )
| ~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) ) ),
inference('sup-',[status(thm)],[zip_derived_cl48180,zip_derived_cl2480]) ).
thf(zip_derived_cl48952,plain,
~ ( meet_semilatt_str @ ( boole_lattice @ sk__16 ) ),
inference(simplify,[status(thm)],[zip_derived_cl48767]) ).
thf(zip_derived_cl48954,plain,
~ ( latt_str @ ( boole_lattice @ sk__16 ) ),
inference('sup-',[status(thm)],[zip_derived_cl45,zip_derived_cl48952]) ).
thf(zip_derived_cl37_094,plain,
! [X0: $i] : ( latt_str @ ( boole_lattice @ X0 ) ),
inference(cnf,[status(esa)],[dt_k1_lattice3]) ).
thf(zip_derived_cl48955,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl48954,zip_derived_cl37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.32 % Problem : SEU345+1 : TPTP v9.2.0. Released v3.3.0.
% 0.10/0.33 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.tkRSbE22Op true
% 0.12/0.54 % Computer : n027.cluster.edu
% 0.12/0.54 % Model : x86_64 x86_64
% 0.12/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.54 % Memory : 8042.1875MB
% 0.12/0.54 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.54 % CPULimit : 300
% 0.12/0.54 % WCLimit : 300
% 0.12/0.54 % DateTime : Wed Oct 1 16:02:38 EDT 2025
% 0.12/0.54 % CPUTime :
% 0.12/0.54 % Running portfolio for 300 s
% 0.12/0.54 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.54 % Number of cores: 8
% 0.12/0.54 % Python version: Python 3.6.8
% 0.12/0.55 % Running in FO mode
% 0.19/0.85 % Total configuration time : 435
% 0.19/0.85 % Estimated wc time : 1092
% 0.19/0.85 % Estimated cpu time (7 cpus) : 156.0
% 0.19/0.97 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.19/1.01 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.19/1.02 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 1.47/1.10 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 1.47/1.10 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 1.47/1.12 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 1.47/1.13 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 1.84/1.36 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 125.66/21.42 % Solved by fo/fo3_bce.sh.
% 125.66/21.42 % BCE start: 138
% 125.66/21.42 % BCE eliminated: 23
% 125.66/21.42 % PE start: 115
% 125.66/21.42 logic: eq
% 125.66/21.42 % PE eliminated: -28
% 125.66/21.42 % done 4269 iterations in 20.285s
% 125.66/21.42 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 125.66/21.42 % SZS output start Refutation
% See solution above
% 125.66/21.42
% 125.66/21.42
% 125.66/21.42 % Terminating...
% 126.74/21.61 % Runner terminated.
% 126.74/21.64 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------