%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEU677^2 : TPTP v9.2.0. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.8Oqqto0nud true
% Computer : n008.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:55:42 PM UTC 2025
% Result : Theorem 3.80s 1.37s
% Output : Refutation 3.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SEU677^2 : TPTP v9.2.0. Released v3.7.0.
% 0.07/0.12 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.8Oqqto0nud true
% 0.11/0.33 % Computer : n008.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Wed Oct 1 16:14:53 EDT 2025
% 0.11/0.33 % CPUTime :
% 0.11/0.33 % Running portfolio for 300 s
% 0.11/0.33 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.33 % Number of cores: 8
% 0.11/0.33 % Python version: Python 3.6.8
% 0.11/0.33 % Running in HO mode
% 0.44/0.63 % Total configuration time : 828
% 0.44/0.63 % Estimated wc time : 1656
% 0.44/0.63 % Estimated cpu time (8 cpus) : 207.0
% 0.51/0.78 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.51/0.79 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.51/0.84 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.51/0.84 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.52/0.87 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.52/0.90 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.52/0.91 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.52/0.93 % /export/starexec/sandbox/solver/bin/lams/30_sp5.sh running for 60s
% 3.80/1.37 % Solved by lams/40_b.comb.sh.
% 3.80/1.37 % done 16 iterations in 0.280s
% 3.80/1.37 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 3.80/1.37 % SZS output start Refutation
% 3.80/1.37 thf(breln_type, type, breln: $i > $i > $i > $o).
% 3.80/1.37 thf(dsetconstr_type, type, dsetconstr: $i > ($i > $o) > $i).
% 3.80/1.37 thf('#sk2_type', type, '#sk2': $i).
% 3.80/1.37 thf('#sk5_type', type, '#sk5': $i).
% 3.80/1.37 thf(powersetI1_type, type, powersetI1: $o).
% 3.80/1.37 thf(in_type, type, in: $i > $i > $o).
% 3.80/1.37 thf(singleton_type, type, singleton: $i > $o).
% 3.80/1.37 thf(cartprod_type, type, cartprod: $i > $i > $i).
% 3.80/1.37 thf(funcSet_type, type, funcSet: $i > $i > $i).
% 3.80/1.37 thf(setadjoin_type, type, setadjoin: $i > $i > $i).
% 3.80/1.37 thf('#sk1_type', type, '#sk1': $i).
% 3.80/1.37 thf(ex1_type, type, ex1: $i > ($i > $o) > $o).
% 3.80/1.37 thf('#sk4_type', type, '#sk4': $i > $i).
% 3.80/1.37 thf(dsetconstrI_type, type, dsetconstrI: $o).
% 3.80/1.37 thf(powerset_type, type, powerset: $i > $i).
% 3.80/1.37 thf(subset_type, type, subset: $i > $i > $o).
% 3.80/1.37 thf(emptyset_type, type, emptyset: $i).
% 3.80/1.37 thf('#sk3_type', type, '#sk3': $i).
% 3.80/1.37 thf(func_type, type, func: $i > $i > $i > $o).
% 3.80/1.37 thf(kpair_type, type, kpair: $i > $i > $i).
% 3.80/1.37 thf(s_comb_type, type, '#S': !>[A:$tType, B:$tType, C:$tType]: ((A > B > C) > (A > B) > A > C)).
% 3.80/1.37 thf(c_comb_type, type, '#C': !>[A:$tType, B:$tType, C:$tType]: ((A > B > C) > B > A > C)).
% 3.80/1.37 thf(b_comb_type, type, '#B': !>[A:$tType, B:$tType, C:$tType]: ((A > B) > (C > A) > C > B)).
% 3.80/1.37 thf(k_comb_type, type, '#K': !>[A:$tType, B:$tType]: (B > A > B)).
% 3.80/1.37 thf(i_comb_type, type, '#I': !>[A:$tType]: (A > A)).
% 3.80/1.37 thf(funcinfuncset, conjecture,
% 3.80/1.37 (( dsetconstrI ) =>
% 3.80/1.37 ( ( powersetI1 ) =>
% 3.80/1.37 ( ![A:$i,B:$i,Xf:$i]:
% 3.80/1.37 ( ( func @ A @ B @ Xf ) => ( in @ Xf @ ( funcSet @ A @ B ) ) ) ) ))).
% 3.80/1.37 thf(zf_stmt_0, negated_conjecture,
% 3.80/1.37 (~( ( dsetconstrI ) =>
% 3.80/1.37 ( ( powersetI1 ) =>
% 3.80/1.37 ( ![A:$i,B:$i,Xf:$i]:
% 3.80/1.37 ( ( func @ A @ B @ Xf ) => ( in @ Xf @ ( funcSet @ A @ B ) ) ) ) ) )),
% 3.80/1.37 inference('cnf.neg', [status(esa)], [funcinfuncset])).
% 3.80/1.37 thf(zip_derived_cl0, plain,
% 3.80/1.37 (~ (((dsetconstrI) =>
% 3.80/1.37 (((powersetI1) =>
% 3.80/1.37 (((!!) @ (^[Y0 : $i]:
% 3.80/1.37 (((!!) @ (^[Y1 : $i]:
% 3.80/1.37 (((!!) @ (^[Y2 : $i]:
% 3.80/1.37 (((func @ Y0 @ Y1 @ Y2) =>
% 3.80/1.37 (in @ Y2 @
% 3.80/1.37 (funcSet @ Y0 @ Y1)))))))))))))))))),
% 3.80/1.37 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.80/1.37 thf(zip_derived_cl1, plain,
% 3.80/1.37 (~ (((dsetconstrI) =>
% 3.80/1.37 (((powersetI1) =>
% 3.80/1.37 (((!!) @ ((('#B') @ (!!) @
% 3.80/1.37 ((('#B') @ ((('#B') @ (!!))) @
% 3.80/1.37 ((('#S') @ ((('#B') @ ('#S') @
% 3.80/1.37 ((('#B') @ ((('#B') @ ('#S'))) @
% 3.80/1.37 ((('#B') @ ((('#B') @ ((('#B') @ (=>))))) @
% 3.80/1.37 func)))))) @
% 3.80/1.37 ((('#B') @ ((('#B') @ ((('#C') @ in)))) @ funcSet))))))))))))))),
% 3.80/1.37 inference('lams2combs', [status(thm)], [zip_derived_cl0])).
% 3.80/1.37 thf(zip_derived_cl3, plain,
% 3.80/1.37 (~ (((powersetI1) =>
% 3.80/1.37 (((!!) @ ((('#B') @ (!!) @
% 3.80/1.37 ((('#B') @ ((('#B') @ (!!))) @
% 3.80/1.37 ((('#S') @ ((('#B') @ ('#S') @
% 3.80/1.37 ((('#B') @ ((('#B') @ ('#S'))) @
% 3.80/1.37 ((('#B') @ ((('#B') @ ((('#B') @ (=>))))) @
% 3.80/1.37 func)))))) @
% 3.80/1.37 ((('#B') @ ((('#B') @ ((('#C') @ in)))) @ funcSet))))))))))))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1])).
% 3.80/1.37 thf(zip_derived_cl5, plain, ( (powersetI1)),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl3])).
% 3.80/1.37 thf(powersetI1, axiom, (powersetI1) =>
% 3.80/1.37 ((((!!) @ (^[Y0 : $i]:
% 3.80/1.37 (((!!) @ (^[Y1 : $i]:
% 3.80/1.37 (((subset @ Y1 @ Y0) => (in @ Y1 @
% 3.80/1.37 (powerset @ Y0))))))))))
% 3.80/1.37 = ($true))).
% 3.80/1.37 thf('0', plain,
% 3.80/1.37 (( powersetI1 ) <=>
% 3.80/1.37 ( ![X5:$i,X7:$i]:
% 3.80/1.37 ( ( subset @ X7 @ X5 ) => ( in @ X7 @ ( powerset @ X5 ) ) ) )),
% 3.80/1.37 inference('rw.lit', [status(esa)], [powersetI1])).
% 3.80/1.37 thf(zip_derived_cl9, plain,
% 3.80/1.37 ( (((!!) @ (^[Y0 : $i]:
% 3.80/1.37 (((!!) @ (^[Y1 : $i]:
% 3.80/1.37 (((subset @ Y1 @ Y0) => (in @ Y1 @
% 3.80/1.37 (powerset @ Y0))))))))))),
% 3.80/1.37 inference('rw_clause', [status(thm)], [zip_derived_cl5, '0'])).
% 3.80/1.37 thf(zip_derived_cl12, plain,
% 3.80/1.37 ( (((!!) @ ((('#B') @ (!!) @
% 3.80/1.37 ((('#S') @ ((('#B') @ ('#S') @
% 3.80/1.37 ((('#B') @ ((('#B') @ (=>))) @
% 3.80/1.37 ((('#C') @ subset)))))) @
% 3.80/1.37 ((('#B') @ ((('#C') @ in)) @ powerset))))))))),
% 3.80/1.37 inference('comb-normalize', [status(thm)], [zip_derived_cl9])).
% 3.80/1.37 thf(zip_derived_cl13, plain,
% 3.80/1.37 (![X2 : $i]:
% 3.80/1.37 (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ subset @ X2)))) @
% 3.80/1.37 ((('#C') @ in @ (powerset @ X2)))))))),
% 3.80/1.37 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl12])).
% 3.80/1.37 thf(zip_derived_cl16, plain,
% 3.80/1.37 (![X2 : $i, X4 : $i]:
% 3.80/1.37 (((subset @ X4 @ X2) => (in @ X4 @ (powerset @ X2))))),
% 3.80/1.37 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl13])).
% 3.80/1.37 thf(zip_derived_cl20, plain,
% 3.80/1.37 (![X2 : $i, X4 : $i]:
% 3.80/1.37 (~ (subset @ X4 @ X2) | (in @ X4 @ (powerset @ X2)))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl16])).
% 3.80/1.37 thf(zip_derived_cl6, plain,
% 3.80/1.37 (~ (((!!) @ ((('#B') @ (!!) @
% 3.80/1.37 ((('#B') @ ((('#B') @ (!!))) @
% 3.80/1.37 ((('#S') @ ((('#B') @ ('#S') @
% 3.80/1.37 ((('#B') @ ((('#B') @ ('#S'))) @
% 3.80/1.37 ((('#B') @ ((('#B') @ ((('#B') @ (=>))))) @
% 3.80/1.37 func)))))) @
% 3.80/1.37 ((('#B') @ ((('#B') @ ((('#C') @ in)))) @ funcSet))))))))))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl3])).
% 3.80/1.37 thf(zip_derived_cl10, plain,
% 3.80/1.37 (~ (((!!) @ ((('#B') @ (!!) @
% 3.80/1.37 ((('#S') @ ((('#B') @ ('#S') @
% 3.80/1.37 ((('#B') @ ((('#B') @ (=>))) @ (func @ '#sk1'))))) @
% 3.80/1.37 ((('#B') @ ((('#C') @ in)) @ (funcSet @ '#sk1')))))))))),
% 3.80/1.37 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl6])).
% 3.80/1.37 thf(zip_derived_cl14, plain,
% 3.80/1.37 (~ (((!!) @ ((('#S') @ ((('#B') @ (=>) @ (func @ '#sk1' @ '#sk2'))) @
% 3.80/1.37 ((('#C') @ in @ (funcSet @ '#sk1' @ '#sk2')))))))),
% 3.80/1.37 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl10])).
% 3.80/1.37 thf(funcSet, axiom,(( funcSet @ (X0)@ (X1)) =
% 3.80/1.37 ((dsetconstr @ (powerset @ (cartprod @ X0 @ X1)) @
% 3.80/1.37 (^[Y0 : $i]: (func @ X0 @ X1 @ Y0)))))).
% 3.80/1.37 thf('1', plain,
% 3.80/1.37 (![X1:$i,X0:$i]:
% 3.80/1.37 ( ( funcSet @ X0 @ X1 ) =
% 3.80/1.37 ( dsetconstr @
% 3.80/1.37 ( powerset @ ( cartprod @ X0 @ X1 ) ) @
% 3.80/1.37 ( ^[V_1:$i]: ( func @ X0 @ X1 @ V_1 ) ) ) )),
% 3.80/1.37 define([status(thm)])).
% 3.80/1.37 thf(zip_derived_cl17, plain,
% 3.80/1.37 (~ (((!!) @ ((('#S') @ ((('#B') @ (=>) @ (func @ '#sk1' @ '#sk2'))) @
% 3.80/1.37 ((('#C') @ in @
% 3.80/1.37 (dsetconstr @
% 3.80/1.37 (powerset @ (cartprod @ '#sk1' @ '#sk2')) @
% 3.80/1.37 (func @ '#sk1' @ '#sk2'))))))))),
% 3.80/1.37 inference('rw', [status(thm)], [zip_derived_cl14, '1'])).
% 3.80/1.37 thf(zip_derived_cl18, plain,
% 3.80/1.37 (~ (((func @ '#sk1' @ '#sk2' @ '#sk3') => (in @ '#sk3' @
% 3.80/1.37 (dsetconstr @ (powerset @ (cartprod @ '#sk1' @ '#sk2')) @
% 3.80/1.37 (func @ '#sk1' @ '#sk2')))))),
% 3.80/1.37 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl17])).
% 3.80/1.37 thf(zip_derived_cl21, plain, ( (func @ '#sk1' @ '#sk2' @ '#sk3')),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl18])).
% 3.80/1.37 thf(func, axiom, (func @ X0 @ X1 @ X2) =>
% 3.80/1.37 ((((((!!) @ (^[Y0 : $i]:
% 3.80/1.37 (((in @ Y0 @ X0) => (ex1 @ X1 @
% 3.80/1.37 (^[Y1 : $i]: (in @ (kpair @ Y0 @ Y1) @ X2)))))))) &
% 3.80/1.37 (breln @ X0 @ X1 @ X2)))
% 3.80/1.37 = ($true))).
% 3.80/1.37 thf('2', plain,
% 3.80/1.37 (![X0:$i,X1:$i,X2:$i]:
% 3.80/1.37 ( ( func @ X0 @ X1 @ X2 ) <=>
% 3.80/1.37 ( ( breln @ X0 @ X1 @ X2 ) &
% 3.80/1.37 ( ![X7:$i]:
% 3.80/1.37 ( ( in @ X7 @ X0 ) =>
% 3.80/1.37 ( ex1 @ X1 @ ( ^[V_1:$i]: ( in @ ( kpair @ X7 @ V_1 ) @ X2 ) ) ) ) ) ) )),
% 3.80/1.37 inference('rw.lit', [status(esa)], [func])).
% 3.80/1.37 thf(zip_derived_cl24, plain,
% 3.80/1.37 ( (((((!!) @ (^[Y0 : $i]:
% 3.80/1.37 (((in @ Y0 @ '#sk1') => (ex1 @ '#sk2' @
% 3.80/1.37 (^[Y1 : $i]: (in @ (kpair @ Y0 @ Y1) @ '#sk3')))))))) &
% 3.80/1.37 (breln @ '#sk1' @ '#sk2' @ '#sk3')))),
% 3.80/1.37 inference('rw_clause', [status(thm)], [zip_derived_cl21, '2'])).
% 3.80/1.37 thf(zip_derived_cl25, plain,
% 3.80/1.37 ( (((((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3')))))))) &
% 3.80/1.37 (breln @ '#sk1' @ '#sk2' @ '#sk3')))),
% 3.80/1.37 inference('comb-normalize', [status(thm)], [zip_derived_cl24])).
% 3.80/1.37 thf(breln, axiom,(( breln @ (X1)@ (X2)@ (X0)) =
% 3.80/1.37 ((subset @ X0 @ (cartprod @ X1 @ X2))))).
% 3.80/1.37 thf('3', plain,
% 3.80/1.37 (![X2:$i,X1:$i,X0:$i]:
% 3.80/1.37 ( ( breln @ X1 @ X2 @ X0 ) = ( subset @ X0 @ ( cartprod @ X1 @ X2 ) ) )),
% 3.80/1.37 define([status(thm)])).
% 3.80/1.37 thf(zip_derived_cl26, plain,
% 3.80/1.37 ( (((((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3')))))))) &
% 3.80/1.37 (subset @ '#sk3' @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('rw', [status(thm)], [zip_derived_cl25, '3'])).
% 3.80/1.37 thf(zip_derived_cl27, plain,
% 3.80/1.37 ( (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3'))))))))),
% 3.80/1.37 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl26])).
% 3.80/1.37 thf(zip_derived_cl29, plain,
% 3.80/1.37 (![X2 : $i]:
% 3.80/1.37 (((in @ X2 @ '#sk1') => (ex1 @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X2))) @ '#sk3')))))),
% 3.80/1.37 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl27])).
% 3.80/1.37 thf(ex1, axiom,(( ex1 @ (X0)@ (X1)) =
% 3.80/1.37 ((singleton @ (dsetconstr @ X0 @ (^[Y0 : $i]: (X1 @ Y0))))))).
% 3.80/1.37 thf('4', plain,
% 3.80/1.37 (![X1:( $i > $o ),X0:$i]:
% 3.80/1.37 ( ( ex1 @ X0 @ X1 ) =
% 3.80/1.37 ( singleton @ ( dsetconstr @ X0 @ ( ^[V_1:$i]: ( X1 @ V_1 ) ) ) ) )),
% 3.80/1.37 define([status(thm)])).
% 3.80/1.37 thf(zip_derived_cl30, plain,
% 3.80/1.37 (![X2 : $i]:
% 3.80/1.37 (((in @ X2 @ '#sk1') => (singleton @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X2))) @ '#sk3'))))))),
% 3.80/1.37 inference('rw', [status(thm)], [zip_derived_cl29, '4'])).
% 3.80/1.37 thf(zip_derived_cl31, plain,
% 3.80/1.37 (![X2 : $i]:
% 3.80/1.37 (~ (in @ X2 @ '#sk1')
% 3.80/1.37 | (singleton @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X2))) @ '#sk3')))))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl30])).
% 3.80/1.37 thf(singleton, axiom, (singleton @ X0) =>
% 3.80/1.37 ((((??) @ (^[Y0 : $i]:
% 3.80/1.37 (((in @ Y0 @ X0) & (((X0) = (setadjoin @ Y0 @ emptyset))))))))
% 3.80/1.37 = ($true))).
% 3.80/1.37 thf('5', plain,
% 3.80/1.37 (![X0:$i]:
% 3.80/1.37 ( ( singleton @ X0 ) <=>
% 3.80/1.37 ( ?[X5:$i]:
% 3.80/1.37 ( ( in @ X5 @ X0 ) & ( ( X0 ) = ( setadjoin @ X5 @ emptyset ) ) ) ) )),
% 3.80/1.37 inference('rw.lit', [status(esa)], [singleton])).
% 3.80/1.37 thf(zip_derived_cl32, plain,
% 3.80/1.37 (![X0 : $i]:
% 3.80/1.37 ( (((??) @ (^[Y0 : $i]:
% 3.80/1.37 (((in @ Y0 @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X0))) @ '#sk3')))) &
% 3.80/1.37 (((dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X0))) @ '#sk3'))) =
% 3.80/1.37 (setadjoin @ Y0 @ emptyset))))))))
% 3.80/1.37 | ~ (in @ X0 @ '#sk1'))),
% 3.80/1.37 inference('rw_clause', [status(thm)], [zip_derived_cl31, '5'])).
% 3.80/1.37 thf(zip_derived_cl33, plain,
% 3.80/1.37 (![X0 : $i]:
% 3.80/1.37 ( (((??) @ ((('#S') @ ((('#B') @ (&) @
% 3.80/1.37 ((('#C') @ in @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X0))) @
% 3.80/1.37 '#sk3'))))))) @
% 3.80/1.37 ((('#B') @ ((($i) = (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X0))) @
% 3.80/1.37 '#sk3'))))) @
% 3.80/1.37 ((('#C') @ setadjoin @ emptyset))))))))
% 3.80/1.37 | ~ (in @ X0 @ '#sk1'))),
% 3.80/1.37 inference('comb-normalize', [status(thm)], [zip_derived_cl32])).
% 3.80/1.37 thf(zip_derived_cl34, plain,
% 3.80/1.37 (![X0 : $i]:
% 3.80/1.37 ( (((in @ ('#sk4' @ X0) @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X0))) @ '#sk3')))) &
% 3.80/1.37 (((dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X0))) @ '#sk3'))) =
% 3.80/1.37 (setadjoin @ ('#sk4' @ X0) @ emptyset)))))
% 3.80/1.37 | ~ (in @ X0 @ '#sk1'))),
% 3.80/1.37 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl33])).
% 3.80/1.37 thf(zip_derived_cl36, plain,
% 3.80/1.37 (![X0 : $i]:
% 3.80/1.37 ( (((dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X0))) @ '#sk3'))) =
% 3.80/1.37 (setadjoin @ ('#sk4' @ X0) @ emptyset)))
% 3.80/1.37 | ~ (in @ X0 @ '#sk1'))),
% 3.80/1.37 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl34])).
% 3.80/1.37 thf(zip_derived_cl37, plain,
% 3.80/1.37 (![X0 : $i]:
% 3.80/1.37 (((dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X0))) @ '#sk3')))
% 3.80/1.37 = (setadjoin @ ('#sk4' @ X0) @ emptyset))
% 3.80/1.37 | ~ (in @ X0 @ '#sk1'))),
% 3.80/1.37 inference('simplify nested equalities', [status(thm)], [zip_derived_cl36])).
% 3.80/1.37 thf(zip_derived_cl35, plain,
% 3.80/1.37 (![X0 : $i]:
% 3.80/1.37 ( (in @ ('#sk4' @ X0) @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ X0))) @ '#sk3'))))
% 3.80/1.37 | ~ (in @ X0 @ '#sk1'))),
% 3.80/1.37 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl34])).
% 3.80/1.37 thf(zip_derived_cl22, plain,
% 3.80/1.37 (~ (in @ '#sk3' @
% 3.80/1.37 (dsetconstr @ (powerset @ (cartprod @ '#sk1' @ '#sk2')) @
% 3.80/1.37 (func @ '#sk1' @ '#sk2')))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl18])).
% 3.80/1.37 thf(zip_derived_cl2, plain, ( (dsetconstrI)),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl1])).
% 3.80/1.37 thf(dsetconstrI, axiom, (dsetconstrI) =>
% 3.80/1.37 ((((!!) @ (^[Y0 : $i]:
% 3.80/1.37 (((!!) @ (^[Y1 : $i > $o]:
% 3.80/1.37 (((!!) @ (^[Y2 : $i]:
% 3.80/1.37 (((in @ Y2 @ Y0) =>
% 3.80/1.37 (((Y1 @ Y2) => (in @ Y2 @
% 3.80/1.37 (dsetconstr @ Y0 @
% 3.80/1.37 (^[Y3 : $i]: (Y1 @ Y3)))))))))))))))))
% 3.80/1.37 = ($true))).
% 3.80/1.37 thf('6', plain,
% 3.80/1.37 (( dsetconstrI ) <=>
% 3.80/1.37 ( ![X5:$i,X7:( $i > $o ),X9:$i]:
% 3.80/1.37 ( ( in @ X9 @ X5 ) =>
% 3.80/1.37 ( ( X7 @ X9 ) =>
% 3.80/1.37 ( in @ X9 @ ( dsetconstr @ X5 @ ( ^[V_1:$i]: ( X7 @ V_1 ) ) ) ) ) ) )),
% 3.80/1.37 inference('rw.lit', [status(esa)], [dsetconstrI])).
% 3.80/1.37 thf(zip_derived_cl4, plain,
% 3.80/1.37 ( (((!!) @ (^[Y0 : $i]:
% 3.80/1.37 (((!!) @ (^[Y1 : $i > $o]:
% 3.80/1.37 (((!!) @ (^[Y2 : $i]:
% 3.80/1.37 (((in @ Y2 @ Y0) =>
% 3.80/1.37 (((Y1 @ Y2) => (in @ Y2 @
% 3.80/1.37 (dsetconstr @ Y0 @
% 3.80/1.37 (^[Y3 : $i]: (Y1 @ Y3)))))))))))))))))),
% 3.80/1.37 inference('rw_clause', [status(thm)], [zip_derived_cl2, '6'])).
% 3.80/1.37 thf(zip_derived_cl7, plain,
% 3.80/1.37 ( (((!!) @ ((('#B') @ (!!) @
% 3.80/1.37 ((('#B') @ ((('#B') @ (!!))) @
% 3.80/1.37 ((('#S') @ ((('#B') @ ('#B') @
% 3.80/1.37 ((('#B') @ ('#S') @
% 3.80/1.37 ((('#B') @ ((('#B') @ (=>))) @
% 3.80/1.37 ((('#C') @ in)))))))) @
% 3.80/1.37 ((('#B') @ ((('#S') @ ((('#B') @ ('#S') @
% 3.80/1.37 ((('#B') @ (=>))))))) @
% 3.80/1.37 ((('#B') @ ((('#B') @ ((('#C') @ in)))) @ dsetconstr))))))))))))),
% 3.80/1.37 inference('comb-normalize', [status(thm)], [zip_derived_cl4])).
% 3.80/1.37 thf(zip_derived_cl8, plain,
% 3.80/1.37 (![X2 : $i]:
% 3.80/1.37 (((!!) @ ((('#B') @ (!!) @
% 3.80/1.37 ((('#B') @ ((('#S') @ ((('#B') @ (=>) @
% 3.80/1.37 ((('#C') @ in @ X2)))))) @
% 3.80/1.37 ((('#S') @ ((('#B') @ ('#S') @ ((('#B') @ (=>))))) @
% 3.80/1.37 ((('#B') @ ((('#C') @ in)) @ (dsetconstr @ X2)))))))))))),
% 3.80/1.37 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl7])).
% 3.80/1.37 thf(zip_derived_cl11, plain,
% 3.80/1.37 (![X2 : $i, X4 : $i > $o]:
% 3.80/1.37 (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ X2)))) @
% 3.80/1.37 ((('#S') @ ((('#B') @ (=>) @ X4)) @
% 3.80/1.37 ((('#C') @ in @ (dsetconstr @ X2 @ X4)))))))))),
% 3.80/1.37 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl8])).
% 3.80/1.37 thf(zip_derived_cl15, plain,
% 3.80/1.37 (![X2 : $i, X4 : $i > $o, X6 : $i]:
% 3.80/1.37 (((in @ X6 @ X2) =>
% 3.80/1.37 (((X4 @ X6) => (in @ X6 @ (dsetconstr @ X2 @ X4))))))),
% 3.80/1.37 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl11])).
% 3.80/1.37 thf(zip_derived_cl19, plain,
% 3.80/1.37 (![X2 : $i, X4 : $i > $o, X6 : $i]:
% 3.80/1.37 (~ (in @ X6 @ X2)
% 3.80/1.37 | (((X4 @ X6) => (in @ X6 @ (dsetconstr @ X2 @ X4)))))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl15])).
% 3.80/1.37 thf(zip_derived_cl23, plain,
% 3.80/1.37 (![X2 : $i, X4 : $i > $o, X6 : $i]:
% 3.80/1.37 (~ (X4 @ X6) | (in @ X6 @ (dsetconstr @ X2 @ X4)) | ~ (in @ X6 @ X2))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl19])).
% 3.80/1.37 thf(zip_derived_cl39, plain,
% 3.80/1.37 ((~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2')))
% 3.80/1.37 | ~ (func @ '#sk1' @ '#sk2' @ '#sk3'))),
% 3.80/1.37 inference('sup+', [status(thm)], [zip_derived_cl22, zip_derived_cl23])).
% 3.80/1.37 thf(func, axiom, ~ (func @ X0 @ X1 @ X2) =>
% 3.80/1.37 ((((breln @ X0 @ X1 @ X2) &
% 3.80/1.37 (((!!) @ (^[Y0 : $i]:
% 3.80/1.37 (((in @ Y0 @ X0) => (ex1 @ X1 @
% 3.80/1.37 (^[Y1 : $i]: (in @ (kpair @ Y0 @ Y1) @ X2))))))))))
% 3.80/1.37 != ($true))).
% 3.80/1.37 thf('7', plain,
% 3.80/1.37 (![X0:$i,X1:$i,X2:$i]:
% 3.80/1.37 ( ( ~( func @ X0 @ X1 @ X2 ) ) <=>
% 3.80/1.37 ( ~( ( breln @ X0 @ X1 @ X2 ) &
% 3.80/1.37 ( ![X7:$i]:
% 3.80/1.37 ( ( in @ X7 @ X0 ) =>
% 3.80/1.37 ( ex1 @
% 3.80/1.37 X1 @ ( ^[V_1:$i]: ( in @ ( kpair @ X7 @ V_1 ) @ X2 ) ) ) ) ) ) ) )),
% 3.80/1.37 inference('rw.lit', [status(esa)], [func])).
% 3.80/1.37 thf(zip_derived_cl68, plain,
% 3.80/1.37 ((~ (((breln @ '#sk1' @ '#sk2' @ '#sk3') &
% 3.80/1.37 (((!!) @ (^[Y0 : $i]:
% 3.80/1.37 (((in @ Y0 @ '#sk1') => (ex1 @ '#sk2' @
% 3.80/1.37 (^[Y1 : $i]: (in @ (kpair @ Y0 @ Y1) @ '#sk3'))))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('rw_clause', [status(thm)], [zip_derived_cl39, '7'])).
% 3.80/1.37 thf(zip_derived_cl69, plain,
% 3.80/1.37 ((~ (((breln @ '#sk1' @ '#sk2' @ '#sk3') &
% 3.80/1.37 (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3'))))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('comb-normalize', [status(thm)], [zip_derived_cl68])).
% 3.80/1.37 thf(zip_derived_cl70, plain,
% 3.80/1.37 ((~ (((subset @ '#sk3' @ (cartprod @ '#sk1' @ '#sk2')) &
% 3.80/1.37 (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3'))))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('rw', [status(thm)], [zip_derived_cl69, '3'])).
% 3.80/1.37 thf(zip_derived_cl28, plain,
% 3.80/1.37 ( (subset @ '#sk3' @ (cartprod @ '#sk1' @ '#sk2'))),
% 3.80/1.37 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl26])).
% 3.80/1.37 thf(zip_derived_cl71, plain,
% 3.80/1.37 ((~ ((($true) &
% 3.80/1.37 (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3'))))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('demod', [status(thm)], [zip_derived_cl70, zip_derived_cl28])).
% 3.80/1.37 thf(zip_derived_cl72, plain,
% 3.80/1.37 ((~ (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3'))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl71])).
% 3.80/1.37 thf(zip_derived_cl73, plain,
% 3.80/1.37 ((~ (((in @ '#sk5' @ '#sk1') => (ex1 @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3')))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl72])).
% 3.80/1.37 thf(zip_derived_cl74, plain,
% 3.80/1.37 ((~ (((in @ '#sk5' @ '#sk1') => (singleton @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3'))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('rw', [status(thm)], [zip_derived_cl73, '4'])).
% 3.80/1.37 thf(zip_derived_cl20, plain,
% 3.80/1.37 (![X2 : $i, X4 : $i]:
% 3.80/1.37 (~ (subset @ X4 @ X2) | (in @ X4 @ (powerset @ X2)))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl16])).
% 3.80/1.37 thf(zip_derived_cl23, plain,
% 3.80/1.37 (![X2 : $i, X4 : $i > $o, X6 : $i]:
% 3.80/1.37 (~ (X4 @ X6) | (in @ X6 @ (dsetconstr @ X2 @ X4)) | ~ (in @ X6 @ X2))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl19])).
% 3.80/1.37 thf(zip_derived_cl22, plain,
% 3.80/1.37 (~ (in @ '#sk3' @
% 3.80/1.37 (dsetconstr @ (powerset @ (cartprod @ '#sk1' @ '#sk2')) @
% 3.80/1.37 (func @ '#sk1' @ '#sk2')))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl18])).
% 3.80/1.37 thf(zip_derived_cl38, plain,
% 3.80/1.37 ((~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2')))
% 3.80/1.37 | ~ (func @ '#sk1' @ '#sk2' @ '#sk3'))),
% 3.80/1.37 inference('sup-', [status(thm)], [zip_derived_cl23, zip_derived_cl22])).
% 3.80/1.37 thf(zip_derived_cl50, plain,
% 3.80/1.37 ((~ (((breln @ '#sk1' @ '#sk2' @ '#sk3') &
% 3.80/1.37 (((!!) @ (^[Y0 : $i]:
% 3.80/1.37 (((in @ Y0 @ '#sk1') => (ex1 @ '#sk2' @
% 3.80/1.37 (^[Y1 : $i]: (in @ (kpair @ Y0 @ Y1) @ '#sk3'))))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('rw_clause', [status(thm)], [zip_derived_cl38, '7'])).
% 3.80/1.37 thf(zip_derived_cl51, plain,
% 3.80/1.37 ((~ (((breln @ '#sk1' @ '#sk2' @ '#sk3') &
% 3.80/1.37 (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3'))))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('comb-normalize', [status(thm)], [zip_derived_cl50])).
% 3.80/1.37 thf(zip_derived_cl52, plain,
% 3.80/1.37 ((~ (((subset @ '#sk3' @ (cartprod @ '#sk1' @ '#sk2')) &
% 3.80/1.37 (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3'))))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('rw', [status(thm)], [zip_derived_cl51, '3'])).
% 3.80/1.37 thf(zip_derived_cl28, plain,
% 3.80/1.37 ( (subset @ '#sk3' @ (cartprod @ '#sk1' @ '#sk2'))),
% 3.80/1.37 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl26])).
% 3.80/1.37 thf(zip_derived_cl53, plain,
% 3.80/1.37 ((~ ((($true) &
% 3.80/1.37 (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3'))))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('demod', [status(thm)], [zip_derived_cl52, zip_derived_cl28])).
% 3.80/1.37 thf(zip_derived_cl54, plain,
% 3.80/1.37 ((~ (((!!) @ ((('#S') @ ((('#B') @ (=>) @ ((('#C') @ in @ '#sk1')))) @
% 3.80/1.37 ((('#B') @ (ex1 @ '#sk2') @
% 3.80/1.37 ((('#C') @ ((('#B') @ ('#C') @
% 3.80/1.37 ((('#B') @ ((('#B') @ in)) @ kpair)))) @
% 3.80/1.37 '#sk3'))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl53])).
% 3.80/1.37 thf(zip_derived_cl55, plain,
% 3.80/1.37 ((~ (((in @ '#sk5' @ '#sk1') => (ex1 @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3')))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl54])).
% 3.80/1.37 thf(zip_derived_cl56, plain,
% 3.80/1.37 ((~ (((in @ '#sk5' @ '#sk1') => (singleton @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3'))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('rw', [status(thm)], [zip_derived_cl55, '4'])).
% 3.80/1.37 thf(zip_derived_cl57, plain,
% 3.80/1.37 (( (in @ '#sk5' @ '#sk1')
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('lazy_cnf_imply', [status(thm)], [zip_derived_cl56])).
% 3.80/1.37 thf(zip_derived_cl65, plain,
% 3.80/1.37 ((~ (subset @ '#sk3' @ (cartprod @ '#sk1' @ '#sk2'))
% 3.80/1.37 | (in @ '#sk5' @ '#sk1'))),
% 3.80/1.37 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl57])).
% 3.80/1.37 thf(zip_derived_cl28, plain,
% 3.80/1.37 ( (subset @ '#sk3' @ (cartprod @ '#sk1' @ '#sk2'))),
% 3.80/1.37 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl26])).
% 3.80/1.37 thf(zip_derived_cl66, plain, ( (in @ '#sk5' @ '#sk1')),
% 3.80/1.37 inference('demod', [status(thm)], [zip_derived_cl65, zip_derived_cl28])).
% 3.80/1.37 thf(zip_derived_cl75, plain,
% 3.80/1.37 ((~ ((($true) => (singleton @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3'))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('demod', [status(thm)], [zip_derived_cl74, zip_derived_cl66])).
% 3.80/1.37 thf(zip_derived_cl76, plain,
% 3.80/1.37 ((~ (singleton @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3'))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('simplify boolean subterms', [status(thm)], [zip_derived_cl75])).
% 3.80/1.37 thf(singleton, axiom, ~ (singleton @ X0) =>
% 3.80/1.37 ((((??) @ (^[Y0 : $i]:
% 3.80/1.37 (((in @ Y0 @ X0) & (((X0) = (setadjoin @ Y0 @ emptyset))))))))
% 3.80/1.37 != ($true))).
% 3.80/1.37 thf('8', plain,
% 3.80/1.37 (![X0:$i]:
% 3.80/1.37 ( ( ~( singleton @ X0 ) ) <=>
% 3.80/1.37 ( ~( ?[X5:$i]:
% 3.80/1.37 ( ( in @ X5 @ X0 ) & ( ( X0 ) = ( setadjoin @ X5 @ emptyset ) ) ) ) ) )),
% 3.80/1.37 inference('rw.lit', [status(esa)], [singleton])).
% 3.80/1.37 thf(zip_derived_cl77, plain,
% 3.80/1.37 ((~ (((??) @ (^[Y0 : $i]:
% 3.80/1.37 (((in @ Y0 @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3')))) &
% 3.80/1.37 (((dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @
% 3.80/1.37 '#sk3'))) =
% 3.80/1.37 (setadjoin @ Y0 @ emptyset))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('rw_clause', [status(thm)], [zip_derived_cl76, '8'])).
% 3.80/1.37 thf(zip_derived_cl78, plain,
% 3.80/1.37 ((~ (((??) @ ((('#S') @ ((('#B') @ (&) @
% 3.80/1.37 ((('#C') @ in @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @
% 3.80/1.37 '#sk3'))))))) @
% 3.80/1.37 ((('#B') @ ((($i) = (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @
% 3.80/1.37 '#sk3'))))) @
% 3.80/1.37 ((('#C') @ setadjoin @ emptyset))))))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('comb-normalize', [status(thm)], [zip_derived_cl77])).
% 3.80/1.37 thf(zip_derived_cl79, plain,
% 3.80/1.37 (![X2 : $i]:
% 3.80/1.37 (~ (((in @ X2 @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3')))) &
% 3.80/1.37 (((dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3'))) =
% 3.80/1.37 (setadjoin @ X2 @ emptyset)))))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl78])).
% 3.80/1.37 thf(zip_derived_cl80, plain,
% 3.80/1.37 (![X2 : $i]:
% 3.80/1.37 (~ (in @ X2 @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3'))))
% 3.80/1.37 | ~ (((dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3'))) =
% 3.80/1.37 (setadjoin @ X2 @ emptyset)))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl79])).
% 3.80/1.37 thf(zip_derived_cl81, plain,
% 3.80/1.37 (![X2 : $i]:
% 3.80/1.37 (~ (in @ X2 @
% 3.80/1.37 (dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3'))))
% 3.80/1.37 | ((dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3')))
% 3.80/1.37 != (setadjoin @ X2 @ emptyset))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('simplify nested equalities', [status(thm)], [zip_derived_cl80])).
% 3.80/1.37 thf(zip_derived_cl85, plain,
% 3.80/1.37 ((~ (in @ '#sk5' @ '#sk1')
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2')))
% 3.80/1.37 | ((dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3')))
% 3.80/1.37 != (setadjoin @ ('#sk4' @ '#sk5') @ emptyset)))),
% 3.80/1.37 inference('sup-', [status(thm)], [zip_derived_cl35, zip_derived_cl81])).
% 3.80/1.37 thf(zip_derived_cl66, plain, ( (in @ '#sk5' @ '#sk1')),
% 3.80/1.37 inference('demod', [status(thm)], [zip_derived_cl65, zip_derived_cl28])).
% 3.80/1.37 thf(zip_derived_cl87, plain,
% 3.80/1.37 ((~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2')))
% 3.80/1.37 | ((dsetconstr @ '#sk2' @
% 3.80/1.37 ((('#C') @ ((('#B') @ in @ (kpair @ '#sk5'))) @ '#sk3')))
% 3.80/1.37 != (setadjoin @ ('#sk4' @ '#sk5') @ emptyset)))),
% 3.80/1.37 inference('demod', [status(thm)], [zip_derived_cl85, zip_derived_cl66])).
% 3.80/1.37 thf(zip_derived_cl102, plain,
% 3.80/1.37 ((((setadjoin @ ('#sk4' @ '#sk5') @ emptyset)
% 3.80/1.37 != (setadjoin @ ('#sk4' @ '#sk5') @ emptyset))
% 3.80/1.37 | ~ (in @ '#sk5' @ '#sk1')
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('sup-', [status(thm)], [zip_derived_cl37, zip_derived_cl87])).
% 3.80/1.37 thf(zip_derived_cl66, plain, ( (in @ '#sk5' @ '#sk1')),
% 3.80/1.37 inference('demod', [status(thm)], [zip_derived_cl65, zip_derived_cl28])).
% 3.80/1.37 thf(zip_derived_cl106, plain,
% 3.80/1.37 ((((setadjoin @ ('#sk4' @ '#sk5') @ emptyset)
% 3.80/1.37 != (setadjoin @ ('#sk4' @ '#sk5') @ emptyset))
% 3.80/1.37 | ~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2'))))),
% 3.80/1.37 inference('demod', [status(thm)], [zip_derived_cl102, zip_derived_cl66])).
% 3.80/1.37 thf(zip_derived_cl107, plain,
% 3.80/1.37 (~ (in @ '#sk3' @ (powerset @ (cartprod @ '#sk1' @ '#sk2')))),
% 3.80/1.37 inference('simplify', [status(thm)], [zip_derived_cl106])).
% 3.80/1.37 thf(zip_derived_cl109, plain,
% 3.80/1.37 (~ (subset @ '#sk3' @ (cartprod @ '#sk1' @ '#sk2'))),
% 3.80/1.37 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl107])).
% 3.80/1.37 thf(zip_derived_cl28, plain,
% 3.80/1.37 ( (subset @ '#sk3' @ (cartprod @ '#sk1' @ '#sk2'))),
% 3.80/1.37 inference('lazy_cnf_and', [status(thm)], [zip_derived_cl26])).
% 3.80/1.37 thf(zip_derived_cl110, plain, ($false),
% 3.80/1.37 inference('demod', [status(thm)], [zip_derived_cl109, zip_derived_cl28])).
% 3.80/1.37
% 3.80/1.37 % SZS output end Refutation
% 3.80/1.37
% 3.80/1.37
% 3.80/1.37 % Terminating...
% 4.16/1.54 % Runner terminated.
% 4.16/1.56 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------