%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM587+3 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.QrJAAA1p0l true
% Computer : n021.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:47:32 PM UTC 2025
% Result : Theorem 51.75s 8.09s
% Output : Refutation 51.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NUM587+3 : TPTP v9.2.0. Released v4.0.0.
% 0.00/0.12 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.QrJAAA1p0l true
% 0.10/0.32 % Computer : n021.cluster.edu
% 0.10/0.32 % Model : x86_64 x86_64
% 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.32 % Memory : 8042.1875MB
% 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.32 % CPULimit : 300
% 0.10/0.32 % WCLimit : 300
% 0.10/0.32 % DateTime : Wed Oct 1 16:16:38 EDT 2025
% 0.10/0.32 % CPUTime :
% 0.10/0.32 % Running portfolio for 300 s
% 0.10/0.32 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.32 % Number of cores: 8
% 0.10/0.33 % Python version: Python 3.6.8
% 0.10/0.33 % Running in FO mode
% 0.49/0.58 % Total configuration time : 435
% 0.49/0.58 % Estimated wc time : 1092
% 0.49/0.58 % Estimated cpu time (7 cpus) : 156.0
% 0.50/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.50/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.50/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.50/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.50/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.51/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.51/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 51.75/8.09 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 51.75/8.09 % Solved by fo/fo13.sh.
% 51.75/8.09 % done 3147 iterations in 7.308s
% 51.75/8.09 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 51.75/8.09 % SZS output start Refutation
% 51.75/8.09 thf(aSet0_type, type, aSet0: $i > $o).
% 51.75/8.09 thf(szDzozmdt0_type, type, szDzozmdt0: $i > $i).
% 51.75/8.09 thf(aFunction0_type, type, aFunction0: $i > $o).
% 51.75/8.09 thf(zip_tseitin_37_type, type, zip_tseitin_37: $i > $o).
% 51.75/8.09 thf(xQ_type, type, xQ: $i).
% 51.75/8.09 thf(slbdtsldtrb0_type, type, slbdtsldtrb0: $i > $i > $i).
% 51.75/8.09 thf(sdtlpdtrp0_type, type, sdtlpdtrp0: $i > $i > $i).
% 51.75/8.09 thf(zip_tseitin_48_type, type, zip_tseitin_48: $i > $i > $i > $o).
% 51.75/8.09 thf(xc_type, type, xc: $i).
% 51.75/8.09 thf(aElement0_type, type, aElement0: $i > $o).
% 51.75/8.09 thf(sbrdtbr0_type, type, sbrdtbr0: $i > $i).
% 51.75/8.09 thf(xS_type, type, xS: $i).
% 51.75/8.09 thf(zip_tseitin_38_type, type, zip_tseitin_38: $i > $i > $o).
% 51.75/8.09 thf(sdtlseqdt0_type, type, sdtlseqdt0: $i > $i > $o).
% 51.75/8.09 thf(zip_tseitin_39_type, type, zip_tseitin_39: $i > $i > $o).
% 51.75/8.09 thf(sk__34_type, type, sk__34: $i).
% 51.75/8.09 thf(sdtmndt0_type, type, sdtmndt0: $i > $i > $i).
% 51.75/8.09 thf(szmzizndt0_type, type, szmzizndt0: $i > $i).
% 51.75/8.09 thf(zip_tseitin_40_type, type, zip_tseitin_40: $i > $o).
% 51.75/8.09 thf(zip_tseitin_46_type, type, zip_tseitin_46: $i > $i > $i > $o).
% 51.75/8.09 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 51.75/8.09 thf(zip_tseitin_49_type, type, zip_tseitin_49: $i > $i > $o).
% 51.75/8.09 thf(xC_type, type, xC: $i).
% 51.75/8.09 thf(zip_tseitin_44_type, type, zip_tseitin_44: $i > $i > $o).
% 51.75/8.09 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 51.75/8.09 thf(xT_type, type, xT: $i).
% 51.75/8.09 thf(xk_type, type, xk: $i).
% 51.75/8.09 thf(xK_type, type, xK: $i).
% 51.75/8.09 thf(szNzAzT0_type, type, szNzAzT0: $i).
% 51.75/8.09 thf(xi_type, type, xi: $i).
% 51.75/8.09 thf(xN_type, type, xN: $i).
% 51.75/8.09 thf(xx_type, type, xx: $i).
% 51.75/8.09 thf(zip_tseitin_47_type, type, zip_tseitin_47: $i > $i > $i > $o).
% 51.75/8.09 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 51.75/8.09 thf(zip_tseitin_43_type, type, zip_tseitin_43: $i > $i > $o).
% 51.75/8.09 thf(zip_tseitin_42_type, type, zip_tseitin_42: $i > $i > $o).
% 51.75/8.09 thf(zip_tseitin_45_type, type, zip_tseitin_45: $i > $i > $o).
% 51.75/8.09 thf(zip_tseitin_41_type, type, zip_tseitin_41: $i > $i > $i > $o).
% 51.75/8.09 thf(sdtlcdtrc0_type, type, sdtlcdtrc0: $i > $i > $i).
% 51.75/8.09 thf(m__, conjecture, (aElementOf0 @ xx @ xT)).
% 51.75/8.09 thf(zf_stmt_0, negated_conjecture, (~( aElementOf0 @ xx @ xT )),
% 51.75/8.09 inference('cnf.neg', [status(esa)], [m__])).
% 51.75/8.09 thf(zip_derived_cl363, plain, (~ (aElementOf0 @ xx @ xT)),
% 51.75/8.09 inference('cnf', [status(esa)], [zf_stmt_0])).
% 51.75/8.09 thf(m__4263, axiom,
% 51.75/8.09 (( ?[W0:$i]:
% 51.75/8.09 ( ( ( sdtlpdtrp0 @ xc @ W0 ) =
% 51.75/8.09 ( sdtlpdtrp0 @
% 51.75/8.09 xc @ ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) &
% 51.75/8.09 ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xc ) ) ) ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 W0 @ ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 51.75/8.09 ( ( aElement0 @ W0 ) &
% 51.75/8.09 ( ( aElementOf0 @ W0 @ xQ ) |
% 51.75/8.09 ( ( W0 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ) ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 W0 @ ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 51.75/8.09 ( ( aElement0 @ W0 ) &
% 51.75/8.09 ( ( aElementOf0 @ W0 @ xQ ) |
% 51.75/8.09 ( ( W0 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ) ) &
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ ( sdtlpdtrp0 @ xN @ xi ) ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 51.75/8.09 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 51.75/8.09 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) &
% 51.75/8.09 ( aSet0 @ ( sdtpldt0 @ xQ @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ))).
% 51.75/8.09 thf(zip_derived_cl361, plain,
% 51.75/8.09 (((sdtlpdtrp0 @ xc @ sk__34)
% 51.75/8.09 = (sdtlpdtrp0 @ xc @
% 51.75/8.09 (sdtpldt0 @ xQ @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi)))))),
% 51.75/8.09 inference('cnf', [status(esa)], [m__4263])).
% 51.75/8.09 thf(m__4151, axiom,
% 51.75/8.09 (( aFunction0 @ xC ) & ( ( szDzozmdt0 @ xC ) = ( szNzAzT0 ) ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 51.75/8.09 ( ( ![W1:$i]:
% 51.75/8.09 ( ( ( ( ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 51.75/8.09 ( sdtlseqdt0 @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W2 ) ) ) &
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) ) ) =>
% 51.75/8.09 ( ( ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 W2 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 51.75/8.09 ( ( ( W2 ) !=
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) &
% 51.75/8.09 ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 51.75/8.09 ( aElement0 @ W2 ) ) ) ) &
% 51.75/8.09 ( aSet0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) =>
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 W1 @
% 51.75/8.09 ( slbdtsldtrb0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) @
% 51.75/8.09 xk ) ) |
% 51.75/8.09 ( ( ( sbrdtbr0 @ W1 ) = ( xk ) ) &
% 51.75/8.09 ( ( aSubsetOf0 @
% 51.75/8.09 W1 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) |
% 51.75/8.09 ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W2 @ W1 ) =>
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 W2 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) ) ) ) ) ) &
% 51.75/8.09 ( aSet0 @ W1 ) ) =>
% 51.75/8.09 ( ( ( sdtlpdtrp0 @ ( sdtlpdtrp0 @ xC @ W0 ) @ W1 ) =
% 51.75/8.09 ( sdtlpdtrp0 @
% 51.75/8.09 xc @
% 51.75/8.09 ( sdtpldt0 @
% 51.75/8.09 W1 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) &
% 51.75/8.09 ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 W2 @
% 51.75/8.09 ( sdtpldt0 @
% 51.75/8.09 W1 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 51.75/8.09 ( ( ( ( W2 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) |
% 51.75/8.09 ( aElementOf0 @ W2 @ W1 ) ) &
% 51.75/8.09 ( aElement0 @ W2 ) ) ) ) &
% 51.75/8.09 ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 51.75/8.09 ( sdtlseqdt0 @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W2 ) ) ) &
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) &
% 51.75/8.09 ( ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) =
% 51.75/8.09 ( slbdtsldtrb0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) @
% 51.75/8.09 xk ) ) &
% 51.75/8.09 ( ![W1:$i]:
% 51.75/8.09 ( ( ( aElementOf0 @ W1 @ ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) ) =>
% 51.75/8.09 ( ( ( sbrdtbr0 @ W1 ) = ( xk ) ) &
% 51.75/8.09 ( aSubsetOf0 @
% 51.75/8.09 W1 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 51.75/8.09 ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W2 @ W1 ) =>
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 W2 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 51.75/8.09 ( aSet0 @ W1 ) ) ) &
% 51.75/8.09 ( ( ( ( sbrdtbr0 @ W1 ) = ( xk ) ) &
% 51.75/8.09 ( ( aSubsetOf0 @
% 51.75/8.09 W1 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) |
% 51.75/8.09 ( ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W2 @ W1 ) =>
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 W2 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 51.75/8.09 ( aSet0 @ W1 ) ) ) ) =>
% 51.75/8.09 ( aElementOf0 @ W1 @ ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) ) ) ) ) &
% 51.75/8.09 ( ![W1:$i]:
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 W1 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 51.75/8.09 ( ( ( W1 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) &
% 51.75/8.09 ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 51.75/8.09 ( aElement0 @ W1 ) ) ) ) &
% 51.75/8.09 ( aSet0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 51.75/8.09 ( ![W1:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 51.75/8.09 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W1 ) ) ) &
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 51.75/8.09 ( aFunction0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) ) ) ))).
% 51.75/8.09 thf(zf_stmt_1, axiom,
% 51.75/8.09 (![W1:$i,W0:$i]:
% 51.75/8.09 ( ( zip_tseitin_49 @ W1 @ W0 ) =>
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 51.75/8.09 ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 51.75/8.09 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W2 ) ) ) &
% 51.75/8.09 ( ![W2:$i]: ( zip_tseitin_48 @ W2 @ W1 @ W0 ) ) &
% 51.75/8.09 ( ( sdtlpdtrp0 @ ( sdtlpdtrp0 @ xC @ W0 ) @ W1 ) =
% 51.75/8.09 ( sdtlpdtrp0 @
% 51.75/8.09 xc @ ( sdtpldt0 @ W1 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) ))).
% 51.75/8.09 thf(zip_derived_cl312, plain,
% 51.75/8.09 (![X0 : $i, X1 : $i]:
% 51.75/8.09 (((sdtlpdtrp0 @ (sdtlpdtrp0 @ xC @ X1) @ X0)
% 51.75/8.09 = (sdtlpdtrp0 @ xc @
% 51.75/8.09 (sdtpldt0 @ X0 @ (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X1)))))
% 51.75/8.09 | ~ (zip_tseitin_49 @ X0 @ X1))),
% 51.75/8.09 inference('cnf', [status(esa)], [zf_stmt_1])).
% 51.75/8.09 thf(zip_derived_cl3645, plain,
% 51.75/8.09 ((((sdtlpdtrp0 @ (sdtlpdtrp0 @ xC @ xi) @ xQ)
% 51.75/8.09 = (sdtlpdtrp0 @ xc @ sk__34))
% 51.75/8.09 | ~ (zip_tseitin_49 @ xQ @ xi))),
% 51.75/8.09 inference('s_sup+', [status(thm)], [zip_derived_cl361, zip_derived_cl312])).
% 51.75/8.09 thf(m__4237, axiom,
% 51.75/8.09 (( ( sdtlpdtrp0 @ ( sdtlpdtrp0 @ xC @ xi ) @ xQ ) = ( xx ) ) &
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 xQ @
% 51.75/8.09 ( slbdtsldtrb0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ xi ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) @
% 51.75/8.09 xk ) ) &
% 51.75/8.09 ( ( sbrdtbr0 @ xQ ) = ( xk ) ) &
% 51.75/8.09 ( aSubsetOf0 @
% 51.75/8.09 xQ @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ xi ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W0 @ xQ ) =>
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 W0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ xi ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ) &
% 51.75/8.09 ( aSet0 @ xQ ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 W0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ xi ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) <=>
% 51.75/8.09 ( ( aElement0 @ W0 ) &
% 51.75/8.09 ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) &
% 51.75/8.09 ( ( W0 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) ) ) &
% 51.75/8.09 ( aSet0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ xi ) @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) ) ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W0 @ ( sdtlpdtrp0 @ xN @ xi ) ) =>
% 51.75/8.09 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ W0 ) ) ) &
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ xi ) ) @ ( sdtlpdtrp0 @ xN @ xi ) ))).
% 51.75/8.09 thf(zip_derived_cl348, plain,
% 51.75/8.09 (((sdtlpdtrp0 @ (sdtlpdtrp0 @ xC @ xi) @ xQ) = (xx))),
% 51.75/8.09 inference('cnf', [status(esa)], [m__4237])).
% 51.75/8.09 thf(zip_derived_cl3648, plain,
% 51.75/8.09 ((((xx) = (sdtlpdtrp0 @ xc @ sk__34)) | ~ (zip_tseitin_49 @ xQ @ xi))),
% 51.75/8.09 inference('demod', [status(thm)], [zip_derived_cl3645, zip_derived_cl348])).
% 51.75/8.09 thf(zip_derived_cl347, plain,
% 51.75/8.09 ( (aElementOf0 @ xQ @
% 51.75/8.09 (slbdtsldtrb0 @
% 51.75/8.09 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ xi) @
% 51.75/8.09 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ xi))) @
% 51.75/8.09 xk))),
% 51.75/8.09 inference('cnf', [status(esa)], [m__4237])).
% 51.75/8.09 thf(zf_stmt_2, axiom,
% 51.75/8.09 (![W1:$i,W0:$i]:
% 51.75/8.09 ( ( ( ( zip_tseitin_42 @ W1 @ W0 ) & ( ( sbrdtbr0 @ W1 ) = ( xk ) ) ) |
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 W1 @
% 51.75/8.09 ( slbdtsldtrb0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) @
% 51.75/8.09 xk ) ) ) =>
% 51.75/8.09 ( zip_tseitin_43 @ W1 @ W0 ) ))).
% 51.75/8.09 thf(zip_derived_cl296, plain,
% 51.75/8.09 (![X0 : $i, X1 : $i]:
% 51.75/8.09 ( (zip_tseitin_43 @ X0 @ X1)
% 51.75/8.09 | ~ (aElementOf0 @ X0 @
% 51.75/8.09 (slbdtsldtrb0 @
% 51.75/8.09 (sdtmndt0 @ (sdtlpdtrp0 @ xN @ X1) @
% 51.75/8.09 (szmzizndt0 @ (sdtlpdtrp0 @ xN @ X1))) @
% 51.75/8.09 xk)))),
% 51.75/8.09 inference('cnf', [status(esa)], [zf_stmt_2])).
% 51.75/8.09 thf(zip_derived_cl3005, plain, ( (zip_tseitin_43 @ xQ @ xi)),
% 51.75/8.09 inference('s_sup-', [status(thm)], [zip_derived_cl347, zip_derived_cl296])).
% 51.75/8.09 thf(zf_stmt_3, axiom,
% 51.75/8.09 (![W1:$i,W0:$i]:
% 51.75/8.09 ( ( ( zip_tseitin_40 @ W0 ) => ( zip_tseitin_43 @ W1 @ W0 ) ) =>
% 51.75/8.09 ( zip_tseitin_44 @ W1 @ W0 ) ))).
% 51.75/8.09 thf(zip_derived_cl297, plain,
% 51.75/8.09 (![X0 : $i, X1 : $i]:
% 51.75/8.09 ( (zip_tseitin_44 @ X0 @ X1) | ~ (zip_tseitin_43 @ X0 @ X1))),
% 51.75/8.09 inference('cnf', [status(esa)], [zf_stmt_3])).
% 51.75/8.09 thf(zip_derived_cl3007, plain, ( (zip_tseitin_44 @ xQ @ xi)),
% 51.75/8.09 inference('s_sup-', [status(thm)],
% 51.75/8.09 [zip_derived_cl3005, zip_derived_cl297])).
% 51.75/8.09 thf(zf_stmt_4, axiom,
% 51.75/8.09 (![W1:$i,W0:$i]:
% 51.75/8.09 ( ( ( zip_tseitin_37 @ W0 ) => ( zip_tseitin_44 @ W1 @ W0 ) ) =>
% 51.75/8.09 ( zip_tseitin_45 @ W1 @ W0 ) ))).
% 51.75/8.09 thf(zip_derived_cl299, plain,
% 51.75/8.09 (![X0 : $i, X1 : $i]:
% 51.75/8.09 ( (zip_tseitin_45 @ X0 @ X1) | ~ (zip_tseitin_44 @ X0 @ X1))),
% 51.75/8.09 inference('cnf', [status(esa)], [zf_stmt_4])).
% 51.75/8.09 thf(zip_derived_cl3009, plain, ( (zip_tseitin_45 @ xQ @ xi)),
% 51.75/8.09 inference('s_sup-', [status(thm)],
% 51.75/8.09 [zip_derived_cl3007, zip_derived_cl299])).
% 51.75/8.09 thf(m__4200, axiom, (aElementOf0 @ xi @ szNzAzT0)).
% 51.75/8.09 thf(zip_derived_cl332, plain, ( (aElementOf0 @ xi @ szNzAzT0)),
% 51.75/8.09 inference('cnf', [status(esa)], [m__4200])).
% 51.75/8.09 thf(zf_stmt_5, type, zip_tseitin_49 : $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_6, type, zip_tseitin_48 : $i > $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_7, axiom,
% 51.75/8.09 (![W2:$i,W1:$i,W0:$i]:
% 51.75/8.09 ( ( zip_tseitin_48 @ W2 @ W1 @ W0 ) =>
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 W2 @ ( sdtpldt0 @ W1 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 51.75/8.09 ( zip_tseitin_47 @ W2 @ W1 @ W0 ) ) ))).
% 51.75/8.09 thf(zf_stmt_8, type, zip_tseitin_47 : $i > $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_9, axiom,
% 51.75/8.09 (![W2:$i,W1:$i,W0:$i]:
% 51.75/8.09 ( ( zip_tseitin_47 @ W2 @ W1 @ W0 ) <=>
% 51.75/8.09 ( ( aElement0 @ W2 ) & ( zip_tseitin_46 @ W2 @ W1 @ W0 ) ) ))).
% 51.75/8.09 thf(zf_stmt_10, type, zip_tseitin_46 : $i > $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_11, axiom,
% 51.75/8.09 (![W2:$i,W1:$i,W0:$i]:
% 51.75/8.09 ( ( zip_tseitin_46 @ W2 @ W1 @ W0 ) <=>
% 51.75/8.09 ( ( aElementOf0 @ W2 @ W1 ) |
% 51.75/8.09 ( ( W2 ) = ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ))).
% 51.75/8.09 thf(zf_stmt_12, type, zip_tseitin_45 : $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_13, type, zip_tseitin_44 : $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_14, type, zip_tseitin_43 : $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_15, type, zip_tseitin_42 : $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_16, axiom,
% 51.75/8.09 (![W1:$i,W0:$i]:
% 51.75/8.09 ( ( ( ![W2:$i]: ( zip_tseitin_41 @ W2 @ W1 @ W0 ) ) |
% 51.75/8.09 ( aSubsetOf0 @
% 51.75/8.09 W1 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) =>
% 51.75/8.09 ( zip_tseitin_42 @ W1 @ W0 ) ))).
% 51.75/8.09 thf(zf_stmt_17, type, zip_tseitin_41 : $i > $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_18, axiom,
% 51.75/8.09 (![W2:$i,W1:$i,W0:$i]:
% 51.75/8.09 ( ( ( aElementOf0 @ W2 @ W1 ) =>
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 W2 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) =>
% 51.75/8.09 ( zip_tseitin_41 @ W2 @ W1 @ W0 ) ))).
% 51.75/8.09 thf(zf_stmt_19, type, zip_tseitin_40 : $i > $o).
% 51.75/8.09 thf(zf_stmt_20, axiom,
% 51.75/8.09 (![W0:$i]:
% 51.75/8.09 ( ( zip_tseitin_40 @ W0 ) =>
% 51.75/8.09 ( ( aSet0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 51.75/8.09 ( ![W2:$i]: ( zip_tseitin_39 @ W2 @ W0 ) ) ) ))).
% 51.75/8.09 thf(zf_stmt_21, type, zip_tseitin_39 : $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_22, axiom,
% 51.75/8.09 (![W2:$i,W0:$i]:
% 51.75/8.09 ( ( zip_tseitin_39 @ W2 @ W0 ) =>
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 W2 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 51.75/8.09 ( zip_tseitin_38 @ W2 @ W0 ) ) ))).
% 51.75/8.09 thf(zf_stmt_23, type, zip_tseitin_38 : $i > $i > $o).
% 51.75/8.09 thf(zf_stmt_24, axiom,
% 51.75/8.09 (![W2:$i,W0:$i]:
% 51.75/8.09 ( ( zip_tseitin_38 @ W2 @ W0 ) <=>
% 51.75/8.09 ( ( aElement0 @ W2 ) &
% 51.75/8.09 ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 51.75/8.09 ( ( W2 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ))).
% 51.75/8.09 thf(zf_stmt_25, type, zip_tseitin_37 : $i > $o).
% 51.75/8.09 thf(zf_stmt_26, axiom,
% 51.75/8.09 (![W0:$i]:
% 51.75/8.09 ( ( zip_tseitin_37 @ W0 ) =>
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 51.75/8.09 ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W2 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 51.75/8.09 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W2 ) ) ) ) ))).
% 51.75/8.09 thf(zf_stmt_27, axiom,
% 51.75/8.09 (( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W0 @ szNzAzT0 ) =>
% 51.75/8.09 ( ( aFunction0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) &
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 51.75/8.09 ( ![W1:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) =>
% 51.75/8.09 ( sdtlseqdt0 @ ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) @ W1 ) ) ) &
% 51.75/8.09 ( aSet0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 51.75/8.09 ( ![W1:$i]:
% 51.75/8.09 ( ( aElementOf0 @
% 51.75/8.09 W1 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) <=>
% 51.75/8.09 ( ( aElement0 @ W1 ) &
% 51.75/8.09 ( aElementOf0 @ W1 @ ( sdtlpdtrp0 @ xN @ W0 ) ) &
% 51.75/8.09 ( ( W1 ) != ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 51.75/8.09 ( ![W1:$i]:
% 51.75/8.09 ( ( ( ( ( ( aSet0 @ W1 ) &
% 51.75/8.09 ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W2 @ W1 ) =>
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 W2 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) ) |
% 51.75/8.09 ( aSubsetOf0 @
% 51.75/8.09 W1 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) &
% 51.75/8.09 ( ( sbrdtbr0 @ W1 ) = ( xk ) ) ) =>
% 51.75/8.09 ( aElementOf0 @ W1 @ ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) ) ) &
% 51.75/8.09 ( ( aElementOf0 @ W1 @ ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) ) =>
% 51.75/8.09 ( ( aSet0 @ W1 ) &
% 51.75/8.09 ( ![W2:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W2 @ W1 ) =>
% 51.75/8.09 ( aElementOf0 @
% 51.75/8.09 W2 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) ) ) &
% 51.75/8.09 ( aSubsetOf0 @
% 51.75/8.09 W1 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) ) &
% 51.75/8.09 ( ( sbrdtbr0 @ W1 ) = ( xk ) ) ) ) ) ) &
% 51.75/8.09 ( ( szDzozmdt0 @ ( sdtlpdtrp0 @ xC @ W0 ) ) =
% 51.75/8.09 ( slbdtsldtrb0 @
% 51.75/8.09 ( sdtmndt0 @
% 51.75/8.09 ( sdtlpdtrp0 @ xN @ W0 ) @
% 51.75/8.09 ( szmzizndt0 @ ( sdtlpdtrp0 @ xN @ W0 ) ) ) @
% 51.75/8.09 xk ) ) &
% 51.75/8.09 ( ![W1:$i]:
% 51.75/8.09 ( ( ( aSet0 @ W1 ) & ( zip_tseitin_45 @ W1 @ W0 ) ) =>
% 51.75/8.09 ( zip_tseitin_49 @ W1 @ W0 ) ) ) ) ) ) &
% 51.75/8.09 ( ( szDzozmdt0 @ xC ) = ( szNzAzT0 ) ) & ( aFunction0 @ xC ))).
% 51.75/8.09 thf(zip_derived_cl331, plain,
% 51.75/8.09 (![X0 : $i, X1 : $i]:
% 51.75/8.09 (~ (aSet0 @ X0)
% 51.75/8.09 | ~ (zip_tseitin_45 @ X0 @ X1)
% 51.75/8.09 | (zip_tseitin_49 @ X0 @ X1)
% 51.75/8.09 | ~ (aElementOf0 @ X1 @ szNzAzT0))),
% 51.75/8.09 inference('cnf', [status(esa)], [zf_stmt_27])).
% 51.75/8.09 thf(zip_derived_cl1069, plain,
% 51.75/8.09 (![X0 : $i]:
% 51.75/8.09 (~ (aSet0 @ X0)
% 51.75/8.09 | ~ (zip_tseitin_45 @ X0 @ xi)
% 51.75/8.09 | (zip_tseitin_49 @ X0 @ xi))),
% 51.75/8.09 inference('s_sup-', [status(thm)], [zip_derived_cl332, zip_derived_cl331])).
% 51.75/8.09 thf(zip_derived_cl21670, plain,
% 51.75/8.09 ((~ (aSet0 @ xQ) | (zip_tseitin_49 @ xQ @ xi))),
% 51.75/8.09 inference('s_sup-', [status(thm)],
% 51.75/8.09 [zip_derived_cl3009, zip_derived_cl1069])).
% 51.75/8.09 thf(zip_derived_cl343, plain, ( (aSet0 @ xQ)),
% 51.75/8.09 inference('cnf', [status(esa)], [m__4237])).
% 51.75/8.09 thf(zip_derived_cl21671, plain, ( (zip_tseitin_49 @ xQ @ xi)),
% 51.75/8.09 inference('demod', [status(thm)],
% 51.75/8.09 [zip_derived_cl21670, zip_derived_cl343])).
% 51.75/8.09 thf(zip_derived_cl21672, plain, (((xx) = (sdtlpdtrp0 @ xc @ sk__34))),
% 51.75/8.09 inference('demod', [status(thm)],
% 51.75/8.09 [zip_derived_cl3648, zip_derived_cl21671])).
% 51.75/8.09 thf(m__3453, axiom,
% 51.75/8.09 (( aSubsetOf0 @ ( sdtlcdtrc0 @ xc @ ( szDzozmdt0 @ xc ) ) @ xT ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W0 @ ( sdtlcdtrc0 @ xc @ ( szDzozmdt0 @ xc ) ) ) =>
% 51.75/8.09 ( aElementOf0 @ W0 @ xT ) ) ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W0 @ ( sdtlcdtrc0 @ xc @ ( szDzozmdt0 @ xc ) ) ) <=>
% 51.75/8.09 ( ?[W1:$i]:
% 51.75/8.09 ( ( ( sdtlpdtrp0 @ xc @ W1 ) = ( W0 ) ) &
% 51.75/8.09 ( aElementOf0 @ W1 @ ( szDzozmdt0 @ xc ) ) ) ) ) ) &
% 51.75/8.09 ( aSet0 @ ( sdtlcdtrc0 @ xc @ ( szDzozmdt0 @ xc ) ) ) &
% 51.75/8.09 ( ( szDzozmdt0 @ xc ) = ( slbdtsldtrb0 @ xS @ xK ) ) &
% 51.75/8.09 ( ![W0:$i]:
% 51.75/8.09 ( ( ( ( ( ( aSet0 @ W0 ) &
% 51.75/8.09 ( ![W1:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W1 @ W0 ) => ( aElementOf0 @ W1 @ xS ) ) ) ) |
% 51.75/8.09 ( aSubsetOf0 @ W0 @ xS ) ) &
% 51.75/8.09 ( ( sbrdtbr0 @ W0 ) = ( xK ) ) ) =>
% 51.75/8.09 ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xc ) ) ) &
% 51.75/8.09 ( ( aElementOf0 @ W0 @ ( szDzozmdt0 @ xc ) ) =>
% 51.75/8.09 ( ( aSet0 @ W0 ) &
% 51.75/8.09 ( ![W1:$i]:
% 51.75/8.09 ( ( aElementOf0 @ W1 @ W0 ) => ( aElementOf0 @ W1 @ xS ) ) ) &
% 51.75/8.09 ( aSubsetOf0 @ W0 @ xS ) & ( ( sbrdtbr0 @ W0 ) = ( xK ) ) ) ) ) ) &
% 51.75/8.09 ( aFunction0 @ xc ))).
% 51.75/8.09 thf(zip_derived_cl164, plain,
% 51.75/8.09 (![X0 : $i]:
% 51.75/8.09 ( (aElementOf0 @ X0 @ xT)
% 51.75/8.09 | ~ (aElementOf0 @ X0 @ (sdtlcdtrc0 @ xc @ (szDzozmdt0 @ xc))))),
% 51.75/8.09 inference('cnf', [status(esa)], [m__3453])).
% 51.75/8.09 thf(zip_derived_cl161, plain,
% 51.75/8.09 (![X0 : $i, X1 : $i]:
% 51.75/8.09 ( (aElementOf0 @ X0 @ (sdtlcdtrc0 @ xc @ (szDzozmdt0 @ xc)))
% 51.75/8.09 | ~ (aElementOf0 @ X1 @ (szDzozmdt0 @ xc))
% 51.75/8.09 | ((sdtlpdtrp0 @ xc @ X1) != (X0)))),
% 51.75/8.09 inference('cnf', [status(esa)], [m__3453])).
% 51.75/8.09 thf(zip_derived_cl2904, plain,
% 51.75/8.09 (![X0 : $i, X1 : $i]:
% 51.75/8.09 ( (aElementOf0 @ X0 @ xT)
% 51.75/8.09 | ~ (aElementOf0 @ X1 @ (szDzozmdt0 @ xc))
% 51.75/8.09 | ((sdtlpdtrp0 @ xc @ X1) != (X0)))),
% 51.75/8.09 inference('s_sup+', [status(thm)], [zip_derived_cl164, zip_derived_cl161])).
% 51.75/8.09 thf(zip_derived_cl21703, plain,
% 51.75/8.09 (![X0 : $i]:
% 51.75/8.09 ( (aElementOf0 @ X0 @ xT)
% 51.75/8.09 | ~ (aElementOf0 @ sk__34 @ (szDzozmdt0 @ xc))
% 51.75/8.09 | ((xx) != (X0)))),
% 51.75/8.09 inference('s_sup-', [status(thm)],
% 51.75/8.09 [zip_derived_cl21672, zip_derived_cl2904])).
% 51.75/8.09 thf(zip_derived_cl362, plain, ( (aElementOf0 @ sk__34 @ (szDzozmdt0 @ xc))),
% 51.75/8.09 inference('cnf', [status(esa)], [m__4263])).
% 51.75/8.09 thf(zip_derived_cl21711, plain,
% 51.75/8.09 (![X0 : $i]: ( (aElementOf0 @ X0 @ xT) | ((xx) != (X0)))),
% 51.75/8.09 inference('demod', [status(thm)],
% 51.75/8.09 [zip_derived_cl21703, zip_derived_cl362])).
% 51.75/8.09 thf(zip_derived_cl21712, plain, ( (aElementOf0 @ xx @ xT)),
% 51.75/8.09 inference('eq_res', [status(thm)], [zip_derived_cl21711])).
% 51.75/8.09 thf(zip_derived_cl21713, plain, ($false),
% 51.75/8.09 inference('demod', [status(thm)],
% 51.75/8.09 [zip_derived_cl363, zip_derived_cl21712])).
% 51.75/8.09
% 51.75/8.09 % SZS output end Refutation
% 51.75/8.09
% 51.75/8.09
% 51.75/8.09 % Terminating...
% 52.31/8.15 % Runner terminated.
% 52.31/8.17 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------